# Changes between Version 78 and Version 79 of TypeFunctionsSolving

Show
Ignore:
Timestamp:
09/05/08 03:10:29 (5 years ago)
Comment:

--

Unmodified
Removed
Modified
• ## TypeFunctionsSolving

v78 v79
8282-- !!!TODO: Adapt to new flattening!!!
8383norm :: EqInst -> [RewriteInst]
84 norm [[co :: F s1..sn ~ t]] = [[co :: F s1'..sn' ~ t']] : eqs1++..++eqsn++eqt
84norm [[co :: F s1..sn ~ t]] = adjust [[co :: F s1'..sn' ~ t']] (F c1..cn |> sym c) (eqs1++..++eqsn++eqt)
8585  where
86     (s1', eqs1) = flatten s1
86    (s1', c1, eqs1) = flatten s1
8787    ..
88     (sn', eqsn) = flatten sn
89     (t', eqt)   = flatten t
88    (sn', cn, eqsn) = flatten sn
89    (t', c, eqt)   = flatten t
9090norm [[co :: t ~ F s1..sn]] = norm [[co' :: F s1..sn ~ t]] with co = sym co'
91 norm [[co :: s ~ t]] = check [[co :: s' ~ t']] ++ eqs ++ eqt
91norm [[co :: s ~ t]] = adjust (check [[co :: s' ~ t']]) (cs |> sym ct) (eqs ++ eqt)
9292  where
93     (s', eqs) = flatten s
94     (t', eqt) = flatten t
93    (s', cs, eqs) = flatten s
94    (t', ct, eqt) = flatten t
9595
9696check :: FlatEqInst -> [RewriteInst]

110110check [[co :: T ~ S]] = fail
111111
112 -- !!!TODO: Well, we actually only want the coercion for wanteds, locals should stay with id...
113112flatten :: Type -> (Type, Coercion, [RewriteInst])
114113-- Result type has no synonym families whatsoever

124123    (t2', c2, eqt) = flatten t2
125124flatten t = (t, t, [])
125
126adjust :: [RewriteInst] -> Coercion -> [RewriteInst] -> [RewriteInst]
127-- Adjust coercions depending on whether we process a local or wanted equality