[html files
ulfn@chalmers.se**20100421105612
Ignore-this: 5aaa96aa27cd6ba4a63b0613a235a7d2
] hunk ./.boring 6
-^html$
adddir ./html
addfile ./html/Agda.css
hunk ./html/Agda.css 1
+/* Aspects. */
+.Comment { color: #B22222 }
+.Keyword { color: #CD6600 }
+.String { color: #B22222 }
+.Number { color: #A020F0 }
+.Symbol { color: #404040 }
+.PrimitiveType { color: #0000CD }
+.Operator {}
+
+/* NameKinds. */
+.Bound { color: black }
+.InductiveConstructor { color: #008B00 }
+.CoinductiveConstructor { color: #8B7500 }
+.Datatype { color: #0000CD }
+.Field { color: #EE1289 }
+.Function { color: #0000CD }
+.Module { color: #A020F0 }
+.Postulate { color: #0000CD }
+.Primitive { color: #0000CD }
+.Record { color: #0000CD }
+
+/* OtherAspects. */
+.DottedPattern {}
+.UnsolvedMeta { color: black; background: yellow }
+.TerminationProblem { color: black; background: #FFA07A }
+.IncompletePattern { color: black; background: #F5DEB3 }
+.Error { color: red; text-decoration: underline }
+
+/* Standard attributes. */
+a { text-decoration: none }
+a[href]:hover { background-color: #B4EEB4 }
addfile ./html/Algebra.FunctionProperties.Core.html
hunk ./html/Algebra.FunctionProperties.Core.html 1
+
+Algebra.FunctionProperties.Core
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+
+
+
+
+
+module Algebra.FunctionProperties.Core where
+
+open import Level
+
+
+
+
+Op₁ : ∀ {ℓ} → Set ℓ → Set ℓ
+Op₁ A = A → A
+
+Op₂ : ∀ {ℓ} → Set ℓ → Set ℓ
+Op₂ A = A → A → A
+
addfile ./html/Algebra.FunctionProperties.html
hunk ./html/Algebra.FunctionProperties.html 1
+
+Algebra.FunctionProperties
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+
+
+
+open import Level
+open import Relation.Binary
+
+
+
+
+module Algebra.FunctionProperties
+ {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where
+
+open import Data.Product
+
+
+
+
+open import Algebra.FunctionProperties.Core public
+
+
+
+
+Associative : Op₂ A → Set _
+Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))
+
+Commutative : Op₂ A → Set _
+Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x)
+
+LeftIdentity : A → Op₂ A → Set _
+LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x
+
+RightIdentity : A → Op₂ A → Set _
+RightIdentity e _∙_ = ∀ x → (x ∙ e) ≈ x
+
+Identity : A → Op₂ A → Set _
+Identity e ∙ = LeftIdentity e ∙ × RightIdentity e ∙
+
+LeftZero : A → Op₂ A → Set _
+LeftZero z _∙_ = ∀ x → (z ∙ x) ≈ z
+
+RightZero : A → Op₂ A → Set _
+RightZero z _∙_ = ∀ x → (x ∙ z) ≈ z
+
+Zero : A → Op₂ A → Set _
+Zero z ∙ = LeftZero z ∙ × RightZero z ∙
+
+LeftInverse : A → Op₁ A → Op₂ A → Set _
+LeftInverse e _⁻¹ _∙_ = ∀ x → (x ⁻¹ ∙ x) ≈ e
+
+RightInverse : A → Op₁ A → Op₂ A → Set _
+RightInverse e _⁻¹ _∙_ = ∀ x → (x ∙ (x ⁻¹)) ≈ e
+
+Inverse : A → Op₁ A → Op₂ A → Set _
+Inverse e ⁻¹ ∙ = LeftInverse e ⁻¹ ∙ × RightInverse e ⁻¹ ∙
+
+_DistributesOverˡ_ : Op₂ A → Op₂ A → Set _
+_*_ DistributesOverˡ _+_ =
+ ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))
+
+_DistributesOverʳ_ : Op₂ A → Op₂ A → Set _
+_*_ DistributesOverʳ _+_ =
+ ∀ x y z → ((y + z) * x) ≈ ((y * x) + (z * x))
+
+_DistributesOver_ : Op₂ A → Op₂ A → Set _
+* DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
+
+_IdempotentOn_ : Op₂ A → A → Set _
+_∙_ IdempotentOn x = (x ∙ x) ≈ x
+
+Idempotent : Op₂ A → Set _
+Idempotent ∙ = ∀ x → ∙ IdempotentOn x
+
+IdempotentFun : Op₁ A → Set _
+IdempotentFun f = ∀ x → f (f x) ≈ f x
+
+_Absorbs_ : Op₂ A → Op₂ A → Set _
+_∙_ Absorbs _∘_ = ∀ x y → (x ∙ (x ∘ y)) ≈ x
+
+Absorptive : Op₂ A → Op₂ A → Set _
+Absorptive ∙ ∘ = (∙ Absorbs ∘) × (∘ Absorbs ∙)
+
+Involutive : Op₁ A → Set _
+Involutive f = ∀ x → f (f x) ≈ x
+
addfile ./html/Algebra.Structures.html
hunk ./html/Algebra.Structures.html 1
+
+Algebra.Structures
+
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+open import Relation.Binary
+
+module Algebra.Structures where
+
+import Algebra.FunctionProperties as FunctionProperties
+open import Data.Product
+open import Function
+open import Level hiding (zero)
+import Relation.Binary.EqReasoning as EqR
+
+open FunctionProperties using (Op₁; Op₂)
+
+
+
+
+record IsSemigroup {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (∙ : Op₂ A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ isEquivalence : IsEquivalence ≈
+ assoc : Associative ∙
+ ∙-cong : ∙ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
+
+ open IsEquivalence isEquivalence public
+
+record IsMonoid {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ isSemigroup : IsSemigroup ≈ ∙
+ identity : Identity ε ∙
+
+ open IsSemigroup isSemigroup public
+
+record IsCommutativeMonoid {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ isSemigroup : IsSemigroup ≈ _∙_
+ identityˡ : LeftIdentity ε _∙_
+ comm : Commutative _∙_
+
+ open IsSemigroup isSemigroup public
+
+ identity : Identity ε _∙_
+ identity = (identityˡ , identityʳ)
+ where
+ open EqR (record { isEquivalence = isEquivalence })
+
+ identityʳ : RightIdentity ε _∙_
+ identityʳ = λ x → begin
+ (x ∙ ε) ≈⟨ comm x ε ⟩
+ (ε ∙ x) ≈⟨ identityˡ x ⟩
+ x ∎
+
+ isMonoid : IsMonoid ≈ _∙_ ε
+ isMonoid = record
+ { isSemigroup = isSemigroup
+ ; identity = identity
+ }
+
+record IsGroup {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ infixl 7 _-_
+ field
+ isMonoid : IsMonoid ≈ _∙_ ε
+ inverse : Inverse ε _⁻¹ _∙_
+ ⁻¹-cong : _⁻¹ Preserves ≈ ⟶ ≈
+
+ open IsMonoid isMonoid public
+
+ _-_ : Op₂ A
+ x - y = x ∙ (y ⁻¹)
+
+record IsAbelianGroup
+ {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (∙ : Op₂ A) (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ isGroup : IsGroup ≈ ∙ ε ⁻¹
+ comm : Commutative ∙
+
+ open IsGroup isGroup public
+
+ isCommutativeMonoid : IsCommutativeMonoid ≈ ∙ ε
+ isCommutativeMonoid = record
+ { isSemigroup = isSemigroup
+ ; identityˡ = proj₁ identity
+ ; comm = comm
+ }
+
+
+
+
+record IsNearSemiring {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ +-isMonoid : IsMonoid ≈ + 0#
+ *-isSemigroup : IsSemigroup ≈ *
+ distribʳ : * DistributesOverʳ +
+ zeroˡ : LeftZero 0# *
+
+ open IsMonoid +-isMonoid public
+ renaming ( assoc to +-assoc
+ ; ∙-cong to +-cong
+ ; isSemigroup to +-isSemigroup
+ ; identity to +-identity
+ )
+
+ open IsSemigroup *-isSemigroup public
+ using ()
+ renaming ( assoc to *-assoc
+ ; ∙-cong to *-cong
+ )
+
+record IsSemiringWithoutOne {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ +-isCommutativeMonoid : IsCommutativeMonoid ≈ + 0#
+ *-isSemigroup : IsSemigroup ≈ *
+ distrib : * DistributesOver +
+ zero : Zero 0# *
+
+ open IsCommutativeMonoid +-isCommutativeMonoid public
+ hiding (identityˡ)
+ renaming ( assoc to +-assoc
+ ; ∙-cong to +-cong
+ ; isSemigroup to +-isSemigroup
+ ; identity to +-identity
+ ; isMonoid to +-isMonoid
+ ; comm to +-comm
+ )
+
+ open IsSemigroup *-isSemigroup public
+ using ()
+ renaming ( assoc to *-assoc
+ ; ∙-cong to *-cong
+ )
+
+ isNearSemiring : IsNearSemiring ≈ + * 0#
+ isNearSemiring = record
+ { +-isMonoid = +-isMonoid
+ ; *-isSemigroup = *-isSemigroup
+ ; distribʳ = proj₂ distrib
+ ; zeroˡ = proj₁ zero
+ }
+
+record IsSemiringWithoutAnnihilatingZero
+ {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+
+
+ +-isCommutativeMonoid : IsCommutativeMonoid ≈ + 0#
+ *-isMonoid : IsMonoid ≈ * 1#
+ distrib : * DistributesOver +
+
+ open IsCommutativeMonoid +-isCommutativeMonoid public
+ hiding (identityˡ)
+ renaming ( assoc to +-assoc
+ ; ∙-cong to +-cong
+ ; isSemigroup to +-isSemigroup
+ ; identity to +-identity
+ ; isMonoid to +-isMonoid
+ ; comm to +-comm
+ )
+
+ open IsMonoid *-isMonoid public
+ using ()
+ renaming ( assoc to *-assoc
+ ; ∙-cong to *-cong
+ ; isSemigroup to *-isSemigroup
+ ; identity to *-identity
+ )
+
+record IsSemiring {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ isSemiringWithoutAnnihilatingZero :
+ IsSemiringWithoutAnnihilatingZero ≈ + * 0# 1#
+ zero : Zero 0# *
+
+ open IsSemiringWithoutAnnihilatingZero
+ isSemiringWithoutAnnihilatingZero public
+
+ isSemiringWithoutOne : IsSemiringWithoutOne ≈ + * 0#
+ isSemiringWithoutOne = record
+ { +-isCommutativeMonoid = +-isCommutativeMonoid
+ ; *-isSemigroup = *-isSemigroup
+ ; distrib = distrib
+ ; zero = zero
+ }
+
+ open IsSemiringWithoutOne isSemiringWithoutOne public
+ using (isNearSemiring)
+
+record IsCommutativeSemiringWithoutOne
+ {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ isSemiringWithoutOne : IsSemiringWithoutOne ≈ + * 0#
+ *-comm : Commutative *
+
+ open IsSemiringWithoutOne isSemiringWithoutOne public
+
+record IsCommutativeSemiring
+ {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (_+_ _*_ : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ +-isCommutativeMonoid : IsCommutativeMonoid ≈ _+_ 0#
+ *-isCommutativeMonoid : IsCommutativeMonoid ≈ _*_ 1#
+ distribʳ : _*_ DistributesOverʳ _+_
+ zeroˡ : LeftZero 0# _*_
+
+ private
+ module +-CM = IsCommutativeMonoid +-isCommutativeMonoid
+ open module *-CM = IsCommutativeMonoid *-isCommutativeMonoid public
+ using () renaming (comm to *-comm)
+ open EqR (record { isEquivalence = +-CM.isEquivalence })
+
+ distrib : _*_ DistributesOver _+_
+ distrib = (distribˡ , distribʳ)
+ where
+ distribˡ : _*_ DistributesOverˡ _+_
+ distribˡ x y z = begin
+ (x * (y + z)) ≈⟨ *-comm x (y + z) ⟩
+ ((y + z) * x) ≈⟨ distribʳ x y z ⟩
+ ((y * x) + (z * x)) ≈⟨ *-comm y x ⟨ +-CM.∙-cong ⟩ *-comm z x ⟩
+ ((x * y) + (x * z)) ∎
+
+ zero : Zero 0# _*_
+ zero = (zeroˡ , zeroʳ)
+ where
+ zeroʳ : RightZero 0# _*_
+ zeroʳ x = begin
+ (x * 0#) ≈⟨ *-comm x 0# ⟩
+ (0# * x) ≈⟨ zeroˡ x ⟩
+ 0# ∎
+
+ isSemiring : IsSemiring ≈ _+_ _*_ 0# 1#
+ isSemiring = record
+ { isSemiringWithoutAnnihilatingZero = record
+ { +-isCommutativeMonoid = +-isCommutativeMonoid
+ ; *-isMonoid = *-CM.isMonoid
+ ; distrib = distrib
+ }
+ ; zero = zero
+ }
+
+ open IsSemiring isSemiring public
+ hiding (distrib; zero; +-isCommutativeMonoid)
+
+ isCommutativeSemiringWithoutOne :
+ IsCommutativeSemiringWithoutOne ≈ _+_ _*_ 0#
+ isCommutativeSemiringWithoutOne = record
+ { isSemiringWithoutOne = isSemiringWithoutOne
+ ; *-comm = *-CM.comm
+ }
+
+record IsRing
+ {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ +-isAbelianGroup : IsAbelianGroup ≈ _+_ 0# -_
+ *-isMonoid : IsMonoid ≈ _*_ 1#
+ distrib : _*_ DistributesOver _+_
+
+ open IsAbelianGroup +-isAbelianGroup public
+ renaming ( assoc to +-assoc
+ ; ∙-cong to +-cong
+ ; isSemigroup to +-isSemigroup
+ ; identity to +-identity
+ ; isMonoid to +-isMonoid
+ ; inverse to -‿inverse
+ ; ⁻¹-cong to -‿cong
+ ; isGroup to +-isGroup
+ ; comm to +-comm
+ ; isCommutativeMonoid to +-isCommutativeMonoid
+ )
+
+ open IsMonoid *-isMonoid public
+ using ()
+ renaming ( assoc to *-assoc
+ ; ∙-cong to *-cong
+ ; isSemigroup to *-isSemigroup
+ ; identity to *-identity
+ )
+
+ zero : Zero 0# _*_
+ zero = (zeroˡ , zeroʳ)
+ where
+ open EqR (record { isEquivalence = isEquivalence })
+
+ zeroˡ : LeftZero 0# _*_
+ zeroˡ x = begin
+ 0# * x ≈⟨ sym $ proj₂ +-identity _ ⟩
+ (0# * x) + 0# ≈⟨ refl ⟨ +-cong ⟩ sym (proj₂ -‿inverse _) ⟩
+ (0# * x) + ((0# * x) + - (0# * x)) ≈⟨ sym $ +-assoc _ _ _ ⟩
+ ((0# * x) + (0# * x)) + - (0# * x) ≈⟨ sym (proj₂ distrib _ _ _) ⟨ +-cong ⟩ refl ⟩
+ ((0# + 0#) * x) + - (0# * x) ≈⟨ (proj₂ +-identity _ ⟨ *-cong ⟩ refl)
+ ⟨ +-cong ⟩
+ refl ⟩
+ (0# * x) + - (0# * x) ≈⟨ proj₂ -‿inverse _ ⟩
+ 0# ∎
+
+ zeroʳ : RightZero 0# _*_
+ zeroʳ x = begin
+ x * 0# ≈⟨ sym $ proj₂ +-identity _ ⟩
+ (x * 0#) + 0# ≈⟨ refl ⟨ +-cong ⟩ sym (proj₂ -‿inverse _) ⟩
+ (x * 0#) + ((x * 0#) + - (x * 0#)) ≈⟨ sym $ +-assoc _ _ _ ⟩
+ ((x * 0#) + (x * 0#)) + - (x * 0#) ≈⟨ sym (proj₁ distrib _ _ _) ⟨ +-cong ⟩ refl ⟩
+ (x * (0# + 0#)) + - (x * 0#) ≈⟨ (refl ⟨ *-cong ⟩ proj₂ +-identity _)
+ ⟨ +-cong ⟩
+ refl ⟩
+ (x * 0#) + - (x * 0#) ≈⟨ proj₂ -‿inverse _ ⟩
+ 0# ∎
+
+ isSemiringWithoutAnnihilatingZero
+ : IsSemiringWithoutAnnihilatingZero ≈ _+_ _*_ 0# 1#
+ isSemiringWithoutAnnihilatingZero = record
+ { +-isCommutativeMonoid = +-isCommutativeMonoid
+ ; *-isMonoid = *-isMonoid
+ ; distrib = distrib
+ }
+
+ isSemiring : IsSemiring ≈ _+_ _*_ 0# 1#
+ isSemiring = record
+ { isSemiringWithoutAnnihilatingZero =
+ isSemiringWithoutAnnihilatingZero
+ ; zero = zero
+ }
+
+ open IsSemiring isSemiring public
+ using (isNearSemiring; isSemiringWithoutOne)
+
+record IsCommutativeRing
+ {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ isRing : IsRing ≈ + * - 0# 1#
+ *-comm : Commutative *
+
+ open IsRing isRing public
+
+ isCommutativeSemiring : IsCommutativeSemiring ≈ + * 0# 1#
+ isCommutativeSemiring = record
+ { +-isCommutativeMonoid = +-isCommutativeMonoid
+ ; *-isCommutativeMonoid = record
+ { isSemigroup = *-isSemigroup
+ ; identityˡ = proj₁ *-identity
+ ; comm = *-comm
+ }
+ ; distribʳ = proj₂ distrib
+ ; zeroˡ = proj₁ zero
+ }
+
+ open IsCommutativeSemiring isCommutativeSemiring public
+ using ( *-isCommutativeMonoid
+ ; isCommutativeSemiringWithoutOne
+ )
+
+record IsLattice {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ isEquivalence : IsEquivalence ≈
+ ∨-comm : Commutative ∨
+ ∨-assoc : Associative ∨
+ ∨-cong : ∨ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
+ ∧-comm : Commutative ∧
+ ∧-assoc : Associative ∧
+ ∧-cong : ∧ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
+ absorptive : Absorptive ∨ ∧
+
+ open IsEquivalence isEquivalence public
+
+record IsDistributiveLattice {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ isLattice : IsLattice ≈ ∨ ∧
+ ∨-∧-distribʳ : ∨ DistributesOverʳ ∧
+
+ open IsLattice isLattice public
+
+record IsBooleanAlgebra
+ {a ℓ} {A : Set a} (≈ : Rel A ℓ)
+ (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where
+ open FunctionProperties ≈
+ field
+ isDistributiveLattice : IsDistributiveLattice ≈ ∨ ∧
+ ∨-complementʳ : RightInverse ⊤ ¬ ∨
+ ∧-complementʳ : RightInverse ⊥ ¬ ∧
+ ¬-cong : ¬ Preserves ≈ ⟶ ≈
+
+ open IsDistributiveLattice isDistributiveLattice public
+
addfile ./html/Algebra.html
hunk ./html/Algebra.html 1
+
+Algebra
+
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Algebra where
+
+open import Relation.Binary
+open import Algebra.FunctionProperties
+open import Algebra.Structures
+open import Function
+open import Level
+
+
+
+
+record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixl 7 _∙_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∙_ : Op₂ Carrier
+ isSemigroup : IsSemigroup _≈_ _∙_
+
+ open IsSemigroup isSemigroup public
+
+ setoid : Setoid _ _
+ setoid = record { isEquivalence = isEquivalence }
+
+
+
+record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixl 7 _∙_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∙_ : Op₂ Carrier
+ ε : Carrier
+
+record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixl 7 _∙_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∙_ : Op₂ Carrier
+ ε : Carrier
+ isMonoid : IsMonoid _≈_ _∙_ ε
+
+ open IsMonoid isMonoid public
+
+ semigroup : Semigroup _ _
+ semigroup = record { isSemigroup = isSemigroup }
+
+ open Semigroup semigroup public using (setoid)
+
+ rawMonoid : RawMonoid _ _
+ rawMonoid = record
+ { _≈_ = _≈_
+ ; _∙_ = _∙_
+ ; ε = ε
+ }
+
+record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixl 7 _∙_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∙_ : Op₂ Carrier
+ ε : Carrier
+ isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε
+
+ open IsCommutativeMonoid isCommutativeMonoid public
+
+ monoid : Monoid _ _
+ monoid = record { isMonoid = isMonoid }
+
+ open Monoid monoid public using (setoid; semigroup; rawMonoid)
+
+record Group c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 8 _⁻¹
+ infixl 7 _∙_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∙_ : Op₂ Carrier
+ ε : Carrier
+ _⁻¹ : Op₁ Carrier
+ isGroup : IsGroup _≈_ _∙_ ε _⁻¹
+
+ open IsGroup isGroup public
+
+ monoid : Monoid _ _
+ monoid = record { isMonoid = isMonoid }
+
+ open Monoid monoid public using (setoid; semigroup; rawMonoid)
+
+record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 8 _⁻¹
+ infixl 7 _∙_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∙_ : Op₂ Carrier
+ ε : Carrier
+ _⁻¹ : Op₁ Carrier
+ isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε _⁻¹
+
+ open IsAbelianGroup isAbelianGroup public
+
+ group : Group _ _
+ group = record { isGroup = isGroup }
+
+ open Group group public using (setoid; semigroup; monoid; rawMonoid)
+
+ commutativeMonoid : CommutativeMonoid _ _
+ commutativeMonoid =
+ record { isCommutativeMonoid = isCommutativeMonoid }
+
+
+
+
+record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ 0# : Carrier
+ isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0#
+
+ open IsNearSemiring isNearSemiring public
+
+ +-monoid : Monoid _ _
+ +-monoid = record { isMonoid = +-isMonoid }
+
+ open Monoid +-monoid public
+ using (setoid)
+ renaming ( semigroup to +-semigroup
+ ; rawMonoid to +-rawMonoid)
+
+ *-semigroup : Semigroup _ _
+ *-semigroup = record { isSemigroup = *-isSemigroup }
+
+record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ 0# : Carrier
+ isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0#
+
+ open IsSemiringWithoutOne isSemiringWithoutOne public
+
+ nearSemiring : NearSemiring _ _
+ nearSemiring = record { isNearSemiring = isNearSemiring }
+
+ open NearSemiring nearSemiring public
+ using ( setoid
+ ; +-semigroup; +-rawMonoid; +-monoid
+ ; *-semigroup
+ )
+
+ +-commutativeMonoid : CommutativeMonoid _ _
+ +-commutativeMonoid =
+ record { isCommutativeMonoid = +-isCommutativeMonoid }
+
+record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ isSemiringWithoutAnnihilatingZero :
+ IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1#
+
+ open IsSemiringWithoutAnnihilatingZero
+ isSemiringWithoutAnnihilatingZero public
+
+ +-commutativeMonoid : CommutativeMonoid _ _
+ +-commutativeMonoid =
+ record { isCommutativeMonoid = +-isCommutativeMonoid }
+
+ open CommutativeMonoid +-commutativeMonoid public
+ using (setoid)
+ renaming ( semigroup to +-semigroup
+ ; rawMonoid to +-rawMonoid
+ ; monoid to +-monoid
+ )
+
+ *-monoid : Monoid _ _
+ *-monoid = record { isMonoid = *-isMonoid }
+
+ open Monoid *-monoid public
+ using ()
+ renaming ( semigroup to *-semigroup
+ ; rawMonoid to *-rawMonoid
+ )
+
+record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#
+
+ open IsSemiring isSemiring public
+
+ semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero _ _
+ semiringWithoutAnnihilatingZero = record
+ { isSemiringWithoutAnnihilatingZero =
+ isSemiringWithoutAnnihilatingZero
+ }
+
+ open SemiringWithoutAnnihilatingZero
+ semiringWithoutAnnihilatingZero public
+ using ( setoid
+ ; +-semigroup; +-rawMonoid; +-monoid
+ ; +-commutativeMonoid
+ ; *-semigroup; *-rawMonoid; *-monoid
+ )
+
+ semiringWithoutOne : SemiringWithoutOne _ _
+ semiringWithoutOne =
+ record { isSemiringWithoutOne = isSemiringWithoutOne }
+
+ open SemiringWithoutOne semiringWithoutOne public
+ using (nearSemiring)
+
+record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ 0# : Carrier
+ isCommutativeSemiringWithoutOne :
+ IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0#
+
+ open IsCommutativeSemiringWithoutOne
+ isCommutativeSemiringWithoutOne public
+
+ semiringWithoutOne : SemiringWithoutOne _ _
+ semiringWithoutOne =
+ record { isSemiringWithoutOne = isSemiringWithoutOne }
+
+ open SemiringWithoutOne semiringWithoutOne public
+ using ( setoid
+ ; +-semigroup; +-rawMonoid; +-monoid
+ ; +-commutativeMonoid
+ ; *-semigroup
+ ; nearSemiring
+ )
+
+record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#
+
+ open IsCommutativeSemiring isCommutativeSemiring public
+
+ semiring : Semiring _ _
+ semiring = record { isSemiring = isSemiring }
+
+ open Semiring semiring public
+ using ( setoid
+ ; +-semigroup; +-rawMonoid; +-monoid
+ ; +-commutativeMonoid
+ ; *-semigroup; *-rawMonoid; *-monoid
+ ; nearSemiring; semiringWithoutOne
+ ; semiringWithoutAnnihilatingZero
+ )
+
+ *-commutativeMonoid : CommutativeMonoid _ _
+ *-commutativeMonoid =
+ record { isCommutativeMonoid = *-isCommutativeMonoid }
+
+ commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _ _
+ commutativeSemiringWithoutOne = record
+ { isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne
+ }
+
+
+
+
+
+
+record RawRing c : Set (suc c) where
+ infix 8 -_
+ infixl 7 _*_
+ infixl 6 _+_
+ field
+ Carrier : Set c
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ -_ : Op₁ Carrier
+ 0# : Carrier
+ 1# : Carrier
+
+record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 8 -_
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ -_ : Op₁ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#
+
+ open IsRing isRing public
+
+ +-abelianGroup : AbelianGroup _ _
+ +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }
+
+ semiring : Semiring _ _
+ semiring = record { isSemiring = isSemiring }
+
+ open Semiring semiring public
+ using ( setoid
+ ; +-semigroup; +-rawMonoid; +-monoid
+ ; +-commutativeMonoid
+ ; *-semigroup; *-rawMonoid; *-monoid
+ ; nearSemiring; semiringWithoutOne
+ ; semiringWithoutAnnihilatingZero
+ )
+
+ open AbelianGroup +-abelianGroup public
+ using () renaming (group to +-group)
+
+ rawRing : RawRing _
+ rawRing = record
+ { _+_ = _+_
+ ; _*_ = _*_
+ ; -_ = -_
+ ; 0# = 0#
+ ; 1# = 1#
+ }
+
+record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 8 -_
+ infixl 7 _*_
+ infixl 6 _+_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _+_ : Op₂ Carrier
+ _*_ : Op₂ Carrier
+ -_ : Op₁ Carrier
+ 0# : Carrier
+ 1# : Carrier
+ isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#
+
+ open IsCommutativeRing isCommutativeRing public
+
+ ring : Ring _ _
+ ring = record { isRing = isRing }
+
+ commutativeSemiring : CommutativeSemiring _ _
+ commutativeSemiring =
+ record { isCommutativeSemiring = isCommutativeSemiring }
+
+ open Ring ring public using (rawRing; +-group; +-abelianGroup)
+ open CommutativeSemiring commutativeSemiring public
+ using ( setoid
+ ; +-semigroup; +-rawMonoid; +-monoid; +-commutativeMonoid
+ ; *-semigroup; *-rawMonoid; *-monoid; *-commutativeMonoid
+ ; nearSemiring; semiringWithoutOne
+ ; semiringWithoutAnnihilatingZero; semiring
+ ; commutativeSemiringWithoutOne
+ )
+
+
+
+
+record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixr 7 _∧_
+ infixr 6 _∨_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∨_ : Op₂ Carrier
+ _∧_ : Op₂ Carrier
+ isLattice : IsLattice _≈_ _∨_ _∧_
+
+ open IsLattice isLattice public
+
+ setoid : Setoid _ _
+ setoid = record { isEquivalence = isEquivalence }
+
+record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
+ infixr 7 _∧_
+ infixr 6 _∨_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∨_ : Op₂ Carrier
+ _∧_ : Op₂ Carrier
+ isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_
+
+ open IsDistributiveLattice isDistributiveLattice public
+
+ lattice : Lattice _ _
+ lattice = record { isLattice = isLattice }
+
+ open Lattice lattice public using (setoid)
+
+record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 8 ¬_
+ infixr 7 _∧_
+ infixr 6 _∨_
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ _∨_ : Op₂ Carrier
+ _∧_ : Op₂ Carrier
+ ¬_ : Op₁ Carrier
+ ⊤ : Carrier
+ ⊥ : Carrier
+ isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥
+
+ open IsBooleanAlgebra isBooleanAlgebra public
+
+ distributiveLattice : DistributiveLattice _ _
+ distributiveLattice =
+ record { isDistributiveLattice = isDistributiveLattice }
+
+ open DistributiveLattice distributiveLattice public
+ using (setoid; lattice)
+
addfile ./html/BString.html
hunk ./html/BString.html 1
+
+BString
+module BString where
+
+open import Function
+open import Data.Nat
+open import List
+open import Data.Bool renaming (T to isTrue)
+open import Data.Vec
+open import Data.Char
+import Data.String as String
+open String using (String)
+open import Relation.Nullary
+
+data BList (A : Set) : ℕ → Set where
+ [] : {n : ℕ} → BList A n
+ _∷_ : {n : ℕ} → A → BList A n → BList A (suc n)
+
+forgetV : {A : Set}{n : ℕ} → Vec A n → List A
+forgetV [] = []
+forgetV (x ∷ xs) = x ∷ forgetV xs
+
+forgetB : {A : Set}{n : ℕ} → BList A n → List A
+forgetB [] = []
+forgetB (x ∷ xs) = x ∷ forgetB xs
+
+_=<_ : ℕ → ℕ → Bool
+zero =< _ = true
+suc n =< zero = false
+suc n =< suc m = n =< m
+
+vec : ∀ {n A} → A → Vec A n
+vec {zero} _ = []
+vec {suc n} x = x ∷ vec x
+
+bList : {n : ℕ}{A : Set}(xs : List A){p : isTrue (length xs =< n)} →
+ BList A n
+bList [] = []
+bList {zero} (x ∷ xs) {}
+bList {suc n} (x ∷ xs) {p} = x ∷ bList xs {p}
+
+vList : {n : ℕ}{A : Set}(xs : List A){p : isTrue (length xs =< n)} →
+ A → Vec A n
+vList [] z = vec z
+vList {zero} (x ∷ xs) {} _
+vList {suc n} (x ∷ xs) {p} z = x ∷ vList xs {p} z
+
+strLen : String → ℕ
+strLen = length ∘ stringToList
+
+BString = BList Char
+
+bString : ∀ {n} s {p : isTrue (strLen s =< n)} → BString n
+bString s {p} = bList (stringToList s) {p}
+
+unBString : ∀ {n} → BString n → String
+unBString = stringFromList ∘ forgetB
+
+VString = Vec Char
+
+vString : ∀ {n} s {p : isTrue (strLen s =< n)} → VString n
+vString s {p} = vList (stringToList s) {p} ' '
+
+unVString : ∀ {n} → VString n → String
+unVString = stringFromList ∘ forgetV
+
+trim : Char → String → String
+trim c = stringFromList ∘ List.reverse ∘ dropWhile (_==_ c) ∘ List.reverse ∘ stringToList
+
addfile ./html/Category.Applicative.Indexed.html
hunk ./html/Category.Applicative.Indexed.html 1
+
+Category.Applicative.Indexed
+
+
+
+
+
+
+module Category.Applicative.Indexed where
+
+open import Function
+open import Data.Product
+open import Category.Functor
+
+IFun : Set → Set₁
+IFun I = I → I → Set → Set
+
+record RawIApplicative {I : Set} (F : IFun I) : Set₁ where
+ infixl 4 _⊛_ _<⊛_ _⊛>_
+ infix 4 _⊗_
+
+ field
+ pure : ∀ {i A} → A → F i i A
+ _⊛_ : ∀ {i j k A B} → F i j (A → B) → F j k A → F i k B
+
+ rawFunctor : ∀ {i j} → RawFunctor (F i j)
+ rawFunctor = record
+ { _<$>_ = λ g x → pure g ⊛ x
+ }
+
+ private
+ open module RF {i j : I} =
+ RawFunctor (rawFunctor {i = i} {j = j})
+ public
+
+ _<⊛_ : ∀ {i j k A B} → F i j A → F j k B → F i k A
+ x <⊛ y = const <$> x ⊛ y
+
+ _⊛>_ : ∀ {i j k A B} → F i j A → F j k B → F i k B
+ x ⊛> y = flip const <$> x ⊛ y
+
+ _⊗_ : ∀ {i j k A B} → F i j A → F j k B → F i k (A × B)
+ x ⊗ y = (_,_) <$> x ⊛ y
+
addfile ./html/Category.Functor.html
hunk ./html/Category.Functor.html 1
+
+Category.Functor
+
+
+
+
+
+module Category.Functor where
+
+open import Function
+
+record RawFunctor (f : Set → Set) : Set₁ where
+ infixl 4 _<$>_ _<$_
+
+ field
+ _<$>_ : ∀ {a b} → (a → b) → f a → f b
+
+ _<$_ : ∀ {a b} → a → f b → f a
+ x <$ y = const x <$> y
+
addfile ./html/Category.Monad.Identity.html
hunk ./html/Category.Monad.Identity.html 1
+
+Category.Monad.Identity
+
+
+
+module Category.Monad.Identity where
+
+open import Category.Monad
+
+Identity : Set → Set
+Identity A = A
+
+IdentityMonad : RawMonad Identity
+IdentityMonad = record
+ { return = λ x → x
+ ; _>>=_ = λ x f → f x
+ }
+
addfile ./html/Category.Monad.Indexed.html
hunk ./html/Category.Monad.Indexed.html 1
+
+Category.Monad.Indexed
+
+
+
+
+
+module Category.Monad.Indexed where
+
+open import Function
+open import Category.Applicative.Indexed
+
+record RawIMonad {I : Set} (M : IFun I) : Set₁ where
+ infixl 1 _>>=_ _>>_
+ infixr 1 _=<<_
+
+ field
+ return : ∀ {i A} → A → M i i A
+ _>>=_ : ∀ {i j k A B} → M i j A → (A → M j k B) → M i k B
+
+ _>>_ : ∀ {i j k A B} → M i j A → M j k B → M i k B
+ m₁ >> m₂ = m₁ >>= λ _ → m₂
+
+ _=<<_ : ∀ {i j k A B} → (A → M j k B) → M i j A → M i k B
+ f =<< c = c >>= f
+
+ join : ∀ {i j k A} → M i j (M j k A) → M i k A
+ join m = m >>= id
+
+ rawIApplicative : RawIApplicative M
+ rawIApplicative = record
+ { pure = return
+ ; _⊛_ = λ f x → f >>= λ f' → x >>= λ x' → return (f' x')
+ }
+
+ open RawIApplicative rawIApplicative public
+
+record RawIMonadZero {I : Set} (M : IFun I) : Set₁ where
+ field
+ monad : RawIMonad M
+ ∅ : ∀ {i j A} → M i j A
+
+ open RawIMonad monad public
+
+record RawIMonadPlus {I : Set} (M : IFun I) : Set₁ where
+ infixr 3 _∣_
+ field
+ monadZero : RawIMonadZero M
+ _∣_ : ∀ {i j A} → M i j A → M i j A → M i j A
+
+ open RawIMonadZero monadZero public
+
addfile ./html/Category.Monad.html
hunk ./html/Category.Monad.html 1
+
+Category.Monad
+
+
+
+
+
+module Category.Monad where
+
+open import Function
+open import Category.Monad.Indexed
+open import Data.Unit
+
+RawMonad : (Set → Set) → Set₁
+RawMonad M = RawIMonad {⊤} (λ _ _ → M)
+
+RawMonadZero : (Set → Set) → Set₁
+RawMonadZero M = RawIMonadZero {⊤} (λ _ _ → M)
+
+RawMonadPlus : (Set → Set) → Set₁
+RawMonadPlus M = RawIMonadPlus {⊤} (λ _ _ → M)
+
+module RawMonad {M : Set → Set} (Mon : RawMonad M) where
+ open RawIMonad Mon public
+
+module RawMonadZero {M : Set → Set} (Mon : RawMonadZero M) where
+ open RawIMonadZero Mon public
+
+module RawMonadPlus {M : Set → Set} (Mon : RawMonadPlus M) where
+ open RawIMonadPlus Mon public
+
addfile ./html/Coinduction.html
hunk ./html/Coinduction.html 1
+
+Coinduction
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Coinduction where
+
+import Level
+
+
+
+
+
+
+
+
+infix 1000 ♯_
+
+codata ∞ {a} (A : Set a) : Set a where
+ ♯_ : (x : A) → ∞ A
+
+♭ : ∀ {a} {A : Set a} → ∞ A → A
+♭ (♯ x) = x
+
+
+
+
+
+record Rec {a} (A : ∞ (Set a)) : Set a where
+ constructor fold
+ field
+ unfold : ♭ A
+
+open Rec public
+
+
+
addfile ./html/Data.Bool.html
hunk ./html/Data.Bool.html 1
+
+Data.Bool
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Data.Bool where
+
+open import Function
+open import Data.Unit using (⊤)
+open import Data.Empty
+open import Level
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as PropEq
+ using (_≡_; refl)
+
+infixr 6 _∧_
+infixr 5 _∨_ _xor_
+infix 0 if_then_else_
+
+
+
+
+data Bool : Set where
+ true : Bool
+ false : Bool
+
+{-# BUILTIN BOOL Bool #-}
+{-# BUILTIN TRUE true #-}
+{-# BUILTIN FALSE false #-}
+
+{-# COMPILED_DATA Bool Bool True False #-}
+
+
+
+
+not : Bool → Bool
+not true = false
+not false = true
+
+
+
+
+T : Bool → Set
+T true = ⊤
+T false = ⊥
+
+if_then_else_ : ∀ {a} {A : Set a} → Bool → A → A → A
+if true then t else f = t
+if false then t else f = f
+
+_∧_ : Bool → Bool → Bool
+true ∧ b = b
+false ∧ b = false
+
+_∨_ : Bool → Bool → Bool
+true ∨ b = true
+false ∨ b = b
+
+_xor_ : Bool → Bool → Bool
+true xor b = not b
+false xor b = b
+
+
+
+
+_≟_ : Decidable {A = Bool} _≡_
+true ≟ true = yes refl
+false ≟ false = yes refl
+true ≟ false = no λ()
+false ≟ true = no λ()
+
+
+
+
+decSetoid : DecSetoid _ _
+decSetoid = PropEq.decSetoid _≟_
+
addfile ./html/Data.BoundedVec.Inefficient.html
hunk ./html/Data.BoundedVec.Inefficient.html 1
+
+Data.BoundedVec.Inefficient
+
+
+
+
+
+module Data.BoundedVec.Inefficient where
+
+open import Data.Nat
+open import Data.List
+
+
+
+
+infixr 5 _∷_
+
+data BoundedVec (a : Set) : ℕ → Set where
+ [] : ∀ {n} → BoundedVec a n
+ _∷_ : ∀ {n} (x : a) (xs : BoundedVec a n) → BoundedVec a (suc n)
+
+
+
+
+
+
+↑ : ∀ {a n} → BoundedVec a n → BoundedVec a (suc n)
+↑ [] = []
+↑ (x ∷ xs) = x ∷ ↑ xs
+
+
+
+
+fromList : ∀ {a} → (xs : List a) → BoundedVec a (length xs)
+fromList [] = []
+fromList (x ∷ xs) = x ∷ fromList xs
+
+toList : ∀ {a n} → BoundedVec a n → List a
+toList [] = []
+toList (x ∷ xs) = x ∷ toList xs
+
addfile ./html/Data.Char.html
hunk ./html/Data.Char.html 1
+
+Data.Char
+
+
+
+module Data.Char where
+
+open import Data.Nat using (ℕ)
+open import Data.Bool using (Bool; true; false)
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
+
+
+
+
+postulate
+ Char : Set
+
+{-# BUILTIN CHAR Char #-}
+{-# COMPILED_TYPE Char Char #-}
+
+
+
+
+private
+ primitive
+ primCharToNat : Char → ℕ
+ primCharEquality : Char → Char → Bool
+
+toNat : Char → ℕ
+toNat = primCharToNat
+
+infix 4 _==_
+
+_==_ : Char → Char → Bool
+_==_ = primCharEquality
+
+_≟_ : Decidable {A = Char} _≡_
+s₁ ≟ s₂ with s₁ == s₂
+... | true = yes trustMe
+ where postulate trustMe : _
+... | false = no trustMe
+ where postulate trustMe : _
+
+setoid : Setoid _ _
+setoid = PropEq.setoid Char
+
+decSetoid : DecSetoid _ _
+decSetoid = PropEq.decSetoid _≟_
+
addfile ./html/Data.Colist.html
hunk ./html/Data.Colist.html 1
+
+Data.Colist
+
+
+
+module Data.Colist where
+
+open import Category.Monad
+open import Coinduction
+open import Data.Bool using (Bool; true; false)
+open import Data.Empty using (⊥)
+open import Data.Maybe using (Maybe; nothing; just)
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Conat using (Coℕ; zero; suc)
+open import Data.List using (List; []; _∷_)
+open import Data.List.NonEmpty using (List⁺; _∷_)
+ renaming ([_] to [_]⁺)
+open import Data.BoundedVec.Inefficient as BVec
+ using (BoundedVec; []; _∷_)
+open import Data.Product using (_,_)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Function
+open import Relation.Binary
+import Relation.Binary.InducedPreorders as Ind
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Nullary
+open import Relation.Nullary.Negation
+open RawMonad ¬¬-Monad
+
+
+
+
+infixr 5 _∷_
+
+data Colist (A : Set) : Set where
+ [] : Colist A
+ _∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A
+
+data Any {A} (P : A → Set) : Colist A → Set where
+ here : ∀ {x xs} (px : P x) → Any P (x ∷ xs)
+ there : ∀ {x xs} (pxs : Any P (♭ xs)) → Any P (x ∷ xs)
+
+data All {A} (P : A → Set) : Colist A → Set where
+ [] : All P []
+ _∷_ : ∀ {x xs} (px : P x) (pxs : ∞ (All P (♭ xs))) → All P (x ∷ xs)
+
+
+
+
+null : ∀ {A} → Colist A → Bool
+null [] = true
+null (_ ∷ _) = false
+
+length : ∀ {A} → Colist A → Coℕ
+length [] = zero
+length (x ∷ xs) = suc (♯ length (♭ xs))
+
+map : ∀ {A B} → (A → B) → Colist A → Colist B
+map f [] = []
+map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)
+
+fromList : ∀ {A} → List A → Colist A
+fromList [] = []
+fromList (x ∷ xs) = x ∷ ♯ fromList xs
+
+take : ∀ {A} (n : ℕ) → Colist A → BoundedVec A n
+take zero xs = []
+take (suc n) [] = []
+take (suc n) (x ∷ xs) = x ∷ take n (♭ xs)
+
+replicate : ∀ {A} → Coℕ → A → Colist A
+replicate zero x = []
+replicate (suc n) x = x ∷ ♯ replicate (♭ n) x
+
+lookup : ∀ {A} → ℕ → Colist A → Maybe A
+lookup n [] = nothing
+lookup zero (x ∷ xs) = just x
+lookup (suc n) (x ∷ xs) = lookup n (♭ xs)
+
+infixr 5 _++_
+
+_++_ : ∀ {A} → Colist A → Colist A → Colist A
+[] ++ ys = ys
+(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)
+
+concat : ∀ {A} → Colist (List⁺ A) → Colist A
+concat [] = []
+concat ([ x ]⁺ ∷ xss) = x ∷ ♯ concat (♭ xss)
+concat ((x ∷ xs) ∷ xss) = x ∷ ♯ concat (xs ∷ xss)
+
+[_] : ∀ {A} → A → Colist A
+[ x ] = x ∷ ♯ []
+
+
+
+
+
+
+infix 4 _≈_
+
+data _≈_ {A} : (xs ys : Colist A) → Set where
+ [] : [] ≈ []
+ _∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys
+
+
+
+setoid : Set → Setoid _ _
+setoid A = record
+ { Carrier = Colist A
+ ; _≈_ = _≈_
+ ; isEquivalence = record
+ { refl = refl
+ ; sym = sym
+ ; trans = trans
+ }
+ }
+ where
+ refl : Reflexive _≈_
+ refl {[]} = []
+ refl {x ∷ xs} = x ∷ ♯ refl
+
+ sym : Symmetric _≈_
+ sym [] = []
+ sym (x ∷ xs≈) = x ∷ ♯ sym (♭ xs≈)
+
+ trans : Transitive _≈_
+ trans [] [] = []
+ trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)
+
+module ≈-Reasoning where
+ import Relation.Binary.EqReasoning as EqR
+ private
+ open module R {A : Set} = EqR (setoid A) public
+
+
+
+map-cong : ∀ {A B} (f : A → B) → _≈_ =[ map f ]⇒ _≈_
+map-cong f [] = []
+map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)
+
+
+
+
+
+
+infix 4 _∈_
+
+_∈_ : {A : Set} → A → Colist A → Set
+x ∈ xs = Any (_≡_ x) xs
+
+
+
+infix 4 _⊆_
+
+_⊆_ : {A : Set} → Colist A → Colist A → Set
+xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys
+
+
+
+infix 4 _⊑_
+
+data _⊑_ {A : Set} : Colist A → Colist A → Set where
+ [] : ∀ {ys} → [] ⊑ ys
+ _∷_ : ∀ x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) → x ∷ xs ⊑ x ∷ ys
+
+
+
+⊑⇒⊆ : {A : Set} → _⊑_ {A = A} ⇒ _⊆_
+⊑⇒⊆ [] ()
+⊑⇒⊆ (x ∷ xs⊑ys) (here ≡x) = here ≡x
+⊑⇒⊆ (_ ∷ xs⊑ys) (there x∈xs) = there (⊑⇒⊆ (♭ xs⊑ys) x∈xs)
+
+
+
+⊑-Poset : Set → Poset _ _ _
+⊑-Poset A = record
+ { Carrier = Colist A
+ ; _≈_ = _≈_
+ ; _≤_ = _⊑_
+ ; isPartialOrder = record
+ { isPreorder = record
+ { isEquivalence = Setoid.isEquivalence (setoid A)
+ ; reflexive = reflexive
+ ; trans = trans
+ }
+ ; antisym = antisym
+ }
+ }
+ where
+ reflexive : _≈_ ⇒ _⊑_
+ reflexive [] = []
+ reflexive (x ∷ xs≈) = x ∷ ♯ reflexive (♭ xs≈)
+
+ trans : Transitive _⊑_
+ trans [] _ = []
+ trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)
+
+ antisym : Antisymmetric _≈_ _⊑_
+ antisym [] [] = []
+ antisym (x ∷ p₁) (.x ∷ p₂) = x ∷ ♯ antisym (♭ p₁) (♭ p₂)
+
+module ⊑-Reasoning where
+ import Relation.Binary.PartialOrderReasoning as POR
+ private
+ open module R {A : Set} = POR (⊑-Poset A)
+ public renaming (_≤⟨_⟩_ to _⊑⟨_⟩_)
+
+
+
+⊆-Preorder : Set → Preorder _ _ _
+⊆-Preorder A =
+ Ind.InducedPreorder₂ (setoid A) _∈_
+ (λ xs≈ys → ⊑⇒⊆ $ ⊑P.reflexive xs≈ys)
+ where module ⊑P = Poset (⊑-Poset A)
+
+module ⊆-Reasoning where
+ import Relation.Binary.PreorderReasoning as PreR
+ private
+ open module R {A : Set} = PreR (⊆-Preorder A)
+ public renaming (_∼⟨_⟩_ to _⊆⟨_⟩_)
+
+ infix 1 _∈⟨_⟩_
+
+ _∈⟨_⟩_ : ∀ {A : Set} (x : A) {xs ys} →
+ x ∈ xs → xs IsRelatedTo ys → x ∈ ys
+ x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs
+
+
+
+take-⊑ : ∀ {A} n (xs : Colist A) →
+ let toColist = fromList ∘ BVec.toList in
+ toColist (take n xs) ⊑ xs
+take-⊑ zero xs = []
+take-⊑ (suc n) [] = []
+take-⊑ (suc n) (x ∷ xs) = x ∷ ♯ take-⊑ n (♭ xs)
+
+
+
+
+
+
+data Finite {A : Set} : Colist A → Set where
+ [] : Finite []
+ _∷_ : ∀ x {xs} (fin : Finite (♭ xs)) → Finite (x ∷ xs)
+
+
+
+data Infinite {A : Set} : Colist A → Set where
+ _∷_ : ∀ x {xs} (inf : ∞ (Infinite (♭ xs))) → Infinite (x ∷ xs)
+
+
+
+not-finite-is-infinite :
+ {A : Set} (xs : Colist A) → ¬ Finite xs → Infinite xs
+not-finite-is-infinite [] hyp with hyp []
+... | ()
+not-finite-is-infinite (x ∷ xs) hyp =
+ x ∷ ♯ not-finite-is-infinite (♭ xs) (hyp ∘ _∷_ x)
+
+
+
+finite-or-infinite :
+ {A : Set} (xs : Colist A) → ¬ ¬ (Finite xs ⊎ Infinite xs)
+finite-or-infinite xs = helper <$> excluded-middle
+ where
+ helper : Dec (Finite xs) → Finite xs ⊎ Infinite xs
+ helper (yes fin) = inj₁ fin
+ helper (no ¬fin) = inj₂ $ not-finite-is-infinite xs ¬fin
+
+
+
+not-finite-and-infinite :
+ {A : Set} {xs : Colist A} → Finite xs → Infinite xs → ⊥
+not-finite-and-infinite [] ()
+not-finite-and-infinite (x ∷ fin) (.x ∷ inf) =
+ not-finite-and-infinite fin (♭ inf)
+
addfile ./html/Data.Conat.html
hunk ./html/Data.Conat.html 1
+
+Data.Conat
+
+
+
+module Data.Conat where
+
+open import Coinduction
+open import Data.Nat using (ℕ; zero; suc)
+open import Relation.Binary
+
+
+
+
+data Coℕ : Set where
+ zero : Coℕ
+ suc : (n : ∞ Coℕ) → Coℕ
+
+
+
+
+fromℕ : ℕ → Coℕ
+fromℕ zero = zero
+fromℕ (suc n) = suc (♯ fromℕ n)
+
+∞ℕ : Coℕ
+∞ℕ = suc (♯ ∞ℕ)
+
+infixl 6 _+_
+
+_+_ : Coℕ → Coℕ → Coℕ
+zero + n = n
+suc m + n = suc (♯ (♭ m + n))
+
+
+
+
+data _≈_ : Coℕ → Coℕ → Set where
+ zero : zero ≈ zero
+ suc : ∀ {m n} (m≈n : ∞ (♭ m ≈ ♭ n)) → suc m ≈ suc n
+
+setoid : Setoid _ _
+setoid = record
+ { Carrier = Coℕ
+ ; _≈_ = _≈_
+ ; isEquivalence = record
+ { refl = refl
+ ; sym = sym
+ ; trans = trans
+ }
+ }
+ where
+ refl : Reflexive _≈_
+ refl {zero} = zero
+ refl {suc n} = suc (♯ refl)
+
+ sym : Symmetric _≈_
+ sym zero = zero
+ sym (suc m≈n) = suc (♯ sym (♭ m≈n))
+
+ trans : Transitive _≈_
+ trans zero zero = zero
+ trans (suc m≈n) (suc n≈k) = suc (♯ trans (♭ m≈n) (♭ n≈k))
+
addfile ./html/Data.Empty.html
hunk ./html/Data.Empty.html 1
+
+Data.Empty
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Data.Empty where
+
+open import Level
+
+data ⊥ : Set where
+
+⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
+⊥-elim ()
+
addfile ./html/Data.Fin.Dec.html
hunk ./html/Data.Fin.Dec.html 1
+
+Data.Fin.Dec
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Data.Fin.Dec where
+
+open import Function
+open import Data.Nat hiding (_<_)
+open import Data.Vec hiding (_∈_)
+open import Data.Fin
+open import Data.Fin.Subset
+open import Data.Fin.Subset.Props
+open import Data.Product as Prod
+open import Data.Empty
+open import Level hiding (Lift)
+open import Relation.Nullary
+open import Relation.Unary using (Pred)
+
+infix 4 _∈?_
+
+_∈?_ : ∀ {n} x (p : Subset n) → Dec (x ∈ p)
+zero ∈? inside ∷ p = yes here
+zero ∈? outside ∷ p = no λ()
+suc n ∈? s ∷ p with n ∈? p
+... | yes n∈p = yes (there n∈p)
+... | no n∉p = no (n∉p ∘ drop-there)
+
+private
+
+ restrictP : ∀ {n} → (Fin (suc n) → Set) → (Fin n → Set)
+ restrictP P f = P (suc f)
+
+ restrict : ∀ {n} {P : Fin (suc n) → Set} →
+ (∀ f → Dec (P f)) →
+ (∀ f → Dec (restrictP P f))
+ restrict dec f = dec (suc f)
+
+any? : ∀ {n} {P : Fin n → Set} →
+ ((f : Fin n) → Dec (P f)) →
+ Dec (∃ P)
+any? {zero} {P} dec = no ((¬ Fin 0 ∶ λ()) ∘ proj₁)
+any? {suc n} {P} dec with dec zero | any? (restrict dec)
+... | yes p | _ = yes (_ , p)
+... | _ | yes (_ , p') = yes (_ , p')
+... | no ¬p | no ¬p' = no helper
+ where
+ helper : ∄ P
+ helper (zero , p) = ¬p p
+ helper (suc f , p') = ¬p' (_ , p')
+
+nonempty? : ∀ {n} (p : Subset n) → Dec (Nonempty p)
+nonempty? p = any? (λ x → x ∈? p)
+
+private
+
+ restrict∈ : ∀ {n} P {Q : Fin (suc n) → Set} →
+ (∀ {f} → Q f → Dec (P f)) →
+ (∀ {f} → restrictP Q f → Dec (restrictP P f))
+ restrict∈ _ dec {f} Qf = dec {suc f} Qf
+
+decFinSubset : ∀ {n} {P Q : Fin n → Set} →
+ (∀ f → Dec (Q f)) →
+ (∀ {f} → Q f → Dec (P f)) →
+ Dec (∀ {f} → Q f → P f)
+decFinSubset {zero} _ _ = yes λ{}
+decFinSubset {suc n} {P} {Q} decQ decP = helper
+ where
+ helper : Dec (∀ {f} → Q f → P f)
+ helper with decFinSubset (restrict decQ) (restrict∈ P decP)
+ helper | no ¬q⟶p = no (λ q⟶p → ¬q⟶p (λ {f} q → q⟶p {suc f} q))
+ helper | yes q⟶p with decQ zero
+ helper | yes q⟶p | yes q₀ with decP q₀
+ helper | yes q⟶p | yes q₀ | no ¬p₀ = no (λ q⟶p → ¬p₀ (q⟶p {zero} q₀))
+ helper | yes q⟶p | yes q₀ | yes p₀ = yes (λ {_} → hlpr _)
+ where
+ hlpr : ∀ f → Q f → P f
+ hlpr zero _ = p₀
+ hlpr (suc f) qf = q⟶p qf
+ helper | yes q⟶p | no ¬q₀ = yes (λ {_} → hlpr _)
+ where
+ hlpr : ∀ f → Q f → P f
+ hlpr zero q₀ = ⊥-elim (¬q₀ q₀)
+ hlpr (suc f) qf = q⟶p qf
+
+all∈? : ∀ {n} {P : Fin n → Set} {q} →
+ (∀ {f} → f ∈ q → Dec (P f)) →
+ Dec (∀ {f} → f ∈ q → P f)
+all∈? {q = q} dec = decFinSubset (λ f → f ∈? q) dec
+
+all? : ∀ {n} {P : Fin n → Set} →
+ (∀ f → Dec (P f)) →
+ Dec (∀ f → P f)
+all? dec with all∈? {q = all inside} (λ {f} _ → dec f)
+... | yes ∀p = yes (λ f → ∀p (allInside f))
+... | no ¬∀p = no (λ ∀p → ¬∀p (λ {f} _ → ∀p f))
+
+decLift : ∀ {n} {P : Fin n → Set} →
+ (∀ x → Dec (P x)) →
+ (∀ p → Dec (Lift P p))
+decLift dec p = all∈? (λ {x} _ → dec x)
+
+private
+
+ restrictSP : ∀ {n} → Side → (Subset (suc n) → Set) → (Subset n → Set)
+ restrictSP s P p = P (s ∷ p)
+
+ restrictS : ∀ {n} {P : Subset (suc n) → Set} →
+ (s : Side) →
+ (∀ p → Dec (P p)) →
+ (∀ p → Dec (restrictSP s P p))
+ restrictS s dec p = dec (s ∷ p)
+
+anySubset? : ∀ {n} {P : Subset n → Set} →
+ (∀ s → Dec (P s)) →
+ Dec (∃ P)
+anySubset? {zero} {P} dec with dec []
+... | yes P[] = yes (_ , P[])
+... | no ¬P[] = no helper
+ where
+ helper : ∄ P
+ helper ([] , P[]) = ¬P[] P[]
+anySubset? {suc n} {P} dec with anySubset? (restrictS inside dec)
+ | anySubset? (restrictS outside dec)
+... | yes (_ , Pp) | _ = yes (_ , Pp)
+... | _ | yes (_ , Pp) = yes (_ , Pp)
+... | no ¬Pp | no ¬Pp' = no helper
+ where
+ helper : ∄ P
+ helper (inside ∷ p , Pp) = ¬Pp (_ , Pp)
+ helper (outside ∷ p , Pp') = ¬Pp' (_ , Pp')
+
+
+
+
+¬∀⟶∃¬-smallest :
+ ∀ n {p} (P : Fin n → Set p) → (∀ i → Dec (P i)) →
+ ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
+¬∀⟶∃¬-smallest zero P dec ¬∀iPi = ⊥-elim (¬∀iPi (λ()))
+¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi with dec zero
+¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi | no ¬P0 = (zero , ¬P0 , λ ())
+¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi | yes P0 =
+ Prod.map suc (Prod.map id extend′) $
+ ¬∀⟶∃¬-smallest n (λ n → P (suc n)) (dec ∘ suc) (¬∀iPi ∘ extend)
+ where
+ extend : (∀ i → P (suc i)) → (∀ i → P i)
+ extend ∀iP[1+i] zero = P0
+ extend ∀iP[1+i] (suc i) = ∀iP[1+i] i
+
+ extend′ : ∀ {i : Fin n} →
+ ((j : Fin′ i) → P (suc (inject j))) →
+ ((j : Fin′ (suc i)) → P (inject j))
+ extend′ g zero = P0
+ extend′ g (suc j) = g j
+
addfile ./html/Data.Fin.Subset.Props.html
hunk ./html/Data.Fin.Subset.Props.html 1
+
+Data.Fin.Subset.Props
+
+
+
+module Data.Fin.Subset.Props where
+
+open import Data.Nat
+open import Data.Vec hiding (_∈_)
+open import Data.Empty
+open import Function
+open import Data.Fin
+open import Data.Fin.Subset
+open import Data.Product
+open import Relation.Binary.PropositionalEquality
+
+
+
+
+drop-there : ∀ {s n x} {p : Subset n} → suc x ∈ s ∷ p → x ∈ p
+drop-there (there x∈p) = x∈p
+
+drop-∷-⊆ : ∀ {n s₁ s₂} {p₁ p₂ : Subset n} → s₁ ∷ p₁ ⊆ s₂ ∷ p₂ → p₁ ⊆ p₂
+drop-∷-⊆ p₁s₁⊆p₂s₂ x∈p₁ = drop-there $ p₁s₁⊆p₂s₂ (there x∈p₁)
+
+drop-∷-Empty : ∀ {n s} {p : Subset n} → Empty (s ∷ p) → Empty p
+drop-∷-Empty ¬¬∅ (x , x∈p) = ¬¬∅ (suc x , there x∈p)
+
+
+
+
+allInside : ∀ {n} (x : Fin n) → x ∈ all inside
+allInside zero = here
+allInside (suc x) = there (allInside x)
+
+allOutside : ∀ {n} (x : Fin n) → x ∉ all outside
+allOutside zero ()
+allOutside (suc x) (there x∈) = allOutside x x∈
+
+⊆⊇⟶≡ : ∀ {n} {p₁ p₂ : Subset n} →
+ p₁ ⊆ p₂ → p₂ ⊆ p₁ → p₁ ≡ p₂
+⊆⊇⟶≡ = helper _ _
+ where
+ helper : ∀ {n} (p₁ p₂ : Subset n) →
+ p₁ ⊆ p₂ → p₂ ⊆ p₁ → p₁ ≡ p₂
+ helper [] [] _ _ = refl
+ helper (s₁ ∷ p₁) (s₂ ∷ p₂) ₁⊆₂ ₂⊆₁ with ⊆⊇⟶≡ (drop-∷-⊆ ₁⊆₂)
+ (drop-∷-⊆ ₂⊆₁)
+ helper (outside ∷ p) (outside ∷ .p) ₁⊆₂ ₂⊆₁ | refl = refl
+ helper (inside ∷ p) (inside ∷ .p) ₁⊆₂ ₂⊆₁ | refl = refl
+ helper (outside ∷ p) (inside ∷ .p) ₁⊆₂ ₂⊆₁ | refl with ₂⊆₁ here
+ ... | ()
+ helper (inside ∷ p) (outside ∷ .p) ₁⊆₂ ₂⊆₁ | refl with ₁⊆₂ here
+ ... | ()
+
+∅⟶allOutside : ∀ {n} {p : Subset n} →
+ Empty p → p ≡ all outside
+∅⟶allOutside {p = []} ¬¬∅ = refl
+∅⟶allOutside {p = s ∷ ps} ¬¬∅ with ∅⟶allOutside (drop-∷-Empty ¬¬∅)
+∅⟶allOutside {p = outside ∷ .(all outside)} ¬¬∅ | refl = refl
+∅⟶allOutside {p = inside ∷ .(all outside)} ¬¬∅ | refl =
+ ⊥-elim (¬¬∅ (zero , here))
+
addfile ./html/Data.Fin.Subset.html
hunk ./html/Data.Fin.Subset.html 1
+
+Data.Fin.Subset
+
+
+
+module Data.Fin.Subset where
+
+open import Data.Nat
+open import Data.Vec hiding (_∈_)
+open import Data.Fin
+open import Data.Product
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality
+
+infixr 2 _∈_ _∉_ _⊆_ _⊈_
+
+
+
+
+data Side : Set where
+ inside : Side
+ outside : Side
+
+
+
+Subset : ℕ → Set
+Subset = Vec Side
+
+
+
+
+_∈_ : ∀ {n} → Fin n → Subset n → Set
+x ∈ p = p [ x ]= inside
+
+_∉_ : ∀ {n} → Fin n → Subset n → Set
+x ∉ p = ¬ (x ∈ p)
+
+_⊆_ : ∀ {n} → Subset n → Subset n → Set
+p₁ ⊆ p₂ = ∀ {x} → x ∈ p₁ → x ∈ p₂
+
+_⊈_ : ∀ {n} → Subset n → Subset n → Set
+p₁ ⊈ p₂ = ¬ (p₁ ⊆ p₂)
+
+
+
+
+all : ∀ {n} → Side → Subset n
+all {zero} _ = []
+all {suc n} s = s ∷ all s
+
+
+
+
+Nonempty : ∀ {n} (p : Subset n) → Set
+Nonempty p = ∃ λ f → f ∈ p
+
+Empty : ∀ {n} (p : Subset n) → Set
+Empty p = ¬ Nonempty p
+
+
+
+Lift : ∀ {n} → (Fin n → Set) → (Subset n → Set)
+Lift P p = ∀ {x} → x ∈ p → P x
+
addfile ./html/Data.Fin.html
hunk ./html/Data.Fin.html 1
+
+Data.Fin
+
+
+
+
+
+
+
+module Data.Fin where
+
+open import Data.Nat as Nat
+ using (ℕ; zero; suc; z≤n; s≤s)
+ renaming ( _+_ to _N+_; _∸_ to _N∸_
+ ; _≤_ to _N≤_; _<_ to _N<_; _≤?_ to _N≤?_)
+open import Function
+open import Level hiding (lift)
+open import Relation.Nullary.Decidable
+open import Relation.Binary
+
+
+
+
+
+
+data Fin : ℕ → Set where
+ zero : {n : ℕ} → Fin (suc n)
+ suc : {n : ℕ} (i : Fin n) → Fin (suc n)
+
+
+
+toℕ : ∀ {n} → Fin n → ℕ
+toℕ zero = 0
+toℕ (suc i) = suc (toℕ i)
+
+
+
+Fin′ : ∀ {n} → Fin n → Set
+Fin′ i = Fin (toℕ i)
+
+
+
+
+
+
+
+
+fromℕ : (n : ℕ) → Fin (suc n)
+fromℕ zero = zero
+fromℕ (suc n) = suc (fromℕ n)
+
+
+
+fromℕ≤ : ∀ {m n} → m N< n → Fin n
+fromℕ≤ (Nat.s≤s Nat.z≤n) = zero
+fromℕ≤ (Nat.s≤s (Nat.s≤s m≤n)) = suc (fromℕ≤ (Nat.s≤s m≤n))
+
+
+
+#_ : ∀ m {n} {m<n : True (suc m N≤? n)} → Fin n
+#_ _ {m<n = m<n} = fromℕ≤ (toWitness m<n)
+
+
+
+raise : ∀ {m} n → Fin m → Fin (n N+ m)
+raise zero i = i
+raise (suc n) i = suc (raise n i)
+
+
+
+inject : ∀ {n} {i : Fin n} → Fin′ i → Fin n
+inject {i = zero} ()
+inject {i = suc i} zero = zero
+inject {i = suc i} (suc j) = suc (inject j)
+
+inject! : ∀ {n} {i : Fin (suc n)} → Fin′ i → Fin n
+inject! {n = zero} {i = suc ()} _
+inject! {i = zero} ()
+inject! {n = suc _} {i = suc _} zero = zero
+inject! {n = suc _} {i = suc _} (suc j) = suc (inject! j)
+
+inject+ : ∀ {m} n → Fin m → Fin (m N+ n)
+inject+ n zero = zero
+inject+ n (suc i) = suc (inject+ n i)
+
+inject₁ : ∀ {m} → Fin m → Fin (suc m)
+inject₁ zero = zero
+inject₁ (suc i) = suc (inject₁ i)
+
+inject≤ : ∀ {m n} → Fin m → m N≤ n → Fin n
+inject≤ zero (Nat.s≤s le) = zero
+inject≤ (suc i) (Nat.s≤s le) = suc (inject≤ i le)
+
+
+
+
+
+
+fold : ∀ (T : ℕ → Set) {m} →
+ (∀ {n} → T n → T (suc n)) →
+ (∀ {n} → T (suc n)) →
+ Fin m → T m
+fold T f x zero = x
+fold T f x (suc i) = f (fold T f x i)
+
+
+
+lift : ∀ {m n} k → (Fin m → Fin n) → Fin (k N+ m) → Fin (k N+ n)
+lift zero f i = f i
+lift (suc k) f zero = zero
+lift (suc k) f (suc i) = suc (lift k f i)
+
+
+
+infixl 6 _+_
+
+_+_ : ∀ {m n} (i : Fin m) (j : Fin n) → Fin (toℕ i N+ n)
+zero + j = j
+suc i + j = suc (i + j)
+
+
+
+infixl 6 _-_
+
+_-_ : ∀ {m} (i : Fin m) (j : Fin′ (suc i)) → Fin (m N∸ toℕ j)
+i - zero = i
+zero - suc ()
+suc i - suc j = i - j
+
+
+
+infixl 6 _ℕ-_
+
+_ℕ-_ : (n : ℕ) (j : Fin (suc n)) → Fin (suc n N∸ toℕ j)
+n ℕ- zero = fromℕ n
+zero ℕ- suc ()
+suc n ℕ- suc i = n ℕ- i
+
+
+
+infixl 6 _ℕ-ℕ_
+
+_ℕ-ℕ_ : (n : ℕ) → Fin (suc n) → ℕ
+n ℕ-ℕ zero = n
+zero ℕ-ℕ suc ()
+suc n ℕ-ℕ suc i = n ℕ-ℕ i
+
+
+
+pred : ∀ {n} → Fin n → Fin n
+pred zero = zero
+pred (suc i) = inject₁ i
+
+
+
+
+infix 4 _≤_ _<_
+
+_≤_ : ∀ {n} → Rel (Fin n) zero
+_≤_ = _N≤_ on toℕ
+
+_<_ : ∀ {n} → Rel (Fin n) zero
+_<_ = _N<_ on toℕ
+
+data _≺_ : ℕ → ℕ → Set where
+ _≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n
+
+
+
+data Ordering {n : ℕ} : Fin n → Fin n → Set where
+ less : ∀ greatest (least : Fin′ greatest) →
+ Ordering (inject least) greatest
+ equal : ∀ i → Ordering i i
+ greater : ∀ greatest (least : Fin′ greatest) →
+ Ordering greatest (inject least)
+
+compare : ∀ {n} (i j : Fin n) → Ordering i j
+compare zero zero = equal zero
+compare zero (suc j) = less (suc j) zero
+compare (suc i) zero = greater (suc i) zero
+compare (suc i) (suc j) with compare i j
+compare (suc .(inject least)) (suc .greatest) | less greatest least =
+ less (suc greatest) (suc least)
+compare (suc .greatest) (suc .(inject least)) | greater greatest least =
+ greater (suc greatest) (suc least)
+compare (suc .i) (suc .i) | equal i = equal (suc i)
+
addfile ./html/Data.Function.html
hunk ./html/Data.Function.html 1
+
+Data.Function
+
+
+
+module Data.Function where
+
+infixr 9 _∘_ _∘′_ _∘₀_ _∘₁_
+infixl 1 _on_ _on₁_
+infixl 1 _⟨_⟩_ _⟨_⟩₁_
+infixr 0 _-[_]₁-_ _-[_]-_ _$_ _$₁_
+infix 0 _∶_ _∶₁_
+
+
+
+
+
+
+Fun₁ : Set → Set
+Fun₁ a = a → a
+
+
+
+Fun₂ : Set → Set
+Fun₂ a = a → a → a
+
+
+
+
+_∘_ : {A : Set} {B : A → Set} {C : {x : A} → B x → Set} →
+ (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
+ ((x : A) → C (g x))
+f ∘ g = λ x → f (g x)
+
+_∘′_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
+f ∘′ g = _∘_ f g
+
+_∘₀_ : {A : Set} {B : A → Set} {C : {x : A} → B x → Set₁} →
+ (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
+ ((x : A) → C (g x))
+f ∘₀ g = λ x → f (g x)
+
+_∘₁_ : {A : Set₁} {B : A → Set₁} {C : {x : A} → B x → Set₁} →
+ (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
+ ((x : A) → C (g x))
+f ∘₁ g = λ x → f (g x)
+
+id : {a : Set} → a → a
+id x = x
+
+id₁ : {a : Set₁} → a → a
+id₁ x = x
+
+const : {a b : Set} → a → b → a
+const x = λ _ → x
+
+const₁ : {a : Set₁} {b : Set} → a → b → a
+const₁ x = λ _ → x
+
+flip : {A B : Set} {C : A → B → Set} →
+ ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
+flip f = λ x y → f y x
+
+flip₁ : {A B : Set} {C : A → B → Set₁} →
+ ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
+flip₁ f = λ x y → f y x
+
+
+
+
+
+
+_$_ : {A : Set} {B : A → Set} → ((x : A) → B x) → ((x : A) → B x)
+f $ x = f x
+
+_$₁_ : {A : Set₁} {B : A → Set₁} → ((x : A) → B x) → ((x : A) → B x)
+f $₁ x = f x
+
+_⟨_⟩_ : {a b c : Set} → a → (a → b → c) → b → c
+x ⟨ f ⟩ y = f x y
+
+_⟨_⟩₁_ : {a b : Set} → a → (a → b → Set) → b → Set
+x ⟨ f ⟩₁ y = f x y
+
+_on_ : {a b c : Set} → (b → b → c) → (a → b) → (a → a → c)
+_*_ on f = λ x y → f x * f y
+
+_on₁_ : {a b : Set} {c : Set₁} → (b → b → c) → (a → b) → (a → a → c)
+_*_ on₁ f = λ x y → f x * f y
+
+_-[_]-_ : {a b c d e : Set} →
+ (a → b → c) → (c → d → e) → (a → b → d) → (a → b → e)
+f -[ _*_ ]- g = λ x y → f x y * g x y
+
+_-[_]₁-_ : {a b : Set} →
+ (a → b → Set) → (Set → Set → Set) → (a → b → Set) →
+ (a → b → Set)
+f -[ _*_ ]₁- g = λ x y → f x y * g x y
+
+
+
+
+
+
+
+_∶_ : (A : Set) → A → A
+_ ∶ x = x
+
+_∶₁_ : (A : Set₁) → A → A
+_ ∶₁ x = x
+
addfile ./html/Data.List.NonEmpty.html
hunk ./html/Data.List.NonEmpty.html 1
+
+Data.List.NonEmpty
+
+
+
+module Data.List.NonEmpty where
+
+open import Data.Product hiding (map)
+open import Data.Nat
+open import Function
+open import Data.Vec as Vec using (Vec; []; _∷_)
+open import Data.List as List using (List; []; _∷_)
+open import Category.Monad
+open import Relation.Binary.PropositionalEquality
+
+infixr 5 _∷_ _∷ʳ_ _⁺++⁺_ _++⁺_ _⁺++_
+
+data List⁺ (A : Set) : Set where
+ [_] : (x : A) → List⁺ A
+ _∷_ : (x : A) (xs : List⁺ A) → List⁺ A
+
+length_-1 : ∀ {A} → List⁺ A → ℕ
+length [ x ] -1 = 0
+length x ∷ xs -1 = 1 + length xs -1
+
+
+
+
+fromVec : ∀ {n A} → Vec A (suc n) → List⁺ A
+fromVec {zero} (x ∷ _) = [ x ]
+fromVec {suc n} (x ∷ xs) = x ∷ fromVec xs
+
+toVec : ∀ {A} (xs : List⁺ A) → Vec A (suc (length xs -1))
+toVec [ x ] = Vec.[_] x
+toVec (x ∷ xs) = x ∷ toVec xs
+
+lift : ∀ {A B} →
+ (∀ {m} → Vec A (suc m) → ∃ λ n → Vec B (suc n)) →
+ List⁺ A → List⁺ B
+lift f xs = fromVec (proj₂ (f (toVec xs)))
+
+fromList : ∀ {A} → A → List A → List⁺ A
+fromList x xs = fromVec (Vec.fromList (x ∷ xs))
+
+toList : ∀ {A} → List⁺ A → List A
+toList = Vec.toList ∘ toVec
+
+
+
+
+head : ∀ {A} → List⁺ A → A
+head = Vec.head ∘ toVec
+
+tail : ∀ {A} → List⁺ A → List A
+tail = Vec.toList ∘ Vec.tail ∘ toVec
+
+map : ∀ {A B} → (A → B) → List⁺ A → List⁺ B
+map f = lift (λ xs → (, Vec.map f xs))
+
+
+
+
+foldr : {A B : Set} → (A → B → B) → (A → B) → List⁺ A → B
+foldr c s [ x ] = s x
+foldr c s (x ∷ xs) = c x (foldr c s xs)
+
+
+
+
+foldl : {A B : Set} → (B → A → B) → (A → B) → List⁺ A → B
+foldl c s [ x ] = s x
+foldl c s (x ∷ xs) = foldl c (c (s x)) xs
+
+
+
+_⁺++⁺_ : ∀ {A} → List⁺ A → List⁺ A → List⁺ A
+xs ⁺++⁺ ys = foldr _∷_ (λ x → x ∷ ys) xs
+
+_⁺++_ : ∀ {A} → List⁺ A → List A → List⁺ A
+xs ⁺++ ys = foldr _∷_ (λ x → fromList x ys) xs
+
+_++⁺_ : ∀ {A} → List A → List⁺ A → List⁺ A
+xs ++⁺ ys = List.foldr _∷_ ys xs
+
+concat : ∀ {A} → List⁺ (List⁺ A) → List⁺ A
+concat [ xs ] = xs
+concat (xs ∷ xss) = xs ⁺++⁺ concat xss
+
+monad : RawMonad List⁺
+monad = record
+ { return = [_]
+ ; _>>=_ = λ xs f → concat (map f xs)
+ }
+
+reverse : ∀ {A} → List⁺ A → List⁺ A
+reverse = lift (,_ ∘′ Vec.reverse)
+
+
+
+_∷ʳ_ : ∀ {A} → List⁺ A → A → List⁺ A
+xs ∷ʳ x = foldr _∷_ (λ y → y ∷ [ x ]) xs
+
+
+
+infixl 5 _∷ʳ′_
+
+data SnocView {A} : List⁺ A → Set where
+ [_] : (x : A) → SnocView [ x ]
+ _∷ʳ′_ : (xs : List⁺ A) (x : A) → SnocView (xs ∷ʳ x)
+
+snocView : ∀ {A} (xs : List⁺ A) → SnocView xs
+snocView [ x ] = [ x ]
+snocView (x ∷ xs) with snocView xs
+snocView (x ∷ .([ y ])) | [ y ] = [ x ] ∷ʳ′ y
+snocView (x ∷ .(ys ∷ʳ y)) | ys ∷ʳ′ y = (x ∷ ys) ∷ʳ′ y
+
+
+
+last : ∀ {A} → List⁺ A → A
+last xs with snocView xs
+last .([ y ]) | [ y ] = y
+last .(ys ∷ʳ y) | ys ∷ʳ′ y = y
+
+
+
+
+
+
+
+private
+ module Examples {A B : Set}
+ (_⊕_ : A → B → B)
+ (_⊗_ : B → A → B)
+ (f : A → B)
+ (a b c : A)
+ where
+
+ hd : head (a ∷ b ∷ [ c ]) ≡ a
+ hd = refl
+
+ tl : tail (a ∷ b ∷ [ c ]) ≡ b ∷ c ∷ []
+ tl = refl
+
+ mp : map f (a ∷ b ∷ [ c ]) ≡ f a ∷ f b ∷ [ f c ]
+ mp = refl
+
+ right : foldr _⊕_ f (a ∷ b ∷ [ c ]) ≡ a ⊕ (b ⊕ f c)
+ right = refl
+
+ left : foldl _⊗_ f (a ∷ b ∷ [ c ]) ≡ (f a ⊗ b) ⊗ c
+ left = refl
+
+ ⁺app⁺ : (a ∷ b ∷ [ c ]) ⁺++⁺ (b ∷ [ c ]) ≡
+ a ∷ b ∷ c ∷ b ∷ [ c ]
+ ⁺app⁺ = refl
+
+ ⁺app : (a ∷ b ∷ [ c ]) ⁺++ (b ∷ c ∷ []) ≡
+ a ∷ b ∷ c ∷ b ∷ [ c ]
+ ⁺app = refl
+
+ app⁺ : (a ∷ b ∷ c ∷ []) ++⁺ (b ∷ [ c ]) ≡
+ a ∷ b ∷ c ∷ b ∷ [ c ]
+ app⁺ = refl
+
+ conc : concat ((a ∷ b ∷ [ c ]) ∷ [ b ∷ [ c ] ]) ≡
+ a ∷ b ∷ c ∷ b ∷ [ c ]
+ conc = refl
+
+ rev : reverse (a ∷ b ∷ [ c ]) ≡ c ∷ b ∷ [ a ]
+ rev = refl
+
+ snoc : (a ∷ b ∷ [ c ]) ∷ʳ a ≡ a ∷ b ∷ c ∷ [ a ]
+ snoc = refl
+
addfile ./html/Data.List.html
hunk ./html/Data.List.html 1
+
+Data.List
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Data.List where
+
+open import Data.Nat
+open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
+open import Data.Bool
+open import Data.Maybe using (Maybe; nothing; just)
+open import Data.Product as Prod using (_×_; _,_)
+open import Function
+open import Algebra
+import Relation.Binary.PropositionalEquality as PropEq
+import Algebra.FunctionProperties as FunProp
+
+infixr 5 _∷_ _++_
+
+
+
+
+data List {a} (A : Set a) : Set a where
+ [] : List A
+ _∷_ : (x : A) (xs : List A) → List A
+
+{-# BUILTIN LIST List #-}
+{-# BUILTIN NIL [] #-}
+{-# BUILTIN CONS _∷_ #-}
+
+
+
+
+
+
+[_] : ∀ {a} {A : Set a} → A → List A
+[ x ] = x ∷ []
+
+_++_ : ∀ {a} {A : Set a} → List A → List A → List A
+[] ++ ys = ys
+(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
+
+
+
+infixl 5 _∷ʳ_
+
+_∷ʳ_ : ∀ {a} {A : Set a} → List A → A → List A
+xs ∷ʳ x = xs ++ [ x ]
+
+null : ∀ {a} {A : Set a} → List A → Bool
+null [] = true
+null (x ∷ xs) = false
+
+
+
+map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B
+map f [] = []
+map f (x ∷ xs) = f x ∷ map f xs
+
+reverse : ∀ {a} {A : Set a} → List A → List A
+reverse xs = rev xs []
+ where
+ rev : ∀ {a} {A : Set a} → List A → List A → List A
+ rev [] ys = ys
+ rev (x ∷ xs) ys = rev xs (x ∷ ys)
+
+replicate : ∀ {a} {A : Set a} → (n : ℕ) → A → List A
+replicate zero x = []
+replicate (suc n) x = x ∷ replicate n x
+
+zipWith : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+ → (A → B → C) → List A → List B → List C
+zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
+zipWith f _ _ = []
+
+zip : ∀ {a b} {A : Set a} {B : Set b} → List A → List B → List (A × B)
+zip = zipWith (_,_)
+
+intersperse : ∀ {a} {A : Set a} → A → List A → List A
+intersperse x [] = []
+intersperse x (y ∷ []) = [ y ]
+intersperse x (y ∷ z ∷ zs) = y ∷ x ∷ intersperse x (z ∷ zs)
+
+
+
+foldr : ∀ {a b} {A : Set a} {B : Set b} → (A → B → B) → B → List A → B
+foldr c n [] = n
+foldr c n (x ∷ xs) = c x (foldr c n xs)
+
+foldl : ∀ {a b} {A : Set a} {B : Set b} → (A → B → A) → A → List B → A
+foldl c n [] = n
+foldl c n (x ∷ xs) = foldl c (c n x) xs
+
+
+
+concat : ∀ {a} {A : Set a} → List (List A) → List A
+concat = foldr _++_ []
+
+concatMap : ∀ {a b} {A : Set a} {B : Set b} →
+ (A → List B) → List A → List B
+concatMap f = concat ∘ map f
+
+and : List Bool → Bool
+and = foldr _∧_ true
+
+or : List Bool → Bool
+or = foldr _∨_ false
+
+any : ∀ {a} {A : Set a} → (A → Bool) → List A → Bool
+any p = or ∘ map p
+
+all : ∀ {a} {A : Set a} → (A → Bool) → List A → Bool
+all p = and ∘ map p
+
+sum : List ℕ → ℕ
+sum = foldr _+_ 0
+
+product : List ℕ → ℕ
+product = foldr _*_ 1
+
+length : ∀ {a} {A : Set a} → List A → ℕ
+length = foldr (λ _ → suc) 0
+
+
+
+
+
+scanr : ∀ {a b} {A : Set a} {B : Set b} →
+ (A → B → B) → B → List A → List B
+scanr f e [] = e ∷ []
+scanr f e (x ∷ xs) with scanr f e xs
+... | [] = []
+... | y ∷ ys = f x y ∷ y ∷ ys
+
+scanl : ∀ {a b} {A : Set a} {B : Set b} →
+ (A → B → A) → A → List B → List A
+scanl f e [] = e ∷ []
+scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs
+
+
+
+
+
+unfold : ∀ {a b} {A : Set a} (B : ℕ → Set b)
+ (f : ∀ {n} → B (suc n) → Maybe (A × B n)) →
+ ∀ {n} → B n → List A
+unfold B f {n = zero} s = []
+unfold B f {n = suc n} s with f s
+... | nothing = []
+... | just (x , s') = x ∷ unfold B f s'
+
+
+
+downFrom : ℕ → List ℕ
+downFrom n = unfold Singleton f (wrap n)
+ where
+ data Singleton : ℕ → Set where
+ wrap : (n : ℕ) → Singleton n
+
+ f : ∀ {n} → Singleton (suc n) → Maybe (ℕ × Singleton n)
+ f {n} (wrap .(suc n)) = just (n , wrap n)
+
+
+
+fromMaybe : ∀ {a} {A : Set a} → Maybe A → List A
+fromMaybe (just x) = [ x ]
+fromMaybe nothing = []
+
+
+
+
+
+take : ∀ {a} {A : Set a} → ℕ → List A → List A
+take zero xs = []
+take (suc n) [] = []
+take (suc n) (x ∷ xs) = x ∷ take n xs
+
+drop : ∀ {a} {A : Set a} → ℕ → List A → List A
+drop zero xs = xs
+drop (suc n) [] = []
+drop (suc n) (x ∷ xs) = drop n xs
+
+splitAt : ∀ {a} {A : Set a} → ℕ → List A → (List A × List A)
+splitAt zero xs = ([] , xs)
+splitAt (suc n) [] = ([] , [])
+splitAt (suc n) (x ∷ xs) with splitAt n xs
+... | (ys , zs) = (x ∷ ys , zs)
+
+takeWhile : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
+takeWhile p [] = []
+takeWhile p (x ∷ xs) with p x
+... | true = x ∷ takeWhile p xs
+... | false = []
+
+dropWhile : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
+dropWhile p [] = []
+dropWhile p (x ∷ xs) with p x
+... | true = dropWhile p xs
+... | false = x ∷ xs
+
+span : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
+span p [] = ([] , [])
+span p (x ∷ xs) with p x
+... | true = Prod.map (_∷_ x) id (span p xs)
+... | false = ([] , x ∷ xs)
+
+break : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
+break p = span (not ∘ p)
+
+inits : ∀ {a} {A : Set a} → List A → List (List A)
+inits [] = [] ∷ []
+inits (x ∷ xs) = [] ∷ map (_∷_ x) (inits xs)
+
+tails : ∀ {a} {A : Set a} → List A → List (List A)
+tails [] = [] ∷ []
+tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
+
+infixl 5 _∷ʳ'_
+
+data InitLast {a} {A : Set a} : List A → Set a where
+ [] : InitLast []
+ _∷ʳ'_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x)
+
+initLast : ∀ {a} {A : Set a} (xs : List A) → InitLast xs
+initLast [] = []
+initLast (x ∷ xs) with initLast xs
+initLast (x ∷ .[]) | [] = [] ∷ʳ' x
+initLast (x ∷ .(ys ∷ʳ y)) | ys ∷ʳ' y = (x ∷ ys) ∷ʳ' y
+
+
+
+
+
+
+
+gfilter : ∀ {a b} {A : Set a} {B : Set b} →
+ (A → Maybe B) → List A → List B
+gfilter p [] = []
+gfilter p (x ∷ xs) with p x
+... | just y = y ∷ gfilter p xs
+... | nothing = gfilter p xs
+
+filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
+filter p = gfilter (λ x → if p x then just x else nothing)
+
+partition : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
+partition p [] = ([] , [])
+partition p (x ∷ xs) with p x | partition p xs
+... | true | (ys , zs) = (x ∷ ys , zs)
+... | false | (ys , zs) = (ys , x ∷ zs)
+
+
+
+
+monoid : ∀ {ℓ} → Set ℓ → Monoid _ _
+monoid A = record
+ { Carrier = List A
+ ; _≈_ = _≡_
+ ; _∙_ = _++_
+ ; ε = []
+ ; isMonoid = record
+ { isSemigroup = record
+ { isEquivalence = PropEq.isEquivalence
+ ; assoc = assoc
+ ; ∙-cong = cong₂ _++_
+ }
+ ; identity = ((λ _ → refl) , identity)
+ }
+ }
+ where
+ open PropEq
+ open FunProp _≡_
+
+ identity : RightIdentity [] _++_
+ identity [] = refl
+ identity (x ∷ xs) = cong (_∷_ x) (identity xs)
+
+ assoc : Associative _++_
+ assoc [] ys zs = refl
+ assoc (x ∷ xs) ys zs = cong (_∷_ x) (assoc xs ys zs)
+
+
+
+
+open import Category.Monad
+
+monad : RawMonad List
+monad = record
+ { return = λ x → x ∷ []
+ ; _>>=_ = λ xs f → concat (map f xs)
+ }
+
+monadZero : RawMonadZero List
+monadZero = record
+ { monad = monad
+ ; ∅ = []
+ }
+
+monadPlus : RawMonadPlus List
+monadPlus = record
+ { monadZero = monadZero
+ ; _∣_ = _++_
+ }
+
+
+
+
+private
+ module Monadic {M} (Mon : RawMonad M) where
+
+ open RawMonad Mon
+
+ sequence : ∀ {A : Set} → List (M A) → M (List A)
+ sequence [] = return []
+ sequence (x ∷ xs) = _∷_ <$> x ⊛ sequence xs
+
+ mapM : ∀ {a} {A : Set a} {B} → (A → M B) → List A → M (List B)
+ mapM f = sequence ∘ map f
+
+open Monadic public
+
addfile ./html/Data.Maybe.Core.html
hunk ./html/Data.Maybe.Core.html 1
+
+Data.Maybe.Core{-# OPTIONS --universe-polymorphism #-}
+
+
+
+
+
+
+module Data.Maybe.Core where
+
+open import Level
+
+data Maybe {a} (A : Set a) : Set a where
+ just : (x : A) → Maybe A
+ nothing : Maybe A
+
addfile ./html/Data.Maybe.html
hunk ./html/Data.Maybe.html 1
+
+Data.Maybe
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Data.Maybe where
+
+open import Level
+
+
+
+
+open import Data.Maybe.Core public
+
+
+
+
+open import Data.Bool using (Bool; true; false)
+open import Data.Unit using (⊤)
+
+boolToMaybe : Bool → Maybe ⊤
+boolToMaybe true = just _
+boolToMaybe false = nothing
+
+maybeToBool : ∀ {a} {A : Set a} → Maybe A → Bool
+maybeToBool (just _) = true
+maybeToBool nothing = false
+
+
+
+maybe : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → B → Maybe A → B
+maybe j n (just x) = j x
+maybe j n nothing = n
+
+
+
+
+open import Function
+open import Category.Functor
+open import Category.Monad
+open import Category.Monad.Identity
+
+functor : RawFunctor Maybe
+functor = record
+ { _<$>_ = λ f → maybe (just ∘ f) nothing
+ }
+
+monadT : ∀ {M} → RawMonad M → RawMonad (λ A → M (Maybe A))
+monadT M = record
+ { return = M.return ∘ just
+ ; _>>=_ = λ m f → M._>>=_ m (maybe f (M.return nothing))
+ }
+ where module M = RawMonad M
+
+monad : RawMonad Maybe
+monad = monadT IdentityMonad
+
+monadZero : RawMonadZero Maybe
+monadZero = record
+ { monad = monad
+ ; ∅ = nothing
+ }
+
+monadPlus : RawMonadPlus Maybe
+monadPlus = record
+ { monadZero = monadZero
+ ; _∣_ = _∣_
+ }
+ where
+ _∣_ : ∀ {a : Set} → Maybe a → Maybe a → Maybe a
+ nothing ∣ y = y
+ just x ∣ y = just x
+
+
+
+
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as PropEq
+ using (_≡_; refl)
+
+drop-just : ∀ {A : Set} {x y : A} → just x ≡ just y → x ≡ y
+drop-just refl = refl
+
+decSetoid : {A : Set} → Decidable (_≡_ {A = A}) → DecSetoid _ _
+decSetoid {A} _A-≟_ = PropEq.decSetoid _≟_
+ where
+ _≟_ : Decidable (_≡_ {A = Maybe A})
+ just x ≟ just y with x A-≟ y
+ just x ≟ just .x | yes refl = yes refl
+ just x ≟ just y | no x≢y = no (x≢y ∘ drop-just)
+ just x ≟ nothing = no λ()
+ nothing ≟ just y = no λ()
+ nothing ≟ nothing = yes refl
+
+
+
+
+open import Data.Empty using (⊥)
+import Relation.Nullary.Decidable as Dec
+
+data Any {a} {A : Set a} (P : A → Set a) : Maybe A → Set a where
+ just : ∀ {x} (px : P x) → Any P (just x)
+
+data All {a} {A : Set a} (P : A → Set a) : Maybe A → Set a where
+ just : ∀ {x} (px : P x) → All P (just x)
+ nothing : All P nothing
+
+IsJust : ∀ {a} {A : Set a} → Maybe A → Set a
+IsJust = Any (λ _ → Lift ⊤)
+
+IsNothing : ∀ {a} {A : Set a} → Maybe A → Set a
+IsNothing = All (λ _ → Lift ⊥)
+
+private
+
+ drop-just-Any : ∀ {A} {P : A → Set} {x} → Any P (just x) → P x
+ drop-just-Any (just px) = px
+
+ drop-just-All : ∀ {A} {P : A → Set} {x} → All P (just x) → P x
+ drop-just-All (just px) = px
+
+anyDec : ∀ {A} {P : A → Set} →
+ (∀ x → Dec (P x)) → (x : Maybe A) → Dec (Any P x)
+anyDec p nothing = no λ()
+anyDec p (just x) = Dec.map′ just drop-just-Any (p x)
+
+allDec : ∀ {A} {P : A → Set} →
+ (∀ x → Dec (P x)) → (x : Maybe A) → Dec (All P x)
+allDec p nothing = yes nothing
+allDec p (just x) = Dec.map′ just drop-just-All (p x)
+
addfile ./html/Data.Nat.html
hunk ./html/Data.Nat.html 1
+
+Data.Nat
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Data.Nat where
+
+open import Function
+open import Function.Equality as F using (_⟨$⟩_)
+open import Function.Injection
+ using (Injection; module Injection)
+open import Data.Sum
+open import Data.Empty
+open import Level using (zero)
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as PropEq
+ using (_≡_; refl)
+
+infixl 7 _*_ _⊓_
+infixl 6 _∸_ _⊔_
+
+
+
+
+data ℕ : Set where
+ zero : ℕ
+ suc : (n : ℕ) → ℕ
+
+{-# BUILTIN NATURAL ℕ #-}
+{-# BUILTIN ZERO zero #-}
+{-# BUILTIN SUC suc #-}
+
+infix 4 _≤_ _<_ _≥_ _>_
+
+data _≤_ : Rel ℕ zero where
+ z≤n : ∀ {n} → zero ≤ n
+ s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
+
+_<_ : Rel ℕ zero
+m < n = suc m ≤ n
+
+_≥_ : Rel ℕ zero
+m ≥ n = n ≤ m
+
+_>_ : Rel ℕ zero
+m > n = n < m
+
+
+
+
+infix 4 _≤′_ _<′_ _≥′_ _>′_
+
+data _≤′_ : Rel ℕ zero where
+ ≤′-refl : ∀ {n} → n ≤′ n
+ ≤′-step : ∀ {m n} (m≤′n : m ≤′ n) → m ≤′ suc n
+
+_<′_ : Rel ℕ zero
+m <′ n = suc m ≤′ n
+
+_≥′_ : Rel ℕ zero
+m ≥′ n = n ≤′ m
+
+_>′_ : Rel ℕ zero
+m >′ n = n <′ m
+
+
+
+
+fold : {a : Set} → a → (a → a) → ℕ → a
+fold z s zero = z
+fold z s (suc n) = s (fold z s n)
+
+module GeneralisedArithmetic {a : Set} (0# : a) (1+ : a → a) where
+
+ add : ℕ → a → a
+ add n z = fold z 1+ n
+
+ mul : (+ : a → a → a) → (ℕ → a → a)
+ mul _+_ n x = fold 0# (λ s → x + s) n
+
+
+
+
+pred : ℕ → ℕ
+pred zero = zero
+pred (suc n) = n
+
+infixl 6 _+_ _+⋎_
+
+_+_ : ℕ → ℕ → ℕ
+zero + n = n
+suc m + n = suc (m + n)
+
+
+
+_+⋎_ : ℕ → ℕ → ℕ
+zero +⋎ n = n
+suc m +⋎ n = suc (n +⋎ m)
+
+{-# BUILTIN NATPLUS _+_ #-}
+
+_∸_ : ℕ → ℕ → ℕ
+m ∸ zero = m
+zero ∸ suc n = zero
+suc m ∸ suc n = m ∸ n
+
+{-# BUILTIN NATMINUS _∸_ #-}
+
+_*_ : ℕ → ℕ → ℕ
+zero * n = zero
+suc m * n = n + m * n
+
+{-# BUILTIN NATTIMES _*_ #-}
+
+
+
+_⊔_ : ℕ → ℕ → ℕ
+zero ⊔ n = n
+suc m ⊔ zero = suc m
+suc m ⊔ suc n = suc (m ⊔ n)
+
+
+
+_⊓_ : ℕ → ℕ → ℕ
+zero ⊓ n = zero
+suc m ⊓ zero = zero
+suc m ⊓ suc n = suc (m ⊓ n)
+
+
+
+⌊_/2⌋ : ℕ → ℕ
+⌊ 0 /2⌋ = 0
+⌊ 1 /2⌋ = 0
+⌊ suc (suc n) /2⌋ = suc ⌊ n /2⌋
+
+
+
+⌈_/2⌉ : ℕ → ℕ
+⌈ n /2⌉ = ⌊ suc n /2⌋
+
+
+
+
+infix 4 _≟_
+
+_≟_ : Decidable {A = ℕ} _≡_
+zero ≟ zero = yes refl
+suc m ≟ suc n with m ≟ n
+suc m ≟ suc .m | yes refl = yes refl
+suc m ≟ suc n | no prf = no (prf ∘ PropEq.cong pred)
+zero ≟ suc n = no λ()
+suc m ≟ zero = no λ()
+
+≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
+≤-pred (s≤s m≤n) = m≤n
+
+_≤?_ : Decidable _≤_
+zero ≤? _ = yes z≤n
+suc m ≤? zero = no λ()
+suc m ≤? suc n with m ≤? n
+... | yes m≤n = yes (s≤s m≤n)
+... | no m≰n = no (m≰n ∘ ≤-pred)
+
+
+
+
+data Ordering : Rel ℕ zero where
+ less : ∀ m k → Ordering m (suc (m + k))
+ equal : ∀ m → Ordering m m
+ greater : ∀ m k → Ordering (suc (m + k)) m
+
+compare : ∀ m n → Ordering m n
+compare zero zero = equal zero
+compare (suc m) zero = greater zero m
+compare zero (suc n) = less zero n
+compare (suc m) (suc n) with compare m n
+compare (suc .m) (suc .(suc m + k)) | less m k = less (suc m) k
+compare (suc .m) (suc .m) | equal m = equal (suc m)
+compare (suc .(suc m + k)) (suc .m) | greater m k = greater (suc m) k
+
+
+
+
+eq? : ∀ {s₁ s₂} {S : Setoid s₁ s₂} →
+ Injection S (PropEq.setoid ℕ) → Decidable (Setoid._≈_ S)
+eq? inj x y with to ⟨$⟩ x ≟ to ⟨$⟩ y where open Injection inj
+... | yes tox≡toy = yes (Injection.injective inj tox≡toy)
+... | no tox≢toy = no (tox≢toy ∘ F.cong (Injection.to inj))
+
+
+
+
+decTotalOrder : DecTotalOrder _ _ _
+decTotalOrder = record
+ { Carrier = ℕ
+ ; _≈_ = _≡_
+ ; _≤_ = _≤_
+ ; isDecTotalOrder = record
+ { isTotalOrder = record
+ { isPartialOrder = record
+ { isPreorder = record
+ { isEquivalence = PropEq.isEquivalence
+ ; reflexive = refl′
+ ; trans = trans
+ }
+ ; antisym = antisym
+ }
+ ; total = total
+ }
+ ; _≟_ = _≟_
+ ; _≤?_ = _≤?_
+ }
+ }
+ where
+ refl′ : _≡_ ⇒ _≤_
+ refl′ {zero} refl = z≤n
+ refl′ {suc m} refl = s≤s (refl′ refl)
+
+ antisym : Antisymmetric _≡_ _≤_
+ antisym z≤n z≤n = refl
+ antisym (s≤s m≤n) (s≤s n≤m) with antisym m≤n n≤m
+ ... | refl = refl
+
+ trans : Transitive _≤_
+ trans z≤n _ = z≤n
+ trans (s≤s m≤n) (s≤s n≤o) = s≤s (trans m≤n n≤o)
+
+ total : Total _≤_
+ total zero _ = inj₁ z≤n
+ total _ zero = inj₂ z≤n
+ total (suc m) (suc n) with total m n
+ ... | inj₁ m≤n = inj₁ (s≤s m≤n)
+ ... | inj₂ n≤m = inj₂ (s≤s n≤m)
+
+import Relation.Binary.PartialOrderReasoning as POR
+module ≤-Reasoning where
+ open POR (DecTotalOrder.poset decTotalOrder) public
+ renaming (_≈⟨_⟩_ to _≡⟨_⟩_)
+
+ infixr 2 _<⟨_⟩_
+
+ _<⟨_⟩_ : ∀ x {y z} → x < y → y IsRelatedTo z → suc x IsRelatedTo z
+ x <⟨ x<y ⟩ y≤z = suc x ≤⟨ x<y ⟩ y≤z
+
addfile ./html/Data.Product.html
hunk ./html/Data.Product.html 1
+
+Data.Product
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Data.Product where
+
+open import Function
+open import Level
+open import Relation.Nullary
+
+infixr 4 _,_ _,′_
+infix 4 ,_
+infixr 2 _×_ _-×-_ _-,-_
+
+
+
+
+record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
+ constructor _,_
+ field
+ proj₁ : A
+ proj₂ : B proj₁
+
+open Σ public
+
+∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
+∃ = Σ _
+
+∄ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
+∄ P = ¬ ∃ P
+
+∃₂ : ∀ {a b c} {A : Set a} {B : A → Set b}
+ (C : (x : A) → B x → Set c) → Set (a ⊔ b ⊔ c)
+∃₂ C = ∃ λ a → ∃ λ b → C a b
+
+_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
+A × B = Σ A (λ _ → B)
+
+_,′_ : ∀ {a b} {A : Set a} {B : Set b} → A → B → A × B
+_,′_ = _,_
+
+
+
+
+
+
+∃! : ∀ {a b ℓ} {A : Set a} →
+ (A → A → Set ℓ) → (A → Set b) → Set (a ⊔ b ⊔ ℓ)
+∃! _≈_ B = ∃ λ x → B x × (∀ {y} → B y → x ≈ y)
+
+
+
+
+
+
+,_ : ∀ {a b} {A : Set a} {B : A → Set b} {x} → B x → ∃ B
+, y = _ , y
+
+<_,_> : ∀ {a b c} {A : Set a} {B : A → Set b} {C : ∀ {x} → B x → Set c}
+ (f : (x : A) → B x) → ((x : A) → C (f x)) →
+ ((x : A) → Σ (B x) C)
+< f , g > x = (f x , g x)
+
+map : ∀ {a b p q}
+ {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} →
+ (f : A → B) → (∀ {x} → P x → Q (f x)) →
+ Σ A P → Σ B Q
+map f g = < f ∘ proj₁ , g ∘ proj₂ >
+
+zip : ∀ {a b c p q r}
+ {A : Set a} {B : Set b} {C : Set c}
+ {P : A → Set p} {Q : B → Set q} {R : C → Set r} →
+ (_∙_ : A → B → C) →
+ (∀ {x y} → P x → Q y → R (x ∙ y)) →
+ Σ A P → Σ B Q → Σ C R
+zip _∙_ _∘_ p₁ p₂ = (proj₁ p₁ ∙ proj₁ p₂ , proj₂ p₁ ∘ proj₂ p₂)
+
+swap : ∀ {a b} {A : Set a} {B : Set b} → A × B → B × A
+swap = < proj₂ , proj₁ >
+
+_-×-_ : ∀ {a b i j} {A : Set a} {B : Set b} →
+ (A → B → Set i) → (A → B → Set j) → (A → B → Set _)
+f -×- g = f -[ _×_ ]- g
+
+_-,-_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
+ (A → B → C) → (A → B → D) → (A → B → C × D)
+f -,- g = f -[ _,_ ]- g
+
+curry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
+ ((p : Σ A B) → C p) →
+ ((x : A) → (y : B x) → C (x , y))
+curry f x y = f (x , y)
+
+uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
+ ((x : A) → (y : B x) → C (x , y)) →
+ ((p : Σ A B) → C p)
+uncurry f p = f (proj₁ p) (proj₂ p)
+
+uncurry′ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
+ (A → B → C) → (A × B → C)
+uncurry′ = uncurry
+
addfile ./html/Data.String.html
hunk ./html/Data.String.html 1
+
+Data.String
+
+
+
+module Data.String where
+
+open import Data.List as List using (_∷_; []; List)
+open import Data.Vec as Vec using (Vec)
+open import Data.Colist as Colist using (Colist)
+open import Data.Char using (Char)
+open import Data.Bool using (Bool; true; false)
+open import Function
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
+open import Relation.Binary.PropositionalEquality.TrustMe
+
+
+
+
+
+
+postulate
+ String : Set
+
+{-# BUILTIN STRING String #-}
+{-# COMPILED_TYPE String String #-}
+
+
+
+Costring : Set
+Costring = Colist Char
+
+
+
+
+private
+ primitive
+ primStringAppend : String → String → String
+ primStringToList : String → List Char
+ primStringFromList : List Char → String
+ primStringEquality : String → String → Bool
+
+infixr 5 _++_
+
+_++_ : String → String → String
+_++_ = primStringAppend
+
+toList : String → List Char
+toList = primStringToList
+
+fromList : List Char → String
+fromList = primStringFromList
+
+toVec : (s : String) → Vec Char (List.length (toList s))
+toVec s = Vec.fromList (toList s)
+
+toCostring : String → Costring
+toCostring = Colist.fromList ∘ toList
+
+unlines : List String → String
+unlines [] = ""
+unlines (x ∷ xs) = x ++ "\n" ++ unlines xs
+
+infix 4 _==_
+
+_==_ : String → String → Bool
+_==_ = primStringEquality
+
+_≟_ : Decidable {A = String} _≡_
+s₁ ≟ s₂ with s₁ == s₂
+... | true = yes trustMe
+... | false = no whatever
+ where postulate whatever : _
+
+setoid : Setoid _ _
+setoid = PropEq.setoid String
+
+decSetoid : DecSetoid _ _
+decSetoid = PropEq.decSetoid _≟_
+
addfile ./html/Data.Sum.html
hunk ./html/Data.Sum.html 1
+
+Data.Sum
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Data.Sum where
+
+open import Function
+open import Data.Maybe.Core
+open import Level
+
+
+
+
+infixr 1 _⊎_
+
+data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
+ inj₁ : (x : A) → A ⊎ B
+ inj₂ : (y : B) → A ⊎ B
+
+
+
+
+[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : A ⊎ B → Set c} →
+ ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
+ ((x : A ⊎ B) → C x)
+[ f , g ] (inj₁ x) = f x
+[ f , g ] (inj₂ y) = g y
+
+[_,_]′ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
+ (A → C) → (B → C) → (A ⊎ B → C)
+[_,_]′ = [_,_]
+
+map : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
+ (A → C) → (B → D) → (A ⊎ B → C ⊎ D)
+map f g = [ inj₁ ∘ f , inj₂ ∘ g ]
+
+infixr 1 _-⊎-_
+
+_-⊎-_ : ∀ {a b c d} {A : Set a} {B : Set b} →
+ (A → B → Set c) → (A → B → Set d) → (A → B → Set (c ⊔ d))
+f -⊎- g = f -[ _⊎_ ]- g
+
+isInj₁ : {A B : Set} → A ⊎ B → Maybe A
+isInj₁ (inj₁ x) = just x
+isInj₁ (inj₂ y) = nothing
+
+isInj₂ : {A B : Set} → A ⊎ B → Maybe B
+isInj₂ (inj₁ x) = nothing
+isInj₂ (inj₂ y) = just y
+
addfile ./html/Data.Unit.html
hunk ./html/Data.Unit.html 1
+
+Data.Unit
+
+
+
+module Data.Unit where
+
+open import Data.Sum
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as PropEq
+ using (_≡_; refl)
+
+
+
+
+
+
+record ⊤ : Set where
+ constructor tt
+
+record _≤_ (x y : ⊤) : Set where
+
+
+
+
+_≟_ : Decidable {A = ⊤} _≡_
+_ ≟ _ = yes refl
+
+_≤?_ : Decidable _≤_
+_ ≤? _ = yes _
+
+total : Total _≤_
+total _ _ = inj₁ _
+
+
+
+
+preorder : Preorder _ _ _
+preorder = PropEq.preorder ⊤
+
+setoid : Setoid _ _
+setoid = PropEq.setoid ⊤
+
+decTotalOrder : DecTotalOrder _ _ _
+decTotalOrder = record
+ { Carrier = ⊤
+ ; _≈_ = _≡_
+ ; _≤_ = _≤_
+ ; isDecTotalOrder = record
+ { isTotalOrder = record
+ { isPartialOrder = record
+ { isPreorder = record
+ { isEquivalence = PropEq.isEquivalence
+ ; reflexive = λ _ → _
+ ; trans = λ _ _ → _
+ }
+ ; antisym = antisym
+ }
+ ; total = total
+ }
+ ; _≟_ = _≟_
+ ; _≤?_ = _≤?_
+ }
+ }
+ where
+ antisym : Antisymmetric _≡_ _≤_
+ antisym _ _ = refl
+
+decSetoid : DecSetoid _ _
+decSetoid = DecTotalOrder.Eq.decSetoid decTotalOrder
+
+poset : Poset _ _ _
+poset = DecTotalOrder.poset decTotalOrder
+
addfile ./html/Data.Vec.html
hunk ./html/Data.Vec.html 1
+
+Data.Vec
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Data.Vec where
+
+open import Data.Nat
+open import Data.Fin using (Fin; zero; suc)
+open import Data.List as List using (List)
+open import Data.Product using (∃; ∃₂; _×_; _,_)
+open import Level
+open import Relation.Binary.PropositionalEquality
+
+
+
+
+infixr 5 _∷_
+
+data Vec {a} (A : Set a) : ℕ → Set a where
+ [] : Vec A zero
+ _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
+
+infix 4 _∈_
+
+data _∈_ {a} {A : Set a} : A → {n : ℕ} → Vec A n → Set a where
+ here : ∀ {n} {x} {xs : Vec A n} → x ∈ x ∷ xs
+ there : ∀ {n} {x y} {xs : Vec A n} (x∈xs : x ∈ xs) → x ∈ y ∷ xs
+
+infix 4 _[_]=_
+
+data _[_]=_ {a} {A : Set a} :
+ {n : ℕ} → Vec A n → Fin n → A → Set a where
+ here : ∀ {n} {x} {xs : Vec A n} → x ∷ xs [ zero ]= x
+ there : ∀ {n} {i} {x y} {xs : Vec A n}
+ (xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x
+
+
+
+
+head : ∀ {a n} {A : Set a} → Vec A (1 + n) → A
+head (x ∷ xs) = x
+
+tail : ∀ {a n} {A : Set a} → Vec A (1 + n) → Vec A n
+tail (x ∷ xs) = xs
+
+[_] : ∀ {a} {A : Set a} → A → Vec A 1
+[ x ] = x ∷ []
+
+infixr 5 _++_
+
+_++_ : ∀ {a m n} {A : Set a} → Vec A m → Vec A n → Vec A (m + n)
+[] ++ ys = ys
+(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
+
+map : ∀ {a b n} {A : Set a} {B : Set b} →
+ (A → B) → Vec A n → Vec B n
+map f [] = []
+map f (x ∷ xs) = f x ∷ map f xs
+
+zipWith : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c} →
+ (A → B → C) → Vec A n → Vec B n → Vec C n
+zipWith _⊕_ [] [] = []
+zipWith _⊕_ (x ∷ xs) (y ∷ ys) = (x ⊕ y) ∷ zipWith _⊕_ xs ys
+
+zip : ∀ {a b n} {A : Set a} {B : Set b} →
+ Vec A n → Vec B n → Vec (A × B) n
+zip = zipWith _,_
+
+replicate : ∀ {a n} {A : Set a} → A → Vec A n
+replicate {n = zero} x = []
+replicate {n = suc n} x = x ∷ replicate x
+
+foldr : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
+ (∀ {n} → A → B n → B (suc n)) →
+ B zero →
+ Vec A m → B m
+foldr b _⊕_ n [] = n
+foldr b _⊕_ n (x ∷ xs) = x ⊕ foldr b _⊕_ n xs
+
+foldr₁ : ∀ {a} {A : Set a} {m} →
+ (A → A → A) → Vec A (suc m) → A
+foldr₁ _⊕_ (x ∷ []) = x
+foldr₁ _⊕_ (x ∷ y ∷ ys) = x ⊕ foldr₁ _⊕_ (y ∷ ys)
+
+foldl : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
+ (∀ {n} → B n → A → B (suc n)) →
+ B zero →
+ Vec A m → B m
+foldl b _⊕_ n [] = n
+foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs
+
+foldl₁ : ∀ {a} {A : Set a} {m} →
+ (A → A → A) → Vec A (suc m) → A
+foldl₁ _⊕_ (x ∷ xs) = foldl _ _⊕_ x xs
+
+concat : ∀ {a m n} {A : Set a} →
+ Vec (Vec A m) n → Vec A (n * m)
+concat [] = []
+concat (xs ∷ xss) = xs ++ concat xss
+
+splitAt : ∀ {a} {A : Set a} m {n} (xs : Vec A (m + n)) →
+ ∃₂ λ (ys : Vec A m) (zs : Vec A n) → xs ≡ ys ++ zs
+splitAt zero xs = ([] , xs , refl)
+splitAt (suc m) (x ∷ xs) with splitAt m xs
+splitAt (suc m) (x ∷ .(ys ++ zs)) | (ys , zs , refl) =
+ ((x ∷ ys) , zs , refl)
+
+take : ∀ {a} {A : Set a} m {n} → Vec A (m + n) → Vec A m
+take m xs with splitAt m xs
+take m .(ys ++ zs) | (ys , zs , refl) = ys
+
+drop : ∀ {a} {A : Set a} m {n} → Vec A (m + n) → Vec A n
+drop m xs with splitAt m xs
+drop m .(ys ++ zs) | (ys , zs , refl) = zs
+
+group : ∀ {a} {A : Set a} n k (xs : Vec A (n * k)) →
+ ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss
+group zero k [] = ([] , refl)
+group (suc n) k xs with splitAt k xs
+group (suc n) k .(ys ++ zs) | (ys , zs , refl) with group n k zs
+group (suc n) k .(ys ++ concat zss) | (ys , ._ , refl) | (zss , refl) =
+ ((ys ∷ zss) , refl)
+
+reverse : ∀ {a n} {A : Set a} → Vec A n → Vec A n
+reverse {A = A} = foldl (Vec A) (λ rev x → x ∷ rev) []
+
+sum : ∀ {n} → Vec ℕ n → ℕ
+sum = foldr _ _+_ 0
+
+toList : ∀ {a n} {A : Set a} → Vec A n → List A
+toList [] = List.[]
+toList (x ∷ xs) = List._∷_ x (toList xs)
+
+fromList : ∀ {a} {A : Set a} → (xs : List A) → Vec A (List.length xs)
+fromList List.[] = []
+fromList (List._∷_ x xs) = x ∷ fromList xs
+
+
+
+infixl 5 _∷ʳ_
+
+_∷ʳ_ : ∀ {a n} {A : Set a} → Vec A n → A → Vec A (1 + n)
+[] ∷ʳ y = [ y ]
+(x ∷ xs) ∷ʳ y = x ∷ (xs ∷ʳ y)
+
+initLast : ∀ {a n} {A : Set a} (xs : Vec A (1 + n)) →
+ ∃₂ λ (ys : Vec A n) (y : A) → xs ≡ ys ∷ʳ y
+initLast {n = zero} (x ∷ []) = ([] , x , refl)
+initLast {n = suc n} (x ∷ xs) with initLast xs
+initLast {n = suc n} (x ∷ .(ys ∷ʳ y)) | (ys , y , refl) =
+ ((x ∷ ys) , y , refl)
+
+init : ∀ {a n} {A : Set a} → Vec A (1 + n) → Vec A n
+init xs with initLast xs
+init .(ys ∷ʳ y) | (ys , y , refl) = ys
+
+last : ∀ {a n} {A : Set a} → Vec A (1 + n) → A
+last xs with initLast xs
+last .(ys ∷ʳ y) | (ys , y , refl) = y
+
+infixl 1 _>>=_
+
+_>>=_ : ∀ {a b m n} {A : Set a} {B : Set b} →
+ Vec A m → (A → Vec B n) → Vec B (m * n)
+xs >>= f = concat (map f xs)
+
+infixl 4 _⊛_
+
+_⊛_ : ∀ {a b m n} {A : Set a} {B : Set b} →
+ Vec (A → B) m → Vec A n → Vec B (m * n)
+fs ⊛ xs = fs >>= λ f → map f xs
+
+
+
+infixr 5 _⋎_
+
+_⋎_ : ∀ {a m n} {A : Set a} →
+ Vec A m → Vec A n → Vec A (m +⋎ n)
+[] ⋎ ys = ys
+(x ∷ xs) ⋎ ys = x ∷ (ys ⋎ xs)
+
+lookup : ∀ {a n} {A : Set a} → Fin n → Vec A n → A
+lookup zero (x ∷ xs) = x
+lookup (suc i) (x ∷ xs) = lookup i xs
+
+
+
+infixl 6 _[_]≔_
+
+_[_]≔_ : ∀ {a n} {A : Set a} → Vec A n → Fin n → A → Vec A n
+[] [ () ]≔ y
+(x ∷ xs) [ zero ]≔ y = y ∷ xs
+(x ∷ xs) [ suc i ]≔ y = x ∷ xs [ i ]≔ y
+
+
+
+
+allFin : ∀ n → Vec (Fin n) n
+allFin zero = []
+allFin (suc n) = zero ∷ map suc (allFin n)
+
addfile ./html/Database.html
hunk ./html/Database.html 1
+
+Database
+module Database where
+
+open import Function
+import IO.Primitive as IO
+open IO using (IO)
+open import Maybe
+open import List
+open import Data.Bool
+open import Data.String as String renaming (_++_ to _&_)
+open import Data.Product
+open import Foreign.Haskell
+open import Category.Monad
+open import Category.Monad.Indexed
+
+open import Util hiding (_<$>_)
+open import Schema
+
+MonadIO : RawMonad IO
+MonadIO = record { return = IO.return
+ ; _>>=_ = IO._>>=_
+ }
+
+open RawMonad MonadIO
+
+{-# IMPORT Database.Firebird #-}
+
+ServerName = String
+UserName = String
+Password = String
+
+postulate
+ RawHandle : Set
+ hs_connect : ServerName → UserName → Password → IO (Maybe RawHandle)
+ hs_tableInfo : RawHandle → TableName → IO (List HsColumnInfo)
+ hs_disconnect : RawHandle → IO Unit
+
+{-# COMPILED_TYPE RawHandle DbHandle #-}
+
+{-# COMPILED hs_connect dbConnect #-}
+{-# COMPILED hs_tableInfo tableInfo #-}
+{-# COMPILED hs_disconnect dbDisconnect #-}
+
+data Db (s₁ s₂ : Schema)(A : Set) : Set where
+ mkDb : (RawHandle → IO A) → Db s₁ s₂ A
+
+unDb : ∀ {A s₁ s₂} → Db s₁ s₂ A → RawHandle → IO A
+unDb (mkDb f) = f
+
+MonadDb : RawIMonad Db
+MonadDb = record
+ { return = λ x → mkDb λ _ → return x
+ ; _>>=_ = λ m f → mkDb λ h → unDb m h >>= λ x → unDb (f x) h
+ }
+
+open RawIMonad MonadDb using () renaming (return to return′; _>>=_ to _>>=′_; _>>_ to _>>′_)
+
+liftIO : ∀ {A s} → IO A → Db s s A
+liftIO io = mkDb λ h → io
+
+data Handle (s : Schema) : Set where
+ handle : RawHandle → Handle s
+
+showType : FieldType → String
+showType (string n) = primStringAppend "STRING " (showInteger (primNatToInteger n))
+showType number = "NUMBER"
+showType date = "DATE"
+showType time = "TIME"
+
+mapM : ∀ {A B} → (A → IO B) → List A → IO (List B)
+mapM f [] = return []
+mapM f (x ∷ xs) = f x >>= λ y → mapM f xs >>= λ ys → return (y ∷ ys)
+
+mapM₋ : ∀ {A B} → (A → IO B) → List A → IO Unit
+mapM₋ f xs = mapM f xs >> return unit
+
+putStr : String → IO Unit
+putStr = IO.putStr ∘ fromColist ∘ String.toCostring
+
+putStrLn : String → IO Unit
+putStrLn = IO.putStrLn ∘ fromColist ∘ String.toCostring
+
+printCol : Attribute → IO Unit
+printCol (name , type) =
+ mapM₋ putStr (name ∷ " : " ∷ showType type ∷ "\n" ∷ [])
+
+printTableInfo : TableType → IO Unit
+printTableInfo = mapM₋ printCol
+
+checkTable : RawHandle → TableName × TableType → IO Bool
+checkTable h (name , type) =
+ hs_tableInfo h name >>= λ info →
+ if parseTableInfo info =TT= type
+ then return true
+ else putStrLn ("Schema mismatch for table " & name) >>
+ putStrLn "Expected:" >>
+ printTableInfo type >>
+ putStrLn "Found:" >>
+ printTableInfo (parseTableInfo info) >>
+ return false
+
+checkSchema : RawHandle → Schema → IO Bool
+checkSchema h s =
+ putStrLn "Checking schema..." >>
+ and <$> mapM (checkTable h) s
+
+withDatabase : ∀ {s′ A} → ServerName → UserName → Password →
+ (s : Schema) → Db s s′ A → IO (Maybe A)
+withDatabase server user pass s action =
+ putStrLn ("Connecting to " & server & "...") >>
+ hs_connect server user pass >>= λ mh →
+ withMaybe mh (return nothing) λ h →
+ checkSchema h s >>= λ ok →
+ if ok then just <$> unDb action h >>= (λ x → hs_disconnect h >> return x)
+ else return nothing
+
+withRawHandle : ∀ {A s₁ s₂} → (RawHandle → Db s₁ s₂ A) → Db s₁ s₂ A
+withRawHandle f = mkDb λ h → unDb (f h) h
+
addfile ./html/Eq.html
hunk ./html/Eq.html 1
+
+Eq
+
+module Eq where
+
+import Data.String as String
+open String using (String)
+open import Data.Nat
+open import Data.Bool
+
+data EqType : Set where
+ nat : EqType
+ bool : EqType
+ string : EqType
+
+El : EqType → Set
+El nat = ℕ
+El bool = Bool
+El string = String
+
+_==_ : ∀ {u} → El u → El u → Bool
+_==_ {nat} zero zero = true
+_==_ {nat} zero (suc n) = false
+_==_ {nat} (suc n) zero = false
+_==_ {nat} (suc n) (suc m) = n == m
+_==_ {bool} true y = y
+_==_ {bool} false y = not y
+_==_ {string} x y = String._==_ x y
addfile ./html/ExampleDatabase.html
hunk ./html/ExampleDatabase.html 1
+
+ExampleDatabase
+module ExampleDatabase where
+
+open import Data.String
+open import Data.Nat
+open import List
+open import Data.Product
+open import Schema
+
+departmentsTable : TableType
+departmentsTable =
+ ("DNAME" , string 100) ∷
+ ("ADDRESS" , string 100) ∷
+ []
+
+programsTable : TableType
+programsTable =
+ ("PNAME" , string 100) ∷
+ ("ABBR" , string 10) ∷
+ []
+
+branchesTable : TableType
+branchesTable =
+ ("BID" , number) ∷
+ ("BNAME" , string 100) ∷
+ ("BPROGRAM" , string 100) ∷
+ []
+
+studentsTable : TableType
+studentsTable =
+ ("SID" , number) ∷
+ ("SNAME" , string 100) ∷
+ ("SBRANCH" , number) ∷
+ []
+
+coursesTable : TableType
+coursesTable =
+ ("CODE" , string 10) ∷
+ ("CNAME" , string 100) ∷
+ ("CREDIT" , number) ∷
+ ("CDEPARTMENT" , string 100) ∷
+ ("NSTUDENTS" , number) ∷
+ []
+
+classifiedCoursesTable : TableType
+classifiedCoursesTable =
+ ("CCOURSE" , string 10) ∷
+ ("CTYPE" , string 20) ∷
+ []
+
+departmentsProgramsTable : TableType
+departmentsProgramsTable =
+ ("DPDEPARTMENT" , string 100) ∷
+ ("DPPROGRAM" , string 100) ∷
+ []
+
+branchRecommendedCoursesTable : TableType
+branchRecommendedCoursesTable =
+ ("RCOURSE" , string 10) ∷
+ ("RBRANCH" , number) ∷
+ []
+
+branchMandatoryCoursesTable : TableType
+branchMandatoryCoursesTable =
+ ("BMCOURSE" , string 10) ∷
+ ("BMBRANCH" , number) ∷
+ []
+
+programMandatoryCoursesTable : TableType
+programMandatoryCoursesTable =
+ ("PMCOURSE" , string 10) ∷
+ ("PMPROGRAM" , string 100) ∷
+ []
+
+requiredCoursesTable : TableType
+requiredCoursesTable =
+ ("DEPENDENT" , string 10) ∷
+ ("REQUIRED" , string 10) ∷
+ []
+
+coursesStudentsTable : TableType
+coursesStudentsTable =
+ ("CSCOURSE" , string 10) ∷
+ ("CSSTUDENT" , number) ∷
+ ("EVENTDATE" , string 19) ∷
+ ("STATUS" , number) ∷
+ []
+
+universitySchema : Schema
+universitySchema =
+ ("Departments" , departmentsTable) ∷
+ ("Programs" , programsTable) ∷
+ ("Branches" , branchesTable) ∷
+ ("Students" , studentsTable) ∷
+ ("Courses" , coursesTable) ∷
+ ("ClassifiedCourses" , classifiedCoursesTable) ∷
+ ("DepartmentsPrograms" , departmentsProgramsTable) ∷
+ ("BranchRecommendedCourses" , branchRecommendedCoursesTable) ∷
+ ("BranchMandatoryCourses" , branchMandatoryCoursesTable) ∷
+ ("ProgramMandatoryCourses" , programMandatoryCoursesTable) ∷
+ ("RequiredCourses" , requiredCoursesTable) ∷
+ ("CoursesStudents" , coursesStudentsTable) ∷
+ []
+
addfile ./html/Foreign.Haskell.html
hunk ./html/Foreign.Haskell.html 1
+
+Foreign.Haskell
+
+
+
+module Foreign.Haskell where
+
+open import Coinduction
+open import Data.Char using (Char)
+open import Data.Colist as C using ([]; _∷_)
+open import Function using (_∘_)
+open import Data.String as String using (String)
+
+
+
+
+
+
+data Unit : Set where
+ unit : Unit
+
+{-# COMPILED_DATA Unit () () #-}
+
+
+
+infixr 5 _∷_
+
+codata Colist (A : Set) : Set where
+ [] : Colist A
+ _∷_ : (x : A) (xs : Colist A) → Colist A
+
+{-# COMPILED_DATA Colist [] [] (:) #-}
+
+fromColist : ∀ {A} → C.Colist A → Colist A
+fromColist [] = []
+fromColist (x ∷ xs) = x ∷ fromColist (♭ xs)
+
+toColist : ∀ {A} → Colist A → C.Colist A
+toColist [] = []
+toColist (x ∷ xs) = x ∷ ♯ toColist xs
+
+fromString : String → Colist Char
+fromString = fromColist ∘ String.toCostring
+
addfile ./html/Function.Equality.html
hunk ./html/Function.Equality.html 1
+
+Function.Equality
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Function.Equality where
+
+open import Function as Fun using (_on_)
+open import Level
+import Relation.Binary as B
+import Relation.Binary.Indexed as I
+
+
+
+
+record Π {f₁ f₂ t₁ t₂}
+ (From : B.Setoid f₁ f₂)
+ (To : I.Setoid (B.Setoid.Carrier From) t₁ t₂) :
+ Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
+ open I using (_=[_]⇒_)
+ infixl 5 _⟨$⟩_
+ field
+ _⟨$⟩_ : (x : B.Setoid.Carrier From) → I.Setoid.Carrier To x
+ cong : B.Setoid._≈_ From =[ _⟨$⟩_ ]⇒ I.Setoid._≈_ To
+
+open Π public
+
+infixr 0 _⟶_
+
+_⟶_ : ∀ {f₁ f₂ t₁ t₂} → B.Setoid f₁ f₂ → B.Setoid t₁ t₂ → Set _
+From ⟶ To = Π From (B.Setoid.indexedSetoid To)
+
+
+
+id : ∀ {a₁ a₂} {A : B.Setoid a₁ a₂} → A ⟶ A
+id = record { _⟨$⟩_ = Fun.id; cong = Fun.id }
+
+infixr 9 _∘_
+
+_∘_ : ∀ {a₁ a₂} {A : B.Setoid a₁ a₂}
+ {b₁ b₂} {B : B.Setoid b₁ b₂}
+ {c₁ c₂} {C : B.Setoid c₁ c₂} →
+ B ⟶ C → A ⟶ B → A ⟶ C
+f ∘ g = record
+ { _⟨$⟩_ = Fun._∘_ (_⟨$⟩_ f) (_⟨$⟩_ g)
+ ; cong = Fun._∘_ (cong f) (cong g)
+ }
+
+
+
+const : ∀ {a₁ a₂} {A : B.Setoid a₁ a₂}
+ {b₁ b₂} {B : B.Setoid b₁ b₂} →
+ B.Setoid.Carrier B → A ⟶ B
+const {B = B} b = record
+ { _⟨$⟩_ = Fun.const b
+ ; cong = Fun.const (B.Setoid.refl B)
+ }
+
+
+
+
+
+
+setoid : ∀ {f₁ f₂ t₁ t₂}
+ (From : B.Setoid f₁ f₂) →
+ I.Setoid (B.Setoid.Carrier From) t₁ t₂ →
+ B.Setoid _ _
+setoid From To = record
+ { Carrier = Π From To
+ ; _≈_ = λ f g → ∀ {x y} → x ≈₁ y → f ⟨$⟩ x ≈₂ g ⟨$⟩ y
+ ; isEquivalence = record
+ { refl = λ {f} → cong f
+ ; sym = λ f∼g x∼y → To.sym (f∼g (From.sym x∼y))
+ ; trans = λ f∼g g∼h x∼y → To.trans (f∼g From.refl) (g∼h x∼y)
+ }
+ }
+ where
+ open module From = B.Setoid From using () renaming (_≈_ to _≈₁_)
+ open module To = I.Setoid To using () renaming (_≈_ to _≈₂_)
+
+
+
+infixr 0 _⇨_
+
+_⇨_ : ∀ {f₁ f₂ t₁ t₂} → B.Setoid f₁ f₂ → B.Setoid t₁ t₂ → B.Setoid _ _
+From ⇨ To = setoid From (B.Setoid.indexedSetoid To)
+
+
+
+
+≡-setoid : ∀ {f t₁ t₂} (From : Set f) → I.Setoid From t₁ t₂ → B.Setoid _ _
+≡-setoid From To = record
+ { Carrier = (x : From) → Carrier x
+ ; _≈_ = λ f g → ∀ x → f x ≈ g x
+ ; isEquivalence = record
+ { refl = λ {f} x → refl
+ ; sym = λ f∼g x → sym (f∼g x)
+ ; trans = λ f∼g g∼h x → trans (f∼g x) (g∼h x)
+ }
+ } where open I.Setoid To
+
addfile ./html/Function.Equivalence.html
hunk ./html/Function.Equivalence.html 1
+
+Function.Equivalence
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Function.Equivalence where
+
+open import Function using (flip)
+open import Function.Equality as F
+ using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
+open import Level
+open import Relation.Binary
+import Relation.Binary.PropositionalEquality as P
+
+
+
+record Equivalent {f₁ f₂ t₁ t₂}
+ (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
+ Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
+ field
+ to : From ⟶ To
+ from : To ⟶ From
+
+
+
+infix 3 _⇔_
+
+_⇔_ : ∀ {f t} → Set f → Set t → Set _
+From ⇔ To = Equivalent (P.setoid From) (P.setoid To)
+
+equivalent : ∀ {f t} {From : Set f} {To : Set t} →
+ (From → To) → (To → From) → From ⇔ To
+equivalent to from = record { to = P.→-to-⟶ to; from = P.→-to-⟶ from }
+
+
+
+
+map : ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
+ {f₁′ f₂′ t₁′ t₂′}
+ {From′ : Setoid f₁′ f₂′} {To′ : Setoid t₁′ t₂′} →
+ ((From ⟶ To) → (From′ ⟶ To′)) →
+ ((To ⟶ From) → (To′ ⟶ From′)) →
+ Equivalent From To → Equivalent From′ To′
+map t f eq = record { to = t to; from = f from }
+ where open Equivalent eq
+
+zip : ∀ {f₁₁ f₂₁ t₁₁ t₂₁}
+ {From₁ : Setoid f₁₁ f₂₁} {To₁ : Setoid t₁₁ t₂₁}
+ {f₁₂ f₂₂ t₁₂ t₂₂}
+ {From₂ : Setoid f₁₂ f₂₂} {To₂ : Setoid t₁₂ t₂₂}
+ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
+ ((From₁ ⟶ To₁) → (From₂ ⟶ To₂) → (From ⟶ To)) →
+ ((To₁ ⟶ From₁) → (To₂ ⟶ From₂) → (To ⟶ From)) →
+ Equivalent From₁ To₁ → Equivalent From₂ To₂ → Equivalent From To
+zip t f eq₁ eq₂ =
+ record { to = t (to eq₁) (to eq₂); from = f (from eq₁) (from eq₂) }
+ where open Equivalent
+
+
+
+
+
+
+id : ∀ {s₁ s₂} → Reflexive (Equivalent {s₁} {s₂})
+id {x = S} = record
+ { to = F.id
+ ; from = F.id
+ }
+
+infixr 9 _∘_
+
+_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂} →
+ TransFlip (Equivalent {f₁} {f₂} {m₁} {m₂})
+ (Equivalent {m₁} {m₂} {t₁} {t₂})
+ (Equivalent {f₁} {f₂} {t₁} {t₂})
+f ∘ g = record
+ { to = to f ⟪∘⟫ to g
+ ; from = from g ⟪∘⟫ from f
+ } where open Equivalent
+
+
+
+sym : ∀ {f₁ f₂ t₁ t₂} →
+ Sym (Equivalent {f₁} {f₂} {t₁} {t₂}) (Equivalent {t₁} {t₂} {f₁} {f₂})
+sym eq = record
+ { from = to
+ ; to = from
+ } where open Equivalent eq
+
+
+
+setoid : (s₁ s₂ : Level) → Setoid (suc (s₁ ⊔ s₂)) (s₁ ⊔ s₂)
+setoid s₁ s₂ = record
+ { Carrier = Setoid s₁ s₂
+ ; _≈_ = Equivalent
+ ; isEquivalence = record {refl = id; sym = sym; trans = flip _∘_}
+ }
+
+⇔-setoid : (ℓ : Level) → Setoid (suc ℓ) ℓ
+⇔-setoid ℓ = record
+ { Carrier = Set ℓ
+ ; _≈_ = _⇔_
+ ; isEquivalence = record {refl = id; sym = sym; trans = flip _∘_}
+ }
+
addfile ./html/Function.Injection.html
hunk ./html/Function.Injection.html 1
+
+Function.Injection
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Function.Injection where
+
+open import Function as Fun using () renaming (_∘_ to _⟨∘⟩_)
+open import Level
+open import Relation.Binary
+open import Function.Equality as F
+ using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
+
+
+
+Injective : ∀ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} →
+ A ⟶ B → Set _
+Injective {A = A} {B} f = ∀ {x y} → f ⟨$⟩ x ≈₂ f ⟨$⟩ y → x ≈₁ y
+ where
+ open Setoid A renaming (_≈_ to _≈₁_)
+ open Setoid B renaming (_≈_ to _≈₂_)
+
+
+
+record Injection {f₁ f₂ t₁ t₂}
+ (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
+ Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
+ field
+ to : From ⟶ To
+ injective : Injective to
+
+
+
+infixr 9 _∘_
+
+id : ∀ {s₁ s₂} {S : Setoid s₁ s₂} → Injection S S
+id = record { to = F.id; injective = Fun.id }
+
+_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂}
+ {F : Setoid f₁ f₂} {M : Setoid m₁ m₂} {T : Setoid t₁ t₂} →
+ Injection M T → Injection F M → Injection F T
+f ∘ g = record
+ { to = to f ⟪∘⟫ to g
+ ; injective = (λ {_} → injective g) ⟨∘⟩ injective f
+ } where open Injection
+
addfile ./html/Function.html
hunk ./html/Function.html 1
+
+Function
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Function where
+
+open import Level
+
+infixr 9 _∘_ _∘′_
+infixl 1 _on_
+infixl 1 _⟨_⟩_
+infixr 0 _-[_]-_ _$_
+infix 0 _∶_
+
+
+
+
+
+
+Fun₁ : ∀ {i} → Set i → Set i
+Fun₁ A = A → A
+
+
+
+Fun₂ : ∀ {i} → Set i → Set i
+Fun₂ A = A → A → A
+
+
+
+
+_∘_ : ∀ {a b c}
+ {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
+ (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
+ ((x : A) → C (g x))
+f ∘ g = λ x → f (g x)
+
+_∘′_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
+ (B → C) → (A → B) → (A → C)
+f ∘′ g = _∘_ f g
+
+id : ∀ {a} {A : Set a} → A → A
+id x = x
+
+const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
+const x = λ _ → x
+
+flip : ∀ {a b c} {A : Set a} {B : Set b} {C : A → B → Set c} →
+ ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
+flip f = λ x y → f y x
+
+
+
+
+
+
+_$_ : ∀ {a b} {A : Set a} {B : A → Set b} →
+ ((x : A) → B x) → ((x : A) → B x)
+f $ x = f x
+
+_⟨_⟩_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
+ A → (A → B → C) → B → C
+x ⟨ f ⟩ y = f x y
+
+_on_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
+ (B → B → C) → (A → B) → (A → A → C)
+_*_ on f = λ x y → f x * f y
+
+_-[_]-_ : ∀ {a b c d e} {A : Set a} {B : Set b} {C : Set c}
+ {D : Set d} {E : Set e} →
+ (A → B → C) → (C → D → E) → (A → B → D) → (A → B → E)
+f -[ _*_ ]- g = λ x y → f x y * g x y
+
+
+
+
+
+
+
+_∶_ : ∀ {a} (A : Set a) → A → A
+_ ∶ x = x
+
addfile ./html/IO.Primitive.html
hunk ./html/IO.Primitive.html 1
+
+IO.Primitive
+
+
+
+module IO.Primitive where
+
+open import Data.String hiding (Costring)
+open import Data.Char
+open import Foreign.Haskell
+
+
+
+
+postulate
+ IO : Set → Set
+
+{-# COMPILED_TYPE IO IO #-}
+
+infixl 1 _>>=_
+
+postulate
+ return : ∀ {A} → A → IO A
+ _>>=_ : ∀ {A B} → IO A → (A → IO B) → IO B
+
+{-# COMPILED return (\_ -> return :: a -> IO a) #-}
+{-# COMPILED _>>=_ (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}
+
+
+
+
+
+
+
+
+
+
+private
+ Costring = Colist Char
+
+postulate
+ getContents : IO Costring
+ readFile : String → IO Costring
+ writeFile : String → Costring → IO Unit
+ appendFile : String → Costring → IO Unit
+ putStr : Costring → IO Unit
+ putStrLn : Costring → IO Unit
+
+{-# COMPILED getContents getContents #-}
+{-# COMPILED readFile readFile #-}
+{-# COMPILED writeFile writeFile #-}
+{-# COMPILED appendFile appendFile #-}
+{-# COMPILED putStr putStr #-}
+{-# COMPILED putStrLn putStrLn #-}
+
addfile ./html/Level.html
hunk ./html/Level.html 1
+
+Level
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Level where
+
+
+
+data Level : Set where
+ zero : Level
+ suc : (i : Level) → Level
+
+{-# BUILTIN LEVEL Level #-}
+{-# BUILTIN LEVELZERO zero #-}
+{-# BUILTIN LEVELSUC suc #-}
+
+
+
+infixl 6 _⊔_
+
+_⊔_ : Level → Level → Level
+zero ⊔ j = j
+suc i ⊔ zero = suc i
+suc i ⊔ suc j = suc (i ⊔ j)
+
+{-# BUILTIN LEVELMAX _⊔_ #-}
+
+
+
+record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where
+ constructor lift
+ field lower : A
+
+open Lift public
+
addfile ./html/List.html
hunk ./html/List.html 1
+
+List
+module List where
+
+open import Function
+open import Data.Bool
+open import Data.Nat
+open import Data.Char
+import Data.String as String
+open String using (String)
+import Data.List as L
+
+data List A : Set where
+ [] : List A
+ _∷_ : A → List A → List A
+
+infixr 40 _∷_ _++_
+
+{-# COMPILED_DATA List [] [] (:) #-}
+
+foldr : ∀ {A B} → (A → B → B) → B → List A → B
+foldr f z [] = z
+foldr f z (x ∷ xs) = f x (foldr f z xs)
+
+foldl : ∀ {A B} → (B → A → B) → B → List A → B
+foldl f z [] = z
+foldl f z (x ∷ xs) = foldl f (f z x) xs
+
+map : ∀ {A B} → (A → B) → List A → List B
+map f [] = []
+map f (x ∷ xs) = f x ∷ map f xs
+
+and : List Bool → Bool
+and = foldr _∧_ true
+
+or : List Bool → Bool
+or = foldr _∨_ false
+
+any : ∀ {A} → (A → Bool) → List A → Bool
+any p = or ∘ map p
+
+all : ∀ {A} → (A → Bool) → List A → Bool
+all p = and ∘ map p
+
+filter : ∀ {A} → (A → Bool) → List A → List A
+filter p [] = []
+filter p (x ∷ xs) = if p x then x ∷ filter p xs
+ else filter p xs
+
+_++_ : ∀ {A} → List A → List A → List A
+[] ++ ys = ys
+(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
+
+length : ∀ {A} → List A → ℕ
+length = foldr (λ _ → suc) 0
+
+reverse : ∀ {A} → List A → List A
+reverse = foldl (λ xs x → x ∷ xs) []
+
+dropWhile : ∀ {A} → (A → Bool) → List A → List A
+dropWhile p [] = []
+dropWhile p (x ∷ xs) =
+ if p x then dropWhile p xs
+ else x ∷ xs
+
+fromList : ∀ {A} → L.List A → List A
+fromList L.[] = []
+fromList (L._∷_ x xs) = x ∷ fromList xs
+
+toList : ∀ {A} → List A → L.List A
+toList = foldr L._∷_ L.[]
+
+stringFromList : List Char → String
+stringFromList = String.fromList ∘ toList
+
+stringToList : String → List Char
+stringToList = fromList ∘ String.toList
addfile ./html/Main.html
hunk ./html/Main.html 1
+
+Main
+module Main where
+
+open import Function
+import IO.Primitive as IO
+open IO using (IO)
+open import Maybe
+open import List
+open import Data.Bool
+open import Data.Product
+open import Relation.Binary.PropositionalEquality
+open import Category.Monad.Indexed
+
+open import Schema
+open import Database
+open import Query
+open import Util
+open import BString
+
+open import ExampleDatabase
+
+open RawIMonad MonadDb hiding (_⊗_)
+
+{-# IMPORT Database.Firebird #-}
+
+queryType : ∀ {s t} → Query s t → TableType
+queryType {t = t} _ = t
+
+departmentPrograms : Query universitySchema _
+departmentPrograms =
+ proj ("PNAME" ∷ "ABBR" ∷ "DNAME" ∷ [])
+ ( select (! "DPDEPARTMENT" === ! "DNAME")
+ ( select (! "DPPROGRAM" === ! "PNAME")
+ (read "Departments" ⊗ read "Programs" ⊗ read "DepartmentsPrograms")
+ ))
+
+studentsInDepartment : BString _ → Query universitySchema _
+studentsInDepartment p =
+ proj ("SNAME" ∷ "PNAME" ∷ [])
+ ( select (! "SBRANCH" === ! "BID")
+ ( select (! "DNAME" === K p)
+ ( select (! "BPROGRAM" === ! "PNAME")
+ (read "Students" ⊗ read "Branches" ⊗ departmentPrograms)
+ )))
+
+q : Query universitySchema _
+q = studentsInDepartment (bString "Applied Mechanics")
+
+
+q′ : Query universitySchema _
+q′ = proj ("DNAME" ∷ []) (read "Departments")
+
+badQ : Query universitySchema _
+badQ = proj ("SNAME" ∷ [])
+ (select (! "SID" === K 0)
+ (read "Students")
+ )
+
+main =
+ withDatabase "university.fdb" "sysdba" "masterkey" universitySchema $
+ query q >>= λ rows →
+ liftIO (putStrLn "Query result:") >>
+ liftIO (mapM₋ (putStrLn ∘ showRow) rows)
+
+
addfile ./html/Maybe.html
hunk ./html/Maybe.html 1
+
+Maybe
+module Maybe where
+
+data Maybe A : Set where
+ nothing : Maybe A
+ just : A → Maybe A
+
+{-# COMPILED_DATA Maybe Maybe Nothing Just #-}
+
addfile ./html/Query.html
hunk ./html/Query.html 1
+
+Query
+module Query where
+
+open import Function
+open import Data.Bool renaming (T to isTrue)
+open import Data.Unit
+open import List hiding (and)
+open import Data.Product hiding (map)
+import IO.Primitive as IO
+open IO using (IO)
+open import Maybe
+import Data.String as String
+open String using (String)
+open import Relation.Binary.PropositionalEquality
+open import Category.Monad.Indexed
+open import Category.Monad
+
+open import Eq
+open import Schema
+open import Util
+open import BString
+open import Database
+
+open RawIMonad MonadDb hiding (_⊗_)
+open RawMonad MonadIO using () renaming (_>>_ to _>>′_)
+
+{-# IMPORT Database.Firebird #-}
+
+infix 0 found_expectedOneOf_ theFields_appearInBoth_and_
+
+data ErrorMsg : Set where
+ found_expectedOneOf_ : String → List String → ErrorMsg
+ theFields_appearInBoth_and_ : List String → List String → List String → ErrorMsg
+ noError : ErrorMsg
+
+Constraint = Bool × ErrorMsg
+
+trivial : Constraint
+trivial = true , noError
+
+_&&_ : Constraint → Constraint → Constraint
+(true , _) && c = c
+(false , e) && _ = false , e
+
+_hasField_ : TableType → FieldName → Constraint
+t hasField x = haskey x t , (found x expectedOneOf map proj₁ t)
+
+_hasTable_ : Schema → TableName → Constraint
+s hasTable t = haskey t s , (found t expectedOneOf map proj₁ s)
+
+_hasFields_ : TableType → List FieldName → Constraint
+t hasFields xs = foldr _&&_ trivial (map (_hasField_ t) xs)
+
+disjoint : TableType → TableType → Constraint
+disjoint s s' = all (λ x → not (elem x names')) names
+ , (theFields filter (λ x → elem x names') names appearInBoth names and names')
+ where
+ names = map proj₁ s
+ names' = map proj₁ s'
+
+data Error (e : ErrorMsg) : Set where
+
+sat : Constraint → Set
+sat (true , _) = ⊤
+sat (false , e) = Error e
+
+trueConstr : ∀ {c} → sat c → isTrue (proj₁ c)
+trueConstr {true , _} p = p
+trueConstr {false , _} ()
+
+lookupField : (x : FieldName)(t : TableType) → sat (t hasField x) → FieldType
+lookupField x t p = lookup' x t (trueConstr p)
+
+lookupTable : (t : TableName)(s : Schema) → sat (s hasTable t) → TableType
+lookupTable t s p = lookup' t s (trueConstr p)
+
+
+
+sat-and₁ : ∀ {a b} → sat (a && b) → sat a
+sat-and₁ {true , _} p = _
+sat-and₁ {false , _} ()
+
+sat-and₂ : ∀ {a b} → sat (a && b) → sat b
+sat-and₂ {true , _} p = p
+sat-and₂ {false , _} ()
+
+subTable : (xs : List FieldName)(t : TableType) → sat (t hasFields xs) → TableType
+subTable [] t _ = []
+subTable (x ∷ xs) t p = (x , lookupField x t (sat-and₁ p)) ∷
+ subTable xs t (sat-and₂ {t hasField x} p)
+
+data EType : Set where
+ bool : EType
+ ftype : FieldType → EType
+
+data Expr (t : TableType) : EType → Set where
+ _===_ : ∀ {a} → Expr t a → Expr t a → Expr t bool
+ !_ : ∀ x {p : sat (t hasField x)} → Expr t (ftype (lookupField x t p))
+ K : ∀ {a} → Field a → Expr t (ftype a)
+
+infixr 25 _⊗_
+
+data Query (s : Schema) : TableType → Set where
+ read : ∀ (x : TableName){p : sat (s hasTable x)} →
+ Query s (lookupTable x s p)
+ _⊗_ : ∀ {t t'}{p : sat (disjoint t t')} →
+ Query s t → Query s t' → Query s (t ++ t')
+ proj : ∀ {t} xs {p : sat (t hasFields xs)} →
+ Query s t → Query s (subTable xs t p)
+ select : ∀ {t} → Expr t bool → Query s t → Query s t
+
+infix 0 SELECT_FROM_WHERE_
+
+data SQL : Set where
+ SELECT_FROM_WHERE_ : List FieldName → List TableName → List String → SQL
+
+infixr 40 _&_
+_&_ = primStringAppend
+
+sepBy : String → List String → String
+sepBy _ [] = ""
+sepBy _ (x ∷ []) = x
+sepBy i (x ∷ xs) = x & i & sepBy i xs
+
+showField : ∀ {a} → Field a → String
+showField {string _} s = "'" & trim ' ' (unBString s) & "'"
+showField {number} n = showNat n
+showField {date} d = sepBy "-" (map showNat (Date.year d ∷ Date.month d ∷ Date.day d ∷ []))
+showField {time} t = sepBy ":" (map showNat (Time.hour t ∷ Time.minute t ∷ Time.second t ∷ []))
+ & "." & showNat (Time.millisecond t)
+
+showRow : ∀ {t} → Row t → String
+showRow [] = ""
+showRow (_∷_ {name = name} x []) = name & " = " & showField x
+showRow (_∷_ {name = name} x xs) = name & " = " & showField x & ", " & showRow xs
+
+showExpr : ∀ {t a} → Expr t a → String
+showExpr (e₁ === e₂) = showExpr e₁ & " = " & showExpr e₂
+showExpr (! x) = x
+showExpr (K c) = showField c
+
+showSQL : SQL → String
+showSQL (SELECT as FROM ts WHERE cs) =
+ "SELECT " & sepBy ", " as & " FROM " & sepBy ", " ts & whereClause cs
+ where
+ whereClause : List String → String
+ whereClause [] = ""
+ whereClause cs = " WHERE " & sepBy " AND " cs
+
+toSQL : ∀ {s t} → Query s t → SQL
+toSQL {s} (read x {p}) = SELECT (map proj₁ (lookup' x s (trueConstr p))) FROM x ∷ [] WHERE []
+toSQL (q₁ ⊗ q₂) with toSQL q₁ | toSQL q₂
+... | SELECT as₁ FROM ts₁ WHERE cs₁
+ | SELECT as₂ FROM ts₂ WHERE cs₂ = SELECT as₁ ++ as₂ FROM nub (ts₁ ++ ts₂) WHERE cs₁ ++ cs₂
+toSQL (proj as q) with toSQL q
+... | SELECT _ FROM ts WHERE cs = SELECT as FROM ts WHERE cs
+toSQL (select c q) with toSQL q
+... | SELECT as FROM ts WHERE cs = SELECT as FROM ts WHERE showExpr c ∷ cs
+
+data HsField : Set where
+ string : String → HsField
+ number : Integer → HsField
+ date : (year month day : Integer) → HsField
+ time : (hour minute second millisecond : Integer) → HsField
+
+{-# COMPILED_DATA HsField Field FString FNumber FDate FTime #-}
+
+HsRow = List HsField
+
+postulate
+ hs_query : RawHandle → String → IO (List HsRow)
+
+{-# COMPILED hs_query sqlQuery #-}
+
+parseHsField : ∀ {t} → HsField → Maybe (Field t)
+parseHsField {string n} (string s) with inspect (strLen s =< n)
+... | true with-≡ p = just (bString s {istrue (sym p)})
+... | false with-≡ _ = nothing
+parseHsField {number} (number n) = just (primIntegerAbs n)
+parseHsField {date} (date y m d) = just (mkDate (primIntegerAbs y)
+ (primIntegerAbs m)
+ (primIntegerAbs d)
+ )
+parseHsField {time} (time h m s ms) = just (mkTime (primIntegerAbs h)
+ (primIntegerAbs m)
+ (primIntegerAbs s)
+ (primIntegerAbs ms)
+ )
+parseHsField _ = nothing
+
+parseHsRow : ∀ {t} → HsRow → Maybe (Row t)
+parseHsRow {[]} [] = just []
+parseHsRow {(_ , t) ∷ ts} (x ∷ xs) =
+ bindMaybe (parseHsField x) λ y →
+ bindMaybe (parseHsRow xs) λ ys →
+ just (y ∷ ys)
+parseHsRow _ = nothing
+
+parseHsRows : ∀ {t} → List HsRow → Maybe (List (Row t))
+parseHsRows = mapMaybe parseHsRow
+
+showHsField : HsField → String
+showHsField (string s) = "'" & s & "'"
+showHsField (number n) = showInteger n
+showHsField (date y m d) = sepBy "-" (map showInteger (y ∷ m ∷ d ∷ []))
+showHsField (time h m s ms) =
+ sepBy ":" (map showInteger (h ∷ m ∷ s ∷ [])) & "." & showInteger ms
+
+printHsRow = putStrLn ∘ sepBy ", " ∘ map showHsField
+printHsRows = mapM₋ printHsRow
+
+query : ∀ {s t} → Query s t → Db s s (List (Row t))
+query q = withRawHandle λ h →
+ let sql = showSQL (toSQL q) in
+ liftIO (putStrLn ("query: " & sql)) >>
+ liftIO (hs_query h sql) >>= λ hrows →
+ withMaybe (parseHsRows hrows)
+ (liftIO (putStrLn "Bad rows:" >>′ printHsRows hrows >>′ ioError "Bad rows"))
+ λ rows → return rows
+
addfile ./html/Relation.Binary.Consequences.Core.html
hunk ./html/Relation.Binary.Consequences.Core.html 1
+
+Relation.Binary.Consequences.Core
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+
+
+
+module Relation.Binary.Consequences.Core where
+
+open import Relation.Binary.Core
+open import Data.Product
+
+subst⟶resp₂ : ∀ {a ℓ p} {A : Set a} {∼ : Rel A ℓ}
+ (P : Rel A p) → Substitutive ∼ p → P Respects₂ ∼
+subst⟶resp₂ {∼ = ∼} P subst =
+ (λ {x _ _} y'∼y Pxy' → subst (P x) y'∼y Pxy') ,
+ (λ {y _ _} x'∼x Px'y → subst (λ x → P x y) x'∼x Px'y)
+
addfile ./html/Relation.Binary.Consequences.html
hunk ./html/Relation.Binary.Consequences.html 1
+
+Relation.Binary.Consequences
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Relation.Binary.Consequences where
+
+open import Relation.Binary.Core hiding (refl)
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality.Core
+open import Function
+open import Data.Sum
+open import Data.Product
+open import Data.Empty
+
+
+
+open import Relation.Binary.Consequences.Core public
+
+trans∧irr⟶asym :
+ ∀ {a ℓ₁ ℓ₂} {A : Set a} → {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
+ Reflexive ≈ →
+ Transitive < → Irreflexive ≈ < → Asymmetric <
+trans∧irr⟶asym refl trans irrefl = λ x<y y<x →
+ irrefl refl (trans x<y y<x)
+
+irr∧antisym⟶asym :
+ ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
+ Irreflexive ≈ < → Antisymmetric ≈ < → Asymmetric <
+irr∧antisym⟶asym irrefl antisym = λ x<y y<x →
+ irrefl (antisym x<y y<x) x<y
+
+asym⟶antisym :
+ ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
+ Asymmetric < → Antisymmetric ≈ <
+asym⟶antisym asym x<y y<x = ⊥-elim (asym x<y y<x)
+
+asym⟶irr :
+ ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
+ < Respects₂ ≈ → Symmetric ≈ →
+ Asymmetric < → Irreflexive ≈ <
+asym⟶irr {< = _<_} resp sym asym {x} {y} x≈y x<y = asym x<y y<x
+ where
+ y<y : y < y
+ y<y = proj₂ resp x≈y x<y
+ y<x : y < x
+ y<x = proj₁ resp (sym x≈y) y<y
+
+total⟶refl :
+ ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} →
+ ∼ Respects₂ ≈ → Symmetric ≈ →
+ Total ∼ → ≈ ⇒ ∼
+total⟶refl {≈ = ≈} {∼ = ∼} resp sym total = refl
+ where
+ refl : ≈ ⇒ ∼
+ refl {x} {y} x≈y with total x y
+ ... | inj₁ x∼y = x∼y
+ ... | inj₂ y∼x =
+ proj₁ resp x≈y (proj₂ resp (sym x≈y) y∼x)
+
+total+dec⟶dec :
+ ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
+ ≈ ⇒ ≤ → Antisymmetric ≈ ≤ →
+ Total ≤ → Decidable ≈ → Decidable ≤
+total+dec⟶dec {≈ = ≈} {≤ = ≤} refl antisym total _≟_ = dec
+ where
+ dec : Decidable ≤
+ dec x y with total x y
+ ... | inj₁ x≤y = yes x≤y
+ ... | inj₂ y≤x with x ≟ y
+ ... | yes x≈y = yes (refl x≈y)
+ ... | no ¬x≈y = no (λ x≤y → ¬x≈y (antisym x≤y y≤x))
+
+tri⟶asym :
+ ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
+ Trichotomous ≈ < → Asymmetric <
+tri⟶asym tri {x} {y} x<y x>y with tri x y
+... | tri< _ _ x≯y = x≯y x>y
+... | tri≈ _ _ x≯y = x≯y x>y
+... | tri> x≮y _ _ = x≮y x<y
+
+tri⟶irr :
+ ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
+ < Respects₂ ≈ → Symmetric ≈ →
+ Trichotomous ≈ < → Irreflexive ≈ <
+tri⟶irr resp sym tri = asym⟶irr resp sym (tri⟶asym tri)
+
+tri⟶dec≈ :
+ ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
+ Trichotomous ≈ < → Decidable ≈
+tri⟶dec≈ compare x y with compare x y
+... | tri< _ x≉y _ = no x≉y
+... | tri≈ _ x≈y _ = yes x≈y
+... | tri> _ x≉y _ = no x≉y
+
+tri⟶dec< :
+ ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
+ Trichotomous ≈ < → Decidable <
+tri⟶dec< compare x y with compare x y
+... | tri< x<y _ _ = yes x<y
+... | tri≈ x≮y _ _ = no x≮y
+... | tri> x≮y _ _ = no x≮y
+
+map-NonEmpty : ∀ {a b p q} {A : Set a} {B : Set b}
+ {P : REL A B p} {Q : REL A B q} →
+ P ⇒ Q → NonEmpty P → NonEmpty Q
+map-NonEmpty f x = nonEmpty (f (NonEmpty.proof x))
+
addfile ./html/Relation.Binary.Core.html
hunk ./html/Relation.Binary.Core.html 1
+
+Relation.Binary.Core
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+
+
+
+module Relation.Binary.Core where
+
+open import Data.Product
+open import Data.Sum
+open import Function
+open import Level
+open import Relation.Nullary
+
+
+
+
+
+
+REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ)
+REL A B ℓ = A → B → Set ℓ
+
+
+
+Rel : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
+Rel A ℓ = REL A A ℓ
+
+
+
+
+infixr 4 _⇒_ _=[_]⇒_
+
+
+
+_⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
+ REL A B ℓ₁ → REL A B ℓ₂ → Set _
+P ⇒ Q = ∀ {i j} → P i j → Q i j
+
+
+
+
+_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
+ Rel A ℓ₁ → (A → B) → Rel B ℓ₂ → Set _
+P =[ f ]⇒ Q = P ⇒ (Q on f)
+
+
+
+_Preserves_⟶_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
+ (A → B) → Rel A ℓ₁ → Rel B ℓ₂ → Set _
+f Preserves P ⟶ Q = P =[ f ]⇒ Q
+
+_Preserves₂_⟶_⟶_ :
+ ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
+ (A → B → C) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Set _
+_+_ Preserves₂ P ⟶ Q ⟶ R =
+ ∀ {x y u v} → P x y → Q u v → R (x + u) (y + v)
+
+
+
+
+
+Reflexive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
+Reflexive _∼_ = ∀ {x} → x ∼ x
+
+
+
+Irreflexive : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
+ REL A B ℓ₁ → REL A B ℓ₂ → Set _
+Irreflexive _≈_ _<_ = ∀ {x y} → x ≈ y → ¬ (x < y)
+
+
+
+Sym : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
+ REL A B ℓ₁ → REL B A ℓ₂ → Set _
+Sym P Q = P ⇒ flip Q
+
+Symmetric : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
+Symmetric _∼_ = Sym _∼_ _∼_
+
+
+
+Trans : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
+ REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
+Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k
+
+
+
+TransFlip : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
+ REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
+TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k
+
+Transitive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
+Transitive _∼_ = Trans _∼_ _∼_ _∼_
+
+Antisymmetric : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
+Antisymmetric _≈_ _≤_ = ∀ {x y} → x ≤ y → y ≤ x → x ≈ y
+
+Asymmetric : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
+Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)
+
+_Respects_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → (A → Set ℓ₁) → Rel A ℓ₂ → Set _
+P Respects _∼_ = ∀ {x y} → x ∼ y → P x → P y
+
+_Respects₂_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
+P Respects₂ _∼_ =
+ (∀ {x} → P x Respects _∼_) ×
+ (∀ {y} → flip P y Respects _∼_)
+
+Substitutive : ∀ {a ℓ₁} {A : Set a} → Rel A ℓ₁ → (ℓ₂ : Level) → Set _
+Substitutive {A = A} _∼_ p = (P : A → Set p) → P Respects _∼_
+
+Decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} → REL A B ℓ → Set _
+Decidable _∼_ = ∀ x y → Dec (x ∼ y)
+
+Total : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
+Total _∼_ = ∀ x y → (x ∼ y) ⊎ (y ∼ x)
+
+data Tri {a b c} (A : Set a) (B : Set b) (C : Set c) :
+ Set (a ⊔ b ⊔ c) where
+ tri< : ( a : A) (¬b : ¬ B) (¬c : ¬ C) → Tri A B C
+ tri≈ : (¬a : ¬ A) ( b : B) (¬c : ¬ C) → Tri A B C
+ tri> : (¬a : ¬ A) (¬b : ¬ B) ( c : C) → Tri A B C
+
+Trichotomous : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
+Trichotomous _≈_ _<_ = ∀ x y → Tri (x < y) (x ≈ y) (x > y)
+ where _>_ = flip _<_
+
+record NonEmpty {a b ℓ} {A : Set a} {B : Set b}
+ (T : REL A B ℓ) : Set (a ⊔ b ⊔ ℓ) where
+ constructor nonEmpty
+ field
+ {x} : A
+ {y} : B
+ proof : T x y
+
+
+
+
+
+
+
+
+private
+ module Dummy where
+
+ infix 4 _≡_ _≢_
+
+ data _≡_ {a} {A : Set a} (x : A) : A → Set where
+ refl : x ≡ x
+
+ {-# BUILTIN EQUALITY _≡_ #-}
+ {-# BUILTIN REFL refl #-}
+
+
+
+ _≢_ : ∀ {a} {A : Set a} → A → A → Set
+ x ≢ y = ¬ x ≡ y
+
+
+
+
+
+
+
+
+record IsEquivalence {a ℓ} {A : Set a}
+ (_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where
+ field
+ refl : Reflexive _≈_
+ sym : Symmetric _≈_
+ trans : Transitive _≈_
+
+ reflexive : Dummy._≡_ ⇒ _≈_
+ reflexive Dummy.refl = refl
+
+open Dummy public
+
addfile ./html/Relation.Binary.EqReasoning.html
hunk ./html/Relation.Binary.EqReasoning.html 1
+
+Relation.Binary.EqReasoning
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+open import Relation.Binary
+
+module Relation.Binary.EqReasoning {s₁ s₂} (S : Setoid s₁ s₂) where
+
+open Setoid S
+import Relation.Binary.PreorderReasoning as PreR
+open PreR preorder public
+ renaming ( _∼⟨_⟩_ to _≈⟨_⟩_
+ ; _≈⟨_⟩_ to _≡⟨_⟩_
+ )
+
addfile ./html/Relation.Binary.FunctionSetoid.html
hunk ./html/Relation.Binary.FunctionSetoid.html 1
+
+Relation.Binary.FunctionSetoid
+
+
+
+module Relation.Binary.FunctionSetoid where
+
+open import Data.Function
+open import Relation.Binary
+
+infixr 0 _↝_ _⟶_ _⇨_ _≡⇨_
+
+
+
+
+_↝_ : ∀ {A B} → (∼₁ : Rel A) (∼₂ : Rel B) → Rel (A → B)
+_∼₁_ ↝ _∼₂_ = λ f g → ∀ {x y} → x ∼₁ y → f x ∼₂ g y
+
+
+
+record _⟶_ (From To : Setoid) : Set where
+ open Setoid
+ infixl 5 _⟨$⟩_
+ field
+ _⟨$⟩_ : carrier From → carrier To
+ pres : _⟨$⟩_ Preserves _≈_ From ⟶ _≈_ To
+
+open _⟶_ public
+
+↝-isEquivalence : ∀ {A B C} {∼₁ : Rel A} {∼₂ : Rel B}
+ (fun : C → (A → B)) →
+ (∀ f → fun f Preserves ∼₁ ⟶ ∼₂) →
+ IsEquivalence ∼₁ → IsEquivalence ∼₂ →
+ IsEquivalence ((∼₁ ↝ ∼₂) on₁ fun)
+↝-isEquivalence _ pres eq₁ eq₂ = record
+ { refl = λ {f} x∼₁y → pres f x∼₁y
+ ; sym = λ f∼g x∼y → sym eq₂ (f∼g (sym eq₁ x∼y))
+ ; trans = λ f∼g g∼h x∼y → trans eq₂ (f∼g (refl eq₁)) (g∼h x∼y)
+ } where open IsEquivalence
+
+
+
+_⇨_ : Setoid → Setoid → Setoid
+S₁ ⇨ S₂ = record
+ { carrier = S₁ ⟶ S₂
+ ; _≈_ = (_≈_ S₁ ↝ _≈_ S₂) on₁ _⟨$⟩_
+ ; isEquivalence =
+ ↝-isEquivalence _⟨$⟩_ pres (isEquivalence S₁) (isEquivalence S₂)
+ } where open Setoid; open _⟶_
+
+
+
+≡↝ : ∀ {A} {B : A → Set} → (∀ x → Rel (B x)) → Rel ((x : A) → B x)
+≡↝ R = λ f g → ∀ x → R x (f x) (g x)
+
+≡↝-isEquivalence : {A : Set} {B : A → Set} {R : ∀ x → Rel (B x)} →
+ (∀ x → IsEquivalence (R x)) → IsEquivalence (≡↝ R)
+≡↝-isEquivalence eq = record
+ { refl = λ _ → refl
+ ; sym = λ f∼g x → sym (f∼g x)
+ ; trans = λ f∼g g∼h x → trans (f∼g x) (g∼h x)
+ } where open module Eq {x} = IsEquivalence (eq x)
+
+_≡⇨_ : (A : Set) → (A → Setoid) → Setoid
+A ≡⇨ S = record
+ { carrier = (x : A) → carrier (S x)
+ ; _≈_ = ≡↝ (λ x → _≈_ (S x))
+ ; isEquivalence = ≡↝-isEquivalence (λ x → isEquivalence (S x))
+ } where open Setoid
+
addfile ./html/Relation.Binary.Indexed.Core.html
hunk ./html/Relation.Binary.Indexed.Core.html 1
+
+Relation.Binary.Indexed.Core
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+
+
+
+module Relation.Binary.Indexed.Core where
+
+open import Function
+open import Level
+import Relation.Binary.Core as B
+import Relation.Binary.Core as P
+
+
+
+
+
+
+REL : ∀ {i₁ i₂ a₁ a₂} {I₁ : Set i₁} {I₂ : Set i₂} →
+ (I₁ → Set a₁) → (I₂ → Set a₂) → (ℓ : Level) → Set _
+REL A₁ A₂ ℓ = ∀ {i₁ i₂} → A₁ i₁ → A₂ i₂ → Set ℓ
+
+
+
+Rel : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
+Rel A ℓ = REL A A ℓ
+
+
+
+
+
+
+Reflexive : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → Rel A ℓ → Set _
+Reflexive _ _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})
+
+
+
+Symmetric : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → Rel A ℓ → Set _
+Symmetric _ _∼_ = ∀ {i j} → B.Sym (_∼_ {i} {j}) _∼_
+
+
+
+Transitive : ∀ {i a ℓ} {I : Set i} (A : I → Set a) → Rel A ℓ → Set _
+Transitive _ _∼_ = ∀ {i j k} → B.Trans _∼_ (_∼_ {j}) (_∼_ {i} {k})
+
+
+
+
+record IsEquivalence {i a ℓ} {I : Set i} (A : I → Set a)
+ (_≈_ : Rel A ℓ) : Set (i ⊔ a ⊔ ℓ) where
+ field
+ refl : Reflexive A _≈_
+ sym : Symmetric A _≈_
+ trans : Transitive A _≈_
+
+ reflexive : ∀ {i} → P._≡_ ⟨ B._⇒_ ⟩ _≈_ {i}
+ reflexive P.refl = refl
+
+record Setoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
+ infix 4 _≈_
+ field
+ Carrier : I → Set c
+ _≈_ : Rel Carrier ℓ
+ isEquivalence : IsEquivalence Carrier _≈_
+
+ open IsEquivalence isEquivalence public
+
addfile ./html/Relation.Binary.Indexed.html
hunk ./html/Relation.Binary.Indexed.html 1
+
+Relation.Binary.Indexed
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Relation.Binary.Indexed where
+
+import Relation.Binary as B
+
+open import Relation.Binary.Indexed.Core public
+
+
+
+_at_ : ∀ {i s₁ s₂} {I : Set i} → Setoid I s₁ s₂ → I → B.Setoid _ _
+S at i = record
+ { Carrier = S.Carrier i
+ ; _≈_ = S._≈_
+ ; isEquivalence = record
+ { refl = S.refl
+ ; sym = S.sym
+ ; trans = S.trans
+ }
+ } where module S = Setoid S
+
+
+
+
+
+
+infixr 4 _=[_]⇒_
+
+_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b} →
+ B.Rel A ℓ₁ → ((x : A) → B x) → Rel B ℓ₂ → Set _
+P =[ f ]⇒ Q = ∀ {i j} → P i j → Q (f i) (f j)
+
addfile ./html/Relation.Binary.InducedPreorders.html
hunk ./html/Relation.Binary.InducedPreorders.html 1
+
+Relation.Binary.InducedPreorders
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+open import Relation.Binary
+
+module Relation.Binary.InducedPreorders
+ {s₁ s₂}
+ (S : Setoid s₁ s₂)
+ where
+
+open import Function
+open import Data.Product
+
+open Setoid S
+
+
+
+
+InducedPreorder₁ : ∀ {p} (P : Carrier → Set p) →
+ P Respects _≈_ → Preorder _ _ _
+InducedPreorder₁ P resp = record
+ { _≈_ = _≈_
+ ; _∼_ = λ c₁ c₂ → P c₁ → P c₂
+ ; isPreorder = record
+ { isEquivalence = isEquivalence
+ ; reflexive = resp
+ ; trans = flip _∘′_
+ }
+ }
+
+
+
+
+InducedPreorder₂ : ∀ {a r} {A : Set a} →
+ (_R_ : A → Carrier → Set r) →
+ (∀ {x} → _R_ x Respects _≈_) → Preorder _ _ _
+InducedPreorder₂ _R_ resp = record
+ { _≈_ = _≈_
+ ; _∼_ = λ c₁ c₂ → ∀ {a} → a R c₁ → a R c₂
+ ; isPreorder = record
+ { isEquivalence = isEquivalence
+ ; reflexive = λ c₁≈c₂ → resp c₁≈c₂
+ ; trans = λ c₁∼c₂ c₂∼c₃ → c₂∼c₃ ∘ c₁∼c₂
+ }
+ }
+
addfile ./html/Relation.Binary.PartialOrderReasoning.html
hunk ./html/Relation.Binary.PartialOrderReasoning.html 1
+
+Relation.Binary.PartialOrderReasoning
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+open import Relation.Binary
+
+module Relation.Binary.PartialOrderReasoning
+ {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where
+
+open Poset P
+import Relation.Binary.PreorderReasoning as PreR
+open PreR preorder public renaming (_∼⟨_⟩_ to _≤⟨_⟩_)
+
addfile ./html/Relation.Binary.PreorderReasoning.html
hunk ./html/Relation.Binary.PreorderReasoning.html 1
+
+Relation.Binary.PreorderReasoning
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+open import Relation.Binary
+
+module Relation.Binary.PreorderReasoning
+ {p₁ p₂ p₃} (P : Preorder p₁ p₂ p₃) where
+
+open Preorder P
+
+infix 4 _IsRelatedTo_
+infix 2 _∎
+infixr 2 _∼⟨_⟩_ _≈⟨_⟩_
+infix 1 begin_
+
+
+
+
+data _IsRelatedTo_ (x y : Carrier) : Set p₃ where
+ relTo : (x∼y : x ∼ y) → x IsRelatedTo y
+
+begin_ : ∀ {x y} → x IsRelatedTo y → x ∼ y
+begin relTo x∼y = x∼y
+
+_∼⟨_⟩_ : ∀ x {y z} → x ∼ y → y IsRelatedTo z → x IsRelatedTo z
+_ ∼⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)
+
+_≈⟨_⟩_ : ∀ x {y z} → x ≈ y → y IsRelatedTo z → x IsRelatedTo z
+_ ≈⟨ x≈y ⟩ relTo y∼z = relTo (trans (reflexive x≈y) y∼z)
+
+_∎ : ∀ x → x IsRelatedTo x
+_∎ _ = relTo refl
+
addfile ./html/Relation.Binary.PropositionalEquality.Core.html
hunk ./html/Relation.Binary.PropositionalEquality.Core.html 1
+
+Relation.Binary.PropositionalEquality.Core
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+
+
+
+module Relation.Binary.PropositionalEquality.Core where
+
+open import Level
+open import Relation.Binary.Core
+open import Relation.Binary.Consequences.Core
+
+
+
+
+sym : ∀ {a} {A : Set a} → Symmetric (_≡_ {A = A})
+sym refl = refl
+
+trans : ∀ {a} {A : Set a} → Transitive (_≡_ {A = A})
+trans refl refl = refl
+
+subst : ∀ {a p} {A : Set a} → Substitutive (_≡_ {A = A}) p
+subst P refl p = p
+
+resp₂ : ∀ {a ℓ} {A : Set a} (∼ : Rel A ℓ) → ∼ Respects₂ _≡_
+resp₂ _∼_ = subst⟶resp₂ _∼_ subst
+
+isEquivalence : ∀ {a} {A : Set a} → IsEquivalence (_≡_ {A = A})
+isEquivalence = record
+ { refl = refl
+ ; sym = sym
+ ; trans = trans
+ }
+
addfile ./html/Relation.Binary.PropositionalEquality.TrustMe.html
hunk ./html/Relation.Binary.PropositionalEquality.TrustMe.html 1
+
+Relation.Binary.PropositionalEquality.TrustMe
+
+
+
+module Relation.Binary.PropositionalEquality.TrustMe where
+
+open import Relation.Binary.PropositionalEquality
+
+private
+ primitive
+ primTrustMe : {A : Set}{a b : A} → a ≡ b
+
+
+
+
+
+
+trustMe : {A : Set}{a b : A} → a ≡ b
+trustMe = primTrustMe
+
addfile ./html/Relation.Binary.PropositionalEquality.html
hunk ./html/Relation.Binary.PropositionalEquality.html 1
+
+Relation.Binary.PropositionalEquality
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Relation.Binary.PropositionalEquality where
+
+open import Function
+open import Function.Equality using (Π; _⟶_; ≡-setoid)
+open import Data.Product
+open import Level
+open import Relation.Binary
+import Relation.Binary.Indexed as I
+open import Relation.Binary.Consequences
+
+
+
+open import Relation.Binary.Core public using (_≡_; refl; _≢_)
+open import Relation.Binary.PropositionalEquality.Core public
+
+
+
+
+subst₂ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p)
+ {x₁ x₂ y₁ y₂} → x₁ ≡ x₂ → y₁ ≡ y₂ → P x₁ y₁ → P x₂ y₂
+subst₂ P refl refl p = p
+
+cong : ∀ {a b} {A : Set a} {B : Set b}
+ (f : A → B) {x y} → x ≡ y → f x ≡ f y
+cong f refl = refl
+
+cong₂ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+ (f : A → B → C) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v
+cong₂ f refl refl = refl
+
+proof-irrelevance : ∀ {a} {A : Set a} {x y : A} (p q : x ≡ y) → p ≡ q
+proof-irrelevance refl refl = refl
+
+setoid : ∀ {a} → Set a → Setoid _ _
+setoid A = record
+ { Carrier = A
+ ; _≈_ = _≡_
+ ; isEquivalence = isEquivalence
+ }
+
+decSetoid : ∀ {a} {A : Set a} → Decidable (_≡_ {A = A}) → DecSetoid _ _
+decSetoid dec = record
+ { _≈_ = _≡_
+ ; isDecEquivalence = record
+ { isEquivalence = isEquivalence
+ ; _≟_ = dec
+ }
+ }
+
+isPreorder : ∀ {a} {A : Set a} → IsPreorder {A = A} _≡_ _≡_
+isPreorder = record
+ { isEquivalence = isEquivalence
+ ; reflexive = id
+ ; trans = trans
+ }
+
+preorder : ∀ {a} → Set a → Preorder _ _ _
+preorder A = record
+ { Carrier = A
+ ; _≈_ = _≡_
+ ; _∼_ = _≡_
+ ; isPreorder = isPreorder
+ }
+
+
+
+
+infix 4 _≗_
+
+_→-setoid_ : ∀ {a b} (A : Set a) (B : Set b) → Setoid _ _
+A →-setoid B = ≡-setoid A (Setoid.indexedSetoid (setoid B))
+
+_≗_ : ∀ {a b} {A : Set a} {B : Set b} (f g : A → B) → Set _
+_≗_ {A = A} {B} = Setoid._≈_ (A →-setoid B)
+
+:→-to-Π : ∀ {a b₁ b₂} {A : Set a} {B : I.Setoid _ b₁ b₂} →
+ ((x : A) → I.Setoid.Carrier B x) → Π (setoid A) B
+:→-to-Π {B = B} f = record { _⟨$⟩_ = f; cong = cong′ }
+ where
+ open I.Setoid B using (_≈_)
+
+ cong′ : ∀ {x y} → x ≡ y → f x ≈ f y
+ cong′ refl = I.Setoid.refl B
+
+→-to-⟶ : ∀ {a b₁ b₂} {A : Set a} {B : Setoid b₁ b₂} →
+ (A → Setoid.Carrier B) → setoid A ⟶ B
+→-to-⟶ = :→-to-Π
+
+
+
+
+
+
+
+
+data Inspect {a} {A : Set a} (x : A) : Set a where
+ _with-≡_ : (y : A) (eq : x ≡ y) → Inspect x
+
+inspect : ∀ {a} {A : Set a} (x : A) → Inspect x
+inspect x = x with-≡ refl
+
+
+
+
+
+
+
+
+
+import Relation.Binary.EqReasoning as EqR
+
+
+
+
+
+
+module ≡-Reasoning where
+ private
+ module Dummy {a} {A : Set a} where
+ open EqR (setoid A) public
+ hiding (_≡⟨_⟩_) renaming (_≈⟨_⟩_ to _≡⟨_⟩_)
+ open Dummy public
+
+
+
+
+
+
+
+Extensionality : ∀ ℓ → Set (suc ℓ)
+Extensionality ℓ =
+ {A B : Set ℓ} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
+
addfile ./html/Relation.Binary.html
hunk ./html/Relation.Binary.html 1
+
+Relation.Binary
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Relation.Binary where
+
+open import Data.Product
+open import Data.Sum
+open import Function
+open import Level
+import Relation.Binary.PropositionalEquality.Core as PropEq
+open import Relation.Binary.Consequences
+open import Relation.Binary.Core as Core using (_≡_)
+import Relation.Binary.Indexed.Core as I
+
+
+
+
+open Core public hiding (_≡_; refl; _≢_)
+
+
+
+
+record IsPreorder {a ℓ₁ ℓ₂} {A : Set a}
+ (_≈_ : Rel A ℓ₁)
+ (_∼_ : Rel A ℓ₂)
+ : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ isEquivalence : IsEquivalence _≈_
+
+ reflexive : _≈_ ⇒ _∼_
+ trans : Transitive _∼_
+
+ module Eq = IsEquivalence isEquivalence
+
+ refl : Reflexive _∼_
+ refl = reflexive Eq.refl
+
+ ∼-resp-≈ : _∼_ Respects₂ _≈_
+ ∼-resp-≈ = (λ x≈y z∼x → trans z∼x (reflexive x≈y))
+ , (λ x≈y x∼z → trans (reflexive $ Eq.sym x≈y) x∼z)
+
+record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 4 _≈_ _∼_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _∼_ : Rel Carrier ℓ₂
+ isPreorder : IsPreorder _≈_ _∼_
+
+ open IsPreorder isPreorder public
+
+
+
+
+
+
+record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ isEquivalence : IsEquivalence _≈_
+
+ open IsEquivalence isEquivalence public
+
+ isPreorder : IsPreorder _≡_ _≈_
+ isPreorder = record
+ { isEquivalence = PropEq.isEquivalence
+ ; reflexive = reflexive
+ ; trans = trans
+ }
+
+ preorder : Preorder c zero ℓ
+ preorder = record { isPreorder = isPreorder }
+
+
+
+ indexedSetoid : ∀ {i} {I : Set i} → I.Setoid I c _
+ indexedSetoid = record
+ { Carrier = λ _ → Carrier
+ ; _≈_ = _≈_
+ ; isEquivalence = record
+ { refl = refl
+ ; sym = sym
+ ; trans = trans
+ }
+ }
+
+
+
+
+record IsDecEquivalence {a ℓ} {A : Set a}
+ (_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where
+ infix 4 _≟_
+ field
+ isEquivalence : IsEquivalence _≈_
+ _≟_ : Decidable _≈_
+
+ open IsEquivalence isEquivalence public
+
+record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
+ infix 4 _≈_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ
+ isDecEquivalence : IsDecEquivalence _≈_
+
+ open IsDecEquivalence isDecEquivalence public
+
+ setoid : Setoid c ℓ
+ setoid = record { isEquivalence = isEquivalence }
+
+ open Setoid setoid public using (preorder)
+
+
+
+
+record IsPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
+ (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
+ Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ isPreorder : IsPreorder _≈_ _≤_
+ antisym : Antisymmetric _≈_ _≤_
+
+ open IsPreorder isPreorder public
+ renaming (∼-resp-≈ to ≤-resp-≈)
+
+record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 4 _≈_ _≤_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _≤_ : Rel Carrier ℓ₂
+ isPartialOrder : IsPartialOrder _≈_ _≤_
+
+ open IsPartialOrder isPartialOrder public
+
+ preorder : Preorder c ℓ₁ ℓ₂
+ preorder = record { isPreorder = isPreorder }
+
+
+
+
+record IsDecPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
+ (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
+ Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ infix 4 _≟_ _≤?_
+ field
+ isPartialOrder : IsPartialOrder _≈_ _≤_
+ _≟_ : Decidable _≈_
+ _≤?_ : Decidable _≤_
+
+ private
+ module PO = IsPartialOrder isPartialOrder
+ open PO public hiding (module Eq)
+
+ module Eq where
+
+ isDecEquivalence : IsDecEquivalence _≈_
+ isDecEquivalence = record
+ { isEquivalence = PO.isEquivalence
+ ; _≟_ = _≟_
+ }
+
+ open IsDecEquivalence isDecEquivalence public
+
+record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 4 _≈_ _≤_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _≤_ : Rel Carrier ℓ₂
+ isDecPartialOrder : IsDecPartialOrder _≈_ _≤_
+
+ private
+ module DPO = IsDecPartialOrder isDecPartialOrder
+ open DPO public hiding (module Eq)
+
+ poset : Poset c ℓ₁ ℓ₂
+ poset = record { isPartialOrder = isPartialOrder }
+
+ open Poset poset public using (preorder)
+
+ module Eq where
+
+ decSetoid : DecSetoid c ℓ₁
+ decSetoid = record { isDecEquivalence = DPO.Eq.isDecEquivalence }
+
+ open DecSetoid decSetoid public
+
+
+
+
+record IsStrictPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
+ (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
+ Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ isEquivalence : IsEquivalence _≈_
+ irrefl : Irreflexive _≈_ _<_
+ trans : Transitive _<_
+ <-resp-≈ : _<_ Respects₂ _≈_
+
+ module Eq = IsEquivalence isEquivalence
+
+record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
+
+ open IsStrictPartialOrder isStrictPartialOrder public
+
+
+
+
+record IsTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
+ (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
+ Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ isPartialOrder : IsPartialOrder _≈_ _≤_
+ total : Total _≤_
+
+ open IsPartialOrder isPartialOrder public
+
+record TotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 4 _≈_ _≤_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _≤_ : Rel Carrier ℓ₂
+ isTotalOrder : IsTotalOrder _≈_ _≤_
+
+ open IsTotalOrder isTotalOrder public
+
+ poset : Poset c ℓ₁ ℓ₂
+ poset = record { isPartialOrder = isPartialOrder }
+
+ open Poset poset public using (preorder)
+
+
+
+
+record IsDecTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
+ (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
+ Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ infix 4 _≟_ _≤?_
+ field
+ isTotalOrder : IsTotalOrder _≈_ _≤_
+ _≟_ : Decidable _≈_
+ _≤?_ : Decidable _≤_
+
+ private
+ module TO = IsTotalOrder isTotalOrder
+ open TO public hiding (module Eq)
+
+ module Eq where
+
+ isDecEquivalence : IsDecEquivalence _≈_
+ isDecEquivalence = record
+ { isEquivalence = TO.isEquivalence
+ ; _≟_ = _≟_
+ }
+
+ open IsDecEquivalence isDecEquivalence public
+
+record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 4 _≈_ _≤_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _≤_ : Rel Carrier ℓ₂
+ isDecTotalOrder : IsDecTotalOrder _≈_ _≤_
+
+ private
+ module DTO = IsDecTotalOrder isDecTotalOrder
+ open DTO public hiding (module Eq)
+
+ totalOrder : TotalOrder c ℓ₁ ℓ₂
+ totalOrder = record { isTotalOrder = isTotalOrder }
+
+ open TotalOrder totalOrder public using (poset; preorder)
+
+ module Eq where
+
+ decSetoid : DecSetoid c ℓ₁
+ decSetoid = record { isDecEquivalence = DTO.Eq.isDecEquivalence }
+
+ open DecSetoid decSetoid public
+
+
+
+
+
+
+record IsStrictTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
+ (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
+ Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+ field
+ isEquivalence : IsEquivalence _≈_
+ trans : Transitive _<_
+ compare : Trichotomous _≈_ _<_
+ <-resp-≈ : _<_ Respects₂ _≈_
+
+ infix 4 _≟_ _<?_
+
+ _≟_ : Decidable _≈_
+ _≟_ = tri⟶dec≈ compare
+
+ _<?_ : Decidable _<_
+ _<?_ = tri⟶dec< compare
+
+ isDecEquivalence : IsDecEquivalence _≈_
+ isDecEquivalence = record
+ { isEquivalence = isEquivalence
+ ; _≟_ = _≟_
+ }
+
+ module Eq = IsDecEquivalence isDecEquivalence
+
+ isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
+ isStrictPartialOrder = record
+ { isEquivalence = isEquivalence
+ ; irrefl = tri⟶irr <-resp-≈ Eq.sym compare
+ ; trans = trans
+ ; <-resp-≈ = <-resp-≈
+ }
+
+ open IsStrictPartialOrder isStrictPartialOrder public using (irrefl)
+
+record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+ infix 4 _≈_ _<_
+ field
+ Carrier : Set c
+ _≈_ : Rel Carrier ℓ₁
+ _<_ : Rel Carrier ℓ₂
+ isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
+
+ open IsStrictTotalOrder isStrictTotalOrder public
+ hiding (module Eq)
+
+ strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
+ strictPartialOrder =
+ record { isStrictPartialOrder = isStrictPartialOrder }
+
+ decSetoid : DecSetoid c ℓ₁
+ decSetoid = record { isDecEquivalence = isDecEquivalence }
+
+ module Eq = DecSetoid decSetoid
+
addfile ./html/Relation.Nullary.Core.html
hunk ./html/Relation.Nullary.Core.html 1
+
+Relation.Nullary.Core
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+
+
+module Relation.Nullary.Core where
+
+open import Data.Empty
+open import Level
+
+
+
+infix 3 ¬_
+
+¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
+¬ P = P → ⊥
+
+
+
+data Dec {p} (P : Set p) : Set p where
+ yes : ( p : P) → Dec P
+ no : (¬p : ¬ P) → Dec P
+
addfile ./html/Relation.Nullary.Decidable.html
hunk ./html/Relation.Nullary.Decidable.html 1
+
+Relation.Nullary.Decidable
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Relation.Nullary.Decidable where
+
+open import Data.Empty
+open import Function
+open import Function.Equality using (_⟨$⟩_)
+open import Function.Equivalence
+ using (_⇔_; equivalent; module Equivalent)
+open import Data.Bool
+open import Data.Product hiding (map)
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality
+
+⌊_⌋ : ∀ {p} {P : Set p} → Dec P → Bool
+⌊ yes _ ⌋ = true
+⌊ no _ ⌋ = false
+
+True : ∀ {p} {P : Set p} → Dec P → Set
+True Q = T ⌊ Q ⌋
+
+False : ∀ {p} {P : Set p} → Dec P → Set
+False Q = T (not ⌊ Q ⌋)
+
+
+
+toWitness : ∀ {p} {P : Set p} {Q : Dec P} → True Q → P
+toWitness {Q = yes p} _ = p
+toWitness {Q = no _} ()
+
+
+
+fromWitness : ∀ {p} {P : Set p} {Q : Dec P} → P → True Q
+fromWitness {Q = yes p} = const _
+fromWitness {Q = no ¬p} = ¬p
+
+map : ∀ {p q} {P : Set p} {Q : Set q} → P ⇔ Q → Dec P → Dec Q
+map P⇔Q (yes p) = yes (Equivalent.to P⇔Q ⟨$⟩ p)
+map P⇔Q (no ¬p) = no (¬p ∘ _⟨$⟩_ (Equivalent.from P⇔Q))
+
+map′ : ∀ {p q} {P : Set p} {Q : Set q} →
+ (P → Q) → (Q → P) → Dec P → Dec Q
+map′ P→Q Q→P = map (equivalent P→Q Q→P)
+
+fromYes : ∀ {p} {P : Set p} → P → Dec P → P
+fromYes _ (yes p) = p
+fromYes p (no ¬p) = ⊥-elim (¬p p)
+
+fromYes-map-commute :
+ ∀ {p q} {P : Set p} {Q : Set q} {x y} (P⇔Q : P ⇔ Q) (d : Dec P) →
+ fromYes y (map P⇔Q d) ≡ Equivalent.to P⇔Q ⟨$⟩ fromYes x d
+fromYes-map-commute _ (yes p) = refl
+fromYes-map-commute {x = p} _ (no ¬p) = ⊥-elim (¬p p)
+
addfile ./html/Relation.Nullary.Negation.html
hunk ./html/Relation.Nullary.Negation.html 1
+
+Relation.Nullary.Negation
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Relation.Nullary.Negation where
+
+open import Relation.Nullary
+open import Relation.Unary
+open import Data.Bool
+open import Data.Empty
+open import Function
+open import Data.Product as Prod
+open import Data.Fin
+open import Data.Fin.Dec
+open import Data.Sum as Sum
+open import Category.Monad
+open import Level
+
+contradiction : ∀ {p w} {P : Set p} {Whatever : Set w} →
+ P → ¬ P → Whatever
+contradiction p ¬p = ⊥-elim (¬p p)
+
+contraposition : ∀ {p q} {P : Set p} {Q : Set q} →
+ (P → Q) → ¬ Q → ¬ P
+contraposition f ¬q p = contradiction (f p) ¬q
+
+
+
+private
+ note : ∀ {p q} {P : Set p} {Q : Set q} →
+ (P → ¬ Q) → Q → ¬ P
+ note = flip
+
+
+
+
+∃⟶¬∀¬ : ∀ {a p} {A : Set a} {P : A → Set p} →
+ ∃ P → ¬ (∀ x → ¬ P x)
+∃⟶¬∀¬ = flip uncurry
+
+∀⟶¬∃¬ : ∀ {a p} {A : Set a} {P : A → Set p} →
+ (∀ x → P x) → ¬ ∃ λ x → ¬ P x
+∀⟶¬∃¬ ∀xPx (x , ¬Px) = ¬Px (∀xPx x)
+
+¬∃⟶∀¬ : ∀ {a p} {A : Set a} {P : A → Set p} →
+ ¬ ∃ (λ x → P x) → ∀ x → ¬ P x
+¬∃⟶∀¬ = curry
+
+∀¬⟶¬∃ : ∀ {a p} {A : Set a} {P : A → Set p} →
+ (∀ x → ¬ P x) → ¬ ∃ (λ x → P x)
+∀¬⟶¬∃ = uncurry
+
+∃¬⟶¬∀ : ∀ {a p} {A : Set a} {P : A → Set p} →
+ ∃ (λ x → ¬ P x) → ¬ (∀ x → P x)
+∃¬⟶¬∀ = flip ∀⟶¬∃¬
+
+
+
+
+¬∀⟶∃¬ : ∀ n {p} (P : Fin n → Set p) → (∀ i → Dec (P i)) →
+ ¬ (∀ i → P i) → ∃ λ i → ¬ P i
+¬∀⟶∃¬ n P dec ¬P = Prod.map id proj₁ $ ¬∀⟶∃¬-smallest n P dec ¬P
+
+
+
+
+¬¬-map : ∀ {p q} {P : Set p} {Q : Set q} →
+ (P → Q) → ¬ ¬ P → ¬ ¬ Q
+¬¬-map f = contraposition (contraposition f)
+
+
+
+Stable : ∀ {ℓ} → Set ℓ → Set ℓ
+Stable P = ¬ ¬ P → P
+
+
+
+stable : ∀ {p} {P : Set p} → ¬ ¬ Stable P
+stable ¬[¬¬p→p] = ¬[¬¬p→p] (λ ¬¬p → ⊥-elim (¬¬p (¬[¬¬p→p] ∘ const)))
+
+
+
+negated-stable : ∀ {p} {P : Set p} → Stable (¬ P)
+negated-stable ¬¬¬P P = ¬¬¬P (λ ¬P → ¬P P)
+
+
+
+decidable-stable : ∀ {p} {P : Set p} → Dec P → Stable P
+decidable-stable (yes p) ¬¬p = p
+decidable-stable (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p)
+
+¬-drop-Dec : ∀ {p} {P : Set p} → Dec (¬ ¬ P) → Dec (¬ P)
+¬-drop-Dec (yes ¬¬p) = no ¬¬p
+¬-drop-Dec (no ¬¬¬p) = yes (negated-stable ¬¬¬p)
+
+
+
+
+¬¬-Monad : RawMonad (λ P → ¬ ¬ P)
+¬¬-Monad = record
+ { return = contradiction
+ ; _>>=_ = λ x f → negated-stable (¬¬-map f x)
+ }
+
+¬¬-push : ∀ {p q} {P : Set p} {Q : P → Set q} →
+ ¬ ¬ ((x : P) → Q x) → (x : P) → ¬ ¬ Q x
+¬¬-push ¬¬P⟶Q P ¬Q = ¬¬P⟶Q (λ P⟶Q → ¬Q (P⟶Q P))
+
+
+
+
+excluded-middle : ∀ {p} {P : Set p} → ¬ ¬ Dec P
+excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))
+
+
+
+
+
+
+
+
+
+
+call/cc : ∀ {w p} {Whatever : Set w} {P : Set p} →
+ ((P → Whatever) → ¬ ¬ P) → ¬ ¬ P
+call/cc hyp ¬p = hyp (λ p → ⊥-elim (¬p p)) ¬p
+
+
+
+
+independence-of-premise
+ : ∀ {p q r} {P : Set p} {Q : Set q} {R : Q → Set r} →
+ Q → (P → Σ Q R) → ¬ ¬ Σ Q (λ x → P → R x)
+independence-of-premise {P = P} q f = ¬¬-map helper excluded-middle
+ where
+ helper : Dec P → _
+ helper (yes p) = Prod.map id const (f p)
+ helper (no ¬p) = (q , ⊥-elim ∘′ ¬p)
+
+
+
+independence-of-premise-⊎
+ : ∀ {p q r} {P : Set p} {Q : Set q} {R : Set r} →
+ (P → Q ⊎ R) → ¬ ¬ ((P → Q) ⊎ (P → R))
+independence-of-premise-⊎ {P = P} f = ¬¬-map helper excluded-middle
+ where
+ helper : Dec P → _
+ helper (yes p) = Sum.map const const (f p)
+ helper (no ¬p) = inj₁ (⊥-elim ∘′ ¬p)
+
+private
+
+
+
+
+
+ corollary : ∀ {p ℓ} {P : Set p} {Q R : Set ℓ} →
+ (P → Q ⊎ R) → ¬ ¬ ((P → Q) ⊎ (P → R))
+ corollary {P = P} {Q} {R} f =
+ ¬¬-map helper (independence-of-premise
+ true ([ _,_ true , _,_ false ] ∘′ f))
+ where
+ helper : ∃ (λ b → P → if b then Q else R) → (P → Q) ⊎ (P → R)
+ helper (true , f) = inj₁ f
+ helper (false , f) = inj₂ f
+
+
+
+
+Excluded-Middle : (ℓ : Level) → Set (suc ℓ)
+Excluded-Middle p = {P : Set p} → Dec P
+
+Double-Negation-Elimination : (ℓ : Level) → Set (suc ℓ)
+Double-Negation-Elimination p = {P : Set p} → Stable P
+
+private
+
+
+
+
+ em⇒dne : ∀ {ℓ} → Excluded-Middle ℓ → Double-Negation-Elimination ℓ
+ em⇒dne em = decidable-stable em
+
+ dne⇒em : ∀ {ℓ} → Double-Negation-Elimination ℓ → Excluded-Middle ℓ
+ dne⇒em dne = dne excluded-middle
+
addfile ./html/Relation.Nullary.html
hunk ./html/Relation.Nullary.html 1
+
+Relation.Nullary
+
+
+
+
+
+module Relation.Nullary where
+
+import Relation.Nullary.Core as Core
+
+
+
+
+open Core public using (¬_)
+
+
+
+
+open Core public using (Dec; yes; no)
+
addfile ./html/Relation.Unary.html
hunk ./html/Relation.Unary.html 1
+
+Relation.Unary
+
+
+
+{-# OPTIONS --universe-polymorphism #-}
+
+module Relation.Unary where
+
+open import Data.Empty
+open import Function
+open import Data.Unit
+open import Data.Product
+open import Data.Sum
+open import Level
+open import Relation.Nullary
+
+
+
+
+Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
+Pred A ℓ = A → Set ℓ
+
+
+
+
+
+
+private
+ module Dummy {a} {A : Set a}
+ where
+
+
+
+ infix 4 _∈_ _∉_
+
+ _∈_ : ∀ {ℓ} → A → Pred A ℓ → Set _
+ x ∈ P = P x
+
+ _∉_ : ∀ {ℓ} → A → Pred A ℓ → Set _
+ x ∉ P = ¬ x ∈ P
+
+
+
+ ∅ : Pred A zero
+ ∅ = λ _ → ⊥
+
+
+
+ Empty : ∀ {ℓ} → Pred A ℓ → Set _
+ Empty P = ∀ x → x ∉ P
+
+ ∅-Empty : Empty ∅
+ ∅-Empty x ()
+
+
+
+ U : Pred A zero
+ U = λ _ → ⊤
+
+
+
+ Universal : ∀ {ℓ} → Pred A ℓ → Set _
+ Universal P = ∀ x → x ∈ P
+
+ U-Universal : Universal U
+ U-Universal = λ _ → _
+
+
+
+ ∁ : ∀ {ℓ} → Pred A ℓ → Pred A ℓ
+ ∁ P = λ x → x ∉ P
+
+ ∁∅-Universal : Universal (∁ ∅)
+ ∁∅-Universal = λ x x∈∅ → x∈∅
+
+ ∁U-Empty : Empty (∁ U)
+ ∁U-Empty = λ x x∈∁U → x∈∁U _
+
+
+
+ infix 4 _⊆_ _⊇_ _⊆′_ _⊇′_
+
+ _⊆_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
+ P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q
+
+ _⊆′_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
+ P ⊆′ Q = ∀ x → x ∈ P → x ∈ Q
+
+ _⊇_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
+ Q ⊇ P = P ⊆ Q
+
+ _⊇′_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
+ Q ⊇′ P = P ⊆′ Q
+
+ ∅-⊆ : ∀ {ℓ} → (P : Pred A ℓ) → ∅ ⊆ P
+ ∅-⊆ P ()
+
+ ⊆-U : ∀ {ℓ} → (P : Pred A ℓ) → P ⊆ U
+ ⊆-U P _ = _
+
+
+
+ infixl 6 _∪_
+
+ _∪_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
+ P ∪ Q = λ x → x ∈ P ⊎ x ∈ Q
+
+
+
+ infixl 7 _∩_
+
+ _∩_ : ∀ {ℓ₁ ℓ₂} → Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
+ P ∩ Q = λ x → x ∈ P × x ∈ Q
+
+open Dummy public
+
+
+
+
+infixr 2 _⟨×⟩_
+infixr 1 _⟨⊎⟩_
+infixr 0 _⟨→⟩_
+
+_⟨×⟩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
+ Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
+P ⟨×⟩ Q = uncurry (λ p q → P p × Q q)
+
+_⟨⊎⟩_ : ∀ {a b ℓ} {A : Set a} {B : Set b} →
+ Pred A ℓ → Pred B ℓ → Pred (A ⊎ B) _
+P ⟨⊎⟩ Q = [ P , Q ]
+
+_⟨→⟩_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} →
+ Pred A ℓ₁ → Pred B ℓ₂ → Pred (A → B) _
+(P ⟨→⟩ Q) f = P ⊆ Q ∘ f
+
addfile ./html/Schema.html
hunk ./html/Schema.html 1
+
+Schema
+module Schema where
+
+open import Data.Nat
+open import Data.Bool
+open import List
+open import Maybe
+open import Data.Product hiding (map)
+import Data.String as String
+open String using (String)
+open import Data.Char hiding (_==_)
+open import Relation.Binary.PropositionalEquality
+
+open import BString
+open import Util
+open import Eq
+
+data FieldType : Set where
+ string : ℕ → FieldType
+ number : FieldType
+ date : FieldType
+ time : FieldType
+
+TableName = String
+FieldName = String
+Attribute = FieldName × FieldType
+TableType = List Attribute
+Schema = List (TableName × TableType)
+
+_=FT=_ : FieldType → FieldType → Bool
+string n =FT= string m = n == m
+number =FT= number = true
+date =FT= date = true
+time =FT= time = true
+_ =FT= _ = false
+
+_=TT=_ : TableType → TableType → Bool
+[] =TT= [] = true
+((f₁ , t₁) ∷ tt₁) =TT= ((f₂ , t₂) ∷ tt₂) =
+ (f₁ == f₂) ∧ (t₁ =FT= t₂) ∧ (tt₁ =TT= tt₂)
+_ =TT= _ = false
+
+record Date : Set where
+ field
+ year : ℕ
+ month : ℕ
+ day : ℕ
+
+record Time : Set where
+ field
+ hour : ℕ
+ minute : ℕ
+ second : ℕ
+ millisecond : ℕ
+
+mkDate : ℕ → ℕ → ℕ → Date
+mkDate y m d = record { year = y; month = m; day = d }
+
+mkTime : ℕ → ℕ → ℕ → ℕ → Time
+mkTime h m s ms = record { hour = h; minute = m; second = s; millisecond = ms }
+
+Field : FieldType → Set
+Field (string n) = BList Char n
+Field number = ℕ
+Field date = Date
+Field time = Time
+
+
+
+{-# IMPORT Database.Firebird #-}
+
+data HsFieldType : Set where
+ text : Integer → HsFieldType
+ vartext : Integer → HsFieldType
+ short : HsFieldType
+ long : HsFieldType
+ date : HsFieldType
+ time : HsFieldType
+
+{-# COMPILED_DATA HsFieldType FieldType Text VarText Short Long Date Time #-}
+
+data HsColumnInfo : Set where
+ colInfo : String → HsFieldType → HsColumnInfo
+
+{-# COMPILED_DATA HsColumnInfo ColumnInfo ColInfo #-}
+
+parseHsFieldType : HsFieldType → FieldType
+parseHsFieldType (text n) = string (primIntegerAbs n)
+parseHsFieldType (vartext n) = string (primIntegerAbs n)
+parseHsFieldType short = number
+parseHsFieldType long = number
+parseHsFieldType date = date
+parseHsFieldType time = time
+
+parseHsColumnInfo : HsColumnInfo → Attribute
+parseHsColumnInfo (colInfo name type) = name , parseHsFieldType type
+
+parseTableInfo : List HsColumnInfo → TableType
+parseTableInfo = map parseHsColumnInfo
+
+
+Cars : TableType
+Cars = ("Model" , string 20)
+ ∷ ("Time" , time)
+ ∷ ("Wet" , number)
+ ∷ []
+
+Students : TableType
+Students =
+ ("Name" , string 30)
+ ∷ ("Passed" , number)
+ ∷ []
+
+infixr 40 _∷_
+data Row : TableType → Set where
+ [] : Row []
+ _∷_ : forall {name ft schema} →
+ Field ft → Row schema → Row ((name , ft) ∷ schema)
+
+zonda : Row Cars
+zonda = bString "Pagani Zonda C122 F"
+ ∷ mkTime 0 1 18 400
+ ∷ 0
+ ∷ []
+
+
addfile ./html/Util.html
hunk ./html/Util.html 1
+
+Util
+module Util where
+
+open import Data.Nat
+open import List
+open import Data.Product hiding (map)
+open import IO.Primitive
+open import Function
+open import Data.Bool renaming (T to isTrue)
+open import Relation.Binary.PropositionalEquality
+open import Maybe
+open import Data.String hiding (_==_)
+open import Eq
+
+postulate Integer : Set
+{-# BUILTIN INTEGER Integer #-}
+{-# COMPILED_TYPE Integer Integer #-}
+
+primitive primIntegerAbs : Integer → ℕ
+ primNatToInteger : ℕ → Integer
+
+postulate showInteger : Integer → String
+{-# COMPILED showInteger (show :: Integer -> String) #-}
+
+showNat : ℕ → String
+showNat = showInteger ∘ primNatToInteger
+
+primitive primStringAppend : String → String → String
+
+postulate
+ ioError : {A : Set} → String → IO A
+
+{-# COMPILED ioError (\_ -> error) #-}
+
+_<$>_ : {A B : Set} → (A → B) → IO A → IO B
+f <$> m = m >>= \x → return (f x)
+
+withMaybe : {A B : Set} → Maybe A → B → (A → B) → B
+withMaybe nothing n j = n
+withMaybe (just x) n j = j x
+
+bindMaybe : {A B : Set} → Maybe A → (A → Maybe B) → Maybe B
+bindMaybe m f = withMaybe m nothing f
+
+mapMaybe : {A B : Set} → (A → Maybe B) → List A → Maybe (List B)
+mapMaybe f [] = just []
+mapMaybe f (x ∷ xs) =
+ bindMaybe (f x) \y →
+ bindMaybe (mapMaybe f xs) \ys →
+ just (y ∷ ys)
+
+elem : {u : EqType} → El u → List (El u) → Bool
+elem x xs = any (_==_ x) xs
+
+nub : {u : EqType} → List (El u) → List (El u)
+nub [] = []
+nub (x ∷ xs) = x ∷ filter (\y → not (x == y)) (nub xs)
+
+lookup : {u : EqType}{A : Set} → El u → List (El u × A) → Maybe A
+lookup x [] = nothing
+lookup x ((y , z) ∷ xs) with x == y
+... | true = just z
+... | false = lookup x xs
+
+haskey : {u : EqType}{A : Set} → El u → List (El u × A) → Bool
+haskey x xs = elem x (map proj₁ xs)
+
+hasKeys : {u : EqType}{A : Set} → List (El u) → List (El u × A) → Bool
+hasKeys [] xs = true
+hasKeys (k ∷ ks) xs = haskey k xs ∧ hasKeys ks xs
+
+lookup' : {u : EqType}{A : Set}(x : El u)(xs : List (El u × A)) →
+ isTrue (elem x (map proj₁ xs)) → A
+lookup' x [] ()
+lookup' x ((y , z) ∷ xs) p with x == y
+... | true = z
+... | false = lookup' x xs p
+
+istrue : ∀ {b} → true ≡ b → isTrue b
+istrue refl = _
+
+isfalse : ∀ {b} → false ≡ b → isTrue (not b)
+isfalse refl = _
+