Changes between Version 71 and Version 72 of TypeFunctionsSolving
 Timestamp:
 Aug 28, 2008 7:50:59 AM (7 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v71 v72 47 47 * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families, 48 48 * the lefthand side of an equality may not occur in the righthand 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. 50 50 51 51 The second bullet of the where clause is trivially true for equalities of Form (1); it also implies that the left and righthand sides are different. … … 116 116 .. 117 117 (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 120 119 flatten [[t1 t2]] = (t1' t2', eqs++eqt) 121 120 where … … 124 123 flatten t = (t, []) 125 124 }}} 126 The substitutions `RECORD`ed during `flatten` need to be (unconditionally) applied during finalisation (i.e., the 3rd phase).127 125 128 126 Notes: … … 132 130 133 131 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 137 132 == Propagation (aka Solving) == 138 133 … … 159 154 co1 :: F t1..tn ~ t & co2' :: t ~ s with co2 = co1 > co2' 160 155 }}} 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. 163 157 164 158 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'`. … … 170 164 co1 :: x ~ t & co2' :: t ~ s with co2 = co1 > co2' 171 165 }}} 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. 173 167 174 168 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'`. … … 184 178 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.. 185 179 186 '''SLPJ''': why distinguish SubstVarVar and SubstVarFam. The paper has only one rule'''.187 180 188 181 === Rule application: specification ===