summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-08-17Extend guarded patterns rewriting to exception catchingBrian Campbell
Also fix nested matches and generic rewriting under E_throw.
2018-08-16Add the type an expression was checked against to tannots, and use for CoqBrian Campbell
Tweak extra Coq files to match. Tweak early return rewrite to use declared return type, which can always be put into an E_cast.
2018-08-16Use Set rather than Hashtbl in graph.mlAlasdair Armstrong
Removes the need for the node type to have a valid Hash function
2018-08-16Remove unused ref typeAlasdair Armstrong
2018-08-16Ressurect builtin tests, and add parallel test runner scriptAlasdair Armstrong
Add new python test runner script, which allows tests to be run in parallel before collecting the results. This makes the tests run a lot faster, especially for the builtins and C compilation tests. Also handles reporting errors mushc more nicely than the previous way of doing it in shell script.
2018-08-16Various cleanups to ott grammarAlasdair Armstrong
Add additional well-formedness check when calling typing rules
2018-08-15Temporary fix for RISC-V Lem generationBrian Campbell
2018-08-15Snapshot of Coq from the RISC-V modelBrian Campbell
2018-08-15Get RISC-V on Coq into reasonable state to showBrian Campbell
- Fill in Coq builtins for more of the RISC-V prelude - Update Barriers - More general autocast - Temporary sub_nat definition (until the backend handles nat better) - Patch to bring results into a reasonable state - Use Let rather than Definition for non-dependent top-level values
2018-08-14Coq: attempt a quick proof before an indepth oneBrian Campbell
2018-08-14Improve error messages from C backend, and fix issues with assigning to pointersAlasdair Armstrong
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 06:39:23 +0000