git.iko.soy/Idris-dev
on master help sign in
Renamed VoidElim to void in order to ensure further consistency
commitd6981dc09bbe20c97ce7328d12f5f8bd67f3729e authorAhmad Salim Al-Sibahi <asal@itu.dk> dateSat 11 Oct 2014, 20:52 (12 years ago) parentedb9980
11 files changed+23−23
compare with master
unifiedsplit
libs/base/Control/Isomorphism.idr+7−7 libs/base/Data/Heap.idr+1−1 libs/base/Decidable/Order.idr+1−1 libs/prelude/Builtins.idr+3−3 libs/prelude/Prelude/Fin.idr+1−1 libs/prelude/Prelude/Uninhabited.idr+1−1 src/Idris/AbsSyntaxTree.hs+2−2 test/quasiquote001/expected+3−3 test/reg002/reg002.idr+2−2 test/reg012/reg012.lidr+1−1 test/reg049/expected+1−1
libs/base/Control/Isomorphism.idr+7−7
@@ -73,14 +73,14 @@ eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
7373eitherBotLeft : Iso (Either Void a) a
7474eitherBotLeft = MkIso to from ok1 ok2
7575 where to : Either Void a -> a
76− to (Left x) = VoidElim x
76+ to (Left x) = void x
7777 to (Right x) = x
7878 from : a -> Either Void a
7979 from = Right
8080 ok1 : (x : a) -> to (from x) = x
8181 ok1 x = Refl
8282 ok2 : (x : Either Void a) -> from (to x) = x
83− ok2 (Left x) = VoidElim x
83+ ok2 (Left x) = void x
8484 ok2 (Right x) = Refl
8585
8686||| Disjunction with false is a no-op
@@ -146,7 +146,7 @@ pairUnitLeft = isoTrans pairComm pairUnitRight
146146
147147||| Conjunction preserves falsehood
148148pairBotLeft : 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))
150150
151151||| Conjunction preserves falsehood
152152pairBotRight : Iso (a, Void) Void
@@ -281,10 +281,10 @@ maybeIsoS = MkIso forth back fb bf
281281 fb (FS x) = Refl
282282
283283finZeroBot : Iso (Fin 0) Void
284−finZeroBot = MkIso (\x => VoidElim (uninhabited x))
285− (\x => VoidElim x)
286− (\x => VoidElim x)
287− (\x => VoidElim (uninhabited x))
284+finZeroBot = MkIso (\x => void (uninhabited x))
285+ (\x => void x)
286+ (\x => void x)
287+ (\x => void (uninhabited x))
288288
289289eitherFinPlus : Iso (Either (Fin m) (Fin n)) (Fin (m + n))
290290eitherFinPlus {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 =
169169
170170isEmptySizeZeroNodeAbsurd = proof {
171171 intros;
172− refine VoidElim;
172+ refine void;
173173 refine absurdBoolDischarge;
174174 exact p;
175175}
libs/base/Decidable/Order.idr+1−1
@@ -92,7 +92,7 @@ total zeroAlwaysSmaller : {n : Nat} -> LTE Z n
9292zeroAlwaysSmaller = LTEZero
9393
9494total 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)
9696ltesuccinjective {n} {m} disprf LTEZero impossible
9797
9898
libs/prelude/Builtins.idr+3−3
@@ -31,12 +31,12 @@ data Sigma : (a : Type) -> (P : a -> Type) -> Type where
3131
3232||| The empty type, also known as the trivially false proposition.
3333|||
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.
3535%elim data Void : Type where
3636
3737||| The eliminator for the `Void` type.
38−VoidElim : Void -> a
39−VoidElim {a} v = elim_for Void (\_ => a) v
38+void : Void -> a
39+void {a} v = elim_for Void (\_ => a) v
4040
4141||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
4242data Symbol_ : String -> Type where
libs/prelude/Prelude/Fin.idr+1−1
@@ -32,7 +32,7 @@ FinZAbsurd : Fin Z -> Void
3232FinZAbsurd FZ impossible
3333
3434FinZElim : Fin Z -> a
35−FinZElim x = VoidElim (FinZAbsurd x)
35+FinZElim x = void (FinZAbsurd x)
3636
3737||| Convert a Fin to a Nat
3838finToNat : Fin n -> Nat
libs/prelude/Prelude/Uninhabited.idr+1−1
@@ -16,4 +16,4 @@ instance Uninhabited Void where
1616||| @ a the goal type
1717||| @ h the contradictory hypothesis
1818absurd : 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
238238primDefs = [sUN "unsafePerformPrimIO",
239239 sUN "mkLazyForeignPrim",
240240 sUN "mkForeignPrim",
241− sUN "VoidElim"]
241+ sUN "void"]
242242
243243-- information that needs writing for the current module's .ibc file
244244data IBCWrite = IBCFix FixDecl
@@ -1075,7 +1075,7 @@ unitCon = sUN "MkUnit"
10751075falseDoc = fmap (const Nothing) . parseDocstring . T.pack $
10761076 "The empty type, also known as the trivially false proposition." ++
10771077 "\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 " ++
10791079 "of type `Void` in scope."
10801080falseTy = sUN "Void"
10811081
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))))))
22--------------
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)))))
44--------------
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
1818
1919S_inj : (n : CoNat) -> (m : CoNat) -> Main.S n = Main.S m -> n = m
2020S_inj (Co n) (Co _) Refl = Refl
21−S_inj (Co n) Infinity p = VoidElim (S_Co_not_Inf p)
22−S_inj Infinity (Co m) p = VoidElim (S_Co_not_Inf (sym p))
21+S_inj (Co n) Infinity p = void (S_Co_not_Inf p)
22+S_inj Infinity (Co m) p = void (S_Co_not_Inf (sym p))
2323S_inj Infinity Infinity Refl = Refl
2424
2525swap : {n : Nat} -> Vect n a -> Vect n a
test/reg012/reg012.lidr+1−1
@@ -4,7 +4,7 @@
44> soElim C coh .True .Oh = coh
55
66> soFalseElim : So False -> a
7−> soFalseElim x = VoidElim (soElim C () False x)
7+> soFalseElim x = void (soElim C () False x)
88> where
99> C : (b : Bool) -> So b -> Type
1010> C True s = ()
test/reg049/expected+1−1
@@ -1,2 +1,2 @@
11reg049.idr:2:9:When elaborating constructor Main.Bogus:
2−{__False0} is not Main.Foo
2+Void is not Main.Foo