X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaEngine.ml;h=3c141126d3c26f8c80be266fc8e18588c42016b4;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=7471e4546e7db2c5841bc1ea2d85884ea910c444;hpb=2d87a9eee93e86d9866120c6ae6dfe7539ee914d;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 7471e4546..3c141126d 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -25,7 +25,8 @@ let tactic_of_ast = function
       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
   | TacticAst.Intros (_, Some num, names) ->
       (* TODO Zack implement intros length *)
-      PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
+      PrimitiveTactics.intros_tac ~howmany:num
+        ~mk_fresh_name_callback:(namer_of names) ()
   | TacticAst.Reflexivity _ -> Tactics.reflexivity
   | TacticAst.Assumption _ -> Tactics.assumption
   | TacticAst.Contradiction _ -> Tactics.contradiction
@@ -59,9 +60,10 @@ let tactic_of_ast = function
   | TacticAst.Discriminate of 'ident
   | TacticAst.Fold of reduction_kind * 'term
   | TacticAst.Injection of 'ident
-  | TacticAst.LetIn of 'term * 'ident
   | TacticAst.Replace_pattern of 'term pattern * 'term
 *)
+  | TacticAst.LetIn (loc,term,name) ->
+      Tactics.letin ~term ~mk_fresh_name_callback:(namer_of [name])
   | TacticAst.ReduceAt (_,reduction_kind,ident,path) ->
       ProofEngineTypes.mk_tactic 
       (fun (((_,metasenv,_,_),goal) as status) ->
@@ -183,6 +185,64 @@ let env_of_list l e =
        e
   ) e l
 
+let eval_coercion status coercion = 
+  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 ty_src,ty_tgt = extract_last_two_p coer_ty in
+  let src_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_src) in
+  let tgt_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) in
+  let new_coercions =
+    (* also adds them to the Db *)
+    CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
+  in
+  let status = 
+    List.fold_left (
+      fun s (uri,o,ugraph) ->
+        match o with
+        | Cic.Constant (_,Some body, ty, params, attrs) ->
+            MatitaSync.add_constant ~uri ~body ~ty ~ugraph ~params ~attrs status
+        | _ -> assert false
+    ) status new_coercions
+  in
+  {status with proof_status = No_proof}
+  
 let eval_command status cmd =
   match cmd with
   | TacticAst.Set (loc, name, value) -> set_option status name value
@@ -283,8 +343,9 @@ let eval_command status cmd =
         CicUnification.fo_unif metasenv [] body_type ty ugraph
       in
       if metasenv <> [] then
-        command_error
-          "metasenv not empty while giving a definition with body";
+        command_error (
+          "metasenv not empty while giving a definition with body: " ^
+          CicMetaSubst.ppmetasenv metasenv []) ;
       let body = CicMetaSubst.apply_subst subst body in
       let ty = CicMetaSubst.apply_subst subst ty in
       let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
@@ -296,7 +357,8 @@ let eval_command status cmd =
       {status with proof_status = No_proof}
   | TacticAst.Theorem (_, _, None, _, _) ->
       command_error "The grammar should avoid having unnamed theorems!"
-  | TacticAst.Coercion (loc, term) -> assert false  (** TODO *)
+  | TacticAst.Coercion (loc, coercion) -> 
+      eval_coercion status coercion
   | TacticAst.Alias (loc, spec) -> 
       match spec with
       | TacticAst.Ident_alias (id,uri) -> 
@@ -404,9 +466,11 @@ let disambiguate_tactic status = function
   | TacticAst.Discriminate of 'ident
   | TacticAst.Fold of reduction_kind * 'term
   | TacticAst.Injection of 'ident
-  | TacticAst.LetIn of 'term * 'ident
   | TacticAst.Replace_pattern of 'term pattern * 'term
 *)
+  | TacticAst.LetIn (loc,term,name) ->
+      let status, term = disambiguate_term status term in
+      status, TacticAst.LetIn (loc,term,name)
   | TacticAst.ReduceAt (loc, reduction_kind, ident, path) ->
       let path = Disambiguate.interpretate [] status.aliases path in
       status, TacticAst.ReduceAt(loc, reduction_kind, ident, path)
@@ -567,7 +631,9 @@ let disambiguate_command status = function
             status, Some body
       in
       status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
-  | TacticAst.Coercion (loc, term) -> assert false  (** TODO *)
+  | TacticAst.Coercion (loc, term) ->
+      let status, term = disambiguate_term status term in
+      status, TacticAst.Coercion (loc,term)
   | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
       status, cmd
   | TacticAst.Alias _ as x -> status, x
@@ -634,7 +700,6 @@ let initial_status =
     aliases = DisambiguateTypes.empty_environment;
     proof_status = No_proof;
     options = default_options ();
-    coercions = [];
     objects = [];
   }