-
Notifications
You must be signed in to change notification settings - Fork 4
Eric's Notes Page 1
This is page 1 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. For example I originally noted that there were two parsers used here when in fact I now know there are three.
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.
This project is based on the HOL Light (Wikipedia) interactive theorem prover / proof checker by John Harrison.
The HOL Light reference manual as HTML and pdf.
The HOL Light tutorial as pdf.
As a introduction to theorem proving and HOL Light in particular see Handbook of Practical Logic and Automated Reasoning (Worldcat) and the related source code in OCaml and our translation to F#. Also of help are various papers by John.
Here is the current repository for the HOL Light. The source code is in OCaml.
The starting code for this project is from Google code. The version used is r163.
The F# code will be written using the Lightwieight syntax as opposed to the Verbose syntax.
To assist in converting OCaml to F#, we bring in the FSharp.Compatibility.OCaml module by Jack Pappas. Then once all of the code is compiling and we have converted the OCaml code to F#, we can then remove the use of FSharp.Compatibility.OCaml.
HOL-Light is meant to be run from the OCaml REPL toplevel. When one first uses HOL-Light, ("You should now see a large amount of output as HOL Light is loaded, which in particular involves proving many theorems and giving them names.")[http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf] This presents a problem when one is done working as there is no way to save the environment within OCaml. John uses checkpointing [(Tutorial 1.4 Checkpointing)] (http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf). Currently we are using the F# Interactive --use option which is only available as a command line option and not from within F# Interactive as #use.
We have thought about integrating this within Visual Studio or another open source IDE, but it is so far down the road it is not actively discussed.
The tools we will be using for this are
- F#: VS 2012 (any version). If you want to use VS extensions such as the one for Fantomas, then you cannot use the express version. Don't know of any open-source IDEs work for this as I have not tired any of them.
- Unit testing: NUnit
- Specification checking: FsCheck
- Git: A Git client such as msysgit
- Package Manager: NuGet
- F# formatting: Fantomas
- Code Coverage: JetBrains dotCover. We were given an open source project license by JetBrains for this project. Thanks goes to the people at JetBrains for their support.
- Documentation: LaTeX using fitch.sty for the proofs and proof.sty (A User Guide) for the rules.http://www.mathstat.dal.ca/~selinger/fitch/).
We learned from our last project that when translating OCaml to F#, it is not uncommon to find corresponding library methods in F# to replace OCaml lib functions. See notes in lib.fs test. While some functions are equivalent, some may have different results, e.g. exception instead of empty list, or the order of the parameters may be different, etc. If you look at NHOL\lib.fs you will see the places we have noted that can be changed to built-in F# functions. e.g. OCaml tl with F# List.tail.
OCaml Built-in F#
map List.map
map2 List.map2
el List.nth
itlist List.fold
rev_itlist List.foldBack
end_itlist List.reduceBack
itlist2 List.fold2
rev_itlist2 List.foldBack2
replicate List.replicate
-- ..
forall List.forall
forall2 List.forall2
exists List.exists
length List.length
filter List.filter
partition List.partition
find List.find
index List.findIndex
chop_list List.take
flat List.concat
sort List.sortWith
mergesort List.sortWith
We also learned that OCaml exceptions "as a general-purpose non-local control structure" in OCaml are time-wise cheap when compared to .NET exceptions in F#, and that .NET exceptions as a means of back-tracking are hard to debug so we will be replacing them with the use of F# Options. We did not do this in the last project as our goal was to keep the F# code as close to the book code as possible. Here are goal is to make a version of HOL-Light that can be used interactively, so the use of exceptions as a general-purpose non-local control structure will not be allowed.
During the conversion phase in order to allow failwith to compile so as not to force the code to be converted to F# options, we modify the failure.
We will be using Fantomas by Anh-Dung Phan to assist in converting to the lightweight syntax and standardizing the formatting. At present Fantomas cannot handle the single and multiline comments, but can handle doc comments, so we change (* to /// when before running Fantomas, and then change /// back to (* as needed to preserve the comment.
As a guideline on the order in which to convert the files so that the project builds and we progress, we will be following the file order listed in hol.ml
(* ------------------------------------------------------------------------- *)
(* Various tweaks to OCaml and general library functions. *)
(* ------------------------------------------------------------------------- *)
loads "system.ml";; (* Set up proper parsing and load bignums *)
loads "lib.ml";; (* Various useful general library functions *)
(* ------------------------------------------------------------------------- *)
(* The logical core. *)
(* ------------------------------------------------------------------------- *)
loads "fusion.ml";;
(* ------------------------------------------------------------------------- *)
(* Some extra support stuff needed outside the core. *)
(* ------------------------------------------------------------------------- *)
loads "basics.ml";; (* Additional syntax operations and other utilities *)
loads "nets.ml";; (* Term nets for fast matchability-based lookup *)
(* ------------------------------------------------------------------------- *)
(* The interface. *)
(* ------------------------------------------------------------------------- *)
loads "printer.ml";; (* Crude prettyprinter *)
loads "preterm.ml";; (* Preterms and their interconversion with terms *)
loads "parser.ml";; (* Lexer and parser *)
(* ------------------------------------------------------------------------- *)
(* Higher level deductive system. *)
(* ------------------------------------------------------------------------- *)
loads "equal.ml";; (* Basic equality reasoning and conversionals *)
loads "bool.ml";; (* Boolean theory and basic derived rules *)
loads "drule.ml";; (* Additional derived rules *)
loads "tactics.ml";; (* Tactics, tacticals and goal stack *)
loads "itab.ml";; (* Toy prover for intuitionistic logic *)
loads "simp.ml";; (* Basic rewriting and simplification tools. *)
loads "theorems.ml";; (* Additional theorems (mainly for quantifiers) etc. *)
loads "ind_defs.ml";; (* Derived rules for inductive definitions *)
loads "class.ml";; (* Classical reasoning: Choice and Extensionality *)
loads "trivia.ml";; (* Some very basic theories, e.g. type ":1" *)
loads "canon.ml";; (* Tools for putting terms in canonical forms *)
loads "meson.ml";; (* First order automation: MESON (model elimination) *)
loads "quot.ml";; (* Derived rules for defining quotient types *)
(* ------------------------------------------------------------------------- *)
(* Mathematical theories and additional proof tools. *)
(* ------------------------------------------------------------------------- *)
loads "pair.ml";; (* Theory of pairs *)
loads "nums.ml";; (* Axiom of Infinity, definition of natural numbers *)
loads "recursion.ml";; (* Tools for primitive recursion on inductive types *)
loads "arith.ml";; (* Natural number arithmetic *)
loads "wf.ml";; (* Theory of wellfounded relations *)
loads "calc_num.ml";; (* Calculation with natural numbers *)
loads "normalizer.ml";; (* Polynomial normalizer for rings and semirings *)
loads "grobner.ml";; (* Groebner basis procedure for most semirings. *)
loads "ind_types.ml";; (* Tools for defining inductive types *)
loads "lists.ml";; (* Theory of lists *)
loads "realax.ml";; (* Definition of real numbers *)
loads "calc_int.ml";; (* Calculation with integer-valued reals *)
loads "realarith.ml";; (* Universal linear real decision procedure *)
loads "real.ml";; (* Derived properties of reals *)
loads "calc_rat.ml";; (* Calculation with rational-valued reals *)
loads "int.ml";; (* Definition of integers *)
loads "sets.ml";; (* Basic set theory. *)
loads "iterate.ml";; (* Iterated operations *)
loads "cart.ml";; (* Finite Cartesian products *)
loads "define.ml";; (* Support for general recursive definitions *)
(* ------------------------------------------------------------------------- *)
(* The help system. *)
(* ------------------------------------------------------------------------- *)
loads "help.ml";; (* Online help using the entries in Help directory *)
loads "database.ml";; (* List of name-theorem pairs for search system *)
ML files missing from the list and that are currently not in our project:
hol.ml, term.ml, thm.ml, type.ml update_database.ml, and pa_xyz.ml files.
To make the process of conversion easier, we will be starting off with the core code and working outward based on dependencies so that the code will compile as we work. If you notice, the starting module is system.ml, but since this has more to do with system related functionality, we just comment it out and move onto lib.ml as the first piece of code in the core.
The F# community creates lots of good free code for use with other projects and is made easily available via NuGet.
We will make extensive use of Unit testing here as we did with our earlier project, and use both NUnit and FSUnit which we bring into the projects via NuGet.
Further down the road we will be making use of the F# core extensions by Jack in ExtCore.
To work with the project on a local machine some of us prefer to use msysgit.
The project can be used with Visual Studio Express for Web with F# Tools for Visual Studio Express 2012 for Web. While you do not have to install NuGet with these tools (because it is installed when these tools are installed), in VS options you do have to enable "Allow NuGet to download missing packages during build."
When you build the solution for the first time, several NuGet packages will be downloaded and installed. The Build log will show:
For NHol project:
Installing 'FSharp.Compatibility.OCaml 0.1.9'.
Successfully installed 'FSharp.Compatibility.OCaml 0.1.9'.
Install 'ExtCore 0.8.23'.
Successfully installed 'ExtCore 0.8.23'.
Install 'FSharp.Compatibility.OCaml.Format 0.1.9'.
Successfully installed 'FSharp.Compatibility.OCaml.Format 0.1.9'.
Install 'FSPowerPack.Community 2.1.3.1'.
Successfully installed 'FSPowerPack.Community 2.1.3.1'.
Install 'FSharp.Compatibility.OCaml.System 0.1.9'.
Successfully installed 'FSharp.Compatibility.OCaml.System 0.1.9'.
For NHol.Tests project:
Installing 'FsUnit 1.2.1.0'
Successfully installed 'FsUnit 1.2.1.0'
Installing 'FsCheck 0.8.3.0'.
Successfully installed 'FsCheck 0.8.3.0'.
Installing 'NUnit 2.6.2'.
Successfully installed 'NUnit 2.6.2'.
All packages listed in packages.config are already installed.
Currently the build will succeed, however if the references are invalid, update the references to the DLLs which are located in the packages directory. If there are multiple directories of DLLs , choose Net40.
When converting OCaml to F# it is helpful to be able to search the original code unaltered and files. The only way to get the original code is via SVN, so one will need to install an SVN client. I used Slik SVN.
When converting OCaml to F# one should have the correct OCaml documentation and F# documentation. What I use most of the time to search them is to Google for: OCaml module <name of module>, or F# module <name of module>.
In order to run HOL-Light I built a hardware virtual machine with Debian Linux on top of VMware workstation.
For some conversion problems, knowing the type signatures of the functions helps to find the problem. To this end a capture of the run of two versions of hol-light are included in the repository.
-
_doc\Recorded Output\hol-light output.txtfrom the snapshot taken on 10 January 2010 which is in the gzip file from the home page. -
_doc\Recorded Output\hol-light output (r163).txtfrom the r163 version taken on 28 May 2013 which is from the Google code site.
When multiple people work on a Git (Wikipedia) project, there will be files that need not and should not be updated to the master Git repository because they would cause problems when updated to someone else's system. To keep certain files from being updated to the master repository for the project there is the .gitignore file.
To help in customizing how Git interacts with the repository there is the .gitattributes file. Some of the things we do here are
- text=auto - Handles line endings. Store as LF, but load specific to system.
- *.cs diff=csharp - diff cs files as csharp.
- *.doc diff=astextplain - diff doc files as text plain.
Git is a free and open source distributed version control system designed to handle everything from small to very large projects with speed and efficiency. From: http://git-scm.com/
GitHub is a web-based hosting service for software development projects that use the Git revision control system. From: https://en.wikipedia.org/wiki/GitHub
It is customary to create a readme.md file when first creating a new Git repo on Github.
As this is based on open source software using the Apache 2.0 license, we include the license in the LICENSE.txt file in the root directory, and reference in the files as required.
When working with the various versions of the code, if one clicks on the commits link one will see all of the revisions to the files.
The code will be created using Microsoft Visual Studio 2012 and the F# programming language. Visual Studio (VS) will create the highest level file known as a solution, e.g. NHol.sln. Under the solution are currently two projects, one for the code, e.g. NHol.fsproj and one for the test, e.g. NHol.Tests.fsproj
VS also uses the AssemblyInfo files.
To keep certain info for the projects consistent we use [CommonAssemblyInfo] (https://github.com/jack-pappas/NHol/blob/master/Common/CommonAssemblyInfo.fs) - Added info
The NuGet packages also need some configuration and support files:
NuGet.Config (NuGet doc)
NuGet.targets (NuGet docs)
packages.config (NuGet docs)
repositories.config
NuGet.exe (NuGet docs)
Jack added app.config for use with FSharp.Core. As this is custom code I will have to revisit the details of this latter.
Behind the scenes, VS uses MSBuild for the build process.
To ensure the code is correct, we will try and not have any warnings when done. A common warning when converting HOL code from OCaml to F# is that not all of the patterns in a match will be handled. To avoid these warnings the unhandled patterns will trigger an exception, thus not allowing the code to succeed. As we better understand the code, we should be able to either convert the expectations to valid code or note examples where they are needed.
HOL uses a parser combinator and F# has a very popular parser combinatory called FParsec. While the concepts of parser combinators are the same, the operators used can be very different and make it hard to convert from one parser combinator to another. At present we are converting some HOL operator syntax to those of FParsec syntax, but to don't take this to mean that all HOL parser combinators operators can be converted to FParsec operators. See HOL Light online manual for additional info.
Here is a list of the operator conversions.
HOL FParsec Synopsis
|| <|> Produce alternative composition of two parsers.
++ .>>. Sequentially compose two parsers.
>> |>> Apply function to parser result.
a Parser that requires a specific item.
atleast Parses at least a given number of successive items using given parser.
elistof Parses a possibly empty separated list of items.
finished Parser that checks emptiness of the input.
fix Applies parser and fails if it raises Noparse.
leftbin Parses iterated left-associated binary operator.
listof Parses a separated list of items.
many Parses zero or more successive items using given parser.
nothing Trivial parser that parses nothing.
possibly Attempts to parse, returning empty list of items in case of failure.
rightbin Parses iterated right-associated binary operator.
some Parses any single item satisfying a predicate.
HOL Notation Signature
Parser Paser Param Param token result
++ Infix ('a -> 'b * 'c) -> ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
elistof Prefix ('a -> 'b * 'a) -> ('a -> 'c * 'a) -> string -> 'a -> 'b list * 'a
listof Prefix ('a -> 'b * 'c) -> ('c -> 'd * 'a) -> string -> 'a -> 'b list * 'c
leftbin Prefix ('a -> 'b * 'c) -> ('c -> 'd * 'a) -> ('d -> 'b -> 'b -> 'b) -> string -> 'a -> 'b * 'c
rightbin Prefix ('a -> 'b * 'c) -> ('c -> 'd * 'a) -> ('d -> 'b -> 'b -> 'b) -> string -> 'a -> 'b * 'c
Notation Param Parser Parser Parm token result
|| Infix ('a -> 'b) -> ('a -> 'b) -> 'a -> 'b
>> Infix ('a -> 'b * 'c) -> ('b -> 'd) -> 'a -> 'd * 'c
atleast Prefix int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
many Prefix ('a -> 'b * 'a) -> 'a -> 'b list * 'a
possibly Prefix ('a -> 'b * 'a) -> 'a -> 'b list * 'a
nothing 'a -> 'b list * 'a
fix Prefix string -> ('a -> 'b) -> 'a -> 'b
Notation Parm Parm result
a Prefix 'a -> 'a list -> 'a * 'a list
some Prefix ('a -> bool) -> 'a list -> 'a * 'a list
finished 'a list -> int * 'a list
OCaml has the Camlp4 preprocessor while F# has no exact equivalent. So we must massage the F# code.
For example in the OCaml code we need to do the following conversions
OCaml F#
`xyz` parse_term "xyz"
`:xyz` parse_type "xyz"
`;xyz` parse_qproof "xyz"
In converting the function BETAS_CONVS in drule to F# one encounters the line
| Comb(Comb(,),_) -> (RATOR_CONV BETAS_CONV THENC BETA_CONV) tm
for which RATOR_CONV BETAS_CONV THENC BETA_CONV will produce the error "This value is not a function and cannot be applied."
Looking at the type signatures of the functions we find
RATOR_CONV : conv -> conv
BETAS_CONV : term -> thm
THENC : conv -> conv -> conv
BETA_CONV : term -> thm
for which if we realize that THENC is an infix operator as opposed to a prefix operator, will compile as
(RATOR_CONV (THENC BETAS_CONV BETA_CONV)) tm
So clearly somewhere in the original OCMAL code, not our F# code, THENC is being defined as an infix operator. Remember that the OCaml code is run through the preprocessor before actually being compiled and if one checks the README file from the original code one will see that the preprocessor relies on the pa_j.cmo file which comes a pa_j_<ver>.ml file depending upon the OCaml version. Looking and any of the pa_j_<ver>.ml files we find
"THENC" -> "thenc_"
and
f = expr; "THENC"; g = expr -> <:expr< ((thenc_ $f$) $g$) >>
so THENC is clearly processed as infix for the OCaml code.
For infix operators defined in code see expr: AFTER "<" in pa_j_3.09.ml
Other OCaml infix operators defined for HOL Light. Note: The are in OCaml not in HOL Light terms and types.
HOL Converted syntax
o <<
upto
F_F ||>>
THENC
THEN
THENL
ORELSE
ORELSEC
THEN_TCL
ORELSE_TCL
Since the infix operators are typically used to make code easier to read, changing code from infix to prefix can make the code harder to read. One way around this since F# does not support infix functions is to use this trick;
|> infix_op <| John uses a nonstandard means of loading dependent modules with the needs function. The needs function is defined in hol.ml. In F# we just use multiple open statements to open all proceeding modules.
Often in converting OCaml to F# most of the code easily converts, but then you get to the last few errors and it seems that there is no way to get rid of the remaining errors. These errors are typically related to the type inferencing not being able to resolve the typing. To fix these, first break the function down into the most basic parts (values, functions, operators) and then list the type signatures for them. Next rebuild the function up one piece at a time adding the type signature as you go. Eventually through syntax changes you get the type inference system to accept the new code.
As an example in theorems for a function causing the last set of errors:
Original OCaml function
((a(Ident "#") ++ disj >> snd) ++ pa_intro >> uncurry (THEN)) toks
part signature
a : 'a -> 'a list -> 'a * 'a list = <fun>
(Ident "#") : lexcode
.>>. : ('a -> 'b * 'c) -> ('c -> 'd * 'e) -> 'a -> (b' * 'd) * 'e = <fun> OCaml: ++
disj : lexcode list -> tactic * lexcode list
snd : 'a * 'b -> 'b
pa_intro : lexcode list -> tactic * lexcode list
|>> : ('a -> 'b * 'c) -> ('b -> 'd) -> 'a -> 'd * 'c = <fun> OCaml: >>
uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c = <fun>
THEN : conv -> conv -> conv = <fun>
toks : lexcode list
Rebuilding function piece by piece with signatures
let (v1 : lexcode) = Ident "#"
let (v2 : lexcode list -> lexcode * lexcode list) = a v1
let (v3 : lexcode list -> (lexcode * tactic) * lexcode list) = v2 .>>. disj
let (v4 : lexcode list -> tactic * lexcode list) = v3 |>> snd
let (v5 : lexcode list -> (tactic * tactic) * lexcode list) = v4 .>>. pa_intro
let (f1 : (tactic * tactic) -> tactic) = uncurry THEN
let (v6 : lexcode list -> tactic * lexcode list) = v5 |>> f1
let v7 = v6 toks
v7
Note: When rebuilding this I knew the code was to function as a parser combinator so the signatures
of (lexcode list -> obj * lexcode list) was expected. Also the |>> operator required a function as
the parameter which was key into getting the last of it sorted out.
New F# function
((a(Ident "#") .>>. disj |>> snd) .>>. pa_intro |>> (uncurry THEN)) toks
When one first starts converting OCaml code to F#, one will fix the errors one at a time and in the order of the errors from top to bottom as this allows you to focus on just one error at a time. As one gets better, you begin to handle entire classes of errors at once using find and replace. However every now and then you encounter a file that has a large number of inner functions and the find and replace methods that changes white space will throw off the alignment of functions. So when near the end of the error list you have a few errors about incomplete structures. At this point one must revert back to the process of handling the errors in order from top to bottom one at a time and manually fix each error.
Handling this error can be tricky.
Block following this 'let' is unfinished. Expect an expression.
If you comment out the entire let and the error moves to the previous let, then what I like to do is
- comment out all of the code following the let giving the error
- Add the empty function, i.e. (), after the let with the error.
- This should show a whole set of new errors. Just fix the errors, remove the () and uncomment the rest of the code.
For sequential try with statements one can format them without indenting:
try
with
| Failure ->
try
with
| Failure ->
instead of
try
with
| Failure ->
try
with
| Failure ->
Another way to help in eliminating errors it to first work in the regular syntax as opposed to the light syntax by using the following directive
#light "off"
When converting ind_types I was unable to resolve all of the errors in light syntax, however was able to resolve all of the errors in regular syntax. I let Fantomas convert the code from regular syntax to light syntax.
There are now four of us working on this project
Jack, Phan, Eric and Domenico.
Domenico started a separate port of HOL Light from OCaml to F# on Github. He is also worked on a port of HOL Zero to F#.
As we are past the initial start and plan to allow for pull-request we are adding a contributing guideline. Note this is an rst file (reStructuredText)and not a md (Markdown) file.
Since I have VS 2010 and not VS 2012 I have to run Fantomas from the command line. As this is a very repetitive process for me here is what I did to make it easier.
Do this once
-
Download and build Fantomas from Github.
-
In a new directory, e.g. D:\Fantomas, copy the files needed to run Fantomas:
a. Args.dll
b. Fantomas.exe
c. FantomasLib.dll
d. FSharp.Compiler.dll -
Create a batch file in the new directory to run Fantomas (Fantomas.bat)
Set Path="D:\Fantomas"
Famtomas.exe <filename>(pre).fs --out <filename>.fs -
Make a new command prompt
a. Name: Fantomas
b. Target: %windir%\system32\cmd.exe /k Fantomas.bat
c. Start in: empty
Do this for each new file.
- Copy the file to be formatted to
- Rename file to be formatted to pre.fs
- Change name of in Fantomas.bat in both places.
- Double click the command prompt named Fantomas.
- Open <filename>.fs and verify formatted correctly.
- If it formatted correctly I just overwrite the old file with the new file.
I could probably make it even easier by setting it up to work from right clicking the file, but this works for now.
The F# 3.0 Language Specification
F# Software Foundation is a great place to start when looking for info for F# where you don't know what or where to look.
The HOL Light code uses many variable names where it can use the wild card pattern _. F# flags these with compiler warning FS1182.
I don't mind the variable names as they help to debug the code, so I decided to suppress seeing the warnings. Normally one would modify the project file's suppress warning field but looking at the options I noticed in the other flags field : --warnon:1182 which I deleted and achieved the same result.
When using Git and working with others, one important thing I learned from Jack is that many small updates are better than a few large changes.
Here's an interesting bug because it creates 3 errors, seems like a semantic problem and is really a simple syntactic fix.
let cfs =
solve_idealism evs ps (map lhs (conjuncts bod)) in
(MAP_EVERY EXISTS_TAC(map (fun v -> rev_assocd v cfs zero_tm) evs)
|>THEN<| REPEAT(POP_ASSUM MP_TAC) |>THEN<| CONV_TAC INT_RING) gl
gives
Successive arguments should be separated by spaces or tupled,
and arguments involving function or method applications should be parenthesized
Type mismatch. Expecting a
'a * term -> tactic
but given a
'a * term -> (term list * instantiation) * ('a * term) list * (instantiation -> thm list -> thm)
The type 'tactic' does not match the type '(term list * instantiation) * ('a * term) list * (instantiation -> thm list -> thm)'
Type mismatch. Expecting a
(('a * term) list -> tactic) -> 'b -> 'c
but given a
tactic -> tactic -> tactic
The type '('a * term) list' does not match the type 'goal'
is fixed by one space after EXISTS_TAC
let cfs =
solve_idealism evs ps (map lhs (conjuncts bod)) in
(MAP_EVERY EXISTS_TAC (map (fun v -> rev_assocd v cfs zero_tm) evs)
|>THEN<| REPEAT(POP_ASSUM MP_TAC) |>THEN<| CONV_TAC INT_RING) gl
When converting OCaml to F# Verbose syntax, one must convert let .. and .. to let .. in let ...
OCaml can handle <function>[] but F# needs <function> []
When converting OCaml ^ to F# + one cannot do a global find and replace because HOL Light uses ^ as a term operator which are found within the term strings. This changes must me done by hand.
As F# originally derived from OCaml, to assist in the transformation F# has a Pervasives module similar to the OCaml Pervasives module.
As time progressed many of these operators were recreated in the core of F#
So, one should strive to us the F# core equivalent of the OCaml version when possible.
OCaml
Pervasives string_of_int
Pervasives ^
F# Pervasives
FSharp.Compatibility.OCaml.PervasivesModule string_of_int
FSharp.Compatibility.OCaml.PervasivesModule ^
F# Core
Microsoft.FSharp.Core.Operators string
Microsoft.FSharp.Core.Operators +
After two days trying to get NHol execute in F# Interactive, I can share my impressions.
We're dealing with a very complex system. Side effects are introduced everywhere, so the code is very sensitive to reordering and changes. You have to reload all modules or even restart F# Interactive to reproduce the same behaviour.
Even worse, try/with is used as control flow, and it makes recursive functions non-tail-recursive. I've got StackOverflowException in many modules, although I only to tried to load them in F# Interactive.
I can only get the modules to load in F# Interactive until quot.fs. The subsequent modules use tactical combinators which are hard to comprehend. I think we can start adding test cases here and fix these modules as we go.
We need to change a few parts of the core to minimize side effects and reduce the use of try/with as control flows. The current code is very difficult to test since they are tight-coupling and dependent on current state of the whole system.
Phan
When creating new fsx files in the VS Tutorial directory using VS, remember that the fsx file will be created in the NHol directory by default and not the NHol/Tutorial directory.
If code is copied in from an alternative source, e.g. PDF, one should check to make sure the displayed characters are ASCII characters.
Currently we have four high level directories in the NHol solution as seen in VS Solution Explorer.
- NHol - This is the OCaml code converted to F#.
- NHol.Tests - These are NUnit test. If you have the NUnit application installed, in addition to the packages being loaded by NuGet, just double click on NHol/NHol.Tests/bin/Debug/NHol.Tests.dll and click Run.
- Tutorial - These are scripts to be run from F# Interactive. To use: open a file, Ctrl-A, Alt+Enter. The main one for end user use is examples.fsx.
- .nuget - Maintained by NuGet. Should not be modified or used after initial setup.
Instead of
open NHol.lib
open NHol.fusion
open NHol.fusion.Hol_kernel
open NHol.basics
open NHol.nets
we use
open NHol
open lib
open fusion
open fusion.Hol_kernel
open basics
open nets
How do deal with
warning FS0025: "Incomplete pattern matches on this expression. For example, the value '[]' may indicate a case not covered by the pattern(s)."
If the code uses a match expression like
let intList = [1;2]
match intList with
| val1 :: val2 :: rest -> val1 + val2
then modify the code to cover the missing case(s)
let intList = [1;2]
match intList with
| val1 :: val2 :: rest -> val1 + val2
| [] -> 0
If the code binds the result to a pattern with a let like
let intList = [1;2]
let val1 :: val2 :: rest = intList
let sum val1 + val2
then change to
let intList = [1;2]
let sum intList =
match intList with
| val1 :: val2 :: rest -> val1 + val2
| [] -> 0
or even
let intList = [1;2]
let sum =
function
| val1 :: val2 :: rest -> val1 + val2
| [] -> 0
For even more examples of fixing warning FS0025: "Incomplete pattern matches on this expression. For example, the value '[]' may indicate a case not covered by the pattern(s)." see [push] (https://github.com/jack-pappas/NHol/commit/7d5e72d56c422ad0fefc36cd8467706188c4255e)
In the HOL Light tutorial the URL http://www.checkpointing.org is no longer valid. http://checkpoiting.org should be used.
We have reached the milestone of getting the core modules to compile and now are working to get the core modules to work the same and HOL Light.
There are currently only two FS0040 and one FS0025 warnings.
The current task of getting the core to function the same as HOL Light is being slowed down by the use of mutables.
For those who want to see the original OCaml code from r163 but don't want to pull a copy down using svn, one can access the code by browsing the source. http://code.google.com/p/hol-light/source/browse/?r=163#svn%2Ftrunk
With the problem of having to wait a few minutes for the FSI environment to be established the creation of application checkpointing has moved up in the list.
I posted a question on the FSharp Open Source Group.
One suggestion is to use dynamic assemblies, and other is to search previous apps no longer supported: WinNTckpt, Winckp, ChaRM-NT
One problem we keep encountering with open source F# projects is that VS projects are not backward compatible, thus requiring us to select a version as a standard. With VS 2013 that should no longer be a problem between VS 2013 and VS 2012. See: Round-tripping with Visual Studio 2012
It seems Jack and I had the same idea since yesterday, and I am sure the others on our group were thinking the same. When we did the Handbook project the code had no mutables and John had marked the interactive sections with begin and end markers which made it very easy to separate the OCaml scripts into F# fs files and F# scripts. The HOL Light code is designed to be entirely run from an interactive environment (OCaml toplevel) and uses checkpointing to save state. Now understanding this more I almost wish we had converted the code to FSI scripts first, then pulled out the code that could be put into fs files.
I was just writing an email to send you guys the same thoughts. I had a quick look this morning at 'hol.ml' (https://code.google.com/p/hol-light/source/browse/trunk/hol.ml) and realized that the code in each of the source files is being loaded directly into the OCaml toplevel (and not compiled into modules then loaded, which is subtly different).
I just went through the project and wrapped the top-level module declarations in each of the files and any 'open' declarations, in a conditional compiler directive so they're only used when the project is actually compiled (i.e., not when running in F# Interactive).
Jack
See branch
Having worked with Prolog and knowing that the same inferencing mechanism of Prolog are built into this code I think about how this would work if one looks at this as Prolog implemented with functional code. It becomes obvious that one would use Prolog assert (think store function) to commit clauses, in this cases theorems, into the database. Then one only needs to save and restore the database to achieve the same result as the checkpointing. As for the other mutables in the code when I did a quick scan the others seemed to be used as global flags, variables internal to a method and a few other persistent data stores such as the one causing us problems with num in the type store.
If we look at the code as layers of a cake with the code in the fs files at the top layer, then supported by .NET with assemblies and then supported by the system with blocks of memory and threads I see three ways to save the state. For the system we would stop the threads and save the memory as is done with virtual machines. For the .NET layer we could use dynamic assemblies, and for the code we could implement the Prolog assert and retract mechanisms into the code.
When working with the scripts yesterday I played around with ways to use #I #r and open statements and looked at initialization.fsx, init_all.fsx and lib.fsx and noticed that this works better for me with NHol.
// initialization.fsx
#I @"./../NHol"
#r @"bin/Debug/FSharp.Compatibility.OCaml.dll"
#r @"bin/Debug/FSharp.Compatibility.OCaml.Format.dll"
#r @"bin/Debug/FSharp.Compatibility.OCaml.System.dll"
#r @"bin/Debug/NHol.dll"and
// <xyz>.fsx
#load "initialization.fsx"
// Disable ML compatibility warnings
#nowarn "62";;
open FSharp.Compatibility.OCaml
open FSharp.Compatibility.OCaml.Num
open NHol.lib
open NHol.fusion
open NHol.basics
open NHol.nets
open NHol.printer
open NHol.preterm
open NHol.parser
open NHol.equal
open NHol.bool
open NHol.drule
open NHol.tactics
open NHol.itab
open NHol.simp
open NHol.theorems
open NHol.ind_defs
open NHol.``class``
open NHol.trivia
open NHol.canon
open NHol.meson
open NHol.quot
open NHol.pair
open NHol.nums
open NHol.recursion
open NHol.arith
open NHol.wf
open NHol.calc_num
open NHol.normalizer
open NHol.grobner
open NHol.ind_types
open NHol.lists
open NHol.realax
open NHol.calc_int
open NHol.realarith
open NHol.real
open NHol.calc_rat
open NHol.int
open NHol.sets
open NHol.iterate
open NHol.cart
open NHol.defineIn initialization.fsx all of the dlls for the project are opened from the bin Debug directory instead of using the packages directory. The #r uses part of the directory in the statement which clears up the Visual Studio Intellisense showing the warning "The value or constructor is not defined". Also a reference to NHol.dll is added.
In <xyz>.fsx we put all of the open statements as they seem to have no effect when put in initialization.fsx.
I have yet to find any official documentation on exactly why it works this way; when I do I will try to update this.
Eventually this will become a working version of HOL Light so I joined the HOL user group at HOL info. Reading the post lead me to target_rewrite.ml. When I saw
needs "imp_rewrite.ml";;I realized why HOL is using needs and not open statements. All of this is about theorems and theorems are built upon other theorems. Theorems rely on other theorems and by default with theorems when you reference one you have to bring in all of the needed theorems to use it; so instead of opening all of the theorems one needs all the way down the list you just use the HOL Light needs function which will recursively pull in the subordinate needed theorems. As such we need to modify our F# version to use needs.
In our code one will see the F# compiler directives
#if INTERACTIVE ... #endifthis is defined in F# Interactive (fsi.exe) Reference
If one tries to send modules from fs files to FSI one can encounter problems. Thus the need for #if INTERACTVIE
We are experimenting with the FSI Interactive Option use which as Jack says should have also been a F# Interactive directive #use, but wasn't implemented.
So instead there is hol.bat
In a windows bat file one can continue a line with the cmd quote character (^).
In order for me to run hol.bat I edited hol.bat and added
set path="C:\Program Files (x86)\Microsoft SDKs\F#\3.0\Framework\v4.0"
I then created a command prompt in the same directory as hol.bat named fsi with the following properties.
target: %windir%\system32\cmd.exe /k hol.bat
start in: <empty>
so that I could just double click on fsi to start it. I just close the fsi window when it doesn't work.
Domenico found some mistakes I made during the conversion of OCaml to F#. When I converted the HOL Light infix operator THEN to an F# operator working as infix using |> THEN <| with a global find and replace, it sometimes converted the then in a term to |> THEN <| which is incorrect. The reason this occurred in only certain files is that when I set up the find and replace, the case sensitive option was not selected and so then in addition to THEN was selected.
Also there is a (parse_term @" at the end of one of the strings. This came about because I was individually doing a find and replace on starting ` to (parse_term @" and then a global find and replace of ` to ") for the ending `. With 4262 terms in the code I am not surprised I missed a few; the mistakes are do to me alone.
Before I forget I am writing down the steps I used to convert most of the OCaml to F#. This will need to be modified as we progress since we are now adding #if INTERACTIVE.
-
Add at top of file
#light "off"- This is done because OCaml is closer to verbose syntax than light syntax. Light can also accept Verbose, but Verbose cannot accept Light, so sticking to Verbose keeps one from making additional changes that can cause the syntax not to compile. -
Add needed open statements. e.g. open FSharp.Compatibility.OCaml
-
For terms, types and qproofs which are enclosed with ` look at the first character after the `.
If it is:then convert the starting ` to(parse_type ".
If it is;then convert the starting ` to(parse_qproof ".
Otherwise convert starting ` to(parse_term ". The starting ` conversion can be done with a find and replace, but you cannot do a global find and replace, instead you must use find next and then decide for each occurrence. For the ending ` conversion it was possible to do a global find and replace converting ` to"). The(and)are added in case the result is an argument. Not all of the parenthesizes are needed, but if you don't add them where need the code will not compile correctly. This is based on system.quotexpander function. -
For the infix operators such as THEN and ORELSE they need to be enclosed with
|> <|to have them function as infix since the OCaml preprocessor converts the code from infix to prefix before compiling. These changes can be done with a global find and replace as long as one starts with the longer strings first, i.e. do THENC and THENL before THEN and ELSEC before ELSE, and one uses the find and replace options,case sensitiveandwhole word only. -
Convert parser combinator operators. e.g. ||, ++, >>. Do these before standard operators because converting
oto>>will cause problem when converting>>to|>>. -
Convert OCaml operators syntax to F# operator syntax. Some examples
OCaml F# comment
o >>
F_F ||>>
// / Num division -
Fix code depending on Pervasives module. e.g.
string_of_inttostringor^to+. -
Fix deprecated code warnings such as using
&&&instead of&&. -
Fix remaining warnings.
-
Use Fantomas to convert Verbose syntax to Light syntax and fix warnings and errors introduced by Fantomas, or remove
#light "off"and removeinand;;and fix warnings and errors introduced.
When you use sprintf, and F# Interactive, be aware of the two sprintf versions.
- Printf.sprintf in Core.Printf module
- ExtraTopLevelOperators.sprintf in Core.ExtraTopLevelOperators module witch has the AutoOpen attribute.
In an fs file was sprintf alone which caused an error when sent to F# Interactive.
error FS0001: The type 'string' is not compatible with the type 'format6<'a,'b,'c,'d,'e,'f>'
Changing this to Printf.sprintf will fix the problem.
For those of us who have the most minimum of Git skills, I am in this group, we have started Notes on using Git.
To make it easier for us to see each others work and to keep our separate changes from stepping on the master Git repository we will be using branches more often.
To help with debugging when running FSI as a standalone, we have removed the optimize option.
We have started to XML commentsto that we can make use of mouse-over summary.
07/15/2013
Currently to find and fix bugs we run hol.bat and wait to see the error. i.e.
System.Exception: EQT_ELIM
...
at FSI_0014.EQT_ELIM(thm th) in <parent directory>\NHol\bool.fs:line 117Stopped due to error
Domenico invented a way to by pass problem theorems to find other bugs.
Since
type thm =
| Sequent of (term list * term)
If we get an error for a theorem
let LAMBDA_PAIR_THM =
prove
((parse_term @"!t. (\p. t p) = (\(x,y). t(x,y))"),
REWRITE_TAC [FORALL_PAIR_THM; FUN_EQ_THM])
then it is replaced with
let LAMBDA_PAIR_THM = Sequent([],parse_term @"!t. (\p. t p) = (\(x,y). t(x,y))")
I still don't fully understand how the swap works, but hope to get time latter to fully understand this.
For some theorems we are getting StackOverflow errors so we are skipping them to move on.
We find that prepending @ to strings with parse_term and parse_type is better. See push.
We have been adding more pages to or wiki. Of note is one to help using Git.
When working with OCaml some of us build an OCaml system on top of Linux and install an OCaml editor. Here are some notes.
Instead of skipping entire modules by commenting out lines in hol.bat we are now using #if in code to skip problematic theorems and sections of code. See push.
In converting the OCaml to F#, OCaml can shadow names but is certain cases F# cannot. To solve this one must give each name a unique name. During the syntactic conversion I did this and introduced a bug. Phan found and fixed this. This also cleared an F# error FS0040.
HOL Light creates terms and types using parse_term and parse_type which take strings for input. Since this is like a language within a language and the term and types are not checked by the editors, i.e. VS, the default way to find problems with them is to run HOL Light and see if you get a runtime error. As there are over 4500 strings to convert from <string> to ( @<string>) and I did not want to do a global find and replace, they were converted as each module was converted with some manual input which introduced some errors. As these problems were becoming the main cause for errors I created a utility to check all of the strings for the common errors.
We have started creating test for use with NUnit. Many of these in lib.fs are based on examples in the HOL Light reference manual. (pdf)
When using F# Interactive, to print a type in a pretty print manner as opposed to as an AST once can use the FSI directive AddPrinter.
fsi.AddPrinter string_of_type;;
fsi.AddPrinter string_of_term;;
fsi.AddPrinter string_of_thm;;
Note: OCaml has #install_printer and #remove_printer while F# has noting to correspond with #remove_printer.
To do the same as remove_printer if I remember correctly one can do an fsi.AddPrinter with a method of the same signature that just returns the value, and thus cause it to be printed as an AST.
To make it easier to find bugs there is exploration.fsx. This allows one to run HOL Light from with in the VS F# Interactive window. With this one can modify functions in F# Interactive to test and reload individual modules without having to run all of the proceeding modules if one used hol.bat.
We ran into a need for gcd_big_int from BigInt which would be in compatibility. Since it is not implemented there Domenico did this work around.
If one wants to highlight a line of code in a github URL once can append #L<line number> e.g. https://github.com/jack-pappas/NHol/blob/master/NHol/lib.fs#L37
Found this which help to understand the fsi.exe use option.
One of the best thing I find to help in learning F# is to study it's predecessors, i.e. ML, CAML, OCaml and siblings such as Lisp, Scheme, and Haskell. In looking for the OCaml toploop code I ran into this. It show how #use, which is missing from F# Interactive, works in other top loop, e.g. REPL. Now that I see this and know how many times I edit some code in an fs file then send it to F# Interactive, I wish F# Interactive had #use. I know most of the time one edits a line or function and can use "Crtl+A" with "Alt+Enter" or "Alt+'" for a single line; but to reload other modules this would be nice.
Once thing I take for granted but is nice to know for people starting with F# it to make use of StackOverlow. I myself did not use this until after reading the book by Tomas Petricek and found that he answers questions at StackOverflow.
Before asking a question on StackOverflow one should search the existing questions to see if the answer doesn't already exist. In particular start with the questions voted most useful. When reading answers to F# questions, pay attention to the answers from these people under Answers - All time.
Note that both Phan and Jack are here on this project and I am very grateful to be working with them daily.
In trying to understand the hierarchy of theorems and supporting functions Domenico has created an Excel spreadsheet (TypesConstsDefsAxsThms.xlsx) in the _docs directory.
Sometimes people don't have access on Microsoft office to view such files, so Microsoft provides free viewers to view but not edit or create such files. See Office Online File Converters and Viewers
Another option that works with some office documents it to use Google Docs which is part ofGoogle Drive.
Just a thought. For creating faster loads need to look at using Native Image Generator (Ngen.exe)
I started looking into implementing the needs function from hol.ml and find that it references the OCaml Digest module which would be in compatibility module but needs to be implemented. It also makes use of the Top Level use directive via code which can be found in the OCaml toploop module. If one goes looking for the corresponding F# code that implements use in fsi.exe, fsi.fs, one will find many copies of the code. The first one I found in Github was for use with Mono. This lead me to the originating code drop from Microsoft at Codeplex with fsi.fs.
Since this is code to build an F# compiler and needs an F# compiler, you need a proto compiler to build the final compiler, so see the readme on how to build the proto compiler in the compiler\3.0\Sep2012 directory.
On a side note related to the F# compiler. Since many of have a use for the F# compiler AST for other F# tools such as Fantomas Dave Thomas has forked off a branch for just this purpose; note that the branch is not master but CompilerEditor.
Once we get the #use directive code working it might be possible for us to implement functionality similar to OCaml TopLevel #trace. Here is a quick and dirty version I did since F# doesn't have this ability.
07/18/2013
Usually when I research things I don't understand I have access to multiple machine running under VMware. This allows me to do things like view a few internet pages at once on different screens, see multiple e-mail messages, run multiple OS at the same time such as Windows and Linux, and to run different languages at the same time on clean installs such as ML, OCaml, F#, C#, Java, etc. Today is not one of those days.
To assist with debugging we are now adding toStringfunctions to our types. This will also help out with FSI AddPrinter.
Domenico has added some infixes() to the code. The way OCAml does infixes with the preprocessor makes sense; for this with HOL Light on F# I will have to do some learning.
Phan has been very productive with his next set of changes.
Phan did a change [here](Change value to function to bypass Exception) called "Change value to function to bypass Exception" which is also something I need to look into to understand better. If this is another tool for debugging F#, I need to learn it so I can add it to my F# debugging toolbox.
Phan also fixed the second and last shadowing change I made. It was a subtitle fix, changed th to th_001 on line 2876. I have to check, but this appears to fix the bug holding up running calc_rat.
Looking at the next push notice the change from pth to <| pth(). More learning for me. Also there are more ;; added. I guess here using the Verbose syntax is helping with debugging and will be pulled out once we have the core running.
If you have been noticing that we sometimes put type signature in above functions as comments then take them out, it is a quick way to help in debugging. By seeing the signature it makes it easy to understand the types for the parameters that are not there. This is especially helpful with single letter parameter names or when learning or seeing new functions for the first time. When I first started debugging F# I use to put the types into the function definition, but that can lead to converting generic code to non generic code which can cause other problems. What is better is to add the signatures as they appear with mouse-over, then if they are generic, add more signature comments with specific types. When it all works just delete the comments.
Notice also that instead of separating the load and open statements apart they appear later in the code and together. Since this is a script for debugging, it is actually a good idea as it allows you to quickly comment out the related code with one select and comment.
For this push only ;; are added at the end. Since F# light syntax can handle the ';;' this helps with debugging converted OCaml code as it makes if clear to the person and compiler where a function ends. They will be removed when we get all of the bugs out.
Today in looking how to make use of the F# compiler services I came across this. It is a bit dated, but something to keep in mind with regards for saving and restoring NHOL sessions and maybe as a way to implement a PROLOG assert and retract for use with NHOL. Basically instead of creating code with F# Interactive, debugging, moving to an FS file, compiling, restarting F# Interactive, loading *.dll for compiled assembly, and continuing, which I know one does not have to do or only do before shutting down F# Interactive, one would replace
moving to an FS file, compiling, restarting F# Interactive, loading *.dll for compiled assembly
with
assert <function name>.
This would take the function known to F# Interactive, compile it, store it in a database of functions and be usable by F# Interactive. Then when one leaves F# Interactive, all of those working functions can be saved and reloaded for the next session without having to copy the code from F# Interactive to an fs file, or keep a copy in an fs file while working with F# Interactive. Just an idea that needs more exploration.
Just ran across FsEye again. Wish I had remembered it a few days ago. Will come in handy for debugging.
In researching topics related to the needs function and automating the conversion of the HOL Light OCaml code, in particular theorems, to F# I keep running into Sergey Tihon's weekly F# blog. It basically gives you the pulse of F#. Not everything but worth the time to read from the first blog.
Here's another idea we borrow form OCaml people. Create a F# Interactive that compiles to native code instead of byte code for running. See OCamlNat.
07/22/13
Debugging is becoming less productive as it take about 30 minutes to run the scripts before the errors occur. We have decided to start replacing try with expressions with various functions based on choice. In reading up on these changes it is commonly noted to replace try with expressions with F# Option, but F# Choice will serve us better. Currently these changes are in the removing-exceptions branch, but this branch will most likely be deleted after we merge the changes. To help in this endeavor we have a Choice module in lib.fs and support functions in a Choice module in ExtCore Pervasive.fs. With these choice modules, changing the try with expression becomes more of a repeatable process.
Process:
- Find a function throwing exceptions
- Make it safe by using Choice.failwith (failing branches), Choice.bind, etc.
- Replace "func" by "Choice.get <| func" in NHol project
- Fix errors which mostly are changing <| to << and adding parentheses
- Create a commit with all changed files
Phan
07/25/13
To help in understanding the conversions necessary, Phan created the wiki page: How to: removing exceptions using Choice _, _.
To help me understand which functions to use I recorded their signatures.
x - used in code
ExtCore.Pervasive.Choice.result value : (Choice<'T, 'Error>)
ExtCore.Pervasive.Choice.error value : (Choice<'T, 'Error>)
NHol.lib.Choice.fail () : (Choice<'T, System.Exception>)
x NHol.lib.Choice.succeed (x : 'T) : (Choice<'T, 'Error>)
x NHol.lib.Choice.failwith (msg : string) : (Choice<'T, System.Exception>)
x NHol.lib.Choice.failwithPair (s: string) : (Choice<'T, System.Exception> * Choice<'U, System.Exception>)
ExtCore.Pervasive.Choice.exists (predicate : 'T -> bool) (value : Choice<'T, 'Error>) : bool
ExtCore.Pervasive.Choice.forall (predicate : 'T -> bool) (value : Choice<'T, 'Error>) : bool
ExtCore.Pervasive.Choice.fold (folder : 'State -> 'T -> 'State) (state : 'State) (value : Choice<'T, 'Error>) : 'State
ExtCore.Pervasive.Choice.foldBack (folder : 'T -> 'State -> 'State) (value : Choice<'T, 'Error>) (state : 'State) : 'State
ExtCore.Pervasive.Choice.iter (action : 'T -> unit) (value : Choice<'T, 'Error>) : unit
ExtCore.Pervasive.Choice.isError (value : Choice<'T, 'Error>) : bool
x ExtCore.Pervasive.Choice.isResult (value : Choice<'T, 'Error>) : bool
Seq.map ('T -> 'U) seq<'T> : seq<'U>)
List.map ('T -> 'U) 'T list : 'U list
x ExtCore.Pervasive.Choice.map (mapping : 'T -> 'U) (value : Choice<'T, 'Error>) : (Choice<'U, 'Error>)
x ExtCore.Pervasive.Choice.mapError (mapping : 'Err1 -> 'Err2) (value : Choice<'T, 'Err1>) : (Choice<'T, 'Err2>)
x NHol.lib.Choice.nestedFailwith (innerException : exn) (message : string) : (Choice<'T, System.Exception>)
x NHol.lib.Choice.nestedFailwithPair (innerException : exn) (message : string) : (Choice<'T, System.Exception> * Choice<'U, System.Exception>)
NHol.lib.Choice.pair (x : 'T, y : 'U ) : (Choice<'T, 'V> * Choice<'U, 'W>)
x ExtCore.Pervasive.Choice.bind (binding : 'T -> Choice<'U, 'Error>) (value : Choice<'T, 'Error>) : (Choice<'U, 'Error>)
x NHol.lib.Choice.bind2 (binding : 'T -> 'U -> Choice<'V,'Error>) (value1 : Choice<'T,'Error>) (value2 : Choice<'U,'Error>) : (Choice<'V, 'Error>)
x NHol.lib.Choice.bindError (binding : ('Error -> Choice<'T, 'Failure>)) (value : Choice<'T, 'Error>) : (Choice<'T, 'Failure>)
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.get (value : Choice<'T, #System.Exception>) : 'T
x NHol.lib.Choice.toOption (value : Choice<'T,'U>) : 'T option
ExtCore.Pervasive.Choice.failwithf (fmt : Printf.StringFormat<'T, Choice<'U, exn>>)