094be98 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add an optional depth to 'search' tactic

Also add it to Language.Reflection. It's now good enough to work with the proof obligations in Effects, so replace the old proof search (it's also noticeably faster in larger programs). Requires ibcs to be rebuilt.

commit094be98e5483995db374bcd53939028d96479189 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 21 May 2014, 20:34 (12 years ago) parentbd566f8

10 files changed+35−72

compare with master

unifiedsplit

libs/base/Language/Reflection.idr+2 libs/effects/Effects.idr+4−50 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/DeepSeq.hs+1−1 src/Idris/ElabTerm.hs+8−4 src/Idris/IBC.hs+9−7 src/Idris/IdrisDoc.hs+2−2 src/Idris/Interactive.hs+2−2 src/Idris/ParseExpr.hs+3−1 src/Idris/ProofSearch.hs+3−4

libs/base/Language/Reflection.idr+2

@@ -167,6 +167,8 @@ data Tactic = Try Tactic Tactic

167167 -- ^ apply both tactics in sequence

168168 | Trivial

169169 -- ^ intelligently construct the proof target from the context

170+ | Search Int

171+ -- ^ build a proof by applying contructors up to a maximum depth

170172 | Instance

171173 -- ^ resolve a type class

172174 | Solve

libs/effects/Effects.idr+4−50

@@ -100,53 +100,6 @@ rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env

100100

101101

102102-- -------------------------------------------------- [ The Effect EDSL itself ]

103−-- some proof automation

104−

105−%reflection

106−reflectListEffElem : List a -> Tactic

107−reflectListEffElem [] = Refine "Here" `Seq` Solve

108−reflectListEffElem (x :: xs)

109− = Try (Refine "Here" `Seq` Solve)

110− (Refine "There" `Seq` (Solve `Seq` reflectListEffElem xs))

111−-- TMP HACK! FIXME!

112−-- The evaluator needs a 'function case' to know its a reflection function

113−-- until we propagate that information! Without this, the _ case won't get

114−-- matched.

115−reflectListEffElem (x ++ y) = Refine "Here" `Seq` Solve

116−reflectListEffElem _ = Refine "Here" `Seq` Solve

117−

118−%reflection

119−reflectSubList : List a -> Tactic

120−reflectSubList [] = Refine "subListId" `Seq` Solve

121−reflectSubList (x :: xs)

122− = Try (Refine "subListId" `Seq` Solve)

123− (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))

124− (Refine "Drop" `Seq` (Solve `Seq` reflectSubList xs)))

125−reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve

126−reflectSubList _ = Refine "subListId" `Seq` Solve

127−

128−%reflection

129−reflectDefaultList : List a -> Tactic

130−reflectDefaultList [] = Refine "enil" `Seq` Solve

131−reflectDefaultList (x :: xs)

132− = Refine "econs" `Seq`

133− (Solve `Seq`

134− (Instance `Seq`

135− (Refine "default" `Seq`

136− (Solve `Seq`

137− (Instance `Seq`

138− (reflectDefaultList xs))))))

139−reflectDefaultList (x ++ y) = Refine "Nil" `Seq` Solve

140−reflectDefaultList _ = Refine "Nil" `Seq` Solve

141−

142−%reflection

143−reflectEff : (P : Type) -> Tactic

144−reflectEff (EffElem m a xs)

145− = reflectListEffElem xs `Seq` Solve

146−reflectEff (SubList xs ys)

147− = reflectSubList ys `Seq` Solve

148−reflectEff (Env m xs)

149− = reflectDefaultList xs `Seq` Solve

150103

151104updateResTy : (val : t) ->

152105 (xs : List EFFECT) -> EffElem e a xs -> e t a b ->

@@ -269,7 +222,8 @@ eff {xs = [l ::: x]} env (l :- prog) k

269222 eff env' prog (\p', envk => k p' (relabel l envk))

270223

271224-- yuck :) Haven't got type class instances working nicely in tactic

272−-- proofs yet, so just brute force it.

225+-- proofs yet, and 'search' can't be told about any hints yet,

226+-- so just brute force it.

273227syntax MkDefaultEnv = with Env

274228 (| [], [default], [default, default],

275229 [default, default, default],

@@ -281,7 +235,7 @@ syntax MkDefaultEnv = with Env

281235

282236implicit

283237lift' : Eff m t ys ys' ->

284− {default tactics { byReflection reflectEff; }

238+ {default tactics { search 100; }

285239 prf : SubList ys xs} ->

286240 Eff m t xs (\v => updateWith (ys' v) xs prf)

287241lift' e {prf} = lift prf e

@@ -289,7 +243,7 @@ lift' e {prf} = lift prf e

289243implicit

290244effect' : {a, b: _} -> {e : Effect} ->

291245 (eff : e t a b) ->

292− {default tactics { byReflection reflectEff; }

246+ {default tactics { search 100; }

293247 prf : EffElem e a xs} ->

294248 Eff m t xs (\v => updateResTy v xs prf eff)

295249effect' e {prf} = effect prf e

src/Idris/AbsSyntaxTree.hs+1−1

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

740740 | MatchRefine Name

741741 | LetTac Name t | LetTacTy Name t t

742742 | Exact t | Compute | Trivial | TCInstance

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

743+ | ProofSearch Bool Bool Int (Maybe Name) [Name]

744744 -- ^ the bool is whether to search recursively

745745 | Solve

746746 | 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 r1 x1 x2)

248+ rnf (ProofSearch r r1 r2 x1 x2)

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

250250 rnf Solve = ()

251251 rnf Attack = ()

src/Idris/ElabTerm.hs+8−4

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

821821

822822trivial' ist

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

824−proofSearch' ist rec prv top n hints

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

824+proofSearch' ist rec depth prv top n hints

825+ = proofSearch rec prv depth

826+ (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

826827

827828

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

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

10531054 runT Compute = compute

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

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

1056− runT (ProofSearch rec prover top hints)

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

1057+ runT (ProofSearch rec prover depth top hints)

1058+ = do proofSearch' ist rec depth prover top fn hints

1059+ when autoSolve solveAll

10581060 runT (Focus n) = focus n

10591061 runT Solve = solve

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

@@ -1181,6 +1183,8 @@ reify _ t = fail ("Unknown tactic " ++ show t)

11811183

11821184reifyApp :: IState -> Name -> [Term] -> ElabD PTactic

11831185reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)

1186+reifyApp _ t [Constant (I i)]

1187+ | t == reflm "Search" = return (ProofSearch True True i Nothing [])

11841188reifyApp _ t [x]

11851189 | t == reflm "Refine" = do n <- reifyTTName x

11861190 return $ Refine n []

src/Idris/IBC.hs+9−7

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

3030import Util.Zlib (decompressEither)

3131

3232ibcVersion :: Word8

33−ibcVersion = 71

33+ibcVersion = 72

3434

3535data IBCFile = IBCFile { ver :: Word8,

3636 sourcefile :: FilePath,

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

19521952 put x1

19531953 ByReflection x1 -> do putWord8 20

19541954 put x1

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

1956− put x1

1957− put x2

1958− put x3

1959− put x4

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

1956+ put x1

1957+ put x2

1958+ put x3

1959+ put x4

1960+ put x5

19601961 DoUnify -> putWord8 22

19611962 get

19621963 = do i <- getWord8

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

20032004 x2 <- get

20042005 x3 <- get

20052006 x4 <- get

2006− return (ProofSearch x1 x2 x3 x4)

2007+ x5 <- get

2008+ return (ProofSearch x1 x2 x3 x4 x5)

20072009 22 -> return DoUnify

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

20092011

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

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

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

167167 _ -> (Nothing, 0, True)

168168 let fc = fileFC fn

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

170− (ProofSearch rec False t hints)]

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

170+ (ProofSearch rec False 10 t hints)]

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

172172 newmv <- idrisCatch

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

src/Idris/ParseExpr.hs+3−1

@@ -1226,7 +1226,9 @@ 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 True Nothing [])

1229+ <|> do reserved "search"

1230+ depth <- option 10 natural

1231+ return (ProofSearch True True (fromInteger depth) Nothing [])

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

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

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

src/Idris/ProofSearch.hs+3−4

@@ -48,9 +48,10 @@ proofSearch :: Bool ->

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

4949 -- new metavariables is meaningless, and there shoudl

5050 -- be an error reported instead.

51+ Int -> -- maximum depth

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

5253 IState -> ElabD ()

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

54+proofSearch False fromProver depth elab _ nroot [fn] ist

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

5556 -- works

5657 let all_imps = lookupCtxtName fn (idris_implicits ist)

@@ -81,13 +82,11 @@ proofSearch False fromProver elab _ nroot [fn] ist

8182

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

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

84−proofSearch rec fromProver elab fn nroot hints ist

85+proofSearch rec fromProver maxDepth elab fn nroot hints ist

8586 = case lookupCtxt nroot (idris_tyinfodata ist) of

8687 [TISolution ts] -> findInferredTy ts

8788 _ -> psRec rec maxDepth

8889 where

89− maxDepth = 6

90−

9190 findInferredTy (t : _) = elab (delab ist (toUN t))

9291

9392 toUN t@(P nt (MN i n) ty)