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

diff --git a/helm/matita/.depend b/helm/matita/.depend
index cf6cf85223fad823d336fa781f0fa66f32759009..605b57a740ceed3866ae718b6aa2b7e520a0a7d8 100644 (file)
--- 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 4600b0ecc8707cc5c1f350fd4dd86b6b57212f16..ab8d4d9cfd0ed78ea20c3c364bcdb53c4f904345 100644 (file)
--- 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 a25f8c79a1abc8e51c70408028f0186070204513..acbc2ecf1b1989fb3b7cbfa9137af18404b71cfe 100644 (file)
--- 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 769f294fd2ef6d2743ef4d925bee4c3191afb3c2..efaaa57074fe0d71261321426daaa3bfac2b70cd 100644 (file)
--- 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 457f376bb2c0afcb3b3540a68aeaca84f482d94e..430151d9a42fbd1594391aac8a1722bb4f8eff81 100644 (file)
--- 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 8c469df391458d2369f45621f9b624ba713041d7..ac6d91cb9bbfaeb506c123cc5ff12532bff7a188 100644 (file)
--- 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 d58ceaf7a45c952d916b91539c26b78ddcf3e67d..c09b22fdd1c053127981cad7226a9968375e34af 100644 (file)
--- 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 641ac4c9aab9a8a0b799f25115ea84902b19f200..6308eab86e3035f0fe170ce0b24bbf82f21cb843 100644 (file)
--- 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 75773e3fe579f3b1ccf9cf12a55befbcf9618cc1..da2c5b2fa168a85080812a7e329004d38f2a2c4d 100644 (file)
--- 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 e407b090a42e85516e4875c7e4d85a19e0b8adf3..2b36a5d3d4fb3165d33ca8aacf00feab8cba5ff2 100644 (file)
--- 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 355ceed6044385e3e325ca9f73008b11ac26f37d..1f9dad80f7dbcf1815dbdf7123c6a7032a7e5945 100644 (file)
--- 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 c845954ed36776a99c3496628e6f853d8894f4a7..e93dbad61ad379b4b1e671c36cd9f6cd092807af 100644 (file)
--- 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 5ae1165bbbc17666f80a5bfd17232b00e300edee..8cbef1fd193a85cc08f35047dfcd3c9ebc831679 100644 (file)
--- 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 ae69759bf4c083fe6ccaf5c4acb2325631d5e69d..aec51ae8b5f699ea51ff97b06bf17fa2adced7fc 100644 (file)
--- 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