summaryrefslogtreecommitdiff
path: root/src/pretty_print_sail.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/pretty_print_sail.ml')
-rw-r--r--src/pretty_print_sail.ml95
1 files changed, 69 insertions, 26 deletions
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 1fa14a7d..218ebf22 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -61,7 +61,7 @@ let doc_op symb a b = infix 2 1 symb a b
let doc_id (Id_aux (id_aux, _)) =
string (match id_aux with
| Id v -> v
- | DeIid op -> "operator " ^ op)
+ | Operator op -> "operator " ^ op)
let doc_kid kid = string (Ast_util.string_of_kid kid)
@@ -88,11 +88,11 @@ let rec doc_typ_pat (TP_aux (tpat_aux, _)) =
| TP_var kid -> doc_kid kid
| TP_app (f, tpats) -> doc_id f ^^ parens (separate_map (comma ^^ space) doc_typ_pat tpats)
-let rec doc_nexp =
+let rec doc_nexp nexp =
let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) =
match n_aux with
| Nexp_constant c -> string (Big_int.to_string c)
- | Nexp_app (Id_aux (DeIid op, _), [n1; n2]) ->
+ | Nexp_app (Id_aux (Operator op, _), [n1; n2]) ->
separate space [atomic_nexp n1; string op; atomic_nexp n2]
| Nexp_app (id, nexps) -> string (string_of_nexp nexp)
(* This segfaults??!!!!
@@ -119,7 +119,7 @@ let rec doc_nexp =
| Nexp_exp n -> separate space [string "2"; string "^"; atomic_nexp n]
| _ -> atomic_nexp nexp
in
- nexp0
+ nexp0 nexp
let doc_effect (Effect_aux (aux, _)) =
match aux with
@@ -136,7 +136,9 @@ let rec doc_nc nc =
| NC_equal (n1, n2) -> nc_op "==" n1 n2
| NC_not_equal (n1, n2) -> nc_op "!=" n1 n2
| NC_bounded_ge (n1, n2) -> nc_op ">=" n1 n2
+ | NC_bounded_gt (n1, n2) -> nc_op ">" n1 n2
| NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
+ | NC_bounded_lt (n1, n2) -> nc_op "<" n1 n2
| NC_set (kid, ints) ->
separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
| NC_app (id, args) ->
@@ -172,7 +174,7 @@ and doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
match typ_aux with
| Typ_id id -> doc_id id
| Typ_app (id, []) -> doc_id id
- | Typ_app (Id_aux (DeIid str, _), [x; y]) ->
+ | Typ_app (Id_aux (Operator str, _), [x; y]) ->
separate space [doc_typ_arg x; doc_typ_arg y]
| Typ_app (id, typs) when Id.compare id (mk_id "atom") = 0 ->
string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
@@ -210,21 +212,48 @@ and doc_arg_typs = function
| [typ] -> doc_typ typ
| typs -> parens (separate_map (comma ^^ space) doc_typ typs)
+let doc_kind (K_aux (k, _)) =
+ string (match k with
+ | K_int -> "Int"
+ | K_type -> "Type"
+ | K_bool -> "Bool"
+ | K_order -> "Order")
+
+let rec doc_kopts constants =
+ let is_in_group is_constant kind kopt =
+ Kind.compare kind (kopt_kind kopt) = 0 && KOptSet.mem kopt constants = is_constant
+ in
+ function
+ | kopt :: kopts ->
+ let is_constant = KOptSet.mem kopt constants in
+ let group, kopts = Util.take_drop (is_in_group is_constant (kopt_kind kopt)) kopts in
+ let attr = if is_constant then string "constant" ^^ space else empty in
+ parens (attr ^^ separate space (List.map (fun kopt -> doc_kid (kopt_kid kopt)) (kopt :: group))
+ ^^ space ^^ colon
+ ^^ space ^^ doc_kind (kopt_kind kopt))
+ ^^ begin match kopts with
+ | [] -> empty
+ | _ -> doc_kopts constants kopts
+ end
+ | [] -> empty
+
let doc_quants quants =
- let doc_qi_kopt (QI_aux (qi_aux, _)) =
- match qi_aux with
- | QI_id kopt when is_int_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])]
- | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])]
- | QI_id kopt when is_bool_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])]
- | QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])]
- | QI_const nc -> []
+ let rec get_constants = function
+ | QI_aux (QI_constant kopts, _) :: qis -> KOptSet.union (KOptSet.of_list kopts) (get_constants qis)
+ | _ :: qis -> get_constants qis
+ | [] -> KOptSet.empty
+ in
+ let rec get_kopts = function
+ | QI_aux (QI_id kopt, _) :: qis -> kopt :: get_kopts qis
+ | _ :: qis -> get_kopts qis
+ | [] -> []
in
let qi_nc (QI_aux (qi_aux, _)) =
match qi_aux with
- | QI_const nc -> [nc]
+ | QI_constraint nc -> [nc]
| _ -> []
in
- let kdoc = separate space (List.concat (List.map doc_qi_kopt quants)) in
+ let kdoc = doc_kopts (get_constants quants) (get_kopts quants) in
let ncs = List.concat (List.map qi_nc quants) in
match ncs with
| [] -> kdoc
@@ -238,11 +267,12 @@ let doc_param_quants quants =
| QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"]
| QI_id kopt when is_bool_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Bool"]
| QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"]
- | QI_const nc -> []
+ | QI_constraint _ -> []
+ | QI_constant _ -> []
in
let qi_nc (QI_aux (qi_aux, _)) =
match qi_aux with
- | QI_const nc -> [nc]
+ | QI_constraint nc -> [nc]
| _ -> []
in
let kdoc = separate (comma ^^ space) (List.concat (List.map doc_qi_kopt quants)) in
@@ -315,7 +345,6 @@ let rec doc_pat (P_aux (p_aux, (l, _)) as pat) =
| P_string_append [] -> string "\"\""
| P_string_append pats ->
parens (separate_map (string " ^ ") doc_pat pats)
- | P_record _ -> raise (Reporting.err_unreachable l __POS__ "P_record passed to doc_pat")
(* if_block_x is true if x should be printed like a block, i.e. with
newlines. Blocks are automatically printed as blocks, so this
@@ -359,7 +388,6 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
| E_block [] -> string "()"
| E_block exps ->
group (lbrace ^^ nest 4 (hardline ^^ doc_block exps) ^^ hardline ^^ rbrace)
- | E_nondet exps -> assert false
(* This is mostly for the -convert option *)
| E_app_infix (x, id, y) when Id.compare (mk_id "quot") id == 0 ->
separate space [doc_atomic_exp x; string "/"; doc_atomic_exp y]
@@ -387,10 +415,10 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
| E_list exps -> string "[|" ^^ separate_map (comma ^^ space) doc_exp exps ^^ string "|]"
| E_cons (exp1, exp2) -> doc_atomic_exp exp1 ^^ space ^^ string "::" ^^ space ^^ doc_exp exp2
| E_record fexps -> separate space [string "struct"; string "{"; doc_fexps fexps; string "}"]
- | E_loop (While, cond, exp) ->
- separate space [string "while"; doc_exp cond; string "do"; doc_exp exp]
- | E_loop (Until, cond, exp) ->
- separate space [string "repeat"; doc_exp exp; string "until"; doc_exp cond]
+ | E_loop (While, measure, cond, exp) ->
+ separate space ([string "while"] @ doc_measure measure @ [doc_exp cond; string "do"; doc_exp exp])
+ | E_loop (Until, measure, cond, exp) ->
+ separate space ([string "repeat"] @ doc_measure measure @ [doc_exp exp; string "until"; doc_exp cond])
| E_record_update (exp, fexps) ->
separate space [string "{"; doc_exp exp; string "with"; doc_fexps fexps; string "}"]
| E_vector_append (exp1, exp2) -> separate space [doc_atomic_exp exp1; string "@"; doc_atomic_exp exp2]
@@ -429,6 +457,10 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
| E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 ->
separate space [string "2"; string "^"; doc_atomic_exp exp]
| _ -> doc_atomic_exp exp
+and doc_measure (Measure_aux (m_aux, _)) =
+ match m_aux with
+ | Measure_none -> []
+ | Measure_some exp -> [string "termination_measure"; braces (doc_exp exp)]
and doc_infix n (E_aux (e_aux, _) as exp) =
match e_aux with
| E_app_infix (l, op, r) when n < 10 ->
@@ -470,7 +502,11 @@ and doc_atomic_exp (E_aux (e_aux, _) as exp) =
brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; equals; doc_exp exp3])
| E_vector_update_subrange (exp1, exp2, exp3, exp4) ->
brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4])
- | E_internal_value v -> string (Value.string_of_value v |> Util.green |> Util.clear)
+ | E_internal_value v ->
+ if !Interactive.opt_interactive then
+ string (Value.string_of_value v |> Util.green |> Util.clear)
+ else
+ string (Value.string_of_value v)
| _ -> parens (doc_exp exp)
and doc_fexps fexps =
separate_map (comma ^^ space) doc_fexp fexps
@@ -623,9 +659,7 @@ let doc_typdef (TD_aux(td,_)) = match td with
let doc_spec ?comment:(comment=false) (VS_aux (v, annot)) =
let doc_extern ext =
- let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^
- utf8string ("\"" ^ String.escaped id ^ "\"")) (ext b) in
- let docs = Util.option_these (List.map doc_backend ["ocaml"; "lem"; "smt"; "interpreter"; "c"]) in
+ let docs = List.map (fun (backend, rep) -> string (backend ^ ":") ^^ space ^^ utf8string ("\"" ^ String.escaped rep ^ "\"")) ext in
if docs = [] then empty else equals ^^ space ^^ braces (separate (comma ^^ space) docs)
in
match v with
@@ -643,6 +677,13 @@ let doc_prec = function
| InfixL -> string "infixl"
| InfixR -> string "infixr"
+let doc_loop_measures l =
+ separate_map (comma ^^ break 1)
+ (function (Loop (l,e)) ->
+ string (match l with While -> "while" | Until -> "until") ^^
+ space ^^ doc_exp e)
+ l
+
let rec doc_scattered (SD_aux (sd_aux, _)) =
match sd_aux with
| SD_function (_, _, _, id) ->
@@ -679,6 +720,8 @@ let rec doc_def def = group (match def with
| DEF_measure (id,pat,exp) ->
string "termination_measure" ^^ space ^^ doc_id id ^/^ doc_pat pat ^^
space ^^ equals ^/^ doc_exp exp
+ | DEF_loop_measures (id,measures) ->
+ string "termination_measure" ^^ space ^^ doc_id id ^/^ doc_loop_measures measures
| DEF_pragma (pragma, arg, l) ->
string ("$" ^ pragma ^ " " ^ arg)
| DEF_fixity (prec, n, id) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:59:35 +0000