-- Haskel data types for the abstract syntax.
-- Generated by the BNF converter.

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternSynonyms #-}

-- | The abstract syntax of language Cubicaltt.

module AbsCubicaltt where

import qualified Prelude as T (String)
import qualified Prelude as C (Eq, Ord, Show, Read, Int, Maybe(..))

import Data.String

data Module
    = Module AIdent [Imp] [Decl]
    -- ^ Module ::= "module" AIdent "where" "{" Imp Decl "}"
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data Imp
    = Import AIdent
    -- ^ Imp ::= "import" AIdent
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data Decl
    = DeclData AIdent [Tele] [Label]
    -- ^ Decl ::= "data" AIdent Tele "=" Label
    | DeclDef AIdent [Tele] Exp ExpWhere
    -- ^ Decl ::= AIdent Tele ":" Exp "=" ExpWhere
    | DeclHData AIdent [Tele] [Label]
    -- ^ Decl ::= "hdata" AIdent Tele "=" Label
    | DeclMutual [Decl]
    -- ^ Decl ::= "mutual" "{" Decl "}"
    | DeclOpaque AIdent
    -- ^ Decl ::= "opaque" AIdent
    | DeclSplit AIdent [Tele] Exp [Branch]
    -- ^ Decl ::= AIdent Tele ":" Exp "=" "split" "{" Branch "}"
    | DeclTransparent AIdent
    -- ^ Decl ::= "transparent" AIdent
    | DeclTransparentAll
    -- ^ Decl ::= "transparent_all"
    | DeclUndef AIdent [Tele] Exp
    -- ^ Decl ::= AIdent Tele ":" Exp "=" "undefined"
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data ExpWhere
    = NoWhere Exp
    -- ^ ExpWhere ::= Exp
    | Where Exp [Decl]
    -- ^ ExpWhere ::= Exp "where" "{" Decl "}"
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data Exp
    = App Exp Exp
    -- ^ Exp ::= Exp2 Exp3
    | AppFormula Exp Formula
    -- ^ Exp ::= Exp2 "@" Formula
    | Comp Exp Exp System
    -- ^ Exp ::= "comp" Exp4 Exp4 System
    | Fill Exp Exp System
    -- ^ Exp ::= "fill" Exp4 Exp4 System
    | Fst Exp
    -- ^ Exp ::= Exp4 ".1"
    | Fun Exp Exp
    -- ^ Exp ::= Exp2 "->" Exp1
    | Glue Exp System
    -- ^ Exp ::= "Glue" Exp4 System
    | GlueElem Exp System
    -- ^ Exp ::= "glue" Exp4 System
    | HComp Exp Exp System
    -- ^ Exp ::= "hComp" Exp4 Exp4 System
    | Hole HoleIdent
    -- ^ Exp ::= HoleIdent
    | Id Exp Exp Exp
    -- ^ Exp ::= "Id" Exp4 Exp4 Exp3
    | IdJ Exp Exp Exp Exp Exp Exp
    -- ^ Exp ::= "idJ" Exp4 Exp4 Exp4 Exp4 Exp4 Exp4
    | IdPair Exp System
    -- ^ Exp ::= "idC" Exp4 System
    | Lam [PTele] Exp
    -- ^ Exp ::= "\\" PTele "->" Exp
    | Let [Decl] Exp
    -- ^ Exp ::= "let" "{" Decl "}" "in" Exp
    | PCon AIdent Exp
    -- ^ Exp ::= AIdent "{" Exp "}"
    | PLam [AIdent] Exp
    -- ^ Exp ::= "<" AIdent ">" Exp
    | Pair Exp [Exp]
    -- ^ Exp ::= "(" Exp "," Exp ")"
    | PathP Exp Exp Exp
    -- ^ Exp ::= "PathP" Exp4 Exp4 Exp4
    | Pi [PTele] Exp
    -- ^ Exp ::= PTele "->" Exp1
    | Sigma [PTele] Exp
    -- ^ Exp ::= PTele "*" Exp1
    | Snd Exp
    -- ^ Exp ::= Exp4 ".2"
    | Split Exp [Branch]
    -- ^ Exp ::= "split@" Exp "with" "{" Branch "}"
    | Trans Exp Exp
    -- ^ Exp ::= "transport" Exp4 Exp4
    | U
    -- ^ Exp ::= "U"
    | UnGlueElem Exp System
    -- ^ Exp ::= "unglue" Exp4 System
    | Var AIdent
    -- ^ Exp ::= AIdent
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data Dir
    = Dir0
    -- ^ Dir ::= "0"
    | Dir1
    -- ^ Dir ::= "1"
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data System
    = System [Side]
    -- ^ System ::= "[" Side "]"
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data Face
    = Face AIdent Dir
    -- ^ Face ::= "(" AIdent "=" Dir ")"
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data Side
    = Side [Face] Exp
    -- ^ Side ::= Face "->" Exp
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data Formula
    = Atom AIdent
    -- ^ Formula ::= AIdent
    | Conj Formula CIdent Formula
    -- ^ Formula ::= Formula1 CIdent Formula2
    | Dir Dir
    -- ^ Formula ::= Dir
    | Disj Formula Formula
    -- ^ Formula ::= Formula "\\/" Formula1
    | Neg Formula
    -- ^ Formula ::= "-" Formula2
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data Branch
    = OBranch AIdent [AIdent] ExpWhere
    -- ^ Branch ::= AIdent AIdent "->" ExpWhere
    | PBranch AIdent [AIdent] [AIdent] ExpWhere
    -- ^ Branch ::= AIdent AIdent "@" AIdent "->" ExpWhere
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data Label
    = OLabel AIdent [Tele]
    -- ^ Label ::= AIdent Tele
    | PLabel AIdent [Tele] [AIdent] System
    -- ^ Label ::= AIdent Tele "<" AIdent ">" System
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data Tele
    = Tele AIdent [AIdent] Exp
    -- ^ Tele ::= "(" AIdent AIdent ":" Exp ")"
  deriving (C.Eq, C.Ord, C.Show, C.Read)

data PTele
    = PTele Exp Exp
    -- ^ PTele ::= "(" Exp ":" Exp ")"
  deriving (C.Eq, C.Ord, C.Show, C.Read)

newtype AIdent
    = AIdent ((C.Int, C.Int), T.String)
  deriving (C.Eq, C.Ord, C.Show, C.Read)

newtype CIdent
    = CIdent T.String
  deriving (C.Eq, C.Ord, C.Show, C.Read, Data.String.IsString)

newtype HoleIdent
    = HoleIdent ((C.Int, C.Int), T.String)
  deriving (C.Eq, C.Ord, C.Show, C.Read)

-- | Start position (line, column) of something.

type BNFC'Position = C.Maybe (C.Int, C.Int)

pattern BNFC'NoPosition :: BNFC'Position
pattern BNFC'NoPosition = C.Nothing

pattern BNFC'Position :: C.Int -> C.Int -> BNFC'Position
pattern BNFC'Position line col = C.Just (line, col)

-- | Get the start position of something.

class HasPosition a where
  hasPosition :: a -> BNFC'Position

instance HasPosition AIdent where
  hasPosition (AIdent (p, _)) = C.Just p

instance HasPosition HoleIdent where
  hasPosition (HoleIdent (p, _)) = C.Just p