src/HOL/Tools/Nitpick/nitpick_rep.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (24 months ago)
changeset 66695 91500c024c7f
parent 59058 a78612c67ec0
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned;
blanchet@33982
     1
(*  Title:      HOL/Tools/Nitpick/nitpick_rep.ML
blanchet@33192
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@34982
     3
    Copyright   2008, 2009, 2010
blanchet@33192
     4
blanchet@33192
     5
Kodkod representations of Nitpick terms.
blanchet@33192
     6
*)
blanchet@33192
     7
blanchet@33192
     8
signature NITPICK_REP =
blanchet@33192
     9
sig
blanchet@33232
    10
  type polarity = Nitpick_Util.polarity
blanchet@33232
    11
  type scope = Nitpick_Scope.scope
blanchet@33192
    12
blanchet@33192
    13
  datatype rep =
blanchet@33192
    14
    Any |
blanchet@33192
    15
    Formula of polarity |
blanchet@33192
    16
    Atom of int * int |
blanchet@33192
    17
    Struct of rep list |
blanchet@33192
    18
    Vect of int * rep |
blanchet@33192
    19
    Func of rep * rep |
blanchet@33192
    20
    Opt of rep
blanchet@33192
    21
blanchet@33192
    22
  exception REP of string * rep list
blanchet@33192
    23
blanchet@33192
    24
  val string_for_polarity : polarity -> string
blanchet@33192
    25
  val string_for_rep : rep -> string
blanchet@33192
    26
  val is_Func : rep -> bool
blanchet@33192
    27
  val is_Opt : rep -> bool
blanchet@33192
    28
  val is_opt_rep : rep -> bool
blanchet@33192
    29
  val flip_rep_polarity : rep -> rep
blanchet@33192
    30
  val card_of_rep : rep -> int
blanchet@33192
    31
  val arity_of_rep : rep -> int
blanchet@33192
    32
  val min_univ_card_of_rep : rep -> int
blanchet@33192
    33
  val is_one_rep : rep -> bool
blanchet@33192
    34
  val is_lone_rep : rep -> bool
blanchet@33192
    35
  val dest_Func : rep -> rep * rep
blanchet@36128
    36
  val lazy_range_rep : int Typtab.table -> typ -> (unit -> int) -> rep -> rep
blanchet@33192
    37
  val binder_reps : rep -> rep list
blanchet@33192
    38
  val body_rep : rep -> rep
blanchet@33192
    39
  val one_rep : int Typtab.table -> typ -> rep -> rep
blanchet@33192
    40
  val optable_rep : int Typtab.table -> typ -> rep -> rep
blanchet@33192
    41
  val opt_rep : int Typtab.table -> typ -> rep -> rep
blanchet@33192
    42
  val unopt_rep : rep -> rep
blanchet@33192
    43
  val min_rep : rep -> rep -> rep
blanchet@33192
    44
  val min_reps : rep list -> rep list -> rep list
blanchet@33192
    45
  val card_of_domain_from_rep : int -> rep -> int
blanchet@33192
    46
  val rep_to_binary_rel_rep : int Typtab.table -> typ -> rep -> rep
blanchet@33192
    47
  val best_one_rep_for_type : scope -> typ -> rep
blanchet@33192
    48
  val best_opt_set_rep_for_type : scope -> typ -> rep
blanchet@33192
    49
  val best_non_opt_set_rep_for_type : scope -> typ -> rep
blanchet@33192
    50
  val best_set_rep_for_type : scope -> typ -> rep
blanchet@33192
    51
  val best_non_opt_symmetric_reps_for_fun_type : scope -> typ -> rep * rep
blanchet@33192
    52
  val atom_schema_of_rep : rep -> (int * int) list
blanchet@33192
    53
  val atom_schema_of_reps : rep list -> (int * int) list
blanchet@33192
    54
  val type_schema_of_rep : typ -> rep -> typ list
blanchet@33192
    55
  val type_schema_of_reps : typ list -> rep list -> typ list
blanchet@33192
    56
  val all_combinations_for_rep : rep -> int list list
blanchet@33192
    57
  val all_combinations_for_reps : rep list -> int list list
blanchet@33192
    58
end;
blanchet@33192
    59
blanchet@33232
    60
structure Nitpick_Rep : NITPICK_REP =
blanchet@33192
    61
struct
blanchet@33192
    62
blanchet@33232
    63
open Nitpick_Util
blanchet@33232
    64
open Nitpick_HOL
blanchet@33232
    65
open Nitpick_Scope
blanchet@33192
    66
blanchet@33192
    67
datatype rep =
blanchet@33192
    68
  Any |
blanchet@33192
    69
  Formula of polarity |
blanchet@33192
    70
  Atom of int * int |
blanchet@33192
    71
  Struct of rep list |
blanchet@33192
    72
  Vect of int * rep |
blanchet@33192
    73
  Func of rep * rep |
blanchet@33192
    74
  Opt of rep
blanchet@33192
    75
blanchet@33192
    76
exception REP of string * rep list
blanchet@33192
    77
blanchet@33192
    78
fun string_for_polarity Pos = "+"
blanchet@33192
    79
  | string_for_polarity Neg = "-"
blanchet@33192
    80
  | string_for_polarity Neut = "="
blanchet@33192
    81
blanchet@33192
    82
fun atomic_string_for_rep rep =
blanchet@33192
    83
  let val s = string_for_rep rep in
blanchet@33192
    84
    if String.isPrefix "[" s orelse not (is_substring_of " " s) then s
blanchet@33192
    85
    else "(" ^ s ^ ")"
blanchet@33192
    86
  end
blanchet@33192
    87
and string_for_rep Any = "X"
blanchet@33192
    88
  | string_for_rep (Formula polar) = "F" ^ string_for_polarity polar
blanchet@33192
    89
  | string_for_rep (Atom (k, j0)) =
blanchet@33192
    90
    "A" ^ string_of_int k ^ (if j0 = 0 then "" else "@" ^ string_of_int j0)
blanchet@33192
    91
  | string_for_rep (Struct rs) = "[" ^ commas (map string_for_rep rs) ^ "]"
blanchet@33192
    92
  | string_for_rep (Vect (k, R)) =
blanchet@33192
    93
    string_of_int k ^ " x " ^ atomic_string_for_rep R
blanchet@33192
    94
  | string_for_rep (Func (R1, R2)) =
blanchet@33192
    95
    atomic_string_for_rep R1 ^ " => " ^ string_for_rep R2
blanchet@33192
    96
  | string_for_rep (Opt R) = atomic_string_for_rep R ^ "?"
blanchet@33192
    97
blanchet@33192
    98
fun is_Func (Func _) = true
blanchet@33192
    99
  | is_Func _ = false
blanchet@55889
   100
blanchet@33192
   101
fun is_Opt (Opt _) = true
blanchet@33192
   102
  | is_Opt _ = false
blanchet@55889
   103
blanchet@33192
   104
fun is_opt_rep (Func (_, R2)) = is_opt_rep R2
blanchet@33192
   105
  | is_opt_rep (Opt _) = true
blanchet@33192
   106
  | is_opt_rep _ = false
blanchet@33192
   107
blanchet@33232
   108
fun card_of_rep Any = raise REP ("Nitpick_Rep.card_of_rep", [Any])
blanchet@33192
   109
  | card_of_rep (Formula _) = 2
blanchet@33192
   110
  | card_of_rep (Atom (k, _)) = k
blanchet@33192
   111
  | card_of_rep (Struct rs) = Integer.prod (map card_of_rep rs)
blanchet@33192
   112
  | card_of_rep (Vect (k, R)) = reasonable_power (card_of_rep R) k
blanchet@33192
   113
  | card_of_rep (Func (R1, R2)) =
blanchet@33192
   114
    reasonable_power (card_of_rep R2) (card_of_rep R1)
blanchet@33192
   115
  | card_of_rep (Opt R) = card_of_rep R
blanchet@55889
   116
blanchet@33232
   117
fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any])
blanchet@33192
   118
  | arity_of_rep (Formula _) = 0
blanchet@33192
   119
  | arity_of_rep (Atom _) = 1
blanchet@33192
   120
  | arity_of_rep (Struct Rs) = Integer.sum (map arity_of_rep Rs)
blanchet@33192
   121
  | arity_of_rep (Vect (k, R)) = k * arity_of_rep R
blanchet@33192
   122
  | arity_of_rep (Func (R1, R2)) = arity_of_rep R1 + arity_of_rep R2
blanchet@33192
   123
  | arity_of_rep (Opt R) = arity_of_rep R
blanchet@55889
   124
blanchet@33192
   125
fun min_univ_card_of_rep Any =
blanchet@33232
   126
    raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any])
blanchet@33192
   127
  | min_univ_card_of_rep (Formula _) = 0
blanchet@33192
   128
  | min_univ_card_of_rep (Atom (k, j0)) = k + j0 + 1
blanchet@33192
   129
  | min_univ_card_of_rep (Struct Rs) =
blanchet@33192
   130
    fold Integer.max (map min_univ_card_of_rep Rs) 0
blanchet@33192
   131
  | min_univ_card_of_rep (Vect (_, R)) = min_univ_card_of_rep R
blanchet@33192
   132
  | min_univ_card_of_rep (Func (R1, R2)) =
blanchet@33192
   133
    Int.max (min_univ_card_of_rep R1, min_univ_card_of_rep R2)
blanchet@33192
   134
  | min_univ_card_of_rep (Opt R) = min_univ_card_of_rep R
blanchet@33192
   135
blanchet@38190
   136
fun is_one_rep (Atom _) = true
blanchet@33192
   137
  | is_one_rep (Struct _) = true
blanchet@33192
   138
  | is_one_rep (Vect _) = true
blanchet@33192
   139
  | is_one_rep _ = false
blanchet@55889
   140
blanchet@33192
   141
fun is_lone_rep (Opt R) = is_one_rep R
blanchet@33192
   142
  | is_lone_rep R = is_one_rep R
blanchet@33192
   143
blanchet@33192
   144
fun dest_Func (Func z) = z
blanchet@33232
   145
  | dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R])
blanchet@55889
   146
blanchet@38190
   147
fun lazy_range_rep _ _ _ (Vect (_, R)) = R
blanchet@36128
   148
  | lazy_range_rep _ _ _ (Func (_, R2)) = R2
blanchet@36128
   149
  | lazy_range_rep ofs T ran_card (Opt R) =
blanchet@36128
   150
    Opt (lazy_range_rep ofs T ran_card R)
blanchet@36128
   151
  | lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) =
blanchet@33192
   152
    Atom (1, offset_of_type ofs T2)
blanchet@36128
   153
  | lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) =
blanchet@33192
   154
    Atom (ran_card (), offset_of_type ofs T2)
blanchet@36128
   155
  | lazy_range_rep _ _ _ R = raise REP ("Nitpick_Rep.lazy_range_rep", [R])
blanchet@33192
   156
blanchet@33192
   157
fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2
blanchet@35280
   158
  | binder_reps _ = []
blanchet@55889
   159
blanchet@33192
   160
fun body_rep (Func (_, R2)) = body_rep R2
blanchet@33192
   161
  | body_rep R = R
blanchet@33192
   162
blanchet@33192
   163
fun flip_rep_polarity (Formula polar) = Formula (flip_polarity polar)
blanchet@33192
   164
  | flip_rep_polarity (Func (R1, R2)) = Func (R1, flip_rep_polarity R2)
blanchet@33192
   165
  | flip_rep_polarity R = R
blanchet@33192
   166
blanchet@33232
   167
fun one_rep _ _ Any = raise REP ("Nitpick_Rep.one_rep", [Any])
blanchet@33192
   168
  | one_rep _ _ (Atom x) = Atom x
blanchet@33192
   169
  | one_rep _ _ (Struct Rs) = Struct Rs
blanchet@33192
   170
  | one_rep _ _ (Vect z) = Vect z
blanchet@33192
   171
  | one_rep ofs T (Opt R) = one_rep ofs T R
blanchet@33192
   172
  | one_rep ofs T R = Atom (card_of_rep R, offset_of_type ofs T)
blanchet@55889
   173
blanchet@35665
   174
fun optable_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
blanchet@33192
   175
    Func (R1, optable_rep ofs T2 R2)
blanchet@46083
   176
  | optable_rep ofs (Type (@{type_name set}, [T'])) R =
blanchet@46083
   177
    optable_rep ofs (T' --> bool_T) R
blanchet@33192
   178
  | optable_rep ofs T R = one_rep ofs T R
blanchet@55889
   179
blanchet@35665
   180
fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
blanchet@33192
   181
    Func (R1, opt_rep ofs T2 R2)
blanchet@46083
   182
  | opt_rep ofs (Type (@{type_name set}, [T'])) R =
blanchet@46083
   183
    opt_rep ofs (T' --> bool_T) R
blanchet@33192
   184
  | opt_rep ofs T R = Opt (optable_rep ofs T R)
blanchet@55889
   185
blanchet@33192
   186
fun unopt_rep (Func (R1, R2)) = Func (R1, unopt_rep R2)
blanchet@33192
   187
  | unopt_rep (Opt R) = R
blanchet@33192
   188
  | unopt_rep R = R
blanchet@33192
   189
blanchet@33192
   190
fun min_polarity polar1 polar2 =
blanchet@33192
   191
  if polar1 = polar2 then
blanchet@33192
   192
    polar1
blanchet@33192
   193
  else if polar1 = Neut then
blanchet@33192
   194
    polar2
blanchet@33192
   195
  else if polar2 = Neut then
blanchet@33192
   196
    polar1
blanchet@33192
   197
  else
blanchet@33232
   198
    raise ARG ("Nitpick_Rep.min_polarity",
blanchet@33192
   199
               commas (map (quote o string_for_polarity) [polar1, polar2]))
blanchet@33192
   200
blanchet@33192
   201
(* It's important that Func is before Vect, because if the range is Opt we
blanchet@33192
   202
   could lose information by converting a Func to a Vect. *)
blanchet@33192
   203
fun min_rep (Opt R1) (Opt R2) = Opt (min_rep R1 R2)
blanchet@33192
   204
  | min_rep (Opt R) _ = Opt R
blanchet@33192
   205
  | min_rep _ (Opt R) = Opt R
blanchet@33192
   206
  | min_rep (Formula polar1) (Formula polar2) =
blanchet@33192
   207
    Formula (min_polarity polar1 polar2)
blanchet@33192
   208
  | min_rep (Formula polar) _ = Formula polar
blanchet@33192
   209
  | min_rep _ (Formula polar) = Formula polar
blanchet@33192
   210
  | min_rep (Atom x) _ = Atom x
blanchet@33192
   211
  | min_rep _ (Atom x) = Atom x
blanchet@33192
   212
  | min_rep (Struct Rs1) (Struct Rs2) = Struct (min_reps Rs1 Rs2)
blanchet@33192
   213
  | min_rep (Struct Rs) _ = Struct Rs
blanchet@33192
   214
  | min_rep _ (Struct Rs) = Struct Rs
blanchet@33192
   215
  | min_rep (R1 as Func (R11, R12)) (R2 as Func (R21, R22)) =
wenzelm@59058
   216
    (case apply2 is_opt_rep (R12, R22) of
blanchet@33192
   217
       (true, false) => R1
blanchet@33192
   218
     | (false, true) => R2
blanchet@33192
   219
     | _ => if R11 = R21 then Func (R11, min_rep R12 R22)
blanchet@33192
   220
            else if min_rep R11 R21 = R11 then R1
blanchet@33192
   221
            else R2)
blanchet@33192
   222
  | min_rep (Func z) _ = Func z
blanchet@33192
   223
  | min_rep _ (Func z) = Func z
blanchet@33192
   224
  | min_rep (Vect (k1, R1)) (Vect (k2, R2)) =
blanchet@33192
   225
    if k1 < k2 then Vect (k1, R1)
blanchet@33192
   226
    else if k1 > k2 then Vect (k2, R2)
blanchet@33192
   227
    else Vect (k1, min_rep R1 R2)
blanchet@33232
   228
  | min_rep R1 R2 = raise REP ("Nitpick_Rep.min_rep", [R1, R2])
blanchet@33192
   229
and min_reps [] _ = []
blanchet@33192
   230
  | min_reps _ [] = []
blanchet@33192
   231
  | min_reps (R1 :: Rs1) (R2 :: Rs2) =
blanchet@33192
   232
    if R1 = R2 then R1 :: min_reps Rs1 Rs2
blanchet@33192
   233
    else if min_rep R1 R2 = R1 then R1 :: Rs1
blanchet@33192
   234
    else R2 :: Rs2
blanchet@33192
   235
blanchet@33192
   236
fun card_of_domain_from_rep ran_card R =
blanchet@33192
   237
  case R of
blanchet@38190
   238
    Atom (k, _) => exact_log ran_card k
blanchet@33192
   239
  | Vect (k, _) => k
blanchet@33192
   240
  | Func (R1, _) => card_of_rep R1
blanchet@33192
   241
  | Opt R => card_of_domain_from_rep ran_card R
blanchet@33232
   242
  | _ => raise REP ("Nitpick_Rep.card_of_domain_from_rep", [R])
blanchet@33192
   243
blanchet@33192
   244
fun rep_to_binary_rel_rep ofs T R =
blanchet@33192
   245
  let
blanchet@33192
   246
    val k = exact_root 2 (card_of_domain_from_rep 2 R)
blanchet@46085
   247
    val j0 =
blanchet@46085
   248
      offset_of_type ofs (fst (HOLogic.dest_prodT (pseudo_domain_type T)))
blanchet@33192
   249
  in Func (Struct [Atom (k, j0), Atom (k, j0)], Formula Neut) end
blanchet@33192
   250
blanchet@33192
   251
fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)
blanchet@35665
   252
                          (Type (@{type_name fun}, [T1, T2])) =
blanchet@38190
   253
    Vect (card_of_type card_assigns T1, (best_one_rep_for_type scope T2))
blanchet@46083
   254
  | best_one_rep_for_type scope (Type (@{type_name set}, [T'])) =
blanchet@46083
   255
    best_one_rep_for_type scope (T' --> bool_T)
blanchet@38190
   256
  | best_one_rep_for_type scope (Type (@{type_name prod}, Ts)) =
blanchet@38190
   257
    Struct (map (best_one_rep_for_type scope) Ts)
blanchet@39345
   258
  | best_one_rep_for_type {card_assigns, ofs, ...} T =
blanchet@38190
   259
    Atom (card_of_type card_assigns T, offset_of_type ofs T)
blanchet@33192
   260
blanchet@35665
   261
fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
blanchet@33192
   262
    Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2)
blanchet@46083
   263
  | best_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) =
blanchet@46083
   264
    best_opt_set_rep_for_type scope (T' --> bool_T)
blanchet@33192
   265
  | best_opt_set_rep_for_type (scope as {ofs, ...}) T =
blanchet@33192
   266
    opt_rep ofs T (best_one_rep_for_type scope T)
blanchet@55889
   267
blanchet@39345
   268
fun best_non_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
blanchet@33192
   269
    (case (best_one_rep_for_type scope T1,
blanchet@33192
   270
           best_non_opt_set_rep_for_type scope T2) of
blanchet@38190
   271
       (R1, Atom (2, _)) => Func (R1, Formula Neut)
blanchet@33192
   272
     | z => Func z)
blanchet@46083
   273
  | best_non_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) =
blanchet@46083
   274
    best_non_opt_set_rep_for_type scope (T' --> bool_T)
blanchet@33192
   275
  | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
blanchet@55889
   276
blanchet@55890
   277
fun best_set_rep_for_type (scope as {data_types, ...}) T =
blanchet@55890
   278
  (if is_exact_type data_types true T then best_non_opt_set_rep_for_type
blanchet@33192
   279
   else best_opt_set_rep_for_type) scope T
blanchet@55889
   280
blanchet@33192
   281
fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
blanchet@35665
   282
                                           (Type (@{type_name fun}, [T1, T2])) =
blanchet@33192
   283
    (optable_rep ofs T1 (best_one_rep_for_type scope T1),
blanchet@33192
   284
     optable_rep ofs T2 (best_one_rep_for_type scope T2))
blanchet@33192
   285
  | best_non_opt_symmetric_reps_for_fun_type _ T =
blanchet@33232
   286
    raise TYPE ("Nitpick_Rep.best_non_opt_symmetric_reps_for_fun_type", [T], [])
blanchet@33192
   287
blanchet@33232
   288
fun atom_schema_of_rep Any = raise REP ("Nitpick_Rep.atom_schema_of_rep", [Any])
blanchet@33192
   289
  | atom_schema_of_rep (Formula _) = []
blanchet@33192
   290
  | atom_schema_of_rep (Atom x) = [x]
blanchet@33192
   291
  | atom_schema_of_rep (Struct Rs) = atom_schema_of_reps Rs
blanchet@33192
   292
  | atom_schema_of_rep (Vect (k, R)) = replicate_list k (atom_schema_of_rep R)
blanchet@33192
   293
  | atom_schema_of_rep (Func (R1, R2)) =
blanchet@33192
   294
    atom_schema_of_rep R1 @ atom_schema_of_rep R2
blanchet@33192
   295
  | atom_schema_of_rep (Opt R) = atom_schema_of_rep R
blanchet@33192
   296
and atom_schema_of_reps Rs = maps atom_schema_of_rep Rs
blanchet@33192
   297
blanchet@33192
   298
fun type_schema_of_rep _ (Formula _) = []
blanchet@33192
   299
  | type_schema_of_rep T (Atom _) = [T]
blanchet@38190
   300
  | type_schema_of_rep (Type (@{type_name prod}, [T1, T2])) (Struct [R1, R2]) =
blanchet@33192
   301
    type_schema_of_reps [T1, T2] [R1, R2]
blanchet@35665
   302
  | type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) =
blanchet@33192
   303
    replicate_list k (type_schema_of_rep T2 R)
blanchet@35665
   304
  | type_schema_of_rep (Type (@{type_name fun}, [T1, T2])) (Func (R1, R2)) =
blanchet@33192
   305
    type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2
blanchet@46083
   306
  | type_schema_of_rep (Type (@{type_name set}, [T'])) R =
blanchet@46083
   307
    type_schema_of_rep (T' --> bool_T) R
blanchet@33192
   308
  | type_schema_of_rep T (Opt R) = type_schema_of_rep T R
blanchet@35280
   309
  | type_schema_of_rep _ R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
blanchet@33192
   310
and type_schema_of_reps Ts Rs = flat (map2 type_schema_of_rep Ts Rs)
blanchet@33192
   311
blanchet@33192
   312
val all_combinations_for_rep = all_combinations o atom_schema_of_rep
blanchet@33192
   313
val all_combinations_for_reps = all_combinations o atom_schema_of_reps
blanchet@33192
   314
blanchet@33192
   315
end;