A SiLCC program is an LCC agent. The fundamental syntactic constructions are listed below. All the other constructions (expect the foreign function interface) are just convenient notations for usual programming idioms and can be rewritten with these fundamental constructions.
Terms are constructed with variables and domain symbols: the domain includes integers, floating-point values, character strings (double-quoted) and other structures that we will detail later on.
A theoretical description of the semantics for these fundamental constructions is given in [HFS07]. Tells add tokens to the store. Asks wait that some tokens are simultaneously present in the store for removing them and executing the ask body. Transient asks are fired only once, persistent asks are fired as many times as there are matching tokens to remove. The term which precedes the dot before a token identifier is called the module of the token.
Lexical conventions.
Blank characters (spaces, tabulations, line feeds . . .) are not distinguished
and can be repeated.
However, the top-level evaluates the phrase as soon as it is well-formed:
therefore inserting line feeds may change the top-level behaviour (e.g.,
a parallel composition becomes two different phrases).
Inside a token, there should not be any space between the predicate and
the opening parenthesis introducing its arguments.
Parentheses are mandatory, even for tokens with zero argument.
Identifiers for predicates and variables should begin by a letter
or an underscore and can contain any combination of letters, digits,
_
,
'
and -
.
Numbers are written in decimal by default, and they can be prefixed by
0x, 0o or
0b for hexadecimal, octal or binary respectively.
Floating-point values are denoted with a dot between the integer part and the
fractional part.
Scientific notation using e followed by an exponent
is supported for all numbers.
Comments are either between // and the end of the line,
or between /* and */ for
free form texts (not nestable),
or between (* and *) for
nestable comments (should respect some lexical conventions, like balanced quoting:
ideal to comment code).
The compiler assumes that the source is UTF-8 encoded and fails if the document
is ill-formed.
Variables are bound with the quantifiers forall and exists with the obvious scope. Other variables are free and denote values defined in other files. Typically, the standard library provides values for interacting with the real world. For example, a term can be printed to standard output by telling the token writeln() with the module variable io.std (yes, free variables can have dots in their name, these dots reflect the package structure). The token writeln() takes two arguments. The first argument is the term to print. The second argument is a continuation, more about this latter. To print "Hello world!", we just need to tell such a token, and say that there exists a continuation without worrying more about it.
exists k (io.std.writeln("Hello world!", k))
Remark.
When an existentially quantified variable is only needed once,
we can simply note it _
.
The previous example is therefore equivalent to the code below.
io.std.writeln("Hello world!", _)
Since they can be fired several times, persistent asks are typically useful to define procedures, as in the following example (note that string concatenation is just obtained by putting strings one after the others).
exists m (
forall s (
m.hello(s)
=>
io.std.writeln("Hello " s "!", _)
)
m.hello("You")
m.hello("Me")
)
There is a convenient notation for persistent asks on single head when all the variables appearing in the arguments of the head are universally quantified (typically, procedure definitions): just write the head followed by the body of the agent surrounded by curly brackets.
exists m (
m.hello(s) {
io.std.writeln("Hello " s "!", _)
}
m.hello("You")
m.hello("Me")
)
Remark. When a variable is existentially quantified up to the next closing delimiter (if any, the end of the file otherwise), the quantification may be followed just by a comma and parentheses omitted. The previous example is therefore equivalent to the code below.
exists m,
m.hello(s) {
io.std.writeln("Hello " s "!", _)
}
m.hello("You")
m.hello("Me")
When agents are put in parallel, as hello("You") and hello("Me") in the previous example, there is no guarantee that the first is executed before or after the second or, worse, that the two executions are not interleaved. To sequence printings, we should use a variable, say k, passed to the continuation argument of writeln("...", k): a token k.done() is told when the printing is finished, allowing us to consume it before pursuing with other printings. Note that forall can be omitted in asks when there is no variable to quantify on.
exists k,
io.std.writeln("One", k)
(
k.done()
->
exists k',
io.std.writeln("Two", k')
(
k'.done()
->
io.std.writeln("Three", _)
)
)
The notation do { ... } allows sequences to be written more conveniently. The previous example is equivalent to the code below.
do {
io.std.writeln("One")
io.std.writeln("Two")
io.std.writeln("Three")
}
Elements in sequences may use tokens of the form value(x) instead of done() to return values. These values are bound with <- notation.
exists m,
forall k (
m.a(k)
=>
k.value(1)
)
do {
x <- m.a()
io.std.writeln(x)
}
Remark. This example is expanded to the following code.
exists m, forall k ( m.a(k) => k.value(1) ) exists k, m.a(k) forall x (k.value(x) -> io.std.writeln(x, _))
We can do some arithmetic by using the standard library module data.arith. The following code prints the product of 123 by 45. Note that io.std.writeln waits that v gets a value before printing it.
exists v, data.arith.mul(123, 45, v) io.std.writeln(v, _)
The functional notations allows such code to be written more elegantly without having to give a name to the intermediary variable: when a token is written in term position, the token is moved and put in parallel with the rest of the agent, a fresh variable is added as its last argument, and the term where the token was is replaced by this variable. The previous example is equivalent to the code below.
io.std.writeln(data.arith.mul(123, 45), _)
Moreover, we can write x * y instead of data.arith.mul(x, y), and, more generally, the operators +, -, *, /, ^, mod are available as usual notations for arithmetic.
The function definition notation defines procedures with an implicit last argument conventionally called result.
exists m,
function m.square(x) {
result = x * x
}
io.std.writeln(m.square(12), _)
When the body of the function is reduced to assign a value to result, we may use the alternative notation function f(...) = value.
exists m, function m.square(x) = x * x io.std.writeln(m.square(12), _)
data.arith defines arithmetic comparisons as well. The result of a comparison is represented with a module for either a token true() or a token false().
exists m,
m.check(22)
m.check(n) {
exists k,
data.arith.le(n, 10, k)
(
k.true()
=>
io.std.writeln(n.string() " is a number less than or equal to 10.", _)
)
(
k.false()
=>
io.std.writeln(n.string() " is a number greater than 10.", _)
)
}
Note that all domain values can be converted to character strings by
telling a string() token in their module.
The idiom of the pair of asks on true() and false() on the same module can be written more usually as follows. (Note that x <= y is a notation for data.arith.le(x, y), usual notations for other comparisons are available as well.)
exists m,
m.check(22)
m.check(n) {
if n <= 10 do {
io.std.writeln(n.string() " is a number less than or equal to 10.")
}
else do {
io.std.writeln(n.string() " is a number greater than 10.")
}
}
Executing an agent can be non-deterministic. Typically, suppose that two asks wait for the same token: when this token is told, there are two possible computations whether the first or the second ask is fired. SiLCC has been designed such that all observable computations are effectively observed. Hence, if each of these two asks leads to an observable behavior (so as to say a side-effect, like printing something), both behaviors will be observed.
exists m,
m.token()
m.token() {
io.std.writeln("First branch.", _)
}
m.token() {
io.std.writeln("Second branch.", _)
}
However, these two branches are two distinct paths in the non-deterministic computation produced by the agent. In particular, they cannot share resources.
exists m,
m.token()
m.token() {
io.std.writeln("First branch.", _)
m.resource1()
}
m.token() {
io.std.writeln("Second branch.", _)
m.resource2()
}
(m.resource1() m.resource2() -> io.std.writeln("Will not be executed!", _))
In the previous example, the third ask can only be fired if there exists a computation path where both resource1 and resource2 are simultaneously available, yet each of these resources is produced by a distinct computation path.
The essential consequence of angelism is the decomposability of asks. For example, forall x (a(x) a(x + 1) a(x + 2) => ...) is equivalent to forall x (a(x) => a(x + 1) -> a(x + 2) -> ...): since the second agent suspends if one of the three tokens to be consumed is not available, and since there is no side-effects between the three nested asks, the possible partial consumption is just not observed. More generally, every program is rewritten to a kernel language which is indeed limited to asks on single tokens where all arguments are universally quantified. All other forms of asks are decomposed: for example, forall (a(x, x + 1) -> ...) is decomposed in forall x y (a(x, y) -> if y = x + 1 { ... }).
There is always a current
module, which tokens not prefixed with a dot
belong to.
This module can always be referred by the keyword this.
The notation with locally changes the current module.
with io.std do {
write("10 + 2 = ")
write(10 + 2)
writeln("")
}
The notation module { ... } is an expression returning a fresh module. This module is the current module of the agent written between the curly brackets.
exists m,
m.operate(a, op, b, f) {
with io.std do {
write(a.string() " " op " " b.string() " = ")
write(f.get(a, b))
writeln("")
}
}
m.operate(12, "*", 5, module { function get(a, b) = a * b })
The agent defined in the file x.lcc is read with the free variable x as current module. When the free variable x is used, the file x.lcc is loaded.
If the file example.lcc contains:
test() {
io.std.writeln("This is an example.", _)
}
the procedure can be called by telling example.test().
Top-level phrases are read with silcc.top as current module. This module reacts to some directives like trace() for debugging purpose.
Files are sought in the current directory and then in the directories
enumerated in the SILCC_PATH environment variable,
where directories are separated by colons.
This variable should typically contains the path to the standard library.
If this variable is not defined, the standard library is heuristically
sought in the path ../lib relatively to the
location of the silcc
executable.
The free variable x.y.z designates the file x/y/z.lcc. To be called this way, the file should begin by package x.y (in order to ensure that the name of the variable is unique).
Here is the classical recursive algorithm for solving the Towers of Hanoi.
exists m,
m.Hanoi(n, A, B, C, k) {
k = do {
if n = 0 do {
io.std.writeln("I have nothing to do.")
}
else if n = 1 do {
io.std.writeln("I move a disk from " A " to " C)
}
else do {
m.Hanoi(n - 1, A, C, B)
io.std.writeln("I move a disk from " A " to " C)
m.Hanoi(n - 1, B, A, C)
}
}
}
m.Hanoi(4, "A", "B", "C", _)
When the do { ... } is used in term position, it returns the last continuation if the sequence is not empty. If the sequence is empty, it tells the token done() in a fresh module variable and returns it.
Lists of values can be constructed with the notation [v1, ..., vn]. Lists are constructed recursively from the value [] (which is a notation for data.list.nil()) and head :: tail (which is a notation for data.list.cons(head, tail)) where head is the first element and tail the list of the other elements. The length of a list is measurable with data.list.length. List concatenation can be computed with data.list.concat(l0, l1) or just by putting lists one after the other like in (l0 l1) (which is just a notation for data.term.concat(l0, l1), defined for lists and strings).
Iterations can be written with the for notation. In the following example, we use it on lists.
do {
for i in ["one", "two", "three"] do {
io.std.writeln(i)
}
}
Remark. The previous code is just a notation for the following.
do {
["one", "two", "three"].iter(
module {
forall i v (do(i, v) => io.std.writeln(i, v))
}
)
}
Hence, all modules which implement asks on the iter token can be iterated with for. There is also a version of the for notation without continuation. For iterating on integers, one can use the notation 1 .. 10 (which is rewritten as data.int.range(1, 10) which returns a module implementing iter).
do {
for _ in 1 .. 10 do {
io.std.writeln("This will be written ten times.")
}
}
Lists can be destructed by pattern-matching: pattern-matching generalizes the if/else by allowing the if branch to introduce existential variables. (Note that let x = v is just a notation for exists x', x' = v exists x, x = x' with the introduction of the fresh variable x' to avoid capturing x in v).
let l = ["a", "b", "c"]
if exists hd tl, l = hd :: tl do {
io.std.writeln("Head: " hd)
io.std.writeln("Tail: " tl.string())
}
Terms are constructed by quoting the functor, possibly followed by arguments between parentheses. Functors are mapped to integers, in particular single-character functors are mapped to Unicode code-point. (Note that pattern-matching can be decomposed in several conjunctions to keep intermediate sub-terms.)
let t = 'a compound term'(1, ['f'('a')])
if exists t' c, t = 'a compound term'(_, [t']) and t' = 'f'(c) do {
io.std.writeln(t.functor())
io.std.writeln(t'.functor())
io.std.write_char(c)
io.std.write_char('\n')
}
Telling functor to a compound term returns its functor as a character string, telling arity returns its arity. t[n] returns the nth argument (in general, e[n] is just a notation for e.get(n)).
Indeed, let is just a particular case of pattern-matching where all free variables are implicitly quantified.
let t = 'f'("Hello")
let 'f'(x) = t
do { io.std.writeln(x) }
for does pattern-matching as well to filter between enumerated items (note that iterating over a compound term means iterating over its arguments).
do {
for [x] in 'f'(["a"], ["b", "c"], ["d"]) do {
io.std.writeln(x)
}
}
Remark. The previous code is just a notation for the following.
do {
'f'(["a"], ["b", "c"], ["d"]).iter(
module {
forall i v (do(i, v) =>
v = (
if exists x, i = [x] do { io.std.writeln(x) }
else do {}
)
)
}
)
}
The <- notation for do sequences allows pattern-matching as well. Note the notation for tuples: in the following, the token value has only one argument (a pair). Tuples are just a notation for terms with the functor ''.
exists m,
forall k (
m.a(k)
=>
k.value((2, 5))
)
do {
(x, y) <- m.a()
io.std.writeln(x + y)
}
Remark. This example is expanded to the following code.
exists m, forall k ( m.a(k) => k.value((2, 5)) ) exists k, m.a(k) forall x y (k.value((x, y)) -> io.std.writeln(x + y, _))
New mutable references may be defined with data.ref.new(initial value). They act as a value but can be modified with do { x := new value } (x := e is just a notation for x.set(e)).
let x = data.ref.new(1)
do {
io.std.writeln(x * 2)
x := x + 1
io.std.writeln(x * 2)
}
Records are denoted { field:value; ...; field:value }. They are modules where each field is a function returning its value, plus support for enumerating fields and values. We can access to the field f in x with the expression x:f which is a notation for x.f() (this notation is not specific to records). In pattern-matching, all fields must match and there should not be other fields except if ... is used.
let x = { a: "hello"; b: 42 }
if exists a, x = { a: a ... } do {
io.std.writeln(a)
}
Remark.
If the value of a field is ommited,
e.g. { f }
, then
the field
takes the value of the variable with the same name:
{ f: f }
.
The previous example can then be rewritten as follows.
let x = { a: "hello"; b: 42 }
if exists a, x = { a ... } do {
io.std.writeln(a)
}
The expression data.hashtbl.new(initial size) (defined in the standard library of the on-going 0.0.1 version) returns a fresh hash-table which associates a fresh variable to each domain value. The expression tbl[key] returns the value associated to key.
let t = data.hashtbl.new(17)
t['f'({ a: 1})] = "example"
t[{u: 2; v: 3}] = "test"
with io.std do {
writeln(t['f'({ a: 1})])
writeln(t[{u: 2; v: 3}])
}
Hash-tables are useful to implement indexing on token arguments. Since there is only native indexation on token modules, filtering on arguments in asks can be inefficient. This is a consequence of kernel design: the ask
forall i (m.a(i) m.b(i) -> ...)
is rewritten in
forall i j (m.a(i) m.b(j) -> if i = j { ... })
and is therefore fired for every pair of tokens a(i) and b(j). However, an hash-table can be introduced to index the tokens m.b(i) on their argument i: each token m.b(i) is consumed to produce a token m'.b() where m' is indexed on i.
exists m, let b-tbl = data.hashtbl.new(17) forall i (m.b(i) => b-tbl[i].b())
The ask on m.a(i) and m.b(i) can now be written with indexing.
forall i (m.a(i) b-tbl[i].b() -> io.std.writeln(i, _))
m.a("Test") m.b("Test")
It is worth noticing that since b-tbl[i].b() depends on b(i), consuming one or the other is equivalent. Therefore, angelism ensures that user-indexing on b-tbl[i].b() correctly cohabitates with other asks on b(i).
Let say we want to write an agent with an ask equivalent to, by abuse of notation, forall i (m.a(i) m.a(i + 1) ... m.a(2 * i) -> ...). The basic idea is to iterativaly construct chains m'.chain(i, j) in a local module m' by consuming the tokens m.a(i), . . . , m.a(j). Since these chains only exist in computation paths where the corresponding a() tokens have been consumed, consuming a chain is equivalent to consume the individual tokens.
exists m, exists m' ( forall i (m.a(i) => m'.chain(i, i)) forall i j (m'.chain(i, j) m.a(j + 1) => m'.chain(i, j + 1)) forall i (m'.chain(i, 2 * i) => io.std.writeln(i, _)) ) m.a(7) m.a(8) m.a(9) m.a(10) m.a(11) m.a(12) m.a(13) m.a(14)
However, the execution is noticeably slow. The m.a(i) tokens should be indexed.
exists m, exists m' ( let a-tbl = data.hashtbl.new(17) forall i (m.a(i) => a-tbl[i].a()) forall i (m.a(i) => m'.chain(i, i)) forall i j (m'.chain(i, j) a-tbl[j + 1].a() => m'.chain(i, j + 1)) forall i (m'.chain(i, 2 * i) => io.std.writeln(i, _)) ) m.a(7) m.a(8) m.a(9) m.a(10) m.a(11) m.a(12) m.a(13) m.a(14)
That's better but it is still slow. The number of chains is quadratic compared to the number of m.a(). Since angelism gives us the possibility to program our own checking procedure, we are now free to optimise it and change the complexity. All chains were constructed whereas the only interesting chains are starting from i such that m.a(2 * i) is present. Therefore, the computation of chains could be driven by the presence of the two enclosing tokens m.a(i) and m.a(2 * i).
exists m,
let a-tbl = data.hashtbl.new(17)
forall i (m.a(i) => a-tbl[i].a())
forall i (
m.a(i) a-tbl[2 * i].a()
=>
exists m',
m'.chain(i)
forall j (
m'.chain(j) a-tbl[j + 1].a()
=>
if j + 1 = 2 * i - 1 {
io.std.writeln(i, _)
}
else {
m'.chain(j + 1)
}
)
)
m.a(7) m.a(8) m.a(9) m.a(10) m.a(11) m.a(12) m.a(13) m.a(14)