f6bebd3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Proper pretty-printing of dependent pairs

f6bebd3David Raymond Christiansen13 years ago

src/Idris/AbsSyntax.hs+20−20

compare with master

unifiedsplit

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

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

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

848 -- 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)

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

851 = 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))

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

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

855 en (PTyped l r) = PTyped (en l) (en r)

856 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)

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

859 en (PHidden t) = PHidden (en t)

860 en (PUnifyLog t) = PUnifyLog (en t)

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

948 bnames (PRef _ n) = [n]

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

950 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

952 bnames _ = []

953

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

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

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

1014 pri (PTyped l r) = pri l

1015 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)))

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

1018 pri (PConstant _) = 0

1019 pri Placeholder = 1

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

1191 = do (decls, ns) <- get

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

1193 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)

1195 = do (decls, ns) <- get

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

1197 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)

1199 = do (decls, ns) <- get

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

1201 namesIn uvars ist r

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

1261 = let l' = ai env ds l

1262 r' = ai env ds r in

1263 PPair fc p l' r'

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

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

1265 = let l' = ai env ds l

1266 t' = ai env ds t

1267 r' = ai env ds r in

1268− PDPair fc l' t' r'

1268+ PDPair fc p l' t' r'

1269 ai env ds (PAlternative a as)

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

1271 PAlternative a as'

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

1461 if null alts' then Placeholder

1462 else PAlternative b alts'

1463 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)

1465 su t = t

1466stripUnmatchable i tm = tm

1467

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

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

1573 mr <- match' r r'

1574 return (ml ++ mr)

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

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

1576− mt <- match' t t'

1576+ mt <- match' t t'

1577− mr <- match' r r'

1577+ mr <- match' r r'

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

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

1579 match (PAlternative a as) (PAlternative a' as')

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

1581 return (concat ms)

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

1653 (fmap (sm xs) tm)

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

1655 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)

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

1658 sm xs (PHidden x) = PHidden (sm xs x)

1659 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

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

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

1677 sm (PTyped x y) = PTyped (sm x) (sm y)

1678 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)

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

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

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

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

1749 mkUniq (PPair fc p l r)

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

1751 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)

1753 | t /= Placeholder

1754 = do env <- get

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

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

1759 put (n' : env)

1760 t' <- mkUniq t

1761 sc'' <- mkUniq sc'

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

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

1763− mkUniq (PDPair fc l t r)

1763+ mkUniq (PDPair fc p l t r)

1764 = 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'

1766 mkUniq (PAlternative b as)

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

1768 mkUniq (PHidden t) = liftM PHidden (mkUniq t)

src/Idris/AbsSyntaxTree.hs+30−12

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

625 | PEq FC PTerm PTerm

626 | PRewrite FC PTerm PTerm (Maybe PTerm)

627 | PPair FC PunInfo PTerm PTerm

628− | PDPair FC PTerm PTerm PTerm

628+ | PDPair FC PunInfo PTerm PTerm PTerm

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

630 | PHidden PTerm -- ^ Irrelevant or hidden pattern

631 | PType

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

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

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

667 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)

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

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

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

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

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

1184 prettySe 10 bnd r <>

1185 annotate (AnnName pairCon Nothing Nothing) rparen

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

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

1187 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

1188 prettySe p bnd (PAlternative a as) =

1206 prettySe p bnd (PAlternative a as) =

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

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

1190 where

1208 where

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

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

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

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

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

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

1423 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

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

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

1408 size (PHidden hidden) = size hidden

1426 size (PHidden hidden) = size hidden

1409 size (PUnifyLog tm) = size tm

1427 size (PUnifyLog tm) = size tm

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

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

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

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

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

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

1462 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

1463+ 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

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

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

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

1448 ni env (PUnifyLog tm) = ni env tm

1466 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1470 ni (PHidden tm) = ni tm

1488 ni (PHidden tm) = ni tm

1471 ni (PUnifyLog tm) = ni tm

1489 ni (PUnifyLog tm) = ni tm

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

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

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

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

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

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

1511 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

1512+ 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

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

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

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

1497 ni env (PHidden tm) = ni env tm

1515 ni env (PHidden tm) = ni env tm

1498 ni env (PUnifyLog tm) = ni env tm

1516 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

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

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

1539 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

1540+ 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

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

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

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

1525 ni env (PHidden tm) = ni env tm

1543 ni env (PHidden tm) = ni env tm

1526 ni env (PUnifyLog tm) = ni env tm

1544 ni env (PUnifyLog tm) = ni env tm

src/Idris/Coverage.hs+2−2

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

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

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

171 [pexp l, pexp r]) o

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

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

173 = ops fc (sUN "Ex_intro")

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

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

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

193 -- put it back to its original form

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

195 | ei == txt "Ex_intro"

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

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

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

198 | n == pairCon

199 = 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)

38 (map (pmap (expandDo dsl)) opts)

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

40expandDo 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)

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

42− (expandDo dsl r)

42+ (expandDo dsl r)

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

44expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

45expandDo dsl (PNoImplicits t) = PNoImplicits (expandDo dsl t)

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

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

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

96 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)

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

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

100 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

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

148 r' <- db' r

149 return (PPair fc p l' r')

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

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

151− r' <- db' r

151+ r' <- db' r

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

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

153 db' t = return t

154

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

src/Idris/DeepSeq.hs+2−2

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

165 rnf (PRewrite x1 x2 x3 x4)

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

167 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)

168+ rnf (PDPair x1 x2 x3 x4 x5)

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

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

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

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

172 rnf PType = ()

src/Idris/Delaborate.hs+2−2

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

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

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

90 | n == sUN "Exists"

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

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

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

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

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

95 | 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

97 (de env [] r)

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

99 = case lookup n (idris_metavars ist) of

src/Idris/ElabTerm.hs+5−5

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

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

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

207 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)

209 = case t of

210 Placeholder ->

211 do hnf_compute

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

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

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

223 pexp l, pexp r])

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

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

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

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

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

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

227− pexp l, pexp r])

227+ pexp l, pexp r])

228 elab' ina (PAlternative True as)

229 = do hnf_compute

230 ty <- goal

src/Idris/IBC.hs+9−7

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

28ibcVersion :: Word8

29−ibcVersion = 59

29+ibcVersion = 60

32data IBCFile = IBCFile { ver :: Word8,

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

1611 put x2

1612 put x3

1613 put x4

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

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

1615− put x1

1615+ put x1

1616− put x2

1616+ put x2

1617− put x3

1617+ put x3

1618− put x4

1618+ put x4

1619+ put x5

1619 PAlternative x1 x2 -> do putWord8 20

1620 PAlternative x1 x2 -> do putWord8 20

1620 put x1

1621 put x1

1621 put x2

1622 put x2

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

1728 x2 <- get

1729 x2 <- get

1729 x3 <- get

1730 x3 <- get

1730 x4 <- get

1731 x4 <- get

1732+ x5 <- get

1731− return (PDPair x1 x2 x3 x4)

1733+ return (PDPair x1 x2 x3 x4 x5)

1732 20 -> do x1 <- get

1734 20 -> do x1 <- get

1733 x2 <- get

1735 x2 <- get

1734 return (PAlternative x1 x2)

1736 return (PAlternative x1 x2)

src/Idris/ParseExpr.hs+4−4

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

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

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

160 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)

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

163 update ns (PHidden t) = PHidden (update ns t)

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

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

349 fc <- getFC

350 r <- expr syn

351 lchar ')'

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

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

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

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

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

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

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

370 <|> do l <- expr syn

371 bracketedExpr syn l

372−

372+

373bracketedExpr :: SyntaxInfo -> PTerm -> IdrisParser PTerm

374bracketedExpr syn e =

375 do lchar ')'; return e

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

384 return fc

385 r <- expr syn

386 lchar ')'

387− return (PDPair fc e Placeholder r)

387+ return (PDPair fc TypeOrTerm e Placeholder r)

388 <?> "end of bracketed expression"

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

390 mergePairs [(t, fc)] = t