sig
  module Ast :
    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
end