When going under a binder, a term must be converted twice, as explained in the

previous commit. The problem is that in this way the complexity of the
translation becomes O(2^n) when n is the maximum depth of binders. However,
this computation is completely unuseful if no (co)fix is found in the term.
This commits adds as much lazyness as possible to fix the issue.

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index ae597f417e47b0783bda100b74bbcce066873ad4..6252842ff0a4d6f7c2d8ff9a1596f8f36e457215 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -1,8 +1,14 @@
 module Ref = NReference
 
 type ctx = 
-  | Ce of NCic.hypothesis * NCic.obj list
-  | Fix of Ref.reference * string * NCic.term
+  | Ce of (NCic.hypothesis * NCic.obj list) Lazy.t
+  | Fix of (Ref.reference * string * NCic.term) Lazy.t
+
+let strictify =
+ function
+    Ce l -> `Ce (Lazy.force l)
+  | Fix l -> `Fix (Lazy.force l)
+;;
 
 (***** A function to restrict the context of a term getting rid of unsed
        variables *******)
@@ -18,15 +24,15 @@ let restrict octx ctx ot =
        aux (m+1) acc (CicSubstitution.subst odummy ot)
         (NCicSubstitution.subst dummy t) (otl,tl)
       else
-       (match ohe,he with
+       (match ohe,strictify he with
            None,_ -> assert false
-         | Some (name,Cic.Decl oty),Ce ((name', NCic.Decl ty),objs) ->
+         | Some (name,Cic.Decl oty),`Ce ((name', NCic.Decl ty),objs) ->
             aux (m+1) ((m+1,objs,None)::acc) (Cic.Lambda (name,oty,ot))
              (NCic.Lambda (name',ty,t)) (otl,tl)
-         | Some (name,Cic.Decl oty),Fix (ref,name',ty) ->
+         | Some (name,Cic.Decl oty),`Fix (ref,name',ty) ->
             aux (m+1) ((m+1,[],Some ref)::acc) (Cic.Lambda (name,oty,ot))
              (NCic.Lambda (name',ty,t)) (otl,tl)
-         | Some (name,Cic.Def (obo,oty)),Ce ((name', NCic.Def (bo,ty)),objs) ->
+         | Some (name,Cic.Def (obo,oty)),`Ce ((name', NCic.Def (bo,ty)),objs) ->
             aux (m+1) ((m+1,objs,None)::acc) (Cic.LetIn (name,obo,oty,ot))
              (NCic.LetIn (name',bo,ty,t)) (otl,tl)
          | _,_ -> assert false)
@@ -36,13 +42,13 @@ let restrict octx ctx ot =
      ([], _, _) -> octx,ctx,ote
    | ((_,objs,None)::tl, Cic.Lambda(name,oso,ota), NCic.Lambda(name',so,ta)) ->
        split_lambdas_and_letins ((Some(name,(Cic.Decl oso)))::octx)
-        (Ce ((name',NCic.Decl so),objs)::ctx) tl (ota,ta)
+        (Ce (lazy ((name',NCic.Decl so),objs))::ctx) tl (ota,ta)
    | ((_,objs,Some r)::tl,Cic.Lambda(name,oso,ota),NCic.Lambda(name',so,ta)) ->
        split_lambdas_and_letins ((Some(name,(Cic.Decl oso)))::octx)
-        (Fix (r,name',so)::ctx) tl (ota,ta)
+        (Fix (lazy (r,name',so))::ctx) tl (ota,ta)
    | ((_,objs,None)::tl,Cic.LetIn(name,obo,oty,ota),NCic.LetIn(nam',bo,ty,ta))->
        split_lambdas_and_letins ((Some (name,(Cic.Def (obo,oty))))::octx)
-        (Ce ((nam',NCic.Def (bo,ty)),objs)::ctx) tl (ota,ta)
+        (Ce (lazy ((nam',NCic.Def (bo,ty)),objs))::ctx) tl (ota,ta)
    | (_, _, _) -> assert false
  in
   let long_t,infos = aux 0 [] ot dummy (octx,ctx) in
@@ -65,12 +71,12 @@ let cn_to_s = function
 let splat mk_pi ctx t =
   List.fold_left
     (fun (t,l) c -> 
-      match c with
-      | Ce ((name, NCic.Def (bo,ty)),l') -> NCic.LetIn (name, ty, bo, t),l@l'
-      | Ce ((name, NCic.Decl ty),l') when mk_pi -> NCic.Prod (name, ty, t),l@l'
-      | Ce ((name, NCic.Decl ty),l') -> NCic.Lambda (name, ty, t),l@l'
-      | Fix (_,name,ty) when mk_pi -> NCic.Prod (name, ty, t),l
-      | Fix (_,name,ty) -> NCic.Lambda (name,ty,t),l)
+      match strictify c with
+      | `Ce ((name, NCic.Def (bo,ty)),l') -> NCic.LetIn (name, ty, bo, t),l@l'
+      | `Ce ((name, NCic.Decl ty),l') when mk_pi -> NCic.Prod (name, ty, t),l@l'
+      | `Ce ((name, NCic.Decl ty),l') -> NCic.Lambda (name, ty, t),l@l'
+      | `Fix (_,name,ty) when mk_pi -> NCic.Prod (name, ty, t),l
+      | `Fix (_,name,ty) -> NCic.Lambda (name,ty,t),l)
     (t,[]) ctx
 ;;
 
@@ -79,11 +85,16 @@ let context_tassonomy ctx =
       | Ce _ :: tl when inner -> split inner (acc+1) (acc1+1) tl
       | Fix _ ::tl -> split false acc (acc1+1) tl
       | _ as l ->
-        let only_decl =
+        let only_decl () =
          List.filter
-          (function Ce ((_, NCic.Decl _),_) | Fix _ -> true | _ -> false) l
+          (function
+              Ce _ as ce ->
+               (match strictify ce with
+                   `Ce ((_, NCic.Decl _),_) -> true
+                 | _ -> false)
+            | Fix _ -> true) l
         in
-         acc, List.length l, List.length only_decl, acc1
+         acc, List.length l, lazy (List.length (only_decl ())), acc1
     in
       split true 0 1 ctx
 ;;
@@ -102,11 +113,12 @@ let splat_args_for_rel ctx t ?rels n_fix =
     let rec aux = function
       | n,_ when n = bound + n_fix -> []
       | n,he::tl -> 
-         (match List.nth ctx (n-1) with
-          | Fix (refe, _, _) when n < primo_ce_dopo_fix ->
+         (match strictify (List.nth ctx (n-1)) with
+          | `Fix (refe, _, _) when n < primo_ce_dopo_fix ->
              NCic.Const refe :: aux (n-1,tl)
-          | Fix _ | Ce ((_, NCic.Decl _),_)-> NCic.Rel (he - n_fix)::aux(n-1,tl)
-          | Ce ((_, NCic.Def _),_) -> aux (n-1,tl))
+          | `Fix _ | `Ce ((_, NCic.Decl _),_) ->
+              NCic.Rel (he - n_fix)::aux(n-1,tl)
+          | `Ce ((_, NCic.Def _),_) -> aux (n-1,tl))
       | _,_ -> assert false
     in
     NCic.Appl (t:: aux (List.length ctx,rels))
@@ -119,12 +131,13 @@ let splat_args ctx t n_fix rels =
    let rec aux = function
      | 0,[] -> []
      | n,he::tl -> 
-        (match List.nth ctx (n-1) with
-         | Ce ((_, NCic.Decl _),_) when n <= bound -> NCic.Rel he:: aux (n-1,tl)
-         | Fix (refe, _, _) when n < primo_ce_dopo_fix ->
+        (match strictify (List.nth ctx (n-1)) with
+         | `Ce ((_, NCic.Decl _),_) when n <= bound ->
+             NCic.Rel he:: aux (n-1,tl)
+         | `Fix (refe, _, _) when n < primo_ce_dopo_fix ->
             splat_args_for_rel ctx (NCic.Const refe) ~rels n_fix :: aux (n-1,tl)
-         | Fix _ | Ce ((_, NCic.Decl _),_) -> NCic.Rel (he - n_fix)::aux(n-1,tl)
-         | Ce ((_, NCic.Def _),_) -> aux (n - 1,tl)
+         | `Fix _ | `Ce((_, NCic.Decl _),_)-> NCic.Rel (he - n_fix)::aux(n-1,tl)
+         | `Ce ((_, NCic.Def _),_) -> aux (n - 1,tl)
         ) 
      | _,_ -> assert false
    in
@@ -371,7 +384,8 @@ let convert_term uri t =
             (fun (name,ty,_) (bctx, fixpoints, tys, idx) -> 
               let ty, fixpoints_ty = aux true octx ctx n_fix uri ty in
               let r = Ref.reference_of_ouri buri(Ref.CoFix idx) in
-              bctx @ [Fix (r,name,ty)], fixpoints_ty @ fixpoints,ty::tys,idx-1)
+              bctx @ [Fix (lazy (r,name,ty))],
+               fixpoints_ty @ fixpoints,ty::tys,idx-1)
             fl ([], [], [], List.length fl-1)
         in
         let bctx = bctx @ ctx in
@@ -416,15 +430,17 @@ let convert_term uri t =
               let r =  (* recno is dummy here, must be lifted by the ctx len *)
                 Ref.reference_of_ouri buri (Ref.Fix (idx,recno)) 
               in
-              bctx @ [Fix (r,name,ty)], fixpoints_ty@fixpoints,ty::tys,idx-1)
+              bctx @ [Fix (lazy (r,name,ty))],
+               fixpoints_ty@fixpoints,ty::tys,idx-1)
             fl ([], [], [], List.length fl-1)
         in
         let _, _, free_decls, _ = context_tassonomy (bad_bctx @ ctx) in
+        let free_decls = Lazy.force free_decls in
         let bctx = 
-          List.map (function 
-            | Fix (Ref.Ref (_,_,Ref.Fix (idx, recno)),name, ty) ->
-              Fix (Ref.reference_of_ouri buri
-                    (Ref.Fix (idx,recno+free_decls)),name,ty)
+          List.map (function ce -> match strictify ce with
+            | `Fix (Ref.Ref (_,_,Ref.Fix (idx, recno)),name, ty) ->
+              Fix (lazy (Ref.reference_of_ouri buri
+                    (Ref.Fix (idx,recno+free_decls)),name,ty))
             | _ -> assert false) bad_bctx @ ctx
         in
         let n_fl = List.length fl in
@@ -461,7 +477,8 @@ let convert_term uri t =
     | 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 -> 
+        | Fix l when n < primo_ce_dopo_fix -> 
+           let r,_,_ = Lazy.force l in
             splat_args_for_rel ctx (NCic.Const r) n_fix, []
         | Ce _ when n <= bound -> NCic.Rel n, []
         | Fix _ when n <= bound -> assert false
@@ -469,25 +486,35 @@ let convert_term uri t =
         | Fix _ | Ce _ -> NCic.Rel (n-n_fix), [])
     | Cic.Lambda (name, (s as old_s), t) ->
         let s, fixpoints_s = aux k octx ctx n_fix uri s in
-        let s', fixpoints_s' = aux true octx ctx n_fix uri old_s in
-        let ctx = Ce ((cn_to_s name, NCic.Decl s'),fixpoints_s') :: ctx in
+        let s'_and_fixpoints_s' = lazy (aux true octx ctx n_fix uri old_s) in
+        let ctx =
+         Ce (lazy
+          let s',fixpoints_s' = Lazy.force s'_and_fixpoints_s' in
+           ((cn_to_s name, NCic.Decl s'),fixpoints_s'))::ctx in
         let octx = Some (name, Cic.Decl old_s) :: octx in
         let t, fixpoints_t = aux k octx ctx n_fix uri t in
         NCic.Lambda (cn_to_s name, s, t), fixpoints_s @ fixpoints_t
     | Cic.Prod (name, (s as old_s), t) ->
         let s, fixpoints_s = aux k octx ctx n_fix uri s in
-        let s', fixpoints_s' = aux true octx ctx n_fix uri old_s in
-        let ctx = Ce ((cn_to_s name, NCic.Decl s'),fixpoints_s') :: ctx in
+        let s'_and_fixpoints_s' = lazy (aux true octx ctx n_fix uri old_s) in
+        let ctx =
+         Ce (lazy
+          let s',fixpoints_s' = Lazy.force s'_and_fixpoints_s' in
+           ((cn_to_s name, NCic.Decl s'),fixpoints_s'))::ctx in
         let octx = Some (name, Cic.Decl old_s) :: octx in
         let t, fixpoints_t = aux k octx ctx n_fix uri t in
         NCic.Prod (cn_to_s name, s, t), fixpoints_s @ fixpoints_t
     | Cic.LetIn (name, (te as old_te), (ty as old_ty), t) ->
         let te, fixpoints_s = aux k octx ctx n_fix uri te in
-        let te', fixpoints_s' = aux true octx ctx n_fix uri old_te in
+        let te_and_fixpoints_s' = lazy (aux true octx ctx n_fix uri old_te) in
         let ty, fixpoints_ty = aux k octx ctx n_fix uri ty in
-        let ty', fixpoints_ty' = aux true octx ctx n_fix uri old_ty in
-        let fixpoints' = fixpoints_s' @ fixpoints_ty' in
-        let ctx = Ce ((cn_to_s name, NCic.Def (te', ty')),fixpoints') :: ctx in
+        let ty_and_fixpoints_ty' = lazy (aux true octx ctx n_fix uri old_ty) in
+        let ctx =
+         Ce (lazy
+          let te',fixpoints_s' = Lazy.force te_and_fixpoints_s' in
+          let ty',fixpoints_ty' = Lazy.force ty_and_fixpoints_ty' in
+          let fixpoints' = fixpoints_s' @ fixpoints_ty' in
+           ((cn_to_s name, NCic.Def (te', ty')),fixpoints'))::ctx in
         let octx = Some (name, Cic.Def (old_te, old_ty)) :: octx in
         let t, fixpoints_t = aux k octx ctx n_fix uri t in
         NCic.LetIn (cn_to_s name, ty, te, t),