module C = Cps
module S = Share
module L = Log
+module Y = Entity
module P = Output
module B = Brg
module O = BrgOutput
module E = BrgEnvironment
-type machine = {
- c: B.context;
- s: (B.context * B.term) list;
+type kam = {
+ c: B.lenv;
+ s: (B.lenv * B.term) list;
i: int
}
let level = 5
let log1 s c t =
- let sc, st = s ^ " in the context", "the term" in
- L.log O.specs level (L.ct_items1 sc c st t)
+ let sc, st = s ^ " in the environment", "the term" in
+ L.log O.specs level (L.et_items1 sc c st t)
let log2 s cu u ct t =
- let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in
- L.log O.specs level (L.ct_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 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)
let are_alpha_convertible err f t1 t2 =
let rec aux f = function
| B.Sort _ -> f m None x
| B.GRef (_, uri) ->
let f = function
- | _, _, B.Abbr (_, v) when delta ->
+ | _, _, Y.Abbr v when delta ->
P.add ~gdelta:1 (); step f ~delta ~rt m v
- | _, _, B.Abst (_, w) when rt ->
+ | _, _, Y.Abst w when rt ->
P.add ~grt:1 (); step f ~delta ~rt m w
- | _, _, B.Void _ ->
- assert false
- | e, _, b ->
- f m (Some (e, b)) x
+ | a, _, Y.Abbr v ->
+ let f e = f m (Some (e, B.Abbr (a, v))) x in
+ Y.apix C.err f a
+ | a, _, Y.Abst w ->
+ let f e = f m (Some (e, B.Abst (a, w))) x in
+ Y.apix C.err f a
in
- E.get_obj C.err f uri
+ E.get_entity C.err f uri
| B.LRef (_, i) ->
let f c = function
| B.Abbr (_, v) ->
assert false
| B.Abst (a, _) as b ->
let f e = f {m with c = c} (Some (e, b)) x in
- B.apix C.err f a
+ Y.apix C.err f a
in
get C.err f m i
| B.Cast (_, _, t) ->
let push f m b =
assert (m.s = []);
let b, i = match b with
- | B.Abst (a, w) -> B.abst (B.Apix m.i :: a) w, succ m.i
+ | B.Abst (a, w) -> B.abst (Y.Apix m.i :: a) w, succ m.i
| b -> b, m.i
in
let f c = f {m with c = c; i = i} in
(* Interface functions ******************************************************)
-let empty_machine = {
- c = B.empty_context; s = []; i = 0
+let empty_kam = {
+ c = B.empty_lenv; s = []; i = 0
}
let get err f m i =
let pp_term m frm t = O.specs.L.pp_term m.c frm t
-let pp_context frm m = O.specs.L.pp_context frm m.c
+let pp_lenv frm m = O.specs.L.pp_lenv frm m.c
let specs = {
- L.pp_term = pp_term; L.pp_context = pp_context
+ L.pp_term = pp_term; L.pp_lenv = pp_lenv
}