| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-21 | More work on quantifier elimination pass | Alasdair Armstrong | |
| Also added a rewriting pass that removes the cast annotations and operator overloading declarations from the AST because they arn't supported by the interpreter. | |||
| 2017-08-21 | Modified sizeof rewriting pass so it can correctly deal with existentials. | Alasdair Armstrong | |
| Basically we needed to make the rewriting step for E_sizeof and E_constraint more aggressively try to rewrite those expressions from variables in scope, without adding new parameters to pass the type variables at runtime, as this can break in the presence of existential quantification. Still some cleanup to do in this code, but tests on the arm spec show that it now introduces the minimal amount of new parameters. | |||
| 2017-08-18 | Fixed a bug where sizeof re-writing fail for aliased type arguments | Alasdair Armstrong | |
| Also: Merge remote-tracking branch 'origin/sail_new_tc' into experiments | |||
| 2017-08-17 | Work on E_constraint removal pass and diagnosing bugs in E_sizeof removal pass | Alasdair Armstrong | |
| 2017-08-17 | Add E_constraint support to re-writer | Alasdair Armstrong | |
| 2017-08-17 | Add support for register types other than bitvector to state monad | Thomas Bauereiss | |
| Make state monad parametric in register state, and generate a record with registers from the Sail spec | |||
| 2017-08-17 | Various sail fixes for ASL hexapod | Alasdair Armstrong | |
| 2017-08-16 | Added the feature to bind type variables in patterns. | Alasdair Armstrong | |
| The reason you want this is to do something like (note new parser only): ********* default Order dec type bits 'n:Int = vector('n - 1, 'n, dec, bit) val zeros : forall 'n. atom('n) -> bits('n) val decode : bool -> unit function decode b = { let 'datasize: {|32, 64|} = if b then 32 else 64; let imm: bits('datasize) = zeros(datasize); () } ********* for the ASL decode functions, where the typechecker now knows that the datasize variable and the length of imm are the same. | |||
| 2017-08-15 | Merge remote-tracking branch 'origin/mono-experiments' into experiments | Alasdair Armstrong | |
| 2017-08-15 | Removed Typ_arg_effect - nobody used it and it isn't supported by the backends. | Alasdair Armstrong | |
| 2017-08-15 | Export existential destructuring function in type_check.mli. | Alasdair Armstrong | |
| Also rename some functions for consistency. | |||
| 2017-08-15 | Export utility functions from type_check.ml | Alasdair Armstrong | |
| 2017-08-15 | Menhir parser support for try/catch | Alasdair Armstrong | |
| 2017-08-15 | Improve and simplify handling of mutable local variables | Thomas Bauereiss | |
| 2017-08-15 | Added exceptions and try/catch blocks to AST and typechecker in order | Alasdair Armstrong | |
| to translate exceptions in ASL. See test/typecheck/pass/trycatch.sail. | |||
| 2017-08-14 | Existentials in free type var functions | Brian Campbell | |
| 2017-08-14 | Some overloaded equality support in monomorphisation | Brian Campbell | |
| 2017-08-14 | Merge remote-tracking branch 'origin/master' into experiments | Alasdair Armstrong | |
| 2017-08-14 | Merge remote-tracking branch 'origin/mono-experiments' into experiments | Alasdair Armstrong | |
| 2017-08-14 | More constructs in menhir parser, plus support for both left and right infix ↵ | Alasdair Armstrong | |
| operators. | |||
| 2017-08-14 | Keep all asserts in the program during type checking | Brian Campbell | |
| 2017-08-14 | Don't reverse lexp tuple during type checking | Brian Campbell | |
| 2017-08-12 | Resolve ambiguity between negation of integers and bools | Thomas Bauereiss | |
| 2017-08-12 | Fix compilation issue for 32-bit systems | Thomas Bauereiss | |
| 2017-08-11 | Menhir for new parser, ocamlyacc for old | Brian Campbell | |
| 2017-08-11 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-08-11 | Make type checking just clever enough to solve 8*n = constant | Brian Campbell | |
| 2017-08-10 | Merge remote-tracking branch 'origin/sail_new_tc' into experiments | Alasdair Armstrong | |
| Conflicts: src/pretty_print_common.ml | |||
| 2017-08-10 | Fix bug with subtyping in let bindings | Alasdair Armstrong | |
| 2017-08-10 | Improved operator support for test menhir parser | Alasdair Armstrong | |
| 2017-08-10 | Experimenting with alternate parser | Alasdair Armstrong | |
| 2017-08-10 | Add support for early return to Lem backend | Thomas Bauereiss | |
| Implemented using the exception monad, by throwing and catching the return value | |||
| 2017-08-10 | Disable menhir on this branch | Brian Campbell | |
| (until location information is updated) | |||
| 2017-08-10 | Merge branch 'experiments' into mono-experiments | Brian Campbell | |
| 2017-08-10 | Existentials in Lem AST output | Brian Campbell | |
| 2017-08-10 | Experimental removal of existentials | Brian Campbell | |
| 2017-08-10 | Improved existentials and type synonyms | Alasdair Armstrong | |
| 2017-08-09 | Pretty-print some more type annotations | Thomas Bauereiss | |
| 2017-08-08 | Add infrastructure to play with new menhir parsers. | Alasdair Armstrong | |
| Added a copy of the current parser/lexer in parser2.mly and lexer2.mll. They can be used with the -new_parser flag. Currently they are just copies of the existing files. | |||
| 2017-08-08 | Switch to using menhir for sail parser in experiments branch | Alasdair Armstrong | |
| 2017-08-08 | Fix Lem bindings in test cases | Thomas Bauereiss | |
| Add a test case with the MIPS spec using the TLB stub. Use the sequential monad for Lem testing for now; the free monad (in "prompt.lem") has not been updated for machine words yet. | |||
| 2017-08-08 | Glue together Sail prelude and Lem library | Thomas Bauereiss | |
| 2017-08-08 | Various fixes and improvements for the Lem pretty-printing | Thomas Bauereiss | |
| - Add some missing "wreg" effect annotations in the type checker - Improve pretty-printing of register type definitions: In addition to a "build" function, output an actual type definition, and some getter/setter functions for register fields - Fix a bug in sizeof rewriting that caused it to fail when rewriting nested calls of functions that contained sizeof expressions - Fix pretty-printing of user-defined union types with type variables (cf. test case option_either.sail) - Simplify nexps, e.g. "(8 * 8) - 1" becomes "63", in order to be able to output more type annotations with bitvector lengths - Add (back) some support for specifying Lem bindings in val specs using "val extern ... foo = bar" - Misc bug fixes | |||
| 2017-08-08 | Add add_typ_var to mli file | Alastair Reid | |
| This function is used by asl_to_sail2.ml | |||
| 2017-08-07 | Improvements to existentials for ASL parser | Alasdair Armstrong | |
| 2017-08-07 | Fixed pretty printing of E_cons | Alasdair Armstrong | |
| 2017-08-07 | Fixed various issues regarding typechecking lists. | Alasdair Armstrong | |
| 2017-08-04 | Various improvements for ASL generation | Alasdair Armstrong | |
| Fixed a bug where existential constraint's weren't used to solve function quantifiers correctly | |||
| 2017-08-02 | Improve pretty-printing of register declaration and assignment | Thomas Bauereiss | |
| 2017-08-02 | Changed some aspects of the typechecker to better support ASL l-values | Alasdair Armstrong | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |