diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 1960655531..ace4a4ec24 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -15,6 +15,7 @@ where import Juvix.Compiler.Concrete.Data.NameSignature.Error import Juvix.Compiler.Concrete.Gen qualified as Gen +import Juvix.Compiler.Concrete.Language.Base import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error import Juvix.Prelude @@ -64,9 +65,7 @@ instance (SingI s) => HasNameSignature s (AxiomDef s) where addArgs a = addArgs (a ^. axiomTypeSig) instance (SingI s) => HasNameSignature s (FunctionLhs s) where - addArgs a = do - mapM_ addSigArg (a ^. funLhsArgs) - whenJust (a ^. funLhsRetType) addExpressionType + addArgs FunctionLhs {..} = addArgs _funLhsTypeSig instance (SingI s) => HasNameSignature s (FunctionDef s) where addArgs = addArgs . functionDefLhs diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs index 2c049b1e7b..cf8dcdcbb4 100644 --- a/src/Juvix/Compiler/Concrete/Extra.hs +++ b/src/Juvix/Compiler/Concrete/Extra.hs @@ -111,7 +111,7 @@ isBodyExpression = \case SigBodyClauses {} -> False isLhsFunctionLike :: FunctionLhs 'Parsed -> Bool -isLhsFunctionLike FunctionLhs {..} = notNull _funLhsArgs +isLhsFunctionLike FunctionLhs {..} = notNull (_funLhsTypeSig ^. typeSigArgs) isFunctionLike :: FunctionDef 'Parsed -> Bool isFunctionLike d@FunctionDef {..} = diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs index ffcc6ab2de..6fbe2cc3b5 100644 --- a/src/Juvix/Compiler/Concrete/Language/Base.hs +++ b/src/Juvix/Compiler/Concrete/Language/Base.hs @@ -888,7 +888,7 @@ deriving stock instance Ord (RhsRecord 'Parsed) deriving stock instance Ord (RhsRecord 'Scoped) -data RhsGadt (s :: Stage) = RhsGadt +newtype RhsGadt (s :: Stage) = RhsGadt { _rhsGadtTypeSig :: TypeSig s } deriving stock (Generic) @@ -3387,7 +3387,7 @@ instance (SingI s) => HasLoc (FunctionLhs s) where (getLoc <$> _funLhsBuiltin) ?<> (getLoc <$> _funLhsTerminating) ?<> ( getLocSymbolType _funLhsName - <>? (getLocExpressionType <$> _funLhsRetType) + <>? (getLocExpressionType <$> _funLhsTypeSig ^. typeSigRetType) ) instance (SingI s) => HasLoc (FunctionDef s) where diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 97bbd5fe28..05f48b38d3 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1072,25 +1072,32 @@ checkDeriving :: Sem r (Deriving 'Scoped) checkDeriving Deriving {..} = do let lhs@FunctionLhs {..} = _derivingFunLhs + TypeSig {..} = _funLhsTypeSig (args', ret') <- withLocalScope $ do - args' <- mapM checkSigArg _funLhsArgs - ret' <- mapM checkParseExpressionAtoms _funLhsRetType + args' <- mapM checkSigArg _typeSigArgs + ret' <- mapM checkParseExpressionAtoms _typeSigRetType return (args', ret') name' <- if | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol _funLhsName | otherwise -> reserveFunctionSymbol lhs - let lhs' = + let typeSig' = + TypeSig + { _typeSigArgs = args', + _typeSigRetType = ret', + .. + } + lhs' = FunctionLhs - { _funLhsArgs = args', - _funLhsRetType = ret', - _funLhsName = name', + { _funLhsName = name', + _funLhsTypeSig = typeSig', .. } return Deriving { _derivingFunLhs = lhs', - .. + _derivingKw, + _derivingPragmas } checkSigArg :: @@ -1156,6 +1163,16 @@ checkSigArgNames = \case ArgumentSymbol s -> ArgumentSymbol <$> bindVariableSymbol s ArgumentWildcard w -> return (ArgumentWildcard w) +checkTypeSig :: + forall r. + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, State ScoperSyntax, Reader BindingStrategy] r) => + TypeSig 'Parsed -> + Sem r (TypeSig 'Scoped) +checkTypeSig TypeSig {..} = do + a' <- mapM checkSigArg _typeSigArgs + t' <- mapM checkParseExpressionAtoms _typeSigRetType + return TypeSig {_typeSigArgs = a', _typeSigRetType = t', ..} + checkFunctionDef :: forall r. (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, State ScoperSyntax, Reader BindingStrategy] r) => @@ -2194,11 +2211,16 @@ checkAxiomDef :: AxiomDef 'Parsed -> Sem r (AxiomDef 'Scoped) checkAxiomDef AxiomDef {..} = do - axiomType' <- withLocalScope (checkParseExpressionAtoms _axiomType) axiomName' <- getReservedDefinitionSymbol _axiomName axiomDoc' <- withLocalScope (mapM checkJudoc _axiomDoc) axiomSig' <- withLocalScope (checkTypeSig _axiomTypeSig) - let a = AxiomDef {_axiomName = axiomName', _axiomTypeSig = axiomSig', _axiomDoc = axiomDoc', ..} + let a = + AxiomDef + { _axiomName = axiomName', + _axiomTypeSig = axiomSig', + _axiomDoc = axiomDoc', + .. + } registerNameSignature (a ^. axiomName . S.nameId) a registerAxiom @$> a diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 95e46588ce..aeed610f40 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -728,26 +728,18 @@ argToPattern arg@SigArg {..} = do goDefType :: forall r. - ( Members - '[ Reader DefaultArgsStack, - NameIdGen, - Error ScoperError, - Reader Pragmas, - Reader S.InfoTable - ] - r - ) => + (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => FunctionLhs 'Scoped -> Sem r Internal.Expression goDefType FunctionLhs {..} = do - args <- concatMapM (fmap toList . argToParam) _funLhsArgs - ret <- maybe freshHole goExpression _funLhsRetType + args <- concatMapM (fmap toList . argToParam) (_funLhsTypeSig ^. typeSigArgs) + ret <- maybe freshHole goExpression (_funLhsTypeSig ^. typeSigRetType) return (Internal.foldFunType args ret) where freshHole :: Sem r Internal.Expression freshHole = do i <- freshNameId - let loc = maybe (getLoc _funLhsName) getLoc (lastMay _funLhsArgs) + let loc = maybe (getLoc _funLhsName) getLoc (lastMay (_funLhsTypeSig ^. typeSigArgs)) h = mkHole loc i return $ Internal.ExpressionHole h diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader.hs b/src/Juvix/Compiler/Pipeline/Package/Loader.hs index cc1a224bdd..38bff632ca 100644 --- a/src/Juvix/Compiler/Pipeline/Package/Loader.hs +++ b/src/Juvix/Compiler/Pipeline/Package/Loader.hs @@ -87,7 +87,8 @@ toConcrete t p = run . runReader l $ do _signTypeSig = TypeSig { _typeSigArgs = [], - .. + _typeSigRetType, + _typeSigColonKw } return ( StatementFunctionDef @@ -98,11 +99,9 @@ toConcrete t p = run . runReader l $ do _signDoc = Nothing, _signCoercion = Nothing, _signBuiltin = Nothing, - _signArgs = [], - _signRetType, _signName, - _signColonKw, - _signBody + _signBody, + _signTypeSig } )