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

exception Arg_parse_type_error of Loc.position * string * exn

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.	`*)`
`\|`	`Ttermlist_same : int * ('a10, 'b10) trans_typ -> (Term.term list -> 'a10, 'b10) trans_typ`	`(*`	transformation with a list of same type term: the int is the predefined length of the list	`*)`
`\|`	`Tterm : ('a11, 'b11) trans_typ -> (Term.term -> 'a11, 'b11) trans_typ`	`(*`	transformation with a Why3 term as argument	`*)`
`\|`	`Tformula : ('a12, 'b12) trans_typ -> (Term.term -> 'a12, 'b12) trans_typ`	`(*`	transformation with a Why3 formula as argument	`*)`
`\|`	`Ttheory : ('a13, 'b13) trans_typ -> (Theory.theory -> 'a13, 'b13) trans_typ`	`(*`	transformation with a Why3 theory name as argument	`*)`
`\|`	`Topt : string * ('a14 -> 'c, 'b14) trans_typ -> ('a14 option -> 'c, 'b14) trans_typ`	`(*`	transformation with an optional argument. The first string is the keyword introducing that optional argument	`*)`
`\|`	`Toptbool : string * ('a15, 'b15) trans_typ -> (bool -> 'a15, 'b15) trans_typ`	`(*`	transformation with an optional boolean argument. The first string is the keyword for that optional argument, its presence meaning "true"	`*)`

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

val set_argument_parsing_functions : Env.fformat ->
       parse_term:(Trans.naming_table -> Stdlib.Lexing.lexbuf -> Ptree.term) ->
       parse_term_list:(Trans.naming_table ->
                        Stdlib.Lexing.lexbuf -> Ptree.term list) ->
       parse_qualid:(Stdlib.Lexing.lexbuf -> Ptree.qualid) ->
       parse_list_qualid:(Stdlib.Lexing.lexbuf -> Ptree.qualid list) ->
       parse_list_ident:(Stdlib.Lexing.lexbuf -> Ptree.ident list) -> unit