From f1d434e2044840f1e3ee7dc7d359a1f25846881e Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 3 Dec 1999 17:32:44 +0000 Subject: compilation native git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@201 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 12 +++ Makefile | 12 ++- parsing/g_natsyntax.ml | 81 +++++++++++++++ parsing/g_natsyntax.mli | 4 + parsing/g_zsyntax.ml | 157 ++++++++++++++++++++++++++++ parsing/g_zsyntax.mli | 4 + scripts/coqmktop.ml | 3 +- toplevel/mltop.ml | 268 ----------------------------------------------- toplevel/mltop.ml4 | 271 ++++++++++++++++++++++++++++++++++++++++++++++++ 9 files changed, 541 insertions(+), 271 deletions(-) create mode 100644 parsing/g_natsyntax.ml create mode 100644 parsing/g_natsyntax.mli create mode 100644 parsing/g_zsyntax.ml create mode 100644 parsing/g_zsyntax.mli delete mode 100644 toplevel/mltop.ml create mode 100644 toplevel/mltop.ml4 diff --git a/.depend b/.depend index 547c304d03..b5035826f4 100644 --- a/.depend +++ b/.depend @@ -432,6 +432,18 @@ parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ lib/gmap.cmi lib/gmapl.cmi lib/pp.cmi lib/util.cmi parsing/esyntax.cmi parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \ lib/gmap.cmx lib/gmapl.cmx lib/pp.cmx lib/util.cmx parsing/esyntax.cmi +parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \ + parsing/coqast.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \ + lib/pp.cmi lib/util.cmi parsing/g_natsyntax.cmi +parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \ + parsing/coqast.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmi \ + lib/pp.cmx lib/util.cmx parsing/g_natsyntax.cmi +parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \ + parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \ + lib/util.cmi +parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \ + parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx \ + lib/util.cmx parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi parsing/pretty.cmo: pretyping/classops.cmi kernel/constant.cmi \ diff --git a/Makefile b/Makefile index f2c7be6092..15d3839b0e 100644 --- a/Makefile +++ b/Makefile @@ -85,6 +85,7 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/extend.cmo parsing/termast.cmo \ parsing/esyntax.cmo parsing/printer.cmo parsing/pretty.cmo \ parsing/astterm.cmo parsing/egrammar.cmo +ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo PROOFS=proofs/proof_trees.cmo proofs/logic.cmo \ proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \ @@ -107,7 +108,7 @@ CMXA=$(CMA:.cma=.cmxa) CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \ $(PROOFS) $(TACTICS) $(TOPLEVEL) -CMX=$(CMO:.cmo=.cmx) +CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx) ########################################################################### # Main targets @@ -255,6 +256,15 @@ parsing/extend.cmx: parsing/extend.ml4 parsing/grammar.cma beforedepend:: $(GRAMMARCMO) +# toplevel/mltop.ml4 (ifdef Opt) + +CAMLP4IFDEF=camlp4o pa_ifdef.cmo + +toplevel/mltop.cmo: toplevel/mltop.ml4 + $(OCAMLC) $(BYTEFLAGS) -c -pp "$(CAMLP4IFDEF) -DByte -impl" -impl $< +toplevel/mltop.cmx: toplevel/mltop.ml4 + $(OCAMLOPT) $(OPTFLAGS) -c -pp "$(CAMLP4IFDEF) -impl" -impl $< + ########################################################################### # Default rules ########################################################################### diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml new file mode 100644 index 0000000000..1c5b64623e --- /dev/null +++ b/parsing/g_natsyntax.ml @@ -0,0 +1,81 @@ + +(* $Id$ *) + +(* This file to allow writing (3) for (S (S (S O))) + and still write (S y) for (S y) *) + +open Pcoq +open Pp +open Util +open Names +open Coqast +open Ast + +exception Non_closed_number + +let get_nat_sign loc = + let ast_of_id id = Astterm.globalize_command (Nvar(loc,id)) in + (ast_of_id "O", ast_of_id "S", ast_of_id "My_special_variable") + +(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *) +let nat_of_int n dloc = + let (astO,astS,_) = get_nat_sign dloc in + let rec mk_nat n = + if n <= 0 then + astO + else + Node(dloc,"APPLIST", [astS; mk_nat (n-1)]) + in + mk_nat n + +let nat_of_string s dloc = + nat_of_int (int_of_string s) dloc + +let rec int_of_nat_rec astS astO p = + match p with + | Node (_,"APPLIST", [b; a]) when alpha_eq(b,astS) -> + (int_of_nat_rec astS astO a)+1 + | a when alpha_eq(a,astO) -> 1 + (***** YES, 1, non 0 ... to print the successor of p *) + | _ -> raise Non_closed_number + +let int_of_nat p = + let (astO,astS,_) = get_nat_sign dummy_loc in + try + Some (int_of_nat_rec astS astO p) + with + Non_closed_number -> None + +let replace_S p = + let (_,astS,astmyvar) = get_nat_sign dummy_loc in + let rec aux p = + match p with + | Node (l,"APPLIST", [b; a]) when b = astS -> + Node (l, "APPLIST", [astmyvar; (aux a)]) + | _ -> p + in + ope("APPLIST", [astmyvar; (aux p)]) + + +(* Declare the primitive printer *) + +(* Prints not p, but the SUCCESSOR of p !!!!! *) +let nat_printer std_pr p = + match (int_of_nat p) with + | Some i -> [< 'sTR (string_of_int i) >] + | None -> std_pr (replace_S p) + +let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer) + +(* Declare the primitive parser *) + +let number = + match create_entry (get_univ "nat") "number" ETast with + | Ast n -> n + | _ -> anomaly "G_natsyntax : create_entry number failed" + +let _ = + Gram.extend number None + [None, None, + [[Gramext.Stoken ("INT", "")], + Gramext.action nat_of_string]] diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli new file mode 100644 index 0000000000..61f305ad9c --- /dev/null +++ b/parsing/g_natsyntax.mli @@ -0,0 +1,4 @@ + +(* $Id$ *) + +(* Nice syntax for naturals. *) diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml new file mode 100644 index 0000000000..8128cb3d99 --- /dev/null +++ b/parsing/g_zsyntax.ml @@ -0,0 +1,157 @@ + +(* $Id$ *) + +open Coqast +open Pcoq +open Pp +open Util +open Names +open Ast + +let get_z_sign loc = + let ast_of_id id = Astterm.globalize_command (Nvar(loc,id)) in + ((ast_of_id "xI", ast_of_id "xO", ast_of_id "xH"), + (ast_of_id "ZERO", ast_of_id "POS", ast_of_id "NEG"), + (ast_of_id "My_special_variable0", ast_of_id "My_special_variable1")) + +let int_array_of_string s = + let a = Array.create (String.length s) 0 in + for i = 0 to String.length s - 1 do + a.(i) <- int_of_string (String.sub s i 1) + done; + a + +let string_of_int_array s = + String.concat "" (Array.to_list (Array.map string_of_int s)) + +let is_nonzero a = + let b = ref false in Array.iter (fun x -> b := x <> 0 || !b) a; !b + +let div2_with_rest n = + let len = Array.length n in + let q = Array.create len 0 in + for i = 0 to len - 2 do + q.(i) <- q.(i) + n.(i) / 2; q.(i + 1) <- 5 * (n.(i) mod 2) + done; + q.(len - 1) <- q.(len - 1) + n.(len - 1) / 2; + q, n.(len - 1) mod 2 + +let add_1 n = + let m = Array.copy n + and i = ref (Array.length n - 1) in + m.(!i) <- m.(!i) + 1; + while m.(!i) = 10 && !i > 0 do + m.(!i) <- 0; decr i; m.(!i) <- m.(!i) + 1 + done; + if !i = 0 && m.(0) = 10 then begin + m.(0) <- 0; Array.concat [[| 1 |]; m] + end else + m + +let rec mult_2 n = + let m = Array.copy n in + m.(Array.length n - 1) <- 2 * m.(Array.length n - 1); + for i = Array.length n - 2 downto 0 do + m.(i) <- 2 * m.(i); + if m.(i + 1) >= 10 then begin + m.(i + 1) <- m.(i + 1) - 10; m.(i) <- m.(i) + 1 + end + done; + if m.(0) >= 10 then begin + m.(0) <- m.(0) - 10; Array.concat [[| 1 |]; m] + end else + m + +let pos_of_int_array astxI astxO astxH x = + let rec pos_of x = + match div2_with_rest x with + | (q, 1) -> + if is_nonzero q then ope("APPLIST", [astxI; pos_of q]) else astxH + | (q, 0) -> ope("APPLIST", [astxO; pos_of q]) + | _ -> anomaly "n mod 2 is neither 1 nor 0. Do you bielive that ?" + in + pos_of x + +let z_of_string pos_or_neg s dloc = + let ((astxI,astxO,astxH),(astZERO,astPOS,astNEG),_) = get_z_sign dloc in + let v = int_array_of_string s in + if is_nonzero v then + if pos_or_neg then + ope("APPLIST",[astPOS; pos_of_int_array astxI astxO astxH v]) + else + ope("APPLIST",[astNEG; pos_of_int_array astxI astxO astxH v]) + else + astZERO + +exception Non_closed_number + +let rec int_array_of_pos c1 c2 c3 p = + match p with + | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c1) -> + mult_2 (int_array_of_pos c1 c2 c3 a) + | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c2) -> + add_1 (mult_2 (int_array_of_pos c1 c2 c3 a)) + | a when alpha_eq(a,c3) -> [| 1 |] + | _ -> raise Non_closed_number + +let int_array_option_of_pos astxI astxO astxH p = + try + Some (int_array_of_pos astxO astxI astxH p) + with Non_closed_number -> + None + +let inside_printer posneg std_pr p = + let ((astxI,astxO,astxH),_,(myvar0,myvar1)) = get_z_sign dummy_loc in + match (int_array_option_of_pos astxI astxO astxH p) with + | Some n -> + if posneg then + [< 'sTR (string_of_int_array n) >] + else + [< 'sTR "(-"; 'sTR (string_of_int_array n); 'sTR ")" >] + | None -> + let c = if posneg then myvar0 else myvar1 in + std_pr (ope("ZEXPR",[ope("APPLIST",[c; p])])) + +let outside_printer posneg std_pr p = + let ((astxI,astxO,astxH),_,(myvar0,myvar1)) = get_z_sign dummy_loc in + match (int_array_option_of_pos astxI astxO astxH p) with + | Some n -> + if posneg then + [< 'sTR "`"; 'sTR (string_of_int_array n); 'sTR "`">] + else + [< 'sTR "`-"; 'sTR (string_of_int_array n); 'sTR "`" >] + | None -> + let c = if posneg then myvar0 else myvar1 in + [< 'sTR "("; std_pr (ope("APPLIST",[c; p])); 'sTR ")" >] + +(* Declare pretty-printers for integers *) +let _ = Esyntax.Ppprim.add ("positive_printer", (outside_printer true)) +let _ = Esyntax.Ppprim.add ("negative_printer", (outside_printer false)) +let _ = Esyntax.Ppprim.add ("positive_printer_inside", (inside_printer true)) +let _ = Esyntax.Ppprim.add ("negative_printer_inside", (inside_printer false)) + +(* Declare the primitive parser *) +open Pcoq + +let number = + match create_entry (get_univ "znatural") "number" ETast with + | Ast n -> n + | _ -> anomaly "G_zsyntax.number" + +let negnumber = + match create_entry (get_univ "znatural") "negnumber" ETast with + | Ast n -> n + | _ -> anomaly "G_zsyntax.negnumber" + +let _ = + Gram.extend number None + [None, None, + [[Gramext.Stoken ("INT", "")], + Gramext.action (z_of_string true)]] + +let _ = + Gram.extend negnumber None + [None, None, + [[Gramext.Stoken ("INT", "")], + Gramext.action (z_of_string false)]] + diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli new file mode 100644 index 0000000000..310d09a12c --- /dev/null +++ b/parsing/g_zsyntax.mli @@ -0,0 +1,4 @@ + +(* $Id$ *) + +(* Nice syntax for integers. *) diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 6a244b9887..bde07410ac 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -17,8 +17,7 @@ let ocamlobjs = ["unix.cma"] let dynobjs = ["dynlink.cma"] let camlp4objs = ["gramlib.cma"] let configobjs = ["coq_config.cmo"] -let launchobjs = ["usage.cmo"] -let libobjs = ocamlobjs @ camlp4objs @ configobjs @ launchobjs +let libobjs = ocamlobjs @ camlp4objs @ configobjs let spaces = Str.regexp "[ \t\n]+" let split_cmo l = Str.split spaces l diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml deleted file mode 100644 index b38fa5756c..0000000000 --- a/toplevel/mltop.ml +++ /dev/null @@ -1,268 +0,0 @@ - -(* $Id$ *) - -open Util -open Pp -open Libobject -open Library -open System -open Vernacinterp - -(* Code to hook Coq into the ML toplevel -- depends on having the - objective-caml compiler mostly visible. The functions implemented here are: - \begin{itemize} - \item [dir_ml_load name]: Loads the ML module fname from the current ML - path. - \item [dir_ml_use]: Directive #use of Ocaml toplevel - \item [dir_ml_dir]: Directive #directory of Ocaml toplevel - \end{itemize} - - How to build an ML module interface with these functions. - The idea is that the ML directory path is like the Coq directory - path. So we can maintain the two in parallel. - In the same way, we can use the "ml_env" as a kind of ML - environment, which we freeze, unfreeze, and add things to just like - to the other environments. - Finally, we can create an object which is an ML module, and require - that the "caching" of the ML module cause the loading of the - associated ML file, if that file has not been yet loaded. Of - course, the problem is how to record dependences between ML - modules. - (I do not know of a solution to this problem, other than to - put all the needed names into the ML Module object.) *) - -(* This path is where we look for .cmo *) -let coq_mlpath_copy = ref [] -let keep_copy_mlpath s = coq_mlpath_copy := (glob s)::!coq_mlpath_copy - -(* If there is a toplevel under Coq *) -type toplevel = { - load_obj : string -> unit; - use_file : string -> unit; - add_dir : string -> unit } - -(* Determines the behaviour of Coq with respect to ML files (compiled - or not) *) -type kind_load = - | WithTop of toplevel - | WithoutTop - | Native - -(* Must be always initialized *) -let load = ref Native - -(* Sets and initializes the kind of loading *) -let set kload = load := kload - -(* Resets load *) -let remove ()= load := Native - -(* Tests if an Ocaml toplevel runs under Coq *) -let is_ocaml_top () = - match !load with - | WithTop _ -> true - |_ -> false - -(* Tests if we can load ML files *) -let enable_load () = - match !load with - | WithTop _ | WithoutTop -> true - |_ -> false - -(* Dynamic loading of .cmo *) -let dir_ml_load s = - match !load with - | WithTop t -> - if is_in_path !coq_mlpath_copy s then - try t.load_obj s - with - | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u - | _ -> errorlabstrm "Mltop.load_object" - [< 'sTR"Cannot link ml-object "; 'sTR s; - 'sTR" to Coq code." >] - else - errorlabstrm "Mltop.load_object" - [< 'sTR"File not found on loadpath : "; 'sTR s >] - | WithoutTop -> - if is_in_path !coq_mlpath_copy s then - let gname = where_in_path !coq_mlpath_copy s in - try - Dynlink.loadfile gname; - Dynlink.add_interfaces - [(String.capitalize (Filename.chop_suffix - (Filename.basename gname) ".cmo"))] - [Filename.dirname gname] - with - | Dynlink.Error(a) -> - errorlabstrm "Mltop.load_object" - [< 'sTR (Dynlink.error_message a) >] - else errorlabstrm "Mltop.load_object" - [< 'sTR"File not found on loadpath : "; 'sTR s >] - | Native -> - errorlabstrm "Mltop.no_load_object" - [< 'sTR"Loading of ML object file forbidden in a native Coq" >] - -(* Dynamic interpretation of .ml *) -let dir_ml_use s = - match !load with - | WithTop t -> t.use_file s - | _ -> warning "Cannot access the ML compiler" - -(* Adds a path to the ML paths *) -let dir_ml_dir s = - match !load with - | WithTop t -> t.add_dir s; keep_copy_mlpath s - | WithoutTop -> keep_copy_mlpath s - | _ -> () - -(* For Rec Add ML Path *) -let rdir_ml_dir dir = List.iter dir_ml_dir (all_subdirs dir) - -(* convertit un nom quelconque en nom de fichier ou de module *) -let mod_of_name name = - let base = - if Filename.check_suffix name ".cmo" then - Filename.chop_suffix name ".cmo" - else - name - in - String.capitalize base - -let file_of_name name = make_suffix (String.uncapitalize name) ".cmo" - -(* TODO: supprimer ce hack, si possible *) -(* Initialisation of ML modules that need the state (ex: tactics like - * natural, omega ...) - * Each module may add some inits (function of type unit -> unit). - * These inits are executed right after the initial state loading if the - * module is statically linked, or after the loading if it is required. *) - -let init_list = ref ([] : (unit -> unit) list) - -let add_init_with_state init_fun = - init_list := init_fun :: !init_list - -let init_with_state () = - List.iter (fun f -> f()) (List.rev !init_list); init_list := [] - - -(* known_loaded_module contains the names of the loaded ML modules - * (linked or loaded with load_object). It is used not to loaded a - * module twice. It is NOT the list of ML modules Coq knows. *) - -type ml_module_object = { mnames : string list } - -let known_loaded_modules = ref Stringset.empty - -let add_known_module mname = - known_loaded_modules := Stringset.add mname !known_loaded_modules - -let module_is_known mname = Stringset.mem mname !known_loaded_modules - -let load_object mname fname= - dir_ml_load fname; - init_with_state(); - add_known_module mname - -(* Summary of declared ML Modules *) - -let loaded_modules = ref Stringset.empty -let get_loaded_modules () = Stringset.elements !loaded_modules -let add_loaded_module md = loaded_modules := Stringset.add md !loaded_modules - -let orig_loaded_modules = ref !loaded_modules -let init_ml_modules () = loaded_modules := !orig_loaded_modules - -let unfreeze_ml_modules x = - List.iter - (fun name -> - let mname = mod_of_name name in - if not (module_is_known mname) then - if enable_load() then - let fname = file_of_name mname in - load_object mname fname - else - errorlabstrm "Mltop.unfreeze_ml_modules" - [< 'sTR"Loading of ML object file forbidden in a native Coq" >]; - add_loaded_module mname) - x - -let _ = - Summary.declare_summary "ML-MODULES" - { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules())); - Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x); - Summary.init_function = (fun () -> init_ml_modules ()) } - -(* Same as restore_ml_modules, but verbosely *) - -let cache_ml_module_object (_,{mnames=mnames}) = - List.iter - (fun name -> - let mname = mod_of_name name in - if not (module_is_known mname) then - let fname= file_of_name mname in - begin try - mSG [< 'sTR"[Loading ML file " ; 'sTR fname ; 'sTR" ..." >]; - load_object mname fname; - mSGNL [< 'sTR"done]" >] - with e -> - begin pPNL [< 'sTR"failed]" >]; raise e end - end; - add_loaded_module mname) - mnames - -let specification_ml_module_object x = x - -let (inMLModule,outMLModule) = - declare_object ("ML-MODULE", - { load_function = cache_ml_module_object; - cache_function = (fun _ -> ()); - open_function = (fun _ -> ()); - specification_function = specification_ml_module_object }) - -let declare_ml_modules l = - let _ = Lib.add_anonymous_leaf (inMLModule {mnames=l}) in () - -let print_ml_path () = - let l = !coq_mlpath_copy in - pPNL [< 'sTR"ML Load Path:"; 'fNL; 'sTR" "; - hV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >] - -let _ = vinterp_add "DeclareMLModule" - (fun l -> - let sl = - List.map - (function - | (VARG_STRING s) -> s - | _ -> anomaly "DeclareMLModule : not a string") l - in - fun () -> declare_ml_modules sl) - -let _ = vinterp_add "AddMLPath" - (function - | [VARG_STRING s] -> - (fun () -> dir_ml_dir (glob s)) - | _ -> anomaly "AddMLPath : not a string") - -let _ = vinterp_add "RecAddMLPath" - (function - | [VARG_STRING s] -> - (fun () -> rdir_ml_dir (glob s)) - | _ -> anomaly "RecAddMLPath : not a string") - -let _ = vinterp_add "PrintMLPath" - (function - | [] -> (fun () -> print_ml_path ()) - | _ -> anomaly "PrintMLPath : does not expect any argument") - - (* Printing of loaded ML modules *) - -let print_ml_modules () = - let l = get_loaded_modules () in - pP [< 'sTR"Loaded ML Modules : " ; - hOV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >] - -let _ = vinterp_add "PrintMLModules" - (function - | [] -> (fun () -> print_ml_modules ()) - | _ -> anomaly "PrintMLModules : does not expect an argument") diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 new file mode 100644 index 0000000000..5329becaea --- /dev/null +++ b/toplevel/mltop.ml4 @@ -0,0 +1,271 @@ + +(* $Id$ *) + +open Util +open Pp +open Libobject +open Library +open System +open Vernacinterp + +(* Code to hook Coq into the ML toplevel -- depends on having the + objective-caml compiler mostly visible. The functions implemented here are: + \begin{itemize} + \item [dir_ml_load name]: Loads the ML module fname from the current ML + path. + \item [dir_ml_use]: Directive #use of Ocaml toplevel + \item [dir_ml_dir]: Directive #directory of Ocaml toplevel + \end{itemize} + + How to build an ML module interface with these functions. + The idea is that the ML directory path is like the Coq directory + path. So we can maintain the two in parallel. + In the same way, we can use the "ml_env" as a kind of ML + environment, which we freeze, unfreeze, and add things to just like + to the other environments. + Finally, we can create an object which is an ML module, and require + that the "caching" of the ML module cause the loading of the + associated ML file, if that file has not been yet loaded. Of + course, the problem is how to record dependences between ML + modules. + (I do not know of a solution to this problem, other than to + put all the needed names into the ML Module object.) *) + +(* This path is where we look for .cmo *) +let coq_mlpath_copy = ref [] +let keep_copy_mlpath s = coq_mlpath_copy := (glob s)::!coq_mlpath_copy + +(* If there is a toplevel under Coq *) +type toplevel = { + load_obj : string -> unit; + use_file : string -> unit; + add_dir : string -> unit } + +(* Determines the behaviour of Coq with respect to ML files (compiled + or not) *) +type kind_load = + | WithTop of toplevel + | WithoutTop + | Native + +(* Must be always initialized *) +let load = ref Native + +(* Sets and initializes the kind of loading *) +let set kload = load := kload + +(* Resets load *) +let remove ()= load := Native + +(* Tests if an Ocaml toplevel runs under Coq *) +let is_ocaml_top () = + match !load with + | WithTop _ -> true + |_ -> false + +(* Tests if we can load ML files *) +let enable_load () = + match !load with + | WithTop _ | WithoutTop -> true + |_ -> false + +(* Dynamic loading of .cmo *) +let dir_ml_load s = + match !load with + | WithTop t -> + if is_in_path !coq_mlpath_copy s then + try t.load_obj s + with + | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u + | _ -> errorlabstrm "Mltop.load_object" + [< 'sTR"Cannot link ml-object "; 'sTR s; + 'sTR" to Coq code." >] + else + errorlabstrm "Mltop.load_object" + [< 'sTR"File not found on loadpath : "; 'sTR s >] + | WithoutTop -> + ifdef Byte then + (if is_in_path !coq_mlpath_copy s then + let gname = where_in_path !coq_mlpath_copy s in + try + Dynlink.loadfile gname; + Dynlink.add_interfaces + [(String.capitalize (Filename.chop_suffix + (Filename.basename gname) ".cmo"))] + [Filename.dirname gname] + with + | Dynlink.Error(a) -> + errorlabstrm "Mltop.load_object" + [< 'sTR (Dynlink.error_message a) >] + else errorlabstrm "Mltop.load_object" + [< 'sTR"File not found on loadpath : "; 'sTR s >]) + else + () + | Native -> + errorlabstrm "Mltop.no_load_object" + [< 'sTR"Loading of ML object file forbidden in a native Coq" >] + +(* Dynamic interpretation of .ml *) +let dir_ml_use s = + match !load with + | WithTop t -> t.use_file s + | _ -> warning "Cannot access the ML compiler" + +(* Adds a path to the ML paths *) +let dir_ml_dir s = + match !load with + | WithTop t -> t.add_dir s; keep_copy_mlpath s + | WithoutTop -> keep_copy_mlpath s + | _ -> () + +(* For Rec Add ML Path *) +let rdir_ml_dir dir = List.iter dir_ml_dir (all_subdirs dir) + +(* convertit un nom quelconque en nom de fichier ou de module *) +let mod_of_name name = + let base = + if Filename.check_suffix name ".cmo" then + Filename.chop_suffix name ".cmo" + else + name + in + String.capitalize base + +let file_of_name name = make_suffix (String.uncapitalize name) ".cmo" + +(* TODO: supprimer ce hack, si possible *) +(* Initialisation of ML modules that need the state (ex: tactics like + * natural, omega ...) + * Each module may add some inits (function of type unit -> unit). + * These inits are executed right after the initial state loading if the + * module is statically linked, or after the loading if it is required. *) + +let init_list = ref ([] : (unit -> unit) list) + +let add_init_with_state init_fun = + init_list := init_fun :: !init_list + +let init_with_state () = + List.iter (fun f -> f()) (List.rev !init_list); init_list := [] + + +(* known_loaded_module contains the names of the loaded ML modules + * (linked or loaded with load_object). It is used not to loaded a + * module twice. It is NOT the list of ML modules Coq knows. *) + +type ml_module_object = { mnames : string list } + +let known_loaded_modules = ref Stringset.empty + +let add_known_module mname = + known_loaded_modules := Stringset.add mname !known_loaded_modules + +let module_is_known mname = Stringset.mem mname !known_loaded_modules + +let load_object mname fname= + dir_ml_load fname; + init_with_state(); + add_known_module mname + +(* Summary of declared ML Modules *) + +let loaded_modules = ref Stringset.empty +let get_loaded_modules () = Stringset.elements !loaded_modules +let add_loaded_module md = loaded_modules := Stringset.add md !loaded_modules + +let orig_loaded_modules = ref !loaded_modules +let init_ml_modules () = loaded_modules := !orig_loaded_modules + +let unfreeze_ml_modules x = + List.iter + (fun name -> + let mname = mod_of_name name in + if not (module_is_known mname) then + if enable_load() then + let fname = file_of_name mname in + load_object mname fname + else + errorlabstrm "Mltop.unfreeze_ml_modules" + [< 'sTR"Loading of ML object file forbidden in a native Coq" >]; + add_loaded_module mname) + x + +let _ = + Summary.declare_summary "ML-MODULES" + { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules())); + Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x); + Summary.init_function = (fun () -> init_ml_modules ()) } + +(* Same as restore_ml_modules, but verbosely *) + +let cache_ml_module_object (_,{mnames=mnames}) = + List.iter + (fun name -> + let mname = mod_of_name name in + if not (module_is_known mname) then + let fname= file_of_name mname in + begin try + mSG [< 'sTR"[Loading ML file " ; 'sTR fname ; 'sTR" ..." >]; + load_object mname fname; + mSGNL [< 'sTR"done]" >] + with e -> + begin pPNL [< 'sTR"failed]" >]; raise e end + end; + add_loaded_module mname) + mnames + +let specification_ml_module_object x = x + +let (inMLModule,outMLModule) = + declare_object ("ML-MODULE", + { load_function = cache_ml_module_object; + cache_function = (fun _ -> ()); + open_function = (fun _ -> ()); + specification_function = specification_ml_module_object }) + +let declare_ml_modules l = + let _ = Lib.add_anonymous_leaf (inMLModule {mnames=l}) in () + +let print_ml_path () = + let l = !coq_mlpath_copy in + pPNL [< 'sTR"ML Load Path:"; 'fNL; 'sTR" "; + hV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >] + +let _ = vinterp_add "DeclareMLModule" + (fun l -> + let sl = + List.map + (function + | (VARG_STRING s) -> s + | _ -> anomaly "DeclareMLModule : not a string") l + in + fun () -> declare_ml_modules sl) + +let _ = vinterp_add "AddMLPath" + (function + | [VARG_STRING s] -> + (fun () -> dir_ml_dir (glob s)) + | _ -> anomaly "AddMLPath : not a string") + +let _ = vinterp_add "RecAddMLPath" + (function + | [VARG_STRING s] -> + (fun () -> rdir_ml_dir (glob s)) + | _ -> anomaly "RecAddMLPath : not a string") + +let _ = vinterp_add "PrintMLPath" + (function + | [] -> (fun () -> print_ml_path ()) + | _ -> anomaly "PrintMLPath : does not expect any argument") + + (* Printing of loaded ML modules *) + +let print_ml_modules () = + let l = get_loaded_modules () in + pP [< 'sTR"Loaded ML Modules : " ; + hOV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >] + +let _ = vinterp_add "PrintMLModules" + (function + | [] -> (fun () -> print_ml_modules ()) + | _ -> anomaly "PrintMLModules : does not expect an argument") -- cgit v1.2.3