redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 12 21:27:06 2010 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Feb 13 11:56:06 2010 +0100
1.3 @@ -97,6 +97,7 @@
1.4 val dest_n_tuple : int -> term -> term list
1.5 val instantiate_type : theory -> typ -> typ -> typ -> typ
1.6 val is_real_datatype : theory -> string -> bool
1.7 + val is_standard_datatype : hol_context -> typ -> bool
1.8 val is_quot_type : theory -> typ -> bool
1.9 val is_codatatype : theory -> typ -> bool
1.10 val is_pure_typedef : theory -> typ -> bool
1.11 @@ -574,6 +575,10 @@
1.12 (* theory -> string -> bool *)
1.13 val is_typedef = is_some oo typedef_info
1.14 val is_real_datatype = is_some oo Datatype.get_info
1.15 +(* hol_context -> typ -> bool *)
1.16 +fun is_standard_datatype ({thy, stds, ...} : hol_context) =
1.17 + the o triple_lookup (type_match thy) stds
1.18 +
1.19 (* theory -> typ -> bool *)
1.20 fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
1.21 | is_quot_type _ (Type ("FSet.fset", _)) = true
1.22 @@ -828,9 +833,8 @@
1.23 fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
1.24 fun suc_const T = Const (@{const_name Suc}, T --> T)
1.25
1.26 -(* hol_context -> typ -> styp list *)
1.27 -fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
1.28 - (T as Type (s, Ts)) =
1.29 +(* theory -> typ -> styp list *)
1.30 +fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
1.31 (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
1.32 SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
1.33 | _ =>
1.34 @@ -843,8 +847,6 @@
1.35 map (fn (s', Us) =>
1.36 (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
1.37 ---> T)) constrs
1.38 - |> (triple_lookup (type_match thy) stds T |> the |> not) ?
1.39 - cons (@{const_name Silly}, @{typ \<xi>} --> T)
1.40 end
1.41 | NONE =>
1.42 if is_record_type T then
1.43 @@ -867,11 +869,11 @@
1.44 [])
1.45 | uncached_datatype_constrs _ _ = []
1.46 (* hol_context -> typ -> styp list *)
1.47 -fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
1.48 +fun datatype_constrs ({thy, constr_cache, ...} : hol_context) T =
1.49 case AList.lookup (op =) (!constr_cache) T of
1.50 SOME xs => xs
1.51 | NONE =>
1.52 - let val xs = uncached_datatype_constrs hol_ctxt T in
1.53 + let val xs = uncached_datatype_constrs thy T in
1.54 (Unsynchronized.change constr_cache (cons (T, xs)); xs)
1.55 end
1.56 fun boxed_datatype_constrs hol_ctxt =
1.57 @@ -957,10 +959,6 @@
1.58 | _ => list_comb (Const x, args)
1.59 end
1.60
1.61 -(* The higher this number is, the more nonstandard models can be generated. It's
1.62 - not important enough to be a user option, though. *)
1.63 -val xi_card = 8
1.64 -
1.65 (* (typ * int) list -> typ -> int *)
1.66 fun card_of_type assigns (Type ("fun", [T1, T2])) =
1.67 reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
1.68 @@ -970,7 +968,6 @@
1.69 | card_of_type _ @{typ prop} = 2
1.70 | card_of_type _ @{typ bool} = 2
1.71 | card_of_type _ @{typ unit} = 1
1.72 - | card_of_type _ @{typ \<xi>} = xi_card
1.73 | card_of_type assigns T =
1.74 case AList.lookup (op =) assigns T of
1.75 SOME k => k
1.76 @@ -1027,7 +1024,6 @@
1.77 | @{typ prop} => 2
1.78 | @{typ bool} => 2
1.79 | @{typ unit} => 1
1.80 - | @{typ \<xi>} => xi_card
1.81 | Type _ =>
1.82 (case datatype_constrs hol_ctxt T of
1.83 [] => if is_integer_type T orelse is_bit_type T then 0
1.84 @@ -1393,21 +1389,11 @@
1.85 fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
1.86 let
1.87 val xs = datatype_constrs hol_ctxt dataT
1.88 - val xs' = filter_out (curry (op =) @{const_name Silly} o fst) xs
1.89 - val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
1.90 + val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
1.91 + val (xs', x) = split_last xs
1.92 in
1.93 - (if length xs = length xs' then
1.94 - let
1.95 - val (xs'', x) = split_last xs'
1.96 - in
1.97 - constr_case_body thy (1, x)
1.98 - |> fold_rev (add_constr_case hol_ctxt res_T)
1.99 - (length xs' downto 2 ~~ xs'')
1.100 - end
1.101 - else
1.102 - Const (@{const_name undefined}, dataT --> res_T) $ Bound 0
1.103 - |> fold_rev (add_constr_case hol_ctxt res_T)
1.104 - (length xs' downto 1 ~~ xs'))
1.105 + constr_case_body thy (1, x)
1.106 + |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
1.107 |> fold_rev (curry absdummy) (func_Ts @ [dataT])
1.108 end
1.109
1.110 @@ -2032,8 +2018,7 @@
1.111 | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
1.112 | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
1.113 | Type (_, Ts) =>
1.114 - if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} ::
1.115 - @{typ \<xi>} :: accum) T then
1.116 + if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
1.117 accum
1.118 else
1.119 T :: accum
2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Feb 12 21:27:06 2010 +0100
2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sat Feb 13 11:56:06 2010 +0100
2.3 @@ -318,7 +318,8 @@
2.4 else
2.5 [KK.TupleSet [],
2.6 if T1 = T2 andalso epsilon > delta andalso
2.7 - not (datatype_spec dtypes T1 |> the |> #co) then
2.8 + (datatype_spec dtypes T1 |> the |> pairf #co #standard)
2.9 + = (false, true) then
2.10 index_seq delta (epsilon - delta)
2.11 |> map (fn j =>
2.12 KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
2.13 @@ -763,6 +764,7 @@
2.14 (* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
2.15 -> dtype_spec -> nfa_entry option *)
2.16 fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
2.17 + | nfa_entry_for_datatype _ _ _ _ {standard = false, ...} = NONE
2.18 | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
2.19 | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
2.20 SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
3.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Feb 12 21:27:06 2010 +0100
3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Feb 13 11:56:06 2010 +0100
3.3 @@ -53,6 +53,8 @@
3.4 val base_mixfix = "_\<^bsub>base\<^esub>"
3.5 val step_mixfix = "_\<^bsub>step\<^esub>"
3.6 val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
3.7 +val cyclic_co_val_name = "\<omega>"
3.8 +val cyclic_non_std_type_name = "\<xi>"
3.9 val opt_flag = nitpick_prefix ^ "opt"
3.10 val non_opt_flag = nitpick_prefix ^ "non_opt"
3.11
3.12 @@ -397,7 +399,7 @@
3.13 else case datatype_spec datatypes T of
3.14 NONE => nth_atom pool for_auto T j k
3.15 | SOME {deep = false, ...} => nth_atom pool for_auto T j k
3.16 - | SOME {co, constrs, ...} =>
3.17 + | SOME {co, standard, constrs, ...} =>
3.18 let
3.19 (* styp -> int list *)
3.20 fun tuples_for_const (s, T) =
3.21 @@ -428,8 +430,9 @@
3.22 map (map_filter (fn js => if hd js = real_j then SOME (tl js)
3.23 else NONE)) sel_jsss
3.24 val uncur_arg_Ts = binder_types constr_T
3.25 + val maybe_cyclic = co orelse not standard
3.26 in
3.27 - if co andalso member (op =) seen (T, j) then
3.28 + if maybe_cyclic andalso member (op =) seen (T, j) then
3.29 Var (var ())
3.30 else if constr_s = @{const_name Word} then
3.31 HOLogic.mk_number
3.32 @@ -437,7 +440,7 @@
3.33 (value_of_bits (the_single arg_jsss))
3.34 else
3.35 let
3.36 - val seen = seen |> co ? cons (T, j)
3.37 + val seen = seen |> maybe_cyclic ? cons (T, j)
3.38 val ts =
3.39 if length arg_Ts = 0 then
3.40 []
3.41 @@ -469,19 +472,20 @@
3.42 (is_abs_fun thy constr_x orelse
3.43 constr_s = @{const_name Quot}) then
3.44 Const (abs_name, constr_T) $ the_single ts
3.45 - else if not for_auto andalso
3.46 - constr_s = @{const_name Silly} then
3.47 - Const (fst (dest_Const (the_single ts)), T)
3.48 else
3.49 list_comb (Const constr_x, ts)
3.50 in
3.51 - if co then
3.52 + if maybe_cyclic then
3.53 let val var = var () in
3.54 if exists_subterm (curry (op =) (Var var)) t then
3.55 - Const (@{const_name The}, (T --> bool_T) --> T)
3.56 - $ Abs ("\<omega>", T,
3.57 - Const (@{const_name "op ="}, T --> T --> bool_T)
3.58 - $ Bound 0 $ abstract_over (Var var, t))
3.59 + if co then
3.60 + Const (@{const_name The}, (T --> bool_T) --> T)
3.61 + $ Abs (cyclic_co_val_name, T,
3.62 + Const (@{const_name "op ="}, T --> T --> bool_T)
3.63 + $ Bound 0 $ abstract_over (Var var, t))
3.64 + else
3.65 + nth_atom pool for_auto
3.66 + (Type (cyclic_non_std_type_name, [])) j k
3.67 else
3.68 t
3.69 end
3.70 @@ -682,7 +686,8 @@
3.71 (* typ -> dtype_spec list *)
3.72 fun integer_datatype T =
3.73 [{typ = T, card = card_of_type card_assigns T, co = false,
3.74 - complete = false, concrete = true, deep = true, constrs = []}]
3.75 + standard = true, complete = false, concrete = true, deep = true,
3.76 + constrs = []}]
3.77 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
3.78 val (codatatypes, datatypes) =
3.79 datatypes |> filter #deep |> List.partition #co
4.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Feb 12 21:27:06 2010 +0100
4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Sat Feb 13 11:56:06 2010 +0100
4.3 @@ -22,6 +22,7 @@
4.4 typ: typ,
4.5 card: int,
4.6 co: bool,
4.7 + standard: bool,
4.8 complete: bool,
4.9 concrete: bool,
4.10 deep: bool,
4.11 @@ -71,6 +72,7 @@
4.12 typ: typ,
4.13 card: int,
4.14 co: bool,
4.15 + standard: bool,
4.16 complete: bool,
4.17 concrete: bool,
4.18 deep: bool,
4.19 @@ -466,6 +468,7 @@
4.20 let
4.21 val deep = member (op =) deep_dataTs T
4.22 val co = is_codatatype thy T
4.23 + val standard = is_standard_datatype hol_ctxt T
4.24 val xs = boxed_datatype_constrs hol_ctxt T
4.25 val self_recs = map (is_self_recursive_constr_type o snd) xs
4.26 val (num_self_recs, num_non_self_recs) =
4.27 @@ -481,8 +484,8 @@
4.28 num_non_self_recs)
4.29 (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
4.30 in
4.31 - {typ = T, card = card, co = co, complete = complete, concrete = concrete,
4.32 - deep = deep, constrs = constrs}
4.33 + {typ = T, card = card, co = co, standard = standard, complete = complete,
4.34 + concrete = concrete, deep = deep, constrs = constrs}
4.35 end
4.36
4.37 (* int -> int *)