# HG changeset patch # User blanchet # Date 1281087310 -7200 # Node ID 1c7d7eaebdf26dc9ea31204b23b367f01818063c # Parent 8164c91039eafa990d2e695fbc90a1155a1e0fd0 quotient types registered as codatatypes are no longer quotient types diff -r 8164c91039ea -r 1c7d7eaebdf2 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 06 11:33:58 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 06 11:35:10 2010 +0200 @@ -113,8 +113,8 @@ val dest_n_tuple : int -> term -> term list val is_real_datatype : theory -> string -> bool val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool + val is_codatatype : theory -> typ -> bool val is_quot_type : theory -> typ -> bool - val is_codatatype : theory -> typ -> bool val is_pure_typedef : Proof.context -> typ -> bool val is_univ_typedef : Proof.context -> typ -> bool val is_datatype : Proof.context -> (typ option * bool) list -> typ -> bool @@ -640,17 +640,19 @@ in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end fun unregister_codatatype co_T = register_codatatype co_T "" [] -fun is_quot_type thy (Type (s, _)) = - is_some (Quotient_Info.quotdata_lookup_raw thy s) - | is_quot_type _ _ = false fun is_codatatype thy (Type (s, _)) = not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s |> Option.map snd |> these)) | is_codatatype _ _ = false +fun is_real_quot_type thy (Type (s, _)) = + is_some (Quotient_Info.quotdata_lookup_raw thy s) + | is_real_quot_type _ _ = false +fun is_quot_type thy T = + is_real_quot_type thy T andalso not (is_codatatype thy T) fun is_pure_typedef ctxt (T as Type (s, _)) = let val thy = ProofContext.theory_of ctxt in is_typedef ctxt s andalso - not (is_real_datatype thy s orelse is_quot_type thy T orelse + not (is_real_datatype thy s orelse is_real_quot_type thy T orelse is_codatatype thy T orelse is_record_type T orelse is_integer_like_type T) end @@ -681,7 +683,7 @@ fun is_datatype ctxt stds (T as Type (s, _)) = let val thy = ProofContext.theory_of ctxt in (is_typedef ctxt s orelse is_codatatype thy T orelse T = @{typ ind} orelse - is_quot_type thy T) andalso not (is_basic_datatype thy stds s) + is_real_quot_type thy T) andalso not (is_basic_datatype thy stds s) end | is_datatype _ _ _ = false @@ -718,15 +720,19 @@ SOME {Rep_name, ...} => s = Rep_name | NONE => false) | is_rep_fun _ _ = false -fun is_quot_abs_fun ctxt - (x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) = - (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s' - = SOME (Const x)) +fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun}, + [_, abs_T as Type (s', _)]))) = + let val thy = ProofContext.theory_of ctxt in + (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s' + = SOME (Const x)) andalso not (is_codatatype thy abs_T) + end | is_quot_abs_fun _ _ = false -fun is_quot_rep_fun ctxt - (x as (_, Type (@{type_name fun}, [Type (s', _), _]))) = - (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s' - = SOME (Const x)) +fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun}, + [abs_T as Type (s', _), _]))) = + let val thy = ProofContext.theory_of ctxt in + (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s' + = SOME (Const x)) andalso not (is_codatatype thy abs_T) + end | is_quot_rep_fun _ _ = false fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun}, @@ -913,7 +919,7 @@ val T' = (Record.get_extT_fields thy T |> apsnd single |> uncurry append |> map snd) ---> T in [(s', T')] end - else if is_quot_type thy T then + else if is_real_quot_type thy T then [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)] else case typedef_info ctxt s of SOME {abs_type, rep_type, Abs_name, ...} => diff -r 8164c91039ea -r 1c7d7eaebdf2 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 06 11:33:58 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 06 11:35:10 2010 +0200 @@ -960,31 +960,25 @@ fold (add_nondef_axiom depth) (nondef_props_for_const thy true choice_spec_table x) accum else if is_abs_fun ctxt x then - if is_quot_type thy (range_type T) then - accum - else - accum |> fold (add_nondef_axiom depth) - (nondef_props_for_const thy false nondef_table x) - |> (is_funky_typedef thy (range_type T) orelse - range_type T = nat_T) - ? fold (add_maybe_def_axiom depth) - (nondef_props_for_const thy true + accum |> fold (add_nondef_axiom depth) + (nondef_props_for_const thy false nondef_table x) + |> (is_funky_typedef thy (range_type T) orelse + range_type T = nat_T) + ? fold (add_maybe_def_axiom depth) + (nondef_props_for_const thy true (extra_table def_table s) x) else if is_rep_fun ctxt x then - if is_quot_type thy (domain_type T) then - accum - else - accum |> fold (add_nondef_axiom depth) - (nondef_props_for_const thy false nondef_table x) - |> (is_funky_typedef thy (range_type T) orelse - range_type T = nat_T) - ? fold (add_maybe_def_axiom depth) - (nondef_props_for_const thy true + accum |> fold (add_nondef_axiom depth) + (nondef_props_for_const thy false nondef_table x) + |> (is_funky_typedef thy (range_type T) orelse + range_type T = nat_T) + ? fold (add_maybe_def_axiom depth) + (nondef_props_for_const thy true (extra_table def_table s) x) - |> add_axioms_for_term depth - (Const (mate_of_rep_fun ctxt x)) - |> fold (add_def_axiom depth) - (inverse_axioms_for_rep_fun ctxt x) + |> add_axioms_for_term depth + (Const (mate_of_rep_fun ctxt x)) + |> fold (add_def_axiom depth) + (inverse_axioms_for_rep_fun ctxt x) else if s = @{const_name TYPE} then accum else case def_of_const thy def_table x of