text:
{- SAMPLE PROGRAMS IN SOURCE LANGUAGE -}

open import Preliminaries
open import Source
open import Pilot2
open import Translation
open import Interp
open import Preorder

module Samples where

  s2r : ∀ {Γ τ} → Γ Source.|- τ → (el ([ (⟨⟨ Γ ⟩⟩c) ]c ->p [ (|| τ ||) ]t))
  s2r p = interpE || p ||e

  -- this works
  {- dbl (n : nat) : nat = 2 * n -}
  dbl : ∀ {Γ} → Γ Source.|- (nat ->s nat)
  dbl = lam (rec (var i0) z (suc (suc (force (var (iS i0))))))

  -- this works
  {- add (m n : nat) : nat = m + n -}
  add : ∀ {Γ} → Γ Source.|- (nat ->s (nat ->s nat))
  add = lam (lam (rec (var (iS i0)) (var i0) (suc (force (var (iS i0))))))

  -- this works
  {- mult (m n : nat) : nat = m * n -}
  mult : ∀ {Γ} → Γ Source.|- (nat ->s (nat ->s nat))
  mult = lam (lam (rec (var (iS i0)) z (app (app add (var (iS (iS i0)))) (force (var (iS i0))))))

  -- this works
  {- pred (n : nat) : nat = predecessor of n -}
  pred : ∀ {Γ} → Γ Source.|- (nat ->s nat)
  pred = lam (rec (var i0) z (var i0))

  -- uhhhh
  fastfib : ∀ {Γ} → Γ Source.|- (nat ->s (nat ×s nat))
  fastfib =
    lam (rec (var i0) (prod z (suc z))
      (prod (split (force (var (iS i0))) (var (iS i0)))
        (app (app add (split (force (var (iS i0))) (var i0))) (split (force (var (iS i0))) (var (iS i0))))))

  -- hack : instead of having bool case analysis just do natural number recursion and return 1/0

  -- this works
  {- iszero (n : nat) : nat = z -> 1 | _ -> 0 -}
  isz : ∀ {Γ} → Γ Source.|- (nat ->s nat)
  isz = lam (rec (var i0) (suc z) z)

  -- this works
  {- leq (m n : nat) : nat = m ≤ n -}
  leq : ∀ {Γ} → Γ Source.|- (nat ->s (nat ->s nat))
  leq = lam (rec (var i0) (lam (suc z)) (lam (rec (var i0) z (app (force (var (iS (iS (iS (iS i0)))))) (var i0)))))

  -- this works
  {- eq (m n : nat) : nat = m = n -}
  eq : ∀ {Γ} → Γ Source.|- (nat ->s (nat ->s nat))
  eq = lam (rec (var i0) (lam (app isz (var i0))) (lam (rec (var i0) z (app (force (var (iS (iS (iS (iS i0)))))) (var i0)))))

  -- this works
  {- len (l : list τ) : nat = [] -> z | x :: xs -> 1 + len xs -}
  len : ∀ {Γ τ} → Γ Source.|- (list τ ->s nat)
  len = lam (listrec (var i0) z (suc (force (var (iS (iS i0))))))

  -- this works
  {- nth (n : nat) (l : list τ) : nat = [] -> 1 (return 1+len(l) if element not in list) | x :: xs -> if n = x then 0 else 1 + (nth n xs) -}
  nth : ∀ {Γ} → Γ Source.|- (list nat ->s (nat ->s nat))
  nth = lam (lam (listrec (var (iS i0)) (suc z) (rec (app (app eq (var (iS (iS (iS i0))))) (var i0)) (suc (force (var (iS (iS i0))))) z)))

  -- this works
  {- append (l1 l2 : list τ) : list τ = match l1 with [] -> l2 | x :: xs -> x :: (append xs ys) -}
  append : ∀ {Γ τ} → Γ Source.|- (list τ ->s (list τ ->s list τ))
  append = lam (lam (listrec (var (iS i0)) (var i0) (var i0 ::s force (var (iS (iS i0))))))

  -- this works
  {- rev (l : list τ) : list τ = [] -> [] | x :: xs -> append (rev xs) [x] -}
  rev : ∀ {Γ τ} → Γ Source.|- (list τ ->s list τ)
  rev = lam (listrec (var i0) nil (app (app append (force (var (iS (iS i0))))) (var i0 ::s nil)))

{-
  {- fast rev -}
  rev2piles : ∀ {Γ τ} → Γ Source.|- (list τ ->s (list τ ->s list τ))
  rev2piles = lam (lam (listrec (var (iS i0)) (var i0) (app (app rev2piles (var (iS i0))) (var i0 ::s var (iS (iS (iS i0)))))))
  fastrev : ∀ {Γ τ} → Γ Source.|- (list τ ->s list τ)
  fastrev = lam (app (app rev2piles (var i0)) nil)
-}

  -- this works
  {- insert (l : list nat) (el : nat) : list nat = [] -> [el] | x :: xs -> (leq el x -> el :: x :: xs | x :: (insert el xs)) -}
  insert : ∀ {Γ} → Γ Source.|- (list nat ->s (nat ->s list nat))
  insert = lam (lam (listrec (var (iS i0)) (var i0 ::s nil)
             (rec (app (app leq (var (iS (iS (iS i0))))) (var i0)) (var i0 ::s force (var (iS (iS i0))))
               (var (iS (iS (iS (iS (iS i0))))) ::s (var (iS (iS i0)) ::s var (iS (iS (iS i0))))))))

  -- this works
  {- insertion sort (l : list nat) : list nat = [] -> [] | x :: xs -> insert x (isort xs) -}
  isort : ∀ {Γ} → Γ Source.|- (list nat ->s list nat)
  isort = lam (listrec (var i0) nil (app (app insert (force (var (iS (iS i0))))) (var i0)))

  -- this works
  {- map (l : list τ) (f : τ → τ') : list τ = [] -> [] | x :: xs -> f x :: map f xs -}
  map : ∀ {Γ τ τ'} → Γ Source.|- ((τ ->s τ') ->s (list τ ->s list τ'))
  map = lam (lam (listrec (var i0) nil (app (var (iS (iS (iS (iS i0))))) (var i0) ::s force (var (iS (iS i0))))))

  dbl-trans : ∀ {Γ τ} → {!!} --el ([ (⟨⟨ Γ ⟩⟩c) ]c ->p [ (|| τ ||) ]t)
  dbl-trans {Γ} = {!|| dbl ||e!}

  example1 : ∀ {Γ τ} → {!!}
  example1 {Γ} {τ} = {!!} --copy and paste from this goal to the thing below
{-
  dbl-trans : ∀ {Γ} → ⟨⟨ Γ ⟩⟩c Pilot2.|- || nat ->s nat ||
  dbl-trans = prod 0C
                                     (lam
                                      (prod
                                       (plusC (l-proj (prod 0C (var i0)))
                                        (l-proj
                                         (rec (r-proj (prod 0C (var i0)))
                                          (prod (plusC 1C (l-proj (prod 0C z))) (r-proj (prod 0C z)))
                                          (prod
                                           (plusC 1C
                                            (l-proj
                                             (prod
                                              (l-proj
                                               (prod
                                                (l-proj
                                                 (prod
                                                  (plusC (l-proj (prod 0C (var (iS i0))))
                                                   (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                  (r-proj (r-proj (prod 0C (var (iS i0)))))))
                                                (s
                                                 (r-proj
                                                  (prod
                                                   (plusC (l-proj (prod 0C (var (iS i0))))
                                                    (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                   (r-proj (r-proj (prod 0C (var (iS i0))))))))))
                                              (s
                                               (r-proj
                                                (prod
                                                 (l-proj
                                                  (prod
                                                   (plusC (l-proj (prod 0C (var (iS i0))))
                                                    (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                   (r-proj (r-proj (prod 0C (var (iS i0)))))))
                                                 (s
                                                  (r-proj
                                                   (prod
                                                    (plusC (l-proj (prod 0C (var (iS i0))))
                                                     (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                    (r-proj (r-proj (prod 0C (var (iS i0))))))))))))))
                                           (r-proj
                                            (prod
                                             (l-proj
                                              (prod
                                               (l-proj
                                                (prod
                                                 (plusC (l-proj (prod 0C (var (iS i0))))
                                                  (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                 (r-proj (r-proj (prod 0C (var (iS i0)))))))
                                               (s
                                                (r-proj
                                                 (prod
                                                  (plusC (l-proj (prod 0C (var (iS i0))))
                                                   (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                  (r-proj (r-proj (prod 0C (var (iS i0))))))))))
                                             (s
                                              (r-proj
                                               (prod
                                                (l-proj
                                                 (prod
                                                  (plusC (l-proj (prod 0C (var (iS i0))))
                                                   (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                  (r-proj (r-proj (prod 0C (var (iS i0)))))))
                                                (s
                                                 (r-proj
                                                  (prod
                                                   (plusC (l-proj (prod 0C (var (iS i0))))
                                                    (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                   (r-proj (r-proj (prod 0C (var (iS i0)))))))))))))))))
                                       (r-proj
                                        (rec (r-proj (prod 0C (var i0)))
                                         (prod (plusC 1C (l-proj (prod 0C z))) (r-proj (prod 0C z)))
                                         (prod
                                          (plusC 1C
                                           (l-proj
                                            (prod
                                             (l-proj
                                              (prod
                                               (l-proj
                                                (prod
                                                 (plusC (l-proj (prod 0C (var (iS i0))))
                                                  (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                 (r-proj (r-proj (prod 0C (var (iS i0)))))))
                                               (s
                                                (r-proj
                                                 (prod
                                                  (plusC (l-proj (prod 0C (var (iS i0))))
                                                   (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                  (r-proj (r-proj (prod 0C (var (iS i0))))))))))
                                             (s
                                              (r-proj
                                               (prod
                                                (l-proj
                                                 (prod
                                                  (plusC (l-proj (prod 0C (var (iS i0))))
                                                   (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                  (r-proj (r-proj (prod 0C (var (iS i0)))))))
                                                (s
                                                 (r-proj
                                                  (prod
                                                   (plusC (l-proj (prod 0C (var (iS i0))))
                                                    (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                   (r-proj (r-proj (prod 0C (var (iS i0))))))))))))))
                                          (r-proj
                                           (prod
                                            (l-proj
                                             (prod
                                              (l-proj
                                               (prod
                                                (plusC (l-proj (prod 0C (var (iS i0))))
                                                 (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                (r-proj (r-proj (prod 0C (var (iS i0)))))))
                                              (s
                                               (r-proj
                                                (prod
                                                 (plusC (l-proj (prod 0C (var (iS i0))))
                                                  (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                 (r-proj (r-proj (prod 0C (var (iS i0))))))))))
                                            (s
                                             (r-proj
                                              (prod
                                               (l-proj
                                                (prod
                                                 (plusC (l-proj (prod 0C (var (iS i0))))
                                                  (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                 (r-proj (r-proj (prod 0C (var (iS i0)))))))
                                               (s
                                                (r-proj
                                                 (prod
                                                  (plusC (l-proj (prod 0C (var (iS i0))))
                                                   (l-proj (r-proj (prod 0C (var (iS i0))))))
                                                  (r-proj (r-proj (prod 0C (var (iS i0))))))))))))))))))

  aaa : ∀ {Γ} → interpE (r-proj (dbl-trans {Γ})) == {!!}
  aaa = {!!}

  interp-dbl-trans : ∀ {Γ} → Monotone (fst [ ⟨⟨ Γ ⟩⟩c ]c) (fst [ ⟨⟨ nat ->s nat ⟩⟩ ]t) (snd [ ⟨⟨ Γ ⟩⟩c ]c) (snd [ ⟨⟨ nat ->s nat ⟩⟩ ]t)
  interp-dbl-trans {Γ} = monotone
                           (λ x →
                              monotone
                              (λ p₁ →
                                 (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) p₁))
                              (λ a b c →
                                 nat-trans
                                 (fst (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) a))
                                 (fst (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) b))
                                 (fst (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) b))
                                 (fst
                                  (♭h-fix-args (monotone (λ x₁ → 1 , 0) (λ x₁ y z₁ → <> , <>))
                                   (monotone
                                    (λ x₁ → S (fst (snd (fst x₁))) , S (S (snd (snd (fst x₁)))))
                                    (λ x₁ y z₁ → fst (snd (fst z₁)) , snd (snd (fst z₁))))
                                   ((x , a) , a) ((x , b) , b) c))
                                 (fst
                                  (♭h-fix-el (monotone (λ x₁ → 1 , 0) (λ x₁ y z₁ → <> , <>))
                                   (monotone
                                    (λ x₁ → S (fst (snd (fst x₁))) , S (S (snd (snd (fst x₁)))))
                                    (λ x₁ y z₁ → fst (snd (fst z₁)) , snd (snd (fst z₁))))
                                   ((x , a) , a) ((x , b) , b)
                                   ((Preorder-str.refl (snd [ ⟨⟨ Γ ⟩⟩c ]c) x , c) , c)))
                                 ,
                                 ♭nat-trans
                                 (snd (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) a))
                                 (snd (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) b))
                                 (snd (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) b))
                                 (snd
                                  (♭h-fix-args (monotone (λ x₁ → 1 , 0) (λ x₁ y z₁ → <> , <>))
                                   (monotone
                                    (λ x₁ → S (fst (snd (fst x₁))) , S (S (snd (snd (fst x₁)))))
                                    (λ x₁ y z₁ → fst (snd (fst z₁)) , snd (snd (fst z₁))))
                                   ((x , a) , a) ((x , b) , b) c))
                                 (snd
                                  (♭h-fix-el (monotone (λ x₁ → 1 , 0) (λ x₁ y z₁ → <> , <>))
                                   (monotone
                                    (λ x₁ → S (fst (snd (fst x₁))) , S (S (snd (snd (fst x₁)))))
                                    (λ x₁ y z₁ → fst (snd (fst z₁)) , snd (snd (fst z₁))))
                                   ((x , a) , a) ((x , b) , b)
                                   ((Preorder-str.refl (snd [ ⟨⟨ Γ ⟩⟩c ]c) x , c) , c)))))
                           (λ x y z₁ w →
                              nat-trans
                              (fst (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) w))
                              (fst (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) w))
                              (fst (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) w))
                              (fst
                               (♭h-fix-args (monotone (λ x₁ → 1 , 0) (λ x₁ y₁ z₂ → <> , <>))
                                (monotone
                                 (λ x₁ → S (fst (snd (fst x₁))) , S (S (snd (snd (fst x₁)))))
                                 (λ x₁ y₁ z₂ → fst (snd (fst z₂)) , snd (snd (fst z₂))))
                                ((x , w) , w) ((y , w) , w) (♭nat-refl w)))
                              (fst
                               (♭h-fix-el (monotone (λ x₁ → 1 , 0) (λ x₁ y₁ z₂ → <> , <>))
                                (monotone
                                 (λ x₁ → S (fst (snd (fst x₁))) , S (S (snd (snd (fst x₁)))))
                                 (λ x₁ y₁ z₂ → fst (snd (fst z₂)) , snd (snd (fst z₂))))
                                ((x , w) , w) ((y , w) , w) ((z₁ , ♭nat-refl w) , ♭nat-refl w)))
                              ,
                              ♭nat-trans
                              (snd (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) w))
                              (snd (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) w))
                              (snd (natrec (1 , 0) (λ n x₂ → S (fst x₂) , S (S (snd x₂))) w))
                              (snd
                               (♭h-fix-args (monotone (λ x₁ → 1 , 0) (λ x₁ y₁ z₂ → <> , <>))
                                (monotone
                                 (λ x₁ → S (fst (snd (fst x₁))) , S (S (snd (snd (fst x₁)))))
                                 (λ x₁ y₁ z₂ → fst (snd (fst z₂)) , snd (snd (fst z₂))))
                                ((x , w) , w) ((y , w) , w) (♭nat-refl w)))
                              (snd
                               (♭h-fix-el (monotone (λ x₁ → 1 , 0) (λ x₁ y₁ z₂ → <> , <>))
                                (monotone
                                 (λ x₁ → S (fst (snd (fst x₁))) , S (S (snd (snd (fst x₁)))))
                                 (λ x₁ y₁ z₂ → fst (snd (fst z₂)) , snd (snd (fst z₂))))
                                ((x , w) , w) ((y , w) , w) ((z₁ , ♭nat-refl w) , ♭nat-refl w))))
-}

{-
  {- halve (l : list nat) : (list nat * list nat) = splits a list in half -}
  halve : ∀ {Γ} → Γ Source.|- (list nat ->s (list nat ×s list nat))
  halve = lam (listrec (var i0)
            (prod nil nil)
            (listrec (var (iS i0))
              (prod (var i0 ::s nil) nil)
              (prod (var (iS (iS (iS i0))) ::s split (force (var (iS (iS i0)))) (var i0)) (var i0 ::s split (force (var (iS (iS i0)))) (var (iS i0))))))

  test : ∀ {Γ τ} → {!!}
  test {Γ} = {!s2r (app halve (z ::s (z ::s (z ::s nil))))!}

  {- merge (l1 l2 : list nat) : list nat =
       match l1 with
       [] -> l2
       x :: xs ->
         match l2 with
           [] -> x :: xs
           y :: ys ->
             x <= y -> x :: merge xs l2
             _ -> y :: merge l1 ys -}
  merge : ∀ {Γ} → Γ Source.|- ((list nat ×s list nat) ->s list nat)
  merge = lam (listrec (split (var i0) (var i0))
            (split (var i0) (var (iS i0)))
            (listrec (split (var (iS (iS (iS i0)))) (var (iS i0)))
              (split (var (iS (iS (iS i0)))) (var i0))
              (rec (app (app leq (var (iS (iS (iS i0))))) (var i0))
                (var (iS (iS (iS i0))) ::s force (var (iS (iS (iS (iS (iS i0)))))))
                (var i0 ::s app merge (prod (split (var (iS (iS (iS (iS (iS (iS (iS (iS i0))))))))) (var (iS i0))) (var (iS (iS (iS i0)))))))))

  {- mergesort (l : list nat) : list nat -}
  msort : ∀ {Γ} → Γ Source.|- (list nat ->s list nat)
  msort = lam (listrec (var i0)
            nil
            (listrec (var (iS i0))
              (var i0 ::s nil)
              (app merge (prod
                (app msort (split (app halve (var (iS (iS (iS (iS (iS (iS i0)))))))) (var i0)))
                (app msort (split (app halve (var (iS (iS (iS (iS (iS (iS i0)))))))) (var (iS i0))))))))
-}

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


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

open import HoTT

module homotopy.HopfJunior where

-- We define the negation function and prove that it’s an equivalence

not : Bool → Bool
not true = false
not false = true

not-not : (b : Bool) → not (not b) == b
not-not true = idp
not-not false = idp

not-equiv : Bool ≃ Bool
not-equiv = equiv not not not-not not-not

-- Definition of the junior Hopf fibration
module HopfJunior = S¹RecType Bool not-equiv
open HopfJunior using (module Wt; Wt; cct; ppt; flattening-S¹)

HopfJunior : S¹ → Type₀
HopfJunior = HopfJunior.f

-- We get that the total space is the type Wt defined in the flattening lemma.
tot-is-Wt : Σ S¹ HopfJunior == Wt
tot-is-Wt = flattening-S¹

-- Now we prove that Wt is equivalent to S¹

private
  -- Map from [Wt] to [S¹]
  to-cct : Unit × Bool → S¹
  to-cct _ = base

  to-ppt : (x : Unit × Bool) → to-cct x == to-cct x
  to-ppt (_ , true) = loop
  to-ppt (_ , false) = idp

  module To = Wt.Rec to-cct to-ppt

  to : Wt → S¹
  to = To.f

  -- Map from [S¹] to [Wt]
  from-base : Wt
  from-base = cct tt true

  from-loop : from-base == from-base
  from-loop = ppt tt true ∙ ppt tt false

  module From = S¹Rec from-base from-loop

  from : S¹ → Wt
  from = From.f

  -- First composite
  abstract
    to-from : (x : S¹) → to (from x) == x
    to-from = S¹-elim idp (↓-∘=idf-in to from
      (ap to (ap from loop)                       =⟨ From.loop-β |in-ctx ap to ⟩
      ap to (ppt tt true ∙ ppt tt false)         =⟨ ap-∙ to (ppt tt true) (ppt tt false) ⟩
      ap to (ppt tt true) ∙ ap to (ppt tt false) =⟨ To.pp-β (tt , true) |in-ctx (λ u → u ∙ ap to (ppt tt false)) ⟩
      loop ∙ ap to (ppt tt false)                =⟨ To.pp-β (tt , false) |in-ctx (λ u → loop ∙ u) ⟩
      loop ∙ idp                                 =⟨ ∙-unit-r loop ⟩
      loop ∎))

  -- Second composite
  from-to-cct : (b : Bool) → from (to (cct tt b)) == cct tt b
  from-to-cct true = idp
  from-to-cct false = ! (ppt tt false)

  abstract
    from-to-ppt : (b : Bool) → ap from (ap to (ppt tt b)) ∙' from-to-cct (not b) == from-to-cct b ∙ ppt tt b
    from-to-ppt true =
      ap from (ap to (ppt tt true)) ∙' ! (ppt tt false) =⟨ To.pp-β (tt , true) |in-ctx (λ u → ap from u ∙' ! (ppt tt false)) ⟩
      ap from loop ∙' ! (ppt tt false)                  =⟨ From.loop-β |in-ctx (λ u → u ∙' ! (ppt tt false)) ⟩
      (ppt tt true ∙ ppt tt false) ∙' ! (ppt tt false)  =⟨ lemma (ppt tt true) (ppt tt false) ⟩
      ppt tt true ∎  where
        lemma : ∀ {i} {A : Type i} {a b c : A} (p : a == b) (q : b == c) → (p ∙ q) ∙' (! q) == p
        lemma idp idp = idp
    from-to-ppt false =
      ap from (ap to (ppt tt false))                    =⟨ To.pp-β (tt , false) |in-ctx ap from ⟩
      ap from (idp {a = base})                          =⟨ ! (!-inv-l (ppt tt false)) ⟩
      ! (ppt tt false) ∙ ppt tt false ∎

    from-to : (x : Wt) → from (to x) == x
    from-to = Wt.elim (from-to-cct ∘ snd) (λ b → ↓-∘=idf-in from to (from-to-ppt (snd b)))

  -- Conclusion
  subresult : Wt ≃ S¹
  subresult = equiv to from to-from from-to

-- Conclusion
result : Σ S¹ HopfJunior ≃ S¹
result = subresult ∘e (coe-equiv tot-is-Wt)

ext: agda

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Andreas, Jesper, 2015-07-02 Error in copyScope

-- To trigger the bug, it is important that
-- the main module is in a subdirectory of the imported module.
module Issue1597.Main where

open import Issue1597   -- external import is needed

module B where
  open A public  -- public is needed

module C = B

postulate p : C.M.Nat

-- ERROR WAS: not in scope C.M.Nat

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists where at least one element satisfies a given property
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.Any {a} {A : Set a} where

open import Data.Empty
open import Data.Fin
open import Data.List.Base as List using (List; []; [_]; _∷_)
open import Data.Product as Prod using (∃; _,_)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Level using (_⊔_)
open import Relation.Nullary using (¬_; yes; no)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Unary hiding (_∈_)

------------------------------------------------------------------------
-- Any P xs means that at least one element in xs satisfies P.

data Any {p} (P : A → Set p) : List A → Set (a ⊔ p) where
  here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)

------------------------------------------------------------------------
-- Operations on Any

module _ {p} {P : A → Set p} {x xs} where

  head : ¬ Any P xs → Any P (x ∷ xs) → P x
  head ¬pxs (here px)   = px
  head ¬pxs (there pxs) = contradiction pxs ¬pxs

  tail : ¬ P x → Any P (x ∷ xs) → Any P xs
  tail ¬px (here  px)  = ⊥-elim (¬px px)
  tail ¬px (there pxs) = pxs

map : ∀ {p q} {P : A → Set p} {Q : A → Set q} → P ⊆ Q → Any P ⊆ Any Q
map g (here px)   = here (g px)
map g (there pxs) = there (map g pxs)

module _ {p} {P : A → Set p} where

  -- `index x∈xs` is the list position (zero-based) which `x∈xs` points to.
  index : ∀ {xs} → Any P xs → Fin (List.length xs)
  index (here  px)  = zero
  index (there pxs) = suc (index pxs)

  lookup : ∀ {xs} → Any P xs → A
  lookup {xs} p = List.lookup xs (index p)

  _∷=_ : ∀ {xs} → Any P xs → A → List A
  _∷=_ {xs} x∈xs v = xs List.[ index x∈xs ]∷= v

  infixl 4 _─_
  _─_ : ∀ xs → Any P xs → List A
  xs ─ x∈xs = xs List.─ index x∈xs

-- If any element satisfies P, then P is satisfied.
satisfied : ∀ {p} {P : A → Set p} {xs} → Any P xs → ∃ P
satisfied (here px) = _ , px
satisfied (there pxs) = satisfied pxs

module _ {p} {P : A → Set p} {x xs} where

  toSum : Any P (x ∷ xs) → P x ⊎ Any P xs
  toSum (here px)   = inj₁ px
  toSum (there pxs) = inj₂ pxs

  fromSum : P x ⊎ Any P xs → Any P (x ∷ xs)
  fromSum (inj₁ px)  = here px
  fromSum (inj₂ pxs) = there pxs

------------------------------------------------------------------------
-- Properties of predicates preserved by Any

module _ {p} {P : A → Set p} where

  any : Decidable P → Decidable (Any P)
  any P? []       = no λ()
  any P? (x ∷ xs) with P? x
  ... | yes px = yes (here px)
  ... | no ¬px = Dec.map′ there (tail ¬px) (any P? xs)

  satisfiable : Satisfiable P → Satisfiable (Any P)
  satisfiable (x , Px) = [ x ] , here Px


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.Posets where

-- The category of partially ordered sets and order-preserving maps.

open import Level
open import Relation.Binary using (Poset; IsEquivalence; _Preserves_⟶_)
open import Relation.Binary.OrderMorphism using (_⇒-Poset_; id; _∘_)

open import Categories.Category

open Poset renaming (_≈_ to ₍_₎_≈_; _≤_ to ₍_₎_≤_)
open _⇒-Poset_

module _ {a₁ a₂ a₃ b₁ b₂ b₃} {A : Poset a₁ a₂ a₃} {B : Poset b₁ b₂ b₃} where

  infix 4 _≗_

  -- Order morphisms preserve equality.

  fun-resp-≈ : (f : A ⇒-Poset B) → fun f Preserves ₍ A ₎_≈_ ⟶ ₍ B ₎_≈_
  fun-resp-≈ f x≈y = antisym B (monotone f (reflexive A x≈y))
                               (monotone f (reflexive A (Eq.sym A x≈y)))

  -- Pointwise equality (on order preserving maps).

  _≗_ : (f g : A ⇒-Poset B) → Set (a₁ ⊔ b₂)
  f ≗ g = ∀ {x} → ₍ B ₎ fun f x ≈ fun g x

  ≗-isEquivalence : IsEquivalence _≗_
  ≗-isEquivalence = record
    { refl    = Eq.refl B
    ; sym     = λ f≈g → Eq.sym B f≈g
    ; trans   = λ f≈g g≈h → Eq.trans B f≈g g≈h
    }

  module ≗ = IsEquivalence ≗-isEquivalence

-- The category of posets and order-preserving maps.

Posets : ∀ c ℓ₁ ℓ₂ → Category (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) (c ⊔ ℓ₂) (c ⊔ ℓ₁)
Posets c ℓ₁ ℓ₂ = record
  { Obj       = Poset c ℓ₁ ℓ₂
  ; _⇒_       = _⇒-Poset_
  ; _≈_       = _≗_
  ; id        = id
  ; _∘_       = _∘_
  ; assoc     = λ {_ _ _ D} → Eq.refl D
  ; sym-assoc = λ {_ _ _ D} → Eq.refl D
  ; identityˡ = λ {_ B} → Eq.refl B
  ; identityʳ = λ {_ B} → Eq.refl B
  ; identity² = λ {A} → Eq.refl A
  ; equiv     = ≗-isEquivalence
  ; ∘-resp-≈  = λ {_ _ C _ h} f≈h g≈i → Eq.trans C f≈h (fun-resp-≈ h g≈i)
  }
  where

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Automaton.NonDeterministic where

import      Lvl
open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Data.List using (List) renaming (∅ to ε ; _⊰_ to _·_)
open import Functional
open import Logic
open import Sets.ExtensionalPredicateSet
open import Structure.Setoid
open import Type

-- Non-deterministic Automata
-- `State`      (Q)  is the set of states.
-- `Alphabet`   (Σ)  is the set of symbols/the alphabet.
-- `transition` (δ)  is the transition function.
-- `start`      (q₀) is the start state.
-- `Final`      (F)  is the subset of State which are the final/accepting states.
record NonDeterministic {ℓₚ ℓₛ ℓₑ ℓₐ} (State : Type{ℓₛ}) ⦃ equiv-state : Equiv{ℓₑ}(State) ⦄ (Alphabet : Type{ℓₐ}) : Type{ℓₛ Lvl.⊔ ℓₑ Lvl.⊔ ℓₐ Lvl.⊔ Lvl.𝐒(ℓₚ)} where
  constructor nondeterministic
  field
    transition : State → Alphabet → PredSet{ℓₚ}(State)
    start      : State
    Final      : PredSet{ℓₚ}(State)

  Word = List(Alphabet)

  -- Chained transition using a word (list of characters).
  wordTransition : State → Word → PredSet{ℓₑ}(State)
  wordTransition initialState ε       = • initialState
  wordTransition initialState (a · l) = {!⋃ ?!} -- wordTransition (transition initialState a) l
{-
  module LetterNotation where
    Q  = State
    Σ  = Alphabet
    δ  = transition
    δ̂  = wordTransition
    q₀ = start
    F  = Final

  -- A word is accepted by the automaton when it can transition from the start state to a final state.
  AcceptsWord : Word → Stmt
  AcceptsWord = (_∈ Final) ∘ wordTransition start

  -- The subset of State which are the accessible states from the start state by chained transitions.
  Accessible : PredSet(State)
  Accessible = ⊶(wordTransition start)

  automatonTransition : Alphabet → NonDeterministic(State)(Alphabet)
  transition (automatonTransition _) = transition
  start      (automatonTransition c) = transition start c
  Final      (automatonTransition _) = Final

  automatonTransitionWord : Word → NonDeterministic(State)(Alphabet)
  transition (automatonTransitionWord _) = transition
  start      (automatonTransitionWord w) = wordTransition start w
  Final      (automatonTransitionWord _) = Final
-}

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 --without-K --safe #-}

module Categories.Category.Monoidal.Construction.Product where

-- The product A × B of (braided/symmetric) monoidal categories
-- A and B is again (braided/symmetric) monoidal.

open import Level using (_⊔_)
open import Data.Product using (_,_; dmap; zip; curry′; uncurry′)

open import Categories.Category using (Category)
open import Categories.Category.Product using (Product)
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Braided using (Braided)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
open import Categories.Functor using (Functor)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)

open Category using (Obj)

module _ {o o′ ℓ ℓ′ e e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
         (M : Monoidal C) (N : Monoidal D) where

  private
    module M  = Monoidal M
    module N  = Monoidal N
    module ⊗₁ = Functor M.⊗
    module ⊗₂ = Functor N.⊗

  ⊗ : Bifunctor (Product C D) (Product C D) (Product C D)
  ⊗ = record
    { F₀           = uncurry′ (zip (curry′ ⊗₁.₀) (curry′ ⊗₂.₀))
    ; F₁           = uncurry′ (zip (curry′ ⊗₁.₁) (curry′ ⊗₂.₁))
    ; identity     = ⊗₁.identity , ⊗₂.identity
    ; homomorphism = ⊗₁.homomorphism , ⊗₂.homomorphism
    ; F-resp-≈     = uncurry′ (zip (curry′ ⊗₁.F-resp-≈) (curry′ ⊗₂.F-resp-≈))
    }

  unit : Obj (Product C D)
  unit = M.unit , N.unit

  Product-Monoidal : Monoidal (Product C D)
  Product-Monoidal = record
    { ⊗        = ⊗
    ; unit     = unit
    ; unitorˡ  = record
      { from   = M.unitorˡ.from , N.unitorˡ.from
      ; to     = M.unitorˡ.to   , N.unitorˡ.to
      ; iso    = record
        { isoˡ = M.unitorˡ.isoˡ , N.unitorˡ.isoˡ
        ; isoʳ = M.unitorˡ.isoʳ , N.unitorˡ.isoʳ
        }
      }
    ; unitorʳ  = record
      { from   = M.unitorʳ.from , N.unitorʳ.from
      ; to     = M.unitorʳ.to   , N.unitorʳ.to
      ; iso    = record
        { isoˡ = M.unitorʳ.isoˡ , N.unitorʳ.isoˡ
        ; isoʳ = M.unitorʳ.isoʳ , N.unitorʳ.isoʳ
        }
      }
    ; associator = record
      { from     = M.associator.from , N.associator.from
      ; to       = M.associator.to   , N.associator.to
      ; iso      = record
        { isoˡ   = M.associator.isoˡ , N.associator.isoˡ
        ; isoʳ   = M.associator.isoʳ , N.associator.isoʳ
        }
      }
    ; unitorˡ-commute-from = M.unitorˡ-commute-from , N.unitorˡ-commute-from
    ; unitorˡ-commute-to   = M.unitorˡ-commute-to   , N.unitorˡ-commute-to
    ; unitorʳ-commute-from = M.unitorʳ-commute-from , N.unitorʳ-commute-from
    ; unitorʳ-commute-to   = M.unitorʳ-commute-to   , N.unitorʳ-commute-to
    ; assoc-commute-from   = M.assoc-commute-from   , N.assoc-commute-from
    ; assoc-commute-to     = M.assoc-commute-to     , N.assoc-commute-to
    ; triangle             = M.triangle             , N.triangle
    ; pentagon             = M.pentagon             , N.pentagon
    }

module _ {o o′ ℓ ℓ′ e e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
         {M : Monoidal C} {N : Monoidal D} where

  Product-Braided : Braided M → Braided N → Braided (Product-Monoidal M N)
  Product-Braided BM BN = record
    { braiding = niHelper (record
      { η       = λ{ ((W , X) , (Y , Z)) →
        BM.braiding.⇒.η (W , Y) , BN.braiding.⇒.η (X , Z) }
      ; η⁻¹     = λ{ ((W , X) , (Y , Z)) →
        BM.braiding.⇐.η (W , Y) , BN.braiding.⇐.η (X , Z) }
      ; commute = λ{ ((f , g) , (h , i)) →
        BM.braiding.⇒.commute (f , h) , BN.braiding.⇒.commute (g , i) }
      ; iso     = λ{ ((W , X) , (Y , Z)) → record
        { isoˡ = BM.braiding.iso.isoˡ (W , Y) , BN.braiding.iso.isoˡ (X , Z)
        ; isoʳ = BM.braiding.iso.isoʳ (W , Y) , BN.braiding.iso.isoʳ (X , Z)
        } }
      })
    ; hexagon₁ = BM.hexagon₁ , BN.hexagon₁
    ; hexagon₂ = BM.hexagon₂ , BN.hexagon₂
    }
    where
      module BM = Braided BM
      module BN = Braided BN

  Product-Symmetric : Symmetric M → Symmetric N → Symmetric (Product-Monoidal M N)
  Product-Symmetric SM SN = record
    { braided     = Product-Braided SM.braided SN.braided
    ; commutative = SM.commutative , SN.commutative
    }
    where
      module SM = Symmetric SM
      module SN = Symmetric SN

Product-MonoidalCategory : ∀ {o o′ ℓ ℓ′ e e′} →
                           MonoidalCategory o ℓ e → MonoidalCategory o′ ℓ′ e′ →
                           MonoidalCategory (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
Product-MonoidalCategory C D = record
  { U        = Product (C.U) (D.U)
  ; monoidal = Product-Monoidal (C.monoidal) (D.monoidal)
  }
  where
    module C = MonoidalCategory C
    module D = MonoidalCategory D

Product-BraidedMonoidalCategory : ∀ {o o′ ℓ ℓ′ e e′} →
  BraidedMonoidalCategory o ℓ e → BraidedMonoidalCategory o′ ℓ′ e′ →
  BraidedMonoidalCategory (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
Product-BraidedMonoidalCategory C D = record
  { U        = Product (C.U) (D.U)
  ; monoidal = Product-Monoidal (C.monoidal) (D.monoidal)
  ; braided  = Product-Braided (C.braided) (D.braided)
  }
  where
    module C = BraidedMonoidalCategory C
    module D = BraidedMonoidalCategory D

Product-SymmetricMonoidalCategory : ∀ {o o′ ℓ ℓ′ e e′} →
  SymmetricMonoidalCategory o ℓ e → SymmetricMonoidalCategory o′ ℓ′ e′ →
  SymmetricMonoidalCategory (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
Product-SymmetricMonoidalCategory C D = record
  { U         = Product (C.U) (D.U)
  ; monoidal  = Product-Monoidal (C.monoidal) (D.monoidal)
  ; symmetric = Product-Symmetric (C.symmetric) (D.symmetric)
  }
  where
    module C = SymmetricMonoidalCategory C
    module D = SymmetricMonoidalCategory D

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:
open import Data.Nat hiding (_^_ ; _+_)
open import Data.List as List hiding (null)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All as All
open import Data.List.All.Properties.Extra
open import Data.Integer
open import Data.Unit
open import Data.Empty
open import Data.Product hiding (map)
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning
open import Function
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Star hiding (return ; _>>=_ ; map)

module MJSF.Semantics (k : ℕ) where

open import MJSF.Syntax k
open import MJSF.Values k
open import MJSF.Monad k
open import ScopesFrames.ScopesFrames k Ty
open import Common.Weakening

-- This file contains the definitional interpreter for MJ using scopes
-- and frames, described in Section 5 of the paper.

module Semantics (g : Graph) where

  open SyntaxG g
  open ValuesG g
  open MonadG g
  open UsesVal Valᵗ valᵗ-weaken renaming (getFrame to getFrame') public

  -----------------
  -- AUXILIARIES --
  -----------------

  -- The interpreter relies on a number of auxiliary function.  We
  -- briefly summarize each.

  -- In Java (and MJ), each field member of an object is initialized
  -- to have a default value.  The `default` function defines a
  -- default value for each value type in MJ.

  default : {Σ : List Scope} → (t : VTy) → Val t Σ
  default int     = num (+ 0)
  default (ref s) = null
  default void    = void

  -- An alias for mapping `default` over a list of well-typed values:

  defaults : ∀ {fs : List Ty}{Σ} → All (#v (λ _ → ⊤)) fs → Slots fs Σ
  defaults fs = All.map (λ{ (#v' {t} _) → vᵗ (default t) }) fs

  -- `override` overrides methods in parent objects by overwriting
  -- method slots in super class frames by overriding child methods.
  --
  -- This notion of overriding does not straightforwardly scale to
  -- deal with `super`, but `super` is not a part of MJ.  See the
  -- paper or the MJ semantics in the appendix of this artifact for
  -- discussion and inspiration for how to represent class methods
  -- separately from object representations.

  override : ∀ {s Σ oms} →
             All (#m (λ ts t → (s ↦ (mᵗ ts t)) × Meth s ts t)) oms →
             M s (λ _ → ⊤) Σ
  override [] =
    return tt
  override (#m' (p , m) ∷ oms) =
    getFrame >>= λ f →
    setv p (mᵗ f m) >>= λ _ →
    override oms

  -- `init-obj` takes as input a class definition and a witness that
  -- the class has a finite inheritance chain.  The function is
  -- structurally recursive over the inheritance chain finity witness.
  --
  -- Each object is initialized by using the `initι` function, which
  -- allows us to refer to the "self" frame and store it in method
  -- definitions (i.e., the `fc` passed to the method value
  -- constructor `mᵗ` in `map-all` below).
  --
  -- Method slots are initialized using the method members in the
  -- class definition.  Field slots are initialized using `defaults`
  -- defined above.
  --
  -- After frame initialization, overrides are applied by using
  -- `override` defined above.
  --
  -- `init-obj` is assumed to be invoked in the context of the root
  -- frame, which all objects are linked to (because all scopes have
  -- an edge to the root scope).

  init-obj : ∀ {sʳ s s' Σ} → Class sʳ s → Inherits s s' → M sʳ (Frame s) Σ
  init-obj (class0 ms fs oms) (obj _)
    = getFrame >>= λ f →
      initι _ (λ fc → (All.map (λ{ (#m' m) → mᵗ fc m }) ms) ++-all (defaults fs)) (f ∷ []) >>= λ f' →
      (usingFrame f' (override oms) ^ f') >>= λ{ (_ , f') →
      return f' }
  init-obj (class0 ⦃ shape ⦄ _ _ _) (super ⦃ shape' ⦄ _)
    with (trans (sym shape) shape')
  ...  | () -- absurd case: the scope shapes of `class0` and `super` do not match
  init-obj (class1 p ⦃ shape ⦄ ms fs oms) (super ⦃ shape' ⦄ x)
    with (trans (sym shape) shape')
  ...  | refl =
    getv p >>= λ{ (cᵗ class' ic f') →
    (usingFrame f' (init-obj class' x) ^ f') >>= λ{ (f , f') →
    initι _ ⦃ shape ⦄ (λ fc → (All.map (λ{ (#m' m) → mᵗ fc m }) ms) ++-all (defaults fs)) (f' ∷ f ∷ []) >>= λ f'' →
    (usingFrame f'' (override oms) ^ f'') >>= λ{ (_ , f'') →
    return f'' }}}
  init-obj (class1 _ ⦃ shape ⦄ _ _ _) (obj _ ⦃ shape' ⦄)
    with (trans (sym shape) shape')
  ...  | () -- absurd case: the scope shapes of `class1` and `obj` do not match

  -------------------------
  -- EARLY RETURNS MONAD --
  -------------------------

  -- In order to deal with early returns, we define a specialized bind
  -- which stops evaluation and returns the yielded value.

  _>>=ᶜ_     :  ∀ {s s' s'' r Σ} →
               M s (λ Σ → Val r Σ ⊎ Frame s' Σ) Σ →
               (∀ {Σ'} → Frame s' Σ' → M s (λ Σ → Val r Σ ⊎ Frame s'' Σ) Σ') →
               M s (λ Σ → Val r Σ ⊎ Frame s'' Σ) Σ
  (m >>=ᶜ f) = m >>= λ{
      (inj₁ v) → return (inj₁ v) ;
      (inj₂ fr) → f fr
    }

  -- Continue is used to indicate that evaluation should continue.

  continue : ∀ {s r Σ} → M s (λ Σ → Val r Σ ⊎ Frame s Σ) Σ
  continue = fmap inj₂ getFrame

  mutual

    ---------------------------
    -- EXPRESSION EVALUATION --
    ---------------------------

    eval    :  ℕ → ∀ {t s Σ} → Expr s t → M s (Val t) Σ
    eval zero _ =
      timeoutᴹ
    eval (suc k) (upcast σ e) =
      eval k e >>= λ v →
      return (upcastRef σ v)
    eval (suc k) (num x) =
      return (num x)
    eval (suc k) (iop x l r) =
      eval k l >>= λ{ (num il) →
      eval k r >>= λ{ (num ir) →
      return (num (il + ir)) }}
    eval (suc k) null =
      return null
    eval (suc k) (var x) =
      getv x >>= λ{ (vᵗ v) →
      return v }
    eval (suc k) (new x) =
      getv x >>= λ{ (cᵗ class ic f) →
      usingFrame f (init-obj class ic) >>= λ{ f' →
      return (ref [] f') }}
    eval (suc k) (get e p) =
      eval k e >>= λ{
        null → raise ;
        (ref p' f) →
          usingFrame f (getv (prepend p' p)) >>= λ{ (vᵗ v) →
          return v }}
    eval (suc k) (call e p args) =
      eval k e >>= λ {
        null → raise ;
        (ref p' f) →
          usingFrame f (getv (prepend p' p)) >>= λ{ (mᵗ f' (meth s b)) →  -- f' is the "self"
          (eval-args k args ^ f') >>= λ{ (slots , f') →
          init s slots (f' ∷ []) >>= λ f'' →  -- f' is the static link of the method call frame
          usingFrame f'' (eval-body k b) }}}
    eval (suc k) (this p e) =
      getf p >>= λ f →
      usingFrame f (getl e) >>= λ f' →
      return (ref [] f')

    eval-args : ℕ → ∀ {s ts Σ} → All (Expr s) ts → M s (Slots (List.map vᵗ ts)) Σ
    eval-args zero _ = timeoutᴹ
    eval-args (suc k) [] = return []
    eval-args (suc k) (e ∷ es) =
      eval k e >>= λ v →
      (eval-args k es ^ v) >>= λ{ (slots , v) →
      return (vᵗ v ∷ slots) }

    --------------------------
    -- STATEMENT EVALUATION --
    --------------------------

    -- The following functions use the early returns monadic bind and
    -- `continue` operation defined above.

    eval-stmt : ℕ → ∀ {s s' r Σ} → Stmt s r s' → M s (λ Σ → Val r Σ ⊎ Frame s' Σ) Σ
    eval-stmt zero _ = timeoutᴹ
    eval-stmt (suc k) (run e) =
      eval k e >>= λ _ →
      continue
    eval-stmt (suc k) (ifz c t e) =
      eval k c >>= λ{
        (num (+ zero)) → eval-stmt k t
      ; (num i) → eval-stmt k e }
    eval-stmt (suc k) (set e p e') =
      eval k e >>= λ{
        null → raise ;
        (ref p' f) →
          (eval k e' ^ f) >>= λ{ (v , f) →
          usingFrame f (setv (prepend p' p) (vᵗ v)) >>= λ _ → continue }}
    eval-stmt (suc k) (loc s t) =
      getFrame >>= λ f →
      fmap inj₂ (init s (vᵗ (default t) ∷ []) (f ∷ [])) -- initializes a new local variable frame
    eval-stmt (suc k) (asgn x e) =
      eval k e >>= λ{ v →
      setv x (vᵗ v) >>= λ _ →
      continue }
    eval-stmt (suc k) (block stmts) =
      eval-stmts k stmts >>= λ{ _ →
      continue }
    eval-stmt (suc k) (ret e) =
      eval k e >>= λ{ v →
      return (inj₁ v) }

    eval-stmts : ℕ → ∀ {s r s' Σ} → Stmts s r s' → M s (λ Σ → Val r Σ ⊎ Frame s' Σ) Σ
    eval-stmts zero _ =
      timeoutᴹ
    eval-stmts (suc k) ε =
      continue
    eval-stmts (suc k) (stmt ◅ stmts) =
      eval-stmt k stmt >>=ᶜ λ f' →
      usingFrame f' (eval-stmts k stmts)

    ---------------------
    -- BODY EVALUATION --
    ---------------------

    -- Defined in terms of statement evaluation; handles early returns:

    eval-body : ℕ → ∀ {s t Σ} → Body s t → M s (Val t) Σ
    eval-body zero _ =
      timeoutᴹ
    eval-body (suc k) (body stmts e) =
      eval-stmts k stmts >>= λ{
        (inj₁ v)  → return v
      ; (inj₂ fr) → usingFrame fr (eval k e) }
    eval-body (suc k) (body-void stmts) =
      eval-stmts k stmts >>= λ _ →
      return void

  ------------------------
  -- PROGRAM EVALUATION --
  ------------------------

  -- Program evaluation first initializes the root frame to store all
  -- class definitions, and subsequently evaluates the program main
  -- function in the context of this root scope.
  --
  -- We use `initι` to initialize the root frame since class
  -- definition values (`cᵗ`) store a pointer to the root frame, i.e.,
  -- slots in the root frame are self-referential.

  eval-program : ℕ → ∀ {sʳ t} → Program sʳ t → Res (∃ λ Σ' → (Heap Σ' × Val t Σ'))
  eval-program k (program _ cs b) =
    let (f₀ , h₀) = initFrameι _ (λ f → All.map (λ{ (#c' (c , _ , ic)) → cᵗ c ic f }) cs) [] []
    in case (eval-body k b f₀ h₀) of λ{
         (ok (Σ' , h' , v , _)) → ok (Σ' , h' , v)
       ; timeout → timeout
       ; nullpointer → nullpointer }

  -- For the purpose of running the interpreter on test programs, we
  -- introduce some short-hand notation:

  -- The program will terminate succesfully in a state where p holds
  _⇓⟨_⟩_ : ∀ {sʳ a} → Program sʳ a → ℕ → (p : ∀ {Σ} → Val a Σ → Set) → Set
  p ⇓⟨ k ⟩ P with eval-program k p
  ... | nullpointer = ⊥
  ... | timeout = ⊥
  ... | ok (_ , _ , v) = P v

  -- The program will raise an exception in a state where p holds
  _⇓⟨_⟩!_ : ∀ {sʳ a} → Program sʳ a → ℕ → (p : ∀ {Σ} → Val a Σ → Set) → Set
  p ⇓⟨ k ⟩! P with eval-program k p
  ... | nullpointer = ⊤
  ... | timeout = ⊥
  ... | ok (_ , _ , v) = ⊥


text:
------------------------------------------------------------------------
-- A terminating parser data type and the accompanying interpreter
------------------------------------------------------------------------

module RecursiveDescent.Coinductive.Internal where

open import RecursiveDescent.Index
open import Data.Bool
open import Data.Product.Record
open import Data.Maybe
open import Data.BoundedVec.Inefficient
import Data.List as L
open import Data.Nat
open import Category.Applicative.Indexed
open import Category.Monad.Indexed
open import Category.Monad.State
open import Utilities

------------------------------------------------------------------------
-- Parser data type

-- A type for parsers which can be implemented using recursive
-- descent. The types used ensure that the implementation below is
-- structurally recursive.

codata Parser (tok : Set) : ParserType₁ where
  symbol :  Parser tok (false , leaf) tok
  ret    :  forall {r} -> r -> Parser tok (true , leaf) r
  fail   :  forall {r} -> Parser tok (false , leaf) r
  bind₀  :  forall {c₁ e₂ c₂ r₁ r₂}
         -> Parser tok (true , c₁) r₁
         -> (r₁ -> Parser tok (e₂ , c₂) r₂)
         -> Parser tok (e₂ , node c₁ c₂) r₂
  bind₁  :  forall {c₁ r₁ r₂} {i₂ : r₁ -> Index}
         -> Parser tok (false , c₁) r₁
         -> ((x : r₁) -> Parser tok (i₂ x) r₂)
         -> Parser tok (false , step c₁) r₂
  alt₀   :  forall {c₁ e₂ c₂ r}
         -> Parser tok (true , c₁)         r
         -> Parser tok (e₂   , c₂)         r
         -> Parser tok (true , node c₁ c₂) r
  alt₁   :  forall {c₁} e₂ {c₂ r}
         -> Parser tok (false , c₁)         r
         -> Parser tok (e₂    , c₂)         r
         -> Parser tok (e₂    , node c₁ c₂) r

------------------------------------------------------------------------
-- Run function for the parsers

-- Parser monad.

P : Set -> IFun ℕ
P tok = IStateT (BoundedVec tok) L.List

PIMonadPlus : (tok : Set) -> RawIMonadPlus (P tok)
PIMonadPlus tok = StateTIMonadPlus (BoundedVec tok) L.monadPlus

PIMonadState : (tok : Set) -> RawIMonadState (BoundedVec tok) (P tok)
PIMonadState tok = StateTIMonadState (BoundedVec tok) L.monad

private
  open module LM {tok} = RawIMonadPlus  (PIMonadPlus  tok)
  open module SM {tok} = RawIMonadState (PIMonadState tok)
                           using (get; put; modify)

-- For every successful parse the run function returns the remaining
-- string. (Since there can be several successful parses a list of
-- strings is returned.)

-- This function is structurally recursive with respect to the
-- following lexicographic measure:
--
-- 1) The upper bound of the length of the input string.
-- 2) The parser's proper left corner tree.

mutual

  parse : forall n {tok e c r} ->
          Parser tok (e , c) r ->
          P tok n (if e then n else pred n) r
  parse zero    symbol             = ∅
  parse (suc n) symbol             = eat =<< get
  parse n       (ret x)            = return x
  parse n       fail               = ∅
  parse n       (bind₀      p₁ p₂) = parse  n      p₁ >>= parse  n ∘′ p₂
  parse zero    (bind₁      p₁ p₂) = ∅
  parse (suc n) (bind₁      p₁ p₂) = parse (suc n) p₁ >>= parse↑ n ∘′ p₂
  parse n       (alt₀       p₁ p₂) = parse  n      p₁ ∣   parse↑ n    p₂
  parse n       (alt₁ true  p₁ p₂) = parse↑ n      p₁ ∣   parse  n    p₂
  parse n       (alt₁ false p₁ p₂) = parse  n      p₁ ∣   parse  n    p₂

  parse↑ : forall n {e tok c r} -> Parser tok (e , c) r -> P tok n n r
  parse↑ n       {true}  p = parse n p
  parse↑ zero    {false} p = ∅
  parse↑ (suc n) {false} p = parse (suc n) p >>= \r ->
                             modify ↑ >>
                             return r

  eat : forall {tok n} -> BoundedVec tok (suc n) -> P tok (suc n) n tok
  eat []      = ∅
  eat (c ∷ s) = put s >> return c

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- Exploit by Jesper Cockx

open import Agda.Builtin.Equality

data Bool : Set where
  tt ff : Bool

const : Bool → (Bool → Bool)
const = λ x _ → x

mutual
  Bool→cBool : Set
  Bool→cBool = _

  const-tt : Bool→cBool
  const-tt = const tt

constant : (f : Bool→cBool) (x y : Bool) → f x ≡ f y
constant f x y = refl

constant' : (f : Bool → Bool) (x y : Bool) → f x ≡ f y
constant' = constant

swap : Bool → Bool
swap tt = ff
swap ff = tt

fireworks : tt ≡ ff
fireworks = constant' swap ff tt


text:
{- 2010-09-28 Andreas, example from Alan Jeffery, see Issue 336 -}

module WhyWeNeedTypedLambda where

data Bool : Set where
  true false : Bool

F : Bool -> Set
F true  = Bool -> Bool
F false = Bool

bool : {b : Bool} -> F b -> Bool
bool {b} _ = b

{-
-- untyped lambda leaves some yellow
-- the problem  \ x -> x : F ?b  is postponed
bla : Bool
bla = bool (\ x -> x)
-}

-- typed lambda succeeds
-- \ (x : _) -> x infers as ?X -> ?X, yielding constraint F ?b = ?X -> ?X
bla' : Bool
bla' = bool (\ (x : _) -> x)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
-- Andreas, 2019-12-03, issue #4200 reported and testcase by nad

open import Agda.Builtin.Bool

data D : Set where
  c₁ : D
  @0 c₂ : D  -- Not allowed

d : D
d = c₂

f : D → Bool
f c₁ = true
f c₂ = false

-- Expected error:

-- Erased constructors are not supported
-- when checking the constructor c₂ in the declaration of D


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
-- the module `Relation.Binary.Construct.Converse` this module flips
-- both the relation and the underlying equality.
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Construct.Flip where

open import Function
open import Data.Product

------------------------------------------------------------------------
-- Properties

module _ {a ℓ} {A : Set a} (∼ : Rel A ℓ) where

  reflexive : Reflexive ∼ → Reflexive (flip ∼)
  reflexive refl = refl

  symmetric : Symmetric ∼ → Symmetric (flip ∼)
  symmetric sym = sym

  transitive : Transitive ∼ → Transitive (flip ∼)
  transitive trans = flip trans

  asymmetric : Asymmetric ∼ → Asymmetric (flip ∼)
  asymmetric asym = asym

  total : Total ∼ → Total (flip ∼)
  total total x y = total y x

  respects : ∀ {p} (P : A → Set p) → Symmetric ∼ →
             P Respects ∼ → P Respects flip ∼
  respects _ sym resp ∼ = resp (sym ∼)

  max : ∀ {⊥} → Minimum ∼ ⊥ → Maximum (flip ∼) ⊥
  max min = min

  min : ∀ {⊤} → Maximum ∼ ⊤ → Minimum (flip ∼) ⊤
  min max = max

module _ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
         (≈ : REL A B ℓ₁) (∼ : REL A B ℓ₂) where

  implies : ≈ ⇒ ∼ → flip ≈ ⇒ flip ∼
  implies impl = impl

  irreflexive : Irreflexive ≈ ∼ → Irreflexive (flip ≈) (flip ∼)
  irreflexive irrefl = irrefl

module _ {a ℓ₁ ℓ₂} {A : Set a} (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) where

  antisymmetric : Antisymmetric ≈ ∼ → Antisymmetric (flip ≈) (flip ∼)
  antisymmetric antisym = antisym

  trichotomous : Trichotomous ≈ ∼ → Trichotomous (flip ≈) (flip ∼)
  trichotomous compare x y = compare y x

module _ {a ℓ₁ ℓ₂} {A : Set a} (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) where

  respects₂ : Symmetric ∼₂ → ∼₁ Respects₂ ∼₂ → flip ∼₁ Respects₂ flip ∼₂
  respects₂ sym (resp₁ , resp₂) = (resp₂ ∘ sym , resp₁ ∘ sym)

module _ {a b ℓ} {A : Set a} {B : Set b} (∼ : REL A B ℓ) where

  decidable : Decidable ∼ → Decidable (flip ∼)
  decidable dec x y = dec y x

module _ {a ℓ} {A : Set a} {≈ : Rel A ℓ} where

  isEquivalence : IsEquivalence ≈ → IsEquivalence (flip ≈)
  isEquivalence eq = record
    { refl  = reflexive  ≈ Eq.refl
    ; sym   = symmetric  ≈ Eq.sym
    ; trans = transitive ≈ Eq.trans
    }
    where module Eq = IsEquivalence eq

  isDecEquivalence : IsDecEquivalence ≈ → IsDecEquivalence (flip ≈)
  isDecEquivalence dec = record
    { isEquivalence = isEquivalence Dec.isEquivalence
    ; _≟_           = decidable ≈ Dec._≟_
    }
    where module Dec = IsDecEquivalence dec

------------------------------------------------------------------------
-- Structures

module _ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} where

  isPreorder : IsPreorder ≈ ∼ → IsPreorder (flip ≈) (flip ∼)
  isPreorder O = record
    { isEquivalence = isEquivalence O.isEquivalence
    ; reflexive     = implies ≈ ∼ O.reflexive
    ; trans         = transitive ∼ O.trans
    }
    where module O = IsPreorder O

  isPartialOrder : IsPartialOrder ≈ ∼ → IsPartialOrder (flip ≈) (flip ∼)
  isPartialOrder O = record
    { isPreorder = isPreorder O.isPreorder
    ; antisym    = antisymmetric ≈ ∼ O.antisym
    }
    where module O = IsPartialOrder O

  isTotalOrder : IsTotalOrder ≈ ∼ → IsTotalOrder (flip ≈) (flip ∼)
  isTotalOrder O = record
    { isPartialOrder = isPartialOrder O.isPartialOrder
    ; total          = total ∼ O.total
    }
    where module O = IsTotalOrder O

  isDecTotalOrder : IsDecTotalOrder ≈ ∼ → IsDecTotalOrder (flip ≈) (flip ∼)
  isDecTotalOrder O = record
    { isTotalOrder = isTotalOrder O.isTotalOrder
    ; _≟_          = decidable ≈ O._≟_
    ; _≤?_         = decidable ∼ O._≤?_
    }
    where module O = IsDecTotalOrder O

  isStrictPartialOrder : IsStrictPartialOrder ≈ ∼ →
                         IsStrictPartialOrder (flip ≈) (flip ∼)
  isStrictPartialOrder O = record
    { isEquivalence = isEquivalence O.isEquivalence
    ; irrefl        = irreflexive ≈ ∼ O.irrefl
    ; trans         = transitive ∼ O.trans
    ; <-resp-≈      = respects₂ ∼ ≈ O.Eq.sym O.<-resp-≈
    }
    where module O = IsStrictPartialOrder O

  isStrictTotalOrder : IsStrictTotalOrder ≈ ∼ →
                       IsStrictTotalOrder (flip ≈) (flip ∼)
  isStrictTotalOrder O = record
    { isEquivalence = isEquivalence O.isEquivalence
    ; trans         = transitive ∼ O.trans
    ; compare       = trichotomous ≈ ∼ O.compare
    } where module O = IsStrictTotalOrder O

module _ {a ℓ} where

  setoid : Setoid a ℓ → Setoid a ℓ
  setoid S = record
    { _≈_           = flip S._≈_
    ; isEquivalence = isEquivalence S.isEquivalence
    }
    where module S = Setoid S

  decSetoid : DecSetoid a ℓ → DecSetoid a ℓ
  decSetoid S = record
    { _≈_              = flip S._≈_
    ; isDecEquivalence = isDecEquivalence S.isDecEquivalence
    }
    where module S = DecSetoid S

module _ {a ℓ₁ ℓ₂} where

  preorder : Preorder a ℓ₁ ℓ₂ → Preorder a ℓ₁ ℓ₂
  preorder O = record
    { isPreorder = isPreorder O.isPreorder
    }
    where module O = Preorder O

  poset : Poset a ℓ₁ ℓ₂ → Poset a ℓ₁ ℓ₂
  poset O = record
    { isPartialOrder = isPartialOrder O.isPartialOrder
    }
    where module O = Poset O

  totalOrder : TotalOrder a ℓ₁ ℓ₂ → TotalOrder a ℓ₁ ℓ₂
  totalOrder O = record
    { isTotalOrder = isTotalOrder O.isTotalOrder
    }
    where module O = TotalOrder O

  decTotalOrder : DecTotalOrder a ℓ₁ ℓ₂ → DecTotalOrder a ℓ₁ ℓ₂
  decTotalOrder O = record
    { isDecTotalOrder = isDecTotalOrder O.isDecTotalOrder
    }
    where module O = DecTotalOrder O

  strictPartialOrder : StrictPartialOrder a ℓ₁ ℓ₂ →
                       StrictPartialOrder a ℓ₁ ℓ₂
  strictPartialOrder O = record
    { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
    }
    where module O = StrictPartialOrder O

  strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂ →
                     StrictTotalOrder a ℓ₁ ℓ₂
  strictTotalOrder O = record
    { isStrictTotalOrder = isStrictTotalOrder O.isStrictTotalOrder
    }
    where module O = StrictTotalOrder O


text:
module Issue148 where

data I : Set where
  i : I

F : I → Set → Set
F i A = A

data T (p : I) : Set where
  t₁ :      T p  → T p
  t₂ : F p (T p) → T p

fold : ((x : T i) → T i) → T i → T i
fold f (t₁ x) = f (fold f x)
fold f (t₂ x) = f (fold f x)

data E : T i → Set where
  e : ∀ x → E x

postulate
  t₂′ : ∀ {p} → F p (T p) → T p

foo : (x : T i) → E (fold t₂ x)
foo x with x
foo x | x′ = e (fold t₂ x′)


text:
module Named where

open import Data.String
open import Data.Nat hiding (_≟_)
open import Data.Bool using (T; not)
open import Data.Product
open import Data.Sum
-- open import Data.Nat.Properties using (strictTotalOrder)
-- open import Relation.Binary using (StrictTotalOrder)
-- open import Relation.Binary.Core
open import Function using (id)
open import Function.Equivalence using (_⇔_; equivalence)

open import Relation.Nullary
open import Relation.Unary
open import Relation.Nullary.Negation
open import Data.Unit using (⊤)
open import Function using (_∘_)
-- open import Level renaming (zero to Lzero)
open import Relation.Binary.PropositionalEquality
-- open ≡-Reasoning

-- open ≡-Reasoning
--     renaming (begin_ to beginEq_; _≡⟨_⟩_ to _≡Eq⟨_⟩_; _∎ to _∎Eq)

open import Data.Collection
open import Data.Collection.Properties
open import Data.Collection.Equivalence
open import Data.Collection.Inclusion

open import Relation.Binary.PartialOrderReasoning ⊆-Poset

Variable = String

data PreTerm : Set where
    Var : (w : Variable) → PreTerm
    App : (P : PreTerm) → (Q : PreTerm) → PreTerm
    Abs : (w : Variable) → (Q : PreTerm) → PreTerm

showPreTerm : PreTerm → String
showPreTerm (Var x)   = x
showPreTerm (App P Q) = "(" ++ showPreTerm P ++ " " ++ showPreTerm Q ++ ")"
showPreTerm (Abs x M) = "(λ" ++ x ++ "." ++ showPreTerm M ++ ")"

I : PreTerm
I = Abs "x" (Var "x")

S : PreTerm
S = Abs "x" (App (Var "y") (Var "x"))

FV : PreTerm → Collection
FV (Var x  ) = singleton x
FV (App f x) = union (FV f) (FV x)
FV (Abs x m) = delete x (FV m)

-- a = singleton "x" ∋ (elem "x" ∪ elem "y")

-- b = C[ singleton "x" ] ∩ C[ singleton "x" ]

-- M = FV S

-- neither∈ : ∀ {x A B} → x ∉ C[ A union B ] →

_[_≔_] : PreTerm → Variable → PreTerm → PreTerm
Var x [ v ≔ N ] with x ≟ v
Var x [ v ≔ N ] | yes p = N
Var x [ v ≔ N ] | no ¬p = Var x
App P Q [ v ≔ N ] = App (P [ v ≔ N ]) (Q [ v ≔ N ])
Abs x P [ v ≔ N ] with x ≟ v
Abs x P [ v ≔ N ] | yes p = Abs v P
Abs x P [ v ≔ N ] | no ¬p = Abs x (P [ v ≔ N ])

-- If v ∉ FV(M) then M[v≔N] is defined and M[v≔N] ≡ M
lem-1-2-5-a : ∀ M N v → v ∉ c[ FV M ] → M [ v ≔ N ] ≡ M
lem-1-2-5-a (Var x) N v v∉M with x ≟ v
lem-1-2-5-a (Var x) N .x v∉M | yes refl = contradiction here v∉M
lem-1-2-5-a (Var x) N v v∉M | no ¬p = refl
lem-1-2-5-a (App P Q) N v v∉M = cong₂
    App
        (lem-1-2-5-a P N v (not-in-left-union (FV P) (FV Q) v∉M))
        (lem-1-2-5-a Q N v (not-in-right-union (FV P) (FV Q) v∉M))
lem-1-2-5-a (Abs x M) N v v∉M with x ≟ v
lem-1-2-5-a (Abs x M) N v v∉M | yes p = cong (λ z → Abs z M) (sym p)
lem-1-2-5-a (Abs x M) N v v∉M | no ¬p = cong (Abs x) (lem-1-2-5-a M N v (still-∉-after-recovered x (FV M) ¬p v∉M))

-- begin
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ∎
-- begin
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- ∎

-- If M[v≔N] is defined, v ≠ x and x ∈ FV(M) iff x ∈ FV(M[v≔N])
lem-1-2-5-b-i : ∀ {v N} M → c[ FV M ] ≋[ _≢_ v ] c[ FV (M [ v ≔ N ]) ]
lem-1-2-5-b-i {v} {N} M v≢x = equivalence (to M v≢x) (from M v≢x)
    where
            to : ∀ {v N} M → c[ FV M ] ⊆[ _≢_ v ] c[ FV (M [ v ≔ N ]) ]
            to {v} (Var w) v≢x ∈FV-M with w ≟ v
            to (Var w) v≢x ∈FV-M | yes p = contradiction (sym (trans (nach singleton-≡ ∈FV-M) p)) v≢x
            to (Var w) v≢x ∈FV-M | no ¬p = ∈FV-M
            to {v} {N} (App P Q) v≢x = begin
                    c[ union (FV P) (FV Q) ]
                ≤⟨ union-monotone {!   !} {!   !} {!   !} ⟩
                    {!   !}
                ≤⟨ {!   !} ⟩
                    {!   !}
                ≤⟨ {!   !} ⟩
                    {!   !}
                ≤⟨ {!   !} ⟩
                    {!   !}
                ≤⟨ {!    !} ⟩
                    c[ union (FV (P [ v ≔ N ])) (FV (Q [ v ≔ N ])) ]
                ∎
            to (Abs w M) v≢x ∈FV-M = {!    !}
            -- to (Var w) ∈FV-M with w ≟ v
            -- to (Var w) ∈FV-M | yes p = contradiction (sym (trans (nach singleton-≡ ∈FV-M) p)) v≢x
            -- to (Var w) ∈FV-M | no ¬p = ∈FV-M
            -- to (App P Q) = begin
            --         c[ union (FV P) (FV Q) ]
            --     ≤⟨ union-monotone {!   !} {!   !} {!   !} ⟩
            --         {!   !}
            --     ≤⟨ {!   !} ⟩
            --         {!   !}
            --     ≤⟨ {!   !} ⟩
            --         c[ union (FV (P [ v ≔ N ])) (FV (Q [ v ≔ N ])) ]
            --     ∎
            -- to (Abs w M) ∈FV-M = {!   !}

            from : ∀ {v N} M → c[ FV (M [ v ≔ N ]) ] ⊆[ _≢_ v ] c[ FV M ]
            from M = {!    !}
-- lem-1-2-5-b-i : ∀ {x v N} M → v ≢ x → x ∈ c[ FV M ] ⇔ x ∈ c[ FV (M [ v ≔ N ]) ]
-- lem-1-2-5-b-i {x} {v} {N} (Var w) v≢x with w ≟ v -- x ≡ w
-- lem-1-2-5-b-i {x} {v} {N} (Var w) v≢x | yes p =
--     equivalence
--         (λ ∈[w] → contradiction (sym (trans (nach singleton-≡ ∈[w]) p)) v≢x)
--         from
--     where   to : x ∈ c[ w ∷ [] ] → x ∈ c[ FV N ]
--             to ∈[w] = {!   !}
--             from : x ∈ c[ FV N ] → x ∈ c[ w ∷ [] ] -- x ∈ c[ FV (N [ v ≔ N ]) ]
--             from ∈FV-N = {!   !}
-- lem-1-2-5-b-i {x} {v} {N} (Var w) v≢x | no ¬p = equivalence id id
-- lem-1-2-5-b-i {x} {v} {N} (App P Q) v≢x = equivalence to {!   !}
--     where   to : c[ union (FV P) (FV Q) ] ⊆ c[ union (FV (P [ v ≔ N ])) (FV (Q [ v ≔ N ])) ]
--             to = map-⊆-union {FV P} {FV Q} {FV (P [ v ≔ N ])} {FV (Q [ v ≔ N ])} (_≢_ v) {!   !} {!   !} {!   !}
--
--
-- lem-1-2-5-b-i (Abs w M) v≢x = {!   !}

-- lem-1-2-5-b-i : ∀ {x v N} M → v ≢ x → (x ∈ FV M) ⇔ (x ∈ FV (M [ v ≔ N ]))
-- lem-1-2-5-b-i : ∀ {x v N} M → v ≢ x → (x ∈ FV M) ≡ (x ∈ FV (M [ v ≔ N ]))
-- lem-1-2-5-b-i : ∀ {x v N} M → v ≢ x → (x ∈ c[ FV M ]) ≡ (x ∈ c[ FV (M [ v ≔ N ]) ])
-- lem-1-2-5-b-i {v = v} (Var w) v≢x with w ≟ v
-- lem-1-2-5-b-i (Var v) v≢x | yes refl = {!   !}
-- lem-1-2-5-b-i {x} (Var w) v≢x | no ¬p = refl -- cong (_∈_ x) refl
-- lem-1-2-5-b-i {x} {v} {N} (App P Q) v≢x =
--     begin
--         x ∈ c[ union (FV P) (FV Q) ]
--     ≡⟨ sym {! ∪-union  !} ⟩
--         {!   !}
--     ≡⟨ {!   !} ⟩
--         {!   !}
--     ≡⟨ {!   !} ⟩
--         {!   !}
--     ≡⟨ {!   !} ⟩
--         {!   !}
--     ≡⟨ {!   !} ⟩
--         x ∈ c[ union (FV (P [ v ≔ N ])) (FV (Q [ v ≔ N ])) ]
--     ∎
-- lem-1-2-5-b-i (Abs w P) v≢x = {!    !}
-- lem-1-2-5-b-i {v = v} (Var w) v≢x x∈FV-M with w ≟ v
-- lem-1-2-5-b-i (Var w)   v≢x x∈FV-M | yes p = ? -- contradiction (trans (singleton-≡ x∈FV-M) p) (v≢x ∘ sym)
-- lem-1-2-5-b-i (Var w)   v≢x x∈FV-M | no ¬p = ? -- x∈FV-M
-- lem-1-2-5-b-i (App P Q) v≢x x∈FV-M = ? -- ∈-respects-≡ {!   !} x∈FV-M
-- lem-1-2-5-b-i (App P Q) v≢x x∈FV-M = ∈-respects-≡ (cong₂ union (cong FV {!   !}) (cong FV {!    !})) x∈FV-M
-- lem-1-2-5-b-i (App P Q) v≢x x∈FV-M = ∈-respects-≡ (cong₂ union ({!   !}) {!   !}) x∈FV-M
-- lem-1-2-5-b-i (Abs w P) v≢x x∈FV-M = {!   !}

-- If M[v≔N] is defined then y ∈ FV(M[v≔N]) iff either y ∈ FV(M) and v ≠ y
-- or y ∈ FV(N) and x ∈ FV(M)

-- lem-1-2-5-b-i : ∀ {x y N} M v →  y ∈ FV (M [ v ≔ N ]) → y ∈ FV M × x ≢ y ⊎ y ∈ FV N × x ∈ FV M
-- lem-1-2-5-b⇒ (Var w) v y∈Applied with w ≟ v
-- lem-1-2-5-b⇒ (Var w) v y∈Applied | yes p = {!   !}
-- lem-1-2-5-b⇒ (Var w) v y∈Applied | no ¬p = inj₁ (y∈Applied , {! singleton-≡ ∈  !})
-- lem-1-2-5-b⇒ (App P Q) v y∈Applied = {!   !}
-- lem-1-2-5-b⇒ (Abs w P) v y∈Applied = {!   !}
--
-- lem-1-2-5-b⇐ : ∀ {x y v M N} → y ∈ FV M × x ≢ y ⊎ y ∈ FV N × x ∈ FV M → y ∈ FV (M [ v ≔ N ])
-- lem-1-2-5-b⇐ = {!   !}

lem-1-2-5-c : (M : PreTerm) → (x : Variable) → M [ x ≔ Var x ] ≡ M
lem-1-2-5-c (Var x  ) y with x ≟ y
lem-1-2-5-c (Var x  ) y | yes p = sym (cong Var p)
lem-1-2-5-c (Var x  ) y | no ¬p = refl
lem-1-2-5-c (App P Q) y = cong₂ App (lem-1-2-5-c P y) (lem-1-2-5-c Q y)
lem-1-2-5-c (Abs x M) y  with x ≟ y
lem-1-2-5-c (Abs x M) y | yes p = cong (λ w → Abs w M) (sym p)
lem-1-2-5-c (Abs x M) y | no ¬p = cong (Abs x) (lem-1-2-5-c M y)

length : PreTerm → ℕ
length (Var x) = 1
length (App P Q) = length P + length Q
length (Abs x M) = 1 + length M

-- lem-1-2-5-c : (M : PreTerm) → (x : Variable) → (N : PreTerm) → T (not (x ∈? FV M)) → M [ x ≔ N ] ≡ M
-- lem-1-2-5-c (Var x') x N x∉M with x' ≟ x
-- lem-1-2-5-c (Var x') x N x∉M | yes p =
--     begin
--         N
--     ≡⟨ {!   !} ⟩
--         {!   !}
--     ≡⟨ {!   !} ⟩
--         Var x'
--     ∎
-- lem-1-2-5-c (Var x') x N x∉M | no ¬p = {!   !}
-- lem-1-2-5-c (App P Q)  x N x∉M =
--     begin
--         App (P [ x ≔ N ]) (Q [ x ≔ N ])
--     ≡⟨ refl ⟩
--         App P Q [ x ≔ N ]
--     ≡⟨ {!   !} ⟩
--         App P Q
--     ∎
-- lem-1-2-5-c (Abs x' M) x N x∉M = {!   !}

-- begin
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ∎

max_stars_repo_name: banacorn/lambda-calculus

max_issues_repo_name: banacorn/lambda-calculus

max_forks_repo_name: banacorn/lambda-calculus


text:
module Rationals.Add.Comm where

open import Equality
open import Function

open import Nats using (zero; ℕ)
                 renaming (suc to s; _+_ to _:+:_; _*_ to _:*:_)
open import Rationals
open import Rationals.Properties
open import Nats.Add.Comm
open import Nats.Multiply.Distrib
open import Nats.Multiply.Comm

------------------------------------------------------------------------
-- internal stuffs

private

  a/c+b/c=a*b/c : ∀ a b c → a ÷ c + b ÷ c ≡ (a :+: b) ÷ c
  a/c+b/c=a*b/c a b c
    rewrite (a :+: b) ÷ c ↑ c
          | sym $ nat-multiply-distrib a b c
            = refl

  a+b=b+a : ∀ x y → x + y ≡ y + x
  a+b=b+a (a ÷ c) (b ÷ d)
    rewrite a ÷ c ↑ d
          | b ÷ d ↑ c
          | a/c+b/c=a*b/c (a :*: d) (b :*: c) $ d :*: c
          | nat-add-comm (a :*: d) $ b :*: c
          | nat-multiply-comm c d
            = refl

------------------------------------------------------------------------
-- public aliases

rational-add-comm : ∀ x y → x + y ≡ y + x
rational-add-comm = a+b=b+a


text:
{- Jesper Cockx, 26-05-2014
   Issue 1023
   Example by Maxime Denes, adapted by Andreas Abel
-}

{-# OPTIONS --cubical-compatible --guardedness #-}

module CoinductionAndUnivalence where

open import Common.Coinduction
open import Common.Equality

prop = Set

data False : prop where

magic : ∀ {a} {A : Set a} → False → A
magic ()

data Pandora : prop where
  C : ∞ False → Pandora

postulate
  ext : (f : False → Pandora) → (g : Pandora → False) →
        (∀ x → f (g x) ≡ x) → (∀ y → g (f y) ≡ y) →
        False ≡ Pandora

foo : False ≡ Pandora
foo = ext f g fg gf
  where
    f : False → Pandora
    f ()

    g : Pandora → False
    g (C c) = ♭ c

    fg : ∀ x → f (g x) ≡ x
    fg x = magic (g x)

    gf : ∀ y → g (f y) ≡ y
    gf ()

loop : False
loop rewrite foo = C (♯ loop)


text:
module Untyped.Monads where

open import Function

open import Data.Unit
open import Data.Product as Prod
open import Data.Sum
open import Data.Sum public using () renaming (_⊎_ to Exceptional; inj₁ to exc; inj₂ to ✓)

open import Category.Monad

id-monad : ∀ {ℓ} → RawMonad {ℓ} id
id-monad = record
  { return = id
  ; _>>=_  = λ a f → f a }

record MonadReader (m : Set → Set) (e : Set) : Set₁ where
  field
    ask       : m e
    local     : ∀ {a} → (e → e) → m a → m a

  asks : ∀ ⦃ _ : RawMonad m ⦄ {a} → (e → a) → m a
  asks ⦃ m ⦄ f = let open RawMonad m in do
    e ← ask
    return $ f (e)

ReaderT : Set → (M : Set → Set) → Set → Set
ReaderT E M A = E → M A

module _ (E : Set) (M : Set → Set) ⦃ mon : RawMonad M ⦄ where
  open RawMonad mon

  reader-monad : RawMonad (ReaderT E M)
  reader-monad = record
    { return = const ∘ return
    ; _>>=_  = λ m f e → m e >>= λ x → f x e }

  reader-monad-reader : MonadReader (ReaderT E M) E
  reader-monad-reader = record
    { ask = return
    ; local = λ f c e → c (f e) }

record MonadWriter (m : Set → Set) (w : Set) : Set₁ where
  field
    write : w → m ⊤

record MonadState (m : Set → Set) (s : Set) : Set₁ where
  field
    state : ∀ {a} → (s → s × a) → m a

  put : s → m ⊤
  put s = state λ _ → (s , tt)

  get : m s
  get = state λ s → (s , s)

  gets : ∀ {a} → (s → a) → m a
  gets f = state λ s → (s , f s)

  modify : ⦃ _ : RawMonad m ⦄ → (s → s) → m ⊤
  modify ⦃ M ⦄ f = let open RawMonad M in do
    s ← get
    put (f s)

StateT : Set → (M : Set → Set) → Set → Set
StateT S M A = S → M (S × A)

module _ (S : Set) (M : Set → Set) ⦃ mon : RawMonad M ⦄ where

  state-monad : RawMonad (StateT S M)
  state-monad = record
    { return = λ a s → return (s , a)
    ; _>>=_  = λ m f s → m s >>= λ where (s' , a) → f a s' }
    where open RawMonad mon

  state-monad-state : MonadState (StateT S M) S
  state-monad-state = record
    { state = λ f s → return (f s) }
    where open RawMonad mon

  open MonadState state-monad-state

{- State focussing -}
module _ {S F M} (focus : S → F) (update : F → S → S)
  ⦃ mon : RawMonad M ⦄
  (st  : MonadState M S)
  where

  focus-monad-state : MonadState M F
  focus-monad-state = record
    { state = λ f →
      MonadState.state st λ s →
        Prod.map₁ (λ f → update f s) (f (focus s))
    }

module _ {M S} ⦃ m : RawMonad M ⦄ (stm : MonadState M S) where
  open RawMonad m
  open MonadState stm

  state-monad-reader : MonadReader M S
  state-monad-reader = record
    { ask   = get
    ; local = λ f m → do
      backup ← get
      modify f
      a ← m
      put backup
      return a
    }

  state-monad-writer : MonadWriter M S
  state-monad-writer = record
    { write = put }

ExceptT : Set → (Set → Set) → Set → Set
ExceptT E M A = M (E ⊎ A)

record MonadExcept (m : Set → Set) (e : Set) : Set₁ where
  field
    throw     : ∀ {a} → e → m a

module _ {E : Set} {M : Set → Set} ⦃ mon : RawMonad M ⦄ where
  open RawMonad mon

  except-monad : RawMonad (ExceptT E M)
  except-monad = record
    { return = λ a → return (✓ a)
    ; _>>=_ = λ where
                c f → c >>= λ where
                  (exc x) → return $ exc x
                  (✓ y)   → f y }

  except-monad-except : MonadExcept (ExceptT E M) E
  except-monad-except = record
    { throw = λ e → return (exc e) }

record MonadResumption (m : Set → Set) (c h : Set) : Set₁ where
  field
    yield : m ⊤
    fork  : c → m h

record MonadComm (m : Set → Set) (c v : Set) : Set₁ where
  field
    recv  : c → m v
    send  : c → v → m ⊤
    close : c → m ⊤

module _ c (r : c → Set) where
  mutual
    Cont = λ cmd a → (r cmd → Free a)

    data Free a : Set where
      pure   : a → Free a
      impure : (cmd : c) → Cont cmd a → Free a

free-monad : ∀ {c r} → RawMonad (Free c r)
free-monad = record
  { return = pure
  ; _>>=_  = bind }
  where
    bind : ∀ {c r a b} → Free c r a → (a → Free c r b) → Free c r b
    bind = λ where
      (pure a) f     → f a
      (impure c k) f → impure c (flip bind f ∘ k)

-- one cannot easily define instances like free-monad-comm generically
-- for some command type and interpretation, because MonadComm
-- requires that the recv return type is fixed a priori, whereas
-- free allows it to be dependent on the command payload.

module M where
  open RawMonad ⦃...⦄ public
  open MonadReader ⦃...⦄ public
  open MonadWriter ⦃...⦄ public renaming (write to schedule)
  open MonadResumption ⦃...⦄ public
  open MonadComm ⦃...⦄ public
  open MonadExcept ⦃...⦄ public
  open MonadState ⦃...⦄ public


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

open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma

module Sec2preliminaries where

-- is-prop, is-contr, is-set, has-dec-eq exist in library.Basicss

-- Let us redefine Type and Σ so that they only refer to the lowest universe.
Type = Type₀
Σ = library.Basics.Σ {lzero} {lzero}

_+_ : Type → Type → Type
X + Y = Coprod X Y

const : {X Y : Type} → (f : X → Y) → Type
const {X} f = (x₁ x₂ : X) → (f x₁) == (f x₂)

hasConst : Type → Type
hasConst X = Σ (X → X) const

pathHasConst : Type → Type
pathHasConst X = (x₁ x₂ : X) → hasConst (x₁ == x₂)

LEM : Type₁
LEM = (P : Type) → is-prop P → P + (¬ P)

LEM∞ : Type₁
LEM∞ = (X : Type) → X + (¬ X)

Funext : {X Y : Type} → Type
Funext {X} {Y} = (f g : X → Y) → ((x : X) → (f x) == (g x)) → f == g

-- In the rest of this file, we define several auxiliary notations or lemmata that are not mentioned
-- explicitly in the article but are somewhat self-explaining.

-- for convenience, we also define ↔ to mean logical equivalence (maps in both directions)
_↔_ : Type → Type → Type
X ↔ Y = (X → Y) × (Y → X)

-- we define it for types in the higher universe separately
-- (because most of the time, we only need the lowest universe and do not want to carry around indices)
_↔₀₁_ : Type → Type₁ → Type₁
A ↔₀₁ B = (A → B) × (B → A)

_↔₁₁_ : Type₁ → Type₁ → Type₁
X ↔₁₁ Y = (X → Y) × (Y → X)

-- composition of ↔
_◎_ : {X Y Z : Type} → (X ↔ Y) → (Y ↔ Z) → (X ↔ Z)
e₁ ◎ e₂ = fst e₂ ∘ fst e₁ , snd e₁ ∘ snd e₂

-- A trivial, but useful lemma. The only thing we do is hiding the arguments.
prop-eq-triv : {P : Type} → {p₁ p₂ : P} → is-prop P → p₁ == p₂
prop-eq-triv h = prop-has-all-paths h _ _

-- A second such useful lemma
second-comp-triv : {X : Type} → {P : X → Type} → ((x : X) → is-prop (P x)) → (a b : Σ X P) → (fst a == fst b) → a == b
second-comp-triv {X} {P} h a b q = pair= q (from-transp P q (prop-eq-triv (h (fst b))))

open import library.types.Pi

-- Note that this lemma needs function extensionality (we use Π-level).
neutral-codomain : {X : Type} → {Y : X → Type} → ((x : X) → is-contr (Y x)) → Π X Y ≃ Unit
neutral-codomain = contr-equiv-Unit ∘ Π-level

-- the following is the function which the univalence axiom postulates to be an equivalence
-- (we define it ourselves as we do not want to implicitly import the whole univalence library)
path-to-equiv : {X Y : Type} → X == Y → X ≃ Y
path-to-equiv {X} idp = ide X

-- some rather silly lemmata

delete-idp : {X : Type} → {x₁ x₂ : X} → (p q : x₁ == x₂) → (p ∙ idp == q) ≃ (p == q)
delete-idp idp q = ide _

add-path : {X : Type} → {x₁ x₂ x₃ : X} → (p q : x₁ == x₂) → (r : x₂ == x₃) → (p == q) == (p ∙ r == q ∙ r)
add-path idp q idp = transport (λ q₁ → (idp == q₁) == (idp == q ∙ idp)) {x = q ∙ idp} {y = q} (∙-unit-r _) idp

open import library.types.Paths

reverse-paths : {X : Type} → {x₁ x₂ : X} → (p : x₂ == x₁) → (q : x₁ == x₂) → (! p == q) ≃ (p == ! q)
reverse-paths p idp =
  ! p == idp   ≃⟨ path-to-equiv (add-path _ _ _) ⟩
  ! p ∙ p == p ≃⟨ path-to-equiv (transport (λ p₁ → (! p ∙ p == p) == (p₁ == p)) (!-inv-l p) idp) ⟩
  idp == p     ≃⟨ !-equiv ⟩
  p == idp     ≃∎

switch-args : {X Y : Type} → {Z : X → Y → Type} → ((x : X) → (y : Y) → Z x y) ≃ ((y : Y) → (x : X) → Z x y)
switch-args = equiv f g h₁ h₂ where
  f = λ k y x → k x y
  g = λ i x y → i y x
  h₁ = λ _ → idp
  h₂ = λ _ → idp

-- another useful (but simple) lemma: if we have a proof of (x , y₁) == (x , y₂) and the type of x is a set, we get a proof of y₁ == y₂.
set-lemma : {X : Type} → (is-set X) → {Y : X → Type} → (x₀ : X) → (y₁ y₂ : Y x₀) → _==_ {A = Σ X Y} (x₀ , y₁) (x₀ , y₂) → y₁ == y₂
set-lemma {X} h {Y} x₀ y₁ y₂ p =
  y₁ =⟨ idp ⟩
  transport Y idp        y₁ =⟨ transport {A = x₀ == x₀} (λ q → y₁ == transport Y q y₁)
                                 {x = idp} {y = ap fst p}
                                 (prop-has-all-paths (h x₀ x₀) _ _)
                                 idp ⟩
  transport Y (ap fst p) y₁ =⟨ snd-of-p ⟩
  y₂ ∎ where
    pairs : =Σ {B = Y} (x₀ , y₁) (x₀ , y₂)
    pairs = <– (=Σ-eqv _ _) p

    paov : y₁ == y₂ [ Y ↓ fst (pairs) ]
    paov = snd pairs

    snd-of-p : transport Y (ap fst p) y₁ == y₂
    snd-of-p = to-transp paov

max_stars_repo_name: nicolaikraus/HoTT-Agda


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

module Issue2442-terminating where

{-# NON_TERMINATING #-}
f : Set
f = f

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda