From da35892c463cd6b9a492c6aee09726a41031ca93 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Mon, 29 Mar 2021 15:56:46 +0100 Subject: Rename parse to derivation. --- src/Cfe/Derivation.agda | 10 +++ src/Cfe/Derivation/Base.agda | 25 +++++++ src/Cfe/Derivation/Properties.agda | 132 +++++++++++++++++++++++++++++++++++++ src/Cfe/Parse.agda | 10 --- src/Cfe/Parse/Base.agda | 25 ------- src/Cfe/Parse/Properties.agda | 132 ------------------------------------- 6 files changed, 167 insertions(+), 167 deletions(-) create mode 100644 src/Cfe/Derivation.agda create mode 100644 src/Cfe/Derivation/Base.agda create mode 100644 src/Cfe/Derivation/Properties.agda delete mode 100644 src/Cfe/Parse.agda delete mode 100644 src/Cfe/Parse/Base.agda delete mode 100644 src/Cfe/Parse/Properties.agda (limited to 'src/Cfe') diff --git a/src/Cfe/Derivation.agda b/src/Cfe/Derivation.agda new file mode 100644 index 0000000..4d54f8f --- /dev/null +++ b/src/Cfe/Derivation.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary using (Setoid) + +module Cfe.Derivation + {c ℓ} (over : Setoid c ℓ) + where + +open import Cfe.Derivation.Base over public +open import Cfe.Derivation.Properties over public diff --git a/src/Cfe/Derivation/Base.agda b/src/Cfe/Derivation/Base.agda new file mode 100644 index 0000000..1f2bb63 --- /dev/null +++ b/src/Cfe/Derivation/Base.agda @@ -0,0 +1,25 @@ +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary using (Setoid) + +module Cfe.Derivation.Base + {c ℓ} (over : Setoid c ℓ) + where + +open Setoid over renaming (Carrier to C; _≈_ to _∼_) + +open import Cfe.Expression over hiding (_≋_) +open import Data.Fin +open import Data.List +open import Data.List.Relation.Binary.Equality.Setoid over +open import Level using (_⊔_) + +infix 4 _⤇_ + +data _⤇_ : Expression 0 → List C → Set (c ⊔ ℓ) where + Eps : ε ⤇ [] + Char : ∀ {c y} → c ∼ y → Char c ⤇ [ y ] + Cat : ∀ {e₁ e₂ l₁ l₂ l} → e₁ ⤇ l₁ → e₂ ⤇ l₂ → l₁ ++ l₂ ≋ l → e₁ ∙ e₂ ⤇ l + Veeˡ : ∀ {e₁ e₂ l} → e₁ ⤇ l → e₁ ∨ e₂ ⤇ l + Veeʳ : ∀ {e₁ e₂ l} → e₂ ⤇ l → e₁ ∨ e₂ ⤇ l + Fix : ∀ {e l} → e [ μ e / zero ] ⤇ l → μ e ⤇ l diff --git a/src/Cfe/Derivation/Properties.agda b/src/Cfe/Derivation/Properties.agda new file mode 100644 index 0000000..303d2f9 --- /dev/null +++ b/src/Cfe/Derivation/Properties.agda @@ -0,0 +1,132 @@ +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary using (Setoid) + +module Cfe.Derivation.Properties + {c ℓ} (over : Setoid c ℓ) + where + +open Setoid over renaming (Carrier to C) + +open import Cfe.Context over hiding (_≋_) +open import Cfe.Expression over hiding (_≋_) +open import Cfe.Language over hiding (≤-refl) +open import Cfe.Language.Construct.Concatenate over using (Concat) +open import Cfe.Language.Indexed.Construct.Iterate over +open import Cfe.Judgement over +open import Cfe.Derivation.Base over +open import Cfe.Type over using (_⊛_; _⊨_) +open import Data.Bool using (T; not; true; false) +open import Data.Empty using (⊥-elim) +open import Data.Fin as F hiding (_<_) +open import Data.List hiding (null) +open import Data.List.Relation.Binary.Equality.Setoid over +open import Data.Nat as ℕ hiding (_⊔_; _^_; _<_) +open import Data.Nat.Properties using (≤-step; m≤m+n; m≤n+m; ≤-refl; n<1+n; module ≤-Reasoning) +open import Data.Nat.Induction using () renaming (<-wellFounded to <ⁿ-wellFounded) +open import Data.Product as Product +open import Data.Product.Relation.Binary.Lex.Strict +open import Data.Sum as Sum +open import Data.Vec hiding (length; _++_) +open import Data.Vec.Relation.Binary.Pointwise.Inductive +open import Data.Vec.Relation.Binary.Pointwise.Extensional +open import Function +open import Induction.WellFounded +open import Level +open import Relation.Binary +import Relation.Binary.Construct.On as On +open import Relation.Binary.PropositionalEquality as ≡ hiding (subst₂; setoid) + +private + infix 4 _<_ + _<_ : Rel (List C × Expression 0) _ + _<_ = ×-Lex _≡_ ℕ._<_ ℕ._<_ on (Product.map length rank) + + <-wellFounded : WellFounded _<_ + <-wellFounded = On.wellFounded (Product.map length rank) (×-wellFounded <ⁿ-wellFounded <ⁿ-wellFounded) + +l∈⟦e⟧⇒e⤇l : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {l} → l ∈ ⟦ e ⟧ [] → e ⤇ l +l∈⟦e⟧⇒e⤇l {e} {τ} ∙,∙⊢e∶τ {l} l∈⟦e⟧ = All.wfRec <-wellFounded _ Pred go (l , e) ∙,∙⊢e∶τ l∈⟦e⟧ + where + Pred : List C × Expression 0 → Set _ + Pred (l , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → l ∈ ⟦ e ⟧ [] → e ⤇ l + + e[μe/0]<μe : ∀ {e τ} l → ∙,∙ ⊢ μ e ∶ τ → (l , e [ μ e / F.zero ]) < (l , μ e) + e[μe/0]<μe {e} l (Fix ∙,τ⊢e∶τ)= inj₂ (≡.refl , (begin-strict + rank (e [ μ e / F.zero ]) ≡⟨ subst-preserves-rank z≤n ∙,τ⊢e∶τ (Fix ∙,τ⊢e∶τ) ⟩ + rank e <⟨ n<1+n (rank e) ⟩ + ℕ.suc (rank e) ≡⟨⟩ + rank (μ e) ∎)) + where + open ≤-Reasoning + + l₁++l₂≋l⇒∣l₁∣≤∣l∣ : ∀ {l₂ l} l₁ → l₁ ++ l₂ ≋ l → (length l₁ ℕ.< length l) ⊎ (length l₁ ≡ length l) + l₁++l₂≋l⇒∣l₁∣≤∣l∣ [] [] = inj₂ ≡.refl + l₁++l₂≋l⇒∣l₁∣≤∣l∣ [] (_ ∷ _) = inj₁ (s≤s z≤n) + l₁++l₂≋l⇒∣l₁∣≤∣l∣ (_ ∷ l₁) (_ ∷ eq) = Sum.map s≤s (cong ℕ.suc) (l₁++l₂≋l⇒∣l₁∣≤∣l∣ l₁ eq) + + l₁++l₂≋l⇒∣l₂∣≤∣l∣ : ∀ {l₂ l} l₁ → l₁ ++ l₂ ≋ l → (length l₂ ℕ.< length l) ⊎ (length l₁ ≡ 0) + l₁++l₂≋l⇒∣l₂∣≤∣l∣ [] _ = inj₂ ≡.refl + l₁++l₂≋l⇒∣l₂∣≤∣l∣ (_ ∷ []) (_ ∷ []) = inj₁ (s≤s z≤n) + l₁++l₂≋l⇒∣l₂∣≤∣l∣ (x ∷ []) (x∼y ∷ _ ∷ eq) = inj₁ ([ s≤s , (λ ()) ]′ (l₁++l₂≋l⇒∣l₂∣≤∣l∣ (x ∷ []) (x∼y ∷ eq))) + l₁++l₂≋l⇒∣l₂∣≤∣l∣ (_ ∷ x ∷ l₁) (_ ∷ eq) = inj₁ ([ ≤-step , (λ ()) ]′ (l₁++l₂≋l⇒∣l₂∣≤∣l∣ (x ∷ l₁) eq)) + + e₁