content: {-
  Copyright (c) 2015, Dan Rosén
  Copyright (c) 2016, Nick Smallbone
  
  All rights reserved.
  
  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions are met:
  
      * Redistributions of source code must retain the above copyright
        notice, this list of conditions and the following disclaimer.
  
      * Redistributions in binary form must reproduce the above
        copyright notice, this list of conditions and the following
        disclaimer in the documentation and/or other materials provided
        with the distribution.
  
      * Neither the name of the copyright holder nor the names of other
        contributors may be used to endorse or promote products derived
        from this software without specific prior written permission.
  
  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
  A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
  OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
  DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
  THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
  (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
  OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  -}
  -- File generated by the BNF Converter (bnfc 2.9.4).
  
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE PatternSynonyms #-}
  
  -- | The abstract syntax of language TIP.
  
  module TIP.AbsTIP where
  
  import Prelude (Integer, String)
  import qualified Prelude as C
    ( Eq, Ord, Show, Read
    , Int, Maybe(..)
    )
  import qualified Data.String
  
  data Start = Start [Decl]
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Decl
      = DeclareDatatype AttrSymbol Datatype
      | DeclareDatatypes [DatatypeName] [Datatype]
      | DeclareSort AttrSymbol Integer
      | DeclareConst AttrSymbol ConstType
      | DeclareFun AttrSymbol FunType
      | DefineFun FunDec Expr
      | DefineFunRec FunDec Expr
      | DefineFunsRec [BracketedFunDec] [Expr]
      | Formula Assertion [Attr] Expr
      | FormulaPar Assertion [Attr] Par Expr
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Assertion = Assert | Prove
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Par = Par [Symbol]
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data ConstType = ConstTypeMono Type | ConstTypePoly Par Type
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data InnerFunType = InnerFunType [Type] Type
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data FunType
      = FunTypeMono InnerFunType | FunTypePoly Par InnerFunType
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data InnerFunDec = InnerFunDec [Binding] Type
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data FunDec
      = FunDecMono AttrSymbol InnerFunDec
      | FunDecPoly AttrSymbol Par InnerFunDec
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data BracketedFunDec = BracketedFunDec FunDec
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data DatatypeName = DatatypeName AttrSymbol Integer
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data InnerDatatype = InnerDatatype [Constructor]
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Datatype
      = DatatypeMono InnerDatatype | DatatypePoly Par InnerDatatype
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Constructor = Constructor AttrSymbol [Binding]
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Binding = Binding Symbol Type
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data LetDecl = LetDecl Symbol Expr
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Type
      = TyVar Symbol
      | TyApp Symbol [Type]
      | ArrowTy [Type]
      | IntTy
      | RealTy
      | BoolTy
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Expr
      = Var PolySymbol
      | App Head [Expr]
      | Match Expr [Case]
      | Let [LetDecl] Expr
      | Binder Binder [Binding] Expr
      | Lit Lit
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Lit = LitInt Integer | LitNegInt Integer | LitTrue | LitFalse
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Binder = Lambda | Forall | Exists
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Case = Case Pattern Expr
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Pattern
      = Default | ConPat Symbol [Symbol] | SimplePat Symbol | LitPat Lit
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Head
      = Const PolySymbol
      | At
      | IfThenElse
      | And
      | Or
      | Not
      | Implies
      | Equal
      | Distinct
      | NumAdd
      | NumSub
      | NumMul
      | NumDiv
      | IntDiv
      | IntMod
      | NumGt
      | NumGe
      | NumLt
      | NumLe
      | NumWiden
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data PolySymbol = NoAs Symbol | As Symbol [Type]
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data AttrSymbol = AttrSymbol Symbol [Attr]
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Attr = NoValue Keyword | Value Keyword Symbol
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  data Symbol = Unquoted UnquotedSymbol | Quoted QuotedSymbol
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  newtype UnquotedSymbol = UnquotedSymbol ((C.Int, C.Int), String)
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  newtype QuotedSymbol = QuotedSymbol ((C.Int, C.Int), String)
    deriving (C.Eq, C.Ord, C.Show, C.Read)
  
  newtype Keyword = Keyword String
    deriving (C.Eq, C.Ord, C.Show, C.Read, 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 UnquotedSymbol where
    hasPosition (UnquotedSymbol (p, _)) = C.Just p
  
  instance HasPosition QuotedSymbol where
    hasPosition (QuotedSymbol (p, _)) = C.Just p
  
  