Reintroduced mutual (wip)

diff --git a/Exp.cf b/Exp.cf
index db7234face5a359b2e1076f07a6fcca34cd9eafb..6b71f3011e8f9a2488d5aa8d58722a6ab3b3e86f 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -3,7 +3,7 @@ entrypoints Module, Exp ;
 comment "--" ;
 comment "{-" "-}" ;
 
-layout "where", "let", "split" ;
+layout "where", "let", "split", "mutual" ;
 layout stop "in" ;
 -- Do not use layout toplevel as it makes pExp fail!
 
@@ -16,7 +16,7 @@ DeclDef.    Decl ::= AIdent [Tele] ":" Exp "=" ExpWhere ;
 DeclData.   Decl ::= "data" AIdent [Tele] "=" [Label] ;
 DeclSplit.  Decl ::= AIdent [Tele] ":" Exp "=" "split" "{" [Branch] "}" ;
 DeclUndef.  Decl ::= AIdent [Tele] ":" Exp "=" "undefined" ;
--- DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ;
+DeclMutual. Decl ::= "mutual" "{" [Decl] "}" ;
 separator   Decl ";" ;
 
 Where.    ExpWhere ::= Exp "where" "{" [Decl] "}" ;

diff --git a/Resolver.hs b/Resolver.hs
index f3738d455741a0bb52b06bb0680c950b1d00df75..dd5e803e209f8eacb3e979e5eb63125865386363 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -136,12 +136,13 @@ resolveVar (AIdent (l,x)) = do
   case lookup x vars of
     Just Variable    -> return $ CTT.Var x
     Just Constructor -> return $ CTT.Con x []
-    Just PConstructor -> throwError $ "The path constructor " ++ x ++ " is used as a"
-                                   ++ " variable at " ++ show l ++ " in " ++ modName
-                                   ++ " (path constructors should have their type in"
-                                   ++ " curly braces as first argument)"
+    Just PConstructor ->
+      throwError $ "The path constructor " ++ x ++ " is used as a" ++
+                   " variable at " ++ show l ++ " in " ++ modName ++
+                   " (path constructors should have their type in" ++
+                   " curly braces as first argument)"
     Just Name        ->
-     throwError $ "Name " ++ x ++ " used as a variable at position " ++
+      throwError $ "Name " ++ x ++ " used as a variable at position " ++
                    show l ++ " in module " ++ modName
     _ -> throwError $ "Cannot resolve variable " ++ x ++ " at position " ++
                       show l ++ " in module " ++ modName
@@ -221,7 +222,8 @@ resolveSystem (System ts) = do
                   | Side alpha u <- ts ]
   let alphas = map fst ts'
   unless (nub alphas == alphas) $
-    throwError $ "system contains same face multiple times: " ++ C.showListSystem ts'
+    throwError $ "system contains same face multiple times: " ++
+                 C.showListSystem ts'
   -- Note: the symbols in alpha are in scope in u, but they mean 0 or 1
   return $ Map.fromList ts'
 
@@ -270,45 +272,72 @@ resolveLabel cs (PLabel n vdecl is sys) = do
                 <*> local (insertNames is . insertIdents cs' . insertVars ts)
                       (resolveSystem sys)
 
--- Resolve Data or Def or Split declarations
-resolveDecl :: Decl -> Resolver (CTT.Decl,[(Ident,SymKind)])
-resolveDecl d = case d of
-  DeclDef (AIdent (_,f)) tele t body -> do
+-- 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
+  DeclDef (AIdent (_,f)) tele t body ->
     let tele' = flattenTele tele
-    a <- binds CTT.Pi tele' (resolveExp t)
-    d <- lams tele' (local (insertVar f) $ resolveWhere body)
-    return ((f,(a,d)),[(f,Variable)])
-  DeclData (AIdent (l,f)) tele sums -> do
+        a     = binds CTT.Pi tele' (resolveExp t)
+        d     = lams tele' (local (insertVar f) $ resolveWhere body)
+    in (f,a,d,[(f,Variable)])
+  DeclData (AIdent (l,f)) tele sums ->
     let tele' = flattenTele tele
-    a <- binds CTT.Pi tele' (return CTT.U)
-    let cs  = [ (unAIdent lbl,Constructor) | OLabel lbl _ <- sums ]
-    let pcs = [ (unAIdent lbl,PConstructor) | PLabel lbl _ _ _ <- sums ]
-    let sum = if null pcs then CTT.Sum else CTT.HSum
-    d <- lams tele' $ local (insertVar f) $
-         sum <$> getLoc l <*> pure f
-             <*> mapM (resolveLabel (cs ++ pcs)) sums
-    return ((f,(a,d)),(f,Variable):cs ++ pcs)
-  DeclSplit (AIdent (l,f)) tele t brs -> do
+        a     = binds CTT.Pi tele' (return CTT.U)
+        cs    = [ (unAIdent lbl,Constructor) | OLabel lbl _ <- sums ]
+        pcs   = [ (unAIdent lbl,PConstructor) | PLabel lbl _ _ _ <- sums ]
+        sum   = if null pcs then CTT.Sum else CTT.HSum
+        d = lams tele' $ local (insertVar f) $
+            sum <$> getLoc l <*> pure f
+               <*> mapM (resolveLabel (cs ++ pcs)) sums
+    in (f,a,d,(f,Variable):cs ++ pcs)
+  DeclSplit (AIdent (l,f)) tele t brs ->
     let tele' = flattenTele tele
-        vars = map fst tele'
-    loc  <- getLoc l
-    a    <- binds CTT.Pi tele' (resolveExp t)
-    ty   <- local (insertVars vars) $ resolveExp t
-    brs' <- local (insertVars (f:vars)) (mapM resolveBranch brs)
-    body <- lams tele' (return $ CTT.Split f loc ty brs')
-    return ((f,(a,body)),[(f,Variable)])
-  DeclUndef (AIdent (l,f)) tele t -> do
+        vars  = map fst tele'
+        a     = binds CTT.Pi tele' (resolveExp t)
+        d     = do
+                  loc <- getLoc l
+                  ty  <- local (insertVars vars) $ resolveExp t
+                  brs' <- local (insertVars (f:vars)) (mapM resolveBranch brs)
+                  lams tele' (return $ CTT.Split f loc ty brs')
+    in (f,a,d,[(f,Variable)])
+  DeclUndef (AIdent (l,f)) tele t ->
     let tele' = flattenTele tele
-    a <- binds CTT.Pi tele' (resolveExp t)
-    d <- CTT.Undef <$> getLoc l <*> pure a
-    return ((f,(a,d)),[(f,Variable)])
+        a     = binds CTT.Pi tele' (resolveExp t)
+        d     = CTT.Undef <$> getLoc l <*> a
+    in (f,a,d,[(f,Variable)])
+
+resolveRTele :: [Ident] -> [Resolver CTT.Ter] -> Resolver CTT.Tele
+resolveRTele [] _ = return []
+resolveRTele (i:is) (t:ts) = do
+  a  <- t
+  as <- local (insertVar i) (resolveRTele is ts)
+  return ((i,a):as)
+
+-- Resolve a declaration
+resolveDecl :: Decl -> Resolver ([CTT.Decl],[(Ident,SymKind)])
+resolveDecl d = case d of
+  DeclMutual decls -> do
+    let (fs,ts,bs,nss) = unzip4 $ map resolveSimpleDecl decls
+        ns = concat nss -- TODO: some sanity checks? Duplicates!?
+    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
+          a <- typ
+          d <- body
+          return ([(f,(a,d))],ns)
 
 resolveDecls :: [Decl] -> Resolver ([[CTT.Decl]],[(Ident,SymKind)])
 resolveDecls []     = return ([],[])
 resolveDecls (d:ds) = do
   (rtd,names)  <- resolveDecl d
   (rds,names') <- local (insertIdents names) $ resolveDecls ds
-  return ([rtd] : rds, names' ++ names)
+  return (rtd : rds, names' ++ names)
 
 resolveModule :: Module -> Resolver ([[CTT.Decl]],[(Ident,SymKind)])
 resolveModule (Module (AIdent (_,n)) _ decls) =