SilvIR: Example with Concrete Syntax

This post assumes you've read the definition of SilvIR, and is intended to be paired with its semantics. It's not a regular one in the series, and if you feel like you've fully understood everything so far, you can probably skip to the next post.

Note that this post is interactive, so enabling JavaScript is necessary for full functionality.

production arith:lit arith:Expr

production-body arith:lit[priority=0]
λ top ->
  let tmp = thunk { nil() } in
    top.arith:errors := tmp;
    top

production arith:var arith:Expr

production-body arith:var[priority=0]
λ top ->
  let errors = thunk {
                 let member = force(core:member) in
                 let nameIsBound = member(top.0, top.arith:boundVars) in
                 case nameIsBound of
                 true() -> nil()
                   false() ->
                     let tmp_nil = thunk { nil() } in
                     cons(undecorable strcat("Unbound variable ", top.0), decorable tmp_nil)
               } in
    top.arith:errors := errors;
    top

production arith:add arith:Expr

production-body arith:add[priority=0]
λ top ->
  let tmp = thunk { force(top.arith:boundVars) } in
    top.0.arith:boundVars := tmp;
    top

production-body arith:add[priority=0]
λ top ->
  let tmp = thunk { force(top.arith:boundVars) } in
    top.1.arith:boundVars := tmp;
    top

production-body arith:add[priority=0]
λ top ->
  let tmp = thunk {
              let append = force(core:append) in
              let thunk = append(top.0.arith:errors, top.1.arith:errors) in
              force(thunk)
            } in
    top.arith:errors := tmp;
    top

production arith:let arith:Expr

production-body arith:let[priority=0]
λ top ->
  let tmp = thunk { force(top.arith:boundVars) } in
    top.1.arith:boundVars := tmp;
    top

production-body arith:let[priority=0]
λ top ->
  let tmp = thunk {
              let topBoundVars = thunk { force(top.arith:boundVars) } in
              cons(undecorable top.0, decorable topBoundVars)
            } in
    top.2.arith:boundVars := tmp;
    top

production-body arith:let[priority=0]
λ top ->
  let tmp = thunk {
              let append = force(core:append) in
              let thunk = append(top.1.arith:errors, top.2.arith:errors) in
              force(thunk)
            } in
    top.arith:errors := tmp;
    top

core:append = λ (l, r) ->
let tmp = force(l) in
  case tmp of
  nil() -> r
    cons(h, t) ->
      thunk {
        let append = force(core:append) in
        let rest = append(t, r) in
        cons(undecorable h, decorable rest)
      }

core:member = λ (x, xs) ->
let tmp = force(xs) in
  case tmp of
  nil() -> false()
    cons(h, t) ->
      let eq = streq(x, h) in
      case eq of
      true() -> true()
        false() -> let member = force(core:member) in member(x, t)

arith:main = λ () ->
let tmp_l2 = arith:lit(undecorable 2) in
  let tmp_vx = arith:var(undecorable "x") in
  let tmp_vy = arith:var(undecorable "y") in
  let tmp_avxvy = arith:add(decorable tmp_vx, decorable tmp_vy) in
  let tmp_lyl2avxvy = arith:let(undecorable "y", decorable tmp_l2, decorable tmp_avxvy) in
  let tmp_vz = arith:var(undecorable "z") in
  let term = arith:add(decorable tmp_lyl2avxvy, decorable tmp_vz) in
  let tmp_nil = thunk { nil() } in
  let tree = decorate term with λ (top) -> top.arith:boundVars := tmp_nil; top in
  tree.arith:errors