text:
------------------------------------------------------------------------
-- A type-checker
------------------------------------------------------------------------

import Axiom.Extensionality.Propositional as E
import Level
open import Data.Universe

-- The code makes use of the assumption that propositional equality of
-- functions is extensional.

module README.DependentlyTyped.Type-checker
  (Uni₀ : Universe Level.zero Level.zero)
  (ext : E.Extensionality Level.zero Level.zero)
  where

open import Category.Monad
open import Data.Maybe hiding (_>>=_)
import Data.Maybe.Categorical as Maybe
open import Data.Nat using (ℕ; zero; suc; pred)
open import Data.Product as Prod
open import Function as F hiding (_∋_) renaming (_∘_ to _⊚_)
import README.DependentlyTyped.Equality-checker as EC; open EC Uni₀ ext
import README.DependentlyTyped.NBE as NBE; open NBE Uni₀ ext
import README.DependentlyTyped.NormalForm as NF
open NF Uni₀ hiding (⌊_⌋; no)
import README.DependentlyTyped.Raw-term as RT; open RT Uni₀
import README.DependentlyTyped.Term as Term; open Term Uni₀
import README.DependentlyTyped.Term.Substitution as S; open S Uni₀
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product

open P.≡-Reasoning
open RawMonadZero (Maybe.monadZero {f = Level.zero})

-- Computes a syntactic type for a variable from a matching syntactic
-- context.

type-of-var : ∀ {Γ σ} → Γ ∋ σ → Γ ctxt → Γ ⊢ σ type
type-of-var zero    (Γ′ ▻ σ′) = σ′               /⊢t wk
type-of-var (suc x) (Γ′ ▻ σ′) = type-of-var x Γ′ /⊢t wk

-- Infers the type of a variable, if possible.

infer-var : (Γ : Ctxt) (x : ℕ) →
            Dec (∃₂ λ σ (x′ : Γ ∋ σ) → position x′ ≡ x)
infer-var ε x = no helper
  where
  helper : ¬ ∃₂ λ σ (x′ : ε ∋ σ) → position x′ ≡ x
  helper (_ , () , _)
infer-var (Γ ▻ σ) zero    = yes (σ /̂ ŵk , zero , P.refl)
infer-var (Γ ▻ σ) (suc x) =
  Dec.map′ (Prod.map (λ σ → σ /̂ ŵk) (Prod.map suc (P.cong suc)))
           helper
           (infer-var Γ x)
  where
  helper : (∃₂ λ τ (x′ : Γ ▻ σ ∋ τ) → position x′ ≡ suc x) →
           (∃₂ λ τ (x′ : Γ     ∋ τ) → position x′ ≡ x)
  helper (._ , zero   , ())
  helper (._ , suc x′ , eq) = (_ , x′ , P.cong pred eq)

-- Infers the /syntactic/ type of a variable, if possible.

infer-var-syntactic :
  ∀ {Γ} → Γ ctxt → (x : ℕ) →
  Dec (∃ λ σ → Γ ⊢ σ type × ∃ λ (x′ : Γ ∋ σ) → position x′ ≡ x)
infer-var-syntactic {Γ} Γ′ x = Dec.map′
  (Prod.map F.id (λ p → type-of-var (proj₁ p) Γ′ , proj₁ p , proj₂ p))
  (Prod.map F.id proj₂)
  (infer-var Γ x)

mutual

  -- Tries to infer a well-typed form of a raw type.

  infer-ty :
    ∀ {Γ} → Γ ctxt → (σ : Raw-ty) →
    Maybe (∃₂ λ σ′ (σ″ : Γ ⊢ σ′ type) → ⌊ σ″ ⌋ty ≡ ⌊ σ ⌋raw-ty)
  infer-ty Γ′ ⋆      = return (_ , ⋆ , P.refl)
  infer-ty Γ′ (el t) =
    check Γ′ ⋆ t                      >>= λ { (t′ , eq) →
    return (_ , el t′ , P.cong el eq) }
  infer-ty Γ′ (π σ′₁ σ′₂) =
    infer-ty Γ′          σ′₁                     >>= λ { (_ , σ′₁′ , eq₁) →
    infer-ty (Γ′ ▻ σ′₁′) σ′₂                     >>= λ { (_ , σ′₂′ , eq₂) →
    return (_ , π σ′₁′ σ′₂′ , P.cong₂ π eq₁ eq₂) }}

  -- Tries to infer a type for a term. In the case of success a
  -- well-typed term is returned.

  infer :
    ∀ {Γ} → Γ ctxt → (t : Raw) →
    Maybe (∃ λ σ → Γ ⊢ σ type × ∃ λ (t′ : Γ ⊢ σ) → ⌊ t′ ⌋ ≡ ⌊ t ⌋raw)
  infer Γ′ (var x) with infer-var-syntactic Γ′ x
  ... | yes (_ , σ′ , x′ , eq) = return (_ , σ′ , var x′ , P.cong var eq)
  ... | no _                   = ∅
  infer Γ′ (ƛ t)     = ∅
  infer Γ′ (t₁ · t₂) =
    infer Γ′ t₁ >>=
    λ { (._ , π σ′₁ σ′₂ , t₁′ , eq₁) →
            check Γ′ σ′₁ t₂                           >>= λ { (t₂′ , eq₂) →
            return (_ , σ′₂ /⊢t sub t₂′ , t₁′ · t₂′ ,
                    P.cong₂ _·_ eq₁ eq₂) }
      ; _ → ∅
      }
  infer Γ′ (t ∶ σ) =
    infer-ty Γ′ σ             >>= λ { (_ , σ′ , eq) →
    check Γ′ σ′ t             >>= λ { (t′ , eq) →
    return (_ , σ′ , t′ , eq) }}

  -- Tries to type-check a term. In the case of success a well-typed
  -- term is returned.

  check : ∀ {Γ σ} → Γ ctxt → (σ′ : Γ ⊢ σ type) (t : Raw) →
          Maybe (∃ λ (t′ : Γ ⊢ σ) → ⌊ t′ ⌋ ≡ ⌊ t ⌋raw)
  check Γ′ (π σ′₁ σ′₂) (ƛ t) =
    check (Γ′ ▻ σ′₁) σ′₂ t      >>= λ { (t′ , eq) →
    return (ƛ t′ , P.cong ƛ eq) }
  check Γ′ σ′ t =
    infer Γ′ t                                           >>= λ { (_ , τ′ , t′ , eq₁) →
    τ′ ≟-Type σ′                                         >>= λ eq₂ →
    return (P.subst (_⊢_ _) (≅-Type-⇒-≡ eq₂) t′ , (begin
              ⌊ P.subst (_⊢_ _) (≅-Type-⇒-≡ eq₂) t′ ⌋  ≡⟨ ⌊⌋-cong $ drop-subst-⊢ F.id (≅-Type-⇒-≡ eq₂) ⟩
              ⌊ t′ ⌋                                   ≡⟨ eq₁ ⟩
              ⌊ t ⌋raw                                 ∎)) }

-- Tries to establish that the given raw term has the given raw type
-- (in the empty context).

infix 4 _∋?_

_∋?_ : (σ : Raw-ty) (t : Raw) →
       Maybe (∃₂ λ (σ′ : Type ε) (σ″ : ε ⊢ σ′ type) →
              ∃  λ (t′ : ε ⊢ σ′) →
                   ⌊ σ″ ⌋ty ≡ ⌊ σ ⌋raw-ty × ⌊ t′ ⌋ ≡ ⌊ t ⌋raw)
σ ∋? t = infer-ty ε σ                      >>= λ { (σ′ , σ″ , eq₁) →
         check ε σ″ t                      >>= λ { (t′ , eq₂) →
         return (σ′ , σ″ , t′ , eq₁ , eq₂) }}

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

private

  σ₁ : Raw-ty
  σ₁ = π ⋆ ⋆

  σ₁′ : Type ε
  σ₁′ = proj₁ $ from-just $ infer-ty ε σ₁

  t₁ : Raw
  t₁ = ƛ (var zero)

  t₁′ : ε ⊢ σ₁′
  t₁′ = proj₁ $ proj₂ $ proj₂ $ from-just $ σ₁ ∋? t₁

  t₂ : ε ▻ (⋆ , _) ⊢ (⋆ , _)
  t₂ = proj₁ $ proj₂ $ proj₂ $ from-just $ infer (ε ▻ ⋆) (var zero)

  t₃ : Raw
  t₃ = (ƛ (var zero) ∶ π ⋆ ⋆) · var zero

  t₃′ : ε ▻ (⋆ , _) ⊢ (⋆ , _)
  t₃′ = proj₁ $ proj₂ $ proj₂ $ from-just $ infer (ε ▻ ⋆) t₃

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


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

module Relation.Binary.Construct.Closure.SymmetricTransitive where

open import Level
open import Function
open import Relation.Binary

private
  variable
    a ℓ ℓ′ : Level
    A B    : Set a

module _ {A : Set a} (_≤_ : Rel A ℓ) where
  private
    variable
      x y z : A

  data Plus⇔ : Rel A (a ⊔ ℓ) where
    forth  : x ≤ y → Plus⇔ x y
    back   : y ≤ x → Plus⇔ x y
    forth⁺ : x ≤ y → Plus⇔ y z → Plus⇔ x z
    back⁺  : y ≤ x → Plus⇔ y z → Plus⇔ x z

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

  trans : Transitive (Plus⇔ _∼_)
  trans (forth r) rel′      = forth⁺ r rel′
  trans (back r) rel′       = back⁺ r rel′
  trans (forth⁺ r rel) rel′ = forth⁺ r (trans rel rel′)
  trans (back⁺ r rel) rel′  = back⁺ r (trans rel rel′)

  sym : Symmetric (Plus⇔ _∼_)
  sym (forth r)      = back r
  sym (back r)       = forth r
  sym (forth⁺ r rel) = trans (sym rel) (back r)
  sym (back⁺ r rel)  = trans (sym rel) (forth r)

  isPartialEquivalence : IsPartialEquivalence (Plus⇔ _∼_)
  isPartialEquivalence = record
    { sym   = sym
    ; trans = trans
    }

  partialSetoid : PartialSetoid _ _
  partialSetoid = record
    { Carrier              = A
    ; _≈_                  = Plus⇔ _∼_
    ; isPartialEquivalence = isPartialEquivalence
    }

  module _ (refl : Reflexive _∼_) where

    isEquivalence : IsEquivalence (Plus⇔ _∼_)
    isEquivalence = record
      { refl  = forth refl
      ; sym   = sym
      ; trans = trans
      }

    setoid : Setoid _ _
    setoid = record
      { Carrier       = A
      ; _≈_           = Plus⇔ _∼_
      ; isEquivalence = isEquivalence
      }

  module _ {c e} (S : Setoid c e) where
    private
      module S = Setoid S

    minimal : (f : A → Setoid.Carrier S) →
              _∼_ =[ f ]⇒ Setoid._≈_ S →
              Plus⇔ _∼_ =[ f ]⇒ Setoid._≈_ S
    minimal f inj (forth r)      = inj r
    minimal f inj (back r)       = S.sym (inj r)
    minimal f inj (forth⁺ r rel) = S.trans (inj r) (minimal f inj rel)
    minimal f inj (back⁺ r rel)  = S.trans (S.sym (inj r)) (minimal f inj rel)

module Plus⇔Reasoning (_≤_ : Rel A ℓ) where
  infix  3 forth-syntax back-syntax
  infixr 2 forth⁺-syntax back⁺-syntax

  forth-syntax : ∀ x y → x ≤ y → Plus⇔ _≤_ x y
  forth-syntax _ _ = forth

  syntax forth-syntax x y x≤y = x ⇒⟨ x≤y ⟩∎ y ∎

  back-syntax : ∀ x y → y ≤ x → Plus⇔ _≤_ x y
  back-syntax _ _ = back

  syntax back-syntax x y y≤x = x ⇐⟨ y≤x ⟩∎ y ∎

  forth⁺-syntax : ∀ x {y z} → x ≤ y → Plus⇔ _≤_ y z → Plus⇔ _≤_ x z
  forth⁺-syntax _ = forth⁺

  syntax forth⁺-syntax x x≤y y⇔z = x ⇒⟨ x≤y ⟩ y⇔z

  back⁺-syntax : ∀ x {y z} → y ≤ x → Plus⇔ _≤_ y z → Plus⇔ _≤_ x z
  back⁺-syntax _ = back⁺

  syntax back⁺-syntax x y≤x y⇔z = x ⇐⟨ y≤x ⟩ y⇔z

module _ {_≤_ : Rel A ℓ} {_≼_ : Rel B ℓ′} (f : A → B) where

  module _ (inj : _≤_ =[ f ]⇒ _≼_) where

    gmap : Plus⇔ _≤_ =[ f ]⇒ Plus⇔ _≼_
    gmap (forth r)      = forth (inj r)
    gmap (back r)       = back (inj r)
    gmap (forth⁺ r rel) = forth⁺ (inj r) (gmap rel)
    gmap (back⁺ r rel)  = back⁺ (inj r) (gmap rel)

map : {_≤_ : Rel A ℓ} {_≼_ : Rel A ℓ′} (inj : _≤_ ⇒ _≼_) → Plus⇔ _≤_ ⇒ Plus⇔ _≼_
map = gmap id

ext: agda

max_stars_repo_name: turion/agda-categories

max_issues_repo_name: turion/agda-categories

max_forks_repo_name: turion/agda-categories


text:
module L.Data.Bool where

-- Reexport definitions
open import L.Data.Bool.Core public
open import L.Data.Bool.Properties public

-- Functions on Bools
infix  7 not_
infixr 6 _∧_
infixr 5 _∨_ _xor_

not_ : Bool → Bool
not x = if (λ _ → Bool) ff tt x

_∧_ : Bool → Bool → Bool
x ∧ y = if (λ _ → Bool) y ff x

_∨_ : Bool → Bool → Bool
x ∨ y = if (λ _ → Bool) tt y x

_xor_ : Bool → Bool → Bool
x xor y = if (λ _ → Bool) y (not y) x

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
------------------------------------------------------------------------------
-- FOTC version of a nested recursive function by the
-- Bove-Capretta method
------------------------------------------------------------------------------

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

-- From: Ana Bove and Venanzio Capretta. Nested general recursion and
-- partiality in type theory. Vol. 2152 of LNCS. 2001.

module FOT.FOTC.Program.Nest.Nest-FOTC-BC where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base

open import FOTC.Data.Nat

import FOTC.Data.Nat.Induction.Acc.WF-I
open FOTC.Data.Nat.Induction.Acc.WF-I.<-WF

open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesI

------------------------------------------------------------------------------
-- The nest function.
postulate
  nest   : D → D
  nest-0 : nest zero            ≡ zero
  nest-S : ∀ d → nest (succ₁ d) ≡ nest (nest d)

data Dom : D → Set where
  dom0 :                              Dom zero
  domS : ∀ d → Dom d → Dom (nest d) → Dom (succ₁ d)

-- Inductive principle associated to the domain predicate.
Dom-ind : (P : D → Set) →
          P zero →
          (∀ {d} → Dom d → P d → Dom (nest d) → P (nest d) → P (succ₁ d)) →
          ∀ {d} → Dom d → P d
Dom-ind P P0 ih dom0           = P0
Dom-ind P P0 ih (domS d h₁ h₂) =
  ih h₁ (Dom-ind P P0 ih h₁) h₂ (Dom-ind P P0 ih h₂)

-- The domain predicate is total.
dom-N : ∀ d → Dom d → N d
dom-N .zero      dom0           = nzero
dom-N .(succ₁ d) (domS d h₁ h₂) = nsucc (dom-N d h₁)

nestCong : ∀ {n₁ n₂} → n₁ ≡ n₂ → nest n₁ ≡ nest n₂
nestCong refl = refl

nest-x≡0 : ∀ {n} → N n → nest n ≡ zero
nest-x≡0 nzero = nest-0
nest-x≡0 (nsucc {n} Nn) =
  nest (succ₁ n) ≡⟨ nest-S n ⟩
  nest (nest n)  ≡⟨ nestCong (nest-x≡0 Nn) ⟩
  nest zero      ≡⟨ nest-0 ⟩
  zero           ∎

-- The nest function is total in its domain (via structural recursion
-- in the domain predicate).
nest-DN : ∀ {d} → Dom d → N (nest d)
nest-DN dom0           = subst N (sym nest-0) nzero
nest-DN (domS d h₁ h₂) = subst N (sym (nest-S d)) (nest-DN h₂)

-- The nest function is total.
nest-N : ∀ {n} → N n → N (nest n)
nest-N Nn = subst N (sym (nest-x≡0 Nn)) nzero

nest-≤ : ∀ {n} → Dom n → nest n ≤ n
nest-≤ dom0 = le (nest zero) zero ≡⟨ leLeftCong nest-0 ⟩
              le zero zero        ≡⟨ x≤x nzero ⟩
              true                ∎

nest-≤ (domS n h₁ h₂) =
  ≤-trans (nest-N (nsucc (dom-N n h₁))) (nest-N (dom-N n h₁)) (nsucc Nn) prf₁ prf₂
    where
    Nn : N n
    Nn = dom-N n h₁

    prf₁ : nest (succ₁ n) ≤ nest n
    prf₁ = le (nest (succ₁ n)) (nest n) ≡⟨ leLeftCong (nest-S n) ⟩
           le (nest (nest n)) (nest n)  ≡⟨ nest-≤ h₂ ⟩
           true                         ∎

    prf₂ : nest n ≤ succ₁ n
    prf₂ = ≤-trans (nest-N (dom-N n h₁)) Nn (nsucc Nn) (nest-≤ h₁) (x≤Sx Nn)

N→Dom : ∀ {n} → N n → Dom n
N→Dom = <-wfind P ih
  where
  P : D → Set
  P = Dom

  ih : ∀ {x} → N x → (∀ {y} → N y → y < x → P y) → P x
  ih nzero          h = dom0
  ih (nsucc {x} Nx) h =
    domS x dn-x (h (nest-N Nx) (x≤y→x<Sy (nest-N Nx) Nx (nest-≤ dn-x)))
      where
      dn-x : Dom x
      dn-x = h Nx (x<Sx Nx)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Instantiates the natural coefficients ring solver, using coefficient
-- equality induced by ℕ.
--
-- This is sufficient for proving equalities that are independent of the
-- characteristic.  In particular, this is enough for equalities in rings of
-- characteristic 0.
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Solver.Ring.NaturalCoefficients.Default
         {r₁ r₂} (R : CommutativeSemiring r₁ r₂) where

import Algebra.Operations.Semiring as SemiringOps
open import Data.Maybe.Base using (Maybe; map)
open import Data.Nat using (_≟_)
open import Relation.Binary.Consequences using (dec⟶weaklyDec)
import Relation.Binary.PropositionalEquality as P

open CommutativeSemiring R
open SemiringOps semiring

private
  dec : ∀ m n → Maybe (m × 1# ≈ n × 1#)
  dec m n = map (λ { P.refl → refl }) (dec⟶weaklyDec _≟_ m n)

open import Algebra.Solver.Ring.NaturalCoefficients R dec public


text:
-- Andreas, 2016-10-30, issue #2286 reported by carlostome

-- {-# OPTIONS -v interaction.give:40 #-}
-- {-# OPTIONS -v tc.term.expr:40 #-}
-- {-# OPTIONS -v tc.meta:40 #-}
-- {-# OPTIONS -v 10 #-}

data Nat : Set where
  zero : Nat
  succ : Nat → Nat

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

f : Nat -> Nat
f x = {! f x !}  -- giving  f x  here used to loop, as termination checking was not redone

p1 : (n : Nat) -> f n == n
p1 n = refl  -- This unsolved constraint triggered the loop.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2018-06-14, issue #2513, parsing attributes

-- Run-time only use.

postulate
  @0      RT₁ : Set
  @erased RT₂ : Set

-- Default: unrestricted use.

postulate
  @ω      CT₁ : Set
  @plenty CT₂ : Set

-- Irrelevance.

postulate
  .           I₀ : Set
  @irr        I₁ : Set
  @irrelevant I₂ : Set

-- Shape-irrelevance

postulate
  -- .. SI₀ : Set -- Does not parse (yet).
  @shirr            SI₁ : Set
  @shape-irrelevant SI₂ : Set

-- Relevance (default).

postulate
  R₀ : Set
  @relevant R₁ : Set

-- Mix.

postulate
  @0 @shape-irrelevant M : Set

-- In function spaces and telescopes.

@ω id : ∀{@0 A : Set} → @relevant @ω A → A
id x = x

data Wrap (@0 A : Set) : Set where
  wrap' : @relevant A → Wrap A

wrap : ∀ (@0 A) → A → Wrap A
wrap A x = wrap' x

-- In record fields.

record Squash (@0 A : Set) : Set where
  no-eta-equality; constructor squash; field
    @irrelevant squashed : A

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda