Changes between Version 71 and Version 72 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 28, 2008 7:50:59 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v71 v72  
    4747 * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families, 
    4848 * the left-hand side of an equality may not occur in the right-hand side, and 
    49  * the relation `x > y` is a total order on type variables, where `alpha > a` whenever `alpha` is a flexible and `a` a rigid type variable (otherwise, the total order may be aribitrary). 
     49 * the relation `x > y` is an arbitrary, but total order on type variables. 
    5050 
    5151The second bullet of the where clause is trivially true for equalities of Form (1); it also implies that the left- and right-hand sides are different. 
     
    116116    .. 
    117117    (tn', eqtn) = flatten tn 
    118     FRESH alpha, such that alpha > x for all x already used 
    119     RECORD alpha := F t1'..tn' 
     118    FRESH alpha 
    120119flatten [[t1 t2]] = (t1' t2', eqs++eqt) 
    121120  where 
     
    124123flatten t = (t, []) 
    125124}}} 
    126 The substitutions `RECORD`ed during `flatten` need to be (unconditionally) applied during finalisation (i.e., the 3rd phase). 
    127125 
    128126Notes: 
     
    132130 
    133131 
    134 '''TODO:''' We may want to drop the `alpha > x for all x already used` side condition on fresh `alpha`s again.  Instead, we should probably consider all ''local'' flexible variable equalities during finalisation, too.  At least, those involving flexible variables introduced by flattening. 
    135  
    136  
    137132== Propagation (aka Solving) == 
    138133 
     
    159154co1 :: F t1..tn ~ t  &  co2' :: t ~ s with co2 = co1 |> co2' 
    160155}}} 
    161  where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable.  '''SLPJ: why this restriction?  I thought we were treating 
    162 flexible and rigid variables the same.''' 
     156 where `co1` may be a wanted only if `co2` is a wanted, too. 
    163157 
    164158 NB: Afterwards, we need to normalise `co2'`.  Then, the !SubstVarVar or !SubstVarFam rules may apply to the results of normalisation.  Moreover, `co1` may have a !SubstFam or a !SubstVarFam match with rules other than the results of normalising `co2'`. 
     
    170164co1 :: x ~ t  &  co2' :: t ~ s with co2 = co1 |> co2' 
    171165}}} 
    172  where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable. 
     166 where `co1` may be a wanted only if `co2` is a wanted, too. 
    173167 
    174168 NB: Afterwards, we need to normalise `co2'`.  Then, the !SubstVarVar or !SubstVarFam rules may apply to the results of normalisation, but not with `co1`, as `s` and `t` cannot contain `x` -- cf. the definition of normal equalities.  However, `co1` may have another !SubstVarVar or !SubstVarFam match with rules other than the results of normalising `co2'`. 
     
    184178 NB: No normalisation required.  Afterwards, !SubstVarVar or !SubstVarFam may apply to `co1` and all rules, except !SubstVarVar, may apply to `co2'`.  However, !SubstVarFam cannot again apply to `co1` and `co2'`, as `t` cannot contain `x` -- cf. the definition of normal equalities.. 
    185179 
    186 '''SLPJ''': why distinguish SubstVarVar and SubstVarFam.  The paper has only one rule'''. 
    187180 
    188181=== Rule application: specification ===