From 5c84fb351c84115dfb66cef9c5aa0f6c9a208d4f Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 14 Mar 2023 18:44:05 +0100 Subject: [PATCH 01/11] implement mutual lets up to typechecking --- .../Abstract/Extra/DependencyBuilder.hs | 61 +++++++--- src/Juvix/Compiler/Internal/Data/InfoTable.hs | 7 +- src/Juvix/Compiler/Internal/Extra.hs | 5 + src/Juvix/Compiler/Internal/Language.hs | 14 ++- src/Juvix/Compiler/Internal/Pretty/Base.hs | 1 + .../Internal/Translation/FromAbstract.hs | 106 ++++++++++-------- .../Analysis/Termination/Data/Graph.hs | 4 +- .../Analysis/Termination/LexOrder.hs | 16 +-- .../Analysis/ArityChecking/Checker.hs | 1 + .../Analysis/Positivity/Checker.hs | 4 + .../Analysis/TypeChecking/Checker.hs | 4 +- src/Juvix/Data/DependencyInfo.hs | 12 +- src/Juvix/Prelude/Base.hs | 8 ++ tests/positive/issue1879/LetSynonym.juvix | 8 ++ 14 files changed, 166 insertions(+), 85 deletions(-) diff --git a/src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs b/src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs index c85cb1fa80..fe0596586d 100644 --- a/src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs +++ b/src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs @@ -1,4 +1,4 @@ -module Juvix.Compiler.Abstract.Extra.DependencyBuilder (buildDependencyInfo, ExportsTable) where +module Juvix.Compiler.Abstract.Extra.DependencyBuilder (buildDependencyInfo, buildDependencyInfoExpr, ExportsTable) where import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet @@ -18,7 +18,23 @@ type ExportsTable = HashSet NameId buildDependencyInfo :: NonEmpty TopModule -> ExportsTable -> NameDependencyInfo buildDependencyInfo ms tab = - createDependencyInfo graph startNodes + buildDependencyInfoHelper tab (mapM_ goModule ms) + +buildDependencyInfoExpr :: Expression -> NameDependencyInfo +buildDependencyInfoExpr = buildDependencyInfoHelper mempty . goExpression Nothing + +buildDependencyInfoHelper :: + ExportsTable -> + ( Sem + '[ Reader ExportsTable, + State DependencyGraph, + State StartNodes, + State VisitedModules + ] + () + ) -> + NameDependencyInfo +buildDependencyInfoHelper tbl m = createDependencyInfo graph startNodes where startNodes :: StartNodes graph :: DependencyGraph @@ -27,12 +43,14 @@ buildDependencyInfo ms tab = evalState (HashSet.empty :: VisitedModules) $ runState HashSet.empty $ execState HashMap.empty $ - runReader tab $ - mapM_ goModule ms + runReader tbl m addStartNode :: (Member (State StartNodes) r) => Name -> Sem r () addStartNode n = modify (HashSet.insert n) +addEdgeMay :: (Member (State DependencyGraph) r) => Maybe Name -> Name -> Sem r () +addEdgeMay mn1 n2 = whenJust mn1 $ \n1 -> addEdge n1 n2 + addEdge :: (Member (State DependencyGraph) r) => Name -> Name -> Sem r () addEdge n1 n2 = modify @@ -87,7 +105,7 @@ goStatement modName = \case StatementAxiom ax -> do checkStartNode (ax ^. axiomName) addEdge (ax ^. axiomName) modName - goExpression (ax ^. axiomName) (ax ^. axiomType) + goExpression (Just (ax ^. axiomName)) (ax ^. axiomType) StatementFunction f -> goTopFunctionDef modName f StatementImport m -> guardNotVisited (m ^. moduleName) (goModule m) StatementLocalModule m -> goLocalModule modName m @@ -95,8 +113,8 @@ goStatement modName = \case checkStartNode (i ^. inductiveName) checkBuiltinInductiveStartNode i addEdge (i ^. inductiveName) modName - mapM_ (goFunctionParameter (i ^. inductiveName)) (i ^. inductiveParameters) - goExpression (i ^. inductiveName) (i ^. inductiveType) + mapM_ (goFunctionParameter (Just (i ^. inductiveName))) (i ^. inductiveParameters) + goExpression (Just (i ^. inductiveName)) (i ^. inductiveType) mapM_ (goConstructorDef (i ^. inductiveName)) (i ^. inductiveConstructors) goTopFunctionDef :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> FunctionDef -> Sem r () @@ -110,7 +128,7 @@ goFunctionDefHelper :: Sem r () goFunctionDefHelper f = do checkStartNode (f ^. funDefName) - goExpression (f ^. funDefName) (f ^. funDefTypeSig) + goExpression (Just (f ^. funDefName)) (f ^. funDefTypeSig) mapM_ (goFunctionClause (f ^. funDefName)) (f ^. funDefClauses) -- constructors of an inductive type depend on the inductive type, not the other @@ -118,14 +136,14 @@ goFunctionDefHelper f = do goConstructorDef :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> InductiveConstructorDef -> Sem r () goConstructorDef indName c = do addEdge (c ^. constructorName) indName - goExpression indName (c ^. constructorType) + goExpression (Just indName) (c ^. constructorType) goFunctionClause :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> FunctionClause -> Sem r () goFunctionClause p c = do - mapM_ (goPattern p) (c ^. clausePatterns) - goExpression p (c ^. clauseBody) + mapM_ (goPattern (Just p)) (c ^. clausePatterns) + goExpression (Just p) (c ^. clauseBody) -goPattern :: forall r. (Member (State DependencyGraph) r) => Name -> PatternArg -> Sem r () +goPattern :: forall r. (Member (State DependencyGraph) r) => Maybe Name -> PatternArg -> Sem r () goPattern n p = case p ^. patternArgPattern of PatternVariable {} -> return () PatternWildcard {} -> return () @@ -134,12 +152,17 @@ goPattern n p = case p ^. patternArgPattern of where goApp :: ConstructorApp -> Sem r () goApp (ConstructorApp ctr ps) = do - addEdge n (ctr ^. constructorRefName) + addEdgeMay n (ctr ^. constructorRefName) mapM_ (goPattern n) ps -goExpression :: forall r. (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> Expression -> Sem r () +goExpression :: + forall r. + (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => + Maybe Name -> + Expression -> + Sem r () goExpression p e = case e of - ExpressionIden i -> addEdge p (idenName i) + ExpressionIden i -> addEdgeMay p (idenName i) ExpressionUniverse {} -> return () ExpressionFunction f -> do goFunctionParameter p (f ^. funParameter) @@ -177,8 +200,12 @@ goExpression p e = case e of goLetClause :: LetClause -> Sem r () goLetClause = \case LetFunDef f -> do - addEdge p (f ^. funDefName) + addEdgeMay p (f ^. funDefName) goFunctionDefHelper f -goFunctionParameter :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> FunctionParameter -> Sem r () +goFunctionParameter :: + (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => + Maybe Name -> + FunctionParameter -> + Sem r () goFunctionParameter p param = goExpression p (param ^. paramType) diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index ceb5469559..eae54f2a3f 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -117,9 +117,14 @@ buildTable1' m = do ] <> [ (f ^. funDefName, FunctionInfo f) | s <- filter (not . isInclude) ss, - LetFunDef f <- universeBi s + Let {..} <- universeBi s, + f <- concatMap (toList . flattenClause) _letClauses ] where + flattenClause :: LetClause -> NonEmpty FunctionDef + flattenClause = \case + LetFunDef f -> pure f + LetMutualBlock (MutualBlock fs) -> fs isInclude :: Statement -> Bool isInclude = \case StatementInclude {} -> True diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index 0707a7cc65..e01be07b80 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -73,9 +73,14 @@ instance HasExpressions Case where where _caseParens = l ^. caseParens +instance HasExpressions MutualBlock where + leafExpressions f (MutualBlock defs) = + MutualBlock <$> traverse (leafExpressions f) defs + instance HasExpressions LetClause where leafExpressions f = \case LetFunDef d -> LetFunDef <$> leafExpressions f d + LetMutualBlock b -> LetMutualBlock <$> leafExpressions f b instance HasExpressions Let where leafExpressions f l = do diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index c0166520af..117aa38fc3 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -46,7 +46,9 @@ data Statement newtype MutualBlock = MutualBlock { _mutualFunctions :: NonEmpty FunctionDef } - deriving stock (Data) + deriving stock (Eq, Generic, Data) + +instance Hashable MutualBlock data AxiomDef = AxiomDef { _axiomName :: AxiomName, @@ -98,8 +100,10 @@ data TypedExpression = TypedExpression _typedExpression :: Expression } -newtype LetClause - = LetFunDef FunctionDef +data LetClause + = -- | Non-recursive let definition + LetFunDef FunctionDef + | LetMutualBlock MutualBlock deriving stock (Eq, Generic, Data) instance Hashable LetClause @@ -367,9 +371,13 @@ instance HasLoc FunctionClause where instance HasLoc FunctionDef where getLoc f = getLoc (f ^. funDefName) <> getLocSpan (f ^. funDefClauses) +instance HasLoc MutualBlock where + getLoc (MutualBlock defs) = getLocSpan defs + instance HasLoc LetClause where getLoc = \case LetFunDef f -> getLoc f + LetMutualBlock f -> getLoc f instance HasLoc Let where getLoc l = getLocSpan (l ^. letClauses) <> getLoc (l ^. letExpression) diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index a6a72c8df7..234eb1fe07 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -93,6 +93,7 @@ instance PrettyCode Let where instance PrettyCode LetClause where ppCode = \case LetFunDef f -> ppCode f + LetMutualBlock b -> ppCode b ppPipeBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann) ppPipeBlock items = vsep <$> mapM (fmap (kwPipe <+>) . ppCode) items diff --git a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs index aa9b50f3cc..be232ae7aa 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs @@ -8,16 +8,15 @@ module Juvix.Compiler.Internal.Translation.FromAbstract ) where -import Data.Graph import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet -import Juvix.Compiler.Abstract.Data.NameDependencyInfo qualified as Abstract +import Juvix.Compiler.Abstract.Data.NameDependencyInfo import Juvix.Compiler.Abstract.Extra.DependencyBuilder import Juvix.Compiler.Abstract.Extra.DependencyBuilder qualified as Abstract import Juvix.Compiler.Abstract.Language qualified as Abstract import Juvix.Compiler.Abstract.Translation.FromConcrete.Data.Context qualified as Abstract import Juvix.Compiler.Internal.Extra -import Juvix.Compiler.Internal.Translation.FromAbstract.Analysis.Termination hiding (Graph) +import Juvix.Compiler.Internal.Translation.FromAbstract.Analysis.Termination import Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context import Juvix.Compiler.Pipeline.EntryPoint qualified as E import Juvix.Prelude @@ -69,10 +68,14 @@ fromAbstract abstractResults = do abstractResults ^. Abstract.abstractResultEntryPoint . E.entryPointNoTermination + depInfo :: NameDependencyInfo depInfo = buildDependencyInfo (abstractResults ^. Abstract.resultModules) (abstractResults ^. Abstract.resultExports) -fromAbstractExpression :: (Members '[NameIdGen] r) => Abstract.Expression -> Sem r Expression -fromAbstractExpression = goExpression +fromAbstractExpression :: Members '[NameIdGen] r => Abstract.Expression -> Sem r Expression +fromAbstractExpression e = runReader depInfo (goExpression e) + where + depInfo :: NameDependencyInfo + depInfo = buildDependencyInfoExpr e goModule :: (Members '[Reader ExportsTable, State TranslationState, NameIdGen] r) => @@ -80,42 +83,45 @@ goModule :: Sem r Module goModule m = do expTbl <- ask - let mutualBlocks :: [NonEmpty Abstract.FunctionDef] - mutualBlocks = buildMutualBlocks expTbl - _moduleBody' <- goModuleBody mutualBlocks (m ^. Abstract.moduleBody) - examples' <- mapM goExample (m ^. Abstract.moduleExamples) - return - Module - { _moduleName = m ^. Abstract.moduleName, - _moduleExamples = examples', - _moduleBody = _moduleBody' - } + let depInfo :: NameDependencyInfo + depInfo = Abstract.buildDependencyInfo (pure m) expTbl + runReader depInfo $ do + mutualBlocks :: [SCC Abstract.FunctionDef] <- buildMutualBlocks moduleFunctionDefs + _moduleBody' <- goModuleBody (map flattenSCC mutualBlocks) (m ^. Abstract.moduleBody) + examples' <- mapM goExample (m ^. Abstract.moduleExamples) + return + Module + { _moduleName = m ^. Abstract.moduleName, + _moduleExamples = examples', + _moduleBody = _moduleBody' + } + where + moduleFunctionDefs :: [Abstract.FunctionDef] + moduleFunctionDefs = [d | Abstract.StatementFunction d <- m ^. Abstract.moduleBody . Abstract.moduleStatements] + +buildMutualBlocks :: Members '[Reader NameDependencyInfo] r => [Abstract.FunctionDef] -> Sem r [SCC Abstract.FunctionDef] +buildMutualBlocks defs = do + depInfo <- ask + let scomponents :: [SCC Abstract.Name] = buildSCCs depInfo + return (mapMaybe helper scomponents) where funsByName :: HashMap Abstract.FunctionName Abstract.FunctionDef - funsByName = - HashMap.fromList - [ (d ^. Abstract.funDefName, d) - | Abstract.StatementFunction d <- m ^. Abstract.moduleBody . Abstract.moduleStatements - ] + funsByName = HashMap.fromList [(d ^. Abstract.funDefName, d) | d <- defs] getFun :: Abstract.FunctionName -> Maybe Abstract.FunctionDef getFun n = funsByName ^. at n - buildMutualBlocks :: Abstract.ExportsTable -> [NonEmpty Abstract.FunctionDef] - buildMutualBlocks expTbl = mapMaybe (nonEmpty . mapMaybe getFun . toList . fromNonEmptyTree) scomponents + helper :: SCC Abstract.Name -> Maybe (SCC Abstract.FunctionDef) + helper = nonEmptySCC . fmap getFun where - fromNonEmptyTree :: Tree a -> NonEmpty a - fromNonEmptyTree = fromJust . nonEmpty . toList - depInfo :: Abstract.NameDependencyInfo - depInfo = Abstract.buildDependencyInfo (pure m) expTbl - graph :: Graph - graph = Abstract.buildDependencyInfo (pure m) expTbl ^. Abstract.depInfoGraph - scomponents :: [Tree Abstract.Name] - scomponents = fmap (Abstract.nameFromVertex depInfo) <$> scc graph + nonEmptySCC :: SCC (Maybe a) -> Maybe (SCC a) + nonEmptySCC = \case + AcyclicSCC a -> AcyclicSCC <$> a + CyclicSCC p -> CyclicSCC . toList <$> nonEmpty (catMaybes p) unsupported :: Text -> a unsupported thing = error ("Abstract to Internal: Not yet supported: " <> thing) goModuleBody :: - (Members '[Reader ExportsTable, State TranslationState, NameIdGen] r) => + (Members '[Reader ExportsTable, Reader NameDependencyInfo, State TranslationState, NameIdGen] r) => [NonEmpty Abstract.FunctionDef] -> Abstract.ModuleBody -> Sem r ModuleBody @@ -143,7 +149,7 @@ goImport m = do ) goStatement :: - (Members '[Reader ExportsTable, State TranslationState, NameIdGen] r) => + (Members '[Reader ExportsTable, State TranslationState, NameIdGen, Reader NameDependencyInfo] r) => Abstract.Statement -> Sem r (Maybe Statement) goStatement = \case @@ -198,7 +204,7 @@ goFunction (Abstract.Function l r) = do r' <- goType r return (Function l' r') -goFunctionDef :: (Members '[NameIdGen] r) => Abstract.FunctionDef -> Sem r FunctionDef +goFunctionDef :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.FunctionDef -> Sem r FunctionDef goFunctionDef f = do _funDefClauses' <- mapM (goFunctionClause _funDefName') (f ^. Abstract.funDefClauses) _funDefType' <- goType (f ^. Abstract.funDefTypeSig) @@ -215,7 +221,7 @@ goFunctionDef f = do _funDefName' :: Name _funDefName' = f ^. Abstract.funDefName -goExample :: (Members '[NameIdGen] r) => Abstract.Example -> Sem r Example +goExample :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Example -> Sem r Example goExample e = do e' <- goExpression (e ^. Abstract.exampleExpression) return @@ -224,7 +230,7 @@ goExample e = do _exampleId = e ^. Abstract.exampleId } -goFunctionClause :: (Members '[NameIdGen] r) => Name -> Abstract.FunctionClause -> Sem r FunctionClause +goFunctionClause :: Members '[NameIdGen, Reader NameDependencyInfo] r => Name -> Abstract.FunctionClause -> Sem r FunctionClause goFunctionClause n c = do _clauseBody' <- goExpression (c ^. Abstract.clauseBody) _clausePatterns' <- mapM goPatternArg (c ^. Abstract.clausePatterns) @@ -287,7 +293,7 @@ goType e = case e of Abstract.ExpressionLet {} -> unsupported "let in types" Abstract.ExpressionCase {} -> unsupported "case in types" -goLambda :: forall r. (Members '[NameIdGen] r) => Abstract.Lambda -> Sem r Lambda +goLambda :: forall r. Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Lambda -> Sem r Lambda goLambda (Abstract.Lambda cl') = do _lambdaClauses <- mapM goClause cl' let _lambdaType :: Maybe Expression = Nothing @@ -304,7 +310,7 @@ goLambda (Abstract.Lambda cl') = do Explicit -> p Implicit -> unsupported "implicit patterns in lambda" -goApplication :: (Members '[NameIdGen] r) => Abstract.Application -> Sem r Application +goApplication :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Application -> Sem r Application goApplication (Abstract.Application f x i) = do f' <- goExpression f x' <- goExpression x @@ -318,7 +324,7 @@ goIden i = case i of Abstract.IdenAxiom a -> IdenAxiom (a ^. Abstract.axiomRefName) Abstract.IdenInductive a -> IdenInductive (a ^. Abstract.inductiveRefName) -goExpressionFunction :: forall r. (Members '[NameIdGen] r) => Abstract.Function -> Sem r Function +goExpressionFunction :: forall r. Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Function -> Sem r Function goExpressionFunction f = do l' <- goParam (f ^. Abstract.funParameter) r' <- goExpression (f ^. Abstract.funReturn) @@ -329,7 +335,7 @@ goExpressionFunction f = do ty' <- goExpression (p ^. Abstract.paramType) return (FunctionParameter (p ^. Abstract.paramName) (p ^. Abstract.paramImplicit) ty') -goExpression :: (Members '[NameIdGen] r) => Abstract.Expression -> Sem r Expression +goExpression :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Expression -> Sem r Expression goExpression e = case e of Abstract.ExpressionIden i -> return (ExpressionIden (goIden i)) Abstract.ExpressionUniverse u -> return (ExpressionUniverse (goUniverse u)) @@ -341,7 +347,7 @@ goExpression e = case e of Abstract.ExpressionLet l -> ExpressionLet <$> goLet l Abstract.ExpressionCase c -> ExpressionCase <$> goCase c -goCase :: Members '[NameIdGen] r => Abstract.Case -> Sem r Case +goCase :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Case -> Sem r Case goCase c = do _caseExpression <- goExpression (c ^. Abstract.caseExpression) _caseBranches <- mapM goCaseBranch (c ^. Abstract.caseBranches) @@ -350,21 +356,25 @@ goCase c = do _caseExpressionWholeType :: Maybe Expression = Nothing return Case {..} -goCaseBranch :: Members '[NameIdGen] r => Abstract.CaseBranch -> Sem r CaseBranch +goCaseBranch :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.CaseBranch -> Sem r CaseBranch goCaseBranch b = do _caseBranchPattern <- goPatternArg (b ^. Abstract.caseBranchPattern) _caseBranchExpression <- goExpression (b ^. Abstract.caseBranchExpression) return CaseBranch {..} -goLetClause :: (Members '[NameIdGen] r) => Abstract.LetClause -> Sem r LetClause -goLetClause = \case - Abstract.LetFunDef f -> LetFunDef <$> goFunctionDef f - -goLet :: (Members '[NameIdGen] r) => Abstract.Let -> Sem r Let +goLet :: forall r. (Members '[NameIdGen, Reader NameDependencyInfo] r) => Abstract.Let -> Sem r Let goLet l = do _letExpression <- goExpression (l ^. Abstract.letExpression) - _letClauses <- mapM goLetClause (l ^. Abstract.letClauses) + mutualBlocks <- buildMutualBlocks funDefs + _letClauses <- nonEmpty' <$> mapM goLetBlock mutualBlocks return Let {..} + where + funDefs :: [Abstract.FunctionDef] + funDefs = [f | Abstract.LetFunDef f <- toList (l ^. Abstract.letClauses)] + goLetBlock :: SCC Abstract.FunctionDef -> Sem r LetClause + goLetBlock = \case + AcyclicSCC f -> LetFunDef <$> goFunctionDef f + CyclicSCC m -> LetMutualBlock . MutualBlock <$> mapM goFunctionDef (nonEmpty' m) goInductiveParameter :: Abstract.FunctionParameter -> Sem r InductiveParameter goInductiveParameter f = @@ -378,7 +388,7 @@ goInductiveParameter f = (Just {}, _) -> unsupported "only type variables of small types are allowed" (Nothing, _) -> unsupported "unnamed inductive parameters" -goInductiveDef :: forall r. (Members '[NameIdGen] r) => Abstract.InductiveDef -> Sem r InductiveDef +goInductiveDef :: forall r. Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.InductiveDef -> Sem r InductiveDef goInductiveDef i | not (isSmallType (i ^. Abstract.inductiveType)) = unsupported "inductive indices" | otherwise = do diff --git a/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/Data/Graph.hs b/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/Data/Graph.hs index cec687bd60..f8695c30e0 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/Data/Graph.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/Data/Graph.hs @@ -11,7 +11,7 @@ import Juvix.Compiler.Internal.Translation.FromAbstract.Analysis.Termination.Dat import Juvix.Prelude import Prettyprinter qualified as PP -type Graph = HashMap (FunctionName, FunctionName) Edge +type EdgeMap = HashMap (FunctionName, FunctionName) Edge data Edge = Edge { _edgeFrom :: FunctionName, @@ -19,7 +19,7 @@ data Edge = Edge _edgeMatrices :: HashSet CallMatrix } -newtype CompleteCallGraph = CompleteCallGraph Graph +newtype CompleteCallGraph = CompleteCallGraph EdgeMap data ReflexiveEdge = ReflexiveEdge { _reflexiveEdgeFun :: FunctionName, diff --git a/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/LexOrder.hs b/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/LexOrder.hs index 714ff2d7d6..b9116c548e 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/LexOrder.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/LexOrder.hs @@ -9,7 +9,7 @@ import Juvix.Compiler.Abstract.Extra import Juvix.Compiler.Internal.Translation.FromAbstract.Analysis.Termination.Data import Juvix.Prelude -fromEdgeList :: [Edge] -> Graph +fromEdgeList :: [Edge] -> EdgeMap fromEdgeList l = HashMap.fromList [((e ^. edgeFrom, e ^. edgeTo), e) | e <- l] composeEdge :: Edge -> Edge -> Maybe Edge @@ -22,7 +22,7 @@ composeEdge a b = do _edgeMatrices = multiplyMany (a ^. edgeMatrices) (b ^. edgeMatrices) } -edgesCompose :: Graph -> Graph -> Graph +edgesCompose :: EdgeMap -> EdgeMap -> EdgeMap edgesCompose g h = fromEdgeList (catMaybes [composeEdge u v | u <- toList g, v <- toList h]) @@ -37,10 +37,10 @@ edgeUnion a b (HashSet.union (a ^. edgeMatrices) (b ^. edgeMatrices)) | otherwise = impossible -edgesUnion :: Graph -> Graph -> Graph +edgesUnion :: EdgeMap -> EdgeMap -> EdgeMap edgesUnion = HashMap.unionWith edgeUnion -edgesCount :: Graph -> Int +edgesCount :: EdgeMap -> Int edgesCount es = sum [HashSet.size (e ^. edgeMatrices) | e <- toList es] multiply :: CallMatrix -> CallMatrix -> CallMatrix @@ -77,10 +77,10 @@ unsafeFilterGraph funNames (CompleteCallGraph g) = completeCallGraph :: CallMap -> CompleteCallGraph completeCallGraph CallMap {..} = CompleteCallGraph (go startingEdges) where - startingEdges :: Graph + startingEdges :: EdgeMap startingEdges = foldr insertCall mempty allCalls where - insertCall :: Call -> Graph -> Graph + insertCall :: Call -> EdgeMap -> EdgeMap insertCall Call {..} = HashMap.alter (Just . aux) (_callFrom, _callTo) where aux :: Maybe Edge -> Edge @@ -96,14 +96,14 @@ completeCallGraph CallMap {..} = CompleteCallGraph (go startingEdges) funCall <- funCalls ] - go :: Graph -> Graph + go :: EdgeMap -> EdgeMap go g | edgesCount g == edgesCount g' = g | otherwise = go g' where g' = step g - step :: Graph -> Graph + step :: EdgeMap -> EdgeMap step s = edgesUnion (edgesCompose s startingEdges) s reflexiveEdges :: CompleteCallGraph -> [ReflexiveEdge] diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs index ffdf87e9e1..e5ca06345e 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs @@ -377,6 +377,7 @@ checkLet ari l = do checkLetClause :: LetClause -> Sem r LetClause checkLetClause = \case LetFunDef f -> LetFunDef <$> checkFunctionDef f + LetMutualBlock f -> LetMutualBlock <$> checkMutualBlock f checkLambda :: forall r. diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs index bd59f3a211..85f97f3f8a 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -89,6 +89,10 @@ checkStrictlyPositiveOccurrences ty ctorName name recLimit ref = helperLetClause :: LetClause -> Sem r () helperLetClause = \case LetFunDef f -> helperFunctionDef f + LetMutualBlock b -> helperMutualBlock b + + helperMutualBlock :: MutualBlock -> Sem r () + helperMutualBlock b = mapM_ helperFunctionDef (b ^. mutualFunctions) helperFunctionDef :: FunctionDef -> Sem r () helperFunctionDef d = do diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs index d4d80abeb7..c9496b206c 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs @@ -385,7 +385,7 @@ checkPattern = go indName = IdenInductive (info ^. constructorInfoInductive) loc = getLoc a paramHoles <- map ExpressionHole <$> replicateM numIndParams (freshHole loc) - let patternTy = foldApplication (ExpressionIden indName) (zip (repeat Explicit) paramHoles) + let patternTy = foldApplication (ExpressionIden indName) (map (Explicit,) paramHoles) whenJustM (matchTypes patternTy (ExpressionHole hole)) err @@ -524,10 +524,10 @@ inferExpression' hint e = case e of } } - -- what about mutually recursive lets? goLetClause :: LetClause -> Sem r LetClause goLetClause = \case LetFunDef f -> LetFunDef <$> checkFunctionDef f + LetMutualBlock f -> LetMutualBlock <$> checkMutualBlock f goHole :: Hole -> Sem r TypedExpression goHole h = do diff --git a/src/Juvix/Data/DependencyInfo.hs b/src/Juvix/Data/DependencyInfo.hs index 9d4de09553..2d17419e09 100644 --- a/src/Juvix/Data/DependencyInfo.hs +++ b/src/Juvix/Data/DependencyInfo.hs @@ -1,6 +1,5 @@ module Juvix.Data.DependencyInfo where -import Data.Graph (Graph, Vertex) import Data.Graph qualified as Graph import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet @@ -13,6 +12,7 @@ import Juvix.Prelude.Base data DependencyInfo n = DependencyInfo { _depInfoGraph :: Graph, _depInfoNodeFromVertex :: Vertex -> (n, HashSet n), + _depInfoEdgeList :: [(n, n, [n])], _depInfoVertexFromName :: n -> Maybe Vertex, _depInfoReachable :: HashSet n, _depInfoTopSort :: [n] @@ -25,6 +25,7 @@ createDependencyInfo edges startNames = DependencyInfo { _depInfoGraph = graph, _depInfoNodeFromVertex = \v -> let (_, x, y) = nodeFromVertex v in (x, HashSet.fromList y), + _depInfoEdgeList = edgeList, _depInfoVertexFromName = vertexFromName, _depInfoReachable = reachableNames, _depInfoTopSort = topSortedNames @@ -33,9 +34,9 @@ createDependencyInfo edges startNames = graph :: Graph nodeFromVertex :: Vertex -> (n, n, [n]) vertexFromName :: n -> Maybe Vertex - (graph, nodeFromVertex, vertexFromName) = - Graph.graphFromEdges $ - map (\(x, y) -> (x, x, HashSet.toList y)) (HashMap.toList edges) + (graph, nodeFromVertex, vertexFromName) = Graph.graphFromEdges edgeList + edgeList :: [(n, n, [n])] + edgeList = map (\(x, y) -> (x, x, HashSet.toList y)) (HashMap.toList edges) reachableNames :: HashSet n reachableNames = HashSet.fromList $ @@ -51,3 +52,6 @@ nameFromVertex depInfo v = fst $ (depInfo ^. depInfoNodeFromVertex) v isReachable :: (Hashable n) => DependencyInfo n -> n -> Bool isReachable depInfo n = HashSet.member n (depInfo ^. depInfoReachable) + +buildSCCs :: Ord n => DependencyInfo n -> [SCC n] +buildSCCs = Graph.stronglyConnComp . (^. depInfoEdgeList) diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs index 559f0f7b8e..40291201fd 100644 --- a/src/Juvix/Prelude/Base.hs +++ b/src/Juvix/Prelude/Base.hs @@ -7,6 +7,7 @@ module Juvix.Prelude.Base ( module Juvix.Prelude.Base, module Control.Applicative, + module Data.Graph, module Data.Map.Strict, module Data.Set, module Data.IntMap.Strict, @@ -95,6 +96,7 @@ import Data.Eq import Data.Foldable hiding (minimum, minimumBy) import Data.Function import Data.Functor +import Data.Graph (Graph, SCC (..), Vertex, stronglyConnComp) import Data.HashMap.Strict (HashMap) import Data.HashMap.Strict qualified as HashMap import Data.HashSet (HashSet) @@ -441,3 +443,9 @@ ensureFile f = unlessM (Path.doesFileExist f) (throwM (mkIOError doesNotExistErrorType "" Nothing (Just (toFilePath f)))) + +-- Ideally `CyclicSCC`'s argument' would have type `NonEmpty a` instead of `[a]` +flattenSCC :: SCC a -> NonEmpty a +flattenSCC = \case + AcyclicSCC a -> pure a + CyclicSCC as -> nonEmpty' as diff --git a/tests/positive/issue1879/LetSynonym.juvix b/tests/positive/issue1879/LetSynonym.juvix index 85da0dac4b..e520bc4633 100644 --- a/tests/positive/issue1879/LetSynonym.juvix +++ b/tests/positive/issue1879/LetSynonym.juvix @@ -1,4 +1,6 @@ module LetSynonym; + open import Stdlib.Prelude; + type T := | t : T; @@ -9,5 +11,11 @@ module LetSynonym; A := T; x : A; x := t; + odd : _; + even : _; + odd zero := false; + odd (suc n) := even n; + even zero := true; + even (suc n) := odd n; in x; end; From 0b3ffbd212cab7fe93fe38e97e39798a806cf40e Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 16 Mar 2023 01:22:36 +0100 Subject: [PATCH 02/11] implement let translation --- .../Compiler/Core/Translation/FromInternal.hs | 61 +++++++++---------- .../FromInternal/Data/IndexTable.hs | 15 +++-- 2 files changed, 41 insertions(+), 35 deletions(-) diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 25029a96f9..e6e2863499 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -311,8 +311,9 @@ goFunctionDef :: Sem r () goFunctionDef ((f, sym), ty) = do mbody <- case f ^. Internal.funDefBuiltin of - Just b | isIgnoredBuiltin b -> return Nothing - Just _ -> Just <$> runReader initIndexTable (mkFunBody ty f) + Just b + | isIgnoredBuiltin b -> return Nothing + | otherwise -> Just <$> runReader initIndexTable (mkFunBody ty f) Nothing -> Just <$> runReader initIndexTable (mkFunBody ty f) forM_ mbody (registerIdentNode sym) forM_ mbody setIdentArgsInfo' @@ -461,35 +462,33 @@ goLet :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) => Internal.Let -> Sem r Node -goLet l = do - vars <- asks (^. indexTableVars) - varsNum <- asks (^. indexTableVarsNum) - let bs :: [Name] - bs = map (\(Internal.LetFunDef Internal.FunctionDef {..}) -> _funDefName) (toList $ l ^. Internal.letClauses) - (vars', varsNum') = - foldl' - ( \(vs, k) name -> - (HashMap.insert (name ^. nameId) k vs, k + 1) - ) - (vars, varsNum) - bs - (defs, value) <- do - values <- - mapM - ( \(Internal.LetFunDef f) -> do - funTy <- goType (f ^. Internal.funDefType) - - funBody <- local (set indexTableVars vars' . set indexTableVarsNum varsNum') (mkFunBody funTy f) - return (funTy, funBody) - ) - (l ^. Internal.letClauses) - - lbody <- - local - (set indexTableVars vars' . set indexTableVarsNum varsNum') - (goExpression (l ^. Internal.letExpression)) - return (values, lbody) - return $ mkLetRec' defs value +goLet l = goClauses (toList (l ^. Internal.letClauses)) + where + goClauses :: [Internal.LetClause] -> Sem r Node + goClauses = \case + [] -> goExpression (l ^. Internal.letExpression) + c : cs -> case c of + Internal.LetFunDef f -> goNonRecFun f + Internal.LetMutualBlock m -> goMutual m + where + goNonRecFun :: Internal.FunctionDef -> Sem r Node + goNonRecFun f = + do + funTy <- goType (f ^. Internal.funDefType) + funBody <- mkFunBody funTy f + rest <- localAddName (f ^. Internal.funDefName) (goClauses cs) + return $ mkLet' funTy funBody rest + goMutual :: Internal.MutualBlock -> Sem r Node + goMutual (Internal.MutualBlock funs) = do + let lfuns = toList funs + names = map (^. Internal.funDefName) lfuns + tys = map (^. Internal.funDefType) lfuns + tys' <- mapM goType tys + localAddNames names $ do + vals' <- sequence [mkFunBody ty f | (ty, f) <- zipExact tys' lfuns] + let items = nonEmpty' (zip tys' vals') + rest <- goClauses cs + return (mkLetRec' items rest) goAxiomInductive :: forall r. diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal/Data/IndexTable.hs b/src/Juvix/Compiler/Core/Translation/FromInternal/Data/IndexTable.hs index f4c960eabc..204a752391 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal/Data/IndexTable.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal/Data/IndexTable.hs @@ -14,17 +14,24 @@ makeLenses ''IndexTable initIndexTable :: IndexTable initIndexTable = IndexTable 0 mempty -localAddName :: forall r a. (Member (Reader IndexTable) r) => Name -> Sem r a -> Sem r a -localAddName n s = do +localAddName :: Member (Reader IndexTable) r => Name -> Sem r a -> Sem r a +localAddName n = localAddNames [n] + +localAddNames :: forall r a. (Member (Reader IndexTable) r) => [Name] -> Sem r a -> Sem r a +localAddNames names s = do updateFn <- update local updateFn s where + len :: Int = length names + insertMany :: [(NameId, Index)] -> HashMap NameId Index -> HashMap NameId Index + insertMany l t = foldl' (\m (k, v) -> HashMap.insert k v m) t l update :: Sem r (IndexTable -> IndexTable) update = do idx <- asks (^. indexTableVarsNum) + let newElems = zip (map (^. nameId) names) [idx ..] return - ( over indexTableVars (HashMap.insert (n ^. nameId) idx) - . over indexTableVarsNum (+ 1) + ( over indexTableVars (insertMany newElems) + . over indexTableVarsNum (+ len) ) underBinders :: Members '[Reader IndexTable] r => Int -> Sem r a -> Sem r a From a64733deda3eaef95713adca1db906dc161387b2 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 16 Mar 2023 17:24:39 +0100 Subject: [PATCH 03/11] add test --- test/Compilation/Positive.hs | 8 +++++++- tests/Compilation/positive/out/test039.out | 2 ++ tests/Compilation/positive/test039.juvix | 22 ++++++++++++++++++++++ 3 files changed, 31 insertions(+), 1 deletion(-) create mode 100644 tests/Compilation/positive/out/test039.out create mode 100644 tests/Compilation/positive/test039.juvix diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index a116aa3bd1..f7692205bf 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -241,5 +241,11 @@ tests = "Simple case expression" $(mkRelDir ".") $(mkRelFile "test038.juvix") - $(mkRelFile "out/test038.out") + $(mkRelFile "out/test038.out"), + posTest + "Mutually recursive let expression" + $(mkRelDir ".") + $(mkRelFile "test039.juvix") + $(mkRelFile "out/test039.out") + ] diff --git a/tests/Compilation/positive/out/test039.out b/tests/Compilation/positive/out/test039.out new file mode 100644 index 0000000000..1d474d5255 --- /dev/null +++ b/tests/Compilation/positive/out/test039.out @@ -0,0 +1,2 @@ +false +true diff --git a/tests/Compilation/positive/test039.juvix b/tests/Compilation/positive/test039.juvix new file mode 100644 index 0000000000..47958220b1 --- /dev/null +++ b/tests/Compilation/positive/test039.juvix @@ -0,0 +1,22 @@ +-- Mutually recursive let expressions +module test039; + +open import Stdlib.Prelude; + +main : IO; +main := + let + Ty : Type; + Ty := Nat; + odd : _; + even : _; + unused : _; + odd zero := false; + odd (suc n) := not (even n); + unused := 123; + even zero := true; + even (suc n) := not (odd n); + plusOne : Ty → Ty; + plusOne n := n + 1; + in printBoolLn (odd (plusOne 13)) + >> printBoolLn (even (plusOne 12)); From 0e10226f1e0376af9f754466185bcbafcc852977 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 16 Mar 2023 17:28:29 +0100 Subject: [PATCH 04/11] format --- test/Compilation/Positive.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index f7692205bf..d9dcbd4778 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -247,5 +247,4 @@ tests = $(mkRelDir ".") $(mkRelFile "test039.juvix") $(mkRelFile "out/test039.out") - ] From b0e1954782e46970bcace964c5a2b859ff3ad595 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 16 Mar 2023 18:30:11 +0100 Subject: [PATCH 05/11] fix infotable --- src/Juvix/Compiler/Internal/Data/InfoTable.hs | 25 +++++++++++++------ tests/smoke/Commands/repl.smoke.yaml | 10 ++++++++ 2 files changed, 28 insertions(+), 7 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index eae54f2a3f..983513d5ba 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -73,9 +73,25 @@ extendWithReplExpression e = over infoFunctions ( HashMap.union - (HashMap.fromList [(f ^. funDefName, FunctionInfo f) | LetFunDef f <- universeBi e]) + ( HashMap.fromList + [ (f ^. funDefName, FunctionInfo f) + | f <- letFunctionDefs e + ] + ) ) +letFunctionDefs :: Data from => from -> [FunctionDef] +letFunctionDefs e = + concat + [ concatMap (toList . flattenClause) _letClauses + | Let {..} <- universeBi e + ] + where + flattenClause :: LetClause -> NonEmpty FunctionDef + flattenClause = \case + LetFunDef f -> pure f + LetMutualBlock (MutualBlock fs) -> fs + -- | moduleName ↦ infoTable type Cache = HashMap Name InfoTable @@ -117,14 +133,9 @@ buildTable1' m = do ] <> [ (f ^. funDefName, FunctionInfo f) | s <- filter (not . isInclude) ss, - Let {..} <- universeBi s, - f <- concatMap (toList . flattenClause) _letClauses + f <- letFunctionDefs s ] where - flattenClause :: LetClause -> NonEmpty FunctionDef - flattenClause = \case - LetFunDef f -> pure f - LetMutualBlock (MutualBlock fs) -> fs isInclude :: Statement -> Bool isInclude = \case StatementInclude {} -> True diff --git a/tests/smoke/Commands/repl.smoke.yaml b/tests/smoke/Commands/repl.smoke.yaml index a6e0814be8..a77704e027 100644 --- a/tests/smoke/Commands/repl.smoke.yaml +++ b/tests/smoke/Commands/repl.smoke.yaml @@ -118,6 +118,16 @@ tests: Nat exit-status: 0 + - name: eval-mutually-recursive-let-expression + command: + - juvix + - repl + stdin: "let even : Nat → Bool; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10" + stdout: + contains: + "true" + exit-status: 0 + - name: eval-let-expression command: - juvix From b8dc93797dc9bb7b227bb23f3ec625eb135d4caf Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 16 Mar 2023 19:03:50 +0100 Subject: [PATCH 06/11] explicitly print mutual blocks in Internal syntax --- src/Juvix/Compiler/Internal/Pretty/Base.hs | 10 +++++++++- src/Juvix/Data/CodeAnn.hs | 3 +++ src/Juvix/Data/Keyword/All.hs | 3 +++ src/Juvix/Extra/Strings.hs | 3 +++ 4 files changed, 18 insertions(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index 234eb1fe07..2f78f7aae9 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -91,9 +91,17 @@ instance PrettyCode Let where return $ kwLet <+> letClauses' <+> kwIn <+> letExpression' instance PrettyCode LetClause where + ppCode :: forall r. Member (Reader Options) r => LetClause -> Sem r (Doc Ann) ppCode = \case LetFunDef f -> ppCode f - LetMutualBlock b -> ppCode b + LetMutualBlock b -> ppMutual b + where + ppMutual :: MutualBlock -> Sem r (Doc Ann) + ppMutual m@(MutualBlock b) + | [_] <- toList b = ppCode b + | otherwise = do + b' <- ppCode m + return (kwMutual <+> braces (line <> indent' b' <> line)) ppPipeBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann) ppPipeBlock items = vsep <$> mapM (fmap (kwPipe <+>) . ppCode) items diff --git a/src/Juvix/Data/CodeAnn.hs b/src/Juvix/Data/CodeAnn.hs index f0cb9e93ec..77d7adf1be 100644 --- a/src/Juvix/Data/CodeAnn.hs +++ b/src/Juvix/Data/CodeAnn.hs @@ -56,6 +56,9 @@ primitive = annotate (AnnKind KNameAxiom) . pretty keyword :: Text -> Doc Ann keyword = annotate AnnKeyword . pretty +kwMutual :: Doc Ann +kwMutual = keyword Str.mutual + kwLambda :: Doc Ann kwLambda = keyword Str.lambdaUnicode diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs index f2f4d01881..e45057f021 100644 --- a/src/Juvix/Data/Keyword/All.hs +++ b/src/Juvix/Data/Keyword/All.hs @@ -210,3 +210,6 @@ kwVoid = asciiKw Str.void kwDollar :: Keyword kwDollar = asciiKw Str.dollar + +kwMutual :: Keyword +kwMutual = asciiKw Str.mutual diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 8020e90d86..9876d98b02 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -311,6 +311,9 @@ mod = "%" dollar :: (IsString s) => s dollar = "$" +mutual :: (IsString s) => s +mutual = "mutual" + if_ :: (IsString s) => s if_ = "if" From 032b6b86e0275bc527340f0a71cf2689bf1b8e2b Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 16 Mar 2023 19:34:14 +0100 Subject: [PATCH 07/11] fix inference for let mutual block --- .../FromInternal/Analysis/TypeChecking/Checker.hs | 11 +++++++---- test/Typecheck/Positive.hs | 6 +++++- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs index c9496b206c..dd5b2d7434 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs @@ -57,7 +57,7 @@ checkStatement :: Statement -> Sem r Statement checkStatement s = case s of - StatementFunction funs -> StatementFunction <$> runReader emptyLocalVars (checkMutualBlock funs) + StatementFunction funs -> StatementFunction <$> runReader emptyLocalVars (checkTopMutualBlock funs) StatementInductive ind -> StatementInductive <$> checkInductiveDef ind StatementInclude i -> StatementInclude <$> checkInclude i StatementAxiom ax -> do @@ -125,11 +125,11 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do withEmptyVars :: Sem (Reader LocalVars : r) a -> Sem r a withEmptyVars = runReader emptyLocalVars -checkMutualBlock :: +checkTopMutualBlock :: (Members '[Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r) => MutualBlock -> Sem r MutualBlock -checkMutualBlock (MutualBlock ds) = MutualBlock <$> runInferenceDefs (mapM checkFunctionDef ds) +checkTopMutualBlock (MutualBlock ds) = MutualBlock <$> runInferenceDefs (mapM checkFunctionDef ds) checkFunctionDef :: (Members '[Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Inference] r) => @@ -527,7 +527,10 @@ inferExpression' hint e = case e of goLetClause :: LetClause -> Sem r LetClause goLetClause = \case LetFunDef f -> LetFunDef <$> checkFunctionDef f - LetMutualBlock f -> LetMutualBlock <$> checkMutualBlock f + LetMutualBlock b -> LetMutualBlock <$> goMutualLet b + where + goMutualLet :: MutualBlock -> Sem r MutualBlock + goMutualLet (MutualBlock fs) = MutualBlock <$> mapM checkFunctionDef fs goHole :: Hole -> Sem r TypedExpression goHole h = do diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs index 82f0b6fdc5..e9d79834f7 100644 --- a/test/Typecheck/Positive.hs +++ b/test/Typecheck/Positive.hs @@ -201,7 +201,11 @@ tests = posTest "Type synonym inside let" $(mkRelDir "issue1879") - $(mkRelFile "LetSynonym.juvix") + $(mkRelFile "LetSynonym.juvix"), + posTest + "Mutual inference inside let" + $(mkRelDir ".") + $(mkRelFile "MutualLet.juvix") ] <> [ compilationTest t | t <- Compilation.tests, t ^. Compilation.name /= "Self-application" ] From 6cbd32a14a82d7c40ed3d754dde9deef9368c062 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 16 Mar 2023 19:34:38 +0100 Subject: [PATCH 08/11] format --- .../Translation/FromInternal/Analysis/TypeChecking/Checker.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs index dd5b2d7434..3c91b9ed5e 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs @@ -529,8 +529,8 @@ inferExpression' hint e = case e of LetFunDef f -> LetFunDef <$> checkFunctionDef f LetMutualBlock b -> LetMutualBlock <$> goMutualLet b where - goMutualLet :: MutualBlock -> Sem r MutualBlock - goMutualLet (MutualBlock fs) = MutualBlock <$> mapM checkFunctionDef fs + goMutualLet :: MutualBlock -> Sem r MutualBlock + goMutualLet (MutualBlock fs) = MutualBlock <$> mapM checkFunctionDef fs goHole :: Hole -> Sem r TypedExpression goHole h = do From 85a625c5ed6a80fe916103ddbe368ef5c3d569e8 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 16 Mar 2023 19:59:52 +0100 Subject: [PATCH 09/11] commit test file --- tests/positive/MutualLet.juvix | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 tests/positive/MutualLet.juvix diff --git a/tests/positive/MutualLet.juvix b/tests/positive/MutualLet.juvix new file mode 100644 index 0000000000..74aba9e6fd --- /dev/null +++ b/tests/positive/MutualLet.juvix @@ -0,0 +1,15 @@ +module MutualLet; + +open import Stdlib.Data.Nat; +open import Stdlib.Data.Bool; + +main : _; +main := + let + odd : _; + even : _; + odd zero := false; + odd (suc n) := not (even n); + even zero := true; + even (suc n) := not (odd n); + in even 5; From fb9a21be03628fabd3185d195850b3054f01f3ac Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 17 Mar 2023 11:04:08 +0100 Subject: [PATCH 10/11] revert involuntary test change --- tests/positive/issue1879/LetSynonym.juvix | 6 ------ 1 file changed, 6 deletions(-) diff --git a/tests/positive/issue1879/LetSynonym.juvix b/tests/positive/issue1879/LetSynonym.juvix index e520bc4633..ad7f61e091 100644 --- a/tests/positive/issue1879/LetSynonym.juvix +++ b/tests/positive/issue1879/LetSynonym.juvix @@ -11,11 +11,5 @@ module LetSynonym; A := T; x : A; x := t; - odd : _; - even : _; - odd zero := false; - odd (suc n) := even n; - even zero := true; - even (suc n) := odd n; in x; end; From 3a448a6f113fdaa9cd7c6dd6fb93d5d401821de2 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 17 Mar 2023 11:05:13 +0100 Subject: [PATCH 11/11] fix --- tests/positive/issue1879/LetSynonym.juvix | 2 -- 1 file changed, 2 deletions(-) diff --git a/tests/positive/issue1879/LetSynonym.juvix b/tests/positive/issue1879/LetSynonym.juvix index ad7f61e091..85da0dac4b 100644 --- a/tests/positive/issue1879/LetSynonym.juvix +++ b/tests/positive/issue1879/LetSynonym.juvix @@ -1,6 +1,4 @@ module LetSynonym; - open import Stdlib.Prelude; - type T := | t : T;