diff options
| -rw-r--r-- | src/type_check.ml | 52 | ||||
| -rw-r--r-- | test/typecheck/fail/exist1.sail | 30 | ||||
| -rw-r--r-- | test/typecheck/pass/exist1.sail | 30 | ||||
| -rw-r--r-- | test/typecheck/pass/exist2.sail | 46 |
4 files changed, 133 insertions, 25 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index d23b7041..1a72edc9 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -250,7 +250,7 @@ and typ_subst_nexp_aux sv subst = function | Typ_tup typs -> Typ_tup (List.map (typ_subst_nexp sv subst) typs) | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_nexp sv subst) args) | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ) - | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_nexp sv subst typ) + | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc_subst_nexp sv subst nc, typ_subst_nexp sv subst typ) and typ_subst_arg_nexp sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_nexp_aux sv subst arg, l) and typ_subst_arg_nexp_aux sv subst = function | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp) @@ -306,7 +306,7 @@ and typ_subst_kid_aux sv subst = function | Typ_tup typs -> Typ_tup (List.map (typ_subst_kid sv subst) typs) | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_kid sv subst) args) | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ) - | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_kid sv subst typ) + | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc_subst_nexp sv (Nexp_var subst) nc, typ_subst_kid sv subst typ) and typ_subst_arg_kid sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_kid_aux sv subst arg, l) and typ_subst_arg_kid_aux sv subst = function | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv (Nexp_var subst) nexp) @@ -359,24 +359,6 @@ let typquant_subst_kid_aux sv subst = function let typquant_subst_kid sv subst (TypQ_aux (typq, l)) = TypQ_aux (typquant_subst_kid_aux sv subst typq, l) -let ex_counter = ref 0 - -let fresh_existential () = - let fresh = Kid_aux (Var ("'ex" ^ string_of_int !ex_counter), Parse_ast.Unknown) in - incr ex_counter; fresh - -let destructure_exist = function - | Typ_aux (Typ_exist (kids, nc, typ), _) -> - let fresh_kids = List.map (fun kid -> (kid, fresh_existential ())) kids in - let nc = List.fold_left (fun nc (kid, fresh) -> nc_subst_nexp kid (Nexp_var fresh) nc) nc fresh_kids in - let typ = List.fold_left (fun typ (kid, fresh) -> typ_subst_nexp kid (Nexp_var fresh) typ) typ fresh_kids in - Some (List.map snd fresh_kids, nc, typ) - | _ -> None - -let is_exist = function - | Typ_aux (Typ_exist (_, _, _), _) -> true - | _ -> false - (**************************************************************************) (* 2. Environment *) (**************************************************************************) @@ -919,6 +901,25 @@ let initial_env = Env.empty |> Env.add_typ_synonym (mk_id "atom") (fun args -> mk_typ (Typ_app (mk_id "range", args @ args))) +let ex_counter = ref 0 + +let fresh_existential () = + let fresh = Kid_aux (Var ("'ex" ^ string_of_int !ex_counter), Parse_ast.Unknown) in + incr ex_counter; fresh + +let destructure_exist env typ = + match Env.expand_synonyms env typ with + | Typ_aux (Typ_exist (kids, nc, typ), _) -> + let fresh_kids = List.map (fun kid -> (kid, fresh_existential ())) kids in + let nc = List.fold_left (fun nc (kid, fresh) -> nc_subst_nexp kid (Nexp_var fresh) nc) nc fresh_kids in + let typ = List.fold_left (fun typ (kid, fresh) -> typ_subst_nexp kid (Nexp_var fresh) typ) typ fresh_kids in + Some (List.map snd fresh_kids, nc, typ) + | _ -> None + +let is_exist = function + | Typ_aux (Typ_exist (_, _, _), _) -> true + | _ -> false + (**************************************************************************) (* 3. Subtyping and constraint solving *) (**************************************************************************) @@ -1395,7 +1396,7 @@ let rec unify l env typ1 typ2 = | Typ_arg_effect _, Typ_arg_effect _ -> assert false | _, _ -> unify_error l (string_of_typ_arg typ_arg1 ^ " cannot be unified with type argument " ^ string_of_typ_arg typ_arg2) in - match destructure_exist typ2 with + match destructure_exist env typ2 with | Some (kids, nc, typ2) -> let typ1, typ2 = Env.expand_synonyms env typ1, Env.expand_synonyms env typ2 in let unifiers = unify_typ l typ1 typ2 in @@ -1425,7 +1426,7 @@ let uv_nexp_constraint env (kid, uvar) = | _ -> env let subtyp l env typ1 typ2 = - match destructure_exist typ2 with + match destructure_exist env typ2 with | Some (kids, nc, typ2) -> let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in let unifiers, existential_kids, existential_nc = @@ -2415,7 +2416,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = let instantiate_ret env quants typs ret_typ = match ret_ctx_typ with | None -> (quants, typs, ret_typ, env) - | Some rct when is_exist rct -> (quants, typs, ret_typ, env) + | Some rct when is_exist (Env.expand_synonyms env rct) -> (quants, typs, ret_typ, env) | Some rct -> begin typ_debug ("RCT is " ^ string_of_typ rct); @@ -2466,9 +2467,10 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = else mk_typ (Typ_exist (existentials, List.fold_left nc_and nc_true ex_constraints, typ_ret)) in let exp = annot_exp (E_app (f, xs_reordered)) typ_ret eff in - + typ_debug ("RETURNING: " ^ string_of_typ (typ_of exp)); match ret_ctx_typ with - | None -> exp, !all_unifiers + | None -> + exp, !all_unifiers | Some rct -> let exp = type_coercion env exp rct in typ_debug ("RETURNING AFTER COERCION " ^ string_of_typ (typ_of exp)); diff --git a/test/typecheck/fail/exist1.sail b/test/typecheck/fail/exist1.sail new file mode 100644 index 00000000..3fab1366 --- /dev/null +++ b/test/typecheck/fail/exist1.sail @@ -0,0 +1,30 @@ + +let (exist 'n, 'n in {0, 1}. [:'n:]) v1 = 0 + +val bool -> exist 'n, 'n in {0, 1}. [:'n:] effect pure test + +function test flag = +{ + if flag then 0 else 1 +} + +let ([|0:1|]) v2 = test(true) + +val forall 'a, 'b. ([:'a:], [:'b:]) -> [:'a + 'b:] effect pure add + +let (exist 'k, 'k in {3, 4}. [:'k:]) v3 = 3 + +let (exist 'q, 'q in {0, 1}. [:'q + 3:]) v4 = v3 + +let v5 = add(test(true), 4) + +let ([:4:]) v6 = 4 + +function unit unit_fn (([:4:]) x) = () + +val forall 'a. ([:'a:], [:'a:]) -> [:'a + 'a:] effect pure s_add + +let (exist 'k, 'k = 4. [:'k:]) v7 = 4 + +let v8 = s_add(test(true), 4) + diff --git a/test/typecheck/pass/exist1.sail b/test/typecheck/pass/exist1.sail new file mode 100644 index 00000000..31968f36 --- /dev/null +++ b/test/typecheck/pass/exist1.sail @@ -0,0 +1,30 @@ + +let (exist 'n, 'n in {0, 1}. [:'n:]) v1 = 0 + +val bool -> exist 'n, 'n in {0, 1}. [:'n:] effect pure test + +function test flag = +{ + if flag then 0 else 1 +} + +let ([|0:1|]) v2 = test(true) + +val forall 'a, 'b. ([:'a:], [:'b:]) -> [:'a + 'b:] effect pure add + +let (exist 'k, 'k in {3, 4}. [:'k:]) v3 = 3 + +let (exist 'q, 'q in {0, 1}. [:'q + 3:]) v4 = v3 + +let v5 = add(test(true), 4) + +let ([:4:]) v6 = 4 + +function unit unit_fn (([:4:]) x) = () + +val forall 'a. ([:'a:], [:'a:]) -> [:'a + 'a:] effect pure s_add + +let (exist 'k, 'k = 4. [:'k:]) v7 = 4 + +let v8 = s_add(v7, 4) + diff --git a/test/typecheck/pass/exist2.sail b/test/typecheck/pass/exist2.sail new file mode 100644 index 00000000..04ccb57b --- /dev/null +++ b/test/typecheck/pass/exist2.sail @@ -0,0 +1,46 @@ + +let (exist 'n, 'n in {0, 1}. [:'n:]) v1 = 0 + +val bool -> exist 'n, 'n in {0, 1}. [:'n:] effect pure test + +function test flag = +{ + if flag then 0 else 1 +} + +let ([|0:1|]) v2 = test(true) + +val forall 'a, 'b. ([:'a:], [:'b:]) -> [:'a + 'b:] effect pure add + +let (exist 'k, 'k in {3, 4}. [:'k:]) v3 = 3 + +let (exist 'q, 'q in {0, 1}. [:'q + 3:]) v4 = v3 + +let v5 = add(test(true), 4) + +let ([:4:]) v6 = 4 + +function unit unit_fn (([:4:]) x) = () + +val forall 'a. ([:'a:], [:'a:]) -> [:'a + 'a:] effect pure s_add + +let (exist 'k, 'k = 4. [:'k:]) v7 = 4 + +(* let v8 = s_add(test(true), 4) *) + +let (exist 'n, 0 = 0. [:'n:]) v9 = 100 + +let (int) v10 = v9 + +typedef Int = exist 'n, 0 = 0. [:'n:] + +val int -> Int effect pure existential_int +val forall 'n, 'm. range<'n,'m> -> exist 'e, 'n <= 'e & 'e <= 'm. [:'e:] effect pure existential_range + +overload existential [existential_int; existential_range] + +let (exist 'n, 0 = 0. [:'n:]) v11 = existential(v10) + +let (exist 'e, 0 <= 'e & 'e <= 3. [:'e:]) v12 = existential(([|0:3|]) 2) + +let (Int) v13 = existential(v10) |