d6981dc · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

@@ -73,14 +73,14 @@ eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2

73eitherBotLeft : Iso (Either Void a) a

74eitherBotLeft = MkIso to from ok1 ok2

75 where to : Either Void a -> a

76− to (Left x) = VoidElim x

76+ to (Left x) = void x

77 to (Right x) = x

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 Void a) -> from (to x) = x

83− ok2 (Left x) = VoidElim x

83+ ok2 (Left x) = void x

84 ok2 (Right x) = Refl

85

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

@@ -146,7 +146,7 @@ pairUnitLeft = isoTrans pairComm pairUnitRight

146

147||| Conjunction preserves falsehood

148pairBotLeft : Iso (Void, a) Void

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

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

150

151||| Conjunction preserves falsehood

152pairBotRight : Iso (a, Void) Void

@@ -281,10 +281,10 @@ maybeIsoS = MkIso forth back fb bf

281 fb (FS x) = Refl

282

283finZeroBot : Iso (Fin 0) Void

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

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

285− (\x => VoidElim x)

285+ (\x => void x)

286− (\x => VoidElim x)

286+ (\x => void x)

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

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

288

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

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

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

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

169

170isEmptySizeZeroNodeAbsurd = proof {

171 intros;

172− refine VoidElim;

172+ refine void;

173 refine absurdBoolDischarge;

174 exact p;

175}

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

@@ -92,7 +92,7 @@ total zeroAlwaysSmaller : {n : Nat} -> LTE Z n

92zeroAlwaysSmaller = LTEZero

93

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

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

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

96ltesuccinjective {n} {m} disprf LTEZero impossible

97

98

libs/prelude/Builtins.idr+3−3

@@ -31,12 +31,12 @@ data Sigma : (a : Type) -> (P : a -> Type) -> Type where

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.

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

35%elim data Void : Type where

36

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

38−VoidElim : Void -> a

38+void : Void -> a

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

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

40

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

42data Symbol_ : String -> Type where

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

@@ -32,7 +32,7 @@ FinZAbsurd : Fin Z -> Void

32FinZAbsurd FZ impossible

33

34FinZElim : Fin Z -> a

35−FinZElim x = VoidElim (FinZAbsurd x)

35+FinZElim x = void (FinZAbsurd x)

36

37||| Convert a Fin to a Nat

38finToNat : Fin n -> Nat

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

@@ -16,4 +16,4 @@ instance Uninhabited Void where

16||| @ a the goal type

17||| @ h the contradictory hypothesis

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

19−absurd h = VoidElim (uninhabited h)

19+absurd h = void (uninhabited h)

src/Idris/AbsSyntaxTree.hs+2−2

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

238primDefs = [sUN "unsafePerformPrimIO",

239 sUN "mkLazyForeignPrim",

240 sUN "mkForeignPrim",

241− sUN "VoidElim"]

241+ sUN "void"]

242

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

244data IBCWrite = IBCFix FixDecl

@@ -1075,7 +1075,7 @@ unitCon = sUN "MkUnit"

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

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

1077 "\n\n" ++

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

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

1079 "of type `Void` in scope."

1080falseTy = sUN "Void"

1081

test/quasiquote001/expected+3−3

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

1−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 9 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 9 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 9 0) (UN Unit) (TType (UVar -1))))))

1+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN Unit) (TType (UVar -1))))))

2--------------

3−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 50))) (TType (UVar 52))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 54))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (P (TCon 9 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 9 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 56)))))

3+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 48))) (TType (UVar 50))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 52))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 54)))))

4--------------

5−(App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (TType (UVar 50))) (TType (UVar 50)))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 44))) (TType (UVar 46))) (TType (UVar 50))) (TType (UVar 50))))

5+(App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48)))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48))))

test/reg002/reg002.idr+2−2

@@ -18,8 +18,8 @@ S_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 = VoidElim (S_Co_not_Inf p)

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

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

22+S_inj Infinity (Co m) p = void (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+1−1

@@ -4,7 +4,7 @@

4> soElim C coh .True .Oh = coh

5

6> soFalseElim : So False -> a

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

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

8> where

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

10> C True s = ()

test/reg049/expected+1−1

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

1reg049.idr:2:9:When elaborating constructor Main.Bogus:

2−{__False0} is not Main.Foo

2+Void is not Main.Foo