Changes between Version 63 and Version 64 of ExplicitCallStack

Timestamp:

02/09/07 04:28:45 (6 years ago)

Author:

bjpop

Comment:

--

ExplicitCallStack

@@ -267 +267 @@
 === Notation ===
 
-Double square brackets denote the transformation function, which has either one or two arguments, depending on what type of entity it is applied to. In most cases it has one argument, which is just a syntactic construct, but for expressions it
-has an additional argument which represents the current stack value.
-
+Double square brackets denote the transformation function, which has two arguments. The first argument is denoted inside the brackets and it is the syntactic object that we are transforming. The second argument is a stack value.
 For instance:
 
@@ -276 +274 @@
 }}}
 
-means transform expression E with k as the current stack value.
+means transform expression E with k as the current stack value. When we wish to ignore the current stack value (because it is not meaningful in a certain context, such as the top-level declarations) we write:
+{{{
+   [[ E ]]_?
+}}}
 
 === Transformation option 1 ===
@@ -286 +287 @@
 Declarations (top level):
 
-   [[ x :: T ]]                       ==>   x :: Trace -> T     , x is function bound, and transformed for tracing
+   [[ x :: T ]]_?                     ==>   x :: Trace -> T     , x is function bound, and transformed for tracing
    
-   [[ x :: T ]]                       ==>   x :: T              , x does not match the above rule
-
-   [[ x = \y1 .. yn -> E ]]           ==>   x = \t y1 .. yn -> [[ E ]]_("x":t)       , x is transformed for tracing
-
-   [[ x = \y1 .. yn -> E ]]           ==>   x = \y1 .. yn -> [[ E ]]_["x"]           , x is not transformed for tracing
-
-   [[ x = E ]]                        ==>   x = [[ E ]]_["x"]
-
-   [[ data f a1 .. an = K1 .. Km ]]   ==>   data f a1 .. an = K1 .. Km
+   [[ x :: T ]]_?                     ==>   x :: T              , x does not match the above rule
+
+   [[ x = \y1 .. yn -> E ]]_?         ==>   x = \t y1 .. yn -> [[ E ]]_("x":t)       , x is transformed for tracing
+
+   [[ x = \y1 .. yn -> E ]]_?         ==>   x = \y1 .. yn -> [[ E ]]_["x"]           , x is not transformed for tracing
+
+   [[ x = E ]]_?                      ==>   x = [[ E ]]_["x"]
+
+   [[ data f a1 .. an = K1 .. Km ]]_? ==>   data f a1 .. an = K1 .. Km
 
 Declarations (local):