src/pattern_matches/patternMatchesLib.sml

993 fun pair_get_col col v = let
995   val (vs', c_v) = replace_element vs col []
1029 val col = 0
1032 fun PMATCH_REMOVE_COL_AUX rc_arg col t = let
1034   val (v', c_v) = pair_get_col col v
1048      val (pt0', pv) = pair_get_col col pt
1074            val _ = if List.all (fn x => List.exists (aconv (#redex x)) vars) sub then () else failwith "not a constant-col after all"
1157 val col = 0
1161 fun PMATCH_REMOVE_FUN_AUX rc_arg col t = let
1166     val c_args = List.nth(vs, col)
1172     val (vars, _) = replace_element vs_vars col args_vars
1173     val (ff_res, _) = replace_element vs_vars col [list_mk_comb (c, args_vars)]
1179       val tt_args = List.nth(tts, col)
1184       val (vars,_) = replace_element tts col args'
1191       val tt_col = List.nth(tts, col)
1199       val (vars, _) = replace_element tts col args
1354   val (col_v, col) = el 1 cols
1355   val (vars, col_pat) = el 3  col
1364   fun elim_col_ok (col_v, col) =
1365     List.all (do_match col_v) col
1367   fun simp_col_ok (col_v, col) = let
1375     List.all check_line col
1378   fun process_col i col = if (elim_col_ok col) then
1380   else if (simp_col_ok col) then
1987 fun colRank_small_branching_factor db : column_ranking_fun = (fn col =>
1988   case col_get_constr_set db col of
1991     | NONE => (~(length (col_get_nonvar_set col) + 2)))
1993 fun colRank_arity db : column_ranking_fun = (fn col =>
1994   case col_get_constr_set db col of
2104     val (v, col) = el (col_no+1) cols
2105     val res = pmatch_compile_db_compile db col
2251     val (v, col) = el (col_no+1) cols
2252     val nchot_thm_opt = pmatch_compile_db_compile_nchotomy db col