src/HOL/Tools/Nitpick/nitpick_kodkod.ML
changeset 35190 ce653cc27a94
parent 35185 9b8f351cced6
child 35220 2bcdae5f4fdb
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 14:11:41 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 20:46:50 2010 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4    val merge_bounds : Kodkod.bound list -> Kodkod.bound list
     1.5    val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
     1.6    val declarative_axioms_for_datatypes :
     1.7 -    hol_context -> int -> int Typtab.table -> kodkod_constrs
     1.8 +    hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
     1.9      -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
    1.10    val kodkod_formula_from_nut :
    1.11      int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
    1.12 @@ -742,12 +742,14 @@
    1.13  (* nut NameTable.table -> styp -> KK.rel_expr *)
    1.14  fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
    1.15  
    1.16 -(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    1.17 -   -> styp -> int -> nfa_transition list *)
    1.18 -fun nfa_transitions_for_sel hol_ctxt ({kk_project, ...} : kodkod_constrs)
    1.19 -                            rel_table (dtypes : dtype_spec list) constr_x n =
    1.20 +(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
    1.21 +   -> dtype_spec list -> styp -> int -> nfa_transition list *)
    1.22 +fun nfa_transitions_for_sel hol_ctxt binarize
    1.23 +                            ({kk_project, ...} : kodkod_constrs) rel_table
    1.24 +                            (dtypes : dtype_spec list) constr_x n =
    1.25    let
    1.26 -    val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt constr_x n
    1.27 +    val x as (_, T) =
    1.28 +      binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n
    1.29      val (r, R, arity) = const_triple rel_table x
    1.30      val type_schema = type_schema_of_rep T R
    1.31    in
    1.32 @@ -756,19 +758,21 @@
    1.33                     else SOME (kk_project r (map KK.Num [0, j]), T))
    1.34                 (index_seq 1 (arity - 1) ~~ tl type_schema)
    1.35    end
    1.36 -(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    1.37 -   -> styp -> nfa_transition list *)
    1.38 -fun nfa_transitions_for_constr hol_ctxt kk rel_table dtypes (x as (_, T)) =
    1.39 -  maps (nfa_transitions_for_sel hol_ctxt kk rel_table dtypes x)
    1.40 +(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
    1.41 +   -> dtype_spec list -> styp -> nfa_transition list *)
    1.42 +fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
    1.43 +                               (x as (_, T)) =
    1.44 +  maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
    1.45         (index_seq 0 (num_sels_for_constr_type T))
    1.46 -(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    1.47 -   -> dtype_spec -> nfa_entry option *)
    1.48 -fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
    1.49 -  | nfa_entry_for_datatype _ _ _ _ {standard = false, ...} = NONE
    1.50 -  | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
    1.51 -  | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
    1.52 -    SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
    1.53 -                     o #const) constrs)
    1.54 +(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
    1.55 +   -> dtype_spec list -> dtype_spec -> nfa_entry option *)
    1.56 +fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
    1.57 +  | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
    1.58 +  | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
    1.59 +  | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
    1.60 +                           {typ, constrs, ...} =
    1.61 +    SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table
    1.62 +                                                dtypes o #const) constrs)
    1.63  
    1.64  val empty_rel = KK.Product (KK.None, KK.None)
    1.65  
    1.66 @@ -825,23 +829,25 @@
    1.67  fun acyclicity_axiom_for_datatype kk dtypes nfa start_T =
    1.68    #kk_no kk (#kk_intersect kk
    1.69                   (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
    1.70 -(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    1.71 -   -> KK.formula list *)
    1.72 -fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
    1.73 -  map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
    1.74 +(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
    1.75 +   -> dtype_spec list -> KK.formula list *)
    1.76 +fun acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes =
    1.77 +  map_filter (nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes)
    1.78 +             dtypes
    1.79    |> strongly_connected_sub_nfas
    1.80    |> maps (fn nfa =>
    1.81                map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa)
    1.82  
    1.83 -(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
    1.84 -   -> constr_spec -> int -> KK.formula *)
    1.85 -fun sel_axiom_for_sel hol_ctxt j0
    1.86 +(* hol_context -> bool -> int -> kodkod_constrs -> nut NameTable.table
    1.87 +   -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
    1.88 +fun sel_axiom_for_sel hol_ctxt binarize j0
    1.89          (kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no,
    1.90                  kk_join, ...}) rel_table dom_r
    1.91          ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
    1.92          n =
    1.93    let
    1.94 -    val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt const n
    1.95 +    val x as (_, T) =
    1.96 +      binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
    1.97      val (r, R, arity) = const_triple rel_table x
    1.98      val R2 = dest_Func R |> snd
    1.99      val z = (epsilon - delta, delta + j0)
   1.100 @@ -855,9 +861,9 @@
   1.101                                (kk_n_ary_function kk R2 r') (kk_no r'))
   1.102        end
   1.103    end
   1.104 -(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
   1.105 +(* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table
   1.106     -> constr_spec -> KK.formula list *)
   1.107 -fun sel_axioms_for_constr hol_ctxt bits j0 kk rel_table
   1.108 +fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table
   1.109          (constr as {const, delta, epsilon, explicit_max, ...}) =
   1.110    let
   1.111      val honors_explicit_max =
   1.112 @@ -879,19 +885,19 @@
   1.113                               " too small for \"max\"")
   1.114        in
   1.115          max_axiom ::
   1.116 -        map (sel_axiom_for_sel hol_ctxt j0 kk rel_table dom_r constr)
   1.117 +        map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr)
   1.118              (index_seq 0 (num_sels_for_constr_type (snd const)))
   1.119        end
   1.120    end
   1.121 -(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
   1.122 +(* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table
   1.123     -> dtype_spec -> KK.formula list *)
   1.124 -fun sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table
   1.125 +fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
   1.126                              ({constrs, ...} : dtype_spec) =
   1.127 -  maps (sel_axioms_for_constr hol_ctxt bits j0 kk rel_table) constrs
   1.128 +  maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
   1.129  
   1.130 -(* hol_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
   1.131 +(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> constr_spec
   1.132     -> KK.formula list *)
   1.133 -fun uniqueness_axiom_for_constr hol_ctxt
   1.134 +fun uniqueness_axiom_for_constr hol_ctxt binarize
   1.135          ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
   1.136           : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
   1.137    let
   1.138 @@ -899,9 +905,10 @@
   1.139      fun conjunct_for_sel r =
   1.140        kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
   1.141      val num_sels = num_sels_for_constr_type (snd const)
   1.142 -    val triples = map (const_triple rel_table
   1.143 -                       o boxed_nth_sel_for_constr hol_ctxt const)
   1.144 -                      (~1 upto num_sels - 1)
   1.145 +    val triples =
   1.146 +      map (const_triple rel_table
   1.147 +           o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
   1.148 +          (~1 upto num_sels - 1)
   1.149      val j0 = case triples |> hd |> #2 of
   1.150                 Func (Atom (_, j0), _) => j0
   1.151               | R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr",
   1.152 @@ -916,11 +923,11 @@
   1.153                    (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
   1.154                    (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
   1.155    end
   1.156 -(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
   1.157 +(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> dtype_spec
   1.158     -> KK.formula list *)
   1.159 -fun uniqueness_axioms_for_datatype hol_ctxt kk rel_table
   1.160 +fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
   1.161                                     ({constrs, ...} : dtype_spec) =
   1.162 -  map (uniqueness_axiom_for_constr hol_ctxt kk rel_table) constrs
   1.163 +  map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
   1.164  
   1.165  (* constr_spec -> int *)
   1.166  fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
   1.167 @@ -937,22 +944,24 @@
   1.168         kk_disjoint_sets kk rs]
   1.169      end
   1.170  
   1.171 -(* hol_context -> int -> int Typtab.table -> kodkod_constrs
   1.172 +(* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
   1.173     -> nut NameTable.table -> dtype_spec -> KK.formula list *)
   1.174 -fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
   1.175 -  | other_axioms_for_datatype hol_ctxt bits ofs kk rel_table
   1.176 +fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = []
   1.177 +  | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table
   1.178                                (dtype as {typ, ...}) =
   1.179      let val j0 = offset_of_type ofs typ in
   1.180 -      sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table dtype @
   1.181 -      uniqueness_axioms_for_datatype hol_ctxt kk rel_table dtype @
   1.182 +      sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @
   1.183 +      uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @
   1.184        partition_axioms_for_datatype j0 kk rel_table dtype
   1.185      end
   1.186  
   1.187 -(* hol_context -> int -> int Typtab.table -> kodkod_constrs
   1.188 +(* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
   1.189     -> nut NameTable.table -> dtype_spec list -> KK.formula list *)
   1.190 -fun declarative_axioms_for_datatypes hol_ctxt bits ofs kk rel_table dtypes =
   1.191 -  acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
   1.192 -  maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
   1.193 +fun declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk rel_table
   1.194 +                                     dtypes =
   1.195 +  acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes @
   1.196 +  maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
   1.197 +       dtypes
   1.198  
   1.199  (* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
   1.200  fun kodkod_formula_from_nut bits ofs