| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
Now constraints on type constructors are checked correctly when
checking that types are well formed using Env.wf_typ. The arity and
kind of type constructor arguments are also checked in the same way.
Also some general cleanups to the type checker code, with some
auxillary functions being moved to more appropriate files.
|
|
|
|
For example,
val test = { ocaml: "test_ocaml" } : unit -> unit
will only be external for OCaml. For other backends, it will have to be
defined.
|
|
- Support tuples in lexps
- Rewrite trivial sizeofs
- Rewrite early returns more aggressively
- Support let bindings with ticked variables (binding both a type-level and
term-level variable at the same time)
|
|
Can now handle nexps such as (2**65 - 1). Uses big_ints for comparisons, and
keeps original nexps in the AST.
|
|
|
|
|
|
sail.ml
Current REMS install script and Jenkins CI server is on an older ocaml
which doesn't have this function in String.
|
|
|
|
|
|
|
|
Note: the resulting Lem file generated may or may not actually work properly with the interpreter (i.e. it might have too many unknowns); still in the process of debugging some changes there.
|
|
|
|
representation of types to support unification; importing support modules from Lem including pp and util
|
