-
Notifications
You must be signed in to change notification settings - Fork 483
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
CIP-0138 Builtin Array #6727
base: master
Are you sure you want to change the base?
CIP-0138 Builtin Array #6727
Conversation
@@ -698,6 +698,26 @@ | |||
"type": "constant_cost" | |||
} | |||
}, | |||
"lengthArray" : { | |||
"cpu": { | |||
"arguments": 99999999999999, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Temporary value (stub)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
When I was adding builtins, I was avoiding doing any of this, but maybe that was wrong, dunno. @kwxm should we add this stuff when adding a new builtin before costing is done?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@kwxm should we add this stuff when adding a new builtin before costing is done?
I think that in order to get the code to compile you have to add something here once you've added paramLengthArray
here, and similarly for the other new functions. However, if you use unimplementedCostingFunction
in toBuiltinMeaning
then these numbers won't be used: they only come into play when you tell the denotation to run the real costing function. I'd normally add a new builtin without adding any costing code at all in order to test that it behaves as it's supposed to, and then do all of the costing at once. That's just to cut down on the initial amount of work, and because of the way all the costing code is plumbed in it's probably not obvious that you don't initially need it. The important thing is that there's no link at all between the builtin and the costing code until you put runCostingFunction<N>Arguments . param<MyNewBuiltin>
in toBuiltinMeaning
. Maybe we should try to make that fact clearer to implementers somewhere.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Right, doing it first time it isn't 100% clear where to draw the line, so I followed the compiler and it wanted me to fix JSON as there is TH which reads it and fails to compile if the section is missing.
92b8011
to
6de1458
Compare
, paramLengthArray = Id $ ModelOneArgumentConstantCost 99 | ||
, paramListToArray = Id $ ModelOneArgumentConstantCost 99 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Dummy values
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@kwxm is this what should be done here before costing? Particularly given that listToArray
isn't gonna be constant-cost.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@kwxm is this what should be done here before costing? Particularly given that listToArray isn't gonna be constant-cost.
Good question. I think that this doesn't really matter as long as you remember to fix it. The only time this gets used is when you run generate-cost-model
, which uses this information to fill in the memory function in the JSON version of the cost model, so it has to be correct before you generate the final form of the cost model.
6de1458
to
acdd3ef
Compare
acdd3ef
to
cfd35ae
Compare
cfd35ae
to
5de42d2
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is the lack of Plinth versions of the builtins intentional?
All looks great. Kinda unfortunate that more and more is needed to add a new builtin, maybe we could automate some more. Although seems not too bad still.
, paramLengthArray = Id $ ModelOneArgumentConstantCost 99 | ||
, paramListToArray = Id $ ModelOneArgumentConstantCost 99 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@kwxm is this what should be done here before costing? Particularly given that listToArray
isn't gonna be constant-cost.
@@ -698,6 +698,26 @@ | |||
"type": "constant_cost" | |||
} | |||
}, | |||
"lengthArray" : { | |||
"cpu": { | |||
"arguments": 99999999999999, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
When I was adding builtins, I was avoiding doing any of this, but maybe that was wrong, dunno. @kwxm should we add this stuff when adding a new builtin before costing is done?
arbitraryBuiltin = do | ||
spine <- Strict.fromLazy <$> arbitrary | ||
let len = length spine | ||
for spine $ \() -> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you define in terms of the list instance instead of the Vector
one? Just arbitraryBuiltin = Strict.fromList <$> arbitraryBuiltin
or something. And the same for shrink
.
let arrayOfInts = mkConstant @(Vector Integer) @DefaultUni () (Vector.fromList [1..10]) | ||
let term = apply () (tyInst () (builtin () ListToArray) integer) listOfInts | ||
typecheckEvaluateCekNoEmit def defaultBuiltinCostModelForTesting term @?= | ||
Right (EvaluationSuccess arrayOfInts) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Some edge cases would be nice, like an empty array etc.
You should've probably used
evals
:: DefaultUni `HasTermLevel` a
=> a
-> DefaultFun
-> [Type TyName DefaultUni ()]
-> [Term TyName Name DefaultUni DefaultFun ()]
-> TestNested
from the below, we use it for unit tests. Not important though.
term = apply () (tyInst () (builtin () LengthArray) integer) arrayOfInts | ||
typecheckEvaluateCekNoEmit def defaultBuiltinCostModelForTesting term @?= | ||
Right (EvaluationSuccess expectedLength) | ||
, testCase "indexArray" do |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We should also have some property tests, but feel free to add them in a follow-up.
Yes. |
5de42d2
to
911f19d
Compare
911f19d
to
8535806
Compare
8535806
to
d3942d7
Compare
d3942d7
to
1c8d186
Compare
1c8d186
to
fe5c0a3
Compare
fe5c0a3
to
2ac9dba
Compare
Closes #6717
Data.Vector.Strict
LengthArray
ListToArray
The PR is ready for review but build is not working until we update flake inputs (need vector 0.13.2)