DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Get everything compiling

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-04-13 14:13:44 -07:00
parent 44f04e4020
commit 8dc5c40eae
2 changed files with 7 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Language.agda
View File

@ -37,6 +37,7 @@ data BasicStmt : Set where
_←_ : String → Expr → BasicStmt _←_ : String → Expr → BasicStmt
noop : BasicStmt noop : BasicStmt
infixr 2 _then_
data Stmt : Set where data Stmt : Set where
⟨_⟩ : BasicStmt → Stmt ⟨_⟩ : BasicStmt → Stmt
_then_ : Stmt → Stmt → Stmt _then_ : Stmt → Stmt → Stmt

14
Main.agda
View File

@ -6,18 +6,16 @@ open import Data.Vec using (Vec; _∷_; [])
open import IO open import IO
open import Level using (0ℓ) open import Level using (0ℓ)
testCode : Vec Stmt _ testCode : Stmt
testCode = testCode =
("zero" ← (# 0)) ∷ ⟨ "zero" ← (# 0) ⟩ then
("pos" ← ((` "zero") Expr.+ (# 1))) ∷ ⟨ "pos" ← ((` "zero") Expr.+ (# 1)) ⟩ then
("neg" ← ((` "zero") Expr.- (# 1))) ∷ ⟨ "neg" ← ((` "zero") Expr.- (# 1)) ⟩ then
("unknown" ← ((` "pos") Expr.+ (` "neg"))) ∷ ⟨ "unknown" ← ((` "pos") Expr.+ (` "neg")) ⟩
[]
testProgram : Program testProgram : Program
testProgram = record testProgram = record
{ length = _ { rootStmt = testCode
; stmts = testCode
} }
open WithProg testProgram using (output) open WithProg testProgram using (output)