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 ===