X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=3c141126d3c26f8c80be266fc8e18588c42016b4;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=10fe24030d00c27951d49580f499fbd5c2c49754;hpb=4b84dd78aa6b596a0d3ee38745890ff65efa8b10;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 10fe24030..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,50 @@ 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) ->
+         let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+         let where, also_in_hypotheses = 
+           if ident = "goal" then
+             ty, false
+           else
+             let hyp = 
+               try 
+                 List.find (function 
+                   | Some (Cic.Name name,entry) when name = ident -> true
+                   | _ -> false) 
+                 context
+               with 
+                 Not_found -> raise (ProofEngineTypes.Fail (ident ^ " is not an hypothesis"))  
+             in 
+             (match hyp with
+             | Some (_, Cic.Decl term) -> term
+             | Some (_, Cic.Def (term,ty)) -> term
+             | None -> assert false),true
+         in
+         let pointers = CicUtil.select ~term:where ~context:path in
+          (match reduction_kind with
+          | `Normalize -> 
+              ProofEngineTypes.apply_tactic 
+                (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers)) 
+                status
+          | `Reduce -> 
+              ProofEngineTypes.apply_tactic 
+                (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers)) 
+                status
+          | `Simpl -> 
+              ProofEngineTypes.apply_tactic 
+                (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers)) 
+                status
+          | `Whd -> 
+              ProofEngineTypes.apply_tactic 
+                (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers)) 
+                status)) 
   | TacticAst.Reduce (_,reduction_kind,opts) ->
       let terms, also_in_hypotheses = 
         match opts with
@@ -70,6 +112,7 @@ let tactic_of_ast = function
         | None -> None, false
       in
       (match reduction_kind with
+      | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms
       | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
       | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
       | `Whd -> Tactics.whd ~also_in_hypotheses ~terms) 
@@ -142,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
@@ -242,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
@@ -255,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) -> 
@@ -363,9 +466,14 @@ 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)
   | TacticAst.Reduce (loc, reduction_kind, opts) ->
       let status, opts = 
         match opts with
@@ -523,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
@@ -590,7 +700,6 @@ let initial_status =
     aliases = DisambiguateTypes.empty_environment;
     proof_status = No_proof;
     options = default_options ();
-    coercions = [];
     objects = [];
   }