From efec9dde0ebb9ea6b8d8556b92bc0173dcab2cb7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Jan 2006 15:46:34 +0000 Subject: [PATCH] fixed coercions undoooing --- helm/matita/matitaGui.ml | 4 +- helm/matita/matitaScript.ml | 44 +++++++++++++--------- helm/matita/matitaScript.mli | 1 + helm/ocaml/grafite_engine/grafiteEngine.ml | 15 +++----- helm/ocaml/lexicon/lexiconEngine.mli | 1 + helm/ocaml/library/librarySync.ml | 9 ++++- helm/ocaml/tactics/paramodulation/Makefile | 4 +- 7 files changed, 47 insertions(+), 31 deletions(-) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 03e50588f..ed739eefb 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -607,7 +607,9 @@ class gui () = (* log *) HLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := - (fun exn -> + (function + | MatitaScript.ActionCancelled -> () + | exn -> if not (Helm_registry.get_bool "matita.debug") then let floc, msg = MatitaExcPp.to_string exn in begin diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 4c53f113b..4b1b994d9 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -36,6 +36,7 @@ let debug_print = if debug then prerr_endline else ignore (** raised when one of the script margins (top or bottom) is reached *) exception Margin exception NoUnfinishedProof +exception ActionCancelled let safe_substring s i j = try String.sub s i j with Invalid_argument _ -> assert false @@ -140,27 +141,24 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal in res,parsed_text_length -let eval_with_engine - guistuff lexicon_status grafite_status user_goal parsed_text st -= - try - eval_with_engine guistuff lexicon_status grafite_status user_goal parsed_text - st +let wrap_with_developments guistuff f arg = + try + f arg with | DependenciesParser.UnableToInclude what + | LexiconEngine.IncludedFileNotCompiled what | GrafiteEngine.IncludedFileNotCompiled what as exc -> let compile_needed_and_go_on d = - let target = what in + let target = Pcre.replace ~pat:"lexicon$" ~templ:"moo" what in let refresh_cb () = while Glib.Main.pending () do ignore(Glib.Main.iteration false); done in if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then raise exc else - eval_with_engine guistuff lexicon_status grafite_status user_goal - parsed_text st + f arg in - let do_nothing () = [], 0 in + let do_nothing () = raise ActionCancelled in let handle_with_devel d = let name = MatitamakeLib.name_for_development d in let title = "Unable to include " ^ what in @@ -198,6 +196,14 @@ let eval_with_engine | None -> handle_without_devel (Some f) | Some d -> handle_with_devel d ;; + +let eval_with_engine + guistuff lexicon_status grafite_status user_goal parsed_text st += + wrap_with_developments guistuff + (eval_with_engine + guistuff lexicon_status grafite_status user_goal parsed_text) st +;; let pp_eager_statement_ast = GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term @@ -352,8 +358,12 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status match statement with | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; - GrafiteParser.parse_statement (Ulexing.from_utf8_string text) - ~include_paths lexicon_status, text + let ast = + wrap_with_developments guistuff + (GrafiteParser.parse_statement + (Ulexing.from_utf8_string text) ~include_paths) lexicon_status + in + ast, text | `Ast (st, text) -> (lexicon_status, st), text in let text_of_loc loc = @@ -770,23 +780,23 @@ object (self) method eos = let s = self#getFuture in - let rec is_there_and_executable lexicon_status s = + let rec is_there_only_comments lexicon_status s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; let lexicon_status,st = GrafiteParser.parse_statement (Ulexing.from_utf8_string s) ~include_paths lexicon_status in match st with - 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 lexicon_status next - | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> false + is_there_only_comments lexicon_status next + | GrafiteParser.LNone _ + | GrafiteParser.LSome (GrafiteAst.Executable _) -> false in try - is_there_and_executable self#lexicon_status s + is_there_only_comments 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 8eb6d8dd9..cfc465541 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -24,6 +24,7 @@ *) exception NoUnfinishedProof +exception ActionCancelled class type script = object diff --git a/helm/ocaml/grafite_engine/grafiteEngine.ml b/helm/ocaml/grafite_engine/grafiteEngine.ml index 60b2b6a9d..65dd17b6a 100644 --- a/helm/ocaml/grafite_engine/grafiteEngine.ml +++ b/helm/ocaml/grafite_engine/grafiteEngine.ml @@ -397,6 +397,7 @@ let coercion_moo_statement_of uri = let eval_coercion status ~add_composites uri = let basedir = Helm_registry.get "matita.basedir" in let status,compounds = + prerr_endline "evaluating a coercion command"; GrafiteSync.add_coercion ~basedir ~add_composites status uri in let moo_content = coercion_moo_statement_of uri in let status = GrafiteTypes.add_moo_content [moo_content] status in @@ -522,18 +523,14 @@ let add_coercions_of_record_to_moo obj lemmas status = None) lemmas) in + prerr_endline "actual coercions:"; List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) coercions; - let status = GrafiteTypes.add_moo_content moo_content status in - let basedir = Helm_registry.get "matita.basedir" in - List.fold_left - (fun (status,lemmas) uri -> - let status,new_lemmas = - GrafiteSync.add_coercion ~basedir ~add_composites:true status uri - in - status,new_lemmas@lemmas - ) (status,[]) coercions + let status = GrafiteTypes.add_moo_content moo_content status in + {status with + GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions}, + lemmas let add_obj uri obj status = let basedir = Helm_registry.get "matita.basedir" in diff --git a/helm/ocaml/lexicon/lexiconEngine.mli b/helm/ocaml/lexicon/lexiconEngine.mli index a2232fe28..ba0938640 100644 --- a/helm/ocaml/lexicon/lexiconEngine.mli +++ b/helm/ocaml/lexicon/lexiconEngine.mli @@ -23,6 +23,7 @@ * http://helm.cs.unibo.it/ *) +exception IncludedFileNotCompiled of string type status = { aliases: DisambiguateTypes.environment; (** disambiguation aliases *) diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml index 922955aa0..abb50f363 100644 --- a/helm/ocaml/library/librarySync.ml +++ b/helm/ocaml/library/librarySync.ml @@ -50,7 +50,7 @@ let merge_coercions obj = C.Lambda (name, aux so, aux dest) | C.LetIn (name,so,dest) -> C.LetIn (name, aux so, aux dest) - | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when + | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> let source_carr = CoercGraph.source_of c2 in let tgt_carr = CoercGraph.target_of c1 in @@ -308,6 +308,9 @@ let add_coercion ~basedir ~add_composites uri = in (* store that composite_uris are related to uri. the first component is the * stuff in the DB while the second is stuff for remove_obj *) + prerr_endline ("aggiungo: " ^ string_of_bool add_composites ^ UriManager.string_of_uri uri); + List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) + composite_uris; UriManager.UriHashtbl.add coercion_hashtbl uri (composite_uris,if add_composites then composite_uris else []); lemmas @@ -317,6 +320,9 @@ let remove_coercion uri = let (composites_in_db, composites_in_lib) = UriManager.UriHashtbl.find coercion_hashtbl uri in + prerr_endline ("removing: " ^UriManager.string_of_uri uri); + List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) + composites_in_db; UriManager.UriHashtbl.remove coercion_hashtbl uri; CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u); (* remove from the DB *) @@ -340,7 +346,6 @@ let generate_projections ~basedir uri fields = CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in let attrs = [`Class `Projection; `Generated] in let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - add_single_obj ~basedir uri obj; let composites = if coercion then diff --git a/helm/ocaml/tactics/paramodulation/Makefile b/helm/ocaml/tactics/paramodulation/Makefile index 467def969..880b95953 100644 --- a/helm/ocaml/tactics/paramodulation/Makefile +++ b/helm/ocaml/tactics/paramodulation/Makefile @@ -4,8 +4,8 @@ LOCALLINKOPTS = -package helm-cic_disambiguation,helm-content_pres,helm-grafite, include ../../Makefile.common -all:saturate -opt:saturate.opt +all $(PACKAGE).cma :saturate +opt $(PACKAGE).cmxa:saturate.opt saturate: saturate_main.ml $(LIBRARIES) $(OCAMLC) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $< -- 2.39.2