Skip to content

more efficient definition of toDate#911

Open
cdisselkoen wants to merge 2 commits intomainfrom
cdisselkoen/toDate
Open

more efficient definition of toDate#911
cdisselkoen wants to merge 2 commits intomainfrom
cdisselkoen/toDate

Conversation

@cdisselkoen
Copy link
Contributor

Refactors the definition of Datetime.toDate (both in Spec and in SymCC) for efficiency.

Some of this diff is just to resolve compiler warnings that currently exist on main.

Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
@@ -269,12 +269,9 @@ public def durationSince (datetime other: Datetime) : Option Duration :=
Int64.sub? datetime.val other.val

public def toDate (datetime: Datetime) : Option Datetime :=
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we leave this implementations as it is? As a definition of the semantics of toDate I think the conditional logic is clearer than wondering what exactly Int64.smod does.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure I agree that the existing definition involving all of {div, *, mod} is easier to reason about than the new one. Maybe there's a third definition that's clearer than either

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it would also be nice to see the semantics remain the same while only the encoding is changed, I don't know how in general you view changes in the spec.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

+1 to @john-h-kastner-aws 's comment

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the issue with smod is that you need to remember which kind of division it implements (truncated vs floored vs Euclidian), while this just keeps it explicit so I also find it more readable.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll see how hard it is to prove the new encoding compliant with the old spec. See if I can get it done by EOD :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants