\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module U = NUri
-module C = Cps
-module L = Log
-module Y = Entity
-module B = Bag
-module O = BagOutput
-module E = BagEnvironment
-module S = BagSubstitution
+module U = NUri
+module C = Cps
+module L = Log
+module E = Entity
+module Z = Bag
+module ZO = BagOutput
+module ZE = BagEnvironment
+module ZS = BagSubstitution
type machine = {
i: int;
- c: B.lenv;
- s: B.term list
+ c: Z.lenv;
+ s: Z.term list
}
type whd_result =
| Sort_ of int
- | LRef_ of int * B.term option
- | GRef_ of B.entity
- | Bind_ of int * B.id * B.term * B.term
+ | LRef_ of int * Z.term option
+ | GRef_ of Z.entity
+ | Bind_ of int * Z.id * Z.term * Z.term
type ho_whd_result =
| Sort of int
- | Abst of B.term
+ | Abst of Z.term
(* Internal functions *******************************************************)
let term_of_whdr = function
- | Sort_ h -> B.Sort h
- | LRef_ (i, _) -> B.LRef i
- | GRef_ (_, uri, _) -> B.GRef uri
- | Bind_ (l, id, w, t) -> B.bind_abst l id w t
+ | Sort_ h -> Z.Sort h
+ | LRef_ (i, _) -> Z.LRef i
+ | GRef_ (_, uri, _) -> Z.GRef uri
+ | Bind_ (l, id, w, t) -> Z.bind_abst l id w t
let level = 5
let log1 s c t =
let sc, st = s ^ " in the environment", "the term" in
- L.log O.specs level (L.et_items1 sc c st t)
+ L.log ZO.specs level (L.et_items1 sc c st t)
let log2 s cu u ct t =
let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
- L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+ L.log ZO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
-let empty_machine = {i = 0; c = B.empty_lenv; s = []}
+let empty_machine = {i = 0; c = Z.empty_lenv; s = []}
let inc m = {m with i = succ m.i}
let unwind_to_term f m t =
- let map f t (l, id, b) = f (B.Bind (l, id, b, t)) in
+ let map f t (l, id, b) = f (Z.Bind (l, id, b, t)) in
let f mc = C.list_fold_left f map t mc in
- B.contents f m.c
+ Z.contents f m.c
let unwind_stack f m =
let map f v = unwind_to_term f m v in
| Some (_, b) -> f b
| None -> assert false
in
- let f c = B.get f c i in
- B.append f c m.c
+ let f c = Z.get f c i in
+ Z.append f c m.c
let push msg f c m l id w =
assert (m.s = []);
- let f w = B.push msg f c l id (B.Abst w) in
+ let f w = Z.push msg f c l id (Z.Abst w) in
unwind_to_term f m w
(* to share *)
let rec whd f c m x =
(* L.warn "entering R.whd"; *)
match x with
- | B.Sort h -> f m (Sort_ h)
- | B.GRef uri ->
+ | Z.Sort h -> f m (Sort_ h)
+ | Z.GRef uri ->
let f entry = f m (GRef_ entry) in
- E.get_entity f uri
- | B.LRef i ->
+ ZE.get_entity f uri
+ | Z.LRef i ->
let f = function
- | B.Void -> f m (LRef_ (i, None))
- | B.Abst t -> f m (LRef_ (i, Some t))
- | B.Abbr t -> whd f c m t
+ | Z.Void -> f m (LRef_ (i, None))
+ | Z.Abst t -> f m (LRef_ (i, Some t))
+ | Z.Abbr t -> whd f c m t
in
get f c m i
- | B.Cast (_, t) -> whd f c m t
- | B.Appl (v, t) -> whd f c {m with s = v :: m.s} t
- | B.Bind (l, id, B.Abst w, t) ->
+ | Z.Cast (_, t) -> whd f c m t
+ | Z.Appl (v, t) -> whd f c {m with s = v :: m.s} t
+ | Z.Bind (l, id, Z.Abst w, t) ->
begin match m.s with
| [] -> f m (Bind_ (l, id, w, t))
| v :: tl ->
- let nl = B.new_location () in
- let f mc = S.subst (whd f c {m with c = mc; s = tl}) nl l t in
- B.push "!" f m.c nl id (B.Abbr (B.Cast (w, v)))
+ let nl = Z.new_location () in
+ let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in
+ Z.push "!" f m.c nl id (Z.Abbr (Z.Cast (w, v)))
end
- | B.Bind (l, id, b, t) ->
- let nl = B.new_location () in
- let f mc = S.subst (whd f c {m with c = mc}) nl l t in
- B.push "!" f m.c nl id b
+ | Z.Bind (l, id, b, t) ->
+ let nl = Z.new_location () in
+ let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in
+ Z.push "!" f m.c nl id b
(* Interface functions ******************************************************)
| Bind_ (_, _, w, _) ->
let f w = f (Abst w) in unwind_to_term f m w
| LRef_ (_, Some w) -> ho_whd f c m w
- | GRef_ (_, _, Y.Abst w) -> ho_whd f c m w
- | GRef_ (_, _, Y.Abbr v) -> ho_whd f c m v
+ | GRef_ (_, _, E.Abst w) -> ho_whd f c m w
+ | GRef_ (_, _, E.Abbr v) -> ho_whd f c m v
| LRef_ (_, None) -> assert false
- | GRef_ (_, _, Y.Void) -> assert false
+ | GRef_ (_, _, E.Void) -> assert false
in
whd aux c m x
if h1 = h2 then f a else f false
| LRef_ (i1, _), LRef_ (i2, _) ->
if i1 = i2 then are_convertible_stacks f ~si a c m1 m2 else f false
- | GRef_ ((Y.Apix a1 :: _), _, Y.Abst _),
- GRef_ ((Y.Apix a2 :: _), _, Y.Abst _) ->
+ | GRef_ ((E.Apix a1 :: _), _, E.Abst _),
+ GRef_ ((E.Apix a2 :: _), _, E.Abst _) ->
if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false
- | GRef_ ((Y.Apix a1 :: _), _, Y.Abbr v1),
- GRef_ ((Y.Apix a2 :: _), _, Y.Abbr v2) ->
+ | GRef_ ((E.Apix a1 :: _), _, E.Abbr v1),
+ GRef_ ((E.Apix a2 :: _), _, E.Abbr v2) ->
if a1 = a2 then
let f a =
if a then f a else are_convertible f ~si true c m1 v1 m2 v2
else
if a1 < a2 then whd (aux m1 r1) c m2 v2 else
whd (aux_rev m2 r2) c m1 v1
- | _, GRef_ (_, _, Y.Abbr v2) ->
+ | _, GRef_ (_, _, E.Abbr v2) ->
whd (aux m1 r1) c m2 v2
- | GRef_ (_, _, Y.Abbr v1), _ ->
+ | GRef_ (_, _, E.Abbr v1), _ ->
whd (aux_rev m2 r2) c m1 v1
| Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2) ->
- let l = B.new_location () in
+ let l = Z.new_location () in
let h c =
let m1, m2 = inc m1, inc m2 in
- let f t1 = S.subst (are_convertible f ~si a c m1 t1 m2) l l2 t2 in
- S.subst f l l1 t1
+ let f t1 = ZS.subst (are_convertible f ~si a c m1 t1 m2) l l2 t2 in
+ ZS.subst f l l1 t1
in
let f r = if r then push "!" h c m1 l id1 w1 else f false in
are_convertible f ~si a c m1 w1 m2 w2
projects / helm.git / blobdiff