Macros
Untyped macros can be defined at the top level of a file. All 3 syntax are equivalent. (If parameterless, then [ ] can be omitted.)
let a[x,y,z] {...}
let a[x,y,z] = {...}
let a[x,y,z] = .....
Macro expansion obeys proper grammar, so each argument to a macro must be an integer/boolean/set/relation or must be a (possibly partial) call to a predicate/function/macro.
Macros are untyped, so in a file we can’t have 2 macros with the same name. Also, if a macro is in scope, it always overrides other possible sig/field/fun/pred with the same name (Just like when inside a paragraph if we see let x=y | F
, then in F
we always take x
to mean y
, even if globally there is some other sig x
or some other field x
)
Lexical scoping: Inside a macro body, if you refer to a name not in the parameter list, then we will resolve it from the file that “defined” the macro, rather than resolve it from the file that “calls” the macro.
Currying: if you call a macro with insufficient number of arguments, then the result is a new macro with the first N
parameters filled in, like currying.
Examples
Applying Macros
let apply [a,b,c] = a[b,c]
let add [x,y] = x.plus[y]
check { apply[add, 2, 3] = 5 }
or even:
check { apply[plus, 2, 3] = 5 }
Implementing “then” using currying
open util/ordering[Time]
sig Time { }
let then [a, b, t, t'] { some x:Time | a[t,x]&& b[x,t'] }
one sig Light { brightness: Int one-> Time }
pred brighter [t, t': Time] {
Light.brightness.t' = Light.brightness.t.plus[1]
t' = t.next
}
pred dimmer [t, t': Time] {
Light.brightness.t' = Light.brightness.t.minus[1]
t' = t.next
}
run {
some t:Time | brighter.then[dimmer].then[dimmer] [first, t]
} for 4 Time
Dynamics
To make it easier to denote dynamic fields macros can be used:
let dynamic[x] = x one->Time
let dynamicSet[x] = x->Time
Sequential composition works due to the currying semantics. Given predicate p[t,t':Time]
or macro p[t,t']
, q[t,t':Time]
, and q[t,t']
, given predicate r[t,t':Time]
or macro r[t,t']
, you can construct the sequential composition pqr
without needing to declaring and passing in t1,t2,t3,t4:
let then [a, b, t, t'] {
some x:Time | a[t,x]&& b[x,t']
}
let pqr = p.then[q].then[r]
It is easy to have in
parameter and an out
parameter for an imperative event. Just list them before t
and t'
. Eg.
let a[x,t,t'] { ... }
It is easy to have local variables in an imperative event, as long as the local variable is written to at most once. Just add a some x:SomeType
in front of the body. eg.
some x, y:Int | a[x].then[b].then[c[x,y]].then[d[y]]
while[cond,body]
works. Where cond should evaluate to a value that takes t
and where body should evaluate to a value that takes t
and t'
)
while0[cond,body,t,t']
ignores the body and just asserts that cond is false at time t and that t==t’. Then while1
as while0
+ one loop unrolling. Then while2
as while1
+ one loop unrolling. etc.
Finally, let while = while3
, so while
by default unrolls up to 3 times, and rejects traces that requires more than 3 unrollings. When the user imports util/time
, the user can re-bind while
to while2
to reduce the amount of loop unrolling, or maybe bind while
to while5
to increase the amount of loop unrolling.
This is how the farmer puzzle can be solved using these macros:
open util/ordering[Time]
sig Time { }
let dynamic[x] = x one-> Time
let dynamicSet[x] = x -> Time
let then [a, b, t, t'] {
some x:Time | a[t,x]&& b[x,t']
}
let while = while3
let while9 [cond, body, t, t'] {
some x:Time | (cond[t] => body[t,x] else t=x)&& while8[cond,body,x,t']
}
let while8 [cond, body, t, t'] {
some x:Time | (cond[t] => body[t,x] else t=x)&& while7[cond,body,x,t']
}
let while7 [cond, body, t, t'] {
some x:Time | (cond[t] => body[t,x] else t=x)&& while6[cond,body,x,t']
}
let while6 [cond, body, t, t'] {
some x:Time | (cond[t] => body[t,x] else t=x)&& while5[cond,body,x,t']
}
let while5 [cond, body, t, t'] {
some x:Time | (cond[t] => body[t,x] else t=x)&& while4[cond,body,x,t']
}
let while4 [cond, body, t, t'] {
some x:Time | (cond[t] => body[t,x] else t=x)&& while3[cond,body,x,t']
}
let while3 [cond, body, t, t'] {
some x:Time | (cond[t] => body[t,x] else t=x)&& while2[cond,body,x,t']
}
let while2 [cond, body, t, t'] {
some x:Time | (cond[t] => body[t,x] else t=x)&& while1[cond,body,x,t']
}
let while1 [cond, body, t, t'] {
some x:Time | (cond[t] => body[t,x] else t=x)&& while0[cond,body,x,t']
}
let while0 [cond, body, t, t'] {
!cond[t]&& t=t'
}
abstract sig Place { }
one sig Near, Far extends Place { }
abstract sig Object { location: dynamic[Place] }
one sig Farmer, Fox, Chicken, Grain extends Object {}
pred eats [a, b: Object] { a->b in Fox->Chicken + Chicken->Grain }
pred crossRiver [t, t': Time] {
t' = t.next
some x:Object | {
x.location.t != x.location.t'
x!=Farmer => {
x.location.t=Farmer.location.t
x.location.t'=Farmer.location.t'
}
all y:Object-Farmer-x | y.location.t = y.location.t'
}
no p, q: Object {
p.eats[q]
p.location.t'=q.location.t'
p.location.t'!=Farmer.location.t'
}
}
let notdone[t] = (Object.location.t != Far)
run {
some t:Time | {
Object.location.first=Near
while7[notdone, crossRiver, first, t]
}
} for 8 Time