*** Description of grid and grid ops

fmod GRID is
  pr NAT .

  sorts Loc LocSet .
  subsort Loc < LocSet .

  op mt : -> LocSet .
  op __ : LocSet LocSet -> LocSet [ assoc comm id: mt ] .

  op `(_`,_`) : Nat Nat -> Loc .

  op member : Loc LocSet -> Bool .
  eq member(l:Loc, l:Loc ls:LocSet) = true .
  eq member(l:Loc, ls:LocSet) = false [owise] .

  sort Dir .
  ops N W E S : -> Dir .

  op newLoc : Nat Nat Loc Dir LocSet -> Loc .
  op next : Nat Nat Loc Dir -> Loc .

  vars ht wd x y : Nat .
  
  eq newLoc(ht, wd, (x,y) , d:Dir, blocked:LocSet) 
      = ( if member(next(ht,wd,(x,y),d:Dir),blocked:LocSet)
          then (x,y)
          else next(ht,wd,(x,y),d:Dir)
          fi )  .

  eq next(ht,wd, (x,y), N) = 
       if (s y < ht) then (x, s y) else (x,y) fi .

  eq next(ht,wd, (x,y), S) =
       if (0 < y) then (x, sd(y,1)) else (x,y) fi .

  eq next(ht,wd, (x,y), E) = 
       if (s x < wd) then (s x, y) else (x,y) fi .

  eq next(ht,wd, (x,y), W) =
       if (0 < x) then (sd(x,1), y) else (x,y) fi .

  op dir : Nat -> Dir .
  eq dir(0) = N .
  eq dir(90) = E .
  eq dir(180) = S .
  eq dir(270) = W .
endfm  


fmod GRID-TEST is
  inc GRID .
  op B : -> LocSet .
  eq B = (1,1) (2,2) (3,3) .
 
endfm

***(
red newLoc(5,5, (0,0) , N, B) .
red newLoc(5,5, (0,0) , S, B) .
red newLoc(5,5, (0,0) , E, B) .
red newLoc(5,5, (0,0) , W, B) .

red newLoc(5,5, (1,0), N, B) .
red newLoc(5,5, (4,4), N, B) .

)