Lines Matching refs:col
512 (* how many rows of the col are not constructor applications
573 fun measure_constructorFamily (cf : constructorFamily) col = let
574 fun list_count p col =
575 foldl (fn (r, c) => if (p r) then c+1 else c) 0 col
596 end handle HOL_ERR _ => false) col)
602 colstat_missed_rows = list_count row_is_missed col,
636 fun lookup_constructorFamily force_exh (db : pmatch_compile_db) col = let
637 val _ = if (List.null col) then (failwith "constructorFamiliesLib" "lookup_constructorFamilies: null col") else ()
639 val _ = if List.all (fn (vs, c) => is_var c andalso Lib.mem c vs) col then
640 (failwith "constructorFamiliesLib" "lookup_constructorFamilies: var col")
643 val ty = type_of (snd (hd col))
651 ((ty, cf), measure_constructorFamily cf col)) cts_fams'
664 fun pmatch_compile_db_compile_aux db col = (
665 if (List.null col) then failwith "pmatch_compile_db_compile" "col 0" else let
666 val fun_res = get_first (fn f => f col handle HOL_ERR _ => NONE) (#pcdb_compile_funs db)
667 val cf_res = lookup_constructorFamily false db col
670 val ty_s = match_type ty (type_of (snd (hd col)))
686 fun pmatch_compile_db_compile db col = (
687 fst (pmatch_compile_db_compile_aux db col))
689 fun pmatch_compile_db_compile_cf db col = (
690 case (snd (pmatch_compile_db_compile_aux db col)) of
696 fun pmatch_compile_db_compile_nchotomy db col = (
697 if (List.null col) then failwith "pmatch_compile_db_compile_cf" "col 0" else
698 case (get_first (fn f => f col handle HOL_ERR _ => NONE) (#pcdb_nchotomy_funs db)) of
700 case (lookup_constructorFamilies true db col) of
705 fun pmatch_compile_db_compile_nchotomy db col = (
706 if (List.null col) then failwith "pmatch_compile_db_compile_nchotomy" "col 0" else let
707 val fun_res = get_first (fn f => f col handle HOL_ERR _ => NONE) (#pcdb_nchotomy_funs db)
708 val cf_res = lookup_constructorFamily true db col
815 fun literals_compile_fun (col:(term list * term) list) = let
830 val (lits_rev, _) = List.foldl extract_literal ([], empty_tmset) col
836 val lit_ty = type_of (snd (List.hd col))
916 fun literals_nchotomy_fun (col:(term list * term) list) = let
925 val ts = List.foldl extract_literal empty_tmset col
930 val lit_ty = type_of (snd (List.hd col))