36b477e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #621 from hannesm/cleanup

Remove "CaseSplit" constructor and implementation which could never

commit36b477e6246859bd81826a20fb325b36418512cc authorEdwin Brady <edwin.brady@gmail.com> dateMon 18 Nov 2013, 14:19 (13 years ago) parent8325f1a 23772e9

3 files changed+1−5

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs−1 src/Idris/CaseSplit.hs+1−1 src/Idris/REPL.hs−3

src/Idris/AbsSyntaxTree.hs−1

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

239239 | Pattelab PTerm

240240 | DebugInfo Name

241241 | Search PTerm

242− | CaseSplit Name PTerm

243242 | CaseSplitAt Bool Int Name

244243 | AddClauseFrom Bool Int Name

245244 | AddProofClauseFrom Bool Int Name

src/Idris/CaseSplit.hs+1−1

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

11{-# LANGUAGE PatternGuards #-}

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

3+module Idris.CaseSplit(splitOnLine, replaceSplits,

44 getClause, getProofClause,

55 mkWith,

66 getUniq, nameRoot) where

src/Idris/REPL.hs−3

@@ -536,9 +536,6 @@ process h fn (Info n)

536536 [c] -> classInfo c

537537 _ -> iPrintError "Not a class"

538538process h fn (Search t) = iPrintError "Not implemented"

539−process h fn (CaseSplit n t)

540− = do tms <- split n t

541− iputStrLn (showSep "\n" (map show tms))

542539-- FIXME: There is far too much repetition in the cases below!

543540process h fn (CaseSplitAt updatefile l n)

544541 = do src <- runIO $ readFile fn