53e1281 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove PEq

53e1281Melvar Chen11 years ago

src/Idris/AbsSyntax.hs−19

compare with master

unifiedsplit

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

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

973 = let n' = mkShadow n in

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

975− en (PEq f lt rt l r) = PEq f (en lt) (en rt) (en l) (en r)

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

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

977 en (PTyped l r) = PTyped (en l) (en r)

976 en (PTyped l r) = PTyped (en l) (en r)

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

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

@@ -1140,7 +1139,6 @@ getPriority i tm = 1 -- pri tm

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

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

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

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

1142 pri (PTrue _ _) = 0

1141 pri (PTrue _ _) = 0

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

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

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

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

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

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

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

@@ -1450,10 +1448,6 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

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

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

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

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

1452 imps True (n:env) sc

1450 imps True (n:env) sc

1453− imps top env (PEq _ _ _ l r)

1454− = do (decls, ns) <- get

1455− let isn = namesIn uvars ist l ++ namesIn uvars ist r

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

1457 imps top env (PRewrite _ l r _)

1451 imps top env (PRewrite _ l r _)

1458 = do (decls, ns) <- get

1452 = do (decls, ns) <- get

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

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

@@ -1523,12 +1517,6 @@ addImpl' inpat env infns imp_meths ist ptm

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

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

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

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

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

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

1526− ai qq env ds (PEq fc lt rt l r)

1527− = let lt' = ai qq env ds lt

1528− rt' = ai qq env ds rt

1529− l' = ai qq env ds l

1530− r' = ai qq env ds r in

1531− PEq fc lt' rt' l' r'

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

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

1533 = let l' = ai qq env ds l

1521 = let l' = ai qq env ds l

1534 r' = ai qq env ds r

1522 r' = ai qq env ds r

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

1813 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)

1801 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)

1814 su t@(PLam fc _ _ _) = PHidden t

1802 su t@(PLam fc _ _ _) = PHidden t

1815 su t@(PPi _ _ _ _) = PHidden t

1803 su t@(PPi _ _ _ _) = PHidden t

1816− su t@(PEq _ _ _ _ _) = PHidden t

1817 su t = t

1804 su t = t

1818

1805

1819 ctxt = tt_ctxt i

1806 ctxt = tt_ctxt i

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

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

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

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

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

1918 = return [(n, tm)]

1905 = return [(n, tm)]

1919− match (PEq _ _ _ l r) (PEq _ _ _ l' r')

1920− = do ml <- match' l l'

1921− mr <- match' r r'

1922− return (ml ++ mr)

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

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

1924 = do ml <- match' l l'

1907 = do ml <- match' l l'

1925 mr <- match' r r'

1908 mr <- match' r r'

@@ -2015,7 +1998,6 @@ substMatchShadow n shs tm t = sm shs t where

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

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

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

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

2017 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)

2000 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)

2018− sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)

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

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

2020 (fmap (sm xs) tm)

2002 (fmap (sm xs) tm)

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

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

@@ -2044,7 +2026,6 @@ shadow n n' t = sm t where

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

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

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

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

2046 sm (PIfThenElse fc c t f) = PIfThenElse fc (sm c) (sm t) (sm f)

2028 sm (PIfThenElse fc c t f) = PIfThenElse fc (sm c) (sm t) (sm f)

2047− sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)

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

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

2049 sm (PTyped x y) = PTyped (sm x) (sm y)

2030 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

src/Idris/AbsSyntaxTree.hs+15−24

@@ -819,7 +819,6 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

819 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

820 | PTrue FC PunInfo -- ^ Unit type..?

821 | PResolveTC FC -- ^ Solve this dictionary by type class resolution

822− | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B

823 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type

822 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type

824 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)

823 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)

825 | PDPair FC PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration)

824 | PDPair FC PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration)

@@ -866,7 +865,6 @@ mapPT f t = f (mpt t) where

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

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

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

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

868 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)

867 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)

869− mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)

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

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

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

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

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

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

@@ -1027,7 +1025,6 @@ highestFC (PCase fc _ _) = Just fc

1027highestFC (PIfThenElse fc _ _ _) = Just fc

1025highestFC (PIfThenElse fc _ _ _) = Just fc

1028highestFC (PTrue fc _) = Just fc

1026highestFC (PTrue fc _) = Just fc

1029highestFC (PResolveTC fc) = Just fc

1027highestFC (PResolveTC fc) = Just fc

1030−highestFC (PEq fc _ _ _ _) = Just fc

1031highestFC (PRewrite fc _ _ _) = Just fc

1028highestFC (PRewrite fc _ _ _) = Just fc

1032highestFC (PPair fc _ _ _) = Just fc

1029highestFC (PPair fc _ _ _) = Just fc

1033highestFC (PDPair fc _ _ _ _) = Just fc

1030highestFC (PDPair fc _ _ _ _) = Just fc

@@ -1479,6 +1476,21 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1479 bracket p startPrec $

1476 bracket p startPrec $

1480 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>

1477 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>

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

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

1479+ -- This case preserves the behavior of the former constructor PEq.

1480+ -- It should be removed if feasible when the pretty-printing of infix

1481+ -- operators in general is improved.

1482+ prettySe p bnd (PApp _ (PRef _ n) [lt, rt, l, r])

1483+ | n == eqTy, ppopt_impl ppo =

1484+ bracket p eqPrec $

1485+ enclose lparen rparen eq <+>

1486+ align (group (vsep (map (prettyArgS bnd)

1487+ [lt, rt, l, r])))

1488+ | n == eqTy =

1489+ bracket p eqPrec . align . group $

1490+ prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))

1491+ where eq = annName eqTy (text "=")

1492+ eqPrec = startPrec

1493+ prettyTerm = prettySe (eqPrec + 1) bnd

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

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

1483 | UN nm <- basename f

1495 | UN nm <- basename f

1484 , not (ppopt_impl ppo) && null (getShowArgs args) =

1496 , not (ppopt_impl ppo) && null (getShowArgs args) =

@@ -1558,21 +1570,6 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1558 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1570 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

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

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

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

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

1561− prettySe p bnd (PEq _ lt rt l r)

1562− | ppopt_impl ppo =

1563− bracket p eqPrec $

1564− enclose lparen rparen eq <+>

1565− align (group (vsep (map (prettyArgS bnd)

1566− [PImp 0 False [] (sUN "A") lt,

1567− PImp 0 False [] (sUN "B") rt,

1568− PExp 0 [] (sUN "x") l,

1569− PExp 0 [] (sUN "y") r])))

1570− | otherwise =

1571− bracket p eqPrec . align . group $

1572− prettyTerm l <+> eq <$> group (prettyTerm r)

1573− where eq = annName eqTy (text "=")

1574− eqPrec = startPrec

1575− prettyTerm = prettySe (eqPrec + 1) bnd

1576 prettySe p bnd (PRewrite _ l r _) =

1573 prettySe p bnd (PRewrite _ l r _) =

1577 bracket p startPrec $

1574 bracket p startPrec $

1578 text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r

1575 text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r

@@ -1870,7 +1867,6 @@ instance Sized PTerm where

1870 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])

1867 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])

1871 size (PTrue fc _) = 1

1868 size (PTrue fc _) = 1

1872 size (PResolveTC fc) = 1

1869 size (PResolveTC fc) = 1

1873− size (PEq fc _ _ left right) = 1 + size left + size right

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

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

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

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

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

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

@@ -1911,7 +1907,6 @@ allNamesIn tm = nub $ ni [] tm

1911 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

1907 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

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

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

1913 ni env (PHidden tm) = ni env tm

1909 ni env (PHidden tm) = ni env tm

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

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

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

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

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

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

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

@@ -1938,7 +1933,6 @@ boundNamesIn tm = S.toList (ni S.empty tm)

1938 ni set (PLam fc n ty sc) = S.insert n $ ni (ni set ty) sc

1933 ni set (PLam fc n ty sc) = S.insert n $ ni (ni set ty) sc

1939 ni set (PLet fc n ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc

1934 ni set (PLet fc n ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc

1940 ni set (PPi p n ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p

1935 ni set (PPi p n ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p

1941− ni set (PEq _ _ _ l r) = ni (ni set l) r

1942 ni set (PRewrite _ l r _) = ni (ni set l) r

1936 ni set (PRewrite _ l r _) = ni (ni set l) r

1943 ni set (PTyped l r) = ni (ni set l) r

1937 ni set (PTyped l r) = ni (ni set l) r

1944 ni set (PPair _ _ l r) = ni (ni set l) r

1938 ni set (PPair _ _ l r) = ni (ni set l) r

@@ -1978,7 +1972,6 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

1978 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

1972 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

1979 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

1973 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

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

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

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

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

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

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

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

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

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

@@ -2009,7 +2002,6 @@ namesIn uvars ist tm = nub $ ni [] tm

2009 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

2002 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

2010 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

2003 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

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

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

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

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

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

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

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

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

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

@@ -2041,7 +2033,6 @@ usedNamesIn vars ist tm = nub $ ni [] tm

2041 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

2033 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

2042 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

2034 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

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

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

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

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

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

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

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

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

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

src/Idris/CaseSplit.hs−2

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

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

241 | isTConName t ctxt = Placeholder -- infer types

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

243− subst (PEq fc _ _ l r) = Placeholder -- PEq fc (subst l) (subst r)

244 subst x = x

243 subst x = x

245

244

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

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

@@ -361,7 +360,6 @@ getClause l fn fp

361 getNameFrom i used (PPi _ _ _ _)

360 getNameFrom i used (PPi _ _ _ _)

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

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

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

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

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

365 getNameFrom i used (PRef fc f)

363 getNameFrom i used (PRef fc f)

366 = case getNameHints i f of

364 = case getNameHints i f of

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

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

src/Idris/DSL.hs−3

@@ -77,8 +77,6 @@ expandSugar dsl (PIfThenElse fc c t f) =

77 , PExp 0 [] (sMN 0 "whenTrue") $ expandSugar dsl t

78 , PExp 0 [] (sMN 0 "whenFalse") $ expandSugar dsl f

79 ]

80−expandSugar dsl (PEq fc lt rt l r) = PEq fc (expandSugar dsl lt) (expandSugar dsl rt)

81− (expandSugar dsl l) (expandSugar dsl r)

82expandSugar dsl (PPair fc p l r) = PPair fc p (expandSugar dsl l) (expandSugar dsl r)

80expandSugar dsl (PPair fc p l r) = PPair fc p (expandSugar dsl l) (expandSugar dsl r)

83expandSugar dsl (PDPair fc p l t r) = PDPair fc p (expandSugar dsl l) (expandSugar dsl t)

81expandSugar dsl (PDPair fc p l t r) = PDPair fc p (expandSugar dsl l) (expandSugar dsl t)

84 (expandSugar dsl r)

82 (expandSugar dsl r)

@@ -139,7 +137,6 @@ var dsl n t i = v' i t where

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

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

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

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

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

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

142− v' i (PEq f lt rt l r) = PEq f (v' i lt) (v' i rt) (v' i l) (v' i r)

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

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

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

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

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

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

src/Idris/DeepSeq.hs−1

@@ -220,7 +220,6 @@ instance NFData PTerm where

220 rnf (PIfThenElse x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

221 rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

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

223− rnf (PEq x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

224 rnf (PRewrite x1 x2 x3 x4)

223 rnf (PRewrite x1 x2 x3 x4)

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

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

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

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

src/Idris/Delaborate.hs−28

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

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

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

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

117− | n == eqTy = PEq un (de env [] lt) (de env [] rt)

118− (de env [] l) (de env [] r)

119 | n == sigmaCon = PDPair un IsTerm (de env [] l) Placeholder

117 | n == sigmaCon = PDPair un IsTerm (de env [] l) Placeholder

120 (de env [] r)

118 (de env [] r)

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

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

@@ -484,30 +482,6 @@ addImplicitDiffs x y

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

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

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

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

486 (PPi p n a' b', PPi p' n' c' d')

484 (PPi p n a' b', PPi p' n' c' d')

487− addI (PEq fc at bt a b) (PEq fc' ct dt c d)

488− | trace (show (at,bt)) False = undefined

489− | at `expLike` ct && bt `expLike` dt

490− = let (a', c') = addI a c

491− (b', d') = addI b d in

492− (PEq fc at bt a' b', PEq fc' ct dt c' d')

493− | otherwise

494− = let (at', ct') = addI at ct

495− (bt', dt') = addI bt dt

496− (a', c') = addI a c

497− (b', d') = addI b d

498− showa = if at `expLike` ct then [] else [AlwaysShow]

499− showb = if bt `expLike` dt then [] else [AlwaysShow] in

500− (PApp fc (PRef fc eqTy) [(pimp (sUN "A") at' True)

501− { argopts = showa },

502− (pimp (sUN "B") bt' True)

503− { argopts = showb },

504− pexp a', pexp b'],

505− PApp fc (PRef fc eqTy) [(pimp (sUN "A") ct' True)

506− { argopts = showa },

507− (pimp (sUN "B") dt' True)

508− { argopts = showb },

509− pexp c', pexp d'])

510−

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

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

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

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

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

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

@@ -530,8 +504,6 @@ addImplicitDiffs x y

530 = n == n' && expLike s s' && expLike t t'

504 = n == n' && expLike s s' && expLike t t'

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

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

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

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

533− expLike (PEq _ xt yt x y) (PEq _ xt' yt' x' y')

534− = expLike x x' && expLike y y'

535 expLike x y = x == y

507 expLike x y = x == y

536

508

537-- Issue #1589 on the issue tracker

509-- Issue #1589 on the issue tracker

src/Idris/Elab/Term.hs+1−5

@@ -343,7 +343,7 @@ elab ist info emode opts fn tm

343 elab' ina fc (PResolveTC fc')

344 = do c <- getNameFrom (sMN 0 "class")

345 instanceArg c

346− elab' ina _ (PEq fc Placeholder Placeholder l r)

346+ elab' ina _ (PApp fc (PRef _ n) args) | n == eqTy, [Placeholder, Placeholder, l, r] <- map getTm args

347 = try (do tyn <- getNameFrom (sMN 0 "aqty")

348 claim tyn RType

349 movelast tyn

@@ -362,10 +362,6 @@ elab ist info emode opts fn tm

362 pimp (sUN "B") (PRef fc btyn) False,

363 pexp l, pexp r]))

364

365− elab' ina _ (PEq fc lt rt l r) = elab' ina (Just fc) (PApp fc (PRef fc eqTy)

366− [pimp (sUN "A") lt True,

367− pimp (sUN "B") rt False,

368− pexp l, pexp r])

369 elab' ina _ (PPair fc _ l r)

365 elab' ina _ (PPair fc _ l r)

370 = do hnf_compute

366 = do hnf_compute

371 g <- goal

367 g <- goal

src/Idris/ElabQuasiquote.hs−6

@@ -109,12 +109,6 @@ extractUnquotes n (PIfThenElse fc c t f)

109 (t', ex2) <- extractUnquotes n t

110 (f', ex3) <- extractUnquotes n f

111 return (PIfThenElse fc c' t' f', ex1 ++ ex2 ++ ex3)

112−extractUnquotes n (PEq fc at bt a b)

113− = do (at', ex1) <- extractUnquotes n at

114− (bt', ex2) <- extractUnquotes n bt

115− (a', ex1) <- extractUnquotes n a

116− (b', ex2) <- extractUnquotes n b

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

118extractUnquotes n (PRewrite fc x y z)

112extractUnquotes n (PRewrite fc x y z)

119 = do (x', ex1) <- extractUnquotes n x

113 = do (x', ex1) <- extractUnquotes n x

120 (y', ex2) <- extractUnquotes n y

114 (y', ex2) <- extractUnquotes n y

src/Idris/Error.hs−2

@@ -105,8 +105,6 @@ warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>

105warnDisamb ist (PIfThenElse _ c t f) = mapM_ (warnDisamb ist) [c, t, f]

106warnDisamb ist (PTrue _ _) = return ()

107warnDisamb ist (PResolveTC _) = return ()

108−warnDisamb ist (PEq _ a b x y) = warnDisamb ist a >> warnDisamb ist b >>

109− warnDisamb ist x >> warnDisamb ist y

110warnDisamb ist (PRewrite _ x y z) = warnDisamb ist x >> warnDisamb ist y >>

108warnDisamb ist (PRewrite _ x y z) = warnDisamb ist x >> warnDisamb ist y >>

111 Foldable.mapM_ (warnDisamb ist) z

109 Foldable.mapM_ (warnDisamb ist) z

112warnDisamb ist (PPair _ _ x y) = warnDisamb ist x >> warnDisamb ist y

110warnDisamb ist (PPair _ _ x y) = warnDisamb ist x >> warnDisamb ist y

src/Idris/IBC.hs−12

@@ -1544,12 +1544,6 @@ instance Binary PTerm where

1544 put x2

1545 PResolveTC x1 -> do putWord8 15

1546 put x1

1547− PEq x1 x2 x3 x4 x5 -> do putWord8 16

1548− put x1

1549− put x2

1550− put x3

1551− put x4

1552− put x5

1553 PRewrite x1 x2 x3 x4 -> do putWord8 17

1547 PRewrite x1 x2 x3 x4 -> do putWord8 17

1554 put x1

1548 put x1

1555 put x2

1549 put x2

@@ -1680,12 +1674,6 @@ instance Binary PTerm where

1680 return (PTrue x1 x2)

1674 return (PTrue x1 x2)

1681 15 -> do x1 <- get

1675 15 -> do x1 <- get

1682 return (PResolveTC x1)

1676 return (PResolveTC x1)

1683− 16 -> do x1 <- get

1684− x2 <- get

1685− x3 <- get

1686− x4 <- get

1687− x5 <- get

1688− return (PEq x1 x2 x3 x4 x5)

1689 17 -> do x1 <- get

1677 17 -> do x1 <- get

1690 x2 <- get

1678 x2 <- get

1691 x3 <- get

1679 x3 <- get

src/Idris/IdrisDoc.hs−1

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

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

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

305extractPTermNames (PIfThenElse _ c t f) = concatMap extract [c, t, f]

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

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

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

308 concatMap extract [a, b, c]

307 concatMap extract [a, b, c]

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

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

src/Idris/ParseOps.hs+1−1

@@ -37,7 +37,7 @@ table fixes

37 toTable (reverse fixes) ++

38 [[backtick],

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

40− [binary "=" (\fc x y -> PEq fc Placeholder Placeholder x y) AssocLeft],

40+ [binary "=" (\fc x y -> PApp fc (PRef fc eqTy) [pexp x, pexp y]) AssocLeft],

41 [nofixityoperator]]

42 where

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

test/reg037/reg037.idr+1−1

@@ -4,6 +4,6 @@

4class Foo (t : a -> b -> Type) where

5 foo : (x : _) -> (y : _) -> t x y -> t x y

7−instance Foo (=) where

7+instance Foo ((=) {A=a} {B=b}) where

8 foo x y prf = prf