{-# LANGUAGE MultiParamTypeClasses,TemplateHaskell,ScopedTypeVariables,FlexibleInstances,FlexibleContexts,UndecidableInstances,TypeSynonymInstances #-}

module MProver.Syntax where

import Data.Maybe
import Data.List

import Unbound.LocallyNameless

------------------------------------------
-- Abstract syntax for MProver programs --
------------------------------------------
type Identifier = String

data Program = Program Identifier (TRec [Decl])
             deriving Show

data Decl = TypeDecl Identifier (Embed (Bind [Name Ty] Ty))
          | DataDecl Identifier (Embed (Bind [Name Ty] [ConstrDecl]))
          | ExprDecl (Maybe (Embed Ty)) (Name Expr) (Embed Expr)
          | ProofDecl (Embed Formula) (Name Proof) (Embed Proof)
          deriving Show

type ProofBind = Bind [Pat] Proof

data Expr = Lambda (Bind (Name Expr) Expr)
          | Var (Name Expr)
          | Ctor Identifier
          | Literal Lit
          | Let (Bind (Rec [(Name Expr,Embed Expr)]) Expr)
          | Case Expr [Alt]
          | App Expr Expr
          | Bottom
          deriving Show

data Lit = LitInteger Integer
         | LitChar Char
         | LitFrac Double
         deriving (Ord,Eq,Show)

type Alt = Bind Pat Expr

data Ty = TyArrow Ty Ty
        | TyApp Ty Ty
        | TyCon Identifier
        | TyVar (Name Ty)
        deriving Show
                 
data Proof = ForallIExpr Ty (Bind (Name Expr) Proof)               -- Foralli x::t, e
           | ProofImpl Formula (Bind (Name Proof) Proof)           -- Assuming p:::fo, pr -- (FIXME: don't like that notation)
           | ProofVar (Name Proof)                                 -- x
           | ProofAppExpr Proof Expr                               -- p [e]
           | ProofAppProof Proof Proof                             -- p1 p2
           | ProofBisim Identifier [Proof]                         -- Ctor p1 p2 .. pn
           | Eval                                                  -- eval
           | Trans Proof Proof                                     -- trans p1 p2
           | Subst (Bind (Name Expr) (Proof,Expr))                 -- subst x by p in e
           | Symm Proof                                            -- symm p
           | ProofCase Expr Formula (Bind (Name Proof) [ProofAlt]) -- case e proving fo by x of { pa1; pa2; pa3 }
           | ProofAnno Proof Formula                               -- proof ::: formula
           deriving Show

type ProofAlt = Bind Pat Proof

data Formula = ForallExpr Ty (Bind (Name Expr) Formula)
             | ForallProof Formula Formula
             | FormulaEq Expr Expr
             deriving Show

data Pat = PatVar (Name Expr)
         | PatCtor Identifier
         | PatLiteral Lit
         | PatWildcard
         | PatApp Identifier [Pat]
         | PatBottom
         deriving Show

patToExpr :: Pat -> Maybe Expr
patToExpr (PatVar x)     = Just $ Var x
patToExpr (PatCtor x)    = Just $ Ctor x
patToExpr (PatLiteral l) = Just $ Literal l
patToExpr PatWildcard    = Nothing
patToExpr (PatApp x ps)  = do
                             es <- mapM patToExpr ps
                             Just $ foldl App (Ctor x) es
patToExpr PatBottom      = Just Bottom

data ConstrDecl = ConstrDecl Identifier [Ty] deriving Show

$(derive [''Decl,''Expr,''Lit,''Pat,''Ty,''ConstrDecl,''Proof,''Formula])

--instance Alpha Program where
instance Alpha Decl where
instance Alpha Expr where
instance Alpha Ty where
instance Alpha Proof where
instance Alpha Formula where
instance Alpha Pat where
instance Alpha ConstrDecl where

-- Not sure why this is needed, but Unbound crashes with something about
-- "compareR1 does not support Integer1"
instance Alpha Lit where
  acompare' _ = compare

instance Subst Expr Expr where
  isvar (Var n) = Just (SubstName n)
  isvar _       = Nothing

instance Subst Expr Formula where
instance Subst Expr Ty where
instance Subst Expr Lit where
instance Subst Expr Pat where