a597154 · Idris-dev · git.iko.soy

contribs/idriscasesplit.vimnew file+17

compare with master

unifiedsplit

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

817 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)

818 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

819

820− addInternalApp (fc_fname fc) (fc_line fc) lhs

821− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) lhs)

822−

823 ((lhs', dlhs, []), _) <-

820 ((lhs', dlhs, []), _) <-

824 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

821 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

825 (errAt "left hand side of " fname

822 (errAt "left hand side of " fname

@@ -828,6 +825,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

828 let lhs_ty = getInferType lhs'

825 let lhs_ty = getInferType lhs'

829 logLvl 3 ("Elaborated: " ++ show lhs_tm)

826 logLvl 3 ("Elaborated: " ++ show lhs_tm)

830 logLvl 3 ("Elaborated type: " ++ show lhs_ty)

827 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+

831 (clhs_c, clhsty) <- recheckC fc [] lhs_tm

832 (clhs_c, clhsty) <- recheckC fc [] lhs_tm

832 let clhs = normalise ctxt [] clhs_c

833 let clhs = normalise ctxt [] clhs_c

833 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

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

503 iLOG (showSep "\n" (map show res))

504 let (before, (ap : later)) = splitAt (l-1) (lines src)

505 let new = concat (replaceSplits ap res)

506− ihputStrLn h new

507 if updatefile then

506 if updatefile then

508 do let fb = fn ++ "~" -- make a backup!

507 do let fb = fn ++ "~" -- make a backup!

509 runIO $ writeFile fb (unlines before ++ new ++ unlines later)

508 runIO $ writeFile fb (unlines before ++ new ++ unlines later)

510 runIO $ copyFile fb fn

509 runIO $ copyFile fb fn

511− else return ()

510+ else do ihputStrLn h (show res)

511+ ihputStrLn h new

512

513

514process h fn (Spec t)