TP Translation: incorrect processing of implicit function parameter types

[ldcouto]

If we have an Implicit Function with multiple parameters of different types, the translation will produce a function where all parameters have the first type.

Minimal example:

functions
 imp(a: int, b:char) r : bool
 post true

Yields:

cmlifun imp
  inp a :: "@int" and b :: "@int"
  out r :: "@bool"
  post "true"
end

[ldcouto]

@richardpayne , I did a tentative fix for this in aeb34df.

Problem seemed to be in the iteration of param types when printing the ThmNode. Please double check and close the bug. I think we need this fixed if we want to do the traffic model without maps.

[richardpaynea55]

The fix looks good, but there is a problem with a function with no parameters:

Minimal:

functions imp() r : bool post true

Generates: cmlifun imp inp out r :: "@bool" post "true"

[richardpaynea55]

Fixed with a slight hack. If an implicit function has no parameters, the visitor will add a 'dummy' input parameter, now input

imp() r : bool post true

gives:

cmlifun imp inp emptyParam :: "@bool" out r :: "@bool" post "true"