diff options
Diffstat (limited to 'src/pretty_print_sail.ml')
| -rw-r--r-- | src/pretty_print_sail.ml | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 7f3a2b63..e46f784e 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -387,10 +387,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 +429,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 -> @@ -643,6 +647,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 +690,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) -> |