undefined variable `Nat` (uniquify) only when processing multiple files

[Temperz87]

When one is in tests/ and runs the command:

PYTHON ../../deduce.py --dir ../../ suffices_rewrite.pf induction1.pf switch_term.pf theorem_implies4.pf theorem_and.pf mark2.pf generic2.pf theorem_and4.pf theorem_or2.pf theorem_false3.pf theorem_implies2.pf all2.pf theorem_iff.pf inst1.pf rec1.pf inst2.pf

deduce errors out saying

inst2.pf:4.13-4.16: undefined variable `Nat`    (uniquify)

Despite inst2.pf containing Import Nat.

Alternatively, doing PYTHON ./deduce.py somefile.pf somefile.pf where somefile.pf imports something will always recreate this issue.

[jsiek]

Indeed. Here's a shorter example with the same bug:

/opt/homebrew/bin/python3.11 ../../deduce.py --dir ../..  inst1.pf inst2.pf
inst1.pf is valid
inst2.pf:4.13-4.16: undefined variable `Nat`    (uniquify)

[Temperz87]

I actually might have a fix for this in https://github.com/Temperz87/deduce/commit/5c52838b70626357c5e65130d9b18ba5fe479087 already

[jsiek]

BTW, thank you for finding this bug!

[jsiek]

The bug was in the uniquify method of the Import class. The mapping from old-names to new-names from the imported module needed to get added to the env. I fixed this with the addition of a new method collect_uniquified_name to accomplish this task.