3448469 · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+3

compare with master

unifiedsplit

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

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

288rewrite tm = processTactic' (Rewrite tm)

289

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

291+equiv tm = processTactic' (Equiv tm)

292+

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

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

291patvar n = do env <- get_env

294patvar n = do env <- get_env

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

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

src/Core/ProofState.hs+9

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

66 | Forall Name Raw

67 | LetBind Name Raw Raw

68 | Rewrite Raw

69+ | Equiv Raw

69 | PatVar Name

70 | PatVar Name

70 | PatBind Name

71 | PatBind Name

71 | Focus Name

72 | Focus Name

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

539 rname = MN 0 "replaced"

540 rname = MN 0 "replaced"

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

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

541

542

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+

542patbind :: Name -> RunTactic

550patbind :: Name -> RunTactic

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

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

544 do let t' = case t of

552 do let t' = case t of

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

724 mktac (Forall n t) = forall n t

732 mktac (Forall n t) = forall n t

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

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

726 mktac (Rewrite t) = rewrite t

734 mktac (Rewrite t) = rewrite t

735+ mktac (Equiv t) = equiv t

727 mktac (PatVar n) = patvar n

736 mktac (PatVar n) = patvar n

728 mktac (PatBind n) = patbind n

737 mktac (PatBind n) = patbind n

729 mktac (CheckIn r) = check_in r

738 mktac (CheckIn r) = check_in r

src/Idris/AbsSyntaxTree.hs+1

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

557

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

559 | Refine Name [Bool] | Rewrite t

560+ | Equiv t

560 | MatchRefine Name

561 | MatchRefine Name

561 | LetTac Name t | LetTacTy Name t t

562 | LetTac Name t | LetTacTy Name t t

562 | Exact t | Compute | Trivial

563 | Exact t | Compute | Trivial

src/Idris/ElabTerm.hs+12

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

769 _ -> return []

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

771 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

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

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

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

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

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

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

src/Idris/Parser.hs+3

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

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

1609 i <- getState

1610 return $ Rewrite (desugar syn i t)

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

1612+ i <- getState

1613+ return $ Equiv (desugar syn i t)

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

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

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

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

1613 i <- getState

1616 i <- getState