why3 1.3.2 · OCaml Package

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

type diff_decl =

| Goal_decl of Decl.decl
| Normal_decl of Decl.decl

val decl_goal_l : 
  (Decl.decl -> diff_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 = {

namespace : Theory.namespace;
known_map : Decl.known_map;
coercion : Coercion.t;
printer : Ident.ident_printer;
aprinter : Ident.ident_printer;
meta_id_args : Ident.ident Wstdlib.Mstr.t;

}

exception Bad_name_table of string

type trans_with_args =
  string list ->
  Env.env ->
  naming_table ->
  Env.fformat ->
  Task.task trans

type trans_with_args_l =
  string list ->
  Env.env ->
  naming_table ->
  Env.fformat ->
  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 =

| Trans_one of Task.task trans
| Trans_list of Task.task tlist
| Trans_with_args of trans_with_args
| 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

exception Unnecessary_arguments of string list

val apply_transform : string -> Env.env -> Task.task -> Task.task list

val apply_transform_args : 
  string ->
  Env.env ->
  string list ->
  naming_table ->
  Env.fformat ->
  Task.task ->
  Task.task list

package why3