Module Trans

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

Compose transformations

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

Iterating transformations

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 Decl.decl
| Normal_decl of Decl.decl
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:

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)

Dependent Transformations

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

Flag-dependent Transformations

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

Debug Transformations

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

Transformations with arguments

These transformations take strings as arguments. For a more "typed" version, see module Args_wrapper.

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;

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
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

Handling of all forms of transformations

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

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