From: Simon Huber Date: Wed, 12 Aug 2015 15:31:28 +0000 (+0200) Subject: Reintroduced mutual (wip) X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=0815d8848d5db076699c157a79e77f5aa92e31c7;p=cubicaltt.git Reintroduced mutual (wip) --- diff --git a/Exp.cf b/Exp.cf index db7234f..6b71f30 100644 --- 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 f3738d4..dd5e803 100644 --- 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) =