totbwf / tactic-haskell Goto Github PK

induction is the last "major" tactic I would like to have done before writing a bit about this.
The general mechanism should be:

1. Use reify to find the type info
2. Generate goals for each of the constructors.

However, there may be some complications. For example, should I do a positivity check?

As it stands, quite a bit of the work involved in implementing new features is mucking around with odd TemplateHaskell representations. Using th-desugar could really cut down on a lot of the work required.

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 (AppT ArrowT (VarT 
a_6989586621679035072)) (VarT a_6989586621679035072)))) GHC.Num.Num isn't implemented yet

Solving this could be a bit tricky, as we would need to work in an understanding of typeclass instances into things...

Take this example:

data List a = Nil | Cons a (List a)
  deriving (Show)

tactic "sum'" [t| List Int -> Int |] $ do
  intro "x"
  induction "x"

Gives the error:

    Tactic Error: Unsolved Subgoals
              ===============
              GHC.Types.Int

              ind :: a_0
              ind1 :: GHC.Types.Int
              ===============
              GHC.Types.Int

The issue here is that ind :: a_0 is not unifying with Int.

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, and modifying
? and UnsolvedGoals to properly print these labels.

As an aside, the printing of ? and UnsolvedGoals could probably be unified in some way.

First, a quick example of the problem:

printTac :: String -> Tactic Judgement ()
printTac s = Tactic $ \j -> (T $ reportWarning s) >> return (pure ((), j))

tactic "pair1" [t| forall a b. a -> b -> (a,b) |] $ do
  forall
  intros_
  (split >> printTac "a") >> printTac "b"
  assumption


tactic "pair2" [t| forall a b. a -> b -> (a,b) |] $ do
  forall
  intros_
  split >> (printTac "a" >> printTac "b")
  assumption

Running the 1st tactic will print out "aabb", and running the 2nd will print out "abab".

The core of this issue is that ProofState is not a monad transformer. I'm not sure exactly how to fix this at this point.

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| foo :: a -> b -> (a, b) |] $ do ..., as well as allow us to (potentially) use tactic-haskell as an editor tool.

2. New types. This would open the door for actual dependent types, which would be a huge win. I'm not sure about the exact specifics of what the desugaring would look like in a few cases, but we could always limit the tricky bits to be only usable within the context of tactics.

This should be pretty straightforward. However, it may be about time to figure out a good strategy for implementing the regular and hypothesis searching versions of each tactic.

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 low priority, as it would be a pretty silly thing to do.