-
Notifications
You must be signed in to change notification settings - Fork 79
/
hol.ml
194 lines (157 loc) · 10.3 KB
/
hol.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
(* ========================================================================= *)
(* HOL LIGHT *)
(* *)
(* Modern OCaml version of the HOL theorem prover *)
(* *)
(* John Harrison *)
(* *)
(* (c) Copyright, University of Cambridge 1998 *)
(* (c) Copyright, John Harrison 1998-2007 *)
(* ========================================================================= *)
let hol_version = "2.20++";;
#directory "+compiler-libs";;
let hol_dir = ref
(try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;
(* ------------------------------------------------------------------------- *)
(* Should eventually change to "ref(Filename.temp_dir_name)". *)
(* However that's not available in 3.08, which is still the default *)
(* in Cygwin, and I don't want to force people to upgrade Ocaml. *)
(* ------------------------------------------------------------------------- *)
let temp_path = ref "/tmp";;
(* ------------------------------------------------------------------------- *)
(* Load files from system and/or user-settable directories. *)
(* Paths map initial "$/" to !hol_dir dynamically; use $$ to get the actual *)
(* $ character at the start of a directory. *)
(* ------------------------------------------------------------------------- *)
(* A flag that sets whether use_file must raise Failure if loading the file *)
(* did not succeed. If set to true, this helps (nested) loading of files fail*)
(* early. However, propagation of the failure will cause Toplevel to forget *)
(* bindings ('let .. = ..;;') that have been made before the erroneous *)
(* statement in the file. This leads to an inconsistent state between *)
(* variable and defined constants in HOL Light. *)
let use_file_raise_failure = ref false;;
let use_file s =
if Toploop.use_file Format.std_formatter s then ()
else if !use_file_raise_failure
then failwith("Error in included file "^s)
else (Format.print_string("Error in included file "^s);
Format.print_newline());;
let hol_expand_directory s =
if s = "$" || s = "$/" then !hol_dir
else if s = "$$" then "$"
else if String.length s <= 2 then s
else if String.sub s 0 2 = "$$" then (String.sub s 1 (String.length s - 1))
else if String.sub s 0 2 = "$/"
then Filename.concat (!hol_dir) (String.sub s 2 (String.length s - 2))
else s;;
let load_path = ref ["."; "$"];;
let loaded_files = ref [];;
let file_on_path p s =
if not (Filename.is_relative s) then s else
let p' = List.map hol_expand_directory p in
let d = List.find (fun d -> Sys.file_exists(Filename.concat d s)) p' in
Filename.concat (if d = "." then Sys.getcwd() else d) s;;
let load_on_path p s =
let s' = file_on_path p s in
let fileid = (Filename.basename s',Digest.file s') in
(use_file s'; loaded_files := fileid::(!loaded_files));;
let loads s = load_on_path ["$"] s;;
let loadt s = load_on_path (!load_path) s;;
let needs s =
let s' = file_on_path (!load_path) s in
let fileid = (Filename.basename s',Digest.file s') in
if List.mem fileid (!loaded_files)
then Format.print_string("File \""^s^"\" already loaded\n") else loadt s;;
(* ------------------------------------------------------------------------- *)
(* Load in parsing extensions. *)
(* For Ocaml < 3.10, use the built-in camlp4 *)
(* and for Ocaml >= 3.10, use camlp5 instead. *)
(* For Ocaml >= 4.14, use ocamlfind to locate camlp5. *)
(* ------------------------------------------------------------------------- *)
let ocaml_version = String.sub Sys.ocaml_version 0 4;;
let version_ge_3_10 = ocaml_version >= "3.10";;
let version_ge_4_14 = ocaml_version >= "4.14";;
if version_ge_4_14
then loads "load_camlp5_topfind.ml"
else if version_ge_3_10
then loads "load_camlp5.ml"
else loads "load_camlp4.ml";;
Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir) "pa_j.cmo");;
if version_ge_4_14
then loads "bignum_zarith.ml"
else loads "bignum_num.ml";;
(* ------------------------------------------------------------------------- *)
(* Bind this to a name that is independent of OCaml versions before it *)
(* is potentially overwritten by a theorem of the same name. On older *)
(* OCaml versions it is "Pervasives.sqrt", and on newer ones "Float.sqrt". *)
(* ------------------------------------------------------------------------- *)
let float_sqrt = sqrt;;
(* ------------------------------------------------------------------------- *)
(* 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 "firstorder.ml";; (* More utilities for first-order shadow terms *)
loads "metis.ml";; (* More advanced first-order automation: Metis *)
loads "thecops.ml";; (* Connection-based automation: leanCoP and nanoCoP *)
loads "quot.ml";; (* Derived rules for defining quotient types *)
loads "impconv.ml";; (* More powerful implicational rewriting etc. *)
(* ------------------------------------------------------------------------- *)
(* Mathematical theories and additional proof tools. *)
(* ------------------------------------------------------------------------- *)
loads "pair.ml";; (* Theory of pairs *)
loads "compute.ml";; (* General call-by-value reduction tool for terms *)
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 *)