From 3b8b9c8a2f6541cb4047e163060050f909e618fd Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Mon, 4 May 2015 11:27:37 +0200 Subject: [PATCH] move neutrality test in app of a split to a composition --- Eval.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Eval.hs b/Eval.hs index bc44157..3368d1f 100644 --- a/Eval.hs +++ b/Eval.hs @@ -204,9 +204,6 @@ app u v = case (u,v) of (Ter (Split _ _ _ nvs) e,VPCon c _ us phis) -> case lookupBranch c nvs of Just (PBranch _ xs is t) -> eval (subs (upds e (zip xs us)) (zip is phis)) t _ -> error $ "app: missing case in split for " ++ c - (Ter Split{} _,_) | isNeutral v -> VSplit u v - (Ter Split{} _,VCompElem _ _ w _) -> app u w - (Ter Split{} _,VElimComp _ _ w) -> app u w (Ter (Split _ _ ty hbr) e,VComp a w ws) -> case eval e ty of VPi _ f -> let j = fresh (e,v) wsj = Map.map (@@ j) ws @@ -214,6 +211,9 @@ app u v = case (u,v) of ws' = mapWithKey (\alpha -> app (u `face` alpha)) wsj in genComp j (app f (fill j a w wsj)) w' ws' _ -> error $ "app: Split annotation not a Pi type " ++ show u + (Ter Split{} _,_) | isNeutral v -> VSplit u v + (Ter Split{} _,VCompElem _ _ w _) -> app u w + (Ter Split{} _,VElimComp _ _ w) -> app u w (VTrans (VPath i (VPi a f)) li0,vi1) -> let j = fresh (u,vi1) (aj,fj) = (a,f) `swap` (i,j) -- 2.34.1