edb9980 · Idris-dev · git.iko.soy

benchmarks/quasigroups/Solver.idr+2−2

compare with master

unifiedsplit

@@ -103,8 +103,8 @@ legalVal b (x, y) v =

103Filled : Cell n -> Type

104--Filled {n=n} x = Not (Empty x) -- TODO: Find out why this doesn't work

105Filled {n=n} = (\x => Not (Empty x))

106−--Filled {n=n} x = the (Maybe (Fin n)) Nothing = x -> _|_

106+--Filled {n=n} x = the (Maybe (Fin n)) Nothing = x -> Void

107−--Filled {n=n} = \x => the (Maybe (Fin n)) Nothing = x -> _|_

107+--Filled {n=n} = \x => the (Maybe (Fin n)) Nothing = x -> Void

108

109filled : (cell : Cell n) -> Dec (Filled cell)

110filled Nothing = No (\f => f Refl)

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

@@ -70,21 +70,21 @@ eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2

70 ok2 (Right x) = Refl

71

72||| Disjunction with false is a no-op

73−eitherBotLeft : Iso (Either _|_ a) a

73+eitherBotLeft : Iso (Either Void a) a

74eitherBotLeft = MkIso to from ok1 ok2

75− where to : Either _|_ a -> a

75+ where to : Either Void a -> a

76− to (Left x) = FalseElim x

76+ to (Left x) = VoidElim x

77 to (Right x) = x

78− from : a -> Either _|_ a

78+ from : a -> Either Void a

79 from = Right

80 ok1 : (x : a) -> to (from x) = x

81 ok1 x = Refl

82− ok2 : (x : Either _|_ a) -> from (to x) = x

82+ ok2 : (x : Either Void a) -> from (to x) = x

83− ok2 (Left x) = FalseElim x

83+ ok2 (Left x) = VoidElim x

84 ok2 (Right x) = Refl

85

86||| Disjunction with false is a no-op

87−eitherBotRight : Iso (Either a _|_) a

87+eitherBotRight : Iso (Either a Void) a

88eitherBotRight = isoTrans eitherComm eitherBotLeft

89

90||| Isomorphism is a congruence with regards to disjunction

@@ -145,11 +145,11 @@ pairUnitLeft : Iso ((), a) a

145pairUnitLeft = isoTrans pairComm pairUnitRight

146

147||| Conjunction preserves falsehood

148−pairBotLeft : Iso (_|_, a) _|_

148+pairBotLeft : Iso (Void, a) Void

149−pairBotLeft = MkIso fst FalseElim (\x => FalseElim x) (\y => FalseElim (fst y))

149+pairBotLeft = MkIso fst VoidElim (\x => VoidElim x) (\y => VoidElim (fst y))

150

151||| Conjunction preserves falsehood

152−pairBotRight : Iso (a, _|_) _|_

152+pairBotRight : Iso (a, Void) Void

153pairBotRight = isoTrans pairComm pairBotLeft

154

155||| Isomorphism is a congruence with regards to conjunction

@@ -240,9 +240,9 @@ maybeEither = MkIso to from iso1 iso2

240 iso2 (Just x) = Refl

241

242||| Maybe of void is just unit

243−maybeVoidUnit : Iso (Maybe _|_) ()

243+maybeVoidUnit : Iso (Maybe Void) ()

244−maybeVoidUnit = (Maybe _|_) ={ maybeEither }=

244+maybeVoidUnit = (Maybe Void) ={ maybeEither }=

245− (Either _|_ ()) ={ eitherBotLeft }=

245+ (Either Void ()) ={ eitherBotLeft }=

246 () QED

247

248eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))

@@ -280,16 +280,16 @@ maybeIsoS = MkIso forth back fb bf

280 fb FZ = Refl

281 fb (FS x) = Refl

282

283−finZeroBot : Iso (Fin 0) _|_

283+finZeroBot : Iso (Fin 0) Void

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

284+finZeroBot = MkIso (\x => VoidElim (uninhabited x))

285− (\x => FalseElim x)

285+ (\x => VoidElim x)

286− (\x => FalseElim x)

286+ (\x => VoidElim x)

287− (\x => FalseElim (uninhabited x))

287+ (\x => VoidElim (uninhabited x))

288

289eitherFinPlus : Iso (Either (Fin m) (Fin n)) (Fin (m + n))

290eitherFinPlus {m = Z} {n=n} =

291 (Either (Fin 0) (Fin n)) ={ eitherCongLeft finZeroBot }=

292− (Either _|_ (Fin n)) ={ eitherBotLeft }=

292+ (Either Void (Fin n)) ={ eitherBotLeft }=

293 (Fin n) QED

294eitherFinPlus {m = S k} {n=n} =

295 (Either (Fin (S k)) (Fin n)) ={ eitherCongLeft (isoSym maybeIsoS) }=

@@ -302,8 +302,8 @@ eitherFinPlus {m = S k} {n=n} =

302finPairTimes : Iso (Fin m, Fin n) (Fin (m * n))

303finPairTimes {m = Z} {n=n} =

304 (Fin Z, Fin n) ={ pairCongLeft finZeroBot }=

305− (_|_, Fin n) ={ pairBotLeft }=

305+ (Void, Fin n) ={ pairBotLeft }=

306− _|_ ={ isoSym finZeroBot }=

306+ Void ={ isoSym finZeroBot }=

307 (Fin Z) QED

308finPairTimes {m = S k} {n=n} =

309 (Fin (S k), Fin n) ={ pairCongLeft (isoSym maybeIsoS) }=

libs/base/Data/Heap.idr+3−3

@@ -135,12 +135,12 @@ instance Ord a => JoinSemilattice (MaxiphobicHeap a) where

135-- Properties

136--------------------------------------------------------------------------------

137

138−total absurdBoolDischarge : False = True -> _|_

138+total absurdBoolDischarge : False = True -> Void

139absurdBoolDischarge p = replace {P = disjointTy} p ()

140 where

141 total disjointTy : Bool -> Type

142 disjointTy False = ()

143− disjointTy True = _|_

143+ disjointTy True = Void

144

145total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z

146isEmptySizeZero Empty p = Refl

@@ -169,7 +169,7 @@ mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =

169

170isEmptySizeZeroNodeAbsurd = proof {

171 intros;

172− refine FalseElim;

172+ refine VoidElim;

173 refine absurdBoolDischarge;

174 exact p;

175}

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

@@ -32,7 +32,7 @@ isElem x (y :: xs) with (decEq x y)

32 isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)

33 where

34 mkNo : {xs' : List a} ->

35− ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->

35+ ((x' = y') -> Void) -> (Elem x' xs' -> Void) ->

36− Elem x' (y' :: xs') -> _|_

36+ Elem x' (y' :: xs') -> Void

37 mkNo f g Here = f Refl

38 mkNo f g (There x) = g x

libs/base/Data/Vect.idr+1−1

@@ -15,7 +15,7 @@ data Elem : a -> Vect k a -> Type where

15 There : Elem x xs -> Elem x (y::xs)

16

17||| Nothing can be in an empty Vect

18−noEmptyElem : {x : a} -> Elem x [] -> _|_

18+noEmptyElem : {x : a} -> Elem x [] -> Void

19noEmptyElem Here impossible

20

21||| An item not in the head and not in the tail is not in the Vect at all

libs/base/Data/Vect/Quantifiers.idr+3−3

@@ -10,7 +10,7 @@ data Any : (P : a -> Type) -> Vect n a -> Type where

10 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)

11

12||| No element of an empty vector satisfies any property

13−anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_

13+anyNilAbsurd : {P : a -> Type} -> Any P Nil -> Void

14anyNilAbsurd (Here _) impossible

15anyNilAbsurd (There _) impossible

16

@@ -48,11 +48,11 @@ negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => N

48negAnyAll {xs=Nil} _ = Nil

49negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))

50

51−notAllHere : {P : a -> Type} -> {xs : Vect n a} -> Not (P x) -> All P (x :: xs) -> _|_

51+notAllHere : {P : a -> Type} -> {xs : Vect n a} -> Not (P x) -> All P (x :: xs) -> Void

52notAllHere _ Nil impossible

53notAllHere np (p :: _) = np p

54

55−notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :: xs) -> _|_

55+notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :: xs) -> Void

56notAllThere _ Nil impossible

57notAllThere np (_ :: ps) = np ps

58

libs/base/Data/ZZ.idr+1−1

@@ -122,7 +122,7 @@ posInjective Refl = Refl

122negSInjective : NegS n = NegS m -> n = m

123negSInjective Refl = Refl

124

125−posNotNeg : Pos n = NegS m -> _|_

125+posNotNeg : Pos n = NegS m -> Void

126posNotNeg Refl impossible

127

128-- Decidable equality

libs/base/Decidable/Order.idr+3−3

@@ -84,15 +84,15 @@ LTEIsAntisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm) with (LTEIsAntisy

84instance Poset Nat LTE where

85 antisymmetric = LTEIsAntisymmetric

86

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

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

88zeroNeverGreater {n} LTEZero impossible

89zeroNeverGreater {n} (LTESucc _) impossible

90

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

92zeroAlwaysSmaller = LTEZero

93

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

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

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

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

96ltesuccinjective {n} {m} disprf LTEZero impossible

97

98

libs/prelude/Builtins.idr+8−2

@@ -29,8 +29,14 @@ data Pair : (A : Type) -> (B : Type) -> Type where

29data Sigma : (a : Type) -> (P : a -> Type) -> Type where

30 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P

31

32+||| The empty type, also known as the trivially false proposition.

33+|||

34+||| Use `VoidElim` or `absurd` to prove anything if you have a variable of type `Void` in scope.

35+%elim data Void : Type where

36+

32−||| The eliminator for the empty type.

37+||| The eliminator for the `Void` type.

33−FalseElim : _|_ -> a

38+VoidElim : Void -> a

39+VoidElim {a} v = elim_for Void (\_ => a) v

34

40

35||| For 'symbol syntax. 'foo becomes Symbol_ "foo"

41||| For 'symbol syntax. 'foo becomes Symbol_ "foo"

36data Symbol_ : String -> Type where

42data Symbol_ : String -> Type where

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

@@ -13,7 +13,7 @@ import Prelude.Maybe

13--------------------------------------------------------------------------------

14

15||| The negation of equality is symmetric (follows from symmetry of equality)

16−total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)

16+total negEqSym : {a : t} -> {b : t} -> (a = b -> Void) -> (b = a -> Void)

17negEqSym p h = p (sym h)

18

19

@@ -36,7 +36,7 @@ instance DecEq () where

36--------------------------------------------------------------------------------

37-- Booleans

38--------------------------------------------------------------------------------

39−total trueNotFalse : True = False -> _|_

39+total trueNotFalse : True = False -> Void

40trueNotFalse Refl impossible

41

42instance DecEq Bool where

@@ -49,7 +49,7 @@ instance DecEq Bool where

49-- Nat

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

51

52−total OnotS : Z = S n -> _|_

52+total OnotS : Z = S n -> Void

53OnotS Refl impossible

54

55instance DecEq Nat where

@@ -64,7 +64,7 @@ instance DecEq Nat where

64-- Maybe

65--------------------------------------------------------------------------------

66

67−total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> _|_

67+total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> Void

68nothingNotJust Refl impossible

69

70instance (DecEq t) => DecEq (Maybe t) where

@@ -79,7 +79,7 @@ instance (DecEq t) => DecEq (Maybe t) where

79-- Either

80--------------------------------------------------------------------------------

81

82−total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _|_

82+total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> Void

83leftNotRight Refl impossible

84

85instance (DecEq a, DecEq b) => DecEq (Either a b) where

@@ -96,7 +96,7 @@ 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 -> Void

100FZNotFS Refl impossible

101

102instance DecEq (Fin n) where

@@ -111,16 +111,16 @@ instance DecEq (Fin n) where

111-- Tuple

112--------------------------------------------------------------------------------

113

114−lemma_both_neq : {x : a, y : b, x' : c, y' : d} -> (x = x' -> _|_) -> (y = y' -> _|_) -> ((x, y) = (x', y') -> _|_)

114+lemma_both_neq : {x : a, y : b, x' : c, y' : d} -> (x = x' -> Void) -> (y = y' -> Void) -> ((x, y) = (x', y') -> Void)

115lemma_both_neq p_x_not_x' p_y_not_y' Refl = p_x_not_x' Refl

116

117−lemma_snd_neq : {x : a, y : b, y' : d} -> (x = x) -> (y = y' -> _|_) -> ((x, y) = (x, y') -> _|_)

117+lemma_snd_neq : {x : a, y : b, y' : d} -> (x = x) -> (y = y' -> Void) -> ((x, y) = (x, y') -> Void)

118lemma_snd_neq Refl p Refl = p Refl

119

120lemma_fst_neq_snd_eq : {x : a, x' : b, y : c, y' : d} ->

121− (x = x' -> _|_) ->

121+ (x = x' -> Void) ->

122 (y = y') ->

123− ((x, y) = (x', y) -> _|_)

123+ ((x, y) = (x', y) -> Void)

124lemma_fst_neq_snd_eq p_x_not_x' Refl Refl = p_x_not_x' Refl

125

126instance (DecEq a, DecEq b) => DecEq (a, b) where

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

137-- List

138--------------------------------------------------------------------------------

139

140−lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {a = t} -> _|_)

140+lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {a = t} -> Void)

141lemma_val_not_nil Refl impossible

142

143−lemma_x_eq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y) -> (xs = ys -> _|_) -> ((x :: xs) = (y :: ys) -> _|_)

143+lemma_x_eq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void)

144lemma_x_eq_xs_neq Refl p Refl = p Refl

145

146−lemma_x_neq_xs_eq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> _|_) -> (xs = ys) -> ((x :: xs) = (y :: ys) -> _|_)

146+lemma_x_neq_xs_eq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> Void) -> (xs = ys) -> ((x :: xs) = (y :: ys) -> Void)

147lemma_x_neq_xs_eq p Refl Refl = p Refl

148

149−lemma_x_neq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> _|_) -> (xs = ys -> _|_) -> ((x :: xs) = (y :: ys) -> _|_)

149+lemma_x_neq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> Void) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void)

150lemma_x_neq_xs_neq p p' Refl = p Refl

151

152instance DecEq a => DecEq (List a) where

@@ -203,7 +203,7 @@ instance DecEq Int where

203 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

204 where primitiveEq : x = y

205 primitiveEq = believe_me (Refl {x})

206− postulate primitiveNotEq : x = y -> _|_

206+ postulate primitiveNotEq : x = y -> Void

207

208--------------------------------------------------------------------------------

209-- Char

@@ -213,7 +213,7 @@ instance DecEq Char where

213 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

214 where primitiveEq : x = y

215 primitiveEq = believe_me (Refl {x})

216− postulate primitiveNotEq : x = y -> _|_

216+ postulate primitiveNotEq : x = y -> Void

217

218--------------------------------------------------------------------------------

219-- Integer

@@ -223,7 +223,7 @@ instance DecEq Integer where

223 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

224 where primitiveEq : x = y

225 primitiveEq = believe_me (Refl {x})

226− postulate primitiveNotEq : x = y -> _|_

226+ postulate primitiveNotEq : x = y -> Void

227

228--------------------------------------------------------------------------------

229-- Float

@@ -233,7 +233,7 @@ instance DecEq Float where

233 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

234 where primitiveEq : x = y

235 primitiveEq = believe_me (Refl {x})

236− postulate primitiveNotEq : x = y -> _|_

236+ postulate primitiveNotEq : x = y -> Void

237

238--------------------------------------------------------------------------------

239-- String

@@ -243,6 +243,6 @@ instance DecEq String where

243 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

244 where primitiveEq : x = y

245 primitiveEq = believe_me (Refl {x})

246− postulate primitiveNotEq : x = y -> _|_

246+ postulate primitiveNotEq : x = y -> Void

247

248

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

@@ -3,7 +3,7 @@ module Prelude.Basics

3import Builtins

4

5Not : Type -> Type

6−Not a = a -> _|_

6+Not a = a -> Void

7

8||| Identity function.

9id : a -> a

@@ -55,5 +55,5 @@ data Dec : Type -> Type where

55

56 ||| The case where the property holding would be a contradiction

57 ||| @ contra a demonstration that A would be a contradiction

58− No : {A : Type} -> (contra : A -> _|_) -> Dec A

58+ No : {A : Type} -> (contra : A -> Void) -> Dec A

59

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

@@ -28,11 +28,11 @@ instance Eq (Fin n) where

28 (==) _ _ = False

29

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

31−FinZAbsurd : Fin Z -> _|_

31+FinZAbsurd : Fin Z -> Void

32FinZAbsurd FZ impossible

33

34FinZElim : Fin Z -> a

35−FinZElim x = FalseElim (FinZAbsurd x)

35+FinZElim x = VoidElim (FinZAbsurd x)

36

37||| Convert a Fin to a Nat

38finToNat : Fin n -> Nat

libs/prelude/Prelude/Uninhabited.idr+3−3

@@ -6,9 +6,9 @@ import Builtins

6class Uninhabited t where

7 ||| If I have a t, I've had a contradiction

8 ||| @ t the uninhabited type

9− total uninhabited : t -> _|_

9+ total uninhabited : t -> Void

10

11−instance Uninhabited _|_ where

11+instance Uninhabited Void where

12 uninhabited a = a

13

14||| Use an absurd assumption to discharge a proof obligation

@@ -16,4 +16,4 @@ instance Uninhabited _|_ where

16||| @ a the goal type

17||| @ h the contradictory hypothesis

18absurd : Uninhabited t => (h : t) -> a

19−absurd h = FalseElim (uninhabited h)

19+absurd h = VoidElim (uninhabited h)

src/Idris/AbsSyntax.hs−2

@@ -1040,7 +1040,6 @@ getPriority i tm = 1 -- pri tm

1040 [] -> 0 -- must be locally bound, if it's not an error...

1041 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))

1042 pri (PTrue _ _) = 0

1043− pri (PFalse _) = 0

1044 pri (PRefl _ _) = 1

1043 pri (PRefl _ _) = 1

1045 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))

1044 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))

1046 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

1045 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

@@ -1772,7 +1771,6 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1772 match (PRefl _ _) (PRefl _ _) = return []

1771 match (PRefl _ _) (PRefl _ _) = return []

1773 match (PResolveTC _) (PResolveTC _) = return []

1772 match (PResolveTC _) (PResolveTC _) = return []

1774 match (PTrue _ _) (PTrue _ _) = return []

1773 match (PTrue _ _) (PTrue _ _) = return []

1775− match (PFalse _) (PFalse _) = return []

1776 match (PReturn _) (PReturn _) = return []

1774 match (PReturn _) (PReturn _) = return []

1777 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'

1775 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'

1778 ms <- match' s s'

1776 ms <- match' s s'

src/Idris/AbsSyntaxTree.hs+5−11

@@ -238,7 +238,7 @@ deriving instance NFData CGInfo

238primDefs = [sUN "unsafePerformPrimIO",

239 sUN "mkLazyForeignPrim",

240 sUN "mkForeignPrim",

241− sUN "FalseElim"]

241+ sUN "VoidElim"]

242

243-- information that needs writing for the current module's .ibc file

244data IBCWrite = IBCFix FixDecl

@@ -711,7 +711,6 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

711 | PMatchApp FC Name -- ^ Make an application by type matching

712 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

713 | PTrue FC PunInfo -- ^ Unit type..?

714− | PFalse FC -- ^ _|_

715 | PRefl FC PTerm -- ^ The canonical proof of the equality type

714 | PRefl FC PTerm -- ^ The canonical proof of the equality type

716 | PResolveTC FC -- ^ Solve this dictionary by type class resolution

715 | PResolveTC FC -- ^ Solve this dictionary by type class resolution

717 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B

716 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B

@@ -1067,7 +1066,7 @@ getInferType (App (App _ ty) _) = ty

1067

1066

1068-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign

1067-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign

1069

1068

1070−primNames = [falseTy, eqTy, eqCon, inferTy, inferCon]

1069+primNames = [eqTy, eqCon, inferTy, inferCon]

1071

1070

1072unitTy = sUN "Unit"

1071unitTy = sUN "Unit"

1073unitCon = sUN "MkUnit"

1072unitCon = sUN "MkUnit"

@@ -1076,11 +1075,9 @@ unitCon = sUN "MkUnit"

1076falseDoc = fmap (const Nothing) . parseDocstring . T.pack $

1075falseDoc = fmap (const Nothing) . parseDocstring . T.pack $

1077 "The empty type, also known as the trivially false proposition." ++

1076 "The empty type, also known as the trivially false proposition." ++

1078 "\n\n" ++

1077 "\n\n" ++

1079− "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++

1078+ "Use `VoidElim` or `absurd` to prove anything if you have a variable " ++

1080− "of type `_|_` in scope."

1079+ "of type `Void` in scope."

1081−falseTy = sMN 0 "__False"

1080+falseTy = sUN "Void"

1082−falseDecl = PDatadecl falseTy PType []

1083−falseOpts = []

1084

1081

1085pairTy = sUN "Pair"

1082pairTy = sUN "Pair"

1086pairCon = sUN "MkPair"

1083pairCon = sUN "MkPair"

@@ -1316,7 +1313,6 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1316 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1313 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1317 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1314 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1318 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1315 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1319− prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"

1320 prettySe p bnd (PEq _ lt rt l r)

1316 prettySe p bnd (PEq _ lt rt l r)

1321 | ppopt_impl ppo =

1317 | ppopt_impl ppo =

1322 bracket p 1 $

1318 bracket p 1 $

@@ -1486,7 +1482,6 @@ prettyName infixParen showNS bnd n

1486 baseName (UN n) = T.unpack n

1482 baseName (UN n) = T.unpack n

1487 baseName (NS n ns) = baseName n

1483 baseName (NS n ns) = baseName n

1488 baseName (MN i s) = T.unpack s

1484 baseName (MN i s) = T.unpack s

1489− baseName n | n == falseTy = "_|_"

1490 baseName other = show other

1485 baseName other = show other

1491 nameSpace = case n of

1486 nameSpace = case n of

1492 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""

1487 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""

@@ -1616,7 +1611,6 @@ instance Sized PTerm where

1616 size (PAppBind fc name args) = 1 + size args

1611 size (PAppBind fc name args) = 1 + size args

1617 size (PCase fc trm bdy) = 1 + size trm + size bdy

1612 size (PCase fc trm bdy) = 1 + size trm + size bdy

1618 size (PTrue fc _) = 1

1613 size (PTrue fc _) = 1

1619− size (PFalse fc) = 1

1620 size (PRefl fc _) = 1

1614 size (PRefl fc _) = 1

1621 size (PResolveTC fc) = 1

1615 size (PResolveTC fc) = 1

1622 size (PEq fc _ _ left right) = 1 + size left + size right

1616 size (PEq fc _ _ left right) = 1 + size left + size right

src/Idris/Apropos.hs−1

@@ -38,7 +38,6 @@ instance Apropos Name where

38 isApropos str (NS n' ns) = isApropos str n' || any (textIn str) ns

39 -- Handle special names from stdlib

40 isApropos str n | (n == unitTy || n == unitCon) && str == T.pack "()" = True

41− | n == falseTy && str == T.pack "_|_" = True

42 | (n == pairTy || n == pairCon) && str == T.pack "," = True

41 | (n == pairTy || n == pairCon) && str == T.pack "," = True

43 | n == eqTy && str == T.pack "=" = True

42 | n == eqTy && str == T.pack "=" = True

44 | n == eqCon && (T.toLower str) == T.pack "Refl" = True

43 | n == eqCon && (T.toLower str) == T.pack "Refl" = True

src/Idris/DeepSeq.hs−1

@@ -202,7 +202,6 @@ instance NFData PTerm where

202 rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

203 rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

204 rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

205− rnf (PFalse x1) = rnf x1 `seq` ()

206 rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

205 rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

207 rnf (PResolveTC x1) = rnf x1 `seq` ()

206 rnf (PResolveTC x1) = rnf x1 `seq` ()

208 rnf (PEq x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

207 rnf (PEq x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

src/Idris/Delaborate.hs−1

@@ -50,7 +50,6 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

50 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))

51 de env _ (P _ n _) | n == unitTy = PTrue un IsType

52 | n == unitCon = PTrue un IsTerm

53− | n == falseTy = PFalse un

54 | Just n' <- lookup n env = PRef un n'

53 | Just n' <- lookup n env = PRef un n'

55 | otherwise

54 | otherwise

56 = case lookup n (idris_metavars ist) of

55 = case lookup n (idris_metavars ist) of

src/Idris/Docs.hs−2

@@ -186,8 +186,6 @@ docFun n

186 where funName :: Name -> String

187 funName (UN n) = str n

188 funName (NS n _) = funName n

189− funName n

190− | n == falseTy = "_|_"

191

189

192getPArgNames :: PTerm -> [(Name, Docstring (Maybe Term))] -> [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))]

190getPArgNames :: PTerm -> [(Name, Docstring (Maybe Term))] -> [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))]

193getPArgNames (PPi plicity name ty body) ds =

191getPArgNames (PPi plicity name ty body) ds =

src/Idris/ElabDecls.hs+4−4

@@ -77,10 +77,10 @@ elabPrims :: Idris ()

77elabPrims = do mapM_ (elabDecl' EAll recinfo)

78 (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)

79 (zip4

80− [inferOpts, falseOpts, eqOpts]

80+ [inferOpts, eqOpts]

81− [inferDecl, falseDecl, eqDecl]

81+ [inferDecl, eqDecl]

82− [emptyDocstring, falseDoc, eqDoc]

82+ [emptyDocstring, eqDoc]

83− [[], [], eqParamDoc]))

83+ [[], eqParamDoc]))

84 addNameHint eqTy (sUN "prf")

85 mapM_ elabPrim primitives

86 -- Special case prim__believe_me because it doesn't work on just constants

src/Idris/ElabTerm.hs−1

@@ -251,7 +251,6 @@ elab ist info emode opts fn tm

251 case g of

252 TType _ -> elab' ina (PRef fc unitTy)

253 _ -> elab' ina (PRef fc unitCon)

254− elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)

255 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

254 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

256 = do g <- goal; resolveTC False 5 g fn ist

255 = do g <- goal; resolveTC False 5 g fn ist

257 elab' ina (PResolveTC fc)

256 elab' ina (PResolveTC fc)

src/Idris/Erasure.hs−3

@@ -342,13 +342,10 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

342

343 -- sanity check: machine-generated names shouldn't occur at top-level

344 | MN _ _ <- n

345− , n `notElem` specialMNs

346 = error $ "erasure analysis: variable " ++ show n ++ " unbound in " ++ show (S.toList cd)

345 = error $ "erasure analysis: variable " ++ show n ++ " unbound in " ++ show (S.toList cd)

347

346

348 -- assumed to be a global reference

347 -- assumed to be a global reference

349 | otherwise = M.singleton cd (M.singleton (n, Result) S.empty)

348 | otherwise = M.singleton cd (M.singleton (n, Result) S.empty)

350− where

351− specialMNs = [falseTy]

352

349

353 -- dependencies of de bruijn variables are described in `bs'

350 -- dependencies of de bruijn variables are described in `bs'

354 getDepsTerm vs bs cd (V i) = snd (bs !! i) cd

351 getDepsTerm vs bs cd (V i) = snd (bs !! i) cd

src/Idris/Error.hs−1

@@ -99,7 +99,6 @@ warnDisamb ist (PMatchApp _ _) = return ()

99warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>

100 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases

101warnDisamb ist (PTrue _ _) = return ()

102−warnDisamb ist (PFalse _) = return ()

103warnDisamb ist (PRefl _ tm) = warnDisamb ist tm

102warnDisamb ist (PRefl _ tm) = warnDisamb ist tm

104warnDisamb ist (PResolveTC _) = return ()

103warnDisamb ist (PResolveTC _) = return ()

105warnDisamb ist (PEq _ a b x y) = warnDisamb ist a >> warnDisamb ist b >>

104warnDisamb ist (PEq _ a b x y) = warnDisamb ist a >> warnDisamb ist b >>

src/Idris/IBC.hs−4

@@ -1435,8 +1435,6 @@ instance Binary PTerm where

1435 PTrue x1 x2 -> do putWord8 12

1436 put x1

1437 put x2

1438− PFalse x1 -> do putWord8 13

1439− put x1

1440 PRefl x1 x2 -> do putWord8 14

1438 PRefl x1 x2 -> do putWord8 14

1441 put x1

1439 put x1

1442 put x2

1440 put x2

@@ -1553,8 +1551,6 @@ instance Binary PTerm where

1553 12 -> do x1 <- get

1551 12 -> do x1 <- get

1554 x2 <- get

1552 x2 <- get

1555 return (PTrue x1 x2)

1553 return (PTrue x1 x2)

1556− 13 -> do x1 <- get

1557− return (PFalse x1)

1558 14 -> do x1 <- get

1554 14 -> do x1 <- get

1559 x2 <- get

1555 x2 <- get

1560 return (PRefl x1 x2)

1556 return (PRefl x1 x2)

src/Idris/ParseExpr.hs+2−5

@@ -293,7 +293,7 @@ SimpleExpr ::=

293 | Bracketed

294 | Constant

295 | Type

296− | '_|_'

296+ | 'Void'

297 | Quasiquote

298 | Unquote

299 | '_'

@@ -333,9 +333,6 @@ simpleExpr syn =

333 fc <- getFC

334 return (PAppBind fc s [])

335 <|> bracketed (disallowImp syn)

336− <|> do symbol "_|_"

337− fc <- getFC

338− return (PFalse fc)

339 <|> quasiquote syn

336 <|> quasiquote syn

340 <|> unquote syn

337 <|> unquote syn

341 <|> do lchar '_'; return Placeholder

338 <|> do lchar '_'; return Placeholder

@@ -1307,7 +1304,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

1307 return (TDocStr (Right c)))

1304 return (TDocStr (Right c)))

1308 <|> try (do reserved "doc"

1305 <|> try (do reserved "doc"

1309 whiteSpace

1306 whiteSpace

1310− n <- (fnName <|> (string "_|_" >> return falseTy))

1307+ n <- fnName

1311 eof

1308 eof

1312 return (TDocStr (Left n)))

1309 return (TDocStr (Left n)))

1313 <|> try (do reserved "search"

1310 <|> try (do reserved "search"

src/Idris/REPLParser.hs+1−6

@@ -208,14 +208,9 @@ cmd_doc name = do

208 eof

209 return $ Right (DocStr (Right c))

210

211− let bottom = do

212− P.string "_|_"

213− eof

214− return $ Right (DocStr (Left falseTy))

215−

216 let fnName = fnNameArg name (\n -> DocStr (Left n))

211 let fnName = fnNameArg name (\n -> DocStr (Left n))

217

212

218− try constant <|> try bottom <|> fnName

213+ try constant <|> fnName

219

214

220cmd_consolewidth :: String -> P.IdrisParser (Either String Command)

215cmd_consolewidth :: String -> P.IdrisParser (Either String Command)

221cmd_consolewidth name = do

216cmd_consolewidth name = do

test/ffi005/Postulate.idr+1−1

@@ -5,7 +5,7 @@ import Providers

5%language TypeProviders

6

7bad : IO (Provider Type)

8−bad = return $ pure _|_

8+bad = return $ pure Void

9

10%provide postulate oops with bad

11

test/proof005/DefaultArgSubstitutionSuccess.idr+3−3

@@ -2,7 +2,7 @@ module DefaultArgSubstitutionSuccess

2

3DecProofType : {a:Type} -> Dec a -> Type

4DecProofType {a} (Yes _) = a

5−DecProofType {a} (No _) = a -> _|_

5+DecProofType {a} (No _) = a -> Void

6

7decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec

8decProof (Yes x) = x

@@ -18,7 +18,7 @@ argsAreSame _ _ = ()

18

19

20argsAreDiff : (n:Nat) -> (m:Nat)

21− -> { default (decProof (decEq m n)) same : (m=n) -> _|_ } -> ()

21+ -> { default (decProof (decEq m n)) same : (m=n) -> Void } -> ()

22argsAreDiff _ _ = ()

23

24

@@ -28,7 +28,7 @@ data SameNats : Type where

28

29data DiffNats : Type where

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

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

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

32

33

34zArgsAreSame : ()

test/proof006/DefaultArgSubstitutionSyntax.idr+2−2

@@ -2,7 +2,7 @@ module DefaultArgSubstitutionSyntax

2

3DecProofType : {a:Type} -> Dec a -> Type

4DecProofType {a} (Yes _) = a

5−DecProofType {a} (No _) = a -> _|_

5+DecProofType {a} (No _) = a -> Void

6

7decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec

8decProof (Yes x) = x

@@ -16,7 +16,7 @@ syntax "{{" [prfname] ":" "accept" [dec] "}}" "->" [ret]

16 = { default (decProof dec) prfname : DecType dec } -> ret

17

18syntax "{{" [prfname] ":" "reject" [dec] "}}" "->" [ret]

19− = { default (decProof dec) prfname : DecType dec -> _|_ } -> ret

19+ = { default (decProof dec) prfname : DecType dec -> Void } -> ret

20

21

22argsAreSame : (n:Nat) -> (m:Nat)

test/reg002/reg002.idr+4−4

@@ -10,16 +10,16 @@ S : CoNat -> CoNat

10S (Co n) = Co (S n)

11S Infinity = Infinity

12

13−Sn_notzero : Main.S n = Co 0 -> _|_

13+Sn_notzero : Main.S n = Co 0 -> Void

14Sn_notzero = believe_me

15

16−S_Co_not_Inf : Main.S (Co n) = Infinity -> _|_

16+S_Co_not_Inf : Main.S (Co n) = Infinity -> Void

17S_Co_not_Inf = believe_me

18

19S_inj : (n : CoNat) -> (m : CoNat) -> Main.S n = Main.S m -> n = m

20S_inj (Co n) (Co _) Refl = Refl

21−S_inj (Co n) Infinity p = FalseElim (S_Co_not_Inf p)

21+S_inj (Co n) Infinity p = VoidElim (S_Co_not_Inf p)

22−S_inj Infinity (Co m) p = FalseElim (S_Co_not_Inf (sym p))

22+S_inj Infinity (Co m) p = VoidElim (S_Co_not_Inf (sym p))

23S_inj Infinity Infinity Refl = Refl

24

25swap : {n : Nat} -> Vect n a -> Vect n a

test/reg012/reg012.lidr+2−2

@@ -4,11 +4,11 @@

4> soElim C coh .True .Oh = coh

5

6> soFalseElim : So False -> a

7−> soFalseElim x = FalseElim (soElim C () False x)

7+> soFalseElim x = VoidElim (soElim C () False x)

8> where

9> C : (b : Bool) -> So b -> Type

10> C True s = ()

11−> C False s = _|_

11+> C False s = Void

12

13> soTrue : So b -> b = True

14> soTrue {b = False} x = soFalseElim x

test/reg035/reg035b.idr+1−1

@@ -6,6 +6,6 @@ finZEmpty : Fin Z -> a

6fins : (n : Nat) -> (xs : Vect n (Fin n) ** ((x : Fin n) -> Elem x xs))

7fins Z = ([] ** (finZEmpty {a=_}))

8

9−-- f : (a : Nat) -> a = S a -> _|_

9+-- f : (a : Nat) -> a = S a -> Void

10-- f a = believe_me

11

test/reg041/ott.idr+1−1

@@ -11,7 +11,7 @@ mutual

11

12 El : U -> Type

13 El u = U

14− El zero = _|_

14+ El zero = Void

15 El one = ()

16 El two = Bool

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

test/reg049/reg049.idr+2−2

@@ -1,5 +1,5 @@

1data Foo : Type where

2− Bogus : _|_

2+ Bogus : Void

3

4−uhOh : _|_

4+uhOh : Void

5uhOh = Bogus

test/totality002/test017b.idr+1−1

@@ -1,5 +1,5 @@

1module foo

2

3−total foo : _|_

3+total foo : Void

4foo = foo

5

test/tutorial004/tutorial004.idr+5−5

@@ -5,23 +5,23 @@ fiveIsFive = Refl

5twoPlusTwo : 2 + 2 = 4

6twoPlusTwo = Refl

7

8−total disjoint : (n : Nat) -> Z = S n -> _|_

8+total disjoint : (n : Nat) -> Z = S n -> Void

9disjoint n p = replace {P = disjointTy} p ()

10 where

11 disjointTy : Nat -> Type

12 disjointTy Z = ()

13− disjointTy (S k) = _|_

13+ disjointTy (S k) = Void

14

15−total acyclic : (n : Nat) -> n = S n -> _|_

15+total acyclic : (n : Nat) -> n = S n -> Void

16acyclic Z p = disjoint _ p

17acyclic (S k) p = acyclic k (succInjective _ _ p)

18

19−empty1 : _|_

19+empty1 : Void

20empty1 = hd [] where

21 hd : List a -> a

22 hd (x :: xs) = x

23

24−empty2 : _|_

24+empty2 : Void

25empty2 = empty2

26

27plusReduces : (n:Nat) -> plus Z n = n