Changes between Version 78 and Version 79 of TypeFunctionsSolving

Timestamp:

09/05/08 03:10:29 (5 years ago)

Author:

chak

Comment:

--

TypeFunctionsSolving

@@ -82 +82 @@
 -- !!!TODO: Adapt to new flattening!!!
 norm :: EqInst -> [RewriteInst]
-norm [[co :: F s1..sn ~ t]] = [[co :: F s1'..sn' ~ t']] : eqs1++..++eqsn++eqt
+norm [[co :: F s1..sn ~ t]] = adjust [[co :: F s1'..sn' ~ t']] (F c1..cn |> sym c) (eqs1++..++eqsn++eqt)
   where
-    (s1', eqs1) = flatten s1
+    (s1', c1, eqs1) = flatten s1
     ..
-    (sn', eqsn) = flatten sn
-    (t', eqt)   = flatten t
+    (sn', cn, eqsn) = flatten sn
+    (t', c, eqt)   = flatten t
 norm [[co :: t ~ F s1..sn]] = norm [[co' :: F s1..sn ~ t]] with co = sym co'
-norm [[co :: s ~ t]] = check [[co :: s' ~ t']] ++ eqs ++ eqt
+norm [[co :: s ~ t]] = adjust (check [[co :: s' ~ t']]) (cs |> sym ct) (eqs ++ eqt)
   where
-    (s', eqs) = flatten s
-    (t', eqt) = flatten t
+    (s', cs, eqs) = flatten s
+    (t', ct, eqt) = flatten t
 
 check :: FlatEqInst -> [RewriteInst]
@@ -110 +110 @@
 check [[co :: T ~ S]] = fail
 
--- !!!TODO: Well, we actually only want the coercion for wanteds, locals should stay with id...
 flatten :: Type -> (Type, Coercion, [RewriteInst])
 -- Result type has no synonym families whatsoever
@@ -124 +123 @@
     (t2', c2, eqt) = flatten t2
 flatten t = (t, t, [])
+
+adjust :: [RewriteInst] -> Coercion -> [RewriteInst] -> [RewriteInst]
+-- Adjust coercions depending on whether we process a local or wanted equality
+adjust ...
 }}}