Janus to Bob Compiler - Syntax

The syntax of Janus is quite like that of an ordinary imperative programming language, but extended with a set of exit conditions for conditional statements. These are here illustrated with flowcharts. A thing to note is that of undefined behavior. The constructs mentioned below all can result in undefined behavior. However during translation we do not have to explicitly make tests and report undefined behavior - this is done automatically.

If condition

Figure 1: Flowchart of reversible if-statement

As seen in Figure 1. We must be able to decide what branch has been taken after the whole statement has executed. Therefore we add the fi exit condition. The behavior is as follows:

If if evaluates to true, then then is executed after which fi must evaluate to true. If not, undefined behavior will occur.
If if evaluates to false, else is executed, and fi must also evaluate to false, otherwise undefined behavior will occur.

Loops

As seen in Figure 2. Loops acts as follows: initially entry must be true, and do is executed. If exit evaluates to true, the loop is terminated. Otherwise loop is executed after which entry must evaluate to false. After this point we keep looping until exit becomes true. If at any point after the initial entry becomes true, undefined behavior will occur. If on the other hand entry evaluates to false in the initial phase, undefined behavior will occur.

Local - Delocal

As stated in Figure 3. We initialize v_{1} of type t_{1} with expression e_{1}. Now statement s_{1} is executed. If we delocal using a different name or a different type, undefined behavior could occur. However we can catch this in the type checker. However if v_{1} \neq e_{2}, undefined behavior will occur.

Janus Syntax

Without further ado

Prog    \rightarrow P_{main} 
D       \rightarrow X
        | X [ C ]
T       \rightarrow "int"
        | "stack"
P_{main}    \rightarrow "procedure" "main" ( ) Declare
Declare \rightarrow \epsilon
        | "int" D Declare
        | "stack" x Declare
P       \rightarrow \epsilon
        | "procedure" Q ( P_{args} ) S_{comp} P
P_{args}    \rightarrow T X_{arg} , P_{args}
        | T X_{arg}
S_{comp}    \rightarrow S
        | S S_{comp}
S       \rightarrow X Bind_{op} E
        | X [ E ] Bind_{op} E
        | X <=> X
        | "if" E "then" S_{comp} "else" S_{comp} "fi" E
        | "from" E "do" S_{comp} "loop" S_{comp} "until" E
        | "local" T X = E S_{comp} "delocal" T X = E
        | "call" Q ( Call_{args} )
        | "uncall" Q ( Call_{args} )
        | "push" ( X , X )
        | "pop" ( X , X )
        | "show" ( X )
        | "skip"
Call_{args}     \rightarrow X , Call_{args}
        | X
E       \rightarrow E_{lit}
        | - E
        | E + E
        | E - E
        | E ^ E
        | E * E
        | E / E
        | E % E
        | E & E
        | E && E
        | E | E
        | E || E
        | E < E
        | E > E
        | E = E
        | E != E
        | E <= E
        | E >= E
E_{lit}     \rightarrow ( E )
        | C
        | X
        | X [ E ]
        | E_{p-buildin}
        | "nil"
E_{p-buildin}   \rightarrow "size" ( X )
        | "empty" ( X )
        | "top" ( X )
C       \rightarrow val_{int}
Bind_{op}   \rightarrow +=
        | -=
        | ^=
X       \rightarrow val_{id}
X_{arg}     \rightarrow val_{id}
        | val_{id} []
Q       \rightarrow val_{id}

The syntax is made to fit FsLexYacc. The result is a list of procedures each containing a list of statements. The complete parser can be found here. I use the .yy extension because vim can recognize and highlight this by default.