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):