    {-# LANGUAGE Safe #-}

    -- | Abstract syntax tree of Kind2 files.
    module Copilot.Theorem.Kind2.AST where

    -- | A file is a sequence of predicates and propositions.
    data File = File
      { File -> [PredDef]
    filePreds     :: [PredDef]
      , File -> [Prop]
    fileProps     :: [Prop] }

    -- | A proposition is defined by a term.
    data Prop = Prop
      { Prop -> String
    propName      :: String
      , Prop -> Term
    propTerm      :: Term }

    -- | A predicate definition.
    data PredDef = PredDef
      { PredDef -> String
    predId        :: String         -- ^ Identifier for the predicate.
      , PredDef -> [StateVarDef]
    predStateVars :: [StateVarDef]  -- ^ Variables identifying the states in the
                                        -- underlying state transition system.
      , PredDef -> Term
    predInit      :: Term           -- ^ Predicate that holds for initial
                                        -- states.
      , PredDef -> Term
    predTrans     :: Term           -- ^ Predicate that holds for two states, if
                                        -- there is state transition between them.
      }

    -- | A definition of a state variable.
    data StateVarDef = StateVarDef
      { StateVarDef -> String
    varId         :: String           -- ^ Name of the variable.
      , StateVarDef -> Type
    varType       :: Type             -- ^ Type of the variable.
      , StateVarDef -> [StateVarFlag]
    varFlags      :: [StateVarFlag] } -- ^ Flags for the variable.

    -- | Types used in Kind2 files to represent Copilot types.
    --
    -- The Kind2 backend provides functions to, additionally, constrain the range
    -- of numeric values depending on their Copilot type ('Int8', 'Int16', etc.).
    data Type = Int | Real | Bool

    -- | Possible flags for a state variable.
    data StateVarFlag = FConst

    -- | Type of the predicate, either belonging to an initial state or a pair of
    -- states with a transition.
    data PredType = Init | Trans

    -- | Datatype to describe a term in the Kind language.
    data Term =
        ValueLiteral  String
      | PrimedStateVar String
      | StateVar       String
      | FunApp         String [Term]
      | PredApp        String PredType [Term]