package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type loc = Loc.position
type qualid = loc * string list
type pty =
  1. | PTyvar of string
  2. | PTyapp of qualid * pty list
  3. | PTuple of pty list
type metarg =
  1. | PMAty of pty
  2. | PMAfs of qualid
  3. | PMAps of qualid
  4. | PMApr of qualid
  5. | PMAstr of string
  6. | PMAint of int
type th_rule =
  1. | Rprelude of string
  2. | Rsyntaxts of qualid * string * bool
  3. | Rsyntaxfs of qualid * string * bool
  4. | Rsyntaxps of qualid * string * bool
  5. | Rliteral of qualid * string * bool
  6. | Rremovepr of qualid
  7. | Rremoveall
  8. | Rmeta of string * metarg list
  9. | Ruse of qualid
type theory_rules = {
  1. thr_name : qualid;
  2. thr_rules : (loc * th_rule) list;
}
type mo_rule =
  1. | MRtheory of th_rule
  2. | MRinterface of string
  3. | MRexception of qualid * string
  4. | MRval of qualid * string * int list
type module_rules = {
  1. mor_name : qualid;
  2. mor_rules : (loc * mo_rule) list;
}
type global =
  1. | Prelude of string
  2. | Printer of string
  3. | ModelParser of string
  4. | RegexpValid of string
  5. | RegexpInvalid of string
  6. | RegexpTimeout of string
  7. | RegexpOutOfMemory of string
  8. | RegexpStepLimitExceeded of string
  9. | RegexpUnknown of string * string
  10. | RegexpFailure of string * string
  11. | TimeRegexp of string
  12. | StepRegexp of string * int
  13. | ExitCodeValid of int
  14. | ExitCodeInvalid of int
  15. | ExitCodeTimeout of int
  16. | ExitCodeStepLimitExceeded of int
  17. | ExitCodeUnknown of int * string
  18. | ExitCodeFailure of int * string
  19. | Filename of string
  20. | Transform of string
  21. | Plugin of string * string
  22. | Blacklist of string list
type file = {
  1. f_global : (loc * global) list;
  2. f_rules : theory_rules list;
}
type global_extract =
  1. | EPrelude of string
  2. | EPrinter of string
  3. | EBlacklist of string list
type file_extract = {
  1. fe_global : (loc * global_extract) list;
  2. fe_th_rules : theory_rules list;
  3. fe_mo_rules : module_rules list;
}
OCaml

Innovation. Community. Security.