agda2hs-1.3: lib/Haskell/Prelude.agda
{-# OPTIONS --no-auto-inline #-}
module Haskell.Prelude where
open import Haskell.Prim
open Haskell.Prim public using
( Bool; True; False; Char; Integer;
List; []; _∷_; Nat; zero; suc; ⊤; tt;
TypeError; ⊥; iNumberNat; lengthNat;
IsTrue; IsFalse; NonEmpty;
All; allNil; allCons;
Any; anyHere; anyThere;
id; _∘_; _$_; flip; const;
if_then_else_; case_of_;
Number; fromNat; Negative; fromNeg;
IsString; fromString;
_≡_; refl;
a; b; c; d; e; f; m; s; t )
open import Haskell.Prim.Absurd public
open import Haskell.Prim.Applicative public
open import Haskell.Prim.Bool public
open import Haskell.Prim.Bounded public
open import Haskell.Prim.Char public
open import Haskell.Prim.Double public
open import Haskell.Prim.Either public
open import Haskell.Prim.Enum public
open import Haskell.Prim.Eq public
open import Haskell.Prim.Foldable public
open import Haskell.Prim.Functor public
open import Haskell.Prim.Int public
open import Haskell.Prim.Integer public
open import Haskell.Prim.IO public
open import Haskell.Prim.List public
open import Haskell.Prim.Maybe public
open import Haskell.Prim.Monad public
open import Haskell.Prim.Monoid public
open import Haskell.Prim.Num public
open import Haskell.Prim.Ord public
open import Haskell.Prim.Show public
open import Haskell.Prim.String public
open import Haskell.Prim.Traversable public
open import Haskell.Prim.Tuple public hiding (first; second; _***_)
open import Haskell.Prim.Word public
-- Problematic features
-- - [Partial]: Could pass implicit/instance arguments to prove totality.
-- - [Float]: Or Float (Agda floats are Doubles)
-- - [Infinite]: Define colists and map to Haskell lists?
-- Missing from the Haskell Prelude:
--
-- Float [Float]
-- Rational
--
-- Real(toRational),
-- Integral(quot, rem, div, mod, quotRem, divMod, toInteger),
-- Fractional((/), recip, fromRational),
-- Floating(pi, exp, log, sqrt, (**), logBase, sin, cos, tan,
-- asin, acos, atan, sinh, cosh, tanh, asinh, acosh, atanh),
-- RealFrac(properFraction, truncate, round, ceiling, floor),
-- RealFloat(floatRadix, floatDigits, floatRange, decodeFloat,
-- encodeFloat, exponent, significand, scaleFloat, isNaN,
-- isInfinite, isDenormalized, isIEEE, isNegativeZero, atan2),
--
-- subtract, even, odd, gcd, lcm, (^), (^^),
-- fromIntegral, realToFrac,
--
-- foldr1, foldl1, maximum, minimum [Partial]
--
-- until [Partial]
--
-- iterate, repeat, cycle [Infinite]
--
-- ReadS, Read(readsPrec, readList),
-- reads, readParen, read, lex,
--
-- IO, putChar, putStr, putStrLn, print,
-- getChar, getLine, getContents, interact,
-- FilePath, readFile, writeFile, appendFile, readIO, readLn,
-- IOError, ioError, userError,
--------------------------------------------------
-- Functions
infixr 0 _$!_
_$!_ : (a → b) → a → b
_$!_ = _$_
seq : a → b → b
seq = const id
asTypeOf : a → a → a
asTypeOf x _ = x
undefined : {@0 @(tactic absurd) i : ⊥} → a
undefined {i = ()}
error : {@0 @(tactic absurd) i : ⊥} → String → a
error {i = ()} err
errorWithoutStackTrace : {@0 @(tactic absurd) i : ⊥} → String → a
errorWithoutStackTrace {i = ()} err
-------------------------------------------------
-- More List functions
-- These uses Eq, Ord, or Foldable, so can't go in Prim.List without
-- turning those dependencies around.
reverse : List a → List a
reverse = foldl (flip _∷_) []
infixl 9 _!!_ _!!ᴺ_
_!!ᴺ_ : (xs : List a) (n : Nat) → @0 ⦃ IsTrue (n < lengthNat xs) ⦄ → a
(x ∷ xs) !!ᴺ zero = x
(x ∷ xs) !!ᴺ suc n = xs !!ᴺ n
_!!_ : (xs : List a) (n : Int)
→ ⦃ @0 nn : IsNonNegativeInt n ⦄
→ ⦃ @0 _ : IsTrue (intToNat n {{nn}} < lengthNat xs) ⦄ → a
xs !! n = xs !!ᴺ intToNat n
lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b
lookup x [] = Nothing
lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs
-------------------------------------------------
-- Unsafe functions
coerce : @0 a ≡ b → a → b
coerce refl x = x
IsJust : Maybe a → Set
IsJust Nothing = ⊥
IsJust (Just _) = ⊤
fromJust : (x : Maybe a) → @0 {IsJust x} → a
fromJust Nothing = error "fromJust Nothing"
fromJust (Just x) = x