Changes between Version 25 and Version 26 of ExplicitCallStack


Ignore:
Timestamp:
Jan 29, 2007 4:58:52 PM (9 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