{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Language where

import AST
import ASTfunc


class    IsSTy t     where magicSTy :: STy t
instance IsSTy Int   where magicSTy = TInt
instance IsSTy Float where magicSTy = TFloat

class    IsTupTy t     where magicTupTy :: Tup STy t
-- Need to list all the scalar types to avoid overlapping instances
instance IsTupTy Int   where magicTupTy = T1 TInt
instance IsTupTy Float where magicTupTy = T1 TFloat
instance IsTupTy ()    where magicTupTy = T0
instance (IsTupTy t1, IsTupTy t2) => IsTupTy (t1, t2) where
    magicTupTy = T2 magicTupTy magicTupTy

con :: IsSTy t => t -> Expr env t
con = Expr . Const magicSTy

pair :: Expr env t1 -> Expr env t2 -> Expr env (t1, t2)
pair = (Expr .) . Pair

nil :: Expr env ()
nil = Expr Nil

add :: IsSTy t => Expr env t -> Expr env t -> Expr env t
add = ((Expr . Prim (Add magicSTy) . Expr) .) . Pair

mul :: IsSTy t => Expr env t -> Expr env t -> Expr env t
mul = ((Expr . Prim (Mul magicSTy) . Expr) .) . Pair

let_ :: IsTupTy t
     => Expr env t
     -> (forall env'. (forall t2. Expr env t2 -> Expr env' t2)
                   -> Expr env' t -> Expr env' t')
     -> Expr env t'
let_ rhs f
  | LetBound lhs vs <- lhsCopy magicTupTy
  = Expr (Let lhs rhs (f (weakenExpr (weakenWithLHS lhs)) (evars vs)))

fst_ :: Expr env (t, t') -> Expr env t
fst_ (Expr (Pair e1 _)) = e1
fst_ _ = error "fst_: explicit let-binding necessary"

snd_ :: Expr env (t, t') -> Expr env t'
snd_ (Expr (Pair _ e2)) = e2
snd_ _ = error "snd_: explicit let-binding necessary"