From: Anders <mortberg@chalmers.se>
Date: Wed, 6 May 2015 17:13:01 +0000 (+0200)
Subject: Add check that systems don't contain the same face multiple times in resolver
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=fd6c09cff0438947f8eb314bac6fa4d86e031a67;p=cubicaltt.git

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

diff --git a/Connections.hs b/Connections.hs
index 9a01639..094b3a9 100644
--- 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 e8a2d8d..a3248e6 100644
--- 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 4f8da35..f359fea 100644
--- 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)