From 3a0e9d3344d113154a9144310b094a2e6a52efda Mon Sep 17 00:00:00 2001 From: Alasdair Date: Mon, 13 May 2024 00:14:16 +0100 Subject: [PATCH 1/2] Infer slightly more types in mapping patterns --- src/lib/type_check.ml | 115 ++++++++++++------ test/c/encdec_subrange.expect | 4 + test/c/encdec_subrange.sail | 31 +++++ .../fail/encdec_unknown_and_error.expect | 10 ++ .../fail/encdec_unknown_and_error.sail | 14 +++ 5 files changed, 137 insertions(+), 37 deletions(-) create mode 100644 test/c/encdec_subrange.expect create mode 100644 test/c/encdec_subrange.sail create mode 100644 test/typecheck/fail/encdec_unknown_and_error.expect create mode 100644 test/typecheck/fail/encdec_unknown_and_error.sail diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index 9b9a364ca..94c649778 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -1933,11 +1933,21 @@ let tc_assume nc (E_aux (aux, annot)) = E_aux (E_internal_assume (nc, E_aux (aux type ('a, 'b) pattern_functions = { infer : Env.t -> 'a -> 'b * Env.t * uannot exp list; bind : Env.t -> 'a -> typ -> 'b * Env.t * uannot exp list; + strip : 'b -> 'a; typ_of : 'b -> typ; get_loc : 'a -> l; get_loc_typed : 'b -> l; } +type ('a, 'b) vector_concat_elem = VC_elem_ok of 'a | VC_elem_error of 'b * exn | VC_elem_unknown of 'a + +let unwrap_vector_concat_elem ~at:l = function + | VC_elem_ok x -> x + | VC_elem_unknown x -> x + | VC_elem_error _ -> Reporting.unreachable l __POS__ "Tried to unwrap VC_elem_error" + +let vector_concat_elem_is_ok = function VC_elem_ok _ -> true | _ -> false + module PC_config = struct type t = tannot let typ_of_t = typ_of_tannot @@ -2748,17 +2758,17 @@ and bind_vector_concat_generic : let typ_opt = Option.bind typ_opt (fun typ -> match destruct_any_vector_typ l env typ with - | Destruct_vector (len, elem_typ) -> Option.map (fun l -> (l, Some elem_typ)) (solve_unique env len) - | Destruct_bitvector len -> Option.map (fun l -> (l, None)) (solve_unique env len) + | Destruct_vector (len, elem_typ) -> Option.map (fun len -> (len, Some elem_typ)) (solve_unique env len) + | Destruct_bitvector len -> Option.map (fun len -> (len, None)) (solve_unique env len) ) in (* Try to infer any subpatterns, skipping those we cannot infer *) let fold_pats (pats, env, guards) pat = - let wrap_some (x, y, z) = (Ok x, y, z) in + let wrap_ok (x, y, z) = (VC_elem_ok x, y, z) in let inferred_pat, env, guards' = - if Option.is_none typ_opt then wrap_some (funcs.infer env pat) - else (try wrap_some (funcs.infer env pat) with Type_error _ as exn -> (Error (pat, exn), env, [])) + if Option.is_none typ_opt then wrap_ok (funcs.infer env pat) + else (try wrap_ok (funcs.infer env pat) with Type_error _ as exn -> (VC_elem_error (pat, exn), env, [])) in (inferred_pat :: pats, env, guards' @ guards) in @@ -2766,22 +2776,32 @@ and bind_vector_concat_generic : let inferred_pats = List.rev inferred_pats in (* If we are checking a mapping we can have unknown types, in this - case we can't continue, so just give the entire vector concat an - unknown type. *) - let have_unknown = - allow_unknown - && List.exists (function Ok pat -> is_unknown_type (funcs.typ_of pat) | Error _ -> false) inferred_pats + case we can't continue if there is more than a single unknown, so + just give the entire vector concat an unknown type. *) + let inferred_pats = + if allow_unknown then + List.map + (function + | VC_elem_ok pat -> if is_unknown_type (funcs.typ_of pat) then VC_elem_unknown pat else VC_elem_ok pat + | err -> err + ) + inferred_pats + else inferred_pats in - if have_unknown && List.for_all Result.is_ok inferred_pats then - (annotate (List.map Result.get_ok inferred_pats) unknown_typ, env, guards) + let num_unknowns = List.length (List.filter (function VC_elem_unknown _ -> true | _ -> false) inferred_pats) in + if num_unknowns > 1 || (num_unknowns > 0 && Option.is_none typ_opt) then ( + match Util.option_first (function VC_elem_error (_, exn) -> Some exn | _ -> None) inferred_pats with + | Some exn -> raise exn + | None -> (annotate (List.map (unwrap_vector_concat_elem ~at:l) inferred_pats) unknown_typ, env, guards) + ) else ( (* Will be none if the subpatterns are bitvectors *) let elem_typ = match typ_opt with | Some (_, elem_typ) -> elem_typ | None -> ( - match List.find_opt Result.is_ok inferred_pats with - | Some (Ok pat) -> begin + match List.find_opt vector_concat_elem_is_ok inferred_pats with + | Some (VC_elem_ok pat) -> begin match destruct_any_vector_typ l env (funcs.typ_of pat) with | Destruct_vector (_, t) -> Some t | Destruct_bitvector _ -> None @@ -2790,32 +2810,43 @@ and bind_vector_concat_generic : ) in - (* We can handle a single None in inferred_pats from something like + (* We can handle a single uninferred element (treating unknown + elements as uninferred) in inferred_pats from something like 0b00 @ _ @ 0b00, because we know the wildcard will be bits('n - 4) where 'n is the total length of the pattern. *) - let before_uninferred, rest = Util.take_drop Result.is_ok inferred_pats in - let before_uninferred = List.map Result.get_ok before_uninferred in + let before_uninferred, rest = Util.take_drop vector_concat_elem_is_ok inferred_pats in + let before_uninferred = List.map (unwrap_vector_concat_elem ~at:l) before_uninferred in let uninferred, after_uninferred = + (* When we encounter an unknown or uninferred pattern, check the rest for a second 'bad' + pattern that is also unknown or uninferred *) + let check_rest ~first_bad rest = + let msg = + "Cannot infer width here, as there are multiple subpatterns with unclear width in vector concatenation \ + pattern" + in + match List.find_opt (fun elem -> not (vector_concat_elem_is_ok elem)) rest with + | Some (VC_elem_error (second_bad, _)) -> + typ_raise (funcs.get_loc second_bad) + (err_because (Err_other msg, first_bad, Err_other "A previous subpattern is here")) + | Some (VC_elem_unknown second_bad) -> + typ_raise + (funcs.get_loc (funcs.strip second_bad)) + (err_because (Err_other msg, first_bad, Err_other "A previous subpattern is here")) + | _ -> () + in match rest with - | Error (first_uninferred, exn) :: rest -> - begin - match List.find_opt Result.is_error rest with - | Some (Error (second_uninferred, _)) -> - let msg = - "Cannot infer width here, as there are multiple subpatterns with unclear width in vector \ - concatenation pattern" - in - typ_raise (funcs.get_loc second_uninferred) - (err_because - (Err_other msg, funcs.get_loc first_uninferred, Err_other "A previous subpattern is here") - ) - | _ -> () - end; - begin - match typ_opt with - | Some (total_len, _) -> (Some (total_len, first_uninferred), List.map Result.get_ok rest) - | None -> raise exn - end + | VC_elem_error (first_uninferred, exn) :: rest -> begin + check_rest ~first_bad:(funcs.get_loc first_uninferred) rest; + match typ_opt with + | Some (total_len, _) -> (Some (total_len, first_uninferred), List.map (unwrap_vector_concat_elem ~at:l) rest) + | None -> raise exn + end + | VC_elem_unknown first_unknown :: rest -> + let first_unknown = funcs.strip first_unknown in + check_rest ~first_bad:(funcs.get_loc first_unknown) rest; + (* If we have unknown elems, we check above that the typ_opt is Some _ *) + let total_len = fst (Option.get typ_opt) in + (Some (total_len, first_unknown), List.map (unwrap_vector_concat_elem ~at:l) rest) | _ -> (None, []) in @@ -2876,7 +2907,16 @@ and bind_vector_concat_generic : and bind_vector_concat_pat l env uannot pat pats typ_opt = let annot_vcp pats typ = P_aux (P_vector_concat pats, (l, mk_tannot ~uannot env typ)) in - let funcs = { infer = infer_pat; bind = bind_pat; typ_of = typ_of_pat; get_loc = pat_loc; get_loc_typed = pat_loc } in + let funcs = + { + infer = infer_pat; + bind = bind_pat; + strip = strip_pat; + typ_of = typ_of_pat; + get_loc = pat_loc; + get_loc_typed = pat_loc; + } + in bind_vector_concat_generic funcs annot_vcp l false env pat pats typ_opt and bind_vector_concat_mpat l allow_unknown other_env env uannot mpat mpats typ_opt = @@ -2885,6 +2925,7 @@ and bind_vector_concat_mpat l allow_unknown other_env env uannot mpat mpats typ_ { infer = infer_mpat allow_unknown other_env; bind = bind_mpat allow_unknown other_env; + strip = strip_mpat; typ_of = typ_of_mpat; get_loc = mpat_loc; get_loc_typed = mpat_loc; diff --git a/test/c/encdec_subrange.expect b/test/c/encdec_subrange.expect new file mode 100644 index 000000000..09282999d --- /dev/null +++ b/test/c/encdec_subrange.expect @@ -0,0 +1,4 @@ +x = 0xFFFC03FF +x = 0xF0000000 +x = 0xFAB00000 +ok diff --git a/test/c/encdec_subrange.sail b/test/c/encdec_subrange.sail new file mode 100644 index 000000000..37dae0950 --- /dev/null +++ b/test/c/encdec_subrange.sail @@ -0,0 +1,31 @@ +default Order dec + +$include + +scattered union instr + +val encdec : instr <-> bits(32) + +scattered mapping encdec + +union clause instr = X : bits(21) + +mapping clause encdec = X(imm20 @ 0b0) + <-> 0xF @ imm20[9..0] @ 0x00 @ imm20[19..10] + +val main : unit -> unit + +function main() = { + let x = encdec(X(0xFFFFF @ 0b0)); + print_bits("x = ", x); + let x = encdec(X(0x00000 @ 0b0)); + print_bits("x = ", x); + let x = encdec(X(0b00 @ 0x00AB @ 0b00 @ 0b0)); + print_bits("x = ", x); + + match encdec(0xFFFC03FF) { + X(y) => assert(y == 0xFFFFF @ 0b0), + }; + + print_endline("ok"); +} \ No newline at end of file diff --git a/test/typecheck/fail/encdec_unknown_and_error.expect b/test/typecheck/fail/encdec_unknown_and_error.expect new file mode 100644 index 000000000..a0d5f336e --- /dev/null +++ b/test/typecheck/fail/encdec_unknown_and_error.expect @@ -0,0 +1,10 @@ +Type error: +fail/encdec_unknown_and_error.sail:13.30-31: +13 |mapping clause encdec = X(y @ x @ Z() : bits(1)) +  | ^ +  | Cannot infer width here, as there are multiple subpatterns with unclear width in vector concatenation pattern +  | +  | Caused by fail/encdec_unknown_and_error.sail:13.26-27: +  | 13 |mapping clause encdec = X(y @ x @ Z() : bits(1)) +  |  | ^ +  |  | A previous subpattern is here diff --git a/test/typecheck/fail/encdec_unknown_and_error.sail b/test/typecheck/fail/encdec_unknown_and_error.sail new file mode 100644 index 000000000..cdc139a89 --- /dev/null +++ b/test/typecheck/fail/encdec_unknown_and_error.sail @@ -0,0 +1,14 @@ +default Order dec + +$include + +scattered union instr + +val encdec : instr <-> bits(32) + +scattered mapping encdec + +union clause instr = X : bits(21) + +mapping clause encdec = X(y @ x @ Z() : bits(1)) + <-> 0xF @ x @ 0x00 @ y From 4c323bd4a11c131acf51a28616d31c3fc541bc31 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Mon, 13 May 2024 03:05:50 +0100 Subject: [PATCH 2/2] Fix some mapping issues and add additional tests Make sure variables on both sides of mappings are the same type. --- src/lib/type_check.ml | 115 ++++++++++++++---- src/lib/type_env.mli | 1 + src/lib/type_error.ml | 3 + src/lib/type_error.mli | 1 + src/lib/type_internal.ml | 1 + .../fail/mapping_length_mismatch.expect | 13 ++ .../fail/mapping_length_mismatch.sail | 9 ++ test/typecheck/fail/poly_ab_mapping.expect | 13 ++ test/typecheck/fail/poly_ab_mapping.sail | 9 ++ test/typecheck/pass/bool_mapping.sail | 13 ++ test/typecheck/pass/bool_mapping2.sail | 13 ++ 11 files changed, 170 insertions(+), 21 deletions(-) create mode 100644 test/typecheck/fail/mapping_length_mismatch.expect create mode 100644 test/typecheck/fail/mapping_length_mismatch.sail create mode 100644 test/typecheck/fail/poly_ab_mapping.expect create mode 100644 test/typecheck/fail/poly_ab_mapping.sail create mode 100644 test/typecheck/pass/bool_mapping.sail create mode 100644 test/typecheck/pass/bool_mapping2.sail diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index 94c649778..e27dc4c51 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -1605,18 +1605,95 @@ let check_pattern_duplicates env pat = !subrange_ids; !ids -(* Test that the output of two calls to check pattern duplicates refer to the same identifiers *) -let same_bindings env lhs rhs = - match Bindings.find_first_opt (fun id -> not (Bindings.mem id rhs)) lhs with - | Some (id, _) -> - typ_error (id_loc id) ("Identifier " ^ string_of_id id ^ " found on left hand side of mapping, but not on right") - | None -> ( - match Bindings.find_first_opt (fun id -> not (Bindings.mem id lhs)) rhs with - | Some (id, _) -> - typ_error (id_loc id) - ("Identifier " ^ string_of_id id ^ " found on right hand side of mapping, but not on left") - | None -> () +(* This function checks if a type from one side of a mapping is the + same as a type from the other side of the mapping. Types from one + side of the mapping will have been checked in a different + environment, so we have to take the root environment used to create + both sides environments and carefully transfer unshared constraints + from one child environment to the other, before we can do the + type equality check. *) +let check_mapping_typ_equality ~root_env ~other_env ~env ~other_typ ~typ = + let kopt_arg (KOpt_aux (KOpt_kind (K_aux (k, _), v), _)) = + match k with K_int -> arg_nexp (nvar v) | K_bool -> arg_bool (nc_var v) | K_type -> arg_typ (mk_typ (Typ_var v)) + in + let shared_vars = Env.get_typ_vars root_env in + let other_vars = KBindings.filter (fun v _ -> not (KBindings.mem v shared_vars)) (Env.get_typ_vars other_env) in + let substs = + KBindings.mapi + (fun v k -> + let fresh = Env.fresh_kid ~kid:v env in + mk_kopt k fresh + ) + other_vars + in + let new_vars = KBindings.fold (fun _ subst set -> KidSet.add (kopt_kid subst) set) substs KidSet.empty in + let env = KBindings.fold (fun _ subst env -> Env.add_typ_var Parse_ast.Unknown subst env) substs env in + let env = + List.fold_left + (fun env nc -> + let nc = KBindings.fold (fun v subst nc -> constraint_subst v (kopt_arg subst) nc) substs nc in + Env.add_constraint nc env + ) + env (Env.get_constraints other_env) + in + let other_typ = KBindings.fold (fun v subst typ -> typ_subst v (kopt_arg subst) typ) substs other_typ in + let goals = KidSet.filter (fun k -> KidSet.mem k new_vars) (tyvars_of_typ other_typ) in + let unifiers = unify Parse_ast.Unknown env goals other_typ typ in + let env = + KBindings.fold + (fun v arg env -> + match arg with + | A_aux (A_nexp n, _) -> Env.add_constraint (nc_eq (nvar v) n) env + | A_aux (A_bool nc, _) -> + Env.add_constraint (nc_or (nc_and (nc_var v) nc) (nc_and (nc_not (nc_var v)) (nc_not nc))) env + | A_aux (A_typ _, _) -> env + ) + unifiers env + in + typ_equality Parse_ast.Unknown env other_typ typ + +(* Test that the output of two calls to check pattern duplicates refer + to the same identifiers, and that those identifiers have the same + types. *) +let same_bindings ~at:l ~env ~left_env ~right_env lhs rhs = + let get_loc = function Pattern_singleton l -> l | Pattern_duplicate (l, _) -> l in + Bindings.iter + (fun id left -> + match Bindings.find_opt id rhs with + | Some right -> + let left_lvar = Env.lookup_id id left_env in + let right_lvar = Env.lookup_id id right_env in + if not (is_unbound left_lvar || is_unbound right_lvar) then ( + let left_typ = lvar_typ left_lvar in + let right_typ = lvar_typ right_lvar in + let mapping_type_mismatch err = + typ_raise l + (Err_inner + ( Err_other + (Printf.sprintf "'%s' must have the same type on both sides of the mapping" (string_of_id id)), + Hint ("has type " ^ string_of_typ left_typ, get_loc left, get_loc right), + "", + Err_with_hint ("has type " ^ string_of_typ right_typ, err) + ) + ) + in + try + check_mapping_typ_equality ~root_env:env ~other_env:left_env ~env:right_env ~other_typ:left_typ + ~typ:right_typ + with + | Unification_error (_, m) -> mapping_type_mismatch (Err_other m) + | Type_error (_, err) -> mapping_type_mismatch err + ) + | None -> + typ_error (get_loc left) + ("Identifier " ^ string_of_id id ^ " found on left hand side of mapping, but not on right") ) + lhs; + match Bindings.find_first_opt (fun id -> not (Bindings.mem id lhs)) rhs with + | Some (id, right) -> + typ_error (get_loc right) + ("Identifier " ^ string_of_id id ^ " found on right hand side of mapping, but not on left") + | None -> () let bitvector_typ_from_range l env n m = let len = @@ -3858,11 +3935,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, uannot)) as mpa let unifiers = unify l env (tyvars_of_typ ret_typ) ret_typ typ in let arg_typ' = subst_unifiers unifiers arg_typ in let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in - if not (List.for_all (solve_quant env) quants') then - typ_raise l - (Err_unresolved_quants - (f, quants', Env.get_locals env, Env.get_typ_vars_info env, Env.get_constraints env) - ); + let env = Env.add_typquant l (mk_typquant quants') env in let _ret_typ' = subst_unifiers unifiers ret_typ in let tpats, env, guards = try List.fold_left2 bind_tuple_mpat ([], env, []) mpats (untuple arg_typ') @@ -4166,14 +4239,14 @@ let check_mapcl env (MCL_aux (cl, (def_annot, _))) typ = | MCL_bidir (left_mpexp, right_mpexp) -> begin let left_mpat, _, _ = destruct_mpexp left_mpexp in let left_dups = check_pattern_duplicates env (pat_of_mpat left_mpat) in - let left_id_env = find_types env left_mpat typ1 in + let left_env = find_types env left_mpat typ1 in let right_mpat, _, _ = destruct_mpexp right_mpexp in let right_dups = check_pattern_duplicates env (pat_of_mpat right_mpat) in - same_bindings env left_dups right_dups; - let right_id_env = find_types env right_mpat typ2 in + let right_env = find_types env right_mpat typ2 in + same_bindings ~at:def_annot.loc ~env ~left_env ~right_env left_dups right_dups; - let typed_left_mpexp = check_mpexp right_id_env env left_mpexp typ1 in - let typed_right_mpexp = check_mpexp left_id_env env right_mpexp typ2 in + let typed_left_mpexp = check_mpexp right_env env left_mpexp typ1 in + let typed_right_mpexp = check_mpexp left_env env right_mpexp typ2 in MCL_aux (MCL_bidir (typed_left_mpexp, typed_right_mpexp), (def_annot, mk_expected_tannot env typ (Some typ))) end | MCL_forwards pexp -> begin diff --git a/src/lib/type_env.mli b/src/lib/type_env.mli index 5bf1951fb..9834bff0c 100644 --- a/src/lib/type_env.mli +++ b/src/lib/type_env.mli @@ -115,6 +115,7 @@ val with_global_scope : t -> t * module_state val restore_scope : module_state -> t -> t +val fresh_kid : ?kid:kid -> env -> kid val freshen_bind : t -> typquant * typ -> typquant * typ val get_default_order : t -> order diff --git a/src/lib/type_error.ml b/src/lib/type_error.ml index cfc2d84b7..3fb6e7635 100644 --- a/src/lib/type_error.ml +++ b/src/lib/type_error.ml @@ -292,6 +292,9 @@ let message_of_type_error type_error = in let rec to_message = function | Err_hint h -> (Seq [], Some h) + | Err_with_hint (h, err) -> + let msg, _ = to_message err in + (msg, Some h) | Err_inner (err, l', prefix, err') -> let prefix = if prefix = "" then "" else Util.(prefix ^ " " |> yellow |> clear) in let msg, hint = to_message err in diff --git a/src/lib/type_error.mli b/src/lib/type_error.mli index 1aed09883..dcfbf5302 100644 --- a/src/lib/type_error.mli +++ b/src/lib/type_error.mli @@ -108,6 +108,7 @@ type type_error = (** Takes the name of the identifier, the set of local bindings, and whether we have a function of the same name in scope. *) | Err_hint of string (** A short error that only appears attached to a location *) + | Err_with_hint of string * type_error exception Type_error of Parse_ast.l * type_error diff --git a/src/lib/type_internal.ml b/src/lib/type_internal.ml index 373fb0f71..563a49e38 100644 --- a/src/lib/type_internal.ml +++ b/src/lib/type_internal.ml @@ -112,6 +112,7 @@ type type_error = | Err_no_function_type of { id : id; functions : (typquant * typ) Bindings.t } | Err_unbound_id of { id : id; locals : (mut * typ) Bindings.t; have_function : bool } | Err_hint of string + | Err_with_hint of string * type_error let err_because (error1, l, error2) = Err_inner (error1, l, "Caused by", error2) diff --git a/test/typecheck/fail/mapping_length_mismatch.expect b/test/typecheck/fail/mapping_length_mismatch.expect new file mode 100644 index 000000000..a7b02d6b8 --- /dev/null +++ b/test/typecheck/fail/mapping_length_mismatch.expect @@ -0,0 +1,13 @@ +Type error: +fail/mapping_length_mismatch.sail:9.21-48: +9 |mapping clause foo = x : bits(1) <-> x : bits(2) +  | ^-------------------------^ +  | 'x' must have the same type on both sides of the mapping +  | +  | fail/mapping_length_mismatch.sail:9.21-22: +  | 9 |mapping clause foo = x : bits(1) <-> x : bits(2) +  |  | ^ has type bits(1) +  | fail/mapping_length_mismatch.sail:9.37-38: +  | 9 |mapping clause foo = x : bits(1) <-> x : bits(2) +  |  | ^ has type bits(2) +  |  | Integer expressions 1 and 2 are not equal diff --git a/test/typecheck/fail/mapping_length_mismatch.sail b/test/typecheck/fail/mapping_length_mismatch.sail new file mode 100644 index 000000000..831fa58c3 --- /dev/null +++ b/test/typecheck/fail/mapping_length_mismatch.sail @@ -0,0 +1,9 @@ +default Order dec + +$include + +val foo : bits(1) <-> bits(2) + +scattered mapping foo + +mapping clause foo = x : bits(1) <-> x : bits(2) diff --git a/test/typecheck/fail/poly_ab_mapping.expect b/test/typecheck/fail/poly_ab_mapping.expect new file mode 100644 index 000000000..269a4e994 --- /dev/null +++ b/test/typecheck/fail/poly_ab_mapping.expect @@ -0,0 +1,13 @@ +Type error: +fail/poly_ab_mapping.sail:9.21-38: +9 |mapping clause foo = x : 'a <-> x : 'b +  | ^---------------^ +  | 'x' must have the same type on both sides of the mapping +  | +  | fail/poly_ab_mapping.sail:9.21-22: +  | 9 |mapping clause foo = x : 'a <-> x : 'b +  |  | ^ has type 'a +  | fail/poly_ab_mapping.sail:9.32-33: +  | 9 |mapping clause foo = x : 'a <-> x : 'b +  |  | ^ has type 'b +  |  | Type mismatch between 'a and 'b diff --git a/test/typecheck/fail/poly_ab_mapping.sail b/test/typecheck/fail/poly_ab_mapping.sail new file mode 100644 index 000000000..dcc150e3f --- /dev/null +++ b/test/typecheck/fail/poly_ab_mapping.sail @@ -0,0 +1,9 @@ +default Order dec + +$include + +val foo : forall ('a 'b : Type). 'a <-> 'b + +scattered mapping foo + +mapping clause foo = x : 'a <-> x : 'b diff --git a/test/typecheck/pass/bool_mapping.sail b/test/typecheck/pass/bool_mapping.sail new file mode 100644 index 000000000..c3f0c4f0d --- /dev/null +++ b/test/typecheck/pass/bool_mapping.sail @@ -0,0 +1,13 @@ +default Order dec + +$include + +union instr = { + Foo : bool +} + +val bar : instr <-> bool + +scattered mapping bar + +mapping clause bar = Foo(b) <-> b diff --git a/test/typecheck/pass/bool_mapping2.sail b/test/typecheck/pass/bool_mapping2.sail new file mode 100644 index 000000000..1588db4a1 --- /dev/null +++ b/test/typecheck/pass/bool_mapping2.sail @@ -0,0 +1,13 @@ +default Order dec + +$include + +union instr = { + Foo : (bool, unit) +} + +val bar : instr <-> bool + +scattered mapping bar + +mapping clause bar = Foo(b, ()) <-> b