Commit b3f82b9e authored by POTTIER Francois's avatar POTTIER Francois

Implemented [reduce] for telescopes.

parent 80608b85
...@@ -202,7 +202,7 @@ end ...@@ -202,7 +202,7 @@ end
class virtual ['self] reduce = object (self : 'self) class virtual ['self] reduce = object (self : 'self)
method private virtual plus: 'z -> 'z -> 'z inherit ['z] VisitorsRuntime.monoid
method private visit_'bn: void -> void -> void method private visit_'bn: void -> void -> void
= fun _ _ -> assert false = fun _ _ -> assert false
...@@ -230,6 +230,29 @@ class virtual ['self] reduce = object (self : 'self) ...@@ -230,6 +230,29 @@ class virtual ['self] reduce = object (self : 'self)
let zu = self#restrict x (visit_u env' u) in let zu = self#restrict x (visit_u env' u) in
self#plus zt zu self#plus zt zu
method visit_tele: 't .
('env -> 't -> 'z) ->
'env -> ('bn, 't) tele -> 'z * 'env
= fun visit_t env xts ->
match xts with
| [] ->
self#zero, env
| (x, t) :: xts ->
let zt = visit_t env t in
let env = self#extend x env in
let zxts, env = self#visit_tele visit_t env xts in
self#plus zt zxts, env
method visit_telescope: 't 'u.
_ ->
('env -> 't -> 'z) ->
('env -> 'u -> 'z) ->
'env -> ('bn, 't, 'u) telescope -> 'z
= 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 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