\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
+
+\startlambda
+\italic{normal} = \italic{lambda}
+\italic{lambda} = λvar.\italic{lambda} (representable(typeof(var)))
+ | \italic{toplet}
+\italic{toplet} = let \italic{binding} in \italic{toplet}
+ | letrec [\italic{binding}] in \italic{toplet}
+ | var (representable(typeof(var)), fvar(var))
+\italic{binding} = var = \italic{rhs} (representable(typeof(rhs)))
+ -- State packing and unpacking by coercion
+ | var0 = var1 :: State ty (fvar(var1))
+ | var0 = var1 :: ty (var0 :: State ty) (fvar(var1))
+\italic{rhs} = userapp
+ | builtinapp
+ -- Extractor case
+ | case var of C a0 ... an -> ai (fvar(var))
+ -- Selector case
+ | case var of (fvar(var))
+ DEFAULT -> var0 (fvar(var0))
+ C w0 ... wn -> resvar (\forall{}i, wi \neq resvar, fvar(resvar))
+\italic{userapp} = \italic{userfunc}
+ | \italic{userapp} {userarg}
+\italic{userfunc} = var (tvar(var))
+\italic{userarg} = var (fvar(var))
+\italic{builtinapp} = \italic{builtinfunc}
+ | \italic{builtinapp} \italic{builtinarg}
+\italic{builtinfunc} = var (bvar(var))
+\italic{builtinarg} = \italic{coreexpr}
\stoplambda
+-- TODO: Define tvar, fvar, typeof, representable
+-- TODO: Limit builtinarg further
+
+-- TODO: There can still be other casts around (which the code can handle,
+e.g., ignore), which still need to be documented here.
+
+-- TODO: Note about the selector case. It just supports Bit and Bool
+currently, perhaps it should be generalized in the normal form?
+
When looking at such a program from a hardware perspective, the top level
lambda's define the input ports. The value produced by the let expression is
the output port. Most function applications bound by the let expression
\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
~