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

git.iko.soy/Idris-dev

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

Improve pretty-printing

commit6bb7f86e1bcc1bfc474930da767d881554b54991 authorEdwin Brady <edwin.brady@gmail.com> dateTue 11 Feb 2014, 19:59 (13 years ago) parent98ddd5b 8e6e14a

10 files changed+117−84

compare with master

unifiedsplit

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

src/Idris/AbsSyntax.hs+20−20

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

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

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

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

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

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

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

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

928928 en (PTyped l r) = PTyped (en l) (en r)

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

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

932932 en (PHidden t) = PHidden (en t)

933933 en (PUnifyLog t) = PUnifyLog (en t)

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

10211021 bnames (PRef _ n) = [n]

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

10231023 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

10251025 bnames _ = []

10261026

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

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

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

10871087 pri (PTyped l r) = pri l

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

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

10911091 pri (PConstant _) = 0

10921092 pri Placeholder = 1

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

12641264 = do (decls, ns) <- get

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

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

12681268 = do (decls, ns) <- get

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

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

12721272 = do (decls, ns) <- get

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

12741274 namesIn uvars ist r

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

13341334 = let l' = ai env ds l

13351335 r' = ai env ds r in

13361336 PPair fc p l' r'

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

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

13381338 = let l' = ai env ds l

13391339 t' = ai env ds t

13401340 r' = ai env ds r in

1341− PDPair fc l' t' r'

1341+ PDPair fc p l' t' r'

13421342 ai env ds (PAlternative a as)

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

13441344 PAlternative a as'

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

15341534 if null alts' then Placeholder

15351535 else PAlternative b alts'

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

15381538 su t = t

15391539stripUnmatchable i tm = tm

15401540

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

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

16461646 mr <- match' r r'

16471647 return (ml ++ mr)

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

1649− mt <- match' t t'

1650− mr <- match' r r'

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

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

1649+ mt <- match' t t'

1650+ mr <- match' r r'

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

16521652 match (PAlternative a as) (PAlternative a' as')

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

16541654 return (concat ms)

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

17261726 (fmap (sm xs) tm)

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

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

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

17311731 sm xs (PHidden x) = PHidden (sm xs x)

17321732 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

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

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

17501750 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

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

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

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

18221822 mkUniq (PPair fc p l r)

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

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

18261826 | t /= Placeholder

18271827 = do env <- get

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

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

18321832 put (n' : env)

18331833 t' <- mkUniq t

18341834 sc'' <- mkUniq sc'

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

1836− mkUniq (PDPair fc l t r)

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

1836+ mkUniq (PDPair fc p l t r)

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

18391839 mkUniq (PAlternative b as)

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

18411841 mkUniq (PHidden t) = liftM PHidden (mkUniq t)

src/Idris/AbsSyntaxTree.hs+30−12

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

626626 | PEq FC PTerm PTerm

627627 | PRewrite FC PTerm PTerm (Maybe PTerm)

628628 | PPair FC PunInfo PTerm PTerm

629− | PDPair FC PTerm PTerm PTerm

629+ | PDPair FC PunInfo PTerm PTerm PTerm

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

631631 | PHidden PTerm -- ^ Irrelevant or hidden pattern

632632 | PType

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

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

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

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

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

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

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

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

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

11941194 prettySe 10 bnd r <>

11951195 annotate (AnnName pairCon Nothing Nothing) rparen

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

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

11971197 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

11981216 prettySe p bnd (PAlternative a as) =

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

12001218 where

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

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

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

14151433 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

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

14181436 size (PHidden hidden) = size hidden

14191437 size (PUnifyLog tm) = size tm

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

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

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

14541472 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

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

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

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

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

14581476 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

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

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

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

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

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

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

14801498 ni (PHidden tm) = ni tm

14811499 ni (PUnifyLog tm) = ni tm

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

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

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

15031521 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

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

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

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

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

15071525 ni env (PHidden tm) = ni env tm

15081526 ni env (PUnifyLog tm) = ni env tm

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

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

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

15311549 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

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

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

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

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

15351553 ni env (PHidden tm) = ni env tm

15361554 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 =

7676 | otherwise = do UI s f <- get

7777 let r = recoverable x y

7878 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

8080 if (not r) then lift $ tfail err

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

8282 lift $ tfail err

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

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

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

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

9494 (errEnv env) s

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

9696 return []

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

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

105105 let r = recoverable x y

106106 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

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

109109 lift $ tfail err

110110 combine bnames as [] = return as

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

309309 | otherwise = do UI s f <- get

310310 let r = recoverable x y

311311 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

313313 if (not r) then lift $ tfail err

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

315315 return [] -- lift $ tfail err

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

445445 = do UI s f <- get

446446 let r = recoverable x y

447447 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

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

450450 return []

451451

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

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

454454 let r = recoverable x y

455455 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

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

458458 lift $ tfail err

459459

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

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

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

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

479479 (errEnv env) s

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

481481 return [] -- lift $ tfail err

src/Idris/Coverage.hs+2−2

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

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

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

171171 [pexp l, pexp r]) o

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

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

173173 = ops fc (sUN "Ex_intro")

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

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

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

193193 -- put it back to its original form

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

195195 | ei == txt "Ex_intro"

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

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

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

198198 | n == pairCon

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

src/Idris/DSL.hs+6−6

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

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

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

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

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

42− (expandDo dsl r)

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

42+ (expandDo dsl r)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

148148 r' <- db' r

149149 return (PPair fc p l' r')

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

151− r' <- db' r

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

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

151+ r' <- db' r

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

153153 db' t = return t

154154

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

src/Idris/DeepSeq.hs+2−2

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

165165 rnf (PRewrite x1 x2 x3 x4)

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

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

168− rnf (PDPair x1 x2 x3 x4)

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

168+ rnf (PDPair x1 x2 x3 x4 x5)

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

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

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

172172 rnf PType = ()

src/Idris/Delaborate.hs+32−19

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

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

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

9090 | n == sUN "Exists"

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

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

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

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

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

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

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

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

9797 (de env [] r)

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

9999 = case lookup n (idris_metavars ist) of

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

127127indented = nest errorIndent . (line <>)

128128

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

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

130+pprintTerm ist = pprintTerm' ist []

131+

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

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

131134

132135pshow :: IState -> Err -> String

133136pshow ist err = displayDecorated (consoleDecorate ist) .

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

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

145148 ]

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

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

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

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

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

149152 case e of

150153 Msg "" -> empty

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

152155 indented (pprintErr' i e) <>

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

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

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

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

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

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

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

158+ text "Can't convert" <>

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

160+ text "with" <>

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

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

158163pprintErr' i (CantSolveGoal x env) =

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

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

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

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

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

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

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

164170 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

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

167173pprintErr' i (NonFunctionType f ty) =

168174 pprintTerm i (delab i f) <+>

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

176182pprintErr' i (CantIntroduce ty) =

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

178184pprintErr' 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) <+>

180187 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

182189pprintErr' i (NotInjective p x y) =

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

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

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

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

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

228235

229−showSc i [] = ""

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

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

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

237+showSc i [] = empty

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

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+

232245

233246showqual :: IState -> Name -> String

234247showqual 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

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

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

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

220220 = case t of

221221 Placeholder ->

222222 do hnf_compute

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

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

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

234234 pexp l, pexp r])

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

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

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

238− pexp l, pexp r])

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

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

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

238+ pexp l, pexp r])

239239 elab' ina (PAlternative True as)

240240 = do hnf_compute

241241 ty <- goal

src/Idris/IBC.hs+9−7

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

2626

2727

2828ibcVersion :: Word8

29−ibcVersion = 59

29+ibcVersion = 60

3030

3131

3232data IBCFile = IBCFile { ver :: Word8,

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

16111611 put x2

16121612 put x3

16131613 put x4

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

1615− put x1

1616− put x2

1617− put x3

1618− put x4

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

1615+ put x1

1616+ put x2

1617+ put x3

1618+ put x4

1619+ put x5

16191620 PAlternative x1 x2 -> do putWord8 20

16201621 put x1

16211622 put x2

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

17281729 x2 <- get

17291730 x3 <- get

17301731 x4 <- get

1731− return (PDPair x1 x2 x3 x4)

1732+ x5 <- get

1733+ return (PDPair x1 x2 x3 x4 x5)

17321734 20 -> do x1 <- get

17331735 x2 <- get

17341736 return (PAlternative x1 x2)

src/Idris/ParseExpr.hs+4−4

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

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

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

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

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

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

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

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

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

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

349349 fc <- getFC

350350 r <- expr syn

351351 lchar ')'

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

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

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

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

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

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

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

370370 <|> do l <- expr syn

371371 bracketedExpr syn l

372−

372+

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

374374bracketedExpr syn e =

375375 do lchar ')'; return e

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

384384 return fc

385385 r <- expr syn

386386 lchar ')'

387− return (PDPair fc e Placeholder r)

387+ return (PDPair fc TypeOrTerm e Placeholder r)

388388 <?> "end of bracketed expression"

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

390390 mergePairs [(t, fc)] = t