summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-06Improve AST slicingAlasdair Armstrong
2019-03-06Add option to slice out printing and tracing functions when generating CAlasdair Armstrong
Make instruction dependency graph use graph.ml Expose incremental graph building functions for performance in graph.mli
2019-03-05Fix missing case in specializationAlasdair
2019-03-05More optimizations and improvments for C generationAlasdair Armstrong
Add some comments in constant_fold.ml
2019-03-05Add missing comma in armV8.sailAlasdair Armstrong
2019-03-05Add forgotten recursive function testBrian Campbell
2019-03-05Add Unallocated to the gen filesBen Simner
Adds the Unallocated sail ast node to be tracked by all the transformation files, to track the change made to sail1.
2019-03-05Coq: firstorder is better at the boolean goalsBrian Campbell
2019-03-05Coq: use setoid rewriting to apply under an existential binderBrian Campbell
2019-03-05Coq: use more local type information when constructing tuplesBrian Campbell
2019-03-05Coq: some debugging messagesBrian Campbell
2019-03-05Coq: output type-level Int definitionsBrian Campbell
2019-03-05Coq 8.9 compatibility fixBrian Campbell
2019-03-05Additional optimizations for C compilationAlasdair
2019-03-04Fix aarch64_small test XML for jenkinsAlasdair Armstrong
Rename rewrite_split_fun_constr_pats to rewrite_split_fun_ctor_pats as constr is commonly used as an abbreviation for constraint rather than constructor, and add a more descriptive comment.
2019-03-04Add test for building handwritten ARM to lem for JenkinsAlasdair Armstrong
2019-03-04Fix execute splitting to work when constructors have constraints.Alasdair Armstrong
Previously any constraints on constructors were just outright dropped when splitting the execute function in Lem generation. Now we get the constraints and type signature for each execute clause from the type given by Env.get_union_constructor, rather than by inferring the type of the pattern in each function clause. Currently this can still fail in the case where we have union U('x: Int), C1('x) = { ctor: {'y. C2('x, 'y), T('x, 'y)} } and val execute : forall 'z, C3('z). U('z) -> unit when C3 implies C1, and the body of an excute clause relies on the fact that C3 is stronger than C1, as each split function execute_ctor is only guaranteed to be constrained by some subset of C1. This seems unlikely to happen in practice though. Also fix a bug when binding P as int('T) against int('T) and similar cases, where the new type variable would cause the old type variable to become shadowed, but the constraint that the bound type variable and the old type variable are equal would not take this into account.
2019-03-04Merge branch 'sail2' of https://github.com/rems-project/sail into sail2Christopher Pulte
2019-03-04check in missing regfp2.sailChristopher Pulte
2019-03-04Do not store type synonyms as functions in the environmentAlasdair Armstrong
2019-03-04cleanupChristopher Pulte
2019-03-04Merge branch 'sail2' of https://github.com/rems-project/sail into sail2Christopher Pulte
2019-03-04last bit of sail1 to sail2 portingChristopher Pulte
2019-03-04Add location to warning in pattern completeness checkAlasdair Armstrong
2019-03-04more sail1-to-sail2 portingChristopher Pulte
2019-03-04more porting of armv8 from sail1 to sail2Christopher Pulte
2019-03-04moreChristopher Pulte
2019-03-02moreChristopher Pulte
2019-03-02moreChristopher Pulte
2019-03-02Merge branch 'sail2' of https://github.com/rems-project/sail into sail2Christopher Pulte
2019-03-02moreChristopher Pulte
2019-03-01WIP: Start working on being able to slice single instructions out of specsAlasdair Armstrong
2019-03-01Add some tricky test cases for quantified Sail AST typesAlasdair Armstrong
Fixes some bugs found by doing this
2019-03-01Coq: some library compatibility changesBrian Campbell
2019-03-01Add a test case for previous commitAlasdair Armstrong
Also make unifying int against int('n) work as expected for constructor applications.
2019-03-01Merge branch 'sail2' of https://github.com/rems-project/sail into sail2Christopher Pulte
2019-03-01Fix bug with naturals in quantified constructorsAlasdair Armstrong
2019-03-01Merge branch 'sail2' of https://github.com/rems-project/sail into sail2Christopher Pulte
2019-03-01Make Sail more flexible with existentials in union typesAlasdair Armstrong
Issues came up with Christophers translation of hand-written ARM into Sail2 where we were being overly pedantic about the exact position of existential quantifiers in constructors with multiple arguments. This commit generalises unify_typ and type_coercion_unify to be more flexible and support this. Should think at some point if unify_typ can be generalised further. This fix should fix the decode side of things, but may be some issues with the executes that still need looking into when existentials and multiple argument constructors are mixed.
2019-03-01Fill in some edge cases in monomorphisationBrian Campbell
2019-03-01more progressChristopher Pulte
2019-03-01Coq tidying: remove old definition, complete a pattern matchBrian Campbell
2019-03-01Coq: add a little bit of boolean solvingBrian Campbell
Just enough for RISC-V to go through
2019-03-01Coq: make iff `iff`Brian Campbell
Also drop unused implication function
2019-02-28Handle implicits in destruct_atom_nexpBrian Campbell
2019-02-28Coq: remove unused library definitionsBrian Campbell
2019-02-28Coq: Clean up rich boolean handling in backendBrian Campbell
Now generates something vaguely sensible for RISC-V, although the solver needs a little work. Adds type annotations around effectful, rich and/or expressions.
2019-02-28Coq: more for informative booleansBrian Campbell
Make internal_plet produce annotations (with code to replace unusable type variables) Add mappings for bool kids at bindings Add version of and_bool that proves a property
2019-02-28Coq: update tyvar merge information at other bindersBrian Campbell
2019-02-28Turn off some debugging messagesBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 18:51:00 +0000