Changes between Version 93 and Version 94 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 16, 2008 5:37:20 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v93 v94  
    8787    (sn', cn, eqsn) = flatten sn 
    8888    (t', c, eqt)    = flatten t 
    89     (co', eqs)      = adjust co (F c1..cn |> sym c) (eqs1++..++eqsn++eqt) 
     89    (co', eqs)      = adjust co (F c1..cn) (sym c) (eqs1++..++eqsn++eqt) 
    9090norm [[co :: t ~ F s1..sn]] = norm [[co' :: F s1..sn ~ t]] with co = sym co' 
    9191norm [[co :: s ~ t]] = check [[co' :: s' ~ t']] ++ eqs 
     
    9393    (s', cs, eqs) = flatten s 
    9494    (t', ct, eqt) = flatten t 
    95     (co', eqs)    = adjust co (cs |> sym ct) (eqs ++ eqt) 
     95    (co', eqs)    = adjust co cs (sym ct) (eqs ++ eqt) 
    9696 
    9797check :: FlatEqInst -> [RewriteInst] 
     
    127127flatten t = (t, t, []) 
    128128 
    129 adjust :: EqInstCo -> Coercion -> [RewriteInst] -> (EqInstCo, [RewriteInst]) 
     129adjust :: EqInstCo -> Coercion -> Coercion -> [RewriteInst] -> (EqInstCo, [RewriteInst]) 
    130130-- Adjust coercions depending on whether we process a local or wanted equality 
    131 adjust co co' eqs@[[co1 :: s1 ~ t1, .., con :: sn ~ tn]] 
    132   | isWanted co = (co_new, eqs) with co = co' |> co_new 
     131adjust co co1 co2 eqs@[[co1 :: s1 ~ t1, .., con :: sn ~ tn]] 
     132  | isWanted co = (co_new, eqs) with co = co1 |> co_new |> co2 
    133133  | otherwise   = (co, [[id :: s1 ~ t1, .., id :: sn ~ tn]]) 
    134134}}}