Changes between Version 25 and Version 26 of ExplicitCallStack


Ignore:
Timestamp:
Jan 29, 2007 4:58:52 PM (7 years ago)
Author:
guest
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • ExplicitCallStack

    v25 v26  
    130130Declarations: 
    131131 
    132    [[ x :: T ]]                 ==>   x :: Trace -> T     , if x is a function binding 
     132   [[ x :: T ]]                       ==>   x :: Trace -> T     , if x is a function binding 
    133133    
    134    [[ x :: T ]]                 ==>   x :: T              , is x is a CAF binding 
     134   [[ x :: T ]]                       ==>   x :: T              , is x is a CAF binding 
    135135 
    136    [[ x = \y1 .. yn -> E ]]     ==>   x = \t y1 .. yn -> [[ E ]]_("x":t) 
     136   [[ x = \y1 .. yn -> E ]]           ==>   x = \t y1 .. yn -> [[ E ]]_("x":t) 
     137 
     138   [[ x = E ]]                        ==>   x = [[ E ]]_["x"] 
     139 
     140   [[ data f a1 .. an = K1 .. Km ]]   ==>   data f a1 .. an = K1 .. Km 
    137141 
    138142Expressions: 
    139143 
    140    [[ x ]]_t                    ==>   x      , if x is either lambda bound, or a CAF. 
     144   [[ x ]]_t                          ==>   x      , if x is either lambda bound, or a CAF. 
    141145   
    142    [[ x ]]_t                    ==>   x t    , if f is function bound 
     146   [[ x ]]_t                          ==>   x t    , if f is function bound 
    143147 
    144    [[ k ]]_t                    ==>   k 
     148   [[ k ]]_t                          ==>   k 
    145149 
    146    [[ E1 E2 ]]_t                ==>   [[ E1 ]]_t [[ E2 ]]_t 
     150   [[ E1 E2 ]]_t                      ==>   [[ E1 ]]_t [[ E2 ]]_t 
    147151 
    148    [[ let D1 .. Dn in E ]]_t    ==>   let [[ D1 ]] .. [[ Dn ]] in  [[ E ]]_t 
     152   [[ let D1 .. Dn in E ]]_t          ==>   let [[ D1 ]] .. [[ Dn ]] in  [[ E ]]_t 
    149153 
    150    [[ case E of A1 .. An ]]_t   ==>   case [[ E ]]_t of [[ A1 ]]_t .. [[ An ]]_t 
     154   [[ case E of A1 .. An ]]_t         ==>   case [[ E ]]_t of [[ A1 ]]_t .. [[ An ]]_t 
    151155 
    152    [[ \y1 .. yn -> E ]]_t       ==>   \y1 .. yn -> [[ E ]]_t 
     156   [[ \y1 .. yn -> E ]]_t             ==>   \y1 .. yn -> [[ E ]]_t 
    153157 
    154158Alternatives: 
    155159 
    156    [[ p -> E ]]_t               ==>   p -> [[ E ]]_t  
     160   [[ p -> E ]]_t                     ==>   p -> [[ E ]]_t  
    157161}}} 
    158162