{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
module AST where


data Idx env t where
    Z :: Idx (t ': env) t
    S :: Idx env t -> Idx (t' ': env) t

data STy t where
    TInt :: STy Int
    TFloat :: STy Float

data V s env t =
    V (s t) (Idx env t)

data Tup s t where
    T0 :: Tup s ()
    T1 :: s t -> Tup s t
    T2 :: Tup s t1 -> Tup s t2 -> Tup s (t1, t2)

data LHS s t env env' where
    L0 :: Tup s t -> LHS s t env env
    L1 :: s t -> LHS s t env (t ': env)
    L2 :: LHS s t1 env env1 -> LHS s t2 env1 env2 -> LHS s (t1, t2) env env2

data PExpr expr env t where
    Const :: STy t -> t -> PExpr expr env t
    Pair :: expr env t1 -> expr env t2 -> PExpr expr env (t1, t2)
    Nil :: PExpr expr env ()
    Prim :: Oper (t -> t') -> expr env t -> PExpr expr env t'
    Var :: V STy env t -> PExpr expr env t
    Let :: LHS STy t env env' -> expr env t -> expr env' t' -> PExpr expr env t'

newtype Expr env t = Expr (PExpr Expr env t)

data Oper t where
    Add :: STy t -> Oper ((t, t) -> t)
    Mul :: STy t -> Oper ((t, t) -> t)
    Round :: Oper (Float -> Int)

data PVal tenv env where  -- partial valuation
    VZ :: PVal tenv tenv
    VS :: PVal tenv env -> t -> PVal tenv (t ': env)

type Val = PVal '[]

data PTVal f tenv env where  -- partial tagged valuation
    TVZ :: PTVal f tenv tenv
    TVS :: PTVal f tenv env -> f t -> PTVal f tenv (t ': env)

type TVal f = PTVal f '[]

data NumDict t where
    NumDict :: Num t => NumDict t

data Exists f where
    Exists :: f t -> Exists f

data env :> env' =
    Weaken { (>:>) :: forall t. Idx env t -> Idx env' t }