Write instantiate_params with exist_ instead of fresh

This commit is contained in:
Olivier 2020-06-22 16:08:17 +02:00
parent 2fade74170
commit 5f6188bbf7
3 changed files with 9 additions and 8 deletions

View File

@ -212,11 +212,6 @@ let type_descr_from_label env l =
let ML.({ type_name ; _ }) = descr_from_label env l in
type_descr_from_type env type_name
let instantiate_params (typarams : string list)
: ((string * variable) list, 'r) binder =
fun (k : (string * variable) list -> 'r co) : 'r co ->
k @@ List.map (fun x -> x , fresh None) typarams
(* Might want to move this function into SolverHi.ml *)
let rec bind_list (f : ('a -> ('b, 'r) binder)) (xs : 'a list)
: ('b list, 'r) binder =
@ -229,6 +224,15 @@ let rec bind_list (f : ('a -> ('b, 'r) binder)) (xs : 'a list)
let@ ys = bind_list f xs in
k (y :: ys)
let instantiate_params (typarams : string list)
: ((string * variable) list, 'r) binder =
let create_var (x : string) : (string * variable, 'r) binder =
fun (k : string * variable -> 'r co) : 'r co ->
let@ y = exist_ in
k (x, y)
in
bind_list create_var typarams
let rec convert (vars : (string * variable) list) (ty : ML.nominal_type)
: (variable, 'r) binder =
fun (k : variable -> 'r co) : 'r co ->

View File

@ -115,7 +115,6 @@ let (^^) (rc1, k1) (rc2, k2) =
type ('a, 'r) binder = ('a -> 'r co) -> 'r co
let (let@) m f = m f
let fresh = fresh
(* BEGIN EXIST *)
let exist f =

View File

@ -93,8 +93,6 @@ module Make
val (let@) : ('a, 'r) binder -> ('a -> 'r co) -> 'r co
val fresh : variable O.structure option -> variable
(* Assume that the user-supplied function [c], applied to a fresh type
variable [v], produces a constraint of type ['a]. Then, [exist c] wraps it
in an existential quantifier for [v]. This results in a constraint of type