text:
------------------------------------------------------------------------
-- Queue instances for the queues in Queue.Quotiented
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

import Equality.Path as P
open import Prelude
import Queue

module Queue.Quotiented.Instances
  {e⁺}
  (eq : ∀ {a p} → P.Equality-with-paths a p e⁺)
  (open P.Derived-definitions-and-properties eq)

  {Q : ∀ {ℓ} → Type ℓ → Type ℓ}
  ⦃ is-queue :
      ∀ {ℓ} → Queue.Is-queue equality-with-J Q (λ _ → ↑ _ ⊤) ℓ ⦄
  ⦃ is-queue-with-map :
      ∀ {ℓ₁ ℓ₂} → Queue.Is-queue-with-map equality-with-J Q ℓ₁ ℓ₂ ⦄
  where

open Queue equality-with-J
open import Queue.Quotiented eq as Q using (Queue)

open import Bijection equality-with-J using (_↔_)
open import H-level.Closure equality-with-J
open import List equality-with-J as L hiding (map)
open import Maybe equality-with-J
open import Monad equality-with-J hiding (map)

private
  variable
    a ℓ ℓ₁ ℓ₂ : Level
    A         : Type a
    xs        : List A

instance

  -- Instances.

  Queue-is-queue : Is-queue (Queue Q) Is-set ℓ
  Queue-is-queue .Is-queue.to-List           = Q.to-List
  Queue-is-queue .Is-queue.from-List         = Q.from-List
  Queue-is-queue .Is-queue.to-List-from-List = Q.to-List-from-List
  Queue-is-queue .Is-queue.enqueue           = Q.enqueue
  Queue-is-queue .Is-queue.to-List-enqueue   = Q.to-List-enqueue
  Queue-is-queue .Is-queue.dequeue           = Q.dequeue
  Queue-is-queue .Is-queue.to-List-dequeue   = Q.to-List-dequeue
  Queue-is-queue .Is-queue.dequeue⁻¹         = Q.dequeue⁻¹
  Queue-is-queue .Is-queue.to-List-dequeue⁻¹ = Q.to-List-dequeue⁻¹

  Queue-is-queue-with-map : Is-queue-with-map (Queue Q) ℓ₁ ℓ₂
  Queue-is-queue-with-map .Is-queue-with-map.map         = Q.map
  Queue-is-queue-with-map .Is-queue-with-map.to-List-map = Q.to-List-map

  Queue-is-queue-with-unique-representations :
    Is-queue-with-unique-representations (Queue Q) ℓ
  Queue-is-queue-with-unique-representations
    .Is-queue-with-unique-representations.from-List-to-List =
    Q.from-List-to-List _

------------------------------------------------------------------------
-- Some examples

private

  ⌊_⌋      = to-List (λ {_ _} → ℕ-set)
  dequeue′ = dequeue (λ {_ _} → ℕ-set)
  empty′   = empty ⦂ Queue Q ℕ

  example₁ : map suc (enqueue 3 empty) ≡ enqueue 4 empty′
  example₁ = _↔_.to ≡-for-lists↔≡ (
    ⌊ map suc (enqueue 3 empty) ⌋  ≡⟨ to-List-map ⟩
    L.map suc ⌊ enqueue 3 empty ⌋  ≡⟨ cong (L.map suc) $ to-List-foldl-enqueue-empty (_ ∷ []) ⟩
    L.map suc (3 ∷ [])             ≡⟨⟩
    4 ∷ []                         ≡⟨ sym $ to-List-foldl-enqueue-empty (_ ∷ []) ⟩∎
    ⌊ enqueue 4 empty ⌋            ∎)

  example₂ :
    dequeue′ (map (_* 2) (enqueue 3 (enqueue 5 empty))) ≡
    just (10 , enqueue 6 empty)
  example₂ =
    dequeue′ (map (_* 2) (enqueue 3 (enqueue 5 empty)))  ≡⟨ cong dequeue′ lemma ⟩
    dequeue′ (cons 10 (enqueue 6 empty))                 ≡⟨ _↔_.right-inverse-of (Queue↔Maybe[×Queue] _) _ ⟩∎
    just (10 , enqueue 6 empty)                          ∎
    where
    lemma = _↔_.to ≡-for-lists↔≡ (
      ⌊ map (_* 2) (enqueue 3 (enqueue 5 empty)) ⌋  ≡⟨ to-List-map ⟩
      L.map (_* 2) ⌊ enqueue 3 (enqueue 5 empty) ⌋  ≡⟨ cong (L.map (_* 2)) $ to-List-foldl-enqueue-empty (_ ∷ _ ∷ []) ⟩
      L.map (_* 2) (5 ∷ 3 ∷ [])                     ≡⟨⟩
      10 ∷ 6 ∷ []                                   ≡⟨ cong (10 ∷_) $ sym $ to-List-foldl-enqueue-empty (_ ∷ []) ⟩
      10 ∷ ⌊ enqueue 6 empty ⌋                      ≡⟨ sym $ to-List-cons ⟩∎
      ⌊ cons 10 (enqueue 6 empty) ⌋                 ∎)

  example₃ :
    (do x , q ← dequeue′ (map (_* 2) (enqueue 3 (enqueue 5 empty)))
        return (enqueue (3 * x) q)) ≡
    just (enqueue 30 (enqueue 6 empty))
  example₃ =
    (do x , q ← dequeue′ (map (_* 2) (enqueue 3 (enqueue 5 empty)))
        return (enqueue (3 * x) q))                                  ≡⟨ cong (_>>= λ _ → return (enqueue _ _)) example₂ ⟩

    (do x , q ← just (10 , enqueue 6 empty)
        return (enqueue (3 * x) (q ⦂ Queue Q ℕ)))                    ≡⟨⟩

    just (enqueue 30 (enqueue 6 empty))                              ∎

  example₄ :
    (do x , q ← dequeue′ (map (_* 2) (enqueue 3 (enqueue 5 empty)))
        let q = enqueue (3 * x) q
        return ⌊ q ⌋) ≡
    just (6 ∷ 30 ∷ [])
  example₄ =
    (do x , q ← dequeue′ (map (_* 2) (enqueue 3 (enqueue 5 empty)))
        let q = enqueue (3 * x) q
        return ⌊ q ⌋)                                                ≡⟨ cong (_>>= λ _ → return ⌊ enqueue _ _ ⌋) example₂ ⟩

    (do x , q ← just (10 , enqueue 6 empty)
        let q = enqueue (3 * x) (q ⦂ Queue Q ℕ)
        return ⌊ q ⌋)                                                ≡⟨⟩

    just ⌊ enqueue 30 (enqueue 6 empty) ⌋                            ≡⟨ cong just $ to-List-foldl-enqueue-empty (_ ∷ _ ∷ []) ⟩∎

    just (6 ∷ 30 ∷ [])                                               ∎

  example₅ :
    ∀ {xs} →
    dequeue′ (from-List (1 ∷ 2 ∷ 3 ∷ xs)) ≡
    just (1 , from-List (2 ∷ 3 ∷ xs))
  example₅ {xs = xs} =
    dequeue′ (from-List (1 ∷ 2 ∷ 3 ∷ xs))       ≡⟨ cong dequeue′ lemma ⟩
    dequeue′ (cons 1 (from-List (2 ∷ 3 ∷ xs)))  ≡⟨ _↔_.right-inverse-of (Queue↔Maybe[×Queue] _) _ ⟩∎
    just (1 , from-List (2 ∷ 3 ∷ xs))           ∎
    where
    lemma = _↔_.to ≡-for-lists↔≡ (
      ⌊ from-List (1 ∷ 2 ∷ 3 ∷ xs) ⌋       ≡⟨ _↔_.right-inverse-of (Queue↔List _) _ ⟩
      1 ∷ 2 ∷ 3 ∷ xs                       ≡⟨ cong (1 ∷_) $ sym $ _↔_.right-inverse-of (Queue↔List _) _ ⟩
      1 ∷ ⌊ from-List (2 ∷ 3 ∷ xs) ⌋       ≡⟨ sym to-List-cons ⟩∎
      ⌊ cons 1 (from-List (2 ∷ 3 ∷ xs)) ⌋  ∎)

  example₆ :
    foldr enqueue empty′ (3 ∷ 2 ∷ 1 ∷ []) ≡
    from-List (1 ∷ 2 ∷ 3 ∷ [])
  example₆ = sym $ from-List≡foldl-enqueue-empty (λ {_ _} → ℕ-set)


text:
postulate
  __ : Set

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Multidimensional.Data.NNat.Properties where

open import Cubical.Core.Glue

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

open import Cubical.Data.Nat
open import Cubical.Data.Prod
open import Cubical.Data.Empty

open import Cubical.Relation.Nullary

open import Multidimensional.Data.Extra.Nat
open import Multidimensional.Data.Dir
open import Multidimensional.Data.DirNum
open import Multidimensional.Data.NNat.Base

-- N→ℕsucN : (r : ℕ) (x : N r) → N→ℕ r (sucN x) ≡ suc (N→ℕ r x)
-- N→ℕsucN zero (bn tt) = refl
-- N→ℕsucN zero (xr tt x) =
--     suc (N→ℕ zero (sucN x))
--   ≡⟨ cong suc (N→ℕsucN zero x) ⟩
--     suc (suc (N→ℕ zero x))
--   ∎
-- N→ℕsucN (suc r) (bn (↓ , d)) = refl
-- N→ℕsucN (suc r) (bn (↑ , d)) with max? d
-- ... | no d≠max =
--           doubleℕ (DirNum→ℕ (next d))
--         ≡⟨ cong doubleℕ (next≡suc r d d≠max)  ⟩
--           doubleℕ (suc (DirNum→ℕ d))
--         ∎
-- ... | yes d≡max = -- this can probably be shortened by not reducing down to zero
--           sucn (doubleℕ (DirNum→ℕ (zero-n r)))
--             (doublesℕ r (suc (suc (doubleℕ (doubleℕ (DirNum→ℕ (zero-n r)))))))
--         ≡⟨ cong (λ x → sucn (doubleℕ x) (doublesℕ r (suc (suc (doubleℕ (doubleℕ x)))))) (zero-n→0 {r}) ⟩
--           sucn (doubleℕ zero) (doublesℕ r (suc (suc (doubleℕ (doubleℕ zero)))))
--         ≡⟨ refl ⟩
--           doublesℕ (suc r) (suc zero) -- 2^(r+1)
--         ≡⟨ sym (doubleDoubles r 1) ⟩
--           doubleℕ (doublesℕ r (suc zero)) --2*2^r
--         ≡⟨ sym (sucPred (doubleℕ (doublesℕ r (suc zero))) (doubleDoublesOne≠0 r)) ⟩
--           suc (predℕ (doubleℕ (doublesℕ r (suc zero))))
--         ≡⟨ cong suc (sym (sucPred (predℕ (doubleℕ (doublesℕ r (suc zero)))) (predDoubleDoublesOne≠0 r))) ⟩
--           suc (suc (predℕ (predℕ (doubleℕ (doublesℕ r (suc zero))))))
--         ≡⟨ cong (λ x → suc (suc x)) (sym (doublePred (doublesℕ r (suc zero)))) ⟩
--           suc (suc (doubleℕ (predℕ (doublesℕ r (suc zero)))))
--         ≡⟨ cong (λ x → suc (suc (doubleℕ x))) (sym (maxr≡pred2ʳ r d d≡max)) ⟩
--           suc (suc (doubleℕ (DirNum→ℕ d))) -- 2*(2^r - 1) + 2 = 2^(r+1) - 2 + 2 = 2^(r+1)
--         ∎
-- N→ℕsucN (suc r) (xr (↓ , d) x) = refl
-- N→ℕsucN (suc r) (xr (↑ , d) x) with max? d
-- ... | no d≠max =
--           sucn (doubleℕ (DirNum→ℕ (next d)))
--            (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))
--         ≡⟨ cong (λ y → sucn (doubleℕ y) (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))) (next≡suc r d d≠max) ⟩
--           sucn (doubleℕ (suc (DirNum→ℕ d)))
--            (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))
--         ≡⟨ refl ⟩
--           suc
--            (suc
--             (iter (doubleℕ (DirNum→ℕ d)) suc
--             (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))
--         ∎
-- ... | yes d≡max =
--         sucn (doubleℕ (DirNum→ℕ (zero-n r)))
--         (doublesℕ r (doubleℕ (N→ℕ (suc r) (sucN x))))
--       ≡⟨ cong (λ z → sucn (doubleℕ z) (doublesℕ r (doubleℕ (N→ℕ (suc r) (sucN x))))) (zero-n≡0 {r}) ⟩
--         sucn (doubleℕ zero)
--         (doublesℕ r (doubleℕ (N→ℕ (suc r) (sucN x))))
--       ≡⟨ refl ⟩
--         doublesℕ r (doubleℕ (N→ℕ (suc r) (sucN x)))
--       ≡⟨ cong (λ x → doublesℕ r (doubleℕ x)) (N→ℕsucN (suc r) x)  ⟩
--         doublesℕ r (doubleℕ (suc (N→ℕ (suc r) x)))
--       ≡⟨ refl ⟩
--         doublesℕ r (suc (suc (doubleℕ (N→ℕ (suc r) x)))) -- 2^r * (2x + 2) = 2^(r+1)x + 2^(r+1)
--       ≡⟨ doublesSucSuc r (doubleℕ (N→ℕ (suc r) x)) ⟩
--         sucn (doublesℕ (suc r) 1) -- _ + 2^(r+1)
--          (doublesℕ (suc r) (N→ℕ (suc r) x)) --  2^(r+1)x + 2^(r+1)
--       ≡⟨ H r (doublesℕ (suc r) (N→ℕ (suc r) x)) ⟩
--         suc
--          (suc
--           (sucn (doubleℕ (predℕ (doublesℕ r 1))) -- _ + 2(2^r - 1) + 2
--            (doublesℕ (suc r) (N→ℕ (suc r) x))))
--       ≡⟨ refl ⟩
--         suc
--          (suc
--           (sucn (doubleℕ (predℕ (doublesℕ r 1)))
--            (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))
--       ≡⟨ cong (λ z → suc (suc (sucn (doubleℕ z) (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))) (sym (max→ℕ r))  ⟩
--          suc
--          (suc
--           (sucn (doubleℕ (DirNum→ℕ (max-n r)))
--            (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))
--       ≡⟨ cong (λ z → suc (suc (sucn (doubleℕ (DirNum→ℕ z)) (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))) (sym (d≡max)) ⟩
--          suc
--          (suc
--           (sucn (doubleℕ (DirNum→ℕ d))
--            (doublesℕ r (doubleℕ (N→ℕ (suc r) x))))) -- (2^r*2x + (2*(2^r - 1))) + 2 = 2^(r+1)x + 2^(r+1)
--       ∎
--       where
--         H : (n m : ℕ) → sucn (doublesℕ (suc n) 1) m ≡ suc (suc (sucn (doubleℕ (predℕ (doublesℕ n 1))) m))
--         H zero m = refl
--         H (suc n) m =
--             sucn (doublesℕ n 4) m
--           ≡⟨ cong (λ z → sucn z m) (doublesSucSuc n 2) ⟩
--             sucn (sucn (doublesℕ (suc n) 1) (doublesℕ n 2)) m
--           ≡⟨ refl ⟩
--             sucn (sucn (doublesℕ n 2) (doublesℕ  n 2)) m
--           ≡⟨ {!!} ⟩
--             sucn (doubleℕ (doublesℕ n 2)) m
--           ≡⟨ {!!} ⟩ {!!}

-- ℕ→Nsuc : (r : ℕ) (n : ℕ) → ℕ→N r (suc n) ≡ sucN (ℕ→N r n)
-- ℕ→Nsuc r n = {!!}

-- ℕ→Nsucn : (r : ℕ) (n m : ℕ) → ℕ→N r (sucn n m) ≡ sucnN n (ℕ→N r m)
-- ℕ→Nsucn r n m = {!!}

-- NℕNlemma : (r : ℕ) (d : DirNum r) → ℕ→N r (DirNum→ℕ d) ≡ bn d
-- NℕNlemma zero tt = refl
-- NℕNlemma (suc r) (↓ , ds) =
--     ℕ→N (suc r) (doubleℕ (DirNum→ℕ ds))
--   ≡⟨ {!!} ⟩ {!!}
-- NℕNlemma (suc r) (↑ , ds) = {!!}

-- N→ℕ→N : (r : ℕ) → (x : N r) → ℕ→N r (N→ℕ r x) ≡ x
-- N→ℕ→N zero (bn tt) = refl
-- N→ℕ→N zero (xr tt x) = cong (xr tt) (N→ℕ→N zero x)
-- N→ℕ→N (suc r) (bn (↓ , ds)) =
--     ℕ→N (suc r) (doubleℕ (DirNum→ℕ ds))
--   ≡⟨ cong (λ x → ℕ→N (suc r) x) (double-lemma ds) ⟩
--     ℕ→N (suc r) (DirNum→ℕ {suc r} (↓ , ds))
--   ≡⟨ NℕNlemma (suc r) (↓ , ds) ⟩
--     bn (↓ , ds)
--   ∎
-- N→ℕ→N (suc r) (bn (↑ , ds)) =
--     sucN (ℕ→N (suc r) (doubleℕ (DirNum→ℕ ds)))
--   ≡⟨ cong (λ x → sucN (ℕ→N (suc r) x)) (double-lemma ds) ⟩
--     sucN (ℕ→N (suc r) (DirNum→ℕ {suc r} (↓ , ds)))
--   ≡⟨ cong sucN (NℕNlemma (suc r) (↓ , ds)) ⟩
--     sucN (bn (↓ , ds))
--   ≡⟨ refl ⟩
--     bn (↑ , ds)
--   ∎
-- N→ℕ→N (suc r) (xr (↓ , ds) x) =
--      ℕ→N (suc r)
--       (sucn (doubleℕ (DirNum→ℕ ds))
--        (doublesℕ r (doubleℕ (N→ℕ (suc r) x))))
--    ≡⟨ cong (λ z → ℕ→N (suc r) (sucn z (doublesℕ r (doubleℕ (N→ℕ (suc r) x))))) (double-lemma ds)  ⟩
--       ℕ→N (suc r)
--       (sucn (DirNum→ℕ {suc r} (↓ , ds))
--        (doublesℕ r (doubleℕ (N→ℕ (suc r) x))))
--    ≡⟨ refl ⟩
--      ℕ→N (suc r)
--       (sucn (DirNum→ℕ {suc r} (↓ , ds))
--        (doublesℕ (suc r) (N→ℕ (suc r) x)))
--    ≡⟨ ℕ→Nsucn (suc r) (DirNum→ℕ {suc r} (↓ , ds)) (doublesℕ (suc r) (N→ℕ (suc r) x)) ⟩
--      sucnN (DirNum→ℕ {suc r} (↓ , ds))
--       (ℕ→N (suc r) (doublesℕ (suc r) (N→ℕ (suc r) x)))
--    ≡⟨ cong (λ z → sucnN (DirNum→ℕ {suc r} (↓ , ds)) z) (H (suc r) (suc r) (N→ℕ (suc r) x)) ⟩
--      sucnN (DirNum→ℕ {suc r} (↓ , ds))
--       (doublesN (suc r) (suc r) (ℕ→N (suc r) (N→ℕ (suc r) x)))
--    ≡⟨ cong (λ z → sucnN (DirNum→ℕ {suc r} (↓ , ds)) (doublesN (suc r) (suc r) z)) (N→ℕ→N (suc r) x) ⟩
--      sucnN (DirNum→ℕ {suc r} (↓ , ds))
--       (doublesN (suc r) (suc r) x)
--    ≡⟨ G (suc r) (↓ , ds) x snotz ⟩
--      xr (↓ , ds) x ∎
--    where
--      H : (r m n : ℕ) → ℕ→N r (doublesℕ m n) ≡ doublesN r m (ℕ→N r n)
--      H r m n = {!!}
--      G : (r : ℕ) (d : DirNum r) (x : N r) → ¬ (r ≡ 0) → sucnN (DirNum→ℕ {r} d) (doublesN r r x) ≡ xr d x
--      G zero d x 0≠0 = ⊥-elim (0≠0 refl)
--      G (suc r) d (bn x) r≠0 = {!!}
--      G (suc r) d (xr x x₁) r≠0 = {!!}
-- N→ℕ→N (suc r) (xr (↑ , ds) x) with max? ds
-- ... | no ds≠max =
--           sucN
--           (ℕ→N (suc r)
--            (sucn (doubleℕ (DirNum→ℕ ds))
--             (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))
--         ≡⟨ sym (ℕ→Nsuc (suc r)
--                 (sucn (doubleℕ (DirNum→ℕ ds)) (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))
--          ⟩
--            ℕ→N (suc r)
--            (suc (sucn (doubleℕ (DirNum→ℕ ds)) (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))
--         ≡⟨ refl ⟩
--            ℕ→N (suc r)
--            (suc (sucn (doubleℕ (DirNum→ℕ ds)) (doublesℕ (suc r) (N→ℕ (suc r) x))))
--         ≡⟨ cong (λ z → ℕ→N (suc r) z)
--                 (sym (sucnsuc (doubleℕ (DirNum→ℕ ds)) (doublesℕ (suc r) (N→ℕ (suc r) x))))
--          ⟩
--            ℕ→N (suc r)
--            (sucn (doubleℕ (DirNum→ℕ ds)) (suc (doublesℕ (suc r) (N→ℕ (suc r) x))))
--          ≡⟨ ℕ→Nsucn (suc r) (doubleℕ (DirNum→ℕ ds)) (suc (doublesℕ (suc r) (N→ℕ (suc r) x))) ⟩
--            sucnN (doubleℕ (DirNum→ℕ ds)) (ℕ→N (suc r) (suc (doublesℕ (suc r) (N→ℕ (suc r) x))))
--          ≡⟨ cong (λ z → sucnN (doubleℕ (DirNum→ℕ ds)) z)
--                   (ℕ→Nsuc (suc r) (doublesℕ (suc r) (N→ℕ (suc r) x)))
--           ⟩
--            --   (2^(r+1)*x + 1) + 2*ds
--            -- = 2*(2^r*x + ds) + 1
--            -- = 2*(
--            sucnN (doubleℕ (DirNum→ℕ ds)) (sucN (ℕ→N (suc r) (doublesℕ (suc r) (N→ℕ (suc r) x))))
--          ≡⟨ {!!} ⟩ {!!}
-- ... | yes ds≡max = {!!}

-- ℕ→N→ℕ : (r : ℕ) → (n : ℕ) → N→ℕ r (ℕ→N r n) ≡ n
-- ℕ→N→ℕ zero zero = refl
-- ℕ→N→ℕ (suc r) zero =
--     doubleℕ (DirNum→ℕ (zero-n r))
--   ≡⟨ cong doubleℕ (zero-n≡0 {r}) ⟩
--     doubleℕ zero
--   ≡⟨ refl ⟩
--     zero
--   ∎
-- ℕ→N→ℕ zero (suc n) = cong suc (ℕ→N→ℕ zero n)
-- ℕ→N→ℕ (suc r) (suc n) =
--     N→ℕ (suc r) (sucN (ℕ→N (suc r) n))
--   ≡⟨ N→ℕsucN (suc r) (ℕ→N (suc r) n) ⟩
--     suc (N→ℕ (suc r) (ℕ→N (suc r) n))
--   ≡⟨ cong suc (ℕ→N→ℕ (suc r) n) ⟩
--     suc n
--   ∎

-- N≃ℕ : (r : ℕ) → N r ≃ ℕ
-- N≃ℕ r = isoToEquiv (iso (N→ℕ r) (ℕ→N r) (ℕ→N→ℕ r) (N→ℕ→N r))

-- N≡ℕ : (r : ℕ) → N r ≡ ℕ
-- N≡ℕ r = ua (N≃ℕ r)

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional


text:
open import Data.Empty using (⊥-elim)
open import Data.Fin using (Fin; _≟_)
open import Data.Nat using (ℕ)
open import Data.Vec using (lookup; _[_]≔_)
open import Data.Vec.Properties using (lookup∘update; lookup∘update′; []≔-commutes; []≔-idempotent; []≔-lookup)
open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Binary.PropositionalEquality using (sym; trans; _≡_; refl; cong; _≢_; module ≡-Reasoning)
open import Data.Product using (∃-syntax; _,_; proj₁; proj₂; _×_)
open ≡-Reasoning

open import Common
open import Global
open import Local
open import Projection

soundness :
  ∀ { n : ℕ } { act : Action n } { c g g′ }
  -> g ↔ c
  -> g - act →g g′
  -> ∃[ c′ ] c - act →c c′ × g′ ↔ c′
soundness
  {n = n}
  {act = act@(action .p .q p≢q .l)}
  {c = c}
  {g = g@(msgSingle p q p≢q-gt l g′)}
  {g′ = .g′}
  assoc
  →g-prefix
  = c′ , (→c-comm c p≢q refl refl refl lpReduce lqReduce , g′↔c′)
  where
    config-without-prefix = config-gt-remove-prefix g c assoc refl
    c′ = proj₁ config-without-prefix
    g′↔c′ : g′ ↔ c′
    g′↔c′ = proj₂ (proj₂ config-without-prefix)
    lpReduce : (p , lookup c p) - act →l (p , project g′ p)
    lpReduce rewrite _↔_.isProj assoc p
      = →l-send p (proj-prefix-send p q g′ p≢q-gt) p≢q
    lqReduce : (q , lookup c q) - act →l (q , project g′ q)
    lqReduce rewrite _↔_.isProj assoc q
      = →l-recv q (proj-prefix-recv p q g′ p≢q-gt) p≢q
soundness
  {n = n}
  {act = act@(.action p q p≢q l)}
  {c = c}
  {g = g@(msgSingle r s r≢s l′ gSub)}
  {g′ = g′@(.msgSingle r s r≢s l′ gSub′)}
  assoc
  (→g-cont gReduce p≢r q≢r p≢s q≢s)
  = c′ , cReduce , assoc′
  where
    config-without-prefix = config-gt-remove-prefix g c assoc refl
    cSub = proj₁ config-without-prefix
    gSub↔cSub : gSub ↔ cSub
    gSub↔cSub = proj₂ (proj₂ config-without-prefix)
    soundness-gSub : ∃[ cSub′ ] cSub - act →c cSub′ × gSub′ ↔ cSub′
    soundness-gSub = soundness gSub↔cSub gReduce
    c′ : Configuration n
    c′ with soundness-gSub
    ... | cSub′ , _ , _ = (cSub′ [ r ]≔ lr′) [ s ]≔ ls′
      where
        lr′ : Local n
        lr′ with soundness-gSub
        ...   | cSub′ , _ , _ = sendSingle s l′ (lookup cSub′ r)
        ls′ : Local n
        ls′ with soundness-gSub
        ...   | cSub′ , _ , _ = recvSingle r l′ (lookup cSub′ s)
    isProj-g′ : ∀(t : Fin n) -> lookup c′ t ≡ project g′ t
    isProj-g′ t with soundness-gSub
    ...   | cSub′ , _ , gSub′↔cSub′
        with r ≟ t   | s ≟ t
    ...   | yes r≡t  | no _
        rewrite sym r≡t
        rewrite lookup∘update′ r≢s (cSub′ [ r ]≔ sendSingle s l′ (lookup cSub′ r)) (recvSingle r l′ (lookup cSub′ s))
        rewrite lookup∘update r cSub′ (sendSingle s l′ (lookup cSub′ r))
        rewrite _↔_.isProj gSub′↔cSub′ r = refl
    ...   | no _     | yes s≡t
        rewrite sym s≡t
        rewrite lookup∘update s (cSub′ [ r ]≔ sendSingle s l′ (lookup cSub′ r)) (recvSingle r l′ (lookup cSub′ s))
        rewrite _↔_.isProj gSub′↔cSub′ s = refl
    ...   | no r≢t   | no s≢t
        rewrite lookup∘update′ (¬≡-flip s≢t) (cSub′ [ r ]≔ sendSingle s l′ (lookup cSub′ r)) (recvSingle r l′ (lookup cSub′ s))
        rewrite lookup∘update′ (¬≡-flip r≢t) cSub′ (sendSingle s l′ (lookup cSub′ r))
        rewrite _↔_.isProj gSub′↔cSub′ t = refl
    ...   | yes refl | yes refl = ⊥-elim (r≢s refl)
    assoc′ : g′ ↔ c′
    assoc′ = record { isProj = isProj-g′ }
    cReduce : c - act →c c′
    cReduce with soundness-gSub
    ...   | cSub′ , →c-comm {lp = lp} {lp′ = lp′} {lq = lq} {lq′ = lq′} .cSub .p≢q refl refl refl lpReduce lqReduce , gSub′↔cSub′
            = →c-comm c p≢q lp≡c[p] lq≡c[q] c→c′ lpReduce lqReduce
      where
        lr′ = sendSingle s l′ (lookup cSub′ r)
        ls′ = recvSingle r l′ (lookup cSub′ s)
        lp≡c[p] : lp ≡ lookup c p
        lp≡c[p]
          rewrite lookup∘update′ p≢s (c [ r ]≔ project gSub r) (project gSub s)
          rewrite lookup∘update′ p≢r c (project gSub r) = refl
        lq≡c[q] : lq ≡ lookup c q
        lq≡c[q]
          rewrite lookup∘update′ q≢s (c [ r ]≔ project gSub r) (project gSub s)
          rewrite lookup∘update′ q≢r c (project gSub r) = refl
        lr′≡c[r] : lr′ ≡ lookup c r
        lr′≡c[r]
          rewrite lookup∘update′ (¬≡-flip q≢r) (cSub [ p ]≔ lp′) lq′
          rewrite lookup∘update′ (¬≡-flip p≢r) cSub lp′
          rewrite _↔_.isProj assoc r
          rewrite proj-prefix-send {l = l′} r s gSub r≢s
          rewrite lookup∘update′ r≢s (c [ r ]≔ project gSub r) (project gSub s)
          rewrite lookup∘update r c (project gSub r)
          = refl
        ls′≡c[s] : ls′ ≡ lookup c s
        ls′≡c[s]
          rewrite lookup∘update′ (¬≡-flip q≢s) (cSub [ p ]≔ lp′) lq′
          rewrite lookup∘update′ (¬≡-flip p≢s) cSub lp′
          rewrite _↔_.isProj assoc s
          rewrite proj-prefix-recv {l = l′} r s gSub r≢s
          rewrite lookup∘update s (c [ r ]≔ project gSub r) (project gSub s)
          = refl
        c→c′ : (cSub′ [ r ]≔ lr′) [ s ]≔ ls′ ≡ (c [ p ]≔ lp′) [ q ]≔ lq′
        c→c′
          rewrite []≔-commutes ((((c [ r ]≔ project gSub r) [ s ]≔ project gSub s) [ p ]≔ lp′) [ q ]≔ lq′) r s {lr′} {ls′} r≢s
          rewrite []≔-commutes (((c [ r ]≔ project gSub r) [ s ]≔ project gSub s) [ p ]≔ lp′) q s {lq′} {ls′} q≢s
          rewrite []≔-commutes ((c [ r ]≔ project gSub r) [ s ]≔ project gSub s) p s {lp′} {ls′} p≢s
          rewrite []≔-idempotent (c [ r ]≔ project gSub r) s {project gSub s} {ls′}
          rewrite []≔-commutes (((c [ r ]≔ project gSub r) [ s ]≔ ls′) [ p ]≔ lp′) q r {lq′} {lr′} q≢r
          rewrite []≔-commutes ((c [ r ]≔ project gSub r) [ s ]≔ ls′) p r {lp′} {lr′} p≢r
          rewrite []≔-commutes (c [ r ]≔ project gSub r) s r {ls′} {lr′} (¬≡-flip r≢s)
          rewrite []≔-idempotent c r {project gSub r} {lr′}
          rewrite lr′≡c[r]
          rewrite ls′≡c[s]
          rewrite []≔-lookup c r
          rewrite []≔-lookup c s
          = refl

max_stars_repo_name: fangyi-zhou/mpst-in-agda

max_issues_repo_name: fangyi-zhou/mpst-in-agda

max_forks_repo_name: fangyi-zhou/mpst-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed AVL trees
------------------------------------------------------------------------

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

open import Relation.Binary using (StrictTotalOrder)

module Data.AVL.Indexed
  {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where

open import Level using (_⊔_)
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Product hiding (map)
open import Data.Maybe hiding (map)
open import Data.DifferenceList using (DiffList; []; _∷_; _++_)
open import Function as F hiding (const)
open import Relation.Unary
open import Relation.Binary using (_Respects_; Tri; tri<; tri≈; tri>)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)

------------------------------------------------------------------------
-- Re-export core definitions publicly

open import Data.AVL.Key strictTotalOrder public
open import Data.AVL.Value Eq.setoid public
open import Data.AVL.Height public

------------------------------------------------------------------------
-- Definitions of the tree

K&_ : ∀ {v} (V : Value v) → Set (a ⊔ v)
K& V = Σ Key (Value.family V)

-- The trees have three parameters/indices: a lower bound on the
-- keys, an upper bound, and a height.
--
-- (The bal argument is the balance factor.)

data Tree {v} (V : Value v) (l u : Key⁺) : ℕ → Set (a ⊔ v ⊔ ℓ₂) where
  leaf : (l<u : l <⁺ u) → Tree V l u 0
  node : ∀ {hˡ hʳ h}
         (k : K& V)
         (lk : Tree V l [ proj₁ k ] hˡ)
         (ku : Tree V [ proj₁ k ] u hʳ)
         (bal : hˡ ∼ hʳ ⊔ h) →
         Tree V l u (suc h)

module _ {v} {V : Value v} where

  private
    Val = Value.family V
    V≈  = Value.respects V

  leaf-injective : ∀ {l u} {p q : l <⁺ u} → (Tree V l u 0 ∋ leaf p) ≡ leaf q → p ≡ q
  leaf-injective refl = refl

  node-injective-key :
    ∀ {hˡ₁ hˡ₂ hʳ₁ hʳ₂ h l u k₁ k₂}
      {lk₁ : Tree V l [ proj₁ k₁ ] hˡ₁} {lk₂ : Tree V l [ proj₁ k₂ ] hˡ₂}
      {ku₁ : Tree V [ proj₁ k₁ ] u hʳ₁} {ku₂ : Tree V [ proj₁ k₂ ] u hʳ₂}
      {bal₁ : hˡ₁ ∼ hʳ₁ ⊔ h} {bal₂ : hˡ₂ ∼ hʳ₂ ⊔ h} →
    node k₁ lk₁ ku₁ bal₁ ≡ node k₂ lk₂ ku₂ bal₂ → k₁ ≡ k₂
  node-injective-key refl = refl

  -- See also node-injectiveˡ, node-injectiveʳ, and node-injective-bal
  -- in Data.AVL.Indexed.WithK.

  -- Cast operations. Logarithmic in the size of the tree, if we don't
  -- count the time needed to construct the new proofs in the leaf
  -- cases. (The same kind of caveat applies to other operations
  -- below.)
  --
  -- Perhaps it would be worthwhile changing the data structure so
  -- that the casts could be implemented in constant time (excluding
  -- proof manipulation). However, note that this would not change the
  -- worst-case time complexity of the operations below (up to Θ).

  castˡ : ∀ {l m u h} → l <⁺ m → Tree V m u h → Tree V l u h
  castˡ {l} l<m (leaf m<u)         = leaf (trans⁺ l l<m m<u)
  castˡ     l<m (node k mk ku bal) = node k (castˡ l<m mk) ku bal

  castʳ : ∀ {l m u h} → Tree V l m h → m <⁺ u → Tree V l u h
  castʳ {l} (leaf l<m)         m<u = leaf (trans⁺ l l<m m<u)
  castʳ     (node k lk km bal) m<u = node k lk (castʳ km m<u) bal

  -- Various constant-time functions which construct trees out of
  -- smaller pieces, sometimes using rotation.

  joinˡ⁺ : ∀ {l u hˡ hʳ h} →
           (k : K& V) →
           (∃ λ i → Tree V l [ proj₁ k ] (i ⊕ hˡ)) →
           Tree V [ proj₁ k ] u hʳ →
           (bal : hˡ ∼ hʳ ⊔ h) →
           ∃ λ i → Tree V l u (i ⊕ (1 + h))
  joinˡ⁺ k₆ (1# , node k₂ t₁
                    (node k₄ t₃ t₅ bal)
                                ∼+) t₇ ∼-  = (0# , node k₄
                                                        (node k₂ t₁ t₃ (max∼ bal))
                                                        (node k₆ t₅ t₇ (∼max bal))
                                                        ∼0)
  joinˡ⁺ k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼-  = (0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)
  joinˡ⁺ k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼-  = (1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)
  joinˡ⁺ k₂ (1# , t₁)               t₃ ∼0  = (1# , node k₂ t₁ t₃ ∼-)
  joinˡ⁺ k₂ (1# , t₁)               t₃ ∼+  = (0# , node k₂ t₁ t₃ ∼0)
  joinˡ⁺ k₂ (0# , t₁)               t₃ bal = (0# , node k₂ t₁ t₃ bal)
  joinˡ⁺ k₂ (## , t₁)               t₃ bal

  joinʳ⁺ : ∀ {l u hˡ hʳ h} →
           (k : K& V) →
           Tree V l [ proj₁ k ] hˡ →
           (∃ λ i → Tree V [ proj₁ k ] u (i ⊕ hʳ)) →
           (bal : hˡ ∼ hʳ ⊔ h) →
           ∃ λ i → Tree V l u (i ⊕ (1 + h))
  joinʳ⁺ k₂ t₁ (1# , node k₆
                       (node k₄ t₃ t₅ bal)
                                t₇ ∼-) ∼+  = (0# , node k₄
                                                        (node k₂ t₁ t₃ (max∼ bal))
                                                        (node k₆ t₅ t₇ (∼max bal))
                                                        ∼0)
  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+  = (0# , node k₄ (node k₂ t₁ t₃ ∼0) t₅ ∼0)
  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+  = (1# , node k₄ (node k₂ t₁ t₃ ∼+) t₅ ∼-)
  joinʳ⁺ k₂ t₁ (1# , t₃)               ∼0  = (1# , node k₂ t₁ t₃ ∼+)
  joinʳ⁺ k₂ t₁ (1# , t₃)               ∼-  = (0# , node k₂ t₁ t₃ ∼0)
  joinʳ⁺ k₂ t₁ (0# , t₃)               bal = (0# , node k₂ t₁ t₃ bal)
  joinʳ⁺ k₂ t₁ (## , t₃)               bal

  joinˡ⁻ : ∀ {l u} hˡ {hʳ h} →
           (k : K& V) →
           (∃ λ i → Tree V l [ proj₁ k ] pred[ i ⊕ hˡ ]) →
           Tree V [ proj₁ k ] u hʳ →
           (bal : hˡ ∼ hʳ ⊔ h) →
           ∃ λ i → Tree V l u (i ⊕ h)
  joinˡ⁻ zero    k₂ (0# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)
  joinˡ⁻ zero    k₂ (1# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)
  joinˡ⁻ (suc _) k₂ (0# , t₁) t₃ ∼+  = joinʳ⁺ k₂ t₁ (1# , t₃) ∼+
  joinˡ⁻ (suc _) k₂ (0# , t₁) t₃ ∼0  = (1# , node k₂ t₁ t₃ ∼+)
  joinˡ⁻ (suc _) k₂ (0# , t₁) t₃ ∼-  = (0# , node k₂ t₁ t₃ ∼0)
  joinˡ⁻ (suc _) k₂ (1# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)
  joinˡ⁻ n       k₂ (## , t₁) t₃ bal

  joinʳ⁻ : ∀ {l u hˡ} hʳ {h} →
           (k : K& V) →
           Tree V l [ proj₁ k ] hˡ →
           (∃ λ i → Tree V [ proj₁ k ] u pred[ i ⊕ hʳ ]) →
           (bal : hˡ ∼ hʳ ⊔ h) →
           ∃ λ i → Tree V l u (i ⊕ h)
  joinʳ⁻ zero    k₂ t₁ (0# , t₃) bal = (1# , node k₂ t₁ t₃ bal)
  joinʳ⁻ zero    k₂ t₁ (1# , t₃) bal = (1# , node k₂ t₁ t₃ bal)
  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃) ∼-  = joinˡ⁺ k₂ (1# , t₁) t₃ ∼-
  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃) ∼0  = (1# , node k₂ t₁ t₃ ∼-)
  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃) ∼+  = (0# , node k₂ t₁ t₃ ∼0)
  joinʳ⁻ (suc _) k₂ t₁ (1# , t₃) bal = (1# , node k₂ t₁ t₃ bal)
  joinʳ⁻ n       k₂ t₁ (## , t₃) bal

  -- Extracts the smallest element from the tree, plus the rest.
  -- Logarithmic in the size of the tree.

  headTail : ∀ {l u h} → Tree V l u (1 + h) →
             ∃ λ (k : K& V) → l <⁺ [ proj₁ k ] ×
                            ∃ λ i → Tree V [ proj₁ k ] u (i ⊕ h)
  headTail (node k₁ (leaf l<k₁) t₂ ∼+) = (k₁ , l<k₁ , 0# , t₂)
  headTail (node k₁ (leaf l<k₁) t₂ ∼0) = (k₁ , l<k₁ , 0# , t₂)
  headTail (node {hˡ = suc _} k₃ t₁₂ t₄ bal) with headTail t₁₂
  ... | (k₁ , l<k₁ , t₂) = (k₁ , l<k₁ , joinˡ⁻ _ k₃ t₂ t₄ bal)

  -- Extracts the largest element from the tree, plus the rest.
  -- Logarithmic in the size of the tree.

  initLast : ∀ {l u h} → Tree V l u (1 + h) →
             ∃ λ (k : K& V) → [ proj₁ k ] <⁺ u ×
                            ∃ λ i → Tree V l [ proj₁ k ] (i ⊕ h)
  initLast (node k₂ t₁ (leaf k₂<u) ∼-) = (k₂ , k₂<u , (0# , t₁))
  initLast (node k₂ t₁ (leaf k₂<u) ∼0) = (k₂ , k₂<u , (0# , t₁))
  initLast (node {hʳ = suc _} k₂ t₁ t₃₄ bal) with initLast t₃₄
  ... | (k₄ , k₄<u , t₃) = (k₄ , k₄<u , joinʳ⁻ _ k₂ t₁ t₃ bal)

  -- Another joining function. Logarithmic in the size of either of
  -- the input trees (which need to have almost equal heights).

  join : ∀ {l m u hˡ hʳ h} →
         Tree V l m hˡ → Tree V m u hʳ → (bal : hˡ ∼ hʳ ⊔ h) →
         ∃ λ i → Tree V l u (i ⊕ h)
  join t₁ (leaf m<u) ∼0 = (0# , castʳ t₁ m<u)
  join t₁ (leaf m<u) ∼- = (0# , castʳ t₁ m<u)
  join {hʳ = suc _} t₁ t₂₃ bal with headTail t₂₃
  ... | (k₂ , m<k₂ , t₃) = joinʳ⁻ _ k₂ (castʳ t₁ m<k₂) t₃ bal

  -- An empty tree.

  empty : ∀ {l u} → l <⁺ u → Tree V l u 0
  empty = leaf

  -- A singleton tree.

  singleton : ∀ {l u} (k : Key) → Val k → l < k < u → Tree V l u 1
  singleton k v (l<k , k<u) = node (k , v) (leaf l<k) (leaf k<u) ∼0

  -- Inserts a key into the tree, using a function to combine any
  -- existing value with the new value. Logarithmic in the size of the
  -- tree (assuming constant-time comparisons and a constant-time
  -- combining function).

  insertWith : ∀ {l u h} (k : Key) → (Maybe (Val k) → Val k) →  -- Maybe old → result.
               Tree V l u h → l < k < u →
               ∃ λ i → Tree V l u (i ⊕ h)
  insertWith k f (leaf l<u) l<k<u = (1# , singleton k (f nothing) l<k<u)
  insertWith k f (node (k′ , v′) lp pu bal) (l<k , k<u) with compare k k′
  ... | tri< k<k′ _ _ = joinˡ⁺ (k′ , v′) (insertWith k f lp (l<k , [ k<k′ ]ᴿ)) pu bal
  ... | tri> _ _ k′<k = joinʳ⁺ (k′ , v′) lp (insertWith k f pu ([ k′<k ]ᴿ , k<u)) bal
  ... | tri≈ _ k≈k′ _ = (0# , node (k′ , V≈ k≈k′ (f (just (V≈ (Eq.sym k≈k′) v′)))) lp pu bal)

  -- Inserts a key into the tree. If the key already exists, then it
  -- is replaced. Logarithmic in the size of the tree (assuming
  -- constant-time comparisons).

  insert : ∀ {l u h} → (k : Key) → Val k → Tree V l u h → l < k < u →
           ∃ λ i → Tree V l u (i ⊕ h)
  insert k v = insertWith k (F.const v)

  -- Deletes the key/value pair containing the given key, if any.
  -- Logarithmic in the size of the tree (assuming constant-time
  -- comparisons).

  delete : ∀ {l u h} (k : Key) → Tree V l u h → l < k < u →
           ∃ λ i → Tree V l u pred[ i ⊕ h ]
  delete k (leaf l<u) l<k<u = (0# , leaf l<u)
  delete k (node p@(k′ , v) lp pu bal) (l<k , k<u) with compare k′ k
  ... | tri< k′<k _ _ = joinʳ⁻ _ p lp (delete k pu ([ k′<k ]ᴿ , k<u)) bal
  ... | tri> _ _ k′>k = joinˡ⁻ _ p (delete k lp (l<k , [ k′>k ]ᴿ)) pu bal
  ... | tri≈ _ k′≡k _ = join lp pu bal

  -- Looks up a key. Logarithmic in the size of the tree (assuming
  -- constant-time comparisons).

  lookup : ∀ {l u h} (k : Key) → Tree V l u h → l < k < u → Maybe (Val k)
  lookup k (leaf _) l<k<u = nothing
  lookup k (node (k′ , v) lk′ k′u _) (l<k , k<u) with compare k′ k
  ... | tri< k′<k _ _ = lookup k k′u ([ k′<k ]ᴿ , k<u)
  ... | tri> _ _ k′>k = lookup k lk′ (l<k , [ k′>k ]ᴿ)
  ... | tri≈ _ k′≡k _ = just (V≈ k′≡k v)

  -- Converts the tree to an ordered list. Linear in the size of the
  -- tree.

  toDiffList : ∀ {l u h} → Tree V l u h → DiffList (K& V)
  toDiffList (leaf _)       = []
  toDiffList (node k l r _) = toDiffList l ++ k ∷ toDiffList r

module _ {v w} {V : Value v} {W : Value w} where

  private
    Val = Value.family V
    Wal = Value.family W

  -- Maps a function over all values in the tree.

  map : ∀[ Val ⇒ Wal ] → ∀ {l u h} → Tree V l u h → Tree W l u h
  map f (leaf l<u)             = leaf l<u
  map f (node (k , v) l r bal) = node (k , f v) (map f l) (map f r) bal


text:
module Function.Domains where

import      Lvl
open import Structure.Setoid
open import Type

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

module _ {X : Type{ℓₒ₁}} {Y : Type{ℓₒ₂}} where
  -- The partial domain of a function
  -- Note: This is the same as the domain because all functions are total (or at least supposed to be)
  ⊷ : (X → Y) → Type{ℓₒ₁}
  ⊷ _ = X

module _ {X : Type{ℓₒ₁}} {Y : Type{ℓₒ₂}} where
  -- ∃(Unapply f(y)) is also called "the fiber of the element y under the map f".
  -- Unapply(f) is similar to the inverse image or the preimage of f when their argument is a singleton set.
  Fiber : ⦃ equiv-Y : Equiv{ℓₑ₂}(Y) ⦄ → (X → Y) → Y → X → Type
  Fiber f(y) x = (f(x) ≡ y)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by preorders
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.Properties.Preorder
         {p₁ p₂ p₃} (P : Preorder p₁ p₂ p₃) where

open import Function
open import Data.Product as Prod

open Relation.Binary.Preorder P

------------------------------------------------------------------------
-- For every preorder there is an induced equivalence

InducedEquivalence : Setoid _ _
InducedEquivalence = record
  { _≈_           = λ x y → x ∼ y × y ∼ x
  ; isEquivalence = record
    { refl  = (refl , refl)
    ; sym   = swap
    ; trans = Prod.zip trans (flip trans)
    }
  }


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

open import algebra.semigroup.core public
open import algebra.semigroup.morphism public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

module Data.Binary.Proofs.Unary where

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

inc⁺⁺-homo : ∀ xs → ⟦ inc⁺⁺ xs ⇓⟧⁺ ≡ suc ⟦ xs ⇓⟧⁺
inc⁺⁺-homo 1ᵇ = refl
inc⁺⁺-homo (O ∷ xs) = refl
inc⁺⁺-homo (I ∷ xs) =
  begin
    2* ⟦ inc⁺⁺ xs ⇓⟧⁺
  ≡⟨ cong 2* (inc⁺⁺-homo xs) ⟩
    2* (suc ⟦ xs ⇓⟧⁺)
  ≡⟨⟩
    (suc ⟦ xs ⇓⟧⁺) ℕ.+ suc ⟦ xs ⇓⟧⁺
  ≡⟨ ℕ.+-suc (suc ⟦ xs ⇓⟧⁺) ⟦ xs ⇓⟧⁺ ⟩
    suc (suc (2* ⟦ xs ⇓⟧⁺))
  ∎

inc-homo : ∀ x → ⟦ inc x ⇓⟧ ≡ suc ⟦ x ⇓⟧
inc-homo 0ᵇ = refl
inc-homo (0< xs) = inc⁺⁺-homo xs

open import Data.Product

⟦x⇓⟧⁺≡suc : ∀ x → ∃[ n ] (⟦ x ⇓⟧⁺ ≡ suc n)
⟦x⇓⟧⁺≡suc 1ᵇ = 0 , refl
⟦x⇓⟧⁺≡suc (I ∷ x) = 2* ⟦ x ⇓⟧⁺ , refl
⟦x⇓⟧⁺≡suc (O ∷ x) with ⟦x⇓⟧⁺≡suc x
⟦x⇓⟧⁺≡suc (O ∷ x) | fst , snd = suc (2* fst) , (cong 2* snd ⟨ trans ⟩ (ℕ.+-suc (suc fst) _))

⟦x⇓⟧⁺≢0 : ∀ x → ⟦ x ⇓⟧⁺ ≢ 0
⟦x⇓⟧⁺≢0 x x≡0 with ⟦x⇓⟧⁺≡suc x
⟦x⇓⟧⁺≢0 x x≡0 | _ , prf with sym x≡0 ⟨ trans ⟩ prf
⟦x⇓⟧⁺≢0 x x≡0 | _ , prf | ()

open import Data.Empty

inc-dec⁺⁺ : ∀ x xs → inc⁺⁺ (dec⁺⁺ x xs) ≡ x ∷ xs
inc-dec⁺⁺ I xs = refl
inc-dec⁺⁺ O 1ᵇ = refl
inc-dec⁺⁺ O (x ∷ xs) = cong (O ∷_) (inc-dec⁺⁺ x xs)

inc-dec : ∀ xs → inc⁺ (dec⁺ xs) ≡ xs
inc-dec 1ᵇ = refl
inc-dec (x ∷ xs) = inc-dec⁺⁺ x xs

data IncView : 𝔹 → ℕ → Set where
  Izero : IncView 0ᵇ 0
  Isuc : ∀ {n xs ys} → inc xs ≡ ys → IncView xs n → IncView ys (suc n)

inc-view : ∀ xs → IncView xs ⟦ xs ⇓⟧
inc-view xs = go _ xs refl
  where
  go : ∀ n xs → ⟦ xs ⇓⟧ ≡ n → IncView xs n
  go .0 0ᵇ refl = Izero
  go zero (0< xs) eq = ⊥-elim (⟦x⇓⟧⁺≢0 xs eq)
  go (suc n) (0< xs) eq =
    Isuc
      (cong 0<_ (inc-dec xs))
      (go n (dec⁺ xs)
            (ℕ.suc-injective (sym (inc-homo (dec⁺ xs)) ⟨ trans ⟩ cong ⟦_⇓⟧⁺ (inc-dec xs) ⟨ trans ⟩ eq)))

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


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

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

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.BlockStorage.BlockTree       as BlockTree
import      LibraBFT.Impl.Consensus.ConsensusTypes.ExecutedBlock as ExecutedBlock
import      LibraBFT.Impl.Consensus.ConsensusTypes.Vote          as Vote
import      LibraBFT.Impl.Consensus.PersistentLivenessStorage    as PersistentLivenessStorage
import      LibraBFT.Impl.Consensus.StateComputerByteString      as SCBS
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.ByteString
open import Util.Hash
open import Util.KVMap                                           as Map
open import Util.PKCS
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                          as String using (String)

module LibraBFT.Impl.Consensus.BlockStorage.BlockStore where

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

build
  : RootInfo      → RootMetadata
  → List Block    → List QuorumCert           → Maybe TimeoutCertificate
  → StateComputer → PersistentLivenessStorage → Usize
  → Either ErrLog BlockStore

executeAndInsertBlockE  : BlockStore → Block → Either  ErrLog (BlockStore × ExecutedBlock)

executeBlockE
  : BlockStore → Block
  → Either ErrLog ExecutedBlock

executeBlockE₀
  : BlockStore → Block
  → EitherD ErrLog ExecutedBlock

getBlock : HashValue → BlockStore → Maybe ExecutedBlock

insertSingleQuorumCertE
  : BlockStore → QuorumCert
  → Either ErrLog (BlockStore × List InfoLog)

pathFromRoot
  : HashValue → BlockStore
  → Either ErrLog (List ExecutedBlock)

pathFromRootM
  : HashValue
  → LBFT (Either ErrLog (List ExecutedBlock))

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

new
  : PersistentLivenessStorage → RecoveryData → StateComputer → Usize
  → Either ErrLog BlockStore
new storage initialData stateComputer maxPrunedBlocksInMem =
  build (initialData ^∙ rdRoot)
        (initialData ^∙ rdRootMetadata)
        (initialData ^∙ rdBlocks)
        (initialData ^∙ rdQuorumCerts)
        (initialData ^∙ rdHighestTimeoutCertificate)
        stateComputer
        storage
        maxPrunedBlocksInMem

abstract
  -- TODO: convert new to EitherD
  new-ed-abs : PersistentLivenessStorage → RecoveryData → StateComputer → Usize
             → EitherD ErrLog BlockStore
  new-ed-abs storage initialData stateComputer maxPrunedBlocksInMem = fromEither $
         new storage initialData stateComputer maxPrunedBlocksInMem

  new-e-abs : PersistentLivenessStorage → RecoveryData → StateComputer → Usize
            → Either ErrLog BlockStore
  new-e-abs = new
  new-e-abs-≡ : new-e-abs ≡ new
  new-e-abs-≡ = refl

build root _rootRootMetadata blocks quorumCerts highestTimeoutCert
           stateComputer storage maxPrunedBlocksInMem = do
  let (RootInfo∙new rootBlock rootQc rootLi) = root
      {- LBFT-OBM-DIFF : OBM does not implement RootMetadata
        assert_eq!(
            root_qc.certified_block().version(),
            root_metadata.version())
        assert_eq!(
            root_qc.certified_block().executed_state_id(),
            root_metadata.accu_hash)
      -}
      executedRootBlock = ExecutedBlock∙new
                            rootBlock
                            (StateComputeResult∙new (stateComputer ^∙ scObmVersion) nothing)
  tree ← BlockTree.new executedRootBlock rootQc rootLi maxPrunedBlocksInMem highestTimeoutCert
  bs1  ← (foldM) (λ bs b → fst <$> executeAndInsertBlockE bs b)
                 (BlockStore∙new tree stateComputer storage)
                 blocks
  (foldM) go bs1 quorumCerts
 where
  go : BlockStore → QuorumCert
     → Either ErrLog BlockStore
  go bs qc = case insertSingleQuorumCertE bs qc of λ where
    (Left e)              → Left e
    (Right (bs' , _info)) → Right bs'

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

commitM
  : LedgerInfoWithSignatures
  → LBFT (Either ErrLog Unit)
commitM finalityProof = do
  bs ← use lBlockStore
  maybeSD (bs ^∙ bsRoot) (bail fakeErr) $ λ bsr → do
    let blockIdToCommit = finalityProof ^∙ liwsLedgerInfo ∙ liConsensusBlockId
    case getBlock blockIdToCommit bs of λ where
      nothing →
        bail (ErrCBlockNotFound blockIdToCommit)
      (just blockToCommit) →
        ifD‖ blockToCommit ^∙ ebRound ≤?ℕ bsr ^∙ ebRound ≔
             bail fakeErr -- "commit block round lower than root"
           ‖ otherwise≔ (pathFromRootM blockIdToCommit >>= λ where
                           (Left  e) → bail e
                           (Right r) → continue blockToCommit r)
 where
  continue : ExecutedBlock → List ExecutedBlock → LBFT (Either ErrLog Unit)
  continue blockToCommit blocksToCommit = do
    -- NOTE: Haskell tells the "StateComputer" to commit 'blocksToCommit'.
    -- TODO-1: The StateComputer might indicate an epoch change.
    -- NO NEED FOR PRUNING: pruneTreeM blockToCommit
    --
    -- THIS IS WHERE COMMIT IS COMPLETED.
    -- To connect to the proof's correctness condition, it will be necessary to
    -- send a CommitMsg, which will carry evidence of the CommitRule
    -- needed to invoke correctness conditions like ConcCommitsDoNotConflict*.
    -- The details of this connection yet have not been settled yet.
    -- TODO-1: Once the details are determined, then make the connection.
    ok unit

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

rebuildM : RootInfo → RootMetadata → List Block → List QuorumCert → LBFT (Either ErrLog Unit)
rebuildM root rootMetadata blocks quorumCerts = do
  -- logEE lEC (here []) $ do
  self0 ← use lBlockStore
  case build
         root rootMetadata blocks quorumCerts
         (self0 ^∙ bsHighestTimeoutCert)
         (self0 ^∙ bsStateComputer)
         (self0 ^∙ bsStorage)
         (self0 ^∙ bsInner ∙ btMaxPrunedBlocksInMem) of λ where
    (Left  e)    → bail e
    (Right (BlockStore∙new inner _ _)) → do
      toRemove ← BlockTree.getAllBlockIdM
      PersistentLivenessStorage.pruneTreeM toRemove ∙?∙  λ _ → do
       lRoundManager ∙ rmBlockStore ∙ bsInner ∙= inner
       self1 ← use lBlockStore
       maybeS (self1 ^∙ bsRoot) (bail fakeErr {-bsRootErrL here-}) $ λ bsr → do
        ifD self1 ^∙ bsHighestCommitCert ∙ qcCommitInfo ∙ biRound >? bsr ^∙ ebRound
          then
            (commitM (self1 ^∙ bsHighestCommitCert ∙ qcLedgerInfo) ∙^∙
              withErrCtx (here' ("commitM failed" ∷ [])) ∙?∙  λ _ →
              ok unit)
          else ok unit
 where
  here' : List String.String → List String.String
  here' t =
    "BlockStore" ∷ "rebuildM" ∷ t
    -- lsRI root : lsRMD rootMetadata : lsBs blocks : lsQCs quorumCerts : t

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

executeAndInsertBlockM : Block → LBFT (Either ErrLog ExecutedBlock)
executeAndInsertBlockM b = do
  bs ← use lBlockStore
  case⊎D executeAndInsertBlockE bs b of λ where
    (Left e) → bail e
    (Right (bs' , eb)) → do
      lBlockStore ∙= bs'
      ok eb

module executeAndInsertBlockE (bs0 : BlockStore) (block : Block) where
  VariantFor : ∀ {ℓ} EL → EL-func {ℓ} EL
  VariantFor EL = EL ErrLog (BlockStore × ExecutedBlock)

  continue step₁ : VariantFor EitherD
  continue = step₁
  step₂ : ExecutedBlock → VariantFor EitherD
  step₃ : ExecutedBlock → VariantFor EitherD
  step₄ : ExecutedBlock → VariantFor EitherD

  step₀ =
    -- NOTE: if the hash is already in our blockstore, then HASH-COLLISION
    -- because we have already confirmed the new block is for the expected round
    -- and if there is already a block for that round then our expected round
    -- should be higher.
    maybeSD (getBlock (block ^∙ bId) bs0) continue (pure ∘ (bs0 ,_))

  here' : List String.String → List String.String
  here' t = "BlockStore" ∷ "executeAndInsertBlockE" {-∷ lsB block-} ∷ t

  step₁ =
      maybeSD (bs0 ^∙ bsRoot) (LeftD fakeErr) λ bsr →
      let btRound = bsr ^∙ ebRound in
      ifD btRound ≥?ℕ block ^∙ bRound
      then LeftD fakeErr -- block with old round
      else step₂ bsr

  step₂ _ = do
        eb ← case⊎D executeBlockE bs0 block of λ where
          (Right res) → RightD res
          -- OBM-LBFT-DIFF : This is never thrown in OBM.
          -- It is thrown by StateComputer in Rust (but not in OBM).
          (Left (ErrECCBlockNotFound parentBlockId)) → do
            eitherSD (pathFromRoot parentBlockId bs0) LeftD λ blocksToReexecute →
              -- OBM-LBFT-DIFF : OBM StateComputer does NOT have state.
              -- If it ever does have state then the following 'forM' will
              -- need to change to some sort of 'fold' because 'executeBlockE'
              -- would change the state, so the state passed to 'executeBlockE'
              -- would no longer be 'bs0'.
              case⊎D (forM) blocksToReexecute (executeBlockE bs0 ∘ (_^∙ ebBlock)) of λ where
                (Left  e) → LeftD e
                (Right _) → executeBlockE₀ bs0 block
          (Left err) → LeftD err
        step₃ eb

  step₃ eb = do
        bs1 ← withErrCtxD'
                (here' [])
                -- TODO-1 : use inspect qualified so Agda List singleton can be in scope.
                (PersistentLivenessStorage.saveTreeE bs0 (eb ^∙ ebBlock ∷ []) [])
        step₄ eb

  step₄ eb = do
        (bt' , eb') ← BlockTree.insertBlockE eb (bs0 ^∙ bsInner)
        pure ((bs0 & bsInner ∙~ bt') , eb')

  E : VariantFor Either
  E = toEither step₀

  D : VariantFor EitherD
  D = fromEither E

executeAndInsertBlockE = executeAndInsertBlockE.E

module executeBlockE (bs : BlockStore) (block : Block) where

  step₀ = do
    case SCBS.compute (bs ^∙ bsStateComputer) block (block ^∙ bParentId) of λ where
      (Left e)                   → Left fakeErr -- (here' e)
      (Right stateComputeResult) →
        pure (ExecutedBlock∙new block stateComputeResult)
   where
    here' : List String → List String
    here' t = "BlockStore" ∷ "executeBlockE" {-∷ lsB block-} ∷ t

abstract
  executeBlockE = executeBlockE.step₀
  executeBlockE₀ bs block = fromEither $ executeBlockE bs block
  executeBlockE≡ : ∀ {bs block r} → executeBlockE bs block ≡ r → executeBlockE₀ bs block ≡ fromEither r
  executeBlockE≡ refl = refl
------------------------------------------------------------------------------

insertSingleQuorumCertM
  : QuorumCert
  → LBFT (Either ErrLog Unit)
insertSingleQuorumCertM qc = do
  bs ← use lBlockStore
  case insertSingleQuorumCertE bs qc of λ where
    (Left  e)   → bail e
    (Right (bs' , info)) → do
      forM_ info logInfo
      lBlockStore ∙= bs'
      ok unit

insertSingleQuorumCertE bs qc =
  maybeS (getBlock (qc ^∙ qcCertifiedBlock ∙ biId) bs)
         (Left (ErrCBlockNotFound
                  -- (here ["insert QC without having the block in store first"])
                  (qc ^∙ qcCertifiedBlock ∙ biId)))
         (λ executedBlock →
             if ExecutedBlock.blockInfo executedBlock /= qc ^∙ qcCertifiedBlock
             then Left fakeErr
 --                      (ErrL (here [ "QC for block has different BlockInfo than EB"
 --                                  , "QC certified BI", show (qc ^∙ qcCertifiedBlock)
 --                                  , "EB BI", show (ExecutedBlock.blockInfo executedBlock)
 --                                  , "EB", show executedBlock ]))

             else (do
                    bs'           ← withErrCtx' (here' [])
                                      (PersistentLivenessStorage.saveTreeE bs [] (qc ∷ []))
                    (bt , output) ← BlockTree.insertQuorumCertE qc (bs' ^∙ bsInner)
                    pure ((bs' & bsInner ∙~ bt) , output)))
 where
  here' : List String.String → List String.String
  here' t = "BlockStore" ∷ "insertSingleQuorumCertE" ∷ t

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

insertTimeoutCertificateM : TimeoutCertificate → LBFT (Either ErrLog Unit)
insertTimeoutCertificateM tc = do
  curTcRound ← maybe {-(Round-} 0 {-)-} (_^∙ tcRound) <$> use (lBlockStore ∙ bsHighestTimeoutCert)
  ifD tc ^∙ tcRound ≤?ℕ curTcRound
    then ok unit
    else
      PersistentLivenessStorage.saveHighestTimeoutCertM tc ∙^∙ withErrCtx ("" ∷ []) ∙?∙ λ _ → do
        BlockTree.replaceTimeoutCertM tc
        ok unit

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

blockExists : HashValue → BlockStore → Bool
blockExists hv bs = Map.kvm-member hv (bs ^∙ bsInner ∙ btIdToBlock)

getBlock hv bs = btGetBlock hv (bs ^∙ bsInner)

getQuorumCertForBlock : HashValue → BlockStore → Maybe QuorumCert
getQuorumCertForBlock hv bs = Map.lookup hv (bs ^∙ bsInner ∙ btIdToQuorumCert)

pathFromRootM hv = pathFromRoot hv <$> use lBlockStore

pathFromRoot hv bs = BlockTree.pathFromRoot hv (bs ^∙ bsInner)

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

syncInfoM : LBFT SyncInfo
syncInfoM =
  SyncInfo∙new <$> use (lBlockStore ∙ bsHighestQuorumCert)
               <*> use (lBlockStore ∙ bsHighestCommitCert)
               <*> use (lBlockStore ∙ bsHighestTimeoutCert)

abstract
  syncInfoM-abs = syncInfoM
  syncInfoM-abs-≡ : syncInfoM-abs ≡ syncInfoM
  syncInfoM-abs-≡ = refl


text:
module Data.Num.Standard where

open import Data.Nat using (ℕ; suc; zero; _≤?_)
open import Data.Fin using (Fin; fromℕ; #_)
open import Level using () renaming (suc to lsuc)
    -- renaming (zero to Fzero; suc to Fsuc; toℕ to F→N; fromℕ≤ to N→F)
open import Relation.Nullary.Decidable

infixr 2 [_]_

-- invariant: base ≥ 1
data Num : ℕ → Set where
    ∙ : ∀ {b} → Num (suc b)
    [_]_ : ∀ {b} → (n : ℕ) → {in-bound : True (n ≤? b)} → Num (suc b) → Num (suc b)

null : Num 2
null = [ 0 ] ∙

eins : Num 2
eins = [ 1 ] ∙

zwei : Num 3
zwei = [ 1 ] [ 2 ] ∙

carry : ∀ {b} → Num b → Num b
carry {zero} ()
carry {suc b} ∙ = [ {!   !} ] ∙
carry {suc b} ([ n ] xs) = {!   !}

_+_ : ∀ {b} → Num b → Num b → Num b
∙ + ys = ys
xs + ∙ = xs
([ x ] xs) + ([ y ] ys) = {!   !}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
open import Prelude
open import Nat
open import core
open import contexts
open import lemmas-disjointness

module lemmas-freshness where
  -- if x is fresh in an hexp, it's fresh in its expansion
  mutual
    fresh-elab-synth1 : ∀{x e τ d Γ Δ} →
                         x # Γ →
                         freshh x e →
                         Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                         fresh x d
    fresh-elab-synth1 _ FRHConst ESConst = FConst
    fresh-elab-synth1 apt (FRHAsc frsh) (ESAsc x₁) = FCast (fresh-elab-ana1 apt frsh x₁)
    fresh-elab-synth1 _ (FRHVar x₂) (ESVar x₃) = FVar x₂
    fresh-elab-synth1 {Γ = Γ} apt (FRHLam2 x₂ frsh) (ESLam x₃ exp) = FLam x₂ (fresh-elab-synth1 (apart-extend1 Γ x₂ apt) frsh exp)
    fresh-elab-synth1 apt FRHEHole ESEHole = FHole (EFId apt)
    fresh-elab-synth1 apt (FRHNEHole frsh) (ESNEHole x₁ exp) = FNEHole (EFId apt) (fresh-elab-synth1 apt frsh exp)
    fresh-elab-synth1 apt (FRHAp frsh frsh₁) (ESAp x₁ x₂ x₃ x₄ x₅ x₆) =
                               FAp (FCast (fresh-elab-ana1 apt frsh x₅))
                                   (FCast (fresh-elab-ana1 apt frsh₁ x₆))

    fresh-elab-ana1 : ∀{ x e τ d τ' Γ Δ} →
                      x # Γ →
                      freshh x e →
                      Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                      fresh x d
    fresh-elab-ana1 {Γ = Γ}  apt (FRHLam1 x₁ frsh) (EALam x₂ x₃ exp) = FLam x₁ (fresh-elab-ana1 (apart-extend1 Γ x₁ apt) frsh exp )
    fresh-elab-ana1 apt frsh (EASubsume x₁ x₂ x₃ x₄) = fresh-elab-synth1 apt frsh x₃
    fresh-elab-ana1 apt FRHEHole EAEHole = FHole (EFId apt)
    fresh-elab-ana1 apt (FRHNEHole frsh) (EANEHole x₁ x₂) = FNEHole (EFId apt) (fresh-elab-synth1 apt frsh x₂)

  -- if x is fresh in the expansion of an hexp, it's fresh in that hexp
  mutual
    fresh-elab-synth2 : ∀{x e τ d Γ Δ} →
                         fresh x d →
                         Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                         freshh x e
    fresh-elab-synth2 FConst ESConst = FRHConst
    fresh-elab-synth2 (FVar x₂) (ESVar x₃) = FRHVar x₂
    fresh-elab-synth2 (FLam x₂ frsh) (ESLam x₃ exp) = FRHLam2 x₂ (fresh-elab-synth2 frsh exp)
    fresh-elab-synth2 (FHole x₁) ESEHole = FRHEHole
    fresh-elab-synth2 (FNEHole x₁ frsh) (ESNEHole x₂ exp) = FRHNEHole (fresh-elab-synth2 frsh exp)
    fresh-elab-synth2 (FAp (FCast frsh) (FCast frsh₁)) (ESAp x₁ x₂ x₃ x₄ x₅ x₆) =
                        FRHAp (fresh-elab-ana2 frsh x₅)
                              (fresh-elab-ana2 frsh₁ x₆)
    fresh-elab-synth2 (FCast frsh) (ESAsc x₁) = FRHAsc (fresh-elab-ana2 frsh x₁)

    fresh-elab-ana2 : ∀{ x e τ d τ' Γ Δ} →
                      fresh x d →
                      Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                      freshh x e
    fresh-elab-ana2 (FLam x₁ frsh) (EALam x₂ x₃ exp) = FRHLam1 x₁ (fresh-elab-ana2 frsh exp)
    fresh-elab-ana2 frsh (EASubsume x₁ x₂ x₃ x₄) = fresh-elab-synth2 frsh x₃
    fresh-elab-ana2 (FHole x₁) EAEHole = FRHEHole
    fresh-elab-ana2 (FNEHole x₁ frsh) (EANEHole x₂ x₃) = FRHNEHole (fresh-elab-synth2 frsh x₃)

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
infix -3.14 _+_

postulate
  _+_ : Set → Set → Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2017-07-25, issue #2649, reported by gallais
-- Serialization killed range needed for error message.

-- {-# OPTIONS -v scope.clash:60 #-}

module Issue2649 where

open import Issue2649-1
open import Issue2649-2

id : (A : Set) → A → A
id A x = M.foo
  where
  module M = MyModule A x

-- Expected:
-- Duplicate definition of module M. Previous definition of module M
-- at .../Issue2649-2.agda:5,13-14


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Unsigned divisibility
------------------------------------------------------------------------
-- For signed divisibility see `Data.Integer.Divisibility.Signed`

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

module Data.Integer.Divisibility where

open import Function
open import Data.Integer
open import Data.Integer.Properties
import Data.Nat as ℕ
import Data.Nat.Properties as ℕᵖ
import Data.Nat.Divisibility as ℕᵈ
import Data.Nat.Coprimality as ℕᶜ
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Divisibility

infix 4 _∣_

_∣_ : Rel ℤ 0ℓ
_∣_ = ℕᵈ._∣_ on ∣_∣

open ℕᵈ public using (divides)

------------------------------------------------------------------------
-- Properties of divisibility

*-monoʳ-∣ : ∀ k → (k *_) Preserves _∣_ ⟶ _∣_
*-monoʳ-∣ k {i} {j} i∣j = begin
  ∣ k * i ∣       ≡⟨ abs-*-commute k i ⟩
  ∣ k ∣ ℕ.* ∣ i ∣ ∣⟨ ℕᵈ.*-cong ∣ k ∣ i∣j ⟩
  ∣ k ∣ ℕ.* ∣ j ∣ ≡⟨ sym (abs-*-commute k j) ⟩
  ∣ k * j ∣       ∎
  where open ℕᵈ.∣-Reasoning

*-monoˡ-∣ : ∀ k → (_* k) Preserves _∣_ ⟶ _∣_
*-monoˡ-∣ k {i} {j}
  rewrite *-comm i k
        | *-comm j k
        = *-monoʳ-∣ k

*-cancelˡ-∣ : ∀ k {i j} → k ≢ + 0 → k * i ∣ k * j → i ∣ j
*-cancelˡ-∣ k {i} {j} k≢0 k*i∣k*j = ℕᵈ./-cong (ℕ.pred ∣ k ∣) $ begin
  let ∣k∣-is-suc = ℕᵖ.m≢0⇒suc[pred[m]]≡m (k≢0 ∘ ∣n∣≡0⇒n≡0) in
  ℕ.suc (ℕ.pred ∣ k ∣) ℕ.* ∣ i ∣ ≡⟨ cong (ℕ._* ∣ i ∣) (∣k∣-is-suc) ⟩
  ∣ k ∣ ℕ.* ∣ i ∣                ≡⟨ sym (abs-*-commute k i) ⟩
  ∣ k * i ∣                      ∣⟨ k*i∣k*j ⟩
  ∣ k * j ∣                      ≡⟨ abs-*-commute k j ⟩
  ∣ k ∣ ℕ.* ∣ j ∣                ≡⟨ cong (ℕ._* ∣ j ∣) (sym ∣k∣-is-suc) ⟩
  ℕ.suc (ℕ.pred ∣ k ∣) ℕ.* ∣ j ∣ ∎
  where open ℕᵈ.∣-Reasoning

*-cancelʳ-∣ : ∀ k {i j} → k ≢ + 0 → i * k ∣ j * k → i ∣ j
*-cancelʳ-∣ k {i} {j} ≢0 = *-cancelˡ-∣ k ≢0 ∘
  subst₂ _∣_ (*-comm i k) (*-comm j k)


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

module Cubical.Categories.Limits.BinProduct where

open import Cubical.Categories.Category.Base
open import Cubical.Data.Sigma.Base
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.HITs.PropositionalTruncation.Base

private
  variable
    ℓ ℓ' : Level

module _ (C : Category ℓ ℓ') where
  open Category C

  module _ {x y x×y : ob}
           (π₁ : Hom[ x×y , x ])
           (π₂ : Hom[ x×y , y ]) where

    isBinProduct : Type (ℓ-max ℓ ℓ')
    isBinProduct = ∀ {z : ob} (f₁ : Hom[ z , x ]) (f₂ : Hom[ z , y ]) →
        ∃![ f ∈ Hom[ z , x×y ] ] (f ⋆ π₁ ≡ f₁) × (f ⋆ π₂ ≡ f₂)

    isPropIsBinProduct : isProp (isBinProduct)
    isPropIsBinProduct = isPropImplicitΠ (λ _ → isPropΠ2 (λ _ _ → isPropIsContr))

  record BinProduct (x y : ob) : Type (ℓ-max ℓ ℓ') where
    field
      binProdOb : ob
      binProdPr₁ : Hom[ binProdOb , x ]
      binProdPr₂ : Hom[ binProdOb , y ]
      univProp : isBinProduct binProdPr₁ binProdPr₂

  BinProducts : Type (ℓ-max ℓ ℓ')
  BinProducts = (x y : ob) → BinProduct x y

  hasBinProducts : Type (ℓ-max ℓ ℓ')
  hasBinProducts = ∥ BinProducts ∥₁

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module _ where

open import Agda.Builtin.Cubical.Glue hiding (primGlue)

primitive
  primGlue : _

max_stars_repo_name: caryoscelus/agda

max_issues_repo_name: caryoscelus/agda

max_forks_repo_name: caryoscelus/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Printing Strings During Evaluation
------------------------------------------------------------------------

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

-- see README.Debug.Trace for a use-case

module Debug.Trace where

open import Agda.Builtin.String
open import Agda.Builtin.Equality

-- Postulating the `trace` function and explaining how to compile it

postulate
  trace : ∀ {a} {A : Set a} → String → A → A

{-# FOREIGN GHC import qualified Debug.Trace as Debug #-}
{-# FOREIGN GHC import qualified Data.Text as Text #-}
{-# COMPILE GHC trace = const (const (Debug.trace . Text.unpack)) #-}

-- Because expressions involving postulates get stuck during evaluation,
-- we also postulate an equality characterising `trace`'s behaviour. By
-- declaring it as a rewrite rule we internalise that evaluation rule.

postulate
  trace-eq : ∀ {a} {A : Set a} (a : A) str → trace str a ≡ a

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE trace-eq #-}

-- Specialised version of `trace` returning the traced message.

traceId : String → String
traceId str = trace str str


text:
------------------------------------------------------------------------------
-- Common stuff used by the gcd example
------------------------------------------------------------------------------

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

module FOTC.Program.GCD.Partial.Definitions where

open import FOTC.Base
open import FOTC.Data.Nat.Divisibility.NotBy0
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- Common divisor.
CD : D → D → D → Set
CD m n cd = cd ∣ m ∧ cd ∣ n
{-# ATP definition CD #-}

-- Divisible for any common divisor.
Divisible : D → D → D → Set
Divisible m n gcd = ∀ cd → N cd → CD m n cd → cd ∣ gcd
{-# ATP definition Divisible #-}

-- Greatest that any common divisor.
GACD : D → D → D → Set
GACD m n gcd = ∀ cd → N cd → CD m n cd → cd ≤ gcd
{-# ATP definition GACD #-}

-- Greatest common divisor specification
gcdSpec : D → D → D → Set
gcdSpec m n gcd = CD m n gcd ∧ GACD m n gcd
{-# ATP definition gcdSpec #-}

x≢0≢y : D → D → Set
x≢0≢y m n = ¬ (m ≡ zero ∧ n ≡ zero)
{-# ATP definition x≢0≢y #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2013-10-21 reported by Christian Sattler
{-# OPTIONS --allow-unsolved-metas #-}
module Issue922 where

import Common.Level

f : Set → Set → Set
f x _ = x   -- Note: second argument is unused

module _ (_ : f ? ?) where
  g = f
  -- Here an instance search for the unused argument (2nd ?)
  -- is triggered.

-- Problem WAS: instance search was started in wrong context.


text:
-- Andreas, 2018-10-27, issue #3323, reported by Guillaume Brunerie
--
-- Mismatches between original and repeated parameter list
-- should not lead to internal errors.

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

data T .(b : Bool) : Set
data T b where  -- Omission of relevance info allowed
  c : Bool → T b

test : ∀{b b'} → T b ≡ T b'
test = refl

-- Should succeed.

record R (@0 b : Bool) : Set
record R b where
  field foo : Bool

-- Should succeed.


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

{- Lower can be a record if using type-in-type or allowing large eliminations:
{-# OPTIONS --type-in-type #-}
record Lower (A : Set₁) : Set where
  constructor lower
  field raise : A
open Lower
-}

postulate
  _≡_ : ∀ {A : Set₁} → A → A → Set
  Lower : (A : Set₁) → Set
  lower : ∀ {A} → A → Lower A
  raise : ∀ {A} → Lower A → A
  beta : ∀ {A} {a : A} → raise (lower a) ≡ a

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE beta #-}

data ⊥ : Set where

℘ : ∀ {ℓ} → Set ℓ → Set _
℘ {ℓ} S = S → Set

U : Set
U = Lower (∀ (X : Set) → (℘ (℘ X) → X) → ℘ (℘ X))

τ : ℘ (℘ U) → U
τ t = lower (λ X f p → t (λ x → p (f (raise x X f))))

σ : U → ℘ (℘ U)
σ s = raise s U τ

Δ : ℘ U
Δ y = Lower (∀ p → σ y p → p (τ (σ y))) → ⊥

Ω : U
Ω = τ (λ p → (∀ x → σ x p → p x))

R : ∀ p → (∀ x → σ x p → p x) → p Ω
R _ 𝟙 = 𝟙 Ω (λ x → 𝟙 (τ (σ x)))

M : ∀ x → σ x Δ → Δ x
M _ 𝟚 𝟛 =
  let 𝟛 = raise 𝟛
  in 𝟛 Δ 𝟚 (lower (λ p → 𝟛 (λ y → p (τ (σ y)))))

L : (∀ p → (∀ x → σ x p → p x) → p Ω) → ⊥
L 𝟘 = 𝟘 Δ M (lower (λ p → 𝟘 (λ y → p (τ (σ y)))))

false : ⊥
false = L R


text: module bstd.bash where

max_stars_repo_name: semenov-vladyslav/bstd

max_issues_repo_name: semenov-vladyslav/bstd

max_forks_repo_name: semenov-vladyslav/bstd


text:
module Cats.Category.Constructions.Product where

open import Relation.Binary.PropositionalEquality as PropEq using (_≡_ ; refl)
open import Data.Bool using (Bool ; true ; false ; not; if_then_else_)
open import Relation.Binary.Core using (IsEquivalence)
open import Level

open import Cats.Category.Base
open import Cats.Category.Constructions.Terminal as Terminal using (HasTerminal)
open import Cats.Functor using (Functor)
open import Cats.Util.Conv
open import Cats.Util.Logic.Constructive

import Cats.Category.Constructions.Iso as Iso
import Cats.Category.Constructions.Unique as Unique

Bool-elim : ∀ {a} {A : Bool → Set a} → A true → A false → (i : Bool) → A i
Bool-elim x y true = x
Bool-elim x y false = y

module Build {lo la l≈} (Cat : Category lo la l≈) where

  private open module Cat = Category Cat
  open Cat.≈-Reasoning
  open Iso.Build Cat
  open Unique.Build Cat
  open Terminal.Build Cat

  IsProduct : ∀ {li} {I : Set li} (O : I → Obj) P → (∀ i → P ⇒ O i)
    → Set (lo ⊔ la ⊔ l≈ ⊔ li)
  IsProduct O P proj
      = ∀ {X} (x : ∀ i → X ⇒ O i) → ∃![ u ] (∀ i → x i ≈ proj i ∘ u)

  -- TODO The types of the equalities in IsBinaryProducts are backwards, since
  -- we want the RHS to be simpler than the LHS. So, projl ∘ u ≈ xl instead
  -- of xl ≈ projl ∘ u.
  IsBinaryProduct : ∀ {A B} P → (P ⇒ A) → (P ⇒ B) → Set (lo ⊔ la ⊔ l≈)
  IsBinaryProduct {A} {B} P projl projr
      = ∀ {X} (xl : X ⇒ A) (xr : X ⇒ B)
        → ∃![ u ] (xl ≈ projl ∘ u ∧ xr ≈ projr ∘ u)

--  BinProduct→id-unique : ∀ {A B P} → {projl : P ⇒ A} → {projr : P ⇒ B}
--                       → (y : IsBinaryProduct P projl projr)
--                       → id ≈ (Unique.Build.∃!′.arr y)
--  BinProduct→id-unique = ?
--      ≈.trans (≈.sym (unique ((≈.sym id-r) , (≈.sym id-r)) )) {!arr!}

  IsBinaryProduct→IsProduct : ∀ {A B P} {pl : P ⇒ A} {pr : P ⇒ B}
    → IsBinaryProduct P pl pr
    → IsProduct (Bool-elim A B) P (Bool-elim pl pr)
  IsBinaryProduct→IsProduct isBinProd x = record
      { arr = f ⃗
      ; prop = Bool-elim (∧-eliml (∃!′.prop f)) (∧-elimr (∃!′.prop f))
      ; unique = λ eq → ∃!′.unique f (eq true , eq false)
      }
    where
      f = isBinProd (x true) (x false)

  record Product {li} {I : Set li} (O : I → Obj) : Set (lo ⊔ la ⊔ l≈ ⊔ li) where
    field
      prod : Obj
      proj : ∀ i → prod ⇒ O i
      isProduct : IsProduct O prod proj

  open Product using (proj ; isProduct ; prod)

  instance
    HasObj-Product : ∀ {li} {I : Set li} {O : I → Obj}
      → HasObj (Product O) lo la l≈
    HasObj-Product = record { Cat = Cat ; _ᴼ = Product.prod }

  BinaryProduct : Obj → Obj → Set (lo ⊔ la ⊔ l≈)
  BinaryProduct A B = Product (Bool-elim A B)

  mkBinaryProduct : ∀ {A B P} (pl : P ⇒ A) (pr : P ⇒ B)
    → IsBinaryProduct P pl pr
    → BinaryProduct A B
  mkBinaryProduct {P = P} pl pr isBinProd = record
      { isProduct = IsBinaryProduct→IsProduct isBinProd }

  nullaryProduct-Terminal : (P : Product {I = ⊥} (λ())) → IsTerminal (P ᴼ)
  nullaryProduct-Terminal P X with isProduct P {X = X} λ()
  ... | ∃!-intro arr _ unique = ∃!-intro arr _ (λ _ → unique λ())

  module _ {li} {I : Set li} {O : I → Obj} (P : Product O) where

    factorizer : ∀ {X} → (∀ i → X ⇒ O i) → X ⇒ P ᴼ
    factorizer proj = isProduct P proj ⃗

    factorizer-proj : ∀ {X} {x : ∀ i → X ⇒ O i} {i}
      → proj P i ∘ factorizer x ≈ x i
    factorizer-proj {x = x} {i} = ≈.sym (∃!′.prop (isProduct P x) i)

    factorizer-resp : ∀ {X} {x y : ∀ i → X ⇒ O i}
      → (∀ i → x i ≈ y i)
      → factorizer x ≈ factorizer y
    factorizer-resp {x = x} {y} eq
        = ∃!′.unique (isProduct P x)
            (λ i → ≈.trans (eq i) (≈.sym factorizer-proj))

    factorizer-∘ : ∀ {X} {x : ∀ i → X ⇒ O i} {Z} {f : Z ⇒ X}
      → factorizer x ∘ f ≈ factorizer (λ i → x i ∘ f)
    factorizer-∘ {x = x} {f = f} = ≈.sym (
          ∃!′.unique (isProduct P (λ i → x i ∘ f))
            (λ i → ≈.sym (≈.trans unassoc (∘-resp-l factorizer-proj)))
        )

  module _ {li} {I : Set li}
    {O : I → Obj}  (P : Product O)
    {O′ : I → Obj} (P′ : Product O′)
    where

    times : (∀ i → O i ⇒ O′ i) → P ᴼ ⇒ P′ ᴼ
    times x = factorizer P′ (λ i → x i ∘ proj P i)

    times-proj : ∀ {x : ∀ i → O i ⇒ O′ i} {i}
      → proj P′ i ∘ times x ≈ x i ∘ proj P i
    times-proj = factorizer-proj P′

    times-resp : {x y : ∀ i → O i ⇒ O′ i}
      → (∀ i → x i ≈ y i)
      → times x ≈ times y
    times-resp {x} {y} eq = factorizer-resp P′ (λ i → ∘-resp-l (eq i))

  times-∘ : ∀ {li} {I : Set li}
    → {O O′ O″ : I → Obj}
    → (P : Product O) (P′ : Product O′) (P″ : Product O″)
    → {x : ∀ i → O i ⇒ O′ i} {y : ∀ i → O′ i ⇒ O″ i}
    → times P′ P″ y ∘ times P P′ x ≈ times P P″ (λ i → y i ∘ x i)
  times-∘ P P′ P″ {x} {y} =
    begin
      times P′ P″ y ∘ times P P′ x
    ≈⟨ factorizer-∘ P″ ⟩
      factorizer P″ (λ i → (y i ∘ proj P′ i) ∘ times P P′ x)
    ≈⟨ factorizer-resp P″ (λ i → assoc) ⟩
      factorizer P″ (λ i → y i ∘ proj P′ i ∘ times P P′ x)
    ≈⟨ factorizer-resp P″ (λ i → ∘-resp-r (times-proj P P′)) ⟩
      factorizer P″ (λ i → y i ∘ x i ∘ proj P i)
    ≈⟨ factorizer-resp P″ (λ i → unassoc) ⟩
      times P P″ (λ i → y i ∘ x i)
    ∎

  tim-fac : ∀ {li} {X} {I : Set li}
     → {O O′ : I → Obj}
     → (P : Product O) (P′ : Product O′)
     → {x : ∀ i → X ⇒ O i} {y : ∀ i → O i ⇒ O′ i}
     → times P P′ y ∘ factorizer P x ≈ factorizer P′ (λ i → y i ∘ x i)
  tim-fac P P′ {x} {y} =
    begin
      times P P′ y ∘ factorizer P x
    ≈⟨ factorizer-∘ P′ ⟩
      factorizer P′ (λ i → (y i ∘ proj P i) ∘ factorizer P x)
    ≈⟨ factorizer-resp P′ (λ i → assoc) ⟩
      factorizer P′ (λ i → y i ∘ proj P i ∘ factorizer P x)
    ≈⟨ factorizer-resp P′ (λ i → (∘-resp-r (factorizer-proj P))) ⟩
      factorizer P′ (λ i → y i ∘ x i)
    ∎

  proj-cancel : ∀ {li} {I : Set li} {O : I → Obj} {P proj}
    → IsProduct O P proj
    → ∀ {X} {f g : X ⇒ P}
    → (∀ i → proj i ∘ f ≈ proj i ∘ g)
    → f ≈ g
  proj-cancel {proj = proj} prod {f = f} {g} eq with prod (λ i → proj i ∘ g)
  ... | ∃!-intro u _ u-uniq
      = begin
          f
        ≈⟨ ≈.sym (u-uniq (λ i → ≈.sym (eq i))) ⟩
          u
        ≈⟨ u-uniq (λ i → ≈.refl) ⟩
          g
        ∎

record HasProducts {lo la l≈} li (C : Category lo la l≈)
  : Set (suc li ⊔ lo ⊔ la ⊔ l≈ )
  where
  private open module Bld = Build C using (Product)
  open Category C

  field
    Π′ : {I : Set li} (O : I → Obj) → Product O

  module _ {I : Set li} where

    Π : ∀ (O : I → Obj) → Obj
    Π O = Π′ O ᴼ

    syntax Π (λ i → O) = Π[ i ] O

    proj : ∀ {O : I → Obj} i → Π O ⇒ O i
    proj {O} = Bld.Product.proj (Π′ O)

    factorizer : ∀ {O : I → Obj} {X} → (∀ i → X ⇒ O i) → X ⇒ Π O
    factorizer {O} = Bld.factorizer (Π′ O)

    times : ∀ {O O′ : I → Obj} → (∀ i → O i ⇒ O′ i) → Π O ⇒ Π O′
    times {O} {O′} = Bld.times (Π′ O) (Π′ O′)

    factorizer-proj : ∀ {O : I → Obj} {X} {x : ∀ i → X ⇒ O i} {i}
      → proj i ∘ factorizer x ≈ x i
    factorizer-proj {O} = Bld.factorizer-proj (Π′ O)

    factorizer-resp : ∀ {O : I → Obj} {X} {x y : ∀ i → X ⇒ O i}
      → (∀ i → x i ≈ y i)
      → factorizer x ≈ factorizer y
    factorizer-resp {O} = Bld.factorizer-resp (Π′ O)

    factorizer-∘ : ∀ {O : I → Obj} {X} {x : ∀ i → X ⇒ O i} {Z} {f : Z ⇒ X}
      → factorizer x ∘ f ≈ factorizer (λ i → x i ∘ f)
    factorizer-∘ {O} = Bld.factorizer-∘ (Π′ O)

    times-proj : ∀ {O O′ : I → Obj} {x : ∀ i → O i ⇒ O′ i} {i}
      → proj i ∘ times x ≈ x i ∘ proj i
    times-proj {O} {O′} = Bld.times-proj (Π′ O) (Π′ O′)

    times-resp : ∀ {O O′ : I → Obj} {x y : ∀ i → O i ⇒ O′ i}
      → (∀ i → x i ≈ y i)
      → times x ≈ times y
    times-resp {O} {O′} = Bld.times-resp (Π′ O) (Π′ O′)

    times-∘ : ∀ {O O′ O″ : I → Obj} {x : ∀ i → O i ⇒ O′ i} {y : ∀ i → O′ i ⇒ O″ i}
      → times y ∘ times x ≈ times (λ i → y i ∘ x i)
    times-∘ {O} {O′} {O″} = Bld.times-∘ (Π′ O) (Π′ O′) (Π′ O″)

HasProducts→HasTerminal : ∀ {lo la l≈} {C : Category lo la l≈}
  → HasProducts zero C
  → HasTerminal C
HasProducts→HasTerminal {C = C} record { Π′ = Π }
    = let P = Π {I = ⊥} λ() in
      record
        { One = P ᴼ
        ; isTerminal = Build.nullaryProduct-Terminal C P
        }

record HasBinaryProducts {lo la l≈} (C : Category lo la l≈)
  : Set (lo ⊔ la ⊔ l≈)
  where
  private open module Bld = Build C using (BinaryProduct ; Product)
  open Category C
  open ≈-Reasoning

  infixr 2 _×_ _×′_ ⟨_×_⟩ ⟨_,_⟩

  field
    _×′_ : ∀ A B → BinaryProduct A B

  _×_ : Obj → Obj → Obj
  A × B = (A ×′ B) ᴼ

  projl : ∀ {A B} → A × B ⇒ A
  projl {A} {B} = Product.proj (A ×′ B) true

  projr : ∀ {A B} → A × B ⇒ B
  projr {A} {B} = Product.proj (A ×′ B) false

  ⟨_,_⟩ : ∀ {A B Z} → Z ⇒ A → Z ⇒ B → Z ⇒ A × B
  ⟨_,_⟩ {A} {B} f g
      = Bld.factorizer (A ×′ B) (Bool-elim f g)

  ⟨_×_⟩ : ∀ {A B A′ B′} → A ⇒ A′ → B ⇒ B′ → A × B ⇒ A′ × B′
  ⟨_×_⟩ {A} {B} {A′} {B′} f g
      = Bld.times (A ×′ B) (A′ ×′ B′) (Bool-elim f g)

  first : ∀ {A A′ B} → A ⇒ A′ → A × B ⇒ A′ × B
  first f = ⟨ f × id ⟩

  second : ∀ {A B B′} → B ⇒ B′ → A × B ⇒ A × B′
  second f = ⟨ id × f ⟩

  swap : ∀ {A B} → A × B ⇒ B × A
  swap = ⟨ projr , projl ⟩

  ⟨,⟩-resp : ∀ {A B Z} {f f′ : Z ⇒ A} {g g′ : Z ⇒ B}
    → f ≈ f′
    → g ≈ g′
    → ⟨ f , g ⟩ ≈ ⟨ f′ , g′ ⟩
  ⟨,⟩-resp {A} {B} f≈f′ g≈g′
      = Bld.factorizer-resp (A ×′ B) (Bool-elim f≈f′ g≈g′)

  ⟨,⟩-projl : ∀ {A B Z} {f : Z ⇒ A} {g : Z ⇒ B} → projl ∘ ⟨ f , g ⟩ ≈ f
  ⟨,⟩-projl {A} {B} = Bld.factorizer-proj (A ×′ B)

  ⟨,⟩-projr : ∀ {A B Z} {f : Z ⇒ A} {g : Z ⇒ B} → projr ∘ ⟨ f , g ⟩ ≈ g
  ⟨,⟩-projr {A} {B} = Bld.factorizer-proj (A ×′ B)

  data Singleton {a} {A : Set a} (x : A) : Set a where
    _with≡_ : (y : A) → x ≡ y → Singleton x

  inspect : ∀ {a} {A : Set a} (x : A) → Singleton x
  inspect x = x with≡ refl

  ⟨projr,projl⟩-id : {A B : Obj} → ⟨ projl , projr ⟩ ≈ id {A × B}
  ⟨projr,projl⟩-id {A} {B} with inspect (A ×′ B)
  ... | record { prod = .(Product.prod (A ×′ B)) ; proj = proj ; isProduct = isProduct } with≡ refl with (isProduct proj)
  ... | Unique.Build.∃!-intro arr prop unique = ≈.trans (≈.sym (unique (Bool-elim (≈.sym ⟨,⟩-projl) (≈.sym ⟨,⟩-projr))) ) (unique λ i → ≈.sym id-r)

--... | p (record { prod = prod' ; proj = proj ; isProduct = isProduct }) with (isProduct proj)
--  ... | Unique.Build.∃!-intro arr prop unique = ≈.trans (≈.sym (unique (Bool-elim {!⟨,⟩-projl {A} {B}  {f = projl} {g = projr}!} {!!})) ) (unique λ i → ≈.sym id-r)

  ⟨,⟩-∘ : ∀ {A B Y Z} {f : Y ⇒ Z} {g : Z ⇒ A} {h : Z ⇒ B}
    → ⟨ g , h ⟩ ∘ f ≈ ⟨ g ∘ f , h ∘ f ⟩
  ⟨,⟩-∘ {A} {B} {Y} {Z} {f} {g} {h}
      = begin
          ⟨ g , h ⟩ ∘ f
        ≈⟨ Bld.factorizer-∘ (A ×′ B) ⟩
        Bld.factorizer (A ×′ B)
            (λ i → Bool-elim {A = λ i → Z ⇒ Bool-elim A B i} g h i ∘ f)
        ≈⟨ Bld.factorizer-resp (A ×′ B) (Bool-elim ≈.refl ≈.refl) ⟩
          ⟨ g ∘ f , h ∘ f ⟩
        ∎

  ⟨×⟩-resp : ∀ {A A′ B B′} {f f′ : A ⇒ A′} {g g′ : B ⇒ B′}
    → f ≈ f′
    → g ≈ g′
    → ⟨ f × g ⟩ ≈ ⟨ f′ × g′ ⟩
  ⟨×⟩-resp {A} {A′} {B} {B′} f≈f′ g≈g′
      = Bld.times-resp (A ×′ B) (A′ ×′ B′) (Bool-elim f≈f′ g≈g′)

  ⟨×⟩-projl : ∀ {A A′ B B′} {f : A ⇒ A′} {g : B ⇒ B′}
    → projl ∘ ⟨ f × g ⟩ ≈ f ∘ projl
  ⟨×⟩-projl {A} {A′} {B} {B′} = Bld.times-proj (A ×′ B) (A′ ×′ B′)

  ⟨×⟩-projr : ∀ {A A′ B B′} {f : A ⇒ A′} {g : B ⇒ B′}
    → projr ∘ ⟨ f × g ⟩ ≈ g ∘ projr
  ⟨×⟩-projr {A} {A′} {B} {B′} = Bld.times-proj (A ×′ B) (A′ ×′ B′)

  ⟨×⟩-∘ : ∀ {A A′ A″ B B′ B″}
    → {f : A′ ⇒ A″} {f′ : A ⇒ A′} {g : B′ ⇒ B″} {g′ : B ⇒ B′}
    → ⟨ f × g ⟩ ∘ ⟨ f′ × g′ ⟩ ≈ ⟨ f ∘ f′ × g ∘ g′ ⟩
  ⟨×⟩-∘ {A} {A′} {A″} {B} {B′} {B″} {f} {f′} {g} {g′}
      = begin
          ⟨ f × g ⟩ ∘ ⟨ f′ × g′ ⟩
        ≈⟨ Bld.times-∘ (A ×′ B) (A′ ×′ B′) (A″ ×′ B″) ⟩
          Bld.times (A ×′ B) (A″ ×′ B″)
            (λ i →
              Bool-elim {A = λ i → Bool-elim A′ B′ i ⇒ Bool-elim A″ B″ i} f g i ∘
              Bool-elim {A = λ i → Bool-elim A B i ⇒ Bool-elim A′ B′ i} f′ g′ i)
        ≈⟨ Bld.times-resp (A ×′ B) (A″ ×′ B″) (Bool-elim ≈.refl ≈.refl) ⟩
          ⟨ f ∘ f′ × g ∘ g′ ⟩
        ∎

  ⟨×⟩-∘-⟨,⟩ : ∀ {X A A′ B B′}
         → {u : X ⇒ A}{v : X ⇒ A′}{f : A ⇒ B}{g : A′ ⇒ B′}
         → ⟨ f × g ⟩ ∘ ⟨ u , v ⟩ ≈ ⟨ f ∘ u , g ∘ v ⟩
  ⟨×⟩-∘-⟨,⟩ {X} {A} {A′} {B} {B′} {u} {v} {f} {g}
    = begin
        ⟨ f × g ⟩ ∘ ⟨ u , v ⟩
      ≈⟨ Bld.tim-fac (A ×′ A′) (B ×′ B′) ⟩
        Bld.factorizer (B ×′ B′) ( λ i →
        Bool-elim {A = λ i → Bool-elim A A′ i ⇒ Bool-elim B B′ i} f g i ∘
        Bool-elim {A = λ i → X ⇒ Bool-elim A A′ i} u v i)
        -- {A = λ i → X ⇒ Bool-elim B B′ i} (f ∘ u) (g ∘ v) i)
      ≈⟨ Bld.factorizer-resp (B ×′ B′) (Bool-elim ≈.refl ≈.refl) ⟩
        ⟨ f ∘ u , g ∘ v ⟩
      ∎

-- The following is conceptually trivial, but we have to dig quite deep to
-- avoid level-related nonsense.
HasProducts→HasBinaryProducts : ∀ {lp lo la l≈} {C : Category lo la l≈}
  → HasProducts lp C
  → HasBinaryProducts C
HasProducts→HasBinaryProducts {lp} {C = C} record { Π′ = Π }
    = record { _×′_ = _×_ }
  where
    open Category C
    open Unique.Build C
    open Build C
    open Product using (proj ; isProduct)
    open ∃!′ using (arr ; prop ; unique)

    _×_ : ∀ A B → Build.BinaryProduct C A B
    A × B = record
        { prod = prod′
        ; proj = proj′
        ; isProduct = isProduct′
        }
      where
        O : Lift lp Bool → _
        O (lift true) = A
        O (lift false) = B

        prod′ = Π O ᴼ

        proj′ = Bool-elim (proj (Π O) (lift true)) (proj (Π O) (lift false))

        isProduct′ : IsProduct (Bool-elim A B) prod′ proj′
        isProduct′ {X} x = record
            { arr = arr′ ⃗
            ; prop = Bool-elim (prop arr′ (lift true)) (prop arr′ (lift false))
            ; unique = λ eq → unique arr′
                (λ { (lift true) → eq true ; (lift false) → eq false})
            }
          where
            arr′ = isProduct (Π O)
              λ { (lift true) → x true ; (lift false) → x false}

record HasFiniteProducts {lo la l≈} (Cat : Category lo la l≈)
  : Set (lo ⊔ la ⊔ l≈)
  where

  field
    {{hasTerminal}} : HasTerminal Cat
    {{hasBinaryProducts}} : HasBinaryProducts Cat

  open HasTerminal hasTerminal public
  open HasBinaryProducts hasBinaryProducts public

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈}
  {D : Category lo′ la′ l≈′}
  where

  open Category C
  open Build using (IsProduct ; IsBinaryProduct)
  open Functor

  PreservesBinaryProducts : (F : Functor C D) → Set _
  PreservesBinaryProducts F
    = ∀ {A B A×B} {projl : A×B ⇒ A} {projr : A×B ⇒ B}
    → IsBinaryProduct C A×B projl projr
    → IsBinaryProduct D (fobj F A×B) (fmap F projl) (fmap F projr)

  PreservesProducts : ∀ {i} (I : Set i) (F : Functor C D) → Set _
  PreservesProducts I F
    = ∀ {O : I → Obj} {P} {proj : ∀ i → P ⇒ O i}
    → IsProduct C O P proj
    → IsProduct D (λ i → fobj F (O i)) (fobj F P) (λ i → fmap F (proj i))

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-# OPTIONS --without-K --safe #-}
module Experiment.Applicative where

open import Function.Base
open import Relation.Binary.PropositionalEquality

record Functor (F : Set → Set) : Set₁ where
  field
    fmap    : ∀ {A B} → (A → B) → F A → F B
  field
    fmap-id : ∀ {A} (x : F A) → fmap id x ≡ x
    fmap-∘  : ∀ {A B C} (f : B → C) (g : A → B) (x : F A) →
      fmap f (fmap g x) ≡ fmap (f ∘′ g) x
    fmap-cong : ∀ {A B} {f g : A → B} {x : F A} →
      (∀ v → f v ≡ g v) → fmap f x ≡ fmap g x

record Applicative (F : Set → Set) : Set₁ where
  infixl 5 _<*>_
  field
    pure  : ∀ {A} → A → F A
    _<*>_ : ∀ {A B} → F (A → B) → F A → F B
  field
    identity : ∀ {A} (v : F A) → pure id <*> v ≡ v
    composition : ∀ {A B C} (u : F (A → C)) (v : F (B → A)) (w : F B) →
      pure _∘′_ <*> u <*> v <*> w ≡ u <*> (v <*> w)
    homomorphism : ∀ {A B} (f : A → B) (x : A) → pure f <*> pure x ≡ pure (f x)
    interchange : ∀ {A B} (u : F (A → B)) (y : A) →
      u <*> pure y ≡ pure (_$ y) <*> u
    -- <*>-cong : (∀ x → ff <*> pure x ≡ fg <*> pure x) → ff <*> fx ≡ fg <*> fx
  homomorphism₂ : ∀ {A B C} (f : A → B → C) (x : A) (y : B) →
    pure f <*> pure x <*> pure y ≡ pure (f x y)
  homomorphism₂ f x y = begin
    pure f <*> pure x <*> pure y ≡⟨ cong (_<*> pure y) $ homomorphism f x ⟩
    pure (f x) <*> pure y        ≡⟨ homomorphism (f x) y ⟩
    pure (f x y)                 ∎
    where open ≡-Reasoning

  functor : Functor F
  functor = record
    { fmap    = λ f fx → pure f <*> fx
    ; fmap-id = identity
    ; fmap-∘  = λ f g x → begin
      pure f <*> (pure g <*> x)
        ≡⟨ sym $ composition (pure f) (pure g) x ⟩
      pure _∘′_ <*> pure f <*> pure g <*> x
        ≡⟨ cong (λ v → v <*> x) $ homomorphism₂ _∘′_ f g ⟩
      pure (f ∘′ g) <*> x
        ∎
    ; fmap-cong = λ {A} {B} {f = f} {g = g} {x = x} f≡g → {!   !}
    }
    where open ≡-Reasoning

  liftA2 : ∀ {A B C} → (A → B → C) → F A → F B → F C
  liftA2 f fx fy = pure f <*> fx <*> fy
{-
forall x y. p (q x y) = f x . g y
it follows from the above that

liftA2 p (liftA2 q u v) = liftA2 f u . liftA2 g v
-}
record ApplicativeViaZip (F : Set → Set) : Set₁ where
  field
    pair : F A → F B → F (A × B)
    pair fx fy = ?
record Monad (F : Set → Set) : Set₁ where
  infixl 5 _>>=_
  field
    return : ∀ {A} → A → F A
    _>>=_ : ∀ {A B} → F A → (A → F B) → F B
  field
    identityˡ : ∀ {A B} (a : A) (k : A → F B) → return a >>= k ≡ k a
    identityʳ : ∀ {A} (m : F A) → m >>= return ≡ m
    assoc : ∀ {A B C} (m : F A) (k : A → F B) (h : B → F C) →
      m >>= (λ x → k x >>= h) ≡ (m >>= k) >>= h

  join : ∀ {A} → F (F A) → F A
  join x = x >>= id
-- pure f <*> x ≡ pure g <*> x
  m >>= k = join (fmap k m)
  (∀ x → k x ≡ l x)
  join (fmap k m)
  join (fmap l m

  liftM1 : ∀ {A B} → (A → B) → F A → F B
  liftM1 f mx = mx >>= (λ x → return (f x))

  functor : Functor F
  functor = record
    { fmap    = liftM1
    ; fmap-id = λ fx → identityʳ fx
    ; fmap-∘  = λ f g x → begin
      liftM1 f (liftM1 g x) ≡⟨ refl ⟩
      liftM1 g x >>= (λ y → return (f y)) ≡⟨ refl ⟩
      (x >>= (λ y → return (g y))) >>= (λ y → return (f y))
        ≡⟨ sym $ assoc x (λ y → return (g y)) (λ y → return (f y)) ⟩
      x >>= (λ y → return (g y) >>= (return ∘ f) )
        ≡⟨ cong (λ v → x >>= v) $ {!   !} ⟩
      x >>= (λ y → return (f (g y))) ≡⟨ refl ⟩
      liftM1 (f ∘′ g) x ∎
    }
    where open ≡-Reasoning

  applicative : Applicative F
  applicative = record
    { pure         = return
    ; _<*>_        = λ fab fa → fab >>= λ ab → fa >>= λ a → return (ab a)
    ; identity     = λ v → begin
      return id >>= (λ ab → v >>= λ a → return (ab a)) ≡⟨ identityˡ id _ ⟩
      v >>= return                                     ≡⟨ identityʳ v ⟩
      v                                                ∎
    ; composition  = λ u v w → begin
      return _∘′_ >>= (λ f → u >>= (return ∘ f)) >>= (λ f → v >>= (return ∘ f))
        >>= (λ f → w >>= (return ∘ f)) ≡⟨ {!   !} ⟩
      u >>= (λ f → v >>= (λ g → w >>= (return ∘ g)) >>= (return ∘ f))
       ∎
    ; homomorphism = {!   !}
    ; interchange  = {!   !}
    }
    where open ≡-Reasoning
{-
return _∘′_ >>= (λ f → u >>= (λ a → return (f a))) >>=
(λ f → v >>= (λ a → return (f a)))
>>= (λ f → w >>= (λ a → return (f a)))
≡
u >>=
(λ f →
   v >>= (λ g → w >>= (λ a → return (g a))) >>=
   (λ a → return (f a)))
-}
-- Traversable


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

open import Agda.Builtin.Equality

postulate
  A : Set
  P : Prop
  p : P
  f : P → A

mutual
  X : A
  X = _

  test₁ : (x : P) → X ≡ f x
  test₁ x = refl

  test₂ : X ≡ f p
  test₂ = refl


text:
-- Andreas, 2016-12-15, issue #2341
-- `with` needs to abstract also in sort of target type.

-- {-# OPTIONS -v tc.with:100 #-}

open import Agda.Primitive

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

{-# BUILTIN EQUALITY _≡_ #-}

postulate
  equalLevel : (x y : Level) → x ≡ y

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

Works : ∀ β α → Set α → Set β
Works β α with equalLevel α β
Works β .β | refl = id

Coerce : ∀ β α → Set α → Set β
Coerce β α rewrite equalLevel α β = id

-- Should succeed

{-
Set α →{1+β⊔α} Set β
added with function .Issue2341.rewrite-42 of type
  (β α w : Level) → w ≡ β → Set w → Set β

  (β α : Level) → (w : Level) →{1+β⊔α} w ≡ β →{1+β⊔α} Set w →{1+β⊔α} Set β

  raw with func. type = El {_getSort = Inf, unEl =
Pi ru(El {_getSort = Type (Max []), unEl = Def Agda.Primitive.Level []}) (Abs "\946" El {_getSort = Inf, unEl =
Pi ru(El {_getSort = Type (Max []), unEl = Def Agda.Primitive.Level []}) (Abs "\945"
  El {_getSort = Type (Max [Plus 1 (UnreducedLevel (Var 0 [])),Plus 1 (UnreducedLevel (Var 1 []))]), unEl =
Pi ru(El {_getSort = Type (Max []), unEl = Def Agda.Primitive.Level []}) (Abs "w"
  El {_getSort = Type (Max [Plus 1 (UnreducedLevel (Var 1 [])),Plus 1 (UnreducedLevel (Var 2 []))]), unEl =
Pi ru(El {_getSort = Type (Max []), unEl = Def Issue2341._≡_ [Apply ru{Level (Max [])},Apply ru{Def Agda.Primitive.Level []},Apply ru(Var 0 []),Apply ru(Var 2 [])]}) (NoAbs "w"
  El {_getSort = Type (Max [Plus 1 (UnreducedLevel (Var 1 [])),Plus 1 (UnreducedLevel (Var 2 []))]), unEl =
Pi ru(El {_getSort = Type (Max [Plus 1 (UnreducedLevel (Var 0 []))]), unEl = Sort (Type (Max [Plus 0 (UnreducedLevel (Var 0 []))]))}) (NoAbs "_"
  El {_getSort = Type (Max [Plus 1 (UnreducedLevel (Var 2 []))]), unEl =
Sort (Type (Max [Plus 0 (UnreducedLevel (Var 2 []))]))})})})})})}
-}


text:
module Thesis.SIRelBigStep.DSyntax where

open import Thesis.SIRelBigStep.Syntax public

-- data DType : Set where
--   _⇒_ : (σ τ : DType) → DType
--   int : DType
DType = Type

import Base.Syntax.Context
module DC = Base.Syntax.Context DType

Δτ : Type → DType
Δτ (σ ⇒ τ) = σ ⇒ Δτ σ ⇒ Δτ τ
Δτ (pair τ1 τ2) = pair (Δτ τ1) (Δτ τ2)
Δτ nat = nat

ΔΔ : Context → DC.Context
ΔΔ ∅ = ∅
ΔΔ (τ • Γ) = Δτ τ • ΔΔ Γ
--ΔΔ Γ = Γ

-- A DTerm evaluates in normal context Δ, change context (ΔΔ Δ), and produces
-- a result of type (Δt τ).
data DTerm (Δ : Context) (τ : DType) : Set
data DSVal (Δ : Context) : (τ : DType) → Set where
  dvar : ∀ {τ} →
    (x : Var Δ τ) →
    DSVal Δ τ
  dabs : ∀ {σ τ}
    (dt : DTerm (σ • Δ) τ) →
    DSVal Δ (σ ⇒ τ)
  dcons : ∀ {τ1 τ2}
    (dsv1 : DSVal Δ τ1)
    (dsv2 : DSVal Δ τ2) →
    DSVal Δ (pair τ1 τ2)
  dconst : ∀ {τ} → (dc : Const (Δτ τ)) → DSVal Δ τ

data DTerm (Δ : Context) (τ : DType) where
  dval :
    DSVal Δ τ →
    DTerm Δ τ
  dprimapp : ∀ {σ}
    (p : Primitive (σ ⇒ τ)) →
    (sv : SVal Δ σ) →
    (dsv : DSVal Δ σ) →
    DTerm Δ τ
  dapp : ∀ {σ}
    (dvs : DSVal Δ (σ ⇒ τ)) →
    (vt : SVal Δ σ) →
    (dvt : DSVal Δ σ) →
    DTerm Δ τ
  dlett : ∀ {σ}
    (s : Term Δ σ) →
    (ds : DTerm Δ σ) →
    (dt : DTerm (σ • Δ) τ) →
    DTerm Δ τ

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module AbsurdPatternRequiresNoRHS where

data   False : Set where
record True  : Set where

f : False -> True
f () = _


text:
-- Andreas, 2015-07-13  Better parse errors for illegal type signatures

(A B) : Set1
A B = Set


text:
module Properties.Step where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Float using (primFloatPlus; primFloatMinus; primFloatTimes; primFloatDiv)
open import FFI.Data.Maybe using (just; nothing)
open import Luau.Heap using (Heap; _[_]; alloc; ok; function_is_end)
open import Luau.Syntax using (Block; Expr; nil; var; addr; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg; number; binexp; +)
open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app₁ ; app₂ ; beta; function; block; return; done; local; subst; binOpEval; evalBinOp; binOp₁; binOp₂)
open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; local; return; bin₁; bin₂)
open import Luau.RuntimeType using (function; number)
open import Luau.Substitution using (_[_/_]ᴮ)
open import Luau.Value using (nil; addr; val; number)
open import Properties.Remember using (remember; _,_)

data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
data StepResultᴱ {a} (H : Heap a) (M : Expr a) : Set

data StepResultᴮ H B where
  step : ∀ H′ B′ → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → StepResultᴮ H B
  return : ∀ V {B′} → (B ≡ (return (val V) ∙ B′)) → StepResultᴮ H B
  done : (B ≡ done) → StepResultᴮ H B
  error : (RuntimeErrorᴮ H B) → StepResultᴮ H B

data StepResultᴱ H M where
  step : ∀ H′ M′ → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → StepResultᴱ H M
  value : ∀ V → (M ≡ val V) → StepResultᴱ H M
  error : (RuntimeErrorᴱ H M) → StepResultᴱ H M

stepᴱ : ∀ {a} H M → StepResultᴱ {a} H M
stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B

stepᴱ H nil = value nil refl
stepᴱ H (var x) = error (UnboundVariable x)
stepᴱ H (addr a) = value (addr a) refl
stepᴱ H (number x) = value (number x) refl
stepᴱ H (M $ N) with stepᴱ H M
stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app₁ D)
stepᴱ H (_ $ N) | value V refl with stepᴱ H N
stepᴱ H (_ $ N) | value V refl | step H′ N′ s = step H′ (val V $ N′) (app₂ s)
stepᴱ H (_ $ _) | value nil refl | value W refl = error (app₁ (TypeMismatch function nil λ()))
stepᴱ H (_ $ _) | value (number n) refl | value W refl = error (app₁ (TypeMismatch function (number n) λ()))
stepᴱ H (_ $ _) | value (addr a) refl | value W refl with remember (H [ a ])
stepᴱ H (_ $ _) | value (addr a) refl | value W refl  | (nothing , p) = error (app₁ (SEGV a p))
stepᴱ H (_ $ _) | value (addr a) refl | value W refl  | (just(function F is B end) , p) = step H (block fun F is B [ W / name (arg F) ]ᴮ end) (beta p)
stepᴱ H (M $ N) | value V p | error E = error (app₂ E)
stepᴱ H (M $ N) | error E = error (app₁ E)
stepᴱ H (block b is B end) with stepᴮ H B
stepᴱ H (block b is B end) | step H′ B′ D = step H′ (block b is B′ end) (block D)
stepᴱ H (block b is (return _ ∙ B′) end) | return V refl = step H (val V) return
stepᴱ H (block b is done end) | done refl = step H nil done
stepᴱ H (block b is B end) | error E = error (block b E)
stepᴱ H (function F is C end) with alloc H (function F is C end)
stepᴱ H function F is C end | ok a H′ p = step H′ (addr a) (function p)
stepᴱ H (binexp x op y) with stepᴱ H x
stepᴱ H (binexp x op y) | value x′ refl with stepᴱ H y
stepᴱ H (binexp x op y) | value (number x′) refl | value (number y′) refl = step H (number (evalBinOp x′ op y′)) binOpEval
stepᴱ H (binexp x op y) | value (number x′) refl | step H′ y′ s = step H′ (binexp (number x′) op y′) (binOp₂ s)
stepᴱ H (binexp x op y) | value (number x′) refl | error E = error (bin₂ E)
stepᴱ H (binexp x op y) | value nil refl | _ = error (bin₁ (TypeMismatch number nil λ()))
stepᴱ H (binexp x op y) | _ | value nil refl = error (bin₂ (TypeMismatch number nil λ()))
stepᴱ H (binexp x op y) | value (addr a) refl | _ = error (bin₁ (TypeMismatch number (addr a) λ()))
stepᴱ H (binexp x op y) | _ | value (addr a) refl = error (bin₂ (TypeMismatch number (addr a) λ()))
stepᴱ H (binexp x op y) | step H′ x′ s = step H′ (binexp x′ op y) (binOp₁ s)
stepᴱ H (binexp x op y) | error E = error (bin₁ E)

stepᴮ H (function F is C end ∙ B) with alloc H (function F is C end)
stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / fun F ]ᴮ) (function p)
stepᴮ H (local x ← M ∙ B) with stepᴱ H M
stepᴮ H (local x ← M ∙ B) | step H′ M′ D = step H′ (local x ← M′ ∙ B) (local D)
stepᴮ H (local x ← _ ∙ B) | value V refl = step H (B [ V / name x ]ᴮ) subst
stepᴮ H (local x ← M ∙ B) | error E = error (local x E)
stepᴮ H (return M ∙ B) with stepᴱ H M
stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (return D)
stepᴮ H (return _ ∙ B) | value V refl = return V refl
stepᴮ H (return M ∙ B) | error E = error (return E)
stepᴮ H done = done refl