da914af · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Consistency of implicit/pattern name binding rules

We've always said that the rules for binding names in patterns are the same as the rules for binding names in implicits, i.e. a name beginning with a lower case letter, not applied to anything, will be bound implicitly, or treated as a pattern variable. This hasn't actually always been quite true, even though it was supposed to be... Correspondingly, added a warning for constructor names which may be unexpectedly bound implicitly. This patch changes the pattern binding rules so that it is the case. Fixes #2653

commitda914af83e36d726ba352fb89f5c15689b675540 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 17 Oct 2015, 18:06 (11 years ago) parenta458e29

31 files changed+220−200

compare with master

unifiedsplit

CHANGELOG+3 docs/tutorial/provisional.rst+12−12 docs/tutorial/typesfuns.rst+2−1 libs/effects/Effect/Random.idr+7−7 src/Idris/AbsSyntax.hs+11−3 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Data.hs+9−1 test/basic002/test006.idr+8−8 test/basic010/Main.idr+13−13 test/basic010/expected+1−1 test/dsl001/test001.idr+10−10 test/dsl002/Resimp.idr+15−15 test/proof003/Parity.idr+6−6 test/proof003/test015.idr+22−22 test/proof005/DefaultArgSubstitutionSuccess.idr+4−4 test/proof006/DefaultArgSubstitutionSyntax.idr+4−4 test/proofsearch002/Process.idr+3−3 test/reg035/reg035a.lidr+5−5 test/reg041/expected+1−1 test/reg041/ott.idr+24−24 test/reg046/reg046.idr+7−7 test/reg047/reg047.idr+2−2 test/reg047/reg047a.idr+3−3 test/totality002/test017.idr+6−6 test/totality004/totality004.idr+7−7 test/totality004/totality004a.idr+7−7 test/totality008/expected+1−1 test/totality008/totality008.idr+4−4 test/tutorial002/tutorial002.idr+15−15 test/tutorial006/expected+1−1 test/tutorial006/tutorial006b.idr+6−6

CHANGELOG+3

@@ -16,6 +16,9 @@ Language updates

1616 valid unbound implicit is now *always* an unbound implicit. This is much

1717 more resilient to changes in inputs, but does require that function names

1818 be explicitly qualified when in argument position.

19+* Name binding in patterns follows the same rule as name binding for implicits

20+ in types: names which begin with lower case letters, not applied to any

21+ arguments, are treated as bound pattern variables.

1922

2023Library updates

2124---------------

docs/tutorial/provisional.rst+12−12

@@ -213,11 +213,11 @@ representation (in this case ``Binary``) with a meaning (in this case

213213.. code-block:: idris

214214

215215 data Binary : Nat -> Type where

216− bEnd : Binary Z

217− bO : Binary n -> Binary (n + n)

218− bI : Binary n -> Binary (S (n + n))

216+ BEnd : Binary Z

217+ BO : Binary n -> Binary (n + n)

218+ BI : Binary n -> Binary (S (n + n))

219219

220−``bO`` and ``bI`` take a binary number as an argument and effectively

220+``BO`` and ``BI`` take a binary number as an argument and effectively

221221shift it one bit left, adding either a zero or one as the new least

222222significant bit. The index, ``n + n`` or ``S (n + n)`` states the result

223223that this left shift then add will have to the meaning of the number.

@@ -234,17 +234,17 @@ original Nat:

234234

235235The ``Parity`` view makes the definition fairly simple — halving the

236236number is effectively a right shift after all — although we need to use

237−a provisional definition in the odd case:

237+a provisional definition in the Odd case:

238238

239239.. code-block:: idris

240240

241241 natToBin : (n:Nat) -> Binary n

242− natToBin Z = bEnd

242+ natToBin Z = BEnd

243243 natToBin (S k) with (parity k)

244− natToBin (S (j + j)) | even = bI (natToBin j)

245− natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))

244+ natToBin (S (j + j)) | Even = BI (natToBin j)

245+ natToBin (S (S (j + j))) | Odd ?= BO (natToBin (S j))

246246

247−The problem with the odd case is the same as in the definition of

247+The problem with the Odd case is the same as in the definition of

248248``parity``, and the proof proceeds in the same way:

249249

250250.. code-block:: idris

@@ -272,6 +272,6 @@ For this to work, of course, we need a ``Show`` instance for

272272.. code-block:: idris

273273

274274 instance Show (Binary n) where

275− show (bO x) = show x ++ "0"

276− show (bI x) = show x ++ "1"

277− show bEnd = ""

275+ show (BO x) = show x ++ "0"

276+ show (BI x) = show x ++ "1"

277+ show BEnd = ""

docs/tutorial/typesfuns.rst+2−1

@@ -445,7 +445,8 @@ are not given in applications of ``index``; their values can be

445445inferred from the types of the ``Fin n`` and ``Vect n a``

446446arguments. Any name beginning with a lower case letter which appears

447447as a parameter or index in a

448−type declaration, but which is otherwise unbound, will be automatically

448+type declaration, which is not applied to any arguments, will

449+*always* be automatically

449450bound as an implicit argument. Implicit arguments can still be given

450451explicitly in applications, using ``{a=value}`` and ``{n=value}``, for

451452example:

libs/effects/Effect/Random.idr+7−7

@@ -4,28 +4,28 @@ import Effects

44import Data.Vect

66data Random : Effect where

7− getRandom : sig Random Integer Integer

8− setSeed : Integer -> sig Random () Integer

7+ GetRandom : sig Random Integer Integer

8+ SetSeed : Integer -> sig Random () Integer

1010instance Handler Random m where

11− handle seed getRandom k

11+ handle seed GetRandom k

1212 = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in

1313 k seed' seed'

14− handle seed (setSeed n) k = k () n

14+ handle seed (SetSeed n) k = k () n

1515

1616RND : EFFECT

1717RND = MkEff Integer Random

1818

1919||| Generates a random Integer in a given range

2020rndInt : Integer -> Integer -> Eff Integer [RND]

21−rndInt lower upper = do v <- call $ getRandom

21+rndInt lower upper = do v <- call $ GetRandom

2222 return ((v `prim__sremBigInt` (upper - lower)) + lower)

2323

2424||| Generate a random number in Fin (S `k`)

2525|||

2626||| Note that rndFin k takes values 0, 1, ..., k.

2727rndFin : (k : Nat) -> Eff (Fin (S k)) [RND]

28−rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))

28+rndFin k = do let v = assert_total $ !(call GetRandom) `prim__sremBigInt` (cast (S k))

2929 return (toFin v)

3030 where toFin : Integer -> Fin (S k)

3131 toFin x = case integerToFin x (S k) of

@@ -43,5 +43,5 @@ rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

4343

4444||| Sets the random seed

4545srand : Integer -> Eff () [RND]

46−srand n = call $ setSeed n

46+srand n = call $ SetSeed n

4747

src/Idris/AbsSyntax.hs+11−3

@@ -1694,7 +1694,9 @@ aiFn :: Name -> Bool -> Bool -> Bool

16941694 -> [PArg] -- ^ initial arguments (if in an expression)

16951695 -> Either Err PTerm

16961696aiFn topname inpat True qq imp_meths ist fc f ffc ds [] _

1697− = case lookupDef f (tt_ctxt ist) of

1697+ | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f

1698+ | otherwise

1699+ = case lookupDef f (tt_ctxt ist) of

16981700 [] -> Right $ PPatvar ffc f

16991701 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

17001702 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $

@@ -1707,6 +1709,10 @@ aiFn topname inpat True qq imp_meths ist fc f ffc ds [] _

17071709 imp _ = True

17081710-- allImp [] = False

17091711 allImp xs = all imp xs

1712+

1713+ unqualified (NS _ _) = False

1714+ unqualified _ = True

1715+

17101716 constructor (TyDecl (DCon _ _ _) _) = True

17111717 constructor _ = False

17121718

@@ -1887,9 +1893,11 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

18871893 su tm@(PRef fc hl f)

18881894 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)

18891895 = Placeholder

1890− | (TType _ : _) <- lookupTy f (tt_ctxt i)

1896+ | (TType _ : _) <- lookupTy f (tt_ctxt i),

1897+ not (implicitable f)

18911898 = PHidden tm

1892− | (UType _ : _) <- lookupTy f (tt_ctxt i)

1899+ | (UType _ : _) <- lookupTy f (tt_ctxt i),

1900+ not (implicitable f)

18931901 = PHidden tm

18941902 su (PApp fc f@(PRef _ _ fn) args)

18951903 -- here we use canBeDConName because the impossible pattern

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

@@ -501,7 +501,7 @@ propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)

501501 | Placeholder <- getTm t,

502502 n `elem` ps,

503503 not (n `elem` bound)

504− = t { getTm = PRef NoFC [] n } : addP sc ts

504+ = t { getTm = PPatvar NoFC n } : addP sc ts

505505 addP (Bind n _ sc) (t : ts) = t : addP sc ts

506506 addP _ ts = ts

507507propagateParams i ps t bound (PApp fc ap args)

src/Idris/Elab/Data.hs+9−1

@@ -48,13 +48,19 @@ import qualified Data.Text as T

4848import Data.Char(isLetter, toLower)

4949import Data.List.Split (splitOn)

5050

51−import Util.Pretty(pretty, text)

51+import Util.Pretty

52+

53+warnLC :: FC -> Name -> Idris ()

54+warnLC fc n

55+ = iWarn fc $ annName n <+> text "has a name which may be implicitly bound."

56+ <> line <> text "This is likely to lead to problems!"

5257

5358elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()

5459elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)

5560 = do let codata = Codata `elem` opts

5661 logLvl 1 (show (fc, doc))

5762 checkUndefined fc n

63+ when (implicitable n) $ warnLC fc n

5864 (cty, _, t, inacc) <- buildType info syn fc [] n t_in

5965

6066 addIBC (IBCDef n)

@@ -65,6 +71,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

6571 = do let codata = Codata `elem` opts

6672 logLvl 1 (show fc)

6773 undef <- isUndefined fc n

74+ when (implicitable n) $ warnLC fc n

6875 (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in

6976 -- if n is defined already, make sure it is just a type declaration

7077 -- with the same type we've just elaborated, and no constructors

@@ -224,6 +231,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

224231 Idris (Name, Type)

225232elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcenames)

226233 = do checkUndefined fc n

234+ when (implicitable n) $ warnLC fc n

227235 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

228236 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

229237 ctxt <- getContext

test/basic002/test006.idr+8−8

@@ -1,21 +1,21 @@

11module Main

33data Parity : Nat -> Type where

4− even : {n : Nat} -> Parity (n + n)

5− odd : {n : Nat} -> Parity (S (n + n))

4+ Even : {n : Nat} -> Parity (n + n)

5+ Odd : {n : Nat} -> Parity (S (n + n))

77parity : (n:Nat) -> Parity n

8−parity Z = even {n=Z}

9−parity (S Z) = odd {n=Z}

8+parity Z = Even {n=Z}

9+parity (S Z) = Odd {n=Z}

1010parity (S (S k)) with (parity k)

11− parity (S (S (j + j))) | (even {n = j}) ?= even {n=S j}

12− parity (S (S (S (j + j)))) | (odd {n = j}) ?= odd {n=S j}

11+ parity (S (S (j + j))) | (Even {n = j}) ?= Even {n=S j}

12+ parity (S (S (S (j + j)))) | (Odd {n = j}) ?= Odd {n=S j}

1313

1414natToBin : Nat -> List Bool

1515natToBin Z = Nil

1616natToBin k with (parity k)

17− natToBin (j + j) | even {n = j} = False :: natToBin j

18− natToBin (S (j + j)) | odd {n = j} = True :: natToBin j

17+ natToBin (j + j) | Even {n = j} = False :: natToBin j

18+ natToBin (S (j + j)) | Odd {n = j} = True :: natToBin j

1919

2020main : IO ()

2121main = do printLn (natToBin 42)

test/basic010/Main.idr+13−13

@@ -9,32 +9,32 @@ qib (S Z) = 2

99qib (S (S n)) = qib n * qib (S n)

1010

1111-- An equality whose size reflects the size of numbers.

12−data equals : Nat -> Nat -> Type where

13− eqZ : Z `equals` Z

14− eqS : m `equals` n -> S m `equals` S n

12+data Equals : Nat -> Nat -> Type where

13+ EqZ : Z `Equals` Z

14+ EqS : m `Equals` n -> S m `Equals` S n

1515

16−eq_refl : {n : Nat} -> n `equals` n

17−eq_refl {n = Z} = eqZ

18−eq_refl {n = S n} = eqS eq_refl

16+eq_refl : {n : Nat} -> n `Equals` n

17+eq_refl {n = Z} = EqZ

18+eq_refl {n = S n} = EqS eq_refl

1919

2020-- Here, the proof is very expensive to compute.

2121-- We add a recursive argument to prevent Idris from inlining the function.

22−f : (r, n : Nat) -> Subset Nat (\k => qib n `equals` qib k)

22+f : (r, n : Nat) -> Subset Nat (\k => qib n `Equals` qib k)

2323f Z n = Element n eq_refl

2424f (S r) n = f r n

2525

2626-- A (contrived) relation, just to have something to show.

27−data represents : Nat -> Nat -> Type where

28− axiom : (n : Nat) -> qib n `represents` n

27+data Represents : Nat -> Nat -> Type where

28+ Axiom : (n : Nat) -> qib n `Represents` n

2929

3030-- Here, the witness is very expensive to compute.

3131-- We add a recursive argument to prevent Idris from inlining the function.

32−g : (r, n : Nat) -> Exists (\k : Nat => k `represents` n)

33−g Z n = Evidence (qib n) (axiom n)

32+g : (r, n : Nat) -> Exists (\k : Nat => k `Represents` n)

33+g Z n = Evidence (qib n) (Axiom n)

3434g (S r) n = g r n

3535

36−fmt : qib n `represents` n -> String

37−fmt (axiom n) = "axiom " ++ show n

36+fmt : qib n `Represents` n -> String

37+fmt (Axiom n) = "Axiom " ++ show n

3838

3939main : IO ()

4040main = do

test/basic010/expected+1−1

@@ -1,3 +1,3 @@

11*oink*

2210000

3−axiom 10000

3+Axiom 10000

test/dsl001/test001.idr+10−10

@@ -17,13 +17,13 @@ using (G : Vect n Ty)

1717 (::) : interpTy a -> Env G -> Env (a :: G)

1818

1919 data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

20− stop : HasType FZ (t :: G) t

21− pop : HasType k G t -> HasType (FS k) (u :: G) t

20+ Stop : HasType FZ (t :: G) t

21+ Pop : HasType k G t -> HasType (FS k) (u :: G) t

2222

2323 lookup : HasType i G t -> Env G -> interpTy t

24− lookup stop (x :: xs) = x

25− lookup (pop k) (x :: xs) = lookup k xs

26− lookup stop [] impossible

24+ lookup Stop (x :: xs) = x

25+ lookup (Pop k) (x :: xs) = lookup k xs

26+ lookup Stop [] impossible

2727

2828 data Expr : Vect n Ty -> Ty -> Type where

2929 Var : HasType i G t -> Expr G t

@@ -41,8 +41,8 @@ using (G : Vect n Ty)

4141 dsl expr

4242 lambda = lam_

4343 variable = Var

44− index_first = stop

45− index_next = pop

44+ index_first = Stop

45+ index_next = Pop

4646

4747 total

4848 interp : Env G -> [static] (e : Expr G t) -> interpTy t

@@ -67,7 +67,7 @@ using (G : Vect n Ty)

6767-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var FZ) (Var (FS FZ))))) (Var FZ)) (Var FZ))

6868

6969 eDouble : Expr G (TyFun TyInt TyInt)

70− eDouble = expr (\x => App (App eAdd x) (Var stop))

70+ eDouble = expr (\x => App (App eAdd x) (Var Stop))

7171

7272-- app : Lazy (Expr G (TyFun a t)) -> Expr G a -> Expr G t

7373-- app = \f, a => App (Force f) a

@@ -81,8 +81,8 @@ using (G : Vect n Ty)

8181

8282 eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt))

8383 eProg = Lam (Lam

84− (Bind (App eDouble (Var (pop stop)))

85− (\x => Bind (App eDouble (Var stop))

84+ (Bind (App eDouble (Var (Pop Stop)))

85+ (\x => Bind (App eDouble (Var Stop))

8686 (\y => Bind (App eDouble (Val x))

8787 (\z => App (App eAdd (Val y)) (Val z))))))

8888

test/dsl002/Resimp.idr+15−15

@@ -49,35 +49,35 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

4949 interpTy (a :-> b) = a -> interpTy b

5050

5151 data HasType : Vect n Ty -> Fin n -> Ty -> Type where

52− stop : HasType (a :: gam) FZ a

53− pop : HasType gam i b -> HasType (a :: gam) (FS i) b

52+ Stop : HasType (a :: gam) FZ a

53+ Pop : HasType gam i b -> HasType (a :: gam) (FS i) b

5454

5555 data Env : Vect n Ty -> Type where

5656 Nil : Env Nil

5757 (::) : interpTy a -> Env gam -> Env (a :: gam)

5858

5959 envLookup : HasType gam i a -> Env gam -> interpTy a

60− envLookup stop (x :: xs) = x

61− envLookup (pop k) (x :: xs) = envLookup k xs

60+ envLookup Stop (x :: xs) = x

61+ envLookup (Pop k) (x :: xs) = envLookup k xs

6262

6363 update : (gam : Vect n Ty) -> HasType gam i b -> Ty -> Vect n Ty

64− update (x :: xs) stop y = y :: xs

65− update (x :: xs) (pop k) y = x :: update xs k y

66− update Nil stop _ impossible

64+ update (x :: xs) Stop y = y :: xs

65+ update (x :: xs) (Pop k) y = x :: update xs k y

66+ update Nil Stop _ impossible

6767

6868 total

6969 envUpdate : (p:HasType gam i a) -> (val:interpTy b) ->

7070 Env gam -> Env (update gam p b)

71− envUpdate stop val (x :: xs) = val :: xs

72− envUpdate (pop k) val (x :: xs) = x :: envUpdate k val xs

73− envUpdate stop _ Nil impossible

71+ envUpdate Stop val (x :: xs) = val :: xs

72+ envUpdate (Pop k) val (x :: xs) = x :: envUpdate k val xs

73+ envUpdate Stop _ Nil impossible

7474

7575 total

7676 envUpdateVal : (p:HasType gam i a) -> (val:b) ->

7777 Env gam -> Env (update gam p (Val b))

78− envUpdateVal stop val (x :: xs) = val :: xs

79− envUpdateVal (pop k) val (x :: xs) = x :: envUpdateVal k val xs

80− envUpdateVal stop _ Nil impossible

78+ envUpdateVal Stop val (x :: xs) = val :: xs

79+ envUpdateVal (Pop k) val (x :: xs) = x :: envUpdateVal k val xs

80+ envUpdateVal Stop _ Nil impossible

8181

8282 envTail : Env (a :: gam) -> Env gam

8383 envTail (x :: xs) = xs

@@ -169,8 +169,8 @@ syntax run [prog] = interp [] prog (\env, res => res)

169169dsl res

170170 variable = id

171171 let = let_

172− index_first = stop

173− index_next = pop

172+ index_first = Stop

173+ index_next = Pop

174174

175175syntax RES [x] = {gam:Vect n Ty} -> Res gam gam (R x)

176176

test/proof003/Parity.idr+6−6

@@ -1,15 +1,15 @@

11module Parity

33data Parity : Nat -> Type where

4− even : {n : Nat} -> Parity (n + n)

5− odd : {n : Nat} -> Parity (S (n + n))

4+ Even : {n : Nat} -> Parity (n + n)

5+ Odd : {n : Nat} -> Parity (S (n + n))

77parity : (n:Nat) -> Parity n

8−parity Z = even {n=Z}

9−parity (S Z) = odd {n=Z}

8+parity Z = Even {n=Z}

9+parity (S Z) = Odd {n=Z}

1010parity (S (S k)) with (parity k)

11− parity (S (S (j + j))) | even ?= even {n=S j}

12− parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

11+ parity (S (S (j + j))) | Even ?= Even {n=S j}

12+ parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}

1313

1414

1515parity_lemma_2 = proof {

test/proof003/test015.idr+22−22

@@ -4,41 +4,41 @@ import Parity

44import System

66data Bit : Nat -> Type where

7− b0 : Bit Z

8− b1 : Bit (S Z)

7+ B0 : Bit Z

8+ B1 : Bit (S Z)

1010instance Show (Bit n) where

1111 show = show' where

1212 show' : Bit x -> String

13− show' b0 = "0"

14− show' b1 = "1"

13+ show' B0 = "0"

14+ show' B1 = "1"

1515

1616infixl 5 #

1717

1818data Binary : (width : Nat) -> (value : Nat) -> Type where

19− zero : Binary Z Z

19+ Zero : Binary Z Z

2020 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)

2121

2222instance Show (Binary w k) where

23− show zero = ""

23+ show Zero = ""

2424 show (bin # bit) = show bin ++ show bit

2525

2626pad : Binary w n -> Binary (S w) n

27−pad zero = zero # b0

27+pad Zero = Zero # B0

2828pad (num # x) = pad num # x

2929

3030natToBin : (width : Nat) -> (n : Nat) ->

3131 Maybe (Binary width n)

3232natToBin Z (S k) = Nothing

33−natToBin Z Z = Just zero

33+natToBin Z Z = Just Zero

3434natToBin (S k) Z = do x <- natToBin k Z

3535 Just (pad x)

3636natToBin (S w) (S k) with (parity k)

37− natToBin (S w) (S (plus j j)) | even = do jbin <- natToBin w j

38− let value = jbin # b1

37+ natToBin (S w) (S (plus j j)) | Even = do jbin <- natToBin w j

38+ let value = jbin # B1

3939 ?ntbEven

40− natToBin (S w) (S (S (plus j j))) | odd = do jbin <- natToBin w (S j)

41− let value = jbin # b0

40+ natToBin (S w) (S (S (plus j j))) | Odd = do jbin <- natToBin w (S j)

41+ let value = jbin # B0

4242 ?ntbOdd

4343

4444testBin : Maybe (Binary 8 42)

@@ -49,17 +49,17 @@ term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, Refl)))

4949

5050addBit : Bit x -> Bit y -> Bit c ->

5151 (bX ** (bY ** (Bit bX, Bit bY, c + x + y = bY + 2 * bX)))

52−addBit b0 b0 b0 = bitpair b0 b0

53−addBit b0 b0 b1 = bitpair b0 b1

54−addBit b0 b1 b0 = bitpair b0 b1

55−addBit b0 b1 b1 = bitpair b1 b0

56−addBit b1 b0 b0 = bitpair b0 b1

57−addBit b1 b0 b1 = bitpair b1 b0

58−addBit b1 b1 b0 = bitpair b1 b0

59−addBit b1 b1 b1 = bitpair b1 b1

52+addBit B0 B0 B0 = bitpair B0 B0

53+addBit B0 B0 B1 = bitpair B0 B1

54+addBit B0 B1 B0 = bitpair B0 B1

55+addBit B0 B1 B1 = bitpair B1 B0

56+addBit B1 B0 B0 = bitpair B0 B1

57+addBit B1 B0 B1 = bitpair B1 B0

58+addBit B1 B1 B0 = bitpair B1 B0

59+addBit B1 B1 B1 = bitpair B1 B1

6060

6161adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)

62−adc zero zero carry ?= zero # carry

62+adc Zero Zero carry ?= Zero # carry

6363adc (numx # bX) (numy # bY) carry

6464 ?= let (bitpair carry0 lsb) = addBit bX bY carry in

6565 adc numx numy carry0 # lsb

@@ -75,7 +75,7 @@ main = do let Just bin1 = natToBin 8 42

7575 printLn bin1

7676 let Just bin2 = natToBin 8 89

7777 printLn bin2

78− printLn (adc bin1 bin2 b0)

78+ printLn (adc bin1 bin2 B0)

7979

8080

8181

test/proof005/DefaultArgSubstitutionSuccess.idr+4−4

@@ -23,11 +23,11 @@ argsAreDiff _ _ = ()

2323

2424

2525data SameNats : Type where

26− same : (n:Nat) -> (m:Nat) ->

26+ Same : (n:Nat) -> (m:Nat) ->

2727 { default (decProof (decEq m n)) same : (m=n) } -> SameNats

2828

2929data DiffNats : Type where

30− diff : (n:Nat) -> (m:Nat) ->

30+ Diff : (n:Nat) -> (m:Nat) ->

3131 { default (decProof (decEq m n)) same : (m=n) -> Void } -> DiffNats

3232

3333

@@ -38,7 +38,7 @@ zszArgsAreDiff : ()

3838zszArgsAreDiff = argsAreDiff Z (S Z)

3939

4040sameNatZs : SameNats

41−sameNatZs = same Z Z

41+sameNatZs = Same Z Z

4242

4343diffNatsZSZ : DiffNats

44−diffNatsZSZ = diff Z (S Z)

44+diffNatsZSZ = Diff Z (S Z)

test/proof006/DefaultArgSubstitutionSyntax.idr+4−4

@@ -30,10 +30,10 @@ argsAreDiff _ _ = ()

3030

3131

3232data SameNats : Type where

33− same : (n:Nat) -> (m:Nat) -> {{ same : accept (decEq m n) }} -> SameNats

33+ Same : (n:Nat) -> (m:Nat) -> {{ same : accept (decEq m n) }} -> SameNats

3434

3535data DiffNats : Type where

36− diff : (n:Nat) -> (m:Nat) -> {{ diff : reject (decEq m n) }} -> DiffNats

36+ Diff : (n:Nat) -> (m:Nat) -> {{ diff : reject (decEq m n) }} -> DiffNats

3737

3838

3939zArgsAreSame : ()

@@ -43,7 +43,7 @@ zszArgsAreDiff : ()

4343zszArgsAreDiff = argsAreDiff Z (S Z)

4444

4545sameNatZs : SameNats

46−sameNatZs = same Z Z

46+sameNatZs = Same Z Z

4747

4848diffNatsZSZ : DiffNats

49−diffNatsZSZ = diff Z (S Z)

49+diffNatsZSZ = Diff Z (S Z)

test/proofsearch002/Process.idr+3−3

@@ -119,7 +119,7 @@ mutual

119119 Pure : a -> Process a iface hs (const hs) p (const p)

120120 Quit : a -> Process a iface hs (const hs) p (const (resetReplied p))

121121

122− bind : Process a iface hs hs' p p' ->

122+ Bind : Process a iface hs hs' p p' ->

123123 ((x : a) -> Process b iface (hs' x) hs'' (p' x) p'') ->

124124 Process b iface hs hs'' p p''

125125

@@ -207,7 +207,7 @@ Lift = Lift'

207207(>>=) : Process a iface hs hs' p p' ->

208208 ((x : a) -> Process b iface (hs' x) hs'' (p' x) p'') ->

209209 Process b iface hs hs'' p p''

210−(>>=) = bind

210+(>>=) = Bind

211211

212212TrySend : (proc : ProcID iface) -> iface ty ->

213213 Process (Maybe ty) iface'

@@ -371,7 +371,7 @@ eval st (Lift' x) k = do x' <- x

371371 k x' st

372372eval st (Pure x) k = k x st

373373eval st (Quit x) k = k x st

374−eval st (bind x f) k = eval st x (\x', st' => eval st' (f x') k)

374+eval st (Bind x f) k = eval st x (\x', st' => eval st' (f x') k)

375375

376376eval st (Fork proc) k

377377 = do ptr <- fork (eval (MkEvalState [] [] 1 0) proc (\_, _ => pure ()))

test/reg035/reg035a.lidr+5−5

@@ -28,26 +28,26 @@

2828> )

2929

3030> data Set : Type -> Type where

31−> setify : (as : List a) -> Set a

31+> Setify : (as : List a) -> Set a

3232

3333> instance (Eq a) => Eq (Set a) where

34−> (==) (setify as) (setify bs) = setEq as bs

34+> (==) (Setify as) (Setify bs) = setEq as bs

3535

3636> postulate reflexive_Set_eqeq : (Eq a) =>

3737> (as : Set a) ->

3838> So (as == as)

3939

4040> unwrap : Set a -> List a

41−> unwrap (setify as) = as

41+> unwrap (Setify as) = as

4242

4343> union : Set (Set a) -> Set a

44−> union (setify ss) = setify (concat (map unwrap ss))

44+> union (Setify ss) = Setify (concat (map unwrap ss))

4545

4646> listify : (Eq a) => Set a -> List a

4747> listify = nub . unwrap

4848

4949> arePairwiseDisjoint : (Eq a) => Set (Set a) -> Bool

50−> arePairwiseDisjoint (setify ss) =

50+> arePairwiseDisjoint (Setify ss) =

5151> hasNoDuplicates (concat (map listify ss))

5252

5353> isPartition : (Eq a) => Set (Set a) -> Set a -> Bool

test/reg041/expected+1−1

@@ -1,2 +1,2 @@

1−?prf : (x : Bool) -> (x1 : Bool) -> El (EQ two x two x1) -> El (EQ two x two x1)

1+?prf : (x : Bool) -> (x1 : Bool) -> El (EQ Two x Two x1) -> El (EQ Two x Two x1)

22Z

test/reg041/ott.idr+24−24

@@ -3,40 +3,40 @@ module OTT

33mutual

55 data U : Type where

6− u : U

7− zero : U

8− one : U

9− two : U

10− pi : (s : U) -> (t : El s -> U) -> U

6+ MkU : U

7+ Zero : U

8+ One : U

9+ Two : U

10+ Pi : (s : U) -> (t : El s -> U) -> U

1111

1212 El : U -> Type

13− El u = U

14− El zero = Void

15− El one = ()

16− El two = Bool

17− El (pi s t) = (x : El s) -> El (t x)

13+ El MkU = U

14+ El Zero = Void

15+ El One = ()

16+ El Two = Bool

17+ El (Pi s t) = (x : El s) -> El (t x)

1818

1919infixr 10 ~>

2020(~>) : U -> U -> U

21−s ~> t = pi s $ const t

21+s ~> t = Pi s $ const t

2222

2323syntax "<|" [s] "|>" = El s

2424syntax [x] "==" [y] "in" [s] = EQ s x s y

2525

2626%assert_total

2727EQ : (s : U) -> <| s |> -> (t : U) -> <| t |> -> U

28−EQ u u u u = one

29−EQ u zero u zero = one

30−EQ u one u one = one

31−EQ u two u two = one

32−EQ u (pi s t) u (pi s' t') = pi s $ \x => pi s' $ \y => EQ s x s' y ~> EQ u (t x) u (t' y)

33−EQ zero x zero y = one

34−EQ one x one y = one

35−EQ two True two True = one

36−EQ two False two False = one

37−EQ (pi s t) f (pi s' t') g = pi s $ \x => pi s' $ \y => EQ s x s' y ~> EQ (t x) (f x) (t' y) (g y)

38−EQ _ _ _ _ = zero

39−

40−example : <| (Basics.id == Basics.id in (OTT.two ~> OTT.two)) |>

28+EQ MkU MkU MkU MkU = One

29+EQ MkU Zero MkU Zero = One

30+EQ MkU One MkU One = One

31+EQ MkU Two MkU Two = One

32+EQ MkU (Pi s t) MkU (Pi s' t') = Pi s $ \x => Pi s' $ \y => EQ s x s' y ~> EQ MkU (t x) MkU (t' y)

33+EQ Zero x Zero y = One

34+EQ One x One y = One

35+EQ Two True Two True = One

36+EQ Two False Two False = One

37+EQ (Pi s t) f (Pi s' t') g = Pi s $ \x => Pi s' $ \y => EQ s x s' y ~> EQ (t x) (f x) (t' y) (g y)

38+EQ _ _ _ _ = Zero

39+

40+example : <| (Basics.id == Basics.id in (OTT.Two ~> OTT.Two)) |>

4141example = ?prf

4242

test/reg046/reg046.idr+7−7

@@ -1,19 +1,19 @@

11module test

33data MyList : (A : Type) -> Type where

4− nil : (A : Type) -> MyList A

5− cons : (A : Type) -> A -> MyList A -> MyList A

4+ MyNil : (A : Type) -> MyList A

5+ MyCons : (A : Type) -> A -> MyList A -> MyList A

77elimList : (A : Type) ->

88 (m : MyList A -> Type) ->

9− (f1 : m (nil A)) ->

10− (f2 : (a : A) -> (as : MyList A) -> m as -> m (cons A a as)) ->

9+ (f1 : m (MyNil A)) ->

10+ (f2 : (a : A) -> (as : MyList A) -> m as -> m (MyCons A a as)) ->

1111 (e : MyList A) ->

1212 m e

13−elimList A m f1 f2 (nil A) = f1

14−elimList A m f1 f2 (cons A a as) = f2 a as (elimList A m f1 f2 as)

13+elimList A m f1 f2 (MyNil A) = f1

14+elimList A m f1 f2 (MyCons A a as) = f2 a as (elimList A m f1 f2 as)

1515

1616append : (A : Type) -> (b : MyList A) -> (c : MyList A) -> MyList A

1717append A b c = (elimList A (\ d => MyList A) c

18− (\ d => \ e => \ f => cons A d f)

18+ (\ d => \ e => \ f => MyCons A d f)

1919 b)

test/reg047/reg047.idr+2−2

@@ -1,7 +1,7 @@

11module test

33data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

4− sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B

4+ Sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B

66data Nat = Zero | Succ Nat

@@ -15,4 +15,4 @@ zzz : Id Nat Zero Zero

1515zzz = IdRefl Nat Zero

1616

1717eep : TTSigma Nat (\ a => Id Nat a Zero)

18−eep = sigma Nat (\ a => Id Nat a Zero) Zero zzz

18+eep = Sigma Nat (\ a => Id Nat a Zero) Zero zzz

test/reg047/reg047a.idr+3−3

@@ -1,7 +1,7 @@

11module test

33data TTSigma : (A : Type) -> (B : A -> Type) -> Type where

4− sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B

4+ Sigma : (A : Type) -> (B : A -> Type) -> (a : A) -> B a -> TTSigma A B

66data MNat = Zero | Succ MNat

@@ -15,10 +15,10 @@ zzzz : Id MNat Zero Zero

1515zzzz = IdRefl MNat Zero

1616

1717eep : TTSigma MNat (\ c => Id MNat c Zero)

18−eep = (sigma MNat (\b => Id MNat b Zero) Zero zzzz)

18+eep = (Sigma MNat (\b => Id MNat b Zero) Zero zzzz)

1919

2020eep2 : TTSigma MNat (\ c => Id MNat c Zero)

21−eep2 = (sigma MNat (\b => Id MNat b Zero) Zero (IdRefl MNat Zero))

21+eep2 = (Sigma MNat (\b => Id MNat b Zero) Zero (IdRefl MNat Zero))

2222

2323

2424

test/totality002/test017.idr+6−6

@@ -62,14 +62,14 @@ ack Z n = S n

6262ack (S m) Z = ack m (S Z)

6363ack (S m) (S n) = ack m (ack (S m) n)

6464

65−data Bin = eps | c0 Bin | c1 Bin

65+data Bin = EPS | C0 Bin | C1 Bin

6666

6767foo : Bin -> Nat

68−foo eps = Z

69−foo (c0 eps) = Z

70−foo (c0 (c1 x)) = S (foo (c1 x))

71−foo (c0 (c0 x)) = foo (c0 x)

72−foo (c1 x) = S (foo x)

68+foo EPS = Z

69+foo (C0 EPS) = Z

70+foo (C0 (C1 x)) = S (foo (C1 x))

71+foo (C0 (C0 x)) = foo (C0 x)

72+foo (C1 x) = S (foo x)

7373

7474bar : Nat -> Nat -> Nat

7575bar x y = mp x y where

test/totality004/totality004.idr+7−7

@@ -3,19 +3,19 @@ module Main

33%default total

55data SP : Type -> Type -> Type where

6− get : (a -> SP a b) -> SP a b

7− put : b -> Inf (SP a b) -> SP a b

6+ Get : (a -> SP a b) -> SP a b

7+ Put : b -> Inf (SP a b) -> SP a b

99copy : SP a a

10−copy = get (\x => put x copy)

10+copy = Get (\x => Put x copy)

1111

1212process : SP a b -> Stream a -> Stream b

13−process (get f) (x :: xs) = process (f x) xs

14−process (put b sp) xs = b :: process sp xs

13+process (Get f) (x :: xs) = process (f x) xs

14+process (Put b sp) xs = b :: process sp xs

1515

1616doubleInt : SP Nat Int

17−doubleInt = get (\x => put (the Int (cast x))

18− (put (the Int (cast x) * 2) doubleInt))

17+doubleInt = Get (\x => Put (the Int (cast x))

18+ (Put (the Int (cast x) * 2) doubleInt))

1919

2020countStream : Nat -> Stream Nat

2121countStream x = x :: countStream (x + 1)

test/totality004/totality004a.idr+7−7

@@ -3,19 +3,19 @@ module Main

33%default total

55data SP : Type -> Type -> Type where

6− get : (a -> SP a b) -> SP a b

7− put : b -> Inf (SP a b) -> SP a b

6+ Get : (a -> SP a b) -> SP a b

7+ Put : b -> Inf (SP a b) -> SP a b

99copy : SP a a

10−copy = get (\x => put x copy)

10+copy = Get (\x => Put x copy)

1111

1212process : SP a b -> Stream a -> Stream b

13−process (get f) (x :: xs) = process (f x) xs

14−process (put b sp) xs = process sp xs

13+process (Get f) (x :: xs) = process (f x) xs

14+process (Put b sp) xs = process sp xs

1515

1616doubleInt : SP Nat Int

17−doubleInt = get (\x => put (the Int (cast x))

18− (put (the Int (cast x) * 2) doubleInt))

17+doubleInt = Get (\x => Put (the Int (cast x))

18+ (Put (the Int (cast x) * 2) doubleInt))

1919

2020countStream : Nat -> Stream Nat

2121countStream x = x :: countStream (x + 1)

test/totality008/expected+1−1

@@ -1,2 +1,2 @@

11totality008.idr:7:1:

2−Main.ElimT is possibly not total due to: Main.c2

2+Main.ElimT is possibly not total due to: Main.C2

test/totality008/totality008.idr+4−4

@@ -1,8 +1,8 @@

11 data T : Type -> Type where

2− c1 : T Nat

3− c2 : T (T Nat)

2+ C1 : T Nat

3+ C2 : T (T Nat)

55total

66ElimT : (A : Type) -> T A -> A

7−ElimT _ c1 = 3

8−ElimT _ c2 = c1

7+ElimT _ C1 = 3

8+ElimT _ C2 = C1

test/tutorial002/tutorial002.idr+15−15

@@ -1,31 +1,31 @@

11module Main

33data Binary : Nat -> Type where

4− bEnd : Binary Z

5− bO : Binary n -> Binary (n + n)

6− bI : Binary n -> Binary (S (n + n))

4+ BEnd : Binary Z

5+ BO : Binary n -> Binary (n + n)

6+ BI : Binary n -> Binary (S (n + n))

88instance Show (Binary n) where

9− show (bO x) = show x ++ "0"

10− show (bI x) = show x ++ "1"

11− show bEnd = ""

9+ show (BO x) = show x ++ "0"

10+ show (BI x) = show x ++ "1"

11+ show BEnd = ""

1212

1313data Parity : Nat -> Type where

14− even : Parity (n + n)

15− odd : Parity (S (n + n))

14+ Even : Parity (n + n)

15+ Odd : Parity (S (n + n))

1616

1717parity : (n:Nat) -> Parity n

18−parity Z = even {n=Z}

19−parity (S Z) = odd {n=Z}

18+parity Z = Even {n=Z}

19+parity (S Z) = Odd {n=Z}

2020parity (S (S k)) with (parity k)

21− parity (S (S (j + j))) | even ?= even {n=S j}

22− parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

21+ parity (S (S (j + j))) | Even ?= Even {n=S j}

22+ parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}

2323

2424natToBin : (n:Nat) -> Binary n

25−natToBin Z = bEnd

25+natToBin Z = BEnd

2626natToBin (S k) with (parity k)

27− natToBin (S (j + j)) | even = bI (natToBin j)

28− natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))

27+ natToBin (S (j + j)) | Even = BI (natToBin j)

28+ natToBin (S (S (j + j))) | Odd ?= BO (natToBin (S j))

2929

3030intToNat : Int -> Nat

3131intToNat 0 = Z

test/tutorial006/expected+1−1

@@ -18,7 +18,7 @@ When checking right hand side of with block in Main.parity with expected type

1818 Parity (S (S (j + j)))

1919

2020Type mismatch between

21− Parity (plus (S j) (S j)) (Type of even)

21+ Parity (plus (S j) (S j)) (Type of Even)

2222and

2323 Parity (S (S (plus j j))) (Expected type)

2424

test/tutorial006/tutorial006b.idr+6−6

@@ -1,12 +1,12 @@

22data Parity : Nat -> Type where

3− even : Parity (n + n)

4− odd : Parity (S (n + n))

3+ Even : Parity (n + n)

4+ Odd : Parity (S (n + n))

66parity : (n:Nat) -> Parity n

7−parity Z = even {n=Z}

8−parity (S Z) = odd {n=Z}

7+parity Z = Even {n=Z}

8+parity (S Z) = Odd {n=Z}

99parity (S (S k)) with (parity k)

10− parity (S (S (j + j))) | even = even {n=S j}

11− parity (S (S (S (j + j)))) | odd = odd {n=S j}

10+ parity (S (S (j + j))) | Even = Even {n=S j}

11+ parity (S (S (S (j + j)))) | Odd = Odd {n=S j}

1212