From c7a8aacd18cadc5342255b58d9f81d906a49654e Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 13 Nov 2024 11:34:34 +0100 Subject: [PATCH 01/11] comment wip --- .../Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index f3095f8fad..0a9d96f415 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1263,6 +1263,7 @@ checkInductiveDef InductiveDef {..} = do -- field is checked with a local scope withLocalScope $ do name' <- bindVariableSymbol _fieldName + -- TODO: register name signature? return RecordField { _fieldType = type', From c0383e772460870c5516d64071b2e8fda4274b01 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 14 Nov 2024 09:47:51 +0100 Subject: [PATCH 02/11] wip --- .../Compiler/Concrete/Data/NameSignature/Builder.hs | 10 ++++++++++ .../Translation/FromParsed/Analysis/Scoping.hs | 11 +++++++++++ tests/Compilation/positive/test061.juvix | 4 ++-- 3 files changed, 23 insertions(+), 2 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 7c60131a55..689eace3d9 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -98,6 +98,16 @@ instance (SingI s) => HasNameSignature s (InductiveDef s) where mapM_ addInductiveParams (a ^. inductiveParameters) whenJust (a ^. inductiveType) addExpressionType +instance (SingI s) => HasNameSignature s (InductiveDef s, RecordField s) where + addArgs :: + forall r. + (Members '[NameSignatureBuilder s] r) => + (InductiveDef s, RecordField s) -> + Sem r () + addArgs (i, f) = do + mapM_ addConstructorParams (i ^. inductiveParameters) + + mkNameSignature :: forall s d r. (SingI s, Members '[Error ScoperError] r, HasNameSignature s d) => diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 0a9d96f415..4f2c966d28 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1208,8 +1208,19 @@ checkInductiveDef InductiveDef {..} = do registerNameSignature (inductiveName' ^. S.nameId) indDef forM_ inductiveConstructors' $ \c -> do registerNameSignature (c ^. constructorName . S.nameId) (indDef, c) + registerRecordFieldSignatures indDef c registerInductive @$> indDef where + registerRecordFieldSignatures :: InductiveDef 'Scoped -> ConstructorDef 'Scoped -> Sem r () + registerRecordFieldSignatures indDef c = + case c ^. constructorRhs of + ConstructorRhsRecord r -> + forM_ (r ^. rhsRecordStatements) $ \case + RecordStatementField f -> do + registerNameSignature (f ^. fieldName . S.nameId) (indDef, f) + _ -> return () + _ -> return () + -- note that the constructor name is not bound here checkConstructorDef :: S.Symbol -> S.Symbol -> ConstructorDef 'Parsed -> Sem r (ConstructorDef 'Scoped) checkConstructorDef inductiveName' constructorName' ConstructorDef {..} = do diff --git a/tests/Compilation/positive/test061.juvix b/tests/Compilation/positive/test061.juvix index a1849f140e..4aa0406cd0 100644 --- a/tests/Compilation/positive/test061.juvix +++ b/tests/Compilation/positive/test061.juvix @@ -33,7 +33,7 @@ g : {A : Type} → {{Show A}} → Nat := 5; instance showListI {A} {{Show' A}} : Show (List A) := mkShow@{ - show {A} : {{Show' A}} → List A → String + show : List A → String | nil := "nil" | (h :: t) := Show.show h ++str " :: " ++str show t }; @@ -41,7 +41,7 @@ showListI {A} {{Show' A}} : Show (List A) := instance showMaybeI {A} {{Show A}} : Show (Maybe A) := mkShow@{ - show {A} {{Show A}} : Maybe A → String + show : Maybe A → String | (just x) := "just (" ++str Show.show x ++str ")" | nothing := "nothing" }; From d7e01edc1adf09401bd2341abbf412b8518dee54 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 14 Nov 2024 11:35:32 +0100 Subject: [PATCH 03/11] wip --- .../Concrete/Data/NameSignature/Builder.hs | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 689eace3d9..2e4f843798 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -106,7 +106,23 @@ instance (SingI s) => HasNameSignature s (InductiveDef s, RecordField s) where Sem r () addArgs (i, f) = do mapM_ addConstructorParams (i ^. inductiveParameters) - + addArgument implicity Nothing Nothing indty + where + implicity :: IsImplicit + implicity + | isJust (i ^. inductiveTrait) = ImplicitInstance + | otherwise = Explicit + + indty :: ExpressionType s + indty = + case sing :: SStage s of + SParsed -> undefined + SScoped -> undefined + +{- let params = i ^. inductiveParameters . inductiveParametersNames + ind = ExpressionIdentifier (IdenInductive (info ^. constructorInfoInductive)) + saturatedTy = foldApplication ind (map (ExpressionIden . IdenVar) paramNames) + in saturatedTy -} mkNameSignature :: forall s d r. From cce456119023580ba364706c8e0f2c1e8d5832b2 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 14 Nov 2024 16:27:00 +0100 Subject: [PATCH 04/11] register field signature --- .../Concrete/Data/NameSignature/Builder.hs | 14 +------ src/Juvix/Compiler/Concrete/Language/Base.hs | 1 + .../FromParsed/Analysis/Scoping.hs | 3 ++ .../Concrete/Translation/FromSource.hs | 37 ++++++++++-------- src/Juvix/Compiler/Internal/Extra.hs | 7 ++-- .../Internal/Translation/FromConcrete.hs | 38 ++++++++++--------- 6 files changed, 53 insertions(+), 47 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 2e4f843798..0251f214ea 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -106,24 +106,14 @@ instance (SingI s) => HasNameSignature s (InductiveDef s, RecordField s) where Sem r () addArgs (i, f) = do mapM_ addConstructorParams (i ^. inductiveParameters) - addArgument implicity Nothing Nothing indty + addArgument implicity Nothing Nothing (f ^. fieldInductive) + addExpressionType (f ^. fieldType) where implicity :: IsImplicit implicity | isJust (i ^. inductiveTrait) = ImplicitInstance | otherwise = Explicit - indty :: ExpressionType s - indty = - case sing :: SStage s of - SParsed -> undefined - SScoped -> undefined - -{- let params = i ^. inductiveParameters . inductiveParametersNames - ind = ExpressionIdentifier (IdenInductive (info ^. constructorInfoInductive)) - saturatedTy = foldApplication ind (map (ExpressionIden . IdenVar) paramNames) - in saturatedTy -} - mkNameSignature :: forall s d r. (SingI s, Members '[Error ScoperError] r, HasNameSignature s d) => diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs index 4be4b13a1e..f3c06291d2 100644 --- a/src/Juvix/Compiler/Concrete/Language/Base.hs +++ b/src/Juvix/Compiler/Concrete/Language/Base.hs @@ -766,6 +766,7 @@ deriving stock instance Ord (RecordUpdateField 'Scoped) data RecordField (s :: Stage) = RecordField { _fieldName :: SymbolType s, + _fieldInductive :: ExpressionType s, _fieldIsImplicit :: IsImplicitField, _fieldColon :: Irrelevant (KeywordRef), _fieldType :: ExpressionType s, diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 4f2c966d28..4f2b0bb610 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1217,6 +1217,7 @@ checkInductiveDef InductiveDef {..} = do ConstructorRhsRecord r -> forM_ (r ^. rhsRecordStatements) $ \case RecordStatementField f -> do + traceM ("register: " <> prettyText (f ^. fieldName)) registerNameSignature (f ^. fieldName . S.nameId) (indDef, f) _ -> return () _ -> return () @@ -1270,6 +1271,7 @@ checkInductiveDef InductiveDef {..} = do checkField RecordField {..} = do doc' <- maybe (return Nothing) (checkJudoc >=> return . Just) _fieldDoc type' <- checkParseExpressionAtoms _fieldType + indName' <- checkParseExpressionAtoms _fieldInductive -- Since we don't allow dependent types in constructor types, each -- field is checked with a local scope withLocalScope $ do @@ -1280,6 +1282,7 @@ checkInductiveDef InductiveDef {..} = do { _fieldType = type', _fieldName = name', _fieldDoc = doc', + _fieldInductive = indName', .. } diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 3620253ea2..a621a3a314 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -1539,8 +1539,15 @@ inductiveDef _inductiveBuiltin = do optional (kw kwColon >> parseExpressionAtoms) P. "" _inductiveAssignKw <- Irrelevant <$> kw kwAssign P. " "" return InductiveDef {..} @@ -1574,8 +1581,8 @@ rhsGadt = P.label "" $ do _rhsGadtType <- parseExpressionAtoms P. "" return RhsGadt {..} -recordField :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RecordField 'Parsed) -recordField = do +recordField :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ExpressionAtoms 'Parsed -> ParsecS r (RecordField 'Parsed) +recordField _fieldInductive = do _fieldDoc <- optional stashJudoc >> getJudoc _fieldPragmas <- optional stashPragmas >> getPragmas _fieldBuiltin <- optional builtinRecordField @@ -1592,19 +1599,19 @@ rhsAdt = P.label "" $ do _rhsAdtArguments <- many atomicExpression return RhsAdt {..} -rhsRecord :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RhsRecord 'Parsed) -rhsRecord = P.label "" $ do +rhsRecord :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ExpressionAtoms 'Parsed -> ParsecS r (RhsRecord 'Parsed) +rhsRecord indType = P.label "" $ do a <- optional (kw kwAt) l <- kw delimBraceL - _rhsRecordStatements <- P.sepEndBy recordStatement semicolon + _rhsRecordStatements <- P.sepEndBy (recordStatement indType) semicolon r <- kw delimBraceR let _rhsRecordDelim = Irrelevant (a, l, r) return RhsRecord {..} -recordStatement :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RecordStatement 'Parsed) -recordStatement = +recordStatement :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ExpressionAtoms 'Parsed -> ParsecS r (RecordStatement 'Parsed) +recordStatement indType = RecordStatementSyntax <$> syntax - <|> RecordStatementField <$> recordField + <|> RecordStatementField <$> recordField indType where syntax :: ParsecS r (RecordSyntaxDef 'Parsed) syntax = do @@ -1612,18 +1619,18 @@ recordStatement = RecordSyntaxIterator <$> iteratorSyntaxDef syn <|> RecordSyntaxOperator <$> operatorSyntaxDef syn -pconstructorRhs :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (ConstructorRhs 'Parsed) -pconstructorRhs = +pconstructorRhs :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ExpressionAtoms 'Parsed -> ParsecS r (ConstructorRhs 'Parsed) +pconstructorRhs indType = ConstructorRhsGadt <$> rhsGadt - <|> ConstructorRhsRecord <$> rhsRecord + <|> ConstructorRhsRecord <$> rhsRecord indType <|> ConstructorRhsAdt <$> rhsAdt -constructorDef :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Symbol -> Irrelevant (Maybe KeywordRef) -> ParsecS r (ConstructorDef 'Parsed) -constructorDef _constructorInductiveName _constructorPipe = do +constructorDef :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ExpressionAtoms 'Parsed -> Symbol -> Irrelevant (Maybe KeywordRef) -> ParsecS r (ConstructorDef 'Parsed) +constructorDef indType _constructorInductiveName _constructorPipe = do _constructorDoc <- optional stashJudoc >> getJudoc _constructorPragmas <- optional stashPragmas >> getPragmas _constructorName <- symbol P. "" - _constructorRhs <- pconstructorRhs + _constructorRhs <- pconstructorRhs indType return ConstructorDef {..} wildcard :: (Members '[ParserResultBuilder] r) => ParsecS r Wildcard diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index ebefec17b4..aed3b5656c 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -114,11 +114,12 @@ genFieldProjection :: ProjectionKind -> FunctionName -> Maybe BuiltinFunction -> + [ArgInfo] -> Maybe Pragmas -> ConstructorInfo -> Int -> Sem r FunctionDef -genFieldProjection kind _funDefName _funDefBuiltin mpragmas info fieldIx = do +genFieldProjection kind _funDefName _funDefBuiltin _funDefArgsInfo mpragmas info fieldIx = do body' <- genBody let (inductiveParams, constrArgs) = constructorArgTypes info saturatedTy :: FunctionParameter = unnamedParameter' constructorImplicity (constructorReturnType info) @@ -132,7 +133,6 @@ genFieldProjection kind _funDefName _funDefBuiltin mpragmas info fieldIx = do if | kind == ProjectionCoercion -> Just IsInstanceCoercionCoercion | otherwise -> Nothing, - _funDefArgsInfo = mempty, _funDefPragmas = maybe (mempty {_pragmasInline = Just InlineAlways}) @@ -142,7 +142,8 @@ genFieldProjection kind _funDefName _funDefBuiltin mpragmas info fieldIx = do _funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy, _funDefDocComment = Nothing, _funDefName, - _funDefBuiltin + _funDefBuiltin, + _funDefArgsInfo } where constructorImplicity :: IsImplicit diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index f911adfac9..093e0a87ff 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -346,25 +346,44 @@ goAxiomInductive = \case goProjectionDef :: forall r. - (Members '[NameIdGen, Error ScoperError, State ConstructorInfos, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, Reader Pragmas, NameIdGen, Error ScoperError, State ConstructorInfos, Reader S.InfoTable] r) => ProjectionDef 'Scoped -> Sem r Internal.FunctionDef goProjectionDef ProjectionDef {..} = do let c = goSymbol _projectionConstructor info <- gets (^?! constructorInfos . at c . _Just) + let field = goSymbol _projectionField + msig <- asks (^. S.infoNameSigs . at (field ^. Internal.nameId)) + argInfos <- maybe (return mempty) (fmap toList . goNameSignature) msig fun <- Internal.genFieldProjection _projectionKind - (goSymbol _projectionField) + field ( (^. withLocParam) <$> _projectionFieldBuiltin ) + argInfos (fmap (^. withLocParam . withSourceValue) _projectionPragmas) info _projectionFieldIx whenJust (fun ^. Internal.funDefBuiltin) (checkBuiltinFunction fun) return fun +goNameSignature :: forall r. (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => NameSignature 'Scoped -> Sem r [Internal.ArgInfo] +goNameSignature = mconcatMapM (fmap toList . goBlock) . (^. nameSignatureArgs) + where + goBlock :: NameBlock 'Scoped -> Sem r (NonEmpty Internal.ArgInfo) + goBlock blk = mapM goItem (blk ^. nameBlockItems) + where + goItem :: NameItem 'Scoped -> Sem r Internal.ArgInfo + goItem i = do + _argInfoDefault' <- mapM goExpression (i ^? nameItemDefault . _Just . argDefaultValue) + return + Internal.ArgInfo + { _argInfoDefault = _argInfoDefault', + _argInfoName = goSymbol <$> (i ^. nameItemSymbol) + } + goFunctionDef :: forall r. (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) => @@ -389,21 +408,6 @@ goFunctionDef FunctionDef {..} = do whenJust _signBuiltin (checkBuiltinFunction fun . (^. withLocParam)) return fun where - goNameSignature :: NameSignature 'Scoped -> Sem r [Internal.ArgInfo] - goNameSignature = mconcatMapM (fmap toList . goBlock) . (^. nameSignatureArgs) - where - goBlock :: NameBlock 'Scoped -> Sem r (NonEmpty Internal.ArgInfo) - goBlock blk = mapM goItem (blk ^. nameBlockItems) - where - goItem :: NameItem 'Scoped -> Sem r Internal.ArgInfo - goItem i = do - _argInfoDefault' <- mapM goExpression (i ^? nameItemDefault . _Just . argDefaultValue) - return - Internal.ArgInfo - { _argInfoDefault = _argInfoDefault', - _argInfoName = goSymbol <$> (i ^. nameItemSymbol) - } - goBody :: Sem r Internal.Expression goBody = do commonPatterns <- concatMapM (fmap toList . argToPattern) _signArgs From f7987f84a6b24834ec40f77b9dbf639d806bef0a Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 15 Nov 2024 13:34:55 +0100 Subject: [PATCH 05/11] name signatures for record projections --- .../Concrete/Data/NameSignature/Builder.hs | 15 +- src/Juvix/Compiler/Concrete/Language/Base.hs | 3 +- .../FromParsed/Analysis/Scoping.hs | 175 +++++++++++++----- .../Concrete/Translation/FromSource.hs | 32 ++-- 4 files changed, 154 insertions(+), 71 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 0251f214ea..7ef1677d59 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -98,21 +98,14 @@ instance (SingI s) => HasNameSignature s (InductiveDef s) where mapM_ addInductiveParams (a ^. inductiveParameters) whenJust (a ^. inductiveType) addExpressionType -instance (SingI s) => HasNameSignature s (InductiveDef s, RecordField s) where +instance (SingI s) => HasNameSignature s (ProjectionDef s) where addArgs :: forall r. (Members '[NameSignatureBuilder s] r) => - (InductiveDef s, RecordField s) -> + ProjectionDef s -> Sem r () - addArgs (i, f) = do - mapM_ addConstructorParams (i ^. inductiveParameters) - addArgument implicity Nothing Nothing (f ^. fieldInductive) - addExpressionType (f ^. fieldType) - where - implicity :: IsImplicit - implicity - | isJust (i ^. inductiveTrait) = ImplicitInstance - | otherwise = Explicit + addArgs p = do + addExpressionType (p ^. projectionType) mkNameSignature :: forall s d r. diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs index f3c06291d2..9a108f77cb 100644 --- a/src/Juvix/Compiler/Concrete/Language/Base.hs +++ b/src/Juvix/Compiler/Concrete/Language/Base.hs @@ -309,6 +309,7 @@ deriving stock instance Ord (Statement 'Scoped) data ProjectionDef s = ProjectionDef { _projectionConstructor :: S.Symbol, _projectionField :: SymbolType s, + _projectionType :: ExpressionType s, _projectionKind :: ProjectionKind, _projectionFieldIx :: Int, _projectionFieldBuiltin :: Maybe (WithLoc BuiltinFunction), @@ -766,7 +767,6 @@ deriving stock instance Ord (RecordUpdateField 'Scoped) data RecordField (s :: Stage) = RecordField { _fieldName :: SymbolType s, - _fieldInductive :: ExpressionType s, _fieldIsImplicit :: IsImplicitField, _fieldColon :: Irrelevant (KeywordRef), _fieldType :: ExpressionType s, @@ -932,6 +932,7 @@ data InductiveDef (s :: Stage) = InductiveDef _inductiveName :: InductiveName s, _inductiveParameters :: [InductiveParameters s], _inductiveType :: Maybe (ExpressionType s), + _inductiveTypeApplied :: ExpressionType s, _inductiveConstructors :: NonEmpty (ConstructorDef s), _inductivePositive :: Maybe KeywordRef, _inductiveTrait :: Maybe KeywordRef diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 4f2b0bb610..61f31f3ed9 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -27,6 +27,7 @@ import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context qualified as import Juvix.Compiler.Pipeline.EntryPoint import Juvix.Compiler.Store.Scoped.Language as Store import Juvix.Data.FixityInfo qualified as FI +import Juvix.Data.Keyword.All qualified as KW import Juvix.Prelude scopeCheck :: @@ -155,25 +156,6 @@ scopeCheckOpenModule = mapError (JuvixError @ScoperError) . checkOpenModule freshVariable :: (Members '[NameIdGen, State ScoperSyntax, State Scope, State ScoperState] r) => Symbol -> Sem r S.Symbol freshVariable = freshSymbol KNameLocal KNameLocal -checkProjectionDef :: - forall r. - (Members '[Error ScoperError, InfoTableBuilder, Reader PackageId, Reader ScopeParameters, Reader InfoTable, Reader BindingStrategy, State Scope, State ScoperState, NameIdGen, State ScoperSyntax] r) => - ProjectionDef 'Parsed -> - Sem r (ProjectionDef 'Scoped) -checkProjectionDef p = do - _projectionField <- getReservedDefinitionSymbol (p ^. projectionField) - _projectionDoc <- maybe (return Nothing) (checkJudoc >=> return . Just) (p ^. projectionDoc) - return - ProjectionDef - { _projectionFieldIx = p ^. projectionFieldIx, - _projectionConstructor = p ^. projectionConstructor, - _projectionFieldBuiltin = p ^. projectionFieldBuiltin, - _projectionPragmas = p ^. projectionPragmas, - _projectionKind = p ^. projectionKind, - _projectionField, - _projectionDoc - } - freshSymbol :: forall r. (Members '[State Scope, State ScoperState, NameIdGen, State ScoperSyntax] r) => @@ -261,6 +243,13 @@ registerConstructorSignature uid sig = do modify' (set (scoperScopedConstructorFields . at uid) (Just sig)) registerConstructorSig uid sig +registerProjectionSignature :: + (Members '[State ScoperState, Error ScoperError, InfoTableBuilder] r) => + ProjectionDef 'Scoped -> + Sem r () +registerProjectionSignature p = + registerNameSignature (p ^. projectionField . S.nameId) p + reserveSymbolOfNameSpace :: forall (ns :: NameSpace) r. ( Members @@ -402,12 +391,9 @@ reserveProjectionSymbol :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, State ScoperState] r) => ProjectionDef 'Parsed -> Sem r S.Symbol -reserveProjectionSymbol d = - reserveSymbolOf - SKNameFunction - Nothing - (toBuiltinPrim <$> d ^. projectionFieldBuiltin) - (d ^. projectionField) +reserveProjectionSymbol d = do + sym <- reserveSymbolSignatureOf SKNameFunction d (toBuiltinPrim <$> d ^. projectionFieldBuiltin) (d ^. projectionField) + return sym reserveConstructorSymbol :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => @@ -1180,9 +1166,10 @@ checkInductiveDef InductiveDef {..} = do i <- bindInductiveSymbol _inductiveName cs <- mapM (bindConstructorSymbol . (^. constructorName)) _inductiveConstructors return (i, cs) - (inductiveParameters', inductiveType', inductiveDoc', inductiveConstructors') <- withLocalScope $ do + (inductiveParameters', inductiveType', inductiveTypeApplied', inductiveDoc', inductiveConstructors') <- withLocalScope $ do inductiveParameters' <- mapM checkInductiveParameters _inductiveParameters inductiveType' <- mapM checkParseExpressionAtoms _inductiveType + inductiveTypeApplied' <- checkParseExpressionAtoms _inductiveTypeApplied inductiveDoc' <- mapM checkJudoc _inductiveDoc inductiveConstructors' <- nonEmpty' @@ -1190,7 +1177,7 @@ checkInductiveDef InductiveDef {..} = do [ checkConstructorDef inductiveName' cname cdef | (cname, cdef) <- zipExact (toList constructorNames') (toList _inductiveConstructors) ] - return (inductiveParameters', inductiveType', inductiveDoc', inductiveConstructors') + return (inductiveParameters', inductiveType', inductiveTypeApplied', inductiveDoc', inductiveConstructors') let indDef = InductiveDef { _inductiveName = inductiveName', @@ -1198,6 +1185,7 @@ checkInductiveDef InductiveDef {..} = do _inductivePragmas = _inductivePragmas, _inductiveParameters = inductiveParameters', _inductiveType = inductiveType', + _inductiveTypeApplied = inductiveTypeApplied', _inductiveConstructors = inductiveConstructors', _inductiveBuiltin, _inductivePositive, @@ -1208,20 +1196,8 @@ checkInductiveDef InductiveDef {..} = do registerNameSignature (inductiveName' ^. S.nameId) indDef forM_ inductiveConstructors' $ \c -> do registerNameSignature (c ^. constructorName . S.nameId) (indDef, c) - registerRecordFieldSignatures indDef c registerInductive @$> indDef where - registerRecordFieldSignatures :: InductiveDef 'Scoped -> ConstructorDef 'Scoped -> Sem r () - registerRecordFieldSignatures indDef c = - case c ^. constructorRhs of - ConstructorRhsRecord r -> - forM_ (r ^. rhsRecordStatements) $ \case - RecordStatementField f -> do - traceM ("register: " <> prettyText (f ^. fieldName)) - registerNameSignature (f ^. fieldName . S.nameId) (indDef, f) - _ -> return () - _ -> return () - -- note that the constructor name is not bound here checkConstructorDef :: S.Symbol -> S.Symbol -> ConstructorDef 'Parsed -> Sem r (ConstructorDef 'Scoped) checkConstructorDef inductiveName' constructorName' ConstructorDef {..} = do @@ -1271,18 +1247,15 @@ checkInductiveDef InductiveDef {..} = do checkField RecordField {..} = do doc' <- maybe (return Nothing) (checkJudoc >=> return . Just) _fieldDoc type' <- checkParseExpressionAtoms _fieldType - indName' <- checkParseExpressionAtoms _fieldInductive -- Since we don't allow dependent types in constructor types, each -- field is checked with a local scope withLocalScope $ do name' <- bindVariableSymbol _fieldName - -- TODO: register name signature? return RecordField { _fieldType = type', _fieldName = name', _fieldDoc = doc', - _fieldInductive = indName', .. } @@ -1303,6 +1276,29 @@ checkInductiveDef InductiveDef {..} = do _rhsGadtColon } +checkProjectionDef :: + forall r. + (Members '[HighlightBuilder, Error ScoperError, InfoTableBuilder, Reader PackageId, Reader ScopeParameters, Reader InfoTable, Reader BindingStrategy, State Scope, State ScoperState, NameIdGen, State ScoperSyntax] r) => + ProjectionDef 'Parsed -> + Sem r (ProjectionDef 'Scoped) +checkProjectionDef p = do + _projectionField <- getReservedDefinitionSymbol (p ^. projectionField) + _projectionType <- checkParseExpressionAtoms (p ^. projectionType) + _projectionDoc <- maybe (return Nothing) (checkJudoc >=> return . Just) (p ^. projectionDoc) + let p' = + ProjectionDef + { _projectionFieldIx = p ^. projectionFieldIx, + _projectionConstructor = p ^. projectionConstructor, + _projectionFieldBuiltin = p ^. projectionFieldBuiltin, + _projectionPragmas = p ^. projectionPragmas, + _projectionKind = p ^. projectionKind, + _projectionField, + _projectionType, + _projectionDoc + } + registerProjectionSignature p' + return p' + topBindings :: Sem (Reader BindingStrategy ': r) a -> Sem r a topBindings = runReader BindingTop @@ -1506,7 +1502,7 @@ checkSections sec = topBindings helper goDefinitions :: DefinitionsSection 'Parsed -> Sem r' (DefinitionsSection 'Scoped) goDefinitions DefinitionsSection {..} = goDefs [] [] (toList _definitionsSection) where - -- This functions go through a section reserving definitions and + -- This function goes through a section reserving definitions and -- collecting inductive modules. It breaks a section when the -- collected inductive modules are non-empty (there were some -- inductive definitions) and the next definition is a function @@ -1715,6 +1711,7 @@ checkSections sec = topBindings helper ProjectionDef { _projectionConstructor = headConstr, _projectionField = field ^. fieldName, + _projectionType = mkProjectionType (field ^. fieldType), _projectionFieldIx = idx, _projectionKind = kind, _projectionFieldBuiltin = field ^. fieldBuiltin, @@ -1740,6 +1737,98 @@ checkSections sec = topBindings helper p2' ) + mkProjectionType :: ExpressionType 'Parsed -> ExpressionType 'Parsed + mkProjectionType ty = + foldr mkFun target params + where + params = map mkFunctionParameters $ i ^. inductiveParameters + target = mkFun (mkInstanceParameter (i ^. inductiveTypeApplied)) ty + + mkFun :: FunctionParameters 'Parsed -> ExpressionType 'Parsed -> ExpressionType 'Parsed + mkFun params tgt = + ExpressionAtoms + { _expressionAtoms = + NonEmpty.singleton $ + AtomFunction $ + Function + { _funParameters = params, + _funReturn = tgt, + _funKw = funkw + }, + _expressionAtomsLoc = Irrelevant $ getLoc (i ^. inductiveName) + } + where + funkw = + KeywordRef + { _keywordRefKeyword = KW.kwRightArrow, + _keywordRefInterval = getLoc (i ^. inductiveName), + _keywordRefUnicode = Ascii + } + + mkFunctionParameters :: InductiveParameters 'Parsed -> FunctionParameters 'Parsed + mkFunctionParameters InductiveParameters {..} = + FunctionParameters + { _paramNames = map FunctionParameterName $ toList _inductiveParametersNames, + _paramImplicit = Implicit, + _paramDelims = Irrelevant (Just (leftBrace, rightBrace)), + _paramColon = Irrelevant Nothing, + _paramType = maybe univ (^. inductiveParametersType) _inductiveParametersRhs + } + where + univ :: ExpressionAtoms 'Parsed + univ = + ExpressionAtoms + { _expressionAtoms = + NonEmpty.singleton $ + AtomUniverse $ + mkUniverse (Just smallLevel) (getLoc (i ^. inductiveName)), + _expressionAtomsLoc = Irrelevant $ getLoc (i ^. inductiveName) + } + + leftBrace :: KeywordRef + leftBrace = + KeywordRef + { _keywordRefKeyword = KW.delimBraceL, + _keywordRefInterval = getLoc (i ^. inductiveName), + _keywordRefUnicode = Ascii + } + + rightBrace :: KeywordRef + rightBrace = + KeywordRef + { _keywordRefKeyword = KW.delimBraceR, + _keywordRefInterval = getLoc (i ^. inductiveName), + _keywordRefUnicode = Ascii + } + + mkInstanceParameter :: ExpressionType 'Parsed -> FunctionParameters 'Parsed + mkInstanceParameter ty = + FunctionParameters + { _paramNames = [FunctionParameterName wildcard], + _paramImplicit = ImplicitInstance, + _paramDelims = Irrelevant (Just (leftDoubleBrace, rightDoubleBrace)), + _paramColon = Irrelevant Nothing, + _paramType = ty + } + where + wildcard = WithLoc (getLoc (i ^. inductiveName)) "_self" + + leftDoubleBrace :: KeywordRef + leftDoubleBrace = + KeywordRef + { _keywordRefKeyword = KW.delimDoubleBraceL, + _keywordRefInterval = getLoc (i ^. inductiveName), + _keywordRefUnicode = Ascii + } + + rightDoubleBrace :: KeywordRef + rightDoubleBrace = + KeywordRef + { _keywordRefKeyword = KW.delimDoubleBraceR, + _keywordRefInterval = getLoc (i ^. inductiveName), + _keywordRefUnicode = Ascii + } + getFields :: Sem (Fail ': s') [RecordStatement 'Parsed] getFields = case i ^. inductiveConstructors of c :| [] -> case c ^. constructorRhs of diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index a621a3a314..fdce76faac 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -1541,13 +1541,13 @@ inductiveDef _inductiveBuiltin = do _inductiveAssignKw <- Irrelevant <$> kw kwAssign P. " "" return InductiveDef {..} @@ -1581,8 +1581,8 @@ rhsGadt = P.label "" $ do _rhsGadtType <- parseExpressionAtoms P. "" return RhsGadt {..} -recordField :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ExpressionAtoms 'Parsed -> ParsecS r (RecordField 'Parsed) -recordField _fieldInductive = do +recordField :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RecordField 'Parsed) +recordField = do _fieldDoc <- optional stashJudoc >> getJudoc _fieldPragmas <- optional stashPragmas >> getPragmas _fieldBuiltin <- optional builtinRecordField @@ -1599,19 +1599,19 @@ rhsAdt = P.label "" $ do _rhsAdtArguments <- many atomicExpression return RhsAdt {..} -rhsRecord :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ExpressionAtoms 'Parsed -> ParsecS r (RhsRecord 'Parsed) -rhsRecord indType = P.label "" $ do +rhsRecord :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RhsRecord 'Parsed) +rhsRecord = P.label "" $ do a <- optional (kw kwAt) l <- kw delimBraceL - _rhsRecordStatements <- P.sepEndBy (recordStatement indType) semicolon + _rhsRecordStatements <- P.sepEndBy recordStatement semicolon r <- kw delimBraceR let _rhsRecordDelim = Irrelevant (a, l, r) return RhsRecord {..} -recordStatement :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ExpressionAtoms 'Parsed -> ParsecS r (RecordStatement 'Parsed) -recordStatement indType = +recordStatement :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RecordStatement 'Parsed) +recordStatement = RecordStatementSyntax <$> syntax - <|> RecordStatementField <$> recordField indType + <|> RecordStatementField <$> recordField where syntax :: ParsecS r (RecordSyntaxDef 'Parsed) syntax = do @@ -1619,18 +1619,18 @@ recordStatement indType = RecordSyntaxIterator <$> iteratorSyntaxDef syn <|> RecordSyntaxOperator <$> operatorSyntaxDef syn -pconstructorRhs :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ExpressionAtoms 'Parsed -> ParsecS r (ConstructorRhs 'Parsed) -pconstructorRhs indType = +pconstructorRhs :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (ConstructorRhs 'Parsed) +pconstructorRhs = ConstructorRhsGadt <$> rhsGadt - <|> ConstructorRhsRecord <$> rhsRecord indType + <|> ConstructorRhsRecord <$> rhsRecord <|> ConstructorRhsAdt <$> rhsAdt -constructorDef :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ExpressionAtoms 'Parsed -> Symbol -> Irrelevant (Maybe KeywordRef) -> ParsecS r (ConstructorDef 'Parsed) -constructorDef indType _constructorInductiveName _constructorPipe = do +constructorDef :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Symbol -> Irrelevant (Maybe KeywordRef) -> ParsecS r (ConstructorDef 'Parsed) +constructorDef _constructorInductiveName _constructorPipe = do _constructorDoc <- optional stashJudoc >> getJudoc _constructorPragmas <- optional stashPragmas >> getPragmas _constructorName <- symbol P. "" - _constructorRhs <- pconstructorRhs indType + _constructorRhs <- pconstructorRhs return ConstructorDef {..} wildcard :: (Members '[ParserResultBuilder] r) => ParsecS r Wildcard From b51b40f4cd5e1ea25d2a4cfc8f25de4e86b5bb3c Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 15 Nov 2024 13:37:10 +0100 Subject: [PATCH 06/11] add test --- test/Scope/Positive.hs | 4 ++++ tests/positive/RecordProjectionSignature.juvix | 8 ++++++++ 2 files changed, 12 insertions(+) create mode 100644 tests/positive/RecordProjectionSignature.juvix diff --git a/test/Scope/Positive.hs b/test/Scope/Positive.hs index 999613e30a..37b2dd9c25 100644 --- a/test/Scope/Positive.hs +++ b/test/Scope/Positive.hs @@ -250,6 +250,10 @@ tests = "Named argument puns" $(mkRelDir ".") $(mkRelFile "Puns.juvix"), + posTest + "Record projection signature" + $(mkRelDir ".") + $(mkRelFile "RecordProjectionSignature.juvix"), posTest "Confluent imports" $(mkRelDir "ConfluentScoping") diff --git a/tests/positive/RecordProjectionSignature.juvix b/tests/positive/RecordProjectionSignature.juvix new file mode 100644 index 0000000000..09905813be --- /dev/null +++ b/tests/positive/RecordProjectionSignature.juvix @@ -0,0 +1,8 @@ +module RecordProjectionSignature; + +import Stdlib.Data.Nat open; + +trait +type R A := mkR@{fun : (n : A) -> A}; + +f {{R Nat}} : Nat := R.fun@{n := 1}; From bddaed08da219113012166971edb2adb44a0b55f Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 15 Nov 2024 13:51:17 +0100 Subject: [PATCH 07/11] use projection type in Internal --- .../Translation/FromParsed/Analysis/Scoping.hs | 13 +++++++++---- src/Juvix/Compiler/Internal/Extra.hs | 10 +++------- .../Compiler/Internal/Translation/FromConcrete.hs | 2 ++ 3 files changed, 14 insertions(+), 11 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 61f31f3ed9..176f5ce29f 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1742,7 +1742,7 @@ checkSections sec = topBindings helper foldr mkFun target params where params = map mkFunctionParameters $ i ^. inductiveParameters - target = mkFun (mkInstanceParameter (i ^. inductiveTypeApplied)) ty + target = mkFun (mkRecordParameter (i ^. inductiveTypeApplied)) ty mkFun :: FunctionParameters 'Parsed -> ExpressionType 'Parsed -> ExpressionType 'Parsed mkFun params tgt = @@ -1801,11 +1801,11 @@ checkSections sec = topBindings helper _keywordRefUnicode = Ascii } - mkInstanceParameter :: ExpressionType 'Parsed -> FunctionParameters 'Parsed - mkInstanceParameter ty = + mkRecordParameter :: ExpressionType 'Parsed -> FunctionParameters 'Parsed + mkRecordParameter ty = FunctionParameters { _paramNames = [FunctionParameterName wildcard], - _paramImplicit = ImplicitInstance, + _paramImplicit = implicity, _paramDelims = Irrelevant (Just (leftDoubleBrace, rightDoubleBrace)), _paramColon = Irrelevant Nothing, _paramType = ty @@ -1813,6 +1813,11 @@ checkSections sec = topBindings helper where wildcard = WithLoc (getLoc (i ^. inductiveName)) "_self" + implicity :: IsImplicit + implicity + | isJust (i ^. inductiveTrait) = ImplicitInstance + | otherwise = Explicit + leftDoubleBrace :: KeywordRef leftDoubleBrace = KeywordRef diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index aed3b5656c..f1f3d133d7 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -113,19 +113,15 @@ genFieldProjection :: (Members '[NameIdGen] r) => ProjectionKind -> FunctionName -> + Expression -> Maybe BuiltinFunction -> [ArgInfo] -> Maybe Pragmas -> ConstructorInfo -> Int -> Sem r FunctionDef -genFieldProjection kind _funDefName _funDefBuiltin _funDefArgsInfo mpragmas info fieldIx = do +genFieldProjection kind _funDefName _funDefType _funDefBuiltin _funDefArgsInfo mpragmas info fieldIx = do body' <- genBody - let (inductiveParams, constrArgs) = constructorArgTypes info - saturatedTy :: FunctionParameter = unnamedParameter' constructorImplicity (constructorReturnType info) - inductiveArgs = map inductiveToFunctionParam inductiveParams - param = constrArgs !! fieldIx - retTy = param ^. paramType cloneFunctionDefSameName FunctionDef { _funDefTerminating = False, @@ -139,8 +135,8 @@ genFieldProjection kind _funDefName _funDefBuiltin _funDefArgsInfo mpragmas info (over pragmasInline (maybe (Just InlineAlways) Just)) mpragmas, _funDefBody = body', - _funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy, _funDefDocComment = Nothing, + _funDefType, _funDefName, _funDefBuiltin, _funDefArgsInfo diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 093e0a87ff..7ef0bcd05d 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -355,10 +355,12 @@ goProjectionDef ProjectionDef {..} = do let field = goSymbol _projectionField msig <- asks (^. S.infoNameSigs . at (field ^. Internal.nameId)) argInfos <- maybe (return mempty) (fmap toList . goNameSignature) msig + projType <- goExpression _projectionType fun <- Internal.genFieldProjection _projectionKind field + projType ( (^. withLocParam) <$> _projectionFieldBuiltin ) From 10997625e6d111f81bc14aba861b016075d13976 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 15 Nov 2024 13:56:57 +0100 Subject: [PATCH 08/11] fix infixities --- src/Juvix/Compiler/Concrete/Translation/FromSource.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index fdce76faac..707430f5df 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -1541,9 +1541,14 @@ inductiveDef _inductiveBuiltin = do _inductiveAssignKw <- Irrelevant <$> kw kwAssign P. " Date: Fri, 15 Nov 2024 14:02:36 +0100 Subject: [PATCH 09/11] fix formatting --- tests/positive/RecordProjectionSignature.juvix | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/positive/RecordProjectionSignature.juvix b/tests/positive/RecordProjectionSignature.juvix index 09905813be..db7facb8fd 100644 --- a/tests/positive/RecordProjectionSignature.juvix +++ b/tests/positive/RecordProjectionSignature.juvix @@ -5,4 +5,7 @@ import Stdlib.Data.Nat open; trait type R A := mkR@{fun : (n : A) -> A}; -f {{R Nat}} : Nat := R.fun@{n := 1}; +f {{R Nat}} : Nat := + R.fun@{ + n := 1; + }; From f7f9c2a63bcd89b8639a49c9252dc51fa38c6c0e Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 15 Nov 2024 14:30:27 +0100 Subject: [PATCH 10/11] minor --- .../Concrete/Translation/FromParsed/Analysis/Scoping.hs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 176f5ce29f..e5d06d5b21 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -391,9 +391,8 @@ reserveProjectionSymbol :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, State ScoperState] r) => ProjectionDef 'Parsed -> Sem r S.Symbol -reserveProjectionSymbol d = do - sym <- reserveSymbolSignatureOf SKNameFunction d (toBuiltinPrim <$> d ^. projectionFieldBuiltin) (d ^. projectionField) - return sym +reserveProjectionSymbol d = + reserveSymbolSignatureOf SKNameFunction d (toBuiltinPrim <$> d ^. projectionFieldBuiltin) (d ^. projectionField) reserveConstructorSymbol :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => From f185df163eef1a7656ab2c16f0fdcbbffffa1d5c Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 15 Nov 2024 16:44:17 +0100 Subject: [PATCH 11/11] move code to Concrete.Gen --- src/Juvix/Compiler/Concrete/Gen.hs | 95 +++++++++++++++++ .../FromParsed/Analysis/Scoping.hs | 100 +----------------- .../Concrete/Translation/FromSource.hs | 13 +-- 3 files changed, 99 insertions(+), 109 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Gen.hs b/src/Juvix/Compiler/Concrete/Gen.hs index e5b6a4f24b..2b310482ac 100644 --- a/src/Juvix/Compiler/Concrete/Gen.hs +++ b/src/Juvix/Compiler/Concrete/Gen.hs @@ -4,6 +4,7 @@ module Juvix.Compiler.Concrete.Gen ) where +import Data.List.NonEmpty qualified as NonEmpty import Juvix.Compiler.Concrete.Keywords import Juvix.Compiler.Concrete.Language.Base import Juvix.Prelude @@ -135,3 +136,97 @@ functionDefExpression :: NonEmpty (ExpressionAtom 'Parsed) -> Sem r (FunctionDefBody 'Parsed) functionDefExpression exp = SigBodyExpression <$> expressionAtoms' exp + +mkProjectionType :: InductiveDef 'Parsed -> ExpressionType 'Parsed -> ExpressionType 'Parsed +mkProjectionType i indTy = + foldr mkFun target indParams + where + indParams = map mkFunctionParameters $ i ^. inductiveParameters + target = mkFun (mkRecordParameter (i ^. inductiveTypeApplied)) indTy + + mkFun :: FunctionParameters 'Parsed -> ExpressionType 'Parsed -> ExpressionType 'Parsed + mkFun params tgt = + mkExpressionAtoms + . NonEmpty.singleton + . AtomFunction + $ Function + { _funParameters = params, + _funReturn = tgt, + _funKw = funkw + } + where + funkw = + KeywordRef + { _keywordRefKeyword = kwRightArrow, + _keywordRefInterval = getLoc (i ^. inductiveName), + _keywordRefUnicode = Ascii + } + + mkFunctionParameters :: InductiveParameters 'Parsed -> FunctionParameters 'Parsed + mkFunctionParameters InductiveParameters {..} = + FunctionParameters + { _paramNames = map FunctionParameterName $ toList _inductiveParametersNames, + _paramImplicit = Implicit, + _paramDelims = Irrelevant (Just (leftBrace, rightBrace)), + _paramColon = Irrelevant Nothing, + _paramType = maybe univ (^. inductiveParametersType) _inductiveParametersRhs + } + where + univ :: ExpressionAtoms 'Parsed + univ = + ExpressionAtoms + { _expressionAtoms = + NonEmpty.singleton $ + AtomUniverse $ + mkUniverse (Just smallLevel) (getLoc (i ^. inductiveName)), + _expressionAtomsLoc = Irrelevant $ getLoc (i ^. inductiveName) + } + + leftBrace :: KeywordRef + leftBrace = + KeywordRef + { _keywordRefKeyword = delimBraceL, + _keywordRefInterval = getLoc (i ^. inductiveName), + _keywordRefUnicode = Ascii + } + + rightBrace :: KeywordRef + rightBrace = + KeywordRef + { _keywordRefKeyword = delimBraceR, + _keywordRefInterval = getLoc (i ^. inductiveName), + _keywordRefUnicode = Ascii + } + + mkRecordParameter :: ExpressionType 'Parsed -> FunctionParameters 'Parsed + mkRecordParameter ty = + FunctionParameters + { _paramNames = [FunctionParameterName wildcard], + _paramImplicit = implicity, + _paramDelims = Irrelevant (Just (leftDoubleBrace, rightDoubleBrace)), + _paramColon = Irrelevant Nothing, + _paramType = ty + } + where + wildcard = WithLoc (getLoc (i ^. inductiveName)) "_self" + + implicity :: IsImplicit + implicity + | isJust (i ^. inductiveTrait) = ImplicitInstance + | otherwise = Explicit + + leftDoubleBrace :: KeywordRef + leftDoubleBrace = + KeywordRef + { _keywordRefKeyword = delimDoubleBraceL, + _keywordRefInterval = getLoc (i ^. inductiveName), + _keywordRefUnicode = Ascii + } + + rightDoubleBrace :: KeywordRef + rightDoubleBrace = + KeywordRef + { _keywordRefKeyword = delimDoubleBraceR, + _keywordRefInterval = getLoc (i ^. inductiveName), + _keywordRefUnicode = Ascii + } diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index e5d06d5b21..c44db9a0cc 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -27,7 +27,6 @@ import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context qualified as import Juvix.Compiler.Pipeline.EntryPoint import Juvix.Compiler.Store.Scoped.Language as Store import Juvix.Data.FixityInfo qualified as FI -import Juvix.Data.Keyword.All qualified as KW import Juvix.Prelude scopeCheck :: @@ -1710,7 +1709,7 @@ checkSections sec = topBindings helper ProjectionDef { _projectionConstructor = headConstr, _projectionField = field ^. fieldName, - _projectionType = mkProjectionType (field ^. fieldType), + _projectionType = G.mkProjectionType i (field ^. fieldType), _projectionFieldIx = idx, _projectionKind = kind, _projectionFieldBuiltin = field ^. fieldBuiltin, @@ -1736,103 +1735,6 @@ checkSections sec = topBindings helper p2' ) - mkProjectionType :: ExpressionType 'Parsed -> ExpressionType 'Parsed - mkProjectionType ty = - foldr mkFun target params - where - params = map mkFunctionParameters $ i ^. inductiveParameters - target = mkFun (mkRecordParameter (i ^. inductiveTypeApplied)) ty - - mkFun :: FunctionParameters 'Parsed -> ExpressionType 'Parsed -> ExpressionType 'Parsed - mkFun params tgt = - ExpressionAtoms - { _expressionAtoms = - NonEmpty.singleton $ - AtomFunction $ - Function - { _funParameters = params, - _funReturn = tgt, - _funKw = funkw - }, - _expressionAtomsLoc = Irrelevant $ getLoc (i ^. inductiveName) - } - where - funkw = - KeywordRef - { _keywordRefKeyword = KW.kwRightArrow, - _keywordRefInterval = getLoc (i ^. inductiveName), - _keywordRefUnicode = Ascii - } - - mkFunctionParameters :: InductiveParameters 'Parsed -> FunctionParameters 'Parsed - mkFunctionParameters InductiveParameters {..} = - FunctionParameters - { _paramNames = map FunctionParameterName $ toList _inductiveParametersNames, - _paramImplicit = Implicit, - _paramDelims = Irrelevant (Just (leftBrace, rightBrace)), - _paramColon = Irrelevant Nothing, - _paramType = maybe univ (^. inductiveParametersType) _inductiveParametersRhs - } - where - univ :: ExpressionAtoms 'Parsed - univ = - ExpressionAtoms - { _expressionAtoms = - NonEmpty.singleton $ - AtomUniverse $ - mkUniverse (Just smallLevel) (getLoc (i ^. inductiveName)), - _expressionAtomsLoc = Irrelevant $ getLoc (i ^. inductiveName) - } - - leftBrace :: KeywordRef - leftBrace = - KeywordRef - { _keywordRefKeyword = KW.delimBraceL, - _keywordRefInterval = getLoc (i ^. inductiveName), - _keywordRefUnicode = Ascii - } - - rightBrace :: KeywordRef - rightBrace = - KeywordRef - { _keywordRefKeyword = KW.delimBraceR, - _keywordRefInterval = getLoc (i ^. inductiveName), - _keywordRefUnicode = Ascii - } - - mkRecordParameter :: ExpressionType 'Parsed -> FunctionParameters 'Parsed - mkRecordParameter ty = - FunctionParameters - { _paramNames = [FunctionParameterName wildcard], - _paramImplicit = implicity, - _paramDelims = Irrelevant (Just (leftDoubleBrace, rightDoubleBrace)), - _paramColon = Irrelevant Nothing, - _paramType = ty - } - where - wildcard = WithLoc (getLoc (i ^. inductiveName)) "_self" - - implicity :: IsImplicit - implicity - | isJust (i ^. inductiveTrait) = ImplicitInstance - | otherwise = Explicit - - leftDoubleBrace :: KeywordRef - leftDoubleBrace = - KeywordRef - { _keywordRefKeyword = KW.delimDoubleBraceL, - _keywordRefInterval = getLoc (i ^. inductiveName), - _keywordRefUnicode = Ascii - } - - rightDoubleBrace :: KeywordRef - rightDoubleBrace = - KeywordRef - { _keywordRefKeyword = KW.delimDoubleBraceR, - _keywordRefInterval = getLoc (i ^. inductiveName), - _keywordRefUnicode = Ascii - } - getFields :: Sem (Fail ': s') [RecordStatement 'Parsed] getFields = case i ^. inductiveConstructors of c :| [] -> case c ^. constructorRhs of diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 707430f5df..452e57ae1e 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -20,6 +20,7 @@ import Juvix.Compiler.Backend.Markdown.Error import Juvix.Compiler.Concrete (HighlightBuilder, ignoreHighlightBuilder) import Juvix.Compiler.Concrete.Extra (takeWhile1P) import Juvix.Compiler.Concrete.Extra qualified as P +import Juvix.Compiler.Concrete.Gen (mkExpressionAtoms) import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context import Juvix.Compiler.Concrete.Translation.FromSource.Lexer hiding @@ -1541,16 +1542,8 @@ inductiveDef _inductiveBuiltin = do _inductiveAssignKw <- Irrelevant <$> kw kwAssign P. " ""