Fix a TODO in the resolver (the arguments in a path constructors cannot refer to...

diff --git a/Resolver.hs b/Resolver.hs
index 3672dfcd51f69b641fef7f99ead3c1f660bf8b19..bbca155d292379588af5bbf59f245c0e1b639bf6 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -8,7 +8,7 @@ import Control.Monad
 import Control.Monad.Reader
 import Control.Monad.Except
 import Control.Monad.Identity
-import Data.List (nub)
+import Data.List
 import Data.Map (Map,(!))
 import qualified Data.Map as Map
 
@@ -52,7 +52,6 @@ unAppsFormulas (AppFormula u phi) phis = unAppsFormulas u (phi:phis)
 unAppsFormulas u phis = (x,xs,phis)
   where (x,xs) = unApps u []
 
-
 -- Flatten a tele
 flattenTele :: [Tele] -> [(Ident,Exp)]
 flattenTele tele =
@@ -253,7 +252,7 @@ resolveBranch (OBranch (AIdent (_,lbl)) args e) = do
   re <- local (insertAIdents args) $ resolveWhere e
   return $ CTT.OBranch lbl (map unAIdent args) re
 resolveBranch (PBranch (AIdent (_,lbl)) args is e) = do
-  re    <- local (insertNames is . insertAIdents args) $ resolveWhere e
+  re <- local (insertNames is . insertAIdents args) $ resolveWhere e
   let names = map (C.Name . unAIdent) is
   return $ CTT.PBranch lbl (map unAIdent args) names re
 
@@ -269,11 +268,11 @@ resolveLabel cs (PLabel n vdecl is sys) = do
   let tele' = flattenTele vdecl
       ts    = map fst tele'
       names = map (C.Name . unAIdent) is
-  -- TODO: the system should *not* know about n; remove n before
-  -- inserting cs
-  CTT.PLabel (unAIdent n) <$> resolveTele tele' <*> pure names
-    <*> local (insertNames is . insertIdents cs . insertVars ts)
-              (resolveSystem sys)
+      n'    = unAIdent n
+      cs'   = delete (n',PConstructor) cs
+  CTT.PLabel n' <$> resolveTele tele' <*> pure names
+                <*> local (insertNames is . insertIdents cs' . insertVars ts)
+                      (resolveSystem sys)
 
 -- Resolve Data or Def or Split declarations
 resolveDecl :: Decl -> Resolver (CTT.Decl,[(Ident,SymKind)])