Re: [isabelle-dev] Towards a "localized" code generator
Dear Lars, Well, we here at ETH have another function transformer, which can also be activated and deactivated basically with almost the same pattern. The only difference is that at the moment we use a command rather than a Config value because de- and reactivation in our case has to do a bit more than just enabling/disabling a function transformer. It also must swap a few code equations. Function transformers could also be declared with an attribute, although there I'd say it's even less clear that attributes should be (ab)used for that. Yes, we felt like that, too. That's why we went for a command. This is an interesting idea. For the above-mentioned function transformer, we also have code_datatype declarations that must be switched back and forth. The big advantage of your approach seems to me that one can envision this alternative setup already where characters are defined (and similarly for int/nat/set/mapping/...). Exactly, that's another goal that could be achieved. But I wonder whether these bundle targets can be extended later. That is, if is some unrelated theory, I write my own function for chars by pattern-matching on Char. If I then import your theory, can I add further declarations (code drop/code) to the bundle such that subsequent theories get a consistent setup no matter whether the unbundle the bundle or not? Currently I'm unaware of any way to extend bundles, except for something like: bundle bar begin unbundle foo end Whether or not extending bundles is possible/canonical in Isar is a question best answered by Makarius. Well, originally, bundles were never meant to be extended later. That's what Makarius told me back in 2012. Maybe the situation has changed now. But I'd say that this is crucial to improve the current state of the art. Otherwise, we'll just have a mess with bundle names. Independently, a localised code generator would of course be nice. Best, Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards a "localized" code generator
Dear Andreas, > Well, we here at ETH have another function transformer, which can also > be activated and deactivated basically with almost the same pattern. The > only difference is that at the moment we use a command rather than a > Config value because de- and reactivation in our case has to do a bit > more than just enabling/disabling a function transformer. It also must > swap a few code equations. Function transformers could also be declared with an attribute, although there I'd say it's even less clear that attributes should be (ab)used for that. Possibly instead we could have a command functrans_setup "constructor_funs" = ‹ (* implementation *) › ... akin to simprocs. Of course, this would need to work in bundles as well. (simprocs do work in bundles) > This is an interesting idea. For the above-mentioned function > transformer, we also have code_datatype declarations that must be > switched back and forth. The big advantage of your approach seems to me > that one can envision this alternative setup already where characters > are defined (and similarly for int/nat/set/mapping/...). Exactly, that's another goal that could be achieved. > But I wonder > whether these bundle targets can be extended later. That is, if is some > unrelated theory, I write my own function for chars by pattern-matching > on Char. If I then import your theory, can I add further declarations > (code drop/code) to the bundle such that subsequent theories get a > consistent setup no matter whether the unbundle the bundle or not? Currently I'm unaware of any way to extend bundles, except for something like: bundle bar begin unbundle foo end Whether or not extending bundles is possible/canonical in Isar is a question best answered by Makarius. With locales, it would be possible, but of course they come with their own sets of issues. The beauty of a localized tool is that it would work uniformly across bundles and locales, so users can pick and choose. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards a "localized" code generator
Dear Lars, On 24/07/17 15:08, Lars Hupel wrote: 1) Function transformers: I want to run a function transformer in special situations. But I can only register it globally (with "Code_Preproc.add_functrans"). What I use is the following pattern: val enabled = Attrib.setup_config_bool @{binding "constructor_funs"} (K false) fun functrans ctxt thms = (* implementation *) val code_functrans = Code_Preproc.simple_functrans (fn ctxt => if Config.get ctxt enabled then functrans ctxt else K NONE) I'm not sure whether this is how attributes are meant to be used, but at least I can enable this locally. But as far as I can tell there are only three function transformers in total, so I'm not sure how relevant this is. Well, we here at ETH have another function transformer, which can also be activated and deactivated basically with almost the same pattern. The only difference is that at the moment we use a command rather than a Config value because de- and reactivation in our case has to do a bit more than just enabling/disabling a function transformer. It also must swap a few code equations. 2) "Fake local" declarations: I want to change the representation of the "char" type in declared code. By default, it is represented using numerals in a "non-free" way (i.e. there are invalid representations). I'd like to replace it with a free representation (bytes), but don't want this to affect the global theory; or at least, I'd like to avoid people importing my theory to be affected [0]. Here's my workaround: ML‹ fun code_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I) › attribute_setup "code_datatype" = ‹ Scan.repeat1 Args.term >> (fn terms => code_attribute (K (Code.declare_datatype_global (map dest_Const terms › Now I can use the "bundle" target: bundle char_byte_representation begin declare [["code_datatype" char_of_byte]] declare [[code drop: equal_char_inst.equal_char String.Char]] (* more ... *) declare char_byte_literals[code_unfold] end Importing this theory doesn't change the code setup. Only when I use "unbundle" the changes become permanent. However, it doesn't work properly in an unnamed context with "including" (this is as expected). There are a lot of occurrences of "code_datatype", often leading to the problem of artificially splitting up theories into an "abstract" and "implementation" part. This is an interesting idea. For the above-mentioned function transformer, we also have code_datatype declarations that must be switched back and forth. The big advantage of your approach seems to me that one can envision this alternative setup already where characters are defined (and similarly for int/nat/set/mapping/...). But I wonder whether these bundle targets can be extended later. That is, if is some unrelated theory, I write my own function for chars by pattern-matching on Char. If I then import your theory, can I add further declarations (code drop/code) to the bundle such that subsequent theories get a consistent setup no matter whether the unbundle the bundle or not? Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Towards a "localized" code generator
Dear users of the code generator, last week I spoke with Florian about some fundamental properties of the code generator. Many Isabelle users are also "power users" of the code generator; in the sense that they exploit many of its facilities (code printing, various attributes, ...). These days the setup is really powerful and can be tweaked in many ways. However, only few bits of the code generator is actually localized: Off the top of my head, this only applies to some of the attributes ("[code]" etc.). There are a lot of commands that only work in a global context and have a permanent effect on the theory. This has led to a problem: My work currently requires gathering code equations for some constants. Afterwards, I need to prove some things about them, which I do with either "code_simp" or "eval" – however, this requires a different setup. To make matters worse, the gathering of the code equations also requires special setup. I'd like to share with you two strategies to cope with this situation. This can serve as the basis for further discussion how to localize the code generator. 1) Function transformers: I want to run a function transformer in special situations. But I can only register it globally (with "Code_Preproc.add_functrans"). What I use is the following pattern: val enabled = Attrib.setup_config_bool @{binding "constructor_funs"} (K false) fun functrans ctxt thms = (* implementation *) val code_functrans = Code_Preproc.simple_functrans (fn ctxt => if Config.get ctxt enabled then functrans ctxt else K NONE) I'm not sure whether this is how attributes are meant to be used, but at least I can enable this locally. But as far as I can tell there are only three function transformers in total, so I'm not sure how relevant this is. 2) "Fake local" declarations: I want to change the representation of the "char" type in declared code. By default, it is represented using numerals in a "non-free" way (i.e. there are invalid representations). I'd like to replace it with a free representation (bytes), but don't want this to affect the global theory; or at least, I'd like to avoid people importing my theory to be affected [0]. Here's my workaround: ML‹ fun code_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I) › attribute_setup "code_datatype" = ‹ Scan.repeat1 Args.term >> (fn terms => code_attribute (K (Code.declare_datatype_global (map dest_Const terms › Now I can use the "bundle" target: bundle char_byte_representation begin declare [["code_datatype" char_of_byte]] declare [[code drop: equal_char_inst.equal_char String.Char]] (* more ... *) declare char_byte_literals[code_unfold] end Importing this theory doesn't change the code setup. Only when I use "unbundle" the changes become permanent. However, it doesn't work properly in an unnamed context with "including" (this is as expected). There are a lot of occurrences of "code_datatype", often leading to the problem of artificially splitting up theories into an "abstract" and "implementation" part. Cheers Lars [0] This is not a theoretical problem, see AFP/e0065e482c76. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev