summaryrefslogtreecommitdiff
path: root/src/pretty_print_lem.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/pretty_print_lem.ml')
-rw-r--r--src/pretty_print_lem.ml135
1 files changed, 36 insertions, 99 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 6a3d1293..0002f8cc 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -52,7 +52,6 @@ open Type_check
open Ast
open Ast_util
open Rewriter
-open Big_int
open PPrint
open Pretty_print_common
@@ -152,27 +151,23 @@ let effectful_set =
| BE_escape -> true
| _ -> false)
-let effectful (Effect_aux (eff,_)) =
- match eff with
- | Effect_var _ -> failwith "effectful: Effect_var not supported"
- | Effect_set effs -> effectful_set effs
+let effectful (Effect_aux (Effect_set effs, _)) = effectful_set effs
let is_regtyp (Typ_aux (typ, _)) env = match typ with
| Typ_app(id, _) when string_of_id id = "register" -> true
- | Typ_id(id) when Env.is_regtyp id env -> true
| _ -> false
let doc_nexp_lem nexp =
let (Nexp_aux (nexp, l) as full_nexp) = nexp_simp nexp in
match nexp with
- | Nexp_constant i -> string ("ty" ^ string_of_big_int i)
+ | Nexp_constant i -> string ("ty" ^ Big_int.to_string i)
| Nexp_var v -> string (string_of_kid (orig_kid v))
| _ ->
let rec mangle_nexp (Nexp_aux (nexp, _)) = begin
match nexp with
| Nexp_id id -> string_of_id id
| Nexp_var kid -> string_of_id (id_of_kid (orig_kid kid))
- | Nexp_constant i -> Pretty_print_lem_ast.lemnum string_of_big_int i
+ | Nexp_constant i -> Pretty_print_lem_ast.lemnum Big_int.to_string i
| Nexp_times (n1, n2) -> mangle_nexp n1 ^ "_times_" ^ mangle_nexp n2
| Nexp_sum (n1, n2) -> mangle_nexp n1 ^ "_plus_" ^ mangle_nexp n2
| Nexp_minus (n1, n2) -> mangle_nexp n1 ^ "_minus_" ^ mangle_nexp n2
@@ -369,10 +364,10 @@ let doc_lit_lem in_pat (L_aux(lit,l)) a =
| L_false -> utf8string "false"
| L_true -> utf8string "true"
| L_num i ->
- let ipp = string_of_big_int i in
+ let ipp = Big_int.to_string i in
utf8string (
if in_pat then "("^ipp^":nn)"
- else if lt_big_int i zero_big_int then "((0"^ipp^"):ii)"
+ else if Big_int.less i Big_int.zero 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*)*)
@@ -398,14 +393,14 @@ let doc_lit_lem in_pat (L_aux(lit,l)) a =
using this would require adding a dependency on ZArith to Sail. *)
let parts = Util.split_on_char '.' s in
let (num, denom) = match parts with
- | [i] -> (big_int_of_string i, unit_big_int)
+ | [i] -> (Big_int.of_string i, Big_int.of_int 1)
| [i;f] ->
- let denom = power_int_positive_int 10 (String.length f) in
- (add_big_int (mult_big_int (big_int_of_string i) denom) (big_int_of_string f), denom)
+ let denom = Big_int.pow_int_positive 10 (String.length f) in
+ (Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom)
| _ ->
raise (Reporting_basic.Fatal_error
(Reporting_basic.Err_syntax_locn (l, "could not parse real literal"))) in
- separate space (List.map string ["realFromFrac"; string_of_big_int num; string_of_big_int denom])
+ separate space (List.map string ["realFromFrac"; Big_int.to_string num; Big_int.to_string denom])
(* typ_doc is the doc for the type being quantified *)
let doc_quant_item vars_included (QI_aux (qi, _)) = match qi with
@@ -735,18 +730,6 @@ let doc_exp_lem, doc_let_lem =
| E_field((E_aux(_,(l,fannot)) as fexp),id) ->
let ft = typ_of_annot (l,fannot) in
(match fannot with
- | 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 = doc_id_lem tid ^^ underscore ^^ doc_id_lem id ^^ dot ^^ string "get_field" in
- let (ta,aexp_needed) =
- if typ_needs_printed t
- then (doc_tannot_lem (effectful eff) t, true)
- else (empty, aexp_needed) 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 =
if prefix_recordtype
@@ -802,7 +785,7 @@ let doc_exp_lem, doc_let_lem =
"E_vector of non-vector type") in
let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
let start = match nexp_simp start with
- | Nexp_aux (Nexp_constant i, _) -> string_of_big_int i
+ | Nexp_aux (Nexp_constant i, _) -> Big_int.to_string i
| _ -> if dir then "0" else string_of_int (List.length exps) in
let expspp =
match exps with
@@ -875,8 +858,8 @@ let doc_exp_lem, doc_let_lem =
| E_app_infix (e1,id,e2) ->
raise (Reporting_basic.err_unreachable l
"E_app_infix should have been rewritten before pretty-printing")
- | E_internal_let(lexp, eq_exp, in_exp) ->
- raise (report l "E_internal_lets should have been removed before pretty-printing")
+ | E_var(lexp, eq_exp, in_exp) ->
+ raise (report l "E_vars should have been removed before pretty-printing")
| E_internal_plet (pat,e1,e2) ->
let epp =
let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
@@ -997,12 +980,12 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
raise (Reporting_basic.err_unreachable Parse_ast.Unknown
("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start))
with
- | _ -> (zero_big_int, true) in
+ | _ -> (Big_int.zero, true) in
doc_op equals
(concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])])
(anglebars (concat [space;
doc_op equals (string "field_name") (string_lit (doc_id_lem fid)); semi_sp;
- doc_op equals (string "field_start") (string (string_of_big_int start)); semi_sp;
+ doc_op equals (string "field_start") (string (Big_int.to_string start)); semi_sp;
doc_op equals (string "field_is_inc") (string (if is_inc then "true" else "false")); semi_sp;
doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp;
doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in
@@ -1191,36 +1174,6 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
fromInterpValuePP ^^ hardline ^^ hardline ^^
fromToInterpValuePP ^^ hardline
else empty)
- | TD_register(id,n1,n2,rs) ->
- match n1, n2 with
- | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
- let dir_b = i1 < i2 in
- let dir = (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 add_big_int (sub_big_int i2 i1) unit_big_int else add_big_int (sub_big_int i1 i2) unit_big_int in
- let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in
- let tannot = doc_tannot_lem false vtyp in
- let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id);
- doc_range_lem r;]) in
- let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in
- doc_op equals
- (concat [string "type";space;doc_id_lem id])
- (doc_typ_lem vtyp)
- ^^ 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 ^^
- 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; string dir;
- break 0 ^^ brackets (align doc_rids)]))
| _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices")
let args_of_typ l env typ =
@@ -1377,29 +1330,22 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
if !opt_sequential then empty
else
let env = env_of_annot annot in
- (match typ with
- | 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 = 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
- let o = if is_order_inc order then "true" else "false" in
- (doc_op equals)
- (string "let" ^^ space ^^ doc_id_lem id)
- (string "Register" ^^ space ^^
- align (separate space [string_lit(doc_id_lem id);
- doc_nexp (size);
- doc_nexp (start);
- string o;
- string "[]"]))
- ^/^ hardline
- else raise (Reporting_basic.err_unreachable l
- ("can't deal with register type " ^ string_of_typ typ))
- else raise (Reporting_basic.err_unreachable l
- ("can't deal with register type " ^ string_of_typ typ)))
+ 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
+ let o = if is_order_inc order then "true" else "false" in
+ (doc_op equals)
+ (string "let" ^^ space ^^ doc_id_lem id)
+ (string "Register" ^^ space ^^
+ align (separate space [string_lit(doc_id_lem id);
+ doc_nexp (size);
+ doc_nexp (start);
+ string o;
+ string "[]"]))
+ ^/^ hardline
+ else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ))
+ else raise (Reporting_basic.err_unreachable l ("can't deal with register type " ^ string_of_typ typ))
| DEC_alias(id,alspec) -> empty
| DEC_typ_alias(typ,id,alspec) -> empty
@@ -1412,15 +1358,6 @@ let doc_spec_lem (VS_aux (valspec,annot)) =
(* | VS_val_spec (_,_,Some _,_) -> empty *)
| _ -> empty
-let find_regtypes defs =
- List.fold_left
- (fun acc def ->
- match def with
- | DEF_type (TD_aux(TD_register (Id_aux (Id tname, _), n1, n2, fields),_)) ->
- (tname, (n1, n2, fields)) :: acc
- | _ -> acc
- ) [] defs
-
let is_field_accessor regtypes fdef =
let is_field_of regtyp field =
List.exists (fun (tname, (_, _, fields)) -> tname = regtyp &&
@@ -1443,11 +1380,11 @@ let doc_regtype_fields (tname, (n1, n2, fields)) =
| BF_aux (BF_range (i, j), _) -> (i, j)
| _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown
("Unsupported type in field " ^ string_of_id fid ^ " of " ^ tname)) in
- let fsize = succ_big_int (abs_big_int (sub_big_int i j)) in
+ let fsize = Big_int.succ (Big_int.abs (Big_int.sub i j)) in
(* 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 (pred_big_int 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)));
@@ -1457,7 +1394,7 @@ let doc_regtype_fields (tname, (n1, n2, fields)) =
(concat [string "let "; parens (concat [string tname; underscore; doc_id_lem fid; rfannot])])
(concat [
space; langlebar; string " field_name = \"" ^^ doc_id_lem fid ^^ string "\";"; hardline;
- space; space; space; string (" field_start = " ^ string_of_big_int i ^ ";"); hardline;
+ space; space; space; string (" field_start = " ^ Big_int.to_string i ^ ";"); hardline;
space; space; space; string (" field_is_inc = " ^ dir ^ ";"); hardline;
space; space; space; string (" get_field = get_" ^ tname ^ "_" ^ string_of_id fid ^ ";"); hardline;
space; space; space; string (" set_field = set_" ^ tname ^ "_" ^ string_of_id fid ^ " "); ranglebar])
@@ -1491,7 +1428,7 @@ let rec doc_def_lem regtypes def =
let doc_defs_lem (Defs defs) =
- let regtypes = find_regtypes defs in
+ let regtypes = [] in
let field_refs = separate_map hardline doc_regtype_fields regtypes in
let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in
(separate empty typdefs ^^ field_refs, separate empty valdefs)
@@ -1564,10 +1501,10 @@ let doc_register_refs_lem registers =
raise (Reporting_basic.err_unreachable Parse_ast.Unknown
("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start))
with
- | _ -> (zero_big_int, true) in
+ | _ -> (Big_int.zero, true) in
concat [string "let "; idd; string " = <|"; hardline;
string " reg_name = \""; idd; string "\";"; hardline;
- string " reg_start = "; string (string_of_big_int start); string ";"; hardline;
+ string " reg_start = "; string (Big_int.to_string start); string ";"; hardline;
string " reg_is_inc = "; string (if is_inc then "true" else "false"); string ";"; hardline;
string " read_from = (fun s -> s."; field; string ");"; hardline;
string " write_to = (fun s v -> (<| s with "; field; string " = v |>)) |>"] in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 20:35:38 +0000