3448469 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add "equiv" tactic

"equiv t" asserts that the current goal has a type equivalent (by conversion) to t

commit3448469f29272137f60ef715e912671c01c2f9be authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 9 Jul 2013, 11:08 (13 years ago) parent62a3eba

5 files changed+28

compare with master

unifiedsplit

src/Core/Elaborate.hs+3 src/Core/ProofState.hs+9 src/Idris/AbsSyntaxTree.hs+1 src/Idris/ElabTerm.hs+12 src/Idris/Parser.hs+3

src/Core/Elaborate.hs+3

@@ -287,6 +287,9 @@ letbind n t v = processTactic' (LetBind n t v)

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

288288rewrite tm = processTactic' (Rewrite tm)

289289

290+equiv :: Raw -> Elab' aux ()

291+equiv tm = processTactic' (Equiv tm)

292+

290293patvar :: Name -> Elab' aux ()

291294patvar n = do env <- get_env

292295 if (n `elem` map fst env) then do apply (Var n) []; solve

src/Core/ProofState.hs+9

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

6666 | Forall Name Raw

6767 | LetBind Name Raw Raw

6868 | Rewrite Raw

69+ | Equiv Raw

6970 | PatVar Name

7071 | PatBind Name

7172 | Focus Name

@@ -539,6 +540,13 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

539540 rname = MN 0 "replaced"

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

541542

543+equiv :: Raw -> RunTactic

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

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

546+ lift $ converts ctxt env tmv t

547+ return $ Bind x (Hole tmv) sc

548+equiv tm ctxt env _ = fail "Can't equiv here"

549+

542550patbind :: Name -> RunTactic

543551patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

544552 do let t' = case t of

@@ -724,6 +732,7 @@ process t h = tactic (Just h) (mktac t)

724732 mktac (Forall n t) = forall n t

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

726734 mktac (Rewrite t) = rewrite t

735+ mktac (Equiv t) = equiv t

727736 mktac (PatVar n) = patvar n

728737 mktac (PatBind n) = patbind n

729738 mktac (CheckIn r) = check_in r

src/Idris/AbsSyntaxTree.hs+1

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

557557

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

559559 | Refine Name [Bool] | Rewrite t

560+ | Equiv t

560561 | MatchRefine Name

561562 | LetTac Name t | LetTacTy Name t t

562563 | Exact t | Compute | Trivial

src/Idris/ElabTerm.hs+12

@@ -769,6 +769,18 @@ runTac autoSolve ist tac

769769 _ -> return []

770770 runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)

771771 when autoSolve solveAll

772+ runT (Equiv tm) -- let bind tm, then

773+ = do attack

774+ tyn <- unique_hole (MN 0 "ety")

775+ claim tyn RType

776+ valn <- unique_hole (MN 0 "eqval")

777+ claim valn (Var tyn)

778+ letn <- unique_hole (MN 0 "equiv_val")

779+ letbind letn (Var tyn) (Var valn)

780+ focus tyn

781+ elab ist toplevel False False (MN 0 "tac") tm

782+ focus valn

783+ when autoSolve solveAll

772784 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

773785 = do attack; -- (h:_) <- get_holes

774786 tyn <- unique_hole (MN 0 "rty")

src/Idris/Parser.hs+3

@@ -1608,6 +1608,9 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

16081608 <|> do reserved "rewrite"; t <- pExpr syn;

16091609 i <- getState

16101610 return $ Rewrite (desugar syn i t)

1611+ <|> do reserved "equiv"; t <- pExpr syn;

1612+ i <- getState

1613+ return $ Equiv (desugar syn i t)

16111614 <|> try (do reserved "let"; n <- pName; lchar ':';

16121615 ty <- pExpr' syn; lchar '='; t <- pExpr syn;

16131616 i <- getState