Commit 7a88cdf
Change
The motivation for this change is to avoid α-normalizing all imported
expressions.
For example, before this change you would get the following behavior
beginning with an empty cache
```
$ cat ./example.dhall
λ(a : Type) → a
$ dhall <<< './example.dhall'
λ(_ : Type) → _
```
The reason why is that the current code α-normalizes all imported
expressions, even when returning them fresh.
To fix this, I changed the `ImportSemantics` type to not require that
expressions are α-normalized. Instead, the α-normalization only
happens at the last minute when interacting with the semantic cache, but
nowhere else.
I figured that this change would also be fine from the perspective of
the semi-semantic cache because false-negatives for this cache are
fine. In particular, we probably don't mind if we get a cache miss for
the semi-semantic cache if the user renames a variable.
After this change imports are no longer α-normalized, whether loaded
from a hot or cold cache:
```
$ cat ./example.dhall
λ(a : Type) → a
$ dhall <<< './example.dhall'
λ(a : Type) → a
$ dhall <<< './example.dhall'
λ(a : Type) → a
```ImportSemantics to not necessarily be α-normalized (#1162)1 parent 1970aa3 commit 7a88cdf
2 files changed
+5
-7
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
517 | 517 | | |
518 | 518 | | |
519 | 519 | | |
520 | | - | |
| 520 | + | |
521 | 521 | | |
522 | 522 | | |
523 | 523 | | |
524 | 524 | | |
525 | 525 | | |
526 | 526 | | |
527 | | - | |
| 527 | + | |
528 | 528 | | |
529 | 529 | | |
530 | 530 | | |
| |||
608 | 608 | | |
609 | 609 | | |
610 | 610 | | |
611 | | - | |
612 | | - | |
613 | | - | |
| 611 | + | |
614 | 612 | | |
615 | 613 | | |
616 | | - | |
| 614 | + | |
617 | 615 | | |
618 | 616 | | |
619 | 617 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
48 | 48 | | |
49 | 49 | | |
50 | 50 | | |
51 | | - | |
| 51 | + | |
52 | 52 | | |
53 | 53 | | |
54 | 54 | | |
| |||
0 commit comments