From 5b306342bf9befa57abd870527d6bd92b0a5ba50 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 21 Dec 2005 13:49:17 +0000 Subject: [PATCH] Huge reorganization of matita and ocaml. Modified Files in matita: .depend configure.ac matita.ml matitaEngine.ml matitaEngine.mli matitaExcPp.ml matitaGui.ml matitaGui.mli matitaInit.ml matitaInit.mli matitaMathView.ml matitaScript.ml matitaScript.mli matitacLib.ml matitaclean.ml matitadep.ml Modified Files in ocaml: .cvsignore Makefile.in clusters.dot daemons.dot patch_deps.sh METAS/meta.helm-grafite.src METAS/meta.helm-grafite_parser.src cic/cic.ml cic_disambiguation/disambiguate.ml cic_disambiguation/disambiguateTypes.ml cic_disambiguation/disambiguateTypes.mli extlib/hExtlib.ml extlib/hExtlib.mli grafite/.depend grafite/Makefile grafite/grafiteAst.ml grafite/grafiteAstPp.ml grafite/grafiteAstPp.mli grafite/grafiteMarshal.ml grafite2/.depend grafite2/Makefile grafite_parser/.depend grafite_parser/Makefile grafite_parser/cicNotation2.ml grafite_parser/cicNotation2.mli grafite_parser/grafiteDisambiguate.ml grafite_parser/grafiteDisambiguate.mli grafite_parser/grafiteParser.ml grafite_parser/grafiteParser.mli grafite_parser/test_dep.ml grafite_parser/test_parser.ml library/libraryClean.ml library/libraryMisc.ml library/libraryMisc.mli library/libraryNoDb.ml library/libraryNoDb.mli library/librarySync.ml tactics/.depend tactics/equalityTactics.mli tactics/proofEngineHelpers.ml tactics/proofEngineTypes.ml tactics/proofEngineTypes.mli tactics/reductionTactics.mli tactics/tactics.mli Added Files in ocaml: METAS/meta.helm-grafite_engine.src METAS/meta.helm-lexicon.src grafite_engine/.cvsignore grafite_engine/.depend grafite_engine/Makefile grafite_engine/grafiteEngine.ml grafite_engine/grafiteEngine.mli grafite_engine/grafiteMisc.ml grafite_engine/grafiteMisc.mli grafite_engine/grafiteSync.ml grafite_engine/grafiteSync.mli grafite_engine/grafiteTypes.ml grafite_engine/grafiteTypes.mli grafite_parser/dependenciesParser.ml grafite_parser/dependenciesParser.mli grafite_parser/grafiteDisambiguator.ml grafite_parser/grafiteDisambiguator.mli lexicon/.cvsignore lexicon/.depend lexicon/Makefile lexicon/cicNotation.ml lexicon/cicNotation.mli lexicon/disambiguatePp.ml lexicon/disambiguatePp.mli lexicon/lexiconAst.ml lexicon/lexiconAstPp.ml lexicon/lexiconAstPp.mli lexicon/lexiconEngine.ml lexicon/lexiconEngine.mli lexicon/lexiconMarshal.ml lexicon/lexiconMarshal.mli lexicon/lexiconSync.ml lexicon/lexiconSync.mli Removed Files in ocaml: METAS/meta.helm-grafite2.src grafite/cicNotation.ml grafite/cicNotation.mli grafite2/disambiguatePp.ml grafite2/disambiguatePp.mli grafite2/grafiteEngine.ml grafite2/grafiteEngine.mli grafite2/grafiteMisc.ml grafite2/grafiteMisc.mli grafite2/grafiteTypes.ml grafite2/grafiteTypes.mli grafite2/matitaSync.ml grafite2/matitaSync.mli grafite_parser/grafiteParserMisc.ml grafite_parser/grafiteParserMisc.mli grafite_parser/matitaDisambiguator.ml grafite_parser/matitaDisambiguator.mli --- helm/matita/.depend | 4 +- helm/matita/configure.ac | 2 +- helm/matita/matita.ml | 12 +- helm/matita/matitaEngine.ml | 84 ++++++--- helm/matita/matitaEngine.mli | 33 +++- helm/matita/matitaExcPp.ml | 2 +- helm/matita/matitaGui.ml | 45 +++-- helm/matita/matitaGui.mli | 4 +- helm/matita/matitaInit.ml | 17 +- helm/matita/matitaInit.mli | 1 - helm/matita/matitaMathView.ml | 6 +- helm/matita/matitaScript.ml | 318 ++++++++++++++++++---------------- helm/matita/matitaScript.mli | 6 +- helm/matita/matitacLib.ml | 61 ++++--- helm/matita/matitaclean.ml | 2 +- helm/matita/matitadep.ml | 10 +- 16 files changed, 351 insertions(+), 256 deletions(-) diff --git a/helm/matita/.depend b/helm/matita/.depend index afad25274..054bee025 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -45,9 +45,9 @@ matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaMisc.cmi \ - buildTimeConf.cmo matitaScript.cmi + matitaEngine.cmi buildTimeConf.cmo matitaScript.cmi matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \ - buildTimeConf.cmx matitaScript.cmi + matitaEngine.cmx buildTimeConf.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi matitaGtkMisc.cmi: matitaGeneratedGui.cmi diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index 2edd078bb..1075d605d 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -35,7 +35,7 @@ fi FINDLIB_COMREQUIRES="\ helm-cic_disambiguation \ helm-grafite \ -helm-grafite2 \ +helm-grafite_engine \ helm-grafite_parser \ helm-hgdome \ helm-tactics \ diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 0b457dd0c..29df1c3d1 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -73,10 +73,10 @@ let _ = cic_math_view#set_href_callback (Some (fun uri -> (MatitaMathView.cicBrowser ())#load (`Uri (UriManager.uri_of_string uri)))); - let browser_observer _ = MatitaMathView.refresh_all_browsers () in - let sequents_observer status = + let browser_observer _ _ = MatitaMathView.refresh_all_browsers () in + let sequents_observer _ grafite_status = sequents_viewer#reset; - match status.proof_status with + match grafite_status.proof_status with | Incomplete_proof ({ stack = stack } as incomplete_proof) -> sequents_viewer#load_sequents incomplete_proof; (try @@ -137,8 +137,8 @@ let _ = addDebugItem "print top-level grammar entries" CicNotationParser.print_l2_pattern; addDebugItem "dump moo to stderr" (fun _ -> - let status = (MatitaScript.current ())#status in - let moo = status.moo_content_rev in + let grafite_status = (MatitaScript.current ())#grafite_status in + let moo = grafite_status.moo_content_rev in List.iter (fun cmd -> prerr_endline (GrafiteAstPp.pp_command ~obj_pp:(fun _ -> assert false) @@ -150,7 +150,7 @@ let _ = (List.map (fun (g, _, _) -> string_of_int g) (MatitaScript.current ())#proofMetasenv)); prerr_endline ("stack: " ^ Continuationals.Stack.pp - (GrafiteTypes.get_stack (MatitaScript.current ())#status))); + (GrafiteTypes.get_stack (MatitaScript.current ())#grafite_status))); (* addDebugItem "ask record choice" (fun _ -> HLog.debug (string_of_int diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 430151d9a..40a80afdd 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -25,34 +25,70 @@ open Printf -open GrafiteTypes - let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; -let eval_ast ~include_paths ?do_heavy_checks ?clean_baseuri status ast = - GrafiteEngine.eval_ast - ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths) - ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic - ~disambiguate_command:GrafiteDisambiguate.disambiguate_command - ?do_heavy_checks ?clean_baseuri status ast +let disambiguate_command lexicon_status_ref status cmd = + let lexicon_status,metasenv,cmd = + GrafiteDisambiguate.disambiguate_command + ~baseuri:( + try + Some (GrafiteTypes.get_string_option status "baseuri") + with + GrafiteTypes.Option_error _ -> None) + !lexicon_status_ref (GrafiteTypes.get_proof_metasenv status) cmd + in + lexicon_status_ref := lexicon_status; + GrafiteTypes.set_metasenv metasenv status,cmd + +let disambiguate_tactic lexicon_status_ref status goal tac = + let metasenv,tac = + GrafiteDisambiguate.disambiguate_tactic + lexicon_status_ref + (GrafiteTypes.get_proof_context status goal) + (GrafiteTypes.get_proof_metasenv status) + tac + in + GrafiteTypes.set_metasenv metasenv status,tac -let eval_from_stream ?(prompt=false) ?do_heavy_checks ~include_paths - ?clean_baseuri status str cb +let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status + status ast = - while true do - if prompt then (print_string "matita> "; flush stdout); - let ast = GrafiteParser.parse_statement str in - cb !status ast; - status := - eval_ast ~include_paths ?do_heavy_checks ?clean_baseuri !status ast - done -;; + let lexicon_status_ref = ref lexicon_status in + let status,new_objs = + GrafiteEngine.eval_ast + ~disambiguate_tactic:(disambiguate_tactic lexicon_status_ref) + ~disambiguate_command:(disambiguate_command lexicon_status_ref) + ?do_heavy_checks ?clean_baseuri status ast + in + let lexicon_status = + LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs + in + lexicon_status,status -let eval_string ?do_heavy_checks ~include_paths ?clean_baseuri status str = - try - eval_from_stream - ?do_heavy_checks ~include_paths ?clean_baseuri status - (Ulexing.from_utf8_string str) (fun _ _ -> ()) - with End_of_file -> () +let eval_from_stream ~include_paths ?(prompt=false) ?do_heavy_checks + ?clean_baseuri lexicon_status status str cb += + let rec loop lexicon_status status = + if prompt then (print_string "matita> "; flush stdout); + try + let lexicon_status,ast = GrafiteParser.parse_statement ~include_paths str lexicon_status in + (match ast with + GrafiteParser.LNone _ -> loop lexicon_status status + | GrafiteParser.LSome ast -> + cb status ast; + let lexicon_status,status = + eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status status ast + in + loop lexicon_status status) + with + End_of_file -> lexicon_status,status +in + loop lexicon_status status +;; +let eval_string ~include_paths ?do_heavy_checks ?clean_baseuri lexicon_status + status str += + eval_from_stream ~include_paths ?do_heavy_checks ?clean_baseuri lexicon_status + status (Ulexing.from_utf8_string str) (fun _ _ -> ()) diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index ac6d91cb9..02b33c66b 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -23,20 +23,35 @@ * http://helm.cs.unibo.it/ *) +val eval_ast : + ?do_heavy_checks:bool -> + ?clean_baseuri:bool -> + LexiconEngine.status -> + GrafiteTypes.status -> + (CicNotationPt.term, CicNotationPt.term, + CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + GrafiteAst.statement -> LexiconEngine.status * GrafiteTypes.status + (* heavy checks slow down the compilation process but give you some interesting * infos like if the theorem is a duplicate *) -val eval_string: - ?do_heavy_checks:bool -> +val eval_string : include_paths:string list -> + ?do_heavy_checks:bool -> ?clean_baseuri:bool -> - GrafiteTypes.status ref -> string -> unit + LexiconEngine.status -> + GrafiteTypes.status -> + string -> LexiconEngine.status * GrafiteTypes.status -val eval_from_stream: +val eval_from_stream : + include_paths:string list -> ?prompt:bool -> ?do_heavy_checks:bool -> - include_paths:string list -> ?clean_baseuri:bool -> - GrafiteTypes.status ref -> Ulexing.lexbuf -> - (GrafiteTypes.status -> GrafiteParser.statement -> unit) -> - unit - + LexiconEngine.status -> + GrafiteTypes.status -> + Ulexing.lexbuf -> + (GrafiteTypes.status -> + (CicNotationPt.term, CicNotationPt.term, + CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + GrafiteAst.statement -> unit) -> + LexiconEngine.status * GrafiteTypes.status diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index af1aeb882..e9e7f488f 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -63,7 +63,7 @@ let rec to_string = None, "Type checking assertion failed: " ^ Lazy.force msg | LibrarySync.AlreadyDefined s -> None, "Already defined: " ^ UriManager.string_of_uri s - | MatitaDisambiguator.DisambiguationError (offset,errorll) -> + | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> let rec aux n ?(dummy=false) (prev_msg,phases) = function [] -> [prev_msg,phases] diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 16712c454..570769102 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -61,24 +61,26 @@ class console ~(buffer: GText.buffer) () = | `Warning -> self#warning (s ^ "\n") end -let clean_current_baseuri status = +let clean_current_baseuri grafite_status = try - let baseuri = GrafiteTypes.get_string_option status "baseuri" in + let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in let basedir = Helm_registry.get "matita.basedir" in LibraryClean.clean_baseuris ~basedir [baseuri] with GrafiteTypes.Option_error _ -> () -let ask_and_save_moo_if_needed parent fname status = +let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = let basedir = Helm_registry.get "matita.basedir" in - let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths:[] fname in + let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in let save () = let metadata_fname= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in - GrafiteMarshal.save_moo moo_fname status.GrafiteTypes.moo_content_rev; - LibraryNoDb.save_metadata metadata_fname status.GrafiteTypes.metadata + GrafiteMarshal.save_moo moo_fname + grafite_status.GrafiteTypes.moo_content_rev; + LibraryNoDb.save_metadata metadata_fname + lexicon_status.LexiconEngine.metadata in if (MatitaScript.current ())#eos && - status.GrafiteTypes.proof_status = GrafiteTypes.No_proof + grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof then begin let rc = @@ -98,10 +100,10 @@ let ask_and_save_moo_if_needed parent fname status = if b then save () else - clean_current_baseuri status + clean_current_baseuri grafite_status end else - clean_current_baseuri status + clean_current_baseuri grafite_status let ask_unsaved parent = MatitaGtkMisc.ask_confirmation @@ -544,7 +546,7 @@ class gui () = (* toolbar *) let module A = GrafiteAst in let hole = CicNotationPt.UserInput in - let loc = DisambiguateTypes.dummy_floc in + let loc = HExtlib.dummy_floc in let tac ast _ = if (MatitaScript.current ())#onGoingProof () then (MatitaScript.current ())#advance @@ -664,7 +666,8 @@ class gui () = console#message ("'"^f^"' saved.\n"); in let abandon_script () = - let status = (s ())#status in + let lexicon_status = (s ())#lexicon_status in + let grafite_status = (s ())#grafite_status in if source_view#buffer#modified then (match ask_unsaved main#toplevel with | `YES -> saveScript () @@ -672,7 +675,9 @@ class gui () = | `CANCEL -> raise MatitaTypes.Cancel); (match script_fname with | None -> () - | Some fname -> ask_and_save_moo_if_needed main#toplevel fname status); + | Some fname -> + ask_and_save_moo_if_needed main#toplevel fname + lexicon_status grafite_status); in let loadScript () = let script = s () in @@ -720,7 +725,8 @@ class gui () = in (* quit *) self#setQuitCallback (fun () -> - let status = (MatitaScript.current ())#status in + let lexicon_status = (MatitaScript.current ())#lexicon_status in + let grafite_status = (MatitaScript.current ())#grafite_status in if source_view#buffer#modified then begin let rc = ask_unsaved main#toplevel in @@ -732,8 +738,8 @@ class gui () = (match script_fname with | None -> () | Some fname -> - ask_and_save_moo_if_needed - main#toplevel fname status); + ask_and_save_moo_if_needed main#toplevel + fname lexicon_status grafite_status); GMain.Main.quit () end | `NO -> GMain.Main.quit () @@ -743,10 +749,11 @@ class gui () = else begin (match script_fname with - | None -> clean_current_baseuri status; GMain.Main.quit () + | None -> clean_current_baseuri grafite_status; GMain.Main.quit () | Some fname -> try - ask_and_save_moo_if_needed main#toplevel fname status; + ask_and_save_moo_if_needed main#toplevel fname lexicon_status + grafite_status; GMain.Main.quit () with MatitaTypes.Cancel -> ()) end); @@ -1260,8 +1267,8 @@ let interactive_interp_choice () choices = let _ = (* disambiguator callbacks *) - MatitaDisambiguator.set_choose_uris_callback (interactive_uri_choice ()); - MatitaDisambiguator.set_choose_interp_callback (interactive_interp_choice ()); + GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ()); + GrafiteDisambiguator.set_choose_interp_callback (interactive_interp_choice ()); (* gtk initialization *) GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf; diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index b82cb3947..8c9064e1d 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -40,10 +40,10 @@ val interactive_uri_choice: ?hide_uri_entry:bool -> ?hide_try:bool -> ?ok_label:string -> ?ok_action:[`AUTO|`SELECT] -> ?copy_cb:(string -> unit) -> unit -> - MatitaDisambiguator.choose_uris_callback + GrafiteDisambiguator.choose_uris_callback (** @raise MatitaTypes.Cancel *) val interactive_interp_choice: unit -> - MatitaDisambiguator.choose_interp_callback + GrafiteDisambiguator.choose_interp_callback diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml index 44f668183..c47bcb164 100644 --- a/helm/matita/matitaInit.ml +++ b/helm/matita/matitaInit.ml @@ -26,7 +26,7 @@ open Printf type thingsToInitilaize = - ConfigurationFile | Db | Environment | Getter | Notation | Makelib | CmdLine + ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine exception FailedToInitialize of thingsToInitilaize @@ -81,16 +81,6 @@ let initialize_makelib init_status = else init_status -let initialize_notation init_status = - wants [ConfigurationFile] init_status; - if not (already_configured [Notation] init_status) then - begin - CicNotation2.load_notation BuildTimeConf.core_notation_script; - Notation::init_status - end - else - init_status - let initialize_environment init_status = wants [ConfigurationFile] init_status; if not (already_configured [Getter;Environment] init_status) then @@ -215,7 +205,7 @@ let initialize_all () = status := List.fold_left (fun s f -> f s) !status [ parse_cmdline; load_configuration; initialize_makelib; - initialize_db; initialize_environment; initialize_notation ] + initialize_db; initialize_environment ] (* initialize_notation (initialize_environment (initialize_db @@ -226,9 +216,6 @@ let initialize_all () = let load_configuration_file () = status := load_configuration !status -let initialize_notation () = - status := initialize_notation (load_configuration !status) - let parse_cmdline () = status := parse_cmdline !status diff --git a/helm/matita/matitaInit.mli b/helm/matita/matitaInit.mli index e8050f9be..9d8671299 100644 --- a/helm/matita/matitaInit.mli +++ b/helm/matita/matitaInit.mli @@ -29,7 +29,6 @@ val initialize_all: unit -> unit (** {2 per-components initialization} *) val parse_cmdline: unit -> unit (** parse cmdline setting registry keys *) val load_configuration_file: unit -> unit -val initialize_notation: unit -> unit (** {2 Utilities} *) diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 93adb1c90..bf0f7f8bd 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -154,7 +154,7 @@ type selected_term = class clickableMathView obj = let text_width = 80 in -let dummy_loc = DisambiguateTypes.dummy_floc in +let dummy_loc = HExtlib.dummy_floc in object (self) inherit GMathViewAux.multi_selection_math_view obj @@ -244,7 +244,7 @@ object (self) let reduction_action kind () = let pat = self#tactic_text_pattern_of_selection in let statement = - let loc = DisambiguateTypes.dummy_floc in + let loc = HExtlib.dummy_floc in "\n" ^ GrafiteAstPp.pp_executable ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) @@ -906,7 +906,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private home () = self#_showMath; - match self#script#status.proof_status with + match self#script#grafite_status.proof_status with | Proof (uri, metasenv, bo, ty) -> let name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index c8411d5cf..ffa356b53 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -59,7 +59,7 @@ let first_line s = (** creates a statement AST for the Goal tactic, e.g. "goal 7" *) let goal_ast n = let module A = GrafiteAst in - let loc = DisambiguateTypes.dummy_floc in + let loc = HExtlib.dummy_floc in A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n)), Some (A.Dot loc))) @@ -72,7 +72,9 @@ type guistuff = { mutable filenamedata: string option * MatitamakeLib.development option } -let eval_with_engine guistuff status user_goal parsed_text st = +let eval_with_engine guistuff lexicon_status grafite_status user_goal + parsed_text st += let module TAPp = GrafiteAstPp in let include_ = match guistuff.filenamedata with @@ -95,46 +97,38 @@ let eval_with_engine guistuff status user_goal parsed_text st = pieces.(1), pieces.(2) with Not_found -> "", parsed_text in - (* we add the goal command if needed *) - let inital_space,new_status,new_status_and_text_list' = - match status.proof_status with -(* | Incomplete_proof { stack = stack } + let inital_space,new_grafite_status,new_lexicon_status,new_status_and_text_list' = + (* the code commented out adds the "select" command if needed *) + initial_space,grafite_status,lexicon_status,[] in +(* match grafite_status.proof_status with + | Incomplete_proof { stack = stack } when not (List.mem user_goal (Continuationals.head_goals stack)) -> - let status = + let grafite_status = MatitaEngine.eval_ast - ~do_heavy_checks:true status (goal_ast user_goal) + ~do_heavy_checks:true grafite_status (goal_ast user_goal) in let initial_space = if initial_space = "" then "\n" else initial_space in - "\n", status, - [ status, - initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] *) - | _ -> initial_space,status,[] in - let new_status = - GrafiteEngine.eval_ast - ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths:include_) - ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic - ~disambiguate_command:GrafiteDisambiguate.disambiguate_command - ~do_heavy_checks:true new_status st + "\n", grafite_status, + [ grafite_status, + initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] + | _ -> initial_space,grafite_status,[] in *) + let new_lexicon_status,new_grafite_status = + MatitaEngine.eval_ast ~do_heavy_checks:true + new_lexicon_status new_grafite_status st in let new_aliases = - match ex with - | TA.Command (_, TA.Alias _) - | TA.Command (_, TA.Include _) - | TA.Command (_, TA.Interpretation _) -> [] - | _ -> MatitaSync.alias_diff ~from:status new_status - in + LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in (* we remove the defined object since we consider them "automatic aliases" *) let dummy_st = - TA.Comment (DisambiguateTypes.dummy_floc, - TA.Note (DisambiguateTypes.dummy_floc, "")) + TA.Comment (HExtlib.dummy_floc, TA.Note (HExtlib.dummy_floc, "")) in - let initial_space,status,new_status_and_text_list_rev = + let initial_space,lexicon_status,new_status_and_text_list_rev = let module DTE = DisambiguateTypes.Environment in let module UM = UriManager in - let baseuri = GrafiteTypes.get_string_option new_status "baseuri" in + let baseuri = GrafiteTypes.get_string_option new_grafite_status "baseuri" in List.fold_left ( - fun (initial_space,status,acc) (k,((v,_) as value)) -> + fun (initial_space,lexicon_status,acc) (k,((v,_) as value)) -> let b = try UM.buri_of_uri (UM.uri_of_string v) = baseuri @@ -142,7 +136,7 @@ let eval_with_engine guistuff status user_goal parsed_text st = UriManager.IllFormedUri _ -> false (* v is a description, not a URI *) in if b then - initial_space,status,acc + initial_space,lexicon_status,acc else let new_text = let initial_space = @@ -151,23 +145,26 @@ let eval_with_engine guistuff status user_goal parsed_text st = DisambiguatePp.pp_environment (DisambiguateTypes.Environment.add k value DisambiguateTypes.Environment.empty) in - let new_status = - MatitaSync.set_proof_aliases status [k,value] + let new_lexicon_status = + LexiconEngine.set_proof_aliases lexicon_status [k,value] in - "\n",new_status,((new_status, (new_text, dummy_st))::acc) - ) (initial_space,status,[]) new_aliases in + "\n",new_lexicon_status,(((new_grafite_status,new_lexicon_status), (new_text, Some dummy_st))::acc) + ) (initial_space,lexicon_status,[]) new_aliases in let parsed_text = initial_space ^ parsed_text in let res = List.rev new_status_and_text_list_rev @ new_status_and_text_list' @ - [new_status, (parsed_text, st)] + [(new_grafite_status,new_lexicon_status),(parsed_text, Some st)] in res,parsed_text_length -let eval_with_engine guistuff status user_goal parsed_text st = +let eval_with_engine + guistuff lexicon_status grafite_status user_goal parsed_text st += try - eval_with_engine guistuff status user_goal parsed_text st + eval_with_engine guistuff lexicon_status grafite_status user_goal parsed_text + st with - | GrafiteParserMisc.UnableToInclude what + | DependenciesParser.UnableToInclude what | GrafiteEngine.IncludedFileNotCompiled what as exc -> let compile_needed_and_go_on d = let target = what in @@ -177,7 +174,8 @@ let eval_with_engine guistuff status user_goal parsed_text st = if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then raise exc else - eval_with_engine guistuff status user_goal parsed_text st + eval_with_engine guistuff lexicon_status grafite_status user_goal + parsed_text st in let do_nothing () = [], 0 in let handle_with_devel d = @@ -218,14 +216,15 @@ let eval_with_engine guistuff status user_goal parsed_text st = | Some d -> handle_with_devel d ;; -let disambiguate_macro_term term status user_goal = - let module MD = MatitaDisambiguator in +let disambiguate_macro_term term lexicon_status grafite_status user_goal = + let module MD = GrafiteDisambiguator in let dbd = LibraryDb.instance () in - let metasenv = GrafiteTypes.get_proof_metasenv status in - let context = GrafiteTypes.get_proof_context status user_goal in + let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in + let context = GrafiteTypes.get_proof_context grafite_status user_goal in let interps = - MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases - ~universe:(Some status.multi_aliases) term in + MD.disambiguate_term ~dbd ~context ~metasenv + ~aliases:lexicon_status.LexiconEngine.aliases + ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) term in match interps with | [_,_,x,_], _ -> x | _ -> assert false @@ -234,7 +233,7 @@ let pp_eager_statement_ast = GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) -let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = +let eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac = let module TAPp = GrafiteAstPp in let module MQ = MetadataQuery in let module MDB = LibraryDb in @@ -248,7 +247,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = match mac with (* WHELP's stuff *) | TA.WMatch (loc, term) -> - let term = disambiguate_macro_term term status user_goal in + let term = + disambiguate_macro_term term lexicon_status grafite_status user_goal in let l = Whelp.match_term ~dbd term in let query_url = MatitaMisc.strip_suffix ~suffix:"." @@ -258,7 +258,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WInstance (loc, term) -> - let term = disambiguate_macro_term term status user_goal in + let term = + disambiguate_macro_term term lexicon_status grafite_status user_goal in let l = Whelp.instance ~dbd term in let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; @@ -269,7 +270,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WElim (loc, term) -> - let term = disambiguate_macro_term term status user_goal in + let term = + disambiguate_macro_term term lexicon_status grafite_status user_goal in let uri = match term with | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None @@ -280,7 +282,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WHint (loc, term) -> - let term = disambiguate_macro_term term status user_goal in + let term = + disambiguate_macro_term term lexicon_status grafite_status user_goal in let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in let entry = `Whelp (pp_macro (TA.WHint (loc, term)), l) in @@ -288,7 +291,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = [], parsed_text_length (* REAL macro *) | TA.Hint loc -> - let proof = GrafiteTypes.get_current_proof status in + let proof = GrafiteTypes.get_current_proof grafite_status in let proof_status = proof, user_goal in let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in let selected = guistuff.urichooser l in @@ -302,15 +305,12 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = TA.Apply (loc, CicNotationPt.Uri (suri, None))), Some (TA.Dot loc)))) in - let new_status = - GrafiteEngine.eval_ast - ~baseuri_of_script:(fun _ -> assert false) - ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic - ~disambiguate_command:GrafiteDisambiguate.disambiguate_command - status ast in + let new_lexicon_status,new_grafite_status = + MatitaEngine.eval_ast lexicon_status grafite_status ast in let extra_text = comment parsed_text ^ "\n" ^ pp_eager_statement_ast ast in - [ new_status , (extra_text, ast) ], parsed_text_length + [ (new_grafite_status,new_lexicon_status), (extra_text, Some ast) ], + parsed_text_length | _ -> HLog.error "The result of the urichooser should be only 1 uri, not:\n"; @@ -319,12 +319,12 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = ) selected; assert false) | TA.Check (_,term) -> - let metasenv = GrafiteTypes.get_proof_metasenv status in - let context = GrafiteTypes.get_proof_context status user_goal in + let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in + let context = GrafiteTypes.get_proof_context grafite_status user_goal in let interps = - MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv - ~aliases:status.aliases ~universe:(Some status.multi_aliases) term - in + GrafiteDisambiguator.disambiguate_term ~dbd ~context ~metasenv + ~aliases:lexicon_status.LexiconEngine.aliases + ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) term in let _, metasenv , term, ugraph = match interps with | [x], _ -> x @@ -336,7 +336,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = [], parsed_text_length (* | TA.Abort _ -> let rec go_back () = - let status = script#status.proof_status in + let grafite_status = script#grafite_status.proof_status in match status with | No_proof -> () | _ -> script#retract ();go_back() @@ -356,20 +356,23 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = | TA.Search_pat (_, search_kind, str) -> failwith "not implemented" | TA.Search_term (_, search_kind, term) -> failwith "not implemented" -let eval_executable guistuff status user_goal unparsed_text parsed_text script - ex +let eval_executable guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script ex = let module TAPp = GrafiteAstPp in - let module MD = MatitaDisambiguator in + let module MD = GrafiteDisambiguator in let module ML = MatitaMisc in match ex with - | TA.Command (loc, _) | TA.Tactical (loc, _, _) -> - (try - (match GrafiteParserMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with - | None -> () - | Some u -> + TA.Tactical (loc, _, _) -> + eval_with_engine + guistuff lexicon_status grafite_status user_goal parsed_text + (TA.Executable (loc, ex)) + | TA.Command (loc, cmd) -> + (try + begin + match cmd with + | TA.Set (loc',"baseuri",u) -> if not (GrafiteMisc.is_empty u) then - match + (match guistuff.ask_confirmation ~title:"Baseuri redefinition" ~message:( @@ -377,26 +380,33 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script "Do you want to redefine the corresponding "^ "part of the library?") with - | `YES -> - let basedir = Helm_registry.get "matita.basedir" in - LibraryClean.clean_baseuris ~basedir [u] - | `NO -> () - | `CANCEL -> raise MatitaTypes.Cancel); - eval_with_engine - guistuff status user_goal parsed_text (TA.Executable (loc, ex)) - with MatitaTypes.Cancel -> [], 0) + | `YES -> + let basedir = Helm_registry.get "matita.basedir" in + LibraryClean.clean_baseuris ~basedir [u] + | `NO -> () + | `CANCEL -> raise MatitaTypes.Cancel) + | _ -> () + end; + eval_with_engine + guistuff lexicon_status grafite_status user_goal parsed_text + (TA.Executable (loc, ex)) + with MatitaTypes.Cancel -> [], 0) | TA.Macro (_,mac) -> - eval_macro guistuff status user_goal unparsed_text parsed_text script mac + eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text + parsed_text script mac -let rec eval_statement (buffer : GText.buffer) guistuff status user_goal - script statement +let rec eval_statement (buffer : GText.buffer) guistuff lexicon_status + grafite_status user_goal script statement = - let st, unparsed_text = + let (lexicon_status,st), unparsed_text = match statement with | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; - GrafiteParser.parse_statement (Ulexing.from_utf8_string text), text - | `Ast (st, text) -> st, text + GrafiteParser.parse_statement (Ulexing.from_utf8_string text) + ~include_paths:(Helm_registry.get_list + Helm_registry.string "matita.includes") + lexicon_status, text + | `Ast (st, text) -> (lexicon_status, st), text in let text_of_loc loc = let parsed_text_length = snd (HExtlib.loc_of_floc loc) in @@ -404,30 +414,35 @@ let rec eval_statement (buffer : GText.buffer) guistuff status user_goal parsed_text, parsed_text_length in match st with - | GrafiteAst.Comment (loc, _) -> + | GrafiteParser.LNone loc -> + let parsed_text, parsed_text_length = text_of_loc loc in + [(grafite_status,lexicon_status),(parsed_text,None)], + parsed_text_length + | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> let parsed_text, parsed_text_length = text_of_loc loc in let remain_len = String.length unparsed_text - parsed_text_length in let s = String.sub unparsed_text parsed_text_length remain_len in let s,len = try - eval_statement buffer guistuff status user_goal script - (`Raw s) + eval_statement buffer guistuff lexicon_status grafite_status user_goal + script (`Raw s) with HExtlib.Localized (floc, exn) -> HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn - | MatitaDisambiguator.DisambiguationError (offset,errorll) -> + | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> raise - (MatitaDisambiguator.DisambiguationError + (GrafiteDisambiguator.DisambiguationError (offset+parsed_text_length, errorll)) in (match s with - | (status, (text, ast)) :: tl -> - ((status, (parsed_text ^ text, ast))::tl), (parsed_text_length + len) + | (statuses,(text, ast)) :: tl -> + (statuses,(parsed_text ^ text, ast))::tl, + parsed_text_length + len | [] -> [], 0) - | GrafiteAst.Executable (loc, ex) -> + | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> let parsed_text, parsed_text_length = text_of_loc loc in - eval_executable guistuff status user_goal unparsed_text parsed_text - script ex + eval_executable guistuff lexicon_status grafite_status user_goal + unparsed_text parsed_text script ex let fresh_script_id = let i = ref 0 in @@ -442,6 +457,15 @@ class script ~(source_view: GSourceView.source_view) () = let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in +let initial_statuses = + let include_paths = + Helm_registry.get_list Helm_registry.string "matita.includes" in + let lexicon_status = + CicNotation2.load_notation ~include_paths + BuildTimeConf.core_notation_script in + let grafite_status = GrafiteSync.init () in + grafite_status,lexicon_status +in object (self) val scriptId = fresh_script_id () @@ -468,8 +492,9 @@ object (self) ignore (buffer#connect#modified_changed (fun _ -> set_star (Filename.basename self#ppFilename) buffer#modified)) - val mutable statements = []; (** executed statements *) - val mutable history = [ MatitaSync.init () ]; + val mutable statements = [] (** executed statements *) + + val mutable history = [ initial_statuses ] (** list of states before having executed statements. Head element of this * list is the current state, last element is the state at the beginning of * the script. @@ -489,13 +514,15 @@ object (self) method error_tag = error_tag (* history can't be empty, the invariant above grant that it contains at - * least the init status *) - method status = match history with hd :: _ -> hd | _ -> assert false + * least the init grafite_status *) + method grafite_status = match history with (s,_)::_ -> s | _ -> assert false + method lexicon_status = match history with (_,ss)::_ -> ss | _ -> assert false method private _advance ?statement () = let rec aux st = let (entries, parsed_len) = - eval_statement buffer guistuff self#status userGoal self st + eval_statement buffer guistuff self#lexicon_status self#grafite_status + userGoal self st in let (new_statuses, new_statements, new_asts) = let statuses, statements = List.split entries in @@ -515,32 +542,20 @@ object (self) buffer#insert ~iter:start new_text; end; end; - self#moveMark (String.length new_text); - (* - (match List.rev new_asts with (* advance again on punctuation *) - | TA.Executable (_, TA.Tactical (_, tac, _)) :: _ -> - let baseoffset = - (buffer#get_iter_at_mark (`MARK locked_mark))#offset - in - let text = self#getFuture in - (try - (match parse_statement baseoffset 0 buffer text with - | TA.Executable (loc, TA.Tactical (_, tac, None)) as st - when GrafiteAst.is_punctuation tac -> - let len = snd (CicNotationPt.loc_of_floc loc) in - aux (`Ast (st, String.sub text 0 len)) - | _ -> ()) - with CicNotationParser.Parse_error _ | End_of_file -> ()) - | _ -> ()) - *) + self#moveMark (String.length new_text) in let s = match statement with Some s -> s | None -> self#getFuture in HLog.debug ("evaluating: " ^ first_line s ^ " ..."); (try aux (`Raw s) with End_of_file -> raise Margin) - method private _retract offset status new_statements new_history = - let cur_status = match history with s::_ -> s | [] -> assert false in - MatitaSync.time_travel ~present:cur_status ~past:status; + method private _retract offset lexicon_status grafite_status new_statements + new_history + = + let cur_grafite_status,cur_lexicon_status = + match history with s::_ -> s | [] -> assert false + in + LexiconSync.time_travel ~present:cur_lexicon_status ~past:lexicon_status; + GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status; statements <- new_statements; history <- new_history; self#moveMark (- offset) @@ -555,14 +570,15 @@ object (self) method retract () = try - let cmp,new_statements,new_history,status = + let cmp,new_statements,new_history,(grafite_status,lexicon_status) = match statements,history with stat::statements, _::(status::_ as history) -> String.length stat, statements, history, status | [],[_] -> raise Margin | _,_ -> assert false in - self#_retract cmp status new_statements new_history; + self#_retract cmp lexicon_status grafite_status new_statements + new_history; self#notify with | Margin -> self#notify @@ -603,12 +619,13 @@ object (self) val mutable observers = [] - method addObserver (o: GrafiteTypes.status -> unit) = + method addObserver (o: LexiconEngine.status -> GrafiteTypes.status -> unit) = observers <- o :: observers method private notify = - let status = self#status in - List.iter (fun o -> o status) observers + let lexicon_status = self#lexicon_status in + let grafite_status = self#grafite_status in + List.iter (fun o -> o lexicon_status grafite_status) observers method loadFromFile f = buffer#set_text (HExtlib.input_file f); @@ -639,20 +656,21 @@ object (self) end method private goto_top = - let init = + let grafite_status,lexicon_status = let rec last x = function | [] -> x | hd::tl -> last hd tl in - last self#status history + last (self#grafite_status,self#lexicon_status) history in (* FIXME: this is not correct since there is no undo for * library_objects.set_default... *) - MatitaSync.time_travel ~present:self#status ~past:init + GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status; + LexiconSync.time_travel ~present:self#lexicon_status ~past:lexicon_status method private reset_buffer = statements <- []; - history <- [ MatitaSync.init () ]; + history <- [ initial_statuses ]; userGoal <- ~-1; self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; @@ -730,8 +748,10 @@ object (self) in let rec back_until_cursor len = (* go backward until locked < cursor *) function - statements, (status::_ as history) when len <= 0 -> - self#_retract (icmp - len) status statements history + statements, ((grafite_status,lexicon_status)::_ as history) + when len <= 0 -> + self#_retract (icmp - len) lexicon_status grafite_status statements + history | statement::tl1, _::tl2 -> back_until_cursor (len - String.length statement) (tl1,tl2) | _,_ -> assert false @@ -753,34 +773,42 @@ object (self) self#notify; raise exc) method onGoingProof () = - match self#status.proof_status with + match self#grafite_status.proof_status with | No_proof | Proof _ -> false | Incomplete_proof _ -> true | Intermediate _ -> assert false (* method proofStatus = MatitaTypes.get_proof_status self#status *) - method proofMetasenv = GrafiteTypes.get_proof_metasenv self#status - method proofContext = GrafiteTypes.get_proof_context self#status userGoal - method proofConclusion= GrafiteTypes.get_proof_conclusion self#status userGoal - method stack = GrafiteTypes.get_stack self#status + method proofMetasenv = GrafiteTypes.get_proof_metasenv self#grafite_status + method proofContext = + GrafiteTypes.get_proof_context self#grafite_status userGoal + method proofConclusion = + GrafiteTypes.get_proof_conclusion self#grafite_status userGoal + method stack = GrafiteTypes.get_stack self#grafite_status method setGoal n = userGoal <- n method goal = userGoal method eos = let s = self#getFuture in - let rec is_there_and_executable s = + let rec is_there_and_executable lexicon_status s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; - let st = GrafiteParser.parse_statement (Ulexing.from_utf8_string s) in + let lexicon_status,st = + GrafiteParser.parse_statement (Ulexing.from_utf8_string s) + ~include_paths:(Helm_registry.get_list + Helm_registry.string "matita.includes") + lexicon_status + in match st with - | GrafiteAst.Comment (loc,_)-> + GrafiteParser.LNone loc + | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> let parsed_text_length = snd (HExtlib.loc_of_floc loc) in let remain_len = String.length s - parsed_text_length in let next = String.sub s parsed_text_length remain_len in - is_there_and_executable next - | GrafiteAst.Executable (loc, ex) -> false + is_there_and_executable lexicon_status next + | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> false in try - is_there_and_executable s + is_there_and_executable self#lexicon_status s with | CicNotationParser.Parse_error _ -> false | Margin | End_of_file -> true diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index 2b36a5d3d..c9e60943b 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -31,11 +31,13 @@ object method error_tag : GText.tag (** @return current status *) - method status: GrafiteTypes.status + method lexicon_status: LexiconEngine.status + method grafite_status: GrafiteTypes.status (** {2 Observers} *) - method addObserver : (GrafiteTypes.status -> unit) -> unit + method addObserver : + (LexiconEngine.status -> GrafiteTypes.status -> unit) -> unit (** {2 History} *) diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 07d58b395..73a4d668f 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -33,21 +33,22 @@ let pp_ast_statement = (** {2 Initialization} *) -let status = ref None +let grafite_status = (ref None : GrafiteTypes.status option ref) +let lexicon_status = (ref None : LexiconEngine.status option ref) let run_script is eval_function = - let status = - match !status with - | None -> assert false - | Some s -> s + let lexicon_status',grafite_status' = + match !lexicon_status,!grafite_status with + | Some ss, Some s -> ss,s + | _,_ -> assert false in let slash_n_RE = Pcre.regexp "\\n" in let cb = if Helm_registry.get_bool "matita.quiet" then (fun _ _ -> ()) else - (fun status stm -> - (* dump_status status; *) + (fun grafite_status stm -> + (* dump_status grafite_status; *) let stm = pp_ast_statement stm in let stm = Pcre.replace ~rex:slash_n_RE stm in let stm = @@ -59,7 +60,11 @@ let run_script is eval_function = HLog.debug ("Executing: ``" ^ stm ^ "''")) in try - eval_function status is cb + let lexicon_status'', grafite_status'' = + eval_function lexicon_status' grafite_status' is cb + in + lexicon_status := Some lexicon_status''; + grafite_status := Some grafite_status'' with | GrafiteEngine.Drop | End_of_file @@ -86,11 +91,11 @@ let clean_exit n = None -> () | Some n -> exit n in - match !status with + match !grafite_status with None -> opt_exit n - | Some status -> + | Some grafite_status -> try - let baseuri = GrafiteTypes.get_string_option !status "baseuri" in + let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in let basedir = Helm_registry.get "matita.basedir" in LibraryClean.clean_baseuris ~basedir ~verbose:false [baseuri]; opt_exit n @@ -120,14 +125,18 @@ let rec interactive_loop () = let go () = Helm_registry.load_from BuildTimeConf.matita_conf; - CicNotation2.load_notation BuildTimeConf.core_notation_script; Http_getter.init (); MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); LibraryDb.create_owner_environment (); CicEnvironment.set_trust (* environment trust *) (let trust = Helm_registry.get_bool "matita.environment_trust" in fun _ -> trust); - status := Some (ref (MatitaSync.init ())); + let include_paths = + Helm_registry.get_list Helm_registry.string "matita.includes" in + grafite_status := Some (GrafiteSync.init ()); + lexicon_status := + Some (CicNotation2.load_notation ~include_paths + BuildTimeConf.core_notation_script); Sys.catch_break true; interactive_loop () @@ -135,7 +144,12 @@ let main ~mode = MatitaInit.initialize_all (); (* must be called after init since args are set by cmdline parsing *) let fname = fname () in - status := Some (ref (MatitaSync.init ())); + let include_paths = + Helm_registry.get_list Helm_registry.string "matita.includes" in + grafite_status := Some (GrafiteSync.init ()); + lexicon_status := + Some (CicNotation2.load_notation ~include_paths + BuildTimeConf.core_notation_script); Sys.catch_break true; let origcb = HLog.get_log_callback () in let newcb tag s = @@ -175,10 +189,12 @@ let main ~mode = let hou = if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" in - let proof_status,moo_content_rev,metadata,status = - match !status with - | Some s -> !s.proof_status, !s.moo_content_rev, !s.metadata, !s - | None -> assert false + let proof_status,moo_content_rev,metadata,lexicon_content_rev = + match !lexicon_status,!grafite_status with + | Some ss, Some s -> + s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata, + ss.LexiconEngine.lexicon_content_rev + | _,_ -> assert false in if proof_status <> GrafiteTypes.No_proof then begin @@ -189,11 +205,16 @@ let main ~mode = else begin let basedir = Helm_registry.get "matita.basedir" in - let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths fname in + let baseuri = + DependenciesParser.baseuri_of_script ~include_paths fname in let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in - let metadata_fname = LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in + let lexicon_fname= LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri in + let metadata_fname = + LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri + in GrafiteMarshal.save_moo moo_fname moo_content_rev; LibraryNoDb.save_metadata metadata_fname metadata; + LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); exit 0 diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index a5669d2e6..912d32cd0 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -54,7 +54,7 @@ let main () = UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> let u = - GrafiteParserMisc.baseuri_of_script ~include_paths:[] suri in + DependenciesParser.baseuri_of_script ~include_paths:[] suri in if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin HLog.error (sprintf "File %s defines a bad baseuri: %s" suri u); diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index e93dbad61..0052199ec 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -44,20 +44,20 @@ let main () = (fun ma_file -> let ic = open_in ma_file in let istream = Ulexing.from_utf8_channel ic in - let dependencies = GrafiteParser.parse_dependencies istream in + let dependencies = DependenciesParser.parse_dependencies istream in close_in ic; List.iter (function - | GrafiteAst.UriDep uri -> + | DependenciesParser.UriDep uri -> let uri = UriManager.string_of_uri uri in Hashtbl.add uri_deps ma_file uri - | GrafiteAst.BaseuriDep uri -> + | DependenciesParser.BaseuriDep uri -> let uri = Http_getter_misc.strip_trailing_slash uri in Hashtbl.add baseuri_of ma_file uri - | GrafiteAst.IncludeDep path -> + | DependenciesParser.IncludeDep path -> try let baseuri = - GrafiteParserMisc.baseuri_of_script ~include_paths path in + DependenciesParser.baseuri_of_script ~include_paths path in let moo_file = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in Hashtbl.add include_deps ma_file moo_file with Sys_error _ -> -- 2.39.2