src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 46083 efeaa79f021b
parent 45479 3387d482e0a9
child 46097 0ed9365fa9d2
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jan 03 18:33:17 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jan 03 18:33:17 2012 +0100
     1.3 @@ -228,6 +228,8 @@
     1.4      ((T1, NONE), (T21, SOME T22))
     1.5    | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
     1.6  
     1.7 +(* Term-encoded data structure for holding key-value pairs as well as an "opt"
     1.8 +   flag indicating whether the function is approximated. *)
     1.9  fun make_plain_fun maybe_opt T1 T2 =
    1.10    let
    1.11      fun aux T1 T2 [] =
    1.12 @@ -268,55 +270,55 @@
    1.13    | pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
    1.14  fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3
    1.15  
    1.16 -fun typecast_fun (Type (@{type_name fun}, [T1', T2'])) T1 T2 t =
    1.17 -    let
    1.18 -      fun do_curry T1 T1a T1b T2 t =
    1.19 -        let
    1.20 -          val (maybe_opt, tsp) = dest_plain_fun t
    1.21 -          val tps =
    1.22 -            tsp |>> map (break_in_two T1 T1a T1b)
    1.23 -                |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
    1.24 -                |> AList.coalesce (op =)
    1.25 -                |> map (apsnd (make_plain_fun maybe_opt T1b T2))
    1.26 -        in make_plain_fun maybe_opt T1a (T1b --> T2) tps end
    1.27 -      and do_uncurry T1 T2 t =
    1.28 -        let
    1.29 -          val (maybe_opt, tsp) = dest_plain_fun t
    1.30 -          val tps =
    1.31 -            tsp |> op ~~
    1.32 -                |> maps (fn (t1, t2) =>
    1.33 -                            multi_pair_up T1 t1 (snd (dest_plain_fun t2)))
    1.34 -        in make_plain_fun maybe_opt T1 T2 tps end
    1.35 -      and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' --> T2')
    1.36 -        | do_arrow T1' T2' T1 T2
    1.37 -                   (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
    1.38 -          Const (@{const_name fun_upd},
    1.39 -                 (T1' --> T2') --> T1' --> T2' --> T1' --> T2')
    1.40 -          $ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2
    1.41 -        | do_arrow _ _ _ _ t =
    1.42 -          raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t])
    1.43 -      and do_fun T1' T2' T1 T2 t =
    1.44 -        case factor_out_types T1' T1 of
    1.45 -          ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
    1.46 -        | ((_, NONE), (T1a, SOME T1b)) =>
    1.47 -          t |> do_curry T1 T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
    1.48 -        | ((T1a', SOME T1b'), (_, NONE)) =>
    1.49 -          t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
    1.50 -        | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
    1.51 -      and do_term (Type (@{type_name fun}, [T1', T2']))
    1.52 -                  (Type (@{type_name fun}, [T1, T2])) t =
    1.53 -          do_fun T1' T2' T1 T2 t
    1.54 -        | do_term (T' as Type (@{type_name prod}, Ts' as [T1', T2']))
    1.55 -                  (Type (@{type_name prod}, [T1, T2]))
    1.56 -                  (Const (@{const_name Pair}, _) $ t1 $ t2) =
    1.57 -          Const (@{const_name Pair}, Ts' ---> T')
    1.58 -          $ do_term T1' T1 t1 $ do_term T2' T2 t2
    1.59 -        | do_term T' T t =
    1.60 -          if T = T' then t
    1.61 -          else raise TYPE ("Nitpick_Model.typecast_fun.do_term", [T, T'], [])
    1.62 -    in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
    1.63 -  | typecast_fun T' _ _ _ =
    1.64 -    raise TYPE ("Nitpick_Model.typecast_fun", [T'], [])
    1.65 +fun format_fun T' T1 T2 t =
    1.66 +  let
    1.67 +    val T1' = pseudo_domain_type T'
    1.68 +    val T2' = pseudo_range_type T'
    1.69 +    fun do_curry T1 T1a T1b T2 t =
    1.70 +      let
    1.71 +        val (maybe_opt, tsp) = dest_plain_fun t
    1.72 +        val tps =
    1.73 +          tsp |>> map (break_in_two T1 T1a T1b)
    1.74 +              |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
    1.75 +              |> AList.coalesce (op =)
    1.76 +              |> map (apsnd (make_plain_fun maybe_opt T1b T2))
    1.77 +      in make_plain_fun maybe_opt T1a (T1b --> T2) tps end
    1.78 +    and do_uncurry T1 T2 t =
    1.79 +      let
    1.80 +        val (maybe_opt, tsp) = dest_plain_fun t
    1.81 +        val tps =
    1.82 +          tsp |> op ~~
    1.83 +              |> maps (fn (t1, t2) =>
    1.84 +                          multi_pair_up T1 t1 (snd (dest_plain_fun t2)))
    1.85 +      in make_plain_fun maybe_opt T1 T2 tps end
    1.86 +    and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' --> T2')
    1.87 +      | do_arrow T1' T2' T1 T2
    1.88 +                 (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
    1.89 +        Const (@{const_name fun_upd},
    1.90 +               (T1' --> T2') --> T1' --> T2' --> T1' --> T2')
    1.91 +        $ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2
    1.92 +      | do_arrow _ _ _ _ t =
    1.93 +        raise TERM ("Nitpick_Model.format_fun.do_arrow", [t])
    1.94 +    and do_fun T1' T2' T1 T2 t =
    1.95 +      case factor_out_types T1' T1 of
    1.96 +        ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
    1.97 +      | ((_, NONE), (T1a, SOME T1b)) =>
    1.98 +        t |> do_curry T1 T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
    1.99 +      | ((T1a', SOME T1b'), (_, NONE)) =>
   1.100 +        t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
   1.101 +      | _ => raise TYPE ("Nitpick_Model.format_fun.do_fun", [T1, T1'], [])
   1.102 +    and do_term (Type (@{type_name fun}, [T1', T2']))
   1.103 +                (Type (@{type_name fun}, [T1, T2])) t =
   1.104 +        do_fun T1' T2' T1 T2 t
   1.105 +      | do_term (T' as Type (@{type_name prod}, Ts' as [T1', T2']))
   1.106 +                (Type (@{type_name prod}, [T1, T2]))
   1.107 +                (Const (@{const_name Pair}, _) $ t1 $ t2) =
   1.108 +        Const (@{const_name Pair}, Ts' ---> T')
   1.109 +        $ do_term T1' T1 t1 $ do_term T2' T2 t2
   1.110 +      | do_term T' T t =
   1.111 +        if T = T' then t
   1.112 +        else raise TYPE ("Nitpick_Model.format_fun.do_term", [T, T'], [])
   1.113 +  in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
   1.114  
   1.115  fun truth_const_sort_key @{const True} = "0"
   1.116    | truth_const_sort_key @{const False} = "2"
   1.117 @@ -385,14 +387,14 @@
   1.118        | postprocess_subterms Ts (Abs (s, T, t')) =
   1.119          Abs (s, T, postprocess_subterms (T :: Ts) t')
   1.120        | postprocess_subterms Ts t = postprocess_term (fastype_of1 (Ts, t)) t
   1.121 -    fun make_set maybe_opt T1 T2 tps =
   1.122 +    fun make_set maybe_opt T tps =
   1.123        let
   1.124 -        val empty_const = Const (@{const_abbrev Set.empty}, T1 --> T2)
   1.125 -        val insert_const = Const (@{const_name insert},
   1.126 -                                  T1 --> (T1 --> T2) --> T1 --> T2)
   1.127 +        val empty_const = Const (@{const_abbrev Set.empty}, T --> bool_T)
   1.128 +        val insert_const =
   1.129 +          Const (@{const_name insert}, T --> (T --> bool_T) --> T --> bool_T)
   1.130          fun aux [] =
   1.131 -            if maybe_opt andalso not (is_complete_type datatypes false T1) then
   1.132 -              insert_const $ Const (unrep (), T1) $ empty_const
   1.133 +            if maybe_opt andalso not (is_complete_type datatypes false T) then
   1.134 +              insert_const $ Const (unrep (), T) $ empty_const
   1.135              else
   1.136                empty_const
   1.137            | aux ((t1, t2) :: zs) =
   1.138 @@ -402,11 +404,11 @@
   1.139                         (insert_const
   1.140                          $ (t1 |> t2 <> @{const True}
   1.141                                   ? curry (op $)
   1.142 -                                         (Const (maybe_name, T1 --> T1))))
   1.143 +                                         (Const (maybe_name, T --> T))))
   1.144        in
   1.145          if forall (fn (_, t) => t <> @{const True} andalso t <> @{const False})
   1.146                    tps then
   1.147 -          Const (unknown, T1 --> T2)
   1.148 +          Const (unknown, T --> bool_T)
   1.149          else
   1.150            aux tps
   1.151        end
   1.152 @@ -431,15 +433,7 @@
   1.153           Type (@{type_name fun}, [T1, T2]) =>
   1.154           if is_plain_fun t then
   1.155             case T2 of
   1.156 -             @{typ bool} =>
   1.157 -             let
   1.158 -               val (maybe_opt, ts_pair) =
   1.159 -                 dest_plain_fun t ||> pairself (map (polish_funs Ts))
   1.160 -             in
   1.161 -               make_set maybe_opt T1 T2
   1.162 -                        (sort_wrt (truth_const_sort_key o snd) (op ~~ ts_pair))
   1.163 -             end
   1.164 -           | Type (@{type_name option}, [T2']) =>
   1.165 +             Type (@{type_name option}, [T2']) =>
   1.166               let
   1.167                 val (maybe_opt, ts_pair) =
   1.168                   dest_plain_fun t ||> pairself (map (polish_funs Ts))
   1.169 @@ -466,13 +460,19 @@
   1.170                 else
   1.171                   t
   1.172               | t => t
   1.173 -    fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
   1.174 -      ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
   1.175 -                 |> make_plain_fun maybe_opt T1 T2
   1.176 -                 |> unarize_unbox_etc_term
   1.177 -                 |> typecast_fun (uniterize_unarize_unbox_etc_type T')
   1.178 -                                 (uniterize_unarize_unbox_etc_type T1)
   1.179 -                                 (uniterize_unarize_unbox_etc_type T2)
   1.180 +    fun make_fun_or_set maybe_opt T T1 T2 T' ts1 ts2 =
   1.181 +      ts1 ~~ ts2
   1.182 +      |> sort (nice_term_ord o pairself fst)
   1.183 +      |> (case T of
   1.184 +            Type (@{type_name set}, _) =>
   1.185 +            sort_wrt (truth_const_sort_key o snd)
   1.186 +            #> make_set maybe_opt T'
   1.187 +          | _ =>
   1.188 +            make_plain_fun maybe_opt T1 T2
   1.189 +            #> unarize_unbox_etc_term
   1.190 +            #> format_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      fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ =
   1.194          let
   1.195            val k1 = card_of_type card_assigns T1
   1.196 @@ -603,11 +603,16 @@
   1.197                    t
   1.198                end
   1.199            end
   1.200 -    and term_for_vect seen k R T1 T2 T' js =
   1.201 -      make_fun true T1 T2 T'
   1.202 -               (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
   1.203 -               (map (term_for_rep true seen T2 T2 R o single)
   1.204 -                    (batch_list (arity_of_rep R) js))
   1.205 +    and term_for_vect seen k R T T' js =
   1.206 +      let
   1.207 +        val T1 = pseudo_domain_type T
   1.208 +        val T2 = pseudo_range_type T
   1.209 +      in
   1.210 +        make_fun_or_set true T T1 T2 T'
   1.211 +            (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
   1.212 +            (map (term_for_rep true seen T2 T2 R o single)
   1.213 +                 (batch_list (arity_of_rep R) js))
   1.214 +      end
   1.215      and term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
   1.216          if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
   1.217          else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
   1.218 @@ -621,29 +626,30 @@
   1.219                       map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
   1.220                            [[js1], [js2]])
   1.221          end
   1.222 -      | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
   1.223 -                     (Vect (k, R')) [js] =
   1.224 -        term_for_vect seen k R' T1 T2 T' js
   1.225 -      | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
   1.226 -                     (Func (R1, Formula Neut)) jss =
   1.227 +      | term_for_rep _ seen T T' (Vect (k, R')) [js] =
   1.228 +        term_for_vect seen k R' T T' js
   1.229 +      | term_for_rep maybe_opt seen T T' (Func (R1, Formula Neut)) jss =
   1.230          let
   1.231 +          val T1 = pseudo_domain_type T
   1.232 +          val T2 = pseudo_range_type T
   1.233            val jss1 = all_combinations_for_rep R1
   1.234            val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1
   1.235            val ts2 =
   1.236              map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0))
   1.237                                         [[int_from_bool (member (op =) jss js)]])
   1.238                  jss1
   1.239 -        in make_fun maybe_opt T1 T2 T' ts1 ts2 end
   1.240 -      | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
   1.241 -                     (Func (R1, R2)) jss =
   1.242 +        in make_fun_or_set maybe_opt T T1 T2 T' ts1 ts2 end
   1.243 +      | term_for_rep maybe_opt seen T T' (Func (R1, R2)) jss =
   1.244          let
   1.245 +          val T1 = pseudo_domain_type T
   1.246 +          val T2 = pseudo_range_type T
   1.247            val arity1 = arity_of_rep R1
   1.248            val jss1 = all_combinations_for_rep R1
   1.249            val ts1 = map (term_for_rep false seen T1 T1 R1 o single) jss1
   1.250            val grouped_jss2 = AList.group (op =) (map (chop arity1) jss)
   1.251            val ts2 = map (term_for_rep false seen T2 T2 R2 o the_default []
   1.252                           o AList.lookup (op =) grouped_jss2) jss1
   1.253 -        in make_fun maybe_opt T1 T2 T' ts1 ts2 end
   1.254 +        in make_fun_or_set maybe_opt T T1 T2 T' ts1 ts2 end
   1.255        | term_for_rep _ seen T T' (Opt R) jss =
   1.256          if null jss then Const (unknown, T)
   1.257          else term_for_rep true seen T T' R jss
   1.258 @@ -1045,11 +1051,13 @@
   1.259                     |> map_types (map_type_tfree
   1.260                                       (fn (s, []) => TFree (s, HOLogic.typeS)
   1.261                                         | x => TFree x))
   1.262 -       val _ = if debug then
   1.263 -                 Output.urgent_message ((if negate then "Genuineness" else "Spuriousness") ^
   1.264 -                           " goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
   1.265 -               else
   1.266 -                 ()
   1.267 +        val _ =
   1.268 +          if debug then
   1.269 +            (if negate then "Genuineness" else "Spuriousness") ^ " goal: " ^
   1.270 +            Syntax.string_of_term ctxt prop ^ "."
   1.271 +            |> Output.urgent_message
   1.272 +          else
   1.273 +            ()
   1.274          val goal = prop |> cterm_of thy |> Goal.init
   1.275        in
   1.276          (goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt))