module Trans:sig
..end
Task transformations
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
parallelize transformations: par l
will duplicate the current
task in n
new tasks, with n
the length of l
, and apply to each of
this new task the corresponding transformation in l
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
decl f t1 t2
appends to task t1
the set of declarations f d
for each declaration d
of task t2
, similarly to a "flat_map"
operation on lists.
For example, if t2
is made of the two declarations d1
and d2
in that order, if f d1 = [d11;d12]
and f d2 = [d21;d22]
, then
the resulting task contains the declarations of t1
followed by
d11;d12;d21;d22
val decl_l : (Decl.decl -> Decl.decl list list) -> Task.task -> Task.task tlist
decl_f f t1 t2
produces a set of tasks obtained by appending new
declarations to task t1
. It iterates on each declaration d
appearing in t2
: if f d = [ld_1; ld_2; ... ld_n]
then it
produces n
tasks t'1;..;t'n
, where ld_i
is appended to t'i
.
The operation on remaining tasks of t2
are then applied to each task t'i
.
For example, if t2
is made of the two declarations d1
and d2
in that order, if f d1 = [[d111;d112];[d12]]
and f d2 =
[[d21];[d221;d222]]
, then the result is made of the 4 tasks
t1;d111;d112;d21
, t1;d111;d112;d221;d222
, t1;d12;d21
and
t1;d12;d221;d222
type
diff_decl =
| |
Goal_decl of |
| |
Normal_decl of |
val decl_goal_l : (Decl.decl -> diff_decl list list) ->
Task.task -> Task.task tlist
decl_goal_l f t1 t2
does the same as Trans.decl_l
except that it can
differentiate a new axiom added to a task from a new goal added to a task.
In case of a new axiom, everything works as in decl_l. When a new goal ng
is generated, it is remembered so that it can replace the old_goal when the
end of the task is encountered.
Example of use of this feature in the code of destruct
:
H1: p1 -> p2
H2: p3
H3: ...
-------------
Goal: True
In destruct H1
, we know that we will add a new goal p1
before we read
through the entire task, so we need to be able to generate a new goal.
Current disallowed cases:
t2
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
rewrite f t1 t2
appends to task t1
the declarations in t2
in which each top level formula t
is replaced by f t
*
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
add_decls ld t1
adds decls ld at the end of the task t1 (before the goal)
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
on_tagged_* m f
allow to do a transformation having all the tagged declarations
in a set as argument of f.
If used to modify the existing task, be careful to not make references to
declarations found in the set before they are actually declared in the new task.
For example, this will likely fail:
Trans.on_tagged_ls some_meta (fun s -> Trans.decl (fun d -> [d; s.choose]))
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
on_flag m ft def arg
takes an exclusive meta m
of type [MTstring]
,
a hash table ft
, a default flag value def
, and an argument arg
.
Returns a transformation that is associated in ft
to the value of m
in a given task. If the meta m
is not set in the task, returns the
transformation associated to def
. Raises Trans.UnknownFlagTrans
if ft
does not have a requested association. Raises Trans.IllegalFlagTrans
if
the type of m
is not [MTstring]
.
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
print_meta f m
is an identity transformation that
prints every meta m
in the task if flag d
is set
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
give transformation a name without registering
These transformations take strings as arguments. For a more "typed" version,
see module Args_wrapper
.
type
naming_table = {
|
namespace : |
|
known_map : |
|
coercion : |
|
printer : |
|
aprinter : |
|
meta_id_args : |
}
In order to interpret, that is type, string arguments as symbols or
terms, a transformation may need a naming_table
. Typing arguments
requires looking up identifiers into the namespace
and also
looking up declarations into the known_map
. Since the identifiers
given as arguments come from the task as it is displayed to the
user, we need to ensure that the names in the namespace
are
coherent with the names that are printed, this why we also record
the printer
.
See module Args_wrapper
for the functions that builds objects of
type naming_table
from given tasks, and types the arguments of
transformations.
exception Bad_name_table of string
typetrans_with_args =
string list ->
Env.env -> naming_table -> Env.fformat -> Task.task trans
typetrans_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 |
| |
Trans_list of |
| |
Trans_with_args of |
| |
Trans_with_args_l of |
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
apply a registered 1-to-1 or a 1-to-n, directly.
val apply_transform_args : string ->
Env.env ->
string list ->
naming_table -> Env.fformat -> Task.task -> Task.task list
apply a registered 1-to-1 or a 1-to-n or a trans with args, directly