Changes between Version 63 and Version 64 of ExplicitCallStack


Ignore:
Timestamp:
Feb 9, 2007 12:28:45 PM (8 years ago)
Author:
bjpop
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • ExplicitCallStack

    v63 v64  
    267267=== Notation ===
    268268
    269 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
    270 has an additional argument which represents the current stack value.
    271 
     269Double 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.
    272270For instance:
    273271
     
    276274}}}
    277275
    278 means transform expression E with k as the current stack value.
     276means 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:
     277{{{
     278   [[ E ]]_?
     279}}}
    279280
    280281=== Transformation option 1 ===
     
    286287Declarations (top level):
    287288
    288    [[ x :: T ]]                       ==>   x :: Trace -> T     , x is function bound, and transformed for tracing
     289   [[ x :: T ]]_?                     ==>   x :: Trace -> T     , x is function bound, and transformed for tracing
    289290   
    290    [[ x :: T ]]                       ==>   x :: T              , x does not match the above rule
    291 
    292    [[ x = \y1 .. yn -> E ]]           ==>   x = \t y1 .. yn -> [[ E ]]_("x":t)       , x is transformed for tracing
    293 
    294    [[ x = \y1 .. yn -> E ]]           ==>   x = \y1 .. yn -> [[ E ]]_["x"]           , x is not transformed for tracing
    295 
    296    [[ x = E ]]                        ==>   x = [[ E ]]_["x"]
    297 
    298    [[ data f a1 .. an = K1 .. Km ]]  ==>   data f a1 .. an = K1 .. Km
     291   [[ x :: T ]]_?                     ==>   x :: T              , x does not match the above rule
     292
     293   [[ x = \y1 .. yn -> E ]]_?         ==>   x = \t y1 .. yn -> [[ E ]]_("x":t)       , x is transformed for tracing
     294
     295   [[ x = \y1 .. yn -> E ]]_?         ==>   x = \y1 .. yn -> [[ E ]]_["x"]           , x is not transformed for tracing
     296
     297   [[ x = E ]]_?                      ==>   x = [[ E ]]_["x"]
     298
     299   [[ data f a1 .. an = K1 .. Km ]]_? ==>   data f a1 .. an = K1 .. Km
    299300
    300301Declarations (local):