f6bebd3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Proper pretty-printing of dependent pairs

* Dependent pairs are properly highlighted as either constructors or types * Names bound in dependent pair types show up as bound in their scope

commitf6bebd300ea7427b8588ae29c4ec9ee53dd23358 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 7 Feb 2014, 16:32 (13 years ago) parent3921855

9 files changed+80−60

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+20−20 src/Idris/AbsSyntaxTree.hs+30−12 src/Idris/Coverage.hs+2−2 src/Idris/DSL.hs+6−6 src/Idris/DeepSeq.hs+2−2 src/Idris/Delaborate.hs+2−2 src/Idris/ElabTerm.hs+5−5 src/Idris/IBC.hs+9−7 src/Idris/ParseExpr.hs+4−4

src/Idris/AbsSyntax.hs+20−20

@@ -846,15 +846,15 @@ expandParams dec ps ns infs tm = en tm

846846 PLet n' (en ty) (en v) (en (shadow n n' s))

847847 | otherwise = PLet n (en ty) (en v) (en s)

848848 -- FIXME: Should only do this in a type signature!

849− en (PDPair f (PRef f' n) t r)

849+ en (PDPair f p (PRef f' n) t r)

850850 | n `elem` (map fst ps ++ ns) && t /= Placeholder

851851 = let n' = mkShadow n in

852− PDPair f (PRef f' n') (en t) (en (shadow n n' r))

852+ PDPair f p (PRef f' n') (en t) (en (shadow n n' r))

853853 en (PEq f l r) = PEq f (en l) (en r)

854854 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)

855855 en (PTyped l r) = PTyped (en l) (en r)

856856 en (PPair f p l r) = PPair f p (en l) (en r)

857− en (PDPair f l t r) = PDPair f (en l) (en t) (en r)

857+ en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)

858858 en (PAlternative a as) = PAlternative a (map en as)

859859 en (PHidden t) = PHidden (en t)

860860 en (PUnifyLog t) = PUnifyLog (en t)

@@ -948,7 +948,7 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

948948 bnames (PRef _ n) = [n]

949949 bnames (PApp _ _ args) = concatMap bnames (map getTm args)

950950 bnames (PPair _ _ l r) = bnames l ++ bnames r

951− bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r

951+ bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r

952952 bnames _ = []

953953

954954expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)

@@ -1013,7 +1013,7 @@ getPriority i tm = 1 -- pri tm

10131013 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))

10141014 pri (PTyped l r) = pri l

10151015 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))

1016− pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

1016+ pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

10171017 pri (PAlternative a as) = maximum (map pri as)

10181018 pri (PConstant _) = 0

10191019 pri Placeholder = 1

@@ -1191,11 +1191,11 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

11911191 = do (decls, ns) <- get

11921192 let isn = namesIn uvars ist l ++ namesIn uvars ist r

11931193 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1194− imps top env (PDPair _ (PRef _ n) t r)

1194+ imps top env (PDPair _ _ (PRef _ n) t r)

11951195 = do (decls, ns) <- get

11961196 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]

11971197 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

1198− imps top env (PDPair _ l t r)

1198+ imps top env (PDPair _ _ l t r)

11991199 = do (decls, ns) <- get

12001200 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++

12011201 namesIn uvars ist r

@@ -1261,11 +1261,11 @@ addImpl' inpat env infns ist ptm

12611261 = let l' = ai env ds l

12621262 r' = ai env ds r in

12631263 PPair fc p l' r'

1264− ai env ds (PDPair fc l t r)

1264+ ai env ds (PDPair fc p l t r)

12651265 = let l' = ai env ds l

12661266 t' = ai env ds t

12671267 r' = ai env ds r in

1268− PDPair fc l' t' r'

1268+ PDPair fc p l' t' r'

12691269 ai env ds (PAlternative a as)

12701270 = let as' = map (ai env ds) as in

12711271 PAlternative a as'

@@ -1461,7 +1461,7 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

14611461 if null alts' then Placeholder

14621462 else PAlternative b alts'

14631463 su (PPair fc p l r) = PPair fc p (su l) (su r)

1464− su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)

1464+ su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)

14651465 su t = t

14661466stripUnmatchable i tm = tm

14671467

@@ -1572,10 +1572,10 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

15721572 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'

15731573 mr <- match' r r'

15741574 return (ml ++ mr)

1575− match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'

1576− mt <- match' t t'

1577− mr <- match' r r'

1578− return (ml ++ mt ++ mr)

1575+ match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'

1576+ mt <- match' t t'

1577+ mr <- match' r r'

1578+ return (ml ++ mt ++ mr)

15791579 match (PAlternative a as) (PAlternative a' as')

15801580 = do ms <- zipWithM match' as as'

15811581 return (concat ms)

@@ -1653,7 +1653,7 @@ substMatchShadow n shs tm t = sm shs t where

16531653 (fmap (sm xs) tm)

16541654 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)

16551655 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)

1656− sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)

1656+ sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)

16571657 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)

16581658 sm xs (PHidden x) = PHidden (sm xs x)

16591659 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

@@ -1676,7 +1676,7 @@ shadow n n' t = sm t where

16761676 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)

16771677 sm (PTyped x y) = PTyped (sm x) (sm y)

16781678 sm (PPair f p x y) = PPair f p (sm x) (sm y)

1679− sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

1679+ sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)

16801680 sm (PAlternative a as) = PAlternative a (map sm as)

16811681 sm (PTactics ts) = PTactics (map (fmap sm) ts)

16821682 sm (PProof ts) = PProof (map (fmap sm) ts)

@@ -1749,7 +1749,7 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

17491749 mkUniq (PPair fc p l r)

17501750 = do l' <- mkUniq l; r' <- mkUniq r

17511751 return $! PPair fc p l' r'

1752− mkUniq (PDPair fc (PRef fc' n) t sc)

1752+ mkUniq (PDPair fc p (PRef fc' n) t sc)

17531753 | t /= Placeholder

17541754 = do env <- get

17551755 (n', sc') <- if n `elem` env

@@ -1759,10 +1759,10 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

17591759 put (n' : env)

17601760 t' <- mkUniq t

17611761 sc'' <- mkUniq sc'

1762− return $! PDPair fc (PRef fc' n') t' sc''

1763− mkUniq (PDPair fc l t r)

1762+ return $! PDPair fc p (PRef fc' n') t' sc''

1763+ mkUniq (PDPair fc p l t r)

17641764 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r

1765− return $! PDPair fc l' t' r'

1765+ return $! PDPair fc p l' t' r'

17661766 mkUniq (PAlternative b as)

17671767 = liftM (PAlternative b) (mapM mkUniq as)

17681768 mkUniq (PHidden t) = liftM PHidden (mkUniq t)

src/Idris/AbsSyntaxTree.hs+30−12

@@ -625,7 +625,7 @@ data PTerm = PQuote Raw

625625 | PEq FC PTerm PTerm

626626 | PRewrite FC PTerm PTerm (Maybe PTerm)

627627 | PPair FC PunInfo PTerm PTerm

628− | PDPair FC PTerm PTerm PTerm

628+ | PDPair FC PunInfo PTerm PTerm PTerm

629629 | PAlternative Bool [PTerm] -- True if only one may work

630630 | PHidden PTerm -- ^ Irrelevant or hidden pattern

631631 | PType

@@ -665,7 +665,7 @@ mapPT f t = f (mpt t) where

665665 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

666666 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

667667 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)

668− mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)

668+ mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)

669669 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)

670670 mpt (PHidden t) = PHidden (mapPT f t)

671671 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)

@@ -1183,8 +1183,26 @@ pprintPTerm impl bnd = prettySe 10 bnd

11831183 annotate (AnnName pairCon Nothing Nothing) comma <+>

11841184 prettySe 10 bnd r <>

11851185 annotate (AnnName pairCon Nothing Nothing) rparen

1186− prettySe p bnd (PDPair _ l t r) =

1186+ prettySe p bnd (PDPair _ TypeOrTerm l t r) =

11871187 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen

1188+ prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =

1189+ annotate (AnnName sigmaTy Nothing Nothing) lparen <>

1190+ bindingOf n False <+>

1191+ annotate (AnnName sigmaTy Nothing Nothing) (text "**") <+>

1192+ prettySe 10 ((n, False):bnd) r <>

1193+ annotate (AnnName sigmaTy Nothing Nothing) rparen

1194+ prettySe p bnd (PDPair _ IsType l t r) =

1195+ annotate (AnnName sigmaTy Nothing Nothing) lparen <>

1196+ prettySe 10 bnd l <+>

1197+ annotate (AnnName sigmaTy Nothing Nothing) (text "**") <+>

1198+ prettySe 10 bnd r <>

1199+ annotate (AnnName sigmaTy Nothing Nothing) rparen

1200+ prettySe p bnd (PDPair _ IsTerm l t r) =

1201+ annotate (AnnName existsCon Nothing Nothing) lparen <>

1202+ prettySe 10 bnd l <+>

1203+ annotate (AnnName existsCon Nothing Nothing) (text "**") <+>

1204+ prettySe 10 bnd r <>

1205+ annotate (AnnName existsCon Nothing Nothing) rparen

11881206 prettySe p bnd (PAlternative a as) =

11891207 lparen <> text "|" <> prettyAs <> text "|" <> rparen

11901208 where

@@ -1403,7 +1421,7 @@ instance Sized PTerm where

14031421 size (PEq fc left right) = 1 + size left + size right

14041422 size (PRewrite fc left right _) = 1 + size left + size right

14051423 size (PPair fc _ left right) = 1 + size left + size right

1406− size (PDPair fs left ty right) = 1 + size left + size ty + size right

1424+ size (PDPair fs _ left ty right) = 1 + size left + size ty + size right

14071425 size (PAlternative a alts) = 1 + size alts

14081426 size (PHidden hidden) = size hidden

14091427 size (PUnifyLog tm) = size tm

@@ -1442,8 +1460,8 @@ allNamesIn tm = nub $ ni [] tm

14421460 ni env (PRewrite _ l r _) = ni env l ++ ni env r

14431461 ni env (PTyped l r) = ni env l ++ ni env r

14441462 ni env (PPair _ _ l r) = ni env l ++ ni env r

1445− ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1446− ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1463+ ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1464+ ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r

14471465 ni env (PAlternative a ls) = concatMap (ni env) ls

14481466 ni env (PUnifyLog tm) = ni env tm

14491467 ni env (PDisamb _ tm) = ni env tm

@@ -1464,8 +1482,8 @@ boundNamesIn tm = nub $ ni tm

14641482 ni (PRewrite _ l r _) = ni l ++ ni r

14651483 ni (PTyped l r) = ni l ++ ni r

14661484 ni (PPair _ _ l r) = ni l ++ ni r

1467− ni (PDPair _ (PRef _ n) t r) = ni t ++ ni r

1468− ni (PDPair _ l t r) = ni l ++ ni t ++ ni r

1485+ ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r

1486+ ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r

14691487 ni (PAlternative a as) = concatMap (ni) as

14701488 ni (PHidden tm) = ni tm

14711489 ni (PUnifyLog tm) = ni tm

@@ -1491,8 +1509,8 @@ namesIn uvars ist tm = nub $ ni [] tm

14911509 ni env (PRewrite _ l r _) = ni env l ++ ni env r

14921510 ni env (PTyped l r) = ni env l ++ ni env r

14931511 ni env (PPair _ _ l r) = ni env l ++ ni env r

1494− ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1495− ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1512+ ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1513+ ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r

14961514 ni env (PAlternative a as) = concatMap (ni env) as

14971515 ni env (PHidden tm) = ni env tm

14981516 ni env (PUnifyLog tm) = ni env tm

@@ -1519,8 +1537,8 @@ usedNamesIn vars ist tm = nub $ ni [] tm

15191537 ni env (PRewrite _ l r _) = ni env l ++ ni env r

15201538 ni env (PTyped l r) = ni env l ++ ni env r

15211539 ni env (PPair _ _ l r) = ni env l ++ ni env r

1522− ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1523− ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1540+ ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1541+ ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r

15241542 ni env (PAlternative a as) = concatMap (ni env) as

15251543 ni env (PHidden tm) = ni env tm

15261544 ni env (PUnifyLog tm) = ni env tm

src/Idris/Coverage.hs+2−2

@@ -169,7 +169,7 @@ genAll i args

169169 ([pimp (sUN "A") Placeholder True,

170170 pimp (sUN "B") Placeholder True] ++

171171 [pexp l, pexp r]) o

172− otherPats o@(PDPair fc t _ v)

172+ otherPats o@(PDPair fc p t _ v)

173173 = ops fc (sUN "Ex_intro")

174174 ([pimp (sUN "a") Placeholder True,

175175 pimp (sUN "P") Placeholder True] ++

@@ -193,7 +193,7 @@ genAll i args

193193 -- put it back to its original form

194194 resugar (PApp _ (PRef fc (UN ei)) [_,_,t,v])

195195 | ei == txt "Ex_intro"

196− = PDPair fc (getTm t) Placeholder (getTm v)

196+ = PDPair fc TypeOrTerm (getTm t) Placeholder (getTm v)

197197 resugar (PApp _ (PRef fc n) [_,_,l,r])

198198 | n == pairCon

199199 = PPair fc IsTerm (getTm l) (getTm r)

src/Idris/DSL.hs+6−6

@@ -38,8 +38,8 @@ expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)

3838 (map (pmap (expandDo dsl)) opts)

3939expandDo dsl (PEq fc l r) = PEq fc (expandDo dsl l) (expandDo dsl r)

4040expandDo dsl (PPair fc p l r) = PPair fc p (expandDo dsl l) (expandDo dsl r)

41−expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)

42− (expandDo dsl r)

41+expandDo dsl (PDPair fc p l t r) = PDPair fc p (expandDo dsl l) (expandDo dsl t)

42+ (expandDo dsl r)

4343expandDo dsl (PAlternative a as) = PAlternative a (map (expandDo dsl) as)

4444expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

4545expandDo dsl (PNoImplicits t) = PNoImplicits (expandDo dsl t)

@@ -94,7 +94,7 @@ var dsl n t i = v' i t where

9494 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)

9595 v' i (PEq f l r) = PEq f (v' i l) (v' i r)

9696 v' i (PPair f p l r) = PPair f p (v' i l) (v' i r)

97− v' i (PDPair f l t r) = PDPair f (v' i l) (v' i t) (v' i r)

97+ v' i (PDPair f p l t r) = PDPair f p (v' i l) (v' i t) (v' i r)

9898 v' i (PAlternative a as) = PAlternative a $ map (v' i) as

9999 v' i (PHidden t) = PHidden (v' i t)

100100 v' i (PIdiom f t) = PIdiom f (v' i t)

@@ -147,9 +147,9 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

147147 db' (PPair fc p l r) = do l' <- db' l

148148 r' <- db' r

149149 return (PPair fc p l' r')

150− db' (PDPair fc l t r) = do l' <- db' l

151− r' <- db' r

152− return (PDPair fc l' t r')

150+ db' (PDPair fc p l t r) = do l' <- db' l

151+ r' <- db' r

152+ return (PDPair fc p l' t r')

153153 db' t = return t

154154

155155 dbArg a = do t' <- db' (getTm a)

src/Idris/DeepSeq.hs+2−2

@@ -165,8 +165,8 @@ instance NFData PTerm where

165165 rnf (PRewrite x1 x2 x3 x4)

166166 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

167167 rnf (PPair x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

168− rnf (PDPair x1 x2 x3 x4)

169− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

168+ rnf (PDPair x1 x2 x3 x4 x5)

169+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

170170 rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

171171 rnf (PHidden x1) = rnf x1 `seq` ()

172172 rnf PType = ()

src/Idris/Delaborate.hs+2−2

@@ -88,12 +88,12 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

8888 | n == sUN "lazy" = de env [] r

8989 deFn env (P _ n _) [ty, Bind x (Lam _) r]

9090 | n == sUN "Exists"

91− = PDPair un (PRef un x) (de env [] ty)

91+ = PDPair un IsType (PRef un x) (de env [] ty)

9292 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

9393 deFn env (P _ n _) [_,_,l,r]

9494 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)

9595 | n == eqTy = PEq un (de env [] l) (de env [] r)

96− | n == sUN "Ex_intro" = PDPair un (de env [] l) Placeholder

96+ | n == sUN "Ex_intro" = PDPair un IsTerm (de env [] l) Placeholder

9797 (de env [] r)

9898 deFn env (P _ n _) args | not mvs

9999 = case lookup n (idris_metavars ist) of

src/Idris/ElabTerm.hs+5−5

@@ -205,7 +205,7 @@ elab ist info pattern opts fn tm

205205 [pimp (sMN 0 "A") Placeholder True,

206206 pimp (sMN 0 "B") Placeholder True,

207207 pexp l, pexp r])

208− elab' ina (PDPair fc l@(PRef _ n) t r)

208+ elab' ina (PDPair fc p l@(PRef _ n) t r)

209209 = case t of

210210 Placeholder ->

211211 do hnf_compute

@@ -221,10 +221,10 @@ elab ist info pattern opts fn tm

221221 [pimp (sMN 0 "a") t False,

222222 pimp (sMN 0 "P") Placeholder True,

223223 pexp l, pexp r])

224− elab' ina (PDPair fc l t r) = elab' ina (PApp fc (PRef fc existsCon)

225− [pimp (sMN 0 "a") t False,

226− pimp (sMN 0 "P") Placeholder True,

227− pexp l, pexp r])

224+ elab' ina (PDPair fc p l t r) = elab' ina (PApp fc (PRef fc existsCon)

225+ [pimp (sMN 0 "a") t False,

226+ pimp (sMN 0 "P") Placeholder True,

227+ pexp l, pexp r])

228228 elab' ina (PAlternative True as)

229229 = do hnf_compute

230230 ty <- goal

src/Idris/IBC.hs+9−7

@@ -26,7 +26,7 @@ import Util.Zlib (decompressEither)

2626

2727

2828ibcVersion :: Word8

29−ibcVersion = 59

29+ibcVersion = 60

3030

3131

3232data IBCFile = IBCFile { ver :: Word8,

@@ -1611,11 +1611,12 @@ instance Binary PTerm where

16111611 put x2

16121612 put x3

16131613 put x4

1614− PDPair x1 x2 x3 x4 -> do putWord8 19

1615− put x1

1616− put x2

1617− put x3

1618− put x4

1614+ PDPair x1 x2 x3 x4 x5 -> do putWord8 19

1615+ put x1

1616+ put x2

1617+ put x3

1618+ put x4

1619+ put x5

16191620 PAlternative x1 x2 -> do putWord8 20

16201621 put x1

16211622 put x2

@@ -1728,7 +1729,8 @@ instance Binary PTerm where

17281729 x2 <- get

17291730 x3 <- get

17301731 x4 <- get

1731− return (PDPair x1 x2 x3 x4)

1732+ x5 <- get

1733+ return (PDPair x1 x2 x3 x4 x5)

17321734 20 -> do x1 <- get

17331735 x2 <- get

17341736 return (PAlternative x1 x2)

src/Idris/ParseExpr.hs+4−4

@@ -158,7 +158,7 @@ extension syn (Rule ssym ptm _)

158158 update ns (PAppBind fc t args) = PAppBind fc (update ns t) (map (fmap (update ns)) args)

159159 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)

160160 update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)

161− update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)

161+ update ns (PDPair fc p l t r) = PDPair fc p (update ns l) (update ns t) (update ns r)

162162 update ns (PAlternative a as) = PAlternative a (map (update ns) as)

163163 update ns (PHidden t) = PHidden (update ns t)

164164 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

@@ -349,7 +349,7 @@ bracketed syn =

349349 fc <- getFC

350350 r <- expr syn

351351 lchar ')'

352− return (PDPair fc (PRef fc ln) lty r))

352+ return (PDPair fc TypeOrTerm (PRef fc ln) lty r))

353353 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'

354354 -- No prefix operators! (bit of a hack here...)

355355 if (o == "-" || o == "!")

@@ -369,7 +369,7 @@ bracketed syn =

369369 pexp (PRef fc0 (sMN 1000 "ARG"))]))

370370 <|> do l <- expr syn

371371 bracketedExpr syn l

372−

372+

373373bracketedExpr :: SyntaxInfo -> PTerm -> IdrisParser PTerm

374374bracketedExpr syn e =

375375 do lchar ')'; return e

@@ -384,7 +384,7 @@ bracketedExpr syn e =

384384 return fc

385385 r <- expr syn

386386 lchar ')'

387− return (PDPair fc e Placeholder r)

387+ return (PDPair fc TypeOrTerm e Placeholder r)

388388 <?> "end of bracketed expression"

389389 where mergePairs :: [(PTerm, FC)] -> PTerm

390390 mergePairs [(t, fc)] = t