src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35180 c57dba973391
parent 35179 4b198af5beb5
child 35188 8c70a34931b1
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 13 11:56:06 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 13 15:04:09 2010 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4  val step_mixfix = "_\<^bsub>step\<^esub>"
     1.5  val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
     1.6  val cyclic_co_val_name = "\<omega>"
     1.7 -val cyclic_non_std_type_name = "\<xi>"
     1.8 +val cyclic_type_name = "\<xi>"
     1.9  val opt_flag = nitpick_prefix ^ "opt"
    1.10  val non_opt_flag = nitpick_prefix ^ "non_opt"
    1.11  
    1.12 @@ -259,14 +259,13 @@
    1.13    | mk_tuple _ (t :: _) = t
    1.14    | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
    1.15  
    1.16 -(* string * string * string * string -> scope -> nut list -> nut list
    1.17 -   -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
    1.18 -   -> int list list -> term *)
    1.19 -fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
    1.20 +(* bool -> atom_pool -> string * string * string * string -> scope -> nut list
    1.21 +   -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
    1.22 +   -> typ -> rep -> int list list -> term *)
    1.23 +fun reconstruct_term elaborate pool (maybe_name, base_name, step_name, abs_name)
    1.24          ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
    1.25           : scope) sel_names rel_table bounds =
    1.26    let
    1.27 -    val pool = Unsynchronized.ref []
    1.28      val for_auto = (maybe_name = "")
    1.29      (* int list list -> int *)
    1.30      fun value_of_bits jss =
    1.31 @@ -404,8 +403,11 @@
    1.32              (* styp -> int list *)
    1.33              fun tuples_for_const (s, T) =
    1.34                tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
    1.35 -            (* unit -> indexname * typ *)
    1.36 -            fun var () = ((nth_atom_name pool "" T j k, 0), T)
    1.37 +            (* unit -> term *)
    1.38 +            fun cyclic_atom () =
    1.39 +              nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
    1.40 +            fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
    1.41 +
    1.42              val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
    1.43                                   constrs
    1.44              val real_j = j + offset_of_type ofs T
    1.45 @@ -432,8 +434,9 @@
    1.46              val uncur_arg_Ts = binder_types constr_T
    1.47              val maybe_cyclic = co orelse not standard
    1.48            in
    1.49 -            if maybe_cyclic andalso member (op =) seen (T, j) then
    1.50 -              Var (var ())
    1.51 +            if maybe_cyclic andalso not (null seen) andalso
    1.52 +               member (op =) (seen |> elaborate ? (fst o split_last)) (T, j) then
    1.53 +              cyclic_var ()
    1.54              else if constr_s = @{const_name Word} then
    1.55                HOLogic.mk_number
    1.56                    (if T = @{typ "unsigned_bit word"} then nat_T else int_T)
    1.57 @@ -476,16 +479,23 @@
    1.58                      list_comb (Const constr_x, ts)
    1.59                in
    1.60                  if maybe_cyclic then
    1.61 -                  let val var = var () in
    1.62 -                    if exists_subterm (curry (op =) (Var var)) t then
    1.63 +                  let val var = cyclic_var () in
    1.64 +                    if elaborate andalso not standard andalso
    1.65 +                       length seen = 1 andalso
    1.66 +                       exists_subterm (fn Const (s, _) =>
    1.67 +                                          String.isPrefix cyclic_type_name s
    1.68 +                                        | t' => t' = var) t then
    1.69 +                      let val atom = cyclic_atom () in
    1.70 +                        HOLogic.mk_eq (atom, subst_atomic [(var, atom)] t)
    1.71 +                      end
    1.72 +                    else if exists_subterm (curry (op =) var) t then
    1.73                        if co then
    1.74                          Const (@{const_name The}, (T --> bool_T) --> T)
    1.75                          $ Abs (cyclic_co_val_name, T,
    1.76                                 Const (@{const_name "op ="}, T --> T --> bool_T)
    1.77 -                               $ Bound 0 $ abstract_over (Var var, t))
    1.78 +                               $ Bound 0 $ abstract_over (var, t))
    1.79                        else
    1.80 -                        nth_atom pool for_auto
    1.81 -                                 (Type (cyclic_non_std_type_name, [])) j k
    1.82 +                        cyclic_atom ()
    1.83                      else
    1.84                        t
    1.85                    end
    1.86 @@ -541,17 +551,15 @@
    1.87          raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
    1.88                     Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
    1.89                     string_of_int (length jss))
    1.90 -  in
    1.91 -    polish_funs [] o unbit_and_unbox_term oooo term_for_rep []
    1.92 -  end
    1.93 +  in polish_funs [] o unbit_and_unbox_term oooo term_for_rep [] end
    1.94  
    1.95 -(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
    1.96 -   -> term *)
    1.97 -fun term_for_name scope sel_names rel_table bounds name =
    1.98 +(* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
    1.99 +   -> nut -> term *)
   1.100 +fun term_for_name pool scope sel_names rel_table bounds name =
   1.101    let val T = type_of name in
   1.102      tuple_list_for_name rel_table bounds name
   1.103 -    |> reconstruct_term ("", "", "", "") scope sel_names rel_table bounds T T
   1.104 -                        (rep_of name)
   1.105 +    |> reconstruct_term false pool ("", "", "", "") scope sel_names rel_table
   1.106 +                        bounds T T (rep_of name)
   1.107    end
   1.108  
   1.109  (* Proof.context -> (string * string * string * string) * Proof.context *)
   1.110 @@ -614,6 +622,7 @@
   1.111           card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
   1.112          formats all_frees free_names sel_names nonsel_names rel_table bounds =
   1.113    let
   1.114 +    val pool = Unsynchronized.ref []
   1.115      val (wacky_names as (_, base_name, step_name, _), ctxt) =
   1.116        add_wacky_syntax ctxt
   1.117      val hol_ctxt =
   1.118 @@ -633,11 +642,13 @@
   1.119      val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
   1.120                   bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
   1.121                   ofs = ofs}
   1.122 -    (* typ -> typ -> rep -> int list list -> term *)
   1.123 -    val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table
   1.124 -                                        bounds
   1.125 +    (* bool -> typ -> typ -> rep -> int list list -> term *)
   1.126 +    fun term_for_rep elaborate =
   1.127 +      reconstruct_term elaborate pool wacky_names scope sel_names rel_table
   1.128 +                       bounds
   1.129      (* nat -> typ -> nat -> typ *)
   1.130 -    fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]]
   1.131 +    fun nth_value_of_type card T n =
   1.132 +      term_for_rep true T T (Atom (card, 0)) [[n]]
   1.133      (* nat -> typ -> typ list *)
   1.134      fun all_values_of_type card T =
   1.135        index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord
   1.136 @@ -670,7 +681,7 @@
   1.137                     Const (@{const_name undefined}, T')
   1.138                   else
   1.139                     tuple_list_for_name rel_table bounds name
   1.140 -                   |> term_for_rep T T' (rep_of name)
   1.141 +                   |> term_for_rep false T T' (rep_of name)
   1.142        in
   1.143          Pretty.block (Pretty.breaks
   1.144              [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
   1.145 @@ -763,7 +774,7 @@
   1.146      (* nut -> term *)
   1.147      fun free_name_assm name =
   1.148        HOLogic.mk_eq (Free (nickname_of name, type_of name),
   1.149 -                     term_for_name scope sel_names rel_table bounds name)
   1.150 +                     term_for_name pool scope sel_names rel_table bounds name)
   1.151      val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
   1.152      val model_assms = map free_name_assm free_names
   1.153      val assm = foldr1 s_conj (freeT_assms @ model_assms)