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