diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/anf.ml | 2 | ||||
| -rw-r--r-- | src/ast_util.ml | 3 | ||||
| -rw-r--r-- | src/ast_util.mli | 2 | ||||
| -rw-r--r-- | src/bytecode_util.ml | 5 | ||||
| -rw-r--r-- | src/c_backend.ml | 28 | ||||
| -rw-r--r-- | src/initial_check.ml | 7 | ||||
| -rw-r--r-- | src/lexer.mll | 1 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 4 | ||||
| -rw-r--r-- | src/parse_ast.ml | 3 | ||||
| -rw-r--r-- | src/parser.mly | 6 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 1 | ||||
| -rw-r--r-- | src/rewriter.ml | 4 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 66 | ||||
| -rw-r--r-- | src/type_check.mli | 2 |
15 files changed, 81 insertions, 55 deletions
@@ -307,7 +307,7 @@ let rec map_functions f (AE_aux (aexp, env, l)) = let pp_lvar lvar doc = match lvar with - | Register typ -> + | Register (_, _, typ) -> string "[R/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc | Local (Mutable, typ) -> string "[M/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc diff --git a/src/ast_util.ml b/src/ast_util.ml index c57cd21f..28b27e93 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -54,7 +54,7 @@ module Big_int = Nat_big_num type mut = Immutable | Mutable -type lvar = Register of typ | Enum of typ | Local of mut * typ | Unbound +type lvar = Register of effect * effect * typ | Enum of typ | Local of mut * typ | Unbound let no_annot = (Parse_ast.Unknown, ()) @@ -562,6 +562,7 @@ let string_of_base_effect_aux = function | BE_unspec -> "unspec" | BE_nondet -> "nondet" | BE_escape -> "escape" + | BE_config -> "configuration" (*| BE_lset -> "lset" | BE_lret -> "lret"*) diff --git a/src/ast_util.mli b/src/ast_util.mli index d23d56da..57e1a7cc 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -58,7 +58,7 @@ type mut = Immutable | Mutable (** [lvar] is the type of variables - they can either be registers, local mutable or immutable variables, nullary union constructors (i.e. None in option), or unbound identifiers *) -type lvar = Register of typ | Enum of typ | Local of mut * typ | Unbound +type lvar = Register of effect * effect * typ | Enum of typ | Local of mut * typ | Unbound val no_annot : unit annot val gen_loc : Parse_ast.l -> Parse_ast.l diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml index 9f23412e..2e6e1e29 100644 --- a/src/bytecode_util.ml +++ b/src/bytecode_util.ml @@ -287,8 +287,9 @@ let pp_cdef = function pp_keyword "function" ^^ pp_id id ^^ ret ^^ parens (separate_map (comma ^^ space) pp_id args) ^^ space ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace ^^ hardline - | CDEF_reg_dec (id, ctyp) -> - pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp + | CDEF_reg_dec (id, ctyp, instrs) -> + pp_keyword "register" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ space + ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace ^^ hardline | CDEF_type tdef -> pp_ctype_def tdef ^^ hardline | CDEF_let (n, bindings, instrs) -> diff --git a/src/c_backend.ml b/src/c_backend.ml index f630e91a..3b57c9ed 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -57,7 +57,7 @@ open PPrint open Value2 open Anf - + module Big_int = Nat_big_num let c_verbosity = ref 1 @@ -303,7 +303,7 @@ let rec c_aval ctx = function match lvar with | Local (_, typ) when is_stack_typ ctx typ -> AV_C_fragment (F_id id, typ) - | Register typ when is_stack_typ ctx typ -> + | Register (_, _, typ) when is_stack_typ ctx typ -> AV_C_fragment (F_id id, typ) | _ -> v end @@ -484,12 +484,12 @@ let rec instr_ctyps (I_aux (instr, aux)) = | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure -> [] let rec c_ast_registers = function - | CDEF_reg_dec (id, ctyp) :: ast -> (id, ctyp) :: c_ast_registers ast + | CDEF_reg_dec (id, ctyp, instrs) :: ast -> (id, ctyp, instrs) :: c_ast_registers ast | _ :: ast -> c_ast_registers ast | [] -> [] let cdef_ctyps ctx = function - | CDEF_reg_dec (_, ctyp) -> [ctyp] + | CDEF_reg_dec (_, ctyp, instrs) -> ctyp :: List.concat (List.map instr_ctyps instrs) | CDEF_spec (_, ctyps, ctyp) -> ctyp :: ctyps | CDEF_fundef (id, _, _, instrs) -> let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in @@ -1482,8 +1482,12 @@ let letdef_count = ref 0 (** Compile a Sail toplevel definition into an IR definition **) let rec compile_def ctx = function | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) -> - [CDEF_reg_dec (id, ctyp_of_typ ctx typ)], ctx - | DEF_reg_dec _ -> failwith "Unsupported register declaration" (* FIXME *) + [CDEF_reg_dec (id, ctyp_of_typ ctx typ, [])], ctx + | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) -> + let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow IdSet.empty (anf exp))) in + let setup, ctyp, call, cleanup = compile_aexp ctx aexp in + let instrs = setup @ [call (CL_id id)] @ cleanup in + [CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), _)) -> c_debug (lazy "Compiling VS"); @@ -2485,7 +2489,7 @@ let codegen_alloc = function | _ -> assert false let codegen_def' ctx = function - | CDEF_reg_dec (id, ctyp) -> + | CDEF_reg_dec (id, ctyp, _) -> string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline ^^ string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) @@ -2605,6 +2609,9 @@ let sgen_startup = function Printf.sprintf " startup_%s();" (sgen_id id) | _ -> assert false +let sgen_instr id ctx instr = + Pretty_print_sail.to_string (codegen_instr id ctx instr) + let is_cdef_finish = function | CDEF_startup _ -> true | _ -> false @@ -2729,11 +2736,12 @@ let compile_ast ctx (Defs defs) = let regs = c_ast_registers cdefs in - let register_init_clear (id, ctyp) = + let register_init_clear (id, ctyp, instrs) = if is_stack_ctyp ctyp then - [], [] + List.map (sgen_instr (mk_id "reg") ctx) instrs, [] else - [ Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ], + [ Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ] + @ List.map (sgen_instr (mk_id "reg") ctx) instrs, [ Printf.sprintf " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id) ] in diff --git a/src/initial_check.ml b/src/initial_check.ml index a774352d..af3d5fd5 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -319,7 +319,8 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect = | Parse_ast.BE_undef -> BE_undef | Parse_ast.BE_unspec -> BE_unspec | Parse_ast.BE_nondet -> BE_nondet - | Parse_ast.BE_escape -> BE_escape),l)) + | Parse_ast.BE_escape -> BE_escape + | Parse_ast.BE_config -> BE_config),l)) effects) | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None None ), l) @@ -857,7 +858,9 @@ let to_ast_dec (names,k_env,def_ord) (Parse_ast.DEC_aux(regdec,l)) = DEC_aux( (match regdec with | Parse_ast.DEC_reg(typ,id) -> - DEC_reg(to_ast_typ k_env def_ord typ,to_ast_id id) + DEC_reg(to_ast_typ k_env def_ord typ,to_ast_id id) + | Parse_ast.DEC_config(id,typ,exp) -> + DEC_config(to_ast_id id,to_ast_typ k_env def_ord typ,to_ast_exp k_env def_ord exp) | Parse_ast.DEC_alias(id,e) -> DEC_alias(to_ast_id id,to_ast_alias_spec k_env def_ord e) | Parse_ast.DEC_typ_alias(typ,id,e) -> diff --git a/src/lexer.mll b/src/lexer.mll index 621a1a44..16574ef1 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -179,6 +179,7 @@ let kw_table = ("unspec", (fun x -> Unspec)); ("nondet", (fun x -> Nondet)); ("escape", (fun x -> Escape)); + ("configuration", (fun _ -> Configuration)); ] diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 6de40977..369a325c 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -322,7 +322,7 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) = | Local (Immutable, _) | Unbound -> zencode ctx id | Enum _ -> zencode_upper ctx id | Register _ when is_passed_by_name (typ_of exp) -> zencode ctx id - | Register typ -> + | Register (_, _, typ) -> if !opt_trace_ocaml then let var = gensym () in let str_typ = parens (ocaml_string_typ (Rewrites.simple_typ typ) var) in @@ -339,7 +339,7 @@ and ocaml_assignment ctx (LEXP_aux (lexp_aux, _) as lexp) exp = | LEXP_cast (_, id) | LEXP_id id -> begin match Env.lookup_id id (env_of exp) with - | Register typ -> + | Register (_, _, typ) -> let var = gensym () in let traced_exp = if !opt_trace_ocaml then diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 2848edc0..26cb9df7 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -98,7 +98,7 @@ base_effect_aux = (* effect *) | BE_unspec (* unspecified values *) | BE_nondet (* nondeterminism from intra-instruction parallelism *) | BE_escape - + | BE_config type kid_aux = (* identifiers with kind, ticked to differntiate from program variables *) @@ -496,6 +496,7 @@ kind_def_aux = (* Definition body for elements of kind; many are shorthands for type dec_spec_aux = (* Register declarations *) DEC_reg of atyp * id + | DEC_config of id * atyp * exp | DEC_alias of id * exp | DEC_typ_alias of atyp * id * exp diff --git a/src/parser.mly b/src/parser.mly index 60ccc81f..0637d61a 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -178,7 +178,7 @@ let rec desugar_rchain chain s e = %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef %token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape -%token Repeat Until While Do Mutual Var Ref +%token Repeat Until While Do Mutual Var Ref Configuration %nonassoc Then %nonassoc Else @@ -634,6 +634,8 @@ effect: { mk_effect BE_nondet $startpos $endpos } | Escape { mk_effect BE_escape $startpos $endpos } + | Configuration + { mk_effect BE_config $startpos $endpos } effect_list: | effect @@ -1331,6 +1333,8 @@ val_spec_def: register_def: | Register id Colon typ { mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos } + | Register Configuration id Colon typ Eq exp + { mk_reg_dec (DEC_config ($3, $5, $7)) $startpos $endpos } default_def: | Default base_kind Inc diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 4b9fa6a9..d59bd132 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -487,6 +487,7 @@ let doc_mapdef (MD_aux (MD_mapping (id, typa, mapcls), _)) = let doc_dec (DEC_aux (reg,_)) = match reg with | DEC_reg (typ, id) -> separate space [string "register"; doc_id id; colon; doc_typ typ] + | DEC_config (id, typ, exp) -> separate space [string "register configuration"; doc_id id; colon; doc_typ typ; equals; doc_exp exp] | DEC_alias(id,alspec) -> string "ALIAS" | DEC_typ_alias(typ,id,alspec) -> string "ALIAS" diff --git a/src/rewriter.ml b/src/rewriter.ml index 6212e0da..b67f9c49 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -396,13 +396,15 @@ let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) let rewrite_def rewriters d = match d with + | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), annot)) -> + DEF_reg_dec (DEC_aux (DEC_config (id, typ, rewriters.rewrite_exp rewriters exp), annot)) | DEF_type _ | DEF_mapdef _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ | DEF_fixity _ -> d | DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef) | DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs) | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind) | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter") -let rewrite_defs_base rewriters (Defs defs) = +let rewrite_defs_base rewriters (Defs defs) = let rec rewrite ds = match ds with | [] -> [] | d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds) in diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 7bb82719..04668989 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -445,6 +445,8 @@ let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd let fv_of_rd consider_var (DEC_aux (d,_)) = match d with | DEC_reg(t,id) -> init_env (string_of_id id), fv_of_typ consider_var mt mt t + | DEC_config(id,t,exp) -> + init_env (string_of_id id), fv_of_typ consider_var mt mt t | DEC_alias(id,alias) -> init_env (string_of_id id),mt | DEC_typ_alias(t,id,alias) -> diff --git a/src/type_check.ml b/src/type_check.ml index fec146a0..0a29b6d6 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -82,10 +82,9 @@ let typ_print m = if !opt_tc_debug > 0 then prerr_endline (indent !depth ^ Lazy. let lvar_typ = function | Local (_, typ) -> typ - | Register typ -> typ + | Register (_, _, typ) -> typ | Enum typ -> typ - | _ -> assert false - + type type_error = (* First parameter is the error that caused us to start doing type coercions, the second is the errors encountered by all possible @@ -384,8 +383,8 @@ module Env : sig val get_flow : id -> t -> typ -> typ val remove_flow : id -> t -> t val is_register : id -> t -> bool - val get_register : id -> t -> typ - val add_register : id -> typ -> t -> t + val get_register : id -> t -> effect * effect * typ + val add_register : id -> effect -> effect -> typ -> t -> t val is_mutable : id -> t -> bool val get_constraints : t -> n_constraint list val add_constraint : n_constraint -> t -> t @@ -450,7 +449,7 @@ end = struct defined_val_specs : IdSet.t; locals : (mut * typ) Bindings.t; union_ids : (typquant * typ) Bindings.t; - registers : typ Bindings.t; + registers : (effect * effect * typ) Bindings.t; variants : (typquant * type_union list) Bindings.t; mappings : (typquant * typ * typ) Bindings.t; typ_vars : (Ast.l * base_kind_aux) KBindings.t; @@ -1048,14 +1047,14 @@ end = struct let get_casts env = env.casts - let add_register id typ env = + let add_register id reff weff typ env = wf_typ env typ; if Bindings.mem id env.registers then typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound") else begin typ_print (lazy ("Adding register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ)); - { env with registers = Bindings.add id typ env.registers } + { env with registers = Bindings.add id (reff, weff, typ) env.registers } end let get_locals env = env.locals @@ -1067,17 +1066,16 @@ end = struct Local (mut, if raw then typ else flow typ) with | Not_found -> - begin - try Register (Bindings.find id env.registers) with - | Not_found -> - begin - try - let (enum, _) = List.find (fun (enum, ctors) -> IdSet.mem id ctors) (Bindings.bindings env.enums) in - Enum (mk_typ (Typ_id enum)) - with - | Not_found -> Unbound - end - end + try + let reff, weff, typ = Bindings.find id env.registers in + Register (reff, weff, typ) + with + | Not_found -> + try + let (enum, _) = List.find (fun (enum, ctors) -> IdSet.mem id ctors) (Bindings.bindings env.enums) in + Enum (mk_typ (Typ_id enum)) + with + | Not_found -> Unbound let add_typ_var l kid k env = if KBindings.mem kid env.typ_vars @@ -2926,7 +2924,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as let infer_flexp = function | LEXP_id v -> begin match Env.lookup_id v env with - | Register typ -> typ, LEXP_id v, true + | Register (_, _, typ) -> typ, LEXP_id v, true | Local (Mutable, typ) -> typ, LEXP_id v, false | _ -> typ_error l "l-expression field is not a register or a local mutable type" end @@ -2938,7 +2936,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as | Enum _ -> typ_error l "Cannot vector assign to enumeration element" | Local (Immutable, vtyp) -> true, vtyp, false | Local (Mutable, vtyp) -> false, vtyp, false - | Register vtyp -> false, vtyp, true + | Register (_, _, vtyp) -> false, vtyp, true in let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in let inferred_exp = match access with @@ -2969,7 +2967,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as annot_assign tlexp checked_exp, env' | LEXP_id v when has_typ v env -> begin match Env.lookup_id ~raw:true v env with - | Local (Mutable, vtyp) | Register vtyp -> + | Local (Mutable, vtyp) | Register (_, _, vtyp) -> let checked_exp = crule check_exp env exp vtyp in let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in annot_assign tlexp checked_exp, env' @@ -2993,10 +2991,10 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = subtyp l env typ typ_annot; subtyp l env typ_annot vtyp; annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env - | Register vtyp -> + | Register (_, weff, vtyp) -> subtyp l env typ typ_annot; subtyp l env typ_annot vtyp; - annot_lexp_effect (LEXP_cast (typ_annot, v)) typ (mk_effect [BE_wreg]), env + annot_lexp_effect (LEXP_cast (typ_annot, v)) typ weff, env | Unbound -> subtyp l env typ typ_annot; annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env @@ -3016,7 +3014,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | Local (Immutable, _) | Enum _ -> typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, Env.remove_flow v env - | Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env + | Register (_, weff, vtyp) -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ weff, env | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env end | LEXP_tup lexps -> @@ -3048,7 +3046,7 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) = begin match Env.lookup_id v env with | Local (Mutable, typ) -> annot_lexp (LEXP_id v) typ (* Probably need to remove flows here *) - | Register typ -> annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]) + | Register (_, weff, typ) -> annot_lexp_effect (LEXP_id v) typ weff | Local (Immutable, _) | Enum _ -> typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v) | Unbound -> @@ -3115,13 +3113,13 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) = end | LEXP_field (LEXP_aux (LEXP_id v, _), fid) -> (* FIXME: will only work for ASL *) - let rec_id = + let rec_id, weff = match Env.lookup_id v env with - | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id + | Register (_, weff, Typ_aux (Typ_id rec_id, _)) -> rec_id, weff | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here") in let typq, _, ret_typ, _ = Env.get_accessor rec_id fid env in - annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg]) + annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ weff | _ -> typ_error l ("Unhandled l-expression " ^ string_of_lexp lexp) and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = @@ -3134,7 +3132,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = begin match Env.lookup_id v env with | Local (_, typ) | Enum typ -> annot_exp (E_id v) typ - | Register typ -> annot_exp_effect (E_id v) typ (mk_effect [BE_rreg]) + | Register (reff, _, typ) -> annot_exp_effect (E_id v) typ reff | Unbound -> typ_error l ("Identifier " ^ string_of_id v ^ " is unbound") end | E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit) @@ -3306,7 +3304,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let (_, typ) = Bindings.find id (Env.get_locals env) in annot_exp (E_ref id) (ref_typ typ) | E_ref id when Env.is_register id env -> - let typ = Env.get_register id env in + let _, _, typ = Env.get_register id env in annot_exp (E_ref id) (register_typ typ) | _ -> typ_error l ("Cannot infer type of: " ^ string_of_exp exp) @@ -4460,8 +4458,12 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t = | DEF_default default -> check_default env default | DEF_overload (id, ids) -> [DEF_overload (id, ids)], Env.add_overloads id ids env | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, _))) -> - let env = Env.add_register id typ env in + let env = Env.add_register id (mk_effect [BE_rreg]) (mk_effect [BE_wreg]) typ env in [DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, Some (env, typ, no_effect))))], env + | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), (l, _))) -> + let checked_exp = crule check_exp env (strip_exp exp) typ in + let env = Env.add_register id no_effect (mk_effect [BE_config]) typ env in + [DEF_reg_dec (DEC_aux (DEC_config (id, typ, checked_exp), (l, Some (env, typ, no_effect))))], env | DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err () | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err () | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker") diff --git a/src/type_check.mli b/src/type_check.mli index 62fd846e..4f87e4e6 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -106,7 +106,7 @@ module Env : sig val update_val_spec : id -> typquant * typ -> t -> t - val get_register : id -> t -> typ + val get_register : id -> t -> effect * effect * typ (** Return all the identifiers in an enumeration. Throws a type error if the enumeration doesn't exist. *) |