summaryrefslogtreecommitdiff
path: root/src/monomorphise.ml
AgeCommit message (Collapse)Author
2018-04-12Fill in some minor missing cases in monomorphisationBrian Campbell
2018-04-11Use more robust method of finding deps of new tyvars in mono analysisBrian Campbell
2018-04-11Make the atom to singleton type rewriter replace literals with guardsBrian Campbell
(previously the typechecker did this for all literal patterns, but now it's only necessary for the rewritten arguments)
2018-04-10Avoid rejecting reasonable pattern matches in monomorphisationBrian Campbell
(when they're not relevant)
2018-04-10Add basic reference support to monomorphisationBrian Campbell
2018-04-09Remove unnecessary restriction on complex nexp rewritingBrian Campbell
2018-04-09Stop vector_typ_args_of from failing when order is a variableBrian Campbell
Now it just returns the actual arguments and a separate function calculates the start index when required.
2018-04-06Generate better tyvar names for complex nexps in monomorphisationBrian Campbell
2018-04-04Use solver properly to simplify nexps in mono analysis, Lem printingBrian Campbell
Turn on complex nexp rewriting for mono by default (NB: solving is currently quite slow, will optimise)
2018-04-04Instantiate type properly when introducing mono castsBrian Campbell
(also reorder the phases a little)
2018-04-04Use valspec equations in monomorphisation analysisBrian Campbell
2018-04-04Add bitvector casts to funcl bodies when necessaryBrian Campbell
2018-04-04Initial rewrite to move complex nexps in fn sigs into constraintsBrian 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-04Improve location information in mono dependency errorsBrian Campbell
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-12 21:11:58 +0000