-

/* File: simp3.k */

requires "arithbool.k"

module SIMP3-SYNTAX
  imports ARITHBOOL-SYNTAX
  imports ARITHBOOL-SEMANTICS

/*
ARITHBOOL-SYNTAX introduces (variable free) arithmetic and boolean
expressions. We wish to extend it with references, which encompass
variables, and arrays.  References will be represented by identifiers
naming locations, or nil when a location has not yet been assigned.
These need to be values, to be the value of reference variables.
*/

  syntax Ref ::= "ref" Id
  syntax Loc ::= "nil" | Ref
//  syntax Array ::= "array" Map // Int -> Val
  syntax Val ::= Int | Loc // | Array

  syntax E ::= Val // Why do I need this for the rule on line 91
  syntax KResult ::= Loc

/*
We extend our syntax with variables represented by identifiers naming
them, repeated dereferencing, and array elements. These will be
syntactic elements to which we may assign.  They may also occur as
expressions inside an arithmentic expression.
*/

  syntax Mutable ::= Id   // Id as variable
                   | Ref
                   | "(" Mutable ")"    [bracket]
                   |  "*" Mutable       [strict]
                   > Mutable "[" E "]"  [strict(2,1)]

  syntax E ::= Mutable

/*
Our syntax for commands needs to be expanded to allow assignment to
mutable terms, not just identifiers.  We will also incorporate the
alias command from simp2.k.
*/

  syntax CFinal ::= "skip"

  syntax C ::= CFinal
             | C ";" C                         [right, strict(1)]
             | "alias" Id "=" Id
             | Mutable ":=" E                  [strict(2)]
             | "if" B "then" C "else" C "fi"   [strict(1)]
             | "{" C "}"
             | "while" B "do" C "od"


/*
S is the syntactic catogory of "syntax", allowing us to incrementally
test each new construct.  It already contains E and B.
*/

 syntax S ::= C


  syntax KResult ::= CFinal

  syntax LVal ::= Ref | "lvalue" Mutable | "(" LVal ")" [bracket]
                   | "forcervalue" Mutable   // so that we can cause assignment to also allocate
                   | "star" LVal [strict]
  syntax Cint ::= C | "assign" LVal Val [strict(1)]
  syntax MutCalc ::= Mutable

endmodule

module SIMP3
  imports SIMP3-SYNTAX
  imports ARITHBOOL-SEMANTICS

  configuration
  <T>
   <k> $PGM:S </k>
    <loc> .Map </loc>
    <mem> .Map </mem>
  </T>

  rule skip ; C2 => C2
  rule if true then C1 else C2 fi => C1
  rule if false then C1 else C2 fi => C2
  rule {C} => C                                [structrual]
  rule while B do C od => if B then {C ; while B do C od} else skip fi
  rule M := (V:Val) => assign (lvalue M) V

  rule <k> I:Id => V ... </k>
       <loc> ... (I |-> L) ... </loc>
       <mem> ... (L |-> V) ... </mem>

  rule <k> (* (ref (L:Id))) => V ...</k>
       <mem> ... (L |-> V) ...</mem>

/*
// Use this if you can't alias a declared variable
  rule <k> alias I1:Id = I2:Id => skip ... </k>
       <loc>Loc:Map (.Map => I1 |-> Loc[I2]) </loc>
       requires (notBool(I1 in keys(Loc)))
*/

// Use this if we are allowing aliasing already declared variables.
  rule <k> alias I1:Id = I2:Id => skip ... </k>
       <loc> Loc => Loc[ I1 <- Loc[I2] ] </loc>

  rule <k> assign (ref (L)) V => skip ... </k>
       <mem> Mem:Map => Mem[L <- V]   </mem>

  rule <k> lvalue Id => ref(L) ...</k>
       <loc>  ... (Id|-> L) ... </loc>

/* 
Use if we want assigning to a variable to allocate space for it even
if it hasn't been previously declared.
*/
  rule <k> lvalue (Id:Id) => ref(!L) ...</k>
       <loc> Loc:Map (.Map => Id |-> !L) </loc>
       requires (notBool(Id in keys(Loc)))

  rule lvalue (ref(L)) => ref(L)

//  rule lvalue (* M) => M

  rule lvalue (* M) => forcervalue M // This must be a ref

  rule <k> forcervalue (Id:Id) => ref L2 ... </k>
       <loc> ... Id |-> L1 ...</loc>
       <mem> ... L1 |-> ref L2 ... </mem>

  rule <k> forcervalue (Id:Id) => ref !L2 ... </k>
       <loc> ... Id |-> L1 ...</loc>
       <mem>  Mem:Map(.Map => L1 |-> ref !L2) </mem>

  rule <k> forcervalue (Id:Id) => ref (!L2:Id) ... </k>
       <loc> Loc:Map (.Map => Id |-> (!L1:Id)) </loc>
       <mem> Mem:Map (.Map => !L1 |-> ref !L2) </mem>
       requires (notBool(Id in keys(Loc)))

// forcervalue of an Int is an error

  rule forcervalue (ref L) => ref L

  rule forcervalue (* M) => star (forcervalue M)


  rule <k> star (ref L1) => ref L2 ... </k>
       <mem> ... L1 |-> ref L2 ... </mem>

  rule <k> star (ref L1) => ref !L2 ... </k>
       <mem> Mem:Map (.Map => L1 |-> ref !L2) </mem>
       requires notBool(L1 in keys(Mem))

endmodule