Changes between Version 11 and Version 12 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 23, 2008 9:20:02 AM (6 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.)