Changes between Version 11 and Version 12 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 23, 2008 9:20:02 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v11 v12  
    2121== Normalisation ==
    2222
     23(Ignoring the coercions for the moment.)
     24
     25{{{
     26norm [[F s1..sn ~ t]] = [[F s1'..sn' ~ t']] : eqs1++..++eqsn++eqt
     27  where
     28    (s1', eqs1) = flatten s1
     29    ..
     30    (sn', eqsn) = flatten sn
     31    (t', eqt)   = flatten t
     32norm [[t ~ F s1..sn]] = norm [[F s1..sn ~ t]]
     33norm [[s ~ t]] = check [[s' ~ t']] : eqs++eqt
     34  where
     35    (s', eqs) = flatten s
     36    (t', eqt) = flatten t
     37
     38check [[t ~ t]] = []
     39check [[x ~ t]] | x `occursIn` t = fail
     40                          | otherwise = [[x ~ t]]
     41check [[t ~ x]] | x `occursIn` t = fail
     42                          | otherwise = [[x ~ t]]
     43check [[a ~ t]] | a `occursIn` t = fail
     44                          | otherwise = [[a ~ t]]
     45check [[t ~ a]] | a `occursIn` t = fail
     46                          | otherwise = [[a ~ t]]
     47check [[s1 s2 ~ t1 t2]] = check [[s1 ~ t1]] ++ check [[s2 ~ t2]]
     48check [[T ~ S]] = fail
     49
     50flatten [[F t1..tn]] = (x, [[F t1'..tn' ~ x]] : eqt1++..++eqtn)
     51  where
     52    (t1', eqt1) = flatten t1
     53    ..
     54    (tn', eqtn) = flatten tn
     55    NEW x
     56    -- also need to add x := F t1'..tn'
     57flatten [[t1 t2]] = (t1' t2', eqs++eqt)
     58  where
     59    (t1', eqs) = flatten t1
     60    (t2', eqt) = flatten t2
     61flatten t = (t, [])
     62}}}
     63
     64Notes:
    2365 * Perform Rule Triv as part of normalisation.
    2466 * Whenever an equality of Form (2) or (3) would be recursive, the program can be rejected on the basis of a failed occurs check.  (Immediate rejection is always justified, as right-hand sides do not contain synonym familles; hence, any recursive occurrences of a left-hand side imply that the equality is unsatisfiable.)