From 74ebf46412a322712efc3658196ec2404faa663c Mon Sep 17 00:00:00 2001 From: coquand Date: Sun, 27 Dec 2015 09:59:19 +0100 Subject: [PATCH] neutral for compU --- Eval.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Eval.hs b/Eval.hs index 6aa2d6b..585d80e 100644 --- a/Eval.hs +++ b/Eval.hs @@ -292,7 +292,7 @@ comp i a u ts = case a of comp_u2 = comp i (app f fill_u1) u2 t2s VPi{} -> VComp (VPath i a) u (Map.map (VPath i) ts) VU -> compUniv u (Map.map (VPath i) ts) - VCompU a es -> compU i a es u ts + VCompU a es | not (isNeutralU i es u ts) -> compU i a es u ts VGlue b equivs | not (isNeutralGlue i equivs u ts) -> compGlue i b equivs u ts Ter (Sum _ _ nass) env -> case u of VCon n us | all isCon (elems ts) -> case lookupLabel n nass of @@ -499,6 +499,12 @@ isNeutralGlue i equivs u0 ts = (eps `notMember` equivsi0 && isNeutral u0) || (assocs ts) where equivsi0 = equivs `face` (i ~> 0) +isNeutralU :: Name -> System Val -> Val -> System Val -> Bool +isNeutralU i eqs u0 ts = (eps `notMember` eqsi0 && isNeutral u0) || + any (\(alpha,talpha) -> + eps `notMember` (eqs `face` alpha) && isNeutral talpha) + (assocs ts) + where eqsi0 = eqs `face` (i ~> 0) -- Extend the system ts to a total element in b given q : isContr b extend :: Val -> Val -> System Val -> Val -- 2.34.1