From: Matthijs Kooijman <matthijs@stdin.nl>
Date: Mon, 7 Dec 2009 14:17:42 +0000 (+0100)
Subject: Add Scrutinee binder removal.
X-Git-Tag: final-thesis~52
X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=commitdiff_plain;h=05ab912a6a0d53892521265750b313126ab442af;hp=98d81639c3c9d4652c5828fca4a76fd88ced42eb

Add Scrutinee binder removal.
---

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index e1a96ff..2768ba2 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -1502,6 +1502,46 @@
           \stopframedtext
         }
 
+      \subsubsection{Scrutinee binder removal}
+        This transformation removes (or rather, makes wild) the binder to
+        which the scrutinee is bound after evaluation. This is done by
+        replacing the bndr with the scrutinee in all alternatives. To prevent
+        duplication of work, this transformation is only applied when the
+        scrutinee is already a simple variable reference (but the previous
+        transformation ensures this will eventually be the case). The
+        scrutinee binder itself is replaced by a wild binder (which is no
+        longer displayed).
+
+        Note that one could argue that this transformation can change the
+        meaning of the Core expression. In the regular Core semantics, a case
+        expression forces the evaluation of its scrutinee and can be used to
+        implement strict evaluation. However, in the generated \VHDL,
+        evaluation is always strict. So the semantics we assign to the Core
+        expression (which differ only at this particular point), this
+        transformation is completely valid.
+
+        \starttrans
+        case x of bndr
+          alts
+        -----------------        \lam{x} is a local variable reference
+        case x of
+          alts[bndr=>x]
+        \stoptrans
+
+        \startbuffer[from]
+        case x of y
+          True -> y
+          False -> not y
+        \stopbuffer
+
+        \startbuffer[to]
+        case x of
+          True -> x
+          False -> not x
+        \stopbuffer
+
+        \transexample{scrutbndrremove}{Scrutinee binder removal}{from}{to}
+
       \subsubsection{Case normalization}
         This transformation ensures that all case expressions get a form
         that is allowed by the intended normal form. This means they
diff --git a/Chapters/Prototype.tex b/Chapters/Prototype.tex
index 7d99104..101594b 100644
--- a/Chapters/Prototype.tex
+++ b/Chapters/Prototype.tex
@@ -516,12 +516,12 @@
       
       A case expression evaluates its scrutinee, which should have an
       algebraic datatype, into weak head normal form (\small{WHNF}) and
-      (optionally) binds it to \lam{bndr}. Every alternative lists a
-      single constructor (\lam{C0 ... Cn}). Based on the actual
-      constructor of the scrutinee, the corresponding alternative is
-      chosen. The binders in the chosen alternative (\lam{bndr0,0 ....
-      bndr0,m} are bound to the actual arguments to the constructor in
-      the scrutinee.
+      (optionally) binds it to \lam{bndr}. If bndr is wild, \refdef{wild
+      binders} it is left out.  Every alternative lists a single constructor
+      (\lam{C0 ... Cn}). Based on the actual constructor of the scrutinee, the
+      corresponding alternative is chosen. The binders in the chosen
+      alternative (\lam{bndr0,0 ....  bndr0,m} are bound to the actual
+      arguments to the constructor in the scrutinee.
 
       This is best illustrated with an example. Assume
       there is an algebraic datatype declared as follows\footnote{This
diff --git a/Outline b/Outline
index c9f6638..56fc5f0 100644
--- a/Outline
+++ b/Outline
@@ -46,7 +46,6 @@ Future work
 TODO: Define user / developer
 TODO: Hardware description / model vs program
 TODO: Separate compilation / Prelude
-TODO: Add case binder removal transformation
 TODO: User-defined type classes (future work?)
 TODO: Entity / Architecture / Component vs Function?
 TODO: Expand on "representable"