84b172a · Idris-dev · git.iko.soy

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+

1New in 0.9.14:

6New in 0.9.14:

2--------------

7--------------

3* Tactic for case analysis in proofs

8* Tactic for case analysis in proofs

idris.cabal+3

@@ -425,6 +425,9 @@ Extra-source-files:

425 test/quasiquote003/run

426 test/quasiquote003/*.idr

427 test/quasiquote003/expected

428+ test/quasiquote004/run

429+ test/quasiquote004/*.idr

430+ test/quasiquote004/expected

428

431

429

432

430 test/records001/run

433 test/records001/run

libs/base/Language/Reflection.idr+10

@@ -156,6 +156,13 @@ data Raw = Var TTName

156

157%name Raw tm, tm'

158

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+

159data Tactic = Try Tactic Tactic

166data Tactic = Try Tactic Tactic

160 -- ^ try the first tactic and resort to the second one on failure

167 -- ^ try the first tactic and resort to the second one on failure

161 | GoalType String Tactic

168 | GoalType String Tactic

@@ -202,4 +209,7 @@ data Tactic = Try Tactic Tactic

202 -- ^ name a reflected term and type it

209 -- ^ name a reflected term and type it

203 | Compute

210 | Compute

204 -- ^ normalise the context

211 -- ^ normalise the context

212+ | Skip

213+ -- ^ do nothing

214+ | Fail (List ErrorReportPart)

205%name Tactic tac, tac'

215%name Tactic tac, tac'

libs/base/Language/Reflection/Errors.idr−7

@@ -40,13 +40,6 @@ data Err = Msg String

40

41%name Err err, e

42

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−

50-- Error reports become functions in List (String, TT) -> Err -> ErrorReport

43-- Error reports become functions in List (String, TT) -> Err -> ErrorReport

51ErrorHandler : Type

44ErrorHandler : Type

52ErrorHandler = Err -> Maybe (List ErrorReportPart)

45ErrorHandler = Err -> Maybe (List ErrorReportPart)

src/Idris/AbsSyntaxTree.hs+4

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

767 | TEval t

768 | TDocStr (Either Name Const)

769 | TSearch t

770+ | Skip

771+ | TFail [ErrorReportPart]

770 | Qed | Abandon

772 | Qed | Abandon

771 deriving (Show, Eq, Functor)

773 deriving (Show, Eq, Functor)

772{-!

774{-!

@@ -796,6 +798,8 @@ instance Sized a => Sized (PTactic' a) where

796 size (Fill t) = 1 + size t

798 size (Fill t) = 1 + size t

797 size Qed = 1

799 size Qed = 1

798 size Abandon = 1

800 size Abandon = 1

801+ size Skip = 1

802+ size (TFail ts) = 1 + size ts

799

803

800type PTactic = PTactic' PTerm

804type PTactic = PTactic' PTerm

801

805

src/Idris/Core/TT.hs+6

@@ -158,6 +158,12 @@ type Err = Err' Term

158deriving instance NFData Err

159!-}

160

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+

161instance Sized Err where

167instance Sized Err where

162 size (Msg msg) = length msg

168 size (Msg msg) = length msg

163 size (InternalMsg msg) = length msg

169 size (InternalMsg msg) = length msg

src/Idris/DeepSeq.hs+8

@@ -260,6 +260,14 @@ instance (NFData t) => NFData (PTactic' t) where

260 rnf (GoalType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

261 rnf Qed = ()

262 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` ()

263

271

264instance (NFData t) => NFData (PDo' t) where

272instance (NFData t) => NFData (PDo' t) where

265 rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

273 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

209 , ns1 == map txt ["Errors","Reflection","Language"]

210 , ns2 == map txt ["Maybe", "Prelude"]

211 , ns3 == map txt ["List", "Prelude"]

212− , ns4 == map txt ["Errors","Reflection","Language"] = True

212+ , ns4 == map txt ["Reflection","Language"] = True

213 tyIsHandler _ = False

214

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

1359 _ -> fail "Wrong goal type"

1360 runT ProofState = do g <- goal

1361 return ()

1362+ runT Skip = return ()

1363+ runT (TFail err) = lift . tfail $ ReflectionError [err] (Msg "")

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

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

1363

1365

1364 runReflected t = do t' <- reify ist t

1366 runReflected t = do t' <- reify ist t

@@ -1376,6 +1378,7 @@ reify _ (P _ n _) | n == reflm "Trivial" = return Trivial

1376reify _ (P _ n _) | n == reflm "Instance" = return TCInstance

1378reify _ (P _ n _) | n == reflm "Instance" = return TCInstance

1377reify _ (P _ n _) | n == reflm "Solve" = return Solve

1379reify _ (P _ n _) | n == reflm "Solve" = return Solve

1378reify _ (P _ n _) | n == reflm "Compute" = return Compute

1380reify _ (P _ n _) | n == reflm "Compute" = return Compute

1381+reify _ (P _ n _) | n == reflm "Skip" = return Skip

1379reify ist t@(App _ _)

1382reify ist t@(App _ _)

1380 | (P _ f _, args) <- unApply t = reifyApp ist f args

1383 | (P _ f _, args) <- unApply t = reifyApp ist f args

1381reify _ t = fail ("Unknown tactic " ++ show t)

1384reify _ t = fail ("Unknown tactic " ++ show t)

@@ -1416,6 +1419,15 @@ reifyApp ist t [n, tt', t']

1416 tt'' <- reifyTT tt'

1419 tt'' <- reifyTT tt'

1417 t'' <- reifyTT t'

1420 t'' <- reifyTT t'

1418 return $ LetTacTy n' (delab ist tt'') (delab ist t'')

1421 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''

1419reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

1431reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

1420

1432

1421-- | Reify terms from their reflected representation

1433-- | Reify terms from their reflected representation

@@ -2042,10 +2054,10 @@ reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

2042-- representation. Not in Idris or ElabD monads because it should be usable

2054-- representation. Not in Idris or ElabD monads because it should be usable

2043-- from either.

2055-- from either.

2044reifyReportPart :: Term -> Either Err ErrorReportPart

2056reifyReportPart :: 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" =

2046 Right (TextPart msg)

2058 Right (TextPart msg)

2047reifyReportPart (App (P (DCon _ _) n _) ttn)

2059reifyReportPart (App (P (DCon _ _) n _) ttn)

2048− | n == reflErrName "NamePart" =

2060+ | n == reflm "NamePart" =

2049 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of

2061 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of

2050 Error e -> Left . InternalMsg $

2062 Error e -> Left . InternalMsg $

2051 "could not reify name term " ++

2063 "could not reify name term " ++

@@ -2053,7 +2065,7 @@ reifyReportPart (App (P (DCon _ _) n _) ttn)

2053 " when reflecting an error:" ++ show e

2065 " when reflecting an error:" ++ show e

2054 OK (n', _)-> Right $ NamePart n'

2066 OK (n', _)-> Right $ NamePart n'

2055reifyReportPart (App (P (DCon _ _) n _) tm)

2067reifyReportPart (App (P (DCon _ _) n _) tm)

2056− | n == reflErrName "TermPart" =

2068+ | n == reflm "TermPart" =

2057 case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

2069 case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

2058 Error e -> Left . InternalMsg $

2070 Error e -> Left . InternalMsg $

2059 "could not reify reflected term " ++

2071 "could not reify reflected term " ++

@@ -2061,7 +2073,7 @@ reifyReportPart (App (P (DCon _ _) n _) tm)

2061 " when reflecting an error:" ++ show e

2073 " when reflecting an error:" ++ show e

2062 OK (tm', _) -> Right $ TermPart tm'

2074 OK (tm', _) -> Right $ TermPart tm'

2063reifyReportPart (App (P (DCon _ _) n _) tm)

2075reifyReportPart (App (P (DCon _ _) n _) tm)

2064− | n == reflErrName "SubReport" =

2076+ | n == reflm "SubReport" =

2065 case unList tm of

2077 case unList tm of

2066 Just xs -> do subParts <- mapM reifyReportPart xs

2078 Just xs -> do subParts <- mapM reifyReportPart xs

2067 Right (SubReport subParts)

2079 Right (SubReport subParts)

src/Idris/ParseExpr.hs+4

@@ -1278,6 +1278,10 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

1278 <|> do reserved "undo"; return Undo

1279 <|> do reserved "qed"; return Qed

1280 <|> 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]

1281 <|> do lchar ':';

1285 <|> do lchar ':';

1282 ( (do reserved "q"; return Abandon)

1286 ( (do reserved "q"; return Abandon)

1283 <|> (do (reserved "e" <|> reserved "eval");

1287 <|> (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