Commit 1c919cc7 authored by POTTIER Francois's avatar POTTIER Francois

Remove [reduce2] and implement [iter2] directly.

parent af102098
......@@ -191,39 +191,34 @@ end
(* -------------------------------------------------------------------------- *)
(* [reduce2] *)
class virtual ['self] reduce2 = object (self : 'self)
(* [iter2] *)
inherit ['z] VisitorsRuntime.monoid
class virtual ['self] iter2 = object (self : 'self)
method private visit_'bn: void -> void -> void -> void
= fun _ _ _ -> assert false
method private virtual extend: 'bn1 -> 'bn2 -> 'env -> 'env
method private virtual restrict: 'bn1 -> 'bn2 -> 'z -> 'z
method private visit_abs: 'term1 'term2 .
_ ->
('env -> 'term1 -> 'term2 -> 'z) ->
'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs -> 'z
= fun _ visit_term env (x1, t1) (x2, t2) ->
let env' = self#extend x1 x2 env in
self#restrict x1 x2 (visit_term env' t1 t2)
visit_term env' t1 t2
method private visit_tele: 't1 't2 .
('env -> 't1 -> 't2 -> 'z) ->
'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele -> 'z * 'env
'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele -> 'env
= fun visit_t env xts1 xts2 ->
match xts1, xts2 with
| [], [] ->
self#zero, env
env
| (x1, t1) :: xts1, (x2, t2) :: xts2 ->
let zt = visit_t env t1 t2 in
visit_t env t1 t2;
let env = self#extend x1 x2 env in
let zxts, env = self#visit_tele visit_t env xts1 xts2 in
self#plus zt zxts, env
self#visit_tele visit_t env xts1 xts2
| _, _ ->
VisitorsRuntime.fail()
......@@ -233,18 +228,7 @@ class virtual ['self] reduce2 = object (self : 'self)
('env -> 'u1 -> 'u2 -> 'z) ->
'env -> ('bn1, 't1, 'u1) telescope -> ('bn2, 't2, 'u2) telescope -> 'z
= fun _ visit_t visit_u env (xts1, u1) (xts2, u2) ->
let zxts, env = self#visit_tele visit_t env xts1 xts2 in
let zu = visit_u env u1 u2 in
self#plus zxts zu
end
(* -------------------------------------------------------------------------- *)
(* [iter2] *)
let env = self#visit_tele visit_t env xts1 xts2 in
visit_u env u1 u2;
class virtual ['self] iter2 = object (_ : 'self)
inherit ['self] reduce2
inherit [_] VisitorsRuntime.unit_monoid
method private restrict _ _ () = ()
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment