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 C = Cps
  14 module S = Share
  15 module B = Brg
  16 module E = BrgEnvironment
  17
  18 exception LRefNotFound of string Lazy.t
  19
  20 type bind = Void_
  21           | Abst_ of B.term
  22           | Abbr_ of B.term
  23
  24 type environment = int * bind list
  25
  26 type stack = B.term list
  27
  28 type context = {
  29    g: environment;
  30    l: environment;
  31    s: stack
  32 }
  33
  34 type whd_result =
  35    | Sort_ of int
  36    | LRef_ of int * B.term option
  37    | GRef_ of int * B.bind * B.term
  38    | Bind_ of B.term * B.term
  39
  40 type ho_whd_result =
  41    | Sort of int
  42    | Abst of B.term
  43
  44 (* Internal functions *******************************************************)
  45
  46 let empty_e = 0, []
  47
  48 let push_e f b (l, e) =
  49    f (succ l, b :: e)
  50
  51 let get_e f c i =
  52    let (gl, ge), (ll, le) = c.g, c.l in
  53    if i >= gl + ll then raise (LRefNotFound (lazy (string_of_int i)));
  54    let b =
  55       if i < gl then List.nth ge (gl - (succ i))
  56       else List.nth le (gl + ll - (succ i))
  57    in
  58    f b
  59
  60 let rec lref_map f map t = match t with
  61    | B.LRef i             -> f (B.LRef (map i))
  62    | B.GRef _             -> f t
  63    | B.Sort _             -> f t
  64    | B.Cast (w, u)        ->
  65       let f w' u' = f (S.sh2 w w' u u' t B.cast) in
  66       let f w' = lref_map (f w') map u in
  67       lref_map f map w
  68    | B.Appl (w, u)        ->
  69       let f w' u' = f (S.sh2 w w' u u' t B.appl) in
  70       let f w' = lref_map (f w') map u in
  71       lref_map f map w
  72    | B.Bind (id, b, w, u) ->
  73       let f w' u' = f (S.sh2 w w' u u' t (B.bind id b)) in
  74       let f w' = lref_map (f w') map u in
  75       lref_map f map w
  76
  77 (* to share *)
  78 let lift f c =
  79    let (gl, _), (ll, le) = c.g, c.l in
  80    let map i = if i >= gl then succ i else i in
  81    let map f = function
  82       | Abbr_ t -> let f t' = f (Abbr_ t') in lref_map f map t
  83       | _       -> assert false
  84    in
  85    let f le' = f {c with l = (ll, le')} in
  86    C.list_map f map le
  87
  88 let xchg f c t =
  89    let (gl, _), (ll, _) = c.g, c.l in
  90    let map i =
  91       if i < gl || i > gl + ll then i else
  92       if i >= gl && i < gl + ll then succ i else gl
  93    in
  94    lref_map (f c) map t
  95
  96 (* to share *)
  97 let rec whd f c t = match t with
  98    | B.Sort h                 -> f c (Sort_ h)
  99    | B.GRef uri               ->
 100       let f (i, _, b, t) = f c (GRef_ (i, b, t)) in
 101       E.get_obj f uri
 102    | B.LRef i                 ->
 103       let f = function
 104          | Void_   -> f c (LRef_ (i, None))
 105          | Abst_ t -> f c (LRef_ (i, Some t))
 106          | Abbr_ t -> whd f c t
 107       in
 108       get_e f c i
 109    | B.Appl (v, t)            -> whd f {c with s = v :: c.s} t
 110    | B.Bind (_, B.Abbr, v, t) ->
 111       let f l = whd f {c with l = l} t in
 112       push_e f (Abbr_ v) c.l
 113    | B.Bind (_, B.Abst, w, t) ->
 114       begin match c.s with
 115          | []      -> f c (Bind_ (w, t))
 116          | v :: tl ->
 117             let f tl l = whd f {c with l = l; s = tl} t in
 118             push_e (f tl) (Abbr_ v) c.l
 119       end
 120    | B.Cast (_, t)            -> whd f c t
 121
 122 let push f c t =
 123    assert (c.s = []);
 124    let f c g = xchg f {c with g = g} t in
 125    let f c = push_e (f c) Void_ c.g in
 126    lift f c
 127
 128 (* Interface functions ******************************************************)
 129
 130 let rec are_convertible f c1 t1 c2 t2 =
 131    let rec aux c1' r1 c2' r2 = match r1, r2 with
 132       | Sort_ h1, Sort_ h2                             -> f (h1 = h2)
 133       | LRef_ (i1, _), LRef_ (i2, _)                   ->
 134          if i1 = i2 then are_convertible_stacks f c1' c2' else f false
 135       | GRef_ (a1, B.Abst, _), GRef_ (a2, B.Abst, _)   ->
 136          if a1 = a2 then are_convertible_stacks f c1' c2' else f false
 137       | GRef_ (a1, B.Abbr, v1), GRef_ (a2, B.Abbr, v2) ->
 138          if a1 = a2 then are_convertible_stacks f c1' c2' else
 139          if a1 < a2 then whd (aux c1' r1) c2' v2 else
 140          whd (aux_rev c2' r2) c1' v1
 141       | _, GRef_ (_, B.Abbr, v2)                       ->
 142          whd (aux c1' r1) c2' v2
 143       | GRef_ (_, B.Abbr, v1), _                       ->
 144          whd (aux_rev c2' r2) c1' v1
 145       | Bind_ (w1, t1), Bind_ (w2, t2)                 ->
 146          let f b =
 147             if b then
 148                let f c1'' t1' = push (are_convertible f c1'' t1') c2' t2 in
 149                push f c1' t1
 150             else f false
 151          in
 152          are_convertible f c1' w1 c2' w2
 153       | _                                              -> f false
 154    and aux_rev c2 r2 c1 r1 = aux c1 r1 c2 r2 in
 155    let f c1' r1 = whd (aux c1' r1) c2 t2 in
 156    whd f c1 t1
 157
 158 and are_convertible_stacks f c1 c2 =
 159    let map f v1 v2 = are_convertible f c1 v1 c2 v2 in
 160    if List.length c1.s <> List.length c2.s then f false else
 161    C.forall2 f map c1.s c2.s
 162
 163 let are_convertible f c t1 t2 = are_convertible f c t1 c t2
 164
 165 let rec ho_whd f c t =
 166    let aux c' = function
 167       | Sort_ h           -> f c' (Sort h)
 168       | Bind_ (w, t)      -> f c' (Abst w)
 169       | LRef_ (_, Some w) -> ho_whd f c w
 170       | GRef_ (_, _, u)   -> ho_whd f c u
 171       | LRef_ (_, None)   -> assert false
 172    in
 173    whd aux c t
 174
 175 let push f c b t =
 176    assert (c.l = empty_e && c.s = []);
 177    let f g = f {c with g = g} in
 178    let b = match b with
 179       | B.Abbr -> Abbr_ t
 180       | B.Abst -> Abst_ t
 181    in
 182    push_e f b c.g
 183
 184 let get f c i =
 185    let gl, ge = c.g in
 186    if i >= gl then raise (LRefNotFound (lazy (string_of_int i)));
 187    match List.nth ge (gl - (succ i)) with
 188       | Abbr_ v -> f (B.Abbr, v)
 189       | Abst_ w -> f (B.Abst, w)
 190       | Void_   -> assert false
 191
 192 let empty_context = {
 193    g = empty_e; l = empty_e; s = []
 194 }