It seems that the required changes are minimal. See the attached patch.
To be on the safe side: could somebody push this to the test server (in
my local tests I just loaded all theories from the Isabelle repo and the
AFP that contained the keyword "adhoc_overloading" in Isabelle/jEdit
instead of building all heap images).
cheers
chris
On 09/30/2013 08:50 PM, Christian Sternagel wrote:
On 09/30/2013 07:33 PM, Makarius wrote:
On Tue, 24 Sep 2013, Christian Sternagel wrote:
After this changeset, variants may be arbitrary terms (due to
localization). Now replacing a variant by the corresponding overloaded
constant is done by rewriting (as Florian already pointed out, this
happens in "insert_overloaded") as follows
fun insert_overloaded ctxt variant =
(case try Term.type_of variant of
NONE => variant
| SOME T =>
Pattern.rewrite_term (Proof_Context.theory_of ctxt) []
[Option.map (Const o rpair T) o
get_overloaded ctxt o Term.map_types (K dummyT)] variant);
Apparently this interferes with abbreviations. Am I doing anything
strange here?
I've looked only briefly so far. Abbreviations are only contracted for
type-correct terms, but above that information is not fully preserved.
Pattern.rewrite_term needs to re-used the type of the replaced subterm
(within the proc), not the overall type of the term called "variant"
above.
Thanks! That's a valuable hint. I will look into it and hope to make
adhoc overloading and abbreviations produce the expected results again,
before the release.
cheers
chris
Makarius
# HG changeset patch
# User Christian Sternagel
# Date 1380546106 -32400
# Mon Sep 30 22:01:46 2013 +0900
# Node ID 1b2bc47df509d6d58dbf7fd8351f6e1f6e9eb736
# Parent c1097679e2955ad7460150e6c4aa8d573ce9b354
preserve types during rewriting
diff --git a/src/Tools/adhoc_overloading.ML b/src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML
+++ b/src/Tools/adhoc_overloading.ML
@@ -165,12 +165,15 @@
| _ => oconst)
| insert_variants _ _ oconst = oconst;
-fun insert_overloaded ctxt variant =
- (case try Term.type_of variant of
- NONE => variant
- | SOME T =>
- Pattern.rewrite_term (Proof_Context.theory_of ctxt) []
- [Option.map (Const o rpair T) o get_overloaded ctxt o Term.map_types (K dummyT)] variant);
+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));
+ in
+ Pattern.rewrite_term (Proof_Context.theory_of ctxt) [] [proc]
+ end;
fun check ctxt =
map (fn t => Term.map_aterms (insert_variants ctxt t) t);
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
