--
-- Abstract Syntax for Minila
--

--
-- Expressions
--
mod! EXP principal-sort Exp {
  pr(NAT)
  pr(VAR)
  [Nat Var < Exp]
  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 -> Exp {constr l-assoc prec: 30}
  op _--_ : Exp Exp -> Exp {constr l-assoc prec: 30}
  op _===_ : Exp Exp -> Exp {constr prec: 40}
  op _!==_ : Exp Exp -> Exp {constr prec: 40}
  op _<<_ : Exp Exp -> Exp {constr prec: 40}
  op _>>_ : Exp Exp -> Exp {constr prec: 40}
  op _&&_ : Exp Exp -> Exp {constr l-assoc prec: 50}
  op _||_ : Exp Exp -> Exp {constr l-assoc prec: 50}
}

--
-- Statements
--
mod! STM {
  pr(EXP)
  [Stm]
  op estm : -> Stm {constr}
  op _:=_; : Var Exp -> Stm {constr}
  op if_then_else_fi : Exp Stm Stm -> Stm {constr}
  op while_do_od : Exp Stm -> Stm {constr}
  op for_ _ _do_od : Var Exp Exp Stm -> Stm {constr}
  op _ _ : Stm Stm -> Stm {constr r-assoc prec: 45 id: estm}
}

eof

open STM
  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 .
  red p1 .

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

  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 .
  red p3 .  

  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 p4 .  
close