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_listparses "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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
(* 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;
Adhoc_Overloading.thy
Description: application/example
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
