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

git.iko.soy/Idris-dev

on master help sign in

A small amount of proof automation, via tactic reflection

04d6f00Edwin Brady14 years ago

lib/Language/Reflection.idr+8−1

compare with master

unifiedsplit

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

1module Language.Reflection

3TTName : Type

4−TTName = String

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

6data TT = Var TTName

7 | Lam TTName TT TT

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

9 | Let TTName TT TT TT

10 | App TTName TT TT

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

484

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

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

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

487−try t1 t2 = do s <- get

491+ = do s <- get

488 case runStateT t1 s of

492 case runStateT t1 s of

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

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

490 return v

494 return v

491− Error e1 -> if recoverableErr e1 then

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

492 do case runStateT t2 s of

496 do case runStateT t2 s of

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

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

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

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

src/Idris/AbsSyntaxTree.hs+1

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

472 | ProofState | ProofTerm | Undo

473 | Try (PTactic' t) (PTactic' t)

474 | TSeq (PTactic' t) (PTactic' t)

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

475 | Qed | Abandon

476 | Qed | Abandon

476 deriving (Show, Eq, Functor)

477 deriving (Show, Eq, Functor)

477{-!

478{-!

src/Idris/ElabTerm.hs+42−3

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

293 tryWhen True

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

295 let (ns', eargs)

296− = unzip $

296+ = unzip $

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

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

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

298 (zip ns args)

299 (zip ns args)

299 try

300 try

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

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

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

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

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

318 tcArg _ = False

319 tcArg _ = False

319

320

321+ tacTm (PTactics _) = True

322+ tacTm (PProof _) = True

323+ tacTm _ = False

324+

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

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

321 = erun fc $

326 = erun fc $

322 do ptm <- get_term

327 do ptm <- get_term

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

630 runT Trivial = do trivial ist; when autoSolve solveAll

635 runT Trivial = do trivial ist; when autoSolve solveAll

631 runT (Focus n) = focus n

636 runT (Focus n) = focus n

632 runT Solve = solve

637 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

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

639 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"

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

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

636

658

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+

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

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

638

677

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

678-- 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

1351 put x1

1352 put x2

1353 Qed -> putWord8 15

1354+ ReflectTac x1 -> do putWord8 16

1355+ put x1

1354 get

1356 get

1355 = do i <- getWord8

1357 = do i <- getWord8

1356 case i of

1358 case i of

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

1382 x2 <- get

1384 x2 <- get

1383 return (TSeq x1 x2)

1385 return (TSeq x1 x2)

1384 15 -> return Qed

1386 15 -> return Qed

1387+ 16 -> do x1 <- get

1388+ return (ReflectTac x1)

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

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

1386

1390

1387

1391

src/Idris/Parser.hs+3

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

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

1504 i <- getState

1505 return $ Exact (desugar syn i t)

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

1507+ i <- getState

1508+ return $ ReflectTac (desugar syn i t)

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

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

1507 lchar '|';

1510 lchar '|';

1508 t1 <- pTactic syn

1511 t1 <- pTactic syn