Dear all,
please find attached patches for localizing
src/Tools/Adhoc_Overloading.thy. It should work like the previous
version in the non-local case, besides a more convenient interface,
i.e., instead of
setup {*
Adhoc_Overloading.add_overloaded @{const_name foo}
#> Adhoc_Overloading.add_variant @{const_name foo} @{const_name bar}
*}
it is now
adhoc_overloading
foo bar
where "bar" may be an arbitrary term (not just a constant). For removing
ad-hoc overloading there is the command "no_adhoc_overloading".
I tested the local case only on toy examples. Comments are welcome.
cheers
chris
On 07/11/2013 04:36 PM, Christian Sternagel wrote:
Dear all,
here is an update to my previous message. Corresponding patches are
attached (tested with `isabelle build_doc -pa` and `isabelle afp_build
-A`).
Some comments:
1) Variants are stored as terms but where all types are mapped to
"dummyT" (which makes it easier to check for a given term, whether it is
a variant of an overloaded constant).
2) In the table that maps overloaded constants to variants in addition
to the "dummy-typed" variant also a type is included (where all free
type variables are replaced by schematic ones).
3) As stated by Dmitriy in the "type unification" thread the current
solution does not work for localization (but the corresponding change is
trivial, I'm just avoiding it for the moment, since without localization
I have to work with a thy, which is inconvenient to turn into a ctxt as
required by Variable.polymorphic).
cheers
chris
On 07/10/2013 04:38 PM, Christian Sternagel wrote:
First of all, thanks for all the useful answers and sorry for my late
reply (I visited a conference and had some holidays ;)). As Alexander
suggested, I first tried to modify the existing adhoc_overloading.ML in
such a way that variants may be arbitrary terms. Please find the results
of my attempt attached (the new adhoc_overloading.ML as well as a
patch-file). Now I will investigate further localization.
Any comments are welcome.
cheers
chris
On 06/02/2013 08:55 AM, Alexander Krauss wrote:
Hi Chris,
I'm currently (as of changeset e6433b34364b) investigating whether it
would be possible to allow adhoc overloading (implemented in
~~/src/Tools/adhoc_overloading.ML) inside local contexts.
Nice!
For completeness find my current adhoc_overloading.ML attached
Apart from the various formalities pointed out by Makarius, here is
another concern, which relates to Florian's earlier question about how
local you want to be...
Currently, Adhoc_Overloading replaces constants with other constants,
which makes it global-only. Your current version tries to deal with
Frees similarly, it's not just that. Recall the example you gave
previously:
consts FOO :: ... (<some syntax>)
setup {* Adhoc_Overloading.add_overloaded @{const_name FOO} *}
locale foo =
fixes foo :: ...
assumes ...
begin
local_setup {*
Adhoc_Overloading.add_variant @{const_name FOO} @{term foo}
*}
Now consider the following interpretation:
interpretation foo "<some term>"
<proof>
Now, <some term> should become a variant of FOO, so at least the variant
side of the overloading relation must be an arbitrary term. With your
current code, the overloading would only survive interpretations where
foo happens to be mapped to a constant.
So, I guess that the overloaded constants should remain constants, since
they are just syntactic anyway. It seems that localizing those would be
rather artificial. But the variants must be properly localized and
subject to the morphism.
As a step towards proper localization, you could start with the global
code, and first generalize it to accept arbitrary terms as variants.
Note that this touches in particular the uncheck phase, which can no
longer use Term_Subst.map_aterms_same (or Term.map_aterms), since it
becomes general rewriting. One must resort to the more general
Pattern.rewrite_term here. When all this is working again, the actual
localization is then a mere formality, of which you have already
discovered the ingredients.
Makarius wrote:
* Same.function seems to be a let-over from the version by Alex
Krauss. He had that once in his function package, copied from
somewhere else (probably old code of mine).
No, it has nothing to do with the function package, which never used any
"Same" stuff. It just arose rather naturally from the requirement to
return NONE when nothing changes... So it was not meant as an
optimization.
There is no point to do
such low-level optimizations in the syntax layer. It is for hardcore
kernel operations only
So should I manually check the result for equality, or does the
framework do this for me?
Alex
diff -r 908304753f7d thys/JinjaThreads/Framework/FWState.thy
--- a/thys/JinjaThreads/Framework/FWState.thy Thu Jul 11 13:37:41 2013 +0200
+++ b/thys/JinjaThreads/Framework/FWState.thy Fri Jul 12 19:47:05 2013 +0900
@@ -188,15 +188,9 @@
"_ta_lock la l" == "CONST inject_thread_action (CONST Pair la l)"
"_ta_block (_ta_snoc btas bta)" == "CONST thread_action'_to_thread_action bta (_ta_block btas)"
-setup {*
- Adhoc_Overloading.add_overloaded @{const_name inject_thread_action}
- #> Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name NewThreadAction}
- #> Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name ConditionalAction}
- #> Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name WaitSetAction}
- #> Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name InterruptAction}
- #> Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name ObsAction}
- #> Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name LockAction}
-*}
+
+adhoc_overloading
+ inject_thread_action NewThreadAction ConditionalAction WaitSetAction InterruptAction ObsAction LockAction
lemma ta_upd_proj_simps [simp]:
shows ta_obs_proj_simps:
@@ -520,4 +514,4 @@
*}
typ "('l,'t,'x,'m,'w,'o) semantics"
-end
\ No newline at end of file
+end
diff -r 908304753f7d thys/Refine_Monadic/Refine_Basic.thy
--- a/thys/Refine_Monadic/Refine_Basic.thy Thu Jul 11 13:37:41 2013 +0200
+++ b/thys/Refine_Monadic/Refine_Basic.thy Fri Jul 12 19:47:05 2013 +0900
@@ -403,10 +403,8 @@
lemma bind_RES: "bind (RES X) f = Sup (f`X)" unfolding bind_def
by (auto)
-setup {*
- Adhoc_Overloading.add_variant
- @{const_name Monad_Syntax.bind} @{const_name bind}
-*}
+adhoc_overloading
+ Monad_Syntax.bind Refine_Basic.bind
lemma pw_bind_nofail[refine_pw_simps]:
"nofail (bind M f) \<longleftrightarrow> (nofail M \<and> (\<forall>x. inres M x \<longrightarrow> nofail (f x)))"
@@ -802,7 +800,6 @@
lemma Let_rule[refine_vcg]:
"f x \<le> SPEC \<Phi> \<Longrightarrow> Let x f \<le> SPEC \<Phi>" by auto
-
text {* The following lemma shows that greatest and least fixed point are equal,
if we can provide a variant. *}
thm RECT_eq_REC
diff -r 908304753f7d thys/Refine_Monadic/Refine_Det.thy
--- a/thys/Refine_Monadic/Refine_Det.thy Thu Jul 11 13:37:41 2013 +0200
+++ b/thys/Refine_Monadic/Refine_Det.thy Fri Jul 12 19:47:05 2013 +0900
@@ -271,10 +271,8 @@
by pat_completeness auto
termination by lexicographic_order
-setup {*
- Adhoc_Overloading.add_variant
- @{const_name Monad_Syntax.bind} @{const_name dbind}
-*}
+adhoc_overloading
+ Monad_Syntax.bind dbind
lemma [code]:
"dbind (dRETURN x) f = f x"
diff -r 908304753f7d thys/Shivers-CFA/AbsCFCorrect.thy
--- a/thys/Shivers-CFA/AbsCFCorrect.thy Thu Jul 11 13:37:41 2013 +0200
+++ b/thys/Shivers-CFA/AbsCFCorrect.thy Fri Jul 12 19:47:05 2013 +0900
@@ -39,19 +39,20 @@
consts abs :: "'a \<Rightarrow> 'b" ("|_|")
-setup {* Adhoc_Overloading.add_overloaded @{const_name abs} *}
-
-setup {* Adhoc_Overloading.add_variant @{const_name abs} @{const_name abs_cnt} *}
+adhoc_overloading
+ abs abs_cnt
definition abs_benv :: "benv \<Rightarrow> 'c::contour_a \<abenv>"
where "abs_benv \<beta> = Option.map abs_cnt \<circ> \<beta>"
-setup {* Adhoc_Overloading.add_variant @{const_name abs} @{const_name abs_benv} *}
+adhoc_overloading
+ abs abs_benv
primrec abs_closure :: "closure \<Rightarrow> 'c::contour_a \<aclosure>"
where "abs_closure (l,\<beta>) = (l,|\<beta>| )"
-setup {* Adhoc_Overloading.add_variant @{const_name abs} @{const_name abs_closure} *}
+adhoc_overloading
+ abs abs_closure
primrec abs_d :: "d \<Rightarrow> 'c::contour_a \<ad>"
where "abs_d (DI i) = {}"
@@ -59,29 +60,34 @@
| "abs_d (DC cl) = {PC |cl|}"
| "abs_d (Stop) = {AStop}"
-setup {* Adhoc_Overloading.add_variant @{const_name abs} @{const_name abs_d} *}
+adhoc_overloading
+ abs abs_d
definition abs_venv :: "venv \<Rightarrow> 'c::contour_a \<avenv>"
where "abs_venv ve = (\<lambda>(v,b_a). \<Union>{(case ve (v,b) of Some d \<Rightarrow> |d| | None \<Rightarrow> {}) | b. |b| = b_a })"
-setup {* Adhoc_Overloading.add_variant @{const_name abs} @{const_name abs_venv} *}
+adhoc_overloading
+ abs abs_venv
definition abs_ccache :: "ccache \<Rightarrow> 'c::contour_a \<accache>"
where "abs_ccache cc = (\<Union>((c,\<beta>),d) \<in> cc . {((c,abs_benv \<beta>), p) | p . p\<in>abs_d d})"
(* equivalent, but I already have cont2cont for UNION
where "abs_ccache cc = { ((c,abs_benv \<beta>),p) | c \<beta> p d . ((c,\<beta>),d) \<in> cc \<and> p \<in> abs_d d}" *)
-setup {* Adhoc_Overloading.add_variant @{const_name abs} @{const_name abs_ccache} *}
+adhoc_overloading
+ abs abs_ccache
fun abs_fstate :: "fstate \<Rightarrow> 'c::contour_a \<afstate>"
where "abs_fstate (d,ds,ve,b) = (the_elem |d|, map abs_d ds, |ve|, |b| )"
-setup {* Adhoc_Overloading.add_variant @{const_name abs} @{const_name abs_fstate} *}
+adhoc_overloading
+ abs abs_fstate
fun abs_cstate :: "cstate \<Rightarrow> 'c::contour_a \<acstate>"
where "abs_cstate (c,\<beta>,ve,b) = (c, |\<beta>|, |ve|, |b| )"
-setup {* Adhoc_Overloading.add_variant @{const_name abs} @{const_name abs_cstate} *}
+adhoc_overloading
+ abs abs_cstate
subsection {* Lemmas about abstraction functions *}
@@ -117,36 +123,42 @@
consts approx :: "'a \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<lessapprox> _")
-setup {* Adhoc_Overloading.add_overloaded @{const_name approx} *}
-
definition venv_approx :: "'c \<avenv> \<Rightarrow>'c \<avenv> \<Rightarrow> bool"
where "venv_approx = smap_less"
-setup {* Adhoc_Overloading.add_variant @{const_name approx} @{const_name venv_approx} *}
+adhoc_overloading
+ approx venv_approx
definition ccache_approx :: "'c \<accache> \<Rightarrow>'c \<accache> \<Rightarrow> bool"
where "ccache_approx = less_eq"
-setup {* Adhoc_Overloading.add_variant @{const_name approx} @{const_name ccache_approx} *}
+adhoc_overloading
+ approx ccache_approx
definition d_approx :: "'c \<ad> \<Rightarrow>'c \<ad> \<Rightarrow> bool"
where "d_approx = less_eq"
-setup {* Adhoc_Overloading.add_variant @{const_name approx} @{const_name d_approx} *}
+adhoc_overloading
+ approx d_approx
definition ds_approx :: "'c \<ad> list \<Rightarrow>'c \<ad> list \<Rightarrow> bool"
where "ds_approx = list_all2 d_approx"
-setup {* Adhoc_Overloading.add_variant @{const_name approx} @{const_name ds_approx} *}
+adhoc_overloading
+ approx ds_approx
inductive fstate_approx :: "'c \<afstate> \<Rightarrow>'c \<afstate> \<Rightarrow> bool"
where "\<lbrakk> ve \<lessapprox> ve' ; ds \<lessapprox> ds' \<rbrakk>
\<Longrightarrow> fstate_approx (proc,ds,ve,b) (proc,ds',ve',b)"
-setup {* Adhoc_Overloading.add_variant @{const_name approx} @{const_name fstate_approx} *}
+
+adhoc_overloading
+ approx fstate_approx
inductive cstate_approx :: "'c \<acstate> \<Rightarrow>'c \<acstate> \<Rightarrow> bool"
where "\<lbrakk> ve \<lessapprox> ve' \<rbrakk> \<Longrightarrow> cstate_approx (c,\<beta>,ve,b) (c,\<beta>,ve',b)"
-setup {* Adhoc_Overloading.add_variant @{const_name approx} @{const_name cstate_approx} *}
+
+adhoc_overloading
+ approx cstate_approx
subsection {* Lemmas about the approximation relation *}
diff -r 8afb396d9178 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jul 11 21:34:50 2013 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Jul 12 19:19:43 2013 +0900
@@ -274,10 +274,8 @@
Some (x, h') \<Rightarrow> execute (g x) h'
| None \<Rightarrow> None)"
-setup {*
- Adhoc_Overloading.add_variant
- @{const_name Monad_Syntax.bind} @{const_name Heap_Monad.bind}
-*}
+adhoc_overloading
+ Monad_Syntax.bind Heap_Monad.bind
lemma execute_bind [execute_simps]:
"execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
diff -r 8afb396d9178 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy Thu Jul 11 21:34:50 2013 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy Fri Jul 12 19:19:43 2013 +0900
@@ -69,12 +69,7 @@
"_do_block (_do_final e)" => "e"
"(m >> n)" => "(m >>= (\<lambda>_. n))"
-setup {*
- Adhoc_Overloading.add_overloaded @{const_name bind}
- #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
- #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
- #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
- #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name List.bind}
-*}
+adhoc_overloading
+ bind Set.bind Predicate.bind Option.bind List.bind
end
diff -r 8afb396d9178 src/Tools/Adhoc_Overloading.thy
--- a/src/Tools/Adhoc_Overloading.thy Thu Jul 11 21:34:50 2013 +0200
+++ b/src/Tools/Adhoc_Overloading.thy Fri Jul 12 19:19:43 2013 +0900
@@ -6,10 +6,10 @@
theory Adhoc_Overloading
imports Pure
+keywords "adhoc_overloading" :: thy_decl and "no_adhoc_overloading" :: thy_decl
begin
ML_file "adhoc_overloading.ML"
-setup Adhoc_Overloading.setup
end
diff -r 8afb396d9178 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML Thu Jul 11 21:34:50 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML Fri Jul 12 19:19:43 2013 +0900
@@ -6,11 +6,14 @@
signature ADHOC_OVERLOADING =
sig
- val add_overloaded: string -> theory -> theory
- val add_variant: string -> string -> theory -> theory
-
+ 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
- val setup: theory -> theory
end
structure Adhoc_Overloading: ADHOC_OVERLOADING =
@@ -18,122 +21,208 @@
val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false);
-
(* errors *)
-fun duplicate_variant_err int_name ext_name =
- error ("Constant " ^ quote int_name ^ " is already a variant of " ^ quote ext_name);
+fun duplicate_variant_error oconst =
+ error ("Duplicate variant of " ^ quote oconst);
-fun not_overloaded_err name =
- error ("Constant " ^ quote name ^ " is not declared as overloaded");
+fun not_a_variant_error oconst =
+ error ("Not a variant of " ^ quote oconst);
-fun already_overloaded_err name =
- error ("Constant " ^ quote name ^ " is already declared as overloaded");
+fun not_overloaded_error oconst =
+ error ("Constant " ^ quote oconst ^ " is not declared as overloaded");
-fun unresolved_err ctxt (c, T) t reason =
- error ("Unresolved overloading of " ^ quote c ^ " :: " ^
+fun unresolved_overloading_error ctxt (c, T) t reason =
+ error ("Unresolved overloading of " ^ quote c ^ " :: " ^
quote (Syntax.string_of_typ ctxt T) ^ " in " ^
quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
+(* generic data *)
-(* theory data *)
+fun variants_eq ((v1, T1), (v2, T2)) =
+ Term.aconv_untyped (v1, v2) andalso T1 = T2;
-structure Overload_Data = Theory_Data
+structure Overload_Data = Generic_Data
(
type T =
- { internalize : (string * typ) list Symtab.table,
- externalize : string Symtab.table };
- val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
+ {variants : (term * typ) list Symtab.table,
+ oconsts : string Termtab.table};
+ val empty = {variants = Symtab.empty, oconsts = Termtab.empty};
val extend = I;
- fun merge_ext int_name (ext_name1, ext_name2) =
- if ext_name1 = ext_name2 then ext_name1
- else duplicate_variant_err int_name ext_name1;
-
fun merge
- ({internalize = int1, externalize = ext1},
- {internalize = int2, externalize = ext2}) : T =
- {internalize = Symtab.merge_list (op =) (int1, int2),
- externalize = Symtab.join merge_ext (ext1, ext2)};
+ ({variants = vtab1, oconsts = otab1},
+ {variants = vtab2, oconsts = otab2}) : T =
+ let
+ fun merge_oconsts _ (oconst1, oconst2) =
+ if oconst1 = oconst2 then oconst1
+ else duplicate_variant_error 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 {internalize=int, externalize=ext} =>
- {internalize=f int, externalize=g ext});
+ Overload_Data.map (fn {variants = vtab, oconsts = otab} =>
+ {variants = f vtab, oconsts = g otab});
-val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
-val get_variants = Symtab.lookup o #internalize o Overload_Data.get;
-val get_external = Symtab.lookup o #externalize o Overload_Data.get;
+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 add_overloaded ext_name thy =
- let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_err ext_name;
- in map_tables (Symtab.update (ext_name, [])) I thy end;
+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 add_variant ext_name name thy =
+fun generic_remove_overloaded oconst context =
let
- val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
- val _ =
- (case get_external thy name of
- NONE => ()
- | SOME gen' => duplicate_variant_err name gen');
- val T = Sign.the_const_type thy name;
+ 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
- map_tables (Symtab.cons_list (ext_name, (name, T)))
- (Symtab.update (name, ext_name)) thy
- end
+ if is_overloaded (Context.proof_of context) oconst then remove_oconst_and_variants context oconst
+ else not_overloaded_error 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 not_overloaded_error oconst;
+ val T = t |> singleton (Variable.polymorphic ctxt) |> 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' => duplicate_variant_error 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 not_a_variant_error 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 ctxt T1 (c, T2) =
+fun unifiable_with thy T1 (t, T2) =
let
- val thy = Proof_Context.theory_of ctxt;
val maxidx1 = Term.maxidx_of_typ T1;
val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
- val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2');
+ val maxidx2 = Term.maxidx_typ T2' maxidx1;
in
- (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
+ (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME t)
handle Type.TUNIFY => NONE
end;
-fun insert_internal_same ctxt t (Const (c, T)) =
- (case map_filter (unifiable_with ctxt T)
- (Same.function (get_variants (Proof_Context.theory_of ctxt)) c) of
- [] => unresolved_err ctxt (c, T) t "no instances"
- | [c'] => Const (c', dummyT)
+fun insert_variants_same ctxt t (Const (c, T)) =
+ (case map_filter (unifiable_with (Proof_Context.theory_of ctxt) T)
+ (Same.function (get_variants ctxt) c) of
+ [] => unresolved_overloading_error ctxt (c, T) t "no instances"
+ | [variant] => variant
| _ => raise Same.SAME)
- | insert_internal_same _ _ _ = raise Same.SAME;
+ | insert_variants_same _ _ _ = raise Same.SAME;
-fun insert_external_same ctxt _ (Const (c, T)) =
- Const (Same.function (get_external (Proof_Context.theory_of ctxt)) c, T)
- | insert_external_same _ _ _ = raise Same.SAME;
+fun insert_overloaded_same ctxt variant =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val t = Pattern.rewrite_term thy [] [fn t =>
+ Term.map_types (K dummyT) t
+ |> get_overloaded ctxt
+ |> Option.map (Const o rpair (fastype_of variant))] variant;
+ in
+ if Term.aconv_untyped (variant, t) then raise Same.SAME
+ else t
+ end;
fun gen_check_uncheck replace ts ctxt =
- Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts
+ Same.capture (Same.map replace) ts
|> Option.map (rpair ctxt);
-val check = gen_check_uncheck insert_internal_same;
+fun check ts ctxt = gen_check_uncheck (fn t =>
+ Term_Subst.map_aterms_same (insert_variants_same ctxt t) t) ts ctxt;
fun uncheck ts ctxt =
if Config.get ctxt show_variants then NONE
- else gen_check_uncheck insert_external_same ts ctxt;
+ else gen_check_uncheck (insert_overloaded_same ctxt) ts ctxt;
fun reject_unresolved ts ctxt =
let
- val thy = Proof_Context.theory_of ctxt;
fun check_unresolved t =
- (case filter (is_overloaded thy o fst) (Term.add_consts t []) of
+ (case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of
[] => ()
- | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances");
+ | ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t "multiple instances");
val _ = map check_unresolved ts;
in NONE end;
-
(* setup *)
-val setup = Context.theory_map
+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 = fst o dest_Const o Proof_Context.read_const ctxt false dummyT;
+ val args =
+ raw_args
+ |> map (apfst (const_name lthy))
+ |> map (apsnd (map (Syntax.read_term lthy)));
+ in
+ Local_Theory.declaration {syntax = true, pervasive = false}
+ (adhoc_overloading_cmd' add args) lthy
+ end;
+
+val _ =
+ Outer_Syntax.local_theory @{command_spec "adhoc_overloading"}
+ "add ad-hoc overloading for constants / fixed variables"
+ (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd true);
+
+val _ =
+ Outer_Syntax.local_theory @{command_spec "no_adhoc_overloading"}
+ "add ad-hoc overloading for constants / fixed variables"
+ (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false);
+
end;
+
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
