# HG changeset patch # User blanchet # Date 1390243916 -3600 # Node ID b7c41accbff2d246078ee4a0a7e1d035baa157f4 # Parent ec08a67e993b45f52621b685eb435b45af59102e have Nitpick lookup codatatypes diff -r ec08a67e993b -r b7c41accbff2 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Jan 20 19:05:25 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Jan 20 19:51:56 2014 +0100 @@ -110,7 +110,6 @@ val strip_n_binders : int -> typ -> typ list * typ val nth_range_type : int -> typ -> typ val num_factors_in_type : typ -> int - val num_binder_types : typ -> int val curried_binder_types : typ -> typ list val mk_flat_tuple : typ -> term list -> term val dest_n_tuple : int -> term -> term list @@ -293,6 +292,7 @@ datatype boxability = InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2 +(* FIXME: Get rid of 'codatatypes' and related functionality *) structure Data = Generic_Data ( type T = {frac_types: (string * (string * string) list) list, @@ -543,9 +543,6 @@ fun num_factors_in_type (Type (@{type_name prod}, [T1, T2])) = fold (Integer.add o num_factors_in_type) [T1, T2] 0 | num_factors_in_type _ = 1 -fun num_binder_types (Type (@{type_name fun}, [_, T2])) = - 1 + num_binder_types T2 - | num_binder_types _ = 0 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types fun maybe_curried_binder_types T = (if is_pair_type (body_type T) then binder_types else curried_binder_types) T @@ -595,8 +592,8 @@ @{type_name int}, @{type_name natural}, @{type_name integer}] s orelse (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T) -fun repair_constr_type thy body_T' T = - varify_and_instantiate_type_global thy (body_type T) body_T' T +fun repair_constr_type (Type (_, Ts)) T = + snd (dest_Const (Ctr_Sugar.mk_ctr Ts (Const (Name.uu, T)))) fun register_frac_type_generic frac_s ersaetze generic = let @@ -627,39 +624,41 @@ register_ersatz_generic ersatz val register_ersatz_global = Context.theory_map o register_ersatz_generic -fun register_codatatype_generic co_T case_name constr_xs generic = +fun register_codatatype_generic coT case_name constr_xs generic = let val thy = Context.theory_of generic val {frac_types, ersatz_table, codatatypes} = Data.get generic - val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs - val (co_s, co_Ts) = dest_Type co_T + val constr_xs = map (apsnd (repair_constr_type coT)) constr_xs + val (co_s, coTs) = dest_Type coT val _ = - if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso + if forall is_TFree coTs andalso not (has_duplicates (op =) coTs) andalso co_s <> @{type_name fun} andalso not (is_basic_datatype thy [(NONE, true)] co_s) then () else - raise TYPE ("Nitpick_HOL.register_codatatype_generic", [co_T], []) + raise TYPE ("Nitpick_HOL.register_codatatype_generic", [coT], []) val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) codatatypes in Data.put {frac_types = frac_types, ersatz_table = ersatz_table, codatatypes = codatatypes} generic end (* TODO: Consider morphism. *) -fun register_codatatype co_T case_name constr_xs (_ : morphism) = - register_codatatype_generic co_T case_name constr_xs +fun register_codatatype coT case_name constr_xs (_ : morphism) = + register_codatatype_generic coT case_name constr_xs val register_codatatype_global = Context.theory_map ooo register_codatatype_generic -fun unregister_codatatype_generic co_T = register_codatatype_generic co_T "" [] +fun unregister_codatatype_generic coT = register_codatatype_generic coT "" [] (* TODO: Consider morphism. *) -fun unregister_codatatype co_T (_ : morphism) = - unregister_codatatype_generic co_T +fun unregister_codatatype coT (_ : morphism) = + unregister_codatatype_generic coT val unregister_codatatype_global = Context.theory_map o unregister_codatatype_generic fun is_codatatype ctxt (Type (s, _)) = - s |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt))) - |> Option.map snd |> these |> null |> not + Option.map #fp (BNF_FP_Def_Sugar.fp_sugar_of ctxt s) + = SOME BNF_FP_Util.Greatest_FP orelse + not (null (these (Option.map snd (AList.lookup (op =) + (#codatatypes (Data.get (Context.Proof ctxt))) s)))) | is_codatatype _ _ = false fun is_registered_type ctxt T = is_frac_type ctxt T orelse is_codatatype ctxt T fun is_real_quot_type ctxt (Type (s, _)) = @@ -782,15 +781,24 @@ raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], []) fun is_coconstr ctxt (s, T) = - let val thy = Proof_Context.theory_of ctxt in - case body_type T of - co_T as Type (co_s, _) => - let val {codatatypes, ...} = Data.get (Context.Proof ctxt) in - exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T) - (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these) - end - | _ => false - end + case body_type T of + coT as Type (co_s, _) => + let + val ctrs1 = + co_s + |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt))) + |> Option.map snd |> these + val ctrs2 = + (case BNF_FP_Def_Sugar.fp_sugar_of ctxt co_s of + SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) => + map dest_Const + (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar)) + | _ => []) + in + exists (fn (s', T') => s = s' andalso repair_constr_type coT T' = T) + (ctrs1 @ ctrs2) + end + | _ => false fun is_constr_like ctxt (s, T) = member (op =) [@{const_name FunBox}, @{const_name PairBox}, @{const_name Quot}, @{const_name Zero_Rep}, @@ -924,44 +932,49 @@ (T as Type (s, Ts)) = (case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt))) s of - SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs' + SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type T)) xs' | _ => - if is_frac_type ctxt T then - case typedef_info ctxt s of - SOME {abs_type, rep_type, Abs_name, ...} => - [(Abs_name, - varify_and_instantiate_type ctxt abs_type T rep_type --> T)] - | NONE => [] (* impossible *) - else if is_datatype ctxt stds T then - case Datatype.get_info thy s of - SOME {index, descr, ...} => - let - val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the - in - map (apsnd (fn Us => - map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T)) - constrs - end - | NONE => - if is_record_type T then - let - val s' = unsuffix Record.ext_typeN s ^ Record.extN - val T' = (Record.get_extT_fields thy T - |> apsnd single |> uncurry append |> map snd) ---> T - in [(s', T')] end - else if is_real_quot_type ctxt T then - [(@{const_name Quot}, rep_type_for_quot_type ctxt T --> T)] - else case typedef_info ctxt s of - SOME {abs_type, rep_type, Abs_name, ...} => - [(Abs_name, - varify_and_instantiate_type ctxt abs_type T rep_type --> T)] - | NONE => - if T = @{typ ind} then - [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}] - else - [] - else - []) + (case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of + SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) => + map (apsnd (repair_constr_type T) o dest_Const) + (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar)) + | _ => + if is_frac_type ctxt T then + case typedef_info ctxt s of + SOME {abs_type, rep_type, Abs_name, ...} => + [(Abs_name, + varify_and_instantiate_type ctxt abs_type T rep_type --> T)] + | NONE => [] (* impossible *) + else if is_datatype ctxt stds T then + case Datatype.get_info thy s of + SOME {index, descr, ...} => + let + val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the + in + map (apsnd (fn Us => + map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T)) + constrs + end + | NONE => + if is_record_type T then + let + val s' = unsuffix Record.ext_typeN s ^ Record.extN + val T' = (Record.get_extT_fields thy T + |> apsnd single |> uncurry append |> map snd) ---> T + in [(s', T')] end + else if is_real_quot_type ctxt T then + [(@{const_name Quot}, rep_type_for_quot_type ctxt T --> T)] + else case typedef_info ctxt s of + SOME {abs_type, rep_type, Abs_name, ...} => + [(Abs_name, + varify_and_instantiate_type ctxt abs_type T rep_type --> T)] + | NONE => + if T = @{typ ind} then + [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}] + else + [] + else + [])) | uncached_datatype_constrs _ _ = [] fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T = case AList.lookup (op =) (!constr_cache) T of @@ -1451,7 +1464,13 @@ cons (case_name, AList.lookup (op =) descr index |> the |> #3 |> length)) (Datatype.get_all thy) [] @ - map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) + map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) @ + maps (fn {fp, ctr_sugars, ...} => + if fp = BNF_FP_Util.Greatest_FP then + map (apsnd num_binder_types o dest_Const o #casex) ctr_sugars + else + []) + (BNF_FP_Def_Sugar.fp_sugars_of ctxt) end fun fixpoint_kind_of_const thy table x = diff -r ec08a67e993b -r b7c41accbff2 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Jan 20 19:05:25 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Jan 20 19:51:56 2014 +0100 @@ -60,6 +60,7 @@ val nat_T : typ val int_T : typ val simple_string_of_typ : typ -> string + val num_binder_types : typ -> int val is_real_constr : theory -> string * typ -> bool val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ val varify_type : Proof.context -> typ -> typ @@ -253,10 +254,12 @@ val nat_T = @{typ nat} val int_T = @{typ int} -fun simple_string_of_typ (Type (s, _)) = s - | simple_string_of_typ (TFree (s, _)) = s +fun simple_string_of_typ (Type (s, _)) = s + | simple_string_of_typ (TFree (s, _)) = s | simple_string_of_typ (TVar ((s, _), _)) = s +val num_binder_types = BNF_Util.num_binder_types + fun is_real_constr thy (s, T) = case body_type T of Type (s', _) =>