package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a trans
type 'a tlist = 'a list trans
val store : (Task.task -> 'a) -> 'a trans
val apply : 'a trans -> Task.task -> 'a
val identity : Task.task trans
val identity_l : Task.task tlist
val singleton : 'a trans -> 'a tlist
val return : 'a -> 'a trans
val bind : 'a trans -> ('a -> 'b trans) -> 'b trans
val bind_comp : ('a * Task.task) trans -> ('a -> 'b trans) -> 'b trans
val trace_goal : string -> Task.task trans -> Task.task trans
val compose : Task.task trans -> 'a trans -> 'a trans
val compose_l : Task.task tlist -> 'a tlist -> 'a tlist
val seq : Task.task trans list -> Task.task trans
val seq_l : Task.task tlist list -> Task.task tlist
val par : Task.task trans list -> Task.task tlist
val fold : (Task.task_hd -> 'a -> 'a) -> 'a -> 'a trans
val fold_l : (Task.task_hd -> 'a -> 'a list) -> 'a -> 'a tlist
val fold_decl : (Decl.decl -> 'a -> 'a) -> 'a -> 'a trans
val fold_map : (Task.task_hd -> ('a * 'b) -> 'a * 'b) -> 'a -> 'b -> 'b trans
val fold_map_l : (Task.task_hd -> ('a * 'b) -> ('a * 'b) list) -> 'a -> 'b -> 'b tlist
val decl : (Decl.decl -> Decl.decl list) -> Task.task -> Task.task trans
val decl_l : (Decl.decl -> Decl.decl list list) -> Task.task -> Task.task tlist
val tdecl : (Decl.decl -> Theory.tdecl list) -> Task.task -> Task.task trans
val tdecl_l : (Decl.decl -> Theory.tdecl list list) -> Task.task -> Task.task tlist
val goal : (Decl.prsymbol -> Term.term -> Decl.decl list) -> Task.task trans
val goal_l : (Decl.prsymbol -> Term.term -> Decl.decl list list) -> Task.task tlist
val tgoal : (Decl.prsymbol -> Term.term -> Theory.tdecl list) -> Task.task trans
val tgoal_l : (Decl.prsymbol -> Term.term -> Theory.tdecl list list) -> Task.task tlist
val rewrite : (Term.term -> Term.term) -> Task.task -> Task.task trans
val rewriteTF : (Term.term -> Term.term) -> (Term.term -> Term.term) -> Task.task -> Task.task trans
val add_decls : Decl.decl list -> Task.task trans
val add_tdecls : Theory.tdecl list -> Task.task trans
val on_meta : Theory.meta -> (Theory.meta_arg list list -> 'a trans) -> 'a trans
val on_meta_excl : Theory.meta -> (Theory.meta_arg list option -> 'a trans) -> 'a trans
val on_used_theory : Theory.theory -> (bool -> 'a trans) -> 'a trans
val on_cloned_theory : Theory.theory -> (Theory.symbol_map list -> 'a trans) -> 'a trans
val on_tagged_ty : Theory.meta -> (Ty.Sty.t -> 'a trans) -> 'a trans
val on_tagged_ts : Theory.meta -> (Ty.Sts.t -> 'a trans) -> 'a trans
val on_tagged_ls : Theory.meta -> (Term.Sls.t -> 'a trans) -> 'a trans
val on_tagged_pr : Theory.meta -> (Decl.Spr.t -> 'a trans) -> 'a trans
exception UnknownFlagTrans of Theory.meta * string * string list
exception IllegalFlagTrans of Theory.meta
type ('a, 'b) flag_trans = ('a -> 'b trans) Wstdlib.Hstr.t
val on_flag : Theory.meta -> ('a, 'b) flag_trans -> string -> 'a -> 'b trans
val on_flag_t : Theory.meta -> ('a, 'b) flag_trans -> ('a -> 'b trans) -> 'a -> 'b trans
val print_meta : Debug.flag -> Theory.meta -> Task.task trans
val create_debugging_trans : string -> Task.task trans -> Task.task trans
exception TransFailure of string * exn
exception UnknownTrans of string
exception KnownTrans of string
val register_env_transform : desc:Pp.formatted -> string -> (Env.env -> Task.task trans) -> unit
val register_env_transform_l : desc:Pp.formatted -> string -> (Env.env -> Task.task tlist) -> unit
val register_transform : desc:Pp.formatted -> string -> Task.task trans -> unit
val register_transform_l : desc:Pp.formatted -> string -> Task.task tlist -> unit
val lookup_transform : string -> Env.env -> Task.task trans
val lookup_transform_l : string -> Env.env -> Task.task tlist
val list_transforms : unit -> (string * Pp.formatted) list
val list_transforms_l : unit -> (string * Pp.formatted) list
val named : string -> 'a trans -> 'a trans
type naming_table = {
  1. namespace : Theory.namespace;
  2. known_map : Decl.known_map;
  3. coercion : Coercion.t;
  4. printer : Ident.ident_printer;
  5. aprinter : Ident.ident_printer;
}
exception Bad_name_table of string
type trans_with_args = string list -> Env.env -> naming_table -> Task.task trans
type trans_with_args_l = string list -> Env.env -> naming_table -> Task.task tlist
val list_transforms_with_args : unit -> (string * Pp.formatted) list
val list_transforms_with_args_l : unit -> (string * Pp.formatted) list
val register_transform_with_args : desc:Pp.formatted -> string -> trans_with_args -> unit
val register_transform_with_args_l : desc:Pp.formatted -> string -> trans_with_args_l -> unit
type gentrans =
  1. | Trans_one of Task.task trans
  2. | Trans_list of Task.task tlist
  3. | Trans_with_args of trans_with_args
  4. | Trans_with_args_l of trans_with_args_l
val lookup_trans : Env.env -> string -> gentrans
val lookup_trans_desc : string -> Pp.formatted
val list_trans : unit -> string list
val apply_transform : string -> Env.env -> Task.task -> Task.task list
val apply_transform_args : string -> Env.env -> string list -> naming_table -> Task.task -> Task.task list
OCaml

Innovation. Community. Security.