text:
module Types where

import Level
open import Data.Unit as Unit renaming (tt to ∗)
open import Data.List as List
open import Categories.Category using (Category)
open import Function

open import Relation.Binary.PropositionalEquality as PE hiding ([_]; subst)
open import Relation.Binary using (module IsEquivalence; Setoid; module Setoid)
open ≡-Reasoning

Kind = ⊤
import Common.Context Kind as Context
open import Common.Context Kind
  using (Ctx; Var; zero; ctx-cat; ctx-bin-coproducts; _≅V_; ≅V-setoid; Vrefl; Vsym; Vtrans)
  renaming (succ to succ′)
open import Categories.Object.BinaryCoproducts ctx-cat
open BinaryCoproducts ctx-bin-coproducts

postulate
  η-≡ : {A : Set} {B : A → Set}
         {f₁ : (x : A) → B x}{f₂ : (y : A) → B y} →
         ((x : A) → f₁ x ≡ f₂ x) → f₁ ≡ f₂

TyCtx = Ctx
TyVar : Ctx → Set
TyVar Γ = Var Γ ∗
succ : ∀{Γ} (x : TyVar Γ) → TyVar (∗ ∷ Γ)
succ = Context.succ ∗

open Categories.Category.Category ctx-cat
  renaming ( _⇒_ to _▹_
           ; _≡_ to _≈_
           ; _∘_ to _●_
           ; id  to ctx-id
           )

-- | Type syntax
data Type (Γ : TyCtx) : Set where
  var  : (x : TyVar Γ)                     → Type Γ
  _⊕_  : (t₁ : Type Γ)       (t₂ : Type Γ) → Type Γ
  μ    : (t : Type (_ ∷ Γ))                → Type Γ
  _⊗_  : (t₁ : Type Γ)       (t₂ : Type Γ) → Type Γ
  _⇒_  : (t₁ : Type [])      (t₂ : Type Γ) → Type Γ
  ν    : (t : Type (_ ∷ Γ))                → Type Γ

-- | Congruence for types
data _≅T_  {Γ Γ' : Ctx} : Type Γ → Type Γ' → Set where
  var  : ∀{x : TyVar Γ} {x' : TyVar Γ'} → (x ≅V x') → var x ≅T var x'
  _⊕_  : ∀{t₁ t₂ : Type Γ} {t₁' t₂' : Type Γ'} →
         (t₁ ≅T t₁') → (t₂ ≅T t₂') →
         (t₁ ⊕ t₂) ≅T (t₁' ⊕ t₂')
  _⊗_  : ∀{t₁ t₂ : Type Γ} {t₁' t₂' : Type Γ'} →
         (t₁ ≅T t₁') → (t₂ ≅T t₂') →
         (t₁ ⊗ t₂) ≅T (t₁' ⊗ t₂')
  μ    : ∀{t : Type (∗ ∷ Γ)} {t' : Type (∗ ∷ Γ')} →
         (t ≅T t') →
         (μ t) ≅T (μ t')
  _⇒_  : ∀{t₁ t₁' : Type []} {t₂ : Type Γ} {t₂' : Type Γ'} →
         (t₁ ≅T t₁') → (t₂ ≅T t₂') →
         (t₁ ⇒ t₂) ≅T (t₁' ⇒ t₂')
  ν    : ∀{t : Type (∗ ∷ Γ)} {t' : Type (∗ ∷ Γ')} →
         (t ≅T t') →
         (ν t) ≅T (ν t')

Trefl : ∀ {Γ : Ctx} {t : Type Γ} → t ≅T t
Trefl {t = var x}   = var e.refl
  where
    module s = Setoid
    module e = IsEquivalence (s.isEquivalence ≅V-setoid)
Trefl {t = t₁ ⊕ t₂} = Trefl ⊕ Trefl
Trefl {t = μ t}     = μ Trefl
Trefl {t = t ⊗ t₁}  = Trefl ⊗ Trefl
Trefl {t = t ⇒ t₁}  = Trefl ⇒ Trefl
Trefl {t = ν t}     = ν Trefl

Tsym : ∀ {Γ Γ' : Ctx} {t : Type Γ} {t' : Type Γ'} → t ≅T t' → t' ≅T t
Tsym (var u)   = var (Vsym u)
Tsym (u₁ ⊕ u₂) = Tsym u₁ ⊕ Tsym u₂
Tsym (u₁ ⊗ u₂) = Tsym u₁ ⊗ Tsym u₂
Tsym (μ u)     = μ (Tsym u)
Tsym (u₁ ⇒ u₂) = Tsym u₁ ⇒ Tsym u₂
Tsym (ν u)     = ν (Tsym u)

Ttrans : ∀ {Γ₁ Γ₂ Γ₃ : Ctx} {t₁ : Type Γ₁} {t₂ : Type Γ₂} {t₃ : Type Γ₃} →
         t₁ ≅T t₂ → t₂ ≅T t₃ → t₁ ≅T t₃
Ttrans (var u₁) (var u₂)   = var (Vtrans u₁ u₂)
Ttrans (u₁ ⊕ u₂) (u₃ ⊕ u₄) = Ttrans u₁ u₃ ⊕ Ttrans u₂ u₄
Ttrans (u₁ ⊗ u₂) (u₃ ⊗ u₄) = Ttrans u₁ u₃ ⊗ Ttrans u₂ u₄
Ttrans (μ u₁) (μ u₂)       = μ (Ttrans u₁ u₂)
Ttrans (u₁ ⇒ u₂) (u₃ ⇒ u₄) = Ttrans u₁ u₃ ⇒ Ttrans u₂ u₄
Ttrans (ν u₁) (ν u₂)       = ν (Ttrans u₁ u₂)

≡→≅T : ∀ {Γ : Ctx} {t₁ t₂ : Type Γ} →
       t₁ ≡ t₂ → t₁ ≅T t₂
≡→≅T {Γ} {t₁} {.t₁} refl = Trefl

-- Note: makes the equality homogeneous in Γ
≅T-setoid : ∀ {Γ} → Setoid _ _
≅T-setoid {Γ} = record
  { Carrier = Type Γ
  ; _≈_ = _≅T_
  ; isEquivalence = record
    { refl = Trefl ; sym = Tsym ; trans = Ttrans }
  }

import Relation.Binary.EqReasoning as EqR

module ≅T-Reasoning where
  module _ {Γ : Ctx} where
    open EqR (≅T-setoid {Γ}) public
      hiding (_≡⟨_⟩_) renaming (_≈⟨_⟩_ to _≅T⟨_⟩_; begin_ to beginT_; _∎ to _∎T)

-- | Variable renaming in types
rename : {Γ Δ : TyCtx} → (ρ : Γ ▹ Δ) → Type Γ → Type Δ
rename         ρ (var x)   = var (ρ ∗ x)
rename         ρ (t₁ ⊕ t₂) = rename ρ t₁ ⊕ rename ρ t₂
rename {Γ} {Δ} ρ (μ t)     = μ (rename ρ' t)
  where
    ρ' : (∗ ∷ Γ) ▹ (∗ ∷ Δ)
    ρ' = ctx-id {[ ∗ ]} ⧻ ρ
rename         ρ (t₁ ⊗ t₂) = rename ρ t₁ ⊗ rename ρ t₂
rename         ρ (t₁ ⇒ t₂) = t₁ ⇒ rename ρ t₂
rename {Γ} {Δ} ρ (ν t)     = ν (rename ρ' t)
  where
    ρ' : (∗ ∷ Γ) ▹ (∗ ∷ Δ)
    ρ' = ctx-id {[ ∗ ]} ⧻ ρ

-------------------------
---- Generating structure on contexts (derived from renaming)

weaken : {Γ : TyCtx} (Δ : TyCtx) → Type Γ -> Type (Δ ∐ Γ)
weaken {Γ} Δ = rename {Γ} {Δ ∐ Γ} (i₂ {Δ} {Γ})

exchange : (Γ Δ : TyCtx) → Type (Γ ∐ Δ) -> Type (Δ ∐ Γ)
exchange Γ Δ = rename [ i₂ {Δ} {Γ} , i₁ {Δ} {Γ} ]

contract : {Γ : TyCtx} → Type (Γ ∐ Γ) -> Type Γ
contract = rename [ ctx-id , ctx-id ]

-- weaken-id-empty-ctx : (Δ : TyCtx) (t : GType) → weaken {[]} Δ t ≡ t
-- weaken-id-empty-ctx = ?

Subst : TyCtx → TyCtx → Set
Subst Γ Δ = TyVar Γ → Type Δ

id-subst : ∀{Γ : TyCtx} → Subst Γ Γ
id-subst x = var x

extend : ∀{Γ Δ : TyCtx} → Subst Γ Δ → Type Δ → (Subst (∗ ∷ Γ) Δ)
extend σ a zero        = a
extend σ _ (succ′ _ x) = σ x

single-subst : ∀{Γ : TyCtx} → Type Γ → (Subst (∗ ∷ Γ) Γ)
single-subst a zero        = a
single-subst _ (succ′ _ x) = var x

lift : ∀{Γ Δ} → Subst Γ Δ → Subst (∗ ∷ Γ) (∗ ∷ Δ)
lift σ = extend (weaken [ ∗ ] ∘ σ) (var zero)

-- | Simultaneous substitution
subst : {Γ Δ : TyCtx} → (σ : Subst Γ Δ) → Type Γ → Type Δ
subst         σ (var x)   = σ x
subst         σ (t₁ ⊕ t₂) = subst σ t₁ ⊕ subst σ t₂
subst {Γ} {Δ} σ (μ t)     = μ (subst (lift σ) t)
subst         σ (t₁ ⊗ t₂) = subst σ t₁ ⊗ subst σ t₂
subst         σ (t₁ ⇒ t₂) = t₁ ⇒ subst σ t₂
subst {Γ} {Δ} σ (ν t)     = ν (subst (lift σ) t)

subst₀ : {Γ : TyCtx} → Type Γ → Type (∗ ∷ Γ) → Type Γ
subst₀ {Γ} a = subst (extend id-subst a)

rename′ : {Γ Δ : TyCtx} → (ρ : Γ ▹ Δ) → Type Γ → Type Δ
rename′ ρ = subst (var ∘ (ρ ∗))

-- | Ground type
GType = Type []

-- | Unfold lfp
unfold-μ : (Type [ ∗ ]) → GType
unfold-μ a = subst₀ (μ a) a

-- | Unfold gfp
unfold-ν : (Type [ ∗ ]) → GType
unfold-ν a = subst₀ (ν a) a

--------------------------------------------------
---- Examples

unit' : GType
unit' = ν (var zero)

Nat : Type []
Nat = μ ((weaken [ ∗ ] unit') ⊕ x)
  where x = var zero

Str-Fun : {Γ : TyCtx} → Type Γ → Type (∗ ∷ Γ)
Str-Fun a = (weaken [ ∗ ] a ⊗ x)
  where x = var zero

Str : {Γ : TyCtx} → Type Γ → Type Γ
Str a = ν (Str-Fun a)

postulate
  lem :  ∀ {Γ : Ctx} (a : Type Γ) (σ : Subst Γ Γ) →
         lift (extend σ a) ≡ extend (lift σ) (weaken [ ∗ ] a)
  lem2 : ∀ {Γ : Ctx} →
         ctx-id {[ ∗ ]} ⧻ i₂ {[ ∗ ]} {Γ} ≡ i₂ {[ ∗ ]} {∗ ∷ Γ}
{-
lem {Γ} b σ =
  begin
    lift (extend σ b)
  ≡⟨ refl ⟩
    extend (weaken [ ∗ ] ∘ (extend σ b)) (var zero)
  ≡⟨ {!!} ⟩
    extend (extend (weaken [ ∗ ] ∘ σ) (var zero))
           (rename {Γ} {[ ∗ ] ∐ Γ} (i₂ {[ ∗ ]} {Γ}) b)
  ≡⟨ refl ⟩
    extend (extend (weaken [ ∗ ] ∘ σ) (var zero)) (weaken [ ∗ ] b)
  ≡⟨ refl ⟩
    extend (lift σ) (weaken [ ∗ ] b)
  ∎
-}

lem3 : ∀ {Γ : Ctx} (a : Type (∗ ∷ Γ)) →
       rename (ctx-id {[ ∗ ]} ⧻ i₂ {[ ∗ ]} {Γ}) a ≡ weaken [ ∗ ] a
lem3 {Γ} a =
     begin
        rename (ctx-id {[ ∗ ]} ⧻ i₂ {[ ∗ ]} {Γ}) a
      ≡⟨ cong (λ x → rename x a) lem2 ⟩
        rename {(∗ ∷ Γ)} {∗ ∷ ∗ ∷ Γ} (i₂ {[ ∗ ]}) a
      ≡⟨ refl ⟩
        rename {(∗ ∷ Γ)} {[ ∗ ] ∐ (∗ ∷ Γ)} (i₂ {[ ∗ ]}) a
      ≡⟨ refl ⟩
        weaken [ ∗ ] a
      ∎

lemma : ∀ {Γ : Ctx} {a b : Type Γ} {σ : Subst Γ Γ} →
        subst (extend σ b) (weaken [ ∗ ] a) ≅T subst σ a
lemma {a = var x}   = Trefl
lemma {a = a₁ ⊕ a₂} = lemma {a = a₁} ⊕ lemma {a = a₂}
lemma {Γ} {μ a} {b} {σ} = μ r
  where
    σ' : Subst (∗ ∷ Γ) (∗ ∷ Γ)
    σ' = lift σ
    b' : Type (∗ ∷ Γ)
    b' = weaken [ ∗ ] b
    a' = rename (ctx-id {[ ∗ ]} ⧻ i₂ {[ ∗ ]} {Γ}) a
    x : subst (extend σ' b') a' ≅T subst σ' a
    x = Ttrans
        (≡→≅T (cong (λ y → subst (extend σ' b') y) (lem3 a)))
        (lemma {∗ ∷ Γ} {a} {b'} {σ'})
    r : subst (lift (extend σ b)) a' ≅T subst (lift σ) a
    r = Ttrans (≡→≅T (cong (λ y → subst y a') (lem b σ))) x
lemma {a = a₁ ⊗ a₂} = lemma {a = a₁} ⊗ lemma {a = a₂}
lemma {a = a₁ ⇒ a₂} = Trefl ⇒ lemma {a = a₂}
lemma {Γ} {ν a} {b} {σ} = ν r
  where
    σ' : Subst (∗ ∷ Γ) (∗ ∷ Γ)
    σ' = lift σ
    b' : Type (∗ ∷ Γ)
    b' = weaken [ ∗ ] b
    a' = rename (ctx-id {[ ∗ ]} ⧻ i₂ {[ ∗ ]} {Γ}) a
    x : subst (extend σ' b') a' ≅T subst σ' a
    x = Ttrans
        (≡→≅T (cong (λ y → subst (extend σ' b') y) (lem3 a)))
        (lemma {∗ ∷ Γ} {a} {b'} {σ'})
    r : subst (lift (extend σ b)) a' ≅T subst (lift σ) a
    r = Ttrans (≡→≅T (cong (λ y → subst y a') (lem b σ))) x

lift-id-is-id-ext : ∀ {Γ : Ctx} (x : TyVar (∗ ∷ Γ)) →
                    (lift (id-subst {Γ})) x ≡ id-subst x
lift-id-is-id-ext zero        = refl
lift-id-is-id-ext (succ′ ∗ x) = refl

lift-id-is-id : ∀ {Γ : Ctx} → lift (id-subst {Γ}) ≡ id-subst
lift-id-is-id = η-≡ lift-id-is-id-ext

id-subst-id : ∀ {Γ : Ctx} {a : Type Γ} →
              subst id-subst a ≅T a
id-subst-id {a = var x}  = var Vrefl
id-subst-id {a = a ⊕ a₁} = id-subst-id ⊕ id-subst-id
id-subst-id {a = μ a}    =
  μ (Ttrans (≡→≅T (cong (λ u → subst u a) lift-id-is-id)) id-subst-id)
id-subst-id {a = a ⊗ a₁} = id-subst-id ⊗ id-subst-id
id-subst-id {a = a ⇒ a₁} = Trefl ⇒ id-subst-id
id-subst-id {a = ν a}    =
  ν (Ttrans (≡→≅T (cong (λ u → subst u a) lift-id-is-id)) id-subst-id)

lemma₂ : ∀ {Γ : Ctx} {a b : Type Γ} →
        subst (extend id-subst b) (weaken [ ∗ ] a) ≅T a
lemma₂ {Γ} {a} {b} = Ttrans (lemma {Γ} {a} {b} {σ = id-subst}) id-subst-id

unfold-str : ∀{a : Type []} → (unfold-ν (Str-Fun a)) ≅T (a ⊗ Str a)
unfold-str {a} = lemma₂ ⊗ Trefl

LFair : {Γ : TyCtx} → Type Γ → Type Γ → Type Γ
LFair a b = ν (μ ((w a ⊗ x) ⊕ (w b ⊗ y)))
  where
    x = var zero
    y = var (succ zero)
    Δ = ∗ ∷ [ ∗ ]
    w = weaken Δ

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
-- Simple test to check if constraint solving for injective
-- functions is working.
module Injectivity where

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

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

{-# BUILTIN NATURAL Nat  #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}
{-# BUILTIN NATPLUS _+_  #-}

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

foldr : {A B : Set} -> (A -> B -> B) -> B -> List A -> B
foldr f z []        = z
foldr f z (x :: xs) = f x (foldr f z xs)

data U : Set where
  nat  : U
  list : U -> U

El : U -> Set
El nat      = Nat
El (list a) = List (El a)

sum : {a : U} -> El a -> Nat
sum {nat}    n  = n
sum {list a} xs = foldr (\a b -> sum a + b) zero xs

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

test₁ = sum (1 :: 2 :: 3 :: [])

ok₁ : test₁ == 6
ok₁ = refl

test₂ = sum ((1 :: []) :: (3 :: 5 :: []) :: [])

ok₂ : test₂ == 9
ok₂ = refl

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.SumFin.Base where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty using (⊥; ⊥-elim) public
open import Cubical.Data.Unit using (tt) renaming (Unit to ⊤) public
open import Cubical.Data.Sum using (_⊎_; inl; inr) public

open import Cubical.Data.Nat

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

private variable k : ℕ

Fin : ℕ → Type₀
Fin zero = ⊥
Fin (suc n) = ⊤ ⊎ (Fin n)

pattern fzero = inl tt
pattern fsuc n = inr n

finj : Fin k → Fin (suc k)
finj {suc k} fzero    = fzero
finj {suc k} (fsuc n) = fsuc (finj {k} n)

toℕ : Fin k → ℕ
toℕ {suc k} (inl tt) = zero
toℕ {suc k} (inr x)  = suc (toℕ {k} x)

toℕ-injective : {m n : Fin k} → toℕ m ≡ toℕ n → m ≡ n
toℕ-injective {suc k} {fzero}  {fzero}  _ = refl
toℕ-injective {suc k} {fzero}  {fsuc x} p = ⊥-elim (znots p)
toℕ-injective {suc k} {fsuc m} {fzero}  p = ⊥-elim (snotz p)
toℕ-injective {suc k} {fsuc m} {fsuc x} p = cong fsuc (toℕ-injective (injSuc p))

-- Thus, Fin k is discrete
discreteFin : Discrete (Fin k)
discreteFin fj fk with discreteℕ (toℕ fj) (toℕ fk)
... | yes p = yes (toℕ-injective p)
... | no ¬p = no (λ p → ¬p (cong toℕ p))

isSetFin : isSet (Fin k)
isSetFin = Discrete→isSet discreteFin

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module Issue318 where

data Bool : Set where

module A where
  data _≤_ : Bool → Bool → Set where

open A hiding (_≤_)

data _≤_ : Bool → Bool → Set where

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module NestedProjectRoots where

import Imports.A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --guardedness-preserving-type-constructors #-}

module TypeConstructorsWhichPreserveGuardedness4 where

open import Common.Coinduction

data Rec (A : ∞ Set) : Set where
  fold : ♭ A → Rec A

D : Set
D = Rec (♯ (D → D))

-- _·_ : D → D → D
-- fold f · x = f x

-- ω : D
-- ω = fold (λ x → x · x)

-- Ω : D
-- Ω = ω · ω

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


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

module Class where

open import Cubical.Core.Everything
open import Function.Base using (id; _$_)

private
  variable
    A B C : Set
    ℓ ℓ′ ℓ″ : Level

-- Custom non-dependent definition, since the one in the prelude is too general
_∘_ : {A : Set ℓ} {B : Set ℓ′} {C : Set ℓ″} → (B → C) → (A → B) → A → C
(f ∘ g) x = f (g x)

infixr 9 _∘_

record Functor (F : Set → Set₁) : Set₂ where
  field
    fmap : (A → B) → F A → F B
    fmap-id-legit : (m : F A) → fmap id m ≡ m
    fmap-compose-legit
      : (m : F A)
      → (f : B → C)
      → (g : A → B)
      → fmap (f ∘ g) m ≡ fmap f (fmap g m)
  _<$>_ : (A → B) → F A → F B
  f <$> x = fmap f x

open Functor

record Applicative (F : Set → Set₁) : Set₂ where
  infixl 4 _<*>_

  field
    functor : Functor F
    pure : A → F A
    _<*>_ : F (A → B) → F A → F B
    app-identity : (v : F A) → (pure id <*> v) ≡ v
    app-compose
      : (u : F (B → C))
      → (v : F (A → B))
      → (w : F A)
      → (pure _∘_ <*> u <*> v <*> w) ≡ (u <*> (v <*> w))
    app-homo
      : (f : A → B)
      → (x : A)
      → (pure f <*> pure x) ≡ pure (f x)
    app-intchg
      : (u : F (A → B))
      → (y : A)
      → (u <*> pure y) ≡ (pure (_$ y) <*> u)

  open Functor functor public

record Monad (M : Set → Set₁) : Set₂ where
  infixl 1 _>>=_

  field
    applicative : Applicative M
    _>>=_ : M A → (A → M B) → M B

  open Applicative applicative public

  return : A → M A
  return = pure

  field
    monad-left-id
      : (a : A)
      → (f : A → M B)
      → (return a >>= f) ≡ f a
    monad-right-id
      : (m : M A)
      → (m >>= return) ≡ m
    monad-assoc
      : (m : M A)
      → (f : A → M B)
      → (g : B → M C)
      → (m >>= f >>= g) ≡ (m >>= (λ x → f x >>= g))


text:
{-
The equivalent "goodness" of can w.r.t. the rmerge reduction.
The lemma proved in this file is

    can-irr : ∀ {BV} {FV} θ₁ θ₂ q →
      CorrectBinding q BV FV →
      (distinct' (proj₁ FV) (proj₁ (Dom θ₂))) →
       Can q θ₁ ≡ Can q (θ₁ ← θ₂)

That is, the result of the Can function will not change
provided that the program does not refer to any variables
in the new environment.

-}
module Esterel.Lang.CanFunction.MergePotentialRuleCan where

open import utility

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.CanFunction
open import Esterel.Lang.CanFunction.Base
open import Esterel.Context
open import Esterel.Context.Properties
  using (plug ; unplug)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; Dom ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)

open import Data.Bool
  using (Bool ; true ; false ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; [] ; _∷_ ; _++_ ; map ; concatMap)
open import Data.List.Properties
  using (map-id)
open import Data.List.Any
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties
  using ()
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ)
open import Data.Maybe
  using (Maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; zero ; suc ; _≟_ ; _+_)
open import Data.Nat.Properties.Simple
  using (+-comm)
open import Data.Product
  using (Σ ; proj₁ ; proj₂ ; ∃ ; _,_ ; _,′_ ; _×_)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Function
  using (_∘_ ; _∋_ ; id)
open import Relation.Nullary
  using (¬_ ; Dec ; yes ; no)
open import Relation.Nullary.Decidable
  using (⌊_⌋)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; trans ; sym ; cong ; subst)

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM

open ListSet Data.Nat._≟_
  using (set-subtract ; set-subtract-[] ; set-subtract-split ; set-subtract-merge
       ; set-subtract-notin
       ; set-remove-mono-∈ ; set-remove-removed ; set-remove-not-removed)

can-new-irr : ∀ {BV} {FV} θ₁ θ₂ θo q →
  CorrectBinding q BV FV →
  (∀ S' → S' ∈ (proj₁ FV) → (S' ∉ proj₁ (Dom θ₂)) ⊎ (S' ∈ proj₁ (Dom θo))) →
  Can q (θ₁ ← θo) ≡ Can q ((θ₁ ← θ₂) ← θo)

canθ-new-irr : ∀ {BV} {FV} sigs S θ₁ θ₂ θo q →
  CorrectBinding q BV FV →
  (∀ S' → S' ∈ (proj₁ FV) →
    ((S' ∉ proj₁ (Dom θ₂)) ⊎ (S' ∈ proj₁ (Dom θo))) ⊎
    S' ∈ map (_+_ S) (SigMap.keys sigs)) →
  Canθ sigs S q (θ₁ ← θo) ≡ Canθ sigs S q ((θ₁ ← θ₂) ← θo)

can-new-irr θ₁ θ₂ θo nothin CBnothing S-prop = refl
can-new-irr θ₁ θ₂ θo pause CBpause S-prop = refl
can-new-irr θ₁ θ₂ θo (signl S q) (CBsig cbq) S-prop
  rewrite canθ-new-irr (Env.sig ([S]-env S)) 0 θ₁ θ₂ θo q cbq
            (λ S' S'∈FV →
              Data.Sum.map
                (S-prop S')
                (subst (S' ∈_) (sym (map-id (proj₁ (Dom ([S]-env S))))) ∘
                 (λ S'∈[S] →
                   subst (_∈ proj₁ (Dom ([S]-env S)))
                     (sym (∈:: S'∈[S]))
                     (Env.sig-∈-single S Signal.unknown)))
                (set-subtract-split {ys = Signal.unwrap S ∷ []} S'∈FV))
  = refl
can-new-irr θ₁ θ₂ θo (present S ∣⇒ p ∣⇒ q) (CBpresent {FVp = FVp} cbp cbq) S-prop
  with S-prop (Signal.unwrap S) (here refl)| Env.Sig∈ S (θ₁ ← θo) | Env.Sig∈ S ((θ₁ ← θ₂) ← θo)
... | inj₂ S∈Domθo | no  S∉domθ₁←θo | S∈domθ₁←θ₂←θo? =
  ⊥-elim (S∉domθ₁←θo (Env.sig-←-monoʳ S θo θ₁ S∈Domθo))
... | inj₂ S∈Domθo | yes S∈domθ₁←θo | no  S∉domθ₁←θ₂←θo =
  ⊥-elim (S∉domθ₁←θ₂←θo (Env.sig-←-monoʳ S θo (θ₁ ← θ₂) S∈Domθo))
... | inj₂ S∈Domθo | yes S∈domθ₁←θo | yes S∈domθ₁←θ₂←θo
  rewrite SigMap.∈-get-U-irr-m S (Env.sig θ₁) (Env.sig (θ₁ ← θ₂)) (Env.sig θo)
          S∈domθ₁←θo S∈domθ₁←θ₂←θo S∈Domθo
  with Env.sig-stats {S} ((θ₁ ← θ₂) ← θo) S∈domθ₁←θ₂←θo
... | Signal.present = can-new-irr θ₁ θ₂ θo p cbp
                         (λ S' S'∈FVp → S-prop S' (++ʳ (Signal.unwrap S ∷ []) (++ˡ S'∈FVp)))
... | Signal.absent  = can-new-irr θ₁ θ₂ θo q cbq
                         (λ S' S'∈FVq → S-prop S' (++ʳ (Signal.unwrap S ∷ proj₁ FVp) S'∈FVq))
... | Signal.unknown
  rewrite can-new-irr θ₁ θ₂ θo p cbp
            (λ S' S'∈FVp → S-prop S' (++ʳ (Signal.unwrap S ∷ []) (++ˡ S'∈FVp)))
        | can-new-irr θ₁ θ₂ θo q cbq
            (λ S' S'∈FVq → S-prop S' (++ʳ (Signal.unwrap S ∷ proj₁ FVp) S'∈FVq))
  = refl
can-new-irr θ₁ θ₂ θo (present S ∣⇒ p ∣⇒ q) (CBpresent {FVp = FVp} cbp cbq) S-prop
  | inj₁ S∉Domθ₂ | yes S∈domθ₁←θo | yes S∈domθ₁←θ₂←θo
  with Env.sig-←⁻ {θ₁} {θo} S S∈domθ₁←θo
... | inj₂ S∈Domθo
  rewrite SigMap.∈-get-U-irr-m S (Env.sig θ₁) (Env.sig (θ₁ ← θ₂)) (Env.sig θo)
          S∈domθ₁←θo S∈domθ₁←θ₂←θo S∈Domθo
  with Env.sig-stats {S} ((θ₁ ← θ₂) ← θo) S∈domθ₁←θ₂←θo
... | Signal.present = can-new-irr θ₁ θ₂ θo p cbp
                         (λ S' S'∈FVp → S-prop S' (++ʳ (Signal.unwrap S ∷ []) (++ˡ S'∈FVp)))
... | Signal.absent  = can-new-irr θ₁ θ₂ θo q cbq
                         (λ S' S'∈FVq → S-prop S' (++ʳ (Signal.unwrap S ∷ proj₁ FVp) S'∈FVq))
... | Signal.unknown
  rewrite can-new-irr θ₁ θ₂ θo p cbp
            (λ S' S'∈FVp → S-prop S' (++ʳ (Signal.unwrap S ∷ []) (++ˡ S'∈FVp)))
        | can-new-irr θ₁ θ₂ θo q cbq
            (λ S' S'∈FVq → S-prop S' (++ʳ (Signal.unwrap S ∷ proj₁ FVp) S'∈FVq))
  = refl
can-new-irr θ₁ θ₂ θo (present S ∣⇒ p ∣⇒ q) (CBpresent {FVp = FVp} cbp cbq) S-prop
  | inj₁ S∉Domθ₂ | yes S∈domθ₁←θo | yes S∈domθ₁←θ₂←θo
  | inj₁ S∈domθ₁ with Env.sig-←-irr-get {θ₁} {θ₂} {S} S∈domθ₁ S∉Domθ₂
... | a , b rewrite SigMap.get-U-both-irr-m S (Env.sig θ₁) (Env.sig (θ₁ ← θ₂)) (Env.sig θo) S∈domθ₁ a S∈domθ₁←θo S∈domθ₁←θ₂←θo b
  with Env.sig-stats {S} ((θ₁ ← θ₂) ← θo) S∈domθ₁←θ₂←θo
... | Signal.present = can-new-irr θ₁ θ₂ θo p cbp
                         (λ S' S'∈FVp → S-prop S' (++ʳ (Signal.unwrap S ∷ []) (++ˡ S'∈FVp)))
... | Signal.absent  = can-new-irr θ₁ θ₂ θo q cbq
                         (λ S' S'∈FVq → S-prop S' (++ʳ (Signal.unwrap S ∷ proj₁ FVp) S'∈FVq))
... | Signal.unknown
  rewrite can-new-irr θ₁ θ₂ θo p cbp
            (λ S' S'∈FVp → S-prop S' (++ʳ (Signal.unwrap S ∷ []) (++ˡ S'∈FVp)))
        | can-new-irr θ₁ θ₂ θo q cbq
            (λ S' S'∈FVq → S-prop S' (++ʳ (Signal.unwrap S ∷ proj₁ FVp) S'∈FVq))
  = refl
can-new-irr θ₁ θ₂ θo (present S ∣⇒ p ∣⇒ q) (CBpresent cbp cbq) S-prop
  | inj₁ S∉Domθ₂ | yes S∈domθ₁←θo | no  S∉domθ₁←θ₂←θo
  rewrite SigMap.keys-assoc-comm (Env.sig θ₁) (Env.sig θ₂) (Env.sig θo)
  = ⊥-elim (S∉domθ₁←θ₂←θo (SigMap.U-mono {m = Env.sig (θ₁ ← θo)} {k = S} S∈domθ₁←θo))
can-new-irr θ₁ θ₂ θo (present S ∣⇒ p ∣⇒ q) (CBpresent cbp cbq) S-prop
  | inj₁ S∉Domθ₂ | no  S∉domθ₁←θo | yes S∈domθ₁←θ₂←θo
  with Env.sig-←⁻ {θ₁ ← θo} {θ₂} S
                  (subst (Signal.unwrap S ∈_)
                    (SigMap.keys-assoc-comm (Env.sig θ₁) (Env.sig θ₂) (Env.sig θo))
                    S∈domθ₁←θ₂←θo)
... | (inj₁ S∈Domθ₁←θo) = ⊥-elim (S∉domθ₁←θo S∈Domθ₁←θo)
... | (inj₂ S∈Domθ₂) = ⊥-elim (S∉Domθ₂ S∈Domθ₂)
can-new-irr θ₁ θ₂ θo (present S ∣⇒ p ∣⇒ q) (CBpresent {FVp = FVp} cbp cbq) S-prop
  | inj₁ S∉Domθ₂ | no  S∉domθ₁←θo | no  S∉domθ₁←θ₂←θo
  rewrite can-new-irr θ₁ θ₂ θo p cbp
            (λ S' S'∈FVp → S-prop S' (++ʳ (Signal.unwrap S ∷ []) (++ˡ S'∈FVp)))
        | can-new-irr θ₁ θ₂ θo q cbq
            (λ S' S'∈FVq → S-prop S' (++ʳ (Signal.unwrap S ∷ proj₁ FVp) S'∈FVq))
  = refl
can-new-irr θ₁ θ₂ θo (emit S) CBemit S-prop = refl
can-new-irr θ₁ θ₂ θo (p ∥ q) (CBpar {FVp = FVp} cbp cbq BVp≠BVq FVp≠BVq BVp≠FVq Xp≠Xq) S-prop
  rewrite can-new-irr θ₁ θ₂ θo p cbp (λ S' S'∈FVp → S-prop S' (++ˡ S'∈FVp))
        | can-new-irr θ₁ θ₂ θo q cbq (λ S' S'∈FVq → S-prop S' (++ʳ (proj₁ FVp) S'∈FVq))
  = refl
can-new-irr θ₁ θ₂ θo (loop q) (CBloop cbq BV≠FV) S-prop =
  can-new-irr θ₁ θ₂ θo q cbq S-prop
can-new-irr θ₁ θ₂ θo (loopˢ p q) (CBloopˢ {BVp = BVp} {FVp = FVp} CBp CBq BVp≠FVq BVq≠FVq) S-prop
  rewrite can-new-irr θ₁ θ₂ θo p CBp (λ S' S'∈FVp → S-prop S' (++ˡ S'∈FVp))
        | can-new-irr θ₁ θ₂ θo q CBq (λ S' S'∈FVq → S-prop S' (++ʳ (proj₁ FVp) S'∈FVq))
 = refl
can-new-irr θ₁ θ₂ θo (p >> q) (CBseq {BVp = BVp} {FVp = FVp} cbp cbq BVp≠FVq) S-prop
  with can-new-irr θ₁ θ₂ θo p cbp (λ S' S'∈FVp → S-prop S' (++ˡ S'∈FVp))
... | can-p-θ₁←θo≡can-p-θ₁←θ₂←θo
  with any (Code._≟_ Code.nothin) (Canₖ p (θ₁ ← θo))
     | any (Code._≟_ Code.nothin) (Canₖ p ((θ₁ ← θ₂) ← θo))
... | yes nothin∈can-p-θ₁←θo | yes nothin∈can-p-θ₁←θ₂←θo
  rewrite can-p-θ₁←θo≡can-p-θ₁←θ₂←θo
        | can-new-irr θ₁ θ₂ θo q cbq (λ S' S'∈FVq → S-prop S' (++ʳ (proj₁ FVp) S'∈FVq))
  = refl
... | yes nothin∈can-p-θ₁←θo | no  nothin∉can-p-θ₁←θ₂←θo
  = ⊥-elim (nothin∉can-p-θ₁←θ₂←θo
            (subst (λ xs → Code.nothin ∈ proj₁ (proj₂ xs))
                   can-p-θ₁←θo≡can-p-θ₁←θ₂←θo
                   nothin∈can-p-θ₁←θo))
... | no  nothin∉can-p-θ₁←θo | yes nothin∈can-p-θ₁←θ₂←θo
  = ⊥-elim (nothin∉can-p-θ₁←θo
            (subst (λ xs → Code.nothin ∈ proj₁ (proj₂ xs))
                   (sym can-p-θ₁←θo≡can-p-θ₁←θ₂←θo)
                   nothin∈can-p-θ₁←θ₂←θo))
... | no  nothin∉can-p-θ₁←θo | no  nothin∉can-p-θ₁←θ₂←θo
  rewrite can-p-θ₁←θo≡can-p-θ₁←θ₂←θo = refl
can-new-irr θ₁ θ₂ θo (suspend q S) (CBsusp cbq [S]≠BVp) S-prop =
  can-new-irr θ₁ θ₂ θo q cbq (λ S' S'∈FV → S-prop S' (there S'∈FV))
can-new-irr θ₁ θ₂ θo (exit n) CBexit S-prop = refl
can-new-irr θ₁ θ₂ θo (trap q) (CBtrap cbq) S-prop
  rewrite can-new-irr θ₁ θ₂ θo q cbq S-prop
  = refl
can-new-irr θ₁ θ₂ θo (shared s ≔ e in: q) (CBshared {FV = FV} cbq) S-prop
  rewrite set-subtract-[] (proj₁ FV)
        | can-new-irr θ₁ θ₂ θo q cbq (λ S' S'∈FV → S-prop S' (++ʳ (proj₁ (FVₑ e)) S'∈FV))
  = refl
can-new-irr θ₁ θ₂ θo (s ⇐ e) CBsset S-prop = refl
can-new-irr θ₁ θ₂ θo (var x ≔ e in: q) (CBvar {FV = FV} cbq) S-prop
  rewrite set-subtract-[] (proj₁ FV)
  = can-new-irr θ₁ θ₂ θo q cbq (λ S' S'∈FV → S-prop S' (++ʳ (proj₁ (FVₑ e)) S'∈FV))
can-new-irr θ₁ θ₂ θo (x ≔ e) CBvset S-prop = refl
can-new-irr θ₁ θ₂ θo (if x ∣⇒ p ∣⇒ q) (CBif {FVp = FVp} cbp cbq) S-prop
  rewrite can-new-irr θ₁ θ₂ θo p cbp (λ S' S'∈FVp → S-prop S' (++ˡ S'∈FVp))
        | can-new-irr θ₁ θ₂ θo q cbq (λ S' S'∈FVq → S-prop S' (++ʳ (proj₁ FVp) S'∈FVq))
  = refl
can-new-irr θ₁ θ₂ θo (ρ⟨ θ , A ⟩· q) (CBρ {FV = FV} cbq) S-prop
  rewrite canθ-new-irr (Env.sig θ) 0 θ₁ θ₂ θo q cbq
            (λ S' S'∈FV →
              Data.Sum.map
                (S-prop S')
                (subst (S' ∈_) (sym (map-id (proj₁ (Dom θ)))))
                (set-subtract-split {ys = proj₁ (Dom θ)} S'∈FV))
  = refl

canθ-new-irr-S-prop-accumulate : ∀ {xs ys zs} S status θo →

  (∀ S' → S' ∈ xs →
    (S' ∉ ys ⊎ S' ∈ proj₁ (Dom θo)) ⊎
    S' ∈ (S + 0 ∷ map (_+_ S) (map suc zs))) →

  ∀ S' → S' ∈ xs →
    (S' ∉ ys ⊎ S' ∈ proj₁ (Dom (θo ← [ (S ₛ) ↦ status ]))) ⊎
    S' ∈ map (_+_ (suc S)) zs

canθ-new-irr-S-prop-accumulate {zs = zs} S status θo S-prop S' S'∈xs with S-prop S' S'∈xs
... | inj₁ (inj₁ S'∉ys) = inj₁ (inj₁ S'∉ys)
... | inj₁ (inj₂ S'∈Domθo) =
  inj₁ (inj₂ (Env.sig-←-monoˡ (S' ₛ) θo [ (S ₛ) ↦ status ]  S'∈Domθo))
... | inj₂ (here refl) rewrite +-comm S 0 =
  inj₁ (inj₂ (Env.sig-←-monoʳ (S ₛ) [ S ₛ ↦ status ] θo (Env.sig-∈-single (S ₛ) status)))
... | inj₂ (there S'∈map-+-S-suc-zs)
  rewrite map-+-compose-suc S zs
  = inj₂ S'∈map-+-S-suc-zs

canθ-new-irr {BV} {FV} [] S θ₁ θ₂ θo q cbq S-prop =
  can-new-irr θ₁ θ₂ θo q cbq S-prop'
  where
    S-prop' : ∀ S' → S' ∈ proj₁ FV → S' ∉ proj₁ (Dom θ₂) ⊎ S' ∈ proj₁ (Dom θo)
    S-prop' S' S'∈FV with S-prop S' S'∈FV
    ... | inj₁ S'∉Domθ₂⊎S'∈Domθo = S'∉Domθ₂⊎S'∈Domθo
    ... | inj₂ ()
canθ-new-irr (nothing ∷ sigs) S θ₁ θ₂ θo q cbq S-prop =
  canθ-new-irr sigs (suc S) θ₁ θ₂ θo q cbq
    (λ S' S'∈FV →
      Data.Sum.map id (subst (S' ∈_) (map-+-compose-suc S (SigMap.keys sigs)))
        (S-prop S' S'∈FV))
canθ-new-irr (just Signal.present ∷ sigs) S θ₁ θ₂ θo q cbq S-prop
  rewrite sym (Env.←-assoc θ₁ θo ([S]-env-present (S ₛ)))
        | sym (Env.←-assoc (θ₁ ← θ₂) θo ([S]-env-present (S ₛ)))
  = canθ-new-irr sigs (suc S) θ₁ θ₂ (θo ← [S]-env-present (S ₛ)) q cbq
      (canθ-new-irr-S-prop-accumulate S Signal.present θo S-prop)
canθ-new-irr (just Signal.absent ∷ sigs) S θ₁ θ₂ θo q cbq S-prop
  rewrite sym (Env.←-assoc θ₁ θo ([S]-env-absent (S ₛ)))
        | sym (Env.←-assoc (θ₁ ← θ₂) θo ([S]-env-absent (S ₛ)))
  = canθ-new-irr sigs (suc S) θ₁ θ₂ (θo ← [S]-env-absent (S ₛ)) q cbq
      (canθ-new-irr-S-prop-accumulate S Signal.absent θo S-prop)
canθ-new-irr (just Signal.unknown ∷ sigs) S θ₁ θ₂ θo q cbq S-prop
  with any (_≟_ S) (Canθₛ sigs (suc S) q ((θ₁ ← θo) ← [S]-env (S ₛ)))
     | any (_≟_ S) (Canθₛ sigs (suc S) q (((θ₁ ← θ₂) ← θo) ← [S]-env (S ₛ)))
... | yes S∈canθ-sigs-q-θ₁←θo←[S] | yes S∈canθ-sigs-q-θ₁←θ₂←θo←[S]
  rewrite sym (Env.←-assoc θ₁ θo ([S]-env (S ₛ)))
        | sym (Env.←-assoc (θ₁ ← θ₂) θo ([S]-env (S ₛ)))
  = canθ-new-irr sigs (suc S) θ₁ θ₂ (θo ← [S]-env (S ₛ)) q cbq
      (canθ-new-irr-S-prop-accumulate S Signal.unknown θo S-prop)
... | no  S∉canθ-sigs-q-θ₁←θo←[S] | no  S∉canθ-sigs-q-θ₁←θ₂←θo←[S]
  rewrite sym (Env.←-assoc θ₁ θo ([S]-env-absent (S ₛ)))
        | sym (Env.←-assoc (θ₁ ← θ₂) θo ([S]-env-absent (S ₛ)))
  = canθ-new-irr sigs (suc S) θ₁ θ₂ (θo ← [S]-env-absent (S ₛ)) q cbq
      (canθ-new-irr-S-prop-accumulate S Signal.absent θo S-prop)
... | yes S∈canθ-sigs-q-θ₁←θo←[S] | no  S∉canθ-sigs-q-θ₁←θ₂←θo←[S]
  rewrite sym (Env.←-assoc θ₁ θo ([S]-env (S ₛ)))
        | sym (Env.←-assoc (θ₁ ← θ₂) θo ([S]-env (S ₛ)))
        | canθ-new-irr sigs (suc S) θ₁ θ₂ (θo ← [S]-env (S ₛ)) q cbq
            (canθ-new-irr-S-prop-accumulate S Signal.unknown θo S-prop)
  = ⊥-elim
      (S∉canθ-sigs-q-θ₁←θ₂←θo←[S]
        S∈canθ-sigs-q-θ₁←θo←[S])
... | no  S∉canθ-sigs-q-θ₁←θo←[S] | yes S∈canθ-sigs-q-θ₁←θ₂←θo←[S]
  rewrite sym (Env.←-assoc θ₁ θo ([S]-env (S ₛ)))
        | sym (Env.←-assoc (θ₁ ← θ₂) θo ([S]-env (S ₛ)))
        | canθ-new-irr sigs (suc S) θ₁ θ₂ (θo ← [S]-env (S ₛ)) q cbq
            (canθ-new-irr-S-prop-accumulate S Signal.unknown θo S-prop)
  = ⊥-elim
      (S∉canθ-sigs-q-θ₁←θo←[S]
        S∈canθ-sigs-q-θ₁←θ₂←θo←[S])

can-irr : ∀ {BV} {FV} θ₁ θ₂ q →
  CorrectBinding q BV FV →
  (distinct' (proj₁ FV) (proj₁ (Dom θ₂))) →
  Can q θ₁ ≡ Can q (θ₁ ← θ₂)
can-irr θ₁ θ₂ q cbq FV≠Domθ₂
  with can-new-irr θ₁ θ₂ Env.[]env q cbq (λ S' S'∈FV → inj₁ (FV≠Domθ₂ S' S'∈FV))
... | eq rewrite cong (Can q) (Env.←-comm Env.[]env θ₁ distinct-empty-left)
               | cong (Can q) (Env.←-comm Env.[]env (θ₁ ← θ₂) distinct-empty-left)
         = eq

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
------------------------------------------------------------------------
-- Properties related to Fin, and operations making use of these
-- properties (or other properties not available in Data.Fin)
------------------------------------------------------------------------

module Data.Fin.Props where

open import Data.Fin
open import Data.Nat as N
  using (ℕ; zero; suc; s≤s; z≤n)
  renaming (_≤_ to _ℕ≤_; _<_ to _ℕ<_; _+_ to _ℕ+_)
open N.≤-Reasoning
import Data.Nat.Properties as N
open import Data.Function
open import Relation.Nullary
open import Relation.Unary
open import Relation.Binary
open import Relation.Binary.FunctionSetoid
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; cong; subst)
open import Category.Functor
open import Category.Applicative

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

private
  drop-suc : ∀ {o} {m n : Fin o} →
             suc m ≡ (Fin (suc o) ∶ suc n) → m ≡ n
  drop-suc refl = refl

preorder : ℕ → Preorder
preorder n = PropEq.preorder (Fin n)

setoid : ℕ → Setoid
setoid n = PropEq.setoid (Fin n)

strictTotalOrder : ℕ → StrictTotalOrder
strictTotalOrder n = record
  { carrier            = Fin n
  ; _≈_                = _≡_
  ; _<_                = _<_
  ; isStrictTotalOrder = record
    { isEquivalence = PropEq.isEquivalence
    ; trans         = N.<-trans
    ; compare       = cmp
    ; <-resp-≈      = PropEq.resp₂ _<_
    }
  }
  where
  cmp : ∀ {n} → Trichotomous _≡_ (_<_ {n})
  cmp zero    zero    = tri≈ (λ())     refl  (λ())
  cmp zero    (suc j) = tri< (s≤s z≤n) (λ()) (λ())
  cmp (suc i) zero    = tri> (λ())     (λ()) (s≤s z≤n)
  cmp (suc i) (suc j) with cmp i j
  ... | tri<  lt ¬eq ¬gt = tri< (s≤s lt)         (¬eq ∘ drop-suc) (¬gt ∘ N.≤-pred)
  ... | tri> ¬lt ¬eq  gt = tri> (¬lt ∘ N.≤-pred) (¬eq ∘ drop-suc) (s≤s gt)
  ... | tri≈ ¬lt  eq ¬gt = tri≈ (¬lt ∘ N.≤-pred) (cong suc eq)    (¬gt ∘ N.≤-pred)

decSetoid : ℕ → DecSetoid
decSetoid n = StrictTotalOrder.decSetoid (strictTotalOrder n)

infix 4 _≟_

_≟_ : {n : ℕ} → Decidable {Fin n} _≡_
_≟_ {n} = DecSetoid._≟_ (decSetoid n)

to-from : ∀ n → toℕ (fromℕ n) ≡ n
to-from zero    = refl
to-from (suc n) = cong suc (to-from n)

bounded : ∀ {n} (i : Fin n) → toℕ i ℕ< n
bounded zero    = s≤s z≤n
bounded (suc i) = s≤s (bounded i)

prop-toℕ-≤ : ∀ {n} (x : Fin n) → toℕ x ℕ≤ N.pred n
prop-toℕ-≤ zero                 = z≤n
prop-toℕ-≤ (suc {n = zero}  ())
prop-toℕ-≤ (suc {n = suc n} i)  = s≤s (prop-toℕ-≤ i)

nℕ-ℕi≤n : ∀ n i → n ℕ-ℕ i ℕ≤ n
nℕ-ℕi≤n n       zero     = begin n ∎
nℕ-ℕi≤n zero    (suc ())
nℕ-ℕi≤n (suc n) (suc i)  = begin
  n ℕ-ℕ i ≤⟨ nℕ-ℕi≤n n i ⟩
  n       ≤⟨ N.n≤1+n n ⟩
  suc n   ∎

inject-lemma : ∀ {n} {i : Fin n} (j : Fin′ i) →
               toℕ (inject j) ≡ toℕ j
inject-lemma {i = zero}  ()
inject-lemma {i = suc i} zero    = refl
inject-lemma {i = suc i} (suc j) = cong suc (inject-lemma j)

inject+-lemma : ∀ m k → m ≡ toℕ (inject+ k (fromℕ m))
inject+-lemma zero    k = refl
inject+-lemma (suc m) k = cong suc (inject+-lemma m k)

inject₁-lemma : ∀ {m} (i : Fin m) → toℕ (inject₁ i) ≡ toℕ i
inject₁-lemma zero    = refl
inject₁-lemma (suc i) = cong suc (inject₁-lemma i)

inject≤-lemma : ∀ {m n} (i : Fin m) (le : m ℕ≤ n) →
                toℕ (inject≤ i le) ≡ toℕ i
inject≤-lemma zero    (N.s≤s le) = refl
inject≤-lemma (suc i) (N.s≤s le) = cong suc (inject≤-lemma i le)

≺⇒<′ : _≺_ ⇒ N._<′_
≺⇒<′ (n ≻toℕ i) = N.≤⇒≤′ (bounded i)

<′⇒≺ : N._<′_ ⇒ _≺_
<′⇒≺ {n} N.≤′-refl    = subst (λ i → i ≺ suc n) (to-from n)
                              (suc n ≻toℕ fromℕ n)
<′⇒≺ (N.≤′-step m≤′n) with <′⇒≺ m≤′n
<′⇒≺ (N.≤′-step m≤′n) | n ≻toℕ i =
  subst (λ i → i ≺ suc n) (inject₁-lemma i) (suc n ≻toℕ (inject₁ i))

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

infixl 6 _+′_

_+′_ : ∀ {m n} (i : Fin m) (j : Fin n) → Fin (N.pred m ℕ+ n)
i +′ j = inject≤ (i + j) (N._+-mono_ (prop-toℕ-≤ i) ≤-refl)
  where open Poset N.poset renaming (refl to ≤-refl)

-- reverse {n} "i" = "n ∸ 1 ∸ i".

reverse : ∀ {n} → Fin n → Fin n
reverse {zero}  ()
reverse {suc n} i  = inject≤ (n ℕ- i) (N.n∸m≤n (toℕ i) (suc n))

-- If there is an injection from a set to a finite set, then equality
-- of the set can be decided.

eq? : ∀ {S n} →
      Injection S (PropEq.setoid (Fin n)) → Decidable (Setoid._≈_ S)
eq? inj x y with to ⟨$⟩ x ≟ to ⟨$⟩ y where open Injection inj
... | yes tox≡toy = yes (Injection.injective inj tox≡toy)
... | no  tox≢toy = no  (tox≢toy ∘ pres (Injection.to inj))

-- Quantification over finite sets commutes with applicative functors.

sequence : ∀ {F n} {P : Pred (Fin n)} → RawApplicative F →
           (∀ i → F (P i)) → F (∀ i → P i)
sequence {F} RA = helper _ _
  where
  open RawApplicative RA

  helper : ∀ n (P : Pred (Fin n)) → (∀ i → F (P i)) → F (∀ i → P i)
  helper zero    P ∀iPi = pure (λ())
  helper (suc n) P ∀iPi =
    combine <$> ∀iPi zero ⊛ helper n (λ n → P (suc n)) (∀iPi ∘ suc)
    where
    combine : P zero → (∀ i → P (suc i)) → ∀ i → P i
    combine z s zero    = z
    combine z s (suc i) = s i

private

  -- Included just to show that sequence above has an inverse (under
  -- an equivalence relation with two equivalence classes, one with
  -- all inhabited sets and the other with all uninhabited sets).

  sequence⁻¹ : ∀ {F A} {P : Pred A} → RawFunctor F →
               F (∀ i → P i) → ∀ i → F (P i)
  sequence⁻¹ RF F∀iPi i = (λ f → f i) <$> F∀iPi
    where open RawFunctor RF

max_issues_repo_name: larrytheliquid/Lemmachine


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Limits where

open import Cubical.Categories.Limits.Limits public
open import Cubical.Categories.Limits.BinProduct public
open import Cubical.Categories.Limits.BinCoproduct public
open import Cubical.Categories.Limits.Initial public
open import Cubical.Categories.Limits.Terminal public
open import Cubical.Categories.Limits.Pullback public

max_stars_repo_name: FernandoLarrain/cubical


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

module FOT.FOTC.Program.Mirror.StructurallySmaller.StructurallySmaller where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Program.Mirror.Type

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

{-# TERMINATING #-}
foo : ∀ {ts} → Tree ts → D
foo (tree d fnil)           = d
foo (tree d (fcons Tt Fts)) = foo (tree d Fts)

{-# TERMINATING #-}
bar : ∀ {ts} → Tree ts → D
bar (tree d fnil)           = d
bar (tree d (fcons Tt Fts)) = helper (bar Tt) (bar (tree d Fts))
  where
  postulate helper : D → D → D

{-# TERMINATING #-}
bar₁ : ∀ ts → Tree ts → D
bar₁ .(node d []) (tree d fnil) = d
bar₁ .(node d (t ∷ ts)) (tree d (fcons {t} {ts} Tt Fts))
  = helper (bar₁ t Tt) (bar₁ (node d ts) (tree d Fts))
  where
  postulate helper : D → D → D

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Oscar.Prelude
open import Oscar.Data.¶

module Oscar.Data.Descender where

-- m ≤ n, counting down from n-1 to m
data Descender⟨_⟩ {a} (A : ¶ → Ø a) (m : ¶) : ¶ → Ø a where
  ∅ : Descender⟨ A ⟩ m m
  _,_ : ∀ {n} → A n → Descender⟨ A ⟩ m n → Descender⟨ A ⟩ m (↑ n)

Vec'⟨_⟩ = λ {a} (A : Ø a) N → Descender⟨ (λ _ → A) ⟩ 0 N
⟨_⟩¶⟨_≤_↓⟩ = Descender⟨_⟩
AList⟨_⟩ = ⟨_⟩¶⟨_≤_↓⟩


text:
module Ferros.Resource.Untyped where

open import Ferros.Resource.Untyped.Base public

max_stars_repo_name: auxoncorp/ferros-spec

max_issues_repo_name: auxoncorp/ferros-spec

max_forks_repo_name: auxoncorp/ferros-spec


text:
module Selective.Simulate where

open import Selective.ActorMonad public
open import Selective.SimulationEnvironment
open import Selective.EnvironmentOperations
open import Prelude

open import Data.List.All.Properties using (++⁺)
open import Data.Nat.Properties using (≤-reflexive ; ≤-step)
open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax)

open Actor
open ValidActor
open Env
open FoundReference
open LiftedReferences
open UpdatedInbox
open ValidMessageList
open NamedInbox
open _comp↦_∈_
open NameSupply
open NameSupplyStream

data Trace (i : Size) : Set₂

record ∞Trace (i : Size) : Set₂ where
  coinductive
  constructor delay_
  field force : {j : Size< i} → Trace j

data Trace (i : Size) where
  TraceStop : (env : Env) → Done env → Trace i
  _∷_ : (x : Env) (xs : ∞Trace i) → Trace i

reduce-unbound-return : {act : Actor} → (env : Env) → Focus act env →
                        ActorAtConstructor Return act →
                        ActorHasNoContinuation act →
                        Env
reduce-unbound-return env Focused AtReturn no-cont = block-focused env Focused (BlockedReturn AtReturn no-cont)

reduce-bound-return : {act : Actor} → (env : Env) → Focus act env →
                      ActorAtConstructor Return act →
                      ActorHasContinuation act →
                      Env
reduce-bound-return env@record {
  acts = actor@record { computation = Return v ⟶ (f ∷ cont) } ∷ rest
  ; actors-valid = actor-valid ∷ rest-valid
  } Focused AtReturn HasContinuation =
    let
      actor' : Actor
      actor' = replace-actorM actor ((f v .force) ⟶ cont)
      env' : Env
      env' = replace-focused
               env
               Focused
               actor'
               (rewrap-valid-actor AreSame actor-valid)
    in env'

reduce-bind : {act : Actor} → (env : Env) → Focus act env →
              ActorAtConstructor Bind act →
              Env
reduce-bind env@record { acts = actor@record { computation = (m ∞>>= f) ⟶ cont } ∷ rest ; actors-valid = actor-valid ∷ rest-valid } Focused AtBind =
  let
    actor' : Actor
    actor' = replace-actorM actor ((m .force) ⟶ (f ∷ cont))
    env' : Env
    env' = replace-focused
             env
             Focused
             actor'
             (rewrap-valid-actor AreSame actor-valid)
  in env'

reduce-spawn : {act : Actor} → (env : Env) → Focus act env →
               ActorAtConstructor Spawn act →
               Env
reduce-spawn env@record {
  acts = actor@record { computation = Spawn {NewIS} {B} act ⟶ cont } ∷ rest
  ; actors-valid = actor-valid ∷ rest-valid
  } Focused AtSpawn =
  let
    new-name : Name
    new-name = env .name-supply .supply .name
    new-store-entry : NamedInbox
    new-store-entry = inbox# new-name [ NewIS ]
    env' : Env
    env' = add-top (act ⟶ []) env
    valid' : ValidActor (env' .store) actor
    valid' = valid-actor-suc (env .name-supply .supply) actor-valid
    env'' : Env
    env'' = top-actor-to-back env'
    actor' : Actor
    actor' = add-reference actor new-store-entry (Return _ ⟶ cont)
    valid'' : ValidActor (env'' .store) actor'
    valid'' = add-reference-valid RefAdded valid' [p: zero ][handles: ⊆-refl ]
    env''' : Env
    env''' = replace-focused env'' Focused actor' valid''
  in env'''

reduce-send : {act : Actor} → (env : Env) → Focus act env →
              ActorAtConstructor Send act →
              Env
reduce-send env@record {
  acts = actor@record { computation = Send {ToIS = ToIS} canSendTo (SendM tag fields) ⟶ cont } ∷ rest
  ; actors-valid = actor-valid ∷ rest-valid
  } Focused AtSend =
  let
    to-reference : FoundReference (store env) ToIS
    to-reference = lookup-reference-act actor-valid canSendTo
    namedFields = name-fields-act (store env) actor fields actor-valid
    actor' : Actor
    actor' = replace-actorM actor (Return _ ⟶ cont)
    withM : Env
    withM = replace-focused
              env
              Focused
              actor'
              (rewrap-valid-actor AreSame actor-valid)
    message = NamedM
                (translate-message-pointer to-reference tag)
                namedFields
    message-is-valid : message-valid (env .store) message
    message-is-valid = make-pointers-compatible
                         (env .store)
                         (actor .pre)
                         (actor .references)
                         (actor .pre-eq-refs)
                         fields
                         (actor-valid .references-have-pointer)
    updater = add-message message message-is-valid
    withUpdatedInbox : Env
    withUpdatedInbox = update-inbox-env
                         withM
                         (underlying-pointer to-reference)
                         updater
  in withUpdatedInbox

reduce-receive-without-message : {act : Actor} → (env : Env) → Focus act env →
                              ActorAtConstructor Receive act →
                              (p : has-inbox (env .store) act) →
                              inbox-for-actor (env .env-inboxes) act p [] →
                              Env
reduce-receive-without-message env Focused AtReceive  p ifa = block-focused env Focused (BlockedReceive AtReceive p ifa)

reduce-receive-with-message : {act : Actor} → (env : Env) → Focus act env →
                              ActorAtConstructor Receive act →
                              (p : has-inbox (env .store) act) →
                              ∀ inbox →
                              all-messages-valid (env .store) inbox →
                              InboxInState NonEmpty inbox →
                              inbox-for-actor (env .env-inboxes) act p inbox →
                              Env
reduce-receive-with-message env@record {
  acts = actor@record { computation = (Receive ⟶ cont) } ∷ rest
  ; actors-valid = actor-valid ∷ rest-valid
  } Focused AtReceive p (nm ∷ messages) (nmv ∷ vms) HasMessage ifa =
  let
    inboxesAfter = update-inbox
                     (env .store)
                     (env .env-inboxes)
                     (env .messages-valid)
                     (actor-valid .actor-has-inbox)
                     remove-message
    actor' : Actor
    actor' = add-references-rewrite
               actor
               (named-inboxes nm)
               {unname-message nm}
               (add-references++
                 nm
                 nmv
                 (pre actor))
               (Return (unname-message nm) ⟶ cont)
    actor-valid' : ValidActor (env .store) actor'
    actor-valid' = record {
      actor-has-inbox = actor-valid .actor-has-inbox
      ; references-have-pointer = valid++ nm nmv (actor-valid .references-have-pointer)
      }
    env' : Env
    env' = let
      updated = update-inbox (env .store) (env .env-inboxes) (env .messages-valid) (actor-valid .actor-has-inbox) remove-message
      unblock-split = unblock-actors updated (env .blocked) (env .blocked-valid) (env .blocked-no-progress)
      open UnblockedActors
        in record
             { acts = actor' ∷ unblock-split .unblocked ++ rest
             ; blocked = unblock-split .still-blocked
             ; store = env .store
             ; env-inboxes = updated .updated-inboxes
             ; name-supply = env .name-supply
             ; actors-valid = actor-valid' ∷ ++⁺ (unblock-split .unblocked-valid) rest-valid
             ; blocked-valid = unblock-split .blocked-valid
             ; messages-valid = updated .inboxes-valid
             ; blocked-no-progress = unblock-split .blocked-no-prog
             }
  in env'

reduce-receive : {act : Actor} → (env : Env) → Focus act env →
                 ActorAtConstructor Receive act →
                 Env
reduce-receive env@record { acts = actor ∷ rest ; actors-valid = actor-valid ∷ _ } Focused AtReceive = choose-reduction (get-inbox env (actor-valid .actor-has-inbox))
  where
    open GetInbox
    choose-reduction : (gi : GetInbox (env .store) (env .env-inboxes) (actor-valid .actor-has-inbox)) → Env
    choose-reduction gi@record { messages = [] } =
      reduce-receive-without-message env Focused AtReceive _ (gi .right-inbox)
    choose-reduction gi@record { messages = _ ∷ _ } =
      reduce-receive-with-message env Focused AtReceive _ (gi .messages) (gi .valid) HasMessage (gi .right-inbox)

reduce-self : {act : Actor} → (env : Env) → Focus act env →
              ActorAtConstructor Self act →
              Env
reduce-self env@record { acts = actor@record {
  computation = Self ⟶ cont } ∷ _
  ; actors-valid = actor-valid ∷ _
  } Focused AtSelf =
  let
    actor' : Actor
    actor' = add-reference actor inbox# (actor .name) [ (actor .inbox-shape) ] ((Return _) ⟶ cont)
    actor-valid' : ValidActor (env .store) actor'
    actor-valid' = add-reference-valid RefAdded actor-valid [p: (actor-valid .actor-has-inbox) ][handles: ⊆-refl ]
    env' : Env
    env' = replace-focused
             env
             Focused
             actor'
             actor-valid'
  in env'

reduce-selective-with-message : {act : Actor} → (env : Env) → Focus act env →
                                (aac : ActorAtConstructor Selective act) →
                                (point : has-inbox (env .store) act) →
                                ∀ inbox →
                                all-messages-valid (env .store) inbox →
                                inbox-for-actor (env .env-inboxes) act point inbox →
                                {split : SplitList inbox} →
                                {p : (filter-named (selected-filter act aac)) (SplitList.el split) ≡ true} →
                                InboxInFilterState {filter = filter-named (selected-filter act aac)} inbox (Found split p) →
                                Env
reduce-selective-with-message env@record {
  acts = actor@record { computation = SelectiveReceive filter ⟶ cont } ∷ rest
  ; actors-valid = actor-valid ∷ rest-valid
  } Focused AtSelective point inb amv ifa (HasMessage split ok) =
  let updated = update-inbox (env .store) (env .env-inboxes) (env .messages-valid) (actor-valid .actor-has-inbox) (remove-found-message filter)
      unblock-split = unblock-actors updated (env .blocked) (env .blocked-valid) (env .blocked-no-progress)
      open SplitList
      received-nm = split .el
      added-references = named-inboxes received-nm
      received-message = unname-message received-nm
      received-valid : message-valid (env .store) received-nm
      received-valid = split-all-el inb amv split
      adds-correct-references : map shape added-references ++ (actor .pre) ≡ add-references (actor .pre) received-message
      adds-correct-references = add-references++ received-nm received-valid (actor .pre)
      new-continuation = Return sm: received-message [ ok ] ⟶ cont
      act' : Actor
      act' = add-references-rewrite actor added-references {received-message} adds-correct-references new-continuation
      act-valid' : ValidActor (env .store) act'
      act-valid' = record {
        actor-has-inbox = actor-valid .actor-has-inbox
        ; references-have-pointer = valid++ received-nm received-valid (actor-valid .references-have-pointer)
        }
      open UnblockedActors
  in record
       { acts = act' ∷ unblock-split .unblocked ++ rest
       ; blocked = unblock-split .still-blocked
       ; store = env .store
       ; env-inboxes = updated-inboxes updated
       ; name-supply = env .name-supply
       ; actors-valid = act-valid' ∷ ++⁺ (unblock-split .unblocked-valid) rest-valid
       ; blocked-valid = unblock-split .blocked-valid
       ; messages-valid = inboxes-valid updated
       ; blocked-no-progress = unblock-split .blocked-no-prog
       }

reduce-selective-without-message : {act : Actor} → (env : Env) → Focus act env →
                                 (aac : ActorAtConstructor Selective act) →
                                 (point : has-inbox (env .store) act) →
                                 ∀ inbox →
                                 {ps : All (misses-filter (filter-named (selected-filter act aac))) inbox} →
                                 inbox-for-actor (env .env-inboxes) act point inbox →
                                 InboxInFilterState inbox (Nothing ps) →
                                 Env
reduce-selective-without-message env Focused AtSelective point inbox ifa iifs =
  block-focused env Focused (BlockedSelective AtSelective point inbox ifa iifs)

reduce-selective : {act : Actor} → (env : Env) → Focus act env →
                 ActorAtConstructor Selective act →
                 Env
reduce-selective env@record {
  acts = actor@record { computation = SelectiveReceive filter ⟶ _  } ∷ _
  ; actors-valid = actor-valid ∷ _
  } Focused AtSelective =
  let inb = get-inbox env (actor-valid .actor-has-inbox)
  in choose-reduction inb (find-split (inb .messages) (filter-named filter))
  where
    open GetInbox
    choose-reduction : (gi : GetInbox (env .store) (env .env-inboxes) (actor-valid .actor-has-inbox)) → FoundInList (gi .messages) (filter-named filter) → Env
    choose-reduction gi (Found split x) = reduce-selective-with-message env Focused AtSelective _ (gi .messages) (gi .valid) (gi .right-inbox) (HasMessage split x)
    choose-reduction gi (Nothing ps) = reduce-selective-without-message env Focused AtSelective _ (gi .messages) (gi .right-inbox) (IsEmpty ps)

reduce-strengthen : {act : Actor} → (env : Env) → Focus act env →
                    ActorAtConstructor Strengthen act →
                    Env
reduce-strengthen env@record {
  acts = actor@record { computation = Strengthen {ys} inc ⟶ cont } ∷ _
  ; actors-valid = actor-valid ∷ _
  } Focused AtStrengthen =
  let
    lifted-references = lift-references inc (references actor) (pre-eq-refs actor)
    actor' : Actor
    actor' = lift-actor actor (lifted-references .contained) (lifted-references .contained-eq-inboxes) (Return _ ⟶ cont)
    actor-valid' : ValidActor (env .store) actor'
    actor-valid' = lift-valid-actor (CanBeLifted lifted-references) actor-valid
    env' : Env
    env' = replace-focused
             env
             Focused
             actor'
             actor-valid'
  in env'

reduce : {act : Actor} → (env : Env) → Focus act env → Env
reduce env@record { acts = record { computation = (Return val ⟶ []) } ∷ _ } Focused =
  reduce-unbound-return env Focused AtReturn (NoContinuation {v = val})
reduce env@record { acts = record { computation = (Return val ⟶ (_ ∷ _)) } ∷ _ } Focused =
  reduce-bound-return env Focused AtReturn (HasContinuation {v = val})
reduce env@record { acts = record { computation = ((m ∞>>= f) ⟶ _)} ∷ _ } Focused =
  reduce-bind env Focused AtBind
reduce env@record { acts = record { computation = (Spawn act ⟶ cont) } ∷ _ } Focused =
  reduce-spawn env Focused AtSpawn
reduce env@record { acts = record { computation = (Send canSendTo msg ⟶ cont) } ∷ _ } Focused =
  reduce-send env Focused AtSend
reduce env@record { acts = record { computation = (Receive ⟶ cont) } ∷ _ } Focused =
  reduce-receive env Focused AtReceive
reduce env@record { acts = record { computation = (SelectiveReceive filter ⟶ cont) } ∷ _ } Focused =
  reduce-selective env Focused AtSelective
reduce env@record { acts = record { computation = (Self ⟶ cont) } ∷ _ } Focused =
  reduce-self env Focused AtSelf
reduce env@record { acts = record { computation = (Strengthen inc ⟶ cont) } ∷ _ } Focused =
  reduce-strengthen env Focused AtStrengthen

simulate : Env → ∞Trace ∞
simulate env@record { acts = [] ; actors-valid = [] } = delay TraceStop env AllBlocked
simulate env@record { acts = _ ∷ _ ; actors-valid = _ ∷ _ } = keep-stepping (reduce env Focused)
  where
    open ∞Trace
    keep-stepping : Env → ∞Trace ∞
    keep-stepping env .force = env ∷ simulate env

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
module Oscar.Data.Vec.Core where

open import Data.Vec public using (Vec; []; _∷_)


text:
module OlderBasicILP.Indirect.Gentzen where

open import OlderBasicILP.Indirect public

-- Derivations, as Gentzen-style natural deduction trees.

mutual
  data Tm : Set where
    VAR      : ℕ → Tm
    LAM      : Tm → Tm
    APP      : Tm → Tm → Tm
    MULTIBOX : Cx Tm → Tm → Tm
    DOWN     : Tm → Tm
    PAIR     : Tm → Tm → Tm
    FST      : Tm → Tm
    SND      : Tm → Tm
    UNIT     : Tm

  infix 3 _⊢_
  data _⊢_ (Γ : Cx (Ty Tm)) : Ty Tm → Set where
    var      : ∀ {A}   → A ∈ Γ → Γ ⊢ A
    lam      : ∀ {A B} → Γ , A ⊢ B → Γ ⊢ A ▻ B
    app      : ∀ {A B} → Γ ⊢ A ▻ B → Γ ⊢ A → Γ ⊢ B
    multibox : ∀ {n A} {SS : VCx Tm n} {Ξ : VCx (Ty Tm) n}
               → Γ ⊢⋆ SS ⦂⋆ Ξ → (u : SS ⦂⋆ Ξ ⊢ A)
               → Γ ⊢ [ u ] ⦂ A
    down     : ∀ {A T} → Γ ⊢ T ⦂ A → Γ ⊢ A
    pair     : ∀ {A B} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧ B
    fst      : ∀ {A B} → Γ ⊢ A ∧ B → Γ ⊢ A
    snd      : ∀ {A B} → Γ ⊢ A ∧ B → Γ ⊢ B
    unit     : Γ ⊢ ⊤

  infix 3 _⊢⋆_
  _⊢⋆_ : Cx (Ty Tm) → Cx (Ty Tm) → Set
  Γ ⊢⋆ ∅     = 𝟙
  Γ ⊢⋆ Ξ , A = Γ ⊢⋆ Ξ × Γ ⊢ A

  [_] : ∀ {A Γ} → Γ ⊢ A → Tm
  [ var i ]         = VAR [ i ]ⁱ
  [ lam t ]         = LAM [ t ]
  [ app t u ]       = APP [ t ] [ u ]
  [ multibox ts u ] = MULTIBOX [ ts ]⋆ [ u ]
  [ down t ]        = DOWN [ t ]
  [ pair t u ]      = PAIR [ t ] [ u ]
  [ fst t ]         = FST [ t ]
  [ snd t ]         = SND [ t ]
  [ unit ]          = UNIT

  [_]⋆ : ∀ {Ξ Γ} → Γ ⊢⋆ Ξ → Cx Tm
  [_]⋆ {∅}     ∙        = ∅
  [_]⋆ {Ξ , A} (ts , t) = [ ts ]⋆ , [ t ]

-- Monotonicity with respect to context inclusion.

mutual
  mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
  mono⊢ η (var i)         = var (mono∈ η i)
  mono⊢ η (lam t)         = lam (mono⊢ (keep η) t)
  mono⊢ η (app t u)       = app (mono⊢ η t) (mono⊢ η u)
  mono⊢ η (multibox ts u) = multibox (mono⊢⋆ η ts) u
  mono⊢ η (down t)        = down (mono⊢ η t)
  mono⊢ η (pair t u)      = pair (mono⊢ η t) (mono⊢ η u)
  mono⊢ η (fst t)         = fst (mono⊢ η t)
  mono⊢ η (snd t)         = snd (mono⊢ η t)
  mono⊢ η unit            = unit

  mono⊢⋆ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ Ξ → Γ′ ⊢⋆ Ξ
  mono⊢⋆ {∅}     η ∙        = ∙
  mono⊢⋆ {Ξ , A} η (ts , t) = mono⊢⋆ η ts , mono⊢ η t

-- Shorthand for variables.

V₀ : Tm
V₀ = VAR 0

V₁ : Tm
V₁ = VAR 1

V₂ : Tm
V₂ = VAR 2

v₀ : ∀ {A Γ} → Γ , A ⊢ A
v₀ = var i₀

v₁ : ∀ {A B Γ} → (Γ , A) , B ⊢ A
v₁ = var i₁

v₂ : ∀ {A B C Γ} → ((Γ , A) , B) , C ⊢ A
v₂ = var i₂

-- Reflexivity.

refl⊢⋆ : ∀ {Γ} → Γ ⊢⋆ Γ
refl⊢⋆ {∅}     = ∙
refl⊢⋆ {Γ , A} = mono⊢⋆ weak⊆ refl⊢⋆ , v₀

-- Deduction theorem is built-in.

-- Detachment theorem.

DET : Tm → Tm
DET T = APP T V₀

det : ∀ {A B Γ} → Γ ⊢ A ▻ B → Γ , A ⊢ B
det t = app (mono⊢ weak⊆ t) v₀

-- Cut and multicut.

CUT : Tm → Tm → Tm
CUT T U = APP (LAM U) T

MULTICUT : Cx Tm → Tm → Tm
MULTICUT ∅        U = U
MULTICUT (TS , T) U = APP (MULTICUT TS (LAM U)) T

cut : ∀ {A B Γ} → Γ ⊢ A → Γ , A ⊢ B → Γ ⊢ B
cut t u = app (lam u) t

multicut : ∀ {Ξ A Γ} → Γ ⊢⋆ Ξ → Ξ ⊢ A → Γ ⊢ A
multicut {∅}     ∙        u = mono⊢ bot⊆ u
multicut {Ξ , B} (ts , t) u = app (multicut ts (lam u)) t

-- Transitivity.

trans⊢⋆ : ∀ {Γ″ Γ′ Γ} → Γ ⊢⋆ Γ′ → Γ′ ⊢⋆ Γ″ → Γ ⊢⋆ Γ″
trans⊢⋆ {∅}      ts ∙        = ∙
trans⊢⋆ {Γ″ , A} ts (us , u) = trans⊢⋆ ts us , multicut ts u

-- Contraction.

CCONT : Tm
CCONT = LAM (LAM (APP (APP V₁ V₀) V₀))

CONT : Tm → Tm
CONT T = DET (APP CCONT (LAM (LAM T)))

ccont : ∀ {A B Γ} → Γ ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = lam (lam (app (app v₁ v₀) v₀))

cont : ∀ {A B Γ} → Γ , A , A ⊢ B → Γ , A ⊢ B
cont t = det (app ccont (lam (lam t)))

-- Exchange, or Schönfinkel’s C combinator.

CEXCH : Tm
CEXCH = LAM (LAM (LAM (APP (APP V₂ V₀) V₁)))

EXCH : Tm → Tm
EXCH T = DET (DET (APP CEXCH (LAM (LAM T))))

cexch : ∀ {A B C Γ} → Γ ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = lam (lam (lam (app (app v₂ v₀) v₁)))

exch : ∀ {A B C Γ} → Γ , A , B ⊢ C → Γ , B , A ⊢ C
exch t = det (det (app cexch (lam (lam t))))

-- Composition, or Schönfinkel’s B combinator.

CCOMP : Tm
CCOMP = LAM (LAM (LAM (APP V₂ (APP V₁ V₀))))

COMP : Tm → Tm → Tm
COMP T U = DET (APP (APP CCOMP (LAM T)) (LAM U))

ccomp : ∀ {A B C Γ} → Γ ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = lam (lam (lam (app v₂ (app v₁ v₀))))

comp : ∀ {A B C Γ} → Γ , B ⊢ C → Γ , A ⊢ B → Γ , A ⊢ C
comp t u = det (app (app ccomp (lam t)) (lam u))

-- Useful theorems in functional form.

DIST : Tm → Tm → Tm
DIST T U = MULTIBOX ((∅ , T) , U) (APP (DOWN V₁) (DOWN V₀))

UP : Tm → Tm
UP T = MULTIBOX (∅ , T) V₀

DISTUP : Tm → Tm → Tm
DISTUP T U = DIST T (UP U)

BOX : Tm → Tm
BOX T = MULTIBOX ∅ T

UNBOX : Tm → Tm → Tm
UNBOX T U = APP (LAM U) T

dist : ∀ {A B T U Γ}
       → (t : Γ ⊢ T ⦂ (A ▻ B)) → (u : Γ ⊢ U ⦂ A)
       → Γ ⊢ APP (DOWN V₁) (DOWN V₀) ⦂ B
dist t u = multibox ((∙ , t) , u) (app (down v₁) (down v₀))

up : ∀ {A T Γ}
     → Γ ⊢ T ⦂ A
     → Γ ⊢ V₀ ⦂ T ⦂ A
up t = multibox (∙ , t) v₀

distup : ∀ {A B T U Γ}
         → (t : Γ ⊢ T ⦂ (U ⦂ A ▻ B)) → (u : Γ ⊢ U ⦂ A)
         → Γ ⊢ APP (DOWN V₁) (DOWN V₀) ⦂ B
distup t u = dist t (up u)

box : ∀ {A Γ}
      → (t : ∅ ⊢ A)
      → Γ ⊢ [ t ] ⦂ A
box t = multibox ∙ t

unbox : ∀ {A C T U Γ}
        → Γ ⊢ T ⦂ A → Γ , T ⦂ A ⊢ U ⦂ C
        → Γ ⊢ U ⦂ C
unbox t u = app (lam u) t

-- Useful theorems in combinatory form.

CI : Tm
CI = LAM V₀

CK : Tm
CK = LAM (LAM V₁)

CS : Tm
CS = LAM (LAM (LAM (APP (APP V₂ V₀) (APP V₁ V₀))))

CDIST : Tm
CDIST = LAM (LAM (DIST V₁ V₀))

CUP : Tm
CUP = LAM (UP V₀)

CDOWN : Tm
CDOWN = LAM (DOWN V₀)

CDISTUP : Tm
CDISTUP = LAM (LAM (DIST V₁ (UP V₀)))

CUNBOX : Tm
CUNBOX = LAM (LAM (APP V₀ V₁))

CPAIR : Tm
CPAIR = LAM (LAM (PAIR V₁ V₀))

CFST : Tm
CFST = LAM (FST V₀)

CSND : Tm
CSND = LAM (SND V₀)

ci : ∀ {A Γ} → Γ ⊢ A ▻ A
ci = lam v₀

ck : ∀ {A B Γ} → Γ ⊢ A ▻ B ▻ A
ck = lam (lam v₁)

cs : ∀ {A B C Γ} → Γ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
cs = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

cdist : ∀ {A B T U Γ}
        → Γ ⊢ T ⦂ (A ▻ B) ▻ U ⦂ A ▻ APP (DOWN V₁) (DOWN V₀) ⦂ B
cdist = lam (lam (dist v₁ v₀))

cup : ∀ {A T Γ} → Γ ⊢ T ⦂ A ▻ V₀ ⦂ T ⦂ A
cup = lam (up v₀)

cdown : ∀ {A T Γ} → Γ ⊢ T ⦂ A ▻ A
cdown = lam (down v₀)

cdistup : ∀ {A B T U Γ}
          → Γ ⊢ T ⦂ (U ⦂ A ▻ B) ▻ U ⦂ A ▻ APP (DOWN V₁) (DOWN V₀) ⦂ B
cdistup = lam (lam (dist v₁ (up v₀)))

cunbox : ∀ {A C T Γ} → Γ ⊢ T ⦂ A ▻ (T ⦂ A ▻ C) ▻ C
cunbox = lam (lam (app v₀ v₁))

cpair : ∀ {A B Γ} → Γ ⊢ A ▻ B ▻ A ∧ B
cpair = lam (lam (pair v₁ v₀))

cfst : ∀ {A B Γ} → Γ ⊢ A ∧ B ▻ A
cfst = lam (fst v₀)

csnd : ∀ {A B Γ} → Γ ⊢ A ∧ B ▻ B
csnd = lam (snd v₀)

-- Closure under context concatenation.

concat : ∀ {A B Γ} Γ′ → Γ , A ⊢ B → Γ′ ⊢ A → Γ ⧺ Γ′ ⊢ B
concat Γ′ t u = app (mono⊢ (weak⊆⧺₁ Γ′) (lam t)) (mono⊢ weak⊆⧺₂ u)

-- Substitution.

mutual
  [_≔_]_ : ∀ {A B Γ} → (i : A ∈ Γ) → Γ ∖ i ⊢ A → Γ ⊢ B → Γ ∖ i ⊢ B
  [ i ≔ s ] var j         with i ≟∈ j
  [ i ≔ s ] var .i        | same   = s
  [ i ≔ s ] var ._        | diff j = var j
  [ i ≔ s ] lam t         = lam ([ pop i ≔ mono⊢ weak⊆ s ] t)
  [ i ≔ s ] app t u       = app ([ i ≔ s ] t) ([ i ≔ s ] u)
  [ i ≔ s ] multibox ts u = multibox ([ i ≔ s ]⋆ ts) u
  [ i ≔ s ] down t        = down ([ i ≔ s ] t)
  [ i ≔ s ] pair t u      = pair ([ i ≔ s ] t) ([ i ≔ s ] u)
  [ i ≔ s ] fst t         = fst ([ i ≔ s ] t)
  [ i ≔ s ] snd t         = snd ([ i ≔ s ] t)
  [ i ≔ s ] unit          = unit

  [_≔_]⋆_ : ∀ {Ξ A Γ} → (i : A ∈ Γ) → Γ ∖ i ⊢ A → Γ ⊢⋆ Ξ → Γ ∖ i ⊢⋆ Ξ
  [_≔_]⋆_ {∅}     i s ∙        = ∙
  [_≔_]⋆_ {Ξ , B} i s (ts , t) = [ i ≔ s ]⋆ ts , [ i ≔ s ] t

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module Luau.Type.ToString where

open import FFI.Data.String using (String; _++_)
open import Luau.Type using (Type; nil; _⇒_; none; any; number; _∪_; _∩_; normalizeOptional)

{-# TERMINATING #-}
typeToString : Type → String
typeToStringᵁ : Type → String
typeToStringᴵ : Type → String

typeToString nil = "nil"
typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
typeToString none = "none"
typeToString any = "any"
typeToString number = "number"
typeToString (S ∪ T) with normalizeOptional(S ∪ T)
typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?"
typeToString (S ∪ T) | (S′ ∪ nil) = typeToString S′ ++ "?"
typeToString (S ∪ T) | (S′ ∪ T′) = "(" ++ typeToStringᵁ (S ∪ T) ++ ")"
typeToString (S ∪ T) | T′ = typeToString T′
typeToString (S ∩ T) = "(" ++ typeToStringᴵ (S ∩ T) ++ ")"

typeToStringᵁ (S ∪ T) = (typeToStringᵁ S) ++ " | " ++ (typeToStringᵁ T)
typeToStringᵁ T = typeToString T

typeToStringᴵ (S ∩ T) = (typeToStringᴵ S) ++ " & " ++ (typeToStringᴵ T)
typeToStringᴵ T = typeToString T


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

module fin where

open import Data.Fin hiding (_<_ ; _≤_ )
open import Data.Fin.Properties hiding ( <-trans )
open import Data.Nat
open import logic
open import nat
open import Relation.Binary.PropositionalEquality

-- toℕ<n
fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
fin<n {_} {zero} = s≤s z≤n
fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})

-- toℕ≤n
fin≤n : {n : ℕ} (f : Fin (suc n)) → toℕ f ≤ n
fin≤n {_} zero = z≤n
fin≤n {suc n} (suc f) = s≤s (fin≤n {n} f)

pred<n : {n : ℕ} {f : Fin (suc n)} → n > 0  → Data.Nat.pred (toℕ f) < n
pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n
pred<n {suc n} {suc f} (s≤s z≤n) = fin<n

fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n
fin<asa = toℕ-fromℕ< nat.a<sa

-- fromℕ<-toℕ
toℕ→from : {n : ℕ} {x : Fin (suc n)} → toℕ x ≡ n → fromℕ n ≡ x
toℕ→from {0} {zero} refl = refl
toℕ→from {suc n} {suc x} eq = cong (λ k → suc k ) ( toℕ→from {n} {x} (cong (λ k → Data.Nat.pred k ) eq ))

0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa
0≤fmax  = subst (λ k → 0 ≤ k ) (sym (toℕ-fromℕ< a<sa)) z≤n

0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa
0<fmax = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< a<sa)) (s≤s z≤n)

-- toℕ-injective
i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j
i=j {suc n} zero zero refl = refl
i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) )

-- raise 1
fin+1 :  { n : ℕ } → Fin n → Fin (suc n)
fin+1  zero = zero
fin+1  (suc x) = suc (fin+1 x)

open import Data.Nat.Properties as NatP  hiding ( _≟_ )

fin+1≤ : { i n : ℕ } → (a : i < n)  → fin+1 (fromℕ< a) ≡ fromℕ< (<-trans a a<sa)
fin+1≤ {0} {suc i} (s≤s z≤n) = refl
fin+1≤ {suc n} {suc (suc i)} (s≤s (s≤s a)) = cong (λ k → suc k ) ( fin+1≤ {n} {suc i} (s≤s a) )

fin+1-toℕ : { n : ℕ } → { x : Fin n} → toℕ (fin+1 x) ≡ toℕ x
fin+1-toℕ {suc n} {zero} = refl
fin+1-toℕ {suc n} {suc x} = cong (λ k → suc k ) (fin+1-toℕ {n} {x})

open import Relation.Nullary
open import Data.Empty

fin-1 :  { n : ℕ } → (x : Fin (suc n)) → ¬ (x ≡ zero )  → Fin n
fin-1 zero ne = ⊥-elim (ne refl )
fin-1 {n} (suc x) ne = x

fin-1-sx : { n : ℕ } → (x : Fin n) →  fin-1 (suc x) (λ ()) ≡ x
fin-1-sx zero = refl
fin-1-sx (suc x) = refl

fin-1-xs : { n : ℕ } → (x : Fin (suc n)) → (ne : ¬ (x ≡ zero ))  → suc (fin-1 x ne ) ≡ x
fin-1-xs zero ne = ⊥-elim ( ne refl )
fin-1-xs (suc x) ne = refl

-- suc-injective
-- suc-eq : {n : ℕ } {x y : Fin n} → Fin.suc x ≡ Fin.suc y  → x ≡ y
-- suc-eq {n} {x} {y} eq = subst₂ (λ j k → j ≡ k ) {!!} {!!} (cong (λ k → Data.Fin.pred k ) eq )

-- this is refl
lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
lemma3 (s≤s lt) = refl

-- fromℕ<-toℕ
lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ< n<m
lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl =  cong suc ( lemma12 {n} {m} n<m f refl  )

open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
open import Data.Fin.Properties

-- <-irrelevant
<-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
<-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
<-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl  )

lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )

-- fromℕ<-irrelevant
lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
lemma10 {n} refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl  ))

lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl)

-- toℕ-fromℕ<
lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
lemma11 {n} {m} {x} n<m  = begin
              toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
           ≡⟨ toℕ-fromℕ< _ ⟩
              toℕ x
           ∎  where
               open ≡-Reasoning

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


text:
module SingleSorted.Context where

-- An attempt to define more structured context
-- that directly support the cartesian structure

data Context : Set where
  ctx-empty : Context
  ctx-slot : Context
  ctx-concat : Context → Context → Context

-- the variables in a context
data var : Context → Set where
  var-var  : var ctx-slot
  var-inl  : ∀ {Γ Δ} → var Γ → var (ctx-concat Γ Δ)
  var-inr  : ∀ {Γ Δ} → var Δ → var (ctx-concat Γ Δ)

-- It is absurd to have a variable in the empty context
ctx-empty-absurd : ∀ {ℓ} {A : Set ℓ} → var ctx-empty → A
ctx-empty-absurd ()

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


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

module Data.PolyP.RecursionSchemes where

open import Function hiding (_⟨_⟩_)
open import Data.Sum
open import Data.Sigma
open import Level
open import Data.Unit
open import Data.Nat
open import Data.Vec.Iterated
open import Data.Empty
open import WellFounded
open import Literals.Number
open import Data.Fin.Indexed.Literals
open import Data.Fin.Indexed.Properties
open import Data.Fin.Indexed
open import Data.Nat.Literals
open import Data.Maybe
open import Path

open import Data.PolyP.Universe

---------------------------------------------------------------------------------
--
-- Helpers for Termination
--
---------------------------------------------------------------------------------

-- This is just the identity type. We need to use it because, if --without-K is
-- turned on, Agda will only use an argument to a function to prove structural
-- descent if that argument is a concrete data type.
--
--   wont-pass : (x : Bool) → (if x then ℕ else ℕ) → ℕ
--   wont-pass false zero    = zero
--   wont-pass false (suc n) = wont-pass true n
--   wont-pass true  zero    = zero
--   wont-pass true  (suc n) = wont-pass false n
--
-- Even though we're clearly structurally descending on the second argument
-- there, Agda won't use it unless we make it concrete, like so:
--
--   will-pass : (x : Bool) → <! (if x then ℕ else ℕ) !> → ℕ
--   will-pass false [! zero  !] = zero
--   will-pass false [! suc n !] = will-pass true  [! n !]
--   will-pass true  [! zero  !] = zero
--   will-pass true  [! suc n !] = will-pass false [! n !]
record <!_!> (A : Type) : Type  where
  eta-equality
  constructor [!_!]
  field !! : A
open <!_!>

-- For the map and cata functions to be structurally
-- terminating, we can't do things like:
--
--   cata f = f ∘ fmap (cata f) ∘ unwrap
--
-- So instead we need to carry a stack of all of the functors
-- we're under at any given point, and pattern match on that to
-- tell whether we should do f or fmap f.

data Layers (n : ℕ) : ℕ → Type₁ where
  []   : Layers n n
  _∷_  :  Functor (1 + m) →
          Layers n m →
          Layers n (1 + m)

_++∙_ : Layers n m → Params n → Params m
[]       ++∙ ys = ys
(x ∷ xs) ++∙ ys = let zs = xs ++∙ ys in μ x zs ∷ zs
infixr 5 _∷_ _++∙_

---------------------------------------------------------------------------------
--
-- Mapping
--
---------------------------------------------------------------------------------

module Mapping {m} {As Bs : Params m} (f : (i : Fin m) → As [ i ] → Bs [ i ]) where
  mapRec : ∀ (F : Functor n) (Fs : Layers m n) →
          <! ⟦ F ⟧ (Fs ++∙ As) !> → ⟦ F ⟧ (Fs ++∙ Bs)
  mapRec (F ⊕ G)    Fs       [! inl x  !] = inl (mapRec F Fs [! x !])
  mapRec (F ⊕ G)    Fs       [! inr x  !] = inr (mapRec G Fs [! x !])
  mapRec (F ⊗ G)    Fs       [! x , y  !] = mapRec F Fs [! x !] , mapRec G Fs [! y !]
  mapRec μ⟨ F ⟩     Fs       [! ⟨ xs ⟩ !] = ⟨ mapRec F (F ∷ Fs) [! xs !] ⟩
  mapRec (! i     ) []       [! xs     !] = f i xs
  mapRec (! f0    ) (F ∷ Fs) [! ⟨ xs ⟩ !] = ⟨ mapRec F (F ∷ Fs) [! xs !] ⟩
  mapRec (! (fs i)) (F ∷ Fs) [! xs     !] = mapRec (! i) Fs [! xs !]
  mapRec ①          Fs       _            = tt

mapParamAt : (i : Fin n) → (As [ i ] → A) → (j : Fin n) → As [ j ] → As [ i ]≔ A [ j ]
mapParamAt f0     f f0     x = f x
mapParamAt f0     f (fs _) x = x
mapParamAt (fs _) f f0     x = x
mapParamAt (fs i) f (fs j) x = mapParamAt i f j x

map : ∀ F → (i : Fin n) → (As [ i ] → A) → ⟦ F ⟧ As → ⟦ F ⟧ (As [ i ]≔ A)
map F i f xs = Mapping.mapRec (mapParamAt i f) F [] [! xs !]

module MapComp
    {m} {As Bs Cs : Params m}
    (f : (i : Fin m) → Bs [ i ] → Cs [ i ])
    (g : (i : Fin m) → As [ i ] → Bs [ i ])
  where
  open Mapping

  mapComp : ∀ (F : Functor n) (Fs : Layers m n) (xs : <! ⟦ F ⟧ (Fs ++∙ As) !>) →
            mapRec f F Fs [! mapRec g F Fs xs !] ≡ mapRec (λ i → f i ∘ g i) F Fs xs
  mapComp (F ⊕ G) Fs [! inl x !] = cong inl (mapComp F Fs [! x !])
  mapComp (F ⊕ G) Fs [! inr x !] = cong inr (mapComp G Fs [! x !])
  mapComp (F ⊗ G) Fs [! x , y !] = cong₂ _,_ (mapComp F Fs [! x !]) (mapComp G Fs [! y !])
  mapComp μ⟨ F ⟩  Fs [! ⟨ x ⟩ !] = cong ⟨_⟩ (mapComp F (F ∷ Fs) [! x !])
  mapComp (! i)      []       [! xs    !] = refl
  mapComp (! f0)     (F ∷ Fs) [! ⟨ x ⟩ !] = cong ⟨_⟩ (mapComp F (F ∷ Fs) [! x !])
  mapComp (! (fs i)) (F ∷ Fs) [! xs    !] = mapComp (! i) Fs [! xs !]
  mapComp ①      Fs xs = refl

map-comp : ∀ (F : Functor (suc n)) → (f : B → C) → (g : A → B) → (x : ⟦ F ⟧ (A ∷ As)) →
           map F f0 f (map F f0 g x) ≡ map F f0 (f ∘ g) x
map-comp F f g x =
  MapComp.mapComp (mapParamAt f0 f) (mapParamAt f0 g) F [] [! x !] ;
  cong (λ c → Mapping.mapRec c F [] [! x !])
    (funExt λ { f0 → refl ; (fs x) → refl } )

module MapId {m} {As : Params m}
  where
  open Mapping {m = m} {As = As} {Bs = As}

  mapId : ∀ (F : Functor n) (Fs : Layers m n) (xs : <! ⟦ F ⟧ (Fs ++∙ As) !>) →
            mapRec (λ _ x → x) F Fs xs ≡ xs .!!
  mapId (F ⊕ G) Fs [! inl x !] = cong inl (mapId F Fs [! x !])
  mapId (F ⊕ G) Fs [! inr x !] = cong inr (mapId G Fs [! x !])
  mapId (F ⊗ G) Fs [! x , y !] = cong₂ _,_ (mapId F Fs [! x !]) (mapId G Fs [! y !])
  mapId μ⟨ F ⟩  Fs [! ⟨ x ⟩ !] = cong ⟨_⟩ (mapId F (F ∷ Fs) [! x !])
  mapId (! i)      []       [! xs    !] = refl
  mapId (! f0)     (F ∷ Fs) [! ⟨ x ⟩ !] = cong ⟨_⟩ (mapId F (F ∷ Fs) [! x !])
  mapId (! (fs i)) (F ∷ Fs) [! xs    !] = mapId (! i) Fs [! xs !]
  mapId ①      Fs xs = refl

map-id : (F : Functor (suc n)) → (x : ⟦ F ⟧ (A ∷ As)) → map F f0 id x ≡ x
map-id F x =
  cong
    (λ c → Mapping.mapRec c F [] [! x !])
    (funExt (λ { f0 → refl ; (fs i) → refl})) ;
  MapId.mapId F [] [! x !]

---------------------------------------------------------------------------------
--
-- Categorical
--
---------------------------------------------------------------------------------
module Categorical (F : Functor (suc n)) (As : Params n) where
  infix 4 _≗_
  _≗_ : (A → B) → (A → B) → Set _
  f ≗ g = ∀ x → f x ≡ g x
  {-# INLINE _≗_ #-}

  Alg : Type₁
  Alg = Σ[ A ⦂ Type ] × (⟦ F ⟧ (A ∷ As) → A)

  -- Hom
  _⟶_ : Alg → Alg → Type
  (A , a) ⟶ (B , b) = Σ[ h ⦂ (A → B) ] × (h ∘ a ≗ b ∘ map F f0 h)

  variable
    X Y Z : Alg

  _∙_ : (Y ⟶ Z) → (X ⟶ Y) → (X ⟶ Z)
  (f ∙ g) .fst = f .fst ∘ g .fst
  _∙_ {Y = Y}  {Z = Z} {X = X} f g .snd x =
    cong (f .fst) (g .snd x) ;
    f .snd (map F f0 (g .fst) x) ;
    cong (Z .snd) (map-comp F (f .fst) (g .fst) x)

  id′ : X ⟶ X
  id′ .fst = id
  id′ {X = X} .snd x = cong (X .snd) (sym (map-id F x))

---------------------------------------------------------------------------------
--
-- Catamorphisms
--
---------------------------------------------------------------------------------

module Cata {k} {F : Functor (suc k)} {As : Params k} (alg : ⟦ F ⟧ (A ∷ As) → A) where
  cataRec : (G : Functor n) (Gs : Layers (suc m) n) →
            <! ⟦ G ⟧ (Gs ++∙ μ F As ∷ Bs) !> → ⟦ G ⟧ (Gs ++∙ A ∷ Bs)
  cataRec (G₁ ⊕ G₂)  Gs       [! inl x !] = inl (cataRec G₁ Gs [! x !])
  cataRec (G₁ ⊕ G₂)  Gs       [! inr x !] = inr (cataRec G₂ Gs [! x !])
  cataRec (G₁ ⊗ G₂)  Gs       [! x , y !] = cataRec G₁ Gs [! x !] , cataRec G₂ Gs [! y !]
  cataRec μ⟨ G ⟩     Gs       [! ⟨ x ⟩ !] = ⟨ cataRec G (G ∷ Gs) [! x !] ⟩
  cataRec (! f0    ) []       [! ⟨ x ⟩ !] = alg (cataRec F [] [! x !])
  cataRec (! (fs i)) []       [! x     !] = x
  cataRec (! (fs i)) (G ∷ Gs) [! x     !] = cataRec (! i) Gs [! x !]
  cataRec (! f0    ) (G ∷ Gs) [! ⟨ x ⟩ !] = ⟨ cataRec G (G ∷ Gs) [! x !] ⟩
  cataRec ①          Gs       [! _     !] = tt

module _ {F : Functor (suc n)} {As : Params n} where
  cata : (⟦ F ⟧ (A ∷ As) → A) → μ F As → A
  cata alg xs = Cata.cataRec alg {Bs = As} (! f0) [] [! xs !]

module CataId {k} {F : Functor (suc k)} {As : Params k} where
  cataRecId : (G : Functor n) (Gs : Layers (suc m) n) →
              (x : <! ⟦ G ⟧ (Gs ++∙ μ F As ∷ Bs) !>) → Cata.cataRec ⟨_⟩ G Gs x ≡ !! x
  cataRecId (G₁ ⊕ G₂)  Gs       [! inl x !] = cong inl (cataRecId G₁ Gs [! x !])
  cataRecId (G₁ ⊕ G₂)  Gs       [! inr x !] = cong inr (cataRecId G₂ Gs [! x !])
  cataRecId (G₁ ⊗ G₂)  Gs       [! x , y !] = cong₂ _,_ (cataRecId G₁ Gs [! x !]) (cataRecId G₂ Gs [! y !])
  cataRecId μ⟨ G ⟩     Gs       [! ⟨ x ⟩ !] = cong ⟨_⟩ (cataRecId G (G ∷ Gs) [! x !])
  cataRecId (! f0    ) []       [! ⟨ x ⟩ !] = cong ⟨_⟩ (cataRecId F [] [! x !])
  cataRecId (! (fs i)) []       [! x     !] = refl
  cataRecId (! (fs i)) (G ∷ Gs) [! x     !] = cataRecId (! i) Gs [! x !]
  cataRecId (! f0    ) (G ∷ Gs) [! ⟨ x ⟩ !] = cong ⟨_⟩ ( cataRecId G (G ∷ Gs) [! x !] )
  cataRecId ①          Gs       [! _     !] = refl

module _ {F : Functor (suc n)} {As : Params n} where
  cataId : (x : μ F As) → cata ⟨_⟩ x ≡ x
  cataId x = CataId.cataRecId (! f0) [] [! x !]
---------------------------------------------------------------------------------
--
-- Eliminators
--
---------------------------------------------------------------------------------

module Eliminator {As : Params k}
         {F : Functor (suc k)}
         (P : μ F As → Type)
         (f : (x : ⟦ F ⟧ ((∃ x × P x) ∷ As)) → P ⟨ map F f0 fst x ⟩)
         where
  open import Path
  open Mapping
  open Cata

  alg : ⟦ F ⟧ ((∃ x × P x) ∷ As) → ∃ x × P x
  alg x = ⟨ map F f0 fst x ⟩ , f x

  mutual
    elimRec : (G : Functor n) (Gs : Layers (suc m) n) →
              (x : <! ⟦ G ⟧ (Gs ++∙ μ F As ∷ Bs) !>) →
              mapRec (mapParamAt f0 fst) G Gs [! cataRec alg G Gs x !] ≡ !! x
    elimRec (G₁ ⊕ G₂)   Gs       [! inl x !] = cong inl (elimRec G₁ Gs [! x !])
    elimRec (G₁ ⊕ G₂)   Gs       [! inr x !] = cong inr (elimRec G₂ Gs [! x !])
    elimRec (G₁ ⊗ G₂)   Gs       [! x , y !] = cong₂ _,_ (elimRec G₁ Gs [! x !]) (elimRec G₂ Gs [! y !])
    elimRec μ⟨ G ⟩      Gs       [! ⟨ x ⟩ !] = cong ⟨_⟩  (elimRec G (G ∷ Gs) [! x !])
    elimRec (! f0    )  []       [! ⟨ x ⟩ !] = cong ⟨_⟩ (elimRec F [] [! x !])
    elimRec (! (fs i))  []       [! x     !] = refl
    elimRec (! (fs i))  (G ∷ Gs) [! x     !] = elimRec (! i) Gs [! x !]
    elimRec (! f0    )  (G ∷ Gs) [! ⟨ x ⟩ !] = cong ⟨_⟩ (elimRec G (G ∷ Gs) [! x !])
    elimRec ①          Gs        [! _     !] = refl

  elim : ∀ x → P x
  elim x = subst P (elimRec {Bs = As} (! f0) [] [! x !]) (snd (cata alg x))

module _ {F : Functor (suc n)} where
  elim : (P : μ F As → Type) →
         ((x : ⟦ F ⟧ ((∃ x × P x) ∷ As)) → P ⟨ map F f0 fst x ⟩) →
         (x : μ F As) → P x
  elim = Eliminator.elim

module AlgIsomorphism {F : Functor (suc n)} {As : Params n} where
  Alg : Type → Type
  Alg A = ⟦ F ⟧ (A ∷ As) → A

  AsAlg : Type₁
  AsAlg = ∀ A → Alg A → A

  open import Function.Isomorphism

  toAlg : μ F As → AsAlg
  toAlg xs A alg = cata alg xs
  {-# INLINE toAlg #-}

  fromAlg : AsAlg → μ F As
  fromAlg f = f _ ⟨_⟩
  {-# INLINE fromAlg #-}

  rinv : (x : μ F As) → fromAlg (toAlg x) ≡ x
  rinv = cataId

  -- think you need parametricity for this
  -- linv : (x : AsAlg) (A : Type) (alg : Alg A) → toAlg (fromAlg x) A alg ≡ x A alg
  -- linv x A alg = {!!}

  -- isom : AsAlg ⇔ μ F As
  -- isom .fun = fromAlg
  -- isom .inv = toAlg
  -- isom .rightInv = rinv
  -- isom .leftInv x = funExt λ A → funExt λ alg → linv x A alg

---------------------------------------------------------------------------------
--
-- Anamorphisms
--
---------------------------------------------------------------------------------

-- Coinductive fixpoint
record ν (F : Functor (suc n)) (As : Params n) : Type where
  coinductive; constructor ⟪_⟫
  field unfold : ⟦ F ⟧ (ν F As ∷ As)
open ν public

-- The "proper" anamorphism, which is coinductive.
module AnaInf {k} {F : Functor (suc k)} {As : Params k} (coalg : A → ⟦ F ⟧ (A  ∷ As)) where
  mutual
    anaRec : (G : Functor n) (Gs : Layers (suc m) n) →
             <! ⟦ G ⟧ (Gs ++∙ A ∷ Bs) !> → <! ⟦ G ⟧ (Gs ++∙ ν F As ∷ Bs) !>
    anaRec (G₁ ⊕ G₂)  Gs       [! inl x !] .!! = inl (anaRec G₁ Gs [! x !] .!!)
    anaRec (G₁ ⊕ G₂)  Gs       [! inr x !] .!! = inr (anaRec G₂ Gs [! x !] .!!)
    anaRec (G₁ ⊗ G₂)  Gs       [! x , y !] .!! .fst = anaRec G₁ Gs [! x !] .!!
    anaRec (G₁ ⊗ G₂)  Gs       [! x , y !] .!! .snd = anaRec G₂ Gs [! y !] .!!
    anaRec μ⟨ G ⟩     Gs       [! ⟨ x ⟩ !] .!! = ⟨ anaRec G (G ∷ Gs) [! x !] .!! ⟩
    anaRec (! f0    ) []       [! x     !] .!! = ana x
    anaRec (! (fs i)) []       [! x     !] .!! = x
    anaRec (! (fs i)) (G ∷ Gs) [! x     !] .!! = anaRec (! i) Gs [! x !] .!!
    anaRec (! f0    ) (G ∷ Gs) [! ⟨ x ⟩ !] .!! = ⟨ anaRec G (G ∷ Gs) [! x !] .!! ⟩
    anaRec ①          Gs       [! _     !] .!! = tt

    ana : A → ν F As
    ana x .unfold = anaRec F [] [! coalg x !] .!!

module AnaInfDisplay {F : Functor (suc n)} {As : Params n} where
  ana : (A → ⟦ F ⟧ (A ∷ As)) → A → ν F As
  ana = AnaInf.ana
open AnaInfDisplay public

-- The terminating anamorphism: uses well-founded recursion to ensure we're
-- building a finite type.
module AnaTerm {B : Type} {_<_ : B → B → Type} (<-wellFounded : WellFounded _<_)
         {k} {F : Functor (suc k)}
         {As : Params k}
         (coalg : (x : B) → ⟦ F ⟧ ((∃ y × (y < x))  ∷ As)) where

  pr-anaAcc : (x : B) → Acc _<_ x → μ F As
  pr-anaAcc x (acc wf) = ⟨ map F f0 (λ { (x , p) → pr-anaAcc x (wf x p) }) (coalg x)  ⟩

  pr-ana : B → μ F As
  pr-ana x = pr-anaAcc x (<-wellFounded x)

module AnaTermDisplay
  {A : Type}
  {_<_ : A → A → Type}
  {F : Functor (suc n)}
  {As : Params n}
  where
  pr-ana :  WellFounded _<_ →
            ((x : A) → ⟦ F ⟧ ((∃ y × (y < x)) ∷ As)) → A → μ F As
  pr-ana wf = AnaTerm.pr-ana wf

module Truncate {B : Type} {_<_ : B → B → Type} (<-wellFounded : WellFounded _<_)
                {k} {F : Functor (suc k)}
                {As : Params k} (step : (x : B) -> ⟦ F ⟧ (ν F As ∷ As) → ⟦ F ⟧ ((ν F As × ∃ y × (y < x)) ∷ As)) where

  truncAcc : (x : B) → Acc _<_ x → ν F As → μ F As
  truncAcc x (acc wf) xs = ⟨ map F f0 (λ { (ys , z , z<x) → truncAcc z (wf z z<x) ys}) (step x (xs .unfold)) ⟩

  trunc : B → ν F As → μ F As
  trunc x = truncAcc x (<-wellFounded x)

module TruncDisplay
  {A : Type}
  {_<_ : A → A → Type}
  {F : Functor (suc n)}
  {As : Params n} where
  trunc :  WellFounded _<_ →
           ((x : A) -> ⟦ F ⟧ (ν F As ∷ As) → ⟦ F ⟧ ((ν F As × ∃ y × (y < x)) ∷ As)) →
           A → ν F As → μ F As
  trunc wf step = Truncate.trunc wf step

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module SystemF.WellTyped where

open import Prelude hiding (id; erase)

open import SystemF.Syntax public
open import SystemF.Substitutions
open import Data.Vec hiding ([_])
open import Data.Vec.Properties
open import Data.Product

infix 4 _⊢_∈_
data _⊢_∈_ {ν n} (Γ : Ctx ν n) : Term ν n → Type ν → Set where
  var : (x : Fin n) → Γ ⊢ var x ∈ lookup x Γ
  Λ   : ∀ {t a} → (ctx-weaken Γ) ⊢ t ∈ a → Γ ⊢ Λ t ∈ ∀' a
  λ'  : ∀ {t b} → (a : Type ν) → a ∷ Γ ⊢ t ∈ b → Γ ⊢ λ' a t ∈ a →' b
  _[_] : ∀ {t a} → Γ ⊢ t ∈ ∀' a → (b : Type ν) → Γ ⊢ t [ b ] ∈ a tp[/tp b ]
  _·_  : ∀ {f t a b} → Γ ⊢ f ∈ (a →' b) → Γ ⊢ t ∈ a → Γ ⊢ f · t ∈ b

_⊢_∉_ : ∀ {ν n} → (Γ : Ctx ν n) → Term ν n → Type ν → Set
_⊢_∉_ Γ t τ = ¬ Γ ⊢ t ∈ τ

erase : ∀ {ν n} {Γ : Ctx ν n} {t τ} → Γ ⊢ t ∈ τ → Term ν n
erase (var x) = var x
erase (Λ {t} x) = Λ t
erase (λ' {t} a x) = λ' a t
erase (_[_] {t} x b) = t
erase (_·_ {f} x x₁) = f

⊢f·a-inversion : ∀ {ν n f t b} {Γ : Ctx ν n} → Γ ⊢ f · t ∈ b →
                 ∃ λ a → Γ ⊢ f ∈ a →' b × Γ ⊢ t ∈ a
⊢f·a-inversion (_·_ f∈a→b t∈a) = , (f∈a→b , t∈a)

⊢tc[a]-inversion : ∀ {ν n tc a' b} {Γ : Ctx ν n} → Γ ⊢ tc [ b ] ∈ a' → ∃ λ a → Γ ⊢ tc ∈ ∀' a
⊢tc[a]-inversion (_[_] tc∈∀'a b) = , tc∈∀'a

unique-type : ∀ {ν n} {Γ : Ctx ν n} {t τ τ'} → Γ ⊢ t ∈ τ → Γ ⊢ t ∈ τ' → τ ≡ τ'
unique-type (var x) (var .x) = refl
unique-type (Λ l) (Λ r) = cong ∀' (unique-type l r)
unique-type (λ' a l) (λ' .a r) = cong (λ b → a →' b) (unique-type l r)
unique-type (l [ b ]) (r [ .b ]) = cong (λ{ (∀' fa) → fa tp[/tp b ]; a → a}) (unique-type l r)
unique-type (f · e) (f' · e') = cong (λ{ (a →' b) → b; a → a }) (unique-type f f')

unique-type′ : ∀ {ν n} {Γ : Ctx ν n} {t τ τ'} → Γ ⊢ t ∈ τ → τ ≢ τ' → Γ ⊢ t ∉ τ'
unique-type′ ⊢t∈τ neq ⊢t∈τ' = neq $ unique-type ⊢t∈τ ⊢t∈τ'

-- Collections of typing derivations for well-typed terms.
data _⊢ⁿ_∈_ {m n} (Γ : Ctx n m) :
  ∀ {k} → Vec (Term n m) k → Vec (Type n) k → Set where
    []  : Γ ⊢ⁿ [] ∈ []
    _∷_ : ∀ {t a k} {ts : Vec (Term n m) k} {as : Vec (Type n) k} →
          Γ ⊢ t ∈ a → Γ ⊢ⁿ ts ∈ as → Γ ⊢ⁿ t ∷ ts ∈ (a ∷ as)

-- Lookup a well-typed term in a collection thereof.
lookup-⊢ : ∀ {m n k} {Γ : Ctx n m} {ts : Vec (Term n m) k}
             {as : Vec (Type n) k} →
           (x : Fin k) → Γ ⊢ⁿ ts ∈ as → Γ ⊢ lookup x ts ∈ lookup x as
lookup-⊢ zero    (⊢t ∷ ⊢ts) = ⊢t
lookup-⊢ (suc x) (⊢t ∷ ⊢ts) = lookup-⊢ x ⊢ts


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Pointed.Homotopy where

{-
  This module defines two kinds of pointed homotopies,
  ∙∼ and ∙∼P, and proves their equivalence
-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Fiberwise
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Path
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Pointed.Base
open import Cubical.Foundations.Pointed.Properties
open import Cubical.Homotopy.Base
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' : Level

module _ {A : Pointed ℓ} {B : typ A → Type ℓ'} {ptB : B (pt A)} where

  ⋆ = pt A

  -- pointed homotopy as pointed Π. This is just a Σ-type, see ∙∼Σ
  _∙∼_ : (f g : Π∙ A B ptB) → Type (ℓ-max ℓ ℓ')
  (f₁ , f₂) ∙∼ (g₁ , g₂) = Π∙ A (λ x → f₁ x ≡ g₁ x) (f₂ ∙ g₂ ⁻¹)

  -- pointed homotopy with PathP. Also a Σ-type, see ∙∼PΣ
  _∙∼P_ : (f g : Π∙ A B ptB) → Type (ℓ-max ℓ ℓ')
  (f₁ , f₂) ∙∼P (g₁ , g₂) = Σ[ h ∈ f₁ ∼ g₁ ] PathP (λ i → h ⋆ i ≡ ptB) f₂ g₂

  -- Proof that f ∙∼ g ≃ f ∙∼P g
  -- using equivalence of the total map of φ
  private
    module _ (f g : Π∙ A B ptB) (H : f .fst ∼ g .fst) where
      -- convenient notation
      f₁ = fst f
      f₂ = snd f
      g₁ = fst g
      g₂ = snd g

      -- P is the predicate on a homotopy H to be pointed of the ∙∼ kind
      P : Type ℓ'
      P = H ⋆ ≡ f₂ ∙ g₂ ⁻¹

      -- Q is the predicate on a homotopy H to be pointed of the ∙∼P kind
      Q : Type ℓ'
      Q = PathP (λ i → H ⋆ i ≡ ptB) f₂ g₂

      -- simplify the notation even more to see that P≡Q
      -- is just a jingle of paths
      p = H ⋆
      r = f₂
      s = g₂
      P≡Q : P ≡ Q
      P≡Q = p ≡ r ∙ s ⁻¹
              ≡⟨ isoToPath (symIso p (r ∙ s ⁻¹)) ⟩
            r ∙ s ⁻¹ ≡ p
              ≡⟨ cong (r ∙ s ⁻¹ ≡_) (rUnit p ∙∙ cong (p ∙_) (sym (rCancel s)) ∙∙ assoc p s (s ⁻¹)) ⟩
            r ∙ s ⁻¹ ≡ (p ∙ s) ∙ s ⁻¹
              ≡⟨ sym (ua (compr≡Equiv r (p ∙ s) (s ⁻¹))) ⟩
            r ≡ p ∙ s
              ≡⟨ ua (compl≡Equiv (p ⁻¹) r (p ∙ s)) ⟩
            p ⁻¹ ∙ r ≡ p ⁻¹ ∙ (p ∙ s)
              ≡⟨ cong (p ⁻¹ ∙ r ≡_ ) (assoc (p ⁻¹) p s ∙∙ (cong (_∙ s) (lCancel p)) ∙∙ sym (lUnit s)) ⟩
            p ⁻¹ ∙ r ≡ s
              ≡⟨ cong (λ z → p ⁻¹ ∙ z ≡ s) (rUnit r) ⟩
            p ⁻¹ ∙ (r ∙ refl) ≡ s
              ≡⟨ cong (_≡ s) (sym (doubleCompPath-elim' (p ⁻¹) r refl)) ⟩
            p ⁻¹ ∙∙ r ∙∙ refl ≡ s
              ≡⟨ sym (ua (Square≃doubleComp r s p refl)) ⟩
            PathP (λ i → p i ≡ ptB) r s ∎

      -- φ is a fiberwise transformation (H : f ∼ g) → P H → Q H
      -- φ is even a fiberwise equivalence by P≡Q
      φ : P → Q
      φ = transport P≡Q

    -- The total map corresponding to φ
    totφ : (f g : Π∙ A B ptB) → f ∙∼ g → f ∙∼P g
    totφ f g p .fst = p .fst
    totφ f g p .snd = φ f g (p .fst) (p .snd)

  -- transformation of the homotopies using totφ
  ∙∼→∙∼P : (f g : Π∙ A B ptB) → (f ∙∼ g) → (f ∙∼P g)
  ∙∼→∙∼P f g = totφ f g

  -- Proof that ∙∼ and ∙∼P are equivalent using the fiberwise equivalence φ
  ∙∼≃∙∼P : (f g : Π∙ A B ptB) → (f ∙∼ g) ≃ (f ∙∼P g)
  ∙∼≃∙∼P f g = Σ-cong-equiv-snd (λ H → transportEquiv (P≡Q f g H))

  -- inverse of ∙∼→∙∼P extracted from the equivalence
  ∙∼P→∙∼ : {f g : Π∙ A B ptB} → f ∙∼P g → f ∙∼ g
  ∙∼P→∙∼ {f = f} {g = g} = invEq (∙∼≃∙∼P f g)

  -- ∙∼≃∙∼P transformed to a path
  ∙∼≡∙∼P : (f g : Π∙ A B ptB) → (f ∙∼ g) ≡ (f ∙∼P g)
  ∙∼≡∙∼P f g = ua (∙∼≃∙∼P f g)

  -- Verifies that the pointed homotopies actually correspond
  -- to their Σ-type versions
  _∙∼Σ_ : (f g : Π∙ A B ptB) → Type (ℓ-max ℓ ℓ')
  f ∙∼Σ g = Σ[ H ∈ f .fst ∼ g .fst ] (P f g H)

  _∙∼PΣ_ : (f g : Π∙ A B ptB) → Type (ℓ-max ℓ ℓ')
  f ∙∼PΣ g = Σ[ H ∈ f .fst ∼ g .fst ] (Q f g H)

  ∙∼≡∙∼Σ : (f g : Π∙ A B ptB) → f ∙∼ g ≡ f ∙∼Σ g
  ∙∼≡∙∼Σ f g = refl

  ∙∼P≡∙∼PΣ : (f g : Π∙ A B ptB) → f ∙∼P g ≡ f ∙∼PΣ g
  ∙∼P≡∙∼PΣ f g = refl

max_stars_repo_name: L-TChen/cubical

max_issues_repo_name: L-TChen/cubical

max_forks_repo_name: L-TChen/cubical


text:
open import Prelude
open import core

module lemmas-matching where
  -- matching produces unique answers for arrows, sums, and products
  ▸arr-unicity : ∀{ t t2 t3 } →
                 t ▸arr t2 →
                 t ▸arr t3 →
                 t2 == t3
  ▸arr-unicity MAHole MAHole = refl
  ▸arr-unicity MAArr MAArr = refl

  -- if an arrow matches, then it's consistent with the least restrictive
  -- function type
  matchconsisthole : ∀{t t'} →
                 t ▸arr t' →
                 t ~ (⦇-⦈ ==> ⦇-⦈)
  matchconsisthole MAHole = TCHole2
  matchconsisthole MAArr = TCArr TCHole1 TCHole1

  match-consist : ∀{τ1 τ2} → τ1 ▸arr τ2 → (τ2 ~ τ1)
  match-consist MAHole = TCHole1
  match-consist MAArr = TCRefl

  match-unicity : ∀{ τ τ1 τ2} → τ ▸arr τ1 → τ ▸arr τ2 → τ1 == τ2
  match-unicity MAHole MAHole = refl
  match-unicity MAArr MAArr = refl

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
-- Reported by Christian Sattler on 2019-12-07

open import Agda.Primitive

postulate
  i : Level
  X : Set i

mutual
  j : Level
  j = _

  Y : Set j
  Y = X

-- WAS: unsolved constraint i = _2
-- SHOULD: succeed with everything solved


text:
module Warnings where

-- empty rewrite pragma
{-# REWRITE #-}

-- termination checking error
A : Set
A = A

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

{-# BUILTIN NATURAL Nat #-}

-- deprecated BUILTIN ZERO
{-# BUILTIN ZERO zero #-}

-- An open goal
g : Set
g = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda