Changes between Version 50 and Version 51 of TypeFunctionsSolving

Show
Ignore:
Timestamp:
08/15/08 21:58:45 (5 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • TypeFunctionsSolving

    v50 v51  
    108108    .. 
    109109    (tn', eqtn) = flatten tn 
    110     NEW alpha 
     110    FRESH alpha 
    111111    RECORD alpha := F t1'..tn' 
    112112flatten [[t1 t2]] = (t1' t2', eqs++eqt) 
    … …  
    121121 * Perform Rule Triv as part of normalisation. 
    122122 * 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.) 
    123  * Use flexible tyvars for flattening of locals, too.  (We have flexibles in locals anyway and don't use (Unify) on locals, so the flexibles shouldn't cause any harm, but the elimination of skolems is much easier for flexibles - we just instantiate them.) 
     123 * We flatten locals and wanteds in the same manner, using fresh flexible type variables.  (We have flexibles in locals anyway and don't use (Unify) during normalisation - this is different to new-single.) 
    124124 
    125125