parameter sintax added to axiom statement

[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 f04f5aa10e1197ea61c8338e3a39a01968083346..c560af569e031f54a7e37baec625c950fae7d314 100644 (file)
--- a/helm/software/components/cic/deannotate.ml
+++ b/helm/software/components/cic/deannotate.ml
@@ -51,8 +51,8 @@ let rec deannotate_term =
       C.Prod (name, deannotate_term so, deannotate_term ta)
    | C.ALambda (_,name,so,ta) ->
       C.Lambda (name, deannotate_term so, deannotate_term ta)
-   | C.ALetIn (_,name,so,ta) ->
-      C.LetIn (name, deannotate_term so, deannotate_term ta)
+   | C.ALetIn (_,name,so,ty,ta) ->
+      C.LetIn (name, deannotate_term so, deannotate_term ty, deannotate_term ta)
    | C.AAppl (_,l) -> C.Appl (List.map deannotate_term l)
    | C.AConst (_,uri,exp_named_subst) ->
       let deann_exp_named_subst =
@@ -89,7 +89,120 @@ let deannotate_inductiveType (_, name, isinductive, arity, cons) =
   List.map (fun (id,ty) -> (id,deannotate_term ty)) cons)
 ;;
 
+let deannotate_conjectures =
+ let module C = Cic in
+  List.map
+   (function 
+     (_,id,acontext,con) -> 
+      let context = 
+       List.map 
+        (function 
+          | _,Some (n,(C.ADef (ate,aty))) ->
+             Some(n,(C.Def(deannotate_term ate,deannotate_term aty)))
+          | _,Some (n,(C.ADecl at)) -> Some (n,(C.Decl (deannotate_term at)))
+          | _,None -> None)
+        acontext  
+      in
+       (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) ->
@@ -103,21 +216,7 @@ let deannotate_obj =
    | C.ACurrentProof (_, _, name, conjs, bo, ty, params, attrs) ->
       C.CurrentProof (
        name,
-        List.map
-         (function 
-           (_,id,acontext,con) -> 
-           let context = 
-            List.map 
-             (function 
-                 _,Some (n,(C.ADef at)) ->
-                   Some (n,(C.Def ((deannotate_term at),None)))
-               | _,Some (n,(C.ADecl at)) ->
-                   Some (n,(C.Decl (deannotate_term at)))
-               | _,None -> None
-              ) acontext  
-            in
-            (id,context,deannotate_term con) 
-         ) conjs,
+       deannotate_conjectures conjs,
        deannotate_term bo,deannotate_term ty, params, attrs
       )
    | C.AInductiveDefinition (_, tys, params, parno, attrs) ->