AltErgoLib.Parsed
type ppure_type =
| PPTint |
| PPTbool |
| PPTreal |
| PPTunit |
| PPTbitv of int |
| PPTvarid of string * Loc.t |
| PPTexternal of ppure_type list * string * Loc.t |
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 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 |
type file = decl list