Changes between Version 14 and Version 15 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 30, 2008 3:32:26 PM (6 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