have Nitpick lookup codatatypes
authorblanchet
Mon Jan 20 19:51:56 2014 +0100 (2014-01-20)
changeset 55080b7c41accbff2
parent 55079 ec08a67e993b
child 55081 45c457a6b987
have Nitpick lookup codatatypes
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Jan 20 19:05:25 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Jan 20 19:51:56 2014 +0100
     1.3 @@ -110,7 +110,6 @@
     1.4    val strip_n_binders : int -> typ -> typ list * typ
     1.5    val nth_range_type : int -> typ -> typ
     1.6    val num_factors_in_type : typ -> int
     1.7 -  val num_binder_types : typ -> int
     1.8    val curried_binder_types : typ -> typ list
     1.9    val mk_flat_tuple : typ -> term list -> term
    1.10    val dest_n_tuple : int -> term -> term list
    1.11 @@ -293,6 +292,7 @@
    1.12  datatype boxability =
    1.13    InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
    1.14  
    1.15 +(* FIXME: Get rid of 'codatatypes' and related functionality *)
    1.16  structure Data = Generic_Data
    1.17  (
    1.18    type T = {frac_types: (string * (string * string) list) list,
    1.19 @@ -543,9 +543,6 @@
    1.20  fun num_factors_in_type (Type (@{type_name prod}, [T1, T2])) =
    1.21      fold (Integer.add o num_factors_in_type) [T1, T2] 0
    1.22    | num_factors_in_type _ = 1
    1.23 -fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
    1.24 -    1 + num_binder_types T2
    1.25 -  | num_binder_types _ = 0
    1.26  val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
    1.27  fun maybe_curried_binder_types T =
    1.28    (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
    1.29 @@ -595,8 +592,8 @@
    1.30                   @{type_name int}, @{type_name natural}, @{type_name integer}] s orelse
    1.31    (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
    1.32  
    1.33 -fun repair_constr_type thy body_T' T =
    1.34 -  varify_and_instantiate_type_global thy (body_type T) body_T' T
    1.35 +fun repair_constr_type (Type (_, Ts)) T =
    1.36 +  snd (dest_Const (Ctr_Sugar.mk_ctr Ts (Const (Name.uu, T))))
    1.37  
    1.38  fun register_frac_type_generic frac_s ersaetze generic =
    1.39    let
    1.40 @@ -627,39 +624,41 @@
    1.41    register_ersatz_generic ersatz
    1.42  val register_ersatz_global = Context.theory_map o register_ersatz_generic
    1.43  
    1.44 -fun register_codatatype_generic co_T case_name constr_xs generic =
    1.45 +fun register_codatatype_generic coT case_name constr_xs generic =
    1.46    let
    1.47      val thy = Context.theory_of generic
    1.48      val {frac_types, ersatz_table, codatatypes} = Data.get generic
    1.49 -    val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
    1.50 -    val (co_s, co_Ts) = dest_Type co_T
    1.51 +    val constr_xs = map (apsnd (repair_constr_type coT)) constr_xs
    1.52 +    val (co_s, coTs) = dest_Type coT
    1.53      val _ =
    1.54 -      if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
    1.55 +      if forall is_TFree coTs andalso not (has_duplicates (op =) coTs) andalso
    1.56           co_s <> @{type_name fun} andalso
    1.57           not (is_basic_datatype thy [(NONE, true)] co_s) then
    1.58          ()
    1.59        else
    1.60 -        raise TYPE ("Nitpick_HOL.register_codatatype_generic", [co_T], [])
    1.61 +        raise TYPE ("Nitpick_HOL.register_codatatype_generic", [coT], [])
    1.62      val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
    1.63                                     codatatypes
    1.64    in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
    1.65                 codatatypes = codatatypes} generic end
    1.66  (* TODO: Consider morphism. *)
    1.67 -fun register_codatatype co_T case_name constr_xs (_ : morphism) =
    1.68 -  register_codatatype_generic co_T case_name constr_xs
    1.69 +fun register_codatatype coT case_name constr_xs (_ : morphism) =
    1.70 +  register_codatatype_generic coT case_name constr_xs
    1.71  val register_codatatype_global =
    1.72    Context.theory_map ooo register_codatatype_generic
    1.73  
    1.74 -fun unregister_codatatype_generic co_T = register_codatatype_generic co_T "" []
    1.75 +fun unregister_codatatype_generic coT = register_codatatype_generic coT "" []
    1.76  (* TODO: Consider morphism. *)
    1.77 -fun unregister_codatatype co_T (_ : morphism) =
    1.78 -  unregister_codatatype_generic co_T
    1.79 +fun unregister_codatatype coT (_ : morphism) =
    1.80 +  unregister_codatatype_generic coT
    1.81  val unregister_codatatype_global =
    1.82    Context.theory_map o unregister_codatatype_generic
    1.83  
    1.84  fun is_codatatype ctxt (Type (s, _)) =
    1.85 -    s |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
    1.86 -      |> Option.map snd |> these |> null |> not
    1.87 +    Option.map #fp (BNF_FP_Def_Sugar.fp_sugar_of ctxt s)
    1.88 +        = SOME BNF_FP_Util.Greatest_FP orelse
    1.89 +    not (null (these (Option.map snd (AList.lookup (op =)
    1.90 +                            (#codatatypes (Data.get (Context.Proof ctxt))) s))))
    1.91    | is_codatatype _ _ = false
    1.92  fun is_registered_type ctxt T = is_frac_type ctxt T orelse is_codatatype ctxt T
    1.93  fun is_real_quot_type ctxt (Type (s, _)) =
    1.94 @@ -782,15 +781,24 @@
    1.95      raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
    1.96  
    1.97  fun is_coconstr ctxt (s, T) =
    1.98 -  let val thy = Proof_Context.theory_of ctxt in
    1.99 -    case body_type T of
   1.100 -      co_T as Type (co_s, _) =>
   1.101 -      let val {codatatypes, ...} = Data.get (Context.Proof ctxt) in
   1.102 -        exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T)
   1.103 -               (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
   1.104 -      end
   1.105 -    | _ => false
   1.106 -  end
   1.107 +  case body_type T of
   1.108 +    coT as Type (co_s, _) =>
   1.109 +    let
   1.110 +      val ctrs1 =
   1.111 +        co_s
   1.112 +        |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
   1.113 +        |> Option.map snd |> these
   1.114 +      val ctrs2 =
   1.115 +        (case BNF_FP_Def_Sugar.fp_sugar_of ctxt co_s of
   1.116 +           SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) =>
   1.117 +           map dest_Const
   1.118 +               (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar))
   1.119 +         | _ => [])
   1.120 +    in
   1.121 +      exists (fn (s', T') => s = s' andalso repair_constr_type coT T' = T)
   1.122 +             (ctrs1 @ ctrs2)
   1.123 +    end
   1.124 +  | _ => false
   1.125  fun is_constr_like ctxt (s, T) =
   1.126    member (op =) [@{const_name FunBox}, @{const_name PairBox},
   1.127                   @{const_name Quot}, @{const_name Zero_Rep},
   1.128 @@ -924,44 +932,49 @@
   1.129                                (T as Type (s, Ts)) =
   1.130      (case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
   1.131                         s of
   1.132 -       SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
   1.133 +       SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type T)) xs'
   1.134       | _ =>
   1.135 -       if is_frac_type ctxt T then
   1.136 -         case typedef_info ctxt s of
   1.137 -           SOME {abs_type, rep_type, Abs_name, ...} =>
   1.138 -           [(Abs_name,
   1.139 -             varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
   1.140 -         | NONE => [] (* impossible *)
   1.141 -       else if is_datatype ctxt stds T then
   1.142 -         case Datatype.get_info thy s of
   1.143 -           SOME {index, descr, ...} =>
   1.144 -           let
   1.145 -             val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
   1.146 -           in
   1.147 -             map (apsnd (fn Us =>
   1.148 -                            map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
   1.149 -                 constrs
   1.150 -           end
   1.151 -         | NONE =>
   1.152 -           if is_record_type T then
   1.153 -             let
   1.154 -               val s' = unsuffix Record.ext_typeN s ^ Record.extN
   1.155 -               val T' = (Record.get_extT_fields thy T
   1.156 -                        |> apsnd single |> uncurry append |> map snd) ---> T
   1.157 -             in [(s', T')] end
   1.158 -           else if is_real_quot_type ctxt T then
   1.159 -             [(@{const_name Quot}, rep_type_for_quot_type ctxt T --> T)]
   1.160 -           else case typedef_info ctxt s of
   1.161 -             SOME {abs_type, rep_type, Abs_name, ...} =>
   1.162 -             [(Abs_name,
   1.163 -               varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
   1.164 -           | NONE =>
   1.165 -             if T = @{typ ind} then
   1.166 -               [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
   1.167 -             else
   1.168 -               []
   1.169 -       else
   1.170 -         [])
   1.171 +       (case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of
   1.172 +          SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) =>
   1.173 +          map (apsnd (repair_constr_type T) o dest_Const)
   1.174 +              (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar))
   1.175 +        | _ =>
   1.176 +          if is_frac_type ctxt T then
   1.177 +            case typedef_info ctxt s of
   1.178 +              SOME {abs_type, rep_type, Abs_name, ...} =>
   1.179 +              [(Abs_name,
   1.180 +                varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
   1.181 +            | NONE => [] (* impossible *)
   1.182 +          else if is_datatype ctxt stds T then
   1.183 +            case Datatype.get_info thy s of
   1.184 +              SOME {index, descr, ...} =>
   1.185 +              let
   1.186 +                val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
   1.187 +              in
   1.188 +                map (apsnd (fn Us =>
   1.189 +                               map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
   1.190 +                    constrs
   1.191 +              end
   1.192 +            | NONE =>
   1.193 +              if is_record_type T then
   1.194 +                let
   1.195 +                  val s' = unsuffix Record.ext_typeN s ^ Record.extN
   1.196 +                  val T' = (Record.get_extT_fields thy T
   1.197 +                           |> apsnd single |> uncurry append |> map snd) ---> T
   1.198 +                in [(s', T')] end
   1.199 +              else if is_real_quot_type ctxt T then
   1.200 +                [(@{const_name Quot}, rep_type_for_quot_type ctxt T --> T)]
   1.201 +              else case typedef_info ctxt s of
   1.202 +                SOME {abs_type, rep_type, Abs_name, ...} =>
   1.203 +                [(Abs_name,
   1.204 +                  varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
   1.205 +              | NONE =>
   1.206 +                if T = @{typ ind} then
   1.207 +                  [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
   1.208 +                else
   1.209 +                  []
   1.210 +          else
   1.211 +            []))
   1.212    | uncached_datatype_constrs _ _ = []
   1.213  fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
   1.214    case AList.lookup (op =) (!constr_cache) T of
   1.215 @@ -1451,7 +1464,13 @@
   1.216                        cons (case_name, AList.lookup (op =) descr index
   1.217                                         |> the |> #3 |> length))
   1.218                  (Datatype.get_all thy) [] @
   1.219 -    map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt)))
   1.220 +    map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) @
   1.221 +    maps (fn {fp, ctr_sugars, ...} =>
   1.222 +             if fp = BNF_FP_Util.Greatest_FP then
   1.223 +               map (apsnd num_binder_types o dest_Const o #casex) ctr_sugars
   1.224 +             else
   1.225 +               [])
   1.226 +         (BNF_FP_Def_Sugar.fp_sugars_of ctxt)
   1.227    end
   1.228  
   1.229  fun fixpoint_kind_of_const thy table x =
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Jan 20 19:05:25 2014 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Jan 20 19:51:56 2014 +0100
     2.3 @@ -60,6 +60,7 @@
     2.4    val nat_T : typ
     2.5    val int_T : typ
     2.6    val simple_string_of_typ : typ -> string
     2.7 +  val num_binder_types : typ -> int
     2.8    val is_real_constr : theory -> string * typ -> bool
     2.9    val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
    2.10    val varify_type : Proof.context -> typ -> typ
    2.11 @@ -253,10 +254,12 @@
    2.12  val nat_T = @{typ nat}
    2.13  val int_T = @{typ int}
    2.14  
    2.15 -fun simple_string_of_typ (Type (s, _))     = s
    2.16 -  | simple_string_of_typ (TFree (s, _))    = s
    2.17 +fun simple_string_of_typ (Type (s, _)) = s
    2.18 +  | simple_string_of_typ (TFree (s, _)) = s
    2.19    | simple_string_of_typ (TVar ((s, _), _)) = s
    2.20  
    2.21 +val num_binder_types = BNF_Util.num_binder_types
    2.22 +
    2.23  fun is_real_constr thy (s, T) =
    2.24    case body_type T of
    2.25      Type (s', _) =>