tnelson/Margrave — Issue #88: Bug: term type not being carried over if term is created during substitution
Author: tnelson
Created: 2012-01-13 20:05:10+00:00
State: open
Labels: FOR-3.1, HIGH-PRIORITY

If the term (f x) exists in a policy IDB formula permit(x), and that formula is invoked with, say, permit('c), the resulting term (f c) is not given a type. The substitution visitor is not informing the vocabulary of the new term.

If old term is a function term, the type remains the same (since the outer func is the same)
If old term is a variable term, the type may change. E.g. if x: A, 'c : B, B < A.