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