summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-08-23Move vector_string_to_bit_list from its odd place in Rewriter.rewrite_pat to ...Jon French
2018-08-22Fix a bug in nested vector concatenation patternsAlasdair Armstrong
2018-08-22Revert "rewrite_defs_pat_lits: add an explicit type annotation around generat...Jon French
2018-08-22rewrite_defs_pat_lits: add an explicit type annotation around generated id pa...Jon French
2018-08-21C: Correctly handle the kinds of patterns generated by mappingsAlasdair Armstrong
2018-08-20Refactor tuple conversions in Sail to C compilationAlasdair Armstrong
2018-08-18Correctly handle specialising polymorphic types in nested unionsAlasdair
2018-08-18Correctly specialise type annotation in polymorphic functionsAlasdair
2018-08-17Improve builtins testsAlasdair Armstrong
2018-08-17Coq: also introduce autocast at type annotationsBrian Campbell
2018-08-17Extend guarded patterns rewriting to exception catchingBrian Campbell
2018-08-16Add the type an expression was checked against to tannots, and use for CoqBrian Campbell
2018-08-16Use Set rather than Hashtbl in graph.mlAlasdair Armstrong
2018-08-16Remove unused ref typeAlasdair Armstrong
2018-08-16Various cleanups to ott grammarAlasdair Armstrong
2018-08-15Temporary fix for RISC-V Lem generationBrian Campbell
2018-08-15Get RISC-V on Coq into reasonable state to showBrian 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
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
2018-08-13Coq: drop redundant final wildcard clausesBrian Campbell
2018-08-13Guarded clauses rewrite: variable patterns subsume enumsBrian Campbell
2018-08-12Coq: handle enums in binders, make top-level patterns exhaustiveBrian Campbell
2018-08-10Coq: add some of string libraryBrian Campbell
2018-08-09Fix a bug by ensuring that monomorphic variant constructors do not get lifted...Alasdair Armstrong
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-08Fix ordering of generated anonymous types for each cdefAlasdair Armstrong
2018-08-07Revert "Warnings: deal with all the deprecation warnings"Alasdair Armstrong
2018-08-07More updates for fixing variant typesAlasdair Armstrong
2018-08-07Lem: print more bitvector typesBrian Campbell
2018-08-07Fix propagation of overly-specific types in early_return rewriteBrian Campbell
2018-08-07Improve cast introduction for LemBrian Campbell
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-03More work on fixing polymorphic constructor monomorphisationAlasdair Armstrong
2018-08-03Fix existential variable problems in monomorphisationBrian Campbell
2018-08-03Coq: generalise dependent pair handling a littleBrian 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-02Start working on a solution for correctly monomorphising polymorphic variant ...Alasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 01:32:02 +0000