From 9bf052cc59f1e62ca6404c4e55660828505aeb85 Mon Sep 17 00:00:00 2001 From: Edsko de Vries Date: Sun, 17 Dec 2023 10:58:09 +0100 Subject: [PATCH] Annotated execution --- .gitignore | 1 + examples/circular_hos.hs | 18 ++++++++++++++++++ examples/repmin.hs | 16 ++++++++++++++++ 3 files changed, 35 insertions(+) diff --git a/.gitignore b/.gitignore index ef7fc1c..24aec9b 100644 --- a/.gitignore +++ b/.gitignore @@ -7,3 +7,4 @@ dist-newstyle/ .stack-work .cabal.sandbox.config .envrc +foo.js diff --git a/examples/circular_hos.hs b/examples/circular_hos.hs index dc8bc6f..28c3fd8 100644 --- a/examples/circular_hos.hs +++ b/examples/circular_hos.hs @@ -17,6 +17,24 @@ -- > --hide-selector-thunk-opt \ -- > --javascript foo.js \ -- > -i examples/circular_hos.hs +-- +-- Annotated execution (as of a59bccb): +-- +-- 2. As soon as we demand the value of @maxBV body_0@ to determine the +-- variable to be used for the outer-most lambda, this will force the +-- construction of the next term down. This happens recursively, so the +-- entire term is build in memory. +-- 14. This is an instructive subsequence: we will see the evaluation of +-- the simple term @lam (\y -> y)@. +-- 20. At this point this term is fully known: @Lam 1 (Var 1)@. +-- 21. The computation is driven by the computation of the variable to be used +-- for the outermost lambda; we can now continue this computation a little +-- bit, because we now know the @maxBV@ of the subterm @Lam 1 (Var 1)@. +-- 22. We repeat for the second simple term @lam (\z -> z)@. +-- 32. At this point we're almost done: we need to know the @max@BV@ of the +-- subterm @Var n_1@, but there aren't any, so that is just @0@. +-- 34. At this point all bound variables are known, and the new term has been +-- constructed. maxBV = (\exp -> case exp of { Var x -> 0 diff --git a/examples/repmin.hs b/examples/repmin.hs index ae28a32..467f28a 100644 --- a/examples/repmin.hs +++ b/examples/repmin.hs @@ -14,6 +14,22 @@ -- > --hide-selector-thunk-opt \ -- > --javascript foo.js \ -- > -i examples/repmin.hs +-- +-- Annotated execution (as of a59bccb): +-- +-- 1. One way to think about this circular program is to consider that it +-- first creates a pointer to an int (the new value in the leaves), and +-- then starts building up a tree with all leaves pointing to this int; +-- as it builds the tree, it is also computing the value of this int. +-- 6. We're starting to see the tree take shape here; the top-level structure +-- of the tree is now known. +-- 10. Similarly, we now see the shape of the left subtree. +-- 13. Here we see the first @Leaf@, ponting to @m_1@; part of the computation +-- of @m_1@ is now also known (@mb_7@). +-- 16. The second @Leaf@ is known. +-- 18. The minimum value of the left subtree is known (@mb_4@). +-- 28. At this point the structure of the tree is mostly done. We can +-- finish the value computation. worker = (\m -> \t -> case t of { Leaf x -> Pair x (Leaf m)