A basic imperitive language in agda

basic.agda

open import Agda.Builtin.List
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.String

Num = ℕ

record Var : Set where
  constructor var
  field
    idx : ℕ

pattern $i = var 8
pattern $x = var 24
pattern $y = var 25
pattern $z = var 26

data Expr : Set where
  varexpr : Var → Expr
  numexpr : Num → Expr
  _plus_  : Expr → Expr → Expr
  _mul_   : Expr → Expr → Expr
  _mod_   : Expr → Expr → Expr

data Cond : Set where
  _equals_ : Expr → Expr → Cond
  negate   : Cond → Cond

data Stmt : Set where
  assign                 : Var → Expr → Stmt
  input                  : Var → Stmt
  output                 : Expr → Stmt
  litprint               : String → Stmt
  if_then_endif          : Cond → List Stmt → Stmt
  if_then_else_endif     : Cond → List Stmt → List Stmt → Stmt
  for_from_to_begin_next : Var → Expr → Expr → List Stmt → Stmt

pattern end = []

fizzbuzz  = input $x ∷
            for $i from numexpr 1 to varexpr $x begin
              if (varexpr $i mod numexpr 3) equals numexpr 0 then
                if (varexpr $i mod numexpr 5) equals numexpr 0 then
                  litprint "Fizzbuzz\n" ∷
                  end
                else
                  litprint "Fizz\n" ∷
                  end
                endif ∷
                end
              else
                if (varexpr $i mod numexpr 5) equals numexpr 0 then
                  litprint "Buzz\n" ∷
                  end
                else
                  output (varexpr $i) ∷
                  litprint "\n" ∷
                  end
                endif ∷
                end
              endif ∷
              end
            next ∷
            end