Lines Matching refs:list
7 {case_const : term, constructors : term list} option
10 (* given a list of rows of patterns, which column to split on? *)
11 col_fun : thry -> term list list -> int }
23 takes the column-number from the provided list of explicit
24 choices. If the list is too short, the first column is
25 chosen. One should run this heuristic first with an empty list
30 val pheu_manual : int list -> pmatch_heuristic
38 and a list of ranking functions prheuL = [r_1, ... r_j]. The
44 val pheu_rank : (thry -> term list -> int) list -> pmatch_heuristic
47 val prheu_first_row : thry -> term list -> int
48 val prheu_constr_prefix : thry -> term list -> int
49 val prheu_small_branching_factor : thry -> term list -> int
50 val prheu_arity : thry -> term list -> int
53 (list of pattern lists, resulting decision tree) *)
54 type pmatch_heuristic_res_compare = (term list list * term) Lib.cmp
75 (* custom pmatch_heuristic_fun can be easiest constructed by an explicit list of heuristics and
77 val pmatch_heuristic_list : pmatch_heuristic_res_compare -> pmatch_heuristic list -> pmatch_heuristic_fun
79 (* A list of useful heuristics to be used with pmatch_heuristic_list *)
80 val default_heuristic_list : pmatch_heuristic list
88 val set_heuristic_list_size : pmatch_heuristic list -> unit
89 val set_heuristic_list_cases : pmatch_heuristic list -> unit
95 val with_manual_heuristic : int list -> ('a -> 'b) -> ('a -> 'b)