text:
module Data.Collection where

open import Data.Collection.Core public
open import Data.Collection.Equivalence
open import Data.Collection.Inclusion
open import Relation.Nullary

--------------------------------------------------------------------------------
--  Singleton
--------------------------------------------------------------------------------

singleton : String → Collection
singleton x = x ∷ []

--------------------------------------------------------------------------------
--  Delete
--------------------------------------------------------------------------------

delete : String → Collection → Collection
delete x [] = []
delete x (a ∷ A) with x ≟ a
delete x (a ∷ A) | yes p =     delete x A -- keep deleting, because there might be many of them
delete x (a ∷ A) | no ¬p = a ∷ delete x A

--------------------------------------------------------------------------------
--  Union
--------------------------------------------------------------------------------

union : Collection → Collection → Collection
union []      B = B
union (a ∷ A) B with a ∈? B
union (a ∷ A) B | yes p = union A B
union (a ∷ A) B | no ¬p = a ∷ union A B

--
-- open import Data.List
-- open import Data.String hiding (setoid)
-- open import Data.List using ([]; _∷_) public
-- open import Data.Product
-- open import Data.Sum renaming (map to mapSum)
-- -- open import Data.Bool using (Bool; true; false; T; not)
-- open import Level renaming (zero to lvl0)
-- open import Function using (_∘_; id; flip; _on_)
-- open import Function.Equivalence using (_⇔_; Equivalence; equivalence)
--
-- open import Function.Equality using (_⟨$⟩_) renaming (cong to cong≈)
-- open import Relation.Nullary
-- open import Relation.Unary
-- open import Relation.Nullary.Negation
-- open import Relation.Nullary.Decidable renaming (map to mapDec; map′ to mapDec′)
-- open import Relation.Binary hiding (_⇒_)
-- open import Relation.Binary.PropositionalEquality
-- -- open ≡-Reasoning
--
--
-- -- I know this notation is a bit confusing
-- _⊈_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
-- P ⊈ Q = ∀ {x} → x ∉ P → x ∉ Q
--
--
-- ⊆-IsPreorder : IsPreorder _≋_ _⊆_
-- ⊆-IsPreorder = record
--     { isEquivalence = {!   !}
--     ; reflexive = {!   !}
--     ; trans = {!   !}
--     }
--
--
-- []-empty : Empty c[ [] ]
-- []-empty = λ x → λ ()
--
-- here-respects-≡ : ∀ {A} → (λ x → x ∈ c[ A ]) Respects _≡_
-- here-respects-≡ refl = id
--
-- there-respects-≡ : ∀ {x A} → (λ a → x ∈ c[ a ∷ A ]) Respects _≡_
-- there-respects-≡ refl = id
--
-- ∈-respects-≡ : ∀ {x} → (λ P → x ∈ c[ P ]) Respects _≡_
-- ∈-respects-≡ refl = id
--
-- there-if-not-here : ∀ {x a A} → x ≢ a → x ∈ c[ a ∷ A ] → x ∈ c[ A ]
-- there-if-not-here x≢a here          = contradiction refl x≢a
-- there-if-not-here x≢a (there x∈a∷A) = x∈a∷A
--
-- here-if-not-there : ∀ {x a A} → x ∉ c[ A ] → x ∈ c[ a ∷ A ] → x ≡ a
-- here-if-not-there x∉A here = refl
-- here-if-not-there x∉A (there x∈A) = contradiction x∈A x∉A

--
-- map-¬∷ : ∀ {x a A B} → (x ∉ c[ A ] → x ∉ c[ B ]) → x ≢ a → x ∉ c[ a ∷ A ] → x ∉ c[ a ∷ B ]
-- map-¬∷ f x≢x x∉a∷A here = contradiction refl x≢x
-- map-¬∷ f x≢a x∉a∷A (there x∈B) = f (x∉a∷A ∘ there) x∈B
--
-- still-not-there : ∀ {x y} A → x ≢ y → x ∉ c[ A ] → x ∉ c[ y ∷ A ]
-- still-not-there [] x≢y x∉[y] here = x≢y refl
-- still-not-there [] x≢y x∉[y] (there ())
-- still-not-there (a ∷ A) x≢y x∉a∷A here = x≢y refl
-- still-not-there (a ∷ A) x≢y x∉a∷A (there x∈a∷A) = x∉a∷A x∈a∷A
--
-- --------------------------------------------------------------------------------
-- --  Union
-- --------------------------------------------------------------------------------
--
-- union : Collection → Collection → Collection
-- union []      B = B
-- union (a ∷ A) B with a ∈? B
-- union (a ∷ A) B | yes p = union A B
-- union (a ∷ A) B | no ¬p = a ∷ union A B
--
-- in-right-union : ∀ A B → c[ B ] ⊆ c[ union A B ]
-- in-right-union []      B x∈B = x∈B
-- in-right-union (a ∷ A) B x∈B with a ∈? B
-- in-right-union (a ∷ A) B x∈B | yes p = in-right-union A B x∈B
-- in-right-union (a ∷ A) B x∈B | no ¬p = there (in-right-union A B x∈B)
--
-- in-left-union : ∀ A B → c[ A ] ⊆ c[ union A B ]
-- in-left-union []      B ()
-- in-left-union (a ∷ A) B x∈A         with a ∈? B
-- in-left-union (a ∷ A) B here        | yes p = in-right-union A B p
-- in-left-union (a ∷ A) B (there x∈A) | yes p = in-left-union A B x∈A
-- in-left-union (a ∷ A) B here        | no ¬p = here
-- in-left-union (a ∷ A) B (there x∈A) | no ¬p = there (in-left-union A B x∈A)
--
-- ∪-left-identity : ∀ A → c[ [] ] ∪ c[ A ] ≋ c[ A ]
-- ∪-left-identity A = equivalence to inj₂
--     where
--             to : c[ [] ] ∪ c[ A ] ⊆ c[ A ]
--             to (inj₁ ())
--             to (inj₂ ∈A) = ∈A
--
-- ∪-right-identity : ∀ A → c[ A ] ∪ c[ [] ] ≋ c[ A ]
-- ∪-right-identity A = equivalence to inj₁
--     where
--             to : c[ A ] ∪ c[ [] ] ⊆ c[ A ]
--             to (inj₁ ∈A) = ∈A
--             to (inj₂ ())
--
-- in-either : ∀ A B → c[ union A B ] ⊆ c[ A ] ∪ c[ B ]
-- in-either []      B x∈A∪B         = inj₂ x∈A∪B
-- in-either (a ∷ A) B x∈A∪B         with a ∈? B
-- in-either (a ∷ A) B x∈A∪B         | yes p = mapSum there id (in-either A B x∈A∪B)
-- in-either (a ∷ A) B here          | no ¬p = inj₁ here
-- in-either (a ∷ A) B (there x∈A∪B) | no ¬p = mapSum there id (in-either A B x∈A∪B)
--
-- ∪-union : ∀ A B → c[ A ] ∪ c[ B ] ≋ c[ union A B ]
-- ∪-union A B = equivalence to (in-either A B)
--     where   to : ∀ {x} → x ∈ c[ A ] ∪ c[ B ] → x ∈ c[ union A B ]
--             to (inj₁ ∈A) = in-left-union A B ∈A
--             to (inj₂ ∈B) = in-right-union A B ∈B
--
-- -- map-⊆-union : ∀ {A B C} → c[ A ] ⊆ c[ B ] → c[ B ] ⊆ c[ C ] → c[  ] ⊆ c[ union C D ]
-- -- map-⊆-union f g ∈union = {!   !}
--
--
-- union-branch-1 : ∀ {x a} A B → a ∈ c[ B ] → x ∈ c[ union (a ∷ A) B ] → x ∈ c[ union A B ]
-- union-branch-1 {x} {a} A B a∈B x∈union with a ∈? B
-- union-branch-1 A B a∈B x∈union | yes p = x∈union
-- union-branch-1 A B a∈B x∈union | no ¬p = contradiction a∈B ¬p
--
-- there-left-union-coherence : ∀ {x} {a} A B → x ∈ c[ a ∷ A ] → x ∈c a ∷ union A B
-- there-left-union-coherence A B here          = here
-- there-left-union-coherence A B (there x∈a∷A) = there (in-left-union A B x∈a∷A)
--
--
-- in-neither : ∀ {x} A B → x ∉c union A B → x ∉ c[ A ] × x ∉ c[ B ]
-- in-neither []      B x∉A∪B = (λ ()) , x∉A∪B
-- in-neither (a ∷ A) B x∉A∪B with a ∈? B
-- in-neither (a ∷ A) B x∉A∪B | yes a∈B = (contraposition (union-branch-1 A B a∈B ∘ in-left-union (a ∷ A) B) x∉A∪B) , (contraposition (in-right-union A B) x∉A∪B)
-- in-neither (a ∷ A) B x∉A∪B | no a∉B = (contraposition (there-left-union-coherence A B) x∉A∪B) , contraposition (there ∘ in-right-union A B) x∉A∪B
--
--
-- delete : String → Collection → Collection
-- delete x [] = []
-- delete x (a ∷ A) with x ≟ a
-- delete x (a ∷ A) | yes p =     delete x A -- keep deleting, because there might be many of them
-- delete x (a ∷ A) | no ¬p = a ∷ delete x A
--
-- ∉-after-deleted : ∀ x A → x ∉ c[ delete x A ]
-- ∉-after-deleted x [] ()
-- ∉-after-deleted x (a ∷ A) with x ≟ a
-- ∉-after-deleted x (a ∷ A) | yes p = ∉-after-deleted x A
-- ∉-after-deleted x (a ∷ A) | no ¬p = still-not-there (delete x A) ¬p (∉-after-deleted x A)
--
--
-- still-∈-after-deleted : ∀ {x} y A → x ≢ y → x ∈ c[ A ] → x ∈ c[ delete y A ]
-- still-∈-after-deleted y []       x≢y ()
-- still-∈-after-deleted y (a  ∷ A) x≢y x∈A with y ≟ a
-- still-∈-after-deleted y (.y ∷ A) x≢y x∈A | yes refl = still-∈-after-deleted y A x≢y (there-if-not-here x≢y x∈A)
-- still-∈-after-deleted y (a  ∷ A) x≢y x∈A | no ¬p    = ∷-⊆-monotone {!   !} {! x∈A  !}
-- -- still-∈-after-deleted y (a  ∷ A) x≢y x∈A | no ¬p    = ∷-⊆-monotone (still-∈-after-deleted y A x≢y) x∈A
--
-- -- still-∉-after-deleted : ∀ {x} y A → x ≢ y → x ∉ c[ A ] → x ∉ c[ delete y A ]
-- -- still-∉-after-deleted y []       x≢y x∉A = x∉A
-- -- still-∉-after-deleted y (a  ∷ A) x≢y x∉A with y ≟ a
-- -- still-∉-after-deleted y (.y ∷ A) x≢y x∉A | yes refl = still-∉-after-deleted y A x≢y (x∉A ∘ there)
-- -- still-∉-after-deleted {x} y (a  ∷ A) x≢y x∉A | (no ¬p) with x ≟ a
-- -- still-∉-after-deleted y (x ∷ A) x≢y x∉A | no ¬p | yes refl = contradiction here x∉A
-- -- still-∉-after-deleted y (a ∷ A) x≢y x∉A | no ¬p | no ¬q = map-¬∷ (still-∉-after-deleted y A x≢y) ¬q x∉A
-- --
-- -- still-∉-after-recovered : ∀ {x} y A → x ≢ y → x ∉c delete y A → x ∉ c[ A ]
-- -- still-∉-after-recovered     y []      x≢y x∉deleted ()
-- -- still-∉-after-recovered     y (a  ∷ A) x≢y x∉deleted x∈a∷A with y ≟ a
-- -- still-∉-after-recovered     y (.y ∷ A) x≢y x∉deleted x∈a∷A | yes refl = still-∉-after-recovered y A x≢y x∉deleted (there-if-not-here x≢y x∈a∷A)
-- -- still-∉-after-recovered {x} y (a  ∷ A) x≢y x∉deleted x∈a∷A | no ¬p with x ≟ a
-- -- still-∉-after-recovered     y (x  ∷ A) x≢y x∉deleted x∈a∷A | no ¬p | yes refl = contradiction here x∉deleted
-- -- still-∉-after-recovered     y (a  ∷ A) x≢y x∉deleted x∈a∷A | no ¬p | no ¬q = x∉deleted (∷-⊆-monotone (still-∈-after-deleted y A x≢y) x∈a∷A)
--
-- singleton : String → Collection
-- singleton x = x ∷ []
--
-- singleton-≡ : ∀ {x y} → x ∈ c[ singleton y ] → x ≡ y
-- singleton-≡ here = refl
-- singleton-≡ (there ())

max_stars_repo_name: banacorn/lambda-calculus

max_issues_repo_name: banacorn/lambda-calculus

max_forks_repo_name: banacorn/lambda-calculus


text:
module Numeral.Natural.Oper.Proofs.Rewrite where

import Lvl
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Induction
open import Relator.Equals
open import Relator.Equals.Proofs
open import Syntax.Function

private variable x y : ℕ

[+]-baseₗ : 𝟎 + y ≡ y
[+]-baseₗ {x} = ℕ-elim [≡]-intro (x ↦ [≡]-with(𝐒) {𝟎 + x}{x}) x
{-# REWRITE [+]-baseₗ #-}

[+]-baseᵣ : x + 𝟎 ≡ x
[+]-baseᵣ = [≡]-intro

[+]-stepₗ : 𝐒(x) + y ≡ 𝐒(x + y)
[+]-stepₗ {x}{y} = ℕ-elim [≡]-intro (i ↦ [≡]-with(𝐒) {𝐒(x) + i} {x + 𝐒(i)}) y
{-# REWRITE [+]-stepₗ #-}

[+]-stepᵣ : x + 𝐒(y) ≡ 𝐒(x + y)
[+]-stepᵣ = [≡]-intro

ext: agda

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Numeral.PositiveInteger where

import Lvl
open import Syntax.Number
open import Data.Boolean.Stmt
open import Functional
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural as ℕ using (ℕ)
open import Type

data ℕ₊ : Type{Lvl.𝟎} where
 𝟏 : ℕ₊
 𝐒 : ℕ₊ → ℕ₊

ℕ₊-to-ℕ : ℕ₊ → ℕ
ℕ₊-to-ℕ (𝟏)    = ℕ.𝐒(ℕ.𝟎)
ℕ₊-to-ℕ (𝐒(n)) = ℕ.𝐒(ℕ₊-to-ℕ (n))

ℕ-to-ℕ₊ : (n : ℕ) → ⦃ _ : IsTrue(positive?(n)) ⦄ → ℕ₊
ℕ-to-ℕ₊ (ℕ.𝟎)         ⦃ ⦄
ℕ-to-ℕ₊ (ℕ.𝐒(ℕ.𝟎))    ⦃ _ ⦄ = 𝟏
ℕ-to-ℕ₊ (ℕ.𝐒(ℕ.𝐒(x))) ⦃ p ⦄ = 𝐒(ℕ-to-ℕ₊ (ℕ.𝐒(x)) ⦃ p ⦄)

instance
  ℕ₊-numeral : Numeral(ℕ₊)
  Numeral.restriction-ℓ (ℕ₊-numeral) = Lvl.𝟎
  Numeral.restriction   (ℕ₊-numeral) (n) = IsTrue(positive?(n))
  num ⦃ ℕ₊-numeral ⦄ (n) ⦃ proof ⦄ = ℕ-to-ℕ₊ (n) ⦃ proof ⦄

𝐒-from-ℕ : ℕ → ℕ₊
𝐒-from-ℕ (ℕ.𝟎)    = 𝟏
𝐒-from-ℕ (ℕ.𝐒(n)) = 𝐒(𝐒-from-ℕ(n))

𝐏-to-ℕ : ℕ₊ → ℕ
𝐏-to-ℕ (𝟏)    = ℕ.𝟎
𝐏-to-ℕ (𝐒(n)) = ℕ.𝐒(𝐏-to-ℕ(n))


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

open import LogicalFormulae

module Functions.Definition where

Rel : {a b : _} → Set a → Set (a ⊔ lsuc b)
Rel {a} {b} A = A → A → Set b

_∘_ : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → (f : B → C) → (g : A → B) → (A → C)
g ∘ f = λ a → g (f a)

Injection : {a b : _} {A : Set a} {B : Set b} (f : A → B) → Set (a ⊔ b)
Injection {A = A} f = {x y : A} → (f x ≡ f y) → x ≡ y

Surjection : {a b : _} {A : Set a} {B : Set b} (f : A → B) → Set (a ⊔ b)
Surjection {A = A} {B = B} f = (b : B) → Sg A (λ a → f a ≡ b)

record Bijection {a b : _} {A : Set a} {B : Set b} (f : A → B) : Set (a ⊔ b) where
  field
    inj : Injection f
    surj : Surjection f

record Invertible {a b : _} {A : Set a} {B : Set b} (f : A → B) : Set (a ⊔ b) where
  field
    inverse : B → A
    isLeft : (b : B) → f (inverse b) ≡ b
    isRight : (a : A) → inverse (f a) ≡ a

id : {a : _} {A : Set a} → (A → A)
id a = a

dom : {a b : _} {A : Set a} {B : Set b} (f : A → B) → Set a
dom {A = A} f = A

codom : {a b : _} {A : Set a} {B : Set b} (f : A → B) → Set b
codom {B = B} f = B


text:
-- This is a selection of useful function
-- from the standard library that we tend to use a lot.
module Prelude where

  open import Data.Nat
    hiding (_⊔_)
    public

  open import Level
    renaming (suc to lsuc; zero to ℓ0)
    public

  open import Relation.Binary.PropositionalEquality
    renaming ([_] to Reveal[_] )
    public

  open import Relation.Unary
    public

  open import Data.Unit
    using (⊤; tt)
    public

  open import Data.Sum
    public

  open import Data.Nat.Properties
    public

  open import Relation.Nullary
    hiding (Irrelevant)
    public

  open import Data.Product
    using (_×_; proj₁; proj₂; Σ; _,_; ∃; Σ-syntax; ∃-syntax)
    public

  open import Data.Empty
    using (⊥; ⊥-elim)
    public

  open import Function
    using (_∘_)
    public

  open import Data.List.Relation.Unary.Any
    using (Any; here; there)
    public

max_stars_repo_name: lisandrasilva/agda-liveness

max_issues_repo_name: lisandrasilva/agda-liveness

max_forks_repo_name: lisandrasilva/agda-liveness


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Agda.Primitive using (Level)
module Tutorials.Monday where

-- Two dashes to comment out the rest of the line
{-
  Opening {-
  and closing -}
  for a multi-line comment
-}

-- In Agda all the tokens are tokenised using whitespace (with the exception of parentheses and some other symbols)
-- Agda offers unicode support
-- We can input unicode using the backslash \ and (most of the time) typing what one would type in LaTeX
-- If in emacs, we can put the cursor over a characted and use M-x describe-char to see how that character is inputted
-- ⊥ is written using \bot
data ⊥ : Set where
  -- AKA the empty set, bottom, falsehood, the absurd type, the empty type, the initial object
  -- ⊥ : Set means ⊥ is a Type (Set = Type, for historical reasons)
  -- The data keyword creates a data type where we list all the constructors of the types
  -- ⊥ has no constructors: there is no way of making something of type ⊥

record ⊤ : Set where
  -- AKA the singleton set, top, truth, the trivial type, the unit type, the terminal object
  -- The record keyword creates a record type
  -- Records have a single constructor
  -- To create a record you must populate all of its fields
  -- ⊤ has no fields: it is trivial to make one, and contains no information
  constructor tt

data Bool : Set where
  -- Bool has two constructors: one bit worth of information
  true : Bool
  false : Bool

--------
-- Simple composite types
--------

module Simple where
  record _×_ (A : Set) (B : Set) : Set where
    -- AKA logical and, product type

    -- Agda offers support for mixfix notation
    -- We use the underscores to specify where the arguments goal
    -- In this case the arguments are the type parameters A and B, so we can write A × B

    -- A × B models a type packing up *both* an A *and* a B
    -- A and B are type parameters, both of type Set, i.e. types
    -- A × B itself is of type Set, i.e. a type
    -- We use the single record constructor _,_ to make something of type A × B
    -- The constructor _,_ takes two parameters: the fields fst and snd, of type A and B, respectively
    -- If we have a of type A and b of type B, then (a , b) is of type A × B
    constructor _,_
    field
      fst : A
      snd : B

  -- Agda has a very expressive module system (more on modules later)
  -- Every record has a module automatically attached to it
  -- Opening a record exposes its constructor and it fields
  -- The fields are projection functions out of the record
  -- In the case of _×_, it exposes
  -- fst : A × B → A
  -- snd : A × B → B
  open _×_

  data _⊎_ (A B : Set) : Set where
    -- AKA logical or, sum type, disjoint union
    -- A ⊎ B models a type packing *either* an A *or* a B
    -- A and B are type parameters, both of type Set, i.e. types
    -- A ⊎ B itself is of type Set, i.e. a type
    -- A ⊎ B has two constructors: inl and inr
    -- The constructor inl takes something of type A as an argument and returns something of type A ⊎ B
    -- The constructor inr takes something of type B as an argument and returns something of type A ⊎ B
    -- We can make something of type A ⊎ B either by using inl and supplying an A, or by using inr and supplying a B
    inl : A → A ⊎ B
    inr : B → A ⊎ B

  --------
  -- Some simple proofs!
  --------

  -- In constructive mathematics logical implication is modelled as function types
  -- An object of type A → B shows that assuming an object of type A, we can construct an object of type B
  -- Below we want to show that assuming an object of type A × B, we can construct an object of type A
  -- We want to show that this is the case regardless of what A and B actually are
  -- We do this using a polymorphic function that is parametrised over A and B, both of type Set
  -- We use curly braces {} to make these function parameters implicit
  -- When we call this function we won't have to supply the arguments A and B unless we want to
  -- When we define this function we won't have to accept A and B as arguments unless we want to
  -- The first line below gives the type of the function get-fst
  -- The second line gives its definition
  get-fst : {A : Set} {B : Set} → A × B → A
  get-fst x = {!!}

  -- Agda is an *interactive* proof assistant
  -- We don't provide our proofs/programs all at once: we develop them iteratively
  -- We write ? where we don't yet have a program to provide, and we reload the file
  -- What we get back is a hole where we can place the cursor and have a conversation with Agda
  -- ctrl+c is the prefix that we use to communicate with Agda
  -- ctrl+c ctrl+l     reload the file
  -- ctrl+c ctrl+,     shows the goal and the context
  -- ctrl+c ctrl+.     shows the goal, the context, and what we have so far
  -- ctrl+c ctrl+c     pattern matches against a given arguments
  -- ctrl+c ctrl+space fill in hole
  -- ctrl+c ctrl+r     refines the goal: it will ask Agda to insert the first constructor we need
  -- ctrl+c ctrl+a     try to automatically fulfill the goal
  -- key bindings: https://agda.readthedocs.io/en/v2.6.1.3/getting-started/quick-guide.html
  get-snd : ∀ {A B} → A × B → B
  get-snd x = {!!}

  -- The variable keyword enables us to declare convention for notation
  -- Unless said otherwise, whenever we refer to A, B or C and these are not bound, we will refer to objects of type Set
  variable
    ℓ : Level
    A B C : Set ℓ

  -- Notice how we don't have to declare A, B and C anymore
  curry : (A → B → C) → (A × B → C)
  curry f = {!!}

  uncurry : (A × B → C) → (A → B → C)
  uncurry f = {!!}

  ×-comm : A × B → B × A
  ×-comm = {!!}

  ×-assoc : (A × B) × C → A × (B × C)
  ×-assoc = {!!}

  -- Pattern matching has to be exhaustive: all cases must be addressed
  ⊎-comm : A ⊎ B → B ⊎ A
  ⊎-comm = {!!}

  ⊎-assoc : (A ⊎ B) ⊎ C → A ⊎ (B ⊎ C)
  ⊎-assoc = {!!}

  -- If there are no cases to be addressed there is nothing for us left to do
  -- If you believe ⊥ exist you believe anything
  absurd : ⊥ → A
  absurd a = {!!}

  -- In constructive mathematics all proofs are constructions
  -- How do we show that an object of type A cannot possibly be constructed, while using a construction to show so?
  -- We take the cannonically impossible-to-construct object ⊥, and show that if we were to assume the existence of A, we could use it to construct ⊥
  ¬_ : Set ℓ → Set ℓ
  ¬ A = A → ⊥

  -- In classical logic double negation can be eliminated: ¬ ¬ A ⇒ A
  -- That is however not the case in constructive mathematics:
  -- The proof ¬ ¬ A is a function that takes (A → ⊥) into ⊥, and offers no witness for A
  -- The opposite direction is however constructive:
  ⇒¬¬ : A → ¬ ¬ A
  ⇒¬¬ = {!!}

  -- Moreover, double negation can be eliminated from non-witnesses
  ¬¬¬⇒¬ : ¬ ¬ ¬ A → ¬ A
  ¬¬¬⇒¬ = {!!}

  -- Here we have a choice of two programs to write
  ×-⇒-⊎₁ : A × B → A ⊎ B
  ×-⇒-⊎₁ = {!!}

  ×-⇒-⊎₂ : A × B → A ⊎ B
  ×-⇒-⊎₂ = {!!}

  -- A little more involved
  -- Show that the implication (A ⊎ B → A × B) is not always true for all A and Bs
  ⊎-⇏-× : ¬ (∀ {A B} → A ⊎ B → A × B)
  ⊎-⇏-× f = {!!}

variable
  ℓ : Level
  A B C : Set ℓ

--------
-- Inductive data types
--------

data ℕ : Set where
  -- The type of unary natural numbers
  -- The zero constructor takes no arguments; the base case
  -- The suc constructor takes one argument: an existing natural number; the inductive case
  -- We represent natural numbers by using ticks: ||| ≈ 3
  -- zero: no ticks
  -- suc: one more tick
  -- suc (suc (suc zero)) ≈ ||| ≈ 3
  zero : ℕ
  suc  : ℕ → ℕ

three : ℕ
three = suc (suc (suc zero))

-- Compiler pragmas allow us to give instructions to Agda
-- They are introduced with an opening {-# and a closing #-}
-- Here we the pragma BUILTIN to tell Agda to use ℕ as the builtin type for natural numbers
-- This allows us to say 3 instead of suc (suc (suc zero))
{-# BUILTIN NATURAL ℕ #-}
three' : ℕ
three' = 3

-- Whenever we say n or m and they haven't been bound, they refer to natural numbers
variable
  n m l : ℕ

-- Brief interlude: we declare the fixity of certain functions
-- By default, all definitions have precedence 20
-- The higher the precedence, the tighter they bind
-- Here we also declare that _+_ is left associative, i.e. 1 + 2 + 3 is parsed as (1 + 2) + 3
infixl 20 _+_

-- Define addition of natural numbers by structural recursion
_+_ : ℕ → ℕ → ℕ
x + y = {!!}

-- In functions recursion must always occur on structurally smaller values (otherwise the computation might never terminate)
-- In Agda *all computations must terminate*
-- We can tell Agda to ignore non-termination with this pragma
{-# TERMINATING #-}
non-terminating : ℕ → ℕ
non-terminating n = non-terminating n

-- However, doing so would allow us to define elements of the type ⊥
-- This is not considered safe: running Agda with the --safe option will make type-checking fail
{-# TERMINATING #-}
loop : ⊥
loop = loop

-- Use structural recursion to define multiplication
_*_ : ℕ → ℕ → ℕ
x * y = {!!}

-- The module keyword allows us to define modules (namespaces)
module List where
  infixr 15 _∷_ _++_
  data List (A : Set) : Set where
    -- Lists are another example of inductive types
    -- The type parameter A is the type of every element in the list
    -- They are like natural numbers, but the successor case contains an A
    []  : List A
    _∷_ : A → List A → List A

  -- List concatenation by structural recursion
  _++_ : List A → List A → List A
  [] ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

  -- Apply a function (A → B) to every element of a list
  map : (A → B) → List A → List B
  map = {!!}

  -- A base case B and an inductive case A → B → B is all we need to take a List A and make a B
  foldr : (A → B → B) → B → List A → B
  foldr f b [] = b
  foldr f b (x ∷ xs) = f x (foldr f b xs)

--------
-- Dependent Types
--------

-- Dependent types are types that depend on values, objects of another type
-- Dependent types allow us to model predicates on types
-- A predicate P on a type A is a function taking elements of A into types
Pred : Set → Set₁
Pred A = A → Set

-- Let us define a predicate on ℕ that models the even numbers
-- Even numbers are taken to the type ⊤, which is trivial to satisfy
-- Odd numbers are taken to the type ⊥, which is impossible to satisfy
Even : Pred ℕ
Even x = {!!}

-- We can now use Even as a precondition on a previous arguments
-- Here we bind the first argument of type ℕ to the name n
-- We then use n as an argument to the type Even
-- As we expose the constructors of n, Even will compute
half : (n : ℕ) → Even n → ℕ
half n n-even = {!!}

-- There is an alternative way of definiting dependent types
-- EvenData is a data type indexed by elements of the type ℕ
-- That is, for every (n : ℕ), EvenData n is a type
-- The constructor zero constructs an element of the type EvenData zero
-- The constructor 2+_ takes an element of the type EvenData n and constructs one of type EvenData (suc (suc n))
-- Note that there is no constructors that constructs elements of the type Evendata (suc zero)
data EvenData : ℕ → Set where -- Pred ℕ
  zero : EvenData zero
  2+_  : EvenData n → EvenData (suc (suc n))

-- We can use EvenData as a precondition too
-- The difference is that while Even n computes automatically, we have to take EvenData n appart by pattern matching
-- It leaves a trace of *why* n is even
half-data : (n : ℕ) → EvenData n → ℕ
half-data n n-even = {!!}

-- Function composition: (f ∘ g) composes two functions f and g
-- The result takes the input, feeds it through g, then feeds the result through f
infixr 20 _∘_
_∘_ : (B → C) → (A → B) → (A → C)
(f ∘ g) x = f (g x)

--------
-- Example of common uses of dependent types
--------

module Fin where
  -- The type Fin n has n distinct inhabitants
  data Fin : ℕ → Set where
    zero : Fin (suc n)
    suc  : Fin n → Fin (suc n)

  -- Note that there is no constructor for Fin zero
  Fin0 : Fin zero → ⊥
  Fin0 x = {!!}

  -- We can erase the type level information to get a ℕ back
  to-ℕ : Fin n → ℕ
  to-ℕ zero = zero
  to-ℕ (suc x) = suc (to-ℕ x)

module Vec where
  open Fin

  -- Vectors are like lists, but they keep track of their length
  -- The type Vec A n is the type of lists of length n containing values of type A
  -- Notice that while A is a parameter (remains unchanged in all constructors), n is an index
  -- We can bind parameters to names (since they don't change) but we cannot bind indices
  data Vec (A : Set) : ℕ → Set where
    []  : Vec A zero
    _∷_ : A → Vec A n → Vec A (suc n)

  -- Now we can define concatenation, but giving more assurances about the resulting length
  _++_ : Vec A n → Vec A m → Vec A (n + m)
  xs ++ ys = {!!}

  map : (A → B) → Vec A n → Vec B n
  map = {!!}

  -- Given a vector and a fin, we can use the latter as a lookup index into the former
  -- Question: what happens if there vector is empty?
  _!_ : Vec A n → Fin n → A
  xs ! i = {!!}

  -- A vector Vec A n is just the inductive form of a function Fin n → A
  tabulate : ∀ {n} → (Fin n → A) → Vec A n
  tabulate {n = zero}  f = []
  tabulate {n = suc n} f = f zero ∷ tabulate (f ∘ suc)

  untabulate : Vec A n → (Fin n → A)
  untabulate [] ()
  untabulate (x ∷ xs) zero = x
  untabulate (x ∷ xs) (suc i) = untabulate xs i

-- Predicates need not be unary, they can be binary! (i.e. relations)
Rel : Set → Set₁
Rel A = A → A → Set

-- Question: how many proofs are there for any n ≤ m
data _≤_ : Rel ℕ where
  z≤n :         zero  ≤ n
  s≤s : n ≤ m → suc n ≤ suc m

_<_ : ℕ → ℕ → Set
n < m = suc n ≤ m

-- _≤_ is reflexive and transitive
≤-refl : ∀ n → n ≤ n
≤-refl n = {!!}

≤-trans : n ≤ m → m ≤ l → n ≤ l
≤-trans a b = {!!}

-----------
-- Propositional Equality
-----------

-- Things get interesting: we can use type indices to define propositional equality
-- For any (x y : A) the type x ≡ y is a proof showing that x and y are in fact definitionally equal
-- It has a single constructor refl which limits the ways of making something of type x ≡ y to those where x and y are in fact the same, i.e. x ≡ x
-- When we pattern match against something of type x ≡ y, the constructor refl will make x and y unify: Agda will internalise the equality
infix 10 _≡_
-- \== ≡
data _≡_ (x : A) : A → Set where
  refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}

-- Definitional equality holds when the two sides compute to the same symbols
2+2≡4 : 2 + 2 ≡ 4
2+2≡4 = {!!}

-- Because of the way in which defined _+_, zero + x ≡ x holds definitionally (the first case in the definition)
+-idˡ : ∀ x → (zero + x) ≡ x
+-idˡ x = {!!}

-- We show that equality respects congruence
cong : {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
cong f p = {!!}

-- However this does not hold definitionally
-- We need to use proof by induction
-- We miss some pieces to prove this
+-idʳ : ∀ x → (x + zero) ≡ x
+-idʳ x = {!!}

-- Propositional equality is reflexive by construction, here we show it is also symmetric and transitive
sym : {x y : A} → x ≡ y → y ≡ x
sym p = {!!}

trans : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans p q = {!!}

-- A binary version that will come in use later on
cong₂ : {x y : A} {w z : B} (f : A → B → C) → x ≡ y → w ≡ z → f x w ≡ f y z
cong₂ f refl refl = refl

-- Leibniz equality, transport
subst : {x y : A} {P : Pred A} → x ≡ y → P x → P y
subst eq p = {!!}

-- Now we can start proving slightly more interesting things!
+-assoc : ∀ x y z → (x + y) + z ≡ x + (y + z)
+-assoc x y z = {!!}

-- Introduce underscores on the RHS
+-comm : ∀ x y → x + y ≡ y + x
+-comm x zero = {!!}
+-comm x (suc y) = {!!}
  -- The keyword where allows us to introduce local definitions
  where
  +-suc : ∀ x y → x + suc y ≡ suc (x + y)
  +-suc x y = {!!}

-----------
-- Some tooling for equational reasoning
-----------

infix  3 _∎
infixr 2 step-≡
infix  1 begin_

begin_ : ∀{x y : A} → x ≡ y → x ≡ y
begin_ x≡y = x≡y

step-≡ : ∀ (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
step-≡ _ y≡z x≡y = trans x≡y y≡z

syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z

_∎ : ∀ (x : A) → x ≡ x
_∎ _ = refl

-- The equational resoning style allows us to explicitly write down the goals at each stage
-- This starts to look like what one would do on the whiteboard
+-comm′ : ∀ x y → x + y ≡ y + x
+-comm′ x zero = {!!}
+-comm′ x (suc y) = begin
  (x + suc y)  ≡⟨ {!!} ⟩
  suc (x + y)  ≡⟨ {!!} ⟩
  suc (y + x)  ∎

max_stars_repo_name: poncev/agda-bcam

max_issues_repo_name: poncev/agda-bcam

max_forks_repo_name: poncev/agda-bcam


text:
module map-Tree where

-- ツリー
data Tree (A B : Set) : Set where
  leaf : A → Tree A B
  node : Tree A B → B → Tree A B → Tree A B

-- ツリーのmap
map-Tree : ∀ {A B C D : Set} → (A → C) → (B → D) → Tree A B → Tree C D
map-Tree f g (leaf a)             = leaf (f a)
map-Tree f g (node treeˡ b treeʳ) = node (map-Tree f g treeˡ) (g b) (map-Tree f g treeʳ)

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


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

open import Base
open import Homotopy.PullbackDef

module Homotopy.PullbackIsPullback {i} (d : pullback-diag i) where

open pullback-diag d

import Homotopy.PullbackUP as PullbackUP
open PullbackUP d (λ _ → unit)

pullback-cone : cone (pullback d)
pullback-cone = (pullback.a d , pullback.b d , pullback.h d)

factor-pullback : (E : Set i) → (cone E → (E → pullback d))
factor-pullback E (top→A , top→B , h) x = (top→A x , top→B x , h x)

pullback-is-pullback : is-pullback (pullback d) pullback-cone
pullback-is-pullback E = iso-is-eq _
  (factor-pullback E)
  (λ y → refl)
  (λ f → refl)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module GUIgeneric.GUIExampleLib where

open import GUIgeneric.Prelude  hiding (addButton)

open import GUIgeneric.GUIDefinitions renaming (add to add'; add' to add)
open import GUIgeneric.GUI

executeChangeGui : ∀{i} → (fr : FFIFrame)(mvar : MVar StateAndGuiObj)
                          (mvarFFI : MVar StateAndFFIComp)
                          (let state = addVar mvar (SingleMVar mvarFFI))
      → StateAndGuiObj × StateAndFFIComp →
      IOˢ GuiLev2Interface i (λ _ → prod state) state

executeChangeGui fr varO varFFI ((gNew , (prop , obj)) , (gOld , ffi)) =

  deleteComp gOld ffi >>=ₚˢ λ _ →
  reCreateFrame gNew fr >>=ₚˢ λ ffiNew →
  setHandlerG gNew ffiNew varO (SingleMVar varFFI)  >>=ₚˢ λ _ →

  (translateLev1toLev2 (setAttributes ∞ gNew prop ffiNew)) >>=ˢ λ _ _ →
  returnˢ ((gNew , (prop , obj)) , (gNew , ffiNew ))

setRightClick₃ : ∀{i} →
                      (g : Frame)
                      (ffiComp : FFIcomponents g)
                      (mvar : MVar StateAndGuiObj)
                      (mvarFFI : MVar StateAndFFIComp)
                      (getFr : FFIcomponents g → FFIFrame)
                      (let state = addVar mvar (SingleMVar mvarFFI))
                      → IOˢ GuiLev3Interface i (λ s → s ≡ state × Unit) state

setRightClick₃ g ffi mvar mvarFFI getFr =
  doˢ (setRightClick (getFr ffi)
                     (executeChangeGui (getFr ffi) mvar mvarFFI ∷ [])) λ r →
  returnˢ (refl , _)

setCustomEvent₃ : ∀{i} →
                      (g : Frame)
                      (ffiComp : FFIcomponents g)
                      (mvar : MVar StateAndGuiObj)
                      (mvarFFI : MVar StateAndFFIComp)
                      (getFr : FFIcomponents g → FFIFrame)
                      (let state = addVar mvar (SingleMVar mvarFFI))
                      → IOˢ GuiLev3Interface i (λ s → s ≡ state × Unit) state

setCustomEvent₃ g ffi mvar mvarFFI getFr =
  doˢ (setCustomEvent (getFr ffi)
                     (executeChangeGui (getFr ffi) mvar mvarFFI ∷ [])) λ r →
  returnˢ (refl , _)

mainGeneric : (g : Frame)(a : properties g)(o : HandlerObject ∞ g)(getFr : FFIcomponents g → FFIFrame)
           → IOˢ GuiLev3Interface ∞ (λ _ → Unit) []

mainGeneric g propDef objDef getFr =
 let _>>=_ = _>>=ₚˢ_
     createGUIElements = λ g → cmd3 (createFrame g)
     setAttributes = λ g prop ffi → cmd3 (translateLev1toLev2ₚ (setAttributes ∞ g prop ffi))

 in
 createGUIElements g         >>=  λ ffi →
 setAttributes g propDef ffi >>=  λ _ →

 cmd3 (initFFIMVar g ffi)                             >>=ₚsemiˢ λ mvaffi →

 cmd3 (initHandlerMVar (SingleMVar mvaffi) g propDef objDef)  >>=ₚsemiˢ λ mvar →
 cmd3 (setHandlerG g ffi mvar (SingleMVar mvaffi))    >>=ₚˢ λ _ →
 setCustomEvent₃ g ffi mvar mvaffi getFr              >>=ˢ λ _ _ →

  returnˢ _
    where
      cmd3 = translateLev2toLev3

compileProgram : (g : Frame)(a : properties g) (h : HandlerObject ∞ g)
                  → NativeIO Unit
compileProgram g a h  = start (translateLev3 (mainGeneric g a h (getFrameGen g)))

generateProgram = compileProgram

addButton : String → CompEls frame → (isOpt : IsOptimized) → CompEls frame
addButton str fr isOpt = add' buttonFrame (create-button str) fr isOpt

addTxtBox' : String → CompEls frame → (isOpt : IsOptimized) → CompEls frame
addTxtBox' str fr isOpt = add' buttonFrame (create-txtbox str) fr isOpt

record GUI {i : Size} : Set₁ where
   field
      defFrame  : Frame
      property  : properties defFrame
      obj       : HandlerObject i defFrame
open GUI public

guiFull2IOˢprog : GUI → IOˢ GuiLev3Interface ∞ (λ _ → Unit) []
guiFull2IOˢprog g = mainGeneric (g .defFrame) (g .property) (g .obj) (getFrameGen (g .defFrame))

compileGUI : GUI → NativeIO Unit
compileGUI g = start (translateLev3 (guiFull2IOˢprog g))

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:
import cedille-options
open import general-util
module spans (options : cedille-options.options) {mF : Set → Set} {{_ : monad mF}} where

open import lib
open import functions

open import cedille-types
open import constants
open import conversion
open import ctxt
open import is-free
open import syntax-util
open import to-string options
open import subst
open import erase
open import datatype-functions

--------------------------------------------------
-- span datatype
--------------------------------------------------

err-m : Set
err-m = maybe string

data span : Set where
  mk-span : string → posinfo → posinfo → 𝕃 tagged-val {- extra information for the span -} → err-m → span

span-to-rope : span → rope
span-to-rope (mk-span name start end extra nothing) =
  [[ "[\"" ^ name ^ "\"," ^ start ^ "," ^ end ^ ",{" ]] ⊹⊹ tagged-vals-to-rope 0 extra ⊹⊹ [[ "}]" ]]
span-to-rope (mk-span name start end extra (just err)) =
  [[ "[\"" ^ name ^ "\"," ^ start ^ "," ^ end ^ ",{" ]] ⊹⊹ tagged-vals-to-rope 0 (strRunTag "error" empty-ctxt (strAdd err) :: extra) ⊹⊹ [[ "}]" ]]

data error-span : Set where
  mk-error-span : string → posinfo → posinfo → 𝕃 tagged-val → string → error-span

data spans : Set where
  regular-spans : maybe error-span → 𝕃 span → spans
  global-error : string {- error message -} → maybe span → spans

is-error-span : span → 𝔹
is-error-span (mk-span _ _ _ _ err) = isJust err

get-span-error : span → err-m
get-span-error (mk-span _ _ _ _ err) = err

get-tagged-vals : span → 𝕃 tagged-val
get-tagged-vals (mk-span _ _ _ tvs _) = tvs

spans-have-error : spans → 𝔹
spans-have-error (regular-spans es ss) = isJust es
spans-have-error (global-error _ _) = tt

empty-spans : spans
empty-spans = regular-spans nothing []

𝕃span-to-rope : 𝕃 span → rope
𝕃span-to-rope (s :: []) = span-to-rope s
𝕃span-to-rope (s :: ss) = span-to-rope s ⊹⊹ [[ "," ]] ⊹⊹ 𝕃span-to-rope ss
𝕃span-to-rope [] = [[]]

spans-to-rope : spans → rope
spans-to-rope (regular-spans _ ss) = [[ "{\"spans\":["]] ⊹⊹ 𝕃span-to-rope ss ⊹⊹ [[ "]}" ]] where
spans-to-rope (global-error e s) =
  [[ global-error-string e ]] ⊹⊹ maybe-else [[]] (λ s → [[", \"global-error\":"]] ⊹⊹ span-to-rope s) s

print-file-id-table : ctxt → 𝕃 tagged-val
print-file-id-table (mk-ctxt mod (syms , mn-fn , mn-ps , fn-ids , id , id-fns) is os Δ) =
  h [] id-fns where
  h : ∀ {i} → 𝕃 tagged-val → 𝕍 string i → 𝕃 tagged-val
  h ts [] = ts
  h {i} ts (fn :: fns) = h (strRunTag "fileid" empty-ctxt (strAdd fn) :: ts) fns

add-span : span → spans → spans
add-span s@(mk-span dsc pi pi' tv nothing) (regular-spans es ss) =
  regular-spans es (s :: ss)
add-span s@(mk-span dsc pi pi' tv (just err)) (regular-spans es ss) =
  regular-spans (just (mk-error-span dsc pi pi' tv err)) (s :: ss)
add-span s (global-error e e') =
  global-error e e'

--------------------------------------------------
-- spanM, a state monad for spans
--------------------------------------------------

spanM : Set → Set
spanM A = ctxt → spans → mF (A × ctxt × spans)

-- return for the spanM monad
spanMr : ∀{A : Set} → A → spanM A
spanMr a Γ ss = returnM (a , Γ , ss)

spanMok : spanM ⊤
spanMok = spanMr triv

get-ctxt : ∀{A : Set} → (ctxt → spanM A) → spanM A
get-ctxt m Γ ss = m Γ Γ ss

set-ctxt : ctxt → spanM ⊤
set-ctxt Γ _ ss = returnM (triv , Γ , ss)

get-error : ∀ {A : Set} → (maybe error-span → spanM A) → spanM A
get-error m Γ ss@(global-error _ _) = m nothing Γ ss
get-error m Γ ss@(regular-spans nothing _) = m nothing Γ ss
get-error m Γ ss@(regular-spans (just es) _) = m (just es) Γ ss

set-error : maybe (error-span) → spanM ⊤
set-error es Γ ss@(global-error _ _) = returnM (triv , Γ , ss)
set-error es Γ (regular-spans _ ss) = returnM (triv , Γ , regular-spans es ss)

restore-def : Set
restore-def = maybe qualif-info × maybe sym-info

spanM-set-params : params → spanM ⊤
spanM-set-params ps Γ ss = returnM (triv , (ctxt-params-def ps Γ) , ss)

-- this returns the previous ctxt-info, if any, for the given variable
spanM-push-term-decl : posinfo → var → type → spanM restore-def
spanM-push-term-decl pi x t Γ ss = let qi = ctxt-get-qi Γ x in returnM ((qi , qi ≫=maybe λ qi → ctxt-get-info (fst qi) Γ) , ctxt-term-decl pi x t Γ , ss)

-- let bindings currently cannot be made opaque, so this is OpacTrans. -tony
spanM-push-term-def : posinfo → var → term → type → spanM restore-def
spanM-push-term-def pi x t T Γ ss = let qi = ctxt-get-qi Γ x in returnM ((qi , qi ≫=maybe λ qi → ctxt-get-info (fst qi) Γ) , ctxt-term-def pi localScope OpacTrans x (just t) T Γ , ss)

spanM-push-term-udef : posinfo → var → term → spanM restore-def
spanM-push-term-udef pi x t Γ ss = let qi = ctxt-get-qi Γ x in returnM ((qi , qi ≫=maybe λ qi → ctxt-get-info (fst qi) Γ) , ctxt-term-udef pi localScope OpacTrans x t Γ , ss)

 -- return previous ctxt-info, if any
spanM-push-type-decl : posinfo → var → kind → spanM restore-def
spanM-push-type-decl pi x k Γ ss = let qi = ctxt-get-qi Γ x in returnM ((qi , qi ≫=maybe λ qi → ctxt-get-info (fst qi) Γ) , ctxt-type-decl pi x k Γ , ss)

spanM-push-type-def : posinfo → var → type → kind → spanM restore-def
spanM-push-type-def pi x t T Γ ss = let qi = ctxt-get-qi Γ x in returnM ((qi , qi ≫=maybe λ qi → ctxt-get-info (fst qi) Γ) , ctxt-type-def pi localScope OpacTrans x (just t) T Γ , ss)

spanM-lookup-restore-info : var → spanM restore-def
spanM-lookup-restore-info x =
  get-ctxt λ Γ →
  let qi = ctxt-get-qi Γ x in
  spanMr (qi , qi ≫=maybe λ qi → ctxt-get-info (fst qi) Γ)

-- returns the original sym-info.
-- clarification is idempotent: if the definition was already clarified,
-- then the operation succeeds, and returns (just sym-info).
-- this only returns nothing in the case that the opening didnt make sense:
-- you tried to open a term def, you tried to open an unknown def, etc...
-- basically any situation where the def wasnt a "proper" type def
spanM-clarify-def : opacity → var → spanM (maybe sym-info)
spanM-clarify-def o x Γ ss = returnM (result (ctxt-clarify-def Γ o x))
  where
  result : maybe (sym-info × ctxt) → (maybe sym-info × ctxt × spans)
  result (just (si , Γ')) = ( just si , Γ' , ss )
  result nothing = ( nothing , Γ , ss )

spanM-restore-clarified-def : var → sym-info → spanM ⊤
spanM-restore-clarified-def x si Γ ss = returnM (triv , ctxt-set-sym-info Γ x si , ss)

-- restore ctxt-info for the variable with given posinfo
spanM-restore-info : var → restore-def → spanM ⊤
spanM-restore-info v rd Γ ss = returnM (triv , ctxt-restore-info Γ v (fst rd) (snd rd) , ss)

_≫=span_ : ∀{A B : Set} → spanM A → (A → spanM B) → spanM B
(m₁ ≫=span m₂) ss Γ = m₁ ss Γ ≫=monad λ where (v , Γ , ss) → m₂ v Γ ss

_≫span_ : ∀{A B : Set} → spanM A → spanM B → spanM B
(m₁ ≫span m₂) = m₁ ≫=span (λ _ → m₂)

spanM-restore-info* : 𝕃 (var × restore-def) → spanM ⊤
spanM-restore-info* [] = spanMok
spanM-restore-info* ((v , qi , m) :: s) = spanM-restore-info v (qi , m) ≫span spanM-restore-info* s

infixl 2 _≫span_ _≫=span_ _≫=spanj_ _≫=spanm_ _≫=spanm'_ _≫=spanc_ _≫=spanc'_ _≫spanc_ _≫spanc'_

_≫=spanj_ : ∀{A : Set} → spanM (maybe A) → (A → spanM ⊤) → spanM ⊤
_≫=spanj_{A} m m' = m ≫=span cont
  where cont : maybe A → spanM ⊤
        cont nothing = spanMok
        cont (just x) = m' x

-- discard changes made by the first computation
_≫=spand_ : ∀{A B : Set} → spanM A → (A → spanM B) → spanM B
_≫=spand_{A} m m' Γ ss = m Γ ss ≫=monad λ where (v , _ , _) → m' v Γ ss

-- discard *spans* generated by first computation
_≫=spands_ : ∀ {A B : Set} → spanM A → (A → spanM B) → spanM B
_≫=spands_ m f Γ ss = m Γ ss ≫=monad λ where (v , Γ , _ ) → f v Γ ss

_≫=spanm_ : ∀{A : Set} → spanM (maybe A) → (A → spanM (maybe A)) → spanM (maybe A)
_≫=spanm_{A} m m' = m ≫=span cont
  where cont : maybe A → spanM (maybe A)
        cont nothing = spanMr nothing
        cont (just a) = m' a

_≫=spans'_ : ∀ {A B E : Set} → spanM (E ∨ A) → (A → spanM (E ∨ B)) → spanM (E ∨ B)
_≫=spans'_ m f = m ≫=span λ where
  (inj₁ e) → spanMr (inj₁ e)
  (inj₂ a) → f a

_≫=spanm'_ : ∀{A B : Set} → spanM (maybe A) → (A → spanM (maybe B)) → spanM (maybe B)
_≫=spanm'_{A}{B} m m' = m ≫=span cont
  where cont : maybe A → spanM (maybe B)
        cont nothing = spanMr nothing
        cont (just a) = m' a

-- Currying/uncurry span binding
_≫=spanc_ : ∀{A B C} → spanM (A × B) → (A → B → spanM C) → spanM C
(m ≫=spanc m') Γ ss = m Γ ss ≫=monad λ where
  ((a , b) , Γ' , ss') → m' a b Γ' ss'

_≫=spanc'_ : ∀{A B C} → spanM (A × B) → (B → spanM C) → spanM C
(m ≫=spanc' m') Γ ss = m Γ ss ≫=monad λ where
  ((a , b) , Γ' , ss') → m' b Γ' ss'

_≫spanc'_ : ∀{A B} → spanM A → B → spanM (A × B)
(m ≫spanc' b) = m ≫=span λ a → spanMr (a , b)

_≫spanc_ : ∀{A B} → spanM A → spanM B → spanM (A × B)
(ma ≫spanc mb) = ma ≫=span λ a → mb ≫=span λ b → spanMr (a , b)

spanMok' : ∀{A} → A → spanM (⊤ × A)
spanMok' a = spanMr (triv , a)

_on-fail_≫=spanm'_ : ∀ {A B} → spanM (maybe A) → spanM B
                            → (A → spanM B) → spanM B
_on-fail_≫=spanm'_ {A}{B} m fail f = m ≫=span cont
  where cont : maybe A → spanM B
        cont nothing  = fail
        cont (just x) = f x

_on-fail_≫=spans'_ : ∀ {A B E} → spanM (E ∨ A) → (E → spanM B) → (A → spanM B) → spanM B
_on-fail_≫=spans'_ {A}{B}{E} m fail f = m ≫=span cont
  where cont : E ∨ A → spanM B
        cont (inj₁ err) = fail err
        cont (inj₂ a) = f a

_exit-early_≫=spans'_ = _on-fail_≫=spans'_

with-ctxt : ∀ {A} → ctxt → spanM A → spanM A
with-ctxt Γ sm
  =   get-ctxt λ Γ' → set-ctxt Γ
    ≫span  sm
    ≫=span λ a → set-ctxt Γ'
    ≫span  spanMr a

sequence-spanM : ∀ {A} → 𝕃 (spanM A) → spanM (𝕃 A)
sequence-spanM [] = spanMr []
sequence-spanM (sp :: sps)
  =   sp
    ≫=span λ x → sequence-spanM sps
    ≫=span λ xs → spanMr (x :: xs)

foldr-spanM : ∀ {A B} → (A → spanM B → spanM B) → spanM B → 𝕃 (spanM A) → spanM B
foldr-spanM f n [] = n
foldr-spanM f n (m :: ms)
  = m ≫=span λ a → f a (foldr-spanM f n ms)

foldl-spanM : ∀ {A B} → (spanM B → A → spanM B) → spanM B → 𝕃 (spanM A) → spanM B
foldl-spanM f m [] = m
foldl-spanM f m (m' :: ms) =
  m' ≫=span λ a → foldl-spanM f (f m a) ms

spanM-for_init_use_ : ∀ {A B} → 𝕃 (spanM A) → spanM B → (A → spanM B → spanM B) → spanM B
spanM-for xs init acc use f = foldr-spanM f acc xs

spanM-add : span → spanM ⊤
spanM-add s Γ ss = returnM (triv , Γ , add-span s ss)

spanM-addl : 𝕃 span → spanM ⊤
spanM-addl [] = spanMok
spanM-addl (s :: ss) = spanM-add s ≫span spanM-addl ss

debug-span : posinfo → posinfo → 𝕃 tagged-val → span
debug-span pi pi' tvs = mk-span "Debug" pi pi' tvs nothing

spanM-debug : posinfo → posinfo → 𝕃 tagged-val → spanM ⊤
--spanM-debug pi pi' tvs = spanM-add (debug-span pi pi' tvs)
spanM-debug pi pi' tvs = spanMok

to-string-tag-tk : (tag : string) → ctxt → tk → tagged-val
to-string-tag-tk t Γ (Tkt T) = to-string-tag t Γ T
to-string-tag-tk t Γ (Tkk k) = to-string-tag t Γ k

--------------------------------------------------
-- tagged-val constants
--------------------------------------------------

location-data : location → tagged-val
location-data (file-name , pi) = strRunTag "location" empty-ctxt (strAdd file-name ≫str strAdd " - " ≫str strAdd pi)

var-location-data : ctxt → var → tagged-val
var-location-data Γ @ (mk-ctxt _ _ i _ _) x =
  location-data (maybe-else ("missing" , "missing") snd
    (trie-lookup i x maybe-or trie-lookup i (qualif-var Γ x)))
{-
{-# TERMINATING #-}
var-location-data : ctxt → var → maybe language-level → tagged-val
var-location-data Γ x (just ll-term) with ctxt-var-location Γ x | qualif-term Γ (Var posinfo-gen x)
...| ("missing" , "missing") | (Var pi x') = location-data (ctxt-var-location Γ x')
...| loc | _ = location-data loc
var-location-data Γ x (just ll-type) with ctxt-var-location Γ x | qualif-type Γ (TpVar posinfo-gen x)
...| ("missing" , "missing") | (TpVar pi x') = location-data (ctxt-var-location Γ x')
...| loc | _ = location-data loc
var-location-data Γ x (just ll-kind) with ctxt-var-location Γ x | qualif-kind Γ (KndVar posinfo-gen x ArgsNil)
...| ("missing" , "missing") | (KndVar pi x' as) = location-data (ctxt-var-location Γ x')
...| loc | _ = location-data loc
var-location-data Γ x nothing with ctxt-lookup-term-var Γ x | ctxt-lookup-type-var Γ x | ctxt-lookup-kind-var-def Γ x
...| just _ | _ | _ = var-location-data Γ x (just ll-term)
...| _ | just _ | _ = var-location-data Γ x (just ll-type)
...| _ | _ | just _ = var-location-data Γ x (just ll-kind)
...| _ | _ | _ = location-data ("missing" , "missing")
-}
explain : string → tagged-val
explain = strRunTag "explanation" empty-ctxt ∘ strAdd

reason : string → tagged-val
reason = strRunTag "reason" empty-ctxt ∘ strAdd

expected-type : ctxt → type → tagged-val
expected-type = to-string-tag "expected-type"

expected-type-subterm : ctxt → type → tagged-val
expected-type-subterm = to-string-tag "expected-type of the subterm"

missing-expected-type : tagged-val
missing-expected-type = strRunTag "expected-type" empty-ctxt $ strAdd "[missing]"

-- hnf-type : ctxt → type → tagged-val
-- hnf-type Γ tp = to-string-tag "hnf of type" Γ (hnf-term-type Γ ff tp)

-- hnf-expected-type : ctxt → type → tagged-val
-- hnf-expected-type Γ tp = to-string-tag "hnf of expected type" Γ (hnf-term-type Γ ff tp)

expected-kind : ctxt → kind → tagged-val
expected-kind = to-string-tag "expected kind"

expected-kind-if : ctxt → maybe kind → 𝕃 tagged-val
expected-kind-if _ nothing = []
expected-kind-if Γ (just k) = [ expected-kind Γ k ]

expected-type-if : ctxt → maybe type → 𝕃 tagged-val
expected-type-if _ nothing = []
expected-type-if Γ (just tp) = [ expected-type Γ tp ]

-- hnf-expected-type-if : ctxt → maybe type → 𝕃 tagged-val
-- hnf-expected-type-if Γ nothing = []
-- hnf-expected-type-if Γ (just tp) = [ hnf-expected-type Γ tp ]

type-data : ctxt → type → tagged-val
type-data = to-string-tag "type"

missing-type : tagged-val
missing-type = strRunTag "type" empty-ctxt $ strAdd "[undeclared]"

warning-data : string → tagged-val
warning-data = strRunTag "warning" empty-ctxt ∘ strAdd

check-for-type-mismatch : ctxt → string → type → type → 𝕃 tagged-val × err-m
check-for-type-mismatch Γ s tp tp' =
  let tp'' = hnf Γ unfold-head tp' tt in
  expected-type Γ tp :: [ type-data Γ tp' ] ,
  if conv-type Γ tp tp'' then nothing else just ("The expected type does not match the " ^ s ^ " type.")

check-for-type-mismatch-if : ctxt → string → maybe type → type → 𝕃 tagged-val × err-m
check-for-type-mismatch-if Γ s (just tp) = check-for-type-mismatch Γ s tp
check-for-type-mismatch-if Γ s nothing tp = [ type-data Γ tp ] , nothing

summary-data : {ed : exprd} → (name : string) → ctxt → ⟦ ed ⟧ → tagged-val
summary-data name Γ t = strRunTag "summary" Γ (strVar name ≫str strAdd " : " ≫str to-stringh t)

missing-kind : tagged-val
missing-kind = strRunTag "kind" empty-ctxt $ strAdd "[undeclared]"

head-kind : ctxt → kind → tagged-val
head-kind = to-string-tag "the kind of the head"

head-type : ctxt → type → tagged-val
head-type = to-string-tag "the type of the head"

arg-type : ctxt → type → tagged-val
arg-type = to-string-tag "computed arg type"

arg-exp-type : ctxt → type → tagged-val
arg-exp-type = to-string-tag "expected arg type"

type-app-head : ctxt → type → tagged-val
type-app-head = to-string-tag "the head"

term-app-head : ctxt → term → tagged-val
term-app-head = to-string-tag "the head"

term-argument : ctxt → term → tagged-val
term-argument = to-string-tag "the argument"

type-argument : ctxt → type → tagged-val
type-argument = to-string-tag "the argument"

contextual-type-argument : ctxt → type → tagged-val
contextual-type-argument = to-string-tag "contextual type arg"

arg-argument : ctxt → arg → tagged-val
arg-argument Γ (TermArg me x) = term-argument Γ x
arg-argument Γ (TypeArg x) = type-argument Γ x

kind-data : ctxt → kind → tagged-val
kind-data = to-string-tag "kind"

liftingType-data : ctxt → liftingType → tagged-val
liftingType-data = to-string-tag "lifting type"

kind-data-if : ctxt → maybe kind → 𝕃 tagged-val
kind-data-if Γ (just k) = [ kind-data Γ k ]
kind-data-if _ nothing = []

super-kind-data : tagged-val
super-kind-data = strRunTag "superkind" empty-ctxt $ strAdd "□"

symbol-data : string → tagged-val
symbol-data = strRunTag "symbol" empty-ctxt ∘ strAdd

tk-data : ctxt → tk → tagged-val
tk-data Γ (Tkk k) = kind-data Γ k
tk-data Γ (Tkt t) = type-data Γ t

checking-to-string : checking-mode → string
checking-to-string checking = "checking"
checking-to-string synthesizing = "synthesizing"
checking-to-string untyped = "untyped"

checking-data : checking-mode → tagged-val
checking-data = strRunTag "checking-mode" empty-ctxt ∘' strAdd ∘' checking-to-string

checked-meta-var : var → tagged-val
checked-meta-var = strRunTag "checked meta-var" empty-ctxt ∘ strAdd

ll-data : language-level → tagged-val
ll-data = strRunTag "language-level" empty-ctxt ∘' strAdd ∘' ll-to-string

ll-data-term = ll-data ll-term
ll-data-type = ll-data ll-type
ll-data-kind = ll-data ll-kind
{-
binder-data : ℕ → tagged-val
binder-data n = "binder" , [[ ℕ-to-string n ]] , []

-- this is the subterm position in the parse tree (as determined by
-- spans) for the bound variable of a binder
binder-data-const : tagged-val
binder-data-const = binder-data 0

bound-data : defTermOrType → ctxt → tagged-val
bound-data (DefTerm pi v mtp t) Γ = to-string-tag "bound-value" Γ t
bound-data (DefType pi v k tp) Γ = to-string-tag "bound-value" Γ tp

-}

binder-data : ctxt → posinfo → var → (atk : tk) → maybeErased → maybe (if tk-is-type atk then term else type) → (from to : posinfo) → tagged-val
binder-data Γ pi x atk me val s e =
  strRunTag "binder" Γ $
  strAdd "symbol:" ≫str --strAdd "{\\\\\"symbol\\\\\":\\\\\"" ≫str
  strAdd x ≫str --strAdd "\\\\\"," ≫str
  atk-val atk val ≫str
  strAdd "§from:" ≫str --strAdd ",\\\\\"from\\\\\":" ≫str
  strAdd s ≫str
  strAdd "§to:" ≫str --strAdd ",\\\\\"to\\\\\":" ≫str
  strAdd e ≫str
  loc ≫str
  erased?
  --strAdd "}"
  where
  loc : strM
  {-loc = maybe-else' (ctxt-get-info (qualif-var Γ x) Γ) strEmpty $ λ where
    (_ , fn , pi) →
      strAdd "§fn:" ≫str --strAdd ",\\\\\"fn\\\\\":\\\\\"" ≫str
      strAdd fn ≫str
      strAdd "§pos:" ≫str --strAdd "\\\\\",\\\\\"pos\\\\\":" ≫str
      strAdd pi-}
  loc = strAdd "§fn:" ≫str strAdd (ctxt-get-current-filename Γ) ≫str strAdd "§pos:" ≫str strAdd pi
  erased? : strM
  erased? =
    strAdd "§erased:" ≫str --strAdd ",\\\\\"erased\\\\\":" ≫str
    strAdd (if me then "true" else "false")
  val? : ∀ {ed} → maybe ⟦ ed ⟧ → strM
  val? = maybe-else strEmpty λ x →
    strAdd "§value:" ≫str --strAdd "\\\\\",\\\\\"value\\\\\":\\\\\"" ≫str
    to-stringh x
  atk-val : (atk : tk) → maybe (if tk-is-type atk then term else type) → strM
  atk-val (Tkt T) t? =
    strAdd "§type:" ≫str --strAdd "\\\\\"type\\\\\":\\\\\"" ≫str
    to-stringh T ≫str
    val? t? -- ≫str
    --strAdd "\\\\\""
  atk-val (Tkk k) T? =
    strAdd "§kind:" ≫str --strAdd "\\\\\"kind\\\\\":\\\\\"" ≫str
    to-stringh k ≫str
    val? T? -- ≫str
    --strAdd "\\\\\""

punctuation-data : tagged-val
punctuation-data = strRunTag "punctuation" empty-ctxt $ strAdd "true"

not-for-navigation : tagged-val
not-for-navigation = strRunTag "not-for-navigation" empty-ctxt $ strAdd "true"

is-erased : type → 𝔹
is-erased (TpVar _ _ ) = tt
is-erased _ = ff

keywords = "keywords"
--keyword-erased = "erased"
--keyword-noterased = "noterased"
keyword-application = "application"
keyword-locale = "meta-var-locale"

--noterased : tagged-val
--noterased = keywords , [[ keyword-noterased ]] , []

keywords-data : 𝕃 string → tagged-val
keywords-data kws = keywords , h kws , [] where
  h : 𝕃 string → rope
  h [] = [[]]
  h (k :: []) = [[ k ]]
  h (k :: ks) = [[ k ]] ⊹⊹ [[ " " ]] ⊹⊹ h ks
{-
keywords-data-var : maybeErased → tagged-val
keywords-data-var e =
  keywords ,  [[ if e then keyword-erased else keyword-noterased ]] , []
-}
keywords-app : (is-locale : 𝔹) → tagged-val
keywords-app l = keywords-data ([ keyword-application ] ++ (if l then [ keyword-locale ] else []))

keywords-app-if-typed : checking-mode → (is-locale : 𝔹) → 𝕃 tagged-val
keywords-app-if-typed untyped l = []
keywords-app-if-typed _ l = [ keywords-app l ]

error-if-not-eq : ctxt → type → 𝕃 tagged-val → 𝕃 tagged-val × err-m
error-if-not-eq Γ (TpEq pi t1 t2 pi') tvs = expected-type Γ (TpEq pi t1 t2 pi') :: tvs , nothing
error-if-not-eq Γ tp tvs = expected-type Γ tp :: tvs , just "This term is being checked against the following type, but an equality type was expected"

error-if-not-eq-maybe : ctxt → maybe type → 𝕃 tagged-val → 𝕃 tagged-val × err-m
error-if-not-eq-maybe Γ (just tp) = error-if-not-eq Γ tp
error-if-not-eq-maybe _ _ tvs = tvs , nothing

params-data : ctxt → params → 𝕃 tagged-val
params-data _ [] = []
params-data Γ ps = [ params-to-string-tag "parameters" Γ ps ]

--------------------------------------------------
-- span-creating functions
--------------------------------------------------

Star-name : string
Star-name = "Star"

parens-span : posinfo → posinfo → span
parens-span pi pi' = mk-span "parentheses" pi pi' [] nothing

data decl-class : Set where
  param : decl-class
  index : decl-class

decl-class-name : decl-class → string
decl-class-name param = "parameter"
decl-class-name index = "index"

Decl-span : ctxt → decl-class → posinfo → posinfo → var → tk → maybeErased → posinfo → span
Decl-span Γ dc pi pi' v atk me pi'' = mk-span ((if tk-is-type atk then "Term " else "Type ") ^ (decl-class-name dc))
                                      pi pi'' [ binder-data Γ pi' v atk me nothing (tk-end-pos atk) pi'' ] nothing

TpVar-span : ctxt → posinfo → string → checking-mode → 𝕃 tagged-val → err-m → span
TpVar-span Γ pi v check tvs =
  mk-span name pi (posinfo-plus-str pi (unqual-local v))
    (checking-data check :: ll-data-type :: var-location-data Γ v :: symbol-data (unqual-local v) :: tvs)
  where
  v' = unqual-local v
  name = if isJust (data-lookup Γ (qualif-var Γ v') [])
           then "Datatype variable" else "Type variable"

Var-span : ctxt → posinfo → string → checking-mode → 𝕃 tagged-val → err-m → span
Var-span Γ pi v check tvs =
  mk-span name pi (posinfo-plus-str pi v')
    (checking-data check :: ll-data-term :: var-location-data Γ v :: symbol-data v' :: tvs)
  where
  v' = unqual-local v
  name : string
  name with qual-lookup Γ v'
  ...| just (_ , ctr-def _ _ _ _ _ , _) = "Constructor variable"
  ...| _ = "Term variable"

KndVar-span : ctxt → (posinfo × var) → (end-pi : posinfo) → params → checking-mode → 𝕃 tagged-val → err-m → span
KndVar-span Γ (pi , v) pi' ps check tvs =
  mk-span "Kind variable" pi pi'
    (checking-data check :: ll-data-kind :: var-location-data Γ v :: symbol-data (unqual-local v) :: super-kind-data :: (params-data Γ ps ++ tvs))

var-span-with-tags : maybeErased → ctxt → posinfo → string → checking-mode → tk → 𝕃 tagged-val → err-m → span
var-span-with-tags _ Γ pi x check (Tkk k) tags = TpVar-span Γ pi x check ({-keywords-data-var ff ::-} [ kind-data Γ k ] ++ tags)
var-span-with-tags e Γ pi x check (Tkt t) tags = Var-span Γ pi x check ({-keywords-data-var e ::-} [ type-data Γ t ] ++ tags)

var-span :  maybeErased → ctxt → posinfo → string → checking-mode → tk → err-m → span
var-span e Γ pi x check tk = var-span-with-tags e Γ pi x check tk []

redefined-var-span : ctxt → posinfo → var → span
redefined-var-span Γ pi x = mk-span "Variable definition" pi (posinfo-plus-str pi x)
                             [ var-location-data Γ x ] (just "This symbol was defined already.")

TpAppt-span : type → term → checking-mode → 𝕃 tagged-val → err-m → span
TpAppt-span tp t check tvs = mk-span "Application of a type to a term" (type-start-pos tp) (term-end-pos t) (checking-data check :: ll-data-type :: tvs)

TpApp-span : type → type → checking-mode → 𝕃 tagged-val → err-m → span
TpApp-span tp tp' check tvs = mk-span "Application of a type to a type" (type-start-pos tp) (type-end-pos tp') (checking-data check :: ll-data-type :: tvs)

App-span : (is-locale : 𝔹) → term → term → checking-mode → 𝕃 tagged-val → err-m → span
App-span l t t' check tvs = mk-span "Application of a term to a term" (term-start-pos t) (term-end-pos t') (checking-data check :: ll-data-term :: keywords-app-if-typed check l ++ tvs)

AppTp-span : term → type → checking-mode → 𝕃 tagged-val → err-m → span
AppTp-span t tp check tvs = mk-span "Application of a term to a type" (term-start-pos t) (type-end-pos tp) (checking-data check :: ll-data-term :: keywords-app-if-typed check ff ++ tvs)

TpQuant-e = 𝔹

is-pi : TpQuant-e
is-pi = tt

TpQuant-span : ctxt → TpQuant-e → posinfo → posinfo → var → tk → type → checking-mode → 𝕃 tagged-val → err-m → span
TpQuant-span Γ is-pi pi pi' x atk body check tvs err =
  let err-if-type-pi = if ~ tk-is-type atk && is-pi then just "Π-types must bind a term, not a type (use ∀ instead)" else nothing in
  mk-span (if is-pi then "Dependent function type" else "Implicit dependent function type")
       pi (type-end-pos body) (checking-data check :: ll-data-type :: binder-data Γ pi' x atk (~ is-pi) nothing (type-start-pos body) (type-end-pos body) :: tvs) (if isJust err-if-type-pi then err-if-type-pi else err)

TpLambda-span : ctxt → posinfo → posinfo → var → tk → type → checking-mode → 𝕃 tagged-val → err-m → span
TpLambda-span Γ pi pi' x atk body check tvs =
  mk-span "Type-level lambda abstraction" pi (type-end-pos body)
    (checking-data check :: ll-data-type :: binder-data Γ pi' x atk NotErased nothing (type-start-pos body) (type-end-pos body) :: tvs)

Iota-span : ctxt → posinfo → posinfo → var → type → checking-mode → 𝕃 tagged-val → err-m → span
Iota-span Γ pi pi' x t2 check tvs = mk-span "Iota-abstraction" pi (type-end-pos t2) (explain "A dependent intersection type" :: checking-data check :: binder-data Γ pi' x (Tkt t2) ff nothing (type-start-pos t2) (type-end-pos t2) :: ll-data-type :: tvs)

TpArrow-span : type → type → checking-mode → 𝕃 tagged-val → err-m → span
TpArrow-span t1 t2 check tvs = mk-span "Arrow type" (type-start-pos t1) (type-end-pos t2) (checking-data check :: ll-data-type :: tvs)

TpEq-span : posinfo → term → term → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
TpEq-span pi t1 t2 pi' check tvs = mk-span "Equation" pi pi'
                             (explain "Equation between terms" :: checking-data check :: ll-data-type :: tvs)

Star-span : posinfo → checking-mode → err-m → span
Star-span pi check = mk-span Star-name pi (posinfo-plus pi 1) (checking-data check :: [ ll-data-kind ])

KndPi-span : ctxt → posinfo → posinfo → var → tk → kind → checking-mode → err-m → span
KndPi-span Γ pi pi' x atk k check =
  mk-span "Pi kind" pi (kind-end-pos k)
    (checking-data check :: ll-data-kind :: binder-data Γ pi' x atk ff nothing (kind-start-pos k) (kind-end-pos k) :: [ super-kind-data ])

KndArrow-span : kind → kind → checking-mode → err-m → span
KndArrow-span k k' check = mk-span "Arrow kind" (kind-start-pos k) (kind-end-pos k') (checking-data check :: ll-data-kind :: [ super-kind-data ])

KndTpArrow-span : type → kind → checking-mode → err-m → span
KndTpArrow-span t k check = mk-span "Arrow kind" (type-start-pos t) (kind-end-pos k) (checking-data check :: ll-data-kind :: [ super-kind-data ])

{- [[file:../cedille-mode.el::(defun%20cedille-mode-filter-out-special(data)][Frontend]]  -}
special-tags : 𝕃 string
special-tags =
  "symbol" :: "location" :: "language-level" :: "checking-mode" :: "summary"
  :: "binder" :: "bound-value" :: "keywords" :: []

error-span-filter-special : error-span → error-span
error-span-filter-special (mk-error-span dsc pi pi' tvs msg) =
  mk-error-span dsc pi pi' tvs' msg
  where tvs' = (flip filter) tvs λ tag → list-any (_=string (fst tag)) special-tags

erasure : ctxt → term → tagged-val
erasure Γ t = to-string-tag "erasure" Γ (erase-term t)

erased-marg-span : ctxt → term → maybe type → span
erased-marg-span Γ t mtp = mk-span "Erased module parameter" (term-start-pos t) (term-end-pos t)
  (maybe-else [] (λ tp → [ type-data Γ tp ]) mtp)
  (just "An implicit module parameter variable occurs free in the erasure of the term.")

Lam-span-erased : maybeErased → string
Lam-span-erased Erased = "Erased lambda abstraction (term-level)"
Lam-span-erased NotErased = "Lambda abstraction (term-level)"

Lam-span : ctxt → checking-mode → posinfo → posinfo → maybeErased → var → tk → term → 𝕃 tagged-val → err-m → span
Lam-span Γ c pi pi' NotErased x {-(SomeClass-} (Tkk k) {-)-} t tvs e =
  mk-span (Lam-span-erased NotErased) pi (term-end-pos t) (ll-data-term :: binder-data Γ pi' x (Tkk k) NotErased nothing (term-start-pos t) (term-end-pos t) :: checking-data c :: tvs) (e maybe-or just "λ-terms must bind a term, not a type (use Λ instead)")
--Lam-span Γ c pi l x NoClass t tvs = mk-span (Lam-span-erased l) pi (term-end-pos t) (ll-data-term :: binder-data Γ x :: checking-data c :: tvs)
Lam-span Γ c pi pi' l x {-(SomeClass-} atk {-)-} t tvs = mk-span (Lam-span-erased l) pi (term-end-pos t)
                                           ((ll-data-term :: binder-data Γ pi' x atk l nothing (term-start-pos t) (term-end-pos t) :: checking-data c :: tvs)
                                           ++ bound-tp atk)
  where
  bound-tp : tk → 𝕃 tagged-val
  bound-tp (Tkt (TpHole _)) = []
  bound-tp atk = [ to-string-tag-tk "type of bound variable" Γ atk ]

compileFail-in : ctxt → term → 𝕃 tagged-val × err-m
compileFail-in Γ t with is-free-in check-erased compileFail-qual | qualif-term Γ t
...| is-free | tₒ with erase-term tₒ | hnf Γ unfold-all tₒ ff
...| tₑ | tₙ with is-free tₒ
...| ff = [] , nothing
...| tt with is-free tₙ | is-free tₑ
...| tt | _ = [ to-string-tag "normalized term" Γ tₙ ] , just "compileFail occurs in the normalized term"
...| ff | ff = [ to-string-tag "the term" Γ tₒ ] , just "compileFail occurs in an erased position"
...| ff | tt = [] , nothing

DefTerm-span : ctxt → posinfo → var → (checked : checking-mode) → maybe type → term → posinfo → 𝕃 tagged-val → span
DefTerm-span Γ pi x checked tp t pi' tvs =
  h ((h-summary tp) ++ ({-erasure Γ t ::-} tvs)) pi x checked tp pi'
  where h : 𝕃 tagged-val → posinfo → var → (checked : checking-mode) → maybe type → posinfo → span
        h tvs pi x checking _ pi' =
          mk-span "Term-level definition (checking)" pi pi' tvs nothing
        h tvs pi x _ (just tp) pi' =
          mk-span "Term-level definition (synthesizing)" pi pi' (to-string-tag "synthesized type" Γ tp :: tvs) nothing
        h tvs pi x _ nothing pi' =
          mk-span "Term-level definition (synthesizing)" pi pi' ((strRunTag "synthesized type" empty-ctxt $ strAdd "[nothing]") :: tvs) nothing
        h-summary : maybe type → 𝕃 tagged-val
        h-summary nothing = [(checking-data synthesizing)]
        h-summary (just tp) = (checking-data checking :: [ summary-data x Γ tp ])

CheckTerm-span : ctxt → (checked : checking-mode) → maybe type → term → posinfo → 𝕃 tagged-val → span
CheckTerm-span Γ checked tp t pi' tvs =
  h ({-erasure Γ t ::-} tvs) checked tp (term-start-pos t) pi'
  where h : 𝕃 tagged-val → (checked : checking-mode) → maybe type → posinfo → posinfo → span
        h tvs checking _ pi pi' =
          mk-span "Checking a term" pi pi' (checking-data checking :: tvs) nothing
        h tvs _ (just tp) pi pi' =
          mk-span "Synthesizing a type for a term" pi pi' (checking-data synthesizing :: to-string-tag "synthesized type" Γ tp :: tvs) nothing
        h tvs _ nothing pi pi' =
          mk-span "Synthesizing a type for a term" pi pi' (checking-data synthesizing :: (strRunTag "synthesized type" empty-ctxt $ strAdd "[nothing]") :: tvs) nothing

normalized-type : ctxt → type → tagged-val
normalized-type = to-string-tag "normalized type"

DefType-span : ctxt → posinfo → var → (checked : checking-mode) → maybe kind → type → posinfo → 𝕃 tagged-val → span
DefType-span Γ pi x checked mk tp pi' tvs =
  h ((h-summary mk) ++ tvs) checked mk
  where h : 𝕃 tagged-val → checking-mode → maybe kind → span
        h tvs checking _ = mk-span "Type-level definition (checking)" pi pi' tvs nothing
        h tvs _ (just k) =
          mk-span "Type-level definition (synthesizing)" pi pi' (to-string-tag "synthesized kind" Γ k :: tvs) nothing
        h tvs _ nothing =
          mk-span "Type-level definition (synthesizing)" pi pi' ( (strRunTag "synthesized kind" empty-ctxt $ strAdd "[nothing]") :: tvs) nothing
        h-summary : maybe kind → 𝕃 tagged-val
        h-summary nothing = [(checking-data synthesizing)]
        h-summary (just k) = (checking-data checking :: [ summary-data x Γ k ])

DefKind-span : ctxt → posinfo → var → kind → posinfo → span
DefKind-span Γ pi x k pi' = mk-span "Kind-level definition" pi pi' (kind-data Γ k :: [ summary-data x Γ (Var pi "□") ]) nothing

DefDatatype-span : ctxt → posinfo → posinfo → var → params → (reg Mu bound : kind) → (mu : type) → (cast : type) → ctrs → posinfo → span
DefDatatype-span Γ pi pi' x ps k kₘᵤ kₓ Tₘᵤ Tₜₒ cs pi'' =
  mk-span "Datatype definition" pi pi'' (binder-data Γ pi' x (Tkk kₓ) ff nothing (kind-end-pos k) pi'' :: summary-data x Γ k :: summary-data (data-Is/ x) Γ kₘᵤ :: summary-data (data-is/ x) Γ Tₘᵤ :: summary-data (data-to/ x) Γ Tₜₒ :: to-string-tag (data-Is/ x) Γ kₘᵤ :: to-string-tag (data-is/ x) Γ Tₘᵤ :: to-string-tag (data-to/ x) Γ Tₜₒ :: []) nothing

{-unchecked-term-span : term → span
unchecked-term-span t = mk-span "Unchecked term" (term-start-pos t) (term-end-pos t)
                           (ll-data-term :: not-for-navigation :: [ explain "This term has not been type-checked."]) nothing-}

Beta-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
Beta-span pi pi' check tvs = mk-span "Beta axiom" pi pi'
                     (checking-data check :: ll-data-term :: explain "A term constant whose type states that β-equal terms are provably equal" :: tvs)

hole-span : ctxt → posinfo → maybe type → 𝕃 tagged-val → span
hole-span Γ pi tp tvs =
  mk-span "Hole" pi (posinfo-plus pi 1)
    (ll-data-term :: expected-type-if Γ tp ++ tvs)
    (just "This hole remains to be filled in")

tp-hole-span : ctxt → posinfo → maybe kind → 𝕃 tagged-val → span
tp-hole-span Γ pi k tvs =
  mk-span "Hole" pi (posinfo-plus pi 1)
    (ll-data-term :: expected-kind-if Γ k ++ tvs)
    (just "This hole remains to be filled in")

expected-to-string : checking-mode → string
expected-to-string checking = "expected"
expected-to-string synthesizing = "synthesized"
expected-to-string untyped = "untyped"

Epsilon-span : posinfo → leftRight → maybeMinus → term → checking-mode → 𝕃 tagged-val → err-m → span
Epsilon-span pi lr m t check tvs = mk-span "Epsilon" pi (term-end-pos t)
                                         (checking-data check :: ll-data-term :: tvs ++
                                         [ explain ("Normalize " ^ side lr ^ " of the "
                                                   ^ expected-to-string check ^ " equation, using " ^ maybeMinus-description m
                                                   ^ " reduction." ) ])
  where side : leftRight → string
        side Left = "the left-hand side"
        side Right = "the right-hand side"
        side Both = "both sides"
        maybeMinus-description : maybeMinus → string
        maybeMinus-description EpsHnf = "head"
        maybeMinus-description EpsHanf = "head-applicative"

optGuide-spans : optGuide → checking-mode → spanM ⊤
optGuide-spans NoGuide _ = spanMok
optGuide-spans (Guide pi x tp) expected =
  get-ctxt λ Γ → spanM-add (Var-span Γ pi x expected [] nothing)

Rho-span : posinfo → term → term → checking-mode → rhoHnf → ℕ ⊎ var → 𝕃 tagged-val → err-m → span
Rho-span pi t t' expected r (inj₂ x) tvs =
  mk-span "Rho" pi (term-end-pos t')
    (checking-data expected :: ll-data-term :: explain ("Rewrite all places where " ^ x ^ " occurs in the " ^ expected-to-string expected ^ " type, using an equation. ") :: tvs)
Rho-span pi t t' expected r (inj₁ numrewrites) tvs err =
  mk-span "Rho" pi (term-end-pos t')
    (checking-data expected :: ll-data-term :: tvs ++
    (explain ("Rewrite terms in the "
      ^ expected-to-string expected ^ " type, using an equation. "
      ^ (if r then "" else "Do not ") ^ "Beta-reduce the type as we look for matches.") :: fst h)) (snd h)
  where h : 𝕃 tagged-val × err-m
        h = if isJust err
              then [] , err
              else if numrewrites =ℕ 0
                then [] , just "No rewrites could be performed."
                else [ strRunTag "Number of rewrites" empty-ctxt (strAdd $ ℕ-to-string numrewrites) ] , err

Phi-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
Phi-span pi pi' expected tvs = mk-span "Phi" pi pi' (checking-data expected :: ll-data-term :: tvs)

Chi-span : ctxt → posinfo → optType → term → checking-mode → 𝕃 tagged-val → err-m → span
Chi-span Γ pi m t' check tvs = mk-span "Chi" pi (term-end-pos t')  (ll-data-term :: checking-data check :: tvs ++ helper m)
  where helper : optType → 𝕃 tagged-val
        helper (SomeType T) =  explain ("Check a term against an asserted type") :: [ to-string-tag "the asserted type" Γ T ]
        helper NoType = [ explain ("Change from checking mode (outside the term) to synthesizing (inside)") ]

Sigma-span : posinfo → term → checking-mode → 𝕃 tagged-val → err-m → span
Sigma-span pi t check tvs =
  mk-span "Sigma" pi (term-end-pos t)
     (ll-data-term :: checking-data check :: explain "Swap the sides of the equation synthesized for the body of this term" :: tvs)

Delta-span : ctxt → posinfo → optType → term → checking-mode → 𝕃 tagged-val → err-m → span
Delta-span Γ pi T t check tvs =
  mk-span "Delta" pi (term-end-pos t)
    (ll-data-term :: explain "Prove anything you want from a contradiction" :: checking-data check :: tvs)

Open-span : ctxt → opacity → posinfo → var → term → checking-mode → 𝕃 tagged-val → err-m → span
Open-span Γ o pi x t check tvs =
  elim-pair (if o iff OpacTrans
    then ("Open" , "Open an opaque definition")
    else ("Close" , "Hide a definition")) λ name expl →
  mk-span name pi (term-end-pos t)
    (ll-data-term :: explain expl :: checking-data check :: tvs)

motive-label : string
motive-label = "the motive"

the-motive : ctxt → type → tagged-val
the-motive = to-string-tag motive-label

Theta-span : ctxt → posinfo → theta → term → lterms → checking-mode → 𝕃 tagged-val → err-m → span
Theta-span Γ pi u t ls check tvs = mk-span "Theta" pi (lterms-end-pos (term-end-pos t) ls) (ll-data-term :: checking-data check :: tvs ++ do-explain u)
  where do-explain : theta → 𝕃 tagged-val
        do-explain Abstract = [ explain ("Perform an elimination with the first term, after abstracting it from the expected type.") ]
        do-explain (AbstractVars vs) = [ strRunTag "explanation" Γ (strAdd "Perform an elimination with the first term, after abstracting the listed variables (" ≫str vars-to-string vs ≫str strAdd ") from the expected type.") ]
        do-explain AbstractEq = [ explain ("Perform an elimination with the first term, after abstracting it with an equation "
                                         ^ "from the expected type.") ]

Mu-span : ctxt → posinfo → maybe var → posinfo → (motive? : maybe type) → checking-mode → 𝕃 tagged-val → err-m → span
Mu-span Γ pi x? pi' motive? check tvs = mk-span (if isJust x? then "Mu" else "Mu'") pi pi' (ll-data-term :: checking-data check :: explain ("Pattern match on a term" ^ (if isJust motive? then ", with a motive" else "")) :: tvs)

pattern-ctr-span : ctxt → posinfo → var → caseArgs → maybe type → err-m → span
pattern-ctr-span Γ pi x as tp =
  let x' = unqual-local x in
  mk-span "Pattern constructor" pi (posinfo-plus-str pi x') (checking-data synthesizing :: var-location-data Γ x :: ll-data-term :: symbol-data x' :: maybe-else' tp [] (λ tp → params-to-string-tag "args" Γ (rename-to-args empty-renamectxt as $ fst $ decompose-arrows Γ tp) :: []))
  where
  open import rename
  rename-to-args : renamectxt → caseArgs → params → params
  rename-to-args ρ (CaseTermArg _ _ x :: as) (Decl pi pi' me x' atk pi'' :: ps) =
    Decl pi pi' me x (subst-renamectxt Γ ρ atk) pi'' ::
      rename-to-args (renamectxt-insert ρ x' x) as ps
  rename-to-args ρ (CaseTypeArg _ x :: as) (Decl pi pi' me x' atk pi'' :: ps) =
    Decl pi pi' me x (subst-renamectxt Γ ρ atk) pi'' ::
      rename-to-args (renamectxt-insert ρ x' x) as ps
  rename-to-args ρ [] (Decl pi pi' me x atk pi'' :: ps) =
    Decl pi pi' me x (subst-renamectxt Γ ρ atk) pi'' ::
      rename-to-args (renamectxt-insert ρ x x) [] ps
  rename-to-args ρ as ps = ps

Lft-span : ctxt → posinfo → posinfo → var → term → checking-mode → 𝕃 tagged-val → err-m → span
Lft-span Γ pi pi' X t check tvs = mk-span "Lift type" pi (term-end-pos t) (checking-data check :: ll-data-type :: binder-data Γ pi' X (Tkk star) tt nothing (term-start-pos t) (term-end-pos t) :: tvs)

File-span : ctxt → posinfo → posinfo → string → span
File-span Γ pi pi' filename = mk-span ("Cedille source file (" ^ filename ^ ")") pi pi' (print-file-id-table Γ) nothing

Module-span : posinfo → posinfo → span
Module-span pi pi' = mk-span "Module declaration" pi pi' [ not-for-navigation ] nothing

Module-header-span : posinfo → posinfo → span
Module-header-span pi pi' = mk-span "Module header" pi pi' [ not-for-navigation ] nothing

DefDatatype-header-span : posinfo → span
DefDatatype-header-span pi = mk-span "Data" pi (posinfo-plus-str pi "data") [ not-for-navigation ] nothing

Import-span : posinfo → string → posinfo → 𝕃 tagged-val → err-m → span
Import-span pi file pi' tvs = mk-span ("Import of another source file") pi pi' (("Path" , [[ file ]] , []) :: location-data (file , first-position) :: tvs)

Import-module-span : ctxt → (posinfo × var) → params → 𝕃 tagged-val → err-m → span
Import-module-span Γ (pi , mn) ps tvs = mk-span "Imported module" pi (posinfo-plus-str pi mn) (params-data Γ ps ++ tvs)

punctuation-span : string → posinfo → posinfo → span
punctuation-span name pi pi'  = mk-span name pi pi' ( punctuation-data ::  not-for-navigation :: [] ) nothing

whitespace-span : posinfo → posinfo → span
whitespace-span pi pi'  = mk-span "Whitespace" pi pi' [ not-for-navigation ] nothing

comment-span : posinfo → posinfo → span
comment-span pi pi'  = mk-span "Comment" pi pi' [ not-for-navigation ] nothing

IotaPair-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
IotaPair-span pi pi' c tvs =
  mk-span "Iota pair" pi pi' (explain "Inhabit a iota-type (dependent intersection type)." :: checking-data c :: ll-data-term :: tvs)

IotaProj-span : term → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
IotaProj-span t pi' c tvs = mk-span "Iota projection" (term-start-pos t) pi' (checking-data c :: ll-data-term :: tvs)

-- <<<<<<< HEAD
Let-span : ctxt → checking-mode → posinfo → posinfo → forceErased → var → (atk : tk) → (if tk-is-type atk then term else type) → term → 𝕃 tagged-val → err-m → span
Let-span Γ c pi pi' fe x atk val t' tvs =
  mk-span name pi (term-end-pos t') (binder-data Γ pi' x atk ff (just val) (term-start-pos t') (term-end-pos t') :: ll-data-term :: checking-data c :: tvs)
  where name = if fe then "Erased Term Let" else "Term Let"
-- =======
-- Let-span : ctxt → checking-mode → posinfo → forceErased → defTermOrType → term → 𝕃 tagged-val → err-m → span
-- Let-span Γ c pi fe d t' tvs = mk-span name pi (term-end-pos t') (binder-data-const :: bound-data d Γ :: ll-data-term :: checking-data c :: tvs)
--   where name = if fe then "Erased Term Let" else "Term Let"
-- >>>>>>> master

TpLet-span : ctxt → checking-mode → posinfo → posinfo → var → (atk : tk) → (if tk-is-type atk then term else type) → type → 𝕃 tagged-val → err-m → span
TpLet-span Γ c pi pi' x atk val t' tvs =
  mk-span "Type Let" pi (type-end-pos t') (binder-data Γ pi' x atk ff (just val) (type-start-pos t') (type-end-pos t') :: ll-data-type :: checking-data c :: tvs)

max_stars_repo_name: CarlOlson/cedille

max_issues_repo_name: CarlOlson/cedille

max_forks_repo_name: CarlOlson/cedille


text:
module Issue2749-2 where

-- testing unicode lambda and arrow
id : {A : Set} -> A -> A
id = {!!}

-- testing unicode double braces
it : {A : Set} {{a : A}} → A → A
it = {!!}

data B : Set where
  mkB : B → B → B

-- testing unicode suffixes
left : B → B
left b₁ = {!!}

open import Agda.Builtin.Equality

-- testing ascii only forall
allq : (∀ m n → m ≡ n) ≡ {!!}
allq = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Coinduction using ( ♯_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; cong ; subst )
open import System.IO.Transducers.Lazy using ( _⇒_ ; inp ; out ; done ; ⟦_⟧ ; _≃_ )
open import System.IO.Transducers.Strict using ( Strict )
open import System.IO.Transducers.Session using ( Session ; I ; Σ ; _/_ )
open import System.IO.Transducers.Trace using ( Trace ; [] ; _∷_ ; _✓ ; _⊑_ )
open import System.IO.Transducers.Properties.Lemmas using ( I-η ; ⟦⟧-mono ; ⟦⟧-resp-✓ ; ⟦⟧-resp-[] )
open import System.IO.Transducers.Properties.Category using ( _≣_ ; ⟦⟧-refl-≣ )

module System.IO.Transducers.Properties.Equivalences where

open Relation.Binary.PropositionalEquality.≡-Reasoning

_//_ : ∀ S → (Trace S) → Session
S // [] = S
S // (a ∷ as) = (S / a) // as

suffix : ∀ {S} {as bs : Trace S} → (as ⊑ bs) → (Trace (S // as))
suffix {bs = bs} [] = bs
suffix (a ∷ as⊑bs) = suffix as⊑bs

_+++_ : ∀ {S} (as : Trace S) (bs : Trace (S // as)) → (Trace S)
[]       +++ bs = bs
(a ∷ as) +++ bs = a ∷ (as +++ bs)

suffix-+++ : ∀ {S} {as : Trace S} {bs} (as⊑bs : as ⊑ bs) →
  as +++ suffix as⊑bs ≡ bs
suffix-+++ []          = refl
suffix-+++ (a ∷ as⊑bs) = cong (_∷_ a) (suffix-+++ as⊑bs)

suffix-mono : ∀ {S} {as : Trace S} {bs cs} (as⊑bs : as ⊑ bs) (as⊑cs : as ⊑ cs) →
  (bs ⊑ cs) → (suffix as⊑bs ⊑ suffix as⊑cs)
suffix-mono []           []           bs⊑cs       = bs⊑cs
suffix-mono (.a ∷ as⊑bs) (.a ∷ as⊑cs) (a ∷ bs⊑cs) = suffix-mono as⊑bs as⊑cs bs⊑cs

suffix-resp-✓ : ∀ {S} {as : Trace S} {bs} (as⊑bs : as ⊑ bs) →
  (bs ✓) → (suffix as⊑bs ✓)
suffix-resp-✓ []           bs✓       = bs✓
suffix-resp-✓ (.a ∷ as⊑bs) (a ∷ bs✓) = suffix-resp-✓ as⊑bs bs✓

suffix-[] : ∀ {S} {as : Trace S} (as⊑as : as ⊑ as) →
  (suffix as⊑as ≡ [])
suffix-[] [] = refl
suffix-[] (a ∷ as⊑as) = suffix-[] as⊑as

strictify : ∀ {S T} (f : Trace S → Trace T) →
  (∀ as bs → as ⊑ bs → f as ⊑ f bs) →
    (Trace S → Trace (T // f []))
strictify f f-mono as = suffix (f-mono [] as [])

lazify : ∀ {S T} (f : Trace S → Trace T) a →
  (Trace (S / a) → Trace T)
lazify f a as = f (a ∷ as)

strictify-mono : ∀ {S T} (f : Trace S → Trace T) f-mono →
  (∀ as bs → as ⊑ bs → strictify f f-mono as ⊑ strictify f f-mono bs)
strictify-mono f f-mono as bs as⊑bs = suffix-mono (f-mono [] as []) (f-mono [] bs []) (f-mono as bs as⊑bs)

strictify-resp-✓ : ∀ {S T} (f : Trace S → Trace T) f-mono →
  (∀ as → as ✓ → f as ✓) →
    (∀ as → as ✓ → strictify f f-mono as ✓)
strictify-resp-✓ f f-mono f-resp-✓ as as✓ = suffix-resp-✓ (f-mono [] as []) (f-resp-✓ as as✓)

strictify-strict : ∀ {S T} (f : Trace S → Trace T) f-mono →
  (strictify f f-mono [] ≡ [])
strictify-strict f f-mono = suffix-[] (f-mono [] [] [])

lazify-mono : ∀ {S T} (f : Trace S → Trace T) a →
  (∀ as bs → as ⊑ bs → f as ⊑ f bs) →
    (∀ as bs → as ⊑ bs → lazify f a as ⊑ lazify f a bs)
lazify-mono f a f-mono as bs as⊑bs = f-mono (a ∷ as) (a ∷ bs) (a ∷ as⊑bs)

lazify-resp-✓ : ∀ {S T} (f : Trace S → Trace T) a →
  (∀ as → as ✓ → f as ✓) →
    (∀ as → as ✓ → lazify f a as ✓)
lazify-resp-✓ f a f-resp-✓ as as✓ = f-resp-✓ (a ∷ as) (a ∷ as✓)

mutual

  lazy' : ∀ {T S} bs (f : Trace S → Trace (T // bs)) →
    (∀ as bs → as ⊑ bs → f as ⊑ f bs) →
      (∀ as → as ✓ → f as ✓) → (f [] ≡ []) →
        (S ⇒ T)
  lazy' [] f f-mono f-resp-✓ f-strict = strict f f-mono f-resp-✓ f-strict
  lazy' {Σ V F} (b ∷ bs) f f-mono f-resp-✓ f-strict = out b (lazy' bs f f-mono f-resp-✓ f-strict)
  lazy' {I} (() ∷ bs) f f-mono f-resp-✓ f-strict

  lazy : ∀ {T S} (f : Trace S → Trace T) →
    (∀ as bs → as ⊑ bs → f as ⊑ f bs) →
      (∀ as → as ✓ → f as ✓) →
        (S ⇒ T)
  lazy f f-mono f-resp-✓ = lazy' (f []) (strictify f f-mono) (strictify-mono f f-mono) (strictify-resp-✓ f f-mono f-resp-✓) (strictify-strict f f-mono)

  strict : ∀ {S T} (f : Trace S → Trace T) →
    (∀ as bs → as ⊑ bs → f as ⊑ f bs) →
      (∀ as → as ✓ → f as ✓) → (f [] ≡ []) →
        (S ⇒ T)
  strict {I} {I} f f-mono f-resp-✓ f-strict = done
  strict {Σ V F} f f-mono f-resp-✓ f-strict = inp (♯ λ a → lazy (lazify f a) (lazify-mono f a f-mono) (lazify-resp-✓ f a f-resp-✓))
  strict {I} {Σ W G} f f-mono f-resp-✓ f-strict with subst _✓ f-strict (f-resp-✓ [] [])
  strict {I} {Σ W G} f f-mono f-resp-✓ f-strict | ()

mutual

  lazy'-⟦⟧ : ∀ {T S} bs (f : Trace S → Trace (T // bs)) f-mono f-resp-✓ f-strict →
    ∀ as → ⟦ lazy' bs f f-mono f-resp-✓ f-strict ⟧ as ≡ bs +++ f as
  lazy'-⟦⟧ [] f f-mono f-resp-✓ f-strict as = strict-⟦⟧ f f-mono f-resp-✓ f-strict as
  lazy'-⟦⟧ {Σ W G} (b ∷ bs)  f f-mono f-resp-✓ f-strict as = cong (_∷_ b) (lazy'-⟦⟧ bs f f-mono f-resp-✓ f-strict as)
  lazy'-⟦⟧ {I}     (() ∷ bs) f f-mono f-resp-✓ f-strict as

  lazy-⟦⟧ : ∀ {S T} (f : Trace S → Trace T) f-mono f-resp-✓ →
    ⟦ lazy f f-mono f-resp-✓ ⟧ ≃ f
  lazy-⟦⟧ f f-mono f-resp-✓ as =
    begin
      ⟦ lazy f f-mono f-resp-✓ ⟧ as
    ≡⟨ lazy'-⟦⟧ (f []) (strictify f f-mono) (strictify-mono f f-mono) (strictify-resp-✓ f f-mono f-resp-✓) (strictify-strict f f-mono) as ⟩
      f [] +++ strictify f f-mono as
    ≡⟨ suffix-+++ (f-mono [] as []) ⟩
      f as
    ∎

  strict-⟦⟧ : ∀ {S T} (f : Trace S → Trace T) f-mono f-resp-✓ f-strict →
    ⟦ strict f f-mono f-resp-✓ f-strict ⟧ ≃ f
  strict-⟦⟧ {I} {I} f f-mono f-resp-✓ f-strict [] = sym (I-η (f []))
  strict-⟦⟧ {Σ V F} f f-mono f-resp-✓ f-strict [] = sym f-strict
  strict-⟦⟧ {Σ V F} f f-mono f-resp-✓ f-strict (a ∷ as) = lazy-⟦⟧ (lazify f a) (lazify-mono f a f-mono) (lazify-resp-✓ f a f-resp-✓) as
  strict-⟦⟧ {I} {Σ W G} f f-mono f-resp-✓ f-strict as with subst _✓ f-strict (f-resp-✓ [] [])
  strict-⟦⟧ {I} {Σ W G} f f-mono f-resp-✓ f-strict as | ()
  strict-⟦⟧ {I} f f-mono f-resp-✓ f-strict (() ∷ as)

⟦⟧-lazy : ∀ {S T} (P : S ⇒ T) →
  lazy ⟦ P ⟧ (⟦⟧-mono P) (⟦⟧-resp-✓ P) ≣ P
⟦⟧-lazy P = ⟦⟧-refl-≣ (lazy ⟦ P ⟧ (⟦⟧-mono P) (⟦⟧-resp-✓ P)) P (lazy-⟦⟧ ⟦ P ⟧ (⟦⟧-mono P) (⟦⟧-resp-✓ P))

⟦⟧-strict : ∀ {S T} (P : S ⇒ T) (#P : Strict P) →
  strict ⟦ P ⟧ (⟦⟧-mono P) (⟦⟧-resp-✓ P) (⟦⟧-resp-[] #P) ≣ P
⟦⟧-strict P #P = ⟦⟧-refl-≣ (strict ⟦ P ⟧ (⟦⟧-mono P) (⟦⟧-resp-✓ P) (⟦⟧-resp-[] #P)) P (strict-⟦⟧ ⟦ P ⟧ (⟦⟧-mono P) (⟦⟧-resp-✓ P) (⟦⟧-resp-[] #P))

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
module Text.Greek.SBLGNT.3John where

open import Data.List
open import Text.Greek.Bible
open import Text.Greek.Script
open import Text.Greek.Script.Unicode

ΙΩΑΝΝΟΥ-Γ : List (Word)
ΙΩΑΝΝΟΥ-Γ =
    word (Ὁ ∷ []) "3John.1.1"
  ∷ word (π ∷ ρ ∷ ε ∷ σ ∷ β ∷ ύ ∷ τ ∷ ε ∷ ρ ∷ ο ∷ ς ∷ []) "3John.1.1"
  ∷ word (Γ ∷ α ∷ ΐ ∷ ῳ ∷ []) "3John.1.1"
  ∷ word (τ ∷ ῷ ∷ []) "3John.1.1"
  ∷ word (ἀ ∷ γ ∷ α ∷ π ∷ η ∷ τ ∷ ῷ ∷ []) "3John.1.1"
  ∷ word (ὃ ∷ ν ∷ []) "3John.1.1"
  ∷ word (ἐ ∷ γ ∷ ὼ ∷ []) "3John.1.1"
  ∷ word (ἀ ∷ γ ∷ α ∷ π ∷ ῶ ∷ []) "3John.1.1"
  ∷ word (ἐ ∷ ν ∷ []) "3John.1.1"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ ᾳ ∷ []) "3John.1.1"
  ∷ word (Ἀ ∷ γ ∷ α ∷ π ∷ η ∷ τ ∷ έ ∷ []) "3John.1.2"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "3John.1.2"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "3John.1.2"
  ∷ word (ε ∷ ὔ ∷ χ ∷ ο ∷ μ ∷ α ∷ ί ∷ []) "3John.1.2"
  ∷ word (σ ∷ ε ∷ []) "3John.1.2"
  ∷ word (ε ∷ ὐ ∷ ο ∷ δ ∷ ο ∷ ῦ ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "3John.1.2"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "3John.1.2"
  ∷ word (ὑ ∷ γ ∷ ι ∷ α ∷ ί ∷ ν ∷ ε ∷ ι ∷ ν ∷ []) "3John.1.2"
  ∷ word (κ ∷ α ∷ θ ∷ ὼ ∷ ς ∷ []) "3John.1.2"
  ∷ word (ε ∷ ὐ ∷ ο ∷ δ ∷ ο ∷ ῦ ∷ τ ∷ α ∷ ί ∷ []) "3John.1.2"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "3John.1.2"
  ∷ word (ἡ ∷ []) "3John.1.2"
  ∷ word (ψ ∷ υ ∷ χ ∷ ή ∷ []) "3John.1.2"
  ∷ word (ἐ ∷ χ ∷ ά ∷ ρ ∷ η ∷ ν ∷ []) "3John.1.3"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "3John.1.3"
  ∷ word (∙λ ∷ ί ∷ α ∷ ν ∷ []) "3John.1.3"
  ∷ word (ἐ ∷ ρ ∷ χ ∷ ο ∷ μ ∷ έ ∷ ν ∷ ω ∷ ν ∷ []) "3John.1.3"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ῶ ∷ ν ∷ []) "3John.1.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "3John.1.3"
  ∷ word (μ ∷ α ∷ ρ ∷ τ ∷ υ ∷ ρ ∷ ο ∷ ύ ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "3John.1.3"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "3John.1.3"
  ∷ word (τ ∷ ῇ ∷ []) "3John.1.3"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ ᾳ ∷ []) "3John.1.3"
  ∷ word (κ ∷ α ∷ θ ∷ ὼ ∷ ς ∷ []) "3John.1.3"
  ∷ word (σ ∷ ὺ ∷ []) "3John.1.3"
  ∷ word (ἐ ∷ ν ∷ []) "3John.1.3"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ ᾳ ∷ []) "3John.1.3"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ π ∷ α ∷ τ ∷ ε ∷ ῖ ∷ ς ∷ []) "3John.1.3"
  ∷ word (μ ∷ ε ∷ ι ∷ ζ ∷ ο ∷ τ ∷ έ ∷ ρ ∷ α ∷ ν ∷ []) "3John.1.4"
  ∷ word (τ ∷ ο ∷ ύ ∷ τ ∷ ω ∷ ν ∷ []) "3John.1.4"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "3John.1.4"
  ∷ word (ἔ ∷ χ ∷ ω ∷ []) "3John.1.4"
  ∷ word (χ ∷ α ∷ ρ ∷ ά ∷ ν ∷ []) "3John.1.4"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "3John.1.4"
  ∷ word (ἀ ∷ κ ∷ ο ∷ ύ ∷ ω ∷ []) "3John.1.4"
  ∷ word (τ ∷ ὰ ∷ []) "3John.1.4"
  ∷ word (ἐ ∷ μ ∷ ὰ ∷ []) "3John.1.4"
  ∷ word (τ ∷ έ ∷ κ ∷ ν ∷ α ∷ []) "3John.1.4"
  ∷ word (ἐ ∷ ν ∷ []) "3John.1.4"
  ∷ word (τ ∷ ῇ ∷ []) "3John.1.4"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ ᾳ ∷ []) "3John.1.4"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ π ∷ α ∷ τ ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ α ∷ []) "3John.1.4"
  ∷ word (Ἀ ∷ γ ∷ α ∷ π ∷ η ∷ τ ∷ έ ∷ []) "3John.1.5"
  ∷ word (π ∷ ι ∷ σ ∷ τ ∷ ὸ ∷ ν ∷ []) "3John.1.5"
  ∷ word (π ∷ ο ∷ ι ∷ ε ∷ ῖ ∷ ς ∷ []) "3John.1.5"
  ∷ word (ὃ ∷ []) "3John.1.5"
  ∷ word (ἐ ∷ ὰ ∷ ν ∷ []) "3John.1.5"
  ∷ word (ἐ ∷ ρ ∷ γ ∷ ά ∷ σ ∷ ῃ ∷ []) "3John.1.5"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "3John.1.5"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "3John.1.5"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ο ∷ ὺ ∷ ς ∷ []) "3John.1.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "3John.1.5"
  ∷ word (τ ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ []) "3John.1.5"
  ∷ word (ξ ∷ έ ∷ ν ∷ ο ∷ υ ∷ ς ∷ []) "3John.1.5"
  ∷ word (ο ∷ ἳ ∷ []) "3John.1.6"
  ∷ word (ἐ ∷ μ ∷ α ∷ ρ ∷ τ ∷ ύ ∷ ρ ∷ η ∷ σ ∷ ά ∷ ν ∷ []) "3John.1.6"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "3John.1.6"
  ∷ word (τ ∷ ῇ ∷ []) "3John.1.6"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ ῃ ∷ []) "3John.1.6"
  ∷ word (ἐ ∷ ν ∷ ώ ∷ π ∷ ι ∷ ο ∷ ν ∷ []) "3John.1.6"
  ∷ word (ἐ ∷ κ ∷ κ ∷ ∙λ ∷ η ∷ σ ∷ ί ∷ α ∷ ς ∷ []) "3John.1.6"
  ∷ word (ο ∷ ὓ ∷ ς ∷ []) "3John.1.6"
  ∷ word (κ ∷ α ∷ ∙λ ∷ ῶ ∷ ς ∷ []) "3John.1.6"
  ∷ word (π ∷ ο ∷ ι ∷ ή ∷ σ ∷ ε ∷ ι ∷ ς ∷ []) "3John.1.6"
  ∷ word (π ∷ ρ ∷ ο ∷ π ∷ έ ∷ μ ∷ ψ ∷ α ∷ ς ∷ []) "3John.1.6"
  ∷ word (ἀ ∷ ξ ∷ ί ∷ ω ∷ ς ∷ []) "3John.1.6"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "3John.1.6"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "3John.1.6"
  ∷ word (ὑ ∷ π ∷ ὲ ∷ ρ ∷ []) "3John.1.7"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "3John.1.7"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "3John.1.7"
  ∷ word (ὀ ∷ ν ∷ ό ∷ μ ∷ α ∷ τ ∷ ο ∷ ς ∷ []) "3John.1.7"
  ∷ word (ἐ ∷ ξ ∷ ῆ ∷ ∙λ ∷ θ ∷ ο ∷ ν ∷ []) "3John.1.7"
  ∷ word (μ ∷ η ∷ δ ∷ ὲ ∷ ν ∷ []) "3John.1.7"
  ∷ word (∙λ ∷ α ∷ μ ∷ β ∷ ά ∷ ν ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "3John.1.7"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "3John.1.7"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "3John.1.7"
  ∷ word (ἐ ∷ θ ∷ ν ∷ ι ∷ κ ∷ ῶ ∷ ν ∷ []) "3John.1.7"
  ∷ word (ἡ ∷ μ ∷ ε ∷ ῖ ∷ ς ∷ []) "3John.1.8"
  ∷ word (ο ∷ ὖ ∷ ν ∷ []) "3John.1.8"
  ∷ word (ὀ ∷ φ ∷ ε ∷ ί ∷ ∙λ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "3John.1.8"
  ∷ word (ὑ ∷ π ∷ ο ∷ ∙λ ∷ α ∷ μ ∷ β ∷ ά ∷ ν ∷ ε ∷ ι ∷ ν ∷ []) "3John.1.8"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "3John.1.8"
  ∷ word (τ ∷ ο ∷ ι ∷ ο ∷ ύ ∷ τ ∷ ο ∷ υ ∷ ς ∷ []) "3John.1.8"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "3John.1.8"
  ∷ word (σ ∷ υ ∷ ν ∷ ε ∷ ρ ∷ γ ∷ ο ∷ ὶ ∷ []) "3John.1.8"
  ∷ word (γ ∷ ι ∷ ν ∷ ώ ∷ μ ∷ ε ∷ θ ∷ α ∷ []) "3John.1.8"
  ∷ word (τ ∷ ῇ ∷ []) "3John.1.8"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ ᾳ ∷ []) "3John.1.8"
  ∷ word (Ἔ ∷ γ ∷ ρ ∷ α ∷ ψ ∷ ά ∷ []) "3John.1.9"
  ∷ word (τ ∷ ι ∷ []) "3John.1.9"
  ∷ word (τ ∷ ῇ ∷ []) "3John.1.9"
  ∷ word (ἐ ∷ κ ∷ κ ∷ ∙λ ∷ η ∷ σ ∷ ί ∷ ᾳ ∷ []) "3John.1.9"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ []) "3John.1.9"
  ∷ word (ὁ ∷ []) "3John.1.9"
  ∷ word (φ ∷ ι ∷ ∙λ ∷ ο ∷ π ∷ ρ ∷ ω ∷ τ ∷ ε ∷ ύ ∷ ω ∷ ν ∷ []) "3John.1.9"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῶ ∷ ν ∷ []) "3John.1.9"
  ∷ word (Δ ∷ ι ∷ ο ∷ τ ∷ ρ ∷ έ ∷ φ ∷ η ∷ ς ∷ []) "3John.1.9"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "3John.1.9"
  ∷ word (ἐ ∷ π ∷ ι ∷ δ ∷ έ ∷ χ ∷ ε ∷ τ ∷ α ∷ ι ∷ []) "3John.1.9"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "3John.1.9"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "3John.1.10"
  ∷ word (τ ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ []) "3John.1.10"
  ∷ word (ἐ ∷ ὰ ∷ ν ∷ []) "3John.1.10"
  ∷ word (ἔ ∷ ∙λ ∷ θ ∷ ω ∷ []) "3John.1.10"
  ∷ word (ὑ ∷ π ∷ ο ∷ μ ∷ ν ∷ ή ∷ σ ∷ ω ∷ []) "3John.1.10"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "3John.1.10"
  ∷ word (τ ∷ ὰ ∷ []) "3John.1.10"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ α ∷ []) "3John.1.10"
  ∷ word (ἃ ∷ []) "3John.1.10"
  ∷ word (π ∷ ο ∷ ι ∷ ε ∷ ῖ ∷ []) "3John.1.10"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ ι ∷ ς ∷ []) "3John.1.10"
  ∷ word (π ∷ ο ∷ ν ∷ η ∷ ρ ∷ ο ∷ ῖ ∷ ς ∷ []) "3John.1.10"
  ∷ word (φ ∷ ∙λ ∷ υ ∷ α ∷ ρ ∷ ῶ ∷ ν ∷ []) "3John.1.10"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "3John.1.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "3John.1.10"
  ∷ word (μ ∷ ὴ ∷ []) "3John.1.10"
  ∷ word (ἀ ∷ ρ ∷ κ ∷ ο ∷ ύ ∷ μ ∷ ε ∷ ν ∷ ο ∷ ς ∷ []) "3John.1.10"
  ∷ word (ἐ ∷ π ∷ ὶ ∷ []) "3John.1.10"
  ∷ word (τ ∷ ο ∷ ύ ∷ τ ∷ ο ∷ ι ∷ ς ∷ []) "3John.1.10"
  ∷ word (ο ∷ ὔ ∷ τ ∷ ε ∷ []) "3John.1.10"
  ∷ word (α ∷ ὐ ∷ τ ∷ ὸ ∷ ς ∷ []) "3John.1.10"
  ∷ word (ἐ ∷ π ∷ ι ∷ δ ∷ έ ∷ χ ∷ ε ∷ τ ∷ α ∷ ι ∷ []) "3John.1.10"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "3John.1.10"
  ∷ word (ἀ ∷ δ ∷ ε ∷ ∙λ ∷ φ ∷ ο ∷ ὺ ∷ ς ∷ []) "3John.1.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "3John.1.10"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "3John.1.10"
  ∷ word (β ∷ ο ∷ υ ∷ ∙λ ∷ ο ∷ μ ∷ έ ∷ ν ∷ ο ∷ υ ∷ ς ∷ []) "3John.1.10"
  ∷ word (κ ∷ ω ∷ ∙λ ∷ ύ ∷ ε ∷ ι ∷ []) "3John.1.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "3John.1.10"
  ∷ word (ἐ ∷ κ ∷ []) "3John.1.10"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "3John.1.10"
  ∷ word (ἐ ∷ κ ∷ κ ∷ ∙λ ∷ η ∷ σ ∷ ί ∷ α ∷ ς ∷ []) "3John.1.10"
  ∷ word (ἐ ∷ κ ∷ β ∷ ά ∷ ∙λ ∷ ∙λ ∷ ε ∷ ι ∷ []) "3John.1.10"
  ∷ word (Ἀ ∷ γ ∷ α ∷ π ∷ η ∷ τ ∷ έ ∷ []) "3John.1.11"
  ∷ word (μ ∷ ὴ ∷ []) "3John.1.11"
  ∷ word (μ ∷ ι ∷ μ ∷ ο ∷ ῦ ∷ []) "3John.1.11"
  ∷ word (τ ∷ ὸ ∷ []) "3John.1.11"
  ∷ word (κ ∷ α ∷ κ ∷ ὸ ∷ ν ∷ []) "3John.1.11"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "3John.1.11"
  ∷ word (τ ∷ ὸ ∷ []) "3John.1.11"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ό ∷ ν ∷ []) "3John.1.11"
  ∷ word (ὁ ∷ []) "3John.1.11"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ο ∷ π ∷ ο ∷ ι ∷ ῶ ∷ ν ∷ []) "3John.1.11"
  ∷ word (ἐ ∷ κ ∷ []) "3John.1.11"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "3John.1.11"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "3John.1.11"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "3John.1.11"
  ∷ word (ὁ ∷ []) "3John.1.11"
  ∷ word (κ ∷ α ∷ κ ∷ ο ∷ π ∷ ο ∷ ι ∷ ῶ ∷ ν ∷ []) "3John.1.11"
  ∷ word (ο ∷ ὐ ∷ χ ∷ []) "3John.1.11"
  ∷ word (ἑ ∷ ώ ∷ ρ ∷ α ∷ κ ∷ ε ∷ ν ∷ []) "3John.1.11"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "3John.1.11"
  ∷ word (θ ∷ ε ∷ ό ∷ ν ∷ []) "3John.1.11"
  ∷ word (Δ ∷ η ∷ μ ∷ η ∷ τ ∷ ρ ∷ ί ∷ ῳ ∷ []) "3John.1.12"
  ∷ word (μ ∷ ε ∷ μ ∷ α ∷ ρ ∷ τ ∷ ύ ∷ ρ ∷ η ∷ τ ∷ α ∷ ι ∷ []) "3John.1.12"
  ∷ word (ὑ ∷ π ∷ ὸ ∷ []) "3John.1.12"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "3John.1.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "3John.1.12"
  ∷ word (ὑ ∷ π ∷ ὸ ∷ []) "3John.1.12"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῆ ∷ ς ∷ []) "3John.1.12"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "3John.1.12"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "3John.1.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "3John.1.12"
  ∷ word (ἡ ∷ μ ∷ ε ∷ ῖ ∷ ς ∷ []) "3John.1.12"
  ∷ word (δ ∷ ὲ ∷ []) "3John.1.12"
  ∷ word (μ ∷ α ∷ ρ ∷ τ ∷ υ ∷ ρ ∷ ο ∷ ῦ ∷ μ ∷ ε ∷ ν ∷ []) "3John.1.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "3John.1.12"
  ∷ word (ο ∷ ἶ ∷ δ ∷ α ∷ ς ∷ []) "3John.1.12"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "3John.1.12"
  ∷ word (ἡ ∷ []) "3John.1.12"
  ∷ word (μ ∷ α ∷ ρ ∷ τ ∷ υ ∷ ρ ∷ ί ∷ α ∷ []) "3John.1.12"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "3John.1.12"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ή ∷ ς ∷ []) "3John.1.12"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "3John.1.12"
  ∷ word (Π ∷ ο ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "3John.1.13"
  ∷ word (ε ∷ ἶ ∷ χ ∷ ο ∷ ν ∷ []) "3John.1.13"
  ∷ word (γ ∷ ρ ∷ ά ∷ ψ ∷ α ∷ ι ∷ []) "3John.1.13"
  ∷ word (σ ∷ ο ∷ ι ∷ []) "3John.1.13"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ []) "3John.1.13"
  ∷ word (ο ∷ ὐ ∷ []) "3John.1.13"
  ∷ word (θ ∷ έ ∷ ∙λ ∷ ω ∷ []) "3John.1.13"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "3John.1.13"
  ∷ word (μ ∷ έ ∷ ∙λ ∷ α ∷ ν ∷ ο ∷ ς ∷ []) "3John.1.13"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "3John.1.13"
  ∷ word (κ ∷ α ∷ ∙λ ∷ ά ∷ μ ∷ ο ∷ υ ∷ []) "3John.1.13"
  ∷ word (σ ∷ ο ∷ ι ∷ []) "3John.1.13"
  ∷ word (γ ∷ ρ ∷ ά ∷ φ ∷ ε ∷ ι ∷ ν ∷ []) "3John.1.13"
  ∷ word (ἐ ∷ ∙λ ∷ π ∷ ί ∷ ζ ∷ ω ∷ []) "3John.1.14"
  ∷ word (δ ∷ ὲ ∷ []) "3John.1.14"
  ∷ word (ε ∷ ὐ ∷ θ ∷ έ ∷ ω ∷ ς ∷ []) "3John.1.14"
  ∷ word (σ ∷ ε ∷ []) "3John.1.14"
  ∷ word (ἰ ∷ δ ∷ ε ∷ ῖ ∷ ν ∷ []) "3John.1.14"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "3John.1.14"
  ∷ word (σ ∷ τ ∷ ό ∷ μ ∷ α ∷ []) "3John.1.14"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "3John.1.14"
  ∷ word (σ ∷ τ ∷ ό ∷ μ ∷ α ∷ []) "3John.1.14"
  ∷ word (∙λ ∷ α ∷ ∙λ ∷ ή ∷ σ ∷ ο ∷ μ ∷ ε ∷ ν ∷ []) "3John.1.14"
  ∷ word (Ε ∷ ἰ ∷ ρ ∷ ή ∷ ν ∷ η ∷ []) "3John.1.15"
  ∷ word (σ ∷ ο ∷ ι ∷ []) "3John.1.15"
  ∷ word (ἀ ∷ σ ∷ π ∷ ά ∷ ζ ∷ ο ∷ ν ∷ τ ∷ α ∷ ί ∷ []) "3John.1.15"
  ∷ word (σ ∷ ε ∷ []) "3John.1.15"
  ∷ word (ο ∷ ἱ ∷ []) "3John.1.15"
  ∷ word (φ ∷ ί ∷ ∙λ ∷ ο ∷ ι ∷ []) "3John.1.15"
  ∷ word (ἀ ∷ σ ∷ π ∷ ά ∷ ζ ∷ ο ∷ υ ∷ []) "3John.1.15"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "3John.1.15"
  ∷ word (φ ∷ ί ∷ ∙λ ∷ ο ∷ υ ∷ ς ∷ []) "3John.1.15"
  ∷ word (κ ∷ α ∷ τ ∷ []) "3John.1.15"
  ∷ word (ὄ ∷ ν ∷ ο ∷ μ ∷ α ∷ []) "3John.1.15"
  ∷ []

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


text: module Dummy where