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

git.iko.soy/Idris-dev

Failed proofsearch branch creates new metavariable

commit5d2d5a7ca246141ac2fc9a52c507ae0f3fae15b0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 29 Oct 2013, 18:51 (13 years ago) parentabf99a5

6 files changed+14−9

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/ElabTerm.hs+5−3 src/Idris/ParseExpr.hs−1 src/Idris/ProofSearch.hs+5−2 src/Idris/REPL.hs+2−1 test/reg007/expected+1−1

src/Idris/AbsSyntaxTree.hs+1−1

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

615615 | Equiv t

616616 | MatchRefine Name

617617 | LetTac Name t | LetTacTy Name t t

618− | Exact t | Compute | Trivial | ProofSearch

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

619619 | Solve

620620 | Attack

621621 | ProofState | ProofTerm | Undo

src/Idris/ElabTerm.hs+5−3

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

644644 _ -> []

645645 | otherwise = []

646646

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

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

647+trivial' ist

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

649+proofSearch' ist n

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

649651

650652

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

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

860862 when autoSolve solveAll

861863 runT Compute = compute

862864 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

864866 runT (Focus n) = focus n

865867 runT Solve = solve

866868 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) (

10281028 return $ TSeq t (mergeSeq ts)

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

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

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

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

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

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

3030 (tryAll xs) True

3131 else tryAll xs

3232

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

34−proofSearch elab ist = trivial elab ist

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

34+proofSearch elab nroot ist

35+ = try (trivial elab ist)

36+ (do attack; defer nroot; solve)

37+

3538

src/Idris/REPL.hs+2−1

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

578578process h fn (DoProofSearch updatefile l n)

579579 = do src <- runIO $ readFile fn

580580 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)]

582582 ctxt <- getContext

583583 mn <- case lookupNames n ctxt of

584584 [x] -> return x

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

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

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

595595 ctxt <- getContext

596+ i <- getIState

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

597598 if updatefile then

598599 do let fb = fn ++ "~"

test/reg007/expected+1−1

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

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

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

33Can't unify

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

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

55with

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