helm/software/lambda-delta/basic_rg/brgReduction.ml

   1 (*
   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.
   5     ||I||
   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_______________________________________________________________ *)
  11
  12 module U = NUri
  13 module B = Brg
  14 module E = BrgEnvironment
  15
  16 exception LRefNotFound of string Lazy.t
  17
  18 type environment = int * (B.bind * B.term) list
  19
  20 type stack = B.term list
  21
  22 type context = {
  23    g: environment;
  24    l: environment;
  25    s: stack
  26 }
  27
  28 type whd_result =
  29    | Sort_ of int
  30    | LRef_ of int
  31    | GRef_ of int * U.uri * B.bind
  32    | Abst_ of B.term
  33
  34 (* Internal functions *******************************************************)
  35
  36 let push_e f b t (l, e) =
  37    f (succ l, (b, t) :: e)
  38
  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)));
  42    let b, t =
  43       if i < gl then List.nth ge (gl - (succ i))
  44       else List.nth le (gl + ll - (succ i))
  45    in
  46    f t b
  47
  48 let rec whd f c t = match t with
  49    | B.Sort h                 -> f c t (Sort_ h)
  50    | B.GRef uri               ->
  51       let f (i, _, b, t) = f c t (GRef_ (i, uri, b)) in
  52       E.get_obj f uri
  53    | B.LRef i                 ->
  54       let f t = function
  55          | B.Abst -> f c t (LRef_ i)
  56          | B.Abbr -> whd f c t
  57       in
  58       find_e f c 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
  62       push_e f B.Abbr v c.l
  63    | B.Bind (_, B.Abst, w, t) ->
  64       begin match c.s with
  65          | []      -> f c t (Abst_ w)
  66          | v :: tl ->
  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
  69       end
  70    | B.Cast (_, t)            -> whd f c t
  71
  72 (* Interface functions ******************************************************)
  73
  74 let push f c b t =
  75    assert (fst c.l = 0 && c.s = []);
  76    let f g = f {c with g = g} in
  77    push_e f b t c.g