summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-08-14Remove some comments from C outputAlasdair Armstrong
Cleanup some debugging output
2018-08-14Merge remote-tracking branch 'origin/sail2' into polymorphic_variantsAlasdair Armstrong
2018-08-13Add graph library graph.ml, and use to correctly sort type definitionsAlasdair
2018-08-13Remove old specialisation code in specialize.mlAlasdair
2018-08-13Sort ctype_defs in dependency order after specialisationAlasdair
We now generate anonymous types in the correct order, but post specialisation more dependencies can occur between named types, so an additional sorting step is needed to ensure that these happen in the correct order. In theory we could end up with circular dependencies here that don't exist at the Sail source level, but this shouldn't occur often (or ever) in practice. I think this is fixable but it would require some code generator changes.
2018-08-13More RISC-V built-in type constraintsBrian Campbell
2018-08-13Coq: more strings for RISC-VBrian Campbell
2018-08-13Coq: drop redundant final wildcard clausesBrian Campbell
Deals with pattern matches generated from mappings, plus the occasional error.
2018-08-13Add constraints to RISC-V duopod, makefile rulesBrian Campbell
2018-08-13RISC-V: mult_range is ill-typed, use mult_atom insteadBrian Campbell
2018-08-13Guarded clauses rewrite: variable patterns subsume enumsBrian Campbell
Prevents redundant clauses.
2018-08-13Basic Coq support for RISC-VBrian Campbell
Note that constraints have been added to ensure that all bitvector types are inhabited.
2018-08-13Coq: drop irrelevant definitions before constraint solvingBrian Campbell
(which were slowing down RISCV unacceptably because dealing with the xlen max/min values is surprisingly expensive)
2018-08-12Coq: handle enums in binders, make top-level patterns exhaustiveBrian Campbell
2018-08-10Coq: add some of string libraryBrian Campbell
2018-08-10Merge pull request #19 from Smattr/5DAF5338-94B5-4F7A-A1CB-1CBB72ED7E93Alasdair Armstrong
fix tutorial infix example
2018-08-09fix tutorial infix exampleMatthew Fernandez
The syntax for these directives requires the precedence first. E.g. a real world version of this in riscv/prelude.sail.
2018-08-09Fix a bug by ensuring that monomorphic variant constructors do not get ↵Alasdair Armstrong
lifted types Add a test case for nested variant constructors
2018-08-09Add type information to AP_app constructorsAlasdair Armstrong
2018-08-09Fix bugs involving multi-argument variant type constructorsAlasdair Armstrong
2018-08-09Coq: debugging on top-level letsBrian Campbell
2018-08-09Coq: tidy up debugging messagesBrian Campbell
2018-08-09Coq: decompose dependent pairs at internal_plet as well as letBrian Campbell
2018-08-09Coq: handle nats like ranges, not atomsBrian Campbell
2018-08-09Coq: a bit more handling of unknown constraintsBrian Campbell
2018-08-08Fix ordering of generated anonymous types for each cdefAlasdair Armstrong
2018-08-07Revert "Warnings: deal with all the deprecation warnings"Alasdair Armstrong
One day we will be free from the 4.02.3 menace, but today is not that day. :( This should fix Sail on Jenkins This reverts commit 86e29bcbb1597c4ef1f6cae8edbeed42f9a31414.
2018-08-07More updates for fixing variant typesAlasdair Armstrong
2018-08-07Lem: print more bitvector typesBrian Campbell
Especially for return expressions, which fixes a test case
2018-08-07Fix propagation of overly-specific types in early_return rewriteBrian Campbell
2018-08-07Improve cast introduction for LemBrian Campbell
Handles mutable variables and conditionals (there are still some corner cases that don't appear in Aarch64 to do). The pretty printer is now back to preferring to use concrete types, but has a special case for casts to print more general types.
2018-08-06Cast each argument to a polymorphic constructor into it's most general typeAlasdair Armstrong
2018-08-06Make sure monomorphic constructors are preservedAlasdair Armstrong
2018-08-06Add a simple test case for polymorphic variant typeAlasdair Armstrong
2018-08-06More fixes for polymorphic data typesAlasdair Armstrong
2018-08-03Merge pull request #18 from Smattr/C756D3DD-F006-4132-A3E3-27856A697A25Alasdair Armstrong
fix some typos
2018-08-03More work on fixing polymorphic constructor monomorphisationAlasdair Armstrong
2018-08-03Fix existential variable problems in monomorphisationBrian Campbell
One due to using raw types from the type checker in casts without trying to turn them into sane types, the other due to forgetting to use the constraint when trying to simplify sizes in existential types. Both triggered because the type checker now records more specific types.
2018-08-03Coq: use a dummy constraint when the real one is unknownBrian Campbell
Not really what we want, but a useful placeholder because of the widespread use of ex_int.
2018-08-03Coq: generalise dependent pair handling a littleBrian Campbell
1. for monadic values (not in a terribly useful way, though) 2. for more types
2018-08-02fix some typosMatthew Fernandez
2018-08-02Coq mips: fix deprecation warningBrian Campbell
2018-08-02Coq: remove type removal holdover from Lem backend, add MIPS lemmaBrian Campbell
2018-08-02Coq: proper precedence for constraints (both prop and bool)Brian Campbell
2018-08-02Coq: limit eauto to ensure termination in reasonable timeBrian Campbell
2018-08-02Fill in more Coq builtins for aarch64Brian Campbell
2018-08-02Update a few prover gitignoresBrian Campbell
2018-08-02Support for comment commands in emacs modeBrian Campbell
2018-08-02Merge pull request #17 from hirataqdees/patch-1Alasdair Armstrong
Update INSTALL.md
2018-08-02Start working on a solution for correctly monomorphising polymorphic variant ↵Alasdair Armstrong
types
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 15:42:07 +0000