ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-14 03:14:14 +03:00
Code Issues Projects Releases Wiki Activity

rename O into Z

Browse Source
This commit is contained in:
raichoo 2013-07-26 21:05:47 +02:00
parent c330406ffc
commit 2311d55013
50 changed files with 422 additions and 422 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
effects/Effect/Memory.idr
View File

@ -63,7 +63,7 @@ do_memmove dest src dest_offset src_offset size
private
do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect Bits8 size)
do_peek _ _ O = return (Prelude.Vect.Nil)
do_peek _ _ Z = return (Prelude.Vect.Nil)
do_peek ptr offset (S n)
= do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)
bs <- do_peek ptr (S offset) n

4
effects/Effects.idr
View File

@ -63,13 +63,13 @@ rebuildEnv (x :: xs) SubNil [] = x :: xs
-- some proof automation
findEffElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic -- Nat is maximum search depth
findEffElem O ctxt goal = Refine "Here" `Seq` Solve
findEffElem Z ctxt goal = Refine "Here" `Seq` Solve
findEffElem (S n) ctxt goal = GoalType "EffElem"
(Try (Refine "Here" `Seq` Solve)
(Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt goal)))
findSubList : Nat -> List (TTName, Binder TT) -> TT -> Tactic
findSubList O ctxt goal = Refine "SubNil" `Seq` Solve
findSubList Z ctxt goal = Refine "SubNil" `Seq` Solve
findSubList (S n) ctxt goal
= GoalType "SubList"
(Try (Refine "subListId" `Seq` Solve)

204
lib/Data/Bits.idr
View File

@ -4,11 +4,11 @@ module Data.Bits
divCeil : Nat -> Nat -> Nat
divCeil x y = case x `mod` y of
O => x `div` y
Z => x `div` y
S _ => S (x `div` y)
nextPow2 : Nat -> Nat
nextPow2 O = O
nextPow2 Z = Z
nextPow2 x = if x == (2 `power` l2x)
then l2x
else S l2x
@ -19,9 +19,9 @@ nextBytes : Nat -> Nat
nextBytes bits = (nextPow2 (bits `divCeil` 8))
machineTy : Nat -> Type
machineTy O = Bits8
machineTy (S O) = Bits16
machineTy (S (S O)) = Bits32
machineTy Z = Bits8
machineTy (S Z) = Bits16
machineTy (S (S Z)) = Bits32
machineTy (S (S (S _))) = Bits64
bitsUsed : Nat -> Nat
@ -29,19 +29,19 @@ bitsUsed n = 8 * (2 `power` n)
%assert_total
natToBits' : machineTy n -> Nat -> machineTy n
natToBits' a O = a
natToBits' a Z = a
natToBits' {n=n} a x with n
-- it seems I have to manually recover the value of n here, instead of being able to reference it
natToBits' a (S x') | O = natToBits' {n=0} (prim__addB8 a (prim__truncInt_B8 1)) x'
natToBits' a (S x') | S O = natToBits' {n=1} (prim__addB16 a (prim__truncInt_B16 1)) x'
natToBits' a (S x') | S (S O) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'
natToBits' a (S x') | Z = natToBits' {n=0} (prim__addB8 a (prim__truncInt_B8 1)) x'
natToBits' a (S x') | S Z = natToBits' {n=1} (prim__addB16 a (prim__truncInt_B16 1)) x'
natToBits' a (S x') | S (S Z) = natToBits' {n=2} (prim__addB32 a (prim__truncInt_B32 1)) x'
natToBits' a (S x') | S (S (S _)) = natToBits' {n=3} (prim__addB64 a (prim__truncInt_B64 1)) x'
natToBits : Nat -> machineTy n
natToBits {n=n} x with n
| O = natToBits' {n=0} (prim__truncInt_B8 0) x
| S O = natToBits' {n=1} (prim__truncInt_B16 0) x
| S (S O) = natToBits' {n=2} (prim__truncInt_B32 0) x
| Z = natToBits' {n=0} (prim__truncInt_B8 0) x
| S Z = natToBits' {n=1} (prim__truncInt_B16 0) x
| S (S Z) = natToBits' {n=2} (prim__truncInt_B32 0) x
| S (S (S _)) = natToBits' {n=3} (prim__truncInt_B64 0) x
getPad : Nat -> machineTy n
@ -94,9 +94,9 @@ pad64' n f x y = prim__lshrB64 (f (prim__shlB64 x pad) y) pad
shiftLeft' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
shiftLeft' {n=n} x c with (nextBytes n)
| O = pad8' n prim__shlB8 x c
| S O = pad16' n prim__shlB16 x c
| S (S O) = pad32' n prim__shlB32 x c
| Z = pad8' n prim__shlB8 x c
| S Z = pad16' n prim__shlB16 x c
| S (S Z) = pad32' n prim__shlB32 x c
| S (S (S _)) = pad64' n prim__shlB64 x c
public
@ -105,9 +105,9 @@ shiftLeft (MkBits x) (MkBits y) = MkBits (shiftLeft' x y)
shiftRightLogical' : machineTy n -> machineTy n -> machineTy n
shiftRightLogical' {n=n} x c with n
| O = prim__lshrB8 x c
| S O = prim__lshrB16 x c
| S (S O) = prim__lshrB32 x c
| Z = prim__lshrB8 x c
| S Z = prim__lshrB16 x c
| S (S Z) = prim__lshrB32 x c
| S (S (S _)) = prim__lshrB64 x c
public
@ -117,9 +117,9 @@ shiftRightLogical {n} (MkBits x) (MkBits y)
shiftRightArithmetic' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
shiftRightArithmetic' {n=n} x c with (nextBytes n)
| O = pad8' n prim__ashrB8 x c
| S O = pad16' n prim__ashrB16 x c
| S (S O) = pad32' n prim__ashrB32 x c
| Z = pad8' n prim__ashrB8 x c
| S Z = pad16' n prim__ashrB16 x c
| S (S Z) = pad32' n prim__ashrB32 x c
| S (S (S _)) = pad64' n prim__ashrB64 x c
public
@ -128,9 +128,9 @@ shiftRightArithmetic (MkBits x) (MkBits y) = MkBits (shiftRightArithmetic' x y)
and' : machineTy n -> machineTy n -> machineTy n
and' {n=n} x y with n
| O = prim__andB8 x y
| S O = prim__andB16 x y
| S (S O) = prim__andB32 x y
| Z = prim__andB8 x y
| S Z = prim__andB16 x y
| S (S Z) = prim__andB32 x y
| S (S (S _)) = prim__andB64 x y
public
@ -139,9 +139,9 @@ and {n} (MkBits x) (MkBits y) = MkBits (and' {n=nextBytes n} x y)
or' : machineTy n -> machineTy n -> machineTy n
or' {n=n} x y with n
| O = prim__orB8 x y
| S O = prim__orB16 x y
| S (S O) = prim__orB32 x y
| Z = prim__orB8 x y
| S Z = prim__orB16 x y
| S (S Z) = prim__orB32 x y
| S (S (S _)) = prim__orB64 x y
public
@ -150,9 +150,9 @@ or {n} (MkBits x) (MkBits y) = MkBits (or' {n=nextBytes n} x y)
xor' : machineTy n -> machineTy n -> machineTy n
xor' {n=n} x y with n
| O = prim__xorB8 x y
| S O = prim__xorB16 x y
| S (S O) = prim__xorB32 x y
| Z = prim__xorB8 x y
| S Z = prim__xorB16 x y
| S (S Z) = prim__xorB32 x y
| S (S (S _)) = prim__xorB64 x y
public
@ -161,9 +161,9 @@ xor {n} (MkBits x) (MkBits y) = MkBits {n} (xor' {n=nextBytes n} x y)
plus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
plus' {n=n} x y with (nextBytes n)
| O = pad8 n prim__addB8 x y
| S O = pad16 n prim__addB16 x y
| S (S O) = pad32 n prim__addB32 x y
| Z = pad8 n prim__addB8 x y
| S Z = pad16 n prim__addB16 x y
| S (S Z) = pad32 n prim__addB32 x y
| S (S (S _)) = pad64 n prim__addB64 x y
public
@ -172,9 +172,9 @@ plus (MkBits x) (MkBits y) = MkBits (plus' x y)
minus' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
minus' {n=n} x y with (nextBytes n)
| O = pad8 n prim__subB8 x y
| S O = pad16 n prim__subB16 x y
| S (S O) = pad32 n prim__subB32 x y
| Z = pad8 n prim__subB8 x y
| S Z = pad16 n prim__subB16 x y
| S (S Z) = pad32 n prim__subB32 x y
| S (S (S _)) = pad64 n prim__subB64 x y
public
@ -183,9 +183,9 @@ minus (MkBits x) (MkBits y) = MkBits (minus' x y)
times' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
times' {n=n} x y with (nextBytes n)
| O = pad8 n prim__mulB8 x y
| S O = pad16 n prim__mulB16 x y
| S (S O) = pad32 n prim__mulB32 x y
| Z = pad8 n prim__mulB8 x y
| S Z = pad16 n prim__mulB16 x y
| S (S Z) = pad32 n prim__mulB32 x y
| S (S (S _)) = pad64 n prim__mulB64 x y
public
@ -195,9 +195,9 @@ times (MkBits x) (MkBits y) = MkBits (times' x y)
partial
sdiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
sdiv' {n=n} x y with (nextBytes n)
| O = prim__sdivB8 x y
| S O = prim__sdivB16 x y
| S (S O) = prim__sdivB32 x y
| Z = prim__sdivB8 x y
| S Z = prim__sdivB16 x y
| S (S Z) = prim__sdivB32 x y
| S (S (S _)) = prim__sdivB64 x y
public partial
@ -207,9 +207,9 @@ sdiv (MkBits x) (MkBits y) = MkBits (sdiv' x y)
partial
udiv' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
udiv' {n=n} x y with (nextBytes n)
| O = prim__udivB8 x y
| S O = prim__udivB16 x y
| S (S O) = prim__udivB32 x y
| Z = prim__udivB8 x y
| S Z = prim__udivB16 x y
| S (S Z) = prim__udivB32 x y
| S (S (S _)) = prim__udivB64 x y
public partial
@ -219,9 +219,9 @@ udiv (MkBits x) (MkBits y) = MkBits (udiv' x y)
partial
srem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
srem' {n=n} x y with (nextBytes n)
| O = prim__sremB8 x y
| S O = prim__sremB16 x y
| S (S O) = prim__sremB32 x y
| Z = prim__sremB8 x y
| S Z = prim__sremB16 x y
| S (S Z) = prim__sremB32 x y
| S (S (S _)) = prim__sremB64 x y
public partial
@ -231,9 +231,9 @@ srem (MkBits x) (MkBits y) = MkBits (srem' x y)
partial
urem' : machineTy (nextBytes n) -> machineTy (nextBytes n) -> machineTy (nextBytes n)
urem' {n=n} x y with (nextBytes n)
| O = prim__uremB8 x y
| S O = prim__uremB16 x y
| S (S O) = prim__uremB32 x y
| Z = prim__uremB8 x y
| S Z = prim__uremB16 x y
| S (S Z) = prim__uremB32 x y
| S (S (S _)) = prim__uremB64 x y
public partial
@ -243,37 +243,37 @@ urem (MkBits x) (MkBits y) = MkBits (urem' x y)
-- TODO: Proofy comparisons via postulates
lt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
lt {n=n} x y with (nextBytes n)
| O = prim__ltB8 x y
| S O = prim__ltB16 x y
| S (S O) = prim__ltB32 x y
| Z = prim__ltB8 x y
| S Z = prim__ltB16 x y
| S (S Z) = prim__ltB32 x y
| S (S (S _)) = prim__ltB64 x y
lte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
lte {n=n} x y with (nextBytes n)
| O = prim__lteB8 x y
| S O = prim__lteB16 x y
| S (S O) = prim__lteB32 x y
| Z = prim__lteB8 x y
| S Z = prim__lteB16 x y
| S (S Z) = prim__lteB32 x y
| S (S (S _)) = prim__lteB64 x y
eq : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
eq {n=n} x y with (nextBytes n)
| O = prim__eqB8 x y
| S O = prim__eqB16 x y
| S (S O) = prim__eqB32 x y
| Z = prim__eqB8 x y
| S Z = prim__eqB16 x y
| S (S Z) = prim__eqB32 x y
| S (S (S _)) = prim__eqB64 x y
gte : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
gte {n=n} x y with (nextBytes n)
| O = prim__gteB8 x y
| S O = prim__gteB16 x y
| S (S O) = prim__gteB32 x y
| Z = prim__gteB8 x y
| S Z = prim__gteB16 x y
| S (S Z) = prim__gteB32 x y
| S (S (S _)) = prim__gteB64 x y
gt : machineTy (nextBytes n) -> machineTy (nextBytes n) -> Int
gt {n=n} x y with (nextBytes n)
| O = prim__gtB8 x y
| S O = prim__gtB16 x y
| S (S O) = prim__gtB32 x y
| Z = prim__gtB8 x y
| S Z = prim__gtB16 x y
| S (S Z) = prim__gtB32 x y
| S (S (S _)) = prim__gtB64 x y
instance Eq (Bits n) where
@ -293,11 +293,11 @@ instance Ord (Bits n) where
complement' : machineTy (nextBytes n) -> machineTy (nextBytes n)
complement' {n=n} x with (nextBytes n)
| O = let pad = getPad {n=0} n in
| Z = let pad = getPad {n=0} n in
prim__complB8 (x `prim__shlB8` pad) `prim__lshrB8` pad
| S O = let pad = getPad {n=1} n in
| S Z = let pad = getPad {n=1} n in
prim__complB16 (x `prim__shlB16` pad) `prim__lshrB16` pad
| S (S O) = let pad = getPad {n=2} n in
| S (S Z) = let pad = getPad {n=2} n in
prim__complB32 (x `prim__shlB32` pad) `prim__lshrB32` pad
| S (S (S _)) = let pad = getPad {n=3} n in
prim__complB64 (x `prim__shlB64` pad) `prim__lshrB64` pad
@ -309,15 +309,15 @@ complement (MkBits x) = MkBits (complement' x)
-- TODO: Prove
zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
| (O, O) = believe_me x
| (O, S O) = believe_me (prim__zextB8_B16 (believe_me x))
| (O, S (S O)) = believe_me (prim__zextB8_B32 (believe_me x))
| (O, S (S (S _))) = believe_me (prim__zextB8_B64 (believe_me x))
| (S O, S O) = believe_me x
| (S O, S (S O)) = believe_me (prim__zextB16_B32 (believe_me x))
| (S O, S (S (S _))) = believe_me (prim__zextB16_B64 (believe_me x))
| (S (S O), S (S O)) = believe_me x
| (S (S O), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))
| (Z, Z) = believe_me x
| (Z, S Z) = believe_me (prim__zextB8_B16 (believe_me x))
| (Z, S (S Z)) = believe_me (prim__zextB8_B32 (believe_me x))
| (Z, S (S (S _))) = believe_me (prim__zextB8_B64 (believe_me x))
| (S Z, S Z) = believe_me x
| (S Z, S (S Z)) = believe_me (prim__zextB16_B32 (believe_me x))
| (S Z, S (S (S _))) = believe_me (prim__zextB16_B64 (believe_me x))
| (S (S Z), S (S Z)) = believe_me x
| (S (S Z), S (S (S _))) = believe_me (prim__zextB32_B64 (believe_me x))
| (S (S (S _)), S (S (S _))) = believe_me x
public
@ -327,11 +327,11 @@ zeroExtend (MkBits x) = MkBits (zext' x)
%assert_total
intToBits' : Integer -> machineTy (nextBytes n)
intToBits' {n=n} x with (nextBytes n)
| O = let pad = getPad {n=0} n in
| Z = let pad = getPad {n=0} n in
prim__lshrB8 (prim__shlB8 (prim__truncBigInt_B8 x) pad) pad
| S O = let pad = getPad {n=1} n in
| S Z = let pad = getPad {n=1} n in
prim__lshrB16 (prim__shlB16 (prim__truncBigInt_B16 x) pad) pad
| S (S O) = let pad = getPad {n=2} n in
| S (S Z) = let pad = getPad {n=2} n in
prim__lshrB32 (prim__shlB32 (prim__truncBigInt_B32 x) pad) pad
| S (S (S _)) = let pad = getPad {n=3} n in
prim__lshrB64 (prim__shlB64 (prim__truncBigInt_B64 x) pad) pad
@ -345,9 +345,9 @@ instance Cast Integer (Bits n) where
bitsToInt' : machineTy (nextBytes n) -> Integer
bitsToInt' {n=n} x with (nextBytes n)
| O = prim__zextB8_BigInt x
| S O = prim__zextB16_BigInt x
| S (S O) = prim__zextB32_BigInt x
| Z = prim__zextB8_BigInt x
| S Z = prim__zextB16_BigInt x
| S (S Z) = prim__zextB32_BigInt x
| S (S (S _)) = prim__zextB64_BigInt x
public
@ -364,28 +364,28 @@ bitsToInt (MkBits x) = bitsToInt' x
-- TODO: Prove
sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))
sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
| (O, O) = let pad = getPad {n=0} n in
| (Z, Z) = let pad = getPad {n=0} n in
believe_me (prim__ashrB8 (prim__shlB8 (believe_me x) pad) pad)
| (O, S O) = let pad = getPad {n=0} n in
| (Z, S Z) = let pad = getPad {n=0} n in
believe_me (prim__ashrB16 (prim__sextB8_B16 (prim__shlB8 (believe_me x) pad))
(prim__zextB8_B16 pad))
| (O, S (S O)) = let pad = getPad {n=0} n in
| (Z, S (S Z)) = let pad = getPad {n=0} n in
believe_me (prim__ashrB32 (prim__sextB8_B32 (prim__shlB8 (believe_me x) pad))
(prim__zextB8_B32 pad))
| (O, S (S (S _))) = let pad = getPad {n=0} n in
| (Z, S (S (S _))) = let pad = getPad {n=0} n in
believe_me (prim__ashrB64 (prim__sextB8_B64 (prim__shlB8 (believe_me x) pad))
(prim__zextB8_B64 pad))
| (S O, S O) = let pad = getPad {n=1} n in
| (S Z, S Z) = let pad = getPad {n=1} n in
believe_me (prim__ashrB16 (prim__shlB16 (believe_me x) pad) pad)
| (S O, S (S O)) = let pad = getPad {n=1} n in
| (S Z, S (S Z)) = let pad = getPad {n=1} n in
believe_me (prim__ashrB32 (prim__sextB16_B32 (prim__shlB16 (believe_me x) pad))
(prim__zextB16_B32 pad))
| (S O, S (S (S _))) = let pad = getPad {n=1} n in
| (S Z, S (S (S _))) = let pad = getPad {n=1} n in
believe_me (prim__ashrB64 (prim__sextB16_B64 (prim__shlB16 (believe_me x) pad))
(prim__zextB16_B64 pad))
| (S (S O), S (S O)) = let pad = getPad {n=2} n in
| (S (S Z), S (S Z)) = let pad = getPad {n=2} n in
believe_me (prim__ashrB32 (prim__shlB32 (believe_me x) pad) pad)
| (S (S O), S (S (S _))) = let pad = getPad {n=2} n in
| (S (S Z), S (S (S _))) = let pad = getPad {n=2} n in
believe_me (prim__ashrB64 (prim__sextB32_B64 (prim__shlB32 (believe_me x) pad))
(prim__zextB32_B64 pad))
| (S (S (S _)), S (S (S _))) = let pad = getPad {n=3} n in
@ -398,15 +398,15 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
-- TODO: Prove
trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
| (O, O) = believe_me x
| (O, S O) = believe_me (prim__truncB16_B8 (believe_me x))
| (O, S (S O)) = believe_me (prim__truncB32_B8 (believe_me x))
| (O, S (S (S _))) = believe_me (prim__truncB64_B8 (believe_me x))
| (S O, S O) = believe_me x
| (S O, S (S O)) = believe_me (prim__truncB32_B16 (believe_me x))
| (S O, S (S (S _))) = believe_me (prim__truncB64_B16 (believe_me x))
| (S (S O), S (S O)) = believe_me x
| (S (S O), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
| (Z, Z) = believe_me x
| (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))
| (Z, S (S Z)) = believe_me (prim__truncB32_B8 (believe_me x))
| (Z, S (S (S _))) = believe_me (prim__truncB64_B8 (believe_me x))
| (S Z, S Z) = believe_me x
| (S Z, S (S Z)) = believe_me (prim__truncB32_B16 (believe_me x))
| (S Z, S (S (S _))) = believe_me (prim__truncB64_B16 (believe_me x))
| (S (S Z), S (S Z)) = believe_me x
| (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
| (S (S (S _)), S (S (S _))) = believe_me x
--public

6
lib/Data/BoundedList.idr
View File

@ -34,7 +34,7 @@ weaken (x :: xs) = x :: weaken xs
take : (n : Nat) -> List a -> BoundedList a n
take _ [] = []
take O _ = []
take Z _ = []
take (S n') (x :: xs) = x :: take n' xs
toList : BoundedList a n -> List a
@ -50,7 +50,7 @@ fromList (x :: xs) = x :: fromList xs
--------------------------------------------------------------------------------
replicate : (n : Nat) -> a -> BoundedList a n
replicate O _ = []
replicate Z _ = []
replicate (S n) x = x :: replicate n x
--------------------------------------------------------------------------------
@ -79,7 +79,7 @@ map f (x :: xs) = f x :: map f xs
%assert_total -- not sure why this isn't accepted - clearly decreasing on n
pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n
pad {n=O} [] _ = []
pad {n=Z} [] _ = []
pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding

2
lib/Data/HVect.idr
View File

@ -40,7 +40,7 @@ using (k : Nat, ts : Vect Type k)
class Shows (k : Nat) (ts : Vect Type k) where
shows : HVect ts -> Vect String k
instance Shows O [] where
instance Shows Z [] where
shows [] = []
instance (Show t, Shows k ts) => Shows (S k) (t::ts) where

12
lib/Data/SortedMap.idr
View File

@ -3,7 +3,7 @@ module Data.SortedMap
-- TODO: write merge and split
data Tree : Nat -> Type -> Type -> Type where
Leaf : k -> v -> Tree O k v
Leaf : k -> v -> Tree Z k v
Branch2 : Tree n k v -> k -> Tree n k v -> Tree (S n) k v
Branch3 : Tree n k v -> k -> Tree n k v -> k -> Tree n k v -> Tree (S n) k v
@ -123,7 +123,7 @@ treeInsert k v t =
Right (a, b, c) => Right (Branch2 a b c)
delType : Nat -> Type -> Type -> Type
delType O k v = ()
delType Z k v = ()
delType (S n) k v = Tree n k v
treeDelete : Ord k => k -> Tree n k v -> Either (Tree n k v) (delType n k v)
@ -132,7 +132,7 @@ treeDelete k (Leaf k' v) =
Right ()
else
Left (Leaf k' v)
treeDelete {n=S O} k (Branch2 t1 k' t2) =
treeDelete {n=S Z} k (Branch2 t1 k' t2) =
if k <= k' then
case treeDelete k t1 of
Left t1' => Left (Branch2 t1' k' t2)
@ -141,7 +141,7 @@ treeDelete {n=S O} k (Branch2 t1 k' t2) =
case treeDelete k t2 of
Left t2' => Left (Branch2 t1 k' t2')
Right () => Right t1
treeDelete {n=S O} k (Branch3 t1 k1 t2 k2 t3) =
treeDelete {n=S Z} k (Branch3 t1 k1 t2 k2 t3) =
if k <= k1 then
case treeDelete k t1 of
Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
@ -201,7 +201,7 @@ lookup _ Empty = Nothing
lookup k (M _ t) = treeLookup k t
insert : Ord k => k -> v -> SortedMap k v -> SortedMap k v
insert k v Empty = M O (Leaf k v)
insert k v Empty = M Z (Leaf k v)
insert k v (M _ t) =
case treeInsert k v t of
Left t' => (M _ t')
@ -209,7 +209,7 @@ insert k v (M _ t) =
delete : Ord k => k -> SortedMap k v -> SortedMap k v
delete _ Empty = Empty
delete k (M O t) =
delete k (M Z t) =
case treeDelete k t of
Left t' => (M _ t')
Right () => Empty

2
lib/Data/Vect.idr
View File

@ -14,7 +14,7 @@ data Elem : a -> Vect a k -> Type where
There : {xs : Vect a k} -> Elem x xs -> Elem x (y::xs)
findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic
findElem O ctxt goal = Refine "Here" `Seq` Solve
findElem Z ctxt goal = Refine "Here" `Seq` Solve
findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))
replaceElem : (xs : Vect t k) -> Elem x xs -> (y : t) -> (ys : Vect t k ** Elem y ys)

12
lib/Data/ZZ.idr
View File

@ -24,17 +24,17 @@ instance Show ZZ where
show (NegS n) = "-" ++ show (S n)
negZ : ZZ -> ZZ
negZ (Pos O) = Pos O
negZ (Pos Z) = Pos Z
negZ (Pos (S n)) = NegS n
negZ (NegS n) = Pos (S n)
negNat : Nat -> ZZ
negNat O = Pos O
negNat Z = Pos Z
negNat (S n) = NegS n
minusNatZ : Nat -> Nat -> ZZ
minusNatZ n O = Pos n
minusNatZ O (S m) = NegS m
minusNatZ n Z = Pos n
minusNatZ Z (S m) = NegS m
minusNatZ (S n) (S m) = minusNatZ n m
plusZ : ZZ -> ZZ -> ZZ
@ -101,9 +101,9 @@ natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)
natMultZMult n m x h = cong h
doubleNegElim : (z : ZZ) -> negZ (negZ z) = z
doubleNegElim (Pos O) = refl
doubleNegElim (Pos Z) = refl
doubleNegElim (Pos (S n)) = refl
doubleNegElim (NegS O) = refl
doubleNegElim (NegS Z) = refl
doubleNegElim (NegS (S n)) = refl
-- Injectivity

8
lib/Decidable/Equality.idr
View File

@ -41,13 +41,13 @@ instance DecEq Bool where
-- Nat
--------------------------------------------------------------------------------
total OnotS : O = S n -> _|_
total OnotS : Z = S n -> _|_
OnotS refl impossible
instance DecEq Nat where
decEq O O = Yes refl
decEq O (S _) = No OnotS
decEq (S _) O = No (negEqSym OnotS)
decEq Z Z = Yes refl
decEq Z (S _) = No OnotS
decEq (S _) Z = No (negEqSym OnotS)
decEq (S n) (S m) with (decEq n m)
| Yes p = Yes $ cong p
| No p = No $ \h : (S n = S m) => p $ succInjective n m h

6
lib/Decidable/Order.idr
View File

@ -55,7 +55,7 @@ NatLTEIsAntisymmetric n m (nLTESm _) (nLTESm _) impossible
instance Poset Nat NatLTE where
antisymmetric = NatLTEIsAntisymmetric
total zeroNeverGreater : {n : Nat} -> NatLTE (S n) O -> _|_
total zeroNeverGreater : {n : Nat} -> NatLTE (S n) Z -> _|_
zeroNeverGreater {n} (nLTESm _) impossible
zeroNeverGreater {n} nEqn impossible
@ -66,8 +66,8 @@ nGTSm {n} {m} disprf (nEqn) impossible
total
decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)
decideNatLTE O O = Yes nEqn
decideNatLTE (S x) O = No zeroNeverGreater
decideNatLTE Z Z = Yes nEqn
decideNatLTE (S x) Z = No zeroNeverGreater
decideNatLTE x (S y) with (decEq x (S y))
| Yes eq = rewrite eq in Yes nEqn
| No _ with (decideNatLTE x y)

2
lib/Prelude.idr
View File

@ -251,7 +251,7 @@ instance Monad List where
%lib C "m"
pow : (Num a) => a -> Nat -> a
pow x O = 1
pow x Z = 1
pow x (S n) = x * (pow x n)
exp : Float -> Float

6
lib/Prelude/Fin.idr
View File

@ -17,7 +17,7 @@ finToNat fO a = a
finToNat (fS x) a = finToNat x (S a)
instance Cast (Fin n) Nat where
cast x = finToNat x O
cast x = finToNat x Z
finToInt : Fin n -> Integer -> Integer
finToInt fO a = a
@ -38,7 +38,7 @@ strengthen {n = S k} (fS i) with (strengthen i)
strengthen f = Left f
last : Fin (S n)
last {n=O} = fO
last {n=Z} = fO
last {n=S _} = fS last
total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
@ -48,7 +48,7 @@ fSinjective refl = refl
-- Construct a Fin from an integer literal which must fit in the given Fin
natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
natToFin O (S j) = Just fO
natToFin Z (S j) = Just fO
natToFin (S k) (S j) with (natToFin k j)
| Just k' = Just (fS k')
| Nothing = Nothing

4
lib/Prelude/Heap.idr
View File

@ -27,7 +27,7 @@ isEmpty Empty = True
isEmpty _ = False
total size : MaxiphobicHeap a -> Nat
size Empty = O
size Empty = Z
size (Node s l e r) = s
isValidHeap : Ord a => MaxiphobicHeap a -> Bool
@ -148,7 +148,7 @@ absurdBoolDischarge p = replace {P = disjointTy} p ()
disjointTy False = ()
disjointTy True = _|_
total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = O
total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
isEmptySizeZero Empty p = refl
isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd

10
lib/Prelude/List.idr
View File

@ -85,12 +85,12 @@ init' (x::xs) =
--------------------------------------------------------------------------------
take : Nat -> List a -> List a
take O xs = []
take Z xs = []
take (S n) [] = []
take (S n) (x::xs) = x :: take n xs
drop : Nat -> List a -> List a
drop O xs = xs
drop Z xs = xs
drop (S n) [] = []
drop (S n) (x::xs) = drop n xs
@ -127,7 +127,7 @@ repeat : a -> List a
repeat x = x :: lazy (repeat x)
replicate : Nat -> a -> List a
replicate O x = []
replicate Z x = []
replicate (S n) x = x :: replicate n x
--------------------------------------------------------------------------------
@ -325,7 +325,7 @@ find p (x::xs) =
find p xs
findIndex : (a -> Bool) -> List a -> Maybe Nat
findIndex = findIndex' O
findIndex = findIndex' Z
where
-- findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat
findIndex' cnt p [] = Nothing
@ -336,7 +336,7 @@ findIndex = findIndex' O
findIndex' (S cnt) p xs
findIndices : (a -> Bool) -> List a -> List Nat
findIndices = findIndices' O
findIndices = findIndices' Z
where
-- findIndices' : Nat -> (a -> Bool) -> List a -> List Nat
findIndices' cnt p [] = []

210
lib/Prelude/Nat.idr
View File

@ -9,7 +9,7 @@ import Prelude.Cast
%default total
data Nat
= O
= Z
| S Nat
--------------------------------------------------------------------------------
@ -17,11 +17,11 @@ data Nat
--------------------------------------------------------------------------------
total isZero : Nat -> Bool
isZero O = True
isZero Z = True
isZero (S n) = False
total isSucc : Nat -> Bool
isSucc O = False
isSucc Z = False
isSucc (S n) = True
--------------------------------------------------------------------------------
@ -29,27 +29,27 @@ isSucc (S n) = True
--------------------------------------------------------------------------------
total plus : Nat -> Nat -> Nat
plus O right = right
plus Z right = right
plus (S left) right = S (plus left right)
total mult : Nat -> Nat -> Nat
mult O right = O
mult Z right = Z
mult (S left) right = plus right $ mult left right
total minus : Nat -> Nat -> Nat
minus O right = O
minus left O = left
minus Z right = Z
minus left Z = left
minus (S left) (S right) = minus left right
total power : Nat -> Nat -> Nat
power base O = S O
power base Z = S Z
power base (S exp) = mult base $ power base exp
hyper : Nat -> Nat -> Nat -> Nat
hyper O a b = S b
hyper (S O) a O = a
hyper (S(S O)) a O = O
hyper n a O = S O
hyper Z a b = S b
hyper (S Z) a Z = a
hyper (S(S Z)) a Z = Z
hyper n a Z = S Z
hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)
@ -58,7 +58,7 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)
--------------------------------------------------------------------------------
data LTE : Nat -> Nat -> Type where
lteZero : LTE O right
lteZero : LTE Z right
lteSucc : LTE left right -> LTE (S left) (S right)
total GTE : Nat -> Nat -> Type
@ -71,8 +71,8 @@ total GT : Nat -> Nat -> Type
GT left right = LT right left
total lte : Nat -> Nat -> Bool
lte O right = True
lte left O = False
lte Z right = True
lte left Z = False
lte (S left) (S right) = lte left right
total gte : Nat -> Nat -> Bool
@ -103,18 +103,18 @@ maximum left right =
--------------------------------------------------------------------------------
instance Eq Nat where
O == O = True
Z == Z = True
(S l) == (S r) = l == r
_ == _ = False
instance Cast Nat Integer where
cast O = 0
cast Z = 0
cast (S k) = 1 + cast k
instance Ord Nat where
compare O O = EQ
compare O (S k) = LT
compare (S k) O = GT
compare Z Z = EQ
compare Z (S k) = LT
compare (S k) Z = GT
compare (S x) (S y) = compare x y
instance Num Nat where
@ -128,12 +128,12 @@ instance Num Nat where
where
%assert_total
fromInteger' : Integer -> Nat
fromInteger' 0 = O
fromInteger' 0 = Z
fromInteger' n =
if (n > 0) then
S (fromInteger' (n - 1))
else
O
Z
instance Cast Integer Nat where
cast = fromInteger
@ -171,10 +171,10 @@ instance Semigroup Additive where
getAdditive m => m
instance Monoid Multiplicative where
neutral = getMultiplicative $ S O
neutral = getMultiplicative $ S Z
instance Monoid Additive where
neutral = getAdditive O
neutral = getAdditive Z
instance MeetSemilattice Nat where
meet = minimum
@ -185,14 +185,14 @@ instance JoinSemilattice Nat where
instance Lattice Nat where { }
instance BoundedJoinSemilattice Nat where
bottom = O
bottom = Z
--------------------------------------------------------------------------------
-- Auxilliary notions
--------------------------------------------------------------------------------
total pred : Nat -> Nat
pred O = O
pred Z = Z
pred (S n) = n
--------------------------------------------------------------------------------
@ -200,8 +200,8 @@ pred (S n) = n
--------------------------------------------------------------------------------
total fib : Nat -> Nat
fib O = O
fib (S O) = S O
fib Z = Z
fib (S Z) = S Z
fib (S (S n)) = fib (S n) + fib n
--------------------------------------------------------------------------------
@ -213,11 +213,11 @@ fib (S (S n)) = fib (S n) + fib n
--------------------------------------------------------------------------------
total mod : Nat -> Nat -> Nat
mod left O = left
mod left Z = left
mod left (S right) = mod' left left right
where
total mod' : Nat -> Nat -> Nat -> Nat
mod' O centre right = centre
mod' Z centre right = centre
mod' (S left) centre right =
if lte centre right then
centre
@ -225,21 +225,21 @@ mod left (S right) = mod' left left right
mod' left (centre - (S right)) right
total div : Nat -> Nat -> Nat
div left O = S left -- div by zero
div left Z = S left -- div by zero
div left (S right) = div' left left right
where
total div' : Nat -> Nat -> Nat -> Nat
div' O centre right = O
div' Z centre right = Z
div' (S left) centre right =
if lte centre right then
O
Z
else
S (div' left (centre - (S right)) right)
%assert_total
log2 : Nat -> Nat
log2 O = O
log2 (S O) = O
log2 Z = Z
log2 (S Z) = Z
log2 n = S (log2 (n `div` 2))
--------------------------------------------------------------------------------
@ -260,28 +260,28 @@ total plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
plusZeroLeftNeutral right = refl
total plusZeroRightNeutral : (left : Nat) -> left + 0 = left
plusZeroRightNeutral O = refl
plusZeroRightNeutral Z = refl
plusZeroRightNeutral (S n) =
let inductiveHypothesis = plusZeroRightNeutral n in
?plusZeroRightNeutralStepCase
total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
S (left + right) = left + (S right)
plusSuccRightSucc O right = refl
plusSuccRightSucc Z right = refl
plusSuccRightSucc (S left) right =
let inductiveHypothesis = plusSuccRightSucc left right in
?plusSuccRightSuccStepCase
total plusCommutative : (left : Nat) -> (right : Nat) ->
left + right = right + left
plusCommutative O right = ?plusCommutativeBaseCase
plusCommutative Z right = ?plusCommutativeBaseCase
plusCommutative (S left) right =
let inductiveHypothesis = plusCommutative left right in
?plusCommutativeStepCase
total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
left + (centre + right) = (left + centre) + right
plusAssociative O centre right = refl
plusAssociative Z centre right = refl
plusAssociative (S left) centre right =
let inductiveHypothesis = plusAssociative left centre right in
?plusAssociativeStepCase
@ -299,38 +299,38 @@ plusOneSucc n = refl
total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
(p : left + right = left + right') -> right = right'
plusLeftCancel O right right' p = ?plusLeftCancelBaseCase
plusLeftCancel Z right right' p = ?plusLeftCancelBaseCase
plusLeftCancel (S left) right right' p =
let inductiveHypothesis = plusLeftCancel left right right' in
?plusLeftCancelStepCase
total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
(p : left + right = left' + right) -> left = left'
plusRightCancel left left' O p = ?plusRightCancelBaseCase
plusRightCancel left left' Z p = ?plusRightCancelBaseCase
plusRightCancel left left' (S right) p =
let inductiveHypothesis = plusRightCancel left left' right in
?plusRightCancelStepCase
total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
(p : left + right = left) -> right = O
plusLeftLeftRightZero O right p = ?plusLeftLeftRightZeroBaseCase
(p : left + right = left) -> right = Z
plusLeftLeftRightZero Z right p = ?plusLeftLeftRightZeroBaseCase
plusLeftLeftRightZero (S left) right p =
let inductiveHypothesis = plusLeftLeftRightZero left right in
?plusLeftLeftRightZeroStepCase
-- Mult
total multZeroLeftZero : (right : Nat) -> O * right = O
total multZeroLeftZero : (right : Nat) -> Z * right = Z
multZeroLeftZero right = refl
total multZeroRightZero : (left : Nat) -> left * O = O
multZeroRightZero O = refl
total multZeroRightZero : (left : Nat) -> left * Z = Z
multZeroRightZero Z = refl
multZeroRightZero (S left) =
let inductiveHypothesis = multZeroRightZero left in
?multZeroRightZeroStepCase
total multRightSuccPlus : (left : Nat) -> (right : Nat) ->
left * (S right) = left + (left * right)
multRightSuccPlus O right = refl
multRightSuccPlus Z right = refl
multRightSuccPlus (S left) right =
let inductiveHypothesis = multRightSuccPlus left right in
?multRightSuccPlusStepCase
@ -341,40 +341,40 @@ multLeftSuccPlus left right = refl
total multCommutative : (left : Nat) -> (right : Nat) ->
left * right = right * left
multCommutative O right = ?multCommutativeBaseCase
multCommutative Z right = ?multCommutativeBaseCase
multCommutative (S left) right =
let inductiveHypothesis = multCommutative left right in
?multCommutativeStepCase
total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
left * (centre + right) = (left * centre) + (left * right)
multDistributesOverPlusRight O centre right = refl
multDistributesOverPlusRight Z centre right = refl
multDistributesOverPlusRight (S left) centre right =
let inductiveHypothesis = multDistributesOverPlusRight left centre right in
?multDistributesOverPlusRightStepCase
total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
(left + centre) * right = (left * right) + (centre * right)
multDistributesOverPlusLeft O centre right = refl
multDistributesOverPlusLeft Z centre right = refl
multDistributesOverPlusLeft (S left) centre right =
let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
?multDistributesOverPlusLeftStepCase
total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
left * (centre * right) = (left * centre) * right
multAssociative O centre right = refl
multAssociative Z centre right = refl
multAssociative (S left) centre right =
let inductiveHypothesis = multAssociative left centre right in
?multAssociativeStepCase
total multOneLeftNeutral : (right : Nat) -> 1 * right = right
multOneLeftNeutral O = refl
multOneLeftNeutral Z = refl
multOneLeftNeutral (S right) =
let inductiveHypothesis = multOneLeftNeutral right in
?multOneLeftNeutralStepCase
total multOneRightNeutral : (left : Nat) -> left * 1 = left
multOneRightNeutral O = refl
multOneRightNeutral Z = refl
multOneRightNeutral (S left) =
let inductiveHypothesis = multOneRightNeutral left in
?multOneRightNeutralStepCase
@ -384,51 +384,51 @@ total minusSuccSucc : (left : Nat) -> (right : Nat) ->
(S left) - (S right) = left - right
minusSuccSucc left right = refl
total minusZeroLeft : (right : Nat) -> 0 - right = O
total minusZeroLeft : (right : Nat) -> 0 - right = Z
minusZeroLeft right = refl
total minusZeroRight : (left : Nat) -> left - 0 = left
minusZeroRight O = refl
minusZeroRight Z = refl
minusZeroRight (S left) = refl
total minusZeroN : (n : Nat) -> O = n - n
minusZeroN O = refl
total minusZeroN : (n : Nat) -> Z = n - n
minusZeroN Z = refl
minusZeroN (S n) = minusZeroN n
total minusOneSuccN : (n : Nat) -> S O = (S n) - n
minusOneSuccN O = refl
total minusOneSuccN : (n : Nat) -> S Z = (S n) - n
minusOneSuccN Z = refl
minusOneSuccN (S n) = minusOneSuccN n
total minusSuccOne : (n : Nat) -> S n - 1 = n
minusSuccOne O = refl
minusSuccOne Z = refl
minusSuccOne (S n) = refl
total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = O
minusPlusZero O m = refl
total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = Z
minusPlusZero Z m = refl
minusPlusZero (S n) m = minusPlusZero n m
total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
left - centre - right = left - (centre + right)
minusMinusMinusPlus O O right = refl
minusMinusMinusPlus (S left) O right = refl
minusMinusMinusPlus O (S centre) right = refl
minusMinusMinusPlus Z Z right = refl
minusMinusMinusPlus (S left) Z right = refl
minusMinusMinusPlus Z (S centre) right = refl
minusMinusMinusPlus (S left) (S centre) right =
let inductiveHypothesis = minusMinusMinusPlus left centre right in
?minusMinusMinusPlusStepCase
total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
(left + right) - (left + right') = right - right'
plusMinusLeftCancel O right right' = refl
plusMinusLeftCancel Z right right' = refl
plusMinusLeftCancel (S left) right right' =
let inductiveHypothesis = plusMinusLeftCancel left right right' in
?plusMinusLeftCancelStepCase
total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
(left - centre) * right = (left * right) - (centre * right)
multDistributesOverMinusLeft O O right = refl
multDistributesOverMinusLeft (S left) O right =
multDistributesOverMinusLeft Z Z right = refl
multDistributesOverMinusLeft (S left) Z right =
?multDistributesOverMinusLeftBaseCase
multDistributesOverMinusLeft O (S centre) right = refl
multDistributesOverMinusLeft Z (S centre) right = refl
multDistributesOverMinusLeft (S left) (S centre) right =
let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
?multDistributesOverMinusLeftStepCase
@ -445,35 +445,35 @@ powerSuccPowerLeft base exp = refl
total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
(power base exp) * (power base exp') = power base (exp + exp')
multPowerPowerPlus base O exp' = ?multPowerPowerPlusBaseCase
multPowerPowerPlus base Z exp' = ?multPowerPowerPlusBaseCase
multPowerPowerPlus base (S exp) exp' =
let inductiveHypothesis = multPowerPowerPlus base exp exp' in
?multPowerPowerPlusStepCase
total powerZeroOne : (base : Nat) -> power base 0 = S O
total powerZeroOne : (base : Nat) -> power base 0 = S Z
powerZeroOne base = refl
total powerOneNeutral : (base : Nat) -> power base 1 = base
powerOneNeutral O = refl
powerOneNeutral Z = refl
powerOneNeutral (S base) =
let inductiveHypothesis = powerOneNeutral base in
?powerOneNeutralStepCase
total powerOneSuccOne : (exp : Nat) -> power 1 exp = S O
powerOneSuccOne O = refl
total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z
powerOneSuccOne Z = refl
powerOneSuccOne (S exp) =
let inductiveHypothesis = powerOneSuccOne exp in
?powerOneSuccOneStepCase
total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base
powerSuccSuccMult O = refl
powerSuccSuccMult Z = refl
powerSuccSuccMult (S base) =
let inductiveHypothesis = powerSuccSuccMult base in
?powerSuccSuccMultStepCase
total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->
power (power base exp) exp' = power base (exp * exp')
powerPowerMultPower base exp O = ?powerPowerMultPowerBaseCase
powerPowerMultPower base exp Z = ?powerPowerMultPowerBaseCase
powerPowerMultPower base exp (S exp') =
let inductiveHypothesis = powerPowerMultPower base exp exp' in
?powerPowerMultPowerStepCase
@ -484,9 +484,9 @@ predSucc n = refl
total minusSuccPred : (left : Nat) -> (right : Nat) ->
left - (S right) = pred (left - right)
minusSuccPred O right = refl
minusSuccPred (S left) O =
let inductiveHypothesis = minusSuccPred left O in
minusSuccPred Z right = refl
minusSuccPred (S left) Z =
let inductiveHypothesis = minusSuccPred left Z in
?minusSuccPredStepCase
minusSuccPred (S left) (S right) =
let inductiveHypothesis = minusSuccPred left right in
@ -520,69 +520,69 @@ boolElimMultMultRight False right t f = refl
-- Orders
total lteNTrue : (n : Nat) -> lte n n = True
lteNTrue O = refl
lteNTrue Z = refl
lteNTrue (S n) = lteNTrue n
total lteSuccZeroFalse : (n : Nat) -> lte (S n) O = False
lteSuccZeroFalse O = refl
total lteSuccZeroFalse : (n : Nat) -> lte (S n) Z = False
lteSuccZeroFalse Z = refl
lteSuccZeroFalse (S n) = refl
-- Minimum and maximum
total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = O
minimumZeroZeroRight O = refl
total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z
minimumZeroZeroRight Z = refl
minimumZeroZeroRight (S right) = minimumZeroZeroRight right
total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = O
minimumZeroZeroLeft O = refl
total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
minimumZeroZeroLeft Z = refl
minimumZeroZeroLeft (S left) = refl
total minimumSuccSucc : (left : Nat) -> (right : Nat) ->
minimum (S left) (S right) = S (minimum left right)
minimumSuccSucc O O = refl
minimumSuccSucc (S left) O = refl
minimumSuccSucc O (S right) = refl
minimumSuccSucc Z Z = refl
minimumSuccSucc (S left) Z = refl
minimumSuccSucc Z (S right) = refl
minimumSuccSucc (S left) (S right) =
let inductiveHypothesis = minimumSuccSucc left right in
?minimumSuccSuccStepCase
total minimumCommutative : (left : Nat) -> (right : Nat) ->
minimum left right = minimum right left
minimumCommutative O O = refl
minimumCommutative O (S right) = refl
minimumCommutative (S left) O = refl
minimumCommutative Z Z = refl
minimumCommutative Z (S right) = refl
minimumCommutative (S left) Z = refl
minimumCommutative (S left) (S right) =
let inductiveHypothesis = minimumCommutative left right in
?minimumCommutativeStepCase
total maximumZeroNRight : (right : Nat) -> maximum O right = right
maximumZeroNRight O = refl
total maximumZeroNRight : (right : Nat) -> maximum Z right = right
maximumZeroNRight Z = refl
maximumZeroNRight (S right) = refl
total maximumZeroNLeft : (left : Nat) -> maximum left O = left
maximumZeroNLeft O = refl
total maximumZeroNLeft : (left : Nat) -> maximum left Z = left
maximumZeroNLeft Z = refl
maximumZeroNLeft (S left) = refl
total maximumSuccSucc : (left : Nat) -> (right : Nat) ->
S (maximum left right) = maximum (S left) (S right)
maximumSuccSucc O O = refl
maximumSuccSucc (S left) O = refl
maximumSuccSucc O (S right) = refl
maximumSuccSucc Z Z = refl
maximumSuccSucc (S left) Z = refl
maximumSuccSucc Z (S right) = refl
maximumSuccSucc (S left) (S right) =
let inductiveHypothesis = maximumSuccSucc left right in
?maximumSuccSuccStepCase
total maximumCommutative : (left : Nat) -> (right : Nat) ->
maximum left right = maximum right left
maximumCommutative O O = refl
maximumCommutative (S left) O = refl
maximumCommutative O (S right) = refl
maximumCommutative Z Z = refl
maximumCommutative (S left) Z = refl
maximumCommutative Z (S right) = refl
maximumCommutative (S left) (S right) =
let inductiveHypothesis = maximumCommutative left right in
?maximumCommutativeStepCase
-- div and mod
total modZeroZero : (n : Nat) -> mod 0 n = O
modZeroZero O = refl
total modZeroZero : (n : Nat) -> mod 0 n = Z
modZeroZero Z = refl
modZeroZero (S n) = refl
--------------------------------------------------------------------------------
@ -613,7 +613,7 @@ powerSuccSuccMultStepCase = proof {
powerOneSuccOneStepCase = proof {
intros;
rewrite inductiveHypothesis;
rewrite sym (plusZeroRightNeutral (power (S O) exp));
rewrite sym (plusZeroRightNeutral (power (S Z) exp));
trivial;
}

6
lib/Prelude/Vect.idr
View File

@ -10,7 +10,7 @@ import Prelude.Nat
infixr 7 ::
data Vect : Type -> Nat -> Type where
Nil : Vect a O
Nil : Vect a Z
(::) : a -> Vect a n -> Vect a (S n)
--------------------------------------------------------------------------------
@ -81,7 +81,7 @@ fromList (x::xs) = x :: fromList xs
(++) (x::xs) ys = x :: xs ++ ys
replicate : (n : Nat) -> a -> Vect a n
replicate O x = []
replicate Z x = []
replicate (S k) x = x :: replicate k x
--------------------------------------------------------------------------------
@ -322,7 +322,7 @@ range =
reverse range_
where
range_ : Vect (Fin n) n
range_ {n=O} = Nil
range_ {n=Z} = Nil
range_ {n=(S _)} = last :: map weaken range_
--------------------------------------------------------------------------------

4
lib/Uninhabited.idr
View File

@ -3,10 +3,10 @@ module Uninhabited
class Uninhabited t where
total uninhabited : t -> _|_
instance Uninhabited (Fin O) where
instance Uninhabited (Fin Z) where
uninhabited fO impossible
uninhabited (fS f) impossible
instance Uninhabited (O = S n) where
instance Uninhabited (Z = S n) where
uninhabited refl impossible

4
samples/binary.idr
View File

@ -11,7 +11,7 @@ instance Show (Bit n) where
infixl 5 #
data Binary : (width : Nat) -> (value : Nat) -> Type where
zero : Binary O O
zero : Binary Z Z
(#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
instance Show (Binary w k) where
@ -83,7 +83,7 @@ main.adc_lemma_2 = proof {
rewrite sym (plusAssociative x v v1);
rewrite sym (plusCommutative (plus (plus x v) v1) v1);
rewrite plusZeroRightNeutral (plus (plus x v) v1);
rewrite sym (plusAssociative (plus x v) v1 (plus (plus (plus x v) v1) O));
rewrite sym (plusAssociative (plus x v) v1 (plus (plus (plus x v) v1) Z));
trivial;
}

6
src/IRTS/Compiler.hs
View File

@ -237,7 +237,7 @@ instance ToIR (TT Name) where
where mkUnused u i [] = []
mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
| otherwise = x : mkUnused u (i + 1) xs
-- ir' env (P _ (NS (UN "O") ["Nat", "Prelude"]) _)
-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
-- = return $ LConst (BI 0)
ir' env (P _ n _) = return $ LV (Glob n)
ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
@ -331,7 +331,7 @@ mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
zname = NS (UN "O") ["Nat","Prelude"]
zname = NS (UN "Z") ["Nat","Prelude"]
sname = NS (UN "S") ["Nat","Prelude"]
instance ToIR ([Name], SC) where
@ -351,7 +351,7 @@ instance ToIR SC where
return $ LCase (LV (Glob n)) alts'
ir' ImpossibleCase = return LNothing
-- special cases for O and S
-- special cases for Z and S
-- Needs rethink: projections make this fail
-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
-- = mkIRAlt n (ConstCase (BI 0) rhs)

4
src/Idris/AbsSyntaxTree.hs
View File

@ -1128,10 +1128,10 @@ showImp impl tm = se 10 tm where
xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"
slist _ _ = Nothing
-- since Prelude is always imported, S & O are unqualified iff they're the
-- since Prelude is always imported, S & Z are unqualified iff they're the
-- Nat ones.
snat p (PRef _ o)
| show o == (natns++"O") || show o == "O" = Just 0
| show o == (natns++"Z") || show o == "Z" = Just 0
snat p (PApp _ s [PExp {getTm=n}])
| show s == (natns++"S") || show s == "S",
Just n' <- snat p n

2
src/Idris/Transforms.hs
View File

@ -39,7 +39,7 @@ instance Transform CaseAlt where
natTrans = [TermTrans zero, TermTrans suc, CaseTrans natcase]
zname = NS (UN "O") ["Nat","Prelude"]
zname = NS (UN "Z") ["Nat","Prelude"]
sname = NS (UN "S") ["Nat","Prelude"]
zero :: TT Name -> TT Name

2
test/reg001/reg001.idr
View File

@ -8,4 +8,4 @@ data Imp : Type where
MkImp : {any : Type} -> any -> Imp
testVal : Imp
testVal = MkImp (apply id O)
testVal = MkImp (apply id Z)

4
test/reg004/reg004.idr
View File

@ -3,12 +3,12 @@ module Main
h : Bool -> Nat
h False = r1 where
r : Nat
r = S O
r = S Z
r1 : Nat
r1 = r
h True = r2 where
r : Nat
r = O
r = Z
r2 : Nat
r2 = r

6
test/reg005/reg005.idr
View File

@ -1,7 +1,7 @@
module Main
rep : (n : Nat) -> Char -> Vect Char n
rep O x = []
rep Z x = []
rep (S k) x = x :: rep k x
data RLE : Vect Char n -> Type where
@ -18,12 +18,12 @@ eq x y = if x == y then Just ?eqCharOK else Nothing
rle : (xs : Vect Char n) -> RLE xs
rle [] = REnd
rle (x :: xs) with (rle xs)
rle (x :: Vect.Nil) | REnd = RChar O x REnd
rle (x :: Vect.Nil) | REnd = RChar Z x REnd
rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)
rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just refl
= RChar (S n) x rs
rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing
= RChar O x (RChar n y rs)
= RChar Z x (RChar n y rs)
compress : Vect Char n -> String
compress xs with (rle xs)

2
test/reg006/reg006.idr
View File

@ -3,7 +3,7 @@ module RBTree
data Colour = Red | Black
data RBTree : Type -> Type -> Nat -> Colour -> Type where
Leaf : RBTree k v O Black
Leaf : RBTree k v Z Black
RedBranch : k -> v -> RBTree k v n Black -> RBTree k v n Black -> RBTree k v n Red
BlackBranch : k -> v -> RBTree k v n x -> RBTree k v n y -> RBTree k v (S n) Black

6
test/reg008/reg008.idr
View File

@ -6,9 +6,9 @@ data Cmp : Nat -> Nat -> Type where
cmpGT : (x : _) -> Cmp (y + S x) y
total cmp : (x, y : Nat) -> Cmp x y
cmp O O = cmpEQ
cmp O (S k) = cmpLT _
cmp (S k) O = cmpGT _
cmp Z Z = cmpEQ
cmp Z (S k) = cmpLT _
cmp (S k) Z = cmpGT _
cmp (S x) (S y) with (cmp x y)
cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k
cmp (S x) (S x) | cmpEQ = cmpEQ

2
test/reg009/reg009.lidr
View File

@ -6,7 +6,7 @@
> filterTagP : (p : alpha -> Bool) ->
> (as : Vect alpha n) ->
> so (isAnyBy p (n ** as)) ->
> (m : Nat ** (Vect (a : alpha ** so (p a)) m, so (m > O)))
> (m : Nat ** (Vect (a : alpha ** so (p a)) m, so (m > Z)))
> filterTagP {n = S m} p (a :: as) q with (p a)
> | True = (_
> **

2
test/reg010/reg010.idr
View File

@ -1,5 +1,5 @@
module usubst
total unsafeSubst : (P : a -> Type) -> (x : a) -> (y : a) -> P x -> P y
unsafeSubst P x y px with (O)
unsafeSubst P x y px with (Z)
unsafeSubst P x x px | _ = px

4
test/reg011/reg011.idr
View File

@ -1,9 +1,9 @@
vfoldl : (P : Nat -> Type) ->
((x : Nat) -> P x -> a -> P (S x)) -> P O
((x : Nat) -> P x -> a -> P (S x)) -> P Z
-> Vect a m -> P m
-- vfoldl P cons nil []
-- = nil
vfoldl P cons nil (x :: xs)
= vfoldl (\k => P (S k)) (\ n => cons (S n)) (cons O nil x) xs
= vfoldl (\k => P (S k)) (\ n => cons (S n)) (cons Z nil x) xs
-- vfoldl P cons nil (x :: xs)
-- = vfoldl (\n => P (S n)) (\ n => cons _) (cons _ nil x) xs

6
test/reg018/reg018b.idr
View File

@ -2,13 +2,13 @@ module A
%default total
codata B = O B | I B
codata B = Z B | I B
showB : B -> String
showB (I x) = "I" ++ showB x
showB (O x) = "O" ++ showB x
showB (Z x) = "Z" ++ showB x
instance Show B where show = showB
os : B
os = O os
os = Z os

2
test/reg018/reg018c.idr
View File

@ -9,7 +9,7 @@ codata InfStream a = (::) a (InfStream a)
-- natFromStream n = (::) n (natFromStream (S n))
take : (n: Nat) -> InfStream a -> Vect a n
take O _ = []
take Z _ = []
take (S n) (x :: xs) = x :: take n xs
hdtl : InfStream a -> (a, InfStream a)

2
test/reg018/reg018d.idr
View File

@ -2,7 +2,7 @@ module Main
total
pull : Fin (S n) -> Vect a (S n) -> (a, Vect a n)
pull {n=O} _ (x :: xs) = (x, xs)
pull {n=Z} _ (x :: xs) = (x, xs)
-- pull {n=S q} fO (Vect.(::) {n=S _} x xs) = (x, xs)
pull {n=S _} (fS n) (x :: xs) =
let (v, vs) = pull n xs in

2
test/test005/test005.idr
View File

@ -8,7 +8,7 @@ tlist = [1, 2, 3, 4, 5]
main : IO ()
main = do print (abs (-8))
print (abs (S O))
print (abs (S Z))
print (span isAlpha tstr)
print (break isDigit tstr)
print (span (\x => x < 3) tlist)

6
test/test006/test006.idr
View File

@ -5,14 +5,14 @@ data Parity : Nat -> Type where
odd : Parity (S (n + n))
parity : (n:Nat) -> Parity n
parity O = even {n=O}
parity (S O) = odd {n=O}
parity Z = even {n=Z}
parity (S Z) = odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | (even {n = j}) ?= even {n=S j}
parity (S (S (S (j + j)))) | (odd {n = j}) ?= odd {n=S j}
natToBin : Nat -> List Bool
natToBin O = Nil
natToBin Z = Nil
natToBin k with (parity k)
natToBin (j + j) | even {n = j} = False :: natToBin j
natToBin (S (j + j)) | odd {n = j} = True :: natToBin j

4
test/test015/Parity.idr
View File

@ -5,8 +5,8 @@ data Parity : Nat -> Type where
odd : Parity (S (n + n))
parity : (n:Nat) -> Parity n
parity O = even {n=O}
parity (S O) = odd {n=O}
parity Z = even {n=Z}
parity (S Z) = odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | even ?= even {n=S j}
parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

12
test/test015/test015.idr
View File

@ -4,8 +4,8 @@ import Parity
import System
data Bit : Nat -> Type where
b0 : Bit O
b1 : Bit (S O)
b0 : Bit Z
b1 : Bit (S Z)
instance Show (Bit n) where
show = show' where
@ -16,7 +16,7 @@ instance Show (Bit n) where
infixl 5 #
data Binary : (width : Nat) -> (value : Nat) -> Type where
zero : Binary O O
zero : Binary Z Z
(#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
instance Show (Binary w k) where
@ -29,9 +29,9 @@ pad (num # x) = pad num # x
natToBin : (width : Nat) -> (n : Nat) ->
Maybe (Binary width n)
natToBin O (S k) = Nothing
natToBin O O = Just zero
natToBin (S k) O = do x <- natToBin k O
natToBin Z (S k) = Nothing
natToBin Z Z = Just zero
natToBin (S k) Z = do x <- natToBin k Z
Just (pad x)
natToBin (S w) (S k) with (parity k)
natToBin (S w) (S (plus j j)) | even = do jbin <- natToBin w j

2
test/test016/test016.idr
View File

@ -8,7 +8,7 @@ countFrom : Int -> Stream Int
countFrom x = x :: countFrom (x + 1)
take : Nat -> Stream a -> List a
take O _ = []
take Z _ = []
take (S n) (x :: xs) = x :: take n xs
take n [] = []

32
test/test017/test017.idr
View File

@ -5,8 +5,8 @@ module scg
data Ord = Zero | Suc Ord | Sup (Nat -> Ord)
natElim : (n : Nat) -> (P : Nat -> Type) ->
(P O) -> ((n : Nat) -> (P n) -> (P (S n))) -> (P n)
natElim O P mO mS = mO
(P Z) -> ((n : Nat) -> (P n) -> (P (S n))) -> (P n)
natElim Z P mO mS = mO
natElim (S k) P mO mS = mS k (natElim k P mO mS)
ordElim : (x : Ord) ->
@ -23,10 +23,10 @@ ordElim (Sup f) P mZ mSuc mSup =
myplus' : Nat -> Nat -> Nat
myplus : Nat -> Nat -> Nat
myplus O y = y
myplus Z y = y
myplus (S k) y = S (myplus' k y)
myplus' O y = y
myplus' Z y = y
myplus' (S k) y = S (myplus y k)
mnubBy : (a -> a -> Bool) -> List a -> List a
@ -46,23 +46,23 @@ vtrans [] _ = []
vtrans (x :: xs) ys = x :: vtrans ys ys
even : Nat -> Bool
even O = True
even Z = True
even (S k) = odd k
where
odd : Nat -> Bool
odd O = False
odd Z = False
odd (S k) = even k
ack : Nat -> Nat -> Nat
ack O n = S n
ack (S m) O = ack m (S O)
ack Z n = S n
ack (S m) Z = ack m (S Z)
ack (S m) (S n) = ack m (ack (S m) n)
data Bin = eps | c0 Bin | c1 Bin
foo : Bin -> Nat
foo eps = O
foo (c0 eps) = O
foo eps = Z
foo (c0 eps) = Z
foo (c0 (c1 x)) = S (foo (c1 x))
foo (c0 (c0 x)) = foo (c0 x)
foo (c1 x) = S (foo x)
@ -70,19 +70,19 @@ foo (c1 x) = S (foo x)
bar : Nat -> Nat -> Nat
bar x y = mp x y where
mp : Nat -> Nat -> Nat
mp O y = y
mp Z y = y
mp (S k) y = S (bar k y)
total mfib : Nat -> Nat
mfib O = O
mfib (S O) = S O
mfib Z = Z
mfib (S Z) = S Z
mfib (S (S n)) = mfib (S n) + mfib n
maxCommutative : (left : Nat) -> (right : Nat) ->
maximum left right = maximum right left
maxCommutative O O = refl
maxCommutative (S left) O = refl
maxCommutative O (S right) = refl
maxCommutative Z Z = refl
maxCommutative (S left) Z = refl
maxCommutative Z (S right) = refl
maxCommutative (S left) (S right) =
let inductiveHypothesis = maxCommutative left right in
?maxCommutativeStepCase

2
test/test019/test019.lidr
View File

@ -1,7 +1,7 @@
> module Main
> ifTrue : so True -> Nat
> ifTrue oh = S O
> ifTrue oh = S Z
> ifFalse : so False -> Nat
> ifFalse oh impossible

4
test/test025/test025.idr
View File

@ -21,9 +21,9 @@ testMemory = do Src :- allocate 5
Dst :- initialize (prim__truncInt_B8 1) 2 oh
move 2 2 3 oh oh
Src :- free
end <- Dst :- peek 4 (S O) oh
end <- Dst :- peek 4 (S Z) oh
Dst :- poke 4 (sub1 end) oh
res <- Dst :- peek 1 (S(S(S(S O)))) oh
res <- Dst :- peek 1 (S(S(S(S Z)))) oh
Dst :- free
return (map (prim__zextB8_Int) res)

16
tutorial/classes.tex
View File

@ -43,10 +43,10 @@ could be defined as:
\begin{SaveVerbatim}{shownat}
instance Show Nat where
show O = "O"
show Z = "Z"
show (S k) = "s" ++ show k
Idris> show (S (S (S O)))
Idris> show (S (S (S Z)))
"sssO" : String
\end{SaveVerbatim}
@ -101,10 +101,10 @@ For example, for an instance of \texttt{Eq} for \texttt{Nat}:
\begin{SaveVerbatim}{eqnat}
instance Eq Nat where
O == O = True
Z == Z = True
(S x) == (S y) = x == y
O == (S y) = False
(S x) == O = False
Z == (S y) = False
(S x) == Z = False
x /= y = not (x == y)
@ -498,9 +498,9 @@ be \remph{named} as follows:
\begin{SaveVerbatim}{myord}
instance [myord] Ord Nat where
compare O (S n) = GT
compare (S n) O = LT
compare O O = EQ
compare Z (S n) = GT
compare (S n) Z = LT
compare Z Z = EQ
compare (S x) (S y) = compare @{myord} x y
\end{SaveVerbatim}

12
tutorial/examples/binary.idr
View File

@ -1,7 +1,7 @@
module Main
data Binary : Nat -> Type where
bEnd : Binary O
bEnd : Binary Z
bO : Binary n -> Binary (n + n)
bI : Binary n -> Binary (S (n + n))
@ -15,21 +15,21 @@ data Parity : Nat -> Type where
odd : Parity (S (n + n))
parity : (n:Nat) -> Parity n
parity O = even {n=O}
parity (S O) = odd {n=O}
parity Z = even {n=Z}
parity (S Z) = odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | even ?= even {n=S j}
parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
natToBin : (n:Nat) -> Binary n
natToBin O = bEnd
natToBin Z = bEnd
natToBin (S k) with (parity k)
natToBin (S (j + j)) | even = bI (natToBin j)
natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
intToNat : Int -> Nat
intToNat 0 = O
intToNat x = if (x>0) then (S (intToNat (x-1))) else O
intToNat 0 = Z
intToNat x = if (x>0) then (S (intToNat (x-1))) else Z
main : IO ()
main = do putStr "Enter a number: "

28
tutorial/examples/theorems.idr
View File

@ -5,15 +5,15 @@ fiveIsFive = refl
twoPlusTwo : 2 + 2 = 4
twoPlusTwo = refl
total disjoint : (n : Nat) -> O = S n -> _|_
total disjoint : (n : Nat) -> Z = S n -> _|_
disjoint n p = replace {P = disjointTy} p ()
where
disjointTy : Nat -> Type
disjointTy O = ()
disjointTy Z = ()
disjointTy (S k) = _|_
total acyclic : (n : Nat) -> n = S n -> _|_
acyclic O p = disjoint _ p
acyclic Z p = disjoint _ p
acyclic (S k) p = acyclic k (succInjective _ _ p)
empty1 : _|_
@ -24,33 +24,33 @@ empty1 = hd [] where
empty2 : _|_
empty2 = empty2
plusReduces : (n:Nat) -> plus O n = n
plusReduces : (n:Nat) -> plus Z n = n
plusReduces n = refl
plusReducesO : (n:Nat) -> n = plus n O
plusReducesO O = refl
plusReducesO (S k) = cong (plusReducesO k)
plusReducesZ : (n:Nat) -> n = plus n Z
plusReducesZ Z = refl
plusReducesZ (S k) = cong (plusReducesZ k)
plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
plusReducesS O m = refl
plusReducesS Z m = refl
plusReducesS (S k) m = cong (plusReducesS k m)
plusReducesO' : (n:Nat) -> n = plus n O
plusReducesO' O = ?plusredO_O
plusReducesO' (S k) = let ih = plusReducesO' k in
?plusredO_S
plusReducesZ' : (n:Nat) -> n = plus n Z
plusReducesZ' Z = ?plusredZ_Z
plusReducesZ' (S k) = let ih = plusReducesZ' k in
?plusredZ_S
---------- Proofs ----------
plusredO_S = proof {
plusredZ_S = proof {
intro;
intro;
rewrite ih;
trivial;
}
plusredO_O = proof {
plusredZ_Z = proof {
compute;
trivial;
}

2
tutorial/examples/usefultypes.idr
View File

@ -10,7 +10,7 @@ vec = (_ ** [3, 4])
list_lookup : Nat -> List a -> Maybe a
list_lookup _ Nil = Nothing
list_lookup O (x :: xs) = Just x
list_lookup Z (x :: xs) = Just x
list_lookup (S k) (x :: xs) = list_lookup k xs
lookup_default : Nat -> List a -> a -> a

6
tutorial/examples/views.idr
View File

@ -5,14 +5,14 @@ data Parity : Nat -> Type where
odd : Parity (S (n + n))
parity : (n:Nat) -> Parity n
parity O = even {n=O}
parity (S O) = odd {n=O}
parity Z = even {n=Z}
parity (S Z) = odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | even ?= even {n=S j}
parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
natToBin : Nat -> List Bool
natToBin O = Nil
natToBin Z = Nil
natToBin k with (parity k)
natToBin (j + j) | even = False :: natToBin j
natToBin (S (j + j)) | odd = True :: natToBin j

6
tutorial/examples/wheres.idr
View File

@ -1,13 +1,13 @@
module wheres
even : Nat -> Bool
even O = True
even Z = True
even (S k) = odd k where
odd O = False
odd Z = False
odd (S k) = even k
test : List Nat
test = [c (S 1), c O, d (S O)]
test = [c (S 1), c Z, d (S Z)]
where c x = 42 + x
d y = c (y + 1 + z y)
where z w = y + w

12
tutorial/provisional.tex
View File

@ -22,8 +22,8 @@ We'd like to implement this as follows:
\begin{SaveVerbatim}{parfail}
parity : (n:Nat) -> Parity n
parity O = even {n=O}
parity (S O) = odd {n=O}
parity Z = even {n=Z}
parity (S Z) = odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | even = even {n=S j}
parity (S (S (S (j + j)))) | odd = odd {n=S j}
@ -77,8 +77,8 @@ except that they introduce the right hand side with a \texttt{?=} rathar than
\begin{SaveVerbatim}{paritypro}
parity : (n:Nat) -> Parity n
parity O = even {n=O}
parity (S O) = odd {n=O}
parity Z = even {n=Z}
parity (S Z) = odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | even ?= even {n=S j}
parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
@ -231,7 +231,7 @@ case \texttt{Nat}):
\begin{SaveVerbatim}{bindef}
data Binary : Nat -> Type where
bEnd : Binary O
bEnd : Binary Z
bO : Binary n -> Binary (n + n)
bI : Binary n -> Binary (S (n + n))
@ -263,7 +263,7 @@ provisional definition in the odd case:
\begin{SaveVerbatim}{ntbdef}
natToBin : (n:Nat) -> Binary n
natToBin O = bEnd
natToBin Z = bEnd
natToBin (S k) with (parity k)
natToBin (S (j + j)) | even = bI (natToBin j)
natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))

92
tutorial/theorems.tex
View File

@ -42,11 +42,11 @@ to a successor:
\begin{SaveVerbatim}{natdisjoint}
disjoint : (n : Nat) -> O = S n -> _|_
disjoint : (n : Nat) -> Z = S n -> _|_
disjoint n p = replace {P = disjointTy} p ()
where
disjointTy : Nat -> Type
disjointTy O = ()
disjointTy Z = ()
disjointTy (S k) = _|_
\end{SaveVerbatim}
@ -76,7 +76,7 @@ we want to prove the following theorem about the reduction behaviour of \texttt{
\begin{SaveVerbatim}{plusred}
plusReduces : (n:Nat) -> plus O n = n
plusReduces : (n:Nat) -> plus Z n = n
\end{SaveVerbatim}
\useverb{plusred}
@ -90,7 +90,7 @@ of interest.
We won't go into details here, but the Curry-Howard
correspondence~\cite{howard} explains this relationship.
The proof itself is trivial, because \texttt{plus O n} normalises to \texttt{n}
The proof itself is trivial, because \texttt{plus Z n} normalises to \texttt{n}
by the definition of \texttt{plus}:
\begin{SaveVerbatim}{plusredp}
@ -107,9 +107,9 @@ on the first argument to \texttt{plus}, namely \texttt{n}.
\begin{SaveVerbatim}{plusRedO}
plusReducesO : (n:Nat) -> n = plus n O
plusReducesO O = refl
plusReducesO (S k) = cong (plusReducesO k)
plusReducesZ : (n:Nat) -> n = plus n Z
plusReducesZ Z = refl
plusReducesZ (S k) = cong (plusReducesZ k)
\end{SaveVerbatim}
\useverb{plusRedO}
@ -131,7 +131,7 @@ We can do the same for the reduction behaviour of plus on successors:
\begin{SaveVerbatim}{plusRedS}
plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
plusReducesS O m = refl
plusReducesS Z m = refl
plusReducesS (S k) m = cong (plusReducesS k m)
\end{SaveVerbatim}
@ -148,16 +148,16 @@ therefore provides an interactive proof mode.
Instead of writing the proof in one go, we can use \Idris{}'s interactive
proof mode. To do this, we write the general \emph{structure} of the proof,
and use the interactive mode to complete the details. We'll be constructing
the proof by \emph{induction}, so we write the cases for \texttt{O} and
the proof by \emph{induction}, so we write the cases for \texttt{Z} and
\texttt{S}, with a recursive call in the \texttt{S} case giving the inductive
hypothesis, and insert \emph{metavariables} for the rest of the definition:
\begin{SaveVerbatim}{prOstruct}
plusReducesO' : (n:Nat) -> n = plus n O
plusReducesO' O = ?plusredO_O
plusReducesO' (S k) = let ih = plusReducesO' k in
?plusredO_S
plusReducesZ' : (n:Nat) -> n = plus n Z
plusReducesZ' Z = ?plusredZ_Z
plusReducesZ' (S k) = let ih = plusReducesZ' k in
?plusredZ_S
\end{SaveVerbatim}
\useverb{prOstruct}
@ -173,17 +173,17 @@ precisely, which functions exist but have no definitions), then the
*theorems> :m
Global metavariables:
[plusredO_S,plusredO_O]
[plusredZ_S,plusredZ_Z]
\end{SaveVerbatim}
\begin{SaveVerbatim}{metatypes}
*theorems> :t plusredO_O
plusredO_O : O = plus O O
*theorems> :t plusredZ_Z
plusredZ_Z : Z = plus Z Z
*theorems> :t plusredO_S
plusredO_S : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)
*theorems> :t plusredZ_S
plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = S (plus k Z)
\end{SaveVerbatim}
\useverb{showmetas}
@ -196,10 +196,10 @@ the missing definitions.
\begin{SaveVerbatim}{proveO}
*theorems> :p plusredO_O
*theorems> :p plusredZ_Z
---------------------------------- (plusredO_O) --------
{hole0} : O = plus O O
---------------------------------- (plusredZ_Z) --------
{hole0} : Z = plus Z Z
\end{SaveVerbatim}
\useverb{proveO}
@ -213,24 +213,24 @@ we can normalise the goal with the \texttt{compute} tactic:
\begin{SaveVerbatim}{compute}
-plusredO_O> compute
-plusredZ_Z> compute
---------------------------------- (plusredO_O) --------
{hole0} : O = O
---------------------------------- (plusredZ_Z) --------
{hole0} : Z = Z
\end{SaveVerbatim}
\useverb{compute}
\noindent
Now we have to prove that \texttt{O} equals \texttt{O}, which is easy to prove by
Now we have to prove that \texttt{Z} equals \texttt{Z}, which is easy to prove by
\texttt{refl}. To apply a function, such as \texttt{refl}, we use \texttt{refine}
which introduces subgoals for each of the function's explicit arguments (\texttt{refl}
has none):
\begin{SaveVerbatim}{refrefl}
-plusredO_O> refine refl
plusredO_O: no more goals
-plusredZ_Z> refine refl
plusredZ_Z: no more goals
\end{SaveVerbatim}
\useverb{refrefl}
@ -244,8 +244,8 @@ This also outputs a trace of the proof:
\begin{SaveVerbatim}{prOprooftrace}
-plusredO_O> qed
plusredO_O = proof {
-plusredZ_Z> qed
plusredZ_Z = proof {
compute;
refine refl;
}
@ -257,7 +257,7 @@ plusredO_O = proof {
*theorems> :m
Global metavariables:
[plusredO_S]
[plusredZ_S]
\end{SaveVerbatim}
\useverb{showmetasO}
@ -269,10 +269,10 @@ Let us now prove the other required lemma, \texttt{plusredO\_S}:
\begin{SaveVerbatim}{plusredOSprf}
*theorems> :p plusredO_S
*theorems> :p plusredZ_S
---------------------------------- (plusredO_S) --------
{hole0} : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)
---------------------------------- (plusredZ_S) --------
{hole0} : (k : Nat) -> (k = plus k Z) -> S k = S (plus k Z)
\end{SaveVerbatim}
\useverb{plusredOSprf}
@ -286,28 +286,28 @@ twice (or \texttt{intros}, which introduces all arguments as premisses). This gi
\begin{SaveVerbatim}{prSintros}
k : Nat
ih : k = plus k O
---------------------------------- (plusredO_S) --------
{hole2} : S k = S (plus k O)
ih : k = plus k Z
---------------------------------- (plusredZ_S) --------
{hole2} : S k = S (plus k Z)
\end{SaveVerbatim}
\useverb{prSintros}
\noindent
We know, from the type of \texttt{ih}, that \texttt{k = plus k O}, so we would like to
use this knowledge to replace \texttt{plus k O} in the goal with \texttt{k}. We can
We know, from the type of \texttt{ih}, that \texttt{k = plus k Z}, so we would like to
use this knowledge to replace \texttt{plus k Z} in the goal with \texttt{k}. We can
achieve this with the \texttt{rewrite} tactic:
\begin{SaveVerbatim}{}
-plusredO_S> rewrite ih
-plusredZ_S> rewrite ih
k : Nat
ih : k = plus k O
---------------------------------- (plusredO_S) --------
ih : k = plus k Z
---------------------------------- (plusredZ_S) --------
{hole3} : S k = S k
-plusredO_S>
-plusredZ_S>
\end{SaveVerbatim}
\useverb{}
@ -318,10 +318,10 @@ the goal using that proof. Here, it results in an equality which is trivially pr
\begin{SaveVerbatim}{prOStrace}
-plusredO_S> trivial
plusredO_S: no more goals
-plusredO_S> qed
plusredO_S = proof {
-plusredZ_S> trivial
plusredZ_S: no more goals
-plusredZ_S> qed
plusredZ_S = proof {
intros;
rewrite ih;
trivial;

46
tutorial/typesfuns.tex
View File

@ -81,7 +81,7 @@ syntax. Natural numbers and lists, for example, can be declared as follows:
\begin{SaveVerbatim}{natlist}
data Nat = O | S Nat -- Natural numbers
data Nat = Z | S Nat -- Natural numbers
-- (zero and successor)
data List a = Nil | (::) a (List a) -- Polymorphic lists
@ -90,7 +90,7 @@ data List a = Nil | (::) a (List a) -- Polymorphic lists
\noindent
The above declarations are taken from the standard library. Unary natural
numbers can be either zero (\texttt{O} - that's a capital letter 'o', not the digit), or
numbers can be either zero (\texttt{Z}), or
the successor of another natural number (\texttt{S k}).
Lists can either be empty (\texttt{Nil})
or a value added to the front of another list (\texttt{x :: xs}).
@ -132,12 +132,12 @@ defined as follows, again taken from the standard library:
-- Unary addition
plus : Nat -> Nat -> Nat
plus O y = y
plus Z y = y
plus (S k) y = S (plus k y)
-- Unary multiplication
mult : Nat -> Nat -> Nat
mult O y = O
mult Z y = Z
mult (S k) y = plus y (mult k y)
\end{SaveVerbatim}
@ -148,7 +148,7 @@ The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
for use by \texttt{Nat}, and are implemented
using the above functions. Unlike Haskell, there is no restriction on whether
types and function names must begin with a capital letter or not. Function
names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},
names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{Z}, \tDC{S},
\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are
all part of the same namespace.
@ -156,10 +156,10 @@ We can test these functions at the \Idris{} prompt:
\begin{SaveVerbatim}{fntest}
Idris> plus (S (S O)) (S (S O))
S (S (S (S O))) : Nat
Idris> mult (S (S (S O))) (plus (S (S O)) (S (S O)))
S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
Idris> plus (S (S Z)) (S (S Z))
S (S (S (S Z))) : Nat
Idris> mult (S (S (S Z))) (plus (S (S Z)) (S (S Z)))
S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat
\end{SaveVerbatim}
\useverb{fntest}
@ -171,9 +171,9 @@ meaning that we can also test the functions as follows:
\begin{SaveVerbatim}{fntest}
Idris> plus 2 2
S (S (S (S O))) : Nat
S (S (S (S Z))) : Nat
Idris> mult 3 (plus 2 2)
S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))) : Nat
\end{SaveVerbatim}
\useverb{fntest}
@ -252,13 +252,13 @@ So, for example, the following definitions are legal:
\begin{SaveVerbatim}{whereinfer}
even : Nat -> Bool
even O = True
even Z = True
even (S k) = odd k where
odd O = False
odd Z = False
odd (S k) = even k
test : List Nat
test = [c (S 1), c O, d (S O)]
test = [c (S 1), c Z, d (S Z)]
where c x = 42 + x
d y = c (y + 1 + z y)
where z w = y + w
@ -278,7 +278,7 @@ we declare vectors as follows:
\begin{SaveVerbatim}{vect}
data Vect : Type -> Nat -> Type where
Nil : Vect a O
Nil : Vect a Z
(::) : a -> Vect a k -> Vect a (S k)
\end{SaveVerbatim}
@ -371,7 +371,7 @@ data Fin : Nat -> Type where
\texttt{n+1}th element of a finite set with \texttt{S k} elements.
\tTC{Fin} is indexed by a \tTC{Nat}, which
represents the number of elements in the set. Obviously we can't construct an
element of an empty set, so neither constructor targets \texttt{Fin O}.
element of an empty set, so neither constructor targets \texttt{Fin Z}.
A useful application of the \tTC{Fin} family is to represent bounded
natural numbers. Since the first \tTC{n} natural numbers form a finite
@ -397,10 +397,10 @@ need for a run-time bounds check. The type checker guarantees that the location
is no larger than the length of the vector.
Note also that there is no case for \texttt{Nil} here. This is because it is
impossible. Since there is no element of \texttt{Fin O}, and the location is a
\texttt{Fin n}, then \texttt{n} can not be \tDC{O}. As a result, attempting to
impossible. Since there is no element of \texttt{Fin Z}, and the location is a
\texttt{Fin n}, then \texttt{n} can not be \tDC{Z}. As a result, attempting to
look up an element in an empty vector would give a compile time type error,
since it would force \texttt{n} to be \tDC{O}.
since it would force \texttt{n} to be \tDC{Z}.
\subsubsection{Implicit Arguments}
@ -520,11 +520,11 @@ data types and functions to be defined simultaneously:
mutual
even : Nat -> Bool
even O = True
even Z = True
even (S k) = odd k
odd : Nat -> Bool
odd O = False
odd Z = False
odd (S k) = even k
\end{SaveVerbatim}
@ -663,7 +663,7 @@ We have already seen the \texttt{List} and \texttt{Vect} data types:
data List a = Nil | (::) a (List a)
data Vect : Type -> Nat -> Type where
Nil : Vect a O
Nil : Vect a Z
(::) : a -> Vect a k -> Vect a (S k)
\end{SaveVerbatim}
@ -787,7 +787,7 @@ bounds error:
list_lookup : Nat -> List a -> Maybe a
list_lookup _ Nil = Nothing
list_lookup O (x :: xs) = Just x
list_lookup Z (x :: xs) = Just x
list_lookup (S k) (x :: xs) = list_lookup k xs
\end{SaveVerbatim}

4
tutorial/views.tex
View File

@ -10,7 +10,7 @@ determined by whether the vector was empty or not:
\begin{SaveVerbatim}{appdep}
(++) : Vect a n -> Vect a m -> Vect a (n + m)
(++) {n=O} [] ys = ys
(++) {n=Z} [] ys = ys
(++) {n=S k} (x :: xs) ys = x :: xs ++ ys
\end{SaveVerbatim}
@ -83,7 +83,7 @@ to write a function which converts a natural number to a list of binary digits
\begin{SaveVerbatim}{natToBin}
natToBin : Nat -> List Bool
natToBin O = Nil
natToBin Z = Nil
natToBin k with (parity k)
natToBin (j + j) | even = False :: natToBin j
natToBin (S (j + j)) | odd = True :: natToBin j