547fa6e · Idris-dev · git.iko.soy

CHANGELOG+3

@@ -1,11 +1,14 @@

11New in 0.9.14:

22--------------

3+* Tactic for case analysis in proofs

4+* Induction and case tactic now work on expressions

35* Support for running tests for a package with the tests section of .ipkg files and the

46 --testpkg command-line option

57* Clearly distinguish between type providers and postulate providers at the use site

68* Allow dependent function syntax to be overridden in dsl blocks, similarly to

79 functions and let. The keyword for this is "pi".

810

11+

912New in 0.9.13:

1013--------------

1114* IDE support for retrieving structured information about metavariables

libs/base/Language/Reflection.idr+3−1

@@ -192,8 +192,10 @@ data Tactic = Try Tactic Tactic

192192 -- ^ focus a named hole

193193 | Rewrite TT

194194 -- ^ rewrite using the reflected rep. of a equality proof

195− | Induction TTName

195+ | Induction TT

196196 -- ^ do induction on the particular expression

197+ | Case TT

198+ -- ^ do case analysis on particular expression

197199 | LetTac TTName TT

198200 -- ^ name a reflected term

199201 | LetTacTy TTName TT TT

libs/prelude/Prelude/Bool.idr+1−1

@@ -5,7 +5,7 @@ import Builtins

55import Prelude.Uninhabited

66

77||| Boolean Data Type

8−data Bool = False | True

8+%case data Bool = False | True

99

1010||| The underlying implementation of the if ... then ... else ... syntax

1111||| @ b the condition on the if

src/Idris/AbsSyntaxTree.hs+5−3

@@ -485,8 +485,9 @@ dictionary = elem Dictionary

485485

486486

487487-- | Data declaration options

488−data DataOpt = Codata -- Set if the the data-type is coinductive

489− | DefaultEliminator -- Set if an eliminator should be generated for data type

488+data DataOpt = Codata -- ^ Set if the the data-type is coinductive

489+ | DefaultEliminator -- ^ Set if an eliminator should be generated for data type

490+ | DefaultCaseFun -- ^ Set if a case function should be generated for data type

490491 | DataErrRev

491492 deriving (Show, Eq)

492493

@@ -739,7 +740,8 @@ mapPT f t = f (mpt t) where

739740

740741data PTactic' t = Intro [Name] | Intros | Focus Name

741742 | Refine Name [Bool] | Rewrite t | DoUnify

742− | Induction Name

743+ | Induction t

744+ | CaseTac t

743745 | Equiv t

744746 | MatchRefine Name

745747 | LetTac Name t | LetTacTy Name t t

src/Idris/Completion.hs+2−1

@@ -44,7 +44,8 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)

4444 , ("reflect", Just ExprTArg)

4545 , ("fill", Just ExprTArg)

4646 , ("try", Just AltsTArg)

47− , ("induction", Just NameTArg)

47+ , ("induction", Just ExprTArg)

48+ , ("case", Just ExprTArg)

4849 , (":t", Just ExprTArg)

4950 , (":type", Just ExprTArg)

5051 , (":e", Just ExprTArg)

src/Idris/Core/Elaborate.hs+5−2

@@ -371,8 +371,11 @@ expandLet n v = processTactic' (ExpandLet n v)

371371rewrite :: Raw -> Elab' aux ()

372372rewrite tm = processTactic' (Rewrite tm)

373373

374−induction :: Name -> Elab' aux ()

375−induction nm = processTactic' (Induction nm)

374+induction :: Raw -> Elab' aux ()

375+induction tm = processTactic' (Induction tm)

376+

377+casetac :: Raw -> Elab' aux ()

378+casetac tm = processTactic' (CaseTac tm)

376379

377380equiv :: Raw -> Elab' aux ()

378381equiv tm = processTactic' (Equiv tm)

src/Idris/Core/ProofState.hs+22−12

@@ -72,7 +72,8 @@ data Tactic = Attack

7272 | LetBind Name Raw Raw

7373 | ExpandLet Name Term

7474 | Rewrite Raw

75− | Induction Name

75+ | Induction Raw

76+ | CaseTac Raw

7677 | Equiv Raw

7778 | PatVar Name

7879 | PatBind Name

@@ -661,13 +662,16 @@ mkP lt l r (Bind n b sc)

661662 b { binderTy = ty' }

662663mkP lt l r x = x

663664

664−induction :: Name -> RunTactic

665−induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

666− (tmv, tmt) <- lift $ check ctxt env (Var nm)

665+casetac :: Raw -> Bool -> RunTactic

666+casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

667+ (tmv, tmt) <- lift $ check ctxt env tm

667668 let tmt' = normalise ctxt env tmt

669+ let (tacn, tacstr, tactt) = if induction

670+ then (ElimN, "an eliminator", "induction")

671+ else (CaseN, "a case function", "case analysis")

668672 case unApply tmt' of

669673 (P _ tnm _, tyargs) -> do

670− case lookupTy (SN (ElimN tnm)) ctxt of

674+ case lookupTy (SN (tacn tnm)) ctxt of

671675 [elimTy] -> do

672676 param_pos <- case lookupMetaInformation tnm ctxt of

673677 [DataMI param_pos] -> return param_pos

@@ -683,9 +687,14 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

683687 let indxargs = drop (length restargs - length indicies) $ restargs

684688 let scr = last $ tail args'

685689 let indxnames = makeIndexNames indicies

686− prop <- replaceIndicies indxnames indicies $ Bind nm (Lam tmt') t

690+ currentNames <- query $ allTTNames . pterm

691+ let tmnm = case tm of

692+ Var nm -> uniqueNameCtxt ctxt nm currentNames

693+ _ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames

694+ let tmvar = P Bound tmnm tmt'

695+ prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)

687696 consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (pterm ps)) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (pterm ps))) consargs)

688− let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0)))

697+ let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))

689698 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))

690699 action (\ps -> ps {holes = holes ps \\ [x]})

691700 mapM_ addConsHole (reverse consargs')

@@ -693,9 +702,9 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

693702 (scv, sct) <- lift $ check ctxt env res'

694703 let scv' = specialise ctxt env [] scv

695704 return scv'

696− [] -> fail $ "Induction needs an eliminator for " ++ show tnm

697− xs -> fail $ "Multiple definitions found when searching for the eliminator of " ++ show tnm

698− _ -> fail "Unkown type for induction"

705+ [] -> fail $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm

706+ xs -> fail $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm

707+ _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"

699708 where scname = sMN 0 "scarg"

700709 makeConsArg (nm, ty) = P Bound nm ty

701710 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

@@ -709,7 +718,7 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

709718 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)

710719 let var = P Bound idnm idxt

711720 return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs

712−induction tm ctxt env _ = do fail "Can't do induction here"

721+induction tm induction ctxt env _ = do fail "Can't do induction here"

713722

714723

715724equiv :: Raw -> RunTactic

@@ -991,7 +1000,8 @@ process t h = tactic (Just h) (mktac t)

9911000 mktac (LetBind n t v) = letbind n t v

9921001 mktac (ExpandLet n b) = expandLet n b

9931002 mktac (Rewrite t) = rewrite t

994− mktac (Induction t) = induction t

1003+ mktac (Induction t) = casetac t True

1004+ mktac (CaseTac t) = casetac t False

9951005 mktac (Equiv t) = equiv t

9961006 mktac (PatVar n) = patvar n

9971007 mktac (PatBind n) = patbind n

src/Idris/DeepSeq.hs+2

@@ -119,6 +119,7 @@ instance NFData FnOpt where

119119instance NFData DataOpt where

120120 rnf Codata = ()

121121 rnf DefaultEliminator = ()

122+ rnf DefaultCaseFun = ()

122123

123124instance (NFData t) => NFData (PDecl' t) where

124125 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

@@ -236,6 +237,7 @@ instance (NFData t) => NFData (PTactic' t) where

236237 rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

237238 rnf (Rewrite x1) = rnf x1 `seq` ()

238239 rnf (Induction x1) = rnf x1 `seq` ()

240+ rnf (CaseTac x1) = rnf x1 `seq` ()

239241 rnf (Equiv x1) = rnf x1 `seq` ()

240242 rnf (MatchRefine x1) = rnf x1 `seq` ()

241243 rnf (LetTac x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/ElabDecls.hs+17−11

@@ -283,7 +283,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

283283

284284 -- create an eliminator

285285 when (DefaultEliminator `elem` opts) $

286− evalStateT (elabEliminator params n t dcons info) Map.empty

286+ evalStateT (elabCaseFun True params n t dcons info) Map.empty

287+ -- create a case function

288+ when (DefaultCaseFun `elem` opts) $

289+ evalStateT (elabCaseFun False params n t dcons info) Map.empty

287290 where

288291 setDetaggable :: Name -> Idris ()

289292 setDetaggable n = do

@@ -369,11 +372,13 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

369372type EliminatorState = StateT (Map.Map String Int) Idris

370373

371374-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)

372−elabEliminator :: [Int] -> Name -> PTerm ->

375+-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function

376+-- rename to caseFun to match updated intend

377+elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->

373378 [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->

374379 ElabInfo -> EliminatorState ()

375−elabEliminator paramPos n ty cons info = do

376− elimLog $ "Elaborating eliminator"

380+elabCaseFun ind paramPos n ty cons info = do

381+ elimLog $ "Elaborating case function"

377382 put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

378383 let (cnstrs, _) = splitPi ty

379384 let (splittedTy@(pms, idxs)) = splitPms cnstrs

@@ -381,7 +386,8 @@ elabEliminator paramPos n ty cons info = do

381386 motiveIdxs <- namePis False idxs

382387 let motive = mkMotive n paramPos generalParams motiveIdxs

383388 consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do

384− name <- freshName $ "elim_" ++ simpleName cnm

389+ let casefunt = if ind then "elim_" else "case_"

390+ name <- freshName $ casefunt ++ simpleName cnm

385391 consTerm <- extractConsTerm c generalParams

386392 return (name, expl, consTerm)) cons

387393 scrutineeIdxs <- namePis False idxs

@@ -392,11 +398,11 @@ elabEliminator paramPos n ty cons info = do

392398 let clauseConsElimArgs = map getPiName consTerms

393399 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

394400 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

395− let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy

401+ let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy

396402 elimLog elimSig

397403 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

398404 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

399− elimLog $ "-- eliminator definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

405+ elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

400406 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

401407 -- Do not elaborate clauses if there aren't any

402408 case eliminatorClauses of

@@ -406,10 +412,10 @@ elabEliminator paramPos n ty cons info = do

406412 elimLog s = State.lift (logLvl 2 s)

407413

408414 elimFC :: FC

409− elimFC = fileFC "(eliminator)"

415+ elimFC = fileFC "(casefun)"

410416

411417 elimDeclName :: Name

412− elimDeclName = SN $ ElimN n

418+ elimDeclName = if ind then SN . ElimN $ n else SN . CaseN $ n

413419

414420 applyNS :: Name -> [String] -> Name

415421 applyNS n [] = n

@@ -560,7 +566,7 @@ elabEliminator paramPos n ty cons info = do

560566 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

561567 consArgs <- namePis False args

562568 let recArgs = findRecArgs consArgs

563− let recMotives = map applyRecMotive recArgs

569+ let recMotives = if ind then map applyRecMotive recArgs else []

564570 let (_, consIdxs) = splitArgPms resTy

565571 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))

566572 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)

@@ -600,7 +606,7 @@ elabEliminator paramPos n ty cons info = do

600606 consArgs <- namePis False args

601607 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])

602608 let recArgs = findRecArgs consArgs

603− let recElims = map applyRecElim recArgs

609+ let recElims = if ind then map applyRecElim recArgs else []

604610 let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)

605611 return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []

606612 where applyRecElim :: (Name, Plicity, PTerm) -> PArg

src/Idris/ElabTerm.hs+24−4

@@ -956,6 +956,24 @@ collectDeferred top (Bind n b t) = do b' <- cdb b

956956collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)

957957collectDeferred top t = return t

958958

959+case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

960+case_ ind autoSolve ist fn tm = do

961+ attack

962+ tyn <- getNameFrom (sMN 0 "ity")

963+ claim tyn RType

964+ valn <- getNameFrom (sMN 0 "ival")

965+ claim valn (Var tyn)

966+ letn <- getNameFrom (sMN 0 "irule")

967+ letbind letn (Var tyn) (Var valn)

968+ focus valn

969+ elab ist toplevel False [] (sMN 0 "tac") tm

970+ env <- get_env

971+ let (Just binding) = lookup letn env

972+ let val = binderVal binding

973+ if ind then induction (forget val)

974+ else casetac (forget val)

975+ when autoSolve solveAll

976+

959977-- Running tactics directly

960978-- if a tactic adds unification problems, return an error

961979

@@ -1046,9 +1064,10 @@ runTac autoSolve ist fn tac

10461064 elab ist toplevel False [] (sMN 0 "tac") tm

10471065 rewrite (Var letn)

10481066 when autoSolve solveAll

1049− runT (Induction nm)

1050− = do induction nm

1051− when autoSolve solveAll

1067+ runT (Induction tm) -- let bind tm, similar to the others

1068+ = case_ True autoSolve ist fn tm

1069+ runT (CaseTac tm)

1070+ = case_ False autoSolve ist fn tm

10521071 runT (LetTac n tm)

10531072 = do attack

10541073 tyn <- getNameFrom (sMN 0 "letty")

@@ -1214,7 +1233,8 @@ reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist

12141233reifyApp ist t [Constant (Str n), x]

12151234 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

12161235reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)

1217−reifyApp _ t [n] | t == reflm "Induction" = liftM Induction (reifyTTName n)

1236+reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')

1237+reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')

12181238reifyApp ist t [t']

12191239 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

12201240reifyApp ist t [t']

src/Idris/IBC.hs+6

@@ -1264,11 +1264,13 @@ instance Binary DataOpt where

12641264 Codata -> putWord8 0

12651265 DefaultEliminator -> putWord8 1

12661266 DataErrRev -> putWord8 2

1267+ DefaultCaseFun -> putWord8 3

12671268 get = do i <- getWord8

12681269 case i of

12691270 0 -> return Codata

12701271 1 -> return DefaultEliminator

12711272 2 -> return DataErrRev

1273+ 3 -> return DefaultCaseFun

12721274

12731275instance Binary FnOpt where

12741276 put x

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

19681970 put x4

19691971 put x5

19701972 DoUnify -> putWord8 22

1973+ CaseTac x1 -> do putWord8 23

1974+ put x1

19711975 get

19721976 = do i <- getWord8

19731977 case i of

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

20162020 x5 <- get

20172021 return (ProofSearch x1 x2 x3 x4 x5)

20182022 22 -> return DoUnify

2023+ 23 -> do x1 <- get

2024+ return (CaseTac x1)

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

20202026

20212027

src/Idris/IdrisDoc.hs+2−1

@@ -334,7 +334,8 @@ extractPTactic (Intro ns) = ns

334334extractPTactic (Focus n) = [n]

335335extractPTactic (Refine n _) = [n]

336336extractPTactic (Rewrite p) = extract p

337−extractPTactic (Induction n) = [n]

337+extractPTactic (Induction p) = extract p

338+extractPTactic (CaseTac p) = extract p

338339extractPTactic (Equiv p) = extract p

339340extractPTactic (MatchRefine n) = [n]

340341extractPTactic (LetTac n p) = n : extract p

src/Idris/ParseData.hs+4−3

@@ -79,12 +79,13 @@ dataI :: IdrisParser DataOpts

7979dataI = do reserved "data"; return []

8080 <|> do reserved "codata"; return [Codata]

8181

82−{- | Parses if a data should not have a default eliminator

82+{- | Parses if a data should not have a default eliminator

8383DefaultEliminator ::= 'noelim'?

8484 -}

8585dataOpts :: DataOpts -> IdrisParser DataOpts

8686dataOpts opts

87− = do reserved "%elim"; dataOpts (DefaultEliminator : opts)

87+ = do reserved "%elim"; dataOpts (DefaultEliminator : DefaultCaseFun : opts)

88+ <|> do reserved "%case"; dataOpts (DefaultCaseFun : opts)

8889 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

8990 <|> return opts

9091 <?> "data options"

@@ -129,7 +130,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

129130 let tyn = expandNS syn tyn_in

130131 option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do

131132 try (lchar '=') <|> do reserved "where"

132− let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

133+ let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

133134 let n = show tyn_in ++ " "

134135 let s = kw ++ n

135136 let as = concat (intersperse " " $ map show args) ++ " "

src/Idris/ParseExpr.hs+7−2

@@ -1136,6 +1136,7 @@ Tactic ::= 'intro' NameList?

11361136 | 'refine' Name Imp+

11371137 | 'mrefine' Name

11381138 | 'rewrite' Expr

1139+ | 'induction' Expr

11391140 | 'equiv' Expr

11401141 | 'let' Name ':' Expr' '=' Expr

11411142 | 'let' Name '=' Expr

@@ -1183,8 +1184,12 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

11831184 <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);

11841185 i <- get

11851186 return $ Rewrite (desugar syn i t)

1186− <|> do reserved "induction"; nm <- (indentPropHolds gtProp *> fnName);

1187− return $ Induction nm

1187+ <|> do reserved "case"; t <- (indentPropHolds gtProp *> expr syn);

1188+ i <- get

1189+ return $ CaseTac (desugar syn i t)

1190+ <|> do reserved "induction"; t <- (indentPropHolds gtProp *> expr syn);

1191+ i <- get

1192+ return $ Induction (desugar syn i t)

11881193 <|> do reserved "equiv"; t <- (indentPropHolds gtProp *> expr syn);

11891194 i <- get

11901195 return $ Equiv (desugar syn i t)