K-user mailing list

[Ulrich Kühne <ulrichk AT informatik.uni-bremen.de>]

Hi,

I am trying to define an imperative language with goto. My idea is to 
have a first "parsing phase", where I put all the statements into a list 
and add an index to each statement. Only after this, I "load" one 
statement at a time into the execution context, indexed by a <pc> 
program counter.

The problem is that the execution / evaluation gets stuck. I guess I 
need some heating rules, but I don't know how to write them. Obviously, 
I don't want the statements to be executed during the parsing phase, but 
only after loading them, so I cannot use a standard sequential heating 
like S:Stmt S2 => S ~> S2.

Does anyone have a good idea how to make this work? I attached the 
definition and an example. The execution yields this:

sputnik$ krun test.goto
<T>
    <k>
        .K
    </k>
    <pc>
        3
    </pc>
    <ctx>
        z = (7 + 8)                  <===== GETTING STUCK!
    </ctx>
    <state>
        RUNNING
    </state>
    <rom>
        ListItem([ 0 , (x = 5) ])
        ListItem([ 1 , (y = 6) ])
        ListItem([ 2 , (z = (7 + 8)) ])
        ListItem([ 3 , (u = (x + 1)) ])
        ListItem([ 4 , (if (u == (x + 2)) then (v = 0) else (v = (x + 1))) ])
        ListItem([ 5 , (w = 42) ])
    </rom>
    <store>
        x |-> 5
        y |-> 6
    </store>
</T>


Thanks for your help
Ulrich

module GOTO-SYNTAX
  syntax Atom  ::= Id | Int
  syntax Exp   ::= Atom
                 | Exp "+" Exp [left,strict]
                 | Exp "-" Exp [left,strict]
                 > Exp "==" Exp [left,strict]
                 | Exp "<=" Exp [left,strict]            
  syntax Stmt  ::= Id "=" Exp [strict(2)]
                 | "if" Exp "then" Stmt "else" Stmt [strict(1)]
                 | "goto" Int
  syntax Prog  ::=      
                   Stmt
                 | Prog Prog [right]
endmodule


module GOTO imports GOTO-SYNTAX 

  syntax State ::= "PARSING" | "RUNNING"

  configuration
  <T>
    <k> $PGM:K </k>
    <state> PARSING </state>
    <pc> 0 </pc>
    <rom> .List </rom>
    <ctx> .K </ctx>
    <store> .Map </store>
  </T>

  //@ note if parsing is done
  rule <k>.</k><state>PARSING => RUNNING</state>

  //@ we add indices to statements in order to perform GOTO later
  syntax IdxStmt ::= "[" Int "," Stmt "]"

  //@ Parse statements, add indices and put them into the ROM
  rule <k>S:Stmt S2 => S2</k>
       <rom> . => ListItem([0,S]) </rom>
  rule <k>S:Stmt => .</k>
       <rom> . => ListItem([0,S]) </rom>
  rule <k>S:Stmt S2 => S2</k>
       <rom>... ListItem([I,T]) => ListItem([I,T]) ListItem([I +Int 
1,S])</rom>
  rule <k>S:Stmt => .</k>
       <rom>... ListItem([I,T]) => ListItem([I,T]) ListItem([I +Int 
1,S])</rom>

  syntax KResult ::= Int

  //@ Evaluation of arithmetic expressions
  rule X:Int + Y:Int => X +Int Y 
  rule X:Int - Y:Int => X -Int Y 
  
  //@ Evaluation of equality expressions
  rule X:Int == Y:Int => 1 when X ==Int Y 
  rule X:Int == Y:Int => 0 when X =/=Int Y 
  rule X:Int <= Y:Int => 1 when X <=Int Y 
  rule X:Int <= Y:Int => 0 when X >Int Y 
  
  //@ Variable lookup
  rule <ctx>X:Id => Y ...</ctx>
       <store>... X|->Y ...</store>

  //@ Evaluate if condition
  rule <ctx>if G:Int then S1 else S2 => S1 </ctx>
  when G =/=Int 0 
  rule <ctx>if G:Int then S1 else S2 => S2 </ctx>
  when G ==Int 0 

  //@ Assignment
  rule <ctx>X:Id = Y:Int => . ...</ctx>
       <store> ... . => X|->Y ... </store>  

  //@ Go to
  rule <ctx>goto T:Int => . </ctx>
       <pc> _ => T </pc>

  //@ Execute next statement
  rule <state> RUNNING </state>
       <ctx>. => S </ctx>
       <pc> I:Int => I +Int 1</pc>
       <rom>... ListItem([I,S:Stmt]) ...</rom>
  
endmodule

x = 5
y = 6
z = 7 + 8
u = x + 1
if u == x + 2 then v = 0 else v = x + 1
w = 42