fixed coercions

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index f52901ea684f4a075e1766b1c6a7d32e0f9413b6..16711fa30b341ed17424ba965f90da053c31e3b4 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -195,9 +195,16 @@ class sharedState
           Quiet
       | TacticAst.Command (TacticAst.Print `Env) ->
           let uris = CicEnvironment.list_uri () in
+          console#echo_message "Environment:";
           List.iter (fun u ->
-            console#echo_message (UriManager.string_of_uri u);
-            prerr_endline "x"
+            console#echo_message ("  " ^ (UriManager.string_of_uri u))
+          ) uris;
+          Quiet
+      | TacticAst.Command (TacticAst.Print `Coer) ->
+          let uris = CoercGraph.get_coercions_list () in
+          console#echo_message "Coercions:";
+          List.iter (fun (s,t,u) ->
+            console#echo_message ("  " ^ (UriManager.string_of_uri u))
           ) uris;
           Quiet
       | tactical ->
@@ -448,8 +455,6 @@ class commandState
             (* do nothing, just for compatibility with coq syntax *)
           New_state Command
       | TacticAst.Command (TacticAst.Coercion c_ast) ->
-          prerr_endline ("beccata la coercion " ^ (CicAstPp.pp_term c_ast));
-
           let env, metasenv, coercion, ugraph = 
             disambiguator#disambiguateTermAst c_ast 
           in
@@ -492,14 +497,18 @@ class commandState
             in  
             aux ty
           in
-          let uri_of_term = function
+          let rec uri_of_term = function
             | Cic.Const(u,_) -> u
             | Cic.MutInd (u, i , _) ->
                 (* we have to build by hand the #xpointer *)
                 let base = UriManager.string_of_uri u in
                 let xp = "#xpointer(1/" ^ (string_of_int (i+1)) ^ ")" in
                   UriManager.uri_of_string (base ^ xp)
-            | _ -> assert false 
+            | Cic.Appl (he::_) -> uri_of_term he
+            | t -> 
+                prerr_endline ("Fallisco a estrarre la uri di " ^ 
+                  (CicPp.ppterm t));
+                assert false 
           in
           let ty_src,ty_tgt = extract_last_two_p coer_ty in
           let src_uri = uri_of_term ty_src in
@@ -510,12 +519,14 @@ class commandState
           (* FIXME: we should chek it this object can be a coercion 
            * maybe add the check to extract_last_two_p
            *)
+          console#echo_message (sprintf "Coercion %s"
+            (UriManager.string_of_uri coer_uri));
           List.iter (fun (uri,obj,ugraph) -> 
-            (*
-            prerr_endline (Printf.sprintf 
-             "Aggiungo la coercion %s\n%s\n\n"
-             (UriManager.string_of_uri uri) (CicPp.ppobj obj));
-            *)
+          (*  
+            console#echo_message 
+             (sprintf "Coercion (automatic) %s" 
+               (UriManager.string_of_uri uri));
+          *)
             let (name, body, ty, attrs) = split_obj obj in
             add_constant_to_world ~console 
               ~dbd ~uri ?body ~ty ~attrs ~ugraph ();

diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma
new file mode 100644 (file)
index 0000000..1e92364
--- /dev/null
+++ b/helm/matita/tests/coercions.ma
@@ -0,0 +1,50 @@
+
+Inductive nat : Set \def
+| O : nat
+| S : nat \to nat.
+
+Inductive list (A:Set) : Set \def
+| nil : list A
+| cons : A \to list A \to list A.
+
+Inductive bool: Set \def
+| true : bool
+| false : bool.
+
+
+
+
+let rec len (A:Set)(l:list A) on l : nat \def
+ match l:list with [
+   nil \Rightarrow O
+ | (cons e tl) \Rightarrow (S (len A tl))].
+
+let rec plus (n,m:nat) : nat \def
+ match n:nat with [
+   O \Rightarrow m
+ | (S x) \Rightarrow (S (plus x m)) ].  
+
+let rec is_zero (n:nat) : bool \def
+  match n:nat with [
+    O \Rightarrow true
+  | (S x) \Rightarrow false].  
+
+let rec nat_eq_dec (n,m:nat) : bool \def
+  match n:nat with [
+    O \Rightarrow 
+         match m:nat with [
+           O \Rightarrow true
+        | (S x) \Rightarrow false]
+  | (S x) \Rightarrow
+             match m:nat with [
+               O \Rightarrow false
+            | (S y) \Rightarrow (nat_eq_dec x y)]
+  ].
+
+
+Coercion is_zero.
+Coercion len.
+
+Print Coer.
+Print Env.
+