Re: [isabelle] Splicing runtime ML values into Isar

Hi Lars,

> While refactoring my code to use theory/context data slots, I got
> carried away and implemented a general mechanism for typed evaluation. I
> uploaded it to a dedicated repository: <>
> It can be used like this:
>   typed_evaluation foo = âintâ
>   Typed_Evaluation.eval @{token foo} â3â @{context}
> There might be a way to get rid of the explicit registration of the
> "token", but I haven't found one yet.

this looks definitely interesting.

Can a malicious attacker with access to the ML name space Âhijack your
evaluation machinery, e.g. by defining it own structure
Typed_Evaluation?  This is something difficult to handle?

We should discuss this on my next visit to TUM.


>>   * Term translations operate on rather raw parse trees.  You have already
>>     discovered that in the examples: referring to a local "x" is not
>>     immediately clear.  It would require some mechanism to "protect"
>>     already internal terms within the parse tree, but that would have to
>>     cooperate properly with the other syntax phases and the term "check"
>>     phases (type inference etc.).
> I haven't quite understood the mechanics yet. It appears that already
> the parsing fails, which makes me wonder whether it'd be sufficient to
> leave a spliced ML expression uninterpreted until checking. This would
> probably warrant a separate check phase.
>>   * Morphisms, which are particularly important for attribute expressions,
>>     introduce another dimension of higher abstract nonsense.  One needs to
>>     look closely that embedded ML works with that, but not all aspects are
>>     properly implemented in the system and existing antiquotations.
>>     E.g. ML antiquotations themselves ignore morphisms.
> I don't understand at all how morphisms come into play here. Are you
> suggesting that the embedded ML should somehow have access to a
> morphism? Which morphism?
> Cheers
> Lars


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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