diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 6 | ||||
| -rw-r--r-- | src/state.ml | 8 |
2 files changed, 8 insertions, 6 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 38395b07..e68a6dd9 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -382,7 +382,7 @@ let doc_typ, doc_atomic_typ = let tpp = match elem_typ with | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> string "mword " ^^ doc_nexp ctx (nexp_simp m) - | _ -> string "list" ^^ space ^^ typ elem_typ in + | _ -> string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ doc_nexp ctx (nexp_simp m) in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> let tpp = string "register_ref regstate register_value " ^^ typ etyp in @@ -1122,7 +1122,9 @@ let doc_exp_lem, doc_let_lem = if is_bit_typ etyp then let bepp = string "vec_of_bits" ^^ space ^^ align epp in (align (group (prefix 0 1 bepp (doc_tannot_lem ctxt (env_of full_exp) false t))), true) - else (epp,aexp_needed) in + else + let vepp = string "vec_of_list_len" ^^ space ^^ align epp in + (vepp,aexp_needed) in if aexp_needed then parens (align epp) else epp | E_vector_update(v,e1,e2) -> raise (Reporting_basic.err_unreachable l diff --git a/src/state.ml b/src/state.ml index c591f753..e788ab6a 100644 --- a/src/state.ml +++ b/src/state.ml @@ -411,7 +411,7 @@ let rec regval_convs_coq (Typ_aux (t, _) as typ) = match t with let size = string_of_nexp (nexp_simp size) in let is_inc = if is_order_inc ord then "true" else "false" in let etyp_of, of_etyp = regval_convs_coq etyp in - "(fun v => vector_of_regval " ^ etyp_of ^ " v)", + "(fun v => vector_of_regval " ^ size ^ " " ^ etyp_of ^ " v)", "(fun v => regval_of_vector " ^ of_etyp ^ " " ^ size ^ " " ^ is_inc ^ " v)" | Typ_app (id, [Typ_arg_aux (Typ_arg_typ etyp, _)]) when string_of_id id = "list" -> @@ -430,12 +430,12 @@ let rec regval_convs_coq (Typ_aux (t, _) as typ) = match t with let register_refs_coq registers = let generic_convs = separate_map hardline string [ - "Definition vector_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (list a) := match rv with"; - " | Regval_vector (_, _, v) => just_list (List.map of_regval v)"; + "Definition vector_of_regval {a} n (of_regval : register_value -> option a) (rv : register_value) : option (vec a n) := match rv with"; + " | Regval_vector (n', _, v) => if n =? n' then map_bind (vec_of_list n) (just_list (List.map of_regval v)) else None"; " | _ => None"; "end."; ""; - "Definition regval_of_vector {a} (regval_of : a -> register_value) (size : Z) (is_inc : bool) (xs : list a) : register_value := Regval_vector (size, is_inc, List.map regval_of xs)."; + "Definition regval_of_vector {a} (regval_of : a -> register_value) (size : Z) (is_inc : bool) (xs : vec a size) : register_value := Regval_vector (size, is_inc, List.map regval_of (list_of_vec xs))."; ""; "Definition list_of_regval {a} (of_regval : register_value -> option a) (rv : register_value) : option (list a) := match rv with"; " | Regval_list v => just_list (List.map of_regval v)"; |