e84cfb6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1251 from david-christiansen/ideslave-proof-depth

e84cfb6David Christiansen12 years ago

src/Idris/IdeSlave.hs+11−6

compare with master

unifiedsplit

@@ -171,7 +171,7 @@ data IdeSlaveCommand = REPLCompletions String

171 | AddProofClause Int String

172 | AddMissing Int String

173 | MakeWithBlock Int String

174− | ProofSearch Bool Int String [String]

174+ | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

175 | MakeLemma Int String

176 | LoadFile String

177 | DocsFor String

@@ -196,12 +196,17 @@ sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom na

196-- The Boolean in ProofSearch means "search recursively"

197-- If it's False, that means "refine", i.e. apply the name and fill in any

198-- arguments which can be done by unification.

199−sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom name, SexpList hintexp]) | Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints)

199+sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAtom name : rest))

200+ | [] <- rest = Just (ProofSearch True (fromInteger line) name [] Nothing)

201+ | [SexpList hintexp] <- rest

202+ , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints Nothing)

203+ | [SexpList hintexp, IntegerAtom depth] <- rest

204+ , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints (Just (fromInteger depth)))

200− where getHints = mapM (\h -> case h of

205+ where getHints = mapM (\h -> case h of

201− StringAtom s -> Just s

206+ StringAtom s -> Just s

202− _ -> Nothing)

207+ _ -> Nothing)

203sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)

208sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)

204−sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint])

209+sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing)

205sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

210sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

206sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

211sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

207sexpToCommand (SymbolAtom "get-options") = Just GetOpts

212sexpToCommand (SymbolAtom "get-options") = Just GetOpts

src/Idris/Interactive.hs+6−4

@@ -152,8 +152,10 @@ makeWith h fn updatefile l n

152

153

154doProofSearch :: Handle -> FilePath -> Bool -> Bool ->

155− Int -> Name -> [Name] -> Idris ()

155+ Int -> Name -> [Name] -> Maybe Int -> Idris ()

156−doProofSearch h fn updatefile rec l n hints

156+doProofSearch h fn updatefile rec l n hints Nothing

157+ = doProofSearch h fn updatefile rec l n hints (Just 10)

158+doProofSearch h fn updatefile rec l n hints (Just depth)

157 = do src <- runIO $ readFile fn

159 = do src <- runIO $ readFile fn

158 let (before, tyline : later) = splitAt (l-1) (lines src)

160 let (before, tyline : later) = splitAt (l-1) (lines src)

159 ctxt <- getContext

161 ctxt <- getContext

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

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

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

167 _ -> (Nothing, 0, True)

169 _ -> (Nothing, 0, True)

168 let fc = fileFC fn

170 let fc = fileFC fn

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

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

170− (ProofSearch rec False 10 t hints)]

172+ (ProofSearch rec False depth t hints)]

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

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

172 newmv <- idrisCatch

174 newmv <- idrisCatch

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

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

src/Idris/REPL.hs+3−3

@@ -293,8 +293,8 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.AddMissing line name) =

293 process stdout fn (AddMissing False line (sUN name))

294runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =

295 process stdout fn (MakeWith False line (sUN name))

296−runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch r line name hints) =

296+runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch r line name hints depth) =

297− process stdout fn (DoProofSearch False r line (sUN name) (map sUN hints))

297+ doProofSearch stdout fn False r line (sUN name) (map sUN hints) depth

298runIdeSlaveCommand id orig fn mods (IdeSlave.MakeLemma line name) =

299 case splitName name of

300 Left err -> iPrintError err

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

716process h fn (MakeLemma updatefile l n)

717 = makeLemma h fn updatefile l n

718process h fn (DoProofSearch updatefile rec l n hints)

719− = doProofSearch h fn updatefile rec l n hints

719+ = doProofSearch h fn updatefile rec l n hints Nothing

720process h fn (Spec t)

721 = do (tm, ty) <- elabVal toplevel False t

722 ctxt <- getContext