Changes between Version 78 and Version 79 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 5, 2008 10:10:29 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
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
     128adjust ...
    126129}}}
    127130