Lines Matching refs:col
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