Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-04-04

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
05:07 tautologico_ joined #isabelle
05:09 chindy_ joined #isabelle
12:38 JCaesar Hm. The docs claim that code_pred generates code equations for an inductively defined predicate. But if I write value[code] "my_pred foo bar" I still get a "No code equations for my_pred".
12:38 JCaesar Is the documentation wrong, or am I misreading it?
12:39 JCaesar (Specifically: this predicate. https://github.com/jcaesar/Iptables_Semantics/blob/09d41b3ec8c8515cfe8f83769c44387fdd380189/thy/Iptables_Semantics/Alternative_Semantics.thy#L105 )
12:40 JCaesar values "{bar. my_pred foo bar}" works fine.
12:40 pruvisto JCaesar: it should do that normally
12:41 JCaesar I do se a my_pred.equation being generated… (and some other stuff…)
12:47 pruvisto yeah I have no idea, sorry
12:47 pruvisto the predicate compiler is an eternal mystery to me
13:34 larsrh JCaesar: let me check that
13:35 JCaesar larsrh: https://paste.pound-python.org/show/11VRhO07vFKVSySWIaRQ/
13:35 JCaesar (put this into thy/Iptables_Semantics)
13:38 larsrh on it
13:57 larsrh JCaesar: https://pastebin.com/DDNN2tXX
14:11 pruvisto JCaesar: ah, I see
14:11 pruvisto could have figured that out myself tbh
14:12 pruvisto like almost every time when something goes wrong with code_pred, it's the mode inference that failed
14:12 pruvisto just do "code_pred (modes: i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool) iptables_bigstep_r ." instead of what you did
14:12 pruvisto then you get a code equation for it.
14:13 pruvisto by default, code_pred doesn't seem to generate code for that mode
14:13 pruvisto no idea why *shrug*
14:15 pruvisto I wonder if it has something to do with the fact that this is a higher-order predicate
14:15 pruvisto ("matcher" is a function)
14:25 JCaesar So is the background ruleset Gamma.
18:28 chindy joined #isabelle
18:36 chindy Is there any autoformatting feature in Jedit isabelle ?
18:45 ammbauer chindy: mark text, then Ctrl-i should work
22:51 ertes joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary