:-(

This commit introduces an hack in deannotate.ml to compute on-the-fly the types
for the body in a LetIn parsed from an XML file. This happens when parsing Coq
files. We should re-export everything from Coq sooner or later.

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index 3d1d3d1aa05ccbcd1ee313d8574b870b09fad3bd..9fac7badba3a10e0b8eb166df6ca67d88ff31bc0 100644 (file)
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -406,8 +406,15 @@ let end_element ctxt tag =
         | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
         | _ -> attribute_error ())
   | "def" ->  (* same as "decl" above *)
-      let ty = pop_cic ctxt in
-      let source = pop_cic ctxt in
+      let ty,source =
+       (*CSC: hack to parse Coq files where the LetIn is not typed *)
+       let ty = pop_cic ctxt in
+       try
+        let source = pop_cic ctxt in
+         ty,source
+       with
+        Parser_failure _ -> Cic.AImplicit ("MISSING_def_TYPE",None),ty
+      in
       push ctxt
         (match pop_tag_attrs ctxt with
         | ["binder", binder; "id", id]

diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml
index f1dfbffed6614ef7c419bbe071d4fe1abde99ffa..69eccd9b9897dec7044791e0979a1c07bbe74760 100644 (file)
--- a/helm/software/components/cic/deannotate.ml
+++ b/helm/software/components/cic/deannotate.ml
@@ -106,7 +106,100 @@ let deannotate_conjectures =
        (id,context,deannotate_term con))
 ;;
 
+let type_of_aux' = ref (fun _ _ -> assert false);;
+let lift  = ref (fun _ _ -> assert false);;
+
+let rec compute_letin_type context te =
+ let module C = Cic in
+   match te with
+      C.Rel _
+    | C.Sort _ -> te
+    | C.Implicit _ -> assert false
+    | C.Meta (n,l) ->
+       C.Meta (n,
+        List.map
+        (fun x ->
+          match x with
+             None -> None
+           | Some x -> Some (compute_letin_type context x)) l)
+    | C.Cast (te,ty) ->
+       C.Cast
+        (compute_letin_type context te,
+         compute_letin_type context ty)
+    | C.Prod (name,so,dest) ->
+       C.Prod (name,
+        compute_letin_type context so,
+        compute_letin_type ((Some (name,(C.Decl so)))::context) dest)
+    | C.Lambda (name,so,dest) ->
+       C.Lambda (name,
+        compute_letin_type context so,
+        compute_letin_type ((Some (name,(C.Decl so)))::context) dest)
+    | C.LetIn (name,so,C.Implicit _,dest) ->
+       let ty = !type_of_aux' context so in
+        C.LetIn (name,
+         compute_letin_type context so,
+         ty,
+         compute_letin_type ((Some (name,(C.Def (so,ty))))::context) dest)
+    | C.LetIn (name,so,ty,dest) ->
+       C.LetIn (name,
+        compute_letin_type context so,
+        compute_letin_type context ty,
+        compute_letin_type ((Some (name,(C.Def (so,ty))))::context) dest)
+    | C.Appl l ->
+       C.Appl (List.map (fun x -> compute_letin_type context x) l)
+    | C.Var (uri,exp_named_subst) -> 
+       C.Var (uri,
+        List.map (fun (u,x) -> u,compute_letin_type context x) exp_named_subst)
+    | C.Const (uri,exp_named_subst) ->
+       C.Const (uri,
+        List.map (fun (u,x) -> u,compute_letin_type context x) exp_named_subst)
+    | C.MutInd (uri,i,exp_named_subst) ->
+       C.MutInd (uri,i,
+        List.map (fun (u,x) -> u,compute_letin_type context x) exp_named_subst)
+    | C.MutConstruct (uri,i,j,exp_named_subst) ->
+       C.MutConstruct (uri,i,j,
+        List.map (fun (u,x) -> u,compute_letin_type context x) exp_named_subst)
+    | C.MutCase (uri,i,out,te,pl) ->
+       C.MutCase (uri,i,
+        compute_letin_type context out,
+        compute_letin_type context te,
+        List.map (fun x -> compute_letin_type context x) pl)
+    | C.Fix (fno,fl) ->
+        let tys,_ =
+         List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (!lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
+        in
+         C.Fix (fno,
+          List.map
+           (fun (name,recno,ty,bo) ->
+             name, recno,
+             compute_letin_type context ty,
+             compute_letin_type (tys @ context) bo
+           ) fl)
+    | C.CoFix (fno,fl) ->
+        let tys,_ =
+         List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (!lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
+        in
+         C.CoFix (fno,
+          List.map
+           (fun (name,ty,bo) ->
+             name,
+             compute_letin_type context ty,
+             compute_letin_type (tys @ context) bo
+           ) fl)
+;;
+
 let deannotate_obj =
+ let deannotate_term t =
+   compute_letin_type [] (deannotate_term t)
+ in
  let module C = Cic in
   function
      C.AConstant (_, _, id, bo, ty, params, attrs) ->

diff --git a/helm/software/components/cic/deannotate.mli b/helm/software/components/cic/deannotate.mli
index 1e29b5b648ded189030f098707b2496156b7573d..f4fdd2d5d59e918a53217323cd79c2f397417a9c 100644 (file)
--- a/helm/software/components/cic/deannotate.mli
+++ b/helm/software/components/cic/deannotate.mli
@@ -32,6 +32,9 @@
 (*                                                                            *)
 (******************************************************************************)
 
+val type_of_aux' : (Cic.context -> Cic.term -> Cic.term) ref
+val lift : (int -> Cic.term -> Cic.term) ref
+
 val deannotate_term : Cic.annterm -> Cic.term
 val deannotate_conjectures : Cic.annmetasenv -> Cic.metasenv
 val deannotate_obj : Cic.annobj -> Cic.obj

diff --git a/helm/software/components/cic_proof_checking/cicSubstitution.ml b/helm/software/components/cic_proof_checking/cicSubstitution.ml
index 4f888a3a5b35bb12e1d3667967346d402250c4ba..8d1dad9e2c2af09ccded670260c3b9c0b8971927 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicSubstitution.ml
+++ b/helm/software/components/cic_proof_checking/cicSubstitution.ml
@@ -440,3 +440,4 @@ let subst_meta l t =
   aux 0 t          
 ;;
 
+Deannotate.lift := lift;;

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index c23555494f803e279be20f54bf85c51b94c4d244..7b98a59be775fe79e02ec35f3e7e497c694554b0 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -2303,3 +2303,6 @@ let check_allowed_sort_elimination uri i s1 s2 =
   ~logger:(new CicLogger.logger) [] uri i true
   (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
   CicUniv.empty_ugraph)
+;;
+
+Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;