text:
-- Axiomatic embedding of guarded recursion in Agda
module guarded-recursion.embedding where

open import guarded-recursion.prelude
  renaming (O to zero; S to suc)
open Coe

module M
    (▹_ : ∀ {a} → Type_ a → Type_ a)

    (▸ : ∀ {a} → ▹ (Type_ a) → Type_ a)

    (next : ∀ {a} {A : Type_ a} → A → ▹ A)

    (▸-rule : ∀ {a} {A : Type_ a} → ▸ (next A) ≡ ▹ A)

    (fix      : ∀ {a} {A : Type_ a} → (▹ A → A) → A)
    (fix-rule : ∀ {a} {A : Type_ a} {f : ▹ A → A} → fix f ≡ f (next (fix f)))

    (_⊛′_ : ∀ {a b} {A : Type_ a} {B : Type_ b} → ▹ (A → B) → ▹ A → ▹ B)
    (_⊛_ : ∀ {a b} {A : Type_ a} {B : A → Type_ b}
           → ▹ ((x : A) → B x) → (x : ▹ A) → ▸ (next B ⊛′ x))

    (fix-uniq : ∀ {a} {A : Type_ a} (u : A) f → u ≡ f (next u) → u ≡ fix f)

    (next⊛next : ∀ {a b} {A : Type_ a} {B : Type_ b} (f : A → B) (x : A)
                 → next f ⊛′ next x ≡ next (f x))

    where

    roll▸ : ∀ {a} {A : Type_ a} → ▹ A → ▸ (next A)
    roll▸ = coe! ▸-rule

    un▸ : ∀ {a} {A : Type_ a} → ▸ (next A) → ▹ A
    un▸ = coe ▸-rule

    ▹Fix : ∀ {a} → Type_ a → Type_ a
    ▹Fix X = (▹ X → X) → X

    ▹Endo : ∀ {a} → Type_ a → Type_ a
    ▹Endo X = ▹ X → X

    μ : ∀ {a} → Fix (Type_ a)
    μ F = fix (F ∘ ▸)

    un : ∀ {a f} → fix {A = Type_ a} f → f (next (fix f))
    un = coe fix-rule

    unμ : ∀ {a} f → μ {a} f → f (▹ μ f)
    unμ {a} f x rewrite ! (▸-rule {A = μ f}) = un x

    roll : ∀ {a f} → f (next (fix f)) → fix {A = Type_ a} f
    roll = coe! fix-rule

    μ-rule : ∀ {a} f → μ {a} f ≡ f (▹ μ f)
    μ-rule f = fix-rule ∙ ap f (▸-rule {A = μ f})

    rollμ : ∀ {a} f → f (▹ μ f) → μ {a} f
    rollμ f = coe! (μ-rule f)

    un₁ : ∀ {a b} {A : Type_ a} {f x} → fix {A = A → Type_ b} f x → f (next (fix f)) x
    un₁ = coe₁ fix-rule

    roll₁ : ∀ {a b} {A : Type_ a} {f x} → f (next (fix f)) x → fix {A = A → Type_ b} f x
    roll₁ = coe₁! fix-rule

    un₂ : ∀ {a b} {A : Type_ a} {B : Type_ b} {c f x y} → fix {A = A → B → Type_ c} f x y → f (next (fix f)) x y
    un₂ = coe₂ fix-rule

    roll₂ : ∀ {a b} {A : Type_ a} {B : Type_ b} {c f x y} → f (next (fix f)) x y → fix {A = A → B → Type_ c} f x y
    roll₂ = coe₂! fix-rule

    map▹ : ∀ {a b} {A : Type_ a} {B : Type_ b} → (A → B) → ▹ A → ▹ B
    map▹ f ▹x = next f ⊛′ ▹x

    {-
    alternatively
    _⊛′′_ : ∀ {a b} {A : Type_ a} {B : A → Type_ b} → ▹ ((x : A) → B x) → (x : A) → ▹ (B x)
    ▹f ⊛′′ x = map▹ (λ f → f x) ▹f
    -}

    {-
    alternatively
    _$_ : ∀ {a b} {A : Type_ a} (B : A → Type_ b) → ▹ A → ▹ (Type_ b)
    f $ ▹x = map▹ f ▹x
    -}

    ▹^ : ∀ {a} → ℕ → Type_ a → Type_ a
    ▹^ zero    A = A
    ▹^ (suc n) A = ▹ ▹^ n A

    next^ : ∀ {a} {A : Type_ a} n → A → ▹^ n A
    next^ zero    x = x
    next^ (suc n) x = next (next^ n x)

    map▹^ : ∀ {a b} {A : Type_ a} {B : Type_ b} n → (A → B) → ▹^ n A → ▹^ n B
    map▹^ zero    f = f
    map▹^ (suc n) f = map▹ (map▹^ n f)

    module SimpleStream where
      F : Type → Type → Type
      F A X = A × X

      S : Type → Type
      S A = μ (F A)

    μ₁F' : ∀ {a} {A : Type_ a} → ((A → ▹ Type) → A → Type) → (▹(A → Type) → A → Type)
    μ₁F' F self = F (λ x → (self ⊛′ next x))

    μ₁F : ∀ {a} {A : Type_ a} → ((A → Type) → A → Type) → (▹(A → Type) → A → Type)
    μ₁F F self = F (λ x → ▸ (self ⊛′ next x))

    μ₁ : ∀ {a} {A : Type_ a} → ((A → Type) → A → Type) → A → Type
    μ₁ F = fix (μ₁F F)

    module μId where
        μid : Type
        μid = μ id

        μid-rule : μid ≡ ▹ μid
        μid-rule = fix-rule ∙ ▸-rule {A = μ id}

        ω : μid
        ω = fix (rollμ id)

    module CoNat where
        Coℕ : Type
        Coℕ = μ Maybe

        rollNat : Maybe (▹ Coℕ) → Coℕ
        rollNat = rollμ Maybe

        ze : Coℕ
        ze = rollNat nothing

        su : ▹ Coℕ → Coℕ
        su x = rollNat (just x)

        su′ : Coℕ → Coℕ
        su′ = su ∘ next

        ω : Coℕ
        ω = fix su

    module Neg where
        {- data X : Type where
             rollX : Fix X
                   : (X → X) → X
           -}
        X : Type
        X = μ Endo

        rollX : Endo (▹ X) → X
           -- : (▹ X → ▹ X) → X
        rollX = rollμ Endo

        rollX′ : ▹(Endo X) → X
            -- : ▹(X → X) → X
        rollX′ = rollX ∘ _⊛′_

        unX : X → Endo (▹ X)
        unX = unμ Endo

        -- δ = λ x → x x
        δ : X → ▹ X
        δ = λ x → (unX x) (next x)

    module Neg' where
        {- data X : Type where
             c : Fix X
               : ((X → X) → X) → X
           -}
        X : Type
        X = μ Fix

        rollX : Fix (▹ X) → X
        rollX = rollμ Fix

        unX : X → Fix (▹ X)
        unX = unμ Fix

    module μ₁Id where
        -- μ₁id = ▹∘▹∘…∘▹
        -- μ₁id A = ▹ (▹ … (▹ A))
        μ₁id : Type → Type
        μ₁id = μ₁ id

        betterfix₁ : ∀ {a} {A : Type_ a} {x : A} (F : Endo (A → Type)) → (▹ μ₁ F x → μ₁F F (next (μ₁ F)) x) → μ₁ F x
        betterfix₁ {a} {A} {x} F f = fix helper
          where helper : _ → _
                helper self = roll₁ (f self)

        ▹ω-inh' : ∀ {A : Type} {x : A} (F : Endo (A → Type)) → (▸ (next (μ₁ F) ⊛′ next x) → μ₁F F (next (μ₁ F)) x) → μ₁ F x
        ▹ω-inh' {A} {x} F f = fix helper
          where helper : _ → _
                helper self = roll₁ (f (coe! (ap ▸ (next⊛next (μ₁ F) x)) (roll▸ self)))

        ▹ω-inh : ∀ {A} → μ₁id A
        -- ▹ω-inh {A} = fix λ self → roll₁ (coe! (ap ▸ (next⊛next μ₁id A)) (roll▸ self))
        ▹ω-inh {A} = betterfix₁ id (λ self → coe! (ap ▸ (next⊛next μ₁id A)) (roll▸ self))

        -- ▹ω-inh {A} = fix λ self → {!!} -- (coe! (ap ▸ (next⊛next μ₁idω A)) (roll▸ self))

    fix2 : ∀ {a} {A : Type_ a} → (▹ A → A) → A
    fix2 f = fix (f ∘ next ∘ f)

    fix≡fix2 : ∀ {a} {A : Type_ a} (f : ▹ A → A) → fix f ≡ fix2 f
    fix≡fix2 f = fix-uniq (fix f) (f ∘ next ∘ f) (fix-rule ∙ ap (f ∘ next) fix-rule)

    module Streams where
        F : Type → Type → Type
        F A X = A × X

        -- S : Type → Type
        -- S A = μ (F A)

        F^ : ℕ → Type → Type → Type
        F^ n A X = A × ▹^ n X

        S^ : ℕ → Type → Type
        S^ n A = μ (F^ n A)

        S : Type → Type
        S = S^ 0

        S₂ = S^ 1

        unS : ∀ {A} → S A → F A (▹ S A)
        unS = unμ (F _)

        rollS : ∀ {A} → F A (▹ S A) → S A
        rollS = rollμ (F _)

        unS^ : ∀ {A} n → S^ n A → F^ n A (▹ S^ n A)
        unS^ n = unμ (F^ n _)

        rollS^ : ∀ {A} n → F^ n A (▹ S^ n A) → S^ n A
        rollS^ n = rollμ (F^ n _)

        hd : ∀ {A} → S A → A
        hd = fst ∘ unS

        tl : ∀ {A} → S A → ▹ S A
        tl = snd ∘ unS

        cons : ∀ {A} n → A → ▹^ n (▹ (S^ n A)) → S^ n A
        cons n x xs = rollS^ n (x , xs)

        infixr 4 _∷_
        _∷_ : ∀ {A} → A → ▹ (S A) → S A
        _∷_ = cons 0

        infixr 4 _∷₂_
        _∷₂_ : ∀ {A} → A → ▹^ 2 (S₂ A) → S₂ A
        x ∷₂ xs = roll (x , map▹ roll▸ xs)

        repeatS : ∀ {A} → A → S A
        repeatS x = fix λ x… → x ∷ x…

        module MapS {A B : Type} (f : A → B) where
            mapSf : ▹(S A → S B) → S A → S B
            mapSf self s = f (hd s) ∷ self ⊛′ tl s

            mapS : S A → S B
            mapS = fix mapSf

            mapS2f : ▹(S A → S B) → S A → S B
            mapS2f self s = f (hd s) ∷ map▹ (λ s' → f (hd s') ∷ self ⊛′ tl s') (tl s)

            mapS2f' : ▹(S A → S B) → S A → S B
            mapS2f' self = mapSf (next (mapSf self))

            mapS2f≡mapS2f' : mapS2f ≡ mapS2f'
            mapS2f≡mapS2f' = idp

            mapS2 : S A → S B
            mapS2 = fix mapS2f

            mapS2' : S A → S B
            mapS2' = fix mapS2f'

            mapS2≡mapS2' : mapS2 ≡ mapS2'
            mapS2≡mapS2' = idp

            mapS2'' : S A → S B
            mapS2'' = fix2 mapSf

            mapS2≡mapS2'' : mapS2 ≡ mapS2''
            mapS2≡mapS2'' = idp

            mapS≡mapS2 : mapS ≡ mapS2
            mapS≡mapS2 = fix≡fix2 mapSf

        open MapS

        group2 : S ℕ → ▹ S₂ ℕ²
        group2 = fix λ self s → map▹ (λ tls → (hd s , hd tls) ∷₂ self ⊛′ tl tls) (tl s)

        ‼ : ∀ {A} → (n : ℕ) → S A → ▹^ n A
        ‼ zero    = hd
        ‼ (suc n) = map▹ (‼ n) ∘ tl

        toFun : ∀ {A} → S A → (n : ℕ) → ▹^ n A
        toFun s n = ‼ n s

        fromFun : ∀ {A} → (ℕ → A) → S A
        fromFun {A} = fix λ self (f : ℕ → A) → f 0 ∷ self ⊛′ next (f ∘ suc)

        nats : S ℕ
        nats = fix λ self → 0 ∷ map▹ (mapS suc) self

        nats2 : S ℕ
        nats2 = fix λ self → 0 ∷ map▹ (mapS2 suc) self

        nats≡nats2 : nats ≡ nats2
        nats≡nats2 rewrite mapS≡mapS2 suc = idp

        arrow : ▹ ℕ
        arrow = ‼ 1 nats

        module Sim
            {A : Type}
            (ℛ : A → A → Type)
            (ℛ-refl : Reflexive ℛ)
          where
            ≈F : ▹(S A × S A → Type) → S A × S A → Type
            ≈F X (xs , ys) = ℛ (hd xs) (hd ys) × ▸ ((map▹ curry X ⊛′ (tl xs)) ⊛′ tl ys)

            _≈_ : S A × S A → Type
            _≈_ = fix ≈F

            ≈-tail : ∀ {xs ys : S A} → _≈_ (xs , ys) → ▸ ((map▹ curry (next _≈_) ⊛′ tl xs) ⊛′ tl ys)
            ≈-tail pf = snd (un₁ pf)

            {- Does not work yet
            ≈-refl : Reflexive (curry _≈_)
            ≈-refl {x} = (fix λ pf x → roll₁ {f = ≈F} (ℛ-refl , helper pf x)) x
              where helper' : _ → _ → _
                    helper' pf x = map▹ (λ f → f x) pf
                    helper : _ → _ → _
                    helper pf x = let r = helper' pf x in {!roll▸ r!}
            -}

    module DelayedStreams where
        data F (A : Type) (X : Type) : Type where
          done  : F A X
          skip  : X → F A X
          yield : A → X → F A X

        mapF : ∀ {A B X Y} → (A → B) → (X → Y) → F A X → F B Y
        mapF f g done = done
        mapF f g (skip x) = skip (g x)
        mapF f g (yield a x) = yield (f a) (g x)

        S : Type → Type
        S A = μ (F A)

        unS : ∀ {A} → S A → F A (▹ S A)
        unS = mapF id un▸ ∘ un

        rollS : ∀ {A} → F A (▹ S A) → S A
        rollS = roll ∘ mapF id roll▸

        unfoldS : ∀ {A X} → (X → F A (▹ X)) → X → S A
        unfoldS coalg = fix λ self x → rollS (mapF id (λ x′ → self ⊛′ x′) (coalg x))

        repeatS : ∀ {A} → A → S A
        repeatS x = fix λ self → rollS (yield x self)

        neverS : ∀ {A} → S A
        neverS = fix λ self → rollS (skip self)

        -- Co-algebra style...
        mapS : ∀ {A B} → (A → B) → S A → S B
        mapS {A} {B} f = unfoldS (mapF f id ∘ unS)

        filterF : ∀ {A X} → (A → 𝟚) → F A X → F A X
        filterF f done         = done
        filterF f (skip xs)    = skip xs
        filterF f (yield x xs) = if f x then yield x xs
                                        else skip xs

        filterS : ∀ {A} → (A → 𝟚) → S A → S A
        filterS f = unfoldS (filterF f ∘ unS)

module FuelBased where
    fix : ∀ {a} {A : Type_ a} → ℕ → (A → A) → A
    fix zero    f = STUCK where postulate STUCK : _
    fix (suc n) f = f (fix n f)

    fix-rule : ∀ {a} {A : Type_ a} (n : ℕ) {f : A → A} → fix n f ≡ f (fix n f)
    fix-rule zero        = ThisIsUnsafeButPlease.trustMe
    fix-rule (suc n) {f} = ap f (fix-rule n)

    fix-uniq : ∀ {a} {A : Type_ a} (n : ℕ) (u : A) f → u ≡ f u → u ≡ fix n f
    fix-uniq zero    u f pf = ThisIsUnsafeButPlease.trustMe
    fix-uniq (suc n) u f pf = pf ∙ ap f (fix-uniq n u f pf)

    module I (n : ℕ) = M id id id idp (fix n) (fix-rule n) id id
                         (fix-uniq n) (λ _ _ → idp)

module HiddenFix {a} {A : Type_ a} (f : A → A) where
    -- This definition is not intended to termination-check.
    -- Use with care it's really easy to make the type-checker loop.
    {-# TERMINATING #-}
    fix : Hidden A
    fix = hide f (reveal fix)

    fix-rule : reveal fix ≡ f (reveal fix)
    fix-rule = idp {a} {A} {reveal fix}

    -- This definition is not intended to termination-check.
    -- Use with care it's really easy to make the type-checker loop.
    {-# TERMINATING #-}
    fix-uniq : (u : A) → u ≡ f u → u ≡ reveal fix
    fix-uniq u pf = pf ∙ ap f (fix-uniq u pf) ∙ ! fix-rule

module Test where
  open HiddenFix
  open M id id id idp (reveal ∘ fix) (λ {_} {_} {f} → fix-rule f) id id
                 (λ {_} {_} u f → fix-uniq f u) (λ _ _ → idp) public
  open Streams
  two : map▹ hd (tl nats) ≡ 1
  two = idp

-- -}
-- -}
-- -}

max_stars_repo_name: np/guarded-recursion

max_issues_repo_name: np/guarded-recursion

max_forks_repo_name: np/guarded-recursion


text:
module Issue644 where

postulate
  A : Set

record R : Set₁ where
  field P : A → Set

module M₁ (r : R) where

  postulate
    Foo₁ : ((x : A) → R.P r x) → Set

module M₂ (r : R) where

  open R r

  postulate
    Foo₂ : ((x : A) → P x) → Set

postulate r : R

open R  r
open M₁ r
open M₂ r

foo₂ : Set
foo₂ = Foo₂ r

-- Error message should speak about
--
--   (x : A) → P x
--
-- not mention
--
--   (x : A) → .Bug.M₂._.P r x

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Categories.Category.Instance.Properties.Setoids.CCC where

open import Level
open import Data.Product using (Σ ; _,_)
open import Function.Equality as ⟶ using (Π; _⟶_)
open import Relation.Binary using (Setoid)

open import Categories.Category
open import Categories.Category.Monoidal.Instance.Setoids
open import Categories.Category.CartesianClosed
open import Categories.Category.CartesianClosed.Canonical renaming (CartesianClosed to CCartesianClosed)
open import Categories.Category.Instance.Setoids

open Π

module _ ℓ where
  private
    S = Setoids ℓ ℓ
    module S = Category S

  Setoids-Canonical : CCartesianClosed S
  Setoids-Canonical = record
    { ⊤            = ⊤
    ; _×_          = _×_
    ; !            = !
    ; π₁           = π₁
    ; π₂           = π₂
    ; ⟨_,_⟩        = ⟨_,_⟩
    ; !-unique     = !-unique
    ; π₁-comp      = λ {_ _ f _ g} → project₁ {h = f} {g}
    ; π₂-comp      = λ {_ _ f _ g} → project₂ {h = f} {g}
    ; ⟨,⟩-unique   = λ {_ _ _ f g h} → unique {h = h} {f} {g}
    ; _^_          = λ X Y → Y ⟶.⇨ X
    ; eval         = λ {X Y} → record
      { _⟨$⟩_ = λ { (f , x) → f ⟨$⟩ x }
      ; cong  = λ { (eq₁ , eq₂) → eq₁ eq₂ }
      }
    ; curry        = λ {C A B} f → record
      { _⟨$⟩_ = λ c → record
        { _⟨$⟩_ = λ a → f ⟨$⟩ (c , a)
        ; cong  = λ eq → cong f (Setoid.refl C , eq)
        }
      ; cong  = λ eq₁ eq₂ → cong f (eq₁ , eq₂)
      }
    ; eval-comp    = λ {_ _ _ f} → cong f
    ; curry-resp-≈ = λ eq₁ eq₂ eq → eq₁ (eq₂ , eq)
    ; curry-unique = λ eq₁ eq₂ eq → eq₁ (eq₂ , eq)
    }
    where open Setoids-Cartesian

  Setoids-CCC : CartesianClosed S
  Setoids-CCC = Equivalence.fromCanonical S Setoids-Canonical

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
module Lec8 where

open import CS410-Prelude
open import CS410-Functor
open import CS410-Monoid
open import CS410-Nat

data Maybe (X : Set) : Set where
  yes  : X -> Maybe X
  no   : Maybe X

maybeFunctor : Functor Maybe
maybeFunctor = record
 { map      = \ { f (yes x) -> yes (f x)
                ; f no      -> no
                }
 ; mapid    = \ { (yes x) -> refl ; no -> refl }
 ; mapcomp  = \ { f g (yes x) -> refl ; f g no -> refl } }

open Functor maybeFunctor

data List (X : Set) : Set where  -- X scopes over the whole declaration...
  []    : List X                 -- ...so you can use it here...
  _::_  : X -> List X -> List X  -- ...and here.
infixr 3 _::_

data Hutton : Set where
  val : Nat -> Hutton
  _+H_ : Hutton -> Hutton -> Hutton
  hif_then_else_ : Hutton -> Hutton -> Hutton -> Hutton
  fail : Hutton

maybeApplicative : Applicative Maybe
maybeApplicative = record
                     { pure = yes
                     ; _<*>_ = \ { no mx -> no
                                 ; (yes f) no -> no
                                 ; (yes f) (yes x) -> yes (f x)
                                 }
                     ; identity = \ {(yes x) -> refl ; no -> refl}
                     ; composition = \
                        { (yes f) (yes g) (yes x) -> refl
                        ; (yes f) (yes g) no -> refl
                        ; (yes x) no mx -> refl
                        ; no mg mx -> refl
                        }
                     ; homomorphism = \ f x -> refl
                     ; interchange = \ { (yes f) y -> refl ; no y → refl }
                     }

open Applicative maybeApplicative public

cond : Nat -> Nat -> Nat -> Nat
cond zero t e = e
cond (suc c) t e = t

_>>=_ : forall {X Y} -> Maybe X -> (X -> Maybe Y) -> Maybe Y
yes x >>= x2my = x2my x
no >>= x2my = no

eval : Hutton -> Maybe Nat
eval (val x) = pure x
eval (h +H h') = pure _+N_ <*> eval h <*> eval h'
eval (hif c then t else e)
  -- = pure cond <*> eval c <*> eval t <*> eval e  -- oops
  = eval c >>= \ { zero -> eval e
                 ; (suc _) -> eval t}
eval fail = no

foo : Hutton
foo = hif val 1 then (val 2 +H val 3) else (hif val 0 then val 4 else val 6)

goo : Hutton
goo = hif val 1 then (val 2 +H val 3) else (hif val 0 then fail else val 6)

ap : forall {X Y} -> Maybe (X -> Y) -> Maybe X -> Maybe Y
ap mf mx = mf >>= \ f -> mx >>= \ x -> yes (f x)


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn.Inference.Separator(x : X) where
  import OutsideIn.Constraints as C
  open C(x)
  open X(x)
  open import Data.List hiding (map)

  mutual
    data SeparatedConstraint (n : Set) : Shape → Set where
      SC : ∀ {s} → QConstraint n → Implications n s → SeparatedConstraint n s
    data Implications (n : Set) : Shape → Set where
      imp-ε : Implications n Nullary
      imp : ∀ {s} → Implication (λ n → SeparatedConstraint n s) n → Implications n (Unary s)
      _imp-∧_ : ∀ {s₁ s₂} →  Implications n s₁ → Implications n s₂ →  Implications n (Binary s₁ s₂)

  mutual
    data _simpl:_ {n : Set} : Constraint n Flat → QConstraint n → Set where
       Simpl-QC : ∀ {c} → QC c simpl: c
       Simpl-∧  : ∀ {a b}{a′ b′} → a simpl: a′ → b simpl: b′ → (a ∧′ b) simpl: (a′ ∧ b′)
       Simpl-Imp : ∀ {i} → Imp i simpl: ε
    data _separate:_,_ {n : Set} : Constraint n Flat → (r : Shape) → SeparatedConstraint n r → Set where
       Separate : ∀ {C}{Q}{r}{I} → C simpl: Q → C implic: r , I → C separate: r , SC Q I
    data _implic:_,_ {n : Set} : Constraint n Flat → (r : Shape) → Implications n r → Set where
       Implic-Qc : ∀ {c} → QC c implic: Nullary , imp-ε
       Implic-∧ : ∀{a b}{r₁ r₂}{a′}{b′} → a implic: r₁ , a′ → b implic: r₂ , b′ → (a ∧′ b) implic: Binary r₁ r₂ , (a′ imp-∧ b′)
       Implic-I : ∀{n}{Q}{C}{s}{v} → C separate: s , v → Imp (∃ n · Q ⊃ C) implic: Unary s , imp (∃ n · Q ⊃ v)

  simpl : ∀ {n} → (C : Constraint n Flat) → ∃ (λ Q → C simpl: Q)
  simpl (QC c) = _ , Simpl-QC
  simpl (a ∧′ b) with simpl a | simpl b
  ... | q₁ , p₁ | q₂ , p₂ = _ , Simpl-∧ p₁ p₂
  simpl (Imp _) = _ , Simpl-Imp

  separate : ∀ {n} → (C : Constraint n Flat) → ∃ (λ r → ∃ (λ S → C separate: r , S))
  implic : ∀ {n} → (C : Constraint n Flat) → ∃ (λ r → ∃ (λ I →  C implic: r , I ))
  separate c with implic c | simpl c
  ... | s , v , p | q , p′ = _ , _ , Separate p′ p
  implic (QC c) = _ , _ , Implic-Qc
  implic (a ∧′ b) with implic a | implic b
  ... | s , v , p | s′ , v′ , p′ = _ , _ , Implic-∧ p p′
  implic (Imp (∃ n · Q ⊃ C)) with separate C
  ... | s , v , p = _ , _ , Implic-I p

  -- Substitution for separated constraints
  substituteSep : ∀ {s}{a b} → (a → Type b) → SeparatedConstraint a s → SeparatedConstraint b s
  substituteImp : ∀ {s}{a b} → (a → Type b) → Implications a s → Implications b s
  substituteSep f (SC qc imps) = SC (qc-substitute f qc) (substituteImp f imps)
    where open Monad (type-is-monad)
          open Functor (type-is-functor)
  substituteImp f (imp-ε) = imp-ε
  substituteImp {Unary s} f (imp (∃ n · Q ⊃ C)) = imp (∃ n · constraint-types (join ∘ map f) Q
                                                           ⊃ substituteSep f′ C)
    where module PlusN-f = Functor (Monad.is-functor (PlusN-is-monad {n}))
          open Monad (type-is-monad)
          open Functor (type-is-functor)
          f′ = sequence-PlusN {n = n} ⦃ type-is-monad ⦄ ∘ PlusN-f.map f

  substituteImp f (a imp-∧ b) = substituteImp f a imp-∧ substituteImp f b

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
-- submitted by Nisse, 2011-06-21
module Issue423 where

------------------------------------------------------------------------
-- Prelude

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

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

-- Andreas: changed lhs variables to lambda-abstractions
-- This should be done automatically (internally).
curry : {A C : Set} {B : A → Set} →
        (Σ A B → C) → ((x : A) → B x → C)
curry f = \ x y -> f (x , y)

uncurry : {A C : Set} {B : A → Set} →
          ((x : A) → (y : B x) → C) → (Σ A B → C)
uncurry f = \ p -> f (Σ.proj₁ p) (Σ.proj₂ p)

------------------------------------------------------------------------
-- Preliminaries

postulate
  U  : Set
  El : U → Set

mutual

  data Ctxt : Set where
    _▻_ : (Γ : Ctxt) (σ : Type Γ) → Ctxt

  Type : Ctxt → Set
  Type Γ = Env Γ → U

  Env : Ctxt → Set
  Env (Γ ▻ σ) = Σ (Env Γ) λ γ → El (σ γ)

postulate
  Γ : Ctxt
  σ : Type Γ

------------------------------------------------------------------------
-- Problem

-- The following equality holds definitionally.

equal : (τ : (γ : Env Γ) → El (σ γ) → U) →
        curry (uncurry τ) ≡ τ
equal τ = refl

-- Bug was:
-- However, the two sides behave differently.

works : (τ₁ τ₂ : (γ : Env Γ) → El (σ γ) → U) →
        τ₁ ≡ τ₂ → Set₁
works τ .τ refl = Set

works′ : (τ₁ τ₂ : (γ : Env Γ) → El (σ γ) → U) →
         curry (uncurry τ₁) ≡ τ₂ → Set₁
works′ τ .τ refl = Set

fails : (τ₁ τ₂ : (γ : Env Γ) → El (σ γ) → U) →
        τ₁ ≡ curry (uncurry τ₂) → Set₁
fails τ .τ refl = Set

fails′ : (τ₁ τ₂ : (γ : Env Γ) → El (σ γ) → U) →
         curry (uncurry τ₁) ≡ curry (uncurry τ₂) → Set₁
fails′ τ .τ refl = Set

-- Bug was:
-- I find it interesting that works′ works, whereas the symmetric
-- variant fails fails.

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Oscar.Category.Category where

open import Oscar.Category.Setoid
open import Oscar.Category.Semigroupoid
open import Oscar.Level

module _
  {𝔬 𝔪 𝔮}
  (semigroupoid : Semigroupoid 𝔬 𝔪 𝔮)
  where
  open Semigroupoid semigroupoid

  record IsCategory (ε : ∀ {x} → x ↦ x) : Set (𝔬 ⊔ 𝔪 ⊔ 𝔮) where
    instance _ = IsSetoid↦
    field
      left-identity : ∀ {x y} (f : x ↦ y) → ε ∙ f ≋ f
      right-identity : ∀ {x y} (f : x ↦ y) → f ∙ ε ≋ f

open IsCategory ⦃ … ⦄ public

record Category 𝔬 𝔪 𝔮 : Set (lsuc (𝔬 ⊔ 𝔪 ⊔ 𝔮)) where
  constructor _,_
  field
    semigroupoid : Semigroupoid 𝔬 𝔪 𝔮
  open Semigroupoid semigroupoid public

  field
    ε : ∀ {x} → x ↦ x
    ⦃ isCategory ⦄ : IsCategory semigroupoid ε
  open IsCategory isCategory public


text:
module Diff where

open import Data.Nat using (ℕ; zero; suc)
open import Data.Float
open import Function using (_∘_)

postulate
  post : ∀ {a} {A : Set a} → A

-- Need to generalize for bilinear forms
data _Is_DiffAt_ (f : Float → Float) : ℕ → Float → Set where
  continuous : ∀ x → f Is zero DiffAt x
  d : ∀ f' {n} x → f' Is n DiffAt x → f Is suc n DiffAt x

data D (A : Set) : ℕ → A → Set where

-- +-diff : ∀ {x} {n} → HasDeriv (x +_) n
-- +-diff {x} {zero} = d⁰
-- +-diff {x} {suc n} = d (x +_) (+-diff {x} {n})

instance
  chain : ∀ {f g n x} → ⦃ f Is n DiffAt x ⦄ → ⦃ g Is n DiffAt g x ⦄ → (f ∘ g) Is n DiffAt x
  chain = post

  -‿diff : ∀ {n x} → -_ Is n DiffAt x
  -‿diff {zero} {x} = continuous x
  -‿diff {suc n} {x} = d -_ x -‿diff

  exp-diff : ∀ {n x} → e^_ Is n DiffAt x
  exp-diff {zero} {x} = continuous x
  exp-diff {suc n} {x} = d e^_ x exp-diff

  mutual
    sin-diff : ∀ {n x} → sin Is n DiffAt x
    sin-diff {zero} {x} = continuous x
    sin-diff {suc n} {x} = d cos x cos-diff

    cos-diff : ∀ {n x} → cos Is n DiffAt x
    cos-diff {zero} {x} = continuous x
    cos-diff {suc n} {x} = d (-_ ∘ sin) x (chain { -_} {sin}) -- (chain -_ sin)

∂ : ∀ f x → ⦃ f Is 1 DiffAt x ⦄ → Float
∂ f x ⦃ d f' x _ ⦄ = f' x

syntax ∂ (λ x → fx) y = ∂ fx /∂ x at y

test : Float → Float
test y = ∂ (cos (e^ x)) /∂ x at y

-- -- run : (∀ {n} → F₁) → F₁
-- -- run f x = f {zero} x

max_stars_repo_name: cspollard/diff

max_issues_repo_name: cspollard/diff

max_forks_repo_name: cspollard/diff


text:
-- New NO_POSITIVITY_CHECK pragma for data definitions and mutual
-- blocks

-- Skipping an old-style mutual block: Before the `mutual` keyword.
{-# NO_POSITIVITY_CHECK #-}
mutual
  data Cheat : Set where
    cheat : Oops → Cheat

  data Oops : Set where
    oops : (Cheat → Cheat) → Oops

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The free monad construction on indexed containers
------------------------------------------------------------------------

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

module Data.Container.Indexed.FreeMonad where

open import Level
open import Function hiding (const)
open import Category.Monad.Predicate
open import Data.Container.Indexed
open import Data.Container.Indexed.Combinator hiding (id; _∘_)
open import Data.Empty
open import Data.Sum using (inj₁; inj₂)
open import Data.Product
open import Data.W.Indexed
open import Relation.Unary
open import Relation.Unary.PredicateTransformer
open import Relation.Binary.PropositionalEquality

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

infixl 9 _⋆C_
infix  9 _⋆_

_⋆C_ : ∀ {i o c r} {I : Set i} {O : Set o} →
       Container I O c r → Pred O c → Container I O _ _
C ⋆C X = const X ⊎ C

_⋆_ : ∀ {ℓ} {O : Set ℓ} → Container O O ℓ ℓ → Pt O ℓ
C ⋆ X = μ (C ⋆C X)

pattern returnP x = (inj₁ x , _)
pattern doP c k   = (inj₂ c , k)

inn : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {X} →
      ⟦ C ⟧ (C ⋆ X) ⊆ C ⋆ X
inn (c , k) = sup (doP c k)

rawPMonad : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} →
            RawPMonad {ℓ = ℓ} (_⋆_ C)
rawPMonad {C = C} = record
  { return? = return
  ; _=<?_  = _=<<_
  }
  where
  return : ∀ {X} → X ⊆ C ⋆ X
  return x = sup (inj₁ x , ⊥-elim ∘ lower)

  _=<<_ : ∀ {X Y} → X ⊆ C ⋆ Y → C ⋆ X ⊆ C ⋆ Y
  f =<< sup (returnP x) = f x
  f =<< sup (doP c k)   = inn (c , λ r → f =<< k r)

leaf : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {X : Pred O ℓ} →
       ⟦ C ⟧ X ⊆ C ⋆ X
leaf (c , k) = inn (c , return? ∘ k)
  where
  open RawPMonad rawPMonad

generic : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {o}
          (c : Command C o) →
          o ∈ C ⋆ (⋃[ r ∶ Response C c ] ｛ next C c r ｝)
generic c = inn (c , λ r → return? (r , refl))
  where
  open RawPMonad rawPMonad


text:
module _ where

open import Agda.Builtin.Nat

postulate
  T : Set

  C₁ : Set
  instance I₁ : C₁

  C₂ : Nat → Set
  instance I₂ : ∀ {n} → C₂ n

it : {A : Set} {{_ : A}} → A
it {{x}} = x

postulate
  f₁ : {{_ : Nat → C₁}} → T
  f₂ : {{_ : ∀ n → C₂ n}} → T

works₁ : T
works₁ = f₁         -- f₁ {{λ _ → I₁}}

fails₁ : T
fails₁ = f₁ {{it}}  -- internal error

works₂ : T
works₂ = f₂         -- f₂ {{λ n → I₂ {n}}}

fails₂ : T
fails₂ = f₂ {{it}}  -- internal error

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module UniDB.Subst.Pair where

open import UniDB.Subst.Core
open import UniDB.Morph.Pair

instance
  iLkPair :
    {T : STX} {{apTT : Ap T T}}
    {Ξ : MOR} {{lkTΞ : Lk T Ξ}}
    {Ζ : MOR} {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}} →
    Lk T (Pair Ξ Ζ)
  lk {{iLkPair {T}}} (ξ ⊗ ζ) i = ap {T} ζ (lk {T} ξ i)

  iLkRenPair :
    {T : STX} {{vrT : Vr T}} {{apTT : Ap T T}} {{apVrT : ApVr T}}
    {Ξ : MOR} {{lkIxΞ : Lk Ix Ξ}} {{lkTΞ : Lk T Ξ}} {{lkRenTΞ : LkRen T Ξ}}
    {Ζ : MOR} {{lkIxΖ : Lk Ix Ζ}} {{lkTΖ : Lk T Ζ}} {{lkRenTΖ : LkRen T Ζ}} {{upΖ : Up Ζ}} →
    LkRen T (Pair Ξ Ζ)
  lk-ren {{iLkRenPair {T} {Ξ} {Ζ}}} (ξ ⊗ ζ) i = begin
    ap {T} ζ (lk {T} ξ i)        ≡⟨ cong (ap {T} ζ) (lk-ren {T} ξ i) ⟩
    ap {T} ζ (vr (lk {Ix} ξ i))  ≡⟨ ap-vr {T} ζ (lk {Ix} ξ i) ⟩
    lk {T} ζ (lk {Ix} ξ i)       ≡⟨ lk-ren {T} ζ (lk {Ix} ξ i) ⟩
    vr (lk {Ix} ζ (lk {Ix} ξ i)) ∎

  iLkHCompPair :
    {T : STX} {{vrT : Vr T}} {{apTT : Ap T T}}
    {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
    {Ζ : MOR} {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}} →
    LkHCompAp T Ξ Ζ (Pair Ξ Ζ)
  lk-⊡-ap {{iLkHCompPair}} ξ ζ i = refl

iLkUpPairRenaming :
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}} {{apVrT : ApVr T}}
  (Ξ : MOR) {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{lkUpTΞ : LkUp T Ξ}}
  {{lkIxΞ : Lk Ix Ξ}} {{lkRenTΞ : LkRen T Ξ}} {{lkUpIxΞ : LkUp Ix Ξ}}
  (Ζ : MOR) {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}} {{lkUpTΖ : LkUp T Ζ}} →
  LkUp T (Pair Ξ Ζ)
lk-↑₁-zero {{iLkUpPairRenaming T Ξ Ζ}} (ξ ⊗ ζ) = begin
  ap {T} (ζ ↑₁) (lk {T} (ξ ↑₁) zero)     ≡⟨ cong (ap {T} (ζ ↑₁)) (lk-↑₁-zero ξ) ⟩
  ap {T} (ζ ↑₁) (vr zero)                ≡⟨ ap-vr {T} (ζ ↑₁) zero ⟩
  lk (ζ ↑₁) zero                         ≡⟨ lk-↑₁-zero ζ ⟩
  vr zero                                ∎
lk-↑₁-suc {{iLkUpPairRenaming T Ξ Ζ}} (ξ ⊗ ζ) i = begin
  ap {T} (ζ ↑₁) (lk (ξ ↑₁) (suc i))      ≡⟨ cong (ap {T} (ζ ↑₁)) (lk-ren (ξ ↑₁) (suc i)) ⟩
  ap {T} (ζ ↑₁) (vr (lk (ξ ↑₁) (suc i))) ≡⟨ ap-vr {T} (ζ ↑₁) (lk (ξ ↑₁) (suc i)) ⟩
  lk (ζ ↑₁) (lk (ξ ↑₁) (suc i))          ≡⟨ cong (lk (_↑₁ ζ)) (lk-↑₁-suc ξ i) ⟩
  lk (ζ ↑₁) (suc (lk ξ i))               ≡⟨ lk-↑₁-suc ζ (lk ξ i) ⟩
  wk₁ (lk ζ (lk ξ i))                    ≡⟨ cong wk₁ (sym (ap-vr {T} ζ (lk ξ i))) ⟩
  wk₁ (ap {T} ζ (vr (lk ξ i)))           ≡⟨ cong wk₁ (cong (ap {T} ζ) (sym (lk-ren ξ i))) ⟩
  wk₁ (ap {T} ζ (lk ξ i))                ∎

iLkUpPairSubstitution :
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}} {{apVrT : ApVr T}}
  (Ξ : MOR) {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{lkUpTΞ : LkUp T Ξ}}
  (Ζ : MOR) {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}} {{lkUpTΖ : LkUp T Ζ}}
  (ap-wk₁-TΖ : {γ₁ γ₂ : Dom} (ζ : Ζ γ₁ γ₂) (t : T γ₁) →
    ap {T} (ζ ↑₁) (wk₁ t) ≡ wk₁ (ap {T} ζ t)) →
  LkUp T (Pair Ξ Ζ)
lk-↑₁-zero {{iLkUpPairSubstitution T Ξ Ζ ap-wk₁-TΖ}} (ξ ⊗ ζ) = begin
  ap {T} (ζ ↑₁) (lk (ξ ↑₁) zero) ≡⟨ cong (ap {T} (ζ ↑₁)) (lk-↑₁-zero ξ) ⟩
  ap {T} (ζ ↑₁) (vr zero)        ≡⟨ ap-vr {T} (ζ ↑₁) zero ⟩
  lk (ζ ↑₁) zero                 ≡⟨ lk-↑₁-zero  ζ ⟩
  vr zero                        ∎
lk-↑₁-suc {{iLkUpPairSubstitution T Ξ Ζ ap-wk₁-TΖ}} (ξ ⊗ ζ) i = begin
  ap {T} (ζ ↑₁) (lk (ξ ↑₁) (suc i)) ≡⟨ cong (ap {T} (ζ ↑₁)) (lk-↑₁-suc ξ i) ⟩
  ap {T} (ζ ↑₁) (wk₁ (lk ξ i))      ≡⟨ ap-wk₁-TΖ ζ (lk ξ i) ⟩
  wk₁ (ap {T} ζ (lk ξ i))           ∎

instance
  iLkUpPair :
    {T : STX} {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}}
    {{apVrT : ApVr T}} {{apWkTT : ApWk T T}}
    {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{lkUpTΞ : LkUp T Ξ}}
    {Ζ : MOR} {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}} {{lkUpTΖ : LkUp T Ζ}} →
    LkUp T (Pair Ξ Ζ)
  iLkUpPair {T} {Ξ} {Ζ} = iLkUpPairSubstitution T Ξ Ζ (ap-wk₁ {T})

record ApPair (T : STX) {{apTT : Ap T T}} (X : STX) {{apTX : Ap T X}} : Set₁ where
  field
    ap-pair :
      {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
      {Ζ : MOR} {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}}
      {γ₁ γ₂ γ₃ : Dom} (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₂ γ₃)
      (x : X γ₁) →
        ap {T} (ξ ⊗ ζ) x ≡ ap {T} ζ (ap {T} ξ x)
open ApPair {{...}} public

instance
  iApPairIxIx : ApPair Ix Ix
  ap-pair {{iApPairIxIx}} {Ξ} ξ ζ i = refl

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
-- This file is the source Agda file
-- Edit this file not Common.hs
-- The warning below will be written to Common.hs

{- Description : Property based testing Name Utilities

This file contains various naming related utilities used for
generating Zerepoch Core types and terms.

-}

module ZerepochCore.Generators.NEAT.Common where

-- warning to be written to Haskell file:
{-# FOREIGN AGDA2HS
{-
!!! THIS FILE IS GENERATED FROM Common.agda
!!! DO NOT EDIT THIS FILE. EDIT Common.agda
!!! AND THEN RUN agda2hs ON IT.
-}
#-}

{-# FOREIGN AGDA2HS

{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE EmptyDataDeriving   #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE ScopedTypeVariables #-}

import           Control.Enumerable
import qualified Data.Stream               as Stream
import qualified Data.Text                 as Text
import           ZerepochCore.Name  (Name, TyName (..))
import           ZerepochCore.Quote (MonadQuote (..), freshName)
#-}
-- * Enumerating deBruijn indices

-- empty type
data Z : Set where

{-# COMPILE AGDA2HS Z deriving (Eq, Ord, Show) #-}

-- maybe type
data S (n : Set) : Set where
  FZ : S n
  FS : n → S n

{-# COMPILE AGDA2HS S deriving (Eq, Ord, Show, Functor) #-}

{-# FOREIGN AGDA2HS
instance Enumerable Z where
  enumerate = datatype []

instance Enumerable n => Enumerable (S n) where
  enumerate = share $ aconcat
    [ c0 FZ
    , c1 FS
    ]

-- |Absurd for the zero type.
fromZ :: Z -> a
fromZ i = case i of {}

-- * Namespaces

data NameState n = NameState { nameOf :: n -> Name, freshNameStrings :: Stream.Stream Text.Text }

newtype TyNameState n = TyNameState (NameState n)

tynameOf :: TyNameState n -> n -> TyName
tynameOf (TyNameState NameState{..}) i = TyName (nameOf i)

-- |Create an empty name state from a stream of text names.
emptyNameState :: Stream.Stream Text.Text -> NameState Z
emptyNameState strs = NameState { nameOf = fromZ, freshNameStrings = strs }

-- |Extend name state with a fresh name.
extNameState
  :: (MonadQuote m)
  => NameState n
  -> m (NameState (S n))
extNameState NameState{..} = liftQuote $ do
  let str = Stream.head freshNameStrings
      freshNameStrings' = Stream.tail freshNameStrings
  name <- freshName str
  let nameOf' FZ     = name
      nameOf' (FS i) = nameOf i
  return NameState { nameOf = nameOf', freshNameStrings = freshNameStrings' }

-- |Create an empty name state from a stream of text names.
emptyTyNameState :: Stream.Stream Text.Text -> TyNameState Z
emptyTyNameState strs = TyNameState (emptyNameState strs)

-- |Extend type name state with a fresh type name.
extTyNameState
  :: (MonadQuote m)
  => TyNameState n
  -> m (TyNameState (S n))
extTyNameState (TyNameState nameState) =
  TyNameState <$> extNameState nameState

-- |Create a stream of names |x0, x1, x2, ...| from a prefix |"x"|
mkTextNameStream :: Text.Text -> Stream.Stream Text.Text
mkTextNameStream prefix =
  Stream.map
    (\n -> prefix <> Text.pack (show n))
    (Stream.iterate (+1) (0 :: Integer))
#-}

max_stars_repo_name: Quantum-One-DLT/zerepoch

max_issues_repo_name: Quantum-One-DLT/zerepoch

max_forks_repo_name: Quantum-One-DLT/zerepoch


text:
-- AIM XXXV, 2022-05-06, issue #5891:
-- SizeUniv : SizeUniv was causing non-termination and inhabitation of Size< 0.
-- This is inconsistent; proof by Jonathan Chan.

{-# OPTIONS --sized-types #-}

open import Agda.Primitive
open import Agda.Builtin.Size

data ⊥ : Set where

-- Original exploit:
-- data False : SizeUniv where

False : SizeUniv
False = (X : SizeUniv) → X

-- Should fail.

-- Expected error:
-- Setω != SizeUniv
-- when checking that the expression (X : SizeUniv) → X has type SizeUniv

-- Step 1: Hurken's Paradox with SizeUniv : SizeUniv.

℘ : SizeUniv → SizeUniv
℘ S = S → SizeUniv

U : SizeUniv
U = ∀ (X : SizeUniv) → (℘ (℘ X) → X) → ℘ (℘ X)

τ : ℘ (℘ U) → U
τ t = λ X f p → t (λ x → p (f (x X f)))

σ : U → ℘ (℘ U)
σ s = s U τ

Δ : ℘ U
Δ y = (∀ p → σ y p → p (τ (σ y))) → False

Ω : U
Ω = τ (λ p → (∀ x → σ x p → p x))

R : ∀ p → (∀ x → σ x p → p x) → p Ω
R _ 𝟙 = 𝟙 Ω (λ x → 𝟙 (τ (σ x)))

M : ∀ x → σ x Δ → Δ x
M _ 𝟚 𝟛 = 𝟛 Δ 𝟚 (λ p → 𝟛 (λ y → p (τ (σ y))))

L : (∀ p → (∀ x → σ x p → p x) → p Ω) → False
L 𝟘 = 𝟘 Δ M (λ p → 𝟘 (λ y → p (τ (σ y))))

-- Prevent unfolding, as this term has no whnf.
-- Stops Agda from looping.

abstract
  false : False
  false = L R

-- This gives us a predecessor on Size.

size-pred : ∀ i → Size< i
size-pred i = false (Size< i)

-- Step 2: Size predecessor is inconsistent.

-- Jonathan Chan:
-- I managed to do so using ∞ but only because it's the only closed
-- size expression, not using the ∞ < ∞ property, although the
-- principle is the same as for #3026:

data _>_ (s : Size) : Size → Set where
  lt : (r : Size< s) → s > r

data Acc (s : Size) : Set where
  acc : (∀ {r} → s > r → Acc r) → Acc s

wf : ∀ s → Acc s
wf s = acc λ{ (lt r) → wf r }

¬wf : ∀ s → Acc s → ⊥
¬wf s (acc p) = ¬wf (size-pred s) (p (lt (size-pred s)))

absurd : ⊥
absurd = (¬wf ∞) (wf ∞)


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

module Demos.Live where

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Issue784.RefAPI where

open import Issue784.Values public hiding (seq)
open import Issue784.Context -- that should be private
open import Issue784.Transformer public

open import Data.List public using (List; []; _∷_; [_])
open import Data.Nat
open import Relation.Binary.PropositionalEquality.TrustMe

private
  postulate
    _seq_ : ∀ {a b} {A : Set a} {B : Set b} → A → B → B

    nativeRef : (A : Set) → Set
    -- create new reference and initialize it with passed value
    nativeNew-ℕ : ℕ → nativeRef ℕ
    -- increment value in place
    nativeInc-ℕ : nativeRef ℕ → Unit
    nativeGet-ℕ : nativeRef ℕ → ℕ
    nativeFree-ℕ : nativeRef ℕ → Unit

data Exact {ℓ} {A : Set ℓ} : A → Set ℓ where
  exact : ∀ a → Exact a

getExact : ∀ {ℓ} {A : Set ℓ} {a : A} → Exact a → A
getExact (exact a) = a

≡-exact : ∀ {ℓ} {A : Set ℓ} {a : A} (e : Exact a) → getExact e ≡ a
≡-exact (exact a) = refl

Ref-ℕ : ℕ → Set
Ref-ℕ a = Σ[ native ∈ nativeRef ℕ ] nativeGet-ℕ native ≡ a

private
  -- making these private to avoid further using
  -- which may lead to inconsistency
  proofNew-ℕ : ∀ a → Ref-ℕ a
  proofNew-ℕ a = nativeNew-ℕ a , trustMe

  proofInc-ℕ : ∀ {a} → Ref-ℕ a → Ref-ℕ (suc a)
  proofInc-ℕ (r , _) = (nativeInc-ℕ r) seq (r , trustMe)

  proofGet-ℕ : ∀ {a} → Ref-ℕ a → Exact a
  proofGet-ℕ (r , p) = ≡-elim′ Exact p (exact $ nativeGet-ℕ r)

  proofFree-ℕ : {a : ℕ} → Ref-ℕ a → Unit
  proofFree-ℕ (r , _) = nativeFree-ℕ r

new-ℕ : ∀ a n → Transformer! [] [(n , Unique (Ref-ℕ a))]
new-ℕ a n ctx nr-v []⊆v nr-v∪n = context w , (≡⇒≋ $ ≡-trans p₁ p₂) where
    v = Context.get ctx
    w = v ∪ [(n , Unique (Ref-ℕ a) , unique (proofNew-ℕ a))]
    p₁ : types (v ∪ [(n , Unique (Ref-ℕ a) , _)]) ≡ types v ∪ [(n , Unique (Ref-ℕ a))]
    p₁ = t-x∪y v [(n , Unique (Ref-ℕ a) , _)]
    p₂ : types v ∪ [(n , Unique (Ref-ℕ a))] ≡ types v ∖∖ [] ∪ [(n , Unique (Ref-ℕ a))]
    p₂ = ≡-cong (λ x → x ∪ [(n , Unique (Ref-ℕ a))]) (≡-sym $ t∖[]≡t $ types v)

inc-ℕ : ∀ {a} n → Transformer! [(n , Unique (Ref-ℕ a))] [(n , Unique (Ref-ℕ (suc a)))]
inc-ℕ {a} n ctx nr-v n⊆v nr-v∪n = context w , (≡⇒≋ $ ≡-trans p₁ p₂) where
    v = Context.get ctx
    r = unique ∘ proofInc-ℕ ∘ Unique.get ∘ getBySignature ∘ n⊆v $ here refl
    w = v ∖∖ [ n ] ∪ [(n , Unique (Ref-ℕ $ suc a) , r)]
    p₁ : types (v ∖∖ [ n ] ∪ [(n , Unique (Ref-ℕ $ suc a) , r)]) ≡ types (v ∖∖ [ n ]) ∪ [(n , Unique (Ref-ℕ $ suc _))]
    p₁ = t-x∪y (v ∖∖ [ n ]) _
    p₂ : types (v ∖∖ [ n ]) ∪ [(n , Unique (Ref-ℕ $ suc a))] ≡ types v ∖∖ [ n ] ∪ [(n , Unique (Ref-ℕ $ suc _))]
    p₂ = ≡-cong (λ x → x ∪ [(n , Unique (Ref-ℕ $ suc a))]) (t-x∖y v [ n ])

get-ℕ : (r n : String) {r≢!n : r s-≢! n} {a : ℕ} →
    Transformer ([(r , Unique (Ref-ℕ a))] , nr-[a]) ((r , Unique (Ref-ℕ a)) ∷ [(n , Pure (Exact a))] , (x≢y⇒x∉l⇒x∉y∷l (s-≢!⇒≢? r≢!n) λ()) ∷ nr-[a])
get-ℕ r n {a = a} ctx nr-v h⊆v _ = context w , ≋-trans p₁ (≋-trans p₂ p₃) where
    v = Context.get ctx
    pr : Pure (Exact a)
    pr = pure ∘ proofGet-ℕ ∘ Unique.get ∘ getBySignature ∘ h⊆v $ here refl
    w = v ∪ [(n , Pure (Exact a) , pr)]
    p₁ : types (v ∪ [(n , Pure (Exact a) , pr)]) ≋ types v ∪ [(n , Pure (Exact a))]
    p₁ = ≡⇒≋ $ t-x∪y v [(n , Pure (Exact a) , pr)]
    p₂ : types v ∪ [(n , Pure (Exact a))] ≋ (types v ∖∖ [ r ] ∪ [(r , Unique (Ref-ℕ _))]) ∪ [(n , Pure (Exact a))]
    p₂ = x≋x̀⇒x∪y≋x̀∪y (≋-trans g₁ g₂) [(n , Pure (Exact a))] where
        g₁ : types v ≋ [(r , Unique (Ref-ℕ _))] ∪ types v ∖∖ [ r ]
        g₁ = t₁⊆t₂⇒t₂≋t₁∪t₂∖nt₁ nr-[a] (nr-x⇒nr-t-x nr-v) h⊆v
        g₂ : [(r , Unique (Ref-ℕ _))] ∪ types v ∖∖ [ r ] ≋ types v ∖∖ [ r ] ∪ [(r , Unique (Ref-ℕ _))]
        g₂ = ∪-sym [(r , Unique (Ref-ℕ _))] (types v ∖∖ [ r ])
    p₃ : (types v ∖∖ [ r ] ∪ [(r , Unique (Ref-ℕ a))]) ∪ [(n , Pure (Exact a))] ≋ types v ∖∖ [ r ] ∪ ((r , Unique (Ref-ℕ _)) ∷ [(n , Pure (Exact a))])
    p₃ = ≡⇒≋ $ ∪-assoc (types v ∖∖ [ r ]) [(r , Unique (Ref-ℕ _))] [(n , Pure (Exact a))]

free-ℕ : (h : String) {a : ℕ} → Transformer! [(h , Unique (Ref-ℕ a))] []
free-ℕ h ctx nr-v h⊆v _ = u seq (context w , ≡⇒≋ p) where
    v = Context.get ctx
    u = proofFree-ℕ ∘ Unique.get ∘ getBySignature ∘ h⊆v $ here refl
    w = v ∖∖ [ h ]
    p : types (v ∖∖ [ h ]) ≡ types v ∖∖ [ h ] ∪ []
    p = ≡-trans (t-x∖y v [ h ]) (≡-sym $ x∪[]≡x (types v ∖∖ [ h ]))


text:
------------------------------------------------------------------------------
-- Properties for the bisimilarity relation
------------------------------------------------------------------------------

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

module FOTC.Relation.Binary.Bisimilarity.PropertiesI where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.List.PropertiesI
open import FOTC.Base.PropertiesI
open import FOTC.Data.Stream.Type
open import FOTC.Relation.Binary.Bisimilarity.Type

------------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, the
-- bisimilarity relation _≈_ on unbounded lists is also a pre-fixed
-- point of the bisimulation functional (see
-- FOTC.Relation.Binary.Bisimulation).
≈-in : ∀ {xs ys} →
       ∃[ x' ]  ∃[ xs' ] ∃[ ys' ]
         xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys' ∧ xs' ≈ ys' →
       xs ≈ ys
≈-in h = ≈-coind B h' h
  where
  B : D → D → Set
  B xs ys = ∃[ x' ]  ∃[ xs' ] ∃[ ys' ]
              xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys' ∧ xs' ≈ ys'

  h' : ∀ {xs} {ys} → B xs ys →
       ∃[ x' ] ∃[ xs' ] ∃[ ys' ] xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys' ∧ B xs' ys'
  h' (x' , xs' , ys' , prf₁ , prf₂ , xs'≈ys') =
    x' , xs' , ys' , prf₁ , prf₂ , ≈-out xs'≈ys'

≈-refl : ∀ {xs} → Stream xs → xs ≈ xs
≈-refl {xs} Sxs = ≈-coind B h₁ h₂
  where
  B : D → D → Set
  B xs ys = Stream xs ∧ xs ≡ ys

  h₁ : ∀ {xs ys} → B xs ys →
       ∃[ x' ] ∃[ xs' ] ∃[ ys' ] xs ≡ x' ∷ xs' ∧ ys ≡ x' ∷ ys' ∧ B xs' ys'
  h₁ (Sxs , refl) with Stream-out Sxs
  ... | x' , xs' , prf , Sxs' =
    x' , xs' , xs' , prf , prf , (Sxs' , refl)

  h₂ : B xs xs
  h₂ = Sxs , refl

≈-sym : ∀ {xs ys} → xs ≈ ys → ys ≈ xs
≈-sym {xs} {ys} xs≈ys = ≈-coind B h₁ h₂
  where
  B : D → D → Set
  B xs ys = ys ≈ xs

  h₁ : ∀ {ys xs} → B ys xs →
       ∃[ y' ] ∃[ ys' ] ∃[ xs' ] ys ≡ y' ∷ ys' ∧ xs ≡ y' ∷ xs' ∧ B ys' xs'
  h₁ Bxsys with ≈-out Bxsys
  ... | y' , ys' , xs' , prf₁ , prf₂ , ys'≈xs' =
    y' , xs' , ys' , prf₂ , prf₁ , ys'≈xs'

  h₂ : B ys xs
  h₂ = xs≈ys

≈-trans : ∀ {xs ys zs} → xs ≈ ys → ys ≈ zs → xs ≈ zs
≈-trans {xs} {ys} {zs} xs≈ys ys≈zs = ≈-coind B h₁ h₂
  where
  B : D → D → Set
  B xs zs = ∃[ ys ] xs ≈ ys ∧ ys ≈ zs

  h₁ : ∀ {as} {cs} → B as cs →
       ∃[ a' ] ∃[ as' ] ∃[ cs' ] as ≡ a' ∷ as' ∧ cs ≡ a' ∷ cs' ∧ B as' cs'
  h₁ {cs = cs} (bs , as≈bs , bs≈cs) with ≈-out as≈bs
  ... | a' , as' , bs' , prf₁ , prf₂ , as'≈bs' with ≈-out bs≈cs
  ... | b' , bs'' , cs' , prf₃ , prf₄ , bs''≈cs' =
    a'
    , as'
    , cs'
    , prf₁
    , subst (λ t → cs ≡ t ∷ cs') b'≡a' prf₄
    , (bs' , as'≈bs' , subst (λ t → t ≈ cs') bs''≡bs' bs''≈cs')
    where
    b'≡a' : b' ≡ a'
    b'≡a' = ∧-proj₁ (∷-injective (trans (sym prf₃) prf₂))

    bs''≡bs' : bs'' ≡ bs'
    bs''≡bs' = ∧-proj₂ (∷-injective (trans (sym prf₃) prf₂))

  h₂ : B xs zs
  h₂ = ys , (xs≈ys , ys≈zs)

∷-injective≈ : ∀ {x xs ys} → x ∷ xs ≈ x ∷ ys → xs ≈ ys
∷-injective≈ {x} {xs} {ys} h with ≈-out h
... | x' , xs' , ys' , prf₁ , prf₂ , prf₃ = xs≈ys
  where
  xs≡xs' : xs ≡ xs'
  xs≡xs' = ∧-proj₂ (∷-injective prf₁)

  ys≡ys' : ys ≡ ys'
  ys≡ys' = ∧-proj₂ (∷-injective prf₂)

  xs≈ys : xs ≈ ys
  xs≈ys = subst (λ t → t ≈ ys)
                (sym xs≡xs')
                (subst (_≈_ xs') (sym ys≡ys') prf₃)

∷-rightCong≈ : ∀ {x xs ys} → xs ≈ ys → x ∷ xs ≈ x ∷ ys
∷-rightCong≈ {x} {xs} {ys} h = ≈-in (x , xs , ys , refl , refl , h)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Prelude

module Implicits.Substitutions.Type where

open import Implicits.Syntax.Type

open import Data.Fin.Substitution
open import Data.Star as Star hiding (map)
open import Data.Star.Properties
open import Data.Vec

module TypeApp {T} (l : Lift T Type) where
  open Lift l hiding (var)

  infixl 8 _/_

  mutual
    _simple/_ : ∀ {m n} → SimpleType m → Sub T m n → Type n
    tc c simple/ σ = simpl (tc c)
    tvar x simple/ σ = lift (lookup x σ)
    (a →' b) simple/ σ = simpl ((a / σ) →' (b / σ))

    _/_ : ∀ {m n} → Type m → Sub T m n → Type n
    (simpl c) / σ = (c simple/ σ)
    (a ⇒ b)  / σ = (a / σ) ⇒ (b / σ)
    (∀' a)   / σ = ∀' (a / σ ↑)

  open Application (record { _/_ = _/_ }) using (_/✶_)

  →'-/✶-↑✶ : ∀ k {m n a b} (ρs : Subs T m n) →
             (simpl (a →' b)) /✶ ρs ↑✶ k ≡ simpl ((a /✶ ρs ↑✶ k) →' (b /✶ ρs ↑✶ k))
  →'-/✶-↑✶ k ε        = refl
  →'-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (→'-/✶-↑✶ k ρs) refl

  ⇒-/✶-↑✶ : ∀ k {m n a b} (ρs : Subs T m n) →
             (a ⇒ b) /✶ ρs ↑✶ k ≡ (a /✶ ρs ↑✶ k) ⇒ (b /✶ ρs ↑✶ k)
  ⇒-/✶-↑✶ k ε        = refl
  ⇒-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (⇒-/✶-↑✶ k ρs) refl

  tc-/✶-↑✶ : ∀ k {c m n} (ρs : Subs T m n) →
             (simpl (tc c)) /✶ ρs ↑✶ k ≡ simpl (tc c)
  tc-/✶-↑✶ k ε        = refl
  tc-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (tc-/✶-↑✶ k ρs) refl

  ∀'-/✶-↑✶ : ∀ k {m n a} (ρs : Subs T m n) →
             (∀' a) /✶ ρs ↑✶ k ≡ ∀' (a /✶ ρs ↑✶ (suc k))
  ∀'-/✶-↑✶ k ε = refl
  ∀'-/✶-↑✶ k (x ◅ ρs) = cong₂ _/_ (∀'-/✶-↑✶ k ρs) refl

typeSubst : TermSubst Type
typeSubst = record { var = (λ n → simpl (tvar n)); app = TypeApp._/_ }

open TermSubst typeSubst public hiding (var)
open TypeApp termLift public using (_simple/_)
open TypeApp varLift public using () renaming (_simple/_ to _simple/Var_)

infix 8 _[/_]

-- Shorthand for single-variable type substitutions
_[/_] : ∀ {n} → Type (suc n) → Type n → Type n
a [/ b ] = a / sub b

-- shorthand for type application
infixl 8 _∙_
_∙_ : ∀ {ν} → (a : Type ν) → {is∀ : is-∀' a} → Type ν → Type ν
_∙_ (simpl (tvar n)) {is∀ = ()} _
_∙_ (simpl (tc c)) b = simpl (tc c)
_∙_ (simpl (_ →' _)) {is∀ = ()} _
_∙_ (∀' x) b = x [/ b ]
_∙_ (_ ⇒ _) {is∀ = ()} _

stp-weaken : ∀ {ν} → SimpleType ν → SimpleType (suc ν)
stp-weaken (tc x) = tc x
stp-weaken (tvar n) = tvar (suc n)
stp-weaken (a →' b) = weaken a →' weaken b


text:
module Thesis.SIRelBigStep.FundamentalProperty where

open import Data.Product
open import Relation.Binary.PropositionalEquality

open import Thesis.SIRelBigStep.IlcSILR

rfundamentalV3v : ∀ {Γ τ} (x : Var Γ τ) → (n : ℕ) → ∀ ρ1 dρ ρ2 (ρρ : rrelρ3 Γ ρ1 dρ ρ2 n) → rrelV3 τ (⟦ x ⟧Var ρ1) (D.⟦ x ⟧Var dρ) (⟦ x ⟧Var ρ2) n
rfundamentalV3v x n ρ1 dρ ρ2 ρρ = ⟦ x ⟧RelVar3 ρρ

rfundamental3constV : ∀ {τ} k (c : Const τ) →
  rrelV3 τ (eval-const c) (deval (derive-const c) ∅ ∅) (eval-const c) k
rfundamental3constV k (lit n) = refl

rfundamental3 : ∀ {τ Γ} k (t : Term Γ τ) → ∀ ρ1 dρ ρ2 → (ρρ : rrelρ3 Γ ρ1 dρ ρ2 k) →
  rrelT3 t (derive-dterm t) t ρ1 dρ ρ2 k

rfundamental3svv : ∀ {τ Γ} k (sv : SVal Γ τ) →
  ∀ ρ1 dρ ρ2 → (ρρ : rrelρ3 Γ ρ1 dρ ρ2 k) → rrelV3 τ (eval sv ρ1) (deval (derive-dsval sv) ρ1 dρ) (eval sv ρ2) k
rfundamental3svv k (var x) ρ1 dρ ρ2 ρρ = rfundamentalV3v x k ρ1 dρ ρ2 ρρ
rfundamental3svv k (cons sv1 sv2) ρ1 dρ ρ2 ρρ = rfundamental3svv k sv1 ρ1 dρ ρ2 ρρ , rfundamental3svv k sv2 ρ1 dρ ρ2 ρρ
rfundamental3svv k (const c) ρ1 dρ ρ2 ρρ rewrite deval-derive-const-inv c ρ1 dρ = rfundamental3constV k c
rfundamental3svv k (abs t) ρ1 dρ ρ2 ρρ = (refl , refl) , refl , rrelρ3→⊕ ρ1 dρ ρ2 ρρ , refl , refl ,
    λ j j<k v1 dv v2 vv →
    -- If we replace abs t by rec t, here we would need to invoke (by
    -- well-founded recursion) rfundamental3svv on (abs t) at a smaller j, as follows:
    --   rfundamental3svv j (abs t) ρ1 dρ ρ2 (rrelρ3-mono j k (lt1 j<k) _ _ _ _ ρρ)
    -- As you'd expect, Agda's termination checker does not accept that call directly.
      rfundamental3 j t (v1 • ρ1) (dv • dρ) (v2 • ρ2) (vv , rrelρ3-mono j k (lt1 j<k) _ _ _ _ ρρ)

rfundamental3sv : ∀ {τ Γ} k (sv : SVal Γ τ) →
  ∀ ρ1 dρ ρ2 → (ρρ : rrelρ3 Γ ρ1 dρ ρ2 k) → rrelT3 (val sv) (dval (derive-dsval sv)) (val sv) ρ1 dρ ρ2 k
rfundamental3sv k sv ρ1 dρ ρ2 ρρ .(eval sv ρ1) .(eval sv ρ2) .0 j<k (val .sv) (val .sv) = deval (derive-dsval sv) ρ1 dρ , dval (derive-dsval sv) , rfundamental3svv k sv ρ1 dρ ρ2 ρρ

open import Theorem.Groups-Nehemiah
rfundamental3primv : ∀ {σ τ} k p →
  ∀ v1 dv v2 → (vv : rrelV3 σ v1 dv v2 k) →
  rrelV3 τ (eval-primitive p v1) (deval-primitive p v1 dv) (eval-primitive p v2) k
rfundamental3primv k succ (natV n₁) (bang .(natV n)) (natV n) refl = refl
rfundamental3primv k succ (natV n) (dnatV dn) (natV .(dn + n)) refl = +-suc dn n
rfundamental3primv k add (pairV (natV a1) (natV b1))
  (dpairV (dnatV da) (dnatV db))
  (pairV (natV .(da + a1)) (natV .(db + b1)))
  (refl , refl) = ℕ-mn·pq=mp·nq {da} {db} {a1} {b1}
rfundamental3primv k add (pairV a1 b1)
  (dpairV (dnatV da) (bang b2))
  (pairV a2 .b2) (aa , refl) rewrite rrelV3→⊕ a1 (dnatV da) a2 aa = refl
rfundamental3primv k add (pairV a1 b1)
  (dpairV (bang a2) db)
  (pairV .a2 b2) (refl , bb) rewrite rrelV3→⊕ b1 db b2 bb = refl
rfundamental3primv k add (pairV a1 b1) (bang p2) .p2 refl = refl

-- Warning: names like ρ1⊢t1↓[j]v1 are all broken, sorry for not fixing them.
rfundamental3 k (val sv) = rfundamental3sv k sv
rfundamental3 (suc k) (primapp p sv) ρ1 dρ ρ2 ρρ
  .(eval-primitive p (eval sv ρ1)) .(eval-primitive p (eval sv ρ2)) .1 (s≤s j<k) (primapp .p .sv) (primapp .p .sv) =
   deval-primitive p (eval sv ρ1) (deval (derive-dsval sv) ρ1 dρ) , dprimapp p sv (derive-dsval sv) ,
     rfundamental3primv k p (eval sv ρ1) (deval (derive-dsval sv) ρ1 dρ) (eval sv ρ2)
       (rfundamental3svv k sv ρ1 dρ ρ2 (rrelρ3-mono k (suc k) (≤-step ≤-refl) _ ρ1 dρ ρ2 ρρ))

rfundamental3 (suc (suc k)) (app vs vt) ρ1 dρ ρ2 ρρ v1 v2 .(suc j) (s≤s (s≤s j<k))
  (app j vtv1 ρ1⊢t1↓[j]v1 ρ1⊢t1↓[j]v2 ρ1⊢t1↓[j]v3)
  (app n₁ vtv2 ρ2⊢t2↓[n2]v2 ρ2⊢t2↓[n2]v3 ρ2⊢t2↓[n2]v4)
  with rfundamental3sv (suc (suc k)) vs ρ1 dρ ρ2 ρρ _ _ zero (s≤s z≤n) ρ1⊢t1↓[j]v1 ρ2⊢t2↓[n2]v2
       | rfundamental3sv (suc (suc k)) vt ρ1 dρ ρ2 ρρ _ _ zero (s≤s z≤n) ρ1⊢t1↓[j]v2 ρ2⊢t2↓[n2]v3
... | bang f2 , vs↓dsv , refl | dtv , vt↓dvv , dtvv
      rewrite sym (rrelV3→⊕ vtv1 dtv vtv2 dtvv) =
        bang v2 , bangapp vs↓dsv ρ1⊢t1↓[j]v2 vt↓dvv ρ2⊢t2↓[n2]v4 , refl
... | dclosure dt ρ dρ₁ , vs↓dsv , (refl , refl) , refl , refl , refl , refl , dsvv | dtv , vt↓dvv , dtvv
      with dsvv (suc k) ≤-refl vtv1 dtv vtv2
           (rrelV3-mono (suc k) (suc (suc k)) (s≤s (≤-step ≤-refl)) _ vtv1 dtv vtv2 dtvv)
           v1 v2 j (s≤s j<k) ρ1⊢t1↓[j]v3 ρ2⊢t2↓[n2]v4
... | dv , ↓dv , dvv =
      dv , dapp vs↓dsv ρ1⊢t1↓[j]v2 vt↓dvv ↓dv , dvv

rfundamental3 (suc (suc k)) (lett s t) ρ1 dρ ρ2 ρρ v1 v2 .(suc (n1 + n2)) (s≤s (s≤s n1+n2≤k))
  (lett n1 n2 vs1 .s .t ρ1⊢t1↓[j]v1 ρ1⊢t1↓[j]v2) (lett _ _ vs2 .s .t ρ2⊢t2↓[n2]v2 ρ2⊢t2↓[n2]v3)
  with rfundamental3 (suc (suc k)) s ρ1 dρ ρ2 ρρ vs1 vs2 n1
    (s≤s (≤-trans (≤-trans (m≤m+n n1 n2) n1+n2≤k) (≤-step ≤-refl)))
    ρ1⊢t1↓[j]v1 ρ2⊢t2↓[n2]v2
... | dsv , ↓dsv , vsv
      with rfundamental3 (suc (suc k) ∸ n1) t (vs1 • ρ1) (dsv • dρ) (vs2 • ρ2) (vsv , rrelρ3-mono (suc (suc k) ∸ n1) (suc (suc k)) (m∸n≤m (suc (suc k)) n1) _ _ _ _ ρρ) v1 v2 n2 (sub∸ n1 (suc n2) (suc (suc k)) n1+[1+n2]≤2+k) ρ1⊢t1↓[j]v2 ρ2⊢t2↓[n2]v3
      where
        n1+[1+n2]≤2+k : n1 + suc n2 ≤ suc (suc k)
        n1+[1+n2]≤2+k rewrite +-suc n1 n2 = ≤-step (s≤s n1+n2≤k)
... | dv , ↓dv , dvv = dv , dlett ρ1⊢t1↓[j]v1 ↓dsv ↓dv , rrelV3-mono (suc k ∸ (n1 + n2)) (suc (suc k) ∸ n1 ∸ n2) 1+k-[n1+n2]≤2+k-n1-n2 _ v1 dv v2 dvv
  where
    1+k-[n1+n2]≤2+k-n1-n2 : suc k ∸ (n1 + n2) ≤ suc (suc k) ∸ n1 ∸ n2
    1+k-[n1+n2]≤2+k-n1-n2 rewrite ∸-+-assoc (suc (suc k)) n1 n2 = ∸-mono {suc k} {suc (suc k)} {n1 + n2} {n1 + n2} (≤-step ≤-refl) ≤-refl

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by decidable total orders
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.Properties.DecTotalOrder
         {d₁ d₂ d₃} (DT : DecTotalOrder d₁ d₂ d₃) where

open Relation.Binary.DecTotalOrder DT hiding (trans)
import Relation.Binary.NonStrictToStrict as Conv
open Conv _≈_ _≤_

strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder = record
  { isStrictTotalOrder = record
      { isEquivalence = isEquivalence
      ; trans         = trans isPartialOrder
      ; compare       = trichotomous Eq.sym _≟_ antisym total
      ; <-resp-≈      = <-resp-≈ isEquivalence ≤-resp-≈
      }
  }

open StrictTotalOrder strictTotalOrder public


text:
open import IO

main = run (putStr "Hacktoberfest")


text:
{-# OPTIONS --show-implicit --show-irrelevant #-}
-- {-# OPTIONS -v tc.conv.irr:20 -v tc.constr.findInScope:20 -v tc.meta:20 -v tc.conv.type:50 -v tc.conv.term:30 -v tc.conv.atom:50 -v tc.inj.use:20 #-}
module Issue631 where

import Common.Level  -- for debug messages

data Bool : Set where
  false true : Bool

F : Bool → Set
F true  = Bool
F false = Bool

postulate
  BAD   : ∀ {u} → F u
  Goal  : Set
  score  : .Goal → Set

buggy : Set
buggy = score _ -- {!!}
-- should remain unsolved


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

module Data.Vec where

open import Prelude

private
  variable
    n m : ℕ

infixr 5 _∷_
data Vec (A : Type a) : ℕ → Type a where
  [] : Vec A zero
  _∷_ : A → Vec A n → Vec A (suc n)

head : Vec A (suc n) → A
head (x ∷ _) = x

foldr : (A → B → B) → B → Vec A n → B
foldr f b [] = b
foldr f b (x ∷ xs) = f x (foldr f b xs)


text:
module GUIgeneric.GUIFeaturesPart3 where

open import GUIgeneric.Prelude renaming (addButton to addButton')

open import GUIgeneric.GUIDefinitions renaming (add to add'; add' to add)
open import GUIgeneric.GUI
open import GUIgeneric.GUIExampleLib
open import StateSizedIO.GUI.WxGraphicsLibLevel3 renaming (addButton to addButton')
open import GUIgeneric.GUIFeatures
open import GUIgeneric.GUIFeaturesPart2 hiding ( main )
open import GUIgeneric.GUIExample hiding (main )

open import Data.Product
open import Data.Fin

liftResultˢ : (S S' : Set) (s2GUI : (s : S') → Frame)
             (ss' : S → S')
             (s : S)
             (m : methodsG (s2GUI (ss' s)))
             (r : Resultˢ (handlerGUIInterfₛ S (s2GUI ∘ ss')) s m)
            → Resultˢ (handlerGUIInterfₛ S' s2GUI) (ss' s) m
liftResultˢ S S' s2GUI ss' s m noChange = noChange
liftResultˢ S S' s2GUI ss' s m (changedState snew) = changedState (ss' snew)

extendHandlerGuiInterfₛ :  (i : Size)
                           (S S' : Set) (s2GUI : (s : S') → Frame)
                           (ss' : S → S')
                           (s : S)
                           (obj : handlerGUIObjectₛ i S (s2GUI ∘ ss') s)
                           → handlerGUIObjectₛ i S' s2GUI (ss' s)
method (extendHandlerGuiInterfₛ i S S' s2GUI ss' s obj) m =
                    x >>= (λ r → return (liftResultˢ S S' s2GUI ss' s m r))
              where
                      x : IO GuiLev1Interface ∞  (Resultˢ (handlerGUIInterfₛ S (s2GUI ∘ ss')) s m)
                      x = method obj m

lift⊎3  : {A B C : Set} → A ⊎ B → A ⊎ B ⊎ C
lift⊎3 (inj₁ x) = inj₁ x
lift⊎3 (inj₂ y) = inj₂ (inj₁ y)

mapReturnTypeₛ : {A B : Set}(f : A → B) (a : ReturnTypeₛ A) → ReturnTypeₛ  B
mapReturnTypeₛ f noChange = noChange
mapReturnTypeₛ f (changedState snew) = changedState (f snew)

mapStateMachineHandl : {S S' : Set}(f : S → S')
                       (p : IO GuiLev1Interface ∞ (ReturnTypeₛ S))
                       → IO GuiLev1Interface ∞ (ReturnTypeₛ S')
mapStateMachineHandl f p = mapIO (mapReturnTypeₛ f) p

mapSMachineState : {S S' : Set}(f : S → S')(s : S)(sm : SMachineState S s)
                    → SMachineState S' (f s)
mapSMachineState f s sm .fSM = sm .fSM
mapSMachineState f s sm .propSM = sm .propSM
mapSMachineState f s sm .handlSM m = mapStateMachineHandl f (sm .handlSM m)

mapFMachineHandle : {A B C : Set}
                          (a : A ⊎ B)(sm : SMachineState (A ⊎ B) a)
                          → SMachineState (A ⊎ B ⊎ C) (lift⊎3 a)
mapFMachineHandle a sm = mapSMachineState lift⊎3 a sm

mapIOFeatureM : {A B C : Set}
            → IO GuiLev1Interface ∞ (ReturnTypeₛ (A ⊎ B))
            → IO GuiLev1Interface ∞ (ReturnTypeₛ (A ⊎ B ⊎ C))
mapIOFeatureM p = mapIO (mapReturnTypeₛ lift⊎3) p

Cancel : FMachine StateV → FMachine StateV
Cancel vm .Features = vm .Features × FeatureCancel
Cancel vm .AddStateF  = vm .AddStateF ⊎ ⊤
Cancel vm .GUIF (f , yesCancel) (inj₁ s1) =
      addBtn2StateMachine (mapFMachineHandle (inj₁ s1) (vm .GUIF f (inj₁ s1)))
                          "Cancel" ((inj₂ (inj₂ _)))
Cancel vm .GUIF (f , _) (inj₁ s) = mapFMachineHandle (inj₁ s) (vm .GUIF f (inj₁ s))
Cancel vm .GUIF (f , _) (inj₂ (inj₁ x)) = mapFMachineHandle (inj₂ x) (vm .GUIF f (inj₂ x))
Cancel vm .GUIF (f , _) (inj₂ (inj₂ _)) = simpleSMState "Intermediate" (inj₁ s0)

Tea : FMachine StateV → FMachine StateV
Tea vm .Features = vm .Features × FeatureTea
Tea vm .AddStateF  = vm .AddStateF ⊎ ⊤
Tea vm .GUIF (f , yeTea) (inj₁ s2) =
      addBtn2StateMachine (mapFMachineHandle (inj₁ s2) (vm .GUIF f (inj₁ s2)))
                          "Tea" ((inj₂ (inj₂ _)))
Tea vm .GUIF (f , _) (inj₁ s) = mapFMachineHandle (inj₁ s) (vm .GUIF f (inj₁ s))
Tea vm .GUIF (f , _) (inj₂ (inj₁ x)) = mapFMachineHandle (inj₂ x) (vm .GUIF f (inj₂ x))
Tea vm .GUIF (f , _) (inj₂ (inj₂ _)) = simpleSMState "Get Your Tea" (inj₁ s0)

cancelBase : FMachine StateV
cancelBase = Cancel baseF

teaCancelBase : FMachine StateV
teaCancelBase = Tea cancelBase

main : NativeIO Unit
main = compileFeatureVM teaCancelBase ((_ , yesCancel) , yesTea) (inj₁ s0) --

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by strict partial orders
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Properties.StrictTotalOrder
       {s₁ s₂ s₃} (STO : StrictTotalOrder s₁ s₂ s₃)
       where

open Relation.Binary.StrictTotalOrder STO
open import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_
import Relation.Binary.Properties.StrictPartialOrder as SPO
open import Relation.Binary.Consequences

------------------------------------------------------------------------
-- Strict total orders can be converted to decidable total orders

decTotalOrder : DecTotalOrder _ _ _
decTotalOrder = record
  { isDecTotalOrder = isDecTotalOrder isStrictTotalOrder
  }

open DecTotalOrder decTotalOrder public


text:
module parse-tree where

open import lib

record ParseTreeRec : Set lone where
  field
    ParseTreeT : Set
    isParseTree : ParseTreeT → 𝕃 char → string → Set
    ParseTreeToString : ParseTreeT → string

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
module List where

data Bool : Set where
  true : Bool
  false : Bool

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

boolElim : (P : Bool -> Set) -> P true -> P false -> (b : Bool) -> P b
boolElim P t f true  = t
boolElim P t f false = f

data False : Set where
data True : Set where
  tt : True

data Or (A B : Set) : Set where
  inl : (a : A) -> Or A B
  inr : (b : B) -> Or A B

orElim : {A B : Set}
    -> (C : Or A B -> Set)
    -> (cl : (a : A) -> C(inl a))
    -> (cr : (b : B) -> C(inr b))
    -> (ab : Or A B)
    -> C ab
orElim {A} {B} C cl cr (inl a) = cl a
orElim {A} {B} C cl cr (inr b) = cr b

data Rel(A : Set) : Set1 where
  rel : (A -> A -> Set) -> Rel A

_is_than_ : {A : Set} -> A -> Rel A -> A -> Set
x is rel f than y = f x y

data Acc {A : Set} (less : Rel A) (x : A) : Set where
  acc : ((y : A) -> y is less than x -> Acc less y) -> Acc less x

data WO {A : Set} (less : Rel A) : Set where
  wo : ((x : A) -> Acc less x) -> WO less

data Nat : Set where
  Z : Nat
  S : Nat -> Nat

eqNat : Nat -> Nat -> Set
eqNat Z Z = True
eqNat (S m) (S n) = eqNat m n
eqNat _ _ = False

substEqNat : (P : Nat -> Set) -> (a b : Nat) -> (e : eqNat a b) -> (P a) -> P b
substEqNat P Z Z e pa = pa
substEqNat P (S x) (S x') e pa = substEqNat (\n -> P(S n)) x  x'  e  pa

ltNat : Nat -> Nat -> Set
ltNat    Z     Z  = False
ltNat    Z  (S n) = True
ltNat (S m) (S n) = ltNat m n
ltNat (S m)    Z  = False

ltZ-elim : (n : Nat) -> ltNat n Z -> {whatever : Set} -> whatever
ltZ-elim Z     ()
ltZ-elim (S _) ()

transNat : (x  y  z : Nat) -> ltNat x y -> ltNat y z -> ltNat x z
transNat x     y     Z     x<y y<z  = ltZ-elim y y<z
transNat x     Z     (S z) x<Z Z<Sz = ltZ-elim x x<Z
transNat Z     (S y) (S z) tt  y<z  = tt
transNat (S x) (S y) (S z) x<y y<z  = transNat x y z x<y y<z

ltNat-S-Lemma : (x : Nat) -> ltNat x (S x)
ltNat-S-Lemma Z     = tt
ltNat-S-Lemma (S x) = ltNat-S-Lemma x

ltNat-S-Lemma2 : (y z : Nat) -> ltNat y (S z) -> Or (eqNat z y) (ltNat y z)
ltNat-S-Lemma2 Z Z h = inl tt
ltNat-S-Lemma2 Z (S x) h = inr tt
ltNat-S-Lemma2 (S x) (S x') h = ltNat-S-Lemma2 x  x' h

ltNatRel : Rel Nat
ltNatRel = rel ltNat

less = ltNatRel

acc-Lemma1 : (x y : Nat) -> Acc less x -> eqNat x y -> Acc less y
acc-Lemma1 x y a e = substEqNat (Acc less ) x  y  e  a

acc-Lemma2 : (x y : Nat) -> Acc less x -> ltNat y x -> Acc less y
acc-Lemma2 x y (acc h) l = h y  l

-- postulate woltNat' : (n : Nat) -> Acc less n
woltNat' : (n : Nat) -> Acc less n
woltNat' Z     = acc (\y y<Z -> ltZ-elim y y<Z)
woltNat' (S x) = acc (\y y<Sx -> orElim (\w -> Acc less y) (\e -> substEqNat (Acc less ) x  y  e  (woltNat' x ) ) (acc-Lemma2 x y (woltNat' x)) (ltNat-S-Lemma2 y x y<Sx ))

woltNat : WO ltNatRel
woltNat = wo woltNat'

postulate le : Nat -> Nat -> Bool
postulate gt : Nat -> Nat -> Bool

data List (A : Set) : Set where
  nil  : List A
  cons : (x : A) -> (xs : List A) -> List A

_++_ : {A : Set} -> List A -> List A -> List A
nil         ++ ys = ys
(cons x xs) ++ ys = cons x (xs ++ ys)

length : {A : Set} -> List A -> Nat
length nil         = Z
length (cons x xs) = S (length xs)

filter : {A : Set} -> (A -> Bool) -> List A -> List A
filter p nil = nil
filter p (cons x xs) = if p x then cons x rest else rest
  where rest = filter p xs

filterLemma
  :  {A : Set} -> (p : A -> Bool) -> (xs : List A)
  -> length (filter p xs) is less than S (length xs)
filterLemma p nil         = tt
filterLemma p (cons x xs) =
  boolElim (\px -> length (if px then cons x (filter p xs)
                                 else (filter p xs))
                   is less than S (S (length xs)))
           (filterLemma p xs)
           (transNat (length (filter p xs)) (S (length xs)) (S (S (length xs)))
                     (filterLemma p xs) (ltNat-S-Lemma (length xs )))
           (p x)

qs : List Nat -> List Nat
qs nil         = nil
qs (cons x xs) = qs (filter (le x) xs)
                 ++ cons x nil
                 ++ qs (filter (gt x) xs)

data Measure : Set1 where
  μ : {M : Set} -> {rel : Rel M} -> (ord : WO rel) -> Measure

down1-measure : Measure
down1-measure = μ woltNat

qs-2-1-hint = \(x : Nat) -> \(xs : List Nat) -> filterLemma (le x) xs
qs-2-2-hint = \(x : Nat) -> \(xs : List Nat) -> filterLemma (gt x) xs


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Permutation.Inductive directly.
------------------------------------------------------------------------

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

module Data.List.Relation.Permutation.Inductive where

open import Data.List.Relation.Binary.Permutation.Inductive public

{-# WARNING_ON_IMPORT
"Data.List.Relation.Permutation.Inductive was deprecated in v1.0.
Use Data.List.Relation.Binary.Permutation.Inductive instead."
#-}