--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 04 13:36:52 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 04 16:03:15 2010 +0100
@@ -8,7 +8,7 @@
signature NITPICK_SCOPE =
sig
type styp = Nitpick_Util.styp
- type extended_context = Nitpick_HOL.extended_context
+ type hol_context = Nitpick_HOL.hol_context
type constr_spec = {
const: styp,
@@ -28,7 +28,7 @@
constrs: constr_spec list}
type scope = {
- ext_ctxt: extended_context,
+ hol_ctxt: hol_context,
card_assigns: (typ * int) list,
bits: int,
bisim_depth: int,
@@ -47,7 +47,7 @@
val scopes_equivalent : scope -> scope -> bool
val scope_less_eq : scope -> scope -> bool
val all_scopes :
- extended_context -> int -> (typ option * int list) list
+ hol_context -> int -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list
-> int list -> int list -> typ list -> typ list -> typ list
-> int * scope list
@@ -77,7 +77,7 @@
constrs: constr_spec list}
type scope = {
- ext_ctxt: extended_context,
+ hol_ctxt: hol_context,
card_assigns: (typ * int) list,
bits: int,
bisim_depth: int,
@@ -131,7 +131,7 @@
(* (string -> string) -> scope
-> string list * string list * string list * string list * string list *)
-fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns,
+fun quintuple_for_scope quote ({hol_ctxt as {thy, ctxt, ...}, card_assigns,
bits, bisim_depth, datatypes, ...} : scope) =
let
val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit}, @{typ \<xi>},
@@ -240,10 +240,9 @@
val max_bits = 31 (* Kodkod limit *)
-(* extended_context -> (typ option * int list) list
- -> (styp option * int list) list -> (styp option * int list) list -> int list
- -> int list -> typ -> block *)
-fun block_for_type (ext_ctxt as {thy, ...}) cards_assigns maxes_assigns
+(* hol_context -> (typ option * int list) list -> (styp option * int list) list
+ -> (styp option * int list) list -> int list -> int list -> typ -> block *)
+fun block_for_type (hol_ctxt as {thy, ...}) cards_assigns maxes_assigns
iters_assigns bitss bisim_depths T =
if T = @{typ unsigned_bit} then
[(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
@@ -261,18 +260,18 @@
(const_for_iterator_type T)))]
else
(Card T, lookup_type_ints_assign thy cards_assigns T) ::
- (case datatype_constrs ext_ctxt T of
+ (case datatype_constrs hol_ctxt T of
[_] => []
| constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
-(* extended_context -> (typ option * int list) list
- -> (styp option * int list) list -> (styp option * int list) list -> int list
- -> int list -> typ list -> typ list -> block list *)
-fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns bitss
+(* hol_context -> (typ option * int list) list -> (styp option * int list) list
+ -> (styp option * int list) list -> int list -> int list -> typ list
+ -> typ list -> block list *)
+fun blocks_for_types hol_ctxt cards_assigns maxes_assigns iters_assigns bitss
bisim_depths mono_Ts nonmono_Ts =
let
(* typ -> block *)
- val block_for = block_for_type ext_ctxt cards_assigns maxes_assigns
+ val block_for = block_for_type hol_ctxt cards_assigns maxes_assigns
iters_assigns bitss bisim_depths
val mono_block = maps block_for mono_Ts
val nonmono_blocks = map block_for nonmono_Ts
@@ -313,10 +312,10 @@
type scope_desc = (typ * int) list * (styp * int) list
-(* extended_context -> scope_desc -> typ * int -> bool *)
-fun is_surely_inconsistent_card_assign ext_ctxt (card_assigns, max_assigns)
+(* hol_context -> scope_desc -> typ * int -> bool *)
+fun is_surely_inconsistent_card_assign hol_ctxt (card_assigns, max_assigns)
(T, k) =
- case datatype_constrs ext_ctxt T of
+ case datatype_constrs hol_ctxt T of
[] => false
| xs =>
let
@@ -329,20 +328,20 @@
| effective_max card max = Int.min (card, max)
val max = map2 effective_max dom_cards maxes |> Integer.sum
in max < k end
-(* extended_context -> (typ * int) list -> (typ * int) list
- -> (styp * int) list -> bool *)
-fun is_surely_inconsistent_scope_description ext_ctxt seen rest max_assigns =
- exists (is_surely_inconsistent_card_assign ext_ctxt
+(* hol_context -> (typ * int) list -> (typ * int) list -> (styp * int) list
+ -> bool *)
+fun is_surely_inconsistent_scope_description hol_ctxt seen rest max_assigns =
+ exists (is_surely_inconsistent_card_assign hol_ctxt
(seen @ rest, max_assigns)) seen
-(* extended_context -> scope_desc -> (typ * int) list option *)
-fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) =
+(* hol_context -> scope_desc -> (typ * int) list option *)
+fun repair_card_assigns hol_ctxt (card_assigns, max_assigns) =
let
(* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
fun aux seen [] = SOME seen
| aux seen ((T, 0) :: _) = NONE
| aux seen ((T, k) :: rest) =
- (if is_surely_inconsistent_scope_description ext_ctxt ((T, k) :: seen)
+ (if is_surely_inconsistent_scope_description hol_ctxt ((T, k) :: seen)
rest max_assigns then
raise SAME ()
else
@@ -374,12 +373,12 @@
(* block -> scope_desc *)
fun scope_descriptor_from_block block =
fold_rev add_row_to_scope_descriptor block ([], [])
-(* extended_context -> block list -> int list -> scope_desc option *)
-fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns =
+(* hol_context -> block list -> int list -> scope_desc option *)
+fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) blocks columns =
let
val (card_assigns, max_assigns) =
maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
- val card_assigns = repair_card_assigns ext_ctxt (card_assigns, max_assigns)
+ val card_assigns = repair_card_assigns hol_ctxt (card_assigns, max_assigns)
|> the
in
SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
@@ -449,25 +448,25 @@
explicit_max = max, total = total} :: constrs
end
-(* extended_context -> (typ * int) list -> typ -> bool *)
-fun has_exact_card ext_ctxt card_assigns T =
+(* hol_context -> (typ * int) list -> typ -> bool *)
+fun has_exact_card hol_ctxt card_assigns T =
let val card = card_of_type card_assigns T in
- card = bounded_exact_card_of_type ext_ctxt (card + 1) 0 card_assigns T
+ card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
end
-(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
-fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) deep_dataTs
+(* hol_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
+fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) deep_dataTs
(desc as (card_assigns, _)) (T, card) =
let
val deep = member (op =) deep_dataTs T
val co = is_codatatype thy T
- val xs = boxed_datatype_constrs ext_ctxt T
+ val xs = boxed_datatype_constrs hol_ctxt T
val self_recs = map (is_self_recursive_constr_type o snd) xs
val (num_self_recs, num_non_self_recs) =
List.partition I self_recs |> pairself length
- val complete = has_exact_card ext_ctxt card_assigns T
+ val complete = has_exact_card hol_ctxt card_assigns T
val concrete = xs |> maps (binder_types o snd) |> maps binder_types
- |> forall (has_exact_card ext_ctxt card_assigns)
+ |> forall (has_exact_card hol_ctxt card_assigns)
(* int -> int *)
fun sum_dom_cards max =
map (domain_card max card_assigns o snd) xs |> Integer.sum
@@ -487,12 +486,12 @@
min_bits_for_nat_value (fold Integer.max
(map snd card_assigns @ map snd max_assigns) 0)
-(* extended_context -> int -> typ list -> scope_desc -> scope *)
-fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break deep_dataTs
+(* hol_context -> int -> typ list -> scope_desc -> scope *)
+fun scope_from_descriptor (hol_ctxt as {thy, ...}) sym_break deep_dataTs
(desc as (card_assigns, _)) =
let
val datatypes =
- map (datatype_spec_from_scope_descriptor ext_ctxt deep_dataTs desc)
+ map (datatype_spec_from_scope_descriptor hol_ctxt deep_dataTs desc)
(filter (is_datatype thy o fst) card_assigns)
val bits = card_of_type card_assigns @{typ signed_bit} - 1
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
@@ -500,7 +499,7 @@
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
in
- {ext_ctxt = ext_ctxt, card_assigns = card_assigns, datatypes = datatypes,
+ {hol_ctxt = hol_ctxt, card_assigns = card_assigns, datatypes = datatypes,
bits = bits, bisim_depth = bisim_depth,
ofs = if sym_break <= 0 then Typtab.empty
else offset_table_for_card_assigns thy card_assigns datatypes}
@@ -521,26 +520,26 @@
val max_scopes = 4096
val distinct_threshold = 512
-(* extended_context -> int -> (typ option * int list) list
+(* hol_context -> int -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list -> int list
-> typ list -> typ list -> typ list -> int * scope list *)
-fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
+fun all_scopes (hol_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
let
val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
cards_assigns
- val blocks = blocks_for_types ext_ctxt cards_assigns maxes_assigns
+ val blocks = blocks_for_types hol_ctxt cards_assigns maxes_assigns
iters_assigns bitss bisim_depths mono_Ts
nonmono_Ts
val ranks = map rank_of_block blocks
val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
val head = take max_scopes all
- val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
+ val descs = map_filter (scope_descriptor_from_combination hol_ctxt blocks)
head
in
(length all - length head,
descs |> length descs <= distinct_threshold ? distinct (op =)
- |> map (scope_from_descriptor ext_ctxt sym_break deep_dataTs))
+ |> map (scope_from_descriptor hol_ctxt sym_break deep_dataTs))
end
end;