git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1425 from david-christiansen/fail-skip-tactics

Add tactics "skip" and "fail"

commit92af9baaa60c77c482704fb414121ad931022b2d authorDavid Christiansen <david@davidchristiansen.dk> dateThu 24 Jul 2014, 23:48 (12 years ago) parent853271084b172a
13 files changed+113−12
compare with master
unifiedsplit
CHANGELOG+5 idris.cabal+3 libs/base/Language/Reflection.idr+10 libs/base/Language/Reflection/Errors.idr−7 src/Idris/AbsSyntaxTree.hs+4 src/Idris/Core/TT.hs+6 src/Idris/DeepSeq.hs+8 src/Idris/ElabDecls.hs+1−1 src/Idris/ElabTerm.hs+16−4 src/Idris/ParseExpr.hs+4 test/quasiquote004/Quasiquote004.idr+51 test/quasiquote004/expected+2 test/quasiquote004/run+3
CHANGELOG+5
@@ -1,3 +1,8 @@
1+New in 0.9.15:
2+--------------
3+* Two new tactics: skip and fail. Skip does nothing, and fail takes a string as an argument and produces it as an error.
4+* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list of ErrorReportParts as an argument, like error handlers produce, allowing access to the pretty-printer.
5+
16New in 0.9.14:
27--------------
38* Tactic for case analysis in proofs
idris.cabal+3
@@ -425,6 +425,9 @@ Extra-source-files:
425425 test/quasiquote003/run
426426 test/quasiquote003/*.idr
427427 test/quasiquote003/expected
428+ test/quasiquote004/run
429+ test/quasiquote004/*.idr
430+ test/quasiquote004/expected
428431
429432
430433 test/records001/run
libs/base/Language/Reflection.idr+10
@@ -156,6 +156,13 @@ data Raw = Var TTName
156156
157157%name Raw tm, tm'
158158
159+||| Error reports are a list of report parts
160+data ErrorReportPart = TextPart String
161+ | NamePart TTName
162+ | TermPart TT
163+ | SubReport (List ErrorReportPart)
164+%name ErrorReportPart part, p
165+
159166data Tactic = Try Tactic Tactic
160167 -- ^ try the first tactic and resort to the second one on failure
161168 | GoalType String Tactic
@@ -202,4 +209,7 @@ data Tactic = Try Tactic Tactic
202209 -- ^ name a reflected term and type it
203210 | Compute
204211 -- ^ normalise the context
212+ | Skip
213+ -- ^ do nothing
214+ | Fail (List ErrorReportPart)
205215%name Tactic tac, tac'
libs/base/Language/Reflection/Errors.idr−7
@@ -40,13 +40,6 @@ data Err = Msg String
4040
4141%name Err err, e
4242
43−||| Error reports are a list of report parts
44−data ErrorReportPart = TextPart String
45− | NamePart TTName
46− | TermPart TT
47− | SubReport (List ErrorReportPart)
48−%name ErrorReportPart part, p
49−
5043-- Error reports become functions in List (String, TT) -> Err -> ErrorReport
5144ErrorHandler : Type
5245ErrorHandler = Err -> Maybe (List ErrorReportPart)
src/Idris/AbsSyntaxTree.hs+4
@@ -767,6 +767,8 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
767767 | TEval t
768768 | TDocStr (Either Name Const)
769769 | TSearch t
770+ | Skip
771+ | TFail [ErrorReportPart]
770772 | Qed | Abandon
771773 deriving (Show, Eq, Functor)
772774{-!
@@ -796,6 +798,8 @@ instance Sized a => Sized (PTactic' a) where
796798 size (Fill t) = 1 + size t
797799 size Qed = 1
798800 size Abandon = 1
801+ size Skip = 1
802+ size (TFail ts) = 1 + size ts
799803
800804type PTactic = PTactic' PTerm
801805
src/Idris/Core/TT.hs+6
@@ -158,6 +158,12 @@ type Err = Err' Term
158158deriving instance NFData Err
159159!-}
160160
161+instance Sized ErrorReportPart where
162+ size (TextPart msg) = 1 + length msg
163+ size (TermPart t) = 1 + size t
164+ size (NamePart n) = 1 + size n
165+ size (SubReport rs) = 1 + size rs
166+
161167instance Sized Err where
162168 size (Msg msg) = length msg
163169 size (InternalMsg msg) = length msg
src/Idris/DeepSeq.hs+8
@@ -260,6 +260,14 @@ instance (NFData t) => NFData (PTactic' t) where
260260 rnf (GoalType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
261261 rnf Qed = ()
262262 rnf Abandon = ()
263+ rnf Skip = ()
264+ rnf (TFail x1) = rnf x1 `seq` ()
265+
266+instance NFData ErrorReportPart where
267+ rnf (TermPart x1) = rnf x1 `seq` ()
268+ rnf (TextPart x1) = rnf x1 `seq` ()
269+ rnf (NamePart x1) = rnf x1 `seq` ()
270+ rnf (SubReport x1) = rnf x1 `seq` ()
263271
264272instance (NFData t) => NFData (PDo' t) where
265273 rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
src/Idris/ElabDecls.hs+1−1
@@ -209,7 +209,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
209209 , ns1 == map txt ["Errors","Reflection","Language"]
210210 , ns2 == map txt ["Maybe", "Prelude"]
211211 , ns3 == map txt ["List", "Prelude"]
212− , ns4 == map txt ["Errors","Reflection","Language"] = True
212+ , ns4 == map txt ["Reflection","Language"] = True
213213 tyIsHandler _ = False
214214
215215-- Get the list of (index, name) of inaccessible arguments from an elaborated
src/Idris/ElabTerm.hs+16−4
@@ -1359,6 +1359,8 @@ runTac autoSolve ist fn tac
13591359 _ -> fail "Wrong goal type"
13601360 runT ProofState = do g <- goal
13611361 return ()
1362+ runT Skip = return ()
1363+ runT (TFail err) = lift . tfail $ ReflectionError [err] (Msg "")
13621364 runT x = fail $ "Not implemented " ++ show x
13631365
13641366 runReflected t = do t' <- reify ist t
@@ -1376,6 +1378,7 @@ reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
13761378reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
13771379reify _ (P _ n _) | n == reflm "Solve" = return Solve
13781380reify _ (P _ n _) | n == reflm "Compute" = return Compute
1381+reify _ (P _ n _) | n == reflm "Skip" = return Skip
13791382reify ist t@(App _ _)
13801383 | (P _ f _, args) <- unApply t = reifyApp ist f args
13811384reify _ t = fail ("Unknown tactic " ++ show t)
@@ -1416,6 +1419,15 @@ reifyApp ist t [n, tt', t']
14161419 tt'' <- reifyTT tt'
14171420 t'' <- reifyTT t'
14181421 return $ LetTacTy n' (delab ist tt'') (delab ist t'')
1422+reifyApp ist t [errs]
1423+ | t == reflm "Fail" = case unList errs of
1424+ Nothing -> fail "Failed to reify errors"
1425+ Just errs' ->
1426+ let parts = mapM reifyReportPart errs' in
1427+ case parts of
1428+ Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
1429+ Right errs'' ->
1430+ return $ TFail errs''
14191431reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
14201432
14211433-- | Reify terms from their reflected representation
@@ -2042,10 +2054,10 @@ reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
20422054-- representation. Not in Idris or ElabD monads because it should be usable
20432055-- from either.
20442056reifyReportPart :: Term -> Either Err ErrorReportPart
2045−reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =
2057+reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =
20462058 Right (TextPart msg)
20472059reifyReportPart (App (P (DCon _ _) n _) ttn)
2048− | n == reflErrName "NamePart" =
2060+ | n == reflm "NamePart" =
20492061 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of
20502062 Error e -> Left . InternalMsg $
20512063 "could not reify name term " ++
@@ -2053,7 +2065,7 @@ reifyReportPart (App (P (DCon _ _) n _) ttn)
20532065 " when reflecting an error:" ++ show e
20542066 OK (n', _)-> Right $ NamePart n'
20552067reifyReportPart (App (P (DCon _ _) n _) tm)
2056− | n == reflErrName "TermPart" =
2068+ | n == reflm "TermPart" =
20572069 case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of
20582070 Error e -> Left . InternalMsg $
20592071 "could not reify reflected term " ++
@@ -2061,7 +2073,7 @@ reifyReportPart (App (P (DCon _ _) n _) tm)
20612073 " when reflecting an error:" ++ show e
20622074 OK (tm', _) -> Right $ TermPart tm'
20632075reifyReportPart (App (P (DCon _ _) n _) tm)
2064− | n == reflErrName "SubReport" =
2076+ | n == reflm "SubReport" =
20652077 case unList tm of
20662078 Just xs -> do subParts <- mapM reifyReportPart xs
20672079 Right (SubReport subParts)
src/Idris/ParseExpr.hs+4
@@ -1278,6 +1278,10 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (
12781278 <|> do reserved "undo"; return Undo
12791279 <|> do reserved "qed"; return Qed
12801280 <|> do reserved "abandon"; return Abandon
1281+ <|> do reserved "skip"; return Skip
1282+ <|> do reserved "fail"
1283+ msg <- stringLiteral
1284+ return $ TFail [Idris.Core.TT.TextPart msg]
12811285 <|> do lchar ':';
12821286 ( (do reserved "q"; return Abandon)
12831287 <|> (do (reserved "e" <|> reserved "eval");
test/quasiquote004/Quasiquote004.idrnew file+51
@@ -0,0 +1,51 @@
1+module Quasiquote004
2+
3+import Language.Reflection
4+
5+%default total
6+
7+normPlus : List (TTName, Binder TT) -> TT -> Tactic
8+normPlus ctxt `((=) {Nat} {Nat} ~x ~y) = normPlus ctxt x `Seq` normPlus ctxt y
9+normPlus ctxt `(S ~n) = normPlus ctxt n
10+normPlus ctxt `(plus ~n (S ~m)) = Seq (Rewrite `(plusSuccRightSucc ~n ~m))
11+ (normPlus ctxt m)
12+normPlus _ _ = Skip
13+
14+
15+zero : List (TTName, Binder TT) -> TT -> Tactic
16+zero ctxt `(Nat) = Exact `(Z)
17+zero _ _ = Fail [TextPart "Not a Nat goal"]
18+
19+-- A number is fizzy if it is evenly divisible by 3
20+data Fizzy : Nat -> Type where
21+ ZeroFizzy : Fizzy Z
22+ Fizz : Fizzy n -> Fizzy (3 + n)
23+
24+-- Fizzy is a correct specification of divisibility by 3 - that is, if n is
25+-- fizzy then there exists some k such that n = 3*k.
26+fizzyCorrect : (n : Nat) -> Fizzy n -> (k : Nat ** n = 3 * k)
27+fizzyCorrect Z ZeroFizzy = (Z ** refl)
28+fizzyCorrect (S (S (S k))) (Fizz x) =
29+ let (k' ** ih) = fizzyCorrect k x
30+ in (S k' ** ?fizzyIsAOK)
31+
32+someNat : Nat
33+someNat = ?getMeNat
34+
35+notNat : String
36+notNat = ?getMeNat'
37+
38+---------- Proofs ----------
39+Quasiquote004.getMeNat = proof
40+ applyTactic zero
41+
42+Quasiquote004.fizzyIsAOK = proof
43+ compute
44+ intros
45+ applyTactic normPlus
46+ applyTactic normPlus
47+ rewrite ih
48+ trivial
49+
50+Quasiquote004.getMeNat' = proof
51+ applyTactic zero
test/quasiquote004/expectednew file+2
@@ -0,0 +1,2 @@
1+Quasiquote004.idr:50:25:When elaborating right hand side of Quasiquote004.getMeNat':
2+Not a Nat goal
test/quasiquote004/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ --check --nocolour Quasiquote004.idr
3+rm -f *.ibc