Ah yes, that makes sense. Thank you for investigating and clarifying that.
+1

Agda tracks the dependencies between all function parameters and the recursive calls in the body, and if the resulting dependencies are of decreasing order then the function will terminate. It should be noted though that the termination checker can find false positives, in which case you must fiddle with moving things around a bit to get the termination to check.

You're right that I did not cover Agda's requirement of termination checking. More specifically, the rule is that recursive calls must use inputs that are structurally smaller than the inputs of the original function. However, this requirement is not present in all proof languages. In Guru you can still prove things such as the reflexive property even about functions that never terminate (see page 28 of the Guru book). Additionally, once totality has been proven, you can register the function as total which gives you access to more things you can prove about it and with it that are restricted by default (page 50).

Woops, fixed that, thanks =)

Thanks for the clarifications, greatly appreciated!

Cucumber might not have your situation built in, but Transform's are very flexible! I think I understand what you need better now, check out this implementation of your TokenTransform:

http://gist.github.com/191691

Yup, the Transform regex just has to match a capture group, not have identical text. That means groups in step defs that don't match anything get checked against every Transform, and a group that matches short circuits checking the rest.

Heya Eric,

I'm not sure if I understand your situation exactly, let me know if this solves it:

# support file
Transform /^new young child (\w+)$ do |first_name|
Person.gen(:child, :first_name => first_name)
end

Transform /^new guest user (\w+)$/ do |username|
User.gen(:guest, :username => username)
end

Transform /^person (\w+)$/ do |first_name|
Person.first :first_name => first_name
end

Transform /^user (\w+)$/ do |username|
User.first :username => username
end

# step definition file
Given /^a (\w+) added by (\w+)$/ do | person, user |
user.add person
end

Then /^(user \w+) has a referral for (person \w+)$/ do |user, person |
user.should have_referral_for(person)
end

# feature file
Given a new young child Mike added by new guest user coolio
Then user coolio has a referral for person Mike

If a transform fails then all the others defined before it (from newest to oldest) are tried. If no transform ends up matching then the original argument is returned.

For simple cases where you do need to parse the entire step argument, you can include capture groups that get yielded as arguments instead:

Transform /^age (\d+)$/ do |age_string|
age_string.to_i
end

Transform /^user (\w+)$/ do |username|
User.first :username => username
end

Also, as of Cucumber 0.3.101 step argument transforms are in the official release!