1269791 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Keep type arguments of = when unelaborating

1269791Edwin Brady12 years ago

src/Idris/AbsSyntax.hs+14−12

compare with master

unifiedsplit

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

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

854 = let n' = mkShadow n in

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

856− en (PEq f l r) = PEq f (en l) (en r)

856+ en (PEq f lt rt l r) = PEq f (en lt) (en r) (en l) (en r)

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

858 en (PTyped l r) = PTyped (en l) (en r)

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

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

1022 pri (PTrue _ _) = 0

1023 pri (PFalse _) = 0

1024 pri (PRefl _ _) = 1

1025− pri (PEq _ l r) = max 1 (max (pri l) (pri r))

1025+ pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))

1026 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

1027 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

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

@@ -1096,8 +1096,6 @@ addUsingConstraints syn fc t

1096 let ns = namesIn [] ist t

1097 let cs = getConstraints t -- check declared constraints

1098 let addconsts = uconsts \\ cs

1099− -- if all names in the arguments of addconsts appear in ns,

1100− -- add the constraint implicitly

1101 return (doAdd addconsts ns t)

1099 return (doAdd addconsts ns t)

1102 where uconsts = filter uconst (using syn)

1100 where uconsts = filter uconst (using syn)

1103 uconst (UConstraint _ _) = True

1101 uconst (UConstraint _ _) = True

@@ -1191,7 +1189,8 @@ getUnboundImplicits i sc tm = []

1191-- argument position.

1189-- argument position.

1192

1190

1193-- This has become a right mess already. Better redo it some time...

1191-- This has become a right mess already. Better redo it some time...

1194−

1192+-- TODO: This is obsoleted by the new way of elaborating types, but there's still

1193+-- a couple of places which use it. Clean them up!

1195implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm

1194implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm

1196implicit info syn n ptm = implicit' info syn [] n ptm

1195implicit info syn n ptm = implicit' info syn [] n ptm

1197

1196

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

1288 put (PTacImplicit 10 l n scr Placeholder : decls,

1287 put (PTacImplicit 10 l n scr Placeholder : decls,

1289 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1288 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1290 imps True (n:env) sc

1289 imps True (n:env) sc

1291− imps top env (PEq _ l r)

1290+ imps top env (PEq _ _ _ l r)

1292 = do (decls, ns) <- get

1291 = do (decls, ns) <- get

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

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

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

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

@@ -1357,10 +1356,12 @@ addImpl' inpat env infns ist ptm

1357 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []

1356 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []

1358 ai qq env ds (PHidden (PRef fc f))

1357 ai qq env ds (PHidden (PRef fc f))

1359 | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []

1358 | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []

1360− ai qq env ds (PEq fc l r)

1359+ ai qq env ds (PEq fc lt rt l r)

1360+ = let lt' = ai qq env ds lt

1361+ rt' = ai qq env ds rt

1361− = let l' = ai qq env ds l

1362+ l' = ai qq env ds l

1362 r' = ai qq env ds r in

1363 r' = ai qq env ds r in

1363− PEq fc l' r'

1364+ PEq fc lt' rt' l' r'

1364 ai qq env ds (PRewrite fc l r g)

1365 ai qq env ds (PRewrite fc l r g)

1365 = let l' = ai qq env ds l

1366 = let l' = ai qq env ds l

1366 r' = ai qq env ds r

1367 r' = ai qq env ds r

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

1698 | not names && (not (isConName n (tt_ctxt i) ||

1699 | not names && (not (isConName n (tt_ctxt i) ||

1699 isFnName n (tt_ctxt i)) || tm == Placeholder)

1700 isFnName n (tt_ctxt i)) || tm == Placeholder)

1700 = return [(n, tm)]

1701 = return [(n, tm)]

1701− match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

1702+ match (PEq _ _ _ l r) (PEq _ _ _ l' r')

1703+ = do ml <- match' l l'

1702 mr <- match' r r'

1704 mr <- match' r r'

1703 return (ml ++ mr)

1705 return (ml ++ mr)

1704 match (PRewrite _ l r _) (PRewrite _ l' r' _)

1706 match (PRewrite _ l r _) (PRewrite _ l' r' _)

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

1789 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)

1791 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)

1790 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

1792 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

1791 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

1793 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

1792− sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)

1794+ sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)

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

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

1794 (fmap (sm xs) tm)

1796 (fmap (sm xs) tm)

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

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

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

1813 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1815 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1814 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

1816 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

1815 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1817 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1816− sm (PEq f x y) = PEq f (sm x) (sm y)

1818+ sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)

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

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

1818 sm (PTyped x y) = PTyped (sm x) (sm y)

1820 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

src/Idris/AbsSyntaxTree.hs+20−18

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

681 | PFalse FC -- ^ _|_

682 | PRefl FC PTerm

683 | PResolveTC FC

684− | PEq FC PTerm PTerm -- ^ Equality type: A = B

684+ | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B

685 | PRewrite FC PTerm PTerm (Maybe PTerm)

686 | PPair FC PunInfo PTerm PTerm

687 | PDPair FC PunInfo PTerm PTerm PTerm

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

723 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

724 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)

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

726− mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

726+ mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)

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

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

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

@@ -1086,7 +1086,7 @@ eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]

1086 pimp (n "B") Placeholder False,

1087 pexp (PRef bi (n "x")),

1088 pexp (PRef bi (n "x"))])), bi, [])]

1089− where n a = sMN 0 a

1089+ where n a = sUN a

1090 reflDoc = parseDocstring . T.pack $

1091 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++

1092 "shown that both sides are in fact equal."

@@ -1096,7 +1096,7 @@ eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]

1096eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),

1097 (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")

1098 ]

1099− where n a = sMN 0 a

1099+ where n a = sUN a

1100

1101eqOpts = []

1102

@@ -1242,7 +1242,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1242 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1243 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1244 | UN nm <- basename f

1245− , not (ppopt_impl ppo) && null (getExps args) =

1245+ , not (ppopt_impl ppo) && null (getShowArgs args) =

1246 prettyName True (ppopt_impl ppo) bnd f

1247 prettySe p bnd (PAppBind _ (PRef _ f) [])

1248 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f

@@ -1250,14 +1250,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1250 | UN nm <- basename op

1251 , not (tnull nm) &&

1252 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

1253− case getExps args of

1253+ case getShowArgs args of

1254 [] -> opName True

1255− [x] -> group (opName True <$> group (prettySe 0 bnd x))

1255+ [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))

1256 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)

1257− in bracket p precedence $ inFix l r

1257+ in bracket p precedence $ inFix (getTm l) (getTm r)

1258+ (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1258− (l:r:rest) -> bracket p 1 $

1259+ bracket p 1 $

1259− enclose lparen rparen (inFix l r) <+>

1260+ enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1260− align (group (vsep (map (prettyArgSe bnd) rest)))

1261+ align (group (vsep (map (prettyArgS bnd) rest)))

1262+ as -> opName True <+> align (vsep (map (prettyArgS bnd) as))

1261 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op

1263 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op

1262 f = getFixity (opStr op)

1264 f = getFixity (opStr op)

1263 left l = case f of

1265 left l = case f of

@@ -1299,7 +1301,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1299 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1301 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1300 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1302 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1301 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"

1303 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"

1302− prettySe p bnd (PEq _ l r) =

1304+ prettySe p bnd (PEq _ _ _ l r) =

1303 bracket p 2 . align . group $

1305 bracket p 2 . align . group $

1304 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1306 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1305 where eq = annName eqTy (text "=")

1307 where eq = annName eqTy (text "=")

@@ -1596,7 +1598,7 @@ instance Sized PTerm where

1596 size (PFalse fc) = 1

1598 size (PFalse fc) = 1

1597 size (PRefl fc _) = 1

1599 size (PRefl fc _) = 1

1598 size (PResolveTC fc) = 1

1600 size (PResolveTC fc) = 1

1599− size (PEq fc left right) = 1 + size left + size right

1601+ size (PEq fc _ _ left right) = 1 + size left + size right

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

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

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

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

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

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

@@ -1634,7 +1636,7 @@ allNamesIn tm = nub $ ni [] tm

1634 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1636 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1635 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1637 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1636 ni env (PHidden tm) = ni env tm

1638 ni env (PHidden tm) = ni env tm

1637− ni env (PEq _ l r) = ni env l ++ ni env r

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

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

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

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

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

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

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

@@ -1659,7 +1661,7 @@ boundNamesIn tm = nub $ ni tm

1659 ni (PLam n ty sc) = n : (ni ty ++ ni sc)

1661 ni (PLam n ty sc) = n : (ni ty ++ ni sc)

1660 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

1662 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

1661 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))

1663 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))

1662− ni (PEq _ l r) = ni l ++ ni r

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

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

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

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

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

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

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

@@ -1695,7 +1697,7 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

1695 \\ nub (concatMap (ni env) (map fst os)))

1697 \\ nub (concatMap (ni env) (map fst os)))

1696 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1698 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1697 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1699 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1698− ni env (PEq _ l r) = ni env l ++ ni env r

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

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

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

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

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

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

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

@@ -1728,7 +1730,7 @@ namesIn uvars ist tm = nub $ ni [] tm

1728 \\ nub (concatMap (ni env) (map fst os)))

1730 \\ nub (concatMap (ni env) (map fst os)))

1729 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1731 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1730 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1732 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1731− ni env (PEq _ l r) = ni env l ++ ni env r

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

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

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

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

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

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

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

@@ -1759,7 +1761,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1759 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1761 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1760 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1762 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1761 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1763 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1762− ni env (PEq _ l r) = ni env l ++ ni env r

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

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

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

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

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

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

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

src/Idris/CaseSplit.hs+2−2

@@ -231,7 +231,7 @@ replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)

231 subst (PApp fc (PRef _ t) pats)

232 | isTConName t ctxt = Placeholder -- infer types

233 subst (PApp fc f pats) = PApp fc f (map substArg pats)

234− subst (PEq fc l r) = Placeholder -- PEq fc (subst l) (subst r)

234+ subst (PEq fc _ _ l r) = Placeholder -- PEq fc (subst l) (subst r)

235 subst x = x

236

237 substArg arg = arg { getTm = subst (getTm arg) }

@@ -349,7 +349,7 @@ getClause l fn fp

349 getNameFrom i used (PPi _ _ _ _)

350 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used

351 getNameFrom i used (PApp fc f as) = getNameFrom i used f

352− getNameFrom i used (PEq _ _ _) = uniqueNameFrom [sUN "prf"] used

352+ getNameFrom i used (PEq _ _ _ _ _) = uniqueNameFrom [sUN "prf"] used

353 getNameFrom i used (PRef fc f)

354 = case getNameHints i f of

355 [] -> uniqueName (sUN "x") used

src/Idris/DSL.hs+3−2

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

39 (map (fmap (expandDo dsl)) args)

40expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)

41 (map (pmap (expandDo dsl)) opts)

42−expandDo dsl (PEq fc l r) = PEq fc (expandDo dsl l) (expandDo dsl r)

42+expandDo dsl (PEq fc lt rt l r) = PEq fc (expandDo dsl lt) (expandDo dsl rt)

43+ (expandDo dsl l) (expandDo dsl r)

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

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

44expandDo dsl (PDPair fc p l t r) = PDPair fc p (expandDo dsl l) (expandDo dsl t)

45expandDo dsl (PDPair fc p l t r) = PDPair fc p (expandDo dsl l) (expandDo dsl t)

45 (expandDo dsl r)

46 (expandDo dsl r)

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

98 v' i (PTyped l r) = PTyped (v' i l) (v' i r)

99 v' i (PTyped l r) = PTyped (v' i l) (v' i r)

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

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

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

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

101− v' i (PEq f l r) = PEq f (v' i l) (v' i r)

102+ v' i (PEq f lt rt l r) = PEq f (v' i lt) (v' i rt) (v' i l) (v' i r)

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

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

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

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

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

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

src/Idris/DeepSeq.hs+1−1

@@ -205,7 +205,7 @@ instance NFData PTerm where

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

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

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

208− rnf (PEq x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

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

209 rnf (PRewrite x1 x2 x3 x4)

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

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

src/Idris/Delaborate.hs+68−9

@@ -12,8 +12,9 @@ import Idris.Core.Evaluate

12import Idris.Docstrings (overview, renderDocstring)

13import Idris.ErrReverse

15−import Data.List (intersperse)

15+import Data.List (intersperse, nub)

16import qualified Data.Text as T

17+import Control.Monad.State

18import Debug.Trace

19import Debug.Trace

@@ -96,9 +97,10 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

96 | n == sUN "Sigma"

97 | n == sUN "Sigma"

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

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

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

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

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

100+ deFn env (P _ n _) [lt,rt,l,r]

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

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

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

102+ | n == eqTy = PEq un (de env [] lt) (de env [] rt)

103+ (de env [] l) (de env [] r)

102 | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder

104 | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder

103 (de env [] r)

105 (de env [] r)

104 deFn env f@(P _ n _) args

106 deFn env f@(P _ n _) args

@@ -165,9 +167,10 @@ pprintErr' i (InternalMsg s) =

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

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

166 ]

168 ]

167pprintErr' i (CantUnify _ x_in y_in e sc s) =

169pprintErr' i (CantUnify _ x_in y_in e sc s) =

170+ let (x_ns, y_ns) = renameMNs x_in y_in

168− let (x, y) = addImplicitDiffs (delab i x_in) (delab i y_in) in

171+ (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in

169− text "Can't unify" <> indented (annTm x_in (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) x)) <$>

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

170− text "with" <> indented (annTm y_in (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) y)) <>

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

171 case e of

174 case e of

172 Msg "" -> empty

175 Msg "" -> empty

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

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

@@ -263,6 +266,41 @@ pprintErr' i (ReflectionFailed msg err) =

263 indented (pprintErr' i err) <>

266 indented (pprintErr' i err) <>

264 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

267 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

265

268

269+-- Make sure the machine invented names are shown helpfully to the user, so

270+-- that any names which differ internally also differ visibly

271+-- FIXME: I can't actually contrive an error to test this! Will revisit later...

272+renameMNs :: Term -> Term -> (Term, Term)

273+renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

274+ newnames = execState getRenames (zip ns ns) in

275+ (rename newnames x, rename newnames y)

276+ where

277+ getRenames :: State [(Name, Name)] ()

278+ getRenames = do getRs x; getRs y

279+

280+ getRs :: Term -> State [(Name, Name)] ()

281+ getRs (P _ n@(MN i x) _) = do

282+ nmap <- get

283+ when (n `notElem` map fst nmap) $

284+ put $ (n, uniqueName n (map fst nmap)) : nmap

285+ getRs (App f a) = do getRs f; getRs a

286+ getRs (Bind n b sc) = do

287+ nmap <- get

288+ when (n `notElem` map fst nmap) $

289+ put $ (n, uniqueName n (map fst nmap)) : nmap

290+ getRs sc

291+ getRs t = return ()

292+

293+ rename :: [(Name, Name)] -> Term -> Term

294+ rename ns (P nt x t) | Just x' <- lookup x ns = P nt x' t

295+ rename ns (App f a) = App (rename ns f) (rename ns a)

296+ rename ns (Bind x b sc)

297+ = let b' = fmap (rename ns) b

298+ sc' = rename ns sc in

299+ case lookup x ns of

300+ Just x' -> Bind x' b' sc'

301+ Nothing -> Bind x b' sc'

302+ rename ns x = x

303+

266-- If the two terms only differ in their implicits, mark the implicits which

304-- If the two terms only differ in their implicits, mark the implicits which

267-- differ as AlwaysShow so that they appear in errors

305-- differ as AlwaysShow so that they appear in errors

268addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)

306addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)

@@ -295,10 +333,30 @@ addImplicitDiffs x y

295 addI (PRefl fc a) (PRefl fc' b)

333 addI (PRefl fc a) (PRefl fc' b)

296 = let (a', b') = addI a b in

334 = let (a', b') = addI a b in

297 (PRefl fc a', PRefl fc' b')

335 (PRefl fc a', PRefl fc' b')

298− addI (PEq fc a b) (PEq fc' c d)

336+ addI (PEq fc at bt a b) (PEq fc' ct dt c d)

337+ | trace (show (at,bt)) False = undefined

338+ | at `expLike` ct && bt `expLike` dt

299 = let (a', c') = addI a c

339 = let (a', c') = addI a c

300 (b', d') = addI b d in

340 (b', d') = addI b d in

301− (PEq fc a' b', PEq fc' c' d')

341+ (PEq fc at bt a' b', PEq fc' ct dt c' d')

342+ | otherwise

343+ = let (at', ct') = addI at ct

344+ (bt', dt') = addI bt dt

345+ (a', c') = addI a c

346+ (b', d') = addI b d

347+ showa = if at `expLike` ct then [] else [AlwaysShow]

348+ showb = if bt `expLike` dt then [] else [AlwaysShow] in

349+ (PApp fc (PRef fc eqTy) [(pimp (sUN "A") at' True)

350+ { argopts = showa },

351+ (pimp (sUN "B") bt' True)

352+ { argopts = showb },

353+ pexp a', pexp b'],

354+ PApp fc (PRef fc eqTy) [(pimp (sUN "A") ct' True)

355+ { argopts = showa },

356+ (pimp (sUN "B") dt' True)

357+ { argopts = showb },

358+ pexp c', pexp d'])

359+

302 addI (PPair fc pi a b) (PPair fc' pi' c d)

360 addI (PPair fc pi a b) (PPair fc' pi' c d)

303 = let (a', c') = addI a c

361 = let (a', c') = addI a c

304 (b', d') = addI b d in

362 (b', d') = addI b d in

@@ -321,7 +379,8 @@ addImplicitDiffs x y

321 = n == n' && expLike s s' && expLike t t'

379 = n == n' && expLike s s' && expLike t t'

322 expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'

380 expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'

323 expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'

381 expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'

382+ expLike (PEq _ xt yt x y) (PEq _ xt' yt' x' y')

324− expLike (PEq _ x y) (PEq _ x' y') = expLike x x' && expLike y y'

383+ = expLike x x' && expLike y y'

325 expLike (PRefl _ x) (PRefl _ x') = expLike x x'

384 expLike (PRefl _ x) (PRefl _ x') = expLike x x'

326 expLike x y = x == y

385 expLike x y = x == y

327

386

src/Idris/ElabQuasiquote.hs+5−3

@@ -106,10 +106,12 @@ extractUnquotes (PCase fc expr cases)

106extractUnquotes (PRefl fc x)

107 = do (x', ex) <- extractUnquotes x

108 return (PRefl fc x', ex)

109−extractUnquotes (PEq fc a b)

109+extractUnquotes (PEq fc at bt a b)

110+ = do (at', ex1) <- extractUnquotes at

111+ (bt', ex2) <- extractUnquotes bt

110− = do (a', ex1) <- extractUnquotes a

112+ (a', ex1) <- extractUnquotes a

111 (b', ex2) <- extractUnquotes b

113 (b', ex2) <- extractUnquotes b

112− return (PEq fc a' b', ex1 ++ ex2)

114+ return (PEq fc at' bt' a' b', ex1 ++ ex2)

113extractUnquotes (PRewrite fc x y z)

115extractUnquotes (PRewrite fc x y z)

114 = do (x', ex1) <- extractUnquotes x

116 = do (x', ex1) <- extractUnquotes x

115 (y', ex2) <- extractUnquotes y

117 (y', ex2) <- extractUnquotes y

src/Idris/ElabTerm.hs+3−3

@@ -254,9 +254,9 @@ elab ist info emode opts fn tm

254 elab' ina (PRefl fc t)

255 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

256 pimp (sMN 0 "x") t False])

257− elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy)

257+ elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)

258− [pimp (sMN 0 "A") Placeholder True,

258+ [pimp (sUN "A") Placeholder True,

259− pimp (sMN 0 "B") Placeholder False,

259+ pimp (sUN "B") Placeholder False,

260 pexp l, pexp r])

261 elab' ina@(_, a, inty, qq) (PPair fc _ l r)

262 = do hnf_compute

src/Idris/IBC.hs+10−6

@@ -31,7 +31,7 @@ import Codec.Compression.Zlib (compress)

31import Util.Zlib (decompressEither)

33ibcVersion :: Word8

34−ibcVersion = 74

34+ibcVersion = 75

36data IBCFile = IBCFile { ver :: Word8,

37 sourcefile :: FilePath,

@@ -1406,10 +1406,12 @@ instance Binary PTerm where

1406 put x2

1407 PResolveTC x1 -> do putWord8 15

1408 put x1

1409− PEq x1 x2 x3 -> do putWord8 16

1409+ PEq x1 x2 x3 x4 x5 -> do putWord8 16

1410− put x1

1410+ put x1

1411− put x2

1411+ put x2

1412− put x3

1412+ put x3

1413+ put x4

1414+ put x5

1413 PRewrite x1 x2 x3 x4 -> do putWord8 17

1415 PRewrite x1 x2 x3 x4 -> do putWord8 17

1414 put x1

1416 put x1

1415 put x2

1417 put x2

@@ -1523,7 +1525,9 @@ instance Binary PTerm where

1523 16 -> do x1 <- get

1525 16 -> do x1 <- get

1524 x2 <- get

1526 x2 <- get

1525 x3 <- get

1527 x3 <- get

1528+ x4 <- get

1529+ x5 <- get

1526− return (PEq x1 x2 x3)

1530+ return (PEq x1 x2 x3 x4 x5)

1527 17 -> do x1 <- get

1531 17 -> do x1 <- get

1528 x2 <- get

1532 x2 <- get

1529 x3 <- get

1533 x3 <- get

src/Idris/IdrisDoc.hs+1−1

@@ -285,7 +285,7 @@ extractPTermNames (PMatchApp _ n) = [n]

285extractPTermNames (PCase _ p ps) = let (ps1, ps2) = unzip ps

286 in concatMap extract (p:(ps1 ++ ps2))

287extractPTermNames (PRefl _ p) = extract p

288−extractPTermNames (PEq _ p1 p2) = concatMap extract [p1, p2]

288+extractPTermNames (PEq _ _ _ p1 p2) = concatMap extract [p1, p2]

289extractPTermNames (PRewrite _ a b m) | Just c <- m =

290 concatMap extract [a, b, c]

291extractPTermNames (PRewrite _ a b _) = concatMap extract [a, b]

src/Idris/ParseOps.hs+1−1

@@ -38,7 +38,7 @@ table fixes

38 ++ toTable (reverse fixes) ++

39 [[backtick],

40 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

41− [binary "=" PEq AssocLeft]]

41+ [binary "=" (\fc x y -> PEq fc Placeholder Placeholder x y) AssocLeft]]

42 where

43 flatten :: PTerm -> PTerm -- flatten application

44 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

test/basic009/expected+1−1

@@ -1,5 +1,5 @@

1MAIN-PASS

2Faulty.idr:6:7:When elaborating type of Faulty.fault:

3−When elaborating an application of type constructor =:

3+When elaborating argument x to type constructor =:

4 Can't disambiguate name: A.num, B.C.num

5Multiple.idr:3:1:import alias not unique: "X"