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

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:

Creating a goal twice in the same branch
Creating a goal when analysing the goal of 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)

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

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