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

libs/base/Language/Reflection.idr+2

compare with master

unifiedsplit

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

177 -- ^ focus a named hole

178 | Rewrite TT

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

180+ | Induction TTName

181+ -- ^ do induction on the particular expression

180 | LetTac TTName TT

182 | LetTac TTName TT

181 -- ^ name a reflected term

183 -- ^ name a reflected term

182 | LetTacTy TTName TT TT

184 | LetTacTy TTName TT TT

src/Core/Elaborate.hs+3

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

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

306rewrite tm = processTactic' (Rewrite tm)

307

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

309+induction nm = processTactic' (Induction nm)

310+

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

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

309equiv tm = processTactic' (Equiv tm)

312equiv tm = processTactic' (Equiv tm)

310

313

src/Core/ProofState.hs+57−20

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

69 | LetBind Name Raw Raw

70 | ExpandLet Name Term

71 | Rewrite Raw

72+ | Induction Name

72 | Equiv Raw

73 | Equiv Raw

73 | PatVar Name

74 | PatVar Name

74 | PatBind Name

75 | PatBind Name

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

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

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

567 return scv

568 return scv

568 _ -> fail "Not an equality type"

569 _ -> 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"

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

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

590

572

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+

591equiv :: Raw -> RunTactic

627equiv :: Raw -> RunTactic

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

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

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

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

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

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

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

820 mktac (ExpandLet n b) = expandLet n b

856 mktac (ExpandLet n b) = expandLet n b

821 mktac (Rewrite t) = rewrite t

857 mktac (Rewrite t) = rewrite t

858+ mktac (Induction t) = induction t

822 mktac (Equiv t) = equiv t

859 mktac (Equiv t) = equiv t

823 mktac (PatVar n) = patvar n

860 mktac (PatVar n) = patvar n

824 mktac (PatBind n) = patbind n

861 mktac (PatBind n) = patbind n

src/Core/TT.hs+1

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

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

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

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

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

288showCG NErased = "_"

289showCG NErased = "_"

289

290

291

src/Idris/AbsSyntaxTree.hs+2

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

638

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

640 | Refine Name [Bool] | Rewrite t

641+ | Induction Name

641 | Equiv t

642 | Equiv t

642 | MatchRefine Name

643 | MatchRefine Name

643 | LetTac Name t | LetTacTy Name t t

644 | LetTac Name t | LetTacTy Name t t

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

665 size (Focus nm) = 1 + size nm

666 size (Focus nm) = 1 + size nm

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

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

667 size (Rewrite t) = 1 + size t

668 size (Rewrite t) = 1 + size t

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

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

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

669 size (Exact t) = 1 + size t

671 size (Exact t) = 1 + size t

670 size Compute = 1

672 size Compute = 1

src/Idris/DeepSeq.hs+1

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

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

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

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

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

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

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

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

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

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

282 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

359 freshName key = do

360 nameMap <- get

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

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

362+ let name = key ++ show i

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

364− return (MN i name)

364+ return (UN name)

365

366 scrutineeName :: Name

367− scrutineeName = MN 0 "scrutinee"

367+ scrutineeName = UN "scrutinee"

368

369 scrutineeArgName :: Name

370− scrutineeArgName = MN 0 "scrutineeArg"

370+ scrutineeArgName = UN "scrutineeArg"

371

372 motiveName :: Name

373− motiveName = MN 0 "prop"

373+ motiveName = UN "prop"

374

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

376 mkMotive n paramPos params indicies =

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

460 let (_, consIdxs) = splitArgPms resTy

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

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

464 where (_, idxs) = splitArgPms ty

465

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

src/Idris/ElabTerm.hs+3

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

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

841 rewrite (Var letn)

842 when autoSolve solveAll

843+ runT (Induction nm)

844+ = do induction nm

845+ when autoSolve solveAll

843 runT (LetTac n tm)

846 runT (LetTac n tm)

844 = do attack

847 = do attack

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

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

src/Idris/IBC.hs+5−1

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

23import Paths_idris

24

25ibcVersion :: Word8

26−ibcVersion = 46

26+ibcVersion = 47

27

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

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

1597 put x1

1598 Fill x1 -> do putWord8 18

1599 put x1

1600+ Induction x1 -> do putWord8 19

1601+ put x1

1600 get

1602 get

1601 = do i <- getWord8

1603 = do i <- getWord8

1602 case i of

1604 case i of

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

1634 return (Reflect x1)

1636 return (Reflect x1)

1635 18 -> do x1 <- get

1637 18 -> do x1 <- get

1636 return (Fill x1)

1638 return (Fill x1)

1639+ 19 -> do x1 <- get

1640+ return (Induction x1)

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

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

1638

1642

1639

1643

src/Idris/ParseExpr.hs+2

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

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

1075 i <- get

1076 return $ Rewrite (desugar syn i t)

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

1078+ return $ Induction nm

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

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

1078 i <- get

1080 i <- get

1079 return $ Equiv (desugar syn i t)

1081 return $ Equiv (desugar syn i t)