git.iko.soy/Idris-dev
on master help sign in
Add vim script to contribs/ for case split

source it from your .vimrc, and use 'ci' to split the variable under the cursor.

commita5971542fbfe1c9a16aa509c2618b5aa0c38010b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 28 Oct 2013, 00:38 (13 years ago) parentd20f35c
3 files changed+23−5
compare with master
unifiedsplit
contribs/idriscasesplit.vim+17 src/Idris/ElabDecls.hs+4−3 src/Idris/REPL.hs+2−2
contribs/idriscasesplit.vimnew file+17
@@ -0,0 +1,17 @@
1+
2+function CaseSplit()
3+ let view = winsaveview()
4+ w
5+ let cline = line(".")
6+ let word = expand("<cword>")
7+ let fn = "idris --client :cs! " . cline . " " . word
8+ let tc = system("idris --client :r")
9+ let result = system(fn)
10+ e
11+ call winrestview(view)
12+ if (! (result is ""))
13+ echo result
14+ endif
15+endfunction
16+
17+map ci :call CaseSplit()<ENTER>
src/Idris/ElabDecls.hs+4−3
@@ -817,9 +817,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
817817 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)
818818 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
819819
820− addInternalApp (fc_fname fc) (fc_line fc) lhs
821− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) lhs)
822−
823820 ((lhs', dlhs, []), _) <-
824821 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
825822 (errAt "left hand side of " fname
@@ -828,6 +825,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
828825 let lhs_ty = getInferType lhs'
829826 logLvl 3 ("Elaborated: " ++ show lhs_tm)
830827 logLvl 3 ("Elaborated type: " ++ show lhs_ty)
828+
829+ addInternalApp (fc_fname fc) (fc_line fc) (delab i lhs_tm)
830+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delab i lhs_tm))
831+
831832 (clhs_c, clhsty) <- recheckC fc [] lhs_tm
832833 let clhs = normalise ctxt [] clhs_c
833834 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
src/Idris/REPL.hs+2−2
@@ -503,12 +503,12 @@ process h fn (CaseSplitAt updatefile l n)
503503 iLOG (showSep "\n" (map show res))
504504 let (before, (ap : later)) = splitAt (l-1) (lines src)
505505 let new = concat (replaceSplits ap res)
506− ihputStrLn h new
507506 if updatefile then
508507 do let fb = fn ++ "~" -- make a backup!
509508 runIO $ writeFile fb (unlines before ++ new ++ unlines later)
510509 runIO $ copyFile fb fn
511− else return ()
510+ else do ihputStrLn h (show res)
511+ ihputStrLn h new
512512
513513
514514process h fn (Spec t)