src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35718 eee1a5e0d334
parent 35712 77aa29bf14ee
child 35807 e4d1b5cbd429
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 11 16:56:22 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 11 17:48:07 2010 +0100
     1.3 @@ -72,6 +72,7 @@
     1.4  val base_mixfix = "_\<^bsub>base\<^esub>"
     1.5  val step_mixfix = "_\<^bsub>step\<^esub>"
     1.6  val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
     1.7 +val arg_var_prefix = "x"
     1.8  val cyclic_co_val_name = "\<omega>"
     1.9  val cyclic_const_prefix = "\<xi>"
    1.10  val cyclic_type_name = nitpick_prefix ^ cyclic_const_prefix
    1.11 @@ -80,6 +81,31 @@
    1.12  
    1.13  type atom_pool = ((string * int) * int list) list
    1.14  
    1.15 +(* Proof.context -> ((string * string) * (string * string)) * Proof.context *)
    1.16 +fun add_wacky_syntax ctxt =
    1.17 +  let
    1.18 +    (* term -> string *)
    1.19 +    val name_of = fst o dest_Const
    1.20 +    val thy = ProofContext.theory_of ctxt |> Context.reject_draft
    1.21 +    val (maybe_t, thy) =
    1.22 +      Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
    1.23 +                          Mixfix (maybe_mixfix, [1000], 1000)) thy
    1.24 +    val (abs_t, thy) =
    1.25 +      Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
    1.26 +                          Mixfix (abs_mixfix, [40], 40)) thy
    1.27 +    val (base_t, thy) =
    1.28 +      Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
    1.29 +                          Mixfix (base_mixfix, [1000], 1000)) thy
    1.30 +    val (step_t, thy) =
    1.31 +      Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
    1.32 +                          Mixfix (step_mixfix, [1000], 1000)) thy
    1.33 +  in
    1.34 +    (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
    1.35 +     ProofContext.transfer_syntax thy ctxt)
    1.36 +  end
    1.37 +
    1.38 +(** Term reconstruction **)
    1.39 +
    1.40  (* atom_pool Unsynchronized.ref -> string -> int -> int -> string *)
    1.41  fun nth_atom_suffix pool s j k =
    1.42    (case AList.lookup (op =) (!pool) (s, k) of
    1.43 @@ -646,6 +672,211 @@
    1.44      oooo term_for_rep true []
    1.45    end
    1.46  
    1.47 +(** Constant postprocessing **)
    1.48 +
    1.49 +(* int -> typ -> typ list *)
    1.50 +fun dest_n_tuple_type 1 T = [T]
    1.51 +  | dest_n_tuple_type n (Type (_, [T1, T2])) =
    1.52 +    T1 :: dest_n_tuple_type (n - 1) T2
    1.53 +  | dest_n_tuple_type _ T =
    1.54 +    raise TYPE ("Nitpick_Model.dest_n_tuple_type", [T], [])
    1.55 +
    1.56 +(* theory -> const_table -> styp -> int list *)
    1.57 +fun const_format thy def_table (x as (s, T)) =
    1.58 +  if String.isPrefix unrolled_prefix s then
    1.59 +    const_format thy def_table (original_name s, range_type T)
    1.60 +  else if String.isPrefix skolem_prefix s then
    1.61 +    let
    1.62 +      val k = unprefix skolem_prefix s
    1.63 +              |> strip_first_name_sep |> fst |> space_explode "@"
    1.64 +              |> hd |> Int.fromString |> the
    1.65 +    in [k, num_binder_types T - k] end
    1.66 +  else if original_name s <> s then
    1.67 +    [num_binder_types T]
    1.68 +  else case def_of_const thy def_table x of
    1.69 +    SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
    1.70 +                 let val k = length (strip_abs_vars t') in
    1.71 +                   [k, num_binder_types T - k]
    1.72 +                 end
    1.73 +               else
    1.74 +                 [num_binder_types T]
    1.75 +  | NONE => [num_binder_types T]
    1.76 +(* int list -> int list -> int list *)
    1.77 +fun intersect_formats _ [] = []
    1.78 +  | intersect_formats [] _ = []
    1.79 +  | intersect_formats ks1 ks2 =
    1.80 +    let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in
    1.81 +      intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else []))
    1.82 +                        (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @
    1.83 +      [Int.min (k1, k2)]
    1.84 +    end
    1.85 +
    1.86 +(* theory -> const_table -> (term option * int list) list -> term -> int list *)
    1.87 +fun lookup_format thy def_table formats t =
    1.88 +  case AList.lookup (fn (SOME x, SOME y) =>
    1.89 +                        (term_match thy) (x, y) | _ => false)
    1.90 +                    formats (SOME t) of
    1.91 +    SOME format => format
    1.92 +  | NONE => let val format = the (AList.lookup (op =) formats NONE) in
    1.93 +              case t of
    1.94 +                Const x => intersect_formats format
    1.95 +                                             (const_format thy def_table x)
    1.96 +              | _ => format
    1.97 +            end
    1.98 +
    1.99 +(* int list -> int list -> typ -> typ *)
   1.100 +fun format_type default_format format T =
   1.101 +  let
   1.102 +    val T = uniterize_unarize_unbox_etc_type T
   1.103 +    val format = format |> filter (curry (op <) 0)
   1.104 +  in
   1.105 +    if forall (curry (op =) 1) format then
   1.106 +      T
   1.107 +    else
   1.108 +      let
   1.109 +        val (binder_Ts, body_T) = strip_type T
   1.110 +        val batched =
   1.111 +          binder_Ts
   1.112 +          |> map (format_type default_format default_format)
   1.113 +          |> rev |> chunk_list_unevenly (rev format)
   1.114 +          |> map (HOLogic.mk_tupleT o rev)
   1.115 +      in List.foldl (op -->) body_T batched end
   1.116 +  end
   1.117 +(* theory -> const_table -> (term option * int list) list -> term -> typ *)
   1.118 +fun format_term_type thy def_table formats t =
   1.119 +  format_type (the (AList.lookup (op =) formats NONE))
   1.120 +              (lookup_format thy def_table formats t) (fastype_of t)
   1.121 +
   1.122 +(* int list -> int -> int list -> int list *)
   1.123 +fun repair_special_format js m format =
   1.124 +  m - 1 downto 0 |> chunk_list_unevenly (rev format)
   1.125 +                 |> map (rev o filter_out (member (op =) js))
   1.126 +                 |> filter_out null |> map length |> rev
   1.127 +
   1.128 +(* hol_context -> string * string -> (term option * int list) list
   1.129 +   -> styp -> term * typ *)
   1.130 +fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
   1.131 +                         : hol_context) (base_name, step_name) formats =
   1.132 +  let
   1.133 +    val default_format = the (AList.lookup (op =) formats NONE)
   1.134 +    (* styp -> term * typ *)
   1.135 +    fun do_const (x as (s, T)) =
   1.136 +      (if String.isPrefix special_prefix s then
   1.137 +         let
   1.138 +           (* term -> term *)
   1.139 +           val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
   1.140 +           val (x' as (_, T'), js, ts) =
   1.141 +             AList.find (op =) (!special_funs) (s, unarize_unbox_etc_type T)
   1.142 +             |> the_single
   1.143 +           val max_j = List.last js
   1.144 +           val Ts = List.take (binder_types T', max_j + 1)
   1.145 +           val missing_js = filter_out (member (op =) js) (0 upto max_j)
   1.146 +           val missing_Ts = filter_indices missing_js Ts
   1.147 +           (* int -> indexname *)
   1.148 +           fun nth_missing_var n =
   1.149 +             ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
   1.150 +           val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
   1.151 +           val vars = special_bounds ts @ missing_vars
   1.152 +           val ts' =
   1.153 +             map (fn j =>
   1.154 +                     case AList.lookup (op =) (js ~~ ts) j of
   1.155 +                       SOME t => do_term t
   1.156 +                     | NONE =>
   1.157 +                       Var (nth missing_vars
   1.158 +                                (find_index (curry (op =) j) missing_js)))
   1.159 +                 (0 upto max_j)
   1.160 +           val t = do_const x' |> fst
   1.161 +           val format =
   1.162 +             case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
   1.163 +                                 | _ => false) formats (SOME t) of
   1.164 +               SOME format =>
   1.165 +               repair_special_format js (num_binder_types T') format
   1.166 +             | NONE =>
   1.167 +               const_format thy def_table x'
   1.168 +               |> repair_special_format js (num_binder_types T')
   1.169 +               |> intersect_formats default_format
   1.170 +         in
   1.171 +           (list_comb (t, ts') |> fold_rev abs_var vars,
   1.172 +            format_type default_format format T)
   1.173 +         end
   1.174 +       else if String.isPrefix uncurry_prefix s then
   1.175 +         let
   1.176 +           val (ss, s') = unprefix uncurry_prefix s
   1.177 +                          |> strip_first_name_sep |>> space_explode "@"
   1.178 +         in
   1.179 +           if String.isPrefix step_prefix s' then
   1.180 +             do_const (s', T)
   1.181 +           else
   1.182 +             let
   1.183 +               val k = the (Int.fromString (hd ss))
   1.184 +               val j = the (Int.fromString (List.last ss))
   1.185 +               val (before_Ts, (tuple_T, rest_T)) =
   1.186 +                 strip_n_binders j T ||> (strip_n_binders 1 #>> hd)
   1.187 +               val T' = before_Ts ---> dest_n_tuple_type k tuple_T ---> rest_T
   1.188 +             in do_const (s', T') end
   1.189 +         end
   1.190 +       else if String.isPrefix unrolled_prefix s then
   1.191 +         let val t = Const (original_name s, range_type T) in
   1.192 +           (lambda (Free (iter_var_prefix, nat_T)) t,
   1.193 +            format_type default_format
   1.194 +                        (lookup_format thy def_table formats t) T)
   1.195 +         end
   1.196 +       else if String.isPrefix base_prefix s then
   1.197 +         (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
   1.198 +          format_type default_format default_format T)
   1.199 +       else if String.isPrefix step_prefix s then
   1.200 +         (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
   1.201 +          format_type default_format default_format T)
   1.202 +       else if String.isPrefix quot_normal_prefix s then
   1.203 +         let val t = Const (nitpick_prefix ^ "normalize quotient type", T) in
   1.204 +           (t, format_term_type thy def_table formats t)
   1.205 +         end
   1.206 +       else if String.isPrefix skolem_prefix s then
   1.207 +         let
   1.208 +           val ss = the (AList.lookup (op =) (!skolems) s)
   1.209 +           val (Ts, Ts') = chop (length ss) (binder_types T)
   1.210 +           val frees = map Free (ss ~~ Ts)
   1.211 +           val s' = original_name s
   1.212 +         in
   1.213 +           (fold lambda frees (Const (s', Ts' ---> T)),
   1.214 +            format_type default_format
   1.215 +                        (lookup_format thy def_table formats (Const x)) T)
   1.216 +         end
   1.217 +       else if String.isPrefix eval_prefix s then
   1.218 +         let
   1.219 +           val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
   1.220 +         in (t, format_term_type thy def_table formats t) end
   1.221 +       else if s = @{const_name undefined_fast_The} then
   1.222 +         (Const (nitpick_prefix ^ "The fallback", T),
   1.223 +          format_type default_format
   1.224 +                      (lookup_format thy def_table formats
   1.225 +                           (Const (@{const_name The}, (T --> bool_T) --> T))) T)
   1.226 +       else if s = @{const_name undefined_fast_Eps} then
   1.227 +         (Const (nitpick_prefix ^ "Eps fallback", T),
   1.228 +          format_type default_format
   1.229 +                      (lookup_format thy def_table formats
   1.230 +                           (Const (@{const_name Eps}, (T --> bool_T) --> T))) T)
   1.231 +       else
   1.232 +         let val t = Const (original_name s, T) in
   1.233 +           (t, format_term_type thy def_table formats t)
   1.234 +         end)
   1.235 +      |>> map_types uniterize_unarize_unbox_etc_type
   1.236 +      |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
   1.237 +  in do_const end
   1.238 +
   1.239 +(* styp -> string *)
   1.240 +fun assign_operator_for_const (s, T) =
   1.241 +  if String.isPrefix ubfp_prefix s then
   1.242 +    if is_fun_type T then "\<subseteq>" else "\<le>"
   1.243 +  else if String.isPrefix lbfp_prefix s then
   1.244 +    if is_fun_type T then "\<supseteq>" else "\<ge>"
   1.245 +  else if original_name s <> s then
   1.246 +    assign_operator_for_const (strip_first_name_sep s |> snd, T)
   1.247 +  else
   1.248 +    "="
   1.249 +
   1.250 +(** Model reconstruction **)
   1.251 +
   1.252  (* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
   1.253     -> nut -> term *)
   1.254  fun term_for_name pool scope sel_names rel_table bounds name =
   1.255 @@ -655,29 +886,6 @@
   1.256                          rel_table bounds T T (rep_of name)
   1.257    end
   1.258  
   1.259 -(* Proof.context -> ((string * string) * (string * string)) * Proof.context *)
   1.260 -fun add_wacky_syntax ctxt =
   1.261 -  let
   1.262 -    (* term -> string *)
   1.263 -    val name_of = fst o dest_Const
   1.264 -    val thy = ProofContext.theory_of ctxt |> Context.reject_draft
   1.265 -    val (maybe_t, thy) =
   1.266 -      Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
   1.267 -                          Mixfix (maybe_mixfix, [1000], 1000)) thy
   1.268 -    val (abs_t, thy) =
   1.269 -      Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
   1.270 -                          Mixfix (abs_mixfix, [40], 40)) thy
   1.271 -    val (base_t, thy) =
   1.272 -      Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
   1.273 -                          Mixfix (base_mixfix, [1000], 1000)) thy
   1.274 -    val (step_t, thy) =
   1.275 -      Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
   1.276 -                          Mixfix (step_mixfix, [1000], 1000)) thy
   1.277 -  in
   1.278 -    (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
   1.279 -     ProofContext.transfer_syntax thy ctxt)
   1.280 -  end
   1.281 -
   1.282  (* term -> term *)
   1.283  fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
   1.284                                     $ Abs (s, T, Const (@{const_name "op ="}, _)