From: Anders <mortberg@chalmers.se>
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) $