(* if avoid_beta_redexes is true (default: false) no new beta redexes *)
(* are generated. WARNING: the substitution can diverge when t2 is not *)
(* well typed and avoid_beta_redexes is true. *)
-let rec psubst ?(avoid_beta_redexes=false) delift lift_args args =
+(* 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 nargs = List.length args in
let rec substaux k = function
| NCic.Sort _
| 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) (List.nth args (n-k))
+ (try lift (k+lift_args) (map_arg (List.nth args (n-k)))
with Failure _ -> assert false))
- | NCic.Meta (_,(m,_)) as t when m >= k + nargs - 1 -> t
- | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t
+ | 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
(match he with
| NCic.Appl l -> NCic.Appl (l@args)
| NCic.Lambda (_,_,bo) when avoid_beta_redexes ->
- avoid (psubst ~avoid_beta_redexes true 0 [arg] bo) tl
+ (* 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
substaux 1
;;
-let subst ?avoid_beta_redexes arg = psubst ?avoid_beta_redexes true 0 [arg];;
+let subst ?avoid_beta_redexes arg =
+ psubst ?avoid_beta_redexes true 0 (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 *)
let subst_meta = function
| m, NCic.Irl _
| m, NCic.Ctx [] -> lift m
- | m, NCic.Ctx l -> psubst false m l
+ | m, NCic.Ctx l -> psubst false m (fun x -> x) l
;;