[isabelle-dev] TYPE_MATCH exception with adhoc_overloading
Christian Sternagel
c.sternagel at gmail.com
Wed Jan 28 13:37:37 CET 2015
During a visit of Florian in Innsbruck we had some discussion on adhoc
overloading. One suspicion was that schematic type variables from
variants had to be "paramified" before using the resulting type unifier.
I tried to do so in the attached patch. Unfortunately, I still obtain
the following error in
~~/src/HOL/ex/Adhoc_Overloading_Examples.thy
Illegal schematic type variable: ?'a2
Please let me know if you have any comments on this topic (especially on
what is going on in the function "unify_filter").
cheers
chris
On 01/20/2015 06:16 PM, Makarius wrote:
> On Mon, 19 Jan 2015, Jasmin Blanchette wrote:
>
>>> Just a reminder that this old thread is not yet resolved and
>>> currently I'm essentially stuck.
>>
>> I hope somebody who has a clue will answer your email.
>
> I still have various "important" markers on this mail thread, to see if
> I can tell something about it, but I did not manage to pick it up again.
> It will happen really soon now ...
>
>
>>> drop_semicolons
>>
>> I’ve applied and push your first change.
>>
>> As for semicolon, the standard style is rather to put them, not to
>> drop them.
>
> Strictly speaking there is no standard for semicolons in Isabelle/ML,
> only the universal standard of uniformity: a file either has extra
> semicolons or does not have extra semicolons.
>
>
> More than 20 years ago, semicolons where generally en-vogue, and no
> surprise for me in SML. Then they became less popular, e.g. in Scala we
> now see sophisticated rules for implicit "semicolon inference". The
> Isar language has lost its semicolon altogether some weeks ago
> (5ff61774df11).
>
> Over the decades I have occasionally experimented with writing less
> semicolons in ML, but each time I ran into practical inconveniences
> concerning error situations (broken partial input), and closed ML
> modules versus open sequences of declarations (e.g. in the 'ML' command).
>
> My present style of doing it (approx. the last 10 years) is somehow
> optimized in that respect. Whenever I do serious renovations on some
> old ML module, I first normalize the semicolon style (and other styles
> as well), just to save a lot of time in the actual work.
>
>
> Makarius
-------------- next part --------------
# HG changeset patch
# Parent 2538b2c51769f9e40c424644233f8f8c5cb6eac3
apply type-unifier before inserting variants
diff -r 2538b2c51769 -r 790518068cc2 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML Tue Jan 27 16:12:40 2015 +0100
+++ b/src/Tools/adhoc_overloading.ML Wed Jan 28 13:18:46 2015 +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;
@@ -84,6 +84,8 @@
Overload_Data.map (fn {variants = vtab, oconsts = otab} =>
{variants = f vtab, oconsts = g otab});
+val dummify_types = map_types (K dummyT)
+
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;
@@ -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_types 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_types t;
in
if add then
let
@@ -121,16 +124,15 @@
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
+ context
+ |> map_tables (Symtab.map_entry oconst (remove1 variants_eq t_T)) (Termtab.delete_safe t')
|> (fn context =>
(case get_variants (Context.proof_of context) oconst of
SOME [] => generic_remove_overloaded oconst context
@@ -145,51 +147,60 @@
(* check / uncheck *)
-fun unifiable_with thy T1 T2 =
+fun unify_filter thy maxidx1 T (t, U) =
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 prepare_tvars = Logic.incr_tvar (maxidx1 + 1) #> Type_Infer.paramify_vars;
+ val U' = prepare_tvars U
+ val t' = map_types prepare_tvars t;
+ val maxidx2 = Term.maxidx_typ U' maxidx1;
+ in
+ try (Sign.typ_unify thy (T, U')) (Vartab.empty, maxidx2)
+ |> Option.map (fn (tyenv, maxidx) =>
+ let val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv}
+ in Envir.norm_term env t' end)
+ 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));
+fun get_candidates ctxt ts (c, T) =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val maxidx = fold Term.maxidx_term ts 0;
+ in
+ get_variants ctxt c
+ |> Option.map (map_filter (unify_filter thy maxidx T))
+ end;
-fun insert_variants ctxt t (oconst as Const (c, T)) =
- (case get_candidates ctxt (c, T) of
+fun insert_variants ctxt ts t (oconst as Const (c, T)) =
+ (case get_candidates ctxt ts (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
+ dummify_types t
|> get_overloaded ctxt
|> Option.map (Const o rpair (Term.type_of t));
in
Pattern.rewrite_term_top (Proof_Context.theory_of ctxt) [] [proc]
end;
-fun check ctxt =
- map (fn t => Term.map_aterms (insert_variants ctxt t) t);
+fun check ctxt ts =
+ map (fn t => Term.map_aterms (insert_variants ctxt ts t) t) ts;
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;
-fun reject_unresolved ctxt =
+fun reject_unresolved ctxt ts =
let
- val the_candidates = the o get_candidates ctxt;
+ val the_candidates = the o get_candidates ctxt ts;
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;
+ in map check_unresolved ts end;
(* setup *)
More information about the isabelle-dev
mailing list