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

git.iko.soy/Idris-dev

on master help sign in

'search' now fails if there are metavariables

719d472Edwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+1−1

compare with master

unifiedsplit

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

742 | MatchRefine Name

743 | LetTac Name t | LetTacTy Name t t

744 | Exact t | Compute | Trivial | TCInstance

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

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

746 -- ^ the bool is whether to search recursively

747 | Solve

748 | Attack

src/Idris/DeepSeq.hs+1−1

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

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

246 rnf Compute = ()

247 rnf Trivial = ()

248− rnf (ProofSearch r x1 x2)

248+ rnf (ProofSearch r r1 x1 x2)

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

250 rnf Solve = ()

251 rnf Attack = ()

src/Idris/ElabTerm.hs+4−4

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

821

822trivial' ist

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

824−proofSearch' ist rec top n hints

824+proofSearch' ist rec prv top n hints

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

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

826

827

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

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

1053 runT Compute = compute

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

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

1056− runT (ProofSearch rec top hints)

1056+ runT (ProofSearch rec prover top hints)

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

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

1058 runT (Focus n) = focus n

1059 runT Solve = solve

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

30import Util.Zlib (decompressEither)

32ibcVersion :: Word8

33−ibcVersion = 70

33+ibcVersion = 71

35data IBCFile = IBCFile { ver :: Word8,

36 sourcefile :: FilePath,

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

1952 put x1

1953 ByReflection x1 -> do putWord8 20

1954 put x1

1955− ProofSearch x1 x2 x3 -> do putWord8 21

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

1956− put x1

1956+ put x1

1957− put x2

1957+ put x2

1958− put x3

1958+ put x3

1959+ put x4

1959 DoUnify -> putWord8 22

1960 DoUnify -> putWord8 22

1960 get

1961 get

1961 = do i <- getWord8

1962 = do i <- getWord8

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

2001 21 -> do x1 <- get

2002 21 -> do x1 <- get

2002 x2 <- get

2003 x2 <- get

2003 x3 <- get

2004 x3 <- get

2005+ x4 <- get

2004− return (ProofSearch x1 x2 x3)

2006+ return (ProofSearch x1 x2 x3 x4)

2005 22 -> return DoUnify

2007 22 -> return DoUnify

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

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

2007

2009

src/Idris/IdrisDoc.hs+2−2

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

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

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

342extractPTactic (Exact p) = extract p

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

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

344−extractPTactic (ProofSearch _ _ ns) = ns

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

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

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

347extractPTactic (ApplyTactic p) = extract p

src/Idris/Interactive.hs+2−2

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

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

165 _ -> (Nothing, 0, True)

166 let fc = fileFC fn

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

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

168− (ProofSearch rec t hints)]

168+ (ProofSearch rec False t hints)]

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

170 newmv <- idrisCatch

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

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

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

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

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

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

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

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

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

src/Idris/ProofSearch.hs+25−9

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

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

16import Control.Monad

17+import Control.Monad.State.Strict

17import Data.List

18import Data.List

18import Debug.Trace

19import Debug.Trace

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

37 (tryAll xs) True

38 (tryAll xs) True

38 else tryAll xs

39 else tryAll xs

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+

40−proofSearch :: Bool ->

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.

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

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

42 IState -> ElabD ()

52 IState -> ElabD ()

43−proofSearch False elab _ nroot [fn] ist

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

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

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

45 -- works

55 -- works

46 let all_imps = lookupCtxtName fn (idris_implicits ist)

56 let all_imps = lookupCtxtName fn (idris_implicits ist)

47 tryAllFns all_imps

57 tryAllFns all_imps

48 where

58 where

49 -- if nothing worked, make a new metavariable

59 -- if nothing worked, make a new metavariable

60+ tryAllFns _ | fromProver = cantSolveGoal

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

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

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

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

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

60 -- Make metavariables for new holes

71 -- Make metavariables for new holes

61 hs' <- get_holes

72 hs' <- get_holes

62 ptm <- get_term

73 ptm <- get_term

74+ if fromProver then cantSolveGoal

75+ else do

63− mapM_ (\ h -> do focus h

76+ mapM_ (\ h -> do focus h

64− attack; defer nroot; solve)

77+ attack; defer nroot; solve)

65− (hs' \\ hs)

78+ (hs' \\ hs)

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

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

67− solve

80+ solve

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

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

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

83 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

72 = case lookupCtxt nroot (idris_tyinfodata ist) of

85 = case lookupCtxt nroot (idris_tyinfodata ist) of

73 [TISolution ts] -> findInferredTy ts

86 [TISolution ts] -> findInferredTy ts

74 _ -> psRec rec maxDepth

87 _ -> psRec rec maxDepth

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

83 toUN (App f a) = App (toUN f) (toUN a)

96 toUN (App f a) = App (toUN f) (toUN a)

84 toUN t = t

97 toUN t = t

99+ psRec _ _ | fromProver = cantSolveGoal

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

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

87 psRec False d = tryCons d hints

101 psRec False d = tryCons d hints

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

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

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

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

90 True)

104 True)

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

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

106+ (if fromProver

107+ then cantSolveGoal

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

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

109

94 getFn d Nothing = []

110 getFn d Nothing = []

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

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