src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35665 ff2bf50505ab
parent 35625 9c818cab0dd0
child 35711 548d3f16404b
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Mar 08 15:20:40 2010 -0800
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Mar 09 09:25:23 2010 +0100
     1.3 @@ -110,48 +110,53 @@
     1.4    the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
     1.5  
     1.6  (* term -> term *)
     1.7 -fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
     1.8 -    unarize_and_unbox_term t1
     1.9 -  | unarize_and_unbox_term (Const (@{const_name PairBox},
    1.10 -                                   Type ("fun", [T1, Type ("fun", [T2, _])]))
    1.11 -                            $ t1 $ t2) =
    1.12 -    let val Ts = map unarize_unbox_and_uniterize_type [T1, T2] in
    1.13 -      Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
    1.14 -      $ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
    1.15 +fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) =
    1.16 +    unarize_unbox_etc_term t1
    1.17 +  | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
    1.18 +    unarize_unbox_etc_term t1
    1.19 +  | unarize_unbox_etc_term
    1.20 +        (Const (@{const_name PairBox},
    1.21 +                Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])]))
    1.22 +         $ t1 $ t2) =
    1.23 +    let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in
    1.24 +      Const (@{const_name Pair}, Ts ---> Type (@{type_name "*"}, Ts))
    1.25 +      $ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
    1.26      end
    1.27 -  | unarize_and_unbox_term (Const (s, T)) =
    1.28 -    Const (s, unarize_unbox_and_uniterize_type T)
    1.29 -  | unarize_and_unbox_term (t1 $ t2) =
    1.30 -    unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
    1.31 -  | unarize_and_unbox_term (Free (s, T)) =
    1.32 -    Free (s, unarize_unbox_and_uniterize_type T)
    1.33 -  | unarize_and_unbox_term (Var (x, T)) =
    1.34 -    Var (x, unarize_unbox_and_uniterize_type T)
    1.35 -  | unarize_and_unbox_term (Bound j) = Bound j
    1.36 -  | unarize_and_unbox_term (Abs (s, T, t')) =
    1.37 -    Abs (s, unarize_unbox_and_uniterize_type T, unarize_and_unbox_term t')
    1.38 +  | unarize_unbox_etc_term (Const (s, T)) =
    1.39 +    Const (s, uniterize_unarize_unbox_etc_type T)
    1.40 +  | unarize_unbox_etc_term (t1 $ t2) =
    1.41 +    unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
    1.42 +  | unarize_unbox_etc_term (Free (s, T)) =
    1.43 +    Free (s, uniterize_unarize_unbox_etc_type T)
    1.44 +  | unarize_unbox_etc_term (Var (x, T)) =
    1.45 +    Var (x, uniterize_unarize_unbox_etc_type T)
    1.46 +  | unarize_unbox_etc_term (Bound j) = Bound j
    1.47 +  | unarize_unbox_etc_term (Abs (s, T, t')) =
    1.48 +    Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t')
    1.49  
    1.50  (* typ -> typ -> (typ * typ) * (typ * typ) *)
    1.51 -fun factor_out_types (T1 as Type ("*", [T11, T12]))
    1.52 -                     (T2 as Type ("*", [T21, T22])) =
    1.53 +fun factor_out_types (T1 as Type (@{type_name "*"}, [T11, T12]))
    1.54 +                     (T2 as Type (@{type_name "*"}, [T21, T22])) =
    1.55      let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
    1.56        if n1 = n2 then
    1.57          let
    1.58            val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
    1.59          in
    1.60 -          ((Type ("*", [T11, T11']), opt_T12'),
    1.61 -           (Type ("*", [T21, T21']), opt_T22'))
    1.62 +          ((Type (@{type_name "*"}, [T11, T11']), opt_T12'),
    1.63 +           (Type (@{type_name "*"}, [T21, T21']), opt_T22'))
    1.64          end
    1.65        else if n1 < n2 then
    1.66          case factor_out_types T1 T21 of
    1.67            (p1, (T21', NONE)) => (p1, (T21', SOME T22))
    1.68          | (p1, (T21', SOME T22')) =>
    1.69 -          (p1, (T21', SOME (Type ("*", [T22', T22]))))
    1.70 +          (p1, (T21', SOME (Type (@{type_name "*"}, [T22', T22]))))
    1.71        else
    1.72          swap (factor_out_types T2 T1)
    1.73      end
    1.74 -  | factor_out_types (Type ("*", [T11, T12])) T2 = ((T11, SOME T12), (T2, NONE))
    1.75 -  | factor_out_types T1 (Type ("*", [T21, T22])) = ((T1, NONE), (T21, SOME T22))
    1.76 +  | factor_out_types (Type (@{type_name "*"}, [T11, T12])) T2 =
    1.77 +    ((T11, SOME T12), (T2, NONE))
    1.78 +  | factor_out_types T1 (Type (@{type_name "*"}, [T21, T22])) =
    1.79 +    ((T1, NONE), (T21, SOME T22))
    1.80    | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
    1.81  
    1.82  (* bool -> typ -> typ -> (term * term) list -> term *)
    1.83 @@ -188,10 +193,11 @@
    1.84      val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
    1.85    in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
    1.86  (* typ -> term -> term -> term *)
    1.87 -fun pair_up (Type ("*", [T1', T2']))
    1.88 +fun pair_up (Type (@{type_name "*"}, [T1', T2']))
    1.89              (t1 as Const (@{const_name Pair},
    1.90 -                          Type ("fun", [_, Type ("fun", [_, T1])])) $ t11 $ t12)
    1.91 -            t2 =
    1.92 +                          Type (@{type_name fun},
    1.93 +                                [_, Type (@{type_name fun}, [_, T1])]))
    1.94 +             $ t11 $ t12) t2 =
    1.95      if T1 = T1' then HOLogic.mk_prod (t1, t2)
    1.96      else HOLogic.mk_prod (t11, pair_up T2' t12 t2)
    1.97    | pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
    1.98 @@ -199,7 +205,7 @@
    1.99  fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3
   1.100  
   1.101  (* typ -> typ -> typ -> term -> term *)
   1.102 -fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t =
   1.103 +fun typecast_fun (Type (@{type_name fun}, [T1', T2'])) T1 T2 t =
   1.104      let
   1.105        (* typ -> typ -> typ -> typ -> term -> term *)
   1.106        fun do_curry T1 T1a T1b T2 t =
   1.107 @@ -238,9 +244,11 @@
   1.108            t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
   1.109          | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
   1.110        (* typ -> typ -> term -> term *)
   1.111 -      and do_term (Type ("fun", [T1', T2'])) (Type ("fun", [T1, T2])) t =
   1.112 +      and do_term (Type (@{type_name fun}, [T1', T2']))
   1.113 +                  (Type (@{type_name fun}, [T1, T2])) t =
   1.114            do_fun T1' T2' T1 T2 t
   1.115 -        | do_term (T' as Type ("*", Ts' as [T1', T2'])) (Type ("*", [T1, T2]))
   1.116 +        | do_term (T' as Type (@{type_name "*"}, Ts' as [T1', T2']))
   1.117 +                  (Type (@{type_name "*"}, [T1, T2]))
   1.118                    (Const (@{const_name Pair}, _) $ t1 $ t2) =
   1.119            Const (@{const_name Pair}, Ts' ---> T')
   1.120            $ do_term T1' T1 t1 $ do_term T2' T2 t2
   1.121 @@ -257,7 +265,7 @@
   1.122    | truth_const_sort_key _ = "1"
   1.123  
   1.124  (* typ -> term list -> term *)
   1.125 -fun mk_tuple (Type ("*", [T1, T2])) ts =
   1.126 +fun mk_tuple (Type (@{type_name "*"}, [T1, T2])) ts =
   1.127      HOLogic.mk_prod (mk_tuple T1 ts,
   1.128          mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
   1.129    | mk_tuple _ (t :: _) = t
   1.130 @@ -307,8 +315,8 @@
   1.131          else
   1.132            aux tps
   1.133        end
   1.134 -    (* typ -> typ -> typ -> (term * term) list -> term *)
   1.135 -    fun make_map T1 T2 T2' =
   1.136 +    (* bool -> typ -> typ -> typ -> (term * term) list -> term *)
   1.137 +    fun make_map maybe_opt T1 T2 T2' =
   1.138        let
   1.139          val update_const = Const (@{const_name fun_upd},
   1.140                                    (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
   1.141 @@ -319,7 +327,7 @@
   1.142                 Const (@{const_name None}, _) => aux' ps
   1.143               | _ => update_const $ aux' ps $ t1 $ t2)
   1.144          fun aux ps =
   1.145 -          if not (is_complete_type datatypes false T1) then
   1.146 +          if maybe_opt andalso not (is_complete_type datatypes false T1) then
   1.147              update_const $ aux' ps $ Const (unrep, T1)
   1.148              $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
   1.149            else
   1.150 @@ -328,7 +336,7 @@
   1.151      (* typ list -> term -> term *)
   1.152      fun polish_funs Ts t =
   1.153        (case fastype_of1 (Ts, t) of
   1.154 -         Type ("fun", [T1, T2]) =>
   1.155 +         Type (@{type_name fun}, [T1, T2]) =>
   1.156           if is_plain_fun t then
   1.157             case T2 of
   1.158               @{typ bool} =>
   1.159 @@ -341,9 +349,9 @@
   1.160               end
   1.161             | Type (@{type_name option}, [T2']) =>
   1.162               let
   1.163 -               val ts_pair = snd (dest_plain_fun t)
   1.164 -                             |> pairself (map (polish_funs Ts))
   1.165 -             in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end
   1.166 +               val (maybe_opt, ts_pair) =
   1.167 +                 dest_plain_fun t ||> pairself (map (polish_funs Ts))
   1.168 +             in make_map maybe_opt T1 T2 T2' (rev (op ~~ ts_pair)) end
   1.169             | _ => raise SAME ()
   1.170           else
   1.171             raise SAME ()
   1.172 @@ -356,7 +364,7 @@
   1.173                 else polish_funs Ts t1 $ polish_funs Ts t2
   1.174               | t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
   1.175               | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
   1.176 -             | Const (s, Type ("fun", [T1, T2])) =>
   1.177 +             | Const (s, Type (@{type_name fun}, [T1, T2])) =>
   1.178                 if s = opt_flag orelse s = non_opt_flag then
   1.179                   Abs ("x", T1, Const (unknown, T2))
   1.180                 else
   1.181 @@ -366,24 +374,24 @@
   1.182      fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
   1.183        ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
   1.184                   |> make_plain_fun maybe_opt T1 T2
   1.185 -                 |> unarize_and_unbox_term
   1.186 -                 |> typecast_fun (unarize_unbox_and_uniterize_type T')
   1.187 -                                 (unarize_unbox_and_uniterize_type T1)
   1.188 -                                 (unarize_unbox_and_uniterize_type T2)
   1.189 +                 |> unarize_unbox_etc_term
   1.190 +                 |> typecast_fun (uniterize_unarize_unbox_etc_type T')
   1.191 +                                 (uniterize_unarize_unbox_etc_type T1)
   1.192 +                                 (uniterize_unarize_unbox_etc_type T2)
   1.193      (* (typ * int) list -> typ -> typ -> int -> term *)
   1.194 -    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j _ =
   1.195 +    fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ =
   1.196          let
   1.197            val k1 = card_of_type card_assigns T1
   1.198            val k2 = card_of_type card_assigns T2
   1.199          in
   1.200 -          term_for_rep seen T T' (Vect (k1, Atom (k2, 0)))
   1.201 +          term_for_rep true seen T T' (Vect (k1, Atom (k2, 0)))
   1.202                         [nth_combination (replicate k1 (k2, 0)) j]
   1.203            handle General.Subscript =>
   1.204                   raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom",
   1.205                              signed_string_of_int j ^ " for " ^
   1.206                              string_for_rep (Vect (k1, Atom (k2, 0))))
   1.207          end
   1.208 -      | term_for_atom seen (Type ("*", [T1, T2])) _ j k =
   1.209 +      | term_for_atom seen (Type (@{type_name "*"}, [T1, T2])) _ j k =
   1.210          let
   1.211            val k1 = card_of_type card_assigns T1
   1.212            val k2 = k div k1
   1.213 @@ -461,8 +469,9 @@
   1.214                    if length arg_Ts = 0 then
   1.215                      []
   1.216                    else
   1.217 -                    map3 (fn Ts => term_for_rep seen Ts Ts) arg_Ts arg_Rs
   1.218 -                         arg_jsss
   1.219 +                    map3 (fn Ts =>
   1.220 +                             term_for_rep (constr_s <> @{const_name FinFun})
   1.221 +                                          seen Ts Ts) arg_Ts arg_Rs arg_jsss
   1.222                      |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
   1.223                      |> dest_n_tuple (length uncur_arg_Ts)
   1.224                  val t =
   1.225 @@ -519,50 +528,54 @@
   1.226      and term_for_vect seen k R T1 T2 T' js =
   1.227        make_fun true T1 T2 T'
   1.228                 (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
   1.229 -               (map (term_for_rep seen T2 T2 R o single)
   1.230 +               (map (term_for_rep true seen T2 T2 R o single)
   1.231                      (batch_list (arity_of_rep R) js))
   1.232 -    (* (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
   1.233 -    and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 1
   1.234 -      | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] =
   1.235 +    (* bool -> (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
   1.236 +    and term_for_rep _ seen T T' Unit [[]] = term_for_atom seen T T' 0 1
   1.237 +      | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
   1.238          if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
   1.239          else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
   1.240 -      | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] =
   1.241 +      | term_for_rep _ seen (Type (@{type_name "*"}, [T1, T2])) _
   1.242 +                     (Struct [R1, R2]) [js] =
   1.243          let
   1.244            val arity1 = arity_of_rep R1
   1.245            val (js1, js2) = chop arity1 js
   1.246          in
   1.247            list_comb (HOLogic.pair_const T1 T2,
   1.248 -                     map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2]
   1.249 +                     map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
   1.250                            [[js1], [js2]])
   1.251          end
   1.252 -      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Vect (k, R')) [js] =
   1.253 +      | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
   1.254 +                     (Vect (k, R')) [js] =
   1.255          term_for_vect seen k R' T1 T2 T' js
   1.256 -      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, Formula Neut))
   1.257 -                     jss =
   1.258 +      | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
   1.259 +                     (Func (R1, Formula Neut)) jss =
   1.260          let
   1.261            val jss1 = all_combinations_for_rep R1
   1.262 -          val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
   1.263 +          val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1
   1.264            val ts2 =
   1.265 -            map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
   1.266 +            map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0))
   1.267                                         [[int_from_bool (member (op =) jss js)]])
   1.268                  jss1
   1.269          in make_fun false T1 T2 T' ts1 ts2 end
   1.270 -      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
   1.271 +      | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
   1.272 +                     (Func (R1, R2)) jss =
   1.273          let
   1.274            val arity1 = arity_of_rep R1
   1.275            val jss1 = all_combinations_for_rep R1
   1.276 -          val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
   1.277 +          val ts1 = map (term_for_rep false seen T1 T1 R1 o single) jss1
   1.278            val grouped_jss2 = AList.group (op =) (map (chop arity1) jss)
   1.279 -          val ts2 = map (term_for_rep seen T2 T2 R2 o the_default []
   1.280 +          val ts2 = map (term_for_rep false seen T2 T2 R2 o the_default []
   1.281                           o AList.lookup (op =) grouped_jss2) jss1
   1.282 -        in make_fun true T1 T2 T' ts1 ts2 end
   1.283 -      | term_for_rep seen T T' (Opt R) jss =
   1.284 -        if null jss then Const (unknown, T) else term_for_rep seen T T' R jss
   1.285 -      | term_for_rep _ T _ R jss =
   1.286 +        in make_fun maybe_opt T1 T2 T' ts1 ts2 end
   1.287 +      | term_for_rep _ seen T T' (Opt R) jss =
   1.288 +        if null jss then Const (unknown, T)
   1.289 +        else term_for_rep true seen T T' R jss
   1.290 +      | term_for_rep _ _ T _ R jss =
   1.291          raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
   1.292                     Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
   1.293                     string_of_int (length jss))
   1.294 -  in polish_funs [] o unarize_and_unbox_term oooo term_for_rep [] end
   1.295 +  in polish_funs [] o unarize_unbox_etc_term oooo term_for_rep true [] end
   1.296  
   1.297  (* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
   1.298     -> nut -> term *)
   1.299 @@ -689,7 +702,7 @@
   1.300          val (oper, (t1, T'), T) =
   1.301            case name of
   1.302              FreeName (s, T, _) =>
   1.303 -            let val t = Free (s, unarize_unbox_and_uniterize_type T) in
   1.304 +            let val t = Free (s, uniterize_unarize_unbox_etc_type T) in
   1.305                ("=", (t, format_term_type thy def_table formats t), T)
   1.306              end
   1.307            | ConstName (s, T, _) =>
   1.308 @@ -710,12 +723,17 @@
   1.309      (* dtype_spec -> Pretty.T *)
   1.310      fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
   1.311        Pretty.block (Pretty.breaks
   1.312 -          [Syntax.pretty_typ ctxt (unarize_unbox_and_uniterize_type typ),
   1.313 -           Pretty.str "=",
   1.314 -           Pretty.enum "," "{" "}"
   1.315 -               (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
   1.316 -                (if fun_from_pair complete false then []
   1.317 -                 else [Pretty.str unrep]))])
   1.318 +          (Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
   1.319 +           (case typ of
   1.320 +              Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
   1.321 +            | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
   1.322 +            | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
   1.323 +            | _ => []) @
   1.324 +           [Pretty.str "=",
   1.325 +            Pretty.enum "," "{" "}"
   1.326 +                (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
   1.327 +                 (if fun_from_pair complete false then []
   1.328 +                  else [Pretty.str unrep]))]))
   1.329      (* typ -> dtype_spec list *)
   1.330      fun integer_datatype T =
   1.331        [{typ = T, card = card_of_type card_assigns T, co = false,
   1.332 @@ -752,13 +770,14 @@
   1.333      val (eval_names, noneval_nonskolem_nonsel_names) =
   1.334        List.partition (String.isPrefix eval_prefix o nickname_of)
   1.335                       nonskolem_nonsel_names
   1.336 -      ||> filter_out (curry (op =) @{const_name bisim_iterator_max}
   1.337 +      ||> filter_out (member (op =) [@{const_name bisim},
   1.338 +                                     @{const_name bisim_iterator_max}]
   1.339                        o nickname_of)
   1.340      val free_names =
   1.341        map (fn x as (s, T) =>
   1.342                case filter (curry (op =) x
   1.343                         o pairf nickname_of
   1.344 -                               (unarize_unbox_and_uniterize_type o type_of))
   1.345 +                               (uniterize_unarize_unbox_etc_type o type_of))
   1.346                         free_names of
   1.347                  [name] => name
   1.348                | [] => FreeName (s, T, Any)