6bb7f86 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #865 from david-christiansen/semantic-pprint

6bb7f86Edwin Brady13 years ago

src/Idris/AbsSyntax.hs+20−20

compare with master

unifiedsplit

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

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

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

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

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

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

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

924 = let n' = mkShadow n in

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

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

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

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

928 en (PTyped l r) = PTyped (en l) (en r)

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

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

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

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

932 en (PHidden t) = PHidden (en t)

933 en (PUnifyLog t) = PUnifyLog (en t)

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

1021 bnames (PRef _ n) = [n]

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

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

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

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

1025 bnames _ = []

1026

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

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

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

1087 pri (PTyped l r) = pri l

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

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

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

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

1091 pri (PConstant _) = 0

1092 pri Placeholder = 1

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

1264 = do (decls, ns) <- get

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

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

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

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

1268 = do (decls, ns) <- get

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

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

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

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

1272 = do (decls, ns) <- get

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

1274 namesIn uvars ist r

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

1334 = let l' = ai env ds l

1335 r' = ai env ds r in

1336 PPair fc p l' r'

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

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

1338 = let l' = ai env ds l

1339 t' = ai env ds t

1340 r' = ai env ds r in

1341− PDPair fc l' t' r'

1341+ PDPair fc p l' t' r'

1342 ai env ds (PAlternative a as)

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

1344 PAlternative a as'

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

1534 if null alts' then Placeholder

1535 else PAlternative b alts'

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

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

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

1538 su t = t

1539stripUnmatchable i tm = tm

1540

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

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

1646 mr <- match' r r'

1647 return (ml ++ mr)

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

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

1649− mt <- match' t t'

1649+ mt <- match' t t'

1650− mr <- match' r r'

1650+ mr <- match' r r'

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

1651+ return (ml ++ mt ++ mr)

1652 match (PAlternative a as) (PAlternative a' as')

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

1654 return (concat ms)

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

1726 (fmap (sm xs) tm)

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

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

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

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

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

1731 sm xs (PHidden x) = PHidden (sm xs x)

1732 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

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

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

1750 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

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

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

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

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

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

1822 mkUniq (PPair fc p l r)

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

1824 return $! PPair fc p l' r'

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

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

1826 | t /= Placeholder

1827 = do env <- get

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

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

1832 put (n' : env)

1833 t' <- mkUniq t

1834 sc'' <- mkUniq sc'

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

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

1836− mkUniq (PDPair fc l t r)

1836+ mkUniq (PDPair fc p l t r)

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

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

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

1839 mkUniq (PAlternative b as)

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

1841 mkUniq (PHidden t) = liftM PHidden (mkUniq t)

src/Idris/AbsSyntaxTree.hs+30−12

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

626 | PEq FC PTerm PTerm

627 | PRewrite FC PTerm PTerm (Maybe PTerm)

628 | PPair FC PunInfo PTerm PTerm

629− | PDPair FC PTerm PTerm PTerm

629+ | PDPair FC PunInfo PTerm PTerm PTerm

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

631 | PHidden PTerm -- ^ Irrelevant or hidden pattern

632 | PType

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

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

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

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

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

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

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

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

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

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

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

1194 prettySe 10 bnd r <>

1195 annotate (AnnName pairCon Nothing Nothing) rparen

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

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

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

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

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

1200+ bindingOf n False <+>

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

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

1203+ annotate (AnnName sigmaTy Nothing Nothing) rparen

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

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

1206+ prettySe 10 bnd l <+>

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

1208+ prettySe 10 bnd r <>

1209+ annotate (AnnName sigmaTy Nothing Nothing) rparen

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

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

1212+ prettySe 10 bnd l <+>

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

1214+ prettySe 10 bnd r <>

1215+ annotate (AnnName existsCon Nothing Nothing) rparen

1198 prettySe p bnd (PAlternative a as) =

1216 prettySe p bnd (PAlternative a as) =

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

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

1200 where

1218 where

@@ -1413,7 +1431,7 @@ instance Sized PTerm where

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

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

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

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

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

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

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

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

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

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

1418 size (PHidden hidden) = size hidden

1436 size (PHidden hidden) = size hidden

1419 size (PUnifyLog tm) = size tm

1437 size (PUnifyLog tm) = size tm

@@ -1452,8 +1470,8 @@ allNamesIn tm = nub $ ni [] tm

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

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

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

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

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

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

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

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

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

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

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

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

1458 ni env (PUnifyLog tm) = ni env tm

1476 ni env (PUnifyLog tm) = ni env tm

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

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

@@ -1474,8 +1492,8 @@ boundNamesIn tm = nub $ ni tm

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

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

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

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

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

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

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

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

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

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

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

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

1480 ni (PHidden tm) = ni tm

1498 ni (PHidden tm) = ni tm

1481 ni (PUnifyLog tm) = ni tm

1499 ni (PUnifyLog tm) = ni tm

@@ -1501,8 +1519,8 @@ namesIn uvars ist tm = nub $ ni [] tm

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

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

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

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

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

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

1504− 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

1505− 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

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

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

1507 ni env (PHidden tm) = ni env tm

1525 ni env (PHidden tm) = ni env tm

1508 ni env (PUnifyLog tm) = ni env tm

1526 ni env (PUnifyLog tm) = ni env tm

@@ -1529,8 +1547,8 @@ usedNamesIn vars ist tm = nub $ ni [] tm

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

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

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

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

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

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

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

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

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

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

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

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

1535 ni env (PHidden tm) = ni env tm

1553 ni env (PHidden tm) = ni env tm

1536 ni env (PUnifyLog tm) = ni env tm

1554 ni env (PUnifyLog tm) = ni env tm

src/Idris/Core/Unify.hs+7−7

@@ -76,7 +76,7 @@ match_unify ctxt env topx topy dont holes =

76 | otherwise = do UI s f <- get

77 let r = recoverable x y

78 let err = CantUnify r

79− topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

79+ topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

80 if (not r) then lift $ tfail err

81 else do put (UI s ((x, y, env, err) : f))

82 lift $ tfail err

@@ -90,7 +90,7 @@ match_unify ctxt env topx topy dont holes =

90 uB bnames x y = do UI s f <- get

91 let r = recoverable (binderTy x) (binderTy y)

92 let err = CantUnify r topx topy

93− (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)

93+ (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

94 (errEnv env) s

95 put (UI s ((binderTy x, binderTy y, env, err) : f))

96 return []

@@ -104,7 +104,7 @@ match_unify ctxt env topx topy dont holes =

104 unifyFail x y = do UI s f <- get

105 let r = recoverable x y

106 let err = CantUnify r

107− topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

107+ topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

108 put (UI s ((x, y, env, err) : f))

109 lift $ tfail err

110 combine bnames as [] = return as

@@ -309,7 +309,7 @@ unify ctxt env topx topy dont holes =

309 | otherwise = do UI s f <- get

310 let r = recoverable x y

311 let err = CantUnify r

312− topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

312+ topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

313 if (not r) then lift $ tfail err

314 else do put (UI s ((x, y, env, err) : f))

315 return [] -- lift $ tfail err

@@ -445,7 +445,7 @@ unify ctxt env topx topy dont holes =

445 = do UI s f <- get

446 let r = recoverable x y

447 let err = CantUnify r

448− topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

448+ topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

449 put (UI s ((topx, topy, env, err) : f))

450 return []

451

@@ -453,7 +453,7 @@ unify ctxt env topx topy dont holes =

453 unifyFail x y = do UI s f <- get

454 let r = recoverable x y

455 let err = CantUnify r

456− topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

456+ topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

457 put (UI s ((topx, topy, env, err) : f))

458 lift $ tfail err

459

@@ -475,7 +475,7 @@ unify ctxt env topx topy dont holes =

475 uB bnames x y = do UI s f <- get

476 let r = recoverable (binderTy x) (binderTy y)

477 let err = CantUnify r topx topy

478− (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)

478+ (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

479 (errEnv env) s

480 put (UI s ((binderTy x, binderTy y, env, err) : f))

481 return [] -- lift $ tfail err

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+32−19

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

@@ -127,7 +127,10 @@ indented :: Doc a -> Doc a

127indented = nest errorIndent . (line <>)

128

129pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

130+pprintTerm ist = pprintTerm' ist []

131+

132+pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

130−pprintTerm ist = prettyImp (opt_showimp (idris_options ist))

133+pprintTerm' ist = pprintPTerm (opt_showimp (idris_options ist))

131

134

132pshow :: IState -> Err -> String

135pshow :: IState -> Err -> String

133pshow ist err = displayDecorated (consoleDecorate ist) .

136pshow ist err = displayDecorated (consoleDecorate ist) .

@@ -144,25 +147,28 @@ pprintErr' i (InternalMsg s) =

144 text ("Please consider reporting at " ++ bugaddr)

147 text ("Please consider reporting at " ++ bugaddr)

145 ]

148 ]

146pprintErr' i (CantUnify _ x y e sc s) =

149pprintErr' i (CantUnify _ x y e sc s) =

147− text "Can't unify" <> indented (pprintTerm i (delab i x)) <$>

150+ text "Can't unify" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i x)) <$>

148− text "with" <> indented (pprintTerm i (delab i y)) <>

151+ text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i y)) <>

149 case e of

152 case e of

150 Msg "" -> empty

153 Msg "" -> empty

151 _ -> line <> line <> text "Specifically:" <>

154 _ -> line <> line <> text "Specifically:" <>

152 indented (pprintErr' i e) <>

155 indented (pprintErr' i e) <>

153− if (opt_errContext (idris_options i)) then text $ showSc i sc else empty

156+ if (opt_errContext (idris_options i)) then showSc i sc else empty

154−pprintErr' i (CantConvert x y env) = trace (show (x,y)) $

157+pprintErr' i (CantConvert x y env) =

158+ text "Can't convert" <>

155− text "Can't convert" <> indented (pprintTerm i (delab i x)) <$>

159+ indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <$>

160+ text "with" <>

156− text "with" <> indented (pprintTerm i (delab i y)) <>

161+ indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i y)) <>

157− if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty

162+ if (opt_errContext (idris_options i)) then line <> showSc i env else empty

158pprintErr' i (CantSolveGoal x env) =

163pprintErr' i (CantSolveGoal x env) =

164+ text "Can't solve goal " <>

159− text "Can't solve goal " <> indented (pprintTerm i (delab i x)) <>

165+ indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <>

160− if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty

166+ if (opt_errContext (idris_options i)) then line <> showSc i env else empty

161pprintErr' i (UnifyScope n out tm env) =

167pprintErr' i (UnifyScope n out tm env) =

162 text "Can't unify" <> indented (annName n) <+>

168 text "Can't unify" <> indented (annName n) <+>

163− text "with" <> indented (pprintTerm i (delab i tm)) <+>

169+ text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>

164 text "as" <> indented (annName out) <> text "is not in scope" <>

170 text "as" <> indented (annName out) <> text "is not in scope" <>

165− if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty

171+ if (opt_errContext (idris_options i)) then line <> showSc i env else empty

166pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t

172pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t

167pprintErr' i (NonFunctionType f ty) =

173pprintErr' i (NonFunctionType f ty) =

168 pprintTerm i (delab i f) <+>

174 pprintTerm i (delab i f) <+>

@@ -176,9 +182,10 @@ pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f

176pprintErr' i (CantIntroduce ty) =

182pprintErr' i (CantIntroduce ty) =

177 text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)

183 text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)

178pprintErr' i (InfiniteUnify x tm env) =

184pprintErr' i (InfiniteUnify x tm env) =

179− text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+> pprintTerm i (delab i tm) <+>

185+ text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>

186+ pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm) <+>

180 text "would lead to infinite value" <>

187 text "would lead to infinite value" <>

181− if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty

188+ if (opt_errContext (idris_options i)) then line <> showSc i env else empty

182pprintErr' i (NotInjective p x y) =

189pprintErr' i (NotInjective p x y) =

183 text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>

190 text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>

184 text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>

191 text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>

@@ -226,9 +233,15 @@ annName n = annName' n (show n)

226annName' :: Name -> String -> Doc OutputAnnotation

233annName' :: Name -> String -> Doc OutputAnnotation

227annName' n str = annotate (AnnName n Nothing Nothing) (text str)

234annName' n str = annotate (AnnName n Nothing Nothing) (text str)

228

235

229−showSc i [] = ""

236+showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

237+showSc i [] = empty

230−showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

238+showSc i xs = line <> line <> text "In context:" <>

231− where showVar (x, y) = "\t" ++ showbasic x ++ " : " ++ show (delab i y)

239+ indented (vsep (reverse (showSc' [] xs)))

240+ where showSc' bnd [] = []

241+ showSc' bnd ((n, ty):ctxt) =

242+ let this = bindingOf n False <+> colon <+> pprintTerm' i bnd (delab i ty)

243+ in this : showSc' ((n,False):bnd) ctxt

244+

232

245

233showqual :: IState -> Name -> String

246showqual :: IState -> Name -> String

234showqual i n = showName (Just i) [] False False (dens n)

247showqual i n = showName (Just i) [] False False (dens n)

src/Idris/ElabTerm.hs+5−5

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

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

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

218 pexp l, pexp r])

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

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

220 = case t of

221 Placeholder ->

222 do hnf_compute

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

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

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

234 pexp l, pexp r])

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

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

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

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

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

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

238− pexp l, pexp r])

238+ pexp l, pexp r])

239 elab' ina (PAlternative True as)

240 = do hnf_compute

241 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