tactic-haskell
tactic-haskell copied to clipboard
TOTBWF
Tactic Metaprogramming in Haskell
Template Haskell is a bit limiting, so I'm going to migrate to GHC API.
As it stands, quite a bit of the work involved in implementing new features is mucking around with odd TemplateHaskell representations. Using [th-desugar](https://hackage.haskell.org/package/th-desugar-1.9) could really cut down on a lot...
This has quite a few benefits. 1) We can have a custom quasi-quoter, which helps us both from an ergonomics and tooling perspective. This would enable the syntax: `tactic [thm|...
For example `apply '(+)` yields the error: ``` Tactic Error: lookupVarType: Variable Type ClassOpI GHC.Num.+ (ForallT [KindedTV a_6989586621679035072 StarT] [AppT (ConT GHC.Num.Num) (VarT a_6989586621679035072)] (AppT (AppT ArrowT (VarT a_6989586621679035072)) (AppT...
Sometimes, it helps to be able to label the subgoals, especially when handling inductive types like `Bool`. Implementation-wise, this is as easy as adding a `Maybe String` field to `Judgement`,...
Right now the code for freshening hypothesis names doesn't take into account cases where someone freshens something that ends in a number. This could cause name overlap, but is of...