From 54f07a87abd25524b0e1599cc5208c0c88b7a8c1 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 21 Nov 2010 15:33:02 -0500 Subject: [PATCH] week9 tweak Signed-off-by: Jim Pryor --- hints/assignment_7_hint_5.mdwn | 2 +- week9.mdwn | 31 ++++++++++++++++++++++++------- 2 files changed, 25 insertions(+), 8 deletions(-) diff --git a/hints/assignment_7_hint_5.mdwn b/hints/assignment_7_hint_5.mdwn index 40df3b81..acbc9015 100644 --- a/hints/assignment_7_hint_5.mdwn +++ b/hints/assignment_7_hint_5.mdwn @@ -49,7 +49,7 @@ 
bind_set (bind_set u \[[∃x]]) \[[Px]]
-* Let's compare this to what \[[∃xPx]] would look like on a non-dynamic semantics, for example, where we use a simple reader monad to implement variable binding. Reminding ourselves, we'd be working in a framework like this. (Here we implement environments or assignments as functions from variables to entities, instead of as lists of pairs of variables and entities. An assignment `r` here is what `fun c -> List.assoc c r` would have been in [week6]( +* Let's compare this to what \[[∃xPx]] would look like on a non-dynamic semantics, for example, where we use a simple reader monad to implement variable binding. Reminding ourselves, we'd be working in a framework like this. (Here we implement environments or assignments as functions from variables to entities, instead of as lists of pairs of variables and entities. An assignment `r` here is what `fun c -> List.assoc c r` would have been in [week7]( /reader_monad_for_variable_binding).) type assignment = char -> entity;; diff --git a/week9.mdwn b/week9.mdwn index b38293d1..f5beebb4 100644 --- a/week9.mdwn +++ b/week9.mdwn @@ -291,7 +291,21 @@ Now we're going to relativize our interpretations not only to the assignment fun > \[[expression]]g s = (value, s') -With that kind of framework, we can interpret `newref`, `deref`, and `setref` as follows. +For expressions we already know how to interpret, `s'` will usually just be `s`. One exception is complex expressions like `let var = expr1 in expr2`. Part of interpreting this will be to interpret the sub-expression `expr1`, and we have to allow that in doing that, the store may have already been updated. We want to use that possibly updated store when interpreting `expr2`. Like this: + + let rec eval expression g s = + match expression with + ... + | Let (c, expr1, expr2) -> + let (value, s') = eval expr1 g s + (* s' may be different from s *) + (* now we evaluate expr2 in a new environment where c has been associated + with the result of evaluating expr1 in the current environment *) + eval expr2 ((c, value) :: g) s' + ... + +Let's consider how to interpet our new syntactic forms `newref`, `deref`, and `setref`: + 1. \[[newref starting_val]] should allocate a new reference cell in the store and insert `starting_val` into that cell. It should return some "key" or "index" or "pointer" to the newly created reference cell, so that we can do things like: @@ -307,7 +321,7 @@ With that kind of framework, we can interpret `newref`, `deref`, and `setref` as let rec eval expression g s = match expression with ... - | Newref expr -> + | Newref (expr) -> let (starting_val, s') = eval expr g s (* note that s' may be different from s, if expr itself contained any mutation operations *) (* now we want to retrieve the next free index in s' *) @@ -323,7 +337,7 @@ With that kind of framework, we can interpret `newref`, `deref`, and `setref` as let rec eval expression g s = match expression with ... - | Deref expr -> + | Deref (expr) -> let (Index n, s') = eval expr g s (* note that s' may be different from s, if expr itself contained any mutation operations *) in (List.nth s' n, s') @@ -334,7 +348,7 @@ With that kind of framework, we can interpret `newref`, `deref`, and `setref` as let rec eval expression g s = match expression with ... - | Setref expr1 expr2 + | Setref (expr1, expr2) -> let (Index n, s') = eval expr1 g s (* note that s' may be different from s, if expr itself contained any mutation operations *) in let (new_value, s'') = eval expr2 g s' @@ -349,6 +363,9 @@ With that kind of framework, we can interpret `newref`, `deref`, and `setref` as ... + + + ##How to implement implicit-style mutable variables## With implicit-style mutation, we don't have new syntactic forms like `newref` and `deref`. Instead, we just treat ordinary variables as being mutable. You could if you wanted to have some variables be mutable and others not; perhaps the first sort are written in Greek and the second in Latin. But we will suppose all variables in our language are mutable. @@ -359,7 +376,7 @@ This brings up an interesting conceptual distinction. Formerly, we'd naturally t To handle implicit-style mutation, we'll need to re-implement the way we interpret expressions like `x` and `let x = expr1 in expr2`. We will also have just one new syntactic form, `change x to expr1 then expr2`. -Here's how to implement these. We'll suppose that our assignment function is list of pairs, as in [week6](/reader_monad_for_variable_binding). +Here's how to implement these. We'll suppose that our assignment function is list of pairs, as in [week7](/reader_monad_for_variable_binding). let rec eval expression g s = match expression with @@ -370,7 +387,7 @@ Here's how to implement these. We'll suppose that our assignment function is lis in let value = List.nth s index in (value, s) - | Let (c : char) expr1 expr2 -> + | Let ((c : char), expr1, expr2) -> let (starting_val, s') = eval expr1 g s (* get next free index in s' *) in let new_index = List.length s' @@ -379,7 +396,7 @@ Here's how to implement these. We'll suppose that our assignment function is lis (* evaluate expr2 using a new assignment function and store *) in eval expr2 ((c, new_index) :: g) s'' - | Change (c : char) expr1 expr2 -> + | Change ((c : char), expr1, expr2) -> let (new_value, s') = eval expr1 g s (* lookup which index is associated with Var c *) in let index = List.assoc c g -- 2.11.0