7cbf0cb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #713 from ahmadsalim/feature/inductiontactic

Added support for induction tactic (works only for nonparameterized types insofar, requires eliminator for type)

commit7cbf0cbcb38c763641b0215bd3723ba80f3a130f authorEdwin Brady <edwin.brady@gmail.com> dateWed 11 Dec 2013, 13:22 (13 years ago) parent15ed733 86e32fb

10 files changed+82−27

compare with master

unifiedsplit

libs/base/Language/Reflection.idr+2 src/Core/Elaborate.hs+3 src/Core/ProofState.hs+57−20 src/Core/TT.hs+1 src/Idris/AbsSyntaxTree.hs+2 src/Idris/DeepSeq.hs+1 src/Idris/ElabDecls.hs+6−6 src/Idris/ElabTerm.hs+3 src/Idris/IBC.hs+5−1 src/Idris/ParseExpr.hs+2

libs/base/Language/Reflection.idr+2

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

177177 -- ^ focus a named hole

178178 | Rewrite TT

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

180+ | Induction TTName

181+ -- ^ do induction on the particular expression

180182 | LetTac TTName TT

181183 -- ^ name a reflected term

182184 | LetTacTy TTName TT TT

src/Core/Elaborate.hs+3

@@ -305,6 +305,9 @@ expandLet n v = processTactic' (ExpandLet n v)

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

306306rewrite tm = processTactic' (Rewrite tm)

307307

308+induction :: Name -> Elab' aux ()

309+induction nm = processTactic' (Induction nm)

310+

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

309312equiv tm = processTactic' (Equiv tm)

310313

src/Core/ProofState.hs+57−20

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

6969 | LetBind Name Raw Raw

7070 | ExpandLet Name Term

7171 | Rewrite Raw

72+ | Induction Name

7273 | Equiv Raw

7374 | PatVar Name

7475 | PatBind Name

@@ -566,28 +567,63 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

566567 (scv, sct) <- lift $ check ctxt env sc

567568 return scv

568569 _ -> fail "Not an equality type"

569− where

570− -- to make the P for rewrite, replace syntactic occurrences of l in ty with

571− -- an x, and put \x : lt in front

572− mkP lt l r ty | l == ty = lt

573− mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f

574− a' = if (r /= a) then mkP lt l r a else a in

575− App f' a'

576− mkP lt l r (Bind n b sc)

577− = let b' = mkPB b

578− sc' = if (r /= sc) then mkP lt l r sc else sc in

579− Bind n b' sc'

580− where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t

581− v' = if (r /= v) then mkP lt l r v else v in

582− Let t' v'

583− mkPB b = let ty = binderTy b

584− ty' = if (r /= ty) then mkP lt l r ty else ty in

585− b { binderTy = ty' }

586− mkP lt l r x = x

587−

588− rname = MN 0 "replaced"

570+ where rname = MN 0 "replaced"

589571rewrite _ _ _ _ = fail "Can't rewrite here"

590572

573+-- To make the P for rewrite, replace syntactic occurrences of l in ty with

574+-- an x, and put \x : lt in front

575+mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name

576+mkP lt l r ty | l == ty = lt

577+mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f

578+ a' = if (r /= a) then mkP lt l r a else a in

579+ App f' a'

580+mkP lt l r (Bind n b sc)

581+ = let b' = mkPB b

582+ sc' = if (r /= sc) then mkP lt l r sc else sc in

583+ Bind n b' sc'

584+ where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t

585+ v' = if (r /= v) then mkP lt l r v else v in

586+ Let t' v'

587+ mkPB b = let ty = binderTy b

588+ ty' = if (r /= ty) then mkP lt l r ty else ty in

589+ b { binderTy = ty' }

590+mkP lt l r x = x

591+

592+induction :: Name -> RunTactic

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

594+ (tmv, tmt) <- lift $ check ctxt env (Var nm)

595+ let tmt' = normalise ctxt env tmt

596+ case unApply tmt' of

597+ (P _ tnm _, pms@[]) -> do

598+ case lookupTy (SN (ElimN tnm)) ctxt of

599+ [elimTy] -> do

600+ let args = getArgTys elimTy

601+ let pmargs = take (length pms) args -- TODO: Fill these correctly when having multiple parameters working

602+ let args' = drop (length pms) args

603+ let propTy = head args'

604+ let consargs = init $ tail args -- TODO: This is incorrect when type has indicies, get indicies and use the correct count

605+ let scr = last $ tail args

606+ let prop = Bind nm (Lam tmt') t -- TODO: Make this work for types with indicies

607+ let res = substV prop $ bindConsArgs consargs (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0))) ([prop] ++ map makeConsArg consargs ++ [tmv]))

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

609+ mapM_ addConsHole (reverse consargs)

610+ let res' = forget $ res

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

612+ let scv' = specialise ctxt env [] scv

613+ return scv'

614+ [] -> fail $ "Induction needs an eliminator for " ++ show nm

615+ xs -> fail $ "Multiple definitions found when searching for the eliminator of " ++ show nm

616+ (P _ nm _, _) -> fail "Induction not yet supported for types with arguments"

617+ _ -> fail "Unkown type for induction"

618+ where scname = MN 0 "scarg"

619+ makeConsArg (nm, ty) = P Bound nm ty

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

621+ bindConsArgs [] v = v

622+ addConsHole (nm, ty) =

623+ action (\ps -> ps { holes = nm : holes ps })

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

625+

626+

591627equiv :: Raw -> RunTactic

592628equiv tm ctxt env (Bind x (Hole t) sc) =

593629 do (tmv, tmt) <- lift $ check ctxt env tm

@@ -819,6 +855,7 @@ process t h = tactic (Just h) (mktac t)

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

820856 mktac (ExpandLet n b) = expandLet n b

821857 mktac (Rewrite t) = rewrite t

858+ mktac (Induction t) = induction t

822859 mktac (Equiv t) = equiv t

823860 mktac (PatVar n) = patvar n

824861 mktac (PatBind n) = patbind n

src/Core/TT.hs+1

@@ -285,6 +285,7 @@ showCG (SN s) = showCG' s

285285 showCG' (MethodN m) = '!':showCG m

286286 showCG' (ParentN p c) = showCG p ++ "#" ++ show c

287287 showCG' (CaseN c) = showCG c ++ "_case"

288+ showCG' (ElimN sn) = showCG sn ++ "_elim"

288289showCG NErased = "_"

289290

290291

src/Idris/AbsSyntaxTree.hs+2

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

638638

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

640640 | Refine Name [Bool] | Rewrite t

641+ | Induction Name

641642 | Equiv t

642643 | MatchRefine Name

643644 | LetTac Name t | LetTacTy Name t t

@@ -665,6 +666,7 @@ instance Sized a => Sized (PTactic' a) where

665666 size (Focus nm) = 1 + size nm

666667 size (Refine nm bs) = 1 + size nm + length bs

667668 size (Rewrite t) = 1 + size t

669+ size (Induction t) = 1 + size t

668670 size (LetTac nm t) = 1 + size nm + size t

669671 size (Exact t) = 1 + size t

670672 size Compute = 1

src/Idris/DeepSeq.hs+1

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

276276 rnf (Focus x1) = rnf x1 `seq` ()

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

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

279+ rnf (Induction x1) = rnf x1 `seq` ()

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

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

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

src/Idris/ElabDecls.hs+6−6

@@ -359,18 +359,18 @@ elabEliminator paramPos n ty cons info = do

359359 freshName key = do

360360 nameMap <- get

361361 let i = fromMaybe 0 (Map.lookup key nameMap)

362− let name = key ++ show i ++ "__"

362+ let name = key ++ show i

363363 put $ Map.insert key (i+1) nameMap

364− return (MN i name)

364+ return (UN name)

365365

366366 scrutineeName :: Name

367− scrutineeName = MN 0 "scrutinee"

367+ scrutineeName = UN "scrutinee"

368368

369369 scrutineeArgName :: Name

370− scrutineeArgName = MN 0 "scrutineeArg"

370+ scrutineeArgName = UN "scrutineeArg"

371371

372372 motiveName :: Name

373− motiveName = MN 0 "prop"

373+ motiveName = UN "prop"

374374

375375 mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm

376376 mkMotive n paramPos params indicies =

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

460460 let (_, consIdxs) = splitArgPms resTy

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

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

463− applyRecMotive (n,_,ty) = (MN 0 $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))

463+ applyRecMotive (n,_,ty) = (UN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))

464464 where (_, idxs) = splitArgPms ty

465465

466466 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]

src/Idris/ElabTerm.hs+3

@@ -840,6 +840,9 @@ runTac autoSolve ist tac

840840 elab ist toplevel False False (MN 0 "tac") tm

841841 rewrite (Var letn)

842842 when autoSolve solveAll

843+ runT (Induction nm)

844+ = do induction nm

845+ when autoSolve solveAll

843846 runT (LetTac n tm)

844847 = do attack

845848 tyn <- unique_hole (MN 0 "letty")

src/Idris/IBC.hs+5−1

@@ -23,7 +23,7 @@ import Debug.Trace

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 46

26+ibcVersion = 47

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

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

15971597 put x1

15981598 Fill x1 -> do putWord8 18

15991599 put x1

1600+ Induction x1 -> do putWord8 19

1601+ put x1

16001602 get

16011603 = do i <- getWord8

16021604 case i of

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

16341636 return (Reflect x1)

16351637 18 -> do x1 <- get

16361638 return (Fill x1)

1639+ 19 -> do x1 <- get

1640+ return (Induction x1)

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

16381642

16391643

src/Idris/ParseExpr.hs+2

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

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

10751075 i <- get

10761076 return $ Rewrite (desugar syn i t)

1077+ <|> do reserved "induction"; nm <- (indentPropHolds gtProp *> name);

1078+ return $ Induction nm

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

10781080 i <- get

10791081 return $ Equiv (desugar syn i t)