Skip to content

Commit

Permalink
[new-syntax] std/ -- rule use pattern matching
Browse files Browse the repository at this point in the history
  • Loading branch information
xieyuheng committed Sep 19, 2023
1 parent 660b8b3 commit 6e7e040
Show file tree
Hide file tree
Showing 4 changed files with 47 additions and 59 deletions.
8 changes: 2 additions & 6 deletions TODO.md
Original file line number Diff line number Diff line change
@@ -1,15 +1,11 @@
# new-syntax

[new-syntax] `std/` -- `rule` use pattern matching

[new-syntax] `Exp` -- `Block` has `body` and `ret`

- `return` is not a statement
- a block always has a `return` at the end
[new-syntax] `Exp` -- `Block` has `stmts: Array<BlockStmt>`

[new-syntax] `exp/block/BlockStmt`
[new-syntax] `exp/block/Let`
[new-syntax] `exp/block/Evaluate`
[new-syntax] `exp/block/Return`

[new-syntax] use `Exp` instead of `Word`

Expand Down
18 changes: 9 additions & 9 deletions std/datatype/DiffList.i
Original file line number Diff line number Diff line change
Expand Up @@ -25,18 +25,18 @@ node diffAppend(

node diffOpen(
target!: DiffList('A),
list: List('A)
newBack: List('A)
----------
result: List('A)
oldBack: List('A)
)
rule diff diffAppend {
let back, value = diff(^diff.front)
@connect(value, ^diffAppend.result)
diffOpen(^diffAppend.rest, back, ^diff.back)
rule diffAppend(target!, rest, result) diff(front, back, value!) {
let newBack, value = diff(front)
@connect(value, result)
diffOpen(rest, newBack, back)
}
rule diff diffOpen {
@connect(^diff.back, ^diffOpen.list)
@connect(^diff.front, ^diffOpen.result)
rule diffOpen(target!, newBack, oldBack) diff(front, back, value!) {
@connect(back, newBack)
@connect(front, oldBack)
}
12 changes: 4 additions & 8 deletions std/datatype/List.i
Original file line number Diff line number Diff line change
Expand Up @@ -19,14 +19,10 @@ node append(
result: List('A)
)
rule null append {
@connect(^append.rest, ^append.result)
rule append(target!, rest, result) null(value!) {
@connect(rest, result)
}
rule cons append {
cons(
^cons.head,
append(^cons.tail, ^append.rest),
^append.result
)
rule append(target!, rest, result) cons(head, tail, value!) {
cons(head, append(tail, rest), result)
}
68 changes: 32 additions & 36 deletions std/datatype/Nat.i
Original file line number Diff line number Diff line change
Expand Up @@ -18,17 +18,15 @@ node add(
result: Nat
)

rule zero(value!) add(target!, addend, result) {
rule add(target!, addend, result) zero(value!) {
@connect(addend, result)
}

rule add1 add {
// @connect(
// add1(add(^add1.prev, ^add.addend)),
// ^add.result,
// )
rule add(target!, addend, result) add1(prev, value!) {
add1(add(prev, addend), result)

add1(add(^add1.prev, ^add.addend), ^add.result)
// Same as:
// @connect(add1(add(prev, addend)), result)
}

function one(): Nat {
Expand All @@ -54,10 +52,10 @@ node natErase(
--------
)

rule zero natErase {}
rule natErase(target!) zero(value!) {}

rule add1 natErase {
natErase(^add1.prev)
rule natErase(target!) add1(prev, value!) {
natErase(prev)
}

node natDup(
Expand All @@ -67,18 +65,19 @@ node natDup(
first: Nat
)

rule zero natDup {
// @connect(zero(), ^natDup.first)
// @connect(zero(), ^natDup.second)
rule natDup(target!, second, first) zero(value!) {
zero(first)
zero(second)

zero(^natDup.first)
zero(^natDup.second)
// Same as:
// @connect(zero(), first)
// @connect(zero(), second)
}

rule add1 natDup {
let first, second = natDup(^add1.prev)
@connect(add1(first), ^natDup.first)
@connect(add1(second), ^natDup.second)
rule natDup(target!, second, first) add1(prev, value1) {
let prevFirst, prevSecond = natDup(prev)
@connect(add1(prevFirst), first)
@connect(add1(prevSecond), second)
}

node mul(
Expand All @@ -88,14 +87,14 @@ node mul(
result: Nat
)

rule zero mul {
natErase(^mul.mulend)
zero(^mul.result)
rule mul(target!, mulend, result) zero(value!) {
natErase(mulend)
zero(result)
}

rule add1 mul {
let first, second = natDup(^mul.mulend)
add(second, mul(first, ^add1.prev), ^mul.result)
rule mul(target!, mulend, result) add1(prev, value!) {
let first, second = natDup(mulend)
add(second, mul(first, prev), result)
}

// To define `max`, we need `maxAux`.
Expand All @@ -114,21 +113,18 @@ node max(
result: Nat
)

rule zero max {
@connect(^max.second, ^max.result)
rule max(first!, second, result) zero(value!) {
@connect(second, result)
}

rule add1 max {
maxAux(^add1.prev, ^max.second, ^max.result)
rule max(first!, second, result) add1(prev, value!) {
maxAux(prev, second, result)
}

rule zero maxAux {
add1(^maxAux.first, ^maxAux.result)
rule maxAux(first, second!, result) zero(value!) {
add1(first, result)
}

rule add1 maxAux {
add1(
max(^maxAux.first, ^add1.prev),
^maxAux.result
)
rule maxAux(first, second!, result) add1(prev, value!) {
add1(max(first, prev), result)
}

0 comments on commit 6e7e040

Please sign in to comment.