| 07:34:00 | * | ryderblue quit (Remote host closed the connection) |
| 07:42:50 | * | Trix[a]r_za is now known as Trixar_za |
| 08:36:21 | * | Araq_ joined #nimrod |
| 08:50:21 | * | Araq_ quit (Quit: ChatZilla 0.9.89 [Firefox 16.0.2/20121024073032]) |
| 09:29:38 | * | Trixar_za is now known as Trix[a]r_za |
| 09:56:42 | * | Trix[a]r_za is now known as Trixar_za |
| 11:30:59 | * | Trixar_za is now known as Trix[a]r_za |
| 12:34:07 | * | Araq_ joined #nimrod |
| 12:39:39 | * | Araq_ quit (Quit: ChatZilla 0.9.89 [Firefox 16.0.2/20121024073032]) |
| 13:47:08 | * | Boscop quit (Ping timeout: 252 seconds) |
| 14:49:41 | * | XAMPP quit (Ping timeout: 244 seconds) |
| 14:51:26 | * | Araq_ joined #nimrod |
| 14:54:19 | * | Araq_ quit (Client Quit) |
| 14:55:54 | * | q66 joined #nimrod |
| 15:32:13 | * | XAMPP joined #nimrod |
| 15:35:42 | * | XAMPP quit (Read error: Connection reset by peer) |
| 18:15:44 | * | ryderblue joined #nimrod |
| 18:32:49 | Araq | ping zahary |
| 18:35:11 | zahary | pong Araq |
| 18:35:40 | Araq | using AI for initialization checking is actually not that easy as I imagined: |
| 18:35:44 | Araq | if b: |
| 18:35:50 | Araq | result.x = "not nil" |
| 18:35:52 | Araq | else: |
| 18:35:56 | Araq | result.y = "not nil" |
| 18:36:18 | Araq | --> we really need to keep the "path" dependence around |
| 18:37:14 | Araq | and even if we do, it looks like lots of work to check for nil-values afterwards |
| 18:38:16 | Araq | my point is, if you take both branches as an approximation, your environment looks like E = {x: "not nil", y: "not nil"} |
| 18:38:19 | zahary | the simpler analysis will treat both x and y as unassigned here, because they are unassigned in one of the branches |
| 18:38:45 | Araq | yeah but that's not what AI does as I'm understanding it |
| 18:39:37 | Araq | well that's not what the algorithm that I have in mind would do with it :-/ |
| 18:42:29 | zahary | the paper is not directly useful here, but it serves more as an analogy - if symbols have compile time properties, some of these properties are "intersected" in if blocks and some of them are "united" |
| 18:43:38 | zahary | "is initialized" clearly should use the && operator when considering the outcomes of both blocks |
| 18:44:00 | Araq | hrm true but that sounds overly pessimistic |
| 18:44:14 | zahary | what do you mean? |
| 18:44:55 | zahary | if will have a false possitive, if there is another if on `b` and the initialization is comleted there |
| 18:45:24 | Araq | that's what I mean, yes |
| 18:45:32 | zahary | that's not very realistic, but more realistic example may be |
| 18:45:32 | zahary | if x: result.a = 10 |
| 18:45:32 | zahary | if not result.a: result.a = 20 |
| 18:45:53 | zahary | here, my logic would fail indeed |
| 18:48:03 | Araq | I'm also having a hard time designing the "algebraic values" |
| 18:48:45 | Araq | for instance, s.len needs to be an abstract value |
| 18:49:19 | Araq | and modelling a kind of relationship between values seems very useful too: |
| 18:49:30 | Araq | var x = 5 |
| 18:49:34 | Araq | var y = x |
| 18:49:40 | Araq | x - y # always 0 |
| 18:50:17 | zahary | what do you mean by "abstract value" (for len) |
| 18:51:41 | Araq | well if we have a loop: for i in 0.. s.len-1: s[i] = 1 |
| 18:51:57 | Araq | and s is unknown length |
| 18:52:13 | Araq | we need a "dummy" value to use for the interpretation |
| 18:52:32 | Araq | but this value needs to stay abstract |
| 18:52:46 | Araq | and we mustn't lose its semantic relationship to 's' |
| 18:53:34 | zahary | just how much interpretation do you imagine? |
| 18:55:07 | Araq | everything that is currently eval-uable should become abstract interpretable |
| 18:55:14 | zahary | my hypolang was supposed to "eval" the loop body once if the looped over value is not statically known |
| 18:55:14 | zahary | I guess you are not suggesting something else here? |
| 18:55:36 | Araq | I dunno :-) |
| 18:55:57 | zahary | s[i] then is also marked as "runtime value of type X" |
| 18:56:18 | Araq | in my mind it should work like this: |
| 18:56:42 | Araq | proc p(c: PContext, n: PNode): PNode = ... complex body here ... |
| 18:57:00 | Araq | the compiler creates an abstract value for 'c' and for 'n' |
| 18:57:14 | Araq | and then 'p' is evaluated with these |
| 18:57:23 | Araq | and produces an abstract value 'result' |
| 18:57:33 | zahary | so s[i] = 1 is emitted as runtime code . the [] operator assigns another compile-time prop on the `s` symbol |
| 18:57:45 | Araq | that is checked for all the properties we can think of |
| 18:58:00 | Araq | starting with non-nullability |
| 18:58:43 | Araq | the evaluation is however nondeterministic |
| 18:59:13 | Araq | if we have 'if cond: t else: e' then we either eval 't' or 'e' or both |
| 18:59:25 | zahary | I have to think about this scheme, but for hypolang I planned to just update the compile time properties as I step through the sem pass |
| 18:59:45 | Araq | depening on 'cond' of course |
| 18:59:45 | Araq | if 'cond' is "unknown" we need to evaluate both |
| 18:59:45 | Araq | like the paper suggests |
| 19:00:29 | zahary | var x = 5 # symbol x is marked as compile-time value 5 |
| 19:00:29 | zahary | var y = x # y is 5 too |
| 19:00:29 | zahary | for i in [0..y] # compile-time for loop - unrolling possible, etc |
| 19:04:03 | Araq | alright but that doesn't work for any non-trivial constructor |
| 19:04:19 | Araq | as you don't input arguments at compile time |
| 19:04:47 | Araq | *don't know |
| 19:06:01 | zahary | if control flow construct is not evaluatable at compile-time, I enter it once (no looping, both branches of the if are taken, etc) |
| 19:06:43 | zahary | the symbol now have either completely unknown value or some superposition of possible values |
| 19:07:05 | zahary | but we continue to assign compile-time properties for it |
| 19:09:29 | Araq | proc ctor(n: int): seq[string] = |
| 19:09:35 | Araq | newSeq(result, n) |
| 19:09:45 | Araq | for i in 0 .. <n: result[i] = "" |
| 19:10:14 | Araq | --> 'n' is unknown and won't become a useful superposition soon ;-) |
| 19:10:46 | Araq | and that's a fairly simple constructor, right? |
| 19:11:12 | zahary | well, I'll tell you how the algorithm will proceed - it doesn't proof the code is correct or incorrect here - I don't know if that's a goal for you here |
| 19:11:32 | Araq | indeed that's my goal |
| 19:12:11 | Araq | but I can live with smart heuristics instead ;-) |
| 19:12:39 | zahary | n is run-time value |
| 19:12:39 | zahary | newSeq(result,n) # result.is_initialized is set to true |
| 19:12:39 | zahary | for i ... n: # run-time loop |
| 19:12:39 | zahary | result[i] = "" # ok to assign, since already initialized, otherwise regular run-time assignment, moving on |
| 19:13:22 | Araq | but it's not ok to assign |
| 19:13:41 | zahary | there is off-by-1 bug? |
| 19:13:56 | Araq | not my point |
| 19:14:10 | Araq | result.is_init is true, ok |
| 19:14:31 | Araq | but that does not mean that it has space for even a single element |
| 19:15:02 | Araq | but I'm still in "evals.nim mode" |
| 19:15:16 | Araq | result is nkBracket after newSeq() |
| 19:15:41 | Araq | with an unkown length that somehow needs to be dealt with |
| 19:16:35 | zahary | well, I was about to explain the next more advanced attempt |
| 19:16:35 | zahary | newSeq(result, n) # besides setting is_init = true, it also sets .known_size = n (run-time value) |
| 19:17:02 | zahary | then in the for loop i gets assigned .known_value = 0..n |
| 19:17:52 | zahary | result[i] = ... # we can avoid bounds check because i = 0..n is withing .known_size = n |
| 19:18:05 | zahary | within |
| 19:19:40 | Araq | ok so you have interval arithmetic with unkown bounds |
| 19:22:43 | zahary | I'll try to understand your approach, but the key difference in what we imagine is that the compile-time properties are determined by the type (the user can add her own properties) and they are carried by the symbols in my design |
| 19:23:46 | zahary | maybe there isn't much of a difference, because symbols will be represented by variables in evals so it's the same thing in the end |
| 19:24:09 | * | gradha joined #nimrod |
| 19:24:38 | Araq | I don't know what you mean with "symbol" in this context |
| 19:25:08 | Araq | I'm not sure I get your compile-time vs. run-time distinction either |
| 19:25:21 | Araq | if we have: |
| 19:25:23 | fowl | I wish I could use nil for var types |
| 19:25:28 | Araq | var x = 0 |
| 19:25:32 | Araq | inc x, 3 |
| 19:25:33 | Araq | echo x |
| 19:25:34 | zahary | var i = 5 # the skVar symbol actually have a ast field for "compile-time properties" - within that object there is the .known_value property that's 5 |
| 19:26:13 | Araq | that's all run-time code but easily interpreted and does not lead to nondeterministic problems for AI |
| 19:26:58 | Araq | fowl: what's wrong with using 'ptr' instead if you need the 'nil'? |
| 19:27:12 | gradha | or ref? |
| 19:27:27 | zahary | proc inc(x, y) = |
| 19:27:54 | zahary | x = x + y |
| 19:27:54 | zahary | x.known_value = x.known_value + y.known_value |
| 19:28:43 | zahary | that's what the user have to write for his own compile time properties - obviously, some of them are already implemented by the compiler |
| 19:30:31 | zahary | the real type of .known_value here is some really complicated interval set type |
| 19:30:39 | Araq | hu? what exactly does the user have to write? |
| 19:31:12 | zahary | what I meant is that he would have to write this if the compiler was not already implementing it |
| 19:31:57 | zahary | if the user introduces his own compile-time property, he must update it like that in his own functions |
| 19:32:17 | Araq | yeah well |
| 19:32:25 | zahary | so the compiler executes the "compile-time" code of the user during the semeval pass |
| 19:32:40 | Araq | that sounds like user definable inference rules for type tags |
| 19:32:48 | Araq | or something like that |
| 19:33:24 | Araq | and sorry, that's not yet a problem I'm interested in as I suppose the number of people that will ever understand and use it is 1 ... ;-) |
| 19:34:36 | Araq | I mean, the programmer shouldn't prove it's not nil; that's the compiler's job |
| 19:35:00 | zahary | but the user may be interested in other properties that are specific for his problem domain |
| 19:35:17 | Araq | if it cannot do that, you should simply annotate it with 'yeah_trust_me' |
| 19:35:19 | zahary | the steps taken by the compiler are the same in both cases - that's my point |
| 19:36:40 | Araq | I can't see how these things are similar ... |
| 19:37:21 | Araq | but I still don't get what this means: x.known_value = x.known_value + y.known_value |
| 19:38:07 | Araq | how is that of any use? |
| 19:38:19 | zahary | .known_value is the compile-time property - what are the possible values for this variable - so far so good? |
| 19:38:52 | zahary | its type is something that can represent itervals and superpositions |
| 19:39:02 | Araq | dunno, go on please |
| 19:39:38 | zahary | it would be hard for the user to write its own version and the compiler has already implemented that particular property |
| 19:39:58 | zahary | but if the user decided to write it nevertheless on its own, he would have to do the following |
| 19:40:14 | zahary | define a type TIntervalSet with all its operators, etc |
| 19:41:10 | zahary | add .known_value compile time field to the int type (in hypolang, it was supposed to be possible to reopen any type both for run-time fields and compile-time fields) |
| 19:41:30 | zahary | known_value: TIntervalSet {.compileTime.} |
| 19:42:34 | zahary | then the user must add updates to this .known_value field for all functions that use int (or to a sufficient set of function that build up all others) |
| 19:43:27 | zahary | the compiler then updates the user .known_values as it steps through the code - for each funtion called it executes the compile-time code, and emits the run-time code |
| 19:44:00 | zahary | the compile-time code write to the compileTime fields that are stored in the symbols, the run-time code is, well, run-time code |
| 19:45:33 | Araq | alright but I still can't see how this helps for proving the absense for nil :P |
| 19:45:42 | Araq | *of nil |
| 19:46:36 | zahary | in a record constructor? if the user were implementing this on its own, it would add one is_init_x compile-time field for each of the record fields |
| 19:47:05 | zahary | and then will hook assignments to update these fields |
| 19:47:32 | zahary | and then it will hook the function "seal" event to verify that all fields were initialized |
| 19:47:59 | zahary | now, again this is something the compiler can implement for the user as it is common enough |
| 19:54:29 | zahary | I mentioned this before - for If and Case expressions, the compiler usually evaluates all branches and calls a user proc responsible to merge the results (to determine the compile-time properties of the symbol after the if/case) |
| 19:56:25 | zahary | ultimately, the complexity/accuracy/usefulness of the analysis is determined by the data structures used as compileTime properties - the user can implement both naive and advanced algorithms |
| 20:00:55 | Araq | meh, it's not a problem that'd want to give to the poor programmer |
| 20:03:26 | zahary | again, I'm not suggesting you should - I'm suggesting that the framework for updating these compile-time values is the same for both user-defined and build-in properties |
| 20:04:06 | zahary | are you saying that there shouldn't be user-defined compileTime properties? |
| 20:04:53 | Araq | again, user-defined and "proof" do play nice with each other |
| 20:05:21 | Araq | so if there are user-defined compiletime properties they shouldn't affect the analysis |
| 20:06:10 | Araq | for me the 2 topics are still completely orthogonal |
| 20:16:43 | Araq | but *shrug* maybe you're right and it ends up using the same algorithm |
| 20:16:54 | zahary | each compileTime prop and its associated analysis is orthogonal to all other compileTime props |
| 20:16:55 | zahary | again, if there is some difference in the scheme I describe it's that a) properties are stored in the symbols and not in the evals operational memory b) properties are updated directly in sem as we step through the expressions. notice that evals is needed in order to provide run-time stack and operational memory - since branching and function calling doesn't exist in what I describe there is no need for these features |
| 20:17:49 | Araq | brb |
| 20:19:49 | gradha | I'll use this intermission to ask Araq: why does the tutorial say that exceptions should be allocated on the heap, then goes to show an example which doesn't do that? |
| 20:20:18 | zahary | well, what's the example? |
| 20:20:55 | gradha | see http://nimrod-code.org/tut2.html#raise-statement |
| 20:21:21 | gradha | actually, the only exception raised in the examples directory uses the proc newException (or whatever it's called) |
| 20:22:10 | gradha | maybe I should rephrase the question: what BAD will happen when I raise an exception not allocated on the heap, like the example shows? |
| 20:22:13 | zahary | in the example, e is a ref type and there is new(e); before raising |
| 20:22:47 | gradha | oh, crap, so I don't know how to read then |
| 20:23:25 | zahary | I think you should get a compile time error if you don't pass a ref type |
| 20:23:42 | gradha | haven't tried yet, it may well be so |
| 20:49:13 | * | shevy quit (Ping timeout: 245 seconds) |
| 20:50:00 | Araq | thinking about it after 'except EOS' the exception could be freed, no GC necessary for it |
| 20:50:25 | Araq | I guess that's how C++ does it |
| 20:51:30 | Araq | but the current way is good enough |
| 20:52:29 | Araq | oh and zahary, I thought about your 'raise within onRaise' example and it's hard to support |
| 20:52:56 | Araq | however, the onraise handler returns a bool to tell 'raise' it should continue and unwind the stack |
| 20:53:14 | zahary | but that's not the whole store in the conditional system |
| 20:54:03 | zahary | I raise to indicate an error and allow the user to tell me that's I should proceed in certain way (each "certain way" can correspond to such counter-exception or some other mechanism) |
| 20:56:51 | zahary | int return code (enum) could be alternative I guess, but I have to look at some real-world examples to see how often they want a little bit of unwinding in the raiser stack before taking the recovery path |
| 20:57:40 | Araq | it could return ref E_Base instead and if != nil, this returned exception is raised |
| 20:58:06 | Araq | that way you can transform EOS into EIO for instance |
| 21:01:12 | Araq | if you allow for an enum/int than the API shouldn't 'raise' in the first place, but call a callback |
| 21:01:26 | Araq | this way it can define its own enum type |
| 21:01:49 | Araq | otherwise you indeed end up with an 'int' as a poor "open" typeless enum |
| 21:02:23 | gradha | I'm thinking of reusing nimrod's parsing code to make it spit out a ctags compatible file with symbol info, because I'm not getting anything useful out of https://github.com/Araq/Nimrod/wiki/Editor-Support with the three different ctags implementations I have on my machine. Araq: what/where could I look to make nimrod stop after parsing so I can coerce it to generating a ctags compatible file? What would be the steps to add a new ni |
| 21:02:24 | gradha | command? |
| 21:03:16 | zahary | gradha, what's your editor? |
| 21:03:26 | gradha | vim |
| 21:03:52 | gradha | would idetools do something like this already? |
| 21:04:08 | zahary | nimrod supports a special command "nimrod idetool --def" that's supposed to implement go to definition |
| 21:04:40 | gradha | yes, I think I'll look at that |
| 21:05:03 | zahary | I'm using the ctags rules at the wiki page and they work for me, but I wanted to add the proper idetool to nimrod.vim |
| 21:05:36 | zahary | the ctags that comes with OS X is broken for me - are you using it? |
| 21:05:55 | gradha | I'm using one from macports, and also another I compiled from a git clone to have objc support |
| 21:06:26 | gradha | both seem to parse/add correctly the configuration file, but they generate an empty tags file after going through the .nim files |
| 21:07:47 | gradha | surprisingly it's the etags which comes with mac that parses correctly the .nim files, but builds an emacs tags file which vim doesn't like |
| 21:08:17 | gradha | rather than update it with a script I thought adding ctags output to the nimrod compiler would be the easiest, as it already has the info and doesn't require you to have an extra tool installed |
| 21:08:39 | zahary | well, let's implement the idetools command instead - ctags still doesn't work ok for type for example as they are harder to catch with a regex |
| 21:09:05 | Araq | I don't really remember but I think ctags is not 1 file format but a couple of formats |
| 21:09:26 | Araq | so I made the compiler output something different instead |
| 21:13:36 | gradha | I'm trying nimrod idetools --track=backend.nim,221,0 --def but it doesn't output anything, do I need to add something else to the commandline? |
| 21:14:00 | Araq | yeah |
| 21:14:09 | Araq | you need to give the project.nim too |
| 21:15:01 | zahary | or you better use a config file with a mainModule="myProject.nim" setting |
| 21:17:13 | gradha | cool, works now |
| 21:18:29 | zahary | Araq, here are some examples for the usage of the lisp condition system |
| 21:18:30 | zahary | http://www.gigamonkeys.com/book/beyond-exception-handling-conditions-and-restarts.html |
| 21:19:13 | zahary | notice that the function raising the exception is indeed oblivious that there are restarts further in the call tree |
| 21:20:27 | zahary | the example is about parsing a log file - parse-log-entry raises an exception, and parse-log-file as a whole allow the user to skip bad lines |
| 21:20:41 | zahary | so it installs a restart case |
| 21:21:18 | Araq | I read this article months ago |
| 21:21:44 | zahary | I've read it a few years ago, but didn't remember the specifics |
| 21:24:55 | zahary | so replacing the exception could work: InvalidLogEntry -> SkipEntry. The next hazard is that SkipEntry is an obsolete restart |
| 21:25:08 | Araq | well there are 2 ways: |
| 21:25:36 | Araq | 1) treat and encourage 'raise' as a general notify mechanism |
| 21:26:08 | Araq | 2) provide a workaround for a stupid API that used 'raise' where it should have used an explicit callback |
| 21:26:25 | Araq | I've implemented 2) and Lisp does 1) |
| 21:27:09 | Araq | replacing the exception works if E_Base gets another field |
| 21:27:24 | Araq | that says whether it's an error, or a warning, or ... |
| 21:27:27 | Araq | aka an enum |
| 21:31:04 | zahary | but the alternative way is to modify parse-log-file to catch InvalidLogEntry and potentially call a user callback to determine whether the error should be ignored |
| 21:31:43 | zahary | not adding onRaise handler to ignore the error directly in parse-log-entry |
| 21:34:00 | Araq | hrm |
| 21:35:40 | Araq | so what do you suggest? |
| 21:36:33 | zahary | changing the exception looks dangerous and you are right that exceptions should not be used too much for control flow |
| 21:37:58 | zahary | also, I guess one can implement the restart cases as thread local variables (so there won't be need to add local fields for callbacks, etc) |
| 21:39:51 | Araq | well in the onraise handler you can call a UI function to ask the user what to do |
| 21:39:53 | zahary | what I'm saying is that the current support is good enough |
| 21:41:02 | * | Araq tries a concrete example |
| 21:41:34 | zahary | most functions should not be written in a way that allows raise to be cancelled |
| 21:41:57 | Araq | that would be my next point, yeah |
| 21:42:10 | Araq | often for instance you 'raise' out of loops |
| 21:42:31 | Araq | it's dangerous to cancel that |
| 21:42:38 | Araq | the code needs to be written with error recovery in mind |
| 21:42:53 | Araq | at which point it may as well take an explicit callback |
| 21:43:05 | zahary | raise that changes the exception may be left as advanced shoot yourself in the foot feature |
| 21:44:50 | Araq | changing the exception object seems very useful |
| 21:45:14 | Araq | for the kind of people who care that exception types do not leak submodules |
| 21:45:28 | Araq | so I'll change it to support that |
| 21:45:37 | zahary | so make that the purpose of onRaise and leave it that way |
| 21:45:52 | zahary | one can implement the lisp style system on top of it oo |
| 21:45:53 | zahary | too |
| 21:45:56 | Araq | the alternative would be to try-catch-reraise |
| 21:46:03 | Araq | which is much more expensive |
| 21:46:26 | Araq | so yeah, one can turn ESQL into an EIO with almost 0 cost |
| 21:46:29 | Araq | I like that |
| 21:49:56 | Araq | er ... no :-) |
| 21:49:56 | Araq | the runtime cost seems to be almost the same |
| 21:50:21 | Araq | oh well, it's more convenient |
| 21:50:26 | zahary | there is less support code |
| 21:51:24 | Araq | ugh, screw this, it fights my new exception analysis pass |
| 21:51:47 | Araq | raise EIO # can raise anything now? |
| 21:52:01 | Araq | that breaks the analysis |
| 21:52:51 | zahary | oops :) |
| 21:59:14 | gradha | What means changing the exception object? It is calling raise newException(somethingElse, "blah") inside an except block? |
| 22:02:26 | Araq | it doesn't really "change" an exception, it catches one and rethrows another |
| 22:03:17 | zahary | and we are talking about another work-in-progress feature - you can install an onRaise hook that is executed immediately at the raise statement before unwinding the stack starts |
| 22:03:56 | Araq | and that can prevent unwinding the stack |
| 22:05:32 | gradha | the change happens in the onRaise hook then |
| 22:06:05 | Araq | yeah |
| 22:40:08 | gradha | some contribution https://github.com/Araq/Nimrod/pull/245 |
| 22:43:12 | Araq | gradha: you read my sections about it in the manual, right? |
| 22:43:46 | * | Trix[a]r_za is now known as Trixar_za |
| 22:44:56 | Araq | "In this situation, call the nimrod compiler with the ``check`` command instead of ``compile``. ..." |
| 22:45:03 | Araq | this is not true :-) |
| 22:45:14 | Araq | that was merely a bug which has been fixed |
| 22:49:40 | gradha | ok, will change and push again, something else that needs changing? |
| 22:52:38 | Araq | wait a sec |
| 22:53:24 | Araq | the rest seems fine |
| 22:54:12 | Araq | I'm not sure all this belongs into the tutorial, but oh well ;-) |
| 22:54:52 | Araq | we said the tutorial should teach the stdlib, so it's fine |
| 22:56:41 | gradha | it doesn't try to reproduce the contents of the manual, but if you don't point to it from there not many people are going to even know that the {.raises.} pragma exists, and saying it just after introducing exceptions seems ok to me |
| 22:57:45 | Araq | yeah it's good |
| 23:03:01 | gradha | changes pushed |
| 23:03:06 | gradha | bye |
| 23:03:17 | * | gradha quit (Quit: gradha) |
| 23:36:33 | * | fowl quit (Remote host closed the connection) |
| 23:37:00 | * | fowl joined #nimrod |