# HG changeset patch # User blanchet # Date 1265295795 -3600 # Node ID 96136eb6218f64d31f1dcec428b17e06118a16a7 # Parent 5e492a862b344e01b46c669113eab37fa04eadd4 split "nitpick_hol.ML" into two files to make it more manageable; more refactoring to come diff -r 5e492a862b34 -r 96136eb6218f src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Feb 04 13:36:52 2010 +0100 +++ b/src/HOL/IsaMakefile Thu Feb 04 16:03:15 2010 +0100 @@ -206,6 +206,7 @@ Tools/Nitpick/nitpick_mono.ML \ Tools/Nitpick/nitpick_nut.ML \ Tools/Nitpick/nitpick_peephole.ML \ + Tools/Nitpick/nitpick_preproc.ML \ Tools/Nitpick/nitpick_rep.ML \ Tools/Nitpick/nitpick_scope.ML \ Tools/Nitpick/nitpick_tests.ML \ diff -r 5e492a862b34 -r 96136eb6218f src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Thu Feb 04 13:36:52 2010 +0100 +++ b/src/HOL/Nitpick.thy Thu Feb 04 16:03:15 2010 +0100 @@ -13,6 +13,7 @@ ("Tools/Nitpick/kodkod_sat.ML") ("Tools/Nitpick/nitpick_util.ML") ("Tools/Nitpick/nitpick_hol.ML") + ("Tools/Nitpick/nitpick_preproc.ML") ("Tools/Nitpick/nitpick_mono.ML") ("Tools/Nitpick/nitpick_scope.ML") ("Tools/Nitpick/nitpick_peephole.ML") @@ -237,6 +238,7 @@ use "Tools/Nitpick/kodkod_sat.ML" use "Tools/Nitpick/nitpick_util.ML" use "Tools/Nitpick/nitpick_hol.ML" +use "Tools/Nitpick/nitpick_preproc.ML" use "Tools/Nitpick/nitpick_mono.ML" use "Tools/Nitpick/nitpick_scope.ML" use "Tools/Nitpick/nitpick_peephole.ML" diff -r 5e492a862b34 -r 96136eb6218f src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 04 13:36:52 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 04 16:03:15 2010 +0100 @@ -69,6 +69,7 @@ open Nitpick_Util open Nitpick_HOL +open Nitpick_Preproc open Nitpick_Mono open Nitpick_Scope open Nitpick_Peephole @@ -273,7 +274,7 @@ val intro_table = inductive_intro_table ctxt def_table val ground_thm_table = ground_theorem_table thy val ersatz_table = ersatz_table thy - val (ext_ctxt as {wf_cache, ...}) = + val (hol_ctxt as {wf_cache, ...}) = {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, binary_ints = binary_ints, destroy_constrs = destroy_constrs, @@ -292,7 +293,7 @@ val _ = null (Term.add_tvars assms_t []) orelse raise NOT_SUPPORTED "schematic type variables" val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)), - core_t) = preprocess_term ext_ctxt assms_t + core_t) = preprocess_term hol_ctxt assms_t val got_all_user_axioms = got_all_mono_user_axioms andalso no_poly_user_axioms @@ -319,9 +320,9 @@ handle TYPE (_, Ts, ts) => raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts) - val core_u = nut_from_term ext_ctxt Eq core_t - val def_us = map (nut_from_term ext_ctxt DefEq) def_ts - val nondef_us = map (nut_from_term ext_ctxt Eq) nondef_ts + val core_u = nut_from_term hol_ctxt Eq core_t + val def_us = map (nut_from_term hol_ctxt DefEq) def_ts + val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts val (free_names, const_names) = fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], []) val (sel_names, nonsel_names) = @@ -344,12 +345,12 @@ case triple_lookup (type_match thy) monos T of SOME (SOME b) => b | _ => is_type_always_monotonic T orelse - formulas_monotonic ext_ctxt T Plus def_ts nondef_ts core_t + formulas_monotonic hol_ctxt T Plus def_ts nondef_ts core_t fun is_deep_datatype T = is_datatype thy T andalso (is_word_type T orelse exists (curry (op =) T o domain_type o type_of) sel_names) - val all_Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts) + val all_Ts = ground_types_in_terms hol_ctxt (core_t :: def_ts @ nondef_ts) |> sort TermOrd.typ_ord val _ = if verbose andalso binary_ints = SOME true andalso exists (member (op =) [nat_T, int_T]) all_Ts then @@ -522,7 +523,7 @@ val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels - val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt bits ofs kk + val dtype_axioms = declarative_axioms_for_datatypes hol_ctxt bits ofs kk rel_table datatypes val declarative_axioms = plain_axioms @ dtype_axioms val univ_card = univ_card nat_card int_card main_j0 @@ -553,7 +554,7 @@ if loc = "Nitpick_Kodkod.check_arity" andalso not (Typtab.is_empty ofs) then problem_for_scope liberal - {ext_ctxt = ext_ctxt, card_assigns = card_assigns, + {hol_ctxt = hol_ctxt, card_assigns = card_assigns, bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = Typtab.empty} else if loc = "Nitpick.pick_them_nits_in_term.\ @@ -891,7 +892,7 @@ end val (skipped, the_scopes) = - all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns + all_scopes hol_ctxt sym_break cards_assigns maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs val _ = if skipped > 0 then print_m (fn () => "Too many scopes. Skipping " ^ diff -r 5e492a862b34 -r 96136eb6218f src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 04 13:36:52 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 04 16:03:15 2010 +0100 @@ -13,7 +13,7 @@ type unrolled = styp * styp type wf_cache = (styp * (bool * bool)) list - type extended_context = { + type hol_context = { thy: theory, ctxt: Proof.context, max_bisim_depth: int, @@ -46,12 +46,24 @@ wf_cache: wf_cache Unsynchronized.ref, constr_cache: (typ * styp list) list Unsynchronized.ref} + datatype fixpoint_kind = Lfp | Gfp | NoFp + datatype boxability = + InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2 + val name_sep : string val numeral_prefix : string + val ubfp_prefix : string + val lbfp_prefix : string val skolem_prefix : string + val special_prefix : string + val uncurry_prefix : string val eval_prefix : string val original_name : string -> string val s_conj : term * term -> term + val s_disj : term * term -> term + val strip_any_connective : term -> term list * term + val conjuncts_of : term -> term list + val disjuncts_of : term -> term list val unbit_and_unbox_type : typ -> typ val string_for_type : Proof.context -> typ -> string val prefix_name : string -> string -> string @@ -76,6 +88,7 @@ val is_record_type : typ -> bool val is_number_type : theory -> typ -> bool val const_for_iterator_type : typ -> styp + val strip_n_binders : int -> typ -> typ list * typ val nth_range_type : int -> typ -> typ val num_factors_in_type : typ -> int val num_binder_types : typ -> int @@ -96,15 +109,18 @@ val is_rep_fun : theory -> styp -> bool val is_quot_abs_fun : Proof.context -> styp -> bool val is_quot_rep_fun : Proof.context -> styp -> bool + val mate_of_rep_fun : theory -> styp -> styp + val is_constr_like : theory -> styp -> bool + val is_stale_constr : theory -> styp -> bool val is_constr : theory -> styp -> bool - val is_stale_constr : theory -> styp -> bool val is_sel : string -> bool val is_sel_like_and_no_discr : string -> bool + val box_type : hol_context -> boxability -> typ -> typ val discr_for_constr : styp -> styp val num_sels_for_constr_type : typ -> int val nth_sel_name_for_constr_name : string -> int -> string val nth_sel_for_constr : styp -> int -> styp - val boxed_nth_sel_for_constr : extended_context -> styp -> int -> styp + val boxed_nth_sel_for_constr : hol_context -> styp -> int -> styp val sel_no_from_name : string -> int val eta_expand : typ list -> term -> int -> term val extensionalize : term -> term @@ -113,19 +129,25 @@ val unregister_frac_type : string -> theory -> theory val register_codatatype : typ -> string -> styp list -> theory -> theory val unregister_codatatype : typ -> theory -> theory - val datatype_constrs : extended_context -> typ -> styp list - val boxed_datatype_constrs : extended_context -> typ -> styp list - val num_datatype_constrs : extended_context -> typ -> int + val datatype_constrs : hol_context -> typ -> styp list + val boxed_datatype_constrs : hol_context -> typ -> styp list + val num_datatype_constrs : hol_context -> typ -> int val constr_name_for_sel_like : string -> string - val boxed_constr_for_sel : extended_context -> styp -> styp + val boxed_constr_for_sel : hol_context -> styp -> styp + val discriminate_value : hol_context -> styp -> term -> term + val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term + val construct_value : theory -> styp -> term list -> term val card_of_type : (typ * int) list -> typ -> int val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int val bounded_exact_card_of_type : - extended_context -> int -> int -> (typ * int) list -> typ -> int - val is_finite_type : extended_context -> typ -> bool + hol_context -> int -> int -> (typ * int) list -> typ -> int + val is_finite_type : hol_context -> typ -> bool + val special_bounds : term list -> (indexname * typ) list + val is_funky_typedef : theory -> typ -> bool val all_axioms_of : theory -> term list * term list * term list val arity_of_built_in_const : bool -> styp -> int option val is_built_in_const : bool -> styp -> bool + val term_under_def : term -> term val case_const_names : theory -> (string * int) list val const_def_table : Proof.context -> term list -> const_table val const_nondef_table : term list -> const_table @@ -134,22 +156,33 @@ val inductive_intro_table : Proof.context -> const_table -> const_table val ground_theorem_table : theory -> term list Inttab.table val ersatz_table : theory -> (string * string) list + val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit + val inverse_axioms_for_rep_fun : theory -> styp -> term list + val optimized_typedef_axioms : theory -> string * typ list -> term list + val optimized_quot_type_axioms : theory -> string * typ list -> term list val def_of_const : theory -> const_table -> styp -> term option - val is_inductive_pred : extended_context -> styp -> bool + val fixpoint_kind_of_const : + theory -> const_table -> string * typ -> fixpoint_kind + val is_inductive_pred : hol_context -> styp -> bool + val is_equational_fun : hol_context -> styp -> bool val is_constr_pattern_lhs : theory -> term -> bool val is_constr_pattern_formula : theory -> term -> bool + val unfold_defs_in_term : hol_context -> term -> term + val codatatype_bisim_axioms : hol_context -> typ -> term list + val is_well_founded_inductive_pred : hol_context -> styp -> bool + val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term + val equational_fun_axioms : hol_context -> styp -> term list + val is_equational_fun_surely_complete : hol_context -> styp -> bool val merge_type_vars_in_terms : term list -> term list - val ground_types_in_type : extended_context -> typ -> typ list - val ground_types_in_terms : extended_context -> term list -> typ list + val ground_types_in_type : hol_context -> typ -> typ list + val ground_types_in_terms : hol_context -> term list -> typ list val format_type : int list -> int list -> typ -> typ val format_term_type : theory -> const_table -> (term option * int list) list -> term -> typ val user_friendly_const : - extended_context -> string * string -> (term option * int list) list + hol_context -> string * string -> (term option * int list) list -> styp -> term * typ val assign_operator_for_const : styp -> string - val preprocess_term : - extended_context -> term -> ((term list * term list) * (bool * bool)) * term end; structure Nitpick_HOL : NITPICK_HOL = @@ -162,7 +195,7 @@ type unrolled = styp * styp type wf_cache = (styp * (bool * bool)) list -type extended_context = { +type hol_context = { thy: theory, ctxt: Proof.context, max_bisim_depth: int, @@ -195,6 +228,10 @@ wf_cache: wf_cache Unsynchronized.ref, constr_cache: (typ * styp list) list Unsynchronized.ref} +datatype fixpoint_kind = Lfp | Gfp | NoFp +datatype boxability = + InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2 + structure Data = Theory_Data( type T = {frac_types: (string * (string * string) list) list, codatatypes: (string * (string * styp list)) list} @@ -222,20 +259,11 @@ val special_prefix = nitpick_prefix ^ "sp" val uncurry_prefix = nitpick_prefix ^ "unc" val eval_prefix = nitpick_prefix ^ "eval" -val bound_var_prefix = "b" -val cong_var_prefix = "c" val iter_var_prefix = "i" -val val_var_prefix = nitpick_prefix ^ "v" val arg_var_prefix = "x" (* int -> string *) fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep -fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep -(* int -> int -> string *) -fun skolem_prefix_for k j = - skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep -fun uncurry_prefix_for k j = - uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep (* string -> string * string *) val strip_first_name_sep = @@ -260,9 +288,6 @@ | s_disj (t1, t2) = if t1 = @{const True} orelse t2 = @{const True} then @{const True} else HOLogic.mk_disj (t1, t2) -(* term -> term -> term *) -fun mk_exists v t = - HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t) (* term -> term -> term list *) fun strip_connective conn_t (t as (t0 $ t1 $ t2)) = @@ -276,8 +301,8 @@ ([t], @{const Not}) | strip_any_connective t = ([t], @{const Not}) (* term -> term list *) -val conjuncts = strip_connective @{const "op &"} -val disjuncts = strip_connective @{const "op |"} +val conjuncts_of = strip_connective @{const "op &"} +val disjuncts_of = strip_connective @{const "op |"} (* When you add constants to these lists, make sure to handle them in "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as @@ -373,8 +398,6 @@ fun shortest_name s = List.last (space_explode "." s) handle List.Empty => "" (* string -> term -> term *) val prefix_abs_vars = Term.map_abs_vars o prefix_name -(* term -> term *) -val shorten_abs_vars = Term.map_abs_vars shortest_name (* string -> string *) fun short_name s = case space_explode name_sep s of @@ -441,7 +464,7 @@ | const_for_iterator_type T = raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) -(* int -> typ -> typ * typ *) +(* int -> typ -> typ list * typ *) fun strip_n_binders 0 T = ([], T) | strip_n_binders n (Type ("fun", [T1, T2])) = strip_n_binders (n - 1) T2 |>> cons T1 @@ -552,7 +575,7 @@ val is_real_datatype = is_some oo Datatype.get_info (* theory -> typ -> bool *) fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *) - | is_quot_type _ (Type ("FSet.fset", _)) = true (* FIXME *) + | is_quot_type _ (Type ("FSet.fset", _)) = true | is_quot_type _ _ = false fun is_codatatype thy (T as Type (s, _)) = not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s @@ -619,11 +642,11 @@ | NONE => false) | is_rep_fun _ _ = false (* Proof.context -> styp -> bool *) -fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* FIXME *) - | is_quot_abs_fun _ ("FSet.abs_fset", _) = true (* FIXME *) +fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true + | is_quot_abs_fun _ ("FSet.abs_fset", _) = true | is_quot_abs_fun _ _ = false -fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* FIXME *) - | is_quot_rep_fun _ ("FSet.rep_fset", _) = true (* FIXME *) +fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true + | is_quot_rep_fun _ ("FSet.rep_fset", _) = true | is_quot_rep_fun _ _ = false (* theory -> styp -> styp *) @@ -682,9 +705,6 @@ String.isPrefix sel_prefix orf (member (op =) [@{const_name fst}, @{const_name snd}]) -datatype boxability = - InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2 - (* boxability -> boxability *) fun in_fun_lhs_for InConstr = InSel | in_fun_lhs_for _ = InFunLHS @@ -693,8 +713,8 @@ | in_fun_rhs_for InFunRHS1 = InFunRHS2 | in_fun_rhs_for _ = InFunRHS1 -(* extended_context -> boxability -> typ -> bool *) -fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T = +(* hol_context -> boxability -> typ -> bool *) +fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T = case T of Type ("fun", _) => (boxy = InPair orelse boxy = InFunLHS) andalso @@ -702,31 +722,31 @@ | Type ("*", Ts) => boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse ((boxy = InExpr orelse boxy = InFunLHS) andalso - exists (is_boxing_worth_it ext_ctxt InPair) - (map (box_type ext_ctxt InPair) Ts)) + exists (is_boxing_worth_it hol_ctxt InPair) + (map (box_type hol_ctxt InPair) Ts)) | _ => false -(* extended_context -> boxability -> string * typ list -> string *) -and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) = +(* hol_context -> boxability -> string * typ list -> string *) +and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) = case triple_lookup (type_match thy) boxes (Type z) of SOME (SOME box_me) => box_me - | _ => is_boxing_worth_it ext_ctxt boxy (Type z) -(* extended_context -> boxability -> typ -> typ *) -and box_type ext_ctxt boxy T = + | _ => is_boxing_worth_it hol_ctxt boxy (Type z) +(* hol_context -> boxability -> typ -> typ *) +and box_type hol_ctxt boxy T = case T of Type (z as ("fun", [T1, T2])) => if boxy <> InConstr andalso boxy <> InSel andalso - should_box_type ext_ctxt boxy z then + should_box_type hol_ctxt boxy z then Type (@{type_name fun_box}, - [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2]) + [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2]) else - box_type ext_ctxt (in_fun_lhs_for boxy) T1 - --> box_type ext_ctxt (in_fun_rhs_for boxy) T2 + box_type hol_ctxt (in_fun_lhs_for boxy) T1 + --> box_type hol_ctxt (in_fun_rhs_for boxy) T2 | Type (z as ("*", Ts)) => if boxy <> InConstr andalso boxy <> InSel - andalso should_box_type ext_ctxt boxy z then - Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts) + andalso should_box_type hol_ctxt boxy z then + Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts) else - Type ("*", map (box_type ext_ctxt + Type ("*", map (box_type hol_ctxt (if boxy = InConstr orelse boxy = InSel then boxy else InPair)) Ts) | _ => T @@ -747,9 +767,9 @@ | nth_sel_for_constr (s, T) n = (nth_sel_name_for_constr_name s n, body_type T --> nth (maybe_curried_binder_types T) n) -(* extended_context -> styp -> int -> styp *) -fun boxed_nth_sel_for_constr ext_ctxt = - apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr +(* hol_context -> styp -> int -> styp *) +fun boxed_nth_sel_for_constr hol_ctxt = + apsnd (box_type hol_ctxt InSel) oo nth_sel_for_constr (* string -> int *) fun sel_no_from_name s = @@ -791,8 +811,8 @@ fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T) fun suc_const T = Const (@{const_name Suc}, T --> T) -(* extended_context -> typ -> styp list *) -fun uncached_datatype_constrs ({thy, stds, ...} : extended_context) +(* hol_context -> typ -> styp list *) +fun uncached_datatype_constrs ({thy, stds, ...} : hol_context) (T as Type (s, Ts)) = (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs' @@ -829,49 +849,49 @@ else []) | uncached_datatype_constrs _ _ = [] -(* extended_context -> typ -> styp list *) -fun datatype_constrs (ext_ctxt as {constr_cache, ...}) T = +(* hol_context -> typ -> styp list *) +fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T = case AList.lookup (op =) (!constr_cache) T of SOME xs => xs | NONE => - let val xs = uncached_datatype_constrs ext_ctxt T in + let val xs = uncached_datatype_constrs hol_ctxt T in (Unsynchronized.change constr_cache (cons (T, xs)); xs) end -fun boxed_datatype_constrs ext_ctxt = - map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt -(* extended_context -> typ -> int *) +fun boxed_datatype_constrs hol_ctxt = + map (apsnd (box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt +(* hol_context -> typ -> int *) val num_datatype_constrs = length oo datatype_constrs (* string -> string *) fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair} | constr_name_for_sel_like @{const_name snd} = @{const_name Pair} | constr_name_for_sel_like s' = original_name s' -(* extended_context -> styp -> styp *) -fun boxed_constr_for_sel ext_ctxt (s', T') = +(* hol_context -> styp -> styp *) +fun boxed_constr_for_sel hol_ctxt (s', T') = let val s = constr_name_for_sel_like s' in - AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s + AList.lookup (op =) (boxed_datatype_constrs hol_ctxt (domain_type T')) s |> the |> pair s end -(* extended_context -> styp -> term *) -fun discr_term_for_constr ext_ctxt (x as (s, T)) = +(* hol_context -> styp -> term *) +fun discr_term_for_constr hol_ctxt (x as (s, T)) = let val dataT = body_type T in if s = @{const_name Suc} then Abs (Name.uu, dataT, @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0)) - else if num_datatype_constrs ext_ctxt dataT >= 2 then + else if num_datatype_constrs hol_ctxt dataT >= 2 then Const (discr_for_constr x) else Abs (Name.uu, dataT, @{const True}) end -(* extended_context -> styp -> term -> term *) -fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t = +(* hol_context -> styp -> term -> term *) +fun discriminate_value (hol_ctxt as {thy, ...}) (x as (_, T)) t = case strip_comb t of (Const x', args) => if x = x' then @{const True} else if is_constr_like thy x' then @{const False} - else betapply (discr_term_for_constr ext_ctxt x, t) - | _ => betapply (discr_term_for_constr ext_ctxt x, t) + else betapply (discr_term_for_constr hol_ctxt x, t) + | _ => betapply (discr_term_for_constr hol_ctxt x, t) (* styp -> term -> term *) fun nth_arg_sel_term_for_constr (x as (s, T)) n = @@ -920,26 +940,6 @@ | _ => list_comb (Const x, args) end -(* extended_context -> typ -> term -> term *) -fun constr_expand (ext_ctxt as {thy, ...}) T t = - (case head_of t of - Const x => if is_constr_like thy x then t else raise SAME () - | _ => raise SAME ()) - handle SAME () => - let - val x' as (_, T') = - if is_pair_type T then - let val (T1, T2) = HOLogic.dest_prodT T in - (@{const_name Pair}, T1 --> T2 --> T) - end - else - datatype_constrs ext_ctxt T |> hd - val arg_Ts = binder_types T' - in - list_comb (Const x', map2 (select_nth_constr_arg thy x' t) - (index_seq 0 (length arg_Ts)) arg_Ts) - end - (* (typ * int) list -> typ -> int *) fun card_of_type assigns (Type ("fun", [T1, T2])) = reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) @@ -975,8 +975,8 @@ card_of_type assigns T handle TYPE ("Nitpick_HOL.card_of_type", _, _) => default_card) -(* extended_context -> int -> (typ * int) list -> typ -> int *) -fun bounded_exact_card_of_type ext_ctxt max default_card assigns T = +(* hol_context -> int -> (typ * int) list -> typ -> int *) +fun bounded_exact_card_of_type hol_ctxt max default_card assigns T = let (* typ list -> typ -> int *) fun aux avoid T = @@ -1006,13 +1006,13 @@ | @{typ bool} => 2 | @{typ unit} => 1 | Type _ => - (case datatype_constrs ext_ctxt T of + (case datatype_constrs hol_ctxt T of [] => if is_integer_type T orelse is_bit_type T then 0 else raise SAME () | constrs => let val constr_cards = - datatype_constrs ext_ctxt T + datatype_constrs hol_ctxt T |> map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd) in @@ -1024,9 +1024,9 @@ AList.lookup (op =) assigns T |> the_default default_card in Int.min (max, aux [] T) end -(* extended_context -> typ -> bool *) -fun is_finite_type ext_ctxt = - not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 [] +(* hol_context -> typ -> bool *) +fun is_finite_type hol_ctxt = + not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 [] (* term -> bool *) fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2 @@ -1052,7 +1052,7 @@ member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"}, @{type_name int}] s orelse is_frac_type thy (Type (s, [])) -(* theory -> term -> bool *) +(* theory -> typ -> bool *) fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s | is_funky_typedef _ _ = false (* term -> bool *) @@ -1199,8 +1199,6 @@ |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s) handle List.Empty => NONE -datatype fixpoint_kind = Lfp | Gfp | NoFp - (* term -> fixpoint_kind *) fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp @@ -1299,35 +1297,6 @@ Unsynchronized.change simp_table (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s))) -(* Similar to "Refute.specialize_type" but returns all matches rather than only - the first (preorder) match. *) -(* theory -> styp -> term -> term list *) -fun multi_specialize_type thy slack (x as (s, T)) t = - let - (* term -> (typ * term) list -> (typ * term) list *) - fun aux (Const (s', T')) ys = - if s = s' then - ys |> (if AList.defined (op =) ys T' then - I - else - cons (T', Refute.monomorphic_term - (Sign.typ_match thy (T', T) Vartab.empty) t) - handle Type.TYPE_MATCH => I - | Refute.REFUTE _ => - if slack then - I - else - raise NOT_SUPPORTED ("too much polymorphism in \ - \axiom involving " ^ quote s)) - else - ys - | aux _ ys = ys - in map snd (fold_aterms aux t []) end - -(* theory -> bool -> const_table -> styp -> term list *) -fun nondef_props_for_const thy slack table (x as (s, _)) = - these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x) - (* theory -> styp -> term list *) fun inverse_axioms_for_rep_fun thy (x as (_, T)) = let val abs_T = domain_type T in @@ -1336,7 +1305,7 @@ |> pairself (Refute.specialize_type thy x o prop_of o the) ||> single |> op :: end -(* theory -> styp list -> term list *) +(* theory -> string * typ list -> term list *) fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) = let val abs_T = Type abs_z in if is_univ_typedef thy abs_T then @@ -1392,15 +1361,15 @@ list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0)) (index_seq 0 (length arg_Ts)) arg_Ts) end -(* extended_context -> typ -> int * styp -> term -> term *) -fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t = +(* hol_context -> typ -> int * styp -> term -> term *) +fun add_constr_case (hol_ctxt as {thy, ...}) res_T (j, x) res_t = Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T) - $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x) + $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy (j, x) $ res_t -(* extended_context -> typ -> typ -> term *) -fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T = +(* hol_context -> typ -> typ -> term *) +fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T = let - val xs = datatype_constrs ext_ctxt dataT + val xs = datatype_constrs hol_ctxt dataT val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs' in @@ -1409,19 +1378,19 @@ val (xs'', x) = split_last xs' in constr_case_body thy (1, x) - |> fold_rev (add_constr_case ext_ctxt res_T) + |> fold_rev (add_constr_case hol_ctxt res_T) (length xs' downto 2 ~~ xs'') end else Const (@{const_name undefined}, dataT --> res_T) $ Bound 0 - |> fold_rev (add_constr_case ext_ctxt res_T) + |> fold_rev (add_constr_case hol_ctxt res_T) (length xs' downto 1 ~~ xs')) |> fold_rev (curry absdummy) (func_Ts @ [dataT]) end -(* extended_context -> string -> typ -> typ -> term -> term *) -fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t = - let val constr_x = hd (datatype_constrs ext_ctxt rec_T) in +(* hol_context -> string -> typ -> typ -> term -> term *) +fun optimized_record_get (hol_ctxt as {thy, ...}) s rec_T res_T t = + let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in case no_of_record_field thy s rec_T of ~1 => (case rec_T of Type (_, Ts as _ :: _) => @@ -1430,16 +1399,16 @@ val j = num_record_fields thy rec_T - 1 in select_nth_constr_arg thy constr_x t j res_T - |> optimized_record_get ext_ctxt s rec_T' res_T + |> optimized_record_get hol_ctxt s rec_T' res_T end | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T], [])) | j => select_nth_constr_arg thy constr_x t j res_T end -(* extended_context -> string -> typ -> term -> term -> term *) -fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t = +(* hol_context -> string -> typ -> term -> term -> term *) +fun optimized_record_update (hol_ctxt as {thy, ...}) s rec_T fun_t rec_t = let - val constr_x as (_, constr_T) = hd (datatype_constrs ext_ctxt rec_T) + val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T) val Ts = binder_types constr_T val n = length Ts val special_j = no_of_record_field thy s rec_T @@ -1450,7 +1419,7 @@ if j = special_j then betapply (fun_t, t) else if j = n - 1 andalso special_j = ~1 then - optimized_record_update ext_ctxt s + optimized_record_update hol_ctxt s (rec_T |> dest_Type |> snd |> List.last) fun_t t else t @@ -1473,19 +1442,19 @@ fixpoint_kind_of_rhs (the (def_of_const thy table x)) handle Option.Option => NoFp -(* extended_context -> styp -> bool *) +(* hol_context -> styp -> bool *) fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...} - : extended_context) x = + : hol_context) x = not (null (def_props_for_const thy fast_descrs intro_table x)) andalso fixpoint_kind_of_const thy def_table x <> NoFp fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...} - : extended_context) x = + : hol_context) x = exists (fn table => not (null (def_props_for_const thy fast_descrs table x))) [!simp_table, psimp_table] -fun is_inductive_pred ext_ctxt = - is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt) -fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) = - (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt +fun is_inductive_pred hol_ctxt = + is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt) +fun is_equational_fun (hol_ctxt as {thy, def_table, ...}) = + (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst) andf (not o has_trivial_definition thy def_table) @@ -1522,11 +1491,11 @@ SOME t' => is_constr_pattern_lhs thy t' | NONE => false +(* Prevents divergence in case of cyclic or infinite definition dependencies. *) val unfold_max_depth = 255 -val axioms_max_depth = 255 -(* extended_context -> term -> term *) -fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs, +(* hol_context -> term -> term *) +fun unfold_defs_in_term (hol_ctxt as {thy, destroy_constrs, fast_descrs, case_names, def_table, ground_thm_table, ersatz_table, ...}) = let @@ -1600,7 +1569,7 @@ val (dataT, res_T) = nth_range_type n T |> pairf domain_type range_type in - (optimized_case_def ext_ctxt dataT res_T + (optimized_case_def hol_ctxt dataT res_T |> do_term (depth + 1) Ts, ts) end | _ => @@ -1628,11 +1597,11 @@ else if is_record_get thy x then case length ts of 0 => (do_term depth Ts (eta_expand Ts t 1), []) - | _ => (optimized_record_get ext_ctxt s (domain_type T) + | _ => (optimized_record_get hol_ctxt s (domain_type T) (range_type T) (do_term depth Ts (hd ts)), tl ts) else if is_record_update thy x then case length ts of - 2 => (optimized_record_update ext_ctxt + 2 => (optimized_record_update hol_ctxt (unsuffix Record.updateN s) (nth_range_type 2 T) (do_term depth Ts (hd ts)) (do_term depth Ts (nth ts 1)), []) @@ -1645,7 +1614,7 @@ else (Const x, ts) end - else if is_equational_fun ext_ctxt x then + else if is_equational_fun hol_ctxt x then (Const x, ts) else case def_of_const thy def_table x of SOME def => @@ -1662,10 +1631,10 @@ in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end in do_term 0 [] end -(* extended_context -> typ -> term list *) -fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T = +(* hol_context -> typ -> term list *) +fun codatatype_bisim_axioms (hol_ctxt as {thy, ...}) T = let - val xs = datatype_constrs ext_ctxt T + val xs = datatype_constrs hol_ctxt T val set_T = T --> bool_T val iter_T = @{typ bisim_iterator} val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T) @@ -1688,14 +1657,14 @@ let val arg_Ts = binder_types T val core_t = - discriminate_value ext_ctxt x y_var :: + discriminate_value hol_ctxt x y_var :: map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts |> foldr1 s_conj in List.foldr absdummy core_t arg_Ts end in [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var) $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T) - $ (betapplys (optimized_case_def ext_ctxt T bool_T, + $ (betapplys (optimized_case_def hol_ctxt T bool_T, map case_func xs @ [x_var]))), HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var) $ (Const (@{const_name insert}, T --> set_T --> set_T) @@ -1754,10 +1723,10 @@ val termination_tacs = [Lexicographic_Order.lex_order_tac true, ScnpReconstruct.sizechange_tac] -(* extended_context -> const_table -> styp -> bool *) +(* hol_context -> const_table -> styp -> bool *) fun uncached_is_well_founded_inductive_pred ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...} - : extended_context) (x as (_, T)) = + : hol_context) (x as (_, T)) = case def_props_for_const thy fast_descrs intro_table x of [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive", [Const x]) @@ -1797,11 +1766,11 @@ handle List.Empty => false | NO_TRIPLE () => false -(* The type constraint below is a workaround for a Poly/ML bug. *) +(* The type constraint below is a workaround for a Poly/ML crash. *) -(* extended_context -> styp -> bool *) +(* hol_context -> styp -> bool *) fun is_well_founded_inductive_pred - (ext_ctxt as {thy, wfs, def_table, wf_cache, ...} : extended_context) + (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context) (x as (s, _)) = case triple_lookup (const_match thy) wfs x of SOME (SOME b) => b @@ -1811,7 +1780,7 @@ | NONE => let val gfp = (fixpoint_kind_of_const thy def_table x = Gfp) - val wf = uncached_is_well_founded_inductive_pred ext_ctxt x + val wf = uncached_is_well_founded_inductive_pred hol_ctxt x in Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf end @@ -1842,14 +1811,14 @@ | do_disjunct j t = case num_occs_of_bound_in_term j t of 0 => true - | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts t) + | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t) | _ => false (* term -> bool *) fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) = let val (xs, body) = strip_abs t2 in case length xs of 1 => false - | n => forall (do_disjunct (n - 1)) (disjuncts body) + | n => forall (do_disjunct (n - 1)) (disjuncts_of body) end | do_lfp_def _ = false in do_lfp_def o strip_abs_body end @@ -1887,7 +1856,7 @@ end val (nonrecs, recs) = List.partition (curry (op =) 0 o num_occs_of_bound_in_term j) - (disjuncts body) + (disjuncts_of body) val base_body = nonrecs |> List.foldl s_disj @{const False} val step_body = recs |> map (repair_rec j) |> List.foldl s_disj @{const False} @@ -1901,8 +1870,8 @@ raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t]) in aux end -(* extended_context -> styp -> term -> term *) -fun starred_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T)) +(* hol_context -> styp -> term -> term *) +fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (x as (s, T)) def = let val j = maxidx_of_term def + 1 @@ -1933,11 +1902,11 @@ $ list_comb (Const step_x, outer_bounds))) $ list_comb (Const base_x, outer_bounds) |> ap_curry tuple_arg_Ts tuple_T bool_T) - |> unfold_defs_in_term ext_ctxt + |> unfold_defs_in_term hol_ctxt end -(* extended_context -> bool -> styp -> term *) -fun unrolled_inductive_pred_const (ext_ctxt as {thy, star_linear_preds, +(* hol_context -> bool -> styp -> term *) +fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds, def_table, simp_table, ...}) gfp (x as (s, T)) = let @@ -1946,11 +1915,11 @@ val unrolled_const = Const x' $ zero_const iter_T val def = the (def_of_const thy def_table x) in - if is_equational_fun ext_ctxt x' then + if is_equational_fun hol_ctxt x' then unrolled_const (* already done *) else if not gfp andalso is_linear_inductive_pred_def def andalso star_linear_preds then - starred_linear_pred_const ext_ctxt x def + starred_linear_pred_const hol_ctxt x def else let val j = maxidx_of_term def + 1 @@ -1973,8 +1942,8 @@ in unrolled_const end end -(* extended_context -> styp -> term *) -fun raw_inductive_pred_axiom ({thy, def_table, ...} : extended_context) x = +(* hol_context -> styp -> term *) +fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x = let val def = the (def_of_const thy def_table x) val (outer, fp_app) = strip_abs def @@ -1992,24 +1961,29 @@ HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs) |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars) end -fun inductive_pred_axiom ext_ctxt (x as (s, T)) = +fun inductive_pred_axiom hol_ctxt (x as (s, T)) = if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then let val x' = (after_name_sep s, T) in - raw_inductive_pred_axiom ext_ctxt x' |> subst_atomic [(Const x', Const x)] + raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)] end else - raw_inductive_pred_axiom ext_ctxt x + raw_inductive_pred_axiom hol_ctxt x -(* extended_context -> styp -> term list *) -fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table, +(* hol_context -> styp -> term list *) +fun raw_equational_fun_axioms (hol_ctxt as {thy, fast_descrs, simp_table, psimp_table, ...}) (x as (s, _)) = case def_props_for_const thy fast_descrs (!simp_table) x of [] => (case def_props_for_const thy fast_descrs psimp_table x of - [] => [inductive_pred_axiom ext_ctxt x] + [] => [inductive_pred_axiom hol_ctxt x] | psimps => psimps) | simps => simps - val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms +(* hol_context -> styp -> bool *) +fun is_equational_fun_surely_complete hol_ctxt x = + case raw_equational_fun_axioms hol_ctxt x of + [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] => + strip_comb t1 |> snd |> forall is_Var + | _ => false (* term list -> term list *) fun merge_type_vars_in_terms ts = @@ -2028,1261 +2002,27 @@ | coalesce T = T in map (map_types (map_atyps coalesce)) ts end -(* extended_context -> typ -> typ list -> typ list *) -fun add_ground_types ext_ctxt T accum = +(* hol_context -> typ -> typ list -> typ list *) +fun add_ground_types hol_ctxt T accum = case T of - Type ("fun", Ts) => fold (add_ground_types ext_ctxt) Ts accum - | Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum - | Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum + Type ("fun", Ts) => fold (add_ground_types hol_ctxt) Ts accum + | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum + | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum | Type (_, Ts) => if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then accum else T :: accum - |> fold (add_ground_types ext_ctxt) - (case boxed_datatype_constrs ext_ctxt T of + |> fold (add_ground_types hol_ctxt) + (case boxed_datatype_constrs hol_ctxt T of [] => Ts | xs => map snd xs) | _ => insert (op =) T accum -(* extended_context -> typ -> typ list *) -fun ground_types_in_type ext_ctxt T = add_ground_types ext_ctxt T [] -(* extended_context -> term list -> typ list *) -fun ground_types_in_terms ext_ctxt ts = - fold (fold_types (add_ground_types ext_ctxt)) ts [] - -(* typ list -> int -> term -> bool *) -fun has_heavy_bounds_or_vars Ts level t = - let - (* typ list -> bool *) - fun aux [] = false - | aux [T] = is_fun_type T orelse is_pair_type T - | aux _ = true - in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end - -(* typ list -> int -> int -> int -> term -> term *) -fun fresh_value_var Ts k n j t = - Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t)) - -(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list - -> term * term list *) -fun pull_out_constr_comb thy Ts relax k level t args seen = - let val t_comb = list_comb (t, args) in - case t of - Const x => - if not relax andalso is_constr thy x andalso - not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso - has_heavy_bounds_or_vars Ts level t_comb andalso - not (loose_bvar (t_comb, level)) then - let - val (j, seen) = case find_index (curry (op =) t_comb) seen of - ~1 => (0, t_comb :: seen) - | j => (j, seen) - in (fresh_value_var Ts k (length seen) j t_comb, seen) end - else - (t_comb, seen) - | _ => (t_comb, seen) - end - -(* (term -> term) -> typ list -> int -> term list -> term list *) -fun equations_for_pulled_out_constrs mk_eq Ts k seen = - let val n = length seen in - map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t)) - (index_seq 0 n) seen - end - -(* theory -> bool -> term -> term *) -fun pull_out_universal_constrs thy def t = - let - val k = maxidx_of_term t + 1 - (* typ list -> bool -> term -> term list -> term list -> term * term list *) - fun do_term Ts def t args seen = - case t of - (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 => - do_eq_or_imp Ts true def t0 t1 t2 seen - | (t0 as @{const "==>"}) $ t1 $ t2 => - if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen - | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 => - do_eq_or_imp Ts true def t0 t1 t2 seen - | (t0 as @{const "op -->"}) $ t1 $ t2 => - do_eq_or_imp Ts false def t0 t1 t2 seen - | Abs (s, T, t') => - let val (t', seen) = do_term (T :: Ts) def t' [] seen in - (list_comb (Abs (s, T, t'), args), seen) - end - | t1 $ t2 => - let val (t2, seen) = do_term Ts def t2 [] seen in - do_term Ts def t1 (t2 :: args) seen - end - | _ => pull_out_constr_comb thy Ts def k 0 t args seen - (* typ list -> bool -> bool -> term -> term -> term -> term list - -> term * term list *) - and do_eq_or_imp Ts eq def t0 t1 t2 seen = - let - val (t2, seen) = if eq andalso def then (t2, seen) - else do_term Ts false t2 [] seen - val (t1, seen) = do_term Ts false t1 [] seen - in (t0 $ t1 $ t2, seen) end - val (concl, seen) = do_term [] def t [] [] - in - Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k - seen, concl) - end - -(* extended_context -> bool -> term -> term *) -fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t = - let - (* styp -> int *) - val num_occs_of_var = - fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1) - | _ => I) t (K 0) - (* bool -> term -> term *) - fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) = - aux_eq careful true t0 t1 t2 - | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) = - t0 $ aux false t1 $ aux careful t2 - | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) = - aux_eq careful true t0 t1 t2 - | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) = - t0 $ aux false t1 $ aux careful t2 - | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t') - | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2 - | aux _ t = t - (* bool -> bool -> term -> term -> term -> term *) - and aux_eq careful pass1 t0 t1 t2 = - ((if careful then - raise SAME () - else if axiom andalso is_Var t2 andalso - num_occs_of_var (dest_Var t2) = 1 then - @{const True} - else case strip_comb t2 of - (* The first case is not as general as it could be. *) - (Const (@{const_name PairBox}, _), - [Const (@{const_name fst}, _) $ Var z1, - Const (@{const_name snd}, _) $ Var z2]) => - if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True} - else raise SAME () - | (Const (x as (s, T)), args) => - let val arg_Ts = binder_types T in - if length arg_Ts = length args andalso - (is_constr thy x orelse s = @{const_name Pair} orelse - x = (@{const_name Suc}, nat_T --> nat_T)) andalso - (not careful orelse not (is_Var t1) orelse - String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then - discriminate_value ext_ctxt x t1 :: - map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args - |> foldr1 s_conj - else - raise SAME () - end - | _ => raise SAME ()) - |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop) - handle SAME () => if pass1 then aux_eq careful false t0 t2 t1 - else t0 $ aux false t2 $ aux false t1 - (* styp -> term -> int -> typ -> term -> term *) - and sel_eq x t n nth_T nth_t = - HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T - |> aux false - in aux axiom t end - -(* theory -> term -> term *) -fun simplify_constrs_and_sels thy t = - let - (* term -> int -> term *) - fun is_nth_sel_on t' n (Const (s, _) $ t) = - (t = t' andalso is_sel_like_and_no_discr s andalso - sel_no_from_name s = n) - | is_nth_sel_on _ _ _ = false - (* term -> term list -> term *) - fun do_term (Const (@{const_name Rep_Frac}, _) - $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 [] - | do_term (Const (@{const_name Abs_Frac}, _) - $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 [] - | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args) - | do_term (t as Const (x as (s, T))) (args as _ :: _) = - ((if is_constr_like thy x then - if length args = num_binder_types T then - case hd args of - Const (x' as (_, T')) $ t' => - if domain_type T' = body_type T andalso - forall (uncurry (is_nth_sel_on t')) - (index_seq 0 (length args) ~~ args) then - t' - else - raise SAME () - | _ => raise SAME () - else - raise SAME () - else if is_sel_like_and_no_discr s then - case strip_comb (hd args) of - (Const (x' as (s', T')), ts') => - if is_constr_like thy x' andalso - constr_name_for_sel_like s = s' andalso - not (exists is_pair_type (binder_types T')) then - list_comb (nth ts' (sel_no_from_name s), tl args) - else - raise SAME () - | _ => raise SAME () - else - raise SAME ()) - handle SAME () => betapplys (t, args)) - | do_term (Abs (s, T, t')) args = - betapplys (Abs (s, T, do_term t' []), args) - | do_term t args = betapplys (t, args) - in do_term t [] end - -(* term -> term *) -fun curry_assms (@{const "==>"} $ (@{const Trueprop} - $ (@{const "op &"} $ t1 $ t2)) $ t3) = - curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3)) - | curry_assms (@{const "==>"} $ t1 $ t2) = - @{const "==>"} $ curry_assms t1 $ curry_assms t2 - | curry_assms t = t - -(* term -> term *) -val destroy_universal_equalities = - let - (* term list -> (indexname * typ) list -> term -> term *) - fun aux prems zs t = - case t of - @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2 - | _ => Logic.list_implies (rev prems, t) - (* term list -> (indexname * typ) list -> term -> term -> term *) - and aux_implies prems zs t1 t2 = - case t1 of - Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2 - | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') => - aux_eq prems zs z t' t1 t2 - | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) => - aux_eq prems zs z t' t1 t2 - | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2 - (* term list -> (indexname * typ) list -> indexname * typ -> term -> term - -> term -> term *) - and aux_eq prems zs z t' t1 t2 = - if not (member (op =) zs z) andalso - not (exists_subterm (curry (op =) (Var z)) t') then - aux prems zs (subst_free [(Var z, t')] t2) - else - aux (t1 :: prems) (Term.add_vars t1 zs) t2 - in aux [] [] end - -(* theory -> term -> term *) -fun pull_out_existential_constrs thy t = - let - val k = maxidx_of_term t + 1 - (* typ list -> int -> term -> term list -> term list -> term * term list *) - fun aux Ts num_exists t args seen = - case t of - (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) => - let - val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] [] - val n = length seen' - (* unit -> term list *) - fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen' - in - (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen' - |> List.foldl s_conj t1 |> fold mk_exists (vars ()) - |> curry3 Abs s1 T1 |> curry (op $) t0, seen) - end - | t1 $ t2 => - let val (t2, seen) = aux Ts num_exists t2 [] seen in - aux Ts num_exists t1 (t2 :: args) seen - end - | Abs (s, T, t') => - let - val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen) - in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end - | _ => - if num_exists > 0 then - pull_out_constr_comb thy Ts false k num_exists t args seen - else - (list_comb (t, args), seen) - in aux [] 0 t [] [] |> fst end - -(* theory -> int -> term list -> term list -> (term * term list) option *) -fun find_bound_assign _ _ _ [] = NONE - | find_bound_assign thy j seen (t :: ts) = - let - (* bool -> term -> term -> (term * term list) option *) - fun aux pass1 t1 t2 = - (if loose_bvar1 (t2, j) then - if pass1 then aux false t2 t1 else raise SAME () - else case t1 of - Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME () - | Const (s, Type ("fun", [T1, T2])) $ Bound j' => - if j' = j andalso s = sel_prefix_for 0 ^ @{const_name FunBox} then - SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2], - ts @ seen) - else - raise SAME () - | _ => raise SAME ()) - handle SAME () => find_bound_assign thy j (t :: seen) ts - in - case t of - Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2 - | _ => find_bound_assign thy j (t :: seen) ts - end - -(* int -> term -> term -> term *) -fun subst_one_bound j arg t = - let - fun aux (Bound i, lev) = - if i < lev then raise SAME () - else if i = lev then incr_boundvars (lev - j) arg - else Bound (i - 1) - | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1)) - | aux (f $ t, lev) = - (aux (f, lev) $ (aux (t, lev) handle SAME () => t) - handle SAME () => f $ aux (t, lev)) - | aux _ = raise SAME () - in aux (t, j) handle SAME () => t end - -(* theory -> term -> term *) -fun destroy_existential_equalities thy = - let - (* string list -> typ list -> term list -> term *) - fun kill [] [] ts = foldr1 s_conj ts - | kill (s :: ss) (T :: Ts) ts = - (case find_bound_assign thy (length ss) [] ts of - SOME (_, []) => @{const True} - | SOME (arg_t, ts) => - kill ss Ts (map (subst_one_bound (length ss) - (incr_bv (~1, length ss + 1, arg_t))) ts) - | NONE => - Const (@{const_name Ex}, (T --> bool_T) --> bool_T) - $ Abs (s, T, kill ss Ts ts)) - | kill _ _ _ = raise UnequalLengths - (* string list -> typ list -> term -> term *) - fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) = - gather (ss @ [s1]) (Ts @ [T1]) t1 - | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1) - | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2 - | gather [] [] t = t - | gather ss Ts t = kill ss Ts (conjuncts (gather [] [] t)) - in gather [] [] end - -(* term -> term *) -fun distribute_quantifiers t = - case t of - (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) => - (case t1 of - (t10 as @{const "op &"}) $ t11 $ t12 => - t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) - $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) - | (t10 as @{const Not}) $ t11 => - t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0) - $ Abs (s, T1, t11)) - | t1 => - if not (loose_bvar1 (t1, 0)) then - distribute_quantifiers (incr_boundvars ~1 t1) - else - t0 $ Abs (s, T1, distribute_quantifiers t1)) - | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) => - (case distribute_quantifiers t1 of - (t10 as @{const "op |"}) $ t11 $ t12 => - t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) - $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) - | (t10 as @{const "op -->"}) $ t11 $ t12 => - t10 $ distribute_quantifiers (Const (@{const_name All}, T0) - $ Abs (s, T1, t11)) - $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) - | (t10 as @{const Not}) $ t11 => - t10 $ distribute_quantifiers (Const (@{const_name All}, T0) - $ Abs (s, T1, t11)) - | t1 => - if not (loose_bvar1 (t1, 0)) then - distribute_quantifiers (incr_boundvars ~1 t1) - else - t0 $ Abs (s, T1, distribute_quantifiers t1)) - | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2 - | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t') - | _ => t - -(* int -> int -> (int -> int) -> term -> term *) -fun renumber_bounds j n f t = - case t of - t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2 - | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t') - | Bound j' => - Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j') - | _ => t - -val quantifier_cluster_threshold = 7 - -(* theory -> term -> term *) -fun push_quantifiers_inward thy = - let - (* string -> string list -> typ list -> term -> term *) - fun aux quant_s ss Ts t = - (case t of - (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) => - if s0 = quant_s then - aux s0 (s1 :: ss) (T1 :: Ts) t1 - else if quant_s = "" andalso - (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then - aux s0 [s1] [T1] t1 - else - raise SAME () - | _ => raise SAME ()) - handle SAME () => - case t of - t1 $ t2 => - if quant_s = "" then - aux "" [] [] t1 $ aux "" [] [] t2 - else - let - val typical_card = 4 - (* ('a -> ''b list) -> 'a list -> ''b list *) - fun big_union proj ps = - fold (fold (insert (op =)) o proj) ps [] - val (ts, connective) = strip_any_connective t - val T_costs = - map (bounded_card_of_type 65536 typical_card []) Ts - val t_costs = map size_of_term ts - val num_Ts = length Ts - (* int -> int *) - val flip = curry (op -) (num_Ts - 1) - val t_boundss = map (map flip o loose_bnos) ts - (* (int list * int) list -> int list - -> (int list * int) list *) - fun merge costly_boundss [] = costly_boundss - | merge costly_boundss (j :: js) = - let - val (yeas, nays) = - List.partition (fn (bounds, _) => - member (op =) bounds j) - costly_boundss - val yeas_bounds = big_union fst yeas - val yeas_cost = Integer.sum (map snd yeas) - * nth T_costs j - in merge ((yeas_bounds, yeas_cost) :: nays) js end - (* (int list * int) list -> int list -> int *) - val cost = Integer.sum o map snd oo merge - (* Inspired by Claessen & Sörensson's polynomial binary - splitting heuristic (p. 5 of their MODEL 2003 paper). *) - (* (int list * int) list -> int list -> int list *) - fun heuristically_best_permutation _ [] = [] - | heuristically_best_permutation costly_boundss js = - let - val (costly_boundss, (j, js)) = - js |> map (`(merge costly_boundss o single)) - |> sort (int_ord - o pairself (Integer.sum o map snd o fst)) - |> split_list |>> hd ||> pairf hd tl - in - j :: heuristically_best_permutation costly_boundss js - end - val js = - if length Ts <= quantifier_cluster_threshold then - all_permutations (index_seq 0 num_Ts) - |> map (`(cost (t_boundss ~~ t_costs))) - |> sort (int_ord o pairself fst) |> hd |> snd - else - heuristically_best_permutation (t_boundss ~~ t_costs) - (index_seq 0 num_Ts) - val back_js = map (fn j => find_index (curry (op =) j) js) - (index_seq 0 num_Ts) - val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip)) - ts - (* (term * int list) list -> term *) - fun mk_connection [] = - raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\ - \mk_connection", "") - | mk_connection ts_cum_bounds = - ts_cum_bounds |> map fst - |> foldr1 (fn (t1, t2) => connective $ t1 $ t2) - (* (term * int list) list -> int list -> term *) - fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection - | build ts_cum_bounds (j :: js) = - let - val (yeas, nays) = - List.partition (fn (_, bounds) => - member (op =) bounds j) - ts_cum_bounds - ||> map (apfst (incr_boundvars ~1)) - in - if null yeas then - build nays js - else - let val T = nth Ts (flip j) in - build ((Const (quant_s, (T --> bool_T) --> bool_T) - $ Abs (nth ss (flip j), T, - mk_connection yeas), - big_union snd yeas) :: nays) js - end - end - in build (ts ~~ t_boundss) js end - | Abs (s, T, t') => Abs (s, T, aux "" [] [] t') - | _ => t - in aux "" [] [] end - -(* polarity -> string -> bool *) -fun is_positive_existential polar quant_s = - (polar = Pos andalso quant_s = @{const_name Ex}) orelse - (polar = Neg andalso quant_s <> @{const_name Ex}) - -(* extended_context -> int -> term -> term *) -fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...}) - skolem_depth = - let - (* int list -> int list *) - val incrs = map (Integer.add 1) - (* string list -> typ list -> int list -> int -> polarity -> term -> term *) - fun aux ss Ts js depth polar t = - let - (* string -> typ -> string -> typ -> term -> term *) - fun do_quantifier quant_s quant_T abs_s abs_T t = - if not (loose_bvar1 (t, 0)) then - aux ss Ts js depth polar (incr_boundvars ~1 t) - else if depth <= skolem_depth andalso - is_positive_existential polar quant_s then - let - val j = length (!skolems) + 1 - val sko_s = skolem_prefix_for (length js) j ^ abs_s - val _ = Unsynchronized.change skolems (cons (sko_s, ss)) - val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T), - map Bound (rev js)) - val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t) - in - if null js then betapply (abs_t, sko_t) - else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t - end - else - Const (quant_s, quant_T) - $ Abs (abs_s, abs_T, - if is_higher_order_type abs_T then - t - else - aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js) - (depth + 1) polar t) - in - case t of - Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => - do_quantifier s0 T0 s1 T1 t1 - | @{const "==>"} $ t1 $ t2 => - @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1 - $ aux ss Ts js depth polar t2 - | @{const Pure.conjunction} $ t1 $ t2 => - @{const Pure.conjunction} $ aux ss Ts js depth polar t1 - $ aux ss Ts js depth polar t2 - | @{const Trueprop} $ t1 => - @{const Trueprop} $ aux ss Ts js depth polar t1 - | @{const Not} $ t1 => - @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1 - | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => - do_quantifier s0 T0 s1 T1 t1 - | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => - do_quantifier s0 T0 s1 T1 t1 - | @{const "op &"} $ t1 $ t2 => - @{const "op &"} $ aux ss Ts js depth polar t1 - $ aux ss Ts js depth polar t2 - | @{const "op |"} $ t1 $ t2 => - @{const "op |"} $ aux ss Ts js depth polar t1 - $ aux ss Ts js depth polar t2 - | @{const "op -->"} $ t1 $ t2 => - @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1 - $ aux ss Ts js depth polar t2 - | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 => - t0 $ t1 $ aux ss Ts js depth polar t2 - | Const (x as (s, T)) => - if is_inductive_pred ext_ctxt x andalso - not (is_well_founded_inductive_pred ext_ctxt x) then - let - val gfp = (fixpoint_kind_of_const thy def_table x = Gfp) - val (pref, connective, set_oper) = - if gfp then - (lbfp_prefix, - @{const "op |"}, - @{const_name upper_semilattice_fun_inst.sup_fun}) - else - (ubfp_prefix, - @{const "op &"}, - @{const_name lower_semilattice_fun_inst.inf_fun}) - (* unit -> term *) - fun pos () = unrolled_inductive_pred_const ext_ctxt gfp x - |> aux ss Ts js depth polar - fun neg () = Const (pref ^ s, T) - in - (case polar |> gfp ? flip_polarity of - Pos => pos () - | Neg => neg () - | Neut => - if is_fun_type T then - let - val ((trunk_arg_Ts, rump_arg_T), body_T) = - T |> strip_type |>> split_last - val set_T = rump_arg_T --> body_T - (* (unit -> term) -> term *) - fun app f = - list_comb (f (), - map Bound (length trunk_arg_Ts - 1 downto 0)) - in - List.foldr absdummy - (Const (set_oper, set_T --> set_T --> set_T) - $ app pos $ app neg) trunk_arg_Ts - end - else - connective $ pos () $ neg ()) - end - else - Const x - | t1 $ t2 => - betapply (aux ss Ts [] (skolem_depth + 1) polar t1, - aux ss Ts [] depth Neut t2) - | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1) - | _ => t - end - in aux [] [] [] 0 Pos end - -(* extended_context -> styp -> (int * term option) list *) -fun static_args_in_term ({ersatz_table, ...} : extended_context) x t = - let - (* term -> term list -> term list -> term list list *) - fun fun_calls (Abs (_, _, t)) _ = fun_calls t [] - | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args) - | fun_calls t args = - (case t of - Const (x' as (s', T')) => - x = x' orelse (case AList.lookup (op =) ersatz_table s' of - SOME s'' => x = (s'', T') - | NONE => false) - | _ => false) ? cons args - (* term list list -> term list list -> term list -> term list list *) - fun call_sets [] [] vs = [vs] - | call_sets [] uss vs = vs :: call_sets uss [] [] - | call_sets ([] :: _) _ _ = [] - | call_sets ((t :: ts) :: tss) uss vs = - OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss) - val sets = call_sets (fun_calls t [] []) [] [] - val indexed_sets = sets ~~ (index_seq 0 (length sets)) - in - fold_rev (fn (set, j) => - case set of - [Var _] => AList.lookup (op =) indexed_sets set = SOME j - ? cons (j, NONE) - | [t as Const _] => cons (j, SOME t) - | [t as Free _] => cons (j, SOME t) - | _ => I) indexed_sets [] - end -(* extended_context -> styp -> term list -> (int * term option) list *) -fun static_args_in_terms ext_ctxt x = - map (static_args_in_term ext_ctxt x) - #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord))) - -(* term -> term list *) -fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2 - | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1 - | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) = - snd (strip_comb t1) - | params_in_equation _ = [] - -(* styp -> styp -> int list -> term list -> term list -> term -> term *) -fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t = - let - val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0 - + 1 - val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t - val fixed_params = filter_indices fixed_js (params_in_equation t) - (* term list -> term -> term *) - fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args) - | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1 - | aux args t = - if t = Const x then - list_comb (Const x', extra_args @ filter_out_indices fixed_js args) - else - let val j = find_index (curry (op =) t) fixed_params in - list_comb (if j >= 0 then nth fixed_args j else t, args) - end - in aux [] t end - -(* typ list -> term -> bool *) -fun is_eligible_arg Ts t = - let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in - null bad_Ts orelse - (is_higher_order_type (fastype_of1 (Ts, t)) andalso - forall (not o is_higher_order_type) bad_Ts) - end - -(* (int * term option) list -> (int * term) list -> int list *) -fun overlapping_indices [] _ = [] - | overlapping_indices _ [] = [] - | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') = - if j1 < j2 then overlapping_indices ps1' ps2 - else if j1 > j2 then overlapping_indices ps1 ps2' - else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1 - -val special_depth = 20 - -(* extended_context -> int -> term -> term *) -fun specialize_consts_in_term (ext_ctxt as {thy, specialize, simp_table, - special_funs, ...}) depth t = - if not specialize orelse depth > special_depth then - t - else - let - val blacklist = if depth = 0 then [] - else case term_under_def t of Const x => [x] | _ => [] - (* term list -> typ list -> term -> term *) - fun aux args Ts (Const (x as (s, T))) = - ((if not (member (op =) blacklist x) andalso not (null args) andalso - not (String.isPrefix special_prefix s) andalso - is_equational_fun ext_ctxt x then - let - val eligible_args = filter (is_eligible_arg Ts o snd) - (index_seq 0 (length args) ~~ args) - val _ = not (null eligible_args) orelse raise SAME () - val old_axs = equational_fun_axioms ext_ctxt x - |> map (destroy_existential_equalities thy) - val static_params = static_args_in_terms ext_ctxt x old_axs - val fixed_js = overlapping_indices static_params eligible_args - val _ = not (null fixed_js) orelse raise SAME () - val fixed_args = filter_indices fixed_js args - val vars = fold Term.add_vars fixed_args [] - |> sort (TermOrd.fast_indexname_ord o pairself fst) - val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js)) - fixed_args [] - |> sort int_ord - val live_args = filter_out_indices fixed_js args - val extra_args = map Var vars @ map Bound bound_js @ live_args - val extra_Ts = map snd vars @ filter_indices bound_js Ts - val k = maxidx_of_term t + 1 - (* int -> term *) - fun var_for_bound_no j = - Var ((bound_var_prefix ^ - nat_subscript (find_index (curry (op =) j) bound_js - + 1), k), - nth Ts j) - val fixed_args_in_axiom = - map (curry subst_bounds - (map var_for_bound_no (index_seq 0 (length Ts)))) - fixed_args - in - case AList.lookup (op =) (!special_funs) - (x, fixed_js, fixed_args_in_axiom) of - SOME x' => list_comb (Const x', extra_args) - | NONE => - let - val extra_args_in_axiom = - map Var vars @ map var_for_bound_no bound_js - val x' as (s', _) = - (special_prefix_for (length (!special_funs) + 1) ^ s, - extra_Ts @ filter_out_indices fixed_js (binder_types T) - ---> body_type T) - val new_axs = - map (specialize_fun_axiom x x' fixed_js - fixed_args_in_axiom extra_args_in_axiom) old_axs - val _ = - Unsynchronized.change special_funs - (cons ((x, fixed_js, fixed_args_in_axiom), x')) - val _ = add_simps simp_table s' new_axs - in list_comb (Const x', extra_args) end - end - else - raise SAME ()) - handle SAME () => list_comb (Const x, args)) - | aux args Ts (Abs (s, T, t)) = - list_comb (Abs (s, T, aux [] (T :: Ts) t), args) - | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1 - | aux args _ t = list_comb (t, args) - in aux [] [] t end - -(* theory -> term -> int Termtab.tab -> int Termtab.tab *) -fun add_to_uncurry_table thy t = - let - (* term -> term list -> int Termtab.tab -> int Termtab.tab *) - fun aux (t1 $ t2) args table = - let val table = aux t2 [] table in aux t1 (t2 :: args) table end - | aux (Abs (_, _, t')) _ table = aux t' [] table - | aux (t as Const (x as (s, _))) args table = - if is_built_in_const true x orelse is_constr_like thy x orelse - is_sel s orelse s = @{const_name Sigma} then - table - else - Termtab.map_default (t, 65536) (curry Int.min (length args)) table - | aux _ _ table = table - in aux t [] end - -(* int Termtab.tab term -> term *) -fun uncurry_term table t = - let - (* term -> term list -> term *) - fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args) - | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args) - | aux (t as Const (s, T)) args = - (case Termtab.lookup table t of - SOME n => - if n >= 2 then - let - val (arg_Ts, rest_T) = strip_n_binders n T - val j = - if hd arg_Ts = @{typ bisim_iterator} orelse - is_fp_iterator_type (hd arg_Ts) then - 1 - else case find_index (not_equal bool_T) arg_Ts of - ~1 => n - | j => j - val ((before_args, tuple_args), after_args) = - args |> chop n |>> chop j - val ((before_arg_Ts, tuple_arg_Ts), rest_T) = - T |> strip_n_binders n |>> chop j - val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts - in - if n - j < 2 then - betapplys (t, args) - else - betapplys (Const (uncurry_prefix_for (n - j) j ^ s, - before_arg_Ts ---> tuple_T --> rest_T), - before_args @ [mk_flat_tuple tuple_T tuple_args] @ - after_args) - end - else - betapplys (t, args) - | NONE => betapplys (t, args)) - | aux t args = betapplys (t, args) - in aux t [] end - -(* (term -> term) -> int -> term -> term *) -fun coerce_bound_no f j t = - case t of - t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2 - | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t') - | Bound j' => if j' = j then f t else t - | _ => t - -(* extended_context -> bool -> term -> term *) -fun box_fun_and_pair_in_term (ext_ctxt as {thy, fast_descrs, ...}) def orig_t = - let - (* typ -> typ *) - fun box_relational_operator_type (Type ("fun", Ts)) = - Type ("fun", map box_relational_operator_type Ts) - | box_relational_operator_type (Type ("*", Ts)) = - Type ("*", map (box_type ext_ctxt InPair) Ts) - | box_relational_operator_type T = T - (* typ -> typ -> term -> term *) - fun coerce_bound_0_in_term new_T old_T = - old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0 - (* typ list -> typ -> term -> term *) - and coerce_term Ts new_T old_T t = - if old_T = new_T then - t - else - case (new_T, old_T) of - (Type (new_s, new_Ts as [new_T1, new_T2]), - Type ("fun", [old_T1, old_T2])) => - (case eta_expand Ts t 1 of - Abs (s, _, t') => - Abs (s, new_T1, - t' |> coerce_bound_0_in_term new_T1 old_T1 - |> coerce_term (new_T1 :: Ts) new_T2 old_T2) - |> Envir.eta_contract - |> new_s <> "fun" - ? construct_value thy (@{const_name FunBox}, - Type ("fun", new_Ts) --> new_T) o single - | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\ - \coerce_term", [t'])) - | (Type (new_s, new_Ts as [new_T1, new_T2]), - Type (old_s, old_Ts as [old_T1, old_T2])) => - if old_s = @{type_name fun_box} orelse - old_s = @{type_name pair_box} orelse old_s = "*" then - case constr_expand ext_ctxt old_T t of - Const (@{const_name FunBox}, _) $ t1 => - if new_s = "fun" then - coerce_term Ts new_T (Type ("fun", old_Ts)) t1 - else - construct_value thy - (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T) - [coerce_term Ts (Type ("fun", new_Ts)) - (Type ("fun", old_Ts)) t1] - | Const _ $ t1 $ t2 => - construct_value thy - (if new_s = "*" then @{const_name Pair} - else @{const_name PairBox}, new_Ts ---> new_T) - [coerce_term Ts new_T1 old_T1 t1, - coerce_term Ts new_T2 old_T2 t2] - | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\ - \coerce_term", [t']) - else - raise TYPE ("coerce_term", [new_T, old_T], [t]) - | _ => raise TYPE ("coerce_term", [new_T, old_T], [t]) - (* indexname * typ -> typ * term -> typ option list -> typ option list *) - fun add_boxed_types_for_var (z as (_, T)) (T', t') = - case t' of - Var z' => z' = z ? insert (op =) T' - | Const (@{const_name Pair}, _) $ t1 $ t2 => - (case T' of - Type (_, [T1, T2]) => - fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)] - | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\ - \add_boxed_types_for_var", [T'], [])) - | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T - (* typ list -> typ list -> term -> indexname * typ -> typ *) - fun box_var_in_def new_Ts old_Ts t (z as (_, T)) = - case t of - @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z - | Const (s0, _) $ t1 $ _ => - if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then - let - val (t', args) = strip_comb t1 - val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t') - in - case fold (add_boxed_types_for_var z) - (fst (strip_n_binders (length args) T') ~~ args) [] of - [T''] => T'' - | _ => T - end - else - T - | _ => T - (* typ list -> typ list -> polarity -> string -> typ -> string -> typ - -> term -> term *) - and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t = - let - val abs_T' = - if polar = Neut orelse is_positive_existential polar quant_s then - box_type ext_ctxt InFunLHS abs_T - else - abs_T - val body_T = body_type quant_T - in - Const (quant_s, (abs_T' --> body_T) --> body_T) - $ Abs (abs_s, abs_T', - t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar) - end - (* typ list -> typ list -> string -> typ -> term -> term -> term *) - and do_equals new_Ts old_Ts s0 T0 t1 t2 = - let - val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2) - val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2) - val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last - in - list_comb (Const (s0, T --> T --> body_type T0), - map2 (coerce_term new_Ts T) [T1, T2] [t1, t2]) - end - (* string -> typ -> term *) - and do_description_operator s T = - let val T1 = box_type ext_ctxt InFunLHS (range_type T) in - Const (s, (T1 --> bool_T) --> T1) - end - (* typ list -> typ list -> polarity -> term -> term *) - and do_term new_Ts old_Ts polar t = - case t of - Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => - do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 - | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 => - do_equals new_Ts old_Ts s0 T0 t1 t2 - | @{const "==>"} $ t1 $ t2 => - @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1 - $ do_term new_Ts old_Ts polar t2 - | @{const Pure.conjunction} $ t1 $ t2 => - @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1 - $ do_term new_Ts old_Ts polar t2 - | @{const Trueprop} $ t1 => - @{const Trueprop} $ do_term new_Ts old_Ts polar t1 - | @{const Not} $ t1 => - @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1 - | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => - do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 - | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => - do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 - | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 => - do_equals new_Ts old_Ts s0 T0 t1 t2 - | @{const "op &"} $ t1 $ t2 => - @{const "op &"} $ do_term new_Ts old_Ts polar t1 - $ do_term new_Ts old_Ts polar t2 - | @{const "op |"} $ t1 $ t2 => - @{const "op |"} $ do_term new_Ts old_Ts polar t1 - $ do_term new_Ts old_Ts polar t2 - | @{const "op -->"} $ t1 $ t2 => - @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1 - $ do_term new_Ts old_Ts polar t2 - | Const (s as @{const_name The}, T) => do_description_operator s T - | Const (s as @{const_name Eps}, T) => do_description_operator s T - | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) => - let val T' = box_type ext_ctxt InSel T2 in - Const (@{const_name quot_normal}, T' --> T') - end - | Const (s as @{const_name Tha}, T) => do_description_operator s T - | Const (x as (s, T)) => - Const (s, if s = @{const_name converse} orelse - s = @{const_name trancl} then - box_relational_operator_type T - else if is_built_in_const fast_descrs x orelse - s = @{const_name Sigma} then - T - else if is_constr_like thy x then - box_type ext_ctxt InConstr T - else if is_sel s - orelse is_rep_fun thy x then - box_type ext_ctxt InSel T - else - box_type ext_ctxt InExpr T) - | t1 $ Abs (s, T, t2') => - let - val t1 = do_term new_Ts old_Ts Neut t1 - val T1 = fastype_of1 (new_Ts, t1) - val (s1, Ts1) = dest_Type T1 - val T' = hd (snd (dest_Type (hd Ts1))) - val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2') - val T2 = fastype_of1 (new_Ts, t2) - val t2 = coerce_term new_Ts (hd Ts1) T2 t2 - in - betapply (if s1 = "fun" then - t1 - else - select_nth_constr_arg thy - (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0 - (Type ("fun", Ts1)), t2) - end - | t1 $ t2 => - let - val t1 = do_term new_Ts old_Ts Neut t1 - val T1 = fastype_of1 (new_Ts, t1) - val (s1, Ts1) = dest_Type T1 - val t2 = do_term new_Ts old_Ts Neut t2 - val T2 = fastype_of1 (new_Ts, t2) - val t2 = coerce_term new_Ts (hd Ts1) T2 t2 - in - betapply (if s1 = "fun" then - t1 - else - select_nth_constr_arg thy - (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0 - (Type ("fun", Ts1)), t2) - end - | Free (s, T) => Free (s, box_type ext_ctxt InExpr T) - | Var (z as (x, T)) => - Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z - else box_type ext_ctxt InExpr T) - | Bound _ => t - | Abs (s, T, t') => - Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t') - in do_term [] [] Pos orig_t end - -(* int -> term -> term *) -fun eval_axiom_for_term j t = - Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t) - -(* extended_context -> styp -> bool *) -fun is_equational_fun_surely_complete ext_ctxt x = - case raw_equational_fun_axioms ext_ctxt x of - [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] => - strip_comb t1 |> snd |> forall is_Var - | _ => false - -type special = int list * term list * styp - -(* styp -> special -> special -> term *) -fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) = - let - val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2) - val Ts = binder_types T - val max_j = fold (fold Integer.max) [js1, js2] ~1 - val (eqs, (args1, args2)) = - fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j) - (js1 ~~ ts1, js2 ~~ ts2) of - (SOME t1, SOME t2) => apfst (cons (t1, t2)) - | (SOME t1, NONE) => apsnd (apsnd (cons t1)) - | (NONE, SOME t2) => apsnd (apfst (cons t2)) - | (NONE, NONE) => - let val v = Var ((cong_var_prefix ^ nat_subscript j, 0), - nth Ts j) in - apsnd (pairself (cons v)) - end) (max_j downto 0) ([], ([], [])) - in - Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =) - |> map Logic.mk_equals, - Logic.mk_equals (list_comb (Const x1, bounds1 @ args1), - list_comb (Const x2, bounds2 @ args2))) - |> Refute.close_form (* TODO: needed? *) - end - -(* extended_context -> styp list -> term list *) -fun special_congruence_axioms (ext_ctxt as {special_funs, ...}) xs = - let - val groups = - !special_funs - |> map (fn ((x, js, ts), x') => (x, (js, ts, x'))) - |> AList.group (op =) - |> filter_out (is_equational_fun_surely_complete ext_ctxt o fst) - |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x))) - (* special -> int *) - fun generality (js, _, _) = ~(length js) - (* special -> special -> bool *) - fun is_more_specific (j1, t1, x1) (j2, t2, x2) = - x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord) - (j2 ~~ t2, j1 ~~ t1) - (* styp -> special list -> special list -> special list -> term list - -> term list *) - fun do_pass_1 _ [] [_] [_] = I - | do_pass_1 x skipped _ [] = do_pass_2 x skipped - | do_pass_1 x skipped all (z :: zs) = - case filter (is_more_specific z) all - |> sort (int_ord o pairself generality) of - [] => do_pass_1 x (z :: skipped) all zs - | (z' :: _) => cons (special_congruence_axiom x z z') - #> do_pass_1 x skipped all zs - (* styp -> special list -> term list -> term list *) - and do_pass_2 _ [] = I - | do_pass_2 x (z :: zs) = - fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs - in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end - -(* term -> bool *) -val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals) - -(* 'a Symtab.table -> 'a list *) -fun all_table_entries table = Symtab.fold (append o snd) table [] -(* const_table -> string -> const_table *) -fun extra_table table s = Symtab.make [(s, all_table_entries table)] - -(* extended_context -> term -> (term list * term list) * (bool * bool) *) -fun axioms_for_term - (ext_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals, - def_table, nondef_table, user_nondefs, ...}) t = - let - type accumulator = styp list * (term list * term list) - (* (term list * term list -> term list) - -> ((term list -> term list) -> term list * term list - -> term list * term list) - -> int -> term -> accumulator -> accumulator *) - fun add_axiom get app depth t (accum as (xs, axs)) = - let - val t = t |> unfold_defs_in_term ext_ctxt - |> skolemize_term_and_more ext_ctxt ~1 - in - if is_trivial_equation t then - accum - else - let val t' = t |> specialize_consts_in_term ext_ctxt depth in - if exists (member (op aconv) (get axs)) [t, t'] then accum - else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs) - end - end - (* int -> term -> accumulator -> accumulator *) - and add_def_axiom depth = add_axiom fst apfst depth - and add_nondef_axiom depth = add_axiom snd apsnd depth - and add_maybe_def_axiom depth t = - (if head_of t <> @{const "==>"} then add_def_axiom - else add_nondef_axiom) depth t - and add_eq_axiom depth t = - (if is_constr_pattern_formula thy t then add_def_axiom - else add_nondef_axiom) depth t - (* int -> term -> accumulator -> accumulator *) - and add_axioms_for_term depth t (accum as (xs, axs)) = - case t of - t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2] - | Const (x as (s, T)) => - (if member (op =) xs x orelse is_built_in_const fast_descrs x then - accum - else - let val accum as (xs, _) = (x :: xs, axs) in - if depth > axioms_max_depth then - raise TOO_LARGE ("Nitpick_HOL.axioms_for_term.\ - \add_axioms_for_term", - "too many nested axioms (" ^ - string_of_int depth ^ ")") - else if Refute.is_const_of_class thy x then - let - val class = Logic.class_of_const s - val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), - class) - val ax1 = try (Refute.specialize_type thy x) of_class - val ax2 = Option.map (Refute.specialize_type thy x o snd) - (Refute.get_classdef thy class) - in - fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2]) - accum - end - else if is_constr thy x then - accum - else if is_equational_fun ext_ctxt x then - fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x) - accum - else if is_abs_fun thy x then - if is_quot_type thy (range_type T) then - raise NOT_SUPPORTED "\"Abs_\" function of quotient type" - else - accum |> fold (add_nondef_axiom depth) - (nondef_props_for_const thy false nondef_table x) - |> is_funky_typedef thy (range_type T) - ? fold (add_maybe_def_axiom depth) - (nondef_props_for_const thy true - (extra_table def_table s) x) - else if is_rep_fun thy x then - if is_quot_type thy (domain_type T) then - raise NOT_SUPPORTED "\"Rep_\" function of quotient type" - else - accum |> fold (add_nondef_axiom depth) - (nondef_props_for_const thy false nondef_table x) - |> is_funky_typedef thy (range_type T) - ? fold (add_maybe_def_axiom depth) - (nondef_props_for_const thy true - (extra_table def_table s) x) - |> add_axioms_for_term depth - (Const (mate_of_rep_fun thy x)) - |> fold (add_def_axiom depth) - (inverse_axioms_for_rep_fun thy x) - else - accum |> user_axioms <> SOME false - ? fold (add_nondef_axiom depth) - (nondef_props_for_const thy false nondef_table x) - end) - |> add_axioms_for_type depth T - | Free (_, T) => add_axioms_for_type depth T accum - | Var (_, T) => add_axioms_for_type depth T accum - | Bound _ => accum - | Abs (_, T, t) => accum |> add_axioms_for_term depth t - |> add_axioms_for_type depth T - (* int -> typ -> accumulator -> accumulator *) - and add_axioms_for_type depth T = - case T of - Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts - | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts - | @{typ prop} => I - | @{typ bool} => I - | @{typ unit} => I - | TFree (_, S) => add_axioms_for_sort depth T S - | TVar (_, S) => add_axioms_for_sort depth T S - | Type (z as (s, Ts)) => - fold (add_axioms_for_type depth) Ts - #> (if is_pure_typedef thy T then - fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z) - else if is_quot_type thy T then - fold (add_def_axiom depth) (optimized_quot_type_axioms thy z) - else if max_bisim_depth >= 0 andalso is_codatatype thy T then - fold (add_maybe_def_axiom depth) - (codatatype_bisim_axioms ext_ctxt T) - else - I) - (* int -> typ -> sort -> accumulator -> accumulator *) - and add_axioms_for_sort depth T S = - let - val supers = Sign.complete_sort thy S - val class_axioms = - maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms - handle ERROR _ => [])) supers - val monomorphic_class_axioms = - map (fn t => case Term.add_tvars t [] of - [] => t - | [(x, S)] => - Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t - | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\ - \add_axioms_for_sort", [t])) - class_axioms - in fold (add_nondef_axiom depth) monomorphic_class_axioms end - val (mono_user_nondefs, poly_user_nondefs) = - List.partition (null o Term.hidden_polymorphism) user_nondefs - val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals)) - evals - val (xs, (defs, nondefs)) = - ([], ([], [])) |> add_axioms_for_term 1 t - |> fold_rev (add_def_axiom 1) eval_axioms - |> user_axioms = SOME true - ? fold (add_nondef_axiom 1) mono_user_nondefs - val defs = defs @ special_congruence_axioms ext_ctxt xs - in - ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs, - null poly_user_nondefs)) - end +(* hol_context -> typ -> typ list *) +fun ground_types_in_type hol_ctxt T = add_ground_types hol_ctxt T [] +(* hol_context -> term list -> typ list *) +fun ground_types_in_terms hol_ctxt ts = + fold (fold_types (add_ground_types hol_ctxt)) ts [] (* theory -> const_table -> styp -> int list *) fun const_format thy def_table (x as (s, T)) = @@ -3356,10 +2096,10 @@ |> map (rev o filter_out (member (op =) js)) |> filter_out null |> map length |> rev -(* extended_context -> string * string -> (term option * int list) list +(* hol_context -> string * string -> (term option * int list) list -> styp -> term * typ *) fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...} - : extended_context) (base_name, step_name) formats = + : hol_context) (base_name, step_name) formats = let val default_format = the (AList.lookup (op =) formats NONE) (* styp -> term * typ *) @@ -3460,7 +2200,7 @@ (t, format_term_type thy def_table formats t) end) |>> map_types unbit_and_unbox_type - |>> shorten_names_in_term |>> shorten_abs_vars + |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name in do_const end (* styp -> string *) @@ -3474,84 +2214,4 @@ else "=" -val binary_int_threshold = 4 - -(* term -> bool *) -fun may_use_binary_ints (t1 $ t2) = - may_use_binary_ints t1 andalso may_use_binary_ints t2 - | may_use_binary_ints (t as Const (s, _)) = - t <> @{const Suc} andalso - not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, - @{const_name nat_gcd}, @{const_name nat_lcm}, - @{const_name Frac}, @{const_name norm_frac}] s) - | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t' - | may_use_binary_ints _ = true -fun should_use_binary_ints (t1 $ t2) = - should_use_binary_ints t1 orelse should_use_binary_ints t2 - | should_use_binary_ints (Const (s, _)) = - member (op =) [@{const_name times_nat_inst.times_nat}, - @{const_name div_nat_inst.div_nat}, - @{const_name times_int_inst.times_int}, - @{const_name div_int_inst.div_int}] s orelse - (String.isPrefix numeral_prefix s andalso - let val n = the (Int.fromString (unprefix numeral_prefix s)) in - n <= ~ binary_int_threshold orelse n >= binary_int_threshold - end) - | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t' - | should_use_binary_ints _ = false - -(* typ -> typ *) -fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"} - | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"} - | binarize_nat_and_int_in_type (Type (s, Ts)) = - Type (s, map binarize_nat_and_int_in_type Ts) - | binarize_nat_and_int_in_type T = T -(* term -> term *) -val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type - -(* extended_context -> term - -> ((term list * term list) * (bool * bool)) * term *) -fun preprocess_term (ext_ctxt as {thy, binary_ints, destroy_constrs, boxes, - skolemize, uncurry, ...}) t = - let - val skolem_depth = if skolemize then 4 else ~1 - val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)), - core_t) = t |> unfold_defs_in_term ext_ctxt - |> Refute.close_form - |> skolemize_term_and_more ext_ctxt skolem_depth - |> specialize_consts_in_term ext_ctxt 0 - |> `(axioms_for_term ext_ctxt) - val binarize = - case binary_ints of - SOME false => false - | _ => - forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso - (binary_ints = SOME true orelse - exists should_use_binary_ints (core_t :: def_ts @ nondef_ts)) - val box = exists (not_equal (SOME false) o snd) boxes - val table = - Termtab.empty |> uncurry - ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts) - (* bool -> bool -> term -> term *) - fun do_rest def core = - binarize ? binarize_nat_and_int_in_term - #> uncurry ? uncurry_term table - #> box ? box_fun_and_pair_in_term ext_ctxt def - #> destroy_constrs ? (pull_out_universal_constrs thy def - #> pull_out_existential_constrs thy - #> destroy_pulled_out_constrs ext_ctxt def) - #> curry_assms - #> destroy_universal_equalities - #> destroy_existential_equalities thy - #> simplify_constrs_and_sels thy - #> distribute_quantifiers - #> push_quantifiers_inward thy - #> not core ? Refute.close_form - #> shorten_abs_vars - in - (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts), - (got_all_mono_user_axioms, no_poly_user_axioms)), - do_rest false true core_t) - end - end; diff -r 5e492a862b34 -r 96136eb6218f src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 04 13:36:52 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 04 16:03:15 2010 +0100 @@ -7,7 +7,7 @@ signature NITPICK_KODKOD = sig - type extended_context = Nitpick_HOL.extended_context + type hol_context = Nitpick_HOL.hol_context type dtype_spec = Nitpick_Scope.dtype_spec type kodkod_constrs = Nitpick_Peephole.kodkod_constrs type nut = Nitpick_Nut.nut @@ -33,7 +33,7 @@ val merge_bounds : Kodkod.bound list -> Kodkod.bound list val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula val declarative_axioms_for_datatypes : - extended_context -> int -> int Typtab.table -> kodkod_constrs + hol_context -> int -> int Typtab.table -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list val kodkod_formula_from_nut : int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula @@ -732,12 +732,12 @@ (* nut NameTable.table -> styp -> KK.rel_expr *) fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> styp -> int -> nfa_transition list *) -fun nfa_transitions_for_sel ext_ctxt ({kk_project, ...} : kodkod_constrs) +fun nfa_transitions_for_sel hol_ctxt ({kk_project, ...} : kodkod_constrs) rel_table (dtypes : dtype_spec list) constr_x n = let - val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt constr_x n + val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt constr_x n val (r, R, arity) = const_triple rel_table x val type_schema = type_schema_of_rep T R in @@ -746,17 +746,17 @@ else SOME (kk_project r (map KK.Num [0, j]), T)) (index_seq 1 (arity - 1) ~~ tl type_schema) end -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> styp -> nfa_transition list *) -fun nfa_transitions_for_constr ext_ctxt kk rel_table dtypes (x as (_, T)) = - maps (nfa_transitions_for_sel ext_ctxt kk rel_table dtypes x) +fun nfa_transitions_for_constr hol_ctxt kk rel_table dtypes (x as (_, T)) = + maps (nfa_transitions_for_sel hol_ctxt kk rel_table dtypes x) (index_seq 0 (num_sels_for_constr_type T)) -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> dtype_spec -> nfa_entry option *) fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE - | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} = - SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes + | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} = + SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes o #const) constrs) val empty_rel = KK.Product (KK.None, KK.None) @@ -812,23 +812,23 @@ fun acyclicity_axiom_for_datatype dtypes kk nfa start = #kk_no kk (#kk_intersect kk (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden) -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> KK.formula list *) -fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes = - map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes +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) -(* extended_context -> int -> kodkod_constrs -> nut NameTable.table - -> KK.rel_expr -> constr_spec -> int -> KK.formula *) -fun sel_axiom_for_sel ext_ctxt j0 +(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr + -> constr_spec -> int -> KK.formula *) +fun sel_axiom_for_sel hol_ctxt j0 (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no, kk_join, ...}) rel_table dom_r ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec) n = let - val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt const n + val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt const n val (r, R, arity) = const_triple rel_table x val R2 = dest_Func R |> snd val z = (epsilon - delta, delta + j0) @@ -842,9 +842,9 @@ (kk_n_ary_function kk R2 r') (kk_no r')) end end -(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table +(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table -> constr_spec -> KK.formula list *) -fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table +fun sel_axioms_for_constr hol_ctxt bits j0 kk rel_table (constr as {const, delta, epsilon, explicit_max, ...}) = let val honors_explicit_max = @@ -866,19 +866,19 @@ " too small for \"max\"") in max_axiom :: - map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr) + map (sel_axiom_for_sel hol_ctxt j0 kk rel_table ran_r constr) (index_seq 0 (num_sels_for_constr_type (snd const))) end end -(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table +(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table -> dtype_spec -> KK.formula list *) -fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table +fun sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table ({constrs, ...} : dtype_spec) = - maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs + maps (sel_axioms_for_constr hol_ctxt bits j0 kk rel_table) constrs -(* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec +(* hol_context -> kodkod_constrs -> nut NameTable.table -> constr_spec -> KK.formula list *) -fun uniqueness_axiom_for_constr ext_ctxt +fun uniqueness_axiom_for_constr hol_ctxt ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...} : kodkod_constrs) rel_table ({const, ...} : constr_spec) = let @@ -887,7 +887,7 @@ kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r) val num_sels = num_sels_for_constr_type (snd const) val triples = map (const_triple rel_table - o boxed_nth_sel_for_constr ext_ctxt const) + o boxed_nth_sel_for_constr hol_ctxt const) (~1 upto num_sels - 1) val j0 = case triples |> hd |> #2 of Func (Atom (_, j0), _) => j0 @@ -903,11 +903,11 @@ (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples))) (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1)))) end -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec -> KK.formula list *) -fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table +fun uniqueness_axioms_for_datatype hol_ctxt kk rel_table ({constrs, ...} : dtype_spec) = - map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs + map (uniqueness_axiom_for_constr hol_ctxt kk rel_table) constrs (* constr_spec -> int *) fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta @@ -924,22 +924,22 @@ kk_disjoint_sets kk rs] end -(* extended_context -> int -> int Typtab.table -> kodkod_constrs +(* hol_context -> int -> int Typtab.table -> kodkod_constrs -> nut NameTable.table -> dtype_spec -> KK.formula list *) fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = [] - | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table + | other_axioms_for_datatype hol_ctxt bits ofs kk rel_table (dtype as {typ, ...}) = let val j0 = offset_of_type ofs typ in - sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table dtype @ - uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @ + sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table dtype @ + uniqueness_axioms_for_datatype hol_ctxt kk rel_table dtype @ partition_axioms_for_datatype j0 kk rel_table dtype end -(* extended_context -> int -> int Typtab.table -> kodkod_constrs +(* hol_context -> int -> int Typtab.table -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> KK.formula list *) -fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes = - acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @ - maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes +fun declarative_axioms_for_datatypes hol_ctxt bits ofs kk rel_table dtypes = + acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @ + maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes (* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *) fun kodkod_formula_from_nut bits ofs liberal diff -r 5e492a862b34 -r 96136eb6218f src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Feb 04 13:36:52 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Feb 04 16:03:15 2010 +0100 @@ -251,7 +251,7 @@ -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep -> int list list -> term *) fun reconstruct_term (maybe_name, base_name, step_name, abs_name) - ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...} + ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...} : scope) sel_names rel_table bounds = let val for_auto = (maybe_name = "") @@ -400,7 +400,7 @@ else NONE) (discr_jsss ~~ constrs) |> the val arg_Ts = curried_binder_types constr_T - val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x) + val sel_xs = map (boxed_nth_sel_for_constr hol_ctxt constr_x) (index_seq 0 (length arg_Ts)) val sel_Rs = map (fn x => get_first @@ -586,7 +586,7 @@ -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> Pretty.T * bool *) fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts} - ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs, + ({hol_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms, debug, binary_ints, destroy_constrs, specialize, skolemize, star_linear_preds, uncurry, fast_descrs, tac_timeout, evals, case_names, def_table, @@ -598,7 +598,7 @@ let val (wacky_names as (_, base_name, step_name, _), ctxt) = add_wacky_syntax ctxt - val ext_ctxt = + val hol_ctxt = {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, binary_ints = binary_ints, destroy_constrs = destroy_constrs, @@ -612,7 +612,7 @@ ersatz_table = ersatz_table, skolems = skolems, special_funs = special_funs, unrolled_preds = unrolled_preds, wf_cache = wf_cache, constr_cache = constr_cache} - val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns, + val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns, bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs} (* typ -> typ -> rep -> int list list -> term *) @@ -644,7 +644,7 @@ end | ConstName (s, T, _) => (assign_operator_for_const (s, T), - user_friendly_const ext_ctxt (base_name, step_name) formats (s, T), + user_friendly_const hol_ctxt (base_name, step_name) formats (s, T), T) | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\ \pretty_for_assign", [name]) @@ -724,7 +724,7 @@ (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> term -> bool option *) -fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, debug, ...}, +fun prove_hol_model (scope as {hol_ctxt as {thy, ctxt, debug, ...}, card_assigns, ...}) auto_timeout free_names sel_names rel_table bounds prop = let diff -r 5e492a862b34 -r 96136eb6218f src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 04 13:36:52 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 04 16:03:15 2010 +0100 @@ -8,10 +8,10 @@ signature NITPICK_MONO = sig datatype sign = Plus | Minus - type extended_context = Nitpick_HOL.extended_context + type hol_context = Nitpick_HOL.hol_context val formulas_monotonic : - extended_context -> typ -> sign -> term list -> term list -> term -> bool + hol_context -> typ -> sign -> term list -> term list -> term -> bool end; structure Nitpick_Mono : NITPICK_MONO = @@ -35,7 +35,7 @@ CRec of string * typ list type cdata = - {ext_ctxt: extended_context, + {hol_ctxt: hol_context, alpha_T: typ, max_fresh: int Unsynchronized.ref, datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref, @@ -114,9 +114,9 @@ | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs | flatten_ctype C = [C] -(* extended_context -> typ -> cdata *) -fun initial_cdata ext_ctxt alpha_T = - ({ext_ctxt = ext_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0, +(* hol_context -> typ -> cdata *) +fun initial_cdata hol_ctxt alpha_T = + ({hol_ctxt = hol_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []} : cdata) @@ -188,7 +188,7 @@ in List.app repair_one (!constr_cache) end (* cdata -> typ -> ctype *) -fun fresh_ctype_for_type ({ext_ctxt as {thy, ...}, alpha_T, max_fresh, +fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, alpha_T, max_fresh, datatype_cache, constr_cache, ...} : cdata) = let (* typ -> typ -> ctype *) @@ -217,7 +217,7 @@ | NONE => let val _ = Unsynchronized.change datatype_cache (cons (z, CRec z)) - val xs = datatype_constrs ext_ctxt T + val xs = datatype_constrs hol_ctxt T val (all_Cs, constr_Cs) = fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) => let @@ -264,7 +264,7 @@ end (* cdata -> styp -> ctype *) -fun ctype_for_constr (cdata as {ext_ctxt as {thy, ...}, alpha_T, constr_cache, +fun ctype_for_constr (cdata as {hol_ctxt as {thy, ...}, alpha_T, constr_cache, ...}) (x as (_, T)) = if could_exist_alpha_sub_ctype thy alpha_T T then case AList.lookup (op =) (!constr_cache) x of @@ -278,8 +278,8 @@ AList.lookup (op =) (!constr_cache) x |> the) else fresh_ctype_for_type cdata T -fun ctype_for_sel (cdata as {ext_ctxt, ...}) (x as (s, _)) = - x |> boxed_constr_for_sel ext_ctxt |> ctype_for_constr cdata +fun ctype_for_sel (cdata as {hol_ctxt, ...}) (x as (s, _)) = + x |> boxed_constr_for_sel hol_ctxt |> ctype_for_constr cdata |> sel_ctype_from_constr_ctype s (* literal list -> ctype -> ctype *) @@ -549,7 +549,7 @@ handle List.Empty => initial_gamma (* cdata -> term -> accumulator -> ctype * accumulator *) -fun consider_term (cdata as {ext_ctxt as {ctxt, thy, def_table, ...}, alpha_T, +fun consider_term (cdata as {hol_ctxt as {ctxt, thy, def_table, ...}, alpha_T, max_fresh, ...}) = let (* typ -> ctype *) @@ -806,7 +806,7 @@ in do_term end (* cdata -> sign -> term -> accumulator -> accumulator *) -fun consider_general_formula (cdata as {ext_ctxt as {ctxt, ...}, ...}) = +fun consider_general_formula (cdata as {hol_ctxt as {ctxt, ...}, ...}) = let (* typ -> ctype *) val ctype_for = fresh_ctype_for_type cdata @@ -895,7 +895,7 @@ not (is_harmless_axiom t) ? consider_general_formula cdata sn t (* cdata -> term -> accumulator -> accumulator *) -fun consider_definitional_axiom (cdata as {ext_ctxt as {thy, ...}, ...}) t = +fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t = if not (is_constr_pattern_formula thy t) then consider_nondefinitional_axiom cdata Plus t else if is_harmless_axiom t then @@ -945,13 +945,13 @@ map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts |> cat_lines |> print_g -(* extended_context -> typ -> sign -> term list -> term list -> term -> bool *) -fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts +(* hol_context -> typ -> sign -> term list -> term list -> term -> bool *) +fun formulas_monotonic (hol_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts core_t = let val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^ Syntax.string_of_typ ctxt alpha_T) - val cdata as {max_fresh, ...} = initial_cdata ext_ctxt alpha_T + val cdata as {max_fresh, ...} = initial_cdata hol_ctxt alpha_T val (gamma, cset) = (initial_gamma, slack) |> fold (consider_definitional_axiom cdata) def_ts diff -r 5e492a862b34 -r 96136eb6218f src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Feb 04 13:36:52 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Feb 04 16:03:15 2010 +0100 @@ -8,7 +8,7 @@ signature NITPICK_NUT = sig type special_fun = Nitpick_HOL.special_fun - type extended_context = Nitpick_HOL.extended_context + type hol_context = Nitpick_HOL.hol_context type scope = Nitpick_Scope.scope type name_pool = Nitpick_Peephole.name_pool type rep = Nitpick_Rep.rep @@ -106,7 +106,7 @@ val name_ord : (nut * nut) -> order val the_name : 'a NameTable.table -> nut -> 'a val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index - val nut_from_term : extended_context -> op2 -> term -> nut + val nut_from_term : hol_context -> op2 -> term -> nut val choose_reps_for_free_vars : scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table val choose_reps_for_consts : @@ -466,8 +466,8 @@ fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z] | factorize z = [z] -(* extended_context -> op2 -> term -> nut *) -fun nut_from_term (ext_ctxt as {thy, fast_descrs, special_funs, ...}) eq = +(* hol_context -> op2 -> term -> nut *) +fun nut_from_term (hol_ctxt as {thy, fast_descrs, special_funs, ...}) eq = let (* string list -> typ list -> term -> nut *) fun aux eq ss Ts t = @@ -597,7 +597,7 @@ Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2) | (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any) | (Const (@{const_name finite}, T), [t1]) => - (if is_finite_type ext_ctxt (domain_type T) then + (if is_finite_type hol_ctxt (domain_type T) then Cst (True, bool_T, Any) else case t1 of Const (@{const_name top}, _) => Cst (False, bool_T, Any) @@ -712,7 +712,7 @@ in (v :: vs, NameTable.update (v, R) table) end (* scope -> bool -> nut -> nut list * rep NameTable.table -> nut list * rep NameTable.table *) -fun choose_rep_for_const (scope as {ext_ctxt as {thy, ctxt, ...}, datatypes, +fun choose_rep_for_const (scope as {hol_ctxt as {thy, ctxt, ...}, datatypes, ofs, ...}) all_exact v (vs, table) = let val x as (s, T) = (nickname_of v, type_of v) @@ -747,10 +747,10 @@ (* scope -> styp -> int -> nut list * rep NameTable.table -> nut list * rep NameTable.table *) -fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) (x as (_, T)) n +fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, ...}) (x as (_, T)) n (vs, table) = let - val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n + val (s', T') = boxed_nth_sel_for_constr hol_ctxt x n val R' = if n = ~1 orelse is_word_type (body_type T) orelse (is_fun_type (range_type T') andalso is_boolean_type (body_type T')) then @@ -890,7 +890,7 @@ | untuple f u = if rep_of u = Unit then [] else [f u] (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *) -fun choose_reps_in_nut (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns, +fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}) liberal table def = let diff -r 5e492a862b34 -r 96136eb6218f src/HOL/Tools/Nitpick/nitpick_preproc.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Feb 04 16:03:15 2010 +0100 @@ -0,0 +1,1431 @@ +(* Title: HOL/Tools/Nitpick/nitpick_preproc.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2008, 2009, 2010 + +Nitpick's HOL preprocessor. +*) + +signature NITPICK_PREPROC = +sig + type hol_context = Nitpick_HOL.hol_context + val preprocess_term : + hol_context -> term -> ((term list * term list) * (bool * bool)) * term +end + +structure Nitpick_Preproc : NITPICK_PREPROC = +struct + +open Nitpick_Util +open Nitpick_HOL + +(* polarity -> string -> bool *) +fun is_positive_existential polar quant_s = + (polar = Pos andalso quant_s = @{const_name Ex}) orelse + (polar = Neg andalso quant_s <> @{const_name Ex}) + +(** Binary coding of integers **) + +(* If a formula contains a numeral whose absolute value is more than this + threshold, the unary coding is likely not to work well and we prefer the + binary coding. *) +val binary_int_threshold = 3 + +(* term -> bool *) +fun may_use_binary_ints (t1 $ t2) = + may_use_binary_ints t1 andalso may_use_binary_ints t2 + | may_use_binary_ints (t as Const (s, _)) = + t <> @{const Suc} andalso + not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, + @{const_name nat_gcd}, @{const_name nat_lcm}, + @{const_name Frac}, @{const_name norm_frac}] s) + | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t' + | may_use_binary_ints _ = true +fun should_use_binary_ints (t1 $ t2) = + should_use_binary_ints t1 orelse should_use_binary_ints t2 + | should_use_binary_ints (Const (s, _)) = + member (op =) [@{const_name times_nat_inst.times_nat}, + @{const_name div_nat_inst.div_nat}, + @{const_name times_int_inst.times_int}, + @{const_name div_int_inst.div_int}] s orelse + (String.isPrefix numeral_prefix s andalso + let val n = the (Int.fromString (unprefix numeral_prefix s)) in + n < ~ binary_int_threshold orelse n > binary_int_threshold + end) + | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t' + | should_use_binary_ints _ = false + +(* typ -> typ *) +fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"} + | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"} + | binarize_nat_and_int_in_type (Type (s, Ts)) = + Type (s, map binarize_nat_and_int_in_type Ts) + | binarize_nat_and_int_in_type T = T +(* term -> term *) +val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type + +(** Uncurrying **) + +(* theory -> term -> int Termtab.tab -> int Termtab.tab *) +fun add_to_uncurry_table thy t = + let + (* term -> term list -> int Termtab.tab -> int Termtab.tab *) + fun aux (t1 $ t2) args table = + let val table = aux t2 [] table in aux t1 (t2 :: args) table end + | aux (Abs (_, _, t')) _ table = aux t' [] table + | aux (t as Const (x as (s, _))) args table = + if is_built_in_const true x orelse is_constr_like thy x orelse + is_sel s orelse s = @{const_name Sigma} then + table + else + Termtab.map_default (t, 65536) (curry Int.min (length args)) table + | aux _ _ table = table + in aux t [] end + +(* int -> int -> string *) +fun uncurry_prefix_for k j = + uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep + +(* int Termtab.tab term -> term *) +fun uncurry_term table t = + let + (* term -> term list -> term *) + fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args) + | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args) + | aux (t as Const (s, T)) args = + (case Termtab.lookup table t of + SOME n => + if n >= 2 then + let + val (arg_Ts, rest_T) = strip_n_binders n T + val j = + if hd arg_Ts = @{typ bisim_iterator} orelse + is_fp_iterator_type (hd arg_Ts) then + 1 + else case find_index (not_equal bool_T) arg_Ts of + ~1 => n + | j => j + val ((before_args, tuple_args), after_args) = + args |> chop n |>> chop j + val ((before_arg_Ts, tuple_arg_Ts), rest_T) = + T |> strip_n_binders n |>> chop j + val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts + in + if n - j < 2 then + betapplys (t, args) + else + betapplys (Const (uncurry_prefix_for (n - j) j ^ s, + before_arg_Ts ---> tuple_T --> rest_T), + before_args @ [mk_flat_tuple tuple_T tuple_args] @ + after_args) + end + else + betapplys (t, args) + | NONE => betapplys (t, args)) + | aux t args = betapplys (t, args) + in aux t [] end + +(** Boxing **) + +(* hol_context -> typ -> term -> term *) +fun constr_expand (hol_ctxt as {thy, ...}) T t = + (case head_of t of + Const x => if is_constr_like thy x then t else raise SAME () + | _ => raise SAME ()) + handle SAME () => + let + val x' as (_, T') = + if is_pair_type T then + let val (T1, T2) = HOLogic.dest_prodT T in + (@{const_name Pair}, T1 --> T2 --> T) + end + else + datatype_constrs hol_ctxt T |> hd + val arg_Ts = binder_types T' + in + list_comb (Const x', map2 (select_nth_constr_arg thy x' t) + (index_seq 0 (length arg_Ts)) arg_Ts) + end + +(* hol_context -> bool -> term -> term *) +fun box_fun_and_pair_in_term (hol_ctxt as {thy, fast_descrs, ...}) def orig_t = + let + (* typ -> typ *) + fun box_relational_operator_type (Type ("fun", Ts)) = + Type ("fun", map box_relational_operator_type Ts) + | box_relational_operator_type (Type ("*", Ts)) = + Type ("*", map (box_type hol_ctxt InPair) Ts) + | box_relational_operator_type T = T + (* (term -> term) -> int -> term -> term *) + fun coerce_bound_no f j t = + case t of + t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2 + | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t') + | Bound j' => if j' = j then f t else t + | _ => t + (* typ -> typ -> term -> term *) + fun coerce_bound_0_in_term new_T old_T = + old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0 + (* typ list -> typ -> term -> term *) + and coerce_term Ts new_T old_T t = + if old_T = new_T then + t + else + case (new_T, old_T) of + (Type (new_s, new_Ts as [new_T1, new_T2]), + Type ("fun", [old_T1, old_T2])) => + (case eta_expand Ts t 1 of + Abs (s, _, t') => + Abs (s, new_T1, + t' |> coerce_bound_0_in_term new_T1 old_T1 + |> coerce_term (new_T1 :: Ts) new_T2 old_T2) + |> Envir.eta_contract + |> new_s <> "fun" + ? construct_value thy (@{const_name FunBox}, + Type ("fun", new_Ts) --> new_T) o single + | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\ + \coerce_term", [t'])) + | (Type (new_s, new_Ts as [new_T1, new_T2]), + Type (old_s, old_Ts as [old_T1, old_T2])) => + if old_s = @{type_name fun_box} orelse + old_s = @{type_name pair_box} orelse old_s = "*" then + case constr_expand hol_ctxt old_T t of + Const (@{const_name FunBox}, _) $ t1 => + if new_s = "fun" then + coerce_term Ts new_T (Type ("fun", old_Ts)) t1 + else + construct_value thy + (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T) + [coerce_term Ts (Type ("fun", new_Ts)) + (Type ("fun", old_Ts)) t1] + | Const _ $ t1 $ t2 => + construct_value thy + (if new_s = "*" then @{const_name Pair} + else @{const_name PairBox}, new_Ts ---> new_T) + [coerce_term Ts new_T1 old_T1 t1, + coerce_term Ts new_T2 old_T2 t2] + | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\ + \coerce_term", [t']) + else + raise TYPE ("coerce_term", [new_T, old_T], [t]) + | _ => raise TYPE ("coerce_term", [new_T, old_T], [t]) + (* indexname * typ -> typ * term -> typ option list -> typ option list *) + fun add_boxed_types_for_var (z as (_, T)) (T', t') = + case t' of + Var z' => z' = z ? insert (op =) T' + | Const (@{const_name Pair}, _) $ t1 $ t2 => + (case T' of + Type (_, [T1, T2]) => + fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)] + | _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\ + \add_boxed_types_for_var", [T'], [])) + | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T + (* typ list -> typ list -> term -> indexname * typ -> typ *) + fun box_var_in_def new_Ts old_Ts t (z as (_, T)) = + case t of + @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z + | Const (s0, _) $ t1 $ _ => + if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then + let + val (t', args) = strip_comb t1 + val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t') + in + case fold (add_boxed_types_for_var z) + (fst (strip_n_binders (length args) T') ~~ args) [] of + [T''] => T'' + | _ => T + end + else + T + | _ => T + (* typ list -> typ list -> polarity -> string -> typ -> string -> typ + -> term -> term *) + and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t = + let + val abs_T' = + if polar = Neut orelse is_positive_existential polar quant_s then + box_type hol_ctxt InFunLHS abs_T + else + abs_T + val body_T = body_type quant_T + in + Const (quant_s, (abs_T' --> body_T) --> body_T) + $ Abs (abs_s, abs_T', + t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar) + end + (* typ list -> typ list -> string -> typ -> term -> term -> term *) + and do_equals new_Ts old_Ts s0 T0 t1 t2 = + let + val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2) + val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2) + val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last + in + list_comb (Const (s0, T --> T --> body_type T0), + map2 (coerce_term new_Ts T) [T1, T2] [t1, t2]) + end + (* string -> typ -> term *) + and do_description_operator s T = + let val T1 = box_type hol_ctxt InFunLHS (range_type T) in + Const (s, (T1 --> bool_T) --> T1) + end + (* typ list -> typ list -> polarity -> term -> term *) + and do_term new_Ts old_Ts polar t = + case t of + Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => + do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 + | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 => + do_equals new_Ts old_Ts s0 T0 t1 t2 + | @{const "==>"} $ t1 $ t2 => + @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1 + $ do_term new_Ts old_Ts polar t2 + | @{const Pure.conjunction} $ t1 $ t2 => + @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1 + $ do_term new_Ts old_Ts polar t2 + | @{const Trueprop} $ t1 => + @{const Trueprop} $ do_term new_Ts old_Ts polar t1 + | @{const Not} $ t1 => + @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1 + | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => + do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 + | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => + do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 + | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 => + do_equals new_Ts old_Ts s0 T0 t1 t2 + | @{const "op &"} $ t1 $ t2 => + @{const "op &"} $ do_term new_Ts old_Ts polar t1 + $ do_term new_Ts old_Ts polar t2 + | @{const "op |"} $ t1 $ t2 => + @{const "op |"} $ do_term new_Ts old_Ts polar t1 + $ do_term new_Ts old_Ts polar t2 + | @{const "op -->"} $ t1 $ t2 => + @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1 + $ do_term new_Ts old_Ts polar t2 + | Const (s as @{const_name The}, T) => do_description_operator s T + | Const (s as @{const_name Eps}, T) => do_description_operator s T + | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) => + let val T' = box_type hol_ctxt InSel T2 in + Const (@{const_name quot_normal}, T' --> T') + end + | Const (s as @{const_name Tha}, T) => do_description_operator s T + | Const (x as (s, T)) => + Const (s, if s = @{const_name converse} orelse + s = @{const_name trancl} then + box_relational_operator_type T + else if is_built_in_const fast_descrs x orelse + s = @{const_name Sigma} then + T + else if is_constr_like thy x then + box_type hol_ctxt InConstr T + else if is_sel s + orelse is_rep_fun thy x then + box_type hol_ctxt InSel T + else + box_type hol_ctxt InExpr T) + | t1 $ Abs (s, T, t2') => + let + val t1 = do_term new_Ts old_Ts Neut t1 + val T1 = fastype_of1 (new_Ts, t1) + val (s1, Ts1) = dest_Type T1 + val T' = hd (snd (dest_Type (hd Ts1))) + val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2') + val T2 = fastype_of1 (new_Ts, t2) + val t2 = coerce_term new_Ts (hd Ts1) T2 t2 + in + betapply (if s1 = "fun" then + t1 + else + select_nth_constr_arg thy + (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0 + (Type ("fun", Ts1)), t2) + end + | t1 $ t2 => + let + val t1 = do_term new_Ts old_Ts Neut t1 + val T1 = fastype_of1 (new_Ts, t1) + val (s1, Ts1) = dest_Type T1 + val t2 = do_term new_Ts old_Ts Neut t2 + val T2 = fastype_of1 (new_Ts, t2) + val t2 = coerce_term new_Ts (hd Ts1) T2 t2 + in + betapply (if s1 = "fun" then + t1 + else + select_nth_constr_arg thy + (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0 + (Type ("fun", Ts1)), t2) + end + | Free (s, T) => Free (s, box_type hol_ctxt InExpr T) + | Var (z as (x, T)) => + Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z + else box_type hol_ctxt InExpr T) + | Bound _ => t + | Abs (s, T, t') => + Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t') + in do_term [] [] Pos orig_t end + +(** Destruction of constructors **) + +val val_var_prefix = nitpick_prefix ^ "v" + +(* typ list -> int -> int -> int -> term -> term *) +fun fresh_value_var Ts k n j t = + Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t)) + +(* typ list -> int -> term -> bool *) +fun has_heavy_bounds_or_vars Ts level t = + let + (* typ list -> bool *) + fun aux [] = false + | aux [T] = is_fun_type T orelse is_pair_type T + | aux _ = true + in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end + +(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list + -> term * term list *) +fun pull_out_constr_comb thy Ts relax k level t args seen = + let val t_comb = list_comb (t, args) in + case t of + Const x => + if not relax andalso is_constr thy x andalso + not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso + has_heavy_bounds_or_vars Ts level t_comb andalso + not (loose_bvar (t_comb, level)) then + let + val (j, seen) = case find_index (curry (op =) t_comb) seen of + ~1 => (0, t_comb :: seen) + | j => (j, seen) + in (fresh_value_var Ts k (length seen) j t_comb, seen) end + else + (t_comb, seen) + | _ => (t_comb, seen) + end + +(* (term -> term) -> typ list -> int -> term list -> term list *) +fun equations_for_pulled_out_constrs mk_eq Ts k seen = + let val n = length seen in + map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t)) + (index_seq 0 n) seen + end + +(* theory -> bool -> term -> term *) +fun pull_out_universal_constrs thy def t = + let + val k = maxidx_of_term t + 1 + (* typ list -> bool -> term -> term list -> term list -> term * term list *) + fun do_term Ts def t args seen = + case t of + (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 => + do_eq_or_imp Ts true def t0 t1 t2 seen + | (t0 as @{const "==>"}) $ t1 $ t2 => + if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen + | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 => + do_eq_or_imp Ts true def t0 t1 t2 seen + | (t0 as @{const "op -->"}) $ t1 $ t2 => + do_eq_or_imp Ts false def t0 t1 t2 seen + | Abs (s, T, t') => + let val (t', seen) = do_term (T :: Ts) def t' [] seen in + (list_comb (Abs (s, T, t'), args), seen) + end + | t1 $ t2 => + let val (t2, seen) = do_term Ts def t2 [] seen in + do_term Ts def t1 (t2 :: args) seen + end + | _ => pull_out_constr_comb thy Ts def k 0 t args seen + (* typ list -> bool -> bool -> term -> term -> term -> term list + -> term * term list *) + and do_eq_or_imp Ts eq def t0 t1 t2 seen = + let + val (t2, seen) = if eq andalso def then (t2, seen) + else do_term Ts false t2 [] seen + val (t1, seen) = do_term Ts false t1 [] seen + in (t0 $ t1 $ t2, seen) end + val (concl, seen) = do_term [] def t [] [] + in + Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k + seen, concl) + end + +(* term -> term -> term *) +fun mk_exists v t = + HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t) + +(* theory -> term -> term *) +fun pull_out_existential_constrs thy t = + let + val k = maxidx_of_term t + 1 + (* typ list -> int -> term -> term list -> term list -> term * term list *) + fun aux Ts num_exists t args seen = + case t of + (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) => + let + val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] [] + val n = length seen' + (* unit -> term list *) + fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen' + in + (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen' + |> List.foldl s_conj t1 |> fold mk_exists (vars ()) + |> curry3 Abs s1 T1 |> curry (op $) t0, seen) + end + | t1 $ t2 => + let val (t2, seen) = aux Ts num_exists t2 [] seen in + aux Ts num_exists t1 (t2 :: args) seen + end + | Abs (s, T, t') => + let + val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen) + in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end + | _ => + if num_exists > 0 then + pull_out_constr_comb thy Ts false k num_exists t args seen + else + (list_comb (t, args), seen) + in aux [] 0 t [] [] |> fst end + +(* hol_context -> bool -> term -> term *) +fun destroy_pulled_out_constrs (hol_ctxt as {thy, ...}) axiom t = + let + (* styp -> int *) + val num_occs_of_var = + fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1) + | _ => I) t (K 0) + (* bool -> term -> term *) + fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) = + aux_eq careful true t0 t1 t2 + | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) = + t0 $ aux false t1 $ aux careful t2 + | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) = + aux_eq careful true t0 t1 t2 + | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) = + t0 $ aux false t1 $ aux careful t2 + | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t') + | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2 + | aux _ t = t + (* bool -> bool -> term -> term -> term -> term *) + and aux_eq careful pass1 t0 t1 t2 = + ((if careful then + raise SAME () + else if axiom andalso is_Var t2 andalso + num_occs_of_var (dest_Var t2) = 1 then + @{const True} + else case strip_comb t2 of + (* The first case is not as general as it could be. *) + (Const (@{const_name PairBox}, _), + [Const (@{const_name fst}, _) $ Var z1, + Const (@{const_name snd}, _) $ Var z2]) => + if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True} + else raise SAME () + | (Const (x as (s, T)), args) => + let val arg_Ts = binder_types T in + if length arg_Ts = length args andalso + (is_constr thy x orelse s = @{const_name Pair} orelse + x = (@{const_name Suc}, nat_T --> nat_T)) andalso + (not careful orelse not (is_Var t1) orelse + String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then + discriminate_value hol_ctxt x t1 :: + map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args + |> foldr1 s_conj + else + raise SAME () + end + | _ => raise SAME ()) + |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop) + handle SAME () => if pass1 then aux_eq careful false t0 t2 t1 + else t0 $ aux false t2 $ aux false t1 + (* styp -> term -> int -> typ -> term -> term *) + and sel_eq x t n nth_T nth_t = + HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T + |> aux false + in aux axiom t end + +(** Destruction of universal and existential equalities **) + +(* term -> term *) +fun curry_assms (@{const "==>"} $ (@{const Trueprop} + $ (@{const "op &"} $ t1 $ t2)) $ t3) = + curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3)) + | curry_assms (@{const "==>"} $ t1 $ t2) = + @{const "==>"} $ curry_assms t1 $ curry_assms t2 + | curry_assms t = t + +(* term -> term *) +val destroy_universal_equalities = + let + (* term list -> (indexname * typ) list -> term -> term *) + fun aux prems zs t = + case t of + @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2 + | _ => Logic.list_implies (rev prems, t) + (* term list -> (indexname * typ) list -> term -> term -> term *) + and aux_implies prems zs t1 t2 = + case t1 of + Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2 + | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') => + aux_eq prems zs z t' t1 t2 + | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) => + aux_eq prems zs z t' t1 t2 + | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2 + (* term list -> (indexname * typ) list -> indexname * typ -> term -> term + -> term -> term *) + and aux_eq prems zs z t' t1 t2 = + if not (member (op =) zs z) andalso + not (exists_subterm (curry (op =) (Var z)) t') then + aux prems zs (subst_free [(Var z, t')] t2) + else + aux (t1 :: prems) (Term.add_vars t1 zs) t2 + in aux [] [] end + +(* theory -> int -> term list -> term list -> (term * term list) option *) +fun find_bound_assign _ _ _ [] = NONE + | find_bound_assign thy j seen (t :: ts) = + let + (* bool -> term -> term -> (term * term list) option *) + fun aux pass1 t1 t2 = + (if loose_bvar1 (t2, j) then + if pass1 then aux false t2 t1 else raise SAME () + else case t1 of + Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME () + | Const (s, Type ("fun", [T1, T2])) $ Bound j' => + if j' = j andalso + s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then + SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2], + ts @ seen) + else + raise SAME () + | _ => raise SAME ()) + handle SAME () => find_bound_assign thy j (t :: seen) ts + in + case t of + Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2 + | _ => find_bound_assign thy j (t :: seen) ts + end + +(* int -> term -> term -> term *) +fun subst_one_bound j arg t = + let + fun aux (Bound i, lev) = + if i < lev then raise SAME () + else if i = lev then incr_boundvars (lev - j) arg + else Bound (i - 1) + | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1)) + | aux (f $ t, lev) = + (aux (f, lev) $ (aux (t, lev) handle SAME () => t) + handle SAME () => f $ aux (t, lev)) + | aux _ = raise SAME () + in aux (t, j) handle SAME () => t end + +(* theory -> term -> term *) +fun destroy_existential_equalities thy = + let + (* string list -> typ list -> term list -> term *) + fun kill [] [] ts = foldr1 s_conj ts + | kill (s :: ss) (T :: Ts) ts = + (case find_bound_assign thy (length ss) [] ts of + SOME (_, []) => @{const True} + | SOME (arg_t, ts) => + kill ss Ts (map (subst_one_bound (length ss) + (incr_bv (~1, length ss + 1, arg_t))) ts) + | NONE => + Const (@{const_name Ex}, (T --> bool_T) --> bool_T) + $ Abs (s, T, kill ss Ts ts)) + | kill _ _ _ = raise UnequalLengths + (* string list -> typ list -> term -> term *) + fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) = + gather (ss @ [s1]) (Ts @ [T1]) t1 + | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1) + | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2 + | gather [] [] t = t + | gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t)) + in gather [] [] end + +(** Skolemization **) + +(* int -> int -> string *) +fun skolem_prefix_for k j = + skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep + +(* hol_context -> int -> term -> term *) +fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...}) + skolem_depth = + let + (* int list -> int list *) + val incrs = map (Integer.add 1) + (* string list -> typ list -> int list -> int -> polarity -> term -> term *) + fun aux ss Ts js depth polar t = + let + (* string -> typ -> string -> typ -> term -> term *) + fun do_quantifier quant_s quant_T abs_s abs_T t = + if not (loose_bvar1 (t, 0)) then + aux ss Ts js depth polar (incr_boundvars ~1 t) + else if depth <= skolem_depth andalso + is_positive_existential polar quant_s then + let + val j = length (!skolems) + 1 + val sko_s = skolem_prefix_for (length js) j ^ abs_s + val _ = Unsynchronized.change skolems (cons (sko_s, ss)) + val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T), + map Bound (rev js)) + val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t) + in + if null js then betapply (abs_t, sko_t) + else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t + end + else + Const (quant_s, quant_T) + $ Abs (abs_s, abs_T, + if is_higher_order_type abs_T then + t + else + aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js) + (depth + 1) polar t) + in + case t of + Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => + do_quantifier s0 T0 s1 T1 t1 + | @{const "==>"} $ t1 $ t2 => + @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1 + $ aux ss Ts js depth polar t2 + | @{const Pure.conjunction} $ t1 $ t2 => + @{const Pure.conjunction} $ aux ss Ts js depth polar t1 + $ aux ss Ts js depth polar t2 + | @{const Trueprop} $ t1 => + @{const Trueprop} $ aux ss Ts js depth polar t1 + | @{const Not} $ t1 => + @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1 + | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => + do_quantifier s0 T0 s1 T1 t1 + | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => + do_quantifier s0 T0 s1 T1 t1 + | @{const "op &"} $ t1 $ t2 => + @{const "op &"} $ aux ss Ts js depth polar t1 + $ aux ss Ts js depth polar t2 + | @{const "op |"} $ t1 $ t2 => + @{const "op |"} $ aux ss Ts js depth polar t1 + $ aux ss Ts js depth polar t2 + | @{const "op -->"} $ t1 $ t2 => + @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1 + $ aux ss Ts js depth polar t2 + | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 => + t0 $ t1 $ aux ss Ts js depth polar t2 + | Const (x as (s, T)) => + if is_inductive_pred hol_ctxt x andalso + not (is_well_founded_inductive_pred hol_ctxt x) then + let + val gfp = (fixpoint_kind_of_const thy def_table x = Gfp) + val (pref, connective, set_oper) = + if gfp then + (lbfp_prefix, + @{const "op |"}, + @{const_name upper_semilattice_fun_inst.sup_fun}) + else + (ubfp_prefix, + @{const "op &"}, + @{const_name lower_semilattice_fun_inst.inf_fun}) + (* unit -> term *) + fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x + |> aux ss Ts js depth polar + fun neg () = Const (pref ^ s, T) + in + (case polar |> gfp ? flip_polarity of + Pos => pos () + | Neg => neg () + | Neut => + if is_fun_type T then + let + val ((trunk_arg_Ts, rump_arg_T), body_T) = + T |> strip_type |>> split_last + val set_T = rump_arg_T --> body_T + (* (unit -> term) -> term *) + fun app f = + list_comb (f (), + map Bound (length trunk_arg_Ts - 1 downto 0)) + in + List.foldr absdummy + (Const (set_oper, set_T --> set_T --> set_T) + $ app pos $ app neg) trunk_arg_Ts + end + else + connective $ pos () $ neg ()) + end + else + Const x + | t1 $ t2 => + betapply (aux ss Ts [] (skolem_depth + 1) polar t1, + aux ss Ts [] depth Neut t2) + | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1) + | _ => t + end + in aux [] [] [] 0 Pos end + +(** Function specialization **) + +(* term -> term list *) +fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2 + | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1 + | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) = + snd (strip_comb t1) + | params_in_equation _ = [] + +(* styp -> styp -> int list -> term list -> term list -> term -> term *) +fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t = + let + val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0 + + 1 + val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t + val fixed_params = filter_indices fixed_js (params_in_equation t) + (* term list -> term -> term *) + fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args) + | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1 + | aux args t = + if t = Const x then + list_comb (Const x', extra_args @ filter_out_indices fixed_js args) + else + let val j = find_index (curry (op =) t) fixed_params in + list_comb (if j >= 0 then nth fixed_args j else t, args) + end + in aux [] t end + +(* hol_context -> styp -> (int * term option) list *) +fun static_args_in_term ({ersatz_table, ...} : hol_context) x t = + let + (* term -> term list -> term list -> term list list *) + fun fun_calls (Abs (_, _, t)) _ = fun_calls t [] + | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args) + | fun_calls t args = + (case t of + Const (x' as (s', T')) => + x = x' orelse (case AList.lookup (op =) ersatz_table s' of + SOME s'' => x = (s'', T') + | NONE => false) + | _ => false) ? cons args + (* term list list -> term list list -> term list -> term list list *) + fun call_sets [] [] vs = [vs] + | call_sets [] uss vs = vs :: call_sets uss [] [] + | call_sets ([] :: _) _ _ = [] + | call_sets ((t :: ts) :: tss) uss vs = + OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss) + val sets = call_sets (fun_calls t [] []) [] [] + val indexed_sets = sets ~~ (index_seq 0 (length sets)) + in + fold_rev (fn (set, j) => + case set of + [Var _] => AList.lookup (op =) indexed_sets set = SOME j + ? cons (j, NONE) + | [t as Const _] => cons (j, SOME t) + | [t as Free _] => cons (j, SOME t) + | _ => I) indexed_sets [] + end +(* hol_context -> styp -> term list -> (int * term option) list *) +fun static_args_in_terms hol_ctxt x = + map (static_args_in_term hol_ctxt x) + #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord))) + +(* (int * term option) list -> (int * term) list -> int list *) +fun overlapping_indices [] _ = [] + | overlapping_indices _ [] = [] + | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') = + if j1 < j2 then overlapping_indices ps1' ps2 + else if j1 > j2 then overlapping_indices ps1 ps2' + else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1 + +(* typ list -> term -> bool *) +fun is_eligible_arg Ts t = + let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in + null bad_Ts orelse + (is_higher_order_type (fastype_of1 (Ts, t)) andalso + forall (not o is_higher_order_type) bad_Ts) + end + +(* int -> string *) +fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep + +(* If a constant's definition is picked up deeper than this threshold, we + prevent excessive specialization by not specializing it. *) +val special_max_depth = 20 + +val bound_var_prefix = "b" + +(* hol_context -> int -> term -> term *) +fun specialize_consts_in_term (hol_ctxt as {thy, specialize, simp_table, + special_funs, ...}) depth t = + if not specialize orelse depth > special_max_depth then + t + else + let + val blacklist = if depth = 0 then [] + else case term_under_def t of Const x => [x] | _ => [] + (* term list -> typ list -> term -> term *) + fun aux args Ts (Const (x as (s, T))) = + ((if not (member (op =) blacklist x) andalso not (null args) andalso + not (String.isPrefix special_prefix s) andalso + is_equational_fun hol_ctxt x then + let + val eligible_args = filter (is_eligible_arg Ts o snd) + (index_seq 0 (length args) ~~ args) + val _ = not (null eligible_args) orelse raise SAME () + val old_axs = equational_fun_axioms hol_ctxt x + |> map (destroy_existential_equalities thy) + val static_params = static_args_in_terms hol_ctxt x old_axs + val fixed_js = overlapping_indices static_params eligible_args + val _ = not (null fixed_js) orelse raise SAME () + val fixed_args = filter_indices fixed_js args + val vars = fold Term.add_vars fixed_args [] + |> sort (TermOrd.fast_indexname_ord o pairself fst) + val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js)) + fixed_args [] + |> sort int_ord + val live_args = filter_out_indices fixed_js args + val extra_args = map Var vars @ map Bound bound_js @ live_args + val extra_Ts = map snd vars @ filter_indices bound_js Ts + val k = maxidx_of_term t + 1 + (* int -> term *) + fun var_for_bound_no j = + Var ((bound_var_prefix ^ + nat_subscript (find_index (curry (op =) j) bound_js + + 1), k), + nth Ts j) + val fixed_args_in_axiom = + map (curry subst_bounds + (map var_for_bound_no (index_seq 0 (length Ts)))) + fixed_args + in + case AList.lookup (op =) (!special_funs) + (x, fixed_js, fixed_args_in_axiom) of + SOME x' => list_comb (Const x', extra_args) + | NONE => + let + val extra_args_in_axiom = + map Var vars @ map var_for_bound_no bound_js + val x' as (s', _) = + (special_prefix_for (length (!special_funs) + 1) ^ s, + extra_Ts @ filter_out_indices fixed_js (binder_types T) + ---> body_type T) + val new_axs = + map (specialize_fun_axiom x x' fixed_js + fixed_args_in_axiom extra_args_in_axiom) old_axs + val _ = + Unsynchronized.change special_funs + (cons ((x, fixed_js, fixed_args_in_axiom), x')) + val _ = add_simps simp_table s' new_axs + in list_comb (Const x', extra_args) end + end + else + raise SAME ()) + handle SAME () => list_comb (Const x, args)) + | aux args Ts (Abs (s, T, t)) = + list_comb (Abs (s, T, aux [] (T :: Ts) t), args) + | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1 + | aux args _ t = list_comb (t, args) + in aux [] [] t end + +type special_triple = int list * term list * styp + +val cong_var_prefix = "c" + +(* styp -> special_triple -> special_triple -> term *) +fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) = + let + val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2) + val Ts = binder_types T + val max_j = fold (fold Integer.max) [js1, js2] ~1 + val (eqs, (args1, args2)) = + fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j) + (js1 ~~ ts1, js2 ~~ ts2) of + (SOME t1, SOME t2) => apfst (cons (t1, t2)) + | (SOME t1, NONE) => apsnd (apsnd (cons t1)) + | (NONE, SOME t2) => apsnd (apfst (cons t2)) + | (NONE, NONE) => + let val v = Var ((cong_var_prefix ^ nat_subscript j, 0), + nth Ts j) in + apsnd (pairself (cons v)) + end) (max_j downto 0) ([], ([], [])) + in + Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =) + |> map Logic.mk_equals, + Logic.mk_equals (list_comb (Const x1, bounds1 @ args1), + list_comb (Const x2, bounds2 @ args2))) + |> Refute.close_form (* TODO: needed? *) + end + +(* hol_context -> styp list -> term list *) +fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs = + let + val groups = + !special_funs + |> map (fn ((x, js, ts), x') => (x, (js, ts, x'))) + |> AList.group (op =) + |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst) + |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x))) + (* special_triple -> int *) + fun generality (js, _, _) = ~(length js) + (* special_triple -> special_triple -> bool *) + fun is_more_specific (j1, t1, x1) (j2, t2, x2) = + x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord) + (j2 ~~ t2, j1 ~~ t1) + (* styp -> special_triple list -> special_triple list -> special_triple list + -> term list -> term list *) + fun do_pass_1 _ [] [_] [_] = I + | do_pass_1 x skipped _ [] = do_pass_2 x skipped + | do_pass_1 x skipped all (z :: zs) = + case filter (is_more_specific z) all + |> sort (int_ord o pairself generality) of + [] => do_pass_1 x (z :: skipped) all zs + | (z' :: _) => cons (special_congruence_axiom x z z') + #> do_pass_1 x skipped all zs + (* styp -> special_triple list -> term list -> term list *) + and do_pass_2 _ [] = I + | do_pass_2 x (z :: zs) = + fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs + in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end + +(** Axiom selection **) + +(* Similar to "Refute.specialize_type" but returns all matches rather than only + the first (preorder) match. *) +(* theory -> styp -> term -> term list *) +fun multi_specialize_type thy slack (x as (s, T)) t = + let + (* term -> (typ * term) list -> (typ * term) list *) + fun aux (Const (s', T')) ys = + if s = s' then + ys |> (if AList.defined (op =) ys T' then + I + else + cons (T', Refute.monomorphic_term + (Sign.typ_match thy (T', T) Vartab.empty) t) + handle Type.TYPE_MATCH => I + | Refute.REFUTE _ => + if slack then + I + else + raise NOT_SUPPORTED ("too much polymorphism in \ + \axiom involving " ^ quote s)) + else + ys + | aux _ ys = ys + in map snd (fold_aterms aux t []) end + +(* theory -> bool -> const_table -> styp -> term list *) +fun nondef_props_for_const thy slack table (x as (s, _)) = + these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x) + +(* 'a Symtab.table -> 'a list *) +fun all_table_entries table = Symtab.fold (append o snd) table [] +(* const_table -> string -> const_table *) +fun extra_table table s = Symtab.make [(s, all_table_entries table)] + +(* int -> term -> term *) +fun eval_axiom_for_term j t = + Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t) + +(* term -> bool *) +val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals) + +(* Prevents divergence in case of cyclic or infinite axiom dependencies. *) +val axioms_max_depth = 255 + +(* hol_context -> term -> (term list * term list) * (bool * bool) *) +fun axioms_for_term + (hol_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals, + def_table, nondef_table, user_nondefs, ...}) t = + let + type accumulator = styp list * (term list * term list) + (* (term list * term list -> term list) + -> ((term list -> term list) -> term list * term list + -> term list * term list) + -> int -> term -> accumulator -> accumulator *) + fun add_axiom get app depth t (accum as (xs, axs)) = + let + val t = t |> unfold_defs_in_term hol_ctxt + |> skolemize_term_and_more hol_ctxt ~1 + in + if is_trivial_equation t then + accum + else + let val t' = t |> specialize_consts_in_term hol_ctxt depth in + if exists (member (op aconv) (get axs)) [t, t'] then accum + else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs) + end + end + (* int -> term -> accumulator -> accumulator *) + and add_def_axiom depth = add_axiom fst apfst depth + and add_nondef_axiom depth = add_axiom snd apsnd depth + and add_maybe_def_axiom depth t = + (if head_of t <> @{const "==>"} then add_def_axiom + else add_nondef_axiom) depth t + and add_eq_axiom depth t = + (if is_constr_pattern_formula thy t then add_def_axiom + else add_nondef_axiom) depth t + (* int -> term -> accumulator -> accumulator *) + and add_axioms_for_term depth t (accum as (xs, axs)) = + case t of + t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2] + | Const (x as (s, T)) => + (if member (op =) xs x orelse is_built_in_const fast_descrs x then + accum + else + let val accum as (xs, _) = (x :: xs, axs) in + if depth > axioms_max_depth then + raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\ + \add_axioms_for_term", + "too many nested axioms (" ^ + string_of_int depth ^ ")") + else if Refute.is_const_of_class thy x then + let + val class = Logic.class_of_const s + val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), + class) + val ax1 = try (Refute.specialize_type thy x) of_class + val ax2 = Option.map (Refute.specialize_type thy x o snd) + (Refute.get_classdef thy class) + in + fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2]) + accum + end + else if is_constr thy x then + accum + else if is_equational_fun hol_ctxt x then + fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) + accum + else if is_abs_fun thy x then + if is_quot_type thy (range_type T) then + raise NOT_SUPPORTED "\"Abs_\" function of quotient type" + else + accum |> fold (add_nondef_axiom depth) + (nondef_props_for_const thy false nondef_table x) + |> is_funky_typedef thy (range_type T) + ? fold (add_maybe_def_axiom depth) + (nondef_props_for_const thy true + (extra_table def_table s) x) + else if is_rep_fun thy x then + if is_quot_type thy (domain_type T) then + raise NOT_SUPPORTED "\"Rep_\" function of quotient type" + else + accum |> fold (add_nondef_axiom depth) + (nondef_props_for_const thy false nondef_table x) + |> is_funky_typedef thy (range_type T) + ? fold (add_maybe_def_axiom depth) + (nondef_props_for_const thy true + (extra_table def_table s) x) + |> add_axioms_for_term depth + (Const (mate_of_rep_fun thy x)) + |> fold (add_def_axiom depth) + (inverse_axioms_for_rep_fun thy x) + else + accum |> user_axioms <> SOME false + ? fold (add_nondef_axiom depth) + (nondef_props_for_const thy false nondef_table x) + end) + |> add_axioms_for_type depth T + | Free (_, T) => add_axioms_for_type depth T accum + | Var (_, T) => add_axioms_for_type depth T accum + | Bound _ => accum + | Abs (_, T, t) => accum |> add_axioms_for_term depth t + |> add_axioms_for_type depth T + (* int -> typ -> accumulator -> accumulator *) + and add_axioms_for_type depth T = + case T of + Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts + | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts + | @{typ prop} => I + | @{typ bool} => I + | @{typ unit} => I + | TFree (_, S) => add_axioms_for_sort depth T S + | TVar (_, S) => add_axioms_for_sort depth T S + | Type (z as (s, Ts)) => + fold (add_axioms_for_type depth) Ts + #> (if is_pure_typedef thy T then + fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z) + else if is_quot_type thy T then + fold (add_def_axiom depth) (optimized_quot_type_axioms thy z) + else if max_bisim_depth >= 0 andalso is_codatatype thy T then + fold (add_maybe_def_axiom depth) + (codatatype_bisim_axioms hol_ctxt T) + else + I) + (* int -> typ -> sort -> accumulator -> accumulator *) + and add_axioms_for_sort depth T S = + let + val supers = Sign.complete_sort thy S + val class_axioms = + maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms + handle ERROR _ => [])) supers + val monomorphic_class_axioms = + map (fn t => case Term.add_tvars t [] of + [] => t + | [(x, S)] => + Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t + | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\ + \add_axioms_for_sort", [t])) + class_axioms + in fold (add_nondef_axiom depth) monomorphic_class_axioms end + val (mono_user_nondefs, poly_user_nondefs) = + List.partition (null o Term.hidden_polymorphism) user_nondefs + val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals)) + evals + val (xs, (defs, nondefs)) = + ([], ([], [])) |> add_axioms_for_term 1 t + |> fold_rev (add_def_axiom 1) eval_axioms + |> user_axioms = SOME true + ? fold (add_nondef_axiom 1) mono_user_nondefs + val defs = defs @ special_congruence_axioms hol_ctxt xs + in + ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs, + null poly_user_nondefs)) + end + +(** Simplification of constructor/selector terms **) + +(* theory -> term -> term *) +fun simplify_constrs_and_sels thy t = + let + (* term -> int -> term *) + fun is_nth_sel_on t' n (Const (s, _) $ t) = + (t = t' andalso is_sel_like_and_no_discr s andalso + sel_no_from_name s = n) + | is_nth_sel_on _ _ _ = false + (* term -> term list -> term *) + fun do_term (Const (@{const_name Rep_Frac}, _) + $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 [] + | do_term (Const (@{const_name Abs_Frac}, _) + $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 [] + | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args) + | do_term (t as Const (x as (s, T))) (args as _ :: _) = + ((if is_constr_like thy x then + if length args = num_binder_types T then + case hd args of + Const (x' as (_, T')) $ t' => + if domain_type T' = body_type T andalso + forall (uncurry (is_nth_sel_on t')) + (index_seq 0 (length args) ~~ args) then + t' + else + raise SAME () + | _ => raise SAME () + else + raise SAME () + else if is_sel_like_and_no_discr s then + case strip_comb (hd args) of + (Const (x' as (s', T')), ts') => + if is_constr_like thy x' andalso + constr_name_for_sel_like s = s' andalso + not (exists is_pair_type (binder_types T')) then + list_comb (nth ts' (sel_no_from_name s), tl args) + else + raise SAME () + | _ => raise SAME () + else + raise SAME ()) + handle SAME () => betapplys (t, args)) + | do_term (Abs (s, T, t')) args = + betapplys (Abs (s, T, do_term t' []), args) + | do_term t args = betapplys (t, args) + in do_term t [] end + +(** Quantifier massaging: Distributing quantifiers **) + +(* term -> term *) +fun distribute_quantifiers t = + case t of + (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) => + (case t1 of + (t10 as @{const "op &"}) $ t11 $ t12 => + t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) + $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) + | (t10 as @{const Not}) $ t11 => + t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0) + $ Abs (s, T1, t11)) + | t1 => + if not (loose_bvar1 (t1, 0)) then + distribute_quantifiers (incr_boundvars ~1 t1) + else + t0 $ Abs (s, T1, distribute_quantifiers t1)) + | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) => + (case distribute_quantifiers t1 of + (t10 as @{const "op |"}) $ t11 $ t12 => + t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) + $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) + | (t10 as @{const "op -->"}) $ t11 $ t12 => + t10 $ distribute_quantifiers (Const (@{const_name All}, T0) + $ Abs (s, T1, t11)) + $ distribute_quantifiers (t0 $ Abs (s, T1, t12)) + | (t10 as @{const Not}) $ t11 => + t10 $ distribute_quantifiers (Const (@{const_name All}, T0) + $ Abs (s, T1, t11)) + | t1 => + if not (loose_bvar1 (t1, 0)) then + distribute_quantifiers (incr_boundvars ~1 t1) + else + t0 $ Abs (s, T1, distribute_quantifiers t1)) + | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2 + | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t') + | _ => t + +(** Quantifier massaging: Pushing quantifiers inward **) + +(* int -> int -> (int -> int) -> term -> term *) +fun renumber_bounds j n f t = + case t of + t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2 + | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t') + | Bound j' => + Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j') + | _ => t + +(* Maximum number of quantifiers in a cluster for which the exponential + algorithm is used. Larger clusters use a heuristic inspired by Claessen & + Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003 + paper). *) +val quantifier_cluster_threshold = 7 + +(* theory -> term -> term *) +fun push_quantifiers_inward thy = + let + (* string -> string list -> typ list -> term -> term *) + fun aux quant_s ss Ts t = + (case t of + (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) => + if s0 = quant_s then + aux s0 (s1 :: ss) (T1 :: Ts) t1 + else if quant_s = "" andalso + (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then + aux s0 [s1] [T1] t1 + else + raise SAME () + | _ => raise SAME ()) + handle SAME () => + case t of + t1 $ t2 => + if quant_s = "" then + aux "" [] [] t1 $ aux "" [] [] t2 + else + let + val typical_card = 4 + (* ('a -> ''b list) -> 'a list -> ''b list *) + fun big_union proj ps = + fold (fold (insert (op =)) o proj) ps [] + val (ts, connective) = strip_any_connective t + val T_costs = + map (bounded_card_of_type 65536 typical_card []) Ts + val t_costs = map size_of_term ts + val num_Ts = length Ts + (* int -> int *) + val flip = curry (op -) (num_Ts - 1) + val t_boundss = map (map flip o loose_bnos) ts + (* (int list * int) list -> int list + -> (int list * int) list *) + fun merge costly_boundss [] = costly_boundss + | merge costly_boundss (j :: js) = + let + val (yeas, nays) = + List.partition (fn (bounds, _) => + member (op =) bounds j) + costly_boundss + val yeas_bounds = big_union fst yeas + val yeas_cost = Integer.sum (map snd yeas) + * nth T_costs j + in merge ((yeas_bounds, yeas_cost) :: nays) js end + (* (int list * int) list -> int list -> int *) + val cost = Integer.sum o map snd oo merge + (* (int list * int) list -> int list -> int list *) + fun heuristically_best_permutation _ [] = [] + | heuristically_best_permutation costly_boundss js = + let + val (costly_boundss, (j, js)) = + js |> map (`(merge costly_boundss o single)) + |> sort (int_ord + o pairself (Integer.sum o map snd o fst)) + |> split_list |>> hd ||> pairf hd tl + in + j :: heuristically_best_permutation costly_boundss js + end + val js = + if length Ts <= quantifier_cluster_threshold then + all_permutations (index_seq 0 num_Ts) + |> map (`(cost (t_boundss ~~ t_costs))) + |> sort (int_ord o pairself fst) |> hd |> snd + else + heuristically_best_permutation (t_boundss ~~ t_costs) + (index_seq 0 num_Ts) + val back_js = map (fn j => find_index (curry (op =) j) js) + (index_seq 0 num_Ts) + val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip)) + ts + (* (term * int list) list -> term *) + fun mk_connection [] = + raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\ + \mk_connection", "") + | mk_connection ts_cum_bounds = + ts_cum_bounds |> map fst + |> foldr1 (fn (t1, t2) => connective $ t1 $ t2) + (* (term * int list) list -> int list -> term *) + fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection + | build ts_cum_bounds (j :: js) = + let + val (yeas, nays) = + List.partition (fn (_, bounds) => + member (op =) bounds j) + ts_cum_bounds + ||> map (apfst (incr_boundvars ~1)) + in + if null yeas then + build nays js + else + let val T = nth Ts (flip j) in + build ((Const (quant_s, (T --> bool_T) --> bool_T) + $ Abs (nth ss (flip j), T, + mk_connection yeas), + big_union snd yeas) :: nays) js + end + end + in build (ts ~~ t_boundss) js end + | Abs (s, T, t') => Abs (s, T, aux "" [] [] t') + | _ => t + in aux "" [] [] end + +(** Preprocessor entry point **) + +(* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *) +fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes, + skolemize, uncurry, ...}) t = + let + val skolem_depth = if skolemize then 4 else ~1 + val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)), + core_t) = t |> unfold_defs_in_term hol_ctxt + |> Refute.close_form + |> skolemize_term_and_more hol_ctxt skolem_depth + |> specialize_consts_in_term hol_ctxt 0 + |> `(axioms_for_term hol_ctxt) + val binarize = + case binary_ints of + SOME false => false + | _ => + forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso + (binary_ints = SOME true orelse + exists should_use_binary_ints (core_t :: def_ts @ nondef_ts)) + val box = exists (not_equal (SOME false) o snd) boxes + val table = + Termtab.empty |> uncurry + ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts) + (* bool -> bool -> term -> term *) + fun do_rest def core = + binarize ? binarize_nat_and_int_in_term + #> uncurry ? uncurry_term table + #> box ? box_fun_and_pair_in_term hol_ctxt def + #> destroy_constrs ? (pull_out_universal_constrs thy def + #> pull_out_existential_constrs thy + #> destroy_pulled_out_constrs hol_ctxt def) + #> curry_assms + #> destroy_universal_equalities + #> destroy_existential_equalities thy + #> simplify_constrs_and_sels thy + #> distribute_quantifiers + #> push_quantifiers_inward thy + #> not core ? Refute.close_form + #> Term.map_abs_vars shortest_name + in + (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts), + (got_all_mono_user_axioms, no_poly_user_axioms)), + do_rest false true core_t) + end + +end; diff -r 5e492a862b34 -r 96136eb6218f src/HOL/Tools/Nitpick/nitpick_scope.ML --- 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 \}, @@ -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;