04d6f00 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

A small amount of proof automation, via tactic reflection

commit04d6f002220a0590adc550ab0a5eec90d5bd2d07 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 6 Jan 2013, 18:23 (14 years ago) parentd06d473

6 files changed+64−6

compare with master

unifiedsplit

lib/Language/Reflection.idr+8−1 src/Core/Elaborate.hs+6−2 src/Idris/AbsSyntaxTree.hs+1 src/Idris/ElabTerm.hs+42−3 src/Idris/IBC.hs+4 src/Idris/Parser.hs+3

lib/Language/Reflection.idr+8−1

@@ -1,7 +1,7 @@

11module Language.Reflection

33TTName : Type

4−TTName = String

4+TTName = String -- needs to capture namespaces too...

66data TT = Var TTName

77 | Lam TTName TT TT

@@ -9,3 +9,10 @@ data TT = Var TTName

99 | Let TTName TT TT TT

1010 | App TTName TT TT

1111

12+data Tactic = Try Tactic Tactic

13+ | Refine TTName

14+ | Seq Tactic Tactic

15+ | Trivial

16+ | Solve

17+ | Exact TT -- not yet implemented

18+

src/Core/Elaborate.hs+6−2

@@ -484,11 +484,15 @@ arg n tyhole = do ty <- unique_hole tyhole

484484

485485-- Try a tactic, if it fails, try another

486486try :: Elab' aux a -> Elab' aux a -> Elab' aux a

487−try t1 t2 = do s <- get

487+try t1 t2 = try' t1 t2 False

488+

489+try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

490+try' t1 t2 proofSearch

491+ = do s <- get

488492 case runStateT t1 s of

489493 OK (v, s') -> do put s'

490494 return v

491− Error e1 -> if recoverableErr e1 then

495+ Error e1 -> if proofSearch || recoverableErr e1 then

492496 do case runStateT t2 s of

493497 OK (v, s') -> do put s'; return v

494498 Error e2 -> if score e1 >= score e2

src/Idris/AbsSyntaxTree.hs+1

@@ -472,6 +472,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

472472 | ProofState | ProofTerm | Undo

473473 | Try (PTactic' t) (PTactic' t)

474474 | TSeq (PTactic' t) (PTactic' t)

475+ | ReflectTac t -- see Language.Reflection module

475476 | Qed | Abandon

476477 deriving (Show, Eq, Functor)

477478{-!

src/Idris/ElabTerm.hs+42−3

@@ -293,8 +293,9 @@ elab ist info pattern tcgen fn tm

293293 tryWhen True

294294 (do ns <- apply (Var f) (map isph args)

295295 let (ns', eargs)

296− = unzip $

297− sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))

296+ = unzip $

297+ sortBy (\(_,x) (_,y) ->

298+ compare (priority x) (priority y))

298299 (zip ns args)

299300 try

300301 (elabArgs (ina || not isinf, guarded)

@@ -317,6 +318,10 @@ elab ist info pattern tcgen fn tm

317318 where tcArg (n, PConstraint _ _ Placeholder _) = True

318319 tcArg _ = False

319320

321+ tacTm (PTactics _) = True

322+ tacTm (PProof _) = True

323+ tacTm _ = False

324+

320325 elab' ina@(_, a) (PApp fc f [arg])

321326 = erun fc $

322327 do ptm <- get_term

@@ -630,10 +635,44 @@ runTac autoSolve ist tac = do env <- get_env

630635 runT Trivial = do trivial ist; when autoSolve solveAll

631636 runT (Focus n) = focus n

632637 runT Solve = solve

633− runT (Try l r) = do try (runT l) (runT r)

638+ runT (Try l r) = do try' (runT l) (runT r) True

634639 runT (TSeq l r) = do runT l; runT r

640+ runT (ReflectTac tm) = do attack -- let x : Tactic = tm in ...

641+ valn <- unique_hole (MN 0 "tacval")

642+ claim valn (Var tacticTy)

643+ tacn <- unique_hole (MN 0 "tacn")

644+ letbind tacn (Var tacticTy) (Var valn)

645+ focus valn

646+ elab ist toplevel False False (MN 0 "tac") tm

647+ (tm', ty') <- get_type_val (Var tacn)

648+ ctxt <- get_context

649+ env <- get_env

650+ -- g <- goal

651+ let tactic = normalise ctxt env tm'

652+ runReflected tactic

653+-- p <- get_term

654+-- trace (show p ++ "\n\n") $

655+ return ()

656+ where tacticTy = tacm "Tactic"

635657 runT x = fail $ "Not implemented " ++ show x

636658

659+ runReflected t = do t' <- reify t

660+ runTac autoSolve ist t'

661+ tacm n = NS (UN n) ["Reflection", "Language"]

662+

663+ reify :: Term -> ElabD PTactic

664+ reify (P _ n _) | n == tacm "Trivial" = return Trivial

665+ reify (P _ n _) | n == tacm "Solve" = return Solve

666+ reify f@(App _ _)

667+ | (P _ f _, args) <- unApply f = reifyAp f args

668+ reify t = fail "Unknown tactic"

669+

670+ reifyAp t [l, r] | t == tacm "Try" = liftM2 Try (reify l) (reify r)

671+ reifyAp t [Constant (Str x)]

672+ | t == tacm "Refine" = return $ Refine (UN x) []

673+ reifyAp t [l, r] | t == tacm "Seq" = liftM2 TSeq (reify l) (reify r)

674+ reifyAp f args = fail "Unknown tactic" -- shouldn't happen

675+

637676solveAll = try (do solve; solveAll) (return ())

638677

639678-- If the function application is specialisable, make a new

src/Idris/IBC.hs+4

@@ -1351,6 +1351,8 @@ instance (Binary t) => Binary (PTactic' t) where

13511351 put x1

13521352 put x2

13531353 Qed -> putWord8 15

1354+ ReflectTac x1 -> do putWord8 16

1355+ put x1

13541356 get

13551357 = do i <- getWord8

13561358 case i of

@@ -1382,6 +1384,8 @@ instance (Binary t) => Binary (PTactic' t) where

13821384 x2 <- get

13831385 return (TSeq x1 x2)

13841386 15 -> return Qed

1387+ 16 -> do x1 <- get

1388+ return (ReflectTac x1)

13851389 _ -> error "Corrupted binary data for PTactic'"

13861390

13871391

src/Idris/Parser.hs+3

@@ -1503,6 +1503,9 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

15031503 <|> do reserved "exact"; t <- pExpr syn;

15041504 i <- getState

15051505 return $ Exact (desugar syn i t)

1506+ <|> do reserved "reflect"; t <- pExpr syn;

1507+ i <- getState

1508+ return $ ReflectTac (desugar syn i t)

15061509 <|> do reserved "try"; t <- pTactic syn;

15071510 lchar '|';

15081511 t1 <- pTactic syn