Commit 01e1f2d1 authored by Gabriel Scherer's avatar Gabriel Scherer
Browse files

merge Solver{Hi,Lo} and split them into separate modules

parent ea85ced0
Pipeline #251595 passed with stage
in 18 minutes and 6 seconds
......@@ -120,9 +120,10 @@ module X = struct
let to_string s = s
end
module Solver = Inferno.SolverHi.Make(X)(S)(O)
open Solver
module Constraints = Inferno.Constraints.Make(X)(S)(O)
type variable = Constraints.Type.variable
module Solver = Constraints.Solver
open Constraints.Combinators
(* -------------------------------------------------------------------------- *)
......@@ -304,7 +305,7 @@ let convert_annot env ((flex_vars, ty) : ML.type_annotation)
(* We will need a type environment to keep trace of term variables that must
be bound to solver variables during typechecking of patterns *)
type type_env = (ML.tevar * Solver.variable) list
type type_env = (ML.tevar * variable) list
(* -------------------------------------------------------------------------- *)
......@@ -493,7 +494,10 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
let u = bind_pattern_vars pat_env u in
k (pat ^& u)
k (
let+ pat = pat and+ u = u
in (pat, u)
)
in
mapM_later on_branch branches
......@@ -536,7 +540,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
List.fold_left union_ [] envs in
let on_pattern pat
: ((Solver.variable * (ML.tevar * variable) list)
: ((variable * (ML.tevar * variable) list)
* F.nominal_pattern co, 'r) binder
= fun k ->
let@ v = exist in
......@@ -574,14 +578,14 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
(* The top-level wrapper uses [let0]. It does not require an expected
type; it creates its own using [exist]. And it runs the solver. *)
type range = Solver.range
type range = Inferno.Utils.range
exception Unbound = Solver.Unbound
exception Unify = Solver.Unify
exception Cycle = Solver.Cycle
let translate (env : ML.datatype_env) (t : ML.term) : F.nominal_term =
solve ~rectypes:false (
let0 (exist (hastype env t)) <$$> fun (vs, t) ->
Solver.solve ~rectypes:false (
let+ (vs, t) = let0 (exist (hastype env t)) in
(* [vs] are the binders that we must introduce *)
F.ftyabs vs t
)
......@@ -12,6 +12,8 @@
open UnifierSig
open SolverSig
type range = Utils.range
module Make
(X : TEVAR)
(S : STRUCTURE)
......@@ -22,13 +24,10 @@ module Make
(* We rely on the low-level solver interface. *)
module Lo =
SolverLo.Make(X)(S)(O)
open Lo
module Constraint =
ConstraintType.Make(X)(S)(O)
type variable =
Lo.variable
open Constraint
(* -------------------------------------------------------------------------- *)
......@@ -44,7 +43,7 @@ type variable =
is invoked. It is allowed to examine the witness, and must produce a value of
type ['a]. *)
type 'a co = 'a rawco
type 'a co = 'a t
(* -------------------------------------------------------------------------- *)
......@@ -235,48 +234,7 @@ let let0 c1 =
(* Correlation with the source code. *)
type range =
Lexing.position * Lexing.position
let correlate range c = CRange (range, c)
(* -------------------------------------------------------------------------- *)
(* Running a constraint. *)
(* The constraint [c] should have been constructed by [let0], otherwise we
risk encountering variables that we cannot register. Recall that
[G.register] must not be called unless [G.enter] has been invoked first. Of
course, we could accept any old constraint from the user and silently wrap
it in [let0], but then, what would we do with the toplevel quantifiers? *)
include struct
[@@@warning "-4"] (* yes, I know the following pattern matching is fragile *)
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
end
(* Solving, or running, a constraint. *)
exception Unbound = Lo.Unbound
exception Unify of range * O.ty * O.ty
exception Cycle of range * O.ty
let solve ~rectypes c =
assert (ok c || (Lo.print_rawco Format.err_formatter c; false));
try
(* Solve the constraint. *)
Lo.solve ~rectypes c
with
| Lo.Unify (range, v1, v2) ->
raise (Unify (range, v1, v2))
| Lo.Cycle (range, v) ->
raise (Cycle (range, v))
end
......@@ -12,6 +12,8 @@
open UnifierSig
open SolverSig
type range = Utils.range
(* -------------------------------------------------------------------------- *)
(* The solver is parameterized over the nature of term variables, the type
......@@ -22,6 +24,8 @@ module Make
(O : OUTPUT with type 'a structure = 'a S.structure)
: sig
module Constraint := ConstraintType.Make(X)(S)(O)
(* The type [tevar] of term variables is provided by [X]. *)
open X
......@@ -35,42 +39,27 @@ module Make
(* ---------------------------------------------------------------------- *)
(* The type [variable] describes the solver's type variables. *)
type variable
type variable := Constraint.variable
(* The type ['a co] is the type of a constraint, which, once solved, produces
a result of type ['a]. Put another way, it is the type of a computation
which, once run to completion, produces a result of type ['a]. *)
type 'a co
type 'a co = 'a Constraint.t
(* ---------------------------------------------------------------------- *)
(* The applicative functor interface: tautology, conjunction, post-processing. *)
(* The following three operations form the applicative functor interface.
[pure] represents the true constraint, while [^&] builds a conjunction
of constraints. [map] does not per se produce any constraint; it only
[pure] represents the true constraint, while [(and+)] builds a conjunction
of constraints. [(let+)] does not per se produce any constraint; it only
performs postprocessing, i.e., it applies a user-supplied function to
the value that is obtained after constraint solving. *)
val pure: 'a -> 'a co
val (^&): 'a co -> 'b co -> ('a * 'b) co
val map: ('a -> 'b) -> 'a co -> 'b co
(* ---------------------------------------------------------------------- *)
val (let+): 'a co -> ('a -> 'b) -> 'b co
val (and+): 'a co -> 'b co -> ('a * 'b) co
(* Variants of the above. *)
(* [<$$>] is just [map] with reversed argument order. *)
val (<$$>): 'a co -> ('a -> 'b) -> 'b co
(* The function [^^], a variation of [^&], also builds a conjunction
constraint, but drops the first component of the resulting pair, and keeps
only the second component. [f ^^ g] is equivalent to [f ^& g <$$> snd]. *)
val (^^): 'a co -> 'b co -> 'b co
(* ---------------------------------------------------------------------- *)
(* Equations. *)
......@@ -186,43 +175,8 @@ module Make
(* Correlation with the source code. *)
(* The type [range] describes a range in the source code. *)
type range =
Lexing.position * Lexing.position
(* 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. *)
val correlate: range -> 'a co -> 'a co
(* ---------------------------------------------------------------------- *)
(* Evaluation. *)
(* [solve rectypes c] determines whether the constraint [c] is satisfiable.
If that is the case, then the constraint [c] is evaluated, and a result
of type ['a] is produced. (During this process, the functions that were
supplied as arguments to [map] during the construction of the constraint
are invoked.)
The flag [rectypes] determines whether equirecursive types are permitted.
If a term variable [x] is out of scope, [Unbound (range, x)] is raised,
where [range] is the range annotation that was most recently encountered
by the solver on the way down.
If the constraint is unsatisfiable, then [Unify] or [Cycle] is raised.
[Cycle] can be raised only if [rectypes] is [false]. *)
(* [solve] destroys its argument. It is not permitted to call [solve] twice
on the same constraint. *)
(* The argument to [solve] must have an application of [let0] at its root. This
is a way of ensuring that the final result has no free type variables. *)
exception Unbound of range * tevar
exception Unify of range * ty * ty
exception Cycle of range * ty
val solve: rectypes:bool -> 'a co -> 'a
end
(******************************************************************************)
(* *)
(* Inferno *)
(* *)
(* François Pottier, Inria Paris *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under the *)
(* terms of the MIT License, as described in the file LICENSE. *)
(* *)
(******************************************************************************)
open UnifierSig
open SolverSig
module Make
(X : TEVAR)
(S : STRUCTURE)
(O : OUTPUT with type 'a structure = 'a S.structure)
= struct
module Constraint = ConstraintType.Make(X)(S)(O)
open Constraint
let pprint c : PPrint.document = begin[@warning "-4"]
let open! PPrint in
let rec print : type a . a t -> _ = fun c -> print_binders c
and print_binders : type a . a t -> _ = fun c ->
let next = print_conj in
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 (
print_var v
^^ (match s with
| None -> empty
| Some s ->
space ^^ string "~" ^^ space ^^ string (S.to_string string_of_var s))
)
^^ space ^^ string "in"
^//^ self c
| CDef (x, v, c) ->
separate space [
string "def"; annot x v;
string "in";
] ^//^ self c
| CLet (xvs, c1, c2) ->
separate space [
string "let";
separate_map (space ^^ string "and" ^^ space) (fun (x, v) -> annot x v) xvs;
string "=";
next c1;
string "in";
] ^//^ self c2
| _ -> next c
and print_conj : type a . a t -> _ = fun c ->
let self = print_conj in
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
and print_simple : type a . a t -> _ = fun c ->
let self = print_simple in
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]
| CInstance (x, v) ->
separate space [string "inst"; print_tevar x; print_var v]
| _ -> next c
and print_parenthesized : type a . a t -> _ = fun c ->
match c with
| CRange _
| CMap _
| CTrue
| CConj _
| CEq _
| CExist _
| CWitness _
| CInstance _
| CDef _
| CLet _
->
surround 2 0 lparen (print c) rparen
and annot x v = separate space [print_tevar x; print_var v]
and print_tevar x = PPrint.string (X.to_string x)
and print_var v = PPrint.string (string_of_var v)
and string_of_var v = string_of_int (v :> int)
in print c
end
let print ppf c =
let open! PPrint in
ToFormatter.pretty 0.9 80 ppf (pprint c);
Format.pp_print_newline ppf ()
end
(******************************************************************************)
(* *)
(* Inferno *)
(* *)
(* François Pottier, Inria Paris *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under the *)
(* terms of the MIT License, as described in the file LICENSE. *)
(* *)
(******************************************************************************)
open UnifierSig
open SolverSig
(* This module offers the traditional, low-level presentation of a constraint
solver: a definition of the syntax of constraints and a function [solve],
which solves a constraint and annotates it, so as to publish information
that can be exploited in the reconstruction phase. *)
module Make
(X : TEVAR)
(S : STRUCTURE)
(O : OUTPUT with type 'a structure = 'a S.structure)
: sig
module Constraint := ConstraintType.Make(X)(S)(O)
val pprint : _ Constraint.t -> PPrint.document
val print : Format.formatter -> _ Constraint.t -> unit
end
......@@ -12,40 +12,27 @@
open UnifierSig
open SolverSig
type range = Utils.range
module Make
(X : TEVAR)
(S : STRUCTURE)
(O : OUTPUT with type 'a structure = 'a S.structure)
= struct
(* -------------------------------------------------------------------------- *)
(* The type [tevar] of term variables is provided by [X]. *)
type tevar =
X.tevar
module XMap =
Map.Make(struct include X type t = tevar end)
module Constraint = ConstraintType.Make(X)(S)(O)
(* The generalization engines is parametrized over inference structures [S],
it instantiates the generalization module [G] but also its underlying
unified [U]. *)
module G = Generalization.Make(S)
module U = G.U
(* The type [variable] of type variables is provided by the unifier [U]. *)
type variable = int
let fresh =
let counter = ref (-1) in
fun () ->
incr counter;
!counter
(* The type [ischeme] is provided by the generalization engine [G]. *)
(* -------------------------------------------------------------------------- *)
(* Decoding types. *)
......@@ -114,116 +101,6 @@ let decode_scheme (decode : U.variable decoder) (s : G.scheme) : O.scheme =
(* -------------------------------------------------------------------------- *)
(* The syntax of constraints is as follows. *)
(* This syntax is exposed to the user in the low-level interface [SolverLo],
but not in the high-level interface [SolverHi]. So, it could be easily
modified if desired. *)
type range =
Lexing.position * Lexing.position
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 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) rawco
| CMap : 'a rawco * ('a -> 'b) -> 'b rawco
let pprint_rawco c : PPrint.document = begin[@warning "-4"]
let open! PPrint in
let rec print : type a . a rawco -> _ = fun c -> print_binders c
and print_binders : type a . a rawco -> _ = fun c ->
let next = print_conj in
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 (
print_var v
^^ (match s with
| None -> empty
| Some s ->
space ^^ string "~" ^^ space ^^ string (S.to_string string_of_var s))
)
^^ space ^^ string "in"
^//^ self c
| CDef (x, v, c) ->
separate space [
string "def"; annot x v;
string "in";
] ^//^ self c
| CLet (xvs, c1, c2) ->
separate space [
string "let";
separate_map (space ^^ string "and" ^^ space) (fun (x, v) -> annot x v) xvs;
string "=";
next c1;
string "in";
] ^//^ self c2
| _ -> next c
and print_conj : type a . a rawco -> _ = fun c ->
let self = print_conj in
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
and print_simple : type a . a rawco -> _ = fun c ->
let self = print_simple in
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]
| CInstance (x, v) ->
separate space [string "inst"; print_tevar x; print_var v]
| _ -> next c
and print_parenthesized : type a . a rawco -> _ = fun c ->
match c with
| CRange _
| CMap _
| CTrue
| CConj _
| CEq _
| CExist _
| CWitness _
| CInstance _
| CDef _
| CLet _
->
surround 2 0 lparen (print c) rparen
and annot x v = separate space [print_tevar x; print_var v]
and print_tevar x = PPrint.string (X.to_string x)
and print_var v = PPrint.string (string_of_var v)
and string_of_var v = string_of_int v
in print c
end
let print_rawco ppf c =
let open! PPrint in
ToFormatter.pretty 0.9 80 ppf (pprint_rawco c);
Format.pp_print_newline ppf ()
(* -------------------------------------------------------------------------- *)
(* The exceptions [Unify] and [Cycle], raised by the unifier, must be caught
and re-raised in a slightly different format, as the unifier does not know
about ranges.
......@@ -256,7 +133,7 @@ let exit range ~rectypes state vs =
flag [rectypes], which indicates whether recursive types are
permitted.
[solve] expects a constraint of type [a rawco] and solves it,
[solve] expects a constraint of type [a Constraint.t] and solves it,
returning a witness of tyoe [a]. It proceedings in two phases:
- resolution: first the constraint is traversed, with each part
......@@ -277,7 +154,7 @@ exception Unbound of range * tevar
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 =
let solve_constraint ~(rectypes : bool) (type a) (c : a Constraint.t) : a =
(* Initialize the generalization engine. It has mutable state, so [state]
does not need to be an explicit parameter of the recursive function
......@@ -289,15 +166,15 @@ let solve ~(rectypes : bool) (type a) (c : a rawco) : a =
We map them to unification variables (uvars) by using a table
indexed over the constraint variable integer identifier. *)
let module VarTbl = Hashtbl.Make(struct
type t = variable
type t = Constraint.variable
let hash v = Hashtbl.hash v
let equal v1 v2 = Int.equal v1 v2
let equal v1 v2 = Int.equal (v1 : t :> int) (v2 : t :> int)
end) in
let uvars = VarTbl.create 8 in
let uvar v =
match VarTbl.find uvars v with
| None -> Printf.ksprintf failwith "Unbound variable %d" v
| None -> Printf.ksprintf failwith "Unbound variable %d" (v :> int)
| Some uv -> uv
in
......@@ -315,7 +192,8 @@ 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 on_sol =
let rec solve : type a . G.scheme XMap.t -> range -> a Constraint.t -> a on_sol =
let open Constraint in
fun env range c -> match c with
| CRange (range, c) ->
solve env range c
......@@ -383,4 +261,31 @@ let solve ~(rectypes : bool) (type a) (c : a rawco) : a =
and range = Lexing.(dummy_pos, dummy_pos) in
let (On_sol witness) = solve env range c in
witness ()
(* The toplevel constraint passed to the solver should have been constructed
by [let0], otherwise we risk encountering variables that we cannot
register. Recall that [G.register] must not be called unless [G.enter] has
been invoked first. Of course, we could accept any old constraint from the
user and silently wrap it in [let0], but then, what would we do with the
toplevel quantifiers? *)
include struct
[@@@warning "-4"] (* yes, I know the following pattern matching is fragile *)
let rec ok : type a . a Constraint.t -> bool =
let open Constraint in
function