src/pattern_matches/constrFamiliesLib.sml

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))