diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/initial_check.ml | 1 | ||||
| -rw-r--r-- | src/interpreter.ml | 19 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 41 | ||||
| -rw-r--r-- | src/rewrites.ml | 2 | ||||
| -rw-r--r-- | src/value.ml | 5 |
5 files changed, 47 insertions, 21 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index f41033ca..ec3e1f24 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -924,7 +924,6 @@ let undefined_builtin_val_specs = extern_of_string (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}"; extern_of_string (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}"; - (* Only used with lem_mwords *) extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> bitvector('n, dec) effect {undef}"; extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"] diff --git a/src/interpreter.ml b/src/interpreter.ml index def0963f..a2cc17bf 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -725,13 +725,20 @@ and pattern_match env (P_aux (p_aux, (l, _)) as pat) value = recursive call that has an empty_tannot we must not use the annotation in the whole vector_concat pattern. *) let open Type_check in + let vector_concat_match n = + let init, rest = Util.take (Big_int.to_int n) (coerce_gv value), Util.drop (Big_int.to_int n) (coerce_gv value) in + let init_match, init_bind = pattern_match env pat (V_vector init) in + let rest_match, rest_bind = pattern_match env (P_aux (P_vector_concat pats, (l, empty_tannot))) (V_vector rest) in + init_match && rest_match, Bindings.merge combine init_bind rest_bind + in begin match destruct_vector (env_of_pat pat) (typ_of_pat pat) with - | Some (Nexp_aux (Nexp_constant n, _), _, _) -> - let init, rest = Util.take (Big_int.to_int n) (coerce_gv value), Util.drop (Big_int.to_int n) (coerce_gv value) in - let init_match, init_bind = pattern_match env pat (V_vector init) in - let rest_match, rest_bind = pattern_match env (P_aux (P_vector_concat pats, (l, empty_tannot))) (V_vector rest) in - init_match && rest_match, Bindings.merge combine init_bind rest_bind - | _ -> failwith ("Bad vector annotation " ^ string_of_typ (Type_check.typ_of_pat pat)) + | Some (Nexp_aux (Nexp_constant n, _), _, _) -> vector_concat_match n + | None -> + begin match destruct_bitvector (env_of_pat pat) (typ_of_pat pat) with + | Some (Nexp_aux (Nexp_constant n, _), _) -> vector_concat_match n + | _ -> failwith ("Bad bitvector annotation for bitvector concatenation pattern " ^ string_of_typ (Type_check.typ_of_pat pat)) + end + | _ -> failwith ("Bad vector annotation for vector concatentation pattern " ^ string_of_typ (Type_check.typ_of_pat pat)) end | P_tup [pat] -> pattern_match env pat value | P_tup pats | P_list pats -> diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 1fea72ea..25abfed8 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -592,15 +592,18 @@ let rec doc_typ_fns ctx env = parens (separate_map (space ^^ star ^^ space) (app_typ false) typs) | _ -> app_typ atyp_needed ty and app_typ atyp_needed ((Typ_aux (t, l)) as ty) = match t with + | Typ_app(Id_aux (Id "bitvector", _), [ + A_aux (A_nexp m, _); + A_aux (A_order ord, _)]) -> + (* TODO: remove duplication with exists, below *) + let tpp = string "mword " ^^ doc_nexp ctx m in + if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "vector", _), [ A_aux (A_nexp m, _); A_aux (A_order ord, _); A_aux (A_typ elem_typ, _)]) -> (* TODO: remove duplication with exists, below *) - let tpp = match elem_typ with - | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> (* TODO: coq-compatible simplification *) - string "mword " ^^ doc_nexp ctx m - | _ -> string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ doc_nexp ctx m in + let tpp = string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ doc_nexp ctx m in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "register", _), [A_aux (A_typ etyp, _)]) -> let tpp = string "register_ref regstate register_value " ^^ typ etyp in @@ -662,6 +665,23 @@ let rec doc_typ_fns ctx env = braces (separate space [doc_var ctx var; colon; string "Z"; ampersand; doc_arithfact ctx env ~exists:(List.map kopt_kid kopts) nc]) end + | Typ_aux (Typ_app (Id_aux (Id "bitvector",_), + [A_aux (A_nexp m, _); + A_aux (A_order ord, _)]), _) -> + (* TODO: proper handling of m, complex elem type, dedup with above *) + let var = mk_kid "_vec" in (* TODO collision avoid *) + let kid_set = KidSet.of_list (List.map kopt_kid kopts) in + let m_pp = doc_nexp ctx ~skip_vars:kid_set m in + let tpp, len_pp = string "mword " ^^ m_pp, string "length_mword" in + let length_constraint_pp = + if KidSet.is_empty (KidSet.inter kid_set (nexp_frees m)) + then None + else Some (separate space [len_pp; doc_var ctx var; equals; doc_nexp ctx m]) + in + braces (separate space + [doc_var ctx var; colon; tpp; + ampersand; + doc_arithfact ctx env ~exists:(List.map kopt_kid kopts) ?extra:length_constraint_pp nc]) | Typ_aux (Typ_app (Id_aux (Id "vector",_), [A_aux (A_nexp m, _); A_aux (A_order ord, _); @@ -670,11 +690,7 @@ let rec doc_typ_fns ctx env = let var = mk_kid "_vec" in (* TODO collision avoid *) let kid_set = KidSet.of_list (List.map kopt_kid kopts) in let m_pp = doc_nexp ctx ~skip_vars:kid_set m in - let tpp, len_pp = match elem_typ with - | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> - string "mword " ^^ m_pp, string "length_mword" - | _ -> string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ m_pp, - string "vec_length" in + let tpp, len_pp = string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ m_pp, string "vec_length" in let length_constraint_pp = if KidSet.is_empty (KidSet.inter kid_set (nexp_frees m)) then None @@ -1020,9 +1036,8 @@ let rec typeclass_nexps (Typ_aux(t,l)) = -> NexpSet.empty | Typ_fn (t1,t2,_) -> List.fold_left NexpSet.union (typeclass_nexps t2) (List.map typeclass_nexps t1) | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts) - | Typ_app (Id_aux (Id "vector",_), - [A_aux (A_nexp size_nexp,_); - _;A_aux (A_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) + | Typ_app (Id_aux (Id "bitvector",_), + [A_aux (A_nexp size_nexp,_); _]) | Typ_app (Id_aux (Id "itself",_), [A_aux (A_nexp size_nexp,_)]) -> let size_nexp = nexp_simp size_nexp in @@ -2020,7 +2035,7 @@ let doc_exp, doc_let = | E_vector exps -> let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let start, (len, order, etyp) = - if is_vector_typ t then vector_start_index t, vector_typ_args_of t + if is_vector_typ t || is_bitvector_typ t then vector_start_index t, vector_typ_args_of t else raise (Reporting.err_unreachable l __POS__ "E_vector of non-vector type") in let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in diff --git a/src/rewrites.ml b/src/rewrites.ml index 0f747f59..3012e49b 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2099,7 +2099,7 @@ let rewrite_vector_concat_assignments env defs = let (_, ord, etyp) = vector_typ_args_of typ in let len (LEXP_aux (le, lannot)) = let ltyp = Env.base_typ_of env (typ_of_annot lannot) in - if is_vector_typ ltyp then + if is_vector_typ ltyp || is_bitvector_typ ltyp then let (len, _, _) = vector_typ_args_of ltyp in match nexp_simp len with | Nexp_aux (Nexp_constant len, _) -> len diff --git a/src/value.ml b/src/value.ml index c509c81f..71d9ffe6 100644 --- a/src/value.ml +++ b/src/value.ml @@ -483,6 +483,10 @@ let value_undefined_vector = function | [v1; v2] -> V_vector (Sail_lib.undefined_vector (coerce_int v1, v2)) | _ -> failwith "value undefined_vector" +let value_undefined_bitvector = function + | [v] -> V_vector (Sail_lib.undefined_vector (coerce_int v, V_bit (Sail_lib.B0))) + | _ -> failwith "value undefined_bitvector" + let value_read_ram = function | [v1; v2; v3; v4] -> mk_vector (Sail_lib.read_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4)) | _ -> failwith "value read_ram" @@ -731,6 +735,7 @@ let primops = ("undefined_int", fun _ -> V_int Big_int.zero); ("undefined_nat", fun _ -> V_int Big_int.zero); ("undefined_bool", fun _ -> V_bool false); + ("undefined_bitvector", value_undefined_bitvector); ("undefined_vector", value_undefined_vector); ("undefined_string", fun _ -> V_string ""); ("internal_pick", value_internal_pick); |