src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 35190 ce653cc27a94
parent 35181 92d857a4e5e0
child 35220 2bcdae5f4fdb
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 17 14:11:41 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 17 20:46:50 2010 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4    val strip_any_connective : term -> term list * term
     1.5    val conjuncts_of : term -> term list
     1.6    val disjuncts_of : term -> term list
     1.7 -  val unbit_and_unbox_type : typ -> typ
     1.8 +  val unarize_and_unbox_type : typ -> typ
     1.9    val string_for_type : Proof.context -> typ -> string
    1.10    val prefix_name : string -> string -> string
    1.11    val shortest_name : string -> string
    1.12 @@ -117,11 +117,14 @@
    1.13    val is_sel : string -> bool
    1.14    val is_sel_like_and_no_discr : string -> bool
    1.15    val box_type : hol_context -> boxability -> typ -> typ
    1.16 +  val binarize_nat_and_int_in_type : typ -> typ
    1.17 +  val binarize_nat_and_int_in_term : term -> term
    1.18    val discr_for_constr : styp -> styp
    1.19    val num_sels_for_constr_type : typ -> int
    1.20    val nth_sel_name_for_constr_name : string -> int -> string
    1.21    val nth_sel_for_constr : styp -> int -> styp
    1.22 -  val boxed_nth_sel_for_constr : hol_context -> styp -> int -> styp
    1.23 +  val binarized_and_boxed_nth_sel_for_constr :
    1.24 +    hol_context -> bool -> styp -> int -> styp
    1.25    val sel_no_from_name : string -> int
    1.26    val close_form : term -> term
    1.27    val eta_expand : typ list -> term -> int -> term
    1.28 @@ -132,10 +135,11 @@
    1.29    val register_codatatype : typ -> string -> styp list -> theory -> theory
    1.30    val unregister_codatatype : typ -> theory -> theory
    1.31    val datatype_constrs : hol_context -> typ -> styp list
    1.32 -  val boxed_datatype_constrs : hol_context -> typ -> styp list
    1.33 +  val binarized_and_boxed_datatype_constrs :
    1.34 +    hol_context -> bool -> typ -> styp list
    1.35    val num_datatype_constrs : hol_context -> typ -> int
    1.36    val constr_name_for_sel_like : string -> string
    1.37 -  val boxed_constr_for_sel : hol_context -> styp -> styp
    1.38 +  val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
    1.39    val discriminate_value : hol_context -> styp -> term -> term
    1.40    val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term
    1.41    val construct_value : theory -> styp -> term list -> term
    1.42 @@ -176,8 +180,8 @@
    1.43    val equational_fun_axioms : hol_context -> styp -> term list
    1.44    val is_equational_fun_surely_complete : hol_context -> styp -> bool
    1.45    val merge_type_vars_in_terms : term list -> term list
    1.46 -  val ground_types_in_type : hol_context -> typ -> typ list
    1.47 -  val ground_types_in_terms : hol_context -> term list -> typ list
    1.48 +  val ground_types_in_type : hol_context -> bool -> typ -> typ list
    1.49 +  val ground_types_in_terms : hol_context -> bool -> term list -> typ list
    1.50    val format_type : int list -> int list -> typ -> typ
    1.51    val format_term_type :
    1.52      theory -> const_table -> (term option * int list) list -> term -> typ
    1.53 @@ -376,23 +380,23 @@
    1.54     (@{const_name ord_fun_inst.less_eq_fun}, 2)]
    1.55  
    1.56  (* typ -> typ *)
    1.57 -fun unbit_type @{typ "unsigned_bit word"} = nat_T
    1.58 -  | unbit_type @{typ "signed_bit word"} = int_T
    1.59 -  | unbit_type @{typ bisim_iterator} = nat_T
    1.60 -  | unbit_type (Type (s, Ts as _ :: _)) = Type (s, map unbit_type Ts)
    1.61 -  | unbit_type T = T
    1.62 -fun unbit_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
    1.63 -    unbit_and_unbox_type (Type ("fun", Ts))
    1.64 -  | unbit_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
    1.65 -    Type ("*", map unbit_and_unbox_type Ts)
    1.66 -  | unbit_and_unbox_type @{typ "unsigned_bit word"} = nat_T
    1.67 -  | unbit_and_unbox_type @{typ "signed_bit word"} = int_T
    1.68 -  | unbit_and_unbox_type @{typ bisim_iterator} = nat_T
    1.69 -  | unbit_and_unbox_type (Type (s, Ts as _ :: _)) =
    1.70 -    Type (s, map unbit_and_unbox_type Ts)
    1.71 -  | unbit_and_unbox_type T = T
    1.72 +fun unarize_type @{typ "unsigned_bit word"} = nat_T
    1.73 +  | unarize_type @{typ "signed_bit word"} = int_T
    1.74 +  | unarize_type @{typ bisim_iterator} = nat_T
    1.75 +  | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
    1.76 +  | unarize_type T = T
    1.77 +fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
    1.78 +    unarize_and_unbox_type (Type ("fun", Ts))
    1.79 +  | unarize_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
    1.80 +    Type ("*", map unarize_and_unbox_type Ts)
    1.81 +  | unarize_and_unbox_type @{typ "unsigned_bit word"} = nat_T
    1.82 +  | unarize_and_unbox_type @{typ "signed_bit word"} = int_T
    1.83 +  | unarize_and_unbox_type @{typ bisim_iterator} = nat_T
    1.84 +  | unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
    1.85 +    Type (s, map unarize_and_unbox_type Ts)
    1.86 +  | unarize_and_unbox_type T = T
    1.87  (* Proof.context -> typ -> string *)
    1.88 -fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbit_and_unbox_type
    1.89 +fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
    1.90  
    1.91  (* string -> string -> string *)
    1.92  val prefix_name = Long_Name.qualify o Long_Name.base_name
    1.93 @@ -692,7 +696,7 @@
    1.94    member (op =) [@{const_name FunBox}, @{const_name PairBox},
    1.95                   @{const_name Quot}, @{const_name Zero_Rep},
    1.96                   @{const_name Suc_Rep}] s orelse
    1.97 -  let val (x as (s, T)) = (s, unbit_and_unbox_type T) in
    1.98 +  let val (x as (s, T)) = (s, unarize_and_unbox_type T) in
    1.99      Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
   1.100      (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
   1.101      x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse
   1.102 @@ -703,7 +707,7 @@
   1.103    not (is_coconstr thy x)
   1.104  fun is_constr thy (x as (_, T)) =
   1.105    is_constr_like thy x andalso
   1.106 -  not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) andalso
   1.107 +  not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
   1.108    not (is_stale_constr thy x)
   1.109  (* string -> bool *)
   1.110  val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
   1.111 @@ -757,6 +761,15 @@
   1.112                             else InPair)) Ts)
   1.113    | _ => T
   1.114  
   1.115 +(* typ -> typ *)
   1.116 +fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
   1.117 +  | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
   1.118 +  | binarize_nat_and_int_in_type (Type (s, Ts)) =
   1.119 +    Type (s, map binarize_nat_and_int_in_type Ts)
   1.120 +  | binarize_nat_and_int_in_type T = T
   1.121 +(* term -> term *)
   1.122 +val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
   1.123 +
   1.124  (* styp -> styp *)
   1.125  fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
   1.126  
   1.127 @@ -773,9 +786,10 @@
   1.128    | nth_sel_for_constr (s, T) n =
   1.129      (nth_sel_name_for_constr_name s n,
   1.130       body_type T --> nth (maybe_curried_binder_types T) n)
   1.131 -(* hol_context -> styp -> int -> styp *)
   1.132 -fun boxed_nth_sel_for_constr hol_ctxt =
   1.133 -  apsnd (box_type hol_ctxt InSel) oo nth_sel_for_constr
   1.134 +(* hol_context -> bool -> styp -> int -> styp *)
   1.135 +fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
   1.136 +  apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
   1.137 +  oo nth_sel_for_constr
   1.138  
   1.139  (* string -> int *)
   1.140  fun sel_no_from_name s =
   1.141 @@ -876,8 +890,10 @@
   1.142      let val xs = uncached_datatype_constrs thy T in
   1.143        (Unsynchronized.change constr_cache (cons (T, xs)); xs)
   1.144      end
   1.145 -fun boxed_datatype_constrs hol_ctxt =
   1.146 -  map (apsnd (box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
   1.147 +(* hol_context -> bool -> typ -> styp list *)
   1.148 +fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
   1.149 +  map (apsnd ((binarize ? binarize_nat_and_int_in_type)
   1.150 +              o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
   1.151  (* hol_context -> typ -> int *)
   1.152  val num_datatype_constrs = length oo datatype_constrs
   1.153  
   1.154 @@ -885,10 +901,12 @@
   1.155  fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
   1.156    | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
   1.157    | constr_name_for_sel_like s' = original_name s'
   1.158 -(* hol_context -> styp -> styp *)
   1.159 -fun boxed_constr_for_sel hol_ctxt (s', T') =
   1.160 +(* hol_context -> bool -> styp -> styp *)
   1.161 +fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
   1.162    let val s = constr_name_for_sel_like s' in
   1.163 -    AList.lookup (op =) (boxed_datatype_constrs hol_ctxt (domain_type T')) s
   1.164 +    AList.lookup (op =)
   1.165 +        (binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T'))
   1.166 +        s
   1.167      |> the |> pair s
   1.168    end
   1.169  
   1.170 @@ -2013,28 +2031,33 @@
   1.171        | coalesce T = T
   1.172    in map (map_types (map_atyps coalesce)) ts end
   1.173  
   1.174 -(* hol_context -> typ -> typ list -> typ list *)
   1.175 -fun add_ground_types hol_ctxt T accum =
   1.176 -  case T of
   1.177 -    Type ("fun", Ts) => fold (add_ground_types hol_ctxt) Ts accum
   1.178 -  | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
   1.179 -  | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
   1.180 -  | Type (_, Ts) =>
   1.181 -    if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
   1.182 -      accum
   1.183 -    else
   1.184 -      T :: accum
   1.185 -      |> fold (add_ground_types hol_ctxt)
   1.186 -              (case boxed_datatype_constrs hol_ctxt T of
   1.187 -                 [] => Ts
   1.188 -               | xs => map snd xs)
   1.189 -  | _ => insert (op =) T accum
   1.190 +(* hol_context -> bool -> typ -> typ list -> typ list *)
   1.191 +fun add_ground_types hol_ctxt binarize =
   1.192 +  let
   1.193 +    fun aux T accum =
   1.194 +      case T of
   1.195 +        Type ("fun", Ts) => fold aux Ts accum
   1.196 +      | Type ("*", Ts) => fold aux Ts accum
   1.197 +      | Type (@{type_name itself}, [T1]) => aux T1 accum
   1.198 +      | Type (_, Ts) =>
   1.199 +        if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
   1.200 +                  T then
   1.201 +          accum
   1.202 +        else
   1.203 +          T :: accum
   1.204 +          |> fold aux (case binarized_and_boxed_datatype_constrs hol_ctxt
   1.205 +                                                                 binarize T of
   1.206 +                         [] => Ts
   1.207 +                       | xs => map snd xs)
   1.208 +      | _ => insert (op =) T accum
   1.209 +  in aux end
   1.210  
   1.211 -(* hol_context -> typ -> typ list *)
   1.212 -fun ground_types_in_type hol_ctxt T = add_ground_types hol_ctxt T []
   1.213 +(* hol_context -> bool -> typ -> typ list *)
   1.214 +fun ground_types_in_type hol_ctxt binarize T =
   1.215 +  add_ground_types hol_ctxt binarize T []
   1.216  (* hol_context -> term list -> typ list *)
   1.217 -fun ground_types_in_terms hol_ctxt ts =
   1.218 -  fold (fold_types (add_ground_types hol_ctxt)) ts []
   1.219 +fun ground_types_in_terms hol_ctxt binarize ts =
   1.220 +  fold (fold_types (add_ground_types hol_ctxt binarize)) ts []
   1.221  
   1.222  (* theory -> const_table -> styp -> int list *)
   1.223  fun const_format thy def_table (x as (s, T)) =
   1.224 @@ -2082,7 +2105,7 @@
   1.225  (* int list -> int list -> typ -> typ *)
   1.226  fun format_type default_format format T =
   1.227    let
   1.228 -    val T = unbit_and_unbox_type T
   1.229 +    val T = unarize_and_unbox_type T
   1.230      val format = format |> filter (curry (op <) 0)
   1.231    in
   1.232      if forall (curry (op =) 1) format then
   1.233 @@ -2121,7 +2144,7 @@
   1.234             (* term -> term *)
   1.235             val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
   1.236             val (x' as (_, T'), js, ts) =
   1.237 -             AList.find (op =) (!special_funs) (s, unbit_and_unbox_type T)
   1.238 +             AList.find (op =) (!special_funs) (s, unarize_and_unbox_type T)
   1.239               |> the_single
   1.240             val max_j = List.last js
   1.241             val Ts = List.take (binder_types T', max_j + 1)
   1.242 @@ -2211,7 +2234,7 @@
   1.243           let val t = Const (original_name s, T) in
   1.244             (t, format_term_type thy def_table formats t)
   1.245           end)
   1.246 -      |>> map_types unbit_and_unbox_type
   1.247 +      |>> map_types unarize_and_unbox_type
   1.248        |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
   1.249    in do_const end
   1.250