-
Notifications
You must be signed in to change notification settings - Fork 79
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #108 from aqjune-aws/module3
Support compilation of HOL Light
- Loading branch information
Showing
9 changed files
with
180 additions
and
14 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,15 @@ | ||
| (* ========================================================================= *) | ||
| (* 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 *) | ||
| (* ========================================================================= *) | ||
|
|
||
| Topdirs.dir_load Format.std_formatter | ||
| (Filename.concat (!hol_dir) "hol_lib.cmo");; | ||
| include Hol_lib;; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,82 @@ | ||
| (* ========================================================================= *) | ||
| (* 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 *) | ||
| (* ========================================================================= *) | ||
|
|
||
| if Array.length Sys.argv <> 3 then | ||
| let _ = Printf.eprintf "inline_load.ml <input.ml> <output.ml>\n" in | ||
| exit 1;; | ||
|
|
||
| let filename = Sys.argv.(1);; | ||
| let fout = open_out (Sys.argv.(2));; | ||
|
|
||
| #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 | ||
| List.iter | ||
| (fun line -> | ||
| match parse_load_statement "loadt" line with | ||
| | Some (path,line') -> loadt path; fprintf fout "%s\n" line' | None -> | ||
| (match parse_load_statement "loads" line with | ||
| | Some (path,line') -> loads path; fprintf fout "%s\n" line' | None -> | ||
| (match parse_load_statement "needs" line with | ||
| | Some (path,line') -> 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;; |