Changes between Version 77 and Version 78 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 5, 2008 6:21:35 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v77 v78  
    8080data RewriteInst    -- normal equality
    8181
     82-- !!!TODO: Adapt to new flattening!!!
    8283norm :: EqInst -> [RewriteInst]
    8384norm [[co :: F s1..sn ~ t]] = [[co :: F s1'..sn' ~ t']] : eqs1++..++eqsn++eqt
     
    109110check [[co :: T ~ S]] = fail
    110111
    111 flatten :: Type -> (Type, [RewriteInst])
     112-- !!!TODO: Well, we actually only want the coercion for wanteds, locals should stay with id...
     113flatten :: Type -> (Type, Coercion, [RewriteInst])
    112114-- Result type has no synonym families whatsoever
    113 flatten [[F t1..tn]] = (alpha, [[id :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn)
     115flatten [[F t1..tn]] = (alpha, [[F c1..cn |> gamma]], [[gamma :: F t1'..tn' ~ alpha]] : eqt1++..++eqtn)
    114116  where
    115     (t1', eqt1) = flatten t1
     117    (t1', c1, eqt1) = flatten t1
    116118    ..
    117     (tn', eqtn) = flatten tn
    118     FRESH alpha
    119 flatten [[t1 t2]] = (t1' t2', eqs++eqt)
     119    (tn', cn, eqtn) = flatten tn
     120    FRESH alpha, gamma
     121flatten [[t1 t2]] = ([[t1' t2']], [[c1 c2]], eqs++eqt)
    120122  where
    121     (t1', eqs) = flatten t1
    122     (t2', eqt) = flatten t2
    123 flatten t = (t, [])
     123    (t1', c1, eqs) = flatten t1
     124    (t2', c2, eqt) = flatten t2
     125flatten t = (t, t, [])
    124126}}}
    125127