Simplify the types of [letr1] and [letrn].

master
François Pottier 8 months ago
parent 9f7a6e73a6
commit 5b51d055eb
  1. 6
      client/Infer.ml
  2. 53
      src/Solver.ml
  3. 10
      src/Solver.mli

@ -383,8 +383,10 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
let x = X.fresh () in
let+ (alphas, _scheme, t', tys) =
(* TODO fp: It is suspicious that the type scheme is dropped. *)
letr1 vs x
(fun tyvs z -> convert_annot typedecl_env tyvs z t ty)
letr1 (List.length vs) x
(fun tys z ->
let tyvs = List.combine vs tys in
convert_annot typedecl_env tyvs z t ty)
(instance x w)
in
F.ftyapp (F.ftyabs alphas t') tys

@ -718,38 +718,47 @@ let single xs =
| _ ->
assert false
let letrn alphas xs f1 c2 =
let rs = List.map (fun _a -> fresh ()) alphas in
(* 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
CLet (rs, xvs, c1, c2)
(* [letr1] is a special case of [letrn], where only one term variable
is bound. *)
(* [letrn] is our most general combinator. It offers full access to the
expressiveness of [CLet] constraints. *)
let letr1 alphas x f1 c2 =
let+ (gammas, ss, v1, v2) =
letrn alphas [x]
(fun rzs xzs ->
let (_,z) = single xzs in
f1 rzs z)
c2
in
(gammas, single ss, v1, v2)
(* 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. *)
(* 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. *)
let xvs = List.combine xs vs in
CLet (rs, xvs, 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 [] xs (fun _ xvs -> f1 (List.map snd xvs)) c2
letrn 0 xs (fun _rs vs -> f1 vs) c2
(* [let1] is a special case of [letn], where only one term variable is bound. *)
(* [let1] is a special case of [letn] where only one term variable
is bound, so the lists [xs], [vs], [ss] are singletons. *)
let let1 x f1 c2 =
let+ gammas, ss, v1, v2 = letn [ x ] (fun vs -> f1 (single vs)) c2
let+ gammas, ss, v1, v2 = letn [x] (fun vs -> f1 (single vs)) c2
in gammas, single ss, v1, v2
(* [let0] is a special case of [letn], where no term variable is bound, and

@ -315,17 +315,15 @@ module Make
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]. *)
val letr1: 'client_tyvar list
val letr1: int
-> tevar
-> (('client_tyvar * variable) list -> variable -> 'a co)
-> (variable list -> variable -> 'a co)
-> 'b co
-> (tyvar list * scheme * 'a * 'b) co
val letrn: 'client_tyvar list
val letrn: int
-> tevar list
-> (('client_tyvar * variable) list
-> (tevar * variable) list
-> 'a co)
-> (variable list -> variable list -> 'a co)
-> 'b co
-> (tyvar list * scheme list * 'a * 'b) co

Loading…
Cancel
Save