jsiek / deduce

A proof checker meant for education. Primarily for teaching proofs of correctness of functional programs.
59 stars 3 forks source link

Overloading Creates Issues for Variables that aren't functions #2

Closed HalflingHelper closed 1 month ago

HalflingHelper commented 2 months ago

The Following program fails:

import Nat
define x = 7
define x = 8
print suc(x)

with the error

test.pf:4.11-4.12: expected a term of type Nat
but got term x of type (x.8: Nat & x.1111: Nat)

This appears to be a problem caused by the type checker and how it handles overloading defines with repeated variable names, and being unable to figure out the situation when they are passed as function arguments.

This is a big issue in particular with the libraries. For example List.pf has L1 defined with in, leading to any program intending to use L1 as a name failing when it tries to pass it as a function argument (A 343 student did exactly this, which is what led me to pursue this bug).

I'm not sure what the best solution is

HalflingHelper commented 2 months ago

I'm not sure what the best way is to detect that with this architecture.

Having said this I modified the Define case of process_declaration in a way that appears to solve the issue (passing all tests).

I'm happy to add additional tests for the cases that cause the bug if you think this is a good solution.

https://github.com/jsiek/deduce/pull/3