some improvements

[helm.git] / helm / software / components / cic_acic / cic2acic.ml

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index d8392f6206ab745e2647a75286e30745e481e18a..89d3d00b410b10c92495716812a8b12cf2423ef9 100644 (file)
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -82,16 +82,16 @@ let fresh_id seed ids_to_terms ids_to_father_ids =
 
 let source_id_of_id id = "#source#" ^ id;;
 
-exception NotEnoughElements;;
+exception NotEnoughElements of string;;
 
 (*CSC: cut&paste da cicPp.ml *)
 (* get_nth l n   returns the nth element of the list l if it exists or *)
 (* raises NotEnoughElements if l has less than n elements             *)
-let rec get_nth l n =
+let rec get_nth msg l n =
  match (n,l) with
     (1, he::_) -> he
-  | (n, he::tail) when n > 1 -> get_nth tail (n-1)
-  | (_,_) -> raise NotEnoughElements
+  | (n, he::tail) when n > 1 -> get_nth msg tail (n-1)
+  | (_,_) -> raise (NotEnoughElements msg)
 ;;
 
 
@@ -224,7 +224,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
          match tt with
             C.Rel n ->
              let id =
-              match get_nth context n with
+              match get_nth "1" context n with
                  (Some (C.Name s,_)) -> s
                | _ -> "__" ^ string_of_int n
              in
@@ -353,8 +353,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
              let fresh_idrefs =
               List.map (function _ -> gen_id seed) funs in
              let new_idrefs = List.rev fresh_idrefs @ idrefs in
-             let tys =
-              List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
+             let tys,_ =
+               List.fold_left
+                 (fun (types,len) (n,_,ty,_) ->
+                    (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                     len+1)
+                ) ([],0) funs
              in
               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
               if innersort = `Prop then
@@ -370,8 +374,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
              let fresh_idrefs =
               List.map (function _ -> gen_id seed) funs in
              let new_idrefs = List.rev fresh_idrefs @ idrefs in
-             let tys =
-              List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
+             let tys,_ =
+               List.fold_left
+                 (fun (types,len) (n,ty,_) ->
+                    (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                     len+1)
+                ) ([],0) funs
              in
               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
               if innersort = `Prop then
@@ -635,7 +643,7 @@ let plain_acic_term_of_cic_term =
   match t with
      C.Rel n ->
       let idref,id =
-       match get_nth context n with
+       match get_nth "2" context n with
           idref,(Some (C.Name s,_)) -> idref,s
         | idref,_ -> idref,"__" ^ string_of_int n
       in
@@ -687,9 +695,12 @@ let plain_acic_term_of_cic_term =
       C.AMutCase (fresh_id, uri, tyno, aux context outty,
        aux context term, List.map (aux context) patterns)
    | C.Fix (funno, funs) ->
-      let tys =
-       List.map
-        (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs
+      let tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+            (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types,
+              len+1
+         ) ([],0) funs
       in
        C.AFix (fresh_id, funno,
         List.map2
@@ -698,9 +709,12 @@ let plain_acic_term_of_cic_term =
          ) tys funs
       )
    | C.CoFix (funno, funs) ->
-      let tys =
-       List.map (fun (name,ty,_) ->
-        mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs
+      let tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+            (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types,
+              len+1
+         ) ([],0) funs
       in
        C.ACoFix (fresh_id, funno,
         List.map2