*Moved from isabelle-users*
Thanks for the crucial hint Dmitriy!
Coming back to the original issue of Andreas, some explanation might be
in order.
What we did until now in adhoc_overloading.ML (more precisely, the
function "insert_variants") was to check for a given constant "c" of
type "T" whether there is a registered variant "v" whose type unifies
with "T". If so, "v" was inserted (but with all type-annotations
"flattened" to "dummyT"). After that we just hoped that type-inference
would do the trick. Apparently this worked quite well in many situations
(or maybe there are just not that many users of "adhoc_overloading" ;)).
Be that as it may. In Andreas' example this "flattening" of types leads
to somewhat unexpected results. Funnily (or maybe it was to be expected
but I don't know the details) everything worked out in top-level
thoeries. Somehow types are more polymorphic there (even though HOL is
not polymorphic at all ;)). With notepad and a fixed type "'b" the
problem occurred (and I guess the same would happen with locales).
(I'm not sure whether the TYPE_MATCH exception, which is not raised
inside adhoc_overloading.ML but caused by its result, is the best
problem-indicator for users here. Maybe there is also space for
improvement elsewhere. Comments?)
Anyway, attached is the following series of patches (to be applied in
this order):
delete - fixes a typo
drop_semicolons - drops semicolons
inst_unifier - uses the obtained unifier to instantiate the type of "v"
tune - misc tuning
With those applied (the important one is "inst_unifier")
"insert_variants" does the following. For a given constant "c" of type
"T", check whether there is a variant "v" of type T' such that T and T'
unify. If so, apply the obtained type-unifier to "v" and insert the
result instead of "c".
I hope this resolves your problem Andreas.
I tested the change on one of my local files that make heavy use of
adhoc overloading. Maybe someone could have a look, push the changes to
a test server, and push them to the main repo if everything is fine?
cheers
chris
On 11/23/2014 11:42 AM, Dmitriy Traytel wrote:
Hi Christian,
just a few weeks ago, I learned that Envir.subst_term_types is indeed
the wrong function when substituting with a unifier (instead it is
intended for matchers).
The right functions for unifiers in envir.ML are the ones prefixed with
"norm".
Hope that helps,
Dmitriy
On 22.11.2014 21:02, Christian Sternagel wrote:
I'm currently a bit confused by the result of "Sign.typ_unify" (or
rather the result of applying the corresponding "unifier"). So maybe
the problem stems from my ignorance w.r.t. to its intended result.
After applying the attached "debug" patch for the following
consts pure :: "'a ⇒ 'b"
definition pure_stream :: "'a ⇒ 'a stream"
where "pure_stream = sconst"
adhoc_overloading pure pure_stream
consts ap_stream :: "('a ⇒ 'b) stream ⇒ 'a stream ⇒ 'b stream"
(infixl "◇" 70)
consts S_stream :: "(('a ⇒ 'b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c) stream"
declare [[show_variants]]
term "pure id :: ('b ⇒ 'b) stream"
we obtain the output
oconst type: (??'a ⇒ ??'a) ⇒ ('b ⇒ 'b) stream
variant type: ?'a ⇒ ?'a stream
("unifier:",
{(("'a", 0), (["HOL.type"], "??'a ⇒ ??'a")),
(("?'a", 0),
(["HOL.type"],
"'b"))}) (line 165 of
"/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
("candidate term:",
Const ("Scratch.pure_stream",
"?'a
⇒ ?'a Stream.stream")) (line 167 of
"/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
("after unification:",
Const ("Scratch.pure_stream",
"(??'a ⇒ ??'a)
⇒ (??'a
⇒ ??'a) Stream.stream")) (line 168 of
"/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
"pure_stream id"
:: "('a ⇒ 'a) stream"
The result of unification is a bit surprising to me, since the
obtained "unifier" seems to claim that
('b => 'b) => ('b => 'b) stream
and
(??'a => ??'a) => (??'a => ??'a) stream
are equal. What am I missing here? Maybe Envir.subst_term_types is not
the way to apply the typenv obtained by typ_unify? (In this special
case, if I would call subst_term_types twice with the same typenv, the
result would be as I expected.)
cheers
chris
Btw: the "delete" patch (which is to be applied before "debug") fixes
a typo in the description of "no_adhoc_overloading". It is entirely
unrelated to the issue at hand, but maybe somebody could apply it anyway.
On 11/21/2014 07:31 PM, Christian Sternagel wrote:
Dear Andreas,
Thanks for the report, I'll have a look. First an immediate observation:
When adding the following to Scratch.thy
declare [[show_variants]]
notepad
begin
fix f :: "('b ⇒ 'b ⇒ 'a) stream"
and x :: "'b stream"
term "pure id :: ('b => 'b) stream"
the first "term" results in
"pure_stream id"
:: "('c ⇒ 'c) stream"
while the second results in
"pure_stream id"
:: "('b ⇒ 'b) stream"
So it is not surprising that the first causes problems while matching.
Why, however "'c" is produced instead of "'b" is not immediately clear
to me. I'll investigate.
cheers
chris
On 11/21/2014 04:09 PM, Andreas Lochbihler wrote:
Dear experts on adhoc overloading,
When I want to instantiate variables in a theorem using the attribute
"of", sometimes the exception TYPE_MATCH gets raised. This seems
strange
to me because I would expect that adhoc_overloading either complains
about not being able to uniquely resolve an overloaded constant or
exchanges the constant in the AST.
By adding more type annotations, I have so far been able to circumvent
the exception, but there seems to be a check missing. Attached you find
a small example.
Best,
Andreas
# HG changeset patch
# Parent be4a911aca712cc928d1f798488205ce7c5fac92
typo in description
diff -r be4a911aca71 -r f653343d16ba src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML Wed Nov 19 19:12:14 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML Fri Nov 21 19:58:22 2014 +0100
@@ -239,7 +239,7 @@
val _ =
Outer_Syntax.local_theory @{command_spec "no_adhoc_overloading"}
- "add adhoc overloading for constants / fixed variables"
+ "delete adhoc overloading for constants / fixed variables"
(Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >>
adhoc_overloading_cmd false);
end;
# HG changeset patch
# Parent 2b1505ca7ff4d324e4c595374c97fdcc8e4769bb
drop superfluous semicolons
diff -r 2b1505ca7ff4 -r 941653538854 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML Sun Nov 23 20:07:19 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML Sun Nov 23 20:09:38 2014 +0100
@@ -19,19 +19,19 @@
structure Adhoc_Overloading: ADHOC_OVERLOADING =
struct
-val show_variants = Attrib.setup_config_bool @{binding show_variants} (K
false);
+val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false)
(* errors *)
fun err_duplicate_variant oconst =
- error ("Duplicate variant of " ^ quote oconst);
+ error ("Duplicate variant of " ^ quote oconst)
fun err_not_a_variant oconst =
- error ("Not a variant of " ^ quote oconst);
+ error ("Not a variant of " ^ quote oconst)
fun err_not_overloaded oconst =
- error ("Constant " ^ quote oconst ^ " is not declared as overloaded");
+ error ("Constant " ^ quote oconst ^ " is not declared as overloaded")
fun err_unresolved_overloading ctxt0 (c, T) t instances =
let
@@ -51,21 +51,21 @@
else Pretty.fbreaks (
Pretty.str "multiple instances:" ::
map (Pretty.mark Markup.item o Syntax.pretty_term ctxt)
instances)))]))
- end;
+ end
(* generic data *)
fun variants_eq ((v1, T1), (v2, T2)) =
- Term.aconv_untyped (v1, v2) andalso T1 = T2;
+ Term.aconv_untyped (v1, v2) andalso T1 = T2
structure Overload_Data = Generic_Data
(
type T =
{variants : (term * typ) list Symtab.table,
- oconsts : string Termtab.table};
- val empty = {variants = Symtab.empty, oconsts = Termtab.empty};
- val extend = I;
+ oconsts : string Termtab.table}
+ val empty = {variants = Symtab.empty, oconsts = Termtab.empty}
+ val extend = I
fun merge
({variants = vtab1, oconsts = otab1},
@@ -73,24 +73,24 @@
let
fun merge_oconsts _ (oconst1, oconst2) =
if oconst1 = oconst2 then oconst1
- else err_duplicate_variant oconst1;
+ else err_duplicate_variant oconst1
in
{variants = Symtab.merge_list variants_eq (vtab1, vtab2),
oconsts = Termtab.join merge_oconsts (otab1, otab2)}
- end;
-);
+ end
+)
fun map_tables f g =
Overload_Data.map (fn {variants = vtab, oconsts = otab} =>
- {variants = f vtab, oconsts = g otab});
+ {variants = f vtab, oconsts = g otab})
-val is_overloaded = Symtab.defined o #variants o Overload_Data.get o
Context.Proof;
-val get_variants = Symtab.lookup o #variants o Overload_Data.get o
Context.Proof;
-val get_overloaded = Termtab.lookup o #oconsts o Overload_Data.get o
Context.Proof;
+val is_overloaded = Symtab.defined o #variants o Overload_Data.get o
Context.Proof
+val get_variants = Symtab.lookup o #variants o Overload_Data.get o
Context.Proof
+val get_overloaded = Termtab.lookup o #oconsts o Overload_Data.get o
Context.Proof
fun generic_add_overloaded oconst context =
if is_overloaded (Context.proof_of context) oconst then context
- else map_tables (Symtab.update (oconst, [])) I context;
+ else map_tables (Symtab.update (oconst, [])) I context
fun generic_remove_overloaded oconst context =
let
@@ -99,27 +99,27 @@
val remove_variants =
(case get_variants (Context.proof_of context) oconst of
NONE => I
- | SOME vs => fold (Termtab.remove (op =) o rpair oconst o fst) vs);
- in map_tables (Symtab.delete_safe oconst) remove_variants context end;
+ | SOME vs => fold (Termtab.remove (op =) o rpair oconst o fst) vs)
+ in map_tables (Symtab.delete_safe oconst) remove_variants context end
in
if is_overloaded (Context.proof_of context) oconst then
remove_oconst_and_variants context oconst
else err_not_overloaded oconst
- end;
+ end
local
fun generic_variant add oconst t context =
let
- val ctxt = Context.proof_of context;
- val _ = if is_overloaded ctxt oconst then () else err_not_overloaded
oconst;
- val T = t |> fastype_of;
- val t' = Term.map_types (K dummyT) t;
+ val ctxt = Context.proof_of context
+ val _ = if is_overloaded ctxt oconst then () else err_not_overloaded
oconst
+ val T = t |> fastype_of
+ val t' = Term.map_types (K dummyT) t
in
if add then
let
val _ =
(case get_overloaded ctxt t' of
NONE => ()
- | SOME oconst' => err_duplicate_variant oconst');
+ | SOME oconst' => err_duplicate_variant oconst')
in
map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t',
oconst)) context
end
@@ -127,7 +127,7 @@
let
val _ =
if member variants_eq (the (get_variants ctxt oconst)) (t', T)
then ()
- else err_not_a_variant oconst;
+ else err_not_a_variant oconst
in
map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T)))
(Termtab.delete_safe t') context
@@ -136,60 +136,60 @@
SOME [] => generic_remove_overloaded oconst context
| _ => context))
end
- end;
+ end
in
- val generic_add_variant = generic_variant true;
- val generic_remove_variant = generic_variant false;
-end;
+ val generic_add_variant = generic_variant true
+ val generic_remove_variant = generic_variant false
+end
(* check / uncheck *)
fun unifiable_with thy T1 T2 =
let
- val maxidx1 = Term.maxidx_of_typ T1;
- val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
- val maxidx2 = Term.maxidx_typ T2' maxidx1;
- in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end;
+ val maxidx1 = Term.maxidx_of_typ T1
+ val T2' = Logic.incr_tvar (maxidx1 + 1) T2
+ val maxidx2 = Term.maxidx_typ T2' maxidx1
+ in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end
fun get_candidates ctxt (c, T) =
get_variants ctxt c
|> Option.map (map_filter (fn (t, T') =>
if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t
- else NONE));
+ else NONE))
fun insert_variants ctxt t (oconst as Const (c, T)) =
(case get_candidates ctxt (c, T) of
SOME [] => err_unresolved_overloading ctxt (c, T) t []
| SOME [variant] => variant
| _ => oconst)
- | insert_variants _ _ oconst = oconst;
+ | insert_variants _ _ oconst = oconst
fun insert_overloaded ctxt =
let
fun proc t =
Term.map_types (K dummyT) t
|> get_overloaded ctxt
- |> Option.map (Const o rpair (Term.type_of t));
+ |> Option.map (Const o rpair (Term.type_of t))
in
Pattern.rewrite_term_top (Proof_Context.theory_of ctxt) [] [proc]
- end;
+ end
fun check ctxt =
- map (fn t => Term.map_aterms (insert_variants ctxt t) t);
+ map (fn t => Term.map_aterms (insert_variants ctxt t) t)
fun uncheck ctxt ts =
if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of)
ts then ts
- else map (insert_overloaded ctxt) ts;
+ else map (insert_overloaded ctxt) ts
fun reject_unresolved ctxt =
let
- val the_candidates = the o get_candidates ctxt;
+ val the_candidates = the o get_candidates ctxt
fun check_unresolved t =
(case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of
[] => t
- | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT));
- in map check_unresolved end;
+ | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT))
+ in map check_unresolved end
(* setup *)
@@ -197,7 +197,7 @@
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);
+ #> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck)
(* commands *)
@@ -209,38 +209,38 @@
#> fold (generic_add_variant oconst) ts)
else
fold (fn (oconst, ts) =>
- fold (generic_remove_variant oconst) ts);
+ fold (generic_remove_variant oconst) ts)
fun adhoc_overloading_cmd' add args phi =
let val args' = args
|> map (apsnd (map_filter (fn t =>
- let val t' = Morphism.term phi t;
- in if Term.aconv_untyped (t, t') then SOME t' else NONE end)));
- in generic_adhoc_overloading_cmd add args' end;
+ let val t' = Morphism.term phi t
+ in if Term.aconv_untyped (t, t') then SOME t' else NONE end)))
+ in generic_adhoc_overloading_cmd add args' end
fun adhoc_overloading_cmd add raw_args lthy =
let
fun const_name ctxt =
- fst o dest_Const o Proof_Context.read_const {proper = false, strict =
false} ctxt; (* FIXME {proper = true, strict = true} (!?) *)
- fun read_term ctxt = singleton (Variable.polymorphic ctxt) o
Syntax.read_term ctxt;
+ fst o dest_Const o Proof_Context.read_const {proper = false, strict =
false} ctxt (* FIXME {proper = true, strict = true} (!?) *)
+ fun read_term ctxt = singleton (Variable.polymorphic ctxt) o
Syntax.read_term ctxt
val args =
raw_args
|> map (apfst (const_name lthy))
- |> map (apsnd (map (read_term lthy)));
+ |> map (apsnd (map (read_term lthy)))
in
Local_Theory.declaration {syntax = true, pervasive = false}
(adhoc_overloading_cmd' add args) lthy
- end;
+ end
val _ =
Outer_Syntax.local_theory @{command_spec "adhoc_overloading"}
"add adhoc overloading for constants / fixed variables"
- (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >>
adhoc_overloading_cmd true);
+ (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >>
adhoc_overloading_cmd true)
val _ =
Outer_Syntax.local_theory @{command_spec "no_adhoc_overloading"}
"delete adhoc overloading for constants / fixed variables"
- (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >>
adhoc_overloading_cmd false);
+ (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >>
adhoc_overloading_cmd false)
-end;
+end
# HG changeset patch
# Parent c102f9684f087adce0e779c2c79c5ca3da09c90a
instantiate types by unifier
diff -r c102f9684f08 -r 65318a8ace19 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML Sun Nov 23 20:10:06 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML Sun Nov 23 20:23:27 2014 +0100
@@ -62,7 +62,7 @@
structure Overload_Data = Generic_Data
(
type T =
- {variants : (term * typ) list Symtab.table,
+ {variants : (term * typ) list Symtab.table, (*store type to avoid repeated
"fastype_of"*)
oconsts : string Termtab.table}
val empty = {variants = Symtab.empty, oconsts = Termtab.empty}
val extend = I
@@ -92,6 +92,8 @@
if is_overloaded (Context.proof_of context) oconst then context
else map_tables (Symtab.update (oconst, [])) I context
+val dummify_type = map_types (K dummyT)
+
fun generic_remove_overloaded oconst context =
let
fun remove_oconst_and_variants context oconst =
@@ -99,10 +101,11 @@
val remove_variants =
(case get_variants (Context.proof_of context) oconst of
NONE => I
- | SOME vs => fold (Termtab.remove (op =) o rpair oconst o fst) vs)
+ | SOME vs => fold (Termtab.remove (op =) o rpair oconst o
dummify_type o fst) vs)
in map_tables (Symtab.delete_safe oconst) remove_variants context end
in
- if is_overloaded (Context.proof_of context) oconst then
remove_oconst_and_variants context oconst
+ if is_overloaded (Context.proof_of context) oconst then
+ remove_oconst_and_variants context oconst
else err_not_overloaded oconst
end
@@ -110,9 +113,9 @@
fun generic_variant add oconst t context =
let
val ctxt = Context.proof_of context
- val _ = if is_overloaded ctxt oconst then () else err_not_overloaded
oconst
- val T = t |> fastype_of
- val t' = Term.map_types (K dummyT) t
+ val _ = is_overloaded ctxt oconst orelse err_not_overloaded oconst
+ val t_T = (t, fastype_of t)
+ val t' = dummify_type t
in
if add then
let
@@ -121,16 +124,14 @@
NONE => ()
| SOME oconst' => err_duplicate_variant oconst')
in
- map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t',
oconst)) context
+ map_tables (Symtab.cons_list (oconst, t_T)) (Termtab.update (t',
oconst)) context
end
else
let
- val _ =
- if member variants_eq (the (get_variants ctxt oconst)) (t', T)
then ()
- else err_not_a_variant oconst
+ val _ = member variants_eq (the (get_variants ctxt oconst)) t_T
orelse
+ err_not_a_variant oconst
in
- map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T)))
- (Termtab.delete_safe t') context
+ map_tables (Symtab.map_entry oconst (remove1 variants_eq t_T))
(Termtab.delete_safe t') context
|> (fn context =>
(case get_variants (Context.proof_of context) oconst of
SOME [] => generic_remove_overloaded oconst context
@@ -145,18 +146,26 @@
(* check / uncheck *)
-fun unifiable_with thy T1 T2 =
+fun unify_filter thy T1 (t, T2) =
let
val maxidx1 = Term.maxidx_of_typ T1
- val T2' = Logic.incr_tvar (maxidx1 + 1) T2
+ val incr = Logic.incr_tvar (maxidx1 + 1)
+ val (t', T2') = (map_types incr t, incr T2)
val maxidx2 = Term.maxidx_typ T2' maxidx1
- in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end
+ in
+ (case try (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) of
+ SOME (tyenv, maxidx) =>
+ let val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv =
tyenv}
+ in Envir.norm_term env t' |> SOME end
+ | NONE => NONE)
+ end
fun get_candidates ctxt (c, T) =
- get_variants ctxt c
- |> Option.map (map_filter (fn (t, T') =>
- if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t
- else NONE))
+ let val thy = Proof_Context.theory_of ctxt
+ in
+ get_variants ctxt c
+ |> Option.map (map_filter (unify_filter thy T))
+ end
fun insert_variants ctxt t (oconst as Const (c, T)) =
(case get_candidates ctxt (c, T) of
@@ -168,7 +177,7 @@
fun insert_overloaded ctxt =
let
fun proc t =
- Term.map_types (K dummyT) t
+ dummify_type t
|> get_overloaded ctxt
|> Option.map (Const o rpair (Term.type_of t))
in
# HG changeset patch
# Parent adc3e730fddd4418ebcbedd15cabf40bb4aec1ad
misc tuning
diff -r adc3e730fddd -r 6bf3e1e70444 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML Sun Nov 23 20:25:39 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML Sun Nov 23 20:55:08 2014 +0100
@@ -167,9 +167,9 @@
|> Option.map (map_filter (unify_filter thy T))
end
-fun insert_variants ctxt t (oconst as Const (c, T)) =
- (case get_candidates ctxt (c, T) of
- SOME [] => err_unresolved_overloading ctxt (c, T) t []
+fun insert_variants ctxt t (oconst as Const c_T) =
+ (case get_candidates ctxt c_T of
+ SOME [] => err_unresolved_overloading ctxt c_T t []
| SOME [variant] => variant
| _ => oconst)
| insert_variants _ _ oconst = oconst
@@ -197,7 +197,7 @@
fun check_unresolved t =
(case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of
[] => t
- | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT))
+ | (c_T :: _) => err_unresolved_overloading ctxt c_T t (the_candidates
c_T))
in map check_unresolved end
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
