Sys.chdir hol_dir;;
let rec do_list f l =
match l with
[] -> ()
| (h::t) -> (f h; do_list f t);;
do_list (fun s -> Topdirs.dir_directory(Filename.concat ocaml_source_dir s))
["parsing"; "typing"; "utils"];;
(* This must be loaded first! It is stateful, and affects Predef *)
#load "ident.cmo";;
#load "misc.cmo";;
#load "path.cmo";;
#load "types.cmo";;
#load "btype.cmo";;
#load "tbl.cmo";;
#load "subst.cmo";;
#load "predef.cmo";;
#load "datarepr.cmo";;
#load "config.cmo";;
#load "consistbl.cmo";;
#load "clflags.cmo";;
#load "env.cmo";;
#load "ctype.cmo";;
#load "printast.cmo";;
#load "oprint.cmo";;
#load "primitive.cmo";;
#load "printtyp.cmo";;
if let v = String.sub Sys.ocaml_version 0 4 in
v >= "3.10"
then (Topdirs.dir_directory "+camlp5";
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());;
if Sys.file_exists "sys.ml" then
use_file "sys.ml"
else
use_file "system.ml";;
let needs f = ();;
#use "lib.ml";;
#use "fusion.ml";;
use_file (Filename.concat ocaml_tools_dir "fixnames.ml");;
module OldToploop = Toploop;;
module OldTopdirs = Topdirs;;
let (store_read_result,begin_load,end_load,get_libs,inject_hol_include) = let libs = ref []
and stack = ref (Stack.create ())
and known = ref (Hashtbl.create 10)
and hol_core_loaded = ref false
and bnds_size = ref 0 in
let _read = ref [] in
let store_read_result s = _read := (List.map fixNames s);
and listify l = if l = [] then "[]"
else "[\n"^(List.fold_right (fun a b -> a^";\n"^b) l "")^"\n]\n" in
let file_of_string filename s =
let fd = Pervasives.open_out filename in
output_string fd s; close_out fd
and pairnames = List.map (fun n -> "(\""^n^"\","^n^")") in
let read_global_vals tns = let exptext =
"store_read_result " ^
(listify(pairnames tns))^
";;\n" in
(let filename = Filename.temp_file "read_global_vals" ".ml" in
file_of_string filename exptext;
use_file filename;
Sys.remove filename) in
let map_new_syms lib =
let rec funpow n f x =
if n < 1 then x else funpow (n-1) f (f x)
and get_value_bindings env =
let rec get_val acc = function
| Env.Env_empty -> acc
| Env.Env_value (next, ident, val_descr) ->
get_val ((ident,val_descr)::acc) next
| Env.Env_type (next,_,_) -> get_val acc next
| Env.Env_exception (next,_,_) -> get_val acc next
| Env.Env_module (next,_,_) -> get_val acc next
| Env.Env_modtype (next,_,_) -> get_val acc next
| Env.Env_class (next,_,_) -> get_val acc next
| Env.Env_cltype (next,_,_) -> get_val acc next
| Env.Env_open (next,_) -> get_val acc next
in get_val [] (Env.summary env)
and type_to_str (x : Types.type_expr) =
let pred = (fun (ident,val_descr) ->
let n = Ident.name ident in
if type_to_str val_descr.Types.val_type = "thm" & n <> "it"
then true else false)
and bnds = get_value_bindings (!Toploop.toplevel_env) in
let new_bnds = funpow (!bnds_size) (List.tl) bnds in
let new_ths = List.filter pred new_bnds in
let new_th_names = List.map (fun (ident,_) -> Ident.name ident) new_ths in
let lib_ths = Hashtbl.find (!known) lib in
(Format.print_string("MAP SYMS - Stack:"^(if (not(Stack.is_empty (!stack))) then Stack.top (!stack) else "")^", lib: "^lib);
bnds_size := List.length bnds;
read_global_vals new_th_names;
List.iter (fun (t,tv) -> Hashtbl.replace lib_ths t tv)
(!_read);
Hashtbl.replace (!known) lib lib_ths in
let begin_load lib = if lib <> "export.ml" && lib <> (Filename.concat hol_dir "fusion.ml") && ((lib <> (Filename.concat hol_dir "hol.ml") && lib <> "hol.ml") || not (!hol_core_loaded)) then
((if(lib <> (Filename.concat hol_dir "hol.ml") || lib <> "hol.ml") then hol_core_loaded := true else ()); (if (Stack.is_empty (!stack)) then ()
else
let plib = Stack.top (!stack)
in map_new_syms plib;
(Format.print_string("LIBLINK:"^lib);
libs :=
(lib,plib)::(!libs));
(Format.print_string("Lib put on stack:"^lib);
Stack.push lib (!stack);
Hashtbl.add (!known) lib (Hashtbl.create 10);
true) else false
and end_load () =
let bname = (Filename.basename (Stack.top (!stack)))
in (if bname = "preterm.ml"
then let filename = Filename.temp_file "rebind" ".ml"
in (file_of_string filename "type_invention_warning:=false";
use_file filename;
Sys.remove filename)
else ());
(if bname = "lib.ml"
then let filename = Filename.temp_file "rebind" ".ml"
in (file_of_string filename "verbose:=false";
use_file filename;
Sys.remove filename)
else ()); map_new_syms (Stack.pop (!stack))
and inject_hol_include f = (libs := (!libs)@[("hol.ml",f)])
and get_libs () = let empty = Hashtbl.fold (fun k v t -> if Hashtbl.length v == 0 then k::t else t) (!known) []
and purge = fun names (h,l) -> (Hashtbl.fold (fun k v t -> (if List.mem k names then () else Hashtbl.add t k v); t) h (Hashtbl.create (Hashtbl.length h)),List.filter (fun (s,_) -> not(List.mem s names)) l)
and childnodes = fun n l -> List.fold_left (fun ch (s,t) -> if t == n || List.mem t ch then s::ch else ch) [] l
in let purgable = fun empty l -> List.filter (fun n ->
List.fold_left (fun b n1 -> b & (List.mem n1 empty)) true (childnodes n l)
) empty
in purge (purgable empty (!libs)) (!known,!libs)
in
(store_read_result,begin_load,end_load,get_libs,inject_hol_include);;
module Topdirs =
struct
type 'a printer_type_new = Format.formatter -> 'a -> unit
type 'a printer_type_old = 'a -> unit
let dir_quit = OldTopdirs.dir_quit
let dir_directory = OldTopdirs.dir_directory
let dir_cd = OldTopdirs.dir_cd
let dir_load = fun f s -> if begin_load s then (OldTopdirs.dir_load f s; end_load()) else ()
let dir_use = fun f s -> if begin_load s then (OldTopdirs.dir_use f s; end_load()) else ()
let dir_install_printer = OldTopdirs.dir_install_printer
let dir_remove_printer = OldTopdirs.dir_remove_printer
let dir_trace = OldTopdirs.dir_trace
let dir_untrace = OldTopdirs.dir_untrace
let dir_untrace_all = OldTopdirs.dir_untrace_all
let load_file = fun f s -> if begin_load s then let ret = OldTopdirs.load_file f s and _ = end_load() in ret else true
end
module Toploop =
struct
let getvalue = OldToploop.getvalue
let setvalue = OldToploop.setvalue
let set_paths = OldToploop.set_paths
let loop = OldToploop.loop
let run_script = OldToploop.run_script
let directive_table = OldToploop.directive_table
let toplevel_env = OldToploop.toplevel_env
let initialize_toplevel_env = OldToploop.initialize_toplevel_env
let print_exception_outcome = OldToploop.print_exception_outcome
let execute_phrase = OldToploop.execute_phrase
let use_file = fun f s -> if begin_load s then let ret = OldToploop.use_file f s and _ = end_load() in ret else true
let use_silently = fun f s -> if begin_load s then let ret = OldToploop.use_silently f s and _ = end_load in ret else true
let eval_path = OldToploop.eval_path
let print_value = OldToploop.print_value
let print_untyped_exception = OldToploop.print_untyped_exception
let install_printer = OldToploop.install_printer
let remove_printer = OldToploop.remove_printer
let max_printer_depth = OldToploop.max_printer_depth
let max_printer_steps = OldToploop.max_printer_steps
let parse_toplevel_phrase = OldToploop.parse_toplevel_phrase
let parse_use_file = OldToploop.parse_use_file
let print_location = OldToploop.print_location
let print_error = OldToploop.print_error
let print_warning = OldToploop.print_warning
let input_name = OldToploop.input_name
let print_out_value = OldToploop.print_out_value
let print_out_type = OldToploop.print_out_type
let print_out_class_type = OldToploop.print_out_class_type
let print_out_module_type = OldToploop.print_out_module_type
let print_out_sig_item = OldToploop.print_out_sig_item
let print_out_signature = OldToploop.print_out_signature
let print_out_phrase = OldToploop.print_out_phrase
let read_interactive_input = OldToploop.read_interactive_input
let toplevel_startup_hook = OldToploop.toplevel_startup_hook
let may_trace = OldToploop.may_trace
end
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());;