From 7b167caf242fc40d03f3f87e2721173f2f2d5060 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 14 Feb 2023 13:07:24 +0100 Subject: [PATCH 1/3] Add lambda type info --- src/Juvix/Compiler/Internal/Extra.hs | 15 ++++++++++++--- src/Juvix/Compiler/Internal/Language.hs | 6 ++++-- src/Juvix/Compiler/Internal/Pretty/Base.hs | 3 ++- .../Compiler/Internal/Translation/FromAbstract.hs | 5 ++++- .../Analysis/ArityChecking/Checker.hs | 11 +++++++---- .../FromInternal/Analysis/Positivity/Checker.hs | 2 +- .../FromInternal/Analysis/TypeChecking/Checker.hs | 6 ++++-- .../Analysis/TypeChecking/Data/Inference.hs | 9 ++++++--- 8 files changed, 40 insertions(+), 17 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index 99d815be5e..71f9acdf24 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -101,7 +101,10 @@ mkConcreteType = fmap ConcreteType . go b' <- go b ty' <- go ty return (ExpressionSimpleLambda (SimpleLambda v ty' b')) - ExpressionLambda (Lambda c) -> ExpressionLambda . Lambda <$> mapM goClause c + ExpressionLambda (Lambda c ty) -> do + let _lambdaType = ty >>= go + _lambdaClauses <- mapM goClause c + return (ExpressionLambda Lambda {..}) ExpressionFunction (Function l r) -> do l' <- goParam l r' <- go r @@ -201,7 +204,10 @@ mkPolyType = fmap PolyType . go ExpressionIden IdenConstructor {} -> return t ExpressionIden IdenAxiom {} -> return t ExpressionIden IdenVar {} -> return t - ExpressionLambda (Lambda c) -> ExpressionLambda . Lambda <$> mapM goClause c + ExpressionLambda (Lambda c ty) -> do + let _lambdaType = ty >>= go + _lambdaClauses <- mapM goClause c + return (ExpressionLambda Lambda {..}) ExpressionSimpleLambda (SimpleLambda v ty b) -> do b' <- go b ty' <- go ty @@ -219,7 +225,10 @@ instance HasExpressions LambdaClause where leafExpressions f (LambdaClause ps b) = LambdaClause ps <$> leafExpressions f b instance HasExpressions Lambda where - leafExpressions f = traverseOf lambdaClauses (traverse (leafExpressions f)) + leafExpressions f l = do + _lambdaClauses <- traverse (leafExpressions f) (l ^. lambdaClauses) + _lambdaType <- traverse (leafExpressions f) (l ^. lambdaType) + pure Lambda {..} instance HasExpressions Expression where leafExpressions f e = case e of diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index 429cced822..b453e94bbb 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -162,8 +162,10 @@ data Case = Case instance Hashable Case -newtype Lambda = Lambda - { _lambdaClauses :: NonEmpty LambdaClause +data Lambda = Lambda + { _lambdaClauses :: NonEmpty LambdaClause, + -- | The typechecker fills this field + _lambdaType :: Maybe Expression } deriving stock (Eq, Generic, Data) diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index 81c07f9569..9f50290a4c 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -107,7 +107,8 @@ instance PrettyCode LambdaClause where instance PrettyCode Lambda where ppCode Lambda {..} = do lambdaClauses' <- ppPipeBlock _lambdaClauses - return $ kwLambda <+> lambdaClauses' + lambdaType' <- mapM ppCode _lambdaType + return $ kwLambda <+> (fmap (kwColon <+>) lambdaType') lambdaClauses' instance PrettyCode a => PrettyCode (WithLoc a) where ppCode = ppCode . (^. withLocParam) diff --git a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs index 8019536797..8edd0aec75 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs @@ -288,7 +288,10 @@ goType e = case e of Abstract.ExpressionCase {} -> unsupported "case in types" goLambda :: forall r. (Members '[NameIdGen] r) => Abstract.Lambda -> Sem r Lambda -goLambda (Abstract.Lambda cl') = Lambda <$> mapM goClause cl' +goLambda (Abstract.Lambda cl') = do + _lambdaClauses <- mapM goClause cl' + let _lambdaType :: Maybe Expression = Nothing + return Lambda {..} where goClause :: Abstract.LambdaClause -> Sem r LambdaClause goClause (Abstract.LambdaClause ps b) = do 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 acfa02506f..214a3101d9 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs @@ -207,10 +207,10 @@ arityCase c = do -- types, it is ok to (partially) infer the arity of the lambda from the clause -- with the most patterns. arityLambda :: Lambda -> Arity -arityLambda (Lambda cl) = +arityLambda l = foldArity UnfoldedArity - { _ufoldArityParams = replicate (maximum1 (fmap numPatterns cl)) (ParamExplicit ArityUnknown), + { _ufoldArityParams = replicate (maximum1 (fmap numPatterns (l ^. lambdaClauses))) (ParamExplicit ArityUnknown), _ufoldArityRest = ArityRestUnknown } where @@ -382,7 +382,10 @@ checkLambda :: Arity -> Lambda -> Sem r Lambda -checkLambda ari (Lambda cl) = Lambda <$> mapM goClause cl +checkLambda ari l = do + let _lambdaType = l ^. lambdaType + _lambdaClauses <- mapM goClause (l ^. lambdaClauses) + return Lambda {..} where goClause :: LambdaClause -> Sem r LambdaClause goClause (LambdaClause ps b) = do @@ -409,7 +412,7 @@ checkLambda ari (Lambda cl) = Lambda <$> mapM goClause cl -- TODO. think what to do in this case return (pats, as) (_ : _, []) -> case rest of - ArityRestUnit -> error ("too many patterns in lambda: " <> ppTrace (Lambda cl) <> "\n" <> prettyText ari) + ArityRestUnit -> error ("too many patterns in lambda: " <> ppTrace l <> "\n" <> prettyText ari) ArityRestUnknown -> return (pats, []) idenArity :: (Members '[Reader LocalVars, Reader InfoTable] r) => Iden -> Sem r Arity 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 94c1b651c0..bd59f3a211 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -104,7 +104,7 @@ checkStrictlyPositiveOccurrences ty ctorName name recLimit ref = helper inside lamBody helperLambda :: Lambda -> Sem r () - helperLambda (Lambda cl) = mapM_ goClause cl + helperLambda l = mapM_ goClause (l ^. lambdaClauses) where goClause :: LambdaClause -> Sem r () goClause (LambdaClause _ b) = helper inside b 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 6bbf0f5cb3..0a6865bccf 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs @@ -573,11 +573,13 @@ inferExpression' hint e = case e of } goLambda :: Lambda -> Sem r TypedExpression - goLambda l@(Lambda cl) = do + goLambda l = do ty <- case hint of Just hi -> return hi Nothing -> ExpressionHole <$> freshHole (getLoc l) - l' <- Lambda <$> mapM (goClause ty) cl + _lambdaClauses <- mapM (goClause ty) (l ^. lambdaClauses) + let _lambdaType = Just ty + l' = Lambda {..} return TypedExpression { _typedType = ty, diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs index f74a673383..02de065a48 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs @@ -119,7 +119,10 @@ strongNormalize' = go return (LambdaClause p b') goLambda :: Lambda -> Sem r Lambda - goLambda (Lambda cl) = Lambda <$> mapM goClause cl + goLambda l = do + _lambdaClauses <- mapM goClause (l ^. lambdaClauses) + _lambdaType <- mapM go (l ^. lambdaType) + return Lambda {..} goSimpleLambda :: SimpleLambda -> Sem r SimpleLambda goSimpleLambda (SimpleLambda lamVar lamTy lamBody) = do @@ -342,9 +345,9 @@ re = reinterpret $ \case _ -> id bicheck (go l1 l2) (local' (go r1 r2)) | otherwise = err - + -- NOTE type is ignored, I think it is ok goLambda :: Lambda -> Lambda -> Sem r (Maybe MatchError) - goLambda (Lambda l1) (Lambda l2) = case zipExactMay (toList l1) (toList l2) of + goLambda (Lambda l1 _) (Lambda l2 _) = case zipExactMay (toList l1) (toList l2) of Just z -> asum <$> mapM (uncurry goClause) z _ -> err where From 289369b289f30e50e9414f1519483d94a72fd443 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 14 Feb 2023 13:14:41 +0100 Subject: [PATCH 2/3] fix printing of lambdas --- src/Juvix/Compiler/Internal/Pretty/Base.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index 9f50290a4c..c661f17914 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -108,7 +108,7 @@ instance PrettyCode Lambda where ppCode Lambda {..} = do lambdaClauses' <- ppPipeBlock _lambdaClauses lambdaType' <- mapM ppCode _lambdaType - return $ kwLambda <+> (fmap (kwColon <+>) lambdaType') lambdaClauses' + return $ kwLambda <+> (fmap (kwColon <+>) lambdaType') braces lambdaClauses' instance PrettyCode a => PrettyCode (WithLoc a) where ppCode = ppCode . (^. withLocParam) @@ -198,7 +198,7 @@ instance PrettyCode FunctionClause where funName <- ppCode (c ^. clauseName) clausePatterns' <- hsepMaybe <$> mapM ppCodeAtom (c ^. clausePatterns) clauseBody' <- ppCode (c ^. clauseBody) - return $ funName <+?> clausePatterns' <+> kwAssign <+> clauseBody' + return $ nest 2 (funName <+?> clausePatterns' <+> kwAssign <+> clauseBody') instance PrettyCode Backend where ppCode = \case From de27b5fde5b8e0fc5303d9fcc818a06087d6e550 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 14 Feb 2023 13:16:54 +0100 Subject: [PATCH 3/3] fix signature colon --- src/Juvix/Compiler/Internal/Pretty/Base.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index c661f17914..5d368357fe 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -188,7 +188,7 @@ instance PrettyCode FunctionDef where clauses' <- mapM ppCode (f ^. funDefClauses) return $ funDefName' - <+> kwColonColon + <+> kwColon <+> funDefType' <> line <> vsep (toList clauses')