summaryrefslogtreecommitdiff
path: root/src/monomorphise.ml
AgeCommit message (Collapse)Author
2018-03-14Remove 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-13Add test for mutual recursion and monomorphisationBrian Campbell
2018-03-13Support a few more set constraints in monoBrian Campbell
2018-03-07Make union types consistent in the ASTAlasdair 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-27Make constant propagation of slicing more generalBrian Campbell
2018-02-22Curtail at more false assertionsBrian Campbell
(plus some adjustments for the test case)
2018-02-21Implement more builtins in constant propagationBrian Campbell
2018-02-21Cut out dead if branches according to the type environment during monoBrian 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-20Remove temporary debugging messageBrian Campbell
2018-02-20Bump up case split limit for nowBrian Campbell
2018-02-20Rework atom-to-itself transformation to check for equivalent size nexpsBrian Campbell
2018-02-14Another mono rewrite for aarch64Brian Campbell
2018-02-14Support monorphisation analysis of bitvectors inside existentialsBrian Campbell
2018-02-14Pick up more equivalent type variables in monomorphisationBrian Campbell
2018-02-14Handle simple returns in constant propagationBrian Campbell
Useful for feature functions, e.g. HaveFP16Ext
2018-02-13Some support in mono for extra fresh tyvars generated in the typecheckerBrian Campbell
(still some work to do in AtomToItself rewrite, but should work despite error messages)
2018-02-08Add (most of) the bitvector cast insertion transformationBrian 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-06Add aux constructor to type patterns for consistencyAlasdair Armstrong
2018-02-05Merge changes to type_check.mlAlasdair Armstrong
2018-02-05Add typ patterns for destructuring existentialsAlasdair Armstrong
2018-02-02When cutting functions short at assertions, put an exit to correct typesBrian Campbell
if necessary
2018-02-02Also rewrite boolean terms in asserts during monomorphisationBrian Campbell
(otherwise wildcard cases won't be cut short at the assertion)
2018-02-01Fix atom -> itself transformation when clauses feature different set of sizesBrian Campbell
2018-02-01Curtail function bodies at known-false assertions during monoBrian Campbell
(preventing non-monomorphised sizes appearing in wildcard cases)
2018-02-01Proper substitution and propagation of size from last commitBrian Campbell
2018-02-01Substitute extra size case splits into body in monomorphisationBrian Campbell
2018-02-01Make mono add case expressions for size tyvars without a corresponding argBrian Campbell
2018-01-31Find buried set constraints in assertsBrian Campbell
2018-01-31Fix mono continue away optionBrian Campbell
2018-01-30Handle 'N == 1 | 'N == 2 | ... style set constraints in monoBrian Campbell
2018-01-30Optionally give *all* monomorphisation errors at onceBrian Campbell
(and stop afterwards unless asked)
2018-01-30Fix monomorphisation analysis to detect type variables which need to beBrian Campbell
concrete but aren't determined by one of the arguments.
2018-01-29Set maximum split size to work with aarch64 no vectorBrian Campbell
2018-01-29Turn off constraint substitution in monoBrian Campbell
(Type checker doesn't seem to use false aggressively enough for this)
2018-01-29Turn off warnings when rechecking after monoBrian Campbell
2018-01-29Avoid generating (_ as n) in mono, broke atom type rewritingBrian Campbell
2018-01-26One more mono rewriteBrian Campbell
2018-01-26Add replacement of complex nexp sizes by equivalent variables in monoBrian Campbell
2018-01-26Preserve more typing info in monomorphisation for later stagesBrian Campbell
2018-01-25Use set asserts as case splits in monomorphisationBrian Campbell
2018-01-25Missing type expansionBrian Campbell
2018-01-25Handle bound variables properly with precise case splittingBrian Campbell
2018-01-25Basic support for match x[5 .. 2] with case splitsBrian Campbell
2018-01-25Implement basic case splitting based on found case expressionsBrian Campbell
(makes some of the monomorphisation case splits smaller)
2018-01-19Update monomorphisation for sail2Brian Campbell
(no vector type start position, comment syntax)
2018-01-18Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-16Fix problem with let-bindings in pattern guardsThomas Bauereiss
Monomorphisation sometimes produces pattern guard with let-bindings, e.g. | ... if (let regsize = size_itself(regsize) in eq(regsize, 32)) -> ... Previously, the rewriting pass for let-bindings (and pattern guards) pulled these out of the guard condition and into the same scope as the case expression, which potentially clashed with let-bindings for the same variables in that case expression. The rewriter now leaves let-bindings in place within pure if-conditions, solving this problem.
2018-01-16Handle for loops correctly when rewriting size parametersBrian Campbell
2018-01-16Another useful monomorphisation rewriteBrian Campbell
2018-01-15Check monomorphisation case split size once for each patternBrian Campbell
(rather than for each argument separately)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-15 15:47:23 +0000