From: Simon Huber Date: Sat, 18 Apr 2015 11:44:42 +0000 (+0200) Subject: let the system in a pcon know about all pcons in the sum X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=630f5f69593f197df96572376b10de038200720e;p=cubicaltt.git let the system in a pcon know about all pcons in the sum TODO: the current pcon should not know about itself --- diff --git a/Resolver.hs b/Resolver.hs index 8123493..3672dfc 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -254,7 +254,7 @@ resolveBranch (OBranch (AIdent (_,lbl)) args e) = do return $ CTT.OBranch lbl (map unAIdent args) re resolveBranch (PBranch (AIdent (_,lbl)) args is e) = do re <- local (insertNames is . insertAIdents args) $ resolveWhere e - names <- mapM resolveName is + let names = map (C.Name . unAIdent) is return $ CTT.PBranch lbl (map unAIdent args) names re resolveTele :: [(Ident,Exp)] -> Resolver CTT.Tele @@ -269,6 +269,8 @@ 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) @@ -285,9 +287,10 @@ resolveDecl d = case d of let tele' = flattenTele tele a <- binds CTT.Pi tele' (return CTT.U) let cs = [ (unAIdent lbl,Constructor) | OLabel lbl _ <- sums ] - d <- lams tele' $ local (insertVar f) $ - CTT.Sum <$> getLoc l <*> pure f <*> mapM (resolveLabel cs) sums let pcs = [ (unAIdent lbl,PConstructor) | PLabel lbl _ _ _ <- sums ] + d <- lams tele' $ local (insertVar f) $ + CTT.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 let tele' = flattenTele tele