e80f871 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Annotate and colour pairs and () properly

e80f871David Raymond Christiansen13 years ago

src/Idris/AbsSyntax.hs+29−29

compare with master

unifiedsplit

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

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

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

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

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

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

854 en (PHidden t) = PHidden (en t)

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

942

943 bnames (PRef _ n) = [n]

944 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

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

947 bnames _ = []

948

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

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

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

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

1001− pri (PTrue _) = 0

1001+ pri (PTrue _ _) = 0

1002 pri (PFalse _) = 0

1003 pri (PRefl _ _) = 1

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

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

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

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

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

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

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

1013 pri (PConstant _) = 0

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

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

1183 imps top env (PTyped l r)

1184 = imps top env l

1185− imps top env (PPair _ l r)

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

1186 = do (decls, ns) <- get

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

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

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

1252 = let l' = ai env ds l

1253 r' = ai env ds r in

1254 PTyped l' r'

1255− ai env ds (PPair fc l r)

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

1256 = let l' = ai env ds l

1257 r' = ai env ds r in

1258− PPair fc l' r'

1258+ PPair fc p l' r'

1259 ai env ds (PDPair fc l t r)

1260 = let l' = ai env ds l

1261 t' = ai env ds t

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

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

1456 if null alts' then Placeholder

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

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

1460 su t = t

1461stripUnmatchable i tm = tm

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

1564 return (ml ++ mr)

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

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

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

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

1568− mr <- match' r r'

1568+ mr <- match' r r'

1569− return (ml ++ mr)

1569+ return (ml ++ mr)

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

1571 mt <- match' t t'

1572 mr <- match' r r'

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

1587 match (PTactics _) _ = return []

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

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

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

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

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

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

1593 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

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

1648 (fmap (sm xs) tm)

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

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

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

1653 sm xs (PHidden x) = PHidden (sm xs x)

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

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

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

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

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

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

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

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

1692

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

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

1695− mkUniqT tac = return tac

1695+ mkUniqT tac = return tac

1696

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

1698 mkUniq (PLam n ty sc)

1699 = do env <- get

1700− (n', sc') <-

1700+ (n', sc') <-

1701− if n `elem` env

1701+ if n `elem` env

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

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

1704 else return (n, sc)

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

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

1709 mkUniq (PPi p n ty sc)

1710 = do env <- get

1711− (n', sc') <-

1711+ (n', sc') <-

1712− if n `elem` env

1712+ if n `elem` env

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

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

1715 else return (n, sc)

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

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

1720 mkUniq (PLet n ty val sc)

1721 = do env <- get

1722− (n', sc') <-

1722+ (n', sc') <-

1723− if n `elem` env

1723+ if n `elem` env

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

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

1726 else return (n, sc)

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

1728 ty' <- mkUniq ty; val' <- mkUniq val

1729 sc'' <- mkUniq sc'

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

1731− mkUniq (PApp fc t args)

1731+ mkUniq (PApp fc t args)

1732 = do t' <- mkUniq t

1733 args' <- mapM mkUniqA args

1734 return $! PApp fc t' args'

1735− mkUniq (PAppBind fc t args)

1735+ mkUniq (PAppBind fc t args)

1736 = do t' <- mkUniq t

1737 args' <- mapM mkUniqA args

1738 return $! PAppBind fc t' args'

1739− mkUniq (PCase fc t alts)

1739+ mkUniq (PCase fc t alts)

1740 = do t' <- mkUniq t

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

1742 return (x', y')) alts

1743 return $! PCase fc t' alts'

1744− mkUniq (PPair fc l r)

1744+ mkUniq (PPair fc p l r)

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

1746− return $! PPair fc l' r'

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

1747− mkUniq (PDPair fc l t r)

1747+ mkUniq (PDPair fc l t r)

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

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

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

1750− mkUniq (PAlternative b as)

1750+ mkUniq (PAlternative b as)

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

1752 mkUniq (PHidden t) = liftM PHidden (mkUniq t)

1753 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)

src/Idris/AbsSyntaxTree.hs+27−11

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

603-- (map (updateDNs ns) ds)

604-- updateDNs ns c = c

605

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

607+

606-- | High level language terms

608-- | High level language terms

607data PTerm = PQuote Raw

609data PTerm = PQuote Raw

608 | PRef FC Name

610 | PRef FC Name

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

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

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

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

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

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

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

619− | PTrue FC

621+ | PTrue FC PunInfo

620 | PFalse FC

622 | PFalse FC

621 | PRefl FC PTerm

623 | PRefl FC PTerm

622 | PResolveTC FC

624 | PResolveTC FC

623 | PEq FC PTerm PTerm

625 | PEq FC PTerm PTerm

624 | PRewrite FC PTerm PTerm (Maybe PTerm)

626 | PRewrite FC PTerm PTerm (Maybe PTerm)

625− | PPair FC PTerm PTerm

627+ | PPair FC PunInfo PTerm PTerm

626 | PDPair FC PTerm PTerm PTerm

628 | PDPair FC PTerm PTerm PTerm

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

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

628 | PHidden PTerm -- ^ Irrelevant or hidden pattern

630 | PHidden PTerm -- ^ Irrelevant or hidden pattern

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1158 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 "()"

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

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

1159 prettySe p bnd (PEq _ l r) =

1163 prettySe p bnd (PEq _ l r) =

1160 bracket p 2 . align . group $

1164 bracket p 2 . align . group $

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

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

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

1166 prettySe p bnd (PTyped l r) =

1170 prettySe p bnd (PTyped l r) =

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

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

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

1173 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

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

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

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

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

1172 prettySe p bnd (PAlternative a as) =

1188 prettySe p bnd (PAlternative a as) =

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

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

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

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

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

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

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

1383− size (PTrue fc) = 1

1399+ size (PTrue fc _) = 1

1384 size (PFalse fc) = 1

1400 size (PFalse fc) = 1

1385 size (PRefl fc _) = 1

1401 size (PRefl fc _) = 1

1386 size (PResolveTC fc) = 1

1402 size (PResolveTC fc) = 1

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

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

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

1404 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

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

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

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

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

1392 size (PHidden hidden) = size hidden

1408 size (PHidden hidden) = size hidden

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

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

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

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

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

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

1443 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

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

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

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

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

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

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

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

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

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

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

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

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

1465 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

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

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

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

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

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

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

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

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

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

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

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

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

1492 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

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

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

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

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

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

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

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

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

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

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

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

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

1520 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

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

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

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

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

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

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

src/Idris/Coverage.hs+2−2

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

164 otherPats :: PTerm -> [PTerm]

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

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

168 = ops fc pairCon

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

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

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

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

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

198 | n == pairCon

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

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

200 resugar t = t

201

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

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

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)

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

42 (expandDo dsl r)

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

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

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

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

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

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

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

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

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

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

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

148− r' <- db' r

148+ r' <- db' r

149− return (PPair fc l' r')

149+ 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')

src/Idris/DeepSeq.hs+5−2

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

122 rnf (PTransform x1 x2 x3 x4)

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

124

125+instance NFData PunInfo where

126+ rnf x = x `seq` ()

127+

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

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

126 rnf (PClause x1 x2 x3 x4 x5 x6)

129 rnf (PClause x1 x2 x3 x4 x5 x6)

127 = rnf x1 `seq`

130 = rnf x1 `seq`

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

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

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

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

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

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

159 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` ()

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

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

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

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

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

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

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

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

162 rnf (PRewrite x1 x2 x3 x4)

165 rnf (PRewrite x1 x2 x3 x4)

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

166 = 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` ()

165 rnf (PDPair x1 x2 x3 x4)

168 rnf (PDPair x1 x2 x3 x4)

166 = 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` ()

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

170 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

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

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

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

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

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

50− | n == unitCon = PTrue un

50+ | n == unitCon = PTrue un IsTerm

51 | n == falseTy = PFalse un

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

53 | otherwise

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

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

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

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

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

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

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

91 = PDPair un (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 (de env [] l) (de env [] 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

97 (de env [] r)

src/Idris/ElabTerm.hs+3−3

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

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

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

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

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

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

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

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

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

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

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

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

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

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

197 pexp l, pexp r])

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

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

199 = do hnf_compute

200 g <- goal

201 case g of

src/Idris/IBC.hs+26−9

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

28ibcVersion :: Word8

29−ibcVersion = 56

29+ibcVersion = 58

32data IBCFile = IBCFile { ver :: Word8,

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

1528 return (PLaterdecl x1 x2)

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

1530

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+

1531instance Binary PTerm where

1544instance Binary PTerm where

1532 put x

1545 put x

1533 = case x of

1546 = case x of

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

1574 put x1

1587 put x1

1575 put x2

1588 put x2

1576 put x3

1589 put x3

1577− PTrue x1 -> do putWord8 12

1590+ PTrue x1 x2 -> do putWord8 12

1578− put x1

1591+ put x1

1592+ put x2

1579 PFalse x1 -> do putWord8 13

1593 PFalse x1 -> do putWord8 13

1580 put x1

1594 put x1

1581 PRefl x1 x2 -> do putWord8 14

1595 PRefl x1 x2 -> do putWord8 14

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

1592 put x2

1606 put x2

1593 put x3

1607 put x3

1594 put x4

1608 put x4

1595− PPair x1 x2 x3 -> do putWord8 18

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

1596− put x1

1610+ put x1

1597− put x2

1611+ put x2

1598− put x3

1612+ put x3

1613+ put x4

1599 PDPair x1 x2 x3 x4 -> do putWord8 19

1614 PDPair x1 x2 x3 x4 -> do putWord8 19

1600 put x1

1615 put x1

1601 put x2

1616 put x2

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

1682 x3 <- get

1697 x3 <- get

1683 return (PCase x1 x2 x3)

1698 return (PCase x1 x2 x3)

1684 12 -> do x1 <- get

1699 12 -> do x1 <- get

1700+ x2 <- get

1685− return (PTrue x1)

1701+ return (PTrue x1 x2)

1686 13 -> do x1 <- get

1702 13 -> do x1 <- get

1687 return (PFalse x1)

1703 return (PFalse x1)

1688 14 -> do x1 <- get

1704 14 -> do x1 <- get

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

1702 18 -> do x1 <- get

1718 18 -> do x1 <- get

1703 x2 <- get

1719 x2 <- get

1704 x3 <- get

1720 x3 <- get

1721+ x4 <- get

1705− return (PPair x1 x2 x3)

1722+ return (PPair x1 x2 x3 x4)

1706 19 -> do x1 <- get

1723 19 -> do x1 <- get

1707 x2 <- get

1724 x2 <- get

1708 x3 <- get

1725 x3 <- get

src/Idris/ParseExpr.hs+4−4

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

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

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

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

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

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

157 update ns (PHidden t) = PHidden (update ns t)

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

336bracketed syn =

337 do lchar ')'

338 fc <- getFC

339− return $ PTrue fc

339+ return $ PTrue fc TypeOrTerm

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

341 lty <- expr syn

342 reservedOp "**"

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

372 return fc

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

374 lchar ')'

375− return $ PPair fc e (mergePairs rs)

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

376 <|> do fc <- do fc <- getFC

377 reservedOp "**"

378 return fc

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

382 <?> "end of bracketed expression"

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

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

386

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

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