Changes between Version 77 and Version 78 of TypeFunctionsSolving
 Timestamp:
 Sep 5, 2008 6:21:35 AM (8 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v77 v78 80 80 data RewriteInst  normal equality 81 81 82  !!!TODO: Adapt to new flattening!!! 82 83 norm :: EqInst > [RewriteInst] 83 84 norm [[co :: F s1..sn ~ t]] = [[co :: F s1'..sn' ~ t']] : eqs1++..++eqsn++eqt … … 109 110 check [[co :: T ~ S]] = fail 110 111 111 flatten :: Type > (Type, [RewriteInst]) 112  !!!TODO: Well, we actually only want the coercion for wanteds, locals should stay with id... 113 flatten :: Type > (Type, Coercion, [RewriteInst]) 112 114  Result type has no synonym families whatsoever 113 flatten [[F t1..tn]] = (alpha, [[ id:: F t1'..tn' ~ alpha]] : eqt1++..++eqtn)115 flatten [[F t1..tn]] = (alpha, [[F c1..cn > gamma]], [[gamma :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn) 114 116 where 115 (t1', eqt1) = flatten t1117 (t1', c1, eqt1) = flatten t1 116 118 .. 117 (tn', eqtn) = flatten tn118 FRESH alpha 119 flatten [[t1 t2]] = ( t1' t2', eqs++eqt)119 (tn', cn, eqtn) = flatten tn 120 FRESH alpha, gamma 121 flatten [[t1 t2]] = ([[t1' t2']], [[c1 c2]], eqs++eqt) 120 122 where 121 (t1', eqs) = flatten t1122 (t2', eqt) = flatten t2123 flatten t = (t, [])123 (t1', c1, eqs) = flatten t1 124 (t2', c2, eqt) = flatten t2 125 flatten t = (t, t, []) 124 126 }}} 125 127