Changes between Version 88 and Version 89 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 13, 2008 1:53:55 PM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v88 v89  
    120120    (tn', cn, eqtn) = flatten tn
    121121    FRESH alpha, gamma
     122    RECORD alpha := F t1..tn IF local equality
    122123flatten [[t1 t2]] = ([[t1' t2']], [[c1 c2]], eqs++eqt)
    123124  where
     
    136137 * Perform Rule Triv & Decomp as part of normalisation.
    137138 * Whenever an equality of Form (2) or (3) would be recursive, the program can be rejected on the basis of a failed occurs check.  (Immediate rejection is always justified, as right-hand sides do not contain synonym familles; hence, any recursive occurrences of a left-hand side imply that the equality is unsatisfiable.)
     139 * For all local equalities, we `RECORD` substitutions for fresh flexibles introduced by `flatten` by already updating the meta type variable.  However, the update will only have an effect after the Insts have been zonked; i.e., after finalisation.
     140 * We do the essentially same for class constraints; i.e., we use `flatten` to extract all family applications as equality constraints.  However, instead of adjusting the coercion at the flattened constraint, we generate a dictionary binding for the new dictionary (using a cast expression).
    138141
    139142== Propagation (aka Solving) ==