summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2019-03-19Coq: more test workBrian Campbell
- add dummy print_bits function - support int(1) like types in axioms
2019-03-19Coq: more work on testsBrian Campbell
- skip a few more that aren't supported yet - produce better debugging information (in particular, in the right order) - avoid some autocasts that aren't supported yet and are usually unnecessary - Handle more constraints like `8 * n = 8 * ?Goal`
2019-03-18Add non-negative constraints for zeros/onesBrian Campbell
2019-03-15Various monomorphisation tweaks and fixesThomas Bauereiss
2019-03-15Make mono_rewrites less dependant on ASL preludeThomas Bauereiss
... so that it can be more easily used for other specs. Also add some functions to vector_dec.sail to support this.
2019-03-15Coq: some progress on the test suiteBrian Campbell
Rewrite <> true/false in goals. Correct implicits in record and variant types. Use expanded valspecs from the type checker in axioms. Allow list notations in type definitions. Skip some not-yet-supported tests.
2019-03-15Coq: better loop handling, discharge some related proof obligationsBrian Campbell
2019-03-13C: Add missing update_lbits builtinAlasdair Armstrong
2019-03-12Coq: try non-linear nia solver tooBrian Campbell
2019-03-12Coq: fix some boolean issues seen in armBrian Campbell
Fixes bad precedence issues, removes an out-of-date special case that's not necessary, and solves more goals.
2019-03-08Fix the Coq mapping for eq_string in Sail lib.Prashanth Mundkur
2019-03-08Adds the DC and IC instructions to AArch64_small;Shaked Flur
Also, removes etc/regfp.sail and etc/regfp2.sail in favour of lib/regfp.sail
2019-03-07Fix bug in a mono rewrite helper functionThomas Bauereiss
2019-03-07Coq: apply a little brute force in some boolean goalsBrian Campbell
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 8.9 compatibility fixBrian Campbell
2019-03-05Additional optimizations for C compilationAlasdair
2019-03-01Coq: some library compatibility changesBrian Campbell
2019-03-01Coq: add a little bit of boolean solvingBrian Campbell
Just enough for RISC-V to go through
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: some work on bool simplificationBrian Campbell
This introduces some simplification of informative booleans, but tries too hard to eliminate all of the existentials resulting in difficulties in and/or trees.
2019-02-25Fix some builtins, and make mod_int return naturalAlasdair Armstrong
2019-02-21Allow monomorphisation with C generationAlasdair
Run C tests with -O -Oconstant_fold -auto_mono
2019-02-08Add missing functions to HOL monad wrapperThomas Bauereiss
Also make the rewriter keep failed assertions in output when pruning blocks.
2019-02-07Monomorphisation tweaks for v8.5Thomas Bauereiss
Various tweaks to the monomorphisation rewrites. Disable old sizeof rewriting for Lem backend and rely on the type checker rewriting implicit arguments. Also avoid unifying nexps with sums, as this can easily fail due to commutativity and associativity.
2019-02-06Fix some testsAlasdair Armstrong
2019-02-06Remove all sizeof rewriting from C compilationAlasdair
All sizeof expressions now removed by the type-checker, so it's now properly a type error if they cannot be removed rather than a bizarre re-write error. This also greatly improves compilation speed overall, at the expense of the first type-checking pass.
2019-02-04Fix some warningsAlasdair Armstrong
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-02-01Tweak HOL LEM_DIR to match riscv makefileBrian Campbell
2019-02-01Make hol libraries use opam Lem library by defaultBrian Campbell
2019-01-31Build Isabelle heap image instead of just running sessionThomas Bauereiss
2019-01-31Adapt HOL library to monad changesThomas Bauereiss
2019-01-31Merge branch 'monads' into asl_flow2Thomas Bauereiss
2019-01-29Fixes for full v8.5Alasdair Armstrong
2019-01-29Add a few more type annotations after mono rewritesThomas Bauereiss
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-23Don't let "make" fail unnecessarily in lib/isabelleThomas Bauereiss
Only check for availability of Lem library if actually trying to build an Isabelle heap image.
2019-01-22Don't hardcode location of BBV libraryThomas Bauereiss
2019-01-22Make sure we optimize constrained union constructorsAlasdair
2019-01-21The RISCV environment variable collides with common usage by the RISC-V ↵Prashanth Mundkur
toolchain; use SAIL_RISCV instead to refer to sail-riscv.
2019-01-21Pass Lem library path to IsabelleThomas Bauereiss
2019-01-21Don't require manual set up of Isabelle session directoriesThomas Bauereiss
Since Isabelle 2018, specifying the same directory both on the command line and persistently in the user's ROOTS file is allowed, so we don't have to choose between one or the other any more.
2019-01-21Fix build of Isabelle documentationThomas Bauereiss
2019-01-14Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-10Fixes so 8.5 with vector instructions compiles to CAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 13:33:56 +0000