splat_args is now better understood and debugged: we need TWO splat_args, one when

the term is a Rel (that skips the bound variables) and one when the term is a Fix
(that passes bound variables around).

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index dd91bbc320ce9206b8e884289c0231eed6fe0493..0d00f031f18c558cbba117337fe7bda33ca8c440 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,27 @@ 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
+  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 +98,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 +142,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), [])

diff --git a/helm/software/components/ng_kernel/rt.ml b/helm/software/components/ng_kernel/rt.ml
index 74ed2eed99a43d64b5084897bef853b322aaf7e5..e7ecaf3aff49e559fa60e8b7d571075689ef6ed2 100644 (file)
--- a/helm/software/components/ng_kernel/rt.ml
+++ b/helm/software/components/ng_kernel/rt.ml
@@ -12,6 +12,7 @@ let _ =
      prerr_endline (CicPp.ppobj o);
      try CicTypeChecker.typecheck_obj u o
      with CicTypeChecker.TypeCheckerFailure s ->
-       prerr_endline (Lazy.force s)) 
+       prerr_endline (Lazy.force s)
+     | CicEnvironment.Object_not_found _ -> ()) 
    objs;
 ;;

diff --git a/helm/software/components/ng_kernel/test.ma b/helm/software/components/ng_kernel/test.ma
index e1c496ca3a028bcfce377f65cb8cbb94bca3f2c3..95c919854b46a9d6ed96ad5d71c4cad4555ca702 100644 (file)
--- a/helm/software/components/ng_kernel/test.ma
+++ b/helm/software/components/ng_kernel/test.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "nat/nat.ma".
+include "nat/plus.ma".
 
 let rec f n := 
   match n with
@@ -20,4 +20,12 @@ let rec f n :=
   | S m => let rec g x := 
              match x with
              [ O => f m
-             | S q => g q] in g m].
\ No newline at end of file
+             | S q => 
+                  let rec h y := 
+                    match y with 
+                    [ O => f m + g q
+                    | S w => h w]
+                  in
+                    h q] 
+           in 
+             g m].
\ No newline at end of file