Commit af102098 authored by POTTIER Francois's avatar POTTIER Francois

Moved the class [BindingForms.map2] to the attic.

parent 6784d7bb
......@@ -191,52 +191,6 @@ end
(* -------------------------------------------------------------------------- *)
(* [map2] *)
class virtual ['self] map2 = object (self : 'self)
method private visit_'bn: void -> void -> void -> void
= fun _ _ _ -> assert false
method private virtual extend: 'bn1 -> 'bn2 -> 'env -> 'bn3 * 'env
method private visit_abs: 'term1 'term2 'term3 .
_ ->
('env -> 'term1 -> 'term2 -> 'term3) ->
'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs -> ('bn3, 'term3) abs
= fun _ visit_term env (x1, t1) (x2, t2) ->
let x3, env' = self#extend x1 x2 env in
x3, visit_term env' t1 t2
method private visit_tele: 't1 't2 't3 .
('env -> 't1 -> 't2 -> 't3) ->
'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele -> ('bn3, 't3) tele * 'env
= fun visit_t env xts1 xts2 ->
match xts1, xts2 with
| [], [] ->
[], env
| (x1, t1) :: xts1, (x2, t2) :: xts2 ->
let t3 = visit_t env t1 t2 in
let x3, env = self#extend x1 x2 env in
let xts3, env = self#visit_tele visit_t env xts1 xts2 in
(x3, t3) :: xts3, env
| _, _ ->
VisitorsRuntime.fail()
method private visit_telescope: 't1 't2 't3 'u1 'u2 'u3 .
_ ->
('env -> 't1 -> 't2 -> 't3) ->
('env -> 'u1 -> 'u2 -> 'u3) ->
'env -> ('bn1, 't1, 'u1) telescope -> ('bn2, 't2, 'u2) telescope -> ('bn3, 't3, 'u3) telescope
= fun _ visit_t visit_u env (xts1, u1) (xts2, u2) ->
let xts3, env = self#visit_tele visit_t env xts1 xts2 in
let u3 = visit_u env u1 u2 in
xts3, u3
end
(* -------------------------------------------------------------------------- *)
(* [reduce2] *)
class virtual ['self] reduce2 = object (self : 'self)
......
(* -------------------------------------------------------------------------- *)
(* [map2] *)
class virtual ['self] map2 = object (self : 'self)
method private visit_'bn: void -> void -> void -> void
= fun _ _ _ -> assert false
method private virtual extend: 'bn1 -> 'bn2 -> 'env -> 'bn3 * 'env
method private visit_abs: 'term1 'term2 'term3 .
_ ->
('env -> 'term1 -> 'term2 -> 'term3) ->
'env -> ('bn1, 'term1) abs -> ('bn2, 'term2) abs -> ('bn3, 'term3) abs
= fun _ visit_term env (x1, t1) (x2, t2) ->
let x3, env' = self#extend x1 x2 env in
x3, visit_term env' t1 t2
method private visit_tele: 't1 't2 't3 .
('env -> 't1 -> 't2 -> 't3) ->
'env -> ('bn1, 't1) tele -> ('bn2, 't2) tele -> ('bn3, 't3) tele * 'env
= fun visit_t env xts1 xts2 ->
match xts1, xts2 with
| [], [] ->
[], env
| (x1, t1) :: xts1, (x2, t2) :: xts2 ->
let t3 = visit_t env t1 t2 in
let x3, env = self#extend x1 x2 env in
let xts3, env = self#visit_tele visit_t env xts1 xts2 in
(x3, t3) :: xts3, env
| _, _ ->
VisitorsRuntime.fail()
method private visit_telescope: 't1 't2 't3 'u1 'u2 'u3 .
_ ->
('env -> 't1 -> 't2 -> 't3) ->
('env -> 'u1 -> 'u2 -> 'u3) ->
'env -> ('bn1, 't1, 'u1) telescope -> ('bn2, 't2, 'u2) telescope -> ('bn3, 't3, 'u3) telescope
= fun _ visit_t visit_u env (xts1, u1) (xts2, u2) ->
let xts3, env = self#visit_tele visit_t env xts1 xts2 in
let u3 = visit_u env u1 u2 in
xts3, u3
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