rawast

-- data types for the parsed syntax.
-- Has the correct basic structure, but doesn't necessarily type check
-- It is also equipped with position information for extra debugging xp

module RawAst where

newtype Id = Id String
  deriving (Eq, Ord, Show, Read)

data Act = Main [RawBehaviour]
  deriving (Eq, Ord, Show, Read)

data RawBehaviour
    = Transition Id Id Id [Decl] [IffH] TransitionClaim
    | Constructor Id Id [Decl] [IffH] ConstructionClaim
  deriving (Eq, Ord, Show, Read)

data ConstructionClaim = CCases [(Expr, PostCreates)] | CDirect PostCreates
  deriving (Eq, Ord, Show, Read)

data TransitionClaim = TCases [(Expr, Post)] | TDirect Post
  deriving (Eq, Ord, Show, Read)

data Post
    = Post (Maybe Storage) [ExtStorage] (Maybe Expr)
  deriving (Eq, Ord, Show, Read)

data PostCreates
    = PostCreates [Assign] [ExtStorage]
  deriving (Eq, Ord, Show, Read)

type Storage = [(Entry, Expr)]

data ExtStorage
    = ExtStorage Expr [(Entry, Expr)]
    | ExtCreates Id Expr [Assign]
  deriving (Eq, Ord, Show, Read)

data Assign = Assignval Decl Expr | AssignMany Decl [Defn] | AssignStruct Decl [Defn]
  deriving (Eq, Ord, Show, Read)

data IffH = Iff [Expr] | IffIn Type [Expr]
  deriving (Eq, Ord, Show, Read)

data Entry
  = Simple Id
  | Lookup Entry Expr
  | Struct Entry Id
  deriving (Eq, Ord, Show, Read)

data Defn = Defn Expr Expr
  deriving (Eq, Ord, Show, Read)

data Expr
    = EAnd Expr Expr
    | EOr Expr Expr
    | EImpl Expr Expr
    | EEq Expr Expr
    | ENeq Expr Expr
    | ELEQ Expr Expr
    | ELE Expr Expr
    | EGEQ Expr Expr
    | EGE Expr Expr
    | ETrue
    | EFalse
    | EAdd Expr Expr
    | ESub Expr Expr
    | EITE Expr Expr Expr
    | EMul Expr Expr
    | EDiv Expr Expr
    | EMod Expr Expr
    | EExp Expr Expr
    | Zoom Expr Expr
    | Func Id [Expr]
    | Look Expr Expr
    | ECat Expr Expr
    | ESlice Expr Expr Expr
    | Newaddr Expr Expr
    | Newaddr2 Expr Expr Expr
    | BYHash Expr
    | BYAbiE Expr
    | StringLit String
    | StorageEntry Entry
    | Var Id
    | IntLit Integer
  deriving (Eq, Ord, Show, Read)

data Decl = Dec Type Id
  deriving (Eq, Ord, Show, Read)

data Type
    = T_uint
    | T_int
    | T_uint256
    | T_int256
    | T_uint126
    | T_int126
    | T_uint8
    | T_int8
    | T_address
    | T_bytes
    | T_bytes32
    | T_bytes4
    | T_bool
    | T_string
    | T_StaticArray Type Integer
    | T_DynamicArray Type
    | T_Map Type Type
    | T_Tuple [Type]
    | T_Contract Id
  deriving (Eq, Ord, Show, Read)