content: -- File generated by the BNF Converter (bnfc 2.9.6).
  
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE DeriveTraversable #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE PatternSynonyms #-}
  
  -- | The abstract syntax of language Syntax.
  
  module Language.Rzk.Syntax.Abs where
  
  import Prelude (String)
  import qualified Prelude as C
    ( Eq, Ord, Show, Read
    , Functor, Foldable, Traversable
    , Int, Maybe(..)
    )
  import qualified Data.String
  
  import qualified Data.Data    as C (Data)
  import qualified GHC.Generics as C (Generic)
  
  type Module = Module' BNFC'Position
  data Module' a = Module a (LanguageDecl' a) [Command' a]
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type HoleIdent = HoleIdent' BNFC'Position
  data HoleIdent' a = HoleIdent a HoleIdentToken
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type VarIdent = VarIdent' BNFC'Position
  data VarIdent' a = VarIdent a VarIdentToken
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type LanguageDecl = LanguageDecl' BNFC'Position
  data LanguageDecl' a = LanguageDecl a (Language' a)
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type Language = Language' BNFC'Position
  data Language' a = Rzk1 a
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type Command = Command' BNFC'Position
  data Command' a
      = CommandSetOption a String String
      | CommandUnsetOption a String
      | CommandCheck a (Term' a) (Term' a)
      | CommandCompute a (Term' a)
      | CommandComputeWHNF a (Term' a)
      | CommandComputeNF a (Term' a)
      | CommandPostulate a (VarIdent' a) (DeclUsedVars' a) [Param' a] (Term' a)
      | CommandAssume a [VarIdent' a] (Term' a)
      | CommandSection a (SectionName' a)
      | CommandSectionEnd a (SectionName' a)
      | CommandDefine a (VarIdent' a) (DeclUsedVars' a) [Param' a] (Term' a) (Term' a)
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type DeclUsedVars = DeclUsedVars' BNFC'Position
  data DeclUsedVars' a = DeclUsedVars a [VarIdent' a]
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type SectionName = SectionName' BNFC'Position
  data SectionName' a
      = NoSectionName a | SomeSectionName a (VarIdent' a)
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type Pattern = Pattern' BNFC'Position
  data Pattern' a
      = PatternUnit a
      | PatternVar a (VarIdent' a)
      | PatternPair a (Pattern' a) (Pattern' a)
      | PatternTuple a (Pattern' a) (Pattern' a) [Pattern' a]
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type Param = Param' BNFC'Position
  data Param' a
      = ParamPattern a (Pattern' a)
      | ParamPatternType a [Pattern' a] (Term' a)
      | ParamPatternShape a [Pattern' a] (Term' a) (Term' a)
      | ParamPatternShapeDeprecated a (Pattern' a) (Term' a) (Term' a)
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type ParamDecl = ParamDecl' BNFC'Position
  data ParamDecl' a
      = ParamType a (Term' a)
      | ParamTermType a (Term' a) (Term' a)
      | ParamTermShape a (Term' a) (Term' a) (Term' a)
      | ParamTermTypeDeprecated a (Pattern' a) (Term' a)
      | ParamVarShapeDeprecated a (Pattern' a) (Term' a) (Term' a)
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type SigmaParam = SigmaParam' BNFC'Position
  data SigmaParam' a = SigmaParam a (Pattern' a) (Term' a)
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type Restriction = Restriction' BNFC'Position
  data Restriction' a
      = Restriction a (Term' a) (Term' a)
      | ASCII_Restriction a (Term' a) (Term' a)
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  type Term = Term' BNFC'Position
  data Term' a
      = Universe a
      | UniverseCube a
      | UniverseTope a
      | CubeUnit a
      | CubeUnitStar a
      | Cube2 a
      | Cube2_0 a
      | Cube2_1 a
      | CubeProduct a (Term' a) (Term' a)
      | TopeTop a
      | TopeBottom a
      | TopeEQ a (Term' a) (Term' a)
      | TopeLEQ a (Term' a) (Term' a)
      | TopeAnd a (Term' a) (Term' a)
      | TopeOr a (Term' a) (Term' a)
      | RecBottom a
      | RecOr a [Restriction' a]
      | RecOrDeprecated a (Term' a) (Term' a) (Term' a) (Term' a)
      | TypeFun a (ParamDecl' a) (Term' a)
      | TypeSigma a (Pattern' a) (Term' a) (Term' a)
      | TypeSigmaTuple a (SigmaParam' a) [SigmaParam' a] (Term' a)
      | TypeUnit a
      | TypeId a (Term' a) (Term' a) (Term' a)
      | TypeIdSimple a (Term' a) (Term' a)
      | TypeRestricted a (Term' a) [Restriction' a]
      | TypeExtensionDeprecated a (ParamDecl' a) (Term' a)
      | App a (Term' a) (Term' a)
      | Lambda a [Param' a] (Term' a)
      | Pair a (Term' a) (Term' a)
      | Tuple a (Term' a) (Term' a) [Term' a]
      | First a (Term' a)
      | Second a (Term' a)
      | Unit a
      | Refl a
      | ReflTerm a (Term' a)
      | ReflTermType a (Term' a) (Term' a)
      | IdJ a (Term' a) (Term' a) (Term' a) (Term' a) (Term' a) (Term' a)
      | Hole a (HoleIdent' a)
      | Var a (VarIdent' a)
      | TypeAsc a (Term' a) (Term' a)
      | ASCII_CubeUnitStar a
      | ASCII_Cube2_0 a
      | ASCII_Cube2_1 a
      | ASCII_TopeTop a
      | ASCII_TopeBottom a
      | ASCII_TopeEQ a (Term' a) (Term' a)
      | ASCII_TopeLEQ a (Term' a) (Term' a)
      | ASCII_TopeAnd a (Term' a) (Term' a)
      | ASCII_TopeOr a (Term' a) (Term' a)
      | ASCII_TypeFun a (ParamDecl' a) (Term' a)
      | ASCII_TypeSigma a (Pattern' a) (Term' a) (Term' a)
      | ASCII_TypeSigmaTuple a (SigmaParam' a) [SigmaParam' a] (Term' a)
      | ASCII_Lambda a [Param' a] (Term' a)
      | ASCII_TypeExtensionDeprecated a (ParamDecl' a) (Term' a)
      | ASCII_First a (Term' a)
      | ASCII_Second a (Term' a)
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic)
  
  commandPostulateNoParams :: a -> VarIdent' a -> DeclUsedVars' a -> Term' a -> Command' a
  commandPostulateNoParams = \ _a x vars ty -> CommandPostulate _a x vars [] ty
  
  commandVariable :: a -> VarIdent' a -> Term' a -> Command' a
  commandVariable = \ _a name term -> CommandAssume _a [name] term
  
  commandVariables :: a -> [VarIdent' a] -> Term' a -> Command' a
  commandVariables = \ _a names term -> CommandAssume _a names term
  
  commandDefineNoParams :: a -> VarIdent' a -> DeclUsedVars' a -> Term' a -> Term' a -> Command' a
  commandDefineNoParams = \ _a x vars ty term -> CommandDefine _a x vars [] ty term
  
  commandDef :: a -> VarIdent' a -> DeclUsedVars' a -> [Param' a] -> Term' a -> Term' a -> Command' a
  commandDef = \ _a x vars params ty term -> CommandDefine _a x vars params ty term
  
  commandDefNoParams :: a -> VarIdent' a -> DeclUsedVars' a -> Term' a -> Term' a -> Command' a
  commandDefNoParams = \ _a x vars ty term -> CommandDefine _a x vars [] ty term
  
  noDeclUsedVars :: a -> DeclUsedVars' a
  noDeclUsedVars = \ _a -> DeclUsedVars _a []
  
  paramVarShapeDeprecated :: a -> Pattern' a -> Term' a -> Term' a -> ParamDecl' a
  paramVarShapeDeprecated = \ _a pat cube tope -> ParamVarShapeDeprecated _a pat cube tope
  
  ascii_CubeProduct :: a -> Term' a -> Term' a -> Term' a
  ascii_CubeProduct = \ _a l r -> CubeProduct _a l r
  
  unicode_TypeSigmaAlt :: a -> Pattern' a -> Term' a -> Term' a -> Term' a
  unicode_TypeSigmaAlt = \ _a pat fst snd -> TypeSigma _a pat fst snd
  
  unicode_TypeSigmaTupleAlt :: a -> SigmaParam' a -> [SigmaParam' a] -> Term' a -> Term' a
  unicode_TypeSigmaTupleAlt = \ _a par pars t -> TypeSigmaTuple _a par pars t
  
  newtype VarIdentToken = VarIdentToken String
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Generic, Data.String.IsString)
  
  newtype HoleIdentToken = HoleIdentToken String
    deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Generic, Data.String.IsString)
  
  -- | 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 HoleIdent where
    hasPosition = \case
      HoleIdent p _ -> p
  
  instance HasPosition VarIdent where
    hasPosition = \case
      VarIdent p _ -> p
  
  instance HasPosition LanguageDecl where
    hasPosition = \case
      LanguageDecl p _ -> p
  
  instance HasPosition Language where
    hasPosition = \case
      Rzk1 p -> p
  
  instance HasPosition Command where
    hasPosition = \case
      CommandSetOption p _ _ -> p
      CommandUnsetOption p _ -> p
      CommandCheck p _ _ -> p
      CommandCompute p _ -> p
      CommandComputeWHNF p _ -> p
      CommandComputeNF p _ -> p
      CommandPostulate p _ _ _ _ -> p
      CommandAssume p _ _ -> p
      CommandSection p _ -> p
      CommandSectionEnd p _ -> p
      CommandDefine p _ _ _ _ _ -> p
  
  instance HasPosition DeclUsedVars where
    hasPosition = \case
      DeclUsedVars p _ -> p
  
  instance HasPosition SectionName where
    hasPosition = \case
      NoSectionName p -> p
      SomeSectionName p _ -> p
  
  instance HasPosition Pattern where
    hasPosition = \case
      PatternUnit p -> p
      PatternVar p _ -> p
      PatternPair p _ _ -> p
      PatternTuple p _ _ _ -> p
  
  instance HasPosition Param where
    hasPosition = \case
      ParamPattern p _ -> p
      ParamPatternType p _ _ -> p
      ParamPatternShape p _ _ _ -> p
      ParamPatternShapeDeprecated p _ _ _ -> p
  
  instance HasPosition ParamDecl where
    hasPosition = \case
      ParamType p _ -> p
      ParamTermType p _ _ -> p
      ParamTermShape p _ _ _ -> p
      ParamTermTypeDeprecated p _ _ -> p
      ParamVarShapeDeprecated p _ _ _ -> p
  
  instance HasPosition SigmaParam where
    hasPosition = \case
      SigmaParam p _ _ -> p
  
  instance HasPosition Restriction where
    hasPosition = \case
      Restriction p _ _ -> p
      ASCII_Restriction p _ _ -> p
  
  instance HasPosition Term where
    hasPosition = \case
      Universe p -> p
      UniverseCube p -> p
      UniverseTope p -> p
      CubeUnit p -> p
      CubeUnitStar p -> p
      Cube2 p -> p
      Cube2_0 p -> p
      Cube2_1 p -> p
      CubeProduct p _ _ -> p
      TopeTop p -> p
      TopeBottom p -> p
      TopeEQ p _ _ -> p
      TopeLEQ p _ _ -> p
      TopeAnd p _ _ -> p
      TopeOr p _ _ -> p
      RecBottom p -> p
      RecOr p _ -> p
      RecOrDeprecated p _ _ _ _ -> p
      TypeFun p _ _ -> p
      TypeSigma p _ _ _ -> p
      TypeSigmaTuple p _ _ _ -> p
      TypeUnit p -> p
      TypeId p _ _ _ -> p
      TypeIdSimple p _ _ -> p
      TypeRestricted p _ _ -> p
      TypeExtensionDeprecated p _ _ -> p
      App p _ _ -> p
      Lambda p _ _ -> p
      Pair p _ _ -> p
      Tuple p _ _ _ -> p
      First p _ -> p
      Second p _ -> p
      Unit p -> p
      Refl p -> p
      ReflTerm p _ -> p
      ReflTermType p _ _ -> p
      IdJ p _ _ _ _ _ _ -> p
      Hole p _ -> p
      Var p _ -> p
      TypeAsc p _ _ -> p
      ASCII_CubeUnitStar p -> p
      ASCII_Cube2_0 p -> p
      ASCII_Cube2_1 p -> p
      ASCII_TopeTop p -> p
      ASCII_TopeBottom p -> p
      ASCII_TopeEQ p _ _ -> p
      ASCII_TopeLEQ p _ _ -> p
      ASCII_TopeAnd p _ _ -> p
      ASCII_TopeOr p _ _ -> p
      ASCII_TypeFun p _ _ -> p
      ASCII_TypeSigma p _ _ _ -> p
      ASCII_TypeSigmaTuple p _ _ _ -> p
      ASCII_Lambda p _ _ -> p
      ASCII_TypeExtensionDeprecated p _ _ -> p
      ASCII_First p _ -> p
      ASCII_Second p _ -> p
  
  