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 aaec3f5a1ba6 thys/JinjaThreads/Framework/FWState.thy
--- a/thys/JinjaThreads/Framework/FWState.thy Wed Jul 10 15:19:23 2013 +0200
+++ b/thys/JinjaThreads/Framework/FWState.thy Thu Jul 11 16:30:08 2013 +0900
@@ -190,12 +190,12 @@
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.add_variant @{const_name inject_thread_action} @{term NewThreadAction}
+ #> Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{term ConditionalAction}
+ #> Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{term WaitSetAction}
+ #> Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{term InterruptAction}
+ #> Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{term ObsAction}
+ #> Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{term LockAction}
*}
lemma ta_upd_proj_simps [simp]:
@@ -520,4 +520,4 @@
*}
typ "('l,'t,'x,'m,'w,'o) semantics"
-end
\ No newline at end of file
+end
diff -r aaec3f5a1ba6 thys/Refine_Monadic/Refine_Basic.thy
--- a/thys/Refine_Monadic/Refine_Basic.thy Wed Jul 10 15:19:23 2013 +0200
+++ b/thys/Refine_Monadic/Refine_Basic.thy Thu Jul 11 16:30:08 2013 +0900
@@ -405,7 +405,7 @@
setup {*
Adhoc_Overloading.add_variant
- @{const_name Monad_Syntax.bind} @{const_name bind}
+ @{const_name Monad_Syntax.bind} @{term Refine_Basic.bind}
*}
lemma pw_bind_nofail[refine_pw_simps]:
@@ -802,7 +802,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 aaec3f5a1ba6 thys/Refine_Monadic/Refine_Det.thy
--- a/thys/Refine_Monadic/Refine_Det.thy Wed Jul 10 15:19:23 2013 +0200
+++ b/thys/Refine_Monadic/Refine_Det.thy Thu Jul 11 16:30:08 2013 +0900
@@ -273,7 +273,7 @@
setup {*
Adhoc_Overloading.add_variant
- @{const_name Monad_Syntax.bind} @{const_name dbind}
+ @{const_name Monad_Syntax.bind} @{term dbind}
*}
lemma [code]:
diff -r aaec3f5a1ba6 thys/Shivers-CFA/AbsCFCorrect.thy
--- a/thys/Shivers-CFA/AbsCFCorrect.thy Wed Jul 10 15:19:23 2013 +0200
+++ b/thys/Shivers-CFA/AbsCFCorrect.thy Thu Jul 11 16:30:08 2013 +0900
@@ -41,17 +41,17 @@
setup {* Adhoc_Overloading.add_overloaded @{const_name abs} *}
-setup {* Adhoc_Overloading.add_variant @{const_name abs} @{const_name abs_cnt} *}
+setup {* Adhoc_Overloading.add_variant @{const_name abs} @{term 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} *}
+setup {* Adhoc_Overloading.add_variant @{const_name abs} @{term 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} *}
+setup {* Adhoc_Overloading.add_variant @{const_name abs} @{term abs_closure} *}
primrec abs_d :: "d \<Rightarrow> 'c::contour_a \<ad>"
where "abs_d (DI i) = {}"
@@ -59,29 +59,29 @@
| "abs_d (DC cl) = {PC |cl|}"
| "abs_d (Stop) = {AStop}"
-setup {* Adhoc_Overloading.add_variant @{const_name abs} @{const_name abs_d} *}
+setup {* Adhoc_Overloading.add_variant @{const_name abs} @{term 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} *}
+setup {* Adhoc_Overloading.add_variant @{const_name abs} @{term 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} *}
+setup {* Adhoc_Overloading.add_variant @{const_name abs} @{term 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} *}
+setup {* Adhoc_Overloading.add_variant @{const_name abs} @{term 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} *}
+setup {* Adhoc_Overloading.add_variant @{const_name abs} @{term abs_cstate} *}
subsection {* Lemmas about abstraction functions *}
@@ -122,31 +122,31 @@
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} *}
+setup {* Adhoc_Overloading.add_variant @{const_name approx} @{term 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} *}
+setup {* Adhoc_Overloading.add_variant @{const_name approx} @{term 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} *}
+setup {* Adhoc_Overloading.add_variant @{const_name approx} @{term 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} *}
+setup {* Adhoc_Overloading.add_variant @{const_name approx} @{term 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} *}
+setup {* Adhoc_Overloading.add_variant @{const_name approx} @{term 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} *}
+setup {* Adhoc_Overloading.add_variant @{const_name approx} @{term cstate_approx} *}
subsection {* Lemmas about the approximation relation *}
diff -r ff525a38dba9 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Jul 10 23:30:10 2013 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jul 11 16:29:31 2013 +0900
@@ -276,7 +276,7 @@
setup {*
Adhoc_Overloading.add_variant
- @{const_name Monad_Syntax.bind} @{const_name Heap_Monad.bind}
+ @{const_name Monad_Syntax.bind} @{term Heap_Monad.bind}
*}
lemma execute_bind [execute_simps]:
diff -r ff525a38dba9 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy Wed Jul 10 23:30:10 2013 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy Thu Jul 11 16:29:31 2013 +0900
@@ -71,10 +71,10 @@
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.add_variant @{const_name bind} @{term Set.bind}
+ #> Adhoc_Overloading.add_variant @{const_name bind} @{term Predicate.bind}
+ #> Adhoc_Overloading.add_variant @{const_name bind} @{term Option.bind}
+ #> Adhoc_Overloading.add_variant @{const_name bind} @{term List.bind}
*}
end
diff -r ff525a38dba9 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML Wed Jul 10 23:30:10 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML Thu Jul 11 16:29:31 2013 +0900
@@ -7,7 +7,7 @@
signature ADHOC_OVERLOADING =
sig
val add_overloaded: string -> theory -> theory
- val add_variant: string -> string -> theory -> theory
+ val add_variant: string -> term -> theory -> theory
val show_variants: bool Config.T
val setup: theory -> theory
@@ -21,17 +21,17 @@
(* 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 ext_name =
+ error ("Duplicate variant of " ^ quote ext_name);
-fun not_overloaded_err name =
+fun not_overloaded_error name =
error ("Constant " ^ quote name ^ " is not declared as overloaded");
-fun already_overloaded_err name =
+fun already_overloaded_error name =
error ("Constant " ^ quote name ^ " is already 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 ^ ")");
@@ -41,82 +41,92 @@
structure Overload_Data = Theory_Data
(
type T =
- { internalize : (string * typ) list Symtab.table,
- externalize : string Symtab.table };
- val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
+ {internalize : (term * typ) list Symtab.table,
+ externalize : string Termtab.table};
+ val empty = {internalize = Symtab.empty, externalize = Termtab.empty};
val extend = I;
- fun merge_ext int_name (ext_name1, ext_name2) =
+ fun merge_ext _ (ext_name1, ext_name2) =
if ext_name1 = ext_name2 then ext_name1
- else duplicate_variant_err int_name ext_name1;
+ else duplicate_variant_error ext_name1;
fun merge
({internalize = int1, externalize = ext1},
- {internalize = int2, externalize = ext2}) : T =
+ {internalize = int2, externalize = ext2}) : T =
{internalize = Symtab.merge_list (op =) (int1, int2),
- externalize = Symtab.join merge_ext (ext1, ext2)};
+ externalize = Termtab.join merge_ext (ext1, ext2)};
);
fun map_tables f g =
- Overload_Data.map (fn {internalize=int, externalize=ext} =>
- {internalize=f int, externalize=g ext});
+ Overload_Data.map (fn {internalize = int, externalize = ext} =>
+ {internalize = f int, externalize = g ext});
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 get_external = Termtab.lookup o #externalize o Overload_Data.get;
fun add_overloaded ext_name thy =
- let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_err ext_name;
+ let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_error ext_name;
in map_tables (Symtab.update (ext_name, [])) I thy end;
-fun add_variant ext_name name thy =
+fun add_variant ext_name t thy =
let
- val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
+ val _ = is_overloaded thy ext_name orelse not_overloaded_error ext_name;
+ val T = Term.type_of t |> Term.map_type_tfree (TVar o apfst (rpair 0));
+ val variant = Term.map_types (K dummyT) t;
val _ =
- (case get_external thy name of
+ (case get_external thy variant of
NONE => ()
- | SOME gen' => duplicate_variant_err name gen');
- val T = Sign.the_const_type thy name;
+ | SOME gen' => duplicate_variant_error gen');
in
- map_tables (Symtab.cons_list (ext_name, (name, T)))
- (Symtab.update (name, ext_name)) thy
+ map_tables (Symtab.cons_list (ext_name, (variant, T)))
+ (Termtab.update (variant, ext_name)) thy
end
(* check / uncheck *)
-fun unifiable_with ctxt T1 (c, T2) =
+fun unifiable_with ctxt T1 (variant, 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');
in
- (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
+ (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME variant)
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)
+ [] => unresolved_overloading_error ctxt (c, T) t "no instances"
+ | [variant] => variant
| _ => raise Same.SAME)
| insert_internal_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_external_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_external thy
+ |> 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_internal_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_external_same ctxt) ts ctxt;
fun reject_unresolved ts ctxt =
let
@@ -124,7 +134,7 @@
fun check_unresolved t =
(case filter (is_overloaded thy 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;
@@ -137,3 +147,4 @@
#> Syntax_Phases.term_uncheck' 0 "adhoc_overloading" uncheck);
end;
+
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
