diff options
| author | Alasdair Armstrong | 2017-12-11 18:34:59 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-12-11 18:34:59 +0000 |
| commit | 89d1f43805ec64ff3537026a84d9a7816a5c23a6 (patch) | |
| tree | d7da4511b099b5f80bda7b30d3d2902457658405 /src/pretty_print_sail2.ml | |
| parent | 47f1892406b5c10d06eb99af40d4523b93b2f254 (diff) | |
Prototype interactive mode for sail.
Requires linenoise library (opam install linenoise) for readline
support. Use 'make isail' to build sail with interactive
support. Plain 'make sail' should work as before with no additional
dependencies.
Use 'sail -i <commands>' to run sail interactively, e.g.
sail -new_parser -i test/ocaml/prelude.sail test/ocaml/trycatch/tc.sail
then try some commands for typechecking and evaluation
sail> :t main
sail> main ()
Doesn't use the lem interpreter right now, instead has a small
operational semantics in src/interpreter.ml, but this is not very
complete and will be changed/removed.
Diffstat (limited to 'src/pretty_print_sail2.ml')
| -rw-r--r-- | src/pretty_print_sail2.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index 0c531301..17185cc9 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -171,13 +171,17 @@ let doc_quants quants = | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs) -let doc_typschm (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = + + +let doc_binding (TypQ_aux (tq_aux, _), typ) = match tq_aux with | TypQ_no_forall -> doc_typ typ | TypQ_tq [] -> doc_typ typ | TypQ_tq qs -> string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ +let doc_typschm (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_binding (typq, typ) + let doc_typschm_typ (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = doc_typ typ let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = @@ -322,7 +326,8 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = end (* Resugar an assert with an empty message *) | E_throw exp -> string "throw" ^^ parens (doc_exp exp) - | E_try (exp, pexps) -> assert false + | E_try (exp, pexps) -> + separate space [string "try"; doc_exp exp; string "catch"; doc_pexps pexps] | E_return exp -> string "return" ^^ parens (doc_exp exp) | E_internal_return exp -> string "internal_return" ^^ parens (doc_exp exp) | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 -> @@ -368,6 +373,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) | _ -> parens (doc_exp exp) and doc_fexps (FES_aux (FES_Fexps (fexps, _), _)) = separate_map (comma ^^ space) doc_fexp fexps @@ -523,3 +529,5 @@ let doc_defs (Defs(defs)) = separate_map hardline doc_def defs let pp_defs f d = ToChannel.pretty 1. 80 f (doc_defs d) + +let pretty_sail f doc = ToChannel.pretty 1. 120 f doc |