text:
module Esterel.Lang.CanFunction.Plug where

open import Data.Nat using (_+_ ; suc)
open import Function using (_∋_ ; _∘_ ; id ; _$_)
open import Data.Nat.Properties.Simple using ( +-comm ; +-assoc)
open import utility
open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Lang.CanFunction
open import Esterel.Environment as Env
open import Esterel.Context
open import Esterel.Context.Properties
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.List using ([] ; [_] ; _∷_ ; List ; _++_)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; subst ; cong ; trans ; module ≡-Reasoning ; cong₂ ; subst₂ ; inspect)
open import Data.Empty
open import Esterel.Lang.Binding
open import Data.Maybe using ( nothing ; just )
open import Data.List.Any
open import Data.List.Any.Properties
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ )
open import Esterel.Lang.CanFunction.SetSigMonotonic

open ≡-Reasoning using (_≡⟨_⟩_ ; _≡⟨⟩_ ; _∎)

open import Relation.Nullary.Decidable
  using (⌊_⌋)
open import Data.FiniteMap
import Data.OrderedListMap as OMap
open import Data.Nat as Nat using (ℕ)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ ; _≟ₛₜ_)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)
open import Esterel.CompletionCode as Code renaming (CompletionCode to Code)

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM
open ListSet Code._≟_
module NSet = ListSet Nat._≟_

canθₖ-plug : ∀ S' sigs → ∀ C p q
             → (Canₖq⊆Canₖp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))
             → (Canₛq⊆Canₛp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))
             → (∀ θ k → k ∈ (Canθₖ sigs S' (C ⟦ q ⟧c) θ) → k ∈ (Canθₖ sigs S' (C ⟦ p ⟧c) θ))

canθₛ-plug : ∀ S' sigs → ∀ C p q
             → (Canₛq⊆Canₛp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))
             → (Canₖq⊆Canₖp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))
             → (∀ θ k → k ∈ (Canθₛ sigs S' (C ⟦ q ⟧c) θ) → k ∈ (Canθₛ sigs S' (C ⟦ p ⟧c) θ))
canθₛₕ-plug : ∀ S' sigs → ∀ C p q
              → (Canₛₕq⊆Canₛₕp : ∀ θ → (Canₛₕ q θ) ⊆¹ (Canₛₕ p θ))
              → (Canₛq⊆Canₛp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))
              → (Canₖq⊆Canₖp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))
              → (∀ θ k → k ∈ (Canθₛₕ sigs S' (C ⟦ q ⟧c) θ) → k ∈ (Canθₛₕ sigs S' (C ⟦ p ⟧c) θ))

canₛₕ-plug : ∀ C p q
           → (Canₛₕq⊆Canₛₕp : ∀ θ → (Canₛₕ q θ) ⊆¹ (Canₛₕ p θ))
           → (∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))
           → (Canₛq⊆Canₛp : ∀ θ → (Canₛ q θ) ⊆¹ (Canₛ p θ))
           → (∀ θ → (Canₛₕ (C ⟦ q ⟧c) θ) ⊆¹ (Canₛₕ (C ⟦ p ⟧c) θ))

canₖ-plug : ∀ C p q
            → (Canₖq⊆Canₖp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))
            → (Canₛq⊆Canₛp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))
            → (∀ θ k → k ∈ (Canₖ (C ⟦ q ⟧c) θ) → k ∈ (Canₖ (C ⟦ p ⟧c) θ))
canₛ-plug : ∀ C p q
            → (Canₛq⊆Canₛp : ∀ θ → (Canₛ q θ) ⊆¹ (Canₛ p θ))
            → (∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))
            → (∀ θ → (Canₛ (C ⟦ q ⟧c) θ) ⊆¹ (Canₛ (C ⟦ p ⟧c) θ))

canθₖ-plug S' [] C p q Canₖq⊆Canₖp Canₛq⊆Canₛp = canₖ-plug C p q Canₖq⊆Canₖp Canₛq⊆Canₛp
canθₖ-plug S' (just Signal.present ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ = canθₖ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _)
canθₖ-plug S' (just Signal.absent ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ = canθₖ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _)
canθₖ-plug S' (nothing ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp = canθₖ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp
canθₖ-plug S' (just Signal.unknown ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ
  with any (Nat._≟_ S') (Canθₛ sigs (suc S') (C ⟦ p ⟧c) (θ ← ([S]-env (S' ₛ))))
     | any (Nat._≟_ S') (Canθₛ sigs (suc S') (C ⟦ q ⟧c) (θ ← ([S]-env (S' ₛ))))
canθₖ-plug S' (just Signal.unknown ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ | yes p₁ | (yes p₂) = canθₖ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _)
canθₖ-plug S' (just Signal.unknown ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ | yes p₁ | (no ¬p)
  with sig-←-monoʳ (S' ₛ) ([S]-env (S' ₛ)) θ (sig-∈-single (S' ₛ) Signal.unknown)
... | S'∈θ←[S]env
  rewrite ((θ ← [S]-env-absent (S' ₛ)) ≡ (set-sig{S' ₛ} (θ ← [S]-env (S' ₛ)) S'∈θ←[S]env Signal.absent)
            ∋
            (θ ← [S]-env-absent (S' ₛ))
             ≡⟨ cong (θ ←_) (sym (←-single-overwrite-sig (S' ₛ) Signal.unknown
                                    ([S]-env-absent (S' ₛ)) ((sig-∈-single (S' ₛ) Signal.absent)))) ⟩
             (θ ← (([S]-env (S' ₛ)) ← [S]-env-absent (S' ₛ)))
             ≡⟨ ←-assoc θ ([S]-env (S' ₛ)) ([S]-env-absent (S' ₛ)) ⟩
             ((θ ← ([S]-env (S' ₛ))) ← ([S]-env-absent (S' ₛ)))
             ≡⟨ sym (sig-set=← (θ ← [S]-env (S' ₛ)) (S' ₛ) Signal.absent  S'∈θ←[S]env) ⟩
             (set-sig{S' ₛ} (θ ← [S]-env (S' ₛ)) S'∈θ←[S]env Signal.absent) ∎)

  with canθₖ-set-sig-monotonic sigs (suc S') (C ⟦ q ⟧c) (S' ₛ) (θ ← [S]-env (S' ₛ))
                               S'∈θ←[S]env Signal.absent
                               (trans (sig-stats-←-right-irr' (S' ₛ) θ ([S]-env (S' ₛ)) (sig-∈-single (S' ₛ) Signal.unknown) S'∈θ←[S]env) (sig-stats-1map' (S' ₛ) Signal.unknown ((sig-∈-single (S' ₛ) Signal.unknown))))
                               (n∉map-suc-n-+ S' (SigM.Dom' sigs))
... | Canabsq⊂Canunq
   = λ k x → (canθₖ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _)) k (Canabsq⊂Canunq k x)
canθₖ-plug S' (just Signal.unknown ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ | no ¬p | (yes p₁)
  = ⊥-elim (¬p ((canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)) _ p₁ ))
canθₖ-plug S' (just Signal.unknown ∷ sigs) C p q Canₖq⊆Canₖp Canₛq⊆Canₛp θ | no ¬p | (no ¬p₁) = canθₖ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _)

canθₛ-plug S' [] C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ
canθₛ-plug S' (nothing ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ
canθₛ-plug S' (just Signal.present ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)
canθₛ-plug S' (just Signal.absent ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)
canθₛ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ
  with any (Nat._≟_ S') (Canθₛ sigs (suc S') (C ⟦ p ⟧c) (θ ← ([S]-env (S' ₛ))))
     | any (Nat._≟_ S') (Canθₛ sigs (suc S') (C ⟦ q ⟧c) (θ ← ([S]-env (S' ₛ))))
canθₛ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ | yes p₁ | (yes p₂) = canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)
canθₛ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ | yes p₁ | (no ¬p)
  with sig-←-monoʳ (S' ₛ) ([S]-env (S' ₛ)) θ (sig-∈-single (S' ₛ) Signal.unknown)
... | S'∈θ←[S]env
  rewrite ((θ ← [S]-env-absent (S' ₛ)) ≡ (set-sig{S' ₛ} (θ ← [S]-env (S' ₛ)) S'∈θ←[S]env Signal.absent)
            ∋
            (θ ← [S]-env-absent (S' ₛ))
             ≡⟨ cong (θ ←_) (sym (←-single-overwrite-sig (S' ₛ) Signal.unknown
                                    ([S]-env-absent (S' ₛ)) ((sig-∈-single (S' ₛ) Signal.absent)))) ⟩
             (θ ← (([S]-env (S' ₛ)) ← [S]-env-absent (S' ₛ)))
             ≡⟨ ←-assoc θ ([S]-env (S' ₛ)) ([S]-env-absent (S' ₛ)) ⟩
             ((θ ← ([S]-env (S' ₛ))) ← ([S]-env-absent (S' ₛ)))
             ≡⟨ sym (sig-set=← (θ ← [S]-env (S' ₛ)) (S' ₛ) Signal.absent  S'∈θ←[S]env) ⟩
             (set-sig{S' ₛ} (θ ← [S]-env (S' ₛ)) S'∈θ←[S]env Signal.absent) ∎)
   with canθₛ-set-sig-monotonic sigs (suc S') (C ⟦ q ⟧c) (S' ₛ) (θ ← [S]-env (S' ₛ))
                               S'∈θ←[S]env Signal.absent
                               (trans (sig-stats-←-right-irr' (S' ₛ) θ ([S]-env (S' ₛ)) (sig-∈-single (S' ₛ) Signal.unknown) S'∈θ←[S]env) (sig-stats-1map' (S' ₛ) Signal.unknown ((sig-∈-single (S' ₛ) Signal.unknown))))
                               (n∉map-suc-n-+ S' (SigM.Dom' sigs))
... | Canabsq⊂Canunq
   = λ k x → (canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)) k (Canabsq⊂Canunq k x)

canθₛ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ | no ¬p | (yes p₁)
  = ⊥-elim (¬p ((canθₛ-plug (suc S') sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _) _ p₁))
canθₛ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ | no ¬p | (no ¬p₁) = canθₛ-plug (suc S') sigs C p q Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)

canθₛₕ-plug S' [] C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ
canθₛₕ-plug S' (nothing ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canθₛₕ-plug (suc S') sigs C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ
canθₛₕ-plug S' (just Signal.present ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canθₛₕ-plug (suc S') sigs C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)
canθₛₕ-plug S' (just Signal.absent ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canθₛₕ-plug (suc S') sigs C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)
canθₛₕ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ
  with any (Nat._≟_ S') (Canθₛ sigs (suc S') (C ⟦ p ⟧c) (θ ← ([S]-env (S' ₛ))))
     | any (Nat._≟_ S') (Canθₛ sigs (suc S') (C ⟦ q ⟧c) (θ ← ([S]-env (S' ₛ))))
canθₛₕ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ | yes p₁ | (yes p₂) =  canθₛₕ-plug (suc S') sigs C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)
canθₛₕ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp Canₛq⊆Canₛp θ | yes p₁ | (no ¬p)
  with sig-←-monoʳ (S' ₛ) ([S]-env (S' ₛ)) θ (sig-∈-single (S' ₛ) Signal.unknown)
... | S'∈θ←[S]env
  rewrite ((θ ← [S]-env-absent (S' ₛ)) ≡ (set-sig{S' ₛ} (θ ← [S]-env (S' ₛ)) S'∈θ←[S]env Signal.absent)
            ∋
            (θ ← [S]-env-absent (S' ₛ))
             ≡⟨ cong (θ ←_) (sym (←-single-overwrite-sig (S' ₛ) Signal.unknown
                                    ([S]-env-absent (S' ₛ)) ((sig-∈-single (S' ₛ) Signal.absent)))) ⟩
             (θ ← (([S]-env (S' ₛ)) ← [S]-env-absent (S' ₛ)))
             ≡⟨ ←-assoc θ ([S]-env (S' ₛ)) ([S]-env-absent (S' ₛ)) ⟩
             ((θ ← ([S]-env (S' ₛ))) ← ([S]-env-absent (S' ₛ)))
             ≡⟨ sym (sig-set=← (θ ← [S]-env (S' ₛ)) (S' ₛ) Signal.absent  S'∈θ←[S]env) ⟩
             (set-sig{S' ₛ} (θ ← [S]-env (S' ₛ)) S'∈θ←[S]env Signal.absent) ∎)
                with canθₛₕ-set-sig-monotonic sigs (suc S') (C ⟦ q ⟧c) (S' ₛ) (θ ← [S]-env (S' ₛ))
                               S'∈θ←[S]env Signal.absent
                               (trans (sig-stats-←-right-irr' (S' ₛ) θ ([S]-env (S' ₛ)) (sig-∈-single (S' ₛ) Signal.unknown) S'∈θ←[S]env) (sig-stats-1map' (S' ₛ) Signal.unknown ((sig-∈-single (S' ₛ) Signal.unknown))))
                               (n∉map-suc-n-+ S' (SigM.Dom' sigs))
... |  Canabsq⊂Canunq
   = λ k x → (canθₛₕ-plug (suc S') sigs C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _)) k (Canabsq⊂Canunq k x)

canθₛₕ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ | no ¬p | (yes p₁)
  = ⊥-elim (¬p (canθₛ-plug (suc S') sigs C p q Canₖq⊆Canₖp Canₛq⊆Canₛp (θ ← _) _ p₁))
canθₛₕ-plug S' (just Signal.unknown ∷ sigs) C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp θ | no ¬p | (no ¬p₁) = canθₛₕ-plug (suc S') sigs C p q Canₛₕq⊆Canₛₕp Canₛq⊆Canₛp Canₖq⊆Canₖp (θ ← _)

canₖ-plug [] p q Canₖq⊆Canₖp _ = Canₖq⊆Canₖp
canₖ-plug (ceval (epar₁ q) ∷ C) p q₁ Canₖq⊆Canₖp ⊂s θ = map-mono² Code._⊔_ (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ) (λ x y → y)
canₖ-plug (ceval (epar₂ p) ∷ C) p₁ q Canₖq⊆Canₖp ⊂s θ = map-mono²{xs = Canₖ p θ} Code._⊔_ (λ x y → y) (canₖ-plug C p₁ q Canₖq⊆Canₖp ⊂s θ)
canₖ-plug (ceval (eloopˢ q) ∷ C) p q₁ Canₖq⊆Canₖp ⊂s θ = canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ
canₖ-plug (ceval (eseq q) ∷ C) p q₁ Canₖq⊆Canₖp ⊂s θ with any (Code.nothin Code.≟_) (Canₖ (C ⟦ p ⟧c) θ) | any (Code.nothin Code.≟_) (Canₖ (C ⟦ q₁ ⟧c) θ)
... | yes 0∈CanC⟦p⟧ | yes 0∈CanC⟦q⟧ = codesub++both ((codesub- Code.nothin (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ))) (λ x y → y)
... | yes 0∈CanC⟦p⟧ | no  0∉CanC⟦q⟧ = λ k x → ++ˡ (set-remove-not-removed{Code.nothin}{k} (λ {refl → 0∉CanC⟦q⟧ x}) (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ _ x))
... | no  0∉CanC⟦p⟧ | yes 0∈CanC⟦q⟧ = ⊥-elim (0∉CanC⟦p⟧ (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ _ 0∈CanC⟦q⟧))
... | no  0∉CanC⟦p⟧ | no  0∉CanC⟦q⟧ = canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ
canₖ-plug (ceval (esuspend S) ∷ C) p q Canₖq⊆Canₖp ⊂s = canₖ-plug C p q Canₖq⊆Canₖp ⊂s
canₖ-plug (ceval etrap ∷ C) p q Canₖq⊆Canₖp ⊂s =   λ θ →  map-mono Code.↓* (canₖ-plug C p q Canₖq⊆Canₖp ⊂s θ)
canₖ-plug (csignl S ∷ C) p q Canₖq⊆Canₖp ⊂s θ = canθₖ-plug 0 (sig ([S]-env S)) C p q Canₖq⊆Canₖp ⊂s θ
canₖ-plug (cpresent₁ S q ∷ C) p q₁ Canₖq⊆Canₖp ⊂s θ with Sig∈ S θ
... | no  S∉Domθ = codesub++both (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ) (λ x y → y)
... | yes S∈Domθ with (Signal.present ≟ₛₜ (sig-stats{S} θ S∈Domθ))
... | yes _ = canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ
... | no  _ with (Signal.absent ≟ₛₜ (sig-stats{S} θ S∈Domθ))
... | yes _ = λ k z → z
... | no  _ = codesub++both (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ) (λ x y → y)
canₖ-plug (cpresent₂ S p₁ ∷ C) p q Canₖq⊆Canₖp ⊂s θ with Sig∈ S θ
... | no  S∉Domθ = codesub++both{a = Canₖ p₁ θ} (λ x y → y) (canₖ-plug C p q Canₖq⊆Canₖp ⊂s θ)
... | yes S∈Domθ with (Signal.present ≟ₛₜ (sig-stats{S} θ S∈Domθ))
... | yes _ = λ x y → y
... | no  _ with (Signal.absent ≟ₛₜ (sig-stats{S} θ S∈Domθ))
... | yes _ = canₖ-plug C p q Canₖq⊆Canₖp ⊂s θ
... | no  _ = codesub++both{a = Canₖ p₁ θ} (λ x y → y) (canₖ-plug C p q Canₖq⊆Canₖp ⊂s θ)
canₖ-plug (cloop ∷ C) p q Canₖq⊆Canₖp ⊂s = (canₖ-plug C p q Canₖq⊆Canₖp ⊂s)
canₖ-plug (cloopˢ₂ p ∷ C) p₁ q Canₖq⊆Canₖp ⊂s θ = λ k z → z
canₖ-plug (cseq₂ p ∷ C) p₁ q Canₖq⊆Canₖp ⊂s θ with any (Code.nothin Code.≟_) (Canₖ p θ)
... | yes 0∈Canp = codesub++both{a = set-remove (Canₖ p θ) Code.nothin } (λ x y → y) (canₖ-plug C p₁ q Canₖq⊆Canₖp ⊂s θ)
... | no  0∉Canp = λ x y → y
canₖ-plug (cshared s e ∷ C) p q Canₖq⊆Canₖp ⊂s = (canₖ-plug C p q Canₖq⊆Canₖp ⊂s)
canₖ-plug (cvar x e ∷ C) p q Canₖq⊆Canₖp ⊂s = (canₖ-plug C p q Canₖq⊆Canₖp ⊂s)
canₖ-plug (cif₁ x q ∷ C) p q₁ Canₖq⊆Canₖp ⊂s θ = codesub++both (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂s θ) (λ x y → y)
canₖ-plug (cif₂ x p ∷ C) p₁ q Canₖq⊆Canₖp ⊂s θ = codesub++both{a = Canₖ p θ} (λ x y → y) (canₖ-plug C p₁ q Canₖq⊆Canₖp ⊂s θ)
canₖ-plug (cenv θ₁ A ∷ C) p q Canₖq⊆Canₖp ⊂s θ = canθₖ-plug 0 (sig θ₁) C p q Canₖq⊆Canₖp ⊂s θ

canₛ-plug [] p q Canₛq⊆Canₛp Canₖq⊆Canₖp = Canₛq⊆Canₛp
canₛ-plug (ceval (epar₁ q) ∷ C) p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ = ∪¹-respect-⊆¹-left (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)
canₛ-plug (ceval (epar₂ p) ∷ C) p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = ∪¹-respect-⊆¹-right (Canₛ p θ) (canₛ-plug C p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)
canₛ-plug (ceval (eloopˢ q) ∷ C) p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ = canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ
canₛ-plug (ceval (eseq q) ∷ C) p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ with any (Code.nothin Code.≟_) (Canₖ (C ⟦ p ⟧c) θ) | any (Code.nothin Code.≟_) (Canₖ (C ⟦ q₁ ⟧c) θ)
... | yes 0∈CanC⟦p⟧ | yes 0∈CanC⟦q⟧ = ∪¹-respect-⊆¹-left (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)
... | yes 0∈CanC⟦p⟧ | no  0∉CanC⟦q⟧ = λ S x → (++ˡ (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ S x))
... | no  0∉CanC⟦p⟧ | yes 0∈CanC⟦q⟧ =  ⊥-elim (0∉CanC⟦p⟧ (canₖ-plug C p q₁ Canₖq⊆Canₖp Canₛq⊆Canₛp θ _ 0∈CanC⟦q⟧))
... | no  0∉CanC⟦p⟧ | no  0∉CanC⟦q⟧ = (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)

--  set-subtract-merge : ∀ {xs ys z} → z ∈ set-subtract xs ys → (z ∈ xs) × (z ∉ ys)

canₛ-plug (ceval (esuspend S) ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp = (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp)
canₛ-plug (ceval etrap ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp = (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp)
canₛ-plug (csignl (S ₛ) ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ S' S'∈CanC⟦q⟧
   = NSet.set-remove-not-removed ((¬ S ≡ S') ∋ NSet.set-remove-not-eq{S'}{S}{Canθₛ (sig ([S]-env (S ₛ))) 0 (C ⟦ q ⟧c) θ} S'∈CanC⟦q⟧)
                                  ((canθₛ-plug 0 (sig ([S]-env (S ₛ))) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ) S' ( (NSet.set-remove-mono-∈ S S'∈CanC⟦q⟧) ))

canₛ-plug (cpresent₁ S q ∷ C) p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ with Sig∈ S θ
... | no  S∉Domθ = ∪¹-respect-⊆¹-left (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)
... | yes S∈Domθ with (Signal.present ≟ₛₜ (sig-stats{S} θ S∈Domθ))
... | yes _ = (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)
... | no  _ with (Signal.absent ≟ₛₜ (sig-stats{S} θ S∈Domθ))
... | yes _ = λ k z → z
... | no  _ = ∪¹-respect-⊆¹-left (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)
canₛ-plug (cpresent₂ S p₁ ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ with Sig∈ S θ
... | no  S∉Domθ = ∪¹-respect-⊆¹-right (Canₛ p₁ θ) (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)
... | yes S∈Domθ with (Signal.present ≟ₛₜ (sig-stats{S} θ S∈Domθ))
... | yes _ = λ x y → y
... | no  _ with (Signal.absent ≟ₛₜ (sig-stats{S} θ S∈Domθ))
... | yes _ = (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)
... | no  _ = ∪¹-respect-⊆¹-right (Canₛ p₁ θ) (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)
canₛ-plug (cloop ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp = (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp)
canₛ-plug (cloopˢ₂ p ∷ C) p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = λ x z → z
canₛ-plug (cseq₂ p ∷ C) p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ with any (Code.nothin Code.≟_) (Canₖ p θ)
... | yes 0∈Canp = ∪¹-respect-⊆¹-right (Canₛ p θ) (canₛ-plug C p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)
... | no  0∉Canp = λ x y → y
canₛ-plug (cshared s e ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp = (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp)
canₛ-plug (cvar x e ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp = (canₛ-plug C p q Canₛq⊆Canₛp Canₖq⊆Canₖp)
canₛ-plug (cif₁ x q ∷ C) p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ = ∪¹-respect-⊆¹-left (canₛ-plug C p q₁ Canₛq⊆Canₛp Canₖq⊆Canₖp θ)
canₛ-plug (cif₂ x p ∷ C) p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ = ∪¹-respect-⊆¹-right (Canₛ p θ) (canₛ-plug C p₁ q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)
canₛ-plug (cenv θ₁ A ∷ C) p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ =   ⊆¹-respect-|¹ (fst $ Dom θ₁) (canθₛ-plug 0 (sig θ₁) C p q Canₛq⊆Canₛp Canₖq⊆Canₖp θ)

canₛₕ-plug [] p q Canₛₕq⊆Canₛₕp Canₖₕq⊆Canₖₕp ⊂S = Canₛₕq⊆Canₛₕp
canₛₕ-plug (ceval (epar₁ q) ∷ C) p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = ∪¹-respect-⊆¹-left (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)
canₛₕ-plug (ceval (epar₂ p) ∷ C) p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = ∪¹-respect-⊆¹-right (Canₛₕ p θ) (canₛₕ-plug C p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)
canₛₕ-plug (ceval (eloopˢ q) ∷ C) p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ
canₛₕ-plug (ceval (eseq q) ∷ C) p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ with any (Code.nothin Code.≟_) (Canₖ (C ⟦ p ⟧c) θ) | any (Code.nothin Code.≟_) (Canₖ (C ⟦ q₁ ⟧c) θ)
... | yes 0∈CanC⟦p⟧ | yes 0∈CanC⟦q⟧ = ∪¹-respect-⊆¹-left (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)
... | yes 0∈CanC⟦p⟧ | no  0∉CanC⟦q⟧ = λ S x → (++ˡ (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ S x))
... | no  0∉CanC⟦p⟧ | yes 0∈CanC⟦q⟧ =  ⊥-elim (0∉CanC⟦p⟧ (canₖ-plug C p q₁ Canₖq⊆Canₖp ⊂S θ _ 0∈CanC⟦q⟧))
... | no  0∉CanC⟦p⟧ | no  0∉CanC⟦q⟧ = (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)

canₛₕ-plug (ceval (esuspend S) ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S = (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S)
canₛₕ-plug (ceval etrap ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S = (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S)
canₛₕ-plug (csignl S ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = canθₛₕ-plug 0 (sig ([S]-env S)) C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ
canₛₕ-plug (cpresent₁ S q ∷ C) p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ with Sig∈ S θ
... | no  S∉Domθ = ∪¹-respect-⊆¹-left (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)
... | yes S∈Domθ with (Signal.present ≟ₛₜ (sig-stats{S} θ S∈Domθ))
... | yes _ = (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)
... | no  _ with (Signal.absent ≟ₛₜ (sig-stats{S} θ S∈Domθ))
... | yes _ = λ k z → z
... | no  _ = ∪¹-respect-⊆¹-left (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)
canₛₕ-plug (cpresent₂ S p₁ ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ with Sig∈ S θ
... | no  S∉Domθ = ∪¹-respect-⊆¹-right (Canₛₕ p₁ θ) (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)
... | yes S∈Domθ with (Signal.present ≟ₛₜ (sig-stats{S} θ S∈Domθ))
... | yes _ = λ x y → y
... | no  _ with (Signal.absent ≟ₛₜ (sig-stats{S} θ S∈Domθ))
... | yes _ = (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)
... | no  _ = ∪¹-respect-⊆¹-right (Canₛₕ p₁ θ) (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)
canₛₕ-plug (cloop ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S = (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S)
canₛₕ-plug (cloopˢ₂ p ∷ C) p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = λ x z → z
canₛₕ-plug (cseq₂ p ∷ C) p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ with any (Code.nothin Code.≟_) (Canₖ p θ)
... | yes 0∈Canp = ∪¹-respect-⊆¹-right (Canₛₕ p θ) (canₛₕ-plug C p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)
... | no  0∉Canp = λ x y → y
canₛₕ-plug (cshared (s ₛₕ) e ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ s' s'∈CanC⟦q⟧
   = NSet.set-remove-not-removed ((¬ s ≡ s') ∋ NSet.set-remove-not-eq{s'}{s}{Canₛₕ (C ⟦ q ⟧c) θ} s'∈CanC⟦q⟧) (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ s' (NSet.set-remove-mono-∈ s s'∈CanC⟦q⟧))
canₛₕ-plug (cvar x e ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S = (canₛₕ-plug C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S)
canₛₕ-plug (cif₁ x q ∷ C) p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = ∪¹-respect-⊆¹-left (canₛₕ-plug C p q₁ Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)
canₛₕ-plug (cif₂ x p ∷ C) p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ = ∪¹-respect-⊆¹-right (Canₛₕ p θ) (canₛₕ-plug C p₁ q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)
canₛₕ-plug (cenv θ₁ A ∷ C) p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ =  ⊆¹-respect-|¹ (snd $ Dom θ₁) (canθₛₕ-plug 0 (sig θ₁) C p q Canₛₕq⊆Canₛₕp Canₖq⊆Canₖp ⊂S θ)

canθₖ-plugE : ∀ S' sigs → ∀ E p q
              → (Canₖq⊆Canₖp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))
              → (Canₛq⊆Canₛp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))
              → (∀ θ k → k ∈ (Canθₖ sigs S' (E ⟦ q ⟧e) θ) → k ∈ (Canθₖ sigs S' (E ⟦ p ⟧e) θ))
canθₖ-plugE S' sigs E p q
  with canθₖ-plug S' sigs (Data.List.map ceval E) p q
... | r rewrite unplugc (⟦⟧e-to-⟦⟧c (Erefl{E}{q}))
              | unplugc (⟦⟧e-to-⟦⟧c (Erefl{E}{p}))
  = r

canθₛ-plugE : ∀ S' sigs → ∀ E p q
              → (Canₛq⊆Canₛp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))
              → (Canₖq⊆Canₖp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))
              → (∀ θ k → k ∈ (Canθₛ sigs S' (E ⟦ q ⟧e) θ) → k ∈ (Canθₛ sigs S' (E ⟦ p ⟧e) θ))
canθₛ-plugE S' sigs E p q
  with canθₛ-plug S' sigs (Data.List.map ceval E) p q
... | r rewrite unplugc (⟦⟧e-to-⟦⟧c (Erefl{E}{q}))
              | unplugc (⟦⟧e-to-⟦⟧c (Erefl{E}{p}))
  = r

canθₛₕ-plugE : ∀ S' sigs → ∀ E p q
              → (Canₛₕq⊆Canₛₕp : ∀ θ → (Canₛₕ q θ) ⊆¹ (Canₛₕ p θ))
              → (Canₛq⊆Canₛp : ∀ θ k → k ∈ (Canₖ q θ) → k ∈ (Canₖ p θ))
              → (Canₖq⊆Canₖp : ∀ θ S → S ∈ (Canₛ q θ) → S ∈ (Canₛ p θ))
              → (∀ θ k → k ∈ (Canθₛₕ sigs S' (E ⟦ q ⟧e) θ) → k ∈ (Canθₛₕ sigs S' (E ⟦ p ⟧e) θ))
canθₛₕ-plugE S' sigs E p q
  with canθₛₕ-plug S' sigs (Data.List.map ceval E) p q
... | r rewrite unplugc (⟦⟧e-to-⟦⟧c (Erefl{E}{q}))
              | unplugc (⟦⟧e-to-⟦⟧c (Erefl{E}{p}))
  = r

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text: open import Issue4959-2

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
-- Andreas, bug found 2011-12-31

{-# OPTIONS --irrelevant-projections #-}

module Issue543a where

open import Common.Equality

data   ⊥ : Set where
record ⊤ : Set where
  constructor tt

data Bool : Set where
  true false : Bool

record Squash (A : Set) : Set where
  constructor squash
  field
    .unsquash : A
open Squash

-- ok:
sqT≡sqF : squash true ≡ squash false
sqT≡sqF = refl

record Inhabited : Set1 where
  constructor inhabited
  field
    Type : Set
    elem : Type
open Inhabited

.bad1 : Inhabited
bad1 = inhabited (true ≡ unsquash (squash true)) refl

.bad2 : Inhabited
bad2 = inhabited (unsquash (squash false) ≡ false) refl

infixl 2 _∘_
_∘_ = trans

-- this should not be provable!!
.irrT≡F : true ≡ false
irrT≡F = elem bad1 ∘ cong unsquash sqT≡sqF ∘ elem bad2

-- the rest is easy

T : Bool → Set
T true  = ⊤
T false = ⊥

T≠F : true ≡ false → ⊥
T≠F p = subst T p tt

.irr⊥ : ⊥
irr⊥ = T≠F irrT≡F

rel⊥ : .⊥ → ⊥
rel⊥ ()

absurd : ⊥
absurd = rel⊥ irr⊥


text:
{-# OPTIONS --exact-split -v tc.cover.cover:100 #-}

open import Common.Bool
open import Common.Equality

record Unit : Set where
  eta-equality
  constructor unit

f : Unit → Bool → Bool
f unit true  = true
f u    false = false  -- passes without --exact-split

-- All equations pass do hold definitionally:

test-1 : f unit true ≡ true
test-1 = refl

test-2 : ∀{u : Unit} → f u false ≡ false
test-2 = refl

-- Error:
-- Exact splitting is enabled, but not all clauses can be preserved as
-- definitional equalities in the translation to a case tree
-- when checking the definition of f

-- Should succeed.

max_forks_repo_name: Agda-zh/agda


text:
open import Common.IO
open import Common.Unit
open import Common.String
open import Common.Nat

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream public

repeat : ∀ {A} → A → Stream A
head (repeat x) = x
tail (repeat x) = repeat x

lookup : ∀ {A} → Stream A → Nat → A
lookup xs zero = xs .head
lookup xs (suc n) = lookup (xs .tail) n

main : IO Unit
main = putStr (lookup (repeat "hello") 1000000)

max_stars_repo_name: xekoukou/agda-ocaml

max_issues_repo_name: xekoukou/agda-ocaml

max_forks_repo_name: xekoukou/agda-ocaml


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A different interface to the Kleene lists, designed to mimic
-- Data.List.
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.List.Kleene.AsList where

open import Level as Level using (Level)

private
  variable
    a b c : Level
    A : Set a
    B : Set b
    C : Set c

import Data.List.Kleene.Base as Kleene

------------------------------------------------------------------------
-- Here we import half of the functions from Data.KleeneList: the half
-- for possibly-empty lists.

open import Data.List.Kleene.Base public
  using ([])
  renaming
    ( _*                 to List
    ; foldr*             to foldr
    ; foldl*             to foldl
    ; _++*_              to _++_
    ; map*               to map
    ; mapMaybe*          to mapMaybe
    ; pure*              to pure
    ; _<*>*_             to _<*>_
    ; _>>=*_             to _>>=_
    ; mapAccumˡ*         to mapAccumˡ
    ; mapAccumʳ*         to mapAccumʳ
    ; _[_]*              to _[_]
    ; applyUpTo*         to applyUpTo
    ; upTo*              to upTo
    ; zipWith*           to zipWith
    ; unzipWith*         to unzipWith
    ; partitionSumsWith* to partitionSumsWith
    ; reverse*           to reverse
    )

------------------------------------------------------------------------
-- A pattern which mimics Data.List._∷_

infixr 5 _∷_
pattern _∷_ x xs = Kleene.∹ x Kleene.& xs

------------------------------------------------------------------------
-- The following functions change the type of the list (from ⁺ to * or vice
-- versa) in Data.KleeneList, so we reimplement them here to keep the
-- type the same.

scanr : (A → B → B) → B → List A → List B
scanr f b xs = Kleene.∹ Kleene.scanr* f b xs

scanl : (B → A → B) → B → List A → List B
scanl f b xs = Kleene.∹ Kleene.scanl* f b xs

tails : List A → List (List A)
tails xs = foldr (λ x xs → (Kleene.∹ x) ∷ xs) ([] ∷ []) (Kleene.tails* xs)


text:
module Nat where

open import Function hiding (_∘_; id)
open import Level

open import Basic
open import Category
import Functor
open Category.Category
open Functor.Functor

record Nat {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} (F G : Functor.Functor C D) : Set (suc (C₀ ⊔ C₁ ⊔ ℓ ⊔ D₀ ⊔ D₁ ⊔ ℓ′)) where
  field
    component : (X : Obj C) → Hom D (fobj F X) (fobj G X)

  field
    naturality : {a b : Obj C} {f : Hom C a b}
      → D [ D [ component b ∘ fmap F f ] ≈ D [ fmap G f ∘ component a ] ]

open Nat

identity : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} → (F : Functor.Functor C D) → Nat F F
identity {D = D} F = record {
  component = λ X → id D ;
  naturality = λ {a} {b} {f} → trans-hom D (leftId D) (sym-hom D (rightId D)) }

compose : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} → {F G H : Functor.Functor C D} → Nat G H → Nat F G → Nat F H
compose {C = C} {D} {F} {G} {H} η ε  = record {
  component = λ X → D [ component η X ∘ component ε X ] ;
  naturality = λ {a} {b} {f} → (begin⟨ D ⟩
    D [ (D [ component η b ∘ component ε b ]) ∘ fmap F f ] ≈⟨ assoc D ⟩
    D [ component η b ∘ (D [ component ε b ∘ fmap F f ]) ] ≈⟨ ≈-composite D (refl-hom D) (naturality ε) ⟩
    D [ component η b ∘ (D [ fmap G f ∘ component ε a ]) ] ≈⟨ sym-hom D (assoc D) ⟩
    D [ (D [ component η b ∘ fmap G f ]) ∘ component ε a ] ≈⟨ ≈-composite D (naturality η) (refl-hom D) ⟩
    D [ (D [ fmap H f ∘ component η a ]) ∘ component ε a ] ≈⟨ assoc D ⟩
    D [ fmap H f ∘ (D [ component η a ∘ component ε a ]) ] ∎) }

composeNF : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′ E₀ E₁ ℓ″} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {E : Category E₀ E₁ ℓ″} {A B : Functor.Functor D E} → Nat A B → (F : Functor.Functor C D) → Nat (Functor.compose A F) (Functor.compose B F)
composeNF {C = C} {D} {E} {A} {B} η F = record {
  component = λ X → component η (fobj F X) ;
  naturality = λ {a} {b} {f} → naturality η }

composeFN : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′ E₀ E₁ ℓ″} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {E : Category E₀ E₁ ℓ″} {A B : Functor.Functor C D} (F : Functor.Functor D E) → Nat A B → Nat (Functor.compose F A) (Functor.compose F B)
composeFN {C = C} {D} {E} {A} {B} F η = record {
  component = λ X → fmap F (component η X) ;
  naturality = λ {a} {b} {f} → begin⟨ E ⟩
    E [ fmap F (component η b) ∘ fmap (Functor.compose F A) f ] ≈⟨ sym-hom E (preserveComp F) ⟩
    fmap F (D [ component η b ∘ fmap A f ]) ≈⟨ Functor.preserveEq F (naturality η) ⟩
    fmap F (D [ fmap B f ∘ component η a ]) ≈⟨ preserveComp F ⟩
    E [ fmap (Functor.compose F B) f ∘ fmap F (component η a) ]
    ∎ }

equality : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F G : Functor.Functor C D} → (η τ : Nat F G) → Set _
equality {C = C} {D} η τ = ∀ {a : Obj C} → D [ component η a ≈ component τ a ]

subst : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F G : Functor.Functor C D} {η τ : Nat F G} → (a : Obj C) → equality η τ → D [ component η a ≈ component τ a ]
subst a eq = eq {a}

HomFunctor : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) (X : Obj C) → Functor.Functor C Setoids
HomFunctor C X = record {
  fobj = λ x → (Homsetoid C X x) ;
  fmapsetoid = record {
    mapping = λ x → record { mapping = λ x₁ → C [ x ∘ x₁ ] ; preserveEq = ≈-composite C (refl-hom C) } ;
    preserveEq = λ x₁ x₂ → ≈-composite C x₁ (refl-hom C) } ;
  preserveId = λ x → leftId C ;
  preserveComp = λ x → assoc C }

HomNat : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) {A B : Obj C} (f : Hom C A B) → Nat (HomFunctor C B) (HomFunctor C A)
HomNat C {A} {B} f = record {
  component = component-map ;
  naturality = λ {a} {b} {x} → λ x₁ → begin⟨ C ⟩
    Map.mapping (Setoids [ component-map b ∘ fmap (HomFunctor C B) x ]) x₁ ≈⟨ refl-hom C ⟩
    C [ C [ x ∘ x₁ ] ∘ f ] ≈⟨ assoc C ⟩
    C [ x ∘ C [ x₁ ∘ f ] ] ≈⟨ refl-hom C ⟩
    Map.mapping (Setoids [ fmap (HomFunctor C A) x ∘ component-map a ]) x₁
  ∎ }
  where
    component-map = λ X → record {
      mapping = λ x → C [ x ∘ f ] ;
      preserveEq = λ x₁ → ≈-composite C x₁ (refl-hom C) }

HomFunctorOp : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) (X : Obj C) → Functor.Functor (op C) Setoids
HomFunctorOp C X = record {
  fobj = λ x → (Homsetoid C x X) ;
  fmapsetoid = record {
    mapping = λ x → record { mapping = λ x₁ → C [ x₁ ∘ x ] ; preserveEq = ≈-composite (op C) (refl-hom C) } ;
    preserveEq = λ x₁ x₂ → ≈-composite (op C) x₁ (refl-hom C) } ;
  preserveId = λ x → leftId (op C) ;
  preserveComp = λ x → assoc (op C) }

HomNatOp : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) {A B : Obj C} (f : Hom C A B) → Nat (HomFunctorOp C A) (HomFunctorOp C B)
HomNatOp C {A} {B} f = record {
  component = component-map ;
  naturality = λ {a} {b} {x} → λ x₁ → begin⟨ C ⟩
    Map.mapping (Setoids [ component-map b ∘ fmap (HomFunctorOp C A) x ]) x₁ ≈⟨ refl-hom C ⟩
    C [ f ∘ C [ x₁ ∘ x ] ] ≈⟨ sym-hom C (assoc C) ⟩
    C [ C [ f ∘ x₁ ] ∘ x ] ≈⟨ refl-hom C ⟩
    Map.mapping (Setoids [ fmap (HomFunctorOp C B) x ∘ component-map a ]) x₁
  ∎ }
  where
    component-map = λ X → record {
      mapping = λ x → C [ f ∘ x ] ;
      preserveEq = λ x₁ → ≈-composite C (refl-hom C) x₁ }

FunCat : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} → (Category C₀ C₁ ℓ) → (Category D₀ D₁ ℓ′) → Category _ _ _
FunCat C D = record {
  Obj = Functor.Functor C D;
  Homsetoid = λ F G → record { Carrier = Nat F G ; _≈_ = equality ; isEquivalence = record {
    refl = λ {x} {a} → refl-hom D ;
    sym = λ x → λ {a} → sym-hom D x ;
    trans = λ x x₁ → λ {a} → trans-hom D x x₁ } };
  comp = compose;
  id = λ {A} → identity A;
  leftId = λ {A} {B} {f} {a} → leftId D;
  rightId = λ {A} {B} {f} {a} → rightId D;
  assoc = λ {A} {B} {C₁} {D₁} {f} {g} {h} {a} → assoc D;
  ≈-composite = λ x x₁ → ≈-composite D x x₁
  }

assocNat→ : ∀{B₀ B₁ ℓ‴ C₀ C₁ ℓ D₀ D₁ ℓ′ E₀ E₁ ℓ″} {B : Category B₀ B₁ ℓ‴} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {E : Category E₀ E₁ ℓ″} {F : Functor.Functor B C} {G : Functor.Functor C D} {H : Functor.Functor D E} → Nat (Functor.compose (Functor.compose H G) F) (Functor.compose H (Functor.compose G F))
assocNat→ {C = C} {D} {E} {F} = record {
  component = λ X → id E ;
  naturality = λ {a} {b} {f} → trans-hom E (leftId E) (sym-hom E (rightId E)) }

assocNat← : ∀{B₀ B₁ ℓ‴ C₀ C₁ ℓ D₀ D₁ ℓ′ E₀ E₁ ℓ″} {B : Category B₀ B₁ ℓ‴} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {E : Category E₀ E₁ ℓ″} {F : Functor.Functor B C} {G : Functor.Functor C D} {H : Functor.Functor D E} → Nat (Functor.compose H (Functor.compose G F)) (Functor.compose (Functor.compose H G) F)
assocNat← {C = C} {D} {E} {F} = record {
  component = λ X → id E ;
  naturality = λ {a} {b} {f} → trans-hom E (leftId E) (sym-hom E (rightId E)) }

leftIdNat→ : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} → Nat (Functor.compose (Functor.identity D) F) F
leftIdNat→ {C = C} {D} {F} = record {
  component = λ X → id D ;
  naturality = λ {a} {b} {f} → trans-hom D (leftId D) (sym-hom D (rightId D)) }

leftIdNat← : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} → Nat F (Functor.compose (Functor.identity D) F)
leftIdNat← {C = C} {D} {F} = record {
  component = λ X → id D ;
  naturality = λ {a} {b} {f} → trans-hom D (leftId D) (sym-hom D (rightId D)) }

rightIdNat→ : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} → Nat (Functor.compose F (Functor.identity C)) F
rightIdNat→ {C = C} {D} {F} = record {
  component = λ X → id D ;
  naturality = λ {a} {b} {f} → trans-hom D (leftId D) (sym-hom D (rightId D)) }

rightIdNat← : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} → Nat F (Functor.compose F (Functor.identity C))
rightIdNat← {C = C} {D} {F} = record {
  component = λ X → id D ;
  naturality = λ {a} {b} {f} → trans-hom D (leftId D) (sym-hom D (rightId D)) }

module Export where
  infixl 6 _F∘N_ _N∘F_
  _F∘N_ = composeFN
  _N∘F_ = composeNF

  Hom[_][_,-] = HomFunctor
  Hom[_][-,_] = HomFunctorOp
  HomNat[_][_,-] = HomNat
  HomNat[_][-,_] = HomNatOp

  [_,_] : ∀{C₀ C₁ ℓ D₀ D₁ ℓ′} (C : Category C₀ C₁ ℓ) → (D : Category D₀ D₁ ℓ′) → Category _ _ _
  [_,_] = FunCat

  PSh[_] : ∀{C₀ C₁ ℓ} (C : Category C₀ C₁ ℓ) → Category _ _ _
  PSh[_] {_} {C₁} {ℓ} C = [ op C , Setoids {C₁} {ℓ} ]

max_stars_repo_name: myuon/agda-cate

max_issues_repo_name: myuon/agda-cate

max_forks_repo_name: myuon/agda-cate


text:
-- Andreas, 2016-07-28, issue #1720

record Foo (A : Set) : Set where
  a : A
  a = {!!} where
    a' : A
    a' = {!!}

  field
    f : A

-- Now: better error:

-- This declaration is illegal in a record before the last field
-- when scope checking the declaration
--   record Foo A where
--     mutual
--       a : A
--       a = ?
--         where
--           a' : A
--           a' = ?
--     field f : A

-- Ideally: should pass

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K --safe #-}

open import Categories.Category.Monoidal.Structure using (MonoidalCategory)

module Categories.Category.Construction.MonoidalFunctors {o ℓ e o′ ℓ′ e′}
  (C : MonoidalCategory o ℓ e) (D : MonoidalCategory o′ ℓ′ e′) where

-- The functor category for a given pair of monoidal categories

open import Level
open import Data.Product using (_,_)
open import Relation.Binary.Construct.On using (isEquivalence)
open import Categories.Category using (Category)
open import Categories.Category.Monoidal
open import Categories.Functor.Monoidal
import Categories.NaturalTransformation.Monoidal as NT
open import Categories.NaturalTransformation.Equivalence
  using (_≃_; ≃-isEquivalence)

open MonoidalCategory D

module Lax where

  MonoidalFunctors : Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′)
                              (o ⊔ e′)
  MonoidalFunctors = record
    { Obj = MonoidalFunctor C D
    ; _⇒_ = MonoidalNaturalTransformation
    ; _≈_ = λ α β → U α ≃ U β
    ; id  = idNT
    ; _∘_ = _∘ᵥ_
    ; assoc     = assoc
    ; sym-assoc = sym-assoc
    ; identityˡ = identityˡ
    ; identityʳ = identityʳ
    ; identity² = identity²
    ; equiv     = isEquivalence U ≃-isEquivalence
    ; ∘-resp-≈  = λ α₁≈β₁ α₂≈β₂ → ∘-resp-≈ α₁≈β₁ α₂≈β₂
    }
    where
      open NT.Lax renaming (id to idNT)
      open MonoidalNaturalTransformation using (U)

module Strong where

  MonoidalFunctors : Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′)
                              (o ⊔ e′)
  MonoidalFunctors = record
    { Obj = StrongMonoidalFunctor C D
    ; _⇒_ = MonoidalNaturalTransformation
    ; _≈_ = λ α β → U α ≃ U β
    ; id  = idNT
    ; _∘_ = _∘ᵥ_
    ; assoc     = assoc
    ; sym-assoc = sym-assoc
    ; identityˡ = identityˡ
    ; identityʳ = identityʳ
    ; identity² = identity²
    ; equiv     = isEquivalence U ≃-isEquivalence
    ; ∘-resp-≈  = λ α₁≈β₁ α₂≈β₂ → ∘-resp-≈ α₁≈β₁ α₂≈β₂
    }
    where
      open NT.Strong renaming (id to idNT)
      open MonoidalNaturalTransformation using (U)

max_stars_repo_name: TOTBWF/agda-categories

max_issues_repo_name: TOTBWF/agda-categories

max_forks_repo_name: TOTBWF/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Homomorphism proofs for constants over polynomials
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Tactic.RingSolver.Core.Polynomial.Parameters

module Tactic.RingSolver.Core.Polynomial.Homomorphism.Constants
  {r₁ r₂ r₃ r₄}
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where

open Homomorphism homo

open import Data.Vec.Base using (Vec)

open import Tactic.RingSolver.Core.Polynomial.Base (Homomorphism.from homo)
open import Tactic.RingSolver.Core.Polynomial.Semantics homo

κ-hom : ∀ {n} (x : Raw.Carrier) (Ρ : Vec Carrier n) → ⟦ κ x ⟧ Ρ ≈ ⟦ x ⟧ᵣ
κ-hom x _ = refl


text:
module PublicWithoutOpen where

module A where

module B = A public


text:
------------------------------------------------------------------------------
-- Alter: An unguarded co-recursive function
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.FOTC.UnguardedCorecursion.Alter.AlterSL where

open import Codata.Musical.Notation
open import Codata.Musical.Stream
open import Data.Bool.Base

------------------------------------------------------------------------------

-- TODO (2019-01-04): Agda doesn't accept this definition which was
-- accepted by a previous version.
{-# TERMINATING #-}
alter : Stream Bool
alter = true ∷ ♯ (false ∷ ♯ alter)

{-# TERMINATING #-}
alter' : Stream Bool
alter' = true ∷ ♯ (map not alter')

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Tactic.Reflection.Telescope where

open import Prelude hiding (abs)
open import Builtin.Reflection
open import Tactic.Reflection.DeBruijn

Telescope = List (String × Arg Type)

telView : Type → Telescope × Type
telView (pi a (abs x b)) = first (_∷_ (x , a)) (telView b)
telView a                = [] , a

visibleArity : Type → Nat
visibleArity = length ∘ filter (isVisible ∘ snd) ∘ fst ∘ telView

telPi : Telescope → Type → Type
telPi tel b = foldr (λ (x , a) b → pi a (abs x b)) b tel

arity : Name → TC Nat
arity f = length ∘ fst ∘ telView <$> getType f

argTel : Name → TC Telescope
argTel f = fst ∘ telView <$> getType f

telePat : Telescope → List (Arg Pattern)
telePat tel = zipWith (λ x (_ , a) → var x <$ a) (reverse $ from 0 for n) tel
  where n = length tel

private
  teleArgs′ : Nat → List (Arg Type) → List (Arg Term)
  teleArgs′ (suc n) (a ∷ Γ) = (var n [] <$ a) ∷ teleArgs′ n Γ
  teleArgs′ _ _ = []

teleArgs : Telescope → List (Arg Term)
teleArgs Γ = teleArgs′ (length Γ) (map snd Γ)

conParams : Name → TC Nat
conParams c =
  caseM getDefinition c of λ
  { (data-cons d) → getParameters d
  ; _             → pure 0 }

conPat : Name → TC Pattern
conPat c = do
  np ← conParams c
  con c ∘ telePat ∘ drop np <$> argTel c

conTerm : Name → TC Term
conTerm c = do
  np ← conParams c
  con c ∘ teleArgs ∘ drop np <$> argTel c

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
-- The ATP pragma with the role <prove> can be used with postulates.

module ATPConjecture where

postulate
  D   : Set
  _≡_ : D → D → Set

postulate
  sym : ∀ {m n} → m ≡ n → n ≡ m
{-# ATP prove sym #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category
open import Categories.Functor hiding (id)

-- Cone over a Functor F (from shape category J into category C)

module Categories.Diagram.Cone
  {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) where

open Category C
open Functor F

open import Level

record Apex (N : Obj) : Set (ℓ′ ⊔ o′ ⊔ e ⊔ ℓ) where
  field
    ψ       : (X : Category.Obj J) → (N ⇒ F₀ X)
    commute : ∀ {X Y} (f : J [ X , Y ]) → F₁ f ∘ ψ X ≈ ψ Y

record Cone : Set (o ⊔ ℓ′ ⊔ o′ ⊔ e ⊔ ℓ) where
  field
    {N}  : Obj
    apex : Apex N

  open Apex apex public

open Apex
open Cone

record Cone⇒ (c c′ : Cone) : Set (ℓ ⊔ e ⊔ o′) where
  field
    arr     : N c ⇒ N c′
    commute : ∀ {X} → ψ c′ X ∘ arr ≈ ψ c X

open Cone⇒

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Luau.Value where

open import Agda.Builtin.Float using (Float)
open import Luau.Addr using (Addr)
open import Luau.Syntax using (Block; Expr; nil; addr; number)
open import Luau.Var using (Var)

data Value : Set where
  nil : Value
  addr : Addr → Value
  number : Float → Value

val : ∀ {a} → Value → Expr a
val nil = nil
val (addr a) = addr a
val (number x) = number x


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to All
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Vec.Functional.Relation.Unary.All.Properties where

open import Data.Fin.Base
open import Data.Fin.Properties
open import Data.Nat.Base
open import Data.Product as Σ using (_×_; _,_; proj₁; proj₂; uncurry)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Vec.Functional as VF hiding (map)
open import Data.Vec.Functional.Relation.Unary.All
open import Function
open import Level using (Level)
open import Relation.Unary

private
  variable
    a b c p q r ℓ : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- map

module _ {P : Pred A p} {Q : Pred B q} {f : A → B} where

  map⁺ :  (∀ {x} → P x → Q (f x)) →
          ∀ {n xs} → All P {n = n} xs → All Q (VF.map f xs)
  map⁺ pq ps i = pq (ps i)

------------------------------------------------------------------------
-- replicate

module _ {P : Pred A p} {x : A} {n : ℕ} where

  replicate⁺ : P x → All P (replicate {n = n} x)
  replicate⁺ = const

------------------------------------------------------------------------
-- _⊛_

module _ {P : Pred A p} {Q : Pred B q} where

  ⊛⁺ : ∀ {n} {fs : Vector (A → B) n} {xs} →
       All (λ f → ∀ {x} → P x → Q (f x)) fs → All P xs → All Q (fs ⊛ xs)
  ⊛⁺ pqs ps i = (pqs i) (ps i)

------------------------------------------------------------------------
-- zipWith

module _ {P : Pred A p} {Q : Pred B q} {R : Pred C r} where

  zipWith⁺ : ∀ {f} → (∀ {x y} → P x → Q y → R (f x y)) → ∀ {n xs ys} →
             All P xs → All Q ys → All R (zipWith f {n = n} xs ys)
  zipWith⁺ pqr ps qs i = pqr (ps i) (qs i)

------------------------------------------------------------------------
-- zip

module _ {P : Pred A p} {Q : Pred B q} {n} {xs : Vector A n} {ys} where

  zip⁺ : All P xs → All Q ys → All (P ⟨×⟩ Q) (zip xs ys)
  zip⁺ ps qs i = ps i , qs i

  zip⁻ : All (P ⟨×⟩ Q) (zip xs ys) → All P xs × All Q ys
  zip⁻ pqs = proj₁ ∘ pqs , proj₂ ∘ pqs

------------------------------------------------------------------------
-- head

head⁺ : ∀ (P : Pred A p) {n v} → All P v → P (head {n = n} v)
head⁺ P ps = ps zero

------------------------------------------------------------------------
-- tail

tail⁺ : ∀ (P : Pred A p) {n v} → All P v → All P (tail {n = n} v)
tail⁺ P ps = ps ∘ suc

------------------------------------------------------------------------
-- ++

module _ (P : Pred A p) {m n : ℕ} {xs : Vector A m} {ys : Vector A n} where

  ++⁺ : All P xs → All P ys → All P (xs ++ ys)
  ++⁺ pxs pys i with splitAt m i
  ... | inj₁ i′ = pxs i′
  ... | inj₂ j′ = pys j′

module _ (P : Pred A p) {m n : ℕ} (xs : Vector A m) {ys : Vector A n} where

  ++⁻ˡ : All P (xs ++ ys) → All P xs
  ++⁻ˡ ps i with ps (inject+ n i)
  ... | p rewrite splitAt-inject+ m n i = p

  ++⁻ʳ : All P (xs ++ ys) → All P ys
  ++⁻ʳ ps i with ps (raise m i)
  ... | p rewrite splitAt-raise m n i = p

  ++⁻ : All P (xs ++ ys) → All P xs × All P ys
  ++⁻ ps = ++⁻ˡ ps , ++⁻ʳ ps


text:
module Structure.Category.Functor.Category where

open import Data.Tuple
open import Function.Equals
import      Lvl
open import Logic
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Category
open import Structure.Category.Functor
open import Structure.Category.NaturalTransformation
open import Structure.Category.NaturalTransformation.Equiv
open import Structure.Category.NaturalTransformation.NaturalTransformations
open import Structure.Categorical.Properties
open import Structure.Operator
open import Syntax.Transitivity
open import Type

module _
  {ℓₗₒ ℓₗₘ ℓₗₑ ℓᵣₒ ℓᵣₘ ℓᵣₑ}
  {catₗ : CategoryObject{ℓₗₒ}{ℓₗₘ}{ℓₗₑ}}
  {catᵣ : CategoryObject{ℓᵣₒ}{ℓᵣₘ}{ℓᵣₑ}}
  where

  open Category ⦃ … ⦄
  open Wrapped

  private open module MorphismEquivₗ {x}{y} = Equiv(CategoryObject.morphism-equiv catₗ {x}{y}) using ()
  private open module MorphismEquivᵣ {x}{y} = Equiv(CategoryObject.morphism-equiv catᵣ {x}{y}) using ()
  private instance _ = CategoryObject.category-instance catₗ
  private instance _ = CategoryObject.category-instance catᵣ

  -- Natural transformations are morphisms on functors.
  functorCategory : Category{Obj = catₗ →ᶠᵘⁿᶜᵗᵒʳ catᵣ} (_→ᴺᵀ_)
  Category._∘_ functorCategory = _∘ᴺᵀ_
  Category.id  functorCategory = idᴺᵀ
  Dependent._⊜_.proof (BinaryOperator.congruence (Category.binaryOperator functorCategory) (Dependent.intro xy1) (Dependent.intro xy2)) = congruence₂(_∘_) xy1 xy2
  Dependent._⊜_.proof (Morphism.Associativity.proof (Category.associativity functorCategory)) = Morphism.associativity(_∘_)
  Dependent._⊜_.proof (Morphism.Identityₗ.proof (left (Category.identity functorCategory)) {F₁} {F₂} {ηᴺᵀ}) {x} =
    ∃.witness (idᴺᵀ ∘ᴺᵀ ηᴺᵀ)(x)                   🝖[ _≡_ ]-[]
    ∃.witness(idᴺᵀ{F = F₂})(x) ∘ ∃.witness ηᴺᵀ(x) 🝖[ _≡_ ]-[]
    id ∘ ∃.witness ηᴺᵀ(x)                         🝖[ _≡_ ]-[ Morphism.identityₗ(_∘_)(id) ]
    ∃.witness ηᴺᵀ(x)                              🝖-end
  Dependent._⊜_.proof (Morphism.Identityᵣ.proof (right (Category.identity functorCategory)) {F₁} {F₂} {ηᴺᵀ}) {x} =
    ∃.witness (ηᴺᵀ ∘ᴺᵀ idᴺᵀ)(x)                   🝖[ _≡_ ]-[]
    ∃.witness ηᴺᵀ(x) ∘ ∃.witness(idᴺᵀ{F = F₁})(x) 🝖[ _≡_ ]-[]
    ∃.witness ηᴺᵀ(x) ∘ id                         🝖[ _≡_ ]-[ Morphism.identityᵣ(_∘_)(id) ]
    ∃.witness ηᴺᵀ(x)                              🝖-end

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Avionics.Maybe where

open import Function using (_∘_)
open import Level using (Level)

private
  variable
    a b c : Level
    A : Set a
    B : Set b
    C : Set c

data Maybe (A : Set a) : Set a where
  nothing : Maybe A
  just    : (x : A) → Maybe A

maybe : ∀ {A : Set a} {B : Maybe A → Set b} →
        ((x : A) → B (just x)) → B nothing → (x : Maybe A) → B x
maybe j n (just x) = j x
maybe j n nothing  = n

map : (A → B) → Maybe A → Maybe B
map f = maybe (just ∘ f) nothing

-- Monad: bind

infixl 1 _>>=_
_>>=_ : Maybe A → (A → Maybe B) → Maybe B
nothing >>= f = nothing
just a  >>= f = f a

{-# FOREIGN GHC type AgdaMaybe erase = Maybe #-}
{-# COMPILE GHC Maybe = data AgdaMaybe (Nothing | Just) #-}


text:
{-

Part 3: Transport and composition

- Cubical transport
- Subst as a special case of cubical transport
- Path induction from subst?
- Homogeneous composition (hcomp)
- Binary composition of paths as special case of hcomp

-}

{-# OPTIONS --cubical #-}
module Part2 where

open import Part1 public

-- Transport is more complex as ≡ isn't inductively defined (so we
-- can't define it by pattern-matching on p)
transport : {A B : Type ℓ} → A ≡ B → A → B
transport p a = transp (λ i → p i) i0 a

-- This lets us define subst (which is called "transport" in the HoTT book)
subst : {A : Type ℓ} (P : A → Type ℓ') {x y : A} (p : x ≡ y) → P x → P y
subst P p pa = transport (λ i → P (p i)) pa

-- The transp operation reduces differently for different types
-- formers. For paths it reduces to another primitive operation called
-- hcomp.

-- We can also define the J eliminator (aka path induction)
-- TODO: rewrite using subst?
-- TODO: talk about ∧
J : {A : Type ℓ} {B : A → Type ℓ'} {x : A}
    (P : (z : A) → x ≡ z → Type ℓ'')
    (d : P x refl) {y : A} (p : x ≡ y) → P y p
J P d p = transport (λ i → P (p i) (λ j → p (i ∧ j))) d

-- So J is provable, but it doesn't satisfy computation rule
-- definitionally. This is almost never a problem in practice as the
-- cubical primitives satisfy many new definitional equalities.


text:
module Structure.Relator.Ordering.Lattice where

import      Lvl
open import Functional
open import Logic
open import Logic.Propositional hiding (⊤ ; ⊥)
open import Logic.Predicate
open import Logic.Propositional.Theorems
open import Structure.Relator.Ordering
open import Structure.Relator.Properties hiding (antisymmetry ; asymmetry ; transitivity ; reflexivity ; irreflexivity)
open import Type

private variable ℓ₁ ℓ₂ ℓ₃ : Lvl.Level

module _ {T : Type{ℓ₁}} where
  record Top (_≤_ : T → T → Stmt{ℓ₂}) (P : T → Stmt{ℓ₃}) (m : T) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    constructor intro
    field
      ⦃ membership ⦄ : P(m)
      proof : ∀{x : T} → ⦃ _ : P(x) ⦄ → (x ≤ m)

  module _ (_≤_ : T → T → Stmt{ℓ₂}) where
    Bottom : (P : T → Stmt{ℓ₃}) (m : T) → Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃}
    Bottom = Top(swap(_≤_))
    module Bottom{ℓ₂}{ℓ₃}{_≤_} = Top{ℓ₂}{ℓ₃}{swap(_≤_)}

  record RightBound (_≤_ : T → T → Stmt{ℓ₂}) (P : T → Stmt{ℓ₃}) (b : T) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    constructor intro
    field proof : ∀{x : T} → ⦃ _ : P(x) ⦄ → (x ≤ b)

  module _ (_≤_ : T → T → Stmt{ℓ₂}) where
    LeftBound : (P : T → Stmt{ℓ₃}) → (b : T) → Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃}
    LeftBound = RightBound(swap(_≤_))
    module LeftBound{ℓ₂}{ℓ₃}{_≤_} = RightBound{ℓ₂}{ℓ₃}{swap(_≤_)}

  record Meet (_≤_ : T → T → Stmt{ℓ₂}) (P : T → Stmt{ℓ₃}) (inf : T) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    constructor intro
    field
      bound : LeftBound(_≤_)(P) (inf)
      extreme : RightBound(_≤_)(LeftBound(_≤_)(P)) (inf)

  module _ (_≤_ : T → T → Stmt{ℓ₂}) where
    Join : (P : T → Stmt{ℓ₃}) → (sup : T) → Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃}
    Join = Meet(swap(_≤_))
    module Join{ℓ₂}{ℓ₃}{_≤_} = Meet{ℓ₂}{ℓ₃}{swap(_≤_)}

  module Complete {ℓ₃} where
    record MeetSemilattice (_≤_ : T → T → Stmt{ℓ₂}) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ Lvl.𝐒(ℓ₃)} where
      constructor intro
      field proof : ∀{P : T → Stmt{ℓ₃}} → ∃(Meet(_≤_)(P))

    module _ (_≤_ : T → T → Stmt{ℓ₂}) where
      JoinSemilattice : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ Lvl.𝐒(ℓ₃)}
      JoinSemilattice = MeetSemilattice(swap(_≤_))
      module JoinSemilattice{ℓ₂}{_≤_} = MeetSemilattice{ℓ₂}{swap(_≤_)}

    record Lattice (_≤_ : T → T → Stmt{ℓ₂}) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ Lvl.𝐒(ℓ₃)} where
      constructor intro
      field
        ⦃ meet-semilattice ⦄ : MeetSemilattice(_≤_)
        ⦃ join-semilattice ⦄ : JoinSemilattice(_≤_)

      record Bounded (_≤_ : T → T → Stmt{ℓ₂}) (⊤ : T) (⊥ : T) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ Lvl.𝐒(ℓ₃)} where
        constructor intro
        field
          ⦃ bottom ⦄ : Weak.Properties.Extremumₗ(_≤_)(⊥)
          ⦃ top ⦄    : Weak.Properties.Extremumᵣ(_≤_)(⊤)

  top : (_≤_ : T → T → Stmt{ℓ₂}) → (P : T → Stmt{ℓ₃}) → ⦃ _ : ∃(Top(_≤_)(P)) ⦄ → T
  top _ (P) ⦃ e ⦄ = [∃]-witness e

  bottom : (_≤_ : T → T → Stmt{ℓ₂}) → (P : T → Stmt{ℓ₃}) → ⦃ _ : ∃(Bottom(_≤_)(P)) ⦄ → T
  bottom(_≤_) = top(swap(_≤_))

  meet : (_≤_ : T → T → Stmt{ℓ₂}) → (P : T → Stmt{ℓ₃}) → ⦃ _ : ∃(Meet(_≤_)(P)) ⦄ → T
  meet _ _ ⦃ e ⦄ = [∃]-witness e

  join :  (_≤_ : T → T → Stmt{ℓ₂}) → (P : T → Stmt{ℓ₃}) → ⦃ _ : ∃(Join(_≤_)(P)) ⦄ → T
  join(_≤_) = meet(swap(_≤_))

  module Oper where
    ⊥ = bottom
    ⊤ = top
    ⋁ = join
    ⋀ = meet

  -- LE is a module with synonyms when the order is interpreted as a (_≤_) (lesser than or equals) relation.
  module LE where
    Minimum    = Bottom
    Maximum    = Top
    LowerBound = LeftBound
    UpperBound = RightBound
    Supremum   = Join
    Infimum    = Meet

    module Minimum    = Bottom
    module Maximum    = Top
    module LowerBound = LeftBound
    module UpperBound = RightBound
    module Supremum   = Join
    module Infimum    = Meet

    min = bottom
    max = top
    sup = join
    inf = meet

-- TODO: https://en.wikipedia.org/wiki/Map_of_lattices


text:
module Haskell.Prim.Enum where

open import Agda.Builtin.Nat as Nat hiding (_==_; _<_; _+_; _*_; _-_)
open import Agda.Builtin.Char
open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Unit
open import Agda.Builtin.Int using (pos; negsuc)

open import Haskell.Prim
open import Haskell.Prim.Bool
open import Haskell.Prim.Bounded
open import Haskell.Prim.Either
open import Haskell.Prim.Eq
open import Haskell.Prim.Functor
open import Haskell.Prim.Int
open import Haskell.Prim.Integer
open import Haskell.Prim.List
open import Haskell.Prim.Maybe
open import Haskell.Prim.Num
open import Haskell.Prim.Ord
open import Haskell.Prim.Tuple
open import Haskell.Prim.Word

--------------------------------------------------
-- Enum
--    Assumptions: unbounded enums have no constraints on their
--    operations and bounded enums should work on all values between
--    minBound and maxBound. Unbounded enums do not support enumFrom
--    and enumFromThen (since they return infinite lists).

IfBoundedBelow : Maybe (BoundedBelow a) → (⦃ BoundedBelow a ⦄ → Set) → Set
IfBoundedBelow Nothing  k = ⊤
IfBoundedBelow (Just i) k = k ⦃ i ⦄

IfBoundedAbove : Maybe (BoundedAbove a) → (⦃ BoundedAbove a ⦄ → Set) → Set
IfBoundedAbove Nothing  k = ⊤
IfBoundedAbove (Just i) k = k ⦃ i ⦄

record Enum (a : Set) : Set₁ where
  field
    BoundedBelowEnum : Maybe (BoundedBelow a)
    BoundedAboveEnum : Maybe (BoundedAbove a)
    fromEnum         : a → Int

  private
    IsBoundedBelow : Set
    IsBoundedBelow = maybe ⊥ (λ _ → ⊤) BoundedBelowEnum

    IsBoundedAbove : Set
    IsBoundedAbove = maybe ⊥ (λ _ → ⊤) BoundedAboveEnum

    TrueIfLB : (⦃ BoundedBelow a ⦄ → Bool) → Set
    TrueIfLB C = IfBoundedBelow BoundedBelowEnum (IsTrue C)

    TrueIfUB : (⦃ BoundedAbove a ⦄ → Bool) → Set
    TrueIfUB C = IfBoundedAbove BoundedAboveEnum (IsTrue C)

    FalseIfLB : (⦃ BoundedBelow a ⦄ → Bool) → Set
    FalseIfLB C = IfBoundedBelow BoundedBelowEnum (IsFalse C)

    FalseIfUB : (⦃ BoundedAbove a ⦄ → Bool) → Set
    FalseIfUB C = IfBoundedAbove BoundedAboveEnum (IsFalse C)

    minInt : ⦃ BoundedBelow a ⦄ → Int
    minInt ⦃ _ ⦄ = fromEnum minBound

    maxInt : ⦃ BoundedAbove a ⦄ → Int
    maxInt ⦃ _ ⦄ = fromEnum maxBound

  field
    toEnum : (n : Int) → ⦃ TrueIfLB (minInt <= n) ⦄ → ⦃ TrueIfUB (n <= maxInt) ⦄ → a
    succ   : (x : a) → ⦃ FalseIfUB (fromEnum x == maxInt) ⦄ → a
    pred   : (x : a) → ⦃ FalseIfLB (fromEnum x == minInt) ⦄ → a

    enumFrom       : ⦃ IsBoundedAbove ⦄ → a → List a
    enumFromTo     : a → a → List a
    -- In the Prelude Enum instances `enumFromThenTo x x y` gives the
    -- infinite list of `x`s. The constraint is a little bit stronger than it needs to be,
    -- since it rules out different x and x₁ that maps to the same Int, but this saves us
    -- requiring an Eq instance for `a`, and it's not a terrible limitation to not be able to
    -- write [0, 2^64 .. 2^66].
    enumFromThenTo : (x x₁ : a) → ⦃ IsFalse (fromEnum x == fromEnum x₁) ⦄ → a → List a
    enumFromThen   : ⦃ IsBoundedBelow ⦄ → ⦃ IsBoundedAbove ⦄ → (x x₁ : a) → ⦃ IsFalse (fromEnum x == fromEnum x₁) ⦄ → List a

open Enum ⦃ ... ⦄ public

private
  divNat : Nat → Nat → Nat
  divNat a 0       = 0
  divNat a (suc b) = div-helper 0 b a b

  diff : Integer → Integer → Maybe Nat
  diff a b =
    case a - b of λ where
      (pos n)    → Just n
      (negsuc _) → Nothing

  unsafeIntegerToNat : Integer → Nat
  unsafeIntegerToNat (pos n) = n
  unsafeIntegerToNat (negsuc _) = 0

  integerFromCount : Integer → Integer → Nat → List Integer
  integerFromCount a step 0       = []
  integerFromCount a step (suc n) = a ∷ integerFromCount (a + step) step n

  integerFromTo : Integer → Integer → List Integer
  integerFromTo a b = maybe [] (integerFromCount a 1 ∘ suc) (diff b a)

  integerFromThenTo : (a a₁ : Integer) → ⦃ IsFalse (integerToInt a == integerToInt a₁) ⦄ → Integer → List Integer
  integerFromThenTo a a₁ b =
    case compare a a₁ of λ where
      LT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a₁ - a))))) (diff b a)
      EQ → [] -- impossible
      GT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a - a₁))))) (diff a b)

instance
  iEnumInteger : Enum Integer
  iEnumInteger .BoundedBelowEnum  = Nothing
  iEnumInteger .BoundedAboveEnum  = Nothing
  iEnumInteger .fromEnum          = integerToInt
  iEnumInteger .toEnum          n = intToInteger n
  iEnumInteger .succ              = _+ 1
  iEnumInteger .pred              = _- 1
  iEnumInteger .enumFromTo        = integerFromTo
  iEnumInteger .enumFromThenTo    = integerFromThenTo

module _ (from : a → Integer) (to : Integer → a) where
  private
    fromTo : a → a → List a
    fromTo a b = map to (enumFromTo (from a) (from b))

    fromThenTo : (x x₁ : a) → ⦃ IsFalse (fromEnum (from x) == fromEnum (from x₁)) ⦄ → a → List a
    fromThenTo a a₁ b = map to (enumFromThenTo (from a) (from a₁) (from b))

  unboundedEnumViaInteger : Enum a
  unboundedEnumViaInteger .BoundedBelowEnum      = Nothing
  unboundedEnumViaInteger .BoundedAboveEnum      = Nothing
  unboundedEnumViaInteger .fromEnum              = integerToInt ∘ from
  unboundedEnumViaInteger .toEnum         n      = to (intToInteger n)
  unboundedEnumViaInteger .succ           x      = to (from x + 1)
  unboundedEnumViaInteger .pred           x      = to (from x - 1)
  unboundedEnumViaInteger .enumFromTo     a b    = fromTo a b
  unboundedEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b

  boundedBelowEnumViaInteger : ⦃ Ord a ⦄ → ⦃ BoundedBelow a ⦄ → Enum a
  boundedBelowEnumViaInteger .BoundedBelowEnum      = Just it
  boundedBelowEnumViaInteger .BoundedAboveEnum      = Nothing
  boundedBelowEnumViaInteger .fromEnum              = integerToInt ∘ from
  boundedBelowEnumViaInteger .toEnum         n      = to (intToInteger n)
  boundedBelowEnumViaInteger .succ           x      = to (from x + 1)
  boundedBelowEnumViaInteger .pred           x      = to (from x - 1)
  boundedBelowEnumViaInteger .enumFromTo     a b    = fromTo a b
  boundedBelowEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b

  boundedAboveEnumViaInteger : ⦃ Ord a ⦄ → ⦃ BoundedAbove a ⦄ → Enum a
  boundedAboveEnumViaInteger .BoundedBelowEnum      = Nothing
  boundedAboveEnumViaInteger .BoundedAboveEnum      = Just it
  boundedAboveEnumViaInteger .fromEnum              = integerToInt ∘ from
  boundedAboveEnumViaInteger .toEnum         n      = to (intToInteger n)
  boundedAboveEnumViaInteger .succ           x      = to (from x + 1)
  boundedAboveEnumViaInteger .pred           x      = to (from x - 1)
  boundedAboveEnumViaInteger .enumFrom       a      = fromTo a maxBound
  boundedAboveEnumViaInteger .enumFromTo     a b    = fromTo a b
  boundedAboveEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b

  boundedEnumViaInteger : ⦃ Ord a ⦄ → ⦃ Bounded a ⦄ → Enum a
  boundedEnumViaInteger .BoundedBelowEnum      = Just it
  boundedEnumViaInteger .BoundedAboveEnum      = Just it
  boundedEnumViaInteger .fromEnum              = integerToInt ∘ from
  boundedEnumViaInteger .toEnum         n      = to (intToInteger n)
  boundedEnumViaInteger .succ           x      = to (from x + 1)
  boundedEnumViaInteger .pred           x      = to (from x - 1)
  boundedEnumViaInteger .enumFromTo     a b    = fromTo a b
  boundedEnumViaInteger .enumFromThenTo a a₁ b = fromThenTo a a₁ b
  boundedEnumViaInteger .enumFrom       a      = fromTo a maxBound
  boundedEnumViaInteger .enumFromThen   a a₁   =
    if a < a₁ then fromThenTo a a₁ maxBound
              else fromThenTo a a₁ minBound

instance
  iEnumNatural : Enum Nat
  iEnumNatural = boundedBelowEnumViaInteger pos unsafeIntegerToNat

  iEnumInt : Enum Int
  iEnumInt = boundedEnumViaInteger intToInteger integerToInt

  iEnumWord : Enum Word
  iEnumWord = boundedEnumViaInteger wordToInteger integerToWord

  iEnumBool : Enum Bool
  iEnumBool = boundedEnumViaInteger (if_then 1 else 0) (_/= 0)

  iEnumOrdering : Enum Ordering
  iEnumOrdering = boundedEnumViaInteger (λ where LT → 0; EQ → 1; GT → 2)
                                        (λ where (pos 0) → LT; (pos 1) → EQ; _ → GT)

  iEnumUnit : Enum (Tuple [])
  iEnumUnit = boundedEnumViaInteger (λ _ → 0) (λ _ → [])

  iEnumChar : Enum Char
  iEnumChar = boundedEnumViaInteger (pos ∘ primCharToNat)
                                    λ where (pos n) → primNatToChar n; _ → '_'

  -- Missing:
  --  Enum Double  (can't go via Integer)