1112fe4 · Idris-dev · git.iko.soy

lib/prelude/vect.idr+3

compare with master

unifiedsplit

@@ -11,6 +11,9 @@ data Vect : Set -> Nat -> Set where

11 Nil : Vect a O

12 (::) : a -> Vect a k -> Vect a (S k)

13

14+tail : Vect a (S n) -> Vect a n

15+tail (x :: xs) = xs

16+

14lookup : Fin n -> Vect a n -> a

17lookup : Fin n -> Vect a n -> a

15lookup fO (x :: xs) = x

18lookup fO (x :: xs) = x

16lookup (fS k) (x :: xs) = lookup k xs

19lookup (fS k) (x :: xs) = lookup k xs

src/Core/CaseTree.hs+26−23

@@ -34,13 +34,18 @@ small :: SC -> Bool

34-- small (STerm t) = True

35small _ = False

36

37−simpleCase :: Bool -> [(Term, Term)] -> CaseDef

37+simpleCase :: Bool -> Bool -> [(Term, Term)] -> CaseDef

38+simpleCase tc cover []

38−simpleCase tc [] = CaseDef [] (UnmatchedCase "No pattern clauses")

39+ = CaseDef [] (UnmatchedCase "No pattern clauses")

40+simpleCase tc cover cs

39−simpleCase tc cs = let pats = map (\ (l, r) -> (toPats tc l, r)) cs

41+ = let pats = map (\ (l, r) -> (toPats tc l, r)) cs

40 numargs = length (fst (head pats))

42 numargs = length (fst (head pats))

41− ns = take numargs args in

43+ ns = take numargs args

42− CaseDef ns (evalState (match ns pats (UnmatchedCase "Error")) numargs)

44+ tree = evalState (match ns pats (defaultCase cover)) numargs in

45+ CaseDef ns (prune tree)

43 where args = map (\i -> MN i "e") [0..]

46 where args = map (\i -> MN i "e") [0..]

47+ defaultCase True = STerm Erased

48+ defaultCase False = UnmatchedCase "Error"

44

49

45data Pat = PCon Name Int [Pat]

50data Pat = PCon Name Int [Pat]

46 | PConst Const

51 | PConst Const

@@ -193,21 +198,19 @@ varRule (v : vs) alts err =

193 repVar v (PV p : ps , res) = (ps, subst p (P Bound v (V 0)) res)

198 repVar v (PV p : ps , res) = (ps, subst p (P Bound v (V 0)) res)

194 repVar v (PAny : ps , res) = (ps, res)

199 repVar v (PAny : ps , res) = (ps, res)

195

200

196−{-

201+prune :: SC -> SC

197−mkOperator :: CaseDef -> [Value] -> Maybe Value

202+prune (Case n alts)

198−mkOperator (CaseDef ns casetree) args

203+ = let alts' = map pruneAlt $

199− | length args /= length ns = Nothing

204+ filter notErased alts in

200− | otherwise = evalArgs (zip ns args) casetree

205+ case alts' of

201− where

206+ [] -> STerm Erased

202− evalArgs map (Case n alts) =

207+ as -> Case n as

203− do v <- lookup n map

208+ where pruneAlt (ConCase n i ns sc) = ConCase n i ns (prune sc)

204− (altmap, tm) <- findAlt (getValArgs v) alts map

209+ pruneAlt (ConstCase c sc) = ConstCase c (prune sc)

205− evalArgs altmap tm

210+ pruneAlt (DefaultCase sc) = DefaultCase (prune sc)

206− evalArgs map (STerm tm) =

211+

207− evalArgs map (UnmatchedCase _) = Nothing

212+ notErased (DefaultCase (STerm Erased)) = False

208−

213+ notErased _ = True

209− getValArgs tm = getValArgs' tm []

214+prune t = t

210− getValArgs' (VApp f a) as = getValArgs' f (a:as)

215+

211− getValArgs' f as = (f, as)

216+

212−

213−-}

src/Core/Evaluate.hs+4−3

@@ -522,12 +522,13 @@ addDatatype (Data n tag ty cons) uctxt

522 addCons (tag+1) cons (addDef n

523 (TyDecl (DCon tag (arity ty')) ty, Public) ctxt)

524

525−addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->

525+addCasedef :: Name -> Bool -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->

526 Type -> Context -> Context

527−addCasedef n alwaysInline tcase ps psrt ty uctxt

527+addCasedef n alwaysInline tcase covering ps psrt ty uctxt

528 = let ctxt = definitions uctxt

529 ps' = ps -- simpl ps in

530− ctxt' = case (simpleCase tcase ps', simpleCase tcase psrt) of

530+ ctxt' = case (simpleCase tcase covering ps',

531+ simpleCase tcase covering psrt) of

531 (CaseDef args sc, CaseDef args' sc') ->

532 (CaseDef args sc, CaseDef args' sc') ->

532 let inl = alwaysInline in

533 let inl = alwaysInline in

533 addDef n (CaseOp inl ty ps args sc args' sc',

534 addDef n (CaseOp inl ty ps args sc args' sc',

src/Core/TT.hs+6

@@ -449,6 +449,12 @@ getArgTys :: TT n -> [(n, TT n)]

449getArgTys (Bind n (Pi t) sc) = (n, t) : getArgTys sc

450getArgTys _ = []

451

452+getRetTy :: TT n -> TT n

453+getRetTy (Bind n (PVar _) sc) = getRetTy sc

454+getRetTy (Bind n (PVTy _) sc) = getRetTy sc

455+getRetTy (Bind n (Pi _) sc) = getRetTy sc

456+getRetTy sc = sc

457+

452uniqueName :: Name -> [Name] -> Name

458uniqueName :: Name -> [Name] -> Name

453uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

459uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

454 | otherwise = n

460 | otherwise = n

src/Idris/AbsSyntax.hs+18−2

@@ -20,13 +20,14 @@ import qualified Epic.Epic as E

20data IOption = IOption { opt_logLevel :: Int,

21 opt_typecase :: Bool,

22 opt_typeintype :: Bool,

23+ opt_coverage :: Bool,

23 opt_showimp :: Bool,

24 opt_showimp :: Bool,

24 opt_repl :: Bool,

25 opt_repl :: Bool,

25 opt_verbose :: Bool

26 opt_verbose :: Bool

26 }

27 }

27 deriving (Show, Eq)

28 deriving (Show, Eq)

28

29

29−defaultOpts = IOption 0 False False False True True

30+defaultOpts = IOption 0 False False True False True True

30

31

31-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

32-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

32-- without typechecking).

33-- without typechecking).

@@ -245,6 +246,16 @@ setTypeInType t = do i <- get

245 let opt' = opts { opt_typeintype = t }

246 let opt' = opts { opt_typeintype = t }

246 put (i { idris_options = opt' })

247 put (i { idris_options = opt' })

247

248

249+coverage :: Idris Bool

250+coverage = do i <- get

251+ return (opt_coverage (idris_options i))

252+

253+setCoverage :: Bool -> Idris ()

254+setCoverage t = do i <- get

255+ let opts = idris_options i

256+ let opt' = opts { opt_coverage = t }

257+ put (i { idris_options = opt' })

258+

248impShow :: Idris Bool

259impShow :: Idris Bool

249impShow = do i <- get

260impShow = do i <- get

250 return (opt_showimp (idris_options i))

261 return (opt_showimp (idris_options i))

@@ -1205,6 +1216,9 @@ matchClause x y = checkRpts $ match (fullApp x) (fullApp y) where

1205 return (mf ++ concat ms)

1216 return (mf ++ concat ms)

1206-- match (PRef _ n) (PRef _ n') | n == n' = return []

1217-- match (PRef _ n) (PRef _ n') | n == n' = return []

1207-- | otherwise = Nothing

1218-- | otherwise = Nothing

1219+ match (PRef f n) (PApp _ x []) = match (PRef f n) x

1220+ match (PApp _ x []) (PRef f n) = match x (PRef f n)

1221+ match (PRef _ n) (PRef _ n') | n == n' = return []

1208 match (PRef _ n) tm = return [(n, tm)]

1222 match (PRef _ n) tm = return [(n, tm)]

1209 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

1223 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

1210 mr <- match' r r'

1224 mr <- match' r r'

@@ -1246,13 +1260,15 @@ matchClause x y = checkRpts $ match (fullApp x) (fullApp y) where

1246 return (mt ++ mty ++ ms)

1260 return (mt ++ mty ++ ms)

1247 match (PHidden x) (PHidden y) = match' x y

1261 match (PHidden x) (PHidden y) = match' x y

1248 match Placeholder _ = return []

1262 match Placeholder _ = return []

1263+ match _ Placeholder = return []

1249 match (PResolveTC _) _ = return []

1264 match (PResolveTC _) _ = return []

1250 match a b | a == b = return []

1265 match a b | a == b = return []

1251 | otherwise = LeftErr (a, b)

1266 | otherwise = LeftErr (a, b)

1252

1267

1253 checkRpts (RightOK ms) = check ms where

1268 checkRpts (RightOK ms) = check ms where

1254 check ((n,t):xs)

1269 check ((n,t):xs)

1270+ | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder

1255− | Just t' <- lookup n xs = if t/=t' then Left (t, t')

1271+ then Left (t, t')

1256 else check xs

1272 else check xs

1257 check (_:xs) = check xs

1273 check (_:xs) = check xs

1258 check [] = Right ms

1274 check [] = Right ms

src/Idris/Compiler.hs+8

@@ -168,6 +168,14 @@ instance ToEpic ([Name], SC) where

168 return $ term (map ename args, tree')

169

170instance ToEpic SC where

171+ epic (Case n [ConCase _ i ns sc])

172+ = epicLet n ns 0 sc

173+ where

174+ epicLet x [] _ sc = epic sc

175+ epicLet x (n:ns) i sc

176+ = do sc' <- epicLet x ns (i+1) sc

177+ return $ let_ (ref (ename x) !. i) (ename n, sc')

178+

171 epic (STerm t) = epic t

179 epic (STerm t) = epic t

172 epic (UnmatchedCase str) = return $ error_ str

180 epic (UnmatchedCase str) = return $ error_ str

173 epic (Case n alts) = do alts' <- mapM mkEpicAlt alts

181 epic (Case n alts) = do alts' <- mapM mkEpicAlt alts

src/Idris/Coverage.hs+89−3

@@ -1,11 +1,97 @@

1+{-# LANGUAGE PatternGuards #-}

2+

1module Idris.Coverage where

3module Idris.Coverage where

2

4

5+import Core.TT

6+import Core.Evaluate

3import Idris.AbsSyntax

7import Idris.AbsSyntax

8+import Idris.Delaborate

9+

10+import Data.List

11+import Debug.Trace

4

12

5−-- Given a list of LHSs, generate a complete collection of clauses which cover all

13+-- Given a list of LHSs, generate a extra clauses which cover the remaining

6-- cases. The ones which haven't been provided are marked 'absurd' so that the

14-- cases. The ones which haven't been provided are marked 'absurd' so that the

7-- checker will make sure they can't happen.

15-- checker will make sure they can't happen.

8

16

17+-- This will only work after the given clauses have been typechecked and the

18+-- names are fully explicit!

19+

9−genClauses :: [PClause] -> [PClause]

20+genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PClause]

10−genClauses xs = xs

21+genClauses fc n xs given

22+ = do i <- getIState

23+ let lhss = map (getLHS i) xs

24+ let argss = transpose lhss

25+ let all_args = map (genAll i) argss

26+ logLvl 7 $ "COVERAGE of " ++ show n

27+ logLvl 10 $ show argss ++ "\n" ++ show all_args

28+ logLvl 10 $ "Original: \n" ++

29+ showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)

30+ let parg = case lookupCtxt Nothing n (idris_implicits i) of

31+ (p : _) -> p

32+ _ -> repeat (pexp Placeholder)

33+ let new = mnub i $ filter (noMatch i) $ mkClauses parg all_args

34+ logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)

35+ return (map (\t -> PClause n t [] PImpossible []) new)

36+ where getLHS i term

37+ | (f, args) <- unApply term = map (\t -> delab' i t True) args

38+ | otherwise = []

39+

40+ lhsApp (PClause _ l _ _ _) = l

41+ lhsApp (PWith _ l _ _ _) = l

42+

43+ mnub i [] = []

44+ mnub i (x : xs) =

45+ if (any (\t -> case matchClause x t of

46+ Right _ -> True

47+ Left _ -> False) xs) then mnub i xs

48+ else x : mnub i xs

49+

50+ noMatch i tm = all (\x -> case matchClause (delab' i x True) tm of

51+ Right _ -> False

52+ Left miss -> True) xs

53+

54+

55+ mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]

56+ mkClauses parg args

57+ = do args' <- mkArg args

58+ let tm = PApp fc (PRef fc n) (zipWith upd args' parg)

59+ return tm

60+ where

61+ mkArg :: [[PTerm]] -> [[PTerm]]

62+ mkArg [] = return []

63+ mkArg (a : as) = do a' <- a

64+ as' <- mkArg as

65+ return (a':as')

66+

67+genAll :: IState -> [PTerm] -> [PTerm]

68+genAll i args = concatMap otherPats (nub args)

69+ where

70+ otherPats :: PTerm -> [PTerm]

71+ otherPats o@(PRef fc n) = ops fc n [] o

72+ otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o

73+ otherPats arg = return arg

74+

75+ ops fc n xs o

76+ | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)

77+ = do xs' <- mapM otherPats (map getTm xs)

78+ let p = PApp fc (PRef fc n) (zipWith upd xs' xs)

79+ let tyn = getTy n (tt_ctxt i)

80+ case lookupCtxt Nothing tyn (idris_datatypes i) of

81+ (TI ns : _) -> p : map (mkPat fc) (ns \\ [n])

82+ _ -> [p]

83+ ops fc n arg o = return o

84+

85+ getTy n ctxt = case lookupTy Nothing n ctxt of

86+ (t : _) -> case unApply (getRetTy t) of

87+ (P _ tyn _, _) -> tyn

88+ x -> error $ "Can't happen getTy 1 " ++ show (n, x)

89+ _ -> error "Can't happen getTy 2"

90+

91+ mkPat fc x = case lookupCtxt Nothing x (idris_implicits i) of

92+ (pargs : _)

93+ -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)

94+ _ -> error "Can't happen - genAll"

95+

96+upd p' p = p { getTm = p' }

11

97

src/Idris/DataOpts.hs+7

@@ -45,6 +45,13 @@ forceArgs n t = do let fargs = force 0 t

45 = mapMaybe isF args ++ concatMap guarded args

46 guarded t = mapMaybe isF [t]

47

48+-- Calculate whether a collection of constructors is collapsible

49+

50+collapseCons :: Name -> [(Name, Type)] -> Idris ()

51+collapseCons ty cons =

52+ do i <- getIState

53+ return ()

54+

48class Optimisable term where

55class Optimisable term where

49 applyOpts :: term -> Idris term

56 applyOpts :: term -> Idris term

50

57

src/Idris/ElabDecls.hs+22−13

@@ -76,6 +76,7 @@ elabData info syn fc (PDatadecl n t_in dcons)

76 (idris_datatypes i) })

77 addIBC (IBCDef n)

78 addIBC (IBCData n)

79+ collapseCons n cons

79 updateContext (addDatatype (Data n ttag cty cons))

80 updateContext (addDatatype (Data n ttag cty cons))

80

81

81elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

82elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

@@ -100,9 +101,8 @@ elabCon info syn (n, t_in, fc)

100 return (n, cty)

101 return (n, cty)

101

102

102elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

103elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

103−elabClauses info fc opts n_in cs_in = let n = liftname info n_in in

104+elabClauses info fc opts n_in cs = let n = liftname info n_in in

104− do let cs = genClauses cs_in

105− pats_in <- mapM (elabClause info fc (TCGen `elem` opts)) cs

105+ do pats_in <- mapM (elabClause info fc (TCGen `elem` opts)) cs

106 solveDeferred n

107 let pats = mapMaybe id pats_in

108 logLvl 3 (showSep "\n" (map (\ (l,r) ->

@@ -111,9 +111,19 @@ elabClauses info fc opts n_in cs_in = let n = liftname info n_in in

111 ist <- get

112 let tcase = opt_typecase (idris_options ist)

113 let pdef = map debind (map (simpl (tt_ctxt ist)) pats)

114+ cov <- coverage

115+ pcover <-

116+ if cov

117+ then idrisCatch

118+ (do missing <- genClauses fc n (map fst pdef) cs

119+ mapM_ (elabClause info fc True) missing

120+ return True)

121+ (\c -> do -- iputStrLn $ "Warning: " ++ show c

122+ return False)

123+ else return False

114 pdef' <- applyOpts pdef

124 pdef' <- applyOpts pdef

115− let tree = simpleCase tcase pdef

125+ let tree = simpleCase tcase pcover pdef

116− let tree' = simpleCase tcase pdef'

126+ let tree' = simpleCase tcase pcover pdef'

117 tclift $ sameLength pdef

127 tclift $ sameLength pdef

118 logLvl 3 (show tree)

128 logLvl 3 (show tree)

119 logLvl 3 $ "Optimised: " ++ show tree'

129 logLvl 3 $ "Optimised: " ++ show tree'

@@ -122,7 +132,7 @@ elabClauses info fc opts n_in cs_in = let n = liftname info n_in in

122 put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })

132 put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })

123 case lookupTy (namespace info) n ctxt of

133 case lookupTy (namespace info) n ctxt of

124 [ty] -> do updateContext (addCasedef n (inlinable opts)

134 [ty] -> do updateContext (addCasedef n (inlinable opts)

125− tcase pdef pdef' ty)

135+ tcase pcover pdef pdef' ty)

126 addIBC (IBCDef n)

136 addIBC (IBCDef n)

127 [] -> return ()

137 [] -> return ()

128 where

138 where

@@ -160,7 +170,11 @@ elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])

160 -- if the LHS type checks, it is possible, so report an error

170 -- if the LHS type checks, it is possible, so report an error

161 case elaborate ctxt (MN 0 "patLHS") infP []

171 case elaborate ctxt (MN 0 "patLHS") infP []

162 (erun fc (buildTC i info True tcgen fname (infTerm lhs))) of

172 (erun fc (buildTC i info True tcgen fname (infTerm lhs))) of

173+ OK ((lhs', _, _), _) ->

174+ do let lhs_tm = orderPats (getInferTerm lhs')

175+ checkInferred fc (delab' i lhs_tm True) lhs

163− OK _ -> fail $ show fc ++ ":" ++ show lhs ++ " is a possible case"

176+ fail $ show fc ++ ":" ++ showImp True (delab' i lhs_tm True) ++ " is a possible case"

177+ ++ "\n" ++ showImp True lhs

164 Error _ -> return ()

178 Error _ -> return ()

165 return Nothing

179 return Nothing

166elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

180elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

@@ -555,11 +569,6 @@ pbty _ tm = tm

555getPBtys (Bind n (PVar t) sc) = (n, t) : getPBtys sc

569getPBtys (Bind n (PVar t) sc) = (n, t) : getPBtys sc

556getPBtys _ = []

570getPBtys _ = []

557

571

558−getRetTy (Bind n (PVar _) sc) = getRetTy sc

559−getRetTy (Bind n (PVTy _) sc) = getRetTy sc

560−getRetTy (Bind n (Pi _) sc) = getRetTy sc

561−getRetTy sc = sc

562−

563psolve (Bind n (PVar t) sc) = do solve; psolve sc

572psolve (Bind n (PVar t) sc) = do solve; psolve sc

564psolve tm = return ()

573psolve tm = return ()

565

574

@@ -617,7 +626,7 @@ checkInferred fc inf user =

617 do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++

626 do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++

618 showImp True user

627 showImp True user

619 tclift $ case matchClause user inf of

628 tclift $ case matchClause user inf of

620− Right _ -> return ()

629+ Right vs -> return ()

621 Left (x, y) -> tfail $ At fc

630 Left (x, y) -> tfail $ At fc

622 (Msg $ "The type-checked term and given term do not match: "

631 (Msg $ "The type-checked term and given term do not match: "

623 ++ show x ++ " and " ++ show y)

632 ++ show x ++ " and " ++ show y)

src/Idris/IBC.hs+1−1

@@ -22,7 +22,7 @@ import System.Directory

22import Paths_idris

23

24ibcVersion :: Word8

25−ibcVersion = 7

25+ibcVersion = 8

26

27data IBCFile = IBCFile { ver :: Word8,

28 sourcefile :: FilePath,

src/Idris/Prover.hs+2−2

@@ -39,11 +39,11 @@ prove ctxt n ty

39 iputStrLn $ showProof n prf

40 i <- get

41 put (i { last_proof = Just (n, prf) })

42− let tree = simpleCase False [(P Ref n ty, tm)]

42+ let tree = simpleCase False True [(P Ref n ty, tm)]

43 logLvl 3 (show tree)

44 (ptm, pty) <- recheckC ctxt (FC "proof" 0) [] tm

45 ptm' <- applyOpts ptm

46− updateContext (addCasedef n True False [(P Ref n ty, ptm)]

46+ updateContext (addCasedef n True False True [(P Ref n ty, ptm)]

47 [(P Ref n ty, ptm')] ty)

48 solveDeferred n

49

src/Main.hs+3

@@ -38,6 +38,7 @@ data Opt = Filename String

38 | Output String

39 | TypeCase

40 | TypeInType

41+ | NoCoverage

41 | Verbose

42 | Verbose

42 deriving Eq

43 deriving Eq

43

44

@@ -73,6 +74,7 @@ runIdris opts =

73 makeOption (OLogging i) = setLogLevel i

74 makeOption (OLogging i) = setLogLevel i

74 makeOption TypeCase = setTypeCase True

75 makeOption TypeCase = setTypeCase True

75 makeOption TypeInType = setTypeInType True

76 makeOption TypeInType = setTypeInType True

77+ makeOption NoCoverage = setCoverage False

76 makeOption _ = return ()

78 makeOption _ = return ()

77

79

78getFile :: Opt -> Maybe String

80getFile :: Opt -> Maybe String

@@ -100,6 +102,7 @@ parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)

100parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)

102parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)

101parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)

103parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)

102parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)

104parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)

105+parseArgs ("--nocoverage":ns) = liftM (NoCoverage : ) (parseArgs ns)

103parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)

106parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)

104parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)

107parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)

105parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)

108parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)