af99a9d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add :makelemma command in interactive editing

af99a9dEdwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

@@ -321,6 +321,7 @@ data Command = Quit

321 | AddProofClauseFrom Bool Int Name

322 | AddMissing Bool Int Name

323 | MakeWith Bool Int Name

324+ | MakeLemma Bool Int Name

324 | DoProofSearch Bool Bool Int Name [Name]

325 | DoProofSearch Bool Bool Int Name [Name]

325 -- ^ the first bool is whether to update,

326 -- ^ the first bool is whether to update,

326 -- the second is whether to search recursively (i.e. for the arguments)

327 -- the second is whether to search recursively (i.e. for the arguments)

src/Idris/ElabDecls.hs+1

@@ -805,6 +805,7 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

805

806 -- Generate projection functions

807 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])

808+ logLvl 3 $ show proj_decls

808 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

809 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

809 let implBinds = getImplB id cty'

810 let implBinds = getImplB id cty'

810

811

src/Idris/ElabTerm.hs+1−1

@@ -560,7 +560,7 @@ elab ist info pattern opts fn tm

560 claim tyn RType

561 valn <- getNameFrom (sMN 0 "rval")

562 claim valn (Var tyn)

563− letn <- getNameFrom (sMN 0 "rewrite_rule")

563+ letn <- getNameFrom (sMN 0 "_rewrite_rule")

564 letbind letn (Var tyn) (Var valn)

565 focus valn

566 elab' ina r

src/Idris/Interactive.hs+59−17

@@ -1,5 +1,6 @@

1module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,

2− addMissing, makeWith, doProofSearch) where

2+ addMissing, makeWith, doProofSearch,

3+ makeLemma) where

4{- Bits and pieces for editing source files interactively, called from

5{- Bits and pieces for editing source files interactively, called from

5 the REPL -}

6 the REPL -}

@@ -195,26 +196,67 @@ doProofSearch h fn updatefile rec l n hints

195 nsroot (SN (WhereN _ _ n)) = nsroot n

196 nsroot (SN (WhereN _ _ n)) = nsroot n

196 nsroot n = n

197 nsroot n = n

197

198

198− updateMeta brack ('?':cs) n new

199+updateMeta brack ('?':cs) n new

199− | length cs >= length n

200+ | length cs >= length n

200− = case splitAt (length n) cs of

201+ = case splitAt (length n) cs of

201− (mv, c:cs) ->

202+ (mv, c:cs) ->

202− if ((isSpace c || c == ')' || c == '}') && mv == n)

203+ if ((isSpace c || c == ')' || c == '}') && mv == n)

203− then addBracket brack new ++ (c : cs)

204+ then addBracket brack new ++ (c : cs)

204− else '?' : mv ++ c : updateMeta True cs n new

205+ else '?' : mv ++ c : updateMeta True cs n new

205− (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv

206+ (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv

206− updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new

207+updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new

207− updateMeta brack (c:cs) n new

208+updateMeta brack (c:cs) n new

208− = c : updateMeta (brack || not (isSpace c)) cs n new

209+ = c : updateMeta (brack || not (isSpace c)) cs n new

209− updateMeta brack [] n new = ""

210+updateMeta brack [] n new = ""

210

211

211− addBracket False new = new

212+addBracket False new = new

212− addBracket True new@('(':xs) | last xs == ')' = new

213+addBracket True new@('(':xs) | last xs == ')' = new

213− addBracket True new | any isSpace new = '(' : new ++ ")"

214+addBracket True new | any isSpace new = '(' : new ++ ")"

214− | otherwise = new

215+ | otherwise = new

215

216

217

218+makeLemma :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

219+makeLemma h fn updatefile l n

220+ = do src <- runIO $ readFile fn

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

222+

223+ ctxt <- getContext

224+ mty <- case lookupTy n ctxt of

225+ [t] -> return t

226+ [] -> ierror (NoSuchVariable n)

227+ ns -> ierror (CantResolveAlts (map show ns))

228+

229+ i <- getIState

230+ let lem = show n ++ " : " ++ show (stripMNBind (delab i mty))

231+ let lem_app = show n ++ appArgs mty

232+

233+ if updatefile then

234+ do let fb = fn ++ "~"

235+ runIO $ writeFile fb (addLem before tyline lem lem_app later)

236+ runIO $ copyFile fb fn

237+ else ihPrintResult h $ lem ++ "\n" ++ lem_app

238+

239+ where getIndent s = length (takeWhile isSpace s)

240+

241+ appArgs (Bind n@(UN c) (Pi _) sc)

242+ | thead c /= '_' = " " ++ show n ++ appArgs sc

243+ appArgs (Bind _ (Pi _) sc) = " " ++ appArgs sc

244+ appArgs _ = ""

245+

246+ stripMNBind (PPi b n@(UN c) ty sc)

247+ | thead c /= '_' = PPi b n ty (stripMNBind sc)

248+ stripMNBind (PPi b _ ty sc) = stripMNBind sc

249+ stripMNBind t = t

250+

251+ blank = all isSpace

217

252

253+ addLem before tyline lem lem_app later

254+ = let (bef_end, blankline : bef_start)

255+ = span (not . blank) (reverse before)

256+ mvline = updateMeta False tyline (show n) lem_app in

257+ unlines $ reverse bef_start ++

258+ [blankline, lem, blankline] ++

259+ reverse bef_end ++ mvline : later

218

260

219

261

220

262

src/Idris/REPL.hs+2

@@ -709,6 +709,8 @@ process h fn (AddMissing updatefile l n)

709 = addMissing h fn updatefile l n

710process h fn (MakeWith updatefile l n)

711 = makeWith h fn updatefile l n

712+process h fn (MakeLemma updatefile l n)

713+ = makeLemma h fn updatefile l n

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

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

713 = doProofSearch h fn updatefile rec l n hints

715 = doProofSearch h fn updatefile rec l n hints

714process h fn (Spec t)

716process h fn (Spec t)

src/Idris/REPLParser.hs+4

@@ -87,6 +87,10 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

87 upd <- option False (do P.lchar '!'; return True)

88 l <- P.natural; n <- P.name;

89 return (MakeWith upd (fromInteger l) n))

90+ <|> try (do cmd ["ml", "makelemma"]; P.whiteSpace;

91+ upd <- option False (do P.lchar '!'; return True)

92+ l <- P.natural; n <- P.name;

93+ return (MakeLemma upd (fromInteger l) n))

90 <|> try (do cmd ["ps", "proofsearch"]; P.whiteSpace;

94 <|> try (do cmd ["ps", "proofsearch"]; P.whiteSpace;

91 upd <- option False (do P.lchar '!'; return True)

95 upd <- option False (do P.lchar '!'; return True)

92 l <- P.natural; n <- P.name;

96 l <- P.natural; n <- P.name;