[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" 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:

   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

     fixes foo_nat :: nat

I try

     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"
   checking constant: "foo_nat"
   checking constant: "foo"
   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 ;)



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.

  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

structure Adhoc_Overloading: ADHOC_OVERLOADING =

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
    error ("Unresolved overloading of " ^ quote c ^ " :: " ^
      quote (Syntax.string_of_typ ctxt T) ^ " in " ^
      quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")")

(* 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 =
      fun merge_oconsts variant (oconst1, oconst2) =
        if oconst1 = oconst2 then oconst1
        else duplicate_variant_error variant oconst1;
      {variant_tab = Symtab.merge_list (op =) (vtab1, vtab2),
       oconst_tab = Symtab.join merge_oconsts (otab1, otab2)}

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;

  fun add_oconst context oconst = map_tables (Symtab.update (oconst, [])) I context;

  fun remove_oconst_and_variants context oconst =
      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
      if is_overloaded context oconst then remove_oconst_and_variants context oconst
      else default_rm context oconst;
  val overload_permissive = gen_overload K K;
  val overload = gen_overload (K already_overloaded_error) (K not_overloaded_error);

fun variant add oconst (var, T) context =
    val _ = if is_overloaded context oconst then () else not_overloaded_error oconst;
    if add then
        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
        val _ =
          if member (op =) (the (get_variants context oconst)) (var, T) then ()
          else not_a_variant_error var oconst
        map_tables (Symtab.map_entry oconst (remove1 (op =) (var, T))) (Symtab.delete var) context

(* check / uncheck *)

fun unifiable_with context T1 (c, T2) =
    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;
    (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2);
     SOME c) handle Type.TUNIFY => NONE

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

fun reject_unresolved ts ctxt =
    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 *)
  fun gen_overload prep_const add =
    fold (fn (c, vs) =>
      let val (oconst, _) = prep_const c;
        overload_permissive add oconst
        #> fold (variant add oconst o prep_const) vs
  fun overload_cmd add args context =
    gen_overload (fn c =>
        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

fun generic_overload add args phi =
    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);


-------------- 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