{-# LANGUAGE Safe #-}
module Copilot.Theorem.Kind2.AST where
data File = File
{ filePreds :: [PredDef]
, fileProps :: [Prop] }
data Prop = Prop
{ propName :: String
, propTerm :: Term }
data PredDef = PredDef
{ predId :: String
, predStateVars :: [StateVarDef]
, predInit :: Term
, predTrans :: Term }
data StateVarDef = StateVarDef
{ varId :: String
, varType :: Type
, 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]