From: Anders Date: Tue, 21 Apr 2015 09:44:39 +0000 (+0200) Subject: Remove unnecessary argument to addBranch X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=cc96b7d53fc869a31b0305a8ab259c34c096c20a;p=cubicaltt.git Remove unnecessary argument to addBranch --- diff --git a/TypeChecker.hs b/TypeChecker.hs index bebce36..b5544e6 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -74,8 +74,8 @@ addSubs = flip $ foldr addSub addType :: (Ident,Ter) -> TEnv -> TEnv addType (x,a) tenv@(TEnv _ _ rho _) = addTypeVal (x,eval rho a) tenv -addBranch :: [(Ident,Val)] -> (Tele,Env) -> TEnv -> TEnv -addBranch nvs (tele,env) (TEnv k ind rho v) = +addBranch :: [(Ident,Val)] -> Env -> TEnv -> TEnv +addBranch nvs env (TEnv k ind rho v) = TEnv (k + length nvs) ind (upds rho nvs) v addDecls :: [Decl] -> TEnv -> TEnv @@ -107,7 +107,7 @@ constPath :: Val -> Val constPath = VPath (Name "_") mkVars :: Int -> Tele -> Env -> [(Ident,Val)] -mkVars k [] _ = [] +mkVars _ [] _ = [] mkVars k ((x,a):xas) nu = let w = mkVar k x (eval nu a) in (x,w) : mkVars (k+1) xas (Upd nu (x,w)) @@ -296,7 +296,7 @@ checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing () checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do k <- asks index let us = map snd $ mkVars k tele nu - local (addBranch (zip ns us) (tele,nu)) $ check (app f (VCon c us)) e + local (addBranch (zip ns us) nu) $ check (app f (VCon c us)) e checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do k <- asks index mapM_ checkFresh js @@ -305,7 +305,7 @@ checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do js' = map Atom js vts = evalSystem (subs (upds nu us) (zip is js')) ts vfts = intersectionWith app (border g ts) vts - local (addSubs (zip js js') . addBranch (zip ns vus) (tele,nu)) $ do + local (addSubs (zip js js') . addBranch (zip ns vus) nu) $ do check (app f (VPCon c va vus js')) e ve <- evalTyping e -- TODO: combine with next line? unlessM (border ve ts === vfts) $