5045dae · Idris-dev · git.iko.soy

libs/base/Language/Reflection.idr+2

@@ -194,6 +194,8 @@ data Tactic = Try Tactic Tactic

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

195195 | 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+4−2

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

484484

485485

486486-- | Data declaration options

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

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

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

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

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

489490 | DataErrRev

490491 deriving (Show, Eq)

491492

@@ -738,6 +739,7 @@ mapPT f t = f (mpt t) where

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

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

740741 | Induction t

742+ | CaseTac t

741743 | Equiv t

742744 | MatchRefine Name

743745 | LetTac Name t | LetTacTy Name t t

src/Idris/Core/Elaborate.hs+3

@@ -374,6 +374,9 @@ rewrite tm = processTactic' (Rewrite tm)

374374induction :: Raw -> Elab' aux ()

375375induction tm = processTactic' (Induction tm)

376376

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

378+casetac tm = processTactic' (CaseTac tm)

379+

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

378381equiv tm = processTactic' (Equiv tm)

379382

src/Idris/Core/ProofState.hs+14−9

@@ -73,6 +73,7 @@ data Tactic = Attack

7373 | ExpandLet Name Term

7474 | Rewrite Raw

7575 | 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 :: Raw -> RunTactic

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

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

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

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

@@ -690,7 +694,7 @@ induction tm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

690694 let tmvar = P Bound tmnm tmt'

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

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

693− 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)))

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

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

696700 mapM_ addConsHole (reverse consargs')

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

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

699703 let scv' = specialise ctxt env [] scv

700704 return scv'

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

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

703− _ -> 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"

704708 where scname = sMN 0 "scarg"

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

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

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

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

715719 let var = P Bound idnm idxt

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

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

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

718722

719723

720724equiv :: Raw -> RunTactic

@@ -992,7 +996,8 @@ process t h = tactic (Just h) (mktac t)

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

993997 mktac (ExpandLet n b) = expandLet n b

994998 mktac (Rewrite t) = rewrite t

995− mktac (Induction t) = induction t

999+ mktac (Induction t) = casetac t True

1000+ mktac (CaseTac t) = casetac t False

9961001 mktac (Equiv t) = equiv t

9971002 mktac (PatVar n) = patvar n

9981003 mktac (PatBind n) = patbind n

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+21−14

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

@@ -1047,20 +1065,9 @@ runTac autoSolve ist fn tac

10471065 rewrite (Var letn)

10481066 when autoSolve solveAll

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

1050− = do attack

1051− tyn <- getNameFrom (sMN 0 "ity")

1052− claim tyn RType

1053− valn <- getNameFrom (sMN 0 "ival")

1054− claim valn (Var tyn)

1055− letn <- getNameFrom (sMN 0 "irule")

1056− letbind letn (Var tyn) (Var valn)

1057− focus valn

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

1059− env <- get_env

1060− let (Just binding) = lookup letn env

1061− let val = binderVal binding

1062− induction (forget val)

1063− when autoSolve solveAll

1068+ = case_ True autoSolve ist fn tm

1069+ runT (CaseTac tm)

1070+ = case_ False autoSolve ist fn tm

10641071 runT (LetTac n tm)

10651072 = do attack

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

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/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+3

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

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

11851185 i <- get

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

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

11881191 i <- get

11891192 return $ Induction (desugar syn i t)