719d472 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

'search' now fails if there are metavariables

But only in tactic mode --- in interactive editing it leaves the metavariables so they can be solved by hand. Requires "make lib_clean" due to ibc version increment.

commit719d4720d53ff4f982c4e0ff23f0b01b46fa5274 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 12 May 2014, 12:56 (12 years ago) parent50f63b5

8 files changed+44−26

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/DeepSeq.hs+1−1 src/Idris/ElabTerm.hs+4−4 src/Idris/IBC.hs+8−6 src/Idris/IdrisDoc.hs+2−2 src/Idris/Interactive.hs+2−2 src/Idris/ParseExpr.hs+1−1 src/Idris/ProofSearch.hs+25−9

src/Idris/AbsSyntaxTree.hs+1−1

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

742742 | MatchRefine Name

743743 | LetTac Name t | LetTacTy Name t t

744744 | Exact t | Compute | Trivial | TCInstance

745− | ProofSearch Bool (Maybe Name) [Name]

745+ | ProofSearch Bool Bool (Maybe Name) [Name]

746746 -- ^ the bool is whether to search recursively

747747 | Solve

748748 | Attack

src/Idris/DeepSeq.hs+1−1

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

245245 rnf (Exact x1) = rnf x1 `seq` ()

246246 rnf Compute = ()

247247 rnf Trivial = ()

248− rnf (ProofSearch r x1 x2)

248+ rnf (ProofSearch r r1 x1 x2)

249249 = rnf x1 `seq` rnf x2 `seq` ()

250250 rnf Solve = ()

251251 rnf Attack = ()

src/Idris/ElabTerm.hs+4−4

@@ -821,8 +821,8 @@ findInstances ist t

821821

822822trivial' ist

823823 = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist

824−proofSearch' ist rec top n hints

825− = proofSearch rec (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

824+proofSearch' ist rec prv top n hints

825+ = proofSearch rec prv (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

826826

827827

828828resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

@@ -1053,8 +1053,8 @@ runTac autoSolve ist fn tac

10531053 runT Compute = compute

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

10551055 runT TCInstance = runT (Exact (PResolveTC emptyFC))

1056− runT (ProofSearch rec top hints)

1057− = do proofSearch' ist rec top fn hints; when autoSolve solveAll

1056+ runT (ProofSearch rec prover top hints)

1057+ = do proofSearch' ist rec prover top fn hints; when autoSolve solveAll

10581058 runT (Focus n) = focus n

10591059 runT Solve = solve

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

src/Idris/IBC.hs+8−6

@@ -30,7 +30,7 @@ import Codec.Compression.Zlib (compress)

3030import Util.Zlib (decompressEither)

3131

3232ibcVersion :: Word8

33−ibcVersion = 70

33+ibcVersion = 71

3434

3535data IBCFile = IBCFile { ver :: Word8,

3636 sourcefile :: FilePath,

@@ -1952,10 +1952,11 @@ instance (Binary t) => Binary (PTactic' t) where

19521952 put x1

19531953 ByReflection x1 -> do putWord8 20

19541954 put x1

1955− ProofSearch x1 x2 x3 -> do putWord8 21

1956− put x1

1957− put x2

1958− put x3

1955+ ProofSearch x1 x2 x3 x4 -> do putWord8 21

1956+ put x1

1957+ put x2

1958+ put x3

1959+ put x4

19591960 DoUnify -> putWord8 22

19601961 get

19611962 = do i <- getWord8

@@ -2001,7 +2002,8 @@ instance (Binary t) => Binary (PTactic' t) where

20012002 21 -> do x1 <- get

20022003 x2 <- get

20032004 x3 <- get

2004− return (ProofSearch x1 x2 x3)

2005+ x4 <- get

2006+ return (ProofSearch x1 x2 x3 x4)

20052007 22 -> return DoUnify

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

20072009

src/Idris/IdrisDoc.hs+2−2

@@ -340,8 +340,8 @@ extractPTactic (MatchRefine n) = [n]

340340extractPTactic (LetTac n p) = n : extract p

341341extractPTactic (LetTacTy n p1 p2) = n : concatMap extract [p1, p2]

342342extractPTactic (Exact p) = extract p

343−extractPTactic (ProofSearch _ m ns) | Just n <- m = n : ns

344−extractPTactic (ProofSearch _ _ ns) = ns

343+extractPTactic (ProofSearch _ _ m ns) | Just n <- m = n : ns

344+extractPTactic (ProofSearch _ _ _ ns) = ns

345345extractPTactic (Try t1 t2) = concatMap extractPTactic [t1, t2]

346346extractPTactic (TSeq t1 t2) = concatMap extractPTactic [t1, t2]

347347extractPTactic (ApplyTactic p) = extract p

src/Idris/Interactive.hs+2−2

@@ -164,8 +164,8 @@ doProofSearch h fn updatefile rec l n hints

164164 Just (t, e, False) -> (t, e, False)

165165 _ -> (Nothing, 0, True)

166166 let fc = fileFC fn

167− let body t = PProof [Try (TSeq Intros (ProofSearch rec t hints))

168− (ProofSearch rec t hints)]

167+ let body t = PProof [Try (TSeq Intros (ProofSearch rec False t hints))

168+ (ProofSearch rec False t hints)]

169169 let def = PClause fc mn (PRef fc mn) [] (body top) []

170170 newmv <- idrisCatch

171171 (do elabDecl' EAll toplevel (PClauses fc [] mn [def])

src/Idris/ParseExpr.hs+1−1

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

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

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

12281228 <|> do reserved "unify"; return DoUnify

1229− <|> do reserved "search"; return (ProofSearch True Nothing [])

1229+ <|> do reserved "search"; return (ProofSearch True True Nothing [])

12301230 <|> do reserved "instance"; return TCInstance

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

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

src/Idris/ProofSearch.hs+25−9

@@ -14,6 +14,7 @@ import Idris.Error

1414

1515import Control.Applicative ((<$>))

1616import Control.Monad

17+import Control.Monad.State.Strict

1718import Data.List

1819import Debug.Trace

1920

@@ -37,16 +38,26 @@ trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)

3738 (tryAll xs) True

3839 else tryAll xs

3940

40−proofSearch :: Bool ->

41+cantSolveGoal :: ElabD ()

42+cantSolveGoal = do g <- goal

43+ env <- get_env

44+ lift $ tfail $

45+ CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)

46+

47+proofSearch :: Bool ->

48+ Bool -> -- invoked from a tactic proof. If so, making

49+ -- new metavariables is meaningless, and there shoudl

50+ -- be an error reported instead.

4151 (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->

4252 IState -> ElabD ()

43−proofSearch False elab _ nroot [fn] ist

53+proofSearch False fromProver elab _ nroot [fn] ist

4454 = do -- get all possible versions of the name, take the first one that

4555 -- works

4656 let all_imps = lookupCtxtName fn (idris_implicits ist)

4757 tryAllFns all_imps

4858 where

4959 -- if nothing worked, make a new metavariable

60+ tryAllFns _ | fromProver = cantSolveGoal

5061 tryAllFns [] = do attack; defer nroot; solve

5162 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True

5263

@@ -60,15 +71,17 @@ proofSearch False elab _ nroot [fn] ist

6071 -- Make metavariables for new holes

6172 hs' <- get_holes

6273 ptm <- get_term

63− mapM_ (\ h -> do focus h

64− attack; defer nroot; solve)

65− (hs' \\ hs)

66−-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))

67− solve

74+ if fromProver then cantSolveGoal

75+ else do

76+ mapM_ (\ h -> do focus h

77+ attack; defer nroot; solve)

78+ (hs' \\ hs)

79+-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))

80+ solve

6881

6982 isImp (PImp p _ _ _ _) = (True, p)

7083 isImp arg = (True, priority arg) -- try to get all of them by unification

71−proofSearch rec elab fn nroot hints ist

84+proofSearch rec fromProver elab fn nroot hints ist

7285 = case lookupCtxt nroot (idris_tyinfodata ist) of

7386 [TISolution ts] -> findInferredTy ts

7487 _ -> psRec rec maxDepth

@@ -83,13 +96,16 @@ proofSearch rec elab fn nroot hints ist

8396 toUN (App f a) = App (toUN f) (toUN a)

8497 toUN t = t

8598

99+ psRec _ _ | fromProver = cantSolveGoal

86100 psRec rec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"

87101 psRec False d = tryCons d hints

88102 psRec True d = try' (trivial elab ist)

89103 (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))

90104 True)

91105 -- if all else fails, make a new metavariable

92− (do attack; defer nroot; solve) True) True

106+ (if fromProver

107+ then cantSolveGoal

108+ else do attack; defer nroot; solve) True) True

93109

94110 getFn d Nothing = []

95111 getFn d (Just f) | d < maxDepth-1 = [f]