text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.RingSolver.RawAlgebra where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Int renaming (_+_ to _+ℤ_ ; _·_ to _·ℤ_ ; -_ to -ℤ_ ; _-_ to _-ℤ_ ; +Assoc to +ℤAssoc ; +Comm to +ℤComm ; -DistL· to -ℤDistL·ℤ)

open import Cubical.Algebra.RingSolver.RawRing renaming (⟨_⟩ to ⟨_⟩ᵣ)
open import Cubical.Algebra.RingSolver.IntAsRawRing
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring

private
  variable
    ℓ ℓ′ : Level

record RawAlgebra (R : RawRing ℓ) (ℓ′ : Level) : Type (ℓ-suc (ℓ-max ℓ ℓ′)) where

  constructor rawalgebra

  field
    Carrier : Type ℓ′
    scalar  : ⟨ R ⟩ᵣ → Carrier
    0r      : Carrier
    1r      : Carrier
    _+_     : Carrier → Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier

  infixl 8 _·_
  infixl 7 -_
  infixl 6 _+_

⟨_⟩ : {R : RawRing ℓ} → RawAlgebra R ℓ′ → Type ℓ′
⟨_⟩ = RawAlgebra.Carrier

{-
  Mapping to integer scalars and its (homorphism) properties.
-}
module _ (R : CommRing ℓ) where
  open CommRingStr (snd R)
  open Cubical.Algebra.Ring.RingTheory (CommRing→Ring R)

  scalarℕ : ℕ → (fst R)
  scalarℕ ℕ.zero = 0r
  scalarℕ (ℕ.suc ℕ.zero) = 1r
  scalarℕ (ℕ.suc (ℕ.suc n)) = 1r + scalarℕ (ℕ.suc n)

  scalar : ℤ → (fst R)
  scalar (pos k)  = scalarℕ k
  scalar (negsuc k)  = - scalarℕ (ℕ.suc k)

  -DistScalar : (k : ℤ)
                → scalar (-ℤ k) ≡ - (scalar k)
  -DistScalar (pos ℕ.zero) = sym 0Selfinverse
  -DistScalar (pos (ℕ.suc n)) = refl
  -DistScalar (negsuc n) = sym (-Idempotent _)

  lemmaSuc : (k : ℤ)
          → scalar (sucℤ k) ≡ 1r + scalar k
  lemmaSuc (pos ℕ.zero) = sym (+Rid _)
  lemmaSuc (pos (ℕ.suc ℕ.zero)) = refl
  lemmaSuc (pos (ℕ.suc (ℕ.suc n))) = refl
  lemmaSuc (negsuc ℕ.zero) = sym (+Rinv _)
  lemmaSuc (negsuc (ℕ.suc n)) =
    scalar (negsuc n)                        ≡⟨ sym (+Lid (scalar (negsuc n))) ⟩
    0r + scalar (negsuc n)                  ≡[ i ]⟨ +Rinv 1r (~ i) + scalar (negsuc n) ⟩
    (1r - 1r) + scalar (negsuc n)           ≡⟨ sym (+Assoc _ _ _) ⟩
    1r + (- 1r + - scalar (pos (ℕ.suc n))) ≡[ i ]⟨ 1r + -Dist 1r (scalar (pos (ℕ.suc n))) i ⟩
    1r + -(1r + scalar (pos (ℕ.suc n)))    ≡⟨ refl ⟩
    1r + -(scalar (pos (ℕ.suc (ℕ.suc n)))) ≡⟨ refl ⟩
    1r + scalar (negsuc (ℕ.suc n)) ∎

  lemmaPred : (k : ℤ)
          → scalar (predℤ k) ≡ - 1r + scalar k
  lemmaPred k = sym(
    - 1r + scalar k                      ≡[ i ]⟨ - 1r + scalar (sucPred k (~ i)) ⟩
    - 1r + scalar (sucℤ (predℤ k))   ≡[ i ]⟨ - 1r + lemmaSuc (predℤ k) i ⟩
    - 1r + (1r + scalar (predℤ k))     ≡⟨ +Assoc _ _ _ ⟩
    (- 1r + 1r) + scalar (predℤ k)     ≡[ i ]⟨ +Linv 1r i + scalar (predℤ k) ⟩
    0r + scalar (predℤ k)              ≡⟨ +Lid _ ⟩
    scalar (predℤ k)  ∎)

  +HomScalar : (k l : ℤ)
               → scalar (k +ℤ l) ≡ (scalar k) + (scalar l)
  +HomScalar (pos ℕ.zero) l =
             scalar (0 +ℤ l)       ≡[ i ]⟨ scalar (sym (pos0+ l) i) ⟩
             scalar l              ≡⟨ sym (+Lid _) ⟩
             0r + scalar l         ≡⟨ refl  ⟩
             scalar 0 + scalar l   ∎

  +HomScalar (pos (ℕ.suc ℕ.zero)) l =
    scalar (1 +ℤ l)                         ≡[ i ]⟨ scalar (+ℤComm 1 l i) ⟩
    scalar (l  +ℤ 1)                        ≡⟨ refl ⟩
    scalar (sucℤ l)                       ≡⟨ lemmaSuc l ⟩
    1r + scalar l                           ≡⟨ refl ⟩
    scalar (pos (ℕ.suc ℕ.zero)) + scalar l ∎

  +HomScalar (pos (ℕ.suc (ℕ.suc n))) l =
    scalar (pos (ℕ.suc (ℕ.suc n)) +ℤ l)        ≡⟨ refl ⟩
    scalar ((pos (ℕ.suc n) +ℤ 1) +ℤ l)         ≡[ i ]⟨ scalar ((+ℤComm (pos (ℕ.suc n)) 1 i) +ℤ l) ⟩
    scalar ((1 +ℤ (pos (ℕ.suc n))) +ℤ l)       ≡[ i ]⟨ scalar (+ℤAssoc 1 (pos (ℕ.suc n)) l (~ i)) ⟩
    scalar (1 +ℤ (pos (ℕ.suc n) +ℤ l))         ≡⟨ +HomScalar (pos (ℕ.suc ℕ.zero)) (pos (ℕ.suc n) +ℤ l) ⟩
    scalar 1 + scalar (pos (ℕ.suc n) +ℤ l)     ≡⟨ refl ⟩
    1r + (scalar (pos (ℕ.suc n) +ℤ l))         ≡[ i ]⟨ 1r + +HomScalar (pos (ℕ.suc n)) l i ⟩
    1r + (scalar (pos (ℕ.suc n)) + scalar l)   ≡⟨ +Assoc _ _ _ ⟩
    (1r + scalar (pos (ℕ.suc n))) + scalar l   ≡⟨ refl ⟩
    scalar (pos (ℕ.suc (ℕ.suc n))) + scalar l ∎

  +HomScalar (negsuc ℕ.zero) l =
    scalar (-1 +ℤ l)                  ≡[ i ]⟨ scalar (+ℤComm -1 l i) ⟩
    scalar (l +ℤ -1)                  ≡⟨ refl ⟩
    scalar (predℤ l)                ≡⟨ lemmaPred l ⟩
    - 1r + scalar l                    ≡⟨ refl ⟩
    scalar -1 + scalar l ∎

  +HomScalar (negsuc (ℕ.suc n)) l =
    scalar (negsuc (ℕ.suc n) +ℤ l)               ≡⟨ refl ⟩
    scalar ((negsuc n +ℤ -1) +ℤ l)               ≡[ i ]⟨ scalar (+ℤComm (negsuc n) -1 i +ℤ l) ⟩
    scalar ((-1 +ℤ negsuc n) +ℤ l)               ≡[ i ]⟨ scalar (+ℤAssoc -1 (negsuc n) l (~ i)) ⟩
    scalar (-1 +ℤ (negsuc n +ℤ l))               ≡⟨ +HomScalar -1 (negsuc n +ℤ l) ⟩
    - 1r + scalar (negsuc n +ℤ l)                 ≡[ i ]⟨ - 1r + +HomScalar (negsuc n) l i ⟩
    - 1r + (scalar (negsuc n) + scalar l)         ≡⟨ +Assoc (- 1r) _ _ ⟩
    (- 1r + (scalar (negsuc n))) + scalar l       ≡⟨ refl ⟩
    (- 1r + - scalar (pos (ℕ.suc n))) + scalar l ≡[ i ]⟨ -Dist 1r (scalar (pos (ℕ.suc n))) i + scalar l ⟩
    (- (1r + scalar (pos (ℕ.suc n)))) + scalar l ≡⟨ refl ⟩
    scalar (negsuc (ℕ.suc n)) + scalar l ∎

  lemma1 : (n : ℕ)
          → 1r + scalar (pos n) ≡ scalar (pos (ℕ.suc n))
  lemma1 ℕ.zero = +Rid _
  lemma1 (ℕ.suc k) = refl

  lemma-1 : (n : ℕ)
          → - 1r + scalar (negsuc n) ≡ scalar (negsuc (ℕ.suc n))
  lemma-1 ℕ.zero = -Dist _ _
  lemma-1 (ℕ.suc k) =
    - 1r + scalar (negsuc (ℕ.suc k))        ≡⟨ refl ⟩
    - 1r + - scalar (pos (ℕ.suc (ℕ.suc k))) ≡⟨ -Dist _ _ ⟩
    - (1r + scalar (pos (ℕ.suc (ℕ.suc k)))) ≡⟨ refl ⟩
    scalar (negsuc (ℕ.suc (ℕ.suc k))) ∎

  ·HomScalar : (k l : ℤ)
             → scalar (k ·ℤ l) ≡ scalar k · scalar l
  ·HomScalar (pos ℕ.zero) l =  0r ≡⟨ sym (0LeftAnnihilates (scalar l)) ⟩ 0r · scalar l ∎
  ·HomScalar (pos (ℕ.suc n)) l =
    scalar (l +ℤ (pos n ·ℤ l))                  ≡⟨ +HomScalar l (pos n ·ℤ l) ⟩
    scalar l + scalar (pos n ·ℤ l)              ≡[ i ]⟨ scalar l + ·HomScalar (pos n) l i ⟩
    scalar l + (scalar (pos n) · scalar l)      ≡[ i ]⟨ ·Lid (scalar l) (~ i) + (scalar (pos n) · scalar l) ⟩
    1r · scalar l + (scalar (pos n) · scalar l) ≡⟨ sym (·Ldist+ 1r _ _) ⟩
    (1r + scalar (pos n)) · scalar l            ≡[ i ]⟨ lemma1 n i · scalar l ⟩
    scalar (pos (ℕ.suc n)) · scalar l ∎

  ·HomScalar (negsuc ℕ.zero) l =
    scalar (-ℤ l)                     ≡⟨ -DistScalar l ⟩
    - scalar l                        ≡[ i ]⟨ - (·Lid (scalar l) (~ i)) ⟩
    - (1r · scalar l)                 ≡⟨ sym (-DistL· _ _) ⟩
    - 1r · scalar l                   ≡⟨ refl ⟩
    scalar (negsuc ℕ.zero) · scalar l ∎

  ·HomScalar (negsuc (ℕ.suc n)) l =
    scalar ((-ℤ l) +ℤ (negsuc n ·ℤ l))             ≡⟨ +HomScalar (-ℤ l) (negsuc n ·ℤ l) ⟩
    scalar (-ℤ l) + scalar (negsuc n ·ℤ l)         ≡[ i ]⟨ -DistScalar l i + scalar (negsuc n ·ℤ l) ⟩
    - scalar l + scalar (negsuc n ·ℤ l)            ≡[ i ]⟨ - scalar l + ·HomScalar (negsuc n) l i ⟩
    - scalar l + scalar (negsuc n) · scalar l      ≡[ i ]⟨ (- ·Lid (scalar l) (~ i))
                                                           + scalar (negsuc n) · scalar l ⟩
    - (1r · scalar l) + scalar (negsuc n) · scalar l ≡[ i ]⟨ -DistL· 1r (scalar l) (~ i)
                                                            + scalar (negsuc n) · scalar l ⟩
    - 1r · scalar l + scalar (negsuc n) · scalar l ≡⟨ sym (·Ldist+ _ _ _) ⟩
    (- 1r + scalar (negsuc n)) · scalar l          ≡[ i ]⟨ lemma-1 n i · scalar l ⟩
    scalar (negsuc (ℕ.suc n)) · scalar l ∎

CommRing→RawℤAlgebra : CommRing ℓ → RawAlgebra ℤAsRawRing ℓ
CommRing→RawℤAlgebra (R , commringstr 0r 1r _+_ _·_ -_ isCommRing) =
  rawalgebra R (scalar ((R , commringstr 0r 1r _+_ _·_ -_ isCommRing))) 0r 1r _+_ _·_ -_

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Simply-typed changes (Fig. 3 and Fig. 4d)
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type

module Parametric.Change.Type
  (Base : Type.Structure)
  where

open Type.Structure Base

-- Extension point: Simply-typed changes of base types.
Structure : Set
Structure = Base → Type

module Structure (ΔBase : Structure) where
  -- We provide: Simply-typed changes on simple types.
  ΔType : Type → Type
  ΔType (base ι) = ΔBase ι
  ΔType (σ ⇒ τ) = σ ⇒ ΔType σ ⇒ ΔType τ

  -- And we also provide context merging.
  open import Base.Change.Context ΔType public

ext: agda

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

open import HoTT

module homotopy.ModalWedgeExtension {i} (M : Modality i)
  {A : Type i} {a₀ : A} {B : Type i} {b₀ : B} where

  open Modality M
  private
    X = ⊙[ A , a₀ ]
    Y = ⊙[ B , b₀ ]
  open import homotopy.FiberOfWedgeToProduct X Y

  record args : Type (lsucc i) where
    field
      join-conn : (a : A) (b : B) → is-◯-connected ((a₀ == a) * (b₀ == b))
      R : A → B → ◯-Type
      f : (a : A) → fst (R a b₀)
      g : (b : B) → fst (R a₀ b)
      p : f a₀ == g b₀

  module _ (r : args) where
    open args r

    abstract
      ∨-to-×-is-◯-equiv : is-◯-equiv (∨-to-× {X = X} {Y = Y})
      ∨-to-×-is-◯-equiv (a , b) = equiv-preserves-◯-conn (fiber-thm a b ⁻¹) (join-conn a b)

    module A∨BToR = WedgeElim f g
      (↓-ap-out= (fst ∘ uncurry R) ∨-to-× wglue (∨-to-×-glue-β {X = X} {Y = Y}) p)

    A∨B-to-R : ∀ w → fst (uncurry R (∨-to-× w))
    A∨B-to-R = A∨BToR.f

    ext : (a : A) → (b : B) → fst (R a b)
    ext = curry $ ◯-extend ∨-to-×-is-◯-equiv (uncurry R) A∨B-to-R

  module _ {r : args} where
    open args r

    abstract
      β-l : (a : A) → ext r a b₀ == f a
      β-l a = ◯-extend-β (∨-to-×-is-◯-equiv r) (uncurry R) (A∨B-to-R r) (winl a)

      β-r : (b : B) → ext r a₀ b == g b
      β-r b = ◯-extend-β (∨-to-×-is-◯-equiv r) (uncurry R) (A∨B-to-R r) (winr b)

      coh : ! (β-l a₀) ∙ β-r b₀ == p
      coh = ap (! (β-l a₀) ∙_) (! (∙'-unit-l (β-r b₀)) ∙ ! lemma₁)
          ∙ ! (∙-assoc (! (β-l a₀)) (β-l a₀) p)
          ∙ ap (_∙ p) (!-inv-l (β-l a₀))
        where
          -- maybe this has been proved somewhere?
          lemma₀ : ∀ {i j k} {A : Type i} {B : Type j} (C : (b : B) → Type k)
            (f : A → B) {x y} (p : x == y) {q : f x == f y} (r : ap f p == q)
            {cx cx' : C (f x)} {cy cy' : C (f y)}
            (s : cx' == cy' [ C ↓ q ]) (t : cx == cy [ C ↓ q ])
            (u : cx == cx') (v : cy == cy')
            → u ◃ ↓-ap-out= C f p r s == ↓-ap-out= C f p r t ▹ v
            → u ◃ s == t ▹ v
          lemma₀ C f idp idp idp idp u v u=v = u=v

          lemma₁ : β-l a₀ ∙ p == idp ∙' β-r b₀
          lemma₁ = lemma₀ (fst ∘ uncurry R) ∨-to-× wglue ∨-to-×-glue-β
            p idp (β-l a₀) (β-r b₀)
            ( ap (β-l a₀ ◃_) (! (A∨BToR.glue-β r))
            ∙ ↓-=-out (apd (◯-extend-β (∨-to-×-is-◯-equiv r) (uncurry R) (A∨B-to-R r)) wglue)
            ∙ ap (_▹ β-r b₀)
                (apd-∘'' (◯-extend (∨-to-×-is-◯-equiv r) (uncurry R) (A∨B-to-R r))
                   ∨-to-× wglue ∨-to-×-glue-β))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Level

-- This is really a degenerate version of Categories.Category.Instance.Zero
-- Here EmptySet is not given an explicit name, it is an alias for Lift o ⊥
module Categories.Category.Instance.EmptySet where

open import Data.Unit
open import Data.Empty using (⊥; ⊥-elim)
open import Function.Equality using (Π)
open Π using (_⟨$⟩_)

open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality using (refl)

open import Categories.Category.Instance.Sets
open import Categories.Category.Instance.Setoids
import Categories.Object.Initial as Init

module _ {o : Level} where
  open Init (Sets o)

  EmptySet-⊥ : Initial
  EmptySet-⊥ = record { ⊥ = Lift o ⊥ ; ⊥-is-initial = record { ! = λ { {A} (lift x) → ⊥-elim x } ; !-unique = λ { f {()} } } }

module _ {c ℓ : Level} where
  open Init (Setoids c ℓ)

  EmptySetoid : Setoid c ℓ
  EmptySetoid = record
    { Carrier = Lift c ⊥
    ; _≈_     = λ _ _ → Lift ℓ ⊤
    }

  EmptySetoid-⊥ : Initial
  EmptySetoid-⊥ = record
    { ⊥            = EmptySetoid
    ; ⊥-is-initial = record
      { !        = record
        { _⟨$⟩_ = λ { () }
        ; cong  = λ { {()} }
        }
      ; !-unique = λ { _ {()} }
      }
    }

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:
open import Data.Nat using ( ℕ )

module README ( n : ℕ ) where

------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Deep Embedding for Propositional Logic.
------------------------------------------------------------------------------

open import Data.PropFormula n public

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
{-

Technical results about elementary transformations

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.Matrix.Elementaries where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Data.Nat hiding (_+_ ; _·_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Bool
open import Cubical.Data.FinData renaming (znots to znotsFin ; snotz to snotzFin)

open import Cubical.Relation.Nullary

open import Cubical.Algebra.RingSolver.Reflection
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.Matrix
open import Cubical.Algebra.Matrix.CommRingCoefficient
open import Cubical.Algebra.Matrix.RowTransformation

private
  variable
    ℓ : Level
    A : Type ℓ
    m n k l : ℕ

module ElemTransformation (𝓡 : CommRing ℓ) where

  private
    R = 𝓡 .fst

  open CommRingStr     (𝓡 .snd) renaming ( is-set to isSetR )
  open KroneckerDelta  (CommRing→Ring 𝓡)
  open Sum             (CommRing→Ring 𝓡)

  open Coefficient           𝓡
  open LinearTransformation  𝓡

  open SimRel
  open Sim

  open isLinear
  open isLinear2×2

  -- Swapping the first row with another

  swapMat : Mat 2 2
  swapMat zero zero = 0r
  swapMat zero one  = 1r
  swapMat one  zero = 1r
  swapMat one  one  = 0r

  uniSwapMat : swapMat ⋆ swapMat ≡ 𝟙
  uniSwapMat t zero zero =
    (mul2 swapMat swapMat zero zero ∙ helper) t
    where helper : 0r · 0r + 1r · 1r ≡ 1r
          helper = solve 𝓡
  uniSwapMat t zero one  =
    (mul2 swapMat swapMat zero one  ∙ helper) t
    where helper : 0r · 1r + 1r · 0r ≡ 0r
          helper = solve 𝓡
  uniSwapMat t one  zero =
    (mul2 swapMat swapMat one  zero ∙ helper) t
    where helper : 1r · 0r + 0r · 1r ≡ 0r
          helper = solve 𝓡
  uniSwapMat t one  one  =
    (mul2 swapMat swapMat one  one  ∙ helper) t
    where helper : 1r · 1r + 0r · 0r ≡ 1r
          helper = solve 𝓡

  isInvSwapMat2 : isInv swapMat
  isInvSwapMat2 .fst = swapMat
  isInvSwapMat2 .snd .fst = uniSwapMat
  isInvSwapMat2 .snd .snd = uniSwapMat

  swapRow2 : Mat 2 n → Mat 2 n
  swapRow2 M zero = M one
  swapRow2 M one  = M zero

  isLinear2×2SwapRow2 : isLinear2×2 {n = n} swapRow2
  isLinear2×2SwapRow2 .transMat _ = swapMat
  isLinear2×2SwapRow2 .transEq M t zero j =
    ((mul2 swapMat M zero j) ∙ helper _ _) (~ t)
    where helper : (a b : R) → 0r · a + 1r · b ≡ b
          helper = solve 𝓡
  isLinear2×2SwapRow2 .transEq M t one  j =
    ((mul2 swapMat M one  j) ∙ helper _ _) (~ t)
    where helper : (a b : R) → 1r · a + 0r · b ≡ a
          helper = solve 𝓡

  swapRow : (i₀ : Fin m)(M : Mat (suc m) n) → Mat (suc m) n
  swapRow i M zero = M (suc i)
  swapRow zero M one  = M zero
  swapRow zero M (suc (suc i)) = M (suc (suc i))
  swapRow (suc i₀) M one   = M one
  swapRow (suc i₀) M (suc (suc i)) = swapRow i₀ (takeRowsᶜ M) (suc i)

  swapRowMat : (i₀ : Fin m) → Mat (suc m) (suc m)
  swapRowMat = trans2RowsMat swapMat

  swapRowEq : (i₀ : Fin m)(M : Mat (suc m) n) → swapRow i₀ M ≡ swapRowMat i₀ ⋆ M
  swapRowEq {m = suc m} zero M t zero j =
      (helper1 _ _
    ∙ (λ t → 0r · M zero j + ∑Mulr1 _ (λ i → M (suc i) j) zero (~ t))
    ∙ (λ t → 0r · M zero j + ∑ (λ i → helper2 (δ i zero) (M (suc i) j) t))) t
    where helper1 : (a b : R) → b ≡ 0r · a + b
          helper1 = solve 𝓡
          helper2 : (a b : R) → b · a ≡ (1r · a) · b
          helper2 = solve 𝓡
  swapRowEq {m = suc m} zero M t one  j =
      (helper _
    ∙ (λ t → (1r · 1r) · M zero j + ∑Mul0r (λ i → M (suc i) j) (~ t))) t
    where helper : (a : R) → a ≡ (1r · 1r) · a + 0r
          helper = solve 𝓡
  swapRowEq {m = suc m} zero M t (suc (suc i)) j =
      (helper _ _
    ∙ (λ t → (1r · 0r) · M zero j + ∑Mul1r _ (λ l → M (suc l) j) (suc i) (~ t))) t
    where helper : (a b : R) → b ≡ (1r · 0r) · a + b
          helper = solve 𝓡
  swapRowEq {m = suc m} (suc i₀) M t zero j =
      (helper1 _ _
    ∙ (λ t → 0r · M zero j + ∑Mul1r _ (λ i → M (suc i) j) (suc i₀) (~ t))
    ∙ (λ t → 0r · M zero j + ∑ (λ l → helper2 (δ (suc i₀) l) (M (suc l) j) t))) t
    where helper1 : (a b : R) → b ≡ 0r · a + b
          helper1 = solve 𝓡
          helper2 : (a b : R) → a · b ≡ (1r · a) · b
          helper2 = solve 𝓡
  swapRowEq {m = suc m} (suc i₀) M t one  j =
        (helper _ _ --helper1 _ _
      ∙ (λ t → (1r · 0r) · M zero j + ∑Mul1r _ (λ i → M (suc i) j) zero (~ t))) t
    where helper : (a b : R) → b ≡ (1r · 0r) · a + b
          helper = solve 𝓡
  swapRowEq {m = suc m} (suc i₀) M t (suc (suc i)) j =
     ((λ t → swapRowEq i₀ (takeRowsᶜ M) t (suc i) j)
    ∙ helper _ (M one j) _) t
    where helper : (a b c : R) → a + c ≡ a + (0r · b + c)
          helper = solve 𝓡

  isLinearSwapRow : (i : Fin m) → isLinear (swapRow {n = n} i)
  isLinearSwapRow i .transMat _ = swapRowMat i
  isLinearSwapRow i .transEq    = swapRowEq  i

  isInvSwapMat : (i : Fin m)(M : Mat (suc m) (suc n)) → isInv (isLinearSwapRow i .transMat M)
  isInvSwapMat i _ = isInvTrans2RowsMat _ i isInvSwapMat2

  -- Similarity defined by swapping

  record SwapFirstRow (i : Fin m)(M : Mat (suc m) (suc n)) : Type ℓ where
    field
      sim : Sim M
      swapEq : (j : Fin (suc n)) → M (suc i) j ≡ sim .result zero j

  record SwapFirstCol (j : Fin n)(M : Mat (suc m) (suc n)) : Type ℓ where
    field
      sim : Sim M
      swapEq : (i : Fin (suc m)) → M i (suc j) ≡ sim .result i zero

  record SwapPivot (i : Fin (suc m))(j : Fin (suc n))(M : Mat (suc m) (suc n)) : Type ℓ where
    field
      sim : Sim M
      swapEq : M i j ≡ sim .result zero zero

  open SwapFirstRow
  open SwapFirstCol
  open SwapPivot

  swapFirstRow : (i : Fin m)(M : Mat (suc m) (suc n)) → SwapFirstRow i M
  swapFirstRow i M .sim .result    = swapRow i M
  swapFirstRow i M .sim .simrel .transMatL = isLinearSwapRow i .transMat M
  swapFirstRow i M .sim .simrel .transMatR = 𝟙
  swapFirstRow i M .sim .simrel .transEq     = isLinearSwapRow i .transEq _ ∙ sym (⋆rUnit _)
  swapFirstRow i M .sim .simrel .isInvTransL = isInvSwapMat i M
  swapFirstRow i M .sim .simrel .isInvTransR = isInv𝟙
  swapFirstRow i M .swapEq j = refl

  swapFirstCol : (j : Fin n)(M : Mat (suc m) (suc n)) → SwapFirstCol j M
  swapFirstCol j M .sim .result    = (swapRow j (M ᵗ))ᵗ
  swapFirstCol j M .sim .simrel .transMatL = 𝟙
  swapFirstCol j M .sim .simrel .transMatR = (isLinearSwapRow j .transMat (M ᵗ))ᵗ
  swapFirstCol j M .sim .simrel .transEq =
    let P = isLinearSwapRow j .transMat (M ᵗ) in
      (λ t → (isLinearSwapRow j .transEq (M ᵗ) t)ᵗ)
    ∙ compᵗ P (M ᵗ)
    ∙ (λ t → idemᵗ M t ⋆ P ᵗ)
    ∙ (λ t → ⋆lUnit M (~ t) ⋆ P ᵗ)
  swapFirstCol j M .sim .simrel .isInvTransL = isInv𝟙
  swapFirstCol j M .sim .simrel .isInvTransR =
    isInvᵗ {M = isLinearSwapRow j .transMat (M ᵗ)} (isInvSwapMat j (M ᵗ))
  swapFirstCol j M .swapEq i t = M i (suc j)

  swapPivot : (i : Fin (suc m))(j : Fin (suc n))(M : Mat (suc m) (suc n)) → SwapPivot i j M
  swapPivot zero zero M .sim    = idSim M
  swapPivot zero zero M .swapEq = refl
  swapPivot (suc i) zero M .sim    = swapFirstRow i M .sim
  swapPivot (suc i) zero M .swapEq = refl
  swapPivot zero (suc j) M .sim    = swapFirstCol j M .sim
  swapPivot zero (suc j) M .swapEq = refl
  swapPivot (suc i) (suc j) M .sim = compSim (swapFirstRow i M .sim) (swapFirstCol j _ .sim)
  swapPivot (suc i) (suc j) M .swapEq = refl

  -- Add the first row to another

  addMat : Mat 2 2
  addMat zero zero = 1r
  addMat zero one  = 0r
  addMat one  zero = 1r
  addMat one  one  = 1r

  subMat : Mat 2 2
  subMat zero zero = 1r
  subMat zero one  = 0r
  subMat one  zero = - 1r
  subMat one  one  = 1r

  add⋆subMat : addMat ⋆ subMat ≡ 𝟙
  add⋆subMat t zero zero =
    (mul2 addMat subMat zero zero ∙ helper) t
    where helper : 1r · 1r + 0r · - 1r ≡ 1r
          helper = solve 𝓡
  add⋆subMat t zero one  =
    (mul2 addMat subMat zero one  ∙ helper) t
    where helper : 1r · 0r + 0r · 1r ≡ 0r
          helper = solve 𝓡
  add⋆subMat t one  zero =
    (mul2 addMat subMat one  zero ∙ helper) t
    where helper : 1r · 1r + 1r · - 1r ≡ 0r
          helper = solve 𝓡
  add⋆subMat t one  one  =
    (mul2 addMat subMat one  one  ∙ helper) t
    where helper : 1r · 0r + 1r · 1r ≡ 1r
          helper = solve 𝓡

  sub⋆addMat : subMat ⋆ addMat ≡ 𝟙
  sub⋆addMat t zero zero =
    (mul2 subMat addMat  zero zero ∙ helper) t
    where helper : 1r · 1r + 0r · 1r ≡ 1r
          helper = solve 𝓡
  sub⋆addMat t zero one  =
    (mul2 subMat addMat  zero one  ∙ helper) t
    where helper : 1r · 0r + 0r · 1r ≡ 0r
          helper = solve 𝓡
  sub⋆addMat t one  zero =
    (mul2 subMat addMat  one  zero ∙ helper) t
    where helper : - 1r · 1r + 1r · 1r ≡ 0r
          helper = solve 𝓡
  sub⋆addMat t one  one  =
    (mul2 subMat addMat  one  one  ∙ helper) t
    where helper : - 1r · 0r + 1r · 1r ≡ 1r
          helper = solve 𝓡

  isInvAddMat2 : isInv addMat
  isInvAddMat2 .fst = subMat
  isInvAddMat2 .snd .fst = add⋆subMat
  isInvAddMat2 .snd .snd = sub⋆addMat

  addRow2 : Mat 2 n → Mat 2 n
  addRow2 M zero  = M zero
  addRow2 M one j = M zero j + M one j

  isLinear2AddRow2 : isLinear2×2 {n = n} addRow2
  isLinear2AddRow2 .transMat _ = addMat
  isLinear2AddRow2 .transEq M t zero j =
    ((mul2 addMat M zero j) ∙ helper _ _) (~ t)
    where helper : (a b : R) → 1r · a + 0r · b ≡ a
          helper = solve 𝓡
  isLinear2AddRow2 .transEq M t one  j =
    ((mul2 addMat M one  j) ∙ helper _ _) (~ t)
    where helper : (a b : R) → 1r · a + 1r · b ≡ a + b
          helper = solve 𝓡

  -- Add the first row to all other rows

  addRows : Mat (suc m) n → Mat (suc m) n
  addRows M zero = M zero
  addRows M (suc i) j = M zero j + M (suc i) j

  private
    firstRowStayInvariant : (M : Mat (suc m) n) → M zero ≡ transRows addRow2 M zero
    firstRowStayInvariant = invRow₀ _ (λ _ → refl)

  addRowsEq : (M : Mat (suc m) n) → transRows addRow2 M ≡ addRows M
  addRowsEq M t zero = firstRowStayInvariant M (~ t)
  addRowsEq M t one j = M zero j + M one j
  addRowsEq M t (suc (suc i)) j = takeCombShufRows addRow2 (λ N → addRowsEq N t) M (suc (suc i)) j

  isLinearAddRows : isLinear (addRows {m = m} {n = suc n})
  isLinearAddRows =
    let isLinear = isLinearTransRows _ isLinear2AddRow2 _
    in  record
          { transMat = isLinear .transMat
          ; transEq  = (λ M → sym (addRowsEq M) ∙ isLinear .transEq M) }

  isInvAddRows : (M : Mat (suc m) (suc n)) → isInv (isLinearAddRows .transMat M)
  isInvAddRows = isInvTransRows _ _ (λ _ → isInvAddMat2)

-- Similarity defined by adding rows

  record AddFirstRow (M : Mat (suc m) (suc n)) : Type ℓ where
    field
      sim : Sim M
      inv₀  : M zero ≡ sim .result zero
      addEq : (i : Fin m)(j : Fin (suc n)) → M zero j + M (suc i) j ≡ sim .result (suc i) j

  open AddFirstRow

  addFirstRow : (M : Mat (suc m) (suc n)) → AddFirstRow M
  addFirstRow M .sim .result    = addRows M
  addFirstRow M .sim .simrel .transMatL = isLinearAddRows .transMat M
  addFirstRow M .sim .simrel .transMatR = 𝟙
  addFirstRow M .sim .simrel .transEq     = isLinearAddRows .transEq _ ∙ sym (⋆rUnit _)
  addFirstRow M .sim .simrel .isInvTransL = isInvAddRows M
  addFirstRow M .sim .simrel .isInvTransR = isInv𝟙
  addFirstRow M .inv₀      = refl
  addFirstRow M .addEq i j = refl


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

open import lib.Basics
open import lib.types.Coproduct
open import lib.types.Paths
open import lib.types.Pointed
open import lib.types.Pushout
open import lib.types.PushoutFlattening
open import lib.types.Span
open import lib.types.Unit

-- Wedge of two pointed types is defined as a particular case of pushout

module lib.types.Wedge where

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  wedge-span : Span
  wedge-span = span (fst X) (fst Y) Unit (λ _ → snd X) (λ _ → snd Y)

  Wedge : Type (lmax i j)
  Wedge = Pushout wedge-span

  infix 80 _∨_
  _∨_ = Wedge

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  winl : fst X → X ∨ Y
  winl x = left x

  winr : fst Y → X ∨ Y
  winr y = right y

  wglue : winl (snd X) == winr (snd Y)
  wglue = glue tt

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  ⊙Wedge : Ptd (lmax i j)
  ⊙Wedge = ⊙[ Wedge X Y , winl (snd X) ]

  infix 80 _⊙∨_
  _⊙∨_ = ⊙Wedge

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  ⊙winl : fst (X ⊙→ X ⊙∨ Y)
  ⊙winl = (winl , idp)

  ⊙winr : fst (Y ⊙→ X ⊙∨ Y)
  ⊙winr = (winr , ! wglue)

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  module WedgeElim {k} {P : X ∨ Y → Type k}
    (winl* : (x : fst X) → P (winl x)) (winr* : (y : fst Y) → P (winr y))
    (wglue* : winl* (snd X) == winr* (snd Y) [ P ↓ wglue ]) where

    private
      module M = PushoutElim winl* winr* (λ _ → wglue*)

    f = M.f
    glue-β = M.glue-β unit

  open WedgeElim public using () renaming (f to Wedge-elim)

  module WedgeRec {k} {C : Type k} (winl* : fst X → C) (winr* : fst Y → C)
    (wglue* : winl* (snd X) == winr* (snd Y)) where

    private
      module M = PushoutRec {d = wedge-span X Y} winl* winr* (λ _ → wglue*)

    f = M.f
    glue-β = M.glue-β unit

add-wglue : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → fst (X ⊙⊔ Y) → X ∨ Y
add-wglue (inl x) = winl x
add-wglue (inr y) = winr y

⊙add-wglue : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → fst (X ⊙⊔ Y ⊙→ X ⊙∨ Y)
⊙add-wglue = (add-wglue , idp)

module ⊙WedgeRec {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : fst (X ⊙→ Z)) (h : fst (Y ⊙→ Z)) where

  open WedgeRec (fst g) (fst h) (snd g ∙ ! (snd h)) public

  ⊙f : fst (X ⊙∨ Y ⊙→ Z)
  ⊙f = (f , snd g)

  ⊙winl-β : ⊙f ⊙∘ ⊙winl == g
  ⊙winl-β = idp

  ⊙winr-β : ⊙f ⊙∘ ⊙winr == h
  ⊙winr-β = ⊙λ= (λ _ → idp) $
    ap (λ w → w ∙ snd g)
       (ap-! f wglue ∙ ap ! glue-β ∙ !-∙ (snd g) (! (snd h)))
    ∙ ∙-assoc (! (! (snd h))) (! (snd g)) (snd g)
    ∙ ap (λ w → ! (! (snd h)) ∙ w) (!-inv-l (snd g))
    ∙ ∙-unit-r (! (! (snd h)))
    ∙ !-! (snd h)

⊙wedge-rec = ⊙WedgeRec.⊙f

⊙wedge-rec-post∘ : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (k : fst (Z ⊙→ W)) (g : fst (X ⊙→ Z)) (h : fst (Y ⊙→ Z))
  → k ⊙∘ ⊙wedge-rec g h == ⊙wedge-rec (k ⊙∘ g) (k ⊙∘ h)
⊙wedge-rec-post∘ k g h = ⊙λ=
  (Wedge-elim (λ _ → idp) (λ _ → idp)
    (↓-='-in $ ⊙WedgeRec.glue-β (k ⊙∘ g) (k ⊙∘ h)
               ∙ lemma (fst k) (snd g) (snd h) (snd k)
               ∙ ! (ap (ap (fst k)) (⊙WedgeRec.glue-β g h))
               ∙ ∘-ap (fst k) (fst (⊙wedge-rec g h)) wglue))
  idp
  where
  lemma : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {x y z : A} {w : B}
    (p : x == z) (q : y == z) (r : f z == w)
    → (ap f p ∙ r) ∙ ! (ap f q ∙ r) == ap f (p ∙ ! q)
  lemma f idp idp idp = idp

⊙wedge-rec-η : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → ⊙wedge-rec ⊙winl ⊙winr == ⊙idf (X ⊙∨ Y)
⊙wedge-rec-η = ⊙λ=
  (Wedge-elim (λ _ → idp) (λ _ → idp)
    (↓-='-in $ ap-idf wglue
               ∙ ! (!-! wglue)
               ∙ ! (⊙WedgeRec.glue-β ⊙winl ⊙winr)))
  idp

module Fold {i} {X : Ptd i} = ⊙WedgeRec (⊙idf X) (⊙idf X)
fold = Fold.f
⊙fold = Fold.⊙f

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  module Projl = ⊙WedgeRec (⊙idf X) (⊙cst {X = Y})
  module Projr = ⊙WedgeRec (⊙cst {X = X}) (⊙idf Y)

  projl = Projl.f
  projr = Projr.f
  ⊙projl = Projl.⊙f
  ⊙projr = Projr.⊙f

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Categories
open import Monads

module Monads.Kleisli.Adjunction {a b}{C : Cat {a}{b}}(M : Monad C) where

open Cat C
open Monad M

open import Library
open import Functors
open import Monads.Kleisli M
open import Adjunctions
open import Monads.Kleisli.Functors M
open Fun

KlAdj : Adj C Kl
KlAdj = record {
  L        = KlL;
  R        = KlR;
  left     = id;
  right    = id;
  lawa     = λ _ → refl;
  lawb     = λ _ → refl;
  natleft  = lem;
  natright = lem}
  where
   lem = λ {X}{X'}{Y}{Y'} (f : Hom X' X)(g : Hom Y (T Y')) h →
    proof
    comp (bind g) (comp h f)
    ≅⟨ cong (λ h → comp (bind g) (comp h f)) (sym law2) ⟩
    comp (bind g) (comp (comp (bind h) η) f)
    ≅⟨ cong (comp (bind g)) ass ⟩
    comp (bind g) (comp (bind h) (comp η f))
    ∎

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
------------------------------------------------------------------------------
-- Conversion rules for the Collatz function
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.Collatz.ConversionRulesATP where

open import FOT.FOTC.Program.Collatz.CollatzConditionals

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Program.Collatz.Data.Nat

------------------------------------------------------------------------------
-- Conversion rules for the Collatz function.
postulate
  collatz-0       : collatz 0' ≡ 1'
  collatz-1       : collatz 1' ≡ 1'
  collatz-even    : ∀ {n} → Even (succ₁ (succ₁ n)) →
                    collatz (succ₁ (succ₁ n)) ≡
                    collatz (div (succ₁ (succ₁ n)) 2')
  collatz-noteven : ∀ {n} → NotEven (succ₁ (succ₁ n)) →
                    collatz (succ₁ (succ₁ n)) ≡
                    collatz (3' * (succ₁ (succ₁ n)) + 1')
{-# ATP prove collatz-0 #-}
{-# ATP prove collatz-1 #-}
{-# ATP prove collatz-even #-}
{-# ATP prove collatz-noteven #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Untyped.Main where

open import Function

open import Data.Nat
open import Data.Unit
open import Data.Product
open import Data.List
open import Data.Sum
open import Category.Monad

open import Strict

open import Untyped.Monads
open import Untyped.Abstract

open M

-- the monad in which we interpret expressions into command trees
M : Set → Set
M = ReaderT Env (Free Cmd ⟦_⟧)

record ServerState : Set where
  constructor server
  field
    threads : ThreadPool
    nextChan : ℕ
    links   : List ℕ
    queues  : List (List Val)

empty : ServerState
empty = record { threads = []; links = []; queues = []; nextChan = 0 }

SchedM : Set → Set
SchedM = StateT ServerState id

SchedM? : Set → Set
SchedM? = ExceptT Blocked (StateT ServerState id)

instance
  free-monad' = free-monad

  {- The monad that interprets expressions into threads -}
  m-monad : RawMonad M
  m-monad = reader-monad Env (Free Cmd ⟦_⟧) ⦃ free-monad ⦄

  m-reader : MonadReader M Env
  m-reader = record
    { ask   = Free.pure
    ; local = λ f c E → c (f E) }

  m-comm : MonadComm M Chan Val
  m-comm = record
    { recv = λ c E   → impure (inj₁ (Comm.recv c)) Free.pure
    ; send = λ c v E → impure (inj₁ (Comm.send c v)) Free.pure
    ; close = λ c E  → impure (inj₁ (Comm.clos c)) Free.pure }

  m-res  : MonadResumption M Closure Chan
  m-res  = record
    { yield = λ _      → impure (inj₂ Threading.yield) Free.pure
    ; fork  = λ clos _ → impure (inj₂ (Threading.fork clos)) Free.pure }

  {- The monad that executes threads -}

  s-monad : RawMonad SchedM
  s-monad = state-monad ServerState id ⦃ id-monad ⦄

  s-state : MonadState SchedM ServerState
  s-state = state-monad-state ServerState id ⦃ id-monad ⦄

  s-thread-state : MonadState SchedM ThreadPool
  s-thread-state = focus-monad-state
    ServerState.threads
    (λ thr s → record s { threads = thr })
    s-state

  s-writer : MonadWriter SchedM ThreadPool
  s-writer = record
    { write = λ pool → do
            modify λ st → record st { threads = ServerState.threads st ++ pool }
            return tt
    }

  s?-monad : RawMonad SchedM?
  s?-monad = except-monad

  s?-monad-except : MonadExcept SchedM? Blocked
  s?-monad-except = except-monad-except

newChan : SchedM (Chan × Chan)
newChan = do
  c ← gets ServerState.nextChan
  let left  = c
  let right = c + 1
  modify (λ st → record st
    { nextChan = c + 2
    ; links   = ServerState.links st ++ (right ∷ left ∷ [])
    ; queues  = ServerState.queues st ++ ([] ∷ [] ∷ []) })
  return (left , right)

instance
  s-comm : MonadComm SchedM? ℕ Val
  s-comm = record
    { recv  = λ ch → do
                queue ← gets (unsafeLookup ch ∘ ServerState.queues)
                case queue of λ where
                  []       → throw blocked
                  (x ∷ xs) → do
                    modify λ st →
                      (record st { queues = unsafeUpdate ch (ServerState.queues st) xs})
                    return x
    ; send  = λ ch v → do
                ch⁻¹  ← gets (unsafeLookup ch ∘ ServerState.links)
                queue ← gets (unsafeLookup ch⁻¹ ∘ ServerState.queues)
                modify λ st →
                  record st { queues = unsafeUpdate ch⁻¹ (ServerState.queues st) (queue ∷ʳ v) }
                return tt
    ; close = λ ch → do
                return tt
    }

  s-res : MonadResumption SchedM? Closure Chan
  s-res = record
    { yield = return tt
    ; fork  = λ where
      ⟨ env ⊢ e ⟩ →
        do
          (l , r) ← newChan
          schedule [ thread $ eval ⦃ m-monad ⦄ e (extend (chan l) env) ]
          return r
    }

handler : (c : Cmd) → Cont Cmd ⟦_⟧ c Val → SchedM ⊤
handler c k s =
  let (s' , r) = handle {SchedM?} c s in
  case r of λ where
    (exc e) → schedule [ thread (impure c k) ] s' -- reschedule
    (✓ v)   → schedule [ thread (k v) ] s'

atomic : Thread → SchedM ⊤
atomic (thread (Free.pure x))  = return tt
atomic (thread (impure cmd x)) = handler cmd x

run : Exp → ℕ
run e =
  let
    main = thread $ eval e []
    (s , v) = robin ⦃ s-monad ⦄ atomic (record empty { threads = [ main ]})
  in case (ServerState.threads s) of λ where
    [] → 0
    _  → 1

example : Exp
example =
  let
    slave  = ƛ (Exp.send (var 0) (nat 3))
    master = Exp.receive (Exp.fork slave)
  in master

import IO

main = do
  let val = run example
  case val of λ where
    0 → IO.run (IO.putStrLn "done!")
    _ → IO.run (IO.putStrLn "?!")


text:
module _ where

data Sigma (A : Set)(B : A → Set) : Set where
  _,_ : (x : A) → B x → Sigma A B

record Top : Set where

_o_ : {A B : Set}{C : Set1} →
      (f : B → C) → (g : A → B) → (A → C)
f o g = \ x → f (g x)

mutual
  data U  : Set where
    top : U
    sig : (X : U) → (T X → U) → U

  T : U → Set
  T top = Top
  T (sig a b) = Sigma (T a) (T o b)

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Agda.Builtin.IO
open import Agda.Builtin.Unit

record Box (A : Set) : Set where
  field
    unbox : A

open Box public

record R : Set where
  coinductive
  field
    force : Box R

open R public

r : R
unbox (force r) = r

postulate
  seq    : {A B : Set} → A → B → B
  return : {A : Set} → A → IO A

{-# COMPILE GHC return = \_   -> return #-}
{-# COMPILE GHC seq    = \_ _ -> seq    #-}

main : IO ⊤
main = seq r (return tt)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Selective.Examples.ChatAO where

open import Selective.ActorMonad
open import Selective.Libraries.Channel
open import Selective.Libraries.Call2
open import Selective.Libraries.ActiveObjects
open import Prelude
  hiding (Maybe)
open import Data.Maybe as Maybe
  hiding (map)

open import Data.List.Properties
open import Category.Monad

open import Debug
open import Data.Nat.Show using (show)

RoomName = ℕ
ClientName = ℕ

Room-to-Client : InboxShape

record Client : Set where
  field
    name : ClientName
    channel : UniqueTag

ClientList : Set
ClientList = List Client

record RoomState : Set₁ where
  field
    clients : ClientList

cl-to-context : ClientList → TypingContext
cl-to-context = map λ _ → Room-to-Client

rs-to-context : RoomState → TypingContext
rs-to-context rs = let open RoomState
  in cl-to-context (rs .clients)

record ChatMessageContent : Set where
  constructor chat-from_message:_
  field
    sender : ClientName
    message : String

SendChatMessage : MessageType
SendChatMessage = [ ValueType ChatMessageContent ]ˡ

ReceiveChatMessage : MessageType
ReceiveChatMessage = ValueType UniqueTag ∷ [ ValueType ChatMessageContent ]ˡ

chat-message-header : ActiveMethod
chat-message-header = VoidMethod [ SendChatMessage ]ˡ

Room-to-Client = [ ReceiveChatMessage ]ˡ

AddToRoom : MessageType
AddToRoom = ValueType UniqueTag ∷ ValueType ClientName ∷ [ ReferenceType Room-to-Client ]ˡ

add-to-room-header : ActiveMethod
add-to-room-header = VoidMethod [ AddToRoom ]ˡ

LeaveRoom : MessageType
LeaveRoom = [ ValueType ClientName ]ˡ

leave-room-header : ActiveMethod
leave-room-header = VoidMethod [ LeaveRoom ]ˡ

room-methods : List ActiveMethod
room-methods = chat-message-header ∷ leave-room-header ∷ [ add-to-room-header ]ˡ

room-inbox = methods-shape room-methods

add-to-room : (active-method room-inbox RoomState rs-to-context add-to-room-header)
add-to-room _ (Msg Z (tag ∷ client-name ∷ _ ∷ [])) state = do
  let
    open RoomState
    state' = record { clients = record { name = client-name ; channel = tag } ∷ state .clients }
  strengthen (Z ∷ ⊆-refl)
  return₁ state'
add-to-room _ (Msg (S ()) _)

record RoomLeave (rs : ClientList) (name : ClientName) : Set₁ where
  field
    filtered : ClientList
    subs : (cl-to-context filtered) ⊆ (cl-to-context rs)

leave-room : (active-method room-inbox RoomState rs-to-context leave-room-header)
leave-room _ (Msg Z (client-name ∷ [])) state = do
    let
      open RoomState
      open RoomLeave
      rl = remove-first-client (state .clients) client-name
      state' = record { clients = rl .filtered }
    debug ("client#" || show client-name || " left the room") (strengthen (rl .subs))
    return₁ state'
  where
    remove-first-client : (cl : ClientList) → (name : ClientName) → RoomLeave cl name
    remove-first-client [] name = record { filtered = [] ; subs = [] }
    remove-first-client (x ∷ cl) name with ((Client.name x) ≟ name)
    ... | (yes _) = record { filtered = cl ; subs = ⊆-suc ⊆-refl }
    ... | (no _) =
      let
        rec = remove-first-client cl name
        open RoomLeave
      in record { filtered = x ∷ rec .filtered ; subs = Z ∷ ⊆-suc (rec .subs) }
leave-room _ (Msg (S ()) _) _

chat-message : (active-method room-inbox RoomState rs-to-context chat-message-header)
chat-message _ (Msg Z ((chat-from sender message: message) ∷ [])) state = do
    let
      open RoomState
      debug-msg = ("room sending " || show (pred (length (state .clients))) ||  " messages from " || show sender || ": " || message)
    debug debug-msg (send-to-others (state .clients) sender message)
    return₁ state
  where
    ++-temp-fix : (l r : ClientList) → (x : Client) → (l ++ (x ∷ r)) ≡ ((l ∷ʳ x) ++ r)
    ++-temp-fix [] r x = refl
    ++-temp-fix (x₁ ∷ l) r x = cong (_∷_ x₁) (++-temp-fix l r x)
    send-to-others : ∀ {i} → (cl : ClientList) →
                     ClientName →
                     String →
                     ∞ActorM i room-inbox ⊤₁ (cl-to-context cl) (λ _ → cl-to-context cl)
    send-to-others [] _ _ = return _
    send-to-others cl@(_ ∷ _) name message = send-loop [] cl
      where
        build-pointer : (l r : ClientList) →
                      cl-to-context r ⊢ Room-to-Client →
                      (cl-to-context (l ++ r)) ⊢ Room-to-Client
        build-pointer [] r p = p
        build-pointer (x ∷ l) r p = S (build-pointer l r p)
        recurse : ∀ {i} → (l r : ClientList) → (x : Client) →
                  ∞ActorM i room-inbox ⊤₁ (cl-to-context (l ++ (x ∷ r))) (λ _ → (cl-to-context (l ++ (x ∷ r))))
        send-loop : ∀ {i} → (l r : ClientList) →
          ∞ActorM i room-inbox ⊤₁ (cl-to-context (l ++ r)) (λ _ → cl-to-context (l ++ r))
        send-loop l [] = return _
        send-loop l (x ∷ r) with ((Client.name x) ≟ name)
        ... | (yes _) = recurse l r x
        ... | (no _) = let p = build-pointer l (x ∷ r) Z
          in debug ("Sending to " || show (Client.name x) || ": " || message) (p ![t: Z ] (lift (Client.channel x) ∷ [ lift (chat-from name message: message) ]ᵃ) ) >> recurse l r x
        recurse l r x rewrite ++-temp-fix l r x = send-loop (l ∷ʳ x) r
chat-message _ (Msg (S ()) _) _

room : ActiveObject
room = record {
  state-type = RoomState
  ; vars = rs-to-context
  ; methods = room-methods
  ; extra-messages = []
  ; handlers = chat-message ∷ leave-room ∷ [ add-to-room ]ᵃ
  }

Client-to-Room : InboxShape
Client-to-Room = SendChatMessage ∷ [ LeaveRoom ]ˡ

-- =============
--  JOIN ROOM
-- =============

data JoinRoomSuccess : Set where
  JR-SUCCESS : RoomName → JoinRoomSuccess

data JoinRoomFail : Set where
  JR-FAIL : RoomName → JoinRoomFail

data JoinRoomStatus : Set where
  JRS-SUCCESS JRS-FAIL : RoomName → JoinRoomStatus

JoinRoomSuccessReply : MessageType
JoinRoomSuccessReply = ValueType UniqueTag ∷ ValueType JoinRoomSuccess ∷ [ ReferenceType Client-to-Room ]ˡ

JoinRoomFailReply : MessageType
JoinRoomFailReply = ValueType UniqueTag ∷ [ ValueType JoinRoomFail ]ˡ

JoinRoomReplyInterface : InboxShape
JoinRoomReplyInterface = JoinRoomSuccessReply ∷ JoinRoomFailReply ∷ Room-to-Client

JoinRoom : MessageType
JoinRoom = ValueType UniqueTag ∷ ReferenceType JoinRoomReplyInterface ∷ ValueType RoomName ∷ [ ValueType ClientName ]ˡ

-- =============
--  CREATE ROOM
-- =============

data CreateRoomResult : Set where
  CR-SUCCESS CR-EXISTS : RoomName → CreateRoomResult

CreateRoomReply : MessageType
CreateRoomReply = ValueType UniqueTag ∷ [ ValueType CreateRoomResult ]ˡ

CreateRoom : MessageType
CreateRoom = ValueType UniqueTag ∷ ReferenceType [ CreateRoomReply ]ˡ ∷ [ ValueType RoomName ]ˡ

-- ============
--  LIST ROOMS
-- ============

RoomList : Set
RoomList = List RoomName

ListRoomsReply : MessageType
ListRoomsReply = ValueType UniqueTag ∷ [ ValueType RoomList ]ˡ

ListRooms : MessageType
ListRooms = ValueType UniqueTag ∷ [ ReferenceType [ ListRoomsReply ]ˡ ]ˡ

-- ===
--
-- ===

Client-to-RoomManager : InboxShape
Client-to-RoomManager = JoinRoom ∷ CreateRoom ∷ [ ListRooms ]ˡ

RoomManagerInterface : InboxShape
RoomManagerInterface = Client-to-RoomManager

GetRoomManagerReply : MessageType
GetRoomManagerReply = ValueType UniqueTag ∷ [ ReferenceType RoomManagerInterface ]ˡ

GetRoomManager : MessageType
GetRoomManager = ValueType UniqueTag ∷ [ ReferenceType [ GetRoomManagerReply ]ˡ ]ˡ

get-room-manager-ci : ChannelInitiation
get-room-manager-ci = record {
  request = [ GetRoomManager ]ˡ
  ; response = record {
    channel-shape = [ GetRoomManagerReply ]ˡ
    ; all-tagged = (HasTag _) ∷ [] }
  ; request-tagged = (HasTag+Ref _) ∷ []
  }

get-room-manager-header : ActiveMethod
get-room-manager-header = ResponseMethod get-room-manager-ci

RoomSupervisorInterface : InboxShape
RoomSupervisorInterface = [ GetRoomManager ]ˡ

ClientSupervisorInterface : InboxShape
ClientSupervisorInterface =
  [ ReferenceType RoomSupervisorInterface ]ˡ ∷ [ GetRoomManagerReply ]ˡ

--
--
--

-- ======================
--  ROOM MANAGER METHODS
-- ======================

join-room-header : ActiveMethod
join-room-header = VoidMethod [ JoinRoom ]ˡ

create-room-ci : ChannelInitiation
create-room-ci = record {
  request = [ CreateRoom ]ˡ
  ; response = record {
    channel-shape = [ CreateRoomReply ]ˡ
    ; all-tagged = (HasTag _) ∷ [] }
  ; request-tagged = (HasTag+Ref _) ∷ []
  }

create-room-header : ActiveMethod
create-room-header = ResponseMethod create-room-ci

list-rooms-header : ActiveMethod
list-rooms-header = ResponseMethod (record {
  request = [ ListRooms ]ˡ
  ; response = record {
    channel-shape = [ ListRoomsReply ]ˡ
    ; all-tagged = (HasTag _) ∷ []
    }
  ; request-tagged = (HasTag+Ref _) ∷ []
  })

record RoomManagerState : Set₁ where
  field
    rooms : RoomList

rms-to-context : RoomManagerState → TypingContext
rms-to-context rms =
  let
    open RoomManagerState
    rl-to-context : RoomList → TypingContext
    rl-to-context = map λ _ → room-inbox
  in rl-to-context (rms .rooms)

room-manager-methods : List ActiveMethod
room-manager-methods = join-room-header ∷ create-room-header ∷ [ list-rooms-header ]ˡ

room-manager-inbox = methods-shape room-manager-methods

list-rooms : active-method room-manager-inbox RoomManagerState rms-to-context list-rooms-header
list-rooms _ msg state =
  let
    open RoomManagerState
  in return₁ (record {
    new-state = state
    ; reply = SendM Z ((lift (state .rooms)) ∷ [])
    })

lookup-room : ∀ {i} → {Γ : TypingContext} →
              (rms : RoomManagerState) →
              RoomName →
              ∞ActorM i room-manager-inbox (Maybe ((Γ ++ (rms-to-context rms)) ⊢ room-inbox)) (Γ ++ (rms-to-context rms)) (λ _ → Γ ++ (rms-to-context rms))
lookup-room rms name =
    let open RoomManagerState
    in return₁ (loop _ (rms .rooms))
    where
      rl-to-context : RoomList → TypingContext
      rl-to-context = map λ _ → room-inbox
      loop : (Γ : TypingContext) → (rl : RoomList) → Maybe ((Γ ++ rl-to-context rl) ⊢ room-inbox)
      loop [] [] = nothing
      loop [] (x ∷ xs) with (x ≟ name)
      ... | (yes p) = just Z
      ... | (no _) = RawMonad._>>=_ Maybe.monad (loop [] xs) λ p → just (S p)
      loop (x ∷ Γ) rl = RawMonad._>>=_ Maybe.monad (loop Γ rl) (λ p → just (S p))

create-room : active-method room-manager-inbox RoomManagerState rms-to-context create-room-header
create-room _ input@(_ sent Msg Z (room-name ∷ [])) state = do
    p ← lookup-room state room-name
    handle-create-room p
  where
    open ResponseInput
    return-type = ActiveReply create-room-ci RoomManagerState rms-to-context input
    precondition = reply-state-vars rms-to-context input state
    postcondition = reply-vars rms-to-context input
    handle-create-room : ∀ {i} → Maybe (precondition ⊢ room-inbox) →
                         ∞ActorM i
                           room-manager-inbox
                           return-type
                           precondition
                           postcondition
    handle-create-room (just x) = return₁ (record { new-state = state ; reply = SendM Z ((lift (CR-EXISTS room-name)) ∷ []) })
    handle-create-room nothing = do
      spawn∞ (run-active-object room (record { clients = [] }))
      let
        open RoomManagerState
        state' : RoomManagerState
        state' = record { rooms = room-name ∷ state .rooms}
      strengthen ((S Z) ∷ (Z ∷ (⊆-suc (⊆-suc ⊆-refl))))
      return₁ (record { new-state = state' ; reply = SendM Z ((lift (CR-SUCCESS room-name)) ∷ []) })
create-room _ (_ sent Msg (S ()) _) _

join-room : active-method room-manager-inbox RoomManagerState rms-to-context join-room-header
join-room _ (Msg Z (tag ∷ _ ∷ room-name ∷ client-name ∷ [])) state = do
    p ← lookup-room state room-name
    handle-join-room p Z
    return₁ state
  where
    handle-join-room : ∀ {i Γ} → Maybe (Γ ⊢ room-inbox) → Γ ⊢ JoinRoomReplyInterface → ∞ActorM i room-manager-inbox ⊤₁ Γ (λ _ → Γ)
    handle-join-room (just rp) cp = do
      (rp ![t: S (S Z) ] ((lift tag) ∷ ((lift client-name) ∷ (([ cp ]>: [ S (S Z) ]ᵐ) ∷ []))))
      (cp ![t: Z ] ((lift tag) ∷ ((lift (JR-SUCCESS room-name)) ∷ (([ rp ]>: (Z ∷ [ S Z ]ᵐ)) ∷ []))))
    handle-join-room nothing cp = cp ![t: S Z ] ((lift tag) ∷ ((lift (JR-FAIL room-name)) ∷ []))
join-room _ (Msg (S ()) _) _

room-manager : ActiveObject
room-manager = record {
  state-type = RoomManagerState
  ; vars = rms-to-context
  ; methods = room-manager-methods
  ; extra-messages = []
  ; handlers = join-room ∷ (create-room ∷ (list-rooms ∷ []))
  }

-- =================
--  ROOM SUPERVISOR
-- =================

rs-context : TypingContext
rs-context = [ room-manager-inbox ]ˡ

rs-vars : ⊤₁ → TypingContext
rs-vars _ = rs-context

room-supervisor-methods : List ActiveMethod
room-supervisor-methods = [ get-room-manager-header ]ˡ

rs-inbox = methods-shape room-supervisor-methods

get-room-manager-handler : active-method rs-inbox ⊤₁ rs-vars get-room-manager-header
get-room-manager-handler _ (_ sent Msg Z received-fields) _ = return₁ (record { new-state = _ ; reply = SendM Z [ [ (S Z) ]>: ⊆-refl ]ᵃ })
get-room-manager-handler _ (_ sent Msg (S ()) _) _

room-supervisor-ao : ActiveObject
room-supervisor-ao = record
                       { state-type = ⊤₁
                       ; vars = λ _ → rs-context
                       ; methods = room-supervisor-methods
                       ; extra-messages = []
                       ; handlers = [ get-room-manager-handler ]ᵃ
                       }

-- room-supervisor spawns the room-manager
-- and provides an interface for getting a reference to the current room-manager
-- we don't ever change that instance, but we could if we want
room-supervisor : ∀ {i} → ActorM i RoomSupervisorInterface ⊤₁ [] (λ _ → rs-context)
room-supervisor = begin do
    spawn∞ (run-active-object room-manager (record { rooms = [] }))
    run-active-object room-supervisor-ao _

-- ================
--  CLIENT GENERAL
-- ================
ClientInterface : InboxShape
ClientInterface = [ ReferenceType RoomManagerInterface ]ˡ ∷ CreateRoomReply ∷ ListRoomsReply ∷ JoinRoomReplyInterface

busy-wait : ∀ {i IS Γ} → ℕ → ∞ActorM i IS ⊤₁ Γ (λ _ → Γ)
busy-wait zero = return _
busy-wait (suc n) = return tt >> busy-wait n

client-get-room-manager : ∀ {i} → ∞ActorM i ClientInterface ⊤₁ [] (λ _ → [ RoomManagerInterface ]ˡ)
client-get-room-manager = do
  record { msg = Msg Z _} ← (selective-receive (λ {
    (Msg Z x₁) → true
    ; (Msg (S _) _) → false
    }))
    where
      record { msg = (Msg (S _) _) ; msg-ok = ()}
  return _

client-create-room : ∀ {i } →
                     {Γ : TypingContext} →
                     Γ ⊢ RoomManagerInterface →
                     UniqueTag →
                     RoomName →
                     ∞ActorM i ClientInterface (Lift (lsuc lzero) CreateRoomResult) Γ (λ _ → Γ)
client-create-room p tag name = do
  Msg Z (_ ∷ cr ∷ []) ← (call create-room-ci (record {
    var = p
    ; chosen-field = Z
    ; fields = (lift name) ∷ []
    ; session = record {
      can-request = (S Z) ∷ []
      ; response-session = record {
      can-receive = (S Z) ∷ []
      ; tag = tag
      }
      }
      }))
    where
      Msg (S ()) _
  return cr

add-if-join-success : TypingContext →
                      Lift (lsuc lzero) JoinRoomStatus →
                      TypingContext
add-if-join-success Γ (lift (JRS-SUCCESS x)) = Client-to-Room ∷ Γ
add-if-join-success Γ (lift (JRS-FAIL x)) = Γ

client-join-room : ∀ {i Γ} →
                   Γ ⊢ RoomManagerInterface →
                   UniqueTag →
                   RoomName →
                   ClientName →
                   ∞ActorM i ClientInterface (Lift (lsuc lzero) JoinRoomStatus) Γ (add-if-join-success Γ)
client-join-room p tag room-name client-name = do
    self
    S p ![t: Z ] (lift tag ∷ (([ Z ]>: ⊆-suc (⊆-suc (⊆-suc ⊆-refl))) ∷ (lift room-name) ∷ [ lift client-name ]ᵃ))
    (strengthen (⊆-suc ⊆-refl))
    m ← (selective-receive (select-join-reply tag))
    handle-message m
  where
    select-join-reply : UniqueTag → MessageFilter ClientInterface
    select-join-reply tag (Msg Z _) = false
    select-join-reply tag (Msg (S Z) _) = false
    select-join-reply tag (Msg (S (S Z)) _) = false
    select-join-reply tag (Msg (S (S (S Z))) (tag' ∷ _)) = ⌊ tag ≟ tag' ⌋
    select-join-reply tag (Msg (S (S (S (S Z)))) (tag' ∷ _)) = ⌊ tag ≟ tag' ⌋
    select-join-reply tag (Msg (S (S (S (S (S Z))))) x₁) = false
    select-join-reply tag (Msg (S (S (S (S (S (S ())))))) _)
    handle-message : ∀ {tag i Γ} → (m : SelectedMessage (select-join-reply tag)) →
                     ∞ActorM i ClientInterface (Lift (lsuc lzero) JoinRoomStatus)
                       (add-selected-references Γ m) (add-if-join-success Γ)
    handle-message record { msg = (Msg Z _) ; msg-ok = () }
    handle-message record { msg = (Msg (S Z) _) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S Z)) _) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S (S Z))) (_ ∷ JR-SUCCESS room-name ∷ _ ∷ [])) } = return (JRS-SUCCESS room-name)
    handle-message record { msg = (Msg (S (S (S (S Z)))) (_ ∷ JR-FAIL room-name ∷ [])) } = return (JRS-FAIL room-name)
    handle-message record { msg = (Msg (S (S (S (S (S Z))))) _) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S (S (S (S (S ())))))) _) }

client-send-message : ∀ {i  Γ} →
                      Γ ⊢ Client-to-Room →
                      ClientName →
                      String →
                      ∞ActorM i ClientInterface ⊤₁ Γ (λ _ → Γ)
client-send-message p client-name message = p ![t: Z ] ([ lift (chat-from client-name message: message) ]ᵃ)

client-receive-message : ∀ {i Γ} →
                         ∞ActorM i ClientInterface (Lift (lsuc lzero) ChatMessageContent) Γ (λ _ → Γ)
client-receive-message = do
    m ← (selective-receive select-message)
    handle-message m
  where
    select-message : MessageFilter ClientInterface
    select-message (Msg (S (S (S (S (S Z))))) _) = true
    select-message (Msg _ _) = false
    handle-message : ∀ {i Γ} → (m : SelectedMessage select-message) →
                     ∞ActorM i ClientInterface (Lift (lsuc lzero) ChatMessageContent) (add-selected-references Γ m) (λ _ → Γ)
    handle-message record { msg = (Msg Z _) ; msg-ok = () }
    handle-message record { msg = (Msg (S Z) _) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S Z)) _) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S (S Z))) x₁) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S (S (S Z)))) _) ; msg-ok = () }
    handle-message record { msg = (Msg (S (S (S (S (S Z))))) (_ ∷ m ∷ f)) ; msg-ok = _ } = return m
    handle-message record { msg = (Msg (S (S (S (S (S (S ())))))) _) }

client-leave-room : ∀ {i Γ} →
                    Γ ⊢ Client-to-Room →
                    ClientName →
                    ∞ActorM i ClientInterface ⊤₁ Γ (λ _ → Γ)
client-leave-room p name = p ![t: S Z ] [ lift name ]ᵃ

debug-chat : {a : Level} {A : Set a} → ClientName → ChatMessageContent → A → A
debug-chat client-name content = let open ChatMessageContent
  in debug ("client#" || show client-name || " received \"" || content .message || "\" from client#" || show (content .sender))

-- ==========
--  CLIENT 1
-- ==========

room1-2 = 1
room2-3 = 2
room3-1 = 3
room1-2-3 = 4
name1 = 1

client1 : ∀ {i} → ActorM i ClientInterface ⊤₁ [] (λ _ → [])
client1 = begin do
  client-get-room-manager
  _ ← (client-create-room Z 0 room1-2)
  _ ← (client-create-room Z 1 room3-1)
  _ ← (client-create-room Z 2 room1-2-3)
  lift (JRS-SUCCESS joined-room) ← (client-join-room Z 3 room3-1 name1)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  lift (JRS-SUCCESS joined-room) ← (client-join-room (S Z) 4 room1-2 name1)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  lift (JRS-SUCCESS joined-room) ← (client-join-room (S (S Z)) 5 room1-2-3 name1)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  busy-wait 100
  (client-send-message (S Z) name1 "hi from 1 to 2")
  (client-send-message Z name1 "hi from 1 to 2-3")
  let open ChatMessageContent
  lift m1 ← client-receive-message
  lift m2 ← debug-chat name1 m1 client-receive-message
  lift m3 ← debug-chat name1 m2 client-receive-message
  debug-chat name1 m3 (client-send-message Z name1 "hi1 from 1 to 2-3")
  (client-send-message Z name1 "hi2 from 1 to 2-3")
  (client-send-message Z name1 "hi3 from 1 to 2-3")
  client-leave-room (S Z) name1
  client-leave-room (Z) name1
  (strengthen [])

-- ==========
--  CLIENT 2
-- ==========

name2 = 2

client2 : ∀ {i} → ActorM i ClientInterface ⊤₁ [] (λ _ → [])
client2 = begin do
  client-get-room-manager
  _ ← (client-create-room Z 0 room1-2)
  _ ← (client-create-room Z 1 room2-3)
  _ ← (client-create-room Z 2 room1-2-3)
  lift (JRS-SUCCESS joined-room) ← (client-join-room Z 3 room1-2 name2)
    where
    (lift (JRS-FAIL failed-room)) → strengthen []
  lift (JRS-SUCCESS joined-room) ← (client-join-room (S Z) 4 room2-3 name2)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  lift (JRS-SUCCESS joined-room) ← (client-join-room (S (S Z)) 5 room1-2-3 name2)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  busy-wait 100
  debug "client2 send message" (client-send-message (S Z) name2 "hi from 2 to 3")
  debug "client2 send message" (client-send-message Z name2 "hi from 2 to 1-3")
  let open ChatMessageContent
  lift m1 ← client-receive-message
  lift m2 ← debug-chat name2 m1 client-receive-message
  lift m3 ← debug-chat name2 m2 client-receive-message
  client-leave-room (S Z) name2
  client-leave-room (Z) name2
  debug-chat name2 m3 (strengthen [])

-- ==========
--  CLIENT 3
-- ==========

name3 = 3

client3 : ∀ {i} → ActorM i ClientInterface ⊤₁ [] (λ _ → [])
client3 = begin do
  client-get-room-manager
  _ ← (client-create-room Z 0 room2-3)
  _ ← (client-create-room Z 1 room3-1)
  _ ← (client-create-room Z 2 room1-2-3)
  lift (JRS-SUCCESS joined-room) ← (client-join-room Z 3 room2-3 name3)
    where
    (lift (JRS-FAIL failed-room)) → strengthen []
  lift (JRS-SUCCESS joined-room) ← (client-join-room (S Z) 4 room3-1 name3)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  lift (JRS-SUCCESS joined-room) ← (client-join-room (S (S Z)) 5 room1-2-3 name3)
    where
      (lift (JRS-FAIL failed-room)) → strengthen []
  busy-wait 100
  debug "client3 send message" (client-send-message (S Z) name3 "hi from 3 to 1")
  debug "client3 send message" (client-send-message Z name3 "hi from 3 to 1-2")
  let open ChatMessageContent
  lift m1 ← client-receive-message
  lift m2 ← debug-chat name3 m1 client-receive-message
  lift m3 ← debug-chat name3 m2 client-receive-message
  debug-chat name3 m3 (client-leave-room Z name3)
  client-leave-room (S Z) name3
  client-leave-room Z name3
  (strengthen [])

-- ===================
--  CLIENT SUPERVISOR
-- ===================

cs-context : TypingContext
cs-context = RoomManagerInterface ∷ RoomSupervisorInterface ∷ []

client-supervisor : ∀ {i} → ActorM i ClientSupervisorInterface ⊤₁ [] (λ _ → cs-context)
client-supervisor = begin do
    wait-for-room-supervisor
    (get-room-manager Z 0)
    spawn-clients
  where
    wait-for-room-supervisor : ∀ {i Γ} → ∞ActorM i ClientSupervisorInterface ⊤₁ Γ (λ _ → RoomSupervisorInterface ∷ Γ)
    wait-for-room-supervisor = do
      record { msg = Msg Z f } ← (selective-receive (λ {
        (Msg Z _) → true
        ; (Msg (S _) _) → false
        }))
        where
          record { msg = (Msg (S _) _) ; msg-ok = () }
      return _
    get-room-manager : ∀ {i Γ} →
                     Γ ⊢ RoomSupervisorInterface →
                     UniqueTag →
                      ∞ActorM i ClientSupervisorInterface ⊤₁ Γ (λ _ → RoomManagerInterface ∷ Γ)
    get-room-manager p tag = do
      Msg Z f ← (call get-room-manager-ci (record {
          var = p
          ; chosen-field = Z
          ; fields = []
          ; session = record {
            can-request = ⊆-refl
            ; response-session = record {
            can-receive = (S Z) ∷ []
            ; tag = tag }
            }
          }))
        where
          Msg (S ()) _
      return _
    spawn-clients : ∀ {i} → ∞ActorM i ClientSupervisorInterface ⊤₁ cs-context (λ _ → cs-context)
    spawn-clients = do
      spawn client1
      Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ
      (strengthen (⊆-suc ⊆-refl))
      (spawn client2)
      Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ
      (strengthen (⊆-suc ⊆-refl))
      (spawn client3)
      Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ
      (strengthen (⊆-suc ⊆-refl))

-- chat-supervisor is the top-most actor
-- it spawns and connects the ClientRegistry to the RoomRegistry
chat-supervisor : ∀ {i} → ∞ActorM i [] ⊤₁ [] (λ _ → [])
chat-supervisor = do
    spawn room-supervisor
    spawn client-supervisor
    Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ
    strengthen []

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
------------------------------------------------------------------------
-- Laws related to _∣_ and fail
------------------------------------------------------------------------

module TotalParserCombinators.Laws.AdditiveMonoid where

open import Algebra
open import Codata.Musical.Notation
import Data.List.Relation.Binary.BagAndSetEquality as Eq
open import Data.Product using (proj₁; proj₂)
open import Function

private
  module BagMonoid {k} {A : Set} =
    CommutativeMonoid (Eq.commutativeMonoid k A)

open import TotalParserCombinators.Derivative
open import TotalParserCombinators.Congruence
open import TotalParserCombinators.Parser

------------------------------------------------------------------------
-- _∣_ and fail form a commutative monoid

-- This monoid is idempotent if language equivalence is used.

commutative : ∀ {Tok R xs₁ xs₂}
              (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂) →
              p₁ ∣ p₂ ≅P p₂ ∣ p₁
commutative {xs₁ = xs₁} {xs₂} p₁ p₂ =
  BagMonoid.comm xs₁ xs₂ ∷ λ t → ♯ commutative (D t p₁) (D t p₂)

left-identity : ∀ {Tok R xs} (p : Parser Tok R xs) → fail ∣ p ≅P p
left-identity {xs = xs} p =
  proj₁ BagMonoid.identity xs ∷ λ t → ♯ left-identity (D t p)

right-identity : ∀ {Tok R xs} (p : Parser Tok R xs) → p ∣ fail ≅P p
right-identity {xs = xs} p =
  proj₂ BagMonoid.identity xs ∷ λ t → ♯ right-identity (D t p)

associative : ∀ {Tok R xs₁ xs₂ xs₃}
              (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂)
              (p₃ : Parser Tok R xs₃) →
              (p₁ ∣ p₂) ∣ p₃ ≅P p₁ ∣ (p₂ ∣ p₃)
associative {xs₁ = xs₁} p₁ p₂ p₃ =
  BagMonoid.assoc xs₁ _ _ ∷ λ t →
  ♯ associative (D t p₁) (D t p₂) (D t p₃)

-- Note that this law uses language equivalence, not parser
-- equivalence.

idempotent : ∀ {Tok R xs} (p : Parser Tok R xs) → p ∣ p ≈P p
idempotent {xs = xs} p =
  Eq.++-idempotent xs ∷ λ t → ♯ idempotent (D t p)

------------------------------------------------------------------------
-- A lemma which can be convenient when proving distributivity laws

swap : ∀ {Tok R xs₁ xs₂ xs₃ xs₄}
       (p₁ : Parser Tok R xs₁) (p₂ : Parser Tok R xs₂)
       (p₃ : Parser Tok R xs₃) (p₄ : Parser Tok R xs₄) →
       (p₁ ∣ p₂) ∣ (p₃ ∣ p₄) ≅P (p₁ ∣ p₃) ∣ (p₂ ∣ p₄)
swap p₁ p₂ p₃ p₄ =
  (p₁ ∣ p₂) ∣ (p₃ ∣ p₄)  ≅⟨ associative p₁ p₂ (p₃ ∣ p₄) ⟩
  p₁ ∣ (p₂ ∣ (p₃ ∣ p₄))  ≅⟨ (p₁ ∎) ∣ (
    p₂ ∣ (p₃ ∣ p₄)            ≅⟨ sym $ associative p₂ p₃ p₄ ⟩
    (p₂ ∣ p₃) ∣ p₄            ≅⟨ commutative p₂ p₃ ∣ (p₄ ∎) ⟩
    (p₃ ∣ p₂) ∣ p₄            ≅⟨ associative p₃ p₂ p₄ ⟩
    p₃ ∣ (p₂ ∣ p₄)            ∎) ⟩
  p₁ ∣ (p₃ ∣ (p₂ ∣ p₄))  ≅⟨ sym $ associative p₁ p₃ (p₂ ∣ p₄) ⟩
  (p₁ ∣ p₃) ∣ (p₂ ∣ p₄)  ∎

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Web.URI.Scheme where

open import Web.URI.Scheme.Primitive public using ( Scheme? ; http: ; https: ; ε )

max_stars_repo_name: agda/agda-web-uri

max_issues_repo_name: agda/agda-web-uri

max_forks_repo_name: agda/agda-web-uri


text:
module PreludeBool where
import AlonzoPrelude
open AlonzoPrelude

-- import Logic.Base

infixr 20 _||_
infixr 30 _&&_

data Bool : Set where
  false : Bool
  true  : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

_&&_ : Bool -> Bool -> Bool
true  && x = x
false && _ = false

_||_ : Bool -> Bool -> Bool
true  || _ = true
false || x = x

not : Bool -> Bool
not true  = false
not false = true

-- open Logic.Base

IsTrue : Bool -> Set
IsTrue true  = True
IsTrue false = False

IsFalse : Bool -> Set
IsFalse x = IsTrue (not x)

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
if false then x else y = y

if'_then_else_ : {A : Set} -> (x : Bool) -> (IsTrue x -> A) -> (IsFalse x -> A) -> A
if' true  then f else g = f tt
if' false then f else g = g tt

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
module Examples where

open import LF
open import IIRD
open import IIRDr

-- Some helper functions

infixl 50 _+OP_

_+OP_ : {I : Set}{D : I -> Set1}{E : Set1} -> OP I D E -> OP I D E -> OP I D E
γ₀ +OP γ₁ = σ Two (\x -> case₂ x γ₀ γ₁)

-- First something simple.

bool : OPr One (\_ -> One')
bool _ = ι★r +OP ι★r

Bool : Set
Bool = Ur bool ★

false : Bool
false = intror < ★₀ | ★ >

true : Bool
true = intror < ★₁ | ★ >

-- We don't have universe subtyping, and we only setup large elimination rules.
if_then_else_ : {A : Set1} -> Bool -> A -> A -> A
if_then_else_ {A} b x y = Rr bool (\_ _ -> A) (\_ a _ -> case₂ (π₀ a) y x) ★ b

-- Something recursive

nat : OPr One (\_ -> One')
nat _ = ι★r +OP δ One (\_ -> ★) (\_ -> ι★r)

Nat : Set
Nat = Ur nat ★

zero : Nat
zero = intror < ★₀ | ★ >

suc : Nat -> Nat
suc n = intror < ★₁ | < (\_ -> n) | ★ > >


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax Prod | P

type
  _⊗_ : 2-ary | l40

term
  pair : α  β  ->  α ⊗ β | ⟨_,_⟩
  fst  : α ⊗ β  ->  α
  snd  : α ⊗ β  ->  β

theory
  (fβ) a : α  b : β |> fst (pair(a, b))      = a
  (sβ) a : α  b : β |> snd (pair(a, b))      = b
  (pη) p : α ⊗ β    |> pair (fst(p), snd(p)) = p
-}

module Prod.Signature where

open import SOAS.Context

-- Type declaration
data PT : Set where
  _⊗_ : PT → PT → PT
infixl 40 _⊗_

open import SOAS.Syntax.Signature PT public
open import SOAS.Syntax.Build PT public

-- Operator symbols
data Pₒ : Set where
  pairₒ fstₒ sndₒ : {α β : PT} → Pₒ

-- Term signature
P:Sig : Signature Pₒ
P:Sig = sig λ
  { (pairₒ {α}{β}) → (⊢₀ α) , (⊢₀ β) ⟼₂ α ⊗ β
  ; (fstₒ  {α}{β}) → (⊢₀ α ⊗ β) ⟼₁ α
  ; (sndₒ  {α}{β}) → (⊢₀ α ⊗ β) ⟼₁ β
  }

open Signature P:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.List
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality
open import Agda.Primitive

record X {a} (A : Set a) : Set a where
  field fld : A

d : X Nat
d = record { fld = 5 }

-- Here we test that suppressing reduction of lzero has no effect on the reconstruction
-- of parameters.  Essentially, we ignore ReduceDefs annotations when reconstructing
-- hidden parameters.
macro
  x : Term → TC ⊤
  x hole = do
      (function (clause tel ps t ∷ [])) ← withReconstructed (getDefinition (quote d))
        where _ → quoteTC "ERROR" >>= unify hole
      a ← withReconstructed (dontReduceDefs (quote lzero ∷ []) (normalise t))
      quoteTC a >>= unify hole

-- If we were to consider suppressed reduction of lzero, we end up with
-- Set ≠ Set lzero.
test₁ : Term
test₁ = x

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 {A = A} xs = reverseAcc xs []
  where
    reverseAcc : List A → List A → List A
    reverseAcc [] a = a
    reverseAcc (x ∷ xs) a = reverseAcc xs (x ∷ a)

foo : Nat → Nat
foo x = 1 + x

bar : Nat → Nat
bar x = foo (foo (x))

-- Here we test that normalisation respects ReduceDefs
-- when parameter reconstruction is on.
macro
  y : Term → TC ⊤
  y hole = do
      (function (clause tel ps t ∷ [])) ← withReconstructed (dontReduceDefs (quote foo ∷ []) (getDefinition (quote bar)))
        where _ → quoteTC "ERROR" >>= unify hole
      t ← inContext (reverse tel)
          (withReconstructed (dontReduceDefs (quote foo ∷ []) (normalise t)))
      quoteTC t >>= unify hole

test₂ : y ≡ def (quote foo) (arg _ (def (quote foo) _) ∷ [])
test₂ = refl


text:
{- Category of reactive types -}
module CategoryTheory.Instances.Reactive where

open import CategoryTheory.Categories
open import CategoryTheory.BCCCs

open import Data.Nat using (ℕ ; zero ; suc ; _+_) public
open import Data.Unit using () renaming (⊤ to top) public
open import Data.Product
open import Data.Empty using (⊥-elim) renaming (⊥ to bot) public
open import Data.Sum renaming ([_,_] to ⟦_,_⟧)
import Function as F using (_∘_)

-- || Reactive types

-- Time-indexed types.
τ : Set₁
τ = ℕ -> Set

-- Time-indexed functions.
_⇴_ : τ -> τ -> Set
A ⇴ B = ∀(n : ℕ) -> A n -> B n
infixr 10 _⇴_

-- Category of reactive types
ℝeactive : Category lzero
ℝeactive = record
         { obj      = τ
         ; _~>_     = _⇴_
         ; id       = λ n a -> a
         ; _∘_      = λ g f -> λ n a -> g n (f n a)
         ; _≈_      = λ f g -> ∀ {n : ℕ} {a} -> f n a ≡ g n a
         ; id-left  = refl
         ; id-right = refl
         ; ∘-assoc  = refl
         ; ≈-equiv  = record { refl = refl
                             ; sym = λ x → sym x
                             ; trans = λ p q → trans p q }
         ; ≈-cong   = ≈-cong-ℝ
         }
         where
         ≈-cong-ℝ : ∀{A B C : τ} {f f′ : A ⇴ B} {g g′ : B ⇴ C}
                 -> (∀ {n a} -> f n a ≡ f′ n a)
                 -> (∀ {n b} -> g n b ≡ g′ n b)
                 -> (∀ {n a} -> g n (f n a) ≡ g′ n (f′ n a))
         ≈-cong-ℝ {f′ = f′} fe ge {n} {a′}
                rewrite fe {n} {a′}
                      | ge {n} {f′ n a′} = refl

-- Bicartesian closed structure for reactive types
ℝeactive-BCCC : BicartesianClosed ℝeactive
ℝeactive-BCCC = record
    { cart = record
        { term = record
            { ⊤ = λ n → top
            ; ! = λ n _ → top.tt
            ; !-unique = λ m → refl
            }
        ; prod = λ A B → record
            { A⊗B = λ n → A n × B n
            ; π₁ = λ n → proj₁
            ; π₂ = λ n → proj₂
            ; ⟨_,_⟩ = λ f g n a → (f n a , g n a)
            ; π₁-comm = λ {P} {p₁} {p₂} {n} {a} → refl
            ; π₂-comm = λ {P} {p₁} {p₂} {n} {a} → refl
            ; ⊗-unique = λ pr1 pr2 → unique-cart (ext λ a → ext λ n → pr1 {a} {n})
                                               (ext λ a → ext λ n → pr2 {a} {n})
            }
        }
    ; cocart = record
        { init = record
            { ⊥ = λ n → bot
            ; ¡ = λ {A} n → λ ()
            ; ¡-unique = λ {A} m {n} → λ {}
            }
        ; sum = λ A B → record
            { A⊕B = λ n → A n ⊎ B n
            ; ι₁ = λ n → inj₁
            ; ι₂ = λ n → inj₂
            ; [_⁏_] = sum
            ; ι₁-comm = λ {S} {i₁} {i₂} {n} {a} → refl
            ; ι₂-comm = λ {S} {i₁} {i₂} {n} {a} → refl
            ; ⊕-unique = λ {S} {i₁} {i₂} {m} pr1 pr2 →
                        unique-cocart {m = m} (ext λ a → ext λ n → pr1 {a} {n})
                                      (ext λ a → ext λ n → pr2 {a} {n})
            }
        }
    ; closed = record
        { exp = λ A B → record
            { A⇒B = λ n → A n -> B n
            ; eval = λ n z → proj₁ z (proj₂ z)
            ; Λ = λ  f n a b → f n (a , b)
            ; Λ-comm = refl
            ; Λ-unique = λ pr → unique-closed (ext λ n → ext λ a → pr {n} {a})
            ; Λ-cong = λ pr → ext λ _ → pr
            }
        }
    }
    where
    open Category ℝeactive
    unique-cart : ∀{A B P : τ}
              -> {p₁ : P ⇴ A} {p₂ : P ⇴ B} {m : P ⇴ (λ n -> A n × B n)}
              -> (λ _ → proj₁) ∘ m ≡ p₁ -> (λ _ → proj₂) ∘ m ≡ p₂
              -> ∀{n : ℕ}{a : P n} -> (p₁ n a , p₂ n a) ≡ m n a
    unique-cart refl refl = refl
    sum : {A B S : obj} → A ⇴ S → B ⇴ S → (λ n → A n ⊎ B n) ⇴ S
    sum f g n (inj₁ x) = f n x
    sum f g n (inj₂ y) = g n y
    unique-cocart : ∀{A B S : τ}
              -> {i₁ : A ⇴ S} {i₂ : B ⇴ S} {m : (λ n -> A n ⊎ B n) ⇴ S}
              -> m ∘ (λ _ -> inj₁) ≡ i₁ -> m ∘ (λ _ -> inj₂) ≡ i₂
              -> ∀{n : ℕ}{a : A n ⊎ B n} -> sum i₁ i₂ n a ≡ m n a
    unique-cocart refl refl {n} {inj₁ x} = refl
    unique-cocart refl refl {n} {inj₂ y} = refl
    unique-closed : ∀{A B E : τ}
              -> {e : (λ n -> E n × A n) ⇴ B} {m : E ⇴ (λ n -> A n -> B n)}
              -> (λ n fa → proj₁ fa (proj₂ fa)) ∘ ((λ n (a : E n × A n) -> ( (m n F.∘ proj₁) a , proj₂ a ))) ≡ e
              -> ∀{n}{a : E n} -> (λ b → e n (a , b)) ≡ m n a
    unique-closed refl = refl

-- | Top-level shorthands for distinguished BCCC objects and morphisms
open BicartesianClosed ℝeactive-BCCC public
open Category ℝeactive hiding (begin_ ; _∎) public

ℝeactive-cart : Cartesian ℝeactive
ℝeactive-cart = cart

-- Non-canonical distribution morphism
dist : ∀{A B C : τ} ->  A ⊗ (B ⊕ C) ⇴ (A ⊗ B) ⊕ (A ⊗ C)
dist n (a , inj₁ b) = inj₁ (a , b)
dist n (a , inj₂ c) = inj₂ (a , c)

dist2 : ∀{A B C D : τ} ->  A ⊗ (B ⊕ C ⊕ D) ⇴ (A ⊗ B) ⊕ (A ⊗ C) ⊕ (A ⊗ D)
dist2 n (a , inj₁ (inj₁ b)) = inj₁ (inj₁ (a , b))
dist2 n (a , inj₁ (inj₂ c)) = inj₁ (inj₂ (a , c))
dist2 n (a , inj₂ d) = inj₂ (a , d)

-- ℝeactive is distributive
dist-ℝ : ∀{A B C : τ} -> (A ⊗ B) ⊕ (A ⊗ C) <~> A ⊗ (B ⊕ C)
dist-ℝ = record
    { iso~> = [ id * ι₁ ⁏ id * ι₂ ]
    ; iso<~ = dist
    ; iso-id₁ = dist-iso-id₁
    ; iso-id₂ = dist-iso-id₂
    }
    where
    dist-iso-id₁ : ∀{A B C : τ} -> dist {A}{B}{C} ∘ [ id * ι₁ ⁏ id * ι₂ ] ≈ id
    dist-iso-id₁ {n = n} {inj₁ (a , b)} = refl
    dist-iso-id₁ {n = n} {inj₂ (a , c)} = refl

    dist-iso-id₂ : ∀{A B C : τ} -> [ id * ι₁ ⁏ id * ι₂ ] ∘ dist {A}{B}{C} ≈ id
    dist-iso-id₂ {n = n} {a , inj₁ b} = refl
    dist-iso-id₂ {n = n} {a , inj₂ c} = refl

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
------------------------------------------------------------------------------
-- Testing the translation of definitions
------------------------------------------------------------------------------

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

module Definition01d where

infixl 6 _+_
infix  4 _≡_

postulate
  D    : Set
  zero : D
  succ : D → D
  _≡_  : D → D → Set

data N : D → Set where
  zN : N zero
  sN : ∀ {n} → N n → N (succ n)

N-ind : (A : D → Set) →
       A zero →
       (∀ {n} → A n → A (succ n)) →
       ∀ {n} → N n → A n
N-ind A A0 h zN      = A0
N-ind A A0 h (sN Nn) = h (N-ind A A0 h Nn)

postulate
  _+_  : D → D → D
  +-0x : ∀ n → zero + n     ≡ n
  +-Sx : ∀ m n → succ m + n ≡ succ (m + n)
{-# ATP axioms +-0x +-Sx #-}

-- We test the translation of the definition of a unary predicate.

A : D → Set
A i = zero + i ≡ i
{-# ATP definition A #-}

postulate A0 : A zero
{-# ATP prove A0 #-}

postulate is : ∀ {i} → A i → A (succ i)
{-# ATP prove is #-}

+-leftIdentity : ∀ {n} → N n → zero + n ≡ n
+-leftIdentity = N-ind A A0 is

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax Prod | P

type
  _⊗_ : 2-ary | l40

term
  pair : α  β  ->  α ⊗ β | ⟨_,_⟩
  fst  : α ⊗ β  ->  α
  snd  : α ⊗ β  ->  β

theory
  (fβ) a : α  b : β |> fst (pair(a, b))      = a
  (sβ) a : α  b : β |> snd (pair(a, b))      = b
  (pη) p : α ⊗ β    |> pair (fst(p), snd(p)) = p
-}

module Prod.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import Prod.Signature
open import Prod.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution P:Syn
open import SOAS.Metatheory.SecondOrder.Equality P:Syn

private
  variable
    α β γ τ : PT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ P) α Γ → (𝔐 ▷ P) α Γ → Set where
  fβ : ⁅ α ⁆ ⁅ β ⁆̣ ▹ ∅ ⊢     fst ⟨ 𝔞 , 𝔟 ⟩ ≋ₐ 𝔞
  sβ : ⁅ α ⁆ ⁅ β ⁆̣ ▹ ∅ ⊢     snd ⟨ 𝔞 , 𝔟 ⟩ ≋ₐ 𝔟
  pη : ⁅ α ⊗ β ⁆̣   ▹ ∅ ⊢ ⟨ fst 𝔞 , snd 𝔞 ⟩ ≋ₐ 𝔞

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning


text:
{-# OPTIONS --cubical --safe #-}

module Algebra.Construct.Free.Semilattice.Relation.Unary.All.Properties where

open import Prelude hiding (⊥; ⊤)
open import Algebra.Construct.Free.Semilattice.Eliminators
open import Algebra.Construct.Free.Semilattice.Definition
open import Cubical.Foundations.HLevels
open import Data.Empty.UniversePolymorphic
open import HITs.PropositionalTruncation.Sugar
open import HITs.PropositionalTruncation.Properties
open import HITs.PropositionalTruncation
open import Data.Unit.UniversePolymorphic
open import Algebra.Construct.Free.Semilattice.Relation.Unary.All.Def
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Membership
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Decidable.Properties
open import Relation.Nullary.Decidable.Logic

private
  variable p : Level

P∈◇ : ∀ {p} {P : A → Type p} → ∀ x xs → x ∈ xs → ◻ P xs → ∥ P x ∥
P∈◇ {A = A} {P = P} = λ x → ∥ P∈◇′ x ∥⇓
  where
  P∈◇′ : (x : A) → xs ∈𝒦 A ⇒∥ (x ∈ xs → ◻ P xs → ∥ P x ∥) ∥
  ∥ P∈◇′ x ∥-prop p q i x∈xs ◻Pxs = squash (p x∈xs ◻Pxs) (q x∈xs ◻Pxs) i
  ∥ P∈◇′ x ∥[] ()
  ∥ P∈◇′ x ∥ y ∷ ys ⟨ Pys ⟩ x∈xs ◻Pxs =
    x∈xs >>=
      either′
        (λ y≡x → subst (∥_∥ ∘ P) y≡x (◻Pxs .fst))
        (λ x∈ys → Pys x∈ys (◻Pxs .snd))

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Example where

loop : Set
loop = loop

_∞_ : Set -> Set -> Set
x ∞ y = x ∞ y

data Nat : Set where
    zero : Nat
    succ : Nat -> Nat

id : Nat -> Nat
id zero = zero
id (succ n) = succ (id n)

bad : Nat -> Nat
bad n = bad n

_+_ : Nat -> Nat -> Nat
zero     + n = n
(succ m) + n = succ (m + n)

bad2 : Nat -> Nat
bad2 (succ x) = bad2 x + bad2 (succ x)
bad2 x        = bad2 x

data Bool : Set where
    true : Bool
    false : Bool

_&&_ : Bool -> Bool -> Bool
true && a = a
false && a = false

mutual

  even : Nat -> Bool
  even zero = true
  even (succ n) = odd n

  odd  : Nat -> Bool
  odd zero = false
  odd (succ n) = even n

data Ty : {_ : Nat} -> Set where
    Base : forall {n} -> Ty {succ n}
    Arr  : forall {n} -> Ty {n} -> Ty {n} -> Ty {succ n}

eqty : forall {n} -> Ty {n} -> Ty {n} -> Bool
eqty Base Base = true
eqty (Arr a b) (Arr a' b') = (eqty a a') && (eqty b b')
eqty _ _ = false

subty : forall {n} -> Ty {n} -> Ty {n} -> Bool
subty Base Base = true
subty (Arr a b) (Arr a' b') = (subty a' a) && (subty b b')
subty _ _ = false

-- the following is enough for making it termination check
subty' : forall {n} -> Ty {n} -> Ty {n} -> Bool
subty' Base Base = true
subty' {succ n} (Arr a b) (Arr a' b')
     = (subty' a' a) && (subty' b b')
subty' _ _ = false

subty'' : forall {n} -> Ty {n} -> Ty {n} -> Bool
subty'' Base Base = true
subty'' {succ n} (Arr {.n} a b) (Arr .{n} a'' b'')
     = (subty'' {n} a'' a) && (subty'' {n} b b'')
subty'' _ _ = false

data _×_ (A B : Set) : Set where
    _,_ : A -> B -> A × B

add : Nat × Nat -> Nat
add (zero   , m) = m
add (succ n , m) = succ (add (n , m))

eq : Nat × Nat -> Bool
eq (zero   , zero  ) = true
eq (succ n , succ m) = eq (n , m)
eq _ = false

-- the following should not termination check

mutual

  f : Nat -> Nat -> Nat
  f zero y = zero
  f (succ x) zero = zero
  f (succ x) (succ y) = (g x (succ y)) + (f  (succ (succ x)) y)

  g : Nat -> Nat -> Nat
  g zero y = zero
  g (succ x) zero = zero
  g (succ x) (succ y) = (f (succ x) (succ y)) + (g x (succ (succ y)))

mutual

  badf : Nat ×  Nat -> Nat
  badf (zero , y) = zero
  badf (succ x , zero) = zero
  badf (succ x , succ y) = badg (x , succ y) + badf  (succ (succ x) , y)

  badg : Nat × Nat -> Nat
  badg (zero , y) = zero
  badg (succ x , zero) = zero
  badg (succ x , succ y) = badf (succ x , succ y) +  badg (x , succ (succ y))

-- these are ok, however

mutual

  f' : Nat -> Nat -> Nat
  f' zero y = zero
  f' (succ x) zero = zero
  f' (succ x) (succ y) = (g' x (succ y)) + (f'  (succ (succ x)) y)

  g' : Nat -> Nat -> Nat
  g' zero y = zero
  g' (succ x) zero = zero
  g' (succ x) (succ y) = (f' (succ x) (succ y)) + (g' x (succ y))

-- these are ok, however

bla : Nat
bla = succ (succ zero)

mutual

  f'' : Nat -> Nat -> Nat
  f'' zero y = zero
  f'' (succ x) zero = zero
  f'' (succ x) (succ y) = (g'' x (succ y)) + (f'' bla y)

  g'' : Nat -> Nat -> Nat
  g'' zero y = zero
  g'' (succ x) zero = zero
  g'' (succ x) (succ y) = (f'' (succ x) (succ y)) + (g'' x (succ y))

-- Ackermann

ack : Nat -> Nat -> Nat
ack zero y = succ y
ack (succ x) zero = ack x (succ zero)
ack (succ x) (succ y) = ack x (ack (succ x) y)

ack' : Nat × Nat -> Nat
ack' (zero , y) = succ y
ack' (succ x , zero) = ack' (x , succ zero)
ack' (succ x , succ y) = ack' (x , ack' (succ x , y))

-- Maximum of 3 numbers

max3 : Nat -> Nat -> Nat -> Nat
max3 zero zero z = z
max3 zero y zero = y
max3 x zero zero = x
max3 (succ x) (succ y) zero = succ (max3 x y zero)
max3 (succ x) zero (succ z) = succ (max3 x zero z)
max3 zero (succ y) (succ z) = succ (max3 zero y z)
max3 (succ x) (succ y) (succ z) = succ (max3 x y z)

-- addition of Ordinals

data Ord : Set where
   ozero : Ord
   olim  : (Nat -> Ord) -> Ord

addord : Ord -> Ord -> Ord
addord x ozero = x
addord x (olim f) = olim (\ n -> addord x (f n))

-- Higher-order example which should not pass the termination checker.
-- (Not the current one, anyway.)

foo : Ord -> (Nat -> Ord) -> Ord
foo ozero    g = ozero
foo (olim f) g = olim (\n -> foo (g n) f)

-- Examples checking that a function can be used with several
-- different numbers of arguments on the right-hand side.

const : {a b : Set1} -> a -> b -> a
const x _ = x

ok : Nat -> Nat -> Set
ok zero     y = Nat
ok (succ x) y = const Nat (const (ok x y) (ok x))

notOK : Set -> Set
notOK x = const (notOK Ord) notOK

-- An example which should fail (37 is an arbitrary number):

data ⊤ : Set where
  tt : ⊤

mutual

  foo37 : ⊤ -> ⊤
  foo37 x = bar37 x

  bar37 : ⊤ -> ⊤
  bar37 tt = foo37 tt

-- Some examples involving with.

-- Not OK:

withNo : Nat -> Nat
withNo n with n
withNo n | m = withNo m

-- OK:

withYes : Nat -> Nat
withYes n with n
withYes n | zero   = zero
withYes n | succ m = withYes m

-- Some rather convoluted examples.

-- OK:

number : Nat
number = zero
  where
  data Foo12 : Nat -> Set where
    foo12 : Foo12 number

-- Should the occurrence of number' in the type signature of foo12
-- really be highlighted here?

number' : Nat
number' with zero
number' | x = g12 foo12
  where
  data Foo12 : Nat -> Set where
    foo12 : Foo12 number'
  abstract
    g12 : {i : Nat} -> Foo12 i -> Nat
    g12 foo12 = zero

-- Tests highlighting (but does not type check yet):

-- number'' : Nat
-- number'' with zero
-- number'' | x = g12 (foo12 x)
--   where
--   data Foo12 : Nat -> Set where
--     foo12 : (n : Nat) -> Foo12 (number'' | n)
--   abstract
--     g12 : {i : Nat} -> Foo12 i -> Nat
--     g12 (foo12 n) = n

data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

infixr 50 _::_

-- butlast function
good1 : {A : Set} -> List A -> A
good1 (a :: []) = a
good1 (a :: b :: bs) = good1 (b :: bs)

infixl 10 _⊕_
postulate
  _⊕_ : {A : Set} -> A -> A -> A  -- non-deterministic choice

-- a funny formulation of insert
-- insert (a :: l)  inserts a into l
insert : {A : Set} -> List A -> List A
insert [] = []
insert (a :: []) = a :: []
insert (a :: b :: bs) = a :: b :: bs ⊕        -- case a <= b
                        b :: insert (a :: bs) -- case a > b

-- list flattening
flat : {A : Set} -> List (List A) -> List A
flat [] = []
flat ([] :: ll) = flat ll
flat ((x :: l) :: ll) = x :: flat (l :: ll)

-- leaf-labelled trees

data Tree (A : Set) : Set where
  leaf : A -> Tree A
  node : Tree A -> Tree A -> Tree A

-- flattening (does not termination check)

tflat : {A : Set} -> Tree A -> List A
tflat (leaf a) = a :: []
tflat (node (leaf a) r) = a :: tflat r
tflat (node (node l1 l2) r) = tflat (node l1 (node l2 r))

-- Maximum of 3 numbers
-- mixing tupling and swapping: does not work with structured orders

max3' : Nat × Nat -> Nat -> Nat
max3' (zero , zero) z = z
max3' (zero , y) zero = y
max3' (x , zero) zero = x
max3' (succ x , succ y) zero   = succ (max3' (x , y) zero)
max3' (succ x , zero) (succ z) = succ (max3' (x , z) zero)
max3' (zero , succ y) (succ z) = succ (max3' (y , z) zero)
max3' (succ x , succ y) (succ z) = succ (max3' (z , x) y)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Adjunction.Composition where

open import Level

open import Categories.Category
open import Categories.Functor hiding (equiv; assoc; identityˡ; identityʳ; ∘-resp-≡) renaming (id to idF; _≡_ to _≡F_; _∘_ to _∘F_)
open import Categories.NaturalTransformation hiding (equiv; setoid) renaming (id to idT; _≡_ to _≡T_)

open import Categories.Adjunction

infixr 9 _∘_
_∘_ : ∀ {o ℓ e} {o₁ ℓ₁ e₁} {o₂ ℓ₂ e₂} {C : Category o ℓ e} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
      {F : Functor D C} {G : Functor C D} {H : Functor E D} {I : Functor D E} →
      Adjunction F G → Adjunction H I → Adjunction (F ∘F H) (I ∘F G)
_∘_ {C = C} {D} {E} {F} {G} {H} {I} X Y = record
  { unit = (I ∘ˡ (Xη′ ∘ʳ H)) ∘₁ Yη′
  ; counit = Xε′ ∘₁ (F ∘ˡ (Yε′ ∘ʳ G))
  ; zig = λ {x} → zig′ {x}
  ; zag = λ {x} → zag′ {x}
  }
  where
    module C = Category C
    module D = Category D
    module E = Category E
    module F = Functor F
    module G = Functor G renaming (F₀ to G₀; F₁ to G₁; F-resp-≡ to G-resp-≡)
    module H = Functor H renaming (F₀ to H₀; F₁ to H₁; F-resp-≡ to H-resp-≡)
    module I = Functor I renaming (F₀ to I₀; F₁ to I₁; F-resp-≡ to I-resp-≡)
    module X′ = Adjunction X renaming (unit to Xη′; counit to Xε′)
    module Y′ = Adjunction Y renaming (unit to Yη′; counit to Yε′)
    module Xη = NaturalTransformation (Adjunction.unit X) renaming (η to ηX)
    module Yη = NaturalTransformation (Adjunction.unit Y) renaming (η to ηY)
    module Xε = NaturalTransformation (Adjunction.counit X) renaming (η to εX)
    module Yε = NaturalTransformation (Adjunction.counit Y) renaming (η to εY)
    open C
    open D
    open E
    open F
    open G
    open H
    open I
    open X′
    open Y′
    open Xη
    open Yη
    open Xε
    open Yε

    .zig′ : {x : E.Obj} →
              C.id C.≡
                (εX (F₀ (H₀ x)) C.∘ F₁ (εY (G₀ (F₀ (H₀ x))))) C.∘
                  F₁ (H₁ (I₁ (ηX (H₀ x)) E.∘ ηY x))
    zig′ {x} =
        begin
          C.id
        ↑⟨ F.identity ⟩
          F₁ D.id
        ↓⟨ F-resp-≡ Y′.zig ⟩
          F₁ (D [ εY (H₀ x) ∘ H₁ (ηY x) ])
        ↓⟨ F.homomorphism ⟩
          F₁ (εY (H₀ x)) C.∘ F₁ (H₁ (ηY x))
        ↑⟨ C.∘-resp-≡ˡ C.identityˡ ⟩
          (C.id C.∘ F₁ (εY (H₀ x))) C.∘
            F₁ (H₁ (ηY x))
        ↓⟨ C.∘-resp-≡ˡ (C.∘-resp-≡ˡ X′.zig) ⟩
          ((εX (F₀ (H₀ x)) C.∘ F₁ (ηX (H₀ x))) C.∘ F₁ (εY (H₀ x))) C.∘
            F₁ (H₁ (ηY x))
        ↓⟨ C.∘-resp-≡ˡ C.assoc ⟩
          (εX (F₀ (H₀ x)) C.∘ F₁ (ηX (H₀ x)) C.∘ F₁ (εY (H₀ x))) C.∘
            F₁ (H₁ (ηY x))
        ↓⟨ C.assoc ⟩
          εX (F₀ (H₀ x)) C.∘ (F₁ (ηX (H₀ x)) C.∘ F₁ (εY (H₀ x))) C.∘ F₁ (H₁ (ηY x))
        ↑⟨ C.∘-resp-≡ʳ (C.∘-resp-≡ˡ F.homomorphism) ⟩
          εX (F₀ (H₀ x)) C.∘ F₁ (ηX (H₀ x) D.∘ εY (H₀ x)) C.∘ F₁ (H₁ (ηY x))
        ↑⟨ C.∘-resp-≡ʳ F.homomorphism ⟩
          εX (F₀ (H₀ x)) C.∘ F₁ ((ηX (H₀ x) D.∘ εY (H₀ x)) D.∘ H₁ (ηY x))
        ↑⟨ C.∘-resp-≡ʳ (F-resp-≡ (D.∘-resp-≡ˡ (Yε.commute (ηX (H₀ x))))) ⟩
          εX (F₀ (H₀ x)) C.∘
            F₁ ((εY (G₀ (F₀ (H₀ x))) D.∘ H₁ (I₁ (ηX (H₀ x)))) D.∘ H₁ (ηY x))
        ↓⟨ C.∘-resp-≡ʳ (F-resp-≡ D.assoc) ⟩
          εX (F₀ (H₀ x)) C.∘
            F₁ (εY (G₀ (F₀ (H₀ x))) D.∘ D [ H₁ (I₁ (ηX (H₀ x))) ∘ H₁ (ηY x) ])
        ↑⟨ C.∘-resp-≡ʳ (F-resp-≡ (D.∘-resp-≡ʳ H.homomorphism)) ⟩
          εX (F₀ (H₀ x)) C.∘
            F₁ (D [ εY (G₀ (F₀ (H₀ x))) ∘ H₁ (I₁ (ηX (H₀ x)) E.∘ ηY x) ])
        ↓⟨ C.∘-resp-≡ʳ F.homomorphism ⟩
          εX (F₀ (H₀ x)) C.∘
            F₁ (εY (G₀ (F₀ (H₀ x)))) C.∘ F₁ (H₁ (I₁ (ηX (H₀ x)) E.∘ ηY x))
        ↑⟨ C.assoc ⟩
          (εX (F₀ (H₀ x)) C.∘ F₁ (εY (G₀ (F₀ (H₀ x))))) C.∘
            F₁ (H₁ (I₁ (ηX (H₀ x)) E.∘ ηY x))
        ∎
      where open C.HomReasoning

    .zag′ : {x : C.Obj} →
              E.id E.≡
                I₁ (G₁ (εX x C.∘ F₁ (εY (G₀ x)))) E.∘
                I₁ (ηX (H₀ (I₀ (G₀ x)))) E.∘ ηY (I₀ (G₀ x))
    zag′ {x} =
        begin
          E.id
        ↓⟨ Y′.zag ⟩
          (I₁ (εY (G₀ x))) E.∘ (ηY (I₀ (G₀ x)))
        ↑⟨ E.∘-resp-≡ˡ (I-resp-≡ D.identityˡ) ⟩
          (I₁ (D.id D.∘ (εY (G₀ x)))) E.∘ (ηY (I₀ (G₀ x)))
        ↓⟨ E.∘-resp-≡ˡ (I-resp-≡ (D.∘-resp-≡ˡ X′.zag)) ⟩
          (I₁ ((G₁ (εX x) D.∘ (ηX (G₀ x))) D.∘ (εY (G₀ x)))) E.∘ (ηY (I₀ (G₀ x)))
        ↓⟨ E.∘-resp-≡ˡ (I-resp-≡ D.assoc) ⟩
          I₁ (G₁ (εX x) D.∘ ηX (G₀ x) D.∘ εY (G₀ x)) E.∘ ηY (I₀ (G₀ x))
        ↓⟨ E.∘-resp-≡ˡ (I-resp-≡ (D.∘-resp-≡ʳ (Xη.commute (εY (G₀ x))))) ⟩
          I₁ (G₁ (εX x) D.∘ G₁ (F₁ (εY (G₀ x))) D.∘ ηX (H₀ (I₀ (G₀ x)))) E.∘
            ηY (I₀ (G₀ x))
        ↑⟨ E.∘-resp-≡ˡ (I-resp-≡ D.assoc) ⟩
          I₁ (D [ G₁ (εX x) ∘ G₁ (F₁ (εY (G₀ x))) ] D.∘ ηX (H₀ (I₀ (G₀ x))))
            E.∘ ηY (I₀ (G₀ x))
        ↑⟨ E.∘-resp-≡ˡ (I-resp-≡ (D.∘-resp-≡ˡ G.homomorphism)) ⟩
          I₁ (D [ G₁ (εX x C.∘ F₁ (εY (G₀ x))) ∘ ηX (H₀ (I₀ (G₀ x))) ]) E.∘
            ηY (I₀ (G₀ x))
        ↓⟨ E.∘-resp-≡ˡ I.homomorphism ⟩
          (I₁ (G₁ (εX x C.∘ F₁ (εY (G₀ x)))) E.∘ I₁ (ηX (H₀ (I₀ (G₀ x))))) E.∘
            ηY (I₀ (G₀ x))
        ↓⟨ E.assoc ⟩
          I₁ (G₁ (εX x C.∘ F₁ (εY (G₀ x)))) E.∘
            I₁ (ηX (H₀ (I₀ (G₀ x)))) E.∘ ηY (I₀ (G₀ x))
        ∎
      where open E.HomReasoning

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Lec7 where

open import Lec1Done

data List (X : Set) : Set where
  []   : List X
  _,-_ : X -> List X -> List X

foldrL : {X T : Set} -> (X -> T -> T) -> T -> List X -> T
foldrL c n [] = n
foldrL c n (x ,- xs) = c x (foldrL c n xs)

data Bwd (X : Set) : Set where
  []   : Bwd X
  _-,_ : Bwd X -> X -> Bwd X
infixl 3 _-,_

data _<=_ {X : Set} : (xz yz : Bwd X) -> Set where
  oz : [] <= []
  os : {xz yz : Bwd X}{y : X} -> xz <= yz -> (xz -, y) <= (yz -, y)
  o' : {xz yz : Bwd X}{y : X} -> xz <= yz ->  xz       <= (yz -, y)

oe : {X : Set}{xz : Bwd X} -> [] <= xz
oe {_} {[]}      = oz
oe {_} {xz -, _} = o' oe

oi : {X : Set}{xz : Bwd X} -> xz <= xz
oi {_} {[]}      = oz
oi {_} {xz -, _} = os oi       -- look here...

_<o<_ : {X : Set}{xz yz zz : Bwd X} -> xz <= yz -> yz <= zz -> xz <= zz
th <o< o' ph = o' (th <o< ph)
oz <o< oz = oz
os th <o< os ph = os (th <o< ph)   -- ...and here
o' th <o< os ph = o' (th <o< ph)

Elem : {X : Set} -> X -> Bwd X -> Set
Elem x yz = ([] -, x) <= yz

data Ty : Set where
  one  : Ty
  list : Ty -> Ty
  _=>_ : Ty -> Ty -> Ty
infixr 4 _=>_

Val : Ty -> Set
Val one      = One
Val (list T) = List (Val T)
Val (S => T) = Val S -> Val T

data Tm (Tz : Bwd Ty) : Ty -> Set where

  var : {T : Ty} -> Elem T Tz -> Tm Tz T

  <> : Tm Tz one

  []   : {T : Ty} -> Tm Tz (list T)
  _,-_ : {T : Ty} -> Tm Tz T -> Tm Tz (list T) -> Tm Tz (list T)
  foldr : {S T : Ty} ->
          Tm Tz (S => T => T) ->
          Tm Tz T ->
          Tm Tz (list S)
          -> Tm Tz T

  lam : {S T : Ty} ->
        Tm (Tz -, S) T
        -> Tm Tz (S => T)
  _$$_ : {S T : Ty} ->
         Tm Tz (S => T) ->
         Tm Tz S
         -> Tm Tz T

infixl 3 _$$_

All : {X : Set} -> (X -> Set) -> Bwd X -> Set
All P []        = One
All P (xz -, x) = All P xz * P x

all : {X : Set}{P Q : X -> Set}(f : (x : X) -> P x -> Q x) -> (xz : Bwd X) -> All P xz -> All Q xz
all f [] <> = <>
all f (xz -, x) (pz , p) = all f xz pz , f x p

Env : Bwd Ty -> Set
Env = All Val

select : {X : Set}{P : X -> Set}{Sz Tz : Bwd X} -> Sz <= Tz -> All P Tz -> All P Sz
select oz     <>       = <>
select (os x) (vz , v) = select x vz , v
select (o' x) (vz , v) = select x vz

eval : {Tz : Bwd Ty}{T : Ty} -> Env Tz -> Tm Tz T -> Val T
eval vz (var x) with select x vz
eval vz (var x) | <> , v = v
eval vz <> = <>
eval vz []               = []
eval vz (t ,- ts)        = eval vz t ,- eval vz ts
eval vz (foldr c n ts)   = foldrL (eval vz c) (eval vz n) (eval vz ts)
eval vz (lam t)          = \ s -> eval (vz , s) t
eval vz (f $$ s)         = eval vz f (eval vz s)

append : {Tz : Bwd Ty}{T : Ty} ->
         Tm Tz (list T => list T => list T)
append = lam (lam (foldr (lam (lam (var (o' (os oe)) ,- var (os oe))))
           (var (os oe)) (var (o' (os oe)))))

test : Val (list one)
test = eval {[]} <> (append $$ (<> ,- []) $$ (<> ,- []))

thin : {Sz Tz : Bwd Ty} -> Sz <= Tz -> {S : Ty} -> Tm Sz S -> Tm Tz S
thin th (var x) = var (x <o< th)
thin th <> = <>
thin th [] = []
thin th (t ,- ts) = thin th t ,- thin th ts
thin th (foldr c n ts) = foldr (thin th c) (thin th n) (thin th ts)
thin th (lam t) = lam (thin (os th) t)
thin th (f $$ s) = thin th f $$ thin th s

Subst : Bwd Ty -> Bwd Ty -> Set
Subst Sz Tz = All (Tm Tz) Sz

subst : {Sz Tz : Bwd Ty} -> Subst Sz Tz -> {S : Ty} -> Tm Sz S -> Tm Tz S
subst tz (var x) with select x tz
subst tz (var x) | <> , t = t
subst tz <> = <>
subst tz [] = []
subst tz (t ,- ts) = subst tz t ,- subst tz ts
subst tz (foldr c n ts) = foldr (subst tz c) (subst tz n) (subst tz ts)
subst tz (lam t) = lam (subst (all (\ T -> thin (o' oi)) _ tz , (var (os oe))) t)
subst tz (f $$ s) = subst tz f $$ subst tz s

record Action (M : Bwd Ty -> Bwd Ty -> Set) : Set where
  field
    varA : forall {S Sz Tz} -> M Sz Tz -> Elem S Sz -> Tm Tz S
    lamA : forall {S Sz Tz} -> M Sz Tz -> M (Sz -, S) (Tz -, S)
  act : {Sz Tz : Bwd Ty} -> M Sz Tz -> {S : Ty} -> Tm Sz S -> Tm Tz S
  act m (var x) = varA m x
  act m <> = <>
  act m [] = []
  act m (t ,- ts) = act m t ,- act m ts
  act m (foldr c n ts) = foldr (act m c) (act m n) (act m ts)
  act m (lam t) = lam (act (lamA m) t)
  act m (f $$ s) = act m f $$ act m s

THIN : Action _<=_
Action.varA THIN th x = var (x <o< th)
Action.lamA THIN = os

SUBST : Action Subst
Action.varA SUBST tz x with select x tz
... | <> , t = t
Action.lamA SUBST tz = all (\ T -> Action.act THIN (o' oi)) _ tz , (var (os oe))

-- substitution
-- thinning
-- abstr-action

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module lambda.vec where

open import Data.Nat
open import Data.Fin hiding (_+_)

infixr 40 _▸_

data vec (T : Set) : ℕ → Set where
  ε : vec T 0
  _▸_ : ∀ {n} → vec T n → T → vec T (suc n)

lookup : ∀ {n} → {T : Set} → Fin n → vec T n → T
lookup zero (Γ ▸ x) = x
lookup (suc i) (Γ ▸ x) = lookup i Γ


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

module PiIter where

open import Level using (_⊔_) renaming (zero to l0; suc to lsuc)
open import Universe using (Universe)

open import Categories.Category using (Category)
open import Categories.Groupoid using (Groupoid)
open import Categories.Functor using (Functor)

open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum hiding ([_,_])
open import Data.Product
open import Relation.Binary.PropositionalEquality as P
open import Function using (flip)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Nat.Properties.Simple using (+-right-identity)
open import Data.Integer using (ℤ;+_;-[1+_]) renaming (suc to ℤsuc; -_ to ℤ-; _+_ to _ℤ+_)

open import PiU using (U; ZERO; ONE; PLUS; TIMES; toℕ)
open import PiLevel0
open import PiLevel1
open import PiEquiv renaming (eval to ap; evalB to apB)
open import Equiv

infix 40 _^_

_^_ : {τ : U} → (p : τ ⟷ τ) → (k : ℤ) → (τ ⟷ τ)
p ^ (+ 0) = id⟷
p ^ (+ (suc k)) = p ◎ (p ^ (+ k))
p ^ -[1+ 0 ] = ! p
p ^ (-[1+ (suc k) ]) = (! p) ◎ (p ^ -[1+ k ])

-- useful properties of ^
-- because ^ is iterated composition of the same thing,
-- then by associativity, we can hive off compositions
-- from left or right

assoc1 : {τ : U} → {p : τ ⟷ τ} → (m : ℕ) →
  (p ◎ (p ^ (+ m))) ⇔ ((p ^ (+ m)) ◎ p)
assoc1 ℕ.zero = trans⇔ idr◎l idl◎r
assoc1 (suc m) = trans⇔ (id⇔ ⊡ assoc1 m) assoc◎l

assoc1- : {τ : U} → {p : τ ⟷ τ} → (m : ℕ) →
  ((! p) ◎ (p ^ -[1+ m ])) ⇔ ((p ^ -[1+ m ]) ◎ (! p))
assoc1- ℕ.zero = id⇔
assoc1- (suc m) = trans⇔ (id⇔ ⊡ assoc1- m) assoc◎l

-- more generally
assoc1g : {τ : U} → {p : τ ⟷ τ} → (i : ℤ) →
  (p ◎ (p ^ i)) ⇔ ((p ^ i) ◎ p)
assoc1g (+_ n) = assoc1 n
assoc1g (-[1+_] zero) = trans⇔ linv◎l rinv◎r
assoc1g (-[1+_] (suc n)) = trans⇔ assoc◎l (trans⇔ (linv◎l ⊡ id⇔) (
  trans⇔ idl◎l (2! (trans⇔ (assoc1- n ⊡ id⇔) (trans⇔ assoc◎r
  (trans⇔ (id⇔ ⊡ rinv◎l) idr◎l))))))

-- Property of ^: negating exponent is same as
-- composing in the other direction, then reversing.
^⇔! : {τ : U} → {p : τ ⟷ τ} → (k : ℤ) →
  (p ^ (ℤ- k)) ⇔ ! (p ^ k)
^⇔! (+_ ℕ.zero) = id⇔
-- need to dig deeper, as we end up negating
^⇔! (+_ (suc ℕ.zero)) = idl◎r
^⇔! (+_ (suc (suc n))) = trans⇔ (assoc1- n) (^⇔! (+ suc n) ⊡ id⇔)
^⇔! {p = p} (-[1+_] ℕ.zero) = trans⇔ idr◎l (2! !!⇔id) -- (!!⇔id {c = p})
^⇔! {p = p} (-[1+_] (suc n)) =
  trans⇔ (assoc1 (suc n)) ((^⇔! -[1+ n ]) ⊡ 2! !!⇔id) -- (!!⇔id p))

-- first match on m, n, then proof is purely PiLevel1
lower : {τ : U} {p : τ ⟷ τ} (m n : ℤ) →
  p ^ (m ℤ+ n) ⇔ ((p ^ m) ◎ (p ^ n))
lower (+_ ℕ.zero) (+_ n) = idl◎r
lower (+_ ℕ.zero) (-[1+_] n) = idl◎r
lower (+_ (suc m)) (+_ n) =
  trans⇔ (id⇔ ⊡ lower (+ m) (+ n)) assoc◎l
lower {p = p} (+_ (suc m)) (-[1+_] ℕ.zero) =
  trans⇔ idr◎r (trans⇔ (id⇔ ⊡ linv◎r) (
  trans⇔ assoc◎l (2! (assoc1 m) ⊡ id⇔)))  -- p ^ ((m + 1) -1)
lower (+_ (suc m)) (-[1+_] (suc n)) = -- p ^ ((m + 1) -(1+1+n)
  trans⇔ (lower (+ m) (-[1+ n ])) (
  trans⇔ ((trans⇔ idr◎r (id⇔ ⊡ linv◎r))  ⊡ id⇔) (
  trans⇔ assoc◎r (trans⇔ (id⇔ ⊡ assoc◎r) (
  trans⇔ assoc◎l (2! (assoc1 m) ⊡ id⇔)))))
lower (-[1+_] m) (+_ ℕ.zero) = idr◎r
lower (-[1+_] ℕ.zero) (+_ (suc n)) = 2! (trans⇔ assoc◎l (
  trans⇔ (rinv◎l ⊡ id⇔) idl◎l))
lower (-[1+_] (suc m)) (+_ (suc n)) = -- p ^ (-(1+m) + (n+1))
  trans⇔ (lower (-[1+ m ]) (+ n)) (
    trans⇔ ((trans⇔ idr◎r (id⇔ ⊡ rinv◎r))  ⊡ id⇔) (
  trans⇔ assoc◎r (trans⇔ (id⇔ ⊡ assoc◎r) (
  trans⇔ assoc◎l ((2! (assoc1- m)) ⊡ id⇔)))))
lower (-[1+_] ℕ.zero) (-[1+_] n) = id⇔
lower (-[1+_] (suc m)) (-[1+_] n) = -- p ^ (-(1+1+m) - (1+n))
  trans⇔ (id⇔ ⊡ lower (-[1+ m ]) (-[1+ n ])) assoc◎l

-- i.e. Iter is: for all i, any p' such that
-- p' ⇔ p ^ i

record Iter {τ : U} (p : τ ⟷ τ) : Set where
  constructor iter
  field
    i : ℤ
    p' : τ ⟷ τ
    p'⇔p^i : p' ⇔ (p ^ i)

-- Equality of Iter.
record _≡c_ {τ : U} {p : τ ⟷ τ} (q r : Iter p) : Set where
  constructor eqc
  field
    iter≡ : Iter.i q ≡ Iter.i r
    p⇔ : Iter.p' q ⇔ Iter.p' r

-- Iterates of id⟷
id^i≡id : {t : U} (i : ℤ) → (id⟷ ^ i) ⇔ (id⟷ {t})
id^i≡id (+_ zero) = id⇔
id^i≡id (+_ (suc n)) = trans⇔ idl◎l (id^i≡id (+ n))
id^i≡id (-[1+_] zero) = id⇔
id^i≡id (-[1+_] (suc n)) = trans⇔ idl◎l (id^i≡id -[1+ n ])

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual