Skip to content

Commit 3e3a4e1

Browse files
nickdrozdnickdrozd
authored
Use truncated case notation (#1562)
1 parent c04835c commit 3e3a4e1

File tree

10 files changed

+188
-190
lines changed

10 files changed

+188
-190
lines changed

‎src/Compiler/ANF.idr

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -188,9 +188,9 @@ mutual
188188
= anfArgs fc vs args (AUnderApp fc n m)
189189
anf vs (LApp fc lazy f a)
190190
= anfArgs fc vs [f, a]
191-
(\args => case args of
192-
[fvar, avar] => AApp fc lazy fvar avar
193-
_ => ACrash fc "Can't happen (AApp)")
191+
\case
192+
[fvar, avar] => AApp fc lazy fvar avar
193+
_ => ACrash fc "Can't happen (AApp)"
194194
anf vs (LLet fc x val sc)
195195
= do i <- nextVar
196196
let vs' = i :: vs

‎src/Core/AutoSearch.idr

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -138,9 +138,9 @@ anyOne : {vars : _} ->
138138
anyOne fc env top [] = throw (CantSolveGoal fc [] top)
139139
anyOne fc env top [elab]
140140
= catch elab
141-
(\err => case err of
142-
CantSolveGoal _ _ _ => throw err
143-
_ => throw (CantSolveGoal fc [] top))
141+
\case
142+
err@(CantSolveGoal _ _ _) => throw err
143+
_ => throw $ CantSolveGoal fc [] top
144144
anyOne fc env top (elab :: elabs)
145145
= tryUnify elab (anyOne fc env top elabs)
146146

@@ -152,9 +152,9 @@ exactlyOne : {vars : _} ->
152152
Core (Term vars)
153153
exactlyOne fc env top target [elab]
154154
= catch elab
155-
(\err => case err of
156-
CantSolveGoal _ _ _ => throw err
157-
_ => throw (CantSolveGoal fc [] top))
155+
\case
156+
err@(CantSolveGoal _ _ _) => throw err
157+
_ => throw $ CantSolveGoal fc [] top
158158
exactlyOne {vars} fc env top target all
159159
= do elabs <- successful all
160160
case rights elabs of

‎src/Core/CaseBuilder.idr

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -757,9 +757,9 @@ getScore : {ns : _} ->
757757
getScore fc phase name npss
758758
= do catch (do sameType fc phase name (mkEnv fc ns) npss
759759
pure (Right ()))
760-
(\err => case err of
761-
CaseCompile _ _ err => pure (Left err)
762-
_ => throw err)
760+
\case
761+
CaseCompile _ _ err => pure $ Left err
762+
err => throw err
763763

764764
-- Pick the leftmost matchable thing with all constructors in the
765765
-- same family, or all variables, or all the same type constructor.

‎src/Core/Core.idr

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -448,11 +448,7 @@ coreFail e = MkCore (pure (Left e))
448448

449449
export
450450
wrapError : (Error -> Error) -> Core a -> Core a
451-
wrapError fe (MkCore prog)
452-
= MkCore (prog >>=
453-
(\x => pure $ case x of
454-
Left err => Left (fe err)
455-
Right val => Right val))
451+
wrapError fe (MkCore prog) = MkCore $ mapFst fe <$> prog
456452

457453
-- This would be better if we restrict it to a limited set of IO operations
458454
export
@@ -498,9 +494,9 @@ export %inline
498494
(>>=) : Core a -> (a -> Core b) -> Core b
499495
(>>=) (MkCore act) f
500496
= MkCore (act >>=
501-
(\x => case x of
502-
Left err => pure (Left err)
503-
Right val => runCore (f val)))
497+
\case
498+
Left err => pure $ Left err
499+
Right val => runCore $ f val)
504500

505501
export %inline
506502
(>>) : Core () -> Core a -> Core a

‎src/Core/Unify.idr

Lines changed: 14 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1437,18 +1437,20 @@ retryGuess mode smode (hid, (loc, hname))
14371437
ignore $ addDef (Resolved hid) gdef
14381438
removeGuess hid
14391439
pure True)
1440-
(\err => case err of
1441-
DeterminingArg _ n i _ _ =>
1442-
do logTerm "unify.retry" 5 ("Failed (det " ++ show hname ++ " " ++ show n ++ ")")
1443-
(type def)
1444-
setInvertible loc (Resolved i)
1445-
pure False -- progress not made yet!
1446-
_ => do logTermNF "unify.retry" 5 ("Search failed at " ++ show rig ++ " for " ++ show hname)
1447-
[] (type def)
1448-
case smode of
1449-
LastChance =>
1450-
throw !(normaliseErr err)
1451-
_ => pure False) -- Postpone again
1440+
\case
1441+
DeterminingArg _ n i _ _ =>
1442+
do logTerm "unify.retry" 5
1443+
("Failed (det " ++ show hname ++ " " ++ show n ++ ")")
1444+
(type def)
1445+
setInvertible loc (Resolved i)
1446+
pure False -- progress not made yet!
1447+
err =>
1448+
do logTermNF "unify.retry" 5
1449+
("Search failed at " ++ show rig ++ " for " ++ show hname)
1450+
[] (type def)
1451+
case smode of
1452+
LastChance => throw !(normaliseErr err)
1453+
_ => pure False -- Postpone again
14521454
Guess tm envb [constr] =>
14531455
do let umode = case smode of
14541456
MatchArgs => inMatch

‎src/Parser/Rule/Package.idr

Lines changed: 55 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -20,117 +20,119 @@ EmptyRule = Grammar () Token False
2020
export
2121
equals : Rule ()
2222
equals = terminal "Expected equals"
23-
(\x => case x of
24-
Equals => Just ()
25-
_ => Nothing)
23+
\case
24+
Equals => Just ()
25+
_ => Nothing
2626

2727
export
2828
lte : Rule ()
2929
lte = terminal "Expected <="
30-
(\x => case x of
31-
LTE => Just ()
32-
_ => Nothing)
30+
\case
31+
LTE => Just ()
32+
_ => Nothing
3333

3434
export
3535
gte : Rule ()
3636
gte = terminal "Expected >="
37-
(\x => case x of
38-
GTE => Just ()
39-
_ => Nothing)
37+
\case
38+
GTE => Just ()
39+
_ => Nothing
4040

4141
export
4242
lt : Rule ()
4343
lt = terminal "Expected <="
44-
(\x => case x of
45-
LT => Just ()
46-
_ => Nothing)
44+
\case
45+
LT => Just ()
46+
_ => Nothing
4747

4848
export
4949
gt : Rule ()
5050
gt = terminal "Expected >="
51-
(\x => case x of
52-
GT => Just ()
53-
_ => Nothing)
51+
\case
52+
GT => Just ()
53+
_ => Nothing
5454

5555
export
5656
eqop : Rule ()
5757
eqop = terminal "Expected =="
58-
(\x => case x of
59-
EqOp => Just ()
60-
_ => Nothing)
58+
\case
59+
EqOp => Just ()
60+
_ => Nothing
6161

6262
export
6363
andop : Rule ()
6464
andop = terminal "Expected &&"
65-
(\x => case x of
66-
AndOp => Just ()
67-
_ => Nothing)
65+
\case
66+
AndOp => Just ()
67+
_ => Nothing
6868

6969
export
7070
eoi : Rule ()
7171
eoi = terminal "Expected end of input"
72-
(\x => case x of
73-
EndOfInput => Just ()
74-
_ => Nothing)
72+
\case
73+
EndOfInput => Just ()
74+
_ => Nothing
7575

7676
export
7777
exactProperty : String -> Rule String
78-
exactProperty p = terminal ("Expected property " ++ p)
79-
(\x => case x of
80-
DotSepIdent Nothing p' =>
81-
if p == p' then Just p
82-
else Nothing
83-
_ => Nothing)
78+
exactProperty p = terminal ("Expected property " ++ p) $
79+
\case
80+
DotSepIdent Nothing p' =>
81+
if p == p' then Just p else Nothing
82+
_ => Nothing
8483

8584
export
8685
stringLit : Rule String
8786
stringLit = terminal "Expected string"
88-
(\x => case x of
89-
StringLit str => Just str
90-
_ => Nothing)
87+
\case
88+
StringLit str => Just str
89+
_ => Nothing
9190

9291
export
9392
integerLit : Rule Integer
9493
integerLit = terminal "Expected integer"
95-
(\x => case x of
96-
IntegerLit i => Just i
97-
_ => Nothing)
94+
\case
95+
IntegerLit i => Just i
96+
_ => Nothing
9897

9998
export
10099
namespacedIdent : Rule (Maybe Namespace, String)
101100
namespacedIdent = terminal "Expected namespaced identifier"
102-
(\x => case x of
103-
DotSepIdent ns n => Just (ns, n)
104-
_ => Nothing)
101+
\case
102+
DotSepIdent ns n => Just (ns, n)
103+
_ => Nothing
105104

106105
export
107106
moduleIdent : Rule ModuleIdent
108107
moduleIdent = terminal "Expected module identifier"
109-
(\x => case x of
110-
DotSepIdent ns m => Just $ nsAsModuleIdent (mkNestedNamespace ns m)
111-
_ => Nothing)
108+
\case
109+
DotSepIdent ns m =>
110+
Just $ nsAsModuleIdent $
111+
mkNestedNamespace ns m
112+
_ => Nothing
112113

113114
export
114115
packageName : Rule String
115116
packageName = terminal "Expected package name"
116-
(\x => case x of
117-
DotSepIdent Nothing str =>
118-
if isIdent AllowDashes str then Just str
119-
else Nothing
120-
_ => Nothing)
117+
\case
118+
DotSepIdent Nothing str =>
119+
if isIdent AllowDashes str
120+
then Just str
121+
else Nothing
122+
_ => Nothing
121123

122124
export
123125
dot' : Rule ()
124126
dot' = terminal "Expected dot"
125-
(\x => case x of
126-
Dot => Just ()
127-
_ => Nothing)
127+
\case
128+
Dot => Just ()
129+
_ => Nothing
128130

129131
sep' : Rule ()
130132
sep' = terminal "Expected separator"
131-
(\x => case x of
132-
Separator => Just ()
133-
_ => Nothing)
133+
\case
134+
Separator => Just ()
135+
_ => Nothing
134136

135137
export
136138
sep : Rule t -> Rule (List t)

0 commit comments

Comments
 (0)