[isabelle-dev] adhoc overloading
Christian Sternagel
c.sternagel at gmail.com
Fri May 31 05:53:21 CEST 2013
Dear all,
as I said earlier I am trying to make some changes (in Generic_Data)
persistent from inside a command. (My special case is ad-hoc
overloading, but I think that is irrelevant for the following.)
My current setup is (could you please point out any inadequate choices):
- To set up a command ("adhoc_overloading" in my case) that should also
work inside local contexts I use "Outer_Syntax.local_theory".
- For data related to the command I use "Generic_Data" (since it should
be available in top-level theories as well as local contexts).
- Investigating "notation" a bit (but not understanding the
implementation details ;)), I suspect that "Local_Theory.declaration" is
used to make changes in my "Generic_Data" persistent. What is the
purpose of the "{syntax: bool, pervasive: bool}" argument of
"Local_Theory.declaration".
- "Local_Theory.declaration" expects a "declaration" as argument, which
abbreviates the type "morphism -> Context.generic -> Context.generic".
For the time being I just ignore "morphism" (of course I will have to
understand and incorporate it at some point). So my declaration is
essentially a call to "Context.mapping" which takes two mappings: "f"
for "theory -> theory" and "g" for "Proof.context -> Proof.context".
- So far so good. Everything compiles fine. When I actually use my newly
defined command, I get the error "Stale theory encountered". So
obviously I'm doing something wrong in the above "f" (if I replace "f"
by "I" the error disappears, but of course then I can also not make
changes in my "Generic_Data" persistent.)
- Even if "f" is replaced by "I" above, something I do not understand
happens w.r.t. "g". But this is specific to my "adhoc_overloading" so I
have to give some more details:
adhoc_overloading
foo foo_list
parses "foo" and "foo_list" with "Parse.const" and preprocesses all its
arguments by "Proof_Context.read_const ctxt false dummyT", which I
thought was the canonical way to check whether a string is a (locally
fixed) constant.
Now inside a local context
context
fixes foo_nat :: nat
begin
I try
adhoc_overloading
foo foo_nat
And obtain
Unknown constant: "foo_nat"
When adding some "debug output" to my internal function I obtain the
following before the error:
checking constant: "foo"
const
DONE.
checking constant: "foo_nat"
free
DONE.
checking constant: "foo"
const
DONE.
checking constant: "foo_nat
Unknown constant: "foo_nat"
Which tells me that once "foo_nat" is parsed as a locally fixed constant
(represented by a Free variable) as expected. What I did not expect was
that all the arguments are considered a second time (so actually "g" is
called twice). In this second run we are apparently in a different
context, since "foo_nat" is no longer locally fixed. I'm sure that this
is the correct behavior, but maybe someone could explain it to me.
For completeness find my current adhoc_overloading.ML attached (but be
aware that it is far from finished; it is merely a sandbox in which I
play to find out more about the internals of Isabelle).
Sorry for the lengthy email, but it's really hard to find your way
through the existing Isabelle/ML API without professional help ;)
cheers
chris
On 05/31/2013 06:08 AM, Makarius wrote:
> On Wed, 29 May 2013, Florian Haftmann wrote:
>
>> Alternatively, use Context.>> directly in the body of the ML file
>> (which, I guess, is nowadays preferred over explicit setup in the
>> surrounding theory).
>
> Hypersearch over the sources shows that Context.>> is still quite rare,
> and there is no trend to be seen yet. Of course, a trend could be
> started now.
>
> Last time we've discussed that privately, you were more in favour of
> setup and I more in favour of Context.>> (quite some years ago).
>
> I am myself used to Context.>> in Isabelle/Pure (there is no other way),
> and I follow the old habit with 'setup' in Isabelle/HOL most of the time.
> On the other hand, the received two-part idiom is a bit odd wrt. proper
> modularity:
>
> ML_file "foo.ML"
> setup Foo.setup
>
> Like two-component glue to be fit together by hand. It used to be three
> components until recently, with extra "uses" in the theory header.
>
>
> Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
(* 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 is_overloaded: Context.generic -> string -> bool
val overload: bool -> string -> Context.generic -> Context.generic
val variant: bool -> string -> (string * typ) -> Context.generic -> Context.generic
val show_overloaded: bool Config.T
end
structure Adhoc_Overloading: ADHOC_OVERLOADING =
struct
val show_overloaded = Attrib.setup_config_bool @{binding show_overloaded} (K true);
(* errors *)
fun already_overloaded_error oconst =
error ("Constant " ^ quote oconst ^ " is already declared as overloaded");
fun duplicate_variant_error variant oconst =
error ("Constant " ^ quote variant ^ " is already a variant of " ^ quote oconst);
fun not_a_variant_error variant oconst =
error ("Constant " ^ quote variant ^ " is not a variant of " ^ quote oconst);
fun not_overloaded_error oconst =
error ("Constant " ^ quote oconst ^ " is not declared as overloaded");
fun unresolved_overloading_error context (c, T) t reason =
let val ctxt = Context.proof_of context
in
error ("Unresolved overloading of " ^ quote c ^ " :: " ^
quote (Syntax.string_of_typ ctxt T) ^ " in " ^
quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")")
end;
(* generic data *)
structure Overload_Data = Generic_Data
(
type T =
{variant_tab : (string * typ) list Symtab.table,
oconst_tab : string Symtab.table};
val empty = {variant_tab = Symtab.empty, oconst_tab = Symtab.empty};
val extend = I;
fun merge
({variant_tab = vtab1, oconst_tab = otab1},
{variant_tab = vtab2, oconst_tab = otab2}) : T =
let
fun merge_oconsts variant (oconst1, oconst2) =
if oconst1 = oconst2 then oconst1
else duplicate_variant_error variant oconst1;
in
{variant_tab = Symtab.merge_list (op =) (vtab1, vtab2),
oconst_tab = Symtab.join merge_oconsts (otab1, otab2)}
end;
);
fun map_tables f g =
Overload_Data.map (fn {variant_tab = vtab, oconst_tab = otab} =>
{variant_tab = f vtab, oconst_tab = g otab});
val is_overloaded = Symtab.defined o #variant_tab o Overload_Data.get;
val get_variants = Symtab.lookup o #variant_tab o Overload_Data.get;
val get_overloaded = Symtab.lookup o #oconst_tab o Overload_Data.get;
local
fun add_oconst context oconst = map_tables (Symtab.update (oconst, [])) I context;
fun remove_oconst_and_variants context oconst =
let
val remove_variants =
(case get_variants context oconst of
NONE => I
| SOME vs => fold (Symtab.remove (op =) o rpair oconst o fst) vs);
in map_tables (Symtab.delete oconst) remove_variants context end;
fun gen_overload default_add default_rm add oconst context =
if add then
if is_overloaded context oconst then default_add context oconst
else add_oconst context oconst
else
if is_overloaded context oconst then remove_oconst_and_variants context oconst
else default_rm context oconst;
in
val overload_permissive = gen_overload K K;
val overload = gen_overload (K already_overloaded_error) (K not_overloaded_error);
end
fun variant add oconst (var, T) context =
let
val _ = if is_overloaded context oconst then () else not_overloaded_error oconst;
in
if add then
let
val _ =
(case get_overloaded context var of
NONE => ()
| SOME oconst' => duplicate_variant_error var oconst');
in map_tables (Symtab.cons_list (oconst, (var, T))) (Symtab.update (var, oconst)) context end
else
let
val _ =
if member (op =) (the (get_variants context oconst)) (var, T) then ()
else not_a_variant_error var oconst
in
map_tables (Symtab.map_entry oconst (remove1 (op =) (var, T))) (Symtab.delete var) context
end
end
(* check / uncheck *)
fun unifiable_with context T1 (c, T2) =
let
val thy = Context.theory_of context;
val maxidx1 = Term.maxidx_of_typ T1;
val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
val maxidx2 = Term.maxidx_typ T2' maxidx1;
in
(Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2);
SOME c) handle Type.TUNIFY => NONE
end;
fun insert_variants_same context t (Const (c, T)) =
(case map_filter (unifiable_with context T)
(Same.function (get_variants context) c) of
[] => unresolved_overloading_error context (c, T) t "no instances"
| [c'] => Const (c', dummyT)
| _ => raise Same.SAME)
| insert_variants_same context t (Free (c, T)) =
(case map_filter (unifiable_with context T)
(Same.function (get_variants context) c) of
[] => unresolved_overloading_error context (c, T) t "no instances"
| [c'] => Free (c', dummyT)
| _ => raise Same.SAME)
| insert_variants_same _ _ _ = raise Same.SAME;
fun insert_overloaded_same context _ (Const (c, T)) =
Const (Same.function (get_overloaded context) c, T)
| insert_overloaded_same context _ (Free (c, T)) =
Const (Same.function (get_overloaded context) c, T)
| insert_overloaded_same _ _ _ = raise Same.SAME;
fun gen_check_uncheck replace ts ctxt =
Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace (Context.Proof ctxt) t) t)) ts
|> Option.map (rpair ctxt);
val check = gen_check_uncheck insert_variants_same;
fun uncheck ts ctxt =
if Config.get ctxt show_overloaded then
gen_check_uncheck insert_overloaded_same ts ctxt
else
NONE;
fun reject_unresolved ts ctxt =
let
val context = Context.Proof ctxt;
fun check_unresolved t =
(case filter (is_overloaded context o fst) ([] |> Term.add_consts t |> Term.add_frees t) of
[] => ()
| ((c, T) :: _) => unresolved_overloading_error context (c, T) t "multiple instances")
val _ = map check_unresolved ts;
in NONE 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 gen_overload prep_const add =
fold (fn (c, vs) =>
let val (oconst, _) = prep_const c;
in
overload_permissive add oconst
#> fold (variant add oconst o prep_const) vs
end);
in
fun overload_cmd add args context =
gen_overload (fn c =>
let
val lthy = Context.proof_of context;
val _ = writeln ("checking constant: " ^ quote c);
val r =
(case Proof_Context.read_const lthy false dummyT c of
Const (c, T) => (writeln "const"; (c, T))
| Free (c, T) => (writeln "free"; (c, T)))
val _ = writeln "DONE."
in r end)
add args context
end
fun generic_overload add args phi =
Context.mapping
I (*(Context.theory_map (overload_cmd add args))*)
(Context.proof_map (overload_cmd add args));
fun overload_cmd' add args =
Local_Theory.declaration {syntax = true, pervasive = false}
(generic_overload add args);
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.const) >> overload_cmd' true);
end;
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Adhoc_Overloading.thy
Type: application/x-example
Size: 291 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130531/6bb7feb6/attachment-0002.bin>
More information about the isabelle-dev
mailing list