Compare commits
1 Commits
master
...
rigid-vari
Author | SHA1 | Date |
---|---|---|
Olivier | c2dfd17f68 |
|
@ -1,12 +1,6 @@
|
|||
# Changes
|
||||
|
||||
## 2022/06/03
|
||||
|
||||
* Support for rigid variables, that is, variables that cannot be unified with
|
||||
other rigid variables or with older flexible variables. These variables are
|
||||
introduced by the new combinators `letr1` and `letrn`. The exception
|
||||
`VariableScopeEscape`, which is raised when a rigid variable escapes its
|
||||
scope, is also new.
|
||||
## 2022/02/XX
|
||||
|
||||
* **Incompatible** changes to the solver's high-level API.
|
||||
The module `Inferno.SolverHi` has been renamed to `Inferno.Solver`.
|
||||
|
|
5
Makefile
5
Makefile
|
@ -84,8 +84,7 @@ VERSIONS := \
|
|||
4.10.0 \
|
||||
4.11.1 \
|
||||
4.12.0 \
|
||||
4.13.1 \
|
||||
4.14.0 \
|
||||
4.13.0 \
|
||||
|
||||
.PHONY: versions
|
||||
versions:
|
||||
|
@ -118,7 +117,7 @@ DOC = $(DOCDIR)/inferno/index.html
|
|||
doc:
|
||||
@ rm -rf _build/default/_doc
|
||||
@ dune clean
|
||||
@ dune build @doc 2>&1 | ./doc.sh
|
||||
@ dune build @doc
|
||||
@ echo "You can view the documentation by typing 'make view'".
|
||||
|
||||
.PHONY: view
|
||||
|
|
19
TODO.md
19
TODO.md
|
@ -23,6 +23,15 @@
|
|||
that would require multiple name transformations (i.e., composing multiple
|
||||
environment lookups).
|
||||
|
||||
* Can `let0`, `let1`, and `letn` be simplified or combined? Do we really need
|
||||
a `CLet` form that binds several names at once? Can the treatment of
|
||||
unreachable type variables be simplified?
|
||||
|
||||
* Solving a `CLet` constraint produces a list of pairs `tevar * scheme`,
|
||||
but `letn` keeps only the second component of every pair. If `letn`
|
||||
is the only entry point, then the result type of `CLet` constraints
|
||||
can be simplified.
|
||||
|
||||
* Can we remove the redundancy between `instance` and `instance_? (See next item.)
|
||||
|
||||
* Introduce a combinator `ignore : 'a co -> unit co` that allows the solver to
|
||||
|
@ -33,12 +42,8 @@
|
|||
elaboration. Also, it could remove the need for a primitive `instance_`
|
||||
combinator, as `instance_ x ty` would correspond to `ignore (instance x ty)`.
|
||||
|
||||
* Introduce a `forall` combinator so as to make it easy to express `∀α.c`.
|
||||
|
||||
## Error Handling
|
||||
|
||||
* Attach exploitable information to the exception `VariableScopeEscape`.
|
||||
|
||||
* Introduce more powerful combinators to handle errors in a programmatic
|
||||
way. Change the type `'a co` to `('a, 'b) co`? Introduce a `CCatch`
|
||||
construct to allow recovering after an error? (Think about Merlin,
|
||||
|
@ -60,6 +65,12 @@
|
|||
decoding is performed either during elaboration or after the
|
||||
unifier has encountered an error.
|
||||
|
||||
* Improve the documentation produced by `make doc`.
|
||||
|
||||
* Document the requirement that the function passed to `map` must be pure.
|
||||
Use this hypothesis to remove the useless evaluation of `k1 env` in the
|
||||
definition of `^^`.
|
||||
|
||||
## Test Suite
|
||||
|
||||
* Improve the coverage of the test suite. Add explicit negative test cases.
|
||||
|
|
|
@ -22,8 +22,8 @@ module O = struct
|
|||
let inject n =
|
||||
2 * n
|
||||
|
||||
type 'a structure = 'a S.structure
|
||||
let pprint = S.pprint
|
||||
type 'a structure =
|
||||
'a S.structure
|
||||
|
||||
type ty =
|
||||
F.nominal_type
|
||||
|
@ -381,14 +381,12 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
|
|||
by t, but they can still be instantiated in the rest of the term.
|
||||
*)
|
||||
let x = X.fresh () in
|
||||
let+ (alphas, (betas, _), t', tys) =
|
||||
letr1 (List.length vs) x
|
||||
(fun tys z ->
|
||||
let tyvs = List.combine vs tys in
|
||||
convert_annot typedecl_env tyvs z t ty)
|
||||
let+ (alphas, t', tys) =
|
||||
letr1 vs x
|
||||
(fun tyvs z -> convert_annot typedecl_env tyvs z t ty)
|
||||
(instance x w)
|
||||
in
|
||||
F.ftyapp (coerce alphas betas (F.ftyabs alphas t')) tys
|
||||
F.ftyapp (F.ftyabs alphas t') tys
|
||||
end
|
||||
|
||||
| ML.Tuple (pos, ts) ->
|
||||
|
@ -616,7 +614,6 @@ type nonrec range = range
|
|||
exception Unbound of range * ML.tevar
|
||||
exception Unify = Solver.Unify
|
||||
exception Cycle = Solver.Cycle
|
||||
exception VariableScopeEscape = Solver.VariableScopeEscape
|
||||
|
||||
let hastype (env : ML.datatype_env) (t : ML.term) : F.nominal_term co =
|
||||
let+ (vs, t) =
|
||||
|
|
|
@ -2,7 +2,6 @@ type range = Lexing.position * Lexing.position
|
|||
exception Unbound of range * ML.tevar
|
||||
exception Unify of range * F.nominal_type * F.nominal_type
|
||||
exception Cycle of range * F.nominal_type
|
||||
exception VariableScopeEscape of range
|
||||
|
||||
(* Contraint generation, constraint solving and elaboration, combined. *)
|
||||
val translate: rectypes:bool -> ML.datatype_env -> ML.term -> F.nominal_term
|
||||
|
|
|
@ -62,20 +62,4 @@ rule read =
|
|||
| "..." { DOTS }
|
||||
| "#use" { USE }
|
||||
| eof { EOF }
|
||||
| "(*" { ocamlcomment lexbuf; read lexbuf }
|
||||
| _ as c { failwith (Printf.sprintf "Unexpected character during lexing: %c" c) }
|
||||
|
||||
(* Skip comments. Comments can be nested. Note that we do not recognize
|
||||
string or character literals inside comments. *)
|
||||
|
||||
and ocamlcomment = parse
|
||||
| "*)"
|
||||
{ () }
|
||||
| "(*"
|
||||
{ ocamlcomment lexbuf; ocamlcomment lexbuf }
|
||||
| newline
|
||||
{ next_line lexbuf; ocamlcomment lexbuf }
|
||||
| eof
|
||||
{ failwith "Unterminated OCaml comment." }
|
||||
| _
|
||||
{ ocamlcomment lexbuf }
|
||||
|
|
|
@ -67,10 +67,8 @@ let term :=
|
|||
| ~ = term_abs ; <>
|
||||
|
||||
let term_abs :=
|
||||
| FUN ; xs = list (tevar_) ; "->" ; t = term_abs ;
|
||||
{
|
||||
List.fold_right (fun x t -> Abs ($loc, x, t)) xs t
|
||||
}
|
||||
| FUN ; x = tevar_ ; "->" ; t = term_abs ;
|
||||
{ Abs ($loc, x, t) }
|
||||
|
||||
| (x, t1, t2) = letin(tevar) ; { Let ($loc, x, t1, t2) }
|
||||
|
||||
|
@ -167,7 +165,6 @@ let type_atom :=
|
|||
|
||||
|
||||
let type_annotation :=
|
||||
| ty = typ; { (Flexible, [], ty) }
|
||||
| SOME ; xs = list(tyvar) ; "." ; ty = typ ;
|
||||
{ (Flexible, xs, ty) }
|
||||
| FOR ; xs = list(tyvar) ; "." ; ty = typ ;
|
||||
|
|
|
@ -110,30 +110,6 @@ let print_let_in lhs rhs body =
|
|||
^^ string "in"
|
||||
^^ prefix 0 1 empty body
|
||||
|
||||
let rec flatten_tyabs t =
|
||||
match t with
|
||||
| TyAbs (x, t) ->
|
||||
let (xs, t) = flatten_tyabs t in
|
||||
(x::xs, t)
|
||||
| t ->
|
||||
([], t)
|
||||
|
||||
let rec flatten_abs t =
|
||||
match t with
|
||||
| Abs (p, t) ->
|
||||
let (ps, t) = flatten_abs t in
|
||||
(p::ps, t)
|
||||
| t ->
|
||||
([], t)
|
||||
|
||||
let print_nary_abstraction abs print_arg args rhs =
|
||||
string abs
|
||||
^^ space
|
||||
^^ separate_map space print_arg args
|
||||
^^ space
|
||||
^^ string "->"
|
||||
^//^ rhs
|
||||
|
||||
let print_annot print_elem (rigidity, tyvars, typ) =
|
||||
let rigidity_kwd =
|
||||
string @@ match rigidity with
|
||||
|
@ -156,17 +132,21 @@ let rec print_term t =
|
|||
|
||||
and print_term_abs t =
|
||||
group @@ match t with
|
||||
| TyAbs _ ->
|
||||
let (xs, t) = flatten_tyabs t in
|
||||
print_nary_abstraction "FUN" print_tyvar xs (print_term_abs t)
|
||||
| TyAbs (x, t1) ->
|
||||
string "FUN" ^^ space
|
||||
^^ print_tyvar x ^^ space
|
||||
^^ string "->"
|
||||
^//^ print_term_abs t1
|
||||
| Let (p, t1, t2) ->
|
||||
print_let_in
|
||||
(print_pattern p)
|
||||
(print_term t1)
|
||||
(print_term_abs t2)
|
||||
| Abs _ ->
|
||||
let (ps, t) = flatten_abs t in
|
||||
print_nary_abstraction "fun" print_pattern ps (print_term_abs t)
|
||||
| Abs (p, t) ->
|
||||
string "fun" ^^ space
|
||||
^^ print_pattern p ^^ space
|
||||
^^ string "->"
|
||||
^//^ print_term_abs t
|
||||
| t ->
|
||||
print_term_app t
|
||||
|
||||
|
|
|
@ -37,13 +37,6 @@ let translate ~verbose ~rectypes e t =
|
|||
Printf.fprintf stdout "%!";
|
||||
end;
|
||||
None
|
||||
| Infer.VariableScopeEscape range ->
|
||||
if verbose then begin
|
||||
Printf.fprintf stdout
|
||||
"%sA rigid variable escapes its scope.\n%!"
|
||||
(LexUtil.range range);
|
||||
end;
|
||||
None
|
||||
|
||||
let equal_term t1 t2 =
|
||||
ML.compare_term t1 t2 = 0
|
||||
|
@ -128,7 +121,7 @@ let test_with_args
|
|||
(LexUtil.range range);
|
||||
false
|
||||
| t' ->
|
||||
assert (equal_term t t');
|
||||
assert (equal_term t t');
|
||||
(* now we check typability; inference should not fail *)
|
||||
let outcome_env =
|
||||
ML2F.translate_env env in
|
||||
|
|
|
@ -1,2 +0,0 @@
|
|||
type nat = | Zero | Succ of nat
|
||||
let f = (fun x -> x : nat -> nat)
|
|
@ -1,2 +0,0 @@
|
|||
let g = fun f ->
|
||||
(f : for 'a. 'a -> 'a)
|
|
@ -1,4 +0,0 @@
|
|||
(* We have a redundant quantifier here: 'b is not used in the type
|
||||
annotation. *)
|
||||
let _ =
|
||||
(fun x -> x : for 'a 'b. 'a -> 'a) ()
|
|
@ -1,4 +0,0 @@
|
|||
(* We have unreachable generalizable variables inside the left-hand
|
||||
side of a [letr] combinator. *)
|
||||
let _ =
|
||||
((fun x -> fun y -> y) (fun x -> x) : for 'a. 'a -> 'a) ()
|
|
@ -103,8 +103,9 @@ Option type
|
|||
Type inference and translation to System F...
|
||||
Formatting the System F term...
|
||||
Pretty-printing the System F term...
|
||||
FUN a0 a1 ->
|
||||
Some<option {a1 -> a1*a0 -> a0}> (fun (x : a1) -> x, fun (x : a0) -> x)
|
||||
FUN a0 ->
|
||||
FUN a1 ->
|
||||
Some<option {a1 -> a1*a0 -> a0}> (fun (x : a1) -> x, fun (x : a0) -> x)
|
||||
Converting the System F term to de Bruijn style...
|
||||
Type-checking the System F term...
|
||||
|
||||
|
@ -178,20 +179,6 @@ List type
|
|||
Converting the System F term to de Bruijn style...
|
||||
Type-checking the System F term...
|
||||
|
||||
Annotations
|
||||
|
||||
$ cat nat-annot.midml
|
||||
type nat = | Zero | Succ of nat
|
||||
let f = (fun x -> x : nat -> nat)
|
||||
|
||||
$ midml nat-annot.midml
|
||||
Type inference and translation to System F...
|
||||
Formatting the System F term...
|
||||
Pretty-printing the System F term...
|
||||
(fun (x : nat ) -> x : nat -> nat )
|
||||
Converting the System F term to de Bruijn style...
|
||||
Type-checking the System F term...
|
||||
|
||||
Pattern-matching
|
||||
|
||||
$ cat match-tuple.midml
|
||||
|
@ -222,11 +209,12 @@ Pattern-matching
|
|||
Type inference and translation to System F...
|
||||
Formatting the System F term...
|
||||
Pretty-printing the System F term...
|
||||
FUN a0 a1 ->
|
||||
match<option a0> Some<option (a1 -> a1)> (fun (x : a1) -> x) with
|
||||
| None<option (a1 -> a1)> () -> None<option a0> ()
|
||||
| (Some<option (a1 -> a1)> _ : option (a1 -> a1)) -> None<option a0> ()
|
||||
end
|
||||
FUN a0 ->
|
||||
FUN a1 ->
|
||||
match<option a0> Some<option (a1 -> a1)> (fun (x : a1) -> x) with
|
||||
| None<option (a1 -> a1)> () -> None<option a0> ()
|
||||
| (Some<option (a1 -> a1)> _ : option (a1 -> a1)) -> None<option a0> ()
|
||||
end
|
||||
Converting the System F term to de Bruijn style...
|
||||
Type-checking the System F term...
|
||||
|
||||
|
@ -296,46 +284,6 @@ Here we see that the variable 'a is rigid inside the annotated term
|
|||
(translated to a System F type abstraction), but can be used at any
|
||||
instantiation type from the outside -- here the unit type {}.
|
||||
|
||||
This example is correct as well.
|
||||
It involves a useless universal quantifier.
|
||||
|
||||
$ cat rigid-redundant.midml
|
||||
(* We have a redundant quantifier here: 'b is not used in the type
|
||||
annotation. *)
|
||||
let _ =
|
||||
(fun x -> x : for 'a 'b. 'a -> 'a) ()
|
||||
|
||||
$ midml rigid-redundant.midml
|
||||
Type inference and translation to System F...
|
||||
Formatting the System F term...
|
||||
Pretty-printing the System F term...
|
||||
(FUN a1 a2 -> (fun (x : a2) -> x : a2 -> a2)) [[a0] a0] [{}] ()
|
||||
Converting the System F term to de Bruijn style...
|
||||
Type-checking the System F term...
|
||||
|
||||
This example is also correct.
|
||||
It involves unreachable generalizable type variables,
|
||||
that is, type variables that are both unconstrained
|
||||
and unreachable from the entry point of a type scheme.
|
||||
|
||||
$ cat rigid-unreachable.midml
|
||||
(* We have unreachable generalizable variables inside the left-hand
|
||||
side of a [letr] combinator. *)
|
||||
let _ =
|
||||
((fun x -> fun y -> y) (fun x -> x) : for 'a. 'a -> 'a) ()
|
||||
|
||||
$ midml rigid-unreachable.midml
|
||||
Type inference and translation to System F...
|
||||
Formatting the System F term...
|
||||
Pretty-printing the System F term...
|
||||
(FUN a1 a2 ->
|
||||
((fun (x : a1 -> a1) (y : a2) -> y) (fun (x : a1) -> x) : a2 -> a2))
|
||||
[[a0] a0]
|
||||
[{}]
|
||||
()
|
||||
Converting the System F term to de Bruijn style...
|
||||
Type-checking the System F term...
|
||||
|
||||
The example below is incorrect, it tries to unify two distinct rigid
|
||||
variables.
|
||||
|
||||
|
@ -378,24 +326,8 @@ its binding scope.
|
|||
$ midml rigid-level-escape-wrong.midml
|
||||
Type inference and translation to System F...
|
||||
File "test", line 2, characters 12-13:
|
||||
A rigid variable escapes its scope.
|
||||
|
||||
|
||||
The example below is incorrect, a rigid variable tries to escape
|
||||
its binding scope. The escape is only noticed at generalization
|
||||
time when adjusting levels.
|
||||
|
||||
$ cat rigid-level-escape-later-wrong.midml
|
||||
let g = fun f ->
|
||||
(f : for 'a. 'a -> 'a)
|
||||
|
||||
In the example above,* the type of f is "old" relative to the
|
||||
rigid-introducing annotation, but we don't notice during the
|
||||
unification itself which only touches the arrow type ->, not the rigid
|
||||
variable 'a. The escape will be noticed at generalization time, when
|
||||
adjusting the level of the type nodes below the arrow.
|
||||
|
||||
$ midml rigid-level-escape-later-wrong.midml
|
||||
Type inference and translation to System F...
|
||||
File "test", line 2, characters 2-24:
|
||||
A rigid variable escapes its scope.
|
||||
Type error: type mismatch.
|
||||
Type error: mismatch between the type:
|
||||
r2
|
||||
and the type:
|
||||
r8
|
||||
|
|
66
doc.sh
66
doc.sh
|
@ -1,66 +0,0 @@
|
|||
#!/bin/bash
|
||||
set -euo pipefail
|
||||
shopt -s extglob
|
||||
|
||||
# This script helps make sense of the error messages produced by odoc.
|
||||
|
||||
# A list of missing modules.
|
||||
missing=""
|
||||
|
||||
while read line
|
||||
do
|
||||
buffer="$line"
|
||||
case "$line" in
|
||||
File*client*:)
|
||||
# A warning about the directory client/. Stop.
|
||||
echo "Skipping all warnings about client/."
|
||||
break
|
||||
;;
|
||||
File*:)
|
||||
read line
|
||||
buffer="$buffer$line"
|
||||
case "$line" in
|
||||
|
||||
"Warning: Couldn't find the following modules:")
|
||||
read line
|
||||
# A warning that some modules could not be found.
|
||||
# Accumulate the names of the missing modules.
|
||||
missing="$missing $line"
|
||||
;;
|
||||
|
||||
"Warning: Failed to lookup type unresolvedroot(Stdlib)"*)
|
||||
# A warning about Stdlib. Skip.
|
||||
echo "Skipping warnings about Stdlib."
|
||||
;;
|
||||
|
||||
"Warning: While"*)
|
||||
read line
|
||||
buffer="$buffer$line"
|
||||
case "$line" in
|
||||
"Failed to lookup type unresolvedroot(Stdlib)"*)
|
||||
# A multi-line warning about Stdlib. Skip.
|
||||
echo "Skipping warnings about Stdlib."
|
||||
;;
|
||||
*)
|
||||
# Another kind of warning. Echo.
|
||||
echo "$buffer"
|
||||
;;
|
||||
esac
|
||||
;;
|
||||
|
||||
*)
|
||||
# Another kind of warning. Echo.
|
||||
echo "$buffer"
|
||||
;;
|
||||
esac
|
||||
;;
|
||||
|
||||
*)
|
||||
echo "$buffer"
|
||||
;;
|
||||
esac
|
||||
done
|
||||
|
||||
# Show the missing modules.
|
||||
echo "Missing modules:"
|
||||
echo "$missing" | sed -e 's/^ *//' | tr " " "\n" | sort | uniq
|
|
@ -12,7 +12,7 @@
|
|||
open Signatures
|
||||
|
||||
module Make
|
||||
(S : DSTRUCTURE)
|
||||
(S : OSTRUCTURE)
|
||||
(U : MUNIFIER with type 'a structure := 'a S.structure)
|
||||
(O : OUTPUT with type 'a structure := 'a S.structure)
|
||||
= struct
|
||||
|
@ -20,6 +20,28 @@ open U
|
|||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Decoding a variable. *)
|
||||
|
||||
(* The public function [decode_variable] decodes a variable, which must have
|
||||
leaf structure. The decoded variable is determined by the unique identity
|
||||
of the variable [v]. *)
|
||||
|
||||
let decode_variable (v : variable) : O.tyvar =
|
||||
let data = U.get v in
|
||||
assert (S.is_leaf data);
|
||||
O.inject (S.id data)
|
||||
|
||||
(* The internal function [decode_id] decodes a variable. As above, this
|
||||
variable must have leaf structure, and the decoded variable is determined
|
||||
by the unique identity [id], which is already at hand. *)
|
||||
|
||||
(* [O.variable] is used to convert the result from [O.tyvar] to [O.ty]. *)
|
||||
|
||||
let decode_id (id : id) : O.ty =
|
||||
O.variable (O.inject id)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* An acyclic decoder performs a bottom-up computation over an acyclic graph. *)
|
||||
|
||||
let new_acyclic_decoder () : variable -> O.ty =
|
||||
|
@ -35,9 +57,14 @@ let new_acyclic_decoder () : variable -> O.ty =
|
|||
try
|
||||
Hashtbl.find visited id
|
||||
with Not_found ->
|
||||
let a = O.structure (S.map decode data) in
|
||||
(* Because the graph is assumed to be acyclic, it is ok to update
|
||||
the hash table only after the recursive call. *)
|
||||
let a =
|
||||
if S.is_leaf data then
|
||||
decode_id id
|
||||
else
|
||||
O.structure (S.map decode data)
|
||||
in
|
||||
Hashtbl.add visited id a;
|
||||
a
|
||||
|
||||
|
@ -174,33 +201,36 @@ let new_cyclic_decoder () : variable -> O.ty =
|
|||
with Not_found ->
|
||||
(* Otherwise, compute a decoded value [a] for this vertex. *)
|
||||
let a =
|
||||
if Hashtbl.mem table id then begin
|
||||
(* We have just rediscovered this vertex via a back edge. Its
|
||||
status may be [Active] or [Rediscovered]. We change it to
|
||||
[Rediscovered], and stop the traversal. *)
|
||||
Hashtbl.replace table id Rediscovered;
|
||||
(* Decode this vertex as a (μ-bound) variable, identified by
|
||||
its unique identity [id]. *)
|
||||
O.variable (O.inject id)
|
||||
end
|
||||
else begin
|
||||
(* This vertex is not being visited. Before the recursive
|
||||
call, mark it as being visited. *)
|
||||
Hashtbl.add table id Active;
|
||||
(* Perform the recursive traversal. *)
|
||||
let a = O.structure (S.map decode data) in
|
||||
(* Mark this vertex as no longer being visited. If it was
|
||||
recursively rediscovered during the recursive call,
|
||||
introduce a μ binder. (It would be correct but noisy to
|
||||
always introduce a μ binder.) *)
|
||||
let status =
|
||||
try Hashtbl.find table id with Not_found -> assert false
|
||||
in
|
||||
Hashtbl.remove table id;
|
||||
match status with
|
||||
| Active -> a
|
||||
| Rediscovered -> O.mu (O.inject id) a
|
||||
end
|
||||
if S.is_leaf data then
|
||||
(* There is no structure. *)
|
||||
decode_id id
|
||||
else
|
||||
(* There is some structure. *)
|
||||
if Hashtbl.mem table id then begin
|
||||
(* We have just rediscovered this vertex via a back edge. Its
|
||||
status may be [Active] or [Rediscovered]. We change it to
|
||||
[Rediscovered], and stop the traversal. *)
|
||||
Hashtbl.replace table id Rediscovered;
|
||||
decode_id id
|
||||
end
|
||||
else begin
|
||||
(* This vertex is not being visited. Before the recursive
|
||||
call, mark it as being visited. *)
|
||||
Hashtbl.add table id Active;
|
||||
(* Perform the recursive traversal. *)
|
||||
let a = O.structure (S.map decode data) in
|
||||
(* Mark this vertex as no longer being visited. If it was
|
||||
recursively rediscovered during the recursive call,
|
||||
introduce a μ binder. (It would be correct but noisy to
|
||||
always introduce a μ binder.) *)
|
||||
let status =
|
||||
try Hashtbl.find table id with Not_found -> assert false
|
||||
in
|
||||
Hashtbl.remove table id;
|
||||
match status with
|
||||
| Active -> a
|
||||
| Rediscovered -> O.mu (O.inject id) a
|
||||
end
|
||||
in
|
||||
(* If this vertex is isolated, store the decoded value [a] in the
|
||||
memoization table [visited]. (It would be correct to never
|
||||
|
|
|
@ -11,29 +11,22 @@
|
|||
|
||||
open Signatures
|
||||
|
||||
(**This module performs decoding, which is the task of traversing the data
|
||||
structure maintained by the unifier and transforming it into a data
|
||||
(**This module offers performs decoding, which is the task of traversing the
|
||||
data structure maintained by the unifier and transforming it into a data
|
||||
representation selected by the user (typically, some form of tree). It is
|
||||
parameterized by the term structure [S], by the unifier [U], and by the
|
||||
data representation [O]. Read-only access to the unifier's data structure
|
||||
suffices.
|
||||
|
||||
Two decoding algorithms are proposed: the {i acyclic decoder} does not
|
||||
tolerate cycles, and produces ordinary trees; whereas the {i cyclic
|
||||
decoder} can deal with cycles, and produces trees that contain μ
|
||||
binders.
|
||||
|
||||
The cyclic decoder can produce μ binders and μ-bound type variables.
|
||||
Neither decoder has specific support for printing ordinary (∀-bound)
|
||||
type variables. In the eyes of the decoders, a type variable is just
|
||||
a vertex that has no structure; it is up to the user-supplied function
|
||||
[O.structure] to determine how such a vertex must be printed. *)
|
||||
suffices. Two decoding algorithms are proposed: the {i acyclic decoder}
|
||||
does not tolerate cycles, and produces ordinary trees; whereas the {i
|
||||
cyclic decoder} can deal with cycles, and produces trees that contain μ
|
||||
binders. *)
|
||||
module Make
|
||||
(S : sig (** @inline *) include DSTRUCTURE end)
|
||||
(S : sig (** @inline *) include OSTRUCTURE end)
|
||||
(U : sig (** @inline *) include MUNIFIER
|
||||
with type 'a structure := 'a S.structure end)
|
||||
(O : sig (** @inline *) include OUTPUT
|
||||
with type 'a structure := 'a S.structure end)
|
||||
: sig (** @inline *) include DECODER
|
||||
with type variable := U.variable
|
||||
and type tyvar := O.tyvar
|
||||
and type ty := O.ty end
|
||||
|
|
|
@ -11,7 +11,7 @@
|
|||
|
||||
open Signatures
|
||||
|
||||
module Make (S : GSTRUCTURE_OPT) = struct
|
||||
module Make (S : STRUCTURE_LEAF) = struct
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -53,6 +53,10 @@ let base_rank =
|
|||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Rigid variables have a fixed rank -- lowering their rank is an error --
|
||||
and a fixed leaf structure -- unifying them with a non-leaf structure
|
||||
is an error. *)
|
||||
|
||||
(* We want to be able to mark an equivalence class as either "active" or
|
||||
"generic". The unifier works with active variables only; it never sees a
|
||||
generic variable. Generic variables are used as part of the representation
|
||||
|
@ -67,16 +71,25 @@ let base_rank =
|
|||
(* An active variable is intended to become generic some day. A generic
|
||||
variable never becomes active again. *)
|
||||
|
||||
(* An active variable is either flexible or generic. *)
|
||||
type status = Rigid | Flexible | Generic
|
||||
|
||||
(* A rigid variable has a fixed rank -- lowering its rank is an error --
|
||||
and a fixed leaf structure -- unifying it with a non-leaf structure
|
||||
is an error. *)
|
||||
type rigidity = Rigid_ | Flexible_
|
||||
|
||||
type status =
|
||||
| Rigid
|
||||
| Flexible
|
||||
| Generic
|
||||
let rigidity_of_status status =
|
||||
match status with
|
||||
| Generic ->
|
||||
assert false
|
||||
| Flexible ->
|
||||
Flexible_
|
||||
| Rigid ->
|
||||
Rigid_
|
||||
|
||||
let status_of_rigidity rigidity =
|
||||
match rigidity with
|
||||
| Flexible_ ->
|
||||
Flexible
|
||||
| Rigid_ ->
|
||||
Rigid
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -126,43 +139,19 @@ type 'a data = {
|
|||
mutable mark: mark;
|
||||
}
|
||||
|
||||
(* A printer (for debugging purposes). *)
|
||||
|
||||
let pprint elem data =
|
||||
let open PPrint in
|
||||
utf8format "@%d[%d]" data.id data.rank ^^
|
||||
S.pprint elem data.structure
|
||||
(* [status] and [mark] are currently not printed. *)
|
||||
|
||||
(* This exception is raised when a rigid variable escapes its scope, that is,
|
||||
when it is unified with (or becomes a child of) a variable of lesser rank.
|
||||
At present, this exception does not carry any data; we do not yet know how
|
||||
to produce a good error message in this situation. *)
|
||||
|
||||
exception VariableScopeEscape
|
||||
|
||||
(* If [data.status] is flexible, then [adjust_rank data k] is equivalent
|
||||
to [data.rank <- min k data.rank]. If [data.status] is rigid, then it
|
||||
causes an error. Indeed, the rank of a rigid variable is fixed; it can
|
||||
never decrease. *)
|
||||
(* [adjust_rank data k] is equivalent to [data.rank <- min k data.rank]. *)
|
||||
|
||||
let adjust_rank (data : 'a data) (k : rank) =
|
||||
assert (data.status <> Generic);
|
||||
if k < data.rank then
|
||||
if data.status = Flexible then
|
||||
data.rank <- k
|
||||
else
|
||||
raise VariableScopeEscape
|
||||
if k < data.rank then data.rank <- k
|
||||
|
||||
(* The module [Data] is meant to be an argument for [Unifier.Make]. *)
|
||||
(* The module [Data] satisfies the signature [USTRUCTURE] required by the
|
||||
functor [Unifier.Make]. *)
|
||||
|
||||
module Data = struct
|
||||
|
||||
type 'a structure =
|
||||
'a data
|
||||
|
||||
let pprint = pprint
|
||||
|
||||
let id data =
|
||||
data.id
|
||||
|
||||
|
@ -207,33 +196,34 @@ module Data = struct
|
|||
let structure = S.conjunction equate data1.structure data2.structure in
|
||||
(* The new rank is the minimum of the two ranks. *)
|
||||
let rank = min data1.rank data2.rank in
|
||||
(* If either variable is rigid, the conjunction is also rigid. However,
|
||||
unification in the presence of rigid variables is subject to certain
|
||||
restrictions. *)
|
||||
let status : status =
|
||||
match data1.status, data1.rank, data2.status, data2.rank with
|
||||
| Generic, _, _, _
|
||||
| _, _, Generic, _ ->
|
||||
assert false
|
||||
| Flexible, _, Flexible, _ ->
|
||||
Flexible
|
||||
| Rigid, _, Rigid, _ ->
|
||||
(* One cannot unify two rigid variables. *)
|
||||
raise InconsistentConjunction
|
||||
| Rigid, rigid_rank, Flexible, _
|
||||
| Flexible, _, Rigid, rigid_rank ->
|
||||
(* One cannot lower the rank of a rigid variable. *)
|
||||
if rank < rigid_rank then raise VariableScopeEscape;
|
||||
(* One cannot assign some structure to a rigid variable. *)
|
||||
if Option.is_some structure then raise InconsistentConjunction;
|
||||
Rigid
|
||||
let fail () = raise InconsistentConjunction in
|
||||
(* If either variables is rigid, the conjunction is also rigid. *)
|
||||
let status =
|
||||
match rigidity_of_status data1.status,
|
||||
rigidity_of_status data2.status with
|
||||
| Flexible_, Flexible_ ->
|
||||
Flexible
|
||||
(* One cannot unify two rigid variables, *)
|
||||
| Rigid_, Rigid_ ->
|
||||
fail ()
|
||||
(* ... or lower the rank of a rigid variable, *)
|
||||
| Rigid_, Flexible_ ->
|
||||
if (rank < data1.rank) then fail ();
|
||||
(* ... or give it a non-leaf structure. *)
|
||||
if not (S.is_leaf structure) then fail ();
|
||||
Rigid
|
||||
| Flexible_, Rigid_ ->
|
||||
if (rank < data2.rank) then fail ();
|
||||
(* ... or give it a non-leaf structure. *)
|
||||
if not (S.is_leaf structure) then fail ();
|
||||
Rigid
|
||||
in
|
||||
(* There is no need to preserve marks during unification. *)
|
||||
let mark = dummy in
|
||||
{ id; structure; rank; status; mark }
|
||||
|
||||
let is_leaf data =
|
||||
Option.is_none data.structure
|
||||
S.is_leaf data.structure
|
||||
|
||||
let project data =
|
||||
data.structure
|
||||
|
@ -331,17 +321,11 @@ let register v r =
|
|||
(* When a fresh unification variable is created, it receives the current rank,
|
||||
and it is immediately registered at this rank. *)
|
||||
|
||||
let flexible structure =
|
||||
let fresh rigidity structure =
|
||||
let r = state.young in
|
||||
let status = Flexible in
|
||||
let v = U.fresh (Data.make structure r status) in
|
||||
register v r;
|
||||
v
|
||||
|
||||
let rigid () =
|
||||
let r = state.young in
|
||||
let status = Rigid in
|
||||
let v = U.fresh (Data.make None r status) in
|
||||
if rigidity = Rigid_ then
|
||||
assert (S.is_leaf structure);
|
||||
let v = U.fresh (Data.make structure r (status_of_rigidity rigidity)) in
|
||||
register v r;
|
||||
v
|
||||
|
||||
|
@ -469,7 +453,7 @@ let discover_young_generation () =
|
|||
discovering a variable [v] cannot improve the value of [k] that we are
|
||||
pushing down).
|
||||
|
||||
In the presence of cycles, the upward propagation phase is incomplete, in the
|
||||
In the presence of cycles, the upward propation phase is incomplete, in the
|
||||
sense that it may compute ranks that are higher than necessary. For
|
||||
instance, imagine a cycle at rank 2, such that every leaf that is reachable
|
||||
from this cycle is at rank 1. Then, in principle, this cycle can be demoted
|
||||
|
@ -692,7 +676,7 @@ let schemify (root : variable) : scheme =
|
|||
let exit ~rectypes roots =
|
||||
|
||||
(* Because calls to [enter] and [exit] must be balanced, we must have: *)
|
||||
assert (state.young >= base_rank);
|
||||
assert (state.young >= 0);
|
||||
|
||||
(* Discover the young variables. *)
|
||||
let generation = discover_young_generation() in
|
||||
|
@ -743,15 +727,15 @@ let exit ~rectypes roots =
|
|||
|
||||
let instantiate { generics; quantifiers; root } =
|
||||
|
||||
(* Create a flexible copy [v'] of every generic variable [v]. At this point,
|
||||
the variable [v'] carries no structure. Record the correspondence between
|
||||
(* Create a flexible copy [v'] of every generic variable [v]. At this point, the
|
||||
variable [v'] carries no structure. Record the correspondence between
|
||||
[v] and [v'] in the mapping. *)
|
||||
let mapping : variable array =
|
||||
generics |> Array.mapi (fun i v ->
|
||||
let data = get v in
|
||||
assert (data.status = Generic);
|
||||
data.mark <- i;
|
||||
flexible None
|
||||
fresh Flexible_ S.leaf
|
||||
)
|
||||
in
|
||||
|
||||
|
|
|
@ -22,7 +22,7 @@ open Signatures
|
|||
operations that allow constructing, inspecting, and instantiating
|
||||
schemes. *)
|
||||
module Make
|
||||
(S : sig (** @inline *) include GSTRUCTURE_OPT end)
|
||||
(S : sig (** @inline *) include STRUCTURE_LEAF end)
|
||||
: sig
|
||||
|
||||
(** {2 Unification} *)
|
||||
|
@ -31,7 +31,7 @@ module Make
|
|||
module Data : sig
|
||||
|
||||
(** @inline *)
|
||||
include DSTRUCTURE
|
||||
include OSTRUCTURE
|
||||
|
||||
(**The type ['a structure] is richer (carries more information) than the
|
||||
type ['a S.structure]. The function [project] witnesses this fact. It
|
||||
|
@ -52,6 +52,31 @@ module Make
|
|||
type variable =
|
||||
U.variable
|
||||
|
||||
(* Existentially-bound variables can "move" in the constraint: some
|
||||
constraint-solving steps have the effect of hoisting their
|
||||
existential quantifier out, to scope over a larger part of the
|
||||
constraint -- this corresponds to lowering the rank of the
|
||||
variable. They can also be unified with some structure. *)
|
||||
|
||||
(* We also support "rigidly-bound" variables that are not allowed to
|
||||
move to a different binding place, or to unify with anything else
|
||||
than themselves. This models language features with abstract
|
||||
variables/types that cannot escape their scope, such as local
|
||||
abstract types or existential unpacking. *)
|
||||
|
||||
type status = Rigid | Flexible | Generic
|
||||
|
||||
type rigidity = Rigid_ | Flexible_
|
||||
|
||||
(* The literature defines a type scheme as a type (the ``body''), placed in
|
||||
the scope of a list of universal quantifiers. Here, the quantifiers are
|
||||
just variables (which definitely carry no structure), while the body is
|
||||
just a variable too (which possibly/probably carries some structure).
|
||||
One may think of a type scheme as a fragment of the unification graph,
|
||||
part of which is marked ``generic'' and is meant to be copied when the
|
||||
type scheme is instantiated, part of which is not (the free variables, so
|
||||
to speak). *)
|
||||
|
||||
(** {2 Schemes} *)
|
||||
|
||||
(**A {i scheme} is usually described in the literature under the form [∀V.T],
|
||||
|
@ -87,8 +112,7 @@ module Make
|
|||
|
||||
(**This module maintains a mutable internal state, which is created and
|
||||
initialized when {!Make} is applied. This state is updated by the
|
||||
functions that follow: {!flexible}, {!rigid}, {!enter}, {!exit},
|
||||
{!instantiate}.
|
||||
functions that follow: {!fresh}, {!enter}, {!exit}, {!instantiate}.
|
||||
|
||||
This internal state keeps track of a {i constraint context}, which can be
|
||||
thought of as a stack of {i frames}. The function {!enter} pushes a new
|
||||
|
@ -104,33 +128,12 @@ module Make
|
|||
are merged, the merged variable is thereafter considered bound at the
|
||||
most ancient of these stack frames. *)
|
||||
|
||||
(**[flexible s] creates a fresh unifier variable with structure [s]. This
|
||||
variable is flexible: this means that it can be unified with other
|
||||
variables without restrictions. This variable is initially bound at the
|
||||
most recent stack frame. If is unified with more ancient variables, then
|
||||
its binding site is implicitly hoisted up.
|
||||
|
||||
Invoking {!flexible} is permitted only if the stack is currently
|
||||
nonempty, that is, if the current balance of calls to {!enter} versus
|
||||
calls to {!exit} is at least one. *)
|
||||
val flexible: variable S.structure -> variable
|
||||
|
||||
(**[rigid()] creates a fresh unifier variable [v] with structure [S.leaf].
|
||||
This variable is rigid: this means that it can be unified with a flexible
|
||||
variable that is as recent as [v] or more recent than [v], and with
|
||||
nothing else. It cannot be unified with a more ancient flexible variable,
|
||||
with another rigid variable, or with a variable that carries nonleaf
|
||||
structure. This variable is bound at the most recent stack frame, and its
|
||||
binding site is never hoisted up.
|
||||
|
||||
By convention, at each stack frame, the rigid variables are bound in
|
||||
front of the flexible variables. Thus, a call to {!flexible} and a call
|
||||
to {!rigid} commute.
|
||||
|
||||
Invoking {!rigid} is permitted only if the stack is currently nonempty,
|
||||
that is, if the current balance of calls to {!enter} versus calls to
|
||||
{!exit} is at least one. *)
|
||||
val rigid: unit -> variable
|
||||
(**[fresh ~rigidity s] creates a fresh unifier variable with structure [s].
|
||||
This variable is initially bound at the most recent stack frame. Invoking
|
||||
{!fresh} is permitted only if the stack is currently nonempty, that is,
|
||||
if the current balance of calls to {!enter} versus calls to {!exit} is at
|
||||
least one. *)
|
||||
val fresh: rigidity -> variable S.structure -> variable
|
||||
|
||||
(**[enter()] updates the current state by pushing a new frame onto the
|
||||
current constraint context. It is invoked when the left-hand side of a
|
||||
|
@ -140,27 +143,23 @@ module Make
|
|||
(**This exception is raised by {!exit}. *)
|
||||
exception Cycle of variable
|
||||
|
||||
(**This exception is raised by {!exit}. *)
|
||||
exception VariableScopeEscape
|
||||
|
||||
(**[exit ~rectypes roots] updates the current state by popping a frame off
|
||||
the current constraint context. It is invoked when the left-hand side of
|
||||
a [CLet] constraint is exited.
|
||||
|
||||
[exit] examines the {i young} fragment of the unification graph, that is,
|
||||
[exit] examines the "young" fragment of the unification graph, that is,
|
||||
the part of the unification graph that has been created or affected since
|
||||
the most recent call to [enter]. The following actions are taken.
|
||||
|
||||
First, if [rectypes] is [false], then an occurs check is performed: that
|
||||
is, if there is a cycle in the young fragment, then an exception of the
|
||||
is, if there is a cycle in the "young" fragment, then an exception of the
|
||||
form [Cycle v] is raised, where the vertex [v] participates in the cycle.
|
||||
|
||||
Second, every young unification variable is inspected so as to
|
||||
Second, every "young" unification variable is inspected so as to
|
||||
determine whether its logical binding site can be hoisted up to a
|
||||
strictly older frame or must remain part of the most recent frame. In the
|
||||
latter case, the variable is {i generalizable}. A list [vs] of the
|
||||
generalizable variables is constructed. If a rigid variable is found
|
||||
to be non-generalizable, then [VariableScopeEscape] is raised.
|
||||
generalizable variables is constructed.
|
||||
|
||||
Third, for each variable [root] provided by the user in the list [roots],
|
||||
a scheme is constructed. The body of this scheme is the variable [root].
|
||||
|
@ -177,10 +176,10 @@ module Make
|
|||
val exit: rectypes:bool -> variable list -> variable list * scheme list
|
||||
|
||||
(**[instantiate sigma] creates a fresh instance of the scheme [sigma]. The
|
||||
generic variables of the type scheme are replaced with fresh flexible
|
||||
variables, obtained by invoking {!flexible}. The images of the scheme's
|
||||
quantifiers and body through this copy are returned. The order of the
|
||||
scheme's quantifiers, as determined by the function {!quantifiers}, is
|
||||
generic variables of the type scheme are replaced with fresh variables,
|
||||
obtained by invoking {!fresh}. The images of the scheme's quantifiers
|
||||
and body through this copy are returned. The order of the scheme's
|
||||
quantifiers, as determined by the function {!quantifiers}, is
|
||||
preserved. *)
|
||||
val instantiate: scheme -> variable list * variable
|
||||
|
||||
|
|
|
@ -12,7 +12,7 @@
|
|||
open Signatures
|
||||
|
||||
module Make
|
||||
(S : OSTRUCTURE)
|
||||
(S : OCSTRUCTURE)
|
||||
(U : MUNIFIER with type 'a structure = 'a S.structure)
|
||||
= struct
|
||||
|
||||
|
|
|
@ -16,7 +16,7 @@ open Signatures
|
|||
parameterized by the term structure [S] and by the unifier [U]. Read-only
|
||||
access to the unifier's data structure suffices. *)
|
||||
module Make
|
||||
(S : sig (** @inline *) include OSTRUCTURE end)
|
||||
(S : sig (** @inline *) include OCSTRUCTURE end)
|
||||
(U : sig (** @inline *) include MUNIFIER
|
||||
with type 'a structure = 'a S.structure end)
|
||||
: sig (** @inline *) include OCCURS_CHECK
|
||||
|
|
|
@ -28,9 +28,9 @@ type id = int
|
|||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* [STRUCTURE] describes just the type ['a structure]. *)
|
||||
(* [SSTRUCTURE] describes just the type ['a structure]. *)
|
||||
|
||||
module type STRUCTURE = sig
|
||||
module type SSTRUCTURE = sig
|
||||
|
||||
(**A structure is a piece of information that the unifier attaches to a
|
||||
variable (or, more accurately, to an equivalence class of variables).
|
||||
|
@ -53,23 +53,14 @@ module type STRUCTURE = sig
|
|||
which indicates the presence of an equality constraint. *)
|
||||
type 'a structure
|
||||
|
||||
(**[pprint] is a structure printer, parameterized over a child printer.
|
||||
It is used for debugging purposes only. *)
|
||||
val pprint: ('a -> PPrint.document) -> 'a structure -> PPrint.document
|
||||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
(* [USTRUCTURE] describes an input of [Unifier.Make]. *)
|
||||
|
||||
(* The following signatures enrich [STRUCTURE] with additional operations. *)
|
||||
|
||||
(* [CONJUNCTIBLE] describes structures with a [conjunction] operation,
|
||||
as required by [Unifier.Make]. *)
|
||||
|
||||
module type CONJUNCTIBLE = sig
|
||||
module type USTRUCTURE = sig
|
||||
|
||||
(** @inline *)
|
||||
include STRUCTURE
|
||||
include SSTRUCTURE
|
||||
|
||||
(**[InconsistentConjunction] is raised by {!conjunction}. *)
|
||||
exception InconsistentConjunction
|
||||
|
@ -100,23 +91,47 @@ module type CONJUNCTIBLE = sig
|
|||
|
||||
end
|
||||
|
||||
(* [IDENTIFIABLE] describes a structure with unique identifiers,
|
||||
as required by [OccursCheck.Make] and [Decoder.Make]. *)
|
||||
module type IDENTIFIABLE = sig
|
||||
(* [OCSTRUCTURE] describes an input of [OccursCheck.Make]. *)
|
||||
|
||||
module type OCSTRUCTURE = sig
|
||||
|
||||
(** @inline *)
|
||||
include STRUCTURE
|
||||
include SSTRUCTURE
|
||||
|
||||
(**[iter] applies an action to every child of a structure. *)
|
||||
val iter: ('a -> unit) -> 'a structure -> unit
|
||||
|
||||
(**[id] extracts the unique identifier of a structure. *)
|
||||
val id: 'a structure -> id
|
||||
|
||||
end
|
||||
|
||||
(* [MAPPABLE] describes traversable, mappable structures. *)
|
||||
module type MAPPABLE = sig
|
||||
(* [OSTRUCTURE] describes an input of [Decoder.Make]. *)
|
||||
|
||||
module type OSTRUCTURE = sig
|
||||
|
||||
(** @inline *)
|
||||
include STRUCTURE
|
||||
include OCSTRUCTURE
|
||||
|
||||
(**[map] applies a transformation to the children of a structure,
|
||||
while preserving the shape of the structure. *)
|
||||
val map: ('a -> 'b) -> 'a structure -> 'b structure
|
||||
|
||||
(**[is_leaf s] determines whether the structure [s] is a leaf, that is,
|
||||
whether it represents the absence of a logical constraint. This function
|
||||
is typically used by a decoder to determine which equivalence classes
|
||||
should be translated to "type variables" in a decoded type. *)
|
||||
val is_leaf: 'a structure -> bool
|
||||
|
||||
end
|
||||
|
||||
(* [GSTRUCTURE] describes an input of [Structure.Option],
|
||||
and also describes part of its output. *)
|
||||
|
||||
module type GSTRUCTURE = sig
|
||||
|
||||
(** @inline *)
|
||||
include USTRUCTURE
|
||||
|
||||
(**[iter] applies an action to every child of a structure. *)
|
||||
val iter: ('a -> unit) -> 'a structure -> unit
|
||||
|
@ -131,74 +146,37 @@ module type MAPPABLE = sig
|
|||
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* [USTRUCTURE] describes an input of [Unifier.Make]. *)
|
||||
|
||||
module type USTRUCTURE = sig
|
||||
|
||||
(** @inline *)
|
||||
include STRUCTURE
|
||||
|
||||
(** @inline *)
|
||||
include CONJUNCTIBLE with type 'a structure := 'a structure
|
||||
|
||||
end
|
||||
|
||||
(* [OSTRUCTURE] describes an input of [OccursCheck.Make]. *)
|
||||
|
||||
module type OSTRUCTURE = sig
|
||||
|
||||
(** @inline *)
|
||||
include STRUCTURE
|
||||
|
||||
(** @inline *)
|
||||
include MAPPABLE with type 'a structure := 'a structure
|
||||
|
||||
(** @inline *)
|
||||
include IDENTIFIABLE with type 'a structure := 'a structure
|
||||
end
|
||||
|
||||
(* [DSTRUCTURE] describes an input of [Decoder.Make]. *)
|
||||
|
||||
module type DSTRUCTURE = sig
|
||||
|
||||
(** @inline *)
|
||||
include STRUCTURE
|
||||
|
||||
(** @inline *)
|
||||
include MAPPABLE with type 'a structure := 'a structure
|
||||
|
||||
(** @inline *)
|
||||
include IDENTIFIABLE with type 'a structure := 'a structure
|
||||
|
||||
end
|
||||
|
||||
(* [GSTRUCTURE] describes an input of [Structure.Option]
|
||||
and an input of [Solver.Make]. *)
|
||||
|
||||
module type GSTRUCTURE = sig
|
||||
|
||||
(** @inline *)
|
||||
include STRUCTURE
|
||||
|
||||
(** @inline *)
|
||||
include CONJUNCTIBLE with type 'a structure := 'a structure
|
||||
|
||||
(** @inline *)
|
||||
include MAPPABLE with type 'a structure := 'a structure
|
||||
|
||||
end
|
||||
|
||||
(* [GSTRUCTURE_OPT] describes the output of [Structure.Option] and
|
||||
(* [STRUCTURE_LEAF] describes the output of [Structure.Option] and
|
||||
an input of [Generalization.Make]. *)
|
||||
|
||||
module type GSTRUCTURE_OPT = sig
|
||||
|
||||
module S : GSTRUCTURE
|
||||
module type STRUCTURE_LEAF = sig
|
||||
|
||||
(** @inline *)
|
||||
include GSTRUCTURE with type 'a structure = 'a S.structure option
|
||||
include GSTRUCTURE
|
||||
|
||||
(**The constant [leaf] is a structure that represents the absence of a
|
||||
logical constraint. It is typically used when a variable is created
|
||||
fresh. *)
|
||||
val leaf: 'a structure
|
||||
|
||||
(**[is_leaf s] determines whether the structure [s] is a leaf, that is,
|
||||
whether it represents the absence of a logical constraint. This function
|
||||
is typically used by a decoder to determine which equivalence classes
|
||||
should be translated to "type variables" in a decoded type. *)
|
||||
val is_leaf: 'a structure -> bool
|
||||
|
||||
end
|
||||
|
||||
(* [HSTRUCTURE] describes an input of [Solver.Make]. *)
|
||||
|
||||
module type HSTRUCTURE = sig
|
||||
|
||||
(** @inline *)
|
||||
include GSTRUCTURE
|
||||
|
||||
(**[pprint] is a structure printer, parameterized over a child printer.
|
||||
It is used for debugging purposes only. *)
|
||||
val pprint: ('a -> PPrint.document) -> 'a structure -> PPrint.document
|
||||
|
||||
end
|
||||
|
||||
|
@ -321,7 +299,7 @@ end
|
|||
module type OUTPUT = sig
|
||||
|
||||
(** @inline *)
|
||||
include STRUCTURE
|
||||
include SSTRUCTURE
|
||||
|
||||
(**A representation of decoded type variables. *)
|
||||
type tyvar
|
||||
|
@ -355,8 +333,12 @@ end
|
|||
module type DECODER = sig
|
||||
|
||||
type variable
|
||||
type tyvar
|
||||
type ty
|
||||
|
||||
(**[decode_variable v] decodes the variable [v]. *)
|
||||
val decode_variable: variable -> tyvar
|
||||
|
||||
(**[new_acyclic_decoder()] initiates a new decoding phase. It returns a
|
||||
decoding function [decode], which can be used as many as times as one
|
||||
wishes. Decoding requires the graph to be acyclic: it is a bottom-up
|
||||
|
|
269
src/Solver.ml
269
src/Solver.ml
|
@ -13,7 +13,7 @@ open Signatures
|
|||
|
||||
module Make
|
||||
(X : TEVAR)
|
||||
(S : GSTRUCTURE)
|
||||
(S : HSTRUCTURE)
|
||||
(O : OUTPUT with type 'a structure = 'a S.structure)
|
||||
= struct
|
||||
|
||||
|
@ -24,9 +24,6 @@ module Make
|
|||
type tevar =
|
||||
X.t
|
||||
|
||||
type tevars =
|
||||
tevar list
|
||||
|
||||
module TeVarMap =
|
||||
Hashtbl.Make(X)
|
||||
|
||||
|
@ -38,9 +35,6 @@ module TeVarMap =
|
|||
type variable =
|
||||
int
|
||||
|
||||
type variables =
|
||||
variable list
|
||||
|
||||
let fresh : unit -> variable =
|
||||
Utils.gensym()
|
||||
|
||||
|
@ -56,17 +50,8 @@ type range =
|
|||
type shallow_ty =
|
||||
variable O.structure
|
||||
|
||||
type tyvars =
|
||||
O.tyvar list
|
||||
|
||||
type tys =
|
||||
O.ty list
|
||||
|
||||
type scheme =
|
||||
tyvars * O.ty
|
||||
|
||||
type schemes =
|
||||
scheme list
|
||||
O.tyvar list * O.ty
|
||||
|
||||
(**A constraint of type ['a co] is a constraint whose resolution, if
|
||||
successful, produces a value of type ['a]. The ability for the
|
||||
|
@ -110,7 +95,7 @@ type _ co =
|
|||
a decoded type which represents the value assigned to the
|
||||
type variable [v] at the end of the resolution process. *)
|
||||
|
||||
| CInstance : tevar * variable -> tys co
|
||||
| CInstance : tevar * variable -> O.ty list co
|
||||
(**An instantiation constraint [CInstance (x, v)] requires the type
|
||||
variable [v] to be an instance of the type scheme denoted by the
|
||||
term variable [x]. Its result is a list of types that indicates
|
||||
|
@ -121,27 +106,25 @@ type _ co =
|
|||
the trivial (monomorphic) type scheme [v] in the constraint [c]. *)
|
||||
|
||||
| CLet :
|
||||
variables * tevars * variables * 'a co * 'b co ->
|
||||
(tyvars * schemes * 'a * 'b) co
|
||||
(**The constraint [CLet rs xs vs c1 c2] is solved as follows:
|
||||
- First, the constraint [∀rs.∃vs.c1] is solved.
|
||||
- Then, for each pair [(x, v)] drawn from the lists [xs] and [vs]
|
||||
(which must have the same length), the term variable [x] is
|
||||
bound to the constraint abstraction [λv.∃rs.∃(vs\v).c1].
|
||||
- Finally, under these bindings, the constraint [c2] is solved.
|
||||
variable list * (tevar * variable) list * 'a co * 'b co ->
|
||||
(O.tyvar list * (tevar * scheme) list * 'a * 'b) co
|
||||
(**[CLet rs (List.combine xs vs) c1 c2] first constructs a list
|
||||
[cs] of constraint abstractions by abstracting the type
|
||||
variables [vs] in the constraint [c1], under the scope of the
|
||||
rigid variables [rs]. Then, it binds the term variables [xs] to
|
||||
the constraint abstractions [cs] in the constraint [c2].
|
||||
|
||||
Thus, the variables [rs] are initially regarded as rigid while [c1]
|
||||
is solved and simplified; but, once this is done, their rigid
|
||||
nature disappears and they become flexible before generalization
|
||||
is performed. The scheme associated with the term variable [x]
|
||||
has the corresponding type variable [v] as its root.
|
||||
|
||||
The semantic value of this constraint is a tuple of:
|
||||
- a list [γs] of decoded type variables that may appear in the semantic
|
||||
value [v1].
|
||||
- a list of decoded schemes, in correspondence with the list [xs].
|
||||
- the semantic value [v1] of the constraint [c1].
|
||||
- the semantic value [v2] of the constraint [c2]. *)
|
||||
It produces a tuple of 4 results, namely:
|
||||
- a list [ws] of (decoded) type variables that may appear in [a1], hence
|
||||
should be universally bound by the client in [a1]. In a typical
|
||||
scenario, [a1] is a System F term, and the client must build a type
|
||||
abstraction [\Lambda vs.a1]. Note that [ws] must contain at least
|
||||
the (decodings of) the rigid variables [rs].
|
||||
- an association list that maps each term variable in [xs] to the type
|
||||
scheme that has been assigned to it while solving [c2].
|
||||
- the value [a1] produced by solving the constraint [c1].
|
||||
- the value [a2] produced by solving the constraint [c2].
|
||||
*)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
(* Exceptions. *)
|
||||
|
@ -149,7 +132,6 @@ type _ co =
|
|||
exception Unbound of range * tevar
|
||||
exception Unify of range * O.ty * O.ty
|
||||
exception Cycle of range * O.ty
|
||||
exception VariableScopeEscape of range
|
||||
|
||||
(* A pretty-printer for constraints, used while debugging. *)
|
||||
|
||||
|
@ -202,9 +184,7 @@ module Printer = struct
|
|||
annot (x, v) ^^
|
||||
string " in" ^/^
|
||||
self c
|
||||
| CLet (rs, xs, vs, c1, c2) ->
|
||||
assert (List.length xs = List.length vs);
|
||||
let xvs = List.combine xs vs in
|
||||
| CLet (rs, xvs, c1, c2) ->
|
||||
string "let" ^^
|
||||
(if rs = [] then empty else brackets (separate_map space var rs)) ^^
|
||||
separate_map (string " and ") annot xvs ^^
|
||||
|
@ -280,8 +260,8 @@ module U = G.U
|
|||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The solver carries an environment, an immutable mapping of term variables
|
||||
to type schemes. *)
|
||||
(* The solver carries an environment, an immutable mapping of term
|
||||
variables to type schemes. *)
|
||||
|
||||
module Env = struct
|
||||
|
||||
|
@ -305,11 +285,11 @@ end (* Env *)
|
|||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The solver maintains a mutable mapping of immutable type variables to
|
||||
unifier variables. *)
|
||||
(* We maintain a mutable mapping of immutable type variables to unifier
|
||||
variables. *)
|
||||
|
||||
(* [uvar] looks up the mapping. [flexible] and [rigid] create a new unifier
|
||||
variable and extend the mapping. [uunbind] removes a mapping. *)
|
||||
(* [uvar] looks up the mapping. [ubind] creates a new unifier variable and
|
||||
extends the mapping. [unbind] removes the mapping created by [bind]. *)
|
||||
|
||||
module UVar = struct
|
||||
|
||||
|
@ -323,15 +303,9 @@ module UVar = struct
|
|||
(* This should never happen. *)
|
||||
Printf.ksprintf failwith "Unbound variable %d" v
|
||||
|
||||
let flexible (v : variable) so =
|
||||
let ubind (v : variable) status so =
|
||||
assert (not (VarTable.mem table v));
|
||||
let uv = G.flexible (OS.map uvar so) in
|
||||
VarTable.add table v uv;
|
||||
uv
|
||||
|
||||
let rigid (v : variable) =
|
||||
assert (not (VarTable.mem table v));
|
||||
let uv = G.rigid() in
|
||||
let uv = G.fresh status (OS.map uvar so) in
|
||||
VarTable.add table v uv;
|
||||
uv
|
||||
|
||||
|
@ -357,41 +331,17 @@ end (* UVar *)
|
|||
(in the acyclic case), regardless of how many calls to the decoder are
|
||||
performed. *)
|
||||
|
||||
(* [decode_variable] decodes a variable, which must have
|
||||
leaf structure. The decoded variable is determined by the unique identity
|
||||
of the variable [v]. *)
|
||||
let decode_variable (v : U.variable) : O.tyvar =
|
||||
let data = U.get v in
|
||||
match G.Data.project data with
|
||||
| Some _ -> assert false
|
||||
| None -> O.inject (G.Data.id data)
|
||||
(* TODO explain *)
|
||||
|
||||
(* The module [D] is used to decode non-leaf structures *)
|
||||
module D =
|
||||
Decoder.Make (G.Data) (U) (struct
|
||||
include O
|
||||
let pprint = G.Data.pprint
|
||||
|
||||
let structure (s : O.ty U.structure) : O.ty =
|
||||
match G.Data.project s with
|
||||
| None -> O.variable (O.inject (G.Data.id s))
|
||||
| Some s -> O.structure s
|
||||
O.structure (OS.project_nonleaf (G.Data.project s))
|
||||
end)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Initialize a decoder for use during elaboration. If [rectypes] is on, a
|
||||
cyclic decoder is used; otherwise, an acyclic decoder is used. *)
|
||||
|
||||
let decode : U.variable -> O.ty =
|
||||
if rectypes then D.new_cyclic_decoder() else D.new_acyclic_decoder()
|
||||
|
||||
let decode_scheme (s : G.scheme) : scheme =
|
||||
List.map decode_variable (G.quantifiers s),
|
||||
decode (G.body s)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The exceptions [Unify] and [Cycle], raised by the unifier, must be caught
|
||||
and re-raised in a slightly different format.
|
||||
|
||||
|
@ -401,22 +351,28 @@ let decode_scheme (s : G.scheme) : scheme =
|
|||
let unify range v1 v2 =
|
||||
try
|
||||
U.unify v1 v2
|
||||
with
|
||||
| U.Unify (v1, v2) ->
|
||||
let decode = D.new_cyclic_decoder() in
|
||||
raise (Unify (range, decode v1, decode v2))
|
||||
| G.VariableScopeEscape ->
|
||||
raise (VariableScopeEscape range)
|
||||
with U.Unify (v1, v2) ->
|
||||
let decode = D.new_cyclic_decoder() in
|
||||
raise (Unify (range, decode v1, decode v2))
|
||||
|
||||
let exit range ~rectypes vs =
|
||||
try
|
||||
G.exit ~rectypes vs
|
||||
with
|
||||
| G.Cycle v ->
|
||||
let decode = D.new_cyclic_decoder() in
|
||||
raise (Cycle (range, decode v))
|
||||
| G.VariableScopeEscape ->
|
||||
raise (VariableScopeEscape range)
|
||||
with G.Cycle v ->
|
||||
let decode = D.new_cyclic_decoder() in
|
||||
raise (Cycle (range, decode v))
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Initialize a decoder for use during elaboration. If [rectypes] is on, a
|
||||
cyclic decoder is used; otherwise, an acyclic decoder is used. *)
|
||||
|
||||
let decode : U.variable -> O.ty =
|
||||
if rectypes then D.new_cyclic_decoder() else D.new_acyclic_decoder()
|
||||
|
||||
let decode_scheme (s : G.scheme) : scheme =
|
||||
List.map D.decode_variable (G.quantifiers s),
|
||||
decode (G.body s)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -439,7 +395,7 @@ let rec ok : type a . a co -> bool =
|
|||
true
|
||||
| CMap (c, _) ->
|
||||
ok c
|
||||
| CLet (_rs, _xs, _vs, _c1, c2) ->
|
||||
| CLet (_rs, _xvs, _c1, c2) ->
|
||||
(* The left-hand constraint [c1] does not need to be [ok], since it is
|
||||
examined after a call to [G.enter]. *)
|
||||
ok c2
|
||||
|
@ -510,7 +466,7 @@ let rec solve : type a . range -> a co -> a on_sol =
|
|||
unify range (uvar v) (uvar w);
|
||||
On_sol (fun () -> ())
|
||||
| CExist (v, s, c) ->
|
||||
ignore (flexible v s);
|
||||
ignore (ubind v G.Flexible_ s);
|
||||
let result = solve range c in
|
||||
uunbind v;
|
||||
result
|
||||
|
@ -531,16 +487,16 @@ let rec solve : type a . range -> a co -> a on_sol =
|
|||
let a = solve range c in
|
||||
Env.unbind x;
|
||||
a
|
||||
| CLet (rs, xs, vs, c1, c2) ->
|
||||
| CLet (rs, xvs, c1, c2) ->
|
||||
(* Warn the generalization engine that we are entering the left-hand
|
||||
side of a [let] construct. *)
|
||||
G.enter();
|
||||
(* Register the rigid prefix [rs] with the generalization engine. *)
|
||||
let urs = List.map (fun v -> rigid v) rs in
|
||||
(* Register the rigid prefix [rs] with th generalization engine. *)
|
||||
let _ = List.map (fun v -> ubind v G.Rigid_ None) rs in
|
||||
(* Register the variables [vs] with the generalization engine, just as
|
||||
if they were existentially bound in [c1]. This is what they are,
|
||||
basically, but they also serve as named entry points. *)
|
||||
let uvs = List.map (fun v -> flexible v None) vs in
|
||||
let vs = List.map (fun (_, v) -> ubind v G.Flexible_ None) xvs in
|
||||
(* Solve the constraint [c1]. *)
|
||||
let (On_sol r1) = solve range c1 in
|
||||
(* Ask the generalization engine to perform an occurs check, to adjust
|
||||
|
@ -548,24 +504,25 @@ let rec solve : type a . range -> a co -> a on_sol =
|
|||
of the type variables that were registered since the call to
|
||||
[G.enter] above), and to construct a list [ss] of type schemes for
|
||||
our entry points. The generalization engine also produces a list
|
||||
[gammas] of the young variables that should be universally
|
||||
[generalizable] of the young variables that should be universally
|
||||
quantified here. *)
|
||||
let gammas, ss = exit range ~rectypes uvs in
|
||||
(* All rigid variables of [rs] must be generalizable. This assertion
|
||||
may be costly and should be removed or disabled in the future. *)
|
||||
assert (urs |> List.for_all (fun r -> List.mem r gammas));
|
||||
List.iter uunbind vs;
|
||||
(* Extend the environment [env]. *)
|
||||
List.iter2 Env.bind xs ss;
|
||||
let generalizable, ss = exit range ~rectypes vs in
|
||||
List.iter (fun (_, v) -> uunbind v) xvs;
|
||||
(* Extend the environment [env] and compute the type schemes [xss]. *)
|
||||
let xss =
|
||||
List.fold_right2 (fun (x, _) s xss ->
|
||||
Env.bind x s;
|
||||
(x, s) :: xss
|
||||
) xvs ss []
|
||||
in
|
||||
(* Proceed to solve [c2] in the extended environment. *)
|
||||
let (On_sol r2) = solve range c2 in
|
||||
List.iter Env.unbind xs;
|
||||
List.iter (fun (x, _) -> Env.unbind x) xss;
|
||||
On_sol (fun () ->
|
||||
List.map decode_variable gammas,
|
||||
List.map decode_scheme ss,
|
||||
r1(),
|
||||
r2()
|
||||
)
|
||||
List.map D.decode_variable generalizable,
|
||||
List.map (fun (x, s) -> (x, decode_scheme s)) xss,
|
||||
r1 (),
|
||||
r2 ())
|
||||
|
||||
(* The solver's state is now ready. The following function (which must be
|
||||
called at most once, as it affects the solver's state) combines solving
|
||||
|
@ -749,55 +706,73 @@ let single xs =
|
|||
| _ ->
|
||||
assert false
|
||||
|
||||
(* [letrn] is our most general combinator. It offers full access to the
|
||||
expressiveness of [CLet] constraints. *)
|
||||
let letrn
|
||||
: 'client_tyvar list
|
||||
-> tevar list
|
||||
-> (('client_tyvar * variable) list
|
||||
-> (tevar * variable) list
|
||||
-> 'a co)
|
||||
-> 'b co
|
||||
-> (O.tyvar list * (tevar * scheme) list * 'a * 'b) co
|
||||
= fun alphas xs f1 c2 ->
|
||||
let rs = List.map (fun _a -> fresh ()) alphas in
|
||||
|
||||
(* The integer parameter [k] indicates how many rigid variables the user
|
||||
wishes to create. These variables are rigid while the left-hand constraint
|
||||
is solved. Once generalization has taken place, they become generic
|
||||
variables in the newly-created schemes. *)
|
||||
(* For each term variable [x], create a fresh type variable [v], as in
|
||||
[CExist]. *)
|
||||
let xvs = List.map (fun x ->
|
||||
x, fresh ()
|
||||
) xs in
|
||||
|
||||
let c1 = f1 (List.combine alphas rs) xvs in
|
||||
let+ (generalizable, ss, v1, v2) =
|
||||
CLet (rs, xvs, c1, c2)
|
||||
in
|
||||
(generalizable, ss, v1, v2)
|
||||
|
||||
(* [letr1] is a special case of [letrn], where only one term variable
|
||||
is bound. *)
|
||||
|
||||
let letr1
|
||||
: 'client_tyvar list
|
||||
-> tevar
|
||||
-> (('client_tyvar * variable) list -> variable -> 'a co)
|
||||
-> 'b co
|
||||
-> (O.tyvar list * 'a * 'b) co
|
||||
= fun alphas x f1 c2 ->
|
||||
let+ (generalizable, _ss, v1, v2) =
|
||||
letrn alphas [x]
|
||||
(fun rzs xzs ->
|
||||
let (_,z) = single xzs in
|
||||
f1 rzs z)
|
||||
c2
|
||||
in
|
||||
(generalizable, v1, v2)
|
||||
|
||||
(* The general form of [CLet] involves two constraints, the left-hand side and
|
||||
the right-hand side, yet it defines a *family* of constraint abstractions,
|
||||
which become bound to the term variables [xs]. *)
|
||||
|
||||
let letrn k xs f1 c2 =
|
||||
(* Allocate a list [rs] of [k] fresh type variables. *)
|
||||
let rs = List.init k (fun _ -> fresh()) in
|
||||
(* Allocate a fresh type variable for each term variable in [xs]. *)
|
||||
let vs = List.map (fun _ -> fresh()) xs in
|
||||
(* Apply [f1] to the lists [rs] and [vs], to obtain a constraint [c1]. *)
|
||||
let c1 = f1 rs vs in
|
||||
(* Done. *)
|
||||
CLet (rs, xs, vs, c1, c2)
|
||||
|
||||
(* [letr1] is a special case of [letrn] where only one term variable
|
||||
is bound, so the lists [xs], [vs], [ss] are singletons. *)
|
||||
|
||||
let letr1 k x f1 c2 =
|
||||
let+ gammas, ss, v1, v2 = letrn k [x] (fun rs vs -> f1 rs (single vs)) c2
|
||||
in gammas, single ss, v1, v2
|
||||
|
||||
(* [letn] is a special case of [letrn] where [k] is zero, so no rigid
|
||||
variables are created. *)
|
||||
|
||||
let letn xs f1 c2 =
|
||||
letrn 0 xs (fun _rs vs -> f1 vs) c2
|
||||
let+ (generalizable, xss, s1, s2) =
|
||||
letrn [] xs (fun _ xvs -> f1 (List.map snd xvs)) c2 in
|
||||
let ss = List.map snd xss in
|
||||
(generalizable, ss, s1, s2)
|
||||
|
||||
(* [let1] is a special case of [letn] where only one term variable
|
||||
is bound, so the lists [xs], [vs], [ss] are singletons. *)
|
||||
(* [let1] is a special case of [letn], where only one term variable is bound. *)
|
||||
|
||||
let let1 x f1 c2 =
|
||||
let+ gammas, ss, v1, v2 = letn [x] (fun vs -> f1 (single vs)) c2
|
||||
in gammas, single ss, v1, v2
|
||||
let+ (generalizable, ss, v1, v2) =
|
||||
letn [ x ] (fun vs -> f1 (single vs)) c2
|
||||
in (generalizable, single ss, v1, v2)
|
||||
|
||||
(* [let0] is a special case of [letn], where no term variable is bound, and
|
||||
the right-hand side is [CTrue]. The constraint produced by [let0] is [ok]
|
||||
by construction; in other words, it is a suitable argument to [solve]. *)
|
||||
|
||||
let let0 c1 =
|
||||
let+ gammas, _, v1, () = letn [] (fun _ -> c1) CTrue
|
||||
in gammas, v1
|
||||
let+ (generalizable, _, v1, ()) =
|
||||
letn [] (fun _ -> c1) CTrue
|
||||
in (generalizable, v1)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
|
|
250
src/Solver.mli
250
src/Solver.mli
|
@ -31,21 +31,17 @@ open Signatures
|
|||
elaboration in order to construct an explicitly-typed program. *)
|
||||
module Make
|
||||
(X : sig (** @inline *) include TEVAR end)
|
||||
(S : sig (** @inline *) include GSTRUCTURE end)
|
||||
(S : sig (** @inline *) include HSTRUCTURE end)
|
||||
(O : sig (** @inline *) include OUTPUT
|
||||
with type 'a structure = 'a S.structure end)
|
||||
: sig
|
||||
|
||||
(**A scheme variable [x] is bound by {!def} or by {!let1} and its variants
|
||||
({!letr1}, {!letn}, {!letrn}) and is referred to by {!instance}. Such a
|
||||
variable denotes a Hindley-Milner type scheme [σ], or (equivalently) a
|
||||
constraint abstraction [λα.c], that is, a constraint [c] that is
|
||||
parameterized with a type variable [α]. *)
|
||||
(**A scheme variable [x] is bound by {!def}, {!let1}, {!letn}
|
||||
and is referred to by {!instance}. Such a variable denotes
|
||||
a Hindley-Milner type scheme σ, or (equivalently) a constraint
|
||||
abstraction λα.c. *)
|
||||
type tevar = X.t
|
||||
|
||||
type tevars =
|
||||
tevar list
|
||||
|
||||
(* The type ['a structure] of shallow types is provided by [S]
|
||||
(and repeated by [O]). *)
|
||||
|
||||
|
@ -53,21 +49,12 @@ module Make
|
|||
are provided by the module [O]. *)
|
||||
open O
|
||||
|
||||
type tyvars =
|
||||
tyvar list
|
||||
|
||||
type tys =
|
||||
ty list
|
||||
|
||||
(**A type variable α denotes an unknown type. The existential quantifier
|
||||
{!exist} introduces a {i flexible} type variable, whose value can be
|
||||
chosen so as to satisfy a constraint. The combinators {!(--)} and
|
||||
{!(---)} allow imposing equality constraints on type variables. *)
|
||||
type variable
|
||||
|
||||
type variables =
|
||||
variable list
|
||||
|
||||
(**A shallow type is a piece of structure whose children are
|
||||
type variables. *)
|
||||
type shallow_ty =
|
||||
|
@ -79,14 +66,11 @@ module Make
|
|||
| DeepVar of variable
|
||||
| DeepStructure of deep_ty structure
|
||||
|
||||
(**A decoded scheme consists of a list of quantifiers and a body. The
|
||||
quantifiers are decoded type variables; the body is a decoded type. The
|
||||
combinator {!let1} and its variants ({!letr1}, {!letn}, {!letrn}) produce
|
||||
schemes as part of their semantic value. *)
|
||||
type scheme = tyvars * ty
|
||||
|
||||
type schemes =
|
||||
scheme list
|
||||
(**A decoded scheme consists of a list of quantifiers and a body.
|
||||
The quantifiers are decoded type variables; the body is a decoded type.
|
||||
The combinators {!let1} and {!letn} produce schemes as part of
|
||||
their semantic value. *)
|
||||
type scheme = tyvar list * ty
|
||||
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -176,7 +160,7 @@ module Make
|
|||
val (let@) : ('a, 'r) binder -> ('a -> 'r co) -> 'r co
|
||||
|
||||
(**The binder [exist] creates a fresh type variable and binds it
|
||||
existentially in the constraint that is being constructed. *)
|
||||
existentially. *)
|
||||
val exist: (variable, 'r) binder
|
||||
|
||||
(**The binder [shallow τ] is analogous to [exist], but additionally
|
||||
|
@ -218,18 +202,19 @@ module Make
|
|||
|
||||
(**The constraint [instance x α] requires the type variable [α] to be an
|
||||
instance of the scheme denoted by the variable [x]. The variable [x]
|
||||
must have been bound earlier by {!def} or by {!let1} and its variants
|
||||
({!letr1}, {!letn}, {!letrn}).
|
||||
must have been bound earlier by {!def}, {!let1}, or {!letn}.
|
||||
|
||||
On paper, this constraint is written [x ≤ α]. One can also think of
|
||||
On paper, this constraint is often written [x ≤ α]. One can also think of
|
||||
[x] as a constraint abstraction, in which case this constraint can be
|
||||
written [x(α)], still on paper.
|
||||
|
||||
The semantic value of the constraint [instance x α] is a list of decoded
|
||||
types. This list indicates how the quantifiers of the scheme denoted by
|
||||
[x] have been instantiated. The length and order of this list match the
|
||||
length and order of the quantifiers of the scheme denoted by [x]. *)
|
||||
val instance: tevar -> variable -> tys co
|
||||
length and order of the quantifiers of the scheme denoted by [x]. This
|
||||
scheme is obtained as part of the semantic value of the combinator
|
||||
{!let1} and {!letn} where [x] is bound. *)
|
||||
val instance: tevar -> variable -> ty list co
|
||||
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -241,146 +226,62 @@ module Make
|
|||
equivalent to the equality constraint [α -- β]. *)
|
||||
val def: tevar -> variable -> 'a co -> 'a co
|
||||
|
||||
(**[let1 x c1 c2] binds the term variable [x] to the constraint abstraction
|
||||
(* [let1 x c1 c2] binds the term variable [x] to the constraint abstraction
|
||||
[c1] in the constraint [c2]. (Technically, [c1] is a function of a fresh
|
||||
type variable [α] to a constraint, as in {!exist}.) On paper, we write
|
||||
[let x = λα.c1(α) in c2] for this constraint.
|
||||
type variable to a constraint, as in [exist].) The resulting constraint
|
||||
produces a tuple of 4 results, namely:
|
||||
- a list [vs] of (decoded) type variables that may appear in [a1], and (hence)
|
||||
should be universally bound by the client in [a1]. In a typical scenario,
|
||||
[a1] is a System F term, and the client will build the type abstraction
|
||||
[\Lambda vs.a1].
|
||||
- the (decoded) type scheme that was assigned to [x] while solving [c2].
|
||||
- the value [a1] produced by the constraint [c1].
|
||||
- the value [a2] produced by the constraint [c2]. *)
|
||||
val let1: tevar -> (variable -> 'a co) -> 'b co ->
|
||||
(tyvar list * scheme * 'a * 'b) co
|
||||
|
||||
This constraint requires [∃α.c1(α)] to be satisfied. This is required
|
||||
even if the term variable [x] is not used in [c2].
|
||||
(* [let0 c] has the same meaning as [c], but, like [let1], produces a list [vs]
|
||||
of the type variables that may appear in the result of [c]. *)
|
||||
val let0: 'a co -> (tyvar list * 'a) co
|
||||
|
||||
Inside [c2], an instantiation constraint of the form [x(α')] is logically
|
||||
equivalent to [c1(α')]. In other words, a [let] constraint acts like a
|
||||
macro definition: every use of the variable [x] in the scope of this
|
||||
definition is equivalent to a copy of the constraint abstraction [c1].
|
||||
(* [letn xs c1 c2] binds [n] term variables [xs] to [n] constraint abstractions
|
||||
in the constraint [c2]. Here, [c1] is a function of [n] fresh type variables
|
||||
[vs] to a constraint. The [i]-th term variable, [x_i], ends up bound to the
|
||||
constraint abstraction of the [i]-th type variable in [c_1], which one could
|
||||
write [\lambda v_i.c_1]. *)
|
||||
val letn: tevar list -> (variable list -> 'a co) -> 'b co ->
|
||||
(tyvar list * scheme list * 'a * 'b) co
|
||||
|
||||
The semantic value of this constraint is a tuple of:
|
||||
- a list [γs] of decoded type variables that may appear in the semantic
|
||||
value [v1] and therefore should be bound by the user in [v1].
|
||||
For instance, if the user wishes to build an explicitly-typed
|
||||
System F term as the result of the elaboration process,
|
||||
then [v1] will be a System F term,
|
||||
and the user should construct the abstraction [Λγs.v1],
|
||||
also a System F term.
|
||||
The length of the list [γs] cannot be predicted.
|
||||
The order of its elements is arbitrarily chosen by the solver.
|
||||
- the decoded scheme assigned to [x] by the solver.
|
||||
- the semantic value [v1] of the constraint [c1].
|
||||
- the semantic value [v2] of the constraint [c2]. *)
|
||||
val let1:
|
||||
(* x: *) tevar ->
|
||||
(* c1: *) (variable -> 'a co) ->
|
||||
(* c2: *) 'b co ->
|
||||
(tyvars * scheme * 'a * 'b) co
|
||||
(* [letr1 alphas x (fun alphavs v -> c1) c2] binds the scheme variable [x]
|
||||
to the constraint abstraction [fun v -> c1] in the contstraint [c2],
|
||||
where [c1] is also abstracted over a list of rigid variables, one for
|
||||
each client type variable passed in the list [alphas].
|
||||
|
||||
(**[letn] is a more general form of the combinator {!let1}. Like {!let1}, it
|
||||
is a binary combinator: it has a left-hand side [c1] and a right-hand
|
||||
side [c2]. However, whereas {!let1} binds one type variable [α] in [c1]
|
||||
and constructs one scheme, which becomes bound to the variable [x] in
|
||||
[c2], [letn] binds [n] type variables [αs] in [c1] and constructs [n]
|
||||
schemes, which become bound to the variables [xs] in [c2].
|
||||
The resulting constraint produces a tuple of 3 results, namely:
|
||||
- a list [vs] of (decoded) type variables corresponding to the client type
|
||||
variables [alphas].
|
||||
- the value [a1] produced by the constraint [c1].
|
||||
- the value [a2] produced by the constraint [c2].
|
||||
|
||||
The meaning of the constraint [letn xs c1 c2] can be described as follows.
|
||||
Let [n] stand for the length of the list [xs].
|
||||
Let [αs] be a list of fresh flexible variables, of the same length.
|
||||
Let us write [xi] and [αi] for the [i]-th elements of the lists [xs]
|
||||
and [αs].
|
||||
Let us write [αs\αi] for the list [αs] deprived of [αi].
|
||||
Then,
|
||||
the constraint [letn xs c1 c2] is logically equivalent to
|
||||
[let xi = λαi.∃(αs\αi).c1(αs) in c2].
|
||||
That is, it is equivalent to the constraint [c2],
|
||||
where each variable [xi] is bound to the
|
||||
constraint abstraction [λαi.∃(αs\αi).c1(αs)].
|
||||
This constraint abstraction has one parameter,
|
||||
namely, the type variable [αi].
|
||||
Every other type variable in the list [αs] is considered
|
||||
existentially bound in this constraint abstraction.
|
||||
|
||||
This constraint requires [∃αs.c1(αs)] to be satisfied. This is required
|
||||
even if some of the term variables in the list [xs] are not used in [c2].
|
||||
|
||||
The semantic value of this constraint is a tuple of:
|
||||
- a list [γs] of decoded type variables that may appear in the semantic
|
||||
value [v1] (see {!let1}).
|
||||
- a list of decoded schemes, in correspondence with the list [xs].
|
||||
- the semantic value [v1] of the constraint [c1].
|
||||
- the semantic value [v2] of the constraint [c2].
|
||||
|
||||
The combinator [letn] is typically useful when performing type inference
|
||||
for a construct such as ML's [let p = e1 in e2], where [p] is a pattern.
|
||||
This construct performs Hindley-Milner generalization and binds several
|
||||
variables at once, namely the variables defined by the pattern [p]. The
|
||||
combinator [letn] allows performing generalization and constructing a
|
||||
scheme for each of the variables defined by [p]. *)
|
||||
val letn:
|
||||
(* xs: *) tevars ->
|
||||
(* c1: *) (variables -> 'a co) ->
|
||||
(* c2: *) 'b co ->
|
||||
(tyvars * schemes * 'a * 'b) co
|
||||
|
||||
(**The constraint [let0 c] is logically equivalent to [c]. Its semantic
|
||||
value is a tuple of:
|
||||
- a list [γs] of decoded type variables that may appear in the semantic
|
||||
value [v] (see {!let1}).
|
||||
- the semantic value [v] of the constraint [c].
|
||||
|
||||
[let0] can be viewed as a special case of {!letn} where [n] is zero
|
||||
and where the right-hand constraint [c2] is trivial (that is, true).
|
||||
|
||||
The constraint [let0 c] is a {i toplevel constraint}, which means that
|
||||
it can be passed as an argument to {!solve}. *)
|
||||
val let0: 'a co -> (tyvars * 'a) co
|
||||
|
||||
(**[letr1] is a more general form of the combinator {!let1}. It takes an
|
||||
integer parameter [k] and binds [k] rigid type variables [βs] in the
|
||||
left-hand constraint. Like [let1], it also binds a type variable [α]
|
||||
in the left-hand constraint. Thus, [c1] is a function of [βs] and [α]
|
||||
to a constraint. On paper, we write [let x = Rβs.λα.c1(βs)(α) in c2].
|
||||
|
||||
This constraint requires [∀βs.∃α.c1(α)] to be satisfied.
|
||||
This is required even if the term variable [x] is not used in [c2].
|
||||
Thus, the variables [βs] are regarded as rigid while [c1] is solved.
|
||||
|
||||
Then, while solving [c2], the term variable [x] is bound to
|
||||
the constraint abstraction [λα.∃βs.c1(βs)(α)].
|
||||
In other words, inside [c2], an instantiation constraint of the form
|
||||
[x(α')] is logically equivalent to [∃βs.c1(βs)(α')].
|
||||
At this stage, the variables [βs] are no longer treated as rigid,
|
||||
and can be instantiated.
|
||||
|
||||
The combinator [letr1] helps deal with programming language constructs
|
||||
where one or more rigid variables are explicitly introduced, such as
|
||||
[let id (type a) (x : a) : a = x in id 0] in OCaml. In this example,
|
||||
the type variable [a] must be treated as rigid while type-checking the
|
||||
left-hand side; then, the term variable [id] must receive the scheme
|
||||
[∀a.a → a], where [a] is no longer regarded as rigid, so this scheme
|
||||
can be instantiated to [int → int] while type-checking the right-hand
|
||||
side. *)
|
||||
val letr1:
|
||||
(* k: *) int ->
|
||||
(* x: *) tevar ->
|
||||
(* c1: *) (variables -> variable -> 'a co) ->
|
||||
(* c2: *) 'b co ->
|
||||
(tyvars * scheme * 'a * 'b) co
|
||||
|
||||
(**[letrn] subsumes {!let1}, {!letr1}, and {!letrn}.
|
||||
|
||||
Like {!letr1}, it takes an integer parameter [k] and binds [k]
|
||||
rigid type variables [βs] in the left-hand constraint.
|
||||
|
||||
Like {!letn}, it takes a list [xs] of term variables and binds a
|
||||
corresponding list [αs] of type variables in the left-hand constraint.
|
||||
|
||||
On paper, we write [let xs = Rβs.λαs.c1(βs)(αs) in c2] for the
|
||||
constraint that it constructs. *)
|
||||
val letrn:
|
||||
(* k: *) int ->
|
||||
(* xs: *) tevars ->
|
||||
(* c1: *) (variables -> variables -> 'a co) ->
|
||||
(* c2: *) 'b co ->
|
||||
(tyvars * schemes * 'a * 'b) co
|
||||
Note: unlike [let1], we do not necessarily decode the type scheme
|
||||
corresponding to [x]; it is less interesting as we know that it
|
||||
must use exactly the rigid variables [vs] and no other. The
|
||||
client could still compute the decoded scheme by asking to decode
|
||||
the witness type of [v] within [c1].
|
||||
*)
|
||||
val letr1: 'client_tyvar list
|
||||
-> tevar
|
||||
-> (('client_tyvar * variable) list -> variable -> 'a co)
|
||||
-> 'b co
|
||||
-> (tyvar list * 'a * 'b) co
|
||||
|
||||
val letrn: 'client_tyvar list
|
||||
-> tevar list
|
||||
-> (('client_tyvar * variable) list
|
||||
-> (tevar * variable) list
|
||||
-> 'a co)
|
||||
-> 'b co
|
||||
-> (tyvar list * (tevar * scheme) list * 'a * 'b) co
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
(* Correlation with the source code. *)
|
||||
|
@ -393,9 +294,8 @@ module Make
|
|||
(**The constraint [correlate range c] is equivalent to [c], but records that
|
||||
this constraint is correlated with the range [range] in the source code.
|
||||
This information is used in error reports. The exceptions {!Unbound},
|
||||
{!Unify}, {!Cycle}, and {!VariableScopeEscape} carry a range: it is the
|
||||
nearest range that encloses the abstract syntax tree node where the error
|
||||
is detected. *)
|
||||
{!Unify}, and {!Cycle} carry a range: it is the nearest range that
|
||||
encloses the abstract syntax tree node where the error is detected. *)
|
||||
val correlate: range -> 'a co -> 'a co
|
||||
|
||||
(** {2 Solving Constraints} *)
|
||||
|
@ -414,13 +314,6 @@ module Make
|
|||
is a recursive type: that is, this type involves a μ binder. *)
|
||||
exception Cycle of range * ty
|
||||
|
||||
(**This exception is raised by {!solve} when a rigid variable escapes its
|
||||
scope, that is, roughly speaking, when one attempts to unify a rigid
|
||||
variable with a more ancient flexible variable. For example, attempting
|
||||
to solve the constraints [∃α. ∀β. α = β] or [∃α. ∀β. ∃γ. α = β → γ]
|
||||
causes this exception to be raised. *)
|
||||
exception VariableScopeEscape of range
|
||||
|
||||
(**[solve ~rectypes c] determines whether the constraint [c] is satisfiable,
|
||||
and if so, computes and returns its semantic value. (The constraint [c]
|
||||
must be closed, so it is satisfiable if and only if it is valid.) If [c]
|
||||
|
@ -430,10 +323,9 @@ module Make
|
|||
can be raised only when [rectypes] is [false].
|
||||
|
||||
The constraint [c] must be a {i toplevel constraint}. This means that
|
||||
every (binding or free) occurrence of a type variable must be wrapped in
|
||||
{!let0} or in the left-hand side of {!let1} or its variants ({!letr1},
|
||||
{!letn}, {!letrn}). To turn an arbitrary constraint [c] into a toplevel
|
||||
constraint, just write [let0 c]. *)
|
||||
every (binding or free) occurrence of a type variable must appear in the
|
||||
left-hand side of {!let0}, {!let1}, or {!letn}. To turn an arbitrary
|
||||
constraint [c] into a toplevel constraint, just write [let0 c]. *)
|
||||
val solve: rectypes:bool -> 'a co -> 'a
|
||||
|
||||
(**/**)
|
||||
|
|
|
@ -13,8 +13,6 @@ open Signatures
|
|||
|
||||
module Option (S : GSTRUCTURE) = struct
|
||||
|
||||
module S = S
|
||||
|
||||
type 'a structure =
|
||||
'a S.structure option
|
||||
|
||||
|
@ -54,7 +52,13 @@ module Option (S : GSTRUCTURE) = struct
|
|||
let s = S.conjunction equate s1 s2 in
|
||||
if s == s1 then so1 else Some s
|
||||
|
||||
let pprint elem os =
|
||||
PPrint.OCaml.option (S.pprint elem) os
|
||||
let leaf =
|
||||
None
|
||||
|
||||
let is_leaf =
|
||||
Option.is_none
|
||||
|
||||
let project_nonleaf =
|
||||
Option.get
|
||||
|
||||
end (* Option *)
|
||||
|
|
|
@ -21,6 +21,11 @@ open Signatures
|
|||
module Option (S : sig (** @inline *) include GSTRUCTURE end) : sig
|
||||
|
||||
(** @inline *)
|
||||
include GSTRUCTURE_OPT with module S = S
|
||||
include STRUCTURE_LEAF with type 'a structure = 'a S.structure option
|
||||
|
||||
(**[project_nonleaf (Some s)] is [s], while [project_nonleaf None] is
|
||||
undefined. In other words, if [os] is a non-leaf optional structure,
|
||||
then [project_nonleaf os] is the underlying structure. *)
|
||||
val project_nonleaf : 'a structure -> 'a S.structure
|
||||
|
||||
end
|
||||
|
|
Loading…
Reference in New Issue