Add check that systems don't contain the same face multiple times in resolver

diff --git a/Connections.hs b/Connections.hs
index 9a01639b3519b17b62fdb62e1a85eb98d3fb8ffc..094b3a9355f960acb191fa824caa8c045245bb9d 100644 (file)
--- a/Connections.hs
+++ b/Connections.hs
@@ -367,10 +367,13 @@ face = Map.foldWithKey (\i d a -> act a (i,Dir d))
 -- the faces should be incomparable
 type System a = Map Face a
 
-showSystem :: Show a => System a -> String
-showSystem ts =
+showListSystem :: Show a => [(Face,a)] -> String
+showListSystem ts =
   "[ " ++ intercalate ", " [ showFace alpha ++ " -> " ++ show u
-                           | (alpha,u) <- Map.toList ts ] ++ " ]"
+                           | (alpha,u) <- ts ] ++ " ]"
+
+showSystem :: Show a => System a -> String
+showSystem = showListSystem . Map.toList
 
 insertSystem :: Face -> a -> System a -> System a
 insertSystem alpha v ts = case find (comparable alpha) (Map.keys ts) of

diff --git a/Resolver.hs b/Resolver.hs
index e8a2d8dc14709f060841bb6d6b8723af72be7c30..a3248e6eeca093663a213bb6a1ea00af9950e86c 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -229,10 +229,14 @@ resolveWhere :: ExpWhere -> Resolver Ter
 resolveWhere = resolveExp . unWhere
 
 resolveSystem :: System -> Resolver (C.System Ter)
-resolveSystem (System ts) =
+resolveSystem (System ts) = do
+  ts' <- sequence [ (,) <$> resolveFace alpha <*> resolveExp u
+                  | Side alpha u <- ts ]
+  let alphas = map fst ts'
+  unless (nub alphas == alphas) $
+    throwError $ "system contains same face multiple times: " ++ C.showListSystem ts'
   -- Note: the symbols in alpha are in scope in u, but they mean 0 or 1
-  Map.fromList <$> sequence [ (,) <$> resolveFace alpha <*> resolveExp u
-                            | Side alpha u <- ts ]
+  return $ Map.fromList ts'
 
 resolveFace :: [Face] -> Resolver C.Face
 resolveFace alpha =

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 4f8da3500c2ad3a67f2500312933cbc8acdab163..f359fead3a15813c76af2197db5265a6c0afaf5a 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -6,6 +6,8 @@ Id (A : U) (a0 a1 : A) : U = IdP (<i> A) a0 a1
 
 refl (A : U) (a : A) : Id A a a = <i> a
 
+testEta (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p p = refl (Id A a b) (<i> p @ i)
+
 mapOnPath (A B : U) (f : A -> B) (a b : A)
           (p : Id A a b) : Id B (f a) (f b) = <i> f (p @ i)