Extract Prelude.Basics, Prelude.Uninhabited from Prelude

libs/prelude/Prelude.idr

@@ -2,6 +2,8 @@ module Prelude
 
 import public Builtin
 import public PrimIO
+import public Prelude.Basics
+import public Prelude.Uninhabited
 
 %default total
 
@@ -60,96 +62,6 @@ infixr 0 $
 
 infixl 9 `div`, `mod`
 
------------------------
--- UTILITY FUNCTIONS --
------------------------
-
-||| Manually assign a type to an expression.
-||| @ a the type to assign
-||| @ x the element to get the type
-public export %inline
-the : (0 a : Type) -> (1 x : a) -> a
-the _ x = x
-
-||| Identity function.
-public export %inline
-id : (1 x : a) -> a           -- Hopefully linearity annotation won't
-                              -- break equality proofs involving id
-id x = x
-
-||| Constant function.  Ignores its second argument.
-public export %inline
-const : a -> b -> a
-const x = \value => x
-
-||| Function composition.
-public export %inline
-(.) : (b -> c) -> (a -> b) -> a -> c
-(.) f g = \x => f (g x)
-
-||| Takes in the first two arguments in reverse order.
-||| @ f the function to flip
-public export
-flip : (f : a -> b -> c) -> b -> a -> c
-flip f x y = f y x
-
-||| Function application.
-public export
-apply : (a -> b) -> a -> b
-apply f a = f a
-
-public export
-curry : ((a, b) -> c) -> a -> b -> c
-curry f a b = f (a, b)
-
-public export
-uncurry : (a -> b -> c) -> (a, b) -> c
-uncurry f (a, b) = f a b
-
--- $ is compiled specially to shortcut any tricky unification issues, but if
--- it did have a type this is what it would be, and it might be useful to
--- use directly sometimes (e.g. in higher order functions)
-public export
-($) : forall a, b . ((x : a) -> b x) -> (x : a) -> b x
-($) f a = f a
-
--------------------
--- PROOF HELPERS --
--------------------
-
-||| Equality is a congruence.
-public export
-cong : (0 f : t -> u) -> (1 p : a = b) -> f a = f b
-cong f Refl = Refl
-
-||| A canonical proof that some type is empty.
-public export
-interface Uninhabited t where
-  ||| If I have a t, I've had a contradiction.
-  ||| @ t the uninhabited type
-  uninhabited : t -> Void
-
-||| The eliminator for the `Void` type.
-%extern
-public export
-void : (0 x : Void) -> a
-
-export
-Uninhabited Void where
-  uninhabited = id
-
-||| Use an absurd assumption to discharge a proof obligation.
-||| @ t some empty type
-||| @ a the goal type
-||| @ h the contradictory hypothesis
-public export
-absurd : Uninhabited t => (h : t) -> a
-absurd h = void (uninhabited h)
-
-public export
-Not : Type -> Type
-Not x = x -> Void
-
 --------------
 -- BOOLEANS --
 --------------

libs/prelude/Prelude/Basics.idr

@@ -0,0 +1,71 @@
+module Prelude.Basics
+
+import Builtin
+
+%default total
+
+public export
+Not : Type -> Type
+Not x = x -> Void
+
+-----------------------
+-- UTILITY FUNCTIONS --
+-----------------------
+
+||| Manually assign a type to an expression.
+||| @ a the type to assign
+||| @ x the element to get the type
+public export %inline
+the : (0 a : Type) -> (1 x : a) -> a
+the _ x = x
+
+||| Identity function.
+public export %inline
+id : (1 x : a) -> a           -- Hopefully linearity annotation won't
+                              -- break equality proofs involving id
+id x = x
+
+||| Constant function.  Ignores its second argument.
+public export %inline
+const : a -> b -> a
+const x = \value => x
+
+||| Function composition.
+public export %inline
+(.) : (b -> c) -> (a -> b) -> a -> c
+(.) f g = \x => f (g x)
+
+||| Takes in the first two arguments in reverse order.
+||| @ f the function to flip
+public export
+flip : (f : a -> b -> c) -> b -> a -> c
+flip f x y = f y x
+
+||| Function application.
+public export
+apply : (a -> b) -> a -> b
+apply f a = f a
+
+public export
+curry : ((a, b) -> c) -> a -> b -> c
+curry f a b = f (a, b)
+
+public export
+uncurry : (a -> b -> c) -> (a, b) -> c
+uncurry f (a, b) = f a b
+
+-- $ is compiled specially to shortcut any tricky unification issues, but if
+-- it did have a type this is what it would be, and it might be useful to
+-- use directly sometimes (e.g. in higher order functions)
+public export
+($) : forall a, b . ((x : a) -> b x) -> (x : a) -> b x
+($) f a = f a
+
+-------------------
+-- PROOF HELPERS --
+-------------------
+
+||| Equality is a congruence.
+public export
+cong : (0 f : t -> u) -> (1 p : a = b) -> f a = f b
+cong f Refl = Refl

libs/prelude/Prelude/Uninhabited.idr

@@ -0,0 +1,30 @@
+module Prelude.Uninhabited
+
+import Builtin
+import Prelude.Basics
+
+%default total
+
+||| A canonical proof that some type is empty.
+public export
+interface Uninhabited t where
+  ||| If I have a t, I've had a contradiction.
+  ||| @ t the uninhabited type
+  uninhabited : t -> Void
+
+||| The eliminator for the `Void` type.
+%extern
+public export
+void : (0 x : Void) -> a
+
+export
+Uninhabited Void where
+  uninhabited = id
+
+||| Use an absurd assumption to discharge a proof obligation.
+||| @ t some empty type
+||| @ a the goal type
+||| @ h the contradictory hypothesis
+public export
+absurd : Uninhabited t => (h : t) -> a
+absurd h = void (uninhabited h)

libs/prelude/prelude.ipkg

@@ -4,5 +4,6 @@ opts = "--no-prelude"
 
 modules = Builtin,
           PrimIO,
-          Prelude
-
+          Prelude,
+          Prelude.Basics,
+          Prelude.Uninhabited

tests/ideMode/ideMode001/expected

@@ -8,7 +8,7 @@
 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:271}_[] ?{_:270}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
-0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
+0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

tests/ideMode/ideMode003/expected

@@ -8,7 +8,7 @@
 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:271}_[] ?{_:270}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
-0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
+0001cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)