6456d6f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add :makewith command at the REPL

:makewith l n will take the definition of 'n' on line l, and replace its right hand side with a 'with' clause, and set up the new clause. :makewith! l n will correspondingly update the source file Also added 'cm' command to the vim script to invoke this.

commit6456d6fcaf1b9c6992e64371ffe696032439030d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 28 Oct 2013, 11:35 (13 years ago) parent46256ab

5 files changed+66−10

compare with master

unifiedsplit

contribs/idriscasesplit.vim+21 src/Idris/AbsSyntaxTree.hs+1 src/Idris/CaseSplit.hs+25−6 src/Idris/REPL.hs+13−2 src/Idris/REPLParser.hs+6−2

contribs/idriscasesplit.vim+21

@@ -37,6 +37,26 @@ function IdrisCaseSplit()

3737 endif

3838endfunction

3939

40+function IdrisMakeWith()

41+ let view = winsaveview()

42+ w

43+ let cline = line(".")

44+ let word = expand("<cword>")

45+ let tc = IdrisReload()

46+

47+ if (tc is "")

48+ let fn = "idris --client :mw! " . cline . " " . word

49+ let result = system(fn)

50+ if (! (result is ""))

51+ echo result

52+ else

53+ e

54+ call winrestview(view)

55+ call search("_")

56+ endif

57+ endif

58+endfunction

59+

4060function IdrisAddClause()

4161 let view = winsaveview()

4262 w

@@ -62,4 +82,5 @@ map ct :call IdrisShowType()<ENTER>

6282map cr :call IdrisReload()<ENTER>

6383map ci :call IdrisCaseSplit()<ENTER>

6484map cd ?:<ENTER>b:call IdrisAddClause()<ENTER>w

85+map cm 0:call IdrisMakeWith()<ENTER>

6586

src/Idris/AbsSyntaxTree.hs+1

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

242242 | CaseSplit Name PTerm

243243 | CaseSplitAt Bool Int Name

244244 | AddClauseFrom Bool Int Name

245+ | MakeWith Bool Int Name

245246 | SetOpt Opt

246247 | UnsetOpt Opt

247248 | NOP

src/Idris/CaseSplit.hs+25−6

@@ -1,6 +1,8 @@

11{-# LANGUAGE PatternGuards #-}

3−module Idris.CaseSplit(split, splitOnLine, replaceSplits, getClause) where

3+module Idris.CaseSplit(split, splitOnLine, replaceSplits,

4+ getClause,

5+ mkWith) where

57-- splitting a variable in a pattern clause

@@ -59,6 +61,7 @@ split n t'

5961 do let splits = findPats ist ty

6062 iLOG ("New patterns " ++ show splits)

6163 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)

64+ logLvl 4 ("Working from " ++ show t)

6265 logLvl 4 ("Trying " ++ showSep "\n" (map show newPats_in))

6366 newPats <- mapM elabNewPat newPats_in

6467 logLvl 3 ("Original:\n" ++ show t)

@@ -95,8 +98,8 @@ mergePat ctxt (PPatvar fc n) new

9598mergePat ctxt old (PPatvar fc n)

9699 = mergePat ctxt old (PRef fc n)

97100mergePat ctxt orig@(PRef fc n) new@(PRef _ n')

98− | isConName n' ctxt = do addUpdate n new;

99− return new

101+ | isDConName n' ctxt = do addUpdate n new;

102+ return new

100103 | otherwise

101104 = do ms <- get

102105 case lookup n' (namemap ms) of

@@ -164,9 +167,10 @@ replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)

164167 subst orig@(PPatvar _ v) | v == n = t

165168 | otherwise = Placeholder

166169 subst orig@(PRef _ v) | v == n = t

167− | isConName v ctxt = orig

170+ | isDConName v ctxt = orig

168171 subst (PRef _ _) = Placeholder

169172 subst (PApp fc f pats) = PApp fc f (map substArg pats)

173+ subst (PEq fc l r) = PEq fc (subst l) (subst r)

170174 subst x = x

171175

172176 substArg arg = arg { getTm = subst (getTm arg) }

@@ -239,7 +243,22 @@ getClause l fn fp = do ty <- getInternalApp fp l

239243 mkApp (PPi _ _ _ sc) ns = mkApp sc ns

240244 mkApp _ _ = ""

241245

242−

243−

246+-- Purely syntactic - turn a pattern match clause into a with and a new

247+-- match clause

248+

249+mkWith :: String -> Name -> String

250+mkWith str n = let ind = getIndent str

251+ str' = replicate ind ' ' ++

252+ replaceRHS str "with (_)"

253+ newpat = replicate (ind + 2) ' ' ++

254+ replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in

255+ str' ++ "\n" ++ newpat

256+

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

258+

259+ replaceRHS [] str = str

260+ replaceRHS ('?':'=': rest) str = str

261+ replaceRHS ('=': rest) str = str

262+ replaceRHS (x : rest) str = x : replaceRHS rest str

244263

245264

src/Idris/REPL.hs+13−2

@@ -532,8 +532,19 @@ process h fn (AddClauseFrom updatefile l n)

532532 getIndent i n [] = 0

533533 getIndent i n xs | take (length n) xs == n = i

534534 getIndent i n (x : xs) = getIndent (i + 1) n xs

535−

536−

535+process h fn (MakeWith updatefile l n)

536+ = do src <- runIO $ readFile fn

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

538+ let with = mkWith tyline n

539+ -- add clause before first blank line in 'later'

540+ let (nonblank, rest) = span (not . all isSpace) later

541+ if updatefile then

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

543+ runIO $ writeFile fb (unlines (before ++ nonblank)

544+ ++ with ++ "\n" ++

545+ unlines rest)

546+ runIO $ copyFile fb fn

547+ else ihputStrLn h with

537548

538549process h fn (Spec t)

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

src/Idris/REPLParser.hs+6−2

@@ -34,7 +34,7 @@ pCmd :: P.IdrisParser Command

3434pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

3535 <|> try (do cmd ["h", "?", "help"]; eof; return Help)

3636 <|> try (do cmd ["r", "reload"]; eof; return Reload)

37− <|> try (do cmd ["m", "module"]; f <- P.identifier; eof;

37+ <|> try (do cmd ["module"]; f <- P.identifier; eof;

3838 return (ModImport (toPath f)))

3939 <|> try (do cmd ["e", "edit"]; eof; return Edit)

4040 <|> try (do cmd ["exec", "execute"]; eof; return Execute)

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

4242 <|> try (do cmd ["c", "compile"]; f <- P.identifier; eof; return (Compile ViaC f))

4343 <|> try (do cmd ["jc", "newcompile"]; f <- P.identifier; eof; return (Compile ViaJava f))

4444 <|> try (do cmd ["js", "javascript"]; f <- P.identifier; eof; return (Compile ViaJavaScript f))

45− <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

4645 <|> try (do cmd ["proofs"]; eof; return Proofs)

4746 <|> try (do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n))

4847 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

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

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

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

8180 return (AddClauseFrom upd (fromInteger l) n))

81+ <|> try (do cmd ["mw", "makewith"]; P.whiteSpace;

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

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

84+ return (MakeWith upd (fromInteger l) n))

85+ <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

8286 <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

8387 return (Just x))

8488 eof; return (AddProof n))