Changes between Version 6 and Version 7 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 23, 2008 4:18:09 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v6 v7  
    5757}}} 
    5858 
     59Same, but de-prioritise (Local) - i.e., (Local) applies only if nothing else does: 
    5960{{{ 
    60   v ~ [x], F v ~ x 
     61[F v] ~ v  ||-  [F v] ~ v 
     62==> normalise 
     63v ~ [a], F v ~ a  ||-  v ~ [x], F v ~ x 
     64a := F v 
     65==> (IdenticalLHS) with v & F v 
     66v ~ [a], F v ~ a  ||- [a] ~ [x], x ~ a 
     67==> normalise 
     68v ~ [a], F v ~ a  ||-  x ~ a, x ~ a 
     69==> (Unify) 
     70v ~ [a], F v ~ a  ||-  a ~ a 
     71==> normalise 
     72v ~ [a], F v ~ a ||- 
     73QED 
     74}}} 
     75 
     76Derivation our modified rules: 
     77{{{ 
     78[F v] ~ v  ||-  [F v] ~ v 
     79==> normalise 
     80v ~ [x2], F v ~ x2  ||-  v ~ [x1], F v ~ x1 
     81** x2 := F v 
    6182==> (Local) with v 
    62   v ~ [x], F [a] ~ x 
    63 ==> (Top) 
    64   v ~ [x], x ~ [F x] 
    65 ===> normalise 
    66   v ~ [x], x ~ [y], F x ~ y 
     83F [x2] ~ x2  ||-  [x2] ~ [x1], F [x2] ~ x1 
     84** x2 := F v 
     85==> normalise 
     86F [x2] ~ x2  ||-  x2 ~ x1, F [x2] ~ x1 
     87** x2 := F v 
     88==> 2x (Top) & Unify 
     89[F x1] ~ x1  ||-  [F x1] ~ x1 
     90** x1 := F v 
     91==> normalise 
     92x1 ~ [y2], F x1 ~ y2  ||-  x1 ~ [y1], F x1 ~ y1 
     93** x1 := F v, y2 := F x1 
     94..we stop here if (Local) doesn't apply to flexible tyvars 
    6795}}} 
     96