Changes between Version 14 and Version 15 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 30, 2008 3:32:26 PM (7 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v14 v15  
    2828
    2929{{{
     30--    EqInst             Arbitrary equalities
     31--    FlattenedEqInst    Any type function application is at the top
     32--    RewriteInst        Satisfies invariants above
     33
     34norm :: EqInst -> [RewriteInst]
    3035norm [[F s1..sn ~ t]] = [[F s1'..sn' ~ t']] : eqs1++..++eqsn++eqt
    3136  where
     
    4045    (t', eqt) = flatten t
    4146
     47check :: FlattenedEqInst -> [FlattenedEqInst]
     48-- Does occurs-checks + decomposition
    4249check [[t ~ t]] = []
    4350check [[x ~ t]] | x `occursIn` t = fail
     
    5259check [[T ~ S]] = fail
    5360
     61flatten :: EqInst -> (FlattenedEqInst, [FlattenedEqInst])
    5462flatten [[F t1..tn]] = (x, [[F t1'..tn' ~ x]] : eqt1++..++eqtn)
    5563  where