From: Simon Huber Date: Tue, 24 Mar 2015 17:18:58 +0000 (+0100) Subject: bugfix in trans X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f517f9e6b8106844d1aebe79c8fea10754b7a39d;p=cubicaltt.git bugfix in trans --- diff --git a/Eval.hs b/Eval.hs index 37ffa34..43bdeaa 100644 --- a/Eval.hs +++ b/Eval.hs @@ -244,6 +244,7 @@ transNegLine u v = transNeg i (u @@ i) v where i = fresh (u,v) trans :: Name -> Val -> Val -> Val +trans i v0 v1 | i `notElem` support v0 = v1 trans i v0 v1 = case (v0,v1) of (VIdP a u v,w) -> let j = fresh (Atom i, v0, w) @@ -262,7 +263,8 @@ trans i v0 v1 = case (v0,v1) of _ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1 (VGlue a ts,_) -> transGlue i a ts v1 (VComp VU a es,_) -> transU i a es v1 - _ | otherwise -> error "trans not implemented" + _ | otherwise -> error $ "trans not implemented for v0 = " ++ show v0 + ++ "\n and v1 = " ++ show v1 transNeg :: Name -> Val -> Val -> Val transNeg i a u = trans i (a `sym` i) u @@ -357,7 +359,7 @@ genComp i a u ts | Map.null ts = trans i a u genComp i a u ts = comp i ai1 (trans i a u) ts' where ai1 = a `face` (i ~> 1) j = fresh (a,Atom i,ts,u) - comp' alpha u = VPath i (trans j ((a `face` alpha) `disj` (i,j)) u) + comp' alpha u = trans j ((a `face` alpha) `disj` (i,j)) u ts' = mapWithKey comp' ts genCompNeg i a u ts = genComp i (a `sym` i) u (ts `sym` i)