robsimmons / dusa / 9492069169 / 1

95%

main: 95%

push

github

Significantly refactor and simplify flattening transformation, unify handling of builtins and functional predicates (#23)

## Background

### Functional predicates

I originally introduced **functional predicates** with the observation
that it's pretty nice to be able to write

```
size is 3.
color 1 is red.
color 2 is blue.
color 3 is green.
color 4 is orange.

a (color N) :- b N, N < size.
```

where the last rule is a shorthand for 

```
a Color :- b N, size is Size, N < Size, color N is Color.
```

Expanding out this shorthand is done in a step called the _flattening
transformation_.

### Built-in operatons

I also originally introduced **built-in operations** in a way that had a
complicated interaction with the term-matching infrastructure, so that,
for example, matching the term `3` against the pattern `succ X` with
`succ` registered as the `NAT_SUCC` operator would result in X being
bound to 2.

This introduced complexity into a pretty core part of the system,
**and** it wasn't clear what should happen if you try to write things
like `succ "Hello world"`.

One correct, well-understood, and uniform way to handle this sort of
operation is by treating the successor operator as an infinite relation
of the form `succ X is Y`, with the following entries:

```
succ 0 is 1.
succ 1 is 2.
succ 2 is 3.
...
```

This PR unifies the way both functional predicates and built-in
relations get treated by the static checker and the flattening
transformation.

## Built-ins are now uniformly treated as relations

Without this PR, Dusa doesn't allow you to write built-in operations as
relations. The following isn't allowed, for example:

```
#builtin NAT_SUCC succ
a 3.
b Y :- a X, succ X is Y.
```

In Dusa 0.0.14 and below, built-ins can only be referenced in their
functional form, not their relational form, even though the program was
compiling everything into the relational form. This is fixed, and... (continued)

389 of 490 branches covered (79.39%)

Branch coverage included in aggregate %.

1306 of 1875 relevant lines covered (69.65%)

9120.85 hits per line