text:
{-# OPTIONS --prop #-}

module Miscellaneous.ClassicalWitness where

open import Agda.Primitive using (Prop)

open import Data
open import Data.Either
open import Functional
import      Lvl
open import Type.Dependent
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable T A B Obj : Type{ℓ}
private variable P Q R : Prop(ℓ)
private variable Pred : T → Prop(ℓ)
private variable x y z : T

empty-prop : Empty{ℓ} → P
empty-prop ()

data Proof(P : Prop(ℓ)) : Type{ℓ} where
  intro : P → Proof(P)

data ⊥ : Prop(Lvl.𝟎) where

[⊥]-elim : ⊥ → P
[⊥]-elim ()

[⊥]-elim-type : ⊥ → T
[⊥]-elim-type ()

¬_ : Prop(ℓ) → Prop(ℓ)
¬ P = P → ⊥

data _∧_ (P : Prop(ℓ₁)) (Q : Prop(ℓ₂)) : Prop(ℓ₁ Lvl.⊔ ℓ₂) where
  [∧]-intro : P → Q → (P ∧ Q)

data _∨_ (P : Prop(ℓ₁)) (Q : Prop(ℓ₂)) : Prop(ℓ₁ Lvl.⊔ ℓ₂) where
  [∨]-introₗ : P → (P ∨ Q)
  [∨]-introᵣ : Q → (P ∨ Q)

[∨]-elim : (P → R) → (Q → R) → (P ∨ Q) → R
[∨]-elim pr qr ([∨]-introₗ p) = pr p
[∨]-elim pr qr ([∨]-introᵣ q) = qr q

data ∃ {Obj : Type{ℓ₁}} (P : Obj → Prop(ℓ₂)) : Prop(ℓ₁ Lvl.⊔ ℓ₂) where
  [∃]-intro : (witness : Obj) → ⦃ proof : P(witness) ⦄ → ∃(P)

[∃]-elim : (∀{x} → Pred(x) → P) → (∃ Pred) → P
[∃]-elim pr ([∃]-intro _ ⦃ p ⦄) = pr p

∃-empty-type : (∀{x : Obj} → Pred(x) → Empty{ℓ}) → ¬(∃{Obj = Obj} Pred)
∃-empty-type empty-p ep = [∃]-elim (\px → empty-prop (empty-p px)) ep

data Inhabited(T : Type{ℓ}) : Prop(Lvl.𝐒(ℓ)) where
  intro : T → Inhabited(T)

Inhabited-elim : (T → P) → (Inhabited(T) → P)
Inhabited-elim f (intro obj) = f(obj)

Inhabited-empty-type : (T → Empty{ℓ}) → (¬ Inhabited(T))
Inhabited-empty-type empty-T inhab-T = Inhabited-elim (\t → empty-prop(empty-T t)) inhab-T

∃-to-Inhabited : (∃{Obj = Obj} Pred) → Inhabited(Obj)
∃-to-Inhabited = [∃]-elim (\{x} _ → intro x)

data _≡_ {T : Type{ℓ}} : T → T → Prop(Lvl.of(T)) where
  refl : ∀{x} → (x ≡ x)

sym : ∀{x y : T} → (x ≡ y) → (y ≡ x)
sym refl = refl

subst : (P : T → Prop(ℓ)) → ∀{x y : T} → (x ≡ y) → (P(x) → P(y))
subst P refl = (\x → x)

data Singleton(T : Type{ℓ}) : Prop(Lvl.𝐒(ℓ)) where
  intro : (x : T) → (∀{y} → (x ≡ y)) → Singleton(T)

data ∃! {Obj : Type{ℓ₁}} (P : Obj → Prop(ℓ₂)) : Prop(ℓ₁ Lvl.⊔ ℓ₂) where
  [∃!]-intro : (witness : Obj) → ⦃ proof : P(witness) ⦄ → (∀{x} → P(x) → (witness ≡ x)) → ∃!(P)

[∃!]-elim : (∀{x} → Pred(x) → (∀{y} → (Pred(y)) → (x ≡ y)) → P) → (∃! Pred) → P
[∃!]-elim pr ([∃!]-intro _ ⦃ p ⦄ eq) = pr p eq

∃!-to-∃ : (∃!{Obj = Obj} Pred) → (∃{Obj = Obj} Pred)
∃!-to-∃ = [∃!]-elim (\{x} p _ → [∃]-intro x ⦃ p ⦄)

∃!-empty-type : (∀{x : Obj} → Pred(x) → Empty{ℓ}) → ¬(∃!{Obj = Obj} Pred)
∃!-empty-type empty-p ep = [∃!]-elim (\px → empty-prop (empty-p px)) ep

module WhenExcludedMiddle (excluded-middle : ∀{ℓ}(P : Prop(ℓ)) → (P ∨ (¬ P))) where
  {-[¬¬]-elim-type : ((T → ⊥) → ⊥) → T
  [¬¬]-elim-type {T = T} nnt with excluded-middle(T)
  ... | p = ?-}

  {-
  decidable : ∀{ℓ ℓₑ}(T : Type{ℓ}) → (T ‖ (T → Empty{ℓₑ}))
  decidable(T) = {!excluded-middle!}
  -}

  {-
  singleton-witness : Singleton(T) → T
  singleton-witness x = {!!}
  -}

module WhenDNEType ([¬¬]-elim-type : ∀{ℓ}{T : Type{ℓ}} → ((T → ⊥) → ⊥) → T) where
  inhabited-witness : Inhabited(T) → T
  inhabited-witness p = [¬¬]-elim-type (\nt → Inhabited-elim nt p)

module WhenDecidable {ℓₑ} (decidable : ∀{ℓ}(T : Type{ℓ}) → (T ‖ (T → Empty{ℓₑ}))) where
  excluded-middle : ∀{ℓ}(P : Prop(ℓ)) → (P ∨ (¬ P))
  excluded-middle(P) with decidable(Proof P)
  ... | Left (intro p) = [∨]-introₗ p
  ... | Right np       = [∨]-introᵣ (\p → empty-prop(np(intro p)))

  inhabited-witness : Inhabited(T) → T -- TODO: Are there any other ways (with weaker assumptions) of doing this?
  inhabited-witness{T = T} x with decidable(T)
  ... | Left  t  = t
  ... | Right nt = [⊥]-elim-type (Inhabited-empty-type nt x)

  ∃-to-Σ : (∃{Obj = Obj} Pred) → (Σ Obj (\p → Proof(Pred p)))
  ∃-to-Σ {Obj = Obj}{Pred = Pred} ep with decidable(Σ Obj (\p → Proof(Pred p)))
  ... | Left  s  = s
  ... | Right ns = [⊥]-elim-type (∃-empty-type (\{x} px → ns (intro x (intro px))) ep)

  [∃]-witness : (∃{Obj = Obj} Pred) → Obj
  [∃]-witness {Obj = Obj}{Pred = Pred} ep = Σ.left (∃-to-Σ ep)
  -- inhabited-witness(∃-to-Inhabited(∃!-to-∃ ep))

  [∃]-proof : (ep : ∃{Obj = Obj} Pred) → Pred([∃]-witness ep)
  [∃]-proof {Obj = Obj}{Pred = Pred} ep with intro p ← Σ.right (∃-to-Σ ep) = p
  -- [∃!]-elim (\p eq → subst(Pred) {!eq p!} p) ep

module WhenInhabitedWitness (inhabited-witness : ∀{ℓ}{T : Type{ℓ}} → Inhabited(T) → T) where
  [∨]-elim-type : (P → T) → (Q → T) → (P ∨ Q) → T
  [∨]-elim-type pt qt pq = inhabited-witness([∨]-elim (\t → intro(pt t)) (\t → intro(qt t)) pq)

  {-
  [∃]-witness : ∀{P : T → Prop(ℓ)} → (∃ P) → T -- TODO: Not really the witness. See TODO in [∃]-proof below
  [∃]-witness ep = inhabited-witness(∃-to-Inhabited ep)

  [∃]-proof : ∀{P : T → Prop(ℓ)} → (ep : ∃ P) → P([∃]-witness ep) -- TODO: Will not work because the witness obtained from `inhabited-witness` (this one is from `decidable`) can obviously be different from the one provided to prove (∃ P) (this one is from `[∃]-intro`). Though, a correct witness _is_ obtainable from (∃! P) as usual in classical logic.
  [∃]-proof{T = T} ep with decidable(T)
  ... | Left  t  = {!!}
  ... | Right nt = {!!}
  -}


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

open import Orders.Total.Definition
open import LogicalFormulae
open import Maybe

module KeyValue.LinearStore.Definition {a b : _} (keySet : Set a) (valueSet : Set b) {c : _} (keyOrder : TotalOrder keySet {c}) where

open import KeyValue.KeyValue keySet valueSet
open import KeyValue.LinearStore.Implementation keySet valueSet keyOrder

LinearStore : KeyValue Map
KeyValue.tryFind LinearStore = lookup
KeyValue.add LinearStore = addMap
KeyValue.empty LinearStore = empty
KeyValue.count LinearStore = count
KeyValue.lookupAfterAdd LinearStore empty k v with TotalOrder.totality keyOrder k k
KeyValue.lookupAfterAdd LinearStore empty k v | inl (inl x) = exFalso (TotalOrder.irreflexive keyOrder x)
KeyValue.lookupAfterAdd LinearStore empty k v | inl (inr x) = exFalso (TotalOrder.irreflexive keyOrder x)
KeyValue.lookupAfterAdd LinearStore empty k v | inr x = refl
KeyValue.lookupAfterAdd LinearStore (nonempty x) k v = lookupReducedSucceedsAfterAdd k v x
KeyValue.lookupAfterAdd' LinearStore empty k1 v k2 with TotalOrder.totality keyOrder k1 k2
KeyValue.lookupAfterAdd' LinearStore empty k1 v k2 | inl (inl x) = inr refl
KeyValue.lookupAfterAdd' LinearStore empty k1 v k2 | inl (inr x) = inr refl
KeyValue.lookupAfterAdd' LinearStore empty k1 v k2 | inr x = inl x
KeyValue.lookupAfterAdd' LinearStore (nonempty x) k1 v k2 with TotalOrder.totality keyOrder k1 k2
KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inl (inl x) with inspect (lookupReduced map k2)
KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inl (inl x) | no with≡ pr rewrite pr = inr (lookupReducedFailsAfterUnrelatedAdd k1 v k2 (inl x) map pr)
KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inl (inl x) | (yes lookedUp) with≡ pr rewrite pr = inr (lookupReducedSucceedsAfterUnrelatedAdd k1 v k2 lookedUp (inl x) map pr)
KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inl (inr x) with inspect (lookupReduced map k2)
KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inl (inr x) | no with≡ pr rewrite pr = inr (lookupReducedFailsAfterUnrelatedAdd k1 v k2 (inr x) map pr)
KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inl (inr x) | yes lookedUp with≡ pr rewrite pr = inr (lookupReducedSucceedsAfterUnrelatedAdd k1 v k2 lookedUp (inr x) map pr)
KeyValue.lookupAfterAdd' LinearStore (nonempty map) k1 v k2 | inr x = inl x
KeyValue.countAfterAdd' LinearStore empty _ _ _ = refl
KeyValue.countAfterAdd' LinearStore (nonempty x) k v = countReducedBehavesWhenAddingNotPresent k v x
KeyValue.countAfterAdd LinearStore empty _ _ _ ()
KeyValue.countAfterAdd LinearStore (nonempty map) k v1 v2 = countReducedBehavesWhenAddingPresent k v1 v2 map

ext: agda


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

module Algebra.Linear.Construct where

import Algebra.Linear.Construct.Vector
import Algebra.Linear.Construct.Matrix

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


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

open import HoTT
open import homotopy.HSpace

module homotopy.CircleHSpace where

S¹-hSpace : HSpaceStructure S¹
S¹-hSpace = hSpaceStructure base μ μ-e-l μ-e-r μ-coh where

  turn-around : (x : S¹) → x == x
  turn-around = S¹-elim loop (↓-idf=idf-in (∙=∙' loop loop))

  module Mu = S¹Rec (idf S¹) (λ= turn-around)

  μ : S¹ → S¹ → S¹
  μ = Mu.f

  μ-e-l : (x : S¹) → μ base x == x
  μ-e-l x = idp

  μ-e-r : (x : S¹) → μ x base == x
  μ-e-r = S¹-elim idp (↓-app=idf-in
    (idp ∙' loop                          =⟨ ∙'-unit-l loop ⟩
     loop                                 =⟨ idp ⟩
     turn-around base                     =⟨ ! (app=-β turn-around base) ⟩
     ap (λ z → z base) (λ= turn-around)   =⟨ ! (Mu.loop-β |in-ctx (ap (λ z → z base))) ⟩
     ap (λ z → z base) (ap μ loop)        =⟨ ! (ap-∘ (λ z → z base) μ loop) ⟩
     ap (λ z → μ z base) loop             =⟨ ! (∙-unit-r _) ⟩
     ap (λ z → μ z base) loop ∙ idp ∎))

  μ-coh = idp

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
open import Agda.Builtin.Nat

-- splitting on a 'with' argument should not expand the ellipsis
foo : Nat → Nat
foo m with 0
... | n = {!n!}

-- splitting on variable hidden by ellipsis should expand the ellipsis
bar : Nat → Nat
bar m with 0
... | n = {!m!}

-- test case with nested with
baz : Nat → Nat
baz m with m
... | n with n
... | p = {!p!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2017-11-01, issue #2824
-- Don't allow built-ins defined in parametrized modules

module _ {a} {A : Set a} where

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

  {-# BUILTIN EQUALITY _≡_ #-}

-- This is forbidden, could maybe allowed using lambda-lifting.


text:
import Common
import Global
import Local
import Projection
import Soundness
import Completeness

import Example

max_stars_repo_name: fangyi-zhou/mpst-in-agda

max_issues_repo_name: fangyi-zhou/mpst-in-agda

max_forks_repo_name: fangyi-zhou/mpst-in-agda


text:
{-# OPTIONS --show-implicit #-}
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality

postulate
  funext : {X : Set} {Y : X → Set} {f g : (x : X) → Y x} → (∀ x → f x ≡ g x) → f ≡ g

_::_ : {X : ℕ → Set} → X 0 → ((n : ℕ) → X (suc n)) → ((n : ℕ) → X n)
(x :: α) 0 = x
(x :: α) (suc n) = α n

hd : {X : ℕ → Set} → ((n : ℕ) → X n) → X 0
hd α = α 0

tl : {X : ℕ → Set} → ((n : ℕ) → X n) → ((n : ℕ) → X (suc n))
tl α n = α(suc n)

-- Needed to add the implicit arguments for funext in Agda 2.5.2:

hd-tl-eta : (X : ℕ → Set) {α : (n : ℕ) → X n} → (hd α :: tl α) ≡ α
hd-tl-eta X {α} = funext {Y = _} lemma
 where
  lemma : ∀ {α} → ∀ i → _::_ {_} (hd α) (tl α) i ≡ α i
  lemma 0 = refl
  lemma (suc i) = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Haskell.RangedSets.Ranges where

open import Haskell.Prim
open import Haskell.Prim.Ord
open import Haskell.Prim.Bool
open import Haskell.Prim.Maybe
open import Haskell.Prim.Enum
open import Haskell.Prim.Num
open import Haskell.Prim.Eq
open import Haskell.Prim.Functor
open import Haskell.Prim.Foldable
open import Haskell.Prim.Monoid
open import Haskell.Prim.Monad
open import Haskell.Prim.Applicative
open import Haskell.Prim.Int
open import Haskell.Prim.List
open import Haskell.Prim.Integer
open import Haskell.Prim.Real
open import Haskell.Prim.Show
open import Haskell.Prim.String
open import Haskell.Prim.Tuple

open import Haskell.RangedSets.Boundaries

{-# FOREIGN AGDA2HS
import Haskell.RangedSets.Boundaries
#-}

data Range (a : Set) ⦃ o : Ord a ⦄ ⦃ dio : DiscreteOrdered a ⦄ : Set where
    Rg : Boundary a → Boundary a → Range a
{-# COMPILE AGDA2HS Range #-}

rangeLower : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Range a → Boundary a

rangeUpper : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Range a → Boundary a

rangeIsEmpty : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a → Bool

emptyRange : ⦃  o : Ord a ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a

rangeHas : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a → a → Bool

rangeListHas : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → List (Range a) → a → Bool

fullRange : ⦃ o : Ord a ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a

singletonRange : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → a → Range a

rangeIsFull : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a → Bool

rangeOverlap : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a → Range a → Bool

rangeEncloses : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a → Range a → Bool

rangeUnion : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a → Range a → List (Range a)

rangeIntersection : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a → Range a → Range a

rangeDifference : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a → Range a → List (Range a)

rangeSingletonValue : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a → Maybe a

instance
    isRangeEq : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Eq (Range a)
    isRangeEq . _==_ r1 r2 = (rangeIsEmpty r1 && rangeIsEmpty r2) || (rangeLower r1 == rangeLower r2 && rangeUpper r1 == rangeUpper r2)
{-# COMPILE AGDA2HS isRangeEq #-}

instance
    isRangeOrd : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Ord (Range a)
    isRangeOrd . compare r1 r2 = if_then_else_ (r1 == r2) EQ
                        (if_then_else_ (rangeIsEmpty r1) LT (if_then_else_ (rangeIsEmpty r2) GT
                        (compare (rangeLower r1) (rangeUpper r1) <> compare (rangeLower r2) (rangeUpper r2))))
    isRangeOrd ._<_ x y = compare x y == LT
    isRangeOrd ._>_ x y = compare x y == GT
    isRangeOrd ._<=_ x y = (compare x y == LT) || (compare x y == EQ)
    isRangeOrd ._>=_ x y = (compare x y == GT) || (compare x y == EQ)
    isRangeOrd .max x y = if (compare x y == GT) then x else y
    isRangeOrd .min x y = if (compare x y == LT) then x else y
{-# COMPILE AGDA2HS isRangeOrd #-}

h : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → ⦃ Show a ⦄ → Boundary a → String
h BoundaryBelowAll = ""
h (BoundaryBelow x) = show x ++ " <= "
h (BoundaryAbove x) = show x ++ " < "
h BoundaryAboveAll = "show Range: lower bound is BoundaryAboveAll"
{-# COMPILE AGDA2HS h #-}

h2 : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → ⦃ Show a ⦄ → Boundary a → String
h2 BoundaryBelowAll = "show Range: upper bound is BoundaryBelowAll"
h2 (BoundaryBelow x) = " < " ++ show x
h2 (BoundaryAbove x) = " <= " ++ show x
h2 BoundaryAboveAll = ""
{-# COMPILE AGDA2HS h2 #-}

showHelper : ⦃ Show a ⦄ → ⦃  o : Ord a  ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Range a → Maybe a → String
showHelper r (Just v) = "x == " ++ show v
showHelper r Nothing = lowerBound ++ "x" ++ upperBound
         where
            lowerBound = h (rangeLower r)
            upperBound = h2 (rangeUpper r)
showHelper2 : ⦃ Show a ⦄ → ⦃  o : Ord a  ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Range a → String
showHelper2 r = if_then_else_ (rangeIsEmpty r) "Empty" (if_then_else_ (rangeIsFull r) "All x" (showHelper r (rangeSingletonValue r)))
{-# COMPILE AGDA2HS showHelper #-}
{-# COMPILE AGDA2HS showHelper2 #-}

instance
   isRangeShow : ⦃ Show a ⦄ → ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Show (Range a)
   isRangeShow .showsPrec _ = showString ∘ showHelper2
   isRangeShow .showList = defaultShowList (showString ∘ showHelper2)
{-# COMPILE AGDA2HS isRangeShow #-}

rangeLower ⦃ o ⦄ ⦃ dio ⦄ (Rg x y) = x
{-# COMPILE AGDA2HS rangeLower #-}

rangeUpper ⦃ o ⦄ ⦃ dio ⦄ (Rg x y) = y
{-# COMPILE AGDA2HS rangeUpper #-}

rangeIsEmpty r@(Rg lower upper) = upper <= lower
{-# COMPILE AGDA2HS rangeIsEmpty #-}

emptyRange = Rg BoundaryAboveAll BoundaryBelowAll
{-# COMPILE AGDA2HS emptyRange #-}

rangeHas r@(Rg b1 b2) v = (v />/ b1) && not (v />/ b2)
{-# COMPILE AGDA2HS rangeHas #-}

rangeHas1 : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → a → Range a → Bool
rangeHas1 v r@(Rg b1 b2) = (v />/ b1) && not (v />/ b2)

rangeListHas (r@(Rg _ _) ∷ []) v = rangeHas r v
rangeListHas (r1@(Rg _ _) ∷ r2@(Rg _ _) ∷ []) v = (rangeHas r1 v) || (rangeHas r2 v)
rangeListHas ls v = or $ map (\r → rangeHas r v) ls
{-# COMPILE AGDA2HS rangeListHas #-}

rangeListHas1 : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → a → List (Range a) → Bool
rangeListHas1 v (r@(Rg _ _) ∷ []) = rangeHas r v
rangeListHas1 v (r1@(Rg _ _) ∷ r2@(Rg _ _) ∷ []) = (rangeHas r1 v) || (rangeHas r2 v)
rangeListHas1 v ls = or $ map (\r → rangeHas r v) ls

fullRange ⦃ o ⦄ ⦃ dio ⦄ = Rg BoundaryBelowAll BoundaryAboveAll
{-# COMPILE AGDA2HS fullRange #-}

singletonRange v = Rg (BoundaryBelow v) (BoundaryAbove v)
{-# COMPILE AGDA2HS singletonRange #-}

rangeIsFull range = (range == fullRange)
{-# COMPILE AGDA2HS rangeIsFull #-}

rangeOverlap r1 r2 =
   not (rangeIsEmpty r1) && not (rangeIsEmpty r2) && not (rangeUpper r1 <= rangeLower r2 || rangeUpper r2 <= rangeLower r1)
{-# COMPILE AGDA2HS rangeOverlap #-}

rangeEncloses r1 r2 =
   (rangeLower r1 <= rangeLower r2 && rangeUpper r2 <= rangeUpper r1)
   || rangeIsEmpty r2
{-# COMPILE AGDA2HS rangeEncloses #-}

rangeIntersection r1@(Rg l1 u1) r2@(Rg l2 u2) = if_then_else_ (rangeIsEmpty r1 || rangeIsEmpty r2) emptyRange (Rg (max l1 l2) (min u1 u2))
{-# COMPILE AGDA2HS rangeIntersection #-}

rangeU2 : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a → Range a → List (Range a)
rangeU2 r1@(Rg l1 u1) r2@(Rg l2 u2) = (if_then_else_ touching ((Rg lower upper) ∷ []) (r1 ∷ r2 ∷ []))
   where
     touching = (max l1 l2) <= (min u1 u2)
     lower = min l1 l2
     upper = max u1 u2
{-# COMPILE AGDA2HS rangeU2 #-}

rangeU1 : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ → Range a → Range a → List (Range a)
rangeU1 r1@(Rg l1 u1) r2@(Rg l2 u2) = if_then_else_ (rangeIsEmpty r2) (r1 ∷ []) (rangeU2 r1 r2)
{-# COMPILE AGDA2HS rangeU1 #-}

rangeUnion r1@(Rg l1 u1) r2@(Rg l2 u2) = if_then_else_ (rangeIsEmpty r1) (r2 ∷ []) (rangeU1 r1 r2)
{-# COMPILE AGDA2HS rangeUnion #-}

rangeDifference (Rg lower1 upper1) (Rg lower2 upper2) = if_then_else_ intersects filtered (r1 ∷ [])
   where
      intersects = ((max lower1 lower2) < (min upper1 upper2))
      r1 = Rg lower1 upper1
      list = ((Rg lower1 lower2) ∷ (Rg upper2 upper1) ∷ [])
      filtered = filter (λ x → (rangeIsEmpty x) == false) list
{-# COMPILE AGDA2HS rangeDifference #-}

rangeSingletonValue (Rg (BoundaryBelow v1) (BoundaryBelow v2)) = if_then_else_ (adjacent v1 v2) (Just v1) Nothing
rangeSingletonValue (Rg (BoundaryBelow v1) (BoundaryAbove v2)) = if_then_else_ (v1 == v2) (Just v1) Nothing
rangeSingletonValue (Rg (BoundaryAbove v1) (BoundaryBelow v2)) = adjacentBelow v2 >>= λ x → adjacentBelow x >>= λ y → if_then_else_ (v1 == y) (return x) Nothing
rangeSingletonValue (Rg (BoundaryAbove v1) (BoundaryAbove v2)) = if_then_else_ (adjacent v1 v2) (Just v2) Nothing
rangeSingletonValue (Rg _ _) = Nothing
{-# COMPILE AGDA2HS rangeSingletonValue #-}


text:
open import Common.Prelude
open import Common.Reflect

id : Nat → Nat
id x = x

-- Used to give error:
-- unquote must be applied to a term
-- when checking that the expression unquote has type _3 x
i : Nat → Nat
i x = unquote (def (quote id) []) x

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


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

module hott.types.coproduct where

open import hott.core.universe

data _∐_ {ℓ₀ ℓ₁ : Level}
         (A : Type ℓ₀)
         (B : Type ℓ₁) : Type (ℓ₀ ⊔ ℓ₁)  where

     inl : (a : A) → A ∐ B -- left  introduction
     inr : (b : B) → A ∐ B -- right introduction

-- A more suggestive way of building elements of nested co-product
-- types. For example if we have a : A, b : B and c : C then the
-- expressions, a ∣∙, ∙∣ b ∣∙ and ∙∣ ∙∣ c are elements inl a, inr (inl
-- b) and inr (inr c) of A ∐ B ∐ C respectively.

_∣∙ : {ℓ₀ ℓ₁ : Level}{A : Type ℓ₀}{B : Type ℓ₁}
    → A → A ∐ B
_∣∙ = inl

∙∣_ : {ℓ₀ ℓ₁ : Level}{A : Type ℓ₀}{B : Type ℓ₁}
   → B → A ∐ B
∙∣_ = inr

infixr 0 ∙∣_
infixr 0 _∣∙

-- A more suggestive way of building a case by case analysis.
-- For example, one can just write f1 ∣ f2 ∣ f3
_∣_ : {a b c : Level}
      {A : Type a}
      {B : Type b}
      {C : Type c}
    → (A → C)
    → (B → C)
    → (A ∐ B → C)

(f ∣ g) (inl a) = f a
(f ∣ g) (inr b) = g b

infixr 0 _∐_
infixr 0 _∣_

-- Case by case analysis.
either : {ℓ₀ ℓ₁ ℓ₃ : Level}
         {A : Type ℓ₀}{B : Type ℓ₁}{C : Type ℓ₃}
       → (A → C) → (B → C) → (A ∐ B → C)
either f g (inl a) = f a
either f g (inr b) = g b

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


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

open import Generics.Prelude
open import Generics.Telescope
open import Generics.Desc
open import Generics.Mu
open import Generics.Mu.All

open import Data.Fin.Properties as Fin
open import Data.Product.Properties
open import Data.Empty
open import Relation.Nullary

module Generics.Mu.NoConfusion {P I n} {D : DataDesc P I n} where

private
  variable
    V : ExTele P
    p : ⟦ P ⟧tel tt
    v : ⟦ V ⟧tel p
    i : ⟦ I ⟧tel p

NoConfusionCon : (C : ConDesc P V I)
               → ⟦ C ⟧Conω (μ D) (p , v , i)
               → ⟦ C ⟧Conω (μ D) (p , v , i)
               → Setω
NoConfusionCon (var f) _ _ = ⊤ω
NoConfusionCon (π ai S C) (s₁ , x) (s₂ , y) =
  Σω (s₁ ≡ s₂) {!!}
NoConfusionCon (A ⊗ B) x y = {!!}

{-

module NoConfusion {P} {I : ExTele P} {n ℓ} (D : DataDesc P I ℓ n) where

  NoConfusionIndArg : ∀ {ℓ} (C : ConDesc P V I ℓ) {ℓ₂} {X : ⟦ P , I ⟧xtel → Set (ℓ ⊔ ℓ₂)}
                    → ∀ {pv} → (x y : ⟦ C ⟧IndArg ℓ₂ X pv) → Set (ℓ ⊔ ℓ₂)

  NoConfusionIndArgᵇ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (e : ℓ₁ ≡ ℓ₂ ⊔ ℓ₃) (i : ArgInfo)
                       {X : ⟦ P , I ⟧xtel → Set (ℓ₃ ⊔ ℓ₄)}
                       (S : ⟦ P , V ⟧xtel → Set ℓ₂)
                       (C : ConDesc P (V ⊢< i > S) I ℓ₃)
                     → ∀ {pv} (x y : IndArgᵇ ℓ₄ e i X S C pv) → Set (ℓ₁ ⊔ ℓ₄)

  NoConfusionIndArg (var i) x y = x ≡ y
  NoConfusionIndArg (A ⊗ B) (xa , xb) (ya , yb) = NoConfusionIndArg A xa ya × NoConfusionIndArg B xb yb
  NoConfusionIndArg (π p i S C) x y = NoConfusionIndArgᵇ p i S C x y

  NoConfusionIndArgᵇ refl i S C {pv} x y = x ≡ y

  NoConfusionConᵇ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (e : ℓ₁ ≡ ℓ₂ ⊔ ℓ₃) (i : ArgInfo)
                       {X : ⟦ P , I ⟧xtel → Set (ℓ₃ ⊔ ℓ₄)}
                       (S : ⟦ P , V ⟧xtel → Set ℓ₂)
                       (C : ConDesc P (V ⊢< i > S) I ℓ₃)
                     → ∀ {pvi} (x y : Conᵇ ℓ₄ e i X S C pvi) → Set (ℓ₁ ⊔ ℓ₄)

  NoConfusionCon (var i) x y = Lift _ ⊤
  NoConfusionCon (π p i S C) x y = NoConfusionConᵇ p i S C x y
  NoConfusionCon (A ⊗ B) (xa , xb) (ya , yb) = NoConfusionIndArg A xa ya × NoConfusionCon B xb yb

  NoConfusionConᵇ refl i S C (xs , xd) (ys , yd) = Σ (xs ≡ ys) λ { refl → NoConfusionCon C xd yd }

  NoConf : ∀ {ℓ′} {X : ⟦ P , I ⟧xtel → Set (ℓ ⊔ ℓ′)}
         → ∀ {pi} (x y : ⟦ D ⟧Data ℓ′ X pi) → Set (ℓ ⊔ ℓ′)
  NoConf (kx , x) (ky , y) with kx Fin.≟ ky
  ... | yes refl = NoConfusionCon (lookupCon D kx) x y
  ... | no _     = Lift _ ⊥

  noConfIndArg-refl : ∀ {ℓ} (C : ConDesc P V I ℓ) {ℓ₂} {X : ⟦ P , I ⟧xtel → Set (ℓ ⊔ ℓ₂)}
                    → ∀ {pvi} → (x : ⟦ C ⟧IndArg ℓ₂ X pvi) → NoConfusionIndArg C x x

  noConfIndArgᵇ-refl : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (e : ℓ₁ ≡ ℓ₂ ⊔ ℓ₃) (i : ArgInfo)
                       {X : ⟦ P , I ⟧xtel → Set (ℓ₃ ⊔ ℓ₄)}
                       (S : ⟦ P , V ⟧xtel → Set ℓ₂)
                       (C : ConDesc P (V ⊢< i > S) I ℓ₃)
                     → ∀ {pvi} (x : IndArgᵇ ℓ₄ e i X S C pvi) → NoConfusionIndArgᵇ e i S C x x

  noConfIndArg-refl (var i) x = refl
  noConfIndArg-refl (A ⊗ B) (xa , xb) = noConfIndArg-refl A xa , noConfIndArg-refl B xb
  noConfIndArg-refl (π p i S C) x = noConfIndArgᵇ-refl p i S C x

  noConfIndArgᵇ-refl refl i S C x = refl

  noConfCon-refl : ∀ {ℓ} (C : ConDesc P V I ℓ) {ℓ₂} {X : ⟦ P , I ⟧xtel → Set (ℓ ⊔ ℓ₂)}
                    → ∀ {pvi} → (x : ⟦_⟧Con C ℓ₂ X pvi) → NoConfusionCon C x x

  noConfConᵇ-refl : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (e : ℓ₁ ≡ ℓ₂ ⊔ ℓ₃) (i : ArgInfo)
                    {X : ⟦ P , I ⟧xtel → Set (ℓ₃ ⊔ ℓ₄)}
                    (S : ⟦ P , V ⟧xtel → Set ℓ₂)
                    (C : ConDesc P (V ⊢< i > S) I ℓ₃)
                  → ∀ {pvi} (x : Conᵇ ℓ₄ e i X S C pvi) → NoConfusionConᵇ e i S C x x

  noConfCon-refl (var i) x = lift tt
  noConfCon-refl (A ⊗ B) (xa , xb) = noConfIndArg-refl A xa , noConfCon-refl B xb
  noConfCon-refl (π p i S C) x = noConfConᵇ-refl p i S C x

  noConfConᵇ-refl refl i S C (_ , x) = refl , noConfCon-refl C x

  noConfIndArg : ∀ {ℓ} (C : ConDesc P V I ℓ) {ℓ₂} {X : ⟦ P , I ⟧xtel → Set (ℓ ⊔ ℓ₂)}
               → ∀ {pvi} {x y : ⟦ C ⟧IndArg ℓ₂ X pvi} → NoConfusionIndArg C x y → x ≡ y

  noConfIndArgᵇ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (e : ℓ₁ ≡ ℓ₂ ⊔ ℓ₃) (i : ArgInfo)
                  {X : ⟦ P , I ⟧xtel → Set (ℓ₃ ⊔ ℓ₄)}
                  (S : ⟦ P , V ⟧xtel → Set ℓ₂)
                  (C : ConDesc P (V ⊢< i > S) I ℓ₃)
                → ∀ {pvi} {x y : IndArgᵇ ℓ₄ e i X S C pvi} → NoConfusionIndArgᵇ e i S C x y → x ≡ y

  noConfIndArg (var i) nc = nc
  noConfIndArg (A ⊗ B) (nca , ncb) = cong₂ _,_ (noConfIndArg A nca) (noConfIndArg B ncb)
  noConfIndArg (π p i S C) nc = noConfIndArgᵇ p i S C nc

  noConfIndArgᵇ refl i S C nc = nc

  noConfCon : ∀ {ℓ} (C : ConDesc P V I ℓ) {ℓ₂} {X : ⟦ P , I ⟧xtel → Set (ℓ ⊔ ℓ₂)}
            → ∀ {pvi} → {x y : ⟦_⟧Con C ℓ₂ X pvi} → NoConfusionCon C x y → x ≡ y

  noConfConᵇ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (e : ℓ₁ ≡ ℓ₂ ⊔ ℓ₃) (i : ArgInfo)
               {X : ⟦ P , I ⟧xtel → Set (ℓ₃ ⊔ ℓ₄)}
               (S : ⟦ P , V ⟧xtel → Set ℓ₂)
               (C : ConDesc P (V ⊢< i > S) I ℓ₃)
             → ∀ {pvi} {x y : Conᵇ ℓ₄ e i X S C pvi} → NoConfusionConᵇ e i S C x y → x ≡ y

  noConfCon (var i) {x = lift refl} {lift refl} nc = refl
  noConfCon (A ⊗ B) (nca , ncb) = cong₂ _,_ (noConfIndArg A nca) (noConfCon B ncb)
  noConfCon (π p i S C) nc = noConfConᵇ p i S C nc

  noConfConᵇ refl i S C (refl , nc) = cong (_ ,_) (noConfCon C nc)

  noConf : ∀ {ℓ′} {X : ⟦ P , I ⟧xtel → Set (ℓ ⊔ ℓ′)}
         → ∀ {pi} {x y : ⟦ D ⟧Data ℓ′ X pi} → x ≡ y → NoConf x y
  noConf {x = kx , x} {ky , _} refl with kx Fin.≟ ky
  ... | yes refl = noConfCon-refl (lookupCon D kx) x
  ... | no kx≢kx = lift (kx≢kx refl)

  noConf₂ : ∀ {ℓ′} {X : ⟦ P , I ⟧xtel → Set (ℓ ⊔ ℓ′)}
          → ∀ {pi} {x y : ⟦ D ⟧Data ℓ′ X pi} → NoConf x y → x ≡ y
  noConf₂ {x = kx , x} {ky , y} nc with kx Fin.≟ ky
  ... | yes refl = cong (kx ,_) (noConfCon (lookupCon D kx) nc)
  ... | no kx≢ky = ⊥-elim (Lift.lower nc)

-}

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
module Numeral.Real where

import Lvl
open import Syntax.Number
open import Data
open import Functional
open import Logic.Propositional{Lvl.𝟎}
open import Logic.Predicate{Lvl.𝟎}{Lvl.𝟎}
open import Numeral.Integer hiding (𝟎)
open import Numeral.Natural
open import Sets.PredicateSet.Filter{Lvl.𝟎}{Lvl.𝟎}
open import Structure.Setoid{Lvl.𝟎}
open import Structure.Operator.Field{Lvl.𝟎}{Lvl.𝟎}
open import Structure.Operator.Group{Lvl.𝟎}{Lvl.𝟎}
open import Structure.Operator.Properties{Lvl.𝟎}{Lvl.𝟎}
open import Structure.Real{Lvl.𝟎}{Lvl.𝟎}
open import Structure.Relator.Ordering{Lvl.𝟎}{Lvl.𝟎}

-- TODO: Write it properly (maybe with a "construction of the reals"?). The following in this file is something to get this started

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- [The set]

postulate ℝ : Set

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- [Relations]

-- infixr 100 _≡_ _≢_ _<_ _>_ _≤_ _≥_ _<_<_

-- Equals
instance postulate [≡]-equiv : Equiv(ℝ)

-- Lesser than
postulate _<_ : ℝ → ℝ → Stmt

open From-[<][≡] (_<_) (_≡_) public

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- [Conversions]

record [ℝ]-conversion (T : Set) : Set where
  infixl 10000 #_
  field
    #_ : T → ℝ
open [ℝ]-conversion ⦃ ... ⦄ public

instance postulate [ℤ]-to-[ℝ] : [ℝ]-conversion(ℤ)
instance postulate [ℕ]-to-[ℝ] : [ℝ]-conversion(ℕ)

instance
  postulate ℝ-InfiniteNumeral : InfiniteNumeral (ℝ)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- [Subsets]

instance
  subset-to-[ℝ] : ∀{P} → [ℝ]-conversion(Filter{ℝ}(P))
  subset-to-[ℝ] {P} = record{#_ = f} where
    f : Filter{ℝ}(P) → ℝ
    f(subelem x) = x

-- Positive real numbers
ℝ₊ = Filter{ℝ}(x ↦ (x > 0))

-- Negative real numbers
ℝ₋ = Filter{ℝ}(x ↦ (x < 0))

-- Non-zero real numbers
ℝ₊₋ = Filter{ℝ}(x ↦ (x ≢ 0))

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- [Elements]

postulate e : ℝ
postulate π : ℝ

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- [Operators]

infixl 1000 _+_ _−_
infixl 1001 _⋅_ _/_
infixl 1002 _^_ _√_
postulate _+_ : ℝ → ℝ → ℝ
postulate _−_ : ℝ → ℝ → ℝ
postulate _⋅_ : ℝ → ℝ → ℝ
postulate _/_ : ℝ → ℝ → ℝ -- TODO: Some of these are partial functions/have smaller domains
postulate _^_ : ℝ → ℝ → ℝ
postulate log : ℝ → ℝ → ℝ
postulate _√_ : ℝ → ℝ → ℝ

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- [Functions]

abs : ℝ → ℝ
abs(x) = 2 √ (x ^ 2)

postulate sin : ℝ → ℝ

cos : ℝ → ℝ
cos(x) = sin(x − (π / 2))

tan : ℝ → ℝ
tan(x) = sin(x) / cos(x)

postulate asin : ℝ → ℝ
postulate acos : ℝ → ℝ
postulate atan : ℝ → ℝ

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- [Stuctures]

instance
  postulate [ℝ]-realTheory : RealTheory(_+_)(_⋅_)(_≤_)

instance
  postulate [ℝ][<]-strictPartialOrder : Strict.Order {ℝ} (_<_)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- [Properties of functions in ℝ]

instance postulate abs-positive : ∀{x} → (abs(x) ≥ 0)
instance postulate cos-periodicity : ∀{v}{n : ℕ} → (cos(v) ≡ cos(v + 2 ⋅ π ⋅ #(n)))
instance postulate sin-periodicity : ∀{v}{n : ℕ} → (sin(v) ≡ sin(v + 2 ⋅ π ⋅ #(n)))
instance postulate cos-even : ∀{v} → (cos(v) ≡ cos(0 − v))
instance postulate sin-odd  : ∀{v} → (sin(v) ≡ 0 − sin(0 − v))
instance postulate circle : ∀{v} → (cos(v) ^ 2 + sin(v) ^ 2 ≡ 1)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- [Properties on functions of ℝ]

-- postulate Axiom1 : {x y : ℝ} → (x < y) → ¬ (y < x)
-- postulate Axiom2 : {x z : ℝ} → (x < z) → ∃(y ↦ (x < y) ∧ (y < z))
-- postulate Axiom4 : {x y z : ℝ} → ((x + y) + z) ≡ (x + (y + z))
-- postulate Axiom5 : {x y : ℝ} → ∃(z ↦ (x + z) ≡ y)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- An ATP type must be used with data-types or postulates.

-- This error is detected by TypeChecking.Rules.Decl.

module ATPBadType2 where

foo : Set → Set
foo A = A

{-# ATP type foo #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


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

module Constructive.Common where

open import Level
open import Data.Product
open import Data.Sum
open import Function.Base
open import Relation.Nullary

infix 2 _<=>_

-- Logical equivalence
_<=>_ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
A <=> B = (A → B) × (B → A)

module _ {a b} {A : Set a} {B : Set b} where
  mk<=> : (A → B) → (B → A) → A <=> B
  mk<=> = _,_

  fwd : A <=> B → A → B
  fwd = proj₁

  bwd : A <=> B → B → A
  bwd = proj₂

_∘<=>_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
         B <=> C → A <=> B → A <=> C
(f , g) ∘<=> (h , i) = f ∘ h , i ∘ g

Stable : ∀ {a} → Set a → Set a
Stable A = ¬ ¬ A → A

Dec⊎ : ∀ {a} → Set a → Set a
Dec⊎ A = A ⊎ ¬ A

-- Unary decidable predicate
DecU : ∀ {a p} {A : Set a} → (A → Set p) → Set (a ⊔ p)
DecU P = ∀ x → P x ⊎ ¬ P x

Inhabited : ∀ {a} → Set a → Set a
Inhabited A = A


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

module Agda.Builtin.List where

infixr 5 _∷_
data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _∷_  #-}

{-# FOREIGN GHC type AgdaList a b = [b] #-}

{-# COMPILE GHC List = data MAlonzo.Code.Agda.Builtin.List.AgdaList ([] | (:)) #-}
{-# COMPILE UHC List = data __LIST__ (__NIL__ | __CONS__) #-}
{-# COMPILE JS  List = function(x,v) {
  if (x.length < 1) { return v["[]"](); } else { return v["_∷_"](x[0], x.slice(1)); }
} #-}
{-# COMPILE JS [] = Array() #-}
{-# COMPILE JS _∷_ = function (x) { return function(y) { return Array(x).concat(y); }; } #-}

max_stars_repo_name: Blaisorblade/Agda

max_issues_repo_name: Blaisorblade/Agda

max_forks_repo_name: Blaisorblade/Agda


text:
module Issue215 where

open import Imports.Bool

{-# COMPILED_DATA Bool Bool True False #-}

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Luau.VarCtxt where

open import Agda.Builtin.Equality using (_≡_)
open import Luau.Type using (Type; _∪_; _∩_)
open import Luau.Var using (Var)
open import FFI.Data.Aeson using (KeyMap; Key; empty; unionWith; singleton; insert; delete; lookup; toString; fromString; lookup-insert; lookup-insert-not; lookup-empty; to-from; insert-swap; insert-over)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Properties.Equality using (_≢_; cong; sym; trans)

VarCtxt : Set
VarCtxt = KeyMap Type

∅ : VarCtxt
∅ = empty

_⋒_ : VarCtxt → VarCtxt → VarCtxt
_⋒_ = unionWith _∩_

_⋓_ : VarCtxt → VarCtxt → VarCtxt
_⋓_ = unionWith _∪_

_[_] : VarCtxt → Var → Maybe Type
Γ [ x ] = lookup (fromString x) Γ

_⊝_ : VarCtxt → Var → VarCtxt
Γ ⊝ x = delete (fromString x) Γ

_↦_ : Var → Type → VarCtxt
x ↦ T = singleton (fromString x) T

_⊕_↦_ : VarCtxt → Var → Type → VarCtxt
Γ ⊕ x ↦ T = insert (fromString x) T Γ

⊕-over : ∀ {Γ x y T U} → (x ≡ y) → ((Γ ⊕ x ↦ T) ⊕ y ↦ U) ≡ (Γ ⊕ y ↦ U)
⊕-over p = insert-over _ _ _ _ _ (cong fromString (sym p))

⊕-swap : ∀ {Γ x y T U} → (x ≢ y) → ((Γ ⊕ x ↦ T) ⊕ y ↦ U) ≡ ((Γ ⊕ y ↦ U) ⊕ x ↦ T)
⊕-swap p = insert-swap _ _ _ _ _ (λ q → p (trans (sym (to-from _)) (trans (cong toString (sym q) ) (to-from _))) )

⊕-lookup-miss : ∀ x y T Γ → (x ≢ y) → (Γ [ y ] ≡ (Γ ⊕ x ↦ T) [ y ])
⊕-lookup-miss x y T Γ p = lookup-insert-not (fromString x) (fromString y) T Γ λ q → p (trans (sym (to-from x)) (trans (cong toString q) (to-from y)))

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
{-# OPTIONS --allow-unsolved-metas #-}
import cedille-options
module elaboration-helpers (options : cedille-options.options) where

open import lib
open import monad-instances
open import general-util
open import cedille-types
open import syntax-util
open import ctxt
open import conversion
open import constants
open import to-string options
open import subst
open import rename
open import is-free
open import toplevel-state options {id}
open import spans options {id}

uncurry' : ∀ {A B C D : Set} → (A → B → C → D) → (A × B × C) → D
uncurry' f (a , b , c) = f a b c

uncurry'' : ∀ {A B C D E : Set} → (A → B → C → D → E) → (A × B × C × D) → E
uncurry'' f (a , b , c , d) = f a b c d

uncurry''' : ∀ {A B C D E F : Set} → (A → B → C → D → E → F) → (A × B × C × D × E) → F
uncurry''' f (a , b , c , d , e) = f a b c d e

ctxt-term-decl' : posinfo → var → type → ctxt → ctxt
ctxt-term-decl' pi x T (mk-ctxt (fn , mn , ps , q) ss is os d) =
  mk-ctxt (fn , mn , ps , trie-insert q x (x , ArgsNil)) ss
    (trie-insert is x (term-decl T , fn , pi)) os d

ctxt-type-decl' : posinfo → var → kind → ctxt → ctxt
ctxt-type-decl' pi x k (mk-ctxt (fn , mn , ps , q) ss is os d) =
  mk-ctxt (fn , mn , ps , trie-insert q x (x , ArgsNil)) ss
    (trie-insert is x (type-decl k , fn , pi)) os d

ctxt-tk-decl' : posinfo → var → tk → ctxt → ctxt
ctxt-tk-decl' pi x (Tkt T) = ctxt-term-decl' pi x T
ctxt-tk-decl' pi x (Tkk k) = ctxt-type-decl' pi x k

ctxt-param-decl : var → var → tk → ctxt → ctxt
ctxt-param-decl x x' atk Γ @ (mk-ctxt (fn , mn , ps , q) ss is os ds) =
  let d = case atk of λ {(Tkt T) → term-decl T; (Tkk k) → type-decl k} in
  mk-ctxt
  (fn , mn , ps , trie-insert q x (x , ArgsNil)) ss
  (trie-insert is x' (d , fn , posinfo-gen)) os ds

ctxt-term-def' : var → var → term → type → opacity → ctxt → ctxt
ctxt-term-def' x x' t T op Γ @ (mk-ctxt (fn , mn , ps , q) ss is os d) = mk-ctxt
  (fn , mn , ps , qualif-insert-params q (mn # x) x ps) ss
  (trie-insert is x' (term-def (just ps) op (hnf Γ unfold-head t tt) T , fn , x)) os d

ctxt-type-def' : var → var → type → kind → opacity → ctxt → ctxt
ctxt-type-def' x x' T k op Γ @ (mk-ctxt (fn , mn , ps , q) ss is os d) = mk-ctxt
  (fn , mn , ps , qualif-insert-params q (mn # x) x ps) ss
  (trie-insert is x' (type-def (just ps) op (hnf Γ (unfolding-elab unfold-head) T tt) k , fn , x)) os d

ctxt-let-term-def : posinfo → var → term → type → ctxt → ctxt
ctxt-let-term-def pi x t T (mk-ctxt (fn , mn , ps , q) ss is os d) =
  mk-ctxt (fn , mn , ps , trie-insert q x (x , ArgsNil)) ss
    (trie-insert is x (term-def nothing OpacTrans t T , fn , pi)) os d

ctxt-let-type-def : posinfo → var → type → kind → ctxt → ctxt
ctxt-let-type-def pi x T k (mk-ctxt (fn , mn , ps , q) ss is os d) =
  mk-ctxt (fn , mn , ps , trie-insert q x (x , ArgsNil)) ss
    (trie-insert is x (type-def nothing OpacTrans T k , fn , pi)) os d

ctxt-kind-def' : var → var → params → kind → ctxt → ctxt
ctxt-kind-def' x x' ps2 k Γ @ (mk-ctxt (fn , mn , ps1 , q) ss is os d) = mk-ctxt
  (fn , mn , ps1 , qualif-insert-params q (mn # x) x ps1) ss
  (trie-insert is x' (kind-def (append-params ps1 $ qualif-params Γ ps2) k' , fn , posinfo-gen)) os d
  where
    k' = hnf Γ unfold-head k tt

ctxt-lookup-term-var' : ctxt → var → maybe type
ctxt-lookup-term-var' Γ @ (mk-ctxt (fn , mn , ps , q) ss is os d) x =
  env-lookup Γ x ≫=maybe λ where
    (term-decl T , _) → just T
    (term-def ps _ _ T , _ , x') →
      let ps = maybe-else ParamsNil id ps in
      just $ abs-expand-type ps T
    _ → nothing

-- TODO: Could there be parameter/argument clashes if the same parameter variable is defined multiple times?
-- TODO: Could variables be parameter-expanded multiple times?
ctxt-lookup-type-var' : ctxt → var → maybe kind
ctxt-lookup-type-var' Γ @ (mk-ctxt (fn , mn , ps , q) ss is os d) x =
  env-lookup Γ x ≫=maybe λ where
    (type-decl k , _) → just k
    (type-def ps _ _ k , _ , x') →
      let ps = maybe-else ParamsNil id ps in
      just $ abs-expand-kind ps k
    _ → nothing

subst-qualif : ∀ {ed : exprd} → ctxt → renamectxt → ⟦ ed ⟧ → ⟦ ed ⟧
subst-qualif{TERM} Γ ρ = subst-renamectxt Γ ρ ∘ qualif-term Γ
subst-qualif{TYPE} Γ ρ = subst-renamectxt Γ ρ ∘ qualif-type Γ
subst-qualif{KIND} Γ ρ = subst-renamectxt Γ ρ ∘ qualif-kind Γ
subst-qualif Γ ρ = id

rename-validify : string → string
rename-validify = 𝕃char-to-string ∘ (h ∘ string-to-𝕃char) where
  validify-char : char → 𝕃 char
  validify-char c with
    (c =char 'a')  ||
    (c =char 'z')  ||
    (c =char 'A')  ||
    (c =char 'Z')  ||
    (c =char '\'') ||
    (c =char '-')  ||
    (c =char '_')  ||
    is-digit c     ||
    (('a' <char c) && (c <char 'z')) ||
    (('A' <char c) && (c <char 'Z'))
  ...| tt = [ c ]
  ...| ff = 'Z' :: string-to-𝕃char (ℕ-to-string (toNat c)) ++ [ 'Z' ]
  h : 𝕃 char → 𝕃 char
  h [] = []
  h (c :: cs) = validify-char c ++ h cs

-- Returns a fresh variable name by adding primes and replacing invalid characters
fresh-var' : string → (string → 𝔹) → renamectxt → string
fresh-var' = fresh-var ∘ rename-validify

rename-new_from_for_ : ∀ {X : Set} → var → ctxt → (var → X) → X
rename-new "_" from Γ for f = f $ fresh-var' "x" (ctxt-binds-var Γ) empty-renamectxt
rename-new x from Γ for f = f $ fresh-var' x (ctxt-binds-var Γ) empty-renamectxt

rename_from_for_ : ∀ {X : Set} → var → ctxt → (var → X) → X
rename "_" from Γ for f = f "_"
rename x from Γ for f = f $ fresh-var' x (ctxt-binds-var Γ) empty-renamectxt

fresh-id-term : ctxt → term
fresh-id-term Γ = rename "x" from Γ for λ x → mlam x $ mvar x

get-renaming : renamectxt → var → var → var × renamectxt
get-renaming ρ xₒ x = let x' = fresh-var' x (renamectxt-in-range ρ) ρ in x' , renamectxt-insert ρ xₒ x'

rename_-_from_for_ : ∀ {X : Set} → var → var → renamectxt → (var → renamectxt → X) → X
rename xₒ - "_" from ρ for f = f "_" ρ
rename xₒ - x from ρ for f = uncurry f $ get-renaming ρ xₒ x

rename_-_lookup_for_ : ∀ {X : Set} → var → var → renamectxt → (var → renamectxt → X) → X
rename xₒ - x lookup ρ for f with renamectxt-lookup ρ xₒ
...| nothing = rename xₒ - x from ρ for f
...| just x' = f x' ρ

qualif-new-var : ctxt → var → var
qualif-new-var Γ x = ctxt-get-current-modname Γ # x

mbeta : term → term → term
mrho : term → var → type → term → term
mtpeq : term → term → type
mbeta t t' = Beta posinfo-gen (SomeTerm t posinfo-gen) (SomeTerm t' posinfo-gen)
mrho t x T t' = Rho posinfo-gen RhoPlain NoNums t (Guide posinfo-gen x T) t'
mtpeq t1 t2 = TpEq posinfo-gen t1 t2 posinfo-gen

subst-args-params : ctxt → args → params → kind → kind
subst-args-params Γ (ArgsCons (TermArg _ t) ys) (ParamsCons (Decl _ _ _ x _ _) ps) k =
  subst-args-params Γ ys ps $ subst Γ t x k
subst-args-params Γ (ArgsCons (TypeArg t) ys) (ParamsCons (Decl _ _ _ x _ _) ps) k =
  subst-args-params Γ ys ps $ subst Γ t x k
subst-args-params Γ ys ps k = k

data indx : Set where
  Index : var → tk → indx

data ctr : Set where
  Ctr : var → type → ctr

parameters = 𝕃 decl
indices = 𝕃 indx
constructors = 𝕃 ctr

data datatype : Set where
  Data : var → parameters → indices → constructors → datatype

params-to-parameters : params → parameters
params-to-parameters ParamsNil = []
params-to-parameters (ParamsCons p ps) = p :: params-to-parameters ps

{-# TERMINATING #-}
decompose-arrows : ctxt → type → parameters × type
decompose-arrows Γ (Abs pi me pi' x atk T) =
  rename-new x from Γ for λ x' →
  case decompose-arrows (ctxt-var-decl x' Γ) (rename-var Γ x x' T) of λ where
    (ps , T') → Decl posinfo-gen posinfo-gen me x' atk posinfo-gen :: ps , T'
decompose-arrows Γ (TpArrow T me T') =
  rename-new "_" from Γ for λ x →
  case decompose-arrows (ctxt-var-decl x Γ) T' of λ where
    (ps , T'') → Decl posinfo-gen posinfo-gen me x (Tkt T) posinfo-gen :: ps , T''
decompose-arrows Γ (TpParens pi T pi') = decompose-arrows Γ T
decompose-arrows Γ T = [] , T

decompose-ctr-type : ctxt → type → type × parameters × 𝕃 tty
decompose-ctr-type Γ T with decompose-arrows Γ T
...| ps , Tᵣ with decompose-tpapps Tᵣ
...| Tₕ , as = Tₕ , ps , as

{-# TERMINATING #-}
kind-to-indices : ctxt → kind → indices
kind-to-indices Γ (KndArrow k k') =
  rename "x" from Γ for λ x' →
  Index x' (Tkk k) :: kind-to-indices (ctxt-var-decl x' Γ) k'
kind-to-indices Γ (KndParens pi k pi') = kind-to-indices Γ k
kind-to-indices Γ (KndPi pi pi' x atk k) =
  rename x from Γ for λ x' →
  Index x' atk :: kind-to-indices (ctxt-var-decl x' Γ) k
kind-to-indices Γ (KndTpArrow T k) =
  rename "x" from Γ for λ x' →
  Index x' (Tkt T) :: kind-to-indices (ctxt-var-decl x' Γ) k
kind-to-indices Γ (KndVar pi x as) with ctxt-lookup-kind-var-def Γ x
...| nothing = []
...| just (ps , k) = kind-to-indices Γ $ subst-args-params Γ as ps k
kind-to-indices Γ (Star pi) = []

dataConsts-to-ctrs : dataConsts → constructors
dataConsts-to-ctrs DataNull = []
dataConsts-to-ctrs (DataCons (DataConst _ x T) cs) = Ctr x T :: dataConsts-to-ctrs cs

defDatatype-to-datatype : ctxt → defDatatype → datatype
defDatatype-to-datatype Γ (Datatype _ _ x ps k dcs _) =
  Data x (params-to-parameters ps) (kind-to-indices Γ k) (dataConsts-to-ctrs dcs)

indices-to-kind : indices → kind → kind
indices-to-kind = flip $ foldr λ {(Index x atk) → KndPi posinfo-gen posinfo-gen x atk}

parameters-to-kind : parameters → kind → kind
parameters-to-kind = flip $ foldr λ {(Decl pi pi' me x atk pi'') → KndPi pi pi' x atk}

indices-to-tplams : indices → (body : type) → type
indices-to-tplams = flip $ foldr λ where
  (Index x atk) → TpLambda posinfo-gen posinfo-gen x atk

parameters-to-tplams : parameters → (body : type) → type
parameters-to-tplams = flip $ foldr λ where
  (Decl pi pi' me x atk pi'') → TpLambda pi pi' x atk

indices-to-alls : indices → (body : type) → type
indices-to-alls = flip $ foldr λ where
  (Index x atk) → Abs posinfo-gen Erased posinfo-gen x atk

parameters-to-alls : parameters → (body : type) → type
parameters-to-alls = flip $ foldr λ where
  (Decl pi pi' me x atk pi'') → Abs pi me pi' x atk

indices-to-lams : indices → (body : term) → term
indices-to-lams = flip $ foldr λ where
  (Index x atk) → Lam posinfo-gen Erased posinfo-gen x (SomeClass atk)

indices-to-lams' : indices → (body : term) → term
indices-to-lams' = flip $ foldr λ where
  (Index x atk) → Lam posinfo-gen Erased posinfo-gen x NoClass

parameters-to-lams : parameters → (body : term) → term
parameters-to-lams = flip $ foldr λ where
  (Decl pi pi' me x atk pi'') → Lam pi me pi' x (SomeClass atk)

parameters-to-lams' : parameters → (body : term) → term
parameters-to-lams' = flip $ foldr λ where
  (Decl pi pi' me x atk pi'') → Lam pi me pi' x NoClass

indices-to-apps : indices → (body : term) → term
indices-to-apps = flip $ foldl λ where
  (Index x (Tkt T)) t → App t Erased (mvar x)
  (Index x (Tkk k)) t → AppTp t (mtpvar x)

parameters-to-apps : parameters → (body : term) → term
parameters-to-apps = flip $ foldl λ where
  (Decl pi pi' me x (Tkt T) pi'') t → App t me (mvar x)
  (Decl pi pi' me x (Tkk k) pi'') t → AppTp t (mtpvar x)

indices-to-tpapps : indices → (body : type) → type
indices-to-tpapps = flip $ foldl λ where
  (Index x (Tkt T)) T' → TpAppt T' (mvar x)
  (Index x (Tkk k)) T  → TpApp  T  (mtpvar x)

parameters-to-tpapps : parameters → (body : type) → type
parameters-to-tpapps = flip $ foldl λ where
  (Decl pi pi' me x (Tkt T) pi'') T' → TpAppt T' (mvar x)
  (Decl pi pi' me x (Tkk k) pi'') T  → TpApp  T  (mtpvar x)

constructors-to-lams' : constructors → (body : term) → term
constructors-to-lams' = flip $ foldr λ where
  (Ctr x T) → Lam posinfo-gen NotErased posinfo-gen x NoClass

constructors-to-lams : ctxt → var → parameters → constructors → (body : term) → term
constructors-to-lams Γ x ps cs t = foldr
  (λ {(Ctr y T) f Γ → Lam posinfo-gen NotErased posinfo-gen y
    (SomeClass $ Tkt $ subst Γ (parameters-to-tpapps ps $ mtpvar y) y T)
    $ f $ ctxt-var-decl y Γ})
  (λ Γ → t) cs Γ

add-indices-to-ctxt : indices → ctxt → ctxt
add-indices-to-ctxt = flip $ foldr λ {(Index x atk) → ctxt-var-decl x}

add-parameters-to-ctxt : parameters → ctxt → ctxt
add-parameters-to-ctxt = flip $ foldr λ {(Decl _ _ _ x'' _ _) → ctxt-var-decl x''}

add-constructors-to-ctxt : constructors → ctxt → ctxt
add-constructors-to-ctxt = flip $ foldr λ where
  (Ctr x T) → ctxt-var-decl x

module reindexing (Γ : ctxt) (isₒ : indices) where

  reindex-fresh-var : renamectxt → trie indices → var → var
  reindex-fresh-var ρ is "_" = "_"
  reindex-fresh-var ρ is x =
    fresh-var x (λ x' → ctxt-binds-var Γ x' || trie-contains is x') ρ

  rename-indices : renamectxt → trie indices → indices
  rename-indices ρ is = foldr {B = renamectxt → indices}
    (λ {(Index x atk) f ρ →
       let x' = reindex-fresh-var ρ is x in
       Index x' (substh-tk {TERM} Γ ρ empty-trie atk) :: f (renamectxt-insert ρ x x')})
    (λ ρ → []) isₒ ρ

  reindex-t : Set → Set
  reindex-t X = renamectxt → trie indices → X → X

  reindex : ∀ {ed} → reindex-t ⟦ ed ⟧
  reindex-term : reindex-t term
  reindex-type : reindex-t type
  reindex-kind : reindex-t kind
  reindex-tk : reindex-t tk
  reindex-liftingType : reindex-t liftingType
  reindex-optTerm : reindex-t optTerm
  reindex-optType : reindex-t optType
  reindex-optGuide : reindex-t optGuide
  reindex-optClass : reindex-t optClass
  reindex-lterms : reindex-t lterms
  reindex-args : reindex-t args
  reindex-arg : reindex-t arg
  reindex-theta : reindex-t theta
  reindex-vars : reindex-t (maybe vars)
  reindex-defTermOrType : renamectxt → trie indices → defTermOrType → defTermOrType × renamectxt

  reindex{TERM} = reindex-term
  reindex{TYPE} = reindex-type
  reindex{KIND} = reindex-kind
  reindex{TK}   = reindex-tk
  reindex       = λ ρ is x → x

  rc-is : renamectxt → indices → renamectxt
  rc-is = foldr λ {(Index x atk) ρ → renamectxt-insert ρ x x}

  index-var = "indices"
  index-type-var = "Indices"
  is-index-var = isJust ∘ is-pfx index-var
  is-index-type-var = isJust ∘ is-pfx index-type-var

  reindex-term ρ is (App t me (Var pi x)) with trie-lookup is x
  ...| nothing = App (reindex-term ρ is t) me (reindex-term ρ is (Var pi x))
  ...| just is' = indices-to-apps is' $ reindex-term ρ is t
  reindex-term ρ is (App t me t') =
    App (reindex-term ρ is t) me (reindex-term ρ is t')
  reindex-term ρ is (AppTp t T) =
    AppTp (reindex-term ρ is t) (reindex-type ρ is T)
  reindex-term ρ is (Beta pi ot ot') =
    Beta pi (reindex-optTerm ρ is ot) (reindex-optTerm ρ is ot')
  reindex-term ρ is (Chi pi oT t) =
    Chi pi (reindex-optType ρ is oT) (reindex-term ρ is t)
  reindex-term ρ is (Delta pi oT t) =
    Delta pi (reindex-optType ρ is oT) (reindex-term ρ is t)
  reindex-term ρ is (Epsilon pi lr m t) =
    Epsilon pi lr m (reindex-term ρ is t)
  reindex-term ρ is (Hole pi) =
    Hole pi
  reindex-term ρ is (IotaPair pi t t' g pi') =
    IotaPair pi (reindex-term ρ is t) (reindex-term ρ is t') (reindex-optGuide ρ is g) pi'
  reindex-term ρ is (IotaProj t n pi) =
    IotaProj (reindex-term ρ is t) n pi
  reindex-term ρ is (Lam pi me pi' x oc t) with is-index-var x
  ...| ff = let x' = reindex-fresh-var ρ is x in
    Lam pi me pi' x' (reindex-optClass ρ is oc) (reindex-term (renamectxt-insert ρ x x') is t)
  ...| tt with rename-indices ρ is | oc
  ...| isₙ | NoClass = indices-to-lams' isₙ $ reindex-term (rc-is ρ isₙ) (trie-insert is x isₙ) t
  ...| isₙ | SomeClass atk = indices-to-lams isₙ $ reindex-term (rc-is ρ isₙ) (trie-insert is x isₙ) t
  reindex-term ρ is (Let pi d t) =
    elim-pair (reindex-defTermOrType ρ is d) λ d' ρ' → Let pi d' (reindex-term ρ' is t)
  reindex-term ρ is (Open pi x t) =
    Open pi x (reindex-term ρ is t)
  reindex-term ρ is (Parens pi t pi') =
    reindex-term ρ is t
  reindex-term ρ is (Phi pi t₌ t₁ t₂ pi') =
    Phi pi (reindex-term ρ is t₌) (reindex-term ρ is t₁) (reindex-term ρ is t₂) pi'
  reindex-term ρ is (Rho pi op on t og t') =
    Rho pi op on (reindex-term ρ is t) (reindex-optGuide ρ is og) (reindex-term ρ is t')
  reindex-term ρ is (Sigma pi t) =
    Sigma pi (reindex-term ρ is t)
  reindex-term ρ is (Theta pi θ t ts) =
    Theta pi (reindex-theta ρ is θ) (reindex-term ρ is t) (reindex-lterms ρ is ts)
  reindex-term ρ is (Var pi x) =
    Var pi $ renamectxt-rep ρ x
  reindex-term ρ is (Mu pi x t oT pi' cs pi'') = Var posinfo-gen "template-mu-not-allowed"
  reindex-term ρ is (Mu' pi t oT pi' cs pi'') = Var posinfo-gen "template-mu-not-allowed"

  reindex-type ρ is (Abs pi me pi' x atk T) with is-index-var x
  ...| ff = let x' = reindex-fresh-var ρ is x in
    Abs pi me pi' x' (reindex-tk ρ is atk) (reindex-type (renamectxt-insert ρ x x') is T)
  ...| tt = let isₙ = rename-indices ρ is in
    indices-to-alls isₙ $ reindex-type (rc-is ρ isₙ) (trie-insert is x isₙ) T
  reindex-type ρ is (Iota pi pi' x T T') =
    let x' = reindex-fresh-var ρ is x in
    Iota pi pi' x' (reindex-type ρ is T) (reindex-type (renamectxt-insert ρ x x') is T')
  reindex-type ρ is (Lft pi pi' x t lT) =
    let x' = reindex-fresh-var ρ is x in
    Lft pi pi' x' (reindex-term (renamectxt-insert ρ x x') is t) (reindex-liftingType ρ is lT)
  reindex-type ρ is (NoSpans T pi) =
    NoSpans (reindex-type ρ is T) pi
  reindex-type ρ is (TpLet pi d T) =
    elim-pair (reindex-defTermOrType ρ is d) λ d' ρ' → TpLet pi d' (reindex-type ρ' is T)
  reindex-type ρ is (TpApp T T') =
    TpApp (reindex-type ρ is T) (reindex-type ρ is T')
  reindex-type ρ is (TpAppt T (Var pi x)) with trie-lookup is x
  ...| nothing = TpAppt (reindex-type ρ is T) (reindex-term ρ is (Var pi x))
  ...| just is' = indices-to-tpapps is' $ reindex-type ρ is T
  reindex-type ρ is (TpAppt T t) =
    TpAppt (reindex-type ρ is T) (reindex-term ρ is t)
  reindex-type ρ is (TpArrow (TpVar pi x) Erased T) with is-index-type-var x
  ...| ff = TpArrow (reindex-type ρ is (TpVar pi x)) Erased (reindex-type ρ is T)
  ...| tt = let isₙ = rename-indices ρ is in
    indices-to-alls isₙ $ reindex-type (rc-is ρ isₙ) (trie-insert is x isₙ) T
  reindex-type ρ is (TpArrow T me T') =
    TpArrow (reindex-type ρ is T) me (reindex-type ρ is T')
  reindex-type ρ is (TpEq pi t t' pi') =
    TpEq pi (reindex-term ρ is t) (reindex-term ρ is t') pi'
  reindex-type ρ is (TpHole pi) =
    TpHole pi
  reindex-type ρ is (TpLambda pi pi' x atk T) with is-index-var x
  ...| ff = let x' = reindex-fresh-var ρ is x in
    TpLambda pi pi' x' (reindex-tk ρ is atk) (reindex-type (renamectxt-insert ρ x x') is T)
  ...| tt = let isₙ = rename-indices ρ is in
    indices-to-tplams isₙ $ reindex-type (rc-is ρ isₙ) (trie-insert is x isₙ) T
  reindex-type ρ is (TpParens pi T pi') =
    reindex-type ρ is T
  reindex-type ρ is (TpVar pi x) =
    TpVar pi $ renamectxt-rep ρ x

  reindex-kind ρ is (KndParens pi k pi') =
    reindex-kind ρ is k
  reindex-kind ρ is (KndArrow k k') =
    KndArrow (reindex-kind ρ is k) (reindex-kind ρ is k')
  reindex-kind ρ is (KndPi pi pi' x atk k) with is-index-var x
  ...| ff = let x' = reindex-fresh-var ρ is x in
    KndPi pi pi' x' (reindex-tk ρ is atk) (reindex-kind (renamectxt-insert ρ x x') is k)
  ...| tt = let isₙ = rename-indices ρ is in
    indices-to-kind isₙ $ reindex-kind (rc-is ρ isₙ) (trie-insert is x isₙ) k
  reindex-kind ρ is (KndTpArrow (TpVar pi x) k) with is-index-type-var x
  ...| ff = KndTpArrow (reindex-type ρ is (TpVar pi x)) (reindex-kind ρ is k)
  ...| tt = let isₙ = rename-indices ρ is in
    indices-to-kind isₙ $ reindex-kind (rc-is ρ isₙ) is k
  reindex-kind ρ is (KndTpArrow T k) =
    KndTpArrow (reindex-type ρ is T) (reindex-kind ρ is k)
  reindex-kind ρ is (KndVar pi x as) =
    KndVar pi (renamectxt-rep ρ x) (reindex-args ρ is as)
  reindex-kind ρ is (Star pi) =
    Star pi

  reindex-tk ρ is (Tkt T) = Tkt $ reindex-type ρ is T
  reindex-tk ρ is (Tkk k) = Tkk $ reindex-kind ρ is k

  -- Can't reindex large indices in a lifting type (LiftPi requires a type, not a tk),
  -- so for now we will just ignore reindexing lifting types.
  -- Types withing lifting types will still be reindexed, though.
  reindex-liftingType ρ is (LiftArrow lT lT') =
    LiftArrow (reindex-liftingType ρ is lT) (reindex-liftingType ρ is lT')
  reindex-liftingType ρ is (LiftParens pi lT pi') =
    reindex-liftingType ρ is lT
  reindex-liftingType ρ is (LiftPi pi x T lT) =
    let x' = reindex-fresh-var ρ is x in
    LiftPi pi x' (reindex-type ρ is T) (reindex-liftingType (renamectxt-insert ρ x x') is lT)
  reindex-liftingType ρ is (LiftStar pi) =
    LiftStar pi
  reindex-liftingType ρ is (LiftTpArrow T lT) =
    LiftTpArrow (reindex-type ρ is T) (reindex-liftingType ρ is lT)

  reindex-optTerm ρ is NoTerm = NoTerm
  reindex-optTerm ρ is (SomeTerm t pi) = SomeTerm (reindex-term ρ is t) pi

  reindex-optType ρ is NoType = NoType
  reindex-optType ρ is (SomeType T) = SomeType (reindex-type ρ is T)

  reindex-optClass ρ is NoClass = NoClass
  reindex-optClass ρ is (SomeClass atk) = SomeClass (reindex-tk ρ is atk)

  reindex-optGuide ρ is NoGuide = NoGuide
  reindex-optGuide ρ is (Guide pi x T) =
    let x' = reindex-fresh-var ρ is x in
    Guide pi x' (reindex-type (renamectxt-insert ρ x x') is T)

  reindex-lterms ρ is (LtermsNil pi) = LtermsNil pi
  reindex-lterms ρ is (LtermsCons me t ts) =
    LtermsCons me (reindex-term ρ is t) (reindex-lterms ρ is ts)

  reindex-theta ρ is (AbstractVars xs) = maybe-else Abstract AbstractVars $ reindex-vars ρ is $ just xs
  reindex-theta ρ is θ = θ

  reindex-vars''' : vars → vars → vars
  reindex-vars''' (VarsNext x xs) xs' = VarsNext x $ reindex-vars''' xs xs'
  reindex-vars''' (VarsStart x) xs = VarsNext x xs
  reindex-vars'' : vars → maybe vars
  reindex-vars'' (VarsNext x (VarsStart x')) = just $ VarsStart x
  reindex-vars'' (VarsNext x xs) = maybe-map (VarsNext x) $ reindex-vars'' xs
  reindex-vars'' (VarsStart x) = nothing
  reindex-vars' : renamectxt → trie indices → var → maybe vars
  reindex-vars' ρ is x = maybe-else (just $ VarsStart $ renamectxt-rep ρ x)
    (reindex-vars'' ∘ flip foldr (VarsStart "") λ {(Index x atk) → VarsNext x}) (trie-lookup is x)
  reindex-vars ρ is (just (VarsStart x)) = reindex-vars' ρ is x
  reindex-vars ρ is (just (VarsNext x xs)) = maybe-else (reindex-vars ρ is $ just xs)
    (λ xs' → maybe-map (reindex-vars''' xs') $ reindex-vars ρ is $ just xs) $ reindex-vars' ρ is x
  reindex-vars ρ is nothing = nothing

  reindex-arg ρ is (TermArg me t) = TermArg me (reindex-term ρ is t)
  reindex-arg ρ is (TypeArg T) = TypeArg (reindex-type ρ is T)

  reindex-args ρ is ArgsNil = ArgsNil
  reindex-args ρ is (ArgsCons a as) = ArgsCons (reindex-arg ρ is a) (reindex-args ρ is as)

  reindex-defTermOrType ρ is (DefTerm pi x oT t) =
    let x' = reindex-fresh-var ρ is x in
    DefTerm pi x' (reindex-optType ρ is oT) (reindex-term ρ is t) , renamectxt-insert ρ x x'
  reindex-defTermOrType ρ is (DefType pi x k T) =
    let x' = reindex-fresh-var ρ is x in
    DefType pi x' (reindex-kind ρ is k) (reindex-type ρ is T) , renamectxt-insert ρ x x'

  reindex-cmds : renamectxt → trie indices → cmds → cmds × renamectxt
  reindex-cmds ρ is CmdsStart = CmdsStart , ρ
  reindex-cmds ρ is (CmdsNext (ImportCmd i) cs) =
    elim-pair (reindex-cmds ρ is cs) $ _,_ ∘ CmdsNext (ImportCmd i)
  reindex-cmds ρ is (CmdsNext (DefTermOrType op d pi) cs) =
    elim-pair (reindex-defTermOrType ρ is d) λ d' ρ' →
    elim-pair (reindex-cmds ρ' is cs) $ _,_ ∘ CmdsNext (DefTermOrType op d' pi)
  reindex-cmds ρ is (CmdsNext (DefKind pi x ps k pi') cs) =
    let x' = reindex-fresh-var ρ is x in
    elim-pair (reindex-cmds (renamectxt-insert ρ x x') is cs) $ _,_ ∘ CmdsNext
      (DefKind pi x' ps (reindex-kind ρ is k) pi')
  reindex-cmds ρ is (CmdsNext (DefDatatype dt pi) cs) =
    reindex-cmds ρ is cs -- Templates can't use datatypes!

reindex-file : ctxt → indices → start → cmds × renamectxt
reindex-file Γ is (File pi csᵢ pi' pi'' x ps cs pi''') =
  reindex-cmds empty-renamectxt empty-trie cs
  where open reindexing Γ is

mk-ctr-term : maybeErased → (x X : var) → constructors → parameters → term
mk-ctr-term me x X cs ps =
  let t = Mlam X $ constructors-to-lams' cs $ parameters-to-apps ps $ mvar x in
  case me of λ where
    Erased → Beta posinfo-gen NoTerm $ SomeTerm t posinfo-gen
    NotErased → IotaPair posinfo-gen (Beta posinfo-gen NoTerm $ SomeTerm t posinfo-gen)
                  t NoGuide posinfo-gen

mk-ctr-type : maybeErased → ctxt → ctr → constructors → var → type
mk-ctr-type me Γ (Ctr x T) cs Tₕ with decompose-ctr-type (ctxt-var-decl Tₕ Γ) T
...| Tₓ , ps , is =
  parameters-to-alls ps $
  TpAppt (curry recompose-tpapps (mtpvar Tₕ) is) $
  rename "X" from add-parameters-to-ctxt ps (ctxt-var-decl Tₕ Γ) for λ X →
  mk-ctr-term me x X cs ps

record encoded-datatype-names : Set where
  constructor mk-encoded-datatype-names
  field
    data-functor : var
    data-fmap : var
    data-functor-ind : var
    cast : var
    fixpoint-type : var
    fixpoint-in : var
    fixpoint-ind : var

record elab-mus : Set where
  field
    elab-check-mu : var → type → maybe term
    elab-synth-mu : var → maybe (term × type)
    elab-check-mu' : type → maybe term
    elab-synth-mu' : maybe (term × type)

record encoded-datatype : Set where
  constructor mk-encoded-datatype
  field
    data-def : datatype
    names : encoded-datatype-names
    elab-mu : datatype → encoded-datatype-names → ctxt → term → optType → cases → elab-mus
  elab-check-mu = λ Γ t oT ms → elab-mus.elab-check-mu $ elab-mu data-def names Γ t oT ms
  elab-synth-mu = λ Γ t oT ms → elab-mus.elab-synth-mu $ elab-mu data-def names Γ t oT ms
  elab-check-mu' = λ Γ t oT ms → elab-mus.elab-check-mu' $ elab-mu data-def names Γ t oT ms
  elab-synth-mu' = λ Γ t oT ms → elab-mus.elab-synth-mu' $ elab-mu data-def names Γ t oT ms

record datatype-encoding : Set where
  constructor mk-datatype-encoding
  field
    template : start
    functor : var
    cast : var
    fixpoint-type : var
    fixpoint-in : var
    fixpoint-ind : var
    elab-mu : datatype → encoded-datatype-names → ctxt → term → optType → cases → elab-mus

  mk-defs : ctxt → datatype → cmds × encoded-datatype
  mk-defs Γ'' (Data x ps is cs) =
    append-cmds tcs
    (csn functor-cmd $
     csn functor-ind-cmd $
     csn fmap-cmd $
     csn type-cmd $
     foldr (csn ∘ ctr-cmd) CmdsStart cs) ,
    record {
      elab-mu = elab-mu;
      data-def = Data x ps is cs;
      names = record {
        data-functor = data-functorₓ;
        data-fmap = data-fmapₓ;
        data-functor-ind = data-functor-indₓ;
        cast = castₓ;
        fixpoint-type = fixpoint-typeₓ;
        fixpoint-in = fixpoint-inₓ;
        fixpoint-ind = fixpoint-indₓ}}
    where
    csn = CmdsNext ∘ flip (DefTermOrType OpacTrans) posinfo-gen
    k = indices-to-kind is $ Star posinfo-gen

    Γ' = add-parameters-to-ctxt ps $ add-constructors-to-ctxt cs $ ctxt-var-decl x Γ''

    tcs-ρ = reindex-file Γ' is template
    tcs = fst tcs-ρ
    ρ = snd tcs-ρ

    data-functorₓ = fresh-var (x ^ "F") (ctxt-binds-var Γ') ρ
    data-fmapₓ = fresh-var (x ^ "Fmap") (ctxt-binds-var Γ') ρ
    data-functor-indₓ = fresh-var (x ^ "IndF") (ctxt-binds-var Γ') ρ
    functorₓ = renamectxt-rep ρ functor
    castₓ = renamectxt-rep ρ cast
    fixpoint-typeₓ = renamectxt-rep ρ fixpoint-type
    fixpoint-inₓ = renamectxt-rep ρ fixpoint-in
    fixpoint-indₓ = renamectxt-rep ρ fixpoint-ind
    Γ = add-indices-to-ctxt is $ ctxt-var-decl data-functorₓ $ ctxt-var-decl data-fmapₓ $ ctxt-var-decl data-functor-indₓ Γ'

    new-var : ∀ {ℓ} {X : Set ℓ} → var → (var → X) → X
    new-var x f = f $ fresh-var x (ctxt-binds-var Γ) ρ

    functor-cmd = DefType posinfo-gen data-functorₓ (parameters-to-kind ps $ KndArrow k k) $
      parameters-to-tplams ps $
      TpLambda posinfo-gen posinfo-gen x (Tkk $ k) $
      indices-to-tplams is $
      new-var "x" λ xₓ → new-var "X" λ Xₓ →
      Iota posinfo-gen posinfo-gen xₓ (mtpeq id-term id-term) $
      Abs posinfo-gen Erased posinfo-gen Xₓ
        (Tkk $ indices-to-kind is $ KndTpArrow (mtpeq id-term id-term) star) $
      foldr (λ c → flip TpArrow NotErased $ mk-ctr-type Erased Γ c cs Xₓ)
        (TpAppt (indices-to-tpapps is $ mtpvar Xₓ) (mvar xₓ)) cs

    functor-ind-cmd = DefTerm posinfo-gen data-functor-indₓ NoType $
      parameters-to-lams ps $
      Lam posinfo-gen Erased posinfo-gen x (SomeClass $ Tkk k) $
      indices-to-lams is $
      new-var "x" λ xₓ → new-var "y" λ yₓ → new-var "e" λ eₓ → new-var "X" λ Xₓ →
      let T = indices-to-tpapps is $ TpApp (parameters-to-tpapps ps $ mtpvar data-functorₓ) (mtpvar x) in
      Lam posinfo-gen NotErased posinfo-gen xₓ (SomeClass $ Tkt T) $
      Lam posinfo-gen Erased posinfo-gen Xₓ
        (SomeClass $ Tkk $ indices-to-kind is $ KndTpArrow T star) $
      flip (foldr λ {c @ (Ctr x' _) → Lam posinfo-gen NotErased posinfo-gen x' $ SomeClass $
                                        Tkt $ mk-ctr-type NotErased Γ c cs Xₓ}) cs $
      flip mappe (Beta posinfo-gen NoTerm NoTerm) $
      flip mappe (mvar xₓ) $
      let Γ' = ctxt-var-decl xₓ $ ctxt-var-decl yₓ $ ctxt-var-decl eₓ $ ctxt-var-decl Xₓ Γ in
      flip (foldl λ {(Ctr x' T) → flip mapp $
                                  elim-pair (decompose-arrows Γ T) λ ps' Tₕ →
                                  parameters-to-lams' ps' $
                                  Mlam yₓ $ Mlam eₓ $
                                  parameters-to-apps ps' $ mvar x'}) cs $
      AppTp (IotaProj (mvar xₓ) "2" posinfo-gen) $
      indices-to-tplams is $
      TpLambda posinfo-gen posinfo-gen xₓ (Tkt $ mtpeq id-term id-term) $
      Abs posinfo-gen Erased posinfo-gen yₓ (Tkt T) $
      Abs posinfo-gen Erased posinfo-gen eₓ (Tkt $ mtpeq (mvar yₓ) (mvar xₓ)) $
      TpAppt (indices-to-tpapps is $ mtpvar Xₓ) $
      Phi posinfo-gen (mvar eₓ) (mvar yₓ) (mvar xₓ) posinfo-gen

    fmap-cmd : defTermOrType
    fmap-cmd with new-var "A" id | new-var "B" id | new-var "c" id
    ...| Aₓ | Bₓ | cₓ = DefTerm posinfo-gen data-fmapₓ (SomeType $
        parameters-to-alls ps $
        TpApp (mtpvar functorₓ) $
        parameters-to-tpapps ps $
        mtpvar data-functorₓ) $
      parameters-to-lams ps $
      Mlam Aₓ $ Mlam Bₓ $ Mlam cₓ $
      IotaPair posinfo-gen
        (indices-to-lams is $
         new-var "x" λ xₓ → mlam xₓ $
         IotaPair posinfo-gen (IotaProj (mvar xₓ) "1" posinfo-gen)
           (new-var "X" λ Xₓ → Mlam Xₓ $
             constructors-to-lams' cs $
             foldl
               (flip mapp ∘ eta-expand-fmap)
               (AppTp (IotaProj (mvar xₓ) "2" posinfo-gen) $ mtpvar Xₓ) cs)
          NoGuide posinfo-gen)
        (Beta posinfo-gen NoTerm NoTerm) NoGuide posinfo-gen
      where
      eta-expand-fmaph-type : ctxt → var → type → term
      eta-expand-fmaph-type Γ x' T with decompose-ctr-type Γ T
      ...| Tₕ , ps , as with add-parameters-to-ctxt ps Γ
      ...| Γ' =
        parameters-to-lams' ps $
        flip mapp (parameters-to-apps ps $ mvar x') $
        recompose-apps Erased as $
        flip mappe (mvar cₓ) $
        flip AppTp (mtpvar Bₓ) $
        AppTp (mvar castₓ) (mtpvar Aₓ)

      eta-expand-fmap : ctr → term
      eta-expand-fmap (Ctr x' T) with
        ctxt-var-decl Aₓ $ ctxt-var-decl Bₓ $ ctxt-var-decl cₓ Γ
      ...| Γ' with decompose-ctr-type Γ' T
      ...| Tₕ , ps , as with foldr (λ {(Decl _ _ _ x'' _ _) → ctxt-var-decl x''}) Γ' ps
      ...| Γ'' = parameters-to-lams' ps $ foldl
        (λ {(Decl pi pi' me x'' (Tkt T) pi'') t → App t me $
              if ~ is-free-in tt x T then mvar x'' else eta-expand-fmaph-type Γ'' x'' T;
            (Decl pi pi' me x'' (Tkk k) pi'') t → AppTp t $ mtpvar x''})
        (mvar x') $ ps

    type-cmd = DefType posinfo-gen x (parameters-to-kind ps $ k) $
      parameters-to-tplams ps $ TpAppt
        (TpApp (mtpvar fixpoint-typeₓ) $ parameters-to-tpapps ps $ mtpvar data-functorₓ)
        (parameters-to-apps ps $ mvar data-fmapₓ)

    ctr-cmd : ctr → defTermOrType
    ctr-cmd (Ctr x' T) with
        decompose-ctr-type Γ (subst Γ (parameters-to-tpapps ps $ mtpvar x) x T)
    ...| Tₕ , ps' , as' = DefTerm posinfo-gen x' NoType $
      parameters-to-lams ps $
      parameters-to-lams ps' $
      mapp (recompose-apps Erased (take (length as' ∸ length ps) as') $
            mappe (AppTp (mvar fixpoint-inₓ) $
              parameters-to-tpapps ps $ mtpvar data-functorₓ) $
        parameters-to-apps ps $ mvar data-fmapₓ) $
      rename "X" from add-parameters-to-ctxt ps' Γ for λ Xₓ →
      mk-ctr-term NotErased x' Xₓ cs ps'

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
open import Function     using (const; id)
open import Auto.Core    using (IsHintDB; simpleHintDB; Rules; Rule; name2rule)
open import Data.List    using ([]; [_]; _++_)
open import Data.Nat     using (ℕ)
open import Data.Product using (_,_)
open import Data.Sum     using (inj₁; inj₂)
open import Reflection   using (Name; Term; TC)

module Auto where

open import Auto.Extensible simpleHintDB public renaming (auto to auto′)

auto : ℕ → HintDB → Term → TC Term
auto = auto′ dfs

macro
  autoMacro = auto

max_stars_repo_name: wenkokke/AutoInAgda

max_issues_repo_name: wenkokke/AutoInAgda

max_forks_repo_name: wenkokke/AutoInAgda


text:
{-# OPTIONS --allow-unsolved-metas #-}
module Term where

open import OscarPrelude
open import VariableName
open import FunctionName
open import Arity
open import Vector

mutual

  data Term : Set
   where
    variable : VariableName → Term
    function : FunctionName → Terms → Term

  record Terms : Set
   where
    constructor ⟨_⟩
    inductive
    field
      {arity} : Arity
      terms : Vector Term arity

open Terms public

termVariable-inj : ∀ {𝑥₁ 𝑥₂} → Term.variable 𝑥₁ ≡ variable 𝑥₂ → 𝑥₁ ≡ 𝑥₂
termVariable-inj refl = refl

termFunction-inj₁ : ∀ {𝑓₁ 𝑓₂ τ₁s τ₂s} → Term.function 𝑓₁ τ₁s ≡ function 𝑓₂ τ₂s → 𝑓₁ ≡ 𝑓₂
termFunction-inj₁ refl = refl

termFunction-inj₂ : ∀ {𝑓₁ 𝑓₂ τ₁s τ₂s} → Term.function 𝑓₁ τ₁s ≡ function 𝑓₂ τ₂s → τ₁s ≡ τ₂s
termFunction-inj₂ refl = refl

terms-inj : ∀ {𝑎} → {τs₁ τs₂ : Vector Term 𝑎} → (τs₁≡τs₂ : (Terms.⟨_⟩ {𝑎} τs₁) ≡ ⟨ τs₂ ⟩) → τs₁ ≡ τs₂
terms-inj refl = refl

module _ where

  open import TermByFunctionNames

  mutual
    termToTermByFunctionNames : Term → Σ Nat TermByFunctionNames
    termToTermByFunctionNames (variable x) = _ , (variable x)
    termToTermByFunctionNames (function x x₁) = {!!}

    termsToVec : Terms → Σ Nat (λ arity → Σ (Vec (Σ Nat TermByFunctionNames) arity) λ τs → Σ Nat λ n → n ≡ sum (vecToList $ (fst <$> τs)))
    termsToVec (⟨_⟩ {arity = arity₁} ⟨ vector₁ ⟩) = {!!}

  iTermToTerm : Σ Nat TermByFunctionNames → Term
  iTermToTerm = {!!}

eq-term-round : ∀ τ → iTermToTerm (termToTermByFunctionNames τ) ≡ τ
eq-term-round = {!!}

eq-iterm-round : ∀ τ → termToTermByFunctionNames (iTermToTerm τ) ≡ τ
eq-iterm-round = {!!}

instance EqTerm : Eq Term
Eq._==_ EqTerm x y with termToTermByFunctionNames x | graphAt termToTermByFunctionNames x | termToTermByFunctionNames y | graphAt termToTermByFunctionNames y
Eq._==_ EqTerm x y | ix | ingraph eqx | iy | ingraph eqy with ix ≟ iy
Eq._==_ EqTerm x y | ix | ingraph eqx | .ix | ingraph eqy | yes refl = yes $ ((cong iTermToTerm eqy ⟨≡⟩ʳ cong iTermToTerm eqx) ⟨≡⟩ eq-term-round x) ʳ⟨≡⟩ eq-term-round y
Eq._==_ EqTerm x y | ix | ingraph eqx | iy | ingraph eqy | no neq = {!!}

instance EqTerms : Eq Terms
EqTerms = {!!}

{-
module _ {i : Size}
 where

  mutual

    EqTerm⇑ : (x y : Term) → Delay i ∘ Dec $ x ≡ y
    EqTerm⇑ (variable _) (variable _) = now (decEq₁ termVariable-inj $ _≟_ _ _)
    EqTerm⇑ (function 𝑓₁ τ₁s) (function 𝑓₂ τ₂s) =
      {-
      τ₁s≟τ₂s ← EqTerms⇑ τ₁s τ₂s -|
      (now $ decEq₂ termFunction-inj₁ termFunction-inj₂ (𝑓₁ ≟ 𝑓₂) τ₁s≟τ₂s)
      -}

      EqTerms⇑ τ₁s τ₂s >>= λ
      τ₁s≟τ₂s → now $ decEq₂ termFunction-inj₁ termFunction-inj₂ (𝑓₁ ≟ 𝑓₂) τ₁s≟τ₂s

    EqTerm⇑ (variable _)   (function _ _) = now $ no λ ()
    EqTerm⇑ (function _ _) (variable _)   = now $ no λ ()

    EqTerms⇑ : (x y : Terms) → Delay i ∘ Dec $ x ≡ y
    EqTerms⇑ (⟨_⟩ {𝑎₁} τ₁s) (⟨_⟩ {𝑎₂} τ₂s)
     with 𝑎₁ ≟ 𝑎₂
    … | no 𝑎₁≢𝑎₂ = now $ no λ {τ₁≡τ₂ → 𝑎₁≢𝑎₂ (cong arity τ₁≡τ₂)}
    … | yes refl =
      EqVectorTerm⇑ τ₁s τ₂s >>= λ
      { (yes refl) → now $ yes refl
      ; (no τ₁s≢τ₂s) → now $ no (λ ⟨τ₁s⟩≡⟨τ₂s⟩ → τ₁s≢τ₂s (terms-inj ⟨τ₁s⟩≡⟨τ₂s⟩)) }

    EqVectorTerm⇑ : ∀ {n} → (x y : Vector Term n) → Delay i ∘ Dec $ x ≡ y
    EqVectorTerm⇑ ⟨ [] ⟩ ⟨ [] ⟩ = now (yes refl)
    EqVectorTerm⇑ ⟨ τ₁ ∷ τ₁s ⟩ ⟨ τ₂ ∷ τ₂s ⟩ =
      EqTerm⇑ τ₁ τ₂ >>= λ
      { (yes refl) → EqVectorTerm⇑ ⟨ τ₁s ⟩ ⟨ τ₂s ⟩ >>= λ
                     { (yes refl) → now $ yes refl
                     ; (no τ₁s≢τ₂s) → now $ no λ τ₁₁s≡τ₁₂s → τ₁s≢τ₂s $ cong ⟨_⟩ ((vcons-inj-tail (cong vector τ₁₁s≡τ₁₂s))) }
      ; (no τ₁≢τ₂) → now $ no λ τ₁₁s≡τ₂₂s → τ₁≢τ₂ $ vcons-inj-head (cong vector τ₁₁s≡τ₂₂s) }

EqVectorTerm⇓ : ∀ {n} → (x y : Vector Term n) → EqVectorTerm⇑ x y ⇓
EqVectorTerm⇓ ⟨ [] ⟩ ⟨ [] ⟩ = _ , now⇓
EqVectorTerm⇓ ⟨ variable 𝑥₁ ∷ τ₁s ⟩ ⟨ variable 𝑥₂ ∷ τ₂s ⟩
 with 𝑥₁ ≟ 𝑥₂
… | yes refl with EqVectorTerm⇓ ⟨ τ₁s ⟩ ⟨ τ₂s ⟩
EqVectorTerm⇓ ⟨ variable 𝑥₁ ∷ τ₁s ⟩ ⟨ variable .𝑥₁ ∷ .τ₁s ⟩ | yes refl | (yes refl , snd₁) = _ , snd₁ >>=⇓ now⇓
EqVectorTerm⇓ ⟨ variable 𝑥₁ ∷ τ₁s ⟩ ⟨ variable .𝑥₁ ∷ τ₂s ⟩ | yes refl | (no x , snd₁) = _ , snd₁ >>=⇓ now⇓
EqVectorTerm⇓ ⟨ variable 𝑥₁ ∷ τ₁s ⟩ ⟨ variable 𝑥₂ ∷ τ₂s ⟩ | no 𝑥₁≢𝑥₂ = _ , now⇓
EqVectorTerm⇓ ⟨ variable x ∷ τ₁s ⟩ ⟨ function x₁ x₂ ∷ τ₂s ⟩ = _ , now⇓
EqVectorTerm⇓ ⟨ function x x₁ ∷ τ₁s ⟩ ⟨ variable x₂ ∷ τ₂s ⟩ = _ , now⇓
EqVectorTerm⇓ ⟨ function 𝑓₁ (⟨_⟩ {𝑎₁} τ₁s) ∷ τ₁₂s ⟩ ⟨ function 𝑓₂ (⟨_⟩ {𝑎₂} τ₂s) ∷ τ₂₂s ⟩
 with 𝑎₁ ≟ 𝑎₂ | 𝑓₁ ≟ 𝑓₂
… | no 𝑎₁≢𝑎₂ | no 𝑓₁≢𝑓₂  = _ , now⇓
… | no 𝑎₁≢𝑎₂ | yes refl  = _ , now⇓
… | yes refl | no 𝑓₁≢𝑓₂
 with EqVectorTerm⇓ τ₁s τ₂s
… | (no τ₁s≢τ₂s , τ⇓)  = _ , τ⇓ >>=⇓ now⇓ >>=⇓ now⇓ >>=⇓ now⇓
… | (yes refl , τ⇓)    = _ , τ⇓ >>=⇓ now⇓ >>=⇓ now⇓ >>=⇓ now⇓
EqVectorTerm⇓ ⟨ function 𝑓₁ (⟨_⟩ {𝑎₁} τ₁s) ∷ τ₁₂s ⟩ ⟨ function 𝑓₂ (⟨_⟩ {𝑎₂} τ₂s) ∷ τ₂₂s ⟩ | yes refl | yes refl
 with EqVectorTerm⇓ τ₁s τ₂s | EqVectorTerm⇓ ⟨ τ₁₂s ⟩ ⟨ τ₂₂s ⟩
… | (no τ₁s≢τ₂s , τ⇓) | (no τ₁₂s≢τ₂₂s , τs⇓) = _ , τ⇓ >>=⇓ now⇓ >>=⇓ now⇓ >>=⇓ now⇓
… | (yes refl , τ⇓)   | (no τ₁₂s≢τ₂₂s , τs⇓) = _ , τ⇓ >>=⇓ now⇓ >>=⇓ now⇓ >>=⇓ (τs⇓ >>=⇓ now⇓)
… | (no τ₁s≢τ₂s , τ⇓) | (yes refl , τs⇓) = _ , τ⇓ >>=⇓ now⇓ >>=⇓ now⇓ >>=⇓ now⇓
… | (yes refl , τ⇓)   | (yes refl , τs⇓) = _ , τ⇓ >>=⇓ now⇓ >>=⇓ now⇓ >>=⇓ (τs⇓ >>=⇓ now⇓)

EqTerms⇓ : (x y : Terms) → EqTerms⇑ x y ⇓
EqTerms⇓ (⟨_⟩ {𝑎₁} τ₁s) (⟨_⟩ {𝑎₂} τ₂s)
 with 𝑎₁ ≟ 𝑎₂
… | no 𝑎₁≢𝑎₂ = _ , now⇓
… | yes refl
 with EqVectorTerm⇓ τ₁s τ₂s
… | (yes refl , τ⇓) = _ , τ⇓ >>=⇓ now⇓
… | (no _ , τ⇓) = _ , τ⇓ >>=⇓ now⇓

EqTerm⇓ : (x y : Term) → EqTerm⇑ x y ⇓
EqTerm⇓ (variable x) (variable x₁) = _ , now⇓
EqTerm⇓ (function _ τ₁s) (function _ τ₂s)
 with EqTerms⇓ τ₁s τ₂s
… | (_ , τ⇓) = _ , τ⇓ >>=⇓ now⇓
EqTerm⇓ (variable x) (function x₁ x₂) = _ , now⇓
EqTerm⇓ (function x x₁) (variable x₂) = _ , now⇓

instance EqTerm : Eq Term
EqTerm = record { _==_ = λ x y → fst (EqTerm⇓ x y) }

instance EqTerms : Eq Terms
Eq._==_ EqTerms x y = fst (EqTerms⇓ x y)
-}

module _ where

  open import Membership

  instance MembershipTermTerms : Membership Term Terms
  Membership._∈_ MembershipTermTerms = _ᵗ∈ᵗˢ_ where
    data _ᵗ∈ᵗˢ_ (τ : Term) : Terms → Set
     where
      zero : τ ᵗ∈ᵗˢ ⟨ ⟨ τ ∷ [] ⟩ ⟩
      suc : ∀ {τs} → τ ᵗ∈ᵗˢ τs → τ ᵗ∈ᵗˢ ⟨ ⟨ τ ∷ vector (terms τs) ⟩ ⟩
  Membership._∉_ MembershipTermTerms x X = ¬ x ∈ X
  fst (Membership.xor-membership MembershipTermTerms) x₁ x₂ = x₂ x₁
  snd (Membership.xor-membership MembershipTermTerms) x₁ x₂ = x₁ x₂

  instance MembershipVariableNameTerm : Membership VariableName Term
  Membership._∈_ MembershipVariableNameTerm = _ᵛ∈ᵗ_ where
    data _ᵛ∈ᵗ_ (𝑥 : VariableName) : Term → Set
     where
      variable : 𝑥 ᵛ∈ᵗ variable 𝑥
      function : ∀ 𝑓 {τ : Term} {τs} → {_ : 𝑥 ∈ τ} → τ ∈ τs → 𝑥 ᵛ∈ᵗ function 𝑓 τs
  Membership._∉_ MembershipVariableNameTerm x X = ¬ x ∈ X
  fst (Membership.xor-membership MembershipVariableNameTerm) x₁ x₂ = x₂ x₁
  snd (Membership.xor-membership MembershipVariableNameTerm) x₁ x₂ = x₁ x₂

module _ where
  import UnifyTermL
  import UnifyMguCorrectL

  module L where
    open UnifyTermL (Maybe FunctionName) public
    open UnifyMguCorrectL (Maybe FunctionName) public

  mutual

    TermLtoTerm : ∃ L.Term → Term
    TermLtoTerm (fst₁ , UnifyTermL.i x) = {!!}
    TermLtoTerm (fst₁ , UnifyTermL.leaf nothing) = {!!}
    TermLtoTerm (fst₁ , UnifyTermL.leaf (just x)) = {!!}
    TermLtoTerm (fst₁ , (snd₁ UnifyTermL.fork snd₂)) = {!!}

    TermtoTermL : Term → ∃ L.Term
    TermtoTermL (variable x) = {!!} , (L.i {!!})
    TermtoTermL (function x ⟨ ⟨ [] ⟩ ⟩) = {!!} , L.leaf (just x) L.fork L.leaf nothing
    TermtoTermL (function x ⟨ ⟨ x₁ ∷ vector₁ ⟩ ⟩) = {!!} , {!!} L.fork {!!}


text:
module PLRTree.Equality.Properties {A : Set} where

open import PLRTree {A}
open import PLRTree.Equality {A}
open import Relation.Binary.Core

sym≃ : Symmetric _≃_
sym≃ ≃lf = ≃lf
sym≃ (≃nd x x' l≃r l'≃r' l≃l') = ≃nd x' x l'≃r' l≃r (sym≃ l≃l')

trans≃ : Transitive _≃_
trans≃ ≃lf t≃t'' = t≃t''
trans≃ (≃nd x x' l≃r l'≃r' l≃l') (≃nd .x' x'' _ l''≃r'' l'≃r'') = ≃nd x x'' l≃r l''≃r'' (trans≃ l≃l' l'≃r'')

lemma-≃-≃ : {t t' : PLRTree} → t ≃ t' → t ≃ t
lemma-≃-≃ ≃lf = ≃lf
lemma-≃-≃ (≃nd x x' l≃r l≃r' l≃l') = ≃nd x x l≃r l≃r (lemma-≃-≃ l≃l')

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Generic.Test.Data.Fin where

open import Generic.Main

import Data.Fin as Fin

Fin : ℕ -> Set
Fin = readData Fin.Fin

pattern fzero {n}   = #₀  (relv n , lrefl)
pattern fsuc  {n} i = !#₁ (relv n , i , lrefl)

elimFin : ∀ {n π}
        -> (P : ∀ {n} -> Fin n -> Set π)
        -> (∀ {n} {i : Fin n} -> P i -> P (fsuc i))
        -> (∀ {n} -> P {suc n} fzero)
        -> (i : Fin n)
        -> P i
elimFin P f x  fzero   = x
elimFin P f x (fsuc i) = f (elimFin P f x i)

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
module Data.Nat.Literal where

open import Data.Nat using (ℕ; suc; zero)
open import Data.Fin using (Fin; suc; zero)
open import Data.Unit using (⊤)
open import Data.Empty using (⊥)
open import Agda.Builtin.FromNat using (Number; fromNat) public

_≤_ : ℕ → ℕ → Set
zero  ≤ n     = ⊤
suc m ≤ zero  = ⊥
suc m ≤ suc n = m ≤ n

instance
  ℕ-num : Number ℕ
  ℕ-num .Number.Constraint _ = ⊤
  ℕ-num .Number.fromNat n = n

instance
  Fin-num : {n : ℕ} → Number (Fin (suc n))
  Fin-num {n} .Number.Constraint m = m ≤ n
  Fin-num {n} .Number.fromNat m ⦃ p ⦄ = from m n p where
    from : (m n : ℕ) → m ≤ n → Fin (suc n)
    from zero _ _ = zero
    from (suc _) zero ()
    from (suc m) (suc n) p = suc (from m n p)

max_stars_repo_name: brunoczim/Celeste

max_issues_repo_name: brunoczim/Celeste

max_forks_repo_name: brunoczim/Celeste


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

module higher where

open import higher.circle public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
open import Prelude hiding (All; module All; _>>=_; ⊥; sym)

module Implicits.Resolution.Infinite.Algorithm.Completeness where

open import Data.Bool
open import Data.Unit.Base
open import Data.Maybe as Maybe using (Is-just; to-witness)
open import Coinduction
open import Data.Fin.Substitution
open import Data.List.Any hiding (tail)
open Membership-≡
open import Data.Fin.Substitution
open import Relation.Binary.HeterogeneousEquality as H using ()
open import Induction.WellFounded

open import Implicits.Syntax
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas.MetaType
open import Implicits.Syntax.Type.Unification
open import Implicits.Syntax.Type.Unification.Lemmas as Unification hiding (complete)
open import Implicits.Resolution.Infinite.Resolution
open import Implicits.Resolution.Infinite.Algorithm
open import Implicits.Resolution.Termination

private
  module HR = H.≅-Reasoning

open import Category.Monad.Partiality as P
open Workaround
open Workaround.Correct
open import Category.Monad.Partiality.All using (All; module Alternative)
open Alternative renaming (sound to AllP-sound) hiding (complete)

open import Category.Functor
private module MaybeFunctor {f} = RawFunctor (Maybe.functor {f})

private
  module M = MetaTypeMetaSubst

module Lemmas where

private
  open import Relation.Binary.PropositionalEquality as PEq using (_≡_)
  open module PartialEq = P.Equality  {A = Bool} _≡_
  open Lemmas

mutual
  {-# NO_TERMINATION_CHECK #-}
  delayed-resolve-complete : ∀ {ν} (Δ : ICtx ν) r → Δ ⊢ᵣ r → AllP (_≡_ true) (delayed-resolve Δ r)
  delayed-resolve-complete Δ r p = later (♯ (complete' Δ r p))

  resolve-context-complete : ∀ {ν m} (Δ : ICtx ν) a (u : Maybe (Sub (flip MetaType ν) m zero)) →
                            (p : Is-just u) →
                            Δ ⊢ᵣ (from-meta (a M./ (to-witness p))) →
                            AllP Is-just (resolve-context Δ a u)
  resolve-context-complete Δ a ._ (just {x = u} px) x =
    _ ≅⟨ resolve-context-comp Δ a u ⟩P
    delayed-resolve-complete Δ (from-meta (M._/_ a u)) x >>=-congP lem
    where
      lem : ∀ {b} → true ≡ b → AllP Is-just (map-bool u b)
      lem refl = now (just tt)

  lemx : ∀ {ν m} {Δ : ICtx ν} r c τ (u : M.MetaSub MetaType ν m zero) →
        Δ ⊢ from-meta (r M./ u M.↑tp) tp[/tp c ] ↓ τ →
        Δ ⊢ from-meta (open-meta r M./ (to-meta c ∷ u)) ↓ τ
  lemx r c τ u p = {!!}

  a/u-↓-unique : ∀ {ν m} {Δ} (a : MetaType m ν) {τ} u v →
                 Δ ⊢ from-meta (a M./ u) ↓ τ → Δ ⊢ from-meta (a M./ v) ↓ τ →
                 (a M./ u) ≡ (a M./ v)
  a/u-↓-unique (a ⇒ b) u v (i-iabs _ p) (i-iabs _ q) = {!a/u-↓-unique b u v p q!}
  a/u-↓-unique (∀' a) u v p q = {!!}
  a/u-↓-unique (simpl x) u v p q = {!!}

  match-u-complete' : ∀ {ν m} (Δ : ICtx ν) → (τ : SimpleType ν) → (r : MetaType m ν) → (ac : m<-Acc r) →
                    ∀ u → Δ ⊢ from-meta (r M./ u) ↓ τ →
                    AllP Is-just (match-u Δ τ r ac)
  match-u-complete' Δ τ (a ⇒ b) (acc f) u (i-iabs q p) =
    _
      ≅⟨ match-u-iabs-comp Δ τ a b f ⟩P
    match-u-complete' Δ τ b (f _ (b-m<-a⇒b a b)) u p >>=-congP lem
    where
      lem : ∀ {v : Maybe (Sub (flip MetaType _) _ zero)} → Is-just v →
            AllP Is-just (resolve-context Δ a v)
      lem x = resolve-context-complete Δ a _ x q'
        where
          -- from q : Δ ⊢ᵣ a / u
          -- we derive q' : Δ ⊢ᵣ a / x
          -- based on the idea that we have Δ ⊢ b / u ↓ τ and
          -- soundness gives us Δ ⊢ b / (to-witness x) ↓ τ.
          -- And assuming ⊢unamb b, we should have u ≡ (to-witness x)
          q' : Δ ⊢ᵣ from-meta (a M./ to-witness x )
          q' = subst (_⊢ᵣ_ Δ) {!!} q
  match-u-complete' {m = m} Δ τ (∀' r) (acc f) u (i-tabs c p) =
    _
      ≅⟨ match-u-tabs-comp Δ τ r f ⟩P
    (match-u-complete' Δ τ (open-meta r) (f _ _) (to-meta {zero} c ∷ u) (lemx r c τ u p))
      >>=-congP now∘tail-compl
    where
      now∘tail-compl : ∀ {ν} {v : Maybe (Sub (flip MetaType ν) (suc m) zero)} →
                      Is-just v →
                      AllP Is-just ((now ∘ (MaybeFunctor._<$>_ tail)) v)
      now∘tail-compl (just px) = now (just tt)

  -- Maybe surprisingly 'u' is ignored in the proofs below.
  -- But if you think about it, it makes sense: mgu doesn't necessarily find the same unifier.
  -- All we need to know is that there is a unifier u; the structure of Δ ⊢ (a / u) ↓ τ does the rest
  match-u-complete' Δ .(tvar x) (simpl (tvar x)) ac u (i-simp .(tvar x)) =
    now (Unification.complete (simpl (tvar x)) (tvar x) u refl)
  match-u-complete' Δ .(tc x) (simpl (tc x)) ac u (i-simp .(tc x)) =
    now (Unification.complete (simpl (tc x)) (tc x) u refl)
  match-u-complete' Δ τ (simpl (mvar x)) ac u p =
    let (u' , u'-uni) = mvar-unifiable x τ in
      now (Unification.complete (simpl (mvar x)) τ u' u'-uni)
  match-u-complete' Δ ._ (simpl (a →' b)) ac u (i-simp ._) =
    now (Unification.complete (simpl (a →' b)) _ u refl)

  -- the trivial predicate holds for all terminating problems
  trivial-allP : ∀ {a} {A : Set a} (a : A ⊥) → AllP (const ⊤) a
  trivial-allP (now x) = now tt
  trivial-allP (later x) = later (♯ (trivial-allP (♭ x)))

  -- Match succeeds if we have a proof Δ ⊢ r ↓ τ
  match-complete : ∀ {ν} (Δ : ICtx ν) → (τ : SimpleType ν) → (r : Type ν) → Δ ⊢ r ↓ τ →
                  AllP (_≡_ true) (match Δ τ r)
  match-complete Δ τ r p = _
      ≅⟨ match-comp Δ τ r ⟩P
    match-u-complete' Δ τ (to-meta {zero} r) (m<-well-founded _) []
      (subst (λ z → Δ ⊢ z ↓ τ) (Prelude.sym $ from-to-meta-/-vanishes) p)
      >>=-congP lem
    where
      lem : ∀ {ν} {v : Maybe (Sub (flip MetaType ν) zero zero)} →
            (Is-just v) → AllP (_≡_ true) (⟦ (now ∘ Maybe.is-just) v ⟧P)
      lem  (just tt) = now refl

  -- 'recovery' of a non failed match succeeds
  recover-true-complete : ∀ {ν} {Δ : ICtx ν} {ρs τ v} → v ≡ true →
                          AllP (_≡_ true) (match1st-recover Δ ρs τ v)
  recover-true-complete refl = now refl

  -- recovery of a failed match succeeds if we know that the recursive match1st succeeds
  recover-false-complete : ∀ {ν} (Δ : ICtx ν) ρs τ v → AllP (_≡_ true) (match1st Δ ρs τ) →
                          AllP (_≡_ true) (match1st-recover Δ ρs τ v)
  recover-false-complete Δ ρs τ true p = now refl
  recover-false-complete Δ ρs τ false p = p

  -- match1st succeeds if we have a proof that some r from the context
  -- should be a match
  match1st-complete : ∀ {ν} (Δ : ICtx ν) {r} →
                      (ρs : ICtx ν) → (τ : SimpleType ν) →
                      r List.∈ ρs → Δ ⊢ r ↓ τ →
                      AllP (_≡_ true) (match1st Δ ρs τ)
  match1st-complete Δ List.[] τ () r↓τ
  match1st-complete Δ (x List.∷ ρs) τ (here refl) r↓τ =
    _
      ≅⟨ match1st-comp Δ x ρs τ ⟩P
    match-complete Δ τ x r↓τ >>=-congP (λ{ v → recover-true-complete (Prelude.sym v)})
  match1st-complete Δ (x List.∷ ρs) τ (there r∈Δ) r↓τ =
    _
      ≅⟨ match1st-comp Δ x ρs τ ⟩P
    ((trivial-allP (match Δ τ x)) >>=-congP
      (λ {v} _ → recover-false-complete Δ ρs τ v (match1st-complete Δ ρs τ r∈Δ r↓τ)))

  -- Mirroring Abel & Altenkirch's work on partial type checking, we say:
  -- Because resolution without an additional termination condition
  -- seems to be undecidable, an appropriate completeness result would be:
  -- if Δ resolves r, then the resolution algorithm searching for a proof of that fact,
  -- will not fail finetely. I.e. the algorithm might diverge or succeed, but not report an error.
  -- We can make this formal using the *coinductive* resolution rules
  -- (Together with soundness we have a 'minimal' completeness result, because the rules allow
  -- for many derivations, while the algorithm will only find *one*.)
  complete' : ∀ {ν} (Δ : ICtx ν) r → Δ ⊢ᵣ r → AllP (_≡_ true) (resolve Δ r)
  complete' Δ (simpl x) (r-simp r∈Δ r↓τ) = (match1st-complete Δ Δ x r∈Δ r↓τ)
  complete' Δ (a ⇒ b) (r-iabs p) = complete' (a List.∷ Δ) b p
  complete' Δ (∀' r) (r-tabs p) = complete' (ictx-weaken Δ) r p

  complete : ∀ {ν} (Δ : ICtx ν) r → Δ ⊢ᵣ r → All (_≡_ true) (resolve Δ r)
  complete Δ r p = AllP-sound (complete' Δ r p)

module Test where

  open import Category.Monad.Partiality.All

  trivial-all : ∀ {a p} {A : Set a} (P : A → Set p) → All P never
  trivial-all p = later (♯ (trivial-all p))


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Support.Equivalence where

open import Level
open import Relation.Binary using (Rel; IsEquivalence; module IsEquivalence; IsPreorder; Preorder; Reflexive; Transitive; Symmetric; _⇒_) renaming (Setoid to RSetoid; module Setoid to RSetoid)
open import Data.Product using (_×_; _,_)
open import Relation.Binary.Product.Pointwise using (×-isEquivalence)
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)

------------------------------------------------------------------------
-- Setoids

-- Equivalence relations are defined in Relation.Binary.Core.

record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier       : Set c
    _≈_           : Rel Carrier ℓ
    .isEquivalence : IsEquivalence _≈_

  .refl : Reflexive _≈_
  refl = IsEquivalence.refl isEquivalence
  .trans : Transitive _≈_
  trans = IsEquivalence.trans isEquivalence
  .sym : Symmetric _≈_
  sym = IsEquivalence.sym isEquivalence
  .reflexive : _≡_ ⇒ _≈_
  reflexive = IsEquivalence.reflexive isEquivalence

  .isPreorder : IsPreorder _≡_ _≈_
  isPreorder = record
    { isEquivalence = PropEq.isEquivalence
    ; reflexive     = reflexive
    ; trans         = trans
    }

  .preorder : Preorder c c ℓ
  preorder = record { isPreorder = isPreorder }

  -- A trivially indexed setoid.

  {-
  indexedSetoid : ∀ {i} {I : Set i} → I.Setoid I c _
  indexedSetoid = record
    { Carrier = λ _ → Carrier
    ; _≈_     = _≈_
    ; isEquivalence = record
      { refl  = refl
      ; sym   = sym
      ; trans = trans
      }
    }
  -}

setoid-r→i : ∀ {c ℓ} → RSetoid c ℓ → Setoid c ℓ
setoid-r→i Base = record
  { Carrier = Base.Carrier
  ; _≈_ = Base._≈_
  ; isEquivalence = Base.isEquivalence
  }
  where module Base = RSetoid Base

record I→R-Wrapper {c ℓ} {Carrier : Set c} (Base : Rel Carrier ℓ) (x y : Carrier) : Set ℓ where
  constructor squash
  field
    .anonymous-witness : Base x y

setoid-i→r : ∀ {c ℓ} → Setoid c ℓ → RSetoid c ℓ
setoid-i→r Base = record
  { Carrier = Base.Carrier
  ; _≈_ = I→R-Wrapper Base._≈_
  ; isEquivalence = record
    { refl = squash Base.refl
    ; sym = λ pf → squash (Base.sym (anonymous-witness pf))
    ; trans = λ i≈j j≈k → squash (Base.trans (anonymous-witness i≈j) (anonymous-witness j≈k))
    }
  }
  where
  module Base = Setoid Base
  open I→R-Wrapper

set→setoid : ∀ {ℓ} → Set ℓ → Setoid ℓ ℓ
set→setoid Base = record
  { Carrier = Base
  ; _≈_ = _≡_
  ; isEquivalence = PropEq.isEquivalence
  }

_×-setoid_ : ∀ {s₁ s₂ s₃ s₄} → Setoid s₁ s₂ → Setoid s₃ s₄ → Setoid _ _
S₁ ×-setoid S₂ = record
  { isEquivalence = ×-isEquivalence (isEquivalence S₁)  (isEquivalence S₂)
  } where open Setoid

Lift-setoid : ∀ {c ℓ a b} -> Setoid c ℓ -> Setoid (c ⊔ a) (ℓ ⊔ b)
Lift-setoid {c} {ℓ} {a} {b} s = record {
    Carrier = Lift {c} a Carrier;
    _≈_ = λ x₁ x₂ → Lift {ℓ} b (lower x₁ ≈ lower x₂);
    isEquivalence = record {
        refl = lift refl;
        sym = λ x₁ → lift (sym (lower x₁));
        trans = λ x₁ x₂ → lift (trans (lower x₁) (lower x₂))}}
 where
   open Setoid s

∀[_]-setoid_ : ∀ {ℓ s₁ s₂} → (A : Set ℓ) → (A → Setoid s₁ s₂) → Setoid _ _
∀[ A ]-setoid B = record
   { Carrier = ∀ a → B.Carrier a
   ; _≈_ = λ f g → ∀ a → B._≈_ a (f a) (g a)
   ; isEquivalence = record
       { refl = λ a → B.refl a
       ; sym = λ f≈g a → B.sym a (f≈g a)
       ; trans = λ f≈g g≈h a → B.trans a (f≈g a) (g≈h a)
       }
   }
  where
    module B a = Setoid (B a)

Fam-setoid : ∀ {ℓ s₁ s₂} → (A : Set ℓ) → (B : Setoid s₁ s₂) → (A → Setoid.Carrier B) → Setoid _ _
Fam-setoid A B p = record
  { Carrier = A
  ; _≈_ = λ a₁ a₂ → p a₁ ≈ p a₂
  ; isEquivalence = record
    { refl = refl
    ; sym = sym
    ; trans = trans
    }
  }
 where
   open Setoid B

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Andreas, 2015-06-24

open import Common.Equality
open import Common.Product

Sing : {A : Set} (a : A) → Set
Sing a = ∃ λ b → a ≡ b

works : {A : Set} (f : ∀{a : A} → Sing a) (a : A) → Sing a
works f a = let b , p = f {_} in b , p

test : {A : Set} (f : ∀{a : A} → Sing a) (a : A) → Sing a
test f a = let b , p = f in b , p

-- ERROR WAS:
-- Type mismatch
-- when checking that the pattern b , p has type
-- {a = a₁ : .A} → Sing a₁

-- should work now

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Pair type which calls out to Haskell via the FFI
------------------------------------------------------------------------

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

module Foreign.Haskell.Pair where

open import Level
open import Data.Product using (_×_; _,_)

private
  variable
    a b : Level
    A : Set a
    B : Set b

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

record Pair (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field  fst : A
         snd : B
open Pair public

{-# FOREIGN GHC type AgdaPair l1 l2 a b = (a , b) #-}
{-# COMPILE GHC Pair = data MAlonzo.Code.Foreign.Haskell.Pair.AgdaPair ((,)) #-}

------------------------------------------------------------------------
-- Conversion

toForeign : A × B → Pair A B
toForeign (a , b) = (a , b)

fromForeign : Pair A B → A × B
fromForeign (a , b) = (a , b)


text:
{-# OPTIONS --cubical-compatible #-}
module Common.String where

open import Agda.Builtin.String public
open import Common.Bool
open import Common.Char
open import Common.List
open import Common.Nat
open import Common.Integer

strEq : (x y : String) -> Bool
strEq = primStringEquality

infixr 30 _+S+_

_+S+_ : (x y : String) -> String
_+S+_ = primStringAppend

fromList : List Char -> String
fromList = primStringFromList

stringToList : String -> List Char
stringToList = primStringToList

charToStr : Char → String
charToStr c = primStringFromList (c ∷ [])

intToString : Integer → String
intToString = primShowInteger

natToString : Nat -> String
natToString n = intToString (pos n)


text:
------------------------------------------------------------------------
-- Generic support for reduction relations.
------------------------------------------------------------------------

module Relation.Binary.Reduction where

open import Data.Fin using (Fin)
open import Data.Fin.Substitution
open import Data.Star as Star using (Star; ε; _◅_)
import Data.Star.Properties as StarProp
open import Data.Nat using (ℕ; _+_)
open import Function using (_∘_)
open import Relation.Binary
open import Relation.Binary.EquivalenceClosure
open import Relation.Binary.SymmetricClosure using (fwd)
import Relation.Binary.PropositionalEquality as PropEq
import Relation.Binary.EqReasoning as EqReasoning

----------------------------------------------------------------------
-- Generic reduction and equivalence relations

record Reduction (T : ℕ → Set) : Set₁ where

  infix  5  _→1_ _→*_ _↔_

  -- One-step reduction.
  field _→1_ : ∀ {n} → T n → T n → Set

  -- The reflexive transitive closure of _→1_, i.e. finite sequences
  -- of reduction steps.
  _→*_ : ∀ {n} → T n → T n → Set
  _→*_ = Star _→1_

  -- The reflexive, transitive and symmetric closure (aka the
  -- equivalence closure) of _→1_.
  _↔_ : ∀ {n} → T n → T n → Set
  _↔_ = EqClosure _→1_

-- All remaining submodules are parametrized by a given reduction.
module _ {T} (reduction : Reduction T) where
  open Reduction reduction

  ----------------------------------------------------------------------
  -- Properties of the reductions/equivalence

  -- Inclusions.

  →1⇒→* : ∀ {n} {a b : T n} → a →1 b → a →* b
  →1⇒→* a→b = a→b ◅ ε

  →*⇒↔ : ∀ {n} {a b : T n} → a →* b → a ↔ b
  →*⇒↔ a→*b = Star.map fwd a→*b

  →1⇒↔ : ∀ {n} {a b : T n} → a →1 b → a ↔ b
  →1⇒↔ = →*⇒↔ ∘ →1⇒→*

  -- Reductions are preorders.
  →*-predorder : ∀ {n : ℕ} → Preorder _ _ _
  →*-predorder {n} = StarProp.preorder (_→1_ {n})

  -- Preorder reasoning for reductions.
  module →*-Reasoning {n} = StarProp.StarReasoning (_→1_ {n})

  -- Terms together with equivalence form a setoid.
  ↔-setoid : ∀ {n : ℕ} → Setoid _ _
  ↔-setoid {n} = setoid (_→1_ {n})

  -- Equational reasoning for ↔-equivalence.
  module ↔-Reasoning {n : ℕ} where
    open EqReasoning (↔-setoid {n}) public
    open Setoid (↔-setoid {n}) using (sym)

    infixr 2 _→⟨_⟩_ _←⟨_⟩_ _→*⟨_⟩_ _←*⟨_⟩_

    _→⟨_⟩_ : ∀ a {b c} → a →1 b → b IsRelatedTo c → a IsRelatedTo c
    a →⟨ a→b ⟩ b≡c = a ≈⟨ →1⇒↔ a→b ⟩ b≡c

    _←⟨_⟩_ : ∀ a {b c} → b →1 a → b IsRelatedTo c → a IsRelatedTo c
    a ←⟨ a←b ⟩ b≡c = a ≈⟨ sym (→1⇒↔ a←b) ⟩ b≡c

    _→*⟨_⟩_ : ∀ a {b c} → a →* b → b IsRelatedTo c → a IsRelatedTo c
    a →*⟨ a→*b ⟩ b≡c = a ≈⟨ →*⇒↔ a→*b ⟩ b≡c

    _←*⟨_⟩_ : ∀ a {b c} → b →* a → b IsRelatedTo c → a IsRelatedTo c
    a ←*⟨ a←*b ⟩ b≡c = a ≈⟨ sym (→*⇒↔ a←*b) ⟩ b≡c

  ----------------------------------------------------------------------
  -- Substitutions in reductions/equivalence
  --
  -- The applications _/→1_, _/→*_ and _/↔_ below may be considered
  -- substitution lemmas, i.e. they establish the commutativity of the
  -- respective reductions/equivalence with substitutions.

  record RedSubstApp {T′} (app : Application T T′) : Set where
    open Application app
    open PropEq

    infixl 8 _/→1_ _/→*_ _/↔_

    field
      -- Substitution commutes with one-step reduction.
      _/→1_ : ∀ {m n a b} → a →1 b → (σ : Sub T′ m n) → a / σ →1 b / σ

    -- Substitution commutes with β-reduction.
    _/→*_ : ∀ {m n a b} → a →* b → (σ : Sub T′ m n) → a / σ →* b / σ
    a→*b /→* σ = Star.gmap (λ a → a / σ) (λ a→b → a→b /→1 σ) a→*b

    -- Substitution commutes with β-equivalence.
    _/↔_ : ∀ {m n a b} → a ↔ b → (σ : Sub T′ m n) → a / σ ↔ b / σ
    a≡b /↔ σ = gmap (λ a → a / σ) (λ a→b → a→b /→1 σ) a≡b

max_stars_repo_name: asr/pts-agda

max_issues_repo_name: asr/pts-agda

max_forks_repo_name: asr/pts-agda


text:
module #12 where

{-
  Using the propositions as types interpretation, derive the following tautologies.
  (i) If A, then (if B then A).
  (ii) If A, then not (not A).
  (iii) If (not A or not B), then not (A and B).
-}

open import Data.Product
open import Data.Sum
open import Relation.Nullary

const : {A B : Set} → A → (B → A)
const = λ z _ → z

double-negation : {A : Set} → A → ¬ (¬ A)
double-negation = λ z z₁ → z₁ z

demorgans-law₁ : {A B C : Set} → ((¬ A) ⊎ (¬ B)) → (¬ (A × B))
demorgans-law₁ (inj₁ ¬x) (a , _) =  ¬x a
demorgans-law₁ (inj₂ ¬y) (_ , b) =  ¬y b

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Induction over Fin
------------------------------------------------------------------------

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

module Data.Fin.Induction where

open import Data.Nat.Base using (ℕ)
open import Data.Nat.Induction using (<′-wellFounded)
open import Data.Fin.Base using (_≺_)
open import Data.Fin.Properties
open import Induction
open import Induction.WellFounded as WF

------------------------------------------------------------------------
-- Re-export accessability

open WF public using (Acc; acc)

------------------------------------------------------------------------
-- Complete induction based on _≺_

≺-Rec : ∀ {ℓ} → RecStruct ℕ ℓ ℓ
≺-Rec = WfRec _≺_

≺-wellFounded : WellFounded _≺_
≺-wellFounded = Subrelation.wellFounded ≺⇒<′ <′-wellFounded

module _ {ℓ} where
  open WF.All ≺-wellFounded ℓ public
    renaming
    ( wfRecBuilder to ≺-recBuilder
    ; wfRec        to ≺-rec
    )
    hiding (wfRec-builder)

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

-- Version 0.15

≺-rec-builder    = ≺-recBuilder
{-# WARNING_ON_USAGE ≺-rec-builder
"Warning: ≺-rec-builder was deprecated in v0.15.
Please use ≺-recBuilder instead."
#-}
≺-well-founded   = ≺-wellFounded
{-# WARNING_ON_USAGE ≺-well-founded
"Warning: ≺-well-founded was deprecated in v0.15.
Please use ≺-wellFounded instead."
#-}


text:
{-#  OPTIONS --type-in-type #-}
module TooFewArgs where

open import AgdaPrelude

myFun : (a : Set) -> a -> a -> a
myFun a x y = x

myApp : Nat
myApp = myFun _ Zero

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint