Search.Auto


   0 | ||| The content of this module is based on the paper
   1 | ||| Auto in Agda - Programming proof search using reflection
   2 | ||| by Wen Kokke and Wouter Swierstra
   3 | 
   4 | module Search.Auto
   5 | 
   6 | import Language.Reflection.TTImp
   7 | import Language.Reflection
   8 | 
   9 | import Data.DPair
  10 | import Data.Fin
  11 | import Data.Maybe
  12 | import Data.Nat
  13 | import Data.SnocList
  14 | import Data.String
  15 | import Data.Vect
  16 | 
  17 | import Syntax.PreorderReasoning
  18 | 
  19 | %default total
  20 | 
  21 | %language ElabReflection
  22 | 
  23 | ------------------------------------------------------------------------------
  24 | -- Basics of reflection
  25 | ------------------------------------------------------------------------------
  26 | 
  27 | ------------------------------------------------------------------------------
  28 | -- Quoting: Id term
  29 | 
  30 | idTerm : TTImp
  31 | idTerm = `( (\ x => x) )
  32 | 
  33 | idTermTest : Auto.idTerm === let x : Name; x = UN (Basic "x") in
  34 |                              ILam ? MW ExplicitArg (Just x) ? (IVar ? x)
  35 | idTermTest = Refl
  36 | 
  37 | ------------------------------------------------------------------------------
  38 | -- Unquoting: const function
  39 | 
  40 | iLam : Maybe UserName -> TTImp -> TTImp -> TTImp
  41 | iLam x a sc = ILam EmptyFC MW ExplicitArg (UN <$> x) a sc
  42 | 
  43 | iVar : UserName -> TTImp
  44 | iVar x = IVar EmptyFC (UN x)
  45 | 
  46 | const : a -> b -> a
  47 | const = %runElab
  48 |       (check
  49 |       $ iLam (Just (Basic "v")) `(a)
  50 |       $ iLam Nothing            `(b)
  51 |       $ iVar (Basic "v"))
  52 | 
  53 | constTest : Auto.const 1 2 === 1
  54 | constTest = Refl
  55 | 
  56 | ------------------------------------------------------------------------------
  57 | -- Section 2: Motivation
  58 | ------------------------------------------------------------------------------
  59 | 
  60 | ------------------------------------------------------------------------------
  61 | -- Goal inspection: building tuples of default values
  62 | 
  63 | getPoint : Elab a
  64 | getPoint = do
  65 |   let err = fail "No clue what to do"
  66 |   Just g <- goal
  67 |     | Nothing => err
  68 |   let mval = buildValue g
  69 |   maybe err check mval
  70 | 
  71 |   where
  72 | 
  73 |     buildValue : TTImp -> Maybe TTImp
  74 |     buildValue g = do
  75 |       let qNat   : List ? = [`{Nat}, `{Prelude.Nat}, `{Prelude.Types.Nat}]
  76 |       let qBool  : List ? = [`{Bool}, `{Prelude.Bool}, `{Prelude.Basics.Bool}]
  77 |       let qList  : List ? = [`{List}, `{Prelude.List}, `{Prelude.Basics.List}]
  78 |       let qMaybe : List ? = [`{Maybe}, `{Prelude.Maybe}, `{Prelude.Types.Maybe}]
  79 |       let qPair  : List ? = [`{Pair}, `{Builtin.Pair}]
  80 |       case g of
  81 |         IVar _ n =>
  82 |           ifThenElse (n `elem` qNat)  (Just `(0)) $
  83 |           ifThenElse (n `elem` qBool) (Just `(False))
  84 |           Nothing
  85 |         IApp _ (IVar _ p) q =>
  86 |           ifThenElse (p `elem` qMaybe)
  87 |             (case buildValue q of
  88 |               Nothing => pure `(Nothing)
  89 |               Just qv => pure `(Just ~(qv)))
  90 |           $ ifThenElse (p `elem` qList)
  91 |             (case buildValue q of
  92 |               Nothing => pure `([])
  93 |               Just qv => pure `([~(qv)]))
  94 |           $ Nothing
  95 |         IApp _ (IApp _ (IVar _ p) q) r =>
  96 |           ifThenElse (not (p `elem` qPair)) Nothing $ do
  97 |             qv <- buildValue q
  98 |             rv <- buildValue r
  99 |             pure `(MkPair ~(qv) ~(rv))
 100 |         _ => Nothing
 101 | 
 102 | getAPoint : (List Nat, (Bool, (Maybe (List Void, Bool, Nat))), Nat)
 103 | getAPoint = %runElab getPoint
 104 | 
 105 | getPointTest : Auto.getAPoint === ([0], (False, Just ([], False, 0)), 0)
 106 | getPointTest = Refl
 107 | 
 108 | ------------------------------------------------------------------------------
 109 | -- Proof automation: Even
 110 | 
 111 | data Even : Nat -> Type where
 112 |   EvenZ : Even Z
 113 |   EvenS : Even n -> Even (S (S n))
 114 | 
 115 | EvenPlus : {0 m, n : Nat} -> Even m -> Even n -> Even (m + n)
 116 | EvenPlus EvenZ      en = en
 117 | EvenPlus (EvenS em) en = EvenS (EvenPlus em en)
 118 | 
 119 | trivial : Even n -> Even (n + 2)
 120 | trivial en = EvenPlus en (EvenS EvenZ)
 121 | 
 122 | ||| This is called Naïve because that's not the actual implementation, it just
 123 | ||| looks like this in the paper's Motivation
 124 | namespace Naïve
 125 | 
 126 |   HintDB : Type
 127 |   HintDB = SnocList Name
 128 | 
 129 |   hints : HintDB
 130 |   hints = [< `{EvenZ}, `{EvenS}, `{EvenPlus}]
 131 | 
 132 | ------------------------------------------------------------------------------
 133 | -- Section 3: Proof search
 134 | ------------------------------------------------------------------------------
 135 | 
 136 | namespace RuleName
 137 | 
 138 |   public export
 139 |   data RuleName : Type where
 140 |     Free  : Name -> RuleName
 141 |     Bound : Nat -> RuleName
 142 | 
 143 |   export
 144 |   toName : RuleName -> Name
 145 |   toName (Free nm) = nm
 146 |   toName (Bound n) = DN (pack $ display n)
 147 |                    $ MN "bound_variable_auto_search" (cast n)
 148 | 
 149 |     where
 150 |     display : Nat -> List Char
 151 |     display n =
 152 |       let (p, q) = divmodNatNZ n 26 ItIsSucc in
 153 |       cast (q + cast 'a') :: if p == 0 then [] else display (assert_smaller n (pred p))
 154 | 
 155 | 
 156 | export
 157 | Show RuleName where
 158 |   show (Free nm) = "Free \{show nm}"
 159 |   show (Bound n) = "Bound \{show n}"
 160 |   -- show . toName
 161 | 
 162 | namespace TermName
 163 | 
 164 |   public export
 165 |   data TermName : Type where
 166 |     UName : Name -> TermName
 167 |     Bound : Nat -> TermName
 168 |     Arrow : TermName
 169 | 
 170 | export
 171 | Eq TermName where
 172 |   UName n1 == UName n2 = n1 == n2
 173 |   Bound n1 == Bound n2 = n1 == n2
 174 |   Arrow == Arrow = True
 175 |   _ == _ = False
 176 | 
 177 | ||| Proof search terms
 178 | public export
 179 | data Tm : Nat -> Type where
 180 |   Var : Fin n -> Tm n
 181 |   Con : TermName -> List (Tm n) -> Tm n
 182 | 
 183 | export
 184 | showTerm : (ns : SnocList Name) -> Tm (length ns) -> String
 185 | showTerm ns = go Open where
 186 | 
 187 |   goVar : (ns : SnocList Name) -> Fin (length ns) -> String
 188 |   goVar (_ :< n) FZ = show n
 189 |   goVar (ns :< _) (FS k) = goVar ns k
 190 | 
 191 |   go : Prec -> Tm (length ns) -> String
 192 |   go d (Var k) = goVar ns k
 193 |   go d (Con (UName n) []) = show n -- (dropNS n)
 194 |   go d (Con Arrow [a,b])
 195 |     = showParens (d > Open) $
 196 |         unwords [ go App a, "->", go Open b ]
 197 |   go d (Con (UName n) [a,b])
 198 |     = showParens (d > Open) $
 199 |         -- let n = dropNS n in
 200 |         if isOp n then unwords [ go App a, show n, go Open b ]
 201 |         else unwords [ show n, go App a, go App b ]
 202 |   go d (Con (UName n) ts)
 203 |     = showParens (d > Open) $
 204 |         unwords (show n :: assert_total (map (go App) ts))
 205 |   go _ _ = ""
 206 | 
 207 | public export
 208 | Env : (Nat -> Type) -> Nat -> Nat -> Type
 209 | Env t m n = Fin m -> t n
 210 | 
 211 | export
 212 | rename : Env Fin m n -> Tm m -> Tm n
 213 | rename rho (Var x) = Var (rho x)
 214 | rename rho (Con f xs) = Con f (assert_total $ map (rename rho) xs)
 215 | 
 216 | export
 217 | subst : Env Tm m n -> Tm m -> Tm n
 218 | subst rho (Var x) = rho x
 219 | subst rho (Con f xs) = Con f (assert_total $ map (subst rho) xs)
 220 | 
 221 | export
 222 | split : Tm m -> (List (Tm m), Tm m)
 223 | split = go [<] where
 224 | 
 225 |   go : SnocList (Tm m) -> Tm m -> (List (Tm m), Tm m)
 226 |   go acc (Con Arrow [a,b]) = go (acc :< a) b
 227 |   go acc t = (acc <>> [], t)
 228 | 
 229 | ------------------------------------------------------------------------------
 230 | -- Interlude: First-order unification by structural recursion by Conor McBride
 231 | ------------------------------------------------------------------------------
 232 | 
 233 | export
 234 | thin : Fin (S n) -> Fin n -> Fin (S n)
 235 | thin FZ y = FS y
 236 | thin (FS x) FZ = FZ
 237 | thin (FS x) (FS y) = FS (thin x y)
 238 | 
 239 | export
 240 | thinInjective : (x : Fin (S n)) -> (y, z : Fin n) -> thin x y === thin x z -> y === z
 241 | thinInjective FZ y z eq = injective eq
 242 | thinInjective (FS x) FZ FZ eq = Refl
 243 | thinInjective (FS x) (FS y) (FS z) eq = cong FS (thinInjective x y z $ injective eq)
 244 | 
 245 | export
 246 | {x : Fin (S n)} -> Injective (thin x) where
 247 |   injective = thinInjective x ? ?
 248 | 
 249 | export
 250 | thinnedApart : (x : Fin (S n)) -> (y : Fin n) -> Not (thin x y === x)
 251 | thinnedApart FZ y = absurd
 252 | thinnedApart (FS x) FZ = absurd
 253 | thinnedApart (FS x) (FS y) = thinnedApart x y . injective
 254 | 
 255 | export
 256 | thinApart : (x, y : Fin (S n)) -> Not (x === y) -> (y' ** thin x y' === y)
 257 | thinApart FZ FZ neq = absurd (neq Refl)
 258 | thinApart FZ (FS y') neq = (y' ** Refl)
 259 | thinApart (FS FZ) FZ neq = (FZ ** Refl)
 260 | thinApart (FS (FS x)) FZ neq = (FZ ** Refl)
 261 | thinApart (FS x@FZ) (FS y) neq = bimap FS (\prf => cong FS prf) (thinApart x y (\prf => neq $ cong FS prf))
 262 | thinApart (FS x@(FS{})) (FS y) neq = bimap FS (\prf => cong FS prf) (thinApart x y (\prf => neq $ cong FS prf))
 263 | 
 264 | public export
 265 | data Thicken : (x, y : Fin n) -> Type where
 266 |   EQ  : Thicken x x
 267 |   NEQ : (y : Fin n) -> Thicken x (thin x y)
 268 | 
 269 | export
 270 | thicken : (x, y : Fin n) -> Thicken x y
 271 | thicken FZ FZ = EQ
 272 | thicken FZ (FS y) = NEQ y
 273 | thicken (FS FZ) FZ = NEQ FZ
 274 | thicken (FS (FS{})) FZ = NEQ FZ
 275 | thicken (FS x) (FS y) with (thicken x y)
 276 |   thicken (FS x) (FS x) | EQ = EQ
 277 |   thicken (FS x) (FS (thin x y)) | NEQ y = NEQ (FS y)
 278 | 
 279 | export
 280 | check : Fin (S n) -> Tm (S n) -> Maybe (Tm n)
 281 | check x (Var y) = case thicken x y of
 282 |   EQ => Nothing
 283 |   NEQ y' => Just (Var y')
 284 | check x (Con f ts) = Con f <$> assert_total (traverse (check x) ts)
 285 | 
 286 | 
 287 | export
 288 | for : Tm n -> Fin (S n) -> Env Tm (S n) n
 289 | (t `for` x) y = case thicken x y of
 290 |   EQ => t
 291 |   NEQ y' => Var y'
 292 | 
 293 | public export
 294 | data AList : (m, n : Nat) -> Type where
 295 |   Lin : AList m m
 296 |   (:<) : AList m n -> (Fin (S m), Tm m) -> AList (S m) n
 297 | 
 298 | export
 299 | (++) : AList m n -> AList l m -> AList l n
 300 | xts ++ [<] = xts
 301 | xts ++ (yus :< yt) = (xts ++ yus) :< yt
 302 | 
 303 | export
 304 | toSubst : AList m n -> Env Tm m n
 305 | toSubst [<] = Var
 306 | toSubst (xts :< (x , t)) =  subst (toSubst xts) . (t `Auto.for` x)
 307 | 
 308 | record Unifying m where
 309 |   constructor MkUnifying
 310 |   {target : Nat}
 311 |   rho : AList m target
 312 |   -- TODO: add proofs too?
 313 | 
 314 | flexFlex : {m : _} -> (x, y : Fin m) -> Unifying m
 315 | flexFlex x y = case thicken x y of
 316 |   EQ => MkUnifying [<]
 317 |   NEQ y' => MkUnifying [<(x, Var y')]
 318 | 
 319 | flexRigid : {m : _} -> (x : Fin m) -> (t : Tm m) -> Maybe (Unifying m)
 320 | -- We only have two cases so that Idris can see that `m` ought to be S-headed
 321 | flexRigid x@FZ t = do
 322 |   t' <- check x t
 323 |   Just (MkUnifying [<(x,t')])
 324 | flexRigid x@(FS{}) t = do
 325 |   t' <- check x t
 326 |   Just (MkUnifying [<(x,t')])
 327 | 
 328 | export
 329 | mgu : {m : _} -> (s, t : Tm m) -> Maybe (Unifying m)
 330 | 
 331 | amgu : {n : _} -> (s, t : Tm m) -> AList m n -> Maybe (Unifying m)
 332 | amgus : {n : _} -> (s, t : List (Tm m)) -> AList m n -> Maybe (Unifying m)
 333 | 
 334 | mgu s t = amgu s t [<]
 335 | 
 336 | amgu (Con f ts) (Con g us) acc
 337 |   = do guard (f == g)
 338 |        amgus ts us acc
 339 | amgu (Var x) (Var y) [<] = Just (flexFlex x y)
 340 | amgu (Var x) t [<] = flexRigid x t
 341 | amgu s (Var y) [<] = flexRigid y s
 342 | amgu s t (rho :< (x, v)) = do
 343 |   let sig = v `for` x
 344 |   MkUnifying acc <- amgu (subst sig s) (subst sig t) rho
 345 |   Just (MkUnifying (acc :< (x, v)))
 346 | 
 347 | amgus [] [] acc = Just (MkUnifying acc)
 348 | amgus (t :: ts) (u :: us) acc = do
 349 |   MkUnifying acc <- amgu t u acc
 350 |   amgus ts us acc
 351 | amgus _ _ _ = Nothing
 352 | 
 353 | ------------------------------------------------------------------------------
 354 | -- End of the interlude
 355 | ------------------------------------------------------------------------------
 356 | 
 357 | export
 358 | record Rule where
 359 |   constructor MkRule
 360 |   context : SnocList Name
 361 |   ruleName : RuleName
 362 |   {arity : Nat}
 363 |   premises : Vect arity (Tm (length context))
 364 |   conclusion : Tm (length context)
 365 | 
 366 | export
 367 | (.scope) : Rule -> Nat
 368 | r .scope = length r.context
 369 | 
 370 | export
 371 | Show Rule where
 372 |   show (MkRule context nm premises conclusion)
 373 |        = unlines
 374 |        $ ifThenElse (null context) "" ("  forall \{unwords (map show context <>> [])}.")
 375 |       :: map (("  " ++) . showTerm context) (toList premises)
 376 |     ++ [ replicate 25 '-' ++ " " ++ show nm
 377 |        , "  " ++ showTerm context conclusion
 378 |        ]
 379 | 
 380 | public export
 381 | HintDB : Type
 382 | HintDB = List Rule
 383 | 
 384 | namespace Example
 385 | 
 386 |   data Add : (m, n, p : Nat) -> Type where
 387 |     AddBase : Add 0 n n
 388 |     AddStep : Add m n p -> Add (S m) n (S p)
 389 | 
 390 |   add : Vect 3 (Tm m) -> Tm m
 391 |   add = Con (UName `{Search.Auto.Example.Add}) . toList
 392 | 
 393 |   zro : Tm m
 394 |   zro = Con (UName `{Prelude.Types.Z}) []
 395 | 
 396 |   suc : Vect 1 (Tm m) -> Tm m
 397 |   suc = Con (UName `{Prelude.Types.S}) . toList
 398 | 
 399 |   qAddBase : Rule
 400 |   qAddBase
 401 |     = MkRule [< UN (Basic "n")] (Free `{AddBase})
 402 |       []
 403 |     -------------------------------
 404 |     $ add [ zro, Var FZ, Var FZ ]
 405 | 
 406 |   qAddStep : Rule
 407 |   qAddStep
 408 |     = MkRule (UN . Basic <$> [<"m","n","p"]) (Free `{AddStep})
 409 |       [add [Var 2, Var 1, Var 0]]
 410 |     -----------------------------
 411 |     $ add [suc [Var 2], Var 1, suc [Var 0]]
 412 | 
 413 |   addHints : HintDB
 414 |   addHints = [qAddBase, qAddStep]
 415 | 
 416 | 
 417 | ||| A search Space represents the space of possible solutions to a problem.
 418 | ||| It is a finitely branching, potentially infinitely deep, tree.
 419 | ||| E.g. we can prove `Nat` using:
 420 | ||| 1. either Z or S                  (finitely branching)
 421 | ||| 2. arbitrarily many S constructor (unbounded depth)
 422 | public export
 423 | data Space : Type -> Type where
 424 |   Solution   : a -> Space a
 425 |   Candidates : List (Inf (Space a)) -> Space a
 426 | 
 427 | ||| A proof is a completed tree where each node is the invocation of a rule
 428 | ||| together with proofs for its premises, or a lambda abstraction with a
 429 | ||| subproof.
 430 | public export
 431 | data Proof : Type where
 432 |   Call : RuleName -> List Proof -> Proof
 433 |   Lam : Nat -> Proof -> Proof
 434 | 
 435 | export
 436 | Show Proof where
 437 |   show prf = unlines (go "" [<] prf <>> []) where
 438 |     go : (indent : String) -> SnocList String -> Proof -> SnocList String
 439 |     go indent acc (Call r prfs) =
 440 |       let acc = acc :< (indent ++ show r) in
 441 |       assert_total $ foldl (go (" " ++ indent)) acc prfs
 442 |     go indent acc (Lam n prf) =
 443 |       let acc = acc :< (indent ++ "\\ x" ++ show n) in
 444 |       assert_total $ go (" " ++ indent) acc prf
 445 | 
 446 | 
 447 | ||| A partial proof is a vector of goals and a continuation which, provided
 448 | ||| a proof for each of the goals, returns a completed proof
 449 | public export
 450 | record PartialProof (m : Nat) where
 451 |   constructor MkPartialProof
 452 |   leftovers : Nat
 453 |   goals : Vect leftovers (Tm m)
 454 |   continuation : Vect leftovers Proof -> Proof
 455 | 
 456 | ||| Helper function to manufacture a proof step
 457 | export
 458 | apply : (r : Rule) -> Vect (r.arity + k) Proof -> Vect (S k) Proof
 459 | apply r args = let (premises, rest) = splitAt r.arity args in
 460 |                Call r.ruleName (toList premises) :: rest
 461 | 
 462 | mkVars : (m : Nat) -> (vars : SnocList Name ** length vars = m)
 463 | mkVars Z = ([<] ** Refl)
 464 | mkVars m@(S m') = bimap (:< UN (Basic $ "_invalidName" ++ show m)) (\prf => cong S prf) (mkVars m')
 465 | 
 466 | solveAcc : {m : _} -> Nat -> HintDB -> PartialProof m -> Space Proof
 467 | solveAcc idx rules (MkPartialProof 0     goals k)
 468 |   = Solution (k [])
 469 | solveAcc idx rules (MkPartialProof (S ar) (Con Arrow [a, b] :: goals) k)
 470 |   -- to discharge an arrow type, we:
 471 |   -- 1. Bind a new variable
 472 |   -- 2. Add a new rule corresponding to that variable whose type is based on the function's domain
 473 |   -- 3. Try to build an element of the codomain
 474 |   = let (prems, res) = split a in
 475 |     let (vars ** Refl) = mkVars m in
 476 |     let rule = MkRule vars (Bound idx) (fromList prems) res in
 477 |     Candidates [ solveAcc (S idx) (rule :: rules)
 478 |                $ MkPartialProof (S ar) (b :: goals)
 479 |                $ \ (b :: prfs) => k (Lam idx b :: prfs)]
 480 | solveAcc idx rules (MkPartialProof (S ar) (g :: goals) k)
 481 |   = Candidates (assert_total $ map step rules) where
 482 | 
 483 |   step : Rule -> Inf (Space Proof)
 484 |   step r with (mgu (rename (weakenN r.scope) g) (rename (shift m) (conclusion r)))
 485 |     _ | Nothing = Candidates []
 486 |     _ | Just sol = let sig = toSubst sol.rho in
 487 |                    solveAcc idx rules $ MkPartialProof
 488 |                      (r.arity + ar)
 489 |                      (map (subst (sig . shift m)) r.premises
 490 |                       ++ map (subst (sig . weakenN r.scope)) goals)
 491 |                      (k . apply r)
 492 | 
 493 | ||| Solve takes a database of hints, a goal to prove and returns
 494 | ||| the full search space.
 495 | export
 496 | solve : {m : _} -> Nat -> HintDB -> Tm m -> Space Proof
 497 | solve idx rules goal = solveAcc idx rules (MkPartialProof 1 [goal] head)
 498 | 
 499 | ||| Depth first search strategy to explore a search space.
 500 | ||| This is made total by preemptively limiting the depth the search
 501 | ||| is willing to explore.
 502 | export
 503 | dfs : (depth : Nat) -> Space a -> List a
 504 | dfs _ (Solution x) = [x]
 505 | dfs 0 _ = []
 506 | dfs (S k) (Candidates cs) = cs >>= \ c => dfs k c
 507 | 
 508 | namespace Example
 509 | 
 510 |   four : Maybe Proof
 511 |   four = head'
 512 |        $ dfs 5
 513 |        $ solve {m = 0} 0 addHints
 514 |        $ add [ suc [suc [zro]]
 515 |              , suc [suc [zro]]
 516 |              , suc [suc [suc [suc [zro]]]]
 517 |              ]
 518 | 
 519 | lengthDistributesOverFish : (sx : SnocList a) -> (xs : List a) ->
 520 |                             length (sx <>< xs) === length sx + length xs
 521 | lengthDistributesOverFish sx [] = sym $ plusZeroRightNeutral ?
 522 | lengthDistributesOverFish sx (x :: xs) = Calc $
 523 |   |~ length ((sx :< x) <>< xs)
 524 |   ~~ length (sx :< x) + length xs ...( lengthDistributesOverFish (sx :< x) xs)
 525 |   ~~ S (length sx) + length xs    ...( Refl )
 526 |   ~~ length sx + S (length xs)    ...( plusSuccRightSucc ? ? )
 527 |   ~~ length sx + length (x :: xs) ...( Refl )
 528 | 
 529 | convertVar : (vars : SnocList Name) -> Name -> Tm (length vars)
 530 | convertVar [<] nm = Con (UName nm) []
 531 | convertVar (sx :< x) nm = if x == nm then Var FZ else go sx [x] FZ
 532 | 
 533 |   where
 534 | 
 535 |   go : (vars : SnocList Name) -> (ctxt : List Name) ->
 536 |        Fin (length ctxt) -> Tm (length (vars <>< ctxt))
 537 |   go [<] ctxt k = Con (UName nm) []
 538 |   go (sx :< x) ctxt k =
 539 |     if x == nm
 540 |     then Var $ rewrite lengthDistributesOverFish sx (x :: ctxt) in
 541 |                rewrite plusCommutative (length sx) (S (length ctxt)) in
 542 |                weakenN (length sx) (FS k)
 543 |     else go sx (x :: ctxt) (FS k)
 544 | 
 545 | skolemVar : SnocList Name -> Name -> Tm 0
 546 | skolemVar [<] nm = Con (UName nm) []
 547 | skolemVar (sx :< x) nm
 548 |   = if nm == x then Con (Bound (length sx)) [] else skolemVar sx nm
 549 | 
 550 | getFnArgs : TTImp -> (TTImp, List TTImp)
 551 | getFnArgs = go [] where
 552 | 
 553 |   go : List TTImp -> TTImp -> (TTImp, List TTImp)
 554 |   go acc (IApp _ f t) = go (t :: acc) f
 555 |   go acc (INamedApp _ f n t) = go acc f
 556 |   go acc (IAutoApp _ f t) = go acc f
 557 |   go acc t = (t, acc)
 558 | 
 559 | parameters (0 f : SnocList Name -> Nat) (cvar : (vars : SnocList Name) -> Name -> Tm (f vars))
 560 | 
 561 |   ||| Converts a type of the form (a -> (a -> b -> c) -> b -> c)
 562 |   ||| to our internal representation
 563 |   export
 564 |   convert : (vars : SnocList Name) -> TTImp -> Either TTImp (Tm (f vars))
 565 |   convert vars (IVar _ nm) = pure (cvar vars nm)
 566 |   convert vars t@(IApp x y z) = do
 567 |     let (IVar _ nm, args) = getFnArgs t
 568 |       | _ => Left t
 569 |     let (Con nm []) = convertVar vars nm
 570 |       | _ => Left t
 571 |     Con nm <$>  assert_total (traverse (convert vars) args)
 572 |   convert vars t@(IPi _ _ ExplicitArg (Just n@(UN{})) argTy retTy) = Left t
 573 |   convert vars (IPi _ _ ExplicitArg _ argTy retTy)
 574 |     = do a <- convert vars argTy
 575 |          b <- convert vars retTy
 576 |          pure (Con Arrow [a,b])
 577 |   convert vars t = Left t
 578 | 
 579 |   ||| Parse a type of the form
 580 |   ||| forall a b c. a -> (a -> b -> c) -> b -> c to
 581 |   ||| 1. a scope [<a,b,c]
 582 |   ||| 2. a representation of the rest
 583 |   export
 584 |   parseType : TTImp -> Either TTImp (vars : SnocList Name ** Tm (f vars))
 585 |   parseType = go [<] where
 586 | 
 587 |     go : SnocList Name -> TTImp -> Either TTImp (vars : SnocList Name ** Tm (f vars))
 588 |     go vars (IPi _ _ ImplicitArg mn _ retTy)
 589 |       = go (vars :< fromMaybe (UN Underscore) mn) retTy
 590 |     go vars t = map (MkDPair vars) (convert vars t)
 591 | 
 592 | ||| Parse a type, where bound variables are flexible variables
 593 | export
 594 | parseRule : TTImp -> Either TTImp (vars : SnocList Name ** Tm (length vars))
 595 | parseRule = parseType length convertVar
 596 | 
 597 | ||| Parse a type, where bound variables are rigid variables
 598 | export
 599 | parseGoal : TTImp -> Either TTImp (SnocList Name, Tm 0)
 600 | parseGoal t = do
 601 |   (vars ** g) <- parseType (\ _ => 0) skolemVar t
 602 |   pure (vars, g)
 603 | 
 604 | export
 605 | mkRule : Name -> Elab Rule
 606 | mkRule nm = do
 607 |   [(_, ty)] <- getType nm
 608 |     | [] => fail "Couldn't find \{show nm}."
 609 |     | nms => fail $ concat
 610 |                   $ "Ambiguous name \{show nm}, could be any of: "
 611 |                   :: intersperse ", " (map (show . fst) nms)
 612 |   logMsg (show nm) 1 "Found the definition."
 613 |   let Right (m ** tm) = parseRule ty
 614 |     | Left t => fail "The type of \{show nm} is unsupported, chocked on \{show t}"
 615 |   logMsg (show nm) 1 "Parsed the type."
 616 |   let (premises, goal) = split tm
 617 |   logMsg (show nm) 1 "Successfully split the type."
 618 |   let r = MkRule m (Free nm) (fromList premises) goal
 619 |   logMsg "auto.quoting.\{show nm}" 1 ("\n" ++ show r)
 620 |   pure r
 621 | 
 622 | namespace Example
 623 | 
 624 |   evenHints : HintDB
 625 |   evenHints = with [Prelude.(::), Prelude.Nil]
 626 |             [ %runElab (mkRule `{EvenZ})
 627 |             , %runElab (mkRule `{EvenS})
 628 |             , %runElab (mkRule `{EvenPlus})
 629 |             ]
 630 | 
 631 | export
 632 | getGoal : Elab (HintDB, Tm 0)
 633 | getGoal = do
 634 |   Just gty <- goal
 635 |     | Nothing => fail "No goal to get"
 636 |   let Right (vars, qgty) = parseGoal gty
 637 |     | Left t => fail "Couldn't parse goal type: \{show t}"
 638 |   let (qass, qg) = split qgty
 639 |   pure (toPremises (length vars) qass, qg)
 640 | 
 641 |   where
 642 |   toPremises : Nat -> List (Tm 0) -> HintDB
 643 |   toPremises acc [] = []
 644 |   toPremises acc (t :: ts)
 645 |     = let (prems, res) = split t in
 646 |       MkRule [<] (Bound acc) (fromList prems) res :: toPremises (S acc) ts
 647 | 
 648 | export
 649 | unquote : Proof -> TTImp
 650 | unquote (Call f xs)
 651 |   = foldl (IApp emptyFC) (IVar emptyFC (toName f))
 652 |   $ assert_total (map unquote xs)
 653 | unquote (Lam n prf)
 654 |   = ILam emptyFC MW ExplicitArg (Just $ toName (Bound n)) (Implicit emptyFC False)
 655 |   $ unquote prf
 656 | 
 657 | export
 658 | intros : List a -> TTImp -> TTImp
 659 | intros = go 0 where
 660 | 
 661 |   go : Nat -> List a -> TTImp -> TTImp
 662 |   go idx [] t = t
 663 |   go idx (_ :: as) t
 664 |     = ILam emptyFC MW ExplicitArg (Just $ toName (Bound idx)) (Implicit emptyFC False)
 665 |     $ go (S idx) as t
 666 | 
 667 | export
 668 | bySearch : (depth : Nat) -> HintDB -> Elab a
 669 | bySearch depth rules = do
 670 |   (rules', g) <- getGoal
 671 |   logMsg "auto.search.goal" 1 (showTerm [<] g)
 672 |   let rules = rules ++ rules'
 673 |   logMsg "auto.search.rules" 1 (unlines $ map show rules')
 674 |   let (prf :: _) = dfs depth (solve (length rules') rules g)
 675 |     | _ => fail "Couldn't find proof for goal"
 676 |   check (intros rules' (unquote prf))
 677 | 
 678 | namespace Example
 679 | 
 680 |   idTest : a -> a
 681 |   idTest = %runElab (bySearch 2 [])
 682 | 
 683 |   constTest : a -> b -> a
 684 |   constTest = %runElab (bySearch 2 [])
 685 | 
 686 |   sTest : (a -> b -> c) -> (a -> b) -> a -> c
 687 |   sTest = %runElab (bySearch 4 [])
 688 | 
 689 |   -- The type of `MkPair` is falsely dependent and makes the machinery choke
 690 |   -- so we define this one instead
 691 |   mkPair : a -> b -> Pair a b
 692 |   mkPair a b = (a, b)
 693 | 
 694 |   listFromDupTest : (a -> (a -> (a, a)) -> List a) -> a -> List a
 695 |   listFromDupTest = %runElab (bySearch 6 [%runElab (mkRule `{mkPair})])
 696 | 
 697 |   even0Test : Even Z
 698 |   even0Test = %runElab (bySearch 1 evenHints)
 699 | 
 700 |   even2Test : Even 2
 701 |   even2Test = %runElab (bySearch 2 evenHints)
 702 | 
 703 |   evenPlusTest : Even n -> Even m -> Even (m + n)
 704 |   evenPlusTest = %runElab (bySearch 3 evenHints)
 705 | 
 706 |   evenPlus2Test : Even m -> Even (m + 2)
 707 |   evenPlus2Test = %runElab (bySearch 4 evenHints)
 708 | 
 709 |   addBaseTest : Add Z Z Z
 710 |   addBaseTest = %runElab (bySearch 3 addHints)
 711 | 
 712 |   add2TwiceTest : Add 2 2 4
 713 |   add2TwiceTest = %runElab (bySearch 3 addHints)
 714 |