{-# 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]