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