module U = NUri
module C = Cps
module S = Share
+module L = Log
module B = Brg
module E = BrgEnvironment
-exception LRefNotFound of string Lazy.t
-
-type bind = Void_
- | Abst_ of B.term
- | Abbr_ of B.term
-
-type environment = int * bind list
+type environment = int * B.bind list
type stack = B.term list
s: stack
}
+exception LRefNotFound of (context, B.term) L.item list
+
type whd_result =
| Sort_ of int
| LRef_ of int * B.term option
- | GRef_ of int * B.bind * B.term
+ | GRef_ of int * B.bind
| Bind_ of B.term * B.term
type ho_whd_result =
(* Internal functions *******************************************************)
+let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
+
let empty_e = 0, []
let push_e f b (l, e) =
let get_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)));
+ if i >= gl + ll then error i;
let b =
if i < gl then List.nth ge (gl - (succ i))
else List.nth le (gl + ll - (succ i))
in
f b
-let rec lref_map f map t = match t with
- | B.LRef i -> f (B.LRef (map i))
- | B.GRef _ -> f t
- | B.Sort _ -> f t
- | B.Cast (w, u) ->
+let rec lref_map_bind f map b = match b with
+ | B.Abbr v ->
+ let f v' = f (S.sh1 v v' b B.abbr) in
+ lref_map f map v
+ | B.Abst w ->
+ let f w' = f (S.sh1 w w' b B.abst) in
+ lref_map f map w
+ | B.Void -> f b
+
+and lref_map f map t = match t with
+ | B.LRef i -> f (B.LRef (map i))
+ | B.GRef _ -> f t
+ | B.Sort _ -> f t
+ | B.Cast (w, u) ->
let f w' u' = f (S.sh2 w w' u u' t B.cast) in
let f w' = lref_map (f w') map u in
lref_map f map w
- | B.Appl (w, u) ->
+ | B.Appl (w, u) ->
let f w' u' = f (S.sh2 w w' u u' t B.appl) in
let f w' = lref_map (f w') map u in
lref_map f map w
- | B.Bind (id, b, w, u) ->
- let f w' u' = f (S.sh2 w w' u u' t (B.bind id b)) in
- let f w' = lref_map (f w') map u in
- lref_map f map w
+ | B.Bind (id, b, u) ->
+ let f b' u' = f (S.sh2 b b' u u' t (B.bind id)) in
+ let f b' = lref_map (f b') map u in
+ lref_map_bind f map b
(* to share *)
let lift f c =
let (gl, _), (ll, le) = c.g, c.l in
let map i = if i >= gl then succ i else i in
let map f = function
- | Abbr_ t -> let f t' = f (Abbr_ t') in lref_map f map t
+ | B.Abbr t -> let f t' = f (B.Abbr t') in lref_map f map t
| _ -> assert false
in
let f le' = f {c with l = (ll, le')} in
let rec whd f c t = match t with
| B.Sort h -> f c (Sort_ h)
| B.GRef uri ->
- let f (i, _, b, t) = f c (GRef_ (i, b, t)) in
+ let f (i, _, b) = f c (GRef_ (i, b)) in
E.get_obj f uri
- | B.LRef i ->
+ | B.LRef i ->
let f = function
- | Void_ -> f c (LRef_ (i, None))
- | Abst_ t -> f c (LRef_ (i, Some t))
- | Abbr_ t -> whd f c t
+ | B.Void -> f c (LRef_ (i, None))
+ | B.Abst t -> f c (LRef_ (i, Some t))
+ | B.Abbr t -> whd f c t
in
get_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 (Abbr_ v) c.l
- | B.Bind (_, B.Abst, w, t) ->
+ | B.Cast (_, t) -> whd f c t
+ | B.Appl (v, t) -> whd f {c with s = v :: c.s} t
+ | B.Bind (_, B.Abst w, t) ->
begin match c.s with
| [] -> f c (Bind_ (w, t))
| v :: tl ->
let f tl l = whd f {c with l = l; s = tl} t in
- push_e (f tl) (Abbr_ v) c.l
+ push_e (f tl) (B.Abbr v) c.l
end
- | B.Cast (_, t) -> whd f c t
+ | B.Bind (_, b, t) ->
+ let f l = whd f {c with l = l} t in
+ push_e f b c.l
let push f c t =
assert (c.s = []);
let f c g = xchg f {c with g = g} t in
- let f c = push_e (f c) Void_ c.g in
+ let f c = push_e (f c) B.Void c.g in
lift f c
(* Interface functions ******************************************************)
let rec are_convertible f c1 t1 c2 t2 =
let rec aux c1' r1 c2' r2 = match r1, r2 with
- | Sort_ h1, Sort_ h2 -> f (h1 = h2)
- | LRef_ (i1, _), LRef_ (i2, _) ->
+ | Sort_ h1, Sort_ h2 -> f (h1 = h2)
+ | LRef_ (i1, _), LRef_ (i2, _) ->
if i1 = i2 then are_convertible_stacks f c1' c2' else f false
- | GRef_ (a1, B.Abst, _), GRef_ (a2, B.Abst, _) ->
+ | GRef_ (a1, B.Abst _), GRef_ (a2, B.Abst _) ->
if a1 = a2 then are_convertible_stacks f c1' c2' else f false
- | GRef_ (a1, B.Abbr, v1), GRef_ (a2, B.Abbr, v2) ->
+ | GRef_ (a1, B.Abbr v1), GRef_ (a2, B.Abbr v2) ->
if a1 = a2 then are_convertible_stacks f c1' c2' else
if a1 < a2 then whd (aux c1' r1) c2' v2 else
whd (aux_rev c2' r2) c1' v1
- | _, GRef_ (_, B.Abbr, v2) ->
+ | _, GRef_ (_, B.Abbr v2) ->
whd (aux c1' r1) c2' v2
- | GRef_ (_, B.Abbr, v1), _ ->
+ | GRef_ (_, B.Abbr v1), _ ->
whd (aux_rev c2' r2) c1' v1
- | Bind_ (w1, t1), Bind_ (w2, t2) ->
+ | Bind_ (w1, t1), Bind_ (w2, t2) ->
let f b =
if b then
let f c1'' t1' = push (are_convertible f c1'' t1') c2' t2 in
let rec ho_whd f c t =
let aux c' = function
- | Sort_ h -> f c' (Sort h)
- | Bind_ (w, t) -> f c' (Abst w)
- | LRef_ (_, Some w) -> ho_whd f c w
- | GRef_ (_, _, u) -> ho_whd f c u
- | LRef_ (_, None) -> assert false
+ | Sort_ h -> f c' (Sort h)
+ | Bind_ (w, t) -> f c' (Abst w)
+ | LRef_ (_, Some w) -> ho_whd f c w
+ | GRef_ (_, B.Abst u) -> ho_whd f c u
+ | GRef_ (_, B.Abbr u) -> ho_whd f c u
+ | LRef_ (_, None) -> assert false
+ | GRef_ (_, B.Void) -> assert false
in
whd aux c t
-let push f c b t =
+let push f c b =
assert (c.l = empty_e && c.s = []);
let f g = f {c with g = g} in
- let b = match b with
- | B.Abbr -> Abbr_ t
- | B.Abst -> Abst_ t
- in
push_e f b c.g
let get f c i =
let gl, ge = c.g in
- if i >= gl then raise (LRefNotFound (lazy (string_of_int i)));
- match List.nth ge (gl - (succ i)) with
- | Abbr_ v -> f (B.Abbr, v)
- | Abst_ w -> f (B.Abst, w)
- | Void_ -> assert false
+ if i >= gl then error i;
+ f (List.nth ge (gl - (succ i)))
let empty_context = {
g = empty_e; l = empty_e; s = []
}
+
+let iter f map c =
+ let _, ge = c.g in
+ C.list_iter f map ge
projects / helm.git / blobdiff