diff --git a/Language.agda b/Language.agda index d6aa45c..d6f83f0 100644 --- a/Language.agda +++ b/Language.agda @@ -37,6 +37,7 @@ data BasicStmt : Set where _←_ : String → Expr → BasicStmt noop : BasicStmt +infixr 2 _then_ data Stmt : Set where ⟨_⟩ : BasicStmt → Stmt _then_ : Stmt → Stmt → Stmt diff --git a/Main.agda b/Main.agda index 176bd5f..09ad11d 100644 --- a/Main.agda +++ b/Main.agda @@ -6,18 +6,16 @@ open import Data.Vec using (Vec; _∷_; []) open import IO open import Level using (0ℓ) -testCode : Vec Stmt _ +testCode : Stmt testCode = - ("zero" ← (# 0)) ∷ - ("pos" ← ((` "zero") Expr.+ (# 1))) ∷ - ("neg" ← ((` "zero") Expr.- (# 1))) ∷ - ("unknown" ← ((` "pos") Expr.+ (` "neg"))) ∷ - [] + ⟨ "zero" ← (# 0) ⟩ then + ⟨ "pos" ← ((` "zero") Expr.+ (# 1)) ⟩ then + ⟨ "neg" ← ((` "zero") Expr.- (# 1)) ⟩ then + ⟨ "unknown" ← ((` "pos") Expr.+ (` "neg")) ⟩ testProgram : Program testProgram = record - { length = _ - ; stmts = testCode + { rootStmt = testCode } open WithProg testProgram using (output)