# HG changeset patch # User blanchet # Date 1266000277 -3600 # Node ID 168041f24f8082f97b2cf1307aaae54d27a4ba04 # Parent e385fa5074685e4d6630f009e7d697f5a9a17bc6 various cosmetic changes to Nitpick diff -r e385fa507468 -r 168041f24f80 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Wed Feb 10 11:47:33 2010 +0100 +++ b/src/HOL/Nitpick.thy Fri Feb 12 19:44:37 2010 +0100 @@ -37,7 +37,7 @@ and bisim_iterator_max :: bisim_iterator and Quot :: "'a \ 'b" and quot_normal :: "'a \ 'a" - and NonStd :: "'a \ 'b" + and Silly :: "'a \ 'b" and Tha :: "('a \ bool) \ 'a" datatype ('a, 'b) pair_box = PairBox 'a 'b @@ -254,7 +254,7 @@ setup {* Nitpick_Isar.setup *} hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim - bisim_iterator_max Quot quot_normal NonStd Tha PairBox FunBox Word refl' wf' + bisim_iterator_max Quot quot_normal Silly Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac diff -r e385fa507468 -r 168041f24f80 src/HOL/Tools/Nitpick/kodkod_sat.ML --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Wed Feb 10 11:47:33 2010 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Fri Feb 12 19:44:37 2010 +0100 @@ -9,7 +9,7 @@ sig val configured_sat_solvers : bool -> string list val smart_sat_solver_name : bool -> string - val sat_solver_spec : bool -> string -> string * string list + val sat_solver_spec : string -> string * string list end; structure Kodkod_SAT : KODKOD_SAT = @@ -51,15 +51,15 @@ ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"], "s SATISFIABLE", "v ", "s UNSATISFIABLE"))] -(* bool -> string -> sink -> string -> string -> string list -> string list +(* string -> sink -> string -> string -> string list -> string list -> (string * (unit -> string list)) option *) -fun dynamic_entry_for_external overlord name dev home exec args markers = +fun dynamic_entry_for_external name dev home exec args markers = case getenv home of "" => NONE | dir => SOME (name, fn () => let - val serial_str = if overlord then "" else serial_string () + val serial_str = serial_string () val base = name ^ serial_str val out_file = base ^ ".out" val dir_sep = @@ -76,9 +76,9 @@ end) (* bool -> bool -> string * sat_solver_info -> (string * (unit -> string list)) option *) -fun dynamic_entry_for_info _ incremental (name, Internal (Java, mode, ss)) = +fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) = if incremental andalso mode = Batch then NONE else SOME (name, K ss) - | dynamic_entry_for_info _ incremental (name, Internal (JNI, mode, ss)) = + | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) = if incremental andalso mode = Batch then NONE else @@ -92,26 +92,25 @@ else NONE end - | dynamic_entry_for_info overlord false - (name, External (dev, home, exec, args)) = - dynamic_entry_for_external overlord name dev home exec args [] - | dynamic_entry_for_info overlord false + | dynamic_entry_for_info false (name, External (dev, home, exec, args)) = + dynamic_entry_for_external name dev home exec args [] + | dynamic_entry_for_info false (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) = - dynamic_entry_for_external overlord name dev home exec args [m1, m2, m3] - | dynamic_entry_for_info _ true _ = NONE -(* bool -> bool -> (string * (unit -> string list)) list *) -fun dynamic_list overlord incremental = - map_filter (dynamic_entry_for_info overlord incremental) static_list + dynamic_entry_for_external name dev home exec args [m1, m2, m3] + | dynamic_entry_for_info true _ = NONE +(* bool -> (string * (unit -> string list)) list *) +fun dynamic_list incremental = + map_filter (dynamic_entry_for_info incremental) static_list (* bool -> string list *) -val configured_sat_solvers = map fst o dynamic_list false +val configured_sat_solvers = map fst o dynamic_list (* bool -> string *) -val smart_sat_solver_name = fst o hd o dynamic_list false +val smart_sat_solver_name = fst o hd o dynamic_list -(* bool -> string -> string * string list *) -fun sat_solver_spec overlord name = +(* string -> string * string list *) +fun sat_solver_spec name = let - val dyn_list = dynamic_list overlord false + val dyn_list = dynamic_list false (* (string * 'a) list -> string *) fun enum_solvers solvers = commas (distinct (op =) (map (quote o fst) solvers)) diff -r e385fa507468 -r 168041f24f80 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 10 11:47:33 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Feb 12 19:44:37 2010 +0100 @@ -398,7 +398,7 @@ val _ = if standard andalso not (null induct_dataTs) then pprint_m (fn () => Pretty.blk (0, pstrs "Hint: To check that the induction hypothesis is \ - \general enough, try the following command: " @ + \general enough, try this command: " @ [Pretty.mark Markup.sendback (Pretty.blk (0, pstrs ("nitpick [" ^ commas (map (prefix "non_std " o maybe_quote @@ -504,7 +504,7 @@ val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^ PrintMode.setmp [] multiline_string_for_scope scope val kodkod_sat_solver = - Kodkod_SAT.sat_solver_spec overlord effective_sat_solver |> snd + Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd val bit_width = if bits = 0 then 16 else bits + 1 val delay = if liberal then Option.map (fn time => Time.- (time, Time.now ())) diff -r e385fa507468 -r 168041f24f80 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 10 11:47:33 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 12 19:44:37 2010 +0100 @@ -844,7 +844,7 @@ (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T)) constrs |> (triple_lookup (type_match thy) stds T |> the |> not) ? - cons (@{const_name NonStd}, @{typ \} --> T) + cons (@{const_name Silly}, @{typ \} --> T) end | NONE => if is_record_type T then @@ -1393,7 +1393,7 @@ fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T = let val xs = datatype_constrs hol_ctxt dataT - val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs + val xs' = filter_out (curry (op =) @{const_name Silly} o fst) xs val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs' in (if length xs = length xs' then diff -r e385fa507468 -r 168041f24f80 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Feb 10 11:47:33 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Feb 12 19:44:37 2010 +0100 @@ -317,7 +317,7 @@ [ts] |> not exclusive ? cons (KK.TupleSet []) else [KK.TupleSet [], - if (* ### exclusive andalso*) T1 = T2 andalso epsilon > delta then + if T1 = T2 andalso epsilon > delta then index_seq delta (epsilon - delta) |> map (fn j => KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]], @@ -770,45 +770,47 @@ val empty_rel = KK.Product (KK.None, KK.None) (* nfa_table -> typ -> typ -> KK.rel_expr list *) -fun direct_path_rel_exprs nfa start final = - case AList.lookup (op =) nfa final of - SOME trans => map fst (filter (curry (op =) start o snd) trans) +fun direct_path_rel_exprs nfa start_T final_T = + case AList.lookup (op =) nfa final_T of + SOME trans => map fst (filter (curry (op =) start_T o snd) trans) | NONE => [] (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> KK.rel_expr *) -and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final = - fold kk_union (direct_path_rel_exprs nfa start final) - (if start = final then KK.Iden else empty_rel) - | any_path_rel_expr (kk as {kk_union, ...}) nfa (q :: qs) start final = - kk_union (any_path_rel_expr kk nfa qs start final) - (knot_path_rel_expr kk nfa qs start q final) +and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T + final_T = + fold kk_union (direct_path_rel_exprs nfa start_T final_T) + (if start_T = final_T then KK.Iden else empty_rel) + | any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T = + kk_union (any_path_rel_expr kk nfa Ts start_T final_T) + (knot_path_rel_expr kk nfa Ts start_T T final_T) (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> typ -> KK.rel_expr *) -and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa qs start - knot final = - kk_join (kk_join (any_path_rel_expr kk nfa qs knot final) - (kk_reflexive_closure (loop_path_rel_expr kk nfa qs knot))) - (any_path_rel_expr kk nfa qs start knot) +and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts + start_T knot_T final_T = + kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T) + (kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T))) + (any_path_rel_expr kk nfa Ts start_T knot_T) (* kodkod_constrs -> nfa_table -> typ list -> typ -> KK.rel_expr *) -and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start = - fold kk_union (direct_path_rel_exprs nfa start start) empty_rel - | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (q :: qs) start = - if start = q then - kk_closure (loop_path_rel_expr kk nfa qs start) +and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T = + fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel + | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts) + start_T = + if start_T = T then + kk_closure (loop_path_rel_expr kk nfa Ts start_T) else - kk_union (loop_path_rel_expr kk nfa qs start) - (knot_path_rel_expr kk nfa qs start q start) + kk_union (loop_path_rel_expr kk nfa Ts start_T) + (knot_path_rel_expr kk nfa Ts start_T T start_T) (* nfa_table -> unit NfaGraph.T *) fun graph_for_nfa nfa = let (* typ -> unit NfaGraph.T -> unit NfaGraph.T *) - fun new_node q = perhaps (try (NfaGraph.new_node (q, ()))) + fun new_node T = perhaps (try (NfaGraph.new_node (T, ()))) (* nfa_table -> unit NfaGraph.T -> unit NfaGraph.T *) fun add_nfa [] = I | add_nfa ((_, []) :: nfa) = add_nfa nfa - | add_nfa ((q, ((_, q') :: transitions)) :: nfa) = - add_nfa ((q, transitions) :: nfa) o NfaGraph.add_edge (q, q') o - new_node q' o new_node q + | add_nfa ((T, ((_, T') :: transitions)) :: nfa) = + add_nfa ((T, transitions) :: nfa) o NfaGraph.add_edge (T, T') o + new_node T' o new_node T in add_nfa nfa NfaGraph.empty end (* nfa_table -> nfa_table list *) @@ -816,17 +818,17 @@ nfa |> graph_for_nfa |> NfaGraph.strong_conn |> map (fn keys => filter (member (op =) keys o fst) nfa) -(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> KK.formula *) -fun acyclicity_axiom_for_datatype dtypes kk nfa start = +(* kodkod_constrs -> dtype_spec list -> nfa_table -> typ -> KK.formula *) +fun acyclicity_axiom_for_datatype kk dtypes nfa start_T = #kk_no kk (#kk_intersect kk - (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden) + (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden) (* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> KK.formula list *) fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes = map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes |> strongly_connected_sub_nfas - |> maps (fn nfa => map (acyclicity_axiom_for_datatype dtypes kk nfa o fst) - nfa) + |> maps (fn nfa => + map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa) (* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr -> constr_spec -> int -> KK.formula *) diff -r e385fa507468 -r 168041f24f80 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 10 11:47:33 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Feb 12 19:44:37 2010 +0100 @@ -88,7 +88,7 @@ Const (nth_atom_name pool "" T j k, T) (* term -> real *) -fun extract_real_number (Const (@{const_name Rings.divide}, _) $ t1 $ t2) = +fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) = real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2)) | extract_real_number t = real (snd (HOLogic.dest_number t)) (* term * term -> order *) @@ -459,7 +459,7 @@ 0 => mk_num 0 | n1 => case HOLogic.dest_number t2 |> snd of 1 => mk_num n1 - | n2 => Const (@{const_name Rings.divide}, + | n2 => Const (@{const_name divide}, num_T --> num_T --> num_T) $ mk_num n1 $ mk_num n2) | _ => raise TERM ("Nitpick_Model.reconstruct_term.\ @@ -470,7 +470,7 @@ constr_s = @{const_name Quot}) then Const (abs_name, constr_T) $ the_single ts else if not for_auto andalso - constr_s = @{const_name NonStd} then + constr_s = @{const_name Silly} then Const (fst (dest_Const (the_single ts)), T) else list_comb (Const constr_x, ts)