- added code for Coercion command, Print Env command.

- better error report in matitac

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 8039e48222351b8e845f80ee02f0519fc6dedabd..818f7fe943621d5c6ad233e5ef1f3b89c31832f4 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -181,6 +181,13 @@ class sharedState
           in
           (* TODO ZACK: show URIs to the user *)
           Quiet
+      | TacticAst.Command (TacticAst.Print `Env) ->
+          let uris = CicEnvironment.list_uri () in
+          List.iter (fun u ->
+            console#echo_message (UriManager.string_of_uri u);
+            prerr_endline "x"
+          ) uris;
+          Quiet
       | tactical ->
           raise (Command_error (TacticAstPp.pp_tactical tactical))
   end
@@ -372,6 +379,80 @@ class commandState
       | TacticAst.Command TacticAst.Proof ->
             (* 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
+          let coer_uri,coer_ty =
+            match coercion with 
+            | Cic.Const (uri,_)
+            | Cic.Var (uri,_) ->
+                let o,_ = 
+                  CicEnvironment.get_obj CicUniv.empty_ugraph uri 
+                in
+                (match o with
+                | Cic.Constant (_,_,ty,_,_)
+                | Cic.Variable (_,_,ty,_,_) ->
+                    uri,ty
+                | _ -> assert false)
+            | Cic.MutConstruct (uri,t,c,_) ->
+                let o,_ = 
+                  CicEnvironment.get_obj CicUniv.empty_ugraph uri 
+                in
+                (match o with
+                | Cic.InductiveDefinition (l,_,_,_) ->
+                    let (_,_,_,cl) = List.nth l t in
+                    let (_,cty) = List.nth cl c in
+                      uri,cty
+                | _ -> assert false)
+            | _ -> assert false 
+          in
+          (* we have to get the source and the tgt type uri 
+           * in Coq syntax we have already their names, but 
+           * since we don't support Funclass and similar I think
+           * all the coercion should be of the form
+           * (A:?)(B:?)T1->T2
+           * So we should be able to extract them from the coercion type
+           *)
+          let extract_last_two_p ty =
+            let rec aux = function
+              | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))   
+              | Cic.Prod( _, src, tgt) -> src, tgt
+              | _ -> assert false
+            in  
+            aux ty
+          in
+          let 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 
+          in
+          let ty_src,ty_tgt = extract_last_two_p coer_ty in
+          let src_uri = uri_of_term ty_src in
+          let tgt_uri = uri_of_term ty_tgt in
+          let coercions_to_add = 
+            CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
+          in
+          (* FIXME: we should chek it this object can be a coercion 
+           * maybe add the check to extract_last_two_p
+           *)
+          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));
+            *)
+            let (name, body, ty, attrs) = split_obj obj in
+            add_constant_to_world ~console 
+              ~dbd ~uri ?body ~ty ~attrs ~ugraph ();
+          ) coercions_to_add;
+          Quiet
       | tactical -> shared#evalTactical tactical
   end
 

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index 3f394cdb1108e9dc70158ad99d51c66b714bccc0..bb796db1e79d8f005630d227cfacd8bdee3437a7 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -87,7 +87,14 @@ let run_script fname =
   message (sprintf "execution of %s started:" fname);
   let script =
     let ic = open_in fname in
-    let ast = snd (CicTextualParser2.parse_script (Stream.of_channel ic)) in
+    let ast = 
+      try 
+        snd (CicTextualParser2.parse_script (Stream.of_channel ic)) 
+      with
+        exn -> 
+          error (explain exn); 
+          assert false (* should be something like (Unix.exit 1) *)
+    in
     close_in ic;
     ast
   in