Module AltErgoLib.Parsed

type constant =
  1. | ConstBitv of string
  2. | ConstInt of string
  3. | ConstReal of Numbers.Q.t
  4. | ConstTrue
  5. | ConstFalse
  6. | ConstVoid
type pp_infix =
  1. | PPand
  2. | PPor
  3. | PPxor
  4. | PPimplies
  5. | PPiff
  6. | PPlt
  7. | PPle
  8. | PPgt
  9. | PPge
  10. | PPeq
  11. | PPneq
  12. | PPadd
  13. | PPsub
  14. | PPmul
  15. | PPdiv
  16. | PPmod
  17. | PPpow_int
  18. | PPpow_real
type pp_prefix =
  1. | PPneg
  2. | PPnot
type ppure_type =
  1. | PPTint
  2. | PPTbool
  3. | PPTreal
  4. | PPTunit
  5. | PPTbitv of int
  6. | PPTvarid of string * Loc.t
  7. | PPTexternal of ppure_type list * string * Loc.t
val pp_ppure_type : Stdlib.Format.formatter -> ppure_type -> unit
val pp_ppure_type_list : Stdlib.Format.formatter -> ppure_type list -> unit
type pattern = {
  1. pat_loc : Loc.t;
  2. pat_desc : string * string list;
}
type lexpr = {
  1. pp_loc : Loc.t;
  2. pp_desc : pp_desc;
}
and pp_desc =
  1. | PPvar of string
  2. | PPapp of string * lexpr list
  3. | PPmapsTo of string * lexpr
  4. | PPinInterval of lexpr * bool * lexpr * lexpr * bool
  5. | PPdistinct of lexpr list
  6. | PPconst of constant
  7. | PPinfix of lexpr * pp_infix * lexpr
  8. | PPprefix of pp_prefix * lexpr
  9. | PPget of lexpr * lexpr
  10. | PPset of lexpr * lexpr * lexpr
  11. | PPdot of lexpr * string
  12. | PPrecord of (string * lexpr) list
  13. | PPwith of lexpr * (string * lexpr) list
  14. | PPextract of lexpr * int * int
  15. | PPconcat of lexpr * lexpr
  16. | PPif of lexpr * lexpr * lexpr
  17. | PPforall of (string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
  18. | PPexists of (string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
  19. | PPforall_named of (string * string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
  20. | PPexists_named of (string * string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
  21. | PPnamed of string * lexpr
  22. | PPlet of (string * lexpr) list * lexpr
  23. | PPcheck of lexpr
  24. | PPcut of lexpr
  25. | PPcast of lexpr * ppure_type
  26. | PPmatch of lexpr * (pattern * lexpr) list
  27. | PPisConstr of lexpr * string
  28. | PPproject of lexpr * string
val pp_lexpr : Stdlib.Format.formatter -> lexpr -> unit
val pp_lexpr_list : Stdlib.Format.formatter -> lexpr list -> unit
type plogic_type =
  1. | PPredicate of ppure_type list
  2. | PFunction of ppure_type list * ppure_type
type body_type_decl =
  1. | Record of string * (string * ppure_type) list
  2. | Enum of string list
  3. | Algebraic of (string * (string * ppure_type) list) list
  4. | Abstract
type type_decl = Loc.t * string list * string * body_type_decl
type decl =
  1. | Theory of Loc.t * string * string * decl list
  2. | Axiom of Loc.t * string * Util.axiom_kind * lexpr
  3. | Rewriting of Loc.t * string * lexpr list
  4. | Goal of Loc.t * string * lexpr
  5. | Check_sat of Loc.t * string * lexpr
  6. | Logic of Loc.t * Symbols.name_kind * (string * string) list * plogic_type
  7. | Predicate_def of Loc.t * string * string * (Loc.t * string * ppure_type) list * lexpr
  8. | Function_def of Loc.t * string * string * (Loc.t * string * ppure_type) list * ppure_type * lexpr
  9. | MutRecDefs of (Loc.t * (string * string) * (Loc.t * string * ppure_type) list * ppure_type option * lexpr) list
  10. | TypeDecl of type_decl list
  11. | Push of Loc.t * int
  12. | Pop of Loc.t * int
  13. | Reset of Loc.t
  14. | Exit of Loc.t
  15. | Optimize of Loc.t * lexpr * bool
type file = decl list