Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
A basic imperitive language in 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.