hol.ml

   1 (* ========================================================================= *)
   2 (*                               HOL LIGHT                                   *)
   3 (*                                                                           *)
   4 (*              Modern OCaml version of the HOL theorem prover               *)
   5 (*                                                                           *)
   6 (*                            John Harrison                                  *)
   7 (*                                                                           *)
   8 (*            (c) Copyright, University of Cambridge 1998                    *)
   9 (*              (c) Copyright, John Harrison 1998-2007                       *)
  10 (* ========================================================================= *)
  11
  12 let hol_version = "2.20++";;
  13
  14 #directory "+compiler-libs";;
  15
  16 let hol_dir = ref
  17   (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* Should eventually change to "ref(Filename.temp_dir_name)".                *)
  21 (* However that's not available in 3.08, which is still the default          *)
  22 (* in Cygwin, and I don't want to force people to upgrade Ocaml.             *)
  23 (* ------------------------------------------------------------------------- *)
  24
  25 let temp_path = ref "/tmp";;
  26
  27 (* ------------------------------------------------------------------------- *)
  28 (* Load in parsing extensions.                                               *)
  29 (* For Ocaml < 3.10, use the built-in camlp4                                 *)
  30 (* and for Ocaml >= 3.10, use camlp5 instead.                                *)
  31 (* ------------------------------------------------------------------------- *)
  32
  33 if let v = String.sub Sys.ocaml_version 0 4 in v >= "3.10"
  34 then (Topdirs.dir_directory "+camlp5";
  35       Topdirs.dir_load Format.std_formatter "camlp5o.cma")
  36 else (Topdirs.dir_load Format.std_formatter "camlp4o.cma");;
  37
  38 Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir) "pa_j.cmo");;
  39
  40 (* ------------------------------------------------------------------------- *)
  41 (* Load files from system and/or user-settable directories.                  *)
  42 (* Paths map initial "$/" to !hol_dir dynamically; use $$ to get the actual  *)
  43 (* $ character at the start of a directory.                                  *)
  44 (* ------------------------------------------------------------------------- *)
  45
  46 let file_stack = ref [];;
  47 let file_order = ref [];;
  48 let use_file_start_hook = ref (fun (s : string) -> file_stack := s :: !file_stack);;
  49 let use_file_end_hook = ref (fun (s : string) ->
  50   file_order := s :: !file_order;
  51   if !file_stack <> [] then file_stack := List.tl !file_stack
  52 );;
  53 let use_file s =
  54   !use_file_start_hook s;
  55   let ret = Toploop.use_file Format.std_formatter s in
  56   !use_file_end_hook s;
  57   if ret then () else (Format.print_string("Error in included file "^s); Format.print_newline());;
  58
  59 let hol_expand_directory s =
  60   if s = "$" or s = "$/" then !hol_dir
  61   else if s = "$$" then "$"
  62   else if String.length s <= 2 then s
  63   else if String.sub s 0 2 = "$$" then (String.sub s 1 (String.length s - 1))
  64   else if String.sub s 0 2 = "$/"
  65   then Filename.concat (!hol_dir) (String.sub s 2 (String.length s - 2))
  66   else s;;
  67
  68 let load_path = ref ["."; "$"];;
  69
  70 let loaded_files = ref [];;
  71
  72 let file_on_path p s =
  73   if not (Filename.is_relative s) then s else
  74   let p' = List.map hol_expand_directory p in
  75   let d = List.find (fun d -> Sys.file_exists(Filename.concat d s)) p' in
  76   Filename.concat (if d = "." then Sys.getcwd() else d) s;;
  77
  78 let load_on_path p s =
  79   let s' = file_on_path p s in
  80   let fileid = (Filename.basename s',Digest.file s') in
  81   (use_file s'; loaded_files := fileid::(!loaded_files));;
  82
  83 let loads s = load_on_path ["$"] s;;
  84
  85 let loadt s = load_on_path (!load_path) s;;
  86
  87 let needs s =
  88   let s' = file_on_path (!load_path) s in
  89   let fileid = (Filename.basename s',Digest.file s') in
  90   if List.mem fileid (!loaded_files)
  91   then Format.print_string("File \""^s^"\" already loaded\n") else loadt s;;
  92
  93 (* ------------------------------------------------------------------------- *)
  94 (* Various tweaks to OCaml and general library functions.                    *)
  95 (* ------------------------------------------------------------------------- *)
  96
  97 loads "system.ml";;     (* Set up proper parsing and load bignums            *)
  98 loads "lib.ml";;        (* Various useful general library functions          *)
  99
 100 (* ------------------------------------------------------------------------- *)
 101 (* The logical core.                                                         *)
 102 (* ------------------------------------------------------------------------- *)
 103
 104 loads "fusion.ml";;
 105
 106 (* ------------------------------------------------------------------------- *)
 107 (* Some extra support stuff needed outside the core.                         *)
 108 (* ------------------------------------------------------------------------- *)
 109
 110 loads "basics.ml";;     (* Additional syntax operations and other utilities  *)
 111 loads "nets.ml";;       (* Term nets for fast matchability-based lookup      *)
 112
 113 (* ------------------------------------------------------------------------- *)
 114 (* The interface.                                                            *)
 115 (* ------------------------------------------------------------------------- *)
 116
 117 loads "printer.ml";;    (* Crude prettyprinter                               *)
 118 loads "preterm.ml";;    (* Preterms and their interconversion with terms     *)
 119 loads "parser.ml";;     (* Lexer and parser                                  *)
 120
 121 (* ------------------------------------------------------------------------- *)
 122 (* Higher level deductive system.                                            *)
 123 (* ------------------------------------------------------------------------- *)
 124
 125 loads "equal.ml";;      (* Basic equality reasoning and conversionals        *)
 126 loads "bool.ml";;       (* Boolean theory and basic derived rules            *)
 127 loads "drule.ml";;      (* Additional derived rules                          *)
 128 loads "tactics.ml";;    (* Tactics, tacticals and goal stack                 *)
 129 loads "itab.ml";;       (* Toy prover for intuitionistic logic               *)
 130 loads "simp.ml";;       (* Basic rewriting and simplification tools.         *)
 131 loads "theorems.ml";;   (* Additional theorems (mainly for quantifiers) etc. *)
 132 loads "ind_defs.ml";;   (* Derived rules for inductive definitions           *)
 133 loads "class.ml";;      (* Classical reasoning: Choice and Extensionality    *)
 134 loads "trivia.ml";;     (* Some very basic theories, e.g. type ":1"          *)
 135 loads "canon.ml";;      (* Tools for putting terms in canonical forms        *)
 136 loads "meson.ml";;      (* First order automation: MESON (model elimination) *)
 137 loads "quot.ml";;       (* Derived rules for defining quotient types         *)
 138 loads "impconv.ml";;    (* More powerful implicational rewriting etc.        *)
 139
 140 (* ------------------------------------------------------------------------- *)
 141 (* Mathematical theories and additional proof tools.                         *)
 142 (* ------------------------------------------------------------------------- *)
 143
 144 loads "pair.ml";;       (* Theory of pairs                                   *)
 145 loads "nums.ml";;       (* Axiom of Infinity, definition of natural numbers  *)
 146 loads "recursion.ml";;  (* Tools for primitive recursion on inductive types  *)
 147 loads "arith.ml";;      (* Natural number arithmetic                         *)
 148 loads "wf.ml";;         (* Theory of wellfounded relations                   *)
 149 loads "calc_num.ml";;   (* Calculation with natural numbers                  *)
 150 loads "normalizer.ml";; (* Polynomial normalizer for rings and semirings     *)
 151 loads "grobner.ml";;    (* Groebner basis procedure for most semirings.      *)
 152 loads "ind_types.ml";;  (* Tools for defining inductive types                *)
 153 loads "lists.ml";;      (* Theory of lists                                   *)
 154 loads "realax.ml";;     (* Definition of real numbers                        *)
 155 loads "calc_int.ml";;   (* Calculation with integer-valued reals             *)
 156 loads "realarith.ml";;  (* Universal linear real decision procedure          *)
 157 loads "real.ml";;       (* Derived properties of reals                       *)
 158 loads "calc_rat.ml";;   (* Calculation with rational-valued reals            *)
 159 loads "int.ml";;        (* Definition of integers                            *)
 160 loads "sets.ml";;       (* Basic set theory.                                 *)
 161 loads "iterate.ml";;    (* Iterated operations                               *)
 162 loads "cart.ml";;       (* Finite Cartesian products                         *)
 163 loads "define.ml";;     (* Support for general recursive definitions         *)
 164
 165 (* ------------------------------------------------------------------------- *)
 166 (* The help system.                                                          *)
 167 (* ------------------------------------------------------------------------- *)
 168
 169 loads "help.ml";;       (* Online help using the entries in Help directory   *)
 170 loads "database.ml";;   (* List of name-theorem pairs for search system      *)