Module AltErgoLib.Parsed

type constant =
| ConstBitv of string
| ConstInt of string
| ConstReal of Num.num
| ConstTrue
| ConstFalse
| ConstVoid
type pp_infix =
| PPand
| PPor
| PPxor
| PPimplies
| PPiff
| PPlt
| PPle
| PPgt
| PPge
| PPeq
| PPneq
| PPadd
| PPsub
| PPmul
| PPdiv
| PPmod
| PPpow_int
| PPpow_real
type pp_prefix =
| PPneg
| PPnot
type ppure_type =
| PPTint
| PPTbool
| PPTreal
| PPTunit
| PPTbitv of int
| PPTvarid of string * Loc.t
| PPTexternal of ppure_type list * string * Loc.t
type pattern = {
pat_loc : Loc.t;
pat_desc : string * string list;
}
type lexpr = {
pp_loc : Loc.t;
pp_desc : pp_desc;
}
and pp_desc =
| PPvar of string
| PPapp of string * lexpr list
| PPmapsTo of string * lexpr
| PPinInterval of lexpr * bool * lexpr * lexpr * bool
| PPdistinct of lexpr list
| PPconst of constant
| PPinfix of lexpr * pp_infix * lexpr
| PPprefix of pp_prefix * lexpr
| PPget of lexpr * lexpr
| PPset of lexpr * lexpr * lexpr
| PPdot of lexpr * string
| PPrecord of (string * lexpr) list
| PPwith of lexpr * (string * lexpr) list
| PPextract of lexpr * lexpr * lexpr
| PPconcat of lexpr * lexpr
| PPif of lexpr * lexpr * lexpr
| PPforall of (string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
| PPexists of (string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
| PPforall_named of (string * string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
| PPexists_named of (string * string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
| PPnamed of string * lexpr
| PPlet of (string * lexpr) list * lexpr
| PPcheck of lexpr
| PPcut of lexpr
| PPcast of lexpr * ppure_type
| PPmatch of lexpr * (pattern * lexpr) list
| PPisConstr of lexpr * string
| PPproject of bool * lexpr * string
type plogic_type =
| PPredicate of ppure_type list
| PFunction of ppure_type list * ppure_type
type body_type_decl =
| Record of string * (string * ppure_type) list
| Enum of string list
| Algebraic of (string * (string * ppure_type) list) list
| Abstract
type type_decl = Loc.t * string list * string * body_type_decl
type decl =
| Theory of Loc.t * string * string * decl list
| Axiom of Loc.t * string * Util.axiom_kind * lexpr
| Rewriting of Loc.t * string * lexpr list
| Goal of Loc.t * string * lexpr
| Logic of Loc.t * Symbols.name_kind * (string * string) list * plogic_type
| Predicate_def of Loc.t * string * string * (Loc.t * string * ppure_type) list * lexpr
| Function_def of Loc.t * string * string * (Loc.t * string * ppure_type) list * ppure_type * lexpr
| TypeDecl of type_decl list
| Push of Loc.t * int
| Pop of Loc.t * int
type file = decl list