summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-11-03Make nexp_simp a little smarterBrian Campbell
2017-11-02Added monomorphism restriction to undefined values.Alasdair Armstrong
What does this mean? Basically undefined values can't be created for types that contain free type variables, so for example: undefined : list(int) is good, but undefined : list('a) is bad. The reason we want to do this is because we can't compile them away statically, and this leads to situations where type-checkable code fails in the rewriter and gives horribly confusing error messages that don't relate to code the user wrote at all. As an example the following used to typecheck, but fail in the rewriter with a confusing error message, whereas now the typechecker should reject all cases which would trigger that failure in rewriting. val test : forall ('a:Type). list('a) -> unit effect {wreg, undef} function test xs = { xs_mut = xs; xs_mut = undefined; (* We don't know what kind of undefined 'a is *) () } There's a slight hitch, namely that in the undefined_type functions created by the -undefined_gen option, we do want to allow functions that have polymorphic undefined values, so that we can generate undefined generators for polymorphic datatypes such as: union option ('a:Type) = { Some : 'a, None } These functions are always have a specific form that allows the rewriter to succesfully remove the polymorphic undefined value for the 'a argument for Sone. As such there's a flag in the typechecking environment for polymorphic undefineds that is enabled when it sees a function with the undefined_ name prefix. Also: Fixed some test cases that were broken due to escape effect being added to assert.
2017-11-02Merge branch 'experiments'Thomas Bauereiss
2017-11-02Fix a few AST and parsing-related bugsThomas Bauereiss
2017-11-02Optionally generate an initial register state for the sequential Lem shallow ↵Thomas Bauereiss
embedding Checks for command-line flag -undefined_gen and uses the undefined value generator functions of the form undefined_typ to initialise registers
2017-11-02Fix translation of repeat-until loops to LemThomas Bauereiss
2017-11-02Handle "undefined" type-level sizes in monomorphisationBrian Campbell
2017-11-01Support bitvector-size-parametric functions in Lem outputBrian Campbell
Translates atom('n) types into itself('n) types that won't be erased Also exports more rewriting functions
2017-11-01Fix some missing nexp simplification in Lem outputBrian Campbell
2017-10-31Fixed wrong image for List-remove.svgAlasdair Armstrong
2017-10-31Added trace viewer application for traces produced by sail -ocaml_traceAlasdair Armstrong
See README file for how to set up and use
2017-10-31Improvements to register read tracing in ocaml backendAlasdair Armstrong
2017-10-31Pretty-print Sail assertions in LemThomas Bauereiss
Map to calls to monadic function assert_exp that throws an exception if the assertion is false
2017-10-31Fix bug in topological sorting of val-specsThomas Bauereiss
Put them before the function they declare
2017-10-31Remove redundant nexp simplification functionThomas Bauereiss
2017-10-27Fixed some ocaml backend related bugsAlasdair Armstrong
2017-10-26Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ↵Alasdair Armstrong
experiments
2017-10-26Unfold nexp abbreviations for pretty-printingThomas Bauereiss
2017-10-26Update val specs after rewriting functionsThomas Bauereiss
2017-10-26Experiment with pretty-printing non-atomic nexps in LemThomas Bauereiss
2017-10-26Updated ocaml backend so tracing instrumentation is optional.Alasdair Armstrong
Cleaned up the option list in sail.ml
2017-10-25Allow mutually recursive functionsThomas Bauereiss
2017-10-25Point sail/src makefile at ott file in language/Alasdair Armstrong
2017-10-25List.cons is too newBrian Campbell
2017-10-25Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-25Generate ast.ml from ott file and update makefile.Alasdair Armstrong
Fix until loop not being counted as sugar
2017-10-25Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-25Alternative low-memory version of barrier_kindCompareBrian Campbell
2017-10-25Avoid name clash in generated LemBrian Campbell
(complains due to added val spec)
2017-10-24Make nexp simplifier handle recursion properlyBrian Campbell
2017-10-24More succinct syntax in new parser for externed valspecs which shareAlasdair Armstrong
the same name between sail and the target
2017-10-24Print type annotations in Lem with type variablesBrian Campbell
(includes variables for bitvector sizes)
2017-10-24Limit quantifiers printed in Lem to type variables that actuallyBrian Campbell
appear in the output
2017-10-24Handle existential types in Lem backend by stripping them andBrian Campbell
checking that the type variables visible in the output aren't existential
2017-10-24Generate undefined_bitvector function when targeting machine wordsBrian Campbell
2017-10-24Produce debug message when an expression can't be converted to a constraintBrian Campbell
2017-10-24Remove special case for boolean (as opposed to bool)Brian Campbell
2017-10-23Type check external castsBrian Campbell
2017-10-23Added effect set pretty printing for new parserAlasdair Armstrong
Also added some new utility functions in ast_util
2017-10-23Added support for better tracing in ocaml backendAlasdair Armstrong
Fixed an issue in ast.ml with uneccessary type variables
2017-10-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-19Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
2017-10-19Fix pretty-printing of type abbreviation definitions with argumentsThomas Bauereiss
2017-10-19Mangle names with '#' characters in Lem pretty-printingThomas Bauereiss
2017-10-19Rewrite undefined values, add type annotations to early returnsThomas Bauereiss
2017-10-19Make some potentially non-terminating library functions terminateThomas Bauereiss
2017-10-19Preserve more type environment information during rewritingThomas Bauereiss
Fixes a bug where resolving a type synonym failed in the Lem pretty-printer due to a missing type environment.
2017-10-19Follow AST changes in (Lem) pretty-printersThomas Bauereiss
2017-10-18Fixes and updates to ocaml backend to compile aarch64_no_vectorAlasdair Armstrong
2017-10-18Merge branch 'experiments' of Peter_Sewell/sail into mono-experimentsBrian Campbell
(and fix up monomorphisation)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 23:31:08 +0000