Langs.hs

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
{-# LANGUAGE GADTs #-}

{-@ LIQUID "--reflection"                @-}
{-@ LIQUID "--ple"                       @-}
{-@ LIQUID "--etabeta"                   @-}
{-@ LIQUID "--dependantcase"             @-}
{-@ LIQUID "--max-case-expand=4"         @-}

module Langs where

import Prelude hiding ((++))
import Data.List hiding ((++))

import Language.Haskell.Liquid.ProofCombinators
import Language.Haskell.Liquid.Prelude

{-@ infix :  @-}
{-@ infix !! @-}
{-@ infix ++ @-}

{-@ reflect !!     @-}
{-@ reflect ++     @-}
(++) :: [a] -> [a] -> [a]
[]     ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)

{-@ reflect singleton @-}
{-@ reflect delete    @-}
{-@ reflect sort     @-}

{-@ reflect pair @-}
pair :: a -> a -> [a]
pair x y = [x, y]

data Ty 
    = Unit
    | Ground
    | Tensor Ty Ty
    deriving (Eq, Ord)

type Ctx = [Ty]

type Structure = [Ty] -> [Ty] -> Bool

data Term where
{-@ Var :: hom:Structure -> τ:Ty -> Prop (Term hom (singleton τ) τ) @-}
    Var :: Structure -> Ty -> Term

{-@ Act :: hom:Structure -> γ:Ctx -> { δ:Ctx | hom γ δ } -> τ:Ty 
        -> Prop (Term hom γ τ) -> Prop (Term hom δ τ) @-}
    Act :: Structure -> Ctx -> Ctx -> Ty -> Term -> Term

{-@ UnitIntro :: hom:Structure -> Prop (Term hom [] Unit) @-}
    UnitIntro :: Structure -> Term

{-@ UnitElim :: hom:Structure -> γ:Ctx -> δ:Ctx -> τ:Ty 
             -> Prop (Term hom γ Unit) -> Prop (Term hom δ) 
             -> Prop (Term hom (γ ++ δ) τ) @-}
    UnitElim :: Structure -> Ctx -> Ctx -> Ty -> Term -> Term -> Term

{-@ TensorIntro :: hom:Structure -> γ:Ctx -> δ:Ctx -> τ:Ty -> σ:Ty
                -> Prop (Term hom γ τ) -> Prop (Term hom δ σ)
                -> Prop (Term hom (γ ++ δ) (Tensor τ σ)) @-}
    TensorIntro :: Structure -> Ctx -> Ctx -> Ty -> Ty -> Term -> Term -> Term

{-@ TensorElim :: hom:Structure -> γ:Ctx -> δ:Ctx -> τ:Ty -> σ:Ty -> υ:Ty
               -> Prop (Term hom γ (Tensor τ σ)) 
               -> Prop (Term hom (τ : σ : δ) υ) @-}
    TensorElim :: Structure -> Ctx -> Ctx -> Ty -> Ty -> Ty -> Term -> Term
data TERM = Term Structure Ctx Ty

{-@ reflect same @-}
same γ δ = δ == γ

{-@ type Planar Γ Τ = Prop (Term same Γ Τ) @-}

{-@ reflect permutation @-}
permutation γ δ = sort γ == sort δ

{-@ type Linear Γ Τ = Prop (Term permutation Γ Τ) @-}

{-@ foo :: τ:Ty -> σ:Ty -> Planar (pair τ σ) (Tensor τ σ) @-}
foo τ σ = TensorIntro same [τ] [σ] τ σ (Var same τ) (Var same σ)

{-@ thm :: τ:Ty -> σ:Ty -> { sort (pair τ σ) ==  sort (pair σ τ) } @-}
thm :: Ty -> Ty -> Proof
thm τ σ | τ <= σ  = trivial
        | otherwise  = trivial

-- {-@ swap :: τ:Ty -> σ:Ty -> Linear (pair τ σ) (Tensor σ τ) @-}
-- swap τ σ = Act permutation [σ, τ] [τ, σ] (Tensor σ τ) $ TensorIntro permutation [σ] [τ] σ τ (Var permutation σ) (Var permutation τ)