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
# HG changeset patch
# Parent be4a911aca712cc928d1f798488205ce7c5fac92
typo in description
diff -r be4a911aca71 -r f653343d16ba src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.MLWed Nov 19 19:12:14 2014 +0100
+++ b/src/Tools/adhoc_overloading.MLFri 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.MLSun Nov 23 20:07:19 2014 +0100
+++ b/src/Tools/adhoc_overloading.MLSun 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
