From 11e4784fbc9df0758b06e4054225edd10cf19d86 Mon Sep 17 00:00:00 2001 From: Thomas Tuerk Date: Wed, 9 Sep 2015 21:31:59 +0200 Subject: [PATCH] pattern_matches: implement syntactic checks these checks can be used to decide which PMATCH expressions can be used for code-generation. They might also be handy during parsing to print warning messages. --- src/pattern_matches/patternMatchesLib.sig | 96 +++++++++ src/pattern_matches/patternMatchesLib.sml | 239 ++++++++++++++++++++++ 2 files changed, 335 insertions(+) diff --git a/src/pattern_matches/patternMatchesLib.sig b/src/pattern_matches/patternMatchesLib.sig index c942a5ce9a..b5500c2a81 100644 --- a/src/pattern_matches/patternMatchesLib.sig +++ b/src/pattern_matches/patternMatchesLib.sig @@ -150,6 +150,102 @@ sig val PMATCH_TO_TOP_RULE : rule + (*************************************) + (* Analyse PMATCH expressions to *) + (* check whether they can be *) + (* translated to ML or OCAML *) + (*************************************) + + (* Record storing detailed information about a PMATCH *) + type pmatch_info = { + (* Is it a well formed PMATCH, i.e. is it of + the from PMATCH input row_list, where + every row is given explicitly via PMATCH_MATCH_ROW + and is wellformed itself? *) + pmi_is_well_formed : bool, + + (* List of all rows that are not well-formed. + If this list is non-empty, pmi_is_well_formed is false. *) + pmi_ill_formed_rows : int list, + + (* List of rows that have guards *) + pmi_has_guards : int list, + + (* List of rows that contain variables in a pattern that + are not bound by the pattern. These free vars are + returned explicitly. *) + pmi_has_free_pat_vars : (int * term list) list, + + (* List of rows whose patterns bind variables that they + do not use. These unused vars are returned explicitly. *) + pmi_has_unused_pat_vars : (int * term list) list, + + (* List of rows whose patterns use a bound variable + multiple times. These vars are returned explicitly. *) + pmi_has_double_bound_pat_vars : (int * term list) list, + + (* List of rows that uses constants that are neither + literals nor datatype-constructors in + patterns. These constants are returned. *) + pmi_has_non_contr_in_pat : (int * term list) list, + + (* List of rows that use lambda-abstractions in patterns. *) + pmi_has_lambda_in_pat : int list, + + (* Optional information about exhaustiveness. + Checking exhaustiveness is expensive, therefore it + can be skipped. However, if a theorem is stored here, + it is of the form `|- ~(cond) -> exhaustive`. + There are no other guarentees. We don't guarentee that + if the condition holds, the pattern match is inexhaustive. + This is usually the case, put we don't guarentee it. + To check, whether the match is exhaustive, check whether + the guard is T. See below for functions using this + field. + *) + pmi_exhaustiveness_cond : thm option + } + + (* Analyse a PMATCH term and return the result. If + the flag is set to true, an exhaustiveness check is + attempted, if no syntactic checks indicate that this + one would most likely fail. *) + val analyse_pmatch : bool -> term -> pmatch_info + + (* Check whether the PMATCH is syntactically well-formed. *) + val is_well_formed_pmatch : pmatch_info -> bool + + (* Check whethe the PMATCH is falling into the subset + supported by OCAML *) + val is_ocaml_pmatch : pmatch_info -> bool + + (* Check whether the PMATCH is falling into the subset + supported by SML. *) + val is_sml_pmatch : pmatch_info -> bool; + + (* Was it proved that the PMATCH is exhaustive? If + the answer is no, we don't know much. *) + val is_proven_exhaustive_pmatch : pmatch_info -> bool + + (* Get the list of patterns that are possibly missing. + If no exhaustiveness information is available, NONE + is returned. The missing patterns are returns as a list + of triples (`bound-vars`, `pattern`, `guard`) *) + val get_possibly_missing_patterns : pmatch_info -> + (term * term * term) list option + + (** extend_possibly_missing_patterns t pmi + tries to extend the original pattern match t with + rows derived from the exhaustiveness information + from its info. It fails, if no exhaustiveness + information is available. The result should + be an exhaustive match, which is equivalent to + the input `t`. If you need a prove, use + PMATCH_COMPLETE_CONV and similar functions instead + of this syntactic one. *) + val extend_possibly_missing_patterns : term -> pmatch_info -> term + + (********************************) (* CASE SPLIT (pattern compile) *) (********************************) diff --git a/src/pattern_matches/patternMatchesLib.sml b/src/pattern_matches/patternMatchesLib.sml index 187371efd9..0cf5b7d313 100644 --- a/src/pattern_matches/patternMatchesLib.sml +++ b/src/pattern_matches/patternMatchesLib.sml @@ -3042,6 +3042,7 @@ fun PMATCH_COMPLETE_GEN_ss ssl db colHeu use_guards = val PMATCH_COMPLETE_ss = PMATCH_COMPLETE_GEN_ss [] (!thePmatchCompileDB) colHeu_default; + (* @@ -3074,4 +3075,242 @@ val tt = list_mk_disj disjs *) + +(*************************************) +(* Analyse PMATCH expressions to *) +(* check whether they can be *) +(* translated to ML or OCAML *) +(*************************************) + +type pmatch_info = { + pmi_is_well_formed : bool, + pmi_ill_formed_rows : int list, + pmi_has_free_pat_vars : (int * term list) list, + pmi_has_unused_pat_vars : (int * term list) list, + pmi_has_double_bound_pat_vars : (int * term list) list, + pmi_has_guards : int list, + pmi_has_lambda_in_pat : int list, + pmi_has_non_contr_in_pat : (int * term list) list, + pmi_exhaustiveness_cond : thm option +} + +fun is_proven_exhaustive_pmatch (pmi : pmatch_info) = + (case (#pmi_exhaustiveness_cond pmi) of + NONE => false + | SOME thm => let + val (pre, _) = dest_imp_only (concl thm) + in + aconv pre ``~F`` + end handle HOL_ERR _ => false + ) + +fun get_possibly_missing_patterns (pmi : pmatch_info) = + (case (#pmi_exhaustiveness_cond pmi) of + NONE => NONE + | SOME thm => (let + val (pre, _) = dest_imp_only (concl thm) + in if aconv pre ``~F`` then SOME [] else + let + val ps = strip_disj (dest_neg pre) + fun dest_p p = let + val (_, vs, p, g) = dest_PMATCH_ROW_COND_EX_ABS p + in (vs, p, g) end + in + SOME (List.map dest_p ps) + end end) handle HOL_ERR _ => NONE + ) + +fun extend_possibly_missing_patterns t (pmi : pmatch_info) = + case get_possibly_missing_patterns pmi of + NONE => failwith "no missing row info available" + | SOME [] => t + | SOME rs => let + val use_guards = not (null (#pmi_has_guards pmi)) + val arb_t = mk_arb (type_of t) + fun mk_row (v, p, g) = let + val vars = pairSyntax.strip_pair v + in + snd (mk_PMATCH_ROW_PABS_WILDCARDS vars (p, + if use_guards then g else T, arb_t)) + end + val rows = List.map mk_row rs + + val (i, rows_org) = dest_PMATCH t + val rows_t = + listSyntax.mk_list (rows_org @ rows, type_of (hd rows)) + in + mk_PMATCH i rows_t + end; + + +fun is_well_formed_pmatch (pmi : pmatch_info) = + (#pmi_is_well_formed pmi) andalso + (null (#pmi_ill_formed_rows pmi)) andalso + (null (#pmi_has_unused_pat_vars pmi)) andalso + (null (#pmi_has_lambda_in_pat pmi)); + +fun is_ocaml_pmatch (pmi : pmatch_info) = + (is_well_formed_pmatch pmi) andalso + (null (#pmi_has_non_contr_in_pat pmi)) andalso + (null (#pmi_has_free_pat_vars pmi)) andalso + (null (#pmi_has_double_bound_pat_vars pmi)); + +fun is_sml_pmatch (pmi : pmatch_info) = + (is_ocaml_pmatch pmi) andalso + (null (#pmi_has_guards pmi)); + +val init_pmatch_info : pmatch_info = { + pmi_is_well_formed = false, + pmi_ill_formed_rows = [], + pmi_has_free_pat_vars = [], + pmi_has_unused_pat_vars = [], + pmi_has_double_bound_pat_vars = [], + pmi_has_guards = [], + pmi_has_lambda_in_pat = [], + pmi_has_non_contr_in_pat = [], + pmi_exhaustiveness_cond = NONE +} + +fun pmi_genupdate f1 f2 f3 f4 f5 f6 f7 f8 f9 + (pmi : pmatch_info) = ({ + pmi_is_well_formed = f1 (#pmi_is_well_formed pmi), + pmi_ill_formed_rows = f2 (#pmi_ill_formed_rows pmi), + pmi_has_free_pat_vars = f3 (#pmi_has_free_pat_vars pmi), + pmi_has_unused_pat_vars = f4 (#pmi_has_unused_pat_vars pmi), + pmi_has_double_bound_pat_vars = f5 (#pmi_has_double_bound_pat_vars pmi), + pmi_has_guards = f6 (#pmi_has_guards pmi), + pmi_has_lambda_in_pat = f7 (#pmi_has_lambda_in_pat pmi), + pmi_has_non_contr_in_pat = f8 (#pmi_has_non_contr_in_pat pmi), + pmi_exhaustiveness_cond = f9 (#pmi_exhaustiveness_cond pmi) +}:pmatch_info) + +fun pmi_set_is_well_formed x = + pmi_genupdate (K x) I I I I I I I I + +fun pmi_add_ill_formed_row row_no = + pmi_genupdate (K true) (cons row_no) I I I I I I I; + +fun pmi_add_has_free_pat_vars row_no vars = + pmi_genupdate I I (cons (row_no, vars)) I I I I I I; + +fun pmi_add_has_unused_pat_vars row_no vars = + pmi_genupdate I I I (cons (row_no, vars)) I I I I I; + +fun pmi_add_has_double_bound_pat_vars row_no vars = + pmi_genupdate I I I I (cons (row_no, vars)) I I I I; + +fun pmi_add_has_guards row_no = + pmi_genupdate I I I I I (cons row_no) I I I; + +fun pmi_add_has_lambda_in_pat row_no = + pmi_genupdate I I I I I I (cons row_no) I I; + +fun pmi_add_has_non_contr_in_pat row_no terms = + pmi_genupdate I I I I I I I (cons (row_no, terms)) I; + +fun pmi_set_pmi_exhaustiveness_cond thm_opt = + pmi_genupdate I I I I I I I I (K thm_opt); + + +local + + fun analyse_pat (ls : bool (* has lamdbda been seen *), + sv : term set (* set of all seen vars *), + msv : term set (* set of all vars seen more than once *), + sc : term set (* set of all seen constants *)) + t = + if is_var t then let + val (sv, msv) = if HOLset.member (sv, t) then + (sv, HOLset.add (msv, t)) + else + (HOLset.add (sv, t), msv) + in (ls, sv, msv, sc) + end else if (Literal.is_literal t orelse is_const t) then + (ls, sv, msv, HOLset.add (sc,t)) + else if (is_abs t) then + (true, sv, msv, sc) + else if (is_comb t) then let + val (t1, t2) = dest_comb t + val (ls, sv, msv, sc) = analyse_pat (ls, sv, msv, sc) t1 + val (ls, sv, msv, sc) = analyse_pat (ls, sv, msv, sc) t2 + in + (ls, sv, msv, sc) + end + else failwith "UNREACHABLE" + + + fun analyse_row ((row_num, row),pmi) = let + val (p_vars, p_body, g_body, _) = + dest_PMATCH_ROW_ABS row + + (* check guard *) + val pmi = if aconv g_body T then pmi else + pmi_add_has_guards row_num pmi + + (* check pattern *) + val vars_l = pairSyntax.strip_pair p_vars + val vars = HOLset.fromList Term.compare vars_l + val (ls, sv, msv, sc) = analyse_pat (false, + HOLset.empty Term.compare, + HOLset.empty Term.compare, + HOLset.empty Term.compare) p_body + + (* Take care of unit vars *) + val sv = case vars_l of + [v] => if type_of v = oneSyntax.one_ty then + HOLset.add (sv, v) else sv + | _ => sv + + (* check lambda *) + val pmi = if ls then + pmi_add_has_lambda_in_pat row_num pmi + else pmi + + (* check free_vars *) + val fv = HOLset.difference (sv, vars) + val pmi = if HOLset.isEmpty fv then pmi else + (pmi_add_has_free_pat_vars row_num + (HOLset.listItems fv) pmi) + + (* check unused vars *) + val uv = HOLset.difference (vars, sv) + val pmi = if HOLset.isEmpty uv then pmi else + (pmi_add_has_unused_pat_vars row_num + (HOLset.listItems uv) pmi) + + (* check double vars *) + val dv = HOLset.intersection (msv, vars) + val pmi = if HOLset.isEmpty dv then pmi else + (pmi_add_has_double_bound_pat_vars row_num + (HOLset.listItems dv) pmi) + + (* check constructors vars *) + val c_l = HOLset.listItems sc + val nc_l = List.filter (fn c => + not (TypeBase.is_constructor c orelse Literal.is_literal c)) c_l + val pmi = if null nc_l then pmi else + (pmi_add_has_non_contr_in_pat row_num + nc_l pmi) + in + pmi + end + +in + +fun analyse_pmatch try_exh t = let + val (_, rows) = dest_PMATCH t + val nrows = enumerate 0 rows + val pmi = pmi_set_is_well_formed true init_pmatch_info + val pmi = List.foldl analyse_row pmi nrows + + val pmi = (if (try_exh andalso is_ocaml_pmatch pmi) then + pmi_set_pmi_exhaustiveness_cond (SOME (PMATCH_IS_EXHAUSTIVE_CONSEQ_CONV t)) pmi else pmi) handle HOL_ERR _ => pmi + +in + pmi +end handle HOL_ERR _ => init_pmatch_info + +end + + end