src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 41791 01d722707a36
parent 41472 f6ab14e61604
child 41803 ef13e3b7cbaf
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 21 10:31:48 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 21 10:42:29 2011 +0100
     1.3 @@ -662,9 +662,9 @@
     1.4    | dest_n_tuple_type _ T =
     1.5      raise TYPE ("Nitpick_Model.dest_n_tuple_type", [T], [])
     1.6  
     1.7 -fun const_format thy def_table (x as (s, T)) =
     1.8 +fun const_format thy def_tables (x as (s, T)) =
     1.9    if String.isPrefix unrolled_prefix s then
    1.10 -    const_format thy def_table (original_name s, range_type T)
    1.11 +    const_format thy def_tables (original_name s, range_type T)
    1.12    else if String.isPrefix skolem_prefix s then
    1.13      let
    1.14        val k = unprefix skolem_prefix s
    1.15 @@ -673,7 +673,7 @@
    1.16      in [k, num_binder_types T - k] end
    1.17    else if original_name s <> s then
    1.18      [num_binder_types T]
    1.19 -  else case def_of_const thy def_table x of
    1.20 +  else case def_of_const thy def_tables x of
    1.21      SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
    1.22                   let val k = length (strip_abs_vars t') in
    1.23                     [k, num_binder_types T - k]
    1.24 @@ -690,7 +690,7 @@
    1.25        [Int.min (k1, k2)]
    1.26      end
    1.27  
    1.28 -fun lookup_format thy def_table formats t =
    1.29 +fun lookup_format thy def_tables formats t =
    1.30    case AList.lookup (fn (SOME x, SOME y) =>
    1.31                          (term_match thy) (x, y) | _ => false)
    1.32                      formats (SOME t) of
    1.33 @@ -698,7 +698,7 @@
    1.34    | NONE => let val format = the (AList.lookup (op =) formats NONE) in
    1.35                case t of
    1.36                  Const x => intersect_formats format
    1.37 -                                             (const_format thy def_table x)
    1.38 +                                             (const_format thy def_tables x)
    1.39                | _ => format
    1.40              end
    1.41  
    1.42 @@ -719,16 +719,16 @@
    1.43            |> map (HOLogic.mk_tupleT o rev)
    1.44        in List.foldl (op -->) body_T batched end
    1.45    end
    1.46 -fun format_term_type thy def_table formats t =
    1.47 +fun format_term_type thy def_tables formats t =
    1.48    format_type (the (AList.lookup (op =) formats NONE))
    1.49 -              (lookup_format thy def_table formats t) (fastype_of t)
    1.50 +              (lookup_format thy def_tables formats t) (fastype_of t)
    1.51  
    1.52  fun repair_special_format js m format =
    1.53    m - 1 downto 0 |> chunk_list_unevenly (rev format)
    1.54                   |> map (rev o filter_out (member (op =) js))
    1.55                   |> filter_out null |> map length |> rev
    1.56  
    1.57 -fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
    1.58 +fun user_friendly_const ({thy, evals, def_tables, skolems, special_funs, ...}
    1.59                           : hol_context) (base_name, step_name) formats =
    1.60    let
    1.61      val default_format = the (AList.lookup (op =) formats NONE)
    1.62 @@ -762,7 +762,7 @@
    1.63                 SOME format =>
    1.64                 repair_special_format js (num_binder_types T') format
    1.65               | NONE =>
    1.66 -               const_format thy def_table x'
    1.67 +               const_format thy def_tables x'
    1.68                 |> repair_special_format js (num_binder_types T')
    1.69                 |> intersect_formats default_format
    1.70           in
    1.71 @@ -789,7 +789,7 @@
    1.72           let val t = Const (original_name s, range_type T) in
    1.73             (lambda (Free (iter_var_prefix, nat_T)) t,
    1.74              format_type default_format
    1.75 -                        (lookup_format thy def_table formats t) T)
    1.76 +                        (lookup_format thy def_tables formats t) T)
    1.77           end
    1.78         else if String.isPrefix base_prefix s then
    1.79           (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
    1.80 @@ -799,7 +799,7 @@
    1.81            format_type default_format default_format T)
    1.82         else if String.isPrefix quot_normal_prefix s then
    1.83           let val t = Const (nitpick_prefix ^ "quotient normal form", T) in
    1.84 -           (t, format_term_type thy def_table formats t)
    1.85 +           (t, format_term_type thy def_tables formats t)
    1.86           end
    1.87         else if String.isPrefix skolem_prefix s then
    1.88           let
    1.89 @@ -810,15 +810,15 @@
    1.90           in
    1.91             (fold lambda frees (Const (s', Ts' ---> T)),
    1.92              format_type default_format
    1.93 -                        (lookup_format thy def_table formats (Const x)) T)
    1.94 +                        (lookup_format thy def_tables formats (Const x)) T)
    1.95           end
    1.96         else if String.isPrefix eval_prefix s then
    1.97           let
    1.98             val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
    1.99 -         in (t, format_term_type thy def_table formats t) end
   1.100 +         in (t, format_term_type thy def_tables formats t) end
   1.101         else
   1.102           let val t = Const (original_name s, T) in
   1.103 -           (t, format_term_type thy def_table formats t)
   1.104 +           (t, format_term_type thy def_tables formats t)
   1.105           end)
   1.106        |>> map_types uniterize_unarize_unbox_etc_type
   1.107        |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
   1.108 @@ -863,7 +863,7 @@
   1.109          ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
   1.110                        debug, whacks, binary_ints, destroy_constrs, specialize,
   1.111                        star_linear_preds, tac_timeout, evals, case_names,
   1.112 -                      def_table, nondef_table, user_nondefs, simp_table,
   1.113 +                      def_tables, nondef_table, user_nondefs, simp_table,
   1.114                        psimp_table, choice_spec_table, intro_table,
   1.115                        ground_thm_table, ersatz_table, skolems, special_funs,
   1.116                        unrolled_preds, wf_cache, constr_cache},
   1.117 @@ -880,7 +880,7 @@
   1.118         whacks = whacks, binary_ints = binary_ints,
   1.119         destroy_constrs = destroy_constrs, specialize = specialize,
   1.120         star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
   1.121 -       evals = evals, case_names = case_names, def_table = def_table,
   1.122 +       evals = evals, case_names = case_names, def_tables = def_tables,
   1.123         nondef_table = nondef_table, user_nondefs = user_nondefs,
   1.124         simp_table = simp_table, psimp_table = psimp_table,
   1.125         choice_spec_table = choice_spec_table, intro_table = intro_table,
   1.126 @@ -912,7 +912,7 @@
   1.127            case name of
   1.128              FreeName (s, T, _) =>
   1.129              let val t = Free (s, uniterize_unarize_unbox_etc_type T) in
   1.130 -              ("=", (t, format_term_type thy def_table formats t), T)
   1.131 +              ("=", (t, format_term_type thy def_tables formats t), T)
   1.132              end
   1.133            | ConstName (s, T, _) =>
   1.134              (assign_operator_for_const (s, T),