text:
import cedille-options
open import general-util

module untyped-spans (options : cedille-options.options) {F : Set → Set} {{monadF : monad F}} where

open import lib
open import ctxt
open import cedille-types
open import conversion
open import spans options {F}
open import syntax-util
open import to-string options
open import is-free

{-# TERMINATING #-}
untyped-term-spans : term → spanM ⊤
untyped-type-spans : type → spanM ⊤
untyped-kind-spans : kind → spanM ⊤
untyped-tk-spans : tk → spanM ⊤
untyped-liftingType-spans : liftingType → spanM ⊤
untyped-optTerm-spans : optTerm → spanM (posinfo → posinfo)
untyped-optType-spans : optType → spanM ⊤
untyped-optGuide-spans : optGuide → spanM (𝕃 tagged-val)
untyped-lterms-spans : lterms → spanM ⊤
untyped-optClass-spans : optClass → spanM ⊤
untyped-defTermOrType-spans : posinfo → (ctxt → posinfo → var → (atk : tk) → (if tk-is-type atk then term else type) → span) → defTermOrType → spanM ⊤ → spanM ⊤
untyped-var-spans : posinfo → var → (ctxt → posinfo → var → checking-mode → 𝕃 tagged-val → err-m → span) → spanM ⊤ → spanM ⊤
untyped-caseArgs-spans : caseArgs → (body : term) → spanM (𝕃 tagged-val)
untyped-case-spans : case → (ℕ → ℕ → err-m) → spanM ((ℕ → ℕ → err-m) × 𝕃 tagged-val)
untyped-cases-spans : cases → spanM (err-m × 𝕃 tagged-val)

untyped-var-spans pi x f m = get-ctxt λ Γ → with-ctxt (ctxt-var-decl-loc pi x Γ) (get-ctxt λ Γ → spanM-add (f Γ pi x untyped [] nothing) ≫span m)

untyped-term-spans (App t me t') = untyped-term-spans t ≫span untyped-term-spans t' ≫span spanM-add (App-span ff t t' untyped [] nothing)
untyped-term-spans (AppTp t T) = untyped-term-spans t ≫span untyped-type-spans T ≫span spanM-add (AppTp-span t T untyped [] nothing)
untyped-term-spans (Beta pi ot ot') = untyped-optTerm-spans ot ≫=span λ f → untyped-optTerm-spans ot' ≫=span λ f' → spanM-add (Beta-span pi (f' (f (posinfo-plus pi 1))) untyped [] nothing)
untyped-term-spans (Chi pi mT t) = untyped-optType-spans mT ≫span untyped-term-spans t ≫span get-ctxt λ Γ → spanM-add (Chi-span Γ pi mT t untyped [] nothing)
untyped-term-spans (Delta pi mT t) = untyped-optType-spans mT ≫span untyped-term-spans t ≫span get-ctxt λ Γ → spanM-add (Delta-span Γ pi mT t untyped [] nothing)
untyped-term-spans (Epsilon pi lr mm t) = untyped-term-spans t ≫span spanM-add (Epsilon-span pi lr mm t untyped [] nothing)
untyped-term-spans (Hole pi) = get-ctxt λ Γ → spanM-add (hole-span Γ pi nothing [])
untyped-term-spans (IotaPair pi t t' og pi') = untyped-term-spans t ≫span untyped-term-spans t' ≫span untyped-optGuide-spans og ≫=span λ tvs → spanM-add (IotaPair-span pi pi' untyped tvs nothing)
untyped-term-spans (IotaProj t n pi) = untyped-term-spans t ≫span spanM-add (IotaProj-span t pi untyped [] nothing)
untyped-term-spans (Lam pi me pi' x oc t) =
  untyped-optClass-spans oc
  ≫span get-ctxt λ Γ → spanM-add (Lam-span Γ untyped pi pi' me x (Tkt $ TpHole pi) t [] occursCheck)
  ≫span untyped-var-spans pi' x Var-span (untyped-term-spans t)
  where
  occursCheck = maybe-if (me && is-free-in skip-erased x t) ≫maybe just "The bound variable occurs free in the erasure of the body (not allowed)"
untyped-term-spans (Let pi fe d t) =
  untyped-defTermOrType-spans pi (λ Γ pi' x atk val → Let-span Γ untyped pi pi' fe x atk val t [] nothing) d (untyped-term-spans t)
  -- ≫span get-ctxt λ Γ → spanM-add (Let-span Γ untyped pi d t [] nothing)
untyped-term-spans (Open pi o pi' x t) = get-ctxt λ Γ → spanM-add (Open-span Γ o pi' x t untyped [] nothing) ≫span spanM-add (Var-span Γ pi' x untyped [] (maybe-not (ctxt-lookup-term-loc Γ x) ≫maybe just "This term variable is not currently in scope")) ≫span untyped-term-spans t
untyped-term-spans (Parens pi t pi') = untyped-term-spans t
untyped-term-spans (Phi pi t t' t'' pi') = untyped-term-spans t ≫span untyped-term-spans t' ≫span untyped-term-spans t'' ≫span spanM-add (Phi-span pi pi' untyped [] nothing)
untyped-term-spans (Rho pi op on t og t') = untyped-term-spans t ≫span untyped-term-spans t' ≫span untyped-optGuide-spans og ≫=span λ tvs → spanM-add (mk-span "Rho" pi (term-end-pos t') (ll-data-term :: checking-data untyped :: tvs) nothing)
untyped-term-spans (Sigma pi t) = untyped-term-spans t ≫span get-ctxt λ Γ → spanM-add (mk-span "Sigma" pi (term-end-pos t) (ll-data-term :: [ checking-data untyped ]) nothing)
untyped-term-spans (Theta pi θ t ls) = untyped-term-spans t ≫span untyped-lterms-spans ls ≫span get-ctxt λ Γ → spanM-add (Theta-span Γ pi θ t ls untyped [] nothing)
untyped-term-spans (Var pi x) = get-ctxt λ Γ →
  spanM-add (Var-span Γ pi x untyped [] (if ctxt-binds-var Γ x then nothing else just "This variable is not currently in scope."))
untyped-term-spans (Mu pi pi' x t ot pi'' cs pi''') = get-ctxt λ Γ → untyped-term-spans t ≫span with-ctxt (ctxt-var-decl x Γ) (get-ctxt λ Γ → spanM-add (Var-span Γ pi' x untyped [ binder-data (ctxt-var-decl-loc pi' x Γ) pi' x (Tkt (TpHole pi')) NotErased nothing pi'' pi''' ] nothing) ≫span untyped-cases-spans cs) ≫=span uncurry λ e ts → spanM-add (Mu-span Γ pi (just x) pi''' (optType-elim ot nothing just) untyped ts e)
untyped-term-spans (Mu' pi ot t oT pi' cs pi'') = get-ctxt λ Γ → untyped-optTerm-spans ot ≫span untyped-term-spans t ≫span untyped-optType-spans oT ≫span untyped-cases-spans cs ≫=span uncurry λ e ts → spanM-add (Mu-span Γ pi nothing pi'' (optType-elim oT nothing just) untyped ts e)

untyped-caseArgs-spans [] t = untyped-term-spans t ≫span spanMr []
untyped-caseArgs-spans (c :: cs) t with caseArg-to-var c
...| pi , x , me , ll =
  let e? = maybe-if (me && is-free-in skip-erased x (caseArgs-to-lams cs t)) ≫maybe
            just "The bound variable occurs free in the erasure of the body (not allowed)"
      f = if ll then Var-span else TpVar-span in
  get-ctxt λ Γ →
  spanM-add (f (ctxt-var-decl-loc pi x Γ) pi x untyped [] e?) ≫span
  with-ctxt (ctxt-var-decl x Γ) (untyped-caseArgs-spans cs t) ≫=span λ ts →
  spanMr (binder-data (ctxt-var-decl x Γ) pi x (if ll then Tkt (TpHole pi) else Tkk star) me nothing (term-start-pos t) (term-end-pos t) :: ts)

untyped-case-spans (Case pi x cas t) fₑ =
  get-ctxt λ Γ →
  let m = untyped-caseArgs-spans cas t
      x' = unqual-all (ctxt-get-qualif Γ) $ unqual-local x
      eᵤ = just $ "This is not a valid constructor name"
      eₗ = just $ "Constructor's datatype has a different number of constructors than " ^ x'
      eᵢ = just $ "This constructor overlaps with " ^ x' in
  case qual-lookup Γ x of λ where
    (just (as , ctr-def ps? T Cₗ cᵢ cₐ , _ , _)) →
      spanM-add (Var-span Γ pi x untyped [] $ fₑ Cₗ cᵢ) ≫span m ≫=span λ s →
      spanMr ((λ Cₗ' cᵢ' → if Cₗ =ℕ Cₗ' then if cᵢ =ℕ cᵢ' then eᵢ else nothing else eₗ) , s)
    _ →
      spanM-add (Var-span Γ pi x untyped [] eᵤ) ≫span m ≫=span λ s →
      spanMr ((λ _ _ → nothing) , s)

untyped-cases-spans ms =
  let eₗ = just $ "Constructor's datatype should have " ^ ℕ-to-string (length ms) ^
             " constructor" ^ (if 1 =ℕ length ms then "" else "s") in
  (λ c → foldr c (λ _ → spanMr (nothing , [])) ms λ Cₗ cᵢ → if Cₗ =ℕ length ms then nothing else eₗ)
  λ c m fₑ → untyped-case-spans c fₑ ≫=span uncurry λ e s →
               m e ≫=span (spanMr ∘ map-snd (s ++_))

untyped-type-spans (Abs pi me pi' x atk T) = untyped-tk-spans atk ≫span untyped-var-spans pi' x (if tk-is-type atk then Var-span else TpVar-span) (get-ctxt λ Γ → spanM-add (TpQuant-span Γ (~ me) pi pi' x atk T untyped [] nothing) ≫span untyped-type-spans T)
untyped-type-spans (Iota pi pi' x T T') = untyped-type-spans T ≫span untyped-var-spans pi' x TpVar-span (get-ctxt λ Γ → spanM-add (Iota-span Γ pi pi' x T' untyped [] nothing) ≫span untyped-type-spans T')
untyped-type-spans (Lft pi pi' x t lT) = untyped-liftingType-spans lT ≫span untyped-var-spans pi' x Var-span (get-ctxt λ Γ → spanM-add (Lft-span Γ pi pi' x t untyped [] nothing) ≫span untyped-term-spans t)
untyped-type-spans (NoSpans T pi) = spanMok
untyped-type-spans (TpApp T T') = untyped-type-spans T ≫span untyped-type-spans T' ≫span spanM-add (TpApp-span T T' untyped [] nothing)
untyped-type-spans (TpAppt T t) = untyped-type-spans T ≫span untyped-term-spans t ≫span spanM-add (TpAppt-span T t untyped [] nothing)
untyped-type-spans (TpArrow T a T') = untyped-type-spans T ≫span untyped-type-spans T' ≫span spanM-add (TpArrow-span T T' untyped [] nothing)
untyped-type-spans (TpEq pi t t' pi') = untyped-term-spans t ≫span untyped-term-spans t' ≫span spanM-add (TpEq-span pi t t' pi' untyped [] nothing)
untyped-type-spans (TpHole pi) = get-ctxt λ Γ → spanM-add (tp-hole-span Γ pi nothing [])
untyped-type-spans (TpLambda pi pi' x atk T) = untyped-tk-spans atk ≫span untyped-var-spans pi' x TpVar-span (get-ctxt λ Γ → spanM-add (TpLambda-span Γ pi pi' x atk T untyped [] nothing) ≫span untyped-type-spans T)
untyped-type-spans (TpParens pi T pi') = untyped-type-spans T
untyped-type-spans (TpVar pi x) = get-ctxt λ Γ →
  spanM-add (TpVar-span Γ pi x untyped [] (if ctxt-binds-var Γ x then nothing else just "This variable is not currently in scope."))
untyped-type-spans (TpLet pi d T) =
 untyped-defTermOrType-spans pi (λ Γ pi' x atk val → TpLet-span Γ untyped pi pi' x atk val T [] nothing) d (untyped-type-spans T)
 --≫span get-ctxt λ Γ → spanM-add (TpLet-span Γ untyped pi d T [] nothing)

untyped-kind-spans (KndArrow k k') = untyped-kind-spans k ≫span untyped-kind-spans k' ≫span spanM-add (KndArrow-span k k' untyped nothing)
untyped-kind-spans (KndParens pi k pi') = untyped-kind-spans k
untyped-kind-spans (KndPi pi pi' x atk k) = untyped-tk-spans atk ≫span untyped-var-spans pi' x (if tk-is-type atk then Var-span else TpVar-span) (get-ctxt λ Γ → spanM-add (KndPi-span Γ pi pi' x atk k untyped nothing) ≫span untyped-kind-spans k)
untyped-kind-spans (KndTpArrow T k) = untyped-type-spans T ≫span untyped-kind-spans k ≫span spanM-add (KndTpArrow-span T k untyped nothing)
untyped-kind-spans (KndVar pi x as) = get-ctxt λ Γ →
  spanM-add (KndVar-span Γ (pi , x) (kvar-end-pos pi x as) [] untyped [] (if ctxt-binds-var Γ x then nothing else just "This variable is not currently in scope."))
untyped-kind-spans (Star pi) = spanM-add (Star-span pi untyped nothing)

untyped-liftingType-spans lT = spanMok -- Unimplemented

untyped-tk-spans (Tkt T) = untyped-type-spans T
untyped-tk-spans (Tkk k) = untyped-kind-spans k

untyped-optTerm-spans NoTerm = spanMr λ pi → pi
untyped-optTerm-spans (SomeTerm t pi) = untyped-term-spans t ≫span spanMr λ _ → pi

untyped-optType-spans NoType = spanMok
untyped-optType-spans (SomeType T) = untyped-type-spans T

untyped-optGuide-spans NoGuide = spanMr []
untyped-optGuide-spans (Guide pi x T) = untyped-var-spans pi x Var-span (untyped-type-spans T) ≫span get-ctxt λ Γ → spanMr [ binder-data Γ pi x (Tkt $ TpHole pi) NotErased nothing (type-start-pos T) (type-end-pos T) ]

untyped-lterms-spans [] = spanMok
untyped-lterms-spans ((Lterm me t) :: ls) = untyped-term-spans t ≫span untyped-lterms-spans ls

untyped-optClass-spans NoClass = spanMok
untyped-optClass-spans (SomeClass atk) = untyped-tk-spans atk

untyped-defTermOrType-spans pi s (DefTerm pi' x NoType t) m =
  untyped-term-spans t ≫span
  get-ctxt λ Γ → with-ctxt (ctxt-var-decl-loc pi' x Γ) $
  get-ctxt λ Γ → spanM-add (s Γ pi' x (Tkt $ TpHole pi') t) ≫span
                 spanM-add (Var-span Γ pi' x untyped [] nothing) ≫span m
untyped-defTermOrType-spans pi s (DefTerm pi' x (SomeType tp) t) m =
  untyped-type-spans tp ≫span
  untyped-term-spans t ≫span
  get-ctxt λ Γ → with-ctxt (ctxt-var-decl-loc pi' x Γ) $
  get-ctxt λ Γ → spanM-add (s Γ pi' x (Tkt $ TpHole pi') t) ≫span
                 spanM-add (Var-span Γ pi' x untyped [] nothing) ≫span m
untyped-defTermOrType-spans pi s (DefType pi' x k tp) m =
  untyped-kind-spans k ≫span
  untyped-type-spans tp ≫span
  get-ctxt λ Γ → with-ctxt (ctxt-var-decl-loc pi' x Γ) $
  get-ctxt λ Γ → spanM-add (s Γ pi' x (Tkk k) tp) ≫span
                 spanM-add (TpVar-span Γ pi' x untyped [] nothing) ≫span m

max_stars_repo_name: CarlOlson/cedille

max_issues_repo_name: CarlOlson/cedille

max_forks_repo_name: CarlOlson/cedille


text:
module Builtin where

open import Agda.Primitive

data Bool : Set where
  false : Bool
  true  : Bool

not : Bool -> Bool
not true = false
not false = true

_||_ : Bool -> Bool -> Bool
true  || _ = true
false || x = x

_&&_ : Bool -> Bool -> Bool
true  && x = x
false && _ = false

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

{-# BUILTIN NATURAL Nat  #-}

zero' : Nat
zero' = 0

one : Nat
one = 1

data Int : Set where
  pos : Nat → Int
  negsuc : Nat → Int

postulate
  String : Set
  Float  : Set
  Char   : Set

{-# BUILTIN INTEGER Int    #-}
{-# BUILTIN INTEGERPOS pos #-}
{-# BUILTIN INTEGERNEGSUC negsuc #-}
{-# BUILTIN STRING  String #-}
{-# BUILTIN FLOAT   Float  #-}
{-# BUILTIN CHAR    Char   #-}

data Maybe (A : Set) : Set where
  just : A → Maybe A
  nothing : Maybe A

{-# BUILTIN MAYBE Maybe #-}

record Sigma {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Sigma public

infixr 4 _,_

{-# BUILTIN SIGMA Sigma #-}

infixr 10 _::_
data List (A : Set) : Set where
  nil  : List A
  _::_ : A -> List A -> List A

{-# BUILTIN LIST List   #-}

postulate Word64 : Set
{-# BUILTIN WORD64 Word64 #-}

primitive

  -- Integer functions
  primShowInteger     : Int -> String

  -- Floating point function
  primFloatInequality        : Float → Float → Bool
  primFloatEquality          : Float → Float → Bool
  primFloatLess              : Float → Float → Bool
  primFloatIsInfinite        : Float → Bool
  primFloatIsNaN             : Float → Bool
  primFloatIsNegativeZero    : Float → Bool
  primFloatToWord64          : Float → Word64
  primNatToFloat             : Nat → Float
  primIntToFloat             : Int → Float
  primFloatRound             : Float → Maybe Int
  primFloatFloor             : Float → Maybe Int
  primFloatCeiling           : Float → Maybe Int
  primFloatToRatio           : Float → (Sigma Int λ _ → Int)
  primRatioToFloat           : Int → Int → Float
  primFloatDecode            : Float → Maybe (Sigma Int λ _ → Int)
  primFloatEncode            : Int → Int → Maybe Float
  primShowFloat              : Float → String
  primFloatPlus              : Float → Float → Float
  primFloatMinus             : Float → Float → Float
  primFloatTimes             : Float → Float → Float
  primFloatDiv               : Float → Float → Float
  primFloatNegate            : Float → Float
  primFloatSqrt              : Float → Float
  primFloatExp               : Float → Float
  primFloatLog               : Float → Float
  primFloatSin               : Float → Float
  primFloatCos               : Float → Float
  primFloatTan               : Float → Float
  primFloatASin              : Float → Float
  primFloatACos              : Float → Float
  primFloatATan              : Float → Float
  primFloatATan2             : Float → Float → Float
  primFloatSinh              : Float → Float
  primFloatCosh              : Float → Float
  primFloatTanh              : Float → Float
  primFloatASinh             : Float → Float
  primFloatACosh             : Float → Float
  primFloatATanh             : Float → Float
  primFloatPow               : Float → Float → Float

   -- Character functions
  primCharEquality   : Char -> Char -> Bool
  primIsLower        : Char -> Bool
  primIsDigit        : Char -> Bool
  primIsAlpha        : Char -> Bool
  primIsSpace        : Char -> Bool
  primIsAscii        : Char -> Bool
  primIsLatin1       : Char -> Bool
  primIsPrint        : Char -> Bool
  primIsHexDigit     : Char -> Bool
  primToUpper        : Char -> Char
  primToLower        : Char -> Char
  primCharToNat      : Char -> Nat
  primNatToChar      : Nat  -> Char -- partial
  primShowChar       : Char -> String

    -- String functions
  primStringToList   : String -> List Char
  primStringFromList : List Char -> String
  primStringAppend   : String -> String -> String
  primStringEquality : String -> String -> Bool
  primShowString     : String -> String

isLower : Char -> Bool
isLower = primIsLower

isAlpha : Char -> Bool
isAlpha = primIsAlpha

isUpper : Char -> Bool
isUpper c = isAlpha c && not (isLower c)

infixl 14 _/_

nat0 = primCharToNat '\0'
int0 = pos nat0

_/_  = primFloatDiv

pi : Float
pi = 3.141592653589793

sin : Float -> Float
sin = primFloatSin

cos : Float -> Float
cos = primFloatCos

tan : Float -> Float
tan = primFloatTan

reverse : {A : Set} -> List A -> List A
reverse xs = rev xs nil
  where
    rev : {A : Set} -> List A -> List A -> List A
    rev nil       ys = ys
    rev (x :: xs) ys = rev xs (x :: ys)

infixr 20 _∘_
_∘_ : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
f ∘ g = \x -> f (g x)

map : {A B : Set} -> (A -> B) -> List A -> List B
map f  nil      = nil
map f (x :: xs) = f x :: map f xs

stringAsList : (List Char -> List Char) -> String -> String
stringAsList f = primStringFromList ∘ f ∘ primStringToList

revStr : String -> String
revStr = stringAsList reverse

mapStr : (Char -> Char) -> String -> String
mapStr f = stringAsList (map f)

-- Testing unicode literals
uString = "åäö⊢ξ∀"
uChar   = '∀'

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

thm-show-pos : primShowInteger (pos 42) ≡ "42"
thm-show-pos = refl

thm-show-neg : primShowInteger (negsuc 41) ≡ "-42"
thm-show-neg = refl

thm-floor : primFloatFloor 4.2 ≡ just (pos 4)
thm-floor = refl

thm-ceiling : primFloatCeiling -5.1 ≡ just (negsuc 4)
thm-ceiling = refl

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
module PiFrac.Interp where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Data.Maybe
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_)
open import PiFrac.Syntax
open import PiFrac.Opsem

interp : {t₁ t₂ : 𝕌} → (t₁ ↔ t₂) → ⟦ t₁ ⟧ → Maybe ⟦ t₂ ⟧
interp unite₊l (inj₂ v) = just v
interp uniti₊l v = just (inj₂ v)
interp swap⋆ (v₁ , v₂) = just (v₂ , v₁)
interp swap₊ (inj₁ v) = just (inj₂ v)
interp swap₊ (inj₂ v) = just (inj₁ v)
interp assocl₊ (inj₁ v) = just (inj₁ (inj₁ v))
interp assocl₊ (inj₂ (inj₁ v)) = just (inj₁ (inj₂ v))
interp assocl₊ (inj₂ (inj₂ v)) = just (inj₂ v)
interp assocr₊ (inj₁ (inj₁ v)) = just (inj₁ v)
interp assocr₊ (inj₁ (inj₂ v)) = just (inj₂ (inj₁ v))
interp assocr₊ (inj₂ v) = just (inj₂ (inj₂ v))
interp unite⋆l v = just (proj₂ v)
interp uniti⋆l v = just (tt , v)
interp assocl⋆ (v₁ , v₂ , v₃) = just ((v₁ , v₂) , v₃)
interp assocr⋆ ((v₁ , v₂) , v₃) = just (v₁ , v₂ , v₃)
interp dist (inj₁ v₁ , v₃) = just (inj₁ (v₁ , v₃))
interp dist (inj₂ v₂ , v₃) = just (inj₂ (v₂ , v₃))
interp factor (inj₁ (v₁ , v₃)) = just (inj₁ v₁ , v₃)
interp factor (inj₂ (v₂ , v₃)) = just (inj₂ v₂ , v₃)
interp id↔ v = just v
interp (c₁ ⊕ c₂) (inj₁ v) = interp c₁ v >>= just ∘ inj₁
interp (c₁ ⊕ c₂) (inj₂ v) = interp c₂ v >>= just ∘ inj₂
interp (c₁ ⊗ c₂) (v₁ , v₂) = interp c₁ v₁ >>=
                               (λ v₁' → interp c₂ v₂ >>=
                                  λ v₂' → just (v₁' , v₂'))
interp (c₁ ⨾ c₂) v = interp c₁ v >>= interp c₂
interp (ηₓ v) tt = just (v , ↻)
interp (εₓ v) (v' , ○) with v ≟ v'
... | yes _ = just tt
... | no _ = nothing


text:
------------------------------------------------------------------------------
-- Elimination properties for the inequalities
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.Inequalities.EliminationPropertiesATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities

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

0<0→⊥ : ¬ (zero < zero)
0<0→⊥ h = prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}

x<0→⊥ : ∀ {n} → N n → ¬ (n < zero)
x<0→⊥ nzero h = prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}
x<0→⊥ (nsucc Nn) h = prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}

x<x→⊥ : ∀ {n} → N n → ¬ (n < n)
x<x→⊥ nzero h = prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}
x<x→⊥ (nsucc {n} Nn) h = prf (x<x→⊥ Nn)
  where postulate prf : ¬ (n < n) → ⊥
        {-# ATP prove prf #-}

0>x→⊥ : ∀ {n} → N n → ¬ (zero > n)
0>x→⊥ nzero h = prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}
0>x→⊥ (nsucc Nn) h = prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}

S≤0→⊥ : ∀ {n} → N n → ¬ (succ₁ n ≤ zero)
S≤0→⊥ nzero h = prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}
S≤0→⊥ (nsucc {n} Nn) h = prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}

0≥S→⊥ : ∀ {n} → N n → ¬ (zero ≥ succ₁ n)
0≥S→⊥ Nn h = prf
  where postulate prf : ⊥
        {-# ATP prove prf S≤0→⊥ #-}

postulate S≯0→⊥ : ∀ {n} → ¬ (succ₁ n ≯ zero)
{-# ATP prove S≯0→⊥ #-}

x<y→y<x→⊥ : ∀ {m n} → N m → N n → m < n → ¬ (n < m)
x<y→y<x→⊥ nzero Nn h₁ h₂ = prf
  where postulate prf : ⊥
        {-# ATP prove prf 0>x→⊥ #-}
x<y→y<x→⊥ (nsucc Nm) nzero h₁ h₂ = prf
  where postulate prf : ⊥
        {-# ATP prove prf 0>x→⊥ #-}
x<y→y<x→⊥ (nsucc {m} Nm) (nsucc {n} Nn) h₁ h₂ = prf (x<y→y<x→⊥ Nm Nn m<n)
  where
  postulate m<n : m < n
  {-# ATP prove m<n #-}

  postulate prf : ¬ (n < m) → ⊥
  {-# ATP prove prf #-}

x>y→x≤y→⊥ : ∀ {m n} → N m → N n → m > n → ¬ (m ≤ n)
x>y→x≤y→⊥ nzero Nn h₁ h₂ = prf
  where postulate prf : ⊥
        {-# ATP prove prf x<0→⊥ #-}
x>y→x≤y→⊥ (nsucc Nm) nzero h₁ h₂ = prf
  where postulate prf : ⊥
        {-# ATP prove prf x<0→⊥ #-}
x>y→x≤y→⊥ (nsucc {m} Nm) (nsucc {n} Nn) h₁ h₂ = prf (x>y→x≤y→⊥ Nm Nn m>n)
  where
  postulate m>n : m > n
  {-# ATP prove m>n #-}

  postulate prf : ¬ (m ≤ n) → ⊥
  {-# ATP prove prf #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import HoTT
open import cohomology.Theory

module cohomology.Sphere {i} (OT : OrdinaryTheory i) where

open OrdinaryTheory OT

abstract
  C-Sphere-≠-is-trivial : (n : ℤ) (m : ℕ) → (n ≠ ℕ-to-ℤ m)
    → is-trivialᴳ (C n (⊙Lift (⊙Sphere m)))
  C-Sphere-≠-is-trivial n O n≠0 = C-dimension n≠0
  C-Sphere-≠-is-trivial n (S m) n≠Sm = iso-preserves'-trivial
    (C n (⊙Lift (⊙Sphere (S m)))
      ≃ᴳ⟨ C-emap n $ ⊙Susp-Lift-econv (⊙Sphere m) ⟩
    C n (⊙Susp (⊙Lift (⊙Sphere m)))
      ≃ᴳ⟨ transportᴳ-iso (λ n → C n (⊙Susp (⊙Lift (⊙Sphere m)))) (succ-pred n) ⁻¹ᴳ ⟩
    C (succ (pred n)) (⊙Susp (⊙Lift (⊙Sphere m)))
      ≃ᴳ⟨ C-Susp (pred n) (⊙Lift (⊙Sphere m)) ⟩
    C (pred n) (⊙Lift (⊙Sphere m))
      ≃ᴳ∎)
    (C-Sphere-≠-is-trivial (pred n) m (pred-≠ n≠Sm))

C-Sphere-diag : (m : ℕ) → C (ℕ-to-ℤ m) (⊙Lift (⊙Sphere m)) ≃ᴳ C2 0
C-Sphere-diag O = idiso _
C-Sphere-diag (S m) =
  C (ℕ-to-ℤ (S m)) (⊙Lift (⊙Sphere (S m)))
    ≃ᴳ⟨ C-emap (ℕ-to-ℤ (S m)) (⊙Susp-Lift-econv (⊙Sphere m)) ⟩
  C (ℕ-to-ℤ (S m)) (⊙Susp (⊙Lift (⊙Sphere m)))
    ≃ᴳ⟨ C-Susp (ℕ-to-ℤ m) (⊙Lift (⊙Sphere m)) ⟩
  C (ℕ-to-ℤ m) (⊙Lift (⊙Sphere m))
    ≃ᴳ⟨ C-Sphere-diag m ⟩
  C 0 (⊙Lift ⊙S⁰)
    ≃ᴳ∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import HoTT
open import cohomology.Exactness
open import cohomology.Theory

{- Cohomology functor sends constant functions to constant functions -}

module cohomology.ConstantFunction {i} (CT : CohomologyTheory i) where

open import cohomology.Unit CT
open CohomologyTheory CT

module _ (n : ℤ) {X Y : Ptd i} where

  CF-cst : CF-hom n (⊙cst {X = X} {Y = Y}) == cst-hom
  CF-cst =
    CF-hom n (⊙cst {X = PLU} ⊙∘ ⊙cst {X = X})
      =⟨ CF-comp n ⊙cst ⊙cst ⟩
    (CF-hom n (⊙cst {X = X})) ∘ᴳ (CF-hom n (⊙cst {X = PLU}))
      =⟨ hom= (CF-hom n (⊙cst {X = PLU})) cst-hom
              (λ= (λ _ → prop-has-all-paths (C-Unit-is-prop n) _ _))
         |in-ctx (λ w → CF-hom n (⊙cst {X = X} {Y = PLU}) ∘ᴳ w) ⟩
    (CF-hom n (⊙cst {X = X} {Y = PLU})) ∘ᴳ cst-hom
      =⟨ pre∘-cst-hom (CF-hom n (⊙cst {X = X} {Y = PLU})) ⟩
    cst-hom ∎
    where
    PLU = ⊙Lift {j = i} ⊙Unit

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
-- Andreas, 2018-10-29, issue #3331

-- Document that using and renaming lists cannot overlap.

open import Agda.Builtin.Bool using (true) renaming (true to tt)

-- Expected error:
-- Repeated name in import directive: true

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Many properties which hold for _∼_ also hold for _∼_ on f
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.On where

open import Function
open import Data.Product

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

  implies : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) →
            ≈ ⇒ ∼ → (≈ on f) ⇒ (∼ on f)
  implies _ _ impl = impl

  reflexive : ∀ {ℓ} (∼ : Rel A ℓ) → Reflexive ∼ → Reflexive (∼ on f)
  reflexive _ refl = refl

  irreflexive : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (∼ : Rel A ℓ₂) →
                Irreflexive ≈ ∼ → Irreflexive (≈ on f) (∼ on f)
  irreflexive _ _ irrefl = irrefl

  symmetric : ∀ {ℓ} (∼ : Rel A ℓ) → Symmetric ∼ → Symmetric (∼ on f)
  symmetric _ sym = sym

  transitive : ∀ {ℓ} (∼ : Rel A ℓ) → Transitive ∼ → Transitive (∼ on f)
  transitive _ trans = trans

  antisymmetric : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (≤ : Rel A ℓ₂) →
                  Antisymmetric ≈ ≤ → Antisymmetric (≈ on f) (≤ on f)
  antisymmetric _ _ antisym = antisym

  asymmetric : ∀ {ℓ} (< : Rel A ℓ) → Asymmetric < → Asymmetric (< on f)
  asymmetric _ asym = asym

  respects : ∀ {ℓ p} (∼ : Rel A ℓ) (P : A → Set p) →
             P Respects ∼ → (P ∘ f) Respects (∼ on f)
  respects _ _ resp = resp

  respects₂ : ∀ {ℓ₁ ℓ₂} (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) →
              ∼₁ Respects₂ ∼₂ → (∼₁ on f) Respects₂ (∼₂ on f)
  respects₂ _ _ (resp₁ , resp₂) =
    ((λ {_} {_} {_} → resp₁) , λ {_} {_} {_} → resp₂)

  decidable : ∀ {ℓ} (∼ : Rel A ℓ) → Decidable ∼ → Decidable (∼ on f)
  decidable _ dec = λ x y → dec (f x) (f y)

  total : ∀ {ℓ} (∼ : Rel A ℓ) → Total ∼ → Total (∼ on f)
  total _ tot = λ x y → tot (f x) (f y)

  trichotomous : ∀ {ℓ₁ ℓ₂} (≈ : Rel A ℓ₁) (< : Rel A ℓ₂) →
                 Trichotomous ≈ < → Trichotomous (≈ on f) (< on f)
  trichotomous _ _ compare = λ x y → compare (f x) (f y)

  isEquivalence : ∀ {ℓ} {≈ : Rel A ℓ} →
                  IsEquivalence ≈ → IsEquivalence (≈ on f)
  isEquivalence {≈ = ≈} eq = record
    { refl  = reflexive  ≈ Eq.refl
    ; sym   = symmetric  ≈ Eq.sym
    ; trans = transitive ≈ Eq.trans
    }
    where module Eq = IsEquivalence eq

  isPreorder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} →
               IsPreorder ≈ ∼ → IsPreorder (≈ on f) (∼ on f)
  isPreorder {≈ = ≈} {∼} pre = record
    { isEquivalence = isEquivalence Pre.isEquivalence
    ; reflexive     = implies ≈ ∼ Pre.reflexive
    ; trans         = transitive ∼ Pre.trans
    }
    where module Pre = IsPreorder pre

  isDecEquivalence : ∀ {ℓ} {≈ : Rel A ℓ} →
                     IsDecEquivalence ≈ → IsDecEquivalence (≈ on f)
  isDecEquivalence {≈ = ≈} dec = record
    { isEquivalence = isEquivalence Dec.isEquivalence
    ; _≟_           = decidable ≈ Dec._≟_
    }
    where module Dec = IsDecEquivalence dec

  isPartialOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
                   IsPartialOrder ≈ ≤ →
                   IsPartialOrder (≈ on f) (≤ on f)
  isPartialOrder {≈ = ≈} {≤} po = record
    { isPreorder = isPreorder Po.isPreorder
    ; antisym    = antisymmetric ≈ ≤ Po.antisym
    }
    where module Po = IsPartialOrder po

  isDecPartialOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
                      IsDecPartialOrder ≈ ≤ →
                      IsDecPartialOrder (≈ on f) (≤ on f)
  isDecPartialOrder dpo = record
    { isPartialOrder = isPartialOrder DPO.isPartialOrder
    ; _≟_            = decidable _ DPO._≟_
    ; _≤?_           = decidable _ DPO._≤?_
    }
    where module DPO = IsDecPartialOrder dpo

  isStrictPartialOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
                         IsStrictPartialOrder ≈ < →
                         IsStrictPartialOrder (≈ on f) (< on f)
  isStrictPartialOrder {≈ = ≈} {<} spo = record
    { isEquivalence = isEquivalence Spo.isEquivalence
    ; irrefl        = irreflexive ≈ < Spo.irrefl
    ; trans         = transitive < Spo.trans
    ; <-resp-≈      = respects₂ < ≈ Spo.<-resp-≈
    }
    where module Spo = IsStrictPartialOrder spo

  isTotalOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
                 IsTotalOrder ≈ ≤ →
                 IsTotalOrder (≈ on f) (≤ on f)
  isTotalOrder {≈ = ≈} {≤} to = record
    { isPartialOrder = isPartialOrder To.isPartialOrder
    ; total          = total ≤ To.total
    }
    where module To = IsTotalOrder to

  isDecTotalOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
                    IsDecTotalOrder ≈ ≤ →
                    IsDecTotalOrder (≈ on f) (≤ on f)
  isDecTotalOrder {≈ = ≈} {≤} dec = record
    { isTotalOrder = isTotalOrder Dec.isTotalOrder
    ; _≟_          = decidable ≈ Dec._≟_
    ; _≤?_         = decidable ≤ Dec._≤?_
    }
    where module Dec = IsDecTotalOrder dec

  isStrictTotalOrder : ∀ {ℓ₁ ℓ₂} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
                       IsStrictTotalOrder ≈ < →
                       IsStrictTotalOrder (≈ on f) (< on f)
  isStrictTotalOrder {≈ = ≈} {<} sto = record
    { isEquivalence = isEquivalence Sto.isEquivalence
    ; trans         = transitive < Sto.trans
    ; compare       = trichotomous ≈ < Sto.compare
    ; <-resp-≈      = respects₂ < ≈ Sto.<-resp-≈
    }
    where module Sto = IsStrictTotalOrder sto

preorder : ∀ {p₁ p₂ p₃ b} {B : Set b} (P : Preorder p₁ p₂ p₃) →
           (B → Preorder.Carrier P) → Preorder _ _ _
preorder P f = record
  { isPreorder = isPreorder f (Preorder.isPreorder P)
  }

setoid : ∀ {s₁ s₂ b} {B : Set b} (S : Setoid s₁ s₂) →
         (B → Setoid.Carrier S) → Setoid _ _
setoid S f = record
  { isEquivalence = isEquivalence f (Setoid.isEquivalence S)
  }

decSetoid : ∀ {d₁ d₂ b} {B : Set b} (D : DecSetoid d₁ d₂) →
            (B → DecSetoid.Carrier D) → DecSetoid _ _
decSetoid D f = record
  { isDecEquivalence = isDecEquivalence f (DecSetoid.isDecEquivalence D)
  }

poset : ∀ {p₁ p₂ p₃ b} {B : Set b} (P : Poset p₁ p₂ p₃) →
        (B → Poset.Carrier P) → Poset _ _ _
poset P f = record
  { isPartialOrder = isPartialOrder f (Poset.isPartialOrder P)
  }

decPoset : ∀ {d₁ d₂ d₃ b} {B : Set b} (D : DecPoset d₁ d₂ d₃) →
           (B → DecPoset.Carrier D) → DecPoset _ _ _
decPoset D f = record
  { isDecPartialOrder =
      isDecPartialOrder f (DecPoset.isDecPartialOrder D)
  }

strictPartialOrder :
  ∀ {s₁ s₂ s₃ b} {B : Set b} (S : StrictPartialOrder s₁ s₂ s₃) →
  (B → StrictPartialOrder.Carrier S) → StrictPartialOrder _ _ _
strictPartialOrder S f = record
  { isStrictPartialOrder =
      isStrictPartialOrder f (StrictPartialOrder.isStrictPartialOrder S)
  }

totalOrder : ∀ {t₁ t₂ t₃ b} {B : Set b} (T : TotalOrder t₁ t₂ t₃) →
             (B → TotalOrder.Carrier T) → TotalOrder _ _ _
totalOrder T f = record
  { isTotalOrder = isTotalOrder f (TotalOrder.isTotalOrder T)
  }

decTotalOrder :
  ∀ {d₁ d₂ d₃ b} {B : Set b} (D : DecTotalOrder d₁ d₂ d₃) →
  (B → DecTotalOrder.Carrier D) → DecTotalOrder _ _ _
decTotalOrder D f = record
  { isDecTotalOrder = isDecTotalOrder f (DecTotalOrder.isDecTotalOrder D)
  }

strictTotalOrder :
  ∀ {s₁ s₂ s₃ b} {B : Set b} (S : StrictTotalOrder s₁ s₂ s₃) →
  (B → StrictTotalOrder.Carrier S) → StrictTotalOrder _ _ _
strictTotalOrder S f = record
  { isStrictTotalOrder =
      isStrictTotalOrder f (StrictTotalOrder.isStrictTotalOrder S)
  }


text:
module options where

open import lib

open import options-types public
----------------------------------------------------------------------------------
-- Run-rewriting rules
----------------------------------------------------------------------------------

data gratr2-nt : Set where
  _ws-plus-34 : gratr2-nt
  _ws : gratr2-nt
  _str-bool : gratr2-nt
  _start : gratr2-nt
  _squote : gratr2-nt
  _posinfo : gratr2-nt
  _paths : gratr2-nt
  _path-star-1 : gratr2-nt
  _path : gratr2-nt
  _ows-star-35 : gratr2-nt
  _ows : gratr2-nt
  _opts : gratr2-nt
  _opt : gratr2-nt
  _numpunct-bar-8 : gratr2-nt
  _numpunct-bar-7 : gratr2-nt
  _numpunct : gratr2-nt
  _numone-range-5 : gratr2-nt
  _numone : gratr2-nt
  _num-plus-6 : gratr2-nt
  _num : gratr2-nt
  _comment-star-30 : gratr2-nt
  _comment : gratr2-nt
  _aws-bar-33 : gratr2-nt
  _aws-bar-32 : gratr2-nt
  _aws-bar-31 : gratr2-nt
  _aws : gratr2-nt
  _anychar-bar-9 : gratr2-nt
  _anychar-bar-29 : gratr2-nt
  _anychar-bar-28 : gratr2-nt
  _anychar-bar-27 : gratr2-nt
  _anychar-bar-26 : gratr2-nt
  _anychar-bar-25 : gratr2-nt
  _anychar-bar-24 : gratr2-nt
  _anychar-bar-23 : gratr2-nt
  _anychar-bar-22 : gratr2-nt
  _anychar-bar-21 : gratr2-nt
  _anychar-bar-20 : gratr2-nt
  _anychar-bar-19 : gratr2-nt
  _anychar-bar-18 : gratr2-nt
  _anychar-bar-17 : gratr2-nt
  _anychar-bar-16 : gratr2-nt
  _anychar-bar-15 : gratr2-nt
  _anychar-bar-14 : gratr2-nt
  _anychar-bar-13 : gratr2-nt
  _anychar-bar-12 : gratr2-nt
  _anychar-bar-11 : gratr2-nt
  _anychar-bar-10 : gratr2-nt
  _anychar : gratr2-nt
  _alpha-range-3 : gratr2-nt
  _alpha-range-2 : gratr2-nt
  _alpha-bar-4 : gratr2-nt
  _alpha : gratr2-nt

gratr2-nt-eq : gratr2-nt → gratr2-nt → 𝔹
gratr2-nt-eq  _ws-plus-34 _ws-plus-34 = tt
gratr2-nt-eq  _ws _ws = tt
gratr2-nt-eq  _str-bool _str-bool = tt
gratr2-nt-eq  _start _start = tt
gratr2-nt-eq  _squote _squote = tt
gratr2-nt-eq  _posinfo _posinfo = tt
gratr2-nt-eq  _paths _paths = tt
gratr2-nt-eq  _path-star-1 _path-star-1 = tt
gratr2-nt-eq  _path _path = tt
gratr2-nt-eq  _ows-star-35 _ows-star-35 = tt
gratr2-nt-eq  _ows _ows = tt
gratr2-nt-eq  _opts _opts = tt
gratr2-nt-eq  _opt _opt = tt
gratr2-nt-eq  _numpunct-bar-8 _numpunct-bar-8 = tt
gratr2-nt-eq  _numpunct-bar-7 _numpunct-bar-7 = tt
gratr2-nt-eq  _numpunct _numpunct = tt
gratr2-nt-eq  _numone-range-5 _numone-range-5 = tt
gratr2-nt-eq  _numone _numone = tt
gratr2-nt-eq  _num-plus-6 _num-plus-6 = tt
gratr2-nt-eq  _num _num = tt
gratr2-nt-eq  _comment-star-30 _comment-star-30 = tt
gratr2-nt-eq  _comment _comment = tt
gratr2-nt-eq  _aws-bar-33 _aws-bar-33 = tt
gratr2-nt-eq  _aws-bar-32 _aws-bar-32 = tt
gratr2-nt-eq  _aws-bar-31 _aws-bar-31 = tt
gratr2-nt-eq  _aws _aws = tt
gratr2-nt-eq  _anychar-bar-9 _anychar-bar-9 = tt
gratr2-nt-eq  _anychar-bar-29 _anychar-bar-29 = tt
gratr2-nt-eq  _anychar-bar-28 _anychar-bar-28 = tt
gratr2-nt-eq  _anychar-bar-27 _anychar-bar-27 = tt
gratr2-nt-eq  _anychar-bar-26 _anychar-bar-26 = tt
gratr2-nt-eq  _anychar-bar-25 _anychar-bar-25 = tt
gratr2-nt-eq  _anychar-bar-24 _anychar-bar-24 = tt
gratr2-nt-eq  _anychar-bar-23 _anychar-bar-23 = tt
gratr2-nt-eq  _anychar-bar-22 _anychar-bar-22 = tt
gratr2-nt-eq  _anychar-bar-21 _anychar-bar-21 = tt
gratr2-nt-eq  _anychar-bar-20 _anychar-bar-20 = tt
gratr2-nt-eq  _anychar-bar-19 _anychar-bar-19 = tt
gratr2-nt-eq  _anychar-bar-18 _anychar-bar-18 = tt
gratr2-nt-eq  _anychar-bar-17 _anychar-bar-17 = tt
gratr2-nt-eq  _anychar-bar-16 _anychar-bar-16 = tt
gratr2-nt-eq  _anychar-bar-15 _anychar-bar-15 = tt
gratr2-nt-eq  _anychar-bar-14 _anychar-bar-14 = tt
gratr2-nt-eq  _anychar-bar-13 _anychar-bar-13 = tt
gratr2-nt-eq  _anychar-bar-12 _anychar-bar-12 = tt
gratr2-nt-eq  _anychar-bar-11 _anychar-bar-11 = tt
gratr2-nt-eq  _anychar-bar-10 _anychar-bar-10 = tt
gratr2-nt-eq  _anychar _anychar = tt
gratr2-nt-eq  _alpha-range-3 _alpha-range-3 = tt
gratr2-nt-eq  _alpha-range-2 _alpha-range-2 = tt
gratr2-nt-eq  _alpha-bar-4 _alpha-bar-4 = tt
gratr2-nt-eq  _alpha _alpha = tt
gratr2-nt-eq _ _ = ff

open import rtn gratr2-nt

options-start : gratr2-nt → 𝕃 gratr2-rule
options-start _ws-plus-34 = (just "P132" , nothing , just _ws-plus-34 , inj₁ _aws :: inj₁ _ws-plus-34 :: []) :: (just "P131" , nothing , just _ws-plus-34 , inj₁ _aws :: []) :: []
options-start _ws = (just "P133" , nothing , just _ws , inj₁ _ws-plus-34 :: []) :: []
options-start _str-bool = (just "StrBoolTrue" , nothing , just _str-bool , inj₂ 't' :: inj₂ 'r' :: inj₂ 'u' :: inj₂ 'e' :: []) :: (just "StrBoolFalse" , nothing , just _str-bool , inj₂ 'f' :: inj₂ 'a' :: inj₂ 'l' :: inj₂ 's' :: inj₂ 'e' :: []) :: []
options-start _start = (just "File" , nothing , just _start , inj₁ _opts :: inj₁ _ows :: []) :: []
options-start _squote = (just "P0" , nothing , just _squote , inj₂ '\"' :: []) :: []
options-start _posinfo = (just "Posinfo" , nothing , just _posinfo , []) :: []
options-start _paths = (just "PathsNil" , nothing , just _paths , []) :: (just "PathsCons" , nothing , just _paths , inj₁ _ws :: inj₁ _path :: inj₁ _paths :: []) :: []
options-start _path-star-1 = (just "P2" , nothing , just _path-star-1 , inj₁ _anychar :: inj₁ _path-star-1 :: []) :: (just "P1" , nothing , just _path-star-1 , []) :: []
options-start _path = (just "P3" , nothing , just _path , inj₁ _squote :: inj₁ _path-star-1 :: inj₁ _squote :: []) :: []
options-start _ows-star-35 = (just "P135" , nothing , just _ows-star-35 , inj₁ _aws :: inj₁ _ows-star-35 :: []) :: (just "P134" , nothing , just _ows-star-35 , []) :: []
options-start _ows = (just "P136" , nothing , just _ows , inj₁ _ows-star-35 :: []) :: []
options-start _opts = (just "OptsNil" , nothing , just _opts , []) :: (just "OptsCons" , nothing , just _opts , inj₁ _ows :: inj₁ _opt :: inj₁ _opts :: []) :: []
options-start _opt = (just "UseCedeFiles" , nothing , just _opt , inj₂ 'u' :: inj₂ 's' :: inj₂ 'e' :: inj₂ '-' :: inj₂ 'c' :: inj₂ 'e' :: inj₂ 'd' :: inj₂ 'e' :: inj₂ '-' :: inj₂ 'f' :: inj₂ 'i' :: inj₂ 'l' :: inj₂ 'e' :: inj₂ 's' :: inj₁ _ows :: inj₂ '=' :: inj₁ _ows :: inj₁ _str-bool :: inj₁ _ows :: inj₂ '.' :: inj₁ _ows :: []) :: (just "ShowQualifiedVars" , nothing , just _opt , inj₂ 's' :: inj₂ 'h' :: inj₂ 'o' :: inj₂ 'w' :: inj₂ '-' :: inj₂ 'q' :: inj₂ 'u' :: inj₂ 'a' :: inj₂ 'l' :: inj₂ 'i' :: inj₂ 'f' :: inj₂ 'i' :: inj₂ 'e' :: inj₂ 'd' :: inj₂ '-' :: inj₂ 'v' :: inj₂ 'a' :: inj₂ 'r' :: inj₂ 's' :: inj₁ _ows :: inj₂ '=' :: inj₁ _ows :: inj₁ _str-bool :: inj₁ _ows :: inj₂ '.' :: inj₁ _ows :: []) :: (just "MakeRktFiles" , nothing , just _opt , inj₂ 'm' :: inj₂ 'a' :: inj₂ 'k' :: inj₂ 'e' :: inj₂ '-' :: inj₂ 'r' :: inj₂ 'k' :: inj₂ 't' :: inj₂ '-' :: inj₂ 'f' :: inj₂ 'i' :: inj₂ 'l' :: inj₂ 'e' :: inj₂ 's' :: inj₁ _ows :: inj₂ '=' :: inj₁ _ows :: inj₁ _str-bool :: inj₁ _ows :: inj₂ '.' :: inj₁ _ows :: []) :: (just "Lib" , nothing , just _opt , inj₂ 'i' :: inj₂ 'm' :: inj₂ 'p' :: inj₂ 'o' :: inj₂ 'r' :: inj₂ 't' :: inj₂ '-' :: inj₂ 'd' :: inj₂ 'i' :: inj₂ 'r' :: inj₂ 'e' :: inj₂ 'c' :: inj₂ 't' :: inj₂ 'o' :: inj₂ 'r' :: inj₂ 'i' :: inj₂ 'e' :: inj₂ 's' :: inj₁ _ows :: inj₂ '=' :: inj₁ _ows :: inj₁ _paths :: inj₁ _ows :: inj₂ '.' :: []) :: (just "GenerateLogs" , nothing , just _opt , inj₂ 'g' :: inj₂ 'e' :: inj₂ 'n' :: inj₂ 'e' :: inj₂ 'r' :: inj₂ 'a' :: inj₂ 't' :: inj₂ 'e' :: inj₂ '-' :: inj₂ 'l' :: inj₂ 'o' :: inj₂ 'g' :: inj₂ 's' :: inj₁ _ows :: inj₂ '=' :: inj₁ _ows :: inj₁ _str-bool :: inj₁ _ows :: inj₂ '.' :: inj₁ _ows :: []) :: []
options-start _numpunct-bar-8 = (just "P76" , nothing , just _numpunct-bar-8 , inj₁ _numpunct-bar-7 :: []) :: (just "P75" , nothing , just _numpunct-bar-8 , inj₁ _numone :: []) :: []
options-start _numpunct-bar-7 = (just "P74" , nothing , just _numpunct-bar-7 , inj₂ '-' :: []) :: (just "P73" , nothing , just _numpunct-bar-7 , inj₂ '\'' :: []) :: []
options-start _numpunct = (just "P77" , nothing , just _numpunct , inj₁ _numpunct-bar-8 :: []) :: []
options-start _numone-range-5 = (just "P68" , nothing , just _numone-range-5 , inj₂ '9' :: []) :: (just "P67" , nothing , just _numone-range-5 , inj₂ '8' :: []) :: (just "P66" , nothing , just _numone-range-5 , inj₂ '7' :: []) :: (just "P65" , nothing , just _numone-range-5 , inj₂ '6' :: []) :: (just "P64" , nothing , just _numone-range-5 , inj₂ '5' :: []) :: (just "P63" , nothing , just _numone-range-5 , inj₂ '4' :: []) :: (just "P62" , nothing , just _numone-range-5 , inj₂ '3' :: []) :: (just "P61" , nothing , just _numone-range-5 , inj₂ '2' :: []) :: (just "P60" , nothing , just _numone-range-5 , inj₂ '1' :: []) :: (just "P59" , nothing , just _numone-range-5 , inj₂ '0' :: []) :: []
options-start _numone = (just "P69" , nothing , just _numone , inj₁ _numone-range-5 :: []) :: []
options-start _num-plus-6 = (just "P71" , nothing , just _num-plus-6 , inj₁ _numone :: inj₁ _num-plus-6 :: []) :: (just "P70" , nothing , just _num-plus-6 , inj₁ _numone :: []) :: []
options-start _num = (just "P72" , nothing , just _num , inj₁ _num-plus-6 :: []) :: []
options-start _comment-star-30 = (just "P122" , nothing , just _comment-star-30 , inj₁ _anychar :: inj₁ _comment-star-30 :: []) :: (just "P121" , nothing , just _comment-star-30 , []) :: []
options-start _comment = (just "P123" , nothing , just _comment , inj₂ '%' :: inj₁ _comment-star-30 :: inj₂ '\n' :: []) :: []
options-start _aws-bar-33 = (just "P129" , nothing , just _aws-bar-33 , inj₁ _aws-bar-32 :: []) :: (just "P128" , nothing , just _aws-bar-33 , inj₂ '\n' :: []) :: []
options-start _aws-bar-32 = (just "P127" , nothing , just _aws-bar-32 , inj₁ _aws-bar-31 :: []) :: (just "P126" , nothing , just _aws-bar-32 , inj₂ '\t' :: []) :: []
options-start _aws-bar-31 = (just "P125" , nothing , just _aws-bar-31 , inj₁ _comment :: []) :: (just "P124" , nothing , just _aws-bar-31 , inj₂ ' ' :: []) :: []
options-start _aws = (just "P130" , nothing , just _aws , inj₁ _aws-bar-33 :: []) :: []
options-start _anychar-bar-9 = (just "P79" , nothing , just _anychar-bar-9 , inj₂ '_' :: []) :: (just "P78" , nothing , just _anychar-bar-9 , inj₂ '/' :: []) :: []
options-start _anychar-bar-29 = (just "P119" , nothing , just _anychar-bar-29 , inj₁ _anychar-bar-28 :: []) :: (just "P118" , nothing , just _anychar-bar-29 , inj₁ _alpha :: []) :: []
options-start _anychar-bar-28 = (just "P117" , nothing , just _anychar-bar-28 , inj₁ _anychar-bar-27 :: []) :: (just "P116" , nothing , just _anychar-bar-28 , inj₁ _numpunct :: []) :: []
options-start _anychar-bar-27 = (just "P115" , nothing , just _anychar-bar-27 , inj₁ _anychar-bar-26 :: []) :: (just "P114" , nothing , just _anychar-bar-27 , inj₂ '\t' :: []) :: []
options-start _anychar-bar-26 = (just "P113" , nothing , just _anychar-bar-26 , inj₁ _anychar-bar-25 :: []) :: (just "P112" , nothing , just _anychar-bar-26 , inj₂ ' ' :: []) :: []
options-start _anychar-bar-25 = (just "P111" , nothing , just _anychar-bar-25 , inj₁ _anychar-bar-24 :: []) :: (just "P110" , nothing , just _anychar-bar-25 , inj₂ '%' :: []) :: []
options-start _anychar-bar-24 = (just "P109" , nothing , just _anychar-bar-24 , inj₁ _anychar-bar-23 :: []) :: (just "P108" , nothing , just _anychar-bar-24 , inj₂ '(' :: []) :: []
options-start _anychar-bar-23 = (just "P107" , nothing , just _anychar-bar-23 , inj₁ _anychar-bar-22 :: []) :: (just "P106" , nothing , just _anychar-bar-23 , inj₂ ')' :: []) :: []
options-start _anychar-bar-22 = (just "P105" , nothing , just _anychar-bar-22 , inj₁ _anychar-bar-21 :: []) :: (just "P104" , nothing , just _anychar-bar-22 , inj₂ ':' :: []) :: []
options-start _anychar-bar-21 = (just "P103" , nothing , just _anychar-bar-21 , inj₁ _anychar-bar-20 :: []) :: (just "P102" , nothing , just _anychar-bar-21 , inj₂ '.' :: []) :: []
options-start _anychar-bar-20 = (just "P101" , nothing , just _anychar-bar-20 , inj₁ _anychar-bar-19 :: []) :: (just "P100" , nothing , just _anychar-bar-20 , inj₂ '[' :: []) :: []
options-start _anychar-bar-19 = (just "P99" , nothing , just _anychar-bar-19 , inj₁ _anychar-bar-18 :: []) :: (just "P98" , nothing , just _anychar-bar-19 , inj₂ ']' :: []) :: []
options-start _anychar-bar-18 = (just "P97" , nothing , just _anychar-bar-18 , inj₁ _anychar-bar-17 :: []) :: (just "P96" , nothing , just _anychar-bar-18 , inj₂ ',' :: []) :: []
options-start _anychar-bar-17 = (just "P95" , nothing , just _anychar-bar-17 , inj₁ _anychar-bar-16 :: []) :: (just "P94" , nothing , just _anychar-bar-17 , inj₂ '!' :: []) :: []
options-start _anychar-bar-16 = (just "P93" , nothing , just _anychar-bar-16 , inj₁ _anychar-bar-15 :: []) :: (just "P92" , nothing , just _anychar-bar-16 , inj₂ '{' :: []) :: []
options-start _anychar-bar-15 = (just "P91" , nothing , just _anychar-bar-15 , inj₁ _anychar-bar-14 :: []) :: (just "P90" , nothing , just _anychar-bar-15 , inj₂ '}' :: []) :: []
options-start _anychar-bar-14 = (just "P89" , nothing , just _anychar-bar-14 , inj₁ _anychar-bar-13 :: []) :: (just "P88" , nothing , just _anychar-bar-14 , inj₂ '-' :: []) :: []
options-start _anychar-bar-13 = (just "P87" , nothing , just _anychar-bar-13 , inj₁ _anychar-bar-12 :: []) :: (just "P86" , nothing , just _anychar-bar-13 , inj₂ '=' :: []) :: []
options-start _anychar-bar-12 = (just "P85" , nothing , just _anychar-bar-12 , inj₁ _anychar-bar-11 :: []) :: (just "P84" , nothing , just _anychar-bar-12 , inj₂ '+' :: []) :: []
options-start _anychar-bar-11 = (just "P83" , nothing , just _anychar-bar-11 , inj₁ _anychar-bar-10 :: []) :: (just "P82" , nothing , just _anychar-bar-11 , inj₂ '<' :: []) :: []
options-start _anychar-bar-10 = (just "P81" , nothing , just _anychar-bar-10 , inj₁ _anychar-bar-9 :: []) :: (just "P80" , nothing , just _anychar-bar-10 , inj₂ '>' :: []) :: []
options-start _anychar = (just "P120" , nothing , just _anychar , inj₁ _anychar-bar-29 :: []) :: []
options-start _alpha-range-3 = (just "P55" , nothing , just _alpha-range-3 , inj₂ 'Z' :: []) :: (just "P54" , nothing , just _alpha-range-3 , inj₂ 'Y' :: []) :: (just "P53" , nothing , just _alpha-range-3 , inj₂ 'X' :: []) :: (just "P52" , nothing , just _alpha-range-3 , inj₂ 'W' :: []) :: (just "P51" , nothing , just _alpha-range-3 , inj₂ 'V' :: []) :: (just "P50" , nothing , just _alpha-range-3 , inj₂ 'U' :: []) :: (just "P49" , nothing , just _alpha-range-3 , inj₂ 'T' :: []) :: (just "P48" , nothing , just _alpha-range-3 , inj₂ 'S' :: []) :: (just "P47" , nothing , just _alpha-range-3 , inj₂ 'R' :: []) :: (just "P46" , nothing , just _alpha-range-3 , inj₂ 'Q' :: []) :: (just "P45" , nothing , just _alpha-range-3 , inj₂ 'P' :: []) :: (just "P44" , nothing , just _alpha-range-3 , inj₂ 'O' :: []) :: (just "P43" , nothing , just _alpha-range-3 , inj₂ 'N' :: []) :: (just "P42" , nothing , just _alpha-range-3 , inj₂ 'M' :: []) :: (just "P41" , nothing , just _alpha-range-3 , inj₂ 'L' :: []) :: (just "P40" , nothing , just _alpha-range-3 , inj₂ 'K' :: []) :: (just "P39" , nothing , just _alpha-range-3 , inj₂ 'J' :: []) :: (just "P38" , nothing , just _alpha-range-3 , inj₂ 'I' :: []) :: (just "P37" , nothing , just _alpha-range-3 , inj₂ 'H' :: []) :: (just "P36" , nothing , just _alpha-range-3 , inj₂ 'G' :: []) :: (just "P35" , nothing , just _alpha-range-3 , inj₂ 'F' :: []) :: (just "P34" , nothing , just _alpha-range-3 , inj₂ 'E' :: []) :: (just "P33" , nothing , just _alpha-range-3 , inj₂ 'D' :: []) :: (just "P32" , nothing , just _alpha-range-3 , inj₂ 'C' :: []) :: (just "P31" , nothing , just _alpha-range-3 , inj₂ 'B' :: []) :: (just "P30" , nothing , just _alpha-range-3 , inj₂ 'A' :: []) :: []
options-start _alpha-range-2 = (just "P9" , nothing , just _alpha-range-2 , inj₂ 'f' :: []) :: (just "P8" , nothing , just _alpha-range-2 , inj₂ 'e' :: []) :: (just "P7" , nothing , just _alpha-range-2 , inj₂ 'd' :: []) :: (just "P6" , nothing , just _alpha-range-2 , inj₂ 'c' :: []) :: (just "P5" , nothing , just _alpha-range-2 , inj₂ 'b' :: []) :: (just "P4" , nothing , just _alpha-range-2 , inj₂ 'a' :: []) :: (just "P29" , nothing , just _alpha-range-2 , inj₂ 'z' :: []) :: (just "P28" , nothing , just _alpha-range-2 , inj₂ 'y' :: []) :: (just "P27" , nothing , just _alpha-range-2 , inj₂ 'x' :: []) :: (just "P26" , nothing , just _alpha-range-2 , inj₂ 'w' :: []) :: (just "P25" , nothing , just _alpha-range-2 , inj₂ 'v' :: []) :: (just "P24" , nothing , just _alpha-range-2 , inj₂ 'u' :: []) :: (just "P23" , nothing , just _alpha-range-2 , inj₂ 't' :: []) :: (just "P22" , nothing , just _alpha-range-2 , inj₂ 's' :: []) :: (just "P21" , nothing , just _alpha-range-2 , inj₂ 'r' :: []) :: (just "P20" , nothing , just _alpha-range-2 , inj₂ 'q' :: []) :: (just "P19" , nothing , just _alpha-range-2 , inj₂ 'p' :: []) :: (just "P18" , nothing , just _alpha-range-2 , inj₂ 'o' :: []) :: (just "P17" , nothing , just _alpha-range-2 , inj₂ 'n' :: []) :: (just "P16" , nothing , just _alpha-range-2 , inj₂ 'm' :: []) :: (just "P15" , nothing , just _alpha-range-2 , inj₂ 'l' :: []) :: (just "P14" , nothing , just _alpha-range-2 , inj₂ 'k' :: []) :: (just "P13" , nothing , just _alpha-range-2 , inj₂ 'j' :: []) :: (just "P12" , nothing , just _alpha-range-2 , inj₂ 'i' :: []) :: (just "P11" , nothing , just _alpha-range-2 , inj₂ 'h' :: []) :: (just "P10" , nothing , just _alpha-range-2 , inj₂ 'g' :: []) :: []
options-start _alpha-bar-4 = (just "P57" , nothing , just _alpha-bar-4 , inj₁ _alpha-range-3 :: []) :: (just "P56" , nothing , just _alpha-bar-4 , inj₁ _alpha-range-2 :: []) :: []
options-start _alpha = (just "P58" , nothing , just _alpha , inj₁ _alpha-bar-4 :: []) :: []

options-return : maybe gratr2-nt → 𝕃 gratr2-rule
options-return _ = []

options-rtn : gratr2-rtn
options-rtn = record { start = _start ; _eq_ = gratr2-nt-eq ; gratr2-start = options-start ; gratr2-return = options-return }

open import run ptr
open noderiv

------------------------------------------
-- Length-decreasing rules
------------------------------------------

len-dec-rewrite : Run → maybe (Run × ℕ)
len-dec-rewrite {- File-} ((Id "File") :: (ParseTree (parsed-opts x0)) :: _::_(ParseTree parsed-ows) rest) = just (ParseTree (parsed-start (norm-start (File x0))) ::' rest , 3)
len-dec-rewrite {- GenerateLogs-} ((Id "GenerateLogs") :: (InputChar 'g') :: (InputChar 'e') :: (InputChar 'n') :: (InputChar 'e') :: (InputChar 'r') :: (InputChar 'a') :: (InputChar 't') :: (InputChar 'e') :: (InputChar '-') :: (InputChar 'l') :: (InputChar 'o') :: (InputChar 'g') :: (InputChar 's') :: (ParseTree parsed-ows) :: (InputChar '=') :: (ParseTree parsed-ows) :: (ParseTree (parsed-str-bool x0)) :: (ParseTree parsed-ows) :: (InputChar '.') :: _::_(ParseTree parsed-ows) rest) = just (ParseTree (parsed-opt (norm-opt (GenerateLogs x0))) ::' rest , 21)
len-dec-rewrite {- Lib-} ((Id "Lib") :: (InputChar 'i') :: (InputChar 'm') :: (InputChar 'p') :: (InputChar 'o') :: (InputChar 'r') :: (InputChar 't') :: (InputChar '-') :: (InputChar 'd') :: (InputChar 'i') :: (InputChar 'r') :: (InputChar 'e') :: (InputChar 'c') :: (InputChar 't') :: (InputChar 'o') :: (InputChar 'r') :: (InputChar 'i') :: (InputChar 'e') :: (InputChar 's') :: (ParseTree parsed-ows) :: (InputChar '=') :: (ParseTree parsed-ows) :: (ParseTree (parsed-paths x0)) :: (ParseTree parsed-ows) :: _::_(InputChar '.') rest) = just (ParseTree (parsed-opt (norm-opt (Lib x0))) ::' rest , 25)
len-dec-rewrite {- MakeRktFiles-} ((Id "MakeRktFiles") :: (InputChar 'm') :: (InputChar 'a') :: (InputChar 'k') :: (InputChar 'e') :: (InputChar '-') :: (InputChar 'r') :: (InputChar 'k') :: (InputChar 't') :: (InputChar '-') :: (InputChar 'f') :: (InputChar 'i') :: (InputChar 'l') :: (InputChar 'e') :: (InputChar 's') :: (ParseTree parsed-ows) :: (InputChar '=') :: (ParseTree parsed-ows) :: (ParseTree (parsed-str-bool x0)) :: (ParseTree parsed-ows) :: (InputChar '.') :: _::_(ParseTree parsed-ows) rest) = just (ParseTree (parsed-opt (norm-opt (MakeRktFiles x0))) ::' rest , 22)
len-dec-rewrite {- OptsCons-} ((Id "OptsCons") :: (ParseTree parsed-ows) :: (ParseTree (parsed-opt x0)) :: _::_(ParseTree (parsed-opts x1)) rest) = just (ParseTree (parsed-opts (norm-opts (OptsCons x0 x1))) ::' rest , 4)
len-dec-rewrite {- P0-} ((Id "P0") :: _::_(InputChar '\"') rest) = just (ParseTree parsed-squote ::' rest , 2)
len-dec-rewrite {- P10-} ((Id "P10") :: _::_(InputChar 'g') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'g'))) ::' rest , 2)
len-dec-rewrite {- P100-} ((Id "P100") :: _::_(InputChar '[') rest) = just (ParseTree (parsed-anychar-bar-20 (string-append 0 (char-to-string '['))) ::' rest , 2)
len-dec-rewrite {- P101-} ((Id "P101") :: _::_(ParseTree (parsed-anychar-bar-19 x0)) rest) = just (ParseTree (parsed-anychar-bar-20 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P102-} ((Id "P102") :: _::_(InputChar '.') rest) = just (ParseTree (parsed-anychar-bar-21 (string-append 0 (char-to-string '.'))) ::' rest , 2)
len-dec-rewrite {- P103-} ((Id "P103") :: _::_(ParseTree (parsed-anychar-bar-20 x0)) rest) = just (ParseTree (parsed-anychar-bar-21 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P104-} ((Id "P104") :: _::_(InputChar ':') rest) = just (ParseTree (parsed-anychar-bar-22 (string-append 0 (char-to-string ':'))) ::' rest , 2)
len-dec-rewrite {- P105-} ((Id "P105") :: _::_(ParseTree (parsed-anychar-bar-21 x0)) rest) = just (ParseTree (parsed-anychar-bar-22 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P106-} ((Id "P106") :: _::_(InputChar ')') rest) = just (ParseTree (parsed-anychar-bar-23 (string-append 0 (char-to-string ')'))) ::' rest , 2)
len-dec-rewrite {- P107-} ((Id "P107") :: _::_(ParseTree (parsed-anychar-bar-22 x0)) rest) = just (ParseTree (parsed-anychar-bar-23 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P108-} ((Id "P108") :: _::_(InputChar '(') rest) = just (ParseTree (parsed-anychar-bar-24 (string-append 0 (char-to-string '('))) ::' rest , 2)
len-dec-rewrite {- P109-} ((Id "P109") :: _::_(ParseTree (parsed-anychar-bar-23 x0)) rest) = just (ParseTree (parsed-anychar-bar-24 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P11-} ((Id "P11") :: _::_(InputChar 'h') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'h'))) ::' rest , 2)
len-dec-rewrite {- P110-} ((Id "P110") :: _::_(InputChar '%') rest) = just (ParseTree (parsed-anychar-bar-25 (string-append 0 (char-to-string '%'))) ::' rest , 2)
len-dec-rewrite {- P111-} ((Id "P111") :: _::_(ParseTree (parsed-anychar-bar-24 x0)) rest) = just (ParseTree (parsed-anychar-bar-25 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P112-} ((Id "P112") :: _::_(InputChar ' ') rest) = just (ParseTree (parsed-anychar-bar-26 (string-append 0 (char-to-string ' '))) ::' rest , 2)
len-dec-rewrite {- P113-} ((Id "P113") :: _::_(ParseTree (parsed-anychar-bar-25 x0)) rest) = just (ParseTree (parsed-anychar-bar-26 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P114-} ((Id "P114") :: _::_(InputChar '\t') rest) = just (ParseTree (parsed-anychar-bar-27 (string-append 0 (char-to-string '\t'))) ::' rest , 2)
len-dec-rewrite {- P115-} ((Id "P115") :: _::_(ParseTree (parsed-anychar-bar-26 x0)) rest) = just (ParseTree (parsed-anychar-bar-27 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P116-} ((Id "P116") :: _::_(ParseTree (parsed-numpunct x0)) rest) = just (ParseTree (parsed-anychar-bar-28 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P117-} ((Id "P117") :: _::_(ParseTree (parsed-anychar-bar-27 x0)) rest) = just (ParseTree (parsed-anychar-bar-28 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P118-} ((Id "P118") :: _::_(ParseTree (parsed-alpha x0)) rest) = just (ParseTree (parsed-anychar-bar-29 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P119-} ((Id "P119") :: _::_(ParseTree (parsed-anychar-bar-28 x0)) rest) = just (ParseTree (parsed-anychar-bar-29 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P12-} ((Id "P12") :: _::_(InputChar 'i') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'i'))) ::' rest , 2)
len-dec-rewrite {- P120-} ((Id "P120") :: _::_(ParseTree (parsed-anychar-bar-29 x0)) rest) = just (ParseTree (parsed-anychar (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P122-} ((Id "P122") :: (ParseTree (parsed-anychar x0)) :: _::_(ParseTree parsed-comment-star-30) rest) = just (ParseTree parsed-comment-star-30 ::' rest , 3)
len-dec-rewrite {- P123-} ((Id "P123") :: (InputChar '%') :: (ParseTree parsed-comment-star-30) :: _::_(InputChar '\n') rest) = just (ParseTree parsed-comment ::' rest , 4)
len-dec-rewrite {- P124-} ((Id "P124") :: _::_(InputChar ' ') rest) = just (ParseTree parsed-aws-bar-31 ::' rest , 2)
len-dec-rewrite {- P125-} ((Id "P125") :: _::_(ParseTree parsed-comment) rest) = just (ParseTree parsed-aws-bar-31 ::' rest , 2)
len-dec-rewrite {- P126-} ((Id "P126") :: _::_(InputChar '\t') rest) = just (ParseTree parsed-aws-bar-32 ::' rest , 2)
len-dec-rewrite {- P127-} ((Id "P127") :: _::_(ParseTree parsed-aws-bar-31) rest) = just (ParseTree parsed-aws-bar-32 ::' rest , 2)
len-dec-rewrite {- P128-} ((Id "P128") :: _::_(InputChar '\n') rest) = just (ParseTree parsed-aws-bar-33 ::' rest , 2)
len-dec-rewrite {- P129-} ((Id "P129") :: _::_(ParseTree parsed-aws-bar-32) rest) = just (ParseTree parsed-aws-bar-33 ::' rest , 2)
len-dec-rewrite {- P13-} ((Id "P13") :: _::_(InputChar 'j') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'j'))) ::' rest , 2)
len-dec-rewrite {- P130-} ((Id "P130") :: _::_(ParseTree parsed-aws-bar-33) rest) = just (ParseTree parsed-aws ::' rest , 2)
len-dec-rewrite {- P131-} ((Id "P131") :: _::_(ParseTree parsed-aws) rest) = just (ParseTree parsed-ws-plus-34 ::' rest , 2)
len-dec-rewrite {- P132-} ((Id "P132") :: (ParseTree parsed-aws) :: _::_(ParseTree parsed-ws-plus-34) rest) = just (ParseTree parsed-ws-plus-34 ::' rest , 3)
len-dec-rewrite {- P133-} ((Id "P133") :: _::_(ParseTree parsed-ws-plus-34) rest) = just (ParseTree parsed-ws ::' rest , 2)
len-dec-rewrite {- P135-} ((Id "P135") :: (ParseTree parsed-aws) :: _::_(ParseTree parsed-ows-star-35) rest) = just (ParseTree parsed-ows-star-35 ::' rest , 3)
len-dec-rewrite {- P136-} ((Id "P136") :: _::_(ParseTree parsed-ows-star-35) rest) = just (ParseTree parsed-ows ::' rest , 2)
len-dec-rewrite {- P14-} ((Id "P14") :: _::_(InputChar 'k') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'k'))) ::' rest , 2)
len-dec-rewrite {- P15-} ((Id "P15") :: _::_(InputChar 'l') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'l'))) ::' rest , 2)
len-dec-rewrite {- P16-} ((Id "P16") :: _::_(InputChar 'm') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'm'))) ::' rest , 2)
len-dec-rewrite {- P17-} ((Id "P17") :: _::_(InputChar 'n') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'n'))) ::' rest , 2)
len-dec-rewrite {- P18-} ((Id "P18") :: _::_(InputChar 'o') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'o'))) ::' rest , 2)
len-dec-rewrite {- P19-} ((Id "P19") :: _::_(InputChar 'p') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'p'))) ::' rest , 2)
len-dec-rewrite {- P2-} ((Id "P2") :: (ParseTree (parsed-anychar x0)) :: _::_(ParseTree (parsed-path-star-1 x1)) rest) = just (ParseTree (parsed-path-star-1 (string-append 1 x0 x1)) ::' rest , 3)
len-dec-rewrite {- P20-} ((Id "P20") :: _::_(InputChar 'q') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'q'))) ::' rest , 2)
len-dec-rewrite {- P21-} ((Id "P21") :: _::_(InputChar 'r') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'r'))) ::' rest , 2)
len-dec-rewrite {- P22-} ((Id "P22") :: _::_(InputChar 's') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 's'))) ::' rest , 2)
len-dec-rewrite {- P23-} ((Id "P23") :: _::_(InputChar 't') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 't'))) ::' rest , 2)
len-dec-rewrite {- P24-} ((Id "P24") :: _::_(InputChar 'u') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'u'))) ::' rest , 2)
len-dec-rewrite {- P25-} ((Id "P25") :: _::_(InputChar 'v') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'v'))) ::' rest , 2)
len-dec-rewrite {- P26-} ((Id "P26") :: _::_(InputChar 'w') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'w'))) ::' rest , 2)
len-dec-rewrite {- P27-} ((Id "P27") :: _::_(InputChar 'x') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'x'))) ::' rest , 2)
len-dec-rewrite {- P28-} ((Id "P28") :: _::_(InputChar 'y') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'y'))) ::' rest , 2)
len-dec-rewrite {- P29-} ((Id "P29") :: _::_(InputChar 'z') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'z'))) ::' rest , 2)
len-dec-rewrite {- P3-} ((Id "P3") :: (ParseTree parsed-squote) :: (ParseTree (parsed-path-star-1 x0)) :: _::_(ParseTree parsed-squote) rest) = just (ParseTree (parsed-path (string-append 0 x0)) ::' rest , 4)
len-dec-rewrite {- P30-} ((Id "P30") :: _::_(InputChar 'A') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'A'))) ::' rest , 2)
len-dec-rewrite {- P31-} ((Id "P31") :: _::_(InputChar 'B') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'B'))) ::' rest , 2)
len-dec-rewrite {- P32-} ((Id "P32") :: _::_(InputChar 'C') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'C'))) ::' rest , 2)
len-dec-rewrite {- P33-} ((Id "P33") :: _::_(InputChar 'D') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'D'))) ::' rest , 2)
len-dec-rewrite {- P34-} ((Id "P34") :: _::_(InputChar 'E') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'E'))) ::' rest , 2)
len-dec-rewrite {- P35-} ((Id "P35") :: _::_(InputChar 'F') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'F'))) ::' rest , 2)
len-dec-rewrite {- P36-} ((Id "P36") :: _::_(InputChar 'G') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'G'))) ::' rest , 2)
len-dec-rewrite {- P37-} ((Id "P37") :: _::_(InputChar 'H') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'H'))) ::' rest , 2)
len-dec-rewrite {- P38-} ((Id "P38") :: _::_(InputChar 'I') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'I'))) ::' rest , 2)
len-dec-rewrite {- P39-} ((Id "P39") :: _::_(InputChar 'J') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'J'))) ::' rest , 2)
len-dec-rewrite {- P4-} ((Id "P4") :: _::_(InputChar 'a') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'a'))) ::' rest , 2)
len-dec-rewrite {- P40-} ((Id "P40") :: _::_(InputChar 'K') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'K'))) ::' rest , 2)
len-dec-rewrite {- P41-} ((Id "P41") :: _::_(InputChar 'L') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'L'))) ::' rest , 2)
len-dec-rewrite {- P42-} ((Id "P42") :: _::_(InputChar 'M') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'M'))) ::' rest , 2)
len-dec-rewrite {- P43-} ((Id "P43") :: _::_(InputChar 'N') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'N'))) ::' rest , 2)
len-dec-rewrite {- P44-} ((Id "P44") :: _::_(InputChar 'O') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'O'))) ::' rest , 2)
len-dec-rewrite {- P45-} ((Id "P45") :: _::_(InputChar 'P') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'P'))) ::' rest , 2)
len-dec-rewrite {- P46-} ((Id "P46") :: _::_(InputChar 'Q') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'Q'))) ::' rest , 2)
len-dec-rewrite {- P47-} ((Id "P47") :: _::_(InputChar 'R') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'R'))) ::' rest , 2)
len-dec-rewrite {- P48-} ((Id "P48") :: _::_(InputChar 'S') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'S'))) ::' rest , 2)
len-dec-rewrite {- P49-} ((Id "P49") :: _::_(InputChar 'T') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'T'))) ::' rest , 2)
len-dec-rewrite {- P5-} ((Id "P5") :: _::_(InputChar 'b') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'b'))) ::' rest , 2)
len-dec-rewrite {- P50-} ((Id "P50") :: _::_(InputChar 'U') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'U'))) ::' rest , 2)
len-dec-rewrite {- P51-} ((Id "P51") :: _::_(InputChar 'V') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'V'))) ::' rest , 2)
len-dec-rewrite {- P52-} ((Id "P52") :: _::_(InputChar 'W') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'W'))) ::' rest , 2)
len-dec-rewrite {- P53-} ((Id "P53") :: _::_(InputChar 'X') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'X'))) ::' rest , 2)
len-dec-rewrite {- P54-} ((Id "P54") :: _::_(InputChar 'Y') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'Y'))) ::' rest , 2)
len-dec-rewrite {- P55-} ((Id "P55") :: _::_(InputChar 'Z') rest) = just (ParseTree (parsed-alpha-range-3 (string-append 0 (char-to-string 'Z'))) ::' rest , 2)
len-dec-rewrite {- P56-} ((Id "P56") :: _::_(ParseTree (parsed-alpha-range-2 x0)) rest) = just (ParseTree (parsed-alpha-bar-4 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P57-} ((Id "P57") :: _::_(ParseTree (parsed-alpha-range-3 x0)) rest) = just (ParseTree (parsed-alpha-bar-4 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P58-} ((Id "P58") :: _::_(ParseTree (parsed-alpha-bar-4 x0)) rest) = just (ParseTree (parsed-alpha (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P59-} ((Id "P59") :: _::_(InputChar '0') rest) = just (ParseTree (parsed-numone-range-5 (string-append 0 (char-to-string '0'))) ::' rest , 2)
len-dec-rewrite {- P6-} ((Id "P6") :: _::_(InputChar 'c') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'c'))) ::' rest , 2)
len-dec-rewrite {- P60-} ((Id "P60") :: _::_(InputChar '1') rest) = just (ParseTree (parsed-numone-range-5 (string-append 0 (char-to-string '1'))) ::' rest , 2)
len-dec-rewrite {- P61-} ((Id "P61") :: _::_(InputChar '2') rest) = just (ParseTree (parsed-numone-range-5 (string-append 0 (char-to-string '2'))) ::' rest , 2)
len-dec-rewrite {- P62-} ((Id "P62") :: _::_(InputChar '3') rest) = just (ParseTree (parsed-numone-range-5 (string-append 0 (char-to-string '3'))) ::' rest , 2)
len-dec-rewrite {- P63-} ((Id "P63") :: _::_(InputChar '4') rest) = just (ParseTree (parsed-numone-range-5 (string-append 0 (char-to-string '4'))) ::' rest , 2)
len-dec-rewrite {- P64-} ((Id "P64") :: _::_(InputChar '5') rest) = just (ParseTree (parsed-numone-range-5 (string-append 0 (char-to-string '5'))) ::' rest , 2)
len-dec-rewrite {- P65-} ((Id "P65") :: _::_(InputChar '6') rest) = just (ParseTree (parsed-numone-range-5 (string-append 0 (char-to-string '6'))) ::' rest , 2)
len-dec-rewrite {- P66-} ((Id "P66") :: _::_(InputChar '7') rest) = just (ParseTree (parsed-numone-range-5 (string-append 0 (char-to-string '7'))) ::' rest , 2)
len-dec-rewrite {- P67-} ((Id "P67") :: _::_(InputChar '8') rest) = just (ParseTree (parsed-numone-range-5 (string-append 0 (char-to-string '8'))) ::' rest , 2)
len-dec-rewrite {- P68-} ((Id "P68") :: _::_(InputChar '9') rest) = just (ParseTree (parsed-numone-range-5 (string-append 0 (char-to-string '9'))) ::' rest , 2)
len-dec-rewrite {- P69-} ((Id "P69") :: _::_(ParseTree (parsed-numone-range-5 x0)) rest) = just (ParseTree (parsed-numone (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P7-} ((Id "P7") :: _::_(InputChar 'd') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'd'))) ::' rest , 2)
len-dec-rewrite {- P70-} ((Id "P70") :: _::_(ParseTree (parsed-numone x0)) rest) = just (ParseTree (parsed-num-plus-6 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P71-} ((Id "P71") :: (ParseTree (parsed-numone x0)) :: _::_(ParseTree (parsed-num-plus-6 x1)) rest) = just (ParseTree (parsed-num-plus-6 (string-append 1 x0 x1)) ::' rest , 3)
len-dec-rewrite {- P72-} ((Id "P72") :: _::_(ParseTree (parsed-num-plus-6 x0)) rest) = just (ParseTree (parsed-num (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P73-} ((Id "P73") :: _::_(InputChar '\'') rest) = just (ParseTree (parsed-numpunct-bar-7 (string-append 0 (char-to-string '\''))) ::' rest , 2)
len-dec-rewrite {- P74-} ((Id "P74") :: _::_(InputChar '-') rest) = just (ParseTree (parsed-numpunct-bar-7 (string-append 0 (char-to-string '-'))) ::' rest , 2)
len-dec-rewrite {- P75-} ((Id "P75") :: _::_(ParseTree (parsed-numone x0)) rest) = just (ParseTree (parsed-numpunct-bar-8 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P76-} ((Id "P76") :: _::_(ParseTree (parsed-numpunct-bar-7 x0)) rest) = just (ParseTree (parsed-numpunct-bar-8 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P77-} ((Id "P77") :: _::_(ParseTree (parsed-numpunct-bar-8 x0)) rest) = just (ParseTree (parsed-numpunct (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P78-} ((Id "P78") :: _::_(InputChar '/') rest) = just (ParseTree (parsed-anychar-bar-9 (string-append 0 (char-to-string '/'))) ::' rest , 2)
len-dec-rewrite {- P79-} ((Id "P79") :: _::_(InputChar '_') rest) = just (ParseTree (parsed-anychar-bar-9 (string-append 0 (char-to-string '_'))) ::' rest , 2)
len-dec-rewrite {- P8-} ((Id "P8") :: _::_(InputChar 'e') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'e'))) ::' rest , 2)
len-dec-rewrite {- P80-} ((Id "P80") :: _::_(InputChar '>') rest) = just (ParseTree (parsed-anychar-bar-10 (string-append 0 (char-to-string '>'))) ::' rest , 2)
len-dec-rewrite {- P81-} ((Id "P81") :: _::_(ParseTree (parsed-anychar-bar-9 x0)) rest) = just (ParseTree (parsed-anychar-bar-10 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P82-} ((Id "P82") :: _::_(InputChar '<') rest) = just (ParseTree (parsed-anychar-bar-11 (string-append 0 (char-to-string '<'))) ::' rest , 2)
len-dec-rewrite {- P83-} ((Id "P83") :: _::_(ParseTree (parsed-anychar-bar-10 x0)) rest) = just (ParseTree (parsed-anychar-bar-11 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P84-} ((Id "P84") :: _::_(InputChar '+') rest) = just (ParseTree (parsed-anychar-bar-12 (string-append 0 (char-to-string '+'))) ::' rest , 2)
len-dec-rewrite {- P85-} ((Id "P85") :: _::_(ParseTree (parsed-anychar-bar-11 x0)) rest) = just (ParseTree (parsed-anychar-bar-12 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P86-} ((Id "P86") :: _::_(InputChar '=') rest) = just (ParseTree (parsed-anychar-bar-13 (string-append 0 (char-to-string '='))) ::' rest , 2)
len-dec-rewrite {- P87-} ((Id "P87") :: _::_(ParseTree (parsed-anychar-bar-12 x0)) rest) = just (ParseTree (parsed-anychar-bar-13 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P88-} ((Id "P88") :: _::_(InputChar '-') rest) = just (ParseTree (parsed-anychar-bar-14 (string-append 0 (char-to-string '-'))) ::' rest , 2)
len-dec-rewrite {- P89-} ((Id "P89") :: _::_(ParseTree (parsed-anychar-bar-13 x0)) rest) = just (ParseTree (parsed-anychar-bar-14 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P9-} ((Id "P9") :: _::_(InputChar 'f') rest) = just (ParseTree (parsed-alpha-range-2 (string-append 0 (char-to-string 'f'))) ::' rest , 2)
len-dec-rewrite {- P90-} ((Id "P90") :: _::_(InputChar '}') rest) = just (ParseTree (parsed-anychar-bar-15 (string-append 0 (char-to-string '}'))) ::' rest , 2)
len-dec-rewrite {- P91-} ((Id "P91") :: _::_(ParseTree (parsed-anychar-bar-14 x0)) rest) = just (ParseTree (parsed-anychar-bar-15 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P92-} ((Id "P92") :: _::_(InputChar '{') rest) = just (ParseTree (parsed-anychar-bar-16 (string-append 0 (char-to-string '{'))) ::' rest , 2)
len-dec-rewrite {- P93-} ((Id "P93") :: _::_(ParseTree (parsed-anychar-bar-15 x0)) rest) = just (ParseTree (parsed-anychar-bar-16 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P94-} ((Id "P94") :: _::_(InputChar '!') rest) = just (ParseTree (parsed-anychar-bar-17 (string-append 0 (char-to-string '!'))) ::' rest , 2)
len-dec-rewrite {- P95-} ((Id "P95") :: _::_(ParseTree (parsed-anychar-bar-16 x0)) rest) = just (ParseTree (parsed-anychar-bar-17 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P96-} ((Id "P96") :: _::_(InputChar ',') rest) = just (ParseTree (parsed-anychar-bar-18 (string-append 0 (char-to-string ','))) ::' rest , 2)
len-dec-rewrite {- P97-} ((Id "P97") :: _::_(ParseTree (parsed-anychar-bar-17 x0)) rest) = just (ParseTree (parsed-anychar-bar-18 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- P98-} ((Id "P98") :: _::_(InputChar ']') rest) = just (ParseTree (parsed-anychar-bar-19 (string-append 0 (char-to-string ']'))) ::' rest , 2)
len-dec-rewrite {- P99-} ((Id "P99") :: _::_(ParseTree (parsed-anychar-bar-18 x0)) rest) = just (ParseTree (parsed-anychar-bar-19 (string-append 0 x0)) ::' rest , 2)
len-dec-rewrite {- PathsCons-} ((Id "PathsCons") :: (ParseTree parsed-ws) :: (ParseTree (parsed-path x0)) :: _::_(ParseTree (parsed-paths x1)) rest) = just (ParseTree (parsed-paths (norm-paths (PathsCons x0 x1))) ::' rest , 4)
len-dec-rewrite {- ShowQualifiedVars-} ((Id "ShowQualifiedVars") :: (InputChar 's') :: (InputChar 'h') :: (InputChar 'o') :: (InputChar 'w') :: (InputChar '-') :: (InputChar 'q') :: (InputChar 'u') :: (InputChar 'a') :: (InputChar 'l') :: (InputChar 'i') :: (InputChar 'f') :: (InputChar 'i') :: (InputChar 'e') :: (InputChar 'd') :: (InputChar '-') :: (InputChar 'v') :: (InputChar 'a') :: (InputChar 'r') :: (InputChar 's') :: (ParseTree parsed-ows) :: (InputChar '=') :: (ParseTree parsed-ows) :: (ParseTree (parsed-str-bool x0)) :: (ParseTree parsed-ows) :: (InputChar '.') :: _::_(ParseTree parsed-ows) rest) = just (ParseTree (parsed-opt (norm-opt (ShowQualifiedVars x0))) ::' rest , 27)
len-dec-rewrite {- StrBoolFalse-} ((Id "StrBoolFalse") :: (InputChar 'f') :: (InputChar 'a') :: (InputChar 'l') :: (InputChar 's') :: _::_(InputChar 'e') rest) = just (ParseTree (parsed-str-bool (norm-str-bool StrBoolFalse)) ::' rest , 6)
len-dec-rewrite {- StrBoolTrue-} ((Id "StrBoolTrue") :: (InputChar 't') :: (InputChar 'r') :: (InputChar 'u') :: _::_(InputChar 'e') rest) = just (ParseTree (parsed-str-bool (norm-str-bool StrBoolTrue)) ::' rest , 5)
len-dec-rewrite {- UseCedeFiles-} ((Id "UseCedeFiles") :: (InputChar 'u') :: (InputChar 's') :: (InputChar 'e') :: (InputChar '-') :: (InputChar 'c') :: (InputChar 'e') :: (InputChar 'd') :: (InputChar 'e') :: (InputChar '-') :: (InputChar 'f') :: (InputChar 'i') :: (InputChar 'l') :: (InputChar 'e') :: (InputChar 's') :: (ParseTree parsed-ows) :: (InputChar '=') :: (ParseTree parsed-ows) :: (ParseTree (parsed-str-bool x0)) :: (ParseTree parsed-ows) :: (InputChar '.') :: _::_(ParseTree parsed-ows) rest) = just (ParseTree (parsed-opt (norm-opt (UseCedeFiles x0))) ::' rest , 22)
len-dec-rewrite {- OptsNil-} (_::_(Id "OptsNil") rest) = just (ParseTree (parsed-opts (norm-opts OptsNil)) ::' rest , 1)
len-dec-rewrite {- P1-} (_::_(Id "P1") rest) = just (ParseTree (parsed-path-star-1 empty-string) ::' rest , 1)
len-dec-rewrite {- P121-} (_::_(Id "P121") rest) = just (ParseTree parsed-comment-star-30 ::' rest , 1)
len-dec-rewrite {- P134-} (_::_(Id "P134") rest) = just (ParseTree parsed-ows-star-35 ::' rest , 1)
len-dec-rewrite {- PathsNil-} (_::_(Id "PathsNil") rest) = just (ParseTree (parsed-paths (norm-paths PathsNil)) ::' rest , 1)
len-dec-rewrite {- Posinfo-} (_::_(Posinfo n) rest) = just (ParseTree (parsed-posinfo (ℕ-to-string n)) ::' rest , 1)
len-dec-rewrite x = nothing

rrs : rewriteRules
rrs = record { len-dec-rewrite = len-dec-rewrite }

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.Types
open import LibraBFT.Abstract.Types.EpochConfig
open        WithAbsVote

-- This module defines RecordChains and related types and utility definitions

module LibraBFT.Abstract.RecordChain
  (UID    : Set)
  (_≟UID_ : (u₀ u₁ : UID) → Dec (u₀ ≡ u₁))
  (NodeId : Set)
  (𝓔      : EpochConfig UID NodeId)
  (𝓥      : VoteEvidence UID NodeId 𝓔)
  where
 open import LibraBFT.Abstract.Records         UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.Records.Extends UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.Types           UID        NodeId
 open        EpochConfig 𝓔

 -- One way of looking at a 'RecordChain r' is as a path from the epoch's
 -- initial record (I) to r.  For generality, we express this in two steps.
 data RecordChainFrom (o : Record) : Record → Set where
   empty : RecordChainFrom o o
   step  : ∀ {r r'}
         → (rc : RecordChainFrom o r)
         → r ← r'
         → RecordChainFrom o r'

 RecordChain : Record → Set
 RecordChain = RecordChainFrom I

 prevBlock : ∀{q} → RecordChain (Q q) → Block
 prevBlock (step {r = B b} _ (B←Q _ _)) = b

 prevQCorI : ∀{b} → RecordChain (B b) → Record
 prevQCorI (step _ (I←B _ _))           = I
 prevQCorI (step {r = Q q} _ (Q←B _ _)) = Q q

 -- Returns the unique identifier of the parent tagged to be either
 -- the initial block or a B or Q.
 parentUID : ∀{b} → RecordChain (B b) → TypedUID
 parentUID (step {r = I} _ _)   = id-I
 parentUID (step {r = Q q} _ _) = id-B∨Q (qCertBlockId q)

 -- Defition of 'previous_round' as in Section 5.5 (see Abstract.Properties).
 currRound : ∀{r} → RecordChain r → Round
 currRound empty = 0
 currRound (step {r = r} _ _) = round r

 -- TODO-1: it would be cleaner to define prevRound only for RecordChains ending in a Block.
 prevRound : ∀{r} → RecordChain r → Round
 prevRound empty = 0
 prevRound (step rc (I←B x vr)) = 0
 prevRound (step rc (Q←B x vr)) = currRound rc
 prevRound (step rc (B←Q x vr)) = prevRound rc

 -- Extensional definition of prevRound; useful to 'rewrite' on.
 prevRound-ss : ∀{b₁ q b}(rc : RecordChain (B b₁))
              → (ext₁ : B b₁ ← Q q)
              → (ext₀ : Q q  ← B b)
              → prevRound (step (step rc ext₁) ext₀) ≡ bRound b₁
 prevRound-ss rc (B←Q _ _) (Q←B _ _) = refl

 ----------------------
 -- RecordChain Equality and Irrelevance
 --

 -- Distributing a record relation pointwise
 -- over record chains. Let rc₀ and rc₁ be as illustrated
 -- below; a value of type ≈RC-pw, named prf is shown
 -- in between them.
 --
 --  rc₀    : B₀ ← C₀  ← B₁ ← C₁ ← ⋯ ← Bₖ  ← Cₖ
 --
 --  prf      ≈    ≈     ≈    ≈        ≈     ≈
 --
 --  rc₁    : 𝓑₀ ← 𝓒₀ ← 𝓑₁ ← 𝓒₁ ← ⋯ ← 𝓑ₖ ← 𝓒ₖ
 --
 --
 data ≈RC-pw {ℓ}(_≈_ : Rel Record ℓ)
     : ∀{o₀ o₁ r₀ r₁} → RecordChainFrom o₀ r₀ → RecordChainFrom o₁ r₁ → Set ℓ where
   eq-empty : ∀{o₀ o₁} → o₀ ≈ o₁ → ≈RC-pw _≈_ (empty {o = o₀}) (empty {o = o₁})
   eq-step  : ∀{o₀ o₁ r₀ r₁ s₀ s₁}
            → (rc₀ : RecordChainFrom o₀ s₀)
            → (rc₁ : RecordChainFrom o₁ s₁)
            → r₀ ≈ r₁
            → (ext₀ : s₀ ← r₀)
            → (ext₁ : s₁ ← r₁)
            → ≈RC-pw _≈_ rc₀ rc₁
            → ≈RC-pw _≈_ (step rc₀ ext₀) (step rc₁ ext₁)

 -- RecordChain equivalence is then defined in terms of
 -- record equivalence (i.e., we don't care about the set of
 -- votes for the QCs in the chain); borrowing the illustration
 -- above, we now have:
 --
 --  rc₀    : B₀ ← C₀  ← B₁ ← C₁ ← ⋯ ← Bₖ  ← Cₖ
 --
 --  prf      ≡    ≈QC   ≡    ≈QC      ≡     ≈QC
 --
 --  rc₁    : 𝓑₀ ← 𝓒₀ ← 𝓑₁ ← 𝓒₁ ← ⋯ ← 𝓑ₖ ← 𝓒ₖ
 --
 -- It is easy to see that if rc₀ ≈RC rc₁, then they contain
 -- the same blocks (propositionally!) but potentially
 -- different /sets of votes/ certifying said blocks.
 _≈RC_ : ∀{o₀ o₁ r₀ r₁} → RecordChainFrom o₀ r₀ → RecordChainFrom o₁ r₁ → Set
 _≈RC_ = ≈RC-pw _≈Rec_

 ≈RC-head : ∀{o₀ o₁ r₀ r₁}{rc₀ : RecordChainFrom o₀ r₀}{rc₁ : RecordChainFrom o₁ r₁}
          → rc₀ ≈RC rc₁ → o₀ ≈Rec o₁
 ≈RC-head (eq-empty x)          = x
 ≈RC-head (eq-step _ _ _ _ _ x) = ≈RC-head x

 -- Heterogeneous irrelevance of _≈RC_ happens only modulo
 -- propositional non-injectivity of block ids.
 ≈RC-refl : ∀{r₀ r₁}(rc₀ : RecordChain r₀)(rc₁ : RecordChain r₁)
          → r₀ ≈Rec r₁
          → NonInjective _≡_ bId ⊎ (rc₀ ≈RC rc₁)
 ≈RC-refl empty empty hyp
    = inj₂ (eq-empty hyp)
 ≈RC-refl (step r0 x) (step r1 x₁) hyp
    = (←-≈Rec x x₁ hyp ⊎⟫= ≈RC-refl r0 r1)
       ⊎⟫= (inj₂ ∘ eq-step r0 r1 hyp x x₁)
 ≈RC-refl empty (step r1 (I←B x x₁)) ()
 ≈RC-refl empty (step r1 (Q←B x x₁)) ()
 ≈RC-refl empty (step r1 (B←Q x x₁)) ()
 ≈RC-refl (step r0 (I←B x x₁)) empty ()
 ≈RC-refl (step r0 (Q←B x x₁)) empty ()
 ≈RC-refl (step r0 (B←Q x x₁)) empty ()

 ≈RC-sym : ∀{o₀ o₁ r₀ r₁}{rc₀ : RecordChainFrom o₀ r₀}{rc₁ : RecordChainFrom o₁ r₁}
         → rc₀ ≈RC rc₁ → rc₁ ≈RC rc₀
 ≈RC-sym (eq-empty x) = eq-empty (≈Rec-sym x)
 ≈RC-sym (eq-step rc₀ rc₁ x ext₀ ext₁ hyp) = eq-step rc₁ rc₀ (≈Rec-sym x) ext₁ ext₀ (≈RC-sym hyp)

 ≈RC-trans : ∀ {r₀ r₁ r₂}
           → {rc₀ : RecordChain r₀}{rc₁ : RecordChain r₁}{rc₂ : RecordChain r₂}
           → rc₀ ≈RC rc₁ → rc₁ ≈RC rc₂ → rc₀ ≈RC rc₂
 ≈RC-trans (eq-empty x) q = q
 ≈RC-trans (eq-step rc₀ rc₁ x ext₀ ext₁ p) (eq-step .rc₁ rc₂ x₁ .ext₁ ext₂ q)
    = eq-step rc₀ rc₂ (≈Rec-trans x x₁) ext₀ ext₂ (≈RC-trans p q)

 -- Heterogeneous irrelevance proves that two record chains that end at the same record
 -- have the same blocks and equivalent QCs.
 RecordChain-irrelevant : ∀{r}(rc₀ : RecordChain r)(rc₁ : RecordChain r)
                        → NonInjective _≡_ bId ⊎ rc₀ ≈RC rc₁
 RecordChain-irrelevant rc0 rc1 = ≈RC-refl rc0 rc1 ≈Rec-refl

 -------------------------------------------------
 -- Sub RecordChains

 -- A value of type '⊆RC-pw _≈_ rc1 rc2' establishes that rc1 is
 -- a suffix of rc2 modulo _≈_.
 data ⊆RC-pw {ℓ}(_≈_ : Rel Record ℓ)
     : ∀{o₀ o₁ r₀ r₁} → RecordChainFrom o₀ r₀ → RecordChainFrom o₁ r₁ → Set ℓ where
   sub-empty : ∀{o₀ o₁ s₁}{r₁ : RecordChainFrom o₁ s₁} → o₀ ≈ s₁ → ⊆RC-pw _≈_ (empty {o = o₀}) r₁
   sub-step  : ∀{o₀ o₁ r₀ r₁ s₀ s₁}
            → (rc₀ : RecordChainFrom o₀ s₀)
            → (rc₁ : RecordChainFrom o₁ s₁)
            → r₀ ≈ r₁
            → (ext₀ : s₀ ← r₀)
            → (ext₁ : s₁ ← r₁)
            → ⊆RC-pw _≈_ rc₀ rc₁
            → ⊆RC-pw _≈_ (step rc₀ ext₀) (step rc₁ ext₁)

 _⊆RC_ : ∀{o₀ o₁ r₀ r₁} → RecordChainFrom o₀ r₀ → RecordChainFrom o₁ r₁ → Set
 _⊆RC_ = ⊆RC-pw _≈Rec_

 -- The ⊆RC relation is used to establish irrelevance of suffixes
 RecordChainFrom-irrelevant : ∀{o₀ o₁ r₀ r₁}(rc₀ : RecordChainFrom o₀ r₀)(rc₁ : RecordChainFrom o₁ r₁)
                            → r₀ ≈Rec r₁
                            → NonInjective _≡_ bId ⊎ (rc₀ ⊆RC rc₁ ⊎ rc₁ ⊆RC rc₀)
 RecordChainFrom-irrelevant empty empty hyp = inj₂ (inj₁ (sub-empty hyp))
 RecordChainFrom-irrelevant empty (step rc1 x) hyp = inj₂ (inj₁ (sub-empty hyp))
 RecordChainFrom-irrelevant (step rc0 x) empty hyp = inj₂ (inj₂ (sub-empty (≈Rec-sym hyp)))
 RecordChainFrom-irrelevant (step rc0 x) (step rc1 x₁) hyp
   = (←-≈Rec x x₁ hyp ⊎⟫= RecordChainFrom-irrelevant rc0 rc1)
     ⊎⟫= (inj₂ ∘ either (inj₁ ∘ sub-step rc0 rc1 hyp x x₁) (inj₂ ∘ sub-step rc1 rc0 (≈Rec-sym hyp) x₁ x))

 -- If a chain from the initial record is a suffix from a second chain,
 -- then the second chain is also from the initial record.
 RecordChain-glb : ∀{o' r r'}{rc : RecordChain r}{rcf : RecordChainFrom o' r'}
                 → rc ⊆RC rcf
                 → rc ≈RC rcf
 RecordChain-glb {rcf = step _ ()} (sub-empty eq-I)
 RecordChain-glb {rcf = empty}     (sub-empty eq-I) = eq-empty eq-I
 RecordChain-glb (sub-step rc₀ rc₁ x ext₀ ext₁ sub) = eq-step rc₀ rc₁ x ext₀ ext₁ (RecordChain-glb sub)

 -------------------------------------------------
 -- Id congruences over RecordChain equivalences

 parentUID-≈ : ∀{b₀ b₁}(rc₀ : RecordChain (B b₀))(rc₁ : RecordChain (B b₁))
             → rc₀ ≈RC rc₁
             → parentUID rc₀ ≡ parentUID rc₁
 parentUID-≈ _ _ (eq-step _ _ (eq-B refl) _ _ (eq-empty x)) = refl
 parentUID-≈ _ _ (eq-step _ _ (eq-B refl) _ _ (eq-step _ _ (eq-Q refl) _ _ _)) = refl

 --------------------------
 -- RecordChain elements

 data _∈RC-simple_ {o : Record}(r₀ : Record) : ∀{r₁} → RecordChainFrom o r₁ → Set where
   here   : ∀{rc : RecordChainFrom o r₀} → r₀ ∈RC-simple rc
   there  : ∀{r₁ r₂}{rc : RecordChainFrom o r₁}(p : r₁ ← r₂)
          → r₀ ∈RC-simple rc
          → r₀ ∈RC-simple (step rc p)

 -- States that a given record belongs in a record chain.
 data _∈RC_ {o : Record}(r₀ : Record) : ∀{r₁} → RecordChainFrom o r₁ → Set where
   here   : ∀{rc : RecordChainFrom o r₀} → r₀ ∈RC rc
   there  : ∀{r₁ r₂}{rc : RecordChainFrom o r₁}(p : r₁ ← r₂)
          → r₀ ∈RC rc
          → r₀ ∈RC (step rc p)
   -- This is an important rule. It is the equivalent of a
   -- /congruence/ on record chains and enables us to prove
   -- the 𝕂-chain-∈RC property.
   transp : ∀{r}{rc₀ : RecordChainFrom o r}{rc₁ : RecordChainFrom o r}
          → r₀ ∈RC rc₀ → rc₀ ≈RC rc₁ → r₀ ∈RC rc₁

 ∈RC-empty-I : ∀{r} → r ∈RC (empty {o = I}) → r ≡ I
 ∈RC-empty-I here                      = refl
 ∈RC-empty-I (transp old (eq-empty x)) = ∈RC-empty-I old

 b∉RCempty : ∀ {b} → B b ∈RC empty → ⊥
 b∉RCempty xx with ∈RC-empty-I xx
 ...| ()

 transp-B∈RC : ∀{r r' b}{rc : RecordChain r}{rc' : RecordChain r'}
             → rc ≈RC rc' → B b ∈RC rc → B b ∈RC rc'
 transp-B∈RC rc≈rc' (transp b∈rc x) = transp-B∈RC (≈RC-trans x rc≈rc') b∈rc
 transp-B∈RC (eq-step rc₀ rc₁ (eq-B refl) ext₀ ext₁ rc≈rc') here = here
 transp-B∈RC (eq-step rc₀ rc₁ x .p ext₁ rc≈rc') (there p b∈rc) = there ext₁ (transp-B∈RC rc≈rc' b∈rc)

 -- A k-chain (paper Section 5.2; see Abstract.Properties) is a sequence of
 -- blocks and quorum certificates for said blocks:
 --
 --  B₀ ← C₀ ← B₁ ← C₁ ← ⋯ ← Bₖ ← Cₖ
 --
 -- such that for each Bᵢ some predicate R is satisfies for Bᵢ and Bᵢ₊₁.
 -- The first parameter R enables predicate definitions to avoid the need
 -- to find a predecessor for B₀ (see Contig definition below).
 --
 -- The 𝕂-chain datatype captures exactly that structure.
 --
 data 𝕂-chain (R : ℕ → Record → Record → Set)
     : (k : ℕ){o r : Record} → RecordChainFrom o r → Set where
   0-chain : ∀{o r}{rc : RecordChainFrom o r} → 𝕂-chain R 0 rc
   s-chain : ∀{k o r}{rc : RecordChainFrom o r}{b : Block}{q : QC}
           → (r←b : r   ← B b)
           → (prf : R k r (B b))
           → (b←q : B b ← Q q)
           → 𝕂-chain R k rc
           → 𝕂-chain R (suc k) (step (step rc r←b) b←q)

 -- Simple 𝕂-chains do not impose any restricton on its records.
 Simple : ℕ → Record → Record → Set
 Simple _ _ _ = Unit

 -- Contiguous 𝕂-chains are those in which all adjacent pairs of Records have contiguous rounds.
 Contig : ℕ → Record → Record → Set
 Contig 0       _  _ = Unit
 Contig (suc _) r r' = round r' ≡ suc (round r)

 -- The 'Contig' relation is substitutive in a rather restrictive setting,
 -- but this is enough for our purposes.
 Contig-subst : ∀{k r r' b}{rc : RecordChain r}{rc' : RecordChain r'}
              → rc ≈RC rc'
              → r ← (B b)
              → Contig k r (B b) → Contig k r' (B b)
 Contig-subst {zero}  _            _ _  = unit
 Contig-subst {suc k} (eq-empty x) _ cr = cr
 Contig-subst {suc k} (eq-step .(step rc₀ ext₂) .(step rc₁ ext₃) (eq-Q x) (B←Q refl refl) (B←Q refl refl)
                    (eq-step rc₀ rc₁ (eq-B refl) ext₂ ext₃ rc≈rc')) (Q←B h0 h1) cr = cr

 -- Consequently, contiguous 𝕂-chains are substitutive w.r.t. _≈RC_
 transp-𝕂-chain : ∀{k r r'}{rc : RecordChain r}{rc' : RecordChain r'}
                → rc ≈RC rc'
                → 𝕂-chain Contig k rc
                → 𝕂-chain Contig k rc'
 transp-𝕂-chain rc≈rc' 0-chain = 0-chain
 transp-𝕂-chain (eq-step .(step rc₀ r←b) .(step rc₁ r←b') (eq-Q refl) _ ext₁
                   (eq-step rc₀ rc₁ (eq-B refl) .r←b r←b' rc≈rc'))
                (s-chain r←b prf (B←Q _ _) kc) =
    s-chain r←b' (Contig-subst rc≈rc' r←b prf) ext₁ (transp-𝕂-chain rc≈rc' kc)

 -- TODO-2: Consider duplicating the above for the ⊆RC relation.
 -- I believe we can generalize all of this via the same function, but
 -- it's nontrivial to change the whole module.
 --
 -- Arguably, the right way to deal with all of this would be to
 -- design the bare record chain type as the most expressive possible:
 --
 -- data RC : ℕ → Record → Record
 --
 -- Then, a value r of type 'RC 12 I (B b)' represents a record chain with
 -- 12 steps from I to (B b). K-chains become trivial to express:
 --
 -- K-chain k = RC (2*k) ...

 Contig-subst-⊆ : ∀{k o o' r r' b}{rc : RecordChainFrom o r}{rc' : RecordChainFrom o' r'}
                → (kc : 𝕂-chain Contig k rc)
                → rc ⊆RC rc'
                → r ← (B b)
                → Contig k r (B b) → Contig k r' (B b)
 Contig-subst-⊆ 0-chain _ ext hyp = unit
 Contig-subst-⊆ (s-chain r←b prf _ kc) (sub-step _ _ (eq-Q x) (B←Q refl refl) (B←Q refl refl)
                                         (sub-step rc₀ rc₁ (eq-B refl) .r←b ext₂ sub)) ext hyp
   = hyp

 transp-𝕂-chain-⊆ : ∀{k o o' r r'}{rc : RecordChainFrom o r}{rc' : RecordChainFrom o' r'}
                → rc ⊆RC rc'
                → 𝕂-chain Contig k rc
                → 𝕂-chain Contig k rc'
 transp-𝕂-chain-⊆ rc⊆rc' 0-chain = 0-chain
 transp-𝕂-chain-⊆ (sub-step .(step rc₀ r←b) .(step rc₁ r←b') (eq-Q refl) _ ext₁
                   (sub-step rc₀ rc₁ (eq-B refl) .r←b r←b' rc⊆rc'))
                (s-chain r←b prf (B←Q _ _) kc) =
    s-chain r←b' (Contig-subst-⊆ kc rc⊆rc' r←b prf) ext₁ (transp-𝕂-chain-⊆ rc⊆rc' kc)

 𝕂-chain-contig : (k : ℕ){o r : Record} → RecordChainFrom o r → Set
 𝕂-chain-contig = 𝕂-chain Contig

 𝕂-chain-to-Simple : ∀{R k r}{rc : RecordChain r} → 𝕂-chain R k rc → 𝕂-chain Simple k rc
 𝕂-chain-to-Simple 0-chain = 0-chain
 𝕂-chain-to-Simple (s-chain r←b prf b←q kc) = s-chain r←b unit b←q (𝕂-chain-to-Simple kc)

 -- Every record chain that ends in a QC is a 𝕂-chain
 to-kchain : ∀{q}(rc : RecordChain (Q q)) → ∃[ k ] (𝕂-chain Simple k rc)
 to-kchain (step (step {B b} rc ()) x@(B←Q _ _))
 to-kchain (step (step {I} rc x₁)   x@(B←Q _ _))
  = 1 , s-chain x₁ unit x 0-chain
 to-kchain (step (step {Q q} rc x₁) x@(B←Q _ _))
  with to-kchain rc
 ...| k , kc = suc k , s-chain x₁ unit x kc

 kchainForget : ∀{P k r}{rc : RecordChain r}(c : 𝕂-chain P k rc) → RecordChain r
 kchainForget {rc = rc} _ = rc

 -- Returns the round of the block heading the k-chain.
 kchainHeadRound : ∀{k r P}{rc : RecordChain r} → 𝕂-chain P k rc → Round
 kchainHeadRound (0-chain {r = r})      = round r
 kchainHeadRound (s-chain r←b _ b←q kk) = kchainHeadRound kk

 kchainBlock : ∀{k o r P}{rc : RecordChainFrom o r} → Fin k → 𝕂-chain P k rc → Block
 kchainBlock zero    (s-chain {b = b} _ _ _ _) = b
 kchainBlock (suc x) (s-chain r←b _ b←q kk)    = kchainBlock x kk

 kchainBlock-toSimple-≡
   : ∀{k r P}{rc : RecordChain r}(x : Fin k)(c : 𝕂-chain P k rc)
   → kchainBlock x (𝕂-chain-to-Simple c) ≡ kchainBlock x c
 kchainBlock-toSimple-≡ zero    (s-chain _ _ _ _)  = refl
 kchainBlock-toSimple-≡ (suc x) (s-chain _ _ _ kk) = kchainBlock-toSimple-≡ x kk

 _b⟦_⟧ : ∀{k o r P}{rc : RecordChainFrom o r} → 𝕂-chain P k rc → Fin k → Block
 chain b⟦ ix ⟧ = kchainBlock ix chain

 kchainBlock-≈RC : ∀{k r r'}{rc : RecordChain r}{rc' : RecordChain r'}
                 → (c3 : 𝕂-chain Contig k rc)(ix : Fin k)
                 → (rc≈rc' : rc ≈RC rc')
                 → c3 b⟦ ix ⟧ ≡ transp-𝕂-chain rc≈rc' c3 b⟦ ix ⟧
 kchainBlock-≈RC 0-chain () _
 kchainBlock-≈RC (s-chain r←b prf (B←Q _ _) kc) ix
                 (eq-step .(step rc₀ r←b) .(step rc₁ r←b') (eq-Q refl) _ ext₁
                   (eq-step rc₀ rc₁ (eq-B refl) .r←b r←b' rc≈rc'))
   with ix
 ...| zero    = refl
 ...| suc ix' = kchainBlock-≈RC kc ix' rc≈rc'

 kchainBlock-⊆RC : ∀{k o o' r r'}{rc : RecordChainFrom o r}{rc' : RecordChainFrom o' r'}
                 → (c3 : 𝕂-chain Contig k rc)(ix : Fin k)
                 → (rc⊆rc' : rc ⊆RC rc')
                 → c3 b⟦ ix ⟧ ≡ transp-𝕂-chain-⊆ rc⊆rc' c3 b⟦ ix ⟧
 kchainBlock-⊆RC 0-chain () _
 kchainBlock-⊆RC (s-chain r←b prf (B←Q _ _) kc) ix
                 (sub-step .(step rc₀ r←b) .(step rc₁ r←b') (eq-Q refl) _ ext₁
                   (sub-step rc₀ rc₁ (eq-B refl) .r←b r←b' rc≈rc'))
   with ix
 ...| zero    = refl
 ...| suc ix' = kchainBlock-⊆RC kc ix' rc≈rc'

 kchainQC : ∀{k r P}{rc : RecordChain r} → Fin k → 𝕂-chain P k rc → QC
 kchainQC zero    (s-chain {q = q} _ _ _ _) = q
 kchainQC (suc x) (s-chain r←b _ b←q kk)    = kchainQC x kk

 kchain-to-RecordChain-at-b⟦⟧
   : ∀{P k r}{rc : RecordChain r}(c : 𝕂-chain P k rc)(ix : Fin k)
   → RecordChain (B (c b⟦ ix ⟧))
 kchain-to-RecordChain-at-b⟦⟧ 0-chain ()
 kchain-to-RecordChain-at-b⟦⟧ (s-chain {rc = rc} r←b x b←q c) zero
   = (step rc r←b)
 kchain-to-RecordChain-at-b⟦⟧ (s-chain r←b x b←q c) (suc zz)
   = kchain-to-RecordChain-at-b⟦⟧ c zz

 kchainBlockRoundZero-lemma
   : ∀{k q P}{rc : RecordChain (Q q)}(c : 𝕂-chain P (suc k) rc)
   → getRound (kchainBlock zero c) ≡ getRound q
 kchainBlockRoundZero-lemma (s-chain r←b prf (B←Q r h) c) = sym r

 kchainBlockRound≤ : ∀{k r P}{rc : RecordChain r}(x y : Fin k)(kc : 𝕂-chain P k rc)
                   → x ≤Fin y → getRound (kchainBlock y kc) ≤ getRound (kchainBlock x kc)
 kchainBlockRound≤ zero zero (s-chain r←b prf b←q kc) hyp = ≤-refl
 kchainBlockRound≤ zero (suc y) (s-chain (Q←B r r←b) prf b←q (s-chain r←b₁ prf₁ (B←Q refl b←q₁) kc)) hyp
   = ≤-trans (kchainBlockRound≤ zero y (s-chain r←b₁ prf₁ (B←Q refl b←q₁) kc) z≤n) (<⇒≤ r)
 kchainBlockRound≤ (suc x) (suc y) (s-chain r←b prf b←q kc) (s≤s hyp)
   = kchainBlockRound≤ x y kc hyp

 kchain-round-≤-lemma'
   : ∀{k q}{rc : RecordChain (Q q)}(c3 : 𝕂-chain Contig k rc)(ix : Fin k)
   → getRound (c3 b⟦ ix ⟧) ≤ getRound q
 kchain-round-≤-lemma' (s-chain r←b x (B←Q refl b←q) c3) zero = ≤-refl
 kchain-round-≤-lemma' (s-chain (I←B prf imp) unit (B←Q refl _) 0-chain) (suc ())
 kchain-round-≤-lemma' (s-chain (Q←B prf imp) x (B←Q refl _) c2) (suc ix)
   = ≤-trans (kchain-round-≤-lemma' c2 ix) (<⇒≤ prf)

 rc-←-maxRound : ∀{r r'}(rc : RecordChain r') → r ∈RC rc → round r ≤ round r'
 rc-←-maxRound rc here                 = ≤-refl
 rc-←-maxRound rc (transp n x)         = rc-←-maxRound _ n
 rc-←-maxRound .(step _ p) (there p n) = ≤-trans (rc-←-maxRound _ n) (←-round-≤ p)

 kchainBlock-correct
   : ∀{P k q b}{rc : RecordChain (B b)}{b←q : B b ← Q q}
   → (kc : 𝕂-chain P k (step rc b←q))
   → (x : Fin k) → (B (kc b⟦ x ⟧)) ∈RC rc
 kchainBlock-correct (s-chain r←b prf b←q kc) zero = here
 kchainBlock-correct (s-chain r←b prf b←q (s-chain r←b₁ prf₁ b←q₁ kc)) (suc x)
   = there r←b (there b←q₁ (kchainBlock-correct (s-chain r←b₁ prf₁ b←q₁ kc) x))

 -- This is an extended form of RecordChain-irrelevance.
 -- Let rc be:
 --
 --  B₀ ← C₀ ← B₁ ← C₁ ← ⋯ ← Bₙ ← Cₙ
 --
 -- The (c : 𝕂-chain P k rc) is a predicate on the shape
 -- of rc, establishing that it must be of the following shape:
 -- (where consecutive blocks satisfy P)
 --
 --  B₀ ← C₀ ← B₁ ← C₁ ← ⋯ ← Bₙ₋ₖ ← Cₙ₋ₖ ⋯ ← Bₙ₋₁ ← Cₙ₋₁ ← Bₙ ← Cₙ
 --                           /\             /\            /
 --                     ⋯ P ₋⌟  ⌞₋₋₋₋ P ₋₋₋₋⌟  ⌞₋₋₋₋ P ₋₋₋⌟
 --
 -- This property states that any other RecordChain that contains one
 -- block b of the kchain above, it also contains the prefix of the
 -- kchain leading to b.
 --
 𝕂-chain-∈RC : ∀{r k P}{rc : RecordChain r}
             → (c : 𝕂-chain P k rc)
             → (x y : Fin k)
             → x ≤Fin y
             → {b : Block}(prf : kchainBlock x c ≡ b)
             → (rc₁ : RecordChain (B b))
             → NonInjective _≡_ bId ⊎ (B (kchainBlock y c) ∈RC rc₁)
 𝕂-chain-∈RC (s-chain r←b prf b←q c) zero y z≤n refl rc1
   with RecordChain-irrelevant (step (kchainForget c) r←b) rc1
 ...| inj₁ hb   = inj₁ hb
 ...| inj₂ res  = inj₂ (transp (kchainBlock-correct (s-chain r←b prf b←q c) y) res)
 𝕂-chain-∈RC (s-chain r←b prf b←q c) (suc x) (suc y) (s≤s x≤y) hyp rc1
   = 𝕂-chain-∈RC c x y x≤y hyp rc1

 -----------------
 -- Commit Rule --

 -- A block (and everything preceeding it) is said to match the commit rule
 -- when the block is the head of a contiguious 3-chain. Here we define an auxiliary
 -- datatype to make definitions more readable.
 data CommitRuleFrom {o r : Record}(rc : RecordChainFrom o r)(b : Block) : Set where
   commit-rule : (c3 : 𝕂-chain Contig 3 rc)
               → b ≡ c3 b⟦ suc (suc zero) ⟧
               → CommitRuleFrom rc b

 CommitRule : ∀{r} → RecordChain r → Block → Set
 CommitRule = CommitRuleFrom

 transp-CR : ∀{b q}{rc rc' : RecordChain (Q q)}
           → rc ≈RC rc'
           → CommitRule rc  b
           → CommitRule rc' b
 transp-CR rc≈rc' (commit-rule c3 x) =
   commit-rule (transp-𝕂-chain rc≈rc' c3)
               (trans x (kchainBlock-≈RC c3 (suc (suc zero)) rc≈rc'))

 crf⇒cr : ∀ {o q b}
        → (rcf : RecordChainFrom o (Q q))
        → (rc : RecordChain (Q q))
        → CommitRuleFrom rcf b
        → NonInjective-≡ bId ⊎ CommitRule {Q q} rc b
 crf⇒cr rcf rc (commit-rule c3 prf)
   with RecordChainFrom-irrelevant rcf rc ≈Rec-refl
 ...| inj₁ hb = inj₁ hb
 ...| inj₂ (inj₁ rcf⊆rc) = inj₂ (commit-rule (transp-𝕂-chain-⊆ rcf⊆rc c3)
                                             (trans prf (kchainBlock-⊆RC c3 (suc (suc zero)) rcf⊆rc)))
 ...| inj₂ (inj₂ rc⊆rcf)
   with ≈RC-sym (RecordChain-glb rc⊆rcf)
 ...| rcf≈rc
   with ≈RC-head rcf≈rc
 ...| eq-I = inj₂ (transp-CR rcf≈rc (commit-rule c3 prf))

 vote≡⇒QPrevId≡ : {q q' : QC} {v v' : Vote}
                → v  ∈ qcVotes q
                → v' ∈ qcVotes q'
                → v ≡ v'
                → qCertBlockId q ≡ qCertBlockId q'
 vote≡⇒QPrevId≡ {q} {q'} v∈q v'∈q' refl
     with witness v∈q (qVotes-C2 q) | witness v'∈q' (qVotes-C2 q')
 ... | refl | refl = refl

 vote≡⇒QRound≡ : {q q' : QC} {v v' : Vote}
               → v  ∈ qcVotes q
               → v' ∈ qcVotes q'
               → v ≡ v'
               → getRound q ≡ getRound q'
 vote≡⇒QRound≡ {q} {q'} v∈q v'∈q' refl
     with witness v∈q (qVotes-C3 q) | witness v'∈q' (qVotes-C3 q')
 ... | refl | refl = refl

 ¬bRound≡0 : ∀{b} → RecordChain (B b) → ¬ (getRound b ≡ 0)
 ¬bRound≡0 (step s (I←B ()  h)) refl
 ¬bRound≡0 (step s (Q←B () h)) refl

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda