Changes between Version 49 and Version 50 of TypeFunctionsSolving
 Timestamp:
 Aug 16, 2008 4:55:07 AM (8 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v49 v50 66 66 == Normalisation == 67 67 68 The following function `norm` turns an arbitrary equality into a set of normal equalities. (It ignores the coercions for the moment.)68 The following function `norm` turns an arbitrary equality into a set of normal equalities. As in `newsingle`, the evidence equations are differently interpreted depending on whether we handle a wanted or local equality. 69 69 {{{ 70 70 data EqInst  arbitrary equalities … … 73 73 74 74 norm :: EqInst > [RewriteInst] 75 norm [[ F s1..sn ~ t]] = [[F s1'..sn' ~ t']] : eqs1++..++eqsn++eqt75 norm [[co :: F s1..sn ~ t]] = [[co :: F s1'..sn' ~ t']] : eqs1++..++eqsn++eqt 76 76 where 77 77 (s1', eqs1) = flatten s1 … … 79 79 (sn', eqsn) = flatten sn 80 80 (t', eqt) = flatten t 81 norm [[ t ~ F s1..sn]] = norm [[F s1..sn ~ t]]82 norm [[ s ~ t]] = check [[s' ~ t']] : eqs++eqt81 norm [[co :: t ~ F s1..sn]] = norm [[co' :: F s1..sn ~ t]] with co = sym co' 82 norm [[co :: s ~ t]] = check [[co :: s' ~ t']] : eqs++eqt 83 83 where 84 84 (s', eqs) = flatten s … … 87 87 check :: FlattenedEqInst > [FlattenedEqInst] 88 88  Does OccursCheck + Decomp + Triv + Swap (of newsingle) 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 89 check [[co :: t ~ t]] = [] with co = id 90 check [[co :: x ~ y]] 91  x < y = [[co :: x ~ y]] 92  otherwise = [[co' :: y ~ x]] with co = sym co' 93 check [[co :: x ~ t]] 94  x `occursIn` t = fail 95  otherwise = [[co :: x ~ t]] 96 check [[co :: t ~ x]] 97  x `occursIn` t = fail 98  otherwise = [[co' :: x ~ t]] with co = sym co' 99 check [[co :: s1 s2 ~ t1 t2]] 100 = check [[col :: s1 ~ t1]] ++ check [[cor :: s2 ~ t2]] with co = col cor 101 check [[co :: T ~ S]] = fail 98 102 99 103 flatten :: Type > (Type, [FlattenedEqInst]) 100 104  Result type has no synonym families whatsoever 101 flatten [[F t1..tn]] = (alpha, [[ F t1'..tn' ~ alpha]] : eqt1++..++eqtn)105 flatten [[F t1..tn]] = (alpha, [[id :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn) 102 106 where 103 107 (t1', eqt1) = flatten t1 … … 105 109 (tn', eqtn) = flatten tn 106 110 NEW alpha 107  also need to addalpha := F t1'..tn'111 RECORD alpha := F t1'..tn' 108 112 flatten [[t1 t2]] = (t1' t2', eqs++eqt) 109 113 where … … 112 116 flatten t = (t, []) 113 117 }}} 118 The substitutions `RECORD`ed during `flatten` need to be (unconditionally) applied during finalisation (i.e., the 3rd phase). 114 119 115 120 Notes: … … 117 122 * 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 righthand sides do not contain synonym familles; hence, any recursive occurrences of a lefthand side imply that the equality is unsatisfiable.) 118 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.) 119 * '''TODO:''' Do we need to record a skolem elimination substitution for skolems introduced during flattening for wanteds, too?120 124 121 125