Compare commits

...

158 Commits

Author SHA1 Message Date
Olivier 3f52bf2a87 Treat CFrozen case in the solve function of SolverLo.ml 2020-07-29 10:53:50 +02:00
Olivier 6184864d10 Add function register_frozen 2020-07-29 10:53:50 +02:00
Olivier 028172053a Add a function flush_freezer 2020-07-29 10:53:50 +02:00
Olivier 3698d045e1 Add frozen combinator in SolverHi 2020-07-29 10:53:00 +02:00
Olivier 286df69574 The typedecl environment now contains a mapping from label to a list of label_descr 2020-07-29 10:53:00 +02:00
Olivier 14d11151d4 Add a new CFrozen constraint 2020-07-29 10:53:00 +02:00
Olivier 68fc16d361 Merge pull request 'Type annotations in expressions and patterns' (#14) from gasche/inferno-experimental:annotations into master 2020-07-29 10:44:21 +02:00
Olivier 66a0235b90 Merge pull request 'Minor fixes' (#13) from gasche/inferno-experimental:minor-fixes into master 2020-07-29 10:44:02 +02:00
Gabriel Scherer f36fe293ba add type annotations in patterns as well 2020-07-27 21:26:31 +02:00
Gabriel Scherer eff9b56b71 add simple annotations to the term syntax
(<term> : some <vars>. <ty>)

binding flexible variables, for example

  ((fun x -> x) : some a b. a -> b)

equivalent to OCaml's

  ((fun x -> x) : _ -> _)
2020-07-27 21:26:31 +02:00
Gabriel Scherer 5957849cea ensure that unification fails on incompatible type constructors 2020-07-27 21:08:07 +02:00
Gabriel Scherer d21d21f9b6 fix typo in TestMLRandom again 2020-07-27 18:46:10 +02:00
Olivier 86c2fa0577 Use mapM_both instead of traverse in hastype_pat 2020-07-22 11:04:20 +02:00
Olivier 9057451455 Add a ' to variable name of inferred system F terms 2020-07-22 11:04:20 +02:00
Olivier 8eb6fb44de Rename bind_list and bind2_list into mapM_now and mapM_both 2020-07-22 11:04:20 +02:00
Olivier a5f8bc6df0 Add mapM_later operator and rewrite hastype_branches using it 2020-07-22 11:04:20 +02:00
Olivier fa66414eb3 Rename type declaration environments into typedecl_env 2020-07-22 11:04:20 +02:00
Olivier 7f76dbaaf7 Rename exception TwoOccurencesOfSameVariable into VariableConflict 2020-07-22 11:04:20 +02:00
Olivier 5d9c03c250 Fix tests 2020-07-22 11:04:20 +02:00
Olivier 971ee24f0c In hastype_pat, rename env into pat_env 2020-07-22 11:04:20 +02:00
Olivier e03b8e4899 Fix PVar case in hastype_pat 2020-07-22 11:04:20 +02:00
Olivier 388e62260d Add a function hastype_branches 2020-07-22 11:04:20 +02:00
Olivier 4ef4625639 Rename variable t in branches into u 2020-07-22 11:04:20 +02:00
Olivier 412f73cd2d Fix size function in TestMLRandom.ml 2020-07-22 11:04:20 +02:00
Olivier 1a9821c86c Add System F test 2020-07-22 11:04:20 +02:00
Olivier eefb1dbcfb Add tests for Match 2020-07-22 11:04:20 +02:00
Olivier 0cdd6f2836 Add hastype_pat 2020-07-22 11:04:20 +02:00
Olivier 494c29cc17 Add Match case in hastype 2020-07-22 11:04:20 +02:00
Olivier 2a5fabc29a Add a Match constructor in ML.term 2020-07-22 11:04:20 +02:00
Gabriel Scherer 42750df730 Merge pull request 'variants' (#11) from variants into master 2020-07-20 09:46:42 +02:00
Olivier f71f878b79 Correct typo in TestMLRandom 2020-07-20 09:42:47 +02:00
Olivier 0e04318e4a Simplify the inference for Variants by removing a useless inference variable 2020-07-19 07:52:22 +02:00
Olivier 4f69f391ed Add comments 2020-07-19 07:50:36 +02:00
Olivier 8d5b691071 Remove useless "ML.( _ )" annotations in TestML.ml 2020-07-04 19:53:11 +02:00
Olivier b528dc6417 Fix a bug in the test file
The bug is due to a wrong copy/pasta !
2020-07-04 19:49:58 +02:00
Olivier 1499305f8f S.TyConstr now contains an environment 2020-07-04 19:15:24 +02:00
Olivier 6f1e2ac714 Closer to a correct translation of S.TyConstr into a System F term 2020-07-03 20:38:51 +02:00
Olivier f5b74073e3 Environment in its own sub module 2020-07-03 20:28:12 +02:00
Olivier 8de13a0208 Move environment definition and translate function to the top of the file 2020-07-03 19:51:33 +02:00
Olivier 79cca9e052 S.TyConstr take a type declaration as argument 2020-07-03 19:19:43 +02:00
Olivier f4271dd44c Add tests with standard tree type 2020-07-03 14:54:19 +02:00
Olivier 696a8932e8 The arguments of variants are single terms (no longer lists) 2020-07-03 14:28:32 +02:00
Olivier d846d4e46a iter2 is more robust 2020-07-03 14:03:16 +02:00
Olivier c8609f9aba Remove debug prints 2020-07-03 14:00:28 +02:00
Olivier ccd6dea901 Fix bug in the equality function of FTypeChecker
The last case of the pattern matching
	 `_,_ -> false`
didn't warned us when we introduced a new construct in system F (variants).
I corrected the function so that the next time we'll add a new construct to system F a
non-exhaustiveness warning will be triggered
2020-07-03 13:15:36 +02:00
Olivier 721e694121 Define translate_type functions 2020-07-03 10:01:35 +02:00
Olivier fc01111e50 Better error message 2020-07-03 09:55:43 +02:00
Olivier 1568dae672 Add test with list type 2020-07-03 09:55:11 +02:00
Olivier 92a14778d3 Separate label_id and type_id 2020-07-03 09:53:24 +02:00
Olivier 96e3d95b29 We need to separate solver and system F variables.
We use even numbers for the first one and odd numbers for the second.
2020-07-02 15:49:27 +02:00
Olivier 0357300fe5 Config.very_verbose for random tests 2020-07-02 15:45:17 +02:00
Olivier 90414caeb0 Remove unnecessary type annotations 2020-07-02 15:45:17 +02:00
Olivier 039cc7b620 wip translate_constr_types 2020-07-02 15:45:17 +02:00
Olivier 590e0ac6df Injections start from 0 (not from 1 anymore) 2020-07-02 15:45:17 +02:00
Olivier 69238b35c2 Add an ML.Variant test 2020-07-02 15:45:17 +02:00
Olivier 3645fd189f Fix minor bug 2020-07-02 15:45:17 +02:00
Olivier 9b680ba84e Remove redundant argument in add_typedecl 2020-07-02 15:45:17 +02:00
Olivier e3c149479e Pattern-matching in TestMLRandom.ml is now exhaustive 2020-07-02 15:45:17 +02:00
Olivier a88aab13b6 Fix minor bug 2020-07-02 15:45:17 +02:00
Olivier 07b324d442 Add helper functions for type declarations environment 2020-07-02 15:45:17 +02:00
Olivier 9706c54fd6 Add environment argument in translate functions 2020-07-02 15:45:17 +02:00
Olivier 2253f20f4c Instantiate_params use bind2_list 2020-07-02 15:45:17 +02:00
Olivier 3fe6ff93dd Rename subst into translate_type 2020-07-02 15:45:17 +02:00
Olivier 7cc9feedc1 Add another instantiate_params function 2020-07-02 15:45:17 +02:00
Olivier 28c086094f Esthetic modifications 2020-07-02 15:45:17 +02:00
Olivier 67a3d5829a Rewrite traverse function in the LetProd case using bind_list 2020-07-02 15:45:17 +02:00
Olivier 1b96dd56fb Rewrite traverse functions using bind2_list 2020-07-02 15:45:17 +02:00
Olivier db37408267 Add function bind2_list 2020-07-02 15:45:17 +02:00
Olivier 22a861e510 Hide the environment to the recursive calls to hastype 2020-07-02 15:45:17 +02:00
Olivier 4cd22737a7 Change "vars" identifier to "params" in convert 2020-07-02 15:45:17 +02:00
Olivier 75a1c609e2 Simplify index_label 2020-07-02 15:45:17 +02:00
Olivier 818d839a46 Add comments 2020-07-02 15:45:17 +02:00
Olivier a96b2e90ad Update the return type of instantiate_params, add function translate_typedecl 2020-07-02 15:45:17 +02:00
Olivier 27b2c67b97 Continue treating the Variant case in hastype 2020-07-02 15:45:17 +02:00
Olivier 108ac2a8dc Begin treating the Variant case in hastype 2020-07-02 15:45:17 +02:00
Olivier 5f6188bbf7 Write instantiate_params with exist_ instead of fresh 2020-07-02 15:45:17 +02:00
Olivier 2fade74170 Add a bind_list function that is more generic than previously defined "traverse" functions 2020-07-02 15:45:17 +02:00
Olivier 8579357e83 Simplify traverse, rename it to convert_list 2020-07-02 15:45:17 +02:00
Olivier f6986c873d Fix typo, simplify code 2020-07-02 15:45:17 +02:00
Olivier a983f7e5ba Add a function that converts ML types into S.structure 2020-07-02 15:45:17 +02:00
Olivier 206ef0bc41 Add a function that instantiate type parameters 2020-07-02 15:45:17 +02:00
Olivier cefbe0fbb9 Add an environment as argument of hastype 2020-07-02 15:45:17 +02:00
Olivier a27a966b54 Add a Variant constructor in ML.term 2020-07-02 15:45:17 +02:00
Olivier 170e8a55f5 Define an environment type and a few helper functions 2020-07-02 15:45:17 +02:00
Olivier 55b71be6b1 Add types in ML 2020-07-02 15:45:17 +02:00
Olivier 4562909c32 Add TyConstr in type structure 2020-07-02 15:45:17 +02:00
Gabriel Scherer b1b9c97544 Merge branch 'tyvar-master' 2020-07-02 15:44:20 +02:00
Gabriel Scherer 4d9633d1e9 SolverSig: use an abstract type for O.tyvar
Currently the Output module signature used by SolverHi lets user provide
their own `ty` type to represent elaborated types, but it defines

    type tyvar = int

to directly inject solver-generated inference variable identifier as
types.

There is a difference in abstraction level here: a signature such as
`mu : tyvar -> ty -> ty` has a first parameter that is a low-level
type fixed by the solver, and the second parameter that is
a user-determined abstract type.

This lack of abstraction for type variables is problematic for users
that would want to generate elaborated types on their own, without
going through inference variables. For example, consider
language-level support for parametrized type abbreviations:

    type 'a cps = { run : 'r . ('a -> 'r) -> 'r }

If we want to reflect a user annotation of the form `foo cps` into
a System F type `∀r. (〚foo〛→r)→r`, we need to generate a Forall
quantifier for `'r`. But how would the user pick a "fresh" nominal
variable that is guaranteed to be distinct from those generated by the
solver ?  (There may be inference variables in scope used in `foo`).

Currently it is not possible for the user to generate System F binders
that are guaranteed to be free of conflicts with solver-generated
variables. The simple change in this commit makes this possible by
making the `tyvar` type abstract, with an explicit conversion function
between unique integers and user type variables.

This enables several possible strategies for users to implement
a `fresh_tyvar : unit -> tyvar` on the side, that does not conflict
with `solver_tyvar`. For example:

1. Keep `tyvar = int` but store already-used identifiers in
   a hashtable that is used to provide a conflict-avoiding translation
   in `solver_tyvar`.
2. Use even numbers for solver variables and odd numbers for user
   variables.
3. Use `type tyvar = Solver of int | User of ...`.

We *could* use approaches (1) and (2) above without the separation
(with the conversion done purely on the client side), but we believe
that enforcing the separation in the Output signature is the better
design. It forces users to give a thought to their tyvar
representation (it's easy to just use `int` and the identity), so they
will know where to go change things if the need for user-side fresh
variables arises. Without this API-level guidance, worse solution
would be considered (our first idea when hitting this issue was to
expose Inferno's fresh-identifier generator to clients).
2020-07-02 15:42:07 +02:00
Gabriel Scherer 73dabefdfd Merge pull request 'New API' (#10) from new-api into master 2020-06-11 15:14:07 +02:00
Gabriel Scherer 097378a909 Merge pull request 'pretty-printer' (#9) from pretty-printer into master 2020-06-05 09:05:55 +02:00
Olivier 5481126b64 Fix indentation in hastype 2020-06-04 17:42:09 +02:00
Olivier 15a4255424 Update ML.LetProd case 2020-06-04 17:41:17 +02:00
Olivier f726ca1cda Update ML.Let case 2020-06-04 17:34:25 +02:00
Olivier d3faf24a39 Change SolverHi interface using binder in type annotations 2020-06-04 17:25:54 +02:00
Olivier 233efdb84e Replace some code with "let@ ... = ... in" construct 2020-06-04 16:54:47 +02:00
Olivier cf1cfb96c4 Add binder type and (let@) 2020-06-04 16:43:19 +02:00
Olivier 682e7c003a Fix typo 2020-06-04 16:32:37 +02:00
Olivier 169cf41605 Update ML.Tuple case 2020-06-01 10:14:03 +02:00
Olivier 1d5bfae6d7 Update ML.App case 2020-06-01 09:46:23 +02:00
Olivier 29a743a30c Update ML.Abs case 2020-06-01 09:38:38 +02:00
Olivier 4da217c3e5 Add let+/and+ binding operators 2020-05-28 16:59:24 +02:00
Olivier 77f169c168 New type for construct 2020-05-28 16:53:48 +02:00
Olivier 0a9a61daa5 New type for exist 2020-05-28 16:20:16 +02:00
Olivier 1a142aa745 Change levels for subterms of Let/LetProd/App 2020-05-28 15:17:35 +02:00
Olivier 81ab70ff75 PInj has now its own level 2020-05-28 10:02:41 +02:00
Olivier 66e2905e28 In App/TyApp cases, we now call print_term_app instead of print_term_atom 2020-05-28 09:58:40 +02:00
Olivier cf68a69b6b In the Let/LetProd cases, we now call print_term instead of print_term_abs 2020-05-28 09:54:59 +02:00
Olivier bc7b3895f7 List unhandled constructors in the atom case 2020-05-28 09:48:46 +02:00
Olivier 8103dacf02 Move already delimited cases into atom 2020-05-28 09:44:34 +02:00
Olivier 0755533396 Proj/Inj on their own level 2020-05-28 09:41:13 +02:00
Olivier 34f850c880 Use print_term_*/print_type_* instead of * 2020-05-28 09:30:30 +02:00
Olivier d2c2043392 Pretty print terms without levels 2020-05-27 10:45:33 +02:00
Olivier f6d439c9a2 Pretty print types without levels 2020-05-26 22:42:40 +02:00
Olivier ad3cafd0c8 Merge pull request 'N-ary tuples in ML, to reveal the difficulty of creating inference variables dynamically' (#8) from gasche/inferno-experimental:letprod into master 2020-05-13 11:32:39 +02:00
Gabriel Scherer c527ded72f Infer: make Tuple a n-ary construct 2020-05-13 11:12:24 +02:00
Gabriel Scherer de498f2bce ML: LetProd, with type inference in CPS 2020-05-13 11:12:24 +02:00
Gabriel Scherer dc530b64d4 Infer: use n-ary product structures 2020-05-13 11:12:24 +02:00
Gabriel Scherer a893f86d7a ML: remove Proj, which does not extend to n-ary products
There is no principal way to type (Proj<3> t) without type-based
disambiguation, as we do not know (at constraint-generation time) what
is the arity of the tuple type of t.
2020-05-13 11:12:24 +02:00
Gabriel Scherer b7d5bdf43a LetProd: Fail more gracefully when there is an arity mismatch 2020-05-13 11:12:24 +02:00
Gabriel Scherer 62f62c23cd F: add a LetProd construct 2020-05-13 11:12:22 +02:00
Olivier 7718ec79a0 Merge pull request 'restore the System F tests that were disabled by #4' (#5) from gasche/inferno-experimental:fix-F-tests into master 2020-05-11 15:59:58 +02:00
Gabriel Scherer 4f5d8dbacc [minor] typo in TestF.ml 2020-05-11 15:56:03 +02:00
Gabriel Scherer 455fd161dd restore the System F tests that were disabled by #4 2020-05-11 15:56:03 +02:00
Olivier 835ef283fa Merge pull request 'FPrinter: fix `print_tuple`' (#6) from gasche/inferno-experimental:fix-print-tuple into master 2020-05-11 15:41:15 +02:00
Olivier c25014e2a8 Merge pull request 'fix-nth_type-bound-checking' (#7) from gasche/inferno-experimental:fix-nth_type-bound-checking into master 2020-05-11 15:35:28 +02:00
Gabriel Scherer 021f6eadee even when INFERNO_SLOW_TESTS is not test, do some *quick* random testing
The tests as selected take 0.6s on my machine, and they should help
catch some simple mistakes.
2020-05-08 15:25:30 +02:00
Gabriel Scherer c45c70bbb7 fix bound checking in nth_type
(The mistake was caught by running the random tests with INFERNO_SLOW_TESTS=1.)
2020-05-08 15:25:30 +02:00
Gabriel Scherer dbb9e76ea6 FPrinter: fix print_tuple
The tuple (foo, bar, baz) would get printed as
  (foobarbaz)
as the comma was missing.

We now also use a specific printing for one-tuple (tuples of size 1),
which get printed as
  (foo,)
to distinguish them from (foo) which is not a tuple.
2020-05-08 14:35:45 +02:00
Gabriel Scherer 1ccc3430bc [minor] Fprinter: move the print-term helpers before the recursive block 2020-05-08 14:27:59 +02:00
Gabriel Scherer b4445ceb4a Merge pull request 'new-f-constructs' (#3) from new-f-constructs into master 2020-05-06 16:40:03 +02:00
Olivier Martinot da874d035c Rebase with master 2020-05-05 15:57:41 +02:00
Olivier Martinot d588ba83f1 Rename union to concat, concat_disjoint returns a result 2020-05-05 14:36:05 +02:00
Olivier Martinot a7921a6d2b More readable type variable names in hand written tests 2020-05-05 14:36:05 +02:00
Olivier Martinot bbd478852b Auxiliary function moved in a more appropriate place 2020-05-05 14:36:05 +02:00
Olivier Martinot 0028456e24 Fix error handling in FTypeChecker 2020-05-05 14:36:05 +02:00
Olivier Martinot adac72c705 Print tuple unambiguously 2020-05-05 14:36:05 +02:00
Olivier Martinot 7a2ebdd726 Better error handling : type errors are now all part of the same sum type 2020-05-05 14:36:05 +02:00
Olivier Martinot 29f2903c5c Changes in type annotations of injections (list of tyeps instead of sum type) 2020-05-05 14:36:05 +02:00
Olivier Martinot 42c355464a Simplify spaghetti code 2020-05-05 14:36:05 +02:00
Olivier Martinot aec8a1a721 Fix bug in printer 2020-05-05 14:36:05 +02:00
Olivier Martinot d857bd6a86 Add pattern-matching example 2020-05-05 14:36:05 +02:00
Olivier Martinot 33f8448014 Fix a typo 2020-05-05 14:36:05 +02:00
Olivier Martinot b9b2a5b63a Environment variable must now be set to enable random tests 2020-05-05 14:36:05 +02:00
Olivier Martinot 9f77b1df42 Fix bug in FTypeChecker interface 2020-05-05 14:31:58 +02:00
Olivier Martinot 2a5daa8145 Add type annotation in pattern-matching 2020-05-05 14:31:58 +02:00
Olivier Martinot fa5e4674f1 Improve FTypeChecker (error handling, code factorization) 2020-05-05 14:31:58 +02:00
Olivier Martinot 4f9652e183 Improve FPrinter 2020-05-05 14:31:58 +02:00
Olivier Martinot 68d98d2a78 Use type environment concatenation in F type checker, add test 2020-05-05 14:31:58 +02:00
Olivier Martinot f6b6b61d49 add match construct in system F 2020-05-05 14:23:53 +02:00
Olivier Martinot a512cb60c8 add product and sum type in System F 2020-05-05 14:23:53 +02:00
Olivier 4e4f411590 Merge pull request 'Separate tests further' (#4) from gasche/inferno-experimental:separate-tests-more into master 2020-05-03 20:54:21 +02:00
Gabriel Scherer 819fd28f48 separate tests further into a test/ directory
Naming convention:
- TestFoo: a bunch of tests to execute
- CheckFoo: definitions of interesting properties to check (in tests)
  and helper functions to check them
2020-05-03 16:56:56 +02:00
Gabriel Scherer 666284748b rename client/Client into client/Infer to name the library Client
Otherwise (as reported by Olivier Martinot) dune complains about
conflicting names.
2020-05-03 16:47:51 +02:00
Gabriel Scherer 70d02b454d Merge pull request 'separate tests' (#2) from separate-test into master 2020-05-03 15:02:28 +02:00
Olivier Martinot 27e824b8e4 Cleaner version of two separate test files 2020-05-02 10:53:17 +02:00
Olivier a1cb15c700 Merge pull request 'Nominal2Debruijn.concat : env -> env -> env' (#1) from gasche/inferno-experimental:debruijn-concat into master 2020-04-24 16:25:20 +02:00
Gabriel Scherer dcb6df34b8 Nominal2Debruijn.concat : env -> env -> env
This function will be useful to implement certain typing rules that
concatenate environments together. For example, in certain formulation
of pattern-matching, typing a pattern returns an environment fragment,
to be concatenated onto the current environment.
2020-04-23 17:51:06 +02:00
Olivier Martinot a3840b7662 separate tests 2020-04-09 11:09:50 +02:00
28 changed files with 1809 additions and 725 deletions

View File

@ -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
)

View File

@ -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

View File

@ -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
(* -------------------------------------------------------------------------- *)

View File

@ -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
(* -------------------------------------------------------------------------- *)

View File

@ -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
(* -------------------------------------------------------------------------- *)

View File

@ -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

View File

@ -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))

View File

@ -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

View File

@ -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

714
client/Infer.ml Normal file
View File

@ -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
)

11
client/Infer.mli Normal file
View File

@ -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

View File

@ -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
}

View File

@ -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%!"

View File

@ -1,5 +1,5 @@
(test
(name Main)
(libraries unix pprint inferno)
(library
(name client)
(libraries pprint inferno)
(flags "-w" "@1..66-4-44")
)

68
client/test/CheckML.ml Normal file
View File

@ -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

5
client/test/Config.ml Normal file
View File

@ -0,0 +1,5 @@
let verbose =
true
let very_verbose =
false

40
client/test/Log.ml Normal file
View File

@ -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

101
client/test/TestF.ml Normal file
View File

@ -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

194
client/test/TestML.ml Normal file
View File

@ -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."

130
client/test/TestMLRandom.ml Normal file
View File

@ -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%!"

24
client/test/dune Normal file
View File

@ -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)
)

View File

@ -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

View File

@ -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

View File

@ -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. *)

View File

@ -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 *)
(* ---------------------------------------------------------------------- *)

View File

@ -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)

View File

@ -92,6 +92,7 @@ module Make
* rawco
* rawco
* variable list WriteOnceRef.t
| CFrozen of variable * (variable S.structure -> rawco)
(* ---------------------------------------------------------------------- *)

View File

@ -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]. *)