da914af · Idris-dev · git.iko.soy

CHANGELOG+3

compare with master

unifiedsplit

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

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

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

18 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.

19

22

20Library updates

23Library updates

21---------------

24---------------

docs/tutorial/provisional.rst+12−12

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

213.. code-block:: idris

214

215 data Binary : Nat -> Type where

216− bEnd : Binary Z

216+ BEnd : Binary Z

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

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

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

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

219

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

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

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

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

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

234

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

236number 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:

238

239.. code-block:: idris

240

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

242− natToBin Z = bEnd

242+ natToBin Z = BEnd

243 natToBin (S k) with (parity k)

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

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

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

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

246

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

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

249

250.. code-block:: idris

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

272.. code-block:: idris

273

274 instance Show (Binary n) where

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

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

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

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

277− show bEnd = ""

277+ show BEnd = ""

docs/tutorial/typesfuns.rst+2−1

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

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

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

447as 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

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

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

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

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

451example:

452example:

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

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

4import Data.Vect

5

6data Random : Effect where

7− getRandom : sig Random Integer Integer

7+ GetRandom : sig Random Integer Integer

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

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

9

10instance Handler Random m where

11− handle seed getRandom k

11+ handle seed GetRandom k

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

13 k seed' seed'

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

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

15

16RND : EFFECT

17RND = MkEff Integer Random

18

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

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

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

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

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

23

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

25|||

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

27rndFin : (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))

29 return (toFin v)

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

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

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

43

44||| Sets the random seed

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

46−srand n = call $ setSeed n

46+srand n = call $ SetSeed n

47

src/Idris/AbsSyntax.hs+11−3

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

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

1695 -> Either Err PTerm

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

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

1698+ | otherwise

1697− = case lookupDef f (tt_ctxt ist) of

1699+ = case lookupDef f (tt_ctxt ist) of

1698 [] -> Right $ PPatvar ffc f

1700 [] -> Right $ PPatvar ffc f

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

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

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

1702 -- 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 [] _

1707 imp _ = True

1709 imp _ = True

1708-- allImp [] = False

1710-- allImp [] = False

1709 allImp xs = all imp xs

1711 allImp xs = all imp xs

1712+

1713+ unqualified (NS _ _) = False

1714+ unqualified _ = True

1715+

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

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

1711 constructor _ = False

1717 constructor _ = False

1712

1718

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

1887 su tm@(PRef fc hl f)

1893 su tm@(PRef fc hl f)

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

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

1889 = Placeholder

1895 = Placeholder

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

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

1897+ not (implicitable f)

1891 = PHidden tm

1898 = PHidden tm

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

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

1900+ not (implicitable f)

1893 = PHidden tm

1901 = PHidden tm

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

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

1895 -- here we use canBeDConName because the impossible pattern

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

501 | Placeholder <- getTm t,

502 n `elem` ps,

503 not (n `elem` bound)

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

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

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

506 addP _ ts = ts

507propagateParams 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

48import Data.Char(isLetter, toLower)

49import Data.List.Split (splitOn)

50

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!"

52

57

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

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

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

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

55 = do let codata = Codata `elem` opts

60 = do let codata = Codata `elem` opts

56 logLvl 1 (show (fc, doc))

61 logLvl 1 (show (fc, doc))

57 checkUndefined fc n

62 checkUndefined fc n

63+ when (implicitable n) $ warnLC fc n

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

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

59

65

60 addIBC (IBCDef n)

66 addIBC (IBCDef n)

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

65 = do let codata = Codata `elem` opts

71 = do let codata = Codata `elem` opts

66 logLvl 1 (show fc)

72 logLvl 1 (show fc)

67 undef <- isUndefined fc n

73 undef <- isUndefined fc n

74+ when (implicitable n) $ warnLC fc n

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

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

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

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

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

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

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

224 Idris (Name, Type)

231 Idris (Name, Type)

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

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

226 = do checkUndefined fc n

233 = do checkUndefined fc n

234+ when (implicitable n) $ warnLC fc n

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

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

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

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

229 ctxt <- getContext

237 ctxt <- getContext

test/basic002/test006.idr+8−8

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

1module Main

2

3data Parity : Nat -> Type where

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

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

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

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

6

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

8−parity Z = even {n=Z}

8+parity Z = Even {n=Z}

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

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

10parity (S (S k)) with (parity k)

11− parity (S (S (j + j))) | (even {n = j}) ?= even {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}

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

13

14natToBin : Nat -> List Bool

15natToBin Z = Nil

16natToBin k with (parity k)

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

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

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

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

19

20main : IO ()

21main = do printLn (natToBin 42)

test/basic010/Main.idr+13−13

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

9qib (S (S n)) = qib n * qib (S n)

10

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

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

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

13− eqZ : Z `equals` Z

13+ EqZ : Z `Equals` Z

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

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

15

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

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

17−eq_refl {n = Z} = eqZ

17+eq_refl {n = Z} = EqZ

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

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

19

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

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

23f Z n = Element n eq_refl

24f (S r) n = f r n

25

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

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

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

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

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

29

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

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

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

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

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

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

34g (S r) n = g r n

35

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

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

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

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

38

39main : IO ()

40main = do

test/basic010/expected+1−1

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

1*oink*

210000

3−axiom 10000

3+Axiom 10000

test/dsl001/test001.idr+10−10

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

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

18

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

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

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

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

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

22

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

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

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

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

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

26− lookup stop [] impossible

26+ lookup Stop [] impossible

27

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

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

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

41 dsl expr

42 lambda = lam_

43 variable = Var

44− index_first = stop

44+ index_first = Stop

45− index_next = pop

45+ index_next = Pop

46

47 total

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

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

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

68

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

71

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

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

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

81

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

83 eProg = Lam (Lam

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

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

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

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

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

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

88

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)

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

50

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

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

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

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

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

54

55 data Env : Vect n Ty -> Type where

56 Nil : Env Nil

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

58

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

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

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

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

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

62

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

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

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

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

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

66− update Nil stop _ impossible

66+ update Nil Stop _ impossible

67

68 total

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

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

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

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

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

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

73− envUpdate stop _ Nil impossible

73+ envUpdate Stop _ Nil impossible

74

75 total

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

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

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

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

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

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

80− envUpdateVal stop _ Nil impossible

80+ envUpdateVal Stop _ Nil impossible

81

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

83 envTail (x :: xs) = xs

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

169dsl res

170 variable = id

171 let = let_

172− index_first = stop

172+ index_first = Stop

173− index_next = pop

173+ index_next = Pop

174

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

176

test/proof003/Parity.idr+6−6

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

1module Parity

2

3data Parity : Nat -> Type where

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

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

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

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

6

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

8−parity Z = even {n=Z}

8+parity Z = Even {n=Z}

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

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

10parity (S (S k)) with (parity k)

11− parity (S (S (j + j))) | even ?= even {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}

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

13

14

15parity_lemma_2 = proof {

test/proof003/test015.idr+22−22

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

4import System

5

6data Bit : Nat -> Type where

7− b0 : Bit Z

7+ B0 : Bit Z

8− b1 : Bit (S Z)

8+ B1 : Bit (S Z)

9

10instance Show (Bit n) where

11 show = show' where

12 show' : Bit x -> String

13− show' b0 = "0"

13+ show' B0 = "0"

14− show' b1 = "1"

14+ show' B1 = "1"

15

16infixl 5 #

17

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

19− zero : Binary Z Z

19+ Zero : Binary Z Z

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

21

22instance Show (Binary w k) where

23− show zero = ""

23+ show Zero = ""

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

25

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

27−pad zero = zero # b0

27+pad Zero = Zero # B0

28pad (num # x) = pad num # x

29

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

31 Maybe (Binary width n)

32natToBin Z (S k) = Nothing

33−natToBin Z Z = Just zero

33+natToBin Z Z = Just Zero

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

35 Just (pad x)

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

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

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

38− let value = jbin # b1

38+ let value = jbin # B1

39 ?ntbEven

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

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

41− let value = jbin # b0

41+ let value = jbin # B0

42 ?ntbOdd

43

44testBin : Maybe (Binary 8 42)

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

49

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

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

52−addBit b0 b0 b0 = bitpair b0 b0

52+addBit B0 B0 B0 = bitpair B0 B0

53−addBit b0 b0 b1 = bitpair b0 b1

53+addBit B0 B0 B1 = bitpair B0 B1

54−addBit b0 b1 b0 = bitpair b0 b1

54+addBit B0 B1 B0 = bitpair B0 B1

55−addBit b0 b1 b1 = bitpair b1 b0

55+addBit B0 B1 B1 = bitpair B1 B0

56−addBit b1 b0 b0 = bitpair b0 b1

56+addBit B1 B0 B0 = bitpair B0 B1

57−addBit b1 b0 b1 = bitpair b1 b0

57+addBit B1 B0 B1 = bitpair B1 B0

58−addBit b1 b1 b0 = bitpair b1 b0

58+addBit B1 B1 B0 = bitpair B1 B0

59−addBit b1 b1 b1 = bitpair b1 b1

59+addBit B1 B1 B1 = bitpair B1 B1

60

61adc : 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

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

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

65 adc numx numy carry0 # lsb

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

75 printLn bin1

76 let Just bin2 = natToBin 8 89

77 printLn bin2

78− printLn (adc bin1 bin2 b0)

78+ printLn (adc bin1 bin2 B0)

79

80

81

test/proof005/DefaultArgSubstitutionSuccess.idr+4−4

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

23

24

25data SameNats : Type where

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

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

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

28

29data DiffNats : Type where

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

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

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

32

33

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

38zszArgsAreDiff = argsAreDiff Z (S Z)

39

40sameNatZs : SameNats

41−sameNatZs = same Z Z

41+sameNatZs = Same Z Z

42

43diffNatsZSZ : DiffNats

44−diffNatsZSZ = diff Z (S Z)

44+diffNatsZSZ = Diff Z (S Z)

test/proof006/DefaultArgSubstitutionSyntax.idr+4−4

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

30

31

32data 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

34

35data 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

37

38

39zArgsAreSame : ()

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

43zszArgsAreDiff = argsAreDiff Z (S Z)

44

45sameNatZs : SameNats

46−sameNatZs = same Z Z

46+sameNatZs = Same Z Z

47

48diffNatsZSZ : DiffNats

49−diffNatsZSZ = diff Z (S Z)

49+diffNatsZSZ = Diff Z (S Z)

test/proofsearch002/Process.idr+3−3

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

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

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

121

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

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

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

124 Process b iface hs hs'' p p''

125

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

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

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

209 Process b iface hs hs'' p p''

210−(>>=) = bind

210+(>>=) = Bind

211

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

213 Process (Maybe ty) iface'

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

371 k x' st

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

373eval 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)

375

376eval st (Fork proc) k

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

test/reg035/reg035a.lidr+5−5

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

28> )

29

30> data Set : Type -> Type where

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

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

32

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

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

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

35

36> postulate reflexive_Set_eqeq : (Eq a) =>

37> (as : Set a) ->

38> So (as == as)

39

40> unwrap : Set a -> List a

41−> unwrap (setify as) = as

41+> unwrap (Setify as) = as

42

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

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

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

45

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

47> listify = nub . unwrap

48

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

50−> arePairwiseDisjoint (setify ss) =

50+> arePairwiseDisjoint (Setify ss) =

51> hasNoDuplicates (concat (map listify ss))

52

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

2Z

test/reg041/ott.idr+24−24

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

3mutual

4

5 data U : Type where

6− u : U

6+ MkU : U

7− zero : U

7+ Zero : U

8− one : U

8+ One : U

9− two : U

9+ Two : U

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

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

11

12 El : U -> Type

13− El u = U

13+ El MkU = U

14− El zero = Void

14+ El Zero = Void

15− El one = ()

15+ El One = ()

16− El two = Bool

16+ El Two = Bool

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

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

18

19infixr 10 ~>

20(~>) : U -> U -> U

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

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

22

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

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

25

26%assert_total

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

28−EQ u u u u = one

28+EQ MkU MkU MkU MkU = One

29−EQ u zero u zero = one

29+EQ MkU Zero MkU Zero = One

30−EQ u one u one = one

30+EQ MkU One MkU One = One

31−EQ u two u two = one

31+EQ MkU Two MkU 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)

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

33+EQ Zero x Zero y = One

34−EQ one x one y = one

34+EQ One x One y = One

35−EQ two True two True = one

35+EQ Two True Two True = One

36−EQ two False two False = 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)

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

38+EQ _ _ _ _ = Zero

39−

39+

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

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

41example = ?prf

42

test/reg046/reg046.idr+7−7

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

1module test

2

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

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

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

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

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

6

7elimList : (A : Type) ->

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

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

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

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

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

11 (e : MyList A) ->

12 m e

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

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

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

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

15

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

17append 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)

19 b)

test/reg047/reg047.idr+2−2

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

1module test

2

3data 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

5

6data Nat = Zero | Succ Nat

7

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

15zzz = IdRefl Nat Zero

16

17eep : 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 @@

1module test

2

3data 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

5

6data MNat = Zero | Succ MNat

7

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

15zzzz = IdRefl MNat Zero

16

17eep : 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)

19

20eep2 : 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))

22

23

24

test/totality002/test017.idr+6−6

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

62ack (S m) Z = ack m (S Z)

63ack (S m) (S n) = ack m (ack (S m) n)

64

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

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

66

67foo : Bin -> Nat

68−foo eps = Z

68+foo EPS = Z

69−foo (c0 eps) = Z

69+foo (C0 EPS) = Z

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

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

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

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

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

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

73

74bar : Nat -> Nat -> Nat

75bar x y = mp x y where

test/totality004/totality004.idr+7−7

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

3%default total

4

5data SP : Type -> Type -> Type where

6− get : (a -> 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

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

8

9copy : SP a a

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

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

11

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

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

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

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

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

15

16doubleInt : SP Nat Int

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

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

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

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

19

20countStream : Nat -> Stream Nat

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

test/totality004/totality004a.idr+7−7

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

3%default total

4

5data SP : Type -> Type -> Type where

6− get : (a -> 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

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

8

9copy : SP a a

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

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

11

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

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

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

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

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

15

16doubleInt : SP Nat Int

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

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

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

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

19

20countStream : Nat -> Stream Nat

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

test/totality008/expected+1−1

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

1totality008.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 @@

1 data T : Type -> Type where

2− c1 : T Nat

2+ C1 : T Nat

3− c2 : T (T Nat)

3+ C2 : T (T Nat)

4

5total

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

7−ElimT _ c1 = 3

7+ElimT _ C1 = 3

8−ElimT _ c2 = c1

8+ElimT _ C2 = C1

test/tutorial002/tutorial002.idr+15−15

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

1module Main

2

3data Binary : Nat -> Type where

4− bEnd : Binary Z

4+ BEnd : Binary Z

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

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

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

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

7

8instance Show (Binary n) where

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

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

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

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

11− show bEnd = ""

11+ show BEnd = ""

12

13data Parity : Nat -> Type where

14− even : Parity (n + n)

14+ Even : Parity (n + n)

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

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

16

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

18−parity Z = even {n=Z}

18+parity Z = Even {n=Z}

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

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

20parity (S (S k)) with (parity k)

21− parity (S (S (j + j))) | even ?= even {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}

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

23

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

25−natToBin Z = bEnd

25+natToBin Z = BEnd

26natToBin (S k) with (parity k)

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

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

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

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

29

30intToNat : Int -> Nat

31intToNat 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

18 Parity (S (S (j + j)))

19

20Type mismatch between

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

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

22and

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

24

test/tutorial006/tutorial006b.idr+6−6

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

1

2data Parity : Nat -> Type where

3− even : Parity (n + n)

3+ Even : Parity (n + n)

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

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

5

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

7−parity Z = even {n=Z}

7+parity Z = Even {n=Z}

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

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

9parity (S (S k)) with (parity k)

10− parity (S (S (j + j))) | even = even {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}

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

12