Changes between Version 49 and Version 50 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 16, 2008 4:55:07 AM (7 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