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;`	`(*`	use/clone 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 list of proof tasks that correspond to goals in th, in the order of appearance. If set s is not empty, then only the goals in s are proved. The goals which are instances of already proved propositions (introduced by cloning) are not proved. Task t is the task prefix that can be used to add some metas to every generated proof task.

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 Task.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 Task.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 Task.GoalNotFound if task t has no goal

Selectors

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

Exceptions

exception NotTaggingMeta of Theory.meta

exception NotExclusiveMeta of Theory.meta

exception GoalNotFound

exception GoalFound

exception LemmaFound