-
Notifications
You must be signed in to change notification settings - Fork 4
Eric's Notes Page 2
Page 2 of 2
These are the notes I keep for the project. Do not take everything here to be correct as I learn as I go.
I try to add any information I find relevant or that might be of use to someone new coming to this project. There are things I take for granted so if you have a question about something in my notes please ask. These notes are for everyone and not just me. As these are notes, they will not be well organized, just a common place to hold information of relevance.
07/28/13
In trying to identify the signatures used for the choice conversion I used the object browser within Visual Studio.
I used a custom component set consisting of NHol and Extcore.
When looking for failwithf in Object Browser I could not find it. Checking the ExtCore source code
/// Creates a Choice representing an error value.
/// The error value in the Choice is the specified formatted error message.
[<CompiledName("PrintFormatToStringThenFail")>]
let inline failwithf (fmt : Printf.StringFormat<'T, Choice<'U, string>>) =
Printf.ksprintf failwith fmt
it became obvious that the use of the CompiledName attribute was changing the name.
Signatures of functions used with Choice conversion.
x - used in code
The standard failwith function that just generates an exception with a message.
x Microsoft.FSharp.Core.Operators.failwith (msg : string) : ('T)
Used to add exception to return value within a Choice.
ExtCore.Choice.error (value : 'T) : (Choice<'T, 'Error>)
x ExtCore.Choice.result (value : 'T) : (Choice<'T, 'Error>)
x NHol.lib.Choice.failwith (msg : string) : (Choice<'T, System.Exception>)
ExtCore.Choice.failwith (msg : string) : (Choice<'T, System.Exception>)
ExtCore.Control.Choice.failwith (msg : string) : (Choice<'T, System.Exception>)
x NHol.lib.Choice.attempt (f : unit -> 'T) : (Choice<'T, System.Exception>)
x NHol.lib.Choice.fail (() : unit) : (Choice<'T, System.Exception>)
x NHol.lib.Choice.nestedFailwith (innerException : System.Exception) (message : string) : (Choice<'T, System.Exception>)
x NHol.lib.Choice.failwithPair (s : string) : (Choice<'T, System.Exception> * Choice<'U, System.Exception>)
NHol.lib.Choice.pair ((x : 'T), (y : 'U) : (Choice<'T, 'V> * Choice<'U, 'V>)
Will remove exception from Choice result.
Used during conversion phase; these are temporarily used to make the functions compile by discarding the exception so as not to pass to the calling function until the calling function can handle the Choice with exception.
x NHol.lib.Choice.fill (defaultResult : 'T) (value : Choice<'T, 'Error>) : 'T
x NHol.lib.Choice.toOption (value : Choice<'T, 'Error>) : ('T Option)
ExtCore.Choice.exists (predicate : 'T -> bool) (value : Choice<'T, 'Error>) : bool
ExtCore.Choice.fold (folder : 'State -> 'T -> 'State) (state : 'State) (value : Choice<'T, 'Error>) : 'State
ExtCore.Choice.foldBack (folder : 'T -> 'State -> 'State) (value : Choice<'T, 'Error>) (state : 'State) : 'State
ExtCore.Choice.forall (predicate : 'T -> bool) (value : Choice<'T, 'Error>) : bool
ExtCore.Choice.isError (value : Choice<'T, 'Error>) : bool
x ExtCore.Choice.isResult (value : Choice<'T, 'Error>) : bool
ExtCore.Choice.failwithf (fmt : Printf.StringFormat<'T, Choice<'U, System.Exception>> -> 'T) : 'T
ExtCore.Control.Choice.bindOrFail (x : Choice<'T,string>) : 'T
x ExtCore.Control.Choice.bindOrRaise (x : Choice<'T, System.Exception>) : 'T
x ExtCore.Choice.get (value : Choice<'T, 'Error>) : 'T
Used to pass exception from called function to calling function.
x NHol.lib.Choice.bindEither (resultBinding : 'T -> Choice<'U,'Failure>) (errorBinding : 'Error -> Choice<'U,'Failure>) (value : Choice<'T, 'Error>) : (Choice<'U, 'Failure>)
x NHol.lib.Choice.bindError (binding : ('Error -> Choice<'T,'Failure>)) (value : Choice<'T, 'Error>) : (Choice<'T, 'Failure>)
x NHol.lib.Choice.attemptNested (f : unit -> Choice<'T,System.Exception>) : (Choice<'T, System.Exception>)
NHol.lib.Choice.nestedFailwithPair (innerException : System.Exception) (message : string) : (Choice<'T, System.Exception> * Choice<'U, System.Exception>)
x ExtCore.Choice.map (mapping : 'T -> 'U) (value : Choice<'T, 'Error>) : (Choice<'U, 'Error>)
x ExtCore.Choice.bind (binding : 'T -> Choice<'U,'Error>) (value : Choice<'T, 'Error>) : (Choice<'U, 'Error>)
x ExtCore.Choice.bind2 (binding : 'T -> 'U -> Choice<'V,'Error>) (value1 : Choice<'T, 'Error>) (value2 : Choice<'U,'Error>) : (Choice<'V, 'Error>)
x ExtCore.Choice.mapError (mapping : 'Err1 -> 'Err2) (value : Choice<'T, 'Err1>) : (Choice<'T, 'Err2>)
ExtCore.Control.Choice.setError (error : 'Error) : (Choice<'T, 'Error>)
ExtCore.Choice.iter (action : 'T -> unit) (value : Choice<'T, 'Error>) : unit
When trying to add some images to a Github wiki pages I ran across GitHub Pages; looks interesting.
Some pages of note relating Haskell either:
Any module that exposes interesting functions for Choice type?
Data.Either
08/02/13
For the removing exceptions branch with this change, one can no longer test the code from within Visual Studio by selecting the code and sending to the FSI window. The preferred way to run the code is to use the HOL Light short cut.
08/03/13
I created a version of the project files to run with VS 2010 but only for the removing exceptions branch. When I tried to use NUnit with the generated code I received an error which was caused because all of the code uses F# 3 and VS 2010 only has F# 2 installed. The typical way to get F# is to use VS 2012. As I did not want to install VS2012 on the same machine as VS2010 I installed F# 3 using the F# Tools for Visual Studio 2012 Express for Web. See Option 4: Install the F# compiler and tools alone
08/04/13
Ran into the Experimental attribute in this push.
//
let [<Literal>] private normalize_ratio_warning =
"Ratio.normalize_ratio does not actually normalize the value \
(the functionality has not yet been implemented), so other functions \
which rely on that invariant will not work properly."
// NOTE : not sure what kind of normalization should be done here
// TODO : Implement this function correctly in the next version of
// FSharp.Compatibility.OCaml, then upgrade to that version ASAP.
[<Experimental(normalize_ratio_warning)>]
let normalize_ratio x =
Debug.Write "Warning: "
Debug.WriteLine normalize_ratio_warning
x
Notice how the Experimental attribute makes use of the string with the Literal attribute and the Literal attribute is within the let statement.
08/08/13
When using F# Interactive, if you get an exception like
> System.Exception: Division_by_zero ---> System.DivideByZeroException: Attempted to divide by zero.
--- End of inner exception stack trace ---
at FSharp.Compatibility.OCaml.NumModule.Num.op_Division(Num x, Num y)
at <StartupCode$FSI_0014>.$FSI_0014.main@()
Stopped due to error
and want to get back to the F# Interactive prompt >
, you do not have to Cancel Interactive Evaluation
or Reset Interactive Session
, just enter ;;
, i.e.
;;
>
I had a need to work with the type FSharp.Compatibility.OCaml.Ratio.BigRationalLarge
in F# Interactive.
When I created a type, e.g. Ratio.BigRationalLarge.Rational (7,2);;
F# Interactive would respond with
val it : Ratio.BigRationalLarge = Q (7 {IsEven = false;
IsOne = false;
IsPowerOfTwo = false;
IsZero = false;
Sign = 1;},2 {IsEven = true;
IsOne = false;
IsPowerOfTwo = true;
IsZero = false;
Sign = 1;})
which was a bit verbose. So I decided to override the printer with fsi.AddPrinter
let printBigRationalLarge (r : FSharp.Compatibility.OCaml.Ratio.BigRationalLarge) = r.ToString()
fsi.AddPrinter printBigRationalLarge;;
and now get
val it : Ratio.BigRationalLarge = 7/2
which is much nicer.
However if I did this
let x2 = Ratio.BigRationalLarge.Rational (7,2);;
printfn "%A" x2;;
with or without fsi.AddPrinter printBigRationalLarge;;
I would always get
Q (7,2)
val it : unit = ()
08/10/13
__SOURCE_DIRECTORY__
can cause problems if you don't understand
how it works with F# Interactive.
To see the value of __SOURCE_DIRECTORY__
just use printfn "%A" __SOURCE_DIRECTORY__;;
If you type directly into F# Interactive window within Visual Studio will get
the temp directory for the user profile, e.g.
C:\Users\Eric.Windows7Ult\AppData\Local\Temp
If sent to F# Interactive window in Visual Studio from fsx script you will get
the directory where the fsx script is located. e.g.
E:\Projects\Github\NHol\NHol
If used in fsi.exe, running fsi.exe from a command prompt, you will get
the directory where fsi.exe is located, e.g.
C:\Program Files (x86)\Microsoft F#\v4.0
If fsi.exe is started from a Windows Explorer search, you will get
the directory where Windows Explorer is located, e.g.
C:\Windows\system32
If fis.exe is started from a batch command, you will get
the directory where the batch command is located, e.g.
E:\Projects
If __SOURCE_DIRECTORY__
is so unstable then why use it? It is stable within a compiled application, it is unstable when used with a stand alone F# Interactive.
08/13/13
I often need to run bat scripts in a Windows command prompt. To quickly open a command prompt to the directory where the script is lactated one can
- Open
Windows Explorer
- Navigate to folder with bat file
- Press
Shift
andRight click
right panel of windows explorer - Select
Open command window here
or
- Open
Windows Explorer
- Navigate to folder with bat file
- In
Windows Explorer
location bar entercmd
The Logging support and setup code has been moved into a module for obvious reasons.
The Logging module now has the RequireQualifiedAccess
Attribute. If you look at the Logging.fs file
you will see that it is a module named Logging
module NHol.Logging
with an inner module named Logging
module Logging =
so to use the function in this inner module you would call them fully qualified with
NHol.Logging.Logging.configureNLogProgramatically ()
but that is to long so you naturally add an open statement
open NHol.Logging.Logging
however doing this results in
error FS0892: This declaration opens the module 'FSI_0002.NHol.Logging.Logging',
which is marked as 'RequireQualifiedAccess'. Adjust your code to use qualified
references to the elements of the module instead, e.g. 'List.map' instead of 'map'.
This change will ensure that your code is robust as new constructs are added to libraries.
So to use this without fully qualified names use
open NHol.Logging
Logging.configureNLogProgramatically ()
There is a need to have three different compiler directives useable in the code. So I used
#if USE
#elif INTERACTIVE
#else
#endif
which worked with the Visual Studio F# Iteractive, but failed when using fsi.exe --use opition
with
error FS0010: Unexpected keyword 'elif' in directive. Expected identifier or other token.
So the old way has to be used,
#if USE
#else
#if INTERACTIVE
#else
#endif
#endif
08/14/13
Those of us that use Visual Studio with C# make common use of the outlining features. My version of VS 2010 Pro does not have outlining for F#. Up to now it didn't make that much of a difference, but lately with a script I am using to develop test cases, think test creation playground, having outlining can be a big benefit. If you don't know about Visual Studio extensions, you should. They are installed with in Visual Studio from the menu: Tools
-> Extension Manager
, then for dialog in left panel click Online Gallery
. In the upper right is a search bar.
So I found F# Outlining. Notice the tags: F#, Outlining, fsharp; these can be put in the search bar.
There are a few things to note about F# Outlining
- Instead of
#region "something"
you need to make it a comment//#region "something"
, likewise for#endregion
as//#endregion
. - The keyboard short cuts
a. Collapse current -CTRL M
,CTRL S
b. Collapse all -CTRL M
,CTRL A
c. Expand current -CTRL M
,CTRL E
d. Expand all -CTRL M
,CTRL X
I tested this with a script and the HOL Light command prompt. Both worked with no problems.
Another extension for F# that I find invaluable is Indent Guides
In working with test cases for (|Failure|_|)
there as some web pages worth noting.
Operators.Failure Active Pattern (F#)
Matches Exception objects whose runtime type is precisely Exception.
However, not all errors should be handled as exceptions in your code.
Usage errors. A usage error represents an error in program logic that can result in an exception. However, the error should be addressed not through exception handling but by modifying the faulty code.
Program errors. A program error is a run-time error that cannot necessarily be avoided by writing bug-free code.
System failures. A system failure is a run-time error that cannot be handled programmatically in a meaningful way.
Performance considerations Throwing or handling an exception consumes a significant amount of system resources and execution time. Throw exceptions only to handle truly extraordinary conditions, not to handle predictable events or flow control.
Core.exn Type Abbreviation (F#)
type exn = System.Exception i.e. type Microsoft.FSharp.Core.exn = System.Exception
This class is provided as a means to differentiate between exceptions defined by the system versus exceptions defined by applications.
These errors result from failed runtime check (such as an array out-of-bound error), and can occur during the execution of any method.
Partial active patterns Active patterns that do not always produce a value are called partial active patterns; they have a return value that is an option type. To define a partial active pattern, you use a wildcard character (_) at the end of the list of patterns inside the banana clips.
Examples of the use of (|Failure|_|)
in code:
try .. with Failure _ as e ->
(function Failure _ -> th1 | e -> Choice.error e)
Note: I am aware of three Failure functions accessible within NHol
- Microsoft.FSharp.Core.Operators.Failure
- FSharp.Compatibility.OCaml.Core.Failure
- NHol.lib.Failure
After many test cases I now know what
Matches Exception objects whose runtime type is precisely Exception.
means. If you use try .. with Failure _
you will only catch exactly System.Exception or its other name exn. You will not catch anything that inherits from System.Exception or that inherits from exn. It catches just the one exception type. So what is the usefulness of a function that catches just one type of exception? The usefulness comes from overriding the function to filter other types of exceptions so that you can handle them. i.e.
let (|Failure|_|)(exn : exn) =
match exn with
| :? System.Collections.Generic.KeyNotFoundException -> Some exn.Message
| :? System.ArgumentException -> Some exn.Message
| Microsoft.FSharp.Core.Operators.Failure s -> Some s
| _ -> None
here we additionally capture KeyNotFoundException and ArgumentException.
In NUnit when working with functions that return exceptions, not as an exception but as a type, I prefer to convert the exception to a string before comparing. This way I can print the string out when developing the test to see what EOL characters need to be inserted. e.g.
Tests.NHol.lib.lib.nestedFailure.01:
Expected string length 110 but was 157. Strings differ at index 110.
Expected: "...d' was thrown."
But was: "...d' was thrown.\r\n --- End of inner exception stack trace ---"
----------------------------^
In writing unit test we use a code coverage tool, and naturally for such a large project there are inline functions. It is almost expected that a code coverage or profiling tool will not correctly handle inline code because it has been optimized and does not have debug information to help the tool identify the source code. That is the case I ran into today. I saw a suggestion to use <@ @> in the test case so that it might identify the real source code, but it did not work. I also looked for ways to disable inline functions and found none. Since I do want to see the code coverage identify the code as covered I will go the old fashioned route of adding a preprocessor directive, i.e. #if and have two versions of the code; one with the inline word and one without. The only thing I do have to be concerned about with this is that the type signature of an inline function is not the same as one without.
The presence of inline affects type inference. This is because inline functions can have
statically resolved type parameters, whereas non-inline functions cannot.
We have started using pre/post conditions, think Debug.Assert, or Hoare logic. e.g.
/// <exception cref="System.ArgumentException">Thrown when the list is empty.</exception>
[<CompiledName("ReduceBack")>]
let reduceBack (reduction : 'T -> 'T -> Choice<'T, 'Error>) (list : 'T list) =
// Preconditions
checkNonNull "list" list
08/15/13
F#The F# 3.0 Language Specification (pdf)
Statically Resolved Type Parameters (F#) (^T)
When you use static type parameters, any functions that are parameterized by type parameters must be inline. This guarantees that that the compiler can resolve these type parameters.
08/18/13
... a couple of tests were failing; as it turns out, they are failing due to typing-related issues.
These issues arise from the design of FsUnit – the “should”, “equal”, and “be” functions/values aren’t type-safe, so you may find that you have tests which look like they should be passing, but aren’t, because you’re actually comparing two values with slightly different types (which NUnit just treats as non-equal).
My recommendation is to use the helper functions in ‘TestHelpers.fs’ – they’re roughly equivalent to those from FsUnit, except that they enforce type-safety so you won’t have any problems with tests compiling, then failing due to type-related issues. If you use the helper functions in the Collection module (e.g., Collection.assertEqual) you’ll get better error messages on failing tests too.
Jack
Domenico has started a very nice NHol manual written in LaTeX using fitch.sty for the proofs and proof.sty (A User Guide) for the rules. While it is not available to the public, it will be a valued addition for the project when completed.
Currently we have several preprocessor symbols:
use
- If you are familiar with OCaml you may know this one. HOL Light is run as a script and not a compiled program. So one runs it by invoking each script file in the correct order which is done in hol.ml which can be run from top-level. Now in F# we would like to do the same, but sadly F# does not support #use
within F# Interactive but does support it as a command line option. So to run the F# script in the same manner as OCaml we run NHol from a command prompt making use of the --use option. Now when a script runs using the --use option, one does not need to use the F# Interactive open command in each fs file. e.g. lib.fs and fusion.fs So to have the fs files open a file only once we have the USE
preprocessor directive.
the original version uses INTERACTIVE. If you load the code into F# Interactive, it fails since there are multiple files without module names. Using USE, loading the code into F# Interactive has module names just like compiling the code. I often use this when I would like to quickly override some functions for bug fixing.
Phan
INTERACTIVE
When you are compiling code in F# Interactive, whether you are running interactively or running a script, the symbol INTERACTIVE is defined.
F# Interactive (fsi.exe) Reference
This symbol is mostly used with printers.
#if INTERACTIVE
fsi.AddPrinter string_of_type
fsi.AddPrinter string_of_term
fsi.AddPrinter string_of_thm
#endif
COMPILED
When you are compiling code in the compiler, the symbol COMPILED is defined.
F# Interactive (fsi.exe) Reference
This one is not used by name, however either INTERACTIVE
or COMPILED
will be active so an #else
section for INTERACTIVE
is the same a using #if COMPILED
.
BUGGY
Instead of proving some theorems, when BUGGY is defined, we assume the results, taken from OCaml output. Back when we used exceptions, the project failed arbitrarily by many reasons e.g. too-deep recursion, stack overflow, raised exceptions, etc. We defined BUGGY in order to load as many modules as possible for examining. Right now, it's still useful since the code is failing at multiple places. Some use of bindOrRaise is put inside BUGGY since they are raised due to incorrect states.
Phan
DEBUG
and TRACE
These are the standard .NET symbols. See: How to trace and debug in Visual C#
FSI_VER_2
This is for use with Visual Studio 2010 which comes with F# Interactive 2.x as opposed to the newer version of F# Interactive that comes with Visual Studio 2012. More specifically it is used when referencing assemblies. e.g.
#if FSI_VER_2
#r "./../packages/FSharp.Compatibility.OCaml.0.1.10/lib/net40/FSharp.Compatibility.OCaml.dll"
#r "./../packages/FSharp.Compatibility.OCaml.Format.0.1.10/lib/net40/FSharp.Compatibility.OCaml.Format.dll"
#r "./../packages/FSharp.Compatibility.OCaml.System.0.1.10/lib/net40/FSharp.Compatibility.OCaml.System.dll"
#r "./../packages/ExtCore.0.8.32/lib/net40/ExtCore.dll"
#r @"./../packages/NLog.2.0.1.2/lib/net40/NLog.dll"
#else
#I "./../packages"
#r "FSharp.Compatibility.OCaml.0.1.10/lib/net40/FSharp.Compatibility.OCaml.dll"
#r "FSharp.Compatibility.OCaml.Format.0.1.10/lib/net40/FSharp.Compatibility.OCaml.Format.dll"
#r "FSharp.Compatibility.OCaml.System.0.1.10/lib/net40/FSharp.Compatibility.OCaml.System.dll"
#r "ExtCore.0.8.32/lib/net40/ExtCore.dll"
#r @"NLog.2.0.1.2/lib/net40/NLog.dll"
#endif
CODE_COVERAGE
This is one currently used exclusively by Eric for use with code coverage. Since most code coverage tools have problems with inline
code they report the code as not covered. To get a truer report we take out the inline
keyword and then generate the code coverage report. There are caveats with this approach.
Most of the work on converting the code to use workflows has been completed, mostly by Phan. This work was done in a branch called removing-exceptions
and has now been merged into master
. removing-exceptions
will be deleted in a few days. I am noting this here in case someone hits a rotted link to removing-exceptions
.
The preference for test with result of option type is
|> assertEqual None
|> assertEqual (Some 1234)
instead of
|> assertEqual None
|> Option.get
|> assertEqual 1234
08/22/13
The other day we received a open source license for JetBrains dotTrace. Again, thanks to the people at JetBrains! While dotCover is working quite well, as NHol is one large F# script and dotTrace works with compiled code, success is very limited. Note: this is not a fault of dotTrace, it is because the main part of this is a script. I don't currently know of any tool that can profile an F# script running in F# Interactive. The one place we are having success with dotTrace is when it is used to trace NUnit test. This works like a charm.
While I can get dotTrace to see F# Interactive, either within Visual Studio or from a standalone fsi.exe, it only profiles fsi, and not the F# script running within fsi. There might be a way to do this, but it is not high on my list.
Found out that dotCover has an ability to skip NUnit test based on NUnit categories. From VS menu dotCover -> options -> Unit Testing (The bold text) Under "Don't run test from categories (comma-separated list)".
The parser for HOL Light is set up to catch exception noparse. I was creating some test today and created some sample parsers that were used by the built-in parsers. I was throwing a different exception than noparse and the results were not correct. So the moral of the story is if you create a parser for HOL light and need to throw an exception, throw noparse.
08/23/13
We are going to start using the github issues tracking. This will be nice for others not in the communications loop to be able to see more of what is going on and I can just reference the issue instead of rewriting parts of it into here.
08/28/13
I have been spending time writing test cases for the lexer in preparation for testing the parser.
The lexer is basically a set of parser combinators of the signature
string list -> (string * string list)
then for rawtoken
the strings are converted to lexcode
string list -> (lexcode * string list)
When rawtoken
runs all tags are Ident
, then when simptoken
runs the Ident
tags are changed to Resword
tags if the string is a reserved word.
How collect
works.
(string * string list) -> string
It takes the result of a parser combinator of the signature
string list -> (string * string list)
and converts it to a string. Notice how it accepts a string * string list
instead of a string list
. This saves a translation step of converting string * string list
to string list
.
For the two separators ,
and ;
, ;
is a Resword
while ,
is a Ident
.
Two separators (,
or ;
) in a row are not tokenized into separate tokens but one token.
Along the line of old habits never die
if t = !comment_token then
is not read as if t equals not comment_token then
, but as if t equals the dereference of the ref comment_token
, in other words, if t starts with // then it is a comment
.
To access characters that are not on a keyboard one can escape the char code in OCaml and HOL Light with
/NNN
or /xNN
while for F# one must use /uNNNN
or /UNNNNNNNN
.
In Hol Light escaped characters can only be used within a quoted string.
The pretype parser can be changed out as needed
let pretype = parse_pretype
09/10/13
The F# 3.0 Language Specification (pdf)
09/11/13
Ran across Pex and Moles again; I knew about it but didn't remember it. Need to look into using it for generating test cases.
Pex automatically generates test suites with high code coverage. Right from the Visual Studio code editor, Pex finds interesting input-output values of your methods, which you can save as a small test suite with high code coverage. Microsoft Pex is a Visual Studio add-in for testing .NET Framework applications.
Moles allows to replace any .NET method with a delegate. The Fakes Framework in Visual Studio 2012 is the next generation of Moles & Stubs, and will eventually replace it. Moles supports unit testing by providing isolation by way of detours and stubs. The Moles framework is provided with Pex, or can be installed by itself as a Microsoft Visual Studio add-in.
09/19/13
When working with parser combinators while most of the info talks about making the combinators, the other side of the coin that needs to be learned is collecting the result and transforming back into a type for the next parser. i.e. the result of two or more parsers may be a string list
or some other structure. One has to convert the result back into the appropriate type. So for a string list one could just add
||> (fun sl -> implode sl)
or as another example use the collect method which converts string * string list
into string
.
11/12/13
You may have noticed that no updates have been pushed in the last few months, this is not because we have stopped, it is because two of us, Jack and Anh-Dung, are working at new jobs and don't have the time for this. Domenico is still working with HOL-Light but more from a user perspective than a coding perspective. I am still learning how HOL-Light internally works to the detail of being able to explain each line of code to someone else with confidence and striving to keep the F# code as close to the original OCaml code as possible. I am uncomfortable with using .NET exceptions here and computation expressions altered the code more than I was expecting so I am looking into other solutions that might work without using/limiting computation expressions. Also, the problem of saving state is something I have looked into and found something that needs more research. Also adding a REPL is something to be resolved.