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/initial_check.mli | |
| 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/initial_check.mli')
| -rw-r--r-- | src/initial_check.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/initial_check.mli b/src/initial_check.mli index 01cf3bec..6059b0ac 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -59,3 +59,5 @@ val process_ast : order -> Parse_ast.defs -> unit defs val val_spec_ids : 'a defs -> IdSet.t val val_spec_of_string : order -> id -> string -> unit def + +val exp_of_string : order -> string -> unit exp |
