(* ||M|| This file is part of HELM, an Hypertextual, Electronic ||A|| Library of Mathematics, developed at the Computer Science ||T|| Department, University of Bologna, Italy. ||I|| ||T|| HELM is free software; you can redistribute it and/or ||A|| modify it under the terms of the GNU General Public License \ / version 2 or (at your option) any later version. \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module U = NUri module B = Brg module E = BrgEnvironment exception LRefNotFound of string Lazy.t type environment = int * (B.bind * B.term) list type stack = B.term list type context = { g: environment; l: environment; s: stack } type whd_result = | Sort_ of int | LRef_ of int | GRef_ of int * U.uri * B.bind | Abst_ of B.term (* Internal functions *******************************************************) let push_e f b t (l, e) = f (succ l, (b, t) :: e) let rec find_e f c i = let (gl, ge), (ll, le) = c.g, c.l in if i >= gl + ll then raise (LRefNotFound (lazy (string_of_int i))); let b, t = if i < gl then List.nth ge (gl - (succ i)) else List.nth le (gl + ll - (succ i)) in f t b let rec whd f c t = match t with | B.Sort h -> f c t (Sort_ h) | B.GRef uri -> let f (i, _, b, t) = f c t (GRef_ (i, uri, b)) in E.get_obj f uri | B.LRef i -> let f t = function | B.Abst -> f c t (LRef_ i) | B.Abbr -> whd f c t in find_e f c i | B.Appl (v, t) -> whd f {c with s = v :: c.s} t | B.Bind (_, B.Abbr, v, t) -> let f l = whd f {c with l = l} t in push_e f B.Abbr v c.l | B.Bind (_, B.Abst, w, t) -> begin match c.s with | [] -> f c t (Abst_ w) | v :: tl -> let f tl l = whd f {c with l = l; s = tl} t in push_e (f tl) B.Abbr v c.l end | B.Cast (_, t) -> whd f c t (* Interface functions ******************************************************) let push f c b t = assert (fst c.l = 0 && c.s = []); let f g = f {c with g = g} in push_e f b t c.g