7e8e25b · Idris-dev · git.iko.soy

docs/proofs/patterns.rst+2−2

compare with master

unifiedsplit

@@ -46,7 +46,7 @@ declaration. You should see:

46 plus_commutes n m = ?plus_commutes_rhs

47

48To prove this by induction on ``n``, as we sketched in Section

49−[sect:induction], we begin with a case split on ``n`` (press

49+:ref:`sect-inductive`, we begin with a case split on ``n`` (press

50``\c`` with the cursor over the ``n`` in the definition.) You

51should see:

52

@@ -334,7 +334,7 @@ defined by matching on its first argument. The complete definition is:

334 plus_commutes_S k Z = Refl

335 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl

336

337−All metavariables have now been solved,

337+All metavariables have now been solved.

338

339The ``total`` annotation means that we require the final function to

340pass the totality checker; i.e. it will terminate on all possible

docs/tutorial/interp.rst+2−2

@@ -213,7 +213,7 @@ because of its type:

213

214 interp env (App f s) = interp env f (interp env s)

215

216−Operators and interpreters are, again, direct translations into the

216+Operators and conditionals are, again, direct translations into the

217equivalent Idris constructs. For operators, we apply the function to

218its operands directly, and for ``If``, we apply the Idris

219``if...then...else`` construct directly.

@@ -236,7 +236,7 @@ We can make some simple test functions. Firstly, adding two inputs

236 add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))

237

238More interestingly, a factorial function ``fact``

239−(e.g. ``\. if (x == 0) then 1 else (fact (x-1) * x)``),

239+(e.g. ``\x. if (x == 0) then 1 else (fact (x-1) * x)``),

240can be written as:

241

242.. code-block:: idris

docs/tutorial/modules.rst+25−3

@@ -26,7 +26,7 @@ module which defines a binary tree type ``BTree`` (in a file

26

27 toList : BTree a -> List a

28 toList Leaf = []

29− toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)

29+ toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)

30

31 toTree : Ord a => List a -> BTree a

32 toTree [] = Leaf

@@ -44,7 +44,7 @@ Then, this gives a main program (in a file

44

45 main : IO ()

46 main = do let t = toTree [1,8,2,7,9,3]

47− print (btree.toList t)

47+ print (Btree.toList t)

48

49

50

@@ -118,7 +118,7 @@ functions to be exported as ``abstract``, as we see below:

118 abstract

119 toList : BTree a -> List a

120 toList Leaf = []

121− toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)

121+ toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)

122

123 abstract

124 toTree : Ord a => List a -> BTree a

@@ -128,6 +128,28 @@ functions to be exported as ``abstract``, as we see below:

128Finally, the default export mode can be changed with the ``%access``

129directive, for example:

130

131+.. code-block:: idris

132+

133+ module Btree

134+

135+ %access abstract

136+

137+ data BTree a = Leaf

138+ | Node (BTree a) a (BTree a)

139+

140+ insert : Ord a => a -> BTree a -> BTree a

141+ insert x Leaf = Node Leaf x Leaf

142+ insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

143+ else (Node l v (insert x r))

144+

145+ toList : BTree a -> List a

146+ toList Leaf = []

147+ toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)

148+

149+ toTree : Ord a => List a -> BTree a

150+ toTree [] = Leaf

151+ toTree (x :: xs) = insert x (toTree xs)

152+

131In this case, any function with no access modifier will be exported as

153In this case, any function with no access modifier will be exported as

132``abstract``, rather than left ``private``.

154``abstract``, rather than left ``private``.

133

155

src/Idris/AbsSyntax.hs+2−25

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

@@ -1141,8 +1140,6 @@ getPriority i tm = 1 -- pri tm

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

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

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

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

1143 pri (PTrue _ _) = 0

1142 pri (PTrue _ _) = 0

1144− pri (PRefl _ _) = 1

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

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

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

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

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

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

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

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

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

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

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

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

1454 imps True (n:env) sc

1451 imps True (n:env) sc

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

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

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

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

1459 imps top env (PRewrite _ l r _)

1452 imps top env (PRewrite _ l r _)

1460 = do (decls, ns) <- get

1453 = do (decls, ns) <- get

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

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

@@ -1525,12 +1518,6 @@ addImpl' inpat env infns imp_meths ist ptm

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

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

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

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

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

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

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

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

1530− rt' = ai qq env ds rt

1531− l' = ai qq env ds l

1532− r' = ai qq env ds r in

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

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

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

1535 = let l' = ai qq env ds l

1522 = let l' = ai qq env ds l

1536 r' = ai qq env ds r

1523 r' = ai qq env ds r

@@ -1611,7 +1598,6 @@ addImpl' inpat env infns imp_meths ist ptm

1611 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)

1598 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)

1612 -- Don't do PProof or PTactics since implicits get added when scope is

1599 -- Don't do PProof or PTactics since implicits get added when scope is

1613 -- properly known in ElabTerm.runTac

1600 -- properly known in ElabTerm.runTac

1614− ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)

1615 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)

1601 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)

1616 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)

1602 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)

1617 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)

1603 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)

@@ -1791,10 +1777,9 @@ stripLinear i tm = evalState (sl tm) [] where

1791 return $ PTacImplicit p l n sc t'

1777 return $ PTacImplicit p l n sc t'

1792 sl x = return x

1778 sl x = return x

1793

1779

1794−-- Remove functions which aren't applied to anything, which must then

1780+-- | Remove functions which aren't applied to anything, which must then

1795-- be resolved by unification. Assume names resolved and alternatives

1781-- be resolved by unification. Assume names resolved and alternatives

1796-- filled in (so no ambiguity).

1782-- filled in (so no ambiguity).

1797−

1798stripUnmatchable :: IState -> PTerm -> PTerm

1783stripUnmatchable :: IState -> PTerm -> PTerm

1799stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1784stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1800 su :: PTerm -> PTerm

1785 su :: PTerm -> PTerm

@@ -1816,9 +1801,8 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1816 else PAlternative b alts'

1801 else PAlternative b alts'

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

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

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

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

1819− su t@(PLam _ _ _ _ _) = PHidden t

1804+ su t@(PLam fc _ _ _ _) = PHidden t

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

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

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

1822 su t = t

1806 su t = t

1823

1807

1824 ctxt = tt_ctxt i

1808 ctxt = tt_ctxt i

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

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

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

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

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

1923 = return [(n, tm)]

1907 = return [(n, tm)]

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

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

1926− mr <- match' r r'

1927− return (ml ++ mr)

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

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

1929 = do ml <- match' l l'

1909 = do ml <- match' l l'

1930 mr <- match' r r'

1910 mr <- match' r r'

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

1955 match (PQuote _) _ = return []

1935 match (PQuote _) _ = return []

1956 match (PProof _) _ = return []

1936 match (PProof _) _ = return []

1957 match (PTactics _) _ = return []

1937 match (PTactics _) _ = return []

1958− match (PRefl _ _) (PRefl _ _) = return []

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

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

1960 match (PTrue _ _) (PTrue _ _) = return []

1939 match (PTrue _ _) (PTrue _ _) = return []

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

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

@@ -2021,7 +2000,6 @@ substMatchShadow n shs tm t = sm shs t where

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

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

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

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

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

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

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

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

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

2026 (fmap (sm xs) tm)

2004 (fmap (sm xs) tm)

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

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

@@ -2050,7 +2028,6 @@ shadow n n' t = sm t where

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

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

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

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

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

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

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

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

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

2055 sm (PTyped x y) = PTyped (sm x) (sm y)

2032 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

src/Idris/AbsSyntaxTree.hs+15−28

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

827 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse

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

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

830− | PRefl FC PTerm -- ^ The canonical proof of the equality type

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

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

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

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

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

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

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

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

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

@@ -876,7 +874,6 @@ mapPT f t = f (mpt t) where

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1036,9 +1033,7 @@ highestFC (PMatchApp fc _) = Just fc

1036highestFC (PCase fc _ _) = Just fc

1033highestFC (PCase fc _ _) = Just fc

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

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

1038highestFC (PTrue fc _) = Just fc

1035highestFC (PTrue fc _) = Just fc

1039−highestFC (PRefl fc _) = Just fc

1040highestFC (PResolveTC fc) = Just fc

1036highestFC (PResolveTC fc) = Just fc

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

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

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

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

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

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

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

@@ -1490,6 +1485,21 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1490 bracket p startPrec $

1485 bracket p startPrec $

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

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

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

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

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

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

1490+ -- operators in general is improved.

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

1492+ | n == eqTy, ppopt_impl ppo =

1493+ bracket p eqPrec $

1494+ enclose lparen rparen eq <+>

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

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

1497+ | n == eqTy =

1498+ bracket p eqPrec . align . group $

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

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

1501+ eqPrec = startPrec

1502+ prettyTerm = prettySe (eqPrec + 1) bnd

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

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

1494 | UN nm <- basename f

1504 | UN nm <- basename f

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

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

@@ -1565,26 +1575,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1565 , kwd "else" <+> prettySe startPrec bnd f

1575 , kwd "else" <+> prettySe startPrec bnd f

1566 ]

1576 ]

1567 prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm

1577 prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm

1568− prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"

1569 prettySe p bnd (PResolveTC _) = kwd "%instance"

1578 prettySe p bnd (PResolveTC _) = kwd "%instance"

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

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

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

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

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

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

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

1574− | ppopt_impl ppo =

1575− bracket p eqPrec $

1576− enclose lparen rparen eq <+>

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

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

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

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

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

1582− | otherwise =

1583− bracket p eqPrec . align . group $

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

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

1586− eqPrec = startPrec

1587− prettyTerm = prettySe (eqPrec + 1) bnd

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

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

1589 bracket p startPrec $

1583 bracket p startPrec $

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

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

@@ -1881,9 +1875,7 @@ instance Sized PTerm where

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

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

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

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

1883 size (PTrue fc _) = 1

1877 size (PTrue fc _) = 1

1884− size (PRefl fc _) = 1

1885 size (PResolveTC fc) = 1

1878 size (PResolveTC fc) = 1

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

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

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

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

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

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

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

@@ -1924,7 +1916,6 @@ allNamesIn tm = nub $ ni [] tm

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

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

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

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

1926 ni env (PHidden tm) = ni env tm

1918 ni env (PHidden tm) = ni env tm

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2047 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−2

@@ -231,9 +231,7 @@ instance NFData PTerm where

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

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

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

234− rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

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

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

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

237 rnf (PRewrite x1 x2 x3 x4)

235 rnf (PRewrite x1 x2 x3 x4)

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

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

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

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

src/Idris/Delaborate.hs−33

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

107 deFn env (App _ f a) args = deFn env f (a:args)

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

109 | n == pairTy = PPair un IsType (de env [] l) (de env [] r)

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

111 | n == sUN "lazy" = de env [] r -- TODO: Fix string based matching

110 | n == sUN "lazy" = de env [] r -- TODO: Fix string based matching

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

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

113 | n == sigmaTy

112 | n == sigmaTy

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

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

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

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

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

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

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

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

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

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

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

121 (de env [] r)

118 (de env [] r)

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

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

@@ -485,33 +482,6 @@ addImplicitDiffs x y

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

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

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

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

487 (PPi p n fc a' b', PPi p' n' fc' c' d')

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

488− addI (PRefl fc a) (PRefl fc' b)

489− = let (a', b') = addI a b in

490− (PRefl fc a', PRefl fc' b')

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

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

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

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

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

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

497− | otherwise

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

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

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

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

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

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

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

505− { argopts = showa },

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

507− { argopts = showb },

508− pexp a', pexp b'],

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

510− { argopts = showa },

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

512− { argopts = showb },

513− pexp c', pexp d'])

514−

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

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

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

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

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

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

@@ -534,9 +504,6 @@ addImplicitDiffs x y

534 = n == n' && expLike s s' && expLike t t'

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

535 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'

536 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'

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

538− = expLike x x' && expLike y y'

539− expLike (PRefl _ x) (PRefl _ x') = expLike x x'

540 expLike x y = x == y

507 expLike x y = x == y

541

508

542-- Issue #1589 on the issue tracker

509-- Issue #1589 on the issue tracker

src/Idris/Elab/Clause.hs+1−1

@@ -897,7 +897,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

897 (map (pexp . (PRef fc) . fst) bargs_post) ++

898 case mpn of

899 Nothing -> []

900− Just _ -> [pexp (PRefl fc Placeholder)])

900+ Just _ -> [pexp (PRef fc eqCon)])

901 logLvl 5 ("New RHS " ++ showTmImpls rhs)

902 ctxt <- getContext -- New context with block added

903 i <- getIState

src/Idris/Elab/Term.hs+4−9

@@ -351,11 +351,10 @@ elab ist info emode opts fn tm

351 elab' ina fc (PResolveTC fc')

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

353 instanceArg c

354− elab' ina _ (PRefl fc t)

354+ -- Elaborate the equality type first homogeneously, then

355+ -- heterogeneously as a fallback

355− = do elab' ina (Just fc) (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

356+ elab' ina _ (PApp fc (PRef _ n) args)

356− pimp (sMN 0 "x") t False])

357+ | n == eqTy, [Placeholder, Placeholder, l, r] <- map getTm args

357− highlightSource fc (AnnName eqCon Nothing Nothing Nothing)

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

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

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

360 claim tyn RType

359 claim tyn RType

361 movelast tyn

360 movelast tyn

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

374 pimp (sUN "B") (PRef NoFC btyn) False,

373 pimp (sUN "B") (PRef NoFC btyn) False,

375 pexp l, pexp r]))

374 pexp l, pexp r]))

376

375

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

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

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

380− pexp l, pexp r])

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

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

382 = do hnf_compute

377 = do hnf_compute

383 g <- goal

378 g <- goal

src/Idris/ElabQuasiquote.hs−9

@@ -109,15 +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 (PRefl fc x)

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

114− return (PRefl fc x', ex)

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

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

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

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

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

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

121extractUnquotes n (PRewrite fc x y z)

112extractUnquotes n (PRewrite fc x y z)

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

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

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

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

src/Idris/Error.hs−3

@@ -104,10 +104,7 @@ warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>

104 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases

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

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

107−warnDisamb ist (PRefl _ tm) = warnDisamb ist tm

108warnDisamb ist (PResolveTC _) = return ()

107warnDisamb ist (PResolveTC _) = return ()

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

110− warnDisamb ist x >> warnDisamb ist y

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

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

112 Foldable.mapM_ (warnDisamb ist) z

109 Foldable.mapM_ (warnDisamb ist) z

113warnDisamb 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−18

@@ -1557,17 +1557,8 @@ instance Binary PTerm where

1557 PTrue x1 x2 -> do putWord8 12

1558 put x1

1559 put x2

1560− PRefl x1 x2 -> do putWord8 14

1561− put x1

1562− put x2

1563 PResolveTC x1 -> do putWord8 15

1560 PResolveTC x1 -> do putWord8 15

1564 put x1

1561 put x1

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

1566− put x1

1567− put x2

1568− put x3

1569− put x4

1570− put x5

1571 PRewrite x1 x2 x3 x4 -> do putWord8 17

1562 PRewrite x1 x2 x3 x4 -> do putWord8 17

1572 put x1

1563 put x1

1573 put x2

1564 put x2

@@ -1701,17 +1692,8 @@ instance Binary PTerm where

1701 12 -> do x1 <- get

1692 12 -> do x1 <- get

1702 x2 <- get

1693 x2 <- get

1703 return (PTrue x1 x2)

1694 return (PTrue x1 x2)

1704− 14 -> do x1 <- get

1705− x2 <- get

1706− return (PRefl x1 x2)

1707 15 -> do x1 <- get

1695 15 -> do x1 <- get

1708 return (PResolveTC x1)

1696 return (PResolveTC x1)

1709− 16 -> do x1 <- get

1710− x2 <- get

1711− x3 <- get

1712− x4 <- get

1713− x5 <- get

1714− return (PEq x1 x2 x3 x4 x5)

1715 17 -> do x1 <- get

1697 17 -> do x1 <- get

1716 x2 <- get

1698 x2 <- get

1717 x3 <- get

1699 x3 <- get

src/Idris/IdrisDoc.hs−2

@@ -303,8 +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 (PRefl _ p) = extract p

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

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

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

309 concatMap extract [a, b, c]

307 concatMap extract [a, b, c]

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

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

src/Idris/ParseExpr.hs−4

@@ -326,10 +326,6 @@ simpleExpr syn =

326 try (simpleExternalExpr syn)

327 <|> do x <- try (lchar '?' *> (fst <$> name)); return (PMetavar x)

328 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)

329− <|> do fc <- reservedFC "Refl"

330− tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';

331− return t)

332− return (PRefl fc tm)

333 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc (SN $ ElimN t))

329 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc (SN $ ElimN t))

334 <|> proofExpr syn

330 <|> proofExpr syn

335 <|> tacticsExpr syn

331 <|> tacticsExpr syn

src/Idris/ParseOps.hs+1−1

@@ -39,7 +39,7 @@ table fixes

39 toTable (reverse fixes) ++

40 [[backtick],

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

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

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

43 [nofixityoperator]]

44 where

45 flatten :: PTerm -> PTerm -- flatten application

src/Idris/ProofSearch.hs+1−1

@@ -22,7 +22,7 @@ import Debug.Trace

22-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

23

24trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

25−trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)

25+trivial elab ist = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

26 return ())

27 (do env <- get_env

28 g <- goal

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

6

7−instance Foo (=) where

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

8 foo x y prf = prf

9

test/reg047/reg047.idr+1−1

@@ -9,7 +9,7 @@ Id : (A : Type) -> A -> A -> Type

9Id A = (=) {A = A} {B = A}

10

11IdRefl : (A : Type) -> (a : A) -> Id A a a

12−IdRefl A a = Refl {a}

12+IdRefl A a = Refl {x = a}

13

14zzz : Id Nat zero zero

15zzz = IdRefl Nat zero

test/reg047/reg047a.idr+1−1

@@ -9,7 +9,7 @@ Id : (A : Type) -> A -> A -> Type

9Id = \A,x,y => x = y -- {a = A} {b = A}

10

11IdRefl : (A : Type) -> (a : A) -> Id A a a

12−IdRefl A a = Refl {a}

12+IdRefl A a = Refl {x = a}

13

14zzzz : Id MNat zero zero

15zzzz = IdRefl MNat zero

test/reg056/reg056.idr+1−1

@@ -6,7 +6,7 @@ postulate trap : Z = Z

6dodgy : (a, b : ()) -> a = b -> Void

7dodgy n m Refl impossible

8

9−nonk : (trap = Refl {Z}) -> Void

9+nonk : (trap = Refl {x = Z}) -> Void

10nonk Refl impossible

11

12false : Void