-
Notifications
You must be signed in to change notification settings - Fork 3
/
hol.ml
182 lines (147 loc) · 9.28 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
(* ========================================================================= *)
(* 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++";;
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 in parsing extensions. *)
(* For Ocaml < 3.10, use the built-in camlp4 *)
(* and for Ocaml >= 3.10, use camlp5 instead. *)
(* ------------------------------------------------------------------------- *)
if let v = String.sub Sys.ocaml_version 0 4 in v >= "3.10"
then (Topdirs.dir_directory "+camlp5";
Topdirs.dir_load Format.std_formatter "camlp5o.cma")
else (Topdirs.dir_load Format.std_formatter "camlp4o.cma");;
Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir) "pa_j.cmo");;
(* ------------------------------------------------------------------------- *)
(* 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. *)
(* ------------------------------------------------------------------------- *)
let use_file s =
if Toploop.use_file Format.std_formatter s then ()
else (Format.print_string("Error in included file "^s);
Format.print_newline());;
let hol_expand_directory s =
if s = "$" or 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;;
let profile_loads s =
let mem1 = Gc.allocated_bytes () in
let time1 = Sys.time() in
let _ = loads s in
let mem2 = Gc.allocated_bytes () in
let time2 = Sys.time() in
print_endline ("mem: "^(string_of_float (mem2 -. mem1))^", time: "^(string_of_float (time2 -. time1)));;
(* ------------------------------------------------------------------------- *)
(* Various tweaks to OCaml and general library functions. *)
(* ------------------------------------------------------------------------- *)
loads "hiproofs/hiproofs.ml";;
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 "hiproofs/mods/equal_m.ml";;
loads "bool.ml";; (* Boolean theory and basic derived rules *)
loads "hiproofs/mods/bool_m.ml";;
loads "drule.ml";; (* Additional derived rules *)
loads "hiproofs/mods/drule_m.ml";;
loads "tactics.ml";; (* Tactics, tacticals and goal stack *)
loads "hiproofs/mods/tactics_m.ml";;
loads "itab.ml";; (* Toy prover for intuitionistic logic *)
loads "simp.ml";; (* Basic rewriting and simplification tools. *)
loads "hiproofs/mods/simp_m.ml";;
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 "hiproofs/mods/class_m.ml";;
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 "hiproofs/mods/meson_m.ml";;
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 "hiproofs/mods/nums_m.ml";;
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 "hiproofs/mods/calc_rat_m.ml";;
loads "int.ml";; (* Definition of integers *)
loads "hiproofs/mods/int_m.ml";;
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 *)
loads "hiproofs/main.ml";;