Merge Env and SVMap.
parent
b7b0bd9fe8
commit
90c0049a87
|
@ -129,11 +129,32 @@ end
|
|||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Instantiate the solver. *)
|
||||
type tvar =
|
||||
| Tevar of string
|
||||
| SVar of int
|
||||
|
||||
let fresh () : tvar =
|
||||
let uid = Inferno.Utils.gensym()() in
|
||||
SVar uid
|
||||
|
||||
module X = struct
|
||||
type tevar = string
|
||||
let compare = String.compare
|
||||
let to_string s = s
|
||||
type tevar = tvar
|
||||
let compare v1 v2 =
|
||||
match v1, v2 with
|
||||
| Tevar v1, Tevar v2 ->
|
||||
compare v1 v2
|
||||
| SVar v1, SVar v2 ->
|
||||
Stdlib.compare v1 v2
|
||||
| Tevar _, SVar _ ->
|
||||
-1
|
||||
| SVar _, Tevar _ ->
|
||||
1
|
||||
let to_string v =
|
||||
match v with
|
||||
| Tevar v ->
|
||||
v
|
||||
| SVar v ->
|
||||
string_of_int v
|
||||
end
|
||||
|
||||
module Solver = Inferno.Solver.Make(X)(S)(O)
|
||||
|
@ -304,7 +325,7 @@ let convert env params ty =
|
|||
let deep_ty = convert_deep env params ty in
|
||||
build deep_ty
|
||||
|
||||
exception VariableConflict of string
|
||||
exception VariableConflict of ML.tevar
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -333,7 +354,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
|
|||
| ML.Var (pos, x) ->
|
||||
|
||||
(* [w] must be an instance of the type scheme associated with [x]. *)
|
||||
let+ tys = instance x w in
|
||||
let+ tys = instance (Tevar x) w in
|
||||
(* The translation makes the type application explicit. *)
|
||||
F.ftyapp (F.Var (pos, x)) tys
|
||||
|
||||
|
@ -349,7 +370,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
|
|||
let+ () = w --- arrow v1 v2
|
||||
(* Under the assumption that [x] has type [domain], the term [u] must
|
||||
have type [codomain]. *)
|
||||
and+ u' = def x v1 (hastype u v2)
|
||||
and+ u' = def (Tevar x) v1 (hastype u v2)
|
||||
and+ ty1 = witness v1
|
||||
in
|
||||
(* Once these constraints are solved, we obtain the translated function
|
||||
|
@ -370,7 +391,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
|
|||
| ML.Let (pos, x, t, u) ->
|
||||
|
||||
(* Construct a ``let'' constraint. *)
|
||||
let+ ((b, _), a, t', u') = let1 x (hastype t) (hastype u w) in
|
||||
let+ ((b, _), a, t', u') = let1 (Tevar x) (hastype t) (hastype u w) in
|
||||
(* [a] are the type variables that we must bind (via Lambda abstractions)
|
||||
while type-checking [t]. [(b, _)] is the type scheme that [x] must
|
||||
receive while type-checking [u]. Its quantifiers [b] are guaranteed to
|
||||
|
@ -400,10 +421,11 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
|
|||
vs |> mapM_now (fun alpha k -> let@ v = exist in k (alpha, v)) in
|
||||
convert_annot typedecl_env params w t ty
|
||||
| (ML.Rigid, vs, ty) ->
|
||||
let sv = fresh () in
|
||||
let+ (alphas, t', tys) =
|
||||
letr1 vs
|
||||
letr1 vs sv
|
||||
(fun tyvs w -> convert_annot typedecl_env tyvs w t ty)
|
||||
(fun s -> instance' s w)
|
||||
(instance sv w)
|
||||
in
|
||||
F.ftyapp (F.ftyabs alphas t') tys
|
||||
end
|
||||
|
@ -425,7 +447,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
|
|||
let on_var (x:ML.tevar) : ('a, 'r) binder =
|
||||
fun (k : 'b -> 'r co) : 'r co ->
|
||||
let@ v = exist in
|
||||
def x v (k v)
|
||||
def (Tevar x) v (k v)
|
||||
in
|
||||
|
||||
let@ vs = mapM_now on_var xs in
|
||||
|
@ -522,7 +544,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
|
|||
as the whole match statement *)
|
||||
hastype u v_return
|
||||
| (x, v1) :: pat_env ->
|
||||
def x v1 @@ bind_pattern_vars pat_env u
|
||||
def (Tevar x) v1 @@ bind_pattern_vars pat_env u
|
||||
in
|
||||
|
||||
let on_branch ((pat,u) : ML.branch)
|
||||
|
@ -630,13 +652,16 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
|
|||
type; it creates its own using [exist]. And it runs the solver. *)
|
||||
|
||||
type nonrec range = range
|
||||
exception Unbound = Solver.Unbound
|
||||
exception Unbound of range * string
|
||||
exception Unify = Solver.Unify
|
||||
exception Cycle = Solver.Cycle
|
||||
|
||||
let translate ~rectypes (env : ML.datatype_env) (t : ML.term) : F.nominal_term =
|
||||
Solver.solve ~rectypes (
|
||||
let+ (vs, t) = let0 (exist (hastype env t)) in
|
||||
(* [vs] are the binders that we must introduce *)
|
||||
F.ftyabs vs t
|
||||
)
|
||||
try
|
||||
Solver.solve ~rectypes (
|
||||
let+ (vs, t) = let0 (exist (hastype env t)) in
|
||||
(* [vs] are the binders that we must introduce *)
|
||||
F.ftyabs vs t
|
||||
)
|
||||
with Solver.Unbound (range, Tevar x) ->
|
||||
raise (Unbound (range, x))
|
||||
|
|
|
@ -25,15 +25,9 @@ module Make
|
|||
type tevar =
|
||||
X.tevar
|
||||
|
||||
type svar =
|
||||
int
|
||||
|
||||
module TeVarMap =
|
||||
Map.Make(struct include X type t = tevar end)
|
||||
|
||||
module SVMap =
|
||||
Map.Make(Int)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The type variables that appear in constraints are immutable: they
|
||||
|
@ -45,9 +39,6 @@ type variable =
|
|||
let fresh : unit -> variable =
|
||||
Utils.gensym()
|
||||
|
||||
let fresh_svar : unit -> svar =
|
||||
Utils.gensym()
|
||||
|
||||
module VarTable = Hashtbl.Make(struct
|
||||
type t = variable
|
||||
let hash = Hashtbl.hash
|
||||
|
@ -105,8 +96,6 @@ type _ co =
|
|||
term variable [x]. Its result is a list of types that indicates
|
||||
how the type scheme was instantiated. *)
|
||||
|
||||
| CInstance' : svar * variable -> O.ty list co
|
||||
|
||||
| CDef : tevar * variable * 'a co -> 'a co
|
||||
(**The constraint [CDef (x, v, c)] binds the term variable [x] to
|
||||
the trivial (monomorphic) type scheme [v] in the constraint [c]. *)
|
||||
|
@ -129,7 +118,7 @@ type _ co =
|
|||
- the value [a2] produced by solving the constraint [c2].
|
||||
*)
|
||||
|
||||
| CLetRigid : variable list * variable * 'a co * svar * 'b co ->
|
||||
| CLetRigid : variable list * variable * 'a co * tevar * 'b co ->
|
||||
(O.tyvar list * 'a * 'b) co
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
@ -197,7 +186,7 @@ module Printer = struct
|
|||
next c1 ^^
|
||||
string " in")) ^/^
|
||||
self c2 ^^
|
||||
string " : " ^^ var s
|
||||
string " : " ^^ tevar s
|
||||
| _ ->
|
||||
next c
|
||||
|
||||
|
@ -229,8 +218,6 @@ module Printer = struct
|
|||
separate space [var v1; string "="; var v2]
|
||||
| CInstance (x, v) ->
|
||||
tevar x ^^ utf8string " ≤ " ^^ var v
|
||||
| CInstance'(sv, w) ->
|
||||
var sv ^^ utf8string " ≤ " ^^ var w
|
||||
| CExist _
|
||||
| CDef _
|
||||
| CLet _
|
||||
|
@ -457,7 +444,6 @@ let rec ok : type a . a co -> bool =
|
|||
| CExist _
|
||||
| CWitness _
|
||||
| CInstance _
|
||||
| CInstance' _
|
||||
| CDef _ ->
|
||||
(* These forms are not [ok], as they involve (free or binding
|
||||
occurrences of) type variables. *)
|
||||
|
@ -509,25 +495,25 @@ let solve ~(rectypes : bool) (type a) (c : a co) : a =
|
|||
range (the range annotation that was most recently encountered on the
|
||||
way down). *)
|
||||
|
||||
let rec solve : type a . env -> 'b SVMap.t -> range -> a co -> a on_sol =
|
||||
fun env senv range c -> match c with
|
||||
let rec solve : type a . env -> range -> a co -> a on_sol =
|
||||
fun env range c -> match c with
|
||||
| CRange (range, c) ->
|
||||
solve env senv range c
|
||||
solve env range c
|
||||
| CTrue ->
|
||||
On_sol (fun () -> ())
|
||||
| CMap (c, f) ->
|
||||
let (On_sol r) = solve env senv range c in
|
||||
let (On_sol r) = solve env range c in
|
||||
On_sol (fun () -> f (r ()))
|
||||
| CConj (c1, c2) ->
|
||||
let (On_sol r1) = solve env senv range c1 in
|
||||
let (On_sol r2) = solve env senv range c2 in
|
||||
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);
|
||||
On_sol (fun () -> ())
|
||||
| CExist (v, s, c) ->
|
||||
ignore (ubind v s);
|
||||
solve env senv range c
|
||||
solve env range c
|
||||
| CWitness v ->
|
||||
On_sol (fun () -> decode (uvar v))
|
||||
| CInstance (x, w) ->
|
||||
|
@ -539,14 +525,9 @@ let solve ~(rectypes : bool) (type a) (c : a co) : a =
|
|||
let witnesses, v = G.instantiate state s in
|
||||
unify range v (uvar w);
|
||||
On_sol (fun () -> List.map decode witnesses)
|
||||
| CInstance' (sv, w) ->
|
||||
let s = SVMap.find sv senv in
|
||||
let witnesses, v = G.instantiate state s in
|
||||
unify range v (uvar w);
|
||||
On_sol (fun () -> List.map decode witnesses)
|
||||
| CDef (x, v, c) ->
|
||||
let env = Env.bind x (G.trivial (uvar v)) env in
|
||||
solve env senv range c
|
||||
solve env range c
|
||||
| CLet (xvs, c1, c2) ->
|
||||
(* Warn the generalization engine that we are entering the left-hand
|
||||
side of a [let] construct. *)
|
||||
|
@ -556,7 +537,7 @@ let solve ~(rectypes : bool) (type a) (c : a co) : a =
|
|||
basically, but they also serve as named entry points. *)
|
||||
let vs = List.map (fun (_, v) -> ubind v None) xvs in
|
||||
(* Solve the constraint [c1]. *)
|
||||
let (On_sol r1) = solve env senv 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
|
||||
|
@ -572,7 +553,7 @@ let solve ~(rectypes : bool) (type a) (c : a co) : a =
|
|||
) xvs ss (env, [])
|
||||
in
|
||||
(* Proceed to solve [c2] in the extended environment. *)
|
||||
let (On_sol r2) = solve env senv 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,
|
||||
|
@ -582,10 +563,10 @@ let solve ~(rectypes : bool) (type a) (c : a co) : a =
|
|||
G.enter state;
|
||||
let vs = List.map (fun v -> ubind_rigid v None) vs in
|
||||
let z = ubind z None in
|
||||
let (On_sol r1) = solve env senv range c1 in
|
||||
let (On_sol r1) = solve env range c1 in
|
||||
let s = exit_rigid range ~rectypes state z in
|
||||
let senv = SVMap.add sv s senv in
|
||||
let (On_sol r2) = solve env senv range c2 in
|
||||
let env = Env.bind sv s env in
|
||||
let (On_sol r2) = solve env range c2 in
|
||||
On_sol (fun () ->
|
||||
List.map decode_variable vs,
|
||||
r1 (),
|
||||
|
@ -593,10 +574,9 @@ let solve ~(rectypes : bool) (type a) (c : a co) : a =
|
|||
in
|
||||
|
||||
let env = Env.empty
|
||||
and senv = SVMap.empty
|
||||
and range = Lexing.(dummy_pos, dummy_pos) in
|
||||
(* Phase 1: solve the constraint. *)
|
||||
let (On_sol r) = solve env senv range c in
|
||||
let (On_sol r) = solve env range c in
|
||||
(* Phase 2: elaborate. *)
|
||||
r()
|
||||
|
||||
|
@ -738,9 +718,6 @@ let instance x v =
|
|||
|
||||
let instance_ x v =
|
||||
CMap (instance x v, ignore)
|
||||
|
||||
let instance' sv v =
|
||||
CInstance' (sv, v)
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Constraint abstractions. *)
|
||||
|
@ -797,17 +774,16 @@ let let0 c1 =
|
|||
|
||||
let letr1
|
||||
: 'tyvar list
|
||||
-> tevar
|
||||
-> (('tyvar * variable) list -> variable -> 'a co)
|
||||
-> (svar -> 'b co)
|
||||
-> 'b co
|
||||
-> (O.tyvar list * 'a * 'b) co
|
||||
= fun alphas f1 f2 ->
|
||||
= fun alphas sv f1 c2 ->
|
||||
let xvss = List.map (fun a ->
|
||||
a, fresh ()
|
||||
) alphas in
|
||||
let z = fresh () in
|
||||
let c1 = f1 xvss z in
|
||||
let sv = fresh_svar () in
|
||||
let c2 = f2 sv in
|
||||
CLetRigid (List.map snd xvss, z, c1, sv, c2)
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
|
|
@ -21,8 +21,6 @@ module Make
|
|||
(* The type [tevar] of term variables is provided by [X]. *)
|
||||
open X
|
||||
|
||||
type svar
|
||||
|
||||
(* The type ['a structure] of shallow types is provided by [S]
|
||||
(and repeated by [O]). *)
|
||||
|
||||
|
@ -129,8 +127,6 @@ module Make
|
|||
|
||||
(* [instance_ x v] is equivalent to [instance x v <$$> ignore]. *)
|
||||
val instance_: tevar -> variable -> unit co
|
||||
|
||||
val instance': svar -> variable -> ty list co
|
||||
(* ---------------------------------------------------------------------- *)
|
||||
|
||||
(* Construction of constraint abstractions, a.k.a. generalization. *)
|
||||
|
@ -154,8 +150,9 @@ module Make
|
|||
(scheme * tyvar list * 'a * 'b) co
|
||||
|
||||
val letr1: 'tyvar list
|
||||
-> tevar
|
||||
-> (('tyvar * variable) list -> variable -> 'a co)
|
||||
-> (svar -> 'b co)
|
||||
-> 'b co
|
||||
-> (tyvar list * 'a * 'b) co
|
||||
|
||||
(* [let0 c] has the same meaning as [c], but, like [let1], produces a list [vs]
|
||||
|
|
Loading…
Reference in New Issue