text:
module SizedIO.Base where

open import Data.Maybe.Base
open import Data.Sum renaming (inj₁ to left; inj₂ to right; [_,_]′ to either)

open import Function
--open import Level using (_⊔_) renaming (suc to lsuc)
open import Size
open import Data.List
open import SizedIO.Object

open import NativeIO
open import Data.Product

record IOInterface  : Set₁ where
  field
    Command   : Set
    Response  : (m : Command) → Set
open IOInterface public

module _ (I : IOInterface ) (let C = Command I) (let R = Response I) where

  mutual
    record IO (i : Size)  (A : Set) : Set where
      coinductive
      constructor delay
      field
        force : {j : Size< i} → IO' j A

    data IO' (i : Size)  (A : Set) : Set where
      do'     : (c : C) (f : R c → IO i A) → IO' i A
      return' : (a : A) → IO' i A

  data IO+ (i : Size)  (A : Set) : Set where
    do' : (c : C) (f : R c → IO i A) → IO+ i A

open IO public

objectInterfToIOInterf : Interface → IOInterface
objectInterfToIOInterf I .Command = I .Method
objectInterfToIOInterf I .Response = I .Result

ioInterfToObjectInterf : IOInterface → Interface
ioInterfToObjectInterf I .Method = I .Command
ioInterfToObjectInterf I .Result = I .Response

module _  {I : IOInterface } (let C = Command I) (let R = Response I) where

  return : ∀{i}{A : Set} (a : A) → IO I i A
  return a .force = return' a

  do : ∀{i}{A : Set} (c : C) (f : R c → IO I i A) → IO I i A
  do c f .force = do' c f

  do1 :  ∀{i} (c : C) → IO I i (R c)
  do1 c = do c return

  infixl 2 _>>=_ _>>='_ _>>_

  mutual
    _>>='_ : ∀{i}{A B : Set}(m : IO' I i A) (k : A → IO I (↑ i) B) → IO' I i B
    do' c f    >>=' k = do' c λ x → f x >>= k
    return' a >>=' k = (k a) .force

    _>>=_ : ∀{i}{A B : Set}(m : IO I i A) (k : A → IO I i B) → IO I i B
    (m >>= k) .force = m .force >>=' k

  _>>_ : ∀{i}{B : Set} (m : IO I i Unit) (k : IO I i B) → IO I i B
  m >> k = m >>= λ _ → k

  {-# NON_TERMINATING #-}
  translateIO : ∀{A : Set}
    →  (translateLocal : (c : C) → NativeIO (R c))
    →  IO I ∞ A
    →  NativeIO A
  translateIO translateLocal m = case (m .force {_}) of
    λ{ (do' c f)    → (translateLocal c) native>>= λ r →
         translateIO translateLocal (f r)
     ; (return' a) → nativeReturn a
     }

  -- Recursion

  -- trampoline provides a generic form of loop (generalizing while/repeat).
  -- Starting at state s : S, step function f is iterated until it returns
  -- a result in A.

  fromIO+' : ∀{i}{A : Set} → IO+ I i A → IO' I i A
  fromIO+' (do' c f) = do' c f

  fromIO+ : ∀{i}{A : Set} → IO+ I i A → IO I i A
  fromIO+ (do' c f) .force = do' c f

  _>>=+'_ : ∀{i}{A B : Set}(m : IO+ I i A) (k : A → IO I i B) → IO' I i B
  do' c f >>=+' k = do' c λ x → f x >>= k

  _>>=+_ : ∀{i}{A B : Set}(m : IO+ I i A) (k : A → IO I i B) → IO I i B
  (m >>=+ k) .force = m >>=+' k

  mutual

    _>>+_ : ∀{i}{A B : Set}(m : IO I i (A ⊎ B)) (k : A → IO I i B) → IO I i B
    (m >>+ k) .force = m .force >>+' k

    _>>+'_ : ∀{j}{A B : Set} (m : IO' I j (A ⊎ B)) (k : A → IO I (↑ j) B) → IO' I j B
    do' c f            >>+' k = do' c λ x → f x >>+ k
    return' (left  a) >>+' k = k a .force
    return' (right b) >>+' k = return' b

   -- loop

  trampoline : ∀{i}{A S : Set} (f : S → IO+ I i (S ⊎ A)) (s : S) → IO I i A
  trampoline f s .force = case (f s) of
    \{ (do' c k) → do' c λ r → k r >>+ trampoline f }

  -- simple infinite loop

  forever : ∀{i}{A B : Set} → IO+ I i A → IO I i B
  forever (do' c f) .force = do' c λ r → f r >>= λ _ → forever (do' c f)

  whenJust : ∀{i}{A : Set} → Maybe A → (A → IO I i (Unit )) → IO I i Unit
  whenJust nothing  k = return _
  whenJust (just a) k = k a

mutual
  mapIO : ∀ {i} → {I : IOInterface} → {A B : Set} → (A → B) → IO I i  A  → IO I i B
  mapIO f p .force = mapIO' f (p .force)

  mapIO' : ∀ {i} → {I : IOInterface} → {A B : Set} → (A → B) → IO' I i  A  → IO' I i B
  mapIO' f (do' c g) = do' c (λ r → mapIO f (g r))
  mapIO' f (return' a) = return' (f a)

sequenceIO : {i : IOInterface} →  List  (IO  i ∞ Unit) → IO i ∞ Unit
sequenceIO [] .force = return' unit
sequenceIO (p ∷ l) = p >>= (λ _ → sequenceIO l)

Return : {i : Size} → {int : IOInterface} →  {A : Set} → A → IO int i A
Return a .force = return' a

Do : {i : Size} → {int : IOInterface} → (c : int .Command)
                → IO int i (int .Response c)
Do c .force = do' c Return

module _  {I : IOInterface }
          (let C = Command I)
          (let R = Response I)
           where
  mutual
    fmap : (i : Size) → {A B : Set} → (f : A → B)
            → IO I i A
            → IO I i B
    fmap i {A} {B} f p .force {j} = fmap' j {A} {B} f (p .force {j})

    fmap' : (i : Size) → {A B : Set} → (f : A → B )
            → IO' I i A
            → IO' I i B
    fmap' i {A} {B} f (do' c f₁) = do' c (λ r → fmap i {A} {B} f (f₁ r))
    fmap' i {A} {B} f (return' a) = return' (f a)

module _ (I : IOInterface )
         (let C = I .Command)
         (let R = I .Response)
           where

    data IOind (A : Set) : Set where

      do''     : (c : C) (f : (r : R c) → IOind A) → IOind A
      return'' : (a : A) → IOind A

_>>''_ : {I : IOInterface}(let C = I .Command)(let R = I .Response)
         {A B : Set} (p : IOind I A) (q : A → IOind I B) → IOind I B
do'' c f >>'' q = do'' c (λ r →  f r >>'' q)
return'' a >>'' q = q a

module _ {I : Interface }
         (let M = I .Method)
         (let R = I .Result)
           where

  translate : ∀{A : Set}
               → Object I
               → IOind (objectInterfToIOInterf I) A
               →  A × Object I
  translate {A} obj (do'' c p) = obj .objectMethod c ▹ λ {(x , o')
                                      → translate {A} o' (p x)  }
  translate {A} obj (return'' a) = a , obj

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
------------------------------------------------------------------------
-- Results relating different instances of certain axioms related to
-- equality
------------------------------------------------------------------------

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

module Equality.Instances-related where

import Bijection
open import Equality
import Equivalence
import Function-universe
import H-level
import H-level.Closure
open import Logical-equivalence using (_⇔_)
open import Prelude
import Surjection

private
  module E (e⁺ : ∀ e → Equivalence-relation⁺ e) where
    open Reflexive-relation′
           (λ e → Equivalence-relation⁺.reflexive-relation (e⁺ e))
         public

-- All families of equality types that satisfy certain axioms are
-- pointwise isomorphic. One of the families are used to define what
-- "isomorphic" means.
--
-- The isomorphisms map reflexivity to reflexivity in both directions.
--
-- Hofmann and Streicher prove something similar in "The groupoid
-- interpretation of type theory".

all-equality-types-isomorphic :
  ∀ {e₁ e₂}
  (eq₁ : ∀ {a p} → Equality-with-J a p e₁)
  (eq₂ : ∀ {a p} → Equality-with-J a p e₂) →
  let open Bijection eq₁ in
  ∀ {a} {A : Type a} →
  ∃ λ (iso : {x y : A} → E._≡_ e₁ x y ↔ E._≡_ e₂ x y) →
    (∀ {x} → E._≡_ e₂ (_↔_.to   iso (E.refl e₁ x)) (E.refl e₂ x)) ×
    (∀ {x} → E._≡_ e₁ (_↔_.from iso (E.refl e₂ x)) (E.refl e₁ x))
all-equality-types-isomorphic {c₁} {c₂} eq₁ eq₂ =
    record
      { surjection = record
        { logical-equivalence = record
          { to   = to c₂ eq₁
          ; from = to c₁ eq₂
          }
        ; right-inverse-of = to c₁ eq₂ ∘ to∘to _ _ eq₂ eq₁
        }
      ; left-inverse-of = to∘to _ _ eq₁ eq₂
      }
  , to-refl c₂ eq₁
  , to-refl c₁ eq₂
  where
  open E
  open module Eq {c} (eq : ∀ {a p} → Equality-with-J a p c) =
    Equality-with-J′ eq hiding (_≡_; refl)

  to : ∀ {c₁} c₂ (eq₁ : ∀ {a p} → Equality-with-J a p c₁)
       {a} {A : Type a} {x y : A} →
       _≡_ c₁ x y → _≡_ c₂ x y
  to c₂ eq₁ {x = x} x≡y = subst eq₁ (_≡_ c₂ x) x≡y (refl c₂ x)

  to-refl :
    ∀ {c₁} c₂ (eq₁ : ∀ {a p} → Equality-with-J a p c₁)
    {a} {A : Type a} {x : A} →
    _≡_ c₂ (to c₂ eq₁ (refl c₁ x)) (refl c₂ x)
  to-refl c₂ eq₁ = to c₂ eq₁ $ subst-refl eq₁ (_≡_ c₂ _) _

  to∘to : ∀ c₁ c₂
          (eq₁ : ∀ {a p} → Equality-with-J a p c₁)
          (eq₂ : ∀ {a p} → Equality-with-J a p c₂) →
          ∀ {a} {A : Type a} {x y : A} (x≡y : _≡_ c₁ x y) →
          _≡_ c₁ (to c₁ eq₂ (to c₂ eq₁ x≡y)) x≡y
  to∘to c₁ c₂ eq₁ eq₂ = elim eq₁
    (λ {x y} x≡y → _≡_ c₁ (to c₁ eq₂ (to c₂ eq₁ x≡y)) x≡y)
    (λ x → to c₁ eq₂ (to c₂ eq₁ (refl c₁ x))  ≡⟨ cong eq₁ (to c₁ eq₂) (subst-refl eq₁ (_≡_ c₂ x) (refl c₂ x)) ⟩
           to c₁ eq₂ (refl c₂ x)              ≡⟨ to c₁ eq₂ $ subst-refl eq₂ (_≡_ c₁ x) (refl c₁ x) ⟩∎
           refl c₁ x                          ∎)
    where
    open Derived-definitions-and-properties eq₁
      using (step-≡; finally)

module _ {congruence⁺}
         (eq : ∀ {a p} → Equality-with-J a p congruence⁺)
         where

  open Derived-definitions-and-properties eq
  open Function-universe eq hiding (_∘_) renaming (id to ⟨id⟩)
  open H-level.Closure eq
  open Surjection eq using (_↠_)

  private
    open module Eq = Equivalence eq using (_≃_)

  abstract

    -- The type Equality-with-J₀ a p reflexive-relation is
    -- contractible (given the assumptions in the telescope above, and
    -- assuming extensionality). A slight variant of this observation
    -- came up in a discussion between Thierry Coquand, Simon Huber
    -- and Nicolai Kraus. The proof is based on one due to Nicolai
    -- Kraus.

    Equality-with-J-contractible :
      ∀ {a p} →
      Extensionality (lsuc (a ⊔ p)) (a ⊔ lsuc p) →
      Contractible (Equality-with-J₀ a p (λ _ → reflexive-relation))
    Equality-with-J-contractible {a} {p} ext =                        $⟨ contr ⟩
      Contractible ((A : Type a) (P : I A → Type p)
                    (d : ∀ x → P (to x)) → Singleton d)               ↝⟨ H-level.respects-surjection eq surj 0 ⟩

      Contractible (Equality-with-J₀ a p (λ _ → reflexive-relation))  □
      where
      I : Type a → Type a
      I A = ∃ λ (x : A) → ∃ λ (y : A) → x ≡ y

      to : ∀ {A} → A → I A
      to x = x , x , refl x

      ≃I : ∀ {A} → A ≃ I A
      ≃I = Eq.↔⇒≃ (record
        { surjection = record
          { logical-equivalence = record
            { to   = to
            ; from = proj₁
            }
          ; right-inverse-of = λ q →
              let x , y , x≡y = q in
              cong (x ,_) $
                Σ-≡,≡→≡ x≡y
                        (subst (x ≡_) x≡y (refl x)  ≡⟨ sym trans-subst ⟩
                         trans (refl x) x≡y         ≡⟨ trans-reflˡ x≡y ⟩∎
                         x≡y                        ∎)
          }
        ; left-inverse-of = refl
        })

      contr :
        Contractible ((A : Type a) (P : I A → Type p)
                      (d : ∀ x → P (to x)) → Singleton d)
      contr =
        Π-closure          (lower-extensionality (lsuc p) lzero    ext) 0 λ _ →
        Π-closure          (lower-extensionality (lsuc a) (lsuc p) ext) 0 λ _ →
        Π-closure          (lower-extensionality _        (lsuc p) ext) 0 λ _ →
        singleton-contractible _

      surj :
        ((A : Type a) (P : I A → Type p)
         (d : ∀ x → P (to x)) → Singleton d) ↠
        Equality-with-J₀ a p (λ _ → reflexive-relation)
      surj =
        ((A : Type a) (P : I A → Type p)
         (d : ∀ x → P (to x)) → Singleton d)                    ↔⟨⟩

        ((A : Type a) (P : I A → Type p)
         (d : ∀ x → P (to x)) →
         ∃ λ (j : (x : A) → P (to x)) → j ≡ d)                  ↔⟨ (∀-cong (lower-extensionality (lsuc p) lzero ext) λ _ →
                                                                              ∀-cong (lower-extensionality (lsuc a) (lsuc p) ext) λ _ →
                                                                              ∀-cong (lower-extensionality _ (lsuc p) ext) λ _ →
                                                                              ∃-cong λ _ → inverse $
                                                                              Eq.extensionality-isomorphism (lower-extensionality _ _ ext)) ⟩
        ((A : Type a) (P : I A → Type p)
         (d : ∀ x → P (to x)) →
         ∃ λ (j : (x : A) → P (to x)) → (x : A) → j x ≡ d x)    ↔⟨ (∀-cong (lower-extensionality (lsuc p) lzero ext) λ _ →
                                                                              ∀-cong (lower-extensionality (lsuc a) (lsuc p) ext) λ _ →
                                                                              ∀-cong (lower-extensionality _ (lsuc p) ext) λ _ → inverse $
                                                                              Σ-cong (inverse $ Π-cong (lower-extensionality _ _ ext)
                                                                                ≃I λ _ → ⟨id⟩ {k = equivalence}) λ _ →
                                                                              ⟨id⟩ {k = equivalence}) ⟩
        ((A : Type a) (P : I A → Type p)
         (d : ∀ x → P (to x)) →
         ∃ λ (j : (q : I A) → P q) → (x : A) → j (to x) ≡ d x)  ↔⟨ (∀-cong (lower-extensionality (lsuc p) lzero ext) λ _ →
                                                                              ∀-cong (lower-extensionality (lsuc a) (lsuc p) ext) λ _ →
                                                                              ΠΣ-comm) ⟩
        ((A : Type a) (P : I A → Type p) →
         ∃ λ (j : (d : ∀ x → P (to x)) →
                  (q : I A) → P q) →
             (d : ∀ x → P (to x))
             (x : A) → j d (to x) ≡ d x)                        ↔⟨ (∀-cong (lower-extensionality (lsuc p) lzero ext) λ _ →
                                                                              ΠΣ-comm) ⟩
        ((A : Type a) →
         ∃ λ (j : (P : I A → Type p) (d : ∀ x → P (to x)) →
                  (q : I A) → P q) →
             (P : I A → Type p) (d : ∀ x → P (to x))
             (x : A) → j P d (to x) ≡ d x)                      ↔⟨ ΠΣ-comm ⟩

        (∃ λ (J : (A : Type a) (P : I A → Type p)
                  (d : ∀ x → P (to x)) →
                  (q : I A) → P q) →
             (A : Type a) (P : I A → Type p)
             (d : ∀ x → P (to x))
             (x : A) → J A P d (to x) ≡ d x)                    ↝⟨ record
                                                                     { logical-equivalence = record
                                                                       { to   = uncurry λ J Jβ → record
                                                                                { elim      = λ P r x≡y →
                                                                                J _ (P ∘ proj₂ ∘ proj₂) r (_ , _ , x≡y)
                                                                                ; elim-refl = λ P r → Jβ _ (P ∘ proj₂ ∘ proj₂) r _
                                                                                }
                                                                       ; from = λ eq →
                                                                             (λ A P d q → Equality-with-J₀.elim eq
                                                                                (λ x≡y → P (_ , _ , x≡y)) d (proj₂ (proj₂ q)))
                                                                           , (λ A P d x → Equality-with-J₀.elim-refl eq
                                                                                (λ x≡y → P (_ , _ , x≡y)) d)
                                                                       }
                                                                     ; right-inverse-of = refl
                                                                     } ⟩□
        Equality-with-J₀ a p (λ _ → reflexive-relation)         □

  private

    -- A related example. It had been suggested that the two proofs
    -- proof₁ and proof₂ below might not be provably equal, but Simon
    -- Huber managed to prove that they are (using a slightly
    -- different type for elim-refl).

    module _ {a p} {A : Type a}
             (P : A → Type p)
             {x : A} (y : P x) where

      subst′ : {x y : A} (P : A → Type p) → x ≡ y → P x → P y
      subst′ P = elim (λ {u v} _ → P u → P v) (λ _ p → p)

      subst′-refl≡id : {x : A} (P : A → Type p) → subst′ P (refl x) ≡ id
      subst′-refl≡id P = elim-refl (λ {u v} _ → P u → P v) (λ _ p → p)

      proof₁ proof₂ :
        subst′ P (refl x) (subst′ P (refl x) y) ≡ subst′ P (refl x) y

      proof₁ = cong (_$ subst′ P (refl x) y) (subst′-refl≡id P)

      proof₂ = cong (subst′ P (refl x)) (cong (_$ y) (subst′-refl≡id P))

      proof₁≡proof₂ : proof₁ ≡ proof₂
      proof₁≡proof₂ =
        subst (λ (s : Singleton id) →
                 ∀ y → cong (_$ proj₁ s y) (proj₂ s) ≡
                       cong (proj₁ s) (cong (_$ y) (proj₂ s)))

              (id                , refl id           ≡⟨ proj₂ (singleton-contractible _) _ ⟩∎
               subst′ P (refl x) , subst′-refl≡id P  ∎)

              (λ y →
                 cong (_$ y) (refl id)            ≡⟨ cong-id _ ⟩∎
                 cong id (cong (_$ y) (refl id))  ∎)

              y

ext: agda

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module index where

-- natural numbers
--- additions
import Nats.Add.Assoc
  using (nat-add-assoc) -- associative law
import Nats.Add.Comm
  using (nat-add-comm) -- commutative law
import Nats.Add.Invert
  using (nat-add-invert) -- a + a == b + b implies a == b
  using (nat-add-invert-1) -- a + 1 == b + 1 implies a == b

--- multiplications
import Nats.Multiply.Comm
  using (nat-multiply-comm) -- commutative law
import Nats.Multiply.Distrib
  using (nat-multiply-distrib) -- distributive law
import Nats.Multiply.Assoc
  using (nat-multiply-assoc) -- associative law

-- integers
--- some properties
import Ints.Properties
  using (eq-int-to-nat) -- for natrual number a, + a == + a implis a == a
  using (eq-neg-int-to-nat) -- for natrual number a, - a == - a implis a == a
  using (eq-nat-to-int) -- for natrual number a, a == a implis + a == + a
  using (eq-neg-nat-to-int) -- for natrual number a, a == a implis - a == - a

--- additions
import Ints.Add.Comm
  using (int-add-comm) -- commutative law
import Ints.Add.Assoc
  using (int-add-assoc) -- associative law
import Ints.Add.Invert
  using (int-add-invert) -- a + a == b + b implis a == b

-- non-negative rationals
--- some properties
import Rationals.Properties
  -- if b is not zero, n times b div b is the original number
  using (times-div-id)

-- additions
import Rationals.Add.Comm
  using (rational-add-comm) -- commutative law
import Rationals.Add.Assoc
  using (rational-add-assoc) -- associative law

-- multiplications
import Rationals.Multiply.Comm
  using (rational-multiply-comm) -- commutative law

-- logics
--- the "and" relations
import Logics.And
  using (and-comm) -- commutative law
  using (and-assoc) -- associative law

--- the "or" relations
import Logics.Or
  using (or-comm) -- commutative law
  using (or-assoc) -- associative law
  using (or-elim) -- elimination rule

--- negations
import Logics.Not
  -- law that negative twice will make a positive
  using (not-not)
  using (contrapositive) -- contrapositive

-- vectors
--- reverse twice gives the original vector
import Vecs.Reverse
  using (vec-rev-rev-id)

-- lists
--- reverse twice gives the original vector
import Lists.Reverse
  using (list-rev-rev-id)

-- isomorphisms
--- natrual numbers and others
import Isos.NatLike
  using (iso-nat-vec) -- with vector
  using (iso-nat-list) -- with list

--- trees
import Isos.TreeLike
  using (iso-seven-tree-in-one) -- seven trees in one

-- groups
--- s3 group, xxx=e, yy=e, yx=xxy
import Groups.Symm.S3
  using (s3-property-1) -- given s3, prove xyx≡y


text:
module sk where

open import nat

data comb : Set where
  S : comb
  K : comb
  app : comb → comb → comb

data _↝_ : comb → comb → Set where
  ↝K : (a b : comb) → (app (app K a) b) ↝ a
  ↝S : (a b c : comb) → (app (app (app S a) b) c) ↝ (app (app a c) (app b c))
  ↝Cong1 : {a a' : comb} (b : comb) → a ↝ a' → (app a b) ↝ (app a' b)
  ↝Cong2 : (a : comb) {b b' : comb} → b ↝ b' → (app a b) ↝ (app a b')

size : comb → ℕ
size S = 1
size K = 1
size (app a b) = suc (size a + size b)

max_stars_repo_name: logicshan/IAL

max_issues_repo_name: logicshan/IAL

max_forks_repo_name: logicshan/IAL


text:
{-# OPTIONS --exact-split #-}
module ExactSplitBerry where

data Bool : Set where
  true false : Bool

maj : Bool → Bool → Bool → Bool
maj true  true  true  = true
maj x     true  false = x
maj false y     true  = y
maj true  false z     = z
maj false false false = false

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Vehicle.Data.Tensor
open import Data.Product
open import Data.Integer as ℤ using (ℤ)
open import Data.Rational as ℚ using (ℚ)
open import Data.Fin as Fin using (Fin; #_)
open import Data.List

module andGate-temp-output where

postulate andGate : Tensor ℚ (2 ∷ []) → Tensor ℚ (1 ∷ [])

Truthy : ℚ → Set
Truthy x = x ℚ.≥ ℤ.+ 1 ℚ./ 2

Falsey : ℚ → Set
Falsey x = x ℚ.≤ ℤ.+ 1 ℚ./ 2

ValidInput : ℚ → Set
ValidInput x = ℤ.+ 0 ℚ./ 1 ℚ.≤ x × x ℚ.≤ ℤ.+ 1 ℚ./ 1

CorrectOutput : ℚ → (ℚ → Set)
CorrectOutput x1 x2 = let y = andGate (x1 ∷ (x2 ∷ [])) (# 0) in (Truthy x1 × Truthy x2 → Truthy y) × ((Truthy x1 × Falsey x2 → Falsey y) × ((Falsey x1 × Truthy x2 → Falsey y) × (Falsey x1 × Falsey x2 → Falsey y)))

abstract
  andGateCorrect : ∀ (x1 : ℚ) → ∀ (x2 : ℚ) → ValidInput x1 × ValidInput x2 → CorrectOutput x1 x2
  andGateCorrect = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to propositional list membership
------------------------------------------------------------------------

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

module Data.List.Membership.Propositional.Properties where

open import Algebra.FunctionProperties using (Op₂; Selective)
open import Category.Monad using (RawMonad)
open import Data.Bool.Base using (Bool; false; true; T)
open import Data.Fin using (Fin)
open import Data.List as List
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
open import Data.List.Relation.Unary.Any.Properties
open import Data.List.Membership.Propositional
import Data.List.Membership.Setoid.Properties as Membershipₛ
open import Data.List.Relation.Binary.Equality.Propositional
  using (_≋_; ≡⇒≋; ≋⇒≡)
open import Data.List.Categorical using (monad)
open import Data.Nat using (ℕ; zero; suc; pred; s≤s; _≤_; _<_; _≤?_)
open import Data.Nat.Properties
open import Data.Product hiding (map)
open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
import Data.Product.Function.Dependent.Propositional as Σ
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (module Equivalence)
open import Function.Injection using (Injection; Injective; _↣_)
open import Function.Inverse as Inv using (_↔_; module Inverse)
import Function.Related as Related
open import Function.Related.TypeIsomorphisms
open import Relation.Binary hiding (Decidable)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; sym; trans; cong; subst; →-to-⟶; _≗_)
import Relation.Binary.Properties.DecTotalOrder as DTOProperties
open import Relation.Unary using (_⟨×⟩_; Decidable)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Negation

private
  open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})

------------------------------------------------------------------------
-- Publicly re-export properties from Core

open import Data.List.Membership.Propositional.Properties.Core public

------------------------------------------------------------------------
-- Equality

module _ {a} {A : Set a} where

  ∈-resp-≋ : ∀ {x} → (x ∈_) Respects _≋_
  ∈-resp-≋ = Membershipₛ.∈-resp-≋ (P.setoid A)

  ∉-resp-≋ : ∀ {x} → (x ∉_) Respects _≋_
  ∉-resp-≋ = Membershipₛ.∉-resp-≋ (P.setoid A)

------------------------------------------------------------------------
-- mapWith∈

module _ {a b} {A : Set a} {B : Set b} where

  mapWith∈-cong : ∀ (xs : List A) → (f g : ∀ {x} → x ∈ xs → B) →
                  (∀ {x} → (x∈xs : x ∈ xs) → f x∈xs ≡ g x∈xs) →
                  mapWith∈ xs f ≡ mapWith∈ xs g
  mapWith∈-cong []       f g cong = refl
  mapWith∈-cong (x ∷ xs) f g cong = P.cong₂ _∷_ (cong (here refl))
    (mapWith∈-cong xs (f ∘ there) (g ∘ there) (cong ∘ there))

  mapWith∈≗map : ∀ f xs → mapWith∈ xs (λ {x} _ → f x) ≡ map f xs
  mapWith∈≗map f xs =
    ≋⇒≡ (Membershipₛ.mapWith∈≗map (P.setoid A) (P.setoid B) f xs)

------------------------------------------------------------------------
-- map

module _ {a b} {A : Set a} {B : Set b} (f : A → B) where

  ∈-map⁺ : ∀ {x xs} → x ∈ xs → f x ∈ map f xs
  ∈-map⁺ = Membershipₛ.∈-map⁺ (P.setoid A) (P.setoid B) (P.cong f)

  ∈-map⁻ : ∀ {y xs} → y ∈ map f xs → ∃ λ x → x ∈ xs × y ≡ f x
  ∈-map⁻ = Membershipₛ.∈-map⁻ (P.setoid A) (P.setoid B)

  map-∈↔ : ∀ {y xs} → (∃ λ x → x ∈ xs × y ≡ f x) ↔ y ∈ map f xs
  map-∈↔ {y} {xs} =
    (∃ λ x → x ∈ xs × y ≡ f x)   ↔⟨ Any↔ ⟩
    Any (λ x → y ≡ f x) xs       ↔⟨ map↔ ⟩
    y ∈ List.map f xs            ∎
    where open Related.EquationalReasoning

------------------------------------------------------------------------
-- _++_

module _ {a} {A : Set a} {v : A} where

  ∈-++⁺ˡ : ∀ {xs ys} → v ∈ xs → v ∈ xs ++ ys
  ∈-++⁺ˡ = Membershipₛ.∈-++⁺ˡ (P.setoid A)

  ∈-++⁺ʳ : ∀ xs {ys} → v ∈ ys → v ∈ xs ++ ys
  ∈-++⁺ʳ = Membershipₛ.∈-++⁺ʳ (P.setoid A)

  ∈-++⁻ : ∀ xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
  ∈-++⁻ = Membershipₛ.∈-++⁻ (P.setoid A)

  ∈-insert : ∀ xs {ys} → v ∈ xs ++ [ v ] ++ ys
  ∈-insert xs = Membershipₛ.∈-insert (P.setoid A) xs refl

  ∈-∃++ : ∀ {xs} → v ∈ xs → ∃₂ λ ys zs → xs ≡ ys ++ [ v ] ++ zs
  ∈-∃++ v∈xs with Membershipₛ.∈-∃++ (P.setoid A) v∈xs
  ... | ys , zs , _ , refl , eq = ys , zs , ≋⇒≡ eq

------------------------------------------------------------------------
-- concat

module _ {a} {A : Set a} {v : A} where

  ∈-concat⁺ : ∀ {xss} → Any (v ∈_) xss → v ∈ concat xss
  ∈-concat⁺ = Membershipₛ.∈-concat⁺ (P.setoid A)

  ∈-concat⁻ : ∀ xss → v ∈ concat xss → Any (v ∈_) xss
  ∈-concat⁻ = Membershipₛ.∈-concat⁻ (P.setoid A)

  ∈-concat⁺′ : ∀ {vs xss} → v ∈ vs → vs ∈ xss → v ∈ concat xss
  ∈-concat⁺′ v∈vs vs∈xss =
    Membershipₛ.∈-concat⁺′ (P.setoid A) v∈vs (Any.map ≡⇒≋ vs∈xss)

  ∈-concat⁻′ : ∀ xss → v ∈ concat xss → ∃ λ xs → v ∈ xs × xs ∈ xss
  ∈-concat⁻′ xss v∈c with Membershipₛ.∈-concat⁻′ (P.setoid A) xss v∈c
  ... | xs , v∈xs , xs∈xss = xs , v∈xs , Any.map ≋⇒≡ xs∈xss

  concat-∈↔ : ∀ {xss : List (List A)} →
              (∃ λ xs → v ∈ xs × xs ∈ xss) ↔ v ∈ concat xss
  concat-∈↔ {xss} =
    (∃ λ xs → v ∈ xs × xs ∈ xss)  ↔⟨ Σ.cong Inv.id $ ×-comm _ _ ⟩
    (∃ λ xs → xs ∈ xss × v ∈ xs)  ↔⟨ Any↔ ⟩
    Any (Any (v ≡_)) xss          ↔⟨ concat↔ ⟩
    v ∈ concat xss                ∎
    where open Related.EquationalReasoning

------------------------------------------------------------------------
-- applyUpTo

module _ {a} {A : Set a} where

  ∈-applyUpTo⁺ : ∀ (f : ℕ → A) {i n} → i < n → f i ∈ applyUpTo f n
  ∈-applyUpTo⁺ = Membershipₛ.∈-applyUpTo⁺ (P.setoid A)

  ∈-applyUpTo⁻ : ∀ {v} f {n} → v ∈ applyUpTo f n →
                 ∃ λ i → i < n × v ≡ f i
  ∈-applyUpTo⁻ = Membershipₛ.∈-applyUpTo⁻ (P.setoid A)

------------------------------------------------------------------------
-- tabulate

module _ {a} {A : Set a} where

  ∈-tabulate⁺ : ∀ {n} {f : Fin n → A} i → f i ∈ tabulate f
  ∈-tabulate⁺ = Membershipₛ.∈-tabulate⁺ (P.setoid A)

  ∈-tabulate⁻ : ∀ {n} {f : Fin n → A} {v} →
                v ∈ tabulate f → ∃ λ i → v ≡ f i
  ∈-tabulate⁻ = Membershipₛ.∈-tabulate⁻ (P.setoid A)

------------------------------------------------------------------------
-- filter

module _ {a p} {A : Set a} {P : A → Set p} (P? : Decidable P) where

  ∈-filter⁺ : ∀ {x xs} → x ∈ xs → P x → x ∈ filter P? xs
  ∈-filter⁺ = Membershipₛ.∈-filter⁺ (P.setoid A) P? (P.subst P)

  ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v
  ∈-filter⁻ = Membershipₛ.∈-filter⁻ (P.setoid A) P? (P.subst P)

------------------------------------------------------------------------
-- _>>=_

module _ {ℓ} {A B : Set ℓ} where

  >>=-∈↔ : ∀ {xs} {f : A → List B} {y} →
           (∃ λ x → x ∈ xs × y ∈ f x) ↔ y ∈ (xs >>= f)
  >>=-∈↔ {xs = xs} {f} {y} =
    (∃ λ x → x ∈ xs × y ∈ f x)  ↔⟨ Any↔ ⟩
    Any (Any (y ≡_) ∘ f) xs     ↔⟨ >>=↔ ⟩
    y ∈ (xs >>= f)              ∎
    where open Related.EquationalReasoning

------------------------------------------------------------------------
-- _⊛_

module _ {ℓ} {A B : Set ℓ} where

  ⊛-∈↔ : ∀ (fs : List (A → B)) {xs y} →
         (∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x) ↔ y ∈ (fs ⊛ xs)
  ⊛-∈↔ fs {xs} {y} =
    (∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x)       ↔⟨ Σ.cong Inv.id (∃∃↔∃∃ _) ⟩
    (∃ λ f → f ∈ fs × ∃ λ x → x ∈ xs × y ≡ f x)  ↔⟨ Σ.cong Inv.id ((_ ∎) ⟨ _×-cong_ ⟩ Any↔) ⟩
    (∃ λ f → f ∈ fs × Any (_≡_ y ∘ f) xs)        ↔⟨ Any↔ ⟩
    Any (λ f → Any (_≡_ y ∘ f) xs) fs            ↔⟨ ⊛↔ ⟩
    y ∈ (fs ⊛ xs)                                ∎
    where open Related.EquationalReasoning

------------------------------------------------------------------------
-- _⊗_

module _ {ℓ} {A B : Set ℓ} where

  ⊗-∈↔ : ∀ {xs ys} {x : A} {y : B} →
         (x ∈ xs × y ∈ ys) ↔ (x , y) ∈ (xs ⊗ ys)
  ⊗-∈↔ {xs} {ys} {x} {y} =
    (x ∈ xs × y ∈ ys)             ↔⟨ ⊗↔′ ⟩
    Any (x ≡_ ⟨×⟩ y ≡_) (xs ⊗ ys) ↔⟨ Any-cong ×-≡×≡↔≡,≡ (_ ∎) ⟩
    (x , y) ∈ (xs ⊗ ys)           ∎
    where
    open Related.EquationalReasoning

------------------------------------------------------------------------
-- length

module _ {a} {A : Set a} where

  ∈-length : ∀ {x xs} → x ∈ xs → 1 ≤ length xs
  ∈-length = Membershipₛ.∈-length (P.setoid A)

------------------------------------------------------------------------
-- lookup

module _ {a} {A : Set a} where

  ∈-lookup : ∀ xs i → lookup xs i ∈ xs
  ∈-lookup = Membershipₛ.∈-lookup (P.setoid A)

------------------------------------------------------------------------
-- foldr

module _ {a} {A : Set a} {_•_ : Op₂ A} where

  foldr-selective : Selective _≡_ _•_ → ∀ e xs →
                    (foldr _•_ e xs ≡ e) ⊎ (foldr _•_ e xs ∈ xs)
  foldr-selective = Membershipₛ.foldr-selective (P.setoid A)

------------------------------------------------------------------------
-- allFin

∈-allFin : ∀ {n} (k : Fin n) → k ∈ allFin n
∈-allFin = ∈-tabulate⁺

------------------------------------------------------------------------
-- inits

[]∈inits : ∀ {a} {A : Set a} (as : List A) → [] ∈ inits as
[]∈inits []       = here refl
[]∈inits (a ∷ as) = here refl

------------------------------------------------------------------------
-- Other properties

-- Only a finite number of distinct elements can be members of a
-- given list.

module _ {a} {A : Set a} where

  finite : (f : ℕ ↣ A) → ∀ xs → ¬ (∀ i → Injection.to f ⟨$⟩ i ∈ xs)
  finite inj []       fᵢ∈[]   = ¬Any[] (fᵢ∈[] 0)
  finite inj (x ∷ xs) fᵢ∈x∷xs = excluded-middle helper
    where
    open Injection inj renaming (injective to f-inj)

    f : ℕ → A
    f = to ⟨$⟩_

    not-x : ∀ {i} → f i ≢ x → f i ∈ xs
    not-x {i} fᵢ≢x with fᵢ∈x∷xs i
    ... | here  fᵢ≡x  = contradiction fᵢ≡x fᵢ≢x
    ... | there fᵢ∈xs = fᵢ∈xs

    helper : ¬ Dec (∃ λ i → f i ≡ x)
    helper (no fᵢ≢x)        = finite inj  xs (λ i → not-x (fᵢ≢x ∘ _,_ i))
    helper (yes (i , fᵢ≡x)) = finite f′-inj xs f′ⱼ∈xs
      where
      f′ : ℕ → A
      f′ j with i ≤? j
      ... | yes i≤j = f (suc j)
      ... | no  i≰j = f j

      ∈-if-not-i : ∀ {j} → i ≢ j → f j ∈ xs
      ∈-if-not-i i≢j = not-x (i≢j ∘ f-inj ∘ trans fᵢ≡x ∘ sym)

      lemma : ∀ {k j} → i ≤ j → ¬ (i ≤ k) → suc j ≢ k
      lemma i≤j i≰1+j refl = i≰1+j (≤-step i≤j)

      f′ⱼ∈xs : ∀ j → f′ j ∈ xs
      f′ⱼ∈xs j with i ≤? j
      ... | yes i≤j = ∈-if-not-i (<⇒≢ (s≤s i≤j))
      ... | no  i≰j = ∈-if-not-i (<⇒≢ (≰⇒> i≰j) ∘ sym)

      f′-injective′ : Injective {B = P.setoid A} (→-to-⟶ f′)
      f′-injective′ {j} {k} eq with i ≤? j | i ≤? k
      ... | yes _   | yes _   = P.cong pred (f-inj eq)
      ... | yes i≤j | no  i≰k = contradiction (f-inj eq) (lemma i≤j i≰k)
      ... | no  i≰j | yes i≤k = contradiction (f-inj eq) (lemma i≤k i≰j ∘ sym)
      ... | no  _   | no  _   = f-inj eq

      f′-inj = record
        { to        = →-to-⟶ f′
        ; injective = f′-injective′
        }

------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

boolFilter-∈ : ∀ {a} {A : Set a} (p : A → Bool) (xs : List A) {x} →
           x ∈ xs → p x ≡ true → x ∈ boolFilter p xs
boolFilter-∈ p []       ()          _
boolFilter-∈ p (x ∷ xs) (here refl) px≡true rewrite px≡true = here refl
boolFilter-∈ p (y ∷ xs) (there pxs) px≡true with p y
... | true  = there (boolFilter-∈ p xs pxs px≡true)
... | false =        boolFilter-∈ p xs pxs px≡true
{-# WARNING_ON_USAGE boolFilter-∈
"Warning: boolFilter was deprecated in v0.15.
Please use filter instead."
#-}

-- Version 0.16

filter-∈ = ∈-filter⁺
{-# WARNING_ON_USAGE filter-∈
"Warning: filter-∈ was deprecated in v0.16.
Please use ∈-filter⁺ instead."
#-}


text:
------------------------------------------------------------------------
-- The derivative operator does not introduce any unneeded ambiguity
------------------------------------------------------------------------

module TotalParserCombinators.Derivative.LeftInverse where

open import Codata.Musical.Notation
open import Data.Maybe hiding (_>>=_)
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality using (refl)

open import TotalParserCombinators.Derivative.Definition
open import TotalParserCombinators.Derivative.SoundComplete
import TotalParserCombinators.InitialBag as I
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics

complete∘sound : ∀ {Tok R xs x s t}
                 (p : Parser Tok R xs) (x∈ : x ∈ D t p · s) →
                 complete (sound p x∈) ≡ x∈
complete∘sound token     return            = refl
complete∘sound (p₁ ∣ p₂) (∣-left     x∈p₁) rewrite complete∘sound p₁ x∈p₁ = refl
complete∘sound (p₁ ∣ p₂) (∣-right ._ x∈p₂) rewrite complete∘sound p₂ x∈p₂ = refl
complete∘sound (f <$> p) (<$> x∈p)         rewrite complete∘sound p  x∈p  = refl

complete∘sound (_⊛_ {fs = nothing} {xs = just _}  p₁ p₂)             (f∈p₁′  ⊛ x∈p₂)  rewrite complete∘sound p₁ f∈p₁′ = refl
complete∘sound (_⊛_ {fs = just _}  {xs = just _}  p₁ p₂) (∣-left     (f∈p₁′  ⊛ x∈p₂)) rewrite complete∘sound p₁ f∈p₁′ = refl
complete∘sound (_⊛_ {fs = just fs} {xs = just xs} p₁ p₂) (∣-right ._ (f∈ret⋆ ⊛ x∈p₂′))
  with (refl , f∈fs) ←          Return⋆.sound fs f∈ret⋆
     | refl          ← Return⋆.complete∘sound fs f∈ret⋆
  rewrite I.complete∘sound p₁ f∈fs | complete∘sound p₂ x∈p₂′ = refl
complete∘sound (_⊛_ {fs = nothing} {xs = nothing} p₁ p₂)             (f∈p₁′  ⊛ x∈p₂)  rewrite complete∘sound (♭ p₁) f∈p₁′ = refl
complete∘sound (_⊛_ {fs = just fs} {xs = nothing} p₁ p₂) (∣-left     (f∈p₁′  ⊛ x∈p₂)) rewrite complete∘sound (♭ p₁) f∈p₁′ = refl
complete∘sound (_⊛_ {fs = just fs} {xs = nothing} p₁ p₂) (∣-right ._ (f∈ret⋆ ⊛ x∈p₂′))
  with (refl , f∈fs) ←          Return⋆.sound fs f∈ret⋆
     | refl          ← Return⋆.complete∘sound fs f∈ret⋆
  rewrite I.complete∘sound (♭ p₁) f∈fs | complete∘sound p₂ x∈p₂′ = refl

complete∘sound (_>>=_ {xs = nothing} {f = just _} p₁ p₂)             (x∈p₁′  >>= y∈p₂x)  rewrite complete∘sound p₁ x∈p₁′ = refl
complete∘sound (_>>=_ {xs = just _}  {f = just _} p₁ p₂) (∣-left     (x∈p₁′  >>= y∈p₂x)) rewrite complete∘sound p₁ x∈p₁′ = refl
complete∘sound (_>>=_ {xs = just xs} {f = just _} p₁ p₂) (∣-right ._ (y∈ret⋆ >>= z∈p₂′y))
  with (refl , y∈xs) ←          Return⋆.sound xs y∈ret⋆
     | refl          ← Return⋆.complete∘sound xs y∈ret⋆
  rewrite I.complete∘sound p₁ y∈xs | complete∘sound (p₂ _) z∈p₂′y = refl
complete∘sound (_>>=_ {xs = nothing} {f = nothing} p₁ p₂)             (x∈p₁′  >>= y∈p₂x)  rewrite complete∘sound (♭ p₁) x∈p₁′ = refl
complete∘sound (_>>=_ {xs = just _}  {f = nothing} p₁ p₂) (∣-left     (x∈p₁′  >>= y∈p₂x)) rewrite complete∘sound (♭ p₁) x∈p₁′ = refl
complete∘sound (_>>=_ {xs = just xs} {f = nothing} p₁ p₂) (∣-right ._ (y∈ret⋆ >>= z∈p₂′y))
  with (refl , y∈xs) ←          Return⋆.sound xs y∈ret⋆
     | refl          ← Return⋆.complete∘sound xs y∈ret⋆
  rewrite I.complete∘sound (♭ p₁) y∈xs | complete∘sound (p₂ _) z∈p₂′y = refl

complete∘sound (nonempty p) x∈p = complete∘sound p x∈p
complete∘sound (cast _ p)   x∈p = complete∘sound p x∈p

complete∘sound (return _) ()
complete∘sound fail       ()

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- 'Set' is no longer a keyword but a primitive defined in
-- 'Agda.Primitive'. It is imported by default but this can be
-- disabled with a flag:

{-# OPTIONS --no-import-sorts #-}

-- By importing Agda.Primitive explicitly we can rename 'Set' to
-- something else:
open import Agda.Primitive renaming (Set to Type)

-- Now 'Set' is no longer in scope:
-- test₁ = Set
-- Error message: Not in scope: Set

-- Instead it is now called 'Type'. Note that suffixed versions
-- 'Type₁', 'Type₂', ... work as expected, as does 'Type ℓ' for a
-- level 'ℓ'!
Foo : Type₁
Foo = Type

Bar : ∀ ℓ → Type (lsuc ℓ)
Bar ℓ = Type ℓ

-- We can now redefine Set however we want:
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

IsSet : ∀ {ℓ} → Type ℓ → Type ℓ
IsSet X = {x y : X} (p q : x ≡ y) → p ≡ q

Set : ∀ ℓ → Type (lsuc ℓ)
Set ℓ = Σ (Type ℓ) IsSet

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- {-# OPTIONS -v tc.conv:30 -v tc.conv.level:60 -v tc.meta.assign:15 #-}

module UniversePolymorphism where

open import Common.Level renaming (_⊔_ to max)

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

infixr 40 _∷_

data Vec {i}(A : Set i) : Nat → Set i where
  []  : Vec {i} A zero
  _∷_ : ∀ {n} → A → Vec {i} A n → Vec {i} A (suc n)

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

vec : ∀ {n a}{A : Set a} → A → Vec A n
vec {zero}  _ = []
vec {suc n} x = x ∷ vec x

_<*>_ : ∀ {n a b}{A : Set a}{B : Set b} → Vec (A → B) n → Vec A n → Vec B n
[]       <*> []       = []
(f ∷ fs) <*> (x ∷ xs) = f x ∷ (fs <*> xs)

flip : ∀ {a b c}{A : Set a}{B : Set b}{C : Set c} →
       (A → B → C) → B → A → C
flip f x y = f y x

module Zip where

  Fun : ∀ {n a} → Vec (Set a) n → Set a → Set a
  Fun []       B = B
  Fun (A ∷ As) B = A → Fun As B

  app : ∀ {n m a}(As : Vec (Set a) n)(B : Set a) →
        Vec (Fun As B) m → Fun (map (flip Vec m) As) (Vec B m)
  app []       B bs = bs
  app (A ∷ As) B fs = λ as → app As B (fs <*> as)

  zipWith : ∀ {n m a}(As : Vec (Set a) n)(B : Set a) →
            Fun As B → Fun (map (flip Vec m) As) (Vec B m)
  zipWith As B f = app As B (vec f)

  zipWith₃ : ∀ {n a}{A B C D : Set a} → (A → B → C → D) → Vec A n → Vec B n → Vec C n → Vec D n
  zipWith₃ = zipWith (_ ∷ _ ∷ _ ∷ []) _

data Σ {a b}(A : Set a)(B : A → Set b) : Set (max a b) where
  _,_ : (x : A)(y : B x) → Σ A B

fst : ∀ {a b}{A : Set a}{B : A → Set b} → Σ A B → A
fst (x , y) = x

snd : ∀ {a b}{A : Set a}{B : A → Set b}(p : Σ A B) → B (fst p)
snd (x , y) = y

-- Normal Σ
List : ∀ {a} → Set a → Set a
List A = Σ _ (Vec A)

nil : ∀ {a}{A : Set a} → List A
nil = _ , []

cons : ∀ {a}{A : Set a} → A → List A → List A
cons x (_ , xs) = _ , x ∷ xs

AnyList : ∀ {i} → Set (lsuc i)
AnyList {i} = Σ (Set i) (List {i})

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Agda.Builtin.Nat

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

f : Fin 1 → Nat
f zero = 0

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Semiring
open import Numbers.Integers.Integers
open import Groups.Definition

module Groups.Cyclic.Definition {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) where

open Setoid S
open Group G
open Equivalence eq
open import Groups.Lemmas G

positiveEltPower : (x : A) (i : ℕ) → A
positiveEltPower x 0 = Group.0G G
positiveEltPower x (succ i) = x · (positiveEltPower x i)

positiveEltPowerWellDefinedG : (x y : A) → (x ∼ y) → (i : ℕ) → (positiveEltPower x i) ∼ (positiveEltPower y i)
positiveEltPowerWellDefinedG x y x=y 0 = reflexive
positiveEltPowerWellDefinedG x y x=y (succ i) = +WellDefined x=y (positiveEltPowerWellDefinedG x y x=y i)

positiveEltPowerCollapse : (x : A) (i j : ℕ) → Setoid._∼_ S ((positiveEltPower x i) · (positiveEltPower x j)) (positiveEltPower x (i +N j))
positiveEltPowerCollapse x zero j = Group.identLeft G
positiveEltPowerCollapse x (succ i) j = transitive (symmetric +Associative) (+WellDefined reflexive (positiveEltPowerCollapse x i j))

elementPower : (x : A) (i : ℤ) → A
elementPower x (nonneg i) = positiveEltPower x i
elementPower x (negSucc i) = Group.inverse G (positiveEltPower x (succ i))

-- TODO: move this to lemmas
elementPowerWellDefinedZ : (i j : ℤ) → (i ≡ j) → {g : A} → elementPower g i ≡ elementPower g j
elementPowerWellDefinedZ i j i=j {g} = applyEquality (elementPower g) i=j

elementPowerWellDefinedZ' : (i j : ℤ) → (i ≡ j) → {g : A} → (elementPower g i) ∼ (elementPower g j)
elementPowerWellDefinedZ' i j i=j {g} = identityOfIndiscernablesRight _∼_ reflexive (elementPowerWellDefinedZ i j i=j)

elementPowerWellDefinedG : (g h : A) → (g ∼ h) → {n : ℤ} → (elementPower g n) ∼ (elementPower h n)
elementPowerWellDefinedG g h g=h {nonneg n} = positiveEltPowerWellDefinedG g h g=h n
elementPowerWellDefinedG g h g=h {negSucc x} = inverseWellDefined (+WellDefined g=h (positiveEltPowerWellDefinedG g h g=h x))

record CyclicGroup : Set (m ⊔ n) where
  field
    generator : A
    cyclic : {a : A} → (Sg ℤ (λ i → Setoid._∼_ S (elementPower generator i) a))


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Prod.Properties where

open import Cubical.Core.Everything

open import Cubical.Data.Prod.Base
open import Cubical.Data.Sigma renaming (_×_ to _×Σ_) hiding (prodIso ; toProdIso ; curryIso)

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

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'

-- Swapping is an equivalence

×≡ : {a b : A × B} → proj₁ a ≡ proj₁ b → proj₂ a ≡ proj₂ b → a ≡ b
×≡ {a = (a1 , b1)} {b = (a2 , b2)} id1 id2 i = (id1 i) , (id2 i)

swap : A × B → B × A
swap (x , y) = (y , x)

swap-invol : (xy : A × B) → swap (swap xy) ≡ xy
swap-invol (_ , _) = refl

isEquivSwap : (A : Type ℓ) (B : Type ℓ') → isEquiv (λ (xy : A × B) → swap xy)
isEquivSwap A B = isoToIsEquiv (iso swap swap swap-invol swap-invol)

swapEquiv : (A : Type ℓ) (B : Type ℓ') → A × B ≃ B × A
swapEquiv A B = (swap , isEquivSwap A B)

swapEq : (A : Type ℓ) (B : Type ℓ') → A × B ≡ B × A
swapEq A B = ua (swapEquiv A B)

private
  open import Cubical.Data.Nat

  -- As × is defined as a datatype this computes as expected
  -- (i.e. "C-c C-n test1" reduces to (2 , 1)). If × is implemented
  -- using Sigma this would be "transp (λ i → swapEq ℕ ℕ i) i0 (1 , 2)"
  test : ℕ × ℕ
  test = transp (λ i → swapEq ℕ ℕ i) i0 (1 , 2)

  testrefl : test ≡ (2 , 1)
  testrefl = refl

-- equivalence between the sigma-based definition and the inductive one
A×B≃A×ΣB : A × B ≃ A ×Σ B
A×B≃A×ΣB = isoToEquiv (iso (λ { (a , b) → (a , b)})
                          (λ { (a , b) → (a , b)})
                          (λ _ → refl)
                          (λ { (a , b) → refl }))

A×B≡A×ΣB : A × B ≡ A ×Σ B
A×B≡A×ΣB = ua A×B≃A×ΣB

-- truncation for products
isOfHLevelProd : (n : HLevel) → isOfHLevel n A → isOfHLevel n B → isOfHLevel n (A × B)
isOfHLevelProd {A = A} {B = B} n h1 h2 =
  let h : isOfHLevel n (A ×Σ B)
      h = isOfHLevelΣ n h1 (λ _ → h2)
  in transport (λ i → isOfHLevel n (A×B≡A×ΣB {A = A} {B = B} (~ i))) h

×-≃ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : Type ℓ₁} {B : Type ℓ₂} {C : Type ℓ₃} {D : Type ℓ₄}
    → A ≃ C → B ≃ D → A × B ≃ C × D
×-≃ {A = A} {B = B} {C = C} {D = D} f g = isoToEquiv (iso φ ψ η ε)
   where
    φ : A × B → C × D
    φ (a , b) = equivFun f a , equivFun g b

    ψ : C × D → A × B
    ψ (c , d) = equivFun (invEquiv f) c , equivFun (invEquiv g) d

    η : section φ ψ
    η (c , d) i = retEq f c i , retEq g d i

    ε : retract φ ψ
    ε (a , b) i = secEq f a i , secEq g b i

{- Some simple ismorphisms -}

prodIso : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {D : Type ℓ'''}
       → Iso A C
       → Iso B D
       → Iso (A × B) (C × D)
Iso.fun (prodIso iAC iBD) (a , b) = (Iso.fun iAC a) , Iso.fun iBD b
Iso.inv (prodIso iAC iBD) (c , d) = (Iso.inv iAC c) , Iso.inv iBD d
Iso.rightInv (prodIso iAC iBD) (c , d) = ×≡ (Iso.rightInv iAC c) (Iso.rightInv iBD d)
Iso.leftInv (prodIso iAC iBD) (a , b) = ×≡ (Iso.leftInv iAC a) (Iso.leftInv iBD b)

toProdIso : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
         → Iso (A → B × C) ((A → B) × (A → C))
Iso.fun toProdIso = λ f → (λ a → proj₁ (f a)) , (λ a → proj₂ (f a))
Iso.inv toProdIso (f , g) = λ a → (f a) , (g a)
Iso.rightInv toProdIso (f , g) = refl
Iso.leftInv toProdIso b = funExt λ a → sym (×-η _)

curryIso : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
         → Iso (A × B → C) (A → B → C)
Iso.fun curryIso f a b = f (a , b)
Iso.inv curryIso f (a , b) = f a b
Iso.rightInv curryIso a = refl
Iso.leftInv curryIso f = funExt λ {(a , b) → refl}

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------
-- Linearisation of mixfix operators
------------------------------------------------------------------------

open import Mixfix.Expr
open import Mixfix.Acyclic.PrecedenceGraph
  using (acyclic; precedence)

module Mixfix.Acyclic.Show
         (g : PrecedenceGraphInterface.PrecedenceGraph acyclic)
         where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.List using (List)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Vec using (Vec; []; _∷_)
import Data.DifferenceList as DiffList
open DiffList using (DiffList; _++_)
              renaming (_∷_ to cons; [_] to singleton)
open import Data.Product using (∃; _,_; -,_)
open import Function using (_∘_; flip)
open import Data.Maybe using (Maybe; nothing; just)
import Data.String as String
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl)

open PrecedenceCorrect acyclic g
open import StructurallyRecursiveDescentParsing.Simplified
open import StructurallyRecursiveDescentParsing.Simplified.Semantics
  as Semantics
open import Mixfix.Fixity
open import Mixfix.Operator
open import Mixfix.Acyclic.Lib as Lib
open Lib.Semantics-⊕
import Mixfix.Acyclic.Grammar
import Mixfix.Acyclic.Lemma
private
  module Grammar = Mixfix.Acyclic.Grammar g
  module Lemma   = Mixfix.Acyclic.Lemma   g

------------------------------------------------------------------------
-- Linearisation

-- Note: The code assumes that the grammar is unambiguous.

module Show where

  mutual

    expr : ∀ {ps} → Expr ps → DiffList NamePart
    expr (_ ∙ e) = exprIn e

    exprIn : ∀ {p assoc} → ExprIn p assoc → DiffList NamePart
    exprIn    ⟪ op ⟫     =            inner op
    exprIn (l ⟨ op ⟫   ) = outer l ++ inner op
    exprIn (  ⟪ op ⟩  r) =            inner op ++ outer r
    exprIn (l ⟨ op ⟩  r) = expr  l ++ inner op ++ expr  r
    exprIn (l ⟨ op ⟩ˡ r) = outer l ++ inner op ++ expr  r
    exprIn (l ⟨ op ⟩ʳ r) = expr  l ++ inner op ++ outer r

    outer : ∀ {p assoc} → Outer p assoc → DiffList NamePart
    outer (similar e) = exprIn e
    outer (tighter e) = expr   e

    inner : ∀ {fix} {ops : List (∃ (Operator fix))} →
            Inner ops → DiffList NamePart
    inner (_∙_ {op = op} _ args) = inner′ (nameParts op) args

    inner′ : ∀ {arity} → Vec NamePart (1 + arity) → Vec (Expr g) arity →
             DiffList NamePart
    inner′ (n ∷ []) []           = singleton n
    inner′ (n ∷ ns) (arg ∷ args) = cons n (expr arg ++ inner′ ns args)

show : ∀ {ps} → Expr ps → List NamePart
show = DiffList.toList ∘ Show.expr

------------------------------------------------------------------------
-- Correctness

module Correctness where

  mutual

    expr : ∀ {ps s} (e : Expr ps) →
           e ⊕ s ∈⟦ Grammar.precs ps ⟧· Show.expr e s
    expr (here refl  ∙ e) = ∣ˡ (<$> exprIn e)
    expr (there x∈xs ∙ e) = ∣ʳ (<$> expr (x∈xs ∙ e))

    exprIn : ∀ {p assoc s} (e : ExprIn p assoc) →
             (-, e) ⊕ s ∈⟦ Grammar.prec p ⟧· Show.exprIn e s
    exprIn {precedence ops sucs} e = exprIn′ _ e
      where
      p        = precedence ops sucs
      module N = Grammar.Prec ops sucs

      lemmaʳ : ∀ {f : Outer p right → ExprIn p right} {s e} {g : DiffList NamePart} →
               (∀ {s} → f ⊕ s ∈⟦ N.preRight ⟧· g s) →
                          e  ⊕ s ∈⟦ N.appʳ <$> N.preRight + ⊛ N.p↑ ⟧·    Show.exprIn e s →
               f (similar e) ⊕ s ∈⟦ N.appʳ <$> N.preRight + ⊛ N.p↑ ⟧· g (Show.exprIn e s)
      lemmaʳ f∈ (<$> fs∈ ⊛ e∈) = <$> +-∷ f∈ fs∈ ⊛ e∈

      preRight : ∀ {s} (e : ExprIn p right) →
                 e ⊕ s ∈⟦ N.appʳ <$> N.preRight + ⊛ N.p↑ ⟧· Show.exprIn e s
      preRight (  ⟪ op ⟩  tighter e) = <$> +-[] (∣ˡ (<$> inner op)) ⊛ expr e
      preRight (  ⟪ op ⟩  similar e) = lemmaʳ   (∣ˡ (<$> inner op)) (preRight e)
      preRight (l ⟨ op ⟩ʳ tighter e) = <$> +-[] (∣ʳ (<$> expr l ⊛ inner op)) ⊛ expr e
      preRight (l ⟨ op ⟩ʳ similar e) = lemmaʳ   (∣ʳ (<$> expr l ⊛ inner op)) (preRight e)

      lemmaˡ : ∀ {f : Outer p left → ExprIn p left} {s e} {g : DiffList NamePart} →
               (∀ {s} → f ⊕ s ∈⟦ N.postLeft ⟧· g s) →
                          e  ⊕ g s ∈⟦ N.appˡ <$> N.p↑ ⊛ N.postLeft + ⟧· Show.exprIn e (g s) →
               f (similar e) ⊕   s ∈⟦ N.appˡ <$> N.p↑ ⊛ N.postLeft + ⟧· Show.exprIn e (g s)
      lemmaˡ {f} f∈ (_⊛_ {x = fs} (<$>_ {x = e} e∈) fs∈) =
        Lib.Semantics-⊕.cast∈ (Lemma.appˡ-∷ʳ (tighter e) fs f) (<$> e∈ ⊛ +-∷ʳ fs∈ f∈)

      postLeft : ∀ {s} (e : ExprIn p left) →
                 e ⊕ s ∈⟦ N.appˡ <$> N.p↑ ⊛ N.postLeft + ⟧· Show.exprIn e s
      postLeft (tighter e ⟨ op ⟫   ) = <$> expr e ⊛ +-[] (∣ˡ (<$> inner op))
      postLeft (similar e ⟨ op ⟫   ) = lemmaˡ            (∣ˡ (<$> inner op)) (postLeft e)
      postLeft (tighter e ⟨ op ⟩ˡ r) = <$> expr e ⊛
                                         +-[] (∣ʳ (<$> inner op ⊛ expr r))
      postLeft (similar e ⟨ op ⟩ˡ r) = lemmaˡ (∣ʳ (<$> inner op ⊛ expr r)) (postLeft e)

      exprIn′ : ∀ assoc {s} (e : ExprIn p assoc) →
                (-, e) ⊕ s ∈⟦ Grammar.prec p ⟧· Show.exprIn e s
      exprIn′ non      ⟪ op ⟫    = ∥ˡ (<$> inner op)
      exprIn′ non   (l ⟨ op ⟩ r) = ∥ʳ (∥ˡ (<$> expr l ⊛ inner op ⊛ expr r))
      exprIn′ right e            = ∥ʳ (∥ʳ (∥ˡ (preRight e)))
      exprIn′ left  e            = ∥ʳ (∥ʳ (∥ʳ (∥ˡ (postLeft e))))

    inner : ∀ {fix s ops} (i : Inner {fix} ops) →
            i ⊕ s ∈⟦ Grammar.inner ops ⟧· Show.inner i s
    inner {fix} {s} (_∙_ {arity} {op} op∈ops args) =
      helper op∈ops args
      where
      helper : {ops : List (∃ (Operator fix))}
               (op∈ : (arity , op) ∈ ops) (args : Vec (Expr g) arity) →
               let i = op∈ ∙ args in
               i ⊕ s ∈⟦ Grammar.inner ops ⟧· Show.inner i s
      helper (here refl) args = ∣ˡ (<$> inner′ (nameParts op) args)
      helper (there {x = _ , _} op∈) args =
        ∣ʳ (<$> helper op∈ args)

    inner′ : ∀ {arity s} (ns : Vec NamePart (1 + arity)) args →
             args ⊕ s ∈⟦ Grammar.expr between ns ⟧· Show.inner′ ns args s
    inner′ (n ∷ [])      []           = between-[]
    inner′ (n ∷ n′ ∷ ns) (arg ∷ args) =
      between-∷ (expr arg) (inner′ (n′ ∷ ns) args)

-- All generated strings are syntactically correct (but possibly
-- ambiguous). Note that this result implies that all
-- precedence-correct expressions are generated by the grammar.

correct : (e : Expr g) → e ∈ Grammar.expression · show e
correct e =
  Semantics.⊕-sound (Lib.Semantics-⊕.sound (Correctness.expr e))


text:
{-# OPTIONS --no-termination-check
  #-}

------------------------------------------------------------------------
-- A library of parser combinators
------------------------------------------------------------------------

module Parallel.Lib where

open import Utilities
open import Parallel
open import Parallel.Index

open import Data.Bool hiding (_≟_)
open import Data.Nat  hiding (_≟_)
open import Data.Product.Record using (_,_)
open import Data.Product renaming (_,_ to pair)
open import Data.List
open import Data.Function
open import Data.Maybe
import Data.Char as C
open import Relation.Nullary
open import Relation.Binary

------------------------------------------------------------------------
-- Applicative functor parsers

-- We could get these for free with better library support.

infixl 4 _⊛_ _<⊛_ _⊛>_ _<$>_ _<$_

-- Parser together with return and _⊛_ form a (generalised)
-- applicative functor. (Warning: I have not checked that the laws are
-- actually satisfied.)

-- Note that all the resulting indices can be inferred.

_⊛_ : forall {tok r₁ r₂ i₁ i₂} ->
      Parser tok i₁ (r₁ -> r₂) -> Parser tok i₂ r₁ ->
      Parser tok _ r₂ -- (i₁ ·I (i₂ ·I 1I))
f ⊛ x = f >>= \f' -> x >>= \x' -> return (f' x')

_<$>_ : forall {tok r₁ r₂ i} ->
        (r₁ -> r₂) -> Parser tok i r₁ -> Parser tok _ r₂ -- (i ·I 1I)
f <$> x = return f ⊛ x

_<⊛_ : forall {tok i₁ i₂ r₁ r₂} ->
       Parser tok i₁ r₁ -> Parser tok i₂ r₂ -> Parser tok _ r₁
x <⊛ y = const <$> x ⊛ y

_⊛>_ : forall {tok i₁ i₂ r₁ r₂} ->
       Parser tok i₁ r₁ -> Parser tok i₂ r₂ -> Parser tok _ r₂
x ⊛> y = flip const <$> x ⊛ y

_<$_ : forall {tok r₁ r₂ i} ->
       r₁ -> Parser tok i r₂ -> Parser tok _ r₁
x <$ y = const x <$> y

------------------------------------------------------------------------
-- Parsers for sequences

mutual

  _⋆ : forall {tok r d} ->
       Parser tok (false , d) r     ->
       Parser tok _           (List r)
  p ⋆ ~ return [] ∣ p +

  _+ : forall {tok r d} ->
       Parser tok (false , d) r     ->
       Parser tok (false , d) (List r)
  p + ~ _∷_ <$> p ⊛ p ⋆

  -- Are these definitions productive? _∣_ and _⊛_ are not
  -- constructors... Unfolding (and ignoring some casts) we get
  -- (unless I've made some mistake)
  --
  --   p ⋆ ~ parser \k -> Base._∣_ (k []) (unP (p +) k)
  --
  -- and
  --
  --   p + ~ parser (\k -> unP p     (\x  ->
  --                       unP (p ⋆) (\xs -> k (x ∷ xs))))
  --       ~ parser (\k -> unP p     (\x  -> Base._∣_ (k (x ∷ []))
  --                      (unP (p +) (\xs -> k (x ∷ xs))))).
  --
  -- Assume that p + is applied to the continuation k =
  -- const Base.fail. We get
  --
  --   unP (p +) k ~ unP p (\x -> unP (p +) (\xs -> k (x ∷ xs))).
  --
  -- This implies that the definitions above are not /obviously/
  -- productive. Note now that when p is defined the function unP p
  -- has type
  --
  --   forall {i' r'} ->
  --   (r -> Base.Parser tok r' i') ->
  --   Base.Parser tok r' (i ·I i')
  --
  -- for arbitrary i' and r', and with i = (false , d) as above this
  -- specialises to
  --
  --   forall {i' r'} ->
  --   (r -> Base.Parser tok r' i') ->
  --   Base.Parser tok r' (false , d).
  --
  -- Note that in some cases it is actually possible for p to
  -- immediately return its input (by first checking that i' =
  -- (false, d)). Furthermore, if p can pattern match on the result of
  -- the continuation (like in Parallel.problematic), then unP (p +)
  -- is not productive. In this case the module system prevents p from
  -- performing such pattern matching /directly/, but ensuring that
  -- this is not possible /indirectly/ seems overly difficult,
  -- considering that there are definitions (other than
  -- Parallel.problematic) which pattern match on Base.Parser.
  --
  -- As an example the type checking of the following definition does
  -- not terminate:
  --
  --   loops : parse-complete (problematic false + >>= \_ -> fail) ('a' ∷ [])
  --           ≡ []
  --   loops = ≡-refl
  --
  -- Furthermore the definition of number below, which uses _+, is
  -- rather fragile, and the type checking of some definitions in
  -- Parallel.Examples which use number fail to terminate (at least
  -- with the version of Agda which is current at the time of
  -- writing).

-- p sepBy sep parses one or more ps separated by seps.

_sepBy_ : forall {tok r r' i d} ->
          Parser tok i r -> Parser tok (false , d) r' ->
          Parser tok _ (List r)
p sepBy sep = _∷_ <$> p ⊛ (sep ⊛> p) ⋆

chain₁ :  forall {tok d₁ i₂ r}
       -> Assoc
       -> Parser tok (false , d₁) r
       -> Parser tok i₂ (r -> r -> r)
       -> Parser tok _ r
chain₁ a p op = chain₁-combine a <$> (pair <$> p ⊛ op) ⋆ ⊛ p

chain :  forall {tok d₁ i₂ r}
      -> Assoc
      -> Parser tok (false , d₁) r
      -> Parser tok i₂ (r -> r -> r)
      -> r
      -> Parser tok _ r
chain a p op x = return x ∣ chain₁ a p op

------------------------------------------------------------------------
-- Parsing a given token (symbol)

module Sym (a : DecSetoid) where

  open DecSetoid a using (_≟_) renaming (carrier to tok)

  sym : tok -> Parser tok _ tok
  sym x = sat p
    where
    p : tok -> Maybe tok
    p y with x ≟ y
    ... | yes _ = just y
    ... | no  _ = nothing

------------------------------------------------------------------------
-- Character parsers

digit : Parser C.Char _ ℕ
digit = 0 <$ sym '0'
      ∣ 1 <$ sym '1'
      ∣ 2 <$ sym '2'
      ∣ 3 <$ sym '3'
      ∣ 4 <$ sym '4'
      ∣ 5 <$ sym '5'
      ∣ 6 <$ sym '6'
      ∣ 7 <$ sym '7'
      ∣ 8 <$ sym '8'
      ∣ 9 <$ sym '9'
  where open Sym C.decSetoid

number : Parser C.Char _ ℕ
number = toNum <$> ds
  where
  -- Inlining ds makes the type checker loop.
  ds = digit +

  toNum = foldr (\n x -> 10 * x + n) 0 ∘ reverse

max_stars_repo_name: yurrriq/parser-combinators


text:
-- Andreas, 2014-01-07 Issue reported by Dmitriy Traytel

{-# OPTIONS --copatterns #-}

module _ where

open import Common.Size
open import Common.Prelude hiding (map)

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream

-- This type should be empty.
data D : (i : Size) → Set where
  cons : ∀ i → Stream (D i) → D (↑ i)

-- BAD: But we can construct an inhabitant.
inh : Stream (D ∞)
head inh = cons ∞ inh  -- Should be rejected by termination checker.
tail inh = inh

map :  ∀{A B} → (A → B) → Stream A → Stream B
head (map f s) = f (head s)
tail (map f s) = map f (tail s)

loop : ∀ i → D i → ⊥
loop .(↑ i) (cons i s) = head (map (loop i) s)

absurd : ⊥
absurd = loop ∞ (cons ∞ inh)


text:
{-# OPTIONS --instance-search-depth=5 --show-implicit #-}

open import Oscar.Prelude
open import Oscar.Class.Smap
open import Oscar.Class.Surjextensionality
open import Oscar.Class.Symmetry
open import Oscar.Class.Transitivity
open import Oscar.Data.Proposequality
open import Oscar.Data.Surjcollation
import Oscar.Class.Surjection.⋆

module Oscar.Data.Surjextenscollation where

module _ {𝔵 𝔞 𝔞̇ 𝔟 𝔟̇} {𝔛 : Ø 𝔵}
  (𝔄 : 𝔛 → 𝔛 → Ø 𝔞)
  (𝔅 : 𝔛 → Ø 𝔟)
  ⦃ _ : Smaphomarrow!.class 𝔄 𝔅 ⦄
  (𝔄̇ : ∀ {x y} → 𝔄 x y → 𝔄 x y → Ø 𝔞̇)
  (let ℭ : 𝔛 → Ø 𝔵 ∙̂ 𝔞 ∙̂ 𝔞̇ ∙̂ ↑̂ 𝔟̇
       ℭ = LeftExtensionṖroperty 𝔟̇ 𝔄 𝔄̇)
  (𝔅̇ : ∀ {y} → 𝔅 y → 𝔅 y → Ø 𝔟̇)
    ⦃ _ : ∀ {y} → Symmetry.class (𝔅̇ {y}) ⦄
    ⦃ _ : ∀ {y} → Transitivity.class (𝔅̇ {y}) ⦄
    ⦃ _ : Surjextensionality!.class 𝔄 𝔄̇ (Extension 𝔅) (Pointwise 𝔅̇) ⦄
  where

  surjextenscollation[_/_]⟦_/_⟧ : ∀ {m} → 𝔅 m → 𝔅 m → ℭ m
  surjextenscollation[_/_]⟦_/_⟧ s t =
    surjcollation⟦ 𝔄 / 𝔅̇ ⟧ s t , λ f≐g f◃s=f◃t →
      -- FIXME this (`surjextensionality[ Pointwise 𝔅̇ ] ⦃ ! ⦄ f≐g t ∙ f◃s=f◃t ∙ symmetry (surjextensionality[ Pointwise 𝔅̇ ] ⦃ ! ⦄ f≐g s)`) used to be a workaround for "instance search depth exhausted", but now does not seem to help. See the FIXME note in Oscar.Class.Surjextensionality.
      ⟪ f≐g ⟫[ Pointwise 𝔅̇ ] t ∙ f◃s=f◃t ∙ symmetry (⟪ f≐g ⟫[ Pointwise 𝔅̇ ] s)

module _ {𝔵 𝔞 𝔞̇} {𝔛 : Ø 𝔵} {𝔄 : 𝔛 → 𝔛 → Ø 𝔞}
  (𝔄̇ : ∀ {x y} → 𝔄 x y → 𝔄 x y → Ø 𝔞̇)
    {𝔟} {𝔅 : 𝔛 → Ø 𝔟}
    {𝔟̇} {𝔅̇ : ∀ {y} → 𝔅 y → 𝔅 y → Ø 𝔟̇}
    ⦃ _ : Smaphomarrow!.class 𝔄 𝔅 ⦄
    ⦃ _ : ∀ {y} → Symmetry.class (𝔅̇ {y}) ⦄
    ⦃ _ : ∀ {y} → Transitivity.class (𝔅̇ {y}) ⦄
    ⦃ _ : Surjextensionality!.class 𝔄 𝔄̇ (Extension 𝔅) (Pointwise 𝔅̇) ⦄
  where
  surjextenscollation⟦_⟧ = surjextenscollation[ 𝔄 / 𝔅 ]⟦ 𝔄̇ / 𝔅̇ ⟧

module _ {𝔵 𝔞 𝔞̇ 𝔟 𝔟̇} {𝔛 : Ø 𝔵} {𝔄 : 𝔛 → 𝔛 → Ø 𝔞} {𝔅 : 𝔛 → Ø 𝔟}
  (𝔄̇ : ∀ {x y} → 𝔄 x y → 𝔄 x y → Ø 𝔞̇)
  (𝔅̇ : ∀ {y} → 𝔅 y → 𝔅 y → Ø 𝔟̇)
    ⦃ _ : Smaphomarrow!.class 𝔄 𝔅 ⦄
    ⦃ _ : ∀ {y} → Symmetry.class (𝔅̇ {y}) ⦄
    ⦃ _ : ∀ {y} → Transitivity.class (𝔅̇ {y}) ⦄
    ⦃ _ : Surjextensionality!.class 𝔄 𝔄̇ (Extension 𝔅) (Pointwise 𝔅̇) ⦄
  where
  surjextenscollation⟦_/_⟧ = surjextenscollation[ 𝔄 / 𝔅 ]⟦ 𝔄̇ / 𝔅̇ ⟧

module Surjextenscollation
  {𝔵 𝔞 𝔞̇} {𝔛 : Ø 𝔵}
  (𝔄 : 𝔛 → 𝔛 → Ø 𝔞)
  (𝔄̇ : ∀ {x y} → 𝔄 x y → 𝔄 x y → Ø 𝔞̇)
    {𝔟} {𝔅 : 𝔛 → Ø 𝔟}
    {𝔟̇} {𝔅̇ : ∀ {y} → 𝔅 y → 𝔅 y → Ø 𝔟̇}
    ⦃ _ : Smaphomarrow!.class 𝔄 𝔅 ⦄
    ⦃ _ : ∀ {y} → Symmetry.class (𝔅̇ {y}) ⦄
    ⦃ _ : ∀ {y} → Transitivity.class (𝔅̇ {y}) ⦄
    ⦃ _ : Surjextensionality!.class 𝔄 𝔄̇ (Extension 𝔅) (Pointwise 𝔅̇) ⦄
  where
  method = surjextenscollation[ 𝔄 / 𝔅 ]⟦ 𝔄̇ / 𝔅̇ ⟧

  infix 18 _⟹_
  _⟹_ = method

module _
  {𝔵} {𝔛 : Ø 𝔵}
  {𝔞₁} {𝔄₁ : 𝔛 → Ø 𝔞₁}
  {𝔞₂} {𝔄₂ : 𝔛 → Ø 𝔞₂}
 (𝔄 : 𝔛 → 𝔛 → Ø 𝔞₁ ∙̂ 𝔞₂)
  ⦃ _ : 𝔄 ≡ Arrow 𝔄₁ 𝔄₂ ⦄
  (let 𝔄 = Arrow 𝔄₁ 𝔄₂)
  where
  open Surjextenscollation 𝔄 _≡̇_ public using () renaming (method to ≡-surjextenscollation⟦_⟧) public


text:
module Ex3 where  -- Conor: 5.5/15 (marked in sem 1 for 3.1-3.4)
                  -- really 5.5/7 then another 3/8 in sem 2, giving 8.5/15

----------------------------------------------------------------------------
-- EXERCISE 3 -- MONADS FOR HUTTON'S RAZOR
--
-- VALUE:     15%
-- DEADLINE:  5pm, Friday 20 November (week 9)
--
-- DON'T SUBMIT, COMMIT!
--
-- The purpose of this exercise is to introduce you to some useful
-- mathematical structures and build good tools for working with
-- vectors
----------------------------------------------------------------------------

open import CS410-Prelude
open import CS410-Monoid
open import CS410-Nat
open import CS410-Vec
open import CS410-Functor

-- HINT: your tasks are heralded with the eminently searchable tag, "???"

----------------------------------------------------------------------------
-- HUTTON'S RAZOR
----------------------------------------------------------------------------

HVal : Set   -- the set of *values* for Hutton's Razor
HVal = Two + Nat   -- Booleans or natural numbers

data HExp (X : Set) : Set where
  var        : X -> HExp X                  -- variables
  val        : HVal -> HExp X               -- values
  _+H_ _>=H_ : (e1 e2 : HExp X) -> HExp X   -- addition, comparison
  ifH_then_else_ : (e1 e2 e3 : HExp X) -> HExp X  -- conditional

_>=2_ : Nat -> Nat -> Two
x      >=2  zero   = tt
zero   >=2  suc _  = ff
suc m  >=2  suc n  = m >=2 n

----------------------------------------------------------------------------
-- ??? 3.1 the HExp syntax-with-substitution monad            (score: 2 / 2)
----------------------------------------------------------------------------

-- Show that HExp is a monad, where the "bind" operation performs
-- simultaneous substitution (transforming all the variables in a term).

hExpMonad : Monad HExp
hExpMonad = record { return = λ x → var x
                   ; _>>=_ = λ x f → hExpMonad>>= x f
                   ; law1 = λ x f → refl
                   ; law2 = λ t → hExpMonadLaw2 t
                   ; law3 = λ f g t → hExpMonadLaw3 t g f
                   } where

  hExpMonad>>= : {X Y : Set} → HExp X → (X → HExp Y) → HExp Y
  hExpMonad>>= (var x) f = f x
  hExpMonad>>= (val x) f = val x
  hExpMonad>>= (x +H y) f = hExpMonad>>= x f +H hExpMonad>>= y f
  hExpMonad>>= (x >=H y) f = hExpMonad>>= x f >=H  hExpMonad>>= y f
  hExpMonad>>= (ifH x then y else z) f = ifH hExpMonad>>= x f then
               hExpMonad>>= y f else hExpMonad>>= z f

  hExpMonadLaw2 : {X : Set} → (t : HExp X) →  hExpMonad>>= t (λ x → var x) == t
  hExpMonadLaw2 (var x) = refl
  hExpMonadLaw2 (val x) = refl
  hExpMonadLaw2 (x +H y) rewrite hExpMonadLaw2 x | hExpMonadLaw2 y  = refl
  hExpMonadLaw2 (x >=H y) rewrite hExpMonadLaw2 x | hExpMonadLaw2 y  = refl
  hExpMonadLaw2 (ifH x then y else z) rewrite hExpMonadLaw2 x | hExpMonadLaw2 y | hExpMonadLaw2 z = refl

  hExpMonadLaw3 : {X Y Z : Set} →  (t  : HExp X) → (g  : Y → HExp Z) → (f  : X → HExp Y) → hExpMonad>>= (hExpMonad>>= t f) g == hExpMonad>>= t (λ x → hExpMonad>>= (f x) g)
  hExpMonadLaw3 (var x) g t = refl
  hExpMonadLaw3 (val x) g t = refl
  hExpMonadLaw3 (f +H f₁) g t rewrite hExpMonadLaw3 f g t | hExpMonadLaw3 f₁ g t = refl
  hExpMonadLaw3 (f >=H f₁) g t rewrite hExpMonadLaw3 f g t | hExpMonadLaw3 f₁ g t = refl
  hExpMonadLaw3 (ifH f then f₁ else f₂) g t rewrite hExpMonadLaw3 f g t | hExpMonadLaw3 f₁ g t | hExpMonadLaw3 f₂ g t = refl

----------------------------------------------------------------------------
-- ??? 3.2 the error management monad                         (score: 1 / 1)
----------------------------------------------------------------------------

-- show that "+ E" is monadic, generalising the "Maybe" monad by allowing
-- some sort of error report

errorMonad : (E : Set) -> Monad \ V -> V + E   -- "value or error"
errorMonad E = record { return = λ x → tt , x
                      ; _>>=_ = errorMonad>>=
                      ; law1 = λ x f → refl
                      ; law2 = errorMonadLaw2
                      ; law3 = errorMonadLaw3
                      } where

  errorMonad>>= : {X Y : Set} → X + E → (X → Y + E) → Y + E
  errorMonad>>= (tt , snd) y = y snd
  errorMonad>>= (ff , snd) y = ff , snd

  errorMonadLaw2 : {X : Set} (t : X + E) → errorMonad>>= t (λ x → tt , x) == t
  errorMonadLaw2 (tt , snd) = refl
  errorMonadLaw2 (ff , snd) = refl

  errorMonadLaw3 :  {X Y Z : Set} (f : X → Y + E) (g : Y → Z + E) (t : X + E) →
                     errorMonad>>= (errorMonad>>= t f) g == errorMonad>>= t
                    (λ x → errorMonad>>= (f x) g)
  errorMonadLaw3 f g (tt , snd) = refl
  errorMonadLaw3 f g (ff , snd) = refl

----------------------------------------------------------------------------
-- ??? 3.3 the environment monad transformer                   (score: 1 / 1)
----------------------------------------------------------------------------

-- show that any monad can be adapted to thread some environment information
-- as well as whatever else it already managed

envMonad : (G : Set){M : Set -> Set} -> Monad M ->
           Monad \ V -> G -> M V      -- "computation in an environment"
envMonad G {M} MM = record { return = λ {X} z _ → Monad.return MM z
                       ; _>>=_ = λ {X} {Y} z z₁ z₂ → (MM Monad.>>= z z₂)
                                   (λ z₃ → z₁ z₃ z₂)
                       ; law1 = λ {X Y} x f → envMonadLaw1 f x
                       ; law2 = envMonadLaw2
                       ; law3 = envMonadLaw3
                       } where
  open Monad MM

  envMonadLaw1 : {X Y : Set} (f  : X → G → M Y) -> (x  : X) ->
                 (λ z₂ → return x >>= (λ z₃ → f z₃ z₂)) == f x
  envMonadLaw1 f x = ext (λ g → Monad.law1 MM x (λ z → f z g))

  envMonadLaw2 : {X : Set} (t : G → M X) →
                 (λ z₂ → t z₂ >>= (λ z₃ → return z₃)) == t
  envMonadLaw2 x = ext (λ a → Monad.law2 MM (x a))

  envMonadLaw3 : {X Y Z : Set} (f : X → G → M Y) (g : Y → G → M Z) (t : G → M X) →(λ z₂ → (t z₂ >>= (λ z₃ → f z₃ z₂)) >>= (λ z₃ → g z₃ z₂)) == (λ z₂ → t z₂ >>= (λ z₃ → f z₃ z₂ >>= (λ z₄ → g z₄ z₂)))
  envMonadLaw3 f g t = ext (λ a → Monad.law3 MM (λ z → f z a) (λ z → g z a) (t a))
----------------------------------------------------------------------------
-- ??? 3.4 interpreting Hutton's Razor                        (score: 1.5 / 3)
----------------------------------------------------------------------------

-- Implement an interpreter for Hutton's Razor.
-- You will need to construct a type to represent possible run-time errors.
-- Ensure that addition and comparison act on numbers, not Booleans.
-- Ensure that the condition in an "if" is a Boolean, not a number.

data InterpretError : Set where
  NotTwo               : InterpretError
  NotNat               : InterpretError

-- helpful things to build

Env : Set -> Set    -- an environment for a given set of variables
Env X = X -> HVal

Compute : Set{- variables -} -> Set{- values -} -> Set
Compute X V = Env X -> V + InterpretError  -- how to compute a V

computeMonad : {Z : Set} -> Monad (Compute Z)
computeMonad {Z} = envMonad (Env Z) (errorMonad InterpretError)

 -- build this from the above parts

-- This operation should explain how to get the value of a variable
-- from the environment.
varVal : {X : Set} -> X -> Compute X HVal
varVal x y = tt , (y x)
--  tt , (y x)

-- These operations should ensure that you get the sort of value
-- that you want, in order to ensure that you don't do bogus
-- computation.
mustBeNat : {X : Set} -> HVal -> Compute X Nat
mustBeNat (tt , tt) x = ff , NotNat        -- Conor: more case analysis than needed
mustBeNat (tt , ff) x = ff , NotNat
mustBeNat (ff , zero) x = tt , zero        -- Conor: more case analysis than needed
mustBeNat (ff , suc snd) x = tt , suc snd

mustBeTwo : {X : Set} -> HVal -> Compute X Two
mustBeTwo (tt , tt) x = tt , tt            -- Conor: more case analysis than needed
mustBeTwo (tt , ff) x = tt , ff
mustBeTwo (ff , zero) x = ff , NotTwo     -- Conor: more case analysis than needed
mustBeTwo (ff , suc snd) x = ff , NotTwo

-- Now, you're ready to go. Don't introduce the environment explicitly.
-- Use the monad to thread it.

interpret : {X : Set} -> HExp X -> Compute X HVal
interpret {X} = go where
  open Monad (computeMonad {X})
  go : HExp X -> Compute X HVal
  -- Conor: you already have the right kit, so it's counterproductive to go down to this detail
  go (var x) E = tt , (E x)
  -- Conor: go (var x) = varVal x
  go (val x) E = tt , x
  go (t +H t₁) E = {!!}
  -- Conor: go (l +H r) =
  --   go l >>= \ lv ->               -- lv : HVal
  --   mustBeNat lv >>= \ ln ->       -- ln : Nat
  --   go r >>= \ rv ->               -- rv : HVal
  --   mustBeNat rv >>= \ rn ->       -- rn : Nat
  --   return (ln +N rn)
  go (t >=H t₁) E = {!!}
  go (ifH t then t₁ else t₂) E = {!!}
----------------------------------------------------------------------------
-- ??? 3.5 Typed Hutton's Razor                               (score: 0.5 / 1)
----------------------------------------------------------------------------

-- Labelling the expressions with their types gives strong guarantees
-- sooner (we can make it grammatically incorrect to add a bool to a
-- nat) and makes some things easier as (if we're adding them then we
-- know they are nats).

-- some names for the types we will use in our typed syntax.

data HType : Set where hTwo hNat : HType

-- mapping names for types to real types.

THVal : HType -> Set
THVal hTwo = Two
THVal hNat = Nat

-- A syntax for types expressions, indexed by typed variables. Compare
-- with the untyped HExp and fill in the missing expression formers,
-- we have shown you the way with _+H_. think: what can be guaranteed?

data THExp (X : HType -> Set) : HType -> Set where
  var : forall {T} -> X T -> THExp X T
  val : forall {T} -> THVal T -> THExp X T
  _+H_ : THExp X hNat -> THExp X hNat -> THExp X hNat
  _>=H_ :  THExp X hNat -> THExp X  hTwo {- Conor: hNat here! -} -> THExp X hTwo
  ifH_then_else_ : forall {T} -> THExp X hTwo -> THExp X T -> THExp X T -> THExp X T

  -- ??? fill in the other two constructs, typed appropriately
  -- (remember that "if then else" can compute values at any type)

----------------------------------------------------------------------------
-- ??? 3.6 Well Typed Programs Don't Go Wrong                 (score: 0 / 1)
----------------------------------------------------------------------------

-- notation for functions betweeen indexed sets (e.g. indexed by types)

_-:>_ : {I : Set}(S T : I -> Set) -> I -> Set
(S -:> T) i = S i -> T i
infixr 3 _-:>_

-- notation for indexed sets

[_] : {I : Set}(X : I -> Set) -> Set
[ X ] = forall {i} -> X i

-- We can put the two together to make types like
--    [ S -:> T ]
--  = forall {i} -> S i -> T i
-- which is the type of functions which work at any index
-- and respect that index. That'll be very useful in just a moment.

-- An evaluator for typed terms, it takes an environment for
-- variables (a function mapping variables to values) and a expression
-- and returns a value). Written as below it looks like it lifts a
-- function from variables to values to a function from terms to
-- values.

eval : {X : HType -> Set} -> [ X -:> THVal ] -> [ THExp X -:> THVal ]
eval g (var x) = g x
eval g (val x) = x
eval g (t +H t1) = eval g t +N eval g t
eval g (t >=H t1) = eval g t >=2 eval g t
eval g (ifH t then t1 else t2) = if eval g t then eval g t1 else eval g t1
  -- Conor: all three step cases get the wrong answers

-- Note that the environment is an *index-respecting* function from
-- variables to values. The index is the type of the variable: you're
-- making sure that when you look up a variable of a given type, you
-- get a value of that type. As a result, you can deliver a *type-safe*
-- evaluator: when an expression has a given type, its value must have
-- that type.

----------------------------------------------------------------------------
-- ??? 3.7 Variable Contexts                                  (score: 1 / 1)
----------------------------------------------------------------------------

-- backwards lists.

data Bwd (X : Set) : Set where
  []   : Bwd X
  _/_  : Bwd X -> X -> Bwd X

-- Our datatype for type indexed expressions is very liberal about
-- variables, they can be any set indexed by types. Here we build
-- something more structured, that nevertheless satisfies the specification

-- We will not use names for variables only numbers.

-- Hence, a context is just a list of types.

Context : Set
Context = Bwd HType

-- Well scoped and well typed variables, top = 0, pop = suc.
-- top is the variable on the right hand end of a non-empty context.
-- pop takes a variable and extends puts it into a longer context.

data Var : (G : Context)(T : HType) -> Set where
  top : {G : Context}{T : HType} -> Var (G / T) T
  pop : {G : Context}{T S : HType} -> Var G T -> Var (G / S) T

-- We can also represent environments as stacks, as opposed to functions.
-- You can read a variable as the sequence of instructions for extracting
-- a value from a stack: you keep popping stuff off until the value you
-- want is the the one at the top.

Stack : Context -> Set
Stack [] = One
Stack (G / S) = Stack G * THVal S

-- Looking up a value for a variable in an an environment or fetching
-- something from a stack given a sequence of pop and top
-- instructions. It's all the same to us!

fetch : {G : Context} -> Stack G -> [ Var G -:> THVal ]
fetch g top = snd g
fetch g (pop v) = fetch (fst g) v

-- An evaluator for expression with more structured variables. We
-- already know how to evaluate, we just have to explain how to deal
-- with manage the different style of environment.

evalStack : {G : Context}{T : HType} ->
            Stack G -> [ THExp (Var G) -:> THVal ]
evalStack g = eval (fetch g)

----------------------------------------------------------------------------
-- ??? 3.8 Terms-With-One-Hole                                (score: 1 / 1)
----------------------------------------------------------------------------

-- Next, we build some kit that we'll use to present type errors.

-- Here we represent an expression with a bit missing. Addition can have
-- have a bit missing (a hole) on the right or on the left. What about
-- the other expression formers?

data HExp' (X : Set) : Set where
  []+H_ _+H[] : HExp X -> HExp' X
  []>=H_ _>=H[] :  HExp X -> HExp' X
  ifH[]then_else_ ifH_then[]else_ ifH_then_else[] : HExp X -> HExp X -> HExp' X

  -- ??? more constructors here
  -- specifically, you will need a constructor for each way that a
  -- subexpression can fit inside an expression;
  -- we use the naming convention of showing where the "hole" is
  -- by putting [] in the corresponding place in the name.

-- take a expression with a hole, and a expression to plug in and plug
-- it in!
_[]<-_ : forall {X} -> HExp' X -> HExp X -> HExp X
([]+H r) []<- t = t +H r
(l +H[]) []<- t = l +H t
([]>=H r) []<- t = t >=H r
(l >=H[]) []<- t = l >=H t
(ifH[]then l else r) []<- t = ifH t then l else r
(ifH e then[]else r) []<- t = ifH e then t else r
(ifH e then l else[]) []<- t = ifH e then l else t
-- ??? more cases here

{-
data List (X : Set) : Set where  -- X scopes over the whole declaration...
  []    : List X                 -- ...so you can use it here...
  _::_  : X -> List X -> List X  -- ...and here.
infixr 3 _::_
-}
-- As we descend down into a term we can keep the pieces we pass along
-- the way in a list, this is a zipper. For example, given the
-- expression 3 + (4 + 5) we could go down by going right and right
-- again to reach 5. In our list we would have [ 4 + [] , 3 + [] ].

-- we need an operation that takes us back up to the root of the tree,
-- restoring the expression to its former state (e.g. 3 + (4 + 5)).

rootToHole : forall {X} -> List (HExp' X) -> HExp X -> HExp X
rootToHole [] t = t
rootToHole (t' :: t's) t = t' []<- rootToHole t's t

-- The idea is that the pair of a List (HExp' X) and a single
-- HExp X together represent a term with a designated subterm "in focus".
-- The list of one-hole terms represents the *path* to the designated
-- subterm, together with the *other stuff* hanging off to either side
-- of that path.

----------------------------------------------------------------------------
-- ??? 3.9 Forgetting Types                                   (score: 0.5 / 1)
----------------------------------------------------------------------------

-- SUSPICION: why would we want to?

-- Given a typed term (THEXP X T) we can forget the types to obtain an
-- untyped term (HExp Y) if we know how to forget types from variables
-- (varFog).

termFog : {X : HType -> Set}{Y : Set}(varFog : {T : HType} -> X T -> Y) ->
          {T : HType} -> THExp X T -> HExp Y
termFog vF (var x) = var (vF x)
termFog vF (val x) = {!x!}  -- Conor: need to find the type
termFog vF (t +H t1) = (termFog vF t) +H (termFog vF t1)
termFog vF (t >=H t1) = (termFog vF t) >=H (termFog vF t1)
termFog vF (ifH t then t1 else t2) = ifH (termFog vF t) then (termFog vF t1) else (termFog vF t2)

-- Note that it's a local naming convention to call functions which
-- forget information "fog". When it is foggy, you can see less.

-- Our purpose in writing a function to throw away information is to
-- *specify* what it means to *obtain* information.

----------------------------------------------------------------------------
-- ??? 3.10 A Typechecking View                               (score: 0 / 3)
----------------------------------------------------------------------------

-- We finish by building a typechecker which will allow us to detect
-- when an untyped Hutton's Razor term can be converted into a typed
-- term (and evaluated safely without rechecking). We make use of
-- your solution to part 3.9 to express the idea that
--    an untyped term is the forgetful image of a typed term we know
-- and your solution to part 3.8 to express the idea that
--    an untyped term can be focused at a place where there is a type error

--  --  --  --  --  --  --  --  --  --  --  --  --  --  --  --  --  --  --
-- But first, we need to build you a wee bit more kit. Typechecking relies
-- on checking that the type you want is the type you've got, which sometimes
-- means testing *equality* of types. It's not enough to have a function
--   htypeEq : HType -> HType -> Two
-- because we need to convince *Agda* of the equality, not just write a function
-- that happens to say yes to equal things.

-- a set with one element removed, i.e. X -[ x ] is the pair of some y in X and
-- a proof that y isn't x

_-[_] : (X : Set) -> X -> Set
X -[ x ] = Sg X \ y -> x == y -> Zero

-- a view for comparing types for equality

data HTypeComparable (T : HType) : HType -> Set where
  same : HTypeComparable T T
  diff : (SnT : HType -[ T ]) -> HTypeComparable T (fst SnT)

-- the above view type presents is two options, and in both of them, we
-- have to come through with enough evidence to convince Agda

-- implementing the view

hTypeCompare : (S T : HType) -> HTypeComparable S T
hTypeCompare hTwo hTwo = same
hTypeCompare hTwo hNat = diff (hNat , \ ())
hTypeCompare hNat hTwo = diff (hTwo , \ ())
hTypeCompare hNat hNat = same

-- we write the obvious four cases; in the "same" cases, the types really
-- do match; in the "diff" cases, Agda can rule out the equation hTwo == hNat
-- (or vice versa) because it knows the constructors of datatypes differ
--  --  --  --  --  --  --  --  --  --  --  --  --  --  --  --  --  --  --

-- But back to our typechecker. To make things easier, we'll assume
-- that our supplier has already been kind enough to do *scope* checking,
-- so that all the variables written by the programmer have been looked
-- up and turned into typed references.

-- a reference: a pair of a type and a variable of that type.

Ref : Context -> Set
Ref G = Sg HType (Var G)

-- making a reference

ref : forall {G S} -> Var G S -> Ref G
ref {G}{S} v = S , v

-- ??? At last, your bit! Show that the following view type covers all
-- untyped terms:
--   either things go well and get the 'ok' and a well typed term
--   or something went wrong down in the expression tree somewhere,
--     so we can explain where that is.

data Checkable (G : Context)  -- the context of typed variables in scope
               (T : HType)    -- the type we expect
               :
               HExp (Ref G)   -- the untyped term we hope has type T
               -> Set where   -- one of two situations applies
  -- either
  ok    : (t : THExp (Var G) T)              -- we have a term of type T
          -> Checkable G T (termFog ref t)   -- and it's what we're checking
  -- or
  err   : (t's : List (HExp' (Ref G)))  -- there's some surroundings
          (s : HExp (Ref G))            -- and a subterm of interest
          -> Checkable G T (rootToHole t's s)  -- in what we're checking

check : (G : Context)(T : HType)(h : HExp (Ref G)) -> Checkable G T h
check G T h = {!!}

-- Now, this isn't quite the whole story, but it's pretty good. We've
-- guaranteed that
--   * if we say yes, it's because we've found the typed version
--     of the untyped input
--   * if we say no, we can point to a place where (we say that) there's a
--     problem
-- So we're *sound* (we never say yes to bad things), but not necessarily
-- *complete* (we can say no to good things). Nothing stops us reporting a
-- bogus type error at the subterm of our choosing! We could work harder
-- and define, in the same way as the typed terms, the "terrors", being
-- the terms containing at least one type error. The canny way to do that
-- is to try writing the typechecker, then grow the datatype that describes
-- all the failure cases.

------------------------------------------------------------------------------
--
-- If you want to read around this topic, you may be interested in
--
--   The Zipper
--   Gerard Huet
--   Journal of Functional Programming, 1997.
--
--   Monadic presentations of lambda terms using generalized inductive types
--   Thorsten Altenkirch and Bernhard Reus
--   Computer Science Logic, 1999.
--
--   An exercise in dependent types: A well-typed interpreter
--   Lennart Augustsson and Magnus Carlsson
--   Workshop on Dependent Types in Programming, Gothenburg, 1999.
--
--   The view from the left
--   Conor McBride and James McKinna
--   Journal of Functional Programming, 2004.


text:
module bool-test where

open import bool
open import eq
open import level

~~tt : ~ ~ tt ≡ tt
~~tt = refl

~~ff : ~ ~ ff ≡ ff
~~ff = refl

~~-elim2 : ∀ (b : 𝔹) → ~ ~ b ≡ b
~~-elim2 tt = ~~tt
~~-elim2 ff = ~~ff

~~tt' : ~ ~ tt ≡ tt
~~tt' = refl{lzero}{𝔹}{tt}

~~ff' : ~ ~ ff ≡ ff
~~ff' = refl{lzero}{𝔹}{ff}

test1 : 𝔹
test1 = tt && ff

test2 : 𝔹
test2 = tt && tt

test1-ff : test1 ≡ ff
test1-ff = refl

test2-tt : test2 ≡ tt
test2-tt = refl

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
import Level as L
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import RevMachine

module PartialRevNoRepeat {ℓ} (M : PartialRevMachine {ℓ}) where
  infix  99 _ᵣₑᵥ
  infixr 10 _∷_
  infixr 10 _++↦_

  open RevMachine.PartialRevMachine M

  is-stuck : State → Set _
  is-stuck st = ∄[ st' ] (st ↦ st')

  is-initial : State → Set _
  is-initial st = ∄[ st' ] (st' ↦ st)

  data _↦ᵣₑᵥ_ : State → State → Set (L.suc ℓ) where
    _ᵣₑᵥ : ∀ {st₁ st₂} → st₁ ↦ st₂ → st₂ ↦ᵣₑᵥ st₁

  data _↦*_ : State → State → Set (L.suc ℓ) where
    ◾ : {st : State} → st ↦* st
    _∷_ : {st₁ st₂ st₃ : State} → st₁ ↦ st₂ → st₂ ↦* st₃ → st₁ ↦* st₃

  _++↦_ : {st₁ st₂ st₃ : State} → st₁ ↦* st₂ → st₂ ↦* st₃ → st₁ ↦* st₃
  ◾ ++↦ st₁↦*st₂ = st₁↦*st₂
  (st₁↦st₁' ∷ st₁'↦*st₂) ++↦ st₂'↦*st₃ = st₁↦st₁' ∷ (st₁'↦*st₂ ++↦ st₂'↦*st₃)

  len↦ : ∀ {st st'} → st ↦* st' → ℕ
  len↦ ◾ = 0
  len↦ (_ ∷ r) = 1 + len↦ r

  data _↦ᵣₑᵥ*_ : State → State → Set (L.suc ℓ) where
    ◾ : ∀ {st} → st ↦ᵣₑᵥ* st
    _∷_ : ∀ {st₁ st₂ st₃} → st₁ ↦ᵣₑᵥ st₂ → st₂ ↦ᵣₑᵥ* st₃ → st₁ ↦ᵣₑᵥ* st₃

  _++↦ᵣₑᵥ_ : ∀ {st₁ st₂ st₃} → st₁ ↦ᵣₑᵥ* st₂ → st₂ ↦ᵣₑᵥ* st₃ → st₁ ↦ᵣₑᵥ* st₃
  ◾ ++↦ᵣₑᵥ st₁↦ᵣₑᵥ*st₂ = st₁↦ᵣₑᵥ*st₂
  (st₁↦ᵣₑᵥst₁' ∷ st₁'↦ᵣₑᵥ*st₂) ++↦ᵣₑᵥ st₂'↦ᵣₑᵥ*st₃ = st₁↦ᵣₑᵥst₁' ∷ (st₁'↦ᵣₑᵥ*st₂ ++↦ᵣₑᵥ st₂'↦ᵣₑᵥ*st₃)

  Rev↦ : ∀ {st₁ st₂} → st₁ ↦* st₂ → st₂ ↦ᵣₑᵥ* st₁
  Rev↦ ◾ = ◾
  Rev↦ (r ∷ rs) = Rev↦ rs ++↦ᵣₑᵥ ((r ᵣₑᵥ) ∷ ◾)

  Rev↦ᵣₑᵥ : ∀ {st₁ st₂} → st₁ ↦ᵣₑᵥ* st₂ → st₂ ↦* st₁
  Rev↦ᵣₑᵥ ◾ = ◾
  Rev↦ᵣₑᵥ ((r ᵣₑᵥ) ∷ rs) = Rev↦ᵣₑᵥ rs ++↦ (r ∷ ◾)

  deterministic* : ∀ {st st₁ st₂} → st ↦* st₁ → st ↦* st₂
                 → is-stuck st₁ → is-stuck st₂
                 → st₁ ≡ st₂
  deterministic* ◾ ◾ stuck₁ stuck₂ = refl
  deterministic* ◾ (r ∷ ↦*₂) stuck₁ stuck₂ = ⊥-elim (stuck₁ (_ , r))
  deterministic* (r ∷ ↦*₁) ◾ stuck₁ stuck₂ = ⊥-elim (stuck₂ (_ , r))
  deterministic* (r₁ ∷ ↦*₁) (r₂ ∷ ↦*₂) stuck₁ stuck₂ with deterministic r₁ r₂
  ... | refl = deterministic* ↦*₁ ↦*₂ stuck₁ stuck₂

  deterministic*' : ∀ {st st₁ st'} → (rs₁ : st ↦* st₁) → (rs : st ↦* st')
                  → is-stuck st'
                  → Σ[ rs' ∈ st₁ ↦* st' ] (len↦ rs ≡ len↦ rs₁ + len↦ rs')
  deterministic*' ◾ rs stuck = rs , refl
  deterministic*' (r ∷ rs₁) ◾ stuck = ⊥-elim (stuck (_ , r))
  deterministic*' (r ∷ rs₁) (r' ∷ rs) stuck with deterministic r r'
  ... | refl with deterministic*' rs₁ rs stuck
  ... | (rs' , eq) = rs' , cong suc eq

  deterministicᵣₑᵥ* : ∀ {st st₁ st₂} → st ↦ᵣₑᵥ* st₁ → st ↦ᵣₑᵥ* st₂ → ¬ (is-fail st)
                    → is-initial st₁ → is-initial st₂
                    → st₁ ≡ st₂
  deterministicᵣₑᵥ* ◾ ◾ _ initial₁ initial₂ = refl
  deterministicᵣₑᵥ* ◾ (r ᵣₑᵥ ∷ ↦ᵣₑᵥ*₂) _ initial₁ initial₂ = ⊥-elim (initial₁ (_ , r))
  deterministicᵣₑᵥ* (r ᵣₑᵥ ∷ ↦ᵣₑᵥ*₁) ◾ _ initial₁ initial₂ = ⊥-elim (initial₂ (_ , r))
  deterministicᵣₑᵥ* (_∷_ {_} {st'} {_} (r₁ ᵣₑᵥ) ↦ᵣₑᵥ*₁) (r₂ ᵣₑᵥ ∷ ↦ᵣₑᵥ*₂) nf initial₁ initial₂ with is-fail? st'
  ... | yes st'-f  = ⊥-elim (fail-is-stuck st'-f (_ , r₁))
  ... | no  st'-nf with deterministicᵣₑᵥ r₁ r₂ nf
  ... | refl = deterministicᵣₑᵥ* ↦ᵣₑᵥ*₁ ↦ᵣₑᵥ*₂ st'-nf initial₁ initial₂

  data _↦[_]_ : State → ℕ → State → Set (L.suc ℓ) where
    ◾ : ∀ {st} → st ↦[ 0 ] st
    _∷_ : ∀ {st₁ st₂ st₃ n} → st₁ ↦ st₂ → st₂ ↦[ n ] st₃ → st₁ ↦[ suc n ] st₃

  _++↦ⁿ_ : ∀ {st₁ st₂ st₃ n m} → st₁ ↦[ n ] st₂ → st₂ ↦[ m ] st₃ → st₁ ↦[ n + m ] st₃
  ◾ ++↦ⁿ st₁↦*st₂ = st₁↦*st₂
  (st₁↦st₁' ∷ st₁'↦*st₂) ++↦ⁿ st₂'↦*st₃ = st₁↦st₁' ∷ (st₁'↦*st₂ ++↦ⁿ st₂'↦*st₃)

  data _↦ᵣₑᵥ[_]_ : State → ℕ → State → Set (L.suc ℓ) where
    ◾ : ∀ {st} → st ↦ᵣₑᵥ[ 0 ] st
    _∷_ : ∀ {st₁ st₂ st₃ n} → st₁ ↦ᵣₑᵥ st₂ → st₂ ↦ᵣₑᵥ[ n ] st₃ → st₁ ↦ᵣₑᵥ[ suc n ] st₃

  _++↦ᵣₑᵥⁿ_ : ∀ {st₁ st₂ st₃ n m} → st₁ ↦ᵣₑᵥ[ n ] st₂ → st₂ ↦ᵣₑᵥ[ m ] st₃ → st₁ ↦ᵣₑᵥ[ n + m ] st₃
  ◾ ++↦ᵣₑᵥⁿ st₁↦*st₂ = st₁↦*st₂
  (st₁↦st₁' ∷ st₁'↦*st₂) ++↦ᵣₑᵥⁿ st₂'↦*st₃ = st₁↦st₁' ∷ (st₁'↦*st₂ ++↦ᵣₑᵥⁿ st₂'↦*st₃)

  deterministicⁿ : ∀ {st st₁ st₂ n} → st ↦[ n ] st₁ → st ↦[ n ] st₂
                 → st₁ ≡ st₂
  deterministicⁿ ◾ ◾ = refl
  deterministicⁿ (r₁ ∷ rs₁) (r₂ ∷ rs₂) with deterministic r₁ r₂
  ... | refl = deterministicⁿ rs₁ rs₂

  deterministicᵣₑᵥⁿ : ∀ {st st₁ st₂ n} → st ↦ᵣₑᵥ[ n ] st₁ → st ↦ᵣₑᵥ[ n ] st₂ → ¬ (is-fail st)
                    → st₁ ≡ st₂
  deterministicᵣₑᵥⁿ ◾ ◾ _ = refl
  deterministicᵣₑᵥⁿ (_∷_ {_} {st'} {_} (r₁ ᵣₑᵥ)  rs₁) (r₂ ᵣₑᵥ ∷ rs₂) nf with is-fail? st'
  ... | yes st'-f  = ⊥-elim (fail-is-stuck st'-f (_ , r₁))
  ... | no  st'-nf with deterministicᵣₑᵥ r₁ r₂ nf
  ... | refl = deterministicᵣₑᵥⁿ rs₁ rs₂ st'-nf

  private
    split↦ⁿ : ∀ {st st'' n m} → st ↦[ n + m ] st''
            → ∃[ st' ] (st ↦[ n ] st' × st' ↦[ m ] st'')
    split↦ⁿ {n = 0} {m} rs = _ , ◾ , rs
    split↦ⁿ {n = suc n} {m} (r ∷ rs) with split↦ⁿ {n = n} {m} rs
    ... | st' , st↦ⁿst' , st'↦ᵐst'' = st' , (r ∷ st↦ⁿst') , st'↦ᵐst''

    split↦ᵣₑᵥⁿ : ∀ {st st'' n m} → st ↦ᵣₑᵥ[ n + m ] st''
               → ∃[ st' ] (st ↦ᵣₑᵥ[ n ] st' × st' ↦ᵣₑᵥ[ m ] st'')
    split↦ᵣₑᵥⁿ {n = 0} {m} rs = _ , ◾ , rs
    split↦ᵣₑᵥⁿ {n = suc n} {m} (r ∷ rs) with split↦ᵣₑᵥⁿ {n = n} {m} rs
    ... | st' , st↦ⁿst' , st'↦ᵐst'' = st' , (r ∷ st↦ⁿst') , st'↦ᵐst''

    diff : ∀ {n m} → n < m → ∃[ k ] (0 < k × n + k ≡ m)
    diff {0} {(suc m)} (s≤s z≤n) = suc m , s≤s z≤n , refl
    diff {(suc n)} {(suc (suc m))} (s≤s (s≤s n≤m)) with diff {n} {suc m} (s≤s n≤m)
    ... | k , 0<k , eq = k , 0<k , cong suc eq

  Revⁿ : ∀ {st st' n} → st ↦[ n ] st' → st' ↦ᵣₑᵥ[ n ] st
  Revⁿ {n = 0} ◾ = ◾
  Revⁿ {n = suc n} (r ∷ rs) rewrite +-comm 1 n = Revⁿ rs ++↦ᵣₑᵥⁿ (r ᵣₑᵥ ∷ ◾)

  NoRepeat : ∀ {st₀ stₙ stₘ n m}
           → is-initial st₀
           → n < m
           → st₀ ↦[ n ] stₙ
           → st₀ ↦[ m ] stₘ
           → stₙ ≢ stₘ
  NoRepeat {stₙ = st} {_} {m} st₀-is-init n<m st₀↦ᵐst st₀↦ᵐ⁺ᵏ⁺¹st refl with diff n<m
  ... | suc k , 0<k , refl with is-fail? st
  ... | yes st-is-f with split↦ⁿ {n = m} {1 + k} st₀↦ᵐ⁺ᵏ⁺¹st
  ... | st′ , st₀↦ᵐst′ , (r ∷ rs) with deterministicⁿ st₀↦ᵐst st₀↦ᵐst′
  ... | refl = ⊥-elim (fail-is-stuck st-is-f (_ , r))
  NoRepeat {stₙ = st} {_} {m} st₀-is-init n<m st₀↦ᵐst st₀↦ᵐ⁺ᵏ⁺¹st refl | suc k , 0<k , refl | no st-is-nf with (Revⁿ st₀↦ᵐst , Revⁿ st₀↦ᵐ⁺ᵏ⁺¹st)
  ... | st'↦ᵐst₀' , st'↦ᵐ⁺ᵏ⁺¹st₀' with split↦ᵣₑᵥⁿ st'↦ᵐ⁺ᵏ⁺¹st₀'
  ... | st′ , st'↦ᵐst′ , st′↦ᵏ⁺¹st₀' with deterministicᵣₑᵥⁿ st'↦ᵐst₀' st'↦ᵐst′ st-is-nf
  ... | refl with st′↦ᵏ⁺¹st₀'
  ... | r ᵣₑᵥ ∷ rs = ⊥-elim (st₀-is-init (_ , r))


text:
module lob--2015-06-14--III where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ    #-}

record Σ {X : Set} (F : X → Set) : Set where
  constructor _,_
  field fst : X
        snd : F fst

data ⊤ : Set where
  unit : ⊤

data Tree (X : Set) : Set where
  br : Tree X → Tree X → Tree X
  leaf : X → Tree X

indtree : {X : Set} → (P : Tree X → Set)
        → ((s t : Tree X) → P s → P t → P (br s t))
        → ((x : X) → P (leaf x))
        → (t : Tree X) → P t
indtree P b l (br s t) = b s t (indtree P b l s) (indtree P b l t)
indtree P b l (leaf x) = l x

data Preterm : Set where
  type : ℕ → Preterm
  pi : Preterm → Preterm → Preterm
  sig : Preterm → Preterm → Preterm
  bot : Preterm
  top : Preterm
  unit : Preterm
  var : ℕ → Preterm
  lam : Preterm → Preterm → Preterm
  app : Preterm → Preterm → Preterm
  tree : Preterm → Preterm
  br : Preterm → Preterm → Preterm → Preterm
  leaf : Preterm → Preterm → Preterm
  ind : Preterm → Preterm → Preterm → Preterm → Preterm → Preterm

‘λ→’ = lam

data _::_ : Preterm → Preterm → Set where
  ::type : (ℓ : ℕ) → type ℓ :: type (suc ℓ)
  -- ...

□ : Preterm → Set
□ T = Σ \(t : Preterm) → t :: T

num : ℕ → Preterm
num 0 = leaf top unit
num (suc n) = br top unit (num n)

data List (X : Set) : Set where
  nil : List X
  _,_ : X → List X → List X

infixr 1 _,_

list : List Preterm → Preterm
list nil = leaf top unit
list (x , xs) = br top x (list xs)

cons : ℕ → List Preterm → Preterm
cons n xs = br top (num n) (list xs)

‘type’ : Preterm → Preterm
‘type’ n = cons 0 (n , nil)

‘pi’ : Preterm → Preterm → Preterm
‘pi’ x f = cons 1 (x , f , nil)

‘sig’ : Preterm → Preterm → Preterm
‘sig’ x f = cons 2 (x , f , nil)

‘bot’ : Preterm
‘bot’ = cons 3 nil

‘top’ : Preterm
‘top’ = cons 4 nil

‘unit’ : Preterm
‘unit’ = cons 5 nil

‘var’ : Preterm → Preterm
‘var’ n = cons 6 (n , nil)

‘lam’ : Preterm → Preterm → Preterm
‘lam’ t b = cons 7 (t , b , nil)

‘app’ : Preterm → Preterm → Preterm
‘app’ f x = cons 8 (f , x , nil)

‘tree’ : Preterm → Preterm
‘tree’ x = cons 9 (x , nil)

‘br’ : Preterm → Preterm → Preterm → Preterm
‘br’ x l r = cons 10 (x , l , r , nil)

‘leaf’ : Preterm → Preterm → Preterm
‘leaf’ x y = cons 11 (x , y , nil)

‘ind’ : Preterm → Preterm → Preterm → Preterm → Preterm → Preterm
‘ind’ x p b l t = cons 12 (x , p , b , l , t , nil)

‘Preterm’ : Preterm
‘Preterm’ = tree top

‘Preterm’::type₀ : ‘Preterm’ :: type 0
‘Preterm’::type₀ = {!!}

‘□’ : Preterm
‘□’ = {!!}

_‘→’_ : Preterm → Preterm → Preterm
A ‘→’ B = pi A {!!}

quot : Preterm → Preterm
quot (type n) = ‘type’ (num n)
quot (pi x f) = ‘pi’ (quot x) (quot f)
quot (sig x f) = ‘sig’ (quot x) (quot f)
quot bot = ‘bot’
quot top = ‘top’
quot unit = ‘unit’
quot (var n) = ‘var’ (num n)
quot (lam x b) = ‘lam’ (quot x) (quot b)
quot (app f x) = ‘app’ (quot f) (quot x)
quot (tree x) = ‘tree’ (quot x)
quot (br x l r) = ‘br’ (quot x) (quot l) (quot r)
quot (leaf x y) = ‘leaf’ (quot x) (quot y)
quot (ind x p b l t) = ‘ind’ (quot x) (quot p) (quot b) (quot l) (quot t)

‘quot’ : Preterm
‘quot’ = {!!}

‘‘→’’ : Preterm
‘‘→’’ = {!!}

⌜_⌝ = quot

_‘’_ = app

infixl 1 _‘’_

postulate
  X        : Set
  ‘X’       : Preterm
  ‘X’::type₀ : ‘X’ :: type 0

App : {‘A’ ‘B’ : Preterm}
      → □ (‘A’ ‘→’ ‘B’)
      → □ ‘A’
      → □ ‘B’
App □‘A→B’ □‘A’ = {!!}

‘App’ : Preterm
‘App’ = {!!}

Quot : {‘T’ : Preterm}
       → □ ‘T’
       → □ (‘□’ ‘’ ⌜ ‘T’ ⌝)
Quot □T = {!!}

‘Quot’ : Preterm
‘Quot’ = {!!}

‘L₀’ : Preterm
‘L₀’ = (‘λ→’ ‘Preterm’ ((‘app’ ⌜ ‘□’ ⌝ (‘app’ (var 0) (‘quot’ ‘’ (var 0)))) ‘’ ‘‘→’’ ‘’ ⌜ ‘X’ ⌝ ))

L : Preterm
L = (λ (h : Preterm) → (app ‘□’ (app h (⌜ h ⌝))) ‘→’ ‘X’) ‘L₀’

‘L’ = app ‘L₀’ ⌜ ‘L₀’ ⌝

Conv : □ (‘□’ ‘’ ⌜ L ⌝) → □ (‘□’ ‘’ ‘L’)
Conv = {!!}

‘Conv’ : Preterm
‘Conv’ = {!!}

postulate
  f    : □ ‘X’ → X
  ‘f’  : Preterm
  d‘f’ : ‘f’ :: (app ‘□’ (quot ‘X’) ‘→’ ‘X’)

y : X
y = (λ (ℓ : □ L) → f (App ℓ (Conv (Quot ℓ))))
      ( ‘λ→’ (‘□’ ‘’ ‘L’) (‘f’ ‘’ (‘App’ ‘’ (var 0) ‘’ (‘Conv’ ‘’ (‘Quot’ ‘’ var 0))))
      , {!!})

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
-- A solution for
--      https://github.com/josevalim/nested-data-structure-traversal
-- in Agda using fold. Basically it is identical to its Haskell sibling except
-- fancy unicode symbols. The `refl` proof at the end is pretty nice though.
--
-- Coded against agda-2.6.1.3 and agda-stdlib-1.5

module Fold where

open import Data.Nat using (ℕ; _+_)
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.String using (String)
open import Data.List using (List; []; _∷_; map; foldl; reverse; length; zipWith; upTo)
open import Data.Product using (_×_; _,_; proj₂)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

record Lesson : Set where
    constructor lesson
    field
        name : String

record Chapter : Set where
    constructor chapter
    field
        title : String
        reset : Bool
        lessons : List Lesson

record PosLesson : Set where
    constructor pos_lesson
    field
        name : String
        pos : ℕ

record PosChapter : Set where
    constructor pos_chapter
    field
        title : String
        reset : Bool
        pos : ℕ
        lessons : List PosLesson

input : List Chapter
input = chapter "Getting started" false
            (lesson "Welcome" ∷ lesson "Installation" ∷ [])
        ∷ chapter "Basic operator" false
            (lesson "Addition / Subtraction" ∷ lesson "Multiplication / Division" ∷ [])
        ∷ chapter "Advanced topics" true
            (lesson "Mutability" ∷ lesson "Immutability" ∷ [])
        ∷ []

expected : List PosChapter
expected = pos_chapter "Getting started" false 1
            (pos_lesson "Welcome" 1 ∷ pos_lesson "Installation" 2 ∷ [])
        ∷ pos_chapter "Basic operator" false 2
            (pos_lesson "Addition / Subtraction" 3 ∷ pos_lesson "Multiplication / Division" 4 ∷ [])
        ∷ pos_chapter "Advanced topics" true 3
            (pos_lesson "Mutability" 1 ∷  pos_lesson "Immutability" 2 ∷ [])
        ∷ []

solve : List Chapter → List PosChapter
solve i = (reverse ∘ proj₂ ∘ proj₂) (foldl go (1 , 1 , []) i)
    where
    go : ℕ × ℕ × List PosChapter → Chapter → ℕ × ℕ × List PosChapter
    go (nc , nl , acc) (chapter title reset lessons) =
        let n = length lessons
            nl' = if reset then 1 else nl
            ps = map (_+ nl') (upTo n)
            plessons = zipWith (λ {(lesson name) p → pos_lesson name p}) lessons ps
        in (nc + 1 , nl' + n , pos_chapter title reset nc plessons ∷ acc)

_ : solve input ≡ expected
_ = refl

max_stars_repo_name: eengineergz/Lambda

max_issues_repo_name: eengineergz/Lambda

max_forks_repo_name: eengineergz/Lambda