src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33581 e1e77265fb1d
parent 33580 45c33e97cb86
child 33583 b5e0909cd5ea
equal deleted inserted replaced
33580:45c33e97cb86 33581:e1e77265fb1d
    85   val is_record_get : theory -> styp -> bool
    85   val is_record_get : theory -> styp -> bool
    86   val is_record_update : theory -> styp -> bool
    86   val is_record_update : theory -> styp -> bool
    87   val is_abs_fun : theory -> styp -> bool
    87   val is_abs_fun : theory -> styp -> bool
    88   val is_rep_fun : theory -> styp -> bool
    88   val is_rep_fun : theory -> styp -> bool
    89   val is_constr : theory -> styp -> bool
    89   val is_constr : theory -> styp -> bool
       
    90   val is_stale_constr : theory -> styp -> bool
    90   val is_sel : string -> bool
    91   val is_sel : string -> bool
    91   val discr_for_constr : styp -> styp
    92   val discr_for_constr : styp -> styp
    92   val num_sels_for_constr_type : typ -> int
    93   val num_sels_for_constr_type : typ -> int
    93   val nth_sel_name_for_constr_name : string -> int -> string
    94   val nth_sel_name_for_constr_name : string -> int -> string
    94   val nth_sel_for_constr : styp -> int -> styp
    95   val nth_sel_for_constr : styp -> int -> styp
   610     orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
   611     orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
   611     orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}]
   612     orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}]
   612     orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
   613     orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
   613     orelse is_coconstr thy x
   614     orelse is_coconstr thy x
   614   end
   615   end
       
   616 fun is_stale_constr thy (x as (_, T)) =
       
   617   is_codatatype thy (body_type T) andalso is_constr_like thy x
       
   618   andalso not (is_coconstr thy x)
   615 fun is_constr thy (x as (_, T)) =
   619 fun is_constr thy (x as (_, T)) =
   616   is_constr_like thy x
   620   is_constr_like thy x
   617   andalso not (is_basic_datatype (fst (dest_Type (body_type T))))
   621   andalso not (is_basic_datatype (fst (dest_Type (body_type T))))
       
   622   andalso not (is_stale_constr thy x)
   618 (* string -> bool *)
   623 (* string -> bool *)
   619 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
   624 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
   620 val is_sel_like_and_no_discr =
   625 val is_sel_like_and_no_discr =
   621   String.isPrefix sel_prefix
   626   String.isPrefix sel_prefix
   622   orf (member (op =) [@{const_name fst}, @{const_name snd}])
   627   orf (member (op =) [@{const_name fst}, @{const_name snd}])
   728 fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
   733 fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
   729 fun suc_const T = Const (@{const_name Suc}, T --> T)
   734 fun suc_const T = Const (@{const_name Suc}, T --> T)
   730 
   735 
   731 (* theory -> typ -> styp list *)
   736 (* theory -> typ -> styp list *)
   732 fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
   737 fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
   733     if is_datatype thy T then
   738     (case AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s of
   734       case Datatype.get_info thy s of
   739        SOME (_, xs' as (_ :: _)) =>
   735         SOME {index, descr, ...} =>
   740        map (apsnd (repair_constr_type thy T)) xs'
   736         let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
   741      | _ =>
   737           map (fn (s', Us) =>
   742        if is_datatype thy T then
   738                   (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
   743          case Datatype.get_info thy s of
   739               constrs
   744            SOME {index, descr, ...} =>
   740          end
   745            let
   741       | NONE =>
   746              val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
   742         case AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s of
   747            in
   743           SOME (_, xs' as (_ :: _)) =>
   748              map (fn (s', Us) =>
   744           map (apsnd (repair_constr_type thy T)) xs'
   749                      (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
   745         | _ =>
   750                           ---> T)) constrs
   746           if is_record_type T then
   751            end
   747             let
   752          | NONE =>
   748               val s' = unsuffix Record.ext_typeN s ^ Record.extN
   753            if is_record_type T then
   749               val T' = (Record.get_extT_fields thy T
   754              let
   750                        |> apsnd single |> uncurry append |> map snd) ---> T
   755                val s' = unsuffix Record.ext_typeN s ^ Record.extN
   751             in [(s', T')] end
   756                val T' = (Record.get_extT_fields thy T
   752           else case typedef_info thy s of
   757                         |> apsnd single |> uncurry append |> map snd) ---> T
   753             SOME {abs_type, rep_type, Abs_name, ...} =>
   758              in [(s', T')] end
   754             [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
   759            else case typedef_info thy s of
   755           | NONE =>
   760              SOME {abs_type, rep_type, Abs_name, ...} =>
   756             if T = @{typ ind} then
   761              [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
   757               [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
   762            | NONE =>
   758             else
   763              if T = @{typ ind} then
   759               []
   764                [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
   760     else
   765              else
   761       []
   766                []
       
   767        else
       
   768          [])
   762   | uncached_datatype_constrs _ _ = []
   769   | uncached_datatype_constrs _ _ = []
   763 (* extended_context -> typ -> styp list *)
   770 (* extended_context -> typ -> styp list *)
   764 fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
   771 fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
   765                      T =
   772                      T =
   766   case AList.lookup (op =) (!constr_cache) T of
   773   case AList.lookup (op =) (!constr_cache) T of
  1500                  |> do_term (depth + 1) Ts, ts)
  1507                  |> do_term (depth + 1) Ts, ts)
  1501               end
  1508               end
  1502             | _ =>
  1509             | _ =>
  1503               if is_constr thy x then
  1510               if is_constr thy x then
  1504                 (Const x, ts)
  1511                 (Const x, ts)
       
  1512               else if is_stale_constr thy x then
       
  1513                 raise NOT_SUPPORTED ("(non-co-)constructors of codatatypes \
       
  1514                                      \(\"" ^ s ^ "\")")
  1505               else if is_record_get thy x then
  1515               else if is_record_get thy x then
  1506                 case length ts of
  1516                 case length ts of
  1507                   0 => (do_term depth Ts (eta_expand Ts t 1), [])
  1517                   0 => (do_term depth Ts (eta_expand Ts t 1), [])
  1508                 | _ => (optimized_record_get ext_ctxt s (domain_type T)
  1518                 | _ => (optimized_record_get ext_ctxt s (domain_type T)
  1509                                              (range_type T) (hd ts), tl ts)
  1519                                              (range_type T) (hd ts), tl ts)