Module Task

module Task: sig .. end
Proof Tasks, Cloning and Meta History

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 

Task
type task = task_hd option 
type task_hd = private {
   task_decl : Theory.tdecl; (*
last declaration
*)
   task_prev : task; (*
context
*)
   task_known : Decl.known_map; (*
known identifiers
*)
   task_clone : clone_map; (*
cloning history
*)
   task_meta : meta_map; (*
meta properties
*)
   task_tag : Weakhtbl.tag; (*
unique magical 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

Constructors


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

Declaration constructors + add_decl


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

Utilities


val split_theory : Theory.theory -> Decl.Spr.t option -> task -> task list
split_theory th s t returns the tasks of th added to t that end by one of s. They are in the opposite order than in the theory

Realization utilities


val used_theories : task -> Theory.theory Ident.Mid.t
returns a map from theory names to theories themselves
val used_symbols : Theory.theory Ident.Mid.t -> Theory.theory Ident.Mid.t
takes the result of used_theories and returns a map from symbol names to their theories of origin
val local_decls : task -> Theory.theory Ident.Mid.t -> Decl.decl list
takes the result of used_symbols and returns the list of declarations that are not imported with those theories or derived thereof

Bottom-up, tail-recursive traversal functions


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
task_separate_goal t returns a pair (g,t') where g is the goal of the task t and t' is the rest. raises GoalNotFound if task t has no goal

Selectors


val on_meta : Theory.meta -> ('a -> Theory.meta_arg list -> 'a) -> 'a -> task -> 'a
val on_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

Exceptions
exception NotTaggingMeta of Theory.meta
exception NotExclusiveMeta of Theory.meta
exception GoalNotFound
exception GoalFound
exception SkipFound
exception LemmaFound