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: <http://git.io/vINfn>
> 
> 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.

Cheers,
	Florian

> 
>>   * 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:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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