Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Measures for inline function definitions don't work #56

Open
nickbattle opened this issue Aug 27, 2021 · 1 comment
Open

Measures for inline function definitions don't work #56

nickbattle opened this issue Aug 27, 2021 · 1 comment
Assignees
Labels

Comments

@nickbattle
Copy link
Owner

Consider the following:

	f: nat -> nat
	f(x) ==
		let g: nat -> nat
			g(a) ==
				if a = 0 then 0 else a + g(a-1)
			pre a > 0
			measure a
		in
			g(x);

> p f(1)
Error 4034: Name 'measure_g' not in scope in 'DEFAULT' (test.vdm) at line 8:21

The problem is that the FunctionValue created by g does not include a measure function (though it does include a pre_g).

@nickbattle nickbattle added the bug label Aug 27, 2021
@nickbattle nickbattle self-assigned this Aug 27, 2021
@nickbattle
Copy link
Owner Author

The "measure" function within a FunctionValue is looked up on the fly, presumably as a hangover from being able to specify measures as the name of a function rather than as an expression. But the Context create that includes "g" (above) does not include a function for "measure_g" because the creation of the Context does not recurse into FunctionValues to see what they "create". It works for pre/post because their FunctionValues can be computed when the containing FunctionValue is defined.

This suggests the solution is to define "measure_g" in the same way as pre_g/post_g, and only do the name lookup if the measure "name" option is used. But be careful about polymorphic and curried functions, which can be awkward.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant