a0b05e2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow induction on terms instead of simply names

commita0b05e23cc590f92bfa3c32f6e5e68647cc8408c authorAhmad Salim Al-Sibahi <asal@itu.dk> dateMon 9 Jun 2014, 12:08 (12 years ago) parentdcd9568

7 files changed+34−15

compare with master

unifiedsplit

libs/base/Language/Reflection.idr+1−1 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/Core/Elaborate.hs+2−2 src/Idris/Core/ProofState.hs+10−5 src/Idris/ElabTerm.hs+15−3 src/Idris/IdrisDoc.hs+1−1 src/Idris/ParseExpr.hs+4−2

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

@@ -192,7 +192,7 @@ 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

197197 | LetTac TTName TT

198198 -- ^ name a reflected term

src/Idris/AbsSyntaxTree.hs+1−1

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

737737

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

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

740− | Induction Name

740+ | Induction t

741741 | Equiv t

742742 | MatchRefine Name

743743 | LetTac Name t | LetTacTy Name t t

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

@@ -371,8 +371,8 @@ 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)

376376

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

378378equiv tm = processTactic' (Equiv tm)

src/Idris/Core/ProofState.hs+10−5

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

7272 | LetBind Name Raw Raw

7373 | ExpandLet Name Term

7474 | Rewrite Raw

75− | Induction Name

75+ | Induction Raw

7676 | Equiv Raw

7777 | PatVar Name

7878 | PatBind Name

@@ -661,9 +661,9 @@ mkP lt l r (Bind n b sc)

661661 b { binderTy = ty' }

662662mkP lt l r x = x

663663

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)

664+induction :: Raw -> RunTactic

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

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

667667 let tmt' = normalise ctxt env tmt

668668 case unApply tmt' of

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

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

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

684684 let scr = last $ tail args'

685685 let indxnames = makeIndexNames indicies

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

686+ currentNames <- query $ allTTNames . pterm

687+ let tmnm = case tm of

688+ Var nm -> uniqueNameCtxt ctxt nm currentNames

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

690+ let tmvar = P Bound tmnm tmt'

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

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

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

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

src/Idris/ElabTerm.hs+15−3

@@ -1046,8 +1046,20 @@ runTac autoSolve ist fn tac

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

10471047 rewrite (Var letn)

10481048 when autoSolve solveAll

1049− runT (Induction nm)

1050− = do induction nm

1049+ 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)

10511063 when autoSolve solveAll

10521064 runT (LetTac n tm)

10531065 = do attack

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

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

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

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

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

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

12181230reifyApp ist t [t']

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

12201232reifyApp ist t [t']

src/Idris/IdrisDoc.hs+1−1

@@ -334,7 +334,7 @@ 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

338338extractPTactic (Equiv p) = extract p

339339extractPTactic (MatchRefine n) = [n]

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

src/Idris/ParseExpr.hs+4−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,9 @@ 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 "induction"; t <- (indentPropHolds gtProp *> expr syn);

1188+ i <- get

1189+ return $ Induction (desugar syn i t)

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

11891191 i <- get

11901192 return $ Equiv (desugar syn i t)