Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
POTTIER Francois
alphaLib
Commits
fef97e45
Commit
fef97e45
authored
Feb 20, 2017
by
POTTIER Francois
Browse files
Move [iter] and [iter2] higher up in the file.
parent
c98487ad
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/BindingForms.ml
View file @
fef97e45
...
...
@@ -51,6 +51,92 @@ type ('bn, 't, 'u) telescope =
(* -------------------------------------------------------------------------- *)
(* [iter] *)
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
visit_abs
:
'
term
.
_
->
(
'
env
->
'
term
->
unit
)
->
'
env
->
(
'
bn
,
'
term
)
abs
->
unit
=
fun
_
visit_term
env
(
x
,
t
)
->
let
env'
=
self
#
extend
x
env
in
visit_term
env'
t
method
private
visit_tele
:
'
t
.
(
'
env
->
'
t
->
unit
)
->
'
env
->
(
'
bn
,
'
t
)
tele
->
'
env
=
fun
visit_t
env
xts
->
match
xts
with
|
[]
->
env
|
(
x
,
t
)
::
xts
->
visit_t
env
t
;
let
env
=
self
#
extend
x
env
in
self
#
visit_tele
visit_t
env
xts
method
private
visit_telescope
:
'
t
'
u
.
_
->
(
'
env
->
'
t
->
unit
)
->
(
'
env
->
'
u
->
unit
)
->
'
env
->
(
'
bn
,
'
t
,
'
u
)
telescope
->
unit
=
fun
_
visit_t
visit_u
env
(
xts
,
u
)
->
let
env
=
self
#
visit_tele
visit_t
env
xts
in
visit_u
env
u
end
(* -------------------------------------------------------------------------- *)
(* [iter2] *)
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
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
visit_term
env'
t1
t2
method
private
visit_tele
:
'
t1
'
t2
.
(
'
env
->
'
t1
->
'
t2
->
'
z
)
->
'
env
->
(
'
bn1
,
'
t1
)
tele
->
(
'
bn2
,
'
t2
)
tele
->
'
env
=
fun
visit_t
env
xts1
xts2
->
match
xts1
,
xts2
with
|
[]
,
[]
->
env
|
(
x1
,
t1
)
::
xts1
,
(
x2
,
t2
)
::
xts2
->
visit_t
env
t1
t2
;
let
env
=
self
#
extend
x1
x2
env
in
self
#
visit_tele
visit_t
env
xts1
xts2
|
_
,
_
->
VisitorsRuntime
.
fail
()
method
private
visit_telescope
:
'
t1
'
t2
'
u1
'
u2
.
_
->
(
'
env
->
'
t1
->
'
t2
->
'
z
)
->
(
'
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
env
=
self
#
visit_tele
visit_t
env
xts1
xts2
in
visit_u
env
u1
u2
;
end
(* -------------------------------------------------------------------------- *)
(* [map] *)
class
virtual
[
'
self
]
map
=
object
(
self
:
'
self
)
...
...
@@ -147,89 +233,3 @@ class virtual ['self] endo = object (self : 'self)
xts2
,
u2
end
(* -------------------------------------------------------------------------- *)
(* [iter] *)
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
visit_abs
:
'
term
.
_
->
(
'
env
->
'
term
->
unit
)
->
'
env
->
(
'
bn
,
'
term
)
abs
->
unit
=
fun
_
visit_term
env
(
x
,
t
)
->
let
env'
=
self
#
extend
x
env
in
visit_term
env'
t
method
private
visit_tele
:
'
t
.
(
'
env
->
'
t
->
unit
)
->
'
env
->
(
'
bn
,
'
t
)
tele
->
'
env
=
fun
visit_t
env
xts
->
match
xts
with
|
[]
->
env
|
(
x
,
t
)
::
xts
->
visit_t
env
t
;
let
env
=
self
#
extend
x
env
in
self
#
visit_tele
visit_t
env
xts
method
private
visit_telescope
:
'
t
'
u
.
_
->
(
'
env
->
'
t
->
unit
)
->
(
'
env
->
'
u
->
unit
)
->
'
env
->
(
'
bn
,
'
t
,
'
u
)
telescope
->
unit
=
fun
_
visit_t
visit_u
env
(
xts
,
u
)
->
let
env
=
self
#
visit_tele
visit_t
env
xts
in
visit_u
env
u
end
(* -------------------------------------------------------------------------- *)
(* [iter2] *)
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
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
visit_term
env'
t1
t2
method
private
visit_tele
:
'
t1
'
t2
.
(
'
env
->
'
t1
->
'
t2
->
'
z
)
->
'
env
->
(
'
bn1
,
'
t1
)
tele
->
(
'
bn2
,
'
t2
)
tele
->
'
env
=
fun
visit_t
env
xts1
xts2
->
match
xts1
,
xts2
with
|
[]
,
[]
->
env
|
(
x1
,
t1
)
::
xts1
,
(
x2
,
t2
)
::
xts2
->
visit_t
env
t1
t2
;
let
env
=
self
#
extend
x1
x2
env
in
self
#
visit_tele
visit_t
env
xts1
xts2
|
_
,
_
->
VisitorsRuntime
.
fail
()
method
private
visit_telescope
:
'
t1
'
t2
'
u1
'
u2
.
_
->
(
'
env
->
'
t1
->
'
t2
->
'
z
)
->
(
'
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
env
=
self
#
visit_tele
visit_t
env
xts1
xts2
in
visit_u
env
u1
u2
;
end
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment