src/pattern_matches/constrFamiliesLib.sml

520      (* how many rows of the col are not constructor applications
581 fun measure_constructorFamily (cf : constructorFamily) col = let
582   fun list_count p col =
583     foldl (fn (r, c) => if (p r) then c+1 else c) 0 col
604      end handle HOL_ERR _ => false) col)
610     colstat_missed_rows = list_count row_is_missed col,
644 fun lookup_constructorFamily force_exh (db : pmatch_compile_db) col = let
645   val _ = if (List.null col) then (failwith "constructorFamiliesLib" "lookup_constructorFamilies: null col") else ()
647   val _ = if List.all (fn (vs, c) => is_var c andalso tmem c vs) col then
649                       "lookup_constructorFamilies: var col")
652   val ty = type_of (snd (hd col))
660     ((ty, cf), measure_constructorFamily cf col)) cts_fams'
673 fun pmatch_compile_db_compile_aux db col = (
674   if (List.null col) then failwith "pmatch_compile_db_compile" "col 0" else let
675     val fun_res = get_first (fn f => f col handle HOL_ERR _ => NONE) (#pcdb_compile_funs db)
676     val cf_res = lookup_constructorFamily false db col
679       val ty_s = match_type ty (type_of (snd (hd col)))
695 fun pmatch_compile_db_compile db col = (
696   fst (pmatch_compile_db_compile_aux db col))
698 fun pmatch_compile_db_compile_cf db col = (
699   case (snd (pmatch_compile_db_compile_aux db col)) of
705 fun pmatch_compile_db_compile_nchotomy db col = (
706   if (List.null col) then failwith "pmatch_compile_db_compile_cf" "col 0" else
707   case (get_first (fn f => f col handle HOL_ERR _ => NONE) (#pcdb_nchotomy_funs db)) of
709       case (lookup_constructorFamilies true db col) of
714 fun pmatch_compile_db_compile_nchotomy db col = (
715   if (List.null col) then failwith "pmatch_compile_db_compile_nchotomy" "col 0" else let
716     val fun_res = get_first (fn f => f col handle HOL_ERR _ => NONE) (#pcdb_nchotomy_funs db)
717     val cf_res = lookup_constructorFamily true db col
824 fun literals_compile_fun (col:(term list * term) list) = let
839   val (lits_rev, _) = List.foldl extract_literal ([], empty_tmset) col
845   val lit_ty = type_of (snd (List.hd col))
925 fun literals_nchotomy_fun (col:(term list * term) list) = let
934   val ts = List.foldl extract_literal empty_tmset col
939   val lit_ty = type_of (snd (List.hd col))