module Patterns:pattern compilationsig
..end
type
match_props = {
|
is_exhaustive : |
|
missing_pats : |
|
redundant_pats : |
|
overlapping_pats : |
val check_match_exp : Typed_ast.env -> Typed_ast.exp -> match_props option
check_match_exp env e
checks the pattern match expression e
in environment env
. If
e
is not a pattern match, None
is returned. Otherwise, a record of type match_props
is
returned that contains information on whether the match is exhaustive, contains redundant parts etc.val check_pat_list : Typed_ast.env -> Typed_ast.pat list -> match_props option
check_pat_list env pl
checks the pattern list pL
in environment env
. If
pL
is empty or the compilation fails, None
is returned. Otherwise, a record of type match_props
is
returned that contains information on whether the match is exhaustive, contains redundant parts etc.val check_match_exp_warn : Typed_ast.env -> Typed_ast.exp -> unit
check_match_exp_warn env e
internally calls check_match_exp env e
. Instead of returning
the properties of the match expression, it prints appropriate warning messages, though.val check_match_def : Typed_ast.env -> Typed_ast.def -> (Name.t * match_props) list
check_match_def env d
checks a definition using pattern matching d
in environment env
.
Definitions of mutually recursive functions can contain multiple top-level pattern matches.
Therefore, a list is returned. This lists consists of pairs of
the name of the defined function and it's properties. If the definition does not have a top-level pattern match,
i.e. if it is not a function definition, the empty list is returned.val check_match_def_warn : Typed_ast.env -> Typed_ast.def -> unit
check_match_def_warn env d
checks a definition and prints appropriate warning messages.type
match_check_arg
val cleanup_match_exp : Typed_ast.env -> bool -> Typed_ast.exp -> Typed_ast.exp option
cleanup_match_exp env add_missing e
tries to cleanup the match-expression e
by removing
redunanant rows. Moreover, missing patterns are added at the end, if the argument add_missing
is set.val compile_match_exp : Target.target ->
match_check_arg ->
Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp option
compile_match_exp target_opt pat_OK env e
compiles match-expressions. In contrast to
check_match_exp
only case-expressions are checked. Other types of pattern matches
have to be brought into this form first.
If the case-expression e
contains a pattern p
such that pat_OK p
does not hold,
the whole case-expression is processed and transformed into an expression with
the same semantics that contains only supported patterns. During this compilation,
warning messages might be issued. This warning uses target_opt
. Otherwise, it is not used.
val compile_exp : Target.target ->
match_check_arg ->
Typed_ast.env ->
Macro_expander.macro_context -> Typed_ast.exp -> Typed_ast.exp option
val compile_def : Target.target ->
match_check_arg -> Typed_ast.env -> Def_trans.def_macro
val is_isabelle_pattern_match : match_check_arg
val is_hol_pattern_match : match_check_arg
val is_coq_pattern_match : match_check_arg
val is_ocaml_pattern_match : match_check_arg
val is_pattern_match_const : bool -> match_check_arg
val check_number_patterns : Typed_ast.env -> Typed_ast.pat -> unit
checked_number_patterns env p
checks that all number patterns which are part of p
are
of type nat or natural.val remove_function : Typed_ast.env ->
(Typed_ast.exp -> Typed_ast.exp) -> Typed_ast.exp -> Typed_ast.exp option
remove_function env case_f e
replaces the function expression e
with with fun x -> match x with ...
.
The function case_f
is then applied to the new match-expression.val remove_fun : Typed_ast.env ->
(Typed_ast.exp -> Typed_ast.exp) -> Typed_ast.exp -> Typed_ast.exp option
remove_fun env case_f e
replaces the fun-expression e
. If e
is of the form fun p0 ... pn -> e'
such that
not all patterns pi
are variable patterns, it is replaced with fun x0 ... xn -> match (x0, ..., xn) with (p0, ..., pn) -> e'
.
The function case_f
is then applied to the new match-expression.val remove_toplevel_match : Target.target ->
match_check_arg -> Typed_ast.env -> Def_trans.def_macro
remove_toplevel_match
tries to introduce matching directly in the function definition by
eliminating match-expressions in the body.val collapse_nested_matches : match_check_arg ->
Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp option
collapse_nested_matches
tries to eliminate nested matches by collapsing them. It is used internally by pattern
compilation.