Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- open import Relation.Nullary
- open import Relation.Binary.PropositionalEquality
- module Data.Functor
- (Alphabet : Set)
- (_≤_ : (a b : Alphabet) → Set)
- (_≟_ : (a b : Alphabet) → Dec (a ≡ b))
- (_≤?_ : (a b : Alphabet) → Dec (a ≤ b))
- where
- open import RegExp.Search Alphabet _≤_ _≟_ _≤?_
- open import Data.Unit
- open import Data.Product
- open import Data.Sum
- open import Data.List
- open import Function
- open import lib.Nullary
- open import Relation.Binary.PropositionalEquality
- infixr 3 _`+_ _`*_
- data Desc : Set₁ where
- `K : (A : Set) → Desc -- constant
- `X : Desc -- recursive
- `L : Desc -- leaf
- _`+_ : (d₁ d₂ : Desc) → Desc -- disjunction
- _`*_ : (d₁ d₂ : Desc) → Desc -- conjunction
- ⟦_⟧ : (d : Desc) (X : (e f : RegExp) → Set) (e f : RegExp) → Set
- ⟦ `K A ⟧ X e f = A × e ≡ f
- ⟦ `X ⟧ X e f = X e f
- ⟦ `L ⟧ X e f = Σ[ a ∈ Alphabet ] (e ⟪ a) ≡ f
- ⟦ d₁ `+ d₂ ⟧ X e f = ⟦ d₁ ⟧ X e f ⊎ ⟦ d₂ ⟧ X e f
- ⟦ d₁ `* d₂ ⟧ X e f = Σ[ ef ∈ RegExp ] ⟦ d₁ ⟧ X e ef × ⟦ d₂ ⟧ X ef f
- data `μ (d : Desc) (e f : RegExp) : Set where
- ⟨_⟩ : ⟦ d ⟧ (`μ d) e f → `μ d e f
- μ : (d : Desc) (e : RegExp) → Set
- μ d e = Σ[ f ∈ RegExp ] ([] ∈ f) × `μ d e f
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement