src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 34982 7b8c366e34a2
parent 34974 18b41bba42b5
child 34998 5e492a862b34
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 01 14:12:12 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Feb 02 11:38:38 2010 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/Tools/Nitpick/nitpick_model.ML
     1.5      Author:     Jasmin Blanchette, TU Muenchen
     1.6 -    Copyright   2009
     1.7 +    Copyright   2009, 2010
     1.8  
     1.9  Model reconstruction for Nitpick.
    1.10  *)
    1.11 @@ -53,7 +53,8 @@
    1.12  val base_mixfix = "_\<^bsub>base\<^esub>"
    1.13  val step_mixfix = "_\<^bsub>step\<^esub>"
    1.14  val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
    1.15 -val non_opt_name = nitpick_prefix ^ "non_opt"
    1.16 +val opt_flag = nitpick_prefix ^ "opt"
    1.17 +val non_opt_flag = nitpick_prefix ^ "non_opt"
    1.18  
    1.19  (* string -> int -> string *)
    1.20  fun atom_suffix s j =
    1.21 @@ -62,7 +63,10 @@
    1.22       ? prefix "\<^isub>,"
    1.23  (* string -> typ -> int -> string *)
    1.24  fun atom_name prefix (T as Type (s, _)) j =
    1.25 -    prefix ^ substring (shortest_name s, 0, 1) ^ atom_suffix s j
    1.26 +    let val s' = shortest_name s in
    1.27 +      prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
    1.28 +      atom_suffix s j
    1.29 +    end
    1.30    | atom_name prefix (T as TFree (s, _)) j =
    1.31      prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
    1.32    | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
    1.33 @@ -139,23 +143,21 @@
    1.34    let
    1.35      (* typ -> typ -> (term * term) list -> term *)
    1.36      fun aux T1 T2 [] =
    1.37 -        Const (if maybe_opt orelse T2 <> bool_T then @{const_name undefined}
    1.38 -               else non_opt_name, T1 --> T2)
    1.39 +        Const (if maybe_opt then opt_flag else non_opt_flag, T1 --> T2)
    1.40        | aux T1 T2 ((t1, t2) :: ps) =
    1.41          Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
    1.42          $ aux T1 T2 ps $ t1 $ t2
    1.43    in aux T1 T2 o rev end
    1.44  (* term -> bool *)
    1.45 -fun is_plain_fun (Const (s, _)) =
    1.46 -    (s = @{const_name undefined} orelse s = non_opt_name)
    1.47 +fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
    1.48    | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
    1.49      is_plain_fun t0
    1.50    | is_plain_fun _ = false
    1.51  (* term -> bool * (term list * term list) *)
    1.52  val dest_plain_fun =
    1.53    let
    1.54 -    (* term -> term list * term list *)
    1.55 -    fun aux (Const (s, _)) = (s <> non_opt_name, ([], []))
    1.56 +    (* term -> bool * (term list * term list) *)
    1.57 +    fun aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
    1.58        | aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
    1.59          let val (s, (ts1, ts2)) = aux t0 in (s, (t1 :: ts1, t2 :: ts2)) end
    1.60        | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
    1.61 @@ -300,7 +302,7 @@
    1.62              aux' ps
    1.63        in aux end
    1.64      (* typ list -> term -> term *)
    1.65 -    fun setify_mapify_funs Ts t =
    1.66 +    fun polish_funs Ts t =
    1.67        (case fastype_of1 (Ts, t) of
    1.68           Type ("fun", [T1, T2]) =>
    1.69           if is_plain_fun t then
    1.70 @@ -308,7 +310,7 @@
    1.71               @{typ bool} =>
    1.72               let
    1.73                 val (maybe_opt, ts_pair) =
    1.74 -                 dest_plain_fun t ||> pairself (map (setify_mapify_funs Ts))
    1.75 +                 dest_plain_fun t ||> pairself (map (polish_funs Ts))
    1.76               in
    1.77                 make_set maybe_opt T1 T2
    1.78                          (sort_wrt (truth_const_sort_key o snd) (op ~~ ts_pair))
    1.79 @@ -316,7 +318,7 @@
    1.80             | Type (@{type_name option}, [T2']) =>
    1.81               let
    1.82                 val ts_pair = snd (dest_plain_fun t)
    1.83 -                             |> pairself (map (setify_mapify_funs Ts))
    1.84 +                             |> pairself (map (polish_funs Ts))
    1.85               in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end
    1.86             | _ => raise SAME ()
    1.87           else
    1.88 @@ -324,9 +326,18 @@
    1.89         | _ => raise SAME ())
    1.90        handle SAME () =>
    1.91               case t of
    1.92 -               t1 $ t2 => setify_mapify_funs Ts t1 $ setify_mapify_funs Ts t2
    1.93 -             | Abs (s, T, t') => Abs (s, T, setify_mapify_funs (T :: Ts) t')
    1.94 -             | _ => t
    1.95 +               (t1 as Const (@{const_name fun_upd}, _) $ t11 $ _)
    1.96 +               $ (t2 as Const (s, _)) =>
    1.97 +               if s = unknown then polish_funs Ts t11
    1.98 +               else polish_funs Ts t1 $ polish_funs Ts t2
    1.99 +             | t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
   1.100 +             | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
   1.101 +             | Const (s, Type ("fun", [T1, T2])) =>
   1.102 +               if s = opt_flag orelse s = non_opt_flag then
   1.103 +                 Abs ("x", T1, Const (unknown, T2))
   1.104 +               else
   1.105 +                 t
   1.106 +             | t => t
   1.107      (* bool -> typ -> typ -> typ -> term list -> term list -> term *)
   1.108      fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
   1.109        ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
   1.110 @@ -371,7 +382,7 @@
   1.111            HOLogic.mk_number nat_T j
   1.112          else case datatype_spec datatypes T of
   1.113            NONE => atom for_auto T j
   1.114 -        | SOME {shallow = true, ...} => atom for_auto T j
   1.115 +        | SOME {deep = false, ...} => atom for_auto T j
   1.116          | SOME {co, constrs, ...} =>
   1.117            let
   1.118              (* styp -> int list *)
   1.119 @@ -437,13 +448,16 @@
   1.120                                   | n2 => Const (@{const_name Algebras.divide},
   1.121                                                  num_T --> num_T --> num_T)
   1.122                                           $ mk_num n1 $ mk_num n2)
   1.123 -                      | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
   1.124 -                                         \for_atom (Abs_Frac)", ts)
   1.125 +                      | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
   1.126 +                                         \term_for_atom (Abs_Frac)", ts)
   1.127                      end
   1.128                    else if not for_auto andalso
   1.129                            (is_abs_fun thy constr_x orelse
   1.130                             constr_s = @{const_name Quot}) then
   1.131                      Const (abs_name, constr_T) $ the_single ts
   1.132 +                  else if not for_auto andalso
   1.133 +                          constr_s = @{const_name NonStd} then
   1.134 +                    Const (fst (dest_Const (the_single ts)), T)
   1.135                    else
   1.136                      list_comb (Const constr_x, ts)
   1.137                in
   1.138 @@ -509,8 +523,7 @@
   1.139                     Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
   1.140                     string_of_int (length jss))
   1.141    in
   1.142 -    (not for_auto ? setify_mapify_funs []) o unbit_and_unbox_term
   1.143 -    oooo term_for_rep []
   1.144 +    (not for_auto ? polish_funs []) o unbit_and_unbox_term oooo term_for_rep []
   1.145    end
   1.146  
   1.147  (* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
   1.148 @@ -522,8 +535,7 @@
   1.149                          (rep_of name)
   1.150    end
   1.151  
   1.152 -(* Proof.context
   1.153 -   -> (string * string * string * string * string) * Proof.context *)
   1.154 +(* Proof.context -> (string * string * string * string) * Proof.context *)
   1.155  fun add_wacky_syntax ctxt =
   1.156    let
   1.157      (* term -> string *)
   1.158 @@ -573,13 +585,13 @@
   1.159    -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
   1.160    -> Pretty.T * bool *)
   1.161  fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
   1.162 -        ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
   1.163 -                       debug, binary_ints, destroy_constrs, specialize,
   1.164 -                       skolemize, star_linear_preds, uncurry, fast_descrs,
   1.165 -                       tac_timeout, evals, case_names, def_table, nondef_table,
   1.166 -                       user_nondefs, simp_table, psimp_table, intro_table,
   1.167 -                       ground_thm_table, ersatz_table, skolems, special_funs,
   1.168 -                       unrolled_preds, wf_cache, constr_cache},
   1.169 +        ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
   1.170 +                       user_axioms, debug, binary_ints, destroy_constrs,
   1.171 +                       specialize, skolemize, star_linear_preds, uncurry,
   1.172 +                       fast_descrs, tac_timeout, evals, case_names, def_table,
   1.173 +                       nondef_table, user_nondefs, simp_table, psimp_table,
   1.174 +                       intro_table, ground_thm_table, ersatz_table, skolems,
   1.175 +                       special_funs, unrolled_preds, wf_cache, constr_cache},
   1.176           card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
   1.177          formats all_frees free_names sel_names nonsel_names rel_table bounds =
   1.178    let
   1.179 @@ -587,7 +599,7 @@
   1.180        add_wacky_syntax ctxt
   1.181      val ext_ctxt =
   1.182        {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
   1.183 -       wfs = wfs, user_axioms = user_axioms, debug = debug,
   1.184 +       stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
   1.185         binary_ints = binary_ints, destroy_constrs = destroy_constrs,
   1.186         specialize = specialize, skolemize = skolemize,
   1.187         star_linear_preds = star_linear_preds, uncurry = uncurry,
   1.188 @@ -650,16 +662,15 @@
   1.189        Pretty.block (Pretty.breaks
   1.190            [Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=",
   1.191             Pretty.enum "," "{" "}"
   1.192 -               (map (Syntax.pretty_term ctxt) (all_values_of_type card typ)
   1.193 -                @ (if complete then [] else [Pretty.str unrep]))])
   1.194 +               (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
   1.195 +                (if complete then [] else [Pretty.str unrep]))])
   1.196      (* typ -> dtype_spec list *)
   1.197      fun integer_datatype T =
   1.198        [{typ = T, card = card_of_type card_assigns T, co = false,
   1.199 -        complete = false, concrete = true, shallow = false, constrs = []}]
   1.200 +        complete = false, concrete = true, deep = true, constrs = []}]
   1.201        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
   1.202      val (codatatypes, datatypes) =
   1.203 -      datatypes |> filter_out #shallow
   1.204 -                |> List.partition #co
   1.205 +      datatypes |> filter #deep |> List.partition #co
   1.206                  ||> append (integer_datatype nat_T @ integer_datatype int_T)
   1.207      val block_of_datatypes =
   1.208        if show_datatypes andalso not (null datatypes) then