From 41be5e85a1103a5b14495bb487995a6a88e79c48 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Dec 2005 15:42:37 +0000 Subject: [PATCH] Big commit to let Ferruccio try the merge_coercion patch. 1) allowed :> syntax in record to specify that a field is a coercion (and it will be used (if needed) in defining the following projections) 2) minor cleanup in CicUtil.is_metaclosed 3) added library_objects.reset_defaults() (used in MatitaSync.init()) 4) added MatitaSync.init() that is the only way to obtain an initial matita status 5) CoercDb is only accessed by CoercGraph 6) insert_coercion flag added to the refiner (and removed the use_coercion flag from CoercDb). Coercions are always available, the refiner will eventually insert them 7) CicRefiner now packs coercions with the avoid_double_coercion function 8) GrafiteAstPp is now "more" in sync and dump_moo seems to work again 9) LibrarySync has a merge_coercions function that calls on `Generated && not(is_coercion) objects. I hope it is enough (calling it on every objects shlows down a bit 10)MatitaScript now calls MatitaSync.init() on reset TODO: - remove CoercGraph.remove_coercion from add_single_obj - find a place for CoercGraph.add_coercion used in generate_projections --- helm/matita/.depend | 48 +++++++++---------- .../contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma | 6 +-- .../PREDICATIVE-TOPOLOGY/coa_props.ma | 6 ++- helm/matita/matita.ml | 1 - helm/matita/matitaEngine.ml | 15 ------ helm/matita/matitaEngine.mli | 1 - helm/matita/matitaExcPp.ml | 2 + helm/matita/matitaGui.ml | 2 +- helm/matita/matitaScript.ml | 20 +++++--- helm/matita/matitaScript.mli | 1 - helm/matita/matitacLib.ml | 4 +- helm/matita/matitadep.ml | 4 +- helm/matita/template_makefile.in | 2 +- helm/matita/tests/coercions.ma | 17 +++++++ 14 files changed, 70 insertions(+), 59 deletions(-) diff --git a/helm/matita/.depend b/helm/matita/.depend index cf6cf8522..605b57a74 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -2,12 +2,16 @@ applyTransformation.cmo: applyTransformation.cmi applyTransformation.cmx: applyTransformation.cmi dump_moo.cmo: buildTimeConf.cmo dump_moo.cmx: buildTimeConf.cmx -matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ - matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi matitaEngine.cmi \ - buildTimeConf.cmo -matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ - matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx matitaEngine.cmx \ - buildTimeConf.cmx +matitaclean.cmo: matitaInit.cmi matitaclean.cmi +matitaclean.cmx: matitaInit.cmx matitaclean.cmi +matitacLib.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ + buildTimeConf.cmo matitacLib.cmi +matitacLib.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ + buildTimeConf.cmx matitacLib.cmi +matitac.cmo: matitamake.cmo matitadep.cmi matitaclean.cmi matitacLib.cmi +matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx +matitadep.cmo: matitaInit.cmi matitadep.cmi +matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi matitaEngine.cmx: matitaEngine.cmi matitaExcPp.cmo: matitaExcPp.cmi @@ -24,34 +28,30 @@ matitaGui.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \ matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi matitaInit.cmo: matitamakeLib.cmi buildTimeConf.cmo matitaInit.cmi matitaInit.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaInit.cmi +matitamakeLib.cmo: buildTimeConf.cmo matitamakeLib.cmi +matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi +matitamake.cmo: matitamakeLib.cmi matitaInit.cmi +matitamake.cmx: matitamakeLib.cmx matitaInit.cmx matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi buildTimeConf.cmo \ applyTransformation.cmi matitaMathView.cmi matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx buildTimeConf.cmx \ applyTransformation.cmx matitaMathView.cmi -matitaMisc.cmo: matitaTypes.cmi buildTimeConf.cmo matitaMisc.cmi -matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi +matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi +matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi +matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ + matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi matitaEngine.cmi \ + buildTimeConf.cmo +matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ + matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx matitaEngine.cmx \ + buildTimeConf.cmx matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaMisc.cmi \ - matitaEngine.cmi buildTimeConf.cmo matitaScript.cmi + buildTimeConf.cmo matitaScript.cmi matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \ - matitaEngine.cmx buildTimeConf.cmx matitaScript.cmi + buildTimeConf.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi -matitac.cmo: matitamake.cmo matitadep.cmi matitaclean.cmi matitacLib.cmi -matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx -matitacLib.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ - buildTimeConf.cmo matitacLib.cmi -matitacLib.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ - buildTimeConf.cmx matitacLib.cmi -matitaclean.cmo: matitaInit.cmi matitaclean.cmi -matitaclean.cmx: matitaInit.cmx matitaclean.cmi -matitadep.cmo: matitaInit.cmi matitadep.cmi -matitadep.cmx: matitaInit.cmx matitadep.cmi -matitamake.cmo: matitamakeLib.cmi matitaInit.cmi -matitamake.cmx: matitamakeLib.cmx matitaInit.cmx -matitamakeLib.cmo: buildTimeConf.cmo matitamakeLib.cmi -matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaGui.cmi: matitaGuiTypes.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmi diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma index 4600b0ecc..ab8d4d9cf 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma @@ -21,10 +21,10 @@ include "domain_data.ma". *) record COA: Type \def { - coa: Class; (* carrier *) + coa:> Class; (* carrier *) le: coa \to coa \to Prop; (* inclusion *) ov: coa \to coa \to Prop; (* overlap *) - sup: \forall (D:Domain). (D \to coa) \to coa; (* suprimum *) + sup: \forall (D:Domain). (D \to coa) \to coa; (* supremum *) inf: \forall (D:Domain). (D \to coa) \to coa; (* infimum *) le_refl: \forall p. le p p; le_trans: \forall p,r. le p r \to \forall q. le r q \to le p q; @@ -36,8 +36,6 @@ record COA: Type \def { density: \forall p,q. (\forall r. ov p r \to ov q r) \to le p q }. -coercion coa. - definition zero: \forall (P:COA). P \def \lambda (P:COA). inf P ? (dvoid_ixfam P). diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma index a25f8c79a..acbc2ecf1 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma @@ -16,4 +16,8 @@ set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/coa_props". include "coa_defs.ma". -theorem zero_le: \forall (P:COA). \forall (p:P). le ? (zero P) p. +theorem zero_le: \forall (P:COA). \forall (p:Type_of_COA P). le ? (zero P) p. + + + + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 769f294fd..efaaa5707 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -41,7 +41,6 @@ let script = let s = MatitaScript.script ~source_view:gui#sourceView - ~init:(Lazy.force MatitaEngine.initial_status) ~mathviewer:(MatitaMathView.mathViewer ()) ~urichooser:(fun uris -> try diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 457f376bb..430151d9a 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -56,18 +56,3 @@ let eval_string ?do_heavy_checks ~include_paths ?clean_baseuri status str = (Ulexing.from_utf8_string str) (fun _ _ -> ()) with End_of_file -> () -let default_options () = no_options - -let initial_status = - lazy { - aliases = DisambiguateTypes.Environment.empty; - multi_aliases = DisambiguateTypes.Environment.empty; - moo_content_rev = []; - metadata = []; - proof_status = No_proof; - options = default_options (); - objects = []; - coercions = []; - notation_ids = []; - } - diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index 8c469df39..ac6d91cb9 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -40,4 +40,3 @@ val eval_from_stream: (GrafiteTypes.status -> GrafiteParser.statement -> unit) -> unit -val initial_status: GrafiteTypes.status lazy_t diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index d58ceaf7a..c09b22fdd 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -61,6 +61,8 @@ let rec to_string = None, "Type checking error: " ^ Lazy.force msg | CicTypeChecker.AssertFailure msg -> None, "Type checking assertion failed: " ^ Lazy.force msg + | LibrarySync.AlreadyDefined s -> + None, "Already defined: " ^ UriManager.string_of_uri s | MatitaDisambiguator.DisambiguationError (offset,errorll) -> let rec aux n = function diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 641ac4c9a..6308eab86 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -96,7 +96,7 @@ let ask_and_save_moo_if_needed parent fname status = | `CANCEL -> raise MatitaTypes.Cancel in if b then - save () + save () else clean_current_baseuri status end diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 75773e3fe..da2c5b2fa 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -427,7 +427,6 @@ let fresh_script_id = fun () -> incr i; !i class script ~(source_view: GSourceView.source_view) - ~(init: GrafiteTypes.status) ~(mathviewer: MatitaTypes.mathViewer) ~set_star ~ask_confirmation @@ -463,7 +462,7 @@ object (self) (fun _ -> set_star (Filename.basename self#ppFilename) buffer#modified)) val mutable statements = []; (** executed statements *) - val mutable history = [ init ]; + val mutable history = [ MatitaSync.init () ]; (** 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. @@ -634,11 +633,20 @@ object (self) end method private goto_top = + let init = + let rec last x = function + | [] -> x + | hd::tl -> last hd tl + in + last self#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 method private reset_buffer = statements <- []; - history <- [ init ]; + history <- [ MatitaSync.init () ]; userGoal <- ~-1; self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; @@ -649,7 +657,7 @@ object (self) source_buffer#begin_not_undoable_action (); buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter; source_buffer#end_not_undoable_action (); - buffer#set_modified false + buffer#set_modified false; method template () = let template = HExtlib.input_file BuildTimeConf.script_template in @@ -786,10 +794,10 @@ end let _script = ref None -let script ~source_view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star () +let script ~source_view ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star () = let s = new script - ~source_view ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () + ~source_view ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () in _script := Some s; s diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index e407b090a..2b36a5d3d 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -81,7 +81,6 @@ end * "*") on the side of a script name *) val script: source_view:GSourceView.source_view -> - init:GrafiteTypes.status -> mathviewer: MatitaTypes.mathViewer-> urichooser: (UriManager.uri list -> UriManager.uri list) -> develcreator: (containing:string option -> unit) -> diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 355ceed60..1f9dad80f 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -123,7 +123,7 @@ let go () = CicEnvironment.set_trust (* environment trust *) (let trust = Helm_registry.get_bool "matita.environment_trust" in fun _ -> trust); - status := Some (ref (Lazy.force MatitaEngine.initial_status)); + status := Some (ref (MatitaSync.init ())); Sys.catch_break true; interactive_loop () @@ -131,7 +131,7 @@ 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 (Lazy.force MatitaEngine.initial_status)); + status := Some (ref (MatitaSync.init ())); Sys.catch_break true; let origcb = HLog.get_log_callback () in let newcb tag s = diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index c845954ed..e93dbad61 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -35,10 +35,10 @@ let main () = let resolve alias current_buri = let buri = buri alias in if buri <> current_buri then Some buri else None in - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" in MatitaInit.load_configuration_file (); MatitaInit.parse_cmdline (); + let include_paths = + Helm_registry.get_list Helm_registry.string "matita.includes" in let basedir = Helm_registry.get "matita.basedir" in List.iter (fun ma_file -> diff --git a/helm/matita/template_makefile.in b/helm/matita/template_makefile.in index 5ae1165bb..8cbef1fd1 100644 --- a/helm/matita/template_makefile.in +++ b/helm/matita/template_makefile.in @@ -21,7 +21,7 @@ clean: ($(MATITAC) $(MATITA_FLAGS) -q -I @ROOT@ $< | (grep -v "^make" || true)) @DEPFILE@ : $(SRC) - $(MATITADEP) $(MATITA_FLAGS) -I '@ROOT@' $^ 1> @DEPFILE@ 2>/dev/null + $(MATITADEP) $(MATITA_FLAGS) -I '@ROOT@' $^ 1> @DEPFILE@ # this is the depend for full targets like: # dir/dir/name.moo: dir/dir/name.ma dir/dep.moo diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma index ae69759bf..aec51ae8b 100644 --- a/helm/matita/tests/coercions.ma +++ b/helm/matita/tests/coercions.ma @@ -45,3 +45,20 @@ definition fst \def \lambda x,y:int.x. theorem a: fst O one = fst (positive O) (next one). reflexivity. qed. + +definition double: + \forall f:int \to int. pos \to int +\def + \lambda f:int \to int. \lambda x : pos .f (nat2int x). + +definition double1: + \forall f:int \to int. pos \to int +\def + \lambda f:int \to int. \lambda x : pos .f (pos2nat x). + +definition double2: + \forall f:int \to int. pos \to int +\def + \lambda f:int \to int. \lambda x : pos .f (nat2int (pos2nat x)). + + \ No newline at end of file -- 2.39.2