(* 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 _
+ | 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) (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
* substitute args[ k-m ... k-m+nargs-1 > 0 ] *)
NCic.Meta (i,(m, NCic.Ctx (List.map (substaux (k-m)) lctx)))
- | NCic.Sort _ as t -> t
| 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)
(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
avoid (substaux k he) tl
| NCic.Appl _ -> assert false
- | NCic.Const _ as t -> t
| NCic.Match (r,outt,t,pl) ->
NCic.Match (r,substaux k outt, substaux k t, List.map (substaux k) pl)
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
;;