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
(* Author: Alexander Krauss, TU Muenchen
Author: Christian Sternagel, University of Innsbruck
Ad-hoc overloading of constants based on their types.
*)
signature ADHOC_OVERLOADING =
sig
val add_overloaded: string -> theory -> theory
val add_variant: string -> term -> theory -> theory
val show_variants: bool Config.T
val setup: theory -> theory
end
structure Adhoc_Overloading: ADHOC_OVERLOADING =
struct
val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false);
(* errors *)
fun duplicate_variant_error ext_name =
error ("Duplicate variant of " ^ quote ext_name);
fun not_overloaded_error name =
error ("Constant " ^ quote name ^ " is not declared as overloaded");
fun already_overloaded_error name =
error ("Constant " ^ quote name ^ " is already declared as overloaded");
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 ^ ")");
(* theory data *)
structure Overload_Data = Theory_Data
(
type T =
{internalize : term list Symtab.table,
externalize : string Termtab.table};
val empty = {internalize = Symtab.empty, externalize = Termtab.empty};
val extend = I;
fun merge_ext _ (ext_name1, ext_name2) =
if ext_name1 = ext_name2 then ext_name1
else duplicate_variant_error ext_name1;
fun merge
({internalize = int1, externalize = ext1},
{internalize = int2, externalize = ext2}) : T =
{internalize = Symtab.merge_list (op aconv) (int1, int2),
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});
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 = 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_error
ext_name;
in map_tables (Symtab.update (ext_name, [])) I thy end;
fun add_variant ext_name variant thy =
let
val _ = is_overloaded thy ext_name orelse not_overloaded_error ext_name;
val _ =
(case get_external thy variant of
NONE => ()
| SOME gen' => duplicate_variant_error gen');
in
map_tables (Symtab.cons_list (ext_name, variant))
(Termtab.update (variant, ext_name)) thy
end
(* check / uncheck *)
fun unifiable_with ctxt T1 variant =
let
val T2 = fastype_of variant;
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 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_overloading_error ctxt (c, T) t "no instances"
| [variant] => variant
| _ => raise Same.SAME)
| insert_internal_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 =>
get_external thy t
|> Option.map (fn c => Const (c, fastype_of variant))] variant;
in if variant aconv t' then raise Same.SAME else t' end;
fun gen_check_uncheck replace ts ctxt =
Same.capture (Same.map replace) ts
|> Option.map (rpair ctxt);
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 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
[] => ()
| ((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
(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);
end;
10c10
< val add_variant: string -> string -> theory -> theory
---
> val add_variant: string -> term -> theory -> theory
24,25c24,25
< 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);
27c27
< fun not_overloaded_err name =
---
> fun not_overloaded_error name =
30c30
< fun already_overloaded_err name =
---
> fun already_overloaded_error name =
33c33
< fun unresolved_err ctxt (c, T) t reason =
---
> fun unresolved_overloading_error ctxt (c, T) t reason =
44,46c44,46
< { internalize : (string * typ) list Symtab.table,
< externalize : string Symtab.table };
< val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
---
> {internalize : term list Symtab.table,
> externalize : string Termtab.table};
> val empty = {internalize = Symtab.empty, externalize = Termtab.empty};
49c49
< fun merge_ext int_name (ext_name1, ext_name2) =
---
> fun merge_ext _ (ext_name1, ext_name2) =
51c51
< else duplicate_variant_err int_name ext_name1;
---
> else duplicate_variant_error ext_name1;
55,57c55,57
< {internalize = int2, externalize = ext2}) : T =
< {internalize = Symtab.merge_list (op =) (int1, int2),
< externalize = Symtab.join merge_ext (ext1, ext2)};
---
> {internalize = int2, externalize = ext2}) : T =
> {internalize = Symtab.merge_list (op aconv) (int1, int2),
> externalize = Termtab.join merge_ext (ext1, ext2)};
61,62c61,62
< 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});
66c66
< val get_external = Symtab.lookup o #externalize o Overload_Data.get;
---
> val get_external = Termtab.lookup o #externalize o Overload_Data.get;
69c69
< 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;
72c72
< fun add_variant ext_name name thy =
---
> fun add_variant ext_name variant thy =
74c74
< val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
---
> val _ = is_overloaded thy ext_name orelse not_overloaded_error ext_name;
76c76
< (case get_external thy name of
---
> (case get_external thy variant of
78,79c78
< | SOME gen' => duplicate_variant_err name gen');
< val T = Sign.the_const_type thy name;
---
> | SOME gen' => duplicate_variant_error gen');
81,82c80,81
< map_tables (Symtab.cons_list (ext_name, (name, T)))
< (Symtab.update (name, ext_name)) thy
---
> map_tables (Symtab.cons_list (ext_name, variant))
> (Termtab.update (variant, ext_name)) thy
88c87
< fun unifiable_with ctxt T1 (c, T2) =
---
> fun unifiable_with ctxt T1 variant =
89a89
> val T2 = fastype_of variant;
95c95
< (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
---
> (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME variant)
102,103c102,103
< [] => unresolved_err ctxt (c, T) t "no instances"
< | [c'] => Const (c', dummyT)
---
> [] => unresolved_overloading_error ctxt (c, T) t "no instances"
> | [variant] => variant
107,109c107,113
< 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 =>
> get_external thy t
> |> Option.map (fn c => Const (c, fastype_of variant))] variant;
> in if variant aconv t' then raise Same.SAME else t' end;
112c116
< Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts
---
> Same.capture (Same.map replace) ts
115c119,121
< 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;
119c125
< else gen_check_uncheck insert_external_same ts ctxt;
---
> else gen_check_uncheck (insert_external_same ctxt) ts ctxt;
127c133
< | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances");
---
> | ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t "multiple instances");
139a146
>
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
