e80f871 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Annotate and colour pairs and () properly

Now, the delaborator remembers if a particular unit or pair is the type or the constructor, and colours them accordingly.

commite80f871f6bcae6f64c1c4a9907725355213af911 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 4 Feb 2014, 09:55 (13 years ago) parentef16e5a

9 files changed+105−69

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+29−29 src/Idris/AbsSyntaxTree.hs+27−11 src/Idris/Coverage.hs+2−2 src/Idris/DSL.hs+5−5 src/Idris/DeepSeq.hs+5−2 src/Idris/Delaborate.hs+4−4 src/Idris/ElabTerm.hs+3−3 src/Idris/IBC.hs+26−9 src/Idris/ParseExpr.hs+4−4

src/Idris/AbsSyntax.hs+29−29

@@ -848,7 +848,7 @@ expandParams dec ps ns infs tm = en tm

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

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

850850 en (PTyped l r) = PTyped (en l) (en r)

851− en (PPair f l r) = PPair f (en l) (en r)

851+ en (PPair f p l r) = PPair f p (en l) (en r)

852852 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)

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

854854 en (PHidden t) = PHidden (en t)

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

942942

943943 bnames (PRef _ n) = [n]

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

945− bnames (PPair _ l r) = bnames l ++ bnames r

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

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

947947 bnames _ = []

948948

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

998998 ((P Ref _ _):_) -> 1

999999 [] -> 0 -- must be locally bound, if it's not an error...

10001000 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))

1001− pri (PTrue _) = 0

1001+ pri (PTrue _ _) = 0

10021002 pri (PFalse _) = 0

10031003 pri (PRefl _ _) = 1

10041004 pri (PEq _ l r) = max 1 (max (pri l) (pri r))

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

10071007 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

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

10091009 pri (PTyped l r) = pri l

1010− pri (PPair _ l r) = max 1 (max (pri l) (pri r))

1010+ pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))

10111011 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

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

10131013 pri (PConstant _) = 0

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

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

11831183 imps top env (PTyped l r)

11841184 = imps top env l

1185− imps top env (PPair _ l r)

1185+ imps top env (PPair _ _ l r)

11861186 = do (decls, ns) <- get

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

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

@@ -1252,10 +1252,10 @@ addImpl' inpat env infns ist ptm

12521252 = let l' = ai env ds l

12531253 r' = ai env ds r in

12541254 PTyped l' r'

1255− ai env ds (PPair fc l r)

1255+ ai env ds (PPair fc p l r)

12561256 = let l' = ai env ds l

12571257 r' = ai env ds r in

1258− PPair fc l' r'

1258+ PPair fc p l' r'

12591259 ai env ds (PDPair fc l t r)

12601260 = let l' = ai env ds l

12611261 t' = ai env ds t

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

14551455 = let alts' = filter (/= Placeholder) (map su alts) in

14561456 if null alts' then Placeholder

14571457 else PAlternative b alts'

1458− su (PPair fc l r) = PPair fc (su l) (su r)

1458+ su (PPair fc p l r) = PPair fc p (su l) (su r)

14591459 su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)

14601460 su t = t

14611461stripUnmatchable i tm = tm

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

15641564 return (ml ++ mr)

15651565 match (PTyped l r) x = match l x

15661566 match x (PTyped l r) = match x l

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

1568− mr <- match' r r'

1569− return (ml ++ mr)

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

1568+ mr <- match' r r'

1569+ return (ml ++ mr)

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

15711571 mt <- match' t t'

15721572 mr <- match' r r'

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

15871587 match (PTactics _) _ = return []

15881588 match (PRefl _ _) (PRefl _ _) = return []

15891589 match (PResolveTC _) (PResolveTC _) = return []

1590− match (PTrue _) (PTrue _) = return []

1590+ match (PTrue _ _) (PTrue _ _) = return []

15911591 match (PFalse _) (PFalse _) = return []

15921592 match (PReturn _) (PReturn _) = return []

15931593 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'

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

16471647 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)

16481648 (fmap (sm xs) tm)

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

1650− sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)

1650+ sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)

16511651 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)

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

16531653 sm xs (PHidden x) = PHidden (sm xs x)

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

16701670 sm (PEq f x y) = PEq f (sm x) (sm y)

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

16721672 sm (PTyped x y) = PTyped (sm x) (sm y)

1673− sm (PPair f x y) = PPair f (sm x) (sm y)

1673+ sm (PPair f p x y) = PPair f p (sm x) (sm y)

16741674 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

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

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

@@ -1692,13 +1692,13 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

16921692

16931693 -- FIXME: Probably ought to do this for completeness! It's fine as

16941694 -- long as there are no bindings inside tactics though.

1695− mkUniqT tac = return tac

1695+ mkUniqT tac = return tac

16961696

16971697 mkUniq :: PTerm -> State [Name] PTerm

16981698 mkUniq (PLam n ty sc)

16991699 = do env <- get

1700− (n', sc') <-

1701− if n `elem` env

1700+ (n', sc') <-

1701+ if n `elem` env

17021702 then do let n' = uniqueName n (env ++ inScope)

17031703 return (n', shadow n n' sc)

17041704 else return (n, sc)

@@ -1708,8 +1708,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

17081708 return $! PLam n' ty' sc''

17091709 mkUniq (PPi p n ty sc)

17101710 = do env <- get

1711− (n', sc') <-

1712− if n `elem` env

1711+ (n', sc') <-

1712+ if n `elem` env

17131713 then do let n' = uniqueName n (env ++ inScope)

17141714 return (n', shadow n n' sc)

17151715 else return (n, sc)

@@ -1719,8 +1719,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

17191719 return $! PPi p n' ty' sc''

17201720 mkUniq (PLet n ty val sc)

17211721 = do env <- get

1722− (n', sc') <-

1723− if n `elem` env

1722+ (n', sc') <-

1723+ if n `elem` env

17241724 then do let n' = uniqueName n (env ++ inScope)

17251725 return (n', shadow n n' sc)

17261726 else return (n, sc)

@@ -1728,26 +1728,26 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

17281728 ty' <- mkUniq ty; val' <- mkUniq val

17291729 sc'' <- mkUniq sc'

17301730 return $! PLet n' ty' val' sc''

1731− mkUniq (PApp fc t args)

1731+ mkUniq (PApp fc t args)

17321732 = do t' <- mkUniq t

17331733 args' <- mapM mkUniqA args

17341734 return $! PApp fc t' args'

1735− mkUniq (PAppBind fc t args)

1735+ mkUniq (PAppBind fc t args)

17361736 = do t' <- mkUniq t

17371737 args' <- mapM mkUniqA args

17381738 return $! PAppBind fc t' args'

1739− mkUniq (PCase fc t alts)

1739+ mkUniq (PCase fc t alts)

17401740 = do t' <- mkUniq t

17411741 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y

17421742 return (x', y')) alts

17431743 return $! PCase fc t' alts'

1744− mkUniq (PPair fc l r)

1744+ mkUniq (PPair fc p l r)

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

1746− return $! PPair fc l' r'

1747− mkUniq (PDPair fc l t r)

1746+ return $! PPair fc p l' r'

1747+ mkUniq (PDPair fc l t r)

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

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

1750− mkUniq (PAlternative b as)

1749+ return $! PDPair fc l' t' r'

1750+ mkUniq (PAlternative b as)

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

17521752 mkUniq (PHidden t) = liftM PHidden (mkUniq t)

17531753 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)

src/Idris/AbsSyntaxTree.hs+27−11

@@ -603,6 +603,8 @@ updateNs ns t = mapPT updateRef t

603603-- (map (updateDNs ns) ds)

604604-- updateDNs ns c = c

605605

606+data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)

607+

606608-- | High level language terms

607609data PTerm = PQuote Raw

608610 | PRef FC Name

@@ -616,13 +618,13 @@ data PTerm = PQuote Raw

616618 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application

617619 | PMatchApp FC Name -- ^ Make an application by type matching

618620 | PCase FC PTerm [(PTerm, PTerm)]

619− | PTrue FC

621+ | PTrue FC PunInfo

620622 | PFalse FC

621623 | PRefl FC PTerm

622624 | PResolveTC FC

623625 | PEq FC PTerm PTerm

624626 | PRewrite FC PTerm PTerm (Maybe PTerm)

625− | PPair FC PTerm PTerm

627+ | PPair FC PunInfo PTerm PTerm

626628 | PDPair FC PTerm PTerm PTerm

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

628630 | PHidden PTerm -- ^ Irrelevant or hidden pattern

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

662664 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

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

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

665− mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)

667+ mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)

666668 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)

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

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

@@ -1154,7 +1156,9 @@ pprintPTerm impl bnd = prettySe 10 bnd

11541156 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

11551157 prettySe p bnd (PRefl _ _) = annotate (AnnName eqCon Nothing Nothing) $ text "refl"

11561158 prettySe p bnd (PResolveTC _) = text "resolvetc"

1157− prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"

1159+ prettySe p bnd (PTrue _ IsType) = annotate (AnnName unitTy Nothing Nothing) $ text "()"

1160+ prettySe p bnd (PTrue _ IsTerm) = annotate (AnnName unitCon Nothing Nothing) $ text "()"

1161+ prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

11581162 prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"

11591163 prettySe p bnd (PEq _ l r) =

11601164 bracket p 2 . align . group $

@@ -1165,8 +1169,20 @@ pprintPTerm impl bnd = prettySe 10 bnd

11651169 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

11661170 prettySe p bnd (PTyped l r) =

11671171 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen

1168− prettySe p bnd (PPair _ l r) =

1172+ prettySe p bnd (PPair _ TypeOrTerm l r) =

11691173 lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen

1174+ prettySe p bnd (PPair _ IsType l r) =

1175+ annotate (AnnName pairTy Nothing Nothing) lparen <>

1176+ prettySe 10 bnd l <>

1177+ annotate (AnnName pairTy Nothing Nothing) comma <+>

1178+ prettySe 10 bnd r <>

1179+ annotate (AnnName pairTy Nothing Nothing) rparen

1180+ prettySe p bnd (PPair _ IsTerm l r) =

1181+ annotate (AnnName pairCon Nothing Nothing) lparen <>

1182+ prettySe 10 bnd l <>

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

1184+ prettySe 10 bnd r <>

1185+ annotate (AnnName pairCon Nothing Nothing) rparen

11701186 prettySe p bnd (PDPair _ l t r) =

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

11721188 prettySe p bnd (PAlternative a as) =

@@ -1380,13 +1396,13 @@ instance Sized PTerm where

13801396 size (PApp fc name args) = 1 + size args

13811397 size (PAppBind fc name args) = 1 + size args

13821398 size (PCase fc trm bdy) = 1 + size trm + size bdy

1383− size (PTrue fc) = 1

1399+ size (PTrue fc _) = 1

13841400 size (PFalse fc) = 1

13851401 size (PRefl fc _) = 1

13861402 size (PResolveTC fc) = 1

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

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

1389− size (PPair fc left right) = 1 + size left + size right

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

13901406 size (PDPair fs left ty right) = 1 + size left + size ty + size right

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

13921408 size (PHidden hidden) = size hidden

@@ -1425,7 +1441,7 @@ allNamesIn tm = nub $ ni [] tm

14251441 ni env (PEq _ l r) = ni env l ++ ni env r

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

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

1428− ni env (PPair _ l r) = ni env l ++ ni env r

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

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

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

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

@@ -1447,7 +1463,7 @@ boundNamesIn tm = nub $ ni tm

14471463 ni (PEq _ l r) = ni l ++ ni r

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

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

1450− ni (PPair _ l r) = ni l ++ ni r

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

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

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

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

@@ -1474,7 +1490,7 @@ namesIn uvars ist tm = nub $ ni [] tm

14741490 ni env (PEq _ l r) = ni env l ++ ni env r

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

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

1477− ni env (PPair _ l r) = ni env l ++ ni env r

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

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

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

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

@@ -1502,7 +1518,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

15021518 ni env (PEq _ l r) = ni env l ++ ni env r

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

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

1505− ni env (PPair _ l r) = ni env l ++ ni env r

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

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

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

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

src/Idris/Coverage.hs+2−2

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

164164 otherPats :: PTerm -> [PTerm]

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

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

167− otherPats o@(PPair fc l r)

167+ otherPats o@(PPair fc _ l r)

168168 = ops fc pairCon

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

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

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

196196 = PDPair fc (getTm t) Placeholder (getTm v)

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

198198 | n == pairCon

199− = PPair fc (getTm l) (getTm r)

199+ = PPair fc IsTerm (getTm l) (getTm r)

200200 resugar t = t

201201

202202 dropForce force (x : xs) i | i `elem` force

src/Idris/DSL.hs+5−5

@@ -37,7 +37,7 @@ expandDo dsl (PAppBind fc t args) = PAppBind fc (expandDo dsl t)

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

40−expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)

40+expandDo dsl (PPair fc p l r) = PPair fc p (expandDo dsl l) (expandDo dsl r)

4141expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)

4242 (expandDo dsl r)

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

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

9393 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)

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)

96− v' i (PPair f l r) = PPair f (v' i l) (v' i r)

96+ v' i (PPair f p l r) = PPair f p (v' i l) (v' i r)

9797 v' i (PDPair f l t r) = PDPair f (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)

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

144144 return (PLet n ty v' (debind b sc))

145145 db' (PCase fc s opts) = do s' <- db' s

146146 return (PCase fc s' (map (pmap (debind b)) opts))

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

148− r' <- db' r

149− return (PPair fc l' r')

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

148+ r' <- db' r

149+ return (PPair fc p l' r')

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

151151 r' <- db' r

152152 return (PDPair fc l' t r')

src/Idris/DeepSeq.hs+5−2

@@ -122,6 +122,9 @@ instance (NFData t) => NFData (PDecl' t) where

122122 rnf (PTransform x1 x2 x3 x4)

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

124124

125+instance NFData PunInfo where

126+ rnf x = x `seq` ()

127+

125128instance (NFData t) => NFData (PClause' t) where

126129 rnf (PClause x1 x2 x3 x4 x5 x6)

127130 = rnf x1 `seq`

@@ -154,14 +157,14 @@ instance NFData PTerm where

154157 rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

155158 rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

156159 rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

157− rnf (PTrue x1) = rnf x1 `seq` ()

160+ rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

158161 rnf (PFalse x1) = rnf x1 `seq` ()

159162 rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

160163 rnf (PResolveTC x1) = rnf x1 `seq` ()

161164 rnf (PEq x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

162165 rnf (PRewrite x1 x2 x3 x4)

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

164− rnf (PPair x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

167+ rnf (PPair x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

165168 rnf (PDPair x1 x2 x3 x4)

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

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

src/Idris/Delaborate.hs+4−4

@@ -46,8 +46,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

4646 de env _ (App f a) = deFn env f [a]

4747 de env _ (V i) | i < length env = PRef un (snd (env!!i))

4848 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))

49− de env _ (P _ n _) | n == unitTy = PTrue un

50− | n == unitCon = PTrue un

49+ de env _ (P _ n _) | n == unitTy = PTrue un IsType

50+ | n == unitCon = PTrue un IsTerm

5151 | n == falseTy = PFalse un

5252 | Just n' <- lookup n env = PRef un n'

5353 | otherwise

@@ -83,7 +83,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

8383

8484 deFn env (App f a) args = deFn env f (a:args)

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

86− | n == pairTy = PPair un (de env [] l) (de env [] r)

86+ | n == pairTy = PPair un IsType (de env [] l) (de env [] r)

8787 | n == eqCon = PRefl un (de env [] r)

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

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

@@ -91,7 +91,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

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

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

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

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

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

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

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

9797 (de env [] r)

src/Idris/ElabTerm.hs+3−3

@@ -176,8 +176,8 @@ elab ist info pattern opts fn tm

176176 = lift $ tfail (Msg "Typecase is not allowed")

177177 elab' ina (PConstant c) = do apply (RConstant c) []; solve

178178 elab' ina (PQuote r) = do fill r; solve

179− elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))

180− (elab' ina (PRef fc unitTy))

179+ elab' ina (PTrue fc _) = try (elab' ina (PRef fc unitCon))

180+ (elab' ina (PRef fc unitTy))

181181 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)

182182 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

183183 = do g <- goal; resolveTC 5 g fn ist

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

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

196196 pimp (sMN 0 "B") Placeholder False,

197197 pexp l, pexp r])

198− elab' ina@(_, a, inty) (PPair fc l r)

198+ elab' ina@(_, a, inty) (PPair fc _ l r)

199199 = do hnf_compute

200200 g <- goal

201201 case g of

src/Idris/IBC.hs+26−9

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

2626

2727

2828ibcVersion :: Word8

29−ibcVersion = 56

29+ibcVersion = 58

3030

3131

3232data IBCFile = IBCFile { ver :: Word8,

@@ -1528,6 +1528,19 @@ instance (Binary t) => Binary (PData' t) where

15281528 return (PLaterdecl x1 x2)

15291529 _ -> error "Corrupted binary data for PData'"

15301530

1531+instance Binary PunInfo where

1532+ put x

1533+ = case x of

1534+ TypeOrTerm -> putWord8 0

1535+ IsType -> putWord8 1

1536+ IsTerm -> putWord8 2

1537+ get

1538+ = do i <- getWord8

1539+ case i of

1540+ 0 -> return TypeOrTerm

1541+ 1 -> return IsType

1542+ 2 -> return IsTerm

1543+

15311544instance Binary PTerm where

15321545 put x

15331546 = case x of

@@ -1574,8 +1587,9 @@ instance Binary PTerm where

15741587 put x1

15751588 put x2

15761589 put x3

1577− PTrue x1 -> do putWord8 12

1578− put x1

1590+ PTrue x1 x2 -> do putWord8 12

1591+ put x1

1592+ put x2

15791593 PFalse x1 -> do putWord8 13

15801594 put x1

15811595 PRefl x1 x2 -> do putWord8 14

@@ -1592,10 +1606,11 @@ instance Binary PTerm where

15921606 put x2

15931607 put x3

15941608 put x4

1595− PPair x1 x2 x3 -> do putWord8 18

1596− put x1

1597− put x2

1598− put x3

1609+ PPair x1 x2 x3 x4 -> do putWord8 18

1610+ put x1

1611+ put x2

1612+ put x3

1613+ put x4

15991614 PDPair x1 x2 x3 x4 -> do putWord8 19

16001615 put x1

16011616 put x2

@@ -1682,7 +1697,8 @@ instance Binary PTerm where

16821697 x3 <- get

16831698 return (PCase x1 x2 x3)

16841699 12 -> do x1 <- get

1685− return (PTrue x1)

1700+ x2 <- get

1701+ return (PTrue x1 x2)

16861702 13 -> do x1 <- get

16871703 return (PFalse x1)

16881704 14 -> do x1 <- get

@@ -1702,7 +1718,8 @@ instance Binary PTerm where

17021718 18 -> do x1 <- get

17031719 x2 <- get

17041720 x3 <- get

1705− return (PPair x1 x2 x3)

1721+ x4 <- get

1722+ return (PPair x1 x2 x3 x4)

17061723 19 -> do x1 <- get

17071724 x2 <- get

17081725 x3 <- get

src/Idris/ParseExpr.hs+4−4

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

151151 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)

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

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

154− update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)

154+ update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)

155155 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)

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

157157 update ns (PHidden t) = PHidden (update ns t)

@@ -336,7 +336,7 @@ bracketed :: SyntaxInfo -> IdrisParser PTerm

336336bracketed syn =

337337 do lchar ')'

338338 fc <- getFC

339− return $ PTrue fc

339+ return $ PTrue fc TypeOrTerm

340340 <|> try (do ln <- name; lchar ':';

341341 lty <- expr syn

342342 reservedOp "**"

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

372372 return fc

373373 rs <- sepBy1 (do fc' <- getFC; r <- expr syn; return (r, fc')) (lchar ',')

374374 lchar ')'

375− return $ PPair fc e (mergePairs rs)

375+ return $ PPair fc TypeOrTerm e (mergePairs rs)

376376 <|> do fc <- do fc <- getFC

377377 reservedOp "**"

378378 return fc

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

382382 <?> "end of bracketed expression"

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

384384 mergePairs [(t, fc)] = t

385− mergePairs ((t, fc):rs) = PPair fc t (mergePairs rs)

385+ mergePairs ((t, fc):rs) = PPair fc TypeOrTerm t (mergePairs rs)

386386

387387-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a

388388-- big integer, otherwise try fromInteger and the constants as alternatives.