text:
import cedille-options
module elaboration (options : cedille-options.options) where

open import lib

options' = record options
  {during-elaboration = tt;
   erase-types = ff;
   show-qualified-vars = ff}

open import general-util
open import monad-instances
open import cedille-types
open import classify options' {id}
open import ctxt
open import constants
open import conversion
open import is-free
open import meta-vars options' {id}
open import spans options {IO}
open import subst
open import syntax-util
open import toplevel-state options {IO}
open import to-string options'
open import rename
open import rewriting
open import elaboration-helpers options
open import templates
import spans options' {id} as id-spans

{- Datatypes -}

mendler-encoding : datatype-encoding
mendler-encoding =
  let functorₓ = "Functor"
      castₓ = "cast"
      fixpoint-typeₓ = "CVFixIndM"
      fixpoint-inₓ = "cvInFixIndM"
      fixpoint-indₓ = "cvIndFixIndM" in
  record {
    template = MendlerTemplate;
    functor = functorₓ;
    cast = castₓ;
    fixpoint-type = fixpoint-typeₓ;
    fixpoint-in = fixpoint-inₓ;
    fixpoint-ind = fixpoint-indₓ;
    elab-mu = λ {
      (Data x ps is cs)
      (mk-encoded-datatype-names data-functorₓ data-fmapₓ data-functor-indₓ castₓ
        fixpoint-typeₓ fixpoint-inₓ fixpoint-indₓ)
      Γ t oT ms → record {
        elab-check-mu = λ ihₓ T → nothing;
        elab-synth-mu = case oT of λ {
          NoType ihₓ → nothing;
          (SomeType Tₘ) ihₓ → nothing
        };

        elab-check-mu' = λ T → nothing;
        elab-synth-mu' = case oT of λ {
          NoType → nothing;
          (SomeType Tₘ) → nothing
        }
      }
    }
  }

mendler-simple-encoding : datatype-encoding
mendler-simple-encoding =
  let functorₓ = "RecFunctor"
      castₓ = "cast"
      fixpoint-typeₓ = "FixM"
      fixpoint-inₓ = "inFix"
      fixpoint-indₓ = "IndFixM" in
  record {
    template = MendlerSimpleTemplate;
    functor = functorₓ;
    cast = castₓ;
    fixpoint-type = fixpoint-typeₓ;
    fixpoint-in = fixpoint-inₓ;
    fixpoint-ind = fixpoint-indₓ;
    elab-mu = λ {
      (Data x ps is cs)
      (mk-encoded-datatype-names data-functorₓ data-fmapₓ data-functor-indₓ castₓ
        fixpoint-typeₓ fixpoint-inₓ fixpoint-indₓ)
      Γ t oT ms → record {
        elab-check-mu = λ ihₓ T →
          -- let Tₘ = case oT of λ {(SomeType Tₘ) → Tₘ; NoType → indices-to-tplams is $ TpLambda posinfo-gen posinfo-gen ignored-var (Tkt {!!}) T} in
          nothing;
        elab-synth-mu = case oT of λ {
          NoType ihₓ → nothing;
          (SomeType Tₘ) ihₓ → nothing
        };

        elab-check-mu' = λ T → nothing;
        elab-synth-mu' = case oT of λ {
          NoType → nothing;
          (SomeType Tₘ) → nothing
        }
      }
    }
  }

selected-encoding = mendler-simple-encoding
-- TODO: ^ Add option so user can choose encoding ^

{-# TERMINATING #-}
elab-check-term : ctxt → term → type → maybe term
elab-synth-term : ctxt → term → maybe (term × type)
elab-pure-term : ctxt → term → maybe term
elab-type : ctxt → type → maybe (type × kind)
elab-pure-type : ctxt → type → maybe type
elab-kind : ctxt → kind → maybe kind
elab-pure-kind : ctxt → kind → maybe kind
elab-tk : ctxt → tk → maybe tk
elab-pure-tk : ctxt → tk → maybe tk

elab-typeh : ctxt → type → 𝔹 → maybe (type × kind)
elab-kindh : ctxt → kind → 𝔹 → maybe kind
elab-tkh : ctxt → tk → 𝔹 → maybe tk
elab-type-arrow : type → type
elab-kind-arrow : kind → kind
elab-tk-arrow : tk → tk
elab-hnf-type : ctxt → type → 𝔹 → maybe type
elab-hnf-kind : ctxt → kind → 𝔹 → maybe kind
elab-hnf-tk : ctxt → tk → 𝔹 → maybe tk
elab-app-term : ctxt → term → prototype → 𝔹 → maybe ((meta-vars → maybe term) × spine-data)

elab-type Γ T = elab-typeh Γ T tt
elab-kind Γ k = elab-kindh Γ k tt
elab-tk Γ atk = elab-tkh Γ atk tt
elab-pure-type Γ T = maybe-map fst (elab-typeh Γ T ff)
elab-pure-kind Γ k = elab-kindh Γ k ff
elab-pure-tk Γ atk = elab-tkh Γ atk ff

elab-type-arrow (Abs pi b pi' x atk T) = Abs pi b pi' x (elab-tk-arrow atk) (elab-type-arrow T)
elab-type-arrow (Iota pi pi' x T T') = Iota pi pi' x (elab-type-arrow T) (elab-type-arrow T')
elab-type-arrow (Lft pi pi' x t lT) = Lft pi pi' x t lT
elab-type-arrow (NoSpans T pi) = elab-type-arrow T
elab-type-arrow (TpLet pi (DefTerm pi' x NoType t) T') = TpLet pi (DefTerm pi x NoType t) (elab-type-arrow T')
elab-type-arrow (TpLet pi (DefTerm pi' x (SomeType T) t) T') = TpLet pi (DefTerm pi x (SomeType (elab-type-arrow T)) t) T'
elab-type-arrow (TpLet pi (DefType pi' x k T) T') = TpLet pi (DefType pi' x (elab-kind-arrow k) (elab-type-arrow T)) (elab-type-arrow T')
elab-type-arrow (TpApp T T') = TpApp (elab-type-arrow T) (elab-type-arrow T')
elab-type-arrow (TpAppt T t) = TpAppt (elab-type-arrow T) t
elab-type-arrow (TpArrow T a T') = Abs posinfo-gen a posinfo-gen "_" (Tkt (elab-type-arrow T)) (elab-type-arrow T')
elab-type-arrow (TpEq pi t t' pi') = TpEq pi (erase-term t) (erase-term t') pi'
elab-type-arrow (TpHole pi) = TpHole pi
elab-type-arrow (TpLambda pi pi' x atk T) = TpLambda pi pi' x (elab-tk-arrow atk) (elab-type-arrow T)
elab-type-arrow (TpParens pi T pi') = elab-type-arrow T
elab-type-arrow (TpVar pi x) = TpVar pi x

elab-kind-arrow (KndArrow k k') = KndPi posinfo-gen posinfo-gen "_" (Tkk (elab-kind-arrow k)) (elab-kind-arrow k')
elab-kind-arrow (KndParens pi k pi') = elab-kind-arrow k
elab-kind-arrow (KndPi pi pi' x atk k) = KndPi pi pi' x (elab-tk-arrow atk) (elab-kind-arrow k)
elab-kind-arrow (KndTpArrow T k) = KndPi posinfo-gen posinfo-gen "_" (Tkt (elab-type-arrow T)) (elab-kind-arrow k)
elab-kind-arrow k = k

elab-tk-arrow (Tkt T) = Tkt (elab-type-arrow T)
elab-tk-arrow (Tkk k) = Tkk (elab-kind-arrow k)

elab-hnf-type Γ T b = just (elab-type-arrow (substh-type {TYPE} Γ empty-renamectxt empty-trie (hnf Γ (unfolding-set-erased unfold-head (~ b)) T tt)))
elab-hnf-kind Γ k b = just (elab-kind-arrow (substh-kind {KIND} Γ empty-renamectxt empty-trie (hnf Γ (unfolding-set-erased unfold-head (~ b)) k tt)))
elab-hnf-tk Γ (Tkt T) b = elab-hnf-type Γ T b ≫=maybe (just ∘ Tkt)
elab-hnf-tk Γ (Tkk k) b = elab-hnf-kind Γ k b ≫=maybe (just ∘ Tkk)

elab-check-term Γ (App t me t') T =
  elab-app-term Γ (App t me t') (proto-maybe (just T)) tt ≫=maybe uncurry λ where
    tf (mk-spine-data Xs T' _) → tf Xs
elab-check-term Γ (AppTp t T) T' =
  elab-synth-term Γ t ≫=maybe uncurry λ t T'' →
  elab-type Γ T ≫=maybe uncurry λ T k →
  just (AppTp t T)
elab-check-term Γ (Beta pi ot ot') T =
  let ot'' = case ot' of λ where NoTerm → just (fresh-id-term Γ); (SomeTerm t _) → elab-pure-term Γ (erase-term t) in
  case ot of λ where
    NoTerm → elab-hnf-type Γ T tt ≫=maybe λ where
      (TpEq _ t₁ t₂ _) → ot'' ≫=maybe (just ∘ mbeta t₁)
      _ → nothing
    (SomeTerm t _) →
      elab-pure-term Γ (erase-term t) ≫=maybe λ t →
      ot'' ≫=maybe (just ∘ mbeta t)
elab-check-term Γ (Chi pi mT t) T = case mT of λ where
  NoType → maybe-map fst (elab-synth-term Γ t)
  (SomeType T') →
    elab-pure-type Γ (erase-type T') ≫=maybe λ T' →
    let id = fresh-id-term Γ in
    elab-check-term Γ t T' ≫=maybe
    (just ∘ mrho (mbeta id id) "_" T')
elab-check-term Γ (Delta pi mT t) T =
  elab-pure-type Γ (erase-type T) ≫=maybe λ T →
  elab-synth-term Γ t ≫=maybe uncurry λ where
    t (TpEq _ t1 t2 _) →
      rename "x" from Γ for λ x →
      rename "y" from Γ for λ y →
      rename "z" from Γ for λ z →
      let ρ = renamectxt-insert (renamectxt-insert (renamectxt-insert empty-renamectxt x x) y y) z z
          tt-term = mlam x (mlam y (mvar x))
          ff-term = mlam x (mlam y (mvar y)) in
      if conv-term Γ t1 tt-term && conv-term Γ t2 ff-term
        then just (Delta posinfo-gen (SomeType T) t)
        else
          delta-contra (hnf Γ unfold-head t1 tt) (hnf Γ unfold-head t2 tt) ≫=maybe λ f →
          let f = substh-term {TERM} Γ ρ empty-trie f in
          elab-pure-term Γ (erase-term t) ≫=maybe λ pt →
          just (Delta posinfo-gen (SomeType T)
            (mrho t z (mtpeq (mapp f t1) (mapp f (mvar z))) (mbeta tt-term pt)))
    t T → nothing
elab-check-term Γ (Epsilon pi lr mm t) T =
  elab-hnf-type Γ T tt ≫=maybe λ where
    (TpEq _ t₁ t₂ _) → elab-check-term Γ (Chi posinfo-gen
      (SomeType (check-term-update-eq Γ lr mm posinfo-gen t₁ t₂ posinfo-gen)) t) T
    _ → nothing
elab-check-term Γ (Hole pi) T = nothing
elab-check-term Γ (IotaPair pi t t' og pi') T =
  elab-hnf-type Γ T tt ≫=maybe λ where
    (Iota _ pi x T' T'') →
      elab-check-term Γ t T' ≫=maybe λ t →
      elab-check-term Γ t' (subst Γ t x T'') ≫=maybe λ t' →
      rename x from Γ for λ x' →
      just (IotaPair posinfo-gen t t' (Guide posinfo-gen x' T'') posinfo-gen)
    _ → nothing
elab-check-term Γ (IotaProj t n pi) T =
  elab-synth-term Γ t ≫=maybe uncurry λ t T' →
  just (IotaProj t n posinfo-gen)
elab-check-term Γ (Lam pi l pi' x oc t) T =
  (elab-hnf-type Γ T tt ≫=maybe to-abs) ≫=maybe λ where
    (mk-abs b x' atk free T') →
      rename (if x =string "_" && free then x' else x) from Γ for λ x'' →
      elab-tk Γ atk ≫=maybe λ tk →
      elab-check-term (ctxt-tk-decl' pi' x'' atk Γ) (rename-var Γ x x'' t)
        (rename-var Γ x' x'' T') ≫=maybe λ t →
      just (Lam posinfo-gen l posinfo-gen x'' (SomeClass atk) t)
elab-check-term Γ (Let pi d t) T =
  case d of λ where
  (DefTerm pi' x NoType t') →
    rename x from Γ for λ x' →
    elab-synth-term Γ t' ≫=maybe uncurry λ t' T' →
    elab-check-term (ctxt-let-term-def pi' x' t' T' Γ) (rename-var Γ x x' t) T ≫=maybe λ t →
    just (Let posinfo-gen (DefTerm posinfo-gen x' NoType t') t)
  (DefTerm pi' x (SomeType T') t') →
    rename x from Γ for λ x' →
    elab-type Γ T' ≫=maybe uncurry λ T' k →
    elab-check-term Γ t' T' ≫=maybe λ t' →
    elab-check-term (ctxt-let-term-def pi' x' t' T' Γ) (rename-var Γ x x' t) T ≫=maybe λ t →
    just (Let posinfo-gen (DefTerm posinfo-gen x' NoType t') t)
  (DefType pi' x k T') →
    rename x from Γ for λ x' →
    elab-type Γ T' ≫=maybe uncurry λ T' k' →
    elab-check-term (ctxt-let-type-def pi' x' T' k' Γ) (rename-var Γ x x' t) T ≫=maybe λ t →
    just (Let posinfo-gen (DefType posinfo-gen x' k' T') t)
elab-check-term Γ (Open pi x t) T =
  ctxt-clarify-def Γ x ≫=maybe uncurry λ _ Γ →
  elab-check-term Γ t T
elab-check-term Γ (Parens pi t pi') T = elab-check-term Γ t T
elab-check-term Γ (Phi pi t t₁ t₂ pi') T =
  elab-pure-term Γ (erase-term t₁) ≫=maybe λ t₁' →
  elab-pure-term Γ (erase-term t₂) ≫=maybe λ t₂ →
  elab-check-term Γ t₁ T ≫=maybe λ t₁ →
  elab-check-term Γ t (mtpeq t₁' t₂) ≫=maybe λ t →
  just (Phi posinfo-gen t t₁ t₂ posinfo-gen)
elab-check-term Γ (Rho pi op on t og t') T =
  elab-synth-term Γ t ≫=maybe uncurry λ t T' →
  elab-hnf-type Γ (erase-type T') ff ≫=maybe λ where
    (TpEq _ t₁ t₂ _) → case og of λ where
      NoGuide →
        elab-hnf-type Γ T tt ≫=maybe λ T →
        rename "x" from Γ for λ x →
        let ns = fst (optNums-to-stringset on)
            Γ' = ctxt-var-decl x Γ
            rT = fst (rewrite-type T Γ' (is-rho-plus op) ns t t₁ x 0)
            rT' = post-rewrite Γ x t t₂ rT in
        elab-hnf-type Γ rT' tt ≫=maybe λ rT' →
        elab-check-term Γ t' rT' ≫=maybe
        (just ∘ mrho (Sigma posinfo-gen t) x (erase-type rT))
      (Guide pi' x T') →
        let Γ' = ctxt-var-decl x Γ in
        elab-pure-type Γ' (erase-type T') ≫=maybe λ T' →
        elab-check-term Γ t' (post-rewrite Γ' x t t₂ (rewrite-at Γ' x t tt T T')) ≫=maybe
        (just ∘ mrho t x T')
    _ → nothing
elab-check-term Γ (Sigma pi t) T =
  elab-hnf-type Γ T tt ≫=maybe λ where
    (TpEq _ t₁ t₂ _) →
      elab-check-term Γ t (mtpeq t₂ t₁) ≫=maybe λ t →
      just (Sigma posinfo-gen t)
    _ → nothing
elab-check-term Γ (Theta pi θ t ts) T =
  elab-synth-term Γ t ≫=maybe uncurry λ t T' →
  let x = case hnf Γ unfold-head t tt of λ {(Var _ x) → x; _ → "_"} in
  rename x from Γ for λ x' →
  motive x x' T T' θ ≫=maybe λ mtv →
  elab-check-term Γ (lterms-to-term θ (AppTp t mtv) ts) T where
  wrap-var : var → type → maybe type
  wrap-var x T =
    rename x from Γ for λ x' →
    env-lookup Γ x ≫=maybe λ where
      (term-decl T' , loc) → just (mtplam x' (Tkt T') (rename-var Γ x x' T))
      (type-decl k , loc) → just (mtplam x' (Tkk k) (rename-var Γ x x' T))
      (term-def ps _ _ T' , loc) → just (mtplam x' (Tkt T') (rename-var Γ x x' T))
      (type-def ps _ _ k , loc) → just (mtplam x' (Tkk k) (rename-var Γ x x' T))
      _ → nothing
  wrap-vars : vars → type → maybe type
  wrap-vars (VarsStart x) T = wrap-var x  T
  wrap-vars (VarsNext x xs) T = wrap-vars xs T ≫=maybe wrap-var x

  motive : var → var → type → type → theta → maybe type
  motive x x' T T' Abstract = just (mtplam x' (Tkt T') (rename-var Γ x x' T))
  motive x x' T T' AbstractEq = just (mtplam x' (Tkt T') (TpArrow (mtpeq t (mvar x')) Erased (rename-var Γ x x' T)))
  motive x x' T T' (AbstractVars vs) = wrap-vars vs T
elab-check-term Γ (Var pi x) T = just (mvar x)
elab-check-term Γ (Mu pi x t ot pi' cs pi'') T = nothing
elab-check-term Γ (Mu' pi t ot pi' cs pi'')  T = nothing

elab-synth-term Γ (App t me t') =
  elab-app-term  Γ (App t me t') (proto-maybe nothing) tt ≫=maybe uncurry λ where
    tf (mk-spine-data Xs T _) →
      tf Xs ≫=maybe λ t'' →
      elab-hnf-type Γ (meta-vars-subst-type' ff Γ Xs (decortype-to-type T)) tt ≫=maybe λ T →
      just (t'' , T)
elab-synth-term Γ (AppTp t T) =
  elab-synth-term Γ t ≫=maybe uncurry λ t T' →
  elab-hnf-type Γ T' tt ≫=maybe λ where
    (Abs _ _ _ x (Tkk k) T'') →
      elab-type Γ T ≫=maybe uncurry λ T k' →
        just (AppTp t T , subst Γ T x T'')
    _ → nothing
elab-synth-term Γ (Beta pi ot ot') =
  let ot'' = case ot' of λ where NoTerm → just (fresh-id-term Γ); (SomeTerm t _) → elab-pure-term Γ (erase-term t) in
  case ot of λ where
    (SomeTerm t _) →
      elab-pure-term Γ (erase-term t) ≫=maybe λ t →
      ot'' ≫=maybe λ t' →
      just (mbeta t t' , mtpeq t t)
    NoTerm → nothing
elab-synth-term Γ (Chi pi mT t) = case mT of λ where
  NoType → elab-synth-term Γ t
  (SomeType T') →
    let id = fresh-id-term Γ in
    elab-pure-type Γ (erase-type T') ≫=maybe λ T' →
    elab-check-term Γ t T' ≫=maybe λ t →
    just (mrho (mbeta id id) "_" T' t , T')
elab-synth-term Γ (Delta pi mT t) = (case mT of λ where
  NoType → just compileFailType
  (SomeType T) → elab-pure-type Γ (erase-type T)) ≫=maybe λ T →
  elab-synth-term Γ t ≫=maybe uncurry λ where
    t (TpEq _ t1 t2 _) →
      elab-pure-term Γ (erase-term t) ≫=maybe λ pt →
      rename "x" from Γ for λ x →
      rename "y" from Γ for λ y →
      rename "z" from Γ for λ z →
      let ρ = renamectxt-insert (renamectxt-insert (renamectxt-insert empty-renamectxt x x) y y) z z
          tt-term = mlam x (mlam y (mvar x))
          ff-term = mlam x (mlam y (mvar y)) in
      if conv-term Γ t1 tt-term && conv-term Γ t2 ff-term
        then just (Delta posinfo-gen (SomeType T) t , T)
        else
          delta-contra (hnf Γ unfold-head t1 tt) (hnf Γ unfold-head t2 tt) ≫=maybe λ f →
          let f = substh-term {TERM} Γ ρ empty-trie f in
          just (Delta posinfo-gen (SomeType T)
            (mrho t z (mtpeq (mapp f t1) (mapp f (mvar z))) (mbeta tt-term pt)) , T)
    t T → nothing
elab-synth-term Γ (Epsilon pi lr mm t) =
  elab-synth-term Γ t ≫=maybe uncurry λ where
    t (TpEq _ t₁ t₂ _) →
      let id = fresh-id-term Γ
          T = check-term-update-eq Γ lr mm posinfo-gen t₁ t₂ posinfo-gen in
      elab-pure-type Γ T ≫=maybe λ T →
      just (mrho (mbeta id id) "_" T t , T)
    _ _ → nothing
elab-synth-term Γ (Hole pi) = nothing
elab-synth-term Γ (IotaPair pi t₁ t₂ og pi') = case og of λ where
  NoGuide → nothing
  (Guide pi'' x T₂) →
    rename x from Γ for λ x' →
    elab-type (ctxt-var-decl x' Γ) (rename-var Γ x x' T₂) ≫=maybe uncurry λ T₂ k₂ →
    elab-synth-term Γ t₁ ≫=maybe uncurry λ t₁ T₁ →
    elab-check-term Γ t₂ (subst Γ t₁ x' T₂) ≫=maybe λ t₂ →
    just (IotaPair posinfo-gen t₁ t₂ (Guide posinfo-gen x' T₂) posinfo-gen ,
          Iota posinfo-gen posinfo-gen x' T₁ T₂)
elab-synth-term Γ (IotaProj t n pi) =
  elab-synth-term Γ t ≫=maybe uncurry λ where
    t (Iota _ pi' x T₁ T₂) →
      case n of λ where
        "1" → elab-hnf-type Γ T₁ tt ≫=maybe λ T₁ →
              just (IotaProj t n posinfo-gen , T₁)
        "2" → elab-hnf-type Γ (subst Γ (IotaProj t "1" posinfo-gen) x T₂) tt ≫=maybe λ T₂ →
              just (IotaProj t n posinfo-gen , subst Γ (IotaProj t "1" posinfo-gen) x T₂) -- , T₂)
        _ → nothing
    _ _ → nothing
elab-synth-term Γ (Lam pi l pi' x oc t) = (case (l , oc) of λ where
  (Erased , SomeClass atk) → elab-tk Γ atk
  (NotErased , SomeClass (Tkt T)) → elab-tk Γ (Tkt T)
  _ → nothing) ≫=maybe λ atk →
  rename x from Γ for λ x' →
  elab-synth-term (ctxt-tk-decl' pi' x' atk Γ) (rename-var Γ x x' t) ≫=maybe uncurry λ t T →
    just (Lam posinfo-gen l posinfo-gen x' (SomeClass atk) t , Abs posinfo-gen l posinfo-gen x' atk T)
elab-synth-term Γ (Let pi d t) = case d of λ where
  (DefTerm pi' x NoType t') →
    rename x from Γ for λ x' →
    elab-synth-term Γ t' ≫=maybe uncurry λ t' T' →
    elab-synth-term (ctxt-let-term-def pi' x' t' T' Γ) (rename-var Γ x x' t) ≫=maybe uncurry λ t T →
    just (Let posinfo-gen (DefTerm posinfo-gen x' NoType t') t , subst Γ t' x' T)
  (DefTerm pi' x (SomeType T') t') →
    rename x from Γ for λ x' →
    elab-type Γ T' ≫=maybe uncurry λ T' k →
    elab-check-term Γ t' T' ≫=maybe λ t' →
    elab-synth-term (ctxt-let-term-def pi' x' t' T' Γ) (rename-var Γ x x' t) ≫=maybe uncurry λ t T →
    just (Let posinfo-gen (DefTerm posinfo-gen x' NoType t') t , subst Γ t' x' T)
  (DefType pi' x k T') →
    rename x from Γ for λ x' →
    elab-type Γ T' ≫=maybe uncurry λ T' k' →
    elab-synth-term (ctxt-let-type-def pi' x' T' k' Γ) (rename-var Γ x x' t) ≫=maybe uncurry λ t T →
    just (Let posinfo-gen (DefType pi' x' k' T') t , subst Γ T' x' T)
elab-synth-term Γ (Open pi x t) =
  ctxt-clarify-def Γ x ≫=maybe uncurry λ _ Γ →
  elab-synth-term Γ t
elab-synth-term Γ (Parens pi t pi') = elab-synth-term Γ t
elab-synth-term Γ (Phi pi t t₁ t₂ pi') =
  elab-pure-term Γ (erase-term t₁) ≫=maybe λ t₁' →
  elab-pure-term Γ (erase-term t₂) ≫=maybe λ t₂ →
  elab-synth-term Γ t₁ ≫=maybe uncurry λ t₁ T →
  elab-check-term Γ t (mtpeq t₁' t₂) ≫=maybe λ t →
  just (Phi posinfo-gen t t₁ t₂ posinfo-gen , T)
elab-synth-term Γ (Rho pi op on t og t') =
  elab-synth-term Γ t ≫=maybe uncurry λ t T →
  elab-synth-term Γ t' ≫=maybe uncurry λ t' T' →
  elab-hnf-type Γ (erase-type T) ff ≫=maybe λ where
    (TpEq _ t₁ t₂ _) → case og of λ where
      NoGuide →
        rename "x" from Γ for λ x →
        let ns = fst (optNums-to-stringset on)
            Γ' = ctxt-var-decl x Γ
            rT = fst (rewrite-type T' Γ' (is-rho-plus op) ns t t₁ x 0)
            rT' = post-rewrite Γ' x t t₂ rT in
        -- elab-hnf-type Γ rT' tt ≫=maybe λ rT' →
        just (mrho t x (erase-type rT) t' , rT')
      (Guide pi' x T'') →
        let Γ' = ctxt-var-decl x Γ in
        elab-pure-type Γ' (erase-type T'') ≫=maybe λ T'' →
        just (mrho t x T'' t' , post-rewrite Γ' x t t₂ (rewrite-at Γ' x t tt T' T''))
    _ → nothing
elab-synth-term Γ (Sigma pi t) =
  elab-synth-term Γ t ≫=maybe uncurry λ where
    t (TpEq _ t₁ t₂ _) → just (Sigma posinfo-gen t , mtpeq t₂ t₁)
    _ _ → nothing
elab-synth-term Γ (Theta pi θ t ts) = nothing
elab-synth-term Γ (Var pi x) =
  ctxt-lookup-term-var' Γ x ≫=maybe λ T →
  elab-hnf-type Γ T tt ≫=maybe λ T →
  just (mvar x , T)
elab-synth-term Γ (Mu pi x t ot pi' cs pi'') = nothing
elab-synth-term Γ (Mu' pi t ot pi' cs pi'')  = nothing

elab-typeh Γ (Abs pi b pi' x atk T) b' =
  elab-tkh Γ atk b' ≫=maybe λ atk →
  rename x from Γ for λ x' →
  elab-typeh (ctxt-tk-decl' pi' x' atk Γ) (rename-var Γ x x' T) b' ≫=maybe uncurry λ T k →
  just (Abs posinfo-gen b posinfo-gen x' atk T , star)
elab-typeh Γ (Iota pi pi' x T T') b =
  elab-typeh Γ T b ≫=maybe uncurry λ T k →
  rename x from Γ for λ x' →
  elab-typeh (ctxt-term-decl' pi' x' T Γ) (rename-var Γ x x' T') b ≫=maybe uncurry λ T' k' →
  just (Iota posinfo-gen posinfo-gen x' T T' , star)
elab-typeh Γ (Lft pi pi' x t lT) b = nothing
elab-typeh Γ (NoSpans T pi) b = nothing
elab-typeh Γ (TpApp T T') b =
  elab-typeh Γ T b ≫=maybe uncurry λ T k →
  elab-typeh Γ T' b ≫=maybe uncurry λ T' k' →
  case k of λ where
    (KndPi _ pi x (Tkk _) k'') → just (TpApp T T' , subst Γ T' x k'')
    _ → nothing
elab-typeh Γ (TpAppt T t) b =
  elab-typeh Γ T b ≫=maybe uncurry λ where
    T (KndPi _ pi x (Tkt T') k) →
      (if b then elab-check-term Γ t T' else elab-pure-term Γ (erase-term t)) ≫=maybe λ t →
      just (TpAppt T t , subst Γ t x k)
    _ _ → nothing
elab-typeh Γ (TpArrow T a T') b =
  elab-typeh Γ T b ≫=maybe uncurry λ T k →
  elab-typeh Γ T' b ≫=maybe uncurry λ T' k' →
  just (Abs posinfo-gen a posinfo-gen "_" (Tkt T) T' , star)
elab-typeh Γ (TpEq pi t t' pi') b =
  elab-pure-term Γ (erase-term t) ≫=maybe λ t →
  elab-pure-term Γ (erase-term t') ≫=maybe λ t' →
  just (mtpeq t t' , star)
elab-typeh Γ (TpHole pi) b = nothing
elab-typeh Γ (TpLambda pi pi' x atk T) b =
  elab-tkh Γ atk b ≫=maybe λ atk →
  rename x from Γ for λ x' →
  elab-typeh (ctxt-tk-decl' pi' x' atk Γ) (rename-var Γ x x' T) b ≫=maybe uncurry λ T k →
  just (mtplam x' atk T , KndPi posinfo-gen posinfo-gen x' atk k)
elab-typeh Γ (TpParens pi T pi') b = elab-typeh Γ T b
elab-typeh Γ (TpVar pi x) b =
  ctxt-lookup-type-var' Γ x ≫=maybe λ k →
  elab-kindh Γ k b ≫=maybe λ k →
  just (mtpvar x , k)
elab-typeh Γ (TpLet pi (DefTerm pi' x ot t) T) = elab-typeh Γ (subst Γ (Chi posinfo-gen ot t) x T)
elab-typeh Γ (TpLet pi (DefType pi' x k T') T) = elab-typeh Γ (subst Γ T' x T)

elab-kindh Γ (KndArrow k k') b =
  elab-kindh Γ k b ≫=maybe λ k →
  elab-kindh Γ k' b ≫=maybe λ k' →
  just (KndPi posinfo-gen posinfo-gen "_" (Tkk k) k')
elab-kindh Γ (KndParens pi k pi') b = elab-kindh Γ k b
elab-kindh Γ (KndPi pi pi' x atk k) b =
  elab-tkh Γ atk b ≫=maybe λ atk →
  rename x from Γ for λ x' →
  elab-kindh (ctxt-tk-decl' pi' x' atk Γ) (rename-var Γ x x' k) b ≫=maybe λ k →
  just (KndPi posinfo-gen posinfo-gen x' atk k)
elab-kindh Γ (KndTpArrow T k) b =
  elab-typeh Γ T b ≫=maybe uncurry λ T _ →
  elab-kindh Γ k b ≫=maybe λ k →
  just (KndPi posinfo-gen posinfo-gen "_" (Tkt T) k)
elab-kindh Γ (KndVar pi x as) b =
  ctxt-lookup-kind-var-def Γ x ≫=maybe uncurry (do-subst as)
  where
  do-subst : args → params → kind → maybe kind
  do-subst (ArgsCons (TermArg _ t) ys) (ParamsCons (Decl _ _ _ x _ _) ps) k = do-subst ys ps (subst Γ t x k)
  do-subst (ArgsCons (TypeArg t) ys) (ParamsCons (Decl _ _ _ x _ _) ps) k = do-subst ys ps (subst Γ t x k)
  do-subst ArgsNil ParamsNil k = elab-kindh Γ k b
  do-subst _ _ _ = nothing
elab-kindh Γ (Star pi) b = just star

elab-tkh Γ (Tkt T) b = elab-typeh Γ T b ≫=maybe uncurry λ T _ → just (Tkt T)
elab-tkh Γ (Tkk k) b = elab-kindh Γ k b ≫=maybe λ k → just (Tkk k)

elab-pure-term Γ (Var pi x) = just (mvar x)
elab-pure-term Γ (App t NotErased t') =
  elab-pure-term Γ t ≫=maybe λ t →
  elab-pure-term Γ t' ≫=maybe λ t' →
  just (App t NotErased t')
elab-pure-term Γ (Lam pi NotErased pi' x NoClass t) =
  rename x from Γ for λ x' →
  elab-pure-term (ctxt-var-decl x' Γ) (rename-var Γ x x' t) ≫=maybe λ t →
  just (mlam x' t)
elab-pure-term Γ (Let pi (DefTerm pi' x NoType t) t') =
  elab-pure-term Γ t ≫=maybe λ t →
  elab-pure-term Γ (subst Γ t x t')
elab-pure-term _ _ = nothing -- should be erased

elab-app-term Γ (App t me t') pt max =
  elab-app-term Γ t (proto-arrow me pt) ff ≫=maybe uncurry λ where
    tf (mk-spine-data Xs dt locl) →
      case fst (meta-vars-unfold-tmapp' Γ ("" , "" , "") Xs dt Γ id-spans.empty-spans) of uncurry λ where
        Ys (not-tpabsd _) → nothing
        Ys (inj₂ arr) →
          elab-app-term' Xs Ys t t' arr (islocl locl) ≫=maybe uncurry λ where
            t' (check-term-app-return Xs' Tᵣ arg-mode _) →
              fst (check-spine-locality Γ Xs' (decortype-to-type Tᵣ) max (pred locl) Γ id-spans.empty-spans) ≫=maybe uncurry' λ Xs'' locl' is-loc →
              just ((λ Xs → tf (if is-loc then Xs' else Xs) ≫=maybe λ t → fill-meta-vars t (if is-loc then Xs' else Xs) Ys ≫=maybe λ t → just (App t me t')) ,
                    mk-spine-data Xs'' Tᵣ locl')
  where
  islocl = (max ||_) ∘ (iszero ∘ pred)
  fill-meta-vars : term → meta-vars → 𝕃 meta-var → maybe term
  fill-meta-vars t Xs = flip foldl (just t) λ where
    (meta-var-mk x _ _) tₘ → tₘ ≫=maybe λ t → meta-vars-lookup Xs x ≫=maybe λ where
      (meta-var-mk _ (meta-var-tp k Tₘ) _) → Tₘ ≫=maybe λ T → just (AppTp t (meta-var-sol.sol T))
      (meta-var-mk _ (meta-var-tm T tₘ) _) → nothing

  elab-app-term' : (Xs : meta-vars) → (Ys : 𝕃 meta-var) → (t₁ t₂ : term) → is-tmabsd → 𝔹 → maybe (term × check-term-app-ret)
  elab-app-term' Xs Zs t₁ t₂ (mk-tmabsd dt me x dom occurs cod) is-locl =
    let Xs' = meta-vars-add* Xs Zs
        T = decortype-to-type dt in
    if ~ meta-vars-are-free-in-type Xs' dom
      then (elab-check-term Γ t₂ dom ≫=maybe λ t₂ →
            let rdt = fst $ subst-decortype Γ t₂ x cod Γ id-spans.empty-spans in
            just (t₂ , check-term-app-return Xs' (if occurs then rdt else cod) checking []))
      else (elab-synth-term Γ t₂ ≫=maybe uncurry λ t₂ T₂ →
            case fst (match-types Xs' empty-trie match-unfolding-both dom T₂ Γ id-spans.empty-spans) of λ where
              (match-error _) → nothing
              (match-ok Xs) →
                let rdt = fst $ subst-decortype Γ t₂ x cod Γ id-spans.empty-spans
                    rdt' = fst $ meta-vars-subst-decortype Γ Xs (if occurs then rdt else cod) Γ id-spans.empty-spans in
                just (t₂ , check-term-app-return Xs rdt' synthesizing []))

elab-app-term Γ (AppTp t T) pt max =
  elab-app-term Γ t pt max ≫=maybe uncurry λ where
    tf (mk-spine-data Xs dt locl) →
      let Tₕ = decortype-to-type dt in
      case fst (meta-vars-unfold-tpapp' Γ Xs dt Γ id-spans.empty-spans) of λ where
        (not-tpabsd _) → nothing
        (yes-tpabsd dt me x k sol rdt) →
          elab-type Γ T ≫=maybe uncurry λ T k' →
          just ((λ Xs → tf Xs ≫=maybe λ t → just (AppTp t T)) ,
            mk-spine-data Xs (fst $ subst-decortype Γ T x rdt Γ id-spans.empty-spans) locl)

elab-app-term Γ (Parens _ t _) pt max =
  elab-app-term Γ t pt max

elab-app-term Γ t pt max =
  elab-synth-term Γ t ≫=maybe uncurry λ t T →
  let locl = num-arrows-in-type Γ T
      ret = fst $ match-prototype meta-vars-empty ff T pt Γ id-spans.empty-spans
      dt = match-prototype-data.match-proto-dectp ret in
  just ((λ Xs → just t) , mk-spine-data meta-vars-empty dt locl)

{- ################################ IO ###################################### -}

private
  ie-set-span-ast : include-elt → ctxt → start → include-elt
  ie-set-span-ast ie Γ ast = record ie
    {ss = inj₁ (regular-spans nothing
      [ mk-span "" "" "" [ "" , strRun Γ (file-to-string ast) , [] ] nothing ])}

  ie-get-span-ast : include-elt → maybe rope
  ie-get-span-ast ie with include-elt.ss ie
  ...| inj₁ (regular-spans nothing (mk-span "" "" ""
         (("" , r , []) :: []) nothing :: [])) = just r
  ...| _ = nothing

elab-t : Set → Set
elab-t X = toplevel-state → (var-mapping file-mapping : renamectxt) → trie encoded-datatype →
             X → maybe (X × toplevel-state × renamectxt × renamectxt × trie encoded-datatype)

{-# TERMINATING #-}
elab-file' : elab-t string
elab-cmds : elab-t cmds
elab-params : elab-t params
elab-args : elab-t (args × params)
elab-imports : elab-t imports

elab-params ts ρ φ μ ParamsNil = just (ParamsNil , ts , ρ , φ , μ)
elab-params ts ρ φ μ (ParamsCons (Decl _ pi me x atk _) ps) =
  let Γ = toplevel-state.Γ ts in
  elab-tk Γ (subst-qualif Γ ρ atk) ≫=maybe λ atk →
  rename x - x from ρ for λ x' ρ →
  elab-params (record ts {Γ = ctxt-param-decl x x' atk Γ}) ρ φ μ ps ≫=maybe uncurry λ ps ω →
  just (ParamsCons (Decl posinfo-gen posinfo-gen me x' atk posinfo-gen) ps , ω)

elab-args ts ρ φ μ (ArgsNil , ParamsNil) = just ((ArgsNil , ParamsNil) , ts , ρ , φ , μ)
elab-args ts ρ φ μ (_ , ParamsNil) = nothing -- Too many arguments
elab-args ts ρ φ μ (ArgsNil , ParamsCons p ps) = just ((ArgsNil , ParamsCons p ps) , ts , ρ , φ , μ)
elab-args ts ρ φ μ (ArgsCons a as , ParamsCons (Decl _ _ me x atk _) ps) =
  let Γ = toplevel-state.Γ ts in
  case (a , atk) of λ where
    (TermArg me' t , Tkt T) →
      elab-type Γ (subst-qualif Γ ρ T) ≫=maybe uncurry λ T k →
      elab-check-term Γ (subst-qualif Γ ρ t) T ≫=maybe λ t →
      rename qualif-new-var Γ x - x lookup ρ for λ x' ρ →
      let ts = record ts {Γ = ctxt-term-def' x x' t T OpacTrans Γ} in
      elab-args ts ρ φ μ (as , ps) ≫=maybe (uncurry ∘ uncurry) λ as ps ω →
      just ((ArgsCons (TermArg me' t) as , ParamsCons (Decl posinfo-gen posinfo-gen me x' (Tkt T) posinfo-gen) ps) , ω)
    (TypeArg T , Tkk _) →
      elab-type Γ (subst-qualif Γ ρ T) ≫=maybe uncurry λ T k →
      rename qualif-new-var Γ x - x lookup ρ for λ x' ρ →
      let ts = record ts {Γ = ctxt-type-def' x x' T k OpacTrans Γ} in
      elab-args ts ρ φ μ (as , ps) ≫=maybe (uncurry ∘ uncurry) λ as ps ω →
      just ((ArgsCons (TypeArg T) as , ParamsCons (Decl posinfo-gen posinfo-gen me x' (Tkk k) posinfo-gen) ps) , ω)
    _ → nothing

elab-imports ts ρ φ μ ImportsStart = just (ImportsStart , ts , ρ , φ , μ)
elab-imports ts ρ φ μ (ImportsNext (Import _ op _ ifn oa as _) is) =
  let Γ = toplevel-state.Γ ts
      fn = ctxt-get-current-filename Γ
      mod = ctxt-get-current-mod Γ in
  get-include-elt-if ts fn ≫=maybe λ ie →
  trie-lookup (include-elt.import-to-dep ie) ifn ≫=maybe λ ifn' →
  elab-file' ts ρ φ μ ifn' ≫=maybe uncurry''' λ fn ts ρ φ μ →
  lookup-mod-params (toplevel-state.Γ ts) ifn' ≫=maybe λ ps →
  elab-args ts ρ φ μ (as , ps) ≫=maybe (uncurry''' ∘ uncurry) λ as ps ts ρ φ μ →
  elim-pair (scope-file (record ts {Γ = ctxt-set-current-mod (toplevel-state.Γ ts) mod}) fn ifn' oa as) λ ts _ →
  elab-imports ts ρ φ μ is ≫=maybe uncurry''' λ is ts ρ φ μ →
  add-imports ts φ (stringset-strings $ get-all-deps ifn' empty-stringset) (just is) ≫=maybe λ is →
  let i = Import posinfo-gen NotPublic posinfo-gen fn NoOptAs ArgsNil posinfo-gen in
  just (ImportsNext i is , ts , ρ , φ , μ)
  where
  get-all-deps : filepath → stringset → stringset
  get-all-deps fp fs = maybe-else fs (foldr get-all-deps $ stringset-insert fs fp)
    ((maybe-not $ trie-lookup fs fp) ≫=maybe λ _ →
     get-include-elt-if ts fp ≫=maybe
     (just ∘ include-elt.deps))
  add-imports : toplevel-state → renamectxt → 𝕃 string → maybe imports → maybe imports
  add-imports ts φ = flip $ foldl λ fn isₘ → renamectxt-lookup φ fn ≫=maybe λ ifn → isₘ ≫=maybe
    (just ∘ ImportsNext (Import posinfo-gen NotPublic posinfo-gen ifn NoOptAs ArgsNil posinfo-gen))

elab-cmds ts ρ φ μ CmdsStart = just (CmdsStart , ts , ρ , φ , μ)
elab-cmds ts ρ φ μ (CmdsNext (DefTermOrType op (DefTerm _ x NoType t) _) cs) =
  let Γ = toplevel-state.Γ ts in
  elab-synth-term Γ (subst-qualif Γ ρ t) ≫=maybe uncurry λ t T →
  rename qualif-new-var Γ x - x from ρ for λ x' ρ →
  let ts = record ts {Γ = ctxt-term-def' x x' t T op Γ} in
  elab-cmds ts ρ φ μ cs ≫=maybe uncurry λ cs ω →
  just (CmdsNext (DefTermOrType OpacTrans (DefTerm posinfo-gen x' NoType t) posinfo-gen) cs , ω)
elab-cmds ts ρ φ μ (CmdsNext (DefTermOrType op (DefTerm _ x (SomeType T) t) _) cs) =
  let Γ = toplevel-state.Γ ts in
  elab-type Γ (subst-qualif Γ ρ T) ≫=maybe uncurry λ T k →
  elab-check-term Γ (subst-qualif Γ ρ t) T ≫=maybe λ t →
  rename qualif-new-var Γ x - x from ρ for λ x' ρ →
  let ts = record ts {Γ = ctxt-term-def' x x' t T op Γ} in
  elab-cmds ts ρ φ μ cs ≫=maybe uncurry λ cs ω →
  just (CmdsNext (DefTermOrType OpacTrans (DefTerm posinfo-gen x' NoType t) posinfo-gen) cs , ω)
elab-cmds ts ρ φ μ (CmdsNext (DefTermOrType op (DefType _ x _ T) _) cs) =
  let Γ = toplevel-state.Γ ts in
  elab-type Γ (subst-qualif Γ ρ T) ≫=maybe uncurry λ T k →
  rename qualif-new-var Γ x - x from ρ for λ x' ρ →
  let ts = record ts {Γ = ctxt-type-def' x x' T k op Γ} in
  elab-cmds ts ρ φ μ cs ≫=maybe uncurry λ cs ω →
  just (CmdsNext (DefTermOrType OpacTrans (DefType posinfo-gen x' k T) posinfo-gen) cs , ω)
elab-cmds ts ρ φ μ (CmdsNext (DefKind _ x ps k _) cs) =
  let Γ = toplevel-state.Γ ts
      x' = fresh-var (qualif-new-var Γ x) (λ _ → ff) ρ
      ρ = renamectxt-insert ρ x x'
      ts = record ts {Γ = ctxt-kind-def' x x' ps k Γ} in
  elab-cmds ts ρ φ μ cs
elab-cmds ts ρ φ μ (CmdsNext (ImportCmd i) cs) =
  elab-imports ts ρ φ μ (ImportsNext i ImportsStart) ≫=maybe uncurry''' λ is ts ρ φ μ →
  elab-cmds ts ρ φ μ cs ≫=maybe uncurry λ cs ω →
  just (append-cmds (imps-to-cmds is) cs , ω)
elab-cmds ts ρ φ μ (CmdsNext (DefDatatype (Datatype pi pi' x ps k dcs pi'') _) cs) =
  let Γ = toplevel-state.Γ ts
      x' = rename qualif-new-var Γ x - x from ρ for λ x' ρ' → x'
      -- Still need to use x (not x') so constructors work,
      -- but we need to know what it will be renamed to later for μ
      d = defDatatype-to-datatype Γ (Datatype pi pi' x ps k dcs pi'') in
  elim-pair (datatype-encoding.mk-defs selected-encoding Γ d) λ cs' d →
  elab-cmds ts ρ φ (trie-insert μ x' d) (append-cmds cs' cs)

elab-file' ts ρ φ μ fn =
  get-include-elt-if ts fn ≫=maybe λ ie →
  case include-elt.need-to-add-symbols-to-context ie of λ where
    ff → rename fn - base-filename (takeFileName fn) lookup φ for λ fn' φ → just (fn' , ts , ρ , φ , μ)
    tt → include-elt.ast ie ≫=maybe λ where
      (File _ is _ _ mn ps cs _) →
        rename fn - base-filename (takeFileName fn) from φ for λ fn' φ →
        let ie = record ie {need-to-add-symbols-to-context = ff; do-type-check = ff; inv = refl} in
        elab-imports (record (set-include-elt ts fn ie)
          {Γ = ctxt-set-current-file (toplevel-state.Γ ts) fn mn}) ρ φ μ is ≫=maybe uncurry''' λ is ts ρ φ μ →
        elab-params ts ρ φ μ ps ≫=maybe uncurry''' λ ps' ts ρ φ μ →
        let Γ = toplevel-state.Γ ts
            Γ = ctxt-add-current-params (ctxt-set-current-mod Γ (fn , mn , ps' , ctxt-get-qualif Γ)) in
        elab-cmds (record ts {Γ = Γ}) ρ φ μ cs ≫=maybe uncurry' λ cs ts ω →
        let ast = File posinfo-gen ImportsStart posinfo-gen posinfo-gen mn ParamsNil
                    (remove-dup-imports empty-stringset (append-cmds (imps-to-cmds is) cs)) posinfo-gen in
        just (fn' , set-include-elt ts fn (ie-set-span-ast ie (toplevel-state.Γ ts) ast) , ω)
  where
  remove-dup-imports : stringset → cmds → cmds
  remove-dup-imports is CmdsStart = CmdsStart
  remove-dup-imports is (CmdsNext c @ (ImportCmd (Import _ _ _ fp _ _ _)) cs) =
    if stringset-contains is fp
      then remove-dup-imports is cs
      else CmdsNext c (remove-dup-imports (stringset-insert is fp) cs)
  remove-dup-imports is (CmdsNext c cs) = CmdsNext c $ remove-dup-imports is cs

{-# TERMINATING #-}
elab-all : toplevel-state → (from-fp to-fp : string) → IO ⊤
elab-all ts fm to =
  elab-file' prep-ts empty-renamectxt empty-renamectxt empty-trie fm err-code 1 else h
  where
  _err-code_else_ : ∀ {X : Set} → maybe X → ℕ → (X → IO ⊤) → IO ⊤
  nothing err-code n else f = putStrLn (ℕ-to-string n)
  just x err-code n else f = f x

  prep-ts : toplevel-state
  prep-ts = record ts
    {Γ = new-ctxt fm "[unknown]";
     is = trie-map (λ ie → record ie
         {need-to-add-symbols-to-context = tt;
          do-type-check = ff;
          inv = refl})
       (toplevel-state.is ts)}

  get-file-imports : toplevel-state → (filename : string) → stringset → maybe stringset
  get-file-imports ts fn is =
    get-include-elt-if ts fn ≫=maybe λ ie →
    foldr
      (λ fn' is → if fn =string fn' then is else
        (is ≫=maybe λ is →
        get-file-imports ts fn' is ≫=maybe λ is →
        just (stringset-insert is fn')))
      (just is)
      (include-elt.deps ie)

  h : (string × toplevel-state × renamectxt × renamectxt × trie encoded-datatype) → IO ⊤
  h' : toplevel-state → renamectxt → stringset → IO ⊤
  h (_ , ts , _ , φ , μ) =
    get-file-imports ts fm (trie-single fm triv) err-code 3 else h' ts φ
  h' ts φ is = foldr
    (λ fn x → x >>= λ e →
      maybe-else
        (return ff)
        (uncurry λ fn ie →
          writeRopeToFile (combineFileNames to fn ^ ".ced")
            (maybe-else [[ "Error lookup up elaborated data" ]] id (ie-get-span-ast ie)) >>
          return e)
      (renamectxt-lookup φ fn ≫=maybe λ fn' →
       get-include-elt-if ts fn ≫=maybe λ ie →
       include-elt.ast ie ≫=maybe λ ast → just (fn' , ie)))
    (createDirectoryIfMissing tt to >> return tt)
    (stringset-strings is) >>= λ e →
    putStrLn (if e then "0" else "2")

elab-file : toplevel-state → (filename : string) → maybe rope
elab-file ts fn =
  elab-file' ts empty-renamectxt empty-renamectxt empty-trie fn ≫=maybe uncurry'' λ fn' ts ρ φ →
  get-include-elt-if ts fn ≫=maybe ie-get-span-ast

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
module Structure.Operator.Proofs.Util where

import Lvl
open import Data
open import Data.Tuple
open import Functional hiding (id)
open import Function.Equals
import      Function.Names as Names
import      Lang.Vars.Structure.Operator
open        Lang.Vars.Structure.Operator.Select
open import Logic.IntroInstances
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Function.Domain
import      Structure.Operator.Names as Names
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type

module One {ℓ ℓₑ} {T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ {_▫_ : T → T → T} where
  open Lang.Vars.Structure.Operator.One ⦃ equiv = equiv ⦄ {_▫_ = _▫_}

  -- TODO: Rename this to associate-commute4-commuting
  associate-commute4 : let _ = op , assoc in ∀{a b c d} → Names.Commuting(_▫_)(b)(c) → ((a ▫ b) ▫ (c ▫ d) ≡ (a ▫ c) ▫ (b ▫ d))
  associate-commute4 {a}{b}{c}{d} com =
    (a ▫ b) ▫ (c ▫ d) 🝖-[ symmetry(_≡_) (associativity(_▫_) {a ▫ b} {c} {d}) ]
    ((a ▫ b) ▫ c) ▫ d 🝖-[ congruence₂ₗ(_▫_)(d) (associativity(_▫_) {a} {b} {c}) ]
    (a ▫ (b ▫ c)) ▫ d 🝖-[ (congruence₂ₗ(_▫_)(d) ∘ congruence₂ᵣ(_▫_)(a)) com ]
    (a ▫ (c ▫ b)) ▫ d 🝖-[ associativity(_▫_) {a} {c ▫ b} {d} ]
    a ▫ ((c ▫ b) ▫ d) 🝖-[ congruence₂ᵣ(_▫_)(a) (associativity(_▫_) {c} {b} {d}) ]
    a ▫ (c ▫ (b ▫ d)) 🝖-[ symmetry(_≡_) (associativity(_▫_) {a} {c} {b ▫ d}) ]
    (a ▫ c) ▫ (b ▫ d) 🝖-end

  -- TODO: Rename this to associate-commute4
  associate-commute4-c : let _ = op , assoc , comm in ∀{a b c d} → ((a ▫ b) ▫ (c ▫ d) ≡ (a ▫ c) ▫ (b ▫ d))
  associate-commute4-c = associate-commute4(commutativity(_▫_))

  associate4-123-321 : let _ = op , assoc in ∀{a b c d} → (((a ▫ b) ▫ c) ▫ d ≡ a ▫ (b ▫ (c ▫ d)))
  associate4-123-321 {a}{b}{c}{d} = associativity(_▫_) 🝖 associativity(_▫_)

  associate4-123-213 : let _ = op , assoc in ∀{a b c d} → (((a ▫ b) ▫ c) ▫ d ≡ (a ▫ (b ▫ c)) ▫ d)
  associate4-123-213 {a}{b}{c}{d} = congruence₂ₗ(_▫_)(_) (associativity(_▫_))

  associate4-321-231 : let _ = op , assoc in ∀{a b c d} → (a ▫ (b ▫ (c ▫ d)) ≡ a ▫ ((b ▫ c) ▫ d))
  associate4-321-231 {a}{b}{c}{d} = congruence₂ᵣ(_▫_)(_) (symmetry(_≡_) (associativity(_▫_)))

  associate4-231-222 : let _ = op , assoc in ∀{a b c d} → (a ▫ ((b ▫ c) ▫ d) ≡ (a ▫ b) ▫ (c ▫ d))
  associate4-231-222 {a}{b}{c}{d} = symmetry(_≡_) associate4-321-231 🝖 symmetry(_≡_) associate4-123-321 🝖 associativity(_▫_)

  associate4-213-222 : let _ = op , assoc in ∀{a b c d} → ((a ▫ (b ▫ c)) ▫ d ≡ (a ▫ b) ▫ (c ▫ d))
  associate4-213-222 {a}{b}{c}{d} = associativity(_▫_) 🝖 associate4-231-222

  commuteᵣ-assocₗ : let _ = op , assoc , comm in ∀{a b c} → (((a ▫ b) ▫ c) ≡ ((a ▫ c) ▫ b))
  commuteᵣ-assocₗ {a}{b}{c} =
    (a ▫ b) ▫ c 🝖-[ associativity(_▫_) ]
    a ▫ (b ▫ c) 🝖-[ congruence₂ᵣ(_▫_)(_) (commutativity(_▫_)) ]
    a ▫ (c ▫ b) 🝖-[ associativity(_▫_) ]-sym
    (a ▫ c) ▫ b 🝖-end

  commuteₗ-assocᵣ : let _ = op , assoc , comm in ∀{a b c} → ((a ▫ (b ▫ c)) ≡ (b ▫ (a ▫ c)))
  commuteₗ-assocᵣ {a}{b}{c} =
    a ▫ (b ▫ c) 🝖-[ associativity(_▫_) ]-sym
    (a ▫ b) ▫ c 🝖-[ congruence₂ₗ(_▫_)(_) (commutativity(_▫_)) ]
    (b ▫ a) ▫ c 🝖-[ associativity(_▫_) ]
    b ▫ (a ▫ c) 🝖-end

  commuteᵣ-assocᵣ : let _ = op , assoc , comm in ∀{a b c} → ((a ▫ (b ▫ c)) ≡ ((a ▫ c) ▫ b))
  commuteᵣ-assocᵣ = symmetry(_≡_) (associativity(_▫_)) 🝖 commuteᵣ-assocₗ

  -- TODO: Rename and generalize this (See commuteBoth in Structure.Operator.Properties)
  commuteBothTemp : let _ = comm in ∀{a₁ a₂ b₁ b₂} → (a₁ ▫ a₂ ≡ b₁ ▫ b₂) → (a₂ ▫ a₁ ≡ b₂ ▫ b₁)
  commuteBothTemp {a₁} {a₂} {b₁} {b₂} p =
    a₂ ▫ a₁ 🝖-[ commutativity(_▫_) ]-sym
    a₁ ▫ a₂ 🝖-[ p ]
    b₁ ▫ b₂ 🝖-[ commutativity(_▫_) ]
    b₂ ▫ b₁ 🝖-end

  moveₗ-to-inv : let _ = op , assoc , select-invₗ(idₗ)(identₗ)(invₗ)(inverₗ) in ∀{a b c} → (a ▫ b ≡ c) → (b ≡ invₗ(a) ▫ c)
  moveₗ-to-inv {idₗ = idₗ} {invₗ = invₗ} {a = a} {b} {c} abc =
    b                🝖-[ identityₗ(_▫_)(idₗ) ]-sym
    idₗ ▫ b          🝖-[ congruence₂ₗ(_▫_)(b) (inverseFunctionₗ(_▫_)(invₗ)) ]-sym
    (invₗ a ▫ a) ▫ b 🝖-[ associativity(_▫_) ]
    invₗ a ▫ (a ▫ b) 🝖-[ congruence₂ᵣ(_▫_)(invₗ a) abc ]
    invₗ a ▫ c       🝖-end

  moveᵣ-to-inv : let _ = op , assoc , select-invᵣ(idᵣ)(identᵣ)(invᵣ)(inverᵣ) in ∀{a b c} → (a ▫ b ≡ c) → (a ≡ c ▫ invᵣ(b))
  moveᵣ-to-inv {idᵣ = idᵣ} {invᵣ = invᵣ} {a = a} {b} {c} abc =
    a                🝖-[ identityᵣ(_▫_)(idᵣ) ]-sym
    a ▫ idᵣ          🝖-[ congruence₂ᵣ(_▫_)(a) (inverseFunctionᵣ(_▫_)(invᵣ)) ]-sym
    a ▫ (b ▫ invᵣ b) 🝖-[ associativity(_▫_) ]-sym
    (a ▫ b) ▫ invᵣ b 🝖-[ congruence₂ₗ(_▫_)(invᵣ b) abc ]
    c ▫ invᵣ b       🝖-end

  moveₗ-from-inv : let _ = op , assoc , select-idₗ(id)(identₗ) , select-invᵣ(id)(identᵣ)(invᵣ)(inverᵣ) in ∀{a b c} → (a ▫ b ≡ c) ← (b ≡ invᵣ(a) ▫ c)
  moveₗ-from-inv {id = id} {invᵣ = invᵣ} {a = a} {b} {c} bac =
    a ▫ b            🝖-[ congruence₂ᵣ(_▫_)(a) bac ]
    a ▫ (invᵣ a ▫ c) 🝖-[ associativity(_▫_) ]-sym
    (a ▫ invᵣ a) ▫ c 🝖-[ congruence₂ₗ(_▫_)(c) (inverseFunctionᵣ(_▫_)(invᵣ)) ]
    id ▫ c           🝖-[ identityₗ(_▫_)(id) ]
    c                🝖-end

  moveᵣ-from-inv : let _ = op , assoc , select-idᵣ(id)(identᵣ) , select-invₗ(id)(identₗ)(invₗ)(inverₗ) in ∀{a b c} → (a ▫ b ≡ c) ← (a ≡ c ▫ invₗ(b))
  moveᵣ-from-inv {id = id} {invₗ = invₗ} {a = a} {b} {c} acb =
    a ▫ b            🝖-[ congruence₂ₗ(_▫_)(b) acb ]
    (c ▫ invₗ b) ▫ b 🝖-[ associativity(_▫_) ]
    c ▫ (invₗ b ▫ b) 🝖-[ congruence₂ᵣ(_▫_)(c) (inverseFunctionₗ(_▫_)(invₗ)) ]
    c ▫ id           🝖-[ identityᵣ(_▫_)(id) ]
    c                🝖-end

module OneTypeTwoOp {ℓ ℓₑ} {T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ {_▫₁_ _▫₂_ : T → T → T} where
  open Lang.Vars.Structure.Operator.OneTypeTwoOp ⦃ equiv = equiv ⦄ {_▫₁_ = _▫₁_} {_▫₂_ = _▫₂_}

  cross-distribute : let _ = op₂ , distriₗ , distriᵣ in ∀{a b c d} → (a ▫₂ b) ▫₁ (c ▫₂ d) ≡ ((a ▫₁ c) ▫₂ (b ▫₁ c)) ▫₂ ((a ▫₁ d) ▫₂ (b ▫₁ d))
  cross-distribute {a = a}{b}{c}{d} =
    (a ▫₂ b) ▫₁ (c ▫₂ d)                             🝖-[ distributivityₗ(_▫₁_)(_▫₂_) ]
    ((a ▫₂ b) ▫₁ c) ▫₂ ((a ▫₂ b) ▫₁ d)               🝖-[ congruence₂(_▫₂_) (distributivityᵣ(_▫₁_)(_▫₂_)) (distributivityᵣ(_▫₁_)(_▫₂_)) ]
    ((a ▫₁ c) ▫₂ (b ▫₁ c)) ▫₂ ((a ▫₁ d) ▫₂ (b ▫₁ d)) 🝖-end

  moveₗ-to-invOp : let _ = op₂ , inverOpₗ in ∀{a b c} → (a ▫₁ b ≡ c) → (b ≡ a ▫₂ c)
  moveₗ-to-invOp {a = a} {b} {c} abc =
    b             🝖[ _≡_ ]-[ inverseOperₗ(_▫₁_)(_▫₂_) ]-sym
    a ▫₂ (a ▫₁ b) 🝖[ _≡_ ]-[ congruence₂ᵣ(_▫₂_)(a) abc ]
    a ▫₂ c        🝖-end

  moveᵣ-to-invOp : let _ = op₂ , inverOpᵣ in ∀{a b c} → (a ▫₁ b ≡ c) → (a ≡ c ▫₂ b)
  moveᵣ-to-invOp {a = a} {b} {c} abc =
    a             🝖[ _≡_ ]-[ inverseOperᵣ(_▫₁_)(_▫₂_) ]-sym
    (a ▫₁ b) ▫₂ b 🝖[ _≡_ ]-[ congruence₂ₗ(_▫₂_)(b) abc ]
    c ▫₂ b        🝖-end

ext: agda

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 -v tc.size:100 #-}

module SizedTypesMergeSort where

open import Common.Size
open import Common.Prelude using (Bool; true; false; if_then_else_)
open import Common.Product

module Old where

  -- sized lists

  data List (A : Set) : {_ : Size} -> Set where
    []   : {size : Size} -> List A {↑ size}
    _::_ : {size : Size} -> A -> List A {size} -> List A {↑ size}

  -- CPS split (non-size increasing)

  split : {A : Set}{i : Size} -> List A {i} ->
          {C : Set} -> (List A {i} -> List A {i} -> C) -> C
  split []        k = k [] []
  split (x :: xs) k = split xs (\ l r -> k (x :: r) l)

  module Sort (A : Set) (compare : A -> A -> {B : Set} -> B -> B -> B) where

    -- Andreas, 4 Sep 2008
    -- the size indices i and j should not be necessary here
    -- but without them, the termination checker does not recognise that
    -- the pattern x :: xs is equal to the term x :: xs
    -- I suspect that _::_ {∞} x xs is not equal to itself since ∞ is a term
    -- not a constructor or variable
    merge : {i j : Size} -> List A {i} -> List A {j} -> List A
    merge [] ys = ys
    merge xs [] = xs
    merge (x :: xs) (y :: ys) =
      compare x y (x :: merge xs (y :: ys))
                  (y :: merge (x :: xs) ys)

    sort : {i : Size} -> List A {i} -> List A
    sort [] = []
    sort (x :: []) = x :: []
    sort (x :: (y :: xs)) = split xs (\ l r -> merge (sort (x :: l))
                                                     (sort (y :: r)))

module New where

  -- sized lists

  data List A {i} : Set where
    []   : List A
    _::_ : {i' : Size< i} → A → List A {i'} → List A

  module CPS where

    -- CPS split (non-size increasing)

    split : ∀ {A i} → List A {i} →
            {C : Set} → (List A {i} → List A {i} → C) → C
    split []        k = k [] []
    split (x :: xs) k = split xs (\ l r → k (x :: r) l)

    module Sort (A : Set) (compare : A → A → {B : Set} → B → B → B) where

      merge : List A → List A → List A
      merge [] ys = ys
      merge xs [] = xs
      merge (x :: xs) (y :: ys) =
        compare x y (x :: merge xs (y :: ys))
                    (y :: merge (x :: xs) ys)

      sort : {i : Size} → List A {i} → List A
      sort []               = []
      sort (x :: [])        = x :: []
      sort (x :: (y :: xs)) = split xs (\ l r → merge (sort (x :: l))
                                                      (sort (y :: r)))

  module Direct where

    split : ∀ {A i} → List A {i} → List A {i} × List A {i}
    split []        = [] , []
    split (x :: xs) = let l , r = split xs in (x :: r) , l

    module Sort (A : Set) (_≤_ : A → A → Bool) where

      merge : List A → List A → List A
      merge [] ys = ys
      merge xs [] = xs
      merge (x :: xs) (y :: ys) =
        if x ≤ y then (x :: merge xs (y :: ys))
                 else (y :: merge (x :: xs) ys)

      sort : {i : Size} → List A {i} → List A
      sort []               = []
      sort (x :: [])        = x :: []
      sort (x :: (y :: xs)) = let l , r = split xs in merge (sort (x :: l))
                                                            (sort (y :: r))


text:
------------------------------------------------------------------------
-- A formalisation of one variant of the language χ, along with a
-- number of properties
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- A description of the language χ, as well as some of the definitions
-- and proofs used in this development, can be found in "The language
-- χ" by Bengt Nordström (edited by me):
--
-- * https://chalmers.instructure.com/courses/10744/file_contents/course%20files/reading/The_language_chi.pdf
--
-- See also the following lecture slides:
--
-- * https://chalmers.instructure.com/courses/10744/file_contents/course%20files/lectures/L4.pdf
-- * https://chalmers.instructure.com/courses/10744/file_contents/course%20files/lectures/L5.pdf
-- * https://chalmers.instructure.com/courses/10744/file_contents/course%20files/lectures/L6.pdf

module README where

-- Atoms.

import Atom

-- Various constants.

import Constants

-- A specification of the language χ.

import Chi

-- The semantics is deterministic.

import Deterministic

-- Values.

import Values

-- Some cancellation lemmas.

import Cancellation

-- "Reasoning" combinators.

import Reasoning

-- The abstract syntax is a set, and the semantics is propositional.

import Propositional

-- The "terminates" relation.

import Termination

-- Compatibility lemmas.

import Compatibility

-- Some substitution lemmas.

import Substitution

-- Definitions of "free in" and "closed", along with some properties.

import Free-variables

-- Alpha-equivalence.

import Alpha-equivalence

-- Encoders and decoders.

import Coding

-- Encoder and decoder instances.

import Coding.Instances

-- Encoder and decoder instances for Atom.χ-ℕ-atoms.

import Coding.Instances.Nat

-- Internal coding.

import Internal-coding

-- Some χ program combinators.

import Combinators

-- The rec construction can be encoded using λ-terms.

import Recursion-without-rec

-- Definition of the size of an expression, along with some
-- properties.

import Expression-size

-- A self-interpreter (without correctness proof).

import Self-interpreter

-- Partial functions, computability.

import Computability

-- The halting problem.

import Halting-problem

-- Rice's theorem.

import Rices-theorem

-- A theorem related to pointwise equality.

import Pointwise-equality

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures

module MLib.Matrix.SemiTensor {c ℓ} (struct : Struct bimonoidCode c ℓ) where

open import MLib.Matrix.SemiTensor.Core struct using (_⋉_) public
open import MLib.Matrix.SemiTensor.GeneralizesMul struct public


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

module Categories.Category.Instance.Monoidals where

open import Level

open import Categories.Category
open import Categories.Category.Helper
open import Categories.Category.Monoidal
open import Categories.Functor.Monoidal
open import Categories.Functor.Monoidal.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal

module _ o ℓ e where

  Monoidals : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
  Monoidals = categoryHelper record
    { Obj       = MonoidalCategory o ℓ e
    ; _⇒_       = MonoidalFunctor
    ; _≈_       = Lax._≃_
    ; id        = idF-Monoidal _
    ; _∘_       = ∘-Monoidal
    -- NOTE: these η-expanded versions typecheck much faster...
    ; assoc     = λ {_ _ _ _ F G H} → associator {F = F} {G} {H}
    ; identityˡ = λ {_ _ F} → unitorˡ {F = F}
    ; identityʳ = λ {_ _ F} → unitorʳ {F = F}
    ; equiv     = isEquivalence
    ; ∘-resp-≈  = _ⓘₕ_
    }
    where open Lax

  StrongMonoidals : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
  StrongMonoidals = categoryHelper record
    { Obj       = MonoidalCategory o ℓ e
    ; _⇒_       = StrongMonoidalFunctor
    ; _≈_       = Strong._≃_
    ; id        = idF-StrongMonoidal _
    ; _∘_       = ∘-StrongMonoidal
    -- NOTE: these η-expanded versions typecheck much faster...
    ; assoc     = λ {_ _ _ _ F G H} → associator {F = F} {G} {H}
    ; identityˡ = λ {_ _ F} → unitorˡ {F = F}
    ; identityʳ = λ {_ _ F} → unitorʳ {F = F}
    ; equiv     = isEquivalence
    ; ∘-resp-≈  = _ⓘₕ_
    }
    where open Strong

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Numeral.FixedPositional where

{-
FixedPositional : ℕ → Type
FixedPositional(b) = List(𝕟(b))

open import Numeral.Natural.Oper

private variable b : ℕ

to-ℕ : FixedPositional(b) → ℕ
to-ℕ {_} ∅       = 𝟎
to-ℕ {b} (n ⊰ l) = 𝕟-to-ℕ (n) + (b ⋅ to-ℕ (l))

-}

{-
module Test2 where
  import      Lvl
  open import Data
  open import Data.Boolean hiding (elim)
  open import Data.Boolean.Stmt
  import      Data.Boolean.Operators
  open        Data.Boolean.Operators.Programming
  open import Numeral.Finite
  open import Numeral.Natural
  open import Functional
  open import Syntax.Number
  open import Type
  open import Type.Dependent

  private variable ℓ : Lvl.Level
  private variable z : Bool
  private variable b n : ℕ

  positive? : 𝕟(n) → Bool
  positive? 𝟎     = 𝐹
  positive? (𝐒 _) = 𝑇

  Positive : 𝕟(n) → Type
  Positive = IsTrue ∘ positive?

  data Positional(b : ℕ) : Type{Lvl.𝟎} where
    #   : (n : 𝕟(b)) → ⦃ Positive(n) ⦄ → Positional b
    _·_ : Positional b → 𝕟(b) → Positional b
  infixl 20 _·_

  test : Positional 10
  test = # 1 · 5 · 0 · 4 · 0 · 0

  open import Numeral.Natural.Oper

  to-ℕ : Positional b → ℕ
  to-ℕ     (# n)   = 𝕟-to-ℕ n
  to-ℕ {b} (l · n) = (b ⋅ (to-ℕ l)) + (to-ℕ (# n))

  open import Logic.Propositional
  -- open import Numeral.Natural.Decidable
  open import Numeral.Natural.Inductions
  open import Numeral.Natural.Oper.Comparisons
  open import Numeral.Natural.Oper.FlooredDivision
  open import Numeral.Natural.Oper.FlooredDivision.Proofs
  open import Numeral.Natural.Oper.Modulo
  open import Numeral.Natural.Oper.Modulo.Proofs
  open import Numeral.Natural.Relation.Order
  open import Numeral.Natural.Relation.Order.Decidable
  open import Numeral.Natural.Relation.Order.Proofs
  open import Structure.Relator.Ordering
  open import Type.Properties.Decidable
  open import Type.Properties.Decidable.Proofs

  from-ℕ-rec : (b : ℕ) → ⦃ b-size : IsTrue(b >? 1) ⦄ → (x : ℕ) → ((prev : ℕ) ⦃ _ : prev < x ⦄ → Positional(b)) → Positional(b)
  from-ℕ-rec b@(𝐒(𝐒 _)) 𝟎       _    = intro 𝐹 (# 𝟎)
  from-ℕ-rec b@(𝐒(𝐒 _)) n@(𝐒 _) prev with prev(n ⌊/⌋ b) ⦃ [⌊/⌋]-ltₗ {n}{b} ⦄
  ... | intro 𝑇 r = intro 𝑇 (r · (ℕ-to-𝕟 (n mod b) ⦃ [↔]-to-[→] decider-true (mod-maxᵣ{n}{b}) ⦄))
  ... | intro 𝐹 r = {!test2 r [≡]-intro!}
  from-ℕ : ⦃ b-size : IsTrue(b >? 1) ⦄ → ℕ → Positional(b)
  from-ℕ b@{𝐒(𝐒 _)} = Strict.Properties.wellfounded-recursion(_<_) (from-ℕ-rec b)
  {-from-ℕ {b = b@(𝐒(𝐒 _))} 𝟎 = intro 𝐹 (# 𝟎)
  from-ℕ {b = b@(𝐒(𝐒 _))} n@(𝐒 _) with [<][≥]-dichotomy {n}{b}
  ... | [∨]-introₗ lt = intro 𝑇 (# (ℕ-to-𝕟 n ⦃ [↔]-to-[→] decider-true lt ⦄))
  ... | [∨]-introᵣ ge with from-ℕ {b} (n ⌊/⌋ b)
  ... |   intro 𝑇 nb = intro 𝑇 (nb · ℕ-to-𝕟 (n mod b) ⦃ [↔]-to-[→] decider-true (mod-maxᵣ{n}{b}) ⦄)
  ... |   intro 𝐹 _  = intro 𝑇 {!!}-}
-}

module Test where
  open import Data.List
  open import Numeral.Finite
  open import Numeral.Natural
  open import Type
  open import Numeral.Natural.Oper

  private variable b : ℕ

  to-ℕ : ℕ → List(ℕ) → ℕ
  to-ℕ _ ∅       = 𝟎
  to-ℕ b (n ⊰ l) = n + (b ⋅ to-ℕ b l)

  module _ where
    open import Data
    open import Data.Boolean.Stmt
    open import Numeral.Natural.Inductions
    open import Numeral.Natural.Oper.Comparisons
    open import Numeral.Natural.Oper.FlooredDivision
    open import Numeral.Natural.Oper.FlooredDivision.Proofs
    open import Numeral.Natural.Oper.Modulo
    open import Numeral.Natural.Relation
    open import Numeral.Natural.Relation.Order
    open import Relator.Equals
    open import Structure.Relator.Ordering

    from-ℕ-rec : (b : ℕ) → ⦃ b-size : IsTrue(b >? 1) ⦄ → (x : ℕ) → ((prev : ℕ) ⦃ _ : prev < x ⦄ → List ℕ) → List ℕ
    from-ℕ-rec b@(𝐒(𝐒 _)) 𝟎       _    = ∅
    from-ℕ-rec b@(𝐒(𝐒 _)) n@(𝐒 _) prev = (n mod b) ⊰ prev(n ⌊/⌋ b) ⦃ [⌊/⌋]-ltₗ {n} {b} ⦄
    from-ℕ : (b : ℕ) → ⦃ b-size : IsTrue(b >? 1) ⦄ → ℕ → List(ℕ)
    from-ℕ b@(𝐒(𝐒 _)) = Strict.Properties.wellfounded-recursion(_<_) (from-ℕ-rec b)

    open import Numeral.Natural.Oper.DivMod.Proofs
    open import Numeral.Natural.Oper.Proofs
    open import Structure.Function
    open import Structure.Operator
    open import Structure.Operator.Properties
    open import Syntax.Transitivity
    open import Relator.Equals.Proofs.Equiv

    to-from-inverse : ∀{b} ⦃ b-size : IsTrue(b >? 1) ⦄ {n} → (to-ℕ b (from-ℕ b n) ≡ n)
    to-from-inverse {b@(𝐒(𝐒 bb))} {n} = Strict.Properties.wellfounded-recursion-intro(_<_) {rec = from-ℕ-rec b} {φ = \{n} expr → (to-ℕ b expr ≡ n)} p {n} where
      p : (y : ℕ) → _ → _ → (to-ℕ b (Strict.Properties.accessible-recursion(_<_) (from-ℕ-rec b) y) ≡ y)
      p 𝟎     _    _    = [≡]-intro
      p (𝐒 y) prev step =
        to-ℕ b (Strict.Properties.accessible-recursion(_<_) (from-ℕ-rec b) (𝐒 y)) 🝖[ _≡_ ]-[ congruence₁(to-ℕ b) (step {𝐒(y) ⌊/⌋ b} ⦃ [⌊/⌋]-ltₗ {𝐒 y}{b} ⦄) ]
        (𝐒(y) mod b) + (b ⋅ to-ℕ b (Strict.Properties.accessible-recursion(_<_) (from-ℕ-rec b) (𝐒(y) ⌊/⌋ b))) 🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(𝐒(y) mod b) (congruence₂ᵣ(_⋅_)(b) (prev{𝐒(y) ⌊/⌋ b} ⦃ [⌊/⌋]-ltₗ {𝐒 y}{b} ⦄)) ]
        (𝐒(y) mod b) + (b ⋅ (𝐒(y) ⌊/⌋ b)) 🝖[ _≡_ ]-[ commutativity(_+_) {𝐒(y) mod b}{b ⋅ (𝐒(y) ⌊/⌋ b)} ]
        (b ⋅ (𝐒(y) ⌊/⌋ b)) + (𝐒(y) mod b) 🝖[ _≡_ ]-[ [⌊/⌋][mod]-is-division-with-remainder-pred-commuted {𝐒 y}{b} ]
        𝐒(y) 🝖-end

  -- TODO: There are some requirements on l for this to hold. For example, it should not end with zeroes (actually start with because the representation is reversed from the usual one), it should not have numbers greater or equal to b
  {-from-to-inverse : ∀{b} ⦃ b-size : IsTrue(b >? 1) ⦄ {l} → (from-ℕ b (to-ℕ b l) ≡ l)
  from-to-inverse b@{𝐒(𝐒 _)} {l = ∅} = [≡]-intro
  from-to-inverse b@{𝐒(𝐒 _)} {l = x ⊰ l} = {!!}-}
  {-Strict.Properties.wellfounded-recursion-intro(_<_) {rec = from-ℕ-rec b} {φ = \{n} expr → (expr ≡ from-ℕ b n)} p {x + (b ⋅ to-ℕ b l)} where
    p : (y : ℕ) → _ → _ → (Strict.Properties.accessible-recursion(_<_) (from-ℕ-rec b) y ≡ from-ℕ b y)
    p 𝟎 prev step = {!!}
    p (𝐒 y) prev step = {!!}-}

{-
module _ where
  open import Functional
  open import Function.Iteration using (repeatᵣ)
  open import Numeral.Natural.Induction
  open import Relator.Equals
  open import Relator.Equals.Proofs
  open import Syntax.Function
  open import Syntax.Transitivity

  {- TODO: Attempt to prove `∀a∀b. aᵇ = 1 + ((a−1) ⋅ ∑(0‥b) (i ↦ aⁱ))` inductively. An intuitive example of this is: `10³ = 1000 = 1+999 = 1+(9⋅111) = 1+(9⋅(1+10+100)) = 1+((10−1)⋅(10⁰+10¹+10²))`. This can also be proved by using the binomial theorem?
  powerSum : ℕ → ℕ → ℕ
  powerSum a 0         = 0
  powerSum a 1         = 1
  powerSum a (𝐒(𝐒(b))) = (powerSum a (𝐒(b))) + (a ⋅ (powerSum a (𝐒(b))))

  exponentiation-is-sum-of-parts : ∀{a b} → (𝐒(a) ^ b ≡ 𝐒(a ⋅ (powerSum (𝐒(a)) b)))
  exponentiation-is-sum-of-parts {a} {0}       = [≡]-intro
  exponentiation-is-sum-of-parts {a} {1}       = [≡]-intro
  exponentiation-is-sum-of-parts {a} {𝐒(b@(𝐒(_)))} =
    𝐒(a) ^ 𝐒(b)                     🝖[ _≡_ ]-[]
    𝐒(a) ⋅ (𝐒(a) ^ b)               🝖[ _≡_ ]-[ {!!} ]
    (𝐒(a) ^ b) + (𝐒(a) ⋅ (a ⋅ (powerSum (𝐒(a)) b)))                   🝖[ _≡_ ]-[ {!!} ]
    (𝐒(a) ^ b) + (a ⋅ (𝐒(a) ⋅ (powerSum (𝐒(a)) b)))                   🝖[ _≡_ ]-[ {!!} ]
    𝐒(a ⋅ (powerSum (𝐒(a)) b)) + (a ⋅ (𝐒(a) ⋅ (powerSum (𝐒(a)) b)))   🝖[ _≡_ ]-[ {!!} ]
    𝐒((a ⋅ (powerSum (𝐒(a)) b)) + (a ⋅ (𝐒(a) ⋅ (powerSum (𝐒(a)) b)))) 🝖[ _≡_ ]-[ {!!} ]
    𝐒(a ⋅ ((powerSum (𝐒(a)) b) + (𝐒(a) ⋅ (powerSum (𝐒(a)) b))))       🝖[ _≡_ ]-[]
    𝐒(a ⋅ (powerSum (𝐒(a)) (𝐒(b))))                                   🝖-end
  -}

module _ where
  open import Data.List.Functions
  open import Numeral.Natural.Relation.Order
  open import Numeral.Natural.Relation.Order.Proofs
  open import Structure.Relator.Properties
  open import Syntax.Transitivity

  {-
  FixedPositional-maximum : ∀{n : FixedPositional(b)} → (to-ℕ (n) < b ^ length(n))
  FixedPositional-maximum {_}   {∅}     = reflexivity(_≤_)
  FixedPositional-maximum {𝐒 b} {n ⊰ l} =
    𝐒(𝕟-to-ℕ (n) + (𝐒(b) ⋅ to-ℕ (l)))                               🝖[ _≤_ ]-[ {!!} ]
    𝐒(𝕟-to-ℕ (n) + (𝐒(b) ⋅ (b ^ length(l))))                        🝖[ _≤_ ]-[ {!!} ]
    𝐒(𝕟-to-ℕ (n) + ((b ⋅ (b ^ length(l))) + (1 ⋅ (b ^ length(l))))) 🝖[ _≤_ ]-[ {!!} ]
    𝐒(𝕟-to-ℕ (n) + ((b ^ 𝐒(length(l))) + (b ^ length(l))))          🝖[ _≤_ ]-[ {!!} ]
    ?                                                               🝖[ _≤_ ]-[ {!!}
    (b ⋅ (𝐒(b) ^ length(l))) + (𝐒(b) ^ length(l))                   🝖[ _≤_ ]-[ {!!} ]
    𝐒(b) ⋅ (𝐒(b) ^ length(l))                                       🝖-end
  -}
-}


text:
module Logic.Predicate.Theorems where

import      Lvl
open import Functional
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
open import Syntax.Type
open import Type
open import Type.Properties.Inhabited using (◊ ; [◊]-existence)

------------------------------------------
-- Swapping nested quantifiers

module _ {ℓₒ₁}{ℓₒ₂}{ℓₗ} {X : Type{ℓₒ₁}}{Y : Type{ℓₒ₂}}{P : X → Y → Stmt{ℓₗ}} where
  [∀]-swap : ∀ₗ(x ↦ ∀ₗ(y ↦ P(x)(y))) → ∀ₗ(y ↦ ∀ₗ(x ↦ P(x)(y)))
  [∀]-swap(xypxy){y}{x} = xypxy{x}{y}

  [∃]-swap : ∃(x ↦ ∃(y ↦ P(x)(y))) → ∃(y ↦ ∃(x ↦ P(x)(y)))
  [∃]-swap([∃]-intro(x) ⦃ [∃]-intro(y) ⦃ proof ⦄ ⦄) = [∃]-intro(y) ⦃ [∃]-intro(x) ⦃ proof ⦄ ⦄

------------------------------------------
-- Introducing and eliminating unnecessary quantifiers when the predicate is constant

module _ {ℓₒ}{ℓₗ} {X : Type{ℓₒ}} ⦃ pos : ◊ X ⦄ {P : Stmt{ℓₗ}} where
  [∃]-unnecessary-intro : P → ∃{Obj = X}(x ↦ P)
  [∃]-unnecessary-intro(p) = [∃]-intro([◊]-existence ⦃ pos ⦄) ⦃ p ⦄

module _ {ℓₒ}{ℓₗ} {X : Type{ℓₒ}} {P : Stmt{ℓₗ}} where
  [∀]-unnecessary-intro : P → ∀ₗ{Obj = X}(x ↦ P)
  [∀]-unnecessary-intro(p){x} = p

  [∃]-unnecessary-elim : ∃{Obj = X}(x ↦ P) → P
  [∃]-unnecessary-elim([∃]-intro(_) ⦃ proof ⦄) = proof

module _ {ℓₒ}{ℓₗ} {X : Type{ℓₒ}} ⦃ pos : ◊ X ⦄ {P : Stmt{ℓₗ}} where
  -- Note:
  --   The following is unprovable:
  --   [∀]-unnecessary : ∀{X}{P : Stmt} → ∀ₗ{X}(x ↦ P) → P
  --   X is not guaranteed to not be the empty type, and even if it was, the ∀ function requires a constructed value. It seems to need a non-empty domain to quantify over.
  [∀ₑ]-unnecessary-elim : ∀ₗ{Obj = X}(x ↦ P) → P
  [∀ₑ]-unnecessary-elim = [∀ₑ]-elim{Obj = X} ⦃ pos ⦄

------------------------------------------
-- When quantifiers contradict

module _ {ℓₒ}{ℓₗ} {X : Type{ℓₒ}} {P : X → Stmt{ℓₗ}} where
  [∀][∃¬]-contradiction : ∀ₗ(x ↦ P(x)) → ∃(x ↦ ¬(P(x))) → ⊥
  [∀][∃¬]-contradiction(ap)(enp) =
    ([∃]-elim(\{a} → np ↦ (
      ([⊥]-intro
        ([∀]-elim{Obj = X}{P} ap(a))
        np
      )
    )) (enp))

  [∀¬][∃]-contradiction : ∀ₗ(x ↦ ¬ P(x)) → ∃(x ↦ P(x)) → ⊥
  [∀¬][∃]-contradiction (axnpx) (expx) =
    axnpx {[∃]-witness(expx)} ([∃]-proof(expx))

------------------------------------------
-- Moving in and out negation from quantifiers

module _ {ℓₒ}{ℓₗ} {X : Type{ℓₒ}} {P : X → Stmt{ℓₗ}} where
  [∃¬]-to-[¬∀] : (∃(x ↦ ¬(P(x)))) → ¬(∀ₗ(x ↦ P(x)))
  [∃¬]-to-[¬∀] = swap ([∀][∃¬]-contradiction {ℓₒ}{ℓₗ})

  [∀¬]-to-[¬∃] : ∀ₗ(x ↦ ¬(P(x))) → ¬(∃(x ↦ P(x)))
  [∀¬]-to-[¬∃] = [∀¬][∃]-contradiction {ℓₒ}{ℓₗ} {X}{P}
    -- [∀¬]-to-[¬∃] (anpx) =
    --   ([¬]-intro(epx ↦
    --     [∃]-elim(\{a} → pa ↦
    --       ([⊥]-intro
    --         pa
    --         (anpx{a})
    --       )
    --     )(epx)
    --   ))

  [¬∃]-to-[∀¬] : ∀ₗ(x ↦ ¬(P(x))) ← ¬(∃(x ↦ P(x)))
  [¬∃]-to-[∀¬] (nepx) =
    ([∀]-intro(a ↦
      (([¬]-intro(pa ↦
        (([⊥]-intro
          (([∃]-intro a ⦃ pa ⦄) :of: (∃(x ↦ P(x))))
          (nepx :of: ¬(∃(x ↦ P(x))))
        ) :of: ⊥)
      )) :of: ¬(P(a)))
    ))

module _ {ℓₒ}{ℓₗ} {X : Type{ℓₒ}} ⦃ pos : ◊ X ⦄ {P : X → Stmt{ℓₗ}} where
  [¬∃]-to-[∃¬] : ¬(∃ P) → ∃(¬_ ∘ P)
  [¬∃]-to-[∃¬] (nexpx) = [∃]-intro ([◊]-existence ⦃ pos ⦄) ⦃ [¬∃]-to-[∀¬] {ℓₒ}{ℓₗ} {X}{P} (nexpx) ⦄

  [¬∃]-to-[¬∀] : ¬(∃ P) → ¬(∀ₗ P)
  [¬∃]-to-[¬∀] = ([∃¬]-to-[¬∀] {ℓₒ}{ℓₗ} {X}{P}) ∘ [¬∃]-to-[∃¬]

  [∀¬]-to-[¬∀] : ∀ₗ(¬_ ∘ P) → ¬(∀ₗ P)
  [∀¬]-to-[¬∀] axnpx axpx = (axnpx{[◊]-existence ⦃ pos ⦄}) (axpx{[◊]-existence ⦃ pos ⦄})

------------------------------------------
-- Introducing negations to change quantifier

module _ {ℓₒ}{ℓₗ} {X : Type{ℓₒ}} {P : X → Stmt{ℓₗ}} where
  [∀]-to-[¬∃¬] : ∀ₗ(x ↦ P(x)) → (¬ ∃(x ↦ ¬(P(x))))
  [∀]-to-[¬∃¬] = [∀][∃¬]-contradiction {ℓₒ}{ℓₗ} {X}{P} -- [∃]-elim(\{a} → npa ↦ npa(p{a}))(ep)

  [∃]-to-[¬∀¬] : ∃(x ↦ P(x)) → (¬ ∀ₗ(x ↦ ¬(P(x))))
  [∃]-to-[¬∀¬] = swap ([∀¬][∃]-contradiction {ℓₒ}{ℓₗ} {X}{P})

------------------------------------------
-- Stuff using double negation

module _ {ℓₒ}{ℓₗ} {X : Type{ℓₒ}} {P : X → Stmt{ℓₗ}} where
  [∀¬¬][∃¬]-contradiction : ∀ₗ(x ↦ ¬¬(P(x))) → (∃(x ↦ ¬(P(x)))) → ⊥
  [∀¬¬][∃¬]-contradiction (annp)([∃]-intro(a) ⦃ na ⦄) =
    [∀][∃¬]-contradiction {ℓₒ}{ℓₗ} {X}{¬¬_ ∘ P} (annp)([∃]-intro(a) ⦃ [¬¬]-intro(na) ⦄)

  [∀¬¬]-to-[¬∃¬] : ∀ₗ(x ↦ ¬¬(P(x))) → (¬ ∃(x ↦ ¬(P(x))))
  [∀¬¬]-to-[¬∃¬] = [∀¬¬][∃¬]-contradiction

  [¬¬∀]-to-[¬∃¬] : ¬¬ ∀ₗ(x ↦ (P(x))) → (¬ ∃(x ↦ ¬(P(x))))
  [¬¬∀]-to-[¬∃¬] = contrapositiveᵣ ([∃¬]-to-[¬∀] {ℓₒ}{ℓₗ} {X}{P})
  -- [¬¬∀]-to-[¬∃¬] (annx) (enx) =
  --   ([⊥]-intro
  --     ([∃¬]-to-[¬∀](enx))
  --     (annx)
  --   )

  [¬∃¬]-to-[∀¬¬] : ¬(∃(x ↦ ¬(P(x)))) → ∀ₗ(x ↦ ¬¬(P(x)))
  [¬∃¬]-to-[∀¬¬] (nenx) {a} (npa) = nenx([∃]-intro(a) ⦃ npa ⦄)

  [¬¬∀]-to-[∀¬¬] : ¬¬ ∀ₗ(x ↦ (P(x))) → ∀ₗ(x ↦ ¬¬(P(x)))
  [¬¬∀]-to-[∀¬¬] = [¬∃¬]-to-[∀¬¬] ∘ [¬¬∀]-to-[¬∃¬]

  [∀]-to-[∃]-conditional-by-existence : ∃(P) → ∀{Q : X → Stmt{ℓₗ}} → ∀ₗ(x ↦ (P(x) → Q(x))) → ∃(x ↦ (P(x) ∧ Q(x)))
  ∃.witness ([∀]-to-[∃]-conditional-by-existence p pq) = [∃]-witness p
  ∃.proof   ([∀]-to-[∃]-conditional-by-existence p pq) = [∧]-intro ([∃]-proof p) (pq{[∃]-witness p} ([∃]-proof p))

  -- TODO: Probably unprovable. Not sure why. Maybe because (¬¬A is valid in constructive logic) ⇔ (A is valid in classical logic), and therefore this would not be possible because everything here is in constructive logic.
  -- [∀¬¬]-to-[¬¬∀] : ∀{X}{P : X → Stmt} → ¬¬∀ₗ(x ↦ (P(x))) ← ∀ₗ(x ↦ ¬¬(P(x)))

------------------------------------------
-- Changing quantifier

module _ {ℓₒ}{ℓₗ} {X : Type{ℓₒ}} ⦃ pos : ◊ X ⦄ {P : X → Stmt{ℓₗ}} where
  -- Note: If X would be empty, then this would be unprovable because [∀]-elim needs a constructed element.
  [∀ₑ]-to-[∃] : ∀ₗ(x ↦ P(x)) → ∃(x ↦ P(x))
  [∀ₑ]-to-[∃] (apx) =
    [∃]-intro ([◊]-existence ⦃ pos ⦄) ⦃ [∀ₑ]-elim{Obj = X}{P = P}(apx) ⦄

------------------------------------------
-- "Distributing" quantifiers into logical operators

module _ {ℓₒ}{ℓₗ₁}{ℓₗ₂} {X : Type{ℓₒ}}{P : X → Stmt{ℓₗ₁}}{Q : X → Stmt{ℓₗ₂}} where
  [∀][→]-distributivity : ∀ₗ(x ↦ (P(x) → Q(x))) → ∀ₗ(x ↦ P(x)) → ∀ₗ(x ↦ Q(x))
  [∀][→]-distributivity (PxQx) (Px) = PxQx(Px)

  [∀][∧]-distributivity : ∀ₗ(x ↦ (P(x) ∧ Q(x))) ↔ (∀ₗ(x ↦ P(x)) ∧ ∀ₗ(x ↦ Q(x)))
  [∀][∧]-distributivity = [↔]-intro l r where
    l : (∀ₗ(x ↦ P(x)) ∧ ∀ₗ(x ↦ Q(x))) → ∀ₗ(x ↦ (P(x) ∧ Q(x)))
    l ([∧]-intro (axPx) (axQx)) {x} = [∧]-intro (axPx{x}) (axQx{x})

    r : (∀ₗ(x ↦ P(x)) ∧ ∀ₗ(x ↦ Q(x))) ← ∀ₗ(x ↦ (P(x) ∧ Q(x)))
    r(apxqx) = [∧]-intro (\{x} → [∧]-elimₗ(apxqx{x})) (\{x} → [∧]-elimᵣ(apxqx{x}))

  [∃][∨]-distributivity : ∃(x ↦ (P(x) ∨ Q(x))) ↔ (∃(x ↦ P(x)) ∨ ∃(x ↦ Q(x)))
  [∃][∨]-distributivity = [↔]-intro l r where
    l : (∃(x ↦ P(x)) ∨ ∃(x ↦ Q(x))) → ∃(x ↦ (P(x) ∨ Q(x)))
    l ([∨]-introₗ ([∃]-intro x ⦃ px ⦄)) = [∃]-intro x ⦃ [∨]-introₗ px ⦄
    l ([∨]-introᵣ ([∃]-intro x ⦃ qx ⦄)) = [∃]-intro x ⦃ [∨]-introᵣ qx ⦄

    r : (∃(x ↦ P(x)) ∨ ∃(x ↦ Q(x))) ← ∃(x ↦ (P(x) ∨ Q(x)))
    r ([∃]-intro x ⦃ [∨]-introₗ px ⦄) = [∨]-introₗ ([∃]-intro x ⦃ px ⦄)
    r ([∃]-intro x ⦃ [∨]-introᵣ qx ⦄) = [∨]-introᵣ ([∃]-intro x ⦃ qx ⦄)

  [∃][∧]-semidistributivity : ∃(x ↦ ∃(y ↦ (P(x) ∧ Q(y)))) ↔ (∃(x ↦ P(x)) ∧ ∃(x ↦ Q(x)))
  [∃][∧]-semidistributivity = [↔]-intro l r where
    l : ∃(x ↦ ∃(y ↦ (P(x) ∧ Q(y)))) ← (∃(x ↦ P(x)) ∧ ∃(x ↦ Q(x)))
    l ([∧]-intro ([∃]-intro x ⦃ px ⦄) ([∃]-intro y ⦃ qy ⦄)) = [∃]-intro x ⦃ [∃]-intro y ⦃ [∧]-intro px qy ⦄ ⦄

    r : ∃(x ↦ ∃(y ↦ (P(x) ∧ Q(y)))) → (∃(x ↦ P(x)) ∧ ∃(x ↦ Q(x)))
    r ([∃]-intro x ⦃ [∃]-intro y ⦃ [∧]-intro px qy ⦄ ⦄) = [∧]-intro ([∃]-intro x ⦃ px ⦄) ([∃]-intro y ⦃ qy ⦄)

  [∃][∧]-distributivity : ∃(x ↦ (P(x) ∧ Q(x))) → (∃(x ↦ P(x)) ∧ ∃(x ↦ Q(x)))
  [∃][∧]-distributivity ([∃]-intro x ⦃ [∧]-intro px qx ⦄ ) = [∧]-intro l r where
    l = [∃]-intro x ⦃ px ⦄
    r = [∃]-intro x ⦃ qx ⦄

module _ {ℓₒ}{ℓₗ₁}{ℓₗ₂} {X : Type{ℓₒ}}{P : X → Stmt{ℓₗ₁}}{Q : X → Stmt{ℓₗ₂}} where
  [∀][↔]-distributivity : ∀ₗ(x ↦ (P(x) ↔ Q(x))) → (∀ₗ(x ↦ P(x)) ↔ ∀ₗ(x ↦ Q(x)))
  [∀][↔]-distributivity = r where -- [↔]-intro l r where
    -- l : ∀ₗ(x ↦ (P(x) ↔ Q(x))) ← (∀ₗ(x ↦ P(x)) ↔ ∀ₗ(x ↦ Q(x)))
    -- l([↔]-intro aqxapx apxaqx) {x} = [↔]-intro (\qx → aqxpx(qx{x})) (apxqx{x})

    r : ∀ₗ(x ↦ (P(x) ↔ Q(x))) → (∀ₗ(x ↦ P(x)) ↔ ∀ₗ(x ↦ Q(x)))
    r apxqx = [↔]-intro ([∀][→]-distributivity rl) ([∀][→]-distributivity rr) where
      rl : ∀ₗ(x ↦ (P(x) ← Q(x)))
      rl{x} = [↔]-to-[←](apxqx{x})

      rr : ∀ₗ(x ↦ (P(x) → Q(x)))
      rr{x} = [↔]-to-[→](apxqx{x})

  [∀]-to-[∃]-[↔]-semidistributivity : ∀ₗ(x ↦ (P(x) ↔ Q(x))) → (∃(x ↦ P(x)) ↔ ∃(x ↦ Q(x)))
  [∀]-to-[∃]-[↔]-semidistributivity apq = [↔]-intro ([∃]-map-proof ([↔]-to-[←] apq)) ([∃]-map-proof ([↔]-to-[→] apq))

------------------------------------------
-- Quantifiers with logical operators inside, but one of the predicates are constant

module _ {ℓₒ}{ℓₗ₁}{ℓₗ₂} {X : Type{ℓₒ}}{P : X → Stmt{ℓₗ₁}}{Q : Stmt{ℓₗ₂}} where
  [∀]-unrelatedₗ-[→] : ∀ₗ(x ↦ (P(x) → Q)) ↔ (∃(x ↦ P(x)) → Q)
  [∀]-unrelatedₗ-[→] = [↔]-intro l r where
    l : ∀ₗ(x ↦ (P(x) → Q)) ← (∃(x ↦ P(x)) → Q)
    l(expxq) {x} px = expxq([∃]-intro(x) ⦃ px ⦄)

    r : ∀ₗ(x ↦ (P(x) → Q)) → (∃(x ↦ P(x)) → Q)
    r(axpxq) = [∃]-elim(\{x} → px ↦ axpxq{x}(px))

  [∃]-unrelatedₗ-[→]ᵣ : ∃(x ↦ (P(x) → Q)) → (∀ₗ(x ↦ P(x)) → Q)
  [∃]-unrelatedₗ-[→]ᵣ = r where -- [↔]-intro l r where
    r : ∃(x ↦ (P(x) → Q)) → (∀ₗ(x ↦ P(x)) → Q)
    r(expxq)(axpx) = [∃]-proof(expxq) (axpx{[∃]-witness(expxq)})

  [∃]-unrelatedₗ-[∧] : ∃(x ↦ (P(x) ∧ Q)) ↔ (∃(x ↦ P(x)) ∧ Q)
  [∃]-unrelatedₗ-[∧] = [↔]-intro l r where
    l : ∃(x ↦ (P(x) ∧ Q)) ← (∃(x ↦ P(x)) ∧ Q)
    l ([∧]-intro ([∃]-intro x ⦃ px ⦄) q) = [∃]-intro x ⦃ [∧]-intro px q ⦄

    r : ∃(x ↦ (P(x) ∧ Q)) → (∃(x ↦ P(x)) ∧ Q)
    r ([∃]-intro x ⦃ [∧]-intro px q ⦄) = [∧]-intro ([∃]-intro x ⦃ px ⦄) q

module _ {ℓₒ}{ℓₗ₁}{ℓₗ₂} {X : Type{ℓₒ}}{P : Stmt{ℓₗ₁}}{Q : X → Stmt{ℓₗ₂}} where
  [∀]-unrelatedᵣ-[→] : ∀ₗ(x ↦ (P → Q(x))) ↔ (P → ∀ₗ(x ↦ Q(x)))
  [∀]-unrelatedᵣ-[→] = [↔]-intro l r where
    l : ∀ₗ(x ↦ (P → Q(x))) ← (P → ∀ₗ(x ↦ Q(x)))
    l(paxqx) {x} p = paxqx(p){x}

    r : ∀ₗ(x ↦ (P → Q(x))) → (P → ∀ₗ(x ↦ Q(x)))
    r(axpqx)(p){x} = axpqx{x}(p)

  [∃]-unrelatedᵣ-[→]ᵣ : ∃(x ↦ (P → Q(x))) → (P → ∃(x ↦ Q(x)))
  [∃]-unrelatedᵣ-[→]ᵣ = r where -- [↔]-intro l r where
    r : ∃(x ↦ (P → Q(x))) → (P → ∃(x ↦ Q(x)))
    r(expqx)(p) = [∃]-elim(\{x} → pqx ↦ [∃]-intro(x) ⦃ pqx(p) ⦄) (expqx)

  [∃]-unrelatedᵣ-[∧] : ∃(x ↦ (P ∧ Q(x))) ↔ (P ∧ ∃(x ↦ Q(x)))
  [∃]-unrelatedᵣ-[∧] = [↔]-intro l r where
    l : ∃(x ↦ (P ∧ Q(x))) ← (P ∧ ∃(x ↦ Q(x)))
    l ([∧]-intro p ([∃]-intro x ⦃ qx ⦄)) = [∃]-intro x ⦃ [∧]-intro p qx ⦄

    r : ∃(x ↦ (P ∧ Q(x))) → (P ∧ ∃(x ↦ Q(x)))
    r ([∃]-intro x ⦃ [∧]-intro p qx ⦄) = [∧]-intro p ([∃]-intro x ⦃ qx ⦄)

------------------------------------------
-- Equivalences

module _ {ℓₒ}{ℓₗ₁}{ℓₗ₂} {X : Type{ℓₒ}}{P : X → Stmt{ℓₗ₁}}{Q : X → Stmt{ℓₗ₂}} where
  [∃]-map-proof-[↔] : (∀{x} → P(x) ↔ Q(x)) → ((∃ P) ↔ (∃ Q))
  [∃]-map-proof-[↔] p = [↔]-intro ([∃]-map-proof ([↔]-to-[←] p)) ([∃]-map-proof ([↔]-to-[→] p))

------------------------------------------
-- Other rules

module _ {ℓₒ}{ℓₗ₁}{ℓₗ₂} {X : Type{ℓₒ}}{P : X → Stmt{ℓₗ₁}}{Q : X → Stmt{ℓₗ₂}} where
  [∀][→]-add-[∃] : ∀ₗ(x ↦ (P(x) → Q(x))) → ∀ₗ(x ↦ (P(x) → ∃(x ↦ Q(x))))
  [∀][→]-add-[∃] (proof) {x} px = [∃]-intro(x) ⦃ proof{x} px ⦄

  [∀][→]-to-[∃] : ∀ₗ(x ↦ (P(x) → Q(x))) → (∃(x ↦ P(x)) → ∃(x ↦ Q(x)))
  [∀][→]-to-[∃] (proof) = ([↔]-to-[→] ([∀]-unrelatedₗ-[→] {X = X} {P})) ([∀][→]-add-[∃] (proof))

module _ {ℓₒ₁}{ℓₒ₂}{ℓₗ} {X : Type{ℓₒ₁}}{Y : Type{ℓₒ₂}}{P : X → Y → Stmt{ℓₗ}} where
  [∀][∃]-swap : ∃(x ↦ ∀ₗ(y ↦ P(x)(y))) → ∀ₗ(y ↦ ∃(x ↦ P(x)(y)))
  [∀][∃]-swap ([∃]-intro x ⦃ aypxy ⦄) {y} = [∃]-intro x ⦃ aypxy{y} ⦄

  {-
  no-intermediate : ∀{X : Stmt} → ¬(¬(X ↔ ⊤) ∧ ¬(X ↔ ⊥))
  no-intermediate = [¬][∨] [¬¬]-excluded-middle

  ¬((¬ X) ∧ (¬ Y)) ↔ ¬(¬ (X ∨ Y))
  ∀{X} → ¬¬(X ∨ (¬ X))
  -}

module _ {ℓₒ₁}{ℓₒ₂}{ℓₗ} {X : Type{ℓₒ₁}}{Y : Type{ℓₒ₂}}{P : X → Y → Stmt{ℓₗ}} where
  [∀][∃]-to-function-existence : ∀ₗ(x ↦ ∃(y ↦ P(x)(y))) → ∃(f ↦ ∀ₗ(x ↦ P(x)(f(x))))
  [∀][∃]-to-function-existence p = [∃]-intro (x ↦ [∃]-witness(p{x})) ⦃ \{x} → [∃]-proof(p{x}) ⦄


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module Quicksort.Correctness.Permutation {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_) where

open import Bound.Total A
open import Bound.Total.Order _≤_
open import Data.List
open import Data.Product
open import Data.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Concatenation A
open import List.Permutation.Base.Equivalence A
open import List.Permutation.Pair A
open import List.Permutation.Pair.Properties A
open import Quicksort _≤_ tot≤
open import SBList _≤_
open import SBList.Properties _≤_
open import Size
open import SOList.Total _≤_

lemma-deal : {ι : Size}{b t : Bound}{x : A} → (b≤x : LeB b (val x)) → (x≤t : LeB (val x) t) → (xs : SBList {ι} b t) → unbound xs ≈ unbound× (deal b≤x x≤t xs)
lemma-deal _ _ (nil _) = ≈[]r []
lemma-deal {x = x} b≤x x≤t (cons y b≤y y≤t ys)
    with tot≤ x y
... | inj₁ x≤y = ≈xr (lemma-deal b≤x x≤t ys)
... | inj₂ y≤x = ≈xl (lemma-deal b≤x x≤t ys)

lemma-quickSort : {ι : Size}{b t : Bound}(xs : SBList {ι} b t) → unbound xs ∼ forget (quickSort xs)
lemma-quickSort (nil _) = ∼[]
lemma-quickSort (cons x b≤x x≤t xs) =  trans∼ (lemma≈∼ (≈xr (lemma-deal b≤x x≤t xs))) (lemma++∼ (lemma-quickSort ys) (∼x /head /head (lemma-quickSort zs)))
                where yszs = deal b≤x x≤t xs
                      ys = proj₁ yszs
                      zs = proj₂ yszs

theorem-quickSort∼ : (xs : List A) → xs ∼ forget (quickSort (bound xs))
theorem-quickSort∼ xs = trans∼ (lemma-unbound-bound xs) (lemma-quickSort (bound xs))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

-- An inhabited Indiscrete category is a -2-Category
module Categories.Minus2-Category.Construction.Indiscrete where

open import Level
open import Data.Unit using (tt)
open import Data.Product using (_,_)
open import Relation.Binary.PropositionalEquality using (refl)

open import Categories.Minus2-Category
open import Categories.Category.Indiscrete
open import Categories.Morphism using (_≅_)

InhIndIs-2 : ∀ {o ℓ} → (X : Set o) → (x : X) → -2-Category {o} {ℓ} {ℓ}
InhIndIs-2 X x = record
  { cat = Indiscrete X
  ; Obj-Contr = x , λ y → record
    { from = lift tt
    ; to = lift tt
    ; iso = record
      { isoˡ = refl
      ; isoʳ = refl
      }
    }
  ; Hom-Conn = refl
  }


text:
-- Builtin things aren't allowed inside parameterised modules. It's not clear
-- what that would mean.
module BuiltinInParameterisedModule where

module A (X : Set) where
  {-# BUILTIN INTEGER X #-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --copatterns #-}

module DataRecordCoinductive where

data ⊥ : Set where

record ⊤ : Set where
  constructor tt

mutual

  data Stream (A : Set) : Set where
    cons : Cons A → Stream A

  -- since Cons is coinductive, we are creating streams
  record Cons (A : Set) : Set where
    coinductive
    constructor _∷_
    field head : A
          tail : Stream A

open Cons

mutual

  repeat : {A : Set}(a : A) → Stream A
  repeat a = cons (repeat' a)

  repeat'  : {A : Set}(a : A) → Cons A
  head (repeat' a) = a
  tail (repeat' a) = repeat a

-- should not termination check: coconstructors are not size preserving
consume : {A : Set} → Stream A → ⊥
-- consume (cons s) = consume (tail s)  -- fails termination check
consume (cons (x ∷ xs)) = consume xs

loop : ⊥
loop = consume (repeat tt)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.UnivariateList.Polyn-nPoly where

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

open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyList
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly

open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.Poly0-A
open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.An[Am[X]]-Anm[X]
open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.AB-An[X]Bn[X]
open import Cubical.Algebra.Polynomials.UnivariateList.Poly1-1Poly

open CommRingEquivs renaming (compCommRingEquiv to _∘-ecr_ ; invCommRingEquiv to inv-ecr)

private variable
  ℓ : Level

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

Equiv-Polyn-nPoly : (A' : CommRing ℓ) → (n : ℕ) → CommRingEquiv (PolyCommRing A' n) (nUnivariatePolyList A' n)
Equiv-Polyn-nPoly A' zero = CRE-Poly0-A A'
Equiv-Polyn-nPoly A' (suc n) =       inv-ecr _ _ (CRE-PolyN∘M-PolyN+M A' 1 n)
                               ∘-ecr (lift-equiv-poly _ _ 1 (Equiv-Polyn-nPoly A' n)
                               ∘-ecr CRE-Poly1-Poly: (nUnivariatePolyList A' n))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------------
-- The Booleans
------------------------------------------------------------------------------

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

module FOTC.Data.Bool where

open import FOTC.Base
open import FOTC.Data.Bool.Type public

infixr 6 _&&_

------------------------------------------------------------------------------
-- Basic functions

-- The conjunction.
_&&_  : D → D → D
a && b = if a then b else false
{-# ATP definition _&&_ #-}

-- The negation.
not : D → D
not b = if b then false else true
{-# ATP definition not #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Let where

f
  : {A : Set}
  → A
  → A
f x
  = let
      y = x
      z = x
    in y

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
module Sections where

open import Haskell.Prelude

test₁ : Nat → Nat
test₁ = 5 +_

test₂ : Nat → Nat
test₂ = _+ 5

test₃ : Nat → Nat
test₃ = _+_ 5

test₄ : Nat → Nat
test₄ = λ x → x + 5

test₅ : Nat → Nat
test₅ = λ x → 5 + x -- Agda eta-contracts this before we get to see it

{-# COMPILE AGDA2HS test₁ #-}
{-# COMPILE AGDA2HS test₂ #-}
{-# COMPILE AGDA2HS test₃ #-}
{-# COMPILE AGDA2HS test₄ #-}
{-# COMPILE AGDA2HS test₅ #-}


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

open import Fragment.Equational.Theory

module Fragment.Equational.Coproduct (Θ : Theory) where

open import Fragment.Equational.Model Θ
open import Fragment.Algebra.Homomorphism (Σ Θ)

open import Level using (Level; Setω)

private
  variable
    a b c ℓ₁ ℓ₂ ℓ₃ : Level

module _
  (A : Model {a} {ℓ₁})
  (B : Model {b} {ℓ₂})
  (A+B : Model {c} {ℓ₃})
  where

  record IsCoproduct : Setω where
    field
      inl : ∥ A ∥ₐ ⟿ ∥ A+B ∥ₐ
      inr : ∥ B ∥ₐ ⟿ ∥ A+B ∥ₐ

      _[_,_] : ∀ {d ℓ₄} (X : Model {d} {ℓ₄})
               → ∥ A ∥ₐ ⟿ ∥ X ∥ₐ
               → ∥ B ∥ₐ ⟿ ∥ X ∥ₐ
               → ∥ A+B ∥ₐ ⟿ ∥ X ∥ₐ

      commute₁ : ∀ {d ℓ₄} {X : Model {d} {ℓ₄}}
                 → {f : ∥ A ∥ₐ ⟿ ∥ X ∥ₐ}
                 → {g : ∥ B ∥ₐ ⟿ ∥ X ∥ₐ}
                 → X [ f , g ] ⊙ inl ≗ f

      commute₂ : ∀ {d ℓ₄} {X : Model {d} {ℓ₄}}
                 → {f : ∥ A ∥ₐ ⟿ ∥ X ∥ₐ}
                 → {g : ∥ B ∥ₐ ⟿ ∥ X ∥ₐ}
                 → X [ f , g ] ⊙ inr ≗ g

      universal : ∀ {d ℓ₄} {X : Model {d} {ℓ₄}}
                  → {f : ∥ A ∥ₐ ⟿ ∥ X ∥ₐ}
                  → {g : ∥ B ∥ₐ ⟿ ∥ X ∥ₐ}
                  → {h : ∥ A+B ∥ₐ ⟿ ∥ X ∥ₐ}
                  → h ⊙ inl ≗ f
                  → h ⊙ inr ≗ g
                  → X [ f , g ] ≗ h

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
-- Parametrised maps of families and their coalgebraic properties
module SOAS.Coalgebraic.Map {T : Set} where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core {T}
open import SOAS.Abstract.Hom {T}
import SOAS.Abstract.Box {T} as □ ;  open □.Sorted
import SOAS.Abstract.Coalgebra {T} as →□ ; open →□.Sorted

private
  variable
    𝒳 𝒴 𝒫 : Familyₛ
    Γ Δ Θ : Ctx
    α : T

record Coalgebraic (𝒳ᴮ : Coalgₚ 𝒳)(𝒫ᴮ : Coalgₚ 𝒫)(𝒴ᴮ : Coalgₚ 𝒴)
                   (f : 𝒳 ⇾̣ 〖 𝒫 , 𝒴 〗) : Set where
  private module 𝒳 = Coalgₚ 𝒳ᴮ
  private module 𝒫 = Coalgₚ 𝒫ᴮ
  private module 𝒴 = Coalgₚ 𝒴ᴮ

  -- Interaction between the point and renaming of all three coalgebras
  field
    r∘f : {σ : Γ ~[ 𝒫 ]↝ Δ}{ϱ : Δ ↝ Θ}{t : 𝒳 α Γ}
        → 𝒴.r (f t σ) ϱ ≡ f t (λ v → 𝒫.r (σ v) ϱ)

    f∘r : {ρ : Γ ↝ Δ}{ς : Δ ~[ 𝒫 ]↝ Θ}{t : 𝒳 α Γ}
        → f (𝒳.r t ρ) ς ≡ f t (ς ∘ ρ)

    f∘η : {v : ℐ α Γ} → f (𝒳.η v) 𝒫.η ≡ 𝒴.η v

  -- Codomain of coalgebraic map is a pointed coalgebra
  〖𝒫,𝒴〗ᴮ : Coalgₚ 〖 𝒫 , 𝒴 〗
  〖𝒫,𝒴〗ᴮ = record
    { ᵇ = record { r = λ h ρ σ → h (σ ∘ ρ) ; counit = refl ; comult = refl }
    ; η = λ v σ → f (𝒳.η v) σ
    ; r∘η = dext (λ σ → trans (sym f∘r) (congr 𝒳.r∘η (λ - → f - σ))) }

  -- The map is a pointed coalgebra homomorphism
  ᴮ⇒ : Coalgₚ⇒ 𝒳ᴮ 〖𝒫,𝒴〗ᴮ f
  ᴮ⇒ = record { ᵇ⇒ = record { ⟨r⟩ = dext′ f∘r } ; ⟨η⟩ = refl }

  -- Equality of two substitutions at the new index extends to equality of
  -- transforming new variables with the substitution
  eq-at-new : {σ : α ∙ Γ ~[ 𝒫 ]↝ α ∙ Θ}
              {ς : α ∙ Δ ~[ 𝒫 ]↝ α ∙ Θ}
           → σ new ≡ ς new
           → f (𝒳.η new) σ ≡ f (𝒳.η new) ς
  eq-at-new {σ = σ} {ς} eq = begin
         f (𝒳.η new) σ           ≡⟨⟩
         f (𝒳.η (ι new)) σ      ≡˘⟨ cong (λ - → f - σ) (𝒳.r∘η) ⟩
         f (𝒳.r (𝒳.η new) ι) σ  ≡⟨ f∘r ⟩
         f (𝒳.η new) (σ ∘ ι)    ≡⟨ cong (f (𝒳.η new)) (dext (λ{ new → eq })) ⟩
         f (𝒳.η new) (ς ∘ ι)    ≡˘⟨ f∘r ⟩
         f (𝒳.r (𝒳.η new) ι) ς  ≡⟨ cong (λ - → f - ς) (𝒳.r∘η) ⟩
         f (𝒳.η (ι new)) ς      ≡⟨⟩
         f (𝒳.η new) ς          ∎
    where
    open ≡-Reasoning
    open Coalgₚ
    ι : (α ∙ ∅) ↝ (α ∙ Δ)
    ι new = new

-- Application for a pointed coalgebra is coalgebraic
jᶜ : (𝒳ᴮ : Coalgₚ 𝒳) → Coalgebraic ℐᴮ 𝒳ᴮ 𝒳ᴮ (j 𝒳)
jᶜ 𝒳ᴮ = record { r∘f = refl ; f∘r = refl ; f∘η = refl }

-- Renaming of pointed coalgebr is coalgebraic
rᶜ : (𝒳ᴮ : Coalgₚ 𝒳) → Coalgebraic 𝒳ᴮ ℐᴮ 𝒳ᴮ (Coalgₚ.r 𝒳ᴮ)
rᶜ 𝒳ᴮ = record { r∘f = sym comult ; f∘r = sym comult ; f∘η = r∘η }
  where open Coalgₚ 𝒳ᴮ

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Strings: builtin type and basic operations
------------------------------------------------------------------------

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

module Data.String.Base where

open import Level using (zero)
open import Data.Bool using (true; false)
open import Data.Nat.Base as ℕ using (ℕ; _∸_; ⌊_/2⌋; ⌈_/2⌉)
import Data.Nat.Properties as ℕₚ
open import Data.List.Base as List using (List; [_])
open import Data.List.NonEmpty as NE using (List⁺)
open import Data.List.Extrema ℕₚ.≤-totalOrder
open import Data.List.Relation.Binary.Pointwise using (Pointwise)
open import Data.List.Relation.Binary.Lex.Strict using (Lex-<)
open import Data.Vec.Base as Vec using (Vec)
open import Data.Char.Base as Char using (Char)
import Data.Char.Properties as Char using (_≟_)
open import Function
open import Relation.Binary using (Rel)
open import Relation.Nullary using (does)

open import Data.List.Membership.DecPropositional Char._≟_

------------------------------------------------------------------------
-- From Agda.Builtin: type and renamed primitives

-- Note that we do not re-export primStringAppend because we want to
-- give it an infix definition and be able to assign it a level.

import Agda.Builtin.String as String

open String public using ( String )
  renaming
  ( primStringToList   to toList
  ; primStringFromList to fromList
  ; primShowString     to show
  )

------------------------------------------------------------------------
-- Relations

-- Pointwise equality on Strings

infix 4 _≈_
_≈_ : Rel String zero
_≈_ = Pointwise Char._≈_ on toList

-- Lexicographic ordering on Strings

infix 4 _<_
_<_ : Rel String zero
_<_ = Lex-< Char._≈_ Char._<_ on toList

------------------------------------------------------------------------
-- Operations

-- Additional conversion functions

fromChar : Char → String
fromChar = fromList ∘′ [_]

fromList⁺ : List⁺ Char → String
fromList⁺ = fromList ∘′ NE.toList

-- List-like functions

infixr 5 _++_
_++_ : String → String → String
_++_ = String.primStringAppend

length : String → ℕ
length = List.length ∘ toList

replicate : ℕ → Char → String
replicate n = fromList ∘ List.replicate n

concat : List String → String
concat = List.foldr _++_ ""

intersperse : String → List String → String
intersperse sep = concat ∘′ (List.intersperse sep)

-- String-specific functions

unlines : List String → String
unlines = intersperse "\n"

unwords : List String → String
unwords = intersperse " "

parens : String → String
parens s = "(" ++ s ++ ")"

-- enclose string with parens if it contains a space character
parensIfSpace : String → String
parensIfSpace s with does (' ' ∈? toList s)
... | true  = parens s
... | false = s

braces : String → String
braces s = "{" ++ s ++ "}"

-- append that also introduces spaces, if necessary
infixr 5 _<+>_
_<+>_ : String → String → String
"" <+> b = b
a <+> "" = a
a <+> b = a ++ " " ++ b

------------------------------------------------------------------------
-- Padding

-- Each one of the padding functions should verify the following
-- invariant:
--   If length str ≤ n then length (padLeft c n str) ≡ n
--   and otherwise padLeft c n str ≡ str.

-- Appending an empty string is expensive (append for Haskell's
-- Text creates a fresh Text value in which both contents are
-- copied) so we precompute `n ∸ length str` and check whether
-- it is equal to 0.

padLeft : Char → ℕ → String → String
padLeft c n str with n ∸ length str
... | 0 = str
... | l = replicate l c ++ str

padRight : Char → ℕ → String → String
padRight c n str with n ∸ length str
... | 0 = str
... | l = str ++ replicate l c

padBoth : Char → Char → ℕ → String → String
padBoth cₗ cᵣ n str with n ∸ length str
... | 0 = str
... | l = replicate ⌊ l /2⌋ cₗ ++ str ++ replicate ⌈ l /2⌉ cᵣ

------------------------------------------------------------------------
-- Alignment

-- We can align a String left, center or right in a column of a given
-- width by padding it with whitespace.

data Alignment : Set where
  Left Center Right : Alignment

fromAlignment : Alignment → ℕ → String → String
fromAlignment Left   = padRight ' '
fromAlignment Center = padBoth ' ' ' '
fromAlignment Right  = padLeft ' '

------------------------------------------------------------------------
-- Rectangle

-- Build a rectangular column by:
-- Given a vector of cells and a padding function for each one
-- Compute the max of the widths, and pad the strings accordingly.

rectangle : ∀ {n} → Vec (ℕ → String → String) n →
            Vec String n → Vec String n
rectangle pads cells = Vec.zipWith (λ p c → p width c) pads cells where

  sizes = List.map length (Vec.toList cells)
  width = max 0 sizes

-- Special cases for left, center, and right alignment

rectangleˡ : ∀ {n} → Char → Vec String n → Vec String n
rectangleˡ c = rectangle (Vec.replicate $ padLeft c)

rectangleʳ : ∀ {n} → Char → Vec String n → Vec String n
rectangleʳ c = rectangle (Vec.replicate $ padRight c)

rectangleᶜ : ∀ {n} → Char → Char → Vec String n → Vec String n
rectangleᶜ cₗ cᵣ = rectangle (Vec.replicate $ padBoth cₗ cᵣ)


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

module Data.Array where

open import Data.Binary
open import Prelude

private
  variable
    ns : 𝔹

record 2× {a} (A : Type a) : Type a where
  eta-equality
  constructor _⊛_
  field
    pr₁ pr₂ : A
open 2× public

infixr 5 _∷₁_ _∷₂_ _∷_

mutual
  record Array0ᵇ {a} : Type a where
    eta-equality
    constructor []

  record Array1ᵇ {a} (A : Type a) (ns : 𝔹) : Type a where
    eta-equality
    inductive
    constructor _∷₁_
    field
      head1ᵇ : A
      tail1ᵇ : Array (2× A) ns

  record Array2ᵇ {a} (A : Type a) (ns : 𝔹) : Type a where
    eta-equality
    inductive
    constructor _∷₂_
    field
      head2ᵇ : 2× A
      tail2ᵇ : Array (2× A) ns

  Array : Type a → 𝔹 → Type a
  Array A 0ᵇ = Array0ᵇ
  Array A (1ᵇ ns) = Array1ᵇ A ns
  Array A (2ᵇ ns) = Array2ᵇ A ns

_∷_ : A → Array A ns → Array A (inc ns)
_∷_ {ns = 0ᵇ} x xs = x ∷₁ xs
_∷_ {ns = 1ᵇ ns} x₁ (x₂ ∷₁ xs) = (x₁ ⊛ x₂) ∷₂ xs
_∷_ {ns = 2ᵇ ns} x₁ (x₂ ∷₂ xs) = x₁ ∷₁ x₂ ∷ xs

open import Lens

⦅head1ᵇ⦆ : Lens (Array A (1ᵇ ns)) A
⦅head1ᵇ⦆ .fst (x ∷₁ xs) = lens-part x (_∷₁ xs)
⦅head1ᵇ⦆ .snd .get-set xs v i = v
⦅head1ᵇ⦆ .snd .set-get xs i = xs
⦅head1ᵇ⦆ .snd .set-set (x ∷₁ xs) v₁ v₂ i = v₂ ∷₁ xs

⦅head2ᵇ⦆ : Lens (Array A (2ᵇ ns)) (2× A)
⦅head2ᵇ⦆ .fst (x ∷₂ xs) = lens-part x (_∷₂ xs)
⦅head2ᵇ⦆ .snd .get-set (x ∷₂ xs) v i = v
⦅head2ᵇ⦆ .snd .set-get (x ∷₂ xs) i = x ∷₂ xs
⦅head2ᵇ⦆ .snd .set-set (x ∷₂ xs) v₁ v₂ i = v₂ ∷₂ xs

⦅tail1ᵇ⦆ : Lens (Array A (1ᵇ ns)) (Array (2× A) ns)
⦅tail1ᵇ⦆ .fst (x ∷₁ xs) = lens-part xs (x ∷₁_)
⦅tail1ᵇ⦆ .snd .get-set (x ∷₁ xs) v i = v
⦅tail1ᵇ⦆ .snd .set-get (x ∷₁ xs) i = x ∷₁ xs
⦅tail1ᵇ⦆ .snd .set-set (x ∷₁ xs) v₁ v₂ i = x ∷₁ v₂

⦅tail2ᵇ⦆ : Lens (Array A (2ᵇ ns)) (Array (2× A) ns)
⦅tail2ᵇ⦆ .fst (x ∷₂ xs) = lens-part xs (x ∷₂_)
⦅tail2ᵇ⦆ .snd .get-set (x ∷₂ xs) v i = v
⦅tail2ᵇ⦆ .snd .set-get (x ∷₂ xs) i = x ∷₂ xs
⦅tail2ᵇ⦆ .snd .set-set (x ∷₂ xs) v₁ v₂ i = x ∷₂ v₂

⦅pr₁⦆ : Lens (2× A) A
⦅pr₁⦆ .fst (x ⊛ y) = lens-part x (_⊛ y)
⦅pr₁⦆ .snd .get-set s v i = v
⦅pr₁⦆ .snd .set-get s i = s
⦅pr₁⦆ .snd .set-set s v₁ v₂ i = v₂ ⊛ s .pr₂

⦅pr₂⦆ : Lens (2× A) A
⦅pr₂⦆ .fst (x ⊛ y) = lens-part y (x ⊛_)
⦅pr₂⦆ .snd .get-set s v i = v
⦅pr₂⦆ .snd .set-get s i = s
⦅pr₂⦆ .snd .set-set s v₁ v₂ i = s .pr₁ ⊛ v₂

open import Data.Binary.Order

mutual
  index : ∀ is {js} → is < js → Lens (Array A js) A
  index 0ᵇ      {1ᵇ js} p = ⦅head1ᵇ⦆
  index 0ᵇ      {2ᵇ js} p = ⦅head2ᵇ⦆ ⋯ ⦅pr₁⦆
  index (1ᵇ is) {js}    p = ind₂1ᵇ is p
  index (2ᵇ is) {1ᵇ js} p = ⦅tail1ᵇ⦆ ⋯ index is p ⋯ ⦅pr₂⦆
  index (2ᵇ is) {2ᵇ js} p = ⦅tail2ᵇ⦆ ⋯ index is p ⋯ ⦅pr₁⦆

  ind₂1ᵇ : ∀ is {js} → 1ᵇ is < js → Lens (Array A js) A
  ind₂1ᵇ is      {1ᵇ js} p = ⦅tail1ᵇ⦆ ⋯ index is p ⋯ ⦅pr₁⦆
  ind₂1ᵇ 0ᵇ      {2ᵇ js} p = ⦅head2ᵇ⦆ ⋯ ⦅pr₂⦆
  ind₂1ᵇ (1ᵇ is) {2ᵇ js} p = ⦅tail2ᵇ⦆ ⋯ ind₃ is p ⋯ ⦅pr₂⦆
  ind₂1ᵇ (2ᵇ is) {2ᵇ js} p = ⦅tail2ᵇ⦆ ⋯ ind₂2ᵇ is p ⋯ ⦅pr₂⦆

  ind₂2ᵇ : ∀ is {js} → 2ᵇ is ≤ js → Lens (Array A js) A
  ind₂2ᵇ is      {1ᵇ js} p = ⦅tail1ᵇ⦆ ⋯ index is p ⋯ ⦅pr₁⦆
  ind₂2ᵇ 0ᵇ      {2ᵇ js} p = ⦅head2ᵇ⦆ ⋯ ⦅pr₂⦆
  ind₂2ᵇ (1ᵇ is) {2ᵇ js} p = ⦅tail2ᵇ⦆ ⋯ ind₃ is p ⋯ ⦅pr₂⦆
  ind₂2ᵇ (2ᵇ is) {2ᵇ js} p = ⦅tail2ᵇ⦆ ⋯ ind₂2ᵇ is p ⋯ ⦅pr₂⦆

  ind₃ : ∀ is {js} → 1ᵇ is ≤ js → Lens (Array A js) A
  ind₃ 0ᵇ      {1ᵇ js} p = ⦅head1ᵇ⦆
  ind₃ 0ᵇ      {2ᵇ js} p = ⦅head2ᵇ⦆ ⋯ ⦅pr₁⦆
  ind₃ (1ᵇ is) {1ᵇ js} p = ⦅tail1ᵇ⦆ ⋯ ind₃ is p ⋯ ⦅pr₂⦆
  ind₃ (1ᵇ is) {2ᵇ js} p = ⦅tail2ᵇ⦆ ⋯ ind₃ is p ⋯ ⦅pr₁⦆
  ind₃ (2ᵇ is) {1ᵇ js} p = ⦅tail1ᵇ⦆ ⋯ ind₂2ᵇ is p ⋯ ⦅pr₂⦆
  ind₃ (2ᵇ is) {2ᵇ js} p = ⦅tail2ᵇ⦆ ⋯ ind₂2ᵇ is p ⋯ ⦅pr₁⦆

at : ∀ is {js} → {p : is < js} → Lens (Array A js) A
at is {p = p} = index is p

import Data.Nat as ℕ

foldrP : ∀ {p} (P : ℕ → Type p) → (∀ {n} → A → P n → P (suc n)) → P zero → Array A ns → P ⟦ ns ⇓⟧
foldrP {ns = 0ᵇ} P f b [] = b
foldrP {ns = 1ᵇ ns} P f b (x ∷₁ xs) = f x (foldrP (λ n → P (n ℕ.* 2)) (λ { (x₁ ⊛ x₂) b → f x₁ (f x₂ b) }) b xs)
foldrP {ns = 2ᵇ ns} P f b ((x₁ ⊛ x₂) ∷₂ xs) = f x₁ (f x₂ (foldrP (λ n → P (n ℕ.* 2)) (λ { (x₁ ⊛ x₂) b → f x₁ (f x₂ b)}) b xs))

foldr : (A → B → B) → B → Array A ns → B
foldr f b = foldrP (λ _ → _) f b

map : (A → B) → Array A ns → Array B ns
map {ns = 0ᵇ}    f xs = []
map {ns = 1ᵇ ns} f (x ∷₁ xs) = f x ∷₁ map (λ { (x₁ ⊛ x₂) → f x₁ ⊛ f x₂ }) xs
map {ns = 2ᵇ ns} f ((x₁ ⊛ x₂) ∷₂ xs) = (f x₁ ⊛ f x₂) ∷₂ map (λ { (x₁ ⊛ x₂) → f x₁ ⊛ f x₂ }) xs

import Data.List as List
open import Data.List using (List)

toList : Array A ns → List.List A
toList = foldr List._∷_ List.[]

fromList : (xs : List A) → Array A ⟦ List.length xs ⇑⟧
fromList List.[] = []
fromList (x List.∷ xs) = x ∷ fromList xs

-- Lens laws are satisfied definitionally:

-- get-set
_ : (xs : Array ℕ ⟦ 10 ⇑⟧) (n : ℕ) →  (xs [ at ⟦ 5 ⇑⟧ ]≔ n [ at ⟦ 5 ⇑⟧ ]) ≡ n
_ = λ xs n → refl

-- set-get
_ : (xs : Array ℕ ⟦ 10 ⇑⟧) → (xs [ at ⟦ 5 ⇑⟧ ]≔ (xs [ at ⟦ 5 ⇑⟧ ])) ≡ xs
_ = λ xs → refl

-- set-set
_ : (xs : Array ℕ ⟦ 10 ⇑⟧) (n m : ℕ) → (xs [ at ⟦ 5 ⇑⟧ ]≔ n [ at ⟦ 5 ⇑⟧ ]≔ m) ≡ (xs [ at ⟦ 5 ⇑⟧ ]≔ m)
_ = λ xs n m → refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

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

import      LibraBFT.Impl.Consensus.ConsensusTypes.VoteData as VoteData
open import LibraBFT.Impl.OBM.Crypto                        hiding (verify)
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Types.ValidatorVerifier           as ValidatorVerifier
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Hash
open import Util.PKCS                                       hiding (verify)
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                     using (String)

module LibraBFT.Impl.Consensus.ConsensusTypes.Vote where

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

timeout : Vote → Timeout

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

newWithSignature : VoteData → Author → LedgerInfo → Signature → Vote
newWithSignature voteData author ledgerInfo signature =
  Vote∙new voteData author ledgerInfo signature nothing

verify : Vote → ValidatorVerifier → Either ErrLog Unit
verify self validator = do
  lcheck (self ^∙ vLedgerInfo ∙ liConsensusDataHash == hashVD (self ^∙ vVoteData))
         (here' ("Vote's hash mismatch with LedgerInfo" ∷ []))
  withErrCtx' (here' ("vote" ∷ []))
    (ValidatorVerifier.verify validator (self ^∙ vAuthor) (self ^∙ vLedgerInfo) (self ^∙ vSignature))
  case self ^∙ vTimeoutSignature of λ where
    nothing    → pure unit
    (just tos) →
      withErrCtx' (here' ("timeout" ∷ []))
        (ValidatorVerifier.verify validator (self ^∙ vAuthor) (timeout self) tos)
  withErrCtx' (here' ("VoteData" ∷ [])) (VoteData.verify (self ^∙ vVoteData))
 where
  here' : List String → List String
  here' t = "Vote" ∷ "verify" ∷ "failed" {-∷lsV self-} ∷ t

addTimeoutSignature : Vote → Signature → Vote
addTimeoutSignature self sig =
  if is-just (self ^∙ vTimeoutSignature)
  then self
  else self & vTimeoutSignature ?~ sig

timeout v =
  Timeout∙new (v ^∙ vVoteData ∙ vdProposed ∙ biEpoch) (v ^∙ vVoteData ∙ vdProposed ∙ biRound)

isTimeout : Vote → Bool
isTimeout v = is-just (v ^∙ vTimeoutSignature)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Instantiates the ring solver, using the natural numbers as the
-- coefficient "ring"
------------------------------------------------------------------------

open import Algebra
import Algebra.Operations
open import Relation.Nullary

module Algebra.RingSolver.Natural-coefficients
         {r₁ r₂}
         (R : CommutativeSemiring r₁ r₂)
         (dec : let open CommutativeSemiring R
                    open Algebra.Operations semiring in
                ∀ m n → Dec (m × 1# ≈ n × 1#)) where

import Algebra.RingSolver
open import Algebra.RingSolver.AlmostCommutativeRing
open import Data.Nat as ℕ
open import Data.Product using (module Σ)
open import Function
import Relation.Binary.EqReasoning
import Relation.Nullary.Decidable as Dec

open CommutativeSemiring R
open Algebra.Operations semiring
open Relation.Binary.EqReasoning setoid

private

  -- The coefficient "ring".

  ℕ-ring : RawRing _
  ℕ-ring = record
    { Carrier = ℕ
    ; _+_     = ℕ._+_
    ; _*_     = ℕ._*_
    ; -_      = id
    ; 0#      = 0
    ; 1#      = 1
    }

  -- There is a homomorphism from ℕ to R.
  --
  -- Note that _×′_ is used rather than _×_. If _×_ were used, then
  -- Function.Related.TypeIsomorphisms.test would fail to type-check.

  homomorphism :
    ℕ-ring -Raw-AlmostCommutative⟶ fromCommutativeSemiring R
  homomorphism = record
    { ⟦_⟧    = λ n → n ×′ 1#
    ; +-homo = ×′-homo-+ 1#
    ; *-homo = ×′1-homo-*
    ; -‿homo = λ _ → refl
    ; 0-homo = refl
    ; 1-homo = refl
    }

  -- Equality of certain expressions can be decided.

  dec′ : ∀ m n → Dec (m ×′ 1# ≈ n ×′ 1#)
  dec′ m n = Dec.map′ to from (dec m n)
    where
    to : m × 1# ≈ n × 1# → m ×′ 1# ≈ n ×′ 1#
    to m≈n = begin
      m ×′ 1#  ≈⟨ sym $ ×≈×′ m 1# ⟩
      m ×  1#  ≈⟨ m≈n ⟩
      n ×  1#  ≈⟨ ×≈×′ n 1# ⟩
      n ×′ 1#  ∎

    from : m ×′ 1# ≈ n ×′ 1# → m × 1# ≈ n × 1#
    from m≈n = begin
      m ×  1#  ≈⟨ ×≈×′ m 1# ⟩
      m ×′ 1#  ≈⟨ m≈n ⟩
      n ×′ 1#  ≈⟨ sym $ ×≈×′ n 1# ⟩
      n ×  1#  ∎

-- The instantiation.

open Algebra.RingSolver _ _ homomorphism dec′ public