1signature PmatchHeuristics = 2sig 3 4 type term = Term.term 5 type thm = Thm.thm 6 type thry = {Thy : string, Tyop : string} -> 7 {case_const : term, constructors : term list} option 8 type pmatch_heuristic = 9 {skip_rows : bool, (* skip splitting for redundant rows? *) 10 collapse_cases : bool, (* collapse cases that lead to same result ? *) 11 (* given a list of rows of patterns, which column to split on? *) 12 col_fun : thry -> term list list -> int} 13 14 (* some predefined heuristics *) 15 val pheu_classic : pmatch_heuristic (* HOL 4's old heuristic *) 16 val pheu_first_row : pmatch_heuristic 17 val pheu_constr_prefix : pmatch_heuristic 18 val pheu_qba : pmatch_heuristic (* the recommended one *) 19 val pheu_cqba : pmatch_heuristic 20 val pheu_first_col : pmatch_heuristic 21 val pheu_last_col : pmatch_heuristic 22 23 (* A manual heuristic. For each decision, it prints the columns and 24 takes the column-number from the provided list of explicit 25 choices. If the list is too short, the first column is 26 chosen. One should run this heuristic first with an empty list 27 as argument. Then look at the choices and add 0s for all the 28 initial choices you liked to be 0 an then a different choice you 29 prefer. Rerun again (because the following choices will change) 30 and iterate. This provided very fine control, but is tedious. *) 31 val pheu_manual : int list -> pmatch_heuristic 32 33 (* A heuristic based on column ranks. Given a pattern match matrix like 34 35 p_11 ... p_1n 36 ... 37 p_m1 --- p_mn 38 39 and a list of ranking functions prheuL = [r_1, ... r_j]. The 40 heuristic pheu_rank applies all ranking functions to all columns. 41 Let's denote the result of "r_i current_thyr [p_k1, ... pkm]" with 42 c_ik. It then picks column i such that [c_1i, ... c_ji] is maximal 43 accroding to the lexicographic ordering of integers. 44 *) 45 val pheu_rank : (thry -> term list -> int) list -> pmatch_heuristic 46 47 (* some ranking functions *) 48 val prheu_first_row : thry -> term list -> int 49 val prheu_constr_prefix : thry -> term list -> int 50 val prheu_small_branching_factor : thry -> term list -> int 51 val prheu_arity : thry -> term list -> int 52 53 (* A comparison for the results of heuristic application 54 (list of pattern lists, resulting decision tree) *) 55 type pmatch_heuristic_res_compare = (term list list * term) Lib.cmp 56 (* few cases are good *) 57 val pmatch_heuristic_cases_cmp : pmatch_heuristic_res_compare 58 59 (* small terms are good *) 60 val pmatch_heuristic_size_cmp : pmatch_heuristic_res_compare 61 62 (* Using such comparisons, we can supply multiple heuristics and 63 choose the best results. For technical reasons, this function 64 might be stateful and therefore get's unit arguments. 65 66 The usage of a heu_fun by the Pmatch library is as follows. 67 Heu_fun initialises the functions and returns a compare function 68 and a function heu_fun' which provides heuristics. As long as 69 heu_fun' () provides fresh heuristics these are tried. Then the 70 best result of all these heuristics according to the compare 71 function is choosen. *) 72 type pmatch_heuristic_fun = 73 unit -> 74 pmatch_heuristic_res_compare * (unit -> pmatch_heuristic option) 75 76 val default_heuristic_fun : pmatch_heuristic_fun 77 val classic_heuristic_fun : pmatch_heuristic_fun 78 79 (* An exhaustive heuristic_fun. It tries all possibilities and very 80 quickly blows up! 81 Only usable for very small examples! *) 82 val exhaustive_heuristic_fun : pmatch_heuristic_res_compare -> 83 pmatch_heuristic_fun 84 85 86 (* custom pmatch_heuristic_fun can be easiest constructed by an 87 explicit list of heuristics and a compare function *) 88 val pmatch_heuristic_list : pmatch_heuristic_res_compare -> 89 pmatch_heuristic list -> pmatch_heuristic_fun 90 91 (* A list of useful heuristics to be used with pmatch_heuristic_list *) 92 val default_heuristic_list : pmatch_heuristic list 93 94 95 (* The pmatch_heuristic_fun to be used by default and various functions 96 to set it *) 97 val pmatch_heuristic : pmatch_heuristic_fun ref 98 99 val set_heuristic : pmatch_heuristic -> unit 100 val set_heuristic_fun : pmatch_heuristic_fun -> unit 101 val set_heuristic_list_size : pmatch_heuristic list -> unit 102 val set_heuristic_list_cases : pmatch_heuristic list -> unit 103 val set_default_heuristic : unit -> unit 104 val set_classic_heuristic : unit -> unit 105 106 val with_classic_heuristic : ('a -> 'b) -> ('a -> 'b) 107 val with_heuristic : pmatch_heuristic -> ('a -> 'b) -> ('a -> 'b) 108 val with_manual_heuristic : int list -> ('a -> 'b) -> ('a -> 'b) 109 val is_classic : unit -> bool 110end 111