summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-07-03Update to copytype and ccseal -- now use belt and braces approach when handli...Robert Norton
2017-06-30Split bit patterns for monomorphisation, do equality checksBrian Campbell
2017-06-30Added flow types to new typecheckerAlasdair Armstrong
2017-06-30add more tests for sail library. Can't compile entire file due to sail perfor...Robert Norton
2017-06-29Rewrite bitvector patternsThomas Bauereiss
2017-06-29Added a large test case to the test-suiteAlasdair Armstrong
2017-06-29Created prelude.sail for initial typing environmentAlasdair Armstrong
2017-06-29Propagate type information from reducing case expressionsBrian Campbell
2017-06-29Ocamlbuild targets should always be remadeBrian Campbell
2017-06-29beginnings of a sail library test suite.Robert Norton
2017-06-29Added support for set constraintsAlasdair Armstrong
2017-06-29Additional tests for overloading and vector patternsAlasdair Armstrong
2017-06-29Various improvements to typecheckerAlasdair Armstrong
2017-06-28User defined overloaded operatorsAlasdair Armstrong
2017-06-28Improvements to implicit type castingAlasdair Armstrong
2017-06-28Reduce simple enumeration cases during monomorphisationBrian Campbell
2017-06-28Use more plausible type for E_caseBrian Campbell
2017-06-27More features in bi-directional typecheckerAlasdair Armstrong
2017-06-26Added register fields for l-values expressions, and enumerationsAlasdair Armstrong
2017-06-24Added implicit castingAlasdair Armstrong
2017-06-23Added support for overloaded operatorsAlasdair Armstrong
2017-06-23Support for more sail constructsAlasdair Armstrong
2017-06-23Get rid of bogus singleton pattern warningsBrian Campbell
2017-06-23Add option for monomorphisation splittingBrian Campbell
2017-06-23Basic constant propagation for partial monomorphisationBrian Campbell
2017-06-22Added basic if statements without flow constraintsAlasdair Armstrong
2017-06-22Added vector subrange support, and testsAlasdair Armstrong
2017-06-22Added support for vector append and indexingAlasdair Armstrong
2017-06-22Can now typecheck register declarations and assignmentsAlasdair Armstrong
2017-06-22Added support for bitvectorsAlasdair Armstrong
2017-06-22fix three different copies of the hardware_quot function to do proper trucati...Robert Norton
2017-06-22add a 'print' built-in function handy for writing sail tests.Robert Norton
2017-06-22fix a typo spotted in CPtrCmp instruction -- CLEU was using signed comparison...Robert Norton
2017-06-22Initial partial monomorphisation workBrian Campbell
2017-06-22revised ccopytype with check for offset being in bounds and clearing tag inst...Robert Norton
2017-06-21MergeThomas Bauereiss
2017-06-21Pretty-print bitvector expressionsThomas Bauereiss
2017-06-19Fix Show on Lem bitvectorBrian Campbell
2017-06-16Some small changes to bi-directional checkerAlasdair Armstrong
2017-06-16Some Isabelle fixes for word version of sail_valuesBrian Campbell
2017-06-16prefer arithmetic on integers followed by cast to bit[64] in CCopyType.Robert Norton
2017-06-16remove unnecessary local variable definitions copy and pasted from cbuildcap.Robert Norton
2017-06-16fix previous commit so that it builds.Robert Norton
2017-06-16implement new CBuildCap and CCopyType instrucitons for ISAv6.Robert Norton
2017-06-15Pretty-print bitvector typesThomas Bauereiss
2017-06-15Added support for default order declarations.Alasdair Armstrong
2017-06-15Prototype Bi-directional type checking algorithm for sailAlasdair Armstrong
2017-06-15Replace sail_values.lem with Brian's machine word versionThomas Bauereiss
2017-06-14Add a work-in-progress version of sail_values.lemBrian Campbell
2017-06-13Add Makefile and ROOT for Isabelle libraryThomas Bauereiss