module Macros: functor (
E
:
sig
end
) ->
sig
.. end
Parameters: |
E |
: |
sig val env : env end
|
|
Record Macros
val remove_singleton_record_updates : Typed_ast.exp Trans.macro
remove_singleton_record_updates
replaces updates of
records that have only one field with the construction
of a completely new record.
val remove_multiple_record_updates : Typed_ast.exp Trans.macro
remove_multiple_record_updates
replaces record updates
simultaneously updating multiple fields with a nested record
update, each affecting only one field, that achieves the same
effect.
val sort_record_fields : Typed_ast.exp Trans.macro
sort_record_fields
sorts the fields of a record expression
into the same order as in the definition of the record
type. If they do not need resorting, everything is fine,
otherwise a warning is produced.
Set and List Comprehension Macros
val remove_list_comprehension : Typed_ast.exp Trans.macro
remove_list_comprehension
removes list comprehensions by turning
them into fold and insert operations. A Trans_error
exception is
thrown, if not only bounded quantification is used.
val remove_set_comprehension : Typed_ast.exp Trans.macro
remove_set_comprehension
removes set comprehensions by turning
them into fold and insert operations. A Trans_error
exception is
thrown, if not only bounded quantification is used.
val remove_set_comprehension_image_filter : bool -> Typed_ast.exp Trans.macro
remove_set_comprehension allow_sigma
removes set comprehensions by turning
them into set-image, set-filter and set-product operations. For example
{ f (x,y,z) | forall ((x,y) IN A) (z IN B) | P (x, y, z)}
is turned into
Set.image f (Set.filter P (Set.cross A B))
. If
allow_sigma
is set and the
quantifiers depend on each other,
set_sigma
is used instead. So, for example
{ f (x,y,z) | forall ((x,y) IN A) (z IN B x) | P (x, y, z)}
is turned into
Set.image f (Set.filter P (Set.set_sigma A (fun (x, y) -> B x)))
.
In contrast to remove_set_comprehension
no exception is thrown, if the translation fails.
This is because it is intended to be used
with theorem prover backends, which can handle unbounded quantification differently.
val remove_setcomp : Typed_ast.exp Trans.macro
remove_setcomp
removes set comprehensions with implicit bound variable to ones with
explicitly bound onces. For example { (x, y) | x > y }
might, depending on context be turned
in { (x, y) | forall x | x > y}
, { (x, y) | forall x y | x > y}
or something similar.
val cleanup_set_quant : Typed_ast.exp Trans.macro
cleanup_set_quant
moves restricted and unrestricted quantification
in set comprehensions to the condition part, if the bound variables are only used by the condition.
This means, that expressions of the form { f x | forall (p IN e) ... | P x }
become
{ f x | forall ... | exists (p IN e). P x }
if x
is not a member of FV p
.
val remove_set_comp_binding : Typed_ast.exp Trans.macro
remove_set_comp_binding
tries to turn Comb_binding
expressions into Set_comb
ones.
Given a term of the form { f x z | forall x z | P x z y1 ... yn }
it checks that only
unbounded quantification is used and that the set of bound variables is exactly the set of free
variables of the expression f x z
. If this is the case, the expression is transformed to
{ f x z | P x z y1 ... yn }
. Otherwise remove_set_comp_binding
fails.
val remove_set_restr_quant : Typed_ast.exp Trans.macro
remove_set_restr_quant
turns restricted quantification in set comprehensions
into unrestricted quantification. Expressions of the form { f x | forall (p IN e) | P x }
become
{ f x | FV(p) | forall FV(p). p IN e /\ P x }
. This requires turning pattern p
into
an expression. This is likely to fail for more complex patterns. In these cases, remove_set_restr_quant
fails and pattern compilation is needed.
Quantifier Macros
val list_quant_to_set_quant : Typed_ast.exp Trans.macro
list_quant_to_set_quant
turns forall (x MEM L). P x
into forall (x IN Set.from_list L). P x
val remove_restr_quant : (Typed_ast.pat -> bool) -> Typed_ast.exp Trans.macro
remove_restr_quant pat_OK
turns restricted quantification into unrestricted quantification,
if then pattern does not satisfy pat_OK
. For example, expressions of the from forall (p IN e). P x
becomes
forall FV(p). p IN e --> P x
, if pat_OK p
does not hold. pat_OK
is used to configure, which types
of restricted quantification are supported by the backend. For example, HOL 4 supports
patterns consisting of variables, tuples and wildcard patterns, while Isabelle does not like wildcard ones.
This macros tries to turn pattern p
into
an expression. This is likely to fail for more complex patterns. In these cases, remove_restr_quant pat_OK
fails and pattern compilation is needed.
val remove_quant : Typed_ast.exp Trans.macro
remove_quant
turns quantifiers into iteration. It throws an Trans_error
exception, if used
on unrestricted quantification. Given an expression forall (x IN X). P x
this returns
Set.forall X (fun x -> P x)
. It also works for existential quantification and quantification
over lists.
val remove_quant_coq : Typed_ast.exp Trans.macro
remove_quant_coq
the same as above but does not apply in the body of lemma or theorem
statements. Specific to the Coq backend.
Pattern Macros
val remove_unit_pats : Trans.pat_macro
remove_unit_pats
replaces unit-patterns ()
with wildcard ones _
.
val coq_type_annot_pat_vars : Trans.pat_macro
Add type annotations to pattern variables whose type contains a type variable
(only add for arguments to top-level functions)
Type Class Macros
val remove_method : Target.target -> bool -> Typed_ast.exp Trans.macro
remove_method target add_dict
is used to remove occurrences of class methods.
If a class method is encountered, the remove_method
macro first tries to
resolve the type-class instantiation statically and replace the method with it's
instantiation. If this static resolving attempt fails, it is checked, whether the method
is inlined for this target. If this is not the case and the flag add_dict
is set,
the method is replaced with a lookup in a dictionary. This dictionary is added by the
Def_trans.class_constraint_to_parameter
to the arguments of each definition that
has type class constraints.
val remove_method_pat : Trans.pat_macro
remove_method_pat
is used to remove occurrences of class methods.
If a class method is encountered, remove_method_pat
macro tries to
resolve the type-class instantiation statically and replace the method with it's
instantiation.
val remove_num_lit : Typed_ast.exp Trans.macro
remove_num_lit
replaces L_num (sk, i)
with fromNumeral (L_numeral (sk, i))
.
This is the first step into using type classes to handle numerals.
val remove_class_const : Target.target -> Typed_ast.exp Trans.macro
remove_class_const
remove constants that have class constraints by adding
explicit dictionary parameters.
Misc
val remove_function : Typed_ast.exp Trans.macro
remove_function
turns function | pat1 -> exp1 ... | patn -> expn end
into
fun x -> match x with | pat1 -> exp1 ... | patn -> expn end
.
val remove_sets : Typed_ast.exp Trans.macro
Warning: OCaml specific! remove_sets
transforms set expressions like {e1, ..., en}
into
Ocaml.Pset.from_list (type_specific compare) [e1, ..., en]
val string_lits_isa : Typed_ast.exp Trans.macro
string_lits_isa
translates non-representable string literals into list
of characters for Isabelle
val remove_fun_pats : bool -> Typed_ast.exp Trans.macro
remove_fun_pats keep_tup
removes patterns from expressions of the from
fun p1 ... pn -> e
by introducing function
expressions.
Variable patterns and - if keep_tup
is set - tuple patterns are kept.
Macros I don't understand
val add_nexp_param_in_const : Typed_ast.exp Trans.macro
val remove_vector_access : Typed_ast.exp Trans.macro
val remove_vector_sub : Typed_ast.exp Trans.macro
val remove_do : Typed_ast.exp Trans.macro