Remove explicit subscription underscores.
[matthijs/master-project/report.git] / Chapters / Normalization.tex
index a8194decdf2826b8c9677989754dcd4e3c78fa25..cbef2c0a7322718897573c561dafc22356276ce8 100644 (file)
@@ -62,27 +62,35 @@ An example of a program in canonical form would be:
 
 \startlambda
   -- All arguments are an inital lambda
-  λx.λc.λd.
-  -- There is one let expression at the top level
+  λa.λd.λsp.
+  -- There are nested let expressions at top level
   let
+    -- Unpack the state by coercion
+    s = sp :: (Word, Word)
+    -- Extract both registers from the state
+    r1 = case s of (fst, snd) -> fst
+    r2 = case s of (fst, snd) -> snd
     -- Calling some other user-defined function.
-    s = foo x
-    -- Extracting result values from a tuple
-    a = case s of (a, b) -> a
-    b = case s of (a, b) -> b
-    -- Some builtin expressions
-    rh = add c d
-    rhh = sub d c
+    d' = foo d
     -- Conditional connections
-    rl = case b of
-      High -> rhh
+    out = case a of
+      High -> r1
+      Low -> r2
+    r1' = case a of
+      High -> d
+      Low -> r1
+    r2' = case a of
+      High -> r2
       Low -> d
-    r = case a of
-      High -> rh
-      Low -> rl
+    -- Packing a tuple
+    s' = (,) r1' r2'
+    -- Packing the state by coercion
+    sp' = s' :: State (Word, Word)
+    -- Pack our return value
+    res = (,) sp' out
   in
     -- The actual result
-    r
+    res
 \stoplambda
 
 When looking at such a program from a hardware perspective, the top level
@@ -472,8 +480,8 @@ translatable. A user-defined function is any other function.
 \starttrans
 x = E
 ~
-x Y0 ... Yi ... Yn                               \lam{Y_i} is not of a runtime representable type
----------------------------------------------    \lam{Y_i} is not a local variable reference
+x Y0 ... Yi ... Yn                               \lam{Yi} is not of a runtime representable type
+---------------------------------------------    \lam{Yi} is not a local variable reference
 x' = λy0 ... yi-1 f0 ... fm yi+1 ... yn .        \lam{f0 ... fm} = free local vars of \lam{Y_i}
       E y0 ... yi-1 Yi yi+1 ... yn   
 ~