aux false
;;
-let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l =
+let rec head_beta_reduce ~delta ~upto ~subst t l =
match upto, t, l with
| 0, C.Appl l1, _ -> C.Appl (l1 @ l)
| 0, t, [] -> t
| 0, t, _ -> C.Appl (t::l)
- | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto hd (tl @ l)
+ | _, C.Meta (n,ctx), _ ->
+ (try
+ let _,_, term,_ = NCicUtils.lookup_subst n subst in
+ head_beta_reduce ~delta ~upto ~subst
+ (NCicSubstitution.subst_meta ctx term) l
+ with NCicUtils.Subst_not_found _ -> if l = [] then t else C.Appl (t::l))
+ | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto ~subst hd (tl @ l)
| _, C.Lambda(_,_,bo), arg::tl ->
let bo = NCicSubstitution.subst arg bo in
- head_beta_reduce ~delta ~upto:(upto - 1) bo tl
+ head_beta_reduce ~delta ~upto:(upto - 1) ~subst bo tl
| _, C.Const (Ref.Ref (_, Ref.Def height) as re), _
when delta <= height ->
let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
- head_beta_reduce ~upto ~delta bo l
+ head_beta_reduce ~upto ~delta ~subst bo l
| _, t, [] -> t
| _, t, _ -> C.Appl (t::l)
;;
-let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];;
+let head_beta_reduce ?(delta=max_int) ?(upto= -1) ?(subst=[]) t =
+ head_beta_reduce ~delta ~upto ~subst t []
+;;
type stack_item = RS.stack_term
type environment_item = RS.env_term
let from_stack = RS.from_stack
let unwind = R.unwind
+let _ =
+ NCicUtils.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t);
+ NCicPp.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t);
+;;
+
+
+
+
(* vim:set foldmethod=marker: *)