Super hacky hint database for Idris.

Hints.idr

||| Hacky and rudimentary hint database for Idris using elaborator reflection.
||| You can now write tactics that does `getHints`
||| and try to prove the goal with the lemmas there.
module Hints
import Language.Reflection.Utils
%language ElabReflection
%access public export

||| The hint to pass the machine generated names. Note that the word hint here
||| is used literally, not in the theorem prover sense.
mnString : String
mnString = "hint"

||| The number from which we can creating machine generated variables.
startNumber : Int
startNumber = 0

||| Learn the number of the last hint, if it exists at all.
learnLastHint : Elab (Maybe Int)
learnLastHint = up startNumber
  where up : Int -> Elab (Maybe Int)
        up i = (do lookupTyExact (MN i mnString) ; up (i + 1))
          <|> pure (if i == startNumber then Nothing else Just (i - 1))

||| Adds the given name to the hint database.
newHint : TTName -> Elab ()
newHint n = do
  let new = MN (fromMaybe startNumber ((+ 1) <$> !learnLastHint)) mnString
  declareType (Declare new [] (Var `{TTName}))
  defineFunction (DefineFun new [MkFunClause (Var new) (quote n)])

reifyString : TT -> Elab String
reifyString (TConst (Str s)) = pure s
reifyString t = fail [ TextPart "Failed to reify", TermPart t
                     , TextPart "as a" , NamePart `{{String}}]

reifyInt : TT -> Elab Int
reifyInt (TConst (BI i)) = pure (fromInteger i)
reifyInt t = fail [ TextPart "Failed to reify", TermPart t
                  , TextPart "as a" , NamePart `{{Int}}]

reifyStringList : TT -> Elab (List String)
reifyStringList `([] : List String) = pure []
reifyStringList `(~x :: ~xs : List String) =
  (::) <$> reifyString x <*> reifyStringList xs
reifyStringList t = fail [ TextPart "Failed to reify", TermPart t
                         , TextPart "as a"
                         , NamePart `{List}, NamePart `{{String}}]

reifyTTName : TT -> Elab TTName
reifyTTName `(UN ~x) = UN <$> reifyString x
reifyTTName `(NS ~n ~xs) = NS <$> reifyTTName n <*> reifyStringList xs
reifyTTName `(MN ~i ~s) = MN <$> reifyInt i <*> reifyString s
reifyTTName t = fail [ TextPart "Failed to reify", TermPart t
                     , TextPart "as a", NamePart `{TTName}]

reifyHint : Int -> Elab TTName
reifyHint i = do
    DefineFun _ [MkFunClause _ t] <- lookupFunDefnExact (MN i mnString)
    reifyTTName t

||| The `Elab` action to get the names of all the hints.
getHints : Elab (List TTName)
getHints = maybe (pure []) go !learnLastHint
  where go : Int -> Elab (List TTName)
        go i = if i < startNumber then pure []
                                  else (::) <$> reifyHint i <*> go (i - 1)

-- Defining Coq-style syntax for hints.
decl syntax "hint" {n} = %runElab (newHint `{n})

-- TIME TO SEE IT IN ACTION!!!

-- Let's declare some hints
hint lteRefl
hint lteSuccRight
hint lteSuccLeft

main : IO ()
main = putStrLn (%runElab (do fill (quote (show !getHints)); solve))

{-
Prints this when run (modulo styling):
[NS (UN "lteSuccLeft") ["Nat", "Prelude"],
 NS (UN "lteSuccRight") ["Nat", "Prelude"],
 NS (UN "lteRefl") ["Nat", "Prelude"]]
-}