fixed coercions

[helm.git] / helm / matita / matitaInterpreter.ml

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 ();