git.iko.soy/Idris-dev
on master help sign in
Add tactics "skip" and "fail"

"skip" does nothing, while "fail" produces an error. They have corresponding reflected versions Skip and Fail. Fail has access to the pretty printer by taking a List ErrorReportPart as its argument.

commit84b172a4e68554720d38695381b8b801d0a75e82 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 24 Jul 2014, 23:26 (12 years ago) parent8532710
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