diff --git a/src/lib/preprocess.ml b/src/lib/preprocess.ml index 18c120b97..ad5107f5f 100644 --- a/src/lib/preprocess.ml +++ b/src/lib/preprocess.ml @@ -240,7 +240,8 @@ let preprocess dir target opts = incorrect start/end annotations *) | (DEF_aux (DEF_pragma ("file_start", _), _) | DEF_aux (DEF_pragma ("file_end", _), _)) :: defs -> aux acc defs | DEF_aux (DEF_pragma (p, arg), l) :: defs -> - if not (StringSet.mem p all_pragmas) then Reporting.warn "" l ("Unrecognised directive: " ^ p); + if not (StringSet.mem p all_pragmas || String.contains p '#') then + Reporting.warn "" l ("Unrecognised directive: " ^ p); aux (DEF_aux (DEF_pragma (p, arg), l) :: acc) defs | DEF_aux (DEF_outcome (outcome_spec, inner_defs), l) :: defs -> aux (DEF_aux (DEF_outcome (outcome_spec, aux [] inner_defs), l) :: acc) defs diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index d11f3b246..4efbf44d9 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -4057,10 +4057,17 @@ let check_fundef env def_annot (FD_aux (FD_function (recopt, tannotopt, funcls), in typ_print (lazy ("\n" ^ Util.("Check function " |> cyan |> clear) ^ string_of_id id)); let have_val_spec, (quant, typ), env = - try (true, Env.get_val_spec id env, env) - with Type_error (l, _) -> - let quant, typ = infer_funtyp l env tannotopt funcls in - (false, (quant, typ), env) + try (true, Env.get_val_spec id env, env) with + | Type_error (l, Err_not_in_scope (_, scope_l)) -> + typ_raise l + (Err_not_in_scope + ( Some "Cannot infer type of function as it has a defined type already. However, this type is not in scope.", + scope_l + ) + ) + | Type_error (l, _) -> + let quant, typ = infer_funtyp l env tannotopt funcls in + (false, (quant, typ), env) in let vtyp_args, vtyp_ret, vl = match typ with @@ -4493,6 +4500,13 @@ and check_def : Env.t -> uannot def -> tannot def list * Env.t = ], env ) + | DEF_pragma ("unscope#", arg, l) when !Initial_check.opt_magic_hash -> + let env = + match String.split_on_char ' ' arg with + | [id_category; id] -> Type_env.unscope_pragma id_category (mk_id id) env + | _ -> env + in + ([DEF_aux (DEF_pragma ("unscope#", arg, l), def_annot)], env) | DEF_pragma (pragma, arg, l) -> ([DEF_aux (DEF_pragma (pragma, arg, l), def_annot)], env) | DEF_scattered sdef -> check_scattered env def_annot sdef | DEF_measure (id, pat, exp) -> ([check_termination_measure_decl env def_annot (id, pat, exp)], env) diff --git a/src/lib/type_env.ml b/src/lib/type_env.ml index 91993ef89..2f571daca 100644 --- a/src/lib/type_env.ml +++ b/src/lib/type_env.ml @@ -88,15 +88,13 @@ end module IdPairMap = Map.Make (IdPair) -type ('a, 'b) generic_env_item = { item : 'a; loc : 'b } +type ('a, 'b) generic_env_item = { item : 'a; loc : 'b; mod_id : int } type 'a env_item = ('a, Parse_ast.l) generic_env_item type 'a multiple_env_item = ('a, Parse_ast.l list) generic_env_item -let mk_item ~loc:l item = { item; loc = l } - -let get_item item = item.item +let mk_item ~loc:l item = { item; loc = l; mod_id = 0 } let item_loc item = item.loc @@ -145,6 +143,7 @@ let empty_global_env = type env = { global : global_env; + opened : IntSet.t; locals : (mut * typ) Bindings.t; typ_vars : (Ast.l * kind_aux) KBindings.t; shadow_vars : int KBindings.t; @@ -158,15 +157,50 @@ type env = { outcome_typschm : (typquant * typ) option; } +let filter_items_with f env bindings = + Bindings.map + (fun item -> f item.item) + (Bindings.filter (fun _ item -> item.mod_id = 0 || IntSet.mem item.mod_id env.opened) bindings) + +let filter_items env bindings = filter_items_with (fun x -> x) env bindings + +let item_in_scope env item = item.mod_id = 0 || IntSet.mem item.mod_id env.opened + +let get_item_with_loc get_loc l env item = + if item_in_scope env item then item.item else typ_raise l (Err_not_in_scope (None, get_loc item.loc)) + +let get_item env item = get_item_with_loc (fun l -> Some l) env item + +let hd_opt = function x :: _ -> Some x | [] -> None + type type_variables = Type_internal.type_variables type t = env let update_global f env = { env with global = f env.global } +let unscope_pragma id_category id env = + typ_debug (lazy ("Unscope " ^ id_category ^ " " ^ string_of_id id)); + let update_id id m = Bindings.update id (function Some item -> Some { item with mod_id = -1 } | None -> None) m in + match id_category with + | "bitfield" -> update_global (fun global -> { global with bitfields = update_id id global.bitfields }) env + | "enum" -> update_global (fun global -> { global with enums = update_id id global.enums }) env + | "let" -> update_global (fun global -> { global with letbinds = update_id id global.letbinds }) env + | "mapping" -> update_global (fun global -> { global with mappings = update_id id global.mappings }) env + | "overload" -> update_global (fun global -> { global with overloads = update_id id global.overloads }) env + | "register" -> update_global (fun global -> { global with registers = update_id id global.registers }) env + | "struct" -> update_global (fun global -> { global with records = update_id id global.records }) env + | "type" -> update_global (fun global -> { global with synonyms = update_id id global.synonyms }) env + | "union" -> update_global (fun global -> { global with unions = update_id id global.unions }) env + | "val" -> update_global (fun global -> { global with val_specs = update_id id global.val_specs }) env + | _ -> + typ_debug (lazy "Unrecognized unscope category"); + env + let empty = { global = empty_global_env; + opened = IntSet.empty; locals = Bindings.empty; typ_vars = KBindings.empty; shadow_vars = KBindings.empty; @@ -345,7 +379,8 @@ let already_bound_ctor_fn str id env = Reporting.unreachable (id_loc id) __POS__ ("Could not find original binding for duplicate " ^ str ^ " called " ^ string_of_id id) -let get_overloads id env = try get_item (Bindings.find id env.global.overloads) with Not_found -> [] +let get_overloads id env = + try get_item_with_loc hd_opt (id_loc id) env (Bindings.find id env.global.overloads) with Not_found -> [] let add_overloads l id ids env = typ_print (lazy (adding ^ "overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]")); @@ -364,7 +399,9 @@ let add_overloads l id ids env = { global with overloads = - Bindings.add id (mk_item ~loc:(l :: item_loc existing) (get_item existing @ ids)) global.overloads; + Bindings.add id + (mk_item ~loc:(l :: item_loc existing) (get_item_with_loc hd_opt l env existing @ ids)) + global.overloads; } ) env @@ -374,9 +411,10 @@ let add_overloads l id ids env = env let infer_kind env id = + let l = id_loc id in if Bindings.mem id builtin_typs then Bindings.find id builtin_typs - else if Bindings.mem id env.global.unions then fst (get_item (Bindings.find id env.global.unions)) - else if Bindings.mem id env.global.records then fst (get_item (Bindings.find id env.global.records)) + else if Bindings.mem id env.global.unions then fst (get_item l env (Bindings.find id env.global.unions)) + else if Bindings.mem id env.global.records then fst (get_item l env (Bindings.find id env.global.records)) else if Bindings.mem id env.global.enums then mk_typquant [] else if Bindings.mem id env.global.synonyms then typ_error (id_loc id) ("Cannot infer kind of type synonym " ^ string_of_id id) @@ -440,11 +478,11 @@ let mk_synonym typq typ_arg = ) let get_typ_synonym id env = - match Option.map get_item (Bindings.find_opt id env.global.synonyms) with + match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.synonyms) with | Some (typq, arg) -> mk_synonym typq arg | None -> raise Not_found -let get_typ_synonyms env = Bindings.map get_item env.global.synonyms +let get_typ_synonyms env = filter_items env env.global.synonyms let get_constraints env = List.map snd env.constraints @@ -791,12 +829,12 @@ let add_typ_synonym id typq arg env = ) let get_val_spec_orig id env = - try get_item (Bindings.find id env.global.val_specs) + try get_item (id_loc id) env (Bindings.find id env.global.val_specs) with Not_found -> typ_error (id_loc id) ("No type signature found for " ^ string_of_id id) let get_val_spec id env = try - let bind = get_item (Bindings.find id env.global.val_specs) in + let bind = get_item (id_loc id) env (Bindings.find id env.global.val_specs) in typ_debug ( lazy ("get_val_spec: Env has " @@ -810,19 +848,19 @@ let get_val_spec id env = bind' with Not_found -> typ_error (id_loc id) ("No type declaration found for " ^ string_of_id id) -let get_val_specs env = Bindings.map get_item env.global.val_specs +let get_val_specs env = filter_items env env.global.val_specs let add_union_id id bind env = if bound_ctor_fn env id then already_bound_ctor_fn "union constructor" id env else ( typ_print (lazy (adding ^ "union identifier " ^ string_of_id id ^ " : " ^ string_of_bind bind)); update_global - (fun global -> { global with union_ids = Bindings.add id { item = bind; loc = id_loc id } global.union_ids }) + (fun global -> { global with union_ids = Bindings.add id (mk_item ~loc:(id_loc id) bind) global.union_ids }) env ) let get_union_id id env = - match Option.map get_item (Bindings.find_opt id env.global.union_ids) with + match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.union_ids) with | Some bind -> List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) | None -> typ_error (id_loc id) ("No union constructor found for " ^ string_of_id id) @@ -910,7 +948,7 @@ and add_outcome id (typq, typ, params, vals, outcome_env) env = env and get_outcome l id env = - match Option.map get_item (Bindings.find_opt id env.global.outcomes) with + match Option.map (get_item l env) (Bindings.find_opt id env.global.outcomes) with | Some (typq, typ, params, vals, val_specs) -> (typq, typ, params, vals, { empty with global = { empty_global_env with val_specs } }) | None -> typ_error l ("Outcome " ^ string_of_id id ^ " does not exist") @@ -1030,20 +1068,20 @@ let add_enum_clause id member env = | None -> typ_error (id_loc id) ("Enumeration " ^ string_of_id id ^ " does not exist") let get_enum id env = - match Option.map get_item (Bindings.find_opt id env.global.enums) with + match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.enums) with | Some (_, enum) -> IdSet.elements enum | None -> typ_error (id_loc id) ("Enumeration " ^ string_of_id id ^ " does not exist") -let get_enums env = Bindings.map (fun item -> item |> get_item |> snd) env.global.enums +let get_enums env = filter_items_with snd env env.global.enums let is_record id env = Bindings.mem id env.global.records let get_record id env = - match Option.map get_item (Bindings.find_opt id env.global.records) with + match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.records) with | Some record -> record | None -> typ_error (id_loc id) ("Struct type " ^ string_of_id id ^ " does not exist") -let get_records env = Bindings.map get_item env.global.records +let get_records env = filter_items env env.global.records let add_record id typq fields env = let fields = List.map (fun (typ, id) -> (expand_synonyms env typ, id)) fields in @@ -1086,7 +1124,7 @@ let get_accessor_fn record_id field env = let freshen_bind bind = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in - try freshen_bind (get_item (IdPairMap.find (record_id, field) env.global.accessors)) + try freshen_bind (get_item (id_loc field) env (IdPairMap.find (record_id, field) env.global.accessors)) with Not_found -> typ_error (id_loc field) ("No field accessor found for " ^ string_of_id record_id ^ "." ^ string_of_id field) @@ -1173,10 +1211,10 @@ let add_variant_clause id tu env = env | None -> typ_error (id_loc id) ("scattered union " ^ string_of_id id ^ " not found") -let get_variants env = Bindings.map get_item env.global.unions +let get_variants env = filter_items env env.global.unions let get_variant id env = - match Option.map get_item (Bindings.find_opt id env.global.unions) with + match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.unions) with | Some (typq, tus) -> (typq, tus) | None -> typ_error (id_loc id) ("union " ^ string_of_id id ^ " not found") @@ -1193,11 +1231,11 @@ let set_scattered_variant_env ~variant_env id env = let is_register id env = Bindings.mem id env.global.registers let get_register id env = - match Option.map get_item (Bindings.find_opt id env.global.registers) with + match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.registers) with | Some typ -> typ | None -> typ_error (id_loc id) ("No register binding found for " ^ string_of_id id) -let get_registers env = Bindings.map get_item env.global.registers +let get_registers env = filter_items env env.global.registers let is_extern id env backend = try not (Ast_util.extern_assoc backend (Bindings.find_opt id env.global.externs) = None) with Not_found -> false @@ -1234,16 +1272,26 @@ let lookup_id id env = match Bindings.find_opt id env.locals with | Some (mut, typ) -> Local (mut, typ) | None -> ( - match Bindings.find_opt id env.global.letbinds with - | Some { item = typ; _ } -> Local (Immutable, typ) + match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.letbinds) with + | Some typ -> Local (Immutable, typ) | None -> ( - match Bindings.find_opt id env.global.registers with - | Some { item = typ; _ } -> Register typ + match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.registers) with + | Some typ -> Register typ | None -> ( match List.find_opt (fun (_, { item = _, ctors }) -> IdSet.mem id ctors) (Bindings.bindings env.global.enums) with - | Some (enum, _) -> Enum (mk_typ (Typ_id enum)) + | Some (enum_id, item) -> + if item_in_scope env item then Enum (mk_typ (Typ_id enum_id)) + else ( + let enum_name = string_of_id enum_id in + typ_raise (id_loc id) + (Err_not_in_scope + ( Some ("Enumeration " ^ enum_name ^ " containing " ^ string_of_id id ^ " is not in scope"), + Some item.loc + ) + ) + ) | None -> Unbound id ) ) @@ -1288,7 +1336,7 @@ let base_typ_of env typ = let is_bitfield id env = Bindings.mem id env.global.bitfields let get_bitfield id env = - match Option.map get_item (Bindings.find_opt id env.global.bitfields) with + match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.bitfields) with | Some bitfield -> bitfield | None -> typ_error (id_loc id) ("Could not find bitfield " ^ string_of_id id) diff --git a/src/lib/type_env.mli b/src/lib/type_env.mli index 8ea2ca7b7..a63677976 100644 --- a/src/lib/type_env.mli +++ b/src/lib/type_env.mli @@ -81,6 +81,12 @@ type env type t = env +(** This implements the unscope# pragma, which removes an identifier + from scope by setting its module id to -1 (which is never a valid + module id). This is used only to test the typechecker, and should + not be used for any other reason! *) +val unscope_pragma : string -> id -> t -> t + 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 d27e62d30..6361f4b9f 100644 --- a/src/lib/type_error.ml +++ b/src/lib/type_error.ml @@ -352,6 +352,14 @@ let message_of_type_error = ([coercion; Line "Coercion failed because:"; msg trigger] @ if not (reasons = []) then Line "Possible reasons:" :: List.map msg reasons else [] ) + | Err_not_in_scope (explanation, Some l) -> + Seq + [ + Line (Option.value ~default:"Not in scope" explanation); + Line "Try bringing the following definition into scope:"; + Location ("", Some "definition here", l, Seq []); + ] + | Err_not_in_scope (explanation, None) -> Line (Option.value ~default:"Not in scope" explanation) in msg diff --git a/src/lib/type_error.mli b/src/lib/type_error.mli index f36955fc1..7795a7481 100644 --- a/src/lib/type_error.mli +++ b/src/lib/type_error.mli @@ -94,6 +94,7 @@ type type_error = | Err_no_num_ident of id | Err_other of string | Err_inner of type_error * Parse_ast.l * string * string option * type_error + | Err_not_in_scope of string option * Parse_ast.l option exception Type_error of Parse_ast.l * type_error diff --git a/src/lib/type_internal.ml b/src/lib/type_internal.ml index 5d3336dfa..70546a1a8 100644 --- a/src/lib/type_internal.ml +++ b/src/lib/type_internal.ml @@ -109,6 +109,7 @@ type type_error = | Err_no_num_ident of id | Err_other of string | Err_inner of type_error * Parse_ast.l * string * string option * type_error + | Err_not_in_scope of string option * Parse_ast.l option let err_because (error1, l, error2) = Err_inner (error1, l, "Caused by", None, error2) diff --git a/test/typecheck/fail/unscope_enum.expect b/test/typecheck/fail/unscope_enum.expect new file mode 100644 index 000000000..65b61dc37 --- /dev/null +++ b/test/typecheck/fail/unscope_enum.expect @@ -0,0 +1,9 @@ +Type error: +fail/unscope_enum.sail:14.10-11: +14 | let _ = A; +  | ^ +  | Enumeration E containing A is not in scope +  | Try bringing the following definition into scope: +  | fail/unscope_enum.sail:7.5-6: +  | 7 |enum E = A | B | C +  |  | ^ definition here diff --git a/test/typecheck/fail/unscope_enum.sail b/test/typecheck/fail/unscope_enum.sail new file mode 100644 index 000000000..3962777c8 --- /dev/null +++ b/test/typecheck/fail/unscope_enum.sail @@ -0,0 +1,16 @@ +$option -dmagic_hash + +default Order dec + +$include + +enum E = A | B | C + +$unscope# enum E + +val bar : unit -> unit + +function bar() = { + let _ = A; + () +} diff --git a/test/typecheck/fail/unscope_let.expect b/test/typecheck/fail/unscope_let.expect new file mode 100644 index 000000000..f4927bf4f --- /dev/null +++ b/test/typecheck/fail/unscope_let.expect @@ -0,0 +1,9 @@ +Type error: +fail/unscope_let.sail:14.10-13: +14 | let _ = foo; +  | ^-^ +  | Not in scope +  | Try bringing the following definition into scope: +  | fail/unscope_let.sail:7.4-7: +  | 7 |let foo : bits(32) = 0xFFFF_FFFF +  |  | ^-^ definition here diff --git a/test/typecheck/fail/unscope_let.sail b/test/typecheck/fail/unscope_let.sail new file mode 100644 index 000000000..836b585f2 --- /dev/null +++ b/test/typecheck/fail/unscope_let.sail @@ -0,0 +1,16 @@ +$option -dmagic_hash + +default Order dec + +$include + +let foo : bits(32) = 0xFFFF_FFFF + +$unscope# let foo + +val bar : unit -> unit + +function bar() = { + let _ = foo; + () +} diff --git a/test/typecheck/fail/unscope_register.expect b/test/typecheck/fail/unscope_register.expect new file mode 100644 index 000000000..afc2745d3 --- /dev/null +++ b/test/typecheck/fail/unscope_register.expect @@ -0,0 +1,9 @@ +Type error: +fail/unscope_register.sail:14.10-13: +14 | let _ = foo; +  | ^-^ +  | Not in scope +  | Try bringing the following definition into scope: +  | fail/unscope_register.sail:7.9-12: +  | 7 |register foo : bits(32) +  |  | ^-^ definition here diff --git a/test/typecheck/fail/unscope_register.sail b/test/typecheck/fail/unscope_register.sail new file mode 100644 index 000000000..a746dbf7b --- /dev/null +++ b/test/typecheck/fail/unscope_register.sail @@ -0,0 +1,16 @@ +$option -dmagic_hash + +default Order dec + +$include + +register foo : bits(32) + +$unscope# register foo + +val bar : unit -> unit + +function bar() = { + let _ = foo; + () +} diff --git a/test/typecheck/fail/unscope_type.expect b/test/typecheck/fail/unscope_type.expect new file mode 100644 index 000000000..03264fb8f --- /dev/null +++ b/test/typecheck/fail/unscope_type.expect @@ -0,0 +1,9 @@ +Type error: +fail/unscope_type.sail:14.10-13: +14 | let _ : foo = 0xFFFF_FFFF; +  | ^-^ +  | Not in scope +  | Try bringing the following definition into scope: +  | fail/unscope_type.sail:7.5-8: +  | 7 |type foo = bits(32) +  |  | ^-^ definition here diff --git a/test/typecheck/fail/unscope_type.sail b/test/typecheck/fail/unscope_type.sail new file mode 100644 index 000000000..01b4397a1 --- /dev/null +++ b/test/typecheck/fail/unscope_type.sail @@ -0,0 +1,16 @@ +$option -dmagic_hash + +default Order dec + +$include + +type foo = bits(32) + +$unscope# type foo + +val bar : unit -> unit + +function bar() = { + let _ : foo = 0xFFFF_FFFF; + () +} diff --git a/test/typecheck/fail/unscope_val.expect b/test/typecheck/fail/unscope_val.expect new file mode 100644 index 000000000..3e54d0f70 --- /dev/null +++ b/test/typecheck/fail/unscope_val.expect @@ -0,0 +1,9 @@ +Type error: +fail/unscope_val.sail:11.9-12: +11 |function foo() = () +  | ^-^ +  | Cannot infer type of function as it has a defined type already. However, this type is not in scope. +  | Try bringing the following definition into scope: +  | fail/unscope_val.sail:7.4-7: +  | 7 |val foo : unit -> unit +  |  | ^-^ definition here diff --git a/test/typecheck/fail/unscope_val.sail b/test/typecheck/fail/unscope_val.sail new file mode 100644 index 000000000..538667a79 --- /dev/null +++ b/test/typecheck/fail/unscope_val.sail @@ -0,0 +1,11 @@ +$option -dmagic_hash + +default Order dec + +$include + +val foo : unit -> unit + +$unscope# val foo + +function foo() = ()