a0b05e2 · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

198 -- ^ name a reflected term

src/Idris/AbsSyntaxTree.hs+1−1

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

737

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

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

740− | Induction Name

740+ | Induction t

741 | Equiv t

742 | MatchRefine Name

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

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

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

378equiv tm = processTactic' (Equiv tm)

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

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

72 | LetBind Name Raw Raw

73 | ExpandLet Name Term

74 | Rewrite Raw

75− | Induction Name

75+ | Induction Raw

76 | Equiv Raw

77 | PatVar Name

78 | PatBind Name

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

661 b { binderTy = ty' }

662mkP lt l r x = x

663

664−induction :: Name -> RunTactic

664+induction :: Raw -> RunTactic

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

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

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

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

667 let tmt' = normalise ctxt env tmt

668 case unApply tmt' of

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

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

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

684 let scr = last $ tail args'

685 let indxnames = makeIndexNames indicies

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'

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

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

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

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

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

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

src/Idris/ElabTerm.hs+15−3

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

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

1047 rewrite (Var letn)

1048 when autoSolve solveAll

1049− runT (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

1050− = do induction nm

1062+ induction (forget val)

1051 when autoSolve solveAll

1063 when autoSolve solveAll

1052 runT (LetTac n tm)

1064 runT (LetTac n tm)

1053 = do attack

1065 = do attack

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

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

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

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

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

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

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

1218reifyApp ist t [t']

1230reifyApp ist t [t']

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

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

1220reifyApp ist t [t']

1232reifyApp ist t [t']

src/Idris/IdrisDoc.hs+1−1

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

338extractPTactic (Equiv p) = extract p

339extractPTactic (MatchRefine n) = [n]

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

src/Idris/ParseExpr.hs+4−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,9 @@ 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)

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

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

1188+ i <- get

1187− return $ Induction nm

1189+ return $ Induction (desugar syn i t)

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

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

1189 i <- get

1191 i <- get

1190 return $ Equiv (desugar syn i t)

1192 return $ Equiv (desugar syn i t)