GRASShopper calls the standard integer type Int (not int), and the standard Boolean type Bool (not bool). This means that every time we have an integer or Boolean variable, we have to add
typedef int Int;
typedef bool Bool;
to the proof, and then jump through hoops like using x == true instead of x if we're trying to use a Bool called x in a bool position. This also turns off a lot of Starling's expression simplification.
Ideally Starling should treat the standard types specially here, and emit the GRASShopper equivalents directly.
In terms of changes I think this would need us to:
Change PrimTypeRec so that the typedef record goes from an optional typedef name to a sum type with 'indefinite', 'standard', and 'aliased type' legs. This means we can distinguish between standard types and aliased types (currently, standard ones are just given a hardcoded typedef name);
Make the GRASShopper backend emit Int and Bool when it sees the standard integer and Boolean types;
Make everything else that cares emit int and bool.
Example: see the GRASShopper proofs we have already.
GRASShopper calls the standard integer type
Int(notint), and the standard Boolean typeBool(notbool). This means that every time we have an integer or Boolean variable, we have to addto the proof, and then jump through hoops like using
x == trueinstead ofxif we're trying to use aBoolcalledxin aboolposition. This also turns off a lot of Starling's expression simplification.Ideally Starling should treat the standard types specially here, and emit the GRASShopper equivalents directly.
In terms of changes I think this would need us to:
PrimTypeRecso that the typedef record goes from anoptional typedef name to a sum type with 'indefinite', 'standard', and 'aliased type' legs. This means we can distinguish between standard types and aliased types (currently, standard ones are just given a hardcoded typedef name);GRASShopperbackend emitIntandBoolwhen it sees the standard integer and Boolean types;intandbool.Example: see the GRASShopper proofs we have already.