-- Agda definition of C-- abstract syntax trees
-- and Haskell bindings to the ones generated by the parser.

module V1.AST where

open import Library

{-# FOREIGN GHC import qualified Data.Text #-}
{-# FOREIGN GHC import While.Abs #-}
{-# FOREIGN GHC import While.Print #-}

data Type : Set where
  bool int : Type

{-# COMPILE GHC Type = data Type
  ( TBool
  | TInt
  ) #-}

data Boolean : Set where
  true false : Boolean

{-# COMPILE GHC Boolean = data Boolean (BTrue | BFalse) #-}

data Exp : Set where
  eInt   : (i : ℤ)          → Exp
  eBool  : (b : Boolean)    → Exp
  ePlus  : (e e' : Exp)     → Exp
  eGt    : (e e' : Exp)     → Exp
  eAnd   : (e e' : Exp)     → Exp
  eCond  : (e e' e'' : Exp) → Exp

{-# COMPILE GHC Exp = data Exp
  ( EInt
  | EBool
  | EPlus
  | EGt
  | EAnd
  | ECond
  ) #-}

record Program : Set where
  constructor program
  field
    theMain  : Exp
open Program public

{-# COMPILE GHC Program = data Program (Prg) #-}

-- Pretty printer

private
  postulate
    printType    : Type    → String
    printBoolean : Boolean → String
    printExp     : Exp     → String
    printProgram : Program → String

{-# COMPILE GHC printType    = \ t -> Data.Text.pack (printTree (t :: Type))    #-}
{-# COMPILE GHC printBoolean = \ b -> Data.Text.pack (printTree (b :: Boolean)) #-}
{-# COMPILE GHC printExp     = \ e -> Data.Text.pack (printTree (e :: Exp))     #-}
{-# COMPILE GHC printProgram = \ p -> Data.Text.pack (printTree (p :: Program)) #-}

instance
  PrintType : Print Type
  print {{PrintType}} = printType

  PrintBoolean : Print Boolean
  print {{PrintBoolean}} = printBoolean

  PrintExp : Print Exp
  print {{PrintExp}} = printExp

  PrintProgram : Print Program
  print {{PrintProgram}} = printProgram

-- Eq instance

instance
  EqType : Eq Type
  _≟_ {{EqType}} = λ where
    bool bool → yes refl
    bool int  → no λ ()
    int  bool → no λ ()
    int  int  → yes refl