text:
{-# OPTIONS --no-auto-inline #-}

-- Agda doesn't have an Int type (only Word64). With some work we
-- can represent signed ints using Word64.

module Haskell.Prim.Int where

open import Agda.Builtin.Nat
open import Agda.Builtin.Word renaming (primWord64ToNat to w2n; primWord64FromNat to n2w)
open import Agda.Builtin.List
open import Agda.Builtin.Char
open import Agda.Builtin.String
open import Agda.Builtin.Unit
open import Agda.Builtin.Int using (pos; negsuc)
open import Agda.Builtin.Equality

open import Haskell.Prim
open import Haskell.Prim.Word
open import Haskell.Prim.Integer
open import Haskell.Prim.Bool

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

data Int : Set where
  int64 : Word64 → Int

intToWord : Int → Word64
intToWord (int64 a) = a

unsafeIntToNat : Int → Nat
unsafeIntToNat a = w2n (intToWord a)

--------------------------------------------------
-- Literals

private
  2⁶⁴ : Nat
  2⁶⁴ = 18446744073709551616

  2⁶³ : Nat
  2⁶³ = 9223372036854775808

  maxInt : Nat
  maxInt = 2⁶³ - 1

instance
  iNumberInt : Number Int
  iNumberInt .Number.Constraint n = IsTrue (n < 2⁶³)
  iNumberInt .fromNat n = int64 (n2w n)

  iNegativeInt : Negative Int
  iNegativeInt .Negative.Constraint n = IsTrue (n < 1 + 2⁶³)
  iNegativeInt .fromNeg n = int64 (n2w (2⁶⁴ - n))

--------------------------------------------------
-- Arithmetic

isNegativeInt : Int → Bool
isNegativeInt (int64 w) = maxInt < w2n w

eqInt : Int → Int → Bool
eqInt (int64 a) (int64 b) = w2n a == w2n b

negateInt : Int → Int
negateInt (int64 a) = int64 (n2w (2⁶⁴ - w2n a))

intToInteger : Int → Integer
intToInteger a = if isNegativeInt a then negsuc (unsafeIntToNat (negateInt a) - 1)
                                    else pos (unsafeIntToNat a)

integerToInt : Integer → Int
integerToInt (pos    n) = int64 (n2w n)
integerToInt (negsuc n) = negateInt (int64 (n2w (suc n)))

private
  ltPosInt : Int → Int → Bool
  ltPosInt (int64 a) (int64 b) = ltWord a b

ltInt : Int → Int → Bool
ltInt a b with isNegativeInt a | isNegativeInt b
... | true  | false = true
... | false | true  = false
... | true  | true  = ltPosInt (negateInt b) (negateInt a)
... | false | false = ltPosInt a b

addInt : Int → Int → Int
addInt (int64 a) (int64 b) = int64 (addWord a b)

subInt : Int → Int → Int
subInt a b = addInt a (negateInt b)

mulInt : Int → Int → Int
mulInt (int64 a) (int64 b) = int64 (mulWord a b)

absInt : Int → Int
absInt a = if isNegativeInt a then negateInt a else a

signInt : Int → Int
signInt a = if      isNegativeInt a then -1
            else if eqInt a 0       then 0 else 1

showInt : Int → List Char
showInt a = showInteger (intToInteger a)

--------------------------------------------------
-- Constraints

IsNonNegativeInt : Int → Set
IsNonNegativeInt a@(int64 _) =
  if isNegativeInt a then TypeError (primStringAppend (primStringFromList (showInt a)) " is negative")
                     else ⊤

intToNat : (a : Int) → ⦃ IsNonNegativeInt a ⦄ → Nat
intToNat a = unsafeIntToNat a


text:
module Vecs.Reverse where

open import Vecs
open import Nats
open import Equality
open import Function

------------------------------------------------------------------------
-- internal stuffs

private

  -- rev$v:a=a:rev$v : ∀ {n m} {A : Set n} (a : A) (v : Vec A m) →
  --                 rev (v ∷ʳ a) ≡ a ∷ rev v
  -- rev$v:a=a:rev$v _ [] = refl
  -- rev$v:a=a:rev$v a (_ ∷ xs) with rev (xs ∷ʳ a) | rev$v:a=a:rev$v a xs
  -- ...                            | .(a ∷ rev xs) | refl = refl

  rev$v:a=a:rev$v : ∀ {n m} {A : Set n} (a : A) (v : Vec A m) →
                  reverse (v ∷ʳ a) ≡ a ∷ reverse v
  rev$v:a=a:rev$v _ [] = refl
  rev$v:a=a:rev$v a (_ ∷ xs)
    rewrite rev$v:a=a:rev$v a xs
            = refl

  rev∘rev=id : ∀ {n m} {A : Set n} (v : Vec A m) → reverse (reverse v) ≡ v
  rev∘rev=id [] = refl
  rev∘rev=id (x ∷ xs)
    rewrite rev$v:a=a:rev$v x $ reverse xs
          | rev∘rev=id xs
            = refl

------------------------------------------------------------------------
-- public aliases

vec-rev-rev-id : ∀ {n m} {A : Set n} (v : Vec A m) → reverse (reverse v) ≡ v
vec-rev-rev-id = rev∘rev=id

ext: agda


text:
-- This file needs to be rewritten so that Rng's are defined as a
-- record (as is the case for other algebraic structures like
-- rings). As this file isn't used for anything at the moment this
-- rewrite has been postponed.

{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Experiments.Rng where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.SIP
open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro
open import Cubical.Algebra.Semigroup hiding (⟨_⟩)
open import Cubical.Algebra.AbGroup

private
  variable
    ℓ ℓ' : Level

module _ {ℓ} where
  rawRngDesc : Desc ℓ
  rawRngDesc = autoDesc (λ (X : Type ℓ) → (X → X → X) × (X → X → X))

  open Macro ℓ rawRngDesc public renaming
    ( structure to RawRngStructure
    ; equiv to RawRngEquivStr
    ; univalent to rawRngUnivalentStr
    )

RngAxioms : (X : Type ℓ) (s : RawRngStructure X) → Type ℓ
RngAxioms X (_·_ , _+_) =
  AbGroupΣTheory.AbGroupAxioms X _·_ ×
  SemigroupΣTheory.SemigroupAxioms X _+_ ×
  ((x y z : X) → x · (y + z) ≡ (x · y) + (x · z)) × ((x y z : X) → (x + y) · z ≡ (x · z) + (y · z))

RngStructure : Type ℓ → Type ℓ
RngStructure = AxiomsStructure RawRngStructure RngAxioms

Rng : Type (ℓ-suc ℓ)
Rng {ℓ} = TypeWithStr ℓ RngStructure

RngEquivStr : StrEquiv RngStructure ℓ
RngEquivStr = AxiomsEquivStr RawRngEquivStr RngAxioms

isPropRngAxioms : (X : Type ℓ) (s : RawRngStructure X) → isProp (RngAxioms X s)
isPropRngAxioms X (_·_ , _+_) = isPropΣ (AbGroupΣTheory.isPropAbGroupAxioms X _·_)
                                  λ _ → isPropΣ (SemigroupΣTheory.isPropSemigroupAxioms X _+_)
                                  λ { (isSetX , _) → isPropΣ (isPropΠ3 (λ _ _ _ → isSetX _ _))
                                  λ _ → isPropΠ3 (λ _ _ _ → isSetX _ _)}

rngUnivalentStr : UnivalentStr {ℓ} RngStructure RngEquivStr
rngUnivalentStr = axiomsUnivalentStr _ isPropRngAxioms rawRngUnivalentStr

RngPath : (M N : Rng {ℓ}) → (M ≃[ RngEquivStr ] N) ≃ (M ≡ N)
RngPath = SIP rngUnivalentStr

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
module Issue27 where

infix  4 _≡_
infixl 4 _>_ _<_
infixr 1 _∨_

postulate ℝ : Set

------------------------------------------------------------------------------
-- Logic stuff

-- The identity type on the universe of discourse.
data _≡_ (x : ℝ) : ℝ → Set where
  refl : x ≡ x

data _∨_ (A B : Set) : Set where
  inj₁ : A → A ∨ B
  inj₂ : B → A ∨ B

case : ∀ {A B} → {C : Set} → (A → C) → (B → C) → A ∨ B → C
case f g (inj₁ a) = f a
case f g (inj₂ b) = g b

------------------------------------------------------------------------------
-- Real numbers stuff

postulate _>_ : ℝ → ℝ → Set

_<_ : ℝ → ℝ → Set
y < x = x > y
{-# ATP definition _<_ #-}

postulate
  trichotomy : (x y : ℝ) → (x > y) ∨ (x ≡ y) ∨ (x < y)
{-# ATP axiom trichotomy #-}

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

rmin : ℝ → ℝ → ℝ
rmin x y = case (λ _ → y) (λ h → case (λ _ → x) (λ _ → x) h) (trichotomy x y)
{-# ATP definition rmin #-}

postulate foo : ∀ x y → rmin x y ≡ rmin x y
{-# ATP prove foo #-}

{-
Error:
$ apia --check Issue27.agda
apia: tptp4X found an error/warning in the file /tmp/Issue27/44-foo.fof
Please report this as a bug

WARNING: Line 34 Char 159 Token "," : Multiple arity symbol n_62__46_8405600604384089447, arity 0 and now 2
WARNING: Line 34 Char 259 Token ")" : Multiple arity symbol n_60__48_8405600604384089447, arity 0 and now 2
WARNING: Line 34 Char 387 Token "," : Multiple arity symbol n_60__48_8405600604384089447, arity 0 and now 2
WARNING: Line 34 Char 460 Token ")" : Multiple arity symbol case_32_8405600604384089447, arity 5 and now 6
-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The identity function
------------------------------------------------------------------------

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

module Function.Construct.Identity where

open import Data.Product using (_,_)
open import Function using (id)
open import Function.Bundles
import Function.Definitions as Definitions
import Function.Structures as Structures
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; setoid)

private
  variable
    a ℓ : Level
    A : Set a

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

module _ (_≈_ : Rel A ℓ) where

  open Definitions _≈_ _≈_

  injective : Injective id
  injective = id

  surjective : Reflexive _≈_ → Surjective id
  surjective refl x = x , refl

  bijective : Reflexive _≈_ → Bijective id
  bijective refl = injective , surjective refl

  inverseˡ : Reflexive _≈_ → Inverseˡ id id
  inverseˡ refl x = refl

  inverseʳ : Reflexive _≈_ → Inverseʳ id id
  inverseʳ refl x = refl

  inverseᵇ : Reflexive _≈_ → Inverseᵇ id id
  inverseᵇ refl = inverseˡ refl , inverseʳ refl

------------------------------------------------------------------------
-- Structures

module _ {_≈_ : Rel A ℓ} (isEq : IsEquivalence _≈_) where

  open Structures _≈_ _≈_
  open IsEquivalence isEq

  isCongruent : IsCongruent id
  isCongruent = record
    { cong           = id
    ; isEquivalence₁ = isEq
    ; isEquivalence₂ = isEq
    }

  isInjection : IsInjection id
  isInjection = record
    { isCongruent = isCongruent
    ; injective   = injective _≈_
    }

  isSurjection : IsSurjection id
  isSurjection = record
    { isCongruent = isCongruent
    ; surjective  = surjective _≈_ refl
    }

  isBijection : IsBijection id
  isBijection = record
    { isInjection = isInjection
    ; surjective  = surjective _≈_ refl
    }

  isLeftInverse : IsLeftInverse id id
  isLeftInverse = record
    { isCongruent = isCongruent
    ; cong₂       = id
    ; inverseˡ    = inverseˡ _≈_ refl
    }

  isRightInverse : IsRightInverse id id
  isRightInverse = record
    { isCongruent = isCongruent
    ; cong₂       = id
    ; inverseʳ    = inverseʳ _≈_ refl
    }

  isInverse : IsInverse id id
  isInverse = record
    { isLeftInverse = isLeftInverse
    ; inverseʳ      = inverseʳ _≈_ refl
    }

------------------------------------------------------------------------
-- Setoid bundles

module _ (S : Setoid a ℓ) where

  open Setoid S

  injection : Injection S S
  injection = record
    { f         = id
    ; cong      = id
    ; injective = injective _≈_
    }

  surjection : Surjection S S
  surjection = record
    { f          = id
    ; cong       = id
    ; surjective = surjective _≈_ refl
    }

  bijection : Bijection S S
  bijection = record
    { f         = id
    ; cong      = id
    ; bijective = bijective _≈_ refl
    }

  equivalence : Equivalence S S
  equivalence = record
    { f     = id
    ; g     = id
    ; cong₁ = id
    ; cong₂ = id
    }

  leftInverse : LeftInverse S S
  leftInverse = record
    { f        = id
    ; g        = id
    ; cong₁    = id
    ; cong₂    = id
    ; inverseˡ = inverseˡ _≈_ refl
    }

  rightInverse : RightInverse S S
  rightInverse = record
    { f        = id
    ; g        = id
    ; cong₁    = id
    ; cong₂    = id
    ; inverseʳ = inverseʳ _≈_ refl
    }

  inverse : Inverse S S
  inverse = record
    { f       = id
    ; f⁻¹     = id
    ; cong₁   = id
    ; cong₂   = id
    ; inverse = inverseᵇ _≈_ refl
    }

------------------------------------------------------------------------
-- Propositional bundles

module _ (A : Set a) where

  id-↣ : A ↣ A
  id-↣ = injection (setoid A)

  id-↠ : A ↠ A
  id-↠ = surjection (setoid A)

  id-⤖ : A ⤖ A
  id-⤖ = bijection (setoid A)

  id-⇔ : A ⇔ A
  id-⇔ = equivalence (setoid A)

  id-↩ : A ↩ A
  id-↩ = leftInverse (setoid A)

  id-↪ : A ↪ A
  id-↪ = rightInverse (setoid A)

  id-↔ : A ↔ A
  id-↔ = inverse (setoid A)


text:
------------------------------------------------------------------------
-- Coinductive axiomatisation of subtyping
------------------------------------------------------------------------

module RecursiveTypes.Subtyping.Axiomatic.Coinductive where

import Data.Empty as E
open import Data.Fin using (Fin; zero; suc)
open import Data.Nat using (ℕ; zero; suc)
open import Codata.Musical.Notation
open import Relation.Nullary

open import RecursiveTypes.Syntax
open import RecursiveTypes.Substitution
open import RecursiveTypes.Semantics
open import RecursiveTypes.Subtyping.Semantic.Coinductive as Sem
  using (_≤∞P_; _≤Coind_; ⟦_⟧P; ⌜_⌝; ⊥; ⊤; var; _⟶_; _≤⟨_⟩_)

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

-- This definition uses mixed induction and coinduction. Induction is
-- used for rules like transitivity, whereas coinduction is used for
-- structural rules. Benjamin Pierce observed in Types and Programming
-- Languages that coinductive inference systems cannot be
-- "declarative" (including rules like transitivity); they can be
-- "algorithmic" (syntax-directed), though. However, by mixing
-- induction and coinduction one can combine the benefits of
-- coinduction and declarative inference systems.

infixr 10 _⟶_
infix  4  _≤_
infix  3  _∎
infixr 2  _≤⟨_⟩_

data _≤_ {n} : Ty n → Ty n → Set where
  -- Structural rules. Note that the rule for _⟶_ is coinductive.
  ⊥   : ∀ {τ} → ⊥ ≤ τ
  ⊤   : ∀ {σ} → σ ≤ ⊤
  _⟶_ : ∀ {σ₁ σ₂ τ₁ τ₂} (τ₁≤σ₁ : ∞ (τ₁ ≤ σ₁)) (σ₂≤τ₂ : ∞ (σ₂ ≤ τ₂)) →
        σ₁ ⟶ σ₂ ≤ τ₁ ⟶ τ₂

  -- Rules for folding and unfolding μ.
  unfold : ∀ {τ₁ τ₂} → μ τ₁ ⟶ τ₂ ≤ unfold[μ τ₁ ⟶ τ₂ ]
  fold   : ∀ {τ₁ τ₂} → unfold[μ τ₁ ⟶ τ₂ ] ≤ μ τ₁ ⟶ τ₂

  -- Reflexivity.
  _∎ : ∀ τ → τ ≤ τ

  -- Transitivity.
  _≤⟨_⟩_ : ∀ τ₁ {τ₂ τ₃} (τ₁≤τ₂ : τ₁ ≤ τ₂) (τ₂≤τ₃ : τ₂ ≤ τ₃) → τ₁ ≤ τ₃

------------------------------------------------------------------------
-- Equivalence

-- The axiomatisation is equivalent to the semantic definitions of
-- subtyping.

soundP : ∀ {n} {σ τ : Ty n} → σ ≤ τ → ⟦ σ ⟧ ≤∞P ⟦ τ ⟧
soundP ⊥                     = ⊥
soundP ⊤                     = ⊤
soundP (τ₁≤σ₁ ⟶ σ₂≤τ₂)       = ♯ soundP (♭ τ₁≤σ₁) ⟶ ♯ soundP (♭ σ₂≤τ₂)
soundP unfold                = ⌜ Sem.unfold  ⌝
soundP fold                  = ⌜ Sem.fold    ⌝
soundP (τ ∎)                 = ⌜ Sem.refl∞ _ ⌝
soundP (τ₁ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) = _ ≤⟨ soundP τ₁≤τ₂ ⟩ soundP τ₂≤τ₃

sound : ∀ {n} {σ τ : Ty n} → σ ≤ τ → σ ≤Coind τ
sound σ≤τ = ⟦ soundP σ≤τ ⟧P

complete : ∀ {n} (σ τ : Ty n) → σ ≤Coind τ → σ ≤ τ
complete ⊥         _         _ = ⊥
complete _         ⊤         _ = ⊤
complete ⊤         ⊥         ()
complete ⊤         (var x)   ()
complete ⊤         (σ ⟶ τ)   ()
complete ⊤         (μ σ ⟶ τ) ()
complete (var x)   ⊥         ()
complete (var x)   (var .x)  var = var x ∎
complete (var x)   (σ ⟶ τ)   ()
complete (var x)   (μ σ ⟶ τ) ()
complete (σ₁ ⟶ σ₂) ⊥         ()
complete (σ₁ ⟶ σ₂) (var x)   ()
complete (σ₁ ⟶ σ₂) (τ₁ ⟶ τ₂) (τ₁≤σ₁ ⟶ σ₂≤τ₂) =
  ♯ complete τ₁ σ₁ (♭ τ₁≤σ₁) ⟶ ♯ complete σ₂ τ₂ (♭ σ₂≤τ₂)
complete (σ₁ ⟶ σ₂) (μ τ₁ ⟶ τ₂) (τ₁≤σ₁ ⟶ σ₂≤τ₂) =
  σ₁ ⟶ σ₂             ≤⟨ ♯ complete _ _ (♭ τ₁≤σ₁) ⟶
                         ♯ complete _ _ (♭ σ₂≤τ₂) ⟩
  unfold[μ τ₁ ⟶ τ₂ ]  ≤⟨ fold ⟩
  μ τ₁ ⟶ τ₂           ∎
complete (μ σ₁ ⟶ σ₂) ⊥         ()
complete (μ σ₁ ⟶ σ₂) (var x)   ()
complete (μ σ₁ ⟶ σ₂) (τ₁ ⟶ τ₂) (τ₁≤σ₁ ⟶ σ₂≤τ₂) =
  μ σ₁ ⟶ σ₂           ≤⟨ unfold ⟩
  unfold[μ σ₁ ⟶ σ₂ ]  ≤⟨ ♯ complete _ _ (♭ τ₁≤σ₁) ⟶
                         ♯ complete _ _ (♭ σ₂≤τ₂) ⟩
  (τ₁ ⟶ τ₂)           ∎
complete (μ σ₁ ⟶ σ₂) (μ τ₁ ⟶ τ₂) (τ₁≤σ₁ ⟶ σ₂≤τ₂) =
  μ σ₁ ⟶ σ₂           ≤⟨ unfold ⟩
  unfold[μ σ₁ ⟶ σ₂ ]  ≤⟨ ♯ complete _ _ (♭ τ₁≤σ₁) ⟶
                         ♯ complete _ _ (♭ σ₂≤τ₂) ⟩
  unfold[μ τ₁ ⟶ τ₂ ]  ≤⟨ fold ⟩
  μ τ₁ ⟶ τ₂           ∎

------------------------------------------------------------------------
-- The reflexivity constructor is essential

-- Minor point: the constructor _∎ cannot be omitted. In
-- RecursiveTypes.Subtyping.Axiomatic.Incorrect it is shown that
-- _≤⟨_⟩_ is also essential.

module ∎-Is-Essential where

  infixr 10 _⟶_
  infix  4  _≤′_
  infixr 2  _≤⟨_⟩_

  data _≤′_ {n} : Ty n → Ty n → Set where
    ⊥   : ∀ {τ} → ⊥ ≤′ τ
    ⊤   : ∀ {σ} → σ ≤′ ⊤
    _⟶_ : ∀ {σ₁ σ₂ τ₁ τ₂}
          (τ₁≤σ₁ : ∞ (τ₁ ≤′ σ₁)) (σ₂≤τ₂ : ∞ (σ₂ ≤′ τ₂)) →
          σ₁ ⟶ σ₂ ≤′ τ₁ ⟶ τ₂

    unfold : ∀ {τ₁ τ₂} → μ τ₁ ⟶ τ₂ ≤′ unfold[μ τ₁ ⟶ τ₂ ]
    fold   : ∀ {τ₁ τ₂} → unfold[μ τ₁ ⟶ τ₂ ] ≤′ μ τ₁ ⟶ τ₂

    _≤⟨_⟩_ : ∀ τ₁ {τ₂ τ₃}
             (τ₁≤τ₂ : τ₁ ≤′ τ₂) (τ₂≤τ₃ : τ₂ ≤′ τ₃) → τ₁ ≤′ τ₃

  sound′ : ∀ {n} {σ τ : Ty n} → σ ≤′ τ → σ ≤ τ
  sound′ ⊥                    = ⊥
  sound′ ⊤                    = ⊤
  sound′ (τ₁≤σ₁ ⟶ σ₂≤τ₂)      = ♯ sound′ (♭ τ₁≤σ₁) ⟶ ♯ sound′ (♭ σ₂≤τ₂)
  sound′ unfold               = unfold
  sound′ fold                 = fold
  sound′ (_ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) = _ ≤⟨ sound′ τ₁≤τ₂ ⟩ sound′ τ₂≤τ₃

  x : Ty 1
  x = var zero

  x≰′x : ¬ x ≤′ x
  x≰′x (.x ≤⟨ x≤′σ ⟩ σ≤x) = helper x≤′σ σ≤x
    where
    helper : ∀ {σ} → x ≤′ σ → σ ≤′ x → E.⊥
    helper (.x ≤⟨ x≤σ₁ ⟩ σ₁≤σ₂) σ₂≤′x = helper x≤σ₁ (_ ≤⟨ σ₁≤σ₂ ⟩ σ₂≤′x)
    helper ⊤                    ⊤≤′x  with sound (sound′ ⊤≤′x)
    ... | ()

  incomplete : ¬ (∀ {n} {σ τ : Ty n} → σ ≤ τ → σ ≤′ τ)
  incomplete hyp with x≰′x (hyp (x ∎))
  ... | ()

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Hilbert-style formalisation of syntax with context pairs.
-- Sequences of terms.

module BasicIS4.Syntax.DyadicHilbertSequential where

open import BasicIS4.Syntax.Common public

-- Derivations.

infix 3 _⊦⊢_
data _⊦⊢_ : Cx² Ty Ty → Cx Ty → Set where
  nil   : ∀ {Γ Δ}         → Γ ⁏ Δ ⊦⊢ ∅
  var   : ∀ {Ξ A Γ Δ}     → A ∈ Γ → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , A
  mp    : ∀ {Ξ A B Γ Δ}   → A ▻ B ∈ Ξ → A ∈ Ξ → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , B
  ci    : ∀ {Ξ A Γ Δ}     → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , A ▻ A
  ck    : ∀ {Ξ A B Γ Δ}   → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , A ▻ B ▻ A
  cs    : ∀ {Ξ A B C Γ Δ} → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
  mvar  : ∀ {Ξ A Γ Δ}     → A ∈ Δ → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , A
  nec   : ∀ {Ξ Ξ′ A Γ Δ}  → ∅ ⁏ Δ ⊦⊢ Ξ′ , A → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , □ A
  cdist : ∀ {Ξ A B Γ Δ}   → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , □ (A ▻ B) ▻ □ A ▻ □ B
  cup   : ∀ {Ξ A Γ Δ}     → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , □ A ▻ □ □ A
  cdown : ∀ {Ξ A Γ Δ}     → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , □ A ▻ A
  cpair : ∀ {Ξ A B Γ Δ}   → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , A ▻ B ▻ A ∧ B
  cfst  : ∀ {Ξ A B Γ Δ}   → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , A ∧ B ▻ A
  csnd  : ∀ {Ξ A B Γ Δ}   → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , A ∧ B ▻ B
  unit  : ∀ {Ξ Γ Δ}       → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , ⊤

infix 3 _⊢_
_⊢_ : Cx² Ty Ty → Ty → Set
Γ ⁏ Δ ⊢ A = ∃ (λ Ξ → Γ ⁏ Δ ⊦⊢ Ξ , A)

-- Monotonicity with respect to context inclusion.

mono⊦⊢ : ∀ {Ξ Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊦⊢ Ξ → Γ′ ⁏ Δ ⊦⊢ Ξ
mono⊦⊢ η nil         = nil
mono⊦⊢ η (var i ts)  = var (mono∈ η i) (mono⊦⊢ η ts)
mono⊦⊢ η (mp i j ts) = mp i j (mono⊦⊢ η ts)
mono⊦⊢ η (ci ts)     = ci (mono⊦⊢ η ts)
mono⊦⊢ η (ck ts)     = ck (mono⊦⊢ η ts)
mono⊦⊢ η (cs ts)     = cs (mono⊦⊢ η ts)
mono⊦⊢ η (mvar i ts) = mvar i (mono⊦⊢ η ts)
mono⊦⊢ η (nec ss ts) = nec ss (mono⊦⊢ η ts)
mono⊦⊢ η (cdist ts)  = cdist (mono⊦⊢ η ts)
mono⊦⊢ η (cup ts)    = cup (mono⊦⊢ η ts)
mono⊦⊢ η (cdown ts)  = cdown (mono⊦⊢ η ts)
mono⊦⊢ η (cpair ts)  = cpair (mono⊦⊢ η ts)
mono⊦⊢ η (cfst ts)   = cfst (mono⊦⊢ η ts)
mono⊦⊢ η (csnd ts)   = csnd (mono⊦⊢ η ts)
mono⊦⊢ η (unit ts)   = unit (mono⊦⊢ η ts)

mono⊢ : ∀ {A Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢ A → Γ′ ⁏ Δ ⊢ A
mono⊢ η (Ξ , ts) = Ξ , mono⊦⊢ η ts

-- Monotonicity with respect to modal context inclusion.

mmono⊦⊢ : ∀ {Ξ Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ′ ⊦⊢ Ξ
mmono⊦⊢ θ nil         = nil
mmono⊦⊢ θ (var i ts)  = var i (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (mp i j ts) = mp i j (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (ci ts)     = ci (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (ck ts)     = ck (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (cs ts)     = cs (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (mvar i ts) = mvar (mono∈ θ i) (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (nec ss ts) = nec (mmono⊦⊢ θ ss) (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (cdist ts)  = cdist (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (cup ts)    = cup (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (cdown ts)  = cdown (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (cpair ts)  = cpair (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (cfst ts)   = cfst (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (csnd ts)   = csnd (mmono⊦⊢ θ ts)
mmono⊦⊢ θ (unit ts)   = unit (mmono⊦⊢ θ ts)

mmono⊢ : ∀ {A Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ′ ⊢ A
mmono⊢ θ (Ξ , ts) = Ξ , mmono⊦⊢ θ ts

-- Concatenation of derivations.

_⧺⊦_ : ∀ {Γ Δ Ξ Ξ′} → Γ ⁏ Δ ⊦⊢ Ξ → Γ ⁏ Δ ⊦⊢ Ξ′ → Γ ⁏ Δ ⊦⊢ Ξ ⧺ Ξ′
us ⧺⊦ nil       = us
us ⧺⊦ var i ts  = var i (us ⧺⊦ ts)
us ⧺⊦ mp i j ts = mp (mono∈ weak⊆⧺₂ i) (mono∈ weak⊆⧺₂ j) (us ⧺⊦ ts)
us ⧺⊦ ci ts     = ci (us ⧺⊦ ts)
us ⧺⊦ ck ts     = ck (us ⧺⊦ ts)
us ⧺⊦ cs ts     = cs (us ⧺⊦ ts)
us ⧺⊦ mvar i ts = mvar i (us ⧺⊦ ts)
us ⧺⊦ nec ss ts = nec ss (us ⧺⊦ ts)
us ⧺⊦ cdist ts  = cdist (us ⧺⊦ ts)
us ⧺⊦ cup ts    = cup (us ⧺⊦ ts)
us ⧺⊦ cdown ts  = cdown (us ⧺⊦ ts)
us ⧺⊦ cpair ts  = cpair (us ⧺⊦ ts)
us ⧺⊦ cfst ts   = cfst (us ⧺⊦ ts)
us ⧺⊦ csnd ts   = csnd (us ⧺⊦ ts)
us ⧺⊦ unit ts   = unit (us ⧺⊦ ts)

-- Modus ponens and necessitation in expanded form.

app : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B
app {A} {B} (Ξ , ts) (Ξ′ , us) = Ξ″ , vs
  where Ξ″ = (Ξ′ , A) ⧺ (Ξ , A ▻ B)
        vs = mp top (mono∈ (weak⊆⧺₁ (Ξ , A ▻ B)) top) (us ⧺⊦ ts)

box : ∀ {A Γ Δ} → ∅ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ □ A
box (Ξ , ts) = ∅ , nec ts nil

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Core.Everything
open import Cubical.Foundations.HLevels

module Cubical.Algebra.Monoid.Construct.Free {ℓ} (Aˢ : hSet ℓ) where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path
open import Cubical.Algebra.Monoid

open import Cubical.Data.Empty.Polymorphic
open import Cubical.Data.Prod

open import Cubical.Relation.Binary.Reasoning.Equality

private
  A = ⟨ Aˢ ⟩
  isSetA = Aˢ .snd

------------------------------------------------------------------------
-- The direct free monoid type

data FreeM : Type ℓ where
  inj : A → FreeM
  _•_ : Op₂ FreeM
  ε   : FreeM

  •-assoc     : Associative _•_
  ε-identityˡ : LeftIdentity ε _•_
  ε-identityʳ : RightIdentity ε _•_

  squash : isSet FreeM

ε-identity : Identity ε _•_
ε-identity = ε-identityˡ , ε-identityʳ

elim : ∀ {ℓ′} {B : FreeM → Type ℓ′} →
        (∀ x → isSet (B x)) →
        (∀ x → B (inj x)) →
        (op : ∀ {x y} → B x → B y → B (x • y)) →
        (e : B ε) →
        (∀ {x y z} (a : B x) (b : B y) (c : B z) → PathP (λ i → B (•-assoc x y z i)) (op (op a b) c) (op a (op b c))) →
        (∀ {x} (a : B x) → PathP (λ i → B (ε-identityˡ x i)) (op e a) a) →
        (∀ {x} (a : B x) → PathP (λ i → B (ε-identityʳ x i)) (op a e) a) →
        (x : FreeM) → B x
elim isSetB f op e assc idˡ idʳ (inj x) = f x
elim isSetB f op e assc idˡ idʳ (x • y) = op (elim isSetB f op e assc idˡ idʳ x) (elim isSetB f op e assc idˡ idʳ y)
elim isSetB f op e assc idˡ idʳ ε = e
elim isSetB f op e assc idˡ idʳ (•-assoc x y z i) = assc (elim isSetB f op e assc idˡ idʳ x)
                                                          (elim isSetB f op e assc idˡ idʳ y)
                                                          (elim isSetB f op e assc idˡ idʳ z) i
elim isSetB f op e assc idˡ idʳ (ε-identityˡ x i) = idˡ (elim isSetB f op e assc idˡ idʳ x) i
elim isSetB f op e assc idˡ idʳ (ε-identityʳ x i) = idʳ (elim isSetB f op e assc idˡ idʳ x) i
elim isSetB f op e assc idˡ idʳ (squash x y p q i j) =
  isOfHLevel→isOfHLevelDep 2 isSetB
    (elim isSetB f op e assc idˡ idʳ x) (elim isSetB f op e assc idˡ idʳ y)
    (cong (elim isSetB f op e assc idˡ idʳ) p) (cong (elim isSetB f op e assc idˡ idʳ) q) (squash x y p q) i j

------------------------------------------------------------------------
-- The simplified free monoid type

-- Defined in Cubical.Data.List
open import Cubical.Data.List
open Structures isSetA public

------------------------------------------------------------------------
-- Proving the two types are equivalent

List→FreeM : List A → FreeM
List→FreeM []       = ε
List→FreeM (x ∷ xs) = inj x • List→FreeM xs

FreeM→List : FreeM → List A
FreeM→List = elim (λ _ → isOfHLevelList 0 isSetA) [_] _++_ [] ++-assoc ++-identityˡ ++-identityʳ

++-hom : Homomorphic₂ List→FreeM _++_ _•_
++-hom [] ys = sym (ε-identityˡ _)
++-hom (x ∷ xs) ys = cong (inj x •_) (++-hom xs ys) ∙ sym (•-assoc (inj x) (List→FreeM xs) (List→FreeM ys))

List→FreeM→List : retract List→FreeM FreeM→List
List→FreeM→List [] = refl
List→FreeM→List (x ∷ xs) = cong (x ∷_) (List→FreeM→List xs)

FreeM→List→FreeM : section List→FreeM FreeM→List
FreeM→List→FreeM = elim (λ _ → isSet→isGroupoid squash _ _) (λ _ → ε-identityʳ _) sectionOp refl
                    (λ _ _ _ → isOfHLevelPathP' 0 (squash _ _) _ _ .fst)
                    (λ _ → isOfHLevelPathP' 0 (squash _ _) _ _ .fst)
                    (λ _ → isOfHLevelPathP' 0 (squash _ _) _ _ .fst)
  where
    sectionOp : ∀ {x y} → List→FreeM (FreeM→List x) ≡ x →
                          List→FreeM (FreeM→List y) ≡ y →
                          List→FreeM (FreeM→List (x • y)) ≡ (x • y)
    sectionOp {x} {y} p q =
      List→FreeM (FreeM→List (x • y))                       ≡⟨⟩
      List→FreeM (FreeM→List x ++ FreeM→List y)             ≡⟨ ++-hom (FreeM→List x) (FreeM→List y) ⟩
      List→FreeM (FreeM→List x) • List→FreeM (FreeM→List y) ≡⟨ cong₂ _•_ p q ⟩
      x • y                                                 ∎

List≃FreeM : List A ≃ FreeM
List≃FreeM = isoToEquiv (iso List→FreeM FreeM→List FreeM→List→FreeM List→FreeM→List)

List≡FreeM : List A ≡ FreeM
List≡FreeM = ua List≃FreeM

------------------------------------------------------------------------
-- Monoid structure

FreeM-isMonoid : IsMonoid FreeM _•_ ε
FreeM-isMonoid = record
  { isSemigroup = record
      { isMagma = record { is-set = squash }
      ; assoc   = •-assoc
      }
  ; identity = ε-identity
  }

FreeMonoid : Monoid ℓ
FreeMonoid = record { isMonoid = FreeM-isMonoid }

EquivFreeM : MonoidEquiv ListMonoid FreeMonoid
EquivFreeM = record
  { eq    = List≃FreeM
  ; isHom = record
      { preservesOp = ++-hom
      ; preservesId = refl
      }
  }

FreeMonoid≡ : ListMonoid ≡ FreeMonoid
FreeMonoid≡ = uaMonoid EquivFreeM


text:
module SolveAll-Norm where

open import Common.Equality
open import Common.List
open import Common.Nat

example = 0 ∷ 1 ∷ 2 ∷ []

test1 : length example ≡ {!!}
test1 = refl

reverse : {A : Set} → List A → List A
reverse = go [] where

  go : {A : Set} → List A → List A → List A
  go acc []       = acc
  go acc (x ∷ xs) = go (x ∷ acc) xs

test2 : reverse example ≡ {!!}
test2 = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Agda.Primitive
open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Reflection

testQuote : quoteTerm Setω ≡ agda-sort (inf 0)
testQuote = refl

macro
  doUnquote : Term → Term → TC _
  doUnquote t hole = bindTC (unquoteTC t) (unify hole)

testUnquote : doUnquote (agda-sort (inf 0))
testUnquote = ∀ ℓ → Set ℓ

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Issue62 where

module A where

  data A : Set where
    a : A

module B where

  open A

  data B : Set where
    a : B

open B

-- Note that a : A.A is not in scope here, so the following should not
-- type check.

foo : A.A -> A.A
foo a = a


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

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

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.ProposalMsg as ProposalMsg
import      LibraBFT.Impl.Consensus.ConsensusTypes.VoteMsg     as VoteMsg
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.NetworkMsg
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Consensus.Network where

processProposal : {- NodeId → -} ProposalMsg → Epoch → ValidatorVerifier → Either (Either ErrLog InfoLog) Unit
processProposal {- peerId -} proposal myEpoch vv =
  case pProposal of λ where
    (Left e) → Left (Left e)
    (Right unit) →
      grd‖ proposal ^∙ pmProposal ∙ bEpoch == myEpoch ≔
           pure unit
         -- TODO : push this onto a queue if epoch is in future (is this still relevant?)
         ‖ proposal ^∙ pmProposal ∙ bEpoch == myEpoch + 1 ≔
           Left (Right fakeInfo) -- proposal in new epoch arrived before my epoch change
         ‖ otherwise≔
           Left (Left fakeErr)   -- proposal for wrong epoch
  where
  pProposal = do
    ProposalMsg.verify proposal vv
    -- Note that our model does not assume knowledge of who sends a message, and therefore we do not
    -- check that the proposal is *sent* by the given peer (of course it must be *signed* by the
    -- peer, which is verified elsewhere).  Our proof should not require this.
    {- lcheck (proposal ^∙ pmProposal ∙ bAuthor == just peerId) -}

processVote : {- NodeId → -} VoteMsg → Epoch → ValidatorVerifier → Either (Either ErrLog InfoLog) Unit
processVote {- peerId -} voteMsg myEpoch vv =
  case pVote of λ where
    (Left e) → Left (Left e)
    (Right unit) →
      grd‖ voteMsg ^∙ vmEpoch == myEpoch ≔
        pure unit
         -- IMPL-TODO : push this onto a queue if epoch is in future (is this still relevant?)
         -- NOTE : epoch might be mismatched because
         -- - vote for EpochChange proposal round + 2 arrives
         --   after leader already already formed a quorum
         -- - timeout votes for previous or subsequent epochs arrive after the epoch change
         ‖ voteMsg ^∙ vmVote ∙ vVoteData ∙ vdProposed ∙ biEpoch + 1 == myEpoch ≔
           Left (Right (fakeInfo {- (here $ "vote for previous epoch arrived after my epoch change" ∷ lsE myEpoch ∷ []) -}))
         ‖ voteMsg ^∙ vmVote ∙ vVoteData ∙ vdProposed ∙ biEpoch == myEpoch + 1 ≔
           Left (Right (fakeInfo {- (here $ "vote for previous epoch arrived before my epoch change" ∷ lsE myEpoch ∷ []) -}))
         ‖ otherwise≔
           Left (Left (fakeErr {- (here $ "vote for wrong epoch" ∷ lsE myEpoch ∷ [])-}))
  where
 -- here t = "Network" ∷ "processVote" ∷ lsVM voteMsg ∷ t

  pVote : Either ErrLog Unit
  pVote = do
 -- See comment above about checking which peer *sent* the message.
 -- lcheck (voteMsg ^∙ vmVote ∙ vAuthor == peerId)
 --        (here $ "vote received must be from the sending peer" ∷ lsA peerId ∷ [])
    VoteMsg.verify voteMsg vv


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Semirings.Definition

module Semirings.Lemmas {a : _} {A : Set a} {Zero One : A} {_+_ _*_ : A → A → A} (S : Semiring Zero One _+_ _*_) where

open Semiring S

doubleIsAddTwo : (a : A) → (a + a) ≡ (One + One) * a
doubleIsAddTwo a = transitivity (equalityCommutative (+WellDefined (productOneLeft a) (productOneLeft a))) (equalityCommutative (+DistributesOver*' One One a))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Integers
------------------------------------------------------------------------

module Data.Integer where

open import Data.Nat as ℕ
  using (ℕ) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
import Data.Nat.Show as ℕ
open import Data.Sign as Sign using (Sign) renaming (_*_ to _S*_)
open import Data.Product as Prod
open import Data.String using (String; _++_)
open import Function
open import Data.Sum as Sum
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; sym; cong; cong₂)
open PropEq.≡-Reasoning

infix  8 +_ -_
infixl 7 _*_ _⊓_
infixl 6 _+_ _-_ _⊖_ _⊔_
infix  4 _≤_ _≤?_

------------------------------------------------------------------------
-- The types

-- Integers.

data ℤ : Set where
  -[1+_] : (n : ℕ) → ℤ  -- -[1+ n ] stands for - (1 + n).
  +_     : (n : ℕ) → ℤ  -- + n stands for n.

------------------------------------------------------------------------
-- Conversions

-- Absolute value.

∣_∣ : ℤ → ℕ
∣ + n      ∣ = n
∣ -[1+ n ] ∣ = ℕ.suc n

-- Gives the sign. For zero the sign is arbitrarily chosen to be +.

sign : ℤ → Sign
sign (+ _)    = Sign.+
sign -[1+ _ ] = Sign.-

-- Decimal string representation.

show : ℤ → String
show i = showSign (sign i) ++ ℕ.show ∣ i ∣
  where
  showSign : Sign → String
  showSign Sign.- = "-"
  showSign Sign.+ = ""

------------------------------------------------------------------------
-- A view of integers as sign + absolute value

infix 5 _◂_ _◃_

_◃_ : Sign → ℕ → ℤ
_      ◃ ℕ.zero  = + ℕ.zero
Sign.+ ◃ n       = + n
Sign.- ◃ ℕ.suc n = -[1+ n ]

◃-left-inverse : ∀ i → sign i ◃ ∣ i ∣ ≡ i
◃-left-inverse -[1+ n ]    = refl
◃-left-inverse (+ ℕ.zero)  = refl
◃-left-inverse (+ ℕ.suc n) = refl

◃-cong : ∀ {i j} → sign i ≡ sign j → ∣ i ∣ ≡ ∣ j ∣ → i ≡ j
◃-cong {i} {j} sign-≡ abs-≡ = begin
  i               ≡⟨ sym $ ◃-left-inverse i ⟩
  sign i ◃ ∣ i ∣  ≡⟨ cong₂ _◃_ sign-≡ abs-≡ ⟩
  sign j ◃ ∣ j ∣  ≡⟨ ◃-left-inverse j ⟩
  j               ∎

data SignAbs : ℤ → Set where
  _◂_ : (s : Sign) (n : ℕ) → SignAbs (s ◃ n)

signAbs : ∀ i → SignAbs i
signAbs i = PropEq.subst SignAbs (◃-left-inverse i) $
              sign i ◂ ∣ i ∣

------------------------------------------------------------------------
-- Equality is decidable

infix 4 _≟_

_≟_ : Decidable {A = ℤ} _≡_
i ≟ j with Sign._≟_ (sign i) (sign j) | ℕ._≟_ ∣ i ∣ ∣ j ∣
i ≟ j | yes sign-≡ | yes abs-≡ = yes (◃-cong sign-≡ abs-≡)
i ≟ j | no  sign-≢ | _         = no (sign-≢ ∘ cong sign)
i ≟ j | _          | no abs-≢  = no (abs-≢  ∘ cong ∣_∣)

decSetoid : DecSetoid _ _
decSetoid = PropEq.decSetoid _≟_

------------------------------------------------------------------------
-- Arithmetic

-- Negation.

-_ : ℤ → ℤ
- (+ ℕ.suc n) = -[1+ n ]
- (+ ℕ.zero)  = + ℕ.zero
- -[1+ n ]    = + ℕ.suc n

-- Subtraction of natural numbers.

_⊖_ : ℕ → ℕ → ℤ
m       ⊖ ℕ.zero  = + m
ℕ.zero  ⊖ ℕ.suc n = -[1+ n ]
ℕ.suc m ⊖ ℕ.suc n = m ⊖ n

-- Addition.

_+_ : ℤ → ℤ → ℤ
-[1+ m ] + -[1+ n ] = -[1+ ℕ.suc (m ℕ+ n) ]
-[1+ m ] + +    n   = n ⊖ ℕ.suc m
+    m   + -[1+ n ] = m ⊖ ℕ.suc n
+    m   + +    n   = + (m ℕ+ n)

-- Subtraction.

_-_ : ℤ → ℤ → ℤ
i - j = i + - j

-- Successor.

suc : ℤ → ℤ
suc i = + 1 + i

private

  suc-is-lazy⁺ : ∀ n → suc (+ n) ≡ + ℕ.suc n
  suc-is-lazy⁺ n = refl

  suc-is-lazy⁻ : ∀ n → suc -[1+ ℕ.suc n ] ≡ -[1+ n ]
  suc-is-lazy⁻ n = refl

-- Predecessor.

pred : ℤ → ℤ
pred i = - + 1 + i

private

  pred-is-lazy⁺ : ∀ n → pred (+ ℕ.suc n) ≡ + n
  pred-is-lazy⁺ n = refl

  pred-is-lazy⁻ : ∀ n → pred -[1+ n ] ≡ -[1+ ℕ.suc n ]
  pred-is-lazy⁻ n = refl

-- Multiplication.

_*_ : ℤ → ℤ → ℤ
i * j = sign i S* sign j ◃ ∣ i ∣ ℕ* ∣ j ∣

-- Maximum.

_⊔_ : ℤ → ℤ → ℤ
-[1+ m ] ⊔ -[1+ n ] = -[1+ ℕ._⊓_ m n ]
-[1+ m ] ⊔ +    n   = + n
+    m   ⊔ -[1+ n ] = + m
+    m   ⊔ +    n   = + (ℕ._⊔_ m n)

-- Minimum.

_⊓_ : ℤ → ℤ → ℤ
-[1+ m ] ⊓ -[1+ n ] = -[1+ ℕ._⊔_ m n ]
-[1+ m ] ⊓ +    n   = -[1+ m ]
+    m   ⊓ -[1+ n ] = -[1+ n ]
+    m   ⊓ +    n   = + (ℕ._⊓_ m n)

------------------------------------------------------------------------
-- Ordering

data _≤_ : ℤ → ℤ → Set where
  -≤+ : ∀ {m n} → -[1+ m ] ≤ + n
  -≤- : ∀ {m n} → (n≤m : ℕ._≤_ n m) → -[1+ m ] ≤ -[1+ n ]
  +≤+ : ∀ {m n} → (m≤n : ℕ._≤_ m n) → + m ≤ + n

drop‿+≤+ : ∀ {m n} → + m ≤ + n → ℕ._≤_ m n
drop‿+≤+ (+≤+ m≤n) = m≤n

drop‿-≤- : ∀ {m n} → -[1+ m ] ≤ -[1+ n ] → ℕ._≤_ n m
drop‿-≤- (-≤- n≤m) = n≤m

_≤?_ : Decidable _≤_
-[1+ m ] ≤? -[1+ n ] = Dec.map′ -≤- drop‿-≤- (ℕ._≤?_ n m)
-[1+ m ] ≤? +    n   = yes -≤+
+    m   ≤? -[1+ n ] = no λ ()
+    m   ≤? +    n   = Dec.map′ +≤+ drop‿+≤+ (ℕ._≤?_ m n)

decTotalOrder : DecTotalOrder _ _ _
decTotalOrder = record
  { Carrier         = ℤ
  ; _≈_             = _≡_
  ; _≤_             = _≤_
  ; isDecTotalOrder = record
      { isTotalOrder = record
          { isPartialOrder = record
              { isPreorder = record
                  { isEquivalence = PropEq.isEquivalence
                  ; reflexive     = refl′
                  ; trans         = trans
                  }
                ; antisym  = antisym
              }
          ; total          = total
          }
      ; _≟_          = _≟_
      ; _≤?_         = _≤?_
      }
  }
  where
  module ℕO = DecTotalOrder ℕ.decTotalOrder

  refl′ : _≡_ ⇒ _≤_
  refl′ { -[1+ n ]} refl = -≤- ℕO.refl
  refl′ {+ n}       refl = +≤+ ℕO.refl

  trans : Transitive _≤_
  trans -≤+       (+≤+ n≤m) = -≤+
  trans (-≤- n≤m) -≤+       = -≤+
  trans (-≤- n≤m) (-≤- k≤n) = -≤- (ℕO.trans k≤n n≤m)
  trans (+≤+ m≤n) (+≤+ n≤k) = +≤+ (ℕO.trans m≤n n≤k)

  antisym : Antisymmetric _≡_ _≤_
  antisym -≤+       ()
  antisym (-≤- n≤m) (-≤- m≤n) = cong -[1+_] $ ℕO.antisym m≤n n≤m
  antisym (+≤+ m≤n) (+≤+ n≤m) = cong +_     $ ℕO.antisym m≤n n≤m

  total : Total _≤_
  total (-[1+ m ]) (-[1+ n ]) = [ inj₂ ∘′ -≤- , inj₁ ∘′ -≤- ]′ $ ℕO.total m n
  total (-[1+ m ]) (+    n  ) = inj₁ -≤+
  total (+    m  ) (-[1+ n ]) = inj₂ -≤+
  total (+    m  ) (+    n  ) = [ inj₁ ∘′ +≤+ , inj₂ ∘′ +≤+ ]′ $ ℕO.total m n

poset : Poset _ _ _
poset = DecTotalOrder.poset decTotalOrder

import Relation.Binary.PartialOrderReasoning as POR
module ≤-Reasoning = POR poset
  renaming (_≈⟨_⟩_ to _≡⟨_⟩_)


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

{-
Imports everything that is not imported by something else.
This is not supposed to be used anywhere, this is just a simple way to
do `make all'

This file is intentionally named index.agda so that
Agda will generate index.html.
-}

module index where

import Base
import Spaces.IntervalProps
import Algebra.F2NotCommutative
import Spaces.LoopSpaceCircle
import Spaces.LoopSpaceDecidableWedgeCircles
import Homotopy.PullbackIsPullback
import Homotopy.PushoutIsPushout
import Homotopy.Truncation
import Sets.QuotientUP
import Spaces.PikSn
import Homotopy.VanKampen
import Homotopy.Cover
import Homotopy.Cover.ExamplePi1Circle

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
data M : Set where
  m : (I : _) → (I → M) → M

-- inferred
-- m : (I : Set) → (I → M) → M

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --cubical --no-import-sorts --guardedness --safe #-}

module Cubical.Codata.M.AsLimit.itree where

open import Cubical.Data.Unit
open import Cubical.Data.Prod
open import Cubical.Data.Nat as ℕ using (ℕ ; suc ; _+_ )
open import Cubical.Data.Sum
open import Cubical.Data.Empty
open import Cubical.Data.Bool

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

open import Cubical.Codata.M.AsLimit.Container
open import Cubical.Codata.M.AsLimit.M
open import Cubical.Codata.M.AsLimit.Coalg

-- Delay monad defined as an M-type
delay-S : (R : Type₀) -> Container ℓ-zero
delay-S R = (Unit ⊎ R) , λ { (inr _) -> ⊥ ; (inl tt) -> Unit }

delay : (R : Type₀) -> Type₀
delay R = M (delay-S R)

delay-ret : {R : Type₀} -> R -> delay R
delay-ret r = in-fun (inr r , λ ())

delay-tau : {R : Type₀} -> delay R -> delay R
delay-tau S = in-fun (inl tt , λ x → S)

-- Bottom element raised
data ⊥₁ : Type₁ where

-- TREES
tree-S : (E : Type₀ -> Type₁) (R : Type₀) -> Container (ℓ-suc ℓ-zero)
tree-S E R = (R ⊎ (Σ[ A ∈ Type₀ ] (E A))) , (λ { (inl _) -> ⊥₁ ; (inr (A , e)) -> Lift A } )

tree : (E : Type₀ -> Type₁) (R : Type₀) -> Type₁
tree E R = M (tree-S E R)

tree-ret : ∀ {E} {R}  -> R -> tree E R
tree-ret {E} {R} r = in-fun (inl r , λ ())

tree-vis : ∀ {E} {R}  -> ∀ {A} -> E A -> (A -> tree E R) -> tree E R
tree-vis {A = A} e k = in-fun (inr (A , e) , λ { (lift x) -> k x } )

-- ITrees (and buildup examples)
-- https://arxiv.org/pdf/1906.00046.pdf
-- Interaction Trees: Representing Recursive and Impure Programs in Coq
-- Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic

itree-S : ∀ (E : Type₀ -> Type₁) (R : Type₀) -> Container (ℓ-suc ℓ-zero)
itree-S E R = ((Unit ⊎ R) ⊎ (Σ[ A ∈ Type₀ ] (E A))) , (λ { (inl (inl _)) -> Lift Unit ; (inl (inr _)) -> ⊥₁ ; (inr (A , e)) -> Lift A } )

itree :  ∀ (E : Type₀ -> Type₁) (R : Type₀) -> Type₁
itree E R = M (itree-S E R)

ret' : ∀ {E} {R}  -> R -> P₀ (itree-S E R) (itree E R)
ret' {E} {R} r = inl (inr r) , λ ()

tau' : {E : Type₀ -> Type₁} -> {R : Type₀} -> itree E R -> P₀ (itree-S E R) (itree E R)
tau' t = inl (inl tt) , λ x → t

vis' : ∀ {E} {R}  -> ∀ {A : Type₀} -> E A -> (A -> itree E R) -> P₀ (itree-S E R) (itree E R)
vis' {A = A} e k = inr (A , e) , λ { (lift x) -> k x }

ret : ∀ {E} {R}  -> R -> itree E R
ret = in-fun ∘ ret'

tau : {E : Type₀ -> Type₁} -> {R : Type₀} -> itree E R -> itree E R
tau = in-fun ∘ tau'

vis : ∀ {E} {R}  -> ∀ {A : Type₀} -> E A -> (A -> itree E R) -> itree E R
vis {A = A} e = in-fun ∘ (vis' {A = A} e)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Andreas, 2017-01-12

data D {A : Set} : A → Set where
  c : (a : A) → D {!!}  -- fill with a
  d : (a : A) → {!!}  -- fill with D a

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.Finite.Fin.Instance.Triangle where

open import Data.Nat using (ℕ)
open import Data.Fin
open import Data.Fin.Patterns
open import Relation.Binary.PropositionalEquality as ≡

open import Categories.Category.Finite.Fin
open import Categories.Category

private
  variable
    a b c d : Fin 3

-- the diagram is the following:
--
--  0
--  | \
--  |  \
--  |   \
--  |    \
--  v     v
--  1 ---> 2
--
-- all morphisms are 0 (because there is at most one morphism between each pair of objects).
TriangleShape : FinCatShape
TriangleShape = record
  { size     = 3
  ; ∣_⇒_∣    = morph
  ; hasShape = record
    { id        = id
    ; _∘_       = _∘_
    ; assoc     = assoc
    ; identityˡ = identityˡ
    ; identityʳ = identityʳ
    }
  }
  where morph : Fin 3 → Fin 3 → ℕ
        morph 0F 0F = 1
        morph 0F 1F = 1
        morph 0F 2F = 1
        morph 1F 1F = 1
        morph 1F 2F = 1
        morph 2F 2F = 1
        morph _ _   = 0

        id : Fin (morph a a)
        id {0F} = 0F
        id {1F} = 0F
        id {2F} = 0F

        _∘_ : ∀ {a b c} → Fin (morph b c) → Fin (morph a b) → Fin (morph a c)
        _∘_ {0F} {0F} {0F} 0F 0F = 0F
        _∘_ {0F} {0F} {1F} 0F 0F = 0F
        _∘_ {0F} {0F} {2F} 0F 0F = 0F
        _∘_ {0F} {1F} {1F} 0F 0F = 0F
        _∘_ {0F} {1F} {2F} 0F 0F = 0F
        _∘_ {0F} {2F} {2F} 0F 0F = 0F
        _∘_ {1F} {1F} {1F} 0F 0F = 0F
        _∘_ {1F} {1F} {2F} 0F 0F = 0F
        _∘_ {1F} {2F} {2F} 0F 0F = 0F
        _∘_ {2F} {2F} {2F} 0F 0F = 0F

        assoc : ∀ {f : Fin (morph a b)} {g : Fin (morph b c)} {h : Fin (morph c d)} →
                  ((h ∘ g) ∘ f) ≡ (h ∘ (g ∘ f))
        assoc {0F} {0F} {0F} {0F} {0F} {0F} {0F} = refl
        assoc {0F} {0F} {0F} {1F} {0F} {0F} {0F} = refl
        assoc {0F} {0F} {0F} {2F} {0F} {0F} {0F} = refl
        assoc {0F} {0F} {1F} {1F} {0F} {0F} {0F} = refl
        assoc {0F} {0F} {1F} {2F} {0F} {0F} {0F} = refl
        assoc {0F} {0F} {2F} {2F} {0F} {0F} {0F} = refl
        assoc {0F} {1F} {1F} {1F} {0F} {0F} {0F} = refl
        assoc {0F} {1F} {1F} {2F} {0F} {0F} {0F} = refl
        assoc {0F} {1F} {2F} {2F} {0F} {0F} {0F} = refl
        assoc {0F} {2F} {2F} {2F} {0F} {0F} {0F} = refl
        assoc {1F} {1F} {1F} {1F} {0F} {0F} {0F} = refl
        assoc {1F} {1F} {1F} {2F} {0F} {0F} {0F} = refl
        assoc {1F} {1F} {2F} {2F} {0F} {0F} {0F} = refl
        assoc {1F} {2F} {2F} {2F} {0F} {0F} {0F} = refl
        assoc {2F} {2F} {2F} {2F} {0F} {0F} {0F} = refl

        identityˡ : ∀ {f : Fin (morph a b)} → (id ∘ f) ≡ f
        identityˡ {0F} {0F} {0F} = refl
        identityˡ {0F} {1F} {0F} = refl
        identityˡ {0F} {2F} {0F} = refl
        identityˡ {1F} {1F} {0F} = refl
        identityˡ {1F} {2F} {0F} = refl
        identityˡ {2F} {2F} {0F} = refl

        identityʳ : ∀ {f : Fin (morph a b)} → (f ∘ id) ≡ f
        identityʳ {0F} {0F} {0F} = refl
        identityʳ {0F} {1F} {0F} = refl
        identityʳ {0F} {2F} {0F} = refl
        identityʳ {1F} {1F} {0F} = refl
        identityʳ {1F} {2F} {0F} = refl
        identityʳ {2F} {2F} {0F} = refl

Triangle : Category _ _ _
Triangle = FinCategory TriangleShape

module Triangle = Category Triangle

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Nats.Multiply.Assoc where

open import Nats
open import Equality
open import Function

open import Nats.Multiply.Comm
open import Nats.Multiply.Distrib

------------------------------------------------------------------------
-- internal stuffs

private

  a*1+b=a+a*b : ∀ a b → a * suc b ≡ a + a * b
  a*1+b=a+a*b a b
    rewrite nat-multiply-comm a $ suc b
          | nat-multiply-comm a b
            = refl

  a*/b*c/=/a*b/*c : ∀ a b c → a * b * c ≡ a * (b * c)
  a*/b*c/=/a*b/*c  zero   b c = refl
  a*/b*c/=/a*b/*c (suc a) b c
    rewrite a*/b*c/=/a*b/*c a b c
          | nat-multiply-comm a b
          | sym $ nat-multiply-distrib b (b * a) c
          | sym $ a*/b*c/=/a*b/*c a b c
          | nat-multiply-comm a b
            = refl

------------------------------------------------------------------------
-- public aliases

nat-multiply-assoc : ∀ a b c → a * b * c ≡ a * (b * c)
nat-multiply-assoc = a*/b*c/=/a*b/*c


text:
open import Reflection hiding (return; _>>=_)

open import Data.List renaming (_++_ to _++l_)
open import Data.Vec as V using (Vec; updateAt)
open import Data.Unit
open import Data.Nat as N
open import Data.Nat.Properties
open import Data.Fin using (Fin; #_; suc; zero)
open import Data.Maybe hiding (_>>=_; map)
open import Function
open import Data.Bool
open import Data.Product hiding (map)
open import Data.String renaming (_++_ to _++s_; concat to sconc; length to slen)
open import Data.Char renaming (_≈?_ to _c≈?_)

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
open import Relation.Nullary.Decidable hiding (map)
open import Data.Nat.Show renaming (show to showNat)

open import Level renaming (zero to lzero; suc to lsuc)

open import Category.Monad using (RawMonad)

open RawMonad {{...}} public

instance
  monadMB : ∀ {f} → RawMonad {f} Maybe
  monadMB = record { return = just ; _>>=_ = Data.Maybe._>>=_ }

  monadTC : ∀ {f} → RawMonad {f} TC
  monadTC = record { return = Reflection.return ; _>>=_ = Reflection._>>=_ }

data Err {a} (A : Set a) : Set a where
  error : String → Err A
  ok : A → Err A

instance
  monadErr : ∀ {f} → RawMonad {f} Err
  monadErr = record {
    return = ok ;
    _>>=_ = λ { (error s) f → error s ; (ok a) f → f a }
    }

record RawMonoid {a}(A : Set a) : Set a where
  field
    _++_ : A → A → A
    ε : A
  ++/_ : List A → A
  ++/ [] = ε
  ++/ (x ∷ a) = x ++ ++/ a

  infixr 5 _++_

open RawMonoid {{...}} public

instance
  monoidLst : ∀ {a}{A : Set a} → RawMonoid (List A)
  monoidLst {A = A} = record {
    _++_ = _++l_;
    ε = []
    }

  monoidStr : RawMonoid String
  monoidStr = record {
    _++_ = _++s_;
    ε = ""
    }

  monoidErrStr : RawMonoid (Err String)
  monoidErrStr = record {
    _++_ =  λ where
      (error s) _ → error s
      _ (error s) → error s
      (ok s₁) (ok s₂) → ok (s₁ ++ s₂)
    ;
    ε = ok ""
    }

  monoidErrLst : ∀{a}{A : Set a} → RawMonoid (Err $ List A)
  monoidErrLst = record {
    _++_ =  λ where
      (error s) _ → error s
      _ (error s) → error s
      (ok s₁) (ok s₂) → ok (s₁ ++ s₂)
    ;
    ε = ok []
    }

defToTerm : Name → Definition → List (Arg Term) → Term
defToTerm _ (function cs) as = pat-lam cs as
defToTerm _ (constructor′ d) as = con d as
defToTerm _ _ _ = unknown

derefImmediate : Term → TC Term
derefImmediate (def f args) = getDefinition f >>= λ f' → return (defToTerm f f' args)
derefImmediate x = return x

derefT : Term → TC Term
derefT (def f args) = getType f
derefT (con f args) = getType f
derefT x = return x

defName : Term → Maybe Name
defName (def f args) = just f
defName _ = nothing

Ctx = List $ Arg Type

pi-to-ctx : Term → Ctx

-- we have a Ctx for the entire function, now we want to build
-- a context for the given variables in the clause.  To do so
-- we merge function's ctx with patterns of the given clause
-- and we grab the types that correspond to the variables within
-- the patterns.
--pats-ctx : Ctx → (List $ Arg Pattern) → TC $ Maybe Ctx

macro
  reflect : Term → Term → TC ⊤
  reflect f a = (derefImmediate f)
                >>= quoteTC >>= unify a

  reflect-ty : Name → Type → TC ⊤
  reflect-ty f a = getType f >>= quoteTC >>= normalise >>= unify a

  rtest : Term → Term → TC ⊤
  rtest f a = do
     t ← derefT f
     v ← derefImmediate f
     --v ← pat-lam-no--rm v (pi-to-ctx t)
     --q ← quoteTC v
     q ← quoteTC (pi-to-ctx t)
     unify a q

  rmkstring : Term → Term → TC ⊤
  rmkstring f a = unify (lit (string "Test")) a

  infert : Type → Term → TC ⊤
  infert t a = inferType t >>= quoteTC >>= unify a

-- FIXME we probably want to error out on these two functions.
pi-to-ctx (Π[ s ∶ a ] x) = (a ∷ pi-to-ctx x)
pi-to-ctx _ = []

Prog = Err $ List String
infixl 5 _#p_
_#p_ = _++_

okl : String → Prog
okl s = ok ([ s ])

-- reduce a list of Progs with a delimiter
_/#p_ : List Prog → (delim : String) → Prog
[] /#p d = ok []
(x ∷ []) /#p d = x
(x ∷ xs@(_ ∷ _)) /#p d = x #p okl d #p xs /#p d

-- Normalise the name of functions that we obtain from showName,
-- i.e. remove dots, replace weird symbols by ascii.
nnorm : String → Prog
nnorm s = okl
        $ replace '.' '_'
        $ replace '-' '_'
        $ s
  where
    repchar : (t f x : Char) → Char
    repchar f t x with x c≈? f
    ... | yes _ = t
    ... | no  _ = x

    replace : (from to : Char) → String → String
    replace f t s = fromList $ map (repchar f t) $ toList s

data NumClauses : Set where
  Many One : NumClauses

record State : Set where
  constructor st
  field
    --arg-ctx     : Ctx
    --ret-typ     : String
    var-names   : List String
    retvar      : String
    cls         : NumClauses
open State

--compile-clause : Clause → State → Prog

-- Pack the information about new variables generated
-- by patterns in the clause, assignments to these,
-- and the list of conditions.  E.g.
--   foo : List ℕ → ℕ
--   foo (x ∷ xs) 2 = ...
--
-- Assume that we named top-level arguments [a, b]
-- Then, new variables for this clause are going to be
--     [x, xs]
-- Assignments are:
--     [x = hd a, xs = tl a]
-- Conditions are:
--     [is-cons a, b = 2]
record ClCond : Set where
  constructor clcond
  field
    vars    : List String
    assigns : List String
    conds   : List String

data MbClCond : Set where
  ok     : ClCond → MbClCond
  error  : String → MbClCond

_#c_ : MbClCond → MbClCond → MbClCond
error s #c _ = error s
_ #c error s = error s
ok (clcond a b c) #c ok (clcond a' b' c') = ok (clcond (a ++ a') (b ++ b') (c ++ c'))

{-# TERMINATING #-}
clause-ctx-vars : (pats : List $ Arg Pattern) → (vars : List String) → (counter : ℕ) → MbClCond

showLitProg : Literal → Prog

comp-term : Term → (varctx : List String) → Prog

sjoin : List String → String → String
sjoin [] delim = ""
sjoin (x ∷ []) delim = x
sjoin (x ∷ xs@(_ ∷ _)) delim = x ++s delim ++s sjoin xs delim

join' : List String → (delim : String) → (empty : String) → String
join' []        _ e = e
join' x@(_ ∷ _) d _ = sjoin x d

compile-cls : List Clause → State → Prog
compile-cls [] s = error "comile-cls: expected at least one clause"
compile-cls (clause ps t ∷ []) s with clause-ctx-vars ps (var-names s) 0
... | error msg = error msg
... | ok (clcond vars assgns conds) = let
        as = sconc (map (_++s "\n") assgns)
        rv = retvar s ++s " = "
    in okl (as ++s rv) #p comp-term t vars #p okl ";"
compile-cls (absurd-clause ps ∷ []) s with clause-ctx-vars ps (var-names s) 0
... | error msg = error msg
... | ok (clcond vars assgns conds) = okl "unreachable ();"
compile-cls (clause ps t ∷ xs@(_ ∷ _)) s with clause-ctx-vars ps (var-names s) 0
... | error msg = error msg
... | ok (clcond vars assgns conds) = let
        cs = join' conds " && " "true"
        as = sconc (map (_++s "\n") assgns)
        rv = retvar s ++s " = "
    in okl ("if (" ++s cs ++s ") {" ++s as ++s rv) #p comp-term t vars #p okl "; }"
       #p okl "else {"
       #p compile-cls xs s
       #p okl "}"
compile-cls (absurd-clause ps ∷ xs@(_ ∷ _)) s with clause-ctx-vars ps (var-names s) 0
... | error msg = error msg
... | ok (clcond vars assgns conds) = let
        -- XXX it would be weird if conds were empty... catch it?
        cs = join' conds " && " "true"
    in okl ("if (" ++s cs ++s ") { unreachable (); } else {" )
       #p compile-cls xs s
       #p okl "}"

clause-ctx-vars (arg i (con c ps) ∷ l) (v ∷ vars) vcnt with showName c
... | "Agda.Builtin.List.List.[]" =
           ok (clcond [] [] [ "emptyvec_p (" ++s v ++s ")" ])
           #c clause-ctx-vars l vars vcnt
... | "Agda.Builtin.List.List._∷_" =
           ok (clcond [] [] [ "nonemptyvec_p (" ++s v ++s ")" ])
           #c clause-ctx-vars (ps ++ l) (("hd (" ++s v ++s ")") ∷ ("tl (" ++s v ++s ")") ∷ vars) vcnt
... | "Agda.Builtin.Bool.Bool.true" =
           ok (clcond [] [] [ v {- == true -} ])
           #c clause-ctx-vars l vars vcnt
... | "Agda.Builtin.Bool.Bool.false" =
           ok (clcond [] [] [ "! " ++s v ])
           #c clause-ctx-vars l vars vcnt
... | "Agda.Builtin.Nat.Nat.suc" =
           ok (clcond [] [] [ v ++s " > 0" ])
           #c clause-ctx-vars (ps ++ l) ((v ++s " - 1") ∷ vars) vcnt
... | "Agda.Builtin.Nat.Nat.zero" =
           ok (clcond [] [] [ v ++s " == 0" ])
           #c clause-ctx-vars l vars vcnt
... | "Data.Fin.Base.Fin.zero" =
           ok (clcond [] [] [ v ++s " == 0" ])  -- XXX can also add v < u
           #c clause-ctx-vars l vars vcnt
... | "Data.Fin.Base.Fin.suc" =
           ok (clcond [] [] [ v ++s " > 0" ])  -- XXX can also add v < u
           #c clause-ctx-vars l vars vcnt
... | "Data.Vec.Base.Vec.[]"  =
           ok (clcond [] [] [ "emptyvec_p (" ++s v ++s ")" ])
           #c clause-ctx-vars l vars vcnt
... | "Data.Vec.Base.Vec._∷_" =
           ok (clcond [] [] [ "nonemptyvec_p (" ++s v ++s ")" ])
           #c clause-ctx-vars (ps ++ l) (("len (" ++s v ++s ") - 1") ∷ ("hd (" ++s v ++s ")") ∷ ("tl (" ++s v ++s ")") ∷ vars) vcnt
      -- Well, let's see how far we can go with this hack
... | "Array.Base.Ar.imap" =
--... | "test-extract.Ar'.imap" =
           ok (clcond [ "IMAP_" ++s v ] [ "\n#define IMAP_" ++s v ++s "(__x) " ++s v ++s "[__x]\n" ] [ "true" ])
           #c clause-ctx-vars l vars vcnt
... | x = error ("clause-ctx-vars: don't know what to do with `" ++s x ++s "` constructor in patterns")
clause-ctx-vars (arg i dot ∷ l) (v ∷ vars) vcnt =
           -- Dot patterns are skipped.
           clause-ctx-vars l vars vcnt
clause-ctx-vars (arg (arg-info visible r) (var s) ∷ l) (v ∷ vars) vcnt =
           -- If we have "_" as a variable, we need  to insert it
           -- into the list, but we don't generate an assignment for it.
           let asgn = case s ≈? "_" of λ where
                          -- XXX hopefully this is fine, otherwise
                          -- we can do the same thing as for hidden
                          -- vars.
                (yes p) → []
                (no ¬p) → [ s ++s " = " ++s v ++s ";" ]
           in ok (clcond [ s ] asgn [])
           #c clause-ctx-vars l vars vcnt
clause-ctx-vars (arg (arg-info hidden r) (var s) ∷ l) (v ∷ vars) vcnt =
           -- Hidden variables are simply added to the context
           -- as regular variables
           let s , vcnt = case s ≈? "_" of λ where
                (yes p) → s ++ "_" ++ showNat vcnt , 1 + vcnt
                (no ¬p) → s , vcnt
           in ok (clcond [ s ] [ s ++ " = " ++ v ++ ";" ] [])
           #c clause-ctx-vars l vars vcnt

clause-ctx-vars (arg (arg-info instance′ r) (var s) ∷ l) (v ∷ vars) vcnt =
           error "FIXME handle instance variables"
clause-ctx-vars (arg i (lit x) ∷ l) (v ∷ vars) vcnt =
           case showLitProg x of λ where
                (error s) → error s
                (ok s) → ok (clcond [] [] [ v ++s " == " ++s (sconc s) ])
                         #c clause-ctx-vars l vars vcnt
clause-ctx-vars (arg i (proj f) ∷ l) (v ∷ vars) vcnt =
           error "FIXME proj pattern"
clause-ctx-vars (arg i absurd ∷ l)  (v ∷ vars) vcnt =
           -- I assume that absurd can only appear in the
           -- absurd clause, therefore, we don't need a condition
           -- for this pattern, so we just skip it.
           clause-ctx-vars l vars vcnt
clause-ctx-vars [] [] _ =
           ok (clcond [] [] [])
clause-ctx-vars _  _  _ =
           error "mismatching number of patterns and types"

showLitProg (name x) = error ("Found name `" ++s (showName x) ++s "` as literal")
showLitProg (meta x) = error ("Found meta `" ++s (showMeta x) ++s "` as literal")
showLitProg x = okl (showLiteral x)

var-lkup : List String → ℕ → Prog
var-lkup [] n = error ("Variable not found")
var-lkup (x ∷ l) zero = okl x
var-lkup (x ∷ l) (suc n) = var-lkup l n

-- Compile each arg and join them with ", "
comp-arglist : List $ Arg Term → (varctx : List String) → Prog
comp-arglist args varctx = map (λ {(arg i x) → comp-term x varctx}) args /#p ", "

-- Helper for comp-arglist-mask
mk-mask : (n : ℕ) → List (Fin n) → List Bool
mk-mask n xs = V.toList $ go (V.replicate {n = n} false) xs
  where go : _ → _ → _
        go e [] = e
        go e (x ∷ xs) = go (updateAt x (λ _ → true) e) xs

comp-arglist-mask : List $ Arg Term → (mask : List Bool) → (varctx : List String) → Prog
comp-arglist-mask args mask varctx = go args mask varctx /#p ", "
  where
     go : List $ Arg Term → (mask : List Bool) → (varctx : List String) → List Prog
     go [] [] _ = []
     go [] (x ∷ mask) _ = [ error "Incorrect argument mask" ]
     go (x ∷ args) [] _ = [ error "Incorrect argument mask" ]
     go (x ∷ args) (false ∷ mask) vars = go args mask vars
     go (arg i x ∷ args) (true ∷ mask) vars = comp-term x vars ∷ go args mask vars

comp-term (var x []) vars = var-lkup (reverse vars) x
comp-term (var x args@(_ ∷ _)) vars = var-lkup (reverse vars) x #p okl "(" #p comp-arglist args vars #p okl ")"
--comp-term (var x (x₁ ∷ args)) vars with var-lkup (reverse vars) x
--comp-term (var x (x₁ ∷ args)) vars | ok l = error ("Variable " ++s (sconc l) ++s " used as a function call")
--comp-term (var x (x₁ ∷ args)) vars | error s = error s
comp-term (lit l) vars = showLitProg l
comp-term exp@(con c args) vars with showName c
... | "Data.Vec.Base.Vec.[]" =
      okl "[]"
... | "Data.Vec.Base.Vec._∷_" =
      okl "cons (" #p comp-arglist-mask args (mk-mask 5 $ # 3 ∷ # 4 ∷ []) vars #p okl ")"
... | "Agda.Builtin.Nat.Nat.suc" =
      okl "(1 + " #p comp-arglist-mask args (mk-mask 1 $ # 0 ∷ []) vars #p okl ")"
... | "Data.Fin.Base.Fin.zero" =
      okl "0"
... | "Data.Fin.Base.Fin.suc" =
      okl "(1 + " #p comp-arglist-mask args (mk-mask 2 $ # 1 ∷ []) vars #p okl ")"
... | "Array.Base.Ar.imap" =
--... | "test-extract.Ar'.imap" =
      case args of λ where
        (_ ∷ _ ∷ _ ∷ arg _ s ∷ arg _ (vLam x e) ∷ []) → let
             p = comp-term e (vars ++ [ x ])
             sh = comp-term s vars --infert exp
           in okl ("with { (. <= " ++s x ++s " <= .): ") #p p #p okl "; }:  genarray (" #p sh #p okl ")"
        _                               →
           error "comp-term: don't recognize arguments to imap"
... | "Array.Base.Ix.[]" =
      okl "[]"
... | "Array.Base.Ix._∷_" =
      okl "cons (" #p comp-arglist-mask args (mk-mask 5 $ # 3 ∷ # 4 ∷ []) vars #p okl ")"
... | n = error ("comp-term: don't know constructor `" ++s n ++s "`")
comp-term (def f args) vars with showName f
... | "Agda.Builtin.Nat._+_" =
      okl "_add_SxS_ (" #p comp-arglist args vars #p okl ")"
... | "Agda.Builtin.Nat._*_" =
      okl "_mul_SxS_ (" #p comp-arglist args vars #p okl ")"
... | "Data.Nat.DivMod._/_" =
      okl "_div_SxS_ (" #p comp-arglist-mask args (mk-mask 3 $ # 0 ∷ # 1 ∷ []) vars #p okl ")"
... | "Data.Fin.#_" =
      comp-arglist-mask args (mk-mask 3 $ # 0 ∷ []) vars
... | "Array.Base.ix-lookup" =
      case args of λ where
        (_ ∷ _ ∷ arg _ iv ∷ arg _ el ∷ []) → let
             iv′ = comp-term iv vars
             el′ = comp-term el vars
           in iv′ #p okl "[" #p el′ #p okl "]"
        _                                  →
           error "comp-term: don't recognize arguments to ix-lookup"
... | "Data.Vec.Base.[_]" =
      case args of λ where
        (_ ∷ _ ∷ arg _ x ∷ []) → okl "[" #p comp-term x vars #p  okl "]"
        _                      →
           error "comp-term: don't recognize arguments to Vec.[_]"

... | "Data.Fin.Base.raise" =
      -- Note that "raise" is a total junk, as it only makes sure that the
      -- Fin value is valid in some context; all we are interested in is the
      -- value of that Fin.
      case args of λ where
        (_ ∷ _ ∷ arg _ x ∷ []) → comp-term x vars
        _                      →
           error "comp-term: don't recognize arguments to Data.Fin.raise"

-- XXX we need to figure out what are we going to do with recursive functions,
--     as clearly its name can't be known in advance.  Probably add it to the
--     state?  Or maintain a list of functions?
... | n = nnorm n #p okl " ("  #p comp-arglist args vars #p okl ")"
--... | n = error ("comp-term: don't know definition `" ++s n ++s "`")
comp-term (lam v t) vars = error "comp-term: lambdas are not supported"
comp-term (pat-lam cs args) vars = error "comp-term: pattern-matching lambdas are not supported"
comp-term (pi a b) vars = error "comp-term: pi types are not supported"
comp-term (sort s) vars = error "comp-term: sorts are not supported"
comp-term (meta x x₁) vars = error "comp-term: metas are not supported"
comp-term unknown vars = error "comp-term: unknowns are not supported"

record Pistate : Set where
  constructor pist-vc=_cv=_vctx=_tctx=_rv=_ret=_cons=_
  field
    var-counter : ℕ
    cur-var : String
    var-ctx : List String
    type-ctx : List String
    ret-var : String
    ret : Prog
    -- XXX come up with a better type for
    -- constraints on variables.
    cons : List (String × Prog)
open Pistate

trav-pi : Type → Pistate → Pistate
trav-pi (Π[ s ∶ arg i x ] y) pst
          = let
              varname = case s of λ where
                          "_" → "x_" ++s (showNat $ var-counter pst)
                          n   → n
              tp = trav-pi x (record pst {cur-var = varname}) -- ; cons = []})
            in case ret tp of λ where
              (error s) → tp
              (ok l)    → trav-pi y (record pst {var-counter = 1 + var-counter pst ;
                                                 cur-var = ret-var pst ;
                                                 var-ctx = var-ctx pst ++ [ varname ] ;
                                                 type-ctx = type-ctx pst ++ [ (sjoin l "") ] ;
                                                 cons =  cons tp}) --cons pst ++ cons tp })
trav-pi (con c args) pst with showName c
... | x = record pst {ret = error ("trav-pi: don't know how to handle `" ++s x ++s "` constructor")}
trav-pi (def f args) pst with showName f
... | "Agda.Builtin.Nat.ℕ" = record pst {ret = okl "int"}
... | "Agda.Builtin.Nat.Nat" = record pst {ret = okl "int"}
... | "Agda.Builtin.Bool.Bool" = record pst {ret = okl "bool"}
... | "Agda.Builtin.List.List" =
         -- We encode lists as 1-d arrays of their argument type.
         case args of λ where
           (_ ∷ arg i x ∷ _) → let tp = trav-pi x (record pst {cons = []})
                               in case ret tp of λ where
                                   (error s) → tp
                                   (ok l)    → record tp {ret = okl $ (sjoin l "") ++s "[.]"}
           _                 → record pst {ret = error "trav-pi: incorrect arguments to List"}

... | "Data.Vec.Base.Vec" =
         -- Vectors are also 1-d arrays (such as lists) but we extract
         -- a bit of extra infromation from these.
         case args of λ where
           (_ ∷ arg _ t ∷ arg _ x ∷ []) → let tp = trav-pi t (record pst {cur-var = "" {- XXX well, typeof (cur-var pst) is the thing -}
                                                                          }) --cons = []})
                                              p = comp-term x (var-ctx pst)
                                          in record tp {ret = ret tp #p okl "[.]" ;
                                                        cons = (cons tp)
                                                            ++ [ cur-var pst ,
                                                                 okl ("/* assert (shape (" ++s (cur-var pst) ++s ")[[0]] == ") #p p #p okl ") */" ]
                                                       }
           _                            → record pst {ret = error "trav-pi: incorrect arguments to Vec"}
... | "Data.Fin.Base.Fin" =
         case args of λ where
           (arg _ x ∷ []) → let
                p = comp-term x (var-ctx pst)
                in record pst {
                     ret  = okl "int";
                     cons = (cons pst)
                         ++ [ cur-var pst ,
                              okl ("/* assert (" ++s (cur-var pst) ++s " < ") #p p #p okl ") */"]
                   }
           _              →
                record pst {ret = error "trav-pi: incorrect arguments to Fin"}
... | "Array.Base.Ar" =
--... | "test-extract.Ar'" =
         case args of λ where
           (_ ∷ arg _ ty ∷ arg _ dim ∷ arg _ sh ∷ []) → let
                  ty′  = trav-pi ty pst
                  dim′ = comp-term dim (var-ctx pst)
                  sh′  = comp-term sh (var-ctx pst)
                in record ty′ {
                     ret = ret ty′ #p okl "[*]" ;
                     cons = cons ty′
                         ++ [ cur-var pst ,
                              okl ("/* assert (dim (" ++s (cur-var pst) ++s ") == ") #p dim′ #p okl " )*/" ]
                         ++ [ cur-var pst ,
                              okl ("/* assert (shape (" ++s (cur-var pst) ++s ") == ") #p sh′ #p okl " )*/" ]
                   }
           _                                     →
                record pst {ret = error "trav-pi: incorrect arguments to Ar"}

... | x = record pst {ret = error ("trav-pi: don't know the `" ++s x ++s "` type")}
trav-pi _ pst = record pst {ret = error "trav-pi ERRR"}

find : List String → String → Bool
find [] x = false
find (y ∷ l) x with x ≈? y
... | yes _ = true
... | no _  = find l x

collect-var-cons : List (String × Prog) → (accum : List String) → List (String × Prog)
collect-var-cons [] acc = []
collect-var-cons ((x , v) ∷ l) acc with find acc x
... | true  = collect-var-cons l acc
... | false = (x , v #p collect l x) ∷ collect-var-cons l (x ∷ acc)
  where
     collect : _ → _ → _
     collect [] x = ok []
     collect ((y , v) ∷ l) x with y ≈? x
     ... | yes _ = v #p collect l x
     ... | no _ = collect l x

-- Get the value bound to the given variable or return (ok [])
lkup-var-cons : List (String × Prog) → String → Prog
lkup-var-cons [] s = ok []
lkup-var-cons ((x , v) ∷ xs) s with x ≈? s
... | yes _ = v
... | no  _ = lkup-var-cons xs s

fltr : List (String × Prog) → (var : String) → List (String × Prog)
fltr [] x = []
fltr ((y , v) ∷ l) x with x ≈? y
... | yes _ = fltr l x
... | no _ = (y , v) ∷ fltr l x

mkfun : Name → _ → Pistate → NumClauses → Prog
mkfun n cls ps nc = let
     rv = (ret-var ps)
     cs = collect-var-cons (cons ps) []
     arg-cons = map proj₂ $ fltr cs rv
     ret-cons = lkup-var-cons cs rv
  in (okl $ "// Function " ++s (showName n) ++s "\n")
  #p ret ps #p okl "\n"
  #p (nnorm $ showName n ++s "(")
  #p tvl (var-ctx ps) (type-ctx ps)
  #p okl ") {\n"
  --#p (cons ps) /#p "\n"
  #p arg-cons /#p "\n"
  #p ret ps #p okl (" " ++s rv ++s ";\n")
  #p compile-cls cls (st (var-ctx ps) rv nc)
  #p ret-cons
  #p okl ("return " ++s rv ++s ";\n}\n\n")
  where
    tvl : List String → List String → Prog
    tvl [] [] = ok []
    tvl [] (t ∷ typs) = error "more types than variables"
    tvl (x ∷ vars) [] = error "more variables than types"
    tvl (x ∷ []) (t ∷ []) = okl (t ++s " " ++s x)
    tvl (x ∷ []) (_ ∷ _ ∷ _) = error "more types than variables"
    tvl (_ ∷ _ ∷ _) (_ ∷ []) = error "more variables than types"
    tvl (x ∷ xs@(_ ∷ _)) (t ∷ ts@(_ ∷ _)) = okl (t ++s " " ++s x ++s ", ") #p tvl xs ts

compile' : (lam : Term) → (sig : Type) → (name : Maybe Name) → TC Prog
compile' (pat-lam cs args) t nm with nm
compile' (pat-lam cs args) t nm | nothing =
  return $ error "compile' got invalid function name"
compile' (pat-lam [] args) t nm | just x =
  return $ error "compile' got zero clauses in the lambda term"
compile' (pat-lam cs@(_ ∷ []) args) t nm | just x =
  -- XXX currently the name `__ret` is hardcoded.
  let ps = trav-pi t (pist-vc= 1 cv= "" vctx= [] tctx= [] rv= "__ret" ret= error "" cons= [])
  in return (mkfun x cs ps One)
compile' (pat-lam cs@(_ ∷ _ ∷ _) args) t nm | just x =
  -- XXX currently the name `__ret` is hardcoded.
  let ps = trav-pi t (pist-vc= 1 cv= "" vctx= [] tctx= [] rv= "__ret" ret= error "" cons= [])
  in return (mkfun x cs ps Many)
compile' x _ _  =
  return (error "compile' expected pattern-matching lambda")

macro
  compile : Term → Term → TC ⊤
  compile f a = do
     t ← derefT f
     v ← derefImmediate f
     let ctx = pi-to-ctx t
     let n = defName f
     --v ← pat-lam-norm v ctx
     let v = return v
     case v of λ where
       (ok v) → do
          v ← compile' v t n
          q ← quoteTC v
          unify a q
       e@(error s) →
          return e >>= quoteTC >>= unify a

---===== These are just all examples to play around ====---

tst-triv : ℕ → ℕ
tst-triv x = x + 1

-- Test pattern contraction
tst-ss : ℕ → ℕ
tst-ss (suc (suc x)) = x
tst-ss _ = 0

-- Here we have the (+ 0) in the last clause that
-- stays in the generated code.
tst-rew0 : ℕ → Bool → ℕ → ℕ
tst-rew0 x true y = let a = x * x in a + y
tst-rew0 x false y = x + 2 + 0

-- XXX can't do with clauses yet, but that shouldn
tst-with : ℕ → ℕ
tst-with x with x >? 0
tst-with x | yes p = 0
tst-with x | no ¬p = 1

-- Trivial test with Lists
lst-test : List ℕ → ℕ
lst-test [] = 0
lst-test (_∷_ x y) = x + 1

data Test : Set where
  cstctr : {x : ℕ} → x > 0 → Test

test-test : Test → ℕ
test-test (cstctr p) = 1

test-dot : (a : ℕ) → a > 0 → ℕ
test-dot a@(.(suc _)) (s≤s pf) = a

data Square : ℕ → Set where
  sq : (m : ℕ) → Square (m * m)

root : (m : ℕ) (n : ℕ) → Square n → ℕ
root a .(m * m) (sq m) =
  -- This is to show that square pattern is skipped
  -- from the context.  In the above case, the clause is
  -- represetned as: a , . , (sq m) ==ctx==> a , m
  -- and the expression is (var 0) + (var 1)
  m + a

open import Data.Vec hiding (concat)
tst-vec : ∀ {n} → Vec ℕ n → Vec ℕ (n + n * n) → ℕ
tst-vec [] _      = 0
tst-vec (x ∷ a) b = x

a = (reflect-ty tst-vec)

tst-undsc : _ → ℕ
tst-undsc n = 1 + n

vec-sum : ∀ {n} → Vec ℕ n → Vec ℕ (n) → Vec ℕ n
vec-sum [] _ = []
vec-sum (x ∷ a) (y ∷ b) = x + y ∷ vec-sum a b

vec-and-1 : ∀ {n} → Vec Bool n → Bool
vec-and-1 (x ∷ xs) = x ∧ vec-and-1 xs
vec-and-1 _ = true

vec-and : ∀ {n} → Vec Bool n → Vec Bool n → Vec Bool n
vec-and [] _ = []
vec-and (x ∷ a) (y ∷ b) = x ∧ y ∷ vec-and a b

vec-+ : ∀ {n} → Vec ℕ n → ℕ
vec-+ (x ∷ xs) = x + vec-+ xs
vec-+ _ = 0

f : ℕ → ℕ
f x = x * x

vec-tst : ∀ n → Vec ℕ (n) → ℕ
vec-tst 0 [] = 0
vec-tst (suc n) x = n * 2 -- (x ∷ xs) = n * 2

def-pst = (pist-vc= 1 cv= "" vctx= [] tctx= [] rv= "__ret" ret= error "" cons= []) --pist 1 [] [] (error "")

q : List String × List String × Prog
q = let (pist-vc= _ cv= _ vctx= v tctx= t rv= _ ret= r cons= _) = (trav-pi (reflect-ty vec-sum) def-pst) in (v , t , r)

--open import Data.Fin

xxx : Fin 5 → Fin 6
xxx zero = suc zero
xxx (suc _) = zero

fun-in-ty : (f : ℕ → ℕ) → Vec ℕ (f 3) → ℕ
fun-in-ty f x = 1 -- V.replicate 1

open import Array

data Ar' {a} (X : Set a) (d : ℕ) :  (Vec ℕ d) → Set a where
  imap : ∀ s → (Ix d s → X) → Ar' X d s

add-2v : ∀ {n} → let X = Ar ℕ 1 (n ∷ []) in X → X → X
add-2v (imap a) (imap b) = imap λ iv → a iv + b iv

postulate
  asum : ∀ {n} → Ar ℕ 1 (n ∷ []) → ℕ
  asum' : ∀ {n} → Ar' ℕ 1 (n ∷ []) → ℕ
  --sum (imap a)

mm : ∀ {m n k} → let Mat a b = Ar ℕ 2 (a ∷ b ∷ []) in
                 Mat m n → Mat n k → Mat m k
mm (imap a) (imap b) = imap λ iv → let i = ix-lookup iv (# 0)
                                       j = ix-lookup iv (# 1)
                                   in asum (imap λ kv → let k = ix-lookup kv (# 0)
                                                        in a (i ∷ k ∷ []) * b (k ∷ j ∷ []))

conv : ∀ {n} → let Ar1d n = Ar ℕ 1 V.[ n ] in
               Ar1d (3 + n) → Ar1d 3 → Ar1d (1 + n)
conv (imap inp) (imap ker) = imap λ iv → let i = ix-lookup iv (# 0)
                                         in (  inp (raise 2 i ∷ []) * ker (# 0 ∷ [])
                                             + inp (raise 1 (suc i) ∷ []) * ker (# 1 ∷ [])
                                             + inp (raise 0 (suc (suc i)) ∷ []) * ker (# 2 ∷ [])
                                            ) / 3
                                          where open import Data.Fin using (raise)
                                                open import Data.Nat.DivMod

test-fin : Fin 3 → Fin 4
test-fin x = suc x

w : String
w = case compile mm of λ where
     (error s) → s
     (ok l) → sjoin l ""

max_stars_repo_name: ashinkarov/agda-array

max_issues_repo_name: ashinkarov/agda-array

max_forks_repo_name: ashinkarov/agda-array


text:
{-# OPTIONS --without-K #-}
module hott.equivalence.logical where

open import sum
open import function.isomorphism.core
open import hott.level.core

_↔_ : ∀ {i j} → Set i → Set j → Set _
X ↔ Y = (X → Y) × (Y → X)

module _ {i j}{X : Set i}{Y : Set j} where
  ≅⇒↔ : X ≅ Y → X ↔ Y
  ≅⇒↔ φ = to , from
    where open _≅_ φ

  ↔⇒≅ : h 1 X → h 1 Y → X ↔ Y → X ≅ Y
  ↔⇒≅ hX hY (f , g) = iso f g (λ x → h1⇒prop hX _ x) (λ y → h1⇒prop hY _ y)

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base