1.1 --- a/doc-src/Nitpick/nitpick.tex Thu Feb 25 10:08:44 2010 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Thu Feb 25 16:33:39 2010 +0100
1.3 @@ -472,7 +472,7 @@
1.4 \prew
1.5 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
1.6 \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
1.7 -\slshape Warning: The conjecture either trivially holds for the given scopes or (more likely) lies outside Nitpick's supported
1.8 +\slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
1.9 fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
1.10 Nitpick found a potential counterexample: \\[2\smallskipamount]
1.11 \hbox{}\qquad Free variable: \nopagebreak \\
2.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Feb 25 10:08:44 2010 +0100
2.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Feb 25 16:33:39 2010 +0100
2.3 @@ -30,8 +30,7 @@
2.4 special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
2.5 wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
2.6 (* term -> bool *)
2.7 -val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a}
2.8 - Nitpick_Mono.Plus [] []
2.9 +val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} [] []
2.10 fun is_const t =
2.11 let val T = fastype_of t in
2.12 is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
3.1 --- a/src/HOL/Tools/Nitpick/HISTORY Thu Feb 25 10:08:44 2010 +0100
3.2 +++ b/src/HOL/Tools/Nitpick/HISTORY Thu Feb 25 16:33:39 2010 +0100
3.3 @@ -5,6 +5,8 @@
3.4 * Added support for quotient types
3.5 * Added support for local definitions
3.6 * Optimized "Multiset.multiset"
3.7 + * Improved precision of infinite datatypes whose constructors don't appear
3.8 + in the formula to falsify based on a monotonicity analysis
3.9 * Fixed soundness bugs related to "destroy_constrs" optimization and record
3.10 getters
3.11 * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
4.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 25 10:08:44 2010 +0100
4.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 25 16:33:39 2010 +0100
4.3 @@ -332,21 +332,36 @@
4.4 *)
4.5
4.6 val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
4.7 + (* typ list -> string -> string *)
4.8 + fun monotonicity_message Ts extra =
4.9 + let val ss = map (quote o string_for_type ctxt) Ts in
4.10 + "The type" ^ plural_s_for_list ss ^ " " ^
4.11 + space_implode " " (serial_commas "and" ss) ^ " " ^
4.12 + (if none_true monos then
4.13 + "passed the monotonicity test"
4.14 + else
4.15 + (if length ss = 1 then "is" else "are") ^ " considered monotonic") ^
4.16 + ". " ^ extra
4.17 + end
4.18 (* typ -> bool *)
4.19 fun is_type_always_monotonic T =
4.20 (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
4.21 (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
4.22 is_number_type thy T orelse is_bit_type T
4.23 + fun is_type_actually_monotonic T =
4.24 + formulas_monotonic hol_ctxt binarize T (def_ts, nondef_ts, core_t)
4.25 fun is_type_monotonic T =
4.26 unique_scope orelse
4.27 case triple_lookup (type_match thy) monos T of
4.28 SOME (SOME b) => b
4.29 - | _ => is_type_always_monotonic T orelse
4.30 - formulas_monotonic hol_ctxt binarize T (def_ts, nondef_ts, core_t)
4.31 - fun is_deep_datatype T =
4.32 - is_datatype thy stds T andalso
4.33 - (not standard orelse T = nat_T orelse is_word_type T orelse
4.34 - exists (curry (op =) T o domain_type o type_of) sel_names)
4.35 + | _ => is_type_always_monotonic T orelse is_type_actually_monotonic T
4.36 + fun is_type_finitizable T =
4.37 + case triple_lookup (type_match thy) monos T of
4.38 + SOME (SOME false) => false
4.39 + | _ => is_type_actually_monotonic T
4.40 + fun is_datatype_deep T =
4.41 + not standard orelse T = nat_T orelse is_word_type T orelse
4.42 + exists (curry (op =) T o domain_type o type_of) sel_names
4.43 val all_Ts = ground_types_in_terms hol_ctxt binarize
4.44 (core_t :: def_ts @ nondef_ts)
4.45 |> sort TermOrd.typ_ord
4.46 @@ -363,23 +378,21 @@
4.47 case filter_out is_type_always_monotonic mono_Ts of
4.48 [] => ()
4.49 | interesting_mono_Ts =>
4.50 - print_v (fn () =>
4.51 - let
4.52 - val ss = map (quote o string_for_type ctxt)
4.53 - interesting_mono_Ts
4.54 - in
4.55 - "The type" ^ plural_s_for_list ss ^ " " ^
4.56 - space_implode " " (serial_commas "and" ss) ^ " " ^
4.57 - (if none_true monos then
4.58 - "passed the monotonicity test"
4.59 - else
4.60 - (if length ss = 1 then "is" else "are") ^
4.61 - " considered monotonic") ^
4.62 - ". Nitpick might be able to skip some scopes."
4.63 - end)
4.64 + print_v (K (monotonicity_message interesting_mono_Ts
4.65 + "Nitpick might be able to skip some scopes."))
4.66 else
4.67 ()
4.68 - val deep_dataTs = filter is_deep_datatype all_Ts
4.69 + val (deep_dataTs, shallow_dataTs) =
4.70 + all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
4.71 + val finitizable_dataTs =
4.72 + shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
4.73 + |> filter is_type_finitizable
4.74 + val _ =
4.75 + if verbose andalso not (null finitizable_dataTs) then
4.76 + print_v (K (monotonicity_message finitizable_dataTs
4.77 + "Nitpick can use a more precise finite encoding."))
4.78 + else
4.79 + ()
4.80 (* This detection code is an ugly hack. Fortunately, it is used only to
4.81 provide a hint to the user. *)
4.82 (* string * (Rule_Cases.T * bool) -> bool *)
4.83 @@ -446,7 +459,7 @@
4.84 string_of_int j0))
4.85 (Typtab.dest ofs)
4.86 *)
4.87 - val all_exact = forall (is_exact_type datatypes) all_Ts
4.88 + val all_exact = forall (is_exact_type datatypes true) all_Ts
4.89 (* nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
4.90 val repify_consts = choose_reps_for_consts scope all_exact
4.91 val main_j0 = offset_of_type ofs bool_T
4.92 @@ -907,6 +920,7 @@
4.93 val (skipped, the_scopes) =
4.94 all_scopes hol_ctxt binarize sym_break cards_assigns maxes_assigns
4.95 iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
4.96 + finitizable_dataTs
4.97 val _ = if skipped > 0 then
4.98 print_m (fn () => "Too many scopes. Skipping " ^
4.99 string_of_int skipped ^ " scope" ^
5.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 25 10:08:44 2010 +0100
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 25 16:33:39 2010 +0100
5.3 @@ -151,7 +151,7 @@
5.4 val card_of_type : (typ * int) list -> typ -> int
5.5 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
5.6 val bounded_exact_card_of_type :
5.7 - hol_context -> int -> int -> (typ * int) list -> typ -> int
5.8 + hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
5.9 val is_finite_type : hol_context -> typ -> bool
5.10 val special_bounds : term list -> (indexname * typ) list
5.11 val is_funky_typedef : theory -> typ -> bool
5.12 @@ -1047,13 +1047,16 @@
5.13 card_of_type assigns T
5.14 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
5.15 default_card)
5.16 -(* hol_context -> int -> (typ * int) list -> typ -> int *)
5.17 -fun bounded_exact_card_of_type hol_ctxt max default_card assigns T =
5.18 +(* hol_context -> typ list -> int -> (typ * int) list -> typ -> int *)
5.19 +fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
5.20 + assigns T =
5.21 let
5.22 (* typ list -> typ -> int *)
5.23 fun aux avoid T =
5.24 (if member (op =) avoid T then
5.25 0
5.26 + else if member (op =) finitizable_dataTs T then
5.27 + raise SAME ()
5.28 else case T of
5.29 Type ("fun", [T1, T2]) =>
5.30 let
5.31 @@ -1097,7 +1100,7 @@
5.32
5.33 (* hol_context -> typ -> bool *)
5.34 fun is_finite_type hol_ctxt T =
5.35 - bounded_exact_card_of_type hol_ctxt 1 2 [] T <> 0
5.36 + bounded_exact_card_of_type hol_ctxt [] 1 2 [] T <> 0
5.37
5.38 (* term -> bool *)
5.39 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
6.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 25 10:08:44 2010 +0100
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 25 16:33:39 2010 +0100
6.3 @@ -255,10 +255,10 @@
6.4 ("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div)
6.5 else if x = nat_less_rel then
6.6 ("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0)
6.7 - (int_for_bool o op <))
6.8 + (int_from_bool o op <))
6.9 else if x = int_less_rel then
6.10 ("int_less", tabulate_int_op2 debug univ_card (int_card, j0)
6.11 - (int_for_bool o op <))
6.12 + (int_from_bool o op <))
6.13 else if x = gcd_rel then
6.14 ("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd)
6.15 else if x = lcm_rel then
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Feb 25 10:08:44 2010 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Feb 25 16:33:39 2010 +0100
7.3 @@ -288,7 +288,7 @@
7.4 T1 --> (T1 --> T2) --> T1 --> T2)
7.5 (* (term * term) list -> term *)
7.6 fun aux [] =
7.7 - if maybe_opt andalso not (is_complete_type datatypes T1) then
7.8 + if maybe_opt andalso not (is_complete_type datatypes false T1) then
7.9 insert_const $ Const (unrep, T1) $ empty_const
7.10 else
7.11 empty_const
7.12 @@ -312,7 +312,7 @@
7.13 Const (@{const_name None}, _) => aux' ps
7.14 | _ => update_const $ aux' ps $ t1 $ t2)
7.15 fun aux ps =
7.16 - if not (is_complete_type datatypes T1) then
7.17 + if not (is_complete_type datatypes false T1) then
7.18 update_const $ aux' ps $ Const (unrep, T1)
7.19 $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
7.20 else
7.21 @@ -537,7 +537,7 @@
7.22 val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
7.23 val ts2 =
7.24 map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
7.25 - [[int_for_bool (member (op =) jss js)]])
7.26 + [[int_from_bool (member (op =) jss js)]])
7.27 jss1
7.28 in make_fun false T1 T2 T' ts1 ts2 end
7.29 | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
7.30 @@ -707,12 +707,13 @@
7.31 Pretty.str "=",
7.32 Pretty.enum "," "{" "}"
7.33 (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
7.34 - (if complete then [] else [Pretty.str unrep]))])
7.35 + (if fun_from_pair complete false then []
7.36 + else [Pretty.str unrep]))])
7.37 (* typ -> dtype_spec list *)
7.38 fun integer_datatype T =
7.39 [{typ = T, card = card_of_type card_assigns T, co = false,
7.40 - standard = true, complete = false, concrete = true, deep = true,
7.41 - constrs = []}]
7.42 + standard = true, complete = (false, false), concrete = (true, true),
7.43 + deep = true, constrs = []}]
7.44 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
7.45 val (codatatypes, datatypes) =
7.46 datatypes |> filter #deep |> List.partition #co
8.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 25 10:08:44 2010 +0100
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 25 16:33:39 2010 +0100
8.3 @@ -26,22 +26,27 @@
8.4
8.5 type literal = var * sign
8.6
8.7 -datatype ctype =
8.8 - CAlpha |
8.9 - CFun of ctype * sign_atom * ctype |
8.10 - CPair of ctype * ctype |
8.11 - CType of string * ctype list |
8.12 - CRec of string * typ list
8.13 +datatype mtyp =
8.14 + MAlpha |
8.15 + MFun of mtyp * sign_atom * mtyp |
8.16 + MPair of mtyp * mtyp |
8.17 + MType of string * mtyp list |
8.18 + MRec of string * typ list
8.19
8.20 -type cdata =
8.21 +datatype mterm =
8.22 + MAtom of term * mtyp |
8.23 + MAbs of string * typ * mtyp * sign_atom * mterm |
8.24 + MApp of mterm * mterm
8.25 +
8.26 +type mdata =
8.27 {hol_ctxt: hol_context,
8.28 binarize: bool,
8.29 alpha_T: typ,
8.30 max_fresh: int Unsynchronized.ref,
8.31 - datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
8.32 - constr_cache: (styp * ctype) list Unsynchronized.ref}
8.33 + datatype_cache: ((string * typ list) * mtyp) list Unsynchronized.ref,
8.34 + constr_cache: (styp * mtyp) list Unsynchronized.ref}
8.35
8.36 -exception CTYPE of string * ctype list
8.37 +exception MTYPE of string * mtyp list
8.38
8.39 (* string -> unit *)
8.40 fun print_g (_ : string) = ()
8.41 @@ -70,55 +75,92 @@
8.42 (* literal -> string *)
8.43 fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
8.44
8.45 -val bool_C = CType (@{type_name bool}, [])
8.46 +val bool_M = MType (@{type_name bool}, [])
8.47 +val irrelevant_M = MType (nitpick_prefix ^ "irrelevant", [])
8.48
8.49 -(* ctype -> bool *)
8.50 -fun is_CRec (CRec _) = true
8.51 - | is_CRec _ = false
8.52 +(* mtyp -> bool *)
8.53 +fun is_MRec (MRec _) = true
8.54 + | is_MRec _ = false
8.55 +(* mtyp -> mtyp * sign_atom * mtyp *)
8.56 +fun dest_MFun (MFun z) = z
8.57 + | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M])
8.58
8.59 val no_prec = 100
8.60 -val prec_CFun = 1
8.61 -val prec_CPair = 2
8.62
8.63 -(* tuple_set -> int *)
8.64 -fun precedence_of_ctype (CFun _) = prec_CFun
8.65 - | precedence_of_ctype (CPair _) = prec_CPair
8.66 - | precedence_of_ctype _ = no_prec
8.67 +(* mtyp -> int *)
8.68 +fun precedence_of_mtype (MFun _) = 1
8.69 + | precedence_of_mtype (MPair _) = 2
8.70 + | precedence_of_mtype _ = no_prec
8.71
8.72 -(* ctype -> string *)
8.73 -val string_for_ctype =
8.74 +(* mtyp -> string *)
8.75 +val string_for_mtype =
8.76 let
8.77 - (* int -> ctype -> string *)
8.78 - fun aux outer_prec C =
8.79 + (* int -> mtyp -> string *)
8.80 + fun aux outer_prec M =
8.81 let
8.82 - val prec = precedence_of_ctype C
8.83 + val prec = precedence_of_mtype M
8.84 val need_parens = (prec < outer_prec)
8.85 in
8.86 (if need_parens then "(" else "") ^
8.87 - (case C of
8.88 - CAlpha => "\<alpha>"
8.89 - | CFun (C1, a, C2) =>
8.90 - aux (prec + 1) C1 ^ " \<Rightarrow>\<^bsup>" ^
8.91 - string_for_sign_atom a ^ "\<^esup> " ^ aux prec C2
8.92 - | CPair (C1, C2) => aux (prec + 1) C1 ^ " \<times> " ^ aux prec C2
8.93 - | CType (s, []) =>
8.94 + (case M of
8.95 + MAlpha => "\<alpha>"
8.96 + | MFun (M1, a, M2) =>
8.97 + aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
8.98 + string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
8.99 + | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
8.100 + | MType (s, []) =>
8.101 if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s
8.102 - | CType (s, Cs) => "(" ^ commas (map (aux 0) Cs) ^ ") " ^ s
8.103 - | CRec (s, _) => "[" ^ s ^ "]") ^
8.104 + | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
8.105 + | MRec (s, _) => "[" ^ s ^ "]") ^
8.106 (if need_parens then ")" else "")
8.107 end
8.108 in aux 0 end
8.109
8.110 -(* ctype -> ctype list *)
8.111 -fun flatten_ctype (CPair (C1, C2)) = maps flatten_ctype [C1, C2]
8.112 - | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
8.113 - | flatten_ctype C = [C]
8.114 +(* mtyp -> mtyp list *)
8.115 +fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2]
8.116 + | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
8.117 + | flatten_mtype M = [M]
8.118
8.119 -(* hol_context -> bool -> typ -> cdata *)
8.120 -fun initial_cdata hol_ctxt binarize alpha_T =
8.121 +(* mterm -> bool *)
8.122 +fun precedence_of_mterm (MAtom _) = no_prec
8.123 + | precedence_of_mterm (MAbs _) = 1
8.124 + | precedence_of_mterm (MApp _) = 2
8.125 +
8.126 +(* Proof.context -> mterm -> string *)
8.127 +fun string_for_mterm ctxt =
8.128 + let
8.129 + (* mtype -> string *)
8.130 + fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
8.131 + (* int -> mterm -> string *)
8.132 + fun aux outer_prec m =
8.133 + let
8.134 + val prec = precedence_of_mterm m
8.135 + val need_parens = (prec < outer_prec)
8.136 + in
8.137 + (if need_parens then "(" else "") ^
8.138 + (case m of
8.139 + MAtom (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
8.140 + | MAbs (s, _, M, a, m) =>
8.141 + "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
8.142 + string_for_sign_atom a ^ "\<^esup> " ^ aux prec m
8.143 + | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
8.144 + (if need_parens then ")" else "")
8.145 + end
8.146 + in aux 0 end
8.147 +
8.148 +(* mterm -> mtyp *)
8.149 +fun mtype_of_mterm (MAtom (_, M)) = M
8.150 + | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
8.151 + | mtype_of_mterm (MApp (m1, _)) =
8.152 + case mtype_of_mterm m1 of
8.153 + MFun (_, _, M12) => M12
8.154 + | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1])
8.155 +
8.156 +(* hol_context -> bool -> typ -> mdata *)
8.157 +fun initial_mdata hol_ctxt binarize alpha_T =
8.158 ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
8.159 max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [],
8.160 - constr_cache = Unsynchronized.ref []} : cdata)
8.161 + constr_cache = Unsynchronized.ref []} : mdata)
8.162
8.163 (* typ -> typ -> bool *)
8.164 fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
8.165 @@ -126,177 +168,179 @@
8.166 exists (could_exist_alpha_subtype alpha_T) Ts)
8.167 | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
8.168 (* theory -> typ -> typ -> bool *)
8.169 -fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
8.170 +fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
8.171 could_exist_alpha_subtype alpha_T T
8.172 - | could_exist_alpha_sub_ctype thy alpha_T T =
8.173 + | could_exist_alpha_sub_mtype thy alpha_T T =
8.174 (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
8.175
8.176 -(* ctype -> bool *)
8.177 -fun exists_alpha_sub_ctype CAlpha = true
8.178 - | exists_alpha_sub_ctype (CFun (C1, _, C2)) =
8.179 - exists exists_alpha_sub_ctype [C1, C2]
8.180 - | exists_alpha_sub_ctype (CPair (C1, C2)) =
8.181 - exists exists_alpha_sub_ctype [C1, C2]
8.182 - | exists_alpha_sub_ctype (CType (_, Cs)) = exists exists_alpha_sub_ctype Cs
8.183 - | exists_alpha_sub_ctype (CRec _) = true
8.184 +(* mtyp -> bool *)
8.185 +fun exists_alpha_sub_mtype MAlpha = true
8.186 + | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
8.187 + exists exists_alpha_sub_mtype [M1, M2]
8.188 + | exists_alpha_sub_mtype (MPair (M1, M2)) =
8.189 + exists exists_alpha_sub_mtype [M1, M2]
8.190 + | exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms
8.191 + | exists_alpha_sub_mtype (MRec _) = true
8.192
8.193 -(* ctype -> bool *)
8.194 -fun exists_alpha_sub_ctype_fresh CAlpha = true
8.195 - | exists_alpha_sub_ctype_fresh (CFun (_, V _, _)) = true
8.196 - | exists_alpha_sub_ctype_fresh (CFun (_, _, C2)) =
8.197 - exists_alpha_sub_ctype_fresh C2
8.198 - | exists_alpha_sub_ctype_fresh (CPair (C1, C2)) =
8.199 - exists exists_alpha_sub_ctype_fresh [C1, C2]
8.200 - | exists_alpha_sub_ctype_fresh (CType (_, Cs)) =
8.201 - exists exists_alpha_sub_ctype_fresh Cs
8.202 - | exists_alpha_sub_ctype_fresh (CRec _) = true
8.203 +(* mtyp -> bool *)
8.204 +fun exists_alpha_sub_mtype_fresh MAlpha = true
8.205 + | exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true
8.206 + | exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) =
8.207 + exists_alpha_sub_mtype_fresh M2
8.208 + | exists_alpha_sub_mtype_fresh (MPair (M1, M2)) =
8.209 + exists exists_alpha_sub_mtype_fresh [M1, M2]
8.210 + | exists_alpha_sub_mtype_fresh (MType (_, Ms)) =
8.211 + exists exists_alpha_sub_mtype_fresh Ms
8.212 + | exists_alpha_sub_mtype_fresh (MRec _) = true
8.213
8.214 -(* string * typ list -> ctype list -> ctype *)
8.215 -fun constr_ctype_for_binders z Cs =
8.216 - fold_rev (fn C => curry3 CFun C (S Minus)) Cs (CRec z)
8.217 +(* string * typ list -> mtyp list -> mtyp *)
8.218 +fun constr_mtype_for_binders z Ms =
8.219 + fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z)
8.220
8.221 -(* ((string * typ list) * ctype) list -> ctype list -> ctype -> ctype *)
8.222 -fun repair_ctype _ _ CAlpha = CAlpha
8.223 - | repair_ctype cache seen (CFun (C1, a, C2)) =
8.224 - CFun (repair_ctype cache seen C1, a, repair_ctype cache seen C2)
8.225 - | repair_ctype cache seen (CPair Cp) =
8.226 - CPair (pairself (repair_ctype cache seen) Cp)
8.227 - | repair_ctype cache seen (CType (s, Cs)) =
8.228 - CType (s, maps (flatten_ctype o repair_ctype cache seen) Cs)
8.229 - | repair_ctype cache seen (CRec (z as (s, _))) =
8.230 +(* ((string * typ list) * mtyp) list -> mtyp list -> mtyp -> mtyp *)
8.231 +fun repair_mtype _ _ MAlpha = MAlpha
8.232 + | repair_mtype cache seen (MFun (M1, a, M2)) =
8.233 + MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2)
8.234 + | repair_mtype cache seen (MPair Mp) =
8.235 + MPair (pairself (repair_mtype cache seen) Mp)
8.236 + | repair_mtype cache seen (MType (s, Ms)) =
8.237 + MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms)
8.238 + | repair_mtype cache seen (MRec (z as (s, _))) =
8.239 case AList.lookup (op =) cache z |> the of
8.240 - CRec _ => CType (s, [])
8.241 - | C => if member (op =) seen C then CType (s, [])
8.242 - else repair_ctype cache (C :: seen) C
8.243 + MRec _ => MType (s, [])
8.244 + | M => if member (op =) seen M then MType (s, [])
8.245 + else repair_mtype cache (M :: seen) M
8.246
8.247 -(* ((string * typ list) * ctype) list Unsynchronized.ref -> unit *)
8.248 +(* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *)
8.249 fun repair_datatype_cache cache =
8.250 let
8.251 - (* (string * typ list) * ctype -> unit *)
8.252 - fun repair_one (z, C) =
8.253 + (* (string * typ list) * mtyp -> unit *)
8.254 + fun repair_one (z, M) =
8.255 Unsynchronized.change cache
8.256 - (AList.update (op =) (z, repair_ctype (!cache) [] C))
8.257 + (AList.update (op =) (z, repair_mtype (!cache) [] M))
8.258 in List.app repair_one (rev (!cache)) end
8.259
8.260 -(* (typ * ctype) list -> (styp * ctype) list Unsynchronized.ref -> unit *)
8.261 +(* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *)
8.262 fun repair_constr_cache dtype_cache constr_cache =
8.263 let
8.264 - (* styp * ctype -> unit *)
8.265 - fun repair_one (x, C) =
8.266 + (* styp * mtyp -> unit *)
8.267 + fun repair_one (x, M) =
8.268 Unsynchronized.change constr_cache
8.269 - (AList.update (op =) (x, repair_ctype dtype_cache [] C))
8.270 + (AList.update (op =) (x, repair_mtype dtype_cache [] M))
8.271 in List.app repair_one (!constr_cache) end
8.272
8.273 -(* cdata -> typ -> ctype *)
8.274 -fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, binarize, alpha_T, max_fresh,
8.275 - datatype_cache, constr_cache, ...} : cdata) =
8.276 +(* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *)
8.277 +fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 =
8.278 let
8.279 - (* typ -> typ -> ctype *)
8.280 - fun do_fun T1 T2 =
8.281 - let
8.282 - val C1 = do_type T1
8.283 - val C2 = do_type T2
8.284 - val a = if is_boolean_type (body_type T2) andalso
8.285 - exists_alpha_sub_ctype_fresh C1 then
8.286 - V (Unsynchronized.inc max_fresh)
8.287 - else
8.288 - S Minus
8.289 - in CFun (C1, a, C2) end
8.290 - (* typ -> ctype *)
8.291 - and do_type T =
8.292 + val M1 = fresh_mtype_for_type mdata T1
8.293 + val M2 = fresh_mtype_for_type mdata T2
8.294 + val a = if is_boolean_type (body_type T2) andalso
8.295 + exists_alpha_sub_mtype_fresh M1 then
8.296 + V (Unsynchronized.inc max_fresh)
8.297 + else
8.298 + S Minus
8.299 + in (M1, a, M2) end
8.300 +(* mdata -> typ -> mtyp *)
8.301 +and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
8.302 + datatype_cache, constr_cache, ...}) =
8.303 + let
8.304 + (* typ -> typ -> mtyp *)
8.305 + val do_fun = MFun oo fresh_mfun_for_fun_type mdata
8.306 + (* typ -> mtyp *)
8.307 + fun do_type T =
8.308 if T = alpha_T then
8.309 - CAlpha
8.310 + MAlpha
8.311 else case T of
8.312 Type ("fun", [T1, T2]) => do_fun T1 T2
8.313 | Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2
8.314 - | Type ("*", [T1, T2]) => CPair (pairself do_type (T1, T2))
8.315 + | Type ("*", [T1, T2]) => MPair (pairself do_type (T1, T2))
8.316 | Type (z as (s, _)) =>
8.317 - if could_exist_alpha_sub_ctype thy alpha_T T then
8.318 + if could_exist_alpha_sub_mtype thy alpha_T T then
8.319 case AList.lookup (op =) (!datatype_cache) z of
8.320 - SOME C => C
8.321 + SOME M => M
8.322 | NONE =>
8.323 let
8.324 - val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
8.325 + val _ = Unsynchronized.change datatype_cache (cons (z, MRec z))
8.326 val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
8.327 - val (all_Cs, constr_Cs) =
8.328 - fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
8.329 + val (all_Ms, constr_Ms) =
8.330 + fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
8.331 let
8.332 - val binder_Cs = map do_type (binder_types T')
8.333 - val new_Cs = filter exists_alpha_sub_ctype_fresh
8.334 - binder_Cs
8.335 - val constr_C = constr_ctype_for_binders z
8.336 - binder_Cs
8.337 + val binder_Ms = map do_type (binder_types T')
8.338 + val new_Ms = filter exists_alpha_sub_mtype_fresh
8.339 + binder_Ms
8.340 + val constr_M = constr_mtype_for_binders z
8.341 + binder_Ms
8.342 in
8.343 - (union (op =) new_Cs all_Cs,
8.344 - constr_C :: constr_Cs)
8.345 + (union (op =) new_Ms all_Ms,
8.346 + constr_M :: constr_Ms)
8.347 end)
8.348 xs ([], [])
8.349 - val C = CType (s, all_Cs)
8.350 + val M = MType (s, all_Ms)
8.351 val _ = Unsynchronized.change datatype_cache
8.352 - (AList.update (op =) (z, C))
8.353 + (AList.update (op =) (z, M))
8.354 val _ = Unsynchronized.change constr_cache
8.355 - (append (xs ~~ constr_Cs))
8.356 + (append (xs ~~ constr_Ms))
8.357 in
8.358 - if forall (not o is_CRec o snd) (!datatype_cache) then
8.359 + if forall (not o is_MRec o snd) (!datatype_cache) then
8.360 (repair_datatype_cache datatype_cache;
8.361 repair_constr_cache (!datatype_cache) constr_cache;
8.362 AList.lookup (op =) (!datatype_cache) z |> the)
8.363 else
8.364 - C
8.365 + M
8.366 end
8.367 else
8.368 - CType (s, [])
8.369 - | _ => CType (Refute.string_of_typ T, [])
8.370 + MType (s, [])
8.371 + | _ => MType (Refute.string_of_typ T, [])
8.372 in do_type end
8.373
8.374 -(* ctype -> ctype list *)
8.375 -fun prodC_factors (CPair (C1, C2)) = maps prodC_factors [C1, C2]
8.376 - | prodC_factors C = [C]
8.377 -(* ctype -> ctype list * ctype *)
8.378 -fun curried_strip_ctype (CFun (C1, S Minus, C2)) =
8.379 - curried_strip_ctype C2 |>> append (prodC_factors C1)
8.380 - | curried_strip_ctype C = ([], C)
8.381 -(* string -> ctype -> ctype *)
8.382 -fun sel_ctype_from_constr_ctype s C =
8.383 - let val (arg_Cs, dataC) = curried_strip_ctype C in
8.384 - CFun (dataC, S Minus,
8.385 - case sel_no_from_name s of ~1 => bool_C | n => nth arg_Cs n)
8.386 +(* mtyp -> mtyp list *)
8.387 +fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
8.388 + | prodM_factors M = [M]
8.389 +(* mtyp -> mtyp list * mtyp *)
8.390 +fun curried_strip_mtype (MFun (M1, S Minus, M2)) =
8.391 + curried_strip_mtype M2 |>> append (prodM_factors M1)
8.392 + | curried_strip_mtype M = ([], M)
8.393 +(* string -> mtyp -> mtyp *)
8.394 +fun sel_mtype_from_constr_mtype s M =
8.395 + let val (arg_Ms, dataM) = curried_strip_mtype M in
8.396 + MFun (dataM, S Minus,
8.397 + case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
8.398 end
8.399
8.400 -(* cdata -> styp -> ctype *)
8.401 -fun ctype_for_constr (cdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
8.402 +(* mdata -> styp -> mtyp *)
8.403 +fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
8.404 ...}) (x as (_, T)) =
8.405 - if could_exist_alpha_sub_ctype thy alpha_T T then
8.406 + if could_exist_alpha_sub_mtype thy alpha_T T then
8.407 case AList.lookup (op =) (!constr_cache) x of
8.408 - SOME C => C
8.409 + SOME M => M
8.410 | NONE => if T = alpha_T then
8.411 - let val C = fresh_ctype_for_type cdata T in
8.412 - (Unsynchronized.change constr_cache (cons (x, C)); C)
8.413 + let val M = fresh_mtype_for_type mdata T in
8.414 + (Unsynchronized.change constr_cache (cons (x, M)); M)
8.415 end
8.416 else
8.417 - (fresh_ctype_for_type cdata (body_type T);
8.418 + (fresh_mtype_for_type mdata (body_type T);
8.419 AList.lookup (op =) (!constr_cache) x |> the)
8.420 else
8.421 - fresh_ctype_for_type cdata T
8.422 -fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
8.423 + fresh_mtype_for_type mdata T
8.424 +fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
8.425 x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
8.426 - |> ctype_for_constr cdata |> sel_ctype_from_constr_ctype s
8.427 + |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
8.428
8.429 -(* literal list -> ctype -> ctype *)
8.430 -fun instantiate_ctype lits =
8.431 +(* literal list -> mtyp -> mtyp *)
8.432 +fun instantiate_mtype lits =
8.433 let
8.434 - (* ctype -> ctype *)
8.435 - fun aux CAlpha = CAlpha
8.436 - | aux (CFun (C1, V x, C2)) =
8.437 + (* mtyp -> mtyp *)
8.438 + fun aux MAlpha = MAlpha
8.439 + | aux (MFun (M1, V x, M2)) =
8.440 let
8.441 val a = case AList.lookup (op =) lits x of
8.442 SOME sn => S sn
8.443 | NONE => V x
8.444 - in CFun (aux C1, a, aux C2) end
8.445 - | aux (CFun (C1, a, C2)) = CFun (aux C1, a, aux C2)
8.446 - | aux (CPair Cp) = CPair (pairself aux Cp)
8.447 - | aux (CType (s, Cs)) = CType (s, map aux Cs)
8.448 - | aux (CRec z) = CRec z
8.449 + in MFun (aux M1, a, aux M2) end
8.450 + | aux (MFun (M1, a, M2)) = MFun (aux M1, a, aux M2)
8.451 + | aux (MPair Mp) = MPair (pairself aux Mp)
8.452 + | aux (MType (s, Ms)) = MType (s, map aux Ms)
8.453 + | aux (MRec z) = MRec z
8.454 in aux end
8.455
8.456 datatype comp_op = Eq | Leq
8.457 @@ -346,98 +390,98 @@
8.458 | do_sign_atom_comp cmp xs a1 a2 (lits, comps) =
8.459 SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
8.460
8.461 -(* comp -> var list -> ctype -> ctype -> (literal list * comp list) option
8.462 +(* comp -> var list -> mtyp -> mtyp -> (literal list * comp list) option
8.463 -> (literal list * comp list) option *)
8.464 -fun do_ctype_comp _ _ _ _ NONE = NONE
8.465 - | do_ctype_comp _ _ CAlpha CAlpha accum = accum
8.466 - | do_ctype_comp Eq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22))
8.467 +fun do_mtype_comp _ _ _ _ NONE = NONE
8.468 + | do_mtype_comp _ _ MAlpha MAlpha accum = accum
8.469 + | do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
8.470 (SOME accum) =
8.471 - accum |> do_sign_atom_comp Eq xs a1 a2 |> do_ctype_comp Eq xs C11 C21
8.472 - |> do_ctype_comp Eq xs C12 C22
8.473 - | do_ctype_comp Leq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22))
8.474 + accum |> do_sign_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21
8.475 + |> do_mtype_comp Eq xs M12 M22
8.476 + | do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
8.477 (SOME accum) =
8.478 - (if exists_alpha_sub_ctype C11 then
8.479 + (if exists_alpha_sub_mtype M11 then
8.480 accum |> do_sign_atom_comp Leq xs a1 a2
8.481 - |> do_ctype_comp Leq xs C21 C11
8.482 + |> do_mtype_comp Leq xs M21 M11
8.483 |> (case a2 of
8.484 S Minus => I
8.485 - | S Plus => do_ctype_comp Leq xs C11 C21
8.486 - | V x => do_ctype_comp Leq (x :: xs) C11 C21)
8.487 + | S Plus => do_mtype_comp Leq xs M11 M21
8.488 + | V x => do_mtype_comp Leq (x :: xs) M11 M21)
8.489 else
8.490 SOME accum)
8.491 - |> do_ctype_comp Leq xs C12 C22
8.492 - | do_ctype_comp cmp xs (C1 as CPair (C11, C12)) (C2 as CPair (C21, C22))
8.493 + |> do_mtype_comp Leq xs M12 M22
8.494 + | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
8.495 accum =
8.496 - (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)]
8.497 + (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
8.498 handle Library.UnequalLengths =>
8.499 - raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]))
8.500 - | do_ctype_comp _ _ (CType _) (CType _) accum =
8.501 + raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2]))
8.502 + | do_mtype_comp _ _ (MType _) (MType _) accum =
8.503 accum (* no need to compare them thanks to the cache *)
8.504 - | do_ctype_comp _ _ C1 C2 _ =
8.505 - raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])
8.506 + | do_mtype_comp _ _ M1 M2 _ =
8.507 + raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2])
8.508
8.509 -(* comp_op -> ctype -> ctype -> constraint_set -> constraint_set *)
8.510 -fun add_ctype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
8.511 - | add_ctype_comp cmp C1 C2 (CSet (lits, comps, sexps)) =
8.512 - (print_g ("*** Add " ^ string_for_ctype C1 ^ " " ^ string_for_comp_op cmp ^
8.513 - " " ^ string_for_ctype C2);
8.514 - case do_ctype_comp cmp [] C1 C2 (SOME (lits, comps)) of
8.515 +(* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *)
8.516 +fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
8.517 + | add_mtype_comp cmp M1 M2 (CSet (lits, comps, sexps)) =
8.518 + (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^
8.519 + " " ^ string_for_mtype M2);
8.520 + case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
8.521 NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
8.522 | SOME (lits, comps) => CSet (lits, comps, sexps))
8.523
8.524 -(* ctype -> ctype -> constraint_set -> constraint_set *)
8.525 -val add_ctypes_equal = add_ctype_comp Eq
8.526 -val add_is_sub_ctype = add_ctype_comp Leq
8.527 +(* mtyp -> mtyp -> constraint_set -> constraint_set *)
8.528 +val add_mtypes_equal = add_mtype_comp Eq
8.529 +val add_is_sub_mtype = add_mtype_comp Leq
8.530
8.531 -(* sign -> sign_expr -> ctype -> (literal list * sign_expr list) option
8.532 +(* sign -> sign_expr -> mtyp -> (literal list * sign_expr list) option
8.533 -> (literal list * sign_expr list) option *)
8.534 -fun do_notin_ctype_fv _ _ _ NONE = NONE
8.535 - | do_notin_ctype_fv Minus _ CAlpha accum = accum
8.536 - | do_notin_ctype_fv Plus [] CAlpha _ = NONE
8.537 - | do_notin_ctype_fv Plus [(x, sn)] CAlpha (SOME (lits, sexps)) =
8.538 +fun do_notin_mtype_fv _ _ _ NONE = NONE
8.539 + | do_notin_mtype_fv Minus _ MAlpha accum = accum
8.540 + | do_notin_mtype_fv Plus [] MAlpha _ = NONE
8.541 + | do_notin_mtype_fv Plus [(x, sn)] MAlpha (SOME (lits, sexps)) =
8.542 SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
8.543 - | do_notin_ctype_fv Plus sexp CAlpha (SOME (lits, sexps)) =
8.544 + | do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) =
8.545 SOME (lits, insert (op =) sexp sexps)
8.546 - | do_notin_ctype_fv sn sexp (CFun (C1, S sn', C2)) accum =
8.547 + | do_notin_mtype_fv sn sexp (MFun (M1, S sn', M2)) accum =
8.548 accum |> (if sn' = Plus andalso sn = Plus then
8.549 - do_notin_ctype_fv Plus sexp C1
8.550 + do_notin_mtype_fv Plus sexp M1
8.551 else
8.552 I)
8.553 |> (if sn' = Minus orelse sn = Plus then
8.554 - do_notin_ctype_fv Minus sexp C1
8.555 + do_notin_mtype_fv Minus sexp M1
8.556 else
8.557 I)
8.558 - |> do_notin_ctype_fv sn sexp C2
8.559 - | do_notin_ctype_fv Plus sexp (CFun (C1, V x, C2)) accum =
8.560 + |> do_notin_mtype_fv sn sexp M2
8.561 + | do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum =
8.562 accum |> (case do_literal (x, Minus) (SOME sexp) of
8.563 NONE => I
8.564 - | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
8.565 - |> do_notin_ctype_fv Minus sexp C1
8.566 - |> do_notin_ctype_fv Plus sexp C2
8.567 - | do_notin_ctype_fv Minus sexp (CFun (C1, V x, C2)) accum =
8.568 + | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
8.569 + |> do_notin_mtype_fv Minus sexp M1
8.570 + |> do_notin_mtype_fv Plus sexp M2
8.571 + | do_notin_mtype_fv Minus sexp (MFun (M1, V x, M2)) accum =
8.572 accum |> (case do_literal (x, Plus) (SOME sexp) of
8.573 NONE => I
8.574 - | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
8.575 - |> do_notin_ctype_fv Minus sexp C2
8.576 - | do_notin_ctype_fv sn sexp (CPair (C1, C2)) accum =
8.577 - accum |> fold (do_notin_ctype_fv sn sexp) [C1, C2]
8.578 - | do_notin_ctype_fv sn sexp (CType (_, Cs)) accum =
8.579 - accum |> fold (do_notin_ctype_fv sn sexp) Cs
8.580 - | do_notin_ctype_fv _ _ C _ =
8.581 - raise CTYPE ("Nitpick_Mono.do_notin_ctype_fv", [C])
8.582 + | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
8.583 + |> do_notin_mtype_fv Minus sexp M2
8.584 + | do_notin_mtype_fv sn sexp (MPair (M1, M2)) accum =
8.585 + accum |> fold (do_notin_mtype_fv sn sexp) [M1, M2]
8.586 + | do_notin_mtype_fv sn sexp (MType (_, Ms)) accum =
8.587 + accum |> fold (do_notin_mtype_fv sn sexp) Ms
8.588 + | do_notin_mtype_fv _ _ M _ =
8.589 + raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M])
8.590
8.591 -(* sign -> ctype -> constraint_set -> constraint_set *)
8.592 -fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet
8.593 - | add_notin_ctype_fv sn C (CSet (lits, comps, sexps)) =
8.594 - (print_g ("*** Add " ^ string_for_ctype C ^ " is right-" ^
8.595 +(* sign -> mtyp -> constraint_set -> constraint_set *)
8.596 +fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet
8.597 + | add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) =
8.598 + (print_g ("*** Add " ^ string_for_mtype M ^ " is right-" ^
8.599 (case sn of Minus => "unique" | Plus => "total") ^ ".");
8.600 - case do_notin_ctype_fv sn [] C (SOME (lits, sexps)) of
8.601 + case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
8.602 NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
8.603 | SOME (lits, sexps) => CSet (lits, comps, sexps))
8.604
8.605 -(* ctype -> constraint_set -> constraint_set *)
8.606 -val add_ctype_is_right_unique = add_notin_ctype_fv Minus
8.607 -val add_ctype_is_right_total = add_notin_ctype_fv Plus
8.608 +(* mtyp -> constraint_set -> constraint_set *)
8.609 +val add_mtype_is_right_unique = add_notin_mtype_fv Minus
8.610 +val add_mtype_is_right_total = add_notin_mtype_fv Plus
8.611
8.612 val bool_from_minus = true
8.613
8.614 @@ -516,209 +560,228 @@
8.615 | _ => NONE
8.616 end
8.617
8.618 -type ctype_schema = ctype * constraint_set
8.619 -type ctype_context =
8.620 - {bounds: ctype list,
8.621 - frees: (styp * ctype) list,
8.622 - consts: (styp * ctype) list}
8.623 +type mtype_schema = mtyp * constraint_set
8.624 +type mtype_context =
8.625 + {bounds: mtyp list,
8.626 + frees: (styp * mtyp) list,
8.627 + consts: (styp * mtyp) list}
8.628
8.629 -type accumulator = ctype_context * constraint_set
8.630 +type accumulator = mtype_context * constraint_set
8.631
8.632 val initial_gamma = {bounds = [], frees = [], consts = []}
8.633 val unsolvable_accum = (initial_gamma, UnsolvableCSet)
8.634
8.635 -(* ctype -> ctype_context -> ctype_context *)
8.636 -fun push_bound C {bounds, frees, consts} =
8.637 - {bounds = C :: bounds, frees = frees, consts = consts}
8.638 -(* ctype_context -> ctype_context *)
8.639 +(* mtyp -> mtype_context -> mtype_context *)
8.640 +fun push_bound M {bounds, frees, consts} =
8.641 + {bounds = M :: bounds, frees = frees, consts = consts}
8.642 +(* mtype_context -> mtype_context *)
8.643 fun pop_bound {bounds, frees, consts} =
8.644 {bounds = tl bounds, frees = frees, consts = consts}
8.645 handle List.Empty => initial_gamma
8.646
8.647 -(* cdata -> term -> accumulator -> ctype * accumulator *)
8.648 -fun consider_term (cdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
8.649 +(* mdata -> term -> accumulator -> mterm * accumulator *)
8.650 +fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
8.651 def_table, ...},
8.652 alpha_T, max_fresh, ...}) =
8.653 let
8.654 - (* typ -> ctype *)
8.655 - val ctype_for = fresh_ctype_for_type cdata
8.656 - (* ctype -> ctype *)
8.657 - fun pos_set_ctype_for_dom C =
8.658 - CFun (C, S (if exists_alpha_sub_ctype C then Plus else Minus), bool_C)
8.659 - (* typ -> accumulator -> ctype * accumulator *)
8.660 - fun do_quantifier T (gamma, cset) =
8.661 + (* typ -> typ -> mtyp * sign_atom * mtyp *)
8.662 + val mfun_for = fresh_mfun_for_fun_type mdata
8.663 + (* typ -> mtyp *)
8.664 + val mtype_for = fresh_mtype_for_type mdata
8.665 + (* mtyp -> mtyp *)
8.666 + fun pos_set_mtype_for_dom M =
8.667 + MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
8.668 + (* typ -> accumulator -> mterm * accumulator *)
8.669 + fun do_all T (gamma, cset) =
8.670 let
8.671 - val abs_C = ctype_for (domain_type (domain_type T))
8.672 - val body_C = ctype_for (range_type T)
8.673 + val abs_M = mtype_for (domain_type (domain_type T))
8.674 + val body_M = mtype_for (range_type T)
8.675 in
8.676 - (CFun (CFun (abs_C, S Minus, body_C), S Minus, body_C),
8.677 - (gamma, cset |> add_ctype_is_right_total abs_C))
8.678 + (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
8.679 + (gamma, cset |> add_mtype_is_right_total abs_M))
8.680 end
8.681 fun do_equals T (gamma, cset) =
8.682 - let val C = ctype_for (domain_type T) in
8.683 - (CFun (C, S Minus, CFun (C, V (Unsynchronized.inc max_fresh),
8.684 - ctype_for (nth_range_type 2 T))),
8.685 - (gamma, cset |> add_ctype_is_right_unique C))
8.686 + let val M = mtype_for (domain_type T) in
8.687 + (MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh),
8.688 + mtype_for (nth_range_type 2 T))),
8.689 + (gamma, cset |> add_mtype_is_right_unique M))
8.690 end
8.691 fun do_robust_set_operation T (gamma, cset) =
8.692 let
8.693 val set_T = domain_type T
8.694 - val C1 = ctype_for set_T
8.695 - val C2 = ctype_for set_T
8.696 - val C3 = ctype_for set_T
8.697 + val M1 = mtype_for set_T
8.698 + val M2 = mtype_for set_T
8.699 + val M3 = mtype_for set_T
8.700 in
8.701 - (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
8.702 - (gamma, cset |> add_is_sub_ctype C1 C3 |> add_is_sub_ctype C2 C3))
8.703 + (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
8.704 + (gamma, cset |> add_is_sub_mtype M1 M3 |> add_is_sub_mtype M2 M3))
8.705 end
8.706 fun do_fragile_set_operation T (gamma, cset) =
8.707 let
8.708 val set_T = domain_type T
8.709 - val set_C = ctype_for set_T
8.710 - (* typ -> ctype *)
8.711 - fun custom_ctype_for (T as Type ("fun", [T1, T2])) =
8.712 - if T = set_T then set_C
8.713 - else CFun (custom_ctype_for T1, S Minus, custom_ctype_for T2)
8.714 - | custom_ctype_for T = ctype_for T
8.715 + val set_M = mtype_for set_T
8.716 + (* typ -> mtyp *)
8.717 + fun custom_mtype_for (T as Type ("fun", [T1, T2])) =
8.718 + if T = set_T then set_M
8.719 + else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2)
8.720 + | custom_mtype_for T = mtype_for T
8.721 in
8.722 - (custom_ctype_for T, (gamma, cset |> add_ctype_is_right_unique set_C))
8.723 + (custom_mtype_for T, (gamma, cset |> add_mtype_is_right_unique set_M))
8.724 end
8.725 - (* typ -> accumulator -> ctype * accumulator *)
8.726 + (* typ -> accumulator -> mtyp * accumulator *)
8.727 fun do_pair_constr T accum =
8.728 - case ctype_for (nth_range_type 2 T) of
8.729 - C as CPair (a_C, b_C) =>
8.730 - (CFun (a_C, S Minus, CFun (b_C, S Minus, C)), accum)
8.731 - | C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C])
8.732 - (* int -> typ -> accumulator -> ctype * accumulator *)
8.733 + case mtype_for (nth_range_type 2 T) of
8.734 + M as MPair (a_M, b_M) =>
8.735 + (MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum)
8.736 + | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M])
8.737 + (* int -> typ -> accumulator -> mtyp * accumulator *)
8.738 fun do_nth_pair_sel n T =
8.739 - case ctype_for (domain_type T) of
8.740 - C as CPair (a_C, b_C) =>
8.741 - pair (CFun (C, S Minus, if n = 0 then a_C else b_C))
8.742 - | C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C])
8.743 - val unsolvable = (CType ("unsolvable", []), unsolvable_accum)
8.744 - (* typ -> term -> accumulator -> ctype * accumulator *)
8.745 - fun do_bounded_quantifier abs_T bound_t body_t accum =
8.746 + case mtype_for (domain_type T) of
8.747 + M as MPair (a_M, b_M) =>
8.748 + pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
8.749 + | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M])
8.750 + (* mtyp * accumulator *)
8.751 + val mtype_unsolvable = (irrelevant_M, unsolvable_accum)
8.752 + (* term -> mterm * accumulator *)
8.753 + fun mterm_unsolvable t = (MAtom (t, irrelevant_M), unsolvable_accum)
8.754 + (* term -> string -> typ -> term -> term -> term -> accumulator
8.755 + -> mterm * accumulator *)
8.756 + fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
8.757 let
8.758 - val abs_C = ctype_for abs_T
8.759 - val (bound_C, accum) = accum |>> push_bound abs_C |> do_term bound_t
8.760 - val expected_bound_C = pos_set_ctype_for_dom abs_C
8.761 + val abs_M = mtype_for abs_T
8.762 + val (bound_m, accum) = accum |>> push_bound abs_M |> do_term bound_t
8.763 + val expected_bound_M = pos_set_mtype_for_dom abs_M
8.764 + val (body_m, accum) =
8.765 + accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
8.766 + |> do_term body_t ||> apfst pop_bound
8.767 + val bound_M = mtype_of_mterm bound_m
8.768 + val (M1, a, M2) = dest_MFun bound_M
8.769 in
8.770 - accum ||> add_ctypes_equal expected_bound_C bound_C |> do_term body_t
8.771 - ||> apfst pop_bound
8.772 + (MApp (MAtom (t0, MFun (bound_M, S Minus, bool_M)),
8.773 + MAbs (abs_s, abs_T, M1, a,
8.774 + MApp (MApp (MAtom (connective_t, irrelevant_M),
8.775 + MApp (bound_m, MAtom (Bound 0, M1))),
8.776 + body_m))), accum)
8.777 end
8.778 - (* term -> accumulator -> ctype * accumulator *)
8.779 - and do_term _ (_, UnsolvableCSet) = unsolvable
8.780 + (* term -> accumulator -> mterm * accumulator *)
8.781 + and do_term t (_, UnsolvableCSet) = mterm_unsolvable t
8.782 | do_term t (accum as (gamma as {bounds, frees, consts}, cset)) =
8.783 (case t of
8.784 Const (x as (s, T)) =>
8.785 (case AList.lookup (op =) consts x of
8.786 - SOME C => (C, accum)
8.787 + SOME M => (M, accum)
8.788 | NONE =>
8.789 if not (could_exist_alpha_subtype alpha_T T) then
8.790 - (ctype_for T, accum)
8.791 + (mtype_for T, accum)
8.792 else case s of
8.793 - @{const_name all} => do_quantifier T accum
8.794 + @{const_name all} => do_all T accum
8.795 | @{const_name "=="} => do_equals T accum
8.796 - | @{const_name All} => do_quantifier T accum
8.797 - | @{const_name Ex} => do_quantifier T accum
8.798 + | @{const_name All} => do_all T accum
8.799 + | @{const_name Ex} =>
8.800 + do_term (@{const Not}
8.801 + $ (HOLogic.eq_const (domain_type T)
8.802 + $ Abs (Name.uu, T, @{const False}))) accum
8.803 + |>> mtype_of_mterm
8.804 | @{const_name "op ="} => do_equals T accum
8.805 - | @{const_name The} => (print_g "*** The"; unsolvable)
8.806 - | @{const_name Eps} => (print_g "*** Eps"; unsolvable)
8.807 + | @{const_name The} => (print_g "*** The"; mtype_unsolvable)
8.808 + | @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable)
8.809 | @{const_name If} =>
8.810 do_robust_set_operation (range_type T) accum
8.811 - |>> curry3 CFun bool_C (S Minus)
8.812 + |>> curry3 MFun bool_M (S Minus)
8.813 | @{const_name Pair} => do_pair_constr T accum
8.814 | @{const_name fst} => do_nth_pair_sel 0 T accum
8.815 | @{const_name snd} => do_nth_pair_sel 1 T accum
8.816 | @{const_name Id} =>
8.817 - (CFun (ctype_for (domain_type T), S Minus, bool_C), accum)
8.818 + (MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
8.819 | @{const_name insert} =>
8.820 let
8.821 val set_T = domain_type (range_type T)
8.822 - val C1 = ctype_for (domain_type set_T)
8.823 - val C1' = pos_set_ctype_for_dom C1
8.824 - val C2 = ctype_for set_T
8.825 - val C3 = ctype_for set_T
8.826 + val M1 = mtype_for (domain_type set_T)
8.827 + val M1' = pos_set_mtype_for_dom M1
8.828 + val M2 = mtype_for set_T
8.829 + val M3 = mtype_for set_T
8.830 in
8.831 - (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
8.832 - (gamma, cset |> add_ctype_is_right_unique C1
8.833 - |> add_is_sub_ctype C1' C3
8.834 - |> add_is_sub_ctype C2 C3))
8.835 + (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
8.836 + (gamma, cset |> add_mtype_is_right_unique M1
8.837 + |> add_is_sub_mtype M1' M3
8.838 + |> add_is_sub_mtype M2 M3))
8.839 end
8.840 | @{const_name converse} =>
8.841 let
8.842 val x = Unsynchronized.inc max_fresh
8.843 - (* typ -> ctype *)
8.844 - fun ctype_for_set T =
8.845 - CFun (ctype_for (domain_type T), V x, bool_C)
8.846 - val ab_set_C = domain_type T |> ctype_for_set
8.847 - val ba_set_C = range_type T |> ctype_for_set
8.848 - in (CFun (ab_set_C, S Minus, ba_set_C), accum) end
8.849 + (* typ -> mtyp *)
8.850 + fun mtype_for_set T =
8.851 + MFun (mtype_for (domain_type T), V x, bool_M)
8.852 + val ab_set_M = domain_type T |> mtype_for_set
8.853 + val ba_set_M = range_type T |> mtype_for_set
8.854 + in (MFun (ab_set_M, S Minus, ba_set_M), accum) end
8.855 | @{const_name trancl} => do_fragile_set_operation T accum
8.856 - | @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable)
8.857 + | @{const_name rtrancl} =>
8.858 + (print_g "*** rtrancl"; mtype_unsolvable)
8.859 | @{const_name finite} =>
8.860 - let val C1 = ctype_for (domain_type (domain_type T)) in
8.861 - (CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum)
8.862 + let val M1 = mtype_for (domain_type (domain_type T)) in
8.863 + (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
8.864 end
8.865 | @{const_name rel_comp} =>
8.866 let
8.867 val x = Unsynchronized.inc max_fresh
8.868 - (* typ -> ctype *)
8.869 - fun ctype_for_set T =
8.870 - CFun (ctype_for (domain_type T), V x, bool_C)
8.871 - val bc_set_C = domain_type T |> ctype_for_set
8.872 - val ab_set_C = domain_type (range_type T) |> ctype_for_set
8.873 - val ac_set_C = nth_range_type 2 T |> ctype_for_set
8.874 + (* typ -> mtyp *)
8.875 + fun mtype_for_set T =
8.876 + MFun (mtype_for (domain_type T), V x, bool_M)
8.877 + val bc_set_M = domain_type T |> mtype_for_set
8.878 + val ab_set_M = domain_type (range_type T) |> mtype_for_set
8.879 + val ac_set_M = nth_range_type 2 T |> mtype_for_set
8.880 in
8.881 - (CFun (bc_set_C, S Minus, CFun (ab_set_C, S Minus, ac_set_C)),
8.882 + (MFun (bc_set_M, S Minus, MFun (ab_set_M, S Minus, ac_set_M)),
8.883 accum)
8.884 end
8.885 | @{const_name image} =>
8.886 let
8.887 - val a_C = ctype_for (domain_type (domain_type T))
8.888 - val b_C = ctype_for (range_type (domain_type T))
8.889 + val a_M = mtype_for (domain_type (domain_type T))
8.890 + val b_M = mtype_for (range_type (domain_type T))
8.891 in
8.892 - (CFun (CFun (a_C, S Minus, b_C), S Minus,
8.893 - CFun (pos_set_ctype_for_dom a_C, S Minus,
8.894 - pos_set_ctype_for_dom b_C)), accum)
8.895 + (MFun (MFun (a_M, S Minus, b_M), S Minus,
8.896 + MFun (pos_set_mtype_for_dom a_M, S Minus,
8.897 + pos_set_mtype_for_dom b_M)), accum)
8.898 end
8.899 | @{const_name Sigma} =>
8.900 let
8.901 val x = Unsynchronized.inc max_fresh
8.902 - (* typ -> ctype *)
8.903 - fun ctype_for_set T =
8.904 - CFun (ctype_for (domain_type T), V x, bool_C)
8.905 + (* typ -> mtyp *)
8.906 + fun mtype_for_set T =
8.907 + MFun (mtype_for (domain_type T), V x, bool_M)
8.908 val a_set_T = domain_type T
8.909 - val a_C = ctype_for (domain_type a_set_T)
8.910 - val b_set_C = ctype_for_set (range_type (domain_type
8.911 + val a_M = mtype_for (domain_type a_set_T)
8.912 + val b_set_M = mtype_for_set (range_type (domain_type
8.913 (range_type T)))
8.914 - val a_set_C = ctype_for_set a_set_T
8.915 - val a_to_b_set_C = CFun (a_C, S Minus, b_set_C)
8.916 - val ab_set_C = ctype_for_set (nth_range_type 2 T)
8.917 + val a_set_M = mtype_for_set a_set_T
8.918 + val a_to_b_set_M = MFun (a_M, S Minus, b_set_M)
8.919 + val ab_set_M = mtype_for_set (nth_range_type 2 T)
8.920 in
8.921 - (CFun (a_set_C, S Minus,
8.922 - CFun (a_to_b_set_C, S Minus, ab_set_C)), accum)
8.923 + (MFun (a_set_M, S Minus,
8.924 + MFun (a_to_b_set_M, S Minus, ab_set_M)), accum)
8.925 end
8.926 | @{const_name Tha} =>
8.927 let
8.928 - val a_C = ctype_for (domain_type (domain_type T))
8.929 - val a_set_C = pos_set_ctype_for_dom a_C
8.930 - in (CFun (a_set_C, S Minus, a_C), accum) end
8.931 + val a_M = mtype_for (domain_type (domain_type T))
8.932 + val a_set_M = pos_set_mtype_for_dom a_M
8.933 + in (MFun (a_set_M, S Minus, a_M), accum) end
8.934 | @{const_name FunBox} =>
8.935 - let val dom_C = ctype_for (domain_type T) in
8.936 - (CFun (dom_C, S Minus, dom_C), accum)
8.937 + let val dom_M = mtype_for (domain_type T) in
8.938 + (MFun (dom_M, S Minus, dom_M), accum)
8.939 end
8.940 | _ =>
8.941 if s = @{const_name minus_class.minus} andalso
8.942 is_set_type (domain_type T) then
8.943 let
8.944 val set_T = domain_type T
8.945 - val left_set_C = ctype_for set_T
8.946 - val right_set_C = ctype_for set_T
8.947 + val left_set_M = mtype_for set_T
8.948 + val right_set_M = mtype_for set_T
8.949 in
8.950 - (CFun (left_set_C, S Minus,
8.951 - CFun (right_set_C, S Minus, left_set_C)),
8.952 - (gamma, cset |> add_ctype_is_right_unique right_set_C
8.953 - |> add_is_sub_ctype right_set_C left_set_C))
8.954 + (MFun (left_set_M, S Minus,
8.955 + MFun (right_set_M, S Minus, left_set_M)),
8.956 + (gamma, cset |> add_mtype_is_right_unique right_set_M
8.957 + |> add_is_sub_mtype right_set_M left_set_M))
8.958 end
8.959 else if s = @{const_name ord_class.less_eq} andalso
8.960 is_set_type (domain_type T) then
8.961 @@ -729,34 +792,37 @@
8.962 do_robust_set_operation T accum
8.963 else if is_sel s then
8.964 if constr_name_for_sel_like s = @{const_name FunBox} then
8.965 - let val dom_C = ctype_for (domain_type T) in
8.966 - (CFun (dom_C, S Minus, dom_C), accum)
8.967 + let val dom_M = mtype_for (domain_type T) in
8.968 + (MFun (dom_M, S Minus, dom_M), accum)
8.969 end
8.970 else
8.971 - (ctype_for_sel cdata x, accum)
8.972 + (mtype_for_sel mdata x, accum)
8.973 else if is_constr thy stds x then
8.974 - (ctype_for_constr cdata x, accum)
8.975 + (mtype_for_constr mdata x, accum)
8.976 else if is_built_in_const thy stds fast_descrs x then
8.977 case def_of_const thy def_table x of
8.978 - SOME t' => do_term t' accum
8.979 - | NONE => (print_g ("*** built-in " ^ s); unsolvable)
8.980 + SOME t' => do_term t' accum |>> mtype_of_mterm
8.981 + | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable)
8.982 else
8.983 - let val C = ctype_for T in
8.984 - (C, ({bounds = bounds, frees = frees,
8.985 - consts = (x, C) :: consts}, cset))
8.986 - end)
8.987 + let val M = mtype_for T in
8.988 + (M, ({bounds = bounds, frees = frees,
8.989 + consts = (x, M) :: consts}, cset))
8.990 + end) |>> curry MAtom t
8.991 | Free (x as (_, T)) =>
8.992 (case AList.lookup (op =) frees x of
8.993 - SOME C => (C, accum)
8.994 + SOME M => (M, accum)
8.995 | NONE =>
8.996 - let val C = ctype_for T in
8.997 - (C, ({bounds = bounds, frees = (x, C) :: frees,
8.998 + let val M = mtype_for T in
8.999 + (M, ({bounds = bounds, frees = (x, M) :: frees,
8.1000 consts = consts}, cset))
8.1001 - end)
8.1002 - | Var _ => (print_g "*** Var"; unsolvable)
8.1003 - | Bound j => (nth bounds j, accum)
8.1004 - | Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum)
8.1005 - | Abs (_, T, t') =>
8.1006 + end) |>> curry MAtom t
8.1007 + | Var _ => (print_g "*** Var"; mterm_unsolvable t)
8.1008 + | Bound j => (MAtom (t, nth bounds j), accum)
8.1009 + | Abs (s, T, t' as @{const False}) =>
8.1010 + let val (M1, a, M2) = mfun_for T bool_T in
8.1011 + (MAbs (s, T, M1, a, MAtom (t', M2)), accum)
8.1012 + end
8.1013 + | Abs (s, T, t') =>
8.1014 ((case t' of
8.1015 t1' $ Bound 0 =>
8.1016 if not (loose_bvar1 (t1', 0)) then
8.1017 @@ -766,43 +832,37 @@
8.1018 | _ => raise SAME ())
8.1019 handle SAME () =>
8.1020 let
8.1021 - val C = ctype_for T
8.1022 - val (C', accum) = do_term t' (accum |>> push_bound C)
8.1023 - in (CFun (C, S Minus, C'), accum |>> pop_bound) end)
8.1024 - | Const (@{const_name All}, _)
8.1025 - $ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) =>
8.1026 - do_bounded_quantifier T' t1 t2 accum
8.1027 - | Const (@{const_name Ex}, _)
8.1028 - $ Abs (_, T', @{const "op &"} $ (t1 $ Bound 0) $ t2) =>
8.1029 - do_bounded_quantifier T' t1 t2 accum
8.1030 + val M = mtype_for T
8.1031 + val (m', accum) = do_term t' (accum |>> push_bound M)
8.1032 + in (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound) end)
8.1033 + | (t0 as Const (@{const_name All}, _))
8.1034 + $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
8.1035 + do_bounded_quantifier t0 s' T' t10 t11 t12 accum
8.1036 + | (t0 as Const (@{const_name Ex}, _))
8.1037 + $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
8.1038 + do_bounded_quantifier t0 s' T' t10 t11 t12 accum
8.1039 | Const (@{const_name Let}, _) $ t1 $ t2 =>
8.1040 do_term (betapply (t2, t1)) accum
8.1041 | t1 $ t2 =>
8.1042 let
8.1043 - val (C1, accum) = do_term t1 accum
8.1044 - val (C2, accum) = do_term t2 accum
8.1045 + val (m1, accum) = do_term t1 accum
8.1046 + val (m2, accum) = do_term t2 accum
8.1047 in
8.1048 case accum of
8.1049 - (_, UnsolvableCSet) => unsolvable
8.1050 - | _ => case C1 of
8.1051 - CFun (C11, _, C12) =>
8.1052 - (C12, accum ||> add_is_sub_ctype C2 C11)
8.1053 - | _ => raise CTYPE ("Nitpick_Mono.consider_term.do_term \
8.1054 - \(op $)", [C1])
8.1055 + (_, UnsolvableCSet) => mterm_unsolvable t
8.1056 + | _ => (MApp (m1, m2), accum)
8.1057 end)
8.1058 - |> tap (fn (C, _) =>
8.1059 - print_g (" \<Gamma> \<turnstile> " ^
8.1060 - Syntax.string_of_term ctxt t ^ " : " ^
8.1061 - string_for_ctype C))
8.1062 + |> tap (fn (m, _) => print_g (" \<Gamma> \<turnstile> " ^
8.1063 + string_for_mterm ctxt m))
8.1064 in do_term end
8.1065
8.1066 -(* cdata -> sign -> term -> accumulator -> accumulator *)
8.1067 -fun consider_general_formula (cdata as {hol_ctxt = {ctxt, ...}, ...}) =
8.1068 +(* mdata -> sign -> term -> accumulator -> accumulator *)
8.1069 +fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
8.1070 let
8.1071 - (* typ -> ctype *)
8.1072 - val ctype_for = fresh_ctype_for_type cdata
8.1073 - (* term -> accumulator -> ctype * accumulator *)
8.1074 - val do_term = consider_term cdata
8.1075 + (* typ -> mtyp *)
8.1076 + val mtype_for = fresh_mtype_for_type mdata
8.1077 + (* term -> accumulator -> mtyp * accumulator *)
8.1078 + val do_term = apfst mtype_of_mterm oo consider_term mdata
8.1079 (* sign -> term -> accumulator -> accumulator *)
8.1080 fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
8.1081 | do_formula sn t (accum as (gamma, cset)) =
8.1082 @@ -813,25 +873,25 @@
8.1083 (* string -> typ -> term -> accumulator *)
8.1084 fun do_quantifier quant_s abs_T body_t =
8.1085 let
8.1086 - val abs_C = ctype_for abs_T
8.1087 + val abs_M = mtype_for abs_T
8.1088 val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
8.1089 - val cset = cset |> side_cond ? add_ctype_is_right_total abs_C
8.1090 + val cset = cset |> side_cond ? add_mtype_is_right_total abs_M
8.1091 in
8.1092 - (gamma |> push_bound abs_C, cset)
8.1093 + (gamma |> push_bound abs_M, cset)
8.1094 |> do_co_formula body_t |>> pop_bound
8.1095 end
8.1096 (* typ -> term -> accumulator *)
8.1097 fun do_bounded_quantifier abs_T body_t =
8.1098 - accum |>> push_bound (ctype_for abs_T) |> do_co_formula body_t
8.1099 + accum |>> push_bound (mtype_for abs_T) |> do_co_formula body_t
8.1100 |>> pop_bound
8.1101 (* term -> term -> accumulator *)
8.1102 fun do_equals t1 t2 =
8.1103 case sn of
8.1104 Plus => do_term t accum |> snd
8.1105 | Minus => let
8.1106 - val (C1, accum) = do_term t1 accum
8.1107 - val (C2, accum) = do_term t2 accum
8.1108 - in accum ||> add_ctypes_equal C1 C2 end
8.1109 + val (M1, accum) = do_term t1 accum
8.1110 + val (M2, accum) = do_term t2 accum
8.1111 + in accum ||> add_mtypes_equal M1 M2 end
8.1112 in
8.1113 case t of
8.1114 Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
8.1115 @@ -849,8 +909,13 @@
8.1116 | Const (@{const_name Ex}, _)
8.1117 $ Abs (_, T1, t1 as @{const "op &"} $ (_ $ Bound 0) $ _) =>
8.1118 do_bounded_quantifier T1 t1
8.1119 - | Const (s0 as @{const_name Ex}, _) $ Abs (_, T1, t1) =>
8.1120 - do_quantifier s0 T1 t1
8.1121 + | Const (s0 as @{const_name Ex}, T0) $ (t1 as Abs (_, T1, t1')) =>
8.1122 + (case sn of
8.1123 + Plus => do_quantifier s0 T1 t1'
8.1124 + | Minus =>
8.1125 + do_term (@{const Not}
8.1126 + $ (HOLogic.eq_const (domain_type T0) $ t1
8.1127 + $ Abs (Name.uu, T1, @{const False}))) accum |> snd)
8.1128 | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2
8.1129 | @{const "op &"} $ t1 $ t2 =>
8.1130 accum |> do_co_formula t1 |> do_co_formula t2
8.1131 @@ -882,32 +947,32 @@
8.1132 |> (forall (member (op =) harmless_consts o original_name o fst)
8.1133 orf exists (member (op =) bounteous_consts o fst))
8.1134
8.1135 -(* cdata -> sign -> term -> accumulator -> accumulator *)
8.1136 -fun consider_nondefinitional_axiom (cdata as {hol_ctxt, ...}) sn t =
8.1137 - not (is_harmless_axiom hol_ctxt t) ? consider_general_formula cdata sn t
8.1138 +(* mdata -> sign -> term -> accumulator -> accumulator *)
8.1139 +fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) sn t =
8.1140 + not (is_harmless_axiom hol_ctxt t) ? consider_general_formula mdata sn t
8.1141
8.1142 -(* cdata -> term -> accumulator -> accumulator *)
8.1143 -fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
8.1144 +(* mdata -> term -> accumulator -> accumulator *)
8.1145 +fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t =
8.1146 if not (is_constr_pattern_formula thy t) then
8.1147 - consider_nondefinitional_axiom cdata Plus t
8.1148 + consider_nondefinitional_axiom mdata Plus t
8.1149 else if is_harmless_axiom hol_ctxt t then
8.1150 I
8.1151 else
8.1152 let
8.1153 - (* term -> accumulator -> ctype * accumulator *)
8.1154 - val do_term = consider_term cdata
8.1155 + (* term -> accumulator -> mtyp * accumulator *)
8.1156 + val do_term = apfst mtype_of_mterm oo consider_term mdata
8.1157 (* typ -> term -> accumulator -> accumulator *)
8.1158 fun do_all abs_T body_t accum =
8.1159 - let val abs_C = fresh_ctype_for_type cdata abs_T in
8.1160 - accum |>> push_bound abs_C |> do_formula body_t |>> pop_bound
8.1161 + let val abs_M = fresh_mtype_for_type mdata abs_T in
8.1162 + accum |>> push_bound abs_M |> do_formula body_t |>> pop_bound
8.1163 end
8.1164 (* term -> term -> accumulator -> accumulator *)
8.1165 and do_implies t1 t2 = do_term t1 #> snd #> do_formula t2
8.1166 and do_equals t1 t2 accum =
8.1167 let
8.1168 - val (C1, accum) = do_term t1 accum
8.1169 - val (C2, accum) = do_term t2 accum
8.1170 - in accum ||> add_ctypes_equal C1 C2 end
8.1171 + val (M1, accum) = do_term t1 accum
8.1172 + val (M2, accum) = do_term t2 accum
8.1173 + in accum ||> add_mtypes_equal M1 M2 end
8.1174 (* term -> accumulator -> accumulator *)
8.1175 and do_formula _ (_, UnsolvableCSet) = unsolvable_accum
8.1176 | do_formula t accum =
8.1177 @@ -926,15 +991,15 @@
8.1178 \do_formula", [t])
8.1179 in do_formula t end
8.1180
8.1181 -(* Proof.context -> literal list -> term -> ctype -> string *)
8.1182 -fun string_for_ctype_of_term ctxt lits t C =
8.1183 +(* Proof.context -> literal list -> term -> mtyp -> string *)
8.1184 +fun string_for_mtype_of_term ctxt lits t M =
8.1185 Syntax.string_of_term ctxt t ^ " : " ^
8.1186 - string_for_ctype (instantiate_ctype lits C)
8.1187 + string_for_mtype (instantiate_mtype lits M)
8.1188
8.1189 -(* theory -> literal list -> ctype_context -> unit *)
8.1190 -fun print_ctype_context ctxt lits ({frees, consts, ...} : ctype_context) =
8.1191 - map (fn (x, C) => string_for_ctype_of_term ctxt lits (Free x) C) frees @
8.1192 - map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
8.1193 +(* theory -> literal list -> mtype_context -> unit *)
8.1194 +fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
8.1195 + map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
8.1196 + map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
8.1197 |> cat_lines |> print_g
8.1198
8.1199 (* hol_context -> bool -> typ -> term list * term list * term -> bool *)
8.1200 @@ -942,20 +1007,20 @@
8.1201 (def_ts, nondef_ts, core_t) =
8.1202 let
8.1203 val _ = print_g ("****** Monotonicity analysis: " ^
8.1204 - string_for_ctype CAlpha ^ " is " ^
8.1205 + string_for_mtype MAlpha ^ " is " ^
8.1206 Syntax.string_of_typ ctxt alpha_T)
8.1207 - val cdata as {max_fresh, constr_cache, ...} =
8.1208 - initial_cdata hol_ctxt binarize alpha_T
8.1209 + val mdata as {max_fresh, constr_cache, ...} =
8.1210 + initial_mdata hol_ctxt binarize alpha_T
8.1211 val (gamma as {frees, consts, ...}, cset) =
8.1212 (initial_gamma, slack)
8.1213 - |> fold (consider_definitional_axiom cdata) def_ts
8.1214 - |> fold (consider_nondefinitional_axiom cdata Plus) nondef_ts
8.1215 - |> consider_general_formula cdata Plus core_t
8.1216 + |> fold (consider_definitional_axiom mdata) def_ts
8.1217 + |> fold (consider_nondefinitional_axiom mdata Plus) nondef_ts
8.1218 + |> consider_general_formula mdata Plus core_t
8.1219 in
8.1220 case solve (!max_fresh) cset of
8.1221 - SOME lits => (print_ctype_context ctxt lits gamma; true)
8.1222 + SOME lits => (print_mtype_context ctxt lits gamma; true)
8.1223 | _ => false
8.1224 end
8.1225 - handle CTYPE (loc, Cs) => raise BAD (loc, commas (map string_for_ctype Cs))
8.1226 + handle MTYPE (loc, Ms) => raise BAD (loc, commas (map string_for_mtype Ms))
8.1227
8.1228 end;
9.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Feb 25 10:08:44 2010 +0100
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Feb 25 16:33:39 2010 +0100
9.3 @@ -1031,7 +1031,7 @@
9.4 if is_opt_rep R then
9.5 triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
9.6 else if opt andalso polar = Pos andalso
9.7 - not (is_concrete_type datatypes (type_of u1)) then
9.8 + not (is_concrete_type datatypes true (type_of u1)) then
9.9 Cst (False, T, Formula Pos)
9.10 else
9.11 s_op2 Subset T R u1 u2
9.12 @@ -1057,7 +1057,7 @@
9.13 else opt_opt_case ()
9.14 in
9.15 if unsound orelse polar = Neg orelse
9.16 - is_concrete_type datatypes (type_of u1) then
9.17 + is_concrete_type datatypes true (type_of u1) then
9.18 case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
9.19 (true, true) => opt_opt_case ()
9.20 | (true, false) => hybrid_case u1'
9.21 @@ -1159,7 +1159,7 @@
9.22 let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
9.23 if def orelse
9.24 (unsound andalso (polar = Pos) = (oper = All)) orelse
9.25 - is_complete_type datatypes (type_of u1) then
9.26 + is_complete_type datatypes true (type_of u1) then
9.27 quant_u
9.28 else
9.29 let
9.30 @@ -1202,7 +1202,7 @@
9.31 else unopt_R |> opt ? opt_rep ofs T
9.32 val u = Op2 (oper, T, R, u1', sub u2)
9.33 in
9.34 - if is_complete_type datatypes T orelse not opt1 then
9.35 + if is_complete_type datatypes true T orelse not opt1 then
9.36 u
9.37 else
9.38 let
10.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Thu Feb 25 10:08:44 2010 +0100
10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Thu Feb 25 16:33:39 2010 +0100
10.3 @@ -126,7 +126,7 @@
10.4 val norm_frac_rel = (4, 0)
10.5
10.6 (* int -> bool -> rel_expr *)
10.7 -fun atom_for_bool j0 = Atom o Integer.add j0 o int_for_bool
10.8 +fun atom_for_bool j0 = Atom o Integer.add j0 o int_from_bool
10.9 (* bool -> formula *)
10.10 fun formula_for_bool b = if b then True else False
10.11
11.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Feb 25 10:08:44 2010 +0100
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Feb 25 16:33:39 2010 +0100
11.3 @@ -168,7 +168,6 @@
11.4 | (Type (new_s, new_Ts as [new_T1, new_T2]),
11.5 Type (old_s, old_Ts as [old_T1, old_T2])) =>
11.6 if old_s = @{type_name fun_box} orelse
11.7 - old_s = @{type_name fin_fun} orelse
11.8 old_s = @{type_name pair_box} orelse old_s = "*" then
11.9 case constr_expand hol_ctxt old_T t of
11.10 Const (old_s, _) $ t1 =>
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Thu Feb 25 10:08:44 2010 +0100
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Thu Feb 25 16:33:39 2010 +0100
12.3 @@ -299,7 +299,7 @@
12.4 | z => Func z)
12.5 | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
12.6 fun best_set_rep_for_type (scope as {datatypes, ...}) T =
12.7 - (if is_exact_type datatypes T then best_non_opt_set_rep_for_type
12.8 + (if is_exact_type datatypes true T then best_non_opt_set_rep_for_type
12.9 else best_opt_set_rep_for_type) scope T
12.10 fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
12.11 (Type ("fun", [T1, T2])) =
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 25 10:08:44 2010 +0100
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 25 16:33:39 2010 +0100
13.3 @@ -23,8 +23,8 @@
13.4 card: int,
13.5 co: bool,
13.6 standard: bool,
13.7 - complete: bool,
13.8 - concrete: bool,
13.9 + complete: bool * bool,
13.10 + concrete: bool * bool,
13.11 deep: bool,
13.12 constrs: constr_spec list}
13.13
13.14 @@ -39,9 +39,9 @@
13.15
13.16 val datatype_spec : dtype_spec list -> typ -> dtype_spec option
13.17 val constr_spec : dtype_spec list -> styp -> constr_spec
13.18 - val is_complete_type : dtype_spec list -> typ -> bool
13.19 - val is_concrete_type : dtype_spec list -> typ -> bool
13.20 - val is_exact_type : dtype_spec list -> typ -> bool
13.21 + val is_complete_type : dtype_spec list -> bool -> typ -> bool
13.22 + val is_concrete_type : dtype_spec list -> bool -> typ -> bool
13.23 + val is_exact_type : dtype_spec list -> bool -> typ -> bool
13.24 val offset_of_type : int Typtab.table -> typ -> int
13.25 val spec_of_type : scope -> typ -> int * int
13.26 val pretties_for_scope : scope -> bool -> Pretty.T list
13.27 @@ -51,7 +51,7 @@
13.28 val all_scopes :
13.29 hol_context -> bool -> int -> (typ option * int list) list
13.30 -> (styp option * int list) list -> (styp option * int list) list
13.31 - -> int list -> int list -> typ list -> typ list -> typ list
13.32 + -> int list -> int list -> typ list -> typ list -> typ list -> typ list
13.33 -> int * scope list
13.34 end;
13.35
13.36 @@ -74,8 +74,8 @@
13.37 card: int,
13.38 co: bool,
13.39 standard: bool,
13.40 - complete: bool,
13.41 - concrete: bool,
13.42 + complete: bool * bool,
13.43 + concrete: bool * bool,
13.44 deep: bool,
13.45 constrs: constr_spec list}
13.46
13.47 @@ -105,22 +105,24 @@
13.48 SOME c => c
13.49 | NONE => constr_spec dtypes x
13.50
13.51 -(* dtype_spec list -> typ -> bool *)
13.52 -fun is_complete_type dtypes (Type ("fun", [T1, T2])) =
13.53 - is_concrete_type dtypes T1 andalso is_complete_type dtypes T2
13.54 - | is_complete_type dtypes (Type ("*", Ts)) =
13.55 - forall (is_complete_type dtypes) Ts
13.56 - | is_complete_type dtypes T =
13.57 +(* dtype_spec list -> bool -> typ -> bool *)
13.58 +fun is_complete_type dtypes facto (Type ("fun", [T1, T2])) =
13.59 + is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
13.60 + | is_complete_type dtypes facto (Type ("*", Ts)) =
13.61 + forall (is_complete_type dtypes facto) Ts
13.62 + | is_complete_type dtypes facto T =
13.63 not (is_integer_like_type T) andalso not (is_bit_type T) andalso
13.64 - #complete (the (datatype_spec dtypes T))
13.65 + fun_from_pair (#complete (the (datatype_spec dtypes T))) facto
13.66 handle Option.Option => true
13.67 -and is_concrete_type dtypes (Type ("fun", [T1, T2])) =
13.68 - is_complete_type dtypes T1 andalso is_concrete_type dtypes T2
13.69 - | is_concrete_type dtypes (Type ("*", Ts)) =
13.70 - forall (is_concrete_type dtypes) Ts
13.71 - | is_concrete_type dtypes T =
13.72 - #concrete (the (datatype_spec dtypes T)) handle Option.Option => true
13.73 -fun is_exact_type dtypes = is_complete_type dtypes andf is_concrete_type dtypes
13.74 +and is_concrete_type dtypes facto (Type ("fun", [T1, T2])) =
13.75 + is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
13.76 + | is_concrete_type dtypes facto (Type ("*", Ts)) =
13.77 + forall (is_concrete_type dtypes facto) Ts
13.78 + | is_concrete_type dtypes facto T =
13.79 + fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
13.80 + handle Option.Option => true
13.81 +fun is_exact_type dtypes facto =
13.82 + is_complete_type dtypes facto andf is_concrete_type dtypes facto
13.83
13.84 (* int Typtab.table -> typ -> int *)
13.85 fun offset_of_type ofs T =
13.86 @@ -461,15 +463,18 @@
13.87 explicit_max = max, total = total} :: constrs
13.88 end
13.89
13.90 -(* hol_context -> (typ * int) list -> typ -> bool *)
13.91 -fun has_exact_card hol_ctxt card_assigns T =
13.92 +(* hol_context -> bool -> typ list -> (typ * int) list -> typ -> bool *)
13.93 +fun has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T =
13.94 let val card = card_of_type card_assigns T in
13.95 - card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
13.96 + card = bounded_exact_card_of_type hol_ctxt
13.97 + (if facto then finitizable_dataTs else []) (card + 1) 0
13.98 + card_assigns T
13.99 end
13.100
13.101 -(* hol_context -> bool -> typ list -> scope_desc -> typ * int -> dtype_spec *)
13.102 +(* hol_context -> bool -> typ list -> typ list -> scope_desc -> typ * int
13.103 + -> dtype_spec *)
13.104 fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, stds, ...}) binarize
13.105 - deep_dataTs (desc as (card_assigns, _)) (T, card) =
13.106 + deep_dataTs finitizable_dataTs (desc as (card_assigns, _)) (T, card) =
13.107 let
13.108 val deep = member (op =) deep_dataTs T
13.109 val co = is_codatatype thy T
13.110 @@ -478,10 +483,16 @@
13.111 val self_recs = map (is_self_recursive_constr_type o snd) xs
13.112 val (num_self_recs, num_non_self_recs) =
13.113 List.partition I self_recs |> pairself length
13.114 - val complete = has_exact_card hol_ctxt card_assigns T
13.115 - val concrete = is_word_type T orelse
13.116 - (xs |> maps (binder_types o snd) |> maps binder_types
13.117 - |> forall (has_exact_card hol_ctxt card_assigns))
13.118 + (* bool -> bool *)
13.119 + fun is_complete facto =
13.120 + has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T
13.121 + fun is_concrete facto =
13.122 + is_word_type T orelse
13.123 + xs |> maps (binder_types o snd) |> maps binder_types
13.124 + |> forall (has_exact_card hol_ctxt facto finitizable_dataTs
13.125 + card_assigns)
13.126 + val complete = pair_from_fun is_complete
13.127 + val concrete = pair_from_fun is_concrete
13.128 (* int -> int *)
13.129 fun sum_dom_cards max =
13.130 map (domain_card max card_assigns o snd) xs |> Integer.sum
13.131 @@ -494,13 +505,15 @@
13.132 concrete = concrete, deep = deep, constrs = constrs}
13.133 end
13.134
13.135 -(* hol_context -> bool -> int -> typ list -> scope_desc -> scope *)
13.136 +(* hol_context -> bool -> int -> typ list -> typ list -> scope_desc -> scope *)
13.137 fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break
13.138 - deep_dataTs (desc as (card_assigns, _)) =
13.139 + deep_dataTs finitizable_dataTs
13.140 + (desc as (card_assigns, _)) =
13.141 let
13.142 val datatypes =
13.143 map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
13.144 - desc) (filter (is_datatype thy stds o fst) card_assigns)
13.145 + finitizable_dataTs desc)
13.146 + (filter (is_datatype thy stds o fst) card_assigns)
13.147 val bits = card_of_type card_assigns @{typ signed_bit} - 1
13.148 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
13.149 card_of_type card_assigns @{typ unsigned_bit}
13.150 @@ -530,10 +543,10 @@
13.151
13.152 (* hol_context -> bool -> int -> (typ option * int list) list
13.153 -> (styp option * int list) list -> (styp option * int list) list -> int list
13.154 - -> typ list -> typ list -> typ list -> int * scope list *)
13.155 + -> typ list -> typ list -> typ list ->typ list -> int * scope list *)
13.156 fun all_scopes (hol_ctxt as {thy, ...}) binarize sym_break cards_assigns
13.157 maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
13.158 - deep_dataTs =
13.159 + deep_dataTs finitizable_dataTs =
13.160 let
13.161 val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
13.162 cards_assigns
13.163 @@ -550,7 +563,7 @@
13.164 (length all - length head,
13.165 descs |> length descs <= distinct_threshold ? distinct (op =)
13.166 |> map (scope_from_descriptor hol_ctxt binarize sym_break
13.167 - deep_dataTs))
13.168 + deep_dataTs finitizable_dataTs))
13.169 end
13.170
13.171 end;
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Feb 25 10:08:44 2010 +0100
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Feb 25 16:33:39 2010 +0100
14.3 @@ -20,7 +20,9 @@
14.4 val nitpick_prefix : string
14.5 val curry3 : ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
14.6 val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
14.7 - val int_for_bool : bool -> int
14.8 + val pair_from_fun : (bool -> 'a) -> 'a * 'a
14.9 + val fun_from_pair : 'a * 'a -> bool -> 'a
14.10 + val int_from_bool : bool -> int
14.11 val nat_minus : int -> int -> int
14.12 val reasonable_power : int -> int -> int
14.13 val exact_log : int -> int -> int
14.14 @@ -84,8 +86,13 @@
14.15 (* ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c *)
14.16 fun pairf f g x = (f x, g x)
14.17
14.18 +(* (bool -> 'a) -> 'a * 'a *)
14.19 +fun pair_from_fun f = (f false, f true)
14.20 +(* 'a * 'a -> bool -> 'a *)
14.21 +fun fun_from_pair (f, t) b = if b then t else f
14.22 +
14.23 (* bool -> int *)
14.24 -fun int_for_bool b = if b then 1 else 0
14.25 +fun int_from_bool b = if b then 1 else 0
14.26 (* int -> int -> int *)
14.27 fun nat_minus i j = if i > j then i - j else 0
14.28