Commit 7d2755a0 authored by POTTIER Francois's avatar POTTIER Francois

In [BindingForms], implement [iter] directly instead of via [reduce].

parent add0d365
......@@ -69,9 +69,6 @@ type ('bn, 't, 'u) telescope =
types of bound names and environments. On the contrary, each kit comes
with certain specific types of bound names and environments. *)
(* Because [iter] and [iter2] are special cases of [reduce] and [reduce2],
respectively, we define them that way, so as to save effort. *)
(* -------------------------------------------------------------------------- *)
(* [map] *)
......@@ -198,71 +195,54 @@ end
(* -------------------------------------------------------------------------- *)
(* [reduce] *)
class virtual ['self] reduce = object (self : 'self)
(* [iter] *)
inherit ['z] VisitorsRuntime.monoid
class virtual ['self] iter = object (self : 'self)
method private visit_'bn: void -> void -> void
= fun _ _ -> assert false
method private virtual extend: 'bn -> 'env -> 'env
method private virtual restrict: 'bn -> 'z -> 'z
method private visit_abs: 'term .
_ ->
('env -> 'term -> 'z) ->
'env -> ('bn, 'term) abs -> 'z
('env -> 'term -> unit) ->
'env -> ('bn, 'term) abs -> unit
= fun _ visit_term env (x, t) ->
let env' = self#extend x env in
self#restrict x (visit_term env' t)
visit_term env' t
method private visit_def: 't 'u .
_ ->
('env -> 't -> 'z) ->
('env -> 'u -> 'z) ->
'env -> ('bn, 't, 'u) def -> 'z
('env -> 't -> unit) ->
('env -> 'u -> unit) ->
'env -> ('bn, 't, 'u) def -> unit
= fun _ visit_t visit_u env (recursive, x, t, u) ->
let env' = self#extend x env in
let zt = visit_t (choose recursive env env') t in
let zu = self#restrict x (visit_u env' u) in
self#plus zt zu
visit_t (choose recursive env env') t;
visit_u env' u
method private visit_tele: 't .
('env -> 't -> 'z) ->
'env -> ('bn, 't) tele -> 'z * 'env
('env -> 't -> unit) ->
'env -> ('bn, 't) tele -> 'env
= fun visit_t env xts ->
match xts with
| [] ->
self#zero, env
env
| (x, t) :: xts ->
let zt = visit_t env t in
visit_t env t;
let env = self#extend x env in
let zxts, env = self#visit_tele visit_t env xts in
self#plus zt zxts, env
self#visit_tele visit_t env xts
method private visit_telescope: 't 'u.
_ ->
('env -> 't -> 'z) ->
('env -> 'u -> 'z) ->
'env -> ('bn, 't, 'u) telescope -> 'z
('env -> 't -> unit) ->
('env -> 'u -> unit) ->
'env -> ('bn, 't, 'u) telescope -> unit
= fun _ visit_t visit_u env (xts, u) ->
let zxts, env = self#visit_tele visit_t env xts in
let zu = visit_u env u in
self#plus zxts zu
end
(* -------------------------------------------------------------------------- *)
(* [iter] *)
let env = self#visit_tele visit_t env xts in
visit_u env u
class virtual ['self] iter = object (_ : 'self)
inherit ['self] reduce
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