5ca9ef8 · Idris-dev · git.iko.soy

CHANGELOG+3

compare with master

unifiedsplit

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

1New in 0.9.14:

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

3+* Tactic for case analysis in proofs

4+* Induction and case tactic now work on expressions

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

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

4 --testpkg command-line option

6 --testpkg command-line option

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

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

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

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

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

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

8

10

11+

9New in 0.9.13:

12New in 0.9.13:

10--------------

13--------------

11* IDE support for retrieving structured information about metavariables

14* IDE support for retrieving structured information about metavariables

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

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

192 -- ^ focus a named hole

193 | Rewrite TT

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

195− | Induction TTName

195+ | Induction TT

196 -- ^ do induction on the particular expression

197+ | Case TT

198+ -- ^ do case analysis on particular expression

197 | LetTac TTName TT

199 | LetTac TTName TT

198 -- ^ name a reflected term

200 -- ^ name a reflected term

199 | LetTacTy TTName TT TT

201 | LetTacTy TTName TT TT

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

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

5import Prelude.Uninhabited

6

7||| Boolean Data Type

8−data Bool = False | True

8+%case data Bool = False | True

9

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

11||| @ b the condition on the if

src/Idris/AbsSyntaxTree.hs+5−3

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

485

486

487-- | Data declaration options

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

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

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

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

490 | DataErrRev

491 | DataErrRev

491 deriving (Show, Eq)

492 deriving (Show, Eq)

492

493

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

739

740

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

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

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

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

742− | Induction Name

743+ | Induction t

744+ | CaseTac t

743 | Equiv t

745 | Equiv t

744 | MatchRefine Name

746 | MatchRefine Name

745 | LetTac Name t | LetTacTy Name t t

747 | 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)

44 , ("reflect", Just ExprTArg)

45 , ("fill", Just ExprTArg)

46 , ("try", Just AltsTArg)

47− , ("induction", Just NameTArg)

47+ , ("induction", Just ExprTArg)

48+ , ("case", Just ExprTArg)

48 , (":t", Just ExprTArg)

49 , (":t", Just ExprTArg)

49 , (":type", Just ExprTArg)

50 , (":type", Just ExprTArg)

50 , (":e", Just ExprTArg)

51 , (":e", Just ExprTArg)

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

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

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

372rewrite tm = processTactic' (Rewrite tm)

373

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

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

375−induction nm = processTactic' (Induction nm)

375+induction tm = processTactic' (Induction tm)

376+

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

378+casetac tm = processTactic' (CaseTac tm)

376

379

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

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

378equiv tm = processTactic' (Equiv tm)

381equiv tm = processTactic' (Equiv tm)

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

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

72 | LetBind Name Raw Raw

73 | ExpandLet Name Term

74 | Rewrite Raw

75− | Induction Name

75+ | Induction Raw

76+ | CaseTac Raw

76 | Equiv Raw

77 | Equiv Raw

77 | PatVar Name

78 | PatVar Name

78 | PatBind Name

79 | PatBind Name

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

661 b { binderTy = ty' }

662 b { binderTy = ty' }

662mkP lt l r x = x

663mkP lt l r x = x

663

664

664−induction :: Name -> RunTactic

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

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

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

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

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

667 let tmt' = normalise ctxt env tmt

668 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")

668 case unApply tmt' of

672 case unApply tmt' of

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

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

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

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

671 [elimTy] -> do

675 [elimTy] -> do

672 param_pos <- case lookupMetaInformation tnm ctxt of

676 param_pos <- case lookupMetaInformation tnm ctxt of

673 [DataMI param_pos] -> return param_pos

677 [DataMI param_pos] -> return param_pos

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

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

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

684 let scr = last $ tail args'

688 let scr = last $ tail args'

685 let indxnames = makeIndexNames indicies

689 let indxnames = makeIndexNames indicies

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'

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

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

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

696 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)))

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

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

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

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

691 mapM_ addConsHole (reverse consargs')

700 mapM_ addConsHole (reverse consargs')

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

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

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

694 let scv' = specialise ctxt env [] scv

703 let scv' = specialise ctxt env [] scv

695 return scv'

704 return scv'

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

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

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

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

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

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

699 where scname = sMN 0 "scarg"

708 where scname = sMN 0 "scarg"

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

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

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

710 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

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

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

710 let var = P Bound idnm idxt

719 let var = P Bound idnm idxt

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

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

713

722

714

723

715equiv :: Raw -> RunTactic

724equiv :: Raw -> RunTactic

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

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

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

992 mktac (ExpandLet n b) = expandLet n b

1001 mktac (ExpandLet n b) = expandLet n b

993 mktac (Rewrite t) = rewrite t

1002 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

995 mktac (Equiv t) = equiv t

1005 mktac (Equiv t) = equiv t

996 mktac (PatVar n) = patvar n

1006 mktac (PatVar n) = patvar n

997 mktac (PatBind n) = patbind n

1007 mktac (PatBind n) = patbind n

src/Idris/DeepSeq.hs+2

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

119instance NFData DataOpt where

120 rnf Codata = ()

121 rnf DefaultEliminator = ()

122+ rnf DefaultCaseFun = ()

122

123

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

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

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

125 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

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

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

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

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

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

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

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

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

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

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

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

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

243 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)

283

284 -- create an eliminator

285 when (DefaultEliminator `elem` opts) $

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

287+ -- create a case function

288+ when (DefaultCaseFun `elem` opts) $

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

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

287 where

290 where

288 setDetaggable :: Name -> Idris ()

291 setDetaggable :: Name -> Idris ()

289 setDetaggable n = do

292 setDetaggable n = do

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

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

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

370

373

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

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

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

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

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

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

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

374 ElabInfo -> EliminatorState ()

379 ElabInfo -> EliminatorState ()

375−elabEliminator paramPos n ty cons info = do

380+elabCaseFun ind paramPos n ty cons info = do

376− elimLog $ "Elaborating eliminator"

381+ elimLog $ "Elaborating case function"

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

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

378 let (cnstrs, _) = splitPi ty

383 let (cnstrs, _) = splitPi ty

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

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

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

381 motiveIdxs <- namePis False idxs

386 motiveIdxs <- namePis False idxs

382 let motive = mkMotive n paramPos generalParams motiveIdxs

387 let motive = mkMotive n paramPos generalParams motiveIdxs

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

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

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

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

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

385 consTerm <- extractConsTerm c generalParams

391 consTerm <- extractConsTerm c generalParams

386 return (name, expl, consTerm)) cons

392 return (name, expl, consTerm)) cons

387 scrutineeIdxs <- namePis False idxs

393 scrutineeIdxs <- namePis False idxs

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

392 let clauseConsElimArgs = map getPiName consTerms

398 let clauseConsElimArgs = map getPiName consTerms

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

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

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

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

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

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

396 elimLog elimSig

402 elimLog elimSig

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

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

398 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

404 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

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

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

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

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

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

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

402 case eliminatorClauses of

408 case eliminatorClauses of

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

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

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

407

413

408 elimFC :: FC

414 elimFC :: FC

409− elimFC = fileFC "(eliminator)"

415+ elimFC = fileFC "(casefun)"

410

416

411 elimDeclName :: Name

417 elimDeclName :: Name

412− elimDeclName = SN $ ElimN n

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

413

419

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

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

415 applyNS n [] = n

421 applyNS n [] = n

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

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

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

561 consArgs <- namePis False args

567 consArgs <- namePis False args

562 let recArgs = findRecArgs consArgs

568 let recArgs = findRecArgs consArgs

563− let recMotives = map applyRecMotive recArgs

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

564 let (_, consIdxs) = splitArgPms resTy

570 let (_, consIdxs) = splitArgPms resTy

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

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

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

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

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

600 consArgs <- namePis False args

606 consArgs <- namePis False args

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

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

602 let recArgs = findRecArgs consArgs

608 let recArgs = findRecArgs consArgs

603− let recElims = map applyRecElim recArgs

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

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

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

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

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

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

612 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

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

957collectDeferred top t = return t

958

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+

959-- Running tactics directly

977-- Running tactics directly

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

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

961

979

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

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

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

1047 rewrite (Var letn)

1065 rewrite (Var letn)

1048 when autoSolve solveAll

1066 when autoSolve solveAll

1049− runT (Induction nm)

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

1050− = do induction nm

1068+ = case_ True autoSolve ist fn tm

1051− when autoSolve solveAll

1069+ runT (CaseTac tm)

1070+ = case_ False autoSolve ist fn tm

1052 runT (LetTac n tm)

1071 runT (LetTac n tm)

1053 = do attack

1072 = do attack

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

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

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

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

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

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

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

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

1235reifyApp _ 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')

1218reifyApp ist t [t']

1238reifyApp ist t [t']

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

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

1220reifyApp ist t [t']

1240reifyApp ist t [t']

src/Idris/IBC.hs+6

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

1264 Codata -> putWord8 0

1265 DefaultEliminator -> putWord8 1

1266 DataErrRev -> putWord8 2

1267+ DefaultCaseFun -> putWord8 3

1267 get = do i <- getWord8

1268 get = do i <- getWord8

1268 case i of

1269 case i of

1269 0 -> return Codata

1270 0 -> return Codata

1270 1 -> return DefaultEliminator

1271 1 -> return DefaultEliminator

1271 2 -> return DataErrRev

1272 2 -> return DataErrRev

1273+ 3 -> return DefaultCaseFun

1272

1274

1273instance Binary FnOpt where

1275instance Binary FnOpt where

1274 put x

1276 put x

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

1968 put x4

1970 put x4

1969 put x5

1971 put x5

1970 DoUnify -> putWord8 22

1972 DoUnify -> putWord8 22

1973+ CaseTac x1 -> do putWord8 23

1974+ put x1

1971 get

1975 get

1972 = do i <- getWord8

1976 = do i <- getWord8

1973 case i of

1977 case i of

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

2016 x5 <- get

2020 x5 <- get

2017 return (ProofSearch x1 x2 x3 x4 x5)

2021 return (ProofSearch x1 x2 x3 x4 x5)

2018 22 -> return DoUnify

2022 22 -> return DoUnify

2023+ 23 -> do x1 <- get

2024+ return (CaseTac x1)

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

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

2020

2026

2021

2027

src/Idris/IdrisDoc.hs+2−1

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

334extractPTactic (Focus n) = [n]

335extractPTactic (Refine n _) = [n]

336extractPTactic (Rewrite p) = extract p

337−extractPTactic (Induction n) = [n]

337+extractPTactic (Induction p) = extract p

338+extractPTactic (CaseTac p) = extract p

338extractPTactic (Equiv p) = extract p

339extractPTactic (Equiv p) = extract p

339extractPTactic (MatchRefine n) = [n]

340extractPTactic (MatchRefine n) = [n]

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

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

src/Idris/ParseData.hs+4−3

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

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

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

81

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

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

83DefaultEliminator ::= 'noelim'?

84 -}

85dataOpts :: DataOpts -> IdrisParser DataOpts

86dataOpts opts

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

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

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

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

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

89 <|> return opts

90 <|> return opts

90 <?> "data options"

91 <?> "data options"

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

129 let tyn = expandNS syn tyn_in

130 let tyn = expandNS syn tyn_in

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

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

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

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

133 let n = show tyn_in ++ " "

134 let n = show tyn_in ++ " "

134 let s = kw ++ n

135 let s = kw ++ n

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

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

src/Idris/ParseExpr.hs+7−2

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

1136 | 'refine' Name Imp+

1137 | 'mrefine' Name

1138 | 'rewrite' Expr

1139+ | 'induction' Expr

1139 | 'equiv' Expr

1140 | 'equiv' Expr

1140 | 'let' Name ':' Expr' '=' Expr

1141 | 'let' Name ':' Expr' '=' Expr

1141 | 'let' Name '=' Expr

1142 | 'let' Name '=' Expr

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

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

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

1184 i <- get

1185 i <- get

1185 return $ Rewrite (desugar syn i t)

1186 return $ Rewrite (desugar syn i t)

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

1188+ i <- get

1189+ return $ CaseTac (desugar syn i t)

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

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

1191+ i <- get

1187− return $ Induction nm

1192+ return $ Induction (desugar syn i t)

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

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

1189 i <- get

1194 i <- get

1190 return $ Equiv (desugar syn i t)

1195 return $ Equiv (desugar syn i t)