module U = NUri
module C = Cps
module L = Log
+module P = Output
module B = Brg
module O = BrgOutput
module E = BrgEnvironment
(* Internal functions *******************************************************)
-let reductions = ref O.initial_reductions
-
let level = 5
let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
f {m with c = (a, b) :: m.c}
(* to share *)
-let rec step f ?(delta=false) ?(sty=false) c m x =
+let rec step f ?(delta=false) ?(rt=false) c m x =
(* L.warn "entering R.step"; *)
match x with
| B.Sort _ -> f m x
| B.GRef (a, uri) ->
let f = function
| _, _, B.Abbr v when delta ->
- reductions := O.add ~gdelta:1 !reductions;
- step f ~delta ~sty c m v
- | _, _, B.Abst w when sty ->
- step f ~delta ~sty c m w
+ P.add ~gdelta:1 ();
+ step f ~delta ~rt c m v
+ | _, _, B.Abst w when rt ->
+ P.add ~grt:1 ();
+ step f ~delta ~rt c m w
| e, _, b ->
f m (B.GRef (B.Entry (e, b) :: a, uri))
in
| B.LRef (a, i) ->
let f e = function
| B.Abbr v ->
- reductions := O.add ~ldelta:1 !reductions;
- step f ~delta ~sty c m v
- | B.Abst w when sty ->
- step f ~delta ~sty c m w
+ P.add ~ldelta:1 ();
+ step f ~delta ~rt c m v
+ | B.Abst w when rt ->
+ P.add ~lrt:1 ();
+ step f ~delta ~rt c m w
| b ->
f m (B.LRef (B.Entry (e, b) :: a, i))
in
let f e = S.lift_bind (f e) (succ i) (0) in
get f c m i
| B.Cast (_, _, t) ->
- reductions := O.add ~tau:1 !reductions;
- step f ~delta ~sty c m t
+ P.add ~tau:1 ();
+ step f ~delta ~rt c m t
| B.Appl (_, v, t) ->
- step f ~delta ~sty c {m with s = (v, 0) :: m.s} t
+ step f ~delta ~rt c {m with s = (v, 0) :: m.s} t
| B.Bind (a, B.Abst w, t) ->
begin match m.s with
| [] -> f m x
| (v, h) :: tl ->
- reductions := O.add ~beta:1 !reductions;
- let f mc = step f ~delta ~sty c {c = mc; s = tl} t in
- let f v = B.push f m.c a (B.Abbr (B.Cast ([], w, v))) in
+ P.add ~beta:1 ~upsilon:(List.length tl) ();
+ let f mc sc = step f ~delta ~rt c {c = mc; s = sc} t in
+ let f mc = lift_stack (f mc) tl in
+ let f v = B.push f m.c a (B.Abbr v (* (B.Cast ([], w, v)) *) ) in
S.lift f h (0) v
end
| B.Bind (a, b, t) ->
- reductions := O.add ~upsilon:(List.length m.s) !reductions;
- let f sc mc = step f ~delta ~sty c {c = mc; s = sc} t in
+ P.add ~upsilon:(List.length m.s) ();
+ let f sc mc = step f ~delta ~rt c {c = mc; s = sc} t in
let f sc = B.push (f sc) m.c a b in
lift_stack f m.s
| x -> f None
in
L.box level; log1 "Now scanning" c t;
- step f ~delta:true ~sty:true c empty_machine t
+ step f ~delta:true ~rt:true c empty_machine t
let rec ac_nfs f ~si r c m1 u m2 t =
(* L.warn "entering R.are_convertible_aux"; *)
match u, t with
| B.Sort (_, h1), B.Sort (_, h2) ->
if h1 = h2 then f r else f false
- | B.LRef (B.Entry (e1, B.Abst _) :: _, _),
- B.LRef (B.Entry (e2, B.Abst _) :: _, _) ->
+ | B.LRef (B.Entry (e1, B.Abst _) :: _, i1),
+ B.LRef (B.Entry (e2, B.Abst _) :: _, i2) ->
+ P.add ~zeta:(i1+i2-e1-e2) ();
if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false
| B.GRef (B.Entry (e1, B.Abst _) :: _, _),
B.GRef (B.Entry (e2, B.Abst _) :: _, _) ->
let f r =
if r then f r
else begin
- reductions := O.add ~gdelta:2 !reductions;
+ P.add ~gdelta:2 ();
ac f ~si true c m1 v1 m2 v2
end
in
ac_stacks f ~si r c m1 m2
else if e1 < e2 then begin
- reductions := O.add ~gdelta:1 !reductions;
+ P.add ~gdelta:1 ();
step (ac_nfs f ~si r c m1 u) c m2 v2
end else begin
- reductions := O.add ~gdelta:1 !reductions;
+ P.add ~gdelta:1 ();
step (ac_nfs_rev f ~si r c m2 t) c m1 v1
end
| _, B.GRef (B.Entry (_, B.Abbr v2) :: _, _) ->
- reductions := O.add ~gdelta:1 !reductions;
+ P.add ~gdelta:1 ();
step (ac_nfs f ~si r c m1 u) c m2 v2
| B.GRef (B.Entry (_, B.Abbr v1) :: _, _), _ ->
- reductions := O.add ~gdelta:1 !reductions;
+ P.add ~gdelta:1 ();
step (ac_nfs_rev f ~si r c m2 t) c m1 v1
| B.Bind (a1, (B.Abst w1 as b1), t1),
B.Bind (a2, (B.Abst w2 as b2), t2) ->
let f r = if r then push g m1 a1 b1 else f false in
ac f ~si r c m1 w1 m2 w2
| B.Sort _, B.Bind (a, b, t) when si ->
+ P.add ~si:1 ();
let f m1 m2 = ac f ~si r c m1 u m2 t in
let f m1 = push (f m1) m2 a b in
push f m1 a b