src/pattern_matches/patternMatchesLib.sml

991 fun pair_get_col col v = let
993   val (vs', c_v) = replace_element vs col []
1027 val col = 0
1030 fun PMATCH_REMOVE_COL_AUX rc_arg col t = let
1032   val (v', c_v) = pair_get_col col v
1046      val (pt0', pv) = pair_get_col col pt
1072            val _ = if List.all (fn x => List.exists (aconv (#redex x)) vars) sub then () else failwith "not a constant-col after all"
1155 val col = 0
1159 fun PMATCH_REMOVE_FUN_AUX rc_arg col t = let
1164     val c_args = List.nth(vs, col)
1170     val (vars, _) = replace_element vs_vars col args_vars
1171     val (ff_res, _) = replace_element vs_vars col [list_mk_comb (c, args_vars)]
1177       val tt_args = List.nth(tts, col)
1182       val (vars,_) = replace_element tts col args'
1189       val tt_col = List.nth(tts, col)
1197       val (vars, _) = replace_element tts col args
1352   val (col_v, col) = el 1 cols
1353   val (vars, col_pat) = el 3  col
1362   fun elim_col_ok (col_v, col) =
1363     List.all (do_match col_v) col
1365   fun simp_col_ok (col_v, col) = let
1373     List.all check_line col
1376   fun process_col i col = if (elim_col_ok col) then
1378   else if (simp_col_ok col) then
1984 fun colRank_small_branching_factor db : column_ranking_fun = (fn col =>
1985   case col_get_constr_set db col of
1988     | NONE => (~(length (col_get_nonvar_set col) + 2)))
1990 fun colRank_arity db : column_ranking_fun = (fn col =>
1991   case col_get_constr_set db col of
2101     val (v, col) = el (col_no+1) cols
2102     val res = pmatch_compile_db_compile db col
2248     val (v, col) = el (col_no+1) cols
2249     val nchot_thm_opt = pmatch_compile_db_compile_nchotomy db col