f8759cd · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

IDESlave support for setting the depth of interactive proof search

commitf8759cddac313ac1c21a0a9a5a0712fec2a3e4e6 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 22 May 2014, 11:12 (12 years ago) parent602552e

3 files changed+20−13

compare with master

unifiedsplit

src/Idris/IdeSlave.hs+11−6 src/Idris/Interactive.hs+6−4 src/Idris/REPL.hs+3−3

src/Idris/IdeSlave.hs+11−6

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

171171 | AddProofClause Int String

172172 | AddMissing Int String

173173 | MakeWithBlock Int String

174− | ProofSearch Bool Int String [String]

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

175175 | MakeLemma Int String

176176 | LoadFile String

177177 | DocsFor String

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

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

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

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

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

201− StringAtom s -> Just s

202− _ -> Nothing)

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

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

206+ StringAtom s -> Just s

207+ _ -> Nothing)

203208sexpToCommand (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)

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

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

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

src/Idris/Interactive.hs+6−4

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

152152

153153

154154doProofSearch :: Handle -> FilePath -> Bool -> Bool ->

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

156−doProofSearch h fn updatefile rec l n hints

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

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)

157159 = do src <- runIO $ readFile fn

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

159161 ctxt <- getContext

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

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

167169 _ -> (Nothing, 0, True)

168170 let fc = fileFC fn

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

170− (ProofSearch rec False 10 t hints)]

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

172+ (ProofSearch rec False depth t hints)]

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

172174 newmv <- idrisCatch

173175 (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) =

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

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

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

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

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

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

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

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

299299 case splitName name of

300300 Left err -> iPrintError err

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

716716process h fn (MakeLemma updatefile l n)

717717 = makeLemma h fn updatefile l n

718718process 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

720720process h fn (Spec t)

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

722722 ctxt <- getContext