Very experimental commit: the type of the source is now required in LetIns

[helm.git] / helm / software / components / acic_content / content2cic.ml

diff --git a/helm/software/components/acic_content/content2cic.ml b/helm/software/components/acic_content/content2cic.ml
index 9acea81fa903b8455c830763b5a4c26fef365b66..33c5921fba83d99344ad540fb1c96a849caf6fe2 100644 (file)
--- a/helm/software/components/acic_content/content2cic.ml
+++ b/helm/software/components/acic_content/content2cic.ml
@@ -70,17 +70,22 @@ let proof2cic deannotate p =
             | None -> 
                 C.Lambda (C.Anonymous, deannotate h.Con.dec_type, target))
       | `Proof p -> 
+          let ty =
+           match p.Con.proof_conclude.Con.conclude_conclusion with
+              None -> (*Cic.Implicit None*) assert false
+            | Some ty -> deannotate ty
+          in
           (match p.Con.proof_name with
               Some s ->
-                C.LetIn (C.Name s, proof2cic premise_env p, target)
+                C.LetIn (C.Name s, proof2cic premise_env p, ty , target)
             | None -> 
-                C.LetIn (C.Anonymous, proof2cic premise_env p, target)) 
+                C.LetIn (C.Anonymous, proof2cic premise_env p, ty, target)) 
       | `Definition d -> 
            (match d.Con.def_name with
               Some s ->
-                C.LetIn (C.Name s, proof2cic premise_env p, target)
+                C.LetIn (C.Name s, proof2cic premise_env p, deannotate d.Con.def_type, target)
             | None -> 
-                C.LetIn (C.Anonymous, proof2cic premise_env p, target)) 
+                C.LetIn (C.Anonymous, proof2cic premise_env p, deannotate d.Con.def_type, target)) 
       | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} -> 
             (match target with
                C.Rel n ->
@@ -141,7 +146,7 @@ let proof2cic deannotate p =
        | _ -> prerr_endline "2"; assert false)
     else if conclude.Con.conclude_method = "Exact" then
       (match conclude.Con.conclude_args with
-         [Con.Term t] -> deannotate t
+         [Con.Term (_,t)] -> deannotate t
        | [Con.Premise prem] -> 
            (match prem.Con.premise_n with
               None -> assert false
@@ -156,7 +161,7 @@ let proof2cic deannotate p =
              conclude.Con.conclude_method = "Exists" ||
              conclude.Con.conclude_method = "FalseInd") then
       (match (List.tl conclude.Con.conclude_args) with
-         Con.Term (C.AAppl (
+         Con.Term (_,C.AAppl (
             id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args ->
            let subst =
              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in 
@@ -166,7 +171,7 @@ let proof2cic deannotate p =
        | _ -> prerr_endline "5"; assert false)
     else if (conclude.Con.conclude_method = "Rewrite") then
       (match conclude.Con.conclude_args with
-         Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
+         Con.Term (_,C.AConst (sid,uri,exp_named_subst))::args ->
            let subst =
              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
            let  cargs = args2cic premise_env args in
@@ -174,7 +179,7 @@ let proof2cic deannotate p =
        | _ -> prerr_endline "6"; assert false)
     else if (conclude.Con.conclude_method = "Case") then
       (match conclude.Con.conclude_args with
-        Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns ->
+        Con.Aux(uri)::Con.Aux(notype)::Con.Term(_,ty)::Con.Premise(prem)::patterns ->
            C.MutCase
             (UriManager.uri_of_string uri,
              int_of_string notype, deannotate ty, 
@@ -183,7 +188,7 @@ let proof2cic deannotate p =
                (function 
                    Con.ArgProof p -> proof2cic [] p
                  | _ -> prerr_endline "7a"; assert false) patterns)
-      | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns ->           C.MutCase
+      | Con.Aux(uri)::Con.Aux(notype)::Con.Term(_,ty)::Con.Term(_,te)::patterns ->           C.MutCase
             (UriManager.uri_of_string uri,
              int_of_string notype, deannotate ty, deannotate te,
              List.map 
@@ -214,7 +219,7 @@ let proof2cic deannotate p =
                   raise Not_found))
       | Con.Lemma lemma ->
          CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri)
-      | Con.Term t -> deannotate t
+      | Con.Term (_,t) -> deannotate t
       | Con.ArgProof p -> proof2cic [] p (* empty! *)
       | Con.ArgMethod s -> raise TO_DO
 
@@ -247,14 +252,14 @@ let cobj2obj deannotate (id,params,metasenv,obj) =
                       | _ -> assert false)
                    | Some (`Definition d) ->
                       (match d with
-                          {K.def_name = Some n ; K.def_term = t} ->
-                            Some (Cic.Name n, Cic.Def ((deannotate t),None))
+                          {K.def_name = Some n ; K.def_term = t ; K.def_type = ty} ->
+                            Some (Cic.Name n, Cic.Def (deannotate t,deannotate ty))
                         | _ -> assert false)
                    | Some (`Proof d) ->
                       (match d with
                           {K.proof_name = Some n } ->
                             Some (Cic.Name n,
-                              Cic.Def ((proof2cic deannotate d),None))
+                              Cic.Def ((proof2cic deannotate d),assert false))
                         | _ -> assert false)
                  ) canonical_context
                in