-
Notifications
You must be signed in to change notification settings - Fork 5
Open
Description
After #193 is implemented.
I'm doing this:
$ cat foo.phi
{⟦ m ↦ Q.k, k ↦ ⟦⟧ ⟧.k}
$ phino rewrite --normalize --sweet --log-level=DEBUG < foo.phi
[DEBUG]: Amount of rewriting cycles: 25
[DEBUG]: Reading from stdin
[DEBUG]: The --normalize option is provided, built-it normalization rules are used
[DEBUG]: Starting rewriting cycle 0 out of 25
[DEBUG]: DOT
{⟦ ρ ↦ ∅ ⟧(
ρ ↦ ⟦
m ↦ Φ.k,
k() ↦ ⟦⟧
⟧
)}
[DEBUG]: Starting rewriting cycle 1 out of 25
[DEBUG]: COPY
{⟦
ρ ↦ ⟦
m ↦ Φ.k,
k() ↦ ⟦⟧
⟧
⟧}
[DEBUG]: Starting rewriting cycle 2 out of 25
[DEBUG]: Rewriting is stopped since it does not affect program anymore
[DEBUG]: Printing rewritten 𝜑-program as phi
{⟦
ρ ↦ ⟦
m ↦ Φ.k,
k() ↦ ⟦⟧
⟧
⟧}
Here, at the second step (COPY) we print the expression that contains something that has already been seen in the previous step (DOT):
⟦ m ↦ Φ.k, k() ↦ ⟦⟧ ⟧
If --output=latex (#193) is specified, we should use \phiAgain to highlight the places that have been seen earlier (with a unique marker of them):
{⟦ ρ ↦ ∅ ⟧(
ρ ↦ \phiAgain{1}{⟦
m ↦ Φ.k,
k() ↦ ⟦⟧
⟧}
)}
{⟦
ρ ↦ \phiAgain{1}{⟦
m ↦ Φ.k,
k() ↦ ⟦⟧
⟧}
⟧}
Metadata
Metadata
Assignees
Labels
No labels