\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module U = NUri
-module C = Cps
-module S = Share
-module L = Log
-module Y = Entity
-module P = Output
-module B = Brg
-module O = BrgOutput
-module E = BrgEnvironment
+module U = NUri
+module C = Cps
+module S = Share
+module L = Log
+module E = Entity
+module O = Output
+module B = Brg
+module BO = BrgOutput
+module BE = BrgEnvironment
type kam = {
e: B.lenv; (* environment *)
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 BO.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 BO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
let rec list_and map = function
| hd1 :: tl1, hd2 :: tl2 ->
match x with
| B.Sort _ -> m, None, x
| B.GRef (_, uri) ->
- begin match E.get_entity uri with
- | _, _, Y.Abbr v when st.Y.delta ->
- P.add ~gdelta:1 (); step st m v
- | _, _, Y.Abst w when st.Y.rt ->
- P.add ~grt:1 (); step st m w
- | a, _, Y.Abbr v ->
- let e = Y.apix C.err C.start a in
+ begin match BE.get_entity uri with
+ | _, _, E.Abbr v when st.E.delta ->
+ O.add ~gdelta:1 (); step st m v
+ | _, _, E.Abst w when st.E.rt ->
+ O.add ~grt:1 (); step st m w
+ | a, _, E.Abbr v ->
+ let e = E.apix C.err C.start a in
m, Some (e, a, B.Abbr v), x
- | a, _, Y.Abst w ->
- let e = Y.apix C.err C.start a in
+ | a, _, E.Abst w ->
+ let e = E.apix C.err C.start a in
m, Some (e, a, B.Abst w), x
- | _, _, Y.Void -> assert false
+ | _, _, E.Void -> assert false
end
| B.LRef (_, i) ->
begin match get m i with
| c, _, B.Abbr v ->
- P.add ~ldelta:1 ();
+ O.add ~ldelta:1 ();
step st {m with e = c} v
- | c, _, B.Abst w when st.Y.rt ->
- P.add ~lrt:1 ();
+ | c, _, B.Abst w when st.E.rt ->
+ O.add ~lrt:1 ();
step st {m with e = c} w
| c, _, B.Void ->
assert false
| c, a, (B.Abst _ as b) ->
- let e = Y.apix C.err C.start a in
+ let e = E.apix C.err C.start a in
{m with e = c}, Some (e, a, b), x
end
| B.Cast (_, _, t) ->
- P.add ~tau:1 ();
+ O.add ~tau:1 ();
step st m t
| B.Appl (_, v, t) ->
step st {m with s = (m.e, v) :: m.s} t
begin match m.s with
| [] -> m, None, x
| (c, v) :: s ->
- P.add ~beta:1 ~upsilon:(List.length s) ();
+ O.add ~beta:1 ~upsilon:(List.length s) ();
let e = B.push m.e c a (B.abbr v) (* (B.Cast ([], w, v)) *) in
step st {m with e = e; s = s} t
end
| B.Bind (a, b, t) ->
- P.add ~upsilon:(List.length m.s) ();
+ O.add ~upsilon:(List.length m.s) ();
let e = B.push m.e m.e a b in
step st {m with e = e} t
let push m a b =
assert (m.s = []);
let a, d = match b with
- | B.Abst _ -> Y.Apix m.d :: a, succ m.d
+ | B.Abst _ -> E.Apix m.d :: a, succ m.d
| b -> a, m.d
in
let e = B.push m.e m.e a b in
| Some (e1, _, B.Abbr v1), _, Some (e2, _, B.Abbr v2), _ ->
if e1 = e2 then
if ac_stacks st m1 m2 then true else begin
- P.add ~gdelta:2 (); ac st m1 v1 m2 v2
+ O.add ~gdelta:2 (); ac st m1 v1 m2 v2
end
else if e1 < e2 then begin
- P.add ~gdelta:1 ();
+ O.add ~gdelta:1 ();
ac_nfs st (m1, r1, u) (step st m2 v2)
end else begin
- P.add ~gdelta:1 ();
+ O.add ~gdelta:1 ();
ac_nfs st (step st m1 v1) (m2, r2, t)
end
| _, _, Some (_, _, B.Abbr v2), _ ->
- P.add ~gdelta:1 ();
+ O.add ~gdelta:1 ();
ac_nfs st (m1, r1, u) (step st m2 v2)
| Some (_, _, B.Abbr v1), _, _, _ ->
- P.add ~gdelta:1 ();
+ O.add ~gdelta:1 ();
ac_nfs st (step st m1 v1) (m2, r2, t)
| _, B.Bind (a1, (B.Abst w1 as b1), t1),
_, B.Bind (a2, (B.Abst w2 as b2), t2) ->
- if ac {st with Y.si = false} m1 w1 m2 w2 then
+ if ac {st with E.si = false} m1 w1 m2 w2 then
ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
else false
- | _, B.Sort _, _, B.Bind (a, b, t) when st.Y.si ->
- P.add ~si:1 ();
+ | _, B.Sort _, _, B.Bind (a, b, t) when st.E.si ->
+ O.add ~si:1 ();
ac st (push m1 a b) u (push m2 a b) t
| _ -> false
if List.length m1.s <> List.length m2.s then false else
let map (c1, v1) (c2, v2) =
let m1, m2 = {m1 with e = c1; s = []}, {m2 with e = c2; s = []} in
- ac {st with Y.si = false} m1 v1 m2 v2
+ ac {st with E.si = false} m1 v1 m2 v2
in
list_and map (m1.s, m2.s)
let xwhd st m t =
L.box level; log1 "Now scanning" m.e t;
- let m, _, t = step {st with Y.delta = true; Y.rt = true} m t in
+ let m, _, t = step {st with E.delta = true; E.rt = true} m t in
L.unbox level; m, t
let are_convertible st mu u mw w =
L.box level; log2 "Now converting" mu.e u mw.e w;
- let r = ac {st with Y.delta = st.Y.expand; Y.rt = false} mu u mw w in
+ let r = ac {st with E.delta = st.E.expand; E.rt = false} mu u mw w in
L.unbox level; r
(* let err _ = in
if S.eq mu mw then are_alpha_convertible err f u w else err () *)
(* error reporting **********************************************************)
-let pp_term m frm t = O.specs.L.pp_term m.e frm t
+let pp_term m frm t = BO.specs.L.pp_term m.e frm t
-let pp_lenv frm m = O.specs.L.pp_lenv frm m.e
+let pp_lenv frm m = BO.specs.L.pp_lenv frm m.e
let specs = {
L.pp_term = pp_term; L.pp_lenv = pp_lenv
projects / helm.git / blobdiff