71 lines
1.9 KiB
Agda
71 lines
1.9 KiB
Agda
open import Data.Nat
|
||
|
||
-- what if we just wanted to describe a pattern of events of blanks
|
||
-- what are the most fundamental parts? Well you have two forms of concatenation:
|
||
-- you have alternation and addition
|
||
-- okay so this is one of those things I've run into before that the difference between alternation
|
||
-- and addition is only relative to a particular time frame: basically concatenation is alternation + a compression
|
||
{-
|
||
data Pat1 : Set where
|
||
Blank : Pat1
|
||
Hit : Pat1
|
||
Cat : Pat1 -> Pat1 -> Pat1
|
||
Alt : Pat1 -> Pat1 -> Pat1
|
||
|
||
-- A pattern doesn't mean anything unless it's turned into something
|
||
-- the most basic thing it could get turned into is, of course, a list
|
||
-- to do this you need more data: how much to extract *out* of the pattern
|
||
-- so really let's just call it a vector
|
||
|
||
data Vec (A : Set) : ℕ → Set where
|
||
[] : Vec A zero
|
||
_∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
|
||
|
||
infixr 5 _∷_
|
||
|
||
data Maybe (A : Set) : Set where
|
||
Nothing : Maybe A
|
||
Just : (a : A) -> Maybe A
|
||
|
||
data Unit : Set where
|
||
unit : Unit
|
||
|
||
nextElement : Pat1 ->
|
||
|
||
{-
|
||
-- so this is flipping trivial, and I know that
|
||
pat1ToVec : (n : ℕ) -> Pat1 -> Vec (Maybe Unit) n
|
||
pat1ToVec zero p = []
|
||
pat1ToVec (suc n) Blank = {!!}
|
||
pat1ToVec (suc n) Hit = {!!}
|
||
pat1ToVec (suc n) (Cat p p₁) = {!!}
|
||
-}
|
||
|
||
-}
|
||
|
||
-- okay I realize that the above was all very full of dogpoo because you can't actually
|
||
-- get the next element out of a pattern unless you have an index that says where you *are*
|
||
-- in the pattern
|
||
|
||
data PatGen : Set where
|
||
Blank : PatGen
|
||
Hit : PatGen
|
||
Cat : PatGen -> PatGen -> PatGen
|
||
Alt : PatGen -> PatGen -> PatGen
|
||
|
||
data Vec (A : Set) : ℕ → Set where
|
||
[] : Vec A zero
|
||
_∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
|
||
|
||
infixr 5 _∷_
|
||
|
||
data Maybe (A : Set) : Set where
|
||
Nothing : Maybe A
|
||
Just : (a : A) -> Maybe A
|
||
|
||
data Unit : Set where
|
||
unit : Unit
|
||
|
||
data Pattern : Set where
|
||
|