    {-# LANGUAGE Safe #-}

    -- | Abstract syntax tree of Kind2 native input files.
    --
    -- This represents the native transition system input format supported by
    -- Kind2 1.0 and newer (@--input_format native@), in which a file is a
    -- sequence of @define-node@ forms, each declaring a state transition system
    -- by means of an initial state predicate and a transition relation predicate.
    -- The last node defined in a file is the top system analyzed by Kind2, and
    -- the properties to check are attached to it.
    --
    -- The native input format is largely undocumented, and Kind2's user
    -- documentation only covers its Lustre frontend. The best available
    -- references for the native format are the parser in the Kind2 sources
    -- ([nativeInput.ml]
    -- (https://github.com/kind2-mc/kind2/blob/v3.0.0/src/nativeInput.ml)),
    -- which includes a sketch of the grammar in a comment near the end of the
    -- file) and the example file
    -- [two_counters.kind2]
    -- (https://github.com/kind2-mc/kind2/blob/develop/examples/two_counters.kind2).
    module Copilot.Theorem.Kind2.AST where

    -- | A file is a sequence of node definitions, together with a distinguished
    -- top node and a series of propositions about the top node.
    --
    -- Kind2 analyzes the last node defined in a file as the top system, so the
    -- top node is always printed after all the other nodes.
    data File = File
      { File -> [Node]
    fileNodes   :: [Node]  -- ^ Nodes other than the top node, in dependency
                               --   order (a node may only refer to nodes defined
                               --   before it).
      , File -> Node
    fileTopNode :: Node    -- ^ The top node, which the propositions are
                               --   attached to.
      , File -> [Prop]
    fileProps   :: [Prop]  -- ^ Propositions about the top node.
      }

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

    -- | A node definition.
    data Node = Node
      { Node -> String
    nodeId        :: String         -- ^ Identifier for the node.
      , Node -> [StateVarDef]
    nodeStateVars :: [StateVarDef]  -- ^ Variables identifying the states in
                                        -- the underlying state transition system.
      , Node -> Term
    nodeInit      :: Term           -- ^ Predicate that holds for initial
                                        -- states.
      , Node -> Term
    nodeTrans     :: Term           -- ^ Predicate that holds for two states,
                                        -- if there is a 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]