From 94c9255e1f3095440f4d49ea1d75443a5a343185 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 28 Jun 2005 15:50:22 +0000 Subject: [PATCH] * new binary matitatop * command drop enabled for matitatop. Once dropped use MatitacLib.go () to enter again the matita toplevel. Use #trace and similar stuff for debugging. Add printers for abstract data types in matitatop.bootstrap Enjoy! --- helm/matita/.depend | 22 ++--- helm/matita/Makefile.in | 8 +- helm/matita/matitaEngine.ml | 18 +++- helm/matita/matitaEngine.mli | 14 ++- helm/matita/matitaMathView.ml | 12 +-- helm/matita/matitaMisc.ml | 4 +- helm/matita/matitac.ml | 125 +------------------------- helm/matita/matitacLib.ml | 151 ++++++++++++++++++++++++++++++++ helm/matita/matitacLib.mli | 2 + helm/matita/matitatop.bootstrap | 16 ++++ helm/matita/matitatop.ml | 5 ++ 11 files changed, 225 insertions(+), 152 deletions(-) create mode 100644 helm/matita/matitacLib.ml create mode 100644 helm/matita/matitacLib.mli create mode 100644 helm/matita/matitatop.bootstrap create mode 100644 helm/matita/matitatop.ml diff --git a/helm/matita/.depend b/helm/matita/.depend index 95217b4b6..c20c1a38f 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,7 +1,9 @@ -matitac.cmo: matitaTypes.cmo matitaLog.cmi matitaEngine.cmi matitaDb.cmi \ - buildTimeConf.cmo -matitac.cmx: matitaTypes.cmx matitaLog.cmx matitaEngine.cmx matitaDb.cmx \ - buildTimeConf.cmx +matita.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \ + matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ + matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo +matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ + matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ + matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx matitaDb.cmo: matitaDb.cmi matitaDb.cmx: matitaDb.cmi matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi @@ -26,12 +28,6 @@ matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx matitaMathView.cmi matitaMisc.cmo: matitaTypes.cmo buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi -matita.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \ - matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo -matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx matitaScript.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi matitaScript.cmi matitaScript.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \ @@ -42,6 +38,12 @@ matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ matitaSync.cmi matitaTypes.cmo: matitaLog.cmi matitaTypes.cmx: matitaLog.cmx +matitac.cmo: matitacLib.cmi +matitac.cmx: matitacLib.cmx +matitacLib.cmo: matitaTypes.cmo matitaLog.cmi matitaEngine.cmi matitaDb.cmi \ + buildTimeConf.cmo matitacLib.cmi +matitacLib.cmx: matitaTypes.cmx matitaLog.cmx matitaEngine.cmx matitaDb.cmx \ + buildTimeConf.cmx matitacLib.cmi matitaDisambiguator.cmi: matitaTypes.cmo matitaEngine.cmi: matitaTypes.cmo matitaGtkMisc.cmi: matitaGeneratedGui.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 0751f845b..43a62c6f5 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -40,10 +40,11 @@ CCMOS = \ matitaDb.cmo \ matitaSync.cmo \ matitaDisambiguator.cmo \ - matitaEngine.cmo + matitaEngine.cmo \ + matitacLib.cmo -all: matita matitac cicbrowser +all: matita matitac matitatop cicbrowser updater: $(LIB_DEPS) $(OCAMLC) $(PKGS) -linkpkg -o $@ updater.ml @@ -69,6 +70,9 @@ matitac: $(LIB_DEPS) $(CCMOS) matitac.ml matitac.opt: $(LIBX_DEPS) $(CCMXS) matitac.ml $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml +matitatop: matitatop.ml $(LIB_DEPS) $(CCMOS) + $(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $< + cicbrowser: matita @test -f $@ || ln -s $< $@ cicbrowser.opt: matita.opt diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 02f13739d..95de73528 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -2,6 +2,8 @@ open Printf open MatitaTypes +exception Drop;; + let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; @@ -223,6 +225,7 @@ let generate_projections uri fields status = let eval_command status cmd = match cmd with | TacticAst.Set (loc, name, value) -> set_option status name value + | TacticAst.Drop loc -> raise Drop | TacticAst.Qed loc -> let uri, metasenv, bo, ty = match status.proof_status with @@ -525,7 +528,7 @@ let disambiguate_command status = function | TacticAst.Coercion (loc, term) -> let status, term = disambiguate_term status term in status, TacticAst.Coercion (loc,term) - | (TacticAst.Set _ | TacticAst.Qed _) as cmd -> + | (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd -> status, cmd | TacticAst.Alias _ as x -> status, x | TacticAst.Obj (loc,obj) -> @@ -567,9 +570,16 @@ let eval_ast status ast = let eval_from_stream status str cb = let stl = CicTextualParser2.parse_statements str in - List.fold_left - (fun status ast -> cb status ast;eval_ast status ast) status - stl + List.iter (fun ast -> cb !status ast;status := eval_ast !status ast) stl + +let eval_from_stream_greedy status str cb = + while true do + print_string "matita> "; + flush stdout; + let ast = CicTextualParser2.parse_statement str in + cb !status ast; + status := eval_ast !status ast + done let eval_string status str = eval_from_stream status (Stream.of_string str) (fun _ _ -> ()) diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index f0730bcca..249bad8f4 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -23,15 +23,21 @@ * http://helm.cs.unibo.it/ *) -(*val eval_ast:*) +exception Drop -val eval_string: MatitaTypes.status -> string -> MatitaTypes.status +val eval_string: MatitaTypes.status ref -> string -> unit val eval_from_stream: - MatitaTypes.status -> char Stream.t -> + MatitaTypes.status ref -> char Stream.t -> (MatitaTypes.status -> (CicAst.term,TacticAst.obj,string) TacticAst.statement -> unit) -> - MatitaTypes.status + unit + +val eval_from_stream_greedy: + MatitaTypes.status ref-> char Stream.t -> + (MatitaTypes.status -> + (CicAst.term,TacticAst.obj,string) TacticAst.statement -> unit) -> + unit val eval_ast: MatitaTypes.status -> diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 7b25b375c..4d0eace3a 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -81,19 +81,19 @@ class clickableMathView obj = ignore (self#connect#click (fun (gdome_elt, _, _, _) -> match gdome_elt with | Some elt (* element is an hyperlink, use href_callback on it *) - when elt#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href -> + when elt#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href -> (match href_callback with | None -> () | Some f -> let uri = - elt#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href + elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href in f (uri#to_string)) | Some elt -> ignore (self#action_toggle elt) | None -> ())) method private choose_selection gdome_elt = let rec aux elt = - if elt#hasAttributeNS ~namespaceURI:Misc.helm_ns ~localName:xref then + if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref then self#set_selection (Some elt) else try @@ -133,7 +133,7 @@ class sequentViewer obj = (fun node -> let xpath = ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helm_ns + ~namespaceURI:DomMisc.helm_ns ~localName:(Gdome.domString "xref"))#to_string in if xpath = "" then assert false (* "ERROR: No xref found!!!" *) @@ -150,7 +150,7 @@ class sequentViewer obj = (fun node -> let xpath = ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helm_ns + ~namespaceURI:DomMisc.helm_ns ~localName:(Gdome.domString "xref"))#to_string in if xpath = "" then assert false (* "ERROR: No xref found!!!" *) @@ -169,7 +169,7 @@ class sequentViewer obj = current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); (* debug_print "load_sequent: dumping MathML to ./prova"; - ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ()); + ignore (DomMisc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ()); *) self#load_root ~root:mathml#get_documentElement end diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index a35a57ed6..73fdd4c54 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -58,11 +58,11 @@ let strip_trailing_blanks = fun s -> Pcre.replace ~rex s let empty_mathml () = - Misc.domImpl#createDocument ~namespaceURI:(Some Misc.mathml_ns) + DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns) ~qualifiedName:(Gdome.domString "math") ~doctype:None let empty_boxml () = - Misc.domImpl#createDocument ~namespaceURI:(Some Misc.boxml_ns) + DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) ~qualifiedName:(Gdome.domString "box") ~doctype:None exception History_failure diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml index e7cdef9f4..52407af54 100644 --- a/helm/matita/matitac.ml +++ b/helm/matita/matitac.ml @@ -1,125 +1,2 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -open Printf - -open MatitaTypes - -(** {2 Initialization} *) - -let arg_spec = [ -(* "-opt", Arg...., "set bla bla bla"; *) -] -let usage = - sprintf "MatitaC v%s\nUsage: matitac [option ...] file ...\nOptions:" - BuildTimeConf.version - let _ = - Helm_registry.load_from "matita.conf.xml"; - Http_getter.init (); - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.clean_owner_environment (); - MatitaDb.create_owner_environment () - -let scripts = - let acc = ref [] in - let add_script fname = acc := fname :: !acc in - Arg.parse arg_spec add_script usage; - List.rev !acc - -let run_script fname = - let is = - Stream.of_channel - (match fname with - | "stdin" -> stdin - | fname -> open_in fname) - in - let status = ref (Lazy.force MatitaEngine.initial_status) in - let slash_n_RE = Pcre.regexp "\\n" in - let cb status stm = - (* dump_status status; *) - let stm = TacticAstPp.pp_statement stm in - let stm = Pcre.replace ~rex:slash_n_RE stm in - let stm = - if String.length stm > 50 then - String.sub stm 0 50 ^ " ..." - else - stm - in - MatitaLog.debug ("Executing: ``" ^ stm ^ "''") - in - try - status := MatitaEngine.eval_from_stream !status is cb ; - !status - with - | CicTextualParser2.Parse_error (floc,err) -> - let (x, y) = CicAst.loc_of_floc floc in - MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); - Http_getter.sync_dump_file (); - exit 1 - | exn -> - MatitaLog.error (Printexc.to_string exn); - raise exn - -let _ = - at_exit - (fun () -> - Http_getter_logger.log "Sync map tree to disk..."; - Http_getter.sync_dump_file (); - print_endline "\nThanks for using Matita!\n"); - Sys.catch_break true; - try - List.iter (fun fname -> - let time = Unix.time () in - MatitaLog.message (sprintf "execution of %s started:" fname); - let status = run_script fname in - let elapsed = Unix.time () -. time in - let tm = Unix.gmtime elapsed in - let sec = - if tm.Unix.tm_sec > 0 then (string_of_int tm.Unix.tm_sec ^ "''") else "" - in - let min = - if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min ^ "' ") else "" - in - let hou = - if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" - in - let proof_status = status.proof_status in - if proof_status <> MatitaTypes.No_proof then - begin - MatitaLog.error - "there are still incomplete proofs at the end of the script"; - exit(-1) - end - else - begin - MatitaLog.message - (sprintf "execution of %s completed in %s." fname (hou^min^sec)) ; - exit(0) - end - ) scripts - with Sys.Break -> - MatitaLog.error "user break!"; - exit (-1) + MatitacLib.main `COMPILER diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml new file mode 100644 index 000000000..1f0aea715 --- /dev/null +++ b/helm/matita/matitacLib.ml @@ -0,0 +1,151 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +open MatitaTypes + +(** {2 Initialization} *) + +let arg_spec = [ +(* "-opt", Arg...., "set bla bla bla"; *) +] +let usage = + sprintf "MatitaC v%s\nUsage: matitac [option ...] file\nOptions:" + BuildTimeConf.version + +let _ = + Helm_registry.load_from "matita.conf.xml"; + Http_getter.init (); + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); + MatitaDb.clean_owner_environment (); + MatitaDb.create_owner_environment () + +let status = ref (Lazy.force MatitaEngine.initial_status) ;; + +let run_script is eval_function = + let slash_n_RE = Pcre.regexp "\\n" in + let cb status stm = + (* dump_status status; *) + let stm = TacticAstPp.pp_statement stm in + let stm = Pcre.replace ~rex:slash_n_RE stm in + let stm = + if String.length stm > 50 then + String.sub stm 0 50 ^ " ..." + else + stm + in + MatitaLog.debug ("Executing: ``" ^ stm ^ "''") + in + try + eval_function status is cb + with + | MatitaEngine.Drop + | CicTextualParser2.Parse_error _ as exn -> raise exn + | exn -> + MatitaLog.error (Printexc.to_string exn); + raise exn + +let fname () = + let acc = ref [] in + let add_script fname = acc := fname :: !acc in + Arg.parse arg_spec add_script usage; + match !acc with + | [x] -> x + | _ -> prerr_endline usage; exit 1 + +let pp_ocaml_mode () = + MatitaLog.message ""; + MatitaLog.message " ** Entering Ocaml mode ** "; + MatitaLog.message "" + +let rec go () = + try + run_script (Stream.of_channel stdin) MatitaEngine.eval_from_stream_greedy + with + | MatitaEngine.Drop -> pp_ocaml_mode () + | Sys.Break -> MatitaLog.error "user break!"; go () + | MatitaTypes.Command_error _ -> go () + | CicTextualParser2.Parse_error (floc,err) -> + let (x, y) = CicAst.loc_of_floc floc in + MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); + go () + | exn -> MatitaLog.error (Printexc.to_string exn); go () + +let main ~mode = + at_exit + (fun () -> + Http_getter_logger.log "Sync map tree to disk..."; + Http_getter.sync_dump_file (); + print_endline "\nThanks for using Matita!\n"); + Sys.catch_break true; + let fname = fname () in + try + let time = Unix.time () in + MatitaLog.message (sprintf "execution of %s started:" fname); + let is = + Stream.of_channel + (match fname with + | "stdin" -> stdin + | fname -> open_in fname) + in + run_script is MatitaEngine.eval_from_stream; + let elapsed = Unix.time () -. time in + let tm = Unix.gmtime elapsed in + let sec = + if tm.Unix.tm_sec > 0 then (string_of_int tm.Unix.tm_sec ^ "''") else "" + in + let min = + if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min ^ "' ") else "" + in + let hou = + if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" + in + let proof_status = !status.proof_status in + if proof_status <> MatitaTypes.No_proof then + begin + MatitaLog.error + "there are still incomplete proofs at the end of the script"; + exit 2 + end + else + begin + MatitaLog.message + (sprintf "execution of %s completed in %s." fname (hou^min^sec)); + exit 0 + end + with + | Sys.Break -> MatitaLog.error "user break!"; exit ~-1 + | MatitaEngine.Drop -> + if mode = `COMPILER then + exit 1 + else + pp_ocaml_mode () + | CicTextualParser2.Parse_error (floc,err) -> + let (x, y) = CicAst.loc_of_floc floc in + MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); + Http_getter.sync_dump_file (); + exit 1 + diff --git a/helm/matita/matitacLib.mli b/helm/matita/matitacLib.mli new file mode 100644 index 000000000..aad2b29ac --- /dev/null +++ b/helm/matita/matitacLib.mli @@ -0,0 +1,2 @@ +val go : unit -> unit +val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit diff --git a/helm/matita/matitatop.bootstrap b/helm/matita/matitatop.bootstrap new file mode 100644 index 000000000..5d6da169e --- /dev/null +++ b/helm/matita/matitatop.bootstrap @@ -0,0 +1,16 @@ +#directory "../ocaml/cic_unification/" +#directory "../ocaml/cic_proof_checking/" + +#install_printer CicMetaSubst.fppsubst;; +(*#install_printer CicMetaSubst.fppterm;;*) +#install_printer CicMetaSubst.fppmetasenv;; + +let go = MatitacLib.go;; + +let _ = + if Array.length Sys.argv > 1 then + MatitacLib.main `TOPLEVEL + else + go () +;; + diff --git a/helm/matita/matitatop.ml b/helm/matita/matitatop.ml new file mode 100644 index 000000000..95a8ec192 --- /dev/null +++ b/helm/matita/matitatop.ml @@ -0,0 +1,5 @@ +let _ = + let _ = Topdirs.dir_quit in + Toploop.initialize_toplevel_env (); + Topdirs.dir_use Format.std_formatter "matitatop.bootstrap"; + Toploop.loop Format.std_formatter -- 2.39.2