# HG changeset patch # User wenzelm # Date 1738013238 -3600 # Node ID d09524fdd40cfe5681e224c9c48c5415f8610f94 # Parent 5dc2c98a6f16a72808eae1e081d16a2a927eb144# Parent e6f5434ad95a6254c7163879dcf93ffb5d389660 merged diff -r 5dc2c98a6f16 -r d09524fdd40c NEWS --- a/NEWS Mon Jan 27 13:13:30 2025 +0100 +++ b/NEWS Mon Jan 27 22:27:18 2025 +0100 @@ -130,6 +130,20 @@ commands, which need to copy mixfix declarations from elsewhere and thus break after changes in the library. +* Former theory "HOL-Library.Adhoc_Overloading" is now included in Pure, +with a few changes (minor INCOMPATIBILITY): + + - Theory imports of "HOL-Library.Adhoc_Overloading" need to be removed + (or replaced by Main). + + - Equivalence of overloaded constants has become more liberal: sorts + of type variables are ignore, schematic type variables only need to + match (in both directions) instead of being literally equal. + + - Command syntax now requires a separator: "adhoc_overloading c \ vs". + + - The "no" keyword for bundles works as for 'syntax' / 'no_syntax'. + * Theory "HOL-Library.Datatype_Records" provides bundle "datatype_record_syntax" to exchange its alternative notation versus regular "record_syntax". This also allows to swap record syntax later @@ -313,6 +327,9 @@ * Theory "HOL-Library.Suc_Notation" provides compact notation for iterated Suc terms. +* Theory "HOL-Library.Adhoc_Overloading" has been moved to Pure. Minor +INCOMPATIBILITY: need to adjust theory imports. + *** ML *** diff -r 5dc2c98a6f16 -r d09524fdd40c src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Mon Jan 27 13:13:30 2025 +0100 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon Jan 27 22:27:18 2025 +0100 @@ -5,7 +5,6 @@ Main "HOL-Library.Old_Datatype" "HOL-Library.Old_Recdef" - "HOL-Library.Adhoc_Overloading" "HOL-Library.Dlist" "HOL-Library.FSet" Base @@ -648,41 +647,6 @@ \ -section \Adhoc overloading of constants\ - -text \ - \begin{tabular}{rcll} - @{command_def "adhoc_overloading"} & : & \local_theory \ local_theory\ \\ - @{command_def "no_adhoc_overloading"} & : & \local_theory \ local_theory\ \\ - @{attribute_def "show_variants"} & : & \attribute\ & default \false\ \\ - \end{tabular} - - \<^medskip> - Adhoc overloading allows to overload a constant depending on its type. - Typically this involves the introduction of an uninterpreted constant (used - for input and output) and the addition of some variants (used internally). - For examples see \<^file>\~~/src/HOL/Examples/Adhoc_Overloading_Examples.thy\ and - \<^file>\~~/src/HOL/Library/Monad_Syntax.thy\. - - \<^rail>\ - (@@{command adhoc_overloading} | @@{command no_adhoc_overloading}) - (@{syntax name} (@{syntax term} + ) + @'and') - \ - - \<^descr> @{command "adhoc_overloading"}~\c v\<^sub>1 ... v\<^sub>n\ associates variants with an - existing constant. - - \<^descr> @{command "no_adhoc_overloading"} is similar to @{command - "adhoc_overloading"}, but removes the specified variants from the present - context. - - \<^descr> @{attribute "show_variants"} controls printing of variants of overloaded - constants. If enabled, the internally used variants are printed instead of - their respective overloaded constants. This is occasionally useful to check - whether the system agrees with a user's expectations about derived variants. -\ - - section \Definition by specification \label{sec:hol-specification}\ text \ diff -r 5dc2c98a6f16 -r d09524fdd40c src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Mon Jan 27 13:13:30 2025 +0100 +++ b/src/Doc/Isar_Ref/Spec.thy Mon Jan 27 22:27:18 2025 +0100 @@ -296,6 +296,7 @@ \<^item> @{command translations} versus @{command no_translations} \<^item> @{command notation} versus @{command no_notation} \<^item> @{command type_notation} versus @{command no_type_notation} + \<^item> @{command adhoc_overloading} versus @{command no_adhoc_overloading} This also works recursively for the @{command unbundle} command as declaration inside a @{command bundle} definition: \<^verbatim>\no\ means that @@ -1093,6 +1094,41 @@ lemma "Length ((a, b, c, d, e), ()) = 1" by simp +section \Overloaded constant abbreviations: adhoc overloading\ + +text \ + \begin{tabular}{rcll} + @{command_def "adhoc_overloading"} & : & \local_theory \ local_theory\ \\ + @{command_def "no_adhoc_overloading"} & : & \local_theory \ local_theory\ \\ + @{attribute_def "show_variants"} & : & \attribute\ & default \false\ \\ + \end{tabular} + + \<^medskip> + Adhoc overloading allows to overload a constant depending on its type. + Typically this involves the introduction of an uninterpreted constant (used + for input and output) and the addition of some variants (used internally). + For examples see \<^file>\~~/src/HOL/Examples/Adhoc_Overloading.thy\ and + \<^file>\~~/src/HOL/Library/Monad_Syntax.thy\. + + \<^rail>\ + (@@{command adhoc_overloading} | @@{command no_adhoc_overloading}) \ + (@{syntax name} ('==' | '\') (@{syntax term} + ) + @'and') + \ + + \<^descr> @{command "adhoc_overloading"}~\c \ v\<^sub>1 ... v\<^sub>n\ associates variants with an + existing constant. + + \<^descr> @{command "no_adhoc_overloading"} is similar to @{command + "adhoc_overloading"}, but removes the specified variants from the present + context. + + \<^descr> @{attribute "show_variants"} controls printing of variants of overloaded + constants. If enabled, the internally used variants are printed instead of + their respective overloaded constants. This is occasionally useful to check + whether the system agrees with a user's expectations about derived variants. +\ + + section \Incorporating ML code \label{sec:ML}\ text \ diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/Examples/Adhoc_Overloading.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Examples/Adhoc_Overloading.thy Mon Jan 27 22:27:18 2025 +0100 @@ -0,0 +1,254 @@ +(* Title: HOL/Examples/Adhoc_Overloading.thy + Author: Christian Sternagel +*) + +section \Ad Hoc Overloading\ + +theory Adhoc_Overloading +imports + Main + "HOL-Library.Infinite_Set" +begin + +text \Adhoc overloading allows to overload a constant depending on +its type. Typically this involves to introduce an uninterpreted +constant (used for input and output) and then add some variants (used +internally).\ + +subsection \Plain Ad Hoc Overloading\ + +text \Consider the type of first-order terms.\ +datatype ('a, 'b) "term" = + Var 'b | + Fun 'a "('a, 'b) term list" + +text \The set of variables of a term might be computed as follows.\ +fun term_vars :: "('a, 'b) term \ 'b set" where + "term_vars (Var x) = {x}" | + "term_vars (Fun f ts) = \(set (map term_vars ts))" + +text \However, also for \emph{rules} (i.e., pairs of terms) and term +rewrite systems (i.e., sets of rules), the set of variables makes +sense. Thus we introduce an unspecified constant \vars\.\ + +consts vars :: "'a \ 'b set" + +text \Which is then overloaded with variants for terms, rules, and TRSs.\ +adhoc_overloading + vars \ term_vars + +value [nbe] "vars (Fun ''f'' [Var 0, Var 1])" + +fun rule_vars :: "('a, 'b) term \ ('a, 'b) term \ 'b set" where + "rule_vars (l, r) = vars l \ vars r" + +adhoc_overloading + vars \ rule_vars + +value [nbe] "vars (Var 1, Var 0)" + +definition trs_vars :: "(('a, 'b) term \ ('a, 'b) term) set \ 'b set" where + "trs_vars R = \(rule_vars ` R)" + +adhoc_overloading + vars \ trs_vars + +value [nbe] "vars {(Var 1, Var 0)}" + +text \Sometimes it is necessary to add explicit type constraints +before a variant can be determined.\ +(*value "vars R" (*has multiple instances*)*) +value "vars (R :: (('a, 'b) term \ ('a, 'b) term) set)" + +text \It is also possible to remove variants.\ +no_adhoc_overloading + vars \ term_vars rule_vars + +(*value "vars (Var 1)" (*does not have an instance*)*) + +text \As stated earlier, the overloaded constant is only used for +input and output. Internally, always a variant is used, as can be +observed by the configuration option \show_variants\.\ + +adhoc_overloading + vars \ term_vars + +declare [[show_variants]] + +term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*) + + +subsection \Adhoc Overloading inside Locales\ + +text \As example we use permutations that are parametrized over an +atom type \<^typ>\'a\.\ + +definition perms :: "('a \ 'a) set" where + "perms = {f. bij f \ finite {x. f x \ x}}" + +typedef 'a perm = "perms :: ('a \ 'a) set" + by standard (auto simp: perms_def) + +text \First we need some auxiliary lemmas.\ +lemma permsI [Pure.intro]: + assumes "bij f" and "MOST x. f x = x" + shows "f \ perms" + using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg) + +lemma perms_imp_bij: + "f \ perms \ bij f" + by (simp add: perms_def) + +lemma perms_imp_MOST_eq: + "f \ perms \ MOST x. f x = x" + by (simp add: perms_def) (metis MOST_iff_finiteNeg) + +lemma id_perms [simp]: + "id \ perms" + "(\x. x) \ perms" + by (auto simp: perms_def bij_def) + +lemma perms_comp [simp]: + assumes f: "f \ perms" and g: "g \ perms" + shows "(f \ g) \ perms" + apply (intro permsI bij_comp) + apply (rule perms_imp_bij [OF g]) + apply (rule perms_imp_bij [OF f]) + apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF g]]) + apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF f]]) + by simp + +lemma perms_inv: + assumes f: "f \ perms" + shows "inv f \ perms" + apply (rule permsI) + apply (rule bij_imp_bij_inv) + apply (rule perms_imp_bij [OF f]) + apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]]) + apply (erule subst, rule inv_f_f) + apply (rule bij_is_inj [OF perms_imp_bij [OF f]]) + done + +lemma bij_Rep_perm: "bij (Rep_perm p)" + using Rep_perm [of p] unfolding perms_def by simp + +instantiation perm :: (type) group_add +begin + +definition "0 = Abs_perm id" +definition "- p = Abs_perm (inv (Rep_perm p))" +definition "p + q = Abs_perm (Rep_perm p \ Rep_perm q)" +definition "(p1::'a perm) - p2 = p1 + - p2" + +lemma Rep_perm_0: "Rep_perm 0 = id" + unfolding zero_perm_def by (simp add: Abs_perm_inverse) + +lemma Rep_perm_add: + "Rep_perm (p1 + p2) = Rep_perm p1 \ Rep_perm p2" + unfolding plus_perm_def by (simp add: Abs_perm_inverse Rep_perm) + +lemma Rep_perm_uminus: + "Rep_perm (- p) = inv (Rep_perm p)" + unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm) + +instance + apply standard + unfolding Rep_perm_inject [symmetric] + unfolding minus_perm_def + unfolding Rep_perm_add + unfolding Rep_perm_uminus + unfolding Rep_perm_0 + apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]]) + done + +end + +lemmas Rep_perm_simps = + Rep_perm_0 + Rep_perm_add + Rep_perm_uminus + + +section \Permutation Types\ + +text \We want to be able to apply permutations to arbitrary types. To +this end we introduce a constant \PERMUTE\ together with +convenient infix syntax.\ + +consts PERMUTE :: "'a perm \ 'b \ 'b" (infixr \\\ 75) + +text \Then we add a locale for types \<^typ>\'b\ that support +appliciation of permutations.\ +locale permute = + fixes permute :: "'a perm \ 'b \ 'b" + assumes permute_zero [simp]: "permute 0 x = x" + and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)" +begin + +adhoc_overloading + PERMUTE \ permute + +end + +text \Permuting atoms.\ +definition permute_atom :: "'a perm \ 'a \ 'a" where + "permute_atom p a = (Rep_perm p) a" + +adhoc_overloading + PERMUTE \ permute_atom + +interpretation atom_permute: permute permute_atom + by standard (simp_all add: permute_atom_def Rep_perm_simps) + +text \Permuting permutations.\ +definition permute_perm :: "'a perm \ 'a perm \ 'a perm" where + "permute_perm p q = p + q - p" + +adhoc_overloading + PERMUTE \ permute_perm + +interpretation perm_permute: permute permute_perm + apply standard + unfolding permute_perm_def + apply simp + apply (simp only: diff_conv_add_uminus minus_add add.assoc) + done + +text \Permuting functions.\ +locale fun_permute = + dom: permute perm1 + ran: permute perm2 + for perm1 :: "'a perm \ 'b \ 'b" + and perm2 :: "'a perm \ 'c \ 'c" +begin + +adhoc_overloading + PERMUTE \ perm1 perm2 + +definition permute_fun :: "'a perm \ ('b \ 'c) \ ('b \ 'c)" where + "permute_fun p f = (\x. p \ (f (-p \ x)))" + +adhoc_overloading + PERMUTE \ permute_fun + +end + +sublocale fun_permute \ permute permute_fun + by (unfold_locales, auto simp: permute_fun_def) + (metis dom.permute_plus minus_add) + +lemma "(Abs_perm id :: nat perm) \ Suc 0 = Suc 0" + unfolding permute_atom_def + by (metis Rep_perm_0 id_apply zero_perm_def) + +interpretation atom_fun_permute: fun_permute permute_atom permute_atom + by (unfold_locales) + +adhoc_overloading + PERMUTE \ atom_fun_permute.permute_fun + +lemma "(Abs_perm id :: 'a perm) \ id = id" + unfolding atom_fun_permute.permute_fun_def + unfolding permute_atom_def + by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def) + +end diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/Examples/Adhoc_Overloading_Examples.thy --- a/src/HOL/Examples/Adhoc_Overloading_Examples.thy Mon Jan 27 13:13:30 2025 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,256 +0,0 @@ -(* Title: HOL/Examples/Adhoc_Overloading_Examples.thy - Author: Christian Sternagel -*) - -section \Ad Hoc Overloading\ - -theory Adhoc_Overloading_Examples -imports - Main - "HOL-Library.Infinite_Set" - "HOL-Library.Adhoc_Overloading" -begin - -text \Adhoc overloading allows to overload a constant depending on -its type. Typically this involves to introduce an uninterpreted -constant (used for input and output) and then add some variants (used -internally).\ - -subsection \Plain Ad Hoc Overloading\ - -text \Consider the type of first-order terms.\ -datatype ('a, 'b) "term" = - Var 'b | - Fun 'a "('a, 'b) term list" - -text \The set of variables of a term might be computed as follows.\ -fun term_vars :: "('a, 'b) term \ 'b set" where - "term_vars (Var x) = {x}" | - "term_vars (Fun f ts) = \(set (map term_vars ts))" - -text \However, also for \emph{rules} (i.e., pairs of terms) and term -rewrite systems (i.e., sets of rules), the set of variables makes -sense. Thus we introduce an unspecified constant \vars\.\ - -consts vars :: "'a \ 'b set" - -text \Which is then overloaded with variants for terms, rules, and TRSs.\ -adhoc_overloading - vars term_vars - -value [nbe] "vars (Fun ''f'' [Var 0, Var 1])" - -fun rule_vars :: "('a, 'b) term \ ('a, 'b) term \ 'b set" where - "rule_vars (l, r) = vars l \ vars r" - -adhoc_overloading - vars rule_vars - -value [nbe] "vars (Var 1, Var 0)" - -definition trs_vars :: "(('a, 'b) term \ ('a, 'b) term) set \ 'b set" where - "trs_vars R = \(rule_vars ` R)" - -adhoc_overloading - vars trs_vars - -value [nbe] "vars {(Var 1, Var 0)}" - -text \Sometimes it is necessary to add explicit type constraints -before a variant can be determined.\ -(*value "vars R" (*has multiple instances*)*) -value "vars (R :: (('a, 'b) term \ ('a, 'b) term) set)" - -text \It is also possible to remove variants.\ -no_adhoc_overloading - vars term_vars rule_vars - -(*value "vars (Var 1)" (*does not have an instance*)*) - -text \As stated earlier, the overloaded constant is only used for -input and output. Internally, always a variant is used, as can be -observed by the configuration option \show_variants\.\ - -adhoc_overloading - vars term_vars - -declare [[show_variants]] - -term "vars (Var 1)" (*which yields: "term_vars (Var 1)"*) - - -subsection \Adhoc Overloading inside Locales\ - -text \As example we use permutations that are parametrized over an -atom type \<^typ>\'a\.\ - -definition perms :: "('a \ 'a) set" where - "perms = {f. bij f \ finite {x. f x \ x}}" - -typedef 'a perm = "perms :: ('a \ 'a) set" - by standard (auto simp: perms_def) - -text \First we need some auxiliary lemmas.\ -lemma permsI [Pure.intro]: - assumes "bij f" and "MOST x. f x = x" - shows "f \ perms" - using assms by (auto simp: perms_def) (metis MOST_iff_finiteNeg) - -lemma perms_imp_bij: - "f \ perms \ bij f" - by (simp add: perms_def) - -lemma perms_imp_MOST_eq: - "f \ perms \ MOST x. f x = x" - by (simp add: perms_def) (metis MOST_iff_finiteNeg) - -lemma id_perms [simp]: - "id \ perms" - "(\x. x) \ perms" - by (auto simp: perms_def bij_def) - -lemma perms_comp [simp]: - assumes f: "f \ perms" and g: "g \ perms" - shows "(f \ g) \ perms" - apply (intro permsI bij_comp) - apply (rule perms_imp_bij [OF g]) - apply (rule perms_imp_bij [OF f]) - apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF g]]) - apply (rule MOST_rev_mp [OF perms_imp_MOST_eq [OF f]]) - by simp - -lemma perms_inv: - assumes f: "f \ perms" - shows "inv f \ perms" - apply (rule permsI) - apply (rule bij_imp_bij_inv) - apply (rule perms_imp_bij [OF f]) - apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]]) - apply (erule subst, rule inv_f_f) - apply (rule bij_is_inj [OF perms_imp_bij [OF f]]) - done - -lemma bij_Rep_perm: "bij (Rep_perm p)" - using Rep_perm [of p] unfolding perms_def by simp - -instantiation perm :: (type) group_add -begin - -definition "0 = Abs_perm id" -definition "- p = Abs_perm (inv (Rep_perm p))" -definition "p + q = Abs_perm (Rep_perm p \ Rep_perm q)" -definition "(p1::'a perm) - p2 = p1 + - p2" - -lemma Rep_perm_0: "Rep_perm 0 = id" - unfolding zero_perm_def by (simp add: Abs_perm_inverse) - -lemma Rep_perm_add: - "Rep_perm (p1 + p2) = Rep_perm p1 \ Rep_perm p2" - unfolding plus_perm_def by (simp add: Abs_perm_inverse Rep_perm) - -lemma Rep_perm_uminus: - "Rep_perm (- p) = inv (Rep_perm p)" - unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm) - -instance - apply standard - unfolding Rep_perm_inject [symmetric] - unfolding minus_perm_def - unfolding Rep_perm_add - unfolding Rep_perm_uminus - unfolding Rep_perm_0 - apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]]) - done - -end - -lemmas Rep_perm_simps = - Rep_perm_0 - Rep_perm_add - Rep_perm_uminus - - -section \Permutation Types\ - -text \We want to be able to apply permutations to arbitrary types. To -this end we introduce a constant \PERMUTE\ together with -convenient infix syntax.\ - -consts PERMUTE :: "'a perm \ 'b \ 'b" (infixr \\\ 75) - -text \Then we add a locale for types \<^typ>\'b\ that support -appliciation of permutations.\ -locale permute = - fixes permute :: "'a perm \ 'b \ 'b" - assumes permute_zero [simp]: "permute 0 x = x" - and permute_plus [simp]: "permute (p + q) x = permute p (permute q x)" -begin - -adhoc_overloading - PERMUTE permute - -end - -text \Permuting atoms.\ -definition permute_atom :: "'a perm \ 'a \ 'a" where - "permute_atom p a = (Rep_perm p) a" - -adhoc_overloading - PERMUTE permute_atom - -interpretation atom_permute: permute permute_atom - by standard (simp_all add: permute_atom_def Rep_perm_simps) - -text \Permuting permutations.\ -definition permute_perm :: "'a perm \ 'a perm \ 'a perm" where - "permute_perm p q = p + q - p" - -adhoc_overloading - PERMUTE permute_perm - -interpretation perm_permute: permute permute_perm - apply standard - unfolding permute_perm_def - apply simp - apply (simp only: diff_conv_add_uminus minus_add add.assoc) - done - -text \Permuting functions.\ -locale fun_permute = - dom: permute perm1 + ran: permute perm2 - for perm1 :: "'a perm \ 'b \ 'b" - and perm2 :: "'a perm \ 'c \ 'c" -begin - -adhoc_overloading - PERMUTE perm1 perm2 - -definition permute_fun :: "'a perm \ ('b \ 'c) \ ('b \ 'c)" where - "permute_fun p f = (\x. p \ (f (-p \ x)))" - -adhoc_overloading - PERMUTE permute_fun - -end - -sublocale fun_permute \ permute permute_fun - by (unfold_locales, auto simp: permute_fun_def) - (metis dom.permute_plus minus_add) - -lemma "(Abs_perm id :: nat perm) \ Suc 0 = Suc 0" - unfolding permute_atom_def - by (metis Rep_perm_0 id_apply zero_perm_def) - -interpretation atom_fun_permute: fun_permute permute_atom permute_atom - by (unfold_locales) - -adhoc_overloading - PERMUTE atom_fun_permute.permute_fun - -lemma "(Abs_perm id :: 'a perm) \ id = id" - unfolding atom_fun_permute.permute_fun_def - unfolding permute_atom_def - by (metis Rep_perm_0 id_def inj_imp_inv_eq inj_on_id uminus_perm_def zero_perm_def) - -end - diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jan 27 13:13:30 2025 +0100 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jan 27 22:27:18 2025 +0100 @@ -250,7 +250,7 @@ | None \ None)" adhoc_overloading - Monad_Syntax.bind Heap_Monad.bind + Monad_Syntax.bind \ Heap_Monad.bind lemma execute_bind [execute_simps]: "execute f h = Some (x, h') \ execute (f \ g) h = execute (g x) h'" diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/Library/Adhoc_Overloading.thy --- a/src/HOL/Library/Adhoc_Overloading.thy Mon Jan 27 13:13:30 2025 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* Title: HOL/Library/Adhoc_Overloading.thy - Author: Alexander Krauss, TU Muenchen - Author: Christian Sternagel, University of Innsbruck -*) - -section \Adhoc overloading of constants based on their types\ - -theory Adhoc_Overloading - imports Main - keywords "adhoc_overloading" "no_adhoc_overloading" :: thy_decl -begin - -ML_file \adhoc_overloading.ML\ - -end diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon Jan 27 13:13:30 2025 +0100 +++ b/src/HOL/Library/Library.thy Mon Jan 27 22:27:18 2025 +0100 @@ -2,7 +2,6 @@ theory Library imports AList - Adhoc_Overloading BNF_Axiomatization BNF_Corec Bourbaki_Witt_Fixpoint diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/Library/Monad_Syntax.thy --- a/src/HOL/Library/Monad_Syntax.thy Mon Jan 27 13:13:30 2025 +0100 +++ b/src/HOL/Library/Monad_Syntax.thy Mon Jan 27 22:27:18 2025 +0100 @@ -6,7 +6,7 @@ section \Monad notation for arbitrary types\ theory Monad_Syntax - imports Adhoc_Overloading + imports Main begin text \ @@ -70,6 +70,6 @@ "(m \ n)" \ "(m \ (\_. n))" adhoc_overloading - bind Set.bind Predicate.bind Option.bind List.bind + bind \ Set.bind Predicate.bind Option.bind List.bind end diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/Library/State_Monad.thy --- a/src/HOL/Library/State_Monad.thy Mon Jan 27 13:13:30 2025 +0100 +++ b/src/HOL/Library/State_Monad.thy Mon Jan 27 22:27:18 2025 +0100 @@ -89,7 +89,7 @@ "run_state (bind x f) s = (case run_state x s of (a, s') \ run_state (f a) s')" unfolding bind_def by auto -adhoc_overloading Monad_Syntax.bind bind +adhoc_overloading Monad_Syntax.bind \ bind lemma bind_left_identity[simp]: "bind (return a) f = f a" unfolding return_def bind_def by simp diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/Library/adhoc_overloading.ML --- a/src/HOL/Library/adhoc_overloading.ML Mon Jan 27 13:13:30 2025 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,247 +0,0 @@ -(* Author: Alexander Krauss, TU Muenchen - Author: Christian Sternagel, University of Innsbruck - -Adhoc overloading of constants based on their types. -*) - -signature ADHOC_OVERLOADING = -sig - val is_overloaded: Proof.context -> string -> bool - val generic_add_overloaded: string -> Context.generic -> Context.generic - val generic_remove_overloaded: string -> Context.generic -> Context.generic - val generic_add_variant: string -> term -> Context.generic -> Context.generic - (*If the list of variants is empty at the end of "generic_remove_variant", then - "generic_remove_overloaded" is called implicitly.*) - val generic_remove_variant: string -> term -> Context.generic -> Context.generic - val show_variants: bool Config.T -end - -structure Adhoc_Overloading: ADHOC_OVERLOADING = -struct - -val show_variants = Attrib.setup_config_bool \<^binding>\show_variants\ (K false); - - -(* errors *) - -fun err_duplicate_variant oconst = - error ("Duplicate variant of " ^ quote oconst); - -fun err_not_a_variant oconst = - error ("Not a variant of " ^ quote oconst); - -fun err_not_overloaded oconst = - error ("Constant " ^ quote oconst ^ " is not declared as overloaded"); - -fun err_unresolved_overloading ctxt0 (c, T) t instances = - let - val ctxt = Config.put show_variants true ctxt0 - val const_space = Proof_Context.const_space ctxt - val prt_const = - Pretty.block [Name_Space.pretty ctxt const_space c, Pretty.str " ::", Pretty.brk 1, - Pretty.quote (Syntax.pretty_typ ctxt T)] - in - error (Pretty.string_of (Pretty.chunks [ - Pretty.block [ - Pretty.str "Unresolved adhoc overloading of constant", Pretty.brk 1, - prt_const, Pretty.brk 1, Pretty.str "in term", Pretty.brk 1, - Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t)]], - Pretty.block ( - (if null instances then [Pretty.str "no instances"] - else Pretty.fbreaks ( - Pretty.str "multiple instances:" :: - map (Pretty.mark Markup.item o Syntax.pretty_term ctxt) instances)))])) - end; - - -(* generic data *) - -fun variants_eq ((v1, T1), (v2, T2)) = - Term.aconv_untyped (v1, v2) andalso T1 = T2; - -structure Overload_Data = Generic_Data -( - type T = - {variants : (term * typ) list Symtab.table, - oconsts : string Termtab.table}; - val empty = {variants = Symtab.empty, oconsts = Termtab.empty}; - - fun merge - ({variants = vtab1, oconsts = otab1}, - {variants = vtab2, oconsts = otab2}) : T = - let - fun merge_oconsts _ (oconst1, oconst2) = - if oconst1 = oconst2 then oconst1 - else err_duplicate_variant oconst1; - in - {variants = Symtab.merge_list variants_eq (vtab1, vtab2), - oconsts = Termtab.join merge_oconsts (otab1, otab2)} - end; -); - -fun map_tables f g = - Overload_Data.map (fn {variants = vtab, oconsts = otab} => - {variants = f vtab, oconsts = g otab}); - -val is_overloaded = Symtab.defined o #variants o Overload_Data.get o Context.Proof; -val get_variants = Symtab.lookup o #variants o Overload_Data.get o Context.Proof; -val get_overloaded = Termtab.lookup o #oconsts o Overload_Data.get o Context.Proof; - -fun generic_add_overloaded oconst context = - if is_overloaded (Context.proof_of context) oconst then context - else map_tables (Symtab.update (oconst, [])) I context; - -fun generic_remove_overloaded oconst context = - let - fun remove_oconst_and_variants context oconst = - let - val remove_variants = - (case get_variants (Context.proof_of context) oconst of - NONE => I - | SOME vs => fold (Termtab.remove (op =) o rpair oconst o fst) vs); - in map_tables (Symtab.delete_safe oconst) remove_variants context end; - in - if is_overloaded (Context.proof_of context) oconst then remove_oconst_and_variants context oconst - else err_not_overloaded oconst - end; - -local - fun generic_variant add oconst t context = - let - val ctxt = Context.proof_of context; - val _ = if is_overloaded ctxt oconst then () else err_not_overloaded oconst; - val T = t |> fastype_of; - val t' = Term.map_types (K dummyT) t; - in - if add then - let - val _ = - (case get_overloaded ctxt t' of - NONE => () - | SOME oconst' => err_duplicate_variant oconst'); - in - map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t', oconst)) context - end - else - let - val _ = - if member variants_eq (the (get_variants ctxt oconst)) (t', T) then () - else err_not_a_variant oconst; - in - map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T))) - (Termtab.delete_safe t') context - |> (fn context => - (case get_variants (Context.proof_of context) oconst of - SOME [] => generic_remove_overloaded oconst context - | _ => context)) - end - end; -in - val generic_add_variant = generic_variant true; - val generic_remove_variant = generic_variant false; -end; - - -(* check / uncheck *) - -fun unifiable_with thy T1 T2 = - let - val maxidx1 = Term.maxidx_of_typ T1; - val T2' = Logic.incr_tvar (maxidx1 + 1) T2; - val maxidx2 = Term.maxidx_typ T2' maxidx1; - in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end; - -fun get_candidates ctxt (c, T) = - get_variants ctxt c - |> Option.map (map_filter (fn (t, T') => - if unifiable_with (Proof_Context.theory_of ctxt) T T' - (*keep the type constraint for the type-inference check phase*) - then SOME (Type.constraint T t) - else NONE)); - -fun insert_variants ctxt t (oconst as Const (c, T)) = - (case get_candidates ctxt (c, T) of - SOME [] => err_unresolved_overloading ctxt (c, T) t [] - | SOME [variant] => variant - | _ => oconst) - | insert_variants _ _ oconst = oconst; - -fun insert_overloaded ctxt = - let - fun proc t = - Term.map_types (K dummyT) t - |> get_overloaded ctxt - |> Option.map (Const o rpair (Term.type_of t)); - in - Pattern.rewrite_term_yoyo (Proof_Context.theory_of ctxt) [] [proc] - end; - -fun check ctxt = - map (fn t => Term.map_aterms (insert_variants ctxt t) t); - -fun uncheck ctxt ts = - if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then ts - else map (insert_overloaded ctxt) ts; - -fun reject_unresolved ctxt = - let - val the_candidates = the o get_candidates ctxt; - fun check_unresolved t = - (case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of - [] => t - | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT)); - in map check_unresolved end; - - -(* setup *) - -val _ = Context.>> - (Syntax_Phases.term_check 0 "adhoc_overloading" check - #> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved - #> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck); - - -(* commands *) - -fun generic_adhoc_overloading_cmd add = - if add then - fold (fn (oconst, ts) => - generic_add_overloaded oconst - #> fold (generic_add_variant oconst) ts) - else - fold (fn (oconst, ts) => - fold (generic_remove_variant oconst) ts); - -fun adhoc_overloading_cmd' add args phi = - let val args' = args - |> map (apsnd (map_filter (fn t => - let val t' = Morphism.term phi t; - in if Term.aconv_untyped (t, t') then SOME t' else NONE end))); - in generic_adhoc_overloading_cmd add args' end; - -fun adhoc_overloading_cmd add raw_args lthy = - let - fun const_name ctxt = - dest_Const_name o Proof_Context.read_const {proper = false, strict = false} ctxt; (* FIXME {proper = true, strict = true} (!?) *) - fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt; - val args = - raw_args - |> map (apfst (const_name lthy)) - |> map (apsnd (map (read_term lthy))); - in - Local_Theory.declaration {syntax = true, pervasive = false, pos = Position.thread_data ()} - (adhoc_overloading_cmd' add args) lthy - end; - -val _ = - Outer_Syntax.local_theory \<^command_keyword>\adhoc_overloading\ - "add adhoc overloading for constants / fixed variables" - (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd true); - -val _ = - Outer_Syntax.local_theory \<^command_keyword>\no_adhoc_overloading\ - "delete adhoc overloading for constants / fixed variables" - (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false); - -end; - diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/Probability/Giry_Monad.thy --- a/src/HOL/Probability/Giry_Monad.thy Mon Jan 27 13:13:30 2025 +0100 +++ b/src/HOL/Probability/Giry_Monad.thy Mon Jan 27 22:27:18 2025 +0100 @@ -1092,7 +1092,7 @@ "bind M f = (if space M = {} then count_space {} else join (distr M (subprob_algebra (f (SOME x. x \ space M))) f))" -adhoc_overloading Monad_Syntax.bind bind +adhoc_overloading Monad_Syntax.bind \ bind lemma bind_empty: "space M = {} \ bind M f = count_space {}" diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Mon Jan 27 13:13:30 2025 +0100 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Mon Jan 27 22:27:18 2025 +0100 @@ -367,7 +367,7 @@ done qed -adhoc_overloading Monad_Syntax.bind bind_pmf +adhoc_overloading Monad_Syntax.bind \ bind_pmf lemma ennreal_pmf_bind: "pmf (bind_pmf N f) i = (\\<^sup>+x. pmf (f x) i \measure_pmf N)" unfolding pmf.rep_eq bind_pmf.rep_eq diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/Probability/SPMF.thy --- a/src/HOL/Probability/SPMF.thy Mon Jan 27 13:13:30 2025 +0100 +++ b/src/HOL/Probability/SPMF.thy Mon Jan 27 22:27:18 2025 +0100 @@ -513,7 +513,7 @@ definition bind_spmf :: "'a spmf \ ('a \ 'b spmf) \ 'b spmf" where "bind_spmf x f = bind_pmf x (\a. case a of None \ return_pmf None | Some a' \ f a')" -adhoc_overloading Monad_Syntax.bind bind_spmf +adhoc_overloading Monad_Syntax.bind \ bind_spmf lemma return_None_bind_spmf [simp]: "return_pmf None \ (f :: 'a \ _) = return_pmf None" by(simp add: bind_spmf_def bind_return_pmf) diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/ROOT --- a/src/HOL/ROOT Mon Jan 27 13:13:30 2025 +0100 +++ b/src/HOL/ROOT Mon Jan 27 22:27:18 2025 +0100 @@ -22,7 +22,7 @@ sessions "HOL-Computational_Algebra" theories - Adhoc_Overloading_Examples + Adhoc_Overloading Ackermann Cantor Coherent diff -r 5dc2c98a6f16 -r d09524fdd40c src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Mon Jan 27 13:13:30 2025 +0100 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Mon Jan 27 22:27:18 2025 +0100 @@ -67,15 +67,14 @@ fun wit_of_code_dt (CODE_DT code_dt) = #wit code_dt; fun wit_thm_of_code_dt (CODE_DT code_dt) = #wit_thm code_dt; fun rep_isom_data_of_code_dt (CODE_DT code_dt) = #rep_isom_data code_dt; -fun ty_alpha_equiv (T, U) = Type.raw_instance (T, U) andalso Type.raw_instance (U, T); -fun code_dt_eq c = (ty_alpha_equiv o apply2 rty_of_code_dt) c - andalso (ty_alpha_equiv o apply2 qty_of_code_dt) c; +fun code_dt_eq c = (Type.raw_equiv o apply2 rty_of_code_dt) c + andalso (Type.raw_equiv o apply2 qty_of_code_dt) c; fun term_of_code_dt code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt |> HOLogic.mk_prodT |> Net.encode_type |> single; (* modulo renaming, typ must contain TVars *) fun is_code_dt_of_type (rty, qty) code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt - |> HOLogic.mk_prodT |> curry ty_alpha_equiv (HOLogic.mk_prodT (rty, qty)); + |> HOLogic.mk_prodT |> curry Type.raw_equiv (HOLogic.mk_prodT (rty, qty)); fun mk_rep_isom_data isom transfer bundle_name pointer = REP_ISOM { isom = isom, transfer = transfer, bundle_name = bundle_name, pointer = pointer} diff -r 5dc2c98a6f16 -r d09524fdd40c src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Mon Jan 27 13:13:30 2025 +0100 +++ b/src/Pure/Admin/build_release.scala Mon Jan 27 22:27:18 2025 +0100 @@ -45,10 +45,8 @@ val isabelle_archive: Path = dist_dir + isabelle.tar.gz val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") - def other_isabelle(dir: Path, suffix: String = "-build"): Other_Isabelle = - Other_Isabelle(dir + isabelle, - isabelle_identifier = dist_name + suffix, - progress = progress) + def other_isabelle(dir: Path): Other_Isabelle = + Other_Isabelle(dir + isabelle, isabelle_identifier = dist_name, progress = progress) def make_announce(id: String): Unit = { if (release_name.isEmpty) { @@ -845,7 +843,7 @@ val bundle_path = context.dist_dir + Path.basic(bundle) execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle_path)) - val other_isabelle = context.other_isabelle(tmp_dir, suffix = "") + val other_isabelle = context.other_isabelle(tmp_dir) Isabelle_System.make_directory(other_isabelle.etc) File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\n") diff -r 5dc2c98a6f16 -r d09524fdd40c src/Pure/Pure.thy --- a/src/Pure/Pure.thy Mon Jan 27 13:13:30 2025 +0100 +++ b/src/Pure/Pure.thy Mon Jan 27 22:27:18 2025 +0100 @@ -96,6 +96,7 @@ and "realizers" :: thy_decl and "realizability" :: thy_decl and "extract_type" "extract" :: thy_decl + and "adhoc_overloading" "no_adhoc_overloading" :: thy_decl and "find_theorems" "find_consts" :: diag and "named_theorems" :: thy_decl abbrevs "\\tag" = "\<^marker>\tag \" @@ -1416,6 +1417,30 @@ in end\ +subsubsection \Adhoc overloading\ + +ML \ +local + +val adhoc_overloading_args = + Parse.and_list1 ((Parse.const --| (\<^keyword>\\\ || \<^keyword>\==\)) -- Scan.repeat Parse.term); + +val _ = + Outer_Syntax.local_theory \<^command_keyword>\adhoc_overloading\ + "add adhoc overloading for constants / fixed variables" + (adhoc_overloading_args + >> Adhoc_Overloading.adhoc_overloading_cmd true); + +val _ = + Outer_Syntax.local_theory \<^command_keyword>\no_adhoc_overloading\ + "delete adhoc overloading for constants / fixed variables" + (adhoc_overloading_args + >> Adhoc_Overloading.adhoc_overloading_cmd false); + +in end +\ + + subsubsection \Find consts and theorems\ ML \ diff -r 5dc2c98a6f16 -r d09524fdd40c src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Jan 27 13:13:30 2025 +0100 +++ b/src/Pure/ROOT.ML Mon Jan 27 22:27:18 2025 +0100 @@ -365,6 +365,7 @@ ML_file "Tools/rule_insts.ML"; ML_file "Tools/thy_deps.ML"; ML_file "Tools/class_deps.ML"; +ML_file "Tools/adhoc_overloading.ML"; ML_file "Tools/find_theorems.ML"; ML_file "Tools/find_consts.ML"; ML_file "Tools/simplifier_trace.ML"; diff -r 5dc2c98a6f16 -r d09524fdd40c src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Mon Jan 27 13:13:30 2025 +0100 +++ b/src/Pure/Syntax/syntax.ML Mon Jan 27 22:27:18 2025 +0100 @@ -121,6 +121,8 @@ val set_polarity: bool -> Proof.context -> Proof.context val set_polarity_generic: bool -> Context.generic -> Context.generic val effective_polarity: Proof.context -> bool -> bool + val effective_polarity_global: theory -> bool -> bool + val effective_polarity_generic: Context.generic -> bool -> bool val const: string -> term val free: string -> term val var: indexname -> term @@ -787,6 +789,8 @@ val set_polarity_generic = Config.put_generic polarity; fun effective_polarity ctxt add = get_polarity ctxt = add; +fun effective_polarity_global thy add = Config.get_global thy polarity = add; +val effective_polarity_generic = Context.cases effective_polarity_global effective_polarity; open Lexicon.Syntax; diff -r 5dc2c98a6f16 -r d09524fdd40c src/Pure/Tools/adhoc_overloading.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/adhoc_overloading.ML Mon Jan 27 22:27:18 2025 +0100 @@ -0,0 +1,247 @@ +(* Title: Pure/Tools/adhoc_overloading.ML + Author: Alexander Krauss, TU Muenchen + Author: Christian Sternagel, University of Innsbruck + +Adhoc overloading of constants based on their types. +*) + +signature ADHOC_OVERLOADING = +sig + val show_variants: bool Config.T + val adhoc_overloading: bool -> (string * term list) list -> local_theory -> local_theory + val adhoc_overloading_cmd: bool -> (string * string list) list -> local_theory -> local_theory +end + +structure Adhoc_Overloading: ADHOC_OVERLOADING = +struct + +val show_variants = Attrib.setup_config_bool \<^binding>\show_variants\ (K false); + + +(* errors *) + +fun err_duplicate_variant oconst = + error ("Duplicate variant of " ^ quote oconst); + +fun err_not_a_variant oconst = + error ("Not a variant of " ^ quote oconst); + +fun err_not_overloaded oconst = + error ("Constant " ^ quote oconst ^ " is not declared as overloaded"); + +fun err_unresolved_overloading ctxt0 (c, T) t instances = + let + val ctxt = Config.put show_variants true ctxt0 + val const_space = Proof_Context.const_space ctxt + val prt_const = + Pretty.block [Name_Space.pretty ctxt const_space c, Pretty.str " ::", Pretty.brk 1, + Pretty.quote (Syntax.pretty_typ ctxt T)] + in + error (Pretty.string_of (Pretty.chunks [ + Pretty.block [ + Pretty.str "Unresolved adhoc overloading of constant", Pretty.brk 1, + prt_const, Pretty.brk 1, Pretty.str "in term", Pretty.brk 1, + Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t)]], + Pretty.block ( + (if null instances then [Pretty.str "no instances"] + else Pretty.fbreaks ( + Pretty.str "multiple instances:" :: + map (Pretty.mark Markup.item o Syntax.pretty_term ctxt) instances)))])) + end; + + +(* generic data *) + +fun variants_eq ((v1, T1), (v2, T2)) = + Term.aconv_untyped (v1, v2) andalso Type.raw_equiv (T1, T2); + +structure Overload_Data = Generic_Data +( + type T = + {variants : (term * typ) list Symtab.table, + oconsts : string Termtab.table}; + val empty = {variants = Symtab.empty, oconsts = Termtab.empty}; + + fun merge + ({variants = vtab1, oconsts = otab1}, + {variants = vtab2, oconsts = otab2}) : T = + let + fun merge_oconsts _ (oconst1, oconst2) = + if oconst1 = oconst2 then oconst1 + else err_duplicate_variant oconst1; + in + {variants = Symtab.merge_list variants_eq (vtab1, vtab2), + oconsts = Termtab.join merge_oconsts (otab1, otab2)} + end; +); + +fun map_tables f g = + Overload_Data.map (fn {variants = vtab, oconsts = otab} => + {variants = f vtab, oconsts = g otab}); + +val is_overloaded = Symtab.defined o #variants o Overload_Data.get o Context.Proof; +val get_variants = Symtab.lookup o #variants o Overload_Data.get o Context.Proof; +val get_overloaded = Termtab.lookup o #oconsts o Overload_Data.get o Context.Proof; + +fun generic_add_overloaded oconst context = + if is_overloaded (Context.proof_of context) oconst then context + else map_tables (Symtab.update (oconst, [])) I context; + +(*If the list of variants is empty at the end of "generic_remove_variant", then +"generic_remove_overloaded" is called implicitly.*) +fun generic_remove_overloaded oconst context = + let + fun remove_oconst_and_variants context oconst = + let + val remove_variants = + (case get_variants (Context.proof_of context) oconst of + NONE => I + | SOME vs => fold (Termtab.remove (op =) o rpair oconst o fst) vs); + in map_tables (Symtab.delete_safe oconst) remove_variants context end; + in + if is_overloaded (Context.proof_of context) oconst then remove_oconst_and_variants context oconst + else err_not_overloaded oconst + end; + +local + fun generic_variant add oconst t context = + let + val ctxt = Context.proof_of context; + val _ = if is_overloaded ctxt oconst then () else err_not_overloaded oconst; + val T = t |> fastype_of; + val t' = Term.map_types (K dummyT) t; + in + if add then + let + val _ = + (case get_overloaded ctxt t' of + NONE => () + | SOME oconst' => err_duplicate_variant oconst'); + in + map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t', oconst)) context + end + else + let + val _ = + if member variants_eq (the (get_variants ctxt oconst)) (t', T) then () + else err_not_a_variant oconst; + in + map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T))) + (Termtab.delete_safe t') context + |> (fn context => + (case get_variants (Context.proof_of context) oconst of + SOME [] => generic_remove_overloaded oconst context + | _ => context)) + end + end; +in + val generic_add_variant = generic_variant true; + val generic_remove_variant = generic_variant false; +end; + + +(* check / uncheck *) + +fun unifiable_with thy T1 T2 = + let + val maxidx1 = Term.maxidx_of_typ T1; + val T2' = Logic.incr_tvar (maxidx1 + 1) T2; + val maxidx2 = Term.maxidx_typ T2' maxidx1; + in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end; + +fun get_candidates ctxt (c, T) = + get_variants ctxt c + |> Option.map (map_filter (fn (t, T') => + if unifiable_with (Proof_Context.theory_of ctxt) T T' + (*keep the type constraint for the type-inference check phase*) + then SOME (Type.constraint T t) + else NONE)); + +fun insert_variants ctxt t (oconst as Const (c, T)) = + (case get_candidates ctxt (c, T) of + SOME [] => err_unresolved_overloading ctxt (c, T) t [] + | SOME [variant] => variant + | _ => oconst) + | insert_variants _ _ oconst = oconst; + +fun insert_overloaded ctxt = + let + fun proc t = + Term.map_types (K dummyT) t + |> get_overloaded ctxt + |> Option.map (Const o rpair (Term.type_of t)); + in + Pattern.rewrite_term_yoyo (Proof_Context.theory_of ctxt) [] [proc] + end; + +fun check ctxt = + map (fn t => Term.map_aterms (insert_variants ctxt t) t); + +fun uncheck ctxt ts = + if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then ts + else map (insert_overloaded ctxt) ts; + +fun reject_unresolved ctxt = + let + val the_candidates = the o get_candidates ctxt; + fun check_unresolved t = + (case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of + [] => t + | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT)); + in map check_unresolved end; + + +(* setup *) + +val _ = Context.>> + (Syntax_Phases.term_check 0 "adhoc_overloading" check + #> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved + #> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck); + + +(* commands *) + +local + +fun generic_adhoc_overloading add args context = + if Syntax.effective_polarity_generic context add then + fold (fn (oconst, ts) => + generic_add_overloaded oconst + #> fold (generic_add_variant oconst) ts) args context + else + fold (fn (oconst, ts) => + fold (generic_remove_variant oconst) ts) args context; + +fun gen_adhoc_overloading prep_arg add raw_args lthy = + let + val args = map (prep_arg lthy) raw_args; + in + lthy |> Local_Theory.declaration {syntax = true, pervasive = false, pos = Position.thread_data ()} + (fn phi => + let val args' = args + |> map (apsnd (map_filter (fn t => + let val t' = Morphism.term phi t; + in if Term.aconv_untyped (t, t') then SOME t' else NONE end))); + in generic_adhoc_overloading add args' end) + end; + +fun cert_const_name ctxt c = + (Consts.the_const_type (Proof_Context.consts_of ctxt) c; c); + +fun read_const_name ctxt = + dest_Const_name o Proof_Context.read_const {proper = true, strict = true} ctxt; + +fun cert_term ctxt = Proof_Context.cert_term ctxt #> singleton (Variable.polymorphic ctxt); +fun read_term ctxt = Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt); + +in + +val adhoc_overloading = + gen_adhoc_overloading (fn ctxt => fn (c, ts) => (cert_const_name ctxt c, map (cert_term ctxt) ts)); + +val adhoc_overloading_cmd = + gen_adhoc_overloading (fn ctxt => fn (c, ts) => (read_const_name ctxt c, map (read_term ctxt) ts)); + +end; + +end; diff -r 5dc2c98a6f16 -r d09524fdd40c src/Pure/type.ML --- a/src/Pure/type.ML Mon Jan 27 13:13:30 2025 +0100 +++ b/src/Pure/type.ML Mon Jan 27 22:27:18 2025 +0100 @@ -84,6 +84,7 @@ val could_match: typ * typ -> bool val could_matches: typ list * typ list -> bool val raw_instance: typ * typ -> bool + val raw_equiv: typ * typ -> bool exception TUNIFY val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int val raw_unify: typ * typ -> tyenv -> tyenv @@ -487,10 +488,11 @@ | could_matches ([], []) = true | could_matches _ = false; -fun raw_instance (T, U) = - if could_match (U, T) then - (Vartab.build (raw_match (U, T)); true) handle TYPE_MATCH => false - else false; +fun can_raw_match arg = + (Vartab.build (raw_match arg); true) handle TYPE_MATCH => false; + +fun raw_instance (T, U) = could_match (U, T) andalso can_raw_match (U, T); +fun raw_equiv (T, U) = could_match (U, T) andalso can_raw_match (U, T) andalso can_raw_match (T, U); (* unification *)