Changes between Version 6 and Version 7 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 23, 2008 4:18:09 AM (7 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