From ed2e3cfadab248c4758b0ea1e7cc3da92de289d8 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 15 May 2008 10:08:00 +0000 Subject: [PATCH] Removed two args from psubst. --- .../components/ng_kernel/nCicReduction.ml | 2 +- .../components/ng_kernel/nCicSubstitution.ml | 18 +++++++++--------- .../components/ng_kernel/nCicSubstitution.mli | 2 +- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 5a8ba4164..99afc2aa8 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -351,7 +351,7 @@ module Reduction(RS : Strategy) = if k = 0 then t else NCicSubstitution.psubst ~avoid_beta_redexes:true - true 0 (RS.from_env_for_unwind ~unwind) e t + (RS.from_env_for_unwind ~unwind) e t in if s = [] then t else NCic.Appl(t::(RS.from_stack_list_for_unwind ~unwind s)) diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml index 51e4244c0..11d17de32 100644 --- a/helm/software/components/ng_kernel/nCicSubstitution.ml +++ b/helm/software/components/ng_kernel/nCicSubstitution.ml @@ -40,21 +40,21 @@ let lift ?(from=1) n t = (* well typed and avoid_beta_redexes is true. *) (* map_arg is ReductionStrategy.from_env_for_unwind when psubst is *) (* used to implement nCicReduction.unwind' *) -let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args = +let rec psubst ?(avoid_beta_redexes=false) 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 && nargs <> 0 then NCic.Rel (n - nargs) else t + if nargs <> 0 then NCic.Rel (n - nargs) else t | n when n < k -> t | n (* k <= n < k+nargs *) -> - (try lift (k-1+lift_args) (map_arg (List.nth args (n-k))) + (try lift (k-1) (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 + if 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 + if 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 @@ -72,7 +72,7 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args = (* 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' + ~avoid_beta_redexes Obj.magic [Obj.magic arg] bo) tl' | _ -> if he == he' && args == tl then t else NCic.Appl (he'::args)) in let tl = HExtlib.sharing_map (substaux k) tl in @@ -83,14 +83,14 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args = ;; let subst ?avoid_beta_redexes arg = - psubst ?avoid_beta_redexes true 0 (fun x -> x)[arg];; + psubst ?avoid_beta_redexes (fun x -> x)[arg];; (* subst_meta (n, Some [t_1 ; ... ; t_n]) t *) (* returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *) (* [t_i] is lifted as usual when it crosses an abstraction *) -(* subst_meta (n, Non) t -> lift n t *) +(* subst_meta (n, Non) t -> lift n t *) let subst_meta = function | m, NCic.Irl _ | m, NCic.Ctx [] -> lift m - | m, NCic.Ctx l -> psubst false m (fun x -> x) l + | m, NCic.Ctx l -> psubst (lift m) l ;; diff --git a/helm/software/components/ng_kernel/nCicSubstitution.mli b/helm/software/components/ng_kernel/nCicSubstitution.mli index 7e3301fa8..9b277078d 100644 --- a/helm/software/components/ng_kernel/nCicSubstitution.mli +++ b/helm/software/components/ng_kernel/nCicSubstitution.mli @@ -35,7 +35,7 @@ val subst : ?avoid_beta_redexes:bool -> NCic.term -> NCic.term -> NCic.term * the function is ReductionStrategy.from_env_for_unwind when psubst is * used to implement nCicReduction.unwind' *) val psubst : - ?avoid_beta_redexes:bool -> bool -> int -> + ?avoid_beta_redexes:bool -> ('a -> NCic.term) -> 'a list -> NCic.term -> NCic.term -- 2.39.2