Commit ea85ced0 authored by Gabriel Scherer's avatar Gabriel Scherer
Browse files

Solver: basically get rid of continuations

By adding a CMap constructor to our raw constraints, we can implement
map directly within the constraint language, so we don't need to
define ('a co) as a pair of a constraint and a continuation anymore,
raw constraints are expressive enough.
parent 6395a62e
Pipeline #251402 passed with stage
in 18 minutes and 4 seconds
......@@ -44,31 +44,23 @@ type variable =
is invoked. It is allowed to examine the witness, and must produce a value of
type ['a]. *)
type 'a co =
Co : 's rawco * ('s -> 'a) -> 'a co
type 'a co = 'a rawco
(* -------------------------------------------------------------------------- *)
(* The type ['a co] forms an applicative functor. *)
let pure a =
Co (CTrue, fun () -> a)
CMap (CTrue, fun () -> a)
let (^&) (Co (rc1, k1)) (Co (rc2, k2)) =
Co (CConj (rc1, rc2),
fun (s1, s2) ->
let v1 = k1 s1 in
let v2 = k2 s2 in
(v1, v2))
let (^&) c1 c2 =
CConj (c1, c2)
let map f (Co (rc, k)) =
Co (rc,
fun s -> f (k s))
let map f c = CMap(c, f)
let (let+) a f = map f a
let (and+) = (^&)
(* The function [<$$>] is just [map] with reversed argument order. *)
let (<$$>) a f =
map f a
......@@ -77,11 +69,8 @@ let (<$$>) a f =
but drops the first component of the resulting pair, and keeps only the second
component. [f ^^ g] is equivalent to [f ^& g <$$> snd]. *)
let (^^) (Co (rc1, k1)) (Co (rc2, k2)) =
Co (CConj (rc1, rc2),
fun (s1, s2) ->
let _ = k1 s1 in
k2 s2)
let (^^) c1 c2 =
CMap(CConj (c1, c2), snd)
(* The type ['a co] does not form a monad. Indeed, there is no way of defining
a [bind] combinator. *)
......@@ -98,16 +87,15 @@ type ('a, 'r) binder = ('a -> 'r co) -> 'r co
let (let@) m f = m f
let witness v =
Co (CWitness v, fun (On_sol ty) -> ty ())
let witness v = CWitness v
let exist_aux t f =
(* Create a fresh constraint variable [v]. *)
let v = fresh () in
(* Pass [v] to the client, *)
let (Co (rc, k)) = f v in
(* and wrap the resulting constraint [rc] in an existential quantifier. *)
Co (CExist (v, t, rc), k)
let c = f v in
(* and wrap the resulting constraint [c] in an existential quantifier. *)
CExist (v, t, c)
let exist f =
exist_aux None f
......@@ -156,19 +144,15 @@ let build dty f =
in
(* Convert the deep type [dty] and pass the variable that stands for its
root to the user function [f]. *)
let (Co (rc, k)) = f (convert dty) in
let c = f (convert dty) in
(* Then, create a bunch of existential quantifiers, in an arbitrary order. *)
Co (List.fold_left (fun rc (v, s) -> CExist (v, Some s, rc)) rc !vs,
(* Keep an unchanged continuation. *)
k)
List.fold_left (fun rc (v, s) -> CExist (v, Some s, rc)) c !vs
(* -------------------------------------------------------------------------- *)
(* Equations. *)
let (--) v1 v2 =
Co (CEq (v1, v2),
fun () -> ())
let (--) v1 v2 = CEq (v1, v2)
let (---) v t =
lift (--) v t
......@@ -187,17 +171,11 @@ let _other_lift f v1 t2 =
(* Instantiation constraints. *)
let instance x v =
Co (CInstance (x, v),
fun (On_sol witnesses) -> witnesses ())
let instance x v = CInstance (x, v)
(* [instance_ x v] is equivalent to [instance x v <$$> ignore]. *)
let instance_ x v =
Co (CInstance (x, v),
fun _witnesses ->
(* In the decoding phase, there is nothing to do. *)
())
let instance_ x v = CMap (instance x v, ignore)
(* -------------------------------------------------------------------------- *)
......@@ -206,15 +184,13 @@ let instance_ x v =
(* The [CDef] form is so trivial that it deserves its own syntax. Viewing it
as a special case of [CLet] would be more costly (by a constant factor). *)
let def x v (Co (rc, k)) =
Co (CDef (x, v, rc),
k)
let def x v c = CDef (x, v, c)
(* 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,
bound the term variables [xs]. *)
let letn xs f1 (Co (rc2, k2)) =
let letn xs f1 c2 =
(* For each term variable [x], create a fresh type variable [v], as in
[CExist]. Also, create an uninitialized scheme hook, which will receive
the type scheme of [x] after the solver runs. *)
......@@ -224,13 +200,12 @@ let letn xs f1 (Co (rc2, k2)) =
(* Pass the vector of type variables to the user-supplied function [f1],
as in [CExist]. *)
let vs = List.map (fun (_, v) -> v) xvs in
let (Co (rc1, k1)) = f1 vs in
let c1 = f1 vs in
(* Build a [CLet] constraint. *)
Co (CLet (xvs, rc1, rc2),
(fun (On_sol extra) ->
let (generalizable, xss, s1, s2) = extra () in
let ss = List.map snd xss in
ss, generalizable, k1 s1, k2 s2))
CMap (CLet (xvs, c1, c2),
fun (generalizable, xss, s1, s2) ->
let ss = List.map snd xss in
(ss, generalizable, s1, s2))
(* The auxiliary function [single] asserts that its argument [xs] is a
singleton list, and extracts its unique element. *)
......@@ -263,8 +238,7 @@ let let0 c1 =
type range =
Lexing.position * Lexing.position
let correlate range (Co (rc, k)) =
Co (CRange (range, rc), k)
let correlate range c = CRange (range, c)
(* -------------------------------------------------------------------------- *)
......@@ -279,11 +253,11 @@ let correlate range (Co (rc, k)) =
include struct
[@@@warning "-4"] (* yes, I know the following pattern matching is fragile *)
let ok (Co (rc, _k)) =
match rc with
| CLet (_, _, CTrue) ->
(* The argument of [solve] should be constructed by [let0]. *)
true
let rec ok : type a . a rawco -> bool = function
| CRange (_range, c) -> ok c
| CMap (c, _f) -> ok c
| CLet (_, _, c) -> ok c
| CTrue -> true
| _ ->
false
......@@ -295,18 +269,14 @@ exception Unbound = Lo.Unbound
exception Unify of range * O.ty * O.ty
exception Cycle of range * O.ty
let solve ~rectypes (Co (rc, k)) =
assert (ok (Co (rc, k)));
let sol = try
let solve ~rectypes c =
assert (ok c || (Lo.print_rawco Format.err_formatter c; false));
try
(* Solve the constraint. *)
Lo.solve ~rectypes rc
Lo.solve ~rectypes c
with
| Lo.Unify (range, v1, v2) ->
raise (Unify (range, v1, v2))
| Lo.Cycle (range, v) ->
raise (Cycle (range, v))
in
(* Invoke the client continuation. *)
k sol
end
......@@ -123,21 +123,20 @@ let decode_scheme (decode : U.variable decoder) (s : G.scheme) : O.scheme =
type range =
Lexing.position * Lexing.position
type 'a on_sol = On_sol of (unit -> 'a) [@@unboxed]
type _ rawco =
| CRange : range * 'a rawco -> 'a rawco
| CTrue : unit rawco
| CConj : 'a rawco * 'b rawco -> ('a * 'b) rawco
| CEq : variable * variable -> unit rawco
| CExist : variable * variable S.structure option * 'a rawco -> 'a rawco
| CWitness : variable -> O.ty on_sol rawco
| CInstance : tevar * variable -> O.ty list on_sol rawco
| CWitness : variable -> O.ty rawco
| CInstance : tevar * variable -> O.ty list rawco
| CDef : tevar * variable * 'a rawco -> 'a rawco
| CLet : (tevar * variable) list
* 'a rawco
* 'b rawco
-> (O.tyvar list * (tevar * O.scheme) list * 'a * 'b) on_sol rawco
-> (O.tyvar list * (tevar * O.scheme) list * 'a * 'b) rawco
| CMap : 'a rawco * ('a -> 'b) -> 'b rawco
let pprint_rawco c : PPrint.document = begin[@warning "-4"]
let open! PPrint in
......@@ -147,6 +146,7 @@ let pprint_rawco c : PPrint.document = begin[@warning "-4"]
let self = print_binders in
group @@ match c with
| CRange(_range, c) -> self c
| CMap(c, _f) -> self c
| CExist (v, s, c) ->
string "exi" ^^ space
^^ group (
......@@ -178,6 +178,7 @@ let pprint_rawco c : PPrint.document = begin[@warning "-4"]
let next = print_simple in
group @@ match c with
| CRange(_range, c) -> self c
| CMap(c, _f) -> self c
| CConj (c1, c2) -> self c1 ^//^ separate space [string "*"; self c2]
| _ -> next c
......@@ -186,6 +187,7 @@ let pprint_rawco c : PPrint.document = begin[@warning "-4"]
let next = print_parenthesized in
group @@ match c with
| CRange(_range, c) -> self c
| CMap(c, _f) -> self c
| CTrue -> string "True"
| CWitness v -> separate space [string "wit"; print_var v]
| CEq (v1, v2) -> separate space [print_var v1; string "="; print_var v2]
......@@ -196,6 +198,7 @@ let pprint_rawco c : PPrint.document = begin[@warning "-4"]
and print_parenthesized : type a . a rawco -> _ = fun c ->
match c with
| CRange _
| CMap _
| CTrue
| CConj _
| CEq _
......@@ -249,14 +252,31 @@ let exit range ~rectypes state vs =
(* -------------------------------------------------------------------------- *)
(* The non-recursive wrapper function [solve] is parameterized by the flag
[rectypes], which indicates whether recursive types are permitted. It
expects a constraint and solves it; that is, either it fails with an
exception, or it succeeds and fills the write-once references that are
embedded in the syntax of the constraint. *)
(* The non-recursive wrapper function [solve] is parameterized by the
flag [rectypes], which indicates whether recursive types are
permitted.
[solve] expects a constraint of type [a rawco] and solves it,
returning a witness of tyoe [a]. It proceedings in two phases:
- resolution: first the constraint is traversed, with each part
solved eagerly,
- witness construction: if the resolution succeeded, a global
solution is available, and we construct a witness from the solution.
This is implemented by having the first phase return a closure of
type ['a on_sol], that describes how the witnesses should be
computed when the final value will be available.
*)
exception Unbound of range * tevar
(* ['a on_sol] represents values of type 'a that will only be
available once the solver has succeeded in finding a global
solution, as opposed to a value that is available as soon as it is
done traversing a sub-constraint. *)
type 'a on_sol = On_sol of (unit -> 'a) [@@unboxed]
let solve ~(rectypes : bool) (type a) (c : a rawco) : a =
(* Initialize the generalization engine. It has mutable state, so [state]
......@@ -295,18 +315,22 @@ let solve ~(rectypes : bool) (type a) (c : a rawco) : a =
(which maps term variables to type schemes) and with a range (it is the
range annotation that was most recently encountered on the way down). *)
let rec solve : type a . G.scheme XMap.t -> range -> a rawco -> a =
let rec solve : type a . G.scheme XMap.t -> range -> a rawco -> a on_sol =
fun env range c -> match c with
| CRange (range, c) ->
solve env range c
| CTrue ->
()
On_sol (fun () -> ())
| CMap (c, f) ->
let (On_sol r) = solve env range c in
On_sol (fun () -> f (r ()))
| CConj (c1, c2) ->
let r1 = solve env range c1 in
let r2 = solve env range c2 in
(r1, r2)
let (On_sol r1) = solve env range c1 in
let (On_sol r2) = solve env range c2 in
On_sol (fun () -> (r1 (), r2 ()))
| CEq (v, w) ->
unify range (uvar v) (uvar w)
unify range (uvar v) (uvar w);
On_sol (fun () -> ())
| CExist (v, s, c) ->
ignore (bind_uvar v s);
solve env range c
......@@ -333,7 +357,7 @@ let solve ~(rectypes : bool) (type a) (c : a rawco) : a =
but they also serve as named entry points. *)
let vs = List.map (fun (_, v) -> bind_uvar v None) xvs in
(* Solve the constraint [c1]. *)
let r1 = solve env range c1 in
let (On_sol r1) = solve env range c1 in
(* Ask the generalization engine to perform an occurs check, to adjust the
ranks of the type variables in the young generation (i.e., all of the
type variables that were registered since the call to [G.enter] above),
......@@ -348,14 +372,15 @@ let solve ~(rectypes : bool) (type a) (c : a rawco) : a =
) xvs ss (env, [])
in
(* Proceed to solve [c2] in the extended environment. *)
let r2 = solve env range c2 in
let (On_sol r2) = solve env range c2 in
On_sol (fun () ->
List.map decode_variable generalizable,
List.map (fun (x, s) -> (x, decode_scheme decode s)) xss,
r1,
r2)
r1 (),
r2 ())
in
let env = XMap.empty
and range = Lexing.(dummy_pos, dummy_pos) in
solve env range c
let (On_sol witness) = solve env range c in
witness ()
end
......@@ -49,13 +49,6 @@ module Make
(* ---------------------------------------------------------------------- *)
(* ['a on_sol] represents values of type 'a that will only be
available once the solver has succeeded in finding a global
solution, as opposed to a value that is available as soon as it is
done traversing a sub-constraint (the more general meaning of the
GADT parameter of raw_constraint). *)
type 'a on_sol = On_sol of (unit -> 'a) [@@unboxed]
(* The syntax of constraints is as follows. *)
type _ rawco =
......@@ -78,7 +71,7 @@ module Make
some structure [s]. *)
| CExist : variable * variable structure option * 'a rawco -> 'a rawco
| CWitness : variable -> ty on_sol rawco
| CWitness : variable -> ty rawco
(* An application of a constraint abstraction, [x w]. The term
variable refers to a constraint abstraction (in other words, a type
......@@ -86,7 +79,7 @@ module Make
abstraction is applied to the type variable [w] (in other words, [w] must
be an instance of this type scheme). The solver will compute and return
a list of witnesses, indicating how the type scheme was instantiated. *)
| CInstance : tevar * variable -> ty list on_sol rawco
| CInstance : tevar * variable -> ty list rawco
(* A trivial type scheme definition, [def x = v in C]. This binds [x] to
the monomorphic type scheme [v] in the constraint [C]. In other words,
......@@ -107,7 +100,9 @@ module Make
| CLet : (tevar * variable) list
* 'a rawco
* 'b rawco
-> (tyvar list * (tevar * scheme) list * 'a * 'b) on_sol rawco
-> (tyvar list * (tevar * scheme) list * 'a * 'b) rawco
| CMap : 'a rawco * ('a -> 'b) -> 'b rawco
val print_rawco : Format.formatter -> _ rawco -> unit
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment