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

{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# 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
  , Functor
  , Foldable
  , Traversable
  , Int, Maybe(..) )

import Data.String

type Module = Module' BNFC'Position
data Module' a
    = Module a AIdent [Imp' a] [Decl' a]
    -- ^ Module ::= "module" AIdent "where" "{" Imp Decl "}"
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

type Imp = Imp' BNFC'Position
data Imp' a
    = Import a AIdent
    -- ^ Imp ::= "import" AIdent
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

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

type ExpWhere = ExpWhere' BNFC'Position
data ExpWhere' a
    = NoWhere a (Exp' a)
    -- ^ ExpWhere ::= Exp
    | Where a (Exp' a) [Decl' a]
    -- ^ ExpWhere ::= Exp "where" "{" Decl "}"
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

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

type Dir = Dir' BNFC'Position
data Dir' a
    = Dir0 a
    -- ^ Dir ::= "0"
    | Dir1 a
    -- ^ Dir ::= "1"
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

type System = System' BNFC'Position
data System' a
    = System a [Side' a]
    -- ^ System ::= "[" Side "]"
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

type Face = Face' BNFC'Position
data Face' a
    = Face a AIdent (Dir' a)
    -- ^ Face ::= "(" AIdent "=" Dir ")"
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

type Side = Side' BNFC'Position
data Side' a
    = Side a [Face' a] (Exp' a)
    -- ^ Side ::= Face "->" Exp
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

type Formula = Formula' BNFC'Position
data Formula' a
    = Atom a AIdent
    -- ^ Formula ::= AIdent
    | Conj a (Formula' a) CIdent (Formula' a)
    -- ^ Formula ::= Formula1 CIdent Formula2
    | Dir a (Dir' a)
    -- ^ Formula ::= Dir
    | Disj a (Formula' a) (Formula' a)
    -- ^ Formula ::= Formula "\\/" Formula1
    | Neg a (Formula' a)
    -- ^ Formula ::= "-" Formula2
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

type Branch = Branch' BNFC'Position
data Branch' a
    = OBranch a AIdent [AIdent] (ExpWhere' a)
    -- ^ Branch ::= AIdent AIdent "->" ExpWhere
    | PBranch a AIdent [AIdent] [AIdent] (ExpWhere' a)
    -- ^ Branch ::= AIdent AIdent "@" AIdent "->" ExpWhere
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

type Label = Label' BNFC'Position
data Label' a
    = OLabel a AIdent [Tele' a]
    -- ^ Label ::= AIdent Tele
    | PLabel a AIdent [Tele' a] [AIdent] (System' a)
    -- ^ Label ::= AIdent Tele "<" AIdent ">" System
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

type Tele = Tele' BNFC'Position
data Tele' a
    = Tele a AIdent [AIdent] (Exp' a)
    -- ^ Tele ::= "(" AIdent AIdent ":" Exp ")"
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

type PTele = PTele' BNFC'Position
data PTele' a
    = PTele a (Exp' a) (Exp' a)
    -- ^ PTele ::= "(" Exp ":" Exp ")"
  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable)

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 Module where
  hasPosition = \case
    Module p _ _ _ -> p

instance HasPosition Imp where
  hasPosition = \case
    Import p _ -> p

instance HasPosition Decl where
  hasPosition = \case
    DeclData p _ _ _ -> p
    DeclDef p _ _ _ _ -> p
    DeclHData p _ _ _ -> p
    DeclMutual p _ -> p
    DeclOpaque p _ -> p
    DeclSplit p _ _ _ _ -> p
    DeclTransparent p _ -> p
    DeclTransparentAll p -> p
    DeclUndef p _ _ _ -> p

instance HasPosition ExpWhere where
  hasPosition = \case
    NoWhere p _ -> p
    Where p _ _ -> p

instance HasPosition Exp where
  hasPosition = \case
    App p _ _ -> p
    AppFormula p _ _ -> p
    Comp p _ _ _ -> p
    Fill p _ _ _ -> p
    Fst p _ -> p
    Fun p _ _ -> p
    Glue p _ _ -> p
    GlueElem p _ _ -> p
    HComp p _ _ _ -> p
    Hole p _ -> p
    Id p _ _ _ -> p
    IdJ p _ _ _ _ _ _ -> p
    IdPair p _ _ -> p
    Lam p _ _ -> p
    Let p _ _ -> p
    PCon p _ _ -> p
    PLam p _ _ -> p
    Pair p _ _ -> p
    PathP p _ _ _ -> p
    Pi p _ _ -> p
    Sigma p _ _ -> p
    Snd p _ -> p
    Split p _ _ -> p
    Trans p _ _ -> p
    U p -> p
    UnGlueElem p _ _ -> p
    Var p _ -> p

instance HasPosition Dir where
  hasPosition = \case
    Dir0 p -> p
    Dir1 p -> p

instance HasPosition System where
  hasPosition = \case
    System p _ -> p

instance HasPosition Face where
  hasPosition = \case
    Face p _ _ -> p

instance HasPosition Side where
  hasPosition = \case
    Side p _ _ -> p

instance HasPosition Formula where
  hasPosition = \case
    Atom p _ -> p
    Conj p _ _ _ -> p
    Dir p _ -> p
    Disj p _ _ -> p
    Neg p _ -> p

instance HasPosition Branch where
  hasPosition = \case
    OBranch p _ _ _ -> p
    PBranch p _ _ _ _ -> p

instance HasPosition Label where
  hasPosition = \case
    OLabel p _ _ -> p
    PLabel p _ _ _ _ -> p

instance HasPosition Tele where
  hasPosition = \case
    Tele p _ _ _ -> p

instance HasPosition PTele where
  hasPosition = \case
    PTele p _ _ -> p

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

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