# Changes between Version 11 and Version 12 of TypeFunctionsSolving

Show
Ignore:
Timestamp:
07/23/08 02:20:02 (5 years ago)
Comment:

--

Unmodified
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.)