text:
{-# OPTIONS --allow-unsolved-metas #-}

module InnerProduct where

open import Algebra.Bundles using (CommutativeRing)
open import NormedModule using (NormedModule)
open import Level using (_⊔_; suc)
open import Relation.Nullary using (¬_)

module _
  {r ℓr} (CR : CommutativeRing r ℓr)
  m ℓm rel
  where

module _
  {r ℓr} {CR : CommutativeRing r ℓr}
  (open CommutativeRing CR renaming (Carrier to S))
  {rel} {_<_ : S → S → Set rel} (STO : IsStrictTotalOrder _≈_ _<_)
  (_† : S → S)
  {m ℓm} (M : Module CR m ℓm)
  (open Module M renaming (Carrierᴹ to A))
  (⟨_,_⟩ : A → A → S)
  where

  record IsInnerProduct : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm ⊔ rel)) where
    field
      ⟨,⟩-linear-+ : ∀ x y z → ⟨ x +ᴹ y , z ⟩ ≈ ⟨ x , z ⟩ + ⟨ y , z ⟩
      ⟨,⟩-linear-* : ∀ s x y → ⟨ s *ₗ x , y ⟩ ≈ s * ⟨ x , y ⟩
      ⟨,⟩-cong : ∀ {x y} → x ≈ᴹ y → ⟨ x , x ⟩ ≈ ⟨ y , y ⟩
      †-linear-+ : ∀ x y → (x + y) † ≈ x † + y †
      †-cong : ∀ {s t} → s ≈ t → s † ≈ t †
      †-inv : ∀ s → (s †) † ≈ s
      ⟨,⟩-herm : ∀ x y → ⟨ x , y ⟩ ≈ ⟨ y , x ⟩ †

    real : S → Set _
    real s = s ≈ s †

    field
      ⟨x,x⟩-real : ∀ x → real ⟨ x , x ⟩
      positive-definite : ∀ {x} → ¬ (x ≈ᴹ 0ᴹ) → 0# < ⟨ x , x ⟩

    open IsStrictTotalOrder STO public
    open import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ public using (_≤_)

    _-ᴹ_ : A → A → A
    x -ᴹ y = x +ᴹ (-ᴹ y)

    ∥_∥² : A → S
    ∥ x ∥² = ⟨ x , x ⟩

    -- TODO
    -- is this universally true?
    -- or just common?
    ∥-x∥²≈∥x∥² : ∀ x → ∥ -ᴹ x ∥² ≈ ∥ x ∥²
    ∥-x∥²≈∥x∥² = {!   !}

    -- ∥a-b∥≤∥a∥-∥b∥ : ∀ a b → ∥ a -ᴹ b ∥² ≤ ∥ a ∥² - ∥ b ∥²
    -- ∥a-b∥≤∥a∥-∥b∥ = {!   !}

    [s+s†]†≈s+s† : ∀ s → (s + s †) † ≈ s + s †
    [s+s†]†≈s+s† s =
      begin
        (s + s †) †
      ≈⟨ †-linear-+ s (s †) ⟩
        (s † + (s †) †)
      ≈⟨ +-cong refl (†-inv _) ⟩
        (s † + s)
      ≈⟨ +-comm _ _ ⟩
        (s + s †)
      ∎
      where open import Relation.Binary.Reasoning.Setoid setoid

max_stars_repo_name: cspollard/diff

max_issues_repo_name: cspollard/diff

max_forks_repo_name: cspollard/diff


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

module Stream where
open import Level as Level using (zero)
import Relation.Binary as BinRel
open import Relation.Binary as BinRel hiding (Setoid; Rel)
open import Relation.Binary.PropositionalEquality as PE

Setoid = BinRel.Setoid Level.zero Level.zero

open import Data.Nat using (ℕ; zero; suc)
open import PropsAsTypes

record Stream (A : Set) : Set where
  coinductive
  field
    hd  : A
    tl  : Stream A
open Stream public

coiter : {X A : Set} → (X → A × X) → (X → Stream A)
coiter c x .hd  = π₁ (c x)
coiter c x .tl  = coiter c (π₂ (c x))

δ : ∀{A} → ℕ → Stream A → Stream A
δ 0        s = s
δ (suc n)  s = δ n (s .tl)

_at_ : ∀{A} → Stream A → ℕ → A
s at n = (δ n s) .hd

module Bisim (A : Set) where

  infix 2 _~_

  record _~_ (s t : Stream A) : Prop where
    coinductive
    field
      hd≡  : s .hd  ≡  t .hd
      tl~  : s .tl  ~  t .tl
  open _~_ public

  isBisim : Rel (Stream A) → Prop
  isBisim _R_ = ∀ s t → s R t → (s .hd ≡ t .hd) ∧ (s .tl R t .tl)

  ∃-bisim→~ :  ∀ {_R_} → isBisim _R_ →
               ∀ (s t : Stream A) → s R t → s ~ t
  ∃-bisim→~ R-isBisim s t q .hd≡  = ∧-elim₁ (R-isBisim s t q)
  ∃-bisim→~ R-isBisim s t q .tl~  =
    ∃-bisim→~ R-isBisim (s .tl) (t .tl) (∧-elim₂ (R-isBisim s t q))

  bisim→ext-≡ : ∀ {s t} → s ~ t → (∀ n → s at n ≡ t at n)
  bisim→ext-≡ p zero     = p .hd≡
  bisim→ext-≡ p (suc n)  = bisim→ext-≡ (p .tl~) n

  s-bisim-refl : ∀ {s : Stream A} → s ~ s
  s-bisim-refl      .hd≡  = PE.refl
  s-bisim-refl {s}  .tl~  = s-bisim-refl {s .tl}

  s-bisim-sym : ∀ {s t : Stream A} → s ~ t → t ~ s
  s-bisim-sym p .hd≡  = PE.sym       (p .hd≡)
  s-bisim-sym p .tl~  = s-bisim-sym  (p .tl~)

  s-bisim-trans : ∀ {r s t : Stream A} → r ~ s → s ~ t → r ~ t
  s-bisim-trans p q .hd≡  = PE.trans       (p .hd≡)  (q .hd≡)
  s-bisim-trans p q .tl~  = s-bisim-trans  (p .tl~)  (q .tl~)

  stream-setoid : Setoid
  stream-setoid = record
    { Carrier = Stream A
    ; _≈_ = _~_
    ; isEquivalence = record
      { refl   = s-bisim-refl
      ; sym    = s-bisim-sym
      ; trans  = s-bisim-trans
      }
    }

  import Relation.Binary.EqReasoning as EqR

  module ~-Reasoning where
    module _ where
      open EqR (stream-setoid) public
        hiding (_≡⟨_⟩_) renaming (_≈⟨_⟩_ to _~⟨_⟩_; begin_ to begin_; _∎ to _∎)

ext: agda

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
open import Issue1296.SolvedMeta

-- Expected error:

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Dave.Algebra.Naturals.Addition where
  open import Dave.Algebra.Naturals.Definition public
  open import Dave.Extensionality

  _+_ : ℕ → ℕ → ℕ
  zero + b = b
  suc a + b = suc (a + b)

  infixl 6 _+_

  {- Semigroup -}
  +-assoc : associative _+_
  +-assoc zero n p = refl
  +-assoc (suc m) n p = cong suc (+-assoc m n p)

  +-assoc' : associative _+_
  +-assoc' zero n p = begin
    (zero + n) + p ≡⟨⟩
    n + p ≡⟨⟩
    zero + (n + p) ∎
  +-assoc' (suc m) n p = begin
    (suc m + n) + p ≡⟨⟩
    suc (m + n) + p ≡⟨⟩
    suc ((m + n) + p) ≡⟨ cong suc (+-assoc' m n p) ⟩
    suc (m + (n + p)) ∎

  ℕ-+-IsSemigroup : IsSemigroup _+_
  IsSemigroup.assoc ℕ-+-IsSemigroup = +-assoc

  ℕ-+-Semigroup : Semigroup
  Semigroup.Carrier ℕ-+-Semigroup = ℕ
  Semigroup._·_ ℕ-+-Semigroup = _+_
  Semigroup.isSemigroup ℕ-+-Semigroup = ℕ-+-IsSemigroup

  {- Identity -}
  +-right-identity : right-identity _+_ 0
  +-right-identity zero = refl
  +-right-identity (suc n) = cong suc (+-right-identity n)

  +-left-identity : left-identity _+_ 0
  +-left-identity m = refl

  ℕ-+-HasIdentity : Identity _+_ 0
  Identity.left ℕ-+-HasIdentity = +-left-identity
  Identity.right ℕ-+-HasIdentity = +-right-identity

  {- Monoid -}
  ℕ-+-IsMonoid : IsMonoid _+_ 0
  IsMonoid.semigroup ℕ-+-IsMonoid = ℕ-+-IsSemigroup
  IsMonoid.identity ℕ-+-IsMonoid = ℕ-+-HasIdentity

  ℕ-+-Monoid : Monoid
  Monoid.Carrier ℕ-+-Monoid = ℕ
  Monoid._·_ ℕ-+-Monoid = _+_
  Monoid.e ℕ-+-Monoid = 0
  Monoid.isMonoid ℕ-+-Monoid = ℕ-+-IsMonoid

  {- Commutative Monoid -}
  +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
  +-suc zero n = refl
  +-suc (suc m) n = cong suc (+-suc m n)

  +-comm : commutative _+_
  +-comm m zero = +-right-identity m
  +-comm m (suc n) = trans (+-suc m n) (cong suc (+-comm m n))

  +-comm' : commutative _+_
  +-comm' m zero = +-right-identity m
  +-comm' m (suc n) = begin
      (m + suc n) ≡⟨ +-suc m n ⟩
      suc (m + n) ≡⟨ cong suc (+-comm' m n) ⟩
      suc (n + m) ∎

  ℕ-+-IsCommutativeMonoid : IsCommutativeMonoid _+_ 0
  IsCommutativeMonoid.isSemigroup ℕ-+-IsCommutativeMonoid = ℕ-+-IsSemigroup
  IsCommutativeMonoid.leftIdentity ℕ-+-IsCommutativeMonoid = +-left-identity
  IsCommutativeMonoid.comm ℕ-+-IsCommutativeMonoid = +-comm

  {- Additional Theorems -}
  +-add1ᵣ : ∀ (m : ℕ) → m + 1 ≡ suc m
  +-add1ᵣ zero = refl
  +-add1ᵣ (suc m) = cong suc (+-add1ᵣ m)

  +-add1ₗ : ∀ (m : ℕ) → 1 + m ≡ suc m
  +-add1ₗ m = refl

  {- Another equal Addition Definition -}
  _+´_ : ℕ → ℕ → ℕ
  m +´ zero = m
  m +´ suc n = suc (m +´ n)

  app-+≡+´ : ∀ (m n : ℕ) → m + n ≡ m +´ n
  app-+≡+´ zero zero = refl
  app-+≡+´ zero (suc n) = cong suc (app-+≡+´ zero n)
  app-+≡+´ (suc m) zero = cong suc (app-+≡+´ m zero)
  app-+≡+´ (suc m) (suc n) = cong suc (
    begin
      m + suc n ≡⟨ +-suc m n ⟩
      suc m + n ≡⟨ app-+≡+´ (suc m) n ⟩
      suc m +´ n ∎ )

  +≡+´ : _+_ ≡ _+´_
  +≡+´ = extensionality (λ m → extensionality (λ n → app-+≡+´ m n))


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

open import Agda.Primitive.Cubical
  renaming ( primIMin       to _∧_  -- I → I → I
           ; primIMax       to _∨_  -- I → I → I
           ; primINeg       to ~_   -- I → I
           )

infix 10 _≡_
postulate
  _≡_ : I → I → Set
  refl : ∀ {i} → i ≡ i

module Vars (i j k : I) where

  _ : i ∧ i1 ≡ i
  _ = refl

  _ : i ∧ i0 ≡ i0
  _ = refl

  _ : i1 ∧ i ≡ i
  _ = refl

  _ : i0 ∧ i ≡ i0
  _ = refl

  _ : i ∧ j ≡ j ∧ i
  _ = refl

  _ : i ∧ (j ∧ k) ≡ (i ∧ j) ∧ k
  _ = refl

  _ : i ∧ i ≡ i
  _ = refl

  _ : i ∨ j ≡ j ∨ i
  _ = refl

  _ : i ∨ (j ∨ k) ≡ (i ∨ j) ∨ k
  _ = refl

  _ : i ∨ i ≡ i
  _ = refl

  _ : i ∨ i1 ≡ i1
  _ = refl

  _ : i ∨ i0 ≡ i
  _ = refl

  _ : i1 ∨ i ≡ i1
  _ = refl

  _ : i0 ∨ i ≡ i
  _ = refl

  _ : ~ i0 ≡ i1
  _ = refl

  _ : ~ i1 ≡ i0
  _ = refl

  _ : ~ (~ i) ≡ i
  _ = refl

  _ : ~ (i ∧ j) ≡ ~ i ∨ ~ j
  _ = refl

  _ : ~ (i ∨ j) ≡ ~ i ∧ ~ j
  _ = refl

  _ : i ∧ (j ∨ k) ≡ (i ∧ j) ∨ (i ∧ k)
  _ = refl

  _ : i ∨ (j ∧ k) ≡ (i ∨ j) ∧ (i ∨ k)
  _ = refl

module Postulates where
  postulate
    i j k : I

  _ : i ∧ i1 ≡ i
  _ = refl

  _ : i ∧ i0 ≡ i0
  _ = refl

  _ : i1 ∧ i ≡ i
  _ = refl

  _ : i0 ∧ i ≡ i0
  _ = refl

  _ : i ∧ j ≡ j ∧ i
  _ = refl

  _ : i ∧ (j ∧ k) ≡ (i ∧ j) ∧ k
  _ = refl

  _ : i ∧ i ≡ i
  _ = refl

  _ : i ∨ j ≡ j ∨ i
  _ = refl

  _ : i ∨ (j ∨ k) ≡ (i ∨ j) ∨ k
  _ = refl

  _ : i ∨ i ≡ i
  _ = refl

  _ : i ∨ i1 ≡ i1
  _ = refl

  _ : i ∨ i0 ≡ i
  _ = refl

  _ : i1 ∨ i ≡ i1
  _ = refl

  _ : i0 ∨ i ≡ i
  _ = refl

  _ : ~ i0 ≡ i1
  _ = refl

  _ : ~ i1 ≡ i0
  _ = refl

  _ : ~ (~ i) ≡ i
  _ = refl

  _ : ~ (i ∧ j) ≡ ~ i ∨ ~ j
  _ = refl

  _ : ~ (i ∨ j) ≡ ~ i ∧ ~ j
  _ = refl

  _ : i ∧ (j ∨ k) ≡ (i ∧ j) ∨ (i ∧ k)
  _ = refl

  _ : i ∨ (j ∧ k) ≡ (i ∨ j) ∧ (i ∨ k)
  _ = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Every respectful unary relation induces a preorder. No claim is
-- made that this preorder is unique.
------------------------------------------------------------------------

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

open import Relation.Binary
open import Relation.Unary using (Pred)

module Relation.Binary.Construct.FromPred
  {s₁ s₂} (S : Setoid s₁ s₂)          -- The underlying equality
  {p} (P : Pred (Setoid.Carrier S) p) -- The predicate
  where

open import Function
open import Data.Product

open module Eq = Setoid S using (_≈_) renaming (Carrier to A)

------------------------------------------------------------------------
-- Definition

Resp : Rel A p
Resp x y = P x → P y

------------------------------------------------------------------------
-- Properties

reflexive : P Respects _≈_ → _≈_ ⇒ Resp
reflexive resp = resp

refl : P Respects _≈_ → Reflexive Resp
refl resp = resp Eq.refl

trans : Transitive Resp
trans x⇒y y⇒z = y⇒z ∘ x⇒y

isPreorder : P Respects _≈_ → IsPreorder _≈_ Resp
isPreorder resp = record
  { isEquivalence = Eq.isEquivalence
  ; reflexive     = reflexive resp
  ; trans         = flip _∘′_
  }

preorder : P Respects _≈_ → Preorder _ _ _
preorder resp = record
  { isPreorder = isPreorder resp
  }


text:
module Dave.Structures.Monoid where
    open import Dave.Structures.Semigroup public

    record Identity {A : Set} (_·_ : op₂ A) (e : A) : Set where
        field
            left : left-identity _·_ e
            right : right-identity _·_ e

    record IsMonoid {A : Set} (_·_ : op₂ A) (e : A) : Set where
        field
            semigroup : IsSemigroup _·_
            identity : Identity _·_ e

    record Monoid : Set₁ where
        field
            Carrier : Set
            _·_ : op₂ Carrier
            e : Carrier
            isMonoid : IsMonoid _·_ e

    record IsCommutativeMonoid {A : Set} (_·_ : op₂ A) (e : A) : Set where
        field
            isSemigroup : IsSemigroup _·_
            leftIdentity : left-identity _·_ e
            comm : commutative _·_

        rightIdentity : right-identity _·_ e
        rightIdentity m = begin
            m · e ≡⟨ comm m e ⟩
            e · m ≡⟨ leftIdentity m ⟩
            m ∎

        identity : Identity _·_ e
        Identity.left identity = leftIdentity
        Identity.right identity = rightIdentity

        isMonoid : IsMonoid _·_ e
        IsMonoid.semigroup isMonoid = isSemigroup
        IsMonoid.identity isMonoid = identity

        swap021 : ∀ (m n p : A) → (m · n) · p ≡ (m · p) · n
        swap021 m n p = begin
            (m · n) · p ≡⟨ IsSemigroup.assoc isSemigroup m n p ⟩
            m · (n · p) ≡⟨ cong (λ a → m · a) (comm n p) ⟩
            m · (p · n) ≡⟨ sym (IsSemigroup.assoc isSemigroup m p n) ⟩
            (m · p) · n ∎

        swap102 : ∀ (m n p : A) → (m · n) · p ≡ (n · m) · p
        swap102 m n p = begin
            (m · n) · p ≡⟨ cong (λ a → a · p) (comm m n) ⟩
            (n · m) · p ∎

        swap120 : ∀ (m n p : A) → (m · n) · p ≡ (n · m) · p
        swap120 m n p = begin
            (m · n) · p ≡⟨ cong (λ a → a · p) (comm m n) ⟩
            (n · m) · p ∎

        swap210 : ∀ (m n p : A) → (m · n) · p ≡ (p · n) · m
        swap210 m n p = begin
            (m · n) · p ≡⟨ comm (m · n) p ⟩
            p · (m · n) ≡⟨ cong (λ a → p · a) (comm m n) ⟩
            p · (n · m) ≡⟨ sym (IsSemigroup.assoc isSemigroup p n m) ⟩
            (p · n) · m ∎

        swap201 : ∀ (m n p : A) → (m · n) · p ≡ (p · m) · n
        swap201 m n p = begin
            (m · n) · p ≡⟨ comm (m · n) p ⟩
            p · (m · n) ≡⟨ sym (IsSemigroup.assoc isSemigroup p m n) ⟩
            (p · m) · n ∎

    record CommutativeMonoid : Set₁ where
        field
            Carrier : Set
            _·_ : op₂ Carrier
            e : Carrier
            isCommutativeMonoid : IsCommutativeMonoid _·_ e


text:
-- Andreas, 2016-02-02, issue reported by Nisse

record R : Set₁ where
  field F : Set

postulate r : R

open R r using (F)

S : Set
S = F

-- Run "Explain why a particular name is in scope" (C-c C-w) for F.
-- Expected result:
--
-- F is in scope as
--   * a record field Issue1804._.F brought into scope by
--     - the application of R at ...
--     - its definition at ...


text:
module Oscar.Property.Reflexivity where

open import Oscar.Level

record Reflexivity {𝔬} {⋆ : Set 𝔬} {ℓ} (_≣_ : ⋆ → ⋆ → Set ℓ) : Set (𝔬 ⊔ ℓ) where
  field
    reflexivity : ∀ x → x ≣ x

open Reflexivity ⦃ … ⦄ public


text:
module Selective.Examples.PingPong where

open import Selective.ActorMonad public
open import Prelude

-- An example including three actors: spawner, pinger, ponger
--
-- Spawner is the actor that starts it all.
-- Spawner spawns both pinger and ponger.
-- Then spawner send the reference of ponger to pinger,
-- and the reference of pinger to ponger.
--
-- Pinger is an actor that can receive Bool messages.
-- Pinger counts the number of 'false' messages it receives, until it receives a 'true'
--
-- Ponger is an actor that can receive Nat messages.
-- Ponger keeps sending 'false' until it receives a message containing 10.

Spawnbox : InboxShape
Spawnbox = []

ℕ₁ : Set₁
ℕ₁ = Lift (lsuc lzero) ℕ

Bool₁ : Set₁
Bool₁ = Lift (lsuc lzero) Bool

mutual
  PingValues = [ Bool ]ˡ
  PongValues = [ ℕ ]ˡ

  PingRefs : TypingContext
  PingRefs = [ ⊠-of-values PongValues ]ˡ
  PongRefs : TypingContext
  PongRefs = [ ⊠-of-values PingValues ]ˡ

  PongReferenceMessage : MessageType
  PongReferenceMessage = [ ReferenceType (⊠-of-values PongValues) ]ˡ

  BoolMessage : MessageType
  BoolMessage = [ ValueType Bool ]ˡ

  Pingbox : InboxShape
  Pingbox = BoolMessage ∷ [ PongReferenceMessage ]ˡ

  PingReferenceMessage : MessageType
  PingReferenceMessage = [ ReferenceType (⊠-of-values PingValues) ]ˡ

  NatMessage : MessageType
  NatMessage = [ ValueType ℕ ]ˡ

  Pongbox : InboxShape
  Pongbox = NatMessage ∷ [ PingReferenceMessage ]ˡ

constPingrefs : {A : Set₁} → (A → TypingContext)
constPingrefs _ =  PingRefs

pingMainActor : (i : Size) (A : Set₁) → Set₂
pingMainActor i A = ∞ActorM i Pingbox A PingRefs constPingrefs

pinger : ∀ {i} → ∞ActorM (↑ i) Pingbox ⊤₁ [] constPingrefs
pinger .force = waitForPong ∞>> pingMain 0
  where
    waitForPong : ∀ {i} → ∞ActorM i Pingbox ⊤₁ [] constPingrefs
    waitForPong = selective-receive (λ {
      (Msg Z _) → false
      ; (Msg (S Z) _) → true
      ; (Msg (S (S ())) _)
      }) >>= λ {
        record { msg = (Msg Z _) ; msg-ok = () }
        ; record { msg = (Msg (S Z) _) ; msg-ok = refl } → return _
        ; record { msg = (Msg (S (S ())) x₁) }
      }
    waitForPingValue : ∀ {i Γ} → ∞ActorM i Pingbox Bool₁ Γ (λ _ → Γ)
    waitForPingValue = selective-receive (λ {
      (Msg Z _) → true
      ; (Msg (S Z) _) → false
      ; (Msg (S (S ())) _)
      }) >>= λ {
      record { msg = (Msg Z (b ∷ [])) ; msg-ok = refl } → return b
      ; record { msg = (Msg (S Z) _) ; msg-ok = () }
      ; record { msg = (Msg (S (S ())) x₁) }
      }
    pingMain : ∀ {i} → ℕ → pingMainActor i ⊤₁
    pingMain n .force = waitForPingValue ∞>>= λ
      { (lift false) → (Z ![t: Z ] ([ lift n ]ᵃ)) >> pingMain (suc n)
      ; (lift true) → return _}

constPongrefs : {A : Set₁} → (A → TypingContext)
constPongrefs _ = PongRefs

pongMainActor : (i : Size) (A : Set₁) → Set₂
pongMainActor i A = ∞ActorM i Pongbox A PongRefs constPongrefs

ponger : ∀ {i} → ∞ActorM (↑ i) Pongbox ⊤₁ [] constPongrefs
ponger .force = waitForPing ∞>> ((Z ![t: Z ] ([ lift false ]ᵃ)) >> pongMain)
  where
    waitForPing : ∀ {i} → ∞ActorM i Pongbox ⊤₁ [] constPongrefs
    waitForPing = selective-receive (λ {
      (Msg Z _) → false
      ; (Msg (S Z) _) → true
      ; (Msg (S (S ())) _)
      }) >>= λ {
        record { msg = (Msg Z _) ; msg-ok = () }
        ; record { msg = (Msg (S Z) x₁) ; msg-ok = refl } → return _
        ; record { msg = (Msg (S (S ())) x₁) }
        }
    waitForPongValue : ∀ {i Γ} → ∞ActorM i Pongbox ℕ₁ Γ (λ _ → Γ)
    waitForPongValue = selective-receive (λ {
      (Msg Z _) → true
      ; (Msg (S Z) _) → false
      ; (Msg (S (S ())) _)
      }) >>= λ {
        record { msg = (Msg Z (n ∷ [])) ; msg-ok = refl } → return n
        ; record { msg = (Msg (S Z) x₁) ; msg-ok = () }
        ; record { msg = (Msg (S (S ())) x₁) }
        }
    pongMain : ∀ {i} → pongMainActor i ⊤₁
    pongMain .force = waitForPongValue ∞>>= λ {
      (lift 10) → Z ![t: Z ] [ lift true ]ᵃ
      ; (lift n) → Z ![t: Z ] [ lift false ]ᵃ >> pongMain
      }

spawner : ∀ {i} → ∞ActorM i Spawnbox ⊤₁ [] (λ _ → Pingbox ∷ [ Pongbox ]ˡ)
spawner = do
  spawn∞ ponger
  spawn∞ pinger
  Z ![t: S Z ] [ [ S Z ]>: [ Z ]ᵐ ]ᵃ
  S Z ![t: S Z ] [ [ Z ]>: [ Z ]ᵐ ]ᵃ

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
-- Minimal implicational logic, vector-based de Bruijn approach, initial encoding

module Vi.ArrMp where

open import Lib using (Nat; suc; _+_; Fin; fin; Vec; _,_; proj; VMem; mem)

-- Types

infixr 0 _=>_
data Ty : Set where
  UNIT :             Ty
  _=>_ : Ty -> Ty -> Ty

-- Context and truth judgement

Cx : Nat -> Set
Cx n = Vec Ty n

isTrue : forall {tn} -> Ty -> Fin tn -> Cx tn -> Set
isTrue a i tc = VMem a i tc

-- Terms

module ArrMp where
  infixr 0 lam=>_
  infixl 1 _$_
  data Tm {tn} (tc : Cx tn) : Ty -> Set where
    var    : forall {a i} -> isTrue a i tc             -> Tm tc a
    lam=>_ : forall {a b} -> Tm (tc , a) b             -> Tm tc (a => b)
    _$_    : forall {a b} -> Tm tc (a => b) -> Tm tc a -> Tm tc b

  v : forall {tn} (k : Nat) {tc : Cx (suc (k + tn))} -> Tm tc (proj tc (fin k))
  v i = var (mem i)

  Thm : Ty -> Set
  Thm a = forall {tn} {tc : Cx tn} -> Tm tc a
open ArrMp public

-- Example theorems

aI : forall {a} -> Thm (a => a)
aI =
  lam=> v 0

aK : forall {a b} -> Thm (a => b => a)
aK =
  lam=>
    lam=> v 1

aS : forall {a b c} -> Thm ((a => b => c) => (a => b) => a => c)
aS =
  lam=>
    lam=>
      lam=> v 2 $ v 0 $ (v 1 $ v 0)

tSKK : forall {a} -> Thm (a => a)
tSKK {a = a} =
  aS {b = a => a} $ aK $ aK

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
-- From Dimytro Starosud
-- https://github.com/dima-starosud/Uniqueness-typing-in-Agda/blob/master/RefAPITest.agda
module Issue784 where

open import Issue784.RefAPI

open import Function
open import Data.Nat
open import Data.Product

-- new : ∀ a n → Transformer! [] [(n , Unique (Ref-ℕ a))]
{-Here also doesn't work without type constraint.
  Note: that type is exactly the same as of new-ℕ !!!
-}
new = new-ℕ
_++ = inc-ℕ
*_ = get-ℕ
free = free-ℕ

tr : (n : ℕ) → Transformer! [] [(_ , Pure (Exact $ suc n))]
tr i = "r" := new i ⇒⟦ refl ⟧⇒  -- new ℕ(i)
       "r" ++       ⇒⟦ refl ⟧⇒  -- r++
       "j" := * "r" ⇒⟦ refl ⟧⇒  -- j := *r
       free "r"

p : ∀ n → getExact (extract $ tr n) ≡ suc n
p = ≡-exact ∘ extract ∘ tr

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
import      Lvl
open import Structure.Operator.Vector
open import Structure.Setoid
open import Type

module Structure.Operator.Vector.LinearCombination
  {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ}
  {V : Type{ℓᵥ}} ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  {S : Type{ℓₛ}} ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  {_+ᵥ_ : V → V → V}
  {_⋅ₛᵥ_ : S → V → V}
  {_+ₛ_ _⋅ₛ_ : S → S → S}
  ⦃ vectorSpace : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_) ⦄
  where

open VectorSpace(vectorSpace)

open import Data.Tuple using (_⨯_ ; _,_)
open import Functional using (id ; _∘_ ; _∘₂_ ; _$_ ; swap ; _on₂_)
open import Function.Equals
open import Logic
open import Logic.Predicate
open import Numeral.CoordinateVector as Vec using () renaming (Vector to Vec)
open import Numeral.Finite
open import Numeral.Natural
open import Sets.ExtensionalPredicateSet as PredSet using (PredSet ; _∈_ ; [∋]-binaryRelator)
open import Structure.Function.Domain
open import Syntax.Function

private variable ℓ ℓₗ : Lvl.Level
private variable n : ℕ

-- A linear combination constructed from a sequence of vectors and a sequence of scalars.
-- Linear combination of 0 scalars and vectors are the zero vector.
-- Linear combination of 1 scalar and vector is just scalar on vector multiplication.
-- Example: LinearCombination {4} sf vf = (sf[0] ⋅ₛᵥ vf[0]) +ᵥ (sf[1] ⋅ₛᵥ vf[1]) +ᵥ (sf[2] ⋅ₛᵥ vf[2]) +ᵥ (sf[3] ⋅ₛᵥ vf[3])
-- Inlined definition:
--   LinearCombination {0}       _  _  = 𝟎ᵥ
--   LinearCombination {1}       vf sf = Vec.proj(sf)(0) ⋅ₛᵥ Vec.proj(vf)(0)
--   LinearCombination {𝐒(𝐒(n))} vf sf = (Vec.proj(sf)(0) ⋅ₛᵥ Vec.proj(vf)(0)) +ᵥ (LinearCombination {𝐒(n)} (Vec.tail vf) (Vec.tail sf))
linearCombination : Vec(n)(V) → Vec(n)(S) → V
linearCombination = Vec.reduceOrᵣ(_+ᵥ_) 𝟎ᵥ ∘₂ Vec.map₂(_⋅ᵥₛ_)

-- Whether the two specified vectors are linearly dependent or not.
-- TODO: Is this definition neccessary?
LinearlyDependentPair : V → V → Stmt
LinearlyDependentPair v₁ v₂ = ∃{Obj = S ⨯ S}(\{(s₁ , s₂) → s₁ ⋅ₛᵥ v₁ ≡ s₂ ⋅ₛᵥ v₂})

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Cardinality.Finite.ManifestEnumerable.Inductive where

open import Prelude
open import Data.List public
open import Data.List.Membership public

ℰ : Type a → Type a
ℰ A = Σ[ xs ⦂ List A ] Π[ x ⦂ A ] ∥ x ∈ xs ∥

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module interactiveProgramsAgdaUnsized where

open import NativeIO
open import Function

record IOInterface : Set₁ where
  field  Command   :  Set
         Response  :  (c : Command) → Set

open IOInterface public

mutual
  record IO (I : IOInterface)  (A : Set) : Set where
     coinductive
     constructor delay
     field force : IO' I A

  data IO' (I : IOInterface)  (A : Set) : Set where
    do'     : (c : Command I) (f : Response I c → IO I A)  → IO' I A
    return' : (a : A)                                       → IO' I A

open IO public

module _ {I : IOInterface} (let C = Command I) (let R = Response I) where
  do  : ∀{A} (c : C) (f : R c → IO I A) → IO I A
  force (do c f) = do' c f

  return : ∀{A} (a : A) → IO I A
  force (return a) = return' a

  infixl 2 _>>=_

  _>>=_ :  ∀{A B} (m : IO I A) (k : A → IO I B) → IO I B
  force (m >>= k) with force m
  ... | do' c f   = do' c λ x → f x >>= k
  ... | return' a = force (k a)

  {-# NON_TERMINATING #-}
  translateIO : ∀ {A} (tr : (c : C) → NativeIO (R c)) → IO I A → NativeIO A
  translateIO tr m = case (force m) of λ
     {  (do' c f)    →  (tr c) native>>= λ r → translateIO tr (f r)
     ;  (return' a)  →  nativeReturn a
     }

data ConsoleCommand : Set where
  getLine   :  ConsoleCommand
  putStrLn  :  String → ConsoleCommand

ConsoleResponse : ConsoleCommand → Set
ConsoleResponse  getLine      =  String
ConsoleResponse (putStrLn s)  =  Unit

ConsoleInterface : IOInterface
Command ConsoleInterface  = ConsoleCommand
Response ConsoleInterface = ConsoleResponse

IOConsole : Set → Set
IOConsole = IO ConsoleInterface

translateIOConsoleLocal : (c : ConsoleCommand) → NativeIO (ConsoleResponse c)
translateIOConsoleLocal (putStrLn s)  =  nativePutStrLn s
translateIOConsoleLocal getLine       =  nativeGetLine

translateIOConsole : {A : Set} → IOConsole A → NativeIO A
translateIOConsole = translateIO translateIOConsoleLocal

{-# NON_TERMINATING #-}
cat   :  IOConsole Unit
force cat =  do' getLine λ{ line →
             do (putStrLn line)   λ _ →
             cat
             }

mutual
  cat' :  IOConsole Unit
  force cat' =  do' getLine λ{ line →
                cat'' line}

  cat'' : String → IOConsole Unit
  force (cat'' line) = do' (putStrLn line)   λ _ →
                       cat'

main : NativeIO Unit
main = translateIOConsole cat

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
------------------------------------------------------------------------------
-- Testing a type synonymous for Set
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.SetType where

open import FOTC.Base
open import FOTC.Data.Nat

-- Type synonymous for Set.
Type = Set

data N' : D → Type where
  nzero' : N' zero
  nsucc' : ∀ {n} → N' n → N' (succ₁ n)
{-# ATP axioms nzero' nsucc' #-}

pred-N' : ∀ {n} → N' n → N' (pred₁ n)
pred-N' nzero' = prf
  where postulate prf : N' (pred₁ zero)
        {-# ATP prove prf #-}

pred-N' (nsucc' {n} N'n) = prf
  where postulate prf : N' (pred₁ (succ₁ n))
        {-# ATP prove prf #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- This file needs to exist because the Makefile dependencies require a *.agda file.
-- The actual test is in Issue2937.sh which uses two files under Issue2737/*.agda


text:
{-# OPTIONS --without-K --safe #-}
module Source.Type where

open import Source.Size as S using
  ( Size ; Δ ; Δ′ ; Δ″ ; Ω ; Ω′ ; Ω″ ; n ; m ; o ; p ; b )
open import Source.Size.Substitution.Canonical as SC using
  ( Sub⊢ )
open import Source.Size.Substitution.Theory
open import Source.Size.Substitution.Universe as SU using
  ( σ ; τ ; ι ; ⟨_⟩ )
open import Util.Prelude

open S.Ctx

infixr 3 Π_,_
infixr 4 _⇒_
infixl 4 _∙_

data Type (Δ : S.Ctx) : Set where
  Nat : (n : Size Δ) → Type Δ
  Stream : (n : Size Δ) → Type Δ
  _⇒_ : (T U : Type Δ) → Type Δ
  Π_,_ : (n : Size Δ) (T : Type (Δ ∙ n)) → Type Δ

variable T U V W T′ U′ V′ W′ : Type Δ

Π-≡⁺ : ∀ {n m} {T : Type (Δ ∙ n)} {U : Type (Δ ∙ m)}
  → (n≡m : n ≡ m)
  → subst (λ n → Type (Δ ∙ n)) n≡m T ≡ U
  → (Π n , T) ≡ (Π m , U)
Π-≡⁺ refl refl = refl

data Ctx (Δ : S.Ctx) : Set where
  [] : Ctx Δ
  _∙_ : (Γ : Ctx Δ) (T : Type Δ) → Ctx Δ

variable Γ Γ′ Γ″ Ψ Ψ′ Ψ″ : Ctx Δ

sub : SC.Sub Δ Ω → Type Ω → Type Δ
sub σ (Nat n) = Nat (SC.sub σ n)
sub σ (Stream n) = Stream (SC.sub σ n)
sub σ (T ⇒ U) = sub σ T ⇒ sub σ U
sub σ (Π n , T) = Π SC.sub σ n , sub (SC.Lift σ) T

abstract
  sub->> : ∀ {Δ Δ′ Δ″} (σ : SC.Sub Δ Δ′) (τ : SC.Sub Δ′ Δ″) T
    → sub (σ SC.>> τ) T ≡ sub σ (sub τ T)
  sub->> σ τ (Nat n) = cong Nat (SC.sub->> n refl)
  sub->> σ τ (Stream n) = cong Stream (SC.sub->> n refl)
  sub->> σ τ (T ⇒ U) = cong₂ _⇒_ (sub->> σ τ T) (sub->> σ τ U)
  sub->> σ τ (Π n , T)
    rewrite SC.sub->> {σ = σ} {τ} n refl
    = cong (λ T → Π SC.sub σ (SC.sub τ n) , T)
        (trans (cong (λ σ → sub σ T) (sym SC.Lift>>Lift))
          (sub->> (SC.Lift σ) (SC.Lift τ) T))

  sub-Id : (T : Type Δ) → sub SC.Id T ≡ T
  sub-Id (Nat n) = cong Nat (SC.sub-Id n refl)
  sub-Id (Stream n) = cong Stream (SC.sub-Id n refl)
  sub-Id (T ⇒ U) = cong₂ _⇒_ (sub-Id T) (sub-Id U)
  sub-Id (Π n , T)
    rewrite SC.sub-Id n refl
    = cong (λ T → Π n , T) (sub-Id T)

instance
  SubTheory-Type : SubTheory Type
  SubTheory-Type = record
    { _[_] = λ T σ → sub σ T
    ; [Id] = sub-Id
    ; [>>] = sub->>
    }

subΓ : SC.Sub Δ Ω → Ctx Ω → Ctx Δ
subΓ σ [] = []
subΓ σ (Γ ∙ T) = subΓ σ Γ ∙ sub σ T

abstract
  subΓ->> : ∀ (σ : SC.Sub Δ Δ′) (τ : SC.Sub Δ′ Δ″) Γ
    → subΓ (σ SC.>> τ) Γ ≡ subΓ σ (subΓ τ Γ)
  subΓ->> σ τ [] = refl
  subΓ->> σ τ (Γ ∙ T) = cong₂ _∙_ (subΓ->> σ τ Γ) (sub->> σ τ T)

  subΓ-Id : (Γ : Ctx Δ) → subΓ SC.Id Γ ≡ Γ
  subΓ-Id [] = refl
  subΓ-Id (Γ ∙ T) = cong₂ _∙_ (subΓ-Id Γ) (sub-Id T)

instance
  SubTheory-Ctx : SubTheory Ctx
  SubTheory-Ctx = record
    { _[_] = λ Γ σ → subΓ σ Γ
    ; [Id] = subΓ-Id
    ; [>>] = subΓ->>
    }

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module map-is-foldr where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; cong)
open Eq.≡-Reasoning
open import lists using (List; []; _∷_; map; foldr)

postulate
  -- 外延性の公理
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

-- 外延性の公理を利用した証明のための補題
lemma : ∀ {A B : Set} → (f : A → B) → (xs : List A)
  → map f xs ≡ foldr (λ x xs → f x ∷ xs) [] xs
lemma f [] =
  begin
    map f []
  ≡⟨⟩
    []
  ≡⟨⟩
    foldr (λ x xs → f x ∷ xs) [] []
  ∎
lemma f (x ∷ xs) =
  begin
    map f (x ∷ xs)
  ≡⟨⟩
    f x ∷ map f xs
  ≡⟨ cong (f x ∷_) (lemma f xs) ⟩
    f x ∷ foldr (λ x xs → f x ∷ xs) [] xs
  ≡⟨⟩
    foldr (λ x xs → f x ∷ xs) [] (x ∷ xs)
  ∎

-- mapが畳み込みで表現できることの証明
map-is-foldr : ∀ {A B : Set} → (f : A → B)
  → map f ≡ foldr (λ x xs → f x ∷ xs) []
map-is-foldr f = extensionality (lemma f)

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
module Proof-last-is-deterministic where

-- Show that last is a deterministic operation.
-- The property to show is:
--
-- l == l1 ++ [x1] and l == l2 ++ [x2]  implies x1 == x2
--
-- Here we show the simplified property
--
--  l1 ++ [x1] == l2 ++ [x2]  implies x1 == x2
--
-- The initial property can be derived from this one by by symmetry
-- and transitivity of Boolean equality.

open import bool
open import bool-thms
open import bool-thms2
open import list
open import nat
open import eq

-- Auxiliary statements: an empty list cannot be equal to a list with
-- an element at the end:
nonemptylast :  ∀ (l : 𝕃 ℕ)(x : ℕ) → =𝕃 _=ℕ_ [] (l ++ [ x ]) ≡ ff
nonemptylast [] x = refl
nonemptylast (z :: l) x = refl

nonemptylastr :  ∀ (l : 𝕃 ℕ)(x : ℕ) → =𝕃 _=ℕ_ (l ++ [ x ]) [] ≡ ff
nonemptylastr [] x = refl
nonemptylastr (z :: l) x = refl

-- Main property formulated as Boolean implication:
lasteqp : ∀ (l1 l2 : 𝕃 ℕ)(x1 x2 : ℕ)
            → (=𝕃 _=ℕ_ (l1 ++ [ x1 ]) (l2 ++ [ x2 ])) imp (x1 =ℕ x2) ≡ tt
lasteqp [] [] x1 x2 rewrite &&-tt (x1 =ℕ x2) | imp-same (x1 =ℕ x2) = refl
lasteqp [] (x :: l2) x1 x2
  rewrite nonemptylast l2 x2 | &&-ff (x1 =ℕ x) = refl
lasteqp (x :: l1) [] x1 x2
  rewrite nonemptylastr l1 x1 | &&-ff (x =ℕ x2) = refl
lasteqp (z1 :: l1) (z2 :: l2) x1 x2 with (z1 =ℕ z2)
lasteqp (z1 :: l1) (z2 :: l2) x1 x2 | tt
  rewrite lasteqp l1 l2 x1 x2 = refl
lasteqp (z1 :: l1) (z2 :: l2) x1 x2 | ff = refl

-- Main property formulated as propositional implication:
lasteq : ∀ (l1 l2 : 𝕃 ℕ)(x1 x2 : ℕ)
            → =𝕃 _=ℕ_ (l1 ++ [ x1 ]) (l2 ++ [ x2 ]) ≡ tt
            → x1 =ℕ x2 ≡ tt
lasteq l1 l2 x1 x2 p = imp-mp (lasteqp l1 l2 x1 x2) p

max_stars_repo_name: phlummox/curry-tools

max_issues_repo_name: phlummox/curry-tools

max_forks_repo_name: phlummox/curry-tools


text:
module Haskell.Prim.Absurd where

open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Unit
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_; absurd to absurdP)
open import Agda.Builtin.Equality

open import Haskell.Prim

private

  pattern vArg x = arg (arg-info visible relevant) x

  refute : Nat → Term
  refute i = def (quote _$_) (vArg (pat-lam (absurd-clause (vArg absurdP ∷ []) ∷ []) []) ∷ vArg (var i []) ∷ [])

  tryRefute : Nat → Term → TC ⊤
  tryRefute 0       _    = typeError (strErr "No variable of empty type found in the context" ∷ [])
  tryRefute (suc n) hole = catchTC (unify hole (refute n)) (tryRefute n hole)

absurd : Term → TC ⊤
absurd hole = do
  Γ ← getContext
  tryRefute (lengthNat Γ) hole


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

module Data.ByteVec where

import Data.ByteString as BS
open import Data.Word8 using (Word8)
open BS using (ByteString; length)
open import Data.Nat using (ℕ; _<_)
open import Data.Product using (Σ; _,_; proj₁; proj₂)

open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (True)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)

open BS public using (ByteStringKind; Lazy; Strict)

ByteVec : ∀ {k} → ℕ → Set
ByteVec {k} n = Σ (ByteString k) (λ bs → n ≡ length bs)

mkVec′ : ∀ {k} → (bs : ByteString k) → ByteVec {k} (length bs)
mkVec′ {k} bs = bs , refl

mkVec : ∀ {k} (n : ℕ) (bs : ByteString k)
  → (n≡∣bs∣ : n ≡ length bs)
  → ByteVec {k} n
mkVec {k} n = _,_

primMkVec : ∀ {k n} → ByteString k → ByteVec {k} n
primMkVec bs = bs , trustMe

index : ∀ {k n} → ByteVec {k} n → (ix : ℕ) → {ix<n : ix < n} → Word8
index (bs , _) ix {_} = BS.unsafeIndex bs ix

module test where
  open import Data.ByteString.Utf8 using (packStrict)
  -- bv5 : ByteVec {_} 5
  -- bv5 = packStrict "asdef" Σ., {!!}
  bv′ : _
  bv′ = mkVec′ (packStrict "asdef")

infix 4 _≟_

private
  t : ∀ {n k} → {v : ByteString k} → (us vs : n ≡ length v) → us ≡ vs
  t us vs = trustMe -- only one proof: refl

_≟_ : ∀ {k n} → Decidable {A = ByteVec {k} n} _≡_
_≟_ {n = n} (u , us) (v , vs) with u BS.≟ v
_≟_ {n = n} (u , us) (v , vs) | yes p rewrite p | t us vs = yes refl
_≟_ {n = n} (u , us) (v , vs) | no ¬p = no (λ x → ¬p (cong proj₁ x))

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


text:
module Haskell.Prim.Show where

open import Agda.Builtin.Char
open import Agda.Builtin.Nat
import Agda.Builtin.String as Str

open import Haskell.Prim
open import Haskell.Prim.String
open import Haskell.Prim.List
open import Haskell.Prim.Word
open import Haskell.Prim.Double
open import Haskell.Prim.Maybe
open import Haskell.Prim.Eq
open import Haskell.Prim.Tuple
open import Haskell.Prim.Ord
open import Haskell.Prim.Either
open import Haskell.Prim.Integer
open import Haskell.Prim.Bool
open import Haskell.Prim.Int
open import Haskell.Prim.Foldable

--------------------------------------------------
-- Show

ShowS : Set
ShowS = String → String

showChar : Char → ShowS
showChar = _∷_

showString : String → ShowS
showString = _++_

showParen : Bool → ShowS → ShowS
showParen false s = s
showParen true  s = showString "(" ∘ s ∘ showString ")"

record Show (a : Set) : Set where
  field
    showsPrec : Int → a → ShowS
    showList  : List a → ShowS

  shows : a → ShowS
  shows = showsPrec 0

  show : a → String
  show x = shows x ""

defaultShowList : (a → ShowS) → List a → ShowS
defaultShowList _     []       = showString "[]"
defaultShowList shows (x ∷ xs) = showString "[" ∘ foldl (λ s x → s ∘ showString "," ∘ shows x) (shows x) xs ∘ showString "]"

open Show ⦃ ... ⦄ public

private
  makeShow : (a → String) → Show a
  makeShow sh .showsPrec _ = showString ∘ sh
  makeShow sh .showList    = defaultShowList (showString ∘ sh)

  makeShowsPrec : (Int → a → ShowS) → Show a
  makeShowsPrec shp .showsPrec = shp
  makeShowsPrec shp .showList = defaultShowList (shp 0)

instance
  iShowNat : Show Nat
  iShowNat = makeShow (Str.primStringToList ∘ Str.primShowNat)

  iShowInteger : Show Integer
  iShowInteger = makeShow showInteger

  iShowInt : Show Int
  iShowInt = makeShow showInt

  iShowWord : Show Word
  iShowWord = makeShow showWord

  iShowDouble : Show Double
  iShowDouble = makeShow (Str.primStringToList ∘ primShowFloat)

  iShowBool : Show Bool
  iShowBool = makeShow λ where false → "False"; true → "True"

  iShowChar : Show Char
  iShowChar .showsPrec _ = showString ∘ Str.primStringToList ∘ Str.primShowChar
  iShowChar .showList    = showString ∘ Str.primStringToList ∘ Str.primShowString ∘ Str.primStringFromList

  iShowList : ⦃ Show a ⦄ → Show (List a)
  iShowList .showsPrec _ = showList
  iShowList .showList    = defaultShowList showList

private
  showApp₁ : ⦃ Show a ⦄ → Int → String → a → ShowS
  showApp₁ p tag x = showParen (p > 10) $ showString tag ∘ showString " " ∘ showsPrec 11 x

instance
  iShowMaybe : ⦃ Show a ⦄ → Show (Maybe a)
  iShowMaybe = makeShowsPrec λ where p Nothing  → showString "Nothing"
                                     p (Just x) → showApp₁ p "Just" x

  iShowEither : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (Either a b)
  iShowEither = makeShowsPrec λ where p (Left  x) → showApp₁ p "Left"  x
                                      p (Right y) → showApp₁ p "Right" y

private
  -- Minus the parens
  showTuple : ∀ {as} → ⦃ All Show as ⦄ → Tuple as → ShowS
  showTuple             []       = showString ""
  showTuple ⦃ allCons ⦄ (x ∷ []) = shows x
  showTuple ⦃ allCons ⦄ (x ∷ xs) = shows x ∘ showString "," ∘ showTuple xs

instance
  iShowTuple : ∀ {as} → ⦃ All Show as ⦄ → Show (Tuple as)
  iShowTuple = makeShowsPrec λ _ → showParen true ∘ showTuple


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Membership of vectors, along with some additional definitions.
------------------------------------------------------------------------

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

open import Relation.Binary using (Setoid; _Respects_)

module Data.Vec.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where

open import Function
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Data.Vec.Relation.Unary.Any as Any
  using (Any; here; there; index)
open import Data.Product using (∃; _×_; _,_)
open import Relation.Nullary using (¬_)
open import Relation.Unary using (Pred)

open Setoid S renaming (Carrier to A)

------------------------------------------------------------------------
-- Definitions

infix 4 _∈_ _∉_

_∈_ : A → ∀ {n} → Vec A n → Set _
x ∈ xs = Any (x ≈_) xs

_∉_ : A → ∀ {n} → Vec A n → Set _
x ∉ xs = ¬ x ∈ xs

------------------------------------------------------------------------
-- Operations

mapWith∈ : ∀ {b} {B : Set b} {n}
           (xs : Vec A n) → (∀ {x} → x ∈ xs → B) → Vec B n
mapWith∈ []       f = []
mapWith∈ (x ∷ xs) f = f (here refl) ∷ mapWith∈ xs (f ∘ there)

_∷=_ : ∀ {n} {xs : Vec A n} {x} → x ∈ xs → A → Vec A n
_∷=_ {xs = xs} x∈xs v = xs Vec.[ index x∈xs ]≔ v

------------------------------------------------------------------------
-- Finding and losing witnesses

module _ {p} {P : Pred A p} where

  find : ∀ {n} {xs : Vec A n} → Any P xs → ∃ λ x → x ∈ xs × P x
  find (here px)   = (_ , here refl , px)
  find (there pxs) with find pxs
  ... | (x , x∈xs , px) = (x , there x∈xs , px)

  lose : P Respects _≈_ → ∀ {x n} {xs : Vec A n} → x ∈ xs → P x → Any P xs
  lose resp x∈xs px = Any.map (flip resp px) x∈xs


text:
-- Andreas, 2017-12-16, issue #2873, reported by m0davis

-- Regression introduced by a fix of #737 that printed
-- the refinement candidate to concrete syntax
-- and ran the scope checker again to get back to abstract syntax.

-- {-# OPTIONS -v interaction:50 #-}

open import Agda.Builtin.Nat

data Vec {a} (A : Set a) : Nat → Set a where
  []  : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

module Fails where
  open import Agda.Builtin.List

  test : Vec Nat 1
  test = {!(_∷_) !} -- WAS: C-c C-r fails here

  test2 : Vec Nat 1
  test2 = {! !} -- WAS: C-c C-r fails here

module Succeeds where
  open import Agda.Builtin.List public

  test : Vec Nat 1
  test = {!!} -- C-c C-r succeeds here


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

module Function.Injective.Base where

open import Level
open import Path
open import Data.Sigma

Injective : (A → B) → Type _
Injective f = ∀ x y → (f⟨x⟩≡f⟨y⟩ : f x ≡ f y) → x ≡ y

infixr 0 _↣_
_↣_ : Type a → Type b → Type (a ℓ⊔ b)
A ↣ B = Σ[ f ⦂ (A → B) ] × Injective f
refl-↣ : A ↣ A
refl-↣ .fst x = x
refl-↣ .snd x y x≡y = x≡y

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --cubical #-}
module _ where

module _ where
  open import Agda.Primitive.Cubical public
  open import Agda.Builtin.Cubical.Path public

  refl : ∀ {a} {A : Set a} {x : A} → x ≡ x
  refl {x = x} = \ _ → x

-- Here there's no solution for H, pattern unification will try
-- H := \ i -> b, but the equality constraints from
-- H : Path b a should rule out that assignment.
testPath : ∀ {A : Set} {b a : A} (let H : b ≡ a; H = _) → ∀ i → H i ≡ b
testPath i = refl


text:
module Structure.Operator.Field.VectorSpace where

import      Lvl
open import Structure.Setoid
open import Structure.Operator.Field
open import Structure.Operator.Properties using (associativity ; identityₗ ; distributivityᵣ)
open import Structure.Operator.Vector
open import Structure.Operator
open import Type

private variable ℓ ℓₑ ℓₗ ℓₗₑ : Lvl.Level
private variable T : Type{ℓ}
private variable _+_ _⋅_ : T → T → T

module _
  ⦃ equiv : Equiv{ℓₑ}(T) ⦄
  ⦃ [+]-oper : BinaryOperator(_+_) ⦄
  ⦃ [⋅]-oper : BinaryOperator(_⋅_) ⦄
  (field-structure : Field{T = T}(_+_)(_⋅_))
  where
  open Field(field-structure)

  fieldVectorSpace : VectorSpace(_+_)(_⋅_)(_+_)(_⋅_)
  VectorSpace.scalarField                   fieldVectorSpace = field-structure
  VectorSpace.[⋅ₛᵥ]-binaryOperator          fieldVectorSpace = [⋅]-oper
  VectorSpace.[⋅ₛ][⋅ₛᵥ]-compatibility       fieldVectorSpace = associativity(_⋅_)
  VectorSpace.[⋅ₛᵥ][+ᵥ]-distributivityₗ     fieldVectorSpace = [⋅][+]-distributivityₗ
  VectorSpace.[⋅ₛᵥ][+ₛ][+ᵥ]-distributivityᵣ fieldVectorSpace = distributivityᵣ(_⋅_)(_+_)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

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

open import Algebra.Bundles

module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where

open Group G
open import Algebra.Definitions _≈_
open import Relation.Binary.Reasoning.Setoid setoid
open import Function
open import Data.Product

ε⁻¹≈ε : ε ⁻¹ ≈ ε
ε⁻¹≈ε = begin
  ε ⁻¹      ≈⟨ sym $ identityʳ (ε ⁻¹) ⟩
  ε ⁻¹ ∙ ε  ≈⟨ inverseˡ ε ⟩
  ε         ∎

private

  left-helper : ∀ x y → x ≈ (x ∙ y) ∙ y ⁻¹
  left-helper x y = begin
    x              ≈⟨ sym (identityʳ x) ⟩
    x ∙ ε          ≈⟨ ∙-congˡ $ sym (inverseʳ y) ⟩
    x ∙ (y ∙ y ⁻¹) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
    (x ∙ y) ∙ y ⁻¹ ∎

  right-helper : ∀ x y → y ≈ x ⁻¹ ∙ (x ∙ y)
  right-helper x y = begin
    y              ≈⟨ sym (identityˡ y) ⟩
    ε          ∙ y ≈⟨ ∙-congʳ $ sym (inverseˡ x) ⟩
    (x ⁻¹ ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
    x ⁻¹ ∙ (x ∙ y) ∎

∙-cancelˡ : LeftCancellative _∙_
∙-cancelˡ x {y} {z} eq = begin
              y  ≈⟨ right-helper x y ⟩
  x ⁻¹ ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩
  x ⁻¹ ∙ (x ∙ z) ≈˘⟨ right-helper x z ⟩
              z  ∎

∙-cancelʳ : RightCancellative _∙_
∙-cancelʳ {x} y z eq = begin
  y            ≈⟨ left-helper y x ⟩
  y ∙ x ∙ x ⁻¹ ≈⟨ ∙-congʳ eq ⟩
  z ∙ x ∙ x ⁻¹ ≈˘⟨ left-helper z x ⟩
  z            ∎

∙-cancel : Cancellative _∙_
∙-cancel = ∙-cancelˡ , ∙-cancelʳ

⁻¹-involutive : ∀ x → x ⁻¹ ⁻¹ ≈ x
⁻¹-involutive x = begin
  x ⁻¹ ⁻¹              ≈˘⟨ identityʳ _ ⟩
  x ⁻¹ ⁻¹ ∙ ε          ≈˘⟨ ∙-congˡ $ inverseˡ _ ⟩
  x ⁻¹ ⁻¹ ∙ (x ⁻¹ ∙ x) ≈˘⟨ right-helper (x ⁻¹) x ⟩
  x                    ∎

⁻¹-injective : ∀ {x y} → x ⁻¹ ≈ y ⁻¹ → x ≈ y
⁻¹-injective {x} {y} eq = ∙-cancelʳ x y ( begin
  x ∙ x ⁻¹ ≈⟨ inverseʳ x ⟩
  ε        ≈˘⟨ inverseʳ y ⟩
  y ∙ y ⁻¹ ≈˘⟨ ∙-congˡ eq ⟩
  y ∙ x ⁻¹ ∎ )

⁻¹-anti-homo-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x ⁻¹
⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ ( begin
  x ∙ y ∙ (x ∙ y) ⁻¹    ≈⟨ inverseʳ _ ⟩
  ε                     ≈˘⟨ inverseʳ _ ⟩
  x ∙ x ⁻¹              ≈⟨ ∙-congʳ (left-helper x y) ⟩
  (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩
  x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎ )

identityˡ-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε
identityˡ-unique x y eq = begin
  x              ≈⟨ left-helper x y ⟩
  (x ∙ y) ∙ y ⁻¹ ≈⟨ ∙-congʳ eq ⟩
       y  ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩
  ε              ∎

identityʳ-unique : ∀ x y → x ∙ y ≈ x → y ≈ ε
identityʳ-unique x y eq = begin
  y              ≈⟨ right-helper x y ⟩
  x ⁻¹ ∙ (x ∙ y) ≈⟨ refl ⟨ ∙-cong ⟩ eq ⟩
  x ⁻¹ ∙  x      ≈⟨ inverseˡ x ⟩
  ε              ∎

identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε
identity-unique {x} id = identityˡ-unique x x (proj₂ id x)

inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹
inverseˡ-unique x y eq = begin
  x              ≈⟨ left-helper x y ⟩
  (x ∙ y) ∙ y ⁻¹ ≈⟨ ∙-congʳ eq ⟩
       ε  ∙ y ⁻¹ ≈⟨ identityˡ (y ⁻¹) ⟩
            y ⁻¹ ∎

inverseʳ-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹
inverseʳ-unique x y eq = begin
  y       ≈⟨ sym (⁻¹-involutive y) ⟩
  y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (sym (inverseˡ-unique x y eq)) ⟩
  x ⁻¹    ∎

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.1

left-identity-unique = identityˡ-unique
{-# WARNING_ON_USAGE left-identity-unique
"Warning: left-identity-unique was deprecated in v1.1.
Please use identityˡ-unique instead."
#-}
right-identity-unique = identityʳ-unique
{-# WARNING_ON_USAGE right-identity-unique
"Warning: right-identity-unique was deprecated in v1.1.
Please use identityʳ-unique instead."
#-}
left-inverse-unique = inverseˡ-unique
{-# WARNING_ON_USAGE left-inverse-unique
"Warning: left-inverse-unique was deprecated in v1.1.
Please use inverseˡ-unique instead."
#-}
right-inverse-unique = inverseʳ-unique
{-# WARNING_ON_USAGE right-inverse-unique
"Warning: right-inverse-unique was deprecated in v1.1.
Please use inverseʳ-unique instead."
#-}


text:
module Category where

open import Agda.Primitive

open import Equality
open import Finite

record Category ℓ : Set (lsuc ℓ) where
  field
    obj : Set ℓ
    hom : obj → obj → Set ℓ
    id-hom : ∀ {x} → hom x x
    compose : ∀ {x y z} → hom y z → hom x y → hom x z
    compose-id-left : ∀ {x y} {f : hom x y} → compose id-hom f ≡ f
    compose-id-right : ∀ {x y} {f : hom x y} → compose f id-hom ≡ f
    compose-assoc : ∀ {x y z w} {f : hom x y} {g : hom y z} {h : hom z w} → compose (compose h g) f ≡ compose h (compose g f)

record FPCategory ℓ : Set (lsuc ℓ) where
  open Category

  field
    {{category}} : Category ℓ
    product : ∀ n (xs : Fin n → obj category) → obj category
    project : ∀ n {xs : Fin n → obj category} → ∀ (i : Fin n) → hom category (product n xs) (xs i)
    tuple : ∀ n {xs : Fin n → obj category} {y} → ∀ (f : ∀ i → hom category y (xs i)) → hom category y (product n xs)
    project-tuple : ∀ {n} {xs : Fin n → obj category} {y} {f : ∀ i → hom category y (xs i)} {j} →
                   compose category (project n j) (tuple n f) ≡ f j
    tuple-project : ∀ {n} {xs : Fin n → obj category} {y} {u v : hom category y (product n xs)} →
                   (∀ i → compose category (project n i) u ≡ compose category (project n i) v) → u ≡ v

  tuple-hom : ∀ n {xs ys : Fin n → obj category} (f : ∀ i → hom category (xs i) (ys i)) →
              hom category (product n xs) (product n ys)
  tuple-hom n f = tuple n (λ i → compose category (f i) (project n i))

  power : ℕ → obj category → obj category
  power n x = product n (λ _  → x)

  power-hom : ∀ n {x y : obj category} → hom category x y → hom category (power n x) (power n y)
  power-hom n f = tuple-hom n (λ i → f)

  terminal-obj : obj category
  terminal-obj = product Z (λ ())

  terminal-hom : ∀ {x : obj category} → hom category x terminal-obj
  terminal-hom = tuple Z (λ ())

  terminal-eq : ∀ {x : obj category} {f g : hom category x terminal-obj} → f ≡ g
  terminal-eq {x} {f} {g} = tuple-project λ ()

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


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

open import Agda.Primitive

data _≡_ {a} {A : Set a} (x : A) : A → Set where
  refl : x ≡ x


text:
-- Andreas and James, Nov 2011 and Oct 2012
-- function with flexible arity
-- {-# OPTIONS --no-coverage-check #-}
-- {-# OPTIONS -v tc.cover:20 #-}
module FlexibleInterpreter where

open import Common.Prelude using (Nat; zero; suc)
open import Common.MAlonzo hiding (main)
open import Common.Equality

data Ty : Set where
  nat : Ty
  arr : Ty -> Ty -> Ty

data Exp : Ty -> Set where
  zero : Exp nat
  suc  : Exp (arr nat nat)
  pred : Exp (arr nat nat)
  app  : {a b : Ty} -> Exp (arr a b) -> Exp a -> Exp b

Sem : Ty -> Set
Sem nat = Nat
Sem (arr a b) = Sem a -> Sem b

module Flex where
  -- Haskell does not seem to handle this

  eval' : (a : Ty) -> Exp a -> Sem a
  eval' ._ zero = zero
  eval' ._ suc  = suc
  eval' b (app f e) = eval' _ f (eval' _ e)
  eval' .(arr nat nat) pred zero = zero
  eval' ._ pred (suc n) = n

  eval : {a : Ty} -> Exp a -> Sem a
  eval zero         = zero
  eval suc          = suc
  eval pred zero    = zero
  eval pred (suc n) = n
  eval (app f e)    = eval f (eval e)

  testEvalSuc : ∀ {n} → eval suc n ≡ suc n
  testEvalSuc = refl

  testEvalPredZero : eval pred zero ≡ zero
  testEvalPredZero = refl

  testEvalPredSuc : ∀ {n} → eval pred (suc n) ≡ n
  testEvalPredSuc = refl

module Rigid where
  -- This executes fine

  eval : {a : Ty} -> Exp a -> Sem a
  eval zero      = zero
  eval suc       = suc
  eval pred      = λ { zero    -> zero
                     ; (suc n) -> n
                     }
  eval (app f e) = eval f (eval e)

open Flex

expr = (app pred (app suc (app suc zero)))
test = eval expr
main = mainPrintNat test
-- should print 1


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Fun.Facts.Limit where

open import Data.Product using (_,_)

open import Cats.Category
open import Cats.Category.Cat.Facts.Exponential using (Eval ; Curry ; Uncurry)
open import Cats.Category.Cat.Facts.Product using (Swap)
open import Cats.Category.Cones as Cones using (Cone ; Apex ; arr ; commute)
open import Cats.Category.Fun using (≈-intro ; ≈-elim) renaming (Fun to _↝_)
open import Cats.Category.Product.Binary using (_×_)
open import Cats.Functor using (Functor ; _∘_)
open import Cats.Limit using (Limit ; IsLimit ; Complete ; trans ; arr∘trans)
open import Cats.Trans using (Trans ; component ; natural)

open Functor
open Limit

instance
  -- Good lord this proof...
  complete : ∀ {lo la l≈ lo′ la′ l≈′ lo″ la″ l≈″}
    → {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
    → {{_ : Complete D lo″ la″ l≈″}}
    → Complete (C ↝ D) lo″ la″ l≈″
  complete {C = C} {D} {{D-complete}} .Complete.lim′ {J} F = record
    { cone = record
      { Apex = DC.limF ∘ F′
      ; arr = λ j → record
        { component = λ c → DC.lim′ (fobj F′ c) .arr j
        ; natural = λ {c} {d} {f} → D.≈.trans
            (arr∘trans (fmap F′ f) (DC.lim′ (fobj F′ c)) (DC.lim′ (fobj F′ d)) j)
            (D.∘-resp-l F′fj≈Fjf)
        }
      ; commute = λ {i} {j} f → ≈-intro λ {c} → D.≈.trans
          (DC.lim′ (fobj F′ c) .commute f)
          (D.∘-resp-l F′cf≈Ffc)
      }
    ; isLimit = λ X → record
      { arr = record
        { arr = record
          { component = λ c → !! (DC.lim′ (F′ .fobj c)) (apCone X c)
          ; natural = λ {c} {d} {f} →
            begin
              !! (DC.lim′ (fobj F′ d)) (apCone X d) D.∘ fmap (Apex X) f
            ≈⟨ !!∘ (DC.lim′ (fobj F′ d)) {C = record
                  { Apex = Apex X .fobj c
                  ; arr = λ j → apCone X d .arr j D.∘ Apex X .fmap f
                  ; commute = λ {i} {j} g → D.≈.sym (
                    begin
                      (F .fobj j .fmap C.id D.∘ F .fmap g .component d) D.∘
                        X .arr i .component d D.∘ Apex X .fmap f
                    ≈⟨ D.∘-resp-l
                        (D.≈.trans (D.∘-resp-l (F .fobj j .fmap-id)) D.id-l) ⟩
                      F .fmap g .component d D.∘ X .arr i .component d D.∘
                        Apex X .fmap f
                    ≈⟨ D.unassoc ⟩
                      (F .fmap g .component d D.∘ X .arr i .component d) D.∘
                        Apex X .fmap f
                    ≈⟨ D.∘-resp-l (D.≈.sym (X .commute g .≈-elim)) ⟩
                      X .arr j .component d D.∘ Apex X .fmap f
                    ∎)
                  }} record
                    { commute = λ j → D.≈.refl } ⟩
              !! (DC.lim′ (fobj F′ d)) _
            ≈⟨ !!-unique (DC.lim′ (fobj F′ d)) record
                  { commute = λ j →
                    begin
                      DC.lim′ (fobj F′ d) .arr j D.∘
                      trans (F′ .fmap f) (DC.lim′ (fobj F′ c)) (DC.lim′ (fobj F′ d)) D.∘
                      !! (DC.lim′ (fobj F′ c)) (apCone X c)
                    ≈⟨ D.unassoc ⟩
                      (DC.lim′ (fobj F′ d) .arr j D.∘
                      trans (F′ .fmap f) (DC.lim′ (fobj F′ c)) (DC.lim′ (fobj F′ d))) D.∘
                      !! (DC.lim′ (fobj F′ c)) (apCone X c)
                    ≈⟨ D.∘-resp-l
                          (arr∘trans (F′ .fmap f) (DC.lim′ (fobj F′ c))
                            (DC.lim′ (fobj F′ d)) j) ⟩
                      (F′ .fmap f .component j D.∘ DC.lim′ (fobj F′ c) .arr j) D.∘
                      !! (DC.lim′ (fobj F′ c)) (apCone X c)
                    ≈⟨ D.assoc ⟩
                      F′ .fmap f .component j D.∘
                      DC.lim′ (fobj F′ c) .arr j D.∘
                      !! (DC.lim′ (fobj F′ c)) (apCone X c)
                    ≈⟨ D.∘-resp-r (arr∘!! (DC.lim′ (fobj F′ c)) (apCone X c)) ⟩
                      F′ .fmap f .component j D.∘ X .arr j .component c
                    ≈⟨ D.∘-resp-l F′fj≈Fjf ⟩
                      F .fobj j .fmap f D.∘ X .arr j .component c
                    ≈˘⟨ X .arr j .natural  ⟩
                      X .arr j .component d D.∘ Apex X .fmap f
                    ∎
                  } ⟩
              fmap (DC.limF ∘ F′) f D.∘ !! (DC.lim′ (fobj F′ c)) (apCone X c)
            ∎
          }
        ; commute = λ j → ≈-intro λ {c} → arr∘!! (DC.lim′ (F′ .fobj c)) (apCone X c)
        }
      ; unique = λ {g} _ → ≈-intro λ {c} → !!-unique (DC.lim′ (F′ .fobj c)) record
          { commute = λ j → g .commute j .≈-elim
          }
      }
    }
    where
      module C = Category C
      module D = Category D
      module J = Category J
      open D.≈-Reasoning
      module DC = Complete D-complete

      F′ : Functor C (J ↝ D)
      F′ = Curry (Uncurry F ∘ Swap)

      F′fj≈Fjf : ∀ {c d} {f : c C.⇒ d} {j}
        → F′ .fmap f .component j D.≈ F .fobj j .fmap f
      F′fj≈Fjf = D.≈.trans (D.∘-resp-r (fmap-id F .≈-elim)) D.id-r

      F′cf≈Ffc : ∀ {c i j} {f : i J.⇒ j}
        → F′ .fobj c .fmap f D.≈ F .fmap f .component c
      F′cf≈Ffc = D.≈.trans (D.∘-resp-l (fmap-id (fobj F _))) D.id-l

      apCone : Cone F → ∀ c → Cone (fobj F′ c)
      apCone X c = record
        { Apex = Apex X .fobj c
        ; arr = λ j → X .arr j .component c
        ; commute = λ f → D.≈.trans
            (X .commute f .≈-elim)
            (D.∘-resp-l (D.≈.sym F′cf≈Ffc))
        }

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.SafetyRules.SafetyRules as SafetyRules
import      LibraBFT.Impl.Consensus.TestUtils.MockStorage   as MockStorage
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.Prelude
open import Optics.All

module LibraBFT.Impl.Consensus.MetricsSafetyRules where

performInitialize : SafetyRules → PersistentLivenessStorage → Either ErrLog SafetyRules
performInitialize self obmPersistentLivenessStorage = do
  let consensusState = SafetyRules.consensusState self
      srWaypoint     = consensusState ^∙ csWaypoint
  proofs            <- MockStorage.retrieveEpochChangeProofE
                         (srWaypoint ^∙ wVersion) obmPersistentLivenessStorage
  SafetyRules.initialize self proofs

max_stars_repo_name: oracle/bft-consensus-agda

max_issues_repo_name: oracle/bft-consensus-agda

max_forks_repo_name: oracle/bft-consensus-agda


text:
-- Andreas, 2020-06-21, issue #3734, reported 2019-05-01 by gallais
-- User warnings also on constructors and pattern synonyms.

-- {-# OPTIONS -v scope.warning.usage:50 #-}

data A : Set where
  s : A → A
  a : A

b : A
b = a  -- (usage of a, but no warning yet installed)

{-# WARNING_ON_USAGE a "Used a" #-}

_ : A
_ = a  -- usage of a

_ : A → A
_ = λ where
  a →  -- pattern usage of a
    a  -- usage of a
  x → x

_ : A
_ = s b  -- (usage of a via b, need not show)

pattern c = s a  -- usage of a

{-# WARNING_ON_USAGE c "Used c" #-}

_ : A
_ = c  -- usage of c

_ : A → A
_ = λ where
  c →     -- pattern usage of c
    a     -- usage of a
  x → x

-- Ambiguous constructors

module M where
  data D1 : Set where cons : D1
  {-# WARNING_ON_USAGE cons "Warning on D1.cons (shouldn't show)" #-}

data D2 : Set where cons : D2
{-# WARNING_ON_USAGE cons "Warning on D2.cons (should show)" #-}

open M

d2 : D2
d2 = cons  -- usage of D2.cons

f2 : D2 → Set
f2 cons = A  -- pattern usage of D2.cons

-- Ambiguous attachments of warnings shall apply to all disambiguations.

data Amb1 : Set where amb : Amb1
data Amb2 : Set where amb : Amb2

{-# WARNING_ON_USAGE amb "Ambiguous constructor amb was used" #-}

test1 : Amb1
test1 = amb

test2 : Amb2
test2 = amb

max_forks_repo_name: shlevy/agda


text:
--------------------------------------------------------------------------------
-- This file provides the data structures and functions for the theory of
-- cedille core extended with the constructs for metaprogramming.
--------------------------------------------------------------------------------

{-# OPTIONS --type-in-type #-}

module CoreTheory where

import Agda.Builtin.Nat using (_+_; _-_; _==_)

import Data.Product

open import Class.Map
open import Class.Monad.Except
open import Data.HSTrie
open import Data.Integer using (ℤ; +_; -[1+_])
open import Data.String using (toList; fromList)
open import Data.Word using (Word64; toℕ; fromℕ)
open import Data.Word64.Exts
open import Monads.Except

open import Prelude

open import Theory.PrimMeta public

private
  variable
    A B C : Set
    M : Set → Set

data Sort : Set where
  ⋆ : Sort
  □ : Sort

instance
  Sort-Show : Show Sort
  Sort-Show = record { show = helper }
    where
      helper : Sort → String
      helper ⋆ = "*"
      helper □ = "□"

  Sort-Eq : Eq Sort
  Sort-Eq = record { _≟_ = helper }
    where
      helper : (s s' : Sort) → Dec (s ≡ s')
      helper ⋆ ⋆ = yes refl
      helper ⋆ □ = no λ ()
      helper □ ⋆ = no λ ()
      helper □ □ = yes refl

  Sort-EqB = Eq→EqB {{Sort-Eq}}

GlobalName : Set
GlobalName = String

𝕀 : Set
𝕀 = Word64

instance
  𝕀-Eq : Eq 𝕀
  𝕀-Eq = record { _≟_ = Data.Word._≟_ }

  𝕀-EqB : EqB 𝕀
  𝕀-EqB = record { _≣_ = Agda.Builtin.Nat._==_ on toℕ }

  𝕀-Show : Show 𝕀
  𝕀-Show = record { show = show ∘ toℕ }

_<𝕀_ : 𝕀 → 𝕀 → Bool
x <𝕀 y = toℕ x <ᵇ toℕ y

_+𝕀_ : 𝕀 → 𝕀 → 𝕀
x +𝕀 y = fromℕ $ toℕ x + toℕ y

_-𝕀_ : 𝕀 → 𝕀 → 𝕀
_-𝕀_ = subWord

suc𝕀 : 𝕀 → 𝕀
suc𝕀 = _+𝕀 fromℕ 1

pred𝕀 : 𝕀 → 𝕀
pred𝕀 = _-𝕀 fromℕ 1

data Name : Set where
  Bound : 𝕀 → Name
  Free : GlobalName → Name

instance
  Name-Eq : Eq Name
  Name-Eq = record { _≟_ = helper }
    where
      helper : (n n' : Name) → Dec (n ≡ n')
      helper (Bound x) (Bound x₁) with x ≟ x₁
      ... | yes p rewrite p = yes refl
      ... | no ¬p = no λ { refl → ¬p refl }
      helper (Bound x) (Free x₁) = no λ ()
      helper (Free x) (Bound x₁) = no λ ()
      helper (Free x) (Free x₁) with x ≟ x₁
      ... | yes p rewrite p = yes refl
      ... | no ¬p = no λ { refl → ¬p refl }

  Name-EqB : EqB Name
  Name-EqB = Eq→EqB

  Name-Show : Show Name
  Name-Show = record { show = helper }
    where
      helper : Name → String
      helper (Bound x) = show x
      helper (Free x) = x

record TermLike (T : Set) : Set where
  infixl -1 _⟪$⟫_ -- same as $ but on the left
  field
    Var : Name → T
    _⟪$⟫_ : T → T → T

  BoundVar : 𝕀 → T
  BoundVar = Var ∘ Bound

  FreeVar : GlobalName → T
  FreeVar = Var ∘ Free

open TermLike {{...}} public

showVar : List String → Name → String
showVar l (Bound x) with lookupMaybe (toℕ x) l
... | nothing = show x
... | just x₁ = if x₁ ≣ "_" then show x else x₁
showVar l (Free x) = x

data Const : Set where
  CharT : Const

instance
  Const-Eq : Eq Const
  Const-Eq = record { _≟_ = helper }
    where
      helper : (c c' : Const) → Dec (c ≡ c')
      helper CharT CharT = yes refl

  Const-EqB : EqB Const
  Const-EqB = Eq→EqB

  Const-Show : Show Const
  Const-Show = record { show = helper }
    where
      helper : Const → String
      helper CharT = "CharT"

data PureTerm : Set where
  Var-P : Name → PureTerm
  Sort-P : Sort → PureTerm
  Const-P : Const → PureTerm
  App-P : PureTerm → PureTerm → PureTerm
  Lam-P : String → PureTerm → PureTerm
  Pi-P : String → PureTerm → PureTerm → PureTerm
  All-P : String → PureTerm → PureTerm → PureTerm
  Iota-P : String → PureTerm → PureTerm → PureTerm
  Eq-P : PureTerm → PureTerm → PureTerm
  M-P : PureTerm → PureTerm
  Mu-P : PureTerm → PureTerm → PureTerm
  Epsilon-P : PureTerm → PureTerm
  Gamma-P : PureTerm → PureTerm → PureTerm
  Ev-P : (m : PrimMeta) → primMetaArgs PureTerm m → PureTerm
  Char-P : Char → PureTerm
  CharEq-P : PureTerm → PureTerm → PureTerm

instance
  PureTerm-TermLike : TermLike PureTerm
  PureTerm-TermLike = record { Var = Var-P ; _⟪$⟫_ = App-P }

  {-# TERMINATING #-}
  PureTerm-Show : Show PureTerm
  PureTerm-Show = record { show = helper [] }
    where
      helper : List String → PureTerm → String
      helper l (Var-P x) = showVar l x
      helper l (Sort-P x) = show x
      helper l (Const-P x) = show x
      helper l (App-P t t₁) = "[" + helper l t <+> helper l t₁ + "]"
      helper l (Lam-P n t) = "λ" <+> n <+> helper (n ∷ l) t
      helper l (Pi-P n t t₁) = "Π" <+> n <+> helper (n ∷ l) t <+> helper l t₁
      helper l (All-P n t t₁) = "∀" <+> n <+> helper (n ∷ l) t <+> helper l t₁
      helper l (Iota-P n t t₁) = "ι" <+> n <+> helper (n ∷ l) t <+> helper l t₁
      helper l (Eq-P t t₁) = "=" <+> helper l t <+> helper l t₁
      helper l (M-P t) = "M" <+> helper l t
      helper l (Mu-P t t₁) = "μ" <+> helper l t <+> helper l t₁
      helper l (Epsilon-P t) = "ε" <+> helper l t
      helper l (Gamma-P t t₁) = "Γ" <+> helper l t <+> helper l t₁
      helper l (Ev-P m args) = "ζ" <+> show m <+> primMetaArgs-Show (helper l) args
      helper l (Char-P c) = "Char" <+> show c
      helper l (CharEq-P t t') = "CharEq" <+> show t <+> show t'

private
  beqMonadHelper : {{_ : EqB A}} {{_ : Show A}} {{_ : Monad M}} {{_ : MonadExcept M String}}
                → A → A → String → M ⊤
  beqMonadHelper a a' s =
    if a ≣ a'
      then return tt
      else throwError (s <+> show a <+> "isn't equal to name" <+> show a')

{-# TERMINATING #-}
pureTermBeq : {{_ : Monad M}} {{_ : MonadExcept M String}}
  → PureTerm → PureTerm → M ⊤
pureTermBeq (Var-P x) (Var-P x₁) = beqMonadHelper x x₁ "Name"
pureTermBeq (Sort-P x) (Sort-P x₁) = beqMonadHelper x x₁ "Sort"
pureTermBeq (Const-P x) (Const-P x₁) = beqMonadHelper x x₁ "Const"
pureTermBeq (App-P t t₁) (App-P x x₁) = pureTermBeq t x >> pureTermBeq t₁ x₁
pureTermBeq (Lam-P _ t) (Lam-P _ t₁) = pureTermBeq t t₁
pureTermBeq (Pi-P _ t t₁) (Pi-P _ x x₁) = pureTermBeq t x >> pureTermBeq t₁ x₁
pureTermBeq (All-P _ t t₁) (All-P _ x x₁) = pureTermBeq t x >> pureTermBeq t₁ x₁
pureTermBeq (Iota-P _ t t₁) (Iota-P _ x x₁) = pureTermBeq t x >> pureTermBeq t₁ x₁
pureTermBeq (Eq-P t t₁) (Eq-P x x₁) = pureTermBeq t x >> pureTermBeq t₁ x₁
pureTermBeq (M-P t) (M-P x) = pureTermBeq x t
pureTermBeq (Mu-P t t₁) (Mu-P x x₁) = pureTermBeq t x >> pureTermBeq t₁ x₁
pureTermBeq (Epsilon-P t) (Epsilon-P x) = pureTermBeq t x
pureTermBeq (Gamma-P t t₁) (Gamma-P x x₁) = pureTermBeq t x >> pureTermBeq t₁ x₁
pureTermBeq (Ev-P m t) (Ev-P m' x) with m ≟ m'
... | yes refl = void $ primMetaArgsSequence $ primMetaArgsZipWith pureTermBeq t x
... | no  _    = throwError $ show m <+> "and" <+> show m' <+> "aren't equal!"
pureTermBeq (Char-P c) (Char-P c') = beqMonadHelper c c' "Char"
pureTermBeq (CharEq-P t t₁) (CharEq-P x x₁) = pureTermBeq t x >> pureTermBeq t₁ x₁
{-# CATCHALL #-}
pureTermBeq t t' =
  throwError $ "The terms" <+> show t <+> "and" <+> show t' <+> "aren't equal!"

data AnnTerm : Set where
  Var-A : Name → AnnTerm
  Sort-A : Sort → AnnTerm
  Const-A : Const → AnnTerm
  Pr1-A : AnnTerm → AnnTerm
  Pr2-A : AnnTerm → AnnTerm
  Beta-A : AnnTerm → AnnTerm → AnnTerm -- proves first arg eq, erase to second arg
  Delta-A : AnnTerm → AnnTerm → AnnTerm -- inhabits first arg if snd arg proves false
  Sigma-A : AnnTerm → AnnTerm
  App-A : AnnTerm → AnnTerm → AnnTerm
  AppE-A : AnnTerm → AnnTerm → AnnTerm
  Rho-A : AnnTerm → AnnTerm → AnnTerm → AnnTerm -- first arg is eq, rewrite the name in the third arg and inhabit with fourth arg
  All-A : String → AnnTerm → AnnTerm → AnnTerm
  Pi-A : String → AnnTerm → AnnTerm → AnnTerm
  Iota-A : String → AnnTerm → AnnTerm → AnnTerm
  Lam-A : String → AnnTerm → AnnTerm → AnnTerm
  LamE-A : String → AnnTerm → AnnTerm → AnnTerm
  Pair-A : AnnTerm → AnnTerm → AnnTerm → AnnTerm
  Phi-A : AnnTerm → AnnTerm → AnnTerm → AnnTerm
  -- there is a let binding here, which is probably unnecessary
  Eq-A : AnnTerm → AnnTerm → AnnTerm
  M-A : AnnTerm → AnnTerm
  Mu-A : AnnTerm → AnnTerm → AnnTerm
  Epsilon-A : AnnTerm → AnnTerm
  Gamma-A : AnnTerm → AnnTerm → AnnTerm
  Ev-A : (x : PrimMeta) → primMetaArgs AnnTerm x → AnnTerm
  Char-A : Char → AnnTerm
  CharEq-A : AnnTerm → AnnTerm → AnnTerm

instance
  AnnTerm-TermLike : TermLike AnnTerm
  AnnTerm-TermLike = record { Var = Var-A ; _⟪$⟫_ = App-A }

  {-# TERMINATING #-}
  AnnTerm-Show : Show AnnTerm
  AnnTerm-Show = record { show = helper [] }
    where
      helper : List String → AnnTerm → String
      helper l (Var-A x)        = showVar l x
      helper l (Sort-A x)       = show x
      helper l (Const-A x)      = show x
      helper l (Pr1-A t)        = "π1" <+> helper l t
      helper l (Pr2-A t)        = "π2" <+> helper l t
      helper l (Beta-A t t₁)    = "β" <+> helper l t <+> helper l t₁
      helper l (Delta-A t t₁)   = "Delta-A" + helper l t <+> helper l t₁
      helper l (Sigma-A t)      = "ς" + helper l t
      helper l (App-A t t₁)     = "[" + helper l t <+> helper l t₁ + "]"
      helper l (AppE-A t t₁)    = "<" + helper l t <+> helper l t₁ + ">"
      helper l (Rho-A t t₁ t₂)  = "ρ" <+> helper l t <+> ":" <+> helper l t₁ <+> helper l t₂
      helper l (All-A n t t₁)   = "∀" <+> n <+> ":" <+> helper l t + "." <+> helper (n ∷ l) t₁
      helper l (Pi-A n t t₁)    = "Π" <+> n <+> ":" <+> helper l t + "." <+> helper (n ∷ l) t₁
      helper l (Iota-A n t t₁)  = "ι" <+> n <+> ":" <+> helper l t + "." <+> helper (n ∷ l) t₁
      helper l (Lam-A n t t₁)   = "λ" <+> n <+> ":" <+> helper l t + "." <+> helper (n ∷ l) t₁
      helper l (LamE-A n t t₁)  = "Λ" <+> n <+> ":" <+> helper l t + "." <+> helper (n ∷ l) t₁
      helper l (Pair-A t t₁ t₂) = "{" + helper l t + "," + helper l t₁ <+> "." <+> helper l t₂ + "}"
      helper l (Phi-A t t₁ t₂)  = "φ" <+> helper l t <+> helper l t₁ <+> helper l t₂
      helper l (Eq-A t t₁)      = "(=" <+> helper l t <+> helper l t₁ + ")"
      helper l (M-A t)          = "M" <+> helper l t
      helper l (Mu-A t t₁)      = "μ" <+> helper l t <+> helper l t₁
      helper l (Epsilon-A t)    = "ε" <+> helper l t
      helper l (Gamma-A t t₁)   = "Γ" <+> helper l t <+> helper l t₁
      helper l (Ev-A m args)    = "Ev" <+> show m <+> primMetaArgs-Show (helper l) args
      helper l (Char-A c)       = "Char" <+> show c
      helper l (CharEq-A t t')  = "CharEq" <+> show t <+> show t'

primMetaS : (m : PrimMeta) → primMetaArgs AnnTerm m
primMetaS EvalStmt      = FreeVar "init$stmt"
primMetaS ShellCmd      = (FreeVar "init$string" , FreeVar "init$stringList")
primMetaS CheckTerm     = (Sort-A ⋆ , FreeVar "init$term")
primMetaS Parse         = (FreeVar "init$string" , Sort-A ⋆ , FreeVar "init$string")
primMetaS Normalize     = FreeVar "init$term"
primMetaS HeadNormalize = FreeVar "init$term"
primMetaS InferType     = FreeVar "init$term"

primMetaT : ∀ {T} {{_ : TermLike T}} (m : PrimMeta) → primMetaArgs T m → T
primMetaT EvalStmt _        = FreeVar "init$metaResult"
primMetaT ShellCmd _        = FreeVar "init$string"
primMetaT CheckTerm (t , _) = t
primMetaT Parse (_ , t , _) = FreeVar "init$product" ⟪$⟫ t ⟪$⟫ FreeVar "init$string"
primMetaT Normalize _       = FreeVar "init$term"
primMetaT HeadNormalize _   = FreeVar "init$term"
primMetaT InferType     _   = FreeVar "init$term"

data Def : Set where
  Let : AnnTerm → AnnTerm → Def
  Axiom : AnnTerm → Def

data EfficientDef : Set where
  EfficientLet : AnnTerm → PureTerm → AnnTerm → EfficientDef
  EfficientAxiom : AnnTerm → EfficientDef

toDef : EfficientDef → Def
toDef (EfficientLet x x₁ x₂)   = Let x x₂
toDef (EfficientAxiom x)       = Axiom x

getNorm : EfficientDef → Maybe PureTerm
getNorm (EfficientLet x x₁ x₂) = return x₁
getNorm (EfficientAxiom x)     = nothing

instance
  Def-Show : Show Def
  Def-Show = record { show = helper }
    where
      helper : Def → String
      helper (Let x x₁) = " :=" <+> show x <+> ":" <+> show x₁
      helper (Axiom x) = " :" <+> show x

typeOfDef : Def → AnnTerm
typeOfDef (Let _ x) = x
typeOfDef (Axiom x) = x

{-# TERMINATING #-}
modifyIndicesPure : 𝕀 → PureTerm → PureTerm
modifyIndicesPure = helper $ fromℕ 0
  where
    helper : 𝕀 → 𝕀 → PureTerm → PureTerm
    helper k n v@(Var-P (Bound x)) = if x <𝕀 k then v else BoundVar (pred𝕀 (x +𝕀 n))
    helper k n v@(Var-P (Free x))  = v
    helper k n v@(Sort-P x)        = v
    helper k n v@(Const-P x)       = v
    helper k n (App-P t t₁)        = App-P (helper k n t) (helper k n t₁)
    helper k n (Lam-P x t)         = Lam-P x (helper (suc𝕀 k) n t)
    helper k n (Pi-P x t t₁)       = Pi-P x (helper k n t) (helper (suc𝕀 k) n t₁)
    helper k n (All-P x t t₁)      = All-P x (helper k n t) (helper (suc𝕀 k) n t₁)
    helper k n (Iota-P x t t₁)     = Iota-P x (helper k n t) (helper (suc𝕀 k) n t₁)
    helper k n (Eq-P t t₁)         = Eq-P (helper k n t) (helper k n t₁)
    helper k n (M-P t)             = M-P (helper k n t)
    helper k n (Mu-P t t₁)         = Mu-P (helper k n t) (helper k n t₁)
    helper k n (Epsilon-P t)       = Epsilon-P (helper k n t)
    helper k n (Gamma-P t t₁)      = Gamma-P (helper k n t) (helper k n t₁)
    helper k n (Ev-P m args)       = Ev-P m (mapPrimMetaArgs (helper k n) args)
    helper k n (Char-P c)          = Char-P c
    helper k n (CharEq-P t t')     = CharEq-P (helper k n t) (helper k n t')

incrementIndicesPureBy : 𝕀 → PureTerm → PureTerm
incrementIndicesPureBy i = modifyIndicesPure (suc𝕀 i)

decrementIndicesPure : PureTerm → PureTerm
decrementIndicesPure = modifyIndicesPure (fromℕ 0)

{-# TERMINATING #-}
modifyIndices : 𝕀 → AnnTerm → AnnTerm
modifyIndices = helper (fromℕ 0)
  where
    helper : 𝕀 → 𝕀 → AnnTerm → AnnTerm
    helper k n v@(Var-A (Bound x)) = if x <𝕀 k then v else BoundVar (pred𝕀 (x +𝕀 n))
    helper k n v@(Var-A (Free x)) = v
    helper k n (Sort-A x) = Sort-A x
    helper k n (Const-A x) = Const-A x
    helper k n (Pr1-A t) = Pr1-A $ helper k n t
    helper k n (Pr2-A t) = Pr2-A $ helper k n t
    helper k n (Beta-A t t₁) = Beta-A (helper k n t) (helper k n t₁)
    helper k n (Delta-A t t₁) = Delta-A (helper k n t) (helper k n t₁)
    helper k n (Sigma-A t) = Sigma-A (helper k n t)
    helper k n (App-A t t₁) = App-A (helper k n t) (helper k n t₁)
    helper k n (AppE-A t t₁) = AppE-A (helper k n t) (helper k n t₁)
    helper k n (Rho-A t t₁ t₂) = Rho-A (helper k n t) (helper (suc𝕀 k) n t₁) (helper k n t₂)
    helper k n (All-A x t t₁) = All-A x (helper k n t) (helper (suc𝕀 k) n t₁)
    helper k n (Pi-A x t t₁) = Pi-A x (helper k n t) (helper (suc𝕀 k) n t₁)
    helper k n (Iota-A x t t₁) = Iota-A x (helper k n t) (helper (suc𝕀 k) n t₁)
    helper k n (Lam-A x t t₁) = Lam-A x (helper k n t) (helper (suc𝕀 k) n t₁)
    helper k n (LamE-A x t t₁) = LamE-A x (helper k n t) (helper (suc𝕀 k) n t₁)
    helper k n (Pair-A t t₁ t₂) = Pair-A (helper k n t) (helper k n t₁) (helper (suc𝕀 k) n t₂)
    helper k n (Phi-A t t₁ t₂) = Phi-A (helper k n t) (helper k n t₁) (helper k n t₂)
    helper k n (Eq-A t t₁) = Eq-A (helper k n t) (helper k n t₁)
    helper k n (M-A t) = M-A (helper k n t)
    helper k n (Mu-A t t₁) = Mu-A (helper k n t) (helper k n t₁)
    helper k n (Epsilon-A t) = Epsilon-A (helper k n t)
    helper k n (Gamma-A t t₁) = Gamma-A (helper k n t) (helper k n t₁)
    helper k n (Ev-A m args) = Ev-A m (mapPrimMetaArgs (helper k n) args)
    helper k n (Char-A c) = Char-A c
    helper k n (CharEq-A t t₁) = CharEq-A (helper k n t) (helper k n t₁)

incrementIndicesBy : 𝕀 → AnnTerm → AnnTerm
incrementIndicesBy i = modifyIndices (suc𝕀 i)

decrementIndices : AnnTerm → AnnTerm
decrementIndices = modifyIndices (fromℕ 0)

{-# TERMINATING #-}
checkFree : Name → PureTerm → Bool
checkFree = helper 0
  where
    helper : ℕ → Name → PureTerm → Bool
    helper k n (Var-P (Bound x)) = case n of λ where
      (Bound x₁) → x ≣ (fromℕ k +𝕀 x₁)
      (Free x₁) → false
    helper k n (Var-P (Free x)) = case n of λ where
      (Bound x₁) → false
      (Free x₁) → x ≣ x₁
    helper k n (Sort-P x) = false
    helper k n (Const-P x) = false
    helper k n (App-P t t₁) = helper k n t ∧ helper k n t₁
    helper k n (Lam-P _ t) = helper (suc k) n t
    helper k n (Pi-P _ t t₁) = helper k n t ∧ helper (suc k) n t₁
    helper k n (All-P _ t t₁) = helper k n t ∧ helper (suc k) n t₁
    helper k n (Iota-P _ t t₁) = helper k n t ∧ helper (suc k) n t₁
    helper k n (Eq-P t t₁) = helper k n t ∧ helper k n t₁
    helper k n (M-P t) = helper k n t
    helper k n (Mu-P t t₁) = helper k n t ∧ helper k n t₁
    helper k n (Epsilon-P t) = helper k n t
    helper k n (Gamma-P t t₁) = helper k n t ∧ helper k n t₁
    helper k n (Ev-P m t) = primMetaArgsAnd $ mapPrimMetaArgs (helper k n) t
    helper k n (Char-P c) = false
    helper k n (CharEq-P t t₁) = helper k n t ∧ helper k n t₁

GlobalContext : Set
GlobalContext = HSTrie EfficientDef

emptyGlobalContext : GlobalContext
emptyGlobalContext = emptyMap

Context : Set
Context = GlobalContext × List AnnTerm

instance
  Context-Show : Show Context
  Context-Show = record { show = helper }
    where
      helper : Context → String
      helper (fst , snd) =
        (show $ length snd) <+> "local variables:" + show snd

globalToContext : GlobalContext → Context
globalToContext Γ = Γ , []

contextToGlobal : Context → GlobalContext
contextToGlobal (fst , snd) = fst

-- add variable to context, so that index 0 points to that variable
pushVar : AnnTerm → Context → Context
pushVar v (fst , snd) = fst , v ∷ snd

localContextLength : Context → ℕ
localContextLength (fst , snd) = length snd

efficientLookupInContext : Name → Context → Maybe EfficientDef
efficientLookupInContext (Bound x) (fst , snd) =
  EfficientAxiom ∘ incrementIndicesBy (suc𝕀 x) <$> lookupMaybe (toℕ x) snd
efficientLookupInContext (Free x) (fst , snd) = lookup x fst

lookupInContext : Name → Context → Maybe Def
lookupInContext n Γ = toDef <$> efficientLookupInContext n Γ

{-# TERMINATING #-}
validInContext : PureTerm → Context → Bool
validInContext = helper 0
  where
    -- instead of modifying the context here, we just count how many variables we would have added if we did
    helper : ℕ → PureTerm → Context → Bool
    helper k (Var-P (Bound x)) Γ = x <𝕀 fromℕ (localContextLength Γ + k)
    helper k (Var-P n@(Free x)) Γ = maybe (λ _ → true) false $ lookupInContext n Γ
    helper k (Sort-P x) Γ = true
    helper k (Const-P x) Γ = true
    helper k (App-P t t₁) Γ = helper k t Γ ∧ helper k t₁ Γ
    helper k (Lam-P _ t) Γ = helper (suc k) t Γ
    helper k (Pi-P _ t t₁) Γ = helper k t Γ ∧ helper (suc k) t₁ Γ
    helper k (All-P _ t t₁) Γ = helper k t Γ ∧ helper (suc k) t₁ Γ
    helper k (Iota-P _ t t₁) Γ = helper k t Γ ∧ helper (suc k) t₁ Γ
    helper k (Eq-P t t₁) Γ = helper k t Γ ∧ helper k t₁ Γ
    helper k (M-P t) Γ = helper k t Γ
    helper k (Mu-P t t₁) Γ = helper k t Γ ∧ helper k t₁ Γ
    helper k (Epsilon-P t) Γ = helper k t Γ
    helper k (Gamma-P t t₁) Γ = helper k t Γ ∧ helper k t₁ Γ
    helper k (Ev-P m t) Γ = primMetaArgsAnd $ mapPrimMetaArgs (λ x → helper k x Γ) t
    helper k (Char-P c) Γ = true
    helper k (CharEq-P t t₁) Γ = helper k t Γ ∧ helper k t₁ Γ

{-# TERMINATING #-}
Erase : AnnTerm → PureTerm
Erase (Var-A x)        = Var-P x
Erase (Sort-A x)       = Sort-P x
Erase (Const-A x)      = Const-P x
Erase (Pr1-A t)        = Erase t
Erase (Pr2-A t)        = Erase t
Erase (Beta-A t t₁)    = Erase t₁
Erase (Delta-A t t₁)   = Erase t₁
Erase (Sigma-A t)      = Erase t
Erase (App-A t t₁)     = App-P (Erase t) (Erase t₁)
Erase (AppE-A t t₁)    = Erase t
Erase (Rho-A t t₁ t₂)  = Erase t₂
Erase (All-A n t t₁)   = All-P n (Erase t) (Erase t₁)
Erase (Pi-A n t t₁)    = Pi-P n (Erase t) (Erase t₁)
Erase (Iota-A n t t₁)  = Iota-P n (Erase t) (Erase t₁)
Erase (Lam-A n t t₁)   = Lam-P n (Erase t₁)
Erase (LamE-A _ t t₁)  = decrementIndicesPure (Erase t₁)
Erase (Pair-A t t₁ t₂) = Erase t
Erase (Phi-A t t₁ t₂)  = Erase t₂
Erase (Eq-A x x₁)      = Eq-P (Erase x) (Erase x₁)
Erase (M-A t)          = M-P (Erase t)
Erase (Mu-A t t₁)      = Mu-P (Erase t) (Erase t₁)
Erase (Epsilon-A t)    = Epsilon-P (Erase t)
Erase (Gamma-A t t₁)   = Gamma-P (Erase t) (Erase t₁)
Erase (Ev-A m args)    = Ev-P m (mapPrimMetaArgs Erase args)
Erase (Char-A c)       = Char-P c
Erase (CharEq-A x x₁)  = CharEq-P (Erase x) (Erase x₁)

-- substitute the first unbound variable in t with t'
{-# TERMINATING #-}
subst : AnnTerm → AnnTerm → AnnTerm
subst t t' = decrementIndices $ substIndex t (fromℕ 0) t'
  where
    -- substitute the k-th unbound variable in t with t'
    substIndex : AnnTerm → 𝕀 → AnnTerm → AnnTerm
    substIndex v@(Var-A (Bound x)) k t' = if k ≣ x then incrementIndicesBy (suc𝕀 k) t' else v
    substIndex v@(Var-A (Free x)) k t' = v
    substIndex v@(Sort-A x) k t' = v
    substIndex v@(Const-A x) k t' = v
    substIndex (Pr1-A t) k t' = Pr1-A (substIndex t k t')
    substIndex (Pr2-A t) k t' = Pr2-A (substIndex t k t')
    substIndex (Beta-A t t₁) k t' = Beta-A (substIndex t k t') (substIndex t₁ k t')
    substIndex (Delta-A t t₁) k t' = Delta-A (substIndex t k t') (substIndex t₁ k t')
    substIndex (Sigma-A t) k t' = Sigma-A (substIndex t k t')
    substIndex (App-A t t₁) k t' = App-A (substIndex t k t') (substIndex t₁ k t')
    substIndex (AppE-A t t₁) k t' = AppE-A (substIndex t k t') (substIndex t₁ k t')
    substIndex (Rho-A t t₁ t₂) k t' = Rho-A (substIndex t k t') (substIndex t₁ k t') (substIndex t₂ k t')
    substIndex (All-A n t t₁) k t' = All-A n (substIndex t k t') (substIndex t₁ (suc𝕀 k) t')
    substIndex (Pi-A n t t₁) k t' = Pi-A n (substIndex t k t') (substIndex t₁ (suc𝕀 k) t')
    substIndex (Iota-A n t t₁) k t' = Iota-A n (substIndex t k t') (substIndex t₁ (suc𝕀 k) t')
    substIndex (Lam-A n t t₁) k t' = Lam-A n (substIndex t k t') (substIndex t₁ (suc𝕀 k) t')
    substIndex (LamE-A n t t₁) k t' = LamE-A n (substIndex t k t') (substIndex t₁ (suc𝕀 k) t')
    substIndex (Pair-A t t₁ t₂) k t' = Pair-A (substIndex t k t') (substIndex t₁ k t') (substIndex t₂ (suc𝕀 k) t')
    substIndex (Phi-A t t₁ t₂) k t' = Phi-A (substIndex t k t') (substIndex t₁ k t') (substIndex t₂ k t')
    substIndex (Eq-A t t₁) k t' = Eq-A (substIndex t k t') (substIndex t₁ k t')
    substIndex (M-A t) k t' = M-A (substIndex t k t')
    substIndex (Mu-A t t₁) k t' = Mu-A (substIndex t k t') (substIndex t₁ k t')
    substIndex (Epsilon-A t) k t' = Epsilon-A (substIndex t k t')
    substIndex (Gamma-A t t₁) k t' = Gamma-A (substIndex t k t') (substIndex t₁ k t')
    substIndex (Ev-A m t) k t' = Ev-A m $ mapPrimMetaArgs (λ x → substIndex x k t') t
    substIndex (Char-A c) k t' = Char-A c
    substIndex (CharEq-A t t₁) k t' = CharEq-A (substIndex t k t') (substIndex t₁ k t')

-- substitute the first unbound variable in t with t'
{-# TERMINATING #-}
substPure : PureTerm → PureTerm → PureTerm
substPure t t' = decrementIndicesPure $ substIndexPure t (fromℕ 0) t'
  where
    -- substitute the k-th unbound variable in t with t'
    substIndexPure : PureTerm → 𝕀 → PureTerm → PureTerm
    substIndexPure v@(Var-P (Bound x)) k t' = if k ≣ x then incrementIndicesPureBy (suc𝕀 k) t' else v
    substIndexPure v@(Var-P (Free x)) k t' = v
    substIndexPure v@(Sort-P x) k t' = v
    substIndexPure v@(Const-P x) k t' = v
    substIndexPure (App-P t t₁) k t' = App-P (substIndexPure t k t') (substIndexPure t₁ k t')
    substIndexPure (Lam-P n t) k t' = Lam-P n (substIndexPure t (suc𝕀 k) t')
    substIndexPure (Pi-P n t t₁) k t' = Pi-P n (substIndexPure t k t') (substIndexPure t₁ (suc𝕀 k) t')
    substIndexPure (All-P n t t₁) k t' = All-P n (substIndexPure t k t') (substIndexPure t₁ (suc𝕀 k) t')
    substIndexPure (Iota-P n t t₁) k t' = Iota-P n (substIndexPure t k t') (substIndexPure t₁ (suc𝕀 k) t')
    substIndexPure (Eq-P t t₁) k t' = Eq-P (substIndexPure t k t') (substIndexPure t₁ k t')
    substIndexPure (M-P t) k t' = M-P (substIndexPure t k t')
    substIndexPure (Mu-P t t₁) k t' = Mu-P (substIndexPure t k t') (substIndexPure t₁ k t')
    substIndexPure (Epsilon-P t) k t' = Epsilon-P (substIndexPure t k t')
    substIndexPure (Gamma-P t t₁) k t' = Gamma-P (substIndexPure t k t') (substIndexPure t₁ k t')
    substIndexPure (Ev-P m t) k t' = Ev-P m $ mapPrimMetaArgs (λ x → substIndexPure x k t') t
    substIndexPure (Char-P c) k t' = Char-P c
    substIndexPure (CharEq-P t t₁) k t' = CharEq-P (substIndexPure t k t') (substIndexPure t₁ k t')

stripBinder : AnnTerm → Maybe AnnTerm
stripBinder (All-A  _ t' t'') = just t''
stripBinder (Pi-A   _ t' t'') = just t''
stripBinder (Iota-A _ t' t'') = just t''
stripBinder (Lam-A  _ t' t'') = just t''
stripBinder (LamE-A _ t' t'') = just t''
{-# CATCHALL #-}
stripBinder t                 = nothing

-- something in is head normal form, if its outermost constructor is not one of the following: Var-A (if the lookup fails), App-A, AppE-A
{-# TERMINATING #-}
hnfNorm : Context → AnnTerm → AnnTerm
hnfNorm Γ v@(Var-A x) with lookupInContext x Γ
... | just (Let x₁ x₂)  = hnfNorm Γ x₁
... | just (Axiom x₁)   = v -- we cannot reduce axioms
... | nothing           = v -- in case the lookup fails, we cannot reduce
hnfNorm Γ (App-A t t₁)  = maybe (λ t' → hnfNorm Γ $ subst t' t₁) (t ⟪$⟫ t₁) $ stripBinder (hnfNorm Γ t)
hnfNorm Γ (AppE-A t t₁) = maybe (λ t' → hnfNorm Γ $ subst t' t₁) (t ⟪$⟫ t₁) $ stripBinder (hnfNorm Γ t)
{-# CATCHALL #-}
hnfNorm Γ v             = v

stripBinderPure : PureTerm → Maybe PureTerm
stripBinderPure (Lam-P  _ t')     = just t'
stripBinderPure (Pi-P   _ t' t'') = just t''
stripBinderPure (All-P  _ t' t'') = just t''
stripBinderPure (Iota-P _ t' t'') = just t''
{-# CATCHALL #-}
stripBinderPure _                 = nothing

hnfNormPure normalizePure : Context → PureTerm → PureTerm

{-# NON_TERMINATING #-}
hnfNormPure Γ v@(Var-P x) with lookupInContext x Γ
... | just (Let x₁ x₂)         = hnfNormPure Γ $ Erase x₁
... | just (Axiom x₁)          = v -- we cannot reduce axioms
... | nothing                  = v -- in case the lookup fails, we cannot reduce
hnfNormPure Γ v@(App-P t t₁) with stripBinderPure (hnfNormPure Γ t)
... | (just t')                = hnfNormPure Γ $ substPure t' t₁
... | nothing                  = v
hnfNormPure Γ v@(CharEq-P _ _) = normalizePure Γ v -- reduce to a bool, if possible
{-# CATCHALL #-}
hnfNormPure Γ v                = v

{-# NON_TERMINATING #-}
normalizePure Γ v@(Var-P x) with efficientLookupInContext x Γ
... | just (EfficientLet x₁ x₂ x₃) = x₂
... | just (EfficientAxiom x₁)     = v -- we cannot reduce axioms
... | nothing                      = v -- in case the lookup fails, we cannot reduce
normalizePure Γ v@(Sort-P x)       = v
normalizePure Γ v@(Const-P x)      = v
normalizePure Γ (App-P t t₁) with hnfNormPure Γ t
...| t' = case stripBinderPure t' of λ where
    (just t'') → normalizePure Γ (substPure t'' t₁)
    nothing    → normalizePure Γ t' ⟪$⟫ normalizePure Γ t₁
normalizePure Γ (Lam-P n t) with normalizePure Γ t
... | t''@(App-P t' (Var-P (Bound i))) = if i ≣ (fromℕ 0) ∧ validInContext t' Γ
  then normalizePure Γ (decrementIndicesPure t') else Lam-P n t'' -- eta reduce here
... | t'' = Lam-P n t''
normalizePure Γ (Pi-P n t t₁)      = Pi-P n (normalizePure Γ t) (normalizePure Γ t₁)
normalizePure Γ (All-P n t t₁)     = All-P n (normalizePure Γ t) (normalizePure Γ t₁)
normalizePure Γ (Iota-P n t t₁)    = Iota-P n (normalizePure Γ t) (normalizePure Γ t₁)
normalizePure Γ (Eq-P t t₁)        = Eq-P (normalizePure Γ t) (normalizePure Γ t₁)
normalizePure Γ (M-P t)            = M-P (normalizePure Γ t)
normalizePure Γ (Mu-P t t₁)        = Mu-P (normalizePure Γ t) (normalizePure Γ t₁)
normalizePure Γ (Epsilon-P t)      = Epsilon-P (normalizePure Γ t)
normalizePure Γ (Gamma-P t t₁)     = Gamma-P (normalizePure Γ t) (normalizePure Γ t₁)
normalizePure Γ (Ev-P m args)      = Ev-P m (mapPrimMetaArgs (normalizePure Γ) args)
normalizePure Γ (Char-P c)         = (Char-P c)
normalizePure Γ (CharEq-P t t₁) with normalizePure Γ t | normalizePure Γ t₁
... | (Char-P c) | (Char-P c')     = normalizePure Γ $ FreeVar $ show (c ≣ c')
{-# CATCHALL #-}
... | x | x₁                       = CharEq-P x x₁

{-# TERMINATING #-}
findOutermostConstructor : PureTerm → PureTerm × List PureTerm
findOutermostConstructor t = outermostApp $ stripBinders t
  where
    stripBinders : PureTerm → PureTerm
    stripBinders t with stripBinderPure t
    stripBinders t | just x = stripBinders x
    stripBinders t | nothing = t

    outermostApp : PureTerm → PureTerm × List PureTerm
    outermostApp (App-P t t₁) = Data.Product.map id (t₁ ∷_) $ outermostApp t
    {-# CATCHALL #-}
    outermostApp t = t , []

insertInGlobalContext : GlobalName → Def → GlobalContext → String ⊎ GlobalContext
insertInGlobalContext n d Γ =
  if is-just $ lookup n Γ
    then inj₁ ("The name" <+> n <+> "is already defined!")
    else (inj₂ $ insert n (toEfficientDef d Γ) Γ)
  where
    toEfficientDef : Def → GlobalContext → EfficientDef
    toEfficientDef (Let x x₁) Γ = EfficientLet x (normalizePure (globalToContext Γ) $ Erase x) x₁
    toEfficientDef (Axiom x) Γ = EfficientAxiom x

module CheckEquality {{_ : Monad M}} {{_ : MonadExcept M String}} (Γ : Context) where

  compareNames : PureTerm → PureTerm → M ⊤
  compareNames (Var-P x) (Var-P x₁) =
    if x ≣ x₁
      then return tt
      else throwError "Names not equal! If you see this message, this is a bug!"
  {-# CATCHALL #-}
  compareNames _ _ = throwError "Terms are not names! If you see this message, this is a bug!"

  {-# NON_TERMINATING #-}
  checkβηPure : PureTerm → PureTerm → M ⊤
  checkβηPure t t' =
    tryElse (compareNames t t') $
    compareHnfs (hnfNormPure Γ t) (hnfNormPure Γ t')
    -- tryElse (compareHnfs (hnfNormPure Γ t) (hnfNormPure Γ t')) $
    -- pureTermBeq t t'
    where
      hnfError : PureTerm → PureTerm → M ⊤
      hnfError t t' =
        throwError $ "The terms" <+> show t <+> "and" <+> show t' <+> "aren't equal!"

      compareHnfs : PureTerm → PureTerm → M ⊤
      compareHnfs (Var-P x) (Var-P x₁) = beqMonadHelper x x₁ "Name"
      compareHnfs (Sort-P x) (Sort-P x₁) = beqMonadHelper x x₁ "Sort"
      compareHnfs (Const-P x) (Const-P x₁) = beqMonadHelper x x₁ "Const"
      compareHnfs (App-P t t₁) (App-P x x₁) = checkβηPure t x >> checkβηPure t₁ x₁
      compareHnfs (Lam-P _ t) (Lam-P _ t₁) = checkβηPure t t₁
      compareHnfs (Pi-P _ t t₁) (Pi-P _ x x₁) = checkβηPure t x >> checkβηPure t₁ x₁
      compareHnfs (All-P _ t t₁) (All-P _ x x₁) = checkβηPure t x >> checkβηPure t₁ x₁
      compareHnfs (Iota-P _ t t₁) (Iota-P _ x x₁) = checkβηPure t x >> checkβηPure t₁ x₁
      compareHnfs (Eq-P t t₁) (Eq-P x x₁) = checkβηPure t x >> checkβηPure t₁ x₁
      compareHnfs (M-P t) (M-P x) = checkβηPure x t
      compareHnfs (Mu-P t t₁) (Mu-P x x₁) = checkβηPure t x >> checkβηPure t₁ x₁
      compareHnfs (Epsilon-P t) (Epsilon-P x) = checkβηPure t x
      compareHnfs (Gamma-P t t₁) (Gamma-P x x₁) = checkβηPure t x >> checkβηPure t₁ x₁
      compareHnfs t@(Ev-P m x) t'@(Ev-P m' x') with m ≟ m'
      ... | yes refl = void $ primMetaArgsSequence $ primMetaArgsZipWith checkβηPure x x'
      ... | no  _    = hnfError t t'
      compareHnfs (Char-P c) (Char-P c') = beqMonadHelper c c' "Char"
      compareHnfs (CharEq-P t t₁) (CharEq-P x x₁) = checkβηPure t x >> checkβηPure t₁ x₁
      compareHnfs (Lam-P _ t) t₁ = case normalizePure Γ t of λ where
        t''@(App-P t' (Var-P (Bound i))) → if i ≣ (fromℕ 0) ∧ validInContext t' Γ
          then (compareHnfs (decrementIndicesPure t') t₁) else hnfError t'' t₁
        t'' → hnfError t'' t₁
      compareHnfs t (Lam-P _ t₁) = case normalizePure Γ t₁ of λ where
        t''@(App-P t' (Var-P (Bound i))) → if i ≣ (fromℕ 0) ∧ validInContext t' Γ
          then (compareHnfs t (decrementIndicesPure t')) else hnfError t t''
        t'' → hnfError t t''
      {-# CATCHALL #-}
      compareHnfs t t' = hnfError t t'

  checkβη : AnnTerm → AnnTerm → M ⊤
  checkβη t t' = checkβηPure (Erase t) (Erase t')

open CheckEquality public

{-# TERMINATING #-}
synthType synthType' :
  {{_ : Monad M}} {{_ : MonadExcept M String}} → Context → AnnTerm → M AnnTerm

synthType Γ t =
  appendIfError (synthType' Γ t) $
    "\n\nWhile synthesizing type for" <+> shortenString 1000 (show t) <+> "in context:\n" + show {{Context-Show}} Γ

synthType' Γ (Var-A x) =
  maybeToError
    (typeOfDef <$> lookupInContext x Γ)
    ("Lookup failed:" <+> show x <+> "in context" <+> show {{Context-Show}} Γ)
synthType' Γ (Sort-A ⋆) = return $ Sort-A □
synthType' Γ (Sort-A □) = throwError "Cannot synthesize type for the superkind"

synthType' Γ (Const-A CharT) = return $ Sort-A ⋆

synthType' Γ (Pr1-A t) = do
  T ← synthType Γ t
  case (hnfNorm Γ T) of λ
    { (Iota-A _ u u₁) → return u
    ; _ → throwError "Term does not normalize to an iota term" }

synthType' Γ (Pr2-A t) = do
  T ← synthType Γ t
  case (hnfNorm Γ T) of λ
    { (Iota-A _ u u₁) → return $ subst u₁ (Pr1-A t)
    ; _ → throwError "Term does not normalize to an iota term" }

synthType' Γ (Beta-A t t₁) = do
  T ← synthType Γ (Eq-A t t)
  case (hnfNorm Γ T) of λ
    { (Sort-A ⋆) → return $ Eq-A t t
    ; _ → throwError "Equality type does not have the right type. Is this a bug?" }

synthType' Γ (Delta-A t t₁) = do
  T ← synthType Γ t₁
  case (hnfNorm Γ T) of λ
    { (Eq-A u u₁) → do
      catchError
        (pureTermBeq (normalizePure Γ $ Erase u) (Lam-P "" $ Lam-P "" $ BoundVar $ fromℕ 1) >>
         pureTermBeq (normalizePure Γ $ Erase u₁) (Lam-P "" $ Lam-P "" $ BoundVar $ fromℕ 0))
        (λ e → throwError $
          "This equality cannot be used for the delta term:" <+> show u
          <+> "=" <+> show u₁ + "\nError:" <+> e)
      return t
    ; _ → throwError "The second argument of a delta needs to be of an eq type" }

synthType' Γ (Sigma-A t) = do
  T ← synthType Γ t
  case (hnfNorm Γ T) of λ
    { (Eq-A u u₁) → return $ Eq-A u₁ u
    ; _ → throwError "Sigma needs an inhabitant of an eq type as argument" }

synthType' Γ (App-A t t₁) = do
  T ← synthType Γ t
  T₁ ← synthType Γ t₁
  case (hnfNorm Γ T) of λ
    { (Pi-A _ u u₁) → do
      catchError
        (checkβη Γ T₁ u)
        (λ e → throwError ("Type mismatch in application, the type of" <+> show t₁
          <+> ":" <+> show T₁ +  " is not βη-equivalent to" <+> show u + "\nError:" <+> e))
      return $ subst u₁ t₁
    ; v → throwError $
      "The left term in an application needs to have a pi type, while it has type" <+> show v }

synthType' Γ (AppE-A t t₁) = do
  T ← synthType Γ t
  T₁ ← synthType Γ t₁
  case (hnfNorm Γ T) of λ
    { (All-A _ u u₁) → do
      catchError (checkβη Γ u T₁)
        (λ e → throwError
          ("Type mismatch in erased application, the following types are not βη-equivalent:\n"
            + show u + "\n" + show T₁ + "\nError:\n" + e))
      return $ subst u₁ t₁
    ; v → throwError $
      "The left term in an erased application needs to have a forall type, while it has type "
        + show v + "\nTest:" <+> show T }

synthType' Γ (Rho-A t t₁ t₂) = do
  T ← synthType Γ t
  T₁ ← synthType Γ t₂
  case (hnfNorm Γ T) of λ
    { (Eq-A u u₁) → do
      catchError (checkβη Γ (subst t₁ u₁) T₁)
        (λ e → throwError $ "Type mismatch in rho:" <+> show (subst t₁ u₁)
          <+> "should be βη-equivalent to the synthesized type of" <+> show t₂ <+> ": "
          + show T₁ + "\nError:\n" + e)
      return $ subst t₁ u
    ; _ → throwError "The type of the first argument of a rho needs to be an equality" }

synthType' Γ (All-A _ t t₁) = do
  u ← synthType Γ t
  case (hnfNorm Γ u) of λ
    { (Sort-A s) → do
      let Γ' = pushVar t Γ
      u₁ ← synthType Γ' t₁
      case (hnfNorm Γ' u₁) of λ
        { (Sort-A ⋆) → return $ Sort-A ⋆
        ; v → throwError $
          "The type family in forall should have type star, while it has type "
          + show v <+> "(" + show t₁ + ")\nContext:" <+> show {{Context-Show}} Γ' }
    ; _ → throwError "The type of the parameter type in forall should be star or square" }

synthType' Γ (Pi-A _ t t₁) = do
  u ← synthType Γ t
  case (hnfNorm Γ u) of λ
    { (Sort-A s) → do
      let Γ' = pushVar t Γ
      u₁ ← synthType Γ' t₁
      case (hnfNorm Γ u₁) of λ
        { (Sort-A s') → return $ Sort-A s'
        ; v → throwError $
          "The type family in pi should have type star or square, while it has type" <+> show v }
    ; _ → throwError "The type of the parameter type in pi should be star or square" }

synthType' Γ (Iota-A _ t t₁) = do
  u ← synthType Γ t
  case (hnfNorm Γ u) of λ
    { (Sort-A ⋆) → do
      let Γ' = pushVar t Γ
      u₁ ← synthType Γ' t₁
      case (hnfNorm Γ' u₁) of λ
        { (Sort-A ⋆) → return $ Sort-A ⋆
        ; _ → throwError "The type family in iota should have type star"}
    ; _ → throwError "The type of the parameter type in iota should be star" }

synthType' Γ (Lam-A n t t₁) = do
  synthType Γ t
  u ← synthType (pushVar t Γ) t₁
  return (Pi-A n t u)

synthType' Γ (LamE-A n t t₁) =
  if checkFree (Bound (fromℕ 0)) (Erase t₁)
    then throwError "Erased arguments cannot appear bound in a term"
    else do
      synthType Γ t
      u ← synthType (pushVar t Γ) t₁
      return $ All-A n t u

synthType' Γ (Pair-A t t₁ t₂) = do
  catchError (checkβη Γ t t₁)
    (λ e → throwError $
      "The terms in dependent intersection introduction have to be βη-equivalent. They normalize to:\n"
        + show (normalizePure Γ $ Erase t) + "\n"
        + show (normalizePure Γ $ Erase t₁) + "\nError:\n" + e)
  u ← synthType Γ t
  u₁ ← synthType Γ t₁
  catchError
    (checkβη Γ (subst t₂ t) u₁)
    (λ e → throwError
      ("Type mismatch in the second argument of the dependent intersection: "
        + show (subst t₂ t) <+> "should be βη-equivalent to the synthesized type "
        + show u₁ + "\n" + e))
  let res = Iota-A "" u t₂
  u₂ ← synthType Γ res
  case (hnfNorm Γ u₂) of λ
    { (Sort-A ⋆) → return res
    ; _ → throwError
      "The resulting iota type of the dependent intersection doesn't have type star. Is this a Bug?" }

synthType' Γ (Phi-A t t₁ t₂) = do
  T ← synthType Γ t
  case (hnfNorm Γ T) of λ
    { (Eq-A u u₁) → do
      catchError
        (checkβη Γ t₁ u >> checkβη Γ t₂ u₁)
        (λ e → throwError $
          "The arguments to phi are not equivalent to the sides of the equality. Error:\n" + e)
      synthType Γ t₁
    ; _ → throwError "The first argument to phi should be of an equality type" }

synthType' Γ (Eq-A x x₁) =
  if validInContext (Erase x) Γ
    then if validInContext (Erase x₁) Γ
      then return $ Sort-A ⋆
      else throwError
        ("The right term in the equality type needs to be valid in the context:" <+> show x₁)
    else throwError
      ("The left term in the equality type needs to be valid in the context:" <+> show x)

synthType' Γ (M-A t) = do
  T ← synthType Γ t
  case (hnfNorm Γ T) of λ
    { (Sort-A ∗) → return $ Sort-A ∗
    ; _ → throwError "The term M is applied to should have type ∗"}

synthType' Γ (Mu-A t t₁) = do
  T ← synthType Γ t
  T' ← synthType Γ t₁
  case (hnfNorm Γ T) of λ
    { (M-A u) →
      case (hnfNorm Γ T') of λ
        { (Pi-A _ v v₁) → do
          T'' ← if checkFree (Bound $ fromℕ 0) (Erase v₁)
            then throwError ("Index 0 is not allowed to appear in" <+> show v₁)
            else synthType (pushVar v Γ) v₁
          case (hnfNorm Γ T'') of λ
            { (Sort-A ∗) →
              case (hnfNorm Γ v₁) of λ
                { (M-A v₂) →
                  appendIfError
                    (checkβη Γ u v)
                    "The types in μ need to be compatible" >> return (M-A $ decrementIndices v₂)
                ; _ → throwError
                  "The second term in a μ needs to have a Pi type that maps to 'M t' for some 't'" }
            ; _ → throwError "The second term in a μ needs to have a non-dependent Pi type" }
        ; _ → throwError "The second term in a μ needs to have a Pi type" }
    ; _ → throwError "The first term in a μ needs to have type 'M t' for some 't'" }

synthType' Γ (Epsilon-A t) = M-A <$> synthType Γ t

synthType' Γ (Ev-A m t) = do
  T ← traversePrimMetaArgs (synthType Γ) t
  appendIfError
    (primMetaArgsSequence $ primMetaArgsZipWith (checkβη Γ) T $ primMetaS m)
    ("The arguments for primitive" <+> show m <+> "have incorrect types!")
  return $ M-A $ primMetaT m t

synthType' Γ (Gamma-A t t₁) = do
  T ← synthType Γ t
  T₁ ← synthType Γ t₁
  case (hnfNorm Γ T) of λ
    { (M-A u) → do
      appendIfError (checkβη Γ T₁ (Pi-A "" (FreeVar "init$err") (incrementIndicesBy (fromℕ 1) $ M-A u)))
        ("The second term supplied to CatchErr has type" <+> show T₁ +
         ", while it should have type 'init$err → M" <+> show u)
      return $ M-A u
    ; _ → throwError "The first term in CatchErr needs to have type 'M t' for some 't'" }

synthType' Γ (Char-A c) = return (Const-A CharT)
synthType' Γ (CharEq-A t t') = do
  T ← synthType Γ t
  T' ← synthType Γ t'
  case (hnfNorm Γ T) of λ
    { (Const-A CharT) → case (hnfNorm Γ T') of λ
      { (Const-A CharT) → return $ FreeVar "Bool"
      ; _ → throwError "The second term in CharEq needs to have type Char" }
    ; _ → throwError "The first term in CharEq needs to have type Char" }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille