Some progress with the DIP1000 semantics. So I made a few changes to the
grammar of the mini-language (call it MiniD1000), which is at
http://erdani.com/d/DIP1000-grammar.html. Notable aspects:
* Programs are a sequence of function definitions, struct definitions,
and global variable definitions. A pass is supposed to go through all
and create the initial typing environment.
* Functions now only have one parameter. This is to reduce the size of
the language (two parameters increase the numbers of typing and
evaluation rules). Aliasing can be studied with globals. I'm unclear
whether we need the second parameter for investigating things like
cross-parameter aliasing; if so, I'll add it back.
* All functions are required to end with a return statement. This avoids
any need for flow control.
* There are no rvalues in MinbiD1000, which I thought is quite clever.
That means `null` and integral literals are not expressions; they are
explicitly present in assignment statements. This simplifies MiniD1000 a
great deal, but again will require us to be careful when we "port"
whatever conclusions we draw back to D.
* The `if` statement has no `else` clause. It only increases the size of
the language without an increase in expressiveness.
Next, I defined a baseline set of typing rules at
http://erdani.com/d/DIP1000-typing-baseline.html for "bad" MiniD1000:
all ref, scope and return attributes are ignored, so there's no special
protection against bad escapes. Based on these rules we'll later define
better rules that enforce safety. A few notes:
* For a general understanding on how to read these rules, see the
Featherweight Java (FJ) paper or see e.g.
http://www.hedonisticlearning.com/posts/understanding-typing-judgments.html.
* Like in FJ, sequences of zero or more things are shown with an overbar.
* In order to identify the current function being compiled, I introduce
the symbol f_{crt}. For example, in rule S-VarDeclaration, a
prerequisite of the judgment is that f_{crt} exists, i.e. the rule
S-VarDeclaration only applies inside a function, not outside. For the
outside rule see D-GlobalVarDeclaration.
* S-VarDeclaration introduces a new name visible to the statements that
follow. This is done by typing not only the variable declaration, but
also all following statements in its scope. The typing environment for
the statements is the union of the preexisting typing environment and
the new variable.
* In fact the typing rules of all statements carry the appendix "and
here are the following statements in the scope" which is workable but
possibly a bit goofy. Any cleverer idea?
* For that matter I need the rule S-NoStmts: "a sequence of zero
statements types just fine".
* In D-Struct, I vaguely state that a struct shall not be a transitive
field of itself. Is there a better way to enforce that succintly?
Please let me know of anything I missed or got wrong. Once the baseline
typing is in place, the hard part starts: defining the enhanced typing
that enforces safe scoping rules.
Thanks,
Andrei
