Patterns.agda

open import Data.Product hiding (<_,_>)
open import Data.Sum
open import Data.Unit

data Type : Set where
    One : Type
    _*_ _+_ _=>_ : Type -> Type -> Type

[[_]]ty : Type -> Set
[[ One ]]ty = ⊤
[[ A * B ]]ty = [[ A ]]ty × [[ B ]]ty
[[ A + B ]]ty = [[ A ]]ty ⊎ [[ B ]]ty
[[ A => B ]]ty = [[ A ]]ty -> [[ B ]]ty

data PType : Set where
    d : Type -> PType
    _->>_ : Type -> PType -> PType

[[_]]pty : PType -> Set
[[ d A ]]pty = [[ A ]]ty
[[ A ->> B ]]pty = [[ A ]]ty -> [[ B ]]pty

data Context : Set where
    [] : Context
    _,_ : Context -> Type -> Context

[[_]]ctx : Context -> Set
[[ [] ]]ctx = ⊤
[[ G , A ]]ctx = [[ G ]]ctx × [[ A ]]ty

data Var : (G : Context) -> (A : Type) -> Set where
    here : forall {G A} -> Var (G , A) A
    there : forall {G A B} -> Var G A -> Var (G , B) A

mutual

    data Term (G : Context) : (A : Type) -> Set where
        <> : Term G One
        <_,_> : forall {A B} -> Term G A -> Term G B -> Term G (A * B)
        left : forall {A B} -> Term G A -> Term G (A + B)
        right : forall {A B} -> Term G B -> Term G (A + B)
        lam : forall {A B} -> PatternMatch G (A ->> d B) -> Term G (A => B)
        _$_ : forall {A B} -> Term G (A => B) -> Term G A -> Term G B
        var : forall {A} -> Var G A -> Term G A

    data PatternMatch (G : Context) : (A : PType) -> Set where
        d : forall {R} -> Term G R -> PatternMatch G (d R)
        <> : forall {A} -> PatternMatch G A -> PatternMatch G (One ->> A)
        <,> : forall {A B C} -> PatternMatch G (A ->> (B ->> C)) -> PatternMatch G ((A * B) ->> C)
        lr : forall {A B C} -> PatternMatch G (A ->> C) -> PatternMatch G (B ->> C) -> PatternMatch G ((A + B) ->> C)
        var : forall {A B} -> PatternMatch (G , A) B -> PatternMatch G (A ->> B)

[[_]]var : forall {G A} -> Var G A -> [[ G ]]ctx -> [[ A ]]ty
[[ here ]]var (env , v) = v
[[ there x ]]var (env , v) = [[ x ]]var env

mutual

    [[_]]tm : forall {G A} -> Term G A -> [[ G ]]ctx -> [[ A ]]ty
    [[ <> ]]tm env = tt
    [[ < M , N > ]]tm env = [[ M ]]tm env , [[ N ]]tm env
    [[ left M ]]tm env = inj₁ ([[ M ]]tm env)
    [[ right N ]]tm env = inj₂ ([[ N ]]tm env)
    [[ lam P ]]tm env = [[ P ]]pat env
    [[ M $ N ]]tm env = [[ M ]]tm env ([[ N ]]tm env)
    [[ var x ]]tm env = [[ x ]]var env

    [[_]]pat : forall {G A} -> PatternMatch G A -> [[ G ]]ctx -> [[ A ]]pty
    [[ d M ]]pat env = [[ M ]]tm env
    [[ <> P ]]pat env = \ _ -> [[ P ]]pat env
    [[ <,> P ]]pat env = \ { (x , y) -> [[ P ]]pat env x y }
    [[ lr P Q ]]pat env = \ { (inj₁ x) -> [[ P ]]pat env x ; (inj₂ y) -> [[ Q ]]pat env y }
    [[ var P ]]pat env = \ x -> [[ P ]]pat (env , x)

-- \ { < x , y > -> < y , x >
ex : forall {A B} -> PatternMatch [] ((A * B) ->> d (B * A))
ex = <,> (var (var (d < var here , var (there here) >)))

-- \ { (left x) -> right x ; (right y) -> left y }
ex2 : forall {A B} -> PatternMatch [] ((A + B) ->> d (B + A))
ex2 = lr (var (d (right (var here)))) (var (d (left (var here))))

-- \ { < < x , y > , z > -> < x , < y , z > > }
ex3 : forall {A B C} -> PatternMatch [] (((A * B) * C) ->> d (A * (B * C)))
ex3 = <,> (<,> (var (var (var (d < var (there (there here)) , < var (there here) , var here > >)))))

-- \ { (left (left x)) -> left x ; (left (right y)) -> right (left y) ; (right z) -> right (right z) }
ex4 : forall {A B C} -> PatternMatch [] (((A + B) + C) ->> d (A + (B + C)))
ex4 = lr (lr (var (d (left (var here)))) (var (d (right (left (var here)))))) (var (d (right (right (var here)))))