Merge branch 'frozen' of https://gitea.lakaban.net/Olivier/inferno-experimental into frozen
This commit is contained in:
commit
5442fff85a
|
@ -409,7 +409,6 @@ let rec convert (env : Env.t) (params : (string * variable) list) (ty : ML.nomin
|
|||
in res
|
||||
|
||||
exception VariableConflict of string
|
||||
exception NotATyConstr of variable S.structure
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The client uses the combinators provided by the solver so as to transparently
|
||||
|
@ -500,6 +499,7 @@ let hastype (typedecl_env : Env.t) (t : ML.term) (w : variable) : F.nominal_term
|
|||
in F.Tuple ts'
|
||||
|
||||
| ML.LetProd (xs, t, u) ->
|
||||
|
||||
let on_var (x:ML.tevar) : ('a, 'r) binder =
|
||||
fun (k : 'b -> 'r co) : 'r co ->
|
||||
let@ v = exist_ in
|
||||
|
@ -512,37 +512,39 @@ let hastype (typedecl_env : Env.t) (t : ML.term) (w : variable) : F.nominal_term
|
|||
in F.LetProd(xs, t', u')
|
||||
|
||||
| ML.Variant (c, t) ->
|
||||
|
||||
let@ ty : variable S.structure = frozen w in
|
||||
|
||||
let (tid, params) =
|
||||
match ty with
|
||||
| S.TyConstr (tid, _env, tys) ->
|
||||
(tid, tys)
|
||||
| s ->
|
||||
raise (NotATyConstr s)
|
||||
|
||||
let ML.{ type_name ; arg_type ; _ } =
|
||||
match Env.descr_from_label typedecl_env c with
|
||||
| [ d ] ->
|
||||
d
|
||||
| _ ->
|
||||
failwith "todo"
|
||||
in
|
||||
|
||||
|
||||
let ML.{ type_params ; data_kind ; _ } as tdescr =
|
||||
Env.type_descr_from_type typedecl_env tid in
|
||||
Env.type_descr_from_type typedecl_env type_name in
|
||||
|
||||
if not data_kind then
|
||||
raise Env.UnexpectedRecord;
|
||||
|
||||
let (i, ldescr) = label_descr_from_type_descr tdescr c in
|
||||
|
||||
(* We begin by instantiating the type parameters of the variant's type *)
|
||||
let@ param_vars, param_types = instantiate_params type_params in
|
||||
|
||||
let@ v1 = exist_ in
|
||||
|
||||
(* Inference variable for the argument of the variant *)
|
||||
let@ w1 = convert typedecl_env param_vars ldescr.ML.arg_type in
|
||||
let@ w1 = convert typedecl_env param_vars arg_type in
|
||||
|
||||
(* Retrieve the index of the constructor in the list of labels_descr *)
|
||||
let i = Env.label_index tdescr c in
|
||||
|
||||
let+ () = w --- (constr type_name typedecl_env @@ List.map snd param_vars)
|
||||
and+ param_types = param_types
|
||||
and+ t' = hastype t w1
|
||||
and+ t' = hastype t v1
|
||||
and+ () = w1 -- v1
|
||||
in
|
||||
let sumtype =
|
||||
translate_constr_types typedecl_env param_types tid in
|
||||
translate_constr_types typedecl_env (List.map snd param_types) type_name in
|
||||
F.Inj (sumtype, i, t')
|
||||
|
||||
| ML.Match (t, branches) ->
|
||||
|
|
Loading…
Reference in New Issue