diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 5 | ||||
| -rw-r--r-- | src/ast_util.mli | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 18 |
3 files changed, 23 insertions, 2 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 7d366803..5393bb81 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -262,6 +262,8 @@ let nc_false = mk_nc NC_false let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown) +let mk_typquant qis = TypQ_aux (TypQ_tq qis, Parse_ast.Unknown) + let mk_fexp id exp = FE_aux (FE_Fexp (id, exp), no_annot) let mk_fexps fexps = FES_aux (FES_Fexps (fexps, false), no_annot) @@ -401,6 +403,9 @@ let prepend_id str = function | Id_aux (Id v, l) -> Id_aux (Id (str ^ v), l) | Id_aux (DeIid v, l) -> Id_aux (DeIid (str ^ v), l) +let prepend_kid str = function + | Kid_aux (Var v, l) -> Kid_aux (Var ("'" ^ str ^ String.sub v 1 (String.length v - 1)), l) + let string_of_base_effect_aux = function | BE_rreg -> "rreg" | BE_wreg -> "wreg" diff --git a/src/ast_util.mli b/src/ast_util.mli index 8f1f06e6..ad5134e0 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -60,6 +60,7 @@ val mk_funcl : id -> unit pat -> unit exp -> unit funcl val mk_fundef : (unit funcl) list -> unit def val mk_val_spec : val_spec_aux -> unit def val mk_typschm : typquant -> typ -> typschm +val mk_typquant : quant_item list -> typquant val mk_qi_id : base_kind_aux -> kid -> quant_item val mk_qi_nc : n_constraint -> quant_item val mk_fexp : id -> unit exp -> unit fexp @@ -176,6 +177,7 @@ val id_of_kid : kid -> id val kid_of_id : id -> kid val prepend_id : string -> id -> id +val prepend_kid : string -> kid -> kid module Id : sig type t = id diff --git a/src/type_check.ml b/src/type_check.ml index 87e747f9..8a56d9b2 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1337,6 +1337,12 @@ type uvar = | U_effect of effect | U_typ of typ +let uvar_subst_nexp sv subst = function + | U_nexp nexp -> U_nexp (nexp_subst sv subst nexp) + | U_typ typ -> U_typ (typ_subst_nexp sv subst typ) + | U_effect eff -> U_effect eff + | U_order ord -> U_order ord + exception Unification_error of l * string;; let unify_error l str = raise (Unification_error (l, str)) @@ -2893,15 +2899,23 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = let iarg = irule infer_exp env arg in typ_debug ("INFER: " ^ string_of_exp arg ^ " type " ^ string_of_typ (typ_of iarg)); try - let iarg, (unifiers, ex_kids, ex_nc) (* FIXME *) = type_coercion_unify env iarg typ in + (* If we get an existential when instantiating, we prepend + the identifier of the exisitential with the tag argN# to + denote that it was bound by the Nth argument to the + function. *) + let ex_tag = "arg" ^ string_of_int n ^ "#" in + let iarg, (unifiers, ex_kids, ex_nc) = type_coercion_unify env iarg typ in typ_debug (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers)); typ_debug ("EX KIDS: " ^ string_of_list ", " string_of_kid ex_kids); let env = match ex_kids, ex_nc with | [], None -> env | _, Some enc -> - let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env ex_kids in + let enc = List.fold_left (fun nc kid -> nc_subst_nexp kid (Nexp_var (prepend_kid ex_tag kid)) nc) enc ex_kids in + let env = List.fold_left (fun env kid -> Env.add_typ_var (prepend_kid ex_tag kid) BK_nat env) env ex_kids in Env.add_constraint enc env in + let tag_unifier uvar = List.fold_left (fun uvar kid -> uvar_subst_nexp kid (Nexp_var (prepend_kid ex_tag kid)) uvar) uvar ex_kids in + let unifiers = KBindings.map tag_unifier unifiers in all_unifiers := merge_uvars l !all_unifiers unifiers; let utyps' = List.map (subst_unifiers unifiers) utyps in let typs' = List.map (subst_unifiers unifiers) typs in |