Circular substitution

This also makes a number of other improvements:

- Support multiple (mutually recursive) bindings in `let`
- Fix pattern matching on heap-allocated objects
  (we were losing sharing)
- Support heap inlining
- Support for selectors (`fst`, `snd`)
- Support the selector thunk optimization
- Add `--disable-ansi` command line
- Improve trace summarization
  (it previously generated confusing output;
  see details comments in the code)
- Add some new primitive functions (`min`, `max`)

examples/circular_hos.hs

@@ -0,0 +1,36 @@
+-- See "Using Circular Programs for Higher-Order Syntax"
+-- by Emil Axelsson and Koen Claessen (ICFP 2013)
+-- <https://emilaxelsson.github.io/documents/axelsson2013using.pdf>
+--
+-- See Unfolder episode 17 for more details.
+--
+-- Suggested execution:
+--
+-- > cabal run visualize-cbn -- \
+-- >   --show-trace \
+-- >   --hide-prelude \
+-- >   --gc \
+-- >   --selector-thunk-opt \
+-- >   --inline-heap \
+-- >   --hide-inlining \
+-- >   --hide-gc \
+-- >   --hide-selector-thunk-opt \
+-- >   --javascript foo.js \
+-- >   -i examples/circular_hos.hs
+maxBV = (\exp ->
+    case exp of {
+        Var x   -> 0
+      ; App f e -> max (@maxBV f) (@maxBV e)
+      ; Lam n f -> n
+      }
+  )
+
+lam = (\f ->
+     let {
+         body = f (Var n)
+       ; n    = succ (@maxBV body)
+       }
+     in seq n (Lam n body)
+  )
+
+main = @lam (\x -> App (App (@lam (\y -> y)) (@lam (\z -> z))) x)

examples/multiple-beta.hs

@@ -0,0 +1,7 @@
+f = (\x -> @g x)
+g = (\x -> @h x)
+h = (\x -> succ x)
+
+main = @f 1
+
+

examples/mutual_rec.hs

@@ -0,0 +1,7 @@
+-- Simple example of two mutually recursive functions
+-- f x will return 0 if x is even and 1 if x is odd.
+main =
+     let {
+         f = (\x -> if eq x 0 then 0 else g (sub x 1))
+       ; g = (\x -> if eq x 0 then 1 else f (sub x 1))
+     } in f 2

examples/repmin.hs

@@ -0,0 +1,35 @@
+-- The classic repMin circular program due to Richard Bird.
+-- See Unfolder episode 17 for more details.
+--
+-- Suggested execution:
+--
+-- > cabal run visualize-cbn -- \
+-- >   --show-trace \
+-- >   --hide-prelude \
+-- >   --gc \
+-- >   --selector-thunk-opt \
+-- >   --inline-heap \
+-- >   --hide-inlining \
+-- >   --hide-gc \
+-- >   --hide-selector-thunk-opt \
+-- >   --javascript foo.js \
+-- >   -i examples/repmin.hs
+worker = (\m -> \t ->
+      case t of {
+          Leaf x -> Pair x (Leaf m)
+        ; Branch l r ->
+            let {
+                resultLeft  = @worker m l
+              ; resultRight = @worker m r
+              ; mb          = min (fst resultLeft) (fst resultRight)
+              }
+            in seq mb (Pair mb (Branch (snd resultLeft) (snd resultRight)))
+        }
+    )
+
+repMin = (\t ->
+      let result = @worker (fst result) t
+      in snd result
+    )
+
+main = @repMin (Branch (Branch (Leaf 1) (Leaf 2)) (Branch (Leaf 3) (Leaf 4)))

examples/selthunkopt.hs

@@ -0,0 +1,28 @@
+-- Demonstration of the need for the selector thunk optimization
+-- This is the example from "Fixing some space leaks with a garbage collector".
+
+break = (\xs ->
+      case xs of {
+          Nil -> Pair Nil Nil
+        ; Cons x xs' ->
+            if eq x 0
+              then Pair Nil xs'
+              else let b = @break xs'
+                   in Pair (Cons x (fst b)) (snd b)
+        }
+    )
+
+-- strict version of concat (makes the example more clear)
+concat = (\xs -> \ys ->
+      case xs of {
+          Nil        -> ys
+        ; Cons x xs' -> let r = @concat xs' ys in seq r (Cons x r)
+        }
+    )
+
+surprise = (\xs ->
+      let b = @break xs
+      in @concat (fst b) (@concat (Cons 4 (Cons 5 (Cons 6 Nil))) (snd b))
+    )
+
+main = @surprise (Cons 1 (Cons 2 (Cons 3 (Cons 0 (Cons 7 (Cons 8 (Cons 9 Nil)))))))

src/CBN/Closure.hs

@@ -1,15 +1,15 @@
 module CBN.Closure (toClosureGraph, Closure(..), Id) where
 
 import Data.Maybe (fromJust)
-import Data.Graph as Graph
+import Data.Graph as Graph hiding (edges)
 import Control.Monad.State
 import qualified Data.Set as Set
 import qualified Data.Map as Map
 import qualified Data.Tree as Tree
 
 import CBN.Language
 import CBN.Heap
-import CBN.Trace
+import CBN.Trace ()
 
 -- Some Terms have a heap Pointer, but not an explicit CBN.Heap.Ptr.
 -- For example the closure `Cons 1 Nil` has a Pointer to `1`
@@ -59,14 +59,14 @@ thunk term = ThunkClosure term $ Set.toList $ pointers term
 -- Heap could be used in the future to eliminate Indirections.
 
 toClosure :: (Heap Term, Term) -> Closure
-toClosure (heap, term) = case term of
+toClosure (_heap, term) = case term of
   TVar (Var x) -> ErrorClosure $ "free variable " ++ show x
   TLam _ _ -> FunClosure term ls
     where ls = Set.toList $ pointers term
   TCon (ConApp con terms) -> ConClosure con terms
   TPtr ptr -> IndirectionClosure ptr
   TPrim (PrimApp p es) -> PrimClosure p es
-  TLet _ _ _ -> thunk term
+  TLet _ _ -> thunk term
   TApp _ _ -> thunk term
   TCase _ _ -> thunk term
   TIf _ _ _ -> thunk term
@@ -88,7 +88,7 @@ toClosureGraph (heap@(Heap _ hp), term) =
     -- If we ignore Heap.Ptrs, each heap term, defines a tree of other reachable
     -- terms.
     mkTree :: (Ptr, Term) -> [(Closure, Id, [Id])]
-    mkTree (ptr, term) = Tree.flatten $ addInternalEdges tree
+    mkTree (ptr, term') = Tree.flatten $ addInternalEdges tree
       where
         identify :: State Int Id
         identify = do
@@ -104,15 +104,15 @@ toClosureGraph (heap@(Heap _ hp), term) =
             cont = map addInternalEdges subTrees
 
         tree :: Tree (Id, (Closure, [Id]))
-        tree = evalState (Tree.unfoldTreeM f term) 0
+        tree = evalState (Tree.unfoldTreeM f term') 0
 
         -- The [Id] here contains only the pointer ids and
         -- Not the Ids of the same Tree, as those are not assigned yet.
         -- They are added  at `addInternalEdges`, after the creation of the whole tree.
 
         f :: Term -> State Int ((Id, (Closure, [Id])), [Term])
-        f term = do
+        f term'' = do
           myid <- identify
-          let closure = toClosure (heap, term)
+          let closure = toClosure (heap, term'')
           let (ptrs, terms) = extractEdges closure
           return ((myid, (closure, map defaultId ptrs)), terms)

src/CBN/Eval.hs

@@ -4,18 +4,27 @@ module CBN.Eval (
   , DescriptionWithContext(..)
   , Step(..)
   , step
+    -- * Case statements
+  , findMatch
+  , AllocdConArgs(..)
+  , allocConArgs
   ) where
 
+import qualified Data.Map as M
+
 import CBN.Language
 import CBN.Heap
 import CBN.Subst
-import qualified Data.Map as M
+
+{-------------------------------------------------------------------------------
+  Small-step semantics
+-------------------------------------------------------------------------------}
 
 type Error = String
 
 -- | Description of a step: what happened?
 data Description =
-    -- | We moved a let-bound variable to the heap
+    -- | We moved let-bound variables to the heap
     StepAlloc
 
     -- | Beta-reduction
@@ -35,12 +44,17 @@ data Description =
 
     -- | Seq finished evaluating its left argument
   | StepSeq
+
+    -- | We allocated constructor arguments to preserve sharing
+  | StepAllocConArgs
   deriving (Show)
 
 data DescriptionWithContext =
-    DescriptionWithContext Description [Ptr]
+    DescriptionWithContext Description Context
   deriving (Show)
 
+type Context = [Ptr]
+
 data Step =
     -- | Evaluation took a single step
     Step DescriptionWithContext (Heap Term, Term)
@@ -79,23 +93,16 @@ step (hp, TPtr ptr) =
           Step d (hp', e') -> pushContext ptr d (mutate (hp', ptr) e', TPtr ptr)
           Stuck err        -> Stuck err
           WHNF val         -> WHNF val
-step (hp, TLet x e1 (TSeq (TVar x') e2)) | x == x' =
-    -- special case for let x = e in seq x ..
-    -- rather than allocate we reduce inside the let
-    case step (hp, e1) of
-      Step d (hp', e1') -> Step d (hp', TLet x e1' (TSeq (TVar x) e2))
-      Stuck err         -> Stuck err
-      WHNF _            -> emptyContext StepSeq (hp, TLet x e1 e2)
-step (hp, TLet x e1 e2) =
-    emptyContext StepAlloc $ allocSubst RecBinding [(x,e1)] (hp, e2)
+step (hp, TLet bound e) =
+    emptyContext StepAlloc $ allocSubst bound (hp, e)
 step (hp, TApp e1 e2) = do
     let descr = case e1 of
                   TPtr ptr   -> StepApply ptr
                   _otherwise -> StepBeta
     case step (hp, e1) of
       Step d (hp', e1') -> Step d (hp', TApp e1' e2)
       Stuck err         -> Stuck err
-      WHNF (VLam x e1') -> emptyContext descr $ allocSubst NonRecBinding [(x,e2)] (hp, e1')
+      WHNF (VLam x e1') -> emptyContext descr $ allocSubst [(x,e2)] (hp, e1')
       WHNF _            -> Stuck "expected lambda"
 step (hp, TCase e ms) =
     case step (hp, e) of
@@ -105,11 +112,23 @@ step (hp, TCase e ms) =
       WHNF (VPrim _)   -> Stuck "cannot pattern match on primitive values"
       WHNF (VCon (ConApp c es)) ->
         case findMatch c ms of
-          Nothing -> Stuck "Non-exhaustive pattern match"
-          Just (xs, e') ->
-            if length xs == length es
-              then emptyContext (StepMatch c) $ allocSubst NonRecBinding (zip xs es) (hp, e')
-              else Stuck $ "Invalid pattern match (cannot match " ++ show (xs, es) ++ ")"
+          Nothing ->
+            Stuck "Non-exhaustive pattern match"
+          Just (xs, _) | length xs /= length es ->
+            Stuck $ "Cannot match " ++ show (xs, es)
+          Just (xs, rhs) ->
+            -- We /know/ that e is a con-app or a pointer to a con-app, but we
+            -- search /again/, this time with 'allocConArgs'. The reason we
+            -- search twice is that the first search enables us to find the
+            -- right variable names to use for allocation. This is not critical,
+            -- but makes the variables in the heap more human-friendly.
+            case allocConArgs xs (hp, e) of
+              ConArgsAllocFailed ->
+                error "step: impossible ConArgsAllocFailed"
+              ConArgsAllocUnnecessary _ ->
+                emptyContext (StepMatch c) $ allocSubst (zip xs es) (hp, rhs)
+              ConArgsAllocDone (ctxt, hp', e') _ ->
+                Step (DescriptionWithContext StepAllocConArgs ctxt) (hp', TCase e' ms)
 step (hp, TPrim (PrimApp p es)) =
     case stepPrimArgs hp es of
       PrimStep d hp' es' -> Step d (hp', TPrim (PrimApp p es'))
@@ -131,6 +150,79 @@ step (hp, TSeq e1 e2) =
       Stuck err         -> Stuck err
       WHNF _            -> emptyContext StepSeq (hp, e2)
 
+{-------------------------------------------------------------------------------
+  Case statements
+-------------------------------------------------------------------------------}
+
+findMatch :: Con -> Branches -> Maybe ([Var], Term)
+findMatch c (Matches ms) = go ms
+  where
+    go :: [Match] -> Maybe ([Var], Term)
+    go []                                    = Nothing
+    go (Match (Pat c' xs) e:ms') | c == c'   = Just (xs, e)
+                                 | otherwise = go ms'
+findMatch c (Selector s) =
+    findMatch c $ Matches [selectorMatch s]
+
+data AllocdConArgs =
+    -- | No allocation was necessary
+    ConArgsAllocUnnecessary ConApp
+
+    -- | The constructor arguments were heap-allocated
+  | ConArgsAllocDone (Context, Heap Term, Term) ConApp
+
+    -- | The term was not a constructor application in WHNF or a pointer to
+    -- such a term
+  | ConArgsAllocFailed
+
+-- | Allocate constructor arguments
+--
+-- This is necessary when doing a case statement on a value in the heap, to
+-- avoid losing sharing.
+allocConArgs ::
+     [Var]
+  -> (Heap Term, Term)
+  -> AllocdConArgs
+allocConArgs xs =
+    go True
+  where
+    go :: Bool -> (Heap Term, Term) -> AllocdConArgs
+    go isTopLevel (hp, term) =
+        case term of
+          TPtr ptr | Just p <- deref (hp, ptr) -> do
+            case go False (hp, p) of
+              ConArgsAllocUnnecessary conApp ->
+                ConArgsAllocUnnecessary conApp
+              ConArgsAllocFailed ->
+                ConArgsAllocFailed
+              ConArgsAllocDone (ctxt, hp', e') conApp ->
+                ConArgsAllocDone
+                  (ptr : ctxt, mutate (hp', ptr) e', TPtr ptr)
+                  conApp
+          TCon conApp@(ConApp con args) | length args == length xs ->
+            if isTopLevel || all termIsSimple args then
+              ConArgsAllocUnnecessary conApp
+            else do
+              let (hp', args') =
+                     allocMany
+                       (zipWith prepareHeapEntry xs args)
+                       processHeapEntries
+                       hp
+                  conApp' = ConApp con args'
+              ConArgsAllocDone ([], hp', TCon conApp') conApp'
+          _ ->
+            ConArgsAllocFailed
+
+    prepareHeapEntry :: Var -> Term -> (Maybe String, Ptr -> (Ptr, Term))
+    prepareHeapEntry x t = (Just (varName x), \ptr -> (ptr, t))
+
+    processHeapEntries :: [(Ptr, Term)] -> ([(Ptr, Term)], [Term])
+    processHeapEntries entries = (entries, map (TPtr . fst) entries)
+
+{-------------------------------------------------------------------------------
+  Primitive operations
+-------------------------------------------------------------------------------}
+
 -- | The result of stepping the arguments to an n-ary primitive function
 data StepPrimArgs =
     -- Some term took a step
@@ -157,19 +249,15 @@ stepPrimArgs hp = go []
           where
             acc' = map (valueToTerm . VPrim) (reverse acc)
 
-findMatch :: Con -> [Match] -> Maybe ([Var], Term)
-findMatch c = go
-  where
-    go :: [Match] -> Maybe ([Var], Term)
-    go []                                   = Nothing
-    go (Match (Pat c' xs) e:ms) | c == c'   = Just (xs, e)
-                                | otherwise = go ms
-
 delta :: Prim -> [Prim] -> Either Error Value
-delta PIAdd [PInt n1, PInt n2] = Right $ liftInt  $ n1 +  n2
-delta PISub [PInt n1, PInt n2] = Right $ liftInt  $ n1 -  n2
-delta PIMul [PInt n1, PInt n2] = Right $ liftInt  $ n1 *  n2
-delta PIEq  [PInt n1, PInt n2] = Right $ liftBool $ n1 == n2
-delta PILt  [PInt n1, PInt n2] = Right $ liftBool $ n1 <  n2
-delta PILe  [PInt n1, PInt n2] = Right $ liftBool $ n1 <= n2
+delta PISucc [PInt n]           = Right $ liftInt  $ n + 1
+delta PIAdd  [PInt n1, PInt n2] = Right $ liftInt  $ n1 + n2
+delta PISub  [PInt n1, PInt n2] = Right $ liftInt  $ n1 - n2
+delta PIMul  [PInt n1, PInt n2] = Right $ liftInt  $ n1 * n2
+delta PIMin  [PInt n1, PInt n2] = Right $ liftInt  $ n1 `min` n2
+delta PIMax  [PInt n1, PInt n2] = Right $ liftInt  $ n1 `max` n2
+delta PIEq   [PInt n1, PInt n2] = Right $ liftBool $ n1 == n2
+delta PILt   [PInt n1, PInt n2] = Right $ liftBool $ n1 <  n2
+delta PILe   [PInt n1, PInt n2] = Right $ liftBool $ n1 <= n2
 delta _op _args = Left $ "delta: cannot evaluate"
+