Module Trans

module Trans: sig .. end

Task transformations


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

val fold : (Task.task_hd -> 'a -> 'a) -> 'a -> 'a trans

Iterating transformations

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 adds to task t1 the declarations f d for each declaration d of task t2. (similar to a "flat_map" operation)

val decl_l : (Decl.decl -> Decl.decl list list) -> Task.task -> Task.task tlist

decl_l f t1 t2: on each declaration d of task t2 (with f d = ld_1; ld_2; ... ld_n), create n duplicates (newt_i) of t1 with the declaration d_i replaced by ld_i.

Note for example that this 'decl_l (fun d -> [d]; [d])' will duplicate the task on each declaration and probably run forever.

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
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
val on_tagged_ty : Theory.meta -> (Ty.Sty.t -> '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_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 UnknownFlagTrans if ft does not have a requested association. Raises 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

Registration

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 file src/transform/args_wrapper.ml

type naming_table = {
   namespace : Theory.namespace;
   known_map : Decl.known_map;
   coercion : Coercion.t;
   printer : Ident.ident_printer;
   aprinter : Ident.ident_printer;
}

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 -> Task.task trans 
type trans_with_args_l = string list -> Env.env -> naming_table -> 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
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 -> Task.task -> Task.task list

apply a registered 1-to-1 or a 1-to-n or a trans with args, directly