Changes between Version 49 and Version 50 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 16, 2008 4:55:07 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v49 v50  
    6666== Normalisation == 
    6767 
    68 The following function `norm` turns an arbitrary equality into a set of normal equalities.  (It ignores the coercions for the moment.) 
     68The following function `norm` turns an arbitrary equality into a set of normal equalities.  As in `new-single`, the evidence equations are differently interpreted depending on whether we handle a wanted or local equality. 
    6969{{{ 
    7070data EqInst         -- arbitrary equalities 
     
    7373 
    7474norm :: EqInst -> [RewriteInst] 
    75 norm [[F s1..sn ~ t]] = [[F s1'..sn' ~ t']] : eqs1++..++eqsn++eqt 
     75norm [[co :: F s1..sn ~ t]] = [[co :: F s1'..sn' ~ t']] : eqs1++..++eqsn++eqt 
    7676  where 
    7777    (s1', eqs1) = flatten s1 
     
    7979    (sn', eqsn) = flatten sn 
    8080    (t', eqt)   = flatten t 
    81 norm [[t ~ F s1..sn]] = norm [[F s1..sn ~ t]] 
    82 norm [[s ~ t]] = check [[s' ~ t']] : eqs++eqt 
     81norm [[co :: t ~ F s1..sn]] = norm [[co' :: F s1..sn ~ t]] with co = sym co' 
     82norm [[co :: s ~ t]] = check [[co :: s' ~ t']] : eqs++eqt 
    8383  where 
    8484    (s', eqs) = flatten s 
     
    8787check :: FlattenedEqInst -> [FlattenedEqInst] 
    8888-- Does OccursCheck + Decomp + Triv + Swap (of new-single) 
    89 check [[t ~ t]] = [] 
    90 check [[x ~ y]] | x < y = [[x ~ y]] 
    91                 | otherwise = [[y ~ x]] 
    92 check [[x ~ t]] | x `occursIn` t = fail 
    93                 | otherwise = [[x ~ t]] 
    94 check [[t ~ x]] | x `occursIn` t = fail 
    95                 | otherwise = [[x ~ t]] 
    96 check [[s1 s2 ~ t1 t2]] = check [[s1 ~ t1]] ++ check [[s2 ~ t2]] 
    97 check [[T ~ S]] = fail 
     89check [[co :: t ~ t]] = [] with co = id 
     90check [[co :: x ~ y]]  
     91  | x < y     = [[co :: x ~ y]] 
     92  | otherwise = [[co' :: y ~ x]] with co = sym co' 
     93check [[co :: x ~ t]]  
     94  | x `occursIn` t = fail 
     95  | otherwise      = [[co :: x ~ t]] 
     96check [[co :: t ~ x]]  
     97  | x `occursIn` t = fail 
     98  | otherwise      = [[co' :: x ~ t]] with co = sym co' 
     99check [[co :: s1 s2 ~ t1 t2]] 
     100  = check [[col :: s1 ~ t1]] ++ check [[cor :: s2 ~ t2]] with co = col cor 
     101check [[co :: T ~ S]] = fail 
    98102 
    99103flatten :: Type -> (Type, [FlattenedEqInst]) 
    100104-- Result type has no synonym families whatsoever 
    101 flatten [[F t1..tn]] = (alpha, [[F t1'..tn' ~ alpha]] : eqt1++..++eqtn) 
     105flatten [[F t1..tn]] = (alpha, [[id :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn) 
    102106  where 
    103107    (t1', eqt1) = flatten t1 
     
    105109    (tn', eqtn) = flatten tn 
    106110    NEW alpha 
    107     -- also need to add alpha := F t1'..tn' 
     111    RECORD alpha := F t1'..tn' 
    108112flatten [[t1 t2]] = (t1' t2', eqs++eqt) 
    109113  where 
     
    112116flatten t = (t, []) 
    113117}}} 
     118The substitutions `RECORD`ed during `flatten` need to be (unconditionally) applied during finalisation (i.e., the 3rd phase). 
    114119 
    115120Notes: 
     
    117122 * 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.) 
    118123 * 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.) 
    119  * '''TODO:''' Do we need to record a skolem elimination substitution for skolems introduced during flattening for wanteds, too? 
    120124 
    121125