From 1f8aafca4b8d57b4bd9fe29348c06894309d8841 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 10 Apr 2018 14:17:18 +0100 Subject: Porting some minisail changes to sail2 branch This commit primarily changes how existential types are bound in letbindings. Essentially, the constraints on both numeric and existentially quantified types are lifted into the surrounding type context automatically, so in ``` val f : nat -> nat let x = f(3) ``` whereas x would have had type nat by default before, it'll now have type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh type variable). This has several advantages: x can be passed to functions expecting an atom argument, such as a vector indexing operation without any clunky cast functions - ex_int, ex_nat, and ex_range are no longer required. The let 'x = something() syntax is also less needed, and is now only really required when we specifically want a name to refer to x's type. This changes slightly the nature of the type pattern syntax---whereas previously it was used to cause an existential to be destructured, it now just provides names for an automatically destructured binding. Usually however, this just works the same. Also: - Fixed an issue where the rewrite_split_fun_constr_pats rewriting pass didn't add type paramemters for newly added type variables in generated function parameters. - Updated string_of_ functions in ast_util to reflect syntax changes - Fixed a C compilation issue where elements of union type constructors were not being coerced between big integers and 64-bit integers where appropriate - Type annotations in patterns now generalise, rather than restrict the type of the pattern. This should be safer and easier to handle in the various backends. I don't think any code we had was relying on this behaviour anyway. - Add inequality operator to lib/flow.sail - Fix an issue whereby top-level let bindings with annotations were checked incorrectly --- aarch64/no_vector/spec.sail | 4 +- aarch64/prelude.sail | 6 +- lib/flow.sail | 10 ++ mips/prelude.sail | 8 -- src/ast_util.ml | 14 +-- src/c_backend.ml | 34 +++--- src/initial_check.ml | 29 ++--- src/rewrites.ml | 11 +- src/type_check.ml | 132 +++++++++++++---------- test/c/enum_match.sail | 3 +- test/c/run_tests.sh | 2 +- test/typecheck/pass/case_simple_constraints.sail | 17 --- test/typecheck/pass/exist_pattern.sail | 6 +- test/typecheck/pass/exist_synonym/v1.expect | 2 +- test/typecheck/pass/exist_synonym/v2.expect | 2 +- test/typecheck/pass/exist_synonym/v3.expect | 2 +- test/typecheck/pass/exist_synonym/v4.expect | 2 +- test/typecheck/pass/flow_gt1.sail | 44 +------- test/typecheck/pass/flow_gteq1.sail | 44 +------- test/typecheck/pass/flow_lt1.sail | 38 +------ test/typecheck/pass/flow_lt2.sail | 38 +------ test/typecheck/pass/flow_lt_assign.sail | 47 -------- test/typecheck/pass/flow_lteq1.sail | 44 +------- test/typecheck/pass/fun_simple_constraints1.sail | 15 --- test/typecheck/pass/fun_simple_constraints2.sail | 15 --- test/typecheck/pass/global_type_var/v1.expect | 4 +- test/typecheck/pass/global_type_var/v2.expect | 4 +- test/typecheck/pass/guards.sail | 17 +-- 28 files changed, 165 insertions(+), 429 deletions(-) delete mode 100644 test/typecheck/pass/case_simple_constraints.sail delete mode 100644 test/typecheck/pass/flow_lt_assign.sail delete mode 100644 test/typecheck/pass/fun_simple_constraints1.sail delete mode 100644 test/typecheck/pass/fun_simple_constraints2.sail diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail index d8a05777..ccf8aba1 100644 --- a/aarch64/no_vector/spec.sail +++ b/aarch64/no_vector/spec.sail @@ -6984,7 +6984,7 @@ function __TakeColdReset () = { val AArch64_TakeException : (bits(2), ExceptionRecord, bits(64), int) -> unit effect {escape, rreg, undef, wreg} function AArch64_TakeException (target_el, exception, preferred_exception_return, vect_offset__arg) = { - vect_offset = vect_offset__arg; + vect_offset : int = vect_offset__arg; SynchronizeContext(); assert((HaveEL(target_el) & ~(ELUsingAArch32(target_el))) & UInt(target_el) >= UInt(PSTATE.EL), "((HaveEL(target_el) && !(ELUsingAArch32(target_el))) && (UInt(target_el) >= UInt((PSTATE).EL)))"); from_32 : bool = UsingAArch32(); @@ -8507,7 +8507,7 @@ val aarch64_memory_vector_single_nowb : forall ('esize : Int) ('selem : Int). function aarch64_memory_vector_single_nowb (datasize, esize, index, m, memop, n, replicate, selem, t__arg, wback) = { assert(constraint('selem >= 1 & 'esize >= 0)); - t = t__arg; + t : int = t__arg; CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; offs : bits(64) = undefined; diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index 902f448f..5cf4ce48 100644 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -103,10 +103,6 @@ val not_vec = { overload ~ = {not_bool, not_vec} -val neq_int = {lem: "neq"} : (int, int) -> bool - -function neq_int (x, y) = not_bool(eq_int(x, y)) - val neq_vec = {lem: "neq_vec"} : forall 'n. (bits('n), bits('n)) -> bool function neq_vec (x, y) = not_bool(eq_vec(x, y)) @@ -115,7 +111,7 @@ val neq_anything = {lem: "neq"} : forall ('a : Type). ('a, 'a) -> bool function neq_anything (x, y) = not_bool(x == y) -overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} +overload operator != = {neq_vec, neq_anything} val builtin_and_vec = {ocaml: "and_vec", c: "and_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n) diff --git a/lib/flow.sail b/lib/flow.sail index f1f24492..ad5f8760 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -29,12 +29,22 @@ val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm 'o 'p. ( val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : (int, int) -> bool val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool"} : (bool, bool) -> bool +val neq_range = {lem: "neq"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool +function neq_range (x, y) = not_bool(neq_range(x, y)) + +val neq_int = {lem: "neq"} : (int, int) -> bool +function neq_int (x, y) = not_bool(eq_int(x, y)) + +val neq_bool : (bool, bool) -> bool +function neq_bool (x, y) = not_bool(eq_bool(x, y)) + val lteq_int = "lteq" : (int, int) -> bool val gteq_int = "gteq" : (int, int) -> bool val lt_int = "lt" : (int, int) -> bool val gt_int = "gt" : (int, int) -> bool overload operator == = {eq_atom, eq_range, eq_int, eq_bool} +overload operator != = {neq_atom, neq_range, neq_int, neq_bool} overload operator | = {or_bool} overload operator & = {and_bool} diff --git a/mips/prelude.sail b/mips/prelude.sail index b407f5c6..aa81175f 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -202,14 +202,6 @@ infix 8 ^^ val operator ^^ = {lem: "replicate_bits"} : forall 'n 'm . (bits('n), atom('m)) -> bits('n * 'm) function operator ^^ (bs, n) = replicate_bits (bs, n) -val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)} - -function ex_nat 'n = n - -val cast ex_int : int -> {'n, true. atom('n)} - -function ex_int 'n = n - val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) val print_int = "print_int" : (string, int) -> unit diff --git a/src/ast_util.ml b/src/ast_util.ml index 97ce3896..09fc9fc9 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -486,7 +486,7 @@ let def_loc = function let string_of_id = function | Id_aux (Id v, _) -> v - | Id_aux (DeIid v, _) -> "(deinfix " ^ v ^ ")" + | Id_aux (DeIid v, _) -> "(operator " ^ v ^ ")" let id_of_kid = function | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l) @@ -528,7 +528,7 @@ let string_of_base_effect_aux = function let string_of_base_kind_aux = function | BK_type -> "Type" - | BK_nat -> "Nat" + | BK_nat -> "Int" | BK_order -> "Order" let string_of_base_kind (BK_aux (bk, _)) = string_of_base_kind_aux bk @@ -567,11 +567,11 @@ and string_of_typ_aux = function | Typ_id id -> string_of_id id | Typ_var kid -> string_of_kid kid | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")" - | Typ_app (id, args) -> string_of_id id ^ "<" ^ string_of_list ", " string_of_typ_arg args ^ ">" + | Typ_app (id, args) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")" | Typ_fn (typ_arg, typ_ret, eff) -> string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff | Typ_exist (kids, nc, typ) -> - "exist " ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ + "{" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}" and string_of_typ_arg = function | Typ_arg_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg and string_of_typ_arg_aux = function @@ -588,7 +588,7 @@ and string_of_n_constraint = function | NC_aux (NC_and (nc1, nc2), _) -> "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_set (kid, ns), _) -> - string_of_kid kid ^ " IN {" ^ string_of_list ", " Big_int.to_string ns ^ "}" + string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}" | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" @@ -599,7 +599,7 @@ let string_of_annot = function let string_of_quant_item_aux = function | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid - | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> string_of_kind k ^ " " ^ string_of_kid kid + | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> "(" ^ string_of_kid kid ^ " :: " ^ string_of_kind k ^ ")" | QI_const constr -> string_of_n_constraint constr let string_of_quant_item = function @@ -641,7 +641,7 @@ let rec string_of_exp (E_aux (exp, _)) = | E_app_infix (x, op, y) -> "(" ^ string_of_exp x ^ " " ^ string_of_id op ^ " " ^ string_of_exp y ^ ")" | E_tuple exps -> "(" ^ string_of_list ", " string_of_exp exps ^ ")" | E_case (exp, cases) -> - "switch " ^ string_of_exp exp ^ " { case " ^ string_of_list " case " string_of_pexp cases ^ "}" + "match " ^ string_of_exp exp ^ " { " ^ string_of_list ", " string_of_pexp cases ^ " }" | E_try (exp, cases) -> "try " ^ string_of_exp exp ^ " catch { case " ^ string_of_list " case " string_of_pexp cases ^ "}" | E_let (letbind, exp) -> "let " ^ string_of_letbind letbind ^ " in " ^ string_of_exp exp diff --git a/src/c_backend.ml b/src/c_backend.ml index 398a0281..6e1083df 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -168,7 +168,7 @@ and sc_op = SC_and | SC_or and apat = | AP_tup of apat list - | AP_id of id + | AP_id of id * typ | AP_global of id * typ | AP_app of id * apat | AP_cons of apat * apat @@ -202,8 +202,8 @@ let rec frag_rename from_id to_id = function let rec apat_bindings = function | AP_tup apats -> List.fold_left IdSet.union IdSet.empty (List.map apat_bindings apats) - | AP_id id -> IdSet.singleton id - | AP_global (id, typ) -> IdSet.empty + | AP_id (id, _) -> IdSet.singleton id + | AP_global (id, _) -> IdSet.empty | AP_app (id, apat) -> apat_bindings apat | AP_cons (apat1, apat2) -> IdSet.union (apat_bindings apat1) (apat_bindings apat2) | AP_nil -> IdSet.empty @@ -211,8 +211,8 @@ let rec apat_bindings = function let rec apat_rename from_id to_id = function | AP_tup apats -> AP_tup (List.map (apat_rename from_id to_id) apats) - | AP_id id when Id.compare id from_id = 0 -> AP_id to_id - | AP_id id -> AP_id id + | AP_id (id, typ) when Id.compare id from_id = 0 -> AP_id (to_id, typ) + | AP_id (id, typ) -> AP_id (id, typ) | AP_global (id, typ) -> AP_global (id, typ) | AP_app (ctor, apat) -> AP_app (ctor, apat_rename from_id to_id apat) | AP_cons (apat1, apat2) -> AP_cons (apat_rename from_id to_id apat1, apat_rename from_id to_id apat2) @@ -430,7 +430,7 @@ let rec pp_aexp = function and pp_apat = function | AP_wild -> string "_" - | AP_id id -> pp_id id + | AP_id (id, typ) -> pp_annot typ (pp_id id) | AP_global (id, _) -> pp_id id | AP_tup apats -> parens (separate_map (comma ^^ space) pp_apat apats) | AP_app (id, apat) -> pp_id id ^^ parens (pp_apat apat) @@ -484,7 +484,7 @@ let rec split_block = function let rec anf_pat ?global:(global=false) (P_aux (p_aux, (l, _)) as pat) = match p_aux with | P_id id when global -> AP_global (id, pat_typ_of pat) - | P_id id -> AP_id id + | P_id id -> AP_id (id, pat_typ_of pat) | P_wild -> AP_wild | P_tup pats -> AP_tup (List.map (fun pat -> anf_pat ~global:global pat) pats) | P_app (id, [pat]) -> AP_app (id, anf_pat ~global:global pat) @@ -1544,8 +1544,9 @@ let compile_funcall ctx id args typ = (List.rev !setup, final_ctyp, call, !cleanup) let rec compile_match ctx apat cval case_label = + prerr_endline ("Compiling match " ^ Pretty_print_sail.to_string (pp_apat apat) ^ " cval " ^ Pretty_print_sail.to_string (pp_cval cval)); match apat, cval with - | AP_id pid, (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env -> + | AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env -> [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label], [] | AP_global (pid, typ), (frag, ctyp) -> @@ -1558,15 +1559,21 @@ let rec compile_match ctx apat cval case_label = [iconvert (CL_id pid) global_ctyp id ctyp], [] | _ -> c_error "Cannot compile global letbinding" end - | AP_id pid, (frag, ctyp) when is_ct_enum ctyp -> + | AP_id (pid, _), (frag, ctyp) when is_ct_enum ctyp -> begin match Env.lookup_id pid ctx.tc_env with | Unbound -> [idecl ctyp pid; icopy (CL_id pid) (frag, ctyp)], [] | _ -> [ijump (F_op (F_id pid, "!=", frag), CT_bool) case_label], [] end - | AP_id pid, _ -> + | AP_id (pid, typ), _ -> let ctyp = cval_ctyp cval in - let init, cleanup = if is_stack_ctyp ctyp then [], [] else [ialloc ctyp pid], [iclear ctyp pid] in - [idecl ctyp pid] @ init @ [icopy (CL_id pid) cval], cleanup + let id_ctyp = ctyp_of_typ ctx typ in + let init, cleanup = if is_stack_ctyp id_ctyp then [], [] else [ialloc id_ctyp pid], [iclear id_ctyp pid] in + if ctyp_equal id_ctyp ctyp then + [idecl ctyp pid] @ init @ [icopy (CL_id pid) cval], cleanup + else + let gs = gensym () in + let gs_init, gs_cleanup = if is_stack_ctyp ctyp then [], [] else [ialloc ctyp gs], [iclear ctyp gs] in + [idecl id_ctyp pid; idecl ctyp gs] @ init @ gs_init @ [icopy (CL_id gs) cval; iconvert (CL_id pid) id_ctyp gs ctyp] @ gs_cleanup, cleanup | AP_tup apats, (frag, ctyp) -> begin let get_tup n ctyp = (F_field (frag, "ztup" ^ string_of_int n), ctyp) in @@ -2170,6 +2177,7 @@ let rec compile_def ctx = function | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow (pat_ids pat) (anf exp))) in + prerr_endline (Pretty_print_sail.to_string (pp_aexp aexp)); let setup, ctyp, call, cleanup = compile_aexp ctx aexp in let fundef_label = label "fundef_fail_" in let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in @@ -3333,7 +3341,7 @@ let codegen_def ctx def = let lists = List.map (fun ctyp -> codegen_list ctx (unlist ctyp)) lists in let vectors = List.filter is_ct_vector (cdef_ctyps ctx def) in let vectors = List.map (fun ctyp -> codegen_vector ctx (unvector ctyp)) vectors in - (* prerr_endline (Pretty_print_sail.to_string (pp_cdef def)); *) + prerr_endline (Pretty_print_sail.to_string (pp_cdef def)); concat tups ^^ concat lists ^^ concat vectors diff --git a/src/initial_check.ml b/src/initial_check.ml index 75668417..06ee1f65 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -1092,13 +1092,14 @@ let generate_initialize_registers vs_ids (Defs defs) = let generate_enum_functions vs_ids (Defs defs) = let rec gen_enums = function | DEF_type (TD_aux (TD_enum (id, _, elems, _), _)) as enum :: defs -> - let enum_val_spec name typ = - mk_val_spec (VS_val_spec (mk_typschm (mk_typquant []) typ, name, (fun _ -> None), !opt_enum_casts)) + let enum_val_spec name quants typ = + mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, (fun _ -> None), !opt_enum_casts)) in - let enum_range = range_typ (nint 0) (nint (List.length elems - 1)) in + let range_constraint kid = nc_and (nc_lteq (nint 0) (nvar kid)) (nc_lteq (nvar kid) (nint (List.length elems - 1))) in (* Create a function that converts a number to an enum. *) let to_enum = + let kid = mk_kid "e" in let name = append_id id "_of_num" in let pexp n id = let pat = @@ -1117,12 +1118,16 @@ let generate_enum_functions vs_ids (Defs defs) = let range = range_typ (nint 0) (nint (List.length elems - 1)) in if IdSet.mem name vs_ids then [] else - [ enum_val_spec name (function_typ enum_range (mk_typ (Typ_id id)) no_effect); + [ enum_val_spec name + [mk_qi_id BK_nat kid; mk_qi_nc (range_constraint kid)] + (function_typ (atom_typ (nvar kid)) (mk_typ (Typ_id id)) no_effect); mk_fundef [funcl] ] in (* Create a function that converts from an enum to a number. *) let from_enum = + let kid = mk_kid "e" in + let to_typ = mk_typ (Typ_exist ([kid], range_constraint kid, atom_typ (nvar kid))) in let name = prepend_id "num_of_" id in let pexp n id = mk_pexp (Pat_exp (mk_pat (P_id id), mk_lit_exp (L_num (Big_int.of_int n)))) in let funcl = @@ -1132,22 +1137,8 @@ let generate_enum_functions vs_ids (Defs defs) = in if IdSet.mem name vs_ids then [] else - [ enum_val_spec name (function_typ (mk_typ (Typ_id id)) enum_range no_effect); + [ enum_val_spec name [] (function_typ (mk_typ (Typ_id id)) to_typ no_effect); mk_fundef [funcl] ] - (* This is the simple way to generate this function, but the - rewriter and backends are all kinds of broken for function clause - patterns. - let name = prepend_id "num_of_" id in - let funcl n id = - mk_funcl name - (mk_pat (P_id id)) - (mk_lit_exp (L_num (Big_int.of_int n))) - in - if IdSet.mem name vs_ids then [] - else - [ enum_val_spec name (function_typ (mk_typ (Typ_id id)) enum_range no_effect); - mk_fundef (List.mapi funcl elems) ] - *) in enum :: to_enum @ from_enum @ gen_enums defs diff --git a/src/rewrites.ml b/src/rewrites.ml index 80c339e6..7ea0dadc 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1961,15 +1961,23 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) = no_effect funcls in let fun_typ = function_typ args_typ ret_typ eff in + let quant_new_tyvars qis = + let quant_tyvars = List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_quant_item qis) in + let typ_tyvars = tyvars_of_typ fun_typ in + let new_tyvars = KidSet.diff typ_tyvars quant_tyvars in + List.map (mk_qi_id BK_nat) (KidSet.elements new_tyvars) + in let typquant = match typquant with | TypQ_aux (TypQ_tq qis, l) -> let qis = List.filter (fun qi -> KidSet.subset (tyvars_of_quant_item qi) (tyvars_of_typ fun_typ)) qis + @ quant_new_tyvars qis in TypQ_aux (TypQ_tq qis, l) - | _ -> typquant + | _ -> + TypQ_aux (TypQ_tq (List.map (mk_qi_id BK_nat) (KidSet.elements (tyvars_of_typ fun_typ))), l) in let val_spec = VS_aux (VS_val_spec @@ -3216,6 +3224,7 @@ let rewrite_defs_ocaml = [ ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); + ("remove_numeral_pats", rewrite_defs_remove_numeral_pats); ("exp_lift_assign", rewrite_defs_exp_lift_assign); ("top_sort_defs", top_sort_defs); ("constraint", rewrite_constraint); diff --git a/src/type_check.ml b/src/type_check.ml index cc88c159..4b716ba8 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -167,6 +167,11 @@ let string_of_index_sort = function ^ string_of_list " & " (fun (x, y) -> string_of_nexp x ^ " <= " ^ string_of_nexp y) constraints ^ "}" +let is_atom (Typ_aux (typ_aux, _)) = + match typ_aux with + | Typ_app (f, [_]) when string_of_id f = "atom" -> true + | _ -> false + (**************************************************************************) (* 1. Substitutions *) (**************************************************************************) @@ -865,11 +870,13 @@ end = struct let get_constraints env = env.constraints - let add_constraint (NC_aux (_, l) as constr) env = + let add_constraint (NC_aux (nc_aux, l) as constr) env = wf_constraint env constr; begin typ_print ("Adding constraint " ^ string_of_n_constraint constr); - { env with constraints = constr :: env.constraints } + match nc_aux with + | NC_true -> env + | _ -> { env with constraints = constr :: env.constraints } end let get_ret_typ env = env.ret_typ @@ -942,7 +949,6 @@ end = struct } end - let add_typquant (quant : typquant) (env : Env.t) : Env.t = let rec add_quant_item env = function | QI_aux (qi, _) -> add_quant_item_aux env qi @@ -978,6 +984,12 @@ let destruct_exist env typ = Some (List.map snd fresh_kids, nc, typ) | _ -> None +let add_existential kids nc env = + let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in + Env.add_constraint nc env + +let add_typ_vars kids env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids + let is_exist = function | Typ_aux (Typ_exist (_, _, _), _) -> true | _ -> false @@ -986,6 +998,41 @@ let exist_typ constr typ = let fresh_kid = fresh_existential () in mk_typ (Typ_exist ([fresh_kid], constr fresh_kid, typ fresh_kid)) +(** Destructure and canonicalise a numeric type into a list of type + variables, a constraint on those type variables, and an + N-expression that represents that numeric type in the + environment. For example: + - {'n, 'n <= 10. atom('n)} => ['n], 'n <= 10, 'n + - int => ['n], true, 'n (where x is fresh) + - atom('n) => [], true, 'n +**) +let destruct_numeric env typ = + let typ = Env.expand_synonyms env typ in + match destruct_exist env typ, typ with + | Some (kids, nc, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]), _)), _ when string_of_id id = "atom" -> + Some (kids, nc, nexp) + | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]), _) when string_of_id id = "atom" -> + Some ([], nc_true, nexp) + | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _) when string_of_id id = "range" -> + let kid = fresh_existential () in + Some ([kid], nc_and (nc_lteq lo (nvar kid)) (nc_lteq (nvar kid) hi), nvar kid) + | None, Typ_aux (Typ_id id, _) when string_of_id id = "nat" -> + let kid = fresh_existential () in + Some ([kid], nc_lteq (nint 0) (nvar kid), nvar kid) + | None, Typ_aux (Typ_id id, _) when string_of_id id = "int" -> + let kid = fresh_existential () in + Some ([kid], nc_true, nvar kid) + | _, _ -> None + +(** Pull an (potentially)-existentially qualified type into the global + typing environment **) +let bind_existential typ env = + match destruct_numeric env typ with + | Some (kids, nc, nexp) -> atom_typ nexp, add_existential kids nc env + | None -> match destruct_exist env typ with + | Some (kids, nc, typ) -> typ, add_existential kids nc env + | None -> typ, env + let destruct_vector env typ = let destruct_vector' = function | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _); @@ -2432,6 +2479,7 @@ and bind_pat_no_guard env (P_aux (_,(l,_)) as pat) typ = | tpat, env, [] -> tpat, env and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) = + let (Typ_aux (typ_aux, _) as typ), env = bind_existential typ env in typ_print ("Binding " ^ string_of_pat pat ^ " to " ^ string_of_typ typ); let annot_pat pat typ = P_aux (pat, (l, Some (env, typ, no_effect))) in let switch_typ pat typ = match pat with @@ -2458,34 +2506,8 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) | Enum enum -> subtyp l env enum typ; annot_pat (P_id v) typ, env, [] end | P_var (pat, typ_pat) -> - let typ = Env.expand_synonyms env typ in - let kid = Env.fresh_kid env in - let env, ex_typ = match destruct_exist env typ, typ with - | Some (kids, nc, ex_typ), _ -> - let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in - let env = Env.add_constraint nc env in - env, ex_typ - | None, Typ_aux (Typ_id id, _) when string_of_id id = "int" -> - Env.add_typ_var kid BK_nat env, atom_typ (nvar kid) - | None, Typ_aux (Typ_id id, _) when string_of_id id = "nat" -> - let env = Env.add_typ_var kid BK_nat env in - let env = Env.add_constraint (nc_gt (nvar kid) (nint 0)) env in - env, atom_typ (nvar kid) - | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _) - when string_of_id id = "range" -> - let env = Env.add_typ_var kid BK_nat env in - let env = Env.add_constraint (nc_lteq lo (nvar kid)) env in - let env = Env.add_constraint (nc_lteq (nvar kid) hi) env in - env, atom_typ (nvar kid) - | None, Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _)]), _) - when string_of_id id = "atom" -> - let env = Env.add_typ_var kid BK_nat env in - let env = Env.add_constraint (nc_eq (nvar kid) n) env in - env, atom_typ (nvar kid) - | None, _ -> typ_error l ("Cannot bind type variable against non existential or numeric type") - in - let env = bind_typ_pat env typ_pat ex_typ in - let typed_pat, env, guards = bind_pat env pat ex_typ in + let env = bind_typ_pat env typ_pat typ in + let typed_pat, env, guards = bind_pat env pat typ in annot_pat (P_var (typed_pat, typ_pat)) typ, env, guards | P_wild -> annot_pat P_wild typ, env, [] | P_cons (hd_pat, tl_pat) -> @@ -2566,10 +2588,14 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) | P_as (pat, id) -> let (typed_pat, env, guards) = bind_pat env pat typ in annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), Env.add_local id (Immutable, pat_typ_of typed_pat) env, guards + (* This is a special case for flow typing when we match a constant numeric literal. *) + | P_lit (L_aux (L_num n, _) as lit) when is_atom typ -> + let nexp = match destruct_atom_nexp env typ with Some n -> n | None -> assert false in + annot_pat (P_lit lit) (atom_typ (nconstant n)), Env.add_constraint (nc_eq nexp (nconstant n)) env, [] | _ -> let (inferred_pat, env, guards) = infer_pat env pat in - match subtyp l env (pat_typ_of inferred_pat) typ with - | () -> switch_typ inferred_pat typ, env, guards + match subtyp l env typ (pat_typ_of inferred_pat) with + | () -> switch_typ inferred_pat (pat_typ_of inferred_pat), env, guards | exception (Type_error _ as typ_exn) -> match pat_aux with | P_lit lit -> @@ -2979,27 +3005,17 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let inferred_f = irule infer_exp env f in let inferred_t = irule infer_exp env t in let checked_step = crule check_exp env step int_typ in - match destruct_range (typ_of inferred_f), destruct_range (typ_of inferred_t) with - | None, _ -> typ_error l ("Type of " ^ string_of_exp f ^ " in foreach must be a range") - | _, None -> typ_error l ("Type of " ^ string_of_exp t ^ " in foreach must be a range") - (* | Some (l1, l2), Some (u1, u2) when prove env (nc_lteq l2 u1) -> - let loop_vtyp = exist_typ (fun e -> nc_and (nc_lteq l1 (nvar e)) (nc_lteq (nvar e) u2)) (fun e -> atom_typ (nvar e)) in + match destruct_numeric env (typ_of inferred_f), destruct_numeric env (typ_of inferred_t) with + | Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) -> + let loop_kid = mk_kid ("loop_" ^ string_of_id v) in + let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env (loop_kid :: kids1 @ kids2) in + let env = Env.add_constraint (nc_and nc1 nc2) env in + let env = Env.add_constraint (nc_and (nc_lteq nexp1 (nvar loop_kid)) (nc_lteq (nvar loop_kid) nexp2)) env in + let loop_vtyp = atom_typ (nvar loop_kid) in let checked_body = crule check_exp (Env.add_local v (Immutable, loop_vtyp) env) body unit_typ in - annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ *) - | Some (l1, l2), Some (u1, u2) when prove env (nc_lteq l2 u1) -> - let kid = mk_kid ("loop_" ^ string_of_id v) in - if KBindings.mem kid (Env.get_typ_vars env) - then typ_error l "Nested loop variables cannot have the same name" - else - begin - let env = Env.add_typ_var kid BK_nat env in - let env = Env.add_constraint (nc_and (nc_lteq l1 (nvar kid)) (nc_lteq (nvar kid) u2)) env in - let loop_vtyp = atom_typ (nvar kid) in - let checked_body = crule check_exp (Env.add_local v (Immutable, loop_vtyp) env) body unit_typ in - if not is_dec (* undo reverse direction in annoteded ast for downto loop *) - then annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ - else annot_exp (E_for (v, inferred_t, inferred_f, checked_step, ord, checked_body)) unit_typ - end + if not is_dec (* undo reverse direction in annotated ast for downto loop *) + then annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ + else annot_exp (E_for (v, inferred_t, inferred_f, checked_step, ord, checked_body)) unit_typ | _, _ -> typ_error l "Ranges in foreach overlap" end | E_if (cond, then_branch, else_branch) -> @@ -3520,14 +3536,15 @@ and propagate_lexp_effect_aux = function (**************************************************************************) let check_letdef orig_env (LB_aux (letbind, (l, _))) = + typ_print "\nChecking top-level let"; begin match letbind with - | LB_val (P_aux (P_typ (typ_annot, pat), _), bind) -> + | LB_val (P_aux (P_typ (typ_annot, _), _) as pat, bind) -> let checked_bind = propagate_exp_effect (crule check_exp orig_env (strip_exp bind) typ_annot) in let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) typ_annot in if (BESet.is_empty (effect_set (effect_of checked_bind)) || !opt_no_effects) then - [DEF_val (LB_aux (LB_val (P_aux (P_typ (typ_annot, tpat), (l, Some (orig_env, typ_annot, no_effect))), checked_bind), (l, None)))], env + [DEF_val (LB_aux (LB_val (tpat, checked_bind), (l, None)))], env else typ_error l ("Top-level definition with effects " ^ string_of_effect (effect_of checked_bind)) | LB_val (pat, bind) -> let inferred_bind = propagate_exp_effect (irule infer_exp orig_env (strip_exp bind)) in @@ -3650,7 +3667,10 @@ let check_val_spec env (VS_aux (vs, (l, _))) = let (id, quants, typ, env) = match vs with | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _) as typschm, id, ext_opt, is_cast) -> typ_debug ("VS typschm: " ^ string_of_id id ^ ", " ^ string_of_typschm typschm); - let env = match ext_opt "smt" with Some op -> Env.add_smt_op id op env | None -> env in + let env = match (ext_opt "smt", ext_opt "#") with + | Some op, None -> Env.add_smt_op id op env + | _, _ -> env + in Env.wf_typ (add_typquant quants env) typ; typ_debug "CHECKED WELL-FORMED VAL SPEC"; let env = diff --git a/test/c/enum_match.sail b/test/c/enum_match.sail index 591e2695..6c04d9dc 100644 --- a/test/c/enum_match.sail +++ b/test/c/enum_match.sail @@ -1,7 +1,8 @@ val "eq_anything" : forall ('a : Type). ('a, 'a) -> bool +val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm. (atom('n), atom('m)) -> bool -overload operator == = {eq_anything} +overload operator == = {eq_atom, eq_anything} val print = "print_endline" : string -> unit diff --git a/test/c/run_tests.sh b/test/c/run_tests.sh index 930c5bc8..e85881f5 100755 --- a/test/c/run_tests.sh +++ b/test/c/run_tests.sh @@ -75,7 +75,7 @@ do red "compiling $file" "fail" fi; rm -f ${file%.sail}.c - rm -r ${file%.sail}.result + rm -f ${file%.sail}.result done finish_suite "C testing" diff --git a/test/typecheck/pass/case_simple_constraints.sail b/test/typecheck/pass/case_simple_constraints.sail deleted file mode 100644 index 66fc0025..00000000 --- a/test/typecheck/pass/case_simple_constraints.sail +++ /dev/null @@ -1,17 +0,0 @@ -val plus = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int). - (atom('n + 20), atom('m)) -> atom('n + 20 + 'm) - -val minus_ten_id = {ocaml: "id", lem: "id"}: forall ('n : Int), 'n <= -10. - atom('n) -> atom('n) - -val ten_id = {ocaml: "id", lem: "id"}: forall ('n : Int), 'n >= 10. - atom('n) -> atom('n) - -val branch : forall ('N : Int), 'N >= 63. range(10, 'N) -> range(10, 'N) - -function branch x = match x { - y : range(10, 30) => y, - _ : atom(31) => 'N, - _ : range(31, 40) => plus(60, 3) -} -and branch _ : range(51, 63) = ten_id('N) diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail index 178f8003..47343e02 100644 --- a/test/typecheck/pass/exist_pattern.sail +++ b/test/typecheck/pass/exist_pattern.sail @@ -41,9 +41,9 @@ function main () = { } }; match word { - 8 : range(0, 8) => x = 32, - 16 : range(0, 16) => x = 64, - 32 : range(0, 32) => x = 128 + 8 => x = 32, + 16 => x = 64, + 32 => x = 128 }; match 0b010101 { 0b01 @ _ : vector(1, inc, bit) @ 0b101 => n = 42, diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect index 8ecba308..c2f05f5c 100644 --- a/test/typecheck/pass/exist_synonym/v1.expect +++ b/test/typecheck/pass/exist_synonym/v1.expect @@ -3,4 +3,4 @@ Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, char let x : {'n, 0 <= 'n <= 33. regno('n)} = 4 Tried performing type coercion on 4 -Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom<'n> with (0 <= 'n & 'n <= 33) +Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 'n & 'n <= 33) diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect index 09bba469..5926bcdb 100644 --- a/test/typecheck/pass/exist_synonym/v2.expect +++ b/test/typecheck/pass/exist_synonym/v2.expect @@ -3,4 +3,4 @@ Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, char let x : {'n, 0 <= 'n <= 8. regno('n)} = 4 Tried performing type coercion on 4 -Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym atom<'n> with (0 <= 'n & 'n <= 8) +Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym atom('n) with (0 <= 'n & 'n <= 8) diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect index be1a92a1..c41f2c4b 100644 --- a/test/typecheck/pass/exist_synonym/v3.expect +++ b/test/typecheck/pass/exist_synonym/v3.expect @@ -1,3 +1,3 @@ Type error at no location information available -Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom<'n> with (0 <= 'n & 'n <= 100) +Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 'n & 'n <= 100), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 8) diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect index 13edc200..a17ed112 100644 --- a/test/typecheck/pass/exist_synonym/v4.expect +++ b/test/typecheck/pass/exist_synonym/v4.expect @@ -1,3 +1,3 @@ Type error at no location information available -Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom<'n> with (0 <= 2 & 2 <= 4) +Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 2 & 2 <= 4), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 8) diff --git a/test/typecheck/pass/flow_gt1.sail b/test/typecheck/pass/flow_gt1.sail index 47b26261..19336fd5 100644 --- a/test/typecheck/pass/flow_gt1.sail +++ b/test/typecheck/pass/flow_gt1.sail @@ -1,46 +1,6 @@ -default Order inc +default Order dec -val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -overload operator + = {add_range} - -overload operator - = {sub_range} - -overload operator < = {lt_atom_range, lt_range_atom} - -overload operator <= = {lteq_atom_range, lteq_range_atom} - -overload operator > = {gt_atom_range, gt_range_atom} - -overload operator >= = {gteq_atom_range, gteq_range_atom} +$include val branch : range(0, 63) -> range(0, 63) diff --git a/test/typecheck/pass/flow_gteq1.sail b/test/typecheck/pass/flow_gteq1.sail index 3ea9d69b..f985cc09 100644 --- a/test/typecheck/pass/flow_gteq1.sail +++ b/test/typecheck/pass/flow_gteq1.sail @@ -1,46 +1,6 @@ -default Order inc +default Order dec -val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -overload operator + = {add_range} - -overload operator - = {sub_range} - -overload operator < = {lt_atom_range, lt_range_atom} - -overload operator <= = {lteq_atom_range, lteq_range_atom} - -overload operator > = {gt_atom_range, gt_range_atom} - -overload operator >= = {gteq_atom_range, gteq_range_atom} +$include val branch : range(0, 63) -> range(0, 63) diff --git a/test/typecheck/pass/flow_lt1.sail b/test/typecheck/pass/flow_lt1.sail index e29424be..0dc6dc98 100644 --- a/test/typecheck/pass/flow_lt1.sail +++ b/test/typecheck/pass/flow_lt1.sail @@ -1,40 +1,6 @@ -default Order inc +default Order dec -val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -overload operator + = {add_range} - -overload operator - = {sub_range} - -overload operator < = {lt_atom_range, lt_range_atom} +$include val branch : range(0, 63) -> range(0, 63) diff --git a/test/typecheck/pass/flow_lt2.sail b/test/typecheck/pass/flow_lt2.sail index 2c1ad667..3101c608 100644 --- a/test/typecheck/pass/flow_lt2.sail +++ b/test/typecheck/pass/flow_lt2.sail @@ -1,40 +1,6 @@ -default Order inc +default Order dec -val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -overload operator + = {add_range} - -overload operator - = {sub_range} - -overload operator < = {lt_atom_range, lt_range_atom} +$include val branch : range(0, 63) -> range(0, 63) diff --git a/test/typecheck/pass/flow_lt_assign.sail b/test/typecheck/pass/flow_lt_assign.sail deleted file mode 100644 index afc620b6..00000000 --- a/test/typecheck/pass/flow_lt_assign.sail +++ /dev/null @@ -1,47 +0,0 @@ -default Order inc - -val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -overload operator + = {add_range} - -overload operator - = {sub_range} - -overload operator < = {lt_atom_range, lt_range_atom} - -val branch : range(0, 63) -> range(0, 63) - -function branch x = { - y = x; - if y < 32 then { - y = 31; - y + 32 - } else y - 32 -} diff --git a/test/typecheck/pass/flow_lteq1.sail b/test/typecheck/pass/flow_lteq1.sail index c61f93e2..30486c7e 100644 --- a/test/typecheck/pass/flow_lteq1.sail +++ b/test/typecheck/pass/flow_lteq1.sail @@ -1,45 +1,5 @@ -default Order inc +default Order dec -val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -overload operator + = {add_range} - -overload operator - = {sub_range} - -overload operator < = {lt_atom_range, lt_range_atom} - -overload operator <= = {lteq_atom_range, lteq_range_atom} - -overload operator > = {gt_atom_range, gt_range_atom} - -overload operator >= = {gteq_atom_range, gteq_range_atom} +$include function branch x : range(0, 63) -> range(0, 63) = if x <= 32 then x + 31 else x - 33 diff --git a/test/typecheck/pass/fun_simple_constraints1.sail b/test/typecheck/pass/fun_simple_constraints1.sail deleted file mode 100644 index 2731c2b9..00000000 --- a/test/typecheck/pass/fun_simple_constraints1.sail +++ /dev/null @@ -1,15 +0,0 @@ -val plus : forall ('n : Int) ('m : Int). - (atom('n + 20), atom('m)) -> atom('n + 20 + 'm) - -val minus_ten_id : forall ('n : Int), 'n <= -10. atom('n) -> atom('n) - -val ten_id : forall ('n : Int), 'n >= 10. atom('n) -> atom('n) - -val branch : forall ('N : Int), 'N >= 63. range(10, 'N) -> range(10, 'N) - -function branch x = x -and branch y : range(10, 30) = y -and branch _ : atom(31) = 'N -and branch _ : range(31, 40) = plus(60, 3) -and branch _ : range(41, 50) = plus('N, minus_ten_id(-53)) -and branch _ : range(51, 63) = ten_id('N) diff --git a/test/typecheck/pass/fun_simple_constraints2.sail b/test/typecheck/pass/fun_simple_constraints2.sail deleted file mode 100644 index b6c4eef5..00000000 --- a/test/typecheck/pass/fun_simple_constraints2.sail +++ /dev/null @@ -1,15 +0,0 @@ -val plus : forall ('n : Int) ('m : Int). - (atom('n + 20), atom('m)) -> atom('n + 20 + 'm) - -val minus_ten_id : forall ('n : Int), 'n <= -10. range('n, 'n) -> atom('n) - -val ten_id : forall ('n : Int), 'n >= 10. atom('n) -> atom('n) - -val branch : forall ('N : Int), 'N >= 63. range(10, 'N) -> range(10, 'N) - -function branch x = x -and branch y : range(10, 30) = y -and branch _ : atom(31) = 'N -and branch _ : range(31, 40) = plus(60, 3) -and branch _ : range(41, 50) = plus('N, minus_ten_id(-53)) -and branch _ : range(51, 63) = ten_id('N) diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect index c421cada..d80cb349 100644 --- a/test/typecheck/pass/global_type_var/v1.expect +++ b/test/typecheck/pass/global_type_var/v1.expect @@ -3,4 +3,6 @@ Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23, let _ = test(32) Tried performing type coercion on 32 -Failed because atom<32> is not a subtype of atom<'size> in context 'size = 'ex1#, ('ex1# = 32 | 'ex1# = 64) +Failed because + atom(32) is not a subtype of atom('size) + in context 'size = 'ex6#, ('ex6# = 32 | 'ex6# = 64), ('ex5# = 32 | 'ex5# = 64) diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect index 8539ea0f..740c1e2e 100644 --- a/test/typecheck/pass/global_type_var/v2.expect +++ b/test/typecheck/pass/global_type_var/v2.expect @@ -3,4 +3,6 @@ Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23, let _ = test(64) Tried performing type coercion on 64 -Failed because atom<64> is not a subtype of atom<'size> in context 'size = 'ex1#, ('ex1# = 32 | 'ex1# = 64) +Failed because + atom(64) is not a subtype of atom('size) + in context 'size = 'ex6#, ('ex6# = 32 | 'ex6# = 64), ('ex5# = 32 | 'ex5# = 64) diff --git a/test/typecheck/pass/guards.sail b/test/typecheck/pass/guards.sail index 9fc753e6..4aac2bed 100644 --- a/test/typecheck/pass/guards.sail +++ b/test/typecheck/pass/guards.sail @@ -1,19 +1,6 @@ -infix 4 == -infixl 6 / +default Order dec -val add_int : (int, int) -> int - -overload operator + = {add_int} - -val eq : forall ('a : Type). ('a, 'a) -> bool - -val neq : forall ('a : Type). ('a, 'a) -> bool - -overload operator == = {eq} - -overload operator != = {neq} - -val quotient : (int, int) -> int +$include overload operator / = {quotient} -- cgit v1.2.3