diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..e1be9e0
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,51 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - master
+      - 'stage/**'
+  pull_request:
+    branches:
+      - master
+
+jobs:
+  build:
+    name: ${{ matrix.name || 'Build' }}
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: ${{ matrix.shell || 'sh' }}
+    strategy:
+      matrix:
+        include:
+        - name: Ubuntu
+          os: ubuntu-latest
+        - name: MacOS
+          os: macos-latest
+        - name: Windows
+          os: windows-latest
+          shell: bash {0}
+      # complete all jobs
+      fail-fast: false
+    steps:
+    - name: Install Elan
+      shell: bash -euo pipefail {0}
+      run: |
+        curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
+        echo "$HOME/.elan/bin" >> $GITHUB_PATH
+    - name: Checkout
+      uses: actions/checkout@v4
+    - name: Check Lean
+      run: lean --version
+    - name: Build
+      run: lake build
+    - name: Upload Build
+      continue-on-error: true
+      uses: actions/upload-artifact@v4
+      with:
+        name: ${{ matrix.os }}
+        path: .lake/build
+    - name: Test
+      run: lake run test
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..4c3f8ab
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,70 @@
+Apache License 2.0 (Apache)
+Apache License
+Version 2.0, January 2004
+http://www.apache.org/licenses/
+
+TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+1. Definitions.
+
+"License" shall mean the terms and conditions for use, reproduction, and distribution as defined by Sections 1 through 9 of this document.
+
+"Licensor" shall mean the copyright owner or entity authorized by the copyright owner that is granting the License.
+
+"Legal Entity" shall mean the union of the acting entity and all other entities that control, are controlled by, or are under common control with that entity. For the purposes of this definition, "control" means (i) the power, direct or indirect, to cause the direction or management of such entity, whether by contract or otherwise, or (ii) ownership of fifty percent (50%) or more of the outstanding shares, or (iii) beneficial ownership of such entity.
+
+"You" (or "Your") shall mean an individual or Legal Entity exercising permissions granted by this License.
+
+"Source" form shall mean the preferred form for making modifications, including but not limited to software source code, documentation source, and configuration files.
+
+"Object" form shall mean any form resulting from mechanical transformation or translation of a Source form, including but not limited to compiled object code, generated documentation, and conversions to other media types.
+
+"Work" shall mean the work of authorship, whether in Source or Object form, made available under the License, as indicated by a copyright notice that is included in or attached to the work (an example is provided in the Appendix below).
+
+"Derivative Works" shall mean any work, whether in Source or Object form, that is based on (or derived from) the Work and for which the editorial revisions, annotations, elaborations, or other modifications represent, as a whole, an original work of authorship. For the purposes of this License, Derivative Works shall not include works that remain separable from, or merely link (or bind by name) to the interfaces of, the Work and Derivative Works thereof.
+
+"Contribution" shall mean any work of authorship, including the original version of the Work and any modifications or additions to that Work or Derivative Works thereof, that is intentionally submitted to Licensor for inclusion in the Work by the copyright owner or by an individual or Legal Entity authorized to submit on behalf of the copyright owner. For the purposes of this definition, "submitted" means any form of electronic, verbal, or written communication sent to the Licensor or its representatives, including but not limited to communication on electronic mailing lists, source code control systems, and issue tracking systems that are managed by, or on behalf of, the Licensor for the purpose of discussing and improving the Work, but excluding communication that is conspicuously marked or otherwise designated in writing by the copyright owner as "Not a Contribution."
+
+"Contributor" shall mean Licensor and any individual or Legal Entity on behalf of whom a Contribution has been received by Licensor and subsequently incorporated within the Work.
+
+2. Grant of Copyright License.
+
+Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable copyright license to reproduce, prepare Derivative Works of, publicly display, publicly perform, sublicense, and distribute the Work and such Derivative Works in Source or Object form.
+
+3. Grant of Patent License.
+
+Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable (except as stated in this section) patent license to make, have made, use, offer to sell, sell, import, and otherwise transfer the Work, where such license applies only to those patent claims licensable by such Contributor that are necessarily infringed by their Contribution(s) alone or by combination of their Contribution(s) with the Work to which such Contribution(s) was submitted. If You institute patent litigation against any entity (including a cross-claim or counterclaim in a lawsuit) alleging that the Work or a Contribution incorporated within the Work constitutes direct or contributory patent infringement, then any patent licenses granted to You under this License for that Work shall terminate as of the date such litigation is filed.
+
+4. Redistribution.
+
+You may reproduce and distribute copies of the Work or Derivative Works thereof in any medium, with or without modifications, and in Source or Object form, provided that You meet the following conditions:
+
+1. You must give any other recipients of the Work or Derivative Works a copy of this License; and
+
+2. You must cause any modified files to carry prominent notices stating that You changed the files; and
+
+3. You must retain, in the Source form of any Derivative Works that You distribute, all copyright, patent, trademark, and attribution notices from the Source form of the Work, excluding those notices that do not pertain to any part of the Derivative Works; and
+
+4. If the Work includes a "NOTICE" text file as part of its distribution, then any Derivative Works that You distribute must include a readable copy of the attribution notices contained within such NOTICE file, excluding those notices that do not pertain to any part of the Derivative Works, in at least one of the following places: within a NOTICE text file distributed as part of the Derivative Works; within the Source form or documentation, if provided along with the Derivative Works; or, within a display generated by the Derivative Works, if and wherever such third-party notices normally appear. The contents of the NOTICE file are for informational purposes only and do not modify the License. You may add Your own attribution notices within Derivative Works that You distribute, alongside or as an addendum to the NOTICE text from the Work, provided that such additional attribution notices cannot be construed as modifying the License.
+
+You may add Your own copyright statement to Your modifications and may provide additional or different license terms and conditions for use, reproduction, or distribution of Your modifications, or for any such Derivative Works as a whole, provided Your use, reproduction, and distribution of the Work otherwise complies with the conditions stated in this License.
+
+5. Submission of Contributions.
+
+Unless You explicitly state otherwise, any Contribution intentionally submitted for inclusion in the Work by You to the Licensor shall be under the terms and conditions of this License, without any additional terms or conditions. Notwithstanding the above, nothing herein shall supersede or modify the terms of any separate license agreement you may have executed with Licensor regarding such Contributions.
+
+6. Trademarks.
+
+This License does not grant permission to use the trade names, trademarks, service marks, or product names of the Licensor, except as required for reasonable and customary use in describing the origin of the Work and reproducing the content of the NOTICE file.
+
+7. Disclaimer of Warranty.
+
+Unless required by applicable law or agreed to in writing, Licensor provides the Work (and each Contributor provides its Contributions) on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied, including, without limitation, any warranties or conditions of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A PARTICULAR PURPOSE. You are solely responsible for determining the appropriateness of using or redistributing the Work and assume any risks associated with Your exercise of permissions under this License.
+
+8. Limitation of Liability.
+
+In no event and under no legal theory, whether in tort (including negligence), contract, or otherwise, unless required by applicable law (such as deliberate and grossly negligent acts) or agreed to in writing, shall any Contributor be liable to You for damages, including any direct, indirect, special, incidental, or consequential damages of any character arising as a result of this License or out of the use or inability to use the Work (including but not limited to damages for loss of goodwill, work stoppage, computer failure or malfunction, or any and all other commercial damages or losses), even if such Contributor has been advised of the possibility of such damages.
+
+9. Accepting Warranty or Additional Liability.
+
+While redistributing the Work or Derivative Works thereof, You may choose to offer, and charge a fee for, acceptance of support, warranty, indemnity, or other liability obligations and/or rights consistent with this License. However, in accepting such obligations, You may act only on Your own behalf and on Your sole responsibility, not on behalf of any other Contributor, and only if You agree to indemnify, defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against, such Contributor by reason of your accepting any such warranty or additional liability.
diff --git a/Lyre.lean b/Lyre.lean
index e69de29..4d0e741 100644
--- a/Lyre.lean
+++ b/Lyre.lean
@@ -0,0 +1,6 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lyre.Commands
diff --git a/Lyre/Builder.lean b/Lyre/Builder.lean
new file mode 100644
index 0000000..0766ec6
--- /dev/null
+++ b/Lyre/Builder.lean
@@ -0,0 +1,417 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lyre.Grammar
+import Lean.Compiler.IR.Basic
+import Lean.Elab.Eval
+
+/-! # IR Builder
+
+Defines the `BuilderM` monad, which is used to convert IR syntax
+parsed from Lyre's IR Grammar into Lean IR objects.
+-/
+
+open Lean IR Elab
+
+namespace Lyre
+
+abbrev Ty := TSyntax `irType
+abbrev Expr := TSyntax `irExpr
+abbrev Stmt := TSyntax `irStmt
+abbrev Decl := TSyntax `irDecl
+
+abbrev Arg := TSyntax ``arg
+abbrev Param := TSyntax ``param
+abbrev CtorInfo := TSyntax ``ctorInfo
+abbrev CtorInfoIdx := TSyntax ``ctorInfoIdx
+abbrev Alt := TSyntax ``alt
+abbrev StmtSeq := TSyntax ``stmtSeq
+abbrev ExternEntry := TSyntax ``Parser.Attr.externEntry
+abbrev MDataVal := TSyntax ``mdataVal
+
+@[inline] def throwWithSyntax [Monad m] [MonadError m] (stx : Syntax) (caption : MessageData) (ref := stx) : m α :=
+  throwErrorAt ref m!"{caption}:{indentD stx}"
+
+@[inline] def throwIllFormedSyntax [Monad m] [MonadError m] (stx : Syntax) (kind := "syntax") : m α :=
+  throwWithSyntax stx m!"ill-formed {kind}"
+
+inductive Var
+| vdecl (id : VarId) (ty : IRType) (val : IR.Expr)
+| param (id : VarId) (ty : IRType)
+
+@[inline] def Var.mk (id : VarId) (ty : IRType) (val? : Option IR.Expr := none) : Var :=
+  match val? with
+  | some val => .vdecl id ty val
+  | none => .param id ty
+
+@[inline] def Var.id : Var → VarId
+| .vdecl id .. | .param id .. => id
+
+@[inline] def Var.ty : Var → IRType
+| .vdecl _ ty .. | .param _ ty .. => ty
+
+structure JoinPoint where
+  id : JoinPointId
+  params : Array IR.Param
+  body : FnBody
+  ty? : Option IRType := none
+
+structure BuilderScope where
+  joinPoints : NameMap JoinPoint := {}
+  vars : NameMap Var := {}
+
+structure BuilderContext where
+  parentScopes : Array BuilderScope := #[]
+
+structure BuilderState where
+  nextVarId : VarId := ⟨1⟩
+  nextJoinPointId : JoinPointId := ⟨1⟩
+  currScope : BuilderScope := {}
+
+abbrev BuilderM :=
+   ReaderT BuilderContext <| StateT BuilderState <| TermElabM
+
+@[inline] nonrec def BuilderM.run (x : BuilderM α) : TermElabM α :=
+  x.run {} |>.run' {}
+
+def withNewScope (x : BuilderM α) : BuilderM α := do
+  let oldScope ← modifyGet fun s => (s.currScope, {s with currScope := {}})
+  try
+    withReader (fun c => {c with parentScopes := c.parentScopes.push oldScope}) x
+  finally
+    modify ({· with currScope := oldScope})
+
+@[inline] def newJoinPoint (name : Name) (ps : Array IR.Param) (b : FnBody) (ty? : Option IRType := none) : BuilderM JoinPointId := modifyGet fun s =>
+  let jp := JoinPoint.mk s.nextJoinPointId ps b ty?
+  let scope := {s.currScope with joinPoints := s.currScope.joinPoints.insert name jp}
+  (jp.id, {s with nextJoinPointId := ⟨jp.id.idx + 1⟩, currScope := scope})
+
+@[inline] def getJoinPoint? (name : Name) : BuilderM (Option JoinPoint) := do
+  return (← get).currScope.joinPoints.find? name <|> (← read).parentScopes.findSome? (·.joinPoints.find? name)
+
+@[inline] def getJoinPoint (id : Ident) : BuilderM JoinPoint := do
+  match (← getJoinPoint? id.getId) with
+  | some j => return j
+  | none => throw <| .error id s!"unknown IR join point '{id.getId}'"
+
+@[inline] def getJoinPointId (id : Ident) : BuilderM JoinPointId := do
+  return (← getJoinPoint id).id
+
+@[inline] def newVar (name : Name) (ty : IRType) (val? : Option IR.Expr := none) : BuilderM VarId := modifyGet fun s =>
+  let v := Var.mk s.nextVarId ty val?
+  let scope := {s.currScope with vars := s.currScope.vars.insert name v}
+  (v.id, {s with nextVarId := ⟨v.id.idx + 1⟩, currScope := scope})
+
+@[inline] def getVar? (name : Name) : BuilderM (Option Var) := do
+  return (← get).currScope.vars.find? name <|> (← read).parentScopes.findSome? (·.vars.find? name)
+
+@[inline]  def getVar (id : Ident) : BuilderM Var := do
+  match (← getVar? id.getId) with
+  | some v => return v
+  | none => throw <| .error id s!"unknown IR variable '{id.getId}'"
+
+@[inline] def getVarId (id : Ident) : BuilderM VarId := do
+  return (← getVar id).id
+
+partial def mkType (ty : Ty) : BuilderM IRType :=
+  match ty with
+  | `(irType|float) => return .float
+  | `(irType|u8)    => return .uint8
+  | `(irType|u16)   => return .uint16
+  | `(irType|u32)   => return .uint32
+  | `(irType|u64)   => return .uint64
+  | `(irType|usize) => return .usize
+  | `(irType|◾)     => return .irrelevant
+  | `(irType|obj)   => return .object
+  | `(irType|tobj)  => return .tobject
+  | `(irType|struct $(id?)? {$tys,*}) =>
+    return .struct (id?.map (·.getId)) (← tys.getElems.mapM mkType)
+  | `(irType|union $(id?)? {$tys,*})  =>
+    return .union (id?.map (·.getId) |>.getD .anonymous) (← tys.getElems.mapM mkType)
+  | ty => throwIllFormedSyntax ty "IR type"
+
+def mkParam (stx : Lyre.Param) : BuilderM IR.Param := do
+  match stx with
+  | `(param|($id : $[@&%$b?]? $ty)) =>
+    let ty ← mkType ty
+    return {x := ← newVar id.getId ty, borrow := b?.isSome, ty}
+  | _ => throwIllFormedSyntax stx "IR parameter"
+
+def mkArg (stx : Lyre.Arg) : BuilderM IR.Arg := do
+  match stx with
+  | `(arg|◾) => return .irrelevant
+  | `(arg|$id:ident) => .var <$> getVarId id
+  | _ => throwIllFormedSyntax stx "IR argument"
+
+def mkArgAndType (stx : Lyre.Arg) : BuilderM (IR.Arg × IRType) := do
+  match stx with
+  | `(arg|◾) => return (.irrelevant, .irrelevant)
+  | `(arg|$id:ident) => let var ← getVar id; return (.var var.id, var.ty)
+  | _ => throwIllFormedSyntax stx "IR argument"
+
+def extractCIdx? (ctor : Ident) : Option Nat := do
+  let .str .anonymous c := ctor.getId | failure
+  unless c.startsWith "ctor_" do failure
+  c.drop 5 |>.toNat?
+
+def mkCtor (stx : Lyre.CtorInfo) (argStxs : Array Lyre.Arg) : BuilderM (IR.CtorInfo × Array IR.Arg) := do
+  let `(ctorInfo|$ctor$[.$usize?.$ssize?]?$[[$id?]]?) := stx
+    | throwIllFormedSyntax stx "IR constructor"
+  let name := id?.map (·.getId) |>.getD .anonymous
+  let some cidx := extractCIdx? ctor
+    | throw <| .error ctor s!"ill-formed IR constructor name '{ctor.getId}'"
+  if let some id := id? then
+    let name ← resolveGlobalConstNoOverloadWithInfo id
+    let some (.ctorInfo {cidx := ecidx, ..}) := (← getEnv).find? name
+      | throwWithSyntax (ref := id) stx m!"'{name}' is not a constructor"
+    if cidx != ecidx then
+      throwWithSyntax stx m!"constructor tag mismatch: constructor '{id.getId}' is expected to be 'ctor_{ecidx}'"
+  let args : Array IR.Arg := Array.mkEmpty argStxs.size
+  let info : IR.CtorInfo := {name, cidx, size := 0, usize := 0, ssize := 0}
+  let (args, info) ← argStxs.foldlM (init := (args, info)) fun (args, info) stx => do
+    match stx with
+    | `(arg|◾) => return (args.push .irrelevant, info)
+    | `(arg|$id:ident) =>
+      let var ← getVar id
+      let info :=
+        match var.ty with
+        | .uint8 => {info with usize := info.ssize+1}
+        | .uint16 => {info with usize := info.ssize+2}
+        | .uint32 => {info with usize := info.ssize+4}
+        | .float | .uint64 => {info with usize := info.ssize+8}
+        | .usize => {info with usize := info.usize+1}
+        | .object | .tobject => {info with size:= info.size+1}
+        | _ => info
+      return (args.push (.var var.id), info)
+    | _ => throwIllFormedSyntax stx "IR argument"
+  if let some usizeStx := usize? then
+    let usize := usizeStx.raw[0].isFieldIdx?.getD 0
+    if usize != info.usize then
+      let stx := Unhygienic.run `(ctor|$stx $argStxs*)
+      throwWithSyntax (ref := usizeStx) stx m!"constructor info mismatch: constructor has {info.usize} usize argument(s), but is expected to have {usize}"
+  if let some ssizeStx := ssize? then
+    let ssize := ssizeStx.raw[0].isFieldIdx?.getD 0
+    if ssize != info.ssize then
+      let stx := Unhygienic.run `(ctor|$stx $argStxs*)
+      throwWithSyntax (ref := ssizeStx) stx m!"constructor info mismatch: constructor has {info.ssize} bytes of scalar argument(s), but is expected to have {ssize}"
+  return (info, args)
+
+def mkExpr (stx : Lyre.Expr) : BuilderM (IR.Expr × Option IRType) := do
+  match stx with
+  | `(ctor|$i:ctorInfo $ys*) =>
+    let (info, args) ← mkCtor i ys
+    let ty := if info.size > 0 then .object else .uint8
+    return (.ctor info args, some ty)
+  | `(irExpr|reset[$n] $x) =>
+    return (.reset n.getNat (← getVarId x), some .object)
+  | `(irExpr|reuse $x in $i $ys*) =>
+    let (info, args) ← mkCtor i ys
+    return (.reuse (← getVarId x) info false args, some .object)
+  | `(irExpr|reuse! $x in $i $ys*) =>
+    let (info, args) ← mkCtor i ys
+    return (.reuse (← getVarId x) info true args, some .object)
+  | `(irExpr|proj[$i] $x) =>
+    return (.proj i.getNat (← getVarId x), some .object)
+  | `(irExpr|uproj[$i] $x) =>
+    return (.uproj i.getNat (← getVarId x), some .usize)
+  | `(irExpr|sproj[$n,$o] $x $[: $ty?]?) =>
+    return (.sproj n.getNat o.getNat (← getVarId x), ← ty?.mapM mkType)
+  | `(fap|$c:ident $ys*) =>
+    let some decl := IR.findEnvDecl (← getEnv) c.getId
+      | throw <| .error c s!"unknown IR constant '{c.getId}'"
+    try discard <| resolveGlobalConstNoOverloadWithInfo c catch _ => pure ()
+    let ty := match decl with
+      | .fdecl (type := ty) .. | .extern (type := ty) .. => ty
+    return (.fap c.getId (← ys.mapM mkArg), some ty)
+  | `(irExpr|pap $c $ys*) =>
+    return (.pap c.getId (← ys.mapM mkArg), some .object)
+  | `(irExpr|app $x $ys*) =>
+    return (.ap (← getVarId x) (← ys.mapM mkArg), none)
+  | `(irExpr|box $x) =>
+    let var ← getVar x
+    return (.box var.ty var.id, some .object)
+  | `(irExpr|unbox $x $[: $ty?]?) =>
+    return (.unbox (← getVarId x), ← ty?.mapM mkType)
+  | `(irExpr|$n:num $[: $ty?]?) =>
+    return (.lit <| .num n.getNat, ← ty?.mapM mkType)
+  | `(irExpr|$s:str) =>
+    return (.lit <| .str s.getString, some .object)
+  | `(irExpr|isShared $x) =>
+    return (.isShared (← getVarId x), some .uint8)
+  | _ =>
+    throwIllFormedSyntax stx "IR expression"
+
+def expectType? (name : Name) (inferred? : Option IRType) (expected? : Option Ty) : BuilderM (Option IRType) := do
+  let some ty := expected? | return inferred?
+  let ety ← mkType ty
+  let some ity := inferred? | return some ety
+  unless ity == ety do
+    throw <| .error ty m!"type mismatch: '{name}' has type '{ity}' but is expected to have type '{ty}'"
+  return some ety
+
+@[implemented_by Term.evalTerm]
+opaque evalTerm (α) (type : Lean.Expr) (value : Syntax) (safety := DefinitionSafety.safe) : TermElabM α
+
+def elabMDataVal (stx: MDataVal) : BuilderM IR.MData := do
+  match stx with
+  | `(mdataVal|$ $val) => evalTerm KVMap (mkConst ``KVMap) val
+  | `(mdataVal|[$kvps,*]) => kvps.getElems.foldlM (init := KVMap.empty) fun m kv => do
+    let `(kvpair|$key := $val) := kv
+      | throwIllFormedSyntax stx "metadata key-value pair"
+    return m.insert key.getId (← evalTerm DataValue (mkConst ``DataValue) val)
+  | _ => throwIllFormedSyntax stx "metadata value"
+
+section end
+
+mutual
+
+partial def initStmtIds (stx : Stmt) : BuilderM Unit := do
+  match stx with
+  | `(irStmt|let $x $[: $ty?]? := $e) =>
+    let (val, ity?) ← mkExpr e
+    let some ty ← expectType? x.getId ity? ty?
+      | throw <| .error x s!"cannot infer type for '{x.getId}'"
+    discard <| newVar x.getId ty val
+  | `(irStmt|$j:ident $ps* $[: $ty?]? := $stmts*) =>
+    let (ps, body, ty?) ← withNewScope do
+      let ps ← ps.mapM mkParam
+      let (body, bty?) ← mkFnBody stmts
+      let ty? ← expectType? j.getId bty? ty?
+      return (ps, body, ty?)
+    discard <| newJoinPoint j.getId ps body ty?
+  | _ => pure ()
+
+
+partial def mkAlt (stx : Lyre.Alt) : BuilderM (IR.Alt × Option IRType) := do
+  match stx with
+  | `(alt|$id:ident → $stmts*) =>
+    -- NOTE: We dummy out the sizes in the ctor here
+    -- because they are not used by the core emitters
+    -- and we do not have the relevant information.
+    let some (.ctorInfo {cidx, ..}) := (← getEnv).find? id.getId
+      | throw <| .error id s!"unknown constructor '{id.getId}'"
+    let info := {name := id.getId, cidx, size := 0, usize := 0, ssize := 0}
+    let (body, ty?) ← mkFnBody stmts
+    return (.ctor info body, ty?)
+  | `(alt|default → $stmts*) =>
+    let (body, ty?) ← mkFnBody stmts
+    return (.default body, ty?)
+  | _ => throwIllFormedSyntax stx "IR case alternative"
+
+partial def mkAlts (stxs : Array Lyre.Alt) : BuilderM (Array IR.Alt × Option IRType) := do
+  stxs.foldlM (init := (Array.mkEmpty stxs.size, none)) fun (alts, ty?) stx => do
+    let (alt, aty?) ← mkAlt stx
+    let ty? ← id do
+      let some ty := ty? | return aty?
+      let some aty := aty? | return ty?
+      unless aty == ty do
+        throw <| .error stx m!"type mismatch:{indentD stx}\nhas type '{aty}' but is expected to have type '{ty}'"
+      return some ty
+    return (alts.push alt, ty?)
+
+-- Precondition: top-level Var/JoinPoint ids are already declared
+partial def mkControlStmt (stx : Stmt) : BuilderM (FnBody × Option IRType) := do
+  match stx with
+  | `(irStmt|case $[[$tid?]]? $x $[: $ty?]? of $cs*) =>
+    let var ← getVar x
+    if let some ty := ty? then
+      let ety ← mkType ty
+      unless ety == var.ty do
+        throw <| .error ty m!"type mismatch: '{x.getId}' has type '{var.ty}' but is expected to have type '{ety}'"
+    let tid := tid?.map (·.getId) |>.getD .anonymous
+    let (alts, ty?) ← mkAlts cs
+    return (.case tid var.id var.ty alts, ty?)
+  | `(irStmt|jmp%$tk $j $ys*) =>
+    let jp ← getJoinPoint j
+    if ys.size != jp.params.size then
+      throwWithSyntax (ref := tk) stx m!"incorrect number of arguments: '{j.getId}' has {jp.params.size} parameter(s), but {ys.size} argument(s) were provided"
+    let args ← (jp.params.zip ys).mapM fun (param, argStx) => do
+      let (arg, ty) ← mkArgAndType argStx
+      unless ty == param.ty do
+        throwWithSyntax (ref := argStx) stx m!"type mismatch: '{argStx}' has type '{ty}' but is expected to have type '{param.ty}'"
+      return arg
+    return (.jmp jp.id args, jp.ty?)
+  | `(irStmt|ret $x) =>
+    let (id, ty) ← mkArgAndType x
+    return (.ret id, some ty)
+  | `(irStmt|⊥) =>
+    return (.unreachable, none)
+  | _ => throwWithSyntax stx m!"invalid terminal statement"
+
+-- Precondition: top-level Var/JoinPoint ids are already declared
+partial def prependStmt (stx : Stmt) (b : FnBody) : BuilderM FnBody := do
+  match stx with
+  | `(irStmt|let $x $[: $_]? := $_) =>
+    let some (.vdecl x ty e) ← getVar? x.getId
+      | throw <| .error x s!"(internal) variable '{x.getId}' not pre-declared"
+    return .vdecl x ty e b
+  | `(irStmt|$j:ident $_* $[: $_]? := $_*) =>
+    let some j ← getJoinPoint? j.getId
+      | throw <| .error j s!"(internal) join point '{j.getId}' not pre-declared"
+    return .jdecl j.id j.params j.body b
+  | `(irStmt|set $x[$i] := $y) =>
+    return .set (← getVarId x) i.getNat (← mkArg y) b
+  | `(irStmt|uset $x[$i] := $y) =>
+    return .uset (← getVarId x) i.getNat (← getVarId y) b
+  | `(irStmt|sset $x[$i,$o] : $ty := $y) =>
+    return .sset (← getVarId x) i.getNat o.getNat (← getVarId y) (← mkType ty) b
+  | `(irStmt|setTag $x:ident := $cidx) =>
+    return .setTag (← getVarId x) cidx.getNat b
+  | `(irStmt|inc $[persistent%$p?]? $[ref%$r?]? $[[$n?]]? $x) =>
+    let n := n?.map (·.getNat) |>.getD 1
+    return .inc (← getVarId x) n r?.isNone p?.isSome b
+  | `(irStmt|dec $[persistent%$p?]? $[ref%$r?]? $[[$n?]]? $x) =>
+    let n := n?.map (·.getNat) |>.getD 1
+    return .dec (← getVarId x) n r?.isNone p?.isSome b
+  | `(irStmt|del $x) =>
+    return .del (← getVarId x) b
+  | `(irStmt|mdata $d) =>
+    return .mdata (← elabMDataVal d) b
+  | `(irStmt|case $[[$_]]? $_ $[: $_]? of $_*) | `(irStmt|jmp $_ $_*) | `(irStmt|ret $_) | `(irStmt|⊥) =>
+    throwWithSyntax stx m!"control statement must be the last statement in a function body"
+  | _ => throwIllFormedSyntax stx "IR statement"
+
+partial def mkFnBody (stmts : Array Stmt) : BuilderM (FnBody × Option IRType) := do
+  stmts.forM initStmtIds
+  let (stmt, ty?) ← mkControlStmt stmts.back
+  let body ← stmts.foldrM prependStmt stmt (start := stmts.size - 1)
+  return (body, ty?)
+
+end
+
+open Lean.Parser.Attr in
+def mkExternEntries (entriesStx : Array Lyre.ExternEntry) : BuilderM (List Lean.ExternEntry) := do
+  if entriesStx.size == 0 then
+    return [ .adhoc `all ]
+  let entries ← entriesStx.foldrM (init := []) fun stx entries => do
+    match stx with
+    | `(externEntry|$[$backend?]? $[inline%$inline?]? $str) =>
+      let backend := backend?.map (·.getId) |>.getD `all
+      let entry :=
+        if inline?.isSome then
+          .inline backend str.getString
+        else
+          .standard backend str.getString
+      return entry :: entries
+    | _ => throwIllFormedSyntax stx "extern entry"
+  return entries
+
+def mkDecl (stx : Lyre.Decl) : BuilderM IR.Decl := do
+  match stx with
+  | `(irDecl|$[@$sorryDep?]? def $did $ps* $[: $ty?]? := $stmts*) =>
+    let ps ← ps.mapM mkParam
+    let (body, bty?) ← mkFnBody stmts
+    let some ty ← expectType? did.getId bty? ty?
+      | throw <| .error did s!"cannot infer type for '{did.getId}'"
+    let sorryDep? := sorryDep?.map (·.getId)
+    return .fdecl did.getId ps ty body {sorryDep?}
+  | `(irDecl|extern $did $ps* : $ty $[:= $entries?*]?) =>
+    let data ← id do
+      if let some entries := entries? then
+        return {entries := ← mkExternEntries entries}
+      else
+        return getExternAttrData? (← getEnv) did.getId |>.getD {entries := []}
+    return .extern did.getId (← ps.mapM mkParam) (← mkType ty) data
+  | _ => throwIllFormedSyntax stx "IR declaration"
diff --git a/Lyre/Commands.lean b/Lyre/Commands.lean
new file mode 100644
index 0000000..2e27ba9
--- /dev/null
+++ b/Lyre/Commands.lean
@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lyre.Builder
+import Lean.Compiler.IR
+
+open Lean IR Elab Command
+
+namespace Lyre
+
+/--
+Directly set the Lean IR for a the definition `name`.
+The definition most not already have IR. This can be accomplish, e.g.,
+by marked the definition `noncumptable` when declared.
+-/
+def setAdhoc [Monad m] [MonadEnv m] [MonadError m]
+  (name : Name) (ps : Array IR.Param) (ty : IRType) (body : FnBody) (info : DeclInfo)
+: m Unit := do
+  let env ← getEnv
+  if env.getModuleIdxFor? name |>.isSome then
+    throwError "declaration is in an imported module"
+  if IR.findEnvDecl env name |>.isSome then
+    throwError "declaration already has an implementation"
+  /-
+  The `extern` attribute only supports `afterSet` on constructors
+  and projections, so we manually extend this to normal definitions
+  lacking an implementation (i.e., `noncomputable` definitions)
+  -/
+  let env := externAttr.ext.modifyState env fun s =>
+    s.insert name {entries := [.adhoc `all]}
+  let decl := .fdecl name ps ty body info
+  let env := IR.declMapExt.addEntry env decl
+  match IR.addBoxedVersion env decl with
+  | .ok env => setEnv env
+  | .error e => throwError s!"(compiler) {e}"
+
+/--
+Implement a definition directly with raw Lean IR.
+The definition most not already have IR. This can be accomplish, e.g.,
+by marked the definition `noncumptable` when declared.
+
+**Example**
+
+```
+noncomputable def myAdd (m n : Nat) : Nat :=
+  m + n
+
+ir_impl myAdd (m : @& obj) (n : @& obj) :=
+  let x := Nat.add m n
+  ret x
+
+#eval myAdd 1 2 -- 3
+```
+-/
+scoped syntax "ir_impl " ident param* (" : " irType)? " := " stmtSeq : command
+
+elab_rules : command | `(ir_impl $id $ps* $[: $ty?]? := $stmts*) => do
+  let name ← resolveGlobalConstNoOverloadWithInfo id
+  let (ps, ty, body) ← liftTermElabM <| BuilderM.run do
+    let ps ← ps.mapM mkParam
+    let (body, bty?) ← mkFnBody stmts
+    let some ty ← expectType? id.getId bty? ty?
+      | throw <| .error id s!"cannot infer type for '{id.getId}'"
+    return (ps, ty, body)
+  setAdhoc name ps ty body {}
diff --git a/Lyre/Grammar.lean b/Lyre/Grammar.lean
new file mode 100644
index 0000000..f868532
--- /dev/null
+++ b/Lyre/Grammar.lean
@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lean.Parser.Attr
+import Lyre.Util.Grammar
+
+/-! # IR Grammar
+
+Syntax definitions which encode Lyre's IR Grammar.
+The goal is to closely mirror the syntax printed by `toString`
+on an Lean IR object (e.g., `Lean.IR.Decl`).
+-/
+
+namespace Lyre
+
+/-! ## Constructors -/
+
+section
+open Lean Parser
+def checkCtor :=
+  checkStackTop (msg := "expected 'ctor_{n}'") fun stx =>
+    match stx with
+    | .ident _ rawVal _ _ => rawVal.toString.startsWith "ctor_"
+    | _ => stx.isAntiquot
+
+def ctorInfoIdx := leading_parser
+  fieldIdx <|> rawCh '0'
+
+syntax ctorInfo :=
+  ident checkCtor
+  (noWs "." noWs ctorInfoIdx noWs "." noWs ctorInfoIdx)?
+  ("[" ident "]")?
+end
+
+/-! ## Types -/
+
+declare_syntax_cat irType (behavior := symbol)
+
+syntax float : irType := &"float"
+syntax uint8 : irType := &"u8"
+syntax uint16 : irType := &"u16"
+syntax uint32 : irType := &"u32"
+syntax uint64 : irType := &"u64"
+syntax usize : irType := &"usize"
+syntax irrelevant : irType := "◾"
+syntax object : irType := &"obj"
+syntax tobject : irType := &"tobj"
+syntax struct : irType := &"struct " (ident)? "{" ppGroup(ppIndent((irType,*))) "}"
+syntax union : irType := &"union " (ident)? "{" ppGroup(ppIndent((irType,*))) "}"
+
+/-- ## Expressions -/
+
+declare_syntax_cat irExpr (behavior := symbol)
+
+syntax param := "(" ident  " : " "@& "? irType ")"
+syntax arg := ident <|> "◾"
+
+syntax ctor : irExpr := ctorInfo (colGt ppSpace arg)*
+syntax reset : irExpr := &"reset" "[" num "] " ident
+syntax reuse : irExpr :=
+  (&"reuse" <|> &"reuse!"?) ppSpace ident " in " ctorInfo (colGt ppSpace arg)*
+syntax proj : irExpr := &"proj" "[" num "] " ident
+syntax uproj : irExpr := &"uproj" "[" num "] " ident
+syntax sproj : irExpr := &"sproj" "[" num ", " num "] " ident (" : " irType)?
+syntax fap : irExpr := ident (colGt arg)*
+syntax pap : irExpr := &"pap " ident (colGt ppSpace arg)*
+syntax ap : irExpr := &"app " ident (colGt ppSpace arg)*
+syntax box : irExpr := &"box " ident
+syntax unbox : irExpr := &"unbox " ident (" : " irType)?
+syntax isShared : irExpr := &"isShared " ident
+
+syntax strLit : irExpr := str
+syntax numLit : irExpr := num (":" irType)?
+
+/-! ## Statements -/
+
+declare_syntax_cat irStmt (behavior := symbol)
+syntax stmtSeq := sepBy1IndentSemicolon(irStmt)
+
+syntax endSemi := ";"?
+syntax ctorAlt := ident " →" ppIndent(stmtSeq)
+syntax defaultAlt := &"default" " →" ppIndent(stmtSeq)
+syntax alt := ctorAlt <|> defaultAlt
+
+syntax kvpair := ident " := " term
+syntax mdataVal := ("$" term:max) <|> ("[" kvpair,* "]")
+
+syntax vdecl : irStmt := "let " ident (" : " irType)? " := " irExpr
+syntax jdecl : irStmt := ident param* (" : " irType)? " :=" ppIndent(stmtSeq)
+syntax set : irStmt := &"set " ident "[" num "] := " arg
+syntax uset : irStmt := &"uset " ident "[" num "] := " ident
+syntax sset : irStmt :=
+  &"sset " ident "[" num ", " num "]" " : " irType " := " ident
+syntax setTag : irStmt := &"setTag " ident " := " num
+syntax inc : irStmt := &"inc" &"persistent"? &"ref"? ("[" num "]")? ident
+syntax dec : irStmt := &"dec" &"persistent"? &"ref"? ("[" num "]")? ident
+syntax del : irStmt := &"del " ident
+syntax mdata : irStmt := &"mdata " mdataVal
+syntax case : irStmt :=
+  &"case " ("[" ident "]")? ident (" : " irType)?  &" of" many1Indent(ppLine alt)
+syntax jmp : irStmt := &"jmp " ident (colGt ppSpace arg)*
+syntax ret : irStmt := &"ret " arg
+syntax unreachable : irStmt := "⊥"
+
+/-! ## Declarations -/
+
+declare_syntax_cat irDecl (behavior := symbol)
+
+syntax funDecl : irDecl := ("@" ident ppLine)?
+  "def " ident param* (" : " irType)? " :=" ppIndent(stmtSeq)
+
+open Lean.Parser.Attr in
+syntax externDecl : irDecl :=
+  &"extern " ident param* " : " irType
+  (" := " (ppSpace externEntry)+)?
diff --git a/Lyre/Util/Grammar.lean b/Lyre/Util/Grammar.lean
new file mode 100644
index 0000000..eabdf77
--- /dev/null
+++ b/Lyre/Util/Grammar.lean
@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lean.Elab.ElabRules
+
+namespace Lyre
+
+open Lean Elab Command in
+/--
+Defines a piece of syntax with a antiquote kind and adds it to a category.
+For example, `syntax foo : term := "foo"` is syntactic sugar for:
+
+```
+syntax foo := "foo"
+attribute [term_parser] foo
+```
+-/
+scoped elab (name := syntaxCatAbbrev) doc?:(docComment)?
+"syntax " id:ident " : " cat:ident " := " xs:stx* : command => do
+  let catName := cat.getId
+  unless (Parser.isParserCategory (← getEnv) catName) do
+    throwErrorAt cat "unknown category '{catName}'"
+  liftTermElabM <| Term.addCategoryInfo cat catName
+  let attr := mkIdentFrom cat (catName.appendAfter "_parser")
+  let cmd ← `($[$doc?]? syntax $id := $[$xs]*)
+  withMacroExpansion (← getRef) cmd <| elabCommand cmd
+  let name ← resolveGlobalConstNoOverload id
+  unless (← getEnv).contains name do
+    return -- skip the attribute if the declaration errored
+  let cmd ← `(attribute [$attr:ident] $id)
+  withMacroExpansion (← getRef) cmd <| elabCommand cmd
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..0415787
--- /dev/null
+++ b/README.md
@@ -0,0 +1,16 @@
+# Lyre
+
+A library for writing Lean IR as Lean syntax.
+
+**Example**
+
+```lean
+noncomputable def myAdd (m n : Nat) : Nat :=
+  m + n
+
+ir_impl myAdd (m : @& obj) (n : @& obj) :=
+  let x := Nat.add m n
+  ret x
+
+#eval myAdd 1 2 -- 3
+```
diff --git a/lakefile.lean b/lakefile.lean
index b7fa147..c33539d 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,4 +2,19 @@ import Lake
 open Lake DSL
 
 package lyre
+
+@[default_target]
 lean_lib Lyre
+
+def runLean (file : FilePath) : ScriptM PUnit := do
+  let exitCode ← IO.Process.spawn {
+    cmd := (← getLean).toString,
+    args := #[file.toString],
+    env := ← getAugmentedEnv
+  } >>= (·.wait)
+  if exitCode ≠ 0 then
+    IO.Process.exit exitCode.toUInt8
+
+script test do
+  runLean <| "tests" / "basic.lean"
+  return 0
diff --git a/tests/basic.lean b/tests/basic.lean
new file mode 100644
index 0000000..feca79e
--- /dev/null
+++ b/tests/basic.lean
@@ -0,0 +1,11 @@
+import Lyre
+open scoped Lyre
+
+noncomputable def myAdd (m n : Nat) : Nat :=
+  m + n
+
+ir_impl myAdd (m : @& obj) (n : @& obj) :=
+  let x := Nat.add m n
+  ret x
+
+#eval myAdd 1 2