Module Args_wrapper

module Args_wrapper: sig .. end

Pre-processing of transformations with arguments, including parsing and typing in the context of a task.


context for parsing/typing transformation arguments

exception Parse_error of string
exception Arg_expected of string * string
exception Arg_theory_not_found of string
exception Arg_expected_none of string
exception Arg_pr_not_found of Decl.prsymbol
exception Arg_qid_not_found of Ptree.qualid
exception Arg_error of string
val build_naming_tables : Task.task -> Trans.naming_table

builds a naming tabl from a task, suitable for both parsing/typing transformation arguments and for printing the task, with coherent identifiers names.

type symbol = 
| Tstysymbol of Ty.tysymbol
| Tsprsymbol of Decl.prsymbol
| Tslsymbol of Term.lsymbol
val find_symbol : string -> Trans.naming_table -> symbol

transformation types

transformations with argument are themselves given types to control the interpretation of their raw string arguments. The type trans_typ of such transformations is elegantly defined as a GADT

type ('_, '_) trans_typ = 
| Ttrans : (Task.task Trans.trans, Task.task) trans_typ (*

transformation with no argument, and exactly one resulting task

*)
| Ttrans_l : (Task.task Trans.tlist, Task.task list) trans_typ (*

transformation with no argument, and many resulting tasks

*)
| Tenvtrans : (Env.env -> Task.task Trans.trans, Task.task) trans_typ (*

transformation with no argument but depending on the environment, and exactly one resulting task

*)
| Tenvtrans_l : (Env.env -> Task.task Trans.tlist, Task.task list) trans_typ (*

transformation with no argument but depending on the environment, and many resulting tasks

*)
| Tstring : ('a, 'b) trans_typ -> (string -> 'a, 'b) trans_typ (*

transformation with a string as argument

*)
| Tint : ('a0, 'b0) trans_typ -> (int -> 'a0, 'b0) trans_typ (*

transformation with an integer argument

*)
| Tty : ('a1, 'b1) trans_typ -> (Ty.ty -> 'a1, 'b1) trans_typ (*

transformation with a Why3 type as argument

*)
| Ttysymbol : ('a2, 'b2) trans_typ -> (Ty.tysymbol -> 'a2, 'b2) trans_typ (*

transformation with a Why3 type symbol as argument

*)
| Tprsymbol : ('a3, 'b3) trans_typ -> (Decl.prsymbol -> 'a3, 'b3) trans_typ (*

transformation with a Why3 proposition symbol as argument

*)
| Tprlist : ('a4, 'b4) trans_typ -> (Decl.prsymbol list -> 'a4, 'b4) trans_typ (*

transformation with a list of Why3 proposition symbols as argument. The symbols must be separated by commas

*)
| Tlsymbol : ('a5, 'b5) trans_typ -> (Term.lsymbol -> 'a5, 'b5) trans_typ (*

transformation with a Why3 logic symbol as argument

*)
| Tsymbol : ('a6, 'b6) trans_typ -> (symbol -> 'a6, 'b6) trans_typ (*

transformation with a Why3 symbol as argument, either a type symbol, a logic symbol or a proposotion symbol

*)
| Tlist : ('a7, 'b7) trans_typ -> (symbol list -> 'a7, 'b7) trans_typ (*

transformation with a list Why3 symbol as argument, either a type symbol, a logic symbol or a proposotion symbol. The symbols must be separated by commas

*)
| Tidentlist : ('a8, 'b8) trans_typ -> (string list -> 'a8, 'b8) trans_typ (*

transformation with a list of identifiers as argument. The identifiers do not need to exist in the task, typically they could be fresh symbols

*)
| Ttermlist : ('a9, 'b9) trans_typ -> (Term.term list -> 'a9, 'b9) trans_typ (*

transformation with a list of terms as argument.

*)
| Tterm : ('a10, 'b10) trans_typ -> (Term.term -> 'a10, 'b10) trans_typ (*

transformation with a Why3 term as argument

*)
| Tformula : ('a11, 'b11) trans_typ -> (Term.term -> 'a11, 'b11) trans_typ (*

transformation with a Why3 formula as argument

*)
| Ttheory : ('a12, 'b12) trans_typ -> (Theory.theory -> 'a12, 'b12) trans_typ (*

transformation with a Why3 theory name as argument

*)
| Topt : string * ('a13 -> 'c, 'b13) trans_typ -> ('a13 option -> 'c, 'b13) trans_typ (*

transformation with an optional argument. The first string is the keyword introducing that optional argument

*)
| Toptbool : string * ('a14, 'b14) trans_typ -> (bool -> 'a14, 'b14) trans_typ (*

transformation with an optional boolean argument. The first string is the keyword for that optional argument, its presence meaning "true"

*)
exception Arg_parse_type_error of Loc.position * string * exn
exception Unnecessary_arguments of string list

parsing and typing of arguments

the functions below wrap arguments of transformations, turning string arguments into arguments of proper types. arguments of type term of formula are parsed and typed, name resolution using the proper naming table.

val wrap_l : ('a, Task.task list) trans_typ -> 'a -> Trans.trans_with_args_l
val wrap : ('a, Task.task) trans_typ -> 'a -> Trans.trans_with_args
val wrap_and_register : desc:Pp.formatted -> string -> ('a, 'b) trans_typ -> 'a -> unit