Re: [isabelle] TYPE_MATCH exception with adhoc_overloading



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 f653343d16ba8595910d5275e1bc460069aac216
debug printing

diff -r f653343d16ba src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Fri Nov 21 19:58:22 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML	Sat Nov 22 21:00:16 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 "fastyp_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 untype = map_types (K dummyT)
+
 fun generic_remove_overloaded oconst context =
   let
     fun remove_oconst_and_variants context oconst =
@@ -99,7 +101,7 @@
         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 untype 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
@@ -112,7 +114,7 @@
       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 t' = untype t;
     in
       if add then
         let
@@ -121,15 +123,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 ()
+            if member variants_eq (the (get_variants ctxt oconst)) (t, T) then ()
             else err_not_a_variant oconst;
         in
-          map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T)))
+          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
@@ -147,16 +149,25 @@
 
 fun unifiable_with thy T1 T2 =
   let
+    val _ = writeln ("oconst type: " ^ Syntax.string_of_typ (Proof_Context.init_global thy) T1)
+    val _ = writeln ("variant type: " ^ Syntax.string_of_typ (Proof_Context.init_global thy) T2)
     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 T1' = Logic.incr_tvar (maxidx2 + 1) T1;*)
+    val maxidx2 = Term.maxidx_typ T2 maxidx1;
+  in try (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));
+    (case unifiable_with (Proof_Context.theory_of ctxt) T T' of
+      SOME (tyenv, _) =>
+        let
+          val _ = @{print} ("unifier:", tyenv);
+          val t' = Envir.subst_term_types tyenv t
+          val _ = @{print} ("candidate term:", t)
+          val _ = @{print} ("after unification:", t')
+       in SOME t' end
+    | NONE => NONE)));
 
 fun insert_variants ctxt t (oconst as Const (c, T)) =
       (case get_candidates ctxt (c, T) of


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.