why3 1.2.0 · OCaml Package

why3

type tdecl_set = private {

tds_set : Theory.Stdecl.t;
tds_tag : Weakhtbl.tag;

}

val tds_equal : tdecl_set -> tdecl_set -> bool

val tds_hash : tdecl_set -> int

val tds_compare : tdecl_set -> tdecl_set -> int

val tds_empty : tdecl_set

val mk_tds : Theory.Stdecl.t -> tdecl_set

type clone_map = tdecl_set Ident.Mid.t

type meta_map = tdecl_set Theory.Mmeta.t

type task = task_hd option

and task_hd = private {

task_decl : Theory.tdecl;
task_prev : task;
task_known : Decl.known_map;
task_clone : clone_map;
task_meta : meta_map;
task_tag : Weakhtbl.tag;

}

val task_equal : task -> task -> bool

val task_hd_equal : task_hd -> task_hd -> bool

val task_hash : task -> int

val task_hd_hash : task_hd -> int

val task_known : task -> Decl.known_map

val task_clone : task -> clone_map

val task_meta : task -> meta_map

val find_clone_tds : task -> Theory.theory -> tdecl_set

val find_meta_tds : task -> Theory.meta -> tdecl_set

val add_decl : task -> Decl.decl -> task

val add_tdecl : task -> Theory.tdecl -> task

val use_export : task -> Theory.theory -> task

val clone_export : task -> Theory.theory -> Theory.th_inst -> task

val add_meta : task -> Theory.meta -> Theory.meta_arg list -> task

val add_ty_decl : task -> Ty.tysymbol -> task

val add_data_decl : task -> Decl.data_decl list -> task

val add_param_decl : task -> Term.lsymbol -> task

val add_logic_decl : task -> Decl.logic_decl list -> task

val add_ind_decl : task -> Decl.ind_sign -> Decl.ind_decl list -> task

val add_prop_decl : 
  task ->
  Decl.prop_kind ->
  Decl.prsymbol ->
  Term.term ->
  task

val split_theory : Theory.theory -> Decl.Spr.t option -> task -> task list

val used_theories : task -> Theory.theory Ident.Mid.t

val used_symbols : Theory.theory Ident.Mid.t -> Theory.theory Ident.Mid.t

val local_decls : task -> Theory.theory Ident.Mid.t -> Decl.decl list

val task_fold : ('a -> Theory.tdecl -> 'a) -> 'a -> task -> 'a

val task_iter : (Theory.tdecl -> unit) -> task -> unit

val task_tdecls : task -> Theory.tdecl list

val task_decls : task -> Decl.decl list

val task_goal : task -> Decl.prsymbol

val task_goal_fmla : task -> Term.term

val task_separate_goal : task -> Theory.tdecl * task

val on_meta : 
  Theory.meta ->
  ('a -> Theory.meta_arg list -> 'a) ->
  'a ->
  task ->
  'a

val on_cloned_theory : 
  Theory.theory ->
  ('a -> Theory.symbol_map -> 'a) ->
  'a ->
  task ->
  'a

val on_meta_excl : Theory.meta -> task -> Theory.meta_arg list option

val on_used_theory : Theory.theory -> task -> bool

val on_tagged_ty : Theory.meta -> task -> Ty.Sty.t

val on_tagged_ts : Theory.meta -> task -> Ty.Sts.t

val on_tagged_ls : Theory.meta -> task -> Term.Sls.t

val on_tagged_pr : Theory.meta -> task -> Decl.Spr.t

exception NotTaggingMeta of Theory.meta

exception NotExclusiveMeta of Theory.meta

exception GoalNotFound

exception GoalFound

exception LemmaFound

package why3