From 5ba3b166fff4398b031774b52bd7c1ae1e5be09b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 31 Mar 2008 14:10:21 +0000 Subject: [PATCH] 1) more sharing everywhere in NCicSubstitution 2) type of iterators in nCicUtils changed to take a NCic.hypothesis when crossing binders --- .../components/ng_kernel/nCicSubstitution.ml | 145 +++++------------- .../components/ng_kernel/nCicUtils.ml | 31 ++-- .../components/ng_kernel/nCicUtils.mli | 12 +- 3 files changed, 68 insertions(+), 120 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml index 3d05948b1..2be7f5871 100644 --- a/helm/software/components/ng_kernel/nCicSubstitution.ml +++ b/helm/software/components/ng_kernel/nCicSubstitution.ml @@ -15,36 +15,15 @@ let debug_print = fun _ -> ();; let lift_from k n = let rec liftaux k = function - | NCic.Rel m as t -> - if m < k then t - else NCic.Rel (m + n) - | NCic.Meta (i,(m,l)) when k <= m -> NCic.Meta (i,(m+n,l)) + | NCic.Rel m as t -> if m < k then t else NCic.Rel (m + n) + | NCic.Meta (i,(m,l)) as t when k <= m -> + if n = 0 then t else NCic.Meta (i,(m+n,l)) | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t | NCic.Meta (i,(m,l)) -> let lctx = NCicUtils.expand_local_context l in - NCic.Meta (i, (m, NCic.Ctx (List.map (liftaux (k-m)) lctx))) + NCic.Meta (i, (m, NCic.Ctx (NCicUtils.sharing_map (liftaux (k-m)) lctx))) | NCic.Implicit _ -> (* was the identity *) assert false - | t -> NCicUtils.map liftaux ((+) 1) k t - (* - | NCic.Const _ - | NCic.Sort _ as t -> t - | NCic.Rel m -> - if m < k then NCic.Rel m - else NCic.Rel (m + n) - | NCic.Meta (i,(m,l)) when k <= m -> NCic.Meta (i,(m+n,l)) - | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t - | NCic.Meta (i,(m,l)) -> - let lctx = NCicUtils.expand_local_context l in - NCic.Meta (i, (m, NCic.Ctx (List.map (liftaux (k-m)) lctx))) - | NCic.Implicit _ -> (* was the identity *) assert false - | NCic.Prod (n,s,t) -> NCic.Prod (n, liftaux k s, liftaux (k+1) t) - | NCic.Lambda (n,s,t) -> NCic.Lambda (n, liftaux k s, liftaux (k+1) t) - | NCic.LetIn (n,ty,te,t) -> - NCic.LetIn (n, liftaux k ty, liftaux k te, liftaux (k+1) t) - | NCic.Appl l -> NCic.Appl (List.map (liftaux k) l) - | NCic.Match (r,outty,t,pl) -> - NCic.Match (r,liftaux k outty,liftaux k t, List.map (liftaux k) pl) - *) + | t -> NCicUtils.map (fun _ k -> k + 1) k liftaux t in liftaux k ;; @@ -64,85 +43,41 @@ let lift ?(from=1) n t = let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args = let nargs = List.length args in let rec substaux k = function - | NCic.Rel n as t -> - (match n with - | n when n >= (k+nargs) -> if delift then NCic.Rel (n - nargs) else t - | n when n < k -> t - | n (* k <= n < k+nargs *) -> - (try lift (k+lift_args) (map_arg (List.nth args (n-k))) - with Failure _ -> assert false)) - | NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> - if delift then NCic.Meta (i,(m-nargs,l)) else t - | NCic.Meta (i,(m,(NCic.Irl l as irl))) as t when k > l + m -> - if delift then NCic.Meta (i,(m-nargs,irl)) else t - | NCic.Meta (i,(m,l)) -> - let lctx = NCicUtils.expand_local_context l in - (* 1-nargs < k-m, when <= 0 is still reasonable because we will - * substitute args[ k-m ... k-m+nargs-1 > 0 ] *) - NCic.Meta (i,(m, NCic.Ctx (List.map (substaux (k-m)) lctx))) - | NCic.Implicit _ -> assert false (* was identity *) - | NCic.Appl (he::tl) -> - (* Invariant: no Appl applied to another Appl *) - let rec avoid he = function - | [] -> he - | arg::tl as args-> - (match he with - | NCic.Appl l -> NCic.Appl (l@args) - | NCic.Lambda (_,_,bo) when avoid_beta_redexes -> - (* map_arg is here \x.x, Obj magic is needed because - * we don't have polymorphic recursion w/o records *) - avoid (psubst - ~avoid_beta_redexes true 0 Obj.magic [Obj.magic arg] bo) tl - | _ as he -> NCic.Appl (he::args)) - in - let tl = List.map (substaux k) tl in - avoid (substaux k he) tl - | NCic.Appl _ -> assert false - | t -> NCicUtils.map substaux ((+) 1) k t - (* - | NCic.Sort _ - | NCic.Const _ as t -> t - | NCic.Rel n as t -> - (match n with - | n when n >= (k+nargs) -> if delift then NCic.Rel (n - nargs) else t - | n when n < k -> t - | n (* k <= n < k+nargs *) -> - (try lift (k+lift_args) (map_arg (List.nth args (n-k))) - with Failure _ -> assert false)) - | NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> - if delift then NCic.Meta (i,(m-nargs,l)) else t - | NCic.Meta (i,(m,(NCic.Irl l as irl))) as t when k > l + m -> - if delift then NCic.Meta (i,(m-nargs,irl)) else t - | NCic.Meta (i,(m,l)) -> - let lctx = NCicUtils.expand_local_context l in - (* 1-nargs < k-m, when <= 0 is still reasonable because we will - * substitute args[ k-m ... k-m+nargs-1 > 0 ] *) - NCic.Meta (i,(m, NCic.Ctx (List.map (substaux (k-m)) lctx))) - | NCic.Implicit _ -> assert false (* was identity *) - | NCic.Prod (n,s,t) -> NCic.Prod (n, substaux k s, substaux (k + 1) t) - | NCic.Lambda (n,s,t) -> NCic.Lambda (n, substaux k s, substaux (k + 1) t) - | NCic.LetIn (n,ty,te,t) -> - NCic.LetIn (n, substaux k ty, substaux k te, substaux (k + 1) t) - | NCic.Appl (he::tl) -> - (* Invariant: no Appl applied to another Appl *) - let rec avoid he = function - | [] -> he - | arg::tl as args-> - (match he with - | NCic.Appl l -> NCic.Appl (l@args) - | NCic.Lambda (_,_,bo) when avoid_beta_redexes -> - (* map_arg is here \x.x, Obj magic is needed because - * we don't have polymorphic recursion w/o records *) - avoid (psubst - ~avoid_beta_redexes true 0 Obj.magic [Obj.magic arg] bo) tl - | _ as he -> NCic.Appl (he::args)) - in - let tl = List.map (substaux k) tl in - avoid (substaux k he) tl - | NCic.Appl _ -> assert false - | NCic.Match (r,outt,t,pl) -> - NCic.Match (r,substaux k outt, substaux k t, List.map (substaux k) pl) - *) + | NCic.Rel n as t -> + (match n with + | n when n >= (k+nargs) -> + if delift && nargs <> 0 then NCic.Rel (n - nargs) else t + | n when n < k -> t + | n (* k <= n < k+nargs *) -> + (try lift (k+lift_args) (map_arg (List.nth args (n-k))) + with Failure _ -> assert false)) + | NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> + if delift && nargs <> 0 then NCic.Meta (i,(m-nargs,l)) else t + | NCic.Meta (i,(m,(NCic.Irl l as irl))) as t when k > l + m -> + if delift && nargs <> 0 then NCic.Meta (i,(m-nargs,irl)) else t + | NCic.Meta (i,(m,l)) -> + let lctx = NCicUtils.expand_local_context l in + (* 1-nargs < k-m, when <= 0 is still reasonable because we will + * substitute args[ k-m ... k-m+nargs-1 > 0 ] *) + NCic.Meta (i,(m, NCic.Ctx (NCicUtils.sharing_map (substaux (k-m)) lctx))) + | NCic.Implicit _ -> assert false (* was identity *) + | NCic.Appl (he::tl) as t -> + (* Invariant: no Appl applied to another Appl *) + let rec avoid he' = function + | [] -> he' + | arg::tl' as args-> + (match he' with + | NCic.Appl l -> NCic.Appl (l@args) + | NCic.Lambda (_,_,bo) when avoid_beta_redexes -> + (* map_arg is here \x.x, Obj magic is needed because + * we don't have polymorphic recursion w/o records *) + avoid (psubst + ~avoid_beta_redexes true 0 Obj.magic [Obj.magic arg] bo) tl' + | _ -> if he == he' && args == tl then t else NCic.Appl (he'::args)) + in + let tl = NCicUtils.sharing_map (substaux k) tl in + avoid (substaux k he) tl + | t -> NCicUtils.map (fun _ k -> k + 1) k substaux t in substaux 1 ;; diff --git a/helm/software/components/ng_kernel/nCicUtils.ml b/helm/software/components/ng_kernel/nCicUtils.ml index 87dc48aa5..707ea93b6 100644 --- a/helm/software/components/ng_kernel/nCicUtils.ml +++ b/helm/software/components/ng_kernel/nCicUtils.ml @@ -36,16 +36,17 @@ let lookup_meta index metasenv = with Not_found -> raise (Meta_not_found index) ;; -let fold f g acc k = function +let fold g k f acc = function + | NCic.Meta _ -> assert false | NCic.Implicit _ | NCic.Sort _ | NCic.Const _ - | NCic.Meta _ | NCic.Rel _ -> acc + | NCic.Appl [] | NCic.Appl [_] -> assert false | NCic.Appl l -> List.fold_left (f k) acc l - | NCic.Prod (_,s,t) - | NCic.Lambda (_,s,t) -> f (g k) (f k acc s) t - | NCic.LetIn (_,ty,t,bo) -> f (g k) (f k (f k acc ty) t) bo + | NCic.Prod (n,s,t) + | NCic.Lambda (n,s,t) -> f (g (n,NCic.Decl s) k) (f k acc s) t + | NCic.LetIn (n,ty,t,bo) -> f (g (n,NCic.Def (t,ty)) k) (f k (f k acc ty) t) bo | NCic.Match (_,oty,t,pl) -> List.fold_left (f k) (f k (f k acc oty) t) pl ;; @@ -61,21 +62,27 @@ let sharing_map f l = if !unchanged then l else l1 ;; -let map f g k = function +let map g k f = function + | NCic.Meta _ -> assert false | NCic.Implicit _ | NCic.Sort _ | NCic.Const _ - | NCic.Meta _ | NCic.Rel _ as t -> t - | NCic.Appl l -> NCic.Appl (sharing_map (f k) l) + | NCic.Appl [] | NCic.Appl [_] -> assert false + | NCic.Appl l as orig -> + (match sharing_map (f k) l with + | NCic.Appl l :: tl -> NCic.Appl (l@tl) + | l1 when l == l1 -> orig + | l1 -> NCic.Appl l1) | NCic.Prod (n,s,t) as orig -> - let s1 = f k s in let t1 = f (g k) t in + let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1) | NCic.Lambda (n,s,t) as orig -> - let s1 = f k s in let t1 = f (g k) t in + let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1) | NCic.LetIn (n,ty,t,b) as orig -> - let ty1 = f k ty in let t1 = f k t in let b1 = f (g k) b in + let ty1 = f k ty in let t1 = f k t in + let b1 = f (g (n,NCic.Def (t,ty)) k) b in if ty1 == ty && t1 == t && b1 == b then orig else NCic.LetIn (n,ty1,t1,b1) | NCic.Match (r,oty,t,pl) as orig -> let oty1 = f k oty in let t1 = f k t in let pl1 = sharing_map (f k) pl in @@ -91,7 +98,7 @@ let is_closed t = | NCic.Rel n when n > k -> raise NotClosed | NCic.Meta (_, (s, NCic.Irl n)) when not (n+s <= k) -> raise NotClosed | NCic.Meta (_, (s, NCic.Ctx l)) -> List.iter (aux (k+s) ()) l - | _ -> fold aux ((+) 1) () k t + | _ -> fold (fun _ k -> k + 1) k aux () t in aux 0 () t; true with NotClosed -> false diff --git a/helm/software/components/ng_kernel/nCicUtils.mli b/helm/software/components/ng_kernel/nCicUtils.mli index f7bf45918..269603c65 100644 --- a/helm/software/components/ng_kernel/nCicUtils.mli +++ b/helm/software/components/ng_kernel/nCicUtils.mli @@ -28,14 +28,20 @@ exception Subst_not_found of int exception Meta_not_found of int +val sharing_map: ('a -> 'a) -> 'a list -> 'a list + val expand_local_context : NCic.lc_kind -> NCic.term list val lookup_subst: int -> NCic.substitution -> NCic.subst_entry val lookup_meta: int -> NCic.metasenv -> NCic.conjecture -(* both Meta agnostic, map attempts to preserve sharing. +(* both functions raise "assert false" when a Meta is found * call the 'a->'a function when a binder is crossed *) -val fold: ('a -> 'b -> NCic.term -> 'b) -> ('a -> 'a) -> 'b -> 'a -> NCic.term -> 'b -val map: ('a -> NCic.term -> NCic.term) -> ('a -> 'a) -> 'a -> NCic.term -> NCic.term +val fold: + (NCic.hypothesis -> 'k -> 'k) -> 'k -> + ('k -> 'a -> NCic.term -> 'a) -> 'a -> NCic.term -> 'a +val map: + (NCic.hypothesis -> 'k -> 'k) -> 'k -> + ('k -> NCic.term -> NCic.term) -> NCic.term -> NCic.term val is_closed: NCic.term -> bool -- 2.39.2