support 'datatype_new'-defined datatypes in Nitpick + better support for 'codatatype's
authorblanchet
Mon Mar 03 22:33:22 2014 +0100 (2014-03-03)
changeset 55891d1a9b07783ab
parent 55890 bd7927cca152
child 55892 6fba7f6c532a
support 'datatype_new'-defined datatypes in Nitpick + better support for 'codatatype's
src/HOL/Library/refute.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
     1.1 --- a/src/HOL/Library/refute.ML	Mon Mar 03 22:33:22 2014 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -372,7 +372,15 @@
     1.4  (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
     1.5  (* ------------------------------------------------------------------------- *)
     1.6  
     1.7 -val typ_of_dtyp = Nitpick_Util.typ_of_dtyp
     1.8 +fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) =
     1.9 +    the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a))
    1.10 +  | typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) =
    1.11 +    Type (s, map (typ_of_dtyp descr typ_assoc) Us)
    1.12 +  | typ_of_dtyp descr typ_assoc (Datatype.DtRec i) =
    1.13 +    let val (s, ds, _) = the (AList.lookup (op =) descr i) in
    1.14 +      Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.15 +    end
    1.16 +
    1.17  val close_form = ATP_Util.close_form
    1.18  val monomorphic_term = ATP_Util.monomorphic_term
    1.19  val specialize_type = ATP_Util.specialize_type
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 22:33:22 2014 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 22:33:22 2014 +0100
     2.3 @@ -611,7 +611,7 @@
     2.4    | _ => NONE
     2.5  
     2.6  val is_raw_typedef = is_some oo typedef_info
     2.7 -val is_raw_old_datatype = is_some oo Datatype.get_info
     2.8 +val is_raw_free_datatype = is_some oo Ctr_Sugar.ctr_sugar_of
     2.9  
    2.10  val is_interpreted_type =
    2.11    member (op =) [@{type_name prod}, @{type_name set}, @{type_name bool},
    2.12 @@ -688,13 +688,13 @@
    2.13    Context.theory_map o unregister_codatatype_generic
    2.14  
    2.15  fun is_raw_codatatype ctxt s =
    2.16 +  Option.map #fp (BNF_FP_Def_Sugar.fp_sugar_of ctxt s)
    2.17 +  = SOME BNF_Util.Greatest_FP
    2.18 +
    2.19 +fun is_registered_codatatype ctxt s =
    2.20    not (null (these (Option.map snd (AList.lookup (op =)
    2.21      (#codatatypes (Data.get (Context.Proof ctxt))) s))))
    2.22  
    2.23 -fun is_registered_codatatype ctxt s =
    2.24 -  Option.map #fp (BNF_FP_Def_Sugar.fp_sugar_of ctxt s)
    2.25 -  = SOME BNF_Util.Greatest_FP
    2.26 -
    2.27  fun is_codatatype ctxt (Type (s, _)) =
    2.28      is_raw_codatatype ctxt s orelse is_registered_codatatype ctxt s
    2.29    | is_codatatype _ _ = false
    2.30 @@ -712,13 +712,11 @@
    2.31    T <> @{typ int}
    2.32  
    2.33  fun is_pure_typedef ctxt (T as Type (s, _)) =
    2.34 -    let val thy = Proof_Context.theory_of ctxt in
    2.35 -      is_frac_type ctxt T orelse
    2.36 -      (is_raw_typedef ctxt s andalso
    2.37 -       not (is_raw_old_datatype thy s orelse is_raw_quot_type ctxt T orelse
    2.38 -            is_codatatype ctxt T orelse is_record_type T orelse
    2.39 -            is_integer_like_type T))
    2.40 -    end
    2.41 +    is_frac_type ctxt T orelse
    2.42 +    (is_raw_typedef ctxt s andalso
    2.43 +     not (is_raw_free_datatype ctxt s orelse is_raw_quot_type ctxt T orelse
    2.44 +          is_codatatype ctxt T orelse is_record_type T orelse
    2.45 +          is_integer_like_type T))
    2.46    | is_pure_typedef _ _ = false
    2.47  
    2.48  fun is_univ_typedef ctxt (Type (s, _)) =
    2.49 @@ -835,32 +833,29 @@
    2.50    | equiv_relation_for_quot_type _ T =
    2.51      raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
    2.52  
    2.53 -fun is_raw_old_datatype_constr thy (s, T) =
    2.54 +fun is_raw_free_datatype_constr ctxt (s, T) =
    2.55    case body_type T of
    2.56 -    Type (s', _) =>
    2.57 -    (case Datatype.get_constrs thy s' of
    2.58 -       SOME constrs =>
    2.59 -       List.exists (fn (cname, cty) =>
    2.60 -         cname = s andalso Sign.typ_instance thy (T, cty)) constrs
    2.61 -     | NONE => false)
    2.62 +    dtT as Type (dt_s, _) =>
    2.63 +    let
    2.64 +      val ctrs =
    2.65 +        case Ctr_Sugar.ctr_sugar_of ctxt dt_s of
    2.66 +          SOME {ctrs, ...} => map dest_Const ctrs
    2.67 +        | _ => []
    2.68 +    in
    2.69 +      exists (fn (s', T') => s = s' andalso repair_constr_type dtT T' = T) ctrs
    2.70 +    end
    2.71    | _  => false
    2.72  
    2.73 -fun is_coconstr ctxt (s, T) =
    2.74 +fun is_registered_coconstr ctxt (s, T) =
    2.75    case body_type T of
    2.76      coT as Type (co_s, _) =>
    2.77      let
    2.78 -      val ctrs1 =
    2.79 +      val ctrs =
    2.80          co_s
    2.81          |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
    2.82          |> Option.map snd |> these
    2.83 -      val ctrs2 =
    2.84 -        (case BNF_FP_Def_Sugar.fp_sugar_of ctxt co_s of
    2.85 -           SOME (fp_sugar as {fp = BNF_Util.Greatest_FP, ...}) =>
    2.86 -           map dest_Const (#ctrs (#ctr_sugar fp_sugar))
    2.87 -         | _ => [])
    2.88      in
    2.89 -      exists (fn (s', T') => s = s' andalso repair_constr_type coT T' = T)
    2.90 -             (ctrs1 @ ctrs2)
    2.91 +      exists (fn (s', T') => s = s' andalso repair_constr_type coT T' = T) ctrs
    2.92      end
    2.93    | _ => false
    2.94  
    2.95 @@ -868,13 +863,10 @@
    2.96    member (op =) [@{const_name FunBox}, @{const_name PairBox},
    2.97                   @{const_name Quot}, @{const_name Zero_Rep},
    2.98                   @{const_name Suc_Rep}] s orelse
    2.99 -  let
   2.100 -    val thy = Proof_Context.theory_of ctxt
   2.101 -    val (x as (_, T)) = (s, unarize_unbox_etc_type T)
   2.102 -  in
   2.103 -    is_raw_old_datatype_constr thy x orelse is_record_constr x orelse
   2.104 +  let val (x as (_, T)) = (s, unarize_unbox_etc_type T) in
   2.105 +    is_raw_free_datatype_constr ctxt x orelse is_record_constr x orelse
   2.106      (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
   2.107 -    is_coconstr ctxt x
   2.108 +    is_registered_coconstr ctxt x
   2.109    end
   2.110  
   2.111  fun is_free_constr ctxt (s, T) =
   2.112 @@ -885,7 +877,7 @@
   2.113  
   2.114  fun is_stale_constr ctxt (x as (s, T)) =
   2.115    is_registered_type ctxt (body_type T) andalso is_nonfree_constr ctxt x andalso
   2.116 -  not (s = @{const_name Nitpick.Abs_Frac} orelse is_coconstr ctxt x)
   2.117 +  not (s = @{const_name Nitpick.Abs_Frac} orelse is_registered_coconstr ctxt x)
   2.118  
   2.119  fun is_constr ctxt (x as (_, T)) =
   2.120    is_nonfree_constr ctxt x andalso
   2.121 @@ -1004,47 +996,36 @@
   2.122                         s of
   2.123         SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type T)) xs'
   2.124       | _ =>
   2.125 -       (case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of
   2.126 -          SOME (fp_sugar as {fp = BNF_Util.Greatest_FP, ...}) =>
   2.127 -          map (apsnd (repair_constr_type T) o dest_Const)
   2.128 -              (#ctrs (#ctr_sugar fp_sugar))
   2.129 -        | _ =>
   2.130 -          if is_frac_type ctxt T then
   2.131 -            case typedef_info ctxt s of
   2.132 -              SOME {abs_type, rep_type, Abs_name, ...} =>
   2.133 -              [(Abs_name,
   2.134 -                varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
   2.135 -            | NONE => [] (* impossible *)
   2.136 -          else if is_data_type ctxt T then
   2.137 -            case Datatype.get_info thy s of
   2.138 -              SOME {index, descr, ...} =>
   2.139 -              let
   2.140 -                val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
   2.141 -              in
   2.142 -                map (apsnd (fn Us =>
   2.143 -                               map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
   2.144 -                    constrs
   2.145 -              end
   2.146 -            | NONE =>
   2.147 -              if is_record_type T then
   2.148 -                let
   2.149 -                  val s' = unsuffix Record.ext_typeN s ^ Record.extN
   2.150 -                  val T' = (Record.get_extT_fields thy T
   2.151 -                           |> apsnd single |> uncurry append |> map snd) ---> T
   2.152 -                in [(s', T')] end
   2.153 -              else if is_raw_quot_type ctxt T then
   2.154 -                [(@{const_name Quot}, rep_type_for_quot_type ctxt T --> T)]
   2.155 -              else case typedef_info ctxt s of
   2.156 -                SOME {abs_type, rep_type, Abs_name, ...} =>
   2.157 -                [(Abs_name,
   2.158 -                  varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
   2.159 -              | NONE =>
   2.160 -                if T = @{typ ind} then
   2.161 -                  [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
   2.162 -                else
   2.163 -                  []
   2.164 -          else
   2.165 -            []))
   2.166 +       if is_frac_type ctxt T then
   2.167 +         case typedef_info ctxt s of
   2.168 +           SOME {abs_type, rep_type, Abs_name, ...} =>
   2.169 +           [(Abs_name,
   2.170 +             varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
   2.171 +         | NONE => [] (* impossible *)
   2.172 +       else if is_data_type ctxt T then
   2.173 +         case Ctr_Sugar.ctr_sugar_of ctxt s of
   2.174 +           SOME {ctrs, ...} =>
   2.175 +           map (apsnd (repair_constr_type T) o dest_Const) ctrs
   2.176 +         | NONE =>
   2.177 +           if is_record_type T then
   2.178 +             let
   2.179 +               val s' = unsuffix Record.ext_typeN s ^ Record.extN
   2.180 +               val T' = (Record.get_extT_fields thy T
   2.181 +                        |> apsnd single |> uncurry append |> map snd) ---> T
   2.182 +             in [(s', T')] end
   2.183 +           else if is_raw_quot_type ctxt T then
   2.184 +             [(@{const_name Quot}, rep_type_for_quot_type ctxt T --> T)]
   2.185 +           else case typedef_info ctxt s of
   2.186 +             SOME {abs_type, rep_type, Abs_name, ...} =>
   2.187 +             [(Abs_name,
   2.188 +               varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
   2.189 +           | NONE =>
   2.190 +             if T = @{typ ind} then
   2.191 +               [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
   2.192 +             else
   2.193 +               []
   2.194 +       else
   2.195 +         [])
   2.196    | uncached_data_type_constrs _ _ = []
   2.197  
   2.198  fun data_type_constrs (hol_ctxt as {constr_cache, ...}) T =
   2.199 @@ -1524,22 +1505,9 @@
   2.200                 | t => t)
   2.201  
   2.202  fun case_const_names ctxt =
   2.203 -  let val thy = Proof_Context.theory_of ctxt in
   2.204 -    Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
   2.205 -                    if is_interpreted_type dtype_s then
   2.206 -                      I
   2.207 -                    else
   2.208 -                      cons (case_name, AList.lookup (op =) descr index
   2.209 -                                       |> the |> #3 |> length))
   2.210 -                (Datatype.get_all thy) [] @
   2.211 -    map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) @
   2.212 -    map_filter (fn {fp, ctr_sugar = {casex, ...}, ...} =>
   2.213 -                   if fp = BNF_Util.Greatest_FP then
   2.214 -                     SOME (apsnd num_binder_types (dest_Const casex))
   2.215 -                   else
   2.216 -                     NONE)
   2.217 -        (BNF_FP_Def_Sugar.fp_sugars_of ctxt)
   2.218 -  end
   2.219 +  map_filter (fn {casex, ...} => SOME (apsnd (fn T => num_binder_types T - 1) (dest_Const casex)))
   2.220 +      (Ctr_Sugar.ctr_sugars_of ctxt) @
   2.221 +  map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt)))
   2.222  
   2.223  fun fixpoint_kind_of_const thy table x =
   2.224    if is_built_in_const x then NoFp
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Mar 03 22:33:22 2014 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Mar 03 22:33:22 2014 +0100
     3.3 @@ -60,7 +60,6 @@
     3.4    val int_T : typ
     3.5    val simple_string_of_typ : typ -> string
     3.6    val num_binder_types : typ -> int
     3.7 -  val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
     3.8    val varify_type : Proof.context -> typ -> typ
     3.9    val instantiate_type : theory -> typ -> typ -> typ -> typ
    3.10    val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
    3.11 @@ -260,15 +259,6 @@
    3.12  
    3.13  val num_binder_types = BNF_Util.num_binder_types
    3.14  
    3.15 -fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) =
    3.16 -    the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a))
    3.17 -  | typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) =
    3.18 -    Type (s, map (typ_of_dtyp descr typ_assoc) Us)
    3.19 -  | typ_of_dtyp descr typ_assoc (Datatype.DtRec i) =
    3.20 -    let val (s, ds, _) = the (AList.lookup (op =) descr i) in
    3.21 -      Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    3.22 -    end
    3.23 -
    3.24  val varify_type = ATP_Util.varify_type
    3.25  val instantiate_type = ATP_Util.instantiate_type
    3.26  val varify_and_instantiate_type = ATP_Util.varify_and_instantiate_type