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

git.iko.soy/Idris-dev

on master help sign in

Add :makewith command at the REPL

6456d6fEdwin Brady13 years ago

contribs/idriscasesplit.vim+21

compare with master

unifiedsplit

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

37 endif

38endfunction

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+

40function IdrisAddClause()

60function IdrisAddClause()

41 let view = winsaveview()

61 let view = winsaveview()

42 w

62 w

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

62map cr :call IdrisReload()<ENTER>

82map cr :call IdrisReload()<ENTER>

63map ci :call IdrisCaseSplit()<ENTER>

83map ci :call IdrisCaseSplit()<ENTER>

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

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

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

src/Idris/AbsSyntaxTree.hs+1

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

242 | CaseSplit Name PTerm

243 | CaseSplitAt Bool Int Name

244 | AddClauseFrom Bool Int Name

245+ | MakeWith Bool Int Name

245 | SetOpt Opt

246 | SetOpt Opt

246 | UnsetOpt Opt

247 | UnsetOpt Opt

247 | NOP

248 | NOP

src/Idris/CaseSplit.hs+25−6

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

1{-# LANGUAGE PatternGuards #-}

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

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

4+ getClause,

5+ mkWith) where

5-- splitting a variable in a pattern clause

7-- splitting a variable in a pattern clause

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

59 do let splits = findPats ist ty

61 do let splits = findPats ist ty

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

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

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

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

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

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

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

63 newPats <- mapM elabNewPat newPats_in

66 newPats <- mapM elabNewPat newPats_in

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

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

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

95mergePat ctxt old (PPatvar fc n)

98mergePat ctxt old (PPatvar fc n)

96 = mergePat ctxt old (PRef fc n)

99 = mergePat ctxt old (PRef fc n)

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

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

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

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

99− return new

102+ return new

100 | otherwise

103 | otherwise

101 = do ms <- get

104 = do ms <- get

102 case lookup n' (namemap ms) of

105 case lookup n' (namemap ms) of

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

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

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

165 | otherwise = Placeholder

168 | otherwise = Placeholder

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

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

167− | isConName v ctxt = orig

170+ | isDConName v ctxt = orig

168 subst (PRef _ _) = Placeholder

171 subst (PRef _ _) = Placeholder

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

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

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

170 subst x = x

174 subst x = x

171

175

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

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

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

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

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

240 mkApp _ _ = ""

244 mkApp _ _ = ""

241

245

242−

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

243−

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

244

263

245

264

src/Idris/REPL.hs+13−2

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

532 getIndent i n [] = 0

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

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

535−

535+process h fn (MakeWith updatefile l n)

536−

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

537

548

538process h fn (Spec t)

549process h fn (Spec t)

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

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

src/Idris/REPLParser.hs+6−2

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

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

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

36 <|> 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;

38 return (ModImport (toPath f)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

83 return (Just x))

87 return (Just x))

84 eof; return (AddProof n))

88 eof; return (AddProof n))