***
*** Gordon's Computer - Programmer's Model
***

*** Module defining: sorts for opcodes (3 bits);
*** addresses (13 bits); and words (16 bits).
*** Also operators to extract opcode and
*** address fields from instructions, and
*** arithmetic.
fmod MACHINE-WORD is
    protecting BINARY .

    sorts Address Word Opcode .

    subsort Address < Bits .
    subsort Word < Bits .
    subsort Opcode < Bits .

    ops zero one : -> Word .
    op opcode : Word -> Opcode .
    op addr : Word -> Address .
    op _+_ : Word Word -> Word [assoc comm] .
    op _-_ : Word Word -> Word .
    op _+_ : Address Address -> Address [assoc comm] .
    
    vars a b c d e f g h : Bit .
    vars i j k l m n o p : Bit .
    vars A B : Word .
    vars C D : Address .

    mb (a b c) : Opcode .
    mb (a b c d e f g h i j k l m) : Address .
    mb (a b c d e f g h i j k l m n o p ) : Word .

    eq one = (0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1) .
    eq zero = (0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0) .

    eq opcode(A) = bits(A,15,13) .
    eq addr(A) = bits(A,12,0) .

    eq A + B = bits(A ++ B, 15,0) .
    eq A - B = bits(A ++ (not B ++ one), 15, 0) .
    eq C + D = bits(C ++ D, 12, 0) .
endfm

*** Module defining memory.
fmod MEM is

    protecting MACHINE-WORD .

    sort Mem .

    op _[_] : Mem Address -> Word .
    op _[_/_] : Mem Word Address -> Mem .

    var M : Mem .
    var A : Word .
    vars I J : Address .

    eq M[A / I][I] = A .
    eq M[A / I][J] = M[J] [owise] .
endfm

*** Module defining the various state elements.
*** This is more complex than normal because of the
*** input-output streams/values.
fmod GORDON-STATE is
    protecting MEM .

    *** The four position dial.
    sort Dial .

    *** Streams of: switch values, button pushes
    *** and dial positions.
    sorts SwitchStr BitStr DialStr .

    *** The state of the machine.
    sort GordonState .

    *** The output of the machine.
    sort GordonOut .

    *** The combined state and output
    sort GordonAll .

    *** Constants representing dial positions
    ops LoadPC LoadACC Store Run : -> Dial .

    *** Operators to evaluate streams,
    *** returning value on a stream at a given
    *** time.
    op _(_) : SwitchStr Int -> Word .
    op _(_) : BitStr Int -> Bit .
    op _(_) : DialStr Int -> Dial .

    *** Operator to make a machine state tuple.
    op _,_,_,_ : Mem Word Address Bit -> GordonState .

    *** Operator to make an output tuple.
    op _,_,_,_ : Word Address
        Bit Bit -> GordonOut .

    *** Operator to combine state and output.
    op _,_ : GordonState GordonOut -> GordonAll .
endfm

*** Module defining the various State, Next-State
*** and output functions.
fmod GORDON-PM is
    protecting GORDON-STATE .

    *** The main iterated map function
    op GORDON : Int GordonState SwitchStr
        BitStr DialStr -> GordonAll .

    *** The state function
    op GORDON-STATE : Int GordonState SwitchStr
        BitStr DialStr -> GordonState .

    *** The output function
    op GORDON-OUT : Int GordonState SwitchStr
        BitStr DialStr -> GordonOut .

    *** The next-state function
    op next : GordonState Word Bit Dial -> GordonState .

    *** function to compute the output at a given time
    op out : GordonState -> GordonOut .

    *** function to execute one instruction
    op exec : GordonState -> GordonState .
    
    var M : Mem .
    var ACC : Word .
    var PC : Address .
    var IDLE : Bit .
    var SWstr : SwitchStr .
    var BUTTONstr : BitStr .
    var DIALstr : DialStr .
    var T : Int .
    var SW : Word .
    var BUTTON : Bit .
    var DIAL : Dial .

    *** The state and output of the machine at any given
    *** time is computed by the state and output functions
    eq GORDON(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr) =
        (GORDON-STATE(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr),
	 GORDON-OUT(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr)) .

    *** At time zero, the state of the machine is just the
    *** initial state.
    eq GORDON-STATE(0,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr) =
        (M,ACC,PC,IDLE) .

    *** At other times, the state of the machine is the
    *** next state function applied to the state at the
    *** machine at the time before.
    eq GORDON-STATE(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr) =
        next(GORDON-STATE(T - 1,M,ACC,PC,IDLE,
	      SWstr,BUTTONstr,DIALstr),
	   SWstr(T),BUTTONstr(T),DIALstr(T)) [owise] .

    *** At any time, the output of the machine is the out
    *** function applied to the state.
    eq GORDON-OUT(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr) =
	 out(GORDON-STATE(T,M,ACC,PC,IDLE,SWstr,
	     BUTTONstr,DIALstr)) .

    *** If the machine is idle, and the button pressed while
    *** the dial is in the 'LoadPC' position, we load the
    *** switches into the program counter.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        (M, ACC, bits(SW,12,0), 1) if (IDLE == 1) and
	                              (BUTTON == 1) and
                                      (DIAL == LoadPC) .
				      
    *** If the machine is idle, and the button pressed while
    *** the dial is in the 'LoadACC' position, we load the
    *** switches into the accumulator.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        (M, SW, PC, 1) if (IDLE == 1) and
	                  (BUTTON == 1) and
                          (DIAL == LoadACC) .
			  
    *** If the machine is idle, and the button pressed while
    *** the dial is in the 'Store' position, we store the
    *** accumulator in the memory at the address specified by
    *** the program counter.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        (M[ACC / PC], ACC, PC, 1) if (IDLE == 1) and
	                           (BUTTON == 1) and
                                   (DIAL == Store) .

    *** If the machine is idle and the button is not pressed,
    *** we remain idle; if the machine is running and the
    *** button is pressed, it stops.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        (M, ACC, PC, 1) if ((IDLE == 1) and
	                    (BUTTON == 0)) or
                           ((IDLE == 0) and
			    (BUTTON == 1)) .
			 
    *** If the machine is running and we do not press the
    *** button, it executes the next instruction; if it is
    *** idle and we press the button with the dial in the
    *** 'Run' position, we start execution.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        exec(M, ACC, PC, 0) if ((IDLE == 0) and
	                    (BUTTON == 0)) or
                           ((IDLE == 1) and
			    (BUTTON == 1) and
			    (DIAL == Run)) .

    *** Stop the machine.
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC,PC,1) if opcode(M[PC]) == (0 0 0) .

    *** Jump unconditionally.
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC,addr(M[PC]),0)
                        if opcode(M[PC]) == (0 0 1) .
			
    *** A successful conditional jump (ACC == 0) .
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC,addr(M[PC]),0)
                        if opcode(M[PC]) == (0 1 0)
			   and (ACC == zero) .
			   
    *** An unsuccessful conditional jump (ACC =/= 0)
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC,PC + one,0)
                        if opcode(M[PC]) == (0 1 0)
			   and (ACC =/= zero) .
			   
    *** Addition.
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC + M[addr(M[PC])],PC + one,0)
                        if opcode(M[PC]) == (0 1 1) .

    *** Subtraction.
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC - M[addr(M[PC])],PC + one,0)
                        if opcode(M[PC]) == (1 0 0) .

    *** Load.
    ceq exec(M,ACC,PC,IDLE) =
        (M,M[addr(M[PC])],PC + one,0)
                        if opcode(M[PC]) == (1 0 1) .

    *** Store.
    ceq exec(M,ACC,PC,IDLE) =
        (M[ACC / addr(M[PC])],ACC,PC + one,0)
                        if opcode(M[PC]) == (1 1 0) .
			
    *** Skip (no-op).
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC,PC + one,0)
                        if opcode(M[PC]) == (1 1 1) .

    *** The output function
    eq out(M,ACC,PC,IDLE) = (ACC,PC,IDLE,1) .
endfm