faf04f3 · Idris-dev · git.iko.soy

javascript/JavaScript/JSON.idr+1−1

compare with master

unifiedsplit

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

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

34

35index : (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

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

38

39infixl 8 ++

lib/Data/Bits.idr+1−1

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

434 where

435 %assert_total

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

437− helper fO _ = []

437+ helper fZ _ = []

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

439

440instance Show (Bits n) where

lib/Data/BoundedList.idr+2−2

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

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

9

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

11−length [] = fO

11+length [] = fZ

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

13

14--------------------------------------------------------------------------------

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

17

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

19index _ [] = Nothing

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

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

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

22

23--------------------------------------------------------------------------------

lib/Data/HVect.idr+4−4

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

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

12

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

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

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

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

16

17 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

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

20 deleteAt _ [] impossible

21

22 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

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

25

26 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

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

29

30 (++) : {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

88-- Fin

89--------------------------------------------------------------------------------

90

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

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

92−fONotfS refl impossible

92+fZNotfS refl impossible

93

94instance DecEq (Fin n) where

95− decEq fO fO = Yes refl

95+ decEq fZ fZ = Yes refl

96− decEq fO (fS f) = No fONotfS

96+ decEq fZ (fS f) = No fZNotfS

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

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

98 decEq (fS f) (fS f') with (decEq f f')

99 | Yes p = Yes $ cong p

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

lib/Prelude/Fin.idr+8−8

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

4import Prelude.Either

5

6data Fin : Nat -> Type where

7− fO : Fin (S k)

7+ fZ : Fin (S k)

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

9

10instance Eq (Fin n) where

11− (==) fO fO = True

11+ (==) fZ fZ = True

12 (==) (fS k) (fS k') = k == k'

13 (==) _ _ = False

14

15finToNat : Fin n -> Nat -> Nat

16−finToNat fO a = a

16+finToNat fZ a = a

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

18

19instance Cast (Fin n) Nat where

20 cast x = finToNat x Z

21

22finToInt : Fin n -> Integer -> Integer

23−finToInt fO a = a

23+finToInt fZ a = a

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

25

26instance Cast (Fin n) Integer where

27 cast x = finToInt x 0

28

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

30−weaken fO = fO

30+weaken fZ = fZ

31weaken (fS k) = fS (weaken k)

32

33strengthen : 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

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

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

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

38strengthen f = Left f

39

40last : Fin (S n)

41−last {n=Z} = fO

41+last {n=Z} = fZ

42last {n=S _} = fS last

43

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

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

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

49

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

51−natToFin Z (S j) = Just fO

51+natToFin Z (S j) = Just fZ

52natToFin (S k) (S j) with (natToFin k j)

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

54 | Nothing = Nothing

lib/Prelude/Vect.idr+6−6

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

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

33

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

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

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

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

37−index fO [] impossible

37+index fZ [] impossible

38

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

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

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

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

42deleteAt _ [] impossible

43

44replaceAt : 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

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

47

48--------------------------------------------------------------------------------

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

50--------------------------------------------------------------------------------

51

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

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

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

54take (fS k) [] impossible

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

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

57

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

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

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

60drop (fS k) [] impossible

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

62

lib/Uninhabited.idr+1−1

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

4 total uninhabited : t -> _|_

5

6instance Uninhabited (Fin Z) where

7− uninhabited fO impossible

7+ uninhabited fZ impossible

8 uninhabited (fS f) impossible

9

10instance Uninhabited (Z = S n) where

samples/interp-alt.idr+11−11

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

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

15

16-- 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

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

19

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

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

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

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

23

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

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

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

42

43 eId : Expr G (TyFun TyInt TyInt)

44− eId = Lam (Var fO)

44+ eId = Lam (Var fZ)

45

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

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

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

48

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

51

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

54

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

57

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

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

60

61 eFac : Expr G (TyFun TyInt TyInt)

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

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

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

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

64

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

66

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

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

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

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

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

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

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

72

samples/interp.idr+1−1

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

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

15

16 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

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

19

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

test/reg018/reg018d.idr+2−2

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

3total

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

5pull {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)

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

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

9 (v, x::vs)

10

11main : 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)

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

15

16 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

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

19

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

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

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

58

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

61

62 eDouble : Expr G (TyFun TyInt TyInt)

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

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

47

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

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

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

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

51

52 data Env : Vect Ty n -> Type where

tutorial/examples/interp.idr+1−1

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

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

15

16 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

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

19

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

tutorial/interp.tex+2−2

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

64\begin{SaveVerbatim}{exprty}

65

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

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

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

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

69

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

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

88\begin{SaveVerbatim}{hastype}

89

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

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

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

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

93

94\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:

384\begin{SaveVerbatim}{vindex}

385

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

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

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

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

389

390\end{SaveVerbatim}

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

438

439\begin{SaveVerbatim}{vindexexp}

440

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

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

442

443\end{SaveVerbatim}

444\useverb{vindexexp}