| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-07 | Fix a small bug in monomorphisation | Thomas Bauereiss | |
| 2018-06-06 | Some work on improving error messages | Alasdair Armstrong | |
| We now store the location where type variables were bound, so we can use this information when printing error messages. Factor type errors out into type_error.ml. This means that Type_check.check is now Type_error.check, as it previously it handled wrapping the type_errors into reporting_basic errors. Type_check.check' has therefore been renamed to Type_check.check. | |||
| 2018-05-22 | Fix one part of cast introduction, leave another for later | Brian Campbell | |
| 2018-05-11 | More builtin names in constant propagation | Brian Campbell | |
| 2018-05-11 | Actually use the correct type for singleton rewriting this time | Brian Campbell | |
| 2018-05-11 | Be much more careful to introduce the right bitvector casts to the right sizes | Brian Campbell | |
| 2018-05-11 | Handle automatic existential unpacking in function application in mono analysis | Brian Campbell | |
| 2018-05-11 | Use type from funcl in singleton rewriting | Brian Campbell | |
| The pattern types may be subtypes, using those caused it to try rewriting int parameters and failing | |||
| 2018-05-04 | Add support for top-level values to monomorphisation singleton rewrite | Brian Campbell | |
| 2018-05-04 | Fix mono cast introduction to avoid a checking to inference change | Brian Campbell | |
| Adds return type to pattern so that the original function body is still type checked, rather than switching to type inference which may fail. | |||
| 2018-05-04 | Start updating monomorphisation | Brian Campbell | |
| + add additional lexp + update aarch64 mono demo source - still needs support for tyvars from assignments in dependency analysis | |||
| 2018-04-20 | Have sign_extend in common Sail Lem library, use it and zero_extend in | Brian Campbell | |
| mono rewrites | |||
| 2018-04-19 | Gloss over UInt/unsigned name difference in monomorphisation | Brian Campbell | |
| 2018-04-18 | Rename BK_nat to BK_int to be consistent with source syntax | Alasdair Armstrong | |
| 2018-04-17 | Fix slicing in constant propagation | Brian Campbell | |
| 2018-04-12 | Fill in some minor missing cases in monomorphisation | Brian Campbell | |
| 2018-04-11 | Use more robust method of finding deps of new tyvars in mono analysis | Brian Campbell | |
| 2018-04-11 | Make the atom to singleton type rewriter replace literals with guards | Brian Campbell | |
| (previously the typechecker did this for all literal patterns, but now it's only necessary for the rewritten arguments) | |||
| 2018-04-10 | Avoid rejecting reasonable pattern matches in monomorphisation | Brian Campbell | |
| (when they're not relevant) | |||
| 2018-04-10 | Add basic reference support to monomorphisation | Brian Campbell | |
| 2018-04-09 | Remove unnecessary restriction on complex nexp rewriting | Brian Campbell | |
| 2018-04-09 | Stop vector_typ_args_of from failing when order is a variable | Brian Campbell | |
| Now it just returns the actual arguments and a separate function calculates the start index when required. | |||
| 2018-04-06 | Generate better tyvar names for complex nexps in monomorphisation | Brian Campbell | |
| 2018-04-04 | Use solver properly to simplify nexps in mono analysis, Lem printing | Brian Campbell | |
| Turn on complex nexp rewriting for mono by default (NB: solving is currently quite slow, will optimise) | |||
| 2018-04-04 | Instantiate type properly when introducing mono casts | Brian Campbell | |
| (also reorder the phases a little) | |||
| 2018-04-04 | Use valspec equations in monomorphisation analysis | Brian Campbell | |
| 2018-04-04 | Add bitvector casts to funcl bodies when necessary | Brian Campbell | |
| 2018-04-04 | Initial rewrite to move complex nexps in fn sigs into constraints | Brian Campbell | |
| (for monomorphisation, off for now because the analysis needs extended). Also tighten up orig_nexp, make Lem backend replace # in type variables. | |||
| 2018-04-04 | Improve location information in mono dependency errors | Brian Campbell | |
| 2018-03-14 | Remove unnecessary size_itself_int uses in guards (for Lem) | Brian Campbell | |
| Doesn't remove them from function bodies because that can produce more work for the sizeof rewriting. | |||
| 2018-03-13 | Add test for mutual recursion and monomorphisation | Brian Campbell | |
| 2018-03-13 | Support a few more set constraints in mono | Brian Campbell | |
| 2018-03-07 | Make union types consistent in the AST | Alasdair Armstrong | |
| Previously union types could have no-argument constructors, for example the option type was previously: union option ('a : Type) = { Some : 'a, None } Now every union constructor must have a type, so option becomes: union option ('a : Type) = { Some : 'a, None : unit } The reason for this is because previously these two different types of constructors where very different in the AST, constructors with arguments were used the E_app AST node, and no-argument constructors used the E_id node. This was particularly awkward, because it meant that E_id nodes could have polymorphic types, i.e. every E_id node that was also a union constructor had to be annotated with a type quantifier, in constrast with all other identifiers that have unquantified types. This became an issue when monomorphising types, because the machinery for figuring out function instantiations can't be applied to identifier nodes. The same story occurs in patterns, where previously unions were split across P_id and P_app nodes - now the P_app node alone is used solely for unions. This is a breaking change because it changes the syntax for union constructors - where as previously option was matched as: function is_none opt = match opt { Some(_) => false, None => true } it is now matched as function is_none opt = match opt { Some(_) => false, None() => true } note that constructor() is syntactic sugar for constructor(()), i.e. a one argument constructor with unit as it's value. This is exactly the same as for functions where a unit-function can be called as f() and not as f(()). (This commit also makes exit() work consistently in the same way) An attempt to pattern match a variable with the same name as a union-constructor now gives an error as a way to guard against mistakes made because of this change. There is probably an argument for supporting the old syntax via some syntactic sugar, as it is slightly prettier that way, but for now I have chosen to keep the implementation as simple as possible. The RISCV spec, ARM spec, and tests have been updated to account for this change. Furthermore the option type can now be included from $SAIL_DIR/lib/ using $include <option.sail> | |||
| 2018-02-27 | Make constant propagation of slicing more general | Brian Campbell | |
| 2018-02-22 | Curtail at more false assertions | Brian Campbell | |
| (plus some adjustments for the test case) | |||
| 2018-02-21 | Implement more builtins in constant propagation | Brian Campbell | |
| 2018-02-21 | Cut out dead if branches according to the type environment during mono | Brian Campbell | |
| const progagation. Needed to avoid negative bitvector sizes on aarch64 Also propagate values found from "if var = const ...", which is needed in aarch64 | |||
| 2018-02-20 | Remove temporary debugging message | Brian Campbell | |
| 2018-02-20 | Bump up case split limit for now | Brian Campbell | |
| 2018-02-20 | Rework atom-to-itself transformation to check for equivalent size nexps | Brian Campbell | |
| 2018-02-14 | Another mono rewrite for aarch64 | Brian Campbell | |
| 2018-02-14 | Support monorphisation analysis of bitvectors inside existentials | Brian Campbell | |
| 2018-02-14 | Pick up more equivalent type variables in monomorphisation | Brian Campbell | |
| 2018-02-14 | Handle simple returns in constant propagation | Brian Campbell | |
| Useful for feature functions, e.g. HaveFP16Ext | |||
| 2018-02-13 | Some support in mono for extra fresh tyvars generated in the typechecker | Brian Campbell | |
| (still some work to do in AtomToItself rewrite, but should work despite error messages) | |||
| 2018-02-08 | Add (most of) the bitvector cast insertion transformation | Brian Campbell | |
| to help Lem go from a general type `bits('n)` to a specific type `bits(16)` at a case split, and the other way around for a returned value. Doesn't handle function clause patterns yet | |||
| 2018-02-06 | Add aux constructor to type patterns for consistency | Alasdair Armstrong | |
| 2018-02-05 | Merge changes to type_check.ml | Alasdair Armstrong | |
| 2018-02-05 | Add typ patterns for destructuring existentials | Alasdair Armstrong | |
| 2018-02-02 | When cutting functions short at assertions, put an exit to correct types | Brian Campbell | |
| if necessary | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |