Changes between Version 20 and Version 21 of NestedCPR


Ignore:
Timestamp:
Jan 9, 2014 12:39:58 PM (14 months ago)
Author:
nomeata
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NestedCPR

    v20 v21  
    5555For the implementation this implies that we need to be careful when `lub`’ing: If one branch is lazy, but not absent in an argument or free variable), and the other branch is strict, then even if both branches claim to terminate, we need to remove the termination flag (as one had the termination under a stronger hypothesis as the hole result) (Feels inelegant.) 
    5656 
    57 When evaluating a demand type as a demand transformer, we need to compare the convergence flags of the argument expressions with the strictness demands, and possibly adjust the termination information. 
     57Similar thought needs to be considered whenever one goes up in the lattice (better always go up by using `lub` then...) 
    5858 
    59 What about nested strictness annotations? For now the hypothesis only requires the arguments (and free variables) to be terminating; if there is a `<S(S)>`, then it should not be marked as converging. Maybe this can be improved later, using nested CPR. 
     59In pictures: This is the lattice, which is not a simple product lattice any more: 
     60{{{ 
     61       ------ <L><L>------ 
     62     /          | \       \ 
     63    /           | <L><L>t  \ 
     64<S><L>          |           <S><L>   
     65 |  \ \         |           |  |  \ 
     66 |   \ <S><L>t  |          /   |   <S><L>t  
     67 |    \         |         /    | 
     68 \     \        |        /     |   
     69  \     ----- <S><S>-----      |  
     70   \           |    \          | 
     71    \          |     <S><S>t   / 
     72     \         |              / 
     73      ---------D-------------/ 
     74}}} 
    6075 
    61  2. For the second one, we’d need a different `both` for functions and case-expressions: For function applications, convergence in the first argument is not affected by (possible) divergence in the second argument. For case expressions, it has to be! Also, data constructors with strict fields, including `I# _` must not be terminating...sounds like a show-stopper. 
    6276 
    63 What is the semantics for bottom? 
     77When evaluating a demand type as a demand transformer, we need to compare the convergence flags of the argument expressions with the strictness demands, and possibly adjust the termination information. I believe can be done using `deferAndUse` as before. 
     78 
     79What about nested strictness annotations? For now the hypothesis of the demand transformer only requires the arguments (and free variables) to be terminating; if there is a `<S(S)>`, then it should not be marked as converging. Maybe this can be improved later, using nested CPR. 
    6480 
    6581=== join points ===