(* $Id$ *)
+let ppterm =
+ ref (fun ~context:_ ~subst:_ ~metasenv:_ ?inside_fix _ ->
+ let _ = inside_fix in assert false)
+;;
+let set_ppterm f = ppterm := f;;
+
module C = NCic
module Ref = NReference
let lift_from k n =
let rec liftaux k = function
| C.Rel m as t -> if m < k then t else C.Rel (m + n)
- | C.Meta (i,(m,l)) as t when k <= m ->
- if n = 0 then t else C.Meta (i,(m+n,l))
+ | C.Meta (i,(m,l)) when k <= m+1 -> C.Meta (i,(m+n,l))
| C.Meta (_,(m,C.Irl l)) as t when k > l + m -> t
| C.Meta (i,(m,l)) ->
let lctx = NCicUtils.expand_local_context l in
else lift_from from n t
;;
+
(* subst t1 t2 *)
(* substitutes [t1] for [Rel 1] in [t2] *)
(* if avoid_beta_redexes is true (default: false) no new beta redexes *)
| n when n < k -> t
| n (* k <= n < k+nargs *) ->
(try lift (k-1) (map_arg (List.nth args (n-k)))
- with Failure _ -> assert false))
+ with Failure _ | Invalid_argument _ -> assert false))
| C.Meta (i,(m,l)) as t when m >= k + nargs - 1 ->
if nargs <> 0 then C.Meta (i,(m-nargs,l)) else t
- | C.Meta (i,(m,(C.Irl l as irl))) as t when k > l + m ->
- if nargs <> 0 then C.Meta (i,(m-nargs,irl)) else t
+ | C.Meta (_,(m,(C.Irl l))) as t when k > l + m -> t
| C.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 ] *)
- C.Meta (i,(m, C.Ctx (HExtlib.sharing_map (substaux (k-m)) lctx)))
+ C.Meta (i,(0,
+ C.Ctx (HExtlib.sharing_map (fun x -> substaux k (lift m x)) lctx)))
| C.Implicit _ -> assert false (* was identity *)
| C.Appl (he::tl) as t ->
(* Invariant: no Appl applied to another Appl *)