From 90c0049a87b2626dd43e5efa16d429feb97fe54b Mon Sep 17 00:00:00 2001 From: Olivier Date: Mon, 24 Jan 2022 11:59:38 +0100 Subject: [PATCH] Merge Env and SVMap. --- client/Infer.ml | 59 ++++++++++++++++++++++++++++++++-------------- src/Solver.ml | 62 +++++++++++++++---------------------------------- src/Solver.mli | 7 ++---- 3 files changed, 63 insertions(+), 65 deletions(-) diff --git a/client/Infer.ml b/client/Infer.ml index bf04c11..550cb2d 100644 --- a/client/Infer.ml +++ b/client/Infer.ml @@ -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)) diff --git a/src/Solver.ml b/src/Solver.ml index c11541e..6865fb2 100644 --- a/src/Solver.ml +++ b/src/Solver.ml @@ -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) (* -------------------------------------------------------------------------- *) diff --git a/src/Solver.mli b/src/Solver.mli index 789799d..195f752 100644 --- a/src/Solver.mli +++ b/src/Solver.mli @@ -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]