X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_content%2Facic2content.ml;h=a2e7622ea6549d6ee1b87941e95daa150b126c36;hb=14c956f9be9e525fc2dd140e8a2ea6c063c48930;hp=57b8502bb3ac4e35029178490e0726766b94f1de;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml
index 57b8502bb..a2e7622ea 100644
--- a/components/acic_content/acic2content.ml
+++ b/components/acic_content/acic2content.ml
@@ -44,6 +44,8 @@ let conclude_prefix = "concl:";;
 let premise_prefix = "prem:";;
 let lemma_prefix = "lemma:";;
 
+let hide_coercions = ref true;;
+
 (* e se mettessi la conversione di BY nell'apply_context ? *)
 (* sarebbe carino avere l'invariante che la proof2pres
 generasse sempre prove con contesto vuoto *)
@@ -500,11 +502,17 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
           generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
         else raise Not_a_proof 
     | C.AAppl (id,li) ->
-        (try rewrite 
+        (try coercion 
+           seed li ~ids_to_inner_types ~ids_to_inner_sorts
+         with NotApplicable ->
+         try rewrite 
            seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
          try inductive 
           seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
+         with NotApplicable ->
+         try transitivity 
+           seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
           let subproofs, args =
             build_subproofs_and_args 
@@ -792,6 +800,22 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
           } 
   | _ -> raise NotApplicable
 
+and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
+  match li with
+    | ((Cic.AConst _) as he)::tl
+    | ((Cic.AMutInd _) as he)::tl
+    | ((Cic.AMutConstruct _) as he)::tl when 
+       CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
+       !hide_coercions ->
+        let rec last =
+         function
+            [] -> assert false
+          | [t] -> t
+          | _::tl -> last tl
+        in
+          acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+    | _ -> raise NotApplicable
+
 and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
   let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
   let module C2A = Cic2acic in
@@ -843,8 +867,66 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
           } 
       else raise NotApplicable
   | _ -> raise NotApplicable
+
+and transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
+  let module C2A = Cic2acic in
+  let module K = Content in
+  let module C = Cic in
+  match li with 
+    | C.AConst (sid,uri,exp_named_subst)::args 
+	when LibraryObjects.is_trans_eq_URI uri ->
+	let exp_args = List.map snd exp_named_subst in
+	let t1,t2,t3,p1,p2 =
+	  match exp_args@args with
+	    | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
+	    | _ -> raise NotApplicable
+	in
+	  { K.proof_name = name;
+            K.proof_id  = gen_id proof_prefix seed;
+            K.proof_context = []; 
+            K.proof_apply_context = [];
+            K.proof_conclude = 
+              { K.conclude_id = gen_id conclude_prefix seed; 
+                K.conclude_aref = id;
+                K.conclude_method = "Eq_chain";
+                K.conclude_args = 
+                   K.Term t1::
+		     (transitivity_aux 
+			seed ~ids_to_inner_types ~ids_to_inner_sorts p1)@
+		     [K.Term t2]@
+		     (transitivity_aux 
+			seed ~ids_to_inner_types ~ids_to_inner_sorts p2)@
+		     [K.Term t3];
+                K.conclude_conclusion = 
+                   try Some 
+                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
+                   with Not_found -> None
+              }
+          } 
+    | _ -> raise NotApplicable
+
+and transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts t =
+  let module C2A = Cic2acic in
+  let module K = Content in
+  let module C = Cic in
+  match t with 
+    | C.AAppl (_,C.AConst (sid,uri,exp_named_subst)::args) 
+	when LibraryObjects.is_trans_eq_URI uri ->
+	let exp_args = List.map snd exp_named_subst in
+	let t1,t2,t3,p1,p2 =
+	  match exp_args@args with
+	    | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
+	    | _ -> raise NotApplicable
+	in
+          (transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p1)
+	  @[K.Term t2]
+	  @(transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p2)
+    | _ -> [K.ArgProof 
+	(acic2content seed ~ids_to_inner_sorts ~ids_to_inner_types t)]
+
 ;; 
 
+
 let map_conjectures
  seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
 =