[isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading
Christian Sternagel
c.sternagel at gmail.com
Fri Jan 16 14:46:54 CET 2015
Just a reminder that this old thread is not yet resolved and currently
I'm essentially stuck.
Independent of my being stuck, could one of the devs apply at least the
first of the following attached patches (and the second one depending on
whether dropping semicolons is in general seen as good style or not)
that somehow drowned in previous emails:
delete
drop_semicolons
cheers
chris
On 12/01/2014 01:56 PM, Christian Sternagel wrote:
> Thanks for the valuable pointers Florian!
>
> As far as I understand, type inference is a necessary prerequisite for
> "expand_abbrevs" (so that afterwards matching and instantiating by the
> obtained substitution suffice for getting the proper type).
>
> Two thoughts:
>
> 1) I wouldn't want to add yet another layer of type-inference directly
> before the adhoc_overloading check. Anyway, currently it doesn't even
> seem possible to inject something after type inference but before
> expand_abbrevs.
>
> 2) Even if full type inference was done before the adhoc_overloading
> check is executed, matching alone wouldn't suffice.
>
> The reason for 2 is that often (adhoc) overloaded constants have a very
> general type (which can't be made more specific while still supporting
> all desired variants). Consider e.g. monadic "bind", whose type is "'a
> => ('b => 'c) => 'd" or "pure :: 'a => 'b" from Andreas' example. More
> specifically, for the term "pure id" type inference will infer type "'b"
> while the corresponding "id" has type "'a => 'a" and this instance of
> "pure" has type "('a => 'a) => 'b". Thus there is no connection between
> the domain- and range-type of "pure" whatsoever. Now the type of
> "pure_stream :: 'a1 => 'a1 stream" cannot be instantiated to "('a => 'a)
> => 'b". Only via unification we can find that with
>
> "['a1 -> ('a => 'a), b' -> ('a => 'a) stream]"
>
> we actually can insert "pure_stream" here. The problem (I think) is that
> by unification we might inject schematic type variables that stem from
> types of variants (like "'a1" above). Into the ongoing check phase whose
> context doesn't know about them.
>
> Thus again my questions. Does this seem plausible? And is there a way to
> turn such "alien" schematic type variables into known ones?
>
> cheers
>
> chris
>
> On 11/27/2014 08:50 AM, Florian Haftmann wrote:
>> Hi Christian,
>>
>>> I'm mostly guessing here. Maybe somebody with deeper knowledge of the
>>> system could comment whether this would be feasible (and also the right
>>> way to go).
>>
>> I have not spent much thought on the code, but tried to take a bird's
>> perspective.
>>
>> The whole matter is about overloaded abbreviations. Hence, it's about
>> abbreviation expansion intermingled with type inference.
>>
>> Having a look syntax_phases.ML
>>
>>> (* standard phases *)
>>>
>>> val _ = Context.>>
>>> (typ_check 0 "standard" Proof_Context.standard_typ_check #>
>>> term_check 0 "standard"
>>> (fn ctxt => Type_Infer_Context.infer_types ctxt #> map
>>> (Proof_Context.expand_abbrevs ctxt)) #>
>>> term_check 100 "standard_finish"
>>> Proof_Context.standard_term_check_finish #>
>>> term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
>>
>> I see that type inference and abbreviation expansion occur on the same
>> term check level. Hence the overloading mechanisms could go here.
>>
>> Proof_Context.expand_abbrevs essentially boils down to Consts.certify.
>>
>> Maybe a comparision of these with the current implementation of
>> adhoc-overloading can give some clues.
>>
>> Cheers,
>> Florian
>>
-------------- 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
More information about the isabelle-dev
mailing list