text:
module rewriting where

open import cedille-types
open import constants
open import conversion
open import ctxt
open import general-util
open import free-vars
--open import lift
open import rename
open import subst
open import syntax-util
open import type-util
--open import erase
open import datatype-util

rewrite-mk-phi : var → (eq t t' : term) → term
rewrite-mk-phi x eq t t' =
  Phi (Rho (VarSigma eq) x (TpEq t t') (Beta t id-term)) t t'

rewrite-t : Set → Set
rewrite-t T = ctxt → (is-plus : 𝔹) → (nums : maybe stringset) → (eq : maybe term) →
              (left : term) → (right : var) → (total-matches : ℕ) →
              T {- Returned value -} ×
              ℕ {- Number of rewrites actually performed -} ×
              ℕ {- Total number of matches, including skipped ones -}

instance
  rewrite-functor : functor rewrite-t
  rewrite-applicative : applicative rewrite-t
  rewrite-monad : monad rewrite-t

  fmap ⦃ rewrite-functor ⦄ g r Γ op on eq t₁ t₂ n with r Γ op on eq t₁ t₂ n
  ...| a , n' , sn = g a , n' , sn

  pure ⦃ rewrite-applicative ⦄ a Γ p on eq t₁ t₂ n = a , 0 , n
  _<*>_ ⦃ rewrite-applicative ⦄ f a Γ op on eq t₁ t₂ n with f Γ op on eq t₁ t₂ n
  ...| f' , n' , sn with a Γ op on eq t₁ t₂ sn
  ...| b , n'' , sn' = f' b , n' + n'' , sn'

  return ⦃ rewrite-monad ⦄ a = pure a
  _>>=_ ⦃ rewrite-monad ⦄ fa fab Γ op on eq t₁ t₂ n with fa Γ op on eq t₁ t₂ n
  ...| a' , n' , sn with fab a' Γ op on eq t₁ t₂ sn
  ...| b , n'' , sn' = b , n' + n'' , sn'

infixl 4 _≫rewrite_
_≫rewrite_ = _<*>_

{-# TERMINATING #-}
rewrite-term  : term → rewrite-t term
rewrite-terma : term → rewrite-t term
rewrite-termh : term → rewrite-t term
rewrite-type  : type → rewrite-t type
rewrite-typeh : type → rewrite-t type
rewrite-kind  : kind → rewrite-t kind
rewrite-tpkd  : tpkd → rewrite-t tpkd
rewrite-tmtp  : tmtp → rewrite-t tmtp
rewrite-exprd : ∀ {ed} → ⟦ ed ⟧ → rewrite-t ⟦ ed ⟧
rewrite-case  : maybe (var × var) → case → rewrite-t case

rewrite-exprd {TERM} = rewrite-term
rewrite-exprd {TYPE} = rewrite-type
rewrite-exprd {KIND} = rewrite-kind

rewrite-rename-var : ∀ {A} → var → (var → rewrite-t A) → rewrite-t A
rewrite-rename-var x r Γ op on eq t₁ t₂ n =
  let x' = rename-var-if Γ (renamectxt-insert empty-renamectxt t₂ t₂) x t₁ in
  r x' Γ op on eq t₁ t₂ n

rewrite-abs : ∀ {ed} → var → var → (⟦ ed ⟧ → rewrite-t ⟦ ed ⟧) → ⟦ ed ⟧ → rewrite-t ⟦ ed ⟧
rewrite-abs x x' g a Γ = let Γ = ctxt-var-decl x' Γ in g (rename-var Γ x x' a) Γ

rewrite-term t Γ op on eq t₁ t₂ sn =
  case rewrite-terma (erase t) Γ op on eq t₁ t₂ sn of λ where
    (t' , 0 , sn') → t , 0 , sn'
    (t' , n , sn') → maybe-else' eq t' (λ eq → rewrite-mk-phi t₂ eq t t') , n , sn'

rewrite-terma t Γ op on eq t₁ t₂ sn =
  case conv-term Γ t t₁ of λ where
  tt → case on of λ where
    (just ns) → case trie-contains ns (ℕ-to-string (suc sn)) of λ where
      tt → Var t₂ , 1 , suc sn -- ρ nums contains n
      ff → t , 0 , suc sn -- ρ nums does not contain n
    nothing → Var t₂ , 1 , suc sn
  ff → case op of λ where
    tt → case rewrite-termh (hnf Γ unfold-head t) Γ op on eq t₁ t₂ sn of λ where
      (t' , 0 , sn') → t , 0 , sn' -- if no rewrites were performed, return the pre-hnf t
      (t' , n' , sn') → t' , n' , sn'
    ff → rewrite-termh t Γ op on eq t₁ t₂ sn

rewrite-termh (App t t') =
  pure App <*> rewrite-terma t <*> rewrite-terma t'
rewrite-termh (Lam NotErased y nothing t) =
  rewrite-rename-var y λ y' → pure (Lam NotErased y' nothing) <*>
  rewrite-abs y y' rewrite-terma t
rewrite-termh (Var x) = pure (Var x)
rewrite-termh (LetTm ff x nothing t t') Γ = rewrite-terma (subst Γ t x t') Γ
--  rewrite-rename-var x λ x' → pure (Let pi₁) <*>
--  (pure (DefTerm pi₂ x' NoType) <*> rewrite-terma t) <*>
--  rewrite-abs x x' rewrite-terma t'
-- ^^^ Need to DEFINE "x" as "hnf Γ unfold-head t tt", not just declare it!
--     We may instead simply rewrite t' after substituting t for x
rewrite-termh (Mu x t nothing t~ ms) =
  rewrite-rename-var x λ x' →
  pure (Mu x') <*>
  rewrite-terma t <*>
  pure nothing <*>
  pure t~ <*>
  foldr (λ c r → pure _::_ <*> rewrite-case (just $ x , x') c <*> r)
    (pure []) ms
rewrite-termh (Sigma tᵢ t nothing t~ ms) =
  pure (Sigma tᵢ) <*>
  rewrite-terma t <*>
  pure nothing <*>
  pure t~ <*>
  foldr (λ c r → pure _::_ <*> rewrite-case nothing c <*> r)
    (pure []) ms
rewrite-termh = pure

rewrite-case xᵣ? (Case x cas t T) =
  let f = maybe-else' xᵣ? id (uncurry rewrite-abs) rewrite-terma in
  pure (uncurry $ Case x) <*>
  foldr {B = rewrite-t case-args → (term → rewrite-t term) → rewrite-t (case-args × term)}
    (λ {(CaseArg ff x nothing) r cas fₜ →
      r (rewrite-rename-var x λ x' → pure _::_ <*> pure (CaseArg ff x' nothing) <*> cas) (λ t → rewrite-rename-var x λ x' → rewrite-abs x x' fₜ t); _ → id})
    (λ cas fₜ → pure (_,_ ∘ reverse) <*> cas <*> fₜ t) cas (pure []) f <*> return T

rewrite-type T Γ tt on eq t₁ t₂ sn
  with rewrite-typeh (hnf Γ unfold-head-elab T) Γ tt on eq t₁ t₂ sn
...| T' , 0 , sn' = T  , 0 , sn'
...| T' , n , sn' = T' , n , sn'
rewrite-type = rewrite-typeh

rewrite-typeh (TpAbs me x atk T) =
  rewrite-rename-var x λ x' →
  pure (TpAbs me x') <*> rewrite-tpkd atk <*>
  rewrite-abs x x' rewrite-type T
rewrite-typeh (TpIota x T T') =
  rewrite-rename-var x λ x' →
  pure (TpIota x') <*> rewrite-type T <*>
  rewrite-abs x x' rewrite-type T'
rewrite-typeh (TpApp T tT) =
  pure TpApp <*> rewrite-typeh T <*> rewrite-tmtp tT
rewrite-typeh (TpEq t₁ t₂) =
  pure TpEq <*> (pure erase <*> rewrite-term t₁) <*>
  (pure erase <*> rewrite-term t₂)
rewrite-typeh (TpLam x atk T) =
  rewrite-rename-var x λ x' →
  pure (TpLam x') <*> rewrite-tpkd atk <*>
  rewrite-abs x x' rewrite-type T
rewrite-typeh (TpHole pi) = pure (TpHole pi)
rewrite-typeh (TpVar x) = pure (TpVar x)

-- If we ever implement kind-level rewriting, we will need to go through
-- all the types of kind pi binding a term or type-to-kind arrow
-- if the right-hand side variable is free in the types of the bound variable,
-- and substitute each occurence of the term variable (eta-expanding if necessary)
-- in the body of the type with itself surrounded by a rewrite back the original
-- expected type (unless we lifted a term, then it gets really tricky because
-- we may not want to rewrite back?).
rewrite-kind = pure
rewrite-liftingType = pure

rewrite-tpkd (Tkt T) = pure Tkt <*> rewrite-type T
rewrite-tpkd (Tkk k) = pure Tkk <*> rewrite-kind k

rewrite-tmtp (Ttm t) = pure Ttm <*> rewrite-term t
rewrite-tmtp (Ttp T) = pure Ttp <*> rewrite-type T

post-rewrite-binder-type : ∀ {ed} → ctxt → var → term → (var → tpkd → ctxt → ctxt) → var → ⟦ ed ⟧ → type → ⟦ ed ⟧
post-rewrite-binder-type Γ x eq tk-decl x' Tₓ Tₓ' with is-free-in x Tₓ'
...| ff = Tₓ
...| tt = subst (tk-decl x' (Tkt Tₓ') Γ) (Rho eq x Tₓ' (Var x')) x' Tₓ

post-rewrite-binder-kind : ∀ {ed} → ctxt → var → term → (var → tpkd → ctxt → ctxt) → var → ⟦ ed ⟧ → kind → ⟦ ed ⟧
post-rewrite-binder-kind Γ x eq tk-decl x' Tₓ kₓ' = Tₓ

post-rewrite-binder-tk : ∀ {ed} → ctxt → var → term → (var → tpkd → ctxt → ctxt) → var → ⟦ ed ⟧ → tpkd → ⟦ ed ⟧
post-rewrite-binder-tk Γ x eq tk-decl x' Tₓ (Tkt Tₓ') =
  post-rewrite-binder-type Γ x eq tk-decl x' Tₓ Tₓ'
post-rewrite-binder-tk Γ x eq tk-decl x' Tₓ (Tkk kₓ') =
  post-rewrite-binder-kind Γ x eq tk-decl x' Tₓ kₓ'

post-rewriteh : ctxt → var → term → (ctxt → var → term → tpkd → tpkd) → (var → tpkd → ctxt → ctxt) → type → type × kind

post-rewriteh Γ x eq prtk tk-decl (TpAbs me x' atk T) =
  let atk = prtk Γ x eq atk
      T = fst $ post-rewriteh (tk-decl x' atk Γ) x eq prtk tk-decl T
      T = post-rewrite-binder-tk Γ x eq tk-decl x' T atk in
  TpAbs me x' atk T , KdStar
post-rewriteh Γ x eq prtk tk-decl (TpIota x' T T') =
  let T = fst $ post-rewriteh Γ x eq prtk tk-decl T
      T' = fst $ post-rewriteh (tk-decl x' (Tkt T) Γ) x eq prtk tk-decl T'
      T' = post-rewrite-binder-type Γ x eq tk-decl x' T' T in
  TpIota x' T T' , KdStar
post-rewriteh Γ x eq prtk tk-decl (TpApp T (Ttp T')) =
  elim-pair (post-rewriteh Γ x eq prtk tk-decl T') λ T' k' →
  elim-pair (post-rewriteh Γ x eq prtk tk-decl T) λ where
    T (KdAbs x' atk k) → TpApp T (Ttp T') , hnf Γ unfold-head-elab (subst Γ T' x' k)
    T k → TpApp T (Ttp T') , k
post-rewriteh Γ x eq prtk tk-decl (TpApp T (Ttm t)) =
  let t2 T' = if is-free-in x T' then Rho (VarSigma eq) x T' t else t in
  elim-pair (post-rewriteh Γ x eq prtk tk-decl T) λ where
    T (KdAbs x' (Tkt T') k) →
      let t3 = t2 T' in TpApp T (Ttm t3) , hnf Γ unfold-head-elab (subst Γ t3 x' k)
    T k → TpApp T (Ttm t) , k
post-rewriteh Γ x eq prtk tk-decl (TpLam x' atk T) =
  let atk = prtk Γ x eq atk in
  elim-pair (post-rewriteh (tk-decl x' atk Γ) x eq prtk tk-decl T) λ T k →
  let T = post-rewrite-binder-tk Γ x eq tk-decl x' T atk
      k = post-rewrite-binder-tk Γ x eq tk-decl x' k atk in
  TpLam x' atk T , KdAbs x' atk k
post-rewriteh Γ x eq prtk tk-decl (TpVar x') with env-lookup Γ x'
...| just (type-decl k , _) = TpVar x' , hnf Γ unfold-head-elab k
...| just (type-def mps _ T k , _) = TpVar x' , (hnf Γ unfold-head-elab (maybe-else id abs-expand-kind mps k))
...| _ = TpVar x' , KdStar
post-rewriteh Γ x eq prtk tk-decl T = T , KdStar

{-# TERMINATING #-}
post-rewrite : ctxt → var → (eq t₂ : term) → type → type
post-rewrite Γ x eq t₂ T = subst Γ t₂ x (fst (post-rewriteh Γ x eq prtk tk-decl T)) where
  prtk : ctxt → var → term → tpkd → tpkd
  tk-decl : var → tpkd → ctxt → ctxt
  prtk Γ x t (Tkt T) = Tkt (fst (post-rewriteh Γ x t prtk tk-decl T))
  prtk Γ x t (Tkk k) = Tkk (hnf Γ unfold-head-elab k)
  tk-decl x atk Γ =
    record Γ { i = trie-insert (ctxt.i Γ) x (either-else' atk term-decl type-decl , "" , "") }

-- Functions for substituting the type T in ρ e @ x . T - t
rewrite-at-t : Set → Set
rewrite-at-t X = ctxt → var → maybe term → 𝔹 → X → X → X
{-# TERMINATING #-}
rewrite-at : rewrite-at-t type
rewrite-at' : ∀ {ed} → rewrite-at-t ⟦ ed ⟧ → rewrite-at-t ⟦ ed ⟧
rewrite-ath : rewrite-at-t type
rewrite-atₖ : rewrite-at-t kind
rewrite-athₖ : rewrite-at-t kind
rewrite-at-tk : rewrite-at-t tpkd

rewrite-at-tk Γ x eq b (Tkt T) (Tkt T') = Tkt (rewrite-at Γ x eq b T T')
rewrite-at-tk Γ x eq b (Tkk k) (Tkk k') = Tkk (rewrite-atₖ Γ x eq b k k')
rewrite-at-tk Γ x eq b atk1 atk2 = atk1

rewrite-at = rewrite-at' rewrite-ath
rewrite-atₖ = rewrite-at' rewrite-athₖ

rewrite-head-types-match : ∀ {ed} → ctxt → var → (complete partial : ⟦ ed ⟧) → 𝔹
rewrite-head-types-match{TYPE} Γ x (TpApp T _) (TpApp T' _) = conv-type Γ T ([ Γ - Hole pi-gen / x ] T')
rewrite-head-types-match Γ x T T' = tt

rewrite-at' ra Γ x eq b T T' =
  if ~ is-free-in x T'
    then T
    else if b && ~ rewrite-head-types-match Γ x T T'
      then ra Γ x eq ff (hnf Γ unfold-head-elab T) (hnf Γ unfold-head-elab T')
      else ra Γ x eq b T T'

rewrite-athₖ Γ x eq b (KdAbs x1 atk1 k1) (KdAbs x2 atk2 k2) =
  KdAbs x1 (rewrite-at-tk Γ x eq tt atk1 atk2) (rewrite-atₖ (ctxt-var-decl x1 Γ) x eq tt k1 $ rename-var Γ x2 x1 k2)
rewrite-athₖ Γ x eq b KdStar KdStar = KdStar
rewrite-athₖ Γ x eq tt k1 k2 = rewrite-atₖ Γ x eq ff (hnf Γ unfold-head-elab k1) (hnf Γ unfold-head-elab k2)
rewrite-athₖ Γ x eq ff k1 k2 = k1

rewrite-ath Γ x eq b (TpAbs me1 x1 atk1 T1) (TpAbs me2 x2 atk2 T2) =
  TpAbs me1 x1 (rewrite-at-tk Γ x eq tt atk1 atk2) (rewrite-at (ctxt-var-decl x1 Γ) x eq tt T1 (rename-var Γ x2 x1 T2))
rewrite-ath Γ x eq b (TpIota x1 T1 T1') (TpIota x2 T2 T2') =
  TpIota x1 (rewrite-at Γ x eq tt T1 T2) (rewrite-at (ctxt-var-decl x1 Γ) x eq tt T1' (rename-var Γ x2 x1 T2'))
rewrite-ath Γ x eq b (TpApp T1 (Ttp T1')) (TpApp T2 (Ttp T2')) =
  TpApp (rewrite-at Γ x eq b T1 T2) (Ttp (rewrite-at Γ x eq tt T1' T2'))
rewrite-ath Γ x eq b (TpApp T1 (Ttm t1)) (TpApp T2 (Ttm t2)) =
  TpApp (rewrite-at Γ x eq b T1 T2) (Ttm (maybe-else' (ifMaybe (is-free-in x t2) eq) t1 λ eq → rewrite-mk-phi x eq t1 t2))
rewrite-ath Γ x eq b (TpEq t1 t1') (TpEq t2 t2') =
  TpEq t2 t2'
rewrite-ath Γ x eq b (TpLam x1 atk1 T1) (TpLam x2 atk2 T2) =
  TpLam x1 (rewrite-at-tk Γ x eq tt atk1 atk2) (rewrite-at (ctxt-var-decl x1 Γ) x eq tt T1 (rename-var Γ x2 x1 T2))
rewrite-ath Γ x eq b (TpVar x1) (TpVar x2) = TpVar x1
rewrite-ath Γ x eq b (TpHole pi1) (TpHole pi2) = TpHole pi1
rewrite-ath Γ x eq tt T1 T2 = rewrite-at Γ x eq ff (hnf Γ unfold-head-elab T1) (hnf Γ unfold-head-elab T2)
rewrite-ath Γ x eq ff T1 T2 = T1

hnf-ctr : ctxt → var → type → type
hnf-ctr Γ x T = hnf Γ unfold-no-defs (rewrite-at Γ x nothing tt (hnf Γ (unfold tt ff ff) T) $ hnf Γ (record unfold-all {unfold-erase = ff}) T)

{-# TERMINATING #-}
refine-term : ctxt → tmtp → var → term → term
refine-type : ctxt → tmtp → var → type → type
refine-typeh : ctxt → tmtp → var → type → type
refine-kind : ctxt → tmtp → var → kind → kind
refine : ∀ {ed} → ctxt → tmtp → var → ⟦ ed ⟧ → ⟦ ed ⟧

refine {TERM} = refine-term
refine {TYPE} = refine-type
refine {KIND} = refine-kind

refine-term Γ (Ttp T) to t = t
refine-term Γ (Ttm t') to t with rewrite-term t Γ ff nothing nothing t' to 0
...| t'' , zero , _ = t
...| t'' , suc _ , _ = t''

refine-type Γ fm to T =
  if either-else' fm (const ff) (conv-type Γ T)
    then TpVar to
    else refine-typeh Γ fm to T

refine-typeh Γ fm to (TpAbs me x atk T) =
  let x' = fresh-var Γ x in
  TpAbs me x' (refine Γ fm to -tk atk) (refine-type (ctxt-var-decl x' Γ) fm to (rename-var Γ x x' T))
refine-typeh Γ fm to (TpIota x T T') =
  let x' = fresh-var Γ x in
  TpIota x' (refine-type Γ fm to T) (refine-type (ctxt-var-decl x' Γ) fm to (rename-var Γ x x' T'))
refine-typeh Γ fm to (TpApp T tT) =
   TpApp (refine-type Γ fm to T) (refine Γ fm to -tT tT)
refine-typeh Γ fm to (TpEq t₁ t₂) =
  TpEq (refine-term Γ fm to t₁) (refine-term Γ fm to t₂)
refine-typeh Γ fm to (TpLam x atk T) =
  let x' = fresh-var Γ x in
  TpLam x' (refine Γ fm to -tk atk) (refine-type (ctxt-var-decl x' Γ) fm to (rename-var Γ x x' T))
refine-typeh Γ fm to (TpHole pi) = TpHole pi
refine-typeh Γ fm to (TpVar x) = TpVar x

refine-kind Γ fm to (KdAbs x atk k) =
  let x' = fresh-var Γ x in
  KdAbs x (refine Γ fm to -tk atk) (refine-kind (ctxt-var-decl x' Γ) fm to (rename-var Γ x x' k))
refine-kind Γ fm to (KdHole pi) = KdHole pi
refine-kind Γ fm to KdStar = KdStar

refine-motive : ctxt → indices → (asᵢ : 𝕃 tmtp) → (expected : type) → type
refine-motive Γ is as =
  foldr
    (λ where
      (Index x atk , ty) f Γ T →
        let body = f (ctxt-var-decl x Γ) $ refine-type (ctxt-var-decl x Γ) ty x T
            x' = if is-free-in x body then x else ignored-var in
        TpLam x' atk body)
    (λ Γ T → T) (zip (rename-indices Γ is as) as) Γ

-- Given a context, the (qualified) scrutinee, the (qualified) datatype name,
-- the datatype's indices, the arguments for module parameter instantiation,
-- the arguments for the indices in the type of the scrutinee, and the expected type,
-- calculate a possibly ill-typed motive that is approximately abstracted over the
-- indices and the scrutinee itself.
{-
refine-motive : ctxt → (scrutinee : term) → (datatype-name : var) → indices → (mod-as : 𝕃 tty) → (idx-as : 𝕃 tty) → (expected : type) → type
refine-motive Γ t name is asₚ asᵢ =
  let x = fresh-var (add-indices-to-ctxt is Γ) "x"
      atkₓ = Tkt $ indices-to-tpapps is $ recompose-tpapps asₚ $ TpVar pi-gen name
      as' = asᵢ ++ [ tterm t ]
      is' = rename? Γ empty-renamectxt (is ++ [ Index x atkₓ ]) as'
      as = zip is' as' in
  foldr
    (λ where
      (Index x atk , ty) f Γ T →
        TpLambda pi-gen pi-gen x atk $ f (ctxt-var-decl x Γ) $
          refine-type (ctxt-var-decl x Γ) ty x T)
    (λ Γ T → T) as Γ
  where
  get-var : var → tty → var
  get-var x (tterm (Var _ x')) = maybe-else (unqual-local x') id $ var-suffix x'
  get-var x (ttype (TpVar _ x')) = maybe-else (unqual-local x') id $ var-suffix x'
  get-var x _ = x

  rename? : ctxt → renamectxt → indices → 𝕃 tty → indices
  rename? Γ ρ (Index x atk :: is) (ty :: tys) =
    let x' = get-var x ty in
    Index x' (subst-renamectxt Γ ρ atk) :: rename? (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') is tys
  rename? _ _ _ _ = []
-}


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.List
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

infix  0 case_of_
case_of_ : ∀ {a b}{A : Set a}{B : Set b} → A → (A → B) → B
case x of f = f x

map : ∀ {a b}{A : Set a}{B : Set b} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

reverse : ∀ {a}{A : Set a} → List A → List A
reverse {A = A} xs = reverseAcc xs []
  where
    reverseAcc : List A → List A → List A
    reverseAcc [] a = a
    reverseAcc (x ∷ xs) a = reverseAcc xs (x ∷ a)

data Maybe (X : Set) : Set where
  nothing : Maybe X
  just : X → Maybe X

data Fin : Nat → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

record RVec {a} (X : Set a) (n : Nat) : Set a where
  constructor vec
  field sel : Fin n → X

test-rvec : Nat → RVec Nat 5
test-rvec x = vec λ _ → x

get-len : Definition → TC Term
get-len (function (clause _ _ (con (quote vec)
                                  (_ ∷ _ ∷ (arg _ a) ∷ _)) ∷ [])) = quoteTC a
get-len _ = quoteTC "ERROR"

macro
  def-reg : Name → Term → TC ⊤
  def-reg n hole = do
    d ← getDefinition n
    l ← get-len d
    unify hole l

  def-recons : Name → Term → TC ⊤
  def-recons n hole = do
    d ← withReconstructed (getDefinition n)
    l ← get-len d
    unify hole l

  -- normaliseR perserves reconstructed expressions.
  def-normR : Name → Term → TC ⊤
  def-normR n hole = do
    (function (clause tel ps t ∷ [])) ←
      withReconstructed (getDefinition n)
      where _ → quoteTC "ERROR" >>= unify hole
    let ctx = map snd tel
    t ← inContext (reverse ctx)
        (withReconstructed (normalise t))
    let d = function (clause tel ps t ∷ [])
    get-len d >>= unify hole

  -- normaliseR perserves reconstructed expressions.
  def-redR : Name → Term → TC ⊤
  def-redR n hole = do
    (function (clause tel ps t ∷ [])) ←
      withReconstructed (getDefinition n)
      where _ → quoteTC "ERROR" >>= unify hole
    let ctx = map snd tel
    t ← inContext (reverse ctx) (withReconstructed (reduce t))
    let d = function (clause tel ps t ∷ [])
    get-len d >>= unify hole

test₁ : unknown ≡ def-reg test-rvec
test₁ = refl

test₂ : (lit (nat 5)) ≡ def-recons test-rvec
test₂ = refl

test₃ : (lit (nat 5)) ≡ def-normR test-rvec
test₃ = refl

test₄ : (lit (nat 5)) ≡ def-redR test-rvec
test₄ = refl

pictx : Term → List (Arg Type)
pictx (pi a (abs s x)) = a ∷ pictx x
pictx _ = []

macro
  get-ctx : Name → Term → TC ⊤
  get-ctx n hole = do
    t ← getType n
    let c = pictx t
    c ← withReconstructed
        (inContext (reverse c) getContext)
    quoteTC c >>= unify hole

bar : (A : Set) (eq : [] {A = A} ≡ []) (x : Nat) → ⊤
bar _ _ _ = tt

-- if getContext were to work incorrectly, this function wouldn't typecheck
test₅ : List (Arg Type)
test₅ = get-ctx bar

data NotAVec (X : Set) (y : Nat) : Set where
  mk : NotAVec X y

f : ∀ {n} → NotAVec Nat n → NotAVec Nat (suc n)
f mk = mk

macro
  chk-type : Term → TC ⊤
  chk-type hole = do
    T ← quoteTC (NotAVec Nat 5)
    t ← quoteTC (mk {X = Nat} {y = 5})
    (con _ (_ ∷ arg _ t ∷ [])) ← withReconstructed (checkType t T)
      where _ → quoteTC "ERROR" >>= unify hole
    quoteTC t >>= unify hole

-- checkType would leave unknown's without the call to withReconstructed
test₆ : chk-type ≡ lit (nat 5)
test₆ = refl

q : [] {A = Nat} ≡ [] {A = Nat}
q = refl

macro
  inf-type : Term → TC ⊤
  inf-type hole = do
    (function (clause _ _ b ∷ [])) ← withReconstructed (getDefinition (quote q))
      where _ → quoteTC "ERROR" >>= unify hole
    (def _ (l ∷ L ∷ e₁ ∷ e₂ ∷ [])) ← withReconstructed  (inferType b)
      where _ → quoteTC "ERROR" >>= unify hole
    (arg _ (con _ (_ ∷ (arg _ N) ∷ []))) ← returnTC e₁
      where _ → quoteTC "ERROR" >>= unify hole
    quoteTC N >>= unify hole

-- inferType would not reconstruct the arguments within the type
-- without the call to withReconstructed
test₇ : inf-type ≡ def (quote Nat) []
test₇ = refl

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Pi.Invariants where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Data.List as L hiding (_∷_)
open import Relation.Binary.PropositionalEquality
open import Pi.Syntax
open import Pi.Opsem
open import Pi.NoRepeat

-- Get the type of the deepest context
get𝕌 : ∀ {A B} → Context {A} {B} → 𝕌 × 𝕌
get𝕌 {A} {B} ☐ = A , B
get𝕌 (☐⨾ c₂ • κ) = get𝕌 κ
get𝕌 (c₁ ⨾☐• κ) = get𝕌 κ
get𝕌 (☐⊕ c₂ • κ) = get𝕌 κ
get𝕌 (c₁ ⊕☐• κ) = get𝕌 κ
get𝕌 (☐⊗[ c₂ , x ]• κ) = get𝕌 κ
get𝕌 ([ c₁ , x ]⊗☐• κ) = get𝕌 κ

get𝕌State : (st : State) → 𝕌 × 𝕌
get𝕌State ⟨ c ∣ v ∣ κ ⟩ = get𝕌 κ
get𝕌State ［ c ∣ v ∣ κ ］ = get𝕌 κ

-- Reconstruct the whole combinator from context
getℂκ : ∀ {A B} → A ↔ B → Context {A} {B} → ∃[ C ] ∃[ D ] (C ↔ D)
getℂκ c ☐ = _ , _ , c
getℂκ c (☐⨾ c₂ • κ) = getℂκ (c ⨾ c₂) κ
getℂκ c (c₁ ⨾☐• κ) = getℂκ (c₁ ⨾ c) κ
getℂκ c (☐⊕ c₂ • κ) = getℂκ (c ⊕ c₂) κ
getℂκ c (c₁ ⊕☐• κ) = getℂκ (c₁ ⊕ c) κ
getℂκ c (☐⊗[ c₂ , x ]• κ) = getℂκ (c ⊗ c₂) κ
getℂκ c ([ c₁ , x ]⊗☐• κ) = getℂκ (c₁ ⊗ c) κ

getℂ : State → ∃[ A ] ∃[ B ] (A ↔ B)
getℂ ⟨ c ∣ _ ∣ κ ⟩ = getℂκ c κ
getℂ ［ c ∣ _ ∣ κ ］ = getℂκ c κ

-- The reconstructed combinator stays the same
ℂInvariant : ∀ {st st'} → st ↦ st' → getℂ st ≡  getℂ st'
ℂInvariant ↦₁ = refl
ℂInvariant ↦₂ = refl
ℂInvariant ↦₃ = refl
ℂInvariant ↦₄ = refl
ℂInvariant ↦₅ = refl
ℂInvariant ↦₆ = refl
ℂInvariant ↦₇ = refl
ℂInvariant ↦₈ = refl
ℂInvariant ↦₉ = refl
ℂInvariant ↦₁₀ = refl
ℂInvariant ↦₁₁ = refl
ℂInvariant ↦₁₂ = refl

ℂInvariant* : ∀ {st st'} → st ↦* st' → getℂ st ≡  getℂ st'
ℂInvariant* ◾ = refl
ℂInvariant* (r ∷ rs) = trans (ℂInvariant r) (ℂInvariant* rs)

-- Append a context to another context
appendκ : ∀ {A B} → (ctx : Context {A} {B}) → let (C , D) = get𝕌  ctx
                                              in  Context {C} {D} → Context {A} {B}
appendκ ☐ ctx = ctx
appendκ (☐⨾ c₂ • κ) ctx = ☐⨾ c₂ • appendκ κ ctx
appendκ (c₁ ⨾☐• κ) ctx = c₁ ⨾☐• appendκ κ ctx
appendκ (☐⊕ c₂ • κ) ctx = ☐⊕ c₂ • appendκ κ ctx
appendκ (c₁ ⊕☐• κ) ctx = c₁ ⊕☐• appendκ κ ctx
appendκ (☐⊗[ c₂ , x ]• κ) ctx = ☐⊗[ c₂ , x ]• appendκ κ ctx
appendκ ([ c₁ , x ]⊗☐• κ) ctx = [ c₁ , x ]⊗☐• appendκ κ ctx

appendκState : ∀ st → let (A , B) = get𝕌State st
                      in  Context {A} {B} → State
appendκState ⟨ c ∣ v ∣ κ ⟩ ctx = ⟨ c ∣ v ∣ appendκ κ ctx ⟩
appendκState ［ c ∣ v ∣ κ ］ ctx = ［ c ∣ v ∣ appendκ κ ctx ］

-- The type of context does not change during execution
𝕌Invariant : ∀ {st st'} → st ↦ st' → get𝕌State st ≡ get𝕌State st'
𝕌Invariant ↦₁  = refl
𝕌Invariant ↦₂  = refl
𝕌Invariant ↦₃  = refl
𝕌Invariant ↦₄  = refl
𝕌Invariant ↦₅  = refl
𝕌Invariant ↦₆  = refl
𝕌Invariant ↦₇  = refl
𝕌Invariant ↦₈  = refl
𝕌Invariant ↦₉  = refl
𝕌Invariant ↦₁₀ = refl
𝕌Invariant ↦₁₁ = refl
𝕌Invariant ↦₁₂ = refl

𝕌Invariant* : ∀ {st st'} → st ↦* st' → get𝕌State st ≡ get𝕌State st'
𝕌Invariant* ◾ = refl
𝕌Invariant* (r ∷ rs) = trans (𝕌Invariant r) (𝕌Invariant* rs)

-- Appending context does not affect reductions
appendκ↦ : ∀ {st st'} → (r : st ↦ st') (eq : get𝕌State st ≡  get𝕌State st')
         → (κ : Context {proj₁ (get𝕌State st)} {proj₂ (get𝕌State st)})
         → appendκState st κ ↦ appendκState st' (subst (λ {(A , B) → Context {A} {B}}) eq κ)
appendκ↦ ↦₁ refl κ = ↦₁
appendκ↦ ↦₂ refl κ = ↦₂
appendκ↦ ↦₃ refl κ = ↦₃
appendκ↦ ↦₄ refl κ = ↦₄
appendκ↦ ↦₅ refl κ = ↦₅
appendκ↦ ↦₆ refl κ = ↦₆
appendκ↦ ↦₇ refl κ = ↦₇
appendκ↦ ↦₈ refl κ = ↦₈
appendκ↦ ↦₉ refl κ = ↦₉
appendκ↦ ↦₁₀ refl κ = ↦₁₀
appendκ↦ ↦₁₁ refl κ = ↦₁₁
appendκ↦ ↦₁₂ refl κ = ↦₁₂

appendκ↦* : ∀ {st st'} → (rs : st ↦* st') (eq : get𝕌State st ≡  get𝕌State st')
          → (κ : Context {proj₁ (get𝕌State st)} {proj₂ (get𝕌State st)})
          → appendκState st κ ↦* appendκState st' (subst (λ {(A , B) → Context {A} {B}}) eq κ)
appendκ↦* ◾ refl ctx = ◾
appendκ↦* (↦₁ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦₁ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦₂ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦₂ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦₃ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦₃ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦₄ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦₄ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦₅ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦₅ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦₆ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦₆ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦₇ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦₇ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦₈ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦₈ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦₉ {κ = κ} ∷ rs) eq ctx = appendκ↦ (↦₉ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦₁₀{κ = κ} ∷ rs) eq ctx = appendκ↦ (↦₁₀ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦₁₁{κ = κ} ∷ rs) eq ctx = appendκ↦ (↦₁₁ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx
appendκ↦* (↦₁₂{κ = κ} ∷ rs) eq ctx = appendκ↦ (↦₁₂ {κ = κ}) refl ctx ∷ appendκ↦* rs eq ctx


text:
module Thesis.SIRelBigStep.ArithExtra where

open import Relation.Binary.PropositionalEquality
open import Data.Nat public
open import Data.Nat.Properties public
open import Relation.Binary hiding (_⇒_)

lt1 : ∀ {k n} → k < n → k ≤ n
lt1 (s≤s p) = ≤-step p

m∸n≤m : ∀ m n → m ∸ n ≤ m
m∸n≤m m zero = ≤-refl
m∸n≤m zero (suc n) = z≤n
m∸n≤m (suc m) (suc n) = ≤-step (m∸n≤m m n)

suc∸ : ∀ m n → n ≤ m → suc (m ∸ n) ≡ suc m ∸ n
suc∸ m zero z≤n = refl
suc∸ (suc m) (suc n) (s≤s n≤m) = suc∸ m n n≤m

sub∸ : ∀ m n o → m + n ≤ o → n ≤ o ∸ m
sub∸ m n o n+m≤o rewrite +-comm m n | cong (_≤ o ∸ m) (sym (m+n∸n≡m n m)) = ∸-mono n+m≤o (≤-refl {m})

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------
-- An implementation of the Fibonacci sequence using tail
------------------------------------------------------------------------

module SingletonChunks where

open import Codata.Musical.Notation
open import Codata.Musical.Stream as S using (Stream; _≈_; _∷_)
open import Data.Bool
open import Data.Nat
open import Data.Vec as V using (Vec; []; _∷_)
import Relation.Binary.PropositionalEquality as P

------------------------------------------------------------------------
-- Stream programs

-- StreamP b A encodes programs generating streams in chunks of size
-- (at least) 1. The first chunk may be empty if b is false.

infixr 5 _∷_

data StreamP : Bool → Set → Set₁ where
  [_]     : ∀ {A} (xs : ∞ (StreamP true A)) → StreamP false A
  _∷_     : ∀ {A} (x : A) (xs : StreamP false A) → StreamP true A
  forget  : ∀ {A} (xs : StreamP true A) → StreamP false A
  tail    : ∀ {A} (xs : StreamP true A) → StreamP false A
  zipWith : ∀ {b A B C} (f : A → B → C)
            (xs : StreamP b A) (ys : StreamP b B) → StreamP b C

data StreamW : Bool → Set → Set₁ where
  [_] : ∀ {A} (xs : StreamP true A) → StreamW false A
  _∷_ : ∀ {A} (x : A) (xs : StreamW false A) → StreamW true A

forgetW : ∀ {A} → StreamW true A → StreamW false A
forgetW (x ∷ [ xs ]) = [ x ∷ forget xs ]

tailW : ∀ {A} → StreamW true A → StreamW false A
tailW (x ∷ xs) = xs

zipWithW : ∀ {b A B C} → (A → B → C) →
           StreamW b A → StreamW b B → StreamW b C
zipWithW f [ xs ]   [ ys ]   = [ zipWith f xs ys ]
zipWithW f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWithW f xs ys

whnf : ∀ {b A} → StreamP b A → StreamW b A
whnf [ xs ]            = [ ♭ xs ]
whnf (x ∷ xs)          = x ∷ whnf xs
whnf (forget xs)       = forgetW (whnf xs)
whnf (tail xs)         = tailW (whnf xs)
whnf (zipWith f xs ys) = zipWithW f (whnf xs) (whnf ys)

mutual

  ⟦_⟧W : ∀ {A} → StreamW true A → Stream A
  ⟦ x ∷ [ xs ] ⟧W = x ∷ ♯ ⟦ xs ⟧P

  ⟦_⟧P : ∀ {A} → StreamP true A → Stream A
  ⟦ xs ⟧P = ⟦ whnf xs ⟧W

------------------------------------------------------------------------
-- The Fibonacci sequence

fib : StreamP true ℕ
fib = 0 ∷ [ ♯ (1 ∷ zipWith _+_ (forget fib) (tail fib)) ]

------------------------------------------------------------------------
-- The definition of fib is correct

-- ⟦_⟧ is homomorphic with respect to zipWith/S.zipWith.

zipWith-hom : ∀ {A B C} (_∙_ : A → B → C) xs ys →
              ⟦ zipWith _∙_ xs ys ⟧P ≈ S.zipWith _∙_ ⟦ xs ⟧P ⟦ ys ⟧P
zipWith-hom _∙_ xs ys with whnf xs | whnf ys
zipWith-hom _∙_ xs ys | x ∷ [ xs′ ] | y ∷ [ ys′ ] =
  P.refl ∷ ♯ zipWith-hom _∙_ xs′ ys′

-- forget is the identity on streams.

open import MapIterate as M using (_≈P_; _∷_; _≈⟨_⟩_; _∎)
open import Relation.Binary.PropositionalEquality as P using (_≡_; [_])

forget-lemma : ∀ {A} x (xs : StreamP true A) →
               ⟦ x ∷ forget xs ⟧P ≈P x ∷ ♯ ⟦ xs ⟧P
forget-lemma x xs with whnf xs | P.inspect whnf xs
... | y ∷ [ ys ] | [ eq ] = x ∷ ♯ helper eq
  where
  helper : whnf xs ≡ y ∷ [ ys ] →
           ⟦ y ∷ forget ys ⟧P ≈P ⟦ xs ⟧P
  helper eq rewrite eq = _ ≈⟨ forget-lemma y ys ⟩ (y ∷ ♯ (_ ∎))

-- The stream ⟦ fib ⟧P satisfies its intended defining equation.

open import Relation.Binary
module SS {A : Set} = Setoid (S.setoid A)

fib-correct :
  ⟦ fib ⟧P ≈ 0 ∷ ♯ (1 ∷ ♯ S.zipWith _+_ ⟦ fib ⟧P (S.tail ⟦ fib ⟧P))
fib-correct =
  P.refl ∷ ♯ (P.refl ∷ ♯ SS.trans
   (zipWith-hom _+_ (0 ∷ forget fib′) fib′)
   (S.zipWith-cong _+_ (SS.trans (M.soundP (forget-lemma 0 fib′))
                                 (P.refl ∷ ♯ SS.refl)) SS.refl))
  where fib′ = 1 ∷ zipWith _+_ (forget fib) (tail fib)

------------------------------------------------------------------------
-- An equality proof language

infix  4 _≈[_]P_ _≈[_]W_
infix  3 _∎
infixr 2 _≈⟨_⟩_

data _≈[_]P_ : {A : Set} → Stream A → Bool → Stream A → Set₁ where
  [_]     : ∀ {A} {xs ys : Stream A}
            (xs≈ys : ∞ (xs ≈[ true ]P ys)) → xs ≈[ false ]P ys
  _∷_     : ∀ {b A} (x : A) {xs ys : ∞ (Stream A)}
            (xs≈ys : ♭ xs ≈[ b ]P ♭ ys) → x ∷ xs ≈[ true ]P x ∷ ys
  forget  : ∀ {A} {xs ys : Stream A}
            (xs≈ys : xs ≈[ true ]P ys) → xs ≈[ false ]P ys
  _≈⟨_⟩_  : ∀ {b A} (xs : Stream A) {ys zs}
            (xs≈ys : xs ≈[ b ]P ys) (ys≈zs : ys ≈[ b ]P zs) →
            xs ≈[ b ]P zs
  _∎      : ∀ {A} (xs : Stream A) → xs ≈[ true ]P xs
  tail    : ∀ {A} {xs ys : Stream A} (xs≈ys : xs ≈[ true ]P ys) →
            S.tail xs ≈[ false ]P S.tail ys
  zipWith : ∀ {b A B C} (f : A → B → C) {xs xs′ ys ys′}
            (xs≈xs′ : xs ≈[ b ]P xs′) (ys≈ys′ : ys ≈[ b ]P ys′) →
            S.zipWith f xs ys ≈[ b ]P S.zipWith f xs′ ys′

-- Completeness.

completeP : ∀ {A : Set} {xs ys : Stream A} →
            xs ≈ ys → xs ≈[ true ]P ys
completeP (P.refl ∷ xs≈ys) = _ ∷ [ ♯ completeP (♭ xs≈ys) ]

-- Weak head normal forms.

data _≈[_]W_ {A : Set} : Stream A → Bool → Stream A → Set₁ where
  [_]     : {xs ys : Stream A}
            (xs≈ys : xs ≈[ true ]P ys) → xs ≈[ false ]W ys
  _∷_     : ∀ (x : A) {xs ys}
            (xs≈ys : ♭ xs ≈[ true ]P ♭ ys) → x ∷ xs ≈[ true ]W x ∷ ys

consW≈ : ∀ {A b} (x : A) {xs ys} →
         ♭ xs ≈[ b ]W ♭ ys → x ∷ xs ≈[ true ]W x ∷ ys
consW≈ x xs≈ys = x ∷ helper xs≈ys
  where
  helper : ∀ {A b} {xs ys : Stream A} →
           xs ≈[ b ]W ys → xs ≈[ true ]P ys
  helper [ xs≈ys ]   = xs≈ys
  helper (x ∷ xs≈ys) = x ∷ xs≈ys

forgetW≈ : ∀ {A} {xs ys : Stream A} →
           xs ≈[ true ]W ys → xs ≈[ false ]W ys
forgetW≈ (x ∷ xs≈ys) = [ x ∷ forget xs≈ys ]

transW≈ : ∀ {A b} {xs ys zs : Stream A} →
          xs ≈[ b ]W ys → ys ≈[ b ]W zs → xs ≈[ b ]W zs
transW≈ [ xs≈ys ]   [ ys≈zs ]    = [ _ ≈⟨ xs≈ys ⟩ ys≈zs ]
transW≈ (x ∷ xs≈ys) (.x ∷ ys≈zs) = x ∷ (_ ≈⟨ xs≈ys ⟩ ys≈zs)

reflW≈ : ∀ {A} (xs : Stream A) → xs ≈[ true ]W xs
reflW≈ (x ∷ xs) = x ∷ (♭ xs ∎)

tailW≈ : ∀ {A} {xs ys : Stream A} →
         xs ≈[ true ]W ys → S.tail xs ≈[ false ]W S.tail ys
tailW≈ (x ∷ xs≈ys) = [ xs≈ys ]

zipWithW≈ : ∀ {A B C b} (_∙_ : A → B → C) {xs₁ ys₁ xs₂ ys₂} →
            xs₁ ≈[ b ]W ys₁ → xs₂ ≈[ b ]W ys₂ →
            S.zipWith _∙_ xs₁ xs₂ ≈[ b ]W S.zipWith _∙_ ys₁ ys₂
zipWithW≈ _∙_ [ xs₁≈ys₁ ]    [ xs₂≈ys₂ ]    = [ zipWith _∙_ xs₁≈ys₁ xs₂≈ys₂ ]
zipWithW≈ _∙_ (x₁ ∷ xs₁≈ys₁) (x₂ ∷ xs₂≈ys₂) =
  (x₁ ∙ x₂) ∷ zipWith _∙_ xs₁≈ys₁ xs₂≈ys₂

whnf≈ : ∀ {A : Set} {xs ys : Stream A} {b} →
        xs ≈[ b ]P ys → xs ≈[ b ]W ys
whnf≈ [ xs≈ys ]                 = [ ♭ xs≈ys ]
whnf≈ (x ∷ xs≈ys)               = consW≈ x (whnf≈ xs≈ys)
whnf≈ (forget xs≈ys)            = forgetW≈ (whnf≈ xs≈ys)
whnf≈ (xs ≈⟨ xs≈ys ⟩ ys≈zs)     = transW≈ (whnf≈ xs≈ys) (whnf≈ ys≈zs)
whnf≈ (xs ∎)                    = reflW≈ xs
whnf≈ (tail xs≈ys)              = tailW≈ (whnf≈ xs≈ys)
whnf≈ (zipWith f xs≈xs′ ys≈ys′) = zipWithW≈ f (whnf≈ xs≈xs′) (whnf≈ ys≈ys′)

-- Soundness.

mutual

  soundW : {A : Set} {xs ys : Stream A} → xs ≈[ true ]W ys → xs ≈ ys
  soundW (x ∷ xs≈ys) = P.refl ∷ ♯ soundP xs≈ys

  soundP : {A : Set} {xs ys : Stream A} → xs ≈[ true ]P ys → xs ≈ ys
  soundP xs≈ys = soundW (whnf≈ xs≈ys)

------------------------------------------------------------------------
-- The equation given for fib has a unique solution

fib-rhs : Stream ℕ → Stream ℕ
fib-rhs ns = 0 ∷ ♯ (1 ∷ ♯ S.zipWith _+_ ns (S.tail ns))

fib-unique :
  ∀ ms ns → ms ≈ fib-rhs ms → ns ≈ fib-rhs ns → ms ≈[ true ]P ns
fib-unique ms ns ms≈ ns≈ =
  ms         ≈⟨ completeP ms≈ ⟩
  fib-rhs ms ≈⟨ 0 ∷ [ ♯ (1 ∷ zipWith _+_ (forget (fib-unique ms ns ms≈ ns≈))
                                         (tail (fib-unique ms ns ms≈ ns≈))) ] ⟩
  fib-rhs ns ≈⟨ completeP (SS.sym ns≈) ⟩
  ns         ∎

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Sn.Base where

open import Cubical.HITs.Susp
open import Cubical.Foundations.Pointed
open import Cubical.Data.Nat
open import Cubical.Data.NatMinusOne
open import Cubical.Data.Empty
open import Cubical.Foundations.Prelude

S : ℕ₋₁ → Type₀
S neg1 = ⊥
S (ℕ→ℕ₋₁ n) = Susp (S (-1+ n))

S₊ : ℕ → Type₀
S₊ n = S (ℕ→ℕ₋₁ n)

-- Pointed version
S₊∙ : (n : ℕ) → Pointed₀
S₊∙ n = (S₊ n) , north

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
module Function.Domains.Functions where

import      Lvl
open import Function.Domains
open import Function.Domains.Id
open import Structure.Relator.Properties
open import Structure.Setoid
open import Type
open import Type.Dependent

private variable ℓₒ₁ ℓₒ₂ ℓₑ₁ ℓₑ₂ : Lvl.Level

module _ {X : Type{ℓₒ₁}} {Y : Type{ℓₒ₂}} where
  module ⊶ where
    private variable f : X → Y

    -- The function which shrinks the given function's codomain to its image.
    shrink : (f : X → Y) → (X → (⊶ f))
    shrink f(x) = intro (f(x)) (intro x)

    -- Applies an argument of type X to a function of type ((⊶ f) → Y) according to the bijection of {X,(⊶ f)} by f.
    apply : X → ((⊶ f) → Y) → Y
    apply{f} x imgfn = imgfn (shrink f(x))

    fn : (⊶ f) → (X → Y)
    fn{f} _ = f

    arg : (⊶ f) → X
    arg (intro _ (intro x)) = x

    -- Could be interpreted as an identity function with an enlarged codomain.
    -- The value of (⊶ f) interpreted as contained in the "set" Y.
    value : (⊶ f) → Y
    value (intro y _) = y

    value-proof : ⦃ equiv-Y : Equiv{ℓₑ₂}(Y) ⦄ → ∀{x} → (value(intro (f(x)) (intro{f = f} x)) ≡ f(x))
    value-proof = reflexivity(_≡_)

    arg-proof : ⦃ equiv-X : Equiv{ℓₑ₁}(X) ⦄ → ∀{x} → (arg(intro (f(x)) (intro{f = f} x)) ≡ x)
    arg-proof = reflexivity(_≡_)

  -- TODO: Problem with levels
  -- TODO: [⊶]-function-surjective : ∀{f : X → Y} → Surjective([⊶]-function(f))
  -- .[⊶]-function-surjective : ∀{f : X → Y}{y : (⊶ f)} → ∃(x ↦ [⊶]-arg(([⊶]-fn f)(x)) ≡ [⊶]-arg(y))
  -- [⊶]-function-surjective {f} {intro(y-value) ⦃ [∃]-intro (x) ⦃ proof ⦄ ⦄} =
  --   Lang.Irrelevance.axiom(
  --     ([∃]-intro (x)
  --       ⦃ [≡]-with-specific {_}{_} {_}{_} {f(x)} {y-value}
  --         (expr ↦ \ ⦃ [≡]-intro ⦄ → \ ⦃ [≡]-intro ⦄ →
  --           (intro
  --             (expr)
  --             ⦃ [∃]-intro (x) ⦃ [≡]-intro :of: (f(x) ≡ y-value) ⦄ ⦄
  --           )
  --         )
  --         (proof :of: (f(x) ≡ y-value))
  --       ⦄
  --     )
  --   )
    -- ∃(x: X). f(x) ≡ obj(y) //proof:
    -- Take x: X
    --   f(x) ≡ obj(y)
    --   ⇒ intro(f(x)) ⦃ [∃]-intro(x) ⦃ e ⦄ ⦄ ≡ intro(obj(y)) ⦃ [∃]-intro(x) ⦃ e ⦄ ⦄

  -- [⊶]-function-injective : ∀{X}{Y}{f : X → Y} → Injective(f) → Injective([⊶]-function(f))
  -- [⊶]-function-injective{_}{_}{f} {x₁}{x₂} [≡]-intro = [≡]-intro

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:
-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.meta:50 -v tc.conv:20 -v tc.conv.type:50 #-}
module Issue659 where

postulate
  Level : Set
  lzero : Level
  lsuc  : Level → Level
  _⊔_   : Level → Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC  lsuc  #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}

record R (ℓ : Level) : Set ℓ where

postulate
  r : ∀ ℓ → R ℓ

module M (r : ∀ ℓ → R ℓ) where

  data D (ℓ : Level) : Set ℓ where

  id : ∀ {a} {A : Set a} → A → A
  id x = x

  data K : Set where
    k₁ k₂ : K

  P : ∀ {ℓ} → K → Set ℓ → Set ℓ
  P k₁ A = A → A
  P k₂ A = D _

open M r

postulate
  Foo : ∀ {k a} {A : Set a} → P k A → Set

Bar : Set
Bar = Foo M.id

-- Could this error message be improved?

-- Setω is not a valid type.
-- when checking that the expression M.id has type P M.k₁ _34

-- New error:
--
-- ((r₁ : (ℓ : Level) → R ℓ) {a : Level} {A : Set a} → A → A) !=<
-- (P {_33} _32 _34)
-- because this would result in an invalid use of Setω
-- when checking that the expression M.id has type (P {_33} _32 _34)

max_stars_repo_name: dagit/agda

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

module Data.Binary.Proofs.Addition where

open import Relation.Binary.PropositionalEquality
open import Data.Binary.Operations.Unary
open import Data.Binary.Operations.Addition
open import Data.Binary.Proofs.Unary
open import Data.Binary.Proofs.Semantics
open import Data.Binary.Definitions
open import Data.Binary.Operations.Semantics
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Relation.Binary.PropositionalEquality.FasterReasoning
import Data.Nat.Properties as ℕ
open import Function
open import Data.Nat.Reasoning

mutual
  add₀-homo : ∀ xs ys → ⟦ add O xs ys ⇓⟧⁺ ≡ ⟦ xs ⇓⟧⁺ ℕ.+ ⟦ ys ⇓⟧⁺
  add₀-homo 1ᵇ 1ᵇ = refl
  add₀-homo 1ᵇ (O ∷ ys) = refl
  add₀-homo 1ᵇ (I ∷ ys) = cong 2* (inc⁺⁺-homo ys) ⟨ trans ⟩ ℕ.+-suc (suc ⟦ ys ⇓⟧⁺) _
  add₀-homo (O ∷ xs) 1ᵇ = ℕ.+-comm 1 _
  add₀-homo (O ∷ xs) (O ∷ ys) = cong 2* (add₀-homo xs ys) ⟨ trans ⟩ 2*-distrib ⟦ xs ⇓⟧⁺ ⟦ ys ⇓⟧⁺
  add₀-homo (O ∷ xs) (I ∷ ys) = cong suc (cong 2* (add₀-homo xs ys) ⟨ trans ⟩ 2*-distrib ⟦ xs ⇓⟧⁺ ⟦ ys ⇓⟧⁺) ⟨ trans ⟩ sym (ℕ.+-suc (2* ⟦ xs ⇓⟧⁺) (2* ⟦ ys ⇓⟧⁺))
  add₀-homo (I ∷ xs) 1ᵇ = inc⁺⁺-homo (I ∷ xs) ⟨ trans ⟩ cong suc (ℕ.+-comm 1 _)
  add₀-homo (I ∷ xs) (O ∷ ys) = cong suc (cong 2* (add₀-homo xs ys) ⟨ trans ⟩ 2*-distrib ⟦ xs ⇓⟧⁺ ⟦ ys ⇓⟧⁺)
  add₀-homo (I ∷ xs) (I ∷ ys) = cong 2* (add₁-homo xs ys) ⟨ trans ⟩ (ℕ.+-suc (suc (⟦ xs ⇓⟧⁺ ℕ.+ ⟦ ys ⇓⟧⁺)) _ ⟨ trans ⟩
                                cong suc (cong suc (2*-distrib ⟦ xs ⇓⟧⁺ ⟦ ys ⇓⟧⁺))) ⟨ trans ⟩
                                sym (cong suc (ℕ.+-suc (2* ⟦ xs ⇓⟧⁺) _))

  add₁-homo : ∀ xs ys → ⟦ add I xs ys ⇓⟧⁺ ≡ suc (⟦ xs ⇓⟧⁺ ℕ.+ ⟦ ys ⇓⟧⁺)
  add₁-homo 1ᵇ 1ᵇ = refl
  add₁-homo 1ᵇ (O ∷ ys) = cong 2* (inc⁺⁺-homo ys) ⟨ trans ⟩ ℕ.+-suc (suc ⟦ ys ⇓⟧⁺) _
  add₁-homo 1ᵇ (I ∷ ys) = cong suc (cong 2* (inc⁺⁺-homo ys) ⟨ trans ⟩ ℕ.+-suc (suc ⟦ ys ⇓⟧⁺) _)
  add₁-homo (O ∷ xs) 1ᵇ = cong 2* (inc⁺⁺-homo xs) ⟨ trans ⟩ (ℕ.+-suc (suc ⟦ xs ⇓⟧⁺) _ ⟨ trans ⟩ cong suc (ℕ.+-comm 1 _))
  add₁-homo (O ∷ xs) (O ∷ ys) = cong suc (cong 2* (add₀-homo xs ys) ⟨ trans ⟩ 2*-distrib ⟦ xs ⇓⟧⁺ ⟦ ys ⇓⟧⁺)
  add₁-homo (O ∷ xs) (I ∷ ys) = cong 2* (add₁-homo xs ys) ⟨ trans ⟩ (ℕ.+-suc (suc (⟦ xs ⇓⟧⁺ ℕ.+ ⟦ ys ⇓⟧⁺)) _ ⟨ trans ⟩ (cong suc (cong suc ((2*-distrib ⟦ xs ⇓⟧⁺ ⟦ ys ⇓⟧⁺))) ⟨ trans ⟩ cong suc (sym (ℕ.+-suc (2* ⟦ xs ⇓⟧⁺) _)) ))
  add₁-homo (I ∷ xs) 1ᵇ = cong suc (cong 2* (inc⁺⁺-homo xs) ⟨ trans ⟩ cong suc (ℕ.+-suc ⟦ xs ⇓⟧⁺ _ ⟨ trans ⟩ ℕ.+-comm 1 _))
  add₁-homo (I ∷ xs) (O ∷ ys) = cong 2* (add₁-homo xs ys) ⟨ trans ⟩ (ℕ.+-suc (suc (⟦ xs ⇓⟧⁺ ℕ.+ ⟦ ys ⇓⟧⁺)) _ ⟨ trans ⟩ cong suc (cong suc (2*-distrib ⟦ xs ⇓⟧⁺ ⟦ ys ⇓⟧⁺)))
  add₁-homo (I ∷ xs) (I ∷ ys) = cong suc (cong 2* (add₁-homo xs ys) ⟨ trans ⟩ (ℕ.+-suc (suc (⟦ xs ⇓⟧⁺ ℕ.+ ⟦ ys ⇓⟧⁺) ) _ ⟨ trans ⟩ cong suc (cong suc (2*-distrib ⟦ xs ⇓⟧⁺ ⟦ ys ⇓⟧⁺)) ⟨ trans ⟩ cong suc (sym (ℕ.+-suc (2* ⟦ xs ⇓⟧⁺) _)) ))

+-homo : ∀ xs ys → ⟦ xs + ys ⇓⟧ ≡ ⟦ xs ⇓⟧ ℕ.+ ⟦ ys ⇓⟧
+-homo 0ᵇ ys = refl
+-homo (0< x) 0ᵇ = sym (ℕ.+-identityʳ _)
+-homo (0< xs) (0< ys) = add₀-homo xs ys

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
open import Relation.Binary.Core

module BBHeap.Equality.Properties {A : Set}(_≤_ : A → A → Set)  where

open import BBHeap _≤_
open import BBHeap.Equality _≤_
open import Bound.Lower A

refl≈ : {b : Bound}{h : BBHeap b} → h ≈ h
refl≈ {b} {leaf} = ≈leaf
refl≈ {b} {left b≤x l⋘r} = ≈left b≤x b≤x l⋘r l⋘r refl≈ refl≈
refl≈ {b} {right b≤x l⋙r} = ≈right b≤x b≤x l⋙r l⋙r refl≈ refl≈

sym≈ : {b b' : Bound}{h : BBHeap b}{h' : BBHeap b'} → h ≈ h' → h' ≈ h
sym≈ ≈leaf = ≈leaf
sym≈ (≈left b≤x b'≤x' l⋘r l'⋘r' l≈l' r≈r') = ≈left b'≤x' b≤x l'⋘r' l⋘r (sym≈ l≈l') (sym≈ r≈r')
sym≈ (≈right b≤x b'≤x' l⋙r l'⋙r' l≈l' r≈r') = ≈right b'≤x' b≤x l'⋙r' l⋙r (sym≈ l≈l') (sym≈ r≈r')

trans≈ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ≈ h' → h' ≈ h'' → h ≈ h''
trans≈ ≈leaf ≈leaf = ≈leaf
trans≈ (≈left b≤x b'≤x' l⋘r l'⋘r' l≈l' r≈r') (≈left .b'≤x' b''≤x'' .l'⋘r' l''⋘r'' l'≈l'' r'≈r'') = ≈left b≤x b''≤x'' l⋘r l''⋘r'' (trans≈ l≈l' l'≈l'') (trans≈ r≈r' r'≈r'')
trans≈ (≈right b≤x b'≤x' l⋙r l'⋙r' l≈l' r≈r') (≈right .b'≤x' b''≤x'' .l'⋙r' l''⋙r'' l'≈l'' r'≈r'') = ≈right b≤x b''≤x'' l⋙r l''⋙r'' (trans≈ l≈l' l'≈l'') (trans≈ r≈r' r'≈r'')

mutual
  lemma≈≃ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ≈ h' → h' ≃ h'' → h ≃ h''
  lemma≈≃ ≈leaf ≃lf = ≃lf
  lemma≈≃ (≈left b≤x b'≤x' l⋘r l'⋘r' l≈l' r≈r') (≃nd .b'≤x' b''≤x'' .l'⋘r' l''⋘r'' l'≃r' l''≃r'' l'≃l'') = ≃nd b≤x b''≤x'' l⋘r l''⋘r'' (lemma≈≃ l≈l' (lemma≃≈ l'≃r' (sym≈ r≈r'))) l''≃r'' (lemma≈≃ l≈l' l'≃l'')

  lemma≃≈ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ≃ h' → h' ≈ h'' → h ≃ h''
  lemma≃≈ ≃lf ≈leaf = ≃lf
  lemma≃≈ (≃nd b≤x b'≤x' l⋘r l'⋘r' l≃r l'≃r' l≃l') (≈left .b'≤x' b''≤x'' .l'⋘r' l''⋘r'' l'≈l'' r'≈r'') = ≃nd b≤x b''≤x'' l⋘r l''⋘r'' l≃r (lemma≈≃ (sym≈ l'≈l'') (lemma≃≈ l'≃r' r'≈r'')) (lemma≃≈ l≃l' l'≈l'')

lemma≈⋗ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ≈ h' → h' ⋗ h'' → h ⋗ h''
lemma≈⋗ (≈left b≤x .b'≤x' lf⋘ .lf⋘ ≈leaf ≈leaf) (⋗lf b'≤x') = ⋗lf b≤x
lemma≈⋗ (≈left b≤x .b'≤x' l⋘r .l'⋘r' l≈l' r≈r') (⋗nd b'≤x' b''≤x'' l'⋘r' l''⋘r'' l'≃r' l''≃r'' l'⋗l'') = ⋗nd b≤x b''≤x'' l⋘r l''⋘r'' (lemma≈≃ l≈l' (lemma≃≈ l'≃r' (sym≈ r≈r'))) l''≃r'' (lemma≈⋗ l≈l' l'⋗l'')

lemma⋗≈ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ⋗ h' → h' ≈ h'' → h ⋗ h''
lemma⋗≈ (⋗lf b≤x) ≈leaf = ⋗lf b≤x
lemma⋗≈ (⋗nd b≤x b'≤x' l⋘r l'⋘r' l≃r l'≃r' l⋗l') (≈left .b'≤x' b''≤x'' .l'⋘r' l''⋘r'' l'≈l'' r'≈r'') = ⋗nd b≤x b''≤x'' l⋘r l''⋘r'' l≃r (lemma≈≃ (sym≈ l'≈l'') (lemma≃≈ l'≃r' r'≈r'')) (lemma⋗≈ l⋗l' l'≈l'')

lemma≈⋘ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ≈ h' → h' ⋘ h'' → h ⋘ h''
lemma≈⋘ ≈leaf lf⋘ = lf⋘
lemma≈⋘ (≈left b≤x b'≤x' l⋘r l'⋘r' l≈l' r≈r') (ll⋘ .b'≤x' b''≤x'' .l'⋘r' l''⋘r'' l''≃r'' r'≃l'') = ll⋘ b≤x b''≤x'' l⋘r l''⋘r'' l''≃r'' (lemma≈≃ r≈r' r'≃l'')
lemma≈⋘ (≈right b≤x b'≤x' l⋙r l'⋙r' l≈l' r≈r') (lr⋘ .b'≤x' b''≤x'' .l'⋙r' l''⋘r'' l''≃r'' l'⋗l'') = lr⋘ b≤x b''≤x'' l⋙r l''⋘r'' l''≃r'' (lemma≈⋗ l≈l' l'⋗l'')

lemma⋘≈ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ⋘ h' → h' ≈ h'' → h ⋘ h''
lemma⋘≈ lf⋘ ≈leaf = lf⋘
lemma⋘≈ (ll⋘ b≤x b'≤x' l⋘r l'⋘r' l'≃r' r≃l') (≈left .b'≤x' b''≤x'' .l'⋘r' l''⋘r'' l'≈l'' r'≈r'') = ll⋘ b≤x b''≤x'' l⋘r l''⋘r'' (lemma≈≃ (sym≈ l'≈l'') (lemma≃≈ l'≃r' r'≈r'')) (lemma≃≈ r≃l' l'≈l'')
lemma⋘≈ (lr⋘ b≤x b'≤x' l⋙r l'⋘r' l'≃r' l⋗l') (≈left .b'≤x' b''≤x'' .l'⋘r' l''⋘r'' l'≈l'' r'≈r'') = lr⋘ b≤x b''≤x'' l⋙r l''⋘r'' (lemma≈≃ (sym≈ l'≈l'') (lemma≃≈ l'≃r' r'≈r'')) (lemma⋗≈ l⋗l' l'≈l'')

lemma≈⋙ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ≈ h' → h' ⋙ h'' → h ⋙ h''
lemma≈⋙ (≈left b≤x b'≤x' lf⋘ lf⋘ ≈leaf ≈leaf) (⋙lf .b'≤x') = ⋙lf b≤x
lemma≈⋙ (≈left b≤x b'≤x' l⋘r l'⋘r' l≈l' r≈r') (⋙rl .b'≤x' b'≤x'' .l'⋘r' l'≃r' l''⋘r'' l'⋗r'') = ⋙rl b≤x b'≤x'' l⋘r (lemma≈≃ l≈l' (lemma≃≈ l'≃r' (sym≈ r≈r'))) l''⋘r'' (lemma≈⋗ l≈l' l'⋗r'')
lemma≈⋙ (≈left b≤x b'≤x' l⋘r l'⋘r' l≈l' r≈r') (⋙rr .b'≤x' b''≤x'' .l'⋘r' l'≃r' l''⋙r'' l'≃l'') = ⋙rr b≤x b''≤x'' l⋘r (lemma≈≃ l≈l' (lemma≃≈ l'≃r' (sym≈ r≈r'))) l''⋙r'' (lemma≈≃ l≈l' l'≃l'')

lemma⋙≈ : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}{h'' : BBHeap b''} → h ⋙ h' → h' ≈ h'' → h ⋙ h''
lemma⋙≈ (⋙lf b≤x) ≈leaf = ⋙lf b≤x
lemma⋙≈ (⋙rl b≤x b'≤x' l⋘r l≃r l'⋘r' l⋗r') (≈left .b'≤x' b'≤x'' .l'⋘r' l''⋘r'' l'≈l'' r'≈r'') = ⋙rl b≤x b'≤x'' l⋘r l≃r l''⋘r'' (lemma⋗≈ l⋗r' r'≈r'')
lemma⋙≈ (⋙rr b≤x b'≤x' l⋘r l≃r l'⋙r' l≃l') (≈right .b'≤x' b''≤x'' .l'⋙r' l'⋙r'' l'≈l'' r'≈r'') = ⋙rr b≤x b''≤x'' l⋘r l≃r l'⋙r'' (lemma≃≈ l≃l' l'≈l'')

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Base.Types
import      LibraBFT.Yasm.Base  as LYB
import      LibraBFT.Yasm.Types as LYT

-- This module defines a model of a distributed system, parameterized by
-- SystemParameters, which establishes various application-dependent types,
-- handlers, etc.  The model supports a set of peers executing handlers in
-- response to messages received; these handlers can update the peer's
-- local state and/or send additional messages.  The model also enables
-- "cheat" steps, which can send arbitrary messages, except that they are
-- constrained to prevent a cheat step from introducing a new signature for
-- an "honest" public key.  The module also contains some structures for
-- proving properties of executions of the modeled system.

module LibraBFT.Yasm.System
   (ℓ-PeerState : Level)
   (ℓ-VSFP      : Level)
   (parms      : LYB.SystemParameters ℓ-PeerState)
 where

 data InitStatus : Set where
   uninitd : InitStatus
   initd   : InitStatus
 open InitStatus

 uninitd≢initd : uninitd ≢ initd
 uninitd≢initd = λ ()

 open import LibraBFT.Yasm.Base
 open SystemParameters parms
 open import Util.FunctionOverride PeerId _≟PeerId_

 open import LibraBFT.Base.PKCS

 SenderMsgPair : Set
 SenderMsgPair = PeerId × Msg

 actionToSMP : PeerId → LYT.Action Msg → Maybe SenderMsgPair
 actionToSMP pid (LYT.send m) = just (pid , m)

 SentMessages : Set
 SentMessages = List SenderMsgPair

 -- Convert the actions a peer `pid` took to a list of sent messages.
 -- Non-message actions are discarded.
 actionsToSentMessages : PeerId → List (LYT.Action Msg) → SentMessages
 actionsToSentMessages pid = mapMaybe (actionToSMP pid)

 -- If the sender-message pair `(pid₁ , m)` is associated with the messages that
 -- were sent as a consequence of the actions `outs` of `pid₂`, then these two
 -- PIDs are equal and this peer performed a `send` action for that message.
 senderMsgPair∈⇒send∈ : ∀ {pid₁ pid₂ m} → (outs : List (LYT.Action Msg)) →
       (pid₁ , m) ∈ (actionsToSentMessages pid₂ outs) →
       (LYT.send m ∈ outs) × pid₁ ≡ pid₂
 senderMsgPair∈⇒send∈ (LYT.send m ∷ outs) (here refl) = (here refl , refl)
 senderMsgPair∈⇒send∈ (LYT.send m ∷ outs) (there pm∈)
    with senderMsgPair∈⇒send∈ outs pm∈
 ...| m∈outs , refl = (there m∈outs) , refl

 -- The model supports sending messages that contain some fields that are
 -- /not/ covered by the message's signature.  Therefore, given a message
 -- with a verifiable signature, it is possible for a propositionally
 -- different message that verifies against the same signature to have been
 -- sent before, which is captured by the following definition.
 record MsgWithSig∈ (pk : PK)(sig : Signature)(pool : SentMessages) : Set where
   constructor mkMsgWithSig∈
   field
     msgWhole   : Msg
     msgPart    : Part
     msg⊆       : msgPart ⊂Msg msgWhole
     msgSender  : PeerId
     msg∈pool   : (msgSender , msgWhole) ∈ pool
     msgSigned  : WithVerSig pk msgPart
     msgSameSig : ver-signature msgSigned ≡ sig
 open MsgWithSig∈ public

 postulate  -- TODO-1: prove it
   MsgWithSig∈? : ∀ {pk} {sig} {pool} → Dec (MsgWithSig∈ pk sig pool)

 MsgWithSig∈-++ʳ : ∀{pk sig pool ms} → MsgWithSig∈ pk sig pool → MsgWithSig∈ pk sig (ms ++ pool)
 MsgWithSig∈-++ʳ {ms = pre} msig = record
    { msgWhole   = msgWhole msig
    ; msgPart    = msgPart  msig
    ; msg⊆       = msg⊆     msig
    ; msg∈pool   = Any-++ʳ pre (msg∈pool msig)
    ; msgSigned  = msgSigned msig
    ; msgSameSig = msgSameSig msig
    }

 MsgWithSig∈-++ˡ : ∀{pk sig pool ms} → MsgWithSig∈ pk sig ms → MsgWithSig∈ pk sig (ms ++ pool)
 MsgWithSig∈-++ˡ {ms = pre} msig = record
    { msgWhole   = msgWhole msig
    ; msgPart    = msgPart  msig
    ; msg⊆       = msg⊆     msig
    ; msg∈pool   = Any-++ˡ (msg∈pool msig)
    ; msgSigned  = msgSigned msig
    ; msgSameSig = msgSameSig msig
    }

 MsgWithSig∈-transp : ∀{pk sig pool pool'}
                    → (mws : MsgWithSig∈ pk sig pool)
                    → (msgSender mws , msgWhole mws) ∈ pool'
                    → MsgWithSig∈ pk sig pool'
 MsgWithSig∈-transp msig ∈pool' = record
    { msgWhole   = msgWhole msig
    ; msgPart    = msgPart  msig
    ; msg⊆       = msg⊆     msig
    ; msg∈pool   = ∈pool'
    ; msgSigned  = msgSigned msig
    ; msgSameSig = msgSameSig msig
    }

 -- * Forbidding the Forging of Signatures
 --
 -- Whenever our reasoning must involve digital signatures, it is standard
 -- to talk about EUF-CMA resistant signature schemes. Informally, this captures
 -- signatures schemes that cannot be compromised by certain adversaries.
 -- Formally, it means that for any probabilistic-polynomial-time adversary 𝓐,
 -- and some security parameter k:
 --
 --      Pr[ EUF-CMA(k) ] ≤ ε(k) for ε a negigible function.
 --
 -- EUF-CMA is defined as:
 --
 -- EUF-CMA(k):                           |  O(m):
 --   L        ← ∅                        |    σ ← Sign(sk , m)
 --   (pk, sk) ← Gen(k)                   |    L ← L ∪ { m }
 --   (m , σ)  ← 𝓐ᴼ(pk)                   |    return σ
 --   return (Verify(pk, m, σ) ∧ m ∉ L)   |
 --
 -- This says that 𝓐 cannot create a message that has /not yet been signed/ and
 -- forge a signature for it. The list 'L' keeps track of the messages that 𝓐
 -- asked to be signed by the oracle.
 --
 -- Because the probability of the adversary to win the EUF-CMA(k) game
 -- approaches 0 as k increases; it is reasonable to assume that winning
 -- the game is /impossible/ for realistic security parameters.
 --
 -- EUF-CMA security is incorporated into our model by constraining messages
 -- sent by a cheat step to ensure that for every verifiably signed part of
 -- such a message, if there is a signature on the part, then it is either for
 -- a dishonest public key (in which cases it's secret key may have been leaked),
 -- or a message has been sent with the same signature before (in which case the
 -- signature is simply being "replayed" from a previous message).
 --
 -- Dishonest (or "cheat") messages are those that are not the result of
 -- a /handle/ or /init/ call, but rather are the result of a /cheat/ step.
 --
 -- A part of a cheat message can contain a verifiable signature only if it
 -- is for a dishonest public key, or a message with the same signature has
 -- been sent before or can be derived from GenesisInfo (a cheater can
 -- "reuse" an honest signature sent before; it just can't produce a new
 -- one).  Note that this constraint precludes a peer sending a message
 -- that contains a new verifiable signature for an honest PK, even if the
 -- PK is the peer's own PK for some epoch (implying that the peer
 -- possesses the associated secret key).  In other words, a peer that is
 -- honest for a given epoch (by virtue of being a member of that epoch and
 -- being assigned an honest PK for the epoch), cannot send a message for
 -- that epoch using a cheat step.
 CheatPartConstraint : SentMessages → Part → Set
 CheatPartConstraint pool m = ∀{pk} → (ver : WithVerSig pk m)
                                    → ¬ ∈GenInfo (ver-signature ver)
                                    → Meta-Dishonest-PK pk
                                    ⊎ MsgWithSig∈ pk (ver-signature ver) pool

 -- The only constraints on messages sent by cheat steps are that:
 -- * the sender is not an honest member in the epoch of any part of the message
 -- * the signature on any part of the message satisfies CheatCanSign, meaning
 --   that it is not a new signature for an honest public key
 CheatMsgConstraint : SentMessages → Msg → Set
 CheatMsgConstraint pool m = ∀{part} → part ⊂Msg m → CheatPartConstraint pool part

 -- * The System State
 --
 -- A system consists in a partial map from PeerId to PeerState, a pool
 -- of sent messages and a number of available epochs.
 record SystemState : Set (ℓ+1 ℓ-PeerState) where
   field
     peerStates  : PeerId → PeerState
     initialised : PeerId → InitStatus
     msgPool     : SentMessages          -- All messages ever sent
 open SystemState public

 initialState : SystemState
 initialState = record
   { peerStates  = const initPS
   ; initialised = const uninitd
   ; msgPool     = []
   }

 -- * Small Step Semantics
 --
 -- The small step semantics are divided into three datatypes:
 --
 -- i)   StepPeerState executes a step through init or handle
 -- ii)  StepPeer executes a step through StepPeerState or cheat
 -- iii) Step transitions the system state by a StepPeer or by
 --      bringing a new epoch into existence

 -- The pre and post states of Honest peers are related iff
 data StepPeerState (pid : PeerId)(pool : SentMessages)
                    (peerInits : PeerId → InitStatus) (ps : PeerState) :
                    (PeerState × List (LYT.Action Msg)) → Set where
   -- An uninitialized peer can be initialized
   step-init : peerInits pid ≡ uninitd
             → StepPeerState pid pool peerInits ps (init pid genInfo)

   -- The peer processes a message in the pool
   step-msg  : ∀{m}
             → m ∈ pool
             → peerInits pid ≡ initd
             → StepPeerState pid pool peerInits ps (handle pid (proj₂ m) ps)

 -- The pre-state of the suplied PeerId is related to the post-state and list of output messages iff:
 data StepPeer (pre : SystemState) : PeerId → PeerState → List (LYT.Action Msg) → Set ℓ-PeerState where
   -- it can be obtained by a handle or init call.
   step-honest : ∀{pid st outs}
               → StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (st , outs)
               → StepPeer pre pid st outs

   -- or the peer decides to cheat.  CheatMsgConstraint ensures it cannot
   -- forge signatures by honest peers.  Cheat steps do not modify peer
   -- state: these are maintained exclusively by the implementation
   -- handlers.
   step-cheat  : ∀{pid m}
               → CheatMsgConstraint (msgPool pre) m
               → StepPeer pre pid (peerStates pre pid) (LYT.send m ∷ [])

 isCheat : ∀ {pre pid ms outs} → StepPeer pre pid ms outs → Set
 isCheat (step-honest _) = ⊥
 isCheat (step-cheat  _) = Unit

 initStatus : ∀ {pid pre ms outs}
            → StepPeer pre pid ms outs
            → InitStatus
            → InitStatus
 initStatus {pid} (step-honest _) preinit = initd
 initStatus {pid} (step-cheat  _) preinit = preinit

 -- Computes the post-sysstate for a given step-peer.
 StepPeer-post : ∀{pid st' outs}{pre : SystemState }
               → StepPeer pre pid st' outs → SystemState
 StepPeer-post {pid} {st'} {outs} {pre} sp = record pre
   { peerStates  = ⟦ peerStates pre  , pid ← st' ⟧
   ; initialised = ⟦ initialised pre , pid ← initStatus sp (initialised pre pid) ⟧
   ; msgPool     = actionsToSentMessages pid outs ++ msgPool pre
   }

 StepPeer-post-lemma : ∀{pid st' outs}{pre : SystemState}
               → (pstep : StepPeer pre pid st' outs)
               → st' ≡ peerStates (StepPeer-post pstep) pid
 StepPeer-post-lemma pstep = sym override-target-≡

 StepPeer-post-lemma2 : ∀{pid}{pre : SystemState}{st outs}
                      → (sps : StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (st , outs))
                      → initialised (StepPeer-post {pid} {st} {outs} {pre} (step-honest sps)) pid ≡ initd
 StepPeer-post-lemma2 {pre = pre} _ = override-target-≡

 cheatStepDNMPeerStates : ∀{pid st' outs}{pre : SystemState}
                        → (theStep : StepPeer pre pid st' outs)
                        → isCheat theStep
                        → peerStates (StepPeer-post theStep) ≡ peerStates pre
 cheatStepDNMPeerStates {pid = pid} {pre = pre} (step-cheat _) _ = overrideSameVal-correct-ext {f = peerStates pre} {pid}

 cheatStepDNMInitialised : ∀{pid st' outs}{pre : SystemState}
                        → (theStep : StepPeer pre pid st' outs)
                        → isCheat theStep
                        → initialised (StepPeer-post theStep) ≡ initialised pre
 cheatStepDNMInitialised {pid = pid} {pre = pre} (step-cheat _) _ = overrideSameVal-correct-ext

 cheatStepDNMInitialised₁ : ∀{pid pid' st' outs}{pre : SystemState}
                        → (theStep : StepPeer pre pid st' outs)
                        → isCheat theStep
                        → initialised (StepPeer-post theStep) pid' ≡ initialised pre pid'
 cheatStepDNMInitialised₁ {pid} {pid'} {pre = pre} (step-cheat _) _ = overrideSameVal-correct pid pid'

 cheatStepDNMPeerStates₁ : ∀{pid pid' st' outs}{pre : SystemState}
                         → (theStep : StepPeer pre pid st' outs)
                         → isCheat theStep
                         → peerStates (StepPeer-post theStep) pid' ≡ peerStates pre pid'
 cheatStepDNMPeerStates₁ {pid} {pid'} (step-cheat _) x = overrideSameVal-correct pid pid'

 pids≢StepDNMPeerStates :  ∀{pid pid' s' outs}{pre : SystemState}
                         → (sps : StepPeerState pid' (msgPool pre) (initialised pre) (peerStates pre pid') (s' , outs))
                         → pid ≢ pid'
                         → peerStates pre pid ≡ peerStates (StepPeer-post {pid'} {s'} {outs} {pre} (step-honest sps)) pid
 pids≢StepDNMPeerStates sps pids≢ = override-target-≢ pids≢

 data Step : SystemState → SystemState → Set (ℓ+1 ℓ-PeerState) where
   -- TO-NOT-DO: it is tempting to merge this and StepPeer, now that step-peer
   -- is the only constructor here.  I started to do so, but it propagates many
   -- changes throughout the repo, and it's possible we will in future add steps
   -- not performed by a specific peer (for example, if we model some notion of
   -- time to prove liveness properties).
   step-peer : ∀{pid st' outs}{pre : SystemState}
             → (pstep : StepPeer pre pid st' outs)
             → Step pre (StepPeer-post pstep)

 msgs-stable : ∀ {pre : SystemState} {post : SystemState} {m}
             → (theStep : Step pre post)
             → m ∈ msgPool pre
             → m ∈ msgPool post
 msgs-stable (step-peer {pid = pid} {outs = outs} _) m∈ = Any-++ʳ (actionsToSentMessages pid outs) m∈

 peersRemainInitialized : ∀ {pid} {pre : SystemState} {post : SystemState}
                        → Step pre post
                        → initialised pre pid ≡ initd
                        → initialised post pid ≡ initd
 peersRemainInitialized {pid} (step-peer {pid'} step) isInitd
   with pid' ≟PeerId pid
 ...| no neq = isInitd
 ...| yes refl
   with step
 ... | step-honest {pidS} {st} {outs} stp = refl
 ... | step-cheat _ = isInitd

 -- not used yet, but some proofs could probably be cleaned up using this,
 -- e.g., prevVoteRnd≤-pred-step in Impl.VotesOnce
 sendMessages-target : ∀ {m : SenderMsgPair} {sm : SentMessages} {ml : List SenderMsgPair}
                     → ¬ (m ∈ sm)
                     → m ∈ (ml ++ sm)
                     → m ∈ ml
 sendMessages-target {ml = ml} ¬m∈sm m∈++
   with Any-++⁻ ml m∈++
 ...| inj₁ m∈ml = m∈ml
 ...| inj₂ m∈sm = ⊥-elim (¬m∈sm m∈sm)

 -- * Reflexive-Transitive Closure

 data Step* : SystemState → SystemState → Set (ℓ+1 ℓ-PeerState) where
   step-0 : ∀{pre : SystemState}
          → Step* pre pre

   step-s : ∀{fst : SystemState}{pre : SystemState}{post : SystemState}
          → Step* fst pre
          → Step pre post
          → Step* fst post

 ReachableSystemState : SystemState → Set (ℓ+1 ℓ-PeerState)
 ReachableSystemState = Step* initialState

 peerStatePostSt : ∀ {pid s' s outs} {st : SystemState}
                 → (r : ReachableSystemState st)
                 → (stP : StepPeerState pid (msgPool st) (initialised st)
                                        (peerStates st pid) (s' , outs))
                 → peerStates (StepPeer-post {pre = st} (step-honest stP)) pid ≡ s
                 → s ≡ s'
 peerStatePostSt _ _ ps≡s = trans (sym ps≡s) override-target-≡

 Step*-trans : ∀ {st st' st''}
             → Step* st st'
             → Step* st' st''
             → Step* st st''
 Step*-trans r step-0 = r
 Step*-trans r (step-s tr x) = step-s (Step*-trans r tr) x

 Step*-initdStable : ∀{st st' pid}
                   → Step* st st'
                   → initialised st  pid ≡ initd
                   → initialised st' pid ≡ initd
 Step*-initdStable step-0 ini = ini
 Step*-initdStable {st} {pid = pid} (step-s {pre = pre} tr theStep) ini =
                   peersRemainInitialized theStep (Step*-initdStable tr ini)

 MsgWithSig∈-Step* : ∀{sig pk}{st : SystemState}{st' : SystemState}
                   → Step* st st'
                   → MsgWithSig∈ pk sig (msgPool st)
                   → MsgWithSig∈ pk sig (msgPool st')
 MsgWithSig∈-Step* step-0        msig = msig
 MsgWithSig∈-Step* (step-s tr (step-peer ps)) msig
   = MsgWithSig∈-++ʳ (MsgWithSig∈-Step* tr msig)

 MsgWithSig∈-Step*-part : ∀{sig pk}{st : SystemState}{st' : SystemState}
                        → (tr   : Step* st st')
                        → (msig : MsgWithSig∈ pk sig (msgPool st))
                        → msgPart msig ≡ msgPart (MsgWithSig∈-Step* tr msig)
 MsgWithSig∈-Step*-part step-0        msig = refl
 MsgWithSig∈-Step*-part (step-s tr (step-peer ps)) msig
   = MsgWithSig∈-Step*-part tr msig

 MsgWithSig∈-Step*-sender : ∀{sig pk}{st : SystemState}{st' : SystemState}
                          → (tr   : Step* st st')
                          → (msig : MsgWithSig∈ pk sig (msgPool st))
                          → msgSender msig ≡ msgSender (MsgWithSig∈-Step* tr msig)
 MsgWithSig∈-Step*-sender step-0        msig = refl
 MsgWithSig∈-Step*-sender (step-s tr (step-peer ps)) msig
   = MsgWithSig∈-Step*-sender tr msig

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

 -- Type synonym to express a relation over system states;
 SystemStateRel : ∀ {ℓ} → (SystemState → SystemState → Set (ℓ+1 ℓ-PeerState)) → Set (ℓ+1 (ℓ ℓ⊔ ℓ-PeerState))
 SystemStateRel {ℓ} P = ∀{st : SystemState}{st' : SystemState} → P st st' → Set (ℓ ℓ⊔ ℓ-PeerState)

 -- Just like Data.List.Any maps a predicate over elements to a predicate over lists,
 -- Any-step maps a relation over steps to a relation over steps in a trace.
 data Any-Step {ℓ : Level} (P : SystemStateRel {ℓ} Step) : SystemStateRel {ℓ} Step* where
  step-here  : ∀{fst : SystemState}{pre : SystemState}{post : SystemState}
             → (cont : Step* fst pre)
             → {this : Step pre post}(prf  : P this)
             → Any-Step P (step-s cont this)

  step-there : ∀{fst : SystemState}{pre : SystemState}{post : SystemState}
             → {cont : Step* fst pre}
             → {this : Step pre post}
             → (prf  : Any-Step {ℓ} P cont)
             → Any-Step P (step-s cont this)

 Any-Step-map : ∀ {ℓ}{P P' : SystemStateRel {ℓ} Step}
              → (∀ {pre : SystemState}{post : SystemState} → (x : Step pre post) → P x → P' x)
              → ∀ {fst lst} {tr : Step* fst lst}
              → Any-Step {ℓ} P tr
              → Any-Step {ℓ} P' tr
 Any-Step-map p⇒p' (step-here cont {this} prf) = step-here cont (p⇒p' this prf)
 Any-Step-map p⇒p' (step-there anyStep) = step-there (Any-Step-map p⇒p' anyStep)

 Any-Step-elim
   : ∀{ℓ}{ℓ-Q}{st₀ : SystemState}{st₁ : SystemState}{P : SystemStateRel {ℓ} Step}{Q : Set ℓ-Q}
   → {r : Step* st₀ st₁}
   → (P⇒Q : ∀{s : SystemState}{s' : SystemState}{st : Step s s'}
          → P st → Step* s' st₁ → Q)
   → Any-Step {ℓ} P r → Q
 Any-Step-elim P⇒Q (step-here cont prf)
   = P⇒Q prf step-0
 Any-Step-elim P⇒Q (step-there {this = this} f)
   = Any-Step-elim (λ p s → P⇒Q p (step-s s this)) f

 -- A predicate over peer states, parts and peerIds, representing which peers can send new
 -- signatures for which PKs.  The PeerState is needed to provide access to information the peer has
 -- about who uses what keys for what parts (in our case, EpochConfigs either derived from genesis
 -- information or agreed during epoch changes).
 ValidSenderForPK-type : Set (ℓ+1 ℓ-VSFP ℓ⊔ ℓ+1 ℓ-PeerState)
 ValidSenderForPK-type = SystemState → Part → PeerId → PK → Set ℓ-VSFP

 ValidSenderForPK-stable-type : ValidSenderForPK-type → Set (ℓ-VSFP ℓ⊔ ℓ+1 ℓ-PeerState)
 ValidSenderForPK-stable-type vs4pk = ∀ {pre post part pid pk}
                                      → ReachableSystemState pre
                                      → Step pre post
                                      → vs4pk pre  part pid pk
                                      → vs4pk post part pid pk

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

 module _ (P : SystemState → Set) where

   Step*-Step-fold : (∀{pid st' outs}{st : SystemState}
                        → ReachableSystemState st
                        → (pstep : StepPeer st pid st' outs)
                        → P st
                        → P (StepPeer-post pstep))
                   → P initialState
                   → ∀{st : SystemState}
                   → (tr : ReachableSystemState st) → P st
   Step*-Step-fold fs p₀ step-0 = p₀
   Step*-Step-fold fs p₀ (step-s tr (step-peer p)) = fs tr p (Step*-Step-fold fs p₀ tr)

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
{-# OPTIONS --rewriting  #-}
open import Array
open import Array.APL using (reduce-1d)

open import Data.Nat as N
open import Data.Nat.Properties
open import Data.Vec as V hiding (_>>=_; _++_)
open import Data.Fin using (Fin; zero; suc; raise; inject+; #_)
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Function

open import Relation.Nullary
open import Relation.Nullary.Decidable

sum-1d : ∀ {n} → Ar ℕ 1 (n ∷ []) → ℕ
sum-1d v = reduce-1d v _+_ 0

zipw : ∀ {a}{X : Set a}{d s} → (X → X → X) → Ar X d s → Ar X d s → Ar X d s
zipw _⊕_ (imap a) (imap b) = imap λ iv → a iv ⊕ b iv

hd : ∀ {n s : ℕ}{ss : Vec ℕ n} → Ix (suc n) (s ∷ ss) → Fin s
hd ix = ix-lookup ix zero

vec-mat-mul : ∀ {n m} → Ar ℕ 2 (m ∷ n ∷ []) → Ar ℕ 1 (n ∷ []) → Ar ℕ 1 (m ∷ [])
vec-mat-mul (imap a) b = imap λ iv → sum-1d (zipw _*_ (imap λ jv → a (iv ix++ jv)) b)

twice : ∀ {n} → (M : Ar ℕ 2 (n ∷ n ∷ [])) → (V : Ar ℕ 1 (n ∷ [])) → Ar ℕ 1 (n ∷ [])
twice m v = vec-mat-mul m (vec-mat-mul m v)

sum-2d : ∀ {m n} → Ar ℕ 2 (m ∷ n ∷ []) → ℕ
sum-2d (imap a) = sum-1d (imap λ i → sum-1d (imap λ j → a $ i ix++ j))

_+'_ : ∀ {m n} → Fin (1 + m) → Fin (1 + n) → Fin (1 + m + n)
_+'_ {m} {n} zero j = subst Fin (+-suc m n) (raise m j)
_+'_ {suc m} {n} (suc i) j = suc (i +' j)

_+''_ : ∀ {m n} → Fin m → Fin n → Fin (m + n ∸ 1)
_+''_ {suc m} {suc n} zero j = raise m j
_+''_ {suc (suc m)} {suc n} (suc i) j = suc (i +'' j)

_ix+2_ : ∀ {m n k p} → Ix 2 (m ∷ n ∷ []) → Ix 2 (k ∷ p ∷ []) → Ix 2 (m + k ∸ 1 ∷ n + p ∸ 1 ∷ [])
(x₁ ∷ x₂ ∷ []) ix+2 (y₁ ∷ y₂ ∷ []) = x₁ +'' y₁ ∷ (x₂ +'' y₂) ∷ []

conv-2 : ∀ {m n k p} → Ar ℕ 2 (m + k ∷ n + p ∷ []) → Ar ℕ 2 (k ∷ p ∷ []) → Ar ℕ 2 (1 + m ∷ 1 + n ∷ [])
conv-2 {k = k} {p} (imap a) (imap w) = imap (λ iv → sum-2d {m = k} {n = p} (imap λ ov → w ov * a (iv ix+2 ov)))

iterate-1 : ∀ {a}{X : Set a}{n} → (Fin n → X) → (X → X → X) → X → X
iterate-1 {n = zero}  f _⊕_ neut = neut
iterate-1 {n = suc n} f _⊕_ neut = f zero ⊕ iterate-1 (f ∘ suc) _⊕_ neut

red-iter : ∀ {a}{X : Set a}{n} → (f : Ix 1 (n ∷ []) → X) → (op : X → X → X) → (neut : X)
         → reduce-1d (imap f) op neut ≡ iterate-1 (λ i → f (i ∷ [])) op neut
red-iter {n = zero}  f op neut = refl
red-iter {n = suc n} f op neut = cong (λ x → op _ x) (red-iter (λ iv → f (suc (hd iv) ∷ [])) op neut)

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE red-iter    #-}

thm : ∀ {n} → (m : Ar ℕ 2 (n ∷ n ∷ []))
    → (v : Ar _ _ (n ∷ []))
    → ∀ iv → unimap (twice m v) iv ≡ {!!}
thm (imap m) (imap v) (i ∷ []) = {!!}

{-
-- Reflection business
open import Reflection
open import Data.List hiding (_++_)
open import Data.Bool
open import Data.Maybe hiding (_>>=_)
open import Data.Unit

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

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

--reflectTerm : TC Term
--reflectTerm = (getType (quote f)) >>= λ ty → quoteTC f >>= derefImmediate >>= λ x → checkType x ty

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

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

r : Term
r = reflect twice

open import Data.String
open import Data.Nat.Show as Ns
open import Data.List as L using (List)

data Prog : Set where
  ok : String → Prog
  error : String → Prog

record State : Set where
  inductive
  constructor st
  field
   vars : List String
   defs : List $ String × String
   cons : List (String × ((List $ Arg Term) → Prog))

var-lkup : State → ℕ → Prog
var-lkup s n = hlpr (State.vars s) n
  where hlpr : _ → _ → _
        hlpr [] n = error $ "Variable not found"
        hlpr (x ∷ l) zero = ok x
        hlpr (x ∷ l) (suc n) = hlpr l n

def-lkup : State → String → Prog
def-lkup ss s = hlpr (State.defs ss) s
  where hlpr : _ → _ → _
        hlpr [] s = error $ "Definition `" ++ s ++ "' not found"
        hlpr ((k , v) ∷ dfs) s with k ≈? s
        ... | yes p = ok v
        ... | no ¬p = hlpr dfs s

cons-cont : State → String → List (Arg Term) → Prog
cons-cont ss s args = {!!} {-hlpr (State.cons ss) s args
  where hlpr : _ → _ → _ → _
        hlpr [] s _ = error $ "Constructor `" ++ s ++ "' not found"
        hlpr ((k , f) ∷ cs) s args with k ≈? s
        ... | yes p = f args
        ... | no ¬p = hlpr cs s args
-}
infixl 5 _#_
_#_ : Prog → Prog → Prog
ok x # ok y = ok $ x ++ y
error x # _ = error x
_ # error y = error y

l→s : List String → String
l→s [] = ""
l→s (x ∷ l) = x ++ " " ++ l→s l

comp-arglist-mask : State → List (Arg Term) → List Bool → Prog

comp-arglist : State → List (Arg Term) → Prog
comp-clauses : State → List Clause → Prog

_at_ : ∀ {a}{X : Set a} → List X → ℕ → Maybe X
[] at idx = nothing
(x ∷ a) at zero = just x
(x ∷ a) at suc idx = a at idx

unmaybe : ∀ {a}{X : Set a} → List (Maybe X) → Maybe (List X)
unmaybe [] = just []
unmaybe (nothing ∷ xs) = nothing
unmaybe (just x ∷ xs) with unmaybe xs
unmaybe (just x ∷ xs) | nothing = nothing
unmaybe (just x ∷ xs) | just xs' = just $ x ∷ xs'

filter-idx : ∀ {a}{X : Set a} → List X → List ℕ → Maybe (List X)
filter-idx xs idxs = unmaybe $ L.map (xs at_) idxs

_!!_ : ∀ {a}{X : Set a} → (xs : List X) → Fin (L.length xs) → X
[] !! ()
(x ∷ xs) !! zero = x
(x ∷ xs) !! suc i = xs !! i

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

compile : State → Term → Prog
compile s (var x args) = ok "V(" # var-lkup s x # ok " " # comp-arglist s args # ok ")"
compile s (con c args) with (showName c)
compile s (con c args) | "Data.Vec.Base.Vec.[]" = ok "nil"
compile s (con c args) | "Array.Base.Ix.[]" = ok "nil"
compile s (con c args) | "Data.Vec.Base.Vec._∷_" =
   ok "(cons " # comp-arglist-mask s args (mk-mask 5 $ # 3 ∷ # 4 ∷ []) # ok ")"
compile s (con c args) | "Array.Base.Ix._∷_" =
   ok "(cons " # comp-arglist-mask s args (mk-mask 5 $ # 3 ∷ # 4 ∷ []) # ok ")"
compile s (con c args) | _ = ok ("C(" ++ showName c ++ " ") # comp-arglist s args # ok ")"

compile s (def f args) with def-lkup s $ showName f
... | error _ = ok "D(" # ok (showName f) # ok " " # comp-arglist s args
... | d       = ok "D(" # d # ok " "
                        # comp-arglist s args # ok ")"

compile s (lam v (abs w x)) = ok ("(\\ " ++ w ++ " -> ") # compile (record s {vars = (w ∷ State.vars s)}) x # ok ")"
compile s (pat-lam cs []) = ok "PAT-LAM (cl = " # comp-clauses s cs # ok ")" --(args = " # comp-arglist s args # ok ")"
compile s (pat-lam cs _) = error "PAT-LAM: I don't know what args to pat-lam are"
compile s (pi a b) = ok "PI TYPE"
compile s (sort _) = ok "SORT"
compile s (lit x) = ok $ showLiteral x
compile s (meta x x₁) = ok "META"
compile s unknown = ok "_" -- "UNKNOWN"

comp-arglist s [] = ok ""
comp-arglist s (arg i x ∷ l) = compile s x # ok " " # comp-arglist s l

comp-arglist-mask s [] [] = ok ""
comp-arglist-mask s [] (x ∷ mask) = error "Incorrect argument mask"
comp-arglist-mask s (x ∷ args) [] = error "Incorrect argument mask"
comp-arglist-mask s (x ∷ args) (false ∷ mask) = comp-arglist-mask s args mask
comp-arglist-mask s (arg i x ∷ args) (true ∷ mask) = compile s x # ok "  " # comp-arglist-mask s args mask

comp-pats : List (Arg Pattern) → List String
comp-pats [] = []
comp-pats (vArg (var x) ∷ l) = x ∷ comp-pats l
comp-pats (vArg _ ∷ l) = "_" ∷ comp-pats l
comp-pats (_ ∷ l) = "_" ∷ comp-pats l

comp-clauses s [] = ok ""
comp-clauses s (clause ps t ∷ cs) = let
   vars = comp-pats ps
   in ok ("pats = " ++ l→s vars) # compile (record s {vars = (L.reverse vars L.++ State.vars s)}) t
comp-clauses s (absurd-clause ps ∷ cs) = error "absurd clause found"

test : ∀ {n} (m : Ix 2 (n ∷ n ∷ []) → ℕ) (v : Ix 1 (n ∷ []) → ℕ)
         (i : Fin n) → ℕ
test m v i = iterate-1
       (λ i₁ →
          m (i ∷ i₁ ∷ []) *
          iterate-1 (λ i₂ → m (i₁ ∷ i₂ ∷ []) * v (i₂ ∷ [])) _+_ 0)
       _+_ 0

bltin-defs : List $ String × String
bltin-defs = ("Agda.Builtin.Nat.Nat" , "nat")
           ∷ ("Agda.Builtin.Nat._+_" , "plus")
           ∷ ("Agda.Builtin.Nat._*_" , "mult")
           ∷ ("Agda.Primitive.lzero" , "tt")
           ∷ ("BLAS.iterate-1" , "for-loop-acc")
           ∷ []

bltin-cons : List (String × (List (Arg Term) → Prog))
bltin-cons = ("Data.Vec.Base.Vec.[]" , λ _ → ok "nil")
           ∷ ("Array.Base.Ix.[]" , λ _ → ok "nil")
           ∷ ("Array.Base.Ix._∷_" , λ args → {!!})
           ∷ []

ct = compile (st [] bltin-defs []) (reflect test)

foo : ∀ {n : ℕ} (a b : ℕ) → ℕ
foo x = _+ x

cr = compile (st [] bltin-defs []) (reflect foo)

cconv = compile (st [] bltin-defs []) (reflect conv-2)

-}

--t : Term
--t = reflect-ty (thm)

-- PAT-LAM (cl = pats = _ m v i D(BLAS.iterate-1 D(Agda.Primitive.lzero ) D(Agda.Builtin.Nat.Nat ) V(i )
--         (\\ i₁ -> D(Agda.Builtin.Nat._*_
--                        V(v C(Array.Base.Ix._∷_ 1 C(Data.Vec.Base.Vec._∷_ UNKNOWN UNKNOWN 0 V(i ) C(Data.Vec.Base.Vec.[] UNKNOWN UNKNOWN ) )
--                                                  V(i )
--                                                  V(_ )
--                                                  C(Array.Base.Ix._∷_ 0 C(Data.Vec.Base.Vec.[] UNKNOWN UNKNOWN ) V(i ) V(i₁ ) C(Array.Base.Ix.[] ) ) ) )
--                        D(BLAS.iterate-1 D(Agda.Primitive.lzero ) D(Agda.Builtin.Nat.Nat ) V(i )
--                         (\\ i₂ -> D(Agda.Builtin.Nat._*_
--                                     V(v C(Array.Base.Ix._∷_ 1 C(Data.Vec.Base.Vec._∷_ UNKNOWN UNKNOWN 0 V(i ) C(Data.Vec.Base.Vec.[] UNKNOWN UNKNOWN ) )
--                                                               V(i )
--                                                               V(i₁ )
--                                                               C(Array.Base.Ix._∷_ 0 C(Data.Vec.Base.Vec.[] UNKNOWN UNKNOWN )
--                                                                                V(i ) V(i₂ ) C(Array.Base.Ix.[] ) ) ) )
--                                     V(m C(Array.Base.Ix._∷_ 0 C(Data.Vec.Base.Vec.[] UNKNOWN UNKNOWN ) V(i ) V(i₂ ) C(Array.Base.Ix.[] ) ) ) ))
--                         D(Agda.Builtin.Nat._+_ ) 0 ) ))
--         D(Agda.Builtin.Nat._+_ ) 0 )) (args = )

--compld _ m v i = D(for-loop-acc D(tt ) D(nat ) V(_ )
--                               (\\ i₁ -> D(mult V(m (cons V(i )  (cons V(i₁ )  nil  )  ) )
--                                                D(for-loop-acc D(tt ) D(nat ) V(_ )
--                                                              (\\ i₂ -> D(mult V(m (cons V(i₁ )  (cons V(i₂ )  nil  )  ) )
--                                                                               V(v (cons V(i₂ )  nil  ) ) ))
--                                                                               D(plus ) 0 ) ))
--                               D(plus ) 0 )

-- A * v = { i → Σ Aᵢ×v }
-- A * A * v = { i → Σ Aᵢ×v }

max_stars_repo_name: ashinkarov/agda-array

max_issues_repo_name: ashinkarov/agda-array

max_forks_repo_name: ashinkarov/agda-array


text:
-- Compiled things must be a postulate

module CompiledMustBePostulate where

postulate
  A : Set

foo : Set
foo = A

{-# COMPILED foo bar #-}

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module equalities where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Data.Equality

module _ {a ℓ} {A : Set a} where
  ≣-Type = A → A → Set ℓ

  record IsEquality (_≣_ : ≣-Type) : Set (ℓ-suc (ℓ-max a ℓ)) where
    constructor eq
    field
      ≣-≡-≡ : ∀ {x y} → let
        ℓ₁ = ℓ-max a ℓ

        x≡y : Type ℓ₁
        x≡y = x ≡ y

        x≣y : Type ℓ₁
        x≣y = x ≣ y

        in _≡_ {ℓ-suc ℓ₁} x≣y x≡y

  record Equality : Set (ℓ-suc (ℓ-max a ℓ)) where
    field
      _≣_ : ≣-Type
      isEquality : IsEquality _≣_

module _ {a} {A : Set a} where
  instance
    ≡-IsEquality : IsEquality {A = A} _≡_
    ≡-IsEquality = eq refl

  instance
    ≡p-IsEquality : IsEquality {A = A} _≡p_
    ≡p-IsEquality = eq (λ {x y} → sym λ i → p-c {x = x} {y = y} i)

module _ {ℓ} where
  univalencePath' : {A B : Type ℓ} → (A ≡ B) ≡ (A ≃ B)
  univalencePath' {A} {B} =
    ua {ℓ-suc ℓ} {A ≡ B} {A ≃ B} (compEquiv (univalence {ℓ} {A} {B})
    (isoToEquiv (iso {ℓ} {ℓ-suc ℓ} (λ x → x) (λ x → x) (λ b i → b) λ a i → a)))

  instance
    ≃-IsEquality : IsEquality {A = Type ℓ} (λ A B → (A ≃ B))
    ≃-IsEquality = eq λ {A B} → sym λ i → univalencePath' {A = A} {B = B} i

max_stars_repo_name: guilhermehas/Equality

max_issues_repo_name: guilhermehas/Equality

max_forks_repo_name: guilhermehas/Equality


text:
import Issue4267.M using ()

-- foo : {!Issue4267.M.R!} -- cannot give, but this is the solution
foo = record { f = Set}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Instances.Int where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Int renaming (ℤ to ℤType ; _+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
open import Cubical.Algebra.Group.Base

open GroupStr

ℤ : Group₀
fst ℤ = ℤType
1g (snd ℤ) = 0
_·_ (snd ℤ) = _+ℤ_
inv (snd ℤ) = _-ℤ_ 0
isGroup (snd ℤ) = isGroupℤ
  where
  abstract
    isGroupℤ : IsGroup (pos 0) _+ℤ_ (_-ℤ_ (pos 0))
    isGroupℤ = makeIsGroup isSetℤ +Assoc (λ _ → refl) (+Comm 0)
                           (λ x → +Comm x (pos 0 -ℤ x) ∙ minusPlus x 0)
                           (λ x → minusPlus x 0)

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
{- revised nomenclature -}
module Oscar.Data4 where

record ⊤ : Set where
  constructor tt

Const_ : ∀ {a} {A : Set a} {b} {B : Set b} → B → A → B
Const_ x _ = x

infixr 20 _∷_

-- List
data ⟦_⟧ {a} (A : Set a) : Set a where
  ∅ : ⟦ A ⟧
  _∷_ : A → ⟦ A ⟧ → ⟦ A ⟧

-- Nat
⟦⟧ = ⟦ ⊤ ⟧

infix 21 ¡_
pattern ¡_ ⟦A⟧ = tt ∷ ⟦A⟧
--¡ : ⟦⟧ → ⟦⟧
--¡ ⟦A⟧ = tt ∷ ⟦A⟧

-- Fin (with a payload)
data ⟦_⟧[_] {a} (A : ⟦⟧ → Set a) : ⟦⟧ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[ ¡ n ]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ n ] → ⟦ A ⟧[ ¡ n ]

⟦⟧[_] = ⟦ Const ⊤ ⟧[_]

-- Vec (with an (optional) index)
data ⟦_⟧[_₀] {a} (A : ⟦⟧ → Set a) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ ∅ ₀]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ n ₀] → ⟦ A ⟧[ ¡ n ₀]

⟦⟧[_₀] = ⟦ Const ⊤ ⟧[_₀]

-- m ≤ n, counting down from n-1 to m
data ⟦_⟧[_≤_↓] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ m ≤ m ↓]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ m ≤ n ↓] → ⟦ A ⟧[ m ≤ ¡ n ↓]

⟦⟧[_≤_↓] = ⟦ Const ⊤ ⟧[_≤_↓]

-- m ≤ n, counting up from m to n-1
data ⟦_⟧[↑_≤_] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[↑ m ≤ m ]
  _∷_ : ∀ {n} → A m → ⟦ A ⟧[↑ ¡ m ≤ n ] → ⟦ A ⟧[↑ m ≤ n ]

⟦⟧[↑_≤_] = ⟦ Const ⊤ ⟧[↑_≤_]

-- Inj (almost)
data ⟦_⟧[↓_≤_↓] {a} (A : ⟦⟧ → ⟦⟧ → Set a) : ⟦⟧ → ⟦⟧ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[↓ ∅ ≤ n ↓]
  _∷_ : ∀ {m n} → A m n → ⟦ A ⟧[↓ m ≤ n ↓] → ⟦ A ⟧[↓ ¡ m ≤ ¡ n ↓]

⟦⟧[↓_≤_↓] = ⟦ Const Const ⊤ ⟧[↓_≤_↓]

infix 21 ‼_
pattern ‼_ ⟦A⟧ = tt ∷ ⟦A⟧ -- tricky, works for all above _∷_ constructors only because it is defined afterwards, won't work for any later-defined constructors

testNat : ⟦⟧
testNat = ¡ ∅

testListNat : ⟦ ⟦⟧ ⟧
testListNat = ¡ ∅ ∷ ‼ ∅ ∷ ‼ ‼ ∅ ∷ ∅ ∷ ¡ ¡ ¡ ∅ ∷ ∅

testFin : ⟦⟧[ ¡ ¡ ∅ ]
testFin = ‼ ∅

test≤↓ : ⟦⟧[ ‼ ‼ ‼ ∅ ≤ ‼ ‼ ‼ ‼ ‼ ∅ ↓]
test≤↓ = ‼ ‼ ∅

⓪ ⑴ ⑵ : ⟦⟧
⓪ = ∅
⑴ = ‼ ∅
⑵ = ‼ ⑴


text:
{-# OPTIONS --show-irrelevant --subtyping #-}

module Issue2170-unify-subtyping where

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

record Squash (A : Set) : Set where
  constructor squash
  field .unsquash : A
open Squash

record UnSquash (A : Set) (s : A → Squash A) : Set where
  constructor inverse
  field
    inv : Squash A → A
    prf : {a : A} → inv (s a) ≡ a

test : {A : Set} → Squash (UnSquash A squash)
test = squash (inverse (λ p@(squash x) → _) refl)

-- `refl` is checked at type `_15 A (squash a) ≡ a`
-- Before, Agda solved this as `_15 := λ A p → unsquash a`, which
-- makes use of the irrelevant projection `unsquash`.
-- However, this is not allowed unless `--irrelevant-projections`
-- is enabled.

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------
-- Normal and neutral terms
------------------------------------------------------------------------

open import Level using (zero)
open import Data.Universe

module README.DependentlyTyped.NormalForm
  (Uni₀ : Universe zero zero) where

open import Data.Product as Prod renaming (curry to c; uncurry to uc)
open import Function hiding (_∋_) renaming (const to k; _∘_ to _⊚_)
import README.DependentlyTyped.Term as Term; open Term Uni₀
import Relation.Binary.PropositionalEquality as P

-- Atomic types (types for which the normaliser does not do
-- η-expansion).

data _⊢_atomic-type (Γ : Ctxt) : Type Γ → Set where
  ⋆  : ∀ {σ} → Γ ⊢ ⋆  , σ atomic-type
  el : ∀ {σ} → Γ ⊢ el , σ atomic-type

-- Two kinds: normal and neutral.

data Kind : Set where
  no ne : Kind

mutual

  -- Γ ⊢ σ ⟨ no ⟩ represents η-long, β-normal terms, Γ ⊢ σ ⟨ ne ⟩
  -- represents neutral terms.

  infixl 9 _·_
  infix  3 _⊢_⟨_⟩

  data _⊢_⟨_⟩ (Γ : Ctxt) : Type Γ → Kind → Set where
    ne  : ∀ {σ} (σ′ : Γ ⊢ σ atomic-type) (t : Γ ⊢ σ ⟨ ne ⟩) →
          Γ ⊢ σ ⟨ no ⟩
    var : ∀ {σ} (x : Γ ∋ σ) → Γ ⊢ σ ⟨ ne ⟩
    ƛ   : ∀ {σ τ} (t : Γ ▻ σ ⊢ τ ⟨ no ⟩) → Γ ⊢ Type-π σ τ ⟨ no ⟩
    _·_ : ∀ {sp₁ sp₂ σ}
          (t₁ : Γ ⊢ π sp₁ sp₂ , σ ⟨ ne ⟩) (t₂ : Γ ⊢ fst σ ⟨ no ⟩) →
          Γ ⊢ snd σ /̂ ŝub ⟦ ⌊ t₂ ⌋ ⟧ ⟨ ne ⟩

  -- Normal and neutral terms can be turned into ordinary terms.

  ⌊_⌋ : ∀ {Γ σ k} → Γ ⊢ σ ⟨ k ⟩ → Γ ⊢ σ
  ⌊ ne σ′ t ⌋ = ⌊ t ⌋
  ⌊ var x   ⌋ = var x
  ⌊ ƛ t     ⌋ = ƛ ⌊ t ⌋
  ⌊ t₁ · t₂ ⌋ = ⌊ t₁ ⌋ · ⌊ t₂ ⌋

-- Normal and neutral terms are "term-like".

Tm-n : Kind → Term-like _
Tm-n k = record { _⊢_ = λ Γ σ → Γ ⊢ σ ⟨ k ⟩; ⟦_⟧ = ⟦_⟧ ⊚ ⌊_⌋ }

private
  open module T {k} = Term-like (Tm-n k) public
    using ([_])
    renaming ( ⟦_⟧ to ⟦_⟧n; _≅-⊢_ to _≅-⊢n_
             ; drop-subst-⊢ to drop-subst-⊢n; ⟦⟧-cong to ⟦⟧n-cong
             )

-- As mentioned above normal and neutral terms can be turned into
-- ordinary terms.

forget-n : ∀ {k} → [ Tm-n k ⟶⁼ Tm ]
forget-n = record
  { function    = λ _ → ⌊_⌋
  ; corresponds = λ _ _ → P.refl
  }

-- Various congruences.

ne-cong : ∀ {Γ σ} {σ′ : Γ ⊢ σ atomic-type}
            {t₁ t₂ : Γ ⊢ σ ⟨ ne ⟩} →
          t₁ ≅-⊢n t₂ → ne σ′ t₁ ≅-⊢n ne σ′ t₂
ne-cong P.refl = P.refl

var-n-cong : ∀ {Γ₁ σ₁} {x₁ : Γ₁ ∋ σ₁}
               {Γ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} →
             x₁ ≅-∋ x₂ → var x₁ ≅-⊢n var x₂
var-n-cong P.refl = P.refl

ƛn-cong : ∀ {Γ₁ σ₁ τ₁} {t₁ : Γ₁ ▻ σ₁ ⊢ τ₁ ⟨ no ⟩}
            {Γ₂ σ₂ τ₂} {t₂ : Γ₂ ▻ σ₂ ⊢ τ₂ ⟨ no ⟩} →
          t₁ ≅-⊢n t₂ → ƛ t₁ ≅-⊢n ƛ t₂
ƛn-cong P.refl = P.refl

·n-cong :
  ∀ {Γ₁ sp₁₁ sp₂₁ σ₁}
    {t₁₁ : Γ₁ ⊢ π sp₁₁ sp₂₁ , σ₁ ⟨ ne ⟩} {t₂₁ : Γ₁ ⊢ fst σ₁ ⟨ no ⟩}
    {Γ₂ sp₁₂ sp₂₂ σ₂}
    {t₁₂ : Γ₂ ⊢ π sp₁₂ sp₂₂ , σ₂ ⟨ ne ⟩} {t₂₂ : Γ₂ ⊢ fst σ₂ ⟨ no ⟩} →
    t₁₁ ≅-⊢n t₁₂ → t₂₁ ≅-⊢n t₂₂ → t₁₁ · t₂₁ ≅-⊢n t₁₂ · t₂₂
·n-cong P.refl P.refl = P.refl

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:
------------------------------------------------------------------------
-- Semantics of the parsers
------------------------------------------------------------------------

-- Currently it is only specified when a string is _accepted_ by a
-- parser; semantic actions are not included.

module RecursiveDescent.Inductive.Semantics where

open import RecursiveDescent.Index
open import RecursiveDescent.Inductive
open import RecursiveDescent.Inductive.SimpleLib

open import Data.List
open import Data.Product.Record
open import Data.Maybe

infix 3 _∈⟦_⟧_

mutual

  _∈⟦_⟧_ : forall {tok nt i r} ->
           List tok -> Parser tok nt i r -> Grammar tok nt -> Set1
  s ∈⟦ p ⟧ g = Semantics g s p

  data Semantics {tok : Set} {nt : ParserType₁} (g : Grammar tok nt)
                 : forall {i r} ->
                   List tok -> Parser tok nt i r -> Set1 where
    !-sem      : forall {e c r} s (x : nt (e , c) r) ->
                 s ∈⟦ g x ⟧ g -> s ∈⟦ ! x ⟧ g
    symbol-sem : forall c -> [ c ] ∈⟦ symbol ⟧ g
    return-sem : forall {r} (x : r) -> [] ∈⟦ return x ⟧ g
    -- The following rule should really describe the intended
    -- semantics of _>>=_, not _⊛_. _!>>=_ should also get a rule.
    ⊛-sem      : forall {i₁ i₂ r₁ r₂ s₁ s₂}
                        {p₁ : Parser tok nt i₁ (r₁ -> r₂)}
                        {p₂ : Parser tok nt i₂ r₁} ->
                 s₁ ∈⟦ p₁ ⟧ g -> s₂ ∈⟦ p₂ ⟧ g -> s₁ ++ s₂ ∈⟦ p₁ ⊛ p₂ ⟧ g
    ∣ˡ-sem     : forall {i₁ i₂ r s}
                        {p₁ : Parser tok nt i₁ r}
                        {p₂ : Parser tok nt i₂ r} ->
                 s ∈⟦ p₁ ⟧ g -> s ∈⟦ p₁ ∣ p₂ ⟧ g
    ∣ʳ-sem     : forall {i₁ i₂ r s}
                        {p₁ : Parser tok nt i₁ r}
                        {p₂ : Parser tok nt i₂ r} ->
                 s ∈⟦ p₂ ⟧ g -> s ∈⟦ p₁ ∣ p₂ ⟧ g

------------------------------------------------------------------------
-- Soundness of recognition

data NonEmpty {a : Set} : List a -> Set where
  nonEmpty : forall x xs -> NonEmpty (x ∷ xs)

postulate
  sound : forall {tok nt i r}
          (p : Parser tok nt i r) (g : Grammar tok nt) (s : List tok) ->
          NonEmpty (parse-complete p g s) -> s ∈⟦ p ⟧ g

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --without-K  #-}
module algebra.group where

open import algebra.group.core public
open import algebra.group.morphism public
open import algebra.group.gset public
open import algebra.group.classifying public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
-- ----------------------------------------------------------------------
-- The Agda σ-library
--
-- Substitutions
-- ----------------------------------------------------------------------

module Sigma.Subst.Core where

open import Sigma.Renaming.Base

open import Data.Nat using (ℕ; _+_)
open import Data.Fin using (Fin)

open import Function using (_∘_)

open import Data.Product using (_×_; proj₁; proj₂) renaming ( _,_ to ⟨_,_⟩ )

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

open import Sigma.Subst.Base public

splitAt : ∀ m { n } { T }
  → Sub T (m + n)
  -- -------------
  → Sub T m × Sub T n
splitAt m σ = ⟨ σ ∘ (id✶ m) , σ ∘ (↑✶ m) ⟩

take : ∀ m { n } { T }
  → Sub T (m + n)
  → Sub T m
take m σ = proj₁ (splitAt m σ)

drop : ∀ m { n } { T }
  → Sub T (m + n)
  → Sub T n
drop m σ = proj₂ (splitAt m σ)

max_stars_repo_name: johnyob/agda-sigma

max_issues_repo_name: johnyob/agda-sigma

max_forks_repo_name: johnyob/agda-sigma


text:
{-# OPTIONS --without-K --safe #-}
module Util.Relation.Binary.Closure.SymmetricTransitive where

open import Relation.Binary using (Rel)

open import Util.Prelude

data SymTrans {α ρ} {A : Set α} (R : Rel A ρ) : Rel A (α ⊔ℓ ρ) where
  `base : ∀ {x y} → R x y → SymTrans R x y
  `sym : ∀ {x y} → SymTrans R y x → SymTrans R x y
  `trans : ∀ {x y z} → SymTrans R x y → SymTrans R y z → SymTrans R x z

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


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

open import HoTT
open import cohomology.CofiberSequence
open import cohomology.Exactness
open import cohomology.FunctionOver
open import cohomology.Theory
open import cohomology.ProductRepr
open import cohomology.WedgeCofiber

{- Finite additivity is provable (and in a stronger form) without using
 - the additivity axiom. For any m ≥ 0,

         Cⁿ(Σᵐ(X ∨ Y)) == Cⁿ(ΣᵐX) × Cⁿ(ΣᵐY)

 - and over this path
\ -   ∙ Cⁿ(Σᵐwinl) corresponds to fst : Cⁿ(ΣᵐX) × Cⁿ(ΣᵐY) → Cⁿ(ΣᵐX),
 -   ∙ Cⁿ(Σᵐwinr) corresponds to snd : Cⁿ(ΣᵐX) × Cⁿ(ΣᵐY) → Cⁿ(ΣᵐY),
 -   ∙ Cⁿ(Σᵐ(Wedge-rec winl* winr* wglue*)) : Cⁿ(ΣᵐZ) → Cⁿ(Σᵐ(X ∨ Y))
       corresponds to Cⁿ(Σᵐwinl*) × Cⁿ(Σᵐwinr*).
 -}

module cohomology.Wedge {i} (CT : CohomologyTheory i) where

module CSusp^Wedge (n : ℤ) (X Y : Ptd i) (m : ℕ) where

  open WedgeCofiber X Y

  open CohomologyTheory CT
  open import cohomology.ConstantFunction CT

  private
    βl : CF-hom n (⊙susp^-fmap m ⊙winl) ∘ᴳ
         CF-hom n (⊙susp^-fmap m ⊙projl)
         == idhom _
    βl = ! (CF-comp n (⊙susp^-fmap m ⊙projl)
                       (⊙susp^-fmap m ⊙winl))
         ∙ ap (CF-hom n)
              (! (⊙susp^-fmap-∘ m ⊙projl ⊙winl)
               ∙ ⊙susp^-fmap-idf m _)
         ∙ CF-ident n

    βr : CF-hom n (⊙susp^-fmap m ⊙winr) ∘ᴳ
         CF-hom n (⊙susp^-fmap m ⊙projr)
         == idhom _
    βr = ! (CF-comp n (⊙susp^-fmap m ⊙projr)
                      (⊙susp^-fmap m ⊙winr))
         ∙ ap (CF-hom n)
              (! (⊙susp^-fmap-∘ m ⊙projr ⊙winr)
               ∙ ap (⊙susp^-fmap m) ⊙projr-winr
               ∙ ⊙susp^-fmap-idf m _)
         ∙ CF-ident n
      where
      ⊙projr-winr : ⊙projr ⊙∘ ⊙winr == ⊙idf _
      ⊙projr-winr = ⊙λ= (λ _ → idp) $
        ∙-unit-r _ ∙ ap-! projr wglue ∙ ap ! Projr.glue-β

  open ProductRepr
    (CF-hom n (⊙susp^-fmap m ⊙projl))
    (CF-hom n (⊙susp^-fmap m ⊙projr))
    (CF-hom n (⊙susp^-fmap m ⊙winl))
    (CF-hom n (⊙susp^-fmap m ⊙winr))
    (app= (ap GroupHom.f βl))
    (app= (ap GroupHom.f βr))
    (transport
      (λ {(_ , f , g) → is-exact (CF n g) (CF n f)})
      (suspend^-cof= m ⊙winr ⊙projl
        (pair= CofWinr.⊙path CofWinr.cfcod-over))
      (C-exact n (⊙susp^-fmap m ⊙winr)))
    (transport
      (λ {(_ , f , g) → is-exact (CF n g) (CF n f)})
      (suspend^-cof= m ⊙winl ⊙projr
        (pair= CofWinl.⊙path CofWinl.cfcod-over))
      (C-exact n (⊙susp^-fmap m ⊙winl)))
    public

  wedge-rec-over : {Z : Ptd i}
    (winl* : fst X → fst Z) (winr* : fst Y → fst Z)
    (wglue* : winl* (snd X) == winr* (snd Y)) (pt : winl* (snd X) == snd Z)
    → CF-hom n (⊙susp^-fmap m (WedgeRec.f winl* winr* wglue* , pt))
      == ×ᴳ-hom-in (CF-hom n (⊙susp^-fmap m (winl* , pt)))
                   (CF-hom n (⊙susp^-fmap m (winr* , ! wglue* ∙ pt)))
      [ (λ K → C n (⊙Susp^ m Z) →ᴳ K) ↓ iso ]
  wedge-rec-over winl* winr* wglue* pt = codomain-over-iso _ _ _ _ $
    codomain-over-equiv
      (fst (CF n (⊙susp^-fmap m (WedgeRec.f winl* winr* wglue* , pt)))) _
    ▹ ap2 (λ f g z → (f z , g z))
        (ap GroupHom.f $ ! $
          ap (CF-hom n) (⊙susp^-fmap-∘ m (rec , pt) ⊙winl)
          ∙ CF-comp n (⊙susp^-fmap m (rec , pt)) (⊙susp^-fmap m ⊙winl))
        (ap GroupHom.f $ ! $
          ap (CF-hom n) (ap (⊙susp^-fmap m) (pair= idp (! pt-lemma))
                         ∙ ⊙susp^-fmap-∘ m (rec , pt) ⊙winr)
          ∙ CF-comp n (⊙susp^-fmap m (rec , pt)) (⊙susp^-fmap m ⊙winr))
    where
    rec = WedgeRec.f winl* winr* wglue*

    pt-lemma : ap rec (! wglue) ∙ pt == ! wglue* ∙ pt
    pt-lemma = ap (λ w → w ∙ pt) $
                 ap-! rec wglue ∙ ap ! (WedgeRec.glue-β winl* winr* wglue*)

  wedge-in-over : {Z : Ptd i}
    (f : fst (⊙Susp^ m Z ⊙→ ⊙Susp^ m (⊙Wedge X Y)))
    → CF-hom n f
      == ×ᴳ-sum-hom (C-abelian n _)
           (CF-hom n (⊙susp^-fmap m ⊙projl ⊙∘ f))
           (CF-hom n (⊙susp^-fmap m ⊙projr ⊙∘ f))
      [ (λ G → G →ᴳ C n (⊙Susp^ m Z)) ↓ iso ]
  wedge-in-over f =
    lemma (C-abelian n _) (C-abelian n _) inl-over inr-over
    ▹ ap2 (×ᴳ-sum-hom (C-abelian n _))
        (! (CF-comp n (⊙susp^-fmap m ⊙projl) f))
        (! (CF-comp n (⊙susp^-fmap m ⊙projr) f))
    where
    lemma : {G H K L : Group i}
      (aG : is-abelian G) (aL : is-abelian L) {p : G == H ×ᴳ K}
      {φ : H →ᴳ G} {ψ : K →ᴳ G} {χ : G →ᴳ L}
      → φ == ×ᴳ-inl [ (λ J → H →ᴳ J) ↓ p ]
      → ψ == ×ᴳ-inr {G = H} [ (λ J → K →ᴳ J) ↓ p ]
      → χ == ×ᴳ-sum-hom aL (χ ∘ᴳ φ) (χ ∘ᴳ ψ) [ (λ J → J →ᴳ L) ↓ p ]
    lemma {H = H} {K = K} aG aL {p = idp} {χ = χ} idp idp =
      ap (λ α → χ ∘ᴳ α) (×ᴳ-sum-hom-η H K aG)
      ∙ ! (∘-×ᴳ-sum-hom aG aL χ (×ᴳ-inl {G = H}) (×ᴳ-inr {G = H}))

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
-- Andreas, 2014-01-17 Issue 1402
-- where clauses after a pointless rewrite

open import Common.Equality

postulate eq : Set1 ≡ Set1

test : Set1
test rewrite eq = bla
  where bla = Set

-- should succeed (or maybe alert the user of the pointless rewrite)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import SystemT
open import Data.List using ([])

module Examples where

  -- λ x . x
  ex1 : [] ⊢ base ⟶ base
  ex1 = lam (var i0)

  -- λ x . λ y . y
  ex2 : [] ⊢ base ⟶ base ⟶ base
  ex2 = lam (lam (var i0))

  -- λ x . λ y . x
  ex3 : [] ⊢ base ⟶ base ⟶ base
  ex3 = lam (lam (var (iS i0)))

max_stars_repo_name: ayberkt/system-t-normalization

max_issues_repo_name: ayberkt/system-t-normalization

max_forks_repo_name: ayberkt/system-t-normalization


text:
{-

Counting how many structured finite sets with a given cardinal

https://github.com/EgbertRijke/OEIS-A000001

-}
{-# OPTIONS --safe #-}

module Cubical.Experiments.CountingFiniteStructure where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Data.Nat
open import Cubical.Data.Bool
open import Cubical.Data.Sigma

open import Cubical.Data.FinSet
open import Cubical.Data.FinSet.Induction
open import Cubical.Data.FinSet.Constructors
open import Cubical.Data.FinType
open import Cubical.Data.FinType.FiniteStructure

private
  variable
    ℓ : Level

-- convenient abbreviation

isFinStrCard : (S : FinSet ℓ-zero → FinSet ℓ) (n : ℕ) → isFinType 0 (FinSetWithStrOfCard S n)
isFinStrCard S n = isFinTypeFinSetWithStrOfCard S n

-- structure that there is no structure

TrivialStr : FinSet ℓ → FinSet ℓ
TrivialStr _ = 𝟙

-- structure that "picking an element in that set"

IdentityStr : FinSet ℓ → FinSet ℓ
IdentityStr X = X

-- finite semi-groups

FinSemiGroupStr : FinSet ℓ → FinSet ℓ
FinSemiGroupStr X .fst =
  Σ[ p ∈ (X .fst → X .fst → X .fst) ] ((x y z : X .fst) → p (p x y) z ≡ p x (p y z))
FinSemiGroupStr X .snd =
  isFinSetΣ (_ , isFinSetΠ2 X (λ _ → X) (λ _ _ → X))
    (λ p → _ , isFinSetΠ3 X (λ _ → X) (λ _ _ → X) (λ _ _ _ → _ , isFinSet≡ X _ _))

-- finite groups

FinGroupStr : FinSet ℓ → FinSet ℓ
FinGroupStr X .fst =
  Σ[ e ∈ X .fst ]
    Σ[ inv ∈ (X .fst → X .fst) ]
      Σ[ p ∈ (X .fst → X .fst → X .fst) ]
          ((x y z : X .fst) → p (p x y) z ≡ p x (p y z))
        × ((x : X .fst)
            → (p x e ≡ x) × (p e x ≡ x) × (p (inv x) x ≡ e) × (p x (inv x) ≡ e))
FinGroupStr X .snd =
  isFinSetΣ X (λ _ → _ ,
    isFinSetΣ (_ , isFinSetΠ X (λ _ → X)) (λ _ → _ ,
      isFinSetΣ (_ , isFinSetΠ2 X (λ _ → X) (λ _ _ → X)) (λ _ → _ ,
        isFinSet× (_ , isFinSetΠ3 X (λ _ → X) (λ _ _ → X) (λ _ _ _ → _ , isFinSet≡ X _ _)) (_ ,
          isFinSetΠ X (λ _ → _ ,
            isFinSet× (_ , isFinSet≡ X _ _) (_ ,
              isFinSet× (_ , isFinSet≡ X _ _) (_ ,
                isFinSet× (_ , isFinSet≡ X _ _) (_ , isFinSet≡ X _ _))))))))

-- two rather trivial numbers
-- but the computation is essentially not that trivial
-- Time: 5 ms
a2 : ℕ
a2 = card (_ , isFinStrCard TrivialStr 2)

-- this is already hard to compute
-- Time: 443 ms
b2 : ℕ
b2 = card (_ , isFinStrCard IdentityStr 2)

-- the number of finite semi-groups
numberOfFinSemiGroups : ℕ → ℕ
numberOfFinSemiGroups n = card (_ , isFinStrCard FinSemiGroupStr n)

-- two trivial cases of semi-groups
-- Time: 29 ms
n0 : ℕ
n0 = numberOfFinSemiGroups 0

-- Time: 2,787ms
n1 : ℕ
n1 = numberOfFinSemiGroups 1

-- the number of finite semi-groups with cardinal 2
-- it should be 5
-- would you like to try?
n2 : ℕ
n2 = numberOfFinSemiGroups 2

-- OEIS-A000001
-- I think you'd better not evaluate this function with n > 1
numberOfFinGroups : ℕ → ℕ
numberOfFinGroups n = card (_ , isFinStrCard FinGroupStr n)

-- group with one element
-- Time: 26,925ms
g1 : ℕ
g1 = numberOfFinGroups 1

-- Rijke's challenge
-- seemed to big to do an exhaustive search
g4 : ℕ
g4 = numberOfFinGroups 4

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical