From 3a81337691b5836a7b127f6e76a69729ee2fd0f6 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Mon, 17 Jun 2024 15:01:15 -0400 Subject: [PATCH] Add an exercise about de-duplicated version --- src/tutorial.adoc | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/src/tutorial.adoc b/src/tutorial.adoc index 07895912..8611d960 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -1173,14 +1173,6 @@ don't have `+take+`s in CN statements, because this is just a simple unfolding.) // TODO: BCP: Ugh. -One final subtlety about the `+pop+` operation: Looking at the code, -it might seem reasonable to move the identical assignments to `+x+` in both -branches to above the `+if+`. But this doesn't work because the -ownership reasoning is different. In the first case, ownership of -`+h+` comes from `+IntQueueFB+` (because `+h == q->back+`). In the -second case, it comes from `+IntQueueAux+` (because `+h != -q->back+`). - *Exercise*: Investigate what happens when you make each of the following changes to the queue definitions. What error does CN report? Where are the @@ -1202,6 +1194,21 @@ Note: I (BCP) have not worked out the details, so am not sure how hard this is (or if it is even not possible, though I'd be surprised). Please let me know if you get it working! +*Exercise*: Looking at the code for the `+pop+` operation, +it might seem reasonable to move the identical assignments to `+x+` in both +branches to above the `+if+`. This doesn't "just work" because the +ownership reasoning is different. In the first case, ownership of +`+h+` comes from `+IntQueueFB+` (because `+h == q->back+`). In the +second case, it comes from `+IntQueueAux+` (because `+h != +q->back+`). + +Can you generalize the `+snoc_facts+` lemma to handle both cases? You +can get past the dereference with a `+split_case+` but formulating the +lemma before the `+return+` will be a bit more complicated. + +Note: Again, this has not been shown to be possible, but Dhruv +believes it should be! + === The Bridge Controller (Liz's stuff goes here)