Patterns2.agda

open import Data.List renaming (_∷_ to _::_)
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 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 B (A :: []) -> 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) (R : Type) : (As : List Type) -> Set where
        d : Term G R -> PatternMatch G R []
        <> : forall {Cs} -> PatternMatch G R Cs -> PatternMatch G R (One :: Cs)
        <,> : forall {A B Cs} -> PatternMatch G R (A :: B :: Cs) -> PatternMatch G R ((A * B) :: Cs)
        lr : forall {A B Cs} -> PatternMatch G R (A :: Cs) -> PatternMatch G R (B :: Cs) -> PatternMatch G R ((A + B):: Cs)
        var : forall {A Cs} -> PatternMatch (G , A) R Cs -> PatternMatch G R (A :: Cs)


data Scrutinees : (Cs : List Type) -> Set where
    [] : Scrutinees []
    _::_ : forall {A Cs} -> [[ A ]]ty -> Scrutinees Cs -> Scrutinees (A :: Cs)

[[_]]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 = \ x -> [[ P ]]pat env (x :: [])
    [[ M $ N ]]tm env = [[ M ]]tm env ([[ N ]]tm env)
    [[ var x ]]tm env = [[ x ]]var env

    [[_]]pat : forall {G R Cs} -> PatternMatch G R Cs -> [[ G ]]ctx -> Scrutinees Cs -> [[ R ]]ty
    [[ d M ]]pat env scrs = [[ M ]]tm env
    [[ <> P ]]pat env (_ :: scrs) = [[ P ]]pat env scrs
    [[ <,> P ]]pat env ((x , y) :: scrs) = [[ P ]]pat env (x :: (y :: scrs))
    [[ lr P P' ]]pat env (inj₁ x :: scrs) = [[ P ]]pat env (x :: scrs)
    [[ lr P P' ]]pat env (inj₂ y :: scrs) = [[ P' ]]pat env (y :: scrs)
    [[ var P ]]pat env (x :: scrs) = [[ P ]]pat (env , x) scrs

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

-- \ { (left x) -> right x ; (right y) -> left y }
ex2 : forall {A B} -> PatternMatch [] (B + A) ((A + B) :: [])
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)) (((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)) (((A + B) + C) :: [])
ex4 = lr (lr (var (d (left (var here)))) (var (d (right (left (var here)))))) (var (d (right (right (var here)))))