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.

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

Make FunctionLhs a field of FunctionDef #3202

Merged
merged 9 commits into from
Dec 1, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
2 changes: 1 addition & 1 deletion app/Commands/Repl.hs
Original file line number Diff line number Diff line change
Expand Up @@ -293,7 +293,7 @@ printDocumentation = replParseIdentifiers >=> printIdentifiers
getDocFunction fun = do
tbl :: Scoped.InfoTable <- getScopedInfoTable
let def = tbl ^?! Scoped.infoFunctions . at fun . _Just
return (def ^. Concrete.signDoc)
return (def ^. Concrete.functionDefDoc)

getDocInductive :: Scoped.NameId -> Repl (Maybe (Concrete.Judoc 'Concrete.Scoped))
getDocInductive ind = do
Expand Down
6 changes: 3 additions & 3 deletions src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
Original file line number Diff line number Diff line change
Expand Up @@ -541,12 +541,12 @@ goAxiom axiom = do
goDeriving :: forall r. (Members '[Reader HtmlOptions] r) => Deriving 'Scoped -> Sem r Html
goDeriving def = do
sig <- ppHelper (ppCode def)
defHeader (def ^. derivingFunLhs . funLhsName . functionDefName) sig Nothing
defHeader (def ^. derivingFunLhs . funLhsName . functionDefNameScoped) sig Nothing

goFunctionDef :: forall r. (Members '[Reader HtmlOptions] r) => FunctionDef 'Scoped -> Sem r Html
goFunctionDef def = do
sig <- ppHelper (ppCode (functionDefLhs def))
defHeader (def ^. signName . functionDefName) sig (def ^. signDoc)
sig <- ppHelper (ppCode (def ^. functionDefLhs))
defHeader (def ^. functionDefName . functionDefNameScoped) sig (def ^. functionDefDoc)

goInductive :: forall r. (Members '[Reader HtmlOptions] r) => InductiveDef 'Scoped -> Sem r Html
goInductive def = do
Expand Down
4 changes: 2 additions & 2 deletions src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs
Original file line number Diff line number Diff line change
Expand Up @@ -61,8 +61,8 @@ runInfoTableBuilder ini = reinterpret (runState ini) $ \case
modify' (over infoInductives (HashMap.insert (ity ^. inductiveName . nameId) ity))
highlightDoc (ity ^. inductiveName . nameId) j
RegisterFunctionDef f -> do
let j = f ^. signDoc
fid = f ^. signName . functionDefName . nameId
let j = f ^. functionDefDoc
fid = f ^. functionDefName . functionDefNameScoped . nameId
modify' (over infoFunctions (HashMap.insert fid f))
highlightDoc fid j
RegisterName n -> highlightName (S.anameFromName n)
Expand Down
2 changes: 1 addition & 1 deletion src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ instance (SingI s) => HasNameSignature s (FunctionLhs s) where
addArgs FunctionLhs {..} = addArgs _funLhsTypeSig

instance (SingI s) => HasNameSignature s (FunctionDef s) where
addArgs = addArgs . functionDefLhs
addArgs = addArgs . (^. functionDefLhs)

instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) where
addArgs ::
Expand Down
4 changes: 2 additions & 2 deletions src/Juvix/Compiler/Concrete/Extra.hs
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ groupStatements = \case
definesSymbol n s = case s of
StatementInductive d -> n `elem` syms d
StatementAxiom d -> n == symbolParsed (d ^. axiomName)
StatementFunctionDef d -> withFunctionSymbol False (\n' -> n == symbolParsed n') (d ^. signName)
StatementFunctionDef d -> withFunctionSymbol False (\n' -> n == symbolParsed n') (d ^. functionDefName)
_ -> False
where
syms :: InductiveDef s -> [Symbol]
Expand Down Expand Up @@ -115,4 +115,4 @@ isLhsFunctionLike FunctionLhs {..} = notNull (_funLhsTypeSig ^. typeSigArgs)

isFunctionLike :: FunctionDef 'Parsed -> Bool
isFunctionLike d@FunctionDef {..} =
isLhsFunctionLike (functionDefLhs d) || (not . isBodyExpression) _signBody
isLhsFunctionLike (d ^. functionDefLhs) || (not . isBodyExpression) _functionDefBody
38 changes: 21 additions & 17 deletions src/Juvix/Compiler/Concrete/Gen.hs
Original file line number Diff line number Diff line change
Expand Up @@ -26,29 +26,33 @@ simplestFunctionDefParsed funNameTxt funBody = do

simplestFunctionDef :: forall s. (SingI s) => FunctionName s -> ExpressionType s -> FunctionDef s
simplestFunctionDef funName funBody =
FunctionDef
{ _signName = name,
_signBody = SigBodyExpression funBody,
_signTypeSig =
TypeSig
{ _typeSigColonKw = Irrelevant Nothing,
_typeSigArgs = [],
_typeSigRetType = Nothing
},
_signDoc = Nothing,
_signPragmas = Nothing,
_signBuiltin = Nothing,
_signTerminating = Nothing,
_signInstance = Nothing,
_signCoercion = Nothing
}
let lhs =
FunctionLhs
{ _funLhsName = name,
_funLhsTypeSig =
TypeSig
{ _typeSigColonKw = Irrelevant Nothing,
_typeSigArgs = [],
_typeSigRetType = Nothing
},
_funLhsBuiltin = Nothing,
_funLhsTerminating = Nothing,
_funLhsInstance = Nothing,
_funLhsCoercion = Nothing
}
in FunctionDef
{ _functionDefBody = SigBodyExpression funBody,
_functionDefLhs = lhs,
_functionDefDoc = Nothing,
_functionDefPragmas = Nothing
}
where
name :: FunctionSymbolType s
name = case sing :: SStage s of
SParsed -> FunctionDefName funName
SScoped ->
FunctionDefNameScoped
{ _functionDefName = funName,
{ _functionDefNameScoped = funName,
_functionDefNamePattern = Nothing
}

Expand Down
2 changes: 1 addition & 1 deletion src/Juvix/Compiler/Concrete/Language.hs
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ statementLabel = \case
StatementSyntax s -> goSyntax s
StatementOpenModule {} -> Nothing
StatementProjectionDef {} -> Nothing
StatementFunctionDef f -> withFunctionSymbol Nothing (Just . (^. symbolTypeLabel)) (f ^. signName)
StatementFunctionDef f -> withFunctionSymbol Nothing (Just . (^. symbolTypeLabel)) (f ^. functionDefName)
StatementDeriving f -> withFunctionSymbol Nothing (Just . (^. symbolTypeLabel)) (f ^. derivingFunLhs . funLhsName)
StatementImport i -> Just (i ^. importModulePath . to modulePathTypeLabel)
StatementInductive i -> Just (i ^. inductiveName . symbolTypeLabel)
Expand Down
67 changes: 35 additions & 32 deletions src/Juvix/Compiler/Concrete/Language/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -716,7 +716,7 @@ instance Serialize FunctionDefNameParsed
instance NFData FunctionDefNameParsed

data FunctionDefNameScoped = FunctionDefNameScoped
{ _functionDefName :: S.Symbol,
{ _functionDefNameScoped :: S.Symbol,
_functionDefNamePattern :: Maybe PatternArg
}
deriving stock (Eq, Ord, Show, Generic)
Expand All @@ -726,15 +726,10 @@ instance Serialize FunctionDefNameScoped
instance NFData FunctionDefNameScoped

data FunctionDef (s :: Stage) = FunctionDef
{ _signName :: FunctionSymbolType s,
_signTypeSig :: TypeSig s,
_signDoc :: Maybe (Judoc s),
_signPragmas :: Maybe ParsedPragmas,
_signBuiltin :: Maybe (WithLoc BuiltinFunction),
_signBody :: FunctionDefBody s,
_signTerminating :: Maybe KeywordRef,
_signInstance :: Maybe KeywordRef,
_signCoercion :: Maybe KeywordRef
{ _functionDefDoc :: Maybe (Judoc s),
_functionDefPragmas :: Maybe ParsedPragmas,
_functionDefLhs :: FunctionLhs s,
_functionDefBody :: FunctionDefBody s
}
deriving stock (Generic)

Expand Down Expand Up @@ -3057,16 +3052,23 @@ makePrisms ''NamedArgumentNew
makePrisms ''ConstructorRhs
makePrisms ''FunctionDefNameParsed

functionDefLhs :: FunctionDef s -> FunctionLhs s
functionDefLhs FunctionDef {..} =
FunctionLhs
{ _funLhsBuiltin = _signBuiltin,
_funLhsTerminating = _signTerminating,
_funLhsInstance = _signInstance,
_funLhsCoercion = _signCoercion,
_funLhsName = _signName,
_funLhsTypeSig = _signTypeSig
}
functionDefBuiltin :: Lens' (FunctionDef s) (Maybe (WithLoc BuiltinFunction))
functionDefBuiltin = functionDefLhs . funLhsBuiltin

functionDefTerminating :: Lens' (FunctionDef s) (Maybe KeywordRef)
functionDefTerminating = functionDefLhs . funLhsTerminating

functionDefInstance :: Lens' (FunctionDef s) (Maybe KeywordRef)
functionDefInstance = functionDefLhs . funLhsInstance

functionDefCoercion :: Lens' (FunctionDef s) (Maybe KeywordRef)
functionDefCoercion = functionDefLhs . funLhsCoercion

functionDefName :: Lens' (FunctionDef s) (FunctionSymbolType s)
functionDefName = functionDefLhs . funLhsName

functionDefTypeSig :: Lens' (FunctionDef s) (TypeSig s)
functionDefTypeSig = functionDefLhs . funLhsTypeSig

fixityFieldHelper :: SimpleGetter (ParsedFixityFields s) (Maybe a) -> SimpleGetter (ParsedFixityInfo s) (Maybe a)
fixityFieldHelper l = to (^? fixityFields . _Just . l . _Just)
Expand Down Expand Up @@ -3263,7 +3265,7 @@ getLocFunctionSymbolType = case sing :: SStage s of

instance HasLoc FunctionDefNameScoped where
getLoc FunctionDefNameScoped {..} =
getLoc _functionDefName
getLoc _functionDefNameScoped
<>? (getLoc <$> _functionDefNamePattern)

instance HasLoc FunctionDefNameParsed where
Expand Down Expand Up @@ -3525,12 +3527,13 @@ instance (SingI s) => HasLoc (FunctionDefBody s) where

instance (SingI s) => HasLoc (FunctionDef s) where
getLoc FunctionDef {..} =
(getLoc <$> _signDoc)
?<> (getLoc <$> _signPragmas)
?<> (getLoc <$> _signBuiltin)
?<> (getLoc <$> _signTerminating)
?<> (getLocFunctionSymbolType _signName)
<> getLoc _signBody
let FunctionLhs {..} = _functionDefLhs
in (getLoc <$> _functionDefDoc)
?<> (getLoc <$> _functionDefPragmas)
?<> (getLoc <$> _funLhsBuiltin)
?<> (getLoc <$> _funLhsTerminating)
?<> (getLocFunctionSymbolType _funLhsName)
<> getLoc _functionDefBody

instance HasLoc (Example s) where
getLoc e = e ^. exampleLoc
Expand Down Expand Up @@ -3719,7 +3722,7 @@ getFunctionSymbol sym = case sing :: SStage s of
SParsed -> case sym of
FunctionDefName p -> p
FunctionDefNamePattern {} -> impossibleError "invalid call"
SScoped -> sym ^. functionDefName
SScoped -> sym ^. functionDefNameScoped

functionSymbolPattern :: forall s. (SingI s) => FunctionSymbolType s -> Maybe (PatternAtomType s)
functionSymbolPattern f = case sing :: SStage s of
Expand All @@ -3729,19 +3732,19 @@ functionSymbolPattern f = case sing :: SStage s of
withFunctionSymbol :: forall s a. (SingI s) => a -> (SymbolType s -> a) -> FunctionSymbolType s -> a
withFunctionSymbol a f sym = case sing :: SStage s of
SParsed -> maybe a f (sym ^? _FunctionDefName)
SScoped -> f (sym ^. functionDefName)
SScoped -> f (sym ^. functionDefNameScoped)

namedArgumentNewSymbolParsed :: (SingI s) => SimpleGetter (NamedArgumentNew s) Symbol
namedArgumentNewSymbolParsed = to $ \case
NamedArgumentItemPun a -> a ^. namedArgumentPunSymbol
NamedArgumentNewFunction a -> symbolParsed (getFunctionSymbol (a ^. namedArgumentFunctionDef . signName))
NamedArgumentNewFunction a -> symbolParsed (getFunctionSymbol (a ^. namedArgumentFunctionDef . functionDefName))

namedArgumentNewSymbol :: Lens' (NamedArgumentNew 'Parsed) Symbol
namedArgumentNewSymbol f = \case
NamedArgumentItemPun a -> NamedArgumentItemPun <$> (namedArgumentPunSymbol f a)
NamedArgumentNewFunction a -> do
a' <- f (a ^?! namedArgumentFunctionDef . signName . _FunctionDefName)
return $ NamedArgumentNewFunction (over namedArgumentFunctionDef (set signName (FunctionDefName a')) a)
a' <- f (a ^?! namedArgumentFunctionDef . functionDefName . _FunctionDefName)
return $ NamedArgumentNewFunction (over namedArgumentFunctionDef (set functionDefName (FunctionDefName a')) a)

scopedIdenSrcName :: Lens' ScopedIden S.Name
scopedIdenSrcName f n = case n ^. scopedIdenAlias of
Expand Down
8 changes: 4 additions & 4 deletions src/Juvix/Compiler/Concrete/Print/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1205,10 +1205,10 @@ ppPipeBranches allowSameLine isTop ppBranch = \case
instance (SingI s) => PrettyPrint (FunctionDef s) where
ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => FunctionDef s -> Sem r ()
ppCode fun@FunctionDef {..} = do
let doc' :: Maybe (Sem r ()) = ppCode <$> _signDoc
pragmas' :: Maybe (Sem r ()) = ppCode <$> _signPragmas
sig' = ppCode (functionDefLhs fun)
body' = case _signBody of
let doc' :: Maybe (Sem r ()) = ppCode <$> _functionDefDoc
pragmas' :: Maybe (Sem r ()) = ppCode <$> _functionDefPragmas
sig' = ppCode (fun ^. functionDefLhs)
body' = case _functionDefBody of
SigBodyExpression e -> space <> ppCode Kw.kwAssign <> oneLineOrNext (ppTopExpressionType e)
SigBodyClauses k -> ppPipeBranches False Top ppFunctionClause k
doc'
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -439,7 +439,7 @@ reserveFunctionLikeSymbol ::
Sem r ()
reserveFunctionLikeSymbol f =
when (P.isFunctionLike f) $
void (reserveFunctionSymbol (functionDefLhs f))
void (reserveFunctionSymbol (f ^. functionDefLhs))

bindFixitySymbol ::
(Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) =>
Expand Down Expand Up @@ -1129,7 +1129,7 @@ checkDeriving Deriving {..} = do
| otherwise -> reserveFunctionSymbol lhs
let defname' =
FunctionDefNameScoped
{ _functionDefName = name',
{ _functionDefNameScoped = name',
_functionDefNamePattern = Nothing
}
let lhs' =
Expand Down Expand Up @@ -1192,44 +1192,50 @@ checkFunctionDef ::
FunctionDef 'Parsed ->
Sem r (FunctionDef 'Scoped)
checkFunctionDef fdef@FunctionDef {..} = do
sigDoc' <- mapM checkJudoc _signDoc
let FunctionLhs {..} = _functionDefLhs
sigDoc' <- mapM checkJudoc _functionDefDoc
(sig', sigBody') <- withLocalScope $ do
a' <- checkTypeSig _signTypeSig
a' <- checkTypeSig _funLhsTypeSig
b' <- checkBody
return (a', b')
whenJust (functionSymbolPattern _signName) reservePatternFunctionSymbols
sigName' <- case _signName of
whenJust (functionSymbolPattern _funLhsName) reservePatternFunctionSymbols
sigName' <- case _funLhsName of
FunctionDefName name -> do
name' <-
if
| P.isFunctionLike fdef -> getReservedDefinitionSymbol name
| otherwise -> reserveFunctionSymbol (functionDefLhs fdef)
| otherwise -> reserveFunctionSymbol (fdef ^. functionDefLhs)
return
FunctionDefNameScoped
{ _functionDefName = name',
{ _functionDefNameScoped = name',
_functionDefNamePattern = Nothing
}
FunctionDefNamePattern p -> do
name' <- freshSymbol KNameFunction KNameFunction (WithLoc (getLoc p) "__pattern__")
p' <- runReader PatternNamesKindFunctions (checkParsePatternAtom p)
return
FunctionDefNameScoped
{ _functionDefName = name',
{ _functionDefNameScoped = name',
_functionDefNamePattern = Just p'
}
let def =
let lhs' =
FunctionLhs
{ _funLhsName = sigName',
_funLhsTypeSig = sig',
..
}
def =
FunctionDef
{ _signName = sigName',
_signDoc = sigDoc',
_signBody = sigBody',
_signTypeSig = sig',
{ _functionDefLhs = lhs',
_functionDefDoc = sigDoc',
_functionDefBody = sigBody',
..
}
registerNameSignature (sigName' ^. functionDefName . S.nameId) def
registerNameSignature (sigName' ^. functionDefNameScoped . S.nameId) def
registerFunctionDef @$> def
where
checkBody :: Sem r (FunctionDefBody 'Scoped)
checkBody = case _signBody of
checkBody = case _functionDefBody of
SigBodyExpression e -> SigBodyExpression <$> checkParseExpressionAtoms e
SigBodyClauses cls -> SigBodyClauses <$> mapM checkClause cls

Expand Down
29 changes: 12 additions & 17 deletions src/Juvix/Compiler/Concrete/Translation/FromSource.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1431,31 +1431,26 @@ functionDefinition ::
FunctionSyntaxOptions ->
Maybe (WithLoc BuiltinFunction) ->
ParsecS r (FunctionDef 'Parsed)
functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
functionDefinition opts _functionDefBuiltin = P.label "<function definition>" $ do
off0 <- P.getOffset
FunctionLhs {..} <- functionDefinitionLhs opts _signBuiltin
lhs <- functionDefinitionLhs opts _functionDefBuiltin
off <- P.getOffset
_signDoc <- getJudoc
_signPragmas <- getPragmas
_signBody <- parseBody
_functionDefDoc <- getJudoc
_functionDefPragmas <- getPragmas
_functionDefBody <- parseBody
unless
( isJust (_funLhsTypeSig ^. typeSigColonKw . unIrrelevant)
|| (P.isBodyExpression _signBody && null (_funLhsTypeSig ^. typeSigArgs))
( isJust (lhs ^. funLhsTypeSig . typeSigColonKw . unIrrelevant)
|| (P.isBodyExpression _functionDefBody && null (lhs ^. funLhsTypeSig . typeSigArgs))
)
$ parseFailure off "expected result type"
let fdef =
FunctionDef
{ _signName = _funLhsName,
_signTypeSig = _funLhsTypeSig,
_signTerminating = _funLhsTerminating,
_signInstance = _funLhsInstance,
_signCoercion = _funLhsCoercion,
_signBuiltin = _funLhsBuiltin,
_signDoc,
_signPragmas,
_signBody
{ _functionDefLhs = lhs,
_functionDefDoc,
_functionDefPragmas,
_functionDefBody
}
when (isNothing (_funLhsName ^? _FunctionDefName) && P.isFunctionLike fdef) $
when (isNothing (lhs ^? funLhsName . _FunctionDefName) && P.isFunctionLike fdef) $
parseFailure off0 "expected function name"
return fdef
where
Expand Down
Loading
Loading