faf04f3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

rename fO into fZ

commitfaf04f3d28b81d6e906f13cd58647b88908f3b97 authorraichoo <raichoo@googlemail.com> dateFri 26 Jul 2013, 21:14 (13 years ago) parent2311d55

16 files changed+50−50

compare with master

unifiedsplit

javascript/JavaScript/JSON.idr+1−1 lib/Data/Bits.idr+1−1 lib/Data/BoundedList.idr+2−2 lib/Data/HVect.idr+4−4 lib/Decidable/Equality.idr+5−5 lib/Prelude/Fin.idr+8−8 lib/Prelude/Vect.idr+6−6 lib/Uninhabited.idr+1−1 samples/interp-alt.idr+11−11 samples/interp.idr+1−1 test/reg018/reg018d.idr+2−2 test/test001/test001.idr+2−2 test/test014/Resimp.idr+1−1 tutorial/examples/interp.idr+1−1 tutorial/interp.tex+2−2 tutorial/typesfuns.tex+2−2

javascript/JavaScript/JSON.idr+1−1

@@ -33,7 +33,7 @@ mutual

3333 JSObject : JObject fs -> JSON (JSONObject fs)

3434

3535index : (i : Fin n) -> JSON (JSONArray n ts) -> JSON (index i ts)

36−index fO (JSArray (x :: xs)) = x

36+index fZ (JSArray (x :: xs)) = x

3737index (fS i) (JSArray (x :: xs)) = index i (JSArray xs)

3838

3939infixl 8 ++

lib/Data/Bits.idr+1−1

@@ -434,7 +434,7 @@ bitsToStr x = pack (helper last x)

434434 where

435435 %assert_total

436436 helper : Fin (S n) -> Bits n -> List Char

437− helper fO _ = []

437+ helper fZ _ = []

438438 helper (fS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b

439439

440440instance Show (Bits n) where

lib/Data/BoundedList.idr+2−2

@@ -8,7 +8,7 @@ data BoundedList : Type -> Nat -> Type where

88 (::) : a -> BoundedList a n -> BoundedList a (S n)

1010length : BoundedList a n -> Fin (S n)

11−length [] = fO

11+length [] = fZ

1212length (x :: xs) = fS (length xs)

1313

1414--------------------------------------------------------------------------------

@@ -17,7 +17,7 @@ length (x :: xs) = fS (length xs)

1717

1818index : Fin (S n) -> BoundedList a n -> Maybe a

1919index _ [] = Nothing

20−index fO (x :: _) = Just x

20+index fZ (x :: _) = Just x

2121index (fS f) (_ :: xs) = index f xs

2222

2323--------------------------------------------------------------------------------

lib/Data/HVect.idr+4−4

@@ -11,20 +11,20 @@ using (k : Nat, ts : Vect Type k)

1111 (::) : t -> HVect ts -> HVect (t::ts)

1212

1313 index : (i : Fin k) -> HVect ts -> index i ts

14− index fO (x::xs) = x

14+ index fZ (x::xs) = x

1515 index (fS j) (x::xs) = index j xs

1616

1717 deleteAt : {us : Vect Type (S l)} -> (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)

18− deleteAt fO (x::xs) = xs

18+ deleteAt fZ (x::xs) = xs

1919 deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs

2020 deleteAt _ [] impossible

2121

2222 replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)

23− replaceAt fO y (x::xs) = y::xs

23+ replaceAt fZ y (x::xs) = y::xs

2424 replaceAt (fS j) y (x::xs) = x :: replaceAt j y xs

2525

2626 updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)

27− updateAt fO f (x::xs) = f x :: xs

27+ updateAt fZ f (x::xs) = f x :: xs

2828 updateAt (fS j) f (x::xs) = x :: updateAt j f xs

2929

3030 (++) : {us : Vect Type l} -> HVect ts -> HVect us -> HVect (ts ++ us)

lib/Decidable/Equality.idr+5−5

@@ -88,13 +88,13 @@ instance (DecEq a, DecEq b) => DecEq (Either a b) where

8888-- Fin

8989--------------------------------------------------------------------------------

9090

91−total fONotfS : {f : Fin n} -> fO {k = n} = fS f -> _|_

92−fONotfS refl impossible

91+total fZNotfS : {f : Fin n} -> fZ {k = n} = fS f -> _|_

92+fZNotfS refl impossible

9393

9494instance DecEq (Fin n) where

95− decEq fO fO = Yes refl

96− decEq fO (fS f) = No fONotfS

97− decEq (fS f) fO = No $ negEqSym fONotfS

95+ decEq fZ fZ = Yes refl

96+ decEq fZ (fS f) = No fZNotfS

97+ decEq (fS f) fZ = No $ negEqSym fZNotfS

9898 decEq (fS f) (fS f') with (decEq f f')

9999 | Yes p = Yes $ cong p

100100 | No p = No $ \h => p $ fSinjective {f = f} {f' = f'} h

lib/Prelude/Fin.idr+8−8

@@ -4,41 +4,41 @@ import Prelude.Nat

44import Prelude.Either

66data Fin : Nat -> Type where

7− fO : Fin (S k)

7+ fZ : Fin (S k)

88 fS : Fin k -> Fin (S k)

1010instance Eq (Fin n) where

11− (==) fO fO = True

11+ (==) fZ fZ = True

1212 (==) (fS k) (fS k') = k == k'

1313 (==) _ _ = False

1414

1515finToNat : Fin n -> Nat -> Nat

16−finToNat fO a = a

16+finToNat fZ a = a

1717finToNat (fS x) a = finToNat x (S a)

1818

1919instance Cast (Fin n) Nat where

2020 cast x = finToNat x Z

2121

2222finToInt : Fin n -> Integer -> Integer

23−finToInt fO a = a

23+finToInt fZ a = a

2424finToInt (fS x) a = finToInt x (a + 1)

2525

2626instance Cast (Fin n) Integer where

2727 cast x = finToInt x 0

2828

2929weaken : Fin n -> Fin (S n)

30−weaken fO = fO

30+weaken fZ = fZ

3131weaken (fS k) = fS (weaken k)

3232

3333strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)

34−strengthen {n = S k} fO = Right fO

34+strengthen {n = S k} fZ = Right fZ

3535strengthen {n = S k} (fS i) with (strengthen i)

3636 strengthen (fS k) | Left x = Left (fS x)

3737 strengthen (fS k) | Right x = Right (fS x)

3838strengthen f = Left f

3939

4040last : Fin (S n)

41−last {n=Z} = fO

41+last {n=Z} = fZ

4242last {n=S _} = fS last

4343

4444total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'

@@ -48,7 +48,7 @@ fSinjective refl = refl

4848-- Construct a Fin from an integer literal which must fit in the given Fin

4949

5050natToFin : Nat -> (n : Nat) -> Maybe (Fin n)

51−natToFin Z (S j) = Just fO

51+natToFin Z (S j) = Just fZ

5252natToFin (S k) (S j) with (natToFin k j)

5353 | Just k' = Just (fS k')

5454 | Nothing = Nothing

lib/Prelude/Vect.idr+6−6

@@ -32,17 +32,17 @@ init (x::[]) = []

3232init (x::y::ys) = x :: init (y::ys)

3333

3434index : Fin n -> Vect a n -> a

35−index fO (x::xs) = x

35+index fZ (x::xs) = x

3636index (fS k) (x::xs) = index k xs

37−index fO [] impossible

37+index fZ [] impossible

3838

3939deleteAt : Fin (S n) -> Vect a (S n) -> Vect a n

40−deleteAt fO (x::xs) = xs

40+deleteAt fZ (x::xs) = xs

4141deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs

4242deleteAt _ [] impossible

4343

4444replaceAt : Fin n -> t -> Vect t n -> Vect t n

45−replaceAt fO y (x::xs) = y::xs

45+replaceAt fZ y (x::xs) = y::xs

4646replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs

4747

4848--------------------------------------------------------------------------------

@@ -50,13 +50,13 @@ replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs

5050--------------------------------------------------------------------------------

5151

5252take : Fin n -> Vect a n -> (p ** Vect a p)

53−take fO xs = (_ ** [])

53+take fZ xs = (_ ** [])

5454take (fS k) [] impossible

5555take (fS k) (x::xs) with (take k xs)

5656 | (_ ** tail) = (_ ** x::tail)

5757

5858drop : Fin n -> Vect a n -> (p ** Vect a p)

59−drop fO xs = (_ ** xs)

59+drop fZ xs = (_ ** xs)

6060drop (fS k) [] impossible

6161drop (fS k) (x::xs) = drop k xs

6262

lib/Uninhabited.idr+1−1

@@ -4,7 +4,7 @@ class Uninhabited t where

44 total uninhabited : t -> _|_

66instance Uninhabited (Fin Z) where

7− uninhabited fO impossible

7+ uninhabited fZ impossible

88 uninhabited (fS f) impossible

1010instance Uninhabited (Z = S n) where

samples/interp-alt.idr+11−11

@@ -14,11 +14,11 @@ using (G : Vect Ty n)

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

1515

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

17−-- stop : HasType fO (t :: G) t

17+-- stop : HasType fZ (t :: G) t

1818-- pop : HasType k G t -> HasType (fS k) (u :: G) t

1919

2020 lookup : (i:Fin n) -> Env G -> interpTy (lookup i G)

21− lookup fO (x :: xs) = x

21+ lookup fZ (x :: xs) = x

2222 lookup (fS i) (x :: xs) = lookup i xs

2323

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

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

4141 interp env (Bind v f) = interp env (f (interp env v))

4242

4343 eId : Expr G (TyFun TyInt TyInt)

44− eId = Lam (Var fO)

44+ eId = Lam (Var fZ)

4545

4646 eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))

47− eTEST = Lam (Lam (Var (fS fO)))

47+ eTEST = Lam (Lam (Var (fS fZ)))

4848

4949 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))

50− eAdd = Lam (Lam (Op prim__addInt (Var fO) (Var (fS fO))))

50+ eAdd = Lam (Lam (Op prim__addInt (Var fZ) (Var (fS fZ))))

5151

5252-- eDouble : Expr G (TyFun TyInt TyInt)

53−-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))

53+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fZ) (Var (fS fZ))))) (Var fZ)) (Var fZ))

5454

5555 eDouble : Expr G (TyFun TyInt TyInt)

56− eDouble = Lam (App (App eAdd (Var fO)) (Var fO))

56+ eDouble = Lam (App (App eAdd (Var fZ)) (Var fZ))

5757

5858 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

5959 app = \f, a => App f a

6060

6161 eFac : Expr G (TyFun TyInt TyInt)

62− eFac = Lam (If (Op (==) (Var fO) (Val 0))

63− (Val 1) (Op (*) (app eFac (Op (-) (Var fO) (Val 1))) (Var fO)))

62+ eFac = Lam (If (Op (==) (Var fZ) (Val 0))

63+ (Val 1) (Op (*) (app eFac (Op (-) (Var fZ) (Val 1))) (Var fZ)))

6464

6565 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

6666

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

68− eProg = Lam (Lam (Bind (App eDouble (Var (fS fO)))

69− (\x => Bind (App eDouble (Var fO))

68+ eProg = Lam (Lam (Bind (App eDouble (Var (fS fZ)))

69+ (\x => Bind (App eDouble (Var fZ))

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

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

7272

samples/interp.idr+1−1

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

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

1515

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

17− stop : HasType fO (t :: G) t

17+ stop : HasType fZ (t :: G) t

1818 pop : HasType k G t -> HasType (fS k) (u :: G) t

1919

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

test/reg018/reg018d.idr+2−2

@@ -3,10 +3,10 @@ module Main

33total

44pull : Fin (S n) -> Vect a (S n) -> (a, Vect a n)

55pull {n=Z} _ (x :: xs) = (x, xs)

6−-- pull {n=S q} fO (Vect.(::) {n=S _} x xs) = (x, xs)

6+-- pull {n=S q} fZ (Vect.(::) {n=S _} x xs) = (x, xs)

77pull {n=S _} (fS n) (x :: xs) =

88 let (v, vs) = pull n xs in

99 (v, x::vs)

1010

1111main : IO ()

12−main = print (pull fO [0, 1, 2])

12+main = print (pull fZ [0, 1, 2])

test/test001/test001.idr+2−2

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

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

1515

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

17− stop : HasType fO (t :: G) t

17+ stop : HasType fZ (t :: G) t

1818 pop : HasType k G t -> HasType (fS k) (u :: G) t

1919

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

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

5757 eAdd = expr (\x, y => Op (+) x y)

5858

5959-- eDouble : Expr G (TyFun TyInt TyInt)

60−-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))

60+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fZ) (Var (fS fZ))))) (Var fZ)) (Var fZ))

6161

6262 eDouble : Expr G (TyFun TyInt TyInt)

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

test/test014/Resimp.idr+1−1

@@ -46,7 +46,7 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

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

4747

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

49− stop : HasType (a :: gam) fO a

49+ stop : HasType (a :: gam) fZ a

5050 pop : HasType gam i b -> HasType (a :: gam) (fS i) b

5151

5252 data Env : Vect Ty n -> Type where

tutorial/examples/interp.idr+1−1

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

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

1515

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

17− stop : HasType fO (t :: G) t

17+ stop : HasType fZ (t :: G) t

1818 pop : HasType k G t -> HasType (fS k) (u :: G) t

1919

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

tutorial/interp.tex+2−2

@@ -64,7 +64,7 @@ constructor in turn.

6464\begin{SaveVerbatim}{exprty}

6565

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

67− stop : HasType fO (t :: G) t

67+ stop : HasType fZ (t :: G) t

6868 pop : HasType k G t -> HasType (fS k) (u :: G) t

6969

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

@@ -88,7 +88,7 @@ Variables are represented by a proof of their membership in the context,

8888\begin{SaveVerbatim}{hastype}

8989

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

91− stop : HasType fO (t :: G) t

91+ stop : HasType fZ (t :: G) t

9292 pop : HasType k G t -> HasType (fS k) (u :: G) t

9393

9494\end{SaveVerbatim}

tutorial/typesfuns.tex+2−2

@@ -384,7 +384,7 @@ by a bounded index given as a \tTC{Fin n}, is defined in the prelude:

384384\begin{SaveVerbatim}{vindex}

385385

386386index : Fin n -> Vect a n -> a

387−index fO (x :: xs) = x

387+index fZ (x :: xs) = x

388388index (fS k) (x :: xs) = index k xs

389389

390390\end{SaveVerbatim}

@@ -438,7 +438,7 @@ can still be given explicitly in applications, using \texttt{\{a=value\}} and

438438

439439\begin{SaveVerbatim}{vindexexp}

440440

441−index {a=Int} {n=2} fO (2 :: 3 :: Nil)

441+index {a=Int} {n=2} fZ (2 :: 3 :: Nil)

442442

443443\end{SaveVerbatim}

444444\useverb{vindexexp}