Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
POTTIER Francois
alphaLib
Commits
af5a3da3
Commit
af5a3da3
authored
Jan 31, 2017
by
POTTIER Francois
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Use cppo macros in the construction of Toolbox.
parent
87136d34
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
112 additions
and
78 deletions
+112
-78
src/AlphaLibMacros.cppo.ml
src/AlphaLibMacros.cppo.ml
+86
-0
src/Makefile
src/Makefile
+9
-2
src/Toolbox.cppo.ml
src/Toolbox.cppo.ml
+13
-76
src/myocamlbuild.ml
src/myocamlbuild.ml
+4
-0
No files found.
src/AlphaLibMacros.cppo.ml
0 → 100644
View file @
af5a3da3
(* -------------------------------------------------------------------------- *)
(* [copy] returns a copy of its argument where every bound name has been
replaced with a fresh copy, and every free name is unchanged. *)
#
define
__COPY
\
class
[
'
self
]
copy
=
object
(
_
:
'
self
)
\
inherit
[
_
]
map
\
inherit
[
_
]
KitCopy
.
map
\
end
#
define
COPY
(
term
)
\
let
CONCAT
(
copy_
,
term
)
t
=
\
new
copy
#
CONCAT
(
visit_
,
term
)
KitCopy
.
empty
t
(* -------------------------------------------------------------------------- *)
(* [show] converts its argument to a raw term, in a NONHYGIENIC manner, using
[Atom.show] both at free name occurrences and bound name occurrences. It
is a debugging tool. *)
#
define
__SHOW
\
class
[
'
self
]
show
=
object
(
_
:
'
self
)
\
inherit
[
_
]
map
\
inherit
[
_
]
KitShow
.
map
\
end
#
define
SHOW
(
term
)
\
let
CONCAT
(
show_
,
term
)
t
=
\
new
show
#
CONCAT
(
visit_
,
term
)
()
t
(* -------------------------------------------------------------------------- *)
(* [import] converts a raw term to a nominal term that satisfies the Global
Uniqueness Hypothesis, that is, a nominal term where every binding name
occurrence is represented by a unique atom. [import] expects every free
name occurrence to be in the domain of [env]. If that is not the case,
the exception [Unbound] is raised. *)
(* TEMPORARY use string * loc so as to be able to give a location *)
#
define
__IMPORT
\
class
[
'
self
]
import
=
object
(
_
:
'
self
)
\
inherit
[
_
]
map
\
inherit
[
_
]
KitImport
.
map
\
end
#
define
IMPORT
(
term
)
\
let
CONCAT
(
import_
,
term
)
env
t
=
\
new
import
#
CONCAT
(
visit_
,
term
)
env
t
(* -------------------------------------------------------------------------- *)
(* [export] converts a nominal term to a raw term, in a hygienic manner. This
is the proper way of displaying a term. [export] expects every free name
occurrence to be in the domain of [env]. *)
#
define
__EXPORT
\
class
[
'
self
]
export
=
object
(
_
:
'
self
)
\
inherit
[
_
]
map
\
inherit
[
_
]
KitExport
.
map
\
end
#
define
EXPORT
(
term
)
\
let
CONCAT
(
export_
,
term
)
env
t
=
\
new
export
#
CONCAT
(
visit_
,
term
)
env
t
(* -------------------------------------------------------------------------- *)
(* [size] computes the size of its argument. *)
(* Beware: this counts the nodes whose type is [term], but does not count the
nodes of other types. *)
#
define
__SIZE
\
class
[
'
self
]
size
=
object
(
_
:
'
self
)
\
inherit
[
_
]
reduce
as
super
\
inherit
[
_
]
KitTrivial
.
reduce
\
inherit
[
_
]
VisitorsRuntime
.
addition_monoid
\
method
!
CONCAT
(
visit_
,
term
)
env
t
=
\
1
+
super
#
CONCAT
(
visit_
,
term
)
env
t
\
end
#
define
SIZE
(
term
)
\
let
CONCAT
(
size_
,
term
)
t
=
\
new
size
#
CONCAT
(
visit_
,
term
)
()
t
src/Makefile
View file @
af5a3da3
...
...
@@ -8,12 +8,19 @@ PACKAGE := \
TARGET
:=
\
$(
patsubst
%,
$(PACKAGE)
.%,a cma cmi cmo cmx cmxa o
)
\
PWD
:=
\
$(
shell
pwd
)
OCAMLBUILD
:=
\
ocamlbuild
\
-j
0
\
-use-ocamlfind
\
-classic-display
\
-cflags
"-g"
-lflags
"-g"
-cflags
"-g"
-lflags
"-g"
\
-plugin-tag
'package(cppo_ocamlbuild)'
\
-tag
"cppo_I(
$(PWD)
)"
\
# TEMPORARY cppo_I should not be required
# TEMPORARY a dependency computation on .cppo.ml files should be carried out
# ------------------------------------------------------------------------------
...
...
src/Toolbox.ml
→
src/Toolbox.
cppo.
ml
View file @
af5a3da3
#
include
"AlphaLibMacros.cppo.ml"
(* -------------------------------------------------------------------------- *)
(* This functor is applied to a type of terms, equipped with visitor classes.
...
...
@@ -89,85 +91,20 @@ type debruijn_term =
(* -------------------------------------------------------------------------- *)
(* [size] computes the size of its argument. *)
(* Beware: this counts the nodes whose type is [term] nodes, but does not count
the nodes of other types. *)
class
[
'
self
]
size
=
object
(
_
:
'
self
)
inherit
[
_
]
reduce
as
super
inherit
[
_
]
KitTrivial
.
reduce
inherit
[
_
]
VisitorsRuntime
.
addition_monoid
method
!
visit_term
env
t
=
1
+
super
#
visit_term
env
t
end
let
size
:
'
fn
'
bn
.
(
'
fn
,
'
bn
)
term
->
int
=
fun
t
->
new
size
#
visit_term
()
t
(* -------------------------------------------------------------------------- *)
(* [show] converts its argument to a raw term, in a NONHYGIENIC manner, using
[Atom.show] both at free name occurrences and bound name occurrences. It
is a debugging tool. *)
class
[
'
self
]
show
=
object
(
_
:
'
self
)
inherit
[
_
]
map
inherit
[
_
]
KitShow
.
map
end
let
show
:
nominal_term
->
raw_term
=
new
show
#
visit_term
()
(* -------------------------------------------------------------------------- *)
(* [copy] returns a copy of its argument where every bound name has been
replaced with a fresh copy, and every free name is unchanged. *)
class
[
'
self
]
copy
=
object
(
_
:
'
self
)
inherit
[
_
]
map
inherit
[
_
]
KitCopy
.
map
end
let
copy
:
nominal_term
->
nominal_term
=
new
copy
#
visit_term
KitCopy
.
empty
(* -------------------------------------------------------------------------- *)
(* [import] converts a raw term to a nominal term that satisfies the Global
Uniqueness Hypothesis, that is, a nominal term where every binding name
occurrence is represented by a unique atom. [import] expects every free
name occurrence to be in the domain of [env]. If that is not the case,
the exception [Unbound] is raised. *)
(* TEMPORARY use string * loc so as to be able to give a location *)
(* TEMPORARY maybe [module Import = KitImport] so that the user does not
have to know about the kits at all. *)
__COPY
COPY
(
term
)
exception
Unbound
=
KitImport
.
Unbound
__SHOW
SHOW
(
term
)
class
[
'
self
]
import
=
object
(
_
:
'
self
)
inherit
[
_
]
map
inherit
[
_
]
KitImport
.
map
end
let
import
:
KitImport
.
env
->
raw_term
->
nominal_term
=
new
import
#
visit_term
(* -------------------------------------------------------------------------- *)
(* [export] converts a nominal term to a raw term, in a hygienic manner. This
is the proper way of displaying a term. [export] expects every free name
occurrence to be in the domain of [env]. *)
__IMPORT
IMPORT
(
term
)
class
[
'
self
]
export
=
object
(
_
:
'
self
)
inherit
[
_
]
map
inherit
[
_
]
KitExport
.
map
end
__EXPORT
EXPORT
(
term
)
let
export
:
KitExport
.
env
->
nominal_term
->
raw_term
=
new
export
#
visit_
term
__SIZE
SIZE
(
term
)
(* -------------------------------------------------------------------------- *)
...
...
@@ -241,7 +178,7 @@ class subst = object
|
u
->
(* Do not forget to copy the term that is being grafted, so as
to maintain the GUH. *)
copy
u
copy
_term
u
|
exception
Not_found
->
this
end
...
...
src/myocamlbuild.ml
0 → 100644
View file @
af5a3da3
let
()
=
Ocamlbuild_plugin
.
dispatch
(
fun
phase
->
Ocamlbuild_cppo
.
dispatcher
phase
)
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