Re: [isabelle-dev] type unification
Dear Dimitriy, thanks that does the trick. However, after having a look at the implementation of Variable.polymorphic, I'm wondering whether it isn't overkill in my case. What about fastype_of # Term.map_type_tfrees (TVar o apfst (rpair 0)) as alternative? Since I'm manually naming schematic type variables apart before unification anyway, shouldn't that also work (without ever using a ctxt)? cheers chris On 07/11/2013 02:57 PM, Dmitriy Traytel wrote: Hi Chris, I think Variable.polymorphic is what you want to use before using fastype_of. Dmitriy Am 11.07.2013 05:12, schrieb Christian Sternagel: Dear list, what is the proper way of obtaining a type from a term, in case I want to give it as argument to Sign.typ_unify (of Sign.typ_match for that matter)? My question arises as follows. In adhoc_overloading.ML previously Sign.the_const_type was used to obtain the type of a constant. The result is a type with schematic type variables. Now that I want to use terms instead of constants (as strings) I replaced Sign.the_const_type by fastype_of, but this yields a type with fixed type variables and thus unification may fail. So once again: What is the proper way of getting a schematic type from a term? cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] type unification
If you are planing to localize the thing, you'll have to take the
context into account. I guess you don't want to generalize over fixed
type variables (as your solution does).
locale A =
fixes a :: 'a
begin
ML {*
val T1 = @{term a} | singleton (Variable.polymorphic @{context}) |
fastype_of
val T2 = @{term a} | (fastype_of # Term.map_type_tfree (TVar o
apfst (rpair 0)))
*}
end
Dmitriy
Am 11.07.2013 09:01, schrieb Christian Sternagel:
Dear Dimitriy,
thanks that does the trick. However, after having a look at the
implementation of Variable.polymorphic, I'm wondering whether it isn't
overkill in my case. What about
fastype_of # Term.map_type_tfrees (TVar o apfst (rpair 0))
as alternative?
Since I'm manually naming schematic type variables apart before
unification anyway, shouldn't that also work (without ever using a ctxt)?
cheers
chris
On 07/11/2013 02:57 PM, Dmitriy Traytel wrote:
Hi Chris,
I think Variable.polymorphic is what you want to use before using
fastype_of.
Dmitriy
Am 11.07.2013 05:12, schrieb Christian Sternagel:
Dear list,
what is the proper way of obtaining a type from a term, in case I want
to give it as argument to Sign.typ_unify (of Sign.typ_match for that
matter)?
My question arises as follows. In adhoc_overloading.ML previously
Sign.the_const_type was used to obtain the type of a constant. The
result is a type with schematic type variables. Now that I want to use
terms instead of constants (as strings) I replaced Sign.the_const_type
by fastype_of, but this yields a type with fixed type variables and
thus unification may fail. So once again: What is the proper way of
getting a schematic type from a term?
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] type unification
You are right. Thanks for the clarification! - chris
On 07/11/2013 04:19 PM, Dmitriy Traytel wrote:
If you are planing to localize the thing, you'll have to take the
context into account. I guess you don't want to generalize over fixed
type variables (as your solution does).
locale A =
fixes a :: 'a
begin
ML {*
val T1 = @{term a} | singleton (Variable.polymorphic @{context}) |
fastype_of
val T2 = @{term a} | (fastype_of # Term.map_type_tfree (TVar o
apfst (rpair 0)))
*}
end
Dmitriy
Am 11.07.2013 09:01, schrieb Christian Sternagel:
Dear Dimitriy,
thanks that does the trick. However, after having a look at the
implementation of Variable.polymorphic, I'm wondering whether it isn't
overkill in my case. What about
fastype_of # Term.map_type_tfrees (TVar o apfst (rpair 0))
as alternative?
Since I'm manually naming schematic type variables apart before
unification anyway, shouldn't that also work (without ever using a ctxt)?
cheers
chris
On 07/11/2013 02:57 PM, Dmitriy Traytel wrote:
Hi Chris,
I think Variable.polymorphic is what you want to use before using
fastype_of.
Dmitriy
Am 11.07.2013 05:12, schrieb Christian Sternagel:
Dear list,
what is the proper way of obtaining a type from a term, in case I want
to give it as argument to Sign.typ_unify (of Sign.typ_match for that
matter)?
My question arises as follows. In adhoc_overloading.ML previously
Sign.the_const_type was used to obtain the type of a constant. The
result is a type with schematic type variables. Now that I want to use
terms instead of constants (as strings) I replaced Sign.the_const_type
by fastype_of, but this yields a type with fixed type variables and
thus unification may fail. So once again: What is the proper way of
getting a schematic type from a term?
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] adhoc overloading
Dear all,
here is an update to my previous message. Corresponding patches are
attached (tested with `isabelle build_doc -pa` and `isabelle afp_build -A`).
Some comments:
1) Variants are stored as terms but where all types are mapped to
dummyT (which makes it easier to check for a given term, whether it is
a variant of an overloaded constant).
2) In the table that maps overloaded constants to variants in addition
to the dummy-typed variant also a type is included (where all free
type variables are replaced by schematic ones).
3) As stated by Dmitriy in the type unification thread the current
solution does not work for localization (but the corresponding change is
trivial, I'm just avoiding it for the moment, since without localization
I have to work with a thy, which is inconvenient to turn into a ctxt as
required by Variable.polymorphic).
cheers
chris
On 07/10/2013 04:38 PM, Christian Sternagel wrote:
First of all, thanks for all the useful answers and sorry for my late
reply (I visited a conference and had some holidays ;)). As Alexander
suggested, I first tried to modify the existing adhoc_overloading.ML in
such a way that variants may be arbitrary terms. Please find the results
of my attempt attached (the new adhoc_overloading.ML as well as a
patch-file). Now I will investigate further localization.
Any comments are welcome.
cheers
chris
On 06/02/2013 08:55 AM, Alexander Krauss wrote:
Hi Chris,
I'm currently (as of changeset e6433b34364b) investigating whether it
would be possible to allow adhoc overloading (implemented in
~~/src/Tools/adhoc_overloading.ML) inside local contexts.
Nice!
For completeness find my current adhoc_overloading.ML attached
Apart from the various formalities pointed out by Makarius, here is
another concern, which relates to Florian's earlier question about how
local you want to be...
Currently, Adhoc_Overloading replaces constants with other constants,
which makes it global-only. Your current version tries to deal with
Frees similarly, it's not just that. Recall the example you gave
previously:
consts FOO :: ... (some syntax)
setup {* Adhoc_Overloading.add_overloaded @{const_name FOO} *}
locale foo =
fixes foo :: ...
assumes ...
begin
local_setup {*
Adhoc_Overloading.add_variant @{const_name FOO} @{term foo}
*}
Now consider the following interpretation:
interpretation foo some term
proof
Now, some term should become a variant of FOO, so at least the variant
side of the overloading relation must be an arbitrary term. With your
current code, the overloading would only survive interpretations where
foo happens to be mapped to a constant.
So, I guess that the overloaded constants should remain constants, since
they are just syntactic anyway. It seems that localizing those would be
rather artificial. But the variants must be properly localized and
subject to the morphism.
As a step towards proper localization, you could start with the global
code, and first generalize it to accept arbitrary terms as variants.
Note that this touches in particular the uncheck phase, which can no
longer use Term_Subst.map_aterms_same (or Term.map_aterms), since it
becomes general rewriting. One must resort to the more general
Pattern.rewrite_term here. When all this is working again, the actual
localization is then a mere formality, of which you have already
discovered the ingredients.
Makarius wrote:
* Same.function seems to be a let-over from the version by Alex
Krauss. He had that once in his function package, copied from
somewhere else (probably old code of mine).
No, it has nothing to do with the function package, which never used any
Same stuff. It just arose rather naturally from the requirement to
return NONE when nothing changes... So it was not meant as an
optimization.
There is no point to do
such low-level optimizations in the syntax layer. It is for hardcore
kernel operations only
So should I manually check the result for equality, or does the
framework do this for me?
Alex
diff -r aaec3f5a1ba6 thys/JinjaThreads/Framework/FWState.thy
--- a/thys/JinjaThreads/Framework/FWState.thy Wed Jul 10 15:19:23 2013 +0200
+++ b/thys/JinjaThreads/Framework/FWState.thy Thu Jul 11 16:30:08 2013 +0900
@@ -190,12 +190,12 @@
setup {*
Adhoc_Overloading.add_overloaded @{const_name inject_thread_action}
- # Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name NewThreadAction}
- # Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name ConditionalAction}
- # Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name WaitSetAction}
- # Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name InterruptAction}
- # Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name ObsAction}
- # Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name LockAction}
+ #
