# meta capability

A new meta capability has been added for greater flexibility to efficiently handle some situations.

When the model contains at least one attempt to reference a meta atom, then the model will be automatically augmented with meta atoms as follows:

- For each user-defined sig X, we add a meta atom “X$”; and for each field Y in a user defined sig X, we add a meta atom “X$Y”.
- Given the meta atom “X$” representing some user signature; “X$.fields” represents the meta atoms for its immediate fields and “X$.subfields” the meta atoms for it and all descendants’ fields.
- Given the meta atom “X$Y” representing some field; “X$Y.value” represents the actual field value in the real world.
- An atom “sig$” is added that represents the union of all meta atoms that represent signatures as well as a “field$” atom representing the union of all meta atoms that represent fields.

So, for example, say we have the following model:

```
sig A {
x: Int,
y: Int,
z: Int
}
```

One common thing you might want to have is an equals predicate:

```
pred eq[a1, a2 : A] { a1.x=a2.x and a1.y=a2.y and a1.z=a2.z }
```

The inconvenience with doing it this way is that it gets very long as there are more fields in the sig and if you happen to add a new field in A you have to remember to modify the eq predicate as well.

Using the meta capability this predicate could be written more succinctly (and with no impact on performance) like this:

```
pred eq[a1, a2 : A] { all f:A$.subfields | a1.(f.value)=a2.(f.value) }
```

You can also have more a intricate model such as:

```
sig A { x: Int }
sig B extends A { y: Int->Int }
```

and the following will still work:

```
pred eq [b1, b2 : B] { all f:B$.subfields | b1.(f.value)=b2.(f.value) }
```

We do some manipulations to make this common idiom work because it’s a fairly common one:
whenever we see an expression of the kind `all f:GUARD | body`

or `some f:GUARD | body`

where GUARD’s
type is a subtype of `(sig$+field$)`

, we replicate the body multiple times for each possible meta atom
in existence, and bind `f`

to each possible meta atom one-at-a-time. We do this in such a way that there’s
no impact in performance; the cost of writing a frame condition using the meta capability is exactly the
same as if you manually enumerate each field.

But this is a one-off case, so always be mindful about the expressions you write since these will still need to type-check.