From f89dad77b4c3eac2e1106f6aa30580b42a086316 Mon Sep 17 00:00:00 2001 From: jespercockx Date: Tue, 24 Sep 2024 08:06:43 +0000 Subject: [PATCH] deploy: 293306eaeefb6464969464473e21629a595fa3a2 --- lib/Agda.Builtin.Bool.html | 17 ++ lib/Agda.Builtin.Char.html | 20 ++ lib/Agda.Builtin.Equality.html | 11 + lib/Agda.Builtin.Float.html | 211 +++++++++++++ lib/Agda.Builtin.FromNat.html | 18 ++ lib/Agda.Builtin.FromNeg.html | 18 ++ lib/Agda.Builtin.FromString.html | 18 ++ lib/Agda.Builtin.Int.html | 20 ++ lib/Agda.Builtin.List.html | 18 ++ lib/Agda.Builtin.Maybe.html | 11 + lib/Agda.Builtin.Nat.html | 136 +++++++++ lib/Agda.Builtin.Reflection.html | 483 ++++++++++++++++++++++++++++++ lib/Agda.Builtin.Sigma.html | 19 ++ lib/Agda.Builtin.Strict.html | 11 + lib/Agda.Builtin.String.html | 38 +++ lib/Agda.Builtin.Unit.html | 12 + lib/Agda.Builtin.Word.html | 15 + lib/Agda.Primitive.html | 43 +++ lib/Agda.css | 42 +++ lib/Haskell.Prelude.html | 144 +++++++++ lib/Haskell.Prim.Absurd.html | 25 ++ lib/Haskell.Prim.Applicative.html | 94 ++++++ lib/Haskell.Prim.Bool.html | 26 ++ lib/Haskell.Prim.Bounded.html | 96 ++++++ lib/Haskell.Prim.Char.html | 11 + lib/Haskell.Prim.Double.html | 17 ++ lib/Haskell.Prim.Either.html | 22 ++ lib/Haskell.Prim.Enum.html | 265 ++++++++++++++++ lib/Haskell.Prim.Eq.html | 84 ++++++ lib/Haskell.Prim.Foldable.html | 124 ++++++++ lib/Haskell.Prim.Functor.html | 91 ++++++ lib/Haskell.Prim.IO.html | 29 ++ lib/Haskell.Prim.Int.html | 112 +++++++ lib/Haskell.Prim.Integer.html | 108 +++++++ lib/Haskell.Prim.List.html | 130 ++++++++ lib/Haskell.Prim.Maybe.html | 19 ++ lib/Haskell.Prim.Monad.html | 131 ++++++++ lib/Haskell.Prim.Monoid.html | 132 ++++++++ lib/Haskell.Prim.Num.html | 122 ++++++++ lib/Haskell.Prim.Ord.html | 236 +++++++++++++++ lib/Haskell.Prim.Show.html | 161 ++++++++++ lib/Haskell.Prim.String.html | 54 ++++ lib/Haskell.Prim.Traversable.html | 80 +++++ lib/Haskell.Prim.Tuple.html | 47 +++ lib/Haskell.Prim.Word.html | 56 ++++ lib/Haskell.Prim.html | 132 ++++++++ lib/index.html | 144 +++++++++ 47 files changed, 3853 insertions(+) create mode 100644 lib/Agda.Builtin.Bool.html create mode 100644 lib/Agda.Builtin.Char.html create mode 100644 lib/Agda.Builtin.Equality.html create mode 100644 lib/Agda.Builtin.Float.html create mode 100644 lib/Agda.Builtin.FromNat.html create mode 100644 lib/Agda.Builtin.FromNeg.html create mode 100644 lib/Agda.Builtin.FromString.html create mode 100644 lib/Agda.Builtin.Int.html create mode 100644 lib/Agda.Builtin.List.html create mode 100644 lib/Agda.Builtin.Maybe.html create mode 100644 lib/Agda.Builtin.Nat.html create mode 100644 lib/Agda.Builtin.Reflection.html create mode 100644 lib/Agda.Builtin.Sigma.html create mode 100644 lib/Agda.Builtin.Strict.html create mode 100644 lib/Agda.Builtin.String.html create mode 100644 lib/Agda.Builtin.Unit.html create mode 100644 lib/Agda.Builtin.Word.html create mode 100644 lib/Agda.Primitive.html create mode 100644 lib/Agda.css create mode 100644 lib/Haskell.Prelude.html create mode 100644 lib/Haskell.Prim.Absurd.html create mode 100644 lib/Haskell.Prim.Applicative.html create mode 100644 lib/Haskell.Prim.Bool.html create mode 100644 lib/Haskell.Prim.Bounded.html create mode 100644 lib/Haskell.Prim.Char.html create mode 100644 lib/Haskell.Prim.Double.html create mode 100644 lib/Haskell.Prim.Either.html create mode 100644 lib/Haskell.Prim.Enum.html create mode 100644 lib/Haskell.Prim.Eq.html create mode 100644 lib/Haskell.Prim.Foldable.html create mode 100644 lib/Haskell.Prim.Functor.html create mode 100644 lib/Haskell.Prim.IO.html create mode 100644 lib/Haskell.Prim.Int.html create mode 100644 lib/Haskell.Prim.Integer.html create mode 100644 lib/Haskell.Prim.List.html create mode 100644 lib/Haskell.Prim.Maybe.html create mode 100644 lib/Haskell.Prim.Monad.html create mode 100644 lib/Haskell.Prim.Monoid.html create mode 100644 lib/Haskell.Prim.Num.html create mode 100644 lib/Haskell.Prim.Ord.html create mode 100644 lib/Haskell.Prim.Show.html create mode 100644 lib/Haskell.Prim.String.html create mode 100644 lib/Haskell.Prim.Traversable.html create mode 100644 lib/Haskell.Prim.Tuple.html create mode 100644 lib/Haskell.Prim.Word.html create mode 100644 lib/Haskell.Prim.html create mode 100644 lib/index.html diff --git a/lib/Agda.Builtin.Bool.html b/lib/Agda.Builtin.Bool.html new file mode 100644 index 00000000..63da33b2 --- /dev/null +++ b/lib/Agda.Builtin.Bool.html @@ -0,0 +1,17 @@ + +Agda.Builtin.Bool
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
+            --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.Bool where
+
+data Bool : Set where
+  false true : Bool
+
+{-# BUILTIN BOOL  Bool  #-}
+{-# BUILTIN FALSE false #-}
+{-# BUILTIN TRUE  true  #-}
+
+{-# COMPILE JS Bool  = function (x,v) { return ((x)? v["true"]() : v["false"]()); } #-}
+{-# COMPILE JS false = false #-}
+{-# COMPILE JS true  = true  #-}
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.Char.html b/lib/Agda.Builtin.Char.html new file mode 100644 index 00000000..ec85da80 --- /dev/null +++ b/lib/Agda.Builtin.Char.html @@ -0,0 +1,20 @@ + +Agda.Builtin.Char
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
+            --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.Char where
+
+open import Agda.Builtin.Nat
+open import Agda.Builtin.Bool
+
+postulate Char : Set
+{-# BUILTIN CHAR Char #-}
+
+primitive
+  primIsLower primIsDigit primIsAlpha primIsSpace primIsAscii
+    primIsLatin1 primIsPrint primIsHexDigit : Char → Bool
+  primToUpper primToLower : Char → Char
+  primCharToNat : Char → Nat
+  primNatToChar : Nat → Char
+  primCharEquality : Char → Char → Bool
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.Equality.html b/lib/Agda.Builtin.Equality.html new file mode 100644 index 00000000..d686af44 --- /dev/null +++ b/lib/Agda.Builtin.Equality.html @@ -0,0 +1,11 @@ + +Agda.Builtin.Equality
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.Equality where
+
+infix 4 _≡_
+data _≡_ {a} {A : Set a} (x : A) : A → Set a where
+  instance refl : x ≡ x
+
+{-# BUILTIN EQUALITY _≡_ #-}
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.Float.html b/lib/Agda.Builtin.Float.html new file mode 100644 index 00000000..34c1c528 --- /dev/null +++ b/lib/Agda.Builtin.Float.html @@ -0,0 +1,211 @@ + +Agda.Builtin.Float
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.Float where
+
+open import Agda.Builtin.Bool
+open import Agda.Builtin.Int
+open import Agda.Builtin.Maybe
+open import Agda.Builtin.Nat
+open import Agda.Builtin.Sigma
+open import Agda.Builtin.String
+open import Agda.Builtin.Word
+
+postulate Float : Set
+{-# BUILTIN FLOAT Float #-}
+
+primitive
+  -- Relations
+  primFloatInequality        : Float → Float → Bool
+  primFloatEquality          : Float → Float → Bool
+  primFloatLess              : Float → Float → Bool
+  primFloatIsInfinite        : Float → Bool
+  primFloatIsNaN             : Float → Bool
+  primFloatIsNegativeZero    : Float → Bool
+  primFloatIsSafeInteger     : Float → Bool
+  -- Conversions
+  primFloatToWord64          : Float → Maybe Word64
+  primNatToFloat             : Nat → Float
+  primIntToFloat             : Int → Float
+  primFloatRound             : Float → Maybe Int
+  primFloatFloor             : Float → Maybe Int
+  primFloatCeiling           : Float → Maybe Int
+  primFloatToRatio           : Float → (Σ Int λ _ → Int)
+  primRatioToFloat           : Int → Int → Float
+  primFloatDecode            : Float → Maybe (Σ Int λ _ → Int)
+  primFloatEncode            : Int → Int → Maybe Float
+  primShowFloat              : Float → String
+  -- Operations
+  primFloatPlus              : Float → Float → Float
+  primFloatMinus             : Float → Float → Float
+  primFloatTimes             : Float → Float → Float
+  primFloatDiv               : Float → Float → Float
+  primFloatPow               : Float → Float → Float
+  primFloatNegate            : Float → Float
+  primFloatSqrt              : Float → Float
+  primFloatExp               : Float → Float
+  primFloatLog               : Float → Float
+  primFloatSin               : Float → Float
+  primFloatCos               : Float → Float
+  primFloatTan               : Float → Float
+  primFloatASin              : Float → Float
+  primFloatACos              : Float → Float
+  primFloatATan              : Float → Float
+  primFloatATan2             : Float → Float → Float
+  primFloatSinh              : Float → Float
+  primFloatCosh              : Float → Float
+  primFloatTanh              : Float → Float
+  primFloatASinh             : Float → Float
+  primFloatACosh             : Float → Float
+  primFloatATanh             : Float → Float
+
+{-# COMPILE JS
+    primFloatRound = function(x) {
+        x = agdaRTS._primFloatRound(x);
+        if (x === null) {
+            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
+        }
+        else {
+            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
+        }
+    };
+#-}
+{-# COMPILE JS
+    primFloatFloor = function(x) {
+        x = agdaRTS._primFloatFloor(x);
+        if (x === null) {
+            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
+        }
+        else {
+            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
+        }
+    };
+#-}
+{-# COMPILE JS
+    primFloatCeiling = function(x) {
+        x = agdaRTS._primFloatCeiling(x);
+        if (x === null) {
+            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
+        }
+        else {
+            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
+        }
+    };
+#-}
+{-# COMPILE JS
+    primFloatToRatio = function(x) {
+        x = agdaRTS._primFloatToRatio(x);
+        return z_jAgda_Agda_Builtin_Sigma["_,_"](x.numerator)(x.denominator);
+    };
+#-}
+{-# COMPILE JS
+    primFloatDecode = function(x) {
+        x = agdaRTS._primFloatDecode(x);
+        if (x === null) {
+            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
+        }
+        else {
+            return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](
+                z_jAgda_Agda_Builtin_Sigma["_,_"](x.mantissa)(x.exponent));
+        }
+    };
+#-}
+{-# COMPILE JS
+    primFloatEncode = function(x) {
+        return function (y) {
+            x = agdaRTS.uprimFloatEncode(x, y);
+            if (x === null) {
+                return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"];
+            }
+            else {
+                return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](x);
+            }
+        }
+    };
+#-}
+
+primFloatNumericalEquality = primFloatEquality
+{-# WARNING_ON_USAGE primFloatNumericalEquality
+"Warning: primFloatNumericalEquality was deprecated in Agda v2.6.2.
+Please use primFloatEquality instead."
+#-}
+
+primFloatNumericalLess = primFloatLess
+{-# WARNING_ON_USAGE primFloatNumericalLess
+"Warning: primFloatNumericalLess was deprecated in Agda v2.6.2.
+Please use primFloatLess instead."
+#-}
+
+primRound = primFloatRound
+{-# WARNING_ON_USAGE primRound
+"Warning: primRound was deprecated in Agda v2.6.2.
+Please use primFloatRound instead."
+#-}
+
+primFloor = primFloatFloor
+{-# WARNING_ON_USAGE primFloor
+"Warning: primFloor was deprecated in Agda v2.6.2.
+Please use primFloatFloor instead."
+#-}
+
+primCeiling = primFloatCeiling
+{-# WARNING_ON_USAGE primCeiling
+"Warning: primCeiling was deprecated in Agda v2.6.2.
+Please use primFloatCeiling instead."
+#-}
+
+primExp = primFloatExp
+{-# WARNING_ON_USAGE primExp
+"Warning: primExp was deprecated in Agda v2.6.2.
+Please use primFloatExp instead."
+#-}
+
+primLog = primFloatLog
+{-# WARNING_ON_USAGE primLog
+"Warning: primLog was deprecated in Agda v2.6.2.
+Please use primFloatLog instead."
+#-}
+
+primSin = primFloatSin
+{-# WARNING_ON_USAGE primSin
+"Warning: primSin was deprecated in Agda v2.6.2.
+Please use primFloatSin instead."
+#-}
+
+primCos = primFloatCos
+{-# WARNING_ON_USAGE primCos
+"Warning: primCos was deprecated in Agda v2.6.2.
+Please use primFloatCos instead."
+#-}
+
+primTan = primFloatTan
+{-# WARNING_ON_USAGE primTan
+"Warning: primTan was deprecated in Agda v2.6.2.
+Please use primFloatTan instead."
+#-}
+
+primASin = primFloatASin
+{-# WARNING_ON_USAGE primASin
+"Warning: primASin was deprecated in Agda v2.6.2.
+Please use primFloatASin instead."
+#-}
+
+
+primACos = primFloatACos
+{-# WARNING_ON_USAGE primACos
+"Warning: primACos was deprecated in Agda v2.6.2.
+Please use primFloatACos instead."
+#-}
+
+primATan = primFloatATan
+{-# WARNING_ON_USAGE primATan
+"Warning: primATan was deprecated in Agda v2.6.2.
+Please use primFloatATan instead."
+#-}
+
+primATan2 = primFloatATan2
+{-# WARNING_ON_USAGE primATan2
+"Warning: primATan2 was deprecated in Agda v2.6.2.
+Please use primFloatATan2 instead."
+#-}
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.FromNat.html b/lib/Agda.Builtin.FromNat.html new file mode 100644 index 00000000..acfa25ae --- /dev/null +++ b/lib/Agda.Builtin.FromNat.html @@ -0,0 +1,18 @@ + +Agda.Builtin.FromNat
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.FromNat where
+
+open import Agda.Primitive
+open import Agda.Builtin.Nat
+
+record Number {a} (A : Set a) : Set (lsuc a) where
+  field
+    Constraint : Nat → Set a
+    fromNat : ∀ n → {{_ : Constraint n}} → A
+
+open Number {{...}} public using (fromNat)
+
+{-# BUILTIN FROMNAT fromNat #-}
+{-# DISPLAY Number.fromNat _ n = fromNat n #-}
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.FromNeg.html b/lib/Agda.Builtin.FromNeg.html new file mode 100644 index 00000000..6253b020 --- /dev/null +++ b/lib/Agda.Builtin.FromNeg.html @@ -0,0 +1,18 @@ + +Agda.Builtin.FromNeg
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.FromNeg where
+
+open import Agda.Primitive
+open import Agda.Builtin.Nat
+
+record Negative {a} (A : Set a) : Set (lsuc a) where
+  field
+    Constraint : Nat → Set a
+    fromNeg : ∀ n → {{_ : Constraint n}} → A
+
+open Negative {{...}} public using (fromNeg)
+
+{-# BUILTIN FROMNEG fromNeg #-}
+{-# DISPLAY Negative.fromNeg _ n = fromNeg n #-}
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.FromString.html b/lib/Agda.Builtin.FromString.html new file mode 100644 index 00000000..0b9dffdc --- /dev/null +++ b/lib/Agda.Builtin.FromString.html @@ -0,0 +1,18 @@ + +Agda.Builtin.FromString
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.FromString where
+
+open import Agda.Primitive
+open import Agda.Builtin.String
+
+record IsString {a} (A : Set a) : Set (lsuc a) where
+  field
+    Constraint : String → Set a
+    fromString : (s : String) {{_ : Constraint s}} → A
+
+open IsString {{...}} public using (fromString)
+
+{-# BUILTIN FROMSTRING fromString #-}
+{-# DISPLAY IsString.fromString _ s = fromString s #-}
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.Int.html b/lib/Agda.Builtin.Int.html new file mode 100644 index 00000000..775af21f --- /dev/null +++ b/lib/Agda.Builtin.Int.html @@ -0,0 +1,20 @@ + +Agda.Builtin.Int
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.Int where
+
+open import Agda.Builtin.Nat
+open import Agda.Builtin.String
+
+infix 8 pos  -- Standard library uses this as +_
+
+data Int : Set where
+  pos    : (n : Nat) → Int
+  negsuc : (n : Nat) → Int
+
+{-# BUILTIN INTEGER       Int    #-}
+{-# BUILTIN INTEGERPOS    pos    #-}
+{-# BUILTIN INTEGERNEGSUC negsuc #-}
+
+primitive primShowInteger : Int → String
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.List.html b/lib/Agda.Builtin.List.html new file mode 100644 index 00000000..add6de61 --- /dev/null +++ b/lib/Agda.Builtin.List.html @@ -0,0 +1,18 @@ + +Agda.Builtin.List
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.List where
+
+infixr 5 _∷_
+data List {a} (A : Set a) : Set a where
+  []  : List A
+  _∷_ : (x : A) (xs : List A) → List A
+
+{-# BUILTIN LIST List #-}
+
+{-# COMPILE JS  List = function(x,v) {
+  if (x.length < 1) { return v["[]"](); } else { return v["_∷_"](x[0], x.slice(1)); }
+} #-}
+{-# COMPILE JS [] = Array() #-}
+{-# COMPILE JS _∷_ = function (x) { return function(y) { return Array(x).concat(y); }; } #-}
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.Maybe.html b/lib/Agda.Builtin.Maybe.html new file mode 100644 index 00000000..76d37bd3 --- /dev/null +++ b/lib/Agda.Builtin.Maybe.html @@ -0,0 +1,11 @@ + +Agda.Builtin.Maybe
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.Maybe where
+
+data Maybe {a} (A : Set a) : Set a where
+  just : A → Maybe A
+  nothing : Maybe A
+
+{-# BUILTIN MAYBE Maybe #-}
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.Nat.html b/lib/Agda.Builtin.Nat.html new file mode 100644 index 00000000..6ccb7bda --- /dev/null +++ b/lib/Agda.Builtin.Nat.html @@ -0,0 +1,136 @@ + +Agda.Builtin.Nat
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
+            --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.Nat where
+
+open import Agda.Builtin.Bool
+
+data Nat : Set where
+  zero : Nat
+  suc  : (n : Nat) → Nat
+
+{-# BUILTIN NATURAL Nat #-}
+
+infix  4 _==_ _<_
+infixl 6 _+_ _-_
+infixl 7 _*_
+
+_+_ : Nat → Nat → Nat
+zero  + m = m
+suc n + m = suc (n + m)
+
+{-# BUILTIN NATPLUS _+_ #-}
+
+_-_ : Nat → Nat → Nat
+n     - zero = n
+zero  - suc m = zero
+suc n - suc m = n - m
+
+{-# BUILTIN NATMINUS _-_ #-}
+
+_*_ : Nat → Nat → Nat
+zero  * m = zero
+suc n * m = m + n * m
+
+{-# BUILTIN NATTIMES _*_ #-}
+
+_==_ : Nat → Nat → Bool
+zero  == zero  = true
+suc n == suc m = n == m
+_     == _     = false
+
+{-# BUILTIN NATEQUALS _==_ #-}
+
+_<_ : Nat → Nat → Bool
+_     < zero  = false
+zero  < suc _ = true
+suc n < suc m = n < m
+
+{-# BUILTIN NATLESS _<_ #-}
+
+-- Helper function  div-helper  for Euclidean division.
+---------------------------------------------------------------------------
+--
+-- div-helper computes n / 1+m via iteration on n.
+--
+--   n div (suc m) = div-helper 0 m n m
+--
+-- The state of the iterator has two accumulator variables:
+--
+--   k: The quotient, returned once n=0.  Initialized to 0.
+--
+--   j: A counter, initialized to the divisor m, decreased on each iteration step.
+--      Once it reaches 0, the quotient k is increased and j reset to m,
+--      starting the next countdown.
+--
+-- Under the precondition j ≤ m, the invariant is
+--
+--   div-helper k m n j = k + (n + m - j) div (1 + m)
+
+div-helper : (k m n j : Nat) → Nat
+div-helper k m  zero    j      = k
+div-helper k m (suc n)  zero   = div-helper (suc k) m n m
+div-helper k m (suc n) (suc j) = div-helper k       m n j
+
+{-# BUILTIN NATDIVSUCAUX div-helper #-}
+
+-- Proof of the invariant by induction on n.
+--
+--   clause 1: div-helper k m 0 j
+--           = k                                        by definition
+--           = k + (0 + m - j) div (1 + m)              since m - j < 1 + m
+--
+--   clause 2: div-helper k m (1 + n) 0
+--           = div-helper (1 + k) m n m                 by definition
+--           = 1 + k + (n + m - m) div (1 + m)          by induction hypothesis
+--           = 1 + k +          n  div (1 + m)          by simplification
+--           = k +   (n + (1 + m)) div (1 + m)          by expansion
+--           = k + (1 + n + m - 0) div (1 + m)          by expansion
+--
+--   clause 3: div-helper k m (1 + n) (1 + j)
+--           = div-helper k m n j                       by definition
+--           = k + (n + m - j) div (1 + m)              by induction hypothesis
+--           = k + ((1 + n) + m - (1 + j)) div (1 + m)  by expansion
+--
+-- Q.e.d.
+
+-- Helper function  mod-helper  for the remainder computation.
+---------------------------------------------------------------------------
+--
+-- (Analogous to div-helper.)
+--
+-- mod-helper computes n % 1+m via iteration on n.
+--
+--   n mod (suc m) = mod-helper 0 m n m
+--
+-- The invariant is:
+--
+--   m = k + j  ==>  mod-helper k m n j = (n + k) mod (1 + m).
+
+mod-helper : (k m n j : Nat) → Nat
+mod-helper k m  zero    j      = k
+mod-helper k m (suc n)  zero   = mod-helper 0       m n m
+mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j
+
+{-# BUILTIN NATMODSUCAUX mod-helper #-}
+
+-- Proof of the invariant by induction on n.
+--
+--   clause 1: mod-helper k m 0 j
+--           = k                               by definition
+--           = (0 + k) mod (1 + m)             since m = k + j, thus k < m
+--
+--   clause 2: mod-helper k m (1 + n) 0
+--           = mod-helper 0 m n m              by definition
+--           = (n + 0)       mod (1 + m)       by induction hypothesis
+--           = (n + (1 + m)) mod (1 + m)       by expansion
+--           = (1 + n) + k)  mod (1 + m)       since k = m (as l = 0)
+--
+--   clause 3: mod-helper k m (1 + n) (1 + j)
+--           = mod-helper (1 + k) m n j        by definition
+--           = (n + (1 + k)) mod (1 + m)       by induction hypothesis
+--           = ((1 + n) + k) mod (1 + m)       by commutativity
+--
+-- Q.e.d.
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.Reflection.html b/lib/Agda.Builtin.Reflection.html new file mode 100644 index 00000000..e0edde26 --- /dev/null +++ b/lib/Agda.Builtin.Reflection.html @@ -0,0 +1,483 @@ + +Agda.Builtin.Reflection
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.Reflection where
+
+open import Agda.Builtin.Unit
+open import Agda.Builtin.Bool
+open import Agda.Builtin.Nat
+open import Agda.Builtin.Word
+open import Agda.Builtin.List
+open import Agda.Builtin.String
+open import Agda.Builtin.Char
+open import Agda.Builtin.Float
+open import Agda.Builtin.Int
+open import Agda.Builtin.Sigma
+open import Agda.Primitive
+
+-- Names --
+
+postulate Name : Set
+{-# BUILTIN QNAME Name #-}
+
+primitive
+  primQNameEquality : Name → Name → Bool
+  primQNameLess     : Name → Name → Bool
+  primShowQName     : Name → String
+
+-- Fixity --
+
+data Associativity : Set where
+  left-assoc  : Associativity
+  right-assoc : Associativity
+  non-assoc   : Associativity
+
+data Precedence : Set where
+  related   : Float → Precedence
+  unrelated : Precedence
+
+data Fixity : Set where
+  fixity : Associativity → Precedence → Fixity
+
+{-# BUILTIN ASSOC      Associativity #-}
+{-# BUILTIN ASSOCLEFT  left-assoc    #-}
+{-# BUILTIN ASSOCRIGHT right-assoc   #-}
+{-# BUILTIN ASSOCNON   non-assoc     #-}
+
+{-# BUILTIN PRECEDENCE    Precedence #-}
+{-# BUILTIN PRECRELATED   related    #-}
+{-# BUILTIN PRECUNRELATED unrelated  #-}
+
+{-# BUILTIN FIXITY       Fixity #-}
+{-# BUILTIN FIXITYFIXITY fixity #-}
+
+{-# COMPILE GHC Associativity = data MAlonzo.RTE.Assoc (MAlonzo.RTE.LeftAssoc | MAlonzo.RTE.RightAssoc | MAlonzo.RTE.NonAssoc) #-}
+{-# COMPILE GHC Precedence    = data MAlonzo.RTE.Precedence (MAlonzo.RTE.Related | MAlonzo.RTE.Unrelated) #-}
+{-# COMPILE GHC Fixity        = data MAlonzo.RTE.Fixity (MAlonzo.RTE.Fixity) #-}
+
+{-# COMPILE JS Associativity  = function (x,v) { return v[x](); } #-}
+{-# COMPILE JS left-assoc     = "left-assoc"  #-}
+{-# COMPILE JS right-assoc    = "right-assoc" #-}
+{-# COMPILE JS non-assoc      = "non-assoc"   #-}
+
+{-# COMPILE JS Precedence     =
+  function (x,v) {
+    if (x === "unrelated") { return v[x](); } else { return v["related"](x); }} #-}
+{-# COMPILE JS related        = function(x) { return x; } #-}
+{-# COMPILE JS unrelated      = "unrelated"               #-}
+
+{-# COMPILE JS Fixity         = function (x,v) { return v["fixity"](x["assoc"], x["prec"]); } #-}
+{-# COMPILE JS fixity         = function (x) { return function (y) { return { "assoc": x, "prec": y}; }; } #-}
+
+primitive
+  primQNameFixity : Name → Fixity
+  primQNameToWord64s : Name → Σ Word64 (λ _ → Word64)
+
+-- Metavariables --
+
+postulate Meta : Set
+{-# BUILTIN AGDAMETA Meta #-}
+
+primitive
+  primMetaEquality : Meta → Meta → Bool
+  primMetaLess     : Meta → Meta → Bool
+  primShowMeta     : Meta → String
+  primMetaToNat    : Meta → Nat
+
+-- Arguments --
+
+-- Arguments can be (visible), {hidden}, or {{instance}}.
+data Visibility : Set where
+  visible hidden instance′ : Visibility
+
+{-# BUILTIN HIDING   Visibility #-}
+{-# BUILTIN VISIBLE  visible    #-}
+{-# BUILTIN HIDDEN   hidden     #-}
+{-# BUILTIN INSTANCE instance′  #-}
+
+-- Arguments can be relevant or irrelevant.
+data Relevance : Set where
+  relevant irrelevant : Relevance
+
+{-# BUILTIN RELEVANCE  Relevance  #-}
+{-# BUILTIN RELEVANT   relevant   #-}
+{-# BUILTIN IRRELEVANT irrelevant #-}
+
+-- Arguments also have a quantity.
+data Quantity : Set where
+  quantity-0 quantity-ω : Quantity
+
+{-# BUILTIN QUANTITY   Quantity   #-}
+{-# BUILTIN QUANTITY-0 quantity-0 #-}
+{-# BUILTIN QUANTITY-ω quantity-ω #-}
+
+-- Relevance and quantity are combined into a modality.
+data Modality : Set where
+  modality : (r : Relevance) (q : Quantity) → Modality
+
+{-# BUILTIN MODALITY             Modality #-}
+{-# BUILTIN MODALITY-CONSTRUCTOR modality #-}
+
+data ArgInfo : Set where
+  arg-info : (v : Visibility) (m : Modality) → ArgInfo
+
+data Arg {a} (A : Set a) : Set a where
+  arg : (i : ArgInfo) (x : A) → Arg A
+
+{-# BUILTIN ARGINFO    ArgInfo  #-}
+{-# BUILTIN ARGARGINFO arg-info #-}
+{-# BUILTIN ARG        Arg      #-}
+{-# BUILTIN ARGARG     arg      #-}
+
+data Blocker : Set where
+  blockerAny  : List Blocker → Blocker
+  blockerAll  : List Blocker → Blocker
+  blockerMeta : Meta → Blocker
+
+{-# BUILTIN AGDABLOCKER     Blocker #-}
+{-# BUILTIN AGDABLOCKERANY  blockerAny #-}
+{-# BUILTIN AGDABLOCKERALL  blockerAll #-}
+{-# BUILTIN AGDABLOCKERMETA blockerMeta #-}
+
+-- Name abstraction --
+
+data Abs {a} (A : Set a) : Set a where
+  abs : (s : String) (x : A) → Abs A
+
+{-# BUILTIN ABS    Abs #-}
+{-# BUILTIN ABSABS abs #-}
+
+-- Literals --
+
+data Literal : Set where
+  nat    : (n : Nat)    → Literal
+  word64 : (n : Word64) → Literal
+  float  : (x : Float)  → Literal
+  char   : (c : Char)   → Literal
+  string : (s : String) → Literal
+  name   : (x : Name)   → Literal
+  meta   : (x : Meta)   → Literal
+
+{-# BUILTIN AGDALITERAL   Literal #-}
+{-# BUILTIN AGDALITNAT    nat     #-}
+{-# BUILTIN AGDALITWORD64 word64  #-}
+{-# BUILTIN AGDALITFLOAT  float   #-}
+{-# BUILTIN AGDALITCHAR   char    #-}
+{-# BUILTIN AGDALITSTRING string  #-}
+{-# BUILTIN AGDALITQNAME  name    #-}
+{-# BUILTIN AGDALITMETA   meta    #-}
+
+
+-- Terms and patterns --
+
+data Term    : Set
+data Sort    : Set
+data Pattern : Set
+data Clause  : Set
+Type = Term
+Telescope = List (Σ String λ _ → Arg Type)
+
+data Term where
+  var       : (x : Nat) (args : List (Arg Term)) → Term
+  con       : (c : Name) (args : List (Arg Term)) → Term
+  def       : (f : Name) (args : List (Arg Term)) → Term
+  lam       : (v : Visibility) (t : Abs Term) → Term
+  pat-lam   : (cs : List Clause) (args : List (Arg Term)) → Term
+  pi        : (a : Arg Type) (b : Abs Type) → Term
+  agda-sort : (s : Sort) → Term
+  lit       : (l : Literal) → Term
+  meta      : (x : Meta) → List (Arg Term) → Term
+  unknown   : Term
+
+data Sort where
+  set     : (t : Term) → Sort
+  lit     : (n : Nat) → Sort
+  prop    : (t : Term) → Sort
+  propLit : (n : Nat) → Sort
+  inf     : (n : Nat) → Sort
+  unknown : Sort
+
+data Pattern where
+  con    : (c : Name) (ps : List (Arg Pattern)) → Pattern
+  dot    : (t : Term)    → Pattern
+  var    : (x : Nat)     → Pattern
+  lit    : (l : Literal) → Pattern
+  proj   : (f : Name)    → Pattern
+  absurd : (x : Nat)     → Pattern  -- absurd patterns counts as variables
+
+data Clause where
+  clause        : (tel : Telescope) (ps : List (Arg Pattern)) (t : Term) → Clause
+  absurd-clause : (tel : Telescope) (ps : List (Arg Pattern)) → Clause
+
+{-# BUILTIN AGDATERM      Term    #-}
+{-# BUILTIN AGDASORT      Sort    #-}
+{-# BUILTIN AGDAPATTERN   Pattern #-}
+{-# BUILTIN AGDACLAUSE    Clause  #-}
+
+{-# BUILTIN AGDATERMVAR         var       #-}
+{-# BUILTIN AGDATERMCON         con       #-}
+{-# BUILTIN AGDATERMDEF         def       #-}
+{-# BUILTIN AGDATERMMETA        meta      #-}
+{-# BUILTIN AGDATERMLAM         lam       #-}
+{-# BUILTIN AGDATERMEXTLAM      pat-lam   #-}
+{-# BUILTIN AGDATERMPI          pi        #-}
+{-# BUILTIN AGDATERMSORT        agda-sort #-}
+{-# BUILTIN AGDATERMLIT         lit       #-}
+{-# BUILTIN AGDATERMUNSUPPORTED unknown   #-}
+
+{-# BUILTIN AGDASORTSET         set     #-}
+{-# BUILTIN AGDASORTLIT         lit     #-}
+{-# BUILTIN AGDASORTPROP        prop    #-}
+{-# BUILTIN AGDASORTPROPLIT     propLit #-}
+{-# BUILTIN AGDASORTINF         inf     #-}
+{-# BUILTIN AGDASORTUNSUPPORTED unknown #-}
+
+{-# BUILTIN AGDAPATCON    con     #-}
+{-# BUILTIN AGDAPATDOT    dot     #-}
+{-# BUILTIN AGDAPATVAR    var     #-}
+{-# BUILTIN AGDAPATLIT    lit     #-}
+{-# BUILTIN AGDAPATPROJ   proj    #-}
+{-# BUILTIN AGDAPATABSURD absurd  #-}
+
+{-# BUILTIN AGDACLAUSECLAUSE clause        #-}
+{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}
+
+-- Definitions --
+
+data Definition : Set where
+  function    : (cs : List Clause) → Definition
+  data-type   : (pars : Nat) (cs : List Name) → Definition
+  record-type : (c : Name) (fs : List (Arg Name)) → Definition
+  data-cons   : (d : Name) (q : Quantity) → Definition
+  axiom       : Definition
+  prim-fun    : Definition
+
+{-# BUILTIN AGDADEFINITION                Definition  #-}
+{-# BUILTIN AGDADEFINITIONFUNDEF          function    #-}
+{-# BUILTIN AGDADEFINITIONDATADEF         data-type   #-}
+{-# BUILTIN AGDADEFINITIONRECORDDEF       record-type #-}
+{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR data-cons   #-}
+{-# BUILTIN AGDADEFINITIONPOSTULATE       axiom       #-}
+{-# BUILTIN AGDADEFINITIONPRIMITIVE       prim-fun    #-}
+
+-- Errors --
+
+data ErrorPart : Set where
+  strErr  : String → ErrorPart
+  termErr : Term → ErrorPart
+  pattErr : Pattern → ErrorPart
+  nameErr : Name → ErrorPart
+
+{-# BUILTIN AGDAERRORPART       ErrorPart #-}
+{-# BUILTIN AGDAERRORPARTSTRING strErr    #-}
+{-# BUILTIN AGDAERRORPARTTERM   termErr   #-}
+{-# BUILTIN AGDAERRORPARTPATT   pattErr   #-}
+{-# BUILTIN AGDAERRORPARTNAME   nameErr   #-}
+
+-- TC monad --
+
+postulate
+  TC               : ∀ {a} → Set a → Set a
+  returnTC         : ∀ {a} {A : Set a} → A → TC A
+  bindTC           : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
+  unify            : Term → Term → TC ⊤
+  typeError        : ∀ {a} {A : Set a} → List ErrorPart → TC A
+  inferType        : Term → TC Type
+  checkType        : Term → Type → TC Term
+  normalise        : Term → TC Term
+  reduce           : Term → TC Term
+  catchTC          : ∀ {a} {A : Set a} → TC A → TC A → TC A
+  quoteTC          : ∀ {a} {A : Set a} → A → TC Term
+  unquoteTC        : ∀ {a} {A : Set a} → Term → TC A
+  quoteωTC         : ∀ {A : Setω} → A → TC Term
+  getContext       : TC Telescope
+  extendContext    : ∀ {a} {A : Set a} → String → Arg Type → TC A → TC A
+  inContext        : ∀ {a} {A : Set a} → Telescope → TC A → TC A
+  freshName        : String → TC Name
+  declareDef       : Arg Name → Type → TC ⊤
+  declarePostulate : Arg Name → Type → TC ⊤
+  declareData      : Name → Nat → Type → TC ⊤
+  defineData       : Name → List (Σ Name (λ _ → Σ Quantity (λ _ → Type))) → TC ⊤
+  defineFun        : Name → List Clause → TC ⊤
+  getType          : Name → TC Type
+  getDefinition    : Name → TC Definition
+  blockTC          : ∀ {a} {A : Set a} → Blocker → TC A
+  commitTC         : TC ⊤
+  isMacro          : Name → TC Bool
+  pragmaForeign    : String → String → TC ⊤
+  pragmaCompile    : String → Name → String → TC ⊤
+
+  -- If 'true', makes the following primitives also normalise
+  -- their results: inferType, checkType, quoteTC, getType, and getContext
+  withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A
+  askNormalisation  : TC Bool
+
+  -- If 'true', makes the following primitives to reconstruct hidden arguments:
+  -- getDefinition, normalise, reduce, inferType, checkType and getContext
+  withReconstructed : ∀ {a} {A : Set a} → Bool → TC A → TC A
+  askReconstructed  : TC Bool
+
+  -- Whether implicit arguments at the end should be turned into metavariables
+  withExpandLast : ∀ {a} {A : Set a} → Bool → TC A → TC A
+  askExpandLast  : TC Bool
+
+  -- White/blacklist specific definitions for reduction while executing the TC computation
+  -- 'true' for whitelist, 'false' for blacklist
+  withReduceDefs : ∀ {a} {A : Set a} → (Σ Bool λ _ → List Name) → TC A → TC A
+  askReduceDefs  : TC (Σ Bool λ _ → List Name)
+
+  formatErrorParts : List ErrorPart → TC String
+  -- Prints the third argument if the corresponding verbosity level is turned
+  -- on (with the -v flag to Agda).
+  debugPrint : String → Nat → List ErrorPart → TC ⊤
+
+  -- Fail if the given computation gives rise to new, unsolved
+  -- "blocking" constraints.
+  noConstraints : ∀ {a} {A : Set a} → TC A → TC A
+
+  -- Run the given computation at the type level, allowing use of erased things.
+  workOnTypes : ∀ {a} {A : Set a} → TC A → TC A
+
+  -- Run the given TC action and return the first component. Resets to
+  -- the old TC state if the second component is 'false', or keep the
+  -- new TC state if it is 'true'.
+  runSpeculative : ∀ {a} {A : Set a} → TC (Σ A λ _ → Bool) → TC A
+
+  -- Get a list of all possible instance candidates for the given meta
+  -- variable (it does not have to be an instance meta).
+  getInstances : Meta → TC (List Term)
+
+  -- Try to solve open instance constraints. When wrapped in `noConstraints`,
+  -- fails if there are unsolved instance constraints left over that originate
+  -- from the current macro invokation. Outside constraints are still attempted,
+  -- but failure to solve them are ignored by `noConstraints`.
+  solveInstanceConstraints : TC ⊤
+
+{-# BUILTIN AGDATCM                           TC                         #-}
+{-# BUILTIN AGDATCMRETURN                     returnTC                   #-}
+{-# BUILTIN AGDATCMBIND                       bindTC                     #-}
+{-# BUILTIN AGDATCMUNIFY                      unify                      #-}
+{-# BUILTIN AGDATCMTYPEERROR                  typeError                  #-}
+{-# BUILTIN AGDATCMINFERTYPE                  inferType                  #-}
+{-# BUILTIN AGDATCMCHECKTYPE                  checkType                  #-}
+{-# BUILTIN AGDATCMNORMALISE                  normalise                  #-}
+{-# BUILTIN AGDATCMREDUCE                     reduce                     #-}
+{-# BUILTIN AGDATCMCATCHERROR                 catchTC                    #-}
+{-# BUILTIN AGDATCMQUOTETERM                  quoteTC                    #-}
+{-# BUILTIN AGDATCMUNQUOTETERM                unquoteTC                  #-}
+{-# BUILTIN AGDATCMQUOTEOMEGATERM             quoteωTC                   #-}
+{-# BUILTIN AGDATCMGETCONTEXT                 getContext                 #-}
+{-# BUILTIN AGDATCMEXTENDCONTEXT              extendContext              #-}
+{-# BUILTIN AGDATCMINCONTEXT                  inContext                  #-}
+{-# BUILTIN AGDATCMFRESHNAME                  freshName                  #-}
+{-# BUILTIN AGDATCMDECLAREDEF                 declareDef                 #-}
+{-# BUILTIN AGDATCMDECLAREPOSTULATE           declarePostulate           #-}
+{-# BUILTIN AGDATCMDECLAREDATA                declareData                #-}
+{-# BUILTIN AGDATCMDEFINEDATA                 defineData                 #-}
+{-# BUILTIN AGDATCMDEFINEFUN                  defineFun                  #-}
+{-# BUILTIN AGDATCMGETTYPE                    getType                    #-}
+{-# BUILTIN AGDATCMGETDEFINITION              getDefinition              #-}
+{-# BUILTIN AGDATCMBLOCK                      blockTC                    #-}
+{-# BUILTIN AGDATCMCOMMIT                     commitTC                   #-}
+{-# BUILTIN AGDATCMISMACRO                    isMacro                    #-}
+{-# BUILTIN AGDATCMPRAGMAFOREIGN              pragmaForeign              #-}
+{-# BUILTIN AGDATCMPRAGMACOMPILE              pragmaCompile              #-}
+{-# BUILTIN AGDATCMWITHNORMALISATION          withNormalisation          #-}
+{-# BUILTIN AGDATCMWITHRECONSTRUCTED          withReconstructed          #-}
+{-# BUILTIN AGDATCMWITHEXPANDLAST             withExpandLast             #-}
+{-# BUILTIN AGDATCMWITHREDUCEDEFS             withReduceDefs             #-}
+{-# BUILTIN AGDATCMASKNORMALISATION           askNormalisation           #-}
+{-# BUILTIN AGDATCMASKRECONSTRUCTED           askReconstructed           #-}
+{-# BUILTIN AGDATCMASKEXPANDLAST              askExpandLast              #-}
+{-# BUILTIN AGDATCMASKREDUCEDEFS              askReduceDefs              #-}
+{-# BUILTIN AGDATCMFORMATERRORPARTS           formatErrorParts           #-}
+{-# BUILTIN AGDATCMDEBUGPRINT                 debugPrint                 #-}
+{-# BUILTIN AGDATCMNOCONSTRAINTS              noConstraints              #-}
+{-# BUILTIN AGDATCMWORKONTYPES                workOnTypes                #-}
+{-# BUILTIN AGDATCMRUNSPECULATIVE             runSpeculative             #-}
+{-# BUILTIN AGDATCMGETINSTANCES               getInstances               #-}
+{-# BUILTIN AGDATCMSOLVEINSTANCES             solveInstanceConstraints   #-}
+
+-- All the TC primitives are compiled to functions that return
+-- undefined, rather than just undefined, in an attempt to make sure
+-- that code will run properly.
+{-# COMPILE JS returnTC          = _ => _ => _ =>      undefined #-}
+{-# COMPILE JS bindTC            = _ => _ => _ => _ =>
+                                   _ => _ =>           undefined #-}
+{-# COMPILE JS unify             = _ => _ =>           undefined #-}
+{-# COMPILE JS typeError         = _ => _ => _ =>      undefined #-}
+{-# COMPILE JS inferType         = _ =>                undefined #-}
+{-# COMPILE JS checkType         = _ => _ =>           undefined #-}
+{-# COMPILE JS normalise         = _ =>                undefined #-}
+{-# COMPILE JS reduce            = _ =>                undefined #-}
+{-# COMPILE JS catchTC           = _ => _ => _ => _ => undefined #-}
+{-# COMPILE JS quoteTC           = _ => _ => _ =>      undefined #-}
+{-# COMPILE JS unquoteTC         = _ => _ => _ =>      undefined #-}
+{-# COMPILE JS quoteωTC          = _ => _ =>           undefined #-}
+{-# COMPILE JS getContext        =                     undefined #-}
+{-# COMPILE JS extendContext     = _ => _ => _ => _ => _ => undefined #-}
+{-# COMPILE JS inContext         = _ => _ => _ => _ => undefined #-}
+{-# COMPILE JS freshName         = _ =>                undefined #-}
+{-# COMPILE JS declareDef        = _ => _ =>           undefined #-}
+{-# COMPILE JS declarePostulate  = _ => _ =>           undefined #-}
+{-# COMPILE JS declareData       = _ => _ => _ =>      undefined #-}
+{-# COMPILE JS defineData        = _ => _ =>           undefined #-}
+{-# COMPILE JS defineFun         = _ => _ =>           undefined #-}
+{-# COMPILE JS getType           = _ =>                undefined #-}
+{-# COMPILE JS getDefinition     = _ =>                undefined #-}
+{-# COMPILE JS blockTC           = _ => _ =>           undefined #-}
+{-# COMPILE JS commitTC          =                     undefined #-}
+{-# COMPILE JS isMacro           = _ =>                undefined #-}
+{-# COMPILE JS pragmaForeign     = _ => _ =>           undefined #-}
+{-# COMPILE JS pragmaCompile     = _ => _ => _ =>      undefined #-}
+{-# COMPILE JS withNormalisation = _ => _ => _ => _ => undefined #-}
+{-# COMPILE JS withReconstructed = _ => _ => _ => _ => undefined #-}
+{-# COMPILE JS withExpandLast    = _ => _ => _ => _ => undefined #-}
+{-# COMPILE JS withReduceDefs    = _ => _ => _ => _ => undefined #-}
+{-# COMPILE JS askNormalisation  =                     undefined #-}
+{-# COMPILE JS askReconstructed  =                     undefined #-}
+{-# COMPILE JS askExpandLast     =                     undefined #-}
+{-# COMPILE JS askReduceDefs     =                     undefined #-}
+{-# COMPILE JS debugPrint        = _ => _ => _ =>      undefined #-}
+{-# COMPILE JS noConstraints     = _ => _ => _ =>      undefined #-}
+{-# COMPILE JS runSpeculative    = _ => _ => _ =>      undefined #-}
+{-# COMPILE JS getInstances      = _ =>                undefined #-}
+
+private
+  filter : (Name → Bool) → List Name → List Name
+  filter p [] = []
+  filter p (x ∷ xs) with p x
+  ... | true  = x ∷ filter p xs
+  ... | false = filter p xs
+
+  _∈_ : Name → List Name → Bool
+  n ∈ []      = false
+  n ∈ (n' ∷ l) with primQNameEquality n n'
+  ... | true  = true
+  ... | false = n ∈ l
+
+  _∉_ : Name → List Name → Bool
+  n ∉ l with n ∈ l
+  ... | true  = false
+  ... | false = true
+
+  _++_ : List Name → List Name → List Name
+  [] ++ l       = l
+  (x ∷ xs) ++ l = x ∷ (xs ++ l)
+
+  combineReduceDefs : (Σ Bool λ _ → List Name) → (Σ Bool λ _ → List Name) → (Σ Bool λ _ → List Name)
+  combineReduceDefs (true  , defs₁) (true  , defs₂) = (true  , filter (_∈ defs₁) defs₂)
+  combineReduceDefs (false , defs₁) (true  , defs₂) = (true  , filter (_∉ defs₁) defs₂)
+  combineReduceDefs (true  , defs₁) (false , defs₂) = (true  , filter (_∉ defs₂) defs₁)
+  combineReduceDefs (false , defs₁) (false , defs₂) = (false , defs₁ ++ defs₂)
+
+onlyReduceDefs dontReduceDefs : ∀ {a} {A : Set a} → List Name → TC A → TC A
+onlyReduceDefs defs x = bindTC askReduceDefs (λ exDefs → withReduceDefs (combineReduceDefs (true  , defs) exDefs) x)
+dontReduceDefs defs x = bindTC askReduceDefs (λ exDefs → withReduceDefs (combineReduceDefs (false , defs) exDefs) x)
+
+blockOnMeta   : ∀ {a} {A : Set a} → Meta → TC A
+blockOnMeta m = blockTC (blockerMeta m)
+
+{-# WARNING_ON_USAGE onlyReduceDefs "DEPRECATED: Use `withReduceDefs` instead of `onlyReduceDefs`" #-}
+{-# WARNING_ON_USAGE dontReduceDefs "DEPRECATED: Use `withReduceDefs` instead of `dontReduceDefs`" #-}
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.Sigma.html b/lib/Agda.Builtin.Sigma.html new file mode 100644 index 00000000..1aa3a993 --- /dev/null +++ b/lib/Agda.Builtin.Sigma.html @@ -0,0 +1,19 @@ + +Agda.Builtin.Sigma
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.Sigma where
+
+open import Agda.Primitive
+
+record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
+  constructor _,_
+  field
+    fst : A
+    snd : B fst
+
+open Σ public
+
+infixr 4 _,_
+
+{-# BUILTIN SIGMA Σ #-}
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.Strict.html b/lib/Agda.Builtin.Strict.html new file mode 100644 index 00000000..7b38c5c8 --- /dev/null +++ b/lib/Agda.Builtin.Strict.html @@ -0,0 +1,11 @@ + +Agda.Builtin.Strict
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.Strict where
+
+open import Agda.Builtin.Equality
+
+primitive
+  primForce      : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
+  primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.String.html b/lib/Agda.Builtin.String.html new file mode 100644 index 00000000..217bfdd4 --- /dev/null +++ b/lib/Agda.Builtin.String.html @@ -0,0 +1,38 @@ + +Agda.Builtin.String
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.String where
+
+open import Agda.Builtin.Bool
+open import Agda.Builtin.Char
+open import Agda.Builtin.List
+open import Agda.Builtin.Maybe
+open import Agda.Builtin.Nat using (Nat)
+open import Agda.Builtin.Sigma
+
+postulate String : Set
+{-# BUILTIN STRING String #-}
+
+primitive
+  primStringUncons   : String → Maybe (Σ Char (λ _ → String))
+  primStringToList   : String → List Char
+  primStringFromList : List Char → String
+  primStringAppend   : String → String → String
+  primStringEquality : String → String → Bool
+  primShowChar       : Char → String
+  primShowString     : String → String
+  primShowNat        : Nat → String
+
+{-# COMPILE JS primStringUncons = function(x) {
+   if (x === "") { return z_jAgda_Agda_Builtin_Maybe["Maybe"]["nothing"]; };
+   return z_jAgda_Agda_Builtin_Maybe["Maybe"]["just"](z_jAgda_Agda_Builtin_Sigma["_,_"](x.charAt(0))(x.slice(1)));
+   }
+ #-}
+{-# COMPILE JS primStringToList = function(x) { return x.split(""); } #-}
+{-# COMPILE JS primStringFromList = function(x) { return x.join(""); } #-}
+{-# COMPILE JS primStringAppend = function(x) { return function(y) { return x+y; }; } #-}
+{-# COMPILE JS primStringEquality = function(x) { return function(y) { return x===y; }; } #-}
+{-# COMPILE JS primShowChar = function(x) { return JSON.stringify(x); } #-}
+{-# COMPILE JS primShowString = function(x) { return JSON.stringify(x); } #-}
+{-# COMPILE JS primShowNat = function(x) { return JSON.stringify(x); } #-}
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.Unit.html b/lib/Agda.Builtin.Unit.html new file mode 100644 index 00000000..ef3fcda6 --- /dev/null +++ b/lib/Agda.Builtin.Unit.html @@ -0,0 +1,12 @@ + +Agda.Builtin.Unit
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
+            --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.Unit where
+
+record ⊤ : Set where
+  instance constructor tt
+
+{-# BUILTIN UNIT ⊤ #-}
+{-# COMPILE GHC ⊤ = data () (()) #-}
+
\ No newline at end of file diff --git a/lib/Agda.Builtin.Word.html b/lib/Agda.Builtin.Word.html new file mode 100644 index 00000000..5267ee5b --- /dev/null +++ b/lib/Agda.Builtin.Word.html @@ -0,0 +1,15 @@ + +Agda.Builtin.Word
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
+            --no-sized-types --no-guardedness --level-universe #-}
+
+module Agda.Builtin.Word where
+
+open import Agda.Builtin.Nat
+
+postulate Word64 : Set
+{-# BUILTIN WORD64 Word64 #-}
+
+primitive
+  primWord64ToNat   : Word64 → Nat
+  primWord64FromNat : Nat → Word64
+
\ No newline at end of file diff --git a/lib/Agda.Primitive.html b/lib/Agda.Primitive.html new file mode 100644 index 00000000..3f6bab08 --- /dev/null +++ b/lib/Agda.Primitive.html @@ -0,0 +1,43 @@ + +Agda.Primitive
-- The Agda primitives (preloaded).
+
+{-# OPTIONS --cubical-compatible --no-import-sorts --level-universe #-}
+
+module Agda.Primitive where
+
+------------------------------------------------------------------------
+-- Universe levels
+------------------------------------------------------------------------
+
+infixl 6 _⊔_
+
+{-# BUILTIN PROP           Prop      #-}
+{-# BUILTIN TYPE           Set       #-}
+{-# BUILTIN STRICTSET      SSet      #-}
+
+{-# BUILTIN PROPOMEGA      Propω     #-}
+{-# BUILTIN SETOMEGA       Setω      #-}
+{-# BUILTIN STRICTSETOMEGA SSetω     #-}
+
+{-# BUILTIN LEVELUNIV      LevelUniv #-}
+
+-- Level is the first thing we need to define.
+-- The other postulates can only be checked if built-in Level is known.
+
+postulate
+  Level : LevelUniv
+
+-- MAlonzo compiles Level to (). This should be safe, because it is
+-- not possible to pattern match on levels.
+
+{-# BUILTIN LEVEL Level #-}
+
+postulate
+  lzero : Level
+  lsuc  : (ℓ : Level) → Level
+  _⊔_   : (ℓ₁ ℓ₂ : Level) → Level
+
+{-# BUILTIN LEVELZERO lzero #-}
+{-# BUILTIN LEVELSUC  lsuc  #-}
+{-# BUILTIN LEVELMAX  _⊔_   #-}
+
\ No newline at end of file diff --git a/lib/Agda.css b/lib/Agda.css new file mode 100644 index 00000000..2da37c9a --- /dev/null +++ b/lib/Agda.css @@ -0,0 +1,42 @@ +/* Aspects. */ +.Agda .Comment { color: #B22222 } +.Agda .Background {} +.Agda .Markup { color: #000000 } +.Agda .Keyword { color: #CD6600 } +.Agda .String { color: #B22222 } +.Agda .Number { color: #A020F0 } +.Agda .Symbol { color: #404040 } +.Agda .PrimitiveType { color: #0000CD } +.Agda .Pragma { color: black } +.Agda .Operator {} +.Agda .Hole { background: #B4EEB4 } + +/* NameKinds. */ +.Agda .Bound { color: black } +.Agda .Generalizable { color: black } +.Agda .InductiveConstructor { color: #008B00 } +.Agda .CoinductiveConstructor { color: #8B7500 } +.Agda .Datatype { color: #0000CD } +.Agda .Field { color: #EE1289 } +.Agda .Function { color: #0000CD } +.Agda .Macro { color: #0000CD } +.Agda .Module { color: #A020F0 } +.Agda .Postulate { color: #0000CD } +.Agda .Primitive { color: #0000CD } +.Agda .Record { color: #0000CD } + +/* OtherAspects. */ +.Agda .DottedPattern {} +.Agda .UnsolvedMeta { color: black; background: yellow } +.Agda .UnsolvedConstraint { color: black; background: yellow } +.Agda .TerminationProblem { color: black; background: #FFA07A } +.Agda .IncompletePattern { color: black; background: #F5DEB3 } +.Agda .Error { color: red; text-decoration: underline } +.Agda .TypeChecks { color: black; background: #ADD8E6 } +.Agda .Deadcode { color: black; background: #808080 } +.Agda .ShadowingInTelescope { color: black; background: #808080 } + +/* Standard attributes. */ +.Agda a { text-decoration: none } +.Agda a[href]:hover { background-color: #B4EEB4 } +.Agda [href].hover-highlight { background-color: #B4EEB4; } diff --git a/lib/Haskell.Prelude.html b/lib/Haskell.Prelude.html new file mode 100644 index 00000000..298f3107 --- /dev/null +++ b/lib/Haskell.Prelude.html @@ -0,0 +1,144 @@ + +Haskell.Prelude
{-# 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
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Absurd.html b/lib/Haskell.Prim.Absurd.html new file mode 100644 index 00000000..ce548d73 --- /dev/null +++ b/lib/Haskell.Prim.Absurd.html @@ -0,0 +1,25 @@ + +Haskell.Prim.Absurd
+module Haskell.Prim.Absurd where
+
+open import Haskell.Prim
+
+open import Agda.Builtin.Reflection renaming (bindTC to _>>=_; absurd to absurdP)
+
+private
+
+  pattern vArg x = arg (arg-info visible (modality relevant quantity-ω)) x
+
+  refute : Nat → Term
+  refute i = def (quote _$_) ( vArg (pat-lam (absurd-clause [] (vArg (absurdP 0) ∷ []) ∷ []) [])
+                             ∷ vArg (var i []) ∷ [])
+
+  tryRefute : Nat → Term → TC ⊤
+  tryRefute 0       _    = typeError (strErr "No variable of empty type found in the context" ∷ [])
+  tryRefute (suc n) hole = catchTC (unify hole (refute n)) (tryRefute n hole)
+
+absurd : Term → TC ⊤
+absurd hole = do
+  Γ ← getContext
+  tryRefute (lengthNat Γ) hole
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Applicative.html b/lib/Haskell.Prim.Applicative.html new file mode 100644 index 00000000..5ad0150b --- /dev/null +++ b/lib/Haskell.Prim.Applicative.html @@ -0,0 +1,94 @@ + +Haskell.Prim.Applicative
module Haskell.Prim.Applicative where
+
+open import Haskell.Prim
+open import Haskell.Prim.Either
+open import Haskell.Prim.Foldable
+open import Haskell.Prim.Functor
+open import Haskell.Prim.IO
+open import Haskell.Prim.List
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Monoid
+open import Haskell.Prim.Tuple
+
+
+--------------------------------------------------
+-- Applicative
+
+-- ** base
+record Applicative (f : Set → Set) : Set₁ where
+  infixl 4 _<*>_ _<*_ _*>_
+  field
+    pure  : a → f a
+    _<*>_ : f (a → b) → f a → f b
+    overlap ⦃ super ⦄ : Functor f
+    _<*_ : f a → f b → f a
+    _*>_ : f a → f b → f b
+-- ** defaults
+record DefaultApplicative (f : Set → Set) : Set₁ where
+  constructor mk
+  infixl 4 _<*>_ _<*_ _*>_
+  field
+    pure  : a → f a
+    _<*>_ : f (a → b) → f a → f b
+    overlap ⦃ super ⦄ : Functor f
+
+  _<*_ : f a → f b → f a
+  x <* y = const <$> x <*> y
+
+  _*>_ : f a → f b → f b
+  x *> y = const id <$> x <*> y
+-- ** export
+open Applicative ⦃...⦄ public
+{-# COMPILE AGDA2HS Applicative existing-class #-}
+-- ** instances
+instance
+  open DefaultApplicative
+
+  iDefaultApplicativeList : DefaultApplicative List
+  iDefaultApplicativeList .pure x = x ∷ []
+  iDefaultApplicativeList ._<*>_ fs xs = concatMap (λ f → map f xs) fs
+
+  iApplicativeList : Applicative List
+  iApplicativeList = record {DefaultApplicative iDefaultApplicativeList}
+
+  iDefaultApplicativeMaybe : DefaultApplicative Maybe
+  iDefaultApplicativeMaybe .pure = Just
+  iDefaultApplicativeMaybe ._<*>_ (Just f) (Just x) = Just (f x)
+  iDefaultApplicativeMaybe ._<*>_ _        _        = Nothing
+
+  iApplicativeMaybe : Applicative Maybe
+  iApplicativeMaybe = record {DefaultApplicative iDefaultApplicativeMaybe}
+
+  iDefaultApplicativeEither : DefaultApplicative (Either a)
+  iDefaultApplicativeEither .pure = Right
+  iDefaultApplicativeEither ._<*>_ (Right f) (Right x) = Right (f x)
+  iDefaultApplicativeEither ._<*>_ (Left e)  _         = Left e
+  iDefaultApplicativeEither ._<*>_ _         (Left e)  = Left e
+
+  iApplicativeEither : Applicative (Either a)
+  iApplicativeEither = record{DefaultApplicative iDefaultApplicativeEither}
+
+  iDefaultApplicativeFun : DefaultApplicative (λ b → a → b)
+  iDefaultApplicativeFun .pure        = const
+  iDefaultApplicativeFun ._<*>_ f g x = f x (g x)
+
+  iApplicativeFun : Applicative (λ b → a → b)
+  iApplicativeFun = record{DefaultApplicative iDefaultApplicativeFun}
+
+  iDefaultApplicativeTuple₂ : ⦃ Monoid a ⦄ → DefaultApplicative (a ×_)
+  iDefaultApplicativeTuple₂ .pure x                = mempty , x
+  iDefaultApplicativeTuple₂ ._<*>_ (a , f) (b , x) = a <> b , f x
+
+  iApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_)
+  iApplicativeTuple₂ = record{DefaultApplicative iDefaultApplicativeTuple₂}
+
+  iDefaultApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultApplicative (a × b ×_)
+  iDefaultApplicativeTuple₃ .pure x = mempty , mempty , x
+  iDefaultApplicativeTuple₃ ._<*>_ (a , u , f) (b , v , x) = a <> b , u <> v , f x
+
+  iApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_)
+  iApplicativeTuple₃ = record{DefaultApplicative iDefaultApplicativeTuple₃}
+
+instance postulate iApplicativeIO : Applicative IO
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Bool.html b/lib/Haskell.Prim.Bool.html new file mode 100644 index 00000000..36ec9c7c --- /dev/null +++ b/lib/Haskell.Prim.Bool.html @@ -0,0 +1,26 @@ + +Haskell.Prim.Bool
+module Haskell.Prim.Bool where
+
+open import Haskell.Prim
+
+--------------------------------------------------
+-- Booleans
+
+infixr 3 _&&_
+_&&_ : Bool → Bool → Bool
+False && _ = False
+True  && x = x
+
+infixr 2 _||_
+_||_ : Bool → Bool → Bool
+False || x = x
+True  || _ = True
+
+not : Bool → Bool
+not False = True
+not True  = False
+
+otherwise : Bool
+otherwise = True
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Bounded.html b/lib/Haskell.Prim.Bounded.html new file mode 100644 index 00000000..cb15129a --- /dev/null +++ b/lib/Haskell.Prim.Bounded.html @@ -0,0 +1,96 @@ + +Haskell.Prim.Bounded
+module Haskell.Prim.Bounded where
+
+open import Haskell.Prim
+open import Haskell.Prim.Eq
+open import Haskell.Prim.Int
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Ord
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Word
+
+--------------------------------------------------
+-- Bounded
+
+record BoundedBelow (a : Set) : Set where
+  field
+    minBound : a
+
+record BoundedAbove (a : Set) : Set where
+  field
+    maxBound : a
+
+record Bounded (a : Set) : Set where
+  field
+    overlap ⦃ below ⦄ : BoundedBelow a
+    overlap ⦃ above ⦄ : BoundedAbove a
+
+{-# COMPILE AGDA2HS Bounded existing-class #-}
+
+open BoundedBelow ⦃...⦄ public
+open BoundedAbove ⦃...⦄ public
+
+instance
+  iBounded : ⦃ BoundedBelow a ⦄ → ⦃ BoundedAbove a ⦄ → Bounded a
+  iBounded .Bounded.below = it
+  iBounded .Bounded.above = it
+
+instance
+  iBoundedBelowNat : BoundedBelow Nat
+  iBoundedBelowNat .minBound = 0
+
+  iBoundedBelowWord : BoundedBelow Word
+  iBoundedBelowWord .minBound = 0
+  iBoundedAboveWord : BoundedAbove Word
+  iBoundedAboveWord .maxBound = 18446744073709551615
+
+  iBoundedBelowInt : BoundedBelow Int
+  iBoundedBelowInt .minBound = -9223372036854775808
+  iBoundedAboveInt : BoundedAbove Int
+  iBoundedAboveInt .maxBound = 9223372036854775807
+
+  iBoundedBelowBool : BoundedBelow Bool
+  iBoundedBelowBool .minBound = False
+  iBoundedAboveBool : BoundedAbove Bool
+  iBoundedAboveBool .maxBound = True
+
+  iBoundedBelowChar : BoundedBelow Char
+  iBoundedBelowChar .minBound = '\0'
+  iBoundedAboveChar : BoundedAbove Char
+  iBoundedAboveChar .maxBound = '\1114111'
+
+  iBoundedBelowUnit : BoundedBelow ⊤
+  iBoundedBelowUnit .minBound = tt
+
+  iBoundedAboveUnit : BoundedAbove ⊤
+  iBoundedAboveUnit .maxBound = tt
+
+  iBoundedBelowTuple₂ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄
+                      → BoundedBelow (a × b)
+  iBoundedBelowTuple₂ .minBound = minBound , minBound
+  iBoundedAboveTuple₂ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄
+                      → BoundedAbove (a × b)
+  iBoundedAboveTuple₂ .maxBound = maxBound , maxBound
+
+  iBoundedBelowTuple₃ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄ → ⦃ BoundedBelow c ⦄
+                      → BoundedBelow (a × b × c)
+  iBoundedBelowTuple₃ .minBound = minBound , minBound , minBound
+  iBoundedAboveTuple₃ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄ → ⦃ BoundedAbove c ⦄
+                      → BoundedAbove (a × b × c)
+  iBoundedAboveTuple₃ .maxBound = maxBound , maxBound , maxBound
+
+  iBoundedBelowOrdering : BoundedBelow Ordering
+  iBoundedBelowOrdering .minBound = LT
+  iBoundedAboveOrdering : BoundedAbove Ordering
+  iBoundedAboveOrdering .maxBound = GT
+
+-- Sanity checks
+
+private
+  _ : addWord maxBound 1 ≡ minBound
+  _ = refl
+
+  _ : addInt maxBound 1 ≡ minBound
+  _ = refl
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Char.html b/lib/Haskell.Prim.Char.html new file mode 100644 index 00000000..5cef9fd6 --- /dev/null +++ b/lib/Haskell.Prim.Char.html @@ -0,0 +1,11 @@ + +Haskell.Prim.Char
module Haskell.Prim.Char where
+
+open import Haskell.Prim
+
+import Agda.Builtin.Char 
+open Agda.Builtin.Char using (Char)
+    
+eqChar : Char → Char → Bool
+eqChar a b = eqNat (c2n a) (c2n b)
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Double.html b/lib/Haskell.Prim.Double.html new file mode 100644 index 00000000..62772ace --- /dev/null +++ b/lib/Haskell.Prim.Double.html @@ -0,0 +1,17 @@ + +Haskell.Prim.Double
+module Haskell.Prim.Double where
+
+open import Agda.Builtin.Float public renaming (Float to Double)
+
+open import Haskell.Prim
+
+instance
+  iNumberDouble : Number Double
+  iNumberDouble .Number.Constraint _ = ⊤
+  iNumberDouble .fromNat n = primNatToFloat n
+
+  iNegativeDouble : Negative Double
+  iNegativeDouble .Negative.Constraint _ = ⊤
+  iNegativeDouble .fromNeg n = primFloatMinus 0.0 (fromNat n)
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Either.html b/lib/Haskell.Prim.Either.html new file mode 100644 index 00000000..84887f84 --- /dev/null +++ b/lib/Haskell.Prim.Either.html @@ -0,0 +1,22 @@ + +Haskell.Prim.Either
+module Haskell.Prim.Either where
+
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+
+--------------------------------------------------
+-- Either
+
+data Either (a b : Set) : Set where
+  Left  : a → Either a b
+  Right : b → Either a b
+
+either : (a → c) → (b → c) → Either a b → c
+either f g (Left  x) = f x
+either f g (Right y) = g y
+
+testBool : (b : Bool) → Either (IsFalse b) (IsTrue b)
+testBool False = Left  itsFalse
+testBool True  = Right itsTrue
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Enum.html b/lib/Haskell.Prim.Enum.html new file mode 100644 index 00000000..531d6c3d --- /dev/null +++ b/lib/Haskell.Prim.Enum.html @@ -0,0 +1,265 @@ + +Haskell.Prim.Enum
+module Haskell.Prim.Enum where
+
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Bounded
+open import Haskell.Prim.Either
+open import Haskell.Prim.Eq
+open import Haskell.Prim.Functor
+open import Haskell.Prim.Int
+open import Haskell.Prim.Integer
+open import Haskell.Prim.List
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Num
+open import Haskell.Prim.Ord
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Word
+
+
+--------------------------------------------------
+-- Enum
+--    Assumptions: unbounded enums have no constraints on their
+--    operations and bounded enums should work on all values between
+--    minBound and maxBound. Unbounded enums do not support enumFrom
+--    and enumFromThen (since they return infinite lists).
+
+@0 IfBoundedBelow : Maybe (BoundedBelow a) → (⦃ BoundedBelow a ⦄ → Set) → Set
+IfBoundedBelow Nothing  k = ⊤
+IfBoundedBelow (Just i) k = k ⦃ i ⦄
+
+@0 IfBoundedAbove : Maybe (BoundedAbove a) → (⦃ BoundedAbove a ⦄ → Set) → Set
+IfBoundedAbove Nothing  k = ⊤
+IfBoundedAbove (Just i) k = k ⦃ i ⦄
+
+record Enum (a : Set) : Set₁ where
+  field
+    BoundedBelowEnum : Maybe (BoundedBelow a)
+    BoundedAboveEnum : Maybe (BoundedAbove a)
+    fromEnum         : a → Int
+
+  private
+    @0 IsBoundedBelow : Set
+    IsBoundedBelow = maybe ⊥ (λ _ → ⊤) BoundedBelowEnum
+
+    @0 IsBoundedAbove : Set
+    IsBoundedAbove = maybe ⊥ (λ _ → ⊤) BoundedAboveEnum
+
+    @0 TrueIfLB : (⦃ BoundedBelow a ⦄ → Bool) → Set
+    TrueIfLB C = IfBoundedBelow BoundedBelowEnum (IsTrue C)
+
+    @0 TrueIfUB : (⦃ BoundedAbove a ⦄ → Bool) → Set
+    TrueIfUB C = IfBoundedAbove BoundedAboveEnum (IsTrue C)
+
+    @0 FalseIfLB : (⦃ BoundedBelow a ⦄ → Bool) → Set
+    FalseIfLB C = IfBoundedBelow BoundedBelowEnum (IsFalse C)
+
+    @0 FalseIfUB : (⦃ BoundedAbove a ⦄ → Bool) → Set
+    FalseIfUB C = IfBoundedAbove BoundedAboveEnum (IsFalse C)
+
+    minInt : ⦃ BoundedBelow a ⦄ → Int
+    minInt ⦃ _ ⦄ = fromEnum minBound
+
+    maxInt : ⦃ BoundedAbove a ⦄ → Int
+    maxInt ⦃ _ ⦄ = fromEnum maxBound
+
+  field
+    toEnum : (n : Int) → @0 ⦃ TrueIfLB (minInt <= n) ⦄ → @0 ⦃ TrueIfUB (n <= maxInt) ⦄ → a
+    succ   : (x : a) → @0 ⦃ FalseIfUB (fromEnum x == maxInt) ⦄ → a
+    pred   : (x : a) → @0 ⦃ FalseIfLB (fromEnum x == minInt) ⦄ → a
+
+    enumFrom       : @0 ⦃ IsBoundedAbove ⦄ → a → List a
+    enumFromTo     : a → a → List a
+    -- In the Prelude Enum instances `enumFromThenTo x x y` gives the
+    -- infinite list of `x`s. The constraint is a little bit stronger than it needs to be,
+    -- since it rules out different x and x₁ that maps to the same Int, but this saves us
+    -- requiring an Eq instance for `a`, and it's not a terrible limitation to not be able to
+    -- write [0, 2^64 .. 2^66].
+    enumFromThenTo : (x x₁ : a) → @0 ⦃ IsFalse (fromEnum x == fromEnum x₁) ⦄ → a → List a
+    enumFromThen   : @0 ⦃ IsBoundedBelow ⦄ → @0 ⦃ IsBoundedAbove ⦄ → (x x₁ : a) → @0 ⦃ IsFalse (fromEnum x == fromEnum x₁) ⦄ → List a
+
+open Enum ⦃...⦄ public
+
+{-# COMPILE AGDA2HS Enum existing-class #-}
+
+private
+  divNat : Nat → Nat → Nat
+  divNat a 0       = 0
+  divNat a (suc b) = div-helper 0 b a b
+
+  diff : Integer → Integer → Maybe Nat
+  diff a b =
+    case a - b of λ where
+      (pos n)    → Just n
+      (negsuc _) → Nothing
+
+  unsafeIntegerToNat : Integer → Nat
+  unsafeIntegerToNat (pos n) = n
+  unsafeIntegerToNat (negsuc _) = 0
+
+  integerFromCount : Integer → Integer → Nat → List Integer
+  integerFromCount a step 0       = []
+  integerFromCount a step (suc n) = a ∷ integerFromCount (a + step) step n
+
+  integerFromTo : Integer → Integer → List Integer
+  integerFromTo a b = maybe [] (integerFromCount a 1 ∘ suc) (diff b a)
+
+  integerFromThenTo : (a a₁ : Integer) → @0 ⦃ IsFalse (integerToInt a == integerToInt a₁) ⦄ → Integer → List Integer
+  integerFromThenTo a a₁ b =
+    case compare a a₁ of λ where
+      LT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a₁ - a))))) (diff b a)
+      EQ → [] -- impossible
+      GT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a - a₁))))) (diff a b)
+
+instance
+  iEnumInteger : Enum Integer
+  iEnumInteger .BoundedBelowEnum  = Nothing
+  iEnumInteger .BoundedAboveEnum  = Nothing
+  iEnumInteger .fromEnum          = integerToInt
+  iEnumInteger .toEnum          n = intToInteger n
+  iEnumInteger .succ              = _+ 1
+  iEnumInteger .pred              = _- 1
+  iEnumInteger .enumFromTo        = integerFromTo
+  iEnumInteger .enumFromThenTo    = integerFromThenTo
+
+private
+  fromTo : (from : a → Integer) (to : Integer → a)
+         → a → a → List a
+  fromTo from to a b = map to (enumFromTo (from a) (from b))
+
+  fromThenTo : (from : a → Integer) (to : Integer → a)
+             → (x x₁ : a) → @0 ⦃ IsFalse (fromEnum (from x) == fromEnum (from x₁)) ⦄ → a → List a
+  fromThenTo from to a a₁ b = map to (enumFromThenTo (from a) (from a₁) (from b))
+
+
+instance
+  iEnumNat : Enum Nat
+  iEnumNat .BoundedBelowEnum = Just it
+  iEnumNat .BoundedAboveEnum = Nothing
+  iEnumNat .fromEnum = integerToInt ∘ pos
+  iEnumNat .toEnum n = unsafeIntegerToNat (intToInteger n)
+  iEnumNat .succ n = suc n
+  iEnumNat .pred (suc n) = n
+  iEnumNat .enumFromTo = fromTo pos unsafeIntegerToNat
+  iEnumNat .enumFromThenTo = fromThenTo pos unsafeIntegerToNat
+
+  iEnumInt : Enum Int
+  iEnumInt .BoundedBelowEnum      = Just it
+  iEnumInt .BoundedAboveEnum      = Just it
+  iEnumInt .fromEnum              = integerToInt ∘ intToInteger
+  iEnumInt .toEnum         n      = integerToInt (intToInteger n)
+  iEnumInt .succ           x      = integerToInt (intToInteger x + 1)
+  iEnumInt .pred           x      = integerToInt (intToInteger x - 1)
+  iEnumInt .enumFromTo     a b    = fromTo intToInteger integerToInt a b
+  iEnumInt .enumFromThenTo a a₁ b = fromThenTo intToInteger integerToInt a a₁ b
+  iEnumInt .enumFrom       a      = fromTo intToInteger integerToInt a maxBound
+  iEnumInt .enumFromThen   a a₁   =
+    if a < a₁ then fromThenTo intToInteger integerToInt a a₁ maxBound
+              else fromThenTo intToInteger integerToInt a a₁ minBound
+
+  iEnumWord : Enum Word
+  iEnumWord .BoundedBelowEnum      = Just it
+  iEnumWord .BoundedAboveEnum      = Just it
+  iEnumWord .fromEnum              = integerToInt ∘ wordToInteger
+  iEnumWord .toEnum         n      = integerToWord (intToInteger n)
+  iEnumWord .succ           x      = integerToWord (wordToInteger x + 1)
+  iEnumWord .pred           x      = integerToWord (wordToInteger x - 1)
+  iEnumWord .enumFromTo     a b    = fromTo wordToInteger integerToWord a b
+  iEnumWord .enumFromThenTo a a₁ b = fromThenTo wordToInteger integerToWord a a₁ b
+  iEnumWord .enumFrom       a      = fromTo wordToInteger integerToWord a maxBound
+  iEnumWord .enumFromThen   a a₁   =
+    if a < a₁ then fromThenTo wordToInteger integerToWord a a₁ maxBound
+              else fromThenTo wordToInteger integerToWord a a₁ minBound
+
+private
+  fromBool : Bool → Integer
+  fromBool = if_then 1 else 0
+
+  toBool : Integer → Bool
+  toBool = _/= 0
+
+instance
+  iEnumBool : Enum Bool
+  iEnumBool .BoundedBelowEnum      = Just it
+  iEnumBool .BoundedAboveEnum      = Just it
+  iEnumBool .fromEnum              = integerToInt ∘ fromBool
+  iEnumBool .toEnum         n      = toBool (intToInteger n)
+  iEnumBool .succ           x      = toBool (fromBool x + 1)
+  iEnumBool .pred           x      = toBool (fromBool x - 1)
+  iEnumBool .enumFromTo     a b    = fromTo fromBool toBool a b
+  iEnumBool .enumFromThenTo a a₁ b = fromThenTo fromBool toBool a a₁ b
+  iEnumBool .enumFrom       a      = fromTo fromBool toBool a maxBound
+  iEnumBool .enumFromThen   a a₁   =
+    if a < a₁ then fromThenTo fromBool toBool a a₁ maxBound
+              else fromThenTo fromBool toBool a a₁ minBound
+
+private
+  fromOrdering : Ordering → Integer
+  fromOrdering = λ where LT → 0; EQ → 1; GT → 2
+
+  toOrdering : Integer → Ordering
+  toOrdering = λ where (pos 0) → LT; (pos 1) → EQ; _ → GT
+
+instance
+  iEnumOrdering : Enum Ordering
+  iEnumOrdering .BoundedBelowEnum      = Just it
+  iEnumOrdering .BoundedAboveEnum      = Just it
+  iEnumOrdering .fromEnum              = integerToInt ∘ fromOrdering
+  iEnumOrdering .toEnum         n      = toOrdering (intToInteger n)
+  iEnumOrdering .succ           x      = toOrdering (fromOrdering x + 1)
+  iEnumOrdering .pred           x      = toOrdering (fromOrdering x - 1)
+  iEnumOrdering .enumFromTo     a b    = fromTo fromOrdering toOrdering a b
+  iEnumOrdering .enumFromThenTo a a₁ b = fromThenTo fromOrdering toOrdering a a₁ b
+  iEnumOrdering .enumFrom       a      = fromTo fromOrdering toOrdering a maxBound
+  iEnumOrdering .enumFromThen   a a₁   =
+    if a < a₁ then fromThenTo fromOrdering toOrdering a a₁ maxBound
+              else fromThenTo fromOrdering toOrdering a a₁ minBound
+
+private
+  fromUnit : ⊤ → Integer
+  fromUnit _ = 0
+
+  toUnit : Integer → ⊤
+  toUnit _ = tt
+
+instance
+  iEnumUnit : Enum ⊤
+  iEnumUnit .BoundedBelowEnum      = Just it
+  iEnumUnit .BoundedAboveEnum      = Just it
+  iEnumUnit .fromEnum              = integerToInt ∘ fromUnit
+  iEnumUnit .toEnum         n      = toUnit (intToInteger n)
+  iEnumUnit .succ           x      = toUnit (fromUnit x + 1)
+  iEnumUnit .pred           x      = toUnit (fromUnit x - 1)
+  iEnumUnit .enumFromTo     a b    = fromTo fromUnit toUnit a b
+  iEnumUnit .enumFromThenTo a a₁ b = fromThenTo fromUnit toUnit a a₁ b
+  iEnumUnit .enumFrom       a      = fromTo fromUnit toUnit a maxBound
+  iEnumUnit .enumFromThen   a a₁   =
+    if a < a₁ then fromThenTo fromUnit toUnit a a₁ maxBound
+              else fromThenTo fromUnit toUnit a a₁ minBound
+
+private
+  fromChar : Char → Integer
+  fromChar = pos ∘ c2n
+
+  toChar : Integer → Char
+  toChar = λ where (pos n) → primNatToChar n; _ → '_'
+
+instance
+  iEnumChar : Enum Char
+  iEnumChar .BoundedBelowEnum      = Just it
+  iEnumChar .BoundedAboveEnum      = Just it
+  iEnumChar .fromEnum              = integerToInt ∘ fromChar
+  iEnumChar .toEnum         n      = toChar (intToInteger n)
+  iEnumChar .succ           x      = toChar (fromChar x + 1)
+  iEnumChar .pred           x      = toChar (fromChar x - 1)
+  iEnumChar .enumFromTo     a b    = fromTo fromChar toChar a b
+  iEnumChar .enumFromThenTo a a₁ b = fromThenTo fromChar toChar a a₁ b
+  iEnumChar .enumFrom       a      = fromTo fromChar toChar a maxBound
+  iEnumChar .enumFromThen   a a₁   =
+    if a < a₁ then fromThenTo fromChar toChar a a₁ maxBound
+              else fromThenTo fromChar toChar a a₁ minBound
+
+  -- Missing:
+  --  Enum Double  (can't go via Integer)
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Eq.html b/lib/Haskell.Prim.Eq.html new file mode 100644 index 00000000..47fb79ea --- /dev/null +++ b/lib/Haskell.Prim.Eq.html @@ -0,0 +1,84 @@ + +Haskell.Prim.Eq
+module Haskell.Prim.Eq where
+
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Char
+open import Haskell.Prim.Integer
+open import Haskell.Prim.Int
+open import Haskell.Prim.Word
+open import Haskell.Prim.Double
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Either
+
+--------------------------------------------------
+-- Eq
+
+record Eq (a : Set) : Set where
+  infix 4 _==_
+  field
+    _==_ : a → a → Bool
+
+open Eq ⦃...⦄ public
+
+{-# COMPILE AGDA2HS Eq existing-class #-}
+
+_/=_ : {{Eq a}} → a → a → Bool
+x /= y = not (x == y)
+
+infix 4 _/=_
+
+instance
+  iEqNat : Eq Nat
+  iEqNat ._==_ = eqNat
+
+  iEqInteger : Eq Integer
+  iEqInteger ._==_ = eqInteger
+
+  iEqInt : Eq Int
+  iEqInt ._==_ = eqInt
+
+  iEqWord : Eq Word
+  iEqWord ._==_ = eqWord
+
+  iEqDouble : Eq Double
+  iEqDouble ._==_ = primFloatEquality
+
+  iEqBool : Eq Bool
+  iEqBool ._==_ False False = True
+  iEqBool ._==_ True  True  = True
+  iEqBool ._==_ _     _     = False
+
+  iEqChar : Eq Char
+  iEqChar ._==_ = eqChar
+
+  iEqUnit : Eq ⊤
+  iEqUnit ._==_ _ _ = True
+
+  iEqTuple₂ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (a × b)
+  iEqTuple₂ ._==_ (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ && y₁ == y₂
+
+  iEqTuple₃ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → ⦃ Eq c ⦄ → Eq (a × b × c)
+  iEqTuple₃ ._==_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ == x₂ && y₁ == y₂ && z₁ == z₂
+
+  iEqList : ⦃ Eq a ⦄ → Eq (List a)
+  iEqList {a} ._==_ = eqList
+    where
+      eqList : List a → List a → Bool
+      eqList [] [] = True
+      eqList (x ∷ xs) (y ∷ ys) = x == y && eqList xs ys
+      eqList _ _ = False
+
+
+  iEqMaybe : ⦃ Eq a ⦄ → Eq (Maybe a)
+  iEqMaybe ._==_ Nothing  Nothing  = True
+  iEqMaybe ._==_ (Just x) (Just y) = x == y
+  iEqMaybe ._==_ _        _        = False
+
+  iEqEither : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (Either a b)
+  iEqEither ._==_ (Left  x) (Left  y) = x == y
+  iEqEither ._==_ (Right x) (Right y) = x == y
+  iEqEither ._==_ _        _          = False
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Foldable.html b/lib/Haskell.Prim.Foldable.html new file mode 100644 index 00000000..4cc43298 --- /dev/null +++ b/lib/Haskell.Prim.Foldable.html @@ -0,0 +1,124 @@ + +Haskell.Prim.Foldable
+module Haskell.Prim.Foldable where
+
+open import Haskell.Prim
+open import Haskell.Prim.Num hiding (abs)
+open import Haskell.Prim.Eq
+open import Haskell.Prim.List
+open import Haskell.Prim.Int
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Either
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Monoid
+
+--------------------------------------------------
+-- Foldable
+
+-- ** base
+record Foldable (t : Set → Set) : Set₁ where
+  field
+    foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b
+    foldr : (a → b → b) → b → t a → b
+    foldl : (b → a → b) → b → t a → b
+    any : (a → Bool) → t a → Bool
+    all : (a → Bool) → t a → Bool
+    and : t Bool → Bool
+    null : t a → Bool
+    or : t Bool → Bool
+    concat : t (List a) → List a
+    concatMap : (a → List b) → t a → List b
+    elem : ⦃ Eq a ⦄ → a → t a → Bool
+    notElem : ⦃ Eq a ⦄ → a → t a → Bool
+    toList : t a → List a
+    sum : ⦃ iNum : Num a ⦄ → t a → a
+    product : ⦃ iNum : Num a ⦄ → t a → a
+    length : t a → Int
+-- ** defaults
+record DefaultFoldable (t : Set → Set) : Set₁ where
+  module M = Foldable {t = t}
+  field foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b
+
+  foldr : (a → b → b) → b → t a → b
+  foldr f z t = foldMap ⦃ MonoidEndo ⦄ f t z
+
+  foldl : (b → a → b) → b → t a → b
+  foldl f z t = foldMap ⦃ MonoidEndoᵒᵖ ⦄ (flip f) t z
+
+  any : (a → Bool) → t a → Bool
+  any = foldMap ⦃ MonoidDisj ⦄
+
+  all : (a → Bool) → t a → Bool
+  all = foldMap ⦃ MonoidConj ⦄
+
+  and : t Bool → Bool
+  and = all id
+
+  or : t Bool → Bool
+  or = any id
+
+  null : t a → Bool
+  null = all (const False)
+
+  concat : t (List a) → List a
+  concat = foldMap id
+
+  concatMap : (a → List b) → t a → List b
+  concatMap = foldMap
+
+  elem : ⦃ Eq a ⦄ → a → t a → Bool
+  elem x = foldMap ⦃ MonoidDisj ⦄ (x ==_)
+
+  notElem : ⦃ Eq a ⦄ → a → t a → Bool
+  notElem x t = not (elem x t)
+
+  toList : t a → List a
+  toList = foldr _∷_ []
+
+  sum : ⦃ iNum : Num a ⦄ → t a → a
+  sum = foldMap ⦃ MonoidSum ⦄ id
+
+  product : ⦃ iNum : Num a ⦄ → t a → a
+  product = foldMap ⦃ MonoidProduct ⦄ id
+
+  length : t a → Int
+  length = foldMap ⦃ MonoidSum ⦄ (const 1)
+-- ** export
+open Foldable ⦃...⦄ public
+{-# COMPILE AGDA2HS Foldable existing-class #-}
+
+-- ** instances
+instance
+  iDefaultFoldableList : DefaultFoldable List
+  iDefaultFoldableList .DefaultFoldable.foldMap = foldMapList
+    where
+      foldMapList : ⦃ Monoid b ⦄ → (a → b) → List a → b
+      foldMapList f []       = mempty
+      foldMapList f (x ∷ xs) = f x <> foldMapList f xs
+
+  iFoldableList : Foldable List
+  iFoldableList = record {DefaultFoldable iDefaultFoldableList}
+
+  iDefaultFoldableMaybe : DefaultFoldable Maybe
+  iDefaultFoldableMaybe .DefaultFoldable.foldMap = λ where
+    _ Nothing  → mempty
+    f (Just x) → f x
+
+  iFoldableMaybe : Foldable Maybe
+  iFoldableMaybe = record {DefaultFoldable iDefaultFoldableMaybe}
+
+  iDefaultFoldableEither : DefaultFoldable (Either a)
+  iDefaultFoldableEither .DefaultFoldable.foldMap = λ where
+    _ (Left _)  → mempty
+    f (Right x) → f x
+
+  iFoldableEither : Foldable (Either a)
+  iFoldableEither = record {DefaultFoldable iDefaultFoldableEither}
+
+  iDefaultFoldablePair : DefaultFoldable (a ×_)
+  iDefaultFoldablePair .DefaultFoldable.foldMap = λ f (_ , x) → f x
+
+  iFoldablePair : Foldable (a ×_)
+  iFoldablePair = record {DefaultFoldable iDefaultFoldablePair}
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Functor.html b/lib/Haskell.Prim.Functor.html new file mode 100644 index 00000000..95277d4e --- /dev/null +++ b/lib/Haskell.Prim.Functor.html @@ -0,0 +1,91 @@ + +Haskell.Prim.Functor
+module Haskell.Prim.Functor where
+
+open import Haskell.Prim
+open import Haskell.Prim.Either
+open import Haskell.Prim.IO
+open import Haskell.Prim.List
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Tuple
+
+--------------------------------------------------
+-- Functor
+
+-- ** base
+record Functor (f : Set → Set) : Set₁ where
+  infixl 4 _<$_
+  field
+    fmap : (a → b) → f a → f b
+    _<$_ : (@0 {{ b }} → a) → f b → f a
+-- ** defaults
+record DefaultFunctor (f : Set → Set) : Set₁ where
+  field fmap : (a → b) → f a → f b
+
+  infixl 4 _<$_
+
+  _<$_ : (@0 {{ b }} → a) → f b → f a
+  x <$ m = fmap (λ b → x {{b}}) m
+
+-- ** export
+open Functor ⦃...⦄ public
+{-# COMPILE AGDA2HS Functor existing-class #-}
+
+_<$>_ : {{Functor f}} → (a → b) → f a → f b
+_<$>_ = fmap
+
+_<&>_ : {{Functor f}} → f a → (a → b) → f b
+m <&> f = fmap f m
+
+_$>_ : {{Functor f}} → f a → (@0 {{ a }} → b) → f b
+m $> x = x <$ m
+
+void : {{Functor f}} → f a → f ⊤
+void = tt <$_
+
+infixl 1 _<&>_
+infixl 4 _<$>_ _$>_
+
+instance
+  iDefaultFunctorList : DefaultFunctor List
+  iDefaultFunctorList .DefaultFunctor.fmap = map
+
+  iFunctorList : Functor List
+  iFunctorList = record{DefaultFunctor iDefaultFunctorList}
+
+  iDefaultFunctorMaybe : DefaultFunctor Maybe
+  iDefaultFunctorMaybe .DefaultFunctor.fmap = λ where
+    f Nothing  → Nothing
+    f (Just x) → Just (f x)
+
+  iFunctorMaybe : Functor Maybe
+  iFunctorMaybe = record{DefaultFunctor iDefaultFunctorMaybe}
+
+  iDefaultFunctorEither : DefaultFunctor (Either a)
+  iDefaultFunctorEither .DefaultFunctor.fmap = λ where
+    f (Left  x) → Left x
+    f (Right y) → Right (f y)
+
+  iFunctorEither : Functor (Either a)
+  iFunctorEither = record{DefaultFunctor iDefaultFunctorEither}
+
+  iDefaultFunctorFun : DefaultFunctor (λ b → a → b)
+  iDefaultFunctorFun .DefaultFunctor.fmap = _∘_
+
+  iFunctorFun : Functor (λ b → a → b)
+  iFunctorFun = record{DefaultFunctor iDefaultFunctorFun}
+
+  iDefaultFunctorTuple₂ : DefaultFunctor (a ×_)
+  iDefaultFunctorTuple₂ .DefaultFunctor.fmap = λ f (x , y) → x , f y
+
+  iFunctorTuple₂ : Functor (a ×_)
+  iFunctorTuple₂ = record{DefaultFunctor iDefaultFunctorTuple₂}
+
+  iDefaultFunctorTuple₃ : DefaultFunctor (a × b ×_)
+  iDefaultFunctorTuple₃ .DefaultFunctor.fmap = λ where f (x , y , z) → x , y , f z
+
+  iFunctorTuple₃ : Functor (a × b ×_)
+  iFunctorTuple₃ = record{DefaultFunctor iDefaultFunctorTuple₃}
+
+instance postulate iFunctorIO : Functor IO
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.IO.html b/lib/Haskell.Prim.IO.html new file mode 100644 index 00000000..03f84638 --- /dev/null +++ b/lib/Haskell.Prim.IO.html @@ -0,0 +1,29 @@ + +Haskell.Prim.IO
module Haskell.Prim.IO where
+
+open import Haskell.Prim
+open import Haskell.Prim.Show
+open import Haskell.Prim.String
+
+postulate IO : ∀{a} → Set a → Set a
+
+FilePath = String
+
+postulate
+  -- Input functions
+  interact       : (String → String) → IO ⊤
+  getContents    : IO String
+  getLine        : IO String
+  getChar        : IO Char
+
+  -- Output functions
+  print          : ⦃ Show a ⦄ → a → IO ⊤
+  putChar        : Char → IO ⊤
+  putStr         : String → IO ⊤
+  putStrLn       : String → IO ⊤
+
+  -- Files
+  readFile       : FilePath → IO String
+  writeFile      : FilePath → String → IO ⊤
+  appendFile     : FilePath → String → IO ⊤
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Int.html b/lib/Haskell.Prim.Int.html new file mode 100644 index 00000000..65fd41c2 --- /dev/null +++ b/lib/Haskell.Prim.Int.html @@ -0,0 +1,112 @@ + +Haskell.Prim.Int
{-# OPTIONS --no-auto-inline #-}
+
+-- Agda doesn't have an Int type (only Word64). With some work we
+-- can represent signed ints using Word64.
+
+module Haskell.Prim.Int where
+
+open import Haskell.Prim
+open import Haskell.Prim.Word
+open import Haskell.Prim.Integer
+open import Haskell.Prim.Bool
+
+
+--------------------------------------------------
+-- Definition
+
+data Int : Set where
+  int64 : Word64 → Int
+
+intToWord : Int → Word64
+intToWord (int64 a) = a
+
+unsafeIntToNat : Int → Nat
+unsafeIntToNat a = w2n (intToWord a)
+
+
+--------------------------------------------------
+-- Literals
+
+private
+  2⁶⁴ : Nat
+  2⁶⁴ = 18446744073709551616
+
+  2⁶³ : Nat
+  2⁶³ = 9223372036854775808
+
+  maxInt : Nat
+  maxInt = monusNat 2⁶³ 1
+
+instance
+  iNumberInt : Number Int
+  iNumberInt .Number.Constraint n = IsTrue (ltNat n 2⁶³)
+  iNumberInt .fromNat n = int64 (n2w n)
+
+  iNegativeInt : Negative Int
+  iNegativeInt .Negative.Constraint n = IsTrue (ltNat n (addNat 1 2⁶³))
+  iNegativeInt .fromNeg n = int64 (n2w (monusNat 2⁶⁴ n))
+
+
+--------------------------------------------------
+-- Arithmetic
+
+isNegativeInt : Int → Bool
+isNegativeInt (int64 w) = ltNat maxInt (w2n w)
+
+eqInt : Int → Int → Bool
+eqInt (int64 a) (int64 b) = eqNat (w2n a) (w2n b)
+
+negateInt : Int → Int
+negateInt (int64 a) = int64 (n2w (monusNat 2⁶⁴ (w2n a)))
+
+intToInteger : Int → Integer
+intToInteger a = if isNegativeInt a then negsuc (monusNat (unsafeIntToNat (negateInt a)) 1)
+                                    else pos (unsafeIntToNat a)
+
+integerToInt : Integer → Int
+integerToInt (pos    n) = int64 (n2w n)
+integerToInt (negsuc n) = negateInt (int64 (n2w (suc n)))
+
+private
+  ltPosInt : Int → Int → Bool
+  ltPosInt (int64 a) (int64 b) = ltWord a b
+
+ltInt : Int → Int → Bool
+ltInt a b with isNegativeInt a | isNegativeInt b
+... | True  | False = True
+... | False | True  = False
+... | True  | True  = ltPosInt (negateInt b) (negateInt a)
+... | False | False = ltPosInt a b
+
+addInt : Int → Int → Int
+addInt (int64 a) (int64 b) = int64 (addWord a b)
+
+subInt : Int → Int → Int
+subInt a b = addInt a (negateInt b)
+
+mulInt : Int → Int → Int
+mulInt (int64 a) (int64 b) = int64 (mulWord a b)
+
+absInt : Int → Int
+absInt a = if isNegativeInt a then negateInt a else a
+
+signInt : Int → Int
+signInt a = if      isNegativeInt a then -1
+            else if eqInt a 0       then 0 else 1
+
+showInt : Int → List Char
+showInt a = showInteger (intToInteger a)
+
+
+--------------------------------------------------
+-- Constraints
+
+@0 IsNonNegativeInt : Int → Set
+IsNonNegativeInt a@(int64 _) =
+  if isNegativeInt a then TypeError (primStringAppend (primStringFromList (showInt a)) " is negative")
+                     else ⊤
+
+intToNat : (a : Int) → @0 ⦃ IsNonNegativeInt a ⦄ → Nat
+intToNat a = unsafeIntToNat a
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Integer.html b/lib/Haskell.Prim.Integer.html new file mode 100644 index 00000000..26a4dd97 --- /dev/null +++ b/lib/Haskell.Prim.Integer.html @@ -0,0 +1,108 @@ + +Haskell.Prim.Integer
+module Haskell.Prim.Integer where
+
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+
+{-|
+This module contains functions that should not be used
+within code that is supposed to be translated to Haskell.
+Nevertheless, these functions must be accessible for
+proofs (within the standard library).
+Hence, these functions are not flagged as private but
+instead are collected in a dedicated module that is not
+opened by default.
+-}
+module Internal where
+  negNat : Nat → Integer
+  negNat 0       = pos 0
+  negNat (suc n) = negsuc n
+
+  subNat : Nat → Nat → Integer
+  subNat n       zero    = pos n
+  subNat zero    (suc m) = negsuc m
+  subNat (suc n) (suc m) = subNat n m
+open Internal
+
+--------------------------------------------------
+-- Literals
+
+
+instance
+  iNumberInteger : Number Integer
+  iNumberInteger .Number.Constraint _ = ⊤
+  iNumberInteger .fromNat n = pos n
+
+  iNegativeInteger : Negative Integer
+  iNegativeInteger .Negative.Constraint _ = ⊤
+  iNegativeInteger .fromNeg n = negNat n
+
+
+--------------------------------------------------
+-- Arithmetic
+
+negateInteger : Integer → Integer
+negateInteger (pos 0)       = pos 0
+negateInteger (pos (suc n)) = negsuc n
+negateInteger (negsuc n)    = pos (suc n)
+
+addInteger : Integer → Integer → Integer
+addInteger (pos    n) (pos    m) = pos (addNat n m)
+addInteger (pos    n) (negsuc m) = subNat n (suc m)
+addInteger (negsuc n) (pos    m) = subNat m (suc n)
+addInteger (negsuc n) (negsuc m) = negsuc (suc (addNat n m))
+
+subInteger : Integer → Integer → Integer
+subInteger n m = addInteger n (negateInteger m)
+
+mulInteger : Integer → Integer → Integer
+mulInteger (pos    n) (pos    m) = pos (mulNat n m)
+mulInteger (pos    n) (negsuc m) = negNat (mulNat n (suc m))
+mulInteger (negsuc n) (pos    m) = negNat (mulNat (suc n) m)
+mulInteger (negsuc n) (negsuc m) = pos (mulNat (suc n) (suc m))
+
+absInteger : Integer → Integer
+absInteger (pos    n) = pos n
+absInteger (negsuc n) = pos (suc n)
+
+signInteger : Integer → Integer
+signInteger (pos 0)       = 0
+signInteger (pos (suc _)) = 1
+signInteger (negsuc _)    = -1
+
+
+--------------------------------------------------
+-- Comparisons
+
+eqInteger : Integer → Integer → Bool
+eqInteger (pos n)    (pos m)    = eqNat n m
+eqInteger (negsuc n) (negsuc m) = eqNat n m
+eqInteger _          _          = False
+
+ltInteger : Integer → Integer → Bool
+ltInteger (pos    n) (pos    m) = ltNat n m
+ltInteger (pos    n) (negsuc _) = False
+ltInteger (negsuc n) (pos    _) = True
+ltInteger (negsuc n) (negsuc m) = ltNat m n
+
+
+--------------------------------------------------
+-- Show
+
+showInteger : Integer → List Char
+showInteger n = primStringToList (primShowInteger n)
+
+
+--------------------------------------------------
+-- Constraints
+
+isNegativeInteger : Integer → Bool
+isNegativeInteger (pos _)    = False
+isNegativeInteger (negsuc _) = True
+
+@0 IsNonNegativeInteger : Integer → Set
+IsNonNegativeInteger (pos _)      = ⊤
+IsNonNegativeInteger n@(negsuc _) =
+  TypeError (primStringAppend (primShowInteger n) (" is negative"))
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.List.html b/lib/Haskell.Prim.List.html new file mode 100644 index 00000000..8ea8afad --- /dev/null +++ b/lib/Haskell.Prim.List.html @@ -0,0 +1,130 @@ + +Haskell.Prim.List
+module Haskell.Prim.List where
+
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Int
+
+
+--------------------------------------------------
+-- List
+
+map : (a → b) → List a → List b
+map f []       = []
+map f (x ∷ xs) = f x ∷ map f xs
+
+infixr 5 _++_
+_++_ : ∀ {@0 ℓ} {@0 a : Set ℓ} → List a → List a → List a
+[]       ++ ys = ys
+(x ∷ xs) ++ ys = x ∷ xs ++ ys
+
+filter : (a → Bool) → List a → List a
+filter p []       = []
+filter p (x ∷ xs) = if p x then x ∷ filter p xs else filter p xs
+
+scanl : (b → a → b) → b → List a → List b
+scanl f z []       = z ∷ []
+scanl f z (x ∷ xs) = z ∷ scanl f (f z x) xs
+
+scanr : (a → b → b) → b → List a → List b
+scanr f z [] = z ∷ []
+scanr f z (x ∷ xs) =
+  case scanr f z xs of λ where
+    []         → [] -- impossible
+    qs@(q ∷ _) → f x q ∷ qs
+
+scanl1 : (a → a → a) → List a → List a
+scanl1 f []       = []
+scanl1 f (x ∷ xs) = scanl f x xs
+
+scanr1 : (a → a → a) → List a → List a
+scanr1 f []       = []
+scanr1 f (x ∷ []) = x ∷ []
+scanr1 f (x ∷ xs) =
+  case scanr1 f xs of λ where
+    []         → [] -- impossible
+    qs@(q ∷ _) → f x q ∷ qs
+
+takeWhile : (a → Bool) → List a → List a
+takeWhile p [] = []
+takeWhile p (x ∷ xs) = if p x then x ∷ takeWhile p xs else []
+
+dropWhile : (a → Bool) → List a → List a
+dropWhile p [] = []
+dropWhile p (x ∷ xs) = if p x then dropWhile p xs else x ∷ xs
+
+span : (a → Bool) → List a → List a × List a
+span p [] = [] , []
+span p (x ∷ xs) = if p x then first (x ∷_) (span p xs)
+                         else ([] , x ∷ xs)
+
+break : (a → Bool) → List a → List a × List a
+break p = span (not ∘ p)
+
+zipWith : (a → b → c) → List a → List b → List c
+zipWith f []       _        = []
+zipWith f _        []       = []
+zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
+
+zip : List a → List b → List (a × b)
+zip = zipWith _,_
+
+zipWith3 : (a → b → c → d) → List a → List b → List c → List d
+zipWith3 f []       _        _        = []
+zipWith3 f _        []       _        = []
+zipWith3 f _        _        []       = []
+zipWith3 f (x ∷ xs) (y ∷ ys) (z ∷ zs) = f x y z ∷ zipWith3 f xs ys zs
+
+zip3 : List a → List b → List c → List (a × b × c)
+zip3 = zipWith3 _,_,_
+
+unzip : List (a × b) → List a × List b
+unzip []              = [] , []
+unzip ((x , y) ∷ xys) = (x ∷_) *** (y ∷_) $ unzip xys
+
+unzip3 : List (a × b × c) → List a × List b × List c
+unzip3 []                   = [] , [] , []
+unzip3 ((x , y , z) ∷ xyzs) =
+  case unzip3 xyzs of λ where
+    (xs , ys , zs) → x ∷ xs , y ∷ ys , z ∷ zs
+
+takeNat : Nat → List a → List a
+takeNat n       [] = []
+takeNat zero    xs = []
+takeNat (suc n) (x ∷ xs) = x ∷ takeNat n xs
+
+take : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a
+take n xs = takeNat (intToNat n) xs
+
+dropNat : Nat → List a → List a
+dropNat n       [] = []
+dropNat zero    xs = xs
+dropNat (suc n) (_ ∷ xs) = dropNat n xs
+
+drop : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a
+drop n xs = dropNat (intToNat n) xs
+
+splitAtNat : (n : Nat) → List a → List a × List a
+splitAtNat _       []       = [] , []
+splitAtNat 0       xs       = [] , xs
+splitAtNat (suc n) (x ∷ xs) = first (x ∷_) (splitAtNat n xs)
+
+splitAt : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a × List a
+splitAt n xs = splitAtNat (intToNat n) xs
+
+head : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a
+head (x ∷ _) = x
+
+tail : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a
+tail (_ ∷ xs) = xs
+
+last : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a
+last (x ∷ [])         = x
+last (_ ∷ xs@(_ ∷ _)) = last xs
+
+init : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a
+init (x ∷ [])         = []
+init (x ∷ xs@(_ ∷ _)) = x ∷ init xs
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Maybe.html b/lib/Haskell.Prim.Maybe.html new file mode 100644 index 00000000..e0cd83ca --- /dev/null +++ b/lib/Haskell.Prim.Maybe.html @@ -0,0 +1,19 @@ + +Haskell.Prim.Maybe
+module Haskell.Prim.Maybe where
+
+--------------------------------------------------
+-- Maybe
+
+data Maybe {@0 ℓ} (a : Set ℓ) : Set ℓ where
+  Nothing : Maybe a
+  Just    : a -> Maybe a
+
+maybe : ∀ {@0 ℓ₁ ℓ₂} {@0 a : Set ℓ₁} {@0 b : Set ℓ₂} → b → (a → b) → Maybe a → b
+maybe n j Nothing  = n
+maybe n j (Just x) = j x
+
+fromMaybe : {a : Set} → a → Maybe a → a
+fromMaybe d Nothing = d
+fromMaybe _ (Just x) = x
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Monad.html b/lib/Haskell.Prim.Monad.html new file mode 100644 index 00000000..b39a38fb --- /dev/null +++ b/lib/Haskell.Prim.Monad.html @@ -0,0 +1,131 @@ + +Haskell.Prim.Monad
+module Haskell.Prim.Monad where
+
+open import Haskell.Prim
+open import Haskell.Prim.Applicative
+open import Haskell.Prim.Either
+open import Haskell.Prim.Foldable
+open import Haskell.Prim.Functor
+open import Haskell.Prim.IO
+open import Haskell.Prim.List
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Monoid
+open import Haskell.Prim.String
+open import Haskell.Prim.Tuple
+
+--------------------------------------------------
+-- Monad
+
+module Do where
+
+  -- ** base
+  record Monad (m : Set → Set) : Set₁ where
+    field
+      _>>=_ : m a → (a → m b) → m b
+      overlap ⦃ super ⦄ : Applicative m
+      return : a → m a
+      _>>_ : m a → (@0 {{ a }} → m b) → m b
+  -- ** defaults
+  record DefaultMonad (m : Set → Set) : Set₁ where
+    field
+      _>>=_ : m a → (a → m b) → m b
+      overlap ⦃ super ⦄ : Applicative m
+    return : a → m a
+    return = pure
+
+    _>>_ : m a → (@0 {{ a }} → m b) → m b
+    m >> m₁ = m >>= λ x → m₁ {{x}}
+
+  -- ** export
+  open Monad ⦃...⦄ public
+  {-# COMPILE AGDA2HS Monad existing-class #-}
+
+-- Use `Dont._>>=_` and `Dont._>>_` if you do not want agda2hs to use
+-- do-notation.
+module Dont where
+
+  open Do using (Monad)
+
+  _>>=_ : ⦃ Monad m ⦄ → m a → (a → m b) → m b
+  _>>=_ = Do._>>=_
+
+  _>>_ : ⦃ Monad m ⦄ → m a → (@0 {{ a }} → m b) → m b
+  _>>_ = Do._>>_
+
+open Do public
+
+_=<<_ : {{Monad m}} → (a → m b) → m a → m b
+_=<<_ = flip _>>=_
+
+mapM₋ : ⦃ Monad m ⦄ → ⦃ Foldable t ⦄ → (a → m b) → t a → m ⊤
+mapM₋ f = foldr (λ x k → f x >> k) (pure tt)
+
+sequence₋ : ⦃ Monad m ⦄ → ⦃ Foldable t ⦄ → t (m a) → m ⊤
+sequence₋ = foldr (λ mx my → mx >> my) (pure tt)
+
+-- ** instances
+private
+  mkMonad : DefaultMonad t → Monad t
+  mkMonad x = record {DefaultMonad x}
+
+  infix 0 bind=_
+  bind=_ : ⦃ Applicative m ⦄ → (∀ {a b} → m a → (a → m b) → m b) → Monad m
+  bind= x = record {DefaultMonad (record {_>>=_ = x})}
+instance
+  iDefaultMonadList : DefaultMonad List
+  iDefaultMonadList .DefaultMonad._>>=_ = flip concatMap
+
+  iMonadList : Monad List
+  iMonadList = record {DefaultMonad iDefaultMonadList}
+
+  iDefaultMonadMaybe : DefaultMonad Maybe
+  iDefaultMonadMaybe .DefaultMonad._>>=_ = flip (maybe Nothing)
+
+  iMonadMaybe : Monad Maybe
+  iMonadMaybe = record {DefaultMonad iDefaultMonadMaybe}
+
+  iDefaultMonadEither : DefaultMonad (Either a)
+  iDefaultMonadEither .DefaultMonad._>>=_ = flip (either Left)
+
+  iMonadEither : Monad (Either a)
+  iMonadEither = record {DefaultMonad iDefaultMonadEither}
+
+  iDefaultMonadFun : DefaultMonad (λ b → a → b)
+  iDefaultMonadFun .DefaultMonad._>>=_ = λ f k r → k (f r) r
+
+  iMonadFun : Monad (λ b → a → b)
+  iMonadFun = record {DefaultMonad iDefaultMonadFun}
+
+  iDefaultMonadTuple₂ : ⦃ Monoid a ⦄ → DefaultMonad (a ×_)
+  iDefaultMonadTuple₂ .DefaultMonad._>>=_ = λ (a , x) k → first (a <>_) (k x)
+
+  iMonadTuple₂ : ⦃ Monoid a ⦄ → Monad (a ×_)
+  iMonadTuple₂ = record {DefaultMonad iDefaultMonadTuple₂}
+
+  iDefaultMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonad (a × b ×_)
+  iDefaultMonadTuple₃ .DefaultMonad._>>=_ = λ where
+    (a , b , x) k → case k x of λ where
+      (a₁ , b₁ , y) → a <> a₁ , b <> b₁ , y
+
+  iMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_)
+  iMonadTuple₃ = record {DefaultMonad iDefaultMonadTuple₃}
+
+instance postulate iMonadIO : Monad IO
+
+record MonadFail (m : Set → Set) : Set₁ where
+  field
+    fail : String → m a
+    overlap ⦃ super ⦄ : Monad m
+
+open MonadFail ⦃...⦄ public
+
+{-# COMPILE AGDA2HS MonadFail existing-class #-}
+
+instance
+  MonadFailList : MonadFail List
+  MonadFailList .fail _ = []
+
+  MonadFailMaybe : MonadFail Maybe
+  MonadFailMaybe .fail _ = Nothing
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Monoid.html b/lib/Haskell.Prim.Monoid.html new file mode 100644 index 00000000..caa4ce8d --- /dev/null +++ b/lib/Haskell.Prim.Monoid.html @@ -0,0 +1,132 @@ + +Haskell.Prim.Monoid
+module Haskell.Prim.Monoid where
+
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+open import Haskell.Prim.List
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Either
+open import Haskell.Prim.Tuple
+
+--------------------------------------------------
+-- Semigroup
+
+record Semigroup (a : Set) : Set where
+  infixr 6 _<>_
+  field _<>_ : a → a → a
+open Semigroup ⦃...⦄ public
+{-# COMPILE AGDA2HS Semigroup existing-class #-}
+
+instance
+  iSemigroupList : Semigroup (List a)
+  iSemigroupList ._<>_ = _++_
+
+  iSemigroupMaybe : ⦃ Semigroup a ⦄ → Semigroup (Maybe a)
+  iSemigroupMaybe ._<>_          Nothing m = m
+  iSemigroupMaybe ._<>_ m        Nothing   = m
+  iSemigroupMaybe ._<>_ (Just x) (Just y)  = Just (x <> y)
+
+  iSemigroupEither : Semigroup (Either a b)
+  iSemigroupEither ._<>_ (Left _) e = e
+  iSemigroupEither ._<>_ e        _ = e
+
+  iSemigroupFun : ⦃ Semigroup b ⦄ → Semigroup (a → b)
+  iSemigroupFun ._<>_ f g x = f x <> g x
+
+  iSemigroupUnit : Semigroup ⊤
+  iSemigroupUnit ._<>_ _ _ = tt
+
+
+  iSemigroupTuple₂ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → Semigroup (a × b)
+  iSemigroupTuple₂ ._<>_ (x₁ , y₁) (x₂ , y₂) = x₁ <> x₂ , y₁ <> y₂
+
+  iSemigroupTuple₃ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → ⦃ Semigroup c ⦄ → Semigroup (a × b × c)
+  iSemigroupTuple₃ ._<>_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ <> x₂ , y₁ <> y₂ , z₁ <> z₂
+
+
+--------------------------------------------------
+-- Monoid
+
+-- ** base
+record Monoid (a : Set) : Set where
+  field
+    mempty : a
+    overlap ⦃ super ⦄ : Semigroup a
+    mappend : a → a → a
+    mconcat : List a → a
+-- ** defaults
+record DefaultMonoid (a : Set) : Set where
+  field
+    mempty : a
+    overlap ⦃ super ⦄ : Semigroup a
+
+  mappend : a → a → a
+  mappend = _<>_
+
+  mconcat : List a → a
+  mconcat []       = mempty
+  mconcat (x ∷ xs) = x <> mconcat xs
+-- ** export
+open Monoid ⦃...⦄ public
+{-# COMPILE AGDA2HS Monoid existing-class #-}
+-- ** instances
+instance
+  iDefaultMonoidList : DefaultMonoid (List a)
+  iDefaultMonoidList .DefaultMonoid.mempty = []
+
+  iMonoidList : Monoid (List a)
+  iMonoidList = record{DefaultMonoid iDefaultMonoidList}
+
+  iDefaultMonoidMaybe : ⦃ Semigroup a ⦄ → DefaultMonoid (Maybe a)
+  iDefaultMonoidMaybe .DefaultMonoid.mempty = Nothing
+
+  iMonoidMaybe : ⦃ Semigroup a ⦄ → Monoid (Maybe a)
+  iMonoidMaybe = record{DefaultMonoid iDefaultMonoidMaybe}
+
+  iDefaultMonoidFun : ⦃ Monoid b ⦄ → DefaultMonoid (a → b)
+  iDefaultMonoidFun .DefaultMonoid.mempty = λ _ → mempty
+
+  iMonoidFun : ⦃ Monoid b ⦄ → Monoid (a → b)
+  iMonoidFun = record{DefaultMonoid iDefaultMonoidFun}
+
+  iDefaultMonoidUnit : DefaultMonoid ⊤
+  iDefaultMonoidUnit .DefaultMonoid.mempty = tt
+
+  iMonoidUnit : Monoid ⊤
+  iMonoidUnit = record{DefaultMonoid iDefaultMonoidUnit}
+
+  iDefaultMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonoid (a × b)
+  iDefaultMonoidTuple₂ .DefaultMonoid.mempty = (mempty , mempty)
+
+  iMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monoid (a × b)
+  iMonoidTuple₂ = record{DefaultMonoid iDefaultMonoidTuple₂}
+
+  iDefaultMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ → DefaultMonoid (a × b × c)
+  iDefaultMonoidTuple₃ .DefaultMonoid.mempty = (mempty , mempty , mempty)
+
+  iMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ →  Monoid (a × b × c)
+  iMonoidTuple₃ = record{DefaultMonoid iDefaultMonoidTuple₃}
+
+open DefaultMonoid
+
+MonoidEndo : Monoid (a → a)
+MonoidEndo = record {DefaultMonoid (λ where
+      .mempty → id
+      .super ._<>_ → _∘_)}
+
+MonoidEndoᵒᵖ : Monoid (a → a)
+MonoidEndoᵒᵖ = record {DefaultMonoid (λ where
+  .mempty      → id
+  .super ._<>_ → flip _∘_) }
+
+MonoidConj : Monoid Bool
+MonoidConj = record {DefaultMonoid (λ where
+  .mempty      → True
+  .super ._<>_ → _&&_)}
+
+MonoidDisj : Monoid Bool
+MonoidDisj = record {DefaultMonoid (λ where
+  .mempty      → False
+  .super ._<>_ → _||_)}
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Num.html b/lib/Haskell.Prim.Num.html new file mode 100644 index 00000000..dc1fb841 --- /dev/null +++ b/lib/Haskell.Prim.Num.html @@ -0,0 +1,122 @@ + +Haskell.Prim.Num
{-# OPTIONS --no-auto-inline #-}
+
+module Haskell.Prim.Num where
+
+open import Haskell.Prim
+open import Haskell.Prim.Word
+open import Haskell.Prim.Int
+open import Haskell.Prim.Integer
+open import Haskell.Prim.Double
+open import Haskell.Prim.Eq
+open import Haskell.Prim.Ord
+open import Haskell.Prim.Monoid
+
+--------------------------------------------------
+-- Num
+
+record Num (a : Set) : Set₁ where
+  infixl 6 _+_ _-_
+  infixl 7 _*_
+  field
+    @0 MinusOK       : a → a → Set
+    @0 NegateOK      : a → Set
+    @0 FromIntegerOK : Integer → Set
+    _+_           : a → a → a
+    _-_           : (x y : a) → @0 ⦃ MinusOK x y ⦄ → a
+    _*_           : a → a → a
+    negate        : (x : a) → @0 ⦃ NegateOK x ⦄ → a
+    abs           : a → a
+    signum        : a → a
+    fromInteger   : (n : Integer) → @0 ⦃ FromIntegerOK n ⦄ → a
+    overlap ⦃ number ⦄  : Number a
+    overlap ⦃ numZero ⦄ : number .Number.Constraint 0
+    overlap ⦃ numOne ⦄  : number .Number.Constraint 1
+
+open Num ⦃...⦄ public hiding (FromIntegerOK; number)
+
+{-# COMPILE AGDA2HS Num existing-class #-}
+
+instance
+  iNumNat : Num Nat
+  iNumNat .MinusOK n m      = IsFalse (ltNat n m)
+  iNumNat .NegateOK 0       = ⊤
+  iNumNat .NegateOK (suc _) = ⊥
+  iNumNat .Num.FromIntegerOK (negsuc _) = ⊥
+  iNumNat .Num.FromIntegerOK (pos _) = ⊤
+  iNumNat ._+_ n m = addNat n m
+  iNumNat ._-_ n m = monusNat n m
+  iNumNat ._*_ n m = mulNat n m
+  iNumNat .negate n = n
+  iNumNat .abs    n = n
+  iNumNat .signum 0       = 0
+  iNumNat .signum (suc n) = 1
+  iNumNat .fromInteger (pos n) = n
+  iNumNat .fromInteger (negsuc _) ⦃ () ⦄
+
+  iNumInt : Num Int
+  iNumInt .MinusOK _ _         = ⊤
+  iNumInt .NegateOK _          = ⊤
+  iNumInt .Num.FromIntegerOK _ = ⊤
+  iNumInt ._+_ x y             = addInt x y
+  iNumInt ._-_ x y             = subInt x y
+  iNumInt ._*_ x y             = mulInt x y
+  iNumInt .negate x            = negateInt x
+  iNumInt .abs x               = absInt x
+  iNumInt .signum x            = signInt x
+  iNumInt .fromInteger n       = integerToInt n
+
+  iNumInteger : Num Integer
+  iNumInteger .MinusOK _ _ = ⊤
+  iNumInteger .NegateOK _          = ⊤
+  iNumInteger .Num.FromIntegerOK _ = ⊤
+  iNumInteger ._+_ x y             = addInteger x y
+  iNumInteger ._-_ x y             = subInteger x y
+  iNumInteger ._*_ x y             = mulInteger x y
+  iNumInteger .negate x            = negateInteger x
+  iNumInteger .abs x               = absInteger x
+  iNumInteger .signum x            = signInteger x
+  iNumInteger .fromInteger n       = n
+
+  iNumWord : Num Word
+  iNumWord .MinusOK _ _         = ⊤
+  iNumWord .NegateOK _          = ⊤
+  iNumWord .Num.FromIntegerOK _ = ⊤
+  iNumWord ._+_ x y             = addWord x y
+  iNumWord ._-_ x y             = subWord x y
+  iNumWord ._*_ x y             = mulWord x y
+  iNumWord .negate x            = negateWord x
+  iNumWord .abs x               = x
+  iNumWord .signum x            = if x == 0 then 0 else 1
+  iNumWord .fromInteger n       = integerToWord n
+
+  iNumDouble : Num Double
+  iNumDouble .MinusOK _ _         = ⊤
+  iNumDouble .NegateOK _          = ⊤
+  iNumDouble .Num.FromIntegerOK _ = ⊤
+  iNumDouble ._+_ x y             = primFloatPlus x y
+  iNumDouble ._-_ x y             = primFloatMinus x y
+  iNumDouble ._*_ x y             = primFloatTimes x y
+  iNumDouble .negate x            = primFloatMinus 0.0 x
+  iNumDouble .abs x               = if x < 0.0 then primFloatMinus 0.0 x else x
+  iNumDouble .signum x            = case compare x 0.0 of λ where
+                                      LT → -1.0
+                                      EQ → x
+                                      GT → 1.0
+  iNumDouble .fromInteger (pos    n) = fromNat n
+  iNumDouble .fromInteger (negsuc n) = fromNeg (suc n)
+
+open DefaultMonoid
+
+MonoidSum : ⦃ iNum : Num a ⦄ → Monoid a
+MonoidSum = record {DefaultMonoid (λ where
+  .mempty      → 0
+  .super ._<>_ → _+_
+ )}
+
+MonoidProduct : ⦃ iNum : Num a ⦄ → Monoid a
+MonoidProduct = record {DefaultMonoid (λ where
+  .mempty      → 1
+  .super ._<>_ → _*_
+ )}
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Ord.html b/lib/Haskell.Prim.Ord.html new file mode 100644 index 00000000..275bf593 --- /dev/null +++ b/lib/Haskell.Prim.Ord.html @@ -0,0 +1,236 @@ + +Haskell.Prim.Ord
+module Haskell.Prim.Ord where
+
+open import Haskell.Prim
+open import Haskell.Prim.Eq
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Int
+open import Haskell.Prim.Word
+open import Haskell.Prim.Integer
+open import Haskell.Prim.Double
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Monoid
+open import Haskell.Prim.List
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Either
+
+--------------------------------------------------
+-- Ordering
+
+data Ordering : Set where
+  LT EQ GT : Ordering
+
+instance
+  iEqOrdering : Eq Ordering
+  iEqOrdering ._==_ LT LT = True
+  iEqOrdering ._==_ EQ EQ = True
+  iEqOrdering ._==_ GT GT = True
+  iEqOrdering ._==_ _  _  = False
+
+  iSemigroupOrdering : Semigroup Ordering
+  iSemigroupOrdering ._<>_ LT _ = LT
+  iSemigroupOrdering ._<>_ EQ o = o
+  iSemigroupOrdering ._<>_ GT _ = GT
+
+  iMonoidOrdering : Monoid Ordering
+  iMonoidOrdering = record {DefaultMonoid (record {mempty = EQ})}
+
+--------------------------------------------------
+-- Ord
+
+record Ord (a : Set) : Set where
+  field
+    compare : a → a → Ordering
+    _<_  : a → a → Bool
+    _>_  : a → a → Bool
+    _>=_ : a → a → Bool
+    _<=_ : a → a → Bool
+    max  : a → a → a
+    min  : a → a → a
+    overlap ⦃ super ⦄ : Eq a
+
+  infix 4 _<_ _>_ _<=_ _>=_
+
+record OrdFromCompare (a : Set) : Set where
+  field
+    compare : a → a → Ordering
+    overlap ⦃ super ⦄ : Eq a
+
+  _<_  : a → a → Bool
+  x < y = compare x y == LT
+
+  _>_  : a → a → Bool
+  x > y = compare x y == GT
+
+  _>=_ : a → a → Bool
+  x >= y = compare x y /= LT
+
+  _<=_ : a → a → Bool
+  x <= y = compare x y /= GT
+
+  max  : a → a → a
+  max x y = if compare x y == LT then y else x
+
+  min  : a → a → a
+  min x y = if compare x y == GT then y else x
+
+record OrdFromLessThan (a : Set) : Set where
+  field
+    _<_ : a → a → Bool
+    overlap ⦃ super ⦄ : Eq a
+
+  compare : a → a → Ordering
+  compare x y = if x < y then LT else if x == y then EQ else GT
+
+  _>_  : a → a → Bool
+  x > y = y < x
+
+  _>=_ : a → a → Bool
+  x >= y = y < x || x == y
+
+  _<=_ : a → a → Bool
+  x <= y = x < y || x == y
+
+  max  : a → a → a
+  max x y = if x < y then y else x
+
+  min  : a → a → a
+  min x y = if y < x then y else x
+
+
+open Ord ⦃...⦄ public
+
+{-# COMPILE AGDA2HS Ord existing-class #-}
+
+private
+  compareFromLt : ⦃ Eq a ⦄ → (a → a → Bool) → a → a → Ordering
+  compareFromLt _<_ x y = if x < y then LT else if x == y then EQ else GT
+
+private
+  maxNat : Nat → Nat → Nat
+  maxNat zero    y       = y
+  maxNat (suc x) zero    = suc x
+  maxNat (suc x) (suc y) = suc (maxNat x y)
+
+  minNat : Nat → Nat → Nat
+  minNat zero    y       = zero
+  minNat (suc x) zero    = zero
+  minNat (suc x) (suc y) = suc (minNat x y)
+
+instance
+  iOrdFromLessThanNat : OrdFromLessThan Nat
+  iOrdFromLessThanNat .OrdFromLessThan._<_ = ltNat
+
+  iOrdNat : Ord Nat
+  iOrdNat = record
+    { OrdFromLessThan iOrdFromLessThanNat
+    ; max = maxNat
+    ; min = minNat
+    }
+
+  iOrdFromLessThanInteger : OrdFromLessThan Integer
+  iOrdFromLessThanInteger .OrdFromLessThan._<_ = ltInteger
+
+  iOrdInteger : Ord Integer
+  iOrdInteger = record {OrdFromLessThan iOrdFromLessThanInteger}
+
+  iOrdFromLessThanInt : OrdFromLessThan Int
+  iOrdFromLessThanInt .OrdFromLessThan._<_ = ltInt
+
+  iOrdInt : Ord Int
+  iOrdInt = record {OrdFromLessThan iOrdFromLessThanInt}
+
+  iOrdFromLessThanWord : OrdFromLessThan Word
+  iOrdFromLessThanWord .OrdFromLessThan._<_ = ltWord
+
+  iOrdWord : Ord Word
+  iOrdWord = record {OrdFromLessThan iOrdFromLessThanWord}
+
+  iOrdFromLessThanDouble : OrdFromLessThan Double
+  iOrdFromLessThanDouble .OrdFromLessThan._<_ = primFloatLess
+
+  iOrdDouble : Ord Double
+  iOrdDouble = record {OrdFromLessThan iOrdFromLessThanDouble}
+
+  iOrdFromLessThanChar : OrdFromLessThan Char
+  iOrdFromLessThanChar .OrdFromLessThan._<_ x y = c2n x < c2n y
+
+  iOrdChar : Ord Char
+  iOrdChar = record {OrdFromLessThan iOrdFromLessThanChar}
+
+  iOrdFromCompareBool : OrdFromCompare Bool
+  iOrdFromCompareBool .OrdFromCompare.compare = λ where
+    False True  → LT
+    True  False → GT
+    _     _     → EQ
+
+  iOrdBool : Ord Bool
+  iOrdBool = record {OrdFromCompare iOrdFromCompareBool}
+
+  iOrdFromCompareUnit : OrdFromCompare ⊤
+  iOrdFromCompareUnit .OrdFromCompare.compare = λ _ _ → EQ
+
+  iOrdUnit : Ord ⊤
+  iOrdUnit = record {OrdFromCompare iOrdFromCompareUnit}
+
+  iOrdFromCompareTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → OrdFromCompare (a × b)
+  iOrdFromCompareTuple₂ .OrdFromCompare.compare = λ where
+    (x₁ , y₁) (x₂ , y₂) → compare x₁ x₂ <> compare y₁ y₂
+
+  iOrdTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (a × b)
+  iOrdTuple₂ = record {OrdFromCompare iOrdFromCompareTuple₂}
+
+  iOrdFromCompareTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → OrdFromCompare (a × b × c)
+  iOrdFromCompareTuple₃ .OrdFromCompare.compare = λ where
+    (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) → compare x₁ x₂ <> compare y₁ y₂ <> compare z₁ z₂
+
+  iOrdTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → Ord (a × b × c)
+  iOrdTuple₃ = record {OrdFromCompare iOrdFromCompareTuple₃}
+
+compareList : ⦃ Ord a ⦄ → List a → List a → Ordering
+compareList []       []       = EQ
+compareList []       (_ ∷ _)  = LT
+compareList (_ ∷ _)  []       = GT
+compareList (x ∷ xs) (y ∷ ys) = compare x y <> compareList xs ys
+
+instance
+  iOrdFromCompareList : ⦃ Ord a ⦄ → OrdFromCompare (List a)
+  iOrdFromCompareList .OrdFromCompare.compare = compareList
+
+  iOrdList : ⦃ Ord a ⦄ → Ord (List a)
+  iOrdList = record {OrdFromCompare iOrdFromCompareList}
+
+  iOrdFromCompareMaybe : ⦃ Ord a ⦄ → OrdFromCompare (Maybe a)
+  iOrdFromCompareMaybe .OrdFromCompare.compare = λ where
+    Nothing  Nothing  → EQ
+    Nothing  (Just _) → LT
+    (Just _) Nothing  → GT
+    (Just x) (Just y) → compare x y
+
+  iOrdMaybe : ⦃ Ord a ⦄ → Ord (Maybe a)
+  iOrdMaybe = record {OrdFromCompare iOrdFromCompareMaybe}
+
+  iOrdFromCompareEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → OrdFromCompare (Either a b)
+  iOrdFromCompareEither .OrdFromCompare.compare = λ where
+    (Left  x) (Left  y) → compare x y
+    (Left  _) (Right _) → LT
+    (Right _) (Left  _) → GT
+    (Right x) (Right y) → compare x y
+
+  iOrdEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (Either a b)
+  iOrdEither = record {OrdFromCompare iOrdFromCompareEither}
+
+  iOrdFromCompareOrdering : OrdFromCompare Ordering
+  iOrdFromCompareOrdering .OrdFromCompare.compare = λ where
+    LT LT → EQ
+    LT _  → LT
+    _  LT → GT
+    EQ EQ → EQ
+    EQ GT → LT
+    GT EQ → GT
+    GT GT → EQ
+
+  iOrdOrdering : Ord Ordering
+  iOrdOrdering = record {OrdFromCompare iOrdFromCompareOrdering}
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Show.html b/lib/Haskell.Prim.Show.html new file mode 100644 index 00000000..cca2ad82 --- /dev/null +++ b/lib/Haskell.Prim.Show.html @@ -0,0 +1,161 @@ + +Haskell.Prim.Show
+module Haskell.Prim.Show where
+
+open import Haskell.Prim
+open import Haskell.Prim.String
+open import Haskell.Prim.List
+open import Haskell.Prim.Word
+open import Haskell.Prim.Double
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Eq
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Ord
+open import Haskell.Prim.Either
+open import Haskell.Prim.Integer
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Int
+open import Haskell.Prim.Foldable
+
+
+--------------------------------------------------
+-- Show
+
+ShowS : Set
+ShowS = String → String
+
+showChar : Char → ShowS
+showChar = _∷_
+
+showString : String → ShowS
+showString = _++_
+
+showParen : Bool → ShowS → ShowS
+showParen False s = s
+showParen True  s = showString "(" ∘ s ∘ showString ")"
+
+defaultShowList : (a → ShowS) → List a → ShowS
+defaultShowList shows = λ where
+  []       → showString "[]"
+  (x ∷ xs) → showString "["
+           ∘ foldl (λ s x → s ∘ showString "," ∘ shows x) (shows x) xs
+           ∘ showString "]"
+
+-- ** base
+record Show (a : Set) : Set where
+  field
+    showsPrec : Int → a → ShowS
+    showList  : List a → ShowS
+    show      : a → String
+-- ** export
+record Show₁ (a : Set) : Set where
+  field showsPrec : Int → a → ShowS
+
+  show : a → String
+  show x = showsPrec 0 x ""
+
+  showList : List a → ShowS
+  showList = defaultShowList (showsPrec 0)
+record Show₂ (a : Set) : Set where
+  field show : a → String
+
+  showsPrec : Int → a → ShowS
+  showsPrec _ x s = show x ++ s
+
+  showList : List a → ShowS
+  showList = defaultShowList (showsPrec 0)
+-- ** export
+open Show ⦃...⦄ public
+
+shows : ⦃ Show a ⦄ → a → ShowS
+shows = showsPrec 0
+
+{-# COMPILE AGDA2HS Show existing-class #-}
+
+-- ** instances
+instance
+  iShow₂Nat : Show₂ Nat
+  iShow₂Nat .Show₂.show = primStringToList ∘ primShowNat
+
+  iShowNat : Show Nat
+  iShowNat = record {Show₂ iShow₂Nat}
+
+  iShow₂Integer : Show₂ Integer
+  iShow₂Integer .Show₂.show = showInteger
+
+  iShowInteger : Show Integer
+  iShowInteger = record {Show₂ iShow₂Integer}
+
+  iShow₂Int : Show₂ Int
+  iShow₂Int .Show₂.show = showInt
+
+  iShowInt : Show Int
+  iShowInt = record{Show₂ iShow₂Int}
+
+  iShow₂Word : Show₂ Word
+  iShow₂Word .Show₂.show = showWord
+
+  iShowWord : Show Word
+  iShowWord = record{Show₂ iShow₂Word}
+
+  iShow₂Double : Show₂ Double
+  iShow₂Double .Show₂.show = primStringToList ∘ primShowFloat
+
+  iShowDouble : Show Double
+  iShowDouble = record{Show₂ iShow₂Double}
+
+  iShow₂Bool : Show₂ Bool
+  iShow₂Bool .Show₂.show = λ where False → "False"; True → "True"
+
+  iShowBool : Show Bool
+  iShowBool = record{Show₂ iShow₂Bool}
+
+  iShow₁Char : Show₁ Char
+  iShow₁Char .Show₁.showsPrec _ = showString ∘ primStringToList ∘ primShowChar
+
+  iShowChar : Show Char
+  iShowChar = record{Show₁ iShow₁Char}
+
+  iShow₁List : ⦃ Show a ⦄ → Show₁ (List a)
+  iShow₁List .Show₁.showsPrec _ = showList
+
+  iShowList : ⦃ Show a ⦄ → Show (List a)
+  iShowList = record{Show₁ iShow₁List}
+
+private
+  showApp₁ : ⦃ Show a ⦄ → Int → String → a → ShowS
+  showApp₁ p tag x = showParen (p > 10) $
+    showString tag ∘ showString " " ∘ showsPrec 11 x
+
+instance
+  iShow₁Maybe : ⦃ Show a ⦄ → Show₁ (Maybe a)
+  iShow₁Maybe .Show₁.showsPrec = λ where
+    p Nothing  → showString "Nothing"
+    p (Just x) → showApp₁ p "Just" x
+
+  iShowMaybe : ⦃ Show a ⦄ → Show (Maybe a)
+  iShowMaybe = record{Show₁ iShow₁Maybe}
+
+  iShow₁Either : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show₁ (Either a b)
+  iShow₁Either .Show₁.showsPrec = λ where
+    p (Left  x) → showApp₁ p "Left"  x
+    p (Right y) → showApp₁ p "Right" y
+
+  iShowEither : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (Either a b)
+  iShowEither = record{Show₁ iShow₁Either}
+
+instance
+  iShow₁Tuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show₁ (a × b)
+  iShow₁Tuple₂ .Show₁.showsPrec = λ _ → λ where
+    (x , y) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ")"
+
+  iShowTuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (a × b)
+  iShowTuple₂ = record{Show₁ iShow₁Tuple₂}
+
+  iShow₁Tuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show₁ (a × b × c)
+  iShow₁Tuple₃ .Show₁.showsPrec = λ _ → λ where
+    (x , y , z) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ", " ∘ shows z ∘ showString ")"
+
+  iShowTuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show (a × b × c)
+  iShowTuple₃ = record{Show₁ iShow₁Tuple₃}
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.String.html b/lib/Haskell.Prim.String.html new file mode 100644 index 00000000..a8ce00a4 --- /dev/null +++ b/lib/Haskell.Prim.String.html @@ -0,0 +1,54 @@ + +Haskell.Prim.String
+module Haskell.Prim.String where
+
+open import Haskell.Prim
+open import Haskell.Prim.List
+open import Haskell.Prim.Foldable
+
+--------------------------------------------------
+-- String
+-- This is _not_ the builtin String type of Agda
+-- which is defined by postulates.
+-- `fromString` can be used to convert back
+-- to builtin Agda strings.
+
+String = List Char
+
+instance
+  iIsStringString : IsString String
+  iIsStringString .IsString.Constraint _ = ⊤
+  iIsStringString .fromString s = primStringToList s
+
+private
+  cons : Char → List String → List String
+  cons c []       = (c ∷ []) ∷ []
+  cons c (s ∷ ss) = (c ∷ s) ∷ ss
+
+lines : String → List String
+lines []         = []
+lines ('\n' ∷ s) = [] ∷ lines s
+lines (c    ∷ s) = cons c (lines s)
+
+private
+ mutual
+  space : String → List String
+  space [] = []
+  space (c ∷ s) = if primIsSpace c then space s else cons c (word s)
+
+  word  : String → List String
+  word []      = []
+  word (c ∷ s) = if primIsSpace c then [] ∷ space s else cons c (word s)
+
+words : String → List String
+words [] = []
+words s@(c ∷ s₁) = if primIsSpace c then space s₁ else word s
+
+unlines : List String → String
+unlines = concatMap (_++ "\n")
+
+unwords : List String → String
+unwords [] = ""
+unwords (w ∷ []) = w
+unwords (w ∷ ws) = w ++ ' ' ∷ unwords ws
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Traversable.html b/lib/Haskell.Prim.Traversable.html new file mode 100644 index 00000000..6fe2d59b --- /dev/null +++ b/lib/Haskell.Prim.Traversable.html @@ -0,0 +1,80 @@ + +Haskell.Prim.Traversable
+
+module Haskell.Prim.Traversable where
+
+open import Haskell.Prim
+open import Haskell.Prim.Applicative
+open import Haskell.Prim.Functor
+open import Haskell.Prim.Foldable
+open import Haskell.Prim.Monad
+open import Haskell.Prim.List
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Either
+open import Haskell.Prim.Tuple
+
+--------------------------------------------------
+-- Traversable
+
+-- ** base
+record Traversable (t : Set → Set) : Set₁ where
+  field
+    traverse : ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b)
+    overlap ⦃ functor ⦄ : Functor t
+    overlap ⦃ foldable ⦄ : Foldable t
+
+    sequenceA : ⦃ Applicative f ⦄ → t (f a) → f (t a)
+    mapM : ⦃ Monad m ⦄ → (a → m b) → t a → m (t b)
+    sequence : ⦃ Monad m ⦄ → t (m a) → m (t a)
+-- ** defaults
+record DefaultTraversable (t : Set → Set) : Set₁ where
+  field
+    traverse : ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b)
+    overlap ⦃ functor ⦄ : Functor t
+    overlap ⦃ foldable ⦄ : Foldable t
+
+  sequenceA : ⦃ Applicative f ⦄ → t (f a) → f (t a)
+  sequenceA = traverse id
+
+  mapM : ⦃ Monad m ⦄ → (a → m b) → t a → m (t b)
+  mapM = traverse
+
+  sequence : ⦃ Monad m ⦄ → t (m a) → m (t a)
+  sequence = sequenceA
+-- ** export
+open Traversable ⦃...⦄ public
+{-# COMPILE AGDA2HS Traversable existing-class #-}
+-- ** instances
+private
+  mkTraversable : DefaultTraversable t → Traversable t
+  mkTraversable x = record {DefaultTraversable x}
+
+  infix 0 traverse=_
+  traverse=_ : ⦃ Functor t ⦄ → ⦃ Foldable t ⦄
+            → (∀ {f a b} → ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b))
+            → Traversable t
+  traverse= x = record {DefaultTraversable (record {traverse = x})}
+instance
+  open DefaultTraversable
+
+  iTraversableList : Traversable List
+  iTraversableList = traverse= traverseList
+    where
+      traverseList : ⦃ Applicative f ⦄ → (a → f b) → List a → f (List b)
+      traverseList f []       = pure []
+      traverseList f (x ∷ xs) = ⦇ f x ∷ traverseList f xs ⦈
+
+  iTraversableMaybe : Traversable Maybe
+  iTraversableMaybe = traverse= λ where
+    f Nothing  → pure Nothing
+    f (Just x) → Just <$> f x
+
+  iTraversableEither : Traversable (Either a)
+  iTraversableEither = traverse= λ where
+    f (Left  x) → pure (Left x)
+    f (Right y) → Right <$> f y
+
+  iTraversablePair : Traversable (a ×_)
+  iTraversablePair = traverse= λ
+    f (x , y) → (x ,_) <$> f y
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Tuple.html b/lib/Haskell.Prim.Tuple.html new file mode 100644 index 00000000..bc5b3a4b --- /dev/null +++ b/lib/Haskell.Prim.Tuple.html @@ -0,0 +1,47 @@ + +Haskell.Prim.Tuple
+module Haskell.Prim.Tuple where
+
+open import Haskell.Prim
+
+--------------------------------------------------
+-- Tuples
+
+infix 3 _×_ _×_×_
+
+infix -1 _,_ _,_,_
+
+record _×_ (a b : Set) : Set where
+  constructor _,_
+  field
+    fst : a
+    snd : b
+open _×_ public
+
+{-# COMPILE AGDA2HS _×_ tuple #-}
+
+record _×_×_ (a b c : Set) : Set where
+  no-eta-equality; pattern
+  constructor _,_,_
+  field
+    fst3 : a
+    snd3 : b
+    thd3 : c
+
+{-# COMPILE AGDA2HS _×_×_ tuple #-}
+
+uncurry : (a → b → c) → a × b → c
+uncurry f (x , y) = f x y
+
+curry : (a × b → c) → a → b → c
+curry f x y = f (x , y)
+
+first : (a → b) → a × c → b × c
+first f (x , y) = f x , y
+
+second : (a → b) → c × a → c × b
+second f (x , y) = x , f y
+
+_***_ : (a → b) → (c → d) → a × c → b × d
+(f *** g) (x , y) = f x , g y
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.Word.html b/lib/Haskell.Prim.Word.html new file mode 100644 index 00000000..2e31aefd --- /dev/null +++ b/lib/Haskell.Prim.Word.html @@ -0,0 +1,56 @@ + +Haskell.Prim.Word
+module Haskell.Prim.Word where
+
+open import Haskell.Prim
+open import Haskell.Prim.Integer
+
+import Agda.Builtin.Word renaming (Word64 to Word)
+open Agda.Builtin.Word public using (Word)
+
+
+--------------------------------------------------
+-- Literals
+
+module WordInternal where
+  2⁶⁴ : Nat
+  2⁶⁴ = 18446744073709551616
+open WordInternal
+
+instance
+  iNumberWord : Number Word
+  iNumberWord .Number.Constraint n = IsTrue (ltNat n 2⁶⁴)
+  iNumberWord .fromNat n = n2w n
+
+
+--------------------------------------------------
+-- Arithmetic
+
+negateWord : Word → Word
+negateWord a = n2w (monusNat 2⁶⁴ (w2n a))
+
+addWord : Word → Word → Word
+addWord a b = n2w (addNat (w2n a) (w2n b))
+
+subWord : Word → Word → Word
+subWord a b = addWord a (negateWord b)
+
+mulWord : Word → Word → Word
+mulWord a b = n2w (mulNat (w2n a) (w2n b))
+
+eqWord : Word → Word → Bool
+eqWord a b = eqNat (w2n a) (w2n b)
+
+ltWord : Word → Word → Bool
+ltWord a b = ltNat (w2n a) (w2n b)
+
+showWord : Word → List Char
+showWord a = primStringToList (primShowNat (w2n a))
+
+integerToWord : Integer → Word
+integerToWord (pos n)    = n2w n
+integerToWord (negsuc n) = negateWord (n2w (suc n))
+
+wordToInteger : Word → Integer
+wordToInteger n = pos (w2n n)
+
\ No newline at end of file diff --git a/lib/Haskell.Prim.html b/lib/Haskell.Prim.html new file mode 100644 index 00000000..a473fe27 --- /dev/null +++ b/lib/Haskell.Prim.html @@ -0,0 +1,132 @@ + +Haskell.Prim
{-# OPTIONS --no-auto-inline #-}
+
+-- Basic things needed by other primitive modules.
+-- Note that this module exports types and functions that should not
+-- be used directly in Haskell definitions, so you probably want to
+-- import Haskell.Prelude instead.
+
+module Haskell.Prim where
+
+open import Agda.Primitive          public
+open import Agda.Builtin.Bool       public renaming (true to True; false to False)
+open import Agda.Builtin.Int        public renaming (Int to Integer)
+open import Agda.Builtin.Nat        public renaming (_==_ to eqNat; _<_ to ltNat; _+_ to addNat; _-_ to monusNat; _*_ to mulNat)
+open import Agda.Builtin.Char       public renaming (primCharToNat to c2n)
+open import Agda.Builtin.Unit       public
+open import Agda.Builtin.Equality   public
+open import Agda.Builtin.FromString public
+open import Agda.Builtin.FromNat    public
+open import Agda.Builtin.FromNeg    public
+open import Agda.Builtin.String     public renaming (String to AgdaString)
+open import Agda.Builtin.Word       public renaming (primWord64ToNat to w2n; primWord64FromNat to n2w)
+open import Agda.Builtin.Strict     public
+open import Agda.Builtin.List       public
+
+variable
+  @0 ℓ : Level
+  a b c d e : Set
+  f m s t : Set → Set
+
+
+--------------------------------------------------
+-- Functions
+
+id : a → a
+id x = x
+
+infixr 9 _∘_
+_∘_ : (b → c) → (a → b) → a → c
+(f ∘ g) x = f (g x)
+
+flip : (a → b → c) → b → a → c
+flip f x y = f y x
+
+const : a → b → a
+const x _ = x
+
+infixr 0 _$_
+_$_ : (a → b) → a → b
+f $ x = f x
+
+
+--------------------------------------------------
+-- Language constructs
+
+infix -1 case_of_
+case_of_ : (a' : a) → ((a'' : a) → @0 {{ a' ≡ a'' }} → b) → b
+case x of f = f x
+
+infix -2 if_then_else_
+if_then_else_ : {@0 a : Set ℓ} → (flg : Bool) → (@0 {{ flg ≡ True }} → a) → (@0 {{ flg ≡ False }} → a) → a
+if False then x else y = y
+if True  then x else y = x
+
+-- for explicit type signatures (e. g. `4 :: Integer` is `the Int 4`)
+the : (@0 a : Set ℓ) -> a -> a
+the _ x = x
+
+--------------------------------------------------
+-- Agda strings
+
+instance
+  iIsStringAgdaString : IsString AgdaString
+  iIsStringAgdaString .IsString.Constraint _ = ⊤
+  iIsStringAgdaString .fromString s = s
+
+
+--------------------------------------------------
+-- Numbers
+
+instance
+  iNumberNat : Number Nat
+  iNumberNat .Number.Constraint _ = ⊤
+  iNumberNat .fromNat n = n
+
+
+--------------------------------------------------
+-- Lists
+
+lengthNat : List a → Nat
+lengthNat []       = 0
+lengthNat (_ ∷ xs) = addNat 1 (lengthNat xs)
+
+
+--------------------------------------------------
+-- Proof things
+
+data ⊥ : Set where
+
+magic : {A : Set} → ⊥ → A
+magic ()
+
+--principle of explosion
+exFalso : {x : Bool} → (x ≡ True) → (x ≡ False) → ⊥
+exFalso {False} () b 
+exFalso {True} a ()
+
+-- Use to bundle up constraints
+data All {a b} {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
+  instance
+    allNil  : All B []
+    allCons : ∀ {x xs} ⦃ i : B x ⦄ ⦃ is : All B xs ⦄ → All B (x ∷ xs)
+
+data Any {a b} {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
+  instance
+    anyHere  : ∀ {x xs} ⦃ i : B x ⦄ → Any B (x ∷ xs)
+    anyThere : ∀ {x xs} ⦃ is : Any B xs ⦄ → Any B (x ∷ xs)
+
+data IsTrue : Bool → Set where
+  instance itsTrue : IsTrue True
+
+data IsFalse : Bool → Set where
+  instance itsFalse : IsFalse False
+
+data NonEmpty {a : Set} : List a → Set where
+  instance itsNonEmpty : ∀ {x xs} → NonEmpty (x ∷ xs)
+
+data TypeError (err : AgdaString) : Set where
+
+it : ∀ {@0 ℓ} {@0 a : Set ℓ} → ⦃ a ⦄ → a
+it ⦃ x ⦄ = x
+
\ No newline at end of file diff --git a/lib/index.html b/lib/index.html new file mode 100644 index 00000000..298f3107 --- /dev/null +++ b/lib/index.html @@ -0,0 +1,144 @@ + +Haskell.Prelude
{-# 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
+
\ No newline at end of file