cicDischarge: new module for discharging the explicit variables occurring in a

[helm.git] / helm / software / components / cic / deannotate.ml

diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml
index f1dfbffed6614ef7c419bbe071d4fe1abde99ffa..c560af569e031f54a7e37baec625c950fae7d314 100644 (file)
--- a/helm/software/components/cic/deannotate.ml
+++ b/helm/software/components/cic/deannotate.ml
@@ -106,7 +106,103 @@ 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) ->
+       let so = compute_letin_type context so in
+       C.Prod (name, so,
+        compute_letin_type ((Some (name,(C.Decl so)))::context) dest)
+    | C.Lambda (name,so,dest) ->
+       let so = compute_letin_type context so in
+       C.Lambda (name, so,
+        compute_letin_type ((Some (name,(C.Decl so)))::context) dest)
+    | C.LetIn (name,so,C.Implicit _,dest) ->
+       let so = compute_letin_type context so in
+       let ty = Unshare.unshare ~fresh_univs:true (!type_of_aux' context so) in
+        C.LetIn (name, so, ty,
+         compute_letin_type ((Some (name,(C.Def (so,ty))))::context) dest)
+    | C.LetIn (name,so,ty,dest) ->
+       let so = compute_letin_type context so in
+       let ty = compute_letin_type context ty in
+       C.LetIn (name, so, 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 fl =
+         List.map
+          (function (name,recno,ty,bo) ->
+            name,recno,compute_letin_type context ty, bo) fl in
+        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, ty, compute_letin_type (tys @ context) bo
+           ) fl)
+    | C.CoFix (fno,fl) ->
+        let fl =
+         List.map
+          (function (name,ty,bo) ->
+            name, compute_letin_type context ty, bo) fl in
+        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, 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) ->