From 15a4844b5d8f64a72964e5a917b6bd6d8d7dbe44 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 7 Jun 2005 16:32:41 +0000
Subject: [PATCH] added letin

---
 helm/matita/matitaEngine.ml | 74 ++++++++++++++++++++++++++++++++++---
 1 file changed, 69 insertions(+), 5 deletions(-)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 7471e4546..ae933d2d0 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -59,9 +59,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 +184,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
@@ -276,6 +335,7 @@ let eval_command status cmd =
         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") 
       in
       let metasenv = MatitaMisc.get_proof_metasenv status in
+      debug_print ("XXXXXXXXXX" ^ CicPp.ppterm body);
       let (body_type, ugraph) =
         CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
       in
@@ -296,7 +356,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 +465,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 +630,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 +699,6 @@ let initial_status =
     aliases = DisambiguateTypes.empty_environment;
     proof_status = No_proof;
     options = default_options ();
-    coercions = [];
     objects = [];
   }
 
-- 
2.39.2