{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
module Presyntax.Presyntax where

import Data.Aeson (ToJSON)
import Data.Text (Text)
import Data.Data

import GHC.Generics (Generic)

data Plicity
  = Im | Ex
  deriving (Eq, Show, Ord, Data)

data Expr
  = Var Text

  | App Plicity Expr Expr
  | Pi  Plicity Text Expr Expr
  | Lam Plicity Text Expr

  | Sigma Text Expr Expr
  | Pair Expr Expr
  | Proj1 Expr
  | Proj2 Expr

  | LamSystem [(Condition, Expr)]
  | LamCase [(Pattern, Expr)]
  | Let [LetItem] Expr

  | Span Expr Posn Posn
  deriving (Eq, Show, Ord)

data LetItem
  = LetDecl { leIName :: Text, leIVal :: Expr }
  | LetBind { leIName :: Text, leIVal :: Expr }
  deriving (Eq, Show, Ord)

data Condition
  = Condition { condF :: Formula, condV :: Maybe Text }
  deriving (Eq, Show, Ord)

data Formula
  = FIs1 Text
  | FIs0 Text
  | FAnd Formula Formula
  | FOr  Formula Formula
  | FTop
  | FBot
  deriving (Eq, Show, Ord)

data Pattern
  = PCon Text [Text]
  | PCap Text
  deriving (Eq, Show, Ord)

data Statement
  = Decl    [Text] Expr
  | Defn    Text Expr
  | Builtin Text Text

  | Postulate [(Text, Expr)]

  | ReplNf Expr -- REPL eval
  | ReplTy Expr -- REPL :t

  | Data Text [(Text, Plicity, Expr)] Expr [(Posn, Posn, Constructor)]

  | SpanSt Statement Posn Posn
  deriving (Eq, Show, Ord)

data Constructor
  = Point Text Expr
  | Path Text [Text] Expr [(Formula, Expr)]
  deriving (Eq, Show, Ord)

data Posn
  = Posn { posnLine :: {-# UNPACK #-} !Int
         , posnColm :: {-# UNPACK #-} !Int
         }
  deriving (Eq, Show, Ord, Generic, ToJSON)