af99a9d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add :makelemma command in interactive editing

Given a metavariable and a line number, add a new top level function to solve that metavariable, and fill in the metavariable with an application of that function. e.g. given plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n plus_commutes Z m = ?pcrhs_Z plus_commutes (S k) m = rewrite plus_commutes k m in ?pcrhs_S :makelemma on pcrhs_S will update the file to pcrhs_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k) plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n plus_commutes Z m = ?pcrhs_Z plus_commutes (S k) m = rewrite plus_commutes k m in (pcrhs_S k m) where pcrhs_S can be built interactively in the normal way.

commitaf99a9db09cdbeff39d77cc1c4ecfaeb838b1248 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 11 May 2014, 20:17 (12 years ago) parent0bb1294

6 files changed+68−18

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/ElabDecls.hs+1 src/Idris/ElabTerm.hs+1−1 src/Idris/Interactive.hs+59−17 src/Idris/REPL.hs+2 src/Idris/REPLParser.hs+4

src/Idris/AbsSyntaxTree.hs+1

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

321321 | AddProofClauseFrom Bool Int Name

322322 | AddMissing Bool Int Name

323323 | MakeWith Bool Int Name

324+ | MakeLemma Bool Int Name

324325 | DoProofSearch Bool Bool Int Name [Name]

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

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

805805

806806 -- Generate projection functions

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

808+ logLvl 3 $ show proj_decls

808809 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

809810 let implBinds = getImplB id cty'

810811

src/Idris/ElabTerm.hs+1−1

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

560560 claim tyn RType

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

562562 claim valn (Var tyn)

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

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

564564 letbind letn (Var tyn) (Var valn)

565565 focus valn

566566 elab' ina r

src/Idris/Interactive.hs+59−17

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

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

2− addMissing, makeWith, doProofSearch) where

2+ addMissing, makeWith, doProofSearch,

3+ makeLemma) where

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

56 the REPL -}

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

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

196197 nsroot n = n

197198

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

199− | length cs >= length n

200− = case splitAt (length n) cs of

201− (mv, c:cs) ->

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

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

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

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

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

207− updateMeta brack (c:cs) n new

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

209− updateMeta brack [] n new = ""

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

200+ | length cs >= length n

201+ = case splitAt (length n) cs of

202+ (mv, c:cs) ->

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

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

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

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

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

208+updateMeta brack (c:cs) n new

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

210+updateMeta brack [] n new = ""

210211

211− addBracket False new = new

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

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

214− | otherwise = new

212+addBracket False new = new

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

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

215+ | otherwise = new

215216

216217

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

217252

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

218260

219261

220262

src/Idris/REPL.hs+2

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

709709 = addMissing h fn updatefile l n

710710process h fn (MakeWith updatefile l n)

711711 = makeWith h fn updatefile l n

712+process h fn (MakeLemma updatefile l n)

713+ = makeLemma h fn updatefile l n

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

713715 = doProofSearch h fn updatefile rec l n hints

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

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

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

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

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

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

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