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