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
|
(* ========================================================================= *)
(* HOL LIGHT *)
(* *)
(* Modern OCaml version of the HOL theorem prover *)
(* *)
(* John Harrison *)
(* *)
(* (c) Copyright, University of Cambridge 1998 *)
(* (c) Copyright, John Harrison 1998-2024 *)
(* (c) Copyright, Juneyoung Lee 2024 *)
(* ========================================================================= *)
let argn = Array.length Sys.argv;;
if argn < 3 || argn > 4 then
let _ = Printf.eprintf "inline_load.ml <input.ml> <output.ml> [-omit-prelude]\n" in
let _ = Printf.eprintf " -omit-prelude: omit 'open Hol_lib;;' and 'open Hol_loader;;'.\n" in
exit 1;;
try
let v = Sys.getenv "HOLLIGHT_DIR" in
if v = "" then Printf.printf "Warning: HOLLIGHT_DIR is not set\n%!"
with Not_found -> Printf.printf "Warning: HOLLIGHT_DIR is not set\n%!";;
let filename = Sys.argv.(1);;
let fout = open_out (Sys.argv.(2));;
let omit_prelude = argn >= 4 && Sys.argv.(3) = "-omit-prelude";;
if not omit_prelude then
Printf.fprintf fout "open Hol_lib;;\nopen Hol_loader;;\n";;
#use "hol_loader.ml";;
let parse_load_statement fnname stmt: (string * string) option =
let stmt = String.trim stmt in
if not (String.starts_with ~prefix:fnname stmt) then None else
let n = String.length fnname in
let stmt = String.trim (String.sub stmt n (String.length stmt - n)) in
if not (stmt.[0] = '"') then None else
let stmt = String.sub stmt 1 (String.length stmt - 1) in
let idx = String.index stmt '"' in
if idx = -1 then None else
let path = String.sub stmt 0 idx in
let stmt = String.sub stmt (idx + 1) (String.length stmt - idx - 1) in
let stmt = String.trim stmt in
if not (String.starts_with ~prefix:";;" stmt) then None else
let stmt = String.sub stmt 2 (String.length stmt - 2) in
Some (path,stmt);;
let strings_of_file filename =
let fd =
try open_in filename
with Sys_error _ -> failwith("strings_of_file: can't open "^filename) in
let rec suck_lines acc =
let l = try [input_line fd] with End_of_file -> [] in
if l = [] then List.rev acc else suck_lines(List.hd l::acc) in
let data = suck_lines [] in
(close_in fd; data);;
file_loader := fun filename ->
let open Printf in
fprintf fout "(* %s *)\n" filename;
let lines = strings_of_file filename in
let fail_if_nonexistent f x = try f x with _ -> failwith x in
List.iter
(fun line ->
match parse_load_statement "loadt" line with
| Some (path,line') -> fail_if_nonexistent loadt path; fprintf fout "%s\n" line' | None ->
(match parse_load_statement "loads" line with
| Some (path,line') -> begin
if path = "update_database.ml"
then Printf.printf "Warning: 'loads \"update_database.ml\";;' is omitted\n"
else (fail_if_nonexistent loads path; fprintf fout "%s\n" line')
end
| None ->
(match parse_load_statement "needs" line with
| Some (path,line') -> fail_if_nonexistent needs path; fprintf fout "%s\n" line'
| None -> fprintf fout "%s\n" line (* no linebreak needed! *))))
lines;
(* add digest *)
let digest_str = Digest.file filename in
let digest = Bytes.of_string digest_str in
let the_str = ref "" in
Bytes.iter (fun c ->
let i = Char.code c in
if !the_str = ""
then the_str := string_of_int i
else the_str := !the_str ^ "; " ^ (string_of_int i))
digest;
fprintf fout "(* update digest *)\n";
fprintf fout "loaded_files := \n";
fprintf fout " let digest_bytes = [|%s|] in\n" !the_str;
fprintf fout " let digest = Bytes.init (Array.length digest_bytes) (fun i -> Char.chr digest_bytes.(i)) in\n";
fprintf fout " (\"%s\", Bytes.to_string digest)::!loaded_files;;\n\n" (Filename.basename filename);
true;;
loadt filename;;
close_out fout;;
|
