5d2d5a7 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1−1

compare with master

unifiedsplit

@@ -615,7 +615,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

615 | Equiv t

616 | MatchRefine Name

617 | LetTac Name t | LetTacTy Name t t

618− | Exact t | Compute | Trivial | ProofSearch

618+ | Exact t | Compute | Trivial | ProofSearch Name

619 | Solve

620 | Attack

621 | ProofState | ProofTerm | Undo

src/Idris/ElabTerm.hs+5−3

@@ -644,8 +644,10 @@ findInstances ist t

644 _ -> []

645 | otherwise = []

646

647+trivial' ist

647−trivial' ist = trivial (elab ist toplevel False False (MN 0 "tac")) ist

648+ = trivial (elab ist toplevel False False (MN 0 "tac")) ist

649+proofSearch' ist n

648−proofSearch' ist = trivial (elab ist toplevel False False (MN 0 "tac")) ist

650+ = proofSearch (elab ist toplevel False False (MN 0 "tac")) n ist

649

651

650

652

651resolveTC :: Int -> Name -> IState -> ElabD ()

653resolveTC :: Int -> Name -> IState -> ElabD ()

@@ -860,7 +862,7 @@ runTac autoSolve ist tac

860 when autoSolve solveAll

862 when autoSolve solveAll

861 runT Compute = compute

863 runT Compute = compute

862 runT Trivial = do trivial' ist; when autoSolve solveAll

864 runT Trivial = do trivial' ist; when autoSolve solveAll

863− runT ProofSearch = do proofSearch' ist; when autoSolve solveAll

865+ runT (ProofSearch n) = do proofSearch' ist n; when autoSolve solveAll

864 runT (Focus n) = focus n

866 runT (Focus n) = focus n

865 runT Solve = solve

867 runT Solve = solve

866 runT (Try l r) = do try' (runT l) (runT r) True

868 runT (Try l r) = do try' (runT l) (runT r) True

src/Idris/ParseExpr.hs−1

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

1028 return $ TSeq t (mergeSeq ts)

1029 <|> do reserved "compute"; return Compute

1030 <|> do reserved "trivial"; return Trivial

1031− <|> do reserved "proofsearch"; return ProofSearch

1032 <|> do reserved "solve"; return Solve

1031 <|> do reserved "solve"; return Solve

1033 <|> do reserved "attack"; return Attack

1032 <|> do reserved "attack"; return Attack

1034 <|> do reserved "state"; return ProofState

1033 <|> do reserved "state"; return ProofState

src/Idris/ProofSearch.hs+5−2

@@ -30,6 +30,9 @@ trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)

30 (tryAll xs) True

31 else tryAll xs

32

33−proofSearch :: (PTerm -> ElabD ()) -> IState -> ElabD ()

33+proofSearch :: (PTerm -> ElabD ()) -> Name -> IState -> ElabD ()

34−proofSearch elab ist = trivial elab ist

34+proofSearch elab nroot ist

35+ = try (trivial elab ist)

36+ (do attack; defer nroot; solve)

37+

35

38

src/Idris/REPL.hs+2−1

@@ -578,7 +578,7 @@ process h fn (MakeWith updatefile l n)

578process h fn (DoProofSearch updatefile l n)

579 = do src <- runIO $ readFile fn

580 let (before, tyline : later) = splitAt (l-1) (lines src)

581− let body = PProof [Try (TSeq Intros ProofSearch) ProofSearch]

581+ let body = PProof [Try (TSeq Intros (ProofSearch n)) (ProofSearch n)]

582 ctxt <- getContext

583 mn <- case lookupNames n ctxt of

584 [x] -> return x

@@ -593,6 +593,7 @@ process h fn (DoProofSearch updatefile l n)

593 elabDecls toplevel [PClauses fc [] mn [def]]

594 (tm, ty) <- elabVal toplevel False (PRef fc mn)

595 ctxt <- getContext

596+ i <- getIState

596 let newmv = show (dropCtxt envlen (delab i (normaliseAll ctxt [] tm)))

597 let newmv = show (dropCtxt envlen (delab i (normaliseAll ctxt [] tm)))

597 if updatefile then

598 if updatefile then

598 do let fb = fn ++ "~"

599 do let fb = fn ++ "~"

test/reg007/expected+1−1

@@ -1,7 +1,7 @@

1reg007.lidr:8:1:A.n is already defined

2reg007.lidr:12:9:When elaborating right hand side of hurrah:

3Can't unify

4− [92mn[0m[94m = [0m[92mA.lala[0m

4+ [92mn[0m[94m = [0m[92mlala[0m

5with

6 [91m0[0m[94m = [0m[91m1[0m

7