--
-- Minila interpreter
--

--
-- - Function interpret interprets a given Minila program,
--   returning the environment made by executing the progam.
-- - Function eval takes a Minila program and an environment 
--   and executes the program under the environment, returning
--   the environment updated by executing the progam.
-- - Function evalAssign executes an assignment under a given
--   environment.
-- - Function evalIf executes an If statement under a given
--   environment.
-- - Function evalWhile executes a While statement under a given
--   environment.
-- - Function evalFor executes a For statement under a given
--   environment.
-- - Function evalExp computes an expression under a given
--   environment, returning the result (a natural number).
--
mod! INTERPRETER {
  pr(STM)
  pr(ENV)
  op interpret : Stm -> Env&Err
  op eval : Stm Env&Err -> Env&Err
  op evalAssign : Var Nat&Err Env&Err -> Env&Err
  op evalIf : Nat&Err Stm Stm Env&Err -> Env&Err
  op evalWhile : Exp Stm Env&Err -> Env&Err
  op evalFor : Var Exp Stm Nat&Err Env&Err -> Env&Err
  op evalExp : Exp Env&Err -> Nat&Err
  vars E E1 E2 : Exp
  vars S S1 S2 : Stm
  var V : Var
  var EV : Env
  var N : Nat
  -- interpret
  eq interpret(S) = eval(S,empEnv).
  -- eval
  eq eval(S,errEnv) = errEnv .
  eq eval(estm,EV) = EV .
  eq eval(V := E ; S,EV)
     = eval(S,evalAssign(V,evalExp(E,EV),EV)) .
  eq eval(if E then S1 else S2 fi S,EV)
     = eval(S,evalIf(evalExp(E,EV),S1,S2,EV)) .
  eq eval(while E do S1 od S,EV)
     = eval(S,evalWhile(E,S1,EV)) .
  eq eval(for V E1 E2 do S1 od S,EV)
     = eval(S,evalFor(V,E2,S1,evalExp(E1,EV),EV)) .
  -- evalAssign
  eq evalAssign(V,errNat,EV) = errEnv .
  eq evalAssign(V,N,errEnv) = errEnv .
  eq evalAssign(V,errNat,errEnv) = errEnv .
  eq evalAssign(V,N,EV) = update(V,N,EV) .
  -- evalIf
  eq evalIf(errNat,S1,S2,EV) = errEnv .
  eq evalIf(N,S1,S2,errEnv) = errEnv .
  eq evalIf(errNat,S1,S2,errEnv) = errEnv .
  eq evalIf(N,S1,S2,EV)
     = if N == 0 then eval(S2,EV) else eval(S1,EV) fi .
  -- evalWhile
  eq evalWhile(E,S,errEnv) = errEnv .
  eq evalWhile(E,S,EV)
     = if evalExp(E,EV) == errNat then errEnv
       else (if evalExp(E,EV) == 0 then EV else evalWhile(E,S,eval(S,EV)) fi)
       fi .
  -- evalFor
  eq evalFor(V,E,S,errNat,EV) = errEnv .
  eq evalFor(V,E,S,N,errEnv) = errEnv .
  eq evalFor(V,E,S,errNat,errEnv) = errEnv .
  eq evalFor(V,E,S,N,EV)
     = if evalExp(V,update(V,N,EV)) == errNat
          or evalExp(E,update(V,N,EV)) == errNat
       then errEnv
       else (if evalExp(V,update(V,N,EV)) > evalExp(E,update(V,N,EV))
             then update(V,N,EV)
             else (if eval(S,update(V,N,EV)) == errEnv then errEnv
                   else evalFor(V,E,S,
                                lookup(V,eval(S,update(V,N,EV))) + 1,
                                eval(S,update(V,N,EV)))
                   fi )
             fi )
       fi .
  -- evalExp
  eq evalExp(E,errEnv) = errNat .
  eq evalExp(N,EV) = N .
  eq evalExp(V,EV) = lookup(V,EV) .
  eq evalExp(E1 ++ E2,EV) = evalExp(E1,EV) + evalExp(E2,EV) .
  eq evalExp(E1 -- E2,EV) = sd(evalExp(E1,EV),evalExp(E2,EV)) .
  eq evalExp(E1 ** E2,EV) = evalExp(E1,EV) * evalExp(E2,EV) .
  eq evalExp(E1 // E2,EV) = evalExp(E1,EV) quo evalExp(E2,EV) .
  eq evalExp(E1 %% E2,EV) = evalExp(E1,EV) rem evalExp(E2,EV) .
  eq evalExp(E1 === E2,EV)
     = if evalExp(E1,EV) == errNat or evalExp(E2,EV) == errNat
       then errNat
       else (if evalExp(E1,EV) == evalExp(E2,EV) then 1 else 0 fi) fi .
  eq evalExp(E1 !== E2,EV)
     = if evalExp(E1,EV) == errNat or evalExp(E2,EV) == errNat
       then errNat
       else (if evalExp(E1,EV) == evalExp(E2,EV) then 0 else 1 fi) fi .
  eq evalExp(E1 << E2,EV)
     = if evalExp(E1,EV) == errNat or evalExp(E2,EV) == errNat
       then errNat
       else (if evalExp(E1,EV) < evalExp(E2,EV) then 1 else 0 fi) fi .
  eq evalExp(E1 >> E2,EV)
     = if evalExp(E1,EV) == errNat or evalExp(E2,EV) == errNat
       then errNat
       else (if evalExp(E1,EV) > evalExp(E2,EV) then 1 else 0 fi) fi .
  eq evalExp(E1 && E2,EV)
     = if evalExp(E1,EV) == errNat or evalExp(E2,EV) == errNat
       then errNat
       else (if (evalExp(E1,EV) == 0) or (evalExp(E2,EV) == 0)
             then 0 else 1 fi ) fi .
  eq evalExp(E1 || E2,EV)
     = if evalExp(E1,EV) == errNat or evalExp(E2,EV) == errNat
       then errNat
       else (if (evalExp(E1,EV) == 0) and (evalExp(E2,EV) == 0)
             then 0 else 1 fi ) fi .
}

eof

open INTERPRETER
  op p1 : -> Stm .
  eq p1 = v(0) := 1 ;
          v(1) := 1 ;
          while v(1) << 10 || v(1) === 10 do
            v(0) := v(0) ** v(1) ;
            v(1) := v(1) ++ 1 ;
          od .

  op p2 : -> Stm .
  eq p2 = v(0) := 1 ;
          for v(1) 1 10 do
            v(0) := v(1) ** v(0) ;
          od .

  op p3 : -> Stm .
  eq p3 = v(0) := 24 ;
          v(1) := 30 ;
          while v(1) !== 0 do
            v(2) := v(0) %% v(1) ;
            v(0) := v(1) ;
            v(1) := v(2) ;
          od .

  op p4 : -> Stm .
  eq p4 = v(0) := 200000000 ;
          v(1) := 0 ;
          v(2) := v(0) ;
          while v(1) !== v(2) do
            if ((v(2) -- v(1)) %% 2) === 0
              then v(3) := v(1) ++ (v(2) -- v(1)) // 2 ;
              else v(3) := v(1) ++ ((v(2) -- v(1)) // 2) ++ 1 ; fi
            if v(3) ** v(3) >> v(0)
              then v(2) := v(3) -- 1 ;
              else v(1) := v(3) ; fi
          od .
          
  red interpret(p1) .
  red interpret(p2) .
  red interpret(p3) .
  red interpret(p4) .
close