Up  

Module Ast.Ast


module Ast: sig .. end

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 (*Expressions.*)

type exp =
| PrimExp of primexp
| RelationExp of string * relation
| VarExp of var
| FunAppExp of string list
| Binop of binop * exp * exp
| Boolop of boolop * exp * exp
| SymExp of symexp

type symexp =
| SymVar of var
| SymExpr of exp
| SymPred of Constraint.Constraint.cexp * exp * exp

type constraintexp =
| ConstraintExp of Constraint.Constraint.cexp
| ConstraintCurVar
| ConstraintDrop

type constraintvalue =
| ConstraintForall of string * string * constraintvalue
| ConstraintExists of string * string * constraintvalue
| CValExp of constraintexp

type constraintbody =
| ConstraintAssume of constraintvalue list
| ConstraintAssert of constraintvalue list

type var =
| Var of string
| RecordIndexVar of string * string * int
| IndexVar of string * string (*Data gets stored with its constraints*)
Data fields for a record (i.e. one line of a file).
type datafields = exp MapUtils.StringMap.t 
type relation = datafields MapUtils.IntMap.t

type stmt =
| AssignStmt of var * exp
| Cond of exp * stmt list * stmt list
| ForEachLoop of string * string * stmt list
| Return of exp
| Assert of exp
| Assume of exp
| Concretize of var
| CRange of var

type userty = {
   dataname : string;
   fieldinfo : (string * bool * typerep) list;
}
type fundecl = {
   funname : string;
   funargs : (string * typerep) list;
   funbody : stmt list;
}
type topdecl =
| TypeDecl of userty * constraintbody list
| FunDecl of fundecl
| AssignDecl of string * typerep * exp