diff --git a/src/AlphaLibMacros.cppo.ml b/src/AlphaLibMacros.cppo.ml new file mode 100644 index 0000000000000000000000000000000000000000..0ebff6700ae0a46a75e5dcb8bfbb632b8dc76405 --- /dev/null +++ b/src/AlphaLibMacros.cppo.ml @@ -0,0 +1,86 @@ +(* -------------------------------------------------------------------------- *) + +(* [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 diff --git a/src/Makefile b/src/Makefile index 7bd730e79f44247efcb000863530e7ce0b970fb6..26b0c23637818ecb37d02e700b143076a4778419 100644 --- a/src/Makefile +++ b/src/Makefile @@ -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 # ------------------------------------------------------------------------------ diff --git a/src/Toolbox.ml b/src/Toolbox.cppo.ml similarity index 76% rename from src/Toolbox.ml rename to src/Toolbox.cppo.ml index 687a83dfe61e1d87d5506728140b2b62fdab67cb..925ecd3f2184dc98a0a3af916fb709b54bcd7461 100644 --- a/src/Toolbox.ml +++ b/src/Toolbox.cppo.ml @@ -1,3 +1,5 @@ +#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 diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml new file mode 100644 index 0000000000000000000000000000000000000000..6024ea0d7bac54683fc0f603fa91ac7bc617afe4 --- /dev/null +++ b/src/myocamlbuild.ml @@ -0,0 +1,4 @@ +let () = + Ocamlbuild_plugin.dispatch (fun phase -> + Ocamlbuild_cppo.dispatcher phase + )