[isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading
Christian Sternagel
c.sternagel at gmail.com
Sun Nov 23 21:20:18 CET 2014
*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
>
-------------- next part --------------
# 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;
-------------- next part --------------
# 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
-------------- next part --------------
# 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
-------------- next part --------------
# 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
More information about the isabelle-dev
mailing list