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

libs/base/Language/Reflection.idr+2

compare with master

unifiedsplit

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

167 -- ^ apply both tactics in sequence

168 | Trivial

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

170+ | Search Int

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

170 | Instance

172 | Instance

171 -- ^ resolve a type class

173 -- ^ resolve a type class

172 | Solve

174 | Solve

libs/effects/Effects.idr+4−50

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

100

101

102-- -------------------------------------------------- [ 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

150

103

151updateResTy : (val : t) ->

104updateResTy : (val : t) ->

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

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

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

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

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

270

223

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

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

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

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

226+-- so just brute force it.

273syntax MkDefaultEnv = with Env

227syntax MkDefaultEnv = with Env

274 (| [], [default], [default, default],

228 (| [], [default], [default, default],

275 [default, default, default],

229 [default, default, default],

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

281

235

282implicit

236implicit

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

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

284− {default tactics { byReflection reflectEff; }

238+ {default tactics { search 100; }

285 prf : SubList ys xs} ->

239 prf : SubList ys xs} ->

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

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

287lift' e {prf} = lift prf e

241lift' e {prf} = lift prf e

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

289implicit

243implicit

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

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

291 (eff : e t a b) ->

245 (eff : e t a b) ->

292− {default tactics { byReflection reflectEff; }

246+ {default tactics { search 100; }

293 prf : EffElem e a xs} ->

247 prf : EffElem e a xs} ->

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

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

295effect' e {prf} = effect prf e

249effect' e {prf} = effect prf e

src/Idris/AbsSyntaxTree.hs+1−1

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

740 | MatchRefine Name

741 | LetTac Name t | LetTacTy Name t t

742 | Exact t | Compute | Trivial | TCInstance

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

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

744 -- ^ the bool is whether to search recursively

745 | Solve

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

248+ rnf (ProofSearch r r1 r2 x1 x2)

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

250 rnf Solve = ()

251 rnf Attack = ()

src/Idris/ElabTerm.hs+8−4

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

821

822trivial' ist

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

824−proofSearch' ist rec prv top n hints

824+proofSearch' ist rec depth prv top n hints

825+ = proofSearch rec prv depth

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

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

826

827

828

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

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

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

1053 runT Compute = compute

1054 runT Compute = compute

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

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

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

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

1056− runT (ProofSearch rec prover top hints)

1057+ runT (ProofSearch rec prover depth top hints)

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

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

1059+ when autoSolve solveAll

1058 runT (Focus n) = focus n

1060 runT (Focus n) = focus n

1059 runT Solve = solve

1061 runT Solve = solve

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

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

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

1181

1183

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

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

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

1185reifyApp 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 [])

1184reifyApp _ t [x]

1188reifyApp _ t [x]

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

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

1186 return $ Refine n []

1190 return $ Refine n []

src/Idris/IBC.hs+9−7

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

30import Util.Zlib (decompressEither)

31

32ibcVersion :: Word8

33−ibcVersion = 71

33+ibcVersion = 72

34

35data IBCFile = IBCFile { ver :: Word8,

36 sourcefile :: FilePath,

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

1952 put x1

1953 ByReflection x1 -> do putWord8 20

1954 put x1

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

1955+ ProofSearch x1 x2 x3 x4 x5 -> 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+ put x4

1960+ put x5

1960 DoUnify -> putWord8 22

1961 DoUnify -> putWord8 22

1961 get

1962 get

1962 = do i <- getWord8

1963 = do i <- getWord8

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

2003 x2 <- get

2004 x2 <- get

2004 x3 <- get

2005 x3 <- get

2005 x4 <- get

2006 x4 <- get

2007+ x5 <- get

2006− return (ProofSearch x1 x2 x3 x4)

2008+ return (ProofSearch x1 x2 x3 x4 x5)

2007 22 -> return DoUnify

2009 22 -> return DoUnify

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

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

2009

2011

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

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

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

167 _ -> (Nothing, 0, True)

168 let fc = fileFC fn

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

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

170− (ProofSearch rec False t hints)]

170+ (ProofSearch rec False 10 t hints)]

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

172 newmv <- idrisCatch

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

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

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

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

1229+ <|> do reserved "search"

1230+ depth <- option 10 natural

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

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

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

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

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

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

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

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

src/Idris/ProofSearch.hs+3−4

@@ -48,9 +48,10 @@ 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.

51+ Int -> -- maximum depth

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

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

52 IState -> ElabD ()

53 IState -> ElabD ()

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

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

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

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

55 -- works

56 -- works

56 let all_imps = lookupCtxtName fn (idris_implicits ist)

57 let all_imps = lookupCtxtName fn (idris_implicits ist)

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

81

82

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

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

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

84 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

85 = case lookupCtxt nroot (idris_tyinfodata ist) of

86 = case lookupCtxt nroot (idris_tyinfodata ist) of

86 [TISolution ts] -> findInferredTy ts

87 [TISolution ts] -> findInferredTy ts

87 _ -> psRec rec maxDepth

88 _ -> psRec rec maxDepth

88 where

89 where

89− maxDepth = 6

90−

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

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

92

91

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

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