Module Patterns

module Patterns: sig .. end

pattern compilation

Pattern Compilation

type match_props = {

	`is_exhaustive : bool;`
	`missing_pats : Typed_ast.pat list list;`
	`redundant_pats : (int * Typed_ast.pat) list;`
	`overlapping_pats : ((int * Typed_ast.pat) * (int * Typed_ast.pat)) list;`

}

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

Other pattern functions

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.