V_______________________________________________________________ *)
module U = NUri
+module C = Cps
+module S = Share
module B = Brg
module E = BrgEnvironment
exception LRefNotFound of string Lazy.t
-type environment = int * (B.bind * B.term) list
+type bind = Void_
+ | Abst_ of B.term
+ | Abbr_ of B.term
+
+type environment = int * bind list
type stack = B.term list
type whd_result =
| Sort_ of int
- | LRef_ of int
- | GRef_ of int * U.uri * B.bind
- | Abst_ of B.term
+ | LRef_ of int * B.term option
+ | GRef_ of int * B.bind * B.term
+ | Bind_ of B.term * B.term
+
+type ho_whd_result =
+ | Sort of int
+ | Abst of B.term
(* Internal functions *******************************************************)
-let push_e f b t (l, e) =
- f (succ l, (b, t) :: e)
+let empty_e = 0, []
+
+let push_e f b (l, e) =
+ f (succ l, b :: e)
-let rec find_e f c i =
+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)));
- let b, t =
+ let b =
if i < gl then List.nth ge (gl - (succ i))
else List.nth le (gl + ll - (succ i))
in
- f t b
-
+ 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 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) ->
+ 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
+
+(* 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
+ | _ -> assert false
+ in
+ let f le' = f {c with l = (ll, le')} in
+ C.list_map f map le
+
+let xchg f c t =
+ let (gl, _), (ll, _) = c.g, c.l in
+ let map i =
+ if i < gl || i > gl + ll then i else
+ if i >= gl && i < gl + ll then succ i else gl
+ in
+ lref_map (f c) map t
+
+(* to share *)
let rec whd f c t = match t with
- | B.Sort h -> f c t (Sort_ h)
+ | B.Sort h -> f c (Sort_ h)
| B.GRef uri ->
- let f (i, _, b, t) = f c t (GRef_ (i, uri, b)) in
+ let f (i, _, b, t) = f c (GRef_ (i, b, t)) in
E.get_obj f uri
| B.LRef i ->
- let f t = function
- | B.Abst -> f c t (LRef_ i)
- | B.Abbr -> whd f c t
+ let f = function
+ | Void_ -> f c (LRef_ (i, None))
+ | Abst_ t -> f c (LRef_ (i, Some t))
+ | Abbr_ t -> whd f c t
in
- find_e f c i
+ 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 B.Abbr v c.l
+ push_e f (Abbr_ v) c.l
| B.Bind (_, B.Abst, w, t) ->
begin match c.s with
- | [] -> f c t (Abst_ w)
+ | [] -> 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) B.Abbr v c.l
+ push_e (f tl) (Abbr_ v) c.l
end
| B.Cast (_, t) -> whd f c t
+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
+ 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, _) ->
+ if i1 = i2 then are_convertible_stacks f c1' c2' else f false
+ | 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) ->
+ 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) ->
+ whd (aux c1' r1) c2' v2
+ | GRef_ (_, B.Abbr, v1), _ ->
+ whd (aux_rev c2' r2) c1' v1
+ | 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
+ push f c1' t1
+ else f false
+ in
+ are_convertible f c1' w1 c2' w2
+ | _ -> f false
+ and aux_rev c2 r2 c1 r1 = aux c1 r1 c2 r2 in
+ let f c1' r1 = whd (aux c1' r1) c2 t2 in
+ whd f c1 t1
+
+and are_convertible_stacks f c1 c2 =
+ let map f v1 v2 = are_convertible f c1 v1 c2 v2 in
+ if List.length c1.s <> List.length c2.s then f false else
+ C.forall2 f map c1.s c2.s
+
+let are_convertible f c t1 t2 = are_convertible f c t1 c t2
+
+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
+ in
+ whd aux c t
+
let push f c b t =
- assert (fst c.l = 0 && c.s = []);
+ assert (c.l = empty_e && c.s = []);
let f g = f {c with g = g} in
- push_e f b t c.g
+ 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
+
+let empty_context = {
+ g = empty_e; l = empty_e; s = []
+}
projects / helm.git / blobdiff