diff --git a/language/sail.ott b/language/sail.ott index 0d84501e1..425411c64 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -77,7 +77,7 @@ open Value type text = string type l = Parse_ast.l -type config = Parse_ast.Config.config +type attribute_data = Parse_ast.Attribute_data.attribute_data type 'a annot = l * 'a @@ -106,10 +106,10 @@ declare ocaml target_rep type ocaml_l = `Parse_ast.l` type l = ocaml_l -type ocaml_config -declare ocaml target_rep type ocaml_config = `Parse_ast.Config.config` +type ocaml_attribute_data +declare ocaml target_rep type ocaml_attribute_data = `Parse_ast.Attribute_data.attribute_data` -type config = ocaml_config +type attribute_data = ocaml_attribute_data type value declare ocaml target_rep type value = `Value.value` @@ -124,7 +124,7 @@ type visibility = Public | Private of l type def_annot = <| doc_comment : maybe string; - attrs : list (l * string * maybe config); + attrs : list (l * string * maybe attribute_data); visibility : visibility; loc : l |> diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index f57836f25..f57707b28 100644 --- a/src/lib/ast_util.ml +++ b/src/lib/ast_util.ml @@ -67,24 +67,27 @@ open Ast open Ast_defs -open Parse_ast.Config +open Parse_ast.Attribute_data open Util module Big_int = Nat_big_num (* The type of annotations for untyped AST nodes *) -type uannot = { attrs : (l * string * config option) list } +type uannot = { attrs : (l * string * attribute_data option) list } -let rec string_of_config (Conf_aux (aux, _)) = +let rec string_of_attribute_data (AD_aux (aux, _)) = match aux with - | Conf_object kvs -> - "{ " ^ Util.string_of_list ", " (fun (k, v) -> Printf.sprintf "%s = %s" k (string_of_config v)) kvs ^ " }" - | Conf_string s -> "\"" ^ s ^ "\"" - | Conf_num n -> Big_int.to_string n - | Conf_list cs -> "[" ^ Util.string_of_list ", " string_of_config cs ^ "]" + | AD_object kvs -> + "{ " + ^ Util.string_of_list ", " (fun (k, v) -> Printf.sprintf "\"%s\" = %s" k (string_of_attribute_data v)) kvs + ^ " }" + | AD_string s -> "\"" ^ s ^ "\"" + | AD_num n -> Big_int.to_string n + | AD_list cs -> "[" ^ Util.string_of_list ", " string_of_attribute_data cs ^ "]" + | AD_bool b -> string_of_bool b let string_of_attribute attr = function | None -> Printf.sprintf "$[%s]" attr - | Some config -> Printf.sprintf "$[%s %s]" attr (string_of_config config) + | Some data -> Printf.sprintf "$[%s %s]" attr (string_of_attribute_data data) let empty_uannot = { attrs = [] } diff --git a/src/lib/ast_util.mli b/src/lib/ast_util.mli index 80f2f0cf3..29339add2 100644 --- a/src/lib/ast_util.mli +++ b/src/lib/ast_util.mli @@ -80,9 +80,9 @@ type uannot val empty_uannot : uannot -val string_of_attribute : string -> config option -> string +val string_of_attribute : string -> attribute_data option -> string -val string_of_config : config -> string +val string_of_attribute_data : attribute_data -> string (** Add an attribute to an annotation. Attributes are attached to expressions in Sail via: {@sail[ @@ -91,21 +91,22 @@ val string_of_config : config -> string The location argument should be a span that corresponds to the attribute itself, and not include the expression. *) -val add_attribute : l -> string -> config option -> uannot -> uannot +val add_attribute : l -> string -> attribute_data option -> uannot -> uannot val remove_attribute : string -> uannot -> uannot -val get_attribute : string -> uannot -> (l * config option) option +val get_attribute : string -> uannot -> (l * attribute_data option) option -val get_attributes : uannot -> (l * string * config option) list +val get_attributes : uannot -> (l * string * attribute_data option) list -val find_attribute_opt : string -> (l * string * config option) list -> config option option +val find_attribute_opt : string -> (l * string * attribute_data option) list -> attribute_data option option -val mk_def_annot : ?doc:string -> ?attrs:(l * string * config option) list -> ?visibility:visibility -> l -> def_annot +val mk_def_annot : + ?doc:string -> ?attrs:(l * string * attribute_data option) list -> ?visibility:visibility -> l -> def_annot -val add_def_attribute : l -> string -> config option -> def_annot -> def_annot +val add_def_attribute : l -> string -> attribute_data option -> def_annot -> def_annot -val get_def_attribute : string -> def_annot -> (l * config option) option +val get_def_attribute : string -> def_annot -> (l * attribute_data option) option val remove_def_attribute : string -> def_annot -> def_annot diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index fbc150215..1c20c45b5 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -68,7 +68,7 @@ open Ast open Ast_defs open Ast_util -open Parse_ast.Config +open Parse_ast.Attribute_data open Jib open Jib_util open Jib_visitor @@ -193,8 +193,8 @@ let initial_ctx env effect_info = } let update_coverage_override' ctx = function - | Some (_, Some (Conf_aux (Conf_string "on", _))) -> { ctx with coverage_override = true } - | Some (_, Some (Conf_aux (Conf_string "off", _))) -> { ctx with coverage_override = false } + | Some (_, Some (AD_aux (AD_string "on", _))) -> { ctx with coverage_override = true } + | Some (_, Some (AD_aux (AD_string "off", _))) -> { ctx with coverage_override = false } | _ -> ctx let update_coverage_override uannot ctx = update_coverage_override' ctx (get_attribute "coverage" uannot) diff --git a/src/lib/monomorphise.ml b/src/lib/monomorphise.ml index 997861125..994bc940d 100644 --- a/src/lib/monomorphise.ml +++ b/src/lib/monomorphise.ml @@ -4159,7 +4159,7 @@ module BitvectorSizeCasts = struct | P_aux (P_wild, (_, annot)), None -> begin (* Similar to the literal case *) match (body, untyped_annot annot |> get_attribute "int_wildcard") with - | _, Some (_, Some (Conf_aux (Conf_num i, _))) -> + | _, Some (_, Some (AD_aux (AD_num i, _))) -> let src_typ = fill_in_type (Env.add_constraint (nc_eq (nvar kid) (nconstant i)) env) result_typ in diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml index 67c289d8a..fc1731ebc 100644 --- a/src/lib/parse_ast.ml +++ b/src/lib/parse_ast.ml @@ -76,19 +76,24 @@ type l = | Hint of string * l * l | Range of Lexing.position * Lexing.position -(* Put the config type in it's own module, so other modules can import - it unqualified. *) -module Config = struct - type config_aux = - (* JSON-style configuration structure *) - | Conf_object of (string * config) list - | Conf_list of config list - | Conf_num of Big_int.num - | Conf_string of string - - and config = Conf_aux of config_aux * l +(** We put the attribute data type in it's own module, so other + modules can import it unqualified. The parse AST and the main AST + share this type, so modules that wouldn't normally import this + module will want to use it. *) +module Attribute_data = struct + type attribute_data_aux = + | AD_object of (string * attribute_data) list + | AD_list of attribute_data list + | AD_num of Big_int.num + | AD_string of string + | AD_bool of bool + + (** JSON-style data structure for attributes *) + and attribute_data = AD_aux of attribute_data_aux * l end +open Attribute_data + type 'a annot = l * 'a type extern = { pure : bool; bindings : (string * string) list } @@ -203,7 +208,7 @@ type pat_aux = | P_cons of pat * pat (* cons pattern *) | P_string_append of pat list (* string append pattern, x ^^ y *) | P_struct of fpat list (* struct pattern *) - | P_attribute of string * Config.config option * pat + | P_attribute of string * attribute_data option * pat and pat = P_aux of pat_aux * l @@ -258,7 +263,7 @@ and exp_aux = | E_return of exp | E_assert of exp * exp | E_var of exp * exp * exp - | E_attribute of string * Config.config option * exp + | E_attribute of string * attribute_data option * exp | E_internal_plet of pat * exp * exp | E_internal_return of exp | E_internal_assume of atyp * exp @@ -306,7 +311,7 @@ type funcl = FCL_aux of funcl_aux * l and funcl_aux = (* Function clause *) | FCL_private of funcl - | FCL_attribute of string * Config.config option * funcl + | FCL_attribute of string * attribute_data option * funcl | FCL_doc of string * funcl | FCL_funcl of id * pexp @@ -315,7 +320,7 @@ type type_union = Tu_aux of type_union_aux * l and type_union_aux = (* Type union constructors *) | Tu_private of type_union - | Tu_attribute of string * Config.config option * type_union + | Tu_attribute of string * attribute_data option * type_union | Tu_doc of string * type_union | Tu_ty_id of atyp * id | Tu_ty_anon_rec of (atyp * id) list * id @@ -371,7 +376,7 @@ type mapcl = MCL_aux of mapcl_aux * l and mapcl_aux = (* mapping clause (bidirectional pattern-match) *) - | MCL_attribute of string * Config.config option * mapcl + | MCL_attribute of string * attribute_data option * mapcl | MCL_doc of string * mapcl | MCL_bidir of mpexp * mpexp | MCL_forwards_deprecated of mpexp * exp @@ -458,7 +463,7 @@ type def_aux = | DEF_register of dec_spec (* register declaration *) | DEF_pragma of string * string * int | DEF_private of def - | DEF_attribute of string * Config.config option * def + | DEF_attribute of string * attribute_data option * def | DEF_doc of string * def | DEF_internal_mutrec of fundef list diff --git a/src/lib/parser.mly b/src/lib/parser.mly index a28f9446f..983bf6d1d 100644 --- a/src/lib/parser.mly +++ b/src/lib/parser.mly @@ -71,7 +71,7 @@ module Big_int = Nat_big_num open Parse_ast -open Parse_ast.Config +open Parse_ast.Attribute_data let loc n m = Range (n, m) @@ -272,13 +272,13 @@ let set_syntax_deprecated l = %start typ_eof %start exp_eof %start def_eof -%start config_eof +%start attribute_data_eof %type typschm_eof %type typ_eof %type exp_eof %type def_eof %type file -%type config_eof +%type attribute_data_eof %% @@ -867,31 +867,35 @@ vector_update_list: | vector_update Comma vector_update_list { $1 :: $3 } -config_key_value: - | key = String; Eq; value = config +attribute_data_key_value: + | key = String; Eq; value = attribute_data { (key, value) } -config: - | Lcurly; kvs = separated_list(Comma, config_key_value) Rcurly - { Conf_aux (Conf_object kvs, loc $startpos $endpos) } +attribute_data: + | Lcurly; kvs = separated_list(Comma, attribute_data_key_value) Rcurly + { AD_aux (AD_object kvs, loc $startpos $endpos) } | n = Num - { Conf_aux (Conf_num n, loc $startpos $endpos) } + { AD_aux (AD_num n, loc $startpos $endpos) } | s = String - { Conf_aux (Conf_string s, loc $startpos $endpos) } + { AD_aux (AD_string s, loc $startpos $endpos) } | id = Id - { Conf_aux (Conf_string id, loc $startpos $endpos) } - | Lsquare; xs = separated_list(Comma, config) Rsquare - { Conf_aux (Conf_list xs, loc $startpos $endpos) } + { AD_aux (AD_string id, loc $startpos $endpos) } + | True + { AD_aux (AD_bool true, loc $startpos $endpos) } + | False + { AD_aux (AD_bool false, loc $startpos $endpos) } + | Lsquare; xs = separated_list(Comma, attribute_data) Rsquare + { AD_aux (AD_list xs, loc $startpos $endpos) } attribute: | attr = Attribute; Rsquare { (attr, None) } - | attr = Attribute; c = config; Rsquare - { (attr, Some c) } + | attr = Attribute; d = attribute_data; Rsquare + { (attr, Some d) } -config_eof: - | c = config; Eof - { c } +attribute_data_eof: + | d = attribute_data; Eof + { d } funcl_annotation: | visibility = Private diff --git a/src/lib/pattern_completeness.ml b/src/lib/pattern_completeness.ml index 2377f8cb0..831332de7 100644 --- a/src/lib/pattern_completeness.ml +++ b/src/lib/pattern_completeness.ml @@ -84,7 +84,7 @@ type ctx = { module type Config = sig type t val typ_of_t : t -> typ - val add_attribute : l -> string -> config option -> t -> t + val add_attribute : l -> string -> attribute_data option -> t -> t end type row_index = { loc : l; num : int } @@ -298,7 +298,7 @@ module Make (C : Config) = struct | P_struct (fps, fwild) -> P_struct (List.map (fun (field, p) -> (field, go wild p)) fps, fwild) | P_id id -> P_id id | P_lit (L_aux (L_num n, _)) when wild -> - t := C.add_attribute (gen_loc l) "int_wildcard" (Some (Conf_aux (Conf_num n, gen_loc l))) !t; + t := C.add_attribute (gen_loc l) "int_wildcard" (Some (AD_aux (AD_num n, gen_loc l))) !t; P_wild | P_lit _ when wild -> let typ = typ_of_pat full_pat in diff --git a/src/lib/pattern_completeness.mli b/src/lib/pattern_completeness.mli index 2786a0ebb..be22c26dc 100644 --- a/src/lib/pattern_completeness.mli +++ b/src/lib/pattern_completeness.mli @@ -85,7 +85,7 @@ type ctx = { module type Config = sig type t val typ_of_t : t -> typ - val add_attribute : l -> string -> config option -> t -> t + val add_attribute : l -> string -> attribute_data option -> t -> t end module Make (C : Config) : sig diff --git a/src/lib/reporting.mli b/src/lib/reporting.mli index 11ed04f39..98c84347f 100644 --- a/src/lib/reporting.mli +++ b/src/lib/reporting.mli @@ -143,12 +143,12 @@ val err_lex : Lexing.position -> string -> exn (** Raise an unreachable exception. -This should always be used over an assert false or a generic OCaml failwith exception when appropriate *) +This should always be used over an assert false or a generic OCaml failwith exception when appropriate. *) val unreachable : Parse_ast.l -> string * int * int * int -> string -> 'a (** Print an error to stdout. -@param interactive If this is true (default false) then unreachable errors are reported as general errors. +@param interactive If this is true (default false) then unreachable errors are reported as general errors. This is used by the interactive read-eval-print loop. The interactive mode exposes a lot of internal features, so it's possible to excute code paths from the interactive mode that would otherwise be unreachable during normal execution. *) val print_error : ?interactive:bool -> error -> unit diff --git a/src/lib/scattered.ml b/src/lib/scattered.ml index 165397ff7..c4233bbd4 100644 --- a/src/lib/scattered.ml +++ b/src/lib/scattered.ml @@ -197,7 +197,7 @@ let rec descatter' accumulator funcls mapcls = function let def_annot = def_annot |> add_def_attribute (gen_loc l) "no_enum_functions" None - |> add_def_attribute (gen_loc l) "undefined_gen" (Some (Conf_aux (Conf_string "forbid", gen_loc l))) + |> add_def_attribute (gen_loc l) "undefined_gen" (Some (AD_aux (AD_string "forbid", gen_loc l))) in let accumulator = DEF_aux (DEF_type (TD_aux (TD_enum (id, members, false), (gen_loc l, Type_check.empty_tannot))), def_annot) diff --git a/src/lib/state.ml b/src/lib/state.ml index fda0cc5dc..38d7fabeb 100644 --- a/src/lib/state.ml +++ b/src/lib/state.ml @@ -145,9 +145,7 @@ let generate_regstate env registers = [ DEF_aux ( DEF_type (TD_aux (regstate_def, (Unknown, empty_uannot))), - add_def_attribute Unknown "undefined_gen" - (Some (Conf_aux (Conf_string "forbid", Unknown))) - (mk_def_annot Unknown) + add_def_attribute Unknown "undefined_gen" (Some (AD_aux (AD_string "forbid", Unknown))) (mk_def_annot Unknown) ); ] diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index 20d382220..b9c5dfcd7 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -70,7 +70,7 @@ open Ast_defs open Ast_util open Util open Lazy -open Parse_ast.Config +open Parse_ast.Attribute_data module Big_int = Nat_big_num @@ -1767,6 +1767,12 @@ let rec filter_overload_tree env = (OT_overloads (f, overloads, List.map fst args, annot), returns) | OT_leaf (_, leaf_type) as tree -> (tree, [leaf_type]) +let add_overload_attribute l f = + let l = gen_loc l in + let name, is_infix = match f with Id_aux (Id v, _) -> (v, false) | Id_aux (Operator v, _) -> (v, true) in + add_attribute l "overloaded" + (Some (AD_aux (AD_object [("name", AD_aux (AD_string name, l)); ("is_infix", AD_aux (AD_bool is_infix, l))], l))) + let rec overload_tree_to_exp env = function | OT_overloads (f, overloads, args, annot) -> let id, env = Env.add_filtered_overload f overloads env in @@ -2112,7 +2118,7 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au | errs, [] -> typ_raise l (Err_no_overloading (orig_f, errs)) | errs, f :: fs -> begin typ_print (lazy ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")")); - try crule check_exp env (E_aux (E_app (f, xs), (l, uannot))) typ + try crule check_exp env (E_aux (E_app (f, xs), (l, add_overload_attribute l orig_f uannot))) typ with Type_error (err_l, err) -> typ_debug (lazy "Error"); try_overload (errs @ [(f, err_l, err)], fs) @@ -2133,17 +2139,17 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au short-circuiting. *) match destruct_exist (typ_of (irule infer_exp env y)) with | None | Some (_, NC_aux (NC_true, _), _) -> - let inferred_exp = infer_funapp l env f [x; y] (Some typ) in + let inferred_exp = infer_funapp l env f [x; y] uannot (Some typ) in expect_subtype env inferred_exp typ | Some _ -> - let inferred_exp = infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] (Some typ) in + let inferred_exp = infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] uannot (Some typ) in expect_subtype env inferred_exp typ | exception Type_error _ -> - let inferred_exp = infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] (Some typ) in + let inferred_exp = infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] uannot (Some typ) in expect_subtype env inferred_exp typ end | E_app (f, xs), _ -> - let inferred_exp = infer_funapp l env f xs (Some typ) in + let inferred_exp = infer_funapp l env f xs uannot (Some typ) in expect_subtype env inferred_exp typ | E_return exp, _ -> let checked_exp = @@ -2452,7 +2458,7 @@ and bind_pat env (P_aux (pat_aux, (l, uannot)) as pat) typ = | P_wild -> let env = match get_attribute "int_wildcard" uannot with - | Some (_, Some (Conf_aux (Conf_num arg, _))) -> + | Some (_, Some (AD_aux (AD_num arg, _))) -> (* If the patterh completeness checker replaced an numeric pattern, modify the environment as if it hadn't *) let _, env, _ = bind_pat env (P_aux (P_lit (L_aux (L_num arg, gen_loc l)), (l, uannot))) typ in env @@ -3202,7 +3208,7 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) = (* Accessing a field of a record *) | Typ_aux (Typ_id rectyp, _) when Env.is_record rectyp env -> begin let inferred_acc = - infer_funapp' l env field (Env.get_accessor_fn rectyp field env) [strip_exp inferred_exp] None + infer_funapp' l env field (Env.get_accessor_fn rectyp field env) [strip_exp inferred_exp] uannot None in match inferred_acc with | E_aux (E_app (field, [inferred_exp]), _) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc) @@ -3211,7 +3217,7 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) = (* Not sure if we need to do anything different with args here. *) | Typ_aux (Typ_app (rectyp, _), _) when Env.is_record rectyp env -> begin let inferred_acc = - infer_funapp' l env field (Env.get_accessor_fn rectyp field env) [strip_exp inferred_exp] None + infer_funapp' l env field (Env.get_accessor_fn rectyp field env) [strip_exp inferred_exp] uannot None in match inferred_acc with | E_aux (E_app (field, [inferred_exp]), _) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc) @@ -3292,7 +3298,7 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) = | errs, [] -> typ_raise l (Err_no_overloading (orig_f, errs)) | errs, f :: fs -> begin typ_print (lazy ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")")); - try irule infer_exp env (E_aux (E_app (f, xs), (l, uannot))) + try irule infer_exp env (E_aux (E_app (f, xs), (l, add_overload_attribute l orig_f uannot))) with Type_error (err_l, err) -> typ_debug (lazy "Error"); try_overload (errs @ [(f, err_l, err)], fs) @@ -3308,11 +3314,11 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) = infer_exp env exp | E_app (f, [x; y]) when string_of_id f = "and_bool" || string_of_id f = "or_bool" -> begin match destruct_exist (typ_of (irule infer_exp env y)) with - | None | Some (_, NC_aux (NC_true, _), _) -> infer_funapp l env f [x; y] None - | Some _ -> infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] None - | exception Type_error _ -> infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] None + | None | Some (_, NC_aux (NC_true, _), _) -> infer_funapp l env f [x; y] uannot None + | Some _ -> infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] uannot None + | exception Type_error _ -> infer_funapp l env f [x; mk_exp (E_typ (bool_typ, y))] uannot None end - | E_app (f, xs) -> infer_funapp l env f xs None + | E_app (f, xs) -> infer_funapp l env f xs uannot None | E_loop (loop_type, measure, cond, body) -> let checked_cond = crule check_exp env cond bool_typ in let checked_measure = @@ -3484,7 +3490,7 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) = annot_exp (E_internal_assume (nc, exp')) (typ_of exp') | _ -> typ_error l ("Cannot infer type of: " ^ string_of_exp exp) -and infer_funapp l env f xs ret_ctx_typ = infer_funapp' l env f (Env.get_val_spec f env) xs ret_ctx_typ +and infer_funapp l env f xs uannot ret_ctx_typ = infer_funapp' l env f (Env.get_val_spec f env) xs uannot ret_ctx_typ and infer_vector_update l env v n exp = let rec nested_updates acc = function @@ -3522,20 +3528,19 @@ and instantiation_of (E_aux (_, (l, tannot)) as exp) = end | _ -> invalid_arg ("instantiation_of expected application, got " ^ string_of_exp exp) -and instantiation_of_without_type (E_aux (exp_aux, (l, _)) as exp) = +and instantiation_of_without_type (E_aux (exp_aux, (l, (_, uannot))) as exp) = let env = env_of exp in match exp_aux with - | E_app (f, xs) -> instantiation_of (infer_funapp' l env f (Env.get_val_spec f env) (List.map strip_exp xs) None) + | E_app (f, xs) -> + instantiation_of (infer_funapp' l env f (Env.get_val_spec f env) (List.map strip_exp xs) uannot None) | _ -> invalid_arg ("instantiation_of expected application, got " ^ string_of_exp exp) -and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ = +and infer_funapp' l env f (typq, f_typ) xs uannot expected_ret_typ = typ_print (lazy (Util.("Function " |> cyan |> clear) ^ string_of_id f)); let annot_exp exp typ inst = E_aux ( exp, - ( l, - (Some { env; typ; monadic = no_effect; expected = expected_ret_typ; instantiation = Some inst }, empty_uannot) - ) + (l, (Some { env; typ; monadic = no_effect; expected = expected_ret_typ; instantiation = Some inst }, uannot)) ) in let is_bound env kid = KBindings.mem kid (Env.get_typ_vars env) in @@ -4411,7 +4416,7 @@ let extension_def_attribute env def_annot = match get_def_attribute "extension" def_annot with | Some (l, name) -> begin match name with - | Some (Conf_aux (Conf_string name, _)) -> begin + | Some (AD_aux (AD_string name, _)) -> begin match Env.get_current_visibility env with | Private vis_l -> raise @@ -4443,7 +4448,7 @@ let check_record l env def_annot id typq fields = let env = try match get_def_attribute "bitfield" def_annot with - | Some (_, Some (Conf_aux (Conf_num size, _))) when not (Env.is_bitfield id env) -> + | Some (_, Some (AD_aux (AD_num size, _))) when not (Env.is_bitfield id env) -> Env.add_bitfield id (bitvector_typ (nconstant size)) Bindings.empty env | _ -> env with _ -> env @@ -4456,8 +4461,8 @@ let check_global_constraint env def_annot nc = typ_error def_annot.loc "Global constraint appears inconsistent with previous global constraints"; ([DEF_aux (DEF_constraint nc, def_annot)], env) -let undefined_skip l = Some (Conf_aux (Conf_string "skip", gen_loc l)) -let undefined_forbid l = Some (Conf_aux (Conf_string "forbid", gen_loc l)) +let undefined_skip l = Some (AD_aux (AD_string "skip", gen_loc l)) +let undefined_forbid l = Some (AD_aux (AD_string "forbid", gen_loc l)) let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list * Env.t = fun env def_annot (TD_aux (tdef, (l, _))) -> @@ -4476,11 +4481,11 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list let env = check_record l env def_annot id typq fields in begin match get_def_attribute "undefined_gen" def_annot with - | Some (_, Some (Conf_aux (Conf_string "forbid", _))) -> + | Some (_, Some (AD_aux (AD_string "forbid", _))) -> ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) - | Some (_, Some (Conf_aux (Conf_string "skip", _))) -> + | Some (_, Some (AD_aux (AD_string "skip", _))) -> ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], Env.allow_user_undefined id env) - | (Some (_, Some (Conf_aux (Conf_string "generate", _))) | None) as attr -> + | (Some (_, Some (AD_aux (AD_string "generate", _))) | None) as attr -> let field_env = Env.add_typquant l typq env in let field_env = List.fold_left @@ -4520,7 +4525,7 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list | Some (attr_l, Some arg) -> typ_error (Hint ("When checking this struct", l, attr_l)) - ("Unrecognized argument to undefined attribute: " ^ string_of_config arg) + ("Unrecognized argument to undefined attribute: " ^ string_of_attribute_data arg) | Some (attr_l, None) -> typ_error (Hint ("When checking this struct", l, attr_l)) "No argument for undefined attribute" end @@ -4537,11 +4542,11 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list let env = Env.add_enum id ids env in begin match get_def_attribute "undefined_gen" def_annot with - | Some (_, Some (Conf_aux (Conf_string "forbid", _))) -> + | Some (_, Some (AD_aux (AD_string "forbid", _))) -> ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], env) - | Some (_, Some (Conf_aux (Conf_string "skip", _))) -> + | Some (_, Some (AD_aux (AD_string "skip", _))) -> ([DEF_aux (DEF_type (TD_aux (tdef, (l, empty_tannot))), def_annot)], Env.allow_user_undefined id env) - | Some (_, Some (Conf_aux (Conf_string "generate", _))) | None -> + | Some (_, Some (AD_aux (AD_string "generate", _))) | None -> let undefined_defs = Initial_check.generate_undefined_enum id ids in let undefined_defs, env = check_defs env undefined_defs in let def_annot = @@ -4554,7 +4559,7 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list | Some (attr_l, Some arg) -> typ_error (Hint ("When checking this enum", l, attr_l)) - ("Unrecognized argument to undefined attribute: " ^ string_of_config arg) + ("Unrecognized argument to undefined attribute: " ^ string_of_attribute_data arg) | Some (attr_l, None) -> typ_error (Hint ("When checking this enum", l, attr_l)) "No argument for undefined attribute" end @@ -4579,7 +4584,7 @@ let rec check_typedef : Env.t -> def_annot -> uannot type_def -> tannot def list let ranges = List.map (fun (f, r) -> (f, expand_range_synonyms r)) ranges |> List.to_seq |> Bindings.of_seq in - let def_annot = add_def_attribute l "bitfield" (Some (Conf_aux (Conf_num size, l))) def_annot in + let def_annot = add_def_attribute l "bitfield" (Some (AD_aux (AD_num size, l))) def_annot in let defs = DEF_aux (DEF_type (TD_aux (record_tdef, (l, empty_uannot))), def_annot) :: Bitfield.macro id size (Env.get_default_order env) ranges diff --git a/src/sail_doc_backend/docinfo.ml b/src/sail_doc_backend/docinfo.ml index bc9e075e7..83a04c4dc 100644 --- a/src/sail_doc_backend/docinfo.ml +++ b/src/sail_doc_backend/docinfo.ml @@ -75,7 +75,7 @@ open Libsail open Ast open Ast_defs open Ast_util -open Parse_ast.Config +open Parse_ast.Attribute_data (** In the case of latex, we generate files containing a sequence of commands that can simply be included. For other documentation @@ -431,7 +431,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct in match find_attribute_opt "split" attrs with | None -> None - | Some (Some (Conf_aux (Conf_string split_id, _))) -> ( + | Some (Some (AD_aux (AD_string split_id, _))) -> ( let split_id = mk_id split_id in let env = Type_check.env_of exp in match Type_check.Env.lookup_id split_id env with @@ -522,7 +522,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct let docinfo_for_mapcl n (MCL_aux (aux, (def_annot, _)) as clause) = let source = doc_loc def_annot.loc Type_check.strip_mapcl Pretty_print_sail.doc_mapcl clause in - let parse_wavedrom_attr = function Some (Conf_aux (Conf_string s, _)) -> Some s | Some _ | None -> None in + let parse_wavedrom_attr = function Some (AD_aux (AD_string s, _)) -> Some s | Some _ | None -> None in let wavedrom_attr = Option.bind (find_attribute_opt "wavedrom" def_annot.attrs) parse_wavedrom_attr in let left, left_wavedrom, right, right_wavedrom, body =