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

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index dd91bbc320ce9206b8e884289c0231eed6fe0493..1d0e453b006457909f1bb6a5c55fe33c27c4667e 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -30,7 +30,7 @@ let context_tassonomy ctx =
       split true 0 1 ctx
 ;;
 
-let splat_args ctx t = 
+let splat_args_for_rel ctx t = 
   let bound, free, primo_ce_dopo_fix = context_tassonomy ctx in
   if free = 0 then t 
   else
@@ -38,12 +38,29 @@ let splat_args ctx t =
       | 0 -> []
       | n -> 
          (match List.nth ctx (n+bound) with
-         | Fix (refe, _, _) when (n+bound) < primo_ce_dopo_fix -> (NCic.Const refe)
+         | Fix (refe, _, _) when (n+bound) < primo_ce_dopo_fix -> NCic.Const refe
          | Fix _ | Ce _ -> NCic.Rel (n+bound)) :: aux (n-1)
     in
     NCic.Appl (t:: aux free)
 ;;
 
+let splat_args ctx t n_fix = 
+  let bound, free, primo_ce_dopo_fix = context_tassonomy ctx in
+  if ctx = [] then t
+  else
+   let rec aux = function
+     | 0 -> []
+     | n -> 
+        (match List.nth ctx (n-1) with
+         | Ce _ when n <= bound -> NCic.Rel n
+         | Fix (refe, _, _) when n < primo_ce_dopo_fix ->
+            splat_args_for_rel ctx (NCic.Const refe)
+         | Fix _ | Ce _ -> NCic.Rel (n - n_fix)
+        ) :: aux (n-1)
+   in
+   NCic.Appl (t:: aux (List.length ctx))
+;;
+
 (* we are lambda-lifting also variables that do not occur *)
 (* ctx does not distinguish successive blocks of cofix, since there may be no
  *   lambda separating them *)
@@ -83,8 +100,9 @@ let convert_term uri t =
           NUri.nuri_of_ouri buri,0,[],[],
             NCic.Fixpoint (false, fl, (`Generated, `Definition)) 
         in
-        splat_args bctx 
-         (NCic.Const (NReference.reference_of_ouri buri (NReference.CoFix k))),
+        splat_args ctx 
+         (NCic.Const (NReference.reference_of_ouri buri (NReference.CoFix k)))
+         n_fix,
         fixpoints @ [obj]
     | Cic.Fix (k, fl) ->
         let buri = 
@@ -126,15 +144,16 @@ let convert_term uri t =
           NUri.nuri_of_ouri buri,0,[],[],
             NCic.Fixpoint (true, fl, (`Generated, `Definition)) 
         in
-        splat_args bctx
+        splat_args ctx
           (NCic.Const 
-            (NReference.reference_of_ouri buri (NReference.Fix (k,!rno)))),
+            (NReference.reference_of_ouri buri (NReference.Fix (k,!rno))))
+          n_fix,
         fixpoints @ [obj]
     | Cic.Rel n ->
         let bound, _, primo_ce_dopo_fix = context_tassonomy ctx in
         (match List.nth ctx (n-1) with
         | Fix (r,_,_) when n < primo_ce_dopo_fix -> 
-            splat_args ctx (NCic.Const r), []
+            splat_args_for_rel ctx (NCic.Const r), []
         | Ce _ when n <= bound -> NCic.Rel n, []
         | Fix _ (* BUG 3 fix nested *) 
         | Ce _ -> NCic.Rel (n-n_fix), [])