2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
15 ref (fun ~context:_ ~subst:_ ~metasenv:_ ?inside_fix _ ->
16 let _ = inside_fix in assert false)
18 let set_ppterm f = ppterm := f;;
21 module Ref = NReference
23 let debug_print = fun _ -> ();;
26 let rec liftaux k = function
27 | C.Rel m as t -> if m < k then t else C.Rel (m + n)
28 | C.Meta (i,(m,l)) when k <= m+1 -> C.Meta (i,(m+n,l))
29 | C.Meta (_,(m,C.Irl l)) as t when k > l + m -> t
31 let lctx = NCicUtils.expand_local_context l in
32 C.Meta (i, (m, C.Ctx (HExtlib.sharing_map (liftaux (k-m)) lctx)))
33 | C.Implicit _ -> (* was the identity *) assert false
34 | t -> NCicUtils.map (fun _ k -> k + 1) k liftaux t
39 let lift ?(from=1) n t =
41 else lift_from from n t
46 (* substitutes [t1] for [Rel 1] in [t2] *)
47 (* if avoid_beta_redexes is true (default: false) no new beta redexes *)
48 (* are generated. WARNING: the substitution can diverge when t2 is not *)
49 (* well typed and avoid_beta_redexes is true. *)
50 (* map_arg is ReductionStrategy.from_env_for_unwind when psubst is *)
51 (* used to implement nCicReduction.unwind' *)
52 let rec psubst ?(avoid_beta_redexes=false) map_arg args =
53 let nargs = List.length args in
54 let rec substaux k = function
57 | n when n >= (k+nargs) ->
58 if nargs <> 0 then C.Rel (n - nargs) else t
60 | n (* k <= n < k+nargs *) ->
61 (try lift (k-1) (map_arg (List.nth args (n-k)))
62 with Failure _ | Invalid_argument _ -> assert false))
63 | C.Meta (i,(m,l)) as t when m >= k + nargs - 1 ->
64 if nargs <> 0 then C.Meta (i,(m-nargs,l)) else t
65 | C.Meta (_,(m,(C.Irl l))) as t when k > l + m -> t
67 let lctx = NCicUtils.expand_local_context l in
69 C.Ctx (HExtlib.sharing_map (fun x -> substaux k (lift m x)) lctx)))
70 | C.Implicit _ -> assert false (* was identity *)
71 | C.Appl (he::tl) as t ->
72 (* Invariant: no Appl applied to another Appl *)
73 let rec avoid he' = function
77 | C.Appl l -> C.Appl (l@args)
78 | C.Lambda (_,_,bo) when avoid_beta_redexes ->
79 (* map_arg is here \x.x, Obj magic is needed because
80 * we don't have polymorphic recursion w/o records *)
82 ~avoid_beta_redexes Obj.magic [Obj.magic arg] bo) tl'
83 | _ -> if he == he' && args == tl then t else C.Appl (he'::args))
85 let tl = HExtlib.sharing_map (substaux k) tl in
86 avoid (substaux k he) tl
87 | t -> NCicUtils.map (fun _ k -> k + 1) k substaux t
92 let subst ?avoid_beta_redexes arg =
93 psubst ?avoid_beta_redexes (fun x -> x)[arg];;
95 (* subst_meta (n, C.Ctx [t_1 ; ... ; t_n]) t *)
96 (* returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *)
97 (* [t_i] is lifted as usual when it crosses an abstraction *)
98 (* subst_meta (n, (C.Irl _ | C.Ctx [])) t | -> lift n t *)
99 let subst_meta = function
101 | m, C.Ctx [] -> lift m
102 | m, C.Ctx l -> psubst (lift m) l