Add the source code.
François Pottier
parent
93a973671c
commit
b25bf2de49
|
|
@ -0,0 +1,8 @@
|
|||
*~
|
||||
*.native
|
||||
*.byte
|
||||
_build
|
||||
_build[1-3]
|
||||
*.cmx
|
||||
*.cmi
|
||||
*.cmo
|
||||
|
|
@ -0,0 +1,18 @@
|
|||
.PHONY: all clean main
|
||||
|
||||
OCAMLBUILD := ocamlbuild -classic-display -use-ocamlfind -use-menhir -cflags "-g" -lflags "-g"
|
||||
|
||||
all:
|
||||
# First build the library alone, so as to make sure it is stand-alone.
|
||||
$(OCAMLBUILD) -build-dir _build1 -I lib SolverHi.native
|
||||
# Then, build the sample client.
|
||||
$(OCAMLBUILD) -build-dir _build2 -I lib -I client Main.native
|
||||
# Also build the miscellaneous tests that we may have on the side.
|
||||
$(OCAMLBUILD) -build-dir _build3 -I lib -I client -I test TestUnionFind.native
|
||||
|
||||
main: all
|
||||
time _build2/client/Main.native
|
||||
|
||||
clean:
|
||||
rm -f {lib,client,test}/*~
|
||||
rm -rf _build1 _build2 _build3
|
||||
|
|
@ -0,0 +1,285 @@
|
|||
(* This sample client performs type inference for a fragment of ML and translates
|
||||
it down to a fragment of System F. *)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The unifier will use the following type structure. *)
|
||||
|
||||
module S = struct
|
||||
|
||||
type 'a structure =
|
||||
| TyArrow of 'a * 'a
|
||||
| TyProduct of 'a * 'a
|
||||
|
||||
let map f t =
|
||||
match t with
|
||||
| TyArrow (t1, t2) ->
|
||||
let t1 = f t1 in
|
||||
let t2 = f t2 in
|
||||
TyArrow (t1, t2)
|
||||
| TyProduct (t1, t2) ->
|
||||
let t1 = f t1 in
|
||||
let t2 = f t2 in
|
||||
TyProduct (t1, t2)
|
||||
|
||||
let fold f t accu =
|
||||
match t with
|
||||
| TyArrow (t1, t2)
|
||||
| TyProduct (t1, t2) ->
|
||||
let accu = f t1 accu in
|
||||
let accu = f t2 accu in
|
||||
accu
|
||||
|
||||
let iter f t =
|
||||
let _ = map f t in
|
||||
()
|
||||
|
||||
exception Iter2
|
||||
|
||||
let iter2 f t u =
|
||||
match t, u with
|
||||
| TyArrow (t1, t2), TyArrow (u1, u2)
|
||||
| TyProduct (t1, t2), TyProduct (u1, u2) ->
|
||||
f t1 u1;
|
||||
f t2 u2
|
||||
| _, _ ->
|
||||
raise Iter2
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The unifier type structure is decoded into the target calculus type structure
|
||||
as follows. *)
|
||||
|
||||
module O = struct
|
||||
|
||||
type tyvar =
|
||||
int
|
||||
|
||||
type 'a structure =
|
||||
'a S.structure
|
||||
|
||||
type ty =
|
||||
F.nominal_type
|
||||
|
||||
let variable x =
|
||||
F.TyVar x
|
||||
|
||||
let structure t =
|
||||
match t with
|
||||
| S.TyArrow (t1, t2) ->
|
||||
F.TyArrow (t1, t2)
|
||||
| S.TyProduct (t1, t2) ->
|
||||
F.TyProduct (t1, t2)
|
||||
|
||||
let mu x t =
|
||||
F.TyMu (x, t)
|
||||
|
||||
type scheme =
|
||||
tyvar list * ty
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Instantiate the solver. *)
|
||||
|
||||
module Solver =
|
||||
SolverHi.Make(struct include String type tevar = t end)(S)(O)
|
||||
|
||||
open Solver
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
let arrow x y =
|
||||
S.TyArrow (x, y)
|
||||
|
||||
let product x y =
|
||||
S.TyProduct (x, y)
|
||||
|
||||
let product_i i x y =
|
||||
assert (i = 1 || i = 2);
|
||||
if i = 1 then
|
||||
product x y
|
||||
else
|
||||
product y x
|
||||
|
||||
(* Should we use smart constructors to eliminate redundant coercions when possible? *)
|
||||
let smart =
|
||||
true
|
||||
|
||||
let flet (x, t, u) =
|
||||
match t with
|
||||
| F.Var y when smart && x = y ->
|
||||
u
|
||||
| t ->
|
||||
F.Let (x, t, u)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The coercion [coerce vs1 vs2] converts a type of the form [forall vs1, _]
|
||||
to a type of the form [forall vs2, _], where [vs2] forms a subset of [vs1].
|
||||
This coercion allows getting rid of unused quantifiers and/or re-ordering
|
||||
quantifiers. *)
|
||||
|
||||
type coercion =
|
||||
F.nominal_term -> F.nominal_term
|
||||
|
||||
let bottom : F.nominal_type =
|
||||
let a : F.tyvar = 0 (* arbitrary *) in
|
||||
F.TyForall (a, F.TyVar a)
|
||||
|
||||
(* [ftyabs1 v t] builds a (capital-Lambda) abstraction of the type variable [v]
|
||||
in the term [t]. It is a smart constructor: if it recognizes an eta-redex,
|
||||
it contracts it on the fly. We are in a special case where, if [v] and [w]
|
||||
are the same variable, then this variable does not occur free in [t], so we
|
||||
don't need to perform this costly check at runtime. This eta-contraction is
|
||||
not essential anyway; it's just a way of avoiding coercion clutter in the
|
||||
common case where the coercion actually has no effect. *)
|
||||
|
||||
let ftyabs1 v t =
|
||||
match t with
|
||||
| F.TyApp (t, F.TyVar w) when smart && v = w ->
|
||||
t
|
||||
| t ->
|
||||
F.TyAbs (v, t)
|
||||
|
||||
(* TEMPORARY find a better name for [coerce] *)
|
||||
|
||||
let coerce (vs1 : O.tyvar list) (vs2 : O.tyvar list) : coercion =
|
||||
(* Assume the term [t] has type [forall vs1, _]. *)
|
||||
fun t ->
|
||||
(* Introduce the desired quantifiers. *)
|
||||
List.fold_right ftyabs1 vs2 (
|
||||
(* Now, specialize the term [t]. For each member of [vs1],
|
||||
we must provide a suitable instantiation. *)
|
||||
F.ftyapp t (
|
||||
(* [vs1] is a superset of [vs2]. For each member of [vs1], if it is a
|
||||
member of [vs2], then we keep it (by instantiating it with itself),
|
||||
otherwise we get rid of it (by instantiating it with an arbitrary
|
||||
closed type, say [bottom]). *)
|
||||
let suitable (v : O.tyvar) : O.ty =
|
||||
if List.mem v vs2 then F.TyVar v else bottom
|
||||
(* TEMPORARY need an efficient membership test in [vs2] *)
|
||||
in
|
||||
List.map suitable vs1
|
||||
)
|
||||
)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The client uses the combinators provided by the solver so as to transparently
|
||||
1- analyse the source term and produce constraints; and 2- decode the solution
|
||||
of the constraints and produce a term in the target calculus. These two steps
|
||||
take place in different phases, but the code is written as if there was just
|
||||
one phase. *)
|
||||
|
||||
(* The function [analyse] takes a source term [t] and an expected type [w].
|
||||
No type environment is required, as everything is built into the constraint via
|
||||
suitable combinators, such as [def]. *)
|
||||
|
||||
(* BEGIN HASTYPE *)
|
||||
let rec hastype (t : ML.term) (w : variable) : F.nominal_term co
|
||||
= match t with
|
||||
|
||||
(* Variable. *)
|
||||
| ML.Var x ->
|
||||
|
||||
(* [w] must be an instance of the type scheme associated with [x]. *)
|
||||
instance x w <$$> fun tys ->
|
||||
(* The translation makes the type application explicit. *)
|
||||
F.ftyapp (F.Var x) tys
|
||||
|
||||
(* Abstraction. *)
|
||||
| ML.Abs (x, u) ->
|
||||
|
||||
(* We do not know a priori what the domain and codomain of this function
|
||||
are, so we must infer them. We introduce two type variables to stand
|
||||
for these unknowns. *)
|
||||
exist (fun v1 ->
|
||||
(* Here, we could use [exist_], because we do not need [ty2]. I refrain
|
||||
from using it, just to simplify the paper. *)
|
||||
exist (fun v2 ->
|
||||
(* [w] must be the function type [v1 -> v2]. *)
|
||||
(* Here, we could use [^^], instead of [^&], so as to avoid building
|
||||
a useless pair. I refrain from using it, just to simplify the paper. *)
|
||||
w --- arrow v1 v2 ^&
|
||||
(* Under the assumption that [x] has type [domain], the term [u] must
|
||||
have type [codomain]. *)
|
||||
def x v1 (hastype u v2)
|
||||
)
|
||||
) <$$> fun (ty1, (ty2, ((), u'))) ->
|
||||
(* Once these constraints are solved, we obtain the translated function
|
||||
body [u']. There remains to construct an explicitly-typed abstraction
|
||||
in the target calculus. *)
|
||||
F.Abs (x, ty1, u')
|
||||
|
||||
(* Application. *)
|
||||
| ML.App (t1, t2) ->
|
||||
|
||||
(* Introduce a type variable to stand for the unknown argument type. *)
|
||||
exist (fun v ->
|
||||
lift hastype t1 (arrow v w) ^&
|
||||
hastype t2 v
|
||||
) <$$> fun (ty, (t1', t2')) ->
|
||||
F.App (t1', t2')
|
||||
|
||||
(* Generalization. *)
|
||||
| ML.Let (x, t, u) ->
|
||||
|
||||
(* Construct a ``let'' constraint. *)
|
||||
let1 x (hastype t)
|
||||
(hastype u w)
|
||||
<$$> fun ((b, _), a, t', u') ->
|
||||
(* [a] are the type variables that we must introduce (via Lambda-abstractions)
|
||||
while type-checking [t]. [(b, _)] is the type scheme that [x] must receive
|
||||
while type-checking [u]. Its quantifiers [b] are guaranteed to form a subset of
|
||||
[a]. Hence, in general, we must re-bind [x] to an application of a suitable
|
||||
coercion to [x]. We use smart constructors so that, if the lists [a] and
|
||||
[b] happen to be equal, no extra code is produced. *)
|
||||
F.Let (x, F.ftyabs a t',
|
||||
(* IFPAPER
|
||||
F.Let (x, coerce a b (F.Var x),
|
||||
ELSE *)
|
||||
flet (x, coerce a b (F.Var x),
|
||||
(* END *)
|
||||
u'))
|
||||
(* END HASTYPE *)
|
||||
|
||||
(* Pair. *)
|
||||
| ML.Pair (t1, t2) ->
|
||||
|
||||
exist_ (fun v1 ->
|
||||
exist_ (fun v2 ->
|
||||
(* [w] must be the product type [v1 * v2]. *)
|
||||
w --- product v1 v2 ^^
|
||||
(* [t1] must have type [t1], and [t2] must have type [t2]. *)
|
||||
hastype t1 v1 ^&
|
||||
hastype t2 v2
|
||||
)
|
||||
) <$$> fun (t1, t2) ->
|
||||
(* The System F term. *)
|
||||
F.Pair (t1, t2)
|
||||
|
||||
(* Projection. *)
|
||||
| ML.Proj (i, t) ->
|
||||
|
||||
exist_ (fun other ->
|
||||
lift hastype t (product_i i w other)
|
||||
) <$$> fun t ->
|
||||
F.Proj (i, t)
|
||||
|
||||
(* The top-level wrapper uses [let0]. It does not require an expected
|
||||
type; it creates its own using [exist]. And it runs the solver. *)
|
||||
|
||||
exception Unbound = Solver.Unbound
|
||||
exception Unify = Solver.Unify
|
||||
exception Cycle = Solver.Cycle
|
||||
|
||||
let translate (t : ML.term) : F.nominal_term =
|
||||
solve false (
|
||||
let0 (exist_ (hastype t)) <$$> fun (vs, t) ->
|
||||
(* [vs] are the binders that we must introduce *)
|
||||
F.ftyabs vs t
|
||||
)
|
||||
|
|
@ -0,0 +1,5 @@
|
|||
exception Unbound of string
|
||||
exception Unify of F.nominal_type * F.nominal_type
|
||||
exception Cycle of F.nominal_type
|
||||
|
||||
val translate: ML.term -> F.nominal_term
|
||||
|
|
@ -0,0 +1,219 @@
|
|||
(* This module defines facilities for working with syntax, in nominal and
|
||||
de Bruijn representations. *)
|
||||
|
||||
type index =
|
||||
int
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The following module offers a facility for translating names to de Bruijn
|
||||
indices. It is parameterized over the type of names, which must come with
|
||||
a comparison function, so as to allow an efficient implementation of maps. *)
|
||||
|
||||
module Nominal2deBruijn (N : Map.OrderedType) = struct
|
||||
|
||||
module M =
|
||||
Map.Make(N)
|
||||
|
||||
(* For efficiency reasons, we must work internally with de Bruijn levels,
|
||||
as opposed to de Bruijn indices, and perform the conversion to an index
|
||||
at the last moment. *)
|
||||
|
||||
type env = {
|
||||
(* A map of every name to a de Bruijn level. *)
|
||||
map: int M.t;
|
||||
(* The current de Bruijn level. It is equal to the level of the most
|
||||
recently bound name. Its absolute value is irrelevant. *)
|
||||
current: int;
|
||||
}
|
||||
|
||||
(* The empty environment. *)
|
||||
|
||||
let empty =
|
||||
{ map = M.empty; current = 0 }
|
||||
|
||||
(* [lookup env x] translates the name [x] to a de Bruijn index. The
|
||||
environment [env] must have been previously extended with [x],
|
||||
otherwise [Unbound x] is raised. *)
|
||||
|
||||
exception Unbound of N.t
|
||||
|
||||
let lookup { map; current } x =
|
||||
(* Looking up the map produces a de Bruijn level, which we
|
||||
convert to a de Bruijn index by subtracting it from the
|
||||
current level. *)
|
||||
try
|
||||
current - M.find x map
|
||||
with Not_found ->
|
||||
raise (Unbound x)
|
||||
|
||||
(* [extend env x] extends the environment with a new binding of the
|
||||
name [x], producing a new environment. Any previous bindings of
|
||||
this name are shadowed. *)
|
||||
|
||||
let extend { map; current } x =
|
||||
let current = current + 1 in
|
||||
let map = M.add x current map in
|
||||
{ map; current }
|
||||
|
||||
(* [slide env x] extends the environment with a new binding of the
|
||||
name [x], producing a new environment. Any previous bindings of
|
||||
this name are shadowed. In contrast with [extend env x], instead
|
||||
of mapping [x] to a distinct index, [slide env x] maps [x] to the
|
||||
same index as the last introduced name. This exotic function can
|
||||
be useful, e.g., when mapping term variables to type indices. *)
|
||||
|
||||
let slide { map; current } x =
|
||||
(* Do not increment [current]. Thus, [x] receives the de Bruijn
|
||||
index 0, as in [extend], but the indices of the previous
|
||||
variables are not shifted up. *)
|
||||
let map = M.add x current map in
|
||||
{ map; current }
|
||||
|
||||
(* [bump env] skips an index, i.e., it shifts the range of the environment
|
||||
[env] up by one. This exotic function can be useful, e.g., when mapping
|
||||
term variables to type indices. Note that [extend env x] is equivalent
|
||||
to [slide (bump env) x]. *)
|
||||
|
||||
let bump { map; current } =
|
||||
let current = current + 1 in
|
||||
{ map; current }
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* This signature defines the functions that we need in order to be able
|
||||
to implement binding representations on top of some syntax. *)
|
||||
|
||||
(* The signatures that follow mention two types [v] and [t]. Think of them as
|
||||
``values'' and ``terms'', where the syntax of terms supports substitution
|
||||
of values for variables. They can be the same type, of course. They are
|
||||
parameterized over a representation of variables ['var] and a
|
||||
representation of binders ['binder]. *)
|
||||
|
||||
module type VAR = sig
|
||||
|
||||
type ('var, 'binder) v
|
||||
|
||||
(* The function [var] expects a variable [x] and injects it into the
|
||||
syntax of values. *)
|
||||
|
||||
val var:
|
||||
'var ->
|
||||
('var, 'binder) v
|
||||
|
||||
end
|
||||
|
||||
module type TRAVERSE = sig
|
||||
|
||||
type ('var, 'binder) v
|
||||
type ('var, 'binder) t
|
||||
|
||||
(* [traverse lookup extend env t] can be thought of, roughly, as the result of
|
||||
applying the substitution [lookup env] to the term [t] in a
|
||||
capture-avoiding manner. The function [lookup], when supplied with a
|
||||
suitable environment, maps variables to values. The function [extend]
|
||||
updates the environment when a binder is crossed; it returns a pair of
|
||||
the updated environment and a new binder. The parameter [env] is the
|
||||
initial environment. *)
|
||||
|
||||
val traverse:
|
||||
('env -> 'var1 -> ('var2, 'binder2) v) ->
|
||||
('env -> 'binder1 -> 'env * 'binder2) ->
|
||||
'env -> ('var1, 'binder1) t -> ('var2, 'binder2) t
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* A renaming function, [map], is defined in terms of [var] and [traverse].
|
||||
It is analogous to [traverse], except that its argument [lookup] has type
|
||||
['env -> 'var1 -> 'var2]. *)
|
||||
|
||||
module MakeMap
|
||||
(V : VAR)
|
||||
(T : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v)
|
||||
= struct
|
||||
|
||||
let map lookup extend env t =
|
||||
T.traverse (fun env x -> V.var (lookup env x)) extend env t
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Translation of a nominal representation to a de Bruijn representation. *)
|
||||
|
||||
module MakeTranslate
|
||||
(V : VAR)
|
||||
(T : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v)
|
||||
(N : Map.OrderedType)
|
||||
= struct
|
||||
|
||||
include MakeMap(V)(T)
|
||||
|
||||
include Nominal2deBruijn(N)
|
||||
|
||||
let translate t =
|
||||
map
|
||||
lookup
|
||||
(fun env x -> extend env x, ())
|
||||
empty
|
||||
t
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Weakening in a de Bruijn representation; also known as lifting. *)
|
||||
|
||||
module MakeLift
|
||||
(V : VAR)
|
||||
(T : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v)
|
||||
= struct
|
||||
|
||||
include MakeMap(V)(T)
|
||||
|
||||
let lift_var w k x =
|
||||
if k <= x then w + x else x
|
||||
|
||||
let cross k () =
|
||||
k + 1, ()
|
||||
|
||||
let lift w k t =
|
||||
if w = 0 then
|
||||
(* Fast path. *)
|
||||
t
|
||||
else
|
||||
map (lift_var w) cross k t
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Substitution in a de Bruijn representation. *)
|
||||
|
||||
module MakeSubst
|
||||
(V : VAR)
|
||||
(TVV : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v and type ('v, 'b) t = ('v, 'b) V.v)
|
||||
(TVT : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v)
|
||||
= struct
|
||||
|
||||
include MakeLift(V)(TVV)
|
||||
|
||||
let subst_var v k x =
|
||||
if x < k then
|
||||
V.var x
|
||||
else if x = k then
|
||||
v
|
||||
else
|
||||
V.var (x - 1)
|
||||
|
||||
let subst v k t =
|
||||
TVT.traverse (fun l x ->
|
||||
subst_var (lift l 0 v) (l + k) x
|
||||
) cross 0 t
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -0,0 +1,184 @@
|
|||
(* This module defines facilities for working with syntax, in nominal and
|
||||
de Bruijn representations. *)
|
||||
|
||||
type index =
|
||||
int
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The following module offers a facility for translating names to de Bruijn
|
||||
indices. It is parameterized over the type of names, which must come with
|
||||
a comparison function, so as to allow an efficient implementation of maps. *)
|
||||
|
||||
module Nominal2deBruijn (N : Map.OrderedType) : sig
|
||||
|
||||
(* A type of translation environments. *)
|
||||
|
||||
type env
|
||||
|
||||
(* The empty environment. *)
|
||||
|
||||
val empty: env
|
||||
|
||||
(* [lookup env x] translates the name [x] to a de Bruijn index. The
|
||||
environment [env] must have been previously extended with [x],
|
||||
otherwise [Unbound x] is raised. *)
|
||||
|
||||
exception Unbound of N.t
|
||||
|
||||
val lookup: env -> N.t -> index
|
||||
|
||||
(* [extend env x] extends the environment with a new binding of the
|
||||
name [x], producing a new environment. Any previous bindings of
|
||||
this name are shadowed. *)
|
||||
|
||||
val extend: env -> N.t -> env
|
||||
|
||||
(* [slide env x] extends the environment with a new binding of the
|
||||
name [x], producing a new environment. Any previous bindings of
|
||||
this name are shadowed. In contrast with [extend env x], instead
|
||||
of mapping [x] to a distinct index, [slide env x] maps [x] to the
|
||||
same index as the last introduced name. This exotic function can
|
||||
be useful, e.g., when mapping term variables to type indices. *)
|
||||
|
||||
val slide: env -> N.t -> env
|
||||
|
||||
(* [bump env] skips an index, i.e., it shifts the range of the environment
|
||||
[env] up by one. This exotic function can be useful, e.g., when mapping
|
||||
term variables to type indices. Note that [extend env x] is equivalent
|
||||
to [slide (bump env) x]. *)
|
||||
|
||||
val bump: env -> env
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* This signature defines the functions that we need in order to be able
|
||||
to implement binding representations on top of some syntax. *)
|
||||
|
||||
(* The signatures that follow mention two types [v] and [t]. Think of them as
|
||||
``values'' and ``terms'', where the syntax of terms supports substitution
|
||||
of values for variables. They can be the same type, of course. They are
|
||||
parameterized over a representation of variables ['var] and a
|
||||
representation of binders ['binder]. *)
|
||||
|
||||
module type VAR = sig
|
||||
|
||||
type ('var, 'binder) v
|
||||
|
||||
(* The function [var] expects a variable [x] and injects it into the
|
||||
syntax of values. *)
|
||||
|
||||
val var:
|
||||
'var ->
|
||||
('var, 'binder) v
|
||||
|
||||
end
|
||||
|
||||
module type TRAVERSE = sig
|
||||
|
||||
type ('var, 'binder) v
|
||||
type ('var, 'binder) t
|
||||
|
||||
(* [traverse lookup extend env t] can be thought of, roughly, as the result of
|
||||
applying the substitution [lookup env] to the term [t] in a
|
||||
capture-avoiding manner. The function [lookup], when supplied with a
|
||||
suitable environment, maps variables to values. The function [extend]
|
||||
updates the environment when a binder is crossed; it returns a pair of
|
||||
the updated environment and a new binder. The parameter [env] is the
|
||||
initial environment. *)
|
||||
|
||||
val traverse:
|
||||
('env -> 'var1 -> ('var2, 'binder2) v) ->
|
||||
('env -> 'binder1 -> 'env * 'binder2) ->
|
||||
'env -> ('var1, 'binder1) t -> ('var2, 'binder2) t
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* A renaming function, [map], is defined in terms of [var] and [traverse].
|
||||
It is analogous to [traverse], except that its argument [lookup] has type
|
||||
['env -> 'var1 -> 'var2]. *)
|
||||
|
||||
module MakeMap
|
||||
(V : VAR)
|
||||
(T : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v)
|
||||
: sig
|
||||
|
||||
open T
|
||||
|
||||
val map :
|
||||
('env -> 'var1 -> 'var2) ->
|
||||
('env -> 'binder1 -> 'env * 'binder2) ->
|
||||
'env -> ('var1, 'binder1) t -> ('var2, 'binder2) t
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Translation of a nominal representation to a de Bruijn representation. *)
|
||||
|
||||
module MakeTranslate
|
||||
(V : VAR)
|
||||
(T : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v)
|
||||
(N : Map.OrderedType)
|
||||
: sig
|
||||
|
||||
val translate: (N.t, N.t) T.t -> (index, unit) T.t
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Weakening in a de Bruijn representation; also known as lifting. *)
|
||||
|
||||
module MakeLift
|
||||
(V : VAR)
|
||||
(T : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v)
|
||||
: sig
|
||||
|
||||
(* [lift_var w k x] adds [w] to the index [x] if it is [k]-free, that is, if
|
||||
[x] is at or above [k]. *)
|
||||
|
||||
val lift_var: int -> index -> index -> index
|
||||
|
||||
(* [lift w k t] adds [w] to the [k]-free indices of the term [t]. *)
|
||||
|
||||
val lift: int -> index -> (index, unit) T.t -> (index, unit) T.t
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Substitution in a de Bruijn representation. *)
|
||||
|
||||
module MakeSubst
|
||||
(V : VAR)
|
||||
(TVV : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v and type ('v, 'b) t = ('v, 'b) V.v)
|
||||
(TVT : TRAVERSE with type ('v, 'b) v = ('v, 'b) V.v)
|
||||
: sig
|
||||
|
||||
open TVT
|
||||
|
||||
(* [subst_var v k x] replaces the variable [k] with the value [v], leaves
|
||||
the variables below [k] unchanged, and decrements the variables above [k]
|
||||
by one. *)
|
||||
|
||||
val subst_var:
|
||||
(index, unit) v ->
|
||||
index ->
|
||||
index ->
|
||||
(index, unit) v
|
||||
|
||||
(* [subst v k t] replaces the variable [k] with the value [v] in the term [t]. *)
|
||||
|
||||
val subst:
|
||||
(index, unit) v ->
|
||||
index ->
|
||||
(index, unit) t ->
|
||||
(index, unit) t
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -0,0 +1,193 @@
|
|||
(* This is the target calculus of the sample client. It is a core System F. *)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Types. *)
|
||||
|
||||
(* We include recursive types [FTyMu] in the target calculus, not only because
|
||||
we might wish to support them, but also because even if we disallow them,
|
||||
they can still arise during unification (the occurs check is run late), so
|
||||
we must be able to display them as part of a type error message. *)
|
||||
|
||||
(* Nominal or de Bruijn representation of type variables and binders. The
|
||||
nominal representation is more convenient when translating from ML to F,
|
||||
while the de Bruijn representation is more convenient when type-checking
|
||||
F. *)
|
||||
|
||||
(* BEGIN F *)
|
||||
type ('a, 'b) typ =
|
||||
| TyVar of 'a
|
||||
| TyArrow of ('a, 'b) typ * ('a, 'b) typ
|
||||
| TyProduct of ('a, 'b) typ * ('a, 'b) typ
|
||||
| TyForall of 'b * ('a, 'b) typ
|
||||
| TyMu of 'b * ('a, 'b) typ
|
||||
(* END F *)
|
||||
|
||||
(* BEGIN F *)
|
||||
type tyvar = int
|
||||
(* END F *)
|
||||
|
||||
(* BEGIN F *)
|
||||
type nominal_type = (tyvar, tyvar) typ
|
||||
(* END F *)
|
||||
|
||||
type debruijn_type =
|
||||
(DeBruijn.index, unit) typ
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Terms. *)
|
||||
|
||||
(* Nominal representation of term variables and binders. *)
|
||||
|
||||
(* BEGIN F *)
|
||||
type tevar = string
|
||||
(* END F*)
|
||||
|
||||
(* BEGIN F *)
|
||||
type ('a, 'b) term =
|
||||
| Var of tevar
|
||||
| Abs of tevar * ('a, 'b) typ * ('a, 'b) term
|
||||
| App of ('a, 'b) term * ('a, 'b) term
|
||||
| Let of tevar * ('a, 'b) term * ('a, 'b) term
|
||||
| TyAbs of 'b * ('a, 'b) term
|
||||
| TyApp of ('a, 'b) term * ('a, 'b) typ
|
||||
(* END F *)
|
||||
| Pair of ('a, 'b) term * ('a, 'b) term
|
||||
| Proj of int * ('a, 'b) term
|
||||
|
||||
(* BEGIN F *)
|
||||
type nominal_term = (tyvar, tyvar) term
|
||||
(* END F *)
|
||||
|
||||
type debruijn_term =
|
||||
(DeBruijn.index, unit) term
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Constructors. *)
|
||||
(* BEGIN F *)
|
||||
|
||||
let ftyabs vs t =
|
||||
List.fold_right (fun v t -> TyAbs (v, t)) vs t
|
||||
let ftyapp t tys =
|
||||
List.fold_left (fun t ty -> TyApp (t, ty)) t tys
|
||||
(* END F *)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Boilerplate code for type-in-type substitutions. *)
|
||||
|
||||
module TypeVar : DeBruijn.VAR
|
||||
with type ('a, 'b) v = ('a, 'b) typ
|
||||
= struct
|
||||
|
||||
type ('v, 'b) v =
|
||||
('v, 'b) typ
|
||||
|
||||
let var x =
|
||||
TyVar x
|
||||
|
||||
end
|
||||
|
||||
module TypeInType : DeBruijn.TRAVERSE
|
||||
with type ('v, 'b) v = ('v, 'b) typ
|
||||
and type ('v, 'b) t = ('v, 'b) typ
|
||||
= struct
|
||||
|
||||
type ('v, 'b) v =
|
||||
('v, 'b) typ
|
||||
|
||||
type ('v, 'b) t =
|
||||
('v, 'b) typ
|
||||
|
||||
(* I note that we could perform physical equality tests in [traverse]
|
||||
so as to preserve sharing when possible, but that would require use
|
||||
of [Obj.magic]. Let's just not do it in this demo. *)
|
||||
|
||||
let rec traverse lookup extend env ty =
|
||||
match ty with
|
||||
| TyVar x ->
|
||||
lookup env x
|
||||
| TyArrow (ty1, ty2) ->
|
||||
let ty1' = traverse lookup extend env ty1
|
||||
and ty2' = traverse lookup extend env ty2 in
|
||||
TyArrow (ty1', ty2')
|
||||
| TyProduct (ty1, ty2) ->
|
||||
let ty1' = traverse lookup extend env ty1
|
||||
and ty2' = traverse lookup extend env ty2 in
|
||||
TyProduct (ty1', ty2')
|
||||
| TyForall (x, ty1) ->
|
||||
let env, x = extend env x in
|
||||
let ty1' = traverse lookup extend env ty1 in
|
||||
TyForall (x, ty1')
|
||||
| TyMu (x, ty1) ->
|
||||
let env, x = extend env x in
|
||||
let ty1' = traverse lookup extend env ty1 in
|
||||
TyMu (x, ty1')
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Boilerplate code for type-in-term substitutions. *)
|
||||
|
||||
module TypeInTerm : DeBruijn.TRAVERSE
|
||||
with type ('v, 'b) v = ('v, 'b) typ
|
||||
with type ('v, 'b) t = ('v, 'b) term
|
||||
= struct
|
||||
|
||||
type ('v, 'b) v =
|
||||
('v, 'b) typ
|
||||
|
||||
type ('v, 'b) t =
|
||||
('v, 'b) term
|
||||
|
||||
let rec traverse lookup extend env t =
|
||||
match t with
|
||||
| Var x ->
|
||||
Var x
|
||||
| Abs (x, ty, t) ->
|
||||
let ty' = TypeInType.traverse lookup extend env ty
|
||||
and t' = traverse lookup extend env t in
|
||||
Abs (x, ty', t')
|
||||
| App (t1, t2) ->
|
||||
let t1' = traverse lookup extend env t1
|
||||
and t2' = traverse lookup extend env t2 in
|
||||
App (t1', t2')
|
||||
| Let (x, t1, t2) ->
|
||||
let t1' = traverse lookup extend env t1
|
||||
and t2' = traverse lookup extend env t2 in
|
||||
Let (x, t1', t2')
|
||||
| TyAbs (x, t) ->
|
||||
let env, x = extend env x in
|
||||
let t' = traverse lookup extend env t in
|
||||
TyAbs (x, t')
|
||||
| TyApp (t, ty) ->
|
||||
let t' = traverse lookup extend env t
|
||||
and ty' = TypeInType.traverse lookup extend env ty in
|
||||
TyApp (t', ty')
|
||||
| Pair (t1, t2) ->
|
||||
let t1' = traverse lookup extend env t1
|
||||
and t2' = traverse lookup extend env t2 in
|
||||
Pair (t1', t2')
|
||||
| Proj (i, t) ->
|
||||
let t' = traverse lookup extend env t in
|
||||
Proj (i, t')
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Type-in-type weakening and substitution. *)
|
||||
|
||||
include DeBruijn.MakeLift(TypeVar)(TypeInType)
|
||||
|
||||
include DeBruijn.MakeSubst(TypeVar)(TypeInType)(TypeInType)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Translation of nominal terms to de Bruijn terms. *)
|
||||
|
||||
include DeBruijn.MakeTranslate(TypeVar)(TypeInTerm)(Int)
|
||||
|
||||
|
|
@ -0,0 +1,86 @@
|
|||
(* This is the target calculus of the sample client. It is a core System F. *)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Types. *)
|
||||
|
||||
(* We include recursive types [FTyMu] in the target calculus, not only because
|
||||
we might wish to support them, but also because even if we disallow them,
|
||||
they can still arise during unification (the occurs check is run late), so
|
||||
we must be able to display them as part of a type error message. *)
|
||||
|
||||
(* Nominal or de Bruijn representation of type variables and binders. The
|
||||
nominal representation is more convenient when translating from ML to F,
|
||||
while the de Bruijn representation is more convenient when type-checking
|
||||
F. *)
|
||||
|
||||
type ('a, 'b) typ =
|
||||
| TyVar of 'a
|
||||
| TyArrow of ('a, 'b) typ * ('a, 'b) typ
|
||||
| TyProduct of ('a, 'b) typ * ('a, 'b) typ
|
||||
| TyForall of 'b * ('a, 'b) typ
|
||||
| TyMu of 'b * ('a, 'b) typ
|
||||
|
||||
type tyvar =
|
||||
int
|
||||
|
||||
type nominal_type =
|
||||
(tyvar, tyvar) typ
|
||||
|
||||
type debruijn_type =
|
||||
(DeBruijn.index, unit) typ
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Terms. *)
|
||||
|
||||
(* Nominal representation of term variables and binders. *)
|
||||
|
||||
(* Nominal or de Bruijn representation of type variables and binders. *)
|
||||
|
||||
type tevar =
|
||||
string
|
||||
|
||||
type ('a, 'b) term =
|
||||
| Var of tevar
|
||||
| Abs of tevar * ('a, 'b) typ * ('a, 'b) term
|
||||
| App of ('a, 'b) term * ('a, 'b) term
|
||||
| Let of tevar * ('a, 'b) term * ('a, 'b) term
|
||||
| TyAbs of 'b * ('a, 'b) term
|
||||
| TyApp of ('a, 'b) term * ('a, 'b) typ
|
||||
| Pair of ('a, 'b) term * ('a, 'b) term
|
||||
| Proj of int * ('a, 'b) term
|
||||
|
||||
type nominal_term =
|
||||
(tyvar, tyvar) term
|
||||
|
||||
type debruijn_term =
|
||||
(DeBruijn.index, unit) term
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Constructors. *)
|
||||
|
||||
val ftyabs: 'b list -> ('a, 'b) term -> ('a, 'b) term
|
||||
val ftyapp: ('a, 'b) term -> ('a, 'b) typ list -> ('a, 'b) term
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Type-in-type weakening and substitution. *)
|
||||
|
||||
(* [lift w k ty] is the type [ty] where the variables at or above index [k]
|
||||
are lifted up by [w]. *)
|
||||
|
||||
val lift: int -> DeBruijn.index -> debruijn_type -> debruijn_type
|
||||
|
||||
(* [subst xty x ty] is the type [ty] where the type variable [x] has been
|
||||
replaced with the type [xty]. *)
|
||||
|
||||
val subst: debruijn_type -> DeBruijn.index -> debruijn_type -> debruijn_type
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Translation of nominal terms to de Bruijn terms. *)
|
||||
|
||||
val translate: nominal_term -> debruijn_term
|
||||
|
||||
|
|
@ -0,0 +1,122 @@
|
|||
(* A pretty-printer for F. *)
|
||||
|
||||
open PPrint
|
||||
open F
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Types. *)
|
||||
|
||||
let print_tyvar x =
|
||||
OCaml.int x (* TEMPORARY *)
|
||||
|
||||
let rec print_type_aux level ty =
|
||||
assert (level >= 0);
|
||||
match ty with
|
||||
| TyVar x ->
|
||||
print_tyvar x
|
||||
| TyProduct (ty1, ty2) ->
|
||||
if level >= 1 then
|
||||
print_type_aux 0 ty1 ^^
|
||||
string " * " ^^
|
||||
print_type_aux 1 ty2
|
||||
else
|
||||
parens (print_type ty)
|
||||
| TyArrow (ty1, ty2) ->
|
||||
if level >= 2 then
|
||||
print_type_aux 1 ty1 ^^
|
||||
string " -> " ^^
|
||||
print_type ty2
|
||||
else
|
||||
parens (print_type ty)
|
||||
| TyForall (x, ty1) ->
|
||||
if level >= 3 then
|
||||
lbracket ^^
|
||||
print_tyvar x ^^
|
||||
rbracket ^^ space ^^
|
||||
print_type_aux 3 ty1
|
||||
else
|
||||
parens (print_type ty)
|
||||
| TyMu (x, ty1) ->
|
||||
if level >= 3 then
|
||||
string "mu " ^^
|
||||
print_tyvar x ^^
|
||||
dot ^^ space ^^
|
||||
print_type_aux 3 ty1
|
||||
else
|
||||
parens (print_type ty)
|
||||
|
||||
and print_type ty =
|
||||
print_type_aux 3 ty
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Terms. *)
|
||||
|
||||
let rec print_term_aux level t =
|
||||
assert (level >= 0);
|
||||
match t with
|
||||
| Var x ->
|
||||
string x
|
||||
| App (t1, t2) ->
|
||||
if level >= 1 then
|
||||
print_term_aux 1 t1 ^^
|
||||
space ^^
|
||||
print_term_aux 0 t2
|
||||
else
|
||||
parens (print_term t)
|
||||
| TyApp (t1, ty2) ->
|
||||
if level >= 1 then
|
||||
print_term_aux 1 t1 ^^
|
||||
space ^^ lbracket ^^
|
||||
print_type ty2 ^^
|
||||
rbracket
|
||||
else
|
||||
parens (print_term t)
|
||||
| Abs (x, ty1, t2) ->
|
||||
if level >= 2 then
|
||||
string "fun " ^^
|
||||
string x ^^
|
||||
string " : " ^^
|
||||
print_type ty1 ^^
|
||||
string " = " ^^
|
||||
print_term_aux 2 t2
|
||||
else
|
||||
parens (print_term t)
|
||||
| Let (x, t1, t2) ->
|
||||
if level >= 2 then
|
||||
string "let " ^^
|
||||
string x ^^
|
||||
string " = " ^^
|
||||
print_term t1 ^^
|
||||
string " in " ^^
|
||||
print_term_aux 2 t2
|
||||
else
|
||||
parens (print_term t)
|
||||
| TyAbs (x, t1) ->
|
||||
if level >= 2 then
|
||||
string "FUN " ^^
|
||||
print_tyvar x ^^
|
||||
string " = " ^^
|
||||
print_term_aux 2 t1
|
||||
else
|
||||
parens (print_term t)
|
||||
| Pair (t1, t2) ->
|
||||
parens (
|
||||
print_term t1 ^^
|
||||
comma ^^ space ^^
|
||||
print_term t2
|
||||
)
|
||||
| Proj (i, t2) ->
|
||||
(* like [App] *)
|
||||
if level >= 1 then
|
||||
string "proj" ^^
|
||||
OCaml.int i ^^
|
||||
space ^^
|
||||
print_term_aux 0 t2
|
||||
else
|
||||
parens (print_term t)
|
||||
|
||||
and print_term t =
|
||||
print_term_aux 2 t
|
||||
|
||||
|
|
@ -0,0 +1,8 @@
|
|||
(* A pretty-printer for F. *)
|
||||
|
||||
open PPrint
|
||||
open F
|
||||
|
||||
val print_type: nominal_type -> document
|
||||
val print_term: nominal_term -> document
|
||||
|
||||
|
|
@ -0,0 +1,177 @@
|
|||
open F
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* A type environment maps term variables to types in de Bruijn's representation. *)
|
||||
|
||||
(* Our term variables are in nominal representation, which allows us to represent
|
||||
the environment as a binary search tree. One difficulty is that when we enter a
|
||||
new type variable binder [TyAbs], we must (conceptually) shift every type in
|
||||
the range of the environment up by one. When term variables are in de Bruijn
|
||||
notation and the environment is a list, this is easily done by inserting a mark
|
||||
in front of the environment. Here, we must be more clever. We maintain an [N2DB]
|
||||
environment that tells us, for every *term* variable, how long ago it was bound,
|
||||
that is, how many *type* variables were introduced since then. Hence, this tells
|
||||
us by how much we must shift its type. It's really a bit too clever, but let's
|
||||
do this for fun. *)
|
||||
|
||||
module TermVar =
|
||||
String
|
||||
|
||||
module TermVarMap =
|
||||
Map.Make(TermVar)
|
||||
|
||||
module N2DB =
|
||||
DeBruijn.Nominal2deBruijn(TermVar)
|
||||
|
||||
type env = {
|
||||
(* A mapping of term variables to types. *)
|
||||
types: debruijn_type TermVarMap.t;
|
||||
(* A translation environment of TERM variables to TYPE indices. *)
|
||||
names: N2DB.env
|
||||
}
|
||||
|
||||
let empty =
|
||||
{ types = TermVarMap.empty; names = N2DB.empty }
|
||||
|
||||
exception UnboundTermVariable of tevar
|
||||
|
||||
let lookup { types; names } x =
|
||||
try
|
||||
(* Obtain the type associated with [x]. *)
|
||||
let ty = TermVarMap.find x types in
|
||||
(* Find how long ago [x] was bound. *)
|
||||
let w = N2DB.lookup names x in
|
||||
(* Shift the type [ty] by this amount, so that it makes sense in the
|
||||
current scope. *)
|
||||
lift w 0 ty
|
||||
with Not_found ->
|
||||
(* must have been raised by [TermVarMap.find] *)
|
||||
raise (UnboundTermVariable x)
|
||||
|
||||
let extend_with_tevar { types; names } x ty =
|
||||
(* Map the name [x] to [ty], and record when it was bound, without
|
||||
incrementing the time. *)
|
||||
{ types = TermVarMap.add x ty types;
|
||||
names = N2DB.slide names x }
|
||||
|
||||
let extend_with_tyvar { types; names } =
|
||||
(* Increment the time. *)
|
||||
{ types; names = N2DB.bump names }
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Destructors. *)
|
||||
|
||||
let unfold ty =
|
||||
match ty with
|
||||
| TyMu ((), body) ->
|
||||
subst ty 0 body
|
||||
| _ ->
|
||||
assert false
|
||||
|
||||
exception NotAnArrow of debruijn_type
|
||||
|
||||
let rec as_arrow ty =
|
||||
match ty with
|
||||
| TyArrow (ty1, ty2) ->
|
||||
ty1, ty2
|
||||
| TyMu _ ->
|
||||
as_arrow (unfold ty)
|
||||
| _ ->
|
||||
raise (NotAnArrow ty)
|
||||
|
||||
exception NotAProduct of debruijn_type
|
||||
|
||||
let rec as_product ty =
|
||||
match ty with
|
||||
| TyProduct (ty1, ty2) ->
|
||||
ty1, ty2
|
||||
| TyMu _ ->
|
||||
as_product (unfold ty)
|
||||
| _ ->
|
||||
raise (NotAProduct ty)
|
||||
|
||||
exception NotAForall of debruijn_type
|
||||
|
||||
let rec as_forall ty =
|
||||
match ty with
|
||||
| TyForall ((), ty) ->
|
||||
ty
|
||||
| TyMu _ ->
|
||||
as_forall (unfold ty)
|
||||
| _ ->
|
||||
raise (NotAForall ty)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* An equality test. *)
|
||||
|
||||
(* In the absence of recursive types, syntactic equality would work. However,
|
||||
in their presence, one must unfold recursive types during the equality
|
||||
check. *)
|
||||
|
||||
(* Note that comparing two [TyMu] types just by comparing their bodies is
|
||||
correct, but incomplete. We do not do it. Naively unfolding every [TyMu]
|
||||
type is complete, but leads to potential non-termination. We do that, with
|
||||
a budget limit, which makes the algorithm unsound (two types may be
|
||||
considered equal when they are different). I should really implement
|
||||
my own algorithm (Gauthier & Pottier, ICFP 2004) but that will be for
|
||||
some other time. *)
|
||||
|
||||
exception TypeMismatch of debruijn_type * debruijn_type
|
||||
|
||||
let rec equal budget ty1 ty2 =
|
||||
match ty1, ty2 with
|
||||
| (TyMu _ as ty1), ty2
|
||||
| ty2, (TyMu _ as ty1) ->
|
||||
budget = 0 || equal (budget - 1) (unfold ty1) ty2
|
||||
| TyVar x1, TyVar x2 ->
|
||||
x1 = x2
|
||||
| TyArrow (ty1a, ty1b), TyArrow (ty2a, ty2b) ->
|
||||
equal budget ty1a ty2a && equal budget ty1b ty2b
|
||||
| TyProduct (ty1a, ty1b), TyProduct (ty2a, ty2b) ->
|
||||
equal budget ty1a ty2a && equal budget ty1b ty2b
|
||||
| TyForall ((), ty1), TyForall ((), ty2) ->
|
||||
equal budget ty1 ty2
|
||||
| _, _ ->
|
||||
false
|
||||
|
||||
let budget =
|
||||
4
|
||||
|
||||
let (--) ty1 ty2 =
|
||||
if not (equal budget ty1 ty2) then
|
||||
raise (TypeMismatch (ty1, ty2))
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The type-checker. *)
|
||||
|
||||
let rec typeof env (t : debruijn_term) : debruijn_type =
|
||||
match t with
|
||||
| Var x ->
|
||||
lookup env x
|
||||
| Abs (x, ty1, t) ->
|
||||
let ty2 = typeof (extend_with_tevar env x ty1) t in
|
||||
TyArrow (ty1, ty2)
|
||||
| App (t, u) ->
|
||||
let ty1, ty2 = as_arrow (typeof env t) in
|
||||
typeof env u -- ty1;
|
||||
ty2
|
||||
| Let (x, t, u) ->
|
||||
let env = extend_with_tevar env x (typeof env t) in
|
||||
typeof env u
|
||||
| TyAbs ((), t) ->
|
||||
TyForall ((), typeof (extend_with_tyvar env) t)
|
||||
| TyApp (t, ty2) ->
|
||||
subst ty2 0 (as_forall (typeof env t))
|
||||
| Pair (t1, t2) ->
|
||||
TyProduct (typeof env t1, typeof env t2)
|
||||
| Proj (i, t) ->
|
||||
assert (i = 1 || i = 2);
|
||||
let ty1, ty2 = as_product (typeof env t) in
|
||||
if i = 1 then ty1 else ty2
|
||||
|
||||
let typeof =
|
||||
typeof empty
|
||||
|
|
@ -0,0 +1,12 @@
|
|||
open F
|
||||
|
||||
(* A type-checker for System F. *)
|
||||
|
||||
(* [typeof t] type-checks the closed term [t] and constructs its type. *)
|
||||
|
||||
exception NotAnArrow of debruijn_type
|
||||
exception NotAForall of debruijn_type
|
||||
exception TypeMismatch of debruijn_type * debruijn_type
|
||||
|
||||
val typeof: debruijn_term -> debruijn_type
|
||||
|
||||
|
|
@ -0,0 +1,10 @@
|
|||
(* Integers as an ordered type. *)
|
||||
|
||||
type t =
|
||||
int
|
||||
|
||||
let compare (x : int) (y : int) =
|
||||
if x < y then -1
|
||||
else if x = y then 0
|
||||
else 1
|
||||
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
(* Integers as an ordered type. *)
|
||||
|
||||
include Map.OrderedType with type t = int
|
||||
|
||||
|
|
@ -0,0 +1,17 @@
|
|||
(* This is the source calculus of the sample client. It is a core ML. *)
|
||||
|
||||
(* The terms carry no type annotations. *)
|
||||
|
||||
(* Nominal representation of term variables and binders. *)
|
||||
|
||||
(* BEGIN ML *)
|
||||
type tevar = string
|
||||
type term =
|
||||
| Var of tevar
|
||||
| Abs of tevar * term
|
||||
| App of term * term
|
||||
| Let of tevar * term * term
|
||||
(* END ML *)
|
||||
| Pair of term * term
|
||||
| Proj of int * term
|
||||
|
||||
|
|
@ -0,0 +1,258 @@
|
|||
let verbose =
|
||||
false
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* A random generator of pure lambda-terms. *)
|
||||
|
||||
let int2var k =
|
||||
"x" ^ string_of_int k
|
||||
|
||||
(* [split n] produces two numbers [n1] and [n2] comprised between [0] and [n]
|
||||
(inclusive) whose sum is [n]. *)
|
||||
|
||||
let split n =
|
||||
let n1 = Random.int (n + 1) in
|
||||
let n2 = n - n1 in
|
||||
n1, n2
|
||||
|
||||
(* The parameter [k] is the number of free variables; the parameter [n] is the
|
||||
size (i.e., the number of internal nodes). *)
|
||||
|
||||
let rec random_ml_term k n =
|
||||
if n = 0 then begin
|
||||
assert (k > 0);
|
||||
ML.Var (int2var (Random.int k))
|
||||
end
|
||||
else
|
||||
let c = Random.int 5 (* Abs, App, Pair, Proj, Let *) in
|
||||
if k = 0 || c = 0 then
|
||||
(* The next available variable is [k]. *)
|
||||
let x, k = int2var k, k + 1 in
|
||||
ML.Abs (x, random_ml_term k (n - 1))
|
||||
else if c = 1 then
|
||||
let n1, n2 = split (n - 1) in
|
||||
ML.App (random_ml_term k n1, random_ml_term k n2)
|
||||
else if c = 2 then
|
||||
let n1, n2 = split (n - 1) in
|
||||
ML.Pair (random_ml_term k n1, random_ml_term k n2)
|
||||
else if c = 3 then
|
||||
ML.Proj (1 + Random.int 2, random_ml_term k (n - 1))
|
||||
else if c = 4 then
|
||||
let n1, n2 = split (n - 1) in
|
||||
ML.Let (int2var k, random_ml_term k n1, random_ml_term (k + 1) n2)
|
||||
else
|
||||
assert false
|
||||
|
||||
let rec size accu = function
|
||||
| ML.Var _ ->
|
||||
accu
|
||||
| ML.Abs (_, t)
|
||||
| ML.Proj (_, t)
|
||||
-> size (accu + 1) t
|
||||
| ML.App (t1, t2)
|
||||
| ML.Let (_, t1, t2)
|
||||
| ML.Pair (t1, t2)
|
||||
-> size (size (accu + 1) t1) t2
|
||||
|
||||
let size =
|
||||
size 0
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Facilities for dealing with exceptions. *)
|
||||
|
||||
(* A log is a mutable list of actions that produce output, stored in reverse
|
||||
order. It is used to suppress the printing of progress messages as long as
|
||||
everything goes well. If a problem occurs, then the printing actions are
|
||||
executed. *)
|
||||
|
||||
type log = {
|
||||
mutable actions: (unit -> unit) list
|
||||
}
|
||||
|
||||
let create_log () =
|
||||
{ actions = [] }
|
||||
|
||||
let log_action log action =
|
||||
log.actions <- action :: log.actions
|
||||
|
||||
let log_msg log msg =
|
||||
log_action log (fun () ->
|
||||
output_string stdout msg
|
||||
)
|
||||
|
||||
let print_log log =
|
||||
List.iter (fun action ->
|
||||
action();
|
||||
(* Flush after every action, as the action itself could raise an
|
||||
exception, and we will want to know which one failed. *)
|
||||
flush stdout
|
||||
) (List.rev log.actions)
|
||||
|
||||
let attempt log msg f x =
|
||||
log_msg log msg;
|
||||
try
|
||||
f x
|
||||
with e ->
|
||||
print_log log;
|
||||
Printf.printf "%s\n" (Printexc.to_string e);
|
||||
Printexc.print_backtrace stdout;
|
||||
flush stdout;
|
||||
exit 1
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* A wrapper over the client's [translate] function. We consider ill-typedness
|
||||
as normal, since our terms are randomly generated, so we translate the client
|
||||
exceptions to [None]. *)
|
||||
|
||||
let print_type ty =
|
||||
PPrint.(ToChannel.pretty 0.9 80 stdout (FPrinter.print_type ty ^^ hardline))
|
||||
|
||||
let translate t =
|
||||
try
|
||||
Some (Client.translate t)
|
||||
with
|
||||
| Client.Cycle ty ->
|
||||
if verbose then begin
|
||||
Printf.fprintf stdout "Type error: a cyclic type arose.\n";
|
||||
print_type ty
|
||||
end;
|
||||
None
|
||||
| Client.Unify (ty1, ty2) ->
|
||||
if verbose then begin
|
||||
Printf.fprintf stdout "Type error: type mismatch.\n";
|
||||
Printf.fprintf stdout "Type error: mismatch between the type:\n";
|
||||