--------------------------------------------------------------------------------

{-# LANGUAGE Safe #-}

module Copilot.Theorem.Kind2.AST where

--------------------------------------------------------------------------------

data File = File
  { File -> [PredDef]
filePreds     :: [PredDef]
  , File -> [Prop]
fileProps     :: [Prop] }

data Prop = Prop
  { Prop -> String
propName      :: String
  , Prop -> Term
propTerm      :: Term }

data PredDef = PredDef
  { PredDef -> String
predId        :: String
  , PredDef -> [StateVarDef]
predStateVars :: [StateVarDef]
  , PredDef -> Term
predInit      :: Term
  , PredDef -> Term
predTrans     :: Term }

data StateVarDef = StateVarDef
  { StateVarDef -> String
varId         :: String
  , StateVarDef -> Type
varType       :: Type
  , StateVarDef -> [StateVarFlag]
varFlags      :: [StateVarFlag] }

data Type = Int | Real | Bool

data StateVarFlag = FConst

data PredType = Init | Trans

data Term =
    ValueLiteral  String
  | PrimedStateVar String
  | StateVar       String
  | FunApp         String [Term]
  | PredApp        String PredType [Term]

--------------------------------------------------------------------------------