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