23772e9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove "CaseSplit" constructor and implementation which could never

be called (the REPLParser uses CaseSplitAt). Furhermore, we no longer need to export "split" from CaseSplit.hs

commit23772e9fd347fbc467b35ff948dc0c08ed75bd32 authorHannes Mehnert <hannes@mehnert.org> dateMon 18 Nov 2013, 17:57 (13 years ago) parentb37d0f4

3 files changed+1−5

unifiedsplit

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

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

532532 [c] -> classInfo c

533533 _ -> iPrintError "Not a class"

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

535−process h fn (CaseSplit n t)

536− = do tms <- split n t

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

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

539536process h fn (CaseSplitAt updatefile l n)

540537 = do src <- runIO $ readFile fn