added a test for the pullback stuff and the possibility to get the coercion graph...

diff --git a/matita/matita.ml b/matita/matita.ml
index 609a014d0f3b573ac9b152ca9816fb880668911a..783b8c0231ed14654b623dd93891c248ca861e9c 100644 (file)
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -198,6 +198,22 @@ let _ =
          let nb = gui#main#hintNotebook in
          nb#goto_page ((nb#current_page + 1) mod 3)); *)
     addDebugSeparator ();
+(*
+    addDebugItem "meets between L and R" 
+      (fun _ -> 
+        let l = CoercDb.coerc_carr_of_term (CicUtil.term_of_uri
+          (UriManager.uri_of_string "cic:/matita/test/L.ind#xpointer(1/1)" )) 
+        in
+        let r = CoercDb.coerc_carr_of_term (CicUtil.term_of_uri
+          (UriManager.uri_of_string "cic:/matita/test/R.ind#xpointer(1/1)" )) 
+        in
+        let meets = CoercGraph.meets l r in
+        prerr_endline "MEETS:";
+        List.iter (fun carr -> prerr_endline (CicPp.ppterm (CoercDb.term_of_carr
+        carr))) meets
+    );
+    addDebugSeparator ();
+*)
     addDebugItem "disable all (pretty printing) notations"
       (fun _ -> CicNotation.set_active_notations []);
     addDebugItem "enable all (pretty printing) notations"
@@ -217,6 +233,9 @@ let _ =
     addDebugItem "show coercions graph" (fun _ ->
       let c = MatitaMathView.cicBrowser () in
       c#load (`About `Coercions));
+    addDebugItem "show coercions graph (full)" (fun _ ->
+      let c = MatitaMathView.cicBrowser () in
+      c#load (`About `CoercionsFull));
     addDebugItem "dump coercions Db" (fun _ ->
       List.iter
       (fun (s,t,ul) -> 

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 5ae8baab6ea2f6ee0943bdf723d275be0d3e8c4c..ee49267fe3c57d1579fb2924dd07dc4c7e1c0150 100644 (file)
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -844,12 +844,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let load_easter_egg = lazy (
     win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
   in
-  let load_coerchgraph () = 
+  let load_coerchgraph tred () = 
       let str = CoercGraph.generate_dot_file () in
       let filename, oc = Filename.open_temp_file "matita" ".dot" in
       output_string oc str;
       close_out oc;
-      gviz#load_graph_from_file filename;
+      if tred then
+        gviz#load_graph_from_file ~gviz_cmd:"tred|dot" filename
+      else
+        gviz#load_graph_from_file filename;
       HExtlib.safe_remove filename
   in
   object (self)
@@ -1024,13 +1027,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private _load ?(force=false) entry =
       handle_error (fun () ->
        if entry <> current_entry || entry = `About `Current_proof || entry =
-         `About `Coercions || force then
+         `About `Coercions || entry = `About `CoercionsFull || force then
         begin
           (match entry with
           | `About `Current_proof -> self#home ()
           | `About `Blank -> self#blank ()
           | `About `Us -> self#egg ()
-          | `About `Coercions -> self#coerchgraph ()
+          | `About `CoercionsFull -> self#coerchgraph false ()
+          | `About `Coercions -> self#coerchgraph true ()
           | `Check term -> self#_loadCheck term
           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
           | `Development d -> self#_showDevelDeps d
@@ -1079,8 +1083,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#redraw_gviz ~center_on:uri ();
       self#_showGviz
 
-    method private coerchgraph () =
-      load_coerchgraph ();
+    method private coerchgraph tred () =
+      load_coerchgraph tred ();
       self#_showGviz
 
     method private home () =

diff --git a/matita/matitaTypes.ml b/matita/matitaTypes.ml
index 791713e56a4b5e13f2fa302cf7c87dac52796c6d..23d0d832f238947adef0cb875c86b65ddd750af4 100644 (file)
--- a/matita/matitaTypes.ml
+++ b/matita/matitaTypes.ml
@@ -36,6 +36,7 @@ type abouts =
   | `Current_proof
   | `Us
   | `Coercions
+  | `CoercionsFull
   ]
   
 type mathViewer_entry =
@@ -54,7 +55,8 @@ let string_of_entry = function
   | `About `Blank -> "about:blank"
   | `About `Current_proof -> "about:proof"
   | `About `Us -> "about:us"
-  | `About `Coercions -> "about:coercions"
+  | `About `Coercions -> "about:coercions?tred=true"
+  | `About `CoercionsFull -> "about:coercions"
   | `Check _ -> "check:"
   | `Cic (_, _) -> "term:"
   | `Development d -> "devel:/" ^ d
@@ -77,7 +79,8 @@ let entry_of_string = function
   | "about:blank" -> `About `Blank
   | "about:proof" -> `About `Current_proof
   | "about:us"    -> `About `Us
-  | "about:coercions"    -> `About `Coercions
+  | "about:coercions?tred=true"    -> `About `Coercions
+  | "about:coercions"    -> `About `CoercionsFull
   | _ ->  (* only about entries supported ATM *)
       raise (Invalid_argument "entry_of_string")
 

diff --git a/matita/matitaTypes.mli b/matita/matitaTypes.mli
index c2e3f40ed3a87e0633d4ec16d777371972255133..c71c99dcc9adc1eea9ad23a780eca3113baa3ce7 100644 (file)
--- a/matita/matitaTypes.mli
+++ b/matita/matitaTypes.mli
@@ -25,7 +25,7 @@
 
 exception Cancel
 
-type abouts = [ `Blank | `Current_proof | `Us | `Coercions]
+type abouts = [ `Blank | `Current_proof | `Us | `Coercions | `CoercionsFull]
 
 type mathViewer_entry =
   [ `About of abouts

diff --git a/matita/tests/pullback.ma b/matita/tests/pullback.ma
new file mode 100644 (file)
index 0000000..228d27d
--- /dev/null
+++ b/matita/tests/pullback.ma
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/test/".
+
+inductive T : Type \def t : T.
+inductive L : Type \def l : L.
+inductive R : Type \def r : R.
+inductive R1 : Type \def r1 : R1.
+inductive P1 : Type \def p1 : P1.
+inductive P2 : Type \def p2 : P2.
+
+definition L_to_T : L \to T \def \lambda x.t.
+definition R_to_T : R \to T \def \lambda x.t.
+definition P1_to_L : P1 \to L \def \lambda x.l.
+definition P1_to_R1 : P1 \to R1 \def \lambda x.r1.
+definition R1_to_P2 : R1 \to P2 \def \lambda x.p2.
+definition R1_to_R : R1 \to R \def \lambda x.r.
+definition P2_to_L : P2 \to L \def \lambda x.l.
+definition P2_to_R : P2 \to R \def \lambda x.r.
+definition P1_to_P1 : P1 \to P1 \def \lambda x.p1.
+
+coercion cic:/matita/test/L_to_T.con.
+coercion cic:/matita/test/R_to_T.con.
+coercion cic:/matita/test/P1_to_L.con.
+coercion cic:/matita/test/P1_to_R1.con.
+coercion cic:/matita/test/R1_to_R.con.
+coercion cic:/matita/test/R1_to_P2.con.
+coercion cic:/matita/test/P2_to_L.con.
+coercion cic:/matita/test/P2_to_R.con.
+coercion cic:/matita/test/P1_to_P1.con.