sig
  type typerep =
      IntType
    | FloatType
    | StringType
    | BoolType
    | RelationType of string
    | OtherType of string
    | Unknown
  type binop = Plus | Minus | Times | Divide
  type boolop = Equiv | Nequiv | Or | And | Lt | Lte | Gt | Gte
  type primexp =
      Float of float
    | Integer of int
    | String of string
    | Bool of bool
  and exp =
      PrimExp of Ast.Ast.primexp
    | RelationExp of string * Ast.Ast.relation
    | VarExp of Ast.Ast.var
    | FunAppExp of string list
    | Binop of Ast.Ast.binop * Ast.Ast.exp * Ast.Ast.exp
    | Boolop of Ast.Ast.boolop * Ast.Ast.exp * Ast.Ast.exp
    | SymExp of Ast.Ast.symexp
  and symexp =
      SymVar of Ast.Ast.var
    | SymExpr of Ast.Ast.exp
    | SymPred of Constraint.Constraint.cexp * Ast.Ast.exp * Ast.Ast.exp
  and constraintexp =
      ConstraintExp of Constraint.Constraint.cexp
    | ConstraintCurVar
    | ConstraintDrop
  and constraintvalue =
      ConstraintForall of string * string * Ast.Ast.constraintvalue
    | ConstraintExists of string * string * Ast.Ast.constraintvalue
    | CValExp of Ast.Ast.constraintexp
  and constraintbody =
      ConstraintAssume of Ast.Ast.constraintvalue list
    | ConstraintAssert of Ast.Ast.constraintvalue list
  and var =
      Var of string
    | RecordIndexVar of string * string * int
    | IndexVar of string * string
  and datafields = Ast.Ast.exp MapUtils.StringMap.t
  and relation = Ast.Ast.datafields MapUtils.IntMap.t
  type stmt =
      AssignStmt of Ast.Ast.var * Ast.Ast.exp
    | Cond of Ast.Ast.exp * Ast.Ast.stmt list * Ast.Ast.stmt list
    | ForEachLoop of string * string * Ast.Ast.stmt list
    | Return of Ast.Ast.exp
    | Assert of Ast.Ast.exp
    | Assume of Ast.Ast.exp
    | Concretize of Ast.Ast.var
    | CRange of Ast.Ast.var
  type userty = {
    dataname : string;
    fieldinfo : (string * bool * Ast.Ast.typerep) list;
  }
  type fundecl = {
    funname : string;
    funargs : (string * Ast.Ast.typerep) list;
    funbody : Ast.Ast.stmt list;
  }
  type topdecl =
      TypeDecl of Ast.Ast.userty * Ast.Ast.constraintbody list
    | FunDecl of Ast.Ast.fundecl
    | AssignDecl of string * Ast.Ast.typerep * Ast.Ast.exp
end