From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 10 Jul 2006 17:09:21 +0000 (+0000)
Subject: - cheanges for the new coercion stuff (including the generated graph)
X-Git-Tag: 0.4.95@7852~1234
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=da415a61eb8ecfc58817196363fad86b35efe490;p=helm.git

- cheanges for the new coercion stuff (including the generated graph)
- new test for coercions
- new test for tinycals
---

diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml
index fe8d9e569..6e92cfa95 100644
--- a/matita/applyTransformation.ml
+++ b/matita/applyTransformation.ml
@@ -78,7 +78,7 @@ let txt_of_cic_sequent_conclusion size metasenv sequent =
   let t, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts t in
   let t = TermContentPres.pp_ast t in
   let t = CicNotationPres.render ids_to_uris t in
-  BoxPp.render_to_string size t
+  BoxPp.render_to_string (function x::_ -> x | _ -> assert false) size t
 
 let txt_of_cic_term size metasenv context t = 
   let fake_sequent = (-1,context,t) in
diff --git a/matita/matita.glade b/matita/matita.glade
index a756e4042..8fc50338f 100644
--- a/matita/matita.glade
+++ b/matita/matita.glade
@@ -412,12 +412,30 @@
 	      </child>
 
 	      <child>
-		<widget class="GtkImage" id="EasterEggImage">
+		<widget class="GtkScrolledWindow" id="scrolledwindow11">
 		  <property name="visible">True</property>
-		  <property name="xalign">0.5</property>
-		  <property name="yalign">0.5</property>
-		  <property name="xpad">0</property>
-		  <property name="ypad">0</property>
+		  <property name="can_focus">True</property>
+		  <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+		  <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+		  <property name="shadow_type">GTK_SHADOW_NONE</property>
+		  <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+		  <child>
+		    <widget class="GtkViewport" id="viewport2">
+		      <property name="visible">True</property>
+		      <property name="shadow_type">GTK_SHADOW_NONE</property>
+
+		      <child>
+			<widget class="GtkImage" id="BrowserImage">
+			  <property name="visible">True</property>
+			  <property name="xalign">0.5</property>
+			  <property name="yalign">0.5</property>
+			  <property name="xpad">0</property>
+			  <property name="ypad">0</property>
+			</widget>
+		      </child>
+		    </widget>
+		  </child>
 		</widget>
 		<packing>
 		  <property name="tab_expand">False</property>
diff --git a/matita/matita.ml b/matita/matita.ml
index 3c5bf8441..164518426 100644
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -160,6 +160,20 @@ let _ =
             | Incomplete_proof i -> let _,_,p,_ = i.GrafiteTypes.proof in p
             | Proof p -> let _,_,p,_ = p in p
             | Intermediate _ -> assert false)));
+     addDebugItem "Print current proof (natural language) to stderr" 
+       (fun _ -> 
+        prerr_endline 
+          (ObjPp.obj_to_string 120 
+            (match 
+            (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
+            with
+            | GrafiteTypes.No_proof -> assert false
+            | Incomplete_proof i -> 
+                let _,m,p,ty = i.GrafiteTypes.proof in 
+                Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],[])
+            | Proof (_,m,p,ty) -> 
+                Cic.CurrentProof ("current proof",m,p,ty,[],[])
+            | Intermediate _ -> assert false)));
 (*     addDebugItem "ask record choice"
       (fun _ ->
         HLog.debug (string_of_int
@@ -187,26 +201,19 @@ let _ =
       (fun _ -> GrafiteDisambiguator.only_one_pass := true);
     addDebugSeparator ();
     addDebugItem "enable coercions hiding"
-      (fun _ -> TermAcicContent.hide_coercions := true);
+      (fun _ -> Acic2content.hide_coercions := true);
     addDebugItem "disable coercions hiding"
-      (fun _ -> TermAcicContent.hide_coercions := false);
+      (fun _ -> Acic2content.hide_coercions := false);
+    addDebugItem "show coercions graph" (fun _ ->
+      let c = MatitaMathView.cicBrowser () in
+      c#load (`About `Coercions));
     addDebugItem "dump coercions Db" (fun _ ->
       List.iter
-        (fun (s,t,u) -> 
+      (fun (s,t,ul) -> 
           HLog.debug
-            (UriManager.name_of_uri u ^ ":"
+           ((String.concat "," (List.map UriManager.name_of_uri ul)) ^ ":"
              ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
         (CoercDb.to_list ()));
-    addDebugItem "show coercions graph" (fun _ ->
-      let str = CoercGraph.generate_dot_file () in
-      let filename, oc = Filename.open_temp_file "xx" ".dot" in
-      output_string oc str;
-      close_out oc;
-      let ps = Filename.temp_file "yy" ".png" in
-      ignore (Unix.system ("/usr/bin/dot -Tpng -o" ^ ps ^ " " ^ filename));
-      ignore (Unix.system ("/usr/bin/display " ^ ps));
-      Sys.remove ps;
-      Sys.remove filename);
     addDebugSeparator ();
     let mview () = (MatitaMathView.sequentsViewer_instance ())#cicMathView in
 (*     addDebugItem "save (sequent) MathML to matita.xml"
diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 5de25e45b..486866013 100644
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -571,8 +571,8 @@ end
 let tab_label meta_markup =
   let rec aux =
     function
-    | `Current m -> sprintf "<b>%s</b>" (aux m)
     | `Closed m -> sprintf "<s>%s</s>" (aux m)
+    | `Current m -> sprintf "<b>%s</b>" (aux m)
     | `Shift (pos, m) -> sprintf "|<sub>%d</sub>: %s" pos (aux m)
     | `Meta n -> sprintf "?%d" n
   in
@@ -694,7 +694,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         ~env:(fun depth tag (pos, sw) ->
           let markup =
             match depth, pos with
-            | 0, _ -> `Current (render_switch sw)
+            | 0, 0 -> `Current (render_switch sw)
+            | 0, _ -> `Shift (pos, `Current (render_switch sw))
             | 1, pos when Stack.head_tag stack = `BranchTag ->
                 `Shift (pos, render_switch sw)
             | _ -> render_switch sw
@@ -824,7 +825,18 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   in
   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
   let load_easter_egg = lazy (
-    win#easterEggImage#set_file (MatitaMisc.image_path "meegg.png"))
+    win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
+  in
+  let load_coerchgraph () = 
+      let str = CoercGraph.generate_dot_file () in
+      let filename, oc = Filename.open_temp_file "xx" ".dot" in
+      output_string oc str;
+      close_out oc;
+      let ps = Filename.temp_file "yy" ".png" in
+      ignore (Unix.system ("/usr/bin/dot -Tpng -o" ^ ps ^ " " ^ filename));
+      Sys.remove filename;
+      at_exit (fun _ -> Sys.remove ps);
+      win#browserImage#set_file ps
   in
   object (self)
     inherit scriptAccessor
@@ -940,12 +952,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       * @param uri string *)
     method private _load ?(force=false) entry =
       handle_error (fun () ->
-       if entry <> current_entry || entry = `About `Current_proof || force then
+       if entry <> current_entry || entry = `About `Current_proof || entry =
+         `About `Coercions || force then
         begin
           (match entry with
           | `About `Current_proof -> self#home ()
           | `About `Blank -> self#blank ()
           | `About `Us -> self#egg ()
+          | `About `Coercions -> self#coerchgraph ()
           | `Check term -> self#_loadCheck term
           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
           | `Dir dir -> self#_loadDir dir
@@ -969,6 +983,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       win#mathOrListNotebook#goto_page 2;
       Lazy.force load_easter_egg
 
+    method private coerchgraph () =
+      win#mathOrListNotebook#goto_page 2;
+      load_coerchgraph ()
+
     method private home () =
       self#_showMath;
       match self#script#grafite_status.proof_status with
diff --git a/matita/matitaTypes.ml b/matita/matitaTypes.ml
index 13543dbb6..5e2e98062 100644
--- a/matita/matitaTypes.ml
+++ b/matita/matitaTypes.ml
@@ -35,6 +35,7 @@ type abouts =
   [ `Blank
   | `Current_proof
   | `Us
+  | `Coercions
   ]
   
 type mathViewer_entry =
@@ -50,6 +51,7 @@ let string_of_entry = function
   | `About `Blank -> "about:blank"
   | `About `Current_proof -> "about:proof"
   | `About `Us -> "about:us"
+  | `About `Coercions -> "about:coercions"
   | `Check _ -> "check:"
   | `Cic (_, _) -> "term:"
   | `Dir uri -> uri
@@ -60,6 +62,7 @@ let entry_of_string = function
   | "about:blank" -> `About `Blank
   | "about:proof" -> `About `Current_proof
   | "about:us"    -> `About `Us
+  | "about:coercions"    -> `About `Coercions
   | _ ->  (* only about entries supported ATM *)
       raise (Invalid_argument "entry_of_string")
 
diff --git a/matita/matitaTypes.mli b/matita/matitaTypes.mli
index be77c4435..78e0c2541 100644
--- a/matita/matitaTypes.mli
+++ b/matita/matitaTypes.mli
@@ -25,7 +25,7 @@
 
 exception Cancel
 
-type abouts = [ `Blank | `Current_proof | `Us ]
+type abouts = [ `Blank | `Current_proof | `Us | `Coercions]
 
 type mathViewer_entry =
   [ `About of abouts
diff --git a/matita/tests/coercions.ma b/matita/tests/coercions.ma
index 20b15cd26..914126de2 100644
--- a/matita/tests/coercions.ma
+++ b/matita/tests/coercions.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/coercions/".
-include "legacy/coq.ma".
+include "nat/nat.ma".
 
 inductive pos: Set \def
 | one : pos
@@ -61,4 +61,26 @@ definition double2:
 \def 
   \lambda f:int \to int. \lambda x : pos .f (nat2int (pos2nat x)).
   
-  
+coercion cic:/matita/logic/equality/eq_f.con.  
+coercion cic:/matita/logic/equality/eq_f1.con.
+variant xxx : ? \def eq_f.
+coercion cic:/matita/tests/coercions/xxx.con.
+
+theorem coercion_svelta : \forall T,S:Type.\forall f:T \to S.\forall x,y:T.x=y \to f y = f x.
+  intros.
+  apply ((\lambda h:f y = f x.h) H).
+qed.
+
+variant pos2nat' : ? \def pos2nat.
+
+coercion cic:/matita/tests/coercions/xxx.con.
+
+inductive initial: Set \def iii : initial.
+
+definition i2pos: ? \def \lambda x:initial.one.
+
+coercion cic:/matita/tests/coercions/i2pos.con.
+
+coercion cic:/matita/tests/coercions/pos2nat'.con.
+
+
diff --git a/matita/tests/tinycals.ma b/matita/tests/tinycals.ma
index 5cd2548a8..7bc189261 100644
--- a/matita/tests/tinycals.ma
+++ b/matita/tests/tinycals.ma
@@ -21,7 +21,7 @@ intros.
 apply H;
   [assumption 
   |3,5:assumption;
-  4:assumption
+  |4:assumption
   |*:assumption
   ]
 qed.
@@ -31,19 +31,21 @@ theorem prova1:
   \forall H:A \to A \to A \to A \to A \to B.A \to B.
 intros.
 apply H;
-  [*:assumption
-  ]
+  [*:assumption]
 qed. 
 
+include "logic/connectives.ma".
+
 theorem prova2: 
   \forall A,B:Prop.
-  \forall H:A \to A \to A \to A \to A \to B.A \to B.
+  \forall H:A \to A \to A \to (A \land A) \to A \to B.A \to B.
 intros.
 apply H;
   [2:assumption
-   |assumption
-   3,5:assumption
-   *:assumption
+  |4:split.assumption
+  |3,5:assumption
+  |*:assumption
   ]
+assumption.
 qed.