-- ==========================================================
--> An example answer for exercises of lecture4
-- ==========================================================

--
-- 1. A possible solution is as follows:
--

mod! EXP {
  pr(NAT)
  [Nat < Exp]
  op _++_ : Exp Exp -> Exp {constr l-assoc prec: 30}
  op _--_ : Exp Exp -> Exp {constr l-assoc prec: 30}
  op _**_ : Exp Exp -> Exp {constr l-assoc prec: 29}
  op _//_ : Exp Exp -> Exp {constr l-assoc prec: 29}
  op _%%_ : Exp Exp -> Exp {constr l-assoc prec: 29}
  op /_ : Exp -> Exp {constr prec 28}
  op _^2 : Exp -> Exp {constr prec 27}
  op _! : Exp -> Exp {constr prec 27}
}

mod! NAT-ERR+ {
  pr(NAT)
  [Nat ErrNat < Nat&Err]
  op errNat : -> ErrNat {constr}
  op _+_ : Nat&Err Nat&Err -> Nat&Err {assoc comm}
  op _*_ : Nat&Err Nat&Err -> Nat&Err {assoc comm}
  op sd : Nat&Err Nat&Err -> Nat&Err 
  op _quo_ : Nat&Err Nat&Err -> Nat&Err 
  op _rem_ : Nat&Err Nat&Err -> Nat&Err
  --
  op sq : Nat&Err -> Nat&Err
  op sq : Nat -> Nat
  op sqr : Nat&Err -> Nat&Err
  op sqr : Nat -> Nat
  op pivot : Nat Nat -> Nat
  op bs : Nat Nat Nat Nat -> Nat
  op fact : Nat&Err -> Nat&Err
  op fact : Nat -> Nat
  vars N L U X : Nat
  var NzN : NzNat
  eq sq(errNat) = errNat .
  eq sq(N) = N * N .
  eq sqr(errNat) = errNat .
  eq sqr(N) = bs(0,N,pivot(0,N),N) .
  eq pivot(L,U) = if 2 divides sd(U,L) then L + (sd(U,L) quo 2)
                  else L + (sd(U,L) quo 2) + 1 fi .
  eq bs(L,U,X,N)
     = if L == U then L
       else (if sq(X) > N
             then bs(L,sd(X,1),pivot(L,sd(X,1)),N)
             else bs(X,U,pivot(X,U),N) fi) fi .
  eq fact(errNat) = errNat .
  eq fact(0) = 1 .
  eq fact(NzN) = NzN * fact(p NzN) .
}

mod! INTERPRETER {
  pr(NAT-ERR+)
  pr(EXP)
  op interpret : Exp -> Nat&Err
  var N : Nat
  vars E E1 E2 : Exp
  eq interpret(N) = N .
  eq interpret(E1 ++ E2) = interpret(E1) + interpret(E2) .
  eq interpret(E1 -- E2) = sd(interpret(E1),interpret(E2)) .
  eq interpret(E1 ** E2) = interpret(E1) * interpret(E2) .
  eq interpret(E1 // E2) = interpret(E1) quo interpret(E2) .
  eq interpret(E1 %% E2) = interpret(E1) rem interpret(E2) .
  eq interpret(E ^2)     = sq(interpret(E)) .
  eq interpret(/ E)    = sqr(interpret(E)) .
  eq interpret(E !)      = fact(interpret(E)) .
}

open INTERPRETER
  red interpret((3 ++ / (3 ^2 -- 4 ** 1 ** 2)) // (2 ** 1)) .
  red interpret((3 -- / (3 ^2 -- 4 ** 1 ** 2)) // (2 ** 1)) .
  red interpret(1 ++ 5 !) .
close


--
-- 2. A possible solution is as follows:
--

mod! LIST (M :: TRIV) {
  [List]
  op nil : -> List {constr}
  op _|_ : Elt.M List -> List {constr}
  op _@_ : List List -> List {r-assoc}
  var E : Elt.M
  vars L1 L2 : List
  eq nil @ L2 = L2 .
  eq (E | L1) @ L2 = E | (L1 @ L2) .
}

mod! COMMAND {
  pr(NAT)
  [Command]
  op push : Nat -> Command {constr}
  op multiply : -> Command {constr}
  op divide : -> Command {constr}
  op mod : -> Command {constr}
  op add : -> Command {constr}
  op minus : -> Command {constr}
  op sq : -> Command {constr}
  op sqr : -> Command {constr}
  op fact : -> Command {constr}
}

mod! CLIST {
  pr(LIST(COMMAND{sort Elt -> Command}) * {sort List -> CList})
}

mod! STACK {
  pr(LIST(NAT-ERR+{sort Elt -> Nat&Err}) * {sort List -> Stack, op nil -> empstk})
  [Stack ErrStack < Stack&Err]
  op errStack : -> ErrStack {constr}
  op _|_ : Nat&Err Stack&Err -> Stack&Err {constr}
  eq errNat | S&E:Stack&Err = errStack .
  eq N&E:Nat&Err | errStack = errStack .
}

mod! VM {
  pr(CLIST)
  pr(STACK)
  op vm : CList -> Nat&Err
  op exec : CList Stack&Err -> Nat&Err
  var CL : CList
  var PC : Nat
  var Stk : Stack
  vars N N1 N2 : Nat
  eq vm(CL) = exec(CL,empstk) .
  eq exec(nil,N | empstk) = N .
  eq exec(push(N) | CL,Stk) = exec(CL,N | Stk) .
  eq exec(add | CL,empstk) = errNat .
  eq exec(add | CL,N1 | empstk) = errNat .
  eq exec(add | CL,N2 | N1 | Stk) = exec(CL,N1 + N2 | Stk) .
  eq exec(multiply | CL,empstk) = errNat .
  eq exec(multiply | CL,N1 | empstk) = errNat .
  eq exec(multiply | CL,N2 | N1 | Stk) = exec(CL,N1 * N2 | Stk) .
  eq exec(divide | CL,empstk) = errNat .
  eq exec(divide | CL,N1 | empstk) = errNat .
  eq exec(divide | CL,N2 | N1 | Stk) = exec(CL,N1 quo N2 | Stk) .
  eq exec(mod | CL,empstk) = errNat .
  eq exec(mod | CL,N1 | empstk) = errNat .
  eq exec(mod | CL,N2 | N1 | Stk) = exec(CL,N1 rem N2 | Stk) .
  eq exec(minus | CL,empstk) = errNat .
  eq exec(minus | CL,N1 | empstk) = errNat .
  eq exec(minus | CL,N2 | N1 | Stk) = exec(CL,sd(N1,N2) | Stk) .
  eq exec(sq | CL,empstk) = errNat .
  eq exec(sq | CL,N | Stk) = exec(CL,sq(N) | Stk) .
  eq exec(sqr | CL,empstk) = errNat .
  eq exec(sqr | CL,N | Stk) = exec(CL,sqr(N) | Stk) .
  eq exec(fact | CL,empstk) = errNat .
  eq exec(fact | CL,N | Stk) = exec(CL,fact(N) | Stk) .
}

open VM
  ops cl1 cl2 cl3 : -> CList .
  eq cl1 = push(3) | push(3) | sq | push(4) | push(1) |
           multiply | push(2) | multiply | minus | sqr |
           add | push(2) | push(1) | multiply | divide | nil .
  eq cl2 = push(3) | push(3) | sq | push(4) | push(1) |
           multiply | push(2) | multiply | minus | sqr |
           minus | push(2) | push(1) | multiply | divide | nil .
  eq cl3 = push(5) | fact | push(1) | add | nil .
  red vm(cl1) .
  red vm(cl2) .
  red vm(cl3) .
close

-- ==========================================================
--> end end end
-- ==========================================================