-- 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