agda-spa/Main.agda

module Main where

open import Language
open import Analysis.Sign
open import Data.Vec using (Vec; _∷_; [])
open import IO
open import Level using (0ℓ)

testCode : Stmt
testCode =
    ⟨ "zero" ← (# 0) ⟩ then
    ⟨ "pos" ← ((` "zero") Expr.+ (# 1)) ⟩ then
    ⟨ "neg" ← ((` "zero") Expr.- (# 1)) ⟩ then
    ⟨ "unknown" ← ((` "pos") Expr.+ (` "neg")) ⟩

testProgram : Program
testProgram = record
    { rootStmt = testCode
    }

open WithProg testProgram using (output)

main = run {0ℓ} (putStrLn output)