package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type attr =
  1. | ATstr of Ident.attribute
  2. | ATpos of Loc.position
type ident = {
  1. id_str : string;
  2. id_ats : attr list;
  3. id_loc : Loc.position;
}
type qualid =
  1. | Qident of ident
  2. | Qdot of qualid * ident
type pty =
  1. | PTtyvar of ident
  2. | PTtyapp of qualid * pty list
  3. | PTtuple of pty list
  4. | PTarrow of pty * pty
  5. | PTscope of qualid * pty
  6. | PTparen of pty
  7. | PTpure of pty
type ghost = bool
type pattern = {
  1. pat_desc : pat_desc;
  2. pat_loc : Loc.position;
}
and pat_desc =
  1. | Pwild
  2. | Pvar of ident
  3. | Papp of qualid * pattern list
  4. | Prec of (qualid * pattern) list
  5. | Ptuple of pattern list
  6. | Pas of pattern * ident * ghost
  7. | Por of pattern * pattern
  8. | Pcast of pattern * pty
  9. | Pscope of qualid * pattern
  10. | Pparen of pattern
  11. | Pghost of pattern
type binder = Loc.position * ident option * ghost * pty option
type param = Loc.position * ident option * ghost * pty
type term = {
  1. term_desc : term_desc;
  2. term_loc : Loc.position;
}
and term_desc =
  1. | Ttrue
  2. | Tfalse
  3. | Tconst of Number.constant
  4. | Tident of qualid
  5. | Tidapp of qualid * term list
  6. | Tapply of term * term
  7. | Tinfix of term * ident * term
  8. | Tinnfix of term * ident * term
  9. | Tbinop of term * Dterm.dbinop * term
  10. | Tbinnop of term * Dterm.dbinop * term
  11. | Tnot of term
  12. | Tif of term * term * term
  13. | Tquant of Dterm.dquant * binder list * term list list * term
  14. | Tattr of attr * term
  15. | Tlet of ident * term * term
  16. | Tcase of term * (pattern * term) list
  17. | Tcast of term * pty
  18. | Ttuple of term list
  19. | Trecord of (qualid * term) list
  20. | Tupdate of term * (qualid * term) list
  21. | Tscope of qualid * term
  22. | Tat of term * ident
type invariant = term list
type variant = (term * qualid option) list
type pre = term
type post = Loc.position * (pattern * term) list
type xpost = Loc.position * (qualid * (pattern * term) option) list
type spec = {
  1. sp_pre : pre list;
  2. sp_post : post list;
  3. sp_xpost : xpost list;
  4. sp_reads : qualid list;
  5. sp_writes : term list;
  6. sp_alias : (term * term) list;
  7. sp_variant : variant;
  8. sp_checkrw : bool;
  9. sp_diverge : bool;
  10. sp_partial : bool;
}
type expr = {
  1. expr_desc : expr_desc;
  2. expr_loc : Loc.position;
}
and expr_desc =
  1. | Etrue
  2. | Efalse
  3. | Econst of Number.constant
  4. | Eident of qualid
  5. | Eidapp of qualid * expr list
  6. | Eapply of expr * expr
  7. | Einfix of expr * ident * expr
  8. | Einnfix of expr * ident * expr
  9. | Elet of ident * ghost * Expr.rs_kind * expr * expr
  10. | Erec of fundef list * expr
  11. | Efun of binder list * pty option * Ity.mask * spec * expr
  12. | Eany of param list * Expr.rs_kind * pty option * Ity.mask * spec
  13. | Etuple of expr list
  14. | Erecord of (qualid * expr) list
  15. | Eupdate of expr * (qualid * expr) list
  16. | Eassign of (expr * qualid * expr) list
  17. | Esequence of expr * expr
  18. | Eif of expr * expr * expr
  19. | Ewhile of expr * invariant * variant * expr
  20. | Eand of expr * expr
  21. | Eor of expr * expr
  22. | Enot of expr
  23. | Ematch of expr * reg_branch list * exn_branch list
  24. | Eabsurd
  25. | Epure of term
  26. | Eidpur of qualid
  27. | Eraise of qualid * expr option
  28. | Eexn of ident * pty * Ity.mask * expr
  29. | Eoptexn of ident * Ity.mask * expr
  30. | Efor of ident * expr * Expr.for_direction * expr * invariant * expr
  31. | Eassert of Expr.assertion_kind * term
  32. | Escope of qualid * expr
  33. | Elabel of ident * expr
  34. | Ecast of expr * pty
  35. | Eghost of expr
  36. | Eattr of attr * expr
and reg_branch = pattern * expr
and exn_branch = qualid * pattern option * expr
and fundef = ident * ghost * Expr.rs_kind * binder list * pty option * Ity.mask * spec * expr
type field = {
  1. f_loc : Loc.position;
  2. f_ident : ident;
  3. f_pty : pty;
  4. f_mutable : bool;
  5. f_ghost : bool;
}
type type_def =
  1. | TDalias of pty
  2. | TDalgebraic of (Loc.position * ident * param list) list
  3. | TDrecord of field list
  4. | TDrange of BigInt.t * BigInt.t
  5. | TDfloat of int * int
type visibility =
  1. | Public
  2. | Private
  3. | Abstract
type type_decl = {
  1. td_loc : Loc.position;
  2. td_ident : ident;
  3. td_params : ident list;
  4. td_vis : visibility;
  5. td_mut : bool;
  6. td_inv : invariant;
  7. td_wit : (qualid * expr) list;
  8. td_def : type_def;
}
type logic_decl = {
  1. ld_loc : Loc.position;
  2. ld_ident : ident;
  3. ld_params : param list;
  4. ld_type : pty option;
  5. ld_def : term option;
}
type ind_decl = {
  1. in_loc : Loc.position;
  2. in_ident : ident;
  3. in_params : param list;
  4. in_def : (Loc.position * ident * term) list;
}
type metarg =
  1. | Mty of pty
  2. | Mfs of qualid
  3. | Mps of qualid
  4. | Max of qualid
  5. | Mlm of qualid
  6. | Mgl of qualid
  7. | Mstr of string
  8. | Mint of int
type clone_subst =
  1. | CStsym of qualid * ident list * pty
  2. | CSfsym of qualid * qualid
  3. | CSpsym of qualid * qualid
  4. | CSvsym of qualid * qualid
  5. | CSxsym of qualid * qualid
  6. | CSprop of Decl.prop_kind
  7. | CSaxiom of qualid
  8. | CSlemma of qualid
  9. | CSgoal of qualid
type decl =
  1. | Dtype of type_decl list
  2. | Dlogic of logic_decl list
  3. | Dind of Decl.ind_sign * ind_decl list
  4. | Dprop of Decl.prop_kind * ident * term
  5. | Dlet of ident * ghost * Expr.rs_kind * expr
  6. | Drec of fundef list
  7. | Dexn of ident * pty * Ity.mask
  8. | Dmeta of ident * metarg list
  9. | Dclone of qualid * clone_subst list
  10. | Duse of qualid
OCaml

Innovation. Community. Security.