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_______________________________________________________________ *)
14 module E = BrgEnvironment
16 exception LRefNotFound of string Lazy.t
18 type environment = int * (B.bind * B.term) list
20 type stack = B.term list
31 | GRef_ of int * U.uri * B.bind
34 (* Internal functions *******************************************************)
36 let push_e f b t (l, e) =
37 f (succ l, (b, t) :: e)
39 let rec find_e f c i =
40 let (gl, ge), (ll, le) = c.g, c.l in
41 if i >= gl + ll then raise (LRefNotFound (lazy (string_of_int i)));
43 if i < gl then List.nth ge (gl - (succ i))
44 else List.nth le (gl + ll - (succ i))
48 let rec whd f c t = match t with
49 | B.Sort h -> f c t (Sort_ h)
51 let f (i, _, b, t) = f c t (GRef_ (i, uri, b)) in
55 | B.Abst -> f c t (LRef_ i)
59 | B.Appl (v, t) -> whd f {c with s = v :: c.s} t
60 | B.Bind (_, B.Abbr, v, t) ->
61 let f l = whd f {c with l = l} t in
63 | B.Bind (_, B.Abst, w, t) ->
65 | [] -> f c t (Abst_ w)
67 let f tl l = whd f {c with l = l; s = tl} t in
68 push_e (f tl) B.Abbr v c.l
70 | B.Cast (_, t) -> whd f c t
72 (* Interface functions ******************************************************)
75 assert (fst c.l = 0 && c.s = []);
76 let f g = f {c with g = g} in