Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
A
alphaLib
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
POTTIER Francois
alphaLib
Commits
64ecdb42
Commit
64ecdb42
authored
Feb 08, 2017
by
POTTIER Francois
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Exchange the order of the parameters of [term].
parent
1020666b
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
14 additions
and
14 deletions
+14
-14
demos/basic/Term.ml
demos/basic/Term.ml
+3
-3
demos/system-F-type/F.cppo.ml
demos/system-F-type/F.cppo.ml
+2
-2
src/ToolboxInput.ml
src/ToolboxInput.ml
+9
-9
No files found.
demos/basic/Term.ml
View file @
64ecdb42
open
AlphaLib
open
BindingForms
type
(
'
fn
,
'
b
n
)
term
=
type
(
'
bn
,
'
f
n
)
term
=
|
TVar
of
'
fn
|
TLambda
of
(
'
bn
,
(
'
fn
,
'
b
n
)
term
)
abs
|
TApp
of
(
'
fn
,
'
bn
)
term
*
(
'
fn
,
'
b
n
)
term
|
TLambda
of
(
'
bn
,
(
'
bn
,
'
f
n
)
term
)
abs
|
TApp
of
(
'
bn
,
'
fn
)
term
*
(
'
bn
,
'
f
n
)
term
[
@@
deriving
...
...
demos/system-F-type/F.cppo.ml
View file @
64ecdb42
...
...
@@ -11,7 +11,7 @@ type tyvar =
(* Types. *)
#
define
TYP
(
'
fn
,
'
b
n
)
typ
#
define
TYP
(
'
bn
,
'
f
n
)
typ
type
TYP
=
|
TyVar
of
'
fn
...
...
@@ -25,7 +25,7 @@ and tevar = (string[@opaque])
(* Terms. *)
#
define
TERM
(
'
fn
,
'
b
n
)
term
#
define
TERM
(
'
bn
,
'
f
n
)
term
and
TERM
=
|
TeVar
of
tevar
...
...
src/ToolboxInput.ml
View file @
64ecdb42
module
type
INPUT
=
sig
(* Suppose there is a type of terms, which is parameterized over the
representations of
free name occurrences and binding
name occurrences. *)
representations of
binding name occurrences and free
name occurrences. *)
type
(
'
fn
,
'
b
n
)
term
type
(
'
bn
,
'
f
n
)
term
(* Suppose the type of terms is equipped with the following visitors. *)
...
...
@@ -22,21 +22,21 @@ module type INPUT = sig
class
virtual
[
'
self
]
iter
:
object
(
'
self
)
method
private
virtual
extend
:
'
bn
->
'
env
->
'
env
method
private
virtual
visit_'fn
:
'
env
->
'
fn
->
_
method
visit_term
:
'
env
->
(
'
fn
,
'
b
n
)
term
->
unit
method
visit_term
:
'
env
->
(
'
bn
,
'
f
n
)
term
->
unit
end
class
virtual
[
'
self
]
map
:
object
(
'
self
)
method
private
virtual
extend
:
'
bn1
->
'
env
->
'
bn2
*
'
env
method
private
virtual
visit_'fn
:
'
env
->
'
fn1
->
'
fn2
method
visit_term
:
'
env
->
(
'
fn1
,
'
bn1
)
term
->
(
'
fn2
,
'
b
n2
)
term
method
private
visit_TVar
:
'
env
->
'
fn1
->
(
'
fn2
,
'
b
n2
)
term
method
visit_term
:
'
env
->
(
'
bn1
,
'
fn1
)
term
->
(
'
bn2
,
'
f
n2
)
term
method
private
visit_TVar
:
'
env
->
'
fn1
->
(
'
bn2
,
'
f
n2
)
term
end
class
virtual
[
'
self
]
endo
:
object
(
'
self
)
method
private
virtual
extend
:
'
bn
->
'
env
->
'
bn
*
'
env
method
private
virtual
visit_'fn
:
'
env
->
'
fn
->
'
fn
method
visit_term
:
'
env
->
(
'
fn
,
'
bn
)
term
->
(
'
fn
,
'
b
n
)
term
method
private
visit_TVar
:
'
env
->
(
'
fn
,
'
bn
)
term
->
'
fn
->
(
'
fn
,
'
b
n
)
term
method
visit_term
:
'
env
->
(
'
bn
,
'
fn
)
term
->
(
'
bn
,
'
f
n
)
term
method
private
visit_TVar
:
'
env
->
(
'
bn
,
'
fn
)
term
->
'
fn
->
(
'
bn
,
'
f
n
)
term
end
class
virtual
[
'
self
]
reduce
:
object
(
'
self
)
...
...
@@ -45,13 +45,13 @@ module type INPUT = sig
method
private
virtual
zero
:
'
z
method
private
virtual
plus
:
'
z
->
'
z
->
'
z
method
private
virtual
restrict
:
'
bn
->
'
z
->
'
z
method
visit_term
:
'
env
->
(
'
fn
,
'
b
n
)
term
->
'
z
method
visit_term
:
'
env
->
(
'
bn
,
'
f
n
)
term
->
'
z
end
class
virtual
[
'
self
]
iter2
:
object
(
'
self
)
method
private
virtual
extend
:
'
bn1
->
'
bn2
->
'
env
->
'
env
method
private
virtual
visit_'fn
:
'
env
->
'
fn1
->
'
fn2
->
_
method
visit_term
:
'
env
->
(
'
fn1
,
'
bn1
)
term
->
(
'
fn2
,
'
b
n2
)
term
->
unit
method
visit_term
:
'
env
->
(
'
bn1
,
'
fn1
)
term
->
(
'
bn2
,
'
f
n2
)
term
->
unit
end
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