From: Simon Huber <hubsim@gmail.com>
Date: Thu, 10 Sep 2015 12:40:47 +0000 (+0200)
Subject: Rename Simple into NonMutual and added sanity check
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=5d3240eaabd6cb432cf3a510e174d5c0c687f6b7;p=cubicaltt.git

Rename Simple into NonMutual and added sanity check
---

diff --git a/Resolver.hs b/Resolver.hs
index dd5e803..4969235 100644
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -272,11 +272,11 @@ resolveLabel cs (PLabel n vdecl is sys) = do
                 <*> local (insertNames is . insertIdents cs' . insertVars ts)
                       (resolveSystem sys)
 
--- Resolve a simple declaration (not mutual); returns resolver for
--- type and body separately
-resolveSimpleDecl :: Decl -> (Ident,Resolver CTT.Ter
-                             ,Resolver CTT.Ter,[(Ident,SymKind)])
-resolveSimpleDecl d = case d of
+-- Resolve a non-mutual declaration; returns resolver for type and
+-- body separately
+resolveNonMutualDecl :: Decl -> (Ident,Resolver CTT.Ter
+                                ,Resolver CTT.Ter,[(Ident,SymKind)])
+resolveNonMutualDecl d = case d of
   DeclDef (AIdent (_,f)) tele t body ->
     let tele' = flattenTele tele
         a     = binds CTT.Pi tele' (resolveExp t)
@@ -319,15 +319,17 @@ resolveRTele (i:is) (t:ts) = do
 resolveDecl :: Decl -> Resolver ([CTT.Decl],[(Ident,SymKind)])
 resolveDecl d = case d of
   DeclMutual decls -> do
-    let (fs,ts,bs,nss) = unzip4 $ map resolveSimpleDecl decls
+    let (fs,ts,bs,nss) = unzip4 $ map resolveNonMutualDecl decls
         ns = concat nss -- TODO: some sanity checks? Duplicates!?
+    when (nub (map fst ns) /= concatMap (map fst) nss) $
+      throwError ("Duplicated constructor or ident: " ++ show nss)
     as <- resolveRTele fs ts
     -- The bodies know about all the names and constructors in the
     -- mutual block
     ds <- sequence $ map (local (insertIdents ns)) bs
     let ads = zipWith (\ (x,y) z -> (x,(y,z))) as ds
     return (ads,ns)
-  _ -> do let (f,typ,body,ns) = resolveSimpleDecl d
+  _ -> do let (f,typ,body,ns) = resolveNonMutualDecl d
           a <- typ
           d <- body
           return ([(f,(a,d))],ns)