Changes between Version 77 and Version 78 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 5, 2008 6:21:35 AM (6 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