fe569c4 · Idris-dev · git.iko.soy

benchmarks/quasigroups/Parser.idr+8−8

compare with master

unifiedsplit

@@ -24,11 +24,11 @@ parseToken x = map Just (tryParseFin ((cast x) - 1))

24 where

25 tryParseFin : Int -> Either String (Fin n)

26 tryParseFin {n=Z} _ = Left ("Given cell " ++ x ++ " out of range")

27− tryParseFin {n=S k} 0 = return fZ

27+ tryParseFin {n=S k} 0 = return FZ

28 tryParseFin {n=S k} x =

29 case tryParseFin {n=k} (x-1) of

30 Left err => Left err

31− Right fin => return (fS fin)

31+ Right fin => return (FS fin)

32

33length : Vect n a -> Nat

34length {n=n} _ = n

@@ -49,9 +49,9 @@ parseCols {n=S k} row l cs = helper last l

49 No _ => Left ("Illegal cell " ++ index x cs)

50

51 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

52− helper fZ l = step l fZ

52+ helper FZ l = step l FZ

53− helper (fS k) l = do

53+ helper (FS k) l = do

54− (_ ** next) <- step l (fS k)

54+ (_ ** next) <- step l (FS k)

55 helper (weaken k) next

56

57parseRows : (b : Board n) -> LegalBoard b -> Vect n String -> Parser n

@@ -66,9 +66,9 @@ parseRows {n=S k} _ l rs = helper last l

66 Yes prf => let foo = (replace {P=\n => Vect n String} prf cs) in parseCols i l foo -- TODO: foo shouldn't be needed

67

68 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

69− helper fZ l = step fZ l

69+ helper FZ l = step FZ l

70− helper (fS k) l = do

70+ helper (FS k) l = do

71− (_ ** next) <- step (fS k) l

71+ (_ ** next) <- step (FS k) l

72 helper (weaken k) next

73

74parse : String -> Either String (n : Nat ** (b : Board n ** LegalBoard b))

benchmarks/quasigroups/Solver.idr+11−11

@@ -35,8 +35,8 @@ instance Show (Board n) where

35 show (MkBoard rs) = unlines (map showRow rs)

36

37updateAt : Fin n -> Vect n a -> (a -> a) -> Vect n a

38−updateAt fZ (x::xs) f = f x :: xs

38+updateAt FZ (x::xs) f = f x :: xs

39−updateAt (fS i) (x::xs) f = x :: updateAt i xs f

39+updateAt (FS i) (x::xs) f = x :: updateAt i xs f

40

41setCell : Board n -> (Fin n, Fin n) -> Fin n -> Board n

42setCell (MkBoard b) (x, y) value = MkBoard (updateAt y b (\row => updateAt x row (const (Just value))))

@@ -127,18 +127,18 @@ data LegalBoard : Board n -> Type where

127CompleteBoard : Board n -> Type

128CompleteBoard b = (LegalBoard b, FullBoard b)

129

130−indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (fS i) (x::xs)

130+indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (FS i) (x::xs)

131indexStep = Refl

132

133find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)

134 -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))

135find _ Nil = Left Nil

136find d (x::xs) with (d x)

137− | Yes prf = Right (x ** (prf, (fZ ** Refl)))

137+ | Yes prf = Right (x ** (prf, (FZ ** Refl)))

138 | No prf =

139 case find d xs of

140 Right (y ** (prf', (i ** prf''))) =>

141− Right (y ** (prf', (fS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))

141+ Right (y ** (prf', (FS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))

142 Left prf' => Left (prf::prf')

143

144findEmptyInRow : (xs : Vect n (Cell n)) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))

@@ -158,11 +158,11 @@ emptyCell (MkBoard rs) =

158 helper Nil = Left Nil

159 helper (r::rs) =

160 case findEmptyInRow r of

161− Right (ci ** pf) => Right (fZ ** (ci ** pf))

161+ Right (ci ** pf) => Right (FZ ** (ci ** pf))

162 Left prf =>

163 case helper rs of

164 Left prf' => Left (prf::prf')

165− Right (ri ** (ci ** pf)) => Right (fS ri ** (ci ** pf))

165+ Right (ri ** (ci ** pf)) => Right (FS ri ** (ci ** pf))

166

167

168tryValue : {b : Board (S n)} -> LegalBoard b -> (c : (Fin (S n), Fin (S n))) -> Empty (getCell b c) -> (v : Fin (S n))

@@ -189,16 +189,16 @@ fillBoard {n=(S n)} b l with (emptyCell b)

189 Right success => (v, Just success)

190 Left _ => -- TODO: Prove unsolvable

191 case v of

192− fS k => tryAll (weaken k)

192+ FS k => tryAll (weaken k)

193− fZ => (v, Nothing)

193+ FZ => (v, Nothing)

194

195 %assert_total

196 recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')

197 recurse start =

198 case tryAll start of

199 (_, Nothing) => Nothing

200− (fZ, Just (b' ** l')) => fillBoard b' l'

200+ (FZ, Just (b' ** l')) => fillBoard b' l'

201− (fS next, Just (b' ** l')) =>

201+ (FS next, Just (b' ** l')) =>

202 case fillBoard b' l' of

203 Just solution => Just solution

204 Nothing => recurse (weaken next)

libs/base/Control/Isomorphism.idr+6−6

@@ -268,17 +268,17 @@ eitherMaybeRightMaybe {a} {b} =

268maybeIsoS : Iso (Maybe (Fin n)) (Fin (S n))

269maybeIsoS = MkIso forth back fb bf

270 where forth : Maybe (Fin n) -> Fin (S n)

271− forth Nothing = fZ

271+ forth Nothing = FZ

272− forth (Just x) = fS x

272+ forth (Just x) = FS x

273 back : Fin (S n) -> Maybe (Fin n)

274− back fZ = Nothing

274+ back FZ = Nothing

275− back (fS x) = Just x

275+ back (FS x) = Just x

276 bf : (x : Maybe (Fin n)) -> back (forth x) = x

277 bf Nothing = Refl

278 bf (Just x) = Refl

279 fb : (y : Fin (S n)) -> forth (back y) = y

280− fb fZ = Refl

280+ fb FZ = Refl

281− fb (fS x) = Refl

281+ fb (FS x) = Refl

282

283finZeroBot : Iso (Fin 0) _|_

284finZeroBot = MkIso (\x => FalseElim (uninhabited x))

libs/base/Data/Bits.idr+2−2

@@ -437,8 +437,8 @@ bitsToStr x = pack (helper last x)

437 where

438 %assert_total

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

440− helper fZ _ = []

440+ helper FZ _ = []

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

441+ helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b

442

443instance Show (Bits n) where

444 show = bitsToStr

libs/base/Data/BoundedList.idr+4−4

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

10

11||| Compute the length of a list.

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

13−length [] = fZ

13+length [] = FZ

14−length (x :: xs) = fS (length xs)

14+length (x :: xs) = FS (length xs)

15

16--------------------------------------------------------------------------------

17-- Indexing into bounded lists

@@ -19,8 +19,8 @@ length (x :: xs) = fS (length xs)

19

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

21index _ [] = Nothing

22−index fZ (x :: _) = Just x

22+index FZ (x :: _) = Just x

23−index (fS f) (_ :: xs) = index f xs

23+index (FS f) (_ :: xs) = index f xs

24

25--------------------------------------------------------------------------------

26-- Adjusting bounds

libs/base/Data/Buffer.idr+2−2

@@ -33,8 +33,8 @@ bitsFromNat Z = 0

33bitsFromNat (S k) = 1 + bitsFromNat k

34

35bitsFromFin : Fin n -> Bits64

36−bitsFromFin fZ = 0

36+bitsFromFin FZ = 0

37−bitsFromFin (fS k) = 1 + bitsFromFin k

37+bitsFromFin (FS k) = 1 + bitsFromFin k

38

39||| Allocate an empty Buffer. The size hint can be used to avoid

40||| unnecessary reallocations and copies under the hood if the

libs/base/Data/HVect.idr+9−9

@@ -13,22 +13,22 @@ data HVect : Vect k Type -> Type where

13

14||| Extract an element from an HVect

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

16−index fZ (x::xs) = x

16+index FZ (x::xs) = x

17−index (fS j) (x::xs) = index j xs

17+index (FS j) (x::xs) = index j xs

18

19deleteAt : (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)

20−deleteAt fZ (x::xs) = xs

20+deleteAt FZ (x::xs) = xs

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

21+deleteAt {l = S m} (FS j) (x::xs) = x :: deleteAt j xs

22−deleteAt {l = Z} (fS j) (x::xs) = absurd j

22+deleteAt {l = Z} (FS j) (x::xs) = absurd j

23deleteAt _ [] impossible

24

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

26−replaceAt fZ y (x::xs) = y::xs

26+replaceAt FZ y (x::xs) = y::xs

27−replaceAt (fS j) y (x::xs) = x :: replaceAt j y xs

27+replaceAt (FS j) y (x::xs) = x :: replaceAt j y xs

28

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

30−updateAt fZ f (x::xs) = f x :: xs

30+updateAt FZ f (x::xs) = f x :: xs

31−updateAt (fS j) f (x::xs) = x :: updateAt j f xs

31+updateAt (FS j) f (x::xs) = x :: updateAt j f xs

32

33||| Append two `HVect`s.

34(++) : HVect ts -> HVect us -> HVect (ts ++ us)

libs/base/Decidable/Order.idr+56−67

@@ -15,7 +15,7 @@ import Decidable.Equality

15

16class Preorder t (po : t -> t -> Type) where

17 total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c

18− total Reflexive : (a : t) -> po a a

18+ total reflexive : (a : t) -> po a a

19

20class (Preorder t po) => Poset t (po : t -> t -> Type) where

21 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b

@@ -48,7 +48,7 @@ maximum x y with (order x y)

48

49instance Preorder t ((=) {A = t} {B = t}) where

50 transitive a b c = trans {a = a} {b = b} {c = c}

51− Reflexive a = Refl

51+ reflexive a = Refl

52

53instance Equivalence t ((=) {A = t} {B = t}) where

54 symmetric a b prf = sym prf

@@ -60,99 +60,88 @@ instance Congruence t f ((=) {A = t} {B = t}) where

60-- Natural numbers

61--------------------------------------------------------------------------------

62

63−data NatLTE : Nat -> Nat -> Type where

63+total LTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->

64− nEqn : NatLTE n n

64+ LTE m n -> LTE n o ->

65− nLTESm : NatLTE n m -> NatLTE n (S m)

65+ LTE m o

66+LTEIsTransitive Z n o LTEZero nlteo = LTEZero

67+LTEIsTransitive (S m) (S n) (S o) (LTESucc mlten) (LTESucc nlteo) = LTESucc (LTEIsTransitive m n o mlten nlteo)

66

68

67−total NatLTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->

69+total LTEIsReflexive : (n : Nat) -> LTE n n

68− NatLTE m n -> NatLTE n o ->

70+LTEIsReflexive Z = LTEZero

69− NatLTE m o

71+LTEIsReflexive (S n) = LTESucc (LTEIsReflexive n)

70−NatLTEIsTransitive m n n mLTEn (nEqn) = mLTEn

71−NatLTEIsTransitive m n (S o) mLTEn (nLTESm nLTEo)

72− = nLTESm (NatLTEIsTransitive m n o mLTEn nLTEo)

73

72

74−total NatLTEIsReflexive : (n : Nat) -> NatLTE n n

73+instance Preorder Nat LTE where

75−NatLTEIsReflexive _ = nEqn

74+ transitive = LTEIsTransitive

75+ reflexive = LTEIsReflexive

76

77−instance Preorder Nat NatLTE where

77+total LTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->

78− transitive = NatLTEIsTransitive

78+ LTE m n -> LTE n m -> m = n

79− Reflexive = NatLTEIsReflexive

79+LTEIsAntisymmetric Z Z LTEZero LTEZero = Refl

80+LTEIsAntisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm) with (LTEIsAntisymmetric n m mLTEn nLTEm)

81+ LTEIsAntisymmetric (S n) (S n) (LTESucc mLTEn) (LTESucc nLTEm) | Refl = Refl

80

82

81−total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->

82− NatLTE m n -> NatLTE n m -> m = n

83−NatLTEIsAntisymmetric n n nEqn nEqn = Refl

84−NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible

85−NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible

86−NatLTEIsAntisymmetric n m (nLTESm _) (nLTESm _) impossible

87

83

88−instance Poset Nat NatLTE where

84+instance Poset Nat LTE where

89− antisymmetric = NatLTEIsAntisymmetric

85+ antisymmetric = LTEIsAntisymmetric

90

86

91−total zeroNeverGreater : {n : Nat} -> NatLTE (S n) Z -> _|_

87+total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> _|_

92−zeroNeverGreater {n} (nLTESm _) impossible

88+zeroNeverGreater {n} LTEZero impossible

93−zeroNeverGreater {n} nEqn impossible

89+zeroNeverGreater {n} (LTESucc _) impossible

94

90

95−total zeroAlwaysSmaller : {n : Nat} -> NatLTE Z n

91+total zeroAlwaysSmaller : {n : Nat} -> LTE Z n

96−zeroAlwaysSmaller {n = Z } = nEqn

92+zeroAlwaysSmaller = LTEZero

97−zeroAlwaysSmaller {n = S k} = nLTESm (zeroAlwaysSmaller {n = k})

98

93

99−total

100−nGTSm : {n : Nat} -> {m : Nat} -> (NatLTE n m -> _|_) -> NatLTE n (S m) -> _|_

94+total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> _|_) -> LTE (S n) (S m) -> _|_

101−nGTSm disprf (nLTESm nLTEm) = FalseElim (disprf nLTEm)

95+ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = FalseElim (disprf nLTEm)

102−nGTSm {n} {m} disprf (nEqn) impossible

96+ltesuccinjective {n} {m} disprf LTEZero impossible

103

97

104−total

98+

105−decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)

99+total decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)

106−decideNatLTE Z Z = Yes nEqn

100+decideLTE Z y = Yes LTEZero

107−decideNatLTE (S x) Z = No zeroNeverGreater

101+decideLTE (S x) Z = No zeroNeverGreater

108−decideNatLTE x (S y) with (decEq x (S y))

102+decideLTE (S x) (S y) with (decEq (S x) (S y))

109− | Yes eq = rewrite eq in Yes nEqn

103+ | Yes eq = rewrite eq in Yes (reflexive x)

110− | No _ with (decideNatLTE x y)

104+ | No _ with (decideLTE x y)

111− | Yes nLTEm = Yes (nLTESm nLTEm)

105+ | Yes nLTEm = Yes (LTESucc nLTEm)

112− | No nGTm = No (nGTSm nGTm)

106+ | No nGTm = No (ltesuccinjective nGTm)

113−

107+

114−instance Decidable [Nat,Nat] NatLTE where

108+instance Decidable [Nat,Nat] LTE where

115− decide = decideNatLTE

109+ decide = decideLTE

116

110

117total

111total

118−lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)

112+lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)

119−lte m n = decide {ts = [Nat,Nat]} {p = NatLTE} m n

113+lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n

120

114

121total

115total

122−shift : (m : Nat) -> (n : Nat) -> NatLTE m n -> NatLTE (S m) (S n)

116+shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)

123−shift Z Z _ = nEqn

117+shift m n mLTEn = LTESucc mLTEn

124−shift Z (S Z) _ = nLTESm nEqn

118+

125−shift Z (S (S j)) _ = nLTESm (shift Z (S j) zeroAlwaysSmaller)

126−shift (S k) Z prf = FalseElim (zeroNeverGreater prf)

127−shift (S k) (S k) nEqn = nEqn

128−shift (S k) (S j) (nLTESm prf) = nLTESm (shift (S k) j prf)

129−

130−instance Ordered Nat NatLTE where

119+instance Ordered Nat LTE where

131− order Z n = Left zeroAlwaysSmaller

120+ order Z n = Left LTEZero

132− order m Z = Right zeroAlwaysSmaller

121+ order m Z = Right LTEZero

133 order (S k) (S j) with (order k j)

122 order (S k) (S j) with (order k j)

134 order (S k) (S j) | Left prf = Left (shift k j prf)

123 order (S k) (S j) | Left prf = Left (shift k j prf)

135 order (S k) (S j) | Right prf = Right (shift j k prf)

124 order (S k) (S j) | Right prf = Right (shift j k prf)

136

125

137−--------------------------------------------------------------------------------

126+----------------------------------------------------------------------------------

138−-- Finite numbers

127+---- Finite numbers

139−--------------------------------------------------------------------------------

128+----------------------------------------------------------------------------------

140

129

141using (k : Nat)

130using (k : Nat)

142 data FinLTE : Fin k -> Fin k -> Type where

131 data FinLTE : Fin k -> Fin k -> Type where

143− FromNatPrf : {m : Fin k} -> {n : Fin k} -> NatLTE (finToNat m) (finToNat n) -> FinLTE m n

132+ FromNatPrf : {m : Fin k} -> {n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n

144

133

145 instance Preorder (Fin k) FinLTE where

134 instance Preorder (Fin k) FinLTE where

146 transitive m n o (FromNatPrf p1) (FromNatPrf p2) =

135 transitive m n o (FromNatPrf p1) (FromNatPrf p2) =

147− FromNatPrf (NatLTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)

136+ FromNatPrf (LTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)

148− Reflexive n = FromNatPrf (NatLTEIsReflexive (finToNat n))

137+ reflexive n = FromNatPrf (LTEIsReflexive (finToNat n))

149

138

150 instance Poset (Fin k) FinLTE where

139 instance Poset (Fin k) FinLTE where

151 antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =

140 antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =

152− finToNatInjective m n (NatLTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)

141+ finToNatInjective m n (LTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)

153

142

154 instance Decidable [Fin k, Fin k] FinLTE where

143 instance Decidable [Fin k, Fin k] FinLTE where

155− decide m n with (decideNatLTE (finToNat m) (finToNat n))

144+ decide m n with (decideLTE (finToNat m) (finToNat n))

156 | Yes prf = Yes (FromNatPrf prf)

145 | Yes prf = Yes (FromNatPrf prf)

157 | No disprf = No (\ (FromNatPrf prf) => disprf prf)

146 | No disprf = No (\ (FromNatPrf prf) => disprf prf)

158

147

libs/base/System/Concurrency/Process.idr+13−13

@@ -12,38 +12,38 @@ data ProcID msg = MkPID Ptr

12||| Type safe message passing programs. Parameterised over the type of

13||| message which can be send, and the return type.

14data Process : (msgType : Type) -> Type -> Type where

15− lift : IO a -> Process msg a

15+ Lift : IO a -> Process msg a

16

17instance Functor (Process msg) where

18− map f (lift a) = lift (map f a)

18+ map f (Lift a) = Lift (map f a)

19

20instance Applicative (Process msg) where

21− pure = lift . return

21+ pure = Lift . return

22− (lift f) <$> (lift a) = lift (f <$> a)

22+ (Lift f) <$> (Lift a) = Lift (f <$> a)

23

24instance Monad (Process msg) where

25− (lift io) >>= k = lift (do x <- io

25+ (Lift io) >>= k = Lift (do x <- io

26 case k x of

27− lift v => v)

27+ Lift v => v)

28

29run : Process msg x -> IO x

30−run (lift prog) = prog

30+run (Lift prog) = prog

31

32||| Get current process ID

33myID : Process msg (ProcID msg)

34−myID = lift (return (MkPID prim__vm))

34+myID = Lift (return (MkPID prim__vm))

35

36||| Send a message to another process

37send : ProcID msg -> msg -> Process msg ()

38−send (MkPID p) m = lift (sendToThread p (prim__vm, m))

38+send (MkPID p) m = Lift (sendToThread p (prim__vm, m))

39

40||| Return whether a message is waiting in the queue

41msgWaiting : Process msg Bool

42−msgWaiting = lift checkMsgs

42+msgWaiting = Lift checkMsgs

43

44||| Receive a message - blocks if there is no message waiting

45recv : Process msg msg

46−recv {msg} = do (senderid, m) <- lift get

46+recv {msg} = do (senderid, m) <- Lift get

47 return m

48 where get : IO (Ptr, msg)

49 get = getMsg

@@ -51,11 +51,11 @@ recv {msg} = do (senderid, m) <- lift get

51||| receive a message, and return with the sender's process ID.

52recvWithSender : Process msg (ProcID msg, msg)

53recvWithSender {msg}

54− = do (senderid, m) <- lift get

54+ = do (senderid, m) <- Lift get

55 return (MkPID senderid, m)

56 where get : IO (Ptr, msg)

57 get = getMsg

58

59create : Process msg () -> Process msg (ProcID msg)

60−create (lift p) = do ptr <- lift (fork p)

60+create (Lift p) = do ptr <- Lift (fork p)

61 return (MkPID ptr)

libs/effects/Effect/Memory.idr+12−12

@@ -16,23 +16,23 @@ data RawMemory : Effect where

16 Free : RawMemory () (MemoryChunk n i) (\v => ())

17 Initialize : Bits8 ->

18 (size : Nat) ->

19− so (i + size <= n) ->

19+ So (i + size <= n) ->

20 RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (i + size))

21 Peek : (offset : Nat) ->

22 (size : Nat) ->

23− so (offset + size <= i) ->

23+ So (offset + size <= i) ->

24 RawMemory (Vect size Bits8)

25 (MemoryChunk n i) (\v => MemoryChunk n i)

26 Poke : (offset : Nat) ->

27 (Vect size Bits8) ->

28− so (offset <= i && offset + size <= n) ->

28+ So (offset <= i && offset + size <= n) ->

29 RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))

30 Move : (src : MemoryChunk src_size src_init) ->

31 (dst_offset : Nat) ->

32 (src_offset : Nat) ->

33 (size : Nat) ->

34− so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

34+ So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

35− so (src_offset + size <= src_init) ->

35+ So (src_offset + size <= src_init) ->

36 RawMemory () (MemoryChunk dst_size dst_init)

37 (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))

38 GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)

@@ -108,7 +108,7 @@ initialize : {i : Nat} ->

108 {n : Nat} ->

109 Bits8 ->

110 (size : Nat) ->

111− so (i + size <= n) ->

111+ So (i + size <= n) ->

112 Eff () [RAW_MEMORY (MemoryChunk n i)]

113 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])

114initialize c size prf = call $ Initialize c size prf

@@ -119,7 +119,7 @@ free = call Free

119peek : {i : Nat} ->

120 (offset : Nat) ->

121 (size : Nat) ->

122− so (offset + size <= i) ->

122+ So (offset + size <= i) ->

123 { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)

124peek offset size prf = call $ Peek offset size prf

125

@@ -127,7 +127,7 @@ poke : {n : Nat} ->

127 {i : Nat} ->

128 (offset : Nat) ->

129 Vect size Bits8 ->

130− so (offset <= i && offset + size <= n) ->

130+ So (offset <= i && offset + size <= n) ->

131 Eff () [RAW_MEMORY (MemoryChunk n i)]

132 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])

133poke offset content prf = call $ Poke offset content prf

@@ -144,8 +144,8 @@ move' : {dst_size : Nat} ->

144 (dst_offset : Nat) ->

145 (src_offset : Nat) ->

146 (size : Nat) ->

147− so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

147+ So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

148− so (src_offset + size <= src_init) ->

148+ So (src_offset + size <= src_init) ->

149 Eff () [RAW_MEMORY (MemoryChunk dst_size dst_init)]

150 (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])

151move' src_ptr dst_offset src_offset size dst_bounds src_bounds

@@ -160,8 +160,8 @@ move : {dst_size : Nat} ->

160 (dst_offset : Nat) ->

161 (src_offset : Nat) ->

162 (size : Nat) ->

163− so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

163+ So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

164− so (src_offset + size <= src_init) ->

164+ So (src_offset + size <= src_init) ->

165 Eff ()

166 [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)

167 , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]

libs/prelude/Decidable/Equality.idr+7−7

@@ -96,16 +96,16 @@ instance (DecEq a, DecEq b) => DecEq (Either a b) where

96-- Fin

97--------------------------------------------------------------------------------

98

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

99+total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> _|_

100−fZNotfS Refl impossible

100+FZNotFS Refl impossible

101

102instance DecEq (Fin n) where

103− decEq fZ fZ = Yes Refl

103+ decEq FZ FZ = Yes Refl

104− decEq fZ (fS f) = No fZNotfS

104+ decEq FZ (FS f) = No FZNotFS

105− decEq (fS f) fZ = No $ negEqSym fZNotfS

105+ decEq (FS f) FZ = No $ negEqSym FZNotFS

106− decEq (fS f) (fS f') with (decEq f f')

106+ decEq (FS f) (FS f') with (decEq f f')

107 | Yes p = Yes $ cong p

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

108+ | No p = No $ \h => p $ FSinjective {f = f} {f' = f'} h

109

110--------------------------------------------------------------------------------

111-- Tuple

libs/prelude/Prelude.idr+3−3

@@ -420,9 +420,9 @@ instance Enum Int where

420 go (x :: xs) = n + (cast x * inc) :: go xs

421

422instance Enum (Fin (S n)) where

423− pred fZ = fZ

423+ pred FZ = FZ

424− pred (fS n) = weaken n

424+ pred (FS n) = weaken n

425− succ n = case strengthen (fS n) of

425+ succ n = case strengthen (FS n) of

426 Left _ => last

427 Right k => k

428 toNat n = cast n

libs/prelude/Prelude/Bool.idr+4−3

@@ -24,10 +24,11 @@ boolElim False t e = e

24||| If you find yourself using `so` for something other than primitive types,

25||| it may be appropriate to define a type of evidence for the property that you

26||| care about instead.

27−data so : Bool -> Type where oh : so True

27+data So : Bool -> Type where

28+ Oh : So True

28

29

29−instance Uninhabited (so False) where

30+instance Uninhabited (So False) where

30− uninhabited oh impossible

31+ uninhabited Oh impossible

31

32

32-- Syntactic sugar for boolean elimination.

33-- Syntactic sugar for boolean elimination.

33syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

34syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

libs/prelude/Prelude/Either.idr+4−4

@@ -30,10 +30,10 @@ isRight (Right r) = True

30-- Misc.

31--------------------------------------------------------------------------------

32

33−||| Perform a case analysis on a Boolean, providing clients with a `so` proof

33+||| Perform a case analysis on a Boolean, providing clients with a `So` proof

34−choose : (b : Bool) -> Either (so b) (so (not b))

34+choose : (b : Bool) -> Either (So b) (So (not b))

35−choose True = Left oh

35+choose True = Left Oh

36−choose False = Right oh

36+choose False = Right Oh

37

38||| Simply-typed eliminator for Either

39||| @ f the action to take on Left

libs/prelude/Prelude/Fin.idr+44−44

@@ -12,39 +12,39 @@ import Prelude.Uninhabited

12||| exceedingly inefficient at run time.

13||| @ n the upper bound

14data Fin : (n : Nat) -> Type where

15− fZ : Fin (S k)

15+ FZ : Fin (S k)

16− fS : Fin k -> Fin (S k)

16+ FS : Fin k -> Fin (S k)

17

18instance Uninhabited (Fin Z) where

19− uninhabited fZ impossible

19+ uninhabited FZ impossible

20− uninhabited (fS f) impossible

20+ uninhabited (FS f) impossible

21

22−fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n

22+FSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = n

23−fSInjective left _ Refl = Refl

23+FSInjective left _ Refl = Refl

24

25instance Eq (Fin n) where

26− (==) fZ fZ = True

26+ (==) FZ FZ = True

27− (==) (fS k) (fS k') = k == k'

27+ (==) (FS k) (FS k') = k == k'

28 (==) _ _ = False

29

30||| There are no elements of `Fin Z`

31FinZAbsurd : Fin Z -> _|_

32−FinZAbsurd fZ impossible

32+FinZAbsurd FZ impossible

33

34FinZElim : Fin Z -> a

35FinZElim x = FalseElim (FinZAbsurd x)

36

37||| Convert a Fin to a Nat

38finToNat : Fin n -> Nat

39−finToNat fZ = Z

39+finToNat FZ = Z

40−finToNat (fS k) = S (finToNat k)

40+finToNat (FS k) = S (finToNat k)

41

42||| `finToNat` is injective

43finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn

44−finToNatInjective fZ fZ Refl = Refl

44+finToNatInjective FZ FZ Refl = Refl

45−finToNatInjective (fS m) fZ Refl impossible

45+finToNatInjective (FS m) FZ Refl impossible

46−finToNatInjective fZ (fS n) Refl impossible

46+finToNatInjective FZ (FS n) Refl impossible

47−finToNatInjective (fS m) (fS n) prf =

47+finToNatInjective (FS m) (FS n) prf =

48 cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))

49

50instance Cast (Fin n) Nat where

@@ -52,29 +52,29 @@ instance Cast (Fin n) Nat where

52

53||| Convert a Fin to an Integer

54finToInteger : Fin n -> Integer

55−finToInteger fZ = 0

55+finToInteger FZ = 0

56−finToInteger (fS k) = 1 + finToInteger k

56+finToInteger (FS k) = 1 + finToInteger k

57

58instance Cast (Fin n) Integer where

59 cast x = finToInteger x

60

61||| Weaken the bound on a Fin by 1

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

63−weaken fZ = fZ

63+weaken FZ = FZ

64−weaken (fS k) = fS (weaken k)

64+weaken (FS k) = FS (weaken k)

65

66||| Weaken the bound on a Fin by some amount

67weakenN : (n : Nat) -> Fin m -> Fin (m + n)

68−weakenN n fZ = fZ

68+weakenN n FZ = FZ

69−weakenN n (fS f) = fS (weakenN n f)

69+weakenN n (FS f) = FS (weakenN n f)

70

71||| Attempt to tighten the bound on a Fin.

72||| Return `Left` if the bound could not be tightened, or `Right` if it could.

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

74−strengthen {n = S k} fZ = Right fZ

74+strengthen {n = S k} FZ = Right FZ

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

75+strengthen {n = S k} (FS i) with (strengthen i)

76− strengthen (fS k) | Left x = Left (fS x)

76+ strengthen (FS k) | Left x = Left (FS x)

77− strengthen (fS k) | Right x = Right (fS x)

77+ strengthen (FS k) | Right x = Right (FS x)

78strengthen f = Left f

79

80||| Add some natural number to a Fin, extending the bound accordingly

@@ -82,24 +82,24 @@ strengthen f = Left f

82||| @ m the number to increase the Fin by

83shift : (m : Nat) -> Fin n -> Fin (m + n)

84shift Z f = f

85−shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)

85+shift {n=n} (S m) f = FS {k = (m + n)} (shift m f)

86

87||| The largest element of some Fin type

88last : Fin (S n)

89−last {n=Z} = fZ

89+last {n=Z} = FZ

90−last {n=S _} = fS last

90+last {n=S _} = FS last

91

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

92+total FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'

93−fSinjective Refl = Refl

93+FSinjective Refl = Refl

94

95instance Ord (Fin n) where

96− compare fZ fZ = EQ

96+ compare FZ FZ = EQ

97− compare fZ (fS _) = LT

97+ compare FZ (FS _) = LT

98− compare (fS _) fZ = GT

98+ compare (FS _) FZ = GT

99− compare (fS x) (fS y) = compare x y

99+ compare (FS x) (FS y) = compare x y

100

101instance MinBound (Fin (S n)) where

102− minBound = fZ

102+ minBound = FZ

103

104instance MaxBound (Fin (S n)) where

105 maxBound = last

@@ -107,28 +107,28 @@ instance MaxBound (Fin (S n)) where

107

108||| Add two Fins, extending the bound

109(+) : Fin n -> Fin m -> Fin (n + m)

110−(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')

110+(+) {n=S n} {m=m} FZ f' = rewrite plusCommutative n m in weaken (weakenN n f')

111−(+) (fS f) f' = fS (f + f')

111+(+) (FS f) f' = FS (f + f')

112

113||| Substract two Fins, keeping the bound of the minuend

114(-) : Fin n -> Fin m -> Fin n

115−fZ - _ = fZ

115+FZ - _ = FZ

116−f - fZ = f

116+f - FZ = f

117−(fS f) - (fS f') = weaken $ f - f'

117+(FS f) - (FS f') = weaken $ f - f'

118

119||| Multiply two Fins, extending the bound

120(*) : Fin n -> Fin m -> Fin (n * m)

121(*) {n=Z} f f' = FinZElim f

122(*) {m=Z} f f' = FinZElim f'

123−(*) {n=S n} {m=S m} fZ f' = fZ

123+(*) {n=S n} {m=S m} FZ f' = FZ

124−(*) {n=S n} {m=S m} (fS f) f' = f' + (f * f')

124+(*) {n=S n} {m=S m} (FS f) f' = f' + (f * f')

125

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

127

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

129−natToFin Z (S j) = Just fZ

129+natToFin Z (S j) = Just FZ

130natToFin (S k) (S j) with (natToFin k j)

131− | Just k' = Just (fS k')

131+ | Just k' = Just (FS k')

132 | Nothing = Nothing

133natToFin _ _ = Nothing

134

libs/prelude/Prelude/Nat.idr+18−18

@@ -94,9 +94,9 @@ hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)

94||| @ m the larger number

95data LTE : (n, m : Nat) -> Type where

96 ||| Zero is the smallest Nat

97− lteZero : LTE Z right

97+ LTEZero : LTE Z right

98 ||| If n <= m, then n + 1 <= m + 1

99− lteSucc : LTE left right -> LTE (S left) (S right)

99+ LTESucc : LTE left right -> LTE (S left) (S right)

100

101||| Greater than or equal to

102total GTE : Nat -> Nat -> Type

@@ -112,18 +112,18 @@ GT left right = LT right left

112

113||| A successor is never less than or equal zero

114succNotLTEzero : Not (S m `LTE` Z)

115−succNotLTEzero lteZero impossible

115+succNotLTEzero LTEZero impossible

116

117||| If two numbers are ordered, their predecessors are too

118fromLteSucc : (S m `LTE` S n) -> (m `LTE` n)

119−fromLteSucc (lteSucc x) = x

119+fromLteSucc (LTESucc x) = x

120

121||| A decision procedure for `LTE`

122isLTE : (m, n : Nat) -> Dec (m `LTE` n)

123−isLTE Z n = Yes lteZero

123+isLTE Z n = Yes LTEZero

124isLTE (S k) Z = No succNotLTEzero

125isLTE (S k) (S j) with (isLTE k j)

126− isLTE (S k) (S j) | (Yes prf) = Yes (lteSucc prf)

126+ isLTE (S k) (S j) | (Yes prf) = Yes (LTESucc prf)

127 isLTE (S k) (S j) | (No contra) = No (contra . fromLteSucc)

128

129||| Boolean test than one Nat is less than or equal to another

@@ -329,18 +329,18 @@ lcm x y = divNat (x * y) (gcd x y)

329-- An informative comparison view

330--------------------------------------------------------------------------------

331data CmpNat : Nat -> Nat -> Type where

332− cmpLT : (y : _) -> CmpNat x (x + S y)

332+ CmpLT : (y : _) -> CmpNat x (x + S y)

333− cmpEQ : CmpNat x x

333+ CmpEQ : CmpNat x x

334− cmpGT : (x : _) -> CmpNat (y + S x) y

334+ CmpGT : (x : _) -> CmpNat (y + S x) y

335

336total cmp : (x, y : Nat) -> CmpNat x y

337−cmp Z Z = cmpEQ

337+cmp Z Z = CmpEQ

338−cmp Z (S k) = cmpLT _

338+cmp Z (S k) = CmpLT _

339−cmp (S k) Z = cmpGT _

339+cmp (S k) Z = CmpGT _

340cmp (S x) (S y) with (cmp x y)

341− cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k

341+ cmp (S x) (S (x + (S k))) | CmpLT k = CmpLT k

342− cmp (S x) (S x) | cmpEQ = cmpEQ

342+ cmp (S x) (S x) | CmpEQ = CmpEQ

343− cmp (S (y + (S k))) (S y) | cmpGT k = cmpGT k

343+ cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k

344

345--------------------------------------------------------------------------------

346-- Properties

@@ -626,9 +626,9 @@ total lteNTrue : (n : Nat) -> lte n n = True

626lteNTrue Z = Refl

627lteNTrue (S n) = lteNTrue n

628

629−total lteSuccZeroFalse : (n : Nat) -> lte (S n) Z = False

629+total LTESuccZeroFalse : (n : Nat) -> lte (S n) Z = False

630−lteSuccZeroFalse Z = Refl

630+LTESuccZeroFalse Z = Refl

631−lteSuccZeroFalse (S n) = Refl

631+LTESuccZeroFalse (S n) = Refl

632

633-- Minimum and maximum

634total maximumAssociative : (l,c,r : Nat) -> maximum l (maximum c r) = maximum (maximum l c) r

libs/prelude/Prelude/Pairs.idr+6−6

@@ -9,27 +9,27 @@ using (a : Type, P : a -> Type)

9

10 ||| Dependent pair where the first field is erased.

11 data Exists : (P : a -> Type) -> Type where

12− evidence : .(x : a) -> (pf : P x) -> Exists P

12+ Evidence : .(x : a) -> (pf : P x) -> Exists P

13

14 ||| Dependent pair where the second field is erased.

15 data Subset : (a : Type) -> (P : a -> Type) -> Type where

16− element : (x : a) -> .(pf : P x) -> Subset a P

16+ Element : (x : a) -> .(pf : P x) -> Subset a P

17

18 -- Monomorphic projections

19

20 namespace Exists

21 getWitness : Exists {a} P -> a

22− getWitness (evidence x pf) = x

22+ getWitness (Evidence x pf) = x

23

24 getProof : (x : Exists {a} P) -> P (getWitness x)

25− getProof (evidence x pf) = pf

25+ getProof (Evidence x pf) = pf

26

27 namespace Subset

28 getWitness : Subset a P -> a

29− getWitness (element x pf) = x

29+ getWitness (Element x pf) = x

30

31 getProof : (x : Subset a P) -> P (getWitness x)

32− getProof (element x pf) = pf

32+ getProof (Element x pf) = pf

33

34 namespace Sigma

35 getWitness : Sigma a P -> a

libs/prelude/Prelude/Strings.idr+2−2

@@ -74,11 +74,11 @@ data StrM : String -> Type where

74 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)

75

76||| Version of 'strHead' that statically verifies that the string is not empty.

77−strHead' : (x : String) -> so (not (x == "")) -> Char

77+strHead' : (x : String) -> So (not (x == "")) -> Char

78strHead' x p = assert_total $ prim__strHead x

79

80||| Version of 'strTail' that statically verifies that the string is not empty.

81−strTail' : (x : String) -> so (not (x == "")) -> String

81+strTail' : (x : String) -> So (not (x == "")) -> String

82strTail' x p = assert_total $ prim__strTail x

83

84-- we need the 'believe_me' because the operations are primitives

libs/prelude/Prelude/Vect.idr+14−14

@@ -64,35 +64,35 @@ init (x::y::ys) = x :: init (y::ys)

64

65||| Extract a particular element from a vector

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

67−index fZ (x::xs) = x

67+index FZ (x::xs) = x

68−index (fS k) (x::xs) = index k xs

68+index (FS k) (x::xs) = index k xs

69−index fZ [] impossible

69+index FZ [] impossible

70

71||| Insert an element at a particular index

72insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a

73−insertAt fZ y xs = y :: xs

73+insertAt FZ y xs = y :: xs

74−insertAt (fS k) y (x::xs) = x :: insertAt k y xs

74+insertAt (FS k) y (x::xs) = x :: insertAt k y xs

75−insertAt (fS k) y [] = absurd k

75+insertAt (FS k) y [] = absurd k

76

77||| Construct a new vector consisting of all but the indicated element

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

79−deleteAt fZ (x::xs) = xs

79+deleteAt FZ (x::xs) = xs

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

80+deleteAt {n = S m} (FS k) (x::xs) = x :: deleteAt k xs

81−deleteAt {n = Z} (fS k) (x::xs) = absurd k

81+deleteAt {n = Z} (FS k) (x::xs) = absurd k

82deleteAt _ [] impossible

83

84||| Replace an element at a particlar index with another

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

86−replaceAt fZ y (x::xs) = y :: xs

86+replaceAt FZ y (x::xs) = y :: xs

87−replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs

87+replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs

88

89||| Replace the element at a particular index with the result of applying a function to it

90||| @ i the index to replace at

91||| @ f the update function

92||| @ xs the vector to replace in

93updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t

94−updateAt fZ f (x::xs) = f x :: xs

94+updateAt FZ f (x::xs) = f x :: xs

95−updateAt (fS k) f (x::xs) = x :: updateAt k f xs

95+updateAt (FS k) f (x::xs) = x :: updateAt k f xs

96

97--------------------------------------------------------------------------------

98-- Subvectors

@@ -456,7 +456,7 @@ diag ((x::xs)::xss) = x :: diag (map tail xss)

456

457range : Vect n (Fin n)

458range {n=Z} = []

459−range {n=S _} = fZ :: map fS range

459+range {n=S _} = FZ :: map FS range

460

461||| Transpose a Vect of Vects, turning rows into columns and vice versa.

462|||

samples/interp-alt.idr+13−13

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

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

15

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

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

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

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

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

19

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

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

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

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

22+ lookup (FS i) (x :: xs) = lookup i xs

23

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

25 Var : (i : Fin n) -> Expr G (index i G)

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

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

42

43 eId : Expr G (TyFun TyInt TyInt)

44− eId = Lam (Var fZ)

44+ eId = Lam (Var FZ)

45

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

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

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 fZ) (Var (fS fZ))))

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 fZ) (Var (fS fZ))))) (Var fZ)) (Var fZ))

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 fZ)) (Var fZ))

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 fZ) (Val 0))

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

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

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

68+ eProg = Lam (Lam (Bind (App eDouble (Var (FS FZ)))

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

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+2−2

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

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

15

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

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

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

18− pop : HasType k G t -> HasType (fS k) (u :: 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

21 lookup stop (x :: xs) = x

src/Idris/AbsSyntaxTree.hs+1−1

@@ -496,7 +496,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

496 | CExport String -- export, with a C name

497 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension

498 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error

499− | Reflection -- a Reflecting function, compile-time only

499+ | Reflection -- a reflecting function, compile-time only

500 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

501 | Constructor -- Data constructor type

502 deriving (Show, Eq)

test/dsl001/test001.idr+3−3

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

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

15

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

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

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

18− pop : HasType k G t -> HasType (fS k) (u :: 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

21 lookup stop (x :: xs) = x

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

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

59

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

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

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

62

63 eDouble : Expr G (TyFun TyInt TyInt)

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

test/dsl002/Resimp.idr+2−2

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

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

47

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

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

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

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

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

51

52 data Env : Vect n Ty -> Type where

53 Nil : Env Nil

test/dsl003/DSLPi.idr+3−3

@@ -25,14 +25,14 @@ using (vars : Vect n Ty)

25dsl specs

26 pi = ForAll

27 variable = Var

28− index_first = fZ

28+ index_first = FZ

29− index_next = fS

29+ index_next = FS

30

31test2 : Spec []

32test2 = specs ((x, y : INT) -> x === y)

33

34test3 : Spec []

35−test3 = ForAll INT . ForAll INT . ItHolds $ Var (fS fZ) === Var fZ

35+test3 = ForAll INT . ForAll INT . ItHolds $ Var (FS FZ) === Var FZ

36

37test4 : test2 = test3

38test4 = Refl

test/dsl003/expected+1−1

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

1−ForAll INT (ForAll INT (ItHolds (Var (fS fZ) === Var fZ))) : Spec []

1+ForAll INT (ForAll INT (ItHolds (Var (FS FZ) === Var FZ))) : Spec []

2Refl : ARR BOOL (ARR INT UNIT) = ARR BOOL (ARR INT UNIT)

test/primitives003/test038.idr+4−4

@@ -52,10 +52,10 @@ main = do

52 putStrLn . show $ test (Left "hello") (Right "world")

53 putStrLn . show $ test (Left "hello") (Right False)

54 -- Fin

55− putStrLn . show $ test (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))

55+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))

56− (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))

56+ (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))

57− putStrLn . show $ test (the (Fin (S (S (S (Z))))) (fS (fS (fZ))))

57+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))

58− (the (Fin (S (S (S (Z))))) (fS (fZ)))

58+ (the (Fin (S (S (S (Z))))) (FS (FZ)))

59 -- Nat

60 putStrLn . show $ test (S (S (S Z))) (S (S (S Z)))

61 putStrLn . show $ test (S (S (S Z))) (S (S Z))

test/quasiquote003/NoInfer.idr+2−2

@@ -4,7 +4,7 @@ import Language.Reflection

4import Language.Reflection.Utils

5

6zzz2 : TT

7−zzz2 = `(fZ : Fin 3)

7+zzz2 = `(FZ : Fin 3)

8

9zzz : TT

10−zzz = `(fZ)

10+zzz = `(FZ)

test/reg018/reg018d.idr+3−3

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

3total

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

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

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

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

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

7+pull {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 fZ [0, 1, 2])

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

test/reg025/reg025.idr+5−5

@@ -21,18 +21,18 @@ Filled {n=n} = (\x => Not (Empty x))

21FullBoard : Board n -> Type

22FullBoard (MkBoard b) = All (All Filled) b

23

24−indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (fS i) (x::xs)

24+indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (FS i) (x::xs)

25indexStep = Refl

26

27find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)

28 -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))

29find _ Nil = Left Nil

30find {P} d (x::xs) with (d x)

31− | Yes prf = Right (x ** (prf, (fZ ** Refl)))

31+ | Yes prf = Right (x ** (prf, (FZ ** Refl)))

32 | No prf =

33 case find {P} d xs of

34 Right (y ** (prf', (i ** prf''))) =>

35− Right (y ** (prf', (fS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))

35+ Right (y ** (prf', (FS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))

36 Left prf' => Left (prf::prf')

37

38empty : (cell : Cell n) -> Dec (Empty cell)

@@ -60,11 +60,11 @@ emptyCell (MkBoard rs) =

60 helper Nil = Left Nil

61 helper (r::rs) =

62 case findEmptyInRow r of

63− Right (ci ** pf3) => Right (fZ ** (ci ** pf3))

63+ Right (ci ** pf3) => Right (FZ ** (ci ** pf3))

64 Left prf =>

65 case helper rs of

66 Left prf' => Left (prf::prf')

67− Right (ri ** (ci ** pf4)) => Right (fS ri ** (ci ** pf4))

67+ Right (ri ** (ci ** pf4)) => Right (FS ri ** (ci ** pf4))

68

69

70main : IO ()