Hrutvik Kanabar
Hrutvik Kanabar
This issue is about implementing a version of `Q.REFINE_EXISTS_TAC` called `qrefinel : term quotation list -> tactic`, which: - Attempts to refine a goal consisting of nested top-level existentials with...
It is not uncommon to have a theory file which proves a single, relatively clean theorem - but the purpose of the file is cluttered by various intermediate definition and...
Allow users to disable generation, mutation, and/or minimisation of syscalls. Using these options correctly should prevent `syzkaller` wasting time generating/mutating/minimising syscalls for which it is unlikely to make much progress....
Add an `Annot` form to `cexp` as follows: ``` annot = Inline mlstring | ... cexp = ... | Annot annot cexp ``` This should desugar as follows: `exp_of (Annot...
Extend the parser to cope with Haskell-line inlining annotations. We should mirror the syntax described [here](https://wiki.haskell.org/Inlining_and_Specialisation) as much as possible.
The inliner should act on user annotations specifying inlining locations.
Augment inlining relation to handle `letrec`s in memory, and inline them by unrolling loops.
Currently `Case` desugars to a series of nested `let` expressions, e.g.: ``` exp_of (case x = e of C a b c -> k) => let x = exp_of e...
**Define TypeClassLang, a new source language with type classes.** TypeClassLang should have both typed and untyped variants - i.e. it can be in either "mode". This could be implemented by...
**Redirect parsing to target TypeClassLang** Aside from PureLang's existing constructs, this will need to handle: - `class` and `instance` declarations - contexts/type class constraints in types - TypeClassLang's new top-level...