Compare commits
158 Commits
master
...
frozen-sol
Author | SHA1 | Date |
---|---|---|
Olivier | 3f52bf2a87 | |
Olivier | 6184864d10 | |
Olivier | 028172053a | |
Olivier | 3698d045e1 | |
Olivier | 286df69574 | |
Olivier | 14d11151d4 | |
Olivier | 68fc16d361 | |
Olivier | 66a0235b90 | |
Gabriel Scherer | f36fe293ba | |
Gabriel Scherer | eff9b56b71 | |
Gabriel Scherer | 5957849cea | |
Gabriel Scherer | d21d21f9b6 | |
Olivier | 86c2fa0577 | |
Olivier | 9057451455 | |
Olivier | 8eb6fb44de | |
Olivier | a5f8bc6df0 | |
Olivier | fa66414eb3 | |
Olivier | 7f76dbaaf7 | |
Olivier | 5d9c03c250 | |
Olivier | 971ee24f0c | |
Olivier | e03b8e4899 | |
Olivier | 388e62260d | |
Olivier | 4ef4625639 | |
Olivier | 412f73cd2d | |
Olivier | 1a9821c86c | |
Olivier | eefb1dbcfb | |
Olivier | 0cdd6f2836 | |
Olivier | 494c29cc17 | |
Olivier | 2a5fabc29a | |
Gabriel Scherer | 42750df730 | |
Olivier | f71f878b79 | |
Olivier | 0e04318e4a | |
Olivier | 4f69f391ed | |
Olivier | 8d5b691071 | |
Olivier | b528dc6417 | |
Olivier | 1499305f8f | |
Olivier | 6f1e2ac714 | |
Olivier | f5b74073e3 | |
Olivier | 8de13a0208 | |
Olivier | 79cca9e052 | |
Olivier | f4271dd44c | |
Olivier | 696a8932e8 | |
Olivier | d846d4e46a | |
Olivier | c8609f9aba | |
Olivier | ccd6dea901 | |
Olivier | 721e694121 | |
Olivier | fc01111e50 | |
Olivier | 1568dae672 | |
Olivier | 92a14778d3 | |
Olivier | 96e3d95b29 | |
Olivier | 0357300fe5 | |
Olivier | 90414caeb0 | |
Olivier | 039cc7b620 | |
Olivier | 590e0ac6df | |
Olivier | 69238b35c2 | |
Olivier | 3645fd189f | |
Olivier | 9b680ba84e | |
Olivier | e3c149479e | |
Olivier | a88aab13b6 | |
Olivier | 07b324d442 | |
Olivier | 9706c54fd6 | |
Olivier | 2253f20f4c | |
Olivier | 3fe6ff93dd | |
Olivier | 7cc9feedc1 | |
Olivier | 28c086094f | |
Olivier | 67a3d5829a | |
Olivier | 1b96dd56fb | |
Olivier | db37408267 | |
Olivier | 22a861e510 | |
Olivier | 4cd22737a7 | |
Olivier | 75a1c609e2 | |
Olivier | 818d839a46 | |
Olivier | a96b2e90ad | |
Olivier | 27b2c67b97 | |
Olivier | 108ac2a8dc | |
Olivier | 5f6188bbf7 | |
Olivier | 2fade74170 | |
Olivier | 8579357e83 | |
Olivier | f6986c873d | |
Olivier | a983f7e5ba | |
Olivier | 206ef0bc41 | |
Olivier | cefbe0fbb9 | |
Olivier | a27a966b54 | |
Olivier | 170e8a55f5 | |
Olivier | 55b71be6b1 | |
Olivier | 4562909c32 | |
Gabriel Scherer | b1b9c97544 | |
Gabriel Scherer | 4d9633d1e9 | |
Gabriel Scherer | 73dabefdfd | |
Gabriel Scherer | 097378a909 | |
Olivier | 5481126b64 | |
Olivier | 15a4255424 | |
Olivier | f726ca1cda | |
Olivier | d3faf24a39 | |
Olivier | 233efdb84e | |
Olivier | cf1cfb96c4 | |
Olivier | 682e7c003a | |
Olivier | 169cf41605 | |
Olivier | 1d5bfae6d7 | |
Olivier | 29a743a30c | |
Olivier | 4da217c3e5 | |
Olivier | 77f169c168 | |
Olivier | 0a9a61daa5 | |
Olivier | 1a142aa745 | |
Olivier | 81ab70ff75 | |
Olivier | 66e2905e28 | |
Olivier | cf68a69b6b | |
Olivier | bc7b3895f7 | |
Olivier | 8103dacf02 | |
Olivier | 0755533396 | |
Olivier | 34f850c880 | |
Olivier | d2c2043392 | |
Olivier | f6d439c9a2 | |
Olivier | ad3cafd0c8 | |
Gabriel Scherer | c527ded72f | |
Gabriel Scherer | de498f2bce | |
Gabriel Scherer | dc530b64d4 | |
Gabriel Scherer | a893f86d7a | |
Gabriel Scherer | b7d5bdf43a | |
Gabriel Scherer | 62f62c23cd | |
Olivier | 7718ec79a0 | |
Gabriel Scherer | 4f5d8dbacc | |
Gabriel Scherer | 455fd161dd | |
Olivier | 835ef283fa | |
Olivier | c25014e2a8 | |
Gabriel Scherer | 021f6eadee | |
Gabriel Scherer | c45c70bbb7 | |
Gabriel Scherer | dbb9e76ea6 | |
Gabriel Scherer | 1ccc3430bc | |
Gabriel Scherer | b4445ceb4a | |
Olivier Martinot | da874d035c | |
Olivier Martinot | d588ba83f1 | |
Olivier Martinot | a7921a6d2b | |
Olivier Martinot | bbd478852b | |
Olivier Martinot | 0028456e24 | |
Olivier Martinot | adac72c705 | |
Olivier Martinot | 7a2ebdd726 | |
Olivier Martinot | 29f2903c5c | |
Olivier Martinot | 42c355464a | |
Olivier Martinot | aec8a1a721 | |
Olivier Martinot | d857bd6a86 | |
Olivier Martinot | 33f8448014 | |
Olivier Martinot | b9b2a5b63a | |
Olivier Martinot | 9f77b1df42 | |
Olivier Martinot | 2a5daa8145 | |
Olivier Martinot | fa5e4674f1 | |
Olivier Martinot | 4f9652e183 | |
Olivier Martinot | 68d98d2a78 | |
Olivier Martinot | f6b6b61d49 | |
Olivier Martinot | a512cb60c8 | |
Olivier | 4e4f411590 | |
Gabriel Scherer | 819fd28f48 | |
Gabriel Scherer | 666284748b | |
Gabriel Scherer | 70d02b454d | |
Olivier Martinot | 27e824b8e4 | |
Olivier | a1cb15c700 | |
Gabriel Scherer | dcb6df34b8 | |
Olivier Martinot | a3840b7662 |
285
client/Client.ml
285
client/Client.ml
|
@ -1,285 +0,0 @@
|
|||
(* 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 =
|
||||
Inferno.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
|
||||
)
|
|
@ -1,5 +0,0 @@
|
|||
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
|
|
@ -79,6 +79,21 @@ module Nominal2deBruijn (N : Map.OrderedType) = struct
|
|||
let current = current + 1 in
|
||||
{ map; current }
|
||||
|
||||
(* [concat env1 env2] extends [env1] with all the bindings of [env2];
|
||||
bindings of [env2] shadow any binding of the same variable in [env1]. *)
|
||||
|
||||
let concat env1 env2 =
|
||||
(* We need to shift the de Bruijn levels of [env2] (and its
|
||||
[current] value) by as many bindings as there are in [env1]. *)
|
||||
let shift _x in1 in2 =
|
||||
match in2 with
|
||||
| None -> in1
|
||||
| Some lvl -> Some (env1.current + lvl)
|
||||
in
|
||||
{
|
||||
current = env1.current + env2.current;
|
||||
map = M.merge shift env1.map env2.map;
|
||||
}
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
|
|
@ -50,6 +50,10 @@ module Nominal2deBruijn (N : Map.OrderedType) : sig
|
|||
|
||||
val bump: env -> env
|
||||
|
||||
(* [concat env1 env2] extends [env1] with all the bindings of [env2];
|
||||
bindings of [env2] shadow any binding of the same variable in [env1]. *)
|
||||
|
||||
val concat: env -> env -> env
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
|
70
client/F.ml
70
client/F.ml
|
@ -18,11 +18,12 @@
|
|||
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 *)
|
||||
|
||||
| TyProduct of ('a,'b) typ list
|
||||
| TySum of ('a,'b) typ list
|
||||
|
||||
(* BEGIN F *)
|
||||
type tyvar = int
|
||||
(* END F *)
|
||||
|
@ -53,13 +54,27 @@ type ('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
|
||||
| Tuple of ('a, 'b) term list
|
||||
| Proj of int * ('a, 'b) term
|
||||
| LetProd of tevar list * ('a, 'b) term * ('a, 'b) term
|
||||
| Inj of (('a,'b) typ list) * int * ('a,'b) term
|
||||
| Match of ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
|
||||
|
||||
and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
|
||||
|
||||
and ('a,'b) pattern =
|
||||
| PVar of tevar
|
||||
| PWildcard
|
||||
| PInj of (('a,'b) typ list) * int * ('a,'b) pattern
|
||||
| PTuple of ('a,'b) pattern list
|
||||
|
||||
|
||||
(* BEGIN F *)
|
||||
type nominal_term = (tyvar, tyvar) term
|
||||
(* END F *)
|
||||
|
||||
type nominal_pattern = (tyvar, tyvar) pattern
|
||||
|
||||
type debruijn_term =
|
||||
(DeBruijn.index, unit) term
|
||||
|
||||
|
@ -113,10 +128,6 @@ module TypeInType : DeBruijn.TRAVERSE
|
|||
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
|
||||
|
@ -125,7 +136,12 @@ module TypeInType : DeBruijn.TRAVERSE
|
|||
let env, x = extend env x in
|
||||
let ty1' = traverse lookup extend env ty1 in
|
||||
TyMu (x, ty1')
|
||||
|
||||
| TyProduct tys ->
|
||||
let tys' = List.map (traverse lookup extend env) tys in
|
||||
TyProduct tys'
|
||||
| TySum tys ->
|
||||
let tys' = List.map (traverse lookup extend env) tys in
|
||||
TySum tys'
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
@ -167,14 +183,44 @@ module TypeInTerm : DeBruijn.TRAVERSE
|
|||
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')
|
||||
| Tuple ts ->
|
||||
let ts' = List.map (traverse lookup extend env) ts in
|
||||
Tuple ts'
|
||||
| Proj (i, t) ->
|
||||
let t' = traverse lookup extend env t in
|
||||
Proj (i, t')
|
||||
| LetProd (xs, t1, t2) ->
|
||||
let t1' = traverse lookup extend env t1
|
||||
and t2' = traverse lookup extend env t2 in
|
||||
LetProd (xs, t1', t2')
|
||||
| Inj (tys, i, t) ->
|
||||
let tys' = List.map (TypeInType.traverse lookup extend env) tys
|
||||
and t' = traverse lookup extend env t in
|
||||
Inj (tys', i, t')
|
||||
| Match (ty, t, brs) ->
|
||||
let ty' = TypeInType.traverse lookup extend env ty in
|
||||
let t' = traverse lookup extend env t
|
||||
and brs' = List.map (traverse_branch lookup extend env) brs in
|
||||
Match (ty', t', brs')
|
||||
|
||||
and traverse_branch lookup extend env (pat,t) =
|
||||
(traverse_pattern lookup extend env pat,
|
||||
traverse lookup extend env t)
|
||||
|
||||
and traverse_pattern lookup extend env pat =
|
||||
match pat with
|
||||
| PVar x ->
|
||||
PVar x
|
||||
| PWildcard ->
|
||||
PWildcard
|
||||
| PInj (tys, i, pat) ->
|
||||
let tys' = List.map (TypeInType.traverse lookup extend env) tys
|
||||
and pat' = traverse_pattern lookup extend env pat in
|
||||
PInj (tys', i, pat')
|
||||
| PTuple ps ->
|
||||
let ps' = List.map (traverse_pattern lookup extend env) ps in
|
||||
PTuple ps'
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
|
21
client/F.mli
21
client/F.mli
|
@ -17,9 +17,10 @@
|
|||
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
|
||||
| TyProduct of ('a,'b) typ list
|
||||
| TySum of ('a,'b) typ list
|
||||
|
||||
type tyvar =
|
||||
int
|
||||
|
@ -48,12 +49,28 @@ type ('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
|
||||
| Tuple of ('a, 'b) term list
|
||||
| Proj of int * ('a, 'b) term
|
||||
| LetProd of tevar list * ('a, 'b) term * ('a, 'b) term
|
||||
(* TODO later: get rid of LetProd(xs, t, u)
|
||||
by using Match(t,PTuple(xs),u) instead *)
|
||||
| Inj of (('a,'b) typ list) * int * ('a,'b) term
|
||||
| Match of ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
|
||||
|
||||
and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
|
||||
|
||||
and ('a,'b) pattern =
|
||||
| PVar of tevar
|
||||
| PWildcard
|
||||
| PInj of (('a,'b) typ list) * int * ('a,'b) pattern
|
||||
| PTuple of ('a,'b) pattern list
|
||||
|
||||
type nominal_term =
|
||||
(tyvar, tyvar) term
|
||||
|
||||
type nominal_pattern =
|
||||
(tyvar, tyvar) pattern
|
||||
|
||||
type debruijn_term =
|
||||
(DeBruijn.index, unit) term
|
||||
|
||||
|
|
|
@ -10,113 +10,163 @@ open F
|
|||
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)
|
||||
let rec print_type ty =
|
||||
print_type_quant ty
|
||||
|
||||
and print_type ty =
|
||||
print_type_aux 3 ty
|
||||
and print_type_quant = function
|
||||
| TyMu (x, ty) ->
|
||||
string "mu " ^^
|
||||
print_tyvar x ^^
|
||||
dot ^^ space ^^
|
||||
print_type_quant ty
|
||||
| TyForall (x, ty) ->
|
||||
lbracket ^^
|
||||
print_tyvar x ^^
|
||||
rbracket ^^ space ^^
|
||||
print_type_quant ty
|
||||
| ty ->
|
||||
print_type_arrow ty
|
||||
|
||||
and print_type_arrow = function
|
||||
| TyArrow (ty1, ty2) ->
|
||||
print_type_atom ty1 ^^
|
||||
string " -> " ^^
|
||||
print_type_arrow ty2
|
||||
| ty ->
|
||||
print_type_atom ty
|
||||
|
||||
and print_type_atom = function
|
||||
| TyVar x ->
|
||||
print_tyvar x
|
||||
| TyProduct tys ->
|
||||
surround_separate_map 2 0 (lbrace ^^ rbrace)
|
||||
lbrace star rbrace print_type tys
|
||||
| TySum tys ->
|
||||
surround_separate_map 2 0 (lbracket ^^ rbracket)
|
||||
lbracket plus rbracket print_type tys
|
||||
| TyMu _ | TyForall _ | TyArrow _ as ty ->
|
||||
group (parens (print_type ty))
|
||||
|
||||
|
||||
let print_angle_type ty =
|
||||
surround 2 0 langle (print_type ty) rangle
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* 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
|
||||
let print_inj tys i t =
|
||||
string "inj" ^^
|
||||
print_angle_type (TySum tys) ^^ space ^^
|
||||
OCaml.int i ^^ space ^^
|
||||
t
|
||||
|
||||
let print_tuple print_elem elems =
|
||||
let contents =
|
||||
match elems with
|
||||
| [elem] -> print_elem elem ^^ comma
|
||||
| _ -> separate_map (comma ^^ space) print_elem elems in
|
||||
surround 2 0 lparen contents rparen
|
||||
|
||||
let print_let_in lhs rhs body =
|
||||
string "let " ^^ lhs
|
||||
^^ string " = " ^^ rhs
|
||||
^^ string " in " ^^ body
|
||||
|
||||
let rec print_term t =
|
||||
print_term_abs t
|
||||
|
||||
and print_term_abs = function
|
||||
| TyAbs (x, t1) ->
|
||||
string "FUN " ^^
|
||||
print_tyvar x ^^
|
||||
string " = " ^^
|
||||
print_term_abs t1
|
||||
| Let (x, t1, t2) ->
|
||||
print_let_in
|
||||
(string x)
|
||||
(print_term t1)
|
||||
(print_term_abs t2)
|
||||
| LetProd (xs, t1, t2) ->
|
||||
print_let_in
|
||||
(print_tuple string xs)
|
||||
(print_term t1)
|
||||
(print_term_abs t2)
|
||||
| Abs (x, ty1, t2) ->
|
||||
string "fun " ^^
|
||||
string x ^^
|
||||
string " : " ^^
|
||||
print_type ty1 ^^
|
||||
string " = " ^^
|
||||
print_term_abs t2
|
||||
| t ->
|
||||
print_term_proj t
|
||||
|
||||
and print_term_proj = function
|
||||
| Proj (i, t) ->
|
||||
string "proj" ^^
|
||||
langle ^^
|
||||
OCaml.int i ^^
|
||||
rangle ^^
|
||||
space ^^
|
||||
print_term_app t
|
||||
| Inj (ty1, i, t2) ->
|
||||
print_inj ty1 i (print_term_app t2)
|
||||
| t ->
|
||||
print_term_app t
|
||||
|
||||
and print_term_app = function
|
||||
| TyApp (t1, ty2) ->
|
||||
print_term_app t1 ^^
|
||||
space ^^ lbracket ^^
|
||||
print_type ty2 ^^
|
||||
rbracket
|
||||
| App (t1, t2) ->
|
||||
print_term_app t1 ^^
|
||||
space ^^
|
||||
print_term_atom t2
|
||||
| t ->
|
||||
print_term_atom t
|
||||
|
||||
and print_term_atom = function
|
||||
| Var x ->
|
||||
string x
|
||||
| Tuple ts ->
|
||||
print_tuple print_term ts
|
||||
| Match (ty, t, brs) ->
|
||||
string "match" ^^ print_angle_type ty ^^ space ^^
|
||||
print_term t ^^ space ^^
|
||||
string "with" ^^ hardline ^^
|
||||
print_branches brs ^^ space ^^
|
||||
string "end"
|
||||
| TyAbs _ | Let _ | LetProd _ | Abs _
|
||||
| Proj _ | Inj _ | TyApp _ | App _ as t ->
|
||||
group (parens (print_term t))
|
||||
|
||||
and print_branches brs =
|
||||
separate_map hardline print_branch brs
|
||||
|
||||
and print_branch (pat,t) =
|
||||
bar ^^ space ^^
|
||||
print_pattern pat ^^
|
||||
string " -> " ^^
|
||||
print_term t
|
||||
|
||||
and print_pattern pat =
|
||||
print_pattern_inj pat
|
||||
|
||||
and print_pattern_inj = function
|
||||
| PInj (tys, i, pat) ->
|
||||
print_inj tys i (print_pattern_atom pat)
|
||||
| pat ->
|
||||
print_pattern_atom pat
|
||||
|
||||
and print_pattern_atom = function
|
||||
| PVar x ->
|
||||
string x
|
||||
| PWildcard ->
|
||||
underscore
|
||||
| PTuple ps ->
|
||||
print_tuple print_pattern ps
|
||||
| PInj _ as pat ->
|
||||
group (parens (print_pattern pat))
|
||||
|
|
|
@ -1,5 +1,18 @@
|
|||
open F
|
||||
|
||||
type arity_requirement = Index of int | Total of int
|
||||
|
||||
type type_error =
|
||||
| TypeMismatch of debruijn_type * debruijn_type
|
||||
| ArityMismatch of arity_requirement * debruijn_type
|
||||
| NotAnArrow of debruijn_type
|
||||
| NotAProduct of debruijn_type
|
||||
| NotAForall of debruijn_type
|
||||
| UnboundTermVariable of tevar
|
||||
| TwoOccurencesOfSameVariable of string
|
||||
|
||||
exception TypeError of type_error
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* A type environment maps term variables to types in de Bruijn's representation. *)
|
||||
|
@ -34,8 +47,6 @@ type 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]. *)
|
||||
|
@ -47,7 +58,7 @@ let lookup { types; names } x =
|
|||
lift w 0 ty
|
||||
with Not_found ->
|
||||
(* must have been raised by [TermVarMap.find] *)
|
||||
raise (UnboundTermVariable x)
|
||||
raise (TypeError(UnboundTermVariable x))
|
||||
|
||||
let extend_with_tevar { types; names } x ty =
|
||||
(* Map the name [x] to [ty], and record when it was bound, without
|
||||
|
@ -59,6 +70,24 @@ let extend_with_tyvar { types; names } =
|
|||
(* Increment the time. *)
|
||||
{ types; names = N2DB.bump names }
|
||||
|
||||
let singleton x ty =
|
||||
extend_with_tevar empty x ty
|
||||
|
||||
let concat env1 env2 =
|
||||
let combine _ _ ty2 = Some ty2 in
|
||||
{ types = TermVarMap.union combine env1.types env2.types ;
|
||||
names = N2DB.concat env1.names env2.names }
|
||||
|
||||
let concat_disjoint env1 env2 =
|
||||
let exception Conflict of TermVarMap.key in
|
||||
try
|
||||
let combine x _ _ =
|
||||
raise (Conflict x) in
|
||||
let types = TermVarMap.union combine env1.types env2.types
|
||||
and names = N2DB.concat env1.names env2.names in
|
||||
Ok { types; names; }
|
||||
with Conflict x -> Error x
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Destructors. *)
|
||||
|
@ -70,8 +99,6 @@ let unfold ty =
|
|||
| _ ->
|
||||
assert false
|
||||
|
||||
exception NotAnArrow of debruijn_type
|
||||
|
||||
let rec as_arrow ty =
|
||||
match ty with
|
||||
| TyArrow (ty1, ty2) ->
|
||||
|
@ -79,20 +106,16 @@ let rec as_arrow ty =
|
|||
| TyMu _ ->
|
||||
as_arrow (unfold ty)
|
||||
| _ ->
|
||||
raise (NotAnArrow ty)
|
||||
|
||||
exception NotAProduct of debruijn_type
|
||||
raise (TypeError (NotAnArrow ty))
|
||||
|
||||
let rec as_product ty =
|
||||
match ty with
|
||||
| TyProduct (ty1, ty2) ->
|
||||
ty1, ty2
|
||||
| TyProduct tys ->
|
||||
tys
|
||||
| TyMu _ ->
|
||||
as_product (unfold ty)
|
||||
| _ ->
|
||||
raise (NotAProduct ty)
|
||||
|
||||
exception NotAForall of debruijn_type
|
||||
raise (TypeError(NotAProduct ty))
|
||||
|
||||
let rec as_forall ty =
|
||||
match ty with
|
||||
|
@ -101,7 +124,7 @@ let rec as_forall ty =
|
|||
| TyMu _ ->
|
||||
as_forall (unfold ty)
|
||||
| _ ->
|
||||
raise (NotAForall ty)
|
||||
raise (TypeError(NotAForall ty))
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -119,8 +142,6 @@ let rec as_forall ty =
|
|||
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
|
||||
|
@ -128,13 +149,23 @@ let rec equal budget ty1 ty2 =
|
|||
budget = 0 || equal (budget - 1) (unfold ty1) ty2
|
||||
| TyVar x1, TyVar x2 ->
|
||||
x1 = x2
|
||||
| TyVar _, _ ->
|
||||
false
|
||||
| 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
|
||||
| TyArrow _, _ ->
|
||||
false
|
||||
| TyProduct tys1, TyProduct tys2
|
||||
| TySum tys1, TySum tys2 ->
|
||||
(try
|
||||
List.for_all2 (equal budget) tys1 tys2
|
||||
with Invalid_argument _ -> false)
|
||||
| TyProduct _, _
|
||||
| TySum _, _ ->
|
||||
false
|
||||
| TyForall ((), ty1), TyForall ((), ty2) ->
|
||||
equal budget ty1 ty2
|
||||
| _, _ ->
|
||||
| TyForall _, _ ->
|
||||
false
|
||||
|
||||
let budget =
|
||||
|
@ -142,7 +173,13 @@ let budget =
|
|||
|
||||
let (--) ty1 ty2 =
|
||||
if not (equal budget ty1 ty2) then
|
||||
raise (TypeMismatch (ty1, ty2))
|
||||
raise (TypeError (TypeMismatch (ty1, ty2)))
|
||||
|
||||
let nth_type complete_ty tys i =
|
||||
if i < 0 || i >= List.length tys then
|
||||
raise (TypeError (ArityMismatch (Index i, complete_ty)))
|
||||
else
|
||||
List.nth tys i
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -166,12 +203,54 @@ let rec typeof env (t : debruijn_term) : debruijn_type =
|
|||
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)
|
||||
| Tuple ts ->
|
||||
TyProduct (List.map (typeof env) ts)
|
||||
| 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 ty = typeof env t in
|
||||
let tys = as_product ty in
|
||||
nth_type ty tys (i-1)
|
||||
| LetProd (xs, t, u) ->
|
||||
let ty = typeof env t in
|
||||
let tys = as_product ty in
|
||||
if List.length xs <> List.length tys then
|
||||
raise (TypeError (ArityMismatch (Total (List.length xs), ty)));
|
||||
let env = List.fold_left2 extend_with_tevar env xs tys in
|
||||
typeof env u
|
||||
| Inj (tys, i, t) ->
|
||||
let ty = typeof env t in
|
||||
ty -- nth_type (TySum tys) tys i;
|
||||
TySum tys
|
||||
|
||||
| Match (ty, t, brs) ->
|
||||
let scrutinee_ty = typeof env t in
|
||||
let tys = List.map (typeof_branch env scrutinee_ty) brs in
|
||||
List.iter ((--) ty) tys;
|
||||
ty
|
||||
|
||||
and typeof_branch env scrutinee_ty (pat, rhs) =
|
||||
let new_bindings = binding_pattern scrutinee_ty pat in
|
||||
let new_env = concat env new_bindings in
|
||||
typeof new_env rhs
|
||||
|
||||
and binding_pattern scrutinee_ty pat =
|
||||
match pat with
|
||||
| PVar x ->
|
||||
singleton x scrutinee_ty
|
||||
| PWildcard ->
|
||||
empty
|
||||
| PInj (tys, i, pat) ->
|
||||
scrutinee_ty -- TySum tys;
|
||||
let ty' = nth_type (TySum tys) tys i in
|
||||
binding_pattern ty' pat
|
||||
| PTuple ps ->
|
||||
let tys = as_product scrutinee_ty in
|
||||
let envs = List.map2 binding_pattern tys ps in
|
||||
let f env1 env2 =
|
||||
match concat_disjoint env1 env2 with
|
||||
| Ok env -> env
|
||||
| Error x -> raise (TypeError (TwoOccurencesOfSameVariable x))
|
||||
in
|
||||
List.fold_left f empty envs
|
||||
|
||||
let typeof =
|
||||
typeof empty
|
||||
|
|
|
@ -4,9 +4,18 @@ open 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
|
||||
type arity_requirement = Index of int | Total of int
|
||||
|
||||
type type_error =
|
||||
| TypeMismatch of debruijn_type * debruijn_type
|
||||
| ArityMismatch of arity_requirement * debruijn_type
|
||||
| NotAnArrow of debruijn_type
|
||||
| NotAProduct of debruijn_type
|
||||
| NotAForall of debruijn_type
|
||||
| UnboundTermVariable of tevar
|
||||
| TwoOccurencesOfSameVariable of string
|
||||
|
||||
exception TypeError of type_error
|
||||
|
||||
val typeof: debruijn_term -> debruijn_type
|
||||
|
||||
|
|
|
@ -0,0 +1,714 @@
|
|||
(* This sample client performs type inference for a fragment of ML and translates
|
||||
it down to a fragment of System F. *)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* During inference, we will need an environment to keep trace of
|
||||
* the user defined types *)
|
||||
|
||||
module Env = struct
|
||||
module LabelId = struct
|
||||
type t = ML.label_id
|
||||
let compare = Stdlib.compare
|
||||
end
|
||||
|
||||
module LabelIdMap =
|
||||
Map.Make(LabelId)
|
||||
|
||||
type label2descr = ML.label_descr list LabelIdMap.t
|
||||
|
||||
module TypeId = struct
|
||||
type t = ML.type_id
|
||||
let compare = Stdlib.compare
|
||||
end
|
||||
|
||||
module TypeIdMap =
|
||||
Map.Make(TypeId)
|
||||
|
||||
type data_type2descr = ML.data_type_descr TypeIdMap.t
|
||||
|
||||
(* Environment for user defined data types *)
|
||||
type t = {
|
||||
data_types : data_type2descr ;
|
||||
labels : label2descr
|
||||
}
|
||||
|
||||
exception UnexpectedRecord
|
||||
|
||||
let empty = {
|
||||
data_types = TypeIdMap.empty;
|
||||
labels = LabelIdMap.empty;
|
||||
}
|
||||
|
||||
let add_data_type m tdescr =
|
||||
TypeIdMap.add ML.(tdescr.name) tdescr m
|
||||
|
||||
let add_labels m ldescrs =
|
||||
List.fold_left (fun m ldescr ->
|
||||
match LabelIdMap.find_opt ML.(ldescr.label_name) m with
|
||||
| None -> LabelIdMap.add ML.(ldescr.label_name) [ldescr] m
|
||||
| Some l -> LabelIdMap.add ML.(ldescr.label_name) (ldescr::l) m
|
||||
) m ldescrs
|
||||
|
||||
let add_typedecl e tdescr = {
|
||||
data_types = add_data_type e.data_types tdescr;
|
||||
labels = add_labels e.labels ML.(tdescr.labels_descr);
|
||||
}
|
||||
|
||||
let descr_from_label { labels ; _ } (ML.Label l) : ML.label_descr list =
|
||||
LabelIdMap.find (ML.Label l) labels
|
||||
|
||||
let type_descr_from_type { data_types ; _ } (ML.Type tid) =
|
||||
TypeIdMap.find (ML.Type tid) data_types
|
||||
|
||||
let label_index (ML.({ labels_descr ; _ })) l =
|
||||
let combine i ldescr = (i, ML.(ldescr.label_name)) in
|
||||
List.mapi combine labels_descr
|
||||
|> List.find (fun (_, l') -> l = l')
|
||||
|> fst
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Translation from ML types to F types *)
|
||||
|
||||
let fresh_tyvar =
|
||||
let cpt = ref 0 in
|
||||
|
||||
(* We generate odd number for the user and even number for the solver *)
|
||||
fun () -> incr cpt; 2 * !cpt + 1
|
||||
|
||||
(* Here [rec_occur] is the function called when we encounter an
|
||||
* occurence of the name of the type we translate *)
|
||||
let rec translate_type
|
||||
(env : Env.t)
|
||||
(params : (string * F.nominal_type) list)
|
||||
(rec_occur : unit -> F.nominal_type)
|
||||
(name_self : ML.type_id)
|
||||
(ty : ML.nominal_type)
|
||||
: F.nominal_type =
|
||||
let rec tt (ty : ML.nominal_type) : F.nominal_type =
|
||||
match ty with
|
||||
| ML.TyVar x ->
|
||||
List.assoc x params
|
||||
|
||||
| ML.TyArrow (ty1, ty2) ->
|
||||
F.TyArrow (tt ty1, tt ty2)
|
||||
|
||||
| ML.TyProduct tys ->
|
||||
F.TyProduct (List.map tt tys)
|
||||
|
||||
| ML.TyConstr (tid, tys) ->
|
||||
if tid = name_self then begin
|
||||
let desc = Env.type_descr_from_type env name_self in
|
||||
|
||||
(* This assert should hold as long as we only treat
|
||||
* regular recursion, that is types in which each type parameters
|
||||
* is instantiated with only one type *)
|
||||
assert (tys = List.map (fun x -> ML.TyVar x) desc.ML.type_params);
|
||||
|
||||
rec_occur ()
|
||||
end
|
||||
else
|
||||
translate_type_expr env (List.map tt tys) tid
|
||||
in
|
||||
tt ty
|
||||
|
||||
and translate_typedecl
|
||||
(env : Env.t)
|
||||
(params : F.nominal_type list)
|
||||
(desc : ML.data_type_descr)
|
||||
(rec_occur : unit -> F.nominal_type)
|
||||
: F.nominal_type list =
|
||||
let params = List.combine ML.(desc.type_params) params in
|
||||
let tys =
|
||||
List.map (fun ldescr -> ML.(ldescr.arg_type)) ML.(desc.labels_descr)
|
||||
|> List.map (translate_type env params rec_occur ML.(desc.name))
|
||||
in
|
||||
tys
|
||||
|
||||
and translate_type_expr
|
||||
(env : Env.t)
|
||||
(params : F.nominal_type list)
|
||||
(type_id : ML.type_id)
|
||||
: F.nominal_type =
|
||||
let desc = Env.type_descr_from_type env type_id in
|
||||
let tau = fresh_tyvar () in
|
||||
let rec_occur () = F.TyVar tau in
|
||||
let tys = translate_typedecl env params desc rec_occur in
|
||||
F.TyMu (tau, F.TySum tys)
|
||||
|
||||
let translate_constr_types
|
||||
(env : Env.t)
|
||||
(params : F.nominal_type list)
|
||||
(type_id : ML.type_id)
|
||||
: F.nominal_type list =
|
||||
let desc = Env.type_descr_from_type env type_id in
|
||||
let rec_occur () =
|
||||
translate_type_expr env params type_id
|
||||
in
|
||||
translate_typedecl env params desc rec_occur
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The unifier will use the following type structure. *)
|
||||
|
||||
module S = struct
|
||||
|
||||
type 'a structure =
|
||||
| TyArrow of 'a * 'a
|
||||
| TyProduct of 'a list
|
||||
| TyConstr of ML.type_id * Env.t * 'a list
|
||||
|
||||
let map f t =
|
||||
match t with
|
||||
| TyArrow (t1, t2) ->
|
||||
let t1 = f t1 in
|
||||
let t2 = f t2 in
|
||||
TyArrow (t1, t2)
|
||||
| TyProduct ts ->
|
||||
let ts = List.map f ts in
|
||||
TyProduct ts
|
||||
| TyConstr (tid, env, ts) ->
|
||||
let ts = List.map f ts in
|
||||
TyConstr (tid, env, ts)
|
||||
|
||||
let fold f t accu =
|
||||
match t with
|
||||
| TyArrow (t1, t2) ->
|
||||
let accu = f t1 accu in
|
||||
let accu = f t2 accu in
|
||||
accu
|
||||
| TyProduct ts ->
|
||||
List.fold_right f ts accu
|
||||
| TyConstr (_, _, ts) ->
|
||||
List.fold_right f ts accu
|
||||
|
||||
let iter f t =
|
||||
let _ = map f t in
|
||||
()
|
||||
|
||||
exception Iter2
|
||||
|
||||
let iter2 f t u =
|
||||
let iter2_list f ts us =
|
||||
if List.length ts <> List.length us then raise Iter2;
|
||||
List.iter2 f ts us
|
||||
in
|
||||
match t, u with
|
||||
| TyArrow (t1, t2), TyArrow (u1, u2) ->
|
||||
f t1 u1;
|
||||
f t2 u2
|
||||
| TyProduct ts1, TyProduct ts2 ->
|
||||
iter2_list f ts1 ts2
|
||||
| TyConstr (tid1, _, ts1), TyConstr (tid2, _, ts2) ->
|
||||
if tid1 <> tid2 then raise Iter2;
|
||||
iter2_list f ts1 ts2
|
||||
| TyArrow _, _
|
||||
| TyProduct _, _
|
||||
| TyConstr _, _ ->
|
||||
raise Iter2
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The unifier type structure is decoded into the target calculus type structure
|
||||
as follows. *)
|
||||
|
||||
module O = struct
|
||||
|
||||
type tyvar =
|
||||
int
|
||||
|
||||
(* See also [fresh_tyvar] *)
|
||||
let solver_tyvar n =
|
||||
2 * n
|
||||
|
||||
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 ts ->
|
||||
F.TyProduct ts
|
||||
| S.TyConstr (tid, env, ts) ->
|
||||
translate_type_expr env ts tid
|
||||
|
||||
let mu x t =
|
||||
F.TyMu (x, t)
|
||||
|
||||
type scheme =
|
||||
tyvar list * ty
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Instantiate the solver. *)
|
||||
|
||||
module Solver =
|
||||
Inferno.SolverHi.Make(struct include String type tevar = t end)(S)(O)
|
||||
|
||||
open Solver
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
let arrow x y =
|
||||
S.TyArrow (x, y)
|
||||
|
||||
let product xs =
|
||||
S.TyProduct xs
|
||||
|
||||
let constr c env xs =
|
||||
S.TyConstr (c, env, xs)
|
||||
|
||||
(* 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
|
||||
)
|
||||
)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
let rec mapM_now (f : ('a -> ('b, 'r) binder)) (xs : 'a list)
|
||||
: ('b list, 'r) binder
|
||||
= fun k ->
|
||||
match xs with
|
||||
| [] ->
|
||||
k []
|
||||
| x :: xs ->
|
||||
let@ y = f x in
|
||||
let@ ys = mapM_now f xs in
|
||||
k (y :: ys)
|
||||
|
||||
let rec mapM_later (f : ('a -> ('c co, 'r) binder)) (xs : 'a list)
|
||||
: ('c list co, 'r) binder
|
||||
= fun k ->
|
||||
match xs with
|
||||
| [] ->
|
||||
k (pure [])
|
||||
| x::xs ->
|
||||
let@ y = f x in
|
||||
let@ ys = mapM_later f xs in
|
||||
k(let+ y = y
|
||||
and+ ys = ys
|
||||
in y :: ys)
|
||||
|
||||
let rec mapM_both (f : ('a -> ('b * 'c co, 'r) binder)) (xs : 'a list)
|
||||
: ('b list * 'c list co, 'r) binder
|
||||
= fun k ->
|
||||
match xs with
|
||||
| [] ->
|
||||
k ([], pure [])
|
||||
| x :: xs ->
|
||||
let@ (y, z) = f x in
|
||||
let@ (ys, zs) = mapM_both f xs in
|
||||
k (y::ys,
|
||||
let+z = z
|
||||
and+ zs = zs
|
||||
in z :: zs
|
||||
)
|
||||
|
||||
let instantiate_params (params : string list)
|
||||
: ((string * variable) list * (string * O.ty) list co, 'r) binder =
|
||||
let on_param (x : string) =
|
||||
fun k ->
|
||||
let@ (y, ty) = exist in
|
||||
k ((x, y), (pure x ^& ty))
|
||||
in
|
||||
mapM_both on_param params
|
||||
|
||||
let rec convert (env : Env.t) (params : (string * variable) list) (ty : ML.nominal_type)
|
||||
: (variable, 'r) binder
|
||||
= fun k ->
|
||||
match ty with
|
||||
| ML.TyVar tx ->
|
||||
let w = List.assoc tx params in
|
||||
k w
|
||||
|
||||
| ML.TyArrow (ty1, ty2) ->
|
||||
let@ w1 = convert env params ty1 in
|
||||
let@ w2 = convert env params ty2 in
|
||||
let@ w = exist_ in
|
||||
let+ () = w --- arrow w1 w2
|
||||
and+ res = k w
|
||||
in res
|
||||
|
||||
| ML.TyProduct tys ->
|
||||
let@ w = exist_ in
|
||||
let@ ws = mapM_now (convert env params) tys in
|
||||
let+ () = w --- product ws
|
||||
and+ res = k w
|
||||
in res
|
||||
|
||||
| ML.TyConstr (tid, tys) ->
|
||||
let@ w = exist_ in
|
||||
let@ ws = mapM_now (convert env params) tys in
|
||||
let+ () = w --- constr tid env ws
|
||||
and+ res = k w
|
||||
in res
|
||||
|
||||
exception VariableConflict of string
|
||||
|
||||
let convert_annot typedecl_env ((flex_vars, ty) : ML.nominal_annotation)
|
||||
: (variable, 'r) binder
|
||||
= fun k ->
|
||||
let@ params =
|
||||
flex_vars |> mapM_now (fun alpha k -> let@ v = exist_ in k (alpha, v)) in
|
||||
let@ v = convert typedecl_env params ty in
|
||||
k v
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* 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 hastype (typedecl_env : Env.t) (t : ML.term) (w : variable) : F.nominal_term co
|
||||
=
|
||||
let rec hastype t w =
|
||||
match t with
|
||||
|
||||
(* Variable. *)
|
||||
| ML.Var x ->
|
||||
|
||||
(* [w] must be an instance of the type scheme associated with [x]. *)
|
||||
let+ tys = instance x w in
|
||||
(* 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. *)
|
||||
let@ (v1, ty1) = exist in
|
||||
(* Here, we could use [exist_], because we do not need [ty2]. I refrain
|
||||
from using it, just to simplify the paper. *)
|
||||
let@ (v2, _ty2) = exist in
|
||||
(* [w] must be the function type [v1 -> v2]. *)
|
||||
let+ () = w --- arrow v1 v2
|
||||
(* Under the assumption that [x] has type [domain], the term [u] must
|
||||
have type [codomain]. *)
|
||||
and+ u' = def x v1 (hastype u v2)
|
||||
and+ ty1 = ty1
|
||||
in
|
||||
(* 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')
|
||||
|
||||
| ML.App (t1, t2) ->
|
||||
|
||||
(* Introduce a type variable to stand for the unknown argument type. *)
|
||||
let@ (v, _ty) = exist in
|
||||
let+ t1' = lift hastype t1 (arrow v w)
|
||||
and+ t2' = hastype t2 v
|
||||
in F.App (t1', t2')
|
||||
|
||||
(* Generalization. *)
|
||||
| ML.Let (x, t, u) ->
|
||||
|
||||
(* Construct a ``let'' constraint. *)
|
||||
let+ ((b, _), a, t', u') = let1 x (hastype t) (hastype u w) in
|
||||
(* [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 *)
|
||||
|
||||
| ML.Annot (t, annot) ->
|
||||
let@ v = convert_annot typedecl_env annot in
|
||||
let+ () = v -- w
|
||||
and+ t' = hastype t v in
|
||||
t'
|
||||
|
||||
| ML.Tuple ts ->
|
||||
let on_term (t:ML.term) : ('b * 'c co, 'r) binder =
|
||||
fun (k : ('b * 'c co) -> 'r co) : 'r co ->
|
||||
let@ v : 'b = exist_ in
|
||||
let t = hastype t v in
|
||||
k (v, t)
|
||||
in
|
||||
|
||||
let@ (vs, ts') = mapM_both on_term ts in
|
||||
let+ () = w --- product vs
|
||||
and+ ts' = ts'
|
||||
in F.Tuple ts'
|
||||
|
||||
| ML.LetProd (xs, t, u) ->
|
||||
let on_var (x:ML.tevar) : ('a, 'r) binder =
|
||||
fun (k : 'b -> 'r co) : 'r co ->
|
||||
let@ v = exist_ in
|
||||
def x v (k v)
|
||||
in
|
||||
|
||||
let@ vs = mapM_now on_var xs in
|
||||
let+ t' = lift hastype t (product vs)
|
||||
and+ u' = hastype u w
|
||||
in F.LetProd(xs, t', u')
|
||||
|
||||
| ML.Variant (c, t) ->
|
||||
let ML.{ type_name ; arg_type ; _ } =
|
||||
match Env.descr_from_label typedecl_env c with
|
||||
| [ d ] ->
|
||||
d
|
||||
| _ ->
|
||||
failwith "todo"
|
||||
in
|
||||
|
||||
let ML.{ type_params ; data_kind ; _ } as tdescr =
|
||||
Env.type_descr_from_type typedecl_env type_name in
|
||||
|
||||
if not data_kind then
|
||||
raise Env.UnexpectedRecord;
|
||||
|
||||
(* We begin by instantiating the type parameters of the variant's type *)
|
||||
let@ param_vars, param_types = instantiate_params type_params in
|
||||
|
||||
(* Inference variable for the argument of the variant *)
|
||||
let@ w1 = convert typedecl_env param_vars arg_type in
|
||||
|
||||
(* Retrieve the index of the constructor in the list of labels_descr *)
|
||||
let i = Env.label_index tdescr c in
|
||||
|
||||
let+ () = w --- (constr type_name typedecl_env @@ List.map snd param_vars)
|
||||
and+ param_types = param_types
|
||||
and+ t' = hastype t w1
|
||||
in
|
||||
let sumtype =
|
||||
translate_constr_types typedecl_env (List.map snd param_types) type_name in
|
||||
F.Inj (sumtype, i, t')
|
||||
|
||||
| ML.Match (t, branches) ->
|
||||
(* Inference variable for the type of the scrutinee
|
||||
* (and of the patterns) *)
|
||||
let@ v = exist_ in
|
||||
|
||||
let@ branches' = hastype_branches typedecl_env branches v in
|
||||
|
||||
(* Get the type of the whole match statement *)
|
||||
let@ (w', ty) = exist in
|
||||
|
||||
let+ t = hastype t v
|
||||
and+ branches' = branches'
|
||||
and+ () = w -- w'
|
||||
and+ ty = ty
|
||||
in F.Match (ty, t, branches')
|
||||
|
||||
and hastype_branches (typedecl_env : Env.t) (branches : ML.branch list) (v : Solver.variable)
|
||||
: ((F.nominal_pattern * F.nominal_term) list co, 'r) binder
|
||||
=
|
||||
let rec bind_pattern_vars
|
||||
(pat_env : (ML.tevar * variable) list) (u : ML.term)
|
||||
: F.nominal_term co
|
||||
= match pat_env with
|
||||
| [] ->
|
||||
(* Here we use [w] because [t] should have the same type
|
||||
* as the whole match statement *)
|
||||
hastype u w
|
||||
| (x, v1) :: pat_env ->
|
||||
def x v1 @@ bind_pattern_vars pat_env u
|
||||
in
|
||||
|
||||
let on_branch ((pat,u) : ML.branch)
|
||||
: ((F.nominal_pattern * F.nominal_term) co, 'r) binder
|
||||
= fun k ->
|
||||
(* [hastype_pat pat v] returns a list of variable [pat_env] that we
|
||||
* must bind, and a System F pattern [pat] *)
|
||||
let@ (pat_env, pat) = hastype_pat typedecl_env pat v in
|
||||
|
||||
(* We translate the ML term [t] into System F and bind the
|
||||
* pattern variables on the fly *)
|
||||
let u = bind_pattern_vars pat_env u in
|
||||
|
||||
k (pat ^& u)
|
||||
in
|
||||
|
||||
mapM_later on_branch branches
|
||||
|
||||
and hastype_pat (typedecl_env : Env.t) (pat : ML.pattern) (w : variable)
|
||||
: ((ML.tevar * variable) list * F.nominal_pattern co, 'r) binder
|
||||
= fun k ->
|
||||
match pat with
|
||||
| ML.PVar x ->
|
||||
let pat_env = [(x, w)] in
|
||||
k (pat_env, pure (F.PVar x))
|
||||
|
||||
| ML.PWildcard ->
|
||||
k ([], pure (F.PWildcard))
|
||||
|
||||
| ML.PAnnot (pat, annot) ->
|
||||
let@ v = convert_annot typedecl_env annot in
|
||||
let@ (pat_env, pat) = hastype_pat typedecl_env pat v in
|
||||
let+ () = v -- w
|
||||
and+ res = k (pat_env, pat)
|
||||
in res
|
||||
|
||||
| ML.PTuple pats ->
|
||||
|
||||
let rec union_ env1 env2 =
|
||||
match env1 with
|
||||
| [] ->
|
||||
env2
|
||||
| ((x, _) as e) :: env1 ->
|
||||
if List.mem_assoc x env2 then
|
||||
raise (VariableConflict x);
|
||||
union_ env1 (e::env2)
|
||||
in
|
||||
|
||||
let union envs =
|
||||
List.fold_left union_ [] envs in
|
||||
|
||||
let on_pattern (pat : ML.pattern)
|
||||
: ((Solver.variable * (ML.tevar * variable) list)
|
||||
* F.nominal_pattern co, 'r) binder
|
||||
= fun k ->
|
||||
let@ v = exist_ in
|
||||
let@ (pat_env, pat) = hastype_pat typedecl_env pat v in
|
||||
k ((v,pat_env), pat)
|
||||
in
|
||||
|
||||
let@ (l, pats) = mapM_both on_pattern pats in
|
||||
let (vs, pat_envs) = List.split l in
|
||||
let pat_env = union pat_envs in
|
||||
|
||||
k (pat_env,
|
||||
let+ () = w --- product vs
|
||||
and+ pats = pats
|
||||
in F.PTuple pats)
|
||||
|
||||
| ML.PVariant (c, pat) ->
|
||||
(* See the ML.Variant case of [hastype] for details *)
|
||||
let ML.{ type_name ; arg_type ; _ } =
|
||||
match Env.descr_from_label typedecl_env c with
|
||||
| [ d ] ->
|
||||
d
|
||||
| _ ->
|
||||
failwith "todo"
|
||||
in
|
||||
|
||||
let ML.{ type_params ; data_kind ; _ } as tdescr =
|
||||
Env.type_descr_from_type typedecl_env type_name in
|
||||
|
||||
if not data_kind then
|
||||
raise Env.UnexpectedRecord;
|
||||
|
||||
let@ param_vars, param_types = instantiate_params type_params in
|
||||
|
||||
let@ v1 = exist_ in
|
||||
|
||||
let@ w1 = convert typedecl_env param_vars arg_type in
|
||||
|
||||
let i = Env.label_index tdescr c in
|
||||
|
||||
let@ (pat_env, pat) = hastype_pat typedecl_env pat v1 in
|
||||
|
||||
k(pat_env,
|
||||
let+ () = w --- (constr type_name typedecl_env @@ List.map snd param_vars)
|
||||
and+ param_types = param_types
|
||||
and+ () = w1 -- v1
|
||||
and+ pat = pat
|
||||
in
|
||||
let sumtype =
|
||||
translate_constr_types typedecl_env (List.map snd param_types) type_name in
|
||||
F.PInj (sumtype, i, pat))
|
||||
|
||||
in
|
||||
hastype t w
|
||||
|
||||
(* 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 (e : Env.t) (t : ML.term) : F.nominal_term =
|
||||
solve false (
|
||||
let0 (exist_ (hastype e t)) <$$> fun (vs, t) ->
|
||||
(* [vs] are the binders that we must introduce *)
|
||||
F.ftyabs vs t
|
||||
)
|
|
@ -0,0 +1,11 @@
|
|||
exception Unbound of string
|
||||
exception Unify of F.nominal_type * F.nominal_type
|
||||
exception Cycle of F.nominal_type
|
||||
|
||||
module Env : sig
|
||||
type t
|
||||
val empty : t
|
||||
val add_typedecl : t -> ML.data_type_descr -> t
|
||||
end
|
||||
|
||||
val translate: Env.t -> ML.term -> F.nominal_term
|
47
client/ML.ml
47
client/ML.ml
|
@ -1,17 +1,54 @@
|
|||
(* 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 tevar = string
|
||||
type type_id = Type of string
|
||||
type label_id = Label of string
|
||||
|
||||
type ('a,'b) typ =
|
||||
| TyVar of 'a
|
||||
| TyArrow of ('a,'b) typ * ('a,'b) typ
|
||||
| TyProduct of ('a,'b) typ list
|
||||
| TyConstr of type_id * ('a,'b) typ list
|
||||
|
||||
type ('a, 'b) annotation = 'b list * ('a, 'b) typ
|
||||
(* some <flexible vars> . <ty> *)
|
||||
|
||||
type nominal_type = (string,string) typ
|
||||
type nominal_annotation = (string,string) annotation
|
||||
|
||||
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
|
||||
| Annot of term * nominal_annotation
|
||||
| Tuple of term list
|
||||
| LetProd of tevar list * term * term
|
||||
| Variant of label_id * term
|
||||
| Match of term * branch list
|
||||
|
||||
and branch = pattern * term
|
||||
|
||||
and pattern =
|
||||
| PVar of tevar
|
||||
| PWildcard
|
||||
| PAnnot of pattern * nominal_annotation
|
||||
| PVariant of label_id * pattern
|
||||
| PTuple of pattern list
|
||||
|
||||
type data_type_descr = {
|
||||
name : type_id ;
|
||||
type_params : string list ;
|
||||
data_kind : bool ; (* true for variants, false for records *)
|
||||
labels_descr : label_descr list
|
||||
}
|
||||
|
||||
and label_descr = {
|
||||
label_name : label_id ;
|
||||
type_name : type_id ;
|
||||
arg_type : nominal_type
|
||||
}
|
||||
|
|
258
client/Main.ml
258
client/Main.ml
|
@ -1,258 +0,0 @@
|
|||
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";
|
||||
print_type ty1;
|
||||
Printf.fprintf stdout "and the type:\n";
|
||||
print_type ty2
|
||||
end;
|
||||
None
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Running all passes over a single ML term. *)
|
||||
|
||||
let test (t : ML.term) : bool =
|
||||
let log = create_log() in
|
||||
let outcome =
|
||||
attempt log
|
||||
"Type inference and translation to System F...\n"
|
||||
translate t
|
||||
in
|
||||
match outcome with
|
||||
| None ->
|
||||
(* This term is ill-typed. This is considered a normal outcome, since
|
||||
our terms can be randomly generated. *)
|
||||
false
|
||||
| Some (t : F.nominal_term) ->
|
||||
log_action log (fun () ->
|
||||
Printf.printf "Formatting the System F term...\n%!";
|
||||
let doc = PPrint.(FPrinter.print_term t ^^ hardline) in
|
||||
Printf.printf "Pretty-printing the System F term...\n%!";
|
||||
PPrint.ToChannel.pretty 0.9 80 stdout doc
|
||||
);
|
||||
let t : F.debruijn_term =
|
||||
attempt log
|
||||
"Converting the System F term to de Bruijn style...\n"
|
||||
F.translate t
|
||||
in
|
||||
let _ty : F.debruijn_type =
|
||||
attempt log
|
||||
"Type-checking the System F term...\n"
|
||||
FTypeChecker.typeof t
|
||||
in
|
||||
(* Everything seems to be OK. *)
|
||||
if verbose then
|
||||
print_log log;
|
||||
true
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* A few manually constructed terms. *)
|
||||
|
||||
let x =
|
||||
ML.Var "x"
|
||||
|
||||
let y =
|
||||
ML.Var "y"
|
||||
|
||||
let id =
|
||||
ML.Abs ("x", x)
|
||||
|
||||
let delta =
|
||||
ML.Abs ("x", ML.App (x, x))
|
||||
|
||||
let deltadelta =
|
||||
ML.App (delta, delta)
|
||||
|
||||
let idid =
|
||||
ML.App (id, id)
|
||||
|
||||
let k =
|
||||
ML.Abs ("x", ML.Abs ("y", x))
|
||||
|
||||
let genid =
|
||||
ML.Let ("x", id, x)
|
||||
|
||||
let genidid =
|
||||
ML.Let ("x", id, ML.App (x, x))
|
||||
|
||||
let genkidid =
|
||||
ML.Let ("x", ML.App (k, id), ML.App (x, id))
|
||||
|
||||
let genkidid2 =
|
||||
ML.Let ("x", ML.App (ML.App (k, id), id), x)
|
||||
|
||||
let app_pair = (* ill-typed *)
|
||||
ML.App (ML.Pair (id, id), id)
|
||||
|
||||
let () =
|
||||
assert (test idid);
|
||||
assert (test genid);
|
||||
assert (test genidid);
|
||||
assert (test genkidid);
|
||||
assert (test genkidid2)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Random testing. *)
|
||||
|
||||
(* A list of pairs [m, n], where [m] is the number of tests and [n] is the
|
||||
size of the randomly generated terms. *)
|
||||
|
||||
let pairs = [
|
||||
100000, 5;
|
||||
100000, 10;
|
||||
100000, 15;
|
||||
100000, 20;
|
||||
100000, 25; (* at this size, about 1% of the terms are well-typed *)
|
||||
100000, 30;
|
||||
(* At the following sizes, no terms are well-typed! *)
|
||||
10000, 100;
|
||||
10000, 500;
|
||||
1000, 1000;
|
||||
100, 10000;
|
||||
10, 100000;
|
||||
1, 1000000;
|
||||
]
|
||||
|
||||
let () =
|
||||
Printf.printf "Preparing to type-check a bunch of randomly-generated terms...\n%!";
|
||||
Random.init 0;
|
||||
let c = ref 0 in
|
||||
let d = ref 0 in
|
||||
List.iter (fun (m, n) ->
|
||||
for i = 1 to m do
|
||||
if verbose then
|
||||
Printf.printf "Test number %d...\n%!" i;
|
||||
let t = random_ml_term 0 n in
|
||||
assert (size t = n);
|
||||
let success = test t in
|
||||
if success then incr c;
|
||||
incr d
|
||||
done
|
||||
) pairs;
|
||||
Printf.printf "In total, %d out of %d terms were considered well-typed.\n%!" !c !d;
|
||||
Printf.printf "No problem detected.\n%!"
|
|
@ -1,5 +1,5 @@
|
|||
(test
|
||||
(name Main)
|
||||
(libraries unix pprint inferno)
|
||||
(library
|
||||
(name client)
|
||||
(libraries pprint inferno)
|
||||
(flags "-w" "@1..66-4-44")
|
||||
)
|
||||
|
|
|
@ -0,0 +1,68 @@
|
|||
open Client
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* 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 ~verbose e t =
|
||||
try
|
||||
Some (Infer.translate e t)
|
||||
with
|
||||
| Infer.Cycle ty ->
|
||||
if verbose then begin
|
||||
Printf.fprintf stdout "Type error: a cyclic type arose.\n";
|
||||
print_type ty
|
||||
end;
|
||||
None
|
||||
| Infer.Unify (ty1, ty2) ->
|
||||
if verbose then begin
|
||||
Printf.fprintf stdout "Type inference error: type mismatch.\n";
|
||||
Printf.fprintf stdout "Type inference error: mismatch between the type:\n";
|
||||
print_type ty1;
|
||||
Printf.fprintf stdout "and the type:\n";
|
||||
print_type ty2
|
||||
end;
|
||||
None
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Running all passes over a single ML term. *)
|
||||
|
||||
let test ?(verbose=Config.verbose) (e : Infer.Env.t) (t : ML.term) : bool =
|
||||
let log = Log.create_log() in
|
||||
let outcome =
|
||||
Log.attempt log
|
||||
"Type inference and translation to System F...\n"
|
||||
(translate ~verbose) e t
|
||||
in
|
||||
match outcome with
|
||||
| None ->
|
||||
(* This term is ill-typed. This is considered a normal outcome, since
|
||||
our terms can be randomly generated. *)
|
||||
false
|
||||
| Some (t : F.nominal_term) ->
|
||||
Log.log_action log (fun () ->
|
||||
Printf.printf "Formatting the System F term...\n%!";
|
||||
let doc = PPrint.(FPrinter.print_term t ^^ hardline) in
|
||||
Printf.printf "Pretty-printing the System F term...\n%!";
|
||||
PPrint.ToChannel.pretty 0.9 80 stdout doc
|
||||
);
|
||||
let t : F.debruijn_term =
|
||||
Log.attempt log
|
||||
"Converting the System F term to de Bruijn style...\n"
|
||||
F.translate t
|
||||
in
|
||||
let _ty : F.debruijn_type =
|
||||
Log.attempt log
|
||||
"Type-checking the System F term...\n"
|
||||
FTypeChecker.typeof t
|
||||
in
|
||||
(* Everything seems to be OK. *)
|
||||
if verbose then
|
||||
Log.print_log log;
|
||||
true
|
|
@ -0,0 +1,5 @@
|
|||
let verbose =
|
||||
true
|
||||
|
||||
let very_verbose =
|
||||
false
|
|
@ -0,0 +1,40 @@
|
|||
(* 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
|
|
@ -0,0 +1,101 @@
|
|||
open Client
|
||||
module Log = Test.Log
|
||||
|
||||
(* ∀a b. ({} -> (a * (a -> b))) -> b
|
||||
Λa b. fun (p : {} -> (a * (a -> b))) ->
|
||||
let (x, f) = p () in f x
|
||||
*)
|
||||
let let_prod =
|
||||
let open F in
|
||||
let alpha, beta = 0, 1 in
|
||||
let p, f, x = "p", "f", "x" in
|
||||
TyAbs (alpha, TyAbs (beta,
|
||||
Abs (p, TyArrow (TyProduct [],
|
||||
TyProduct [TyVar alpha; TyArrow (TyVar alpha, TyVar beta)]),
|
||||
LetProd ([x; f], App (Var p, Tuple []),
|
||||
App (Var f, Var x)))))
|
||||
|
||||
(* Inj<∀α. α → α + ∀βα. α → β> 0 Λα.λx:α.x *)
|
||||
let variant =
|
||||
let alpha, beta = 0, 1 in
|
||||
F.(
|
||||
Inj
|
||||
(
|
||||
[
|
||||
TyForall (alpha, TyArrow (TyVar alpha, TyVar alpha)) ;
|
||||
TyForall (beta, TyForall (alpha, TyArrow (TyVar alpha, TyVar beta)))
|
||||
],
|
||||
0,
|
||||
TyAbs (alpha, Abs("x", TyVar alpha, Var "x"))
|
||||
)
|
||||
)
|
||||
|
||||
(* Λαβ. λx. match x with (_, y) -> y end *)
|
||||
let match_with =
|
||||
let alpha, beta = 1, 0 in
|
||||
F.(
|
||||
TyAbs(alpha,
|
||||
TyAbs(beta,
|
||||
Abs("x",
|
||||
TyProduct [ TyVar alpha ; TyVar beta ],
|
||||
Match(TyVar beta,
|
||||
Var "x",
|
||||
[
|
||||
(PTuple [ PWildcard ; PVar "y" ] ,
|
||||
Var "y")
|
||||
]
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
|
||||
(* Λβ. match () with
|
||||
* | () -> ()
|
||||
* | (_) -> ()
|
||||
*)
|
||||
let match_none = F.(
|
||||
let alpha = 25 in
|
||||
let beta = 308 in
|
||||
let option_type = [ TyProduct []; TyProduct [TyVar beta] ] in
|
||||
let none = Inj ( option_type, 0, Tuple []) in
|
||||
TyAbs(beta,
|
||||
Match (
|
||||
TyMu (alpha, TySum option_type ),
|
||||
none,
|
||||
[
|
||||
PInj ( option_type, 0, PTuple []),
|
||||
none
|
||||
;
|
||||
PInj ( option_type, 1, PTuple [PWildcard]),
|
||||
none
|
||||
]
|
||||
)
|
||||
)
|
||||
)
|
||||
|
||||
|
||||
let print_term t =
|
||||
PPrint.(ToChannel.pretty 0.9 80 stdout
|
||||
(FPrinter.print_term t ^^ hardline))
|
||||
|
||||
let test_f (t : F.nominal_term) =
|
||||
let log = Log.create_log () in
|
||||
print_term t;
|
||||
let t : F.debruijn_term =
|
||||
Log.attempt log
|
||||
"Converting the System F term to de Bruijn style...\n"
|
||||
F.translate t
|
||||
in
|
||||
let _ty : F.debruijn_type =
|
||||
Log.attempt log
|
||||
"Type-checking the System F term...\n"
|
||||
FTypeChecker.typeof t
|
||||
in
|
||||
()
|
||||
|
||||
let () =
|
||||
test_f let_prod;
|
||||
test_f variant;
|
||||
test_f match_with;
|
||||
test_f match_none
|
|
@ -0,0 +1,194 @@
|
|||
open Client
|
||||
|
||||
(* A few manually constructed terms. *)
|
||||
|
||||
let x =
|
||||
ML.Var "x"
|
||||
|
||||
let y =
|
||||
ML.Var "y"
|
||||
|
||||
let id =
|
||||
ML.Abs ("x", x)
|
||||
|
||||
let delta =
|
||||
ML.Abs ("x", ML.App (x, x))
|
||||
|
||||
let deltadelta =
|
||||
ML.App (delta, delta)
|
||||
|
||||
let idid =
|
||||
ML.App (id, id)
|
||||
|
||||
let k =
|
||||
ML.Abs ("x", ML.Abs ("y", x))
|
||||
|
||||
let genid =
|
||||
ML.Let ("x", id, x)
|
||||
|
||||
let genidid =
|
||||
ML.Let ("x", id, ML.App (x, x))
|
||||
|
||||
let genkidid =
|
||||
ML.Let ("x", ML.App (k, id), ML.App (x, id))
|
||||
|
||||
let genkidid2 =
|
||||
ML.Let ("x", ML.App (ML.App (k, id), id), x)
|
||||
|
||||
let app_pair = (* ill-typed *)
|
||||
ML.App (ML.Tuple [id; id], id)
|
||||
|
||||
(* option *)
|
||||
let option_env =
|
||||
|
||||
(* type 'a option = None | Some of 'a *)
|
||||
let option_typedecl = ML.{
|
||||
name = Type "option";
|
||||
type_params = [ "a" ];
|
||||
data_kind = true;
|
||||
labels_descr = [
|
||||
{
|
||||
label_name = Label"None";
|
||||
type_name = Type "option";
|
||||
arg_type = TyProduct [];
|
||||
} ; {
|
||||
label_name = Label "Some";
|
||||
type_name = Type "option";
|
||||
arg_type = TyVar "a";
|
||||
}
|
||||
]
|
||||
} in
|
||||
|
||||
Infer.Env.add_typedecl Infer.Env.empty option_typedecl
|
||||
|
||||
let none = ML.Variant ( ML.Label "None" , ML.Tuple [] )
|
||||
|
||||
let some =
|
||||
ML.Variant (
|
||||
ML.Label "Some",
|
||||
id
|
||||
)
|
||||
|
||||
let match_none = ML.(
|
||||
Match (none, [
|
||||
PVariant (Label "None", PTuple []), none ;
|
||||
PVariant (Label "Some", PTuple [(PVar "x")]), x
|
||||
])
|
||||
)
|
||||
|
||||
let match_some = ML.(
|
||||
Match (some, [
|
||||
PVariant (Label "None", PTuple []), none ;
|
||||
PVariant (Label "Some", PWildcard), none
|
||||
])
|
||||
)
|
||||
|
||||
let match_some_annotated = ML.(
|
||||
Match (some, [
|
||||
( PVariant (Label "None", PTuple []), none );
|
||||
( PAnnot (PVariant (Label "Some", PWildcard),
|
||||
(["a"], TyConstr (Type "option", [ TyVar "a" ]))),
|
||||
none );
|
||||
])
|
||||
)
|
||||
|
||||
(* list *)
|
||||
let list_env =
|
||||
|
||||
(* type 'a list = Nil | Cons of 'a * 'a list *)
|
||||
let list_typedecl = ML.{
|
||||
name = Type "list";
|
||||
type_params = [ "a" ];
|
||||
data_kind = true;
|
||||
labels_descr = [
|
||||
{
|
||||
label_name = Label "Nil";
|
||||
type_name = Type "list";
|
||||
arg_type = TyProduct [];
|
||||
} ; {
|
||||
label_name = Label "Cons";
|
||||
type_name = Type "list";
|
||||
arg_type = TyProduct [ TyVar "a" ; TyConstr (Type "list", [ TyVar "a" ]) ];
|
||||
}
|
||||
]
|
||||
} in
|
||||
|
||||
Infer.Env.add_typedecl option_env list_typedecl
|
||||
|
||||
let nil = ML.Variant ( ML.Label "Nil" , ML.Tuple [] )
|
||||
|
||||
let list =
|
||||
ML.Variant (
|
||||
ML.Label "Cons",
|
||||
ML.Tuple [ id ; nil ]
|
||||
)
|
||||
|
||||
let list_annotated =
|
||||
let open ML in
|
||||
Annot (
|
||||
Variant (
|
||||
Label "Cons",
|
||||
Tuple [ Annot (id, (["a"], TyArrow (TyVar "a", TyVar "a")));
|
||||
nil ]
|
||||
),
|
||||
(["a"; "b"], TyConstr (Type "list", [TyArrow (TyVar "a", TyVar "b")]))
|
||||
)
|
||||
|
||||
(* tree *)
|
||||
let tree_env =
|
||||
|
||||
(* type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree *)
|
||||
let tree_typedecl = ML.{
|
||||
name = Type "tree";
|
||||
type_params = [ "a" ];
|
||||
data_kind = true;
|
||||
labels_descr = [
|
||||
{
|
||||
label_name = Label "Leaf";
|
||||
type_name = Type "tree";
|
||||
arg_type = TyProduct []
|
||||
} ; {
|
||||
label_name = Label "Node";
|
||||
type_name = Type "tree";
|
||||
arg_type = TyProduct [
|
||||
TyConstr (Type "tree", [ TyVar "a" ]);
|
||||
TyVar "a";
|
||||
TyConstr (Type "tree", [ TyVar "a" ]);
|
||||
]
|
||||
}
|
||||
]
|
||||
} in
|
||||
|
||||
Infer.Env.add_typedecl list_env tree_typedecl
|
||||
|
||||
let leaf = ML.Variant ( ML.Label "Leaf" , ML.Tuple [] )
|
||||
|
||||
let node =
|
||||
ML.Variant (
|
||||
ML.Label "Node",
|
||||
ML.Tuple [
|
||||
leaf ;
|
||||
id ;
|
||||
leaf ;
|
||||
]
|
||||
)
|
||||
|
||||
let () =
|
||||
assert (Test.CheckML.test Infer.Env.empty idid);
|
||||
assert (Test.CheckML.test Infer.Env.empty genid);
|
||||
assert (Test.CheckML.test Infer.Env.empty genidid);
|
||||
assert (Test.CheckML.test Infer.Env.empty genkidid);
|
||||
assert (Test.CheckML.test Infer.Env.empty genkidid2);
|
||||
assert (Test.CheckML.test option_env none);
|
||||
assert (Test.CheckML.test option_env some);
|
||||
assert (Test.CheckML.test list_env nil);
|
||||
assert (Test.CheckML.test list_env list);
|
||||
assert (Test.CheckML.test list_env list_annotated);
|
||||
assert (Test.CheckML.test tree_env leaf);
|
||||
assert (Test.CheckML.test tree_env node);
|
||||
assert (Test.CheckML.test option_env match_none);
|
||||
assert (Test.CheckML.test option_env match_some);
|
||||
assert (Test.CheckML.test option_env match_some_annotated);
|
||||
(* we include some printing below because Dune
|
||||
appears to only show tests that show some output. *)
|
||||
print_endline "TestML: all tests passed."
|
|
@ -0,0 +1,130 @@
|
|||
open Client
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* 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, Let, LetProd *) 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.Tuple [random_ml_term k n1; random_ml_term k n2]
|
||||
else if c = 3 then
|
||||
let n1, n2 = split (n - 1) in
|
||||
ML.Let (int2var k, random_ml_term k n1, random_ml_term (k + 1) n2)
|
||||
else if c = 4 then
|
||||
let n1, n2 = split (n - 1) in
|
||||
let x1, x2, k' = int2var k, int2var (k + 1), k + 2 in
|
||||
ML.LetProd ([x1; x2], random_ml_term k n1, random_ml_term k' n2)
|
||||
else
|
||||
assert false
|
||||
|
||||
let rec size accu = function
|
||||
| ML.Var _ ->
|
||||
accu
|
||||
| ML.Abs (_, t)
|
||||
| ML.Variant (_, t)
|
||||
| ML.Annot (t, _)
|
||||
-> size (accu + 1) t
|
||||
| ML.App (t1, t2)
|
||||
| ML.Let (_, t1, t2)
|
||||
| ML.LetProd (_, t1, t2)
|
||||
-> size (size (accu + 1) t1) t2
|
||||
| ML.Tuple ts
|
||||
-> List.fold_left size (accu + 1) ts
|
||||
| ML.Match (t, brs)
|
||||
-> List.fold_left size_branch (size (accu + 1) t) brs
|
||||
|
||||
and size_branch accu (pat,u) =
|
||||
size (size_pattern accu pat) u
|
||||
|
||||
and size_pattern accu = function
|
||||
| ML.PVar _ ->
|
||||
accu
|
||||
| ML.PWildcard ->
|
||||
accu
|
||||
| ML.PTuple ps ->
|
||||
List.fold_left size_pattern (accu + 1) ps
|
||||
| ML.PVariant (_, p)
|
||||
| ML.PAnnot (p, _) ->
|
||||
size_pattern (accu + 1) p
|
||||
|
||||
|
||||
|
||||
let size =
|
||||
size 0
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Random testing. *)
|
||||
|
||||
(* A list of pairs [m, n], where [m] is the number of tests and [n] is the
|
||||
size of the randomly generated terms. *)
|
||||
|
||||
let pairs =
|
||||
match Sys.getenv_opt "INFERNO_SLOW_TESTS" with
|
||||
| Some ("0" | "false" | "") | None -> [
|
||||
10_000, 10;
|
||||
10_000, 15;
|
||||
]
|
||||
| Some _ -> [
|
||||
100_000, 5;
|
||||
100_000, 10;
|
||||
100_000, 15;
|
||||
100_000, 20;
|
||||
100_000, 25; (* at this size, about 1% of the terms are well-typed *)
|
||||
100_000, 30;
|
||||
(* At the following sizes, no terms are well-typed! *)
|
||||
10_000, 100;
|
||||
10_000, 500;
|
||||
1000, 1000;
|
||||
100, 10_000;
|
||||
10, 100_000;
|
||||
1, 1_000_000;
|
||||
]
|
||||
|
||||
let () =
|
||||
Printf.printf "Preparing to type-check a bunch of randomly-generated terms...\n%!";
|
||||
Random.init 0;
|
||||
let c = ref 0 in
|
||||
let d = ref 0 in
|
||||
List.iter (fun (m, n) ->
|
||||
for i = 1 to m do
|
||||
if Test.Config.very_verbose then
|
||||
Printf.printf "Test number %d...\n%!" i;
|
||||
let t = random_ml_term 0 n in
|
||||
assert (size t = n);
|
||||
let success =
|
||||
Test.CheckML.test ~verbose:Test.Config.very_verbose Infer.Env.empty t in
|
||||
if success then incr c;
|
||||
incr d
|
||||
done
|
||||
) pairs;
|
||||
Printf.printf "In total, %d out of %d terms were considered well-typed.\n%!" !c !d;
|
||||
Printf.printf "No problem detected.\n%!"
|
|
@ -0,0 +1,24 @@
|
|||
(library
|
||||
(name test)
|
||||
(libraries client)
|
||||
(modules Config Log CheckML)
|
||||
(flags "-w" "@1..66-4-44")
|
||||
)
|
||||
|
||||
(test
|
||||
(name TestML)
|
||||
(libraries client test)
|
||||
(modules TestML)
|
||||
)
|
||||
|
||||
(test
|
||||
(name TestMLRandom)
|
||||
(libraries client test)
|
||||
(modules TestMLRandom)
|
||||
)
|
||||
|
||||
(test
|
||||
(name TestF)
|
||||
(libraries client test)
|
||||
(modules TestF)
|
||||
)
|
|
@ -53,9 +53,17 @@ module Make (S : STRUCTURE) (U : UNIFIER with type 'a structure = 'a S.structure
|
|||
pool number [j], where [i <= j] holds. Immediately after generalization has
|
||||
been performed, the array has been updated, so [i = j] holds. *)
|
||||
|
||||
(* A set of callbacks associated to
|
||||
frozen constraints on a variable (see CFrozen) *)
|
||||
type freezer = (U.variable * (U.variable S.structure -> unit)) list
|
||||
|
||||
type state = {
|
||||
(* An array of pools (lists of variables), indexed by ranks. *)
|
||||
pool: U.variable list InfiniteArray.t;
|
||||
|
||||
(* An array of freezers indexed by ranks *)
|
||||
freezers: freezer InfiniteArray.t;
|
||||
|
||||
(* The current rank. *)
|
||||
mutable young: int;
|
||||
}
|
||||
|
@ -136,6 +144,7 @@ let base_rank =
|
|||
|
||||
let init () = {
|
||||
pool = InfiniteArray.make 8 [];
|
||||
freezers = InfiniteArray.make 8 [];
|
||||
young = no_rank;
|
||||
}
|
||||
|
||||
|
@ -206,7 +215,8 @@ let show_state label state =
|
|||
|
||||
let enter state =
|
||||
state.young <- state.young + 1;
|
||||
assert (InfiniteArray.get state.pool state.young = [])
|
||||
assert (InfiniteArray.get state.pool state.young = []);
|
||||
assert (InfiniteArray.get state.freezers state.young = [])
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -257,9 +267,45 @@ let make_scheme (is_generic : U.variable -> bool) (body : U.variable) : scheme =
|
|||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
exception RemainingFrozenVariables of U.variable list
|
||||
|
||||
let flush_freezer state =
|
||||
let freezer = InfiniteArray.get state.freezers state.young in
|
||||
|
||||
let rec loop freezer : unit =
|
||||
let work_done = ref false in
|
||||
let still_frozen =
|
||||
freezer |> List.filter (fun (v, callback) ->
|
||||
match U.structure v with
|
||||
| None ->
|
||||
true
|
||||
| Some t ->
|
||||
callback t;
|
||||
work_done := true;
|
||||
false
|
||||
) in
|
||||
if !work_done then
|
||||
loop still_frozen
|
||||
else
|
||||
if still_frozen = [] then
|
||||
()
|
||||
else
|
||||
raise (RemainingFrozenVariables
|
||||
(List.map fst still_frozen))
|
||||
in
|
||||
|
||||
loop freezer;
|
||||
|
||||
InfiniteArray.set state.freezers state.young []
|
||||
|
||||
let register_frozen state v callback =
|
||||
let freezer = InfiniteArray.get state.freezers state.young in
|
||||
InfiniteArray.set state.freezers state.young ((v, callback) :: freezer)
|
||||
|
||||
(* [exit] is where the moderately subtle generalization work takes place. *)
|
||||
|
||||
let exit rectypes state roots =
|
||||
flush_freezer state;
|
||||
|
||||
(* Get the list [vs] of all variables in the young generation. *)
|
||||
let vs = InfiniteArray.get state.pool state.young in
|
||||
|
|
|
@ -91,6 +91,9 @@ module Make (S : STRUCTURE) (U : UNIFIER with type 'a structure = 'a S.structure
|
|||
|
||||
val enter: state -> unit
|
||||
|
||||
val flush_freezer: state -> unit
|
||||
val register_frozen: state -> variable -> (variable structure -> unit) -> unit
|
||||
|
||||
(* [exit] updates the current state by popping a [CLet] construct. This
|
||||
involves an inspection of the unifier state. The most recent [CLet]
|
||||
construct, combined with the unifier state, takes the form [let exist
|
||||
|
|
|
@ -81,8 +81,11 @@ let map f (rc, k) =
|
|||
fun env -> f (k env)
|
||||
(* END MAP *)
|
||||
|
||||
(* The function [<$$>] is just [map] with reversed argument order. *)
|
||||
let (let+) a f = map f a
|
||||
let (and+) = (^&)
|
||||
|
||||
|
||||
(* The function [<$$>] is just [map] with reversed argument order. *)
|
||||
(* BEGIN RMAP *)
|
||||
let (<$$>) a f =
|
||||
map f a
|
||||
|
@ -109,19 +112,25 @@ let (^^) (rc1, k1) (rc2, k2) =
|
|||
|
||||
(* Existential quantification. *)
|
||||
|
||||
type ('a, 'r) binder = ('a -> 'r co) -> 'r co
|
||||
|
||||
let (let@) m f = m f
|
||||
|
||||
(* BEGIN EXIST *)
|
||||
let exist f =
|
||||
(* Create a fresh unifier variable [v]. *)
|
||||
let v = fresh None in
|
||||
(* Pass [v] to the client. *)
|
||||
let rc, k = f v in
|
||||
(* Wrap the constraint [c] in an existential quantifier, *)
|
||||
CExist (v, rc),
|
||||
(* and construct a continuation which returns a pair of the witness for [v]
|
||||
and the value of the underlying continuation [k]. *)
|
||||
fun env ->
|
||||
let decode = env in
|
||||
(decode v, k env)
|
||||
(* Construct a continuation which returns the witness for [v]. *)
|
||||
let ty =
|
||||
CTrue,
|
||||
(fun env ->
|
||||
let decode = env in
|
||||
decode v)
|
||||
in
|
||||
(* Pass [v] to the client, *)
|
||||
let rc, k = f (v, ty) in
|
||||
(* and wrap the resulting constraint [rc] in an existential quantifier. *)
|
||||
CExist (v, rc), k
|
||||
(* END EXIST *)
|
||||
|
||||
(* [construct] is identical to [exist], except [None] is replaced with
|
||||
|
@ -130,11 +139,14 @@ let exist f =
|
|||
|
||||
let construct t f =
|
||||
let v = fresh (Some t) in
|
||||
let rc, k = f v in
|
||||
CExist (v, rc),
|
||||
fun env ->
|
||||
let decode = env in
|
||||
(decode v, k env)
|
||||
let ty =
|
||||
CTrue,
|
||||
(fun env ->
|
||||
let decode = env in
|
||||
decode v)
|
||||
in
|
||||
let rc, k = f (v, ty) in
|
||||
CExist (v, rc), k
|
||||
|
||||
let exist_aux_ t f =
|
||||
let v = fresh t in
|
||||
|
@ -266,6 +278,18 @@ let let0 c1 =
|
|||
letn [] (fun _ -> c1) (pure ()) <$$>
|
||||
fun (_, generalizable, v1, ()) -> (generalizable, v1)
|
||||
|
||||
let frozen w : (variable S.structure, 'r) binder =
|
||||
fun (k : variable S.structure -> 'r co) ->
|
||||
let rk_hook : (env -> 'r) WriteOnceRef.t =
|
||||
WriteOnceRef.create () in
|
||||
let callback t =
|
||||
let (rc, rk) = k t in
|
||||
WriteOnceRef.set rk_hook rk;
|
||||
rc
|
||||
in
|
||||
CFrozen (w, callback),
|
||||
fun env -> WriteOnceRef.get rk_hook env
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Running a constraint. *)
|
||||
|
|
|
@ -60,6 +60,9 @@ module Make
|
|||
(* ---------------------------------------------------------------------- *)
|
||||
(* END HI *)
|
||||
|
||||
val (let+): 'a co -> ('a -> 'b) -> 'b co
|
||||
val (and+): 'a co -> 'b co -> ('a * 'b) co
|
||||
|
||||
(* Variants of the above. *)
|
||||
|
||||
(* [<$$>] is just [map] with reversed argument order. *)
|
||||
|
@ -86,18 +89,22 @@ module Make
|
|||
|
||||
(* Existential quantification. *)
|
||||
|
||||
type ('a, 'r) binder = ('a -> 'r co) -> 'r co
|
||||
|
||||
val (let@) : ('a, 'r) binder -> ('a -> 'r co) -> 'r co
|
||||
|
||||
(* Assume that the user-supplied function [c], applied to a fresh type
|
||||
variable [v], produces a constraint of type ['a]. Then, [exist c] wraps it
|
||||
in an existential quantifier for [v]. This results in a constraint of type
|
||||
[ty * 'a], where the left-hand component of the pair, a decoded type, is
|
||||
the witness for [v]. *)
|
||||
val exist: (variable -> 'a co) -> (ty * 'a) co
|
||||
val exist: (variable * ty co, 'r) binder
|
||||
|
||||
(* END HI *)
|
||||
(* [construct t c] is analogous to [exist c], but additionally constrains
|
||||
the type variable [v] to be equal to the type [t]. So, it is really a
|
||||
way of constructing a variable that stands for a shallow term. *)
|
||||
val construct: variable structure -> (variable -> 'a co) -> (ty * 'a) co
|
||||
val construct: variable structure -> (variable * ty co, 'r) binder
|
||||
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -105,8 +112,8 @@ module Make
|
|||
|
||||
(* The following variants are used when one does not need access to the
|
||||
witness. [exist_ body] is logically equivalent to [exist body <$$> snd]. *)
|
||||
val exist_: (variable -> 'a co) -> 'a co
|
||||
val construct_: variable structure -> (variable -> 'a co) -> 'a co
|
||||
val exist_: (variable, 'r) binder
|
||||
val construct_: variable structure -> (variable, 'r) binder
|
||||
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -164,6 +171,8 @@ module Make
|
|||
val letn: tevar list -> (variable list -> 'a co) -> 'b co ->
|
||||
(scheme list * tyvar list * 'a * 'b) co
|
||||
|
||||
val frozen : variable -> (variable S.structure, 'r) binder
|
||||
|
||||
(* BEGIN HI *)
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
|
|
|
@ -72,6 +72,7 @@ type rawco =
|
|||
* rawco
|
||||
* rawco
|
||||
* variable list WriteOnceRef.t
|
||||
| CFrozen of variable * (variable S.structure -> rawco)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -152,7 +153,8 @@ let solve (rectypes : bool) (c : rawco) : unit =
|
|||
in
|
||||
(* Proceed to solve [c2] in the extended environment. *)
|
||||
solve env c2
|
||||
|
||||
| CFrozen (v, callback) ->
|
||||
G.register_frozen state v (fun t -> solve env (callback t))
|
||||
in
|
||||
solve XMap.empty c
|
||||
|
||||
|
@ -170,7 +172,7 @@ let decode_variable (x : variable) : O.tyvar =
|
|||
time of writing this comment, the API does not expose the decoder,
|
||||
so the client should have no way of violating this assertion. *)
|
||||
assert (U.rank x <> G.no_rank);
|
||||
U.id x
|
||||
O.solver_tyvar (U.id x)
|
||||
|
||||
let decode_variable_as_type (x : variable) : O.ty =
|
||||
O.variable (decode_variable x)
|
||||
|
|
|
@ -92,6 +92,7 @@ module Make
|
|||
* rawco
|
||||
* rawco
|
||||
* variable list WriteOnceRef.t
|
||||
| CFrozen of variable * (variable S.structure -> rawco)
|
||||
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
|
|
|
@ -38,9 +38,12 @@ end
|
|||
|
||||
(* BEGIN OUTPUT *)
|
||||
module type OUTPUT = sig
|
||||
(* nominal type variables *)
|
||||
type tyvar
|
||||
|
||||
(* The solver represents type variables via unique integer identifiers. *)
|
||||
type tyvar = int
|
||||
(* The solver represents inference variables via unique integer identifiers,
|
||||
and needs to be able to inject them into decoded type variables. *)
|
||||
val solver_tyvar : int -> tyvar
|
||||
|
||||
(* The solver works with first-order types whose structure is defined by
|
||||
the type ['a structure], as in the signature [Unifier.STRUCTURE]. *)
|
||||
|
|
Loading…
Reference in New Issue