Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Named arguments for record projections #3173

Merged
merged 11 commits into from
Nov 15, 2024
Merged

Named arguments for record projections #3173

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
c7a8aac
comment wip
lukaszcz Nov 13, 2024
c0383e7
wip
lukaszcz Nov 14, 2024
d7e01ed
wip
lukaszcz Nov 14, 2024
cce4561
register field signature
lukaszcz Nov 14, 2024
f7987f8
name signatures for record projections
lukaszcz Nov 15, 2024
b51b40f
add test
lukaszcz Nov 15, 2024
bddaed0
use projection type in Internal
lukaszcz Nov 15, 2024
1099762
fix infixities
lukaszcz Nov 15, 2024
02cb288
fix formatting
lukaszcz Nov 15, 2024
f7f9c2a
minor
lukaszcz Nov 15, 2024
f185df1
move code to Concrete.Gen
lukaszcz Nov 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,15 @@ instance (SingI s) => HasNameSignature s (InductiveDef s) where
mapM_ addInductiveParams (a ^. inductiveParameters)
whenJust (a ^. inductiveType) addExpressionType

instance (SingI s) => HasNameSignature s (ProjectionDef s) where
addArgs ::
forall r.
(Members '[NameSignatureBuilder s] r) =>
ProjectionDef s ->
Sem r ()
addArgs p = do
addExpressionType (p ^. projectionType)

mkNameSignature ::
forall s d r.
(SingI s, Members '[Error ScoperError] r, HasNameSignature s d) =>
Expand Down
2 changes: 2 additions & 0 deletions src/Juvix/Compiler/Concrete/Language/Base.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down Expand Up @@ -931,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
Expand Down
162 changes: 135 additions & 27 deletions src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ::
Expand Down Expand Up @@ -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) =>
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -403,11 +392,7 @@ reserveProjectionSymbol ::
ProjectionDef 'Parsed ->
Sem r S.Symbol
reserveProjectionSymbol d =
reserveSymbolOf
SKNameFunction
Nothing
(toBuiltinPrim <$> d ^. projectionFieldBuiltin)
(d ^. projectionField)
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) =>
Expand Down Expand Up @@ -1180,24 +1165,26 @@ 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'
<$> sequence
[ 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',
_inductiveDoc = inductiveDoc',
_inductivePragmas = _inductivePragmas,
_inductiveParameters = inductiveParameters',
_inductiveType = inductiveType',
_inductiveTypeApplied = inductiveTypeApplied',
_inductiveConstructors = inductiveConstructors',
_inductiveBuiltin,
_inductivePositive,
Expand Down Expand Up @@ -1288,6 +1275,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

Expand Down Expand Up @@ -1491,7 +1501,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
Expand Down Expand Up @@ -1700,6 +1710,7 @@ checkSections sec = topBindings helper
ProjectionDef
{ _projectionConstructor = headConstr,
_projectionField = field ^. fieldName,
_projectionType = mkProjectionType (field ^. fieldType),
_projectionFieldIx = idx,
_projectionKind = kind,
_projectionFieldBuiltin = field ^. fieldBuiltin,
Expand All @@ -1725,6 +1736,103 @@ checkSections sec = topBindings helper
p2'
)

mkProjectionType :: ExpressionType 'Parsed -> ExpressionType 'Parsed
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

most of this code could go to Juvix.Compiler.Concrete.Gen

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

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
Expand Down
12 changes: 12 additions & 0 deletions src/Juvix/Compiler/Concrete/Translation/FromSource.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1539,6 +1539,18 @@ inductiveDef _inductiveBuiltin = do
optional (kw kwColon >> parseExpressionAtoms)
P.<?> "<type annotation e.g. ': Type'>"
_inductiveAssignKw <- Irrelevant <$> kw kwAssign P.<?> "<assignment symbol ':='>"
let name' = NameUnqualified _inductiveName
params = fmap (AtomIdentifier . NameUnqualified) (concatMap (toList . (^. inductiveParametersNames)) _inductiveParameters)
iden =
ExpressionAtoms
{ _expressionAtoms = AtomIdentifier name' :| [],
_expressionAtomsLoc = Irrelevant (getLoc _inductiveName)
}
_inductiveTypeApplied =
ExpressionAtoms
{ _expressionAtoms = AtomParens iden :| params,
_expressionAtomsLoc = Irrelevant (getLoc _inductiveName)
}
_inductiveConstructors <-
pipeSep1 (constructorDef _inductiveName)
P.<?> "<constructor definition>"
Expand Down
15 changes: 6 additions & 9 deletions src/Juvix/Compiler/Internal/Extra.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,36 +113,33 @@ genFieldProjection ::
(Members '[NameIdGen] r) =>
ProjectionKind ->
FunctionName ->
Expression ->
Maybe BuiltinFunction ->
[ArgInfo] ->
Maybe Pragmas ->
ConstructorInfo ->
Int ->
Sem r FunctionDef
genFieldProjection kind _funDefName _funDefBuiltin 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,
_funDefIsInstanceCoercion =
if
| kind == ProjectionCoercion -> Just IsInstanceCoercionCoercion
| otherwise -> Nothing,
_funDefArgsInfo = mempty,
_funDefPragmas =
maybe
(mempty {_pragmasInline = Just InlineAlways})
(over pragmasInline (maybe (Just InlineAlways) Just))
mpragmas,
_funDefBody = body',
_funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy,
_funDefDocComment = Nothing,
_funDefType,
_funDefName,
_funDefBuiltin
_funDefBuiltin,
_funDefArgsInfo
}
where
constructorImplicity :: IsImplicit
Expand Down
Loading
Loading