From: Anders Date: Mon, 11 May 2015 12:18:24 +0000 (+0200) Subject: Fix the bug in transport and add optimizations to compElem and elimComp X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=fd124da780ddf5eb6306f014f58fa9aec3b2f220;p=cubicaltt.git Fix the bug in transport and add optimizations to compElem and elimComp --- diff --git a/Eval.hs b/Eval.hs index b24a98a..594e9bb 100644 --- a/Eval.hs +++ b/Eval.hs @@ -324,6 +324,8 @@ trans i v0 v1 = case (v0,v1) of " in " ++ show v0 _ | isNeutral w -> w where w = VTrans (VPath i v0) v1 + (Ter (Sum _ _ nass) env,VElimComp _ _ u) -> trans i v0 u + (Ter (Sum _ _ nass) env,VCompElem _ _ u _) -> trans i v0 u (VGlue a ts,_) -> transGlue i a ts v1 (VGlueLine a phi psi,_) -> transGlueLine i a phi psi v1 (VComp VU a es,_) -> transU i a es v1 @@ -694,15 +696,21 @@ auxTransGlueLine i (phi,b,wi0) vi1 = fillLine (b `face` (i ~> 1)) vi1 ls' ------------------------------------------------------------------------------- -- | Composition in the Universe +isConstPath :: Val -> Bool +isConstPath (VPath i u) = i `notElem` support u +isConstPath _ = False + compElem :: Val -> System Val -> Val -> System Val -> Val -compElem a es u us | Map.null es = u - | eps `Map.member` us = us ! eps - | otherwise = VCompElem a es u us - -elimComp ::Val -> System Val -> Val -> Val -elimComp a es u | Map.null es = u - | eps `Map.member` es = transNegLine (es ! eps) u - | otherwise = VElimComp a es u +compElem a es u us = compElem' (Map.filter (not . isConstPath) es) + where compElem' es | Map.null es = u + | eps `Map.member` us = us ! eps + | otherwise = VCompElem a es u us + +elimComp :: Val -> System Val -> Val -> Val +elimComp a es u = elimComp' (Map.filter (not . isConstPath) es) + where elimComp' es | Map.null es = u + | eps `Map.member` es = transNegLine (es ! eps) u + | otherwise = VElimComp a es u compU :: Name -> Val -> System Val -> Val -> System Val -> Val compU i a es w0 ws =