From fbcc27ca1bd3801beac0338e657b933d6a9c8f95 Mon Sep 17 00:00:00 2001 From: Jon French Date: Thu, 27 Dec 2018 12:19:44 +0000 Subject: refactor val-spec AST to store externs as an assoc-list rather than a function (preparing for marshalling) --- src/pretty_print_sail.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'src/pretty_print_sail.ml') diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 0b0a8305..179ef208 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -538,9 +538,7 @@ let doc_typdef (TD_aux(td,_)) = match td with let doc_spec (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 -- cgit v1.2.3 From 4f14ccb421443dbc10b88e190526dda754f324aa Mon Sep 17 00:00:00 2001 From: Jon French Date: Wed, 13 Mar 2019 17:11:39 +0000 Subject: Pretty_print_sail: don't use colour to highlight E_internal_value --- src/pretty_print_sail.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/pretty_print_sail.ml') diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 56026c81..9712b62c 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -470,7 +470,7 @@ 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 -> string (Value.string_of_value v (* |> Util.green |> Util.clear *)) | _ -> parens (doc_exp exp) and doc_fexps fexps = separate_map (comma ^^ space) doc_fexp fexps -- cgit v1.2.3 From 1f421b865a87a161a82550443a0cf39aa2642d9c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Mon, 15 Apr 2019 12:08:28 +0100 Subject: Basic loop termination measures for Coq Currently only supports pure termination measures for loops with effects. The user syntax uses separate termination measure declarations, as in the previous recursive termination measures, which are rewritten into the loop AST nodes before type checking (because it would be rather difficult to calculate the correct environment to type check the separate declaration in). --- src/pretty_print_sail.ml | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) (limited to 'src/pretty_print_sail.ml') 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) -> -- cgit v1.2.3