Changes between Version 88 and Version 89 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 13, 2008 1:53:55 PM (6 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) ==