content: {-# OPTIONS -Wall                #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE DataKinds           #-}
  {-# LANGUAGE GADTs               #-}
  {-# LANGUAGE TypeOperators       #-}
  {-# LANGUAGE PolyKinds           #-}
  
  module ImperativeDSL where
  
  import GHC.TypeLits
  import Data.Proxy
  
  import NamedVariables
  
  ------------------------------------------------
  -- Types
  ------------------------------------------------
  
  -- Our programs are ascribed types. They are reflected
  -- as real Haskell types, however we impose that they
  -- should be "known" to us i.e. that we get a singleton
  -- representing them.
  
  data Type (a :: *) = KnownType a => Of
  
  data SType (a :: *) where
    SBool :: SType Bool
    SInt  :: SType Int
  
  instance Show (SType a) where
    show sty = case sty of
      SBool -> "Bool"
      SInt  -> "Int"
  
  class Show a => KnownType a where sType :: Proxy a -> SType a
  instance KnownType Bool where sType _ = SBool
  instance KnownType Int  where sType _ = SInt
  
  instance KnownType a => Show (Type a) where
    show Of = show $ sType (Proxy :: Proxy a)
  
  ------------------------------------------------
  -- Expressions
  ------------------------------------------------
  
  -- Expressions are fairly basic. We allow literals as long
  -- they are of a known type.
  
  data Exp (g :: [(Symbol,*)]) (t :: *) where
    EVar :: ScopedSymbol s g a -> Exp g a
    ELit :: KnownType s => s -> Exp g s
    EAdd :: Exp g Int -> Exp g Int -> Exp g Int
    ENot :: Exp g Bool -> Exp g Bool
  
  instance Show (Exp g t) where
    show e = case e of
      EVar v   -> "Var " ++ show v
      ELit b   -> show b
      EAdd l r -> concat [ "(", show l, ") + (", show r, ")" ]
      ENot b   -> concat [ "¬ (", show b, ")" ]
  
  ------------------------------------------------
  -- Statements
  ------------------------------------------------
  
  -- A `Statement` can be seen as a Scope-transformer: it takes
  -- the current scope and returns an updated one.
  --   In the case of `Declare`, the returned scope has been
  -- extended with the newly declared variable (and its associated
  -- type).
  --   In the case of `Assign`, the scope is left unchanged.
  
  data Statement (g :: [(Symbol, *)]) (h :: [(Symbol,*)]) where
    Declare :: Name s -> Type a -> Statement g ('(s, a) ': g)
    Assign  :: ScopedSymbol s g a -> Exp g a -> Statement g g
    Print   :: KnownType a => Exp g a -> Statement g g
  
  -- `Statements` are a list of scope-aligned `Statement`s.
  
  infixr 5 :>
  data Statements (g :: [(Symbol, *)]) (h :: [(Symbol,*)]) where
    Done :: Statements g g
    (:>) :: Statement g h -> Statements h i -> Statements g i
  
  instance Show (Statement g h) where
    show (Declare v@Var t@Of) = concat [ "new ", show v, " :: ", show t ]
    show (Assign v e)         = concat [ show v, " := ", show e ]
    show (Print e)            = concat [ "print (", show e, ")" ]
  
  instance Show (Statements g h) where
    show Done         = ""
    show (st :> Done) = show st
    show (st :> rest) = concat [ show st, "\n", show rest ]
  
  ------------------------------------------------
  -- Programs
  ------------------------------------------------
  
  -- A Program is a sequence of `Statements` starting in the
  -- empty scope.
  
  data Program = forall h. Program (Statements '[] h)
  
  instance Show Program where show (Program sts) = show sts
  