Re: [Toss-devel] Matching and Rewriting of Hierarchical Terms with Sharing

[Lukasz S. <luk...@gm...>]

Unlike in term rewriting, we often have more variables on the RHS than
in the LHS, since the variables are just a way to name new nodes.

*** Board example ***

I'll use numbers below. I'm in favor of having at least floating point
numbers as built-in, which if not eliminated by rewriting, are
translated into structures directly as structure function values.

I'll write it in some concrete syntax... parentheses are fully
optional ;-) but I'll use them for clarity, in the
functional-programming style.

First, we need a way to ignore terms, to use them for the
"side-effect" of constraining a variable. Let's also define the
parentheses. Sorry for not using the Speagram syntax, I like
succinctness.

x ';' y ISA y.
x; y => y.
'(' x ')' ISA x.
(x) => x.

Let's build the last row of a board:

'last-row' number ISA Node.
last-row 0 => x.
last-row n => R (last-row (n-1)).

Realize that "last-row 0 => x" is the same as "last-row 0 => Node",
because the variable "x" is inferred to be a "Node" -- being a
variable, it doesn't add any other constraint. Now let's stack more
rows in front:

'stack-row' Node ISA Node.
stack-row x@R y => z@C x; z@R (stack-row y).
stack-row x => C x.

The rule "stack-row x => C x" matches when the first rule doesn't
match, i.e. at the end of the row. Now let's do the loop:

'board' number number ISA Node.
board 0 n => last-row n.
board m n => stack-row (board (m-1) n).

Should I clarify anything? Perhaps I'll collect the definitions
together. Super-concise concrete syntax this time. In concrete syntax
the ISA part is after the argument part, while in the abstract syntax
I prefer to have it first...

Because the maximal sharing inside ISA part of definitions is
required, we can leave to the system to ensure it.

'Node'.
'R' Node ISA Node.
'C' Node ISA Node.
'Grid' ISA R Node AND C Node.
x ';' y ISA y.
x; y => y.
'(' x ')' ISA x.
(x) => x.
'last-row' number ISA Node.
last-row 0 => Node.
last-row n => R (last-row (n-1)).
'stack-row' Node ISA Node.
stack-row x@R y => z@C x; z@R (stack-row y).
stack-row x => C x.
'board' number number ISA Node.
board 0 n => last-row n.
board m n => stack-row (board (m-1) n).

Again, in a bit less terse, more Speagram syntax, only without "type"
/ "function". Also, without introducing variables before use.

Variables x, y, z.
New ''Node''.
New ''R'' Node as Node.
New ''C'' Node as Node.
New ''Grid'' as R Node and C Node.
New x '';'' y as y.
Let x; y be y.
New ''('' x '')'' as x.
Let (x) be x.
New ''last-row'' number as Node.
Let last-row 0 be Node.
Let last-row n be R (last-row (n-1)).
New ''stack-row'' Node as Node.
Let stack-row x@R y be z@C x; z@R (stack-row y).
Let stack-row x be C x.
New ''board'' number number as Node.
Let board 0 n be last-row n.
Let board m n be stack-row (board (m-1) n).

I assume above that variable bindings last only for one instruction.
Note that variables by themselves do not have "types", they just get
bound to ever more specific terms: explicitly by "@" and implicitly by
inference during parsing. E.g. in "last-row 0 => x" -- "Let last-row 0
be x." -- "x" is by parsing inference bound to new "Node".

Let's try how readable it is without parentheses:

Variables x, y, z.
New ''Node''.
New ''R'' Node as Node.
New ''C'' Node as Node.
New ''Grid'' as R Node and C Node.
New x '';'' y as y.
Let x; y be y.
New ''last-row'' number as Node.
Let last-row 0 be Node.
Let last-row n be R last-row n-1.
New ''stack-row'' Node as Node.
Let stack-row x@R y be z@C x; z@R stack-row y.
Let stack-row x be C x.
New ''board'' number number as Node.
Let board 0 n be last-row n.
Let board m n be stack-row board m-1 n.