diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 14 | ||||
| -rw-r--r-- | src/ast_util.mli | 2 | ||||
| -rw-r--r-- | src/initial_check.ml | 6 | ||||
| -rw-r--r-- | src/isail.ml | 20 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 8 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 4 | ||||
| -rw-r--r-- | src/rewrites.ml | 6 | ||||
| -rw-r--r-- | src/type_check.ml | 92 | ||||
| -rw-r--r-- | src/type_check.mli | 7 |
9 files changed, 61 insertions, 98 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index ec572bd4..20697005 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -249,10 +249,9 @@ let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)] let tuple_typ typs = mk_typ (Typ_tup typs) let function_typ typ1 typ2 eff = mk_typ (Typ_fn (typ1, typ2, eff)) -let vector_typ n m ord typ = +let vector_typ n ord typ = mk_typ (Typ_app (mk_id "vector", [mk_typ_arg (Typ_arg_nexp (nexp_simp n)); - mk_typ_arg (Typ_arg_nexp (nexp_simp m)); mk_typ_arg (Typ_arg_order ord); mk_typ_arg (Typ_arg_typ typ)])) @@ -744,7 +743,7 @@ let is_reftyp (Typ_aux (typ_aux, _)) = match typ_aux with | _ -> false let rec is_vector_typ = function - | Typ_aux (Typ_app (Id_aux (Id "vector",_), [_;_;_;_]), _) -> true + | Typ_aux (Typ_app (Id_aux (Id "vector",_), [_;_;_]), _) -> true | Typ_aux (Typ_app (Id_aux (Id "register",_), [Typ_arg_aux (Typ_arg_typ rtyp,_)]), _) -> is_vector_typ rtyp | _ -> false @@ -757,8 +756,13 @@ let typ_app_args_of = function ("typ_app_args_of called on non-app type " ^ string_of_typ typ)) let rec vector_typ_args_of typ = match typ_app_args_of typ with - | ("vector", [Typ_arg_nexp start; Typ_arg_nexp len; Typ_arg_order ord; Typ_arg_typ etyp], _) -> - (nexp_simp start, nexp_simp len, ord, etyp) + | ("vector", [Typ_arg_nexp len; Typ_arg_order ord; Typ_arg_typ etyp], l) -> + begin + match ord with + | Ord_aux (Ord_inc, _) -> (nint 0, nexp_simp len, ord, etyp) + | Ord_aux (Ord_dec, _) -> (nexp_simp (nminus len (nint 1)), nexp_simp len, ord, etyp) (* FIXME to return 3 arguments *) + | _ -> raise (Reporting_basic.err_typ l "Can't calculate start index without order") + end | ("register", [Typ_arg_typ rtyp], _) -> vector_typ_args_of rtyp | (_, _, l) -> raise (Reporting_basic.err_typ l diff --git a/src/ast_util.mli b/src/ast_util.mli index a3ccc00c..7ff46b02 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -106,7 +106,7 @@ val app_typ : id -> typ_arg list -> typ val unit_typ : typ val string_typ : typ val real_typ : typ -val vector_typ : nexp -> nexp -> order -> typ -> typ +val vector_typ : nexp -> order -> typ -> typ val list_typ : typ -> typ val exc_typ : typ val tuple_typ : typ list -> typ diff --git a/src/initial_check.ml b/src/initial_check.ml index 7ec0154e..c44a3b42 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -945,7 +945,7 @@ let initial_kind_env = ("reg", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); ("register", {k = K_Lam( [{k = K_Typ}], {k= K_Typ})}); ("range", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}], {k = K_Typ}) }); - ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ); + ("vector", {k = K_Lam( [{k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ); ("atom", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); ("option", { k = K_Lam( [{k=K_Typ}], {k=K_Typ}) }); ("implicit", {k = K_Lam( [{k = K_Nat}], {k=K_Typ})} ); @@ -1011,9 +1011,9 @@ let generate_undefineds vs_ids (Defs defs) = gen_vs (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}"; gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; (* FIXME: How to handle inc/dec order correctly? *) - gen_vs (mk_id "undefined_vector") "forall 'n 'm ('a:Type). (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}"; + gen_vs (mk_id "undefined_vector") "forall 'n ('a:Type). (atom('n), 'a) -> vector('n, dec,'a) effect {undef}"; (* Only used with lem_mwords *) - gen_vs (mk_id "undefined_bitvector") "forall 'n 'm. (atom('n), atom('m)) -> vector('n, 'm, dec,bit) effect {undef}"; + gen_vs (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}"; gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"] in let undefined_tu = function diff --git a/src/isail.ml b/src/isail.ml index e1860451..97b92809 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -86,14 +86,14 @@ let clear str = str ^ termcode 0 let sail_logo = let banner str = str |> bold |> red |> clear in - [ " ___ ___ ___ ___ "; - " /\\ \\ /\\ \\ /\\ \\ /\\__\\"; - " /::\\ \\ /::\\ \\ _\\:\\ \\ /:/ /"; - " /\\:\\:\\__\\ /::\\:\\__\\ /\\/::\\__\\ /:/__/ "; - " \\:\\:\\/__/ \\/\\::/ / \\::/\\/__/ \\:\\ \\ "; - " \\::/ / /:/ / \\:\\__\\ \\:\\__\\"; - " \\/__/ \\/__/ \\/__/ \\/__/"; - "" + [ {| ___ ___ ___ ___ |}; + {| /\ \ /\ \ /\ \ /\__\ |}; + {| /::\ \ /::\ \ _\:\ \ /:/ / |}; + {| /\:\:\__\ /::\:\__\ /\/::\__\ /:/__/ |}; + {| \:\:\/__/ \/\::/ / \::/\/__/ \:\ \ |}; + {| \::/ / /:/ / \:\__\ \:\__\ |}; + {| \/__/ \/__/ \/__/ \/__/ |}; + {| |} ] |> List.map banner @@ -152,8 +152,6 @@ let handle_input input = let () = - List.iter print_endline sail_logo; - (* Auto complete function names based on val specs *) LNoise.set_completion_callback begin @@ -179,5 +177,5 @@ let () = LNoise.history_set ~max_length:100 |> ignore; if !opt_interactive then - user_input handle_input + (List.iter print_endline sail_logo; user_input handle_input) else () diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index b1a19482..273ca829 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -283,14 +283,14 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = let loop_var = separate space [string "let"; zencode ctx id; equals; string "ref"; ocaml_atomic_exp ctx exp_from; string "in"] in let loop_mod = match ord with - | Ord_aux (Ord_inc, _) -> string "Big_int.add" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step - | Ord_aux (Ord_dec, _) -> string "Big_int.sub" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step + | Ord_aux (Ord_inc, _) -> string "add_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step + | Ord_aux (Ord_dec, _) -> string "sub_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step | Ord_aux (Ord_var _, _) -> failwith "Cannot have variable loop order!" in let loop_compare = match ord with - | Ord_aux (Ord_inc, _) -> string "Big_int.less_equal" - | Ord_aux (Ord_dec, _) -> string "Big_int.greater" + | Ord_aux (Ord_inc, _) -> string "le_big_int" + | Ord_aux (Ord_dec, _) -> string "gt_big_int" | Ord_aux (Ord_var _, _) -> failwith "Cannot have variable loop order!" in let loop_body = diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 11b34a3d..ae332b39 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1171,7 +1171,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with 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 Big_int.add (Big_int.sub i2 i1) (Big_int.of_int 1) else Big_int.add (Big_int.sub i1 i2) (Big_int.of_int 1) in - let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in + let vtyp = vector_typ (nconstant size) ord bit_typ in let tannot = doc_tannot_lem sequential mwords false vtyp in let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id); doc_range_lem r;]) in @@ -1405,7 +1405,7 @@ let doc_regtype_fields sequential mwords (tname, (n1, n2, fields)) = (* TODO Assumes normalised, decreasing bitvector slices; however, since start indices or indexing order do not appear in Lem type annotations, this does not matter. *) - let ftyp = vector_typ (nconstant (Big_int.pred fsize)) (nconstant fsize) dec_ord bit_typ in + let ftyp = vector_typ (nconstant fsize) dec_ord bit_typ in let reftyp = mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), [mk_typ_arg (Typ_arg_typ (mk_id_typ (mk_id tname))); diff --git a/src/rewrites.ml b/src/rewrites.ml index 8c0526fe..e96dd17f 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -173,7 +173,7 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp = | _ -> begin match destruct_vector env typ with - | Some (_, len, _, _) when prove env (nc_eq len nexp) -> + | Some (len, _, _) when prove env (nc_eq len nexp) -> Some (E_aux (E_app (mk_id "length", [var]), (l, Some (env, atom_typ len, no_effect)))) | _ -> None end @@ -1550,7 +1550,7 @@ let rewrite_register_ref_writes (Defs defs) = let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in let size = if dir_b then Big_int.succ (Big_int.sub i2 i1) else Big_int.succ (Big_int.sub i1 i2) in let rtyp = mk_id_typ id in - let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in + let vtyp = vector_typ (nconstant size) ord bit_typ in let accessors (fr, fid) = let i, j = match fr with | BF_aux (BF_single i, _) -> (i, i) @@ -1936,7 +1936,7 @@ let rewrite_undefined mwords = let rec simple_typ (Typ_aux (typ_aux, l) as typ) = Typ_aux (simple_typ_aux typ_aux, l) and simple_typ_aux = function | Typ_id id -> Typ_id id - | Typ_app (id, [_; _; _; Typ_arg_aux (Typ_arg_typ typ, l)]) when Id.compare id (mk_id "vector") = 0 -> + | Typ_app (id, [_; _; Typ_arg_aux (Typ_arg_typ typ, l)]) when Id.compare id (mk_id "vector") = 0 -> Typ_app (mk_id "list", [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)]) | Typ_app (id, [_]) when Id.compare id (mk_id "atom") = 0 -> Typ_id (mk_id "int") diff --git a/src/type_check.ml b/src/type_check.ml index c1390e84..756efbfd 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -428,7 +428,7 @@ end = struct List.fold_left (fun m (name, kinds) -> Bindings.add (mk_id name) (kinds_typq kinds) m) Bindings.empty [ ("range", [BK_nat; BK_nat]); ("atom", [BK_nat]); - ("vector", [BK_nat; BK_nat; BK_order; BK_type]); + ("vector", [BK_nat; BK_order; BK_type]); ("register", [BK_type]); ("bit", []); ("unit", []); @@ -494,8 +494,8 @@ end = struct | kopt :: kopts, Typ_arg_aux (Typ_arg_order arg, _) :: args when is_order_kopt kopt -> subst_args kopts args | [], [] -> ncs - | _, Typ_arg_aux (_, l) :: _ -> typ_error l "ERROR 1" - | _, _ -> typ_error Parse_ast.Unknown "ERROR 2" + | _, Typ_arg_aux (_, l) :: _ -> typ_error l ("Error when processing type quantifer arguments " ^ string_of_typquant typq) + | _, _ -> typ_error Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq) in let ncs = subst_args kopts args in if List.for_all (env.prove env) ncs @@ -931,7 +931,7 @@ end = struct | Typ_id id when is_regtyp id env -> let base, top, ranges = get_regtyp id env in let len = Big_int.succ (Big_int.abs (Big_int.sub top base)) in - vector_typ (nconstant base) (nconstant len) (get_default_order env) bit_typ + vector_typ (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)) = @@ -966,16 +966,7 @@ let add_typquant (quant : typquant) (env : Env.t) : Env.t = let default_order_error_string = "No default Order (if you have set a default Order, move it earlier in the specification)" -let dvector_typ env n m typ = vector_typ n m (Env.get_default_order env) typ - -let lvector_typ env l typ = - match Env.get_default_order env with - | Ord_aux (Ord_inc, _) as ord -> - vector_typ (nint 0) l ord typ - | Ord_aux (Ord_dec, _) as ord -> - vector_typ (nminus l (nint 1)) l ord typ - | Ord_aux (Ord_var _, _) as ord -> - typ_error Parse_ast.Unknown default_order_error_string +let dvector_typ env n typ = vector_typ n (Env.get_default_order env) typ let ex_counter = ref 0 @@ -1003,10 +994,9 @@ let exist_typ constr typ = let destruct_vector env typ = let destruct_vector' = function | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _); - Typ_arg_aux (Typ_arg_nexp n2, _); Typ_arg_aux (Typ_arg_order o, _); Typ_arg_aux (Typ_arg_typ vtyp, _)] - ), _) when string_of_id id = "vector" -> Some (n1, n2, o, vtyp) + ), _) when string_of_id id = "vector" -> Some (n1, o, vtyp) | typ -> None in destruct_vector' (Env.expand_synonyms env typ) @@ -1698,27 +1688,15 @@ let infer_lit env (L_aux (lit_aux, l) as lit) = | L_bin str -> begin match Env.get_default_order env with - | Ord_aux (Ord_inc, _) -> - dvector_typ env (nint 0) (nint (String.length str)) (mk_typ (Typ_id (mk_id "bit"))) - | Ord_aux (Ord_dec, _) -> - dvector_typ env - (nint (String.length str - 1)) - (nint (String.length str)) - (mk_typ (Typ_id (mk_id "bit"))) + | Ord_aux (Ord_inc, _) | Ord_aux (Ord_dec, _) -> + dvector_typ env (nint (String.length str)) (mk_typ (Typ_id (mk_id "bit"))) | Ord_aux (Ord_var _, _) -> typ_error l default_order_error_string - end | L_hex str -> begin match Env.get_default_order env with - | Ord_aux (Ord_inc, _) -> - dvector_typ env (nint 0) (nint (String.length str * 4)) (mk_typ (Typ_id (mk_id "bit"))) - | Ord_aux (Ord_dec, _) -> - dvector_typ env - (nint (String.length str * 4 - 1)) - (nint (String.length str * 4)) - (mk_typ (Typ_id (mk_id "bit"))) - + | Ord_aux (Ord_inc, _) | Ord_aux (Ord_dec, _) -> + dvector_typ env (nint (String.length str * 4)) (mk_typ (Typ_id (mk_id "bit"))) | Ord_aux (Ord_var _, _) -> typ_error l default_order_error_string end | L_undef -> typ_error l "Cannot infer the type of undefined" @@ -1767,10 +1745,9 @@ let rec instantiate_quants quants kid uvar = match quants with let destruct_vec_typ l env typ = let destruct_vec_typ' l = function | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _); - Typ_arg_aux (Typ_arg_nexp n2, _); Typ_arg_aux (Typ_arg_order o, _); Typ_arg_aux (Typ_arg_typ vtyp, _)] - ), _) when string_of_id id = "vector" -> (n1, n2, o, vtyp) + ), _) when string_of_id id = "vector" -> (n1, o, vtyp) | typ -> typ_error l ("Expected vector type, got " ^ string_of_typ typ) in destruct_vec_typ' l (Env.expand_synonyms env typ) @@ -2188,7 +2165,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ let checked_body = crule check_exp env body typ in annot_exp (E_internal_plet (tpat, bind_exp, checked_body)) typ | E_vector vec, _ -> - let (start, len, ord, vtyp) = destruct_vec_typ l env typ in + let (len, ord, vtyp) = destruct_vec_typ l env typ in let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in if prove env (nc_eq (nint (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ else typ_error l "List length didn't match" (* FIXME: improve error message *) @@ -2474,21 +2451,21 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = let len = nexp_simp (nint (List.length pats)) in let etyp = pat_typ_of (List.hd pats) in List.iter (fun pat -> typ_equality l env etyp (pat_typ_of pat)) pats; - annot_pat (P_vector pats) (lvector_typ env len etyp), env + annot_pat (P_vector pats) (dvector_typ env len etyp), env | P_vector_concat (pat :: pats) -> let fold_pats (pats, env) pat = let inferred_pat, env = infer_pat env pat in pats @ [inferred_pat], env in let inferred_pats, env = List.fold_left fold_pats ([], env) (pat :: pats) in - let (_, len, _, vtyp) = destruct_vec_typ l env (pat_typ_of (List.hd inferred_pats)) in + let (len, _, vtyp) = destruct_vec_typ l env (pat_typ_of (List.hd inferred_pats)) in let fold_len len pat = - let (_, len', _, vtyp') = destruct_vec_typ l env (pat_typ_of pat) in + let (len', _, vtyp') = destruct_vec_typ l env (pat_typ_of pat) in typ_equality l env vtyp vtyp'; nsum len len' in let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_pats)) in - annot_pat (P_vector_concat inferred_pats) (lvector_typ env len vtyp), env + annot_pat (P_vector_concat inferred_pats) (dvector_typ env len vtyp), env | P_as (pat, id) -> let (typed_pat, env) = infer_pat env pat in annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), Env.add_local id (Immutable, pat_typ_of typed_pat) env @@ -2537,6 +2514,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as typ_debug ("REGTYP: " ^ string_of_typ regtyp ^ " / " ^ string_of_typ (Env.expand_synonyms env regtyp)); match Env.expand_synonyms env regtyp with | Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id regtyp_id, _)), _)]), _) + (* FIXME: Almost certainly broken *) | Typ_aux (Typ_id regtyp_id, _) when Env.is_regtyp regtyp_id env -> let eff = mk_effect [BE_wreg] in let base, top, ranges = Env.get_regtyp regtyp_id env in @@ -2546,9 +2524,9 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as in let vec_typ = match range, Env.get_default_order env with | BF_aux (BF_single n, _), Ord_aux (Ord_dec, _) -> - dvector_typ env (nconstant n) (nint 1) (mk_typ (Typ_id (mk_id "bit"))) + dvector_typ env (nint 1) (mk_typ (Typ_id (mk_id "bit"))) | BF_aux (BF_range (n, m), _), Ord_aux (Ord_dec, _) -> - dvector_typ env (nconstant n) (nconstant (Big_int.add (Big_int.sub n m) (Big_int.of_int 1))) (mk_typ (Typ_id (mk_id "bit"))) + dvector_typ env (nconstant (Big_int.add (Big_int.sub n m) (Big_int.of_int 1))) (mk_typ (Typ_id (mk_id "bit"))) | _, _ -> typ_error l "Not implemented this register field type yet..." in let checked_exp = crule check_exp env exp vec_typ in @@ -2635,7 +2613,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = | Typ_app (id, _) when Id.compare id (mk_id "vector") == 0 -> begin match destruct_vector env typ with - | Some (_, vec_len, _, _) -> + | Some (vec_len, _, _) -> let bind_bits_tuple lexp (tlexps, env, llen) = match lexp with | LEXP_aux (LEXP_id v, _) -> @@ -2647,7 +2625,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = typ_error l "Unbound variable in vector tuple assignment" | Local (Mutable, vtyp) | Register vtyp -> let llen' = match destruct_vector env vtyp with - | Some (_, llen', _, _) -> llen' + | Some (llen', _, _) -> llen' | None -> typ_error l "Variables in vector tuple assignment must be vectors" in let tlexp, env = bind_lexp env lexp vtyp in @@ -2662,7 +2640,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ = in let typq, _, vtyp, _ = Env.get_accessor rec_id fid env in let llen' = match destruct_vector env vtyp with - | Some (_, llen', _, _) -> llen' + | Some (llen', _, _) -> llen' | None -> typ_error l "Variables in vector tuple assignment must be vectors" in let tlexp, env = bind_lexp env lexp vtyp in @@ -2781,16 +2759,16 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = 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) (nint 1) bit_typ in + let vec_typ = dvector_typ env (nint 1) bit_typ in 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 (Big_int.add (Big_int.sub n m) (Big_int.of_int 1))) bit_typ in + let vec_typ = dvector_typ env (nconstant (Big_int.add (Big_int.sub n m) (Big_int.of_int 1))) bit_typ in 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) (nint 1) bit_typ in + let vec_typ = dvector_typ env (nint 1) bit_typ in 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 (Big_int.add (Big_int.sub m n) (Big_int.of_int 1))) bit_typ in + let vec_typ = dvector_typ env (nconstant (Big_int.add (Big_int.sub m n) (Big_int.of_int 1))) bit_typ in annot_exp (E_field (checked_exp, field)) vec_typ | _, _ -> typ_error l "Invalid register field type" end @@ -2894,21 +2872,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | E_vector ((item :: items) as vec) -> let inferred_item = irule infer_exp env item in let checked_items = List.map (fun i -> crule check_exp env i (typ_of inferred_item)) items in - let vec_typ = match Env.get_default_order env with - | Ord_aux (Ord_inc, _) -> - mk_typ (Typ_app (mk_id "vector", - [mk_typ_arg (Typ_arg_nexp (nint 0)); - mk_typ_arg (Typ_arg_nexp (nint (List.length vec))); - mk_typ_arg (Typ_arg_order (Env.get_default_order env)); - mk_typ_arg (Typ_arg_typ (typ_of inferred_item))])) - | Ord_aux (Ord_dec, _) -> - mk_typ (Typ_app (mk_id "vector", - [mk_typ_arg (Typ_arg_nexp (nint (List.length vec - 1))); - mk_typ_arg (Typ_arg_nexp (nint (List.length vec))); - mk_typ_arg (Typ_arg_order (Env.get_default_order env)); - mk_typ_arg (Typ_arg_typ (typ_of inferred_item))])) - | Ord_aux (Ord_var _, _) -> typ_error l default_order_error_string - in + let vec_typ = dvector_typ env (nint (List.length vec)) (typ_of inferred_item) in annot_exp (E_vector (inferred_item :: checked_items)) vec_typ | E_assert (test, msg) -> let checked_test = crule check_exp env test bool_typ in @@ -3524,7 +3488,7 @@ let check_register env id base top ranges = | Nexp_aux (Nexp_constant basec, _), Nexp_aux (Nexp_constant topc, _) -> let no_typq = TypQ_aux (TypQ_tq [], Parse_ast.Unknown) (* Maybe could be TypQ_no_forall? *) in (* FIXME: wrong for default Order inc? *) - let vec_typ = dvector_typ env base (nconstant (Big_int.add (Big_int.sub basec topc) (Big_int.of_int 1))) bit_typ in + let vec_typ = dvector_typ env (nconstant (Big_int.add (Big_int.sub basec topc) (Big_int.of_int 1))) bit_typ in let cast_typ = mk_typ (Typ_fn (mk_id_typ id, vec_typ, no_effect)) in let cast_to_typ = mk_typ (Typ_fn (vec_typ, mk_id_typ id, no_effect)) in env diff --git a/src/type_check.mli b/src/type_check.mli index 9a61f196..8f0cd98c 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -177,10 +177,7 @@ val add_typquant : typquant -> Env.t -> Env.t val orig_kid : kid -> kid (* Vector with default order. *) -val dvector_typ : Env.t -> nexp -> nexp -> typ -> typ - -(* Vector of specific length with default order, i.e. lvector_typ env n bit_typ = bit[n]. *) -val lvector_typ : Env.t -> nexp -> typ -> typ +val dvector_typ : Env.t -> nexp -> typ -> typ val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ @@ -231,7 +228,7 @@ val destruct_atom_nexp : Env.t -> typ -> nexp option existential to ensure that no name-clashes occur. *) val destruct_exist : Env.t -> typ -> (kid list * n_constraint * typ) option -val destruct_vector : Env.t -> typ -> (nexp * nexp * order * typ) option +val destruct_vector : Env.t -> typ -> (nexp * order * typ) option type uvar = | U_nexp of nexp |