Open zhangyuanlin opened 5 years ago
Fixing this is going to require a more unified and consistent treatment of Herbrand Terms throughout the compiler. There is not a common framework for the treatment of constants and sort instances.
I can do a micro-patch for this, but all these micro-patches are creating a Frankenstein solution to a larger problem.
To the original problem, I replied in email but my reply did not get forwarded here. I've included it below. To the work around, I will need to fix as I stated in the last comment.
======
I believe we added the capability of defining attributes of constants in the theory, same grammar as sort instances but without the where clause. In my mind, sort instances definitions are always new entities being introduced. A constant definition in the structure would need to be used to subsume the named constant. But since constants are interpreted by themselves by default, using a same named entity for implicit constant definition is a potential pitfall.
Consider the scenario where there is deep hierarchy, multiple nesting of module imports. In one of those deep modules a constant is declared. The programmer is unaware of it. One of the purposes of modularity is to not have to reason about deep module imports. The programmer in the structure creates a sort instance with the same name as the constant. Should this be reported as an error? If it was the programmers intent to perform subsumption of the constant with a sort instance, shouldn't they be forced to do that explicitly through a constant definition?
=====
What do u think?
Fixing this is going to require a more unified and consistent treatment of Herbrand Terms throughout the compiler. There is not a common framework for the treatment of constants and sort instances.
I can do a micro-patch for this, but all these micro-patches are creating a Frankenstein solution to a larger problem.
My memory is that CALM doesn't support constant definition, right?
This is related to #10.
The question is: how to instantiate the attribute of a constant with a non-constant?
In theory I declare box as a constant
in structure, I have
The problem here: 1) I cannot define attribute top in theory because it refers to an instance object "t(box)."
An alternative is to define constant box as a new instance mybox. Then when defining instance mybox, we define its attribute top. This causes no error, but an exception.
What may be a solution for the above question?
Here I attach the program with constant definition.
Here is the compiler complaint: