src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 41898 55d981e1232a
parent 41876 03f699556955
child 41994 c567c860caf6
equal deleted inserted replaced
41897:c24e7fd17464 41898:55d981e1232a
   165   val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
   165   val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
   166   val bounded_exact_card_of_type :
   166   val bounded_exact_card_of_type :
   167     hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
   167     hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
   168   val typical_card_of_type : typ -> int
   168   val typical_card_of_type : typ -> int
   169   val is_finite_type : hol_context -> typ -> bool
   169   val is_finite_type : hol_context -> typ -> bool
   170   val is_small_finite_type : hol_context -> typ -> bool
       
   171   val is_special_eligible_arg : bool -> typ list -> term -> bool
   170   val is_special_eligible_arg : bool -> typ list -> term -> bool
   172   val s_let :
   171   val s_let :
   173     typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
   172     typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
   174   val s_betapply : typ list -> term * term -> term
   173   val s_betapply : typ list -> term * term -> term
   175   val s_betapplys : typ list -> term * term list -> term
   174   val s_betapplys : typ list -> term * term list -> term
  1027       handle SAME () =>
  1026       handle SAME () =>
  1028              AList.lookup (op =) assigns T |> the_default default_card
  1027              AList.lookup (op =) assigns T |> the_default default_card
  1029   in Int.min (max, aux [] T) end
  1028   in Int.min (max, aux [] T) end
  1030 
  1029 
  1031 val typical_atomic_card = 4
  1030 val typical_atomic_card = 4
  1032 val typical_card_of_type = bounded_card_of_type 65536 typical_atomic_card []
  1031 val typical_card_of_type = bounded_card_of_type 16777217 typical_atomic_card []
  1033 
       
  1034 val small_type_max_card = 5
       
  1035 
  1032 
  1036 fun is_finite_type hol_ctxt T =
  1033 fun is_finite_type hol_ctxt T =
  1037   bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
  1034   bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
  1038 fun is_small_finite_type hol_ctxt T =
       
  1039   let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
       
  1040     n > 0 andalso n <= small_type_max_card
       
  1041   end
       
  1042 
  1035 
  1043 fun is_special_eligible_arg strict Ts t =
  1036 fun is_special_eligible_arg strict Ts t =
  1044   case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of
  1037   case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of
  1045     [] => true
  1038     [] => true
  1046   | bad_Ts =>
  1039   | bad_Ts =>
  1047     let
  1040     let
  1048       val bad_Ts_cost = fold (Integer.max o typical_card_of_type) bad_Ts 0
  1041       val bad_Ts_cost =
       
  1042         if strict then fold (curry (op *) o typical_card_of_type) bad_Ts 1
       
  1043         else fold (Integer.max o typical_card_of_type) bad_Ts 0
  1049       val T_cost = typical_card_of_type (fastype_of1 (Ts, t))
  1044       val T_cost = typical_card_of_type (fastype_of1 (Ts, t))
  1050     in (bad_Ts_cost, T_cost) |> (if strict then op < else op <=) end
  1045     in (bad_Ts_cost, T_cost) |> (if strict then op < else op <=) end
  1051 
  1046 
  1052 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
  1047 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
  1053 
  1048