summaryrefslogtreecommitdiff
path: root/src/monomorphise.ml
AgeCommit message (Collapse)Author
2018-01-02Experimenting with power specAlasdair Armstrong
2017-12-14Merge remote-tracking branch 'origin/experiments' into interactiveAlasdair Armstrong
2017-12-13Use big_nums from LemAlasdair Armstrong
2017-12-12Make mono analysis fail properly on effectful functionsBrian Campbell
2017-12-11Remove some duplication from monomorphisation analysis failure reportsBrian Campbell
2017-12-07Support monomorphisation with set constrained integersBrian Campbell
Also, to support this, constant propagation for integer multiply, fix substitution of concrete values for nvars, size parameters in single argument functions, fix kind for itself, add eq_atom to prelude
2017-12-06Remove filename mangling in monomorphisationBrian Campbell
Broke analysis a little
2017-12-06Add top-level pattern match guards internallyBrian Campbell
Also fix bug in mono analysis with generated variables Breaks lots of typechecking tests because it generates unnecessary equality tests on units (and the tests don't have generic equality), which I'll fix next.
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-11-27Replace bad generic comparisons in monoBrian Campbell
2017-11-27Case splitting on boolsBrian Campbell
(mostly to make test cases easier)
2017-11-24Use unbound precision big_ints throughout sail.Alasdair Armstrong
Alastair's test cases revealed that using regular ints causes issues throughout sail, where all kinds of things can internally overflow in edge cases. This either causes crashes (e.g. int_of_string fails for big ints) or bizarre inexplicable behaviour. This patch switches the sail AST to use big_int rather than int, and updates everything accordingly. This touches everything and there may be bugs where I mistranslated things, and also n = m will still typecheck with big_ints but fail at runtime (ocaml seems to have decided that static typing is unnecessary for equality...), as it needs to be changed to eq_big_int. I also got rid of the old unused ocaml backend while I was updating things, so as to not have to fix it.
2017-11-21Merge Thomas' suggested changesBrian Campbell
Use overloading to find eq/neq Track range/atom split Missing type expansion
2017-11-20Tidy last upBrian Campbell
2017-11-20Constant propagation in guardsBrian Campbell
2017-11-20Basic handling of recursive calls in monomorphisation analysisBrian Campbell
2017-11-20Look up the right type variables in monomorphisation analysisBrian Campbell
2017-11-20Support new nexp in monoBrian Campbell
2017-11-16Remove unused Typ_wild constructorAlasdair Armstrong
2017-11-15Report all monomorphisation problemsBrian Campbell
2017-11-15For loops bind a type variableBrian Campbell
2017-11-15Remove untested infix monomorphisation (removed by type checker)Brian Campbell
2017-11-15Tidy up in monomorphisationBrian Campbell
2017-11-14During monomorphisation always refine constructors,Brian Campbell
not just when there's been a case split
2017-11-14Fix existential union typing problem in monomorphisationBrian Campbell
2017-11-14Remove some obsolete codeBrian Campbell
2017-11-14Automatic analysis for monomorphisationBrian Campbell
2017-11-02Merge branch 'experiments'Thomas Bauereiss
2017-11-02Fix a few AST and parsing-related bugsThomas Bauereiss
2017-11-02Handle "undefined" type-level sizes in monomorphisationBrian Campbell
2017-11-01Support bitvector-size-parametric functions in Lem outputBrian Campbell
Translates atom('n) types into itself('n) types that won't be erased Also exports more rewriting functions
2017-10-25List.cons is too newBrian Campbell
2017-10-18Merge branch 'experiments' of Peter_Sewell/sail into mono-experimentsBrian Campbell
(and fix up monomorphisation)
2017-10-13Handle bitvector_access in constant propagationBrian Campbell
2017-10-06Fix constant propagation on multi-argument functionsBrian Campbell
2017-10-02Make undefined constant propagation stop at ex_intBrian Campbell
2017-09-28Use (K)Bindings from ast_util rather than making new onesBrian Campbell
2017-09-28Add loops to monomorphisationBrian Campbell
2017-09-28Refine constructors during monomorphisationBrian Campbell
2017-09-26Remove obsolete existential removal codeBrian Campbell
2017-09-26Remove debugging statements included accidentallyBrian Campbell
2017-09-26Add propagation of local assignments to monomorphisationBrian Campbell
2017-09-21Change NC_fixed to NC_equal to match NC_not_equalAlasdair Armstrong
also rename NC_nat_set_bounded to NC_set (it was an int set not a nat set anyway)
2017-09-21Simplify AST by removing LB_val_explicit and replace LB_val_implicit with ↵Alasdair Armstrong
just LB_val in AST also rename functions in rewriter.ml appropriately.
2017-09-21Cleaning up the AST and removing redundant and/or unused nodesAlasdair Armstrong
2017-09-21Support more functions and vector construction in mono for hexapodBrian Campbell
2017-09-21Substitute into constraints to make assert work with monoBrian Campbell
2017-09-21Disable existential removal for nowBrian Campbell
2017-09-20Handle let (exists 't...[:'t:]) 't = lit in monoBrian Campbell
2017-09-20Remove obsolete nexp refinementBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:08:52 +0000