PLT-1566 Add cost semantics for basic builtins

[mjaskelioff]

Cost semantics in the metatheory for the following builtin functions, and their corresponding costing models.

addInteger
subtractInteger
multiplyInteger
divideInteger
quotientInteger
remainderInteger
modInteger
equalsInteger
lessThanInteger
lessThanEqualsInteger
ifThenElse

[michaelpj]

LGTM!

[michaelpj]

aren't these exactly two arguments? or have you just generalised?

[mjaskelioff]

This a generalisation. As for higher number of arguments, constant and linear-on-a-single variable seem to be the used models. In this way I only need to provide semantics for these two models.

[michaelpj]

this doesn't seem right, isn't arity here counting the type arguments too? whereas I think the model arguments are only the value arguments

[michaelpj]

I'm unsure if this is a problem or not, you might be getting away with it because you're using the constant model for all the builtins that have type arguments?

[mjaskelioff]

We don't have type arguments per se, so this is the number of value arguments. In the formalisation, all signatures have the type quantifiers at the beginning, so we only record them with a number (actually two numbers, so we know how many * and how many # variables there are). See the definition of signature.

[michaelpj]

At some point we'll want to do a version with something like SatInt and I guess prove this?

[mjaskelioff]

Yes. That is something we can do to be more certain about this. However, I don't think it matters for the purposes of analysing different cost models.