Wrap module and open declarations with a compiler directive so they'r…

…e not used when running in scripting mode (i.e., F# interactive). This is to emulate the way hol-light loads code into the OCaml toplevel.

NHol/arith.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Natural number arithmetic.
 module NHol.arith
 
@@ -49,6 +51,7 @@ open quot
 open pair
 open nums
 open recursion
+#endif
 
 parse_as_infix("<", (12, "right"))
 parse_as_infix("<=", (12, "right"))

NHol/basics.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// More syntax constructors, and prelogical utilities like matching.
 module NHol.basics
 
@@ -28,6 +30,7 @@ open NHol
 open lib
 open fusion
 open fusion.Hol_kernel
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Create probably-fresh variable                                            *)

NHol/bool.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Boolean theory including (intuitionistic) defs of logical connectives.
 module NHol.bool
 
@@ -33,6 +35,7 @@ open printer
 open preterm
 open parser
 open equal
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Set up parse status of basic and derived logical constants.               *)

NHol/calc_int.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Calculation with integer-valued reals.
 module NHol.calc_int
 
@@ -57,6 +59,7 @@ open grobner
 open ind_types
 open lists
 open realax
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Syntax operations on integer constants of type ":real".                   *)

NHol/calc_num.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Calculation with natural numbers.
 module NHol.calc_num
 
@@ -51,6 +53,7 @@ open nums
 open recursion
 open arith
 open wf
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Simple rule to get rid of NUMERAL constant.                               *)

NHol/calc_rat.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Calculation with rational-valued reals.
 module NHol.calc_rat
 
@@ -60,6 +62,7 @@ open realax
 open calc_int
 open realarith
 open real
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Constant for decimal fractions written #xxx.yyy                           *)

NHol/canon.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Tools for putting terms in canonical forms.
 module NHol.canon
 
@@ -43,6 +45,7 @@ open theorems
 open ind_defs
 open ``class``
 open trivia
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Pre-simplification.                                                       *)

NHol/cart.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Finite Cartesian products.
 module NHol.cart
 
@@ -64,6 +66,7 @@ open calc_rat
 open int
 open sets
 open iterate
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Association of a number with an indexing type.                            *)

NHol/class.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Classical reasoning: Choice and Extensionality.
 module NHol.``class``
 
@@ -41,6 +43,7 @@ open itab
 open simp
 open theorems
 open ind_defs
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Eta-axiom, corresponding conversion, and extensionality.                  *)

NHol/define.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 // Support for general recursive definitions.
 module NHol.define
 
@@ -65,6 +67,7 @@ open int
 open sets
 open iterate
 open cart
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Constant supporting casewise definitions.                                 *)

NHol/drule.fs

@@ -18,8 +18,9 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// More sophisticated derived rules including definitions and rewriting.
-
 module NHol.drule
 
 open FSharp.Compatibility.OCaml
@@ -36,6 +37,7 @@ open preterm
 open parser
 open equal
 open bool
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Type of instantiations, with terms, types and higher-order data.          *)

NHol/equal.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Basic equality reasoning including conversionals.
 module NHol.equal
 
@@ -32,6 +34,7 @@ open nets
 open printer
 open preterm
 open parser
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Type abbreviation for conversions.                                        *)

NHol/fusion.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Complete HOL kernel of types, terms and theorems.
 module NHol.fusion
 
@@ -26,6 +28,7 @@ open FSharp.Compatibility.OCaml.Num
 
 open NHol
 open lib
+#endif
 
 [<AutoOpen>]
 module Hol_kernel = 

NHol/grobner.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Groebner basis procedure for most semirings.
 module NHol.grobner
 
@@ -53,6 +55,7 @@ open arith
 open wf
 open calc_num
 open normalizer
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Type for recording history, i.e. how a polynomial was obtained.           *)

NHol/ind_defs.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Derived rules for inductive definitions.
 module NHol.ind_defs
 
@@ -40,6 +42,7 @@ open tactics
 open itab
 open simp
 open theorems
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Strip off exactly n arguments from combination.                           *)

NHol/ind_types.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 //// Tools for defining inductive types.
 module NHol.ind_types
 
@@ -53,6 +55,7 @@ open arith
 open wf
 open calc_num
 open normalizer
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Abstract left inverses for binary injections (we could construct them...) *)

NHol/int.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Definition of integers.
 module NHol.int
 
@@ -61,6 +63,7 @@ open calc_int
 open realarith
 open real
 open calc_rat
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Representing predicate. The "is_int" variant is useful for backwards      *)

NHol/itab.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Intuitionistic theorem prover (complete for propositional fragment).
 module NHol.itab
 
@@ -37,6 +39,7 @@ open equal
 open bool
 open drule
 open tactics
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Accept a theorem modulo unification.                                      *)

NHol/iterate.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Iterated operations.
 module NHol.iterate
 
@@ -63,6 +65,7 @@ open real
 open calc_rat
 open int
 open sets
+#endif
 
 prioritize_num();;
 

NHol/lib.fs

@@ -18,25 +18,29 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Various useful general library functions.
 module NHol.lib
 
 open FSharp.Compatibility.OCaml
 open FSharp.Compatibility.OCaml.Num
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* A few missing functions to convert OCaml code to F#.                      *)
 (* ------------------------------------------------------------------------- *)
 
+// TODO : Move this into FSharp.Compatibility.OCaml
 module Ratio = 
     // NOTE : not sure what kind of normalization should be done here
     let normalize_ratio x = x
     let numerator_ratio(r : Ratio.ratio) = r.Numerator
     let denominator_ratio(r : Ratio.ratio) = r.Denominator
 
-// TODO : Replace uses of (==) with (===) from ExtCore.
-let (==) (x : 'T) (y : 'T) = obj.ReferenceEquals(x, y)
-let fail() = raise <| exn()
+let inline (==) (x : 'T) (y : 'T) =
+    System.Object.ReferenceEquals(x, y)
+let inline fail() = raise <| exn()
 
 // The exception fired by failwith is used as a control flow.
 // KeyNotFoundException is not recognized in many cases, so we have to use redefine Failure for compatibility.

NHol/lists.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// Theory of lists.
 module NHol.lists
 
@@ -55,6 +57,7 @@ open calc_num
 open normalizer
 open grobner
 open ind_types
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Standard tactic for list induction using MATCH_MP_TAC list_INDUCT         *)

NHol/meson.fs

@@ -18,6 +18,8 @@ limitations under the License.
 
 *)
 
+#if INTERACTIVE
+#else
 /// First order automation: MESON (model elimination).
 module NHol.meson
 
@@ -44,6 +46,7 @@ open ind_defs
 open ``class``
 open trivia
 open canon
+#endif
 
 (* ------------------------------------------------------------------------- *)
 (* Some parameters controlling MESON behaviour.                              *)