From: Claudio Sacerdoti Coen Date: Thu, 24 Apr 2008 16:22:17 +0000 (+0000) Subject: When going under a binder, a term must be converted twice, as explained in the X-Git-Tag: make_still_working~5287 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=97e4383bf560f98edf3ea57e9e10e140070300ac;p=helm.git 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 ae597f417..6252842ff 100644 --- 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),