Changes between Version 93 and Version 94 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 16, 2008 5:37:20 AM (7 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}}}