Skip to content

GitLab

A
alphaLib
Commit 2c528d10 authored by POTTIER Francois's avatar POTTIER Francois
Browse files
Options

Merge branch 'master' of gitlab.inria.fr:fpottier/alphaLib

parents f34affb2 161d3f5f
Hide whitespace changes
Inline Side-by-side
Showing with 205 additions and 182 deletions
TODO
View file @ 2c528d10
......@@ -58,6 +58,8 @@ Look at the visitors in Why3.
TODO (POSSIBLY):
Change all of the macros to build objects on the fly instead of using classes?
Avoid reduce, which is not tail recursive.
Use iter in [ba] and [fa].
That should save a constant factor in stack usage?
demos/basic/Main.ml
View file @ 2c528d10
......@@ -243,8 +243,8 @@ let () =
TApp (subst1 u x t1, subst1 u x t2))
end
);
let x = Atom.freshh "x"
and y = Atom.freshh "y" in
let x = Atom.fresh "x"
and y = Atom.fresh "y" in
let u = generate_nominal atoms size_of_u in
assert (subst1 u x (TVar x) = u);
assert (subst1 u x (TVar y) = TVar y);
......@@ -330,10 +330,10 @@ let () =
(* Sample terms. *)
let x =
Atom.freshh "x"
Atom.fresh "x"
let y =
Atom.freshh "y"
Atom.fresh "y"
let id =
TLambda (x, TVar x)
......
demos/basic/Term.ml
View file @ 2c528d10
open AlphaLib
open BindingForms
type ('fn, 'bn) term =
type ('bn, 'fn) term =
| TVar of 'fn
| TLambda of ('bn, ('fn, 'bn) term) abs
| TApp of ('fn, 'bn) term * ('fn, 'bn) term
| TLambda of ('bn, ('bn, 'fn) term) abs
| TApp of ('bn, 'fn) term * ('bn, 'fn) term
[@@deriving
......
demos/basic/TermGenerator.ml
View file @ 2c528d10
......@@ -89,7 +89,7 @@ let rec atoms accu k =
if k = 0 then
accu
else
let a = AlphaLib.Atom.freshh "a" in
let a = AlphaLib.Atom.fresh "a" in
atoms (AtomSet.add a accu) (k - 1)
let atoms =
......
demos/system-F-type/F.cppo.ml
View file @ 2c528d10
......@@ -11,7 +11,7 @@ type tyvar =
(* Types. *)
#define TYP ('fn, 'bn) typ
#define TYP ('bn, 'fn) typ
type TYP =
| TyVar of 'fn
......@@ -25,7 +25,7 @@ and tevar = (string[@opaque])
(* Terms. *)
#define TERM ('fn, 'bn) term
#define TERM ('bn, 'fn) term
and TERM =
| TeVar of tevar
......@@ -93,10 +93,6 @@ __AVOID
AVOID(typ)
AVOID(term)
__SHOW
SHOW(typ)
SHOW(term)
__IMPORT
IMPORT(typ)
IMPORT(term)
......@@ -105,6 +101,10 @@ __EXPORT
EXPORT(typ)
EXPORT(term)
__SHOW
SHOW(typ)
SHOW(term)
__SIZE
SIZE(typ)
SIZE(term)
......
src/AlphaLibMacros.cppo.ml
View file @ 2c528d10
......@@ -3,9 +3,9 @@
#define VISIT(term) \
CONCAT(visit_, term)
(* -------------------------------------------------------------------------- *)
(* For comments about the operations that follow, see [ToolboxOutput.ml]. *)
(* [fa_term] computes the set of the free atoms of a term. *)
(* -------------------------------------------------------------------------- *)
#define FA_CLASS __fa
#define FA_FUN(term) CONCAT(fa_, term)
......@@ -22,14 +22,6 @@
(* -------------------------------------------------------------------------- *)
(* [filter_term p t] returns a free atom of the term [t] that satisfies the
predicate [p], if such an atom exists. *)
(* [closed_term t] tests whether the term [t] is closed, that is, whether
[t] has no free atom. *)
(* [occurs_term x t] tests whether the atom [x] occurs free in the term [t]. *)
#define FILTER_CLASS __filter
#define FILTER_FUN(term) CONCAT(filter_, term)
#define CLOSED_FUN(term) CONCAT(closed_, term)
......@@ -55,8 +47,6 @@
(* -------------------------------------------------------------------------- *)
(* [ba_term] computes the set of bound atoms of a term. *)
#define BA_CLASS __ba
#define BA_FUN(term) CONCAT(ba_, term)
......@@ -72,11 +62,6 @@
(* -------------------------------------------------------------------------- *)
(* [avoids_term env t] tests whether the bound atoms of [t] avoid the set [env],
that is, [ba(t) # env]. It also checks that there is no shadowing within [t],
that is, no atom is bound twice along a branch. It returns [true] if these
two conditions are satisfied. *)
#define AVOIDS_CLASS __avoids
#define AVOIDS_FUN(term) CONCAT(avoids_, term)
......@@ -92,17 +77,6 @@
(* -------------------------------------------------------------------------- *)
(* [guq_term] tests whether a term satisfies global uniqueness, that is, no atom
is bound twice within this term (not even along different branches). *)
(* [guq_terms] checks that a list of terms satisfies global uniqueness, that is,
no atom is bound twice within this list (not even within two distinct list
elements). *)
(* [guq_term] and [guq_terms] should be used only in debugging mode, typically
in an [assert] construct. They print the identity of one offending atom on
the standard error channel. *)
#define GUQ_CLASS __guq
#define GUQ_FUN(term) CONCAT(guq_, term)
#define GUQS_FUN(term) GUQ_FUN(CONCAT(term, s))
......@@ -127,9 +101,6 @@
(* -------------------------------------------------------------------------- *)
(* [copy_term] 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 __copy
#define COPY_FUN(term) CONCAT(copy_, term)
......@@ -145,10 +116,6 @@
(* -------------------------------------------------------------------------- *)
(* [avoid_term bad] returns a copy of its argument where some bound names have
been replaced with a fresh copy, so as to ensure that no bound name is in
the set [bad]. *)
#define AVOID_CLASS __avoid
#define AVOID_FUN(term) CONCAT(avoid_, term)
......@@ -164,53 +131,22 @@
(* -------------------------------------------------------------------------- *)
(* [show_term] 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 __show
#define SHOW_FUN(term) CONCAT(show_, term)
#define __SHOW \
class ['self] SHOW_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitShow.map \
end \
#define SHOW(term) \
let SHOW_FUN(term) t = \
new SHOW_CLASS # VISIT(term) () t \
(* -------------------------------------------------------------------------- *)
(* [import_term] 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 __import
#define IMPORT_FUN(term) CONCAT(import_, term)
#define __IMPORT \
exception Unbound = KitImport.Unbound \
class ['self] IMPORT_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitImport.map \
end \
#define IMPORT(term) \
let IMPORT_FUN(term) env t = \
new IMPORT_CLASS # VISIT(term) env t \
(object \
inherit [_] map \
inherit [_] KitImport.map \
end) # VISIT(term) env t \
(* -------------------------------------------------------------------------- *)
(* [export_term] 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 __export
#define EXPORT_FUN(term) CONCAT(export_, term)
......@@ -226,10 +162,20 @@
(* -------------------------------------------------------------------------- *)
(* [size_term] computes the size of its argument. *)
#define SHOW_CLASS __show
#define SHOW_FUN(term) CONCAT(show_, term)
(* Beware: this counts the nodes whose type is [term], but does not count the
nodes of other types. *)
#define __SHOW \
class ['self] SHOW_CLASS = object (_ : 'self) \
inherit [_] map \
inherit [_] KitShow.map \
end \
#define SHOW(term) \
let SHOW_FUN(term) t = \
new SHOW_CLASS # VISIT(term) () t \
(* -------------------------------------------------------------------------- *)
#define SIZE_CLASS __size
#define SIZE_FUN(term) CONCAT(size_, term)
......@@ -249,8 +195,6 @@
(* -------------------------------------------------------------------------- *)
(* [equiv_term] tests whether two terms are alpha-equivalent. *)
#define EQUIV_CLASS __equiv
#define EQUIV_FUN(term) CONCAT(equiv_, term)
......@@ -268,26 +212,6 @@
(* -------------------------------------------------------------------------- *)
(* [subst_thing_term] applies a substitution to a nominal term,
yielding a nominal term. *)
(* [subst_thing_term1] applies a singleton substitution to a nominal term,
yielding a nominal term. *)
(* A substitution is a finite map of atoms to nominal things. Things need not
be terms: this is a thing-in-term substitution, substituting things for
variables in terms. *)
(* When applying a substitution [sigma] to a term [t], the GUH guarantees that
the free atoms of (the codomain of) [sigma] cannot be captured by a binder
within [t]. The GUH also guarantees that a binder within [t] cannot appear
in the domain of [sigma], which means that we can go down into [t] and apply
[sigma] to every variable. *)
(* Global uniqueness can be preserved, if desired, by copying the things that
are grafted into [t]. The user decides which [copy] operation should be used.
It could be [copy_thing], or it could be the identity. *)
#define SUBST_CLASS(Var) CONCAT(__subst_, Var)
#define SUBST_FUN(Var, term) CONCAT(subst_, CONCAT(Var, CONCAT(_, term)))
#define SUBST_FUN1(Var, term) CONCAT(SUBST_FUN(Var, term), 1)
......
src/Atom.ml
View file @ 2c528d10
......@@ -72,11 +72,11 @@ let allocate () =
assert (number >= 0);
number
(* [freshh hint] produces a fresh atom. *)
(* [fresh hint] produces a fresh atom. *)
(* The argument [hint] must not be a string of digits. *)
let freshh hint =
let fresh hint =
let identity = allocate()
and hint = share (remove_trailing_digits hint) in
{ identity; hint }
......@@ -84,7 +84,7 @@ let freshh hint =
(* [fresha a] returns a fresh atom modeled after the atom [a]. *)
let fresha a =
freshh a.hint
fresh a.hint
(* -------------------------------------------------------------------------- *)
......
src/Atom.mli
View file @ 2c528d10
......@@ -14,7 +14,7 @@ val print: out_channel -> atom -> unit
(* Producing fresh atoms. *)
val freshh: string -> atom
val fresh: string -> atom
val fresha: atom -> atom
(* Comparison of atoms. *)
......
src/KitImport.ml
View file @ 2c528d10
(* This kit serves to construct an [import] function for terms, that is, a
function that transforms strings to atoms. *)
(* We impose the GUH by mapping each binding occurrence to a fresh atom. *)
(* We map every binding occurrence to a fresh atom, so the term that we
produce satisfies global uniqueness. *)
module StringMap =
Map.Make(String)
......@@ -13,7 +14,7 @@ let empty =
StringMap.empty
let extend (x : string) (env : env) : Atom.t * env =
let a = Atom.freshh x in
let a = Atom.fresh x in
let env = StringMap.add x a env in
a, env
......@@ -26,6 +27,6 @@ let lookup (env : env) (x : string) : Atom.t =
raise (Unbound x)
class ['self] map = object (_ : 'self)
method private extend = extend
method private visit_'fn = lookup
method private extend x env = extend x env
method private visit_'fn env x = lookup env x
end
src/Toolbox.cppo.ml
View file @ 2c528d10
open ToolboxInput
(* This functor is applied to a type of terms, equipped with visitor classes.
It produces a toolbox of useful functions that operate on terms. *)
module Make (Term : ToolboxInput.INPUT) = struct
module Make (Term : INPUT) = struct
open Term
include Term
(* -------------------------------------------------------------------------- *)
......@@ -53,15 +55,15 @@ module Make (Term : ToolboxInput.INPUT) = struct
__AVOID
AVOID(term)
__SHOW
SHOW(term)
__IMPORT
IMPORT(term)
__EXPORT
EXPORT(term)
__SHOW
SHOW(term)
__SIZE
SIZE(term)
......
src/Toolbox.mli
View file @ 2c528d10
open ToolboxInput
open ToolboxOutput
(* This functor is applied to a type of terms, equipped with visitor classes.
It produces a toolbox of useful functions that operate on terms. *)
module Make (Term : ToolboxInput.INPUT) : sig
open Term
(* A raw term is one where every name is represented as a string. This form
is typically produced by a parser, and consumed by a printer. It is not
used internally. *)
type raw_term =
(string, string) term
(* A nominal term is one where every name is represented as an atom. Although
this is not visible in this type definition, we may additionally impose a
Global Uniqueness Hypothesis (GUH), that is, we may require every binding
name occurrence to carry a distinct atom. *)
type nominal_term =
(Atom.t, Atom.t) term
val fa_term: nominal_term -> Atom.Set.t
val filter_term: (Atom.t -> bool) -> nominal_term -> Atom.t option
val closed_term: nominal_term -> bool
val occurs_term: Atom.t -> nominal_term -> bool
val ba_term: nominal_term -> Atom.Set.t
val avoids_term: Atom.Set.t -> nominal_term -> bool
val guq_term: nominal_term -> bool
val guq_terms: nominal_term list -> bool
val copy_term: nominal_term -> nominal_term
val avoid_term: Atom.Set.t -> nominal_term -> nominal_term
val show_term: nominal_term -> raw_term
exception Unbound of string (* = KitImport.Unbound *)
val import_term: KitImport.env -> raw_term -> nominal_term
val export_term: KitExport.env -> nominal_term -> raw_term
val size_term: (_, _) term -> int
val equiv_term: nominal_term -> nominal_term -> bool
val subst_TVar_term:
(nominal_term -> nominal_term) ->
nominal_term Atom.Map.t -> nominal_term -> nominal_term
val subst_TVar_term1:
(nominal_term -> nominal_term) ->
nominal_term -> Atom.t -> nominal_term -> nominal_term
end
module Make (Term : INPUT) : OUTPUT
with type ('bn, 'fn) term = ('bn, 'fn) Term.term
src/ToolboxInput.ml
View file @ 2c528d10
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, 'bn) term
type ('bn, 'fn) 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, 'bn) term -> unit
method visit_term : 'env -> ('bn, 'fn) 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, 'bn2) term
method private visit_TVar : 'env -> 'fn1 -> ('fn2, 'bn2) term
method visit_term : 'env -> ('bn1, 'fn1) term -> ('bn2, 'fn2) term
method private visit_TVar : 'env -> 'fn1 -> ('bn2, 'fn2) 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, 'bn) term
method private visit_TVar : 'env -> ('fn, 'bn) term -> 'fn -> ('fn, 'bn) term
method visit_term : 'env -> ('bn, 'fn) term -> ('bn, 'fn) term
method private visit_TVar : 'env -> ('bn, 'fn) term -> 'fn -> ('bn, 'fn) 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, 'bn) term -> 'z
method visit_term : 'env -> ('bn, 'fn) 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, 'bn2) term -> unit
method visit_term : 'env -> ('bn1, 'fn1) term -> ('bn2, 'fn2) term -> unit
end
end
src/ToolboxOutput.ml 0 → 100644
View file @ 2c528d10
module type OUTPUT = sig
(* A type of terms, is parameterized over the representations of binding
name occurrences and free name occurrences. *)
type ('bn, 'fn) term
(* A raw term is one where every name is represented as a string. This form
is typically produced by a parser, and consumed by a printer. It is not
used internally. *)
type raw_term =
(string, string) term
(* A nominal term is one where every name is represented as an atom. Although
this is not visible in this type definition, we may additionally impose a
Global Uniqueness Hypothesis (GUH), that is, we may require every binding
name occurrence to carry a distinct atom. *)
type nominal_term =
(Atom.t, Atom.t) term
(* [fa_term] computes the set of the free atoms of a term. *)
val fa_term: nominal_term -> Atom.Set.t
(* [filter_term p t] returns a free atom of the term [t] that satisfies the
predicate [p], if such an atom exists. *)
val filter_term: (Atom.t -> bool) -> nominal_term -> Atom.t option
(* [closed_term t] tests whether the term [t] is closed, that is, whether
[t] has no free atom. *)
val closed_term: nominal_term -> bool
(* [occurs_term x t] tests whether the atom [x] occurs free in the term [t]. *)
val occurs_term: Atom.t -> nominal_term -> bool
(* [ba_term] computes the set of bound atoms of a term. *)
val ba_term: nominal_term -> Atom.Set.t
(* [avoids_term env t] tests whether the bound atoms of [t] avoid the set [env],
that is, [ba(t) # env]. It also checks that there is no shadowing within [t],
that is, no atom is bound twice along a branch. It returns [true] if these
two conditions are satisfied. *)
val avoids_term: Atom.Set.t -> nominal_term -> bool
(* [guq_term] tests whether a term satisfies global uniqueness, that is, no atom
is bound twice within this term (not even along different branches). *)
(* [guq_terms] checks that a list of terms satisfies global uniqueness, that is,
no atom is bound twice within this list (not even within two distinct list
elements). *)
(* [guq_term] and [guq_terms] should be used only in debugging mode, typically
in an [assert] construct. They print the identity of one offending atom on
the standard error channel. *)
val guq_term: nominal_term -> bool
val guq_terms: nominal_term list -> bool
(* [copy_term] returns a copy of its argument where every bound name has been
replaced with a fresh copy, and every free name is unchanged. *)
val copy_term: nominal_term -> nominal_term
(* [avoid_term bad] returns a copy of its argument where some bound names have
been replaced with a fresh copy, so as to ensure that no bound name is in
the set [bad]. *)
val avoid_term: Atom.Set.t -> nominal_term -> nominal_term
(* [import_term] 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. *)
exception Unbound of string
val import_term: KitImport.env -> raw_term -> nominal_term
(* [export_term] 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]. *)
val export_term: KitExport.env -> nominal_term -> raw_term
(* [show_term] converts its argument to a raw term using [Atom.show] both at
free name occurrences and bound name occurrences. It is in principle a
debugging tool only, as the strings produced by [Atom.show] do not make
sense (at free atoms) and are not beautiful. It is nevertheless a correct
printer IF the term is closed. *)
val show_term: nominal_term -> raw_term
(* [size_term] computes the size of its argument. Beware: this counts the
nodes whose type is [term], but does not count the nodes of other types. *)
val size_term: (_, _) term -> int
(* [equiv_term] tests whether two terms are alpha-equivalent. *)
val equiv_term: nominal_term -> nominal_term -> bool
(* [subst_TVar_term] applies a substitution to a nominal term, yielding a
nominal term. This is a substitution of things for variables; in the
general case, [TVar] could be a constructor of some type [thing] other
than [term]. *)
(* A substitution is a finite map of atoms to things. *)
(* When applying a substitution [sigma] to a term [t], the precondition of this
operation is that the bound atoms of [t] are fresh for [sigma], that is, do
not appear in the domain or codomain of [sigma]. This guarantees two things: