Changes between Version 79 and Version 80 of TypeFunctionsSolving
 Timestamp:
 Sep 5, 2008 11:07:42 AM (8 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v79 v80 80 80 data RewriteInst  normal equality 81 81 82  !!!TODO: Adapt to new flattening!!!83 82 norm :: EqInst > [RewriteInst] 84 norm [[co :: F s1..sn ~ t]] = adjust [[co :: F s1'..sn' ~ t']] (F c1..cn > sym c) (eqs1++..++eqsn++eqt)83 norm [[co :: F s1..sn ~ t]] = [[co' :: F s1'..sn' ~ t']] : eqs 85 84 where 86 85 (s1', c1, eqs1) = flatten s1 87 86 .. 88 87 (sn', cn, eqsn) = flatten sn 89 (t', c, eqt) = flatten t 88 (t', c, eqt) = flatten t 89 (co', eqs) = adjust co (F c1..cn > sym c) (eqs1++..++eqsn++eqt) 90 90 norm [[co :: t ~ F s1..sn]] = norm [[co' :: F s1..sn ~ t]] with co = sym co' 91 norm [[co :: s ~ t]] = adjust (check [[co :: s' ~ t']]) (cs > sym ct) (eqs ++ eqt)91 norm [[co :: s ~ t]] = check [[co' :: s' ~ t']] ++ eqs 92 92 where 93 93 (s', cs, eqs) = flatten s 94 94 (t', ct, eqt) = flatten t 95 (co', eqs) = adjust co (cs > sym ct) (eqs ++ eqt) 95 96 96 97 check :: FlatEqInst > [RewriteInst] … … 112 113 flatten :: Type > (Type, Coercion, [RewriteInst]) 113 114  Result type has no synonym families whatsoever 114 flatten [[F t1..tn]] = (alpha, [[F c1..cn > gamma]], [[gamma :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn) 115 flatten [[F t1..tn] 116 = (alpha, [[F c1..cn > gamma]], [[gamma :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn) 115 117 where 116 118 (t1', c1, eqt1) = flatten t1 … … 124 126 flatten t = (t, t, []) 125 127 126 adjust :: [RewriteInst] > Coercion > [RewriteInst] > [RewriteInst]128 adjust :: EqInstCo > Coercion > [RewriteInst] > (EqInstCo, [RewriteInst]) 127 129  Adjust coercions depending on whether we process a local or wanted equality 128 adjust ... 130 adjust co co' eqs@[[co1 :: s1 ~ t1, .., con :: sn ~ tn]] 131  isWanted co = (co_new, eqs) with co = co' > co_new 132  otherwise = (co, [[id :: s1 ~ t1, .., id :: sn ~ tn]]) 129 133 }}} 130 134 … … 179 183 co1 :: x ~ t & co2' :: [t/x](F s1..sn) ~ s with co2 = [co1/x](F s1..sn) > co2' 180 184 }}} 181 where `x` occurs in `F s1..sn` . (`co1` may be local or wanted.)185 where `x` occurs in `F s1..sn`, and `co1` may be a wanted only if `co2` is a wanted, too. 182 186 183 187 NB: No normalisation required. Afterwards, !SubstVarVar or !SubstVarFam may apply to `co1` and all rules, except !SubstVarVar, may apply to `co2'`. However, !SubstVarFam cannot again apply to `co1` and `co2'`, as `t` cannot contain `x`  cf. the definition of normal equalities. … … 237 241 == Finalisation == 238 242 243 '''!!!TODO:''' complete the following. 244 239 245 The finalisation step instantiates as many flexible type variables as possible, but it takes care to not to affect variables occurring in the global environment. The latter is important to obtain principle types (c.f., Andrew Kennedy's thesis). Hence, we perform finalisation in two phases: 240 246 1. '''Instantiation:''' For any variable equality of the form `co :: alpha ~ t` or `co :: a ~ alpha`, where `co` is wanted or `alpha` is a variable introduced by flattening, we instantiate `alpha` with `t` or `a`, respectively, and set `co := id`. 241 247 2. '''Substitution:''' For any family equality... 248 249 '''!!!TODO:''' What about unflattening the locals? 242 250 243 251 {{{