diff options
| -rw-r--r-- | src/ast_util.ml | 36 | ||||
| -rw-r--r-- | src/ast_util.mli | 1 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 238 | ||||
| -rw-r--r-- | src/rewriter.ml | 99 | ||||
| -rw-r--r-- | src/type_check.ml | 93 | ||||
| -rw-r--r-- | src/type_check.mli | 4 |
6 files changed, 332 insertions, 139 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 01509ab8..cc21f2af 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -400,11 +400,37 @@ let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) = | _, _ -> false let rec is_nexp_constant (Nexp_aux (nexp, _)) = match nexp with -| Nexp_id _ | Nexp_var _ -> false -| Nexp_constant _ -> true -| Nexp_times (n1, n2) | Nexp_sum (n1, n2) | Nexp_minus (n1, n2) -> - is_nexp_constant n1 && is_nexp_constant n2 -| Nexp_exp n | Nexp_neg n -> is_nexp_constant n + | Nexp_id _ | Nexp_var _ -> false + | Nexp_constant _ -> true + | Nexp_times (n1, n2) | Nexp_sum (n1, n2) | Nexp_minus (n1, n2) -> + is_nexp_constant n1 && is_nexp_constant n2 + | Nexp_exp n | Nexp_neg n -> is_nexp_constant n + +let rec simplify_nexp (Nexp_aux (nexp, l)) = + let rewrap n = Nexp_aux (n, l) in + let try_binop op n1 n2 c = (match simplify_nexp n1, simplify_nexp n2 with + | Nexp_aux (Nexp_constant i1, _), Nexp_aux (Nexp_constant i2, _) -> + rewrap (Nexp_constant (op i1 i2)) + | n1, n2 -> rewrap (c n1 n2)) in + match nexp with + | Nexp_times (n1, n2) -> try_binop ( * ) n1 n2 (fun n1 n2 -> Nexp_times (n1, n2)) + | Nexp_sum (n1, n2) -> try_binop ( + ) n1 n2 (fun n1 n2 -> Nexp_sum (n1, n2)) + | Nexp_minus (n1, n2) -> try_binop ( - ) n1 n2 (fun n1 n2 -> Nexp_minus (n1, n2)) + | Nexp_exp n -> + (match simplify_nexp n with + | Nexp_aux (Nexp_constant i, _) -> + rewrap (Nexp_constant (power 2 i)) + | n -> rewrap (Nexp_exp n)) + | Nexp_neg n -> + (match simplify_nexp n with + | Nexp_aux (Nexp_constant i, _) -> + rewrap (Nexp_constant (-i)) + | n -> rewrap (Nexp_neg n)) + | _ -> rewrap nexp + (* | Nexp_sum of nexp * nexp (* sum *) + | Nexp_minus of nexp * nexp (* subtraction *) + | Nexp_exp of nexp (* exponential *) + | Nexp_neg of nexp (* For internal use *) *) let rec is_number (Typ_aux (t,_)) = match t with diff --git a/src/ast_util.mli b/src/ast_util.mli index 8a07b83f..ae340839 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -120,6 +120,7 @@ end val nexp_frees : nexp -> KidSet.t val nexp_identical : nexp -> nexp -> bool val is_nexp_constant : nexp -> bool +val simplify_nexp : nexp -> nexp val is_number : typ -> bool val is_vector_typ : typ -> bool diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 1f557e74..09f1a466 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -160,7 +160,7 @@ let doc_typ_lem, doc_atomic_typ_lem = let tpp = separate_map (space ^^ star ^^ space) (app_typ regtypes false) typs in if atyp_needed then parens tpp else tpp | _ -> app_typ regtypes atyp_needed ty - and app_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with + and app_typ regtypes atyp_needed ((Typ_aux (t, l)) as ty) = match t with | Typ_app(Id_aux (Id "vector", _), [ Typ_arg_aux (Typ_arg_nexp n, _); Typ_arg_aux (Typ_arg_nexp m, _); @@ -168,19 +168,16 @@ let doc_typ_lem, doc_atomic_typ_lem = Typ_arg_aux (Typ_arg_typ elem_typ, _)]) -> let tpp = match elem_typ with | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> - let len = match m with - | (Nexp_aux(Nexp_constant i,_)) -> string "ty" ^^ doc_int i - | _ -> doc_nexp m in - string "bitvector" ^^ space ^^ len + (match simplify_nexp m with + | (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i + | _ -> raise (Reporting_basic.err_unreachable l + "cannot pretty-print bitvector type with non-constant length")) | _ -> string "vector" ^^ space ^^ typ regtypes elem_typ in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> - (* TODO: Better distinguish register names and contents? - The former are represented in the Lem library using a type - "register" (without parameters), the latter just using the content - type (e.g. "bitvector ty64"). We assume the latter is meant here - and drop the "register" keyword. *) - fn_typ regtypes atyp_needed etyp + (* TODO: Better distinguish register names and contents? *) + (* fn_typ regtypes atyp_needed etyp *) + (string "register") | Typ_app(Id_aux (Id "range", _),_) -> (string "integer") | Typ_app(Id_aux (Id "implicit", _),_) -> @@ -192,13 +189,13 @@ let doc_typ_lem, doc_atomic_typ_lem = if atyp_needed then parens tpp else tpp | _ -> atomic_typ regtypes atyp_needed ty and atomic_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with - | Typ_id (Id_aux (Id "bool",_)) -> string "bitU" - | Typ_id (Id_aux (Id "boolean",_)) -> string "bitU" + | Typ_id (Id_aux (Id "bool",_)) -> string "bool" + | Typ_id (Id_aux (Id "boolean",_)) -> string "bool" | Typ_id (Id_aux (Id "bit",_)) -> string "bitU" | Typ_id (id) -> - if List.exists ((=) (string_of_id id)) regtypes + (*if List.exists ((=) (string_of_id id)) regtypes then string "register" - else doc_id_lem_type id + else*) doc_id_lem_type id | Typ_var v -> doc_var v | Typ_wild -> underscore | Typ_app _ | Typ_tup _ | Typ_fn _ -> @@ -213,39 +210,67 @@ let doc_typ_lem, doc_atomic_typ_lem = | Typ_arg_effect e -> empty in typ', atomic_typ +(* Check for variables in types that would be pretty-printed. + In particular, in case of vector types, only the element type and the + length argument are checked for variables, and the latter only if it is + a bitvector; for other types of vectors, the length is not pretty-printed + in the type, and the start index is never pretty-printed in vector types. *) +let rec contains_t_pp_var (Typ_aux (t,a) as typ) = match t with + | Typ_wild -> true + | Typ_id _ -> false + | Typ_var _ -> true + | Typ_fn (t1,t2,_) -> contains_t_pp_var t1 || contains_t_pp_var t2 + | Typ_tup ts -> List.exists contains_t_pp_var ts + | Typ_app (c,targs) -> + if Ast_util.is_number typ then false + else if is_bitvector_typ typ then + let (_,length,_,_) = vector_typ_args_of typ in + not (is_nexp_constant (simplify_nexp length)) + else List.exists contains_t_arg_pp_var targs +and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with + | Typ_arg_typ t -> contains_t_pp_var t + | Typ_arg_nexp nexp -> not (is_nexp_constant (simplify_nexp nexp)) + | _ -> false + let doc_tannot_lem regtypes eff typ = - let ta = doc_typ_lem regtypes typ in - if eff then string " : M " ^^ parens ta - else string " : " ^^ ta + if contains_t_pp_var typ then empty + else + let ta = doc_typ_lem regtypes typ in + if eff then string " : M " ^^ parens ta + else string " : " ^^ ta (* doc_lit_lem gets as an additional parameter the type information from the * expression around it: that's a hack, but how else can we distinguish between * undefined values of different types ? *) -let doc_lit_lem in_pat (L_aux(lit,l)) a = - utf8string (match lit with - | L_unit -> "()" - | L_zero -> "B0" - | L_one -> "B1" - | L_false -> "B0" - | L_true -> "B1" +let doc_lit_lem regtypes in_pat (L_aux(lit,l)) a = + match lit with + | L_unit -> utf8string "()" + | L_zero -> utf8string "B0" + | L_one -> utf8string "B1" + | L_false -> utf8string "false" + | L_true -> utf8string "true" | L_num i -> let ipp = string_of_int i in - if in_pat then "("^ipp^":nn)" - else if i < 0 then "((0"^ipp^"):ii)" - else "("^ipp^":ii)" + utf8string ( + if in_pat then "("^ipp^":nn)" + else if i < 0 then "((0"^ipp^"):ii)" + else "("^ipp^":ii)") | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) | L_undef -> (match a with - | Some (_, Typ_aux (t,_), _) -> + | Some (_, (Typ_aux (t,_) as typ), _) -> (match t with | Typ_id (Id_aux (Id "bit", _)) - | Typ_app (Id_aux (Id "register", _),_) -> "UndefinedRegister 0" - | Typ_id (Id_aux (Id "string", _)) -> "\"\"" - | _ -> "(failwith \"undefined value of unsupported type\")") - | _ -> "(failwith \"undefined value of unsupported type\")") - | L_string s -> "\"" ^ s ^ "\"" - | L_real s -> s (* TODO What's the Lem syntax for reals? *)) + | Typ_app (Id_aux (Id "register", _),_) -> utf8string "UndefinedRegister 0" + | Typ_id (Id_aux (Id "string", _)) -> utf8string "\"\"" + | _ -> + parens + ((utf8string "(failwith \"undefined value of unsupported type\")") ^^ + (doc_tannot_lem regtypes false typ))) + | _ -> utf8string "(failwith \"undefined value of unsupported type\")") + | L_string s -> utf8string ("\"" ^ s ^ "\"") + | L_real s -> utf8string s (* TODO What's the Lem syntax for reals? *) (* typ_doc is the doc for the type being quantified *) @@ -267,14 +292,17 @@ let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p w (parens (separate_map comma (doc_pat_lem regtypes true) pats)) in if apat_needed then parens ppp else ppp | P_app(id,[]) -> doc_id_lem_ctor id - | P_lit lit -> doc_lit_lem true lit annot + | P_lit lit -> doc_lit_lem regtypes true lit annot | P_wild -> underscore | P_id id -> begin match id with | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *) | _ -> doc_id_lem id end | P_as(p,id) -> parens (separate space [doc_pat_lem regtypes true p; string "as"; doc_id_lem id]) - | P_typ(typ,p) -> parens (doc_op colon (doc_pat_lem regtypes true p) (doc_typ_lem regtypes typ)) + | P_typ(typ,p) -> + let doc_p = doc_pat_lem regtypes true p in + if contains_t_pp_var typ then doc_p + else parens (doc_op colon doc_p (doc_typ_lem regtypes typ)) | P_vector pats -> let ppp = (separate space) @@ -300,27 +328,6 @@ and contains_bitvector_typ_arg (Typ_arg_aux (targ, _)) = match targ with | Typ_arg_typ t -> contains_bitvector_typ t | _ -> false -(* Check for variables in types that would be pretty-printed. - In particular, in case of vector types, only the element type and the - length argument are checked for variables, and the latter only if it is - a bitvector; for other types of vectors, the length is not pretty-printed - in the type, and the start index is never pretty-printed in vector types. *) -let rec contains_t_pp_var (Typ_aux (t,a) as typ) = match t with - | Typ_wild -> true - | Typ_id _ -> false - | Typ_var _ -> true - | Typ_fn (t1,t2,_) -> contains_t_pp_var t1 || contains_t_pp_var t2 - | Typ_tup ts -> List.exists contains_t_pp_var ts - | Typ_app (c,targs) -> - if is_bitvector_typ typ then - let (_,length,_,_) = vector_typ_args_of typ in - not (is_nexp_constant ((*normalize_nexp*) length)) - else List.exists contains_t_arg_pp_var targs -and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with - | Typ_arg_typ t -> contains_t_pp_var t - | Typ_arg_nexp nexp -> not (is_nexp_constant ((*normalize_nexp*) nexp)) - | _ -> false - let prefix_recordtype = true let report = Reporting_basic.err_unreachable let doc_exp_lem, doc_let_lem = @@ -387,7 +394,9 @@ let doc_exp_lem, doc_let_lem = | _ -> (prefix 2 1) (string "write_reg") (doc_lexp_deref_lem regtypes le ^/^ expY e)) | E_vector_append(le,re) -> - let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in + raise (Reporting_basic.err_unreachable l + "E_vector_access should have been rewritten before pretty-printing") + (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let (call,ta,aexp_needed) = if is_bitvector_typ t then if not (contains_t_pp_var t) @@ -396,12 +405,12 @@ let doc_exp_lem, doc_let_lem = else ("vector_concat",empty,aexp_needed) in let epp = align (group (separate space [string call;expY le;expY re])) ^^ ta in - if aexp_needed then parens epp else epp + if aexp_needed then parens epp else epp *) | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re) | E_if(c,t,e) -> let (E_aux (_,(_,cannot))) = c in let epp = - separate space [string "if";group (align (string "bitU_to_bool" ^//^ group (expY c)))] ^^ + separate space [string "if";group (expY c)] ^^ break 1 ^^ (prefix 2 1 (string "then") (expN t)) ^^ (break 1) ^^ (prefix 2 1 (string "else") (expN e)) in @@ -434,7 +443,7 @@ let doc_exp_lem, doc_let_lem = (prefix 1 1 (separate space [string "fun";expY id;varspp;arrow]) (expN body)) ) ) - | Id_aux (Id "append",_) -> + (* | Id_aux (Id "append",_) -> let [e1;e2] = args in let epp = align (expY e1 ^^ space ^^ string "++" ^//^ expY e2) in if aexp_needed then parens (align epp) else epp @@ -460,7 +469,7 @@ let doc_exp_lem, doc_let_lem = | Id_aux (Id "bool_not", _) -> let [a] = args in let epp = align (string "~" ^^ expY a) in - if aexp_needed then parens (align epp) else epp + if aexp_needed then parens (align epp) else epp *) | _ -> begin match annot with | Some (env, _, _) when (is_ctor env f) -> @@ -473,15 +482,16 @@ let doc_exp_lem, doc_let_lem = parens (separate_map comma (expV false) args) in if aexp_needed then parens (align epp) else epp | _ -> - let call = (*match annot with - | Base(_,External (Some n),_,_,_,_) -> string n - | _ ->*) doc_id_lem f in + let call = match annot with + | Some (env, _, _) when Env.is_extern f env -> + string (Env.get_extern f env) + | _ -> doc_id_lem f in let argspp = match args with | [arg] -> expV true arg | args -> parens (align (separate_map (comma ^^ break 0) (expV false) args)) in let epp = align (call ^//^ argspp) in let (taepp,aexp_needed) = - let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in + let t = (*Env.base_typ_of (env_of full_exp)*) (typ_of full_exp) in let eff = effect_of full_exp in if contains_bitvector_typ t && not (contains_t_pp_var t) then (align epp ^^ (doc_tannot_lem regtypes (effectful eff) t), true) @@ -490,7 +500,9 @@ let doc_exp_lem, doc_let_lem = end end | E_vector_access (v,e) -> - let eff = effect_of full_exp in + raise (Reporting_basic.err_unreachable l + "E_vector_access should have been rewritten before pretty-printing") + (* let eff = effect_of full_exp in let epp = if has_effect eff BE_rreg then separate space [string "read_reg_bit";expY v;expY e] @@ -498,9 +510,11 @@ let doc_exp_lem, doc_let_lem = let tv = typ_of v in let call = if is_bitvector_typ tv then "bvaccess" else "access" in separate space [string call;expY v;expY e] in - if aexp_needed then parens (align epp) else epp + if aexp_needed then parens (align epp) else epp*) | E_vector_subrange (v,e1,e2) -> - let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in + raise (Reporting_basic.err_unreachable l + "E_vector_access should have been rewritten before pretty-printing") + (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let eff = effect_of full_exp in let (epp,aexp_needed) = if has_effect eff BE_rreg then @@ -515,22 +529,22 @@ let doc_exp_lem, doc_let_lem = then (bepp ^^ doc_tannot_lem regtypes false t, true) else (bepp, aexp_needed) else (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2, aexp_needed) in - if aexp_needed then parens (align epp) else epp + if aexp_needed then parens (align epp) else epp *) | E_field((E_aux(_,(l,fannot)) as fexp),id) -> let ft = typ_of_annot (l,fannot) in (match fannot with - | Some(env, ftyp, _) when is_regtyp ftyp env -> - let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in + | Some(env, (Typ_aux (Typ_id tid, _)), _) + | Some(env, (Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]), _)), _) + when Env.is_regtyp tid env -> + let t = (* Env.base_typ_of (env_of full_exp) *) (typ_of full_exp) in let eff = effect_of full_exp in - let field_f = string - (if is_bit_typ t - then "read_reg_bitfield" - else "read_reg_field") in + let field_f = string "get" ^^ underscore ^^ + doc_id_lem tid ^^ underscore ^^ doc_id_lem id in let (ta,aexp_needed) = if contains_bitvector_typ t && not (contains_t_pp_var t) then (doc_tannot_lem regtypes (effectful eff) t, true) else (empty, aexp_needed) in - let epp = field_f ^^ space ^^ (expY fexp) ^^ space ^^ string_lit (doc_id_lem id) in + let epp = field_f ^^ space ^^ (expY fexp) in if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta) | Some(env, (Typ_aux (Typ_id tid, _)), _) when Env.is_record tid env -> let fname = @@ -550,7 +564,7 @@ let doc_exp_lem, doc_let_lem = let base_typ = Env.base_typ_of env typ in if has_effect eff BE_rreg then let epp = separate space [string "read_reg";doc_id_lem id] in - if contains_bitvector_typ base_typ && not (contains_t_pp_var base_typ) + if is_bitvector_typ base_typ && not (contains_t_pp_var base_typ) then parens (epp ^^ doc_tannot_lem regtypes true base_typ) else epp else if is_ctor env id then doc_id_lem_ctor id @@ -588,7 +602,7 @@ let doc_exp_lem, doc_let_lem = separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in if aexp_needed then parens (align epp) else epp )*) - | E_lit lit -> doc_lit_lem false lit annot + | E_lit lit -> doc_lit_lem regtypes false lit annot | E_cast(typ,e) -> expV aexp_needed e (* (match annot with @@ -649,7 +663,7 @@ let doc_exp_lem, doc_let_lem = | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp]) | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])}) ->*) let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in - let start = match start with + let start = match simplify_nexp start with | Nexp_aux (Nexp_constant i, _) -> string_of_int i | _ -> if dir then "0" else string_of_int (List.length exps) in let expspp = @@ -681,10 +695,10 @@ let doc_exp_lem, doc_let_lem = if is_vector_typ t then vector_typ_args_of t else raise (Reporting_basic.err_unreachable l "E_vector_indexed of non-vector type") in let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in - let start = match start with + let start = match simplify_nexp start with | Nexp_aux (Nexp_constant i, _) -> string_of_int i | _ -> if dir then "0" else string_of_int (List.length iexps) in - let size = match len with + let size = match simplify_nexp len with | Nexp_aux (Nexp_constant i, _)-> string_of_int i | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) -> string_of_int (Util.power 2 i) @@ -885,8 +899,8 @@ let doc_exp_lem, doc_let_lem = | E_internal_return (e1) -> separate space [string "return"; expY e1;] | E_sizeof nexp -> - (match nexp with - | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem false (L_aux (L_num i, l)) annot + (match simplify_nexp nexp with + | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem regtypes false (L_aux (L_num i, l)) annot | _ -> raise (Reporting_basic.err_unreachable l "pretty-printing non-constant sizeof expressions to Lem not supported")) @@ -943,7 +957,7 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with | BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2)) | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2) -let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with +let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with | TD_abbrev(id,nm,typschm) -> doc_op equals (concat [string "type"; space; doc_id_lem_type id]) (doc_typschm_lem regtypes typschm) @@ -967,6 +981,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with | Id_aux ((Id "regfp"),_) -> empty | Id_aux ((Id "niafp"),_) -> empty | Id_aux ((Id "diafp"),_) -> empty + | Id_aux ((Id "option"),_) -> empty | _ -> let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in let typ_pp = @@ -1138,7 +1153,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with fromToInterpValuePP ^^ hardline else empty) | TD_register(id,n1,n2,rs) -> - match n1,n2 with + match n1, n2 with | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id); doc_range_lem r;]) in @@ -1149,14 +1164,46 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with (string "Register_field" ^^ space ^^ string_lit(doc_id_lem id)) in*) let dir_b = i1 < i2 in let dir = string (if dir_b then "true" else "false") in + let dir_suffix = (if dir_b then "_inc" else "_dec") in + let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in let size = if dir_b then i2-i1 +1 else i1-i2 + 1 in - (doc_op equals) + let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in + let tannot = doc_tannot_lem regtypes false vtyp in + let doc_field (fr, fid) = + let i, j = match fr with + | BF_aux (BF_single i, _) -> (i, i) + | BF_aux (BF_range (i, j), _) -> (i, j) + | _ -> raise (Reporting_basic.err_unreachable l "unsupported field type") in + let get, set = + "bitvector_subrange" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ")", + "bitvector_update" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ", v)" in + doc_op equals + (concat [string "let get_"; doc_id_lem id; underscore; doc_id_lem fid; + space; parens (string "reg" ^^ tannot)]) (string get) ^^ + hardline ^^ + doc_op equals + (concat [string "let set_"; doc_id_lem id; underscore; doc_id_lem fid; + space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set) + in + doc_op equals + (concat [string "type";space;doc_id_lem id]) + (doc_typ_lem regtypes vtyp) + ^^ hardline ^^ + doc_op equals (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"]) (string "Register" ^^ space ^^ align (separate space [string "regname"; doc_int size; doc_int i1; dir; break 0 ^^ brackets (align doc_rids)])) - (*^^ hardline ^^ - separate_map hardline doc_rfield rs *) + ^^ hardline ^^ + doc_op equals + (concat [string "let";space;string "cast_";doc_id_lem id;space;string "reg"]) + (string "reg") + ^^ hardline ^^ + doc_op equals + (concat [string "let";space;string "cast_to_";doc_id_lem id;space;string "reg"]) + (string "reg") + ^^ hardline ^^ + separate_map hardline doc_field rs let doc_rec_lem (Rec_aux(r,_)) = match r with | Rec_nonrec -> space @@ -1226,7 +1273,7 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot)) let named_pat = P_aux (P_app (Id_aux (Id ctor,l),named_argspat),pannot) in let doc_arg idx (P_aux (p,(l,a))) = match p with | P_as (pat,id) -> doc_id_lem id - | P_lit lit -> doc_lit_lem false lit a + | P_lit lit -> doc_lit_lem regtypes false lit a | P_id id -> doc_id_lem id | _ -> string ("arg" ^ string_of_int idx) in let clauses = @@ -1252,17 +1299,16 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot)) -let doc_dec_lem (DEC_aux (reg,(l,annot))) = +let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = match reg with | DEC_reg(typ,id) -> + let env = env_of_annot annot in (match typ with - | Typ_aux (Typ_id idt, _) -> + | Typ_aux (Typ_id idt, _) when Env.is_regtyp idt env -> separate space [string "let";doc_id_lem id;equals; string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline | _ -> - let rt = (match annot with - | Some (env, _, _) -> Env.base_typ_of env typ - | _ -> typ) in + let rt = Env.base_typ_of env typ in if is_vector_typ rt then let (start, size, order, etyp) = vector_typ_args_of rt in if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then diff --git a/src/rewriter.ml b/src/rewriter.ml index 33fe3c25..1f8452ba 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -66,7 +66,13 @@ let effect_of_fexp (FE_aux (_,(_,a))) = effect_of_annot a let effect_of_fexps (FES_aux (FES_Fexps (fexps,_),_)) = List.fold_left union_effects no_effect (List.map effect_of_fexp fexps) let effect_of_opt_default (Def_val_aux (_,(_,a))) = effect_of_annot a -let effect_of_pexp (Pat_aux (_,(_,a))) = effect_of_annot a +(* The typechecker does not seem to annotate pexps themselves *) +let effect_of_pexp (Pat_aux (pexp,(_,a))) = match a with + | Some (_, _, eff) -> eff + | None -> + (match pexp with + | Pat_exp (_, e) -> effect_of e + | Pat_when (_, g, e) -> union_effects (effect_of g) (effect_of e)) let effect_of_lb (LB_aux (_,(_,a))) = effect_of_annot a let get_loc_exp (E_aux (_,(l,_))) = l @@ -1048,6 +1054,7 @@ let rewrite_sizeof (Defs defs) = Id_aux (Id op, Parse_ast.Unknown), E_aux (e_sizeof nmap nexp2, simple_annot l (atom_typ nexp2)) ) in + let (Nexp_aux (nexp, l) as nexp_aux) = simplify_nexp nexp_aux in (match nexp with | Nexp_constant i -> E_lit (L_aux (L_num i, l)) | Nexp_times (nexp1, nexp2) -> binop nexp1 "*" nexp2 @@ -1058,14 +1065,15 @@ let rewrite_sizeof (Defs defs) = (* Rewrite calls to functions which have had parameters added to pass values of type-level variables; these are added as sizeof expressions first, and then further rewritten as above. *) - let e_app_aux param_map (exp, ((l,_) as annot)) = + let e_app_aux param_map ((exp, exp_orig), ((l,_) as annot)) = let full_exp = E_aux (exp, annot) in + let orig_exp = E_aux (exp_orig, annot) in match exp with | E_app (f, args) -> if Bindings.mem f param_map then (* Retrieve instantiation of the type variables of the called function - for the given parameters in the current environment *) - let inst = instantiation_of full_exp in + for the given parameters in the original environment *) + let inst = instantiation_of orig_exp in let kid_exp kid = begin match KBindings.find kid inst with | U_nexp nexp -> E_aux (E_sizeof nexp, simple_annot l (atom_typ nexp)) @@ -1075,9 +1083,75 @@ let rewrite_sizeof (Defs defs) = " of function " ^ string_of_id f)) end in let kid_exps = List.map kid_exp (KidSet.elements (Bindings.find f param_map)) in - E_aux (E_app (f, kid_exps @ args), annot) - else full_exp - | _ -> full_exp in + (E_aux (E_app (f, kid_exps @ args), annot), orig_exp) + else (full_exp, orig_exp) + | _ -> (full_exp, orig_exp) in + + (* Plug this into a folding algorithm that also keeps around a copy of the + original expressions, which we use to infer instantiations of type variables + in the original environments *) + let copy_exp_alg = + { e_block = (fun es -> let (es, es') = List.split es in (E_block es, E_block es')) + ; e_nondet = (fun es -> let (es, es') = List.split es in (E_nondet es, E_nondet es')) + ; e_id = (fun id -> (E_id id, E_id id)) + ; e_lit = (fun lit -> (E_lit lit, E_lit lit)) + ; e_cast = (fun (typ,(e,e')) -> (E_cast (typ,e), E_cast (typ,e'))) + ; e_app = (fun (id,es) -> let (es, es') = List.split es in (E_app (id,es), E_app (id,es'))) + ; e_app_infix = (fun ((e1,e1'),id,(e2,e2')) -> (E_app_infix (e1,id,e2), E_app_infix (e1',id,e2'))) + ; e_tuple = (fun es -> let (es, es') = List.split es in (E_tuple es, E_tuple es')) + ; e_if = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_if (e1,e2,e3), E_if (e1',e2',e3'))) + ; e_for = (fun (id,(e1,e1'),(e2,e2'),(e3,e3'),order,(e4,e4')) -> (E_for (id,e1,e2,e3,order,e4), E_for (id,e1',e2',e3',order,e4'))) + ; e_vector = (fun es -> let (es, es') = List.split es in (E_vector es, E_vector es')) + ; e_vector_indexed = (fun (es,(opt2,opt2')) -> let (is, es) = List.split es in let (es, es') = List.split es in let (es, es') = (List.combine is es, List.combine is es') in (E_vector_indexed (es,opt2), E_vector_indexed (es',opt2'))) + ; e_vector_access = (fun ((e1,e1'),(e2,e2')) -> (E_vector_access (e1,e2), E_vector_access (e1',e2'))) + ; e_vector_subrange = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_vector_subrange (e1,e2,e3), E_vector_subrange (e1',e2',e3'))) + ; e_vector_update = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_vector_update (e1,e2,e3), E_vector_update (e1',e2',e3'))) + ; e_vector_update_subrange = (fun ((e1,e1'),(e2,e2'),(e3,e3'),(e4,e4')) -> (E_vector_update_subrange (e1,e2,e3,e4), E_vector_update_subrange (e1',e2',e3',e4'))) + ; e_vector_append = (fun ((e1,e1'),(e2,e2')) -> (E_vector_append (e1,e2), E_vector_append (e1',e2'))) + ; e_list = (fun es -> let (es, es') = List.split es in (E_list es, E_list es')) + ; e_cons = (fun ((e1,e1'),(e2,e2')) -> (E_cons (e1,e2), E_cons (e1',e2'))) + ; e_record = (fun (fexps, fexps') -> (E_record fexps, E_record fexps')) + ; e_record_update = (fun ((e1,e1'),(fexp,fexp')) -> (E_record_update (e1,fexp), E_record_update (e1',fexp'))) + ; e_field = (fun ((e1,e1'),id) -> (E_field (e1,id), E_field (e1',id))) + ; e_case = (fun ((e1,e1'),pexps) -> let (pexps, pexps') = List.split pexps in (E_case (e1,pexps), E_case (e1',pexps'))) + ; e_let = (fun ((lb,lb'),(e2,e2')) -> (E_let (lb,e2), E_let (lb',e2'))) + ; e_assign = (fun ((lexp,lexp'),(e2,e2')) -> (E_assign (lexp,e2), E_assign (lexp',e2'))) + ; e_sizeof = (fun nexp -> (E_sizeof nexp, E_sizeof nexp)) + ; e_exit = (fun (e1,e1') -> (E_exit (e1), E_exit (e1'))) + ; e_return = (fun (e1,e1') -> (E_return e1, E_return e1')) + ; e_assert = (fun ((e1,e1'),(e2,e2')) -> (E_assert(e1,e2), E_assert(e1',e2')) ) + ; e_internal_cast = (fun (a,(e1,e1')) -> (E_internal_cast (a,e1), E_internal_cast (a,e1'))) + ; e_internal_exp = (fun a -> (E_internal_exp a, E_internal_exp a)) + ; e_internal_exp_user = (fun (a1,a2) -> (E_internal_exp_user (a1,a2), E_internal_exp_user (a1,a2))) + ; e_comment = (fun c -> (E_comment c, E_comment c)) + ; e_comment_struc = (fun (e,e') -> (E_comment_struc e, E_comment_struc e')) + ; e_internal_let = (fun ((lexp,lexp'), (e2,e2'), (e3,e3')) -> (E_internal_let (lexp,e2,e3), E_internal_let (lexp',e2',e3'))) + ; e_internal_plet = (fun (pat, (e1,e1'), (e2,e2')) -> (E_internal_plet (pat,e1,e2), E_internal_plet (pat,e1',e2'))) + ; e_internal_return = (fun (e,e') -> (E_internal_return e, E_internal_return e')) + ; e_aux = (fun ((e,e'),annot) -> (E_aux (e,annot), E_aux (e',annot))) + ; lEXP_id = (fun id -> (LEXP_id id, LEXP_id id)) + ; lEXP_memory = (fun (id,es) -> let (es, es') = List.split es in (LEXP_memory (id,es), LEXP_memory (id,es'))) + ; lEXP_cast = (fun (typ,id) -> (LEXP_cast (typ,id), LEXP_cast (typ,id))) + ; lEXP_tup = (fun tups -> let (tups,tups') = List.split tups in (LEXP_tup tups, LEXP_tup tups')) + ; lEXP_vector = (fun ((lexp,lexp'),(e2,e2')) -> (LEXP_vector (lexp,e2), LEXP_vector (lexp',e2'))) + ; lEXP_vector_range = (fun ((lexp,lexp'),(e2,e2'),(e3,e3')) -> (LEXP_vector_range (lexp,e2,e3), LEXP_vector_range (lexp',e2',e3'))) + ; lEXP_field = (fun ((lexp,lexp'),id) -> (LEXP_field (lexp,id), LEXP_field (lexp',id))) + ; lEXP_aux = (fun ((lexp,lexp'),annot) -> (LEXP_aux (lexp,annot), LEXP_aux (lexp',annot))) + ; fE_Fexp = (fun (id,(e,e')) -> (FE_Fexp (id,e), FE_Fexp (id,e'))) + ; fE_aux = (fun ((fexp,fexp'),annot) -> (FE_aux (fexp,annot), FE_aux (fexp',annot))) + ; fES_Fexps = (fun (fexps,b) -> let (fexps, fexps') = List.split fexps in (FES_Fexps (fexps,b), FES_Fexps (fexps',b))) + ; fES_aux = (fun ((fexp,fexp'),annot) -> (FES_aux (fexp,annot), FES_aux (fexp',annot))) + ; def_val_empty = (Def_val_empty, Def_val_empty) + ; def_val_dec = (fun (e,e') -> (Def_val_dec e, Def_val_dec e')) + ; def_val_aux = (fun ((defval,defval'),aux) -> (Def_val_aux (defval,aux), Def_val_aux (defval',aux))) + ; pat_exp = (fun (pat,(e,e')) -> (Pat_exp (pat,e), Pat_exp (pat,e'))) + ; pat_when = (fun (pat,(e1,e1'),(e2,e2')) -> (Pat_when (pat,e1,e2), Pat_when (pat,e1',e2'))) + ; pat_aux = (fun ((pexp,pexp'),a) -> (Pat_aux (pexp,a), Pat_aux (pexp',a))) + ; lB_val_explicit = (fun (typ,pat,(e,e')) -> (LB_val_explicit (typ,pat,e), LB_val_explicit (typ,pat,e'))) + ; lB_val_implicit = (fun (pat,(e,e')) -> (LB_val_implicit (pat,e), LB_val_implicit (pat,e'))) + ; lB_aux = (fun ((lb,lb'),annot) -> (LB_aux (lb,annot), LB_aux (lb',annot))) + ; pat_alg = id_pat_alg + } in let rewrite_sizeof_fun params_map (FD_aux (FD_function (rec_opt,tannot,eff,funcls),((l,_) as annot))) = @@ -1086,7 +1160,7 @@ let rewrite_sizeof (Defs defs) = let body_typ = typ_of exp in let nmap = nexps_from_params pat in (* first rewrite calls to other functions... *) - let exp' = fold_exp { id_exp_alg with e_aux = e_app_aux params_map } exp in + let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in (* ... then rewrite sizeof expressions in current function body *) let exp'' = fold_exp { id_exp_alg with e_sizeof = e_sizeof nmap } exp' in (FCL_aux (FCL_Funcl (id,pat,exp''), annot) :: funcls, @@ -1133,9 +1207,10 @@ let rewrite_sizeof (Defs defs) = let rewrite_sizeof_fundef (params_map, defs) = function | DEF_fundef fd -> let (nvars, fd') = rewrite_sizeof_fun params_map fd in + let id = id_of_fundef fd in let params_map' = if KidSet.is_empty nvars then params_map - else Bindings.add (id_of_fundef fd) nvars params_map in + else Bindings.add id nvars params_map in (params_map', defs @ [DEF_fundef fd']) | def -> (params_map, defs @ [def]) in @@ -1947,7 +2022,7 @@ let rewrite_defs_remove_bitvector_pats (Defs defs) = let defvals = List.map (fun lb -> DEF_val lb) letbinds in [DEF_val (LB_aux (LB_val_implicit (pat',exp),a))] @ defvals | d -> [d] in - Defs (List.flatten (List.map rewrite_def defs)) + fst (check initial_env (Defs (List.flatten (List.map rewrite_def defs)))) (* Remove pattern guards by rewriting them to if-expressions within the @@ -2399,7 +2474,7 @@ let rewrite_defs_letbind_effects = | E_case (exp1,pexps) -> let newreturn = List.fold_left - (fun b (Pat_aux (_,(_,annot))) -> b || effectful_effs (effect_of_annot annot)) + (fun b pexp -> b || effectful_effs (effect_of_pexp pexp)) false pexps in n_exp_name exp1 (fun exp1 -> n_pexpL newreturn pexps (fun pexps -> @@ -2969,6 +3044,7 @@ let rewrite_defs_remove_e_assign = ; rewrite_defs = rewrite_defs_base } +let recheck_defs defs = fst (check initial_env defs) let rewrite_defs_lem =[ top_sort_defs; @@ -2976,6 +3052,7 @@ let rewrite_defs_lem =[ rewrite_defs_remove_vector_concat; rewrite_defs_remove_bitvector_pats; rewrite_defs_guarded_pats; + (* recheck_defs; *) rewrite_defs_exp_lift_assign; rewrite_defs_remove_blocks; rewrite_defs_letbind_effects; diff --git a/src/type_check.ml b/src/type_check.ml index e61d1425..5e9ff5f1 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -386,6 +386,7 @@ module Env : sig val add_union_id : id -> typquant * typ -> t -> t val add_flow : id -> (typ -> typ) -> t -> t val get_flow : id -> t -> typ -> typ + val is_register : id -> t -> bool val get_register : id -> t -> typ val add_register : id -> typ -> t -> t val add_regtyp : id -> int -> int -> (index_range * id) list -> t -> t @@ -403,6 +404,9 @@ module Env : sig val get_typ_synonym : id -> t -> typ_arg list -> typ val add_overloads : id -> id list -> t -> t val get_overloads : id -> t -> id list + val is_extern : id -> t -> bool + val add_extern : id -> string -> t -> t + val get_extern : id -> t -> string val get_default_order : t -> order val set_default_order_inc : t -> t val set_default_order_dec : t -> t @@ -433,6 +437,7 @@ end = struct enums : IdSet.t Bindings.t; records : (typquant * (typ * id) list) Bindings.t; accessors : (typquant * typ) Bindings.t; + externs : string Bindings.t; casts : id list; allow_casts : bool; constraints : n_constraint list; @@ -454,6 +459,7 @@ end = struct enums = Bindings.empty; records = Bindings.empty; accessors = Bindings.empty; + externs = Bindings.empty; casts = []; allow_casts = true; constraints = []; @@ -670,6 +676,9 @@ end = struct { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow } end + let is_register id env = + Bindings.mem id env.registers + let get_register id env = try Bindings.find id env.registers with | Not_found -> typ_error (id_loc id) ("No register binding found for " ^ string_of_id id) @@ -682,6 +691,16 @@ end = struct typ_print ("Adding overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]"); { env with overloads = Bindings.add id ids env.overloads } + let is_extern id env = + Bindings.mem id env.externs + + let add_extern id ext env = + { env with externs = Bindings.add id ext env.externs } + + let get_extern id env = + try Bindings.find id env.externs with + | Not_found -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id) + let get_casts env = env.casts let check_index_range cmp f t (BF_aux (ir, l)) = @@ -839,6 +858,19 @@ end = struct | Typ_arg_typ typ -> Typ_arg_aux (Typ_arg_typ (expand_synonyms env typ), l) | arg -> Typ_arg_aux (arg, l) + let get_default_order env = + match env.default_order with + | None -> typ_error Parse_ast.Unknown ("No default order has been set") + | Some ord -> ord + + let set_default_order o env = + match env.default_order with + | None -> { env with default_order = Some (Ord_aux (o, Parse_ast.Unknown)) } + | Some _ -> typ_error Parse_ast.Unknown ("Cannot change default order once already set") + + let set_default_order_inc = set_default_order Ord_inc + let set_default_order_dec = set_default_order Ord_dec + let base_typ_of env typ = let rec aux (Typ_aux (t,a)) = let rewrap t = Typ_aux (t,a) in @@ -852,6 +884,11 @@ end = struct aux rtyp | Typ_app (id, targs) -> rewrap (Typ_app (id, List.map aux_arg targs)) + | Typ_id id when is_regtyp id env -> + let base, top, ranges = get_regtyp id env in + let len = abs(top - base) + 1 in + vector_typ (nconstant base) (nconstant len) (get_default_order env) bit_typ + (* TODO registers with non-default order? non-bitvector registers? *) | t -> rewrap t and aux_arg (Typ_arg_aux (targ,a)) = let rewrap targ = Typ_arg_aux (targ,a) in @@ -860,19 +897,6 @@ end = struct | targ -> rewrap targ in aux (expand_synonyms env typ) - let get_default_order env = - match env.default_order with - | None -> typ_error Parse_ast.Unknown ("No default order has been set") - | Some ord -> ord - - let set_default_order o env = - match env.default_order with - | None -> { env with default_order = Some (Ord_aux (o, Parse_ast.Unknown)) } - | Some _ -> typ_error Parse_ast.Unknown ("Cannot change default order once already set") - - let set_default_order_inc = set_default_order Ord_inc - let set_default_order_dec = set_default_order Ord_dec - end @@ -1767,7 +1791,8 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ | E_lit (L_aux (L_undef, _) as lit), _ -> annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef]) (* This rule allows registers of type t to be passed by name with type register<t>*) - | E_id reg, Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) when string_of_id id = "register" -> + | E_id reg, Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) + when string_of_id id = "register" && Env.is_register reg env -> let rtyp = Env.get_register reg env in subtyp l env rtyp typ; annot_exp (E_id reg) typ (* CHECK: is this subtyp the correct way around? *) | E_id id, _ when is_union_id id env -> @@ -2154,11 +2179,12 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = (* Not sure about this case... can the left lexp be anything other than an identifier? *) | LEXP_vector (LEXP_aux (LEXP_id v, _), exp) -> begin - let is_immutable, vtyp = match Env.lookup_id v env with + let is_immutable, is_register, vtyp = match Env.lookup_id v env with | Unbound -> typ_error l "Cannot assign to element of unbound vector" | Enum _ -> typ_error l "Cannot vector assign to enumeration element" - | Local (Immutable, vtyp) -> true, vtyp - | Local (Mutable, vtyp) | Register vtyp -> false, vtyp + | Local (Immutable, vtyp) -> true, false, vtyp + | Local (Mutable, vtyp) -> false, false, vtyp + | Register vtyp -> false, true, vtyp 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 E_aux (E_app (_, [_; inferred_exp]), _) = access in @@ -2166,6 +2192,9 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" -> subtyp l env typ deref_typ; annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env + | _ when not is_immutable && is_register -> + subtyp l env typ (typ_of access); + annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env | _ when not is_immutable -> subtyp l env typ (typ_of access); annot_lexp (LEXP_vector (annot_lexp (LEXP_id v) vtyp, inferred_exp)) typ, env @@ -2205,27 +2234,28 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let inferred_exp = irule infer_exp env exp in match Env.expand_synonyms env (typ_of inferred_exp) with (* Accessing a (bit) field of a register *) - | Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id regtyp, _)), _)]), _) - | Typ_aux (Typ_id regtyp, _) when Env.is_regtyp regtyp env -> + | Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ ((Typ_aux (Typ_id regtyp, _) as regtyp_aux)), _)]), _) + | (Typ_aux (Typ_id regtyp, _) as regtyp_aux) when Env.is_regtyp regtyp env -> let base, top, ranges = Env.get_regtyp regtyp env in let range, _ = try List.find (fun (_, id) -> Id.compare id field = 0) ranges with | Not_found -> typ_error l ("Field " ^ string_of_id field ^ " doesn't exist for register type " ^ string_of_id regtyp) in + let checked_exp = crule check_exp env (strip_exp inferred_exp) regtyp_aux in begin match range, Env.get_default_order env with | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) -> let vec_typ = dvector_typ env (nconstant n) (nconstant 1) bit_typ in - annot_exp (E_field (inferred_exp, field)) vec_typ + annot_exp (E_field (checked_exp, field)) vec_typ | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) -> let vec_typ = dvector_typ env (nconstant n) (nconstant (n - m + 1)) bit_typ in - annot_exp (E_field (inferred_exp, field)) vec_typ + annot_exp (E_field (checked_exp, field)) vec_typ | BF_aux (BF_single n, _), Ord_aux (Ord_inc, _) -> let vec_typ = dvector_typ env (nconstant n) (nconstant 1) bit_typ in - annot_exp (E_field (inferred_exp, field)) vec_typ + annot_exp (E_field (checked_exp, field)) vec_typ | BF_aux (BF_range (n, m), _), Ord_aux (Ord_inc, _) -> let vec_typ = dvector_typ env (nconstant n) (nconstant (m - n + 1)) bit_typ in - annot_exp (E_field (inferred_exp, field)) vec_typ + annot_exp (E_field (checked_exp, field)) vec_typ | _, _ -> typ_error l "Invalid register field type" end (* Accessing a field of a record *) @@ -2719,8 +2749,12 @@ let check_val_spec env (VS_aux (vs, (l, _))) = let (id, quants, typ, env) = match vs with | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ, env) | VS_cast_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ, Env.add_cast id env) - | VS_extern_no_rename (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ, env) - | VS_extern_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, _) -> (id, quants, typ, env) in + | VS_extern_no_rename (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> + let env = Env.add_extern id (string_of_id id) env in + (id, quants, typ, env) + | VS_extern_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, ext) -> + let env = Env.add_extern id ext env in + (id, quants, typ, env) in [DEF_spec (VS_aux (vs, (l, None)))], Env.add_val_spec id (quants, typ) env let check_default env (DT_aux (ds, l)) = @@ -2768,7 +2802,11 @@ let check_type_union env variant typq (Tu_aux (tu, l)) = let ret_typ = app_typ variant (List.fold_left fold_union_quant [] (quant_items typq)) in match tu with | Tu_id v -> Env.add_union_id v (typq, ret_typ) env - | Tu_ty_id (typ, v) -> Env.add_val_spec v (typq, mk_typ (Typ_fn (typ, ret_typ, no_effect))) env + | Tu_ty_id (typ, v) -> + let typ' = mk_typ (Typ_fn (typ, ret_typ, no_effect)) in + env + |> Env.add_union_id v (typq, typ') + |> Env.add_val_spec v (typq, typ') let check_typedef env (TD_aux (tdef, (l, _))) = let td_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented Typedef") in @@ -2799,7 +2837,8 @@ let rec check_def env def = | 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, _))) -> - [DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, None)))], Env.add_register id typ env + let env = Env.add_register id 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_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 88d4ecae..fe582568 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -101,6 +101,10 @@ module Env : sig val get_overloads : id -> t -> id list + val is_extern : id -> t -> bool + + val get_extern : id -> t -> string + (* Lookup id searchs for a specified id in the environment, and returns it's type and what kind of identifier it is, using the lvar type. Returns Unbound if the identifier is unbound, and |