Reorganise prelude into multiple files

This is partly to tidy things up, but also a good test for 'import as'. Requires some internal changes since there are parts of reflection, unelaboration and a compiler hack that rely on where things are in the Prelude.
2024-11-24 06:52:19 +03:00 · 2020-07-12 15:54:10 +01:00 · 2020-07-12 15:54:10 +01:00 · 6a53e0177c
commit 6a53e0177c
parent 9d6f365ad7
23 changed files with 1971 additions and 1880 deletions
--- a/libs/prelude/Prelude.idr
+++ b/libs/prelude/Prelude.idr
--- a/libs/prelude/Prelude/Basics.idr
+++ b/libs/prelude/Prelude/Basics.idr
@ -69,3 +69,35 @@ public export
 public export
 cong : (0 f : t -> u) -> (1 p : a = b) -> f a = f b
 cong f Refl = Refl
+
+--------------
+-- BOOLEANS --
+--------------
+
+||| Boolean Data Type.
+public export
+data Bool = True | False
+
+||| Boolean NOT.
+public export
+not : (1 b : Bool) -> Bool
+not True = False
+not False = True
+
+||| Boolean AND only evaluates the second argument if the first is `True`.
+public export
+(&&) : (1 b : Bool) -> Lazy Bool -> Bool
+(&&) True x = x
+(&&) False x = False
+
+||| Boolean OR only evaluates the second argument if the first is `False`.
+public export
+(||) : (1 b : Bool) -> Lazy Bool -> Bool
+(||) True x = True
+(||) False x = x
+
+%inline
+public export
+intToBool : Int -> Bool
+intToBool 0 = False
+intToBool x = True
--- a/libs/prelude/Prelude/EqOrd.idr
+++ b/libs/prelude/Prelude/EqOrd.idr
@ -0,0 +1,203 @@
+module Prelude.EqOrd
+
+import Builtin
+import Prelude.Basics
+import Prelude.Ops
+
+%default total
+
+------------------------
+-- EQUALITY, ORDERING --
+------------------------
+
+||| The Eq interface defines inequality and equality.
+public export
+interface Eq ty where
+  (==) : ty -> ty -> Bool
+  (/=) : ty -> ty -> Bool
+
+  x == y = not (x /= y)
+  x /= y = not (x == y)
+
+public export
+Eq () where
+  _ == _ = True
+
+public export
+Eq Bool where
+  True == True = True
+  False == False = True
+  _ == _ = False
+
+public export
+Eq Int where
+  x == y = intToBool (prim__eq_Int x y)
+
+public export
+Eq Integer where
+  x == y = intToBool (prim__eq_Integer x y)
+
+public export
+Eq Bits8 where
+  x == y = intToBool (prim__eq_Bits8 x y)
+
+public export
+Eq Bits16 where
+  x == y = intToBool (prim__eq_Bits16 x y)
+
+public export
+Eq Bits32 where
+  x == y = intToBool (prim__eq_Bits32 x y)
+
+public export
+Eq Bits64 where
+  x == y = intToBool (prim__eq_Bits64 x y)
+
+public export
+Eq Double where
+  x == y = intToBool (prim__eq_Double x y)
+
+public export
+Eq Char where
+  x == y = intToBool (prim__eq_Char x y)
+
+public export
+Eq String where
+  x == y = intToBool (prim__eq_String x y)
+
+public export
+Eq a => Eq b => Eq (a, b) where
+  (x1, y1) == (x2, y2) = x1 == x2 && y1 == y2
+
+public export
+data Ordering = LT | EQ | GT
+
+public export
+Eq Ordering where
+  LT == LT = True
+  EQ == EQ = True
+  GT == GT = True
+  _  == _  = False
+
+||| The Ord interface defines comparison operations on ordered data types.
+public export
+interface Eq ty => Ord ty where
+  compare : ty -> ty -> Ordering
+
+  (<) : ty -> ty -> Bool
+  (<) x y = compare x y == LT
+
+  (>) : ty -> ty -> Bool
+  (>) x y = compare x y == GT
+
+  (<=) : ty -> ty -> Bool
+  (<=) x y = compare x y /= GT
+
+  (>=) : ty -> ty -> Bool
+  (>=) x y = compare x y /= LT
+
+  max : ty -> ty -> ty
+  max x y = if x > y then x else y
+
+  min : ty -> ty -> ty
+  min x y = if (x < y) then x else y
+
+public export
+Ord () where
+  compare _ _ = EQ
+
+public export
+Ord Bool where
+  compare False False = EQ
+  compare False True = LT
+  compare True False = GT
+  compare True True = EQ
+
+public export
+Ord Int where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Int x y)
+  (<=) x y = intToBool (prim__lte_Int x y)
+  (>) x y = intToBool (prim__gt_Int x y)
+  (>=) x y = intToBool (prim__gte_Int x y)
+
+public export
+Ord Integer where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Integer x y)
+  (<=) x y = intToBool (prim__lte_Integer x y)
+  (>) x y = intToBool (prim__gt_Integer x y)
+  (>=) x y = intToBool (prim__gte_Integer x y)
+
+public export
+Ord Bits8 where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Bits8 x y)
+  (<=) x y = intToBool (prim__lte_Bits8 x y)
+  (>) x y = intToBool (prim__gt_Bits8 x y)
+  (>=) x y = intToBool (prim__gte_Bits8 x y)
+
+public export
+Ord Bits16 where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Bits16 x y)
+  (<=) x y = intToBool (prim__lte_Bits16 x y)
+  (>) x y = intToBool (prim__gt_Bits16 x y)
+  (>=) x y = intToBool (prim__gte_Bits16 x y)
+
+public export
+Ord Bits32 where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Bits32 x y)
+  (<=) x y = intToBool (prim__lte_Bits32 x y)
+  (>) x y = intToBool (prim__gt_Bits32 x y)
+  (>=) x y = intToBool (prim__gte_Bits32 x y)
+
+public export
+Ord Bits64 where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Bits64 x y)
+  (<=) x y = intToBool (prim__lte_Bits64 x y)
+  (>) x y = intToBool (prim__gt_Bits64 x y)
+  (>=) x y = intToBool (prim__gte_Bits64 x y)
+
+public export
+Ord Double where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Double x y)
+  (<=) x y = intToBool (prim__lte_Double x y)
+  (>) x y = intToBool (prim__gt_Double x y)
+  (>=) x y = intToBool (prim__gte_Double x y)
+
+public export
+Ord String where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_String x y)
+  (<=) x y = intToBool (prim__lte_String x y)
+  (>) x y = intToBool (prim__gt_String x y)
+  (>=) x y = intToBool (prim__gte_String x y)
+
+public export
+Ord Char where
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  (<) x y = intToBool (prim__lt_Char x y)
+  (<=) x y = intToBool (prim__lte_Char x y)
+  (>) x y = intToBool (prim__gt_Char x y)
+  (>=) x y = intToBool (prim__gte_Char x y)
+
+public export
+Ord a => Ord b => Ord (a, b) where
+  compare (x1, y1) (x2, y2)
+      = if x1 /= x2 then compare x1 x2
+                    else compare y1 y2
+
+
--- a/libs/prelude/Prelude/IO.idr
+++ b/libs/prelude/Prelude/IO.idr
@ -0,0 +1,126 @@
+module Prelude.IO
+
+import Builtin
+import PrimIO
+import Prelude.Basics
+import Prelude.Interfaces
+import Prelude.Show
+
+%default total
+
+--------
+-- IO --
+--------
+
+public export
+Functor IO where
+  map f io = io_bind io (\b => io_pure (f b))
+
+%inline
+public export
+Applicative IO where
+  pure x = io_pure x
+  f <*> a
+      = io_bind f (\f' =>
+          io_bind a (\a' =>
+            io_pure (f' a')))
+
+%inline
+public export
+Monad IO where
+  b >>= k = io_bind b k
+
+public export
+interface Monad io => HasIO io where
+  liftIO : (1 _ : IO a) -> io a
+
+public export %inline
+HasIO IO where
+  liftIO x = x
+
+export %inline
+primIO : HasIO io => (1 fn : (1 x : %World) -> IORes a) -> io a
+primIO op = liftIO (fromPrim op)
+
+%extern
+prim__onCollectAny : AnyPtr -> (AnyPtr -> PrimIO ()) -> PrimIO GCAnyPtr
+%extern
+prim__onCollect : Ptr t -> (Ptr t -> PrimIO ()) -> PrimIO (GCPtr t)
+
+export
+onCollectAny : AnyPtr -> (AnyPtr -> IO ()) -> IO GCAnyPtr
+onCollectAny ptr c = fromPrim (prim__onCollectAny ptr (\x => toPrim (c x)))
+
+export
+onCollect : Ptr t -> (Ptr t -> IO ()) -> IO (GCPtr t)
+onCollect ptr c = fromPrim (prim__onCollect ptr (\x => toPrim (c x)))
+
+%foreign "C:idris2_getString, libidris2_support"
+         "javascript:lambda:x=>x"
+export
+prim__getString : Ptr String -> String
+
+%foreign "C:putchar,libc 6"
+prim__putChar : Char -> (1 x : %World) -> IORes ()
+%foreign "C:getchar,libc 6"
+%extern prim__getChar : (1 x : %World) -> IORes Char
+
+%foreign "C:idris2_getStr,libidris2_support"
+         "node:support:getStr,support_system_file"
+prim__getStr : PrimIO String
+
+%foreign "C:idris2_putStr,libidris2_support"
+         "node:lambda:x=>process.stdout.write(x)"
+prim__putStr : String -> PrimIO ()
+
+||| Output a string to stdout without a trailing newline.
+export
+putStr : HasIO io => String -> io ()
+putStr str = primIO (prim__putStr str)
+
+||| Output a string to stdout with a trailing newline.
+export
+putStrLn : HasIO io => String -> io ()
+putStrLn str = putStr (prim__strAppend str "\n")
+
+||| Read one line of input from stdin, without the trailing newline.
+export
+getLine : HasIO io => io String
+getLine = primIO prim__getStr
+
+||| Write a single character to stdout.
+export
+putChar : HasIO io => Char -> io ()
+putChar c = primIO (prim__putChar c)
+
+||| Write a single character to stdout, with a trailing newline.
+export
+putCharLn : HasIO io => Char -> io ()
+putCharLn c = putStrLn (prim__cast_CharString c)
+
+||| Read a single character from stdin.
+export
+getChar : HasIO io => io Char
+getChar = primIO prim__getChar
+
+export
+prim_fork : (1 prog : PrimIO ()) -> PrimIO ThreadID
+prim_fork act w = prim__schemeCall ThreadID "blodwen-thread" [act] w
+
+export
+fork : (1 prog : IO ()) -> IO ThreadID
+fork act = schemeCall ThreadID "blodwen-thread" [toPrim act]
+
+%foreign "C:idris2_readString, libidris2_support"
+export
+prim__getErrno : Int
+
+||| Output something showable to stdout, without a trailing newline.
+export
+print : (HasIO io, Show a) => a -> io ()
+print x = putStr $ show x
+
+||| Output something showable to stdout, with a trailing newline.
+export
+printLn : (HasIO io, Show a) => a -> io ()
+printLn x = putStrLn $ show x
--- a/libs/prelude/Prelude/Interfaces.idr
+++ b/libs/prelude/Prelude/Interfaces.idr
@ -0,0 +1,268 @@
+module Prelude.Interfaces
+
+import Builtin
+import Prelude.Basics
+import Prelude.Num
+import Prelude.Ops
+
+%default total
+
+-------------
+-- ALGEBRA --
+-------------
+
+||| Sets equipped with a single binary operation that is associative.  Must
+||| satisfy the following laws:
+|||
+||| + Associativity of `<+>`:
+|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
+public export
+interface Semigroup ty where
+  (<+>) : ty -> ty -> ty
+
+||| Sets equipped with a single binary operation that is associative, along with
+||| a neutral element for that binary operation.  Must satisfy the following
+||| laws:
+|||
+||| + Associativity of `<+>`:
+|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
+||| + Neutral for `<+>`:
+|||     forall a, a <+> neutral == a
+|||     forall a, neutral <+> a == a
+public export
+interface Semigroup ty => Monoid ty where
+  neutral : ty
+
+export
+shiftL : Int -> Int -> Int
+shiftL = prim__shl_Int
+
+export
+shiftR : Int -> Int -> Int
+shiftR = prim__shr_Int
+
+----------------------------------------------
+-- FUNCTOR, APPLICATIVE, ALTERNATIVE, MONAD --
+----------------------------------------------
+
+||| Functors allow a uniform action over a parameterised type.
+||| @ f a parameterised type
+public export
+interface Functor f where
+  ||| Apply a function across everything of type 'a' in a parameterised type
+  ||| @ f the parameterised type
+  ||| @ func the function to apply
+  map : (func : a -> b) -> f a -> f b
+
+||| An infix alias for `map`, applying a function across everything of type 'a'
+||| in a parameterised type.
+||| @ f the parameterised type
+||| @ func the function to apply
+public export
+(<$>) : Functor f => (func : a -> b) -> f a -> f b
+(<$>) func x = map func x
+
+||| Run something for effects, throwing away the return value.
+public export
+ignore : Functor f => f a -> f ()
+ignore = map (const ())
+
+public export
+interface Functor f => Applicative f where
+  pure : a -> f a
+  (<*>) : f (a -> b) -> f a -> f b
+
+public export
+(<*) : Applicative f => f a -> f b -> f a
+a <* b = map const a <*> b
+
+public export
+(*>) : Applicative f => f a -> f b -> f b
+a *> b = map (const id) a <*> b
+
+%allow_overloads pure
+%allow_overloads (<*)
+%allow_overloads (*>)
+
+public export
+interface Applicative f => Alternative f where
+  empty : f a
+  (<|>) : f a -> f a -> f a
+
+public export
+interface Applicative m => Monad m where
+  ||| Also called `bind`.
+  (>>=) : m a -> (a -> m b) -> m b
+
+  ||| Also called `flatten` or mu.
+  join : m (m a) -> m a
+
+  -- default implementations
+  (>>=) x f = join (f <$> x)
+  join x = x >>= id
+
+%allow_overloads (>>=)
+
+||| `guard a` is `pure ()` if `a` is `True` and `empty` if `a` is `False`.
+public export
+guard : Alternative f => Bool -> f ()
+guard x = if x then pure () else empty
+
+||| Conditionally execute an applicative expression.
+public export
+when : Applicative f => Bool -> Lazy (f ()) -> f ()
+when True f = f
+when False f = pure ()
+
+---------------------------
+-- FOLDABLE, TRAVERSABLE --
+---------------------------
+
+||| The `Foldable` interface describes how you can iterate over the elements in
+||| a parameterised type and combine the elements together, using a provided
+||| function, into a single result.
+||| @ t The type of the 'Foldable' parameterised type.
+public export
+interface Foldable (t : Type -> Type) where
+  ||| Successively combine the elements in a parameterised type using the
+  ||| provided function, starting with the element that is in the final position
+  ||| i.e. the right-most position.
+  ||| @ func  The function used to 'fold' an element into the accumulated result
+  ||| @ init  The starting value the results are being combined into
+  ||| @ input The parameterised type
+  foldr : (func : elem -> acc -> acc) -> (init : acc) -> (input : t elem) -> acc
+
+  ||| The same as `foldr` but begins the folding from the element at the initial
+  ||| position in the data structure i.e. the left-most position.
+  ||| @ func  The function used to 'fold' an element into the accumulated result
+  ||| @ init  The starting value the results are being combined into
+  ||| @ input The parameterised type
+  foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc
+  foldl f z t = foldr (flip (.) . flip f) id t z
+
+||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.
+||| Consequently, the final value is wrapped in the same `Monad`.
+public export
+foldlM : (Foldable t, Monad m) => (funcM: a -> b -> m a) -> (init: a) -> (input: t b) -> m a
+foldlM fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)
+
+||| Combine each element of a structure into a monoid.
+public export
+concat : (Foldable t, Monoid a) => t a -> a
+concat = foldr (<+>) neutral
+
+||| Combine into a monoid the collective results of applying a function to each
+||| element of a structure.
+public export
+concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m
+concatMap f = foldr ((<+>) . f) neutral
+
+||| The conjunction of all elements of a structure containing lazy boolean
+||| values.  `and` short-circuits from left to right, evaluating until either an
+||| element is `False` or no elements remain.
+public export
+and : Foldable t => t (Lazy Bool) -> Bool
+and = foldl (&&) True
+
+||| The disjunction of all elements of a structure containing lazy boolean
+||| values.  `or` short-circuits from left to right, evaluating either until an
+||| element is `True` or no elements remain.
+public export
+or : Foldable t => t (Lazy Bool) -> Bool
+or = foldl (||) False
+
+||| The disjunction of the collective results of applying a predicate to all
+||| elements of a structure.  `any` short-circuits from left to right.
+public export
+any : Foldable t => (a -> Bool) -> t a -> Bool
+any p = foldl (\x,y => x || p y) False
+
+||| The disjunction of the collective results of applying a predicate to all
+||| elements of a structure.  `all` short-circuits from left to right.
+public export
+all : Foldable t => (a -> Bool) -> t a -> Bool
+all p = foldl (\x,y => x && p y)  True
+
+||| Add together all the elements of a structure.
+public export
+sum : (Foldable t, Num a) => t a -> a
+sum = foldr (+) 0
+
+||| Add together all the elements of a structure.
+||| Same as `sum` but tail recursive.
+export
+sum' : (Foldable t, Num a) => t a -> a
+sum' = foldl (+) 0
+
+||| Multiply together all elements of a structure.
+public export
+product : (Foldable t, Num a) => t a -> a
+product = foldr (*) 1
+
+||| Multiply together all elements of a structure.
+||| Same as `product` but tail recursive.
+export
+product' : (Foldable t, Num a) => t a -> a
+product' = foldl (*) 1
+
+||| Map each element of a structure to a computation, evaluate those
+||| computations and discard the results.
+public export
+traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
+traverse_ f = foldr ((*>) . f) (pure ())
+
+||| Evaluate each computation in a structure and discard the results.
+public export
+sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
+sequence_ = foldr (*>) (pure ())
+
+||| Like `traverse_` but with the arguments flipped.
+public export
+for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
+for_ = flip traverse_
+
+||| Fold using Alternative.
+|||
+||| If you have a left-biased alternative operator `<|>`, then `choice` performs
+||| left-biased choice from a list of alternatives, which means that it
+||| evaluates to the left-most non-`empty` alternative.
+|||
+||| If the list is empty, or all values in it are `empty`, then it evaluates to
+||| `empty`.
+|||
+||| Example:
+|||
+||| ```
+||| -- given a parser expression like:
+||| expr = literal <|> keyword <|> funcall
+|||
+||| -- choice lets you write this as:
+||| expr = choice [literal, keyword, funcall]
+||| ```
+|||
+||| Note: In Haskell, `choice` is called `asum`.
+public export
+choice : (Foldable t, Alternative f) => t (f a) -> f a
+choice = foldr (<|>) empty
+
+||| A fused version of `choice` and `map`.
+public export
+choiceMap : (Foldable t, Alternative f) => (a -> f b) -> t a -> f b
+choiceMap f = foldr (\e, a => f e <|> a) empty
+
+public export
+interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where
+  ||| Map each element of a structure to a computation, evaluate those
+  ||| computations and combine the results.
+  traverse : Applicative f => (a -> f b) -> t a -> f (t b)
+
+||| Evaluate each computation in a structure and collect the results.
+public export
+sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)
+sequence = traverse id
+
+||| Like `traverse` but with the arguments flipped.
+public export
+for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
+for = flip traverse
+
--- a/libs/prelude/Prelude/Num.idr
+++ b/libs/prelude/Prelude/Num.idr
@ -0,0 +1,175 @@
+module Prelude.Num
+
+import Builtin
+import Prelude.Basics
+import Prelude.EqOrd
+import Prelude.Ops
+
+%default total
+
+------------------------
+-- NUMERIC INTERFACES --
+------------------------
+
+%integerLit fromInteger
+
+||| The Num interface defines basic numerical arithmetic.
+public export
+interface Num ty where
+  (+) : ty -> ty -> ty
+  (*) : ty -> ty -> ty
+  ||| Conversion from Integer.
+  fromInteger : Integer -> ty
+
+%allow_overloads fromInteger
+
+||| The `Neg` interface defines operations on numbers which can be negative.
+public export
+interface Num ty => Neg ty where
+  ||| The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.
+  negate : ty -> ty
+  (-) : ty -> ty -> ty
+
+||| Numbers for which the absolute value is defined should implement `Abs`.
+public export
+interface Num ty => Abs ty where
+  ||| Absolute value.
+  abs : ty -> ty
+
+public export
+interface Num ty => Fractional ty where
+  partial
+  (/) : ty -> ty -> ty
+  partial
+  recip : ty -> ty
+
+  recip x = 1 / x
+
+public export
+interface Num ty => Integral ty where
+  partial
+  div : ty -> ty -> ty
+  partial
+  mod : ty -> ty -> ty
+
+----- Instances for primitives
+
+-- Integer
+
+%inline
+public export
+Num Integer where
+  (+) = prim__add_Integer
+  (*) = prim__mul_Integer
+  fromInteger = id
+
+public export
+Neg Integer where
+  negate x = prim__sub_Integer 0 x
+  (-) = prim__sub_Integer
+
+public export
+Abs Integer where
+  abs x = if x < 0 then -x else x
+
+public export
+Integral Integer where
+  div x y
+      = case y == 0 of
+             False => prim__div_Integer x y
+  mod x y
+      = case y == 0 of
+             False => prim__mod_Integer x y
+
+-- This allows us to pick integer as a default at the end of elaboration if
+-- all other possibilities fail. I don't plan to provide a nicer syntax for
+-- this...
+%defaulthint
+%inline
+public export
+defaultInteger : Num Integer
+defaultInteger = %search
+
+-- Int
+
+%inline
+public export
+Num Int where
+  (+) = prim__add_Int
+  (*) = prim__mul_Int
+  fromInteger = prim__cast_IntegerInt
+
+public export
+Neg Int where
+  negate x = prim__sub_Int 0 x
+  (-) = prim__sub_Int
+
+public export
+Abs Int where
+  abs x = if x < 0 then -x else x
+
+public export
+Integral Int where
+  div x y
+      = case y == 0 of
+             False => prim__div_Int x y
+  mod x y
+      = case y == 0 of
+             False => prim__mod_Int x y
+
+-- Bits8
+
+%inline
+public export
+Num Bits8 where
+  (+) = prim__add_Bits8
+  (*) = prim__mul_Bits8
+  fromInteger = prim__cast_IntegerBits8
+
+-- Bits16
+
+%inline
+public export
+Num Bits16 where
+  (+) = prim__add_Bits16
+  (*) = prim__mul_Bits16
+  fromInteger = prim__cast_IntegerBits16
+
+-- Bits32
+
+%inline
+public export
+Num Bits32 where
+  (+) = prim__add_Bits32
+  (*) = prim__mul_Bits32
+  fromInteger = prim__cast_IntegerBits32
+
+-- Bits64
+
+%inline
+public export
+Num Bits64 where
+  (+) = prim__add_Bits64
+  (*) = prim__mul_Bits64
+  fromInteger = prim__cast_IntegerBits64
+
+-- Double
+
+public export
+Num Double where
+  (+) = prim__add_Double
+  (*) = prim__mul_Double
+  fromInteger = prim__cast_IntegerDouble
+
+public export
+Neg Double where
+  negate x = prim__negate_Double x
+  (-) = prim__sub_Double
+
+public export
+Abs Double where
+  abs x = if x < 0 then -x else x
+
+public export
+Fractional Double where
+  (/) = prim__div_Double
--- a/libs/prelude/Prelude/Ops.idr
+++ b/libs/prelude/Prelude/Ops.idr
@ -0,0 +1,28 @@
+module Prelude.Ops
+
+-- Numerical operators
+infix 6 ==, /=, <, <=, >, >=
+infixl 7 <<, >> -- unused
+infixl 8 +, -
+infixl 9 *, /
+
+-- Boolean operators
+infixr 4 &&
+infixr 5 ||
+
+-- List and String operators
+infixr 7 ::, ++
+
+-- Functor/Applicative/Monad/Algebra operators
+infixl 1 >>=
+infixr 2 <|>
+infixl 3 <*>, *>, <*
+infixr 4 <$>
+infixl 6 <+>
+
+-- Utility operators
+infixr 9 .
+infixr 0 $
+
+infixl 9 `div`, `mod`
+
--- a/libs/prelude/Prelude/Show.idr
+++ b/libs/prelude/Prelude/Show.idr
@ -0,0 +1,214 @@
+module Prelude.Show
+
+import Builtin
+import Prelude.Basics
+import Prelude.EqOrd
+import Prelude.Num
+import Prelude.Types
+
+%default total
+
+----------
+-- SHOW --
+----------
+
+||| The precedence of an Idris operator or syntactic context.
+public export
+data Prec = Open | Equal | Dollar | Backtick | User Nat | PrefixMinus | App
+
+||| Gives the constructor index of the Prec as a helper for writing
+||| implementations.
+public export
+precCon : Prec -> Integer
+precCon Open        = 0
+precCon Equal       = 1
+precCon Dollar      = 2
+precCon Backtick    = 3
+precCon (User n)    = 4
+precCon PrefixMinus = 5
+precCon App         = 6
+
+export
+Eq Prec where
+  (==) (User m) (User n) = m == n
+  (==) x        y        = precCon x == precCon y
+
+export
+Ord Prec where
+  compare (User m) (User n) = compare m n
+  compare x        y        = compare (precCon x) (precCon y)
+
+||| Things that have a canonical `String` representation.
+public export
+interface Show ty where
+  ||| Convert a value to its `String` representation.
+  ||| @ x the value to convert
+  show : (x : ty) -> String
+  show x = showPrec Open x
+
+  ||| Convert a value to its `String` representation in a certain precedence
+  ||| context.
+  |||
+  ||| A value should produce parentheses around itself if and only if the given
+  ||| precedence context is greater than or equal to the precedence of the
+  ||| outermost operation represented in the produced `String`.  *This is
+  ||| different from Haskell*, which requires it to be strictly greater.  `Open`
+  ||| should thus always produce *no* outermost parens, `App` should always
+  ||| produce outermost parens except on atomic values and those that provide
+  ||| their own bracketing, like `Pair` and `List`.
+  ||| @ d the precedence context.
+  ||| @ x the value to convert
+  showPrec : (d : Prec) -> (x : ty) -> String
+  showPrec _ x = show x
+
+||| Surround a `String` with parentheses depending on a condition.
+||| @ b whether to add parentheses
+showParens : (1 b : Bool) -> String -> String
+showParens False s = s
+showParens True  s = "(" ++ s ++ ")"
+
+||| A helper for the common case of showing a non-infix constructor with at
+||| least one argument, for use with `showArg`.
+|||
+||| Apply `showCon` to the precedence context, the constructor name, and the
+||| args shown with `showArg` and concatenated.  Example:
+||| ```
+||| data Ann a = MkAnn String a
+|||
+||| Show a => Show (Ann a) where
+|||   showPrec d (MkAnn s x) = showCon d "MkAnn" $ showArg s ++ showArg x
+||| ```
+export
+showCon : (d : Prec) -> (conName : String) -> (shownArgs : String) -> String
+showCon d conName shownArgs = showParens (d >= App) (conName ++ shownArgs)
+
+||| A helper for the common case of showing a non-infix constructor with at
+||| least one argument, for use with `showCon`.
+|||
+||| This adds a space to the front so the results can be directly concatenated.
+||| See `showCon` for details and an example.
+export
+showArg : Show a => (x : a) -> String
+showArg x = " " ++ showPrec App x
+
+firstCharIs : (Char -> Bool) -> String -> Bool
+firstCharIs p "" = False
+firstCharIs p str = p (assert_total (prim__strHead str))
+
+primNumShow : (a -> String) -> Prec -> a -> String
+primNumShow f d x = let str = f x in showParens (d >= PrefixMinus && firstCharIs (== '-') str) str
+
+export
+Show Int where
+  showPrec = primNumShow prim__cast_IntString
+
+export
+Show Integer where
+  showPrec = primNumShow prim__cast_IntegerString
+
+export
+Show Bits8 where
+  showPrec = primNumShow prim__cast_Bits8String
+
+export
+Show Bits16 where
+  showPrec = primNumShow prim__cast_Bits16String
+
+export
+Show Bits32 where
+  showPrec = primNumShow prim__cast_Bits32String
+
+export
+Show Bits64 where
+  showPrec = primNumShow prim__cast_Bits64String
+
+export
+Show Double where
+  showPrec = primNumShow prim__cast_DoubleString
+
+protectEsc : (Char -> Bool) -> String -> String -> String
+protectEsc p f s = f ++ (if firstCharIs p s then "\\&" else "") ++ s
+
+showLitChar : Char -> String -> String
+showLitChar '\a'   = ("\\a" ++)
+showLitChar '\b'   = ("\\b" ++)
+showLitChar '\f'   = ("\\f" ++)
+showLitChar '\n'   = ("\\n" ++)
+showLitChar '\r'   = ("\\r" ++)
+showLitChar '\t'   = ("\\t" ++)
+showLitChar '\v'   = ("\\v" ++)
+showLitChar '\SO'  = protectEsc (== 'H') "\\SO"
+showLitChar '\DEL' = ("\\DEL" ++)
+showLitChar '\\'   = ("\\\\" ++)
+showLitChar c
+    = case getAt (fromInteger (prim__cast_CharInteger c)) asciiTab of
+           Just k => strCons '\\' . (k ++)
+           Nothing => if (c > '\DEL')
+                         then strCons '\\' . protectEsc isDigit (show (prim__cast_CharInt c))
+                         else strCons c
+  where
+    asciiTab : List String
+    asciiTab
+        = ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",
+           "BS",  "HT",  "LF",  "VT",  "FF",  "CR",  "SO",  "SI",
+           "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",
+           "CAN", "EM",  "SUB", "ESC", "FS",  "GS",  "RS",  "US"]
+
+    getAt : Nat -> List String -> Maybe String
+    getAt Z     (x :: xs) = Just x
+    getAt (S k) (x :: xs) = getAt k xs
+    getAt _     []        = Nothing
+
+showLitString : List Char -> String -> String
+showLitString []        = id
+showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs
+showLitString (c  ::cs) = (showLitChar c) . showLitString cs
+
+export
+Show Char where
+  show '\'' = "'\\''"
+  show c    = strCons '\'' (showLitChar c "'")
+
+export
+Show String where
+  show cs = strCons '"' (showLitString (unpack cs) "\"")
+
+export
+Show Nat where
+  show n = show (the Integer (natToInteger n))
+
+export
+Show Bool where
+  show True = "True"
+  show False = "False"
+
+export
+Show () where
+  show () = "()"
+
+export
+(Show a, Show b) => Show (a, b) where
+  show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
+
+export
+(Show a, {y : a} -> Show (p y)) => Show (DPair a p) where
+    show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
+
+export
+Show a => Show (List a) where
+  show xs = "[" ++ show' "" xs ++ "]"
+    where
+      show' : String -> List a -> String
+      show' acc []        = acc
+      show' acc [x]       = acc ++ show x
+      show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs
+
+export
+Show a => Show (Maybe a) where
+  showPrec d Nothing  = "Nothing"
+  showPrec d (Just x) = showCon d "Just" (showArg x)
+
+export
+(Show a, Show b) => Show (Either a b) where
+  showPrec d (Left x)  = showCon d "Left" $ showArg x
+  showPrec d (Right x) = showCon d "Right" $ showArg x
--- a/libs/prelude/Prelude/Types.idr
+++ b/libs/prelude/Prelude/Types.idr
@ -0,0 +1,811 @@
+module Prelude.Types
+
+import Builtin
+import PrimIO
+import Prelude.Basics
+import Prelude.EqOrd
+import Prelude.Interfaces
+import Prelude.Num
+import Prelude.Uninhabited
+
+%default total
+
+-----------
+-- NATS ---
+-----------
+
+||| Natural numbers: unbounded, unsigned integers which can be pattern matched.
+public export
+data Nat =
+  ||| Zero.
+    Z
+  | ||| Successor.
+  S Nat
+
+%name Nat k, j, i
+
+public export
+integerToNat : Integer -> Nat
+integerToNat x
+  = if intToBool (prim__lte_Integer x 0)
+       then Z
+       else S (assert_total (integerToNat (prim__sub_Integer x 1)))
+
+-- Define separately so we can spot the name when optimising Nats
+||| Add two natural numbers.
+||| @ x the number to case-split on
+||| @ y the other numberpublic export
+public export
+plus : (1 x : Nat) -> (1 y : Nat) -> Nat
+plus Z y = y
+plus (S k) y = S (plus k y)
+
+||| Subtract natural numbers.  If the second number is larger than the first,
+||| return 0.
+public export
+minus : (1 left : Nat) -> Nat -> Nat
+minus Z        right     = Z
+minus left     Z         = left
+minus (S left) (S right) = minus left right
+
+||| Multiply natural numbers.
+public export
+mult : (1 x : Nat) -> Nat -> Nat
+mult Z y = Z
+mult (S k) y = plus y (mult k y)
+
+public export
+Num Nat where
+  (+) = plus
+  (*) = mult
+
+  fromInteger x = integerToNat x
+
+public export
+Eq Nat where
+  Z == Z = True
+  S j == S k = j == k
+  _ == _ = False
+
+public export
+Ord Nat where
+  compare Z Z = EQ
+  compare Z (S k) = LT
+  compare (S k) Z = GT
+  compare (S j) (S k) = compare j k
+
+public export
+natToInteger : Nat -> Integer
+natToInteger Z = 0
+natToInteger (S k) = 1 + natToInteger k
+                         -- integer (+) may be non-linear in second
+                         -- argument
+
+-----------
+-- PAIRS --
+-----------
+
+public export
+Functor (Pair a) where
+  map f (x, y) = (x, f y)
+
+public export
+mapFst : (a -> c) -> (a, b) -> (c, b)
+mapFst f (x, y) = (f x, y)
+
+-----------
+-- MAYBE --
+-----------
+
+||| An optional value.  This can be used to represent the possibility of
+||| failure, where a function may return a value, or not.
+public export
+data Maybe : (ty : Type) -> Type where
+  ||| No value stored
+  Nothing : Maybe ty
+
+  ||| A value of type `ty` is stored
+  Just : (1 x : ty) -> Maybe ty
+
+public export
+Uninhabited (Nothing = Just x) where
+  uninhabited Refl impossible
+
+public export
+Uninhabited (Just x = Nothing) where
+  uninhabited Refl impossible
+
+public export
+maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
+maybe n j Nothing  = n
+maybe n j (Just x) = j x
+
+public export
+Eq a => Eq (Maybe a) where
+  Nothing  == Nothing  = True
+  Nothing  == (Just _) = False
+  (Just _) == Nothing  = False
+  (Just a) == (Just b) = a == b
+
+public export
+Ord a => Ord (Maybe a) where
+  compare Nothing  Nothing  = EQ
+  compare Nothing  (Just _) = LT
+  compare (Just _) Nothing  = GT
+  compare (Just a) (Just b) = compare a b
+
+public export
+Semigroup (Maybe a) where
+  Nothing   <+> m = m
+  (Just x)  <+> _ = Just x
+
+public export
+Monoid (Maybe a) where
+  neutral = Nothing
+
+public export
+Functor Maybe where
+  map f (Just x) = Just (f x)
+  map f Nothing  = Nothing
+
+public export
+Applicative Maybe where
+  pure = Just
+
+  Just f <*> Just a = Just (f a)
+  _      <*> _        = Nothing
+
+public export
+Alternative Maybe where
+    empty = Nothing
+
+    (Just x) <|> _ = Just x
+    Nothing  <|> v = v
+
+public export
+Monad Maybe where
+  Nothing  >>= k = Nothing
+  (Just x) >>= k = k x
+
+public export
+Foldable Maybe where
+  foldr _ z Nothing  = z
+  foldr f z (Just x) = f x z
+
+public export
+Traversable Maybe where
+  traverse f Nothing = pure Nothing
+  traverse f (Just x) = (pure Just) <*> (f x)
+
+---------
+-- DEC --
+---------
+
+||| Decidability.  A decidable property either holds or is a contradiction.
+public export
+data Dec : Type -> Type where
+  ||| The case where the property holds.
+  ||| @ prf the proof
+  Yes : (prf : prop) -> Dec prop
+
+  ||| The case where the property holding would be a contradiction.
+  ||| @ contra a demonstration that prop would be a contradiction
+  No  : (contra : prop -> Void) -> Dec prop
+
+------------
+-- EITHER --
+------------
+
+||| A sum type.
+public export
+data Either : (a : Type) -> (b : Type) -> Type where
+  ||| One possibility of the sum, conventionally used to represent errors.
+  Left : forall a, b. (1 x : a) -> Either a b
+
+  ||| The other possibility, conventionally used to represent success.
+  Right : forall a, b. (1 x : b) -> Either a b
+
+||| Simply-typed eliminator for Either.
+||| @ f the action to take on Left
+||| @ g the action to take on Right
+||| @ e the sum to analyze
+public export
+either : (f : Lazy (a -> c)) -> (g : Lazy (b -> c)) -> (e : Either a b) -> c
+either l r (Left x) = l x
+either l r (Right x) = r x
+
+public export
+(Eq a, Eq b) => Eq (Either a b) where
+  Left x == Left x' = x == x'
+  Right x == Right x' = x == x'
+  _ == _ = False
+  
+public export
+(Ord a, Ord b) => Ord (Either a b) where
+  compare (Left x) (Left x') = compare x x'
+  compare (Left _) (Right _) = LT
+  compare (Right _) (Left _) = GT
+  compare (Right x) (Right x') = compare x x'
+
+%inline
+public export
+Functor (Either e) where
+  map f (Left x) = Left x
+  map f (Right x) = Right (f x)
+
+%inline
+public export
+Applicative (Either e) where
+    pure = Right
+
+    (Left a) <*> _          = Left a
+    (Right f) <*> (Right r) = Right (f r)
+    (Right _) <*> (Left l)  = Left l
+
+public export
+Monad (Either e) where
+    (Left n) >>= _ = Left n
+    (Right r) >>= f = f r
+
+-----------
+-- LISTS --
+-----------
+
+||| Generic lists.
+public export
+data List a =
+  ||| Empty list
+  Nil
+
+  | ||| A non-empty list, consisting of a head element and the rest of the list.
+  (::) a (List a)
+
+%name List xs, ys, zs
+
+public export
+Eq a => Eq (List a) where
+  [] == [] = True
+  x :: xs == y :: ys = x == y && xs == ys
+  _ == _ = False
+
+public export
+Ord a => Ord (List a) where
+  compare [] [] = EQ
+  compare [] (x :: xs) = LT
+  compare (x :: xs) [] = GT
+  compare (x :: xs) (y ::ys)
+     = case compare x y of
+            EQ => compare xs ys
+            c => c
+
+namespace List
+  public export
+  (++) : (1 xs : List a) -> List a -> List a
+  [] ++ ys = ys
+  (x :: xs) ++ ys = x :: xs ++ ys
+
+public export
+Functor List where
+  map f [] = []
+  map f (x :: xs) = f x :: map f xs
+
+public export
+Semigroup (List a) where
+  (<+>) = (++)
+
+public export
+Monoid (List a) where
+  neutral = []
+
+public export
+Foldable List where
+  foldr c n [] = n
+  foldr c n (x::xs) = c x (foldr c n xs)
+
+  foldl f q [] = q
+  foldl f q (x::xs) = foldl f (f q x) xs
+
+public export
+Applicative List where
+  pure x = [x]
+  fs <*> vs = concatMap (\f => map f vs) fs
+
+public export
+Alternative List where
+    empty = []
+    (<|>) = (++)
+
+public export
+Monad List where
+  m >>= f = concatMap f m
+
+public export
+Traversable List where
+  traverse f [] = pure []
+  traverse f (x::xs) = pure (::) <*> (f x) <*> (traverse f xs)
+
+||| Check if something is a member of a list using the default Boolean equality.
+public export
+elem : Eq a => a -> List a -> Bool
+x `elem` [] = False
+x `elem` (y :: ys) = if x == y then True else x `elem` ys
+
+-------------
+-- STREAMS --
+-------------
+
+namespace Stream
+  ||| An infinite stream.
+  public export
+  data Stream : Type -> Type where
+       (::) : a -> Inf (Stream a) -> Stream a
+
+public export
+Functor Stream where
+  map f (x :: xs) = f x :: map f xs
+
+||| The first element of an infinite stream.
+public export
+head : Stream a -> a
+head (x :: xs) = x
+
+||| All but the first element.
+public export
+tail : Stream a -> Stream a
+tail (x :: xs) = xs
+
+||| Take precisely n elements from the stream.
+||| @ n how many elements to take
+||| @ xs the stream
+public export
+take : (1 n : Nat) -> (xs : Stream a) -> List a
+take Z xs = []
+take (S k) (x :: xs) = x :: take k xs
+
+-------------
+-- STRINGS --
+-------------
+
+namespace Strings
+  public export
+  (++) : (1 x : String) -> (1 y : String) -> String
+  x ++ y = prim__strAppend x y
+
+||| Returns the length of the string.
+|||
+||| ```idris example
+||| length ""
+||| ```
+||| ```idris example
+||| length "ABC"
+||| ```
+public export
+length : String -> Nat
+length str = fromInteger (prim__cast_IntInteger (prim__strLength str))
+
+||| Reverses the elements within a string.
+|||
+||| ```idris example
+||| reverse "ABC"
+||| ```
+||| ```idris example
+||| reverse ""
+||| ```
+public export
+reverse : String -> String
+reverse = prim__strReverse
+
+||| Returns a substring of a given string
+|||
+||| @ index The (zero based) index of the string to extract.  If this is beyond
+|||         the end of the string, the function returns the empty string.
+||| @ len The desired length of the substring.  Truncated if this exceeds the
+|||       length of the input
+||| @ subject The string to return a portion of
+public export
+substr : (index : Nat) -> (len : Nat) -> (subject : String) -> String
+substr s e subj
+    = if natToInteger s < natToInteger (length subj)
+         then prim__strSubstr (prim__cast_IntegerInt (natToInteger s))
+                              (prim__cast_IntegerInt (natToInteger e))
+                              subj
+         else ""
+
+||| Adds a character to the front of the specified string.
+|||
+||| ```idris example
+||| strCons 'A' "B"
+||| ```
+||| ```idris example
+||| strCons 'A' ""
+||| ```
+public export
+strCons : Char -> String -> String
+strCons = prim__strCons
+
+public export
+strUncons : String -> Maybe (Char, String)
+strUncons "" = Nothing
+strUncons str = assert_total $ Just (prim__strHead str, prim__strTail str)
+
+||| Turns a list of characters into a string.
+public export
+pack : List Char -> String
+pack [] = ""
+pack (x :: xs) = strCons x (pack xs)
+
+export
+fastPack : List Char -> String
+fastPack xs
+   = unsafePerformIO (schemeCall String "string" (toFArgs xs))
+  where
+    toFArgs : List Char -> FArgList
+    toFArgs [] = []
+    toFArgs (x :: xs) = x :: toFArgs xs
+
+||| Turns a string into a list of characters.
+|||
+||| ```idris example
+||| unpack "ABC"
+||| ```
+public export
+unpack : String -> List Char
+unpack str = unpack' (prim__cast_IntegerInt (natToInteger (length str)) - 1) str []
+  where
+    unpack' : Int -> String -> List Char -> List Char
+    unpack' pos str acc
+        = if pos < 0
+             then acc
+             else assert_total $ unpack' (pos - 1) str (assert_total (prim__strIndex str pos)::acc)
+
+public export
+Semigroup String where
+  (<+>) = (++)
+
+public export
+Monoid String where
+  neutral = ""
+
+----------------
+-- CHARACTERS --
+----------------
+
+||| Returns true if the character is in the range [A-Z].
+public export
+isUpper : Char -> Bool
+isUpper x = x >= 'A' && x <= 'Z'
+
+||| Returns true if the character is in the range [a-z].
+public export
+isLower : Char -> Bool
+isLower x = x >= 'a' && x <= 'z'
+
+||| Returns true if the character is in the ranges [A-Z][a-z].
+public export
+isAlpha : Char -> Bool
+isAlpha x = isUpper x || isLower x
+
+||| Returns true if the character is in the range [0-9].
+public export
+isDigit : Char -> Bool
+isDigit x = (x >= '0' && x <= '9')
+
+||| Returns true if the character is in the ranges [A-Z][a-z][0-9].
+public export
+isAlphaNum : Char -> Bool
+isAlphaNum x = isDigit x || isAlpha x
+
+||| Returns true if the character is a whitespace character.
+public export
+isSpace : Char -> Bool
+isSpace x
+    = x == ' '  || x == '\t' || x == '\r' ||
+      x == '\n' || x == '\f' || x == '\v' ||
+      x == '\xa0'
+
+||| Returns true if the character represents a new line.
+public export
+isNL : Char -> Bool
+isNL x = x == '\r' || x == '\n'
+
+||| Convert a letter to the corresponding upper-case letter, if any.
+||| Non-letters are ignored.
+public export
+toUpper : Char -> Char
+toUpper x
+    = if (isLower x)
+         then prim__cast_IntChar (prim__cast_CharInt x - 32)
+         else x
+
+||| Convert a letter to the corresponding lower-case letter, if any.
+||| Non-letters are ignored.
+public export
+toLower : Char -> Char
+toLower x
+    = if (isUpper x)
+         then prim__cast_IntChar (prim__cast_CharInt x + 32)
+         else x
+
+||| Returns true if the character is a hexadecimal digit i.e. in the range
+||| [0-9][a-f][A-F].
+public export
+isHexDigit : Char -> Bool
+isHexDigit x = elem (toUpper x) hexChars where
+  hexChars : List Char
+  hexChars
+      = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
+         'A', 'B', 'C', 'D', 'E', 'F']
+
+||| Returns true if the character is an octal digit.
+public export
+isOctDigit : Char -> Bool
+isOctDigit x = (x >= '0' && x <= '7')
+
+||| Returns true if the character is a control character.
+public export
+isControl : Char -> Bool
+isControl x
+    = (x >= '\x0000' && x <= '\x001f')
+       || (x >= '\x007f' && x <= '\x009f')
+
+||| Convert the number to its backend dependent (usually Unicode) Char
+||| equivalent.
+public export
+chr : Int -> Char
+chr = prim__cast_IntChar
+
+||| Return the backend dependent (usually Unicode) numerical equivalent of the Char.
+public export
+ord : Char -> Int
+ord = prim__cast_CharInt
+
+-----------------------
+-- DOUBLE PRIMITIVES --
+-----------------------
+
+public export
+pi : Double
+pi = 3.14159265358979323846
+
+public export
+euler : Double
+euler = 2.7182818284590452354
+
+public export
+exp : Double -> Double
+exp x = prim__doubleExp x
+
+public export
+log : Double -> Double
+log x = prim__doubleLog x
+
+public export
+pow : Double -> Double -> Double
+pow x y = exp (y * log x)
+
+public export
+sin : Double -> Double
+sin x = prim__doubleSin x
+
+public export
+cos : Double -> Double
+cos x = prim__doubleCos x
+
+public export
+tan : Double -> Double
+tan x = prim__doubleTan x
+
+public export
+asin : Double -> Double
+asin x = prim__doubleASin x
+
+public export
+acos : Double -> Double
+acos x = prim__doubleACos x
+
+public export
+atan : Double -> Double
+atan x = prim__doubleATan x
+
+public export
+sinh : Double -> Double
+sinh x = (exp x - exp (-x)) / 2
+
+public export
+cosh : Double -> Double
+cosh x = (exp x + exp (-x)) / 2
+
+public export
+tanh : Double -> Double
+tanh x = sinh x / cosh x
+
+public export
+sqrt : Double -> Double
+sqrt x = prim__doubleSqrt x
+
+public export
+floor : Double -> Double
+floor x = prim__doubleFloor x
+
+public export
+ceiling : Double -> Double
+ceiling x = prim__doubleCeiling x
+
+-----------
+-- CASTS --
+-----------
+
+-- Casts between primitives only here.  They might be lossy.
+
+||| Interface for transforming an instance of a data type to another type.
+public export
+interface Cast from to where
+  ||| Perform a (potentially lossy!) cast operation.
+  ||| @ orig The original type
+  cast : (orig : from) -> to
+
+-- To String
+
+export
+Cast Int String where
+  cast = prim__cast_IntString
+
+export
+Cast Integer String where
+  cast = prim__cast_IntegerString
+
+export
+Cast Char String where
+  cast = prim__cast_CharString
+
+export
+Cast Double String where
+  cast = prim__cast_DoubleString
+
+-- To Integer
+
+export
+Cast Int Integer where
+  cast = prim__cast_IntInteger
+
+export
+Cast Char Integer where
+  cast = prim__cast_CharInteger
+
+export
+Cast Double Integer where
+  cast = prim__cast_DoubleInteger
+
+export
+Cast String Integer where
+  cast = prim__cast_StringInteger
+
+export
+Cast Nat Integer where
+  cast = natToInteger
+
+-- To Int
+
+export
+Cast Integer Int where
+  cast = prim__cast_IntegerInt
+
+export
+Cast Char Int where
+  cast = prim__cast_CharInt
+
+export
+Cast Double Int where
+  cast = prim__cast_DoubleInt
+
+export
+Cast String Int where
+  cast = prim__cast_StringInt
+
+export
+Cast Nat Int where
+  cast = fromInteger . natToInteger
+
+-- To Char
+
+export
+Cast Int Char where
+  cast = prim__cast_IntChar
+
+-- To Double
+
+export
+Cast Int Double where
+  cast = prim__cast_IntDouble
+
+export
+Cast Integer Double where
+  cast = prim__cast_IntegerDouble
+
+export
+Cast String Double where
+  cast = prim__cast_StringDouble
+
+export
+Cast Nat Double where
+  cast = prim__cast_IntegerDouble . natToInteger
+
+------------
+-- RANGES --
+------------
+
+public export
+countFrom : n -> (n -> n) -> Stream n
+countFrom start diff = start :: countFrom (diff start) diff
+
+-- this and takeBefore are for range syntax, and not exported here since
+-- they're partial. They are exported from Data.Stream instead.
+partial
+takeUntil : (n -> Bool) -> Stream n -> List n
+takeUntil p (x :: xs)
+    = if p x
+         then [x]
+         else x :: takeUntil p xs
+
+partial
+takeBefore : (n -> Bool) -> Stream n -> List n
+takeBefore p (x :: xs)
+    = if p x
+         then []
+         else x :: takeBefore p xs
+
+public export
+interface Range a where
+  rangeFromTo : a -> a -> List a
+  rangeFromThenTo : a -> a -> a -> List a
+
+  rangeFrom : a -> Stream a
+  rangeFromThen : a -> a -> Stream a
+
+-- Idris 1 went to great lengths to prove that these were total. I don't really
+-- think it's worth going to those lengths! Let's keep it simple and assert.
+export
+Range Nat where
+  rangeFromTo x y
+      = if y > x
+           then assert_total $ takeUntil (>= y) (countFrom x S)
+           else if x > y
+                   then assert_total $ takeUntil (<= y) (countFrom x (\n => minus n 1))
+                   else [x]
+  rangeFromThenTo x y z
+      = if y > x
+           then (if z > x
+                    then assert_total $ takeBefore (> z) (countFrom x (plus (minus y x)))
+                    else [])
+           else (if x == y
+                    then (if x == z then [x] else [])
+                    else assert_total $ takeBefore (< z) (countFrom x (\n => minus n (minus x y))))
+  rangeFrom x = countFrom x S
+  rangeFromThen x y
+      = if y > x
+           then countFrom x (plus (minus y x))
+           else countFrom x (\n => minus n (minus x y))
+
+export
+(Integral a, Ord a, Neg a) => Range a where
+  rangeFromTo x y
+      = if y > x
+           then assert_total $ takeUntil (>= y) (countFrom x (+1))
+           else if x > y
+                   then assert_total $ takeUntil (<= y) (countFrom x (\x => x-1))
+                   else [x]
+  rangeFromThenTo x y z
+      = if (z - x) > (z - y)
+           then -- go up
+             assert_total $ takeBefore (> z) (countFrom x (+ (y-x)))
+           else if (z - x) < (z - y)
+                then -- go down
+                     assert_total $ takeBefore (< z) (countFrom x (\n => n - (x - y)))
+                else -- meaningless
+                  if x == y && y == z
+                     then [x] else []
+  rangeFrom x = countFrom x (1+)
+  rangeFromThen x y
+      = if y > x
+           then countFrom x (+ (y - x))
+           else countFrom x (\n => n - (x - y))
--- a/libs/prelude/Prelude/Uninhabited.idr
+++ b/libs/prelude/Prelude/Uninhabited.idr
@ -28,3 +28,12 @@ Uninhabited Void where
 public export
 absurd : Uninhabited t => (h : t) -> a
 absurd h = void (uninhabited h)
+
+public export
+Uninhabited (True = False) where
+  uninhabited Refl impossible
+
+public export
+Uninhabited (False = True) where
+  uninhabited Refl impossible
+
--- a/libs/prelude/prelude.ipkg
+++ b/libs/prelude/prelude.ipkg
@ -6,4 +6,11 @@ modules = Builtin,
          PrimIO,
          Prelude,
          Prelude.Basics,
+          Prelude.EqOrd,
+          Prelude.Interfaces,
+          Prelude.IO,
+          Prelude.Num,
+          Prelude.Ops,
+          Prelude.Show,
+          Prelude.Types,
          Prelude.Uninhabited
--- a/src/Compiler/CompileExpr.idr
+++ b/src/Compiler/CompileExpr.idr
@ -136,14 +136,14 @@ mkDropSubst i es rest (x :: xs)
 -- Common.idr, so that they get compiled, as they won't be spotted by the
 -- usual calls to 'getRefs'.
 natHack : CExp vars -> CExp vars
-natHack (CCon fc (NS ["Prelude"] (UN "Z")) _ []) = CPrimVal fc (BI 0)
-natHack (CCon fc (NS ["Prelude"] (UN "S")) _ [k])
+natHack (CCon fc (NS ["Types", "Prelude"] (UN "Z")) _ []) = CPrimVal fc (BI 0)
+natHack (CCon fc (NS ["Types", "Prelude"] (UN "S")) _ [k])
    = CApp fc (CRef fc (UN "prim__add_Integer")) [CPrimVal fc (BI 1), k]
-natHack (CApp fc (CRef _ (NS ["Prelude"] (UN "natToInteger"))) [k]) = k
-natHack (CApp fc (CRef _ (NS ["Prelude"] (UN "integerToNat"))) [k]) = k
-natHack (CApp fc (CRef fc' (NS ["Prelude"] (UN "plus"))) args)
+natHack (CApp fc (CRef _ (NS ["Types", "Prelude"] (UN "natToInteger"))) [k]) = k
+natHack (CApp fc (CRef _ (NS ["Types", "Prelude"] (UN "integerToNat"))) [k]) = k
+natHack (CApp fc (CRef fc' (NS ["Types", "Prelude"] (UN "plus"))) args)
    = CApp fc (CRef fc' (UN "prim__add_Integer")) args
-natHack (CApp fc (CRef fc' (NS ["Prelude"] (UN "mult"))) args)
+natHack (CApp fc (CRef fc' (NS ["Types", "Prelude"] (UN "mult"))) args)
    = CApp fc (CRef fc' (UN "prim__mul_Integer")) args
 natHack (CApp fc (CRef fc' (NS ["Nat", "Data"] (UN "minus"))) args)
    = CApp fc (CRef fc' (UN "prim__sub_Integer")) args
@ -151,22 +151,22 @@ natHack (CLam fc x exp) = CLam fc x (natHack exp)
 natHack t = t

 isNatCon : Name -> Bool
-isNatCon (NS ["Prelude"] (UN "Z")) = True
-isNatCon (NS ["Prelude"] (UN "S")) = True
+isNatCon (NS ["Types", "Prelude"] (UN "Z")) = True
+isNatCon (NS ["Types", "Prelude"] (UN "S")) = True
 isNatCon _ = False

 natBranch : CConAlt vars -> Bool
 natBranch (MkConAlt n _ _ _) = isNatCon n

 trySBranch : CExp vars -> CConAlt vars -> Maybe (CExp vars)
-trySBranch n (MkConAlt (NS ["Prelude"] (UN "S")) _ [arg] sc)
+trySBranch n (MkConAlt (NS ["Types", "Prelude"] (UN "S")) _ [arg] sc)
    = let fc = getFC n in
          Just (CLet fc arg True (CApp fc (CRef fc (UN "prim__sub_Integer"))
                    [n, CPrimVal fc (BI 1)]) sc)
 trySBranch _ _ = Nothing

 tryZBranch : CConAlt vars -> Maybe (CExp vars)
-tryZBranch (MkConAlt (NS ["Prelude"] (UN "Z")) _ [] sc) = Just sc
+tryZBranch (MkConAlt (NS ["Types", "Prelude"] (UN "Z")) _ [] sc) = Just sc
 tryZBranch _ = Nothing

 getSBranch : CExp vars -> List (CConAlt vars) -> Maybe (CExp vars)
@ -198,15 +198,15 @@ boolHackTree (CConCase fc sc alts def)
         CConstCase fc sc alts' def
  where
    toBool : CConAlt vars -> Maybe (CConstAlt vars)
-    toBool (MkConAlt (NS ["Prelude"] (UN "True")) (Just tag) [] sc)
+    toBool (MkConAlt (NS ["Basics", "Prelude"] (UN "True")) (Just tag) [] sc)
        = Just $ MkConstAlt (I tag) sc
-    toBool (MkConAlt (NS ["Prelude"] (UN "False")) (Just tag) [] sc)
+    toBool (MkConAlt (NS ["Basics", "Prelude"] (UN "False")) (Just tag) [] sc)
        = Just $ MkConstAlt (I tag) sc
-    toBool (MkConAlt (NS ["Prelude"] (UN "LT")) (Just tag) [] sc)
+    toBool (MkConAlt (NS ["EqOrd", "Prelude"] (UN "LT")) (Just tag) [] sc)
        = Just $ MkConstAlt (I tag) sc
-    toBool (MkConAlt (NS ["Prelude"] (UN "EQ")) (Just tag) [] sc)
+    toBool (MkConAlt (NS ["EqOrd", "Prelude"] (UN "EQ")) (Just tag) [] sc)
        = Just $ MkConstAlt (I tag) sc
-    toBool (MkConAlt (NS ["Prelude"] (UN "GT")) (Just tag) [] sc)
+    toBool (MkConAlt (NS ["EqOrd", "Prelude"] (UN "GT")) (Just tag) [] sc)
        = Just $ MkConstAlt (I tag) sc
    toBool _ = Nothing
 boolHackTree t = t
@ -219,15 +219,15 @@ mutual
      = pure $ CLocal fc prf
  -- TMP HACK: extend this to all types which look like enumerations
  -- after erasure
-  toCExpTm n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "True")))
+  toCExpTm n (Ref fc (DataCon tag Z) (NS ["Basics", "Prelude"] (UN "True")))
      = pure $ CPrimVal fc (I tag)
-  toCExpTm n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "False")))
+  toCExpTm n (Ref fc (DataCon tag Z) (NS ["Basics", "Prelude"] (UN "False")))
      = pure $ CPrimVal fc (I tag)
-  toCExpTm n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "LT")))
+  toCExpTm n (Ref fc (DataCon tag Z) (NS ["EqOrd", "Prelude"] (UN "LT")))
      = pure $ CPrimVal fc (I tag)
-  toCExpTm n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "EQ")))
+  toCExpTm n (Ref fc (DataCon tag Z) (NS ["EqOrd", "Prelude"] (UN "EQ")))
      = pure $ CPrimVal fc (I tag)
-  toCExpTm n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "GT")))
+  toCExpTm n (Ref fc (DataCon tag Z) (NS ["EqOrd", "Prelude"] (UN "GT")))
      = pure $ CPrimVal fc (I tag)
  toCExpTm n (Ref fc (DataCon tag arity) fn)
      = -- get full name for readability, and the Nat hack
--- a/src/Core/Reflect.idr
+++ b/src/Core/Reflect.idr
@ -39,8 +39,12 @@ appCon fc defs n args
         resolved (gamma defs) (apply fc fn args)

 export
-prelude : String -> Name
-prelude n = NS ["Prelude"] (UN n)
+preludetypes : String -> Name
+preludetypes n = NS ["Types", "Prelude"] (UN n)
+
+export
+basics : String -> Name
+basics n = NS ["Basics", "Prelude"] (UN n)

 export
 builtin : String -> Name
@ -136,8 +140,8 @@ Reify Bool where

 export
 Reflect Bool where
-  reflect fc defs lhs env True = getCon fc defs (prelude "True")
-  reflect fc defs lhs env False = getCon fc defs (prelude "False")
+  reflect fc defs lhs env True = getCon fc defs (basics "True")
+  reflect fc defs lhs env False = getCon fc defs (basics "False")

 export
 Reify Nat where
@ -152,10 +156,10 @@ Reify Nat where

 export
 Reflect Nat where
-  reflect fc defs lhs env Z = getCon fc defs (prelude "Z")
+  reflect fc defs lhs env Z = getCon fc defs (preludetypes "Z")
  reflect fc defs lhs env (S k)
      = do k' <- reflect fc defs lhs env k
-           appCon fc defs (prelude "S") [k']
+           appCon fc defs (preludetypes "S") [k']

 export
 Reify a => Reify (List a) where
@ -171,11 +175,11 @@ Reify a => Reify (List a) where

 export
 Reflect a => Reflect (List a) where
-  reflect fc defs lhs env [] = appCon fc defs (prelude "Nil") [Erased fc False]
+  reflect fc defs lhs env [] = appCon fc defs (preludetypes "Nil") [Erased fc False]
  reflect fc defs lhs env (x :: xs)
      = do x' <- reflect fc defs lhs env x
           xs' <- reflect fc defs lhs env xs
-           appCon fc defs (prelude "::") [Erased fc False, x', xs']
+           appCon fc defs (preludetypes "::") [Erased fc False, x', xs']

 export
 Reify a => Reify (Maybe a) where
@ -190,10 +194,10 @@ Reify a => Reify (Maybe a) where

 export
 Reflect a => Reflect (Maybe a) where
-  reflect fc defs lhs env Nothing = appCon fc defs (prelude "Nothing") [Erased fc False]
+  reflect fc defs lhs env Nothing = appCon fc defs (preludetypes "Nothing") [Erased fc False]
  reflect fc defs lhs env (Just x)
      = do x' <- reflect fc defs lhs env x
-           appCon fc defs (prelude "Just") [Erased fc False, x']
+           appCon fc defs (preludetypes "Just") [Erased fc False, x']

 export
 (Reify a, Reify b) => Reify (a, b) where
--- a/src/Idris/Error.idr
+++ b/src/Idris/Error.idr
@ -99,7 +99,8 @@ perror (InvisibleName fc x Nothing)
 perror (BadTypeConType fc n)
    = pure $ "Return type of " ++ show n ++ " must be Type at:\n" ++ !(ploc fc)
 perror (BadDataConType fc n fam)
-    = pure $ "Return type of " ++ show n ++ " must be in " ++ show fam ++ " at:\n" ++ !(ploc fc)
+    = pure $ "Return type of " ++ show n ++ " must be in "
+                 ++ show !(toFullNames fam) ++ " at:\n" ++ !(ploc fc)
 perror (NotCovering fc n IsCovering)
    = pure $ "Internal error (Coverage of " ++ show n ++ ")"
 perror (NotCovering fc n (MissingCases cs))
--- a/src/Idris/Resugar.idr
+++ b/src/Idris/Resugar.idr
@ -95,11 +95,17 @@ unbracket tm = tm
 ||| Attempt to extract a constant natural number
 extractNat : Nat -> PTerm -> Maybe Nat
 extractNat acc tm = case tm of
-  PRef _ (NS ["Prelude"] (UN "Z"))            => pure acc
-  PApp _ (PRef _ (NS ["Prelude"] (UN "S"))) k => extractNat (1 + acc) k
-  PPrimVal _ (BI n)                           => pure (acc + integerToNat n)
-  PBracketed _ k                              => extractNat acc k
-  _                                           => Nothing
+  PRef _ (NS ["Types", "Prelude"] (UN "Z"))
+         => pure acc
+  PApp _ (PRef _ (NS ["Types", "Prelude"] (UN "S"))) k
+         => extractNat (1 + acc) k
+  PRef _ (NS ["Prelude"] (UN "Z"))
+         => pure acc
+  PApp _ (PRef _ (NS ["Prelude"] (UN "S"))) k
+         => extractNat (1 + acc) k
+  PPrimVal _ (BI n) => pure (acc + integerToNat n)
+  PBracketed _ k    => extractNat acc k
+  _                 => Nothing

 mutual

@ -121,6 +127,11 @@ mutual
        _           => Nothing
      _        => Nothing
  -- refolding natural numbers if the expression is a constant
+  -- we might see either Prelude.Types.Nat or Prelude.Nat, depending on whether
+  -- unelaboration used the canonical name or not
+  sugarAppM (PRef fc (NS ["Types", "Prelude"] (UN "Z"))) = pure $ PPrimVal fc (BI 0)
+  sugarAppM (PApp fc (PRef _ (NS ["Types", "Prelude"] (UN "S"))) k) =
+    PPrimVal fc . BI . cast <$> extractNat 1 k
  sugarAppM (PRef fc (NS ["Prelude"] (UN "Z"))) = pure $ PPrimVal fc (BI 0)
  sugarAppM (PApp fc (PRef _ (NS ["Prelude"] (UN "S"))) k) =
    PPrimVal fc . BI . cast <$> extractNat 1 k
--- a/src/TTImp/Elab/Quote.idr
+++ b/src/TTImp/Elab/Quote.idr
@ -237,7 +237,7 @@ checkQuoteDecl rig elabinfo nest env fc ds exp
         qds <- reflect fc defs (onLHS (elabMode elabinfo)) env ds'
         unqs <- get Unq
         qd <- getCon fc defs (reflectionttimp "Decl")
-         qty <- appCon fc defs (prelude "List") [qd]
+         qty <- appCon fc defs (preludetypes "List") [qd]
         checkExp rig elabinfo env fc
                  !(bindUnqs unqs rig elabinfo nest env qds)
                  (gnf env qty) exp
--- a/src/TTImp/Unelab.idr
+++ b/src/TTImp/Unelab.idr
@ -142,7 +142,10 @@ mutual
               | Nothing => case umode of
                                 ImplicitHoles => pure (Implicit fc True, gErased fc)
                                 _ => pure (IVar fc n, gErased fc)
-           pure (IVar fc !(aliasName !(getFullName n)), gnf env (embed ty))
+           n' <- case umode of
+                      NoSugar _ => getFullName n
+                      _ => aliasName !(getFullName n)
+           pure (IVar fc n', gnf env (embed ty))
  unelabTy' umode env (Meta fc n i args)
      = do defs <- get Ctxt
           let mkn = nameRoot n
--- a/tests/ideMode/ideMode001/expected
+++ b/tests/ideMode/ideMode001/expected
@ -8,18 +8,18 @@
 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 ?{_:242}_[] ?{_:241}_[])")))))) 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 ?{_:231}_[] ?{_:230}_[])")))))) 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:221} : (Main.Vect n[0] a[1])) -> (({arg:222} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:769:1--776:1 n[2] m[4]) a[3])))")))))) 1)
+0001eb(: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.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> (({arg:221} : (Main.Vect n[0] a[1])) -> (({arg:222} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64: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)
+0000d9(: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.Types.Nat")))))) 1)
+0000d9(: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.Types.Nat")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 29) (:end 5 30)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 28)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 28)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 17) (:end 5 18)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 16)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 16)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 41) (:end 3 42)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 38) (:end 3 39)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 38) (:end 3 39)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 25) (:end 3 26)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 24)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 24)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 13) (:end 3 14)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 2 19) (:end 2 20)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 000015(:return (:ok ()) 1)
--- a/tests/ideMode/ideMode003/expected
+++ b/tests/ideMode/ideMode003/expected
@ -8,18 +8,18 @@
 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 ?{_:242}_[] ?{_:241}_[])")))))) 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 ?{_:231}_[] ?{_:230}_[])")))))) 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:221} : (Main.Vect n[0] a[1])) -> (({arg:222} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:769:1--776:1 n[2] m[4]) a[3])))")))))) 1)
+0001eb(: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.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> (({arg:221} : (Main.Vect n[0] a[1])) -> (({arg:222} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64: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)
+0000d9(: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.Types.Nat")))))) 1)
+0000d9(: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.Types.Nat")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 29) (:end 5 30)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 28)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 28)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 17) (:end 5 18)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 16)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 16)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 41) (:end 3 42)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 38) (:end 3 39)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 38) (:end 3 39)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 25) (:end 3 26)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 24)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
+0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 24)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 13) (:end 3 14)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 2 19) (:end 2 20)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 000015(:return (:ok ()) 1)
--- a/tests/idris2/docs001/expected
+++ b/tests/idris2/docs001/expected
@ -78,9 +78,9 @@ join : m (m a) -> m a
 	 Also called `flatten` or mu.

 Implementations:
+	Monad IO
 	Monad Maybe
 	Monad (Either e)
 	Monad List
-	Monad IO

 Main> Bye for now!
--- a/tests/idris2/reflection003/expected
+++ b/tests/idris2/reflection003/expected
@ -1,10 +1,10 @@
 1/1: Building refprims (refprims.idr)
-LOG 0: Name: Prelude.List.++
-LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just xs) (Prelude.List a) (%pi RigW Explicit (Just {arg:6633}) (Prelude.List a) (Prelude.List a))))
-LOG 0: Name: Prelude.Strings.++
+LOG 0: Name: Prelude.Types.List.++
+LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just xs) (Prelude.Types.List a) (%pi RigW Explicit (Just {arg:2578}) (Prelude.Types.List a) (Prelude.Types.List a))))
+LOG 0: Name: Prelude.Types.Strings.++
 LOG 0: Type: (%pi Rig1 Explicit (Just x) String (%pi Rig1 Explicit (Just y) String String))
-LOG 0: Resolved name: Prelude.Nat
-LOG 0: Constructors: [Prelude.Z, Prelude.S]
+LOG 0: Resolved name: Prelude.Types.Nat
+LOG 0: Constructors: [Prelude.Types.Z, Prelude.Types.S]
 refprims.idr:43:10--43:27:While processing right hand side of dummy1 at refprims.idr:43:1--45:1:
 Error during reflection: Not really trying at:
 43	dummy1 = %runElab logPrims
--- a/tests/idris2/reflection006/expected
+++ b/tests/idris2/reflection006/expected
@ -1,7 +1,7 @@
 1/1: Building refleq (refleq.idr)
 LOG 0: [x, y]
-LOG 0: Left: ((Prelude.plus x) y)
-LOG 0: Right: ((Prelude.plus y) x)
+LOG 0: Left: ((Prelude.Types.plus x) y)
+LOG 0: Right: ((Prelude.Types.plus y) x)
 refleq.idr:24:16--24:21:While processing right hand side of commutes at refleq.idr:24:1--25:1:
 Error during reflection: Not done at:
 24	commutes x y = prove
--- a/tests/idris2/reflection007/NatExpr.idr
+++ b/tests/idris2/reflection007/NatExpr.idr
@ -9,14 +9,14 @@ data NatExpr : Nat -> Type where
     Val : (val : Nat) -> NatExpr val

 getNatExpr : TTImp -> Elab (n ** NatExpr n)
-getNatExpr `(Prelude.plus ~(x) ~(y))
+getNatExpr `(Prelude.Types.plus ~(x) ~(y))
   = do (_ ** xval) <- getNatExpr x
        (_ ** yval) <- getNatExpr y
        pure (_ ** Plus xval yval)
-getNatExpr `(Prelude.mult (Prelude.S (Prelude.S Prelude.Z)) ~(y))
+getNatExpr `(Prelude.Types.mult (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)) ~(y))
   = do (y ** yval) <- getNatExpr y
        pure (_ ** Dbl yval)
-getNatExpr `(Prelude.mult ~(x) ~(y))
+getNatExpr `(Prelude.Types.mult ~(x) ~(y))
   = do (_ ** xval) <- getNatExpr x
        (_ ** yval) <- getNatExpr y
        pure (_ ** Mult xval yval)