src/pattern_matches/patternMatchesLib.sml

1352   val cols = dest_PMATCH_COLS t
1354   val (col_v, col) = el 1 cols
1384   val thm_opt = first_opt process_col cols
1572   fun split_var avoid cols l = let
1580     val types = splits [] (col_no - cols) (type_of l)
1594      val cols = length pts
1596      val _ = if (cols < col_no) then () else failwith "nothing to do"
1602      val new_vars = split_var avoids cols l
1909 val colHeu_last_col : column_heuristic = (fn cols => length cols - 1)
2008 fun colHeu_default cols = colHeu_qba (!thePmatchCompileDB) cols
2102   fun find_col cols = if (List.null cols) then raise UNCHANGED else let
2103     val col_no = col_heu cols
2104     val (v, col) = el (col_no+1) cols
2110              val (cols', _) = replace_element cols col_no []
2111              val (col_no', expand_thm, expand_ss) = find_col cols'
2137   val cols = dest_PMATCH_COLS t'
2138   val col_no = length cols
2247   fun find_nchotomy_for_cols db col_heu cols = let
2248     val _ = if (List.null cols) then
2250     val col_no = col_heu cols
2251     val (v, col) = el (col_no+1) cols
2257         val (cols', _) = replace_element cols col_no []
2259         find_nchotomy_for_cols db col_heu cols'
2269     val cols = dest_PATLIST_COLS initial_value pats
2279     (initial_thm, cols, lbl)
2377   fun get_columns_for_constructor current_col (c, evs) cols' = let
2399        (v, List.map snd (Lib.filter fst (zip kl rs)))) cols'
2401     val cols'' = cols1 @ cols2
2403     (* remove cols consisting of only vars *)
2404     val cols''' = filter (fn (_, ps) => not (List.all (fn (vs, p) =>    is_var p andalso List.exists (aconv p) vs) ps)) cols''
2406      cols'''
2411   fun pick_current_column v cols =
2412     pick_element (fn (v', _) => aconv v v') cols
2421       val (thm, cols, lbl) = mk_initial_state var_gen lbl_gen pats
2422       val (thm, cols, lbl) = (thm1, cols'', lbl)
2424       val (thm, cols, lbl) = el 3 xxx
2427     fun compile (thm, cols, lbl) = let
2428       val (v, nthm) = find_nchotomy_for_cols db col_heu cols
2429       val (current_col, cols_rest) = pick_current_column v cols
2439           val cols' = get_columns_for_constructor current_col (c, evs) cols_rest
2441           compile (current_thm, cols', lbl)