Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-03-08

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

All times shown according to UTC.

Time Nick Message
02:36 JCaesar Can I somehow retrieve the string value of a term in ML? (The term is an Isabelle string.)
05:42 larsrh joined #isabelle
06:59 ThreeOfEight JCaesar: what kind of term?
06:59 ThreeOfEight i.e. is the term already "evaluated" in a sense or do you still have to evaluate it?
06:59 ThreeOfEight i.e. is it something like "'foobar''" or is it something like "f 1 2"
07:01 JCaesar the latter.
07:01 JCaesar (value[code] works.)
07:02 JCaesar In the end, I'd like to build a command that evaluates an expression and writes the result to a file. Just saying to prevent the a-b-problem.
07:14 JCaesar Thinking about it, something like that should already exist. Outputting a computed string to a file sounds like a pretty common use case.
07:17 ThreeOfEight do you just need the value or also a theorem that it is that value?
07:33 JCaesar Just the value. (I don't really think I can state some theorem about that string value. I'll leave my deserialization unverified. :/)
07:37 ThreeOfEight then you should use Code_Evaluation.dynamic_value or Code_Evaluation.static_value
07:38 ThreeOfEight the difference is that static_value builds a continuation with fixed code equations
07:38 ThreeOfEight i.e. you can call it in such a way that it uses the code equations and code generator config at compile time
07:38 ThreeOfEight dynamic_value uses the setup from when it is called
07:39 ThreeOfEight the down side is that you need to provide static_conv with a full list of constants that can appear in the terms you want to evaluate
07:39 ThreeOfEight also, they are both a bit slow because the code gets re-generated and re-compiled with every call
07:40 ThreeOfEight there are two ways to get around this, but one of them is a bit fishy and the other one is a massive pain in the arse
12:50 chuchucorny Isabelle/SML: why does the following just print the empty string? writeln "\r"
12:57 larsrh chuchucorny: I have the suspicion that the "Output panel" ignores many control symbols
12:57 larsrh What would you expect to get printed?
13:01 chuchucorny something that would help me to debug that there are remains of windows line endings left in the string
13:01 chuchucorny I got the string list from File.read_lines
13:02 chuchucorny and having it read a text file with windows file endings broke my parser without any error message
13:07 larsrh I guess File.read_lines preserves \r, then
13:07 chuchucorny yes
13:11 larsrh fun read_lines path = rev (fold_lines cons path []);
13:11 larsrh fun fold_lines f = fold_chunks #"\n" f;
13:12 larsrh You could use String.translate to remove \r
13:14 larsrh val filter_cr = String.translate (fn c => if c = #"\r" then "" else String.implode [c])
14:08 chuchucorny thx

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