From 2e38aa609fb0f10b1ac2c6f87a07cf344669b6da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Wed, 20 Nov 2024 16:57:15 +0100 Subject: [PATCH] Unify type signature declaration syntax (#3178) * Closes #2990 * Allows type signatures for constructors, record fields and axioms to have the same form as in function definitions, e.g., ``` field {A} {{M A}} (arg1 arg2 : A) : List A ``` * For constructors, this introduces an ambiguity between record and GADT syntax with names. For example, ``` ctr { A : Type } ``` can be confused by the parser with initial part of GADT type signature: ``` ctr {A : Type} : A -> C A ``` For now, this is resolved by preferring the record syntax. Hence, it's currently not possible to use type signatures with implicit arguments for constructors. Ultimately, the `@` in record syntax should be made mandatory, which would resolve the ambiguity: ``` ctr@{ A : Type } ``` --------- Co-authored-by: Jan Mas Rovira --- include/package/PackageDescription/V2.juvix | 8 +- .../Concrete/Data/NameSignature/Builder.hs | 13 +- src/Juvix/Compiler/Concrete/Extra.hs | 2 +- src/Juvix/Compiler/Concrete/Gen.hs | 124 ++++++++++++++---- src/Juvix/Compiler/Concrete/Language/Base.hs | 52 +++++--- src/Juvix/Compiler/Concrete/Print/Base.hs | 38 +++--- .../FromParsed/Analysis/Scoping.hs | 76 ++++++----- .../Concrete/Translation/FromSource.hs | 92 ++++++++----- .../Internal/Translation/FromConcrete.hs | 19 ++- src/Juvix/Compiler/Pipeline/Package/Loader.hs | 10 +- src/Juvix/Parser/Error.hs | 2 +- test/Scope/Positive.hs | 6 +- tests/positive/Format.juvix | 16 ++- tests/positive/LetOpen.juvix | 21 +-- tests/positive/TypeSignatures.juvix | 16 +++ 15 files changed, 333 insertions(+), 162 deletions(-) create mode 100644 tests/positive/TypeSignatures.juvix diff --git a/include/package/PackageDescription/V2.juvix b/include/package/PackageDescription/V2.juvix index 666d721819..dc043f1bc8 100644 --- a/include/package/PackageDescription/V2.juvix +++ b/include/package/PackageDescription/V2.juvix @@ -4,7 +4,7 @@ import Juvix.Builtin.V1 open public; --- A ;Package; defines the configuration for a Juvix package type Package := - mkPackage { + mkPackage@{ -- The name of the package name : String; -- The version for the package @@ -19,7 +19,7 @@ type Package := --- A ;SemVer; defines a version that conforms to the Semantic Versioning specification. type SemVer := - mkSemVer { + mkSemVer@{ major : Nat; minor : Nat; patch : Nat; @@ -30,9 +30,9 @@ type SemVer := --- A ;Dependency; defines a Juvix package dependency. type Dependency := | --- A filesystem path to another Juvix Package. - path {path : String} + path@{path : String} | --- A ;git; repository containing a Juvix package at its root - git { + git@{ -- A name for this dependency name : String; -- The URL to the git repository diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 7ef1677d59..82b60b9737 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -54,14 +54,17 @@ addSymbol isImplicit mdefault sym ty = addArgument isImplicit mdefault (Just sym class HasNameSignature (s :: Stage) d | d -> s where addArgs :: (Members '[NameSignatureBuilder s] r) => d -> Sem r () +instance (SingI s) => HasNameSignature s (TypeSig s) where + addArgs a = do + mapM_ addSigArg (a ^. typeSigArgs) + whenJust (a ^. typeSigRetType) addExpressionType + instance (SingI s) => HasNameSignature s (AxiomDef s) where addArgs :: (Members '[NameSignatureBuilder s] r) => AxiomDef s -> Sem r () - addArgs a = addExpressionType (a ^. axiomType) + addArgs a = addArgs (a ^. axiomTypeSig) instance (SingI s) => HasNameSignature s (FunctionDef s) where - addArgs a = do - mapM_ addSigArg (a ^. signArgs) - whenJust (a ^. signRetType) addExpressionType + addArgs a = addArgs (a ^. signTypeSig) instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) where addArgs :: @@ -89,7 +92,7 @@ instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) wher addRhs :: ConstructorRhs s -> Sem r () addRhs = \case - ConstructorRhsGadt g -> addExpressionType (g ^. rhsGadtType) + ConstructorRhsGadt g -> addArgs (g ^. rhsGadtTypeSig) ConstructorRhsRecord g -> addRecord g ConstructorRhsAdt {} -> return () diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs index 9b24884e1d..6745e8d43b 100644 --- a/src/Juvix/Compiler/Concrete/Extra.hs +++ b/src/Juvix/Compiler/Concrete/Extra.hs @@ -110,4 +110,4 @@ isBodyExpression = \case isFunctionLike :: FunctionDef a -> Bool isFunctionLike = \case - FunctionDef {..} -> not (null _signArgs) || not (isBodyExpression _signBody) + FunctionDef {..} -> not (null (_signTypeSig ^. typeSigArgs)) || not (isBodyExpression _signBody) diff --git a/src/Juvix/Compiler/Concrete/Gen.hs b/src/Juvix/Compiler/Concrete/Gen.hs index 2b310482ac..bb55008436 100644 --- a/src/Juvix/Compiler/Concrete/Gen.hs +++ b/src/Juvix/Compiler/Concrete/Gen.hs @@ -29,9 +29,12 @@ simplestFunctionDef funName funBody = FunctionDef { _signName = funName, _signBody = SigBodyExpression funBody, - _signColonKw = Irrelevant Nothing, - _signArgs = [], - _signRetType = Nothing, + _signTypeSig = + TypeSig + { _typeSigColonKw = Irrelevant Nothing, + _typeSigArgs = [], + _typeSigRetType = Nothing + }, _signDoc = Nothing, _signPragmas = Nothing, _signBuiltin = Nothing, @@ -137,30 +140,45 @@ functionDefExpression :: Sem r (FunctionDefBody 'Parsed) functionDefExpression exp = SigBodyExpression <$> expressionAtoms' exp +mkFun :: forall s. (SingI s) => FunctionParameters s -> ExpressionType s -> ExpressionType s +mkFun params tgt = case sing :: SStage s of + SParsed -> mkFunParsed params tgt + SScoped -> mkFunScoped params tgt + +mkFunction :: forall s. (SingI s) => FunctionParameters s -> ExpressionType s -> Function s +mkFunction params tgt = + Function + { _funParameters = params, + _funReturn = tgt, + _funKw = funkw + } + where + funkw = + KeywordRef + { _keywordRefKeyword = kwRightArrow, + _keywordRefInterval = case sing :: SStage s of + SParsed -> getLoc tgt + SScoped -> getLoc tgt, + _keywordRefUnicode = Ascii + } + +mkFunParsed :: FunctionParameters 'Parsed -> ExpressionType 'Parsed -> ExpressionType 'Parsed +mkFunParsed params tgt = + mkExpressionAtoms + . NonEmpty.singleton + . AtomFunction + $ mkFunction params tgt + +mkFunScoped :: FunctionParameters 'Scoped -> ExpressionType 'Scoped -> ExpressionType 'Scoped +mkFunScoped params tgt = + ExpressionFunction $ mkFunction params tgt + 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 - } + target = mkFunParsed (mkRecordParameter (i ^. inductiveTypeApplied)) indTy mkFunctionParameters :: InductiveParameters 'Parsed -> FunctionParameters 'Parsed mkFunctionParameters InductiveParameters {..} = @@ -230,3 +248,65 @@ mkProjectionType i indTy = _keywordRefInterval = getLoc (i ^. inductiveName), _keywordRefUnicode = Ascii } + +mkWildcardKw :: Interval -> KeywordRef +mkWildcardKw loc = + KeywordRef + { _keywordRefKeyword = kwWildcard, + _keywordRefUnicode = Ascii, + _keywordRefInterval = loc + } + +mkWildcardParsed :: Interval -> ExpressionType 'Parsed +mkWildcardParsed loc = + mkExpressionAtoms + . NonEmpty.singleton + . AtomHole + $ mkWildcardKw loc + +mkTypeSigType :: forall s r. (SingI s, Member NameIdGen r) => TypeSig s -> Sem r (ExpressionType s) +mkTypeSigType ts = do + wildcard <- + case sing :: SStage s of + SParsed -> + return $ mkWildcardParsed defaultLoc + SScoped -> do + ExpressionHole + . mkHole defaultLoc + <$> freshNameId + return $ mkTypeSigType' wildcard ts + where + defaultLoc :: Interval + defaultLoc = singletonInterval (mkInitialLoc sourcePath) + + sourcePath :: Path Abs File + sourcePath = $(mkAbsFile "/") + +mkTypeSigType' :: forall s. (SingI s) => ExpressionType s -> TypeSig s -> (ExpressionType s) +mkTypeSigType' wildcard TypeSig {..} = + foldr mkFun rty (map mkFunctionParameters _typeSigArgs) + where + rty = fromMaybe wildcard _typeSigRetType + + univ :: Interval -> ExpressionType s + univ loc = run (runReader loc smallUniverseExpression) + + mkFunctionParameters :: SigArg s -> FunctionParameters s + mkFunctionParameters arg@SigArg {..} = + FunctionParameters + { _paramNames = getSigArgNames arg, + _paramImplicit = _sigArgImplicit, + _paramDelims = fmap Just _sigArgDelims, + _paramColon = Irrelevant $ maybe Nothing (Just . (^. unIrrelevant)) _sigArgColon, + _paramType = fromMaybe (univ (getLoc arg)) _sigArgType + } + + getSigArgNames :: SigArg s -> [FunctionParameter s] + getSigArgNames arg = case arg ^. sigArgNames of + SigArgNames ns -> map getArgName (toList ns) + SigArgNamesInstance -> [FunctionParameterWildcard (mkWildcardKw (getLoc arg))] + + getArgName :: Argument s -> FunctionParameter s + getArgName = \case + ArgumentSymbol n -> FunctionParameterName n + ArgumentWildcard (Wildcard loc) -> FunctionParameterWildcard (mkWildcardKw loc) diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs index 9a108f77cb..5bf5224963 100644 --- a/src/Juvix/Compiler/Concrete/Language/Base.hs +++ b/src/Juvix/Compiler/Concrete/Language/Base.hs @@ -592,6 +592,33 @@ deriving stock instance Ord (SigArg 'Parsed) deriving stock instance Ord (SigArg 'Scoped) +data TypeSig (s :: Stage) = TypeSig + { _typeSigArgs :: [SigArg s], + _typeSigColonKw :: Irrelevant (Maybe KeywordRef), + _typeSigRetType :: Maybe (ExpressionType s) + } + deriving stock (Generic) + +instance Serialize (TypeSig 'Scoped) + +instance NFData (TypeSig 'Scoped) + +instance Serialize (TypeSig 'Parsed) + +instance NFData (TypeSig 'Parsed) + +deriving stock instance Show (TypeSig 'Parsed) + +deriving stock instance Show (TypeSig 'Scoped) + +deriving stock instance Eq (TypeSig 'Parsed) + +deriving stock instance Eq (TypeSig 'Scoped) + +deriving stock instance Ord (TypeSig 'Parsed) + +deriving stock instance Ord (TypeSig 'Scoped) + data FunctionClause (s :: Stage) = FunctionClause { _clausenPipeKw :: Irrelevant KeywordRef, _clausenPatterns :: NonEmpty (PatternAtomType s), @@ -647,9 +674,7 @@ deriving stock instance Ord (FunctionDefBody 'Scoped) data FunctionDef (s :: Stage) = FunctionDef { _signName :: FunctionName s, - _signArgs :: [SigArg s], - _signColonKw :: Irrelevant (Maybe KeywordRef), - _signRetType :: Maybe (ExpressionType s), + _signTypeSig :: TypeSig s, _signDoc :: Maybe (Judoc s), _signPragmas :: Maybe ParsedPragmas, _signBuiltin :: Maybe (WithLoc BuiltinFunction), @@ -685,9 +710,8 @@ data AxiomDef (s :: Stage) = AxiomDef _axiomDoc :: Maybe (Judoc s), _axiomPragmas :: Maybe ParsedPragmas, _axiomName :: SymbolType s, - _axiomColonKw :: Irrelevant KeywordRef, - _axiomBuiltin :: Maybe (WithLoc BuiltinAxiom), - _axiomType :: ExpressionType s + _axiomTypeSig :: TypeSig s, + _axiomBuiltin :: Maybe (WithLoc BuiltinAxiom) } deriving stock (Generic) @@ -768,7 +792,7 @@ deriving stock instance Ord (RecordUpdateField 'Scoped) data RecordField (s :: Stage) = RecordField { _fieldName :: SymbolType s, _fieldIsImplicit :: IsImplicitField, - _fieldColon :: Irrelevant (KeywordRef), + _fieldTypeSig :: TypeSig s, _fieldType :: ExpressionType s, _fieldBuiltin :: Maybe (WithLoc BuiltinFunction), _fieldDoc :: Maybe (Judoc s), @@ -836,8 +860,7 @@ deriving stock instance Ord (RhsRecord 'Parsed) deriving stock instance Ord (RhsRecord 'Scoped) data RhsGadt (s :: Stage) = RhsGadt - { _rhsGadtColon :: Irrelevant KeywordRef, - _rhsGadtType :: ExpressionType s + { _rhsGadtTypeSig :: TypeSig s } deriving stock (Generic) @@ -2809,12 +2832,11 @@ data FunctionLhs (s :: Stage) = FunctionLhs _funLhsInstance :: Maybe KeywordRef, _funLhsCoercion :: Maybe KeywordRef, _funLhsName :: FunctionName s, - _funLhsArgs :: [SigArg s], - _funLhsColonKw :: Irrelevant (Maybe KeywordRef), - _funLhsRetType :: Maybe (ExpressionType s) + _funLhsTypeSig :: TypeSig s } makeLenses ''SideIfs +makeLenses ''TypeSig makeLenses ''FunctionLhs makeLenses ''Statements makeLenses ''NamedArgumentFunctionDef @@ -2910,9 +2932,7 @@ functionDefLhs FunctionDef {..} = _funLhsInstance = _signInstance, _funLhsCoercion = _signCoercion, _funLhsName = _signName, - _funLhsArgs = _signArgs, - _funLhsColonKw = _signColonKw, - _funLhsRetType = _signRetType + _funLhsTypeSig = _signTypeSig } fixityFieldHelper :: SimpleGetter (ParsedFixityFields s) (Maybe a) -> SimpleGetter (ParsedFixityInfo s) (Maybe a) @@ -3060,7 +3080,7 @@ instance HasLoc (InductiveDef s) where getLoc i = (getLoc <$> i ^. inductivePositive) ?<> getLoc (i ^. inductiveKw) instance (SingI s) => HasLoc (AxiomDef s) where - getLoc m = getLoc (m ^. axiomKw) <> getLocExpressionType (m ^. axiomType) + getLoc m = getLoc (m ^. axiomKw) <> getLocExpressionType (fromJust (m ^. axiomTypeSig . typeSigRetType)) getLocPublicAnn :: PublicAnn -> Maybe Interval getLocPublicAnn p = getLoc <$> p ^? _Public diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 09f2f338bf..fa30dbc2a8 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -1095,8 +1095,7 @@ instance (SingI s) => PrettyPrint (AxiomDef s) where ?<> builtin' ?<> ppCode _axiomKw <+> axiomName' - <+> ppCode _axiomColonKw - <+> ppExpressionType _axiomType + <> ppCode _axiomTypeSig instance PrettyPrint BuiltinInductive where ppCode i = ppCode Kw.kwBuiltin <+> keywordText (P.prettyText i) @@ -1143,27 +1142,34 @@ instance (SingI s) => PrettyPrint (SigArg s) where defaultVal = ppCode <$> _sigArgDefault ppCode l <> arg <+?> defaultVal <> ppCode r +instance (SingI s) => PrettyPrint (TypeSig s) where + ppCode TypeSig {..} = do + let margs' = fmap ppCode <$> nonEmpty _typeSigArgs + mtype' = case _typeSigColonKw ^. unIrrelevant of + Just col -> Just (ppCode col <+> ppExpressionType (fromJust _typeSigRetType)) + Nothing -> Nothing + margsAndType' = case mtype' of + Nothing -> margs' + Just ty' -> case margs' of + Nothing -> Just (pure ty') + Just args' -> Just (args' <> pure ty') + case margsAndType' of + Nothing -> return () + Just argsAndType' -> oneLineOrNext (sep argsAndType') + instance (SingI s) => PrettyPrint (FunctionLhs s) where ppCode FunctionLhs {..} = do let termin' = (<> line) . ppCode <$> _funLhsTerminating coercion' = (<> if isJust instance' then space else line) . ppCode <$> _funLhsCoercion instance' = (<> line) . ppCode <$> _funLhsInstance builtin' = (<> line) . ppCode <$> _funLhsBuiltin - margs' = fmap ppCode <$> nonEmpty _funLhsArgs - mtype' = case _funLhsColonKw ^. unIrrelevant of - Just col -> Just (ppCode col <+> ppExpressionType (fromJust _funLhsRetType)) - Nothing -> Nothing - argsAndType' = case mtype' of - Nothing -> margs' - Just ty' -> case margs' of - Nothing -> Just (pure ty') - Just args' -> Just (args' <> pure ty') name' = annDef _funLhsName (ppSymbolType _funLhsName) + sig' = ppCode _funLhsTypeSig builtin' ?<> termin' ?<> coercion' ?<> instance' - ?<> (name' <>? (oneLineOrNext . sep <$> argsAndType')) + ?<> (name' <> sig') instance (SingI s) => PrettyPrint (FunctionDef s) where ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => FunctionDef s -> Sem r () @@ -1412,8 +1418,7 @@ instance (PrettyPrint a) => PrettyPrint (Irrelevant a) where ppCode (Irrelevant a) = ppCode a instance (SingI s) => PrettyPrint (RhsGadt s) where - ppCode RhsGadt {..} = - ppCode _rhsGadtColon <+> ppExpressionType _rhsGadtType + ppCode RhsGadt {..} = ppCode _rhsGadtTypeSig instance (SingI s) => PrettyPrint (RecordField s) where ppCode RecordField {..} = do @@ -1428,8 +1433,7 @@ instance (SingI s) => PrettyPrint (RecordField s) where ?<> pragmas' ?<> builtin' ?<> mayBraces (ppSymbolType _fieldName) - <+> ppCode _fieldColon - <+> ppExpressionType _fieldType + <> ppCode _fieldTypeSig instance (SingI s) => PrettyPrint (RhsRecord s) where ppCode RhsRecord {..} = do @@ -1462,7 +1466,7 @@ ppConstructorDef singleConstructor ConstructorDef {..} = do constructorRhsHelper r = spaceMay <> ppCode r where spaceMay = case r of - ConstructorRhsGadt {} -> space + ConstructorRhsGadt {} -> mempty ConstructorRhsRecord {} -> mempty ConstructorRhsAdt a | null (a ^. rhsAdtArguments) -> mempty diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index c44db9a0cc..993a5ec04a 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1063,33 +1063,15 @@ resolveIteratorSyntaxDef s@IteratorSyntaxDef {..} = do (@$>) :: (Functor m) => (a -> m ()) -> a -> m a (@$>) f a = f a $> a -checkFunctionDef :: +checkTypeSig :: forall r. (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, State ScoperSyntax, Reader BindingStrategy] r) => - FunctionDef 'Parsed -> - Sem r (FunctionDef 'Scoped) -checkFunctionDef fdef@FunctionDef {..} = do - sigDoc' <- mapM checkJudoc _signDoc - (args', sigType', sigBody') <- withLocalScope $ do - a' <- mapM checkArg _signArgs - t' <- mapM checkParseExpressionAtoms _signRetType - b' <- checkBody - return (a', t', b') - sigName' <- - if - | P.isFunctionLike fdef -> bindFunctionSymbol _signName - | otherwise -> reserveFunctionSymbol fdef - let def = - FunctionDef - { _signName = sigName', - _signRetType = sigType', - _signDoc = sigDoc', - _signBody = sigBody', - _signArgs = args', - .. - } - registerNameSignature (sigName' ^. S.nameId) def - registerFunctionDef @$> def + TypeSig 'Parsed -> + Sem r (TypeSig 'Scoped) +checkTypeSig TypeSig {..} = do + a' <- mapM checkArg _typeSigArgs + t' <- mapM checkParseExpressionAtoms _typeSigRetType + return TypeSig {_typeSigArgs = a', _typeSigRetType = t', ..} where checkSigArgNames :: SigArgNames 'Parsed -> Sem r (SigArgNames 'Scoped) checkSigArgNames = \case @@ -1119,6 +1101,33 @@ checkFunctionDef fdef@FunctionDef {..} = do _sigArgDefault = default', .. } + +checkFunctionDef :: + forall r. + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, State ScoperSyntax, Reader BindingStrategy] r) => + FunctionDef 'Parsed -> + Sem r (FunctionDef 'Scoped) +checkFunctionDef fdef@FunctionDef {..} = do + sigDoc' <- mapM checkJudoc _signDoc + (sig', sigBody') <- withLocalScope $ do + a' <- checkTypeSig _signTypeSig + b' <- checkBody + return (a', b') + sigName' <- + if + | P.isFunctionLike fdef -> bindFunctionSymbol _signName + | otherwise -> reserveFunctionSymbol fdef + let def = + FunctionDef + { _signName = sigName', + _signDoc = sigDoc', + _signBody = sigBody', + _signTypeSig = sig', + .. + } + registerNameSignature (sigName' ^. S.nameId) def + registerFunctionDef @$> def + where checkBody :: Sem r (FunctionDefBody 'Scoped) checkBody = case _signBody of SigBodyExpression e -> SigBodyExpression <$> checkParseExpressionAtoms e @@ -1244,14 +1253,16 @@ checkInductiveDef InductiveDef {..} = do checkField :: RecordField 'Parsed -> Sem r (RecordField 'Scoped) checkField RecordField {..} = do doc' <- maybe (return Nothing) (checkJudoc >=> return . Just) _fieldDoc - type' <- checkParseExpressionAtoms _fieldType -- Since we don't allow dependent types in constructor types, each -- field is checked with a local scope withLocalScope $ do + type' <- checkParseExpressionAtoms _fieldType + typeSig' <- checkTypeSig _fieldTypeSig name' <- bindVariableSymbol _fieldName return RecordField - { _fieldType = type', + { _fieldTypeSig = typeSig', + _fieldType = type', _fieldName = name', _fieldDoc = doc', .. @@ -1267,11 +1278,10 @@ checkInductiveDef InductiveDef {..} = do checkGadt :: RhsGadt 'Parsed -> Sem r (RhsGadt 'Scoped) checkGadt RhsGadt {..} = do - constructorType' <- checkParseExpressionAtoms _rhsGadtType + constructorTypeSig' <- withLocalScope (checkTypeSig _rhsGadtTypeSig) return RhsGadt - { _rhsGadtType = constructorType', - _rhsGadtColon + { _rhsGadtTypeSig = constructorTypeSig' } checkProjectionDef :: @@ -1709,7 +1719,7 @@ checkSections sec = topBindings helper ProjectionDef { _projectionConstructor = headConstr, _projectionField = field ^. fieldName, - _projectionType = G.mkProjectionType i (field ^. fieldType), + _projectionType = G.mkProjectionType i (G.mkTypeSigType' (G.mkWildcardParsed (getLoc (i ^. inductiveName))) (field ^. fieldTypeSig)), _projectionFieldIx = idx, _projectionKind = kind, _projectionFieldBuiltin = field ^. fieldBuiltin, @@ -2112,10 +2122,10 @@ checkAxiomDef :: AxiomDef 'Parsed -> Sem r (AxiomDef 'Scoped) checkAxiomDef AxiomDef {..} = do - axiomType' <- withLocalScope (checkParseExpressionAtoms _axiomType) axiomName' <- bindAxiomSymbol _axiomName axiomDoc' <- withLocalScope (mapM checkJudoc _axiomDoc) - let a = AxiomDef {_axiomName = axiomName', _axiomType = axiomType', _axiomDoc = axiomDoc', ..} + axiomSig' <- withLocalScope (checkTypeSig _axiomTypeSig) + let a = AxiomDef {_axiomName = axiomName', _axiomTypeSig = axiomSig', _axiomDoc = axiomDoc', ..} registerNameSignature (a ^. axiomName . S.nameId) a registerAxiom @$> a diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 452e57ae1e..d65f1a352b 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -20,7 +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.Gen qualified as Gen import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context import Juvix.Compiler.Concrete.Translation.FromSource.Lexer hiding @@ -43,6 +43,11 @@ data FunctionSyntaxOptions = FunctionSyntaxOptions _funAllowInstance :: Bool } +data SigOptions = SigOptions + { _sigAllowOmitType :: Bool, + _sigAllowDefault :: Bool + } + data MdModuleBuilder = MdModuleBuilder { _mdModuleBuilder :: Module 'Parsed 'ModuleTop, _mdModuleBuilderBlocksLengths :: [Int] @@ -50,6 +55,14 @@ data MdModuleBuilder = MdModuleBuilder makeLenses ''MdModuleBuilder makeLenses ''FunctionSyntaxOptions +makeLenses ''SigOptions + +defaultSigOptions :: SigOptions +defaultSigOptions = + SigOptions + { _sigAllowDefault = False, + _sigAllowOmitType = False + } type JudocStash = State (Maybe (Judoc 'Parsed)) @@ -1291,6 +1304,20 @@ getPragmas = P.lift $ do put (Nothing @ParsedPragmas) return j +typeSig :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => SigOptions -> ParsecS r (TypeSig 'Parsed) +typeSig opts = P.label "" $ do + _typeSigArgs <- many (parseArg opts) + _typeSigColonKw <- + Irrelevant + <$> if + | opts ^. sigAllowOmitType -> optional (kw kwColon) + | otherwise -> Just <$> kw kwColon + _typeSigRetType <- + case _typeSigColonKw ^. unIrrelevant of + Just {} -> Just <$> parseExpressionAtoms + Nothing -> return Nothing + return TypeSig {..} + functionDefinitionLhs :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => @@ -1312,30 +1339,24 @@ functionDefinitionLhs opts _funLhsBuiltin = P.label "" $ do when (isJust _funLhsCoercion && isNothing _funLhsInstance) $ parseFailure off0 "expected: instance" _funLhsName <- symbol - _funLhsArgs <- many parseArg - _funLhsColonKw <- - Irrelevant - <$> if - | allowOmitType -> optional (kw kwColon) - | otherwise -> Just <$> kw kwColon - _funLhsRetType <- - case _funLhsColonKw ^. unIrrelevant of - Just {} -> Just <$> parseExpressionAtoms - Nothing -> return Nothing + let sigOpts = + SigOptions + { _sigAllowDefault = True, + _sigAllowOmitType = allowOmitType + } + _funLhsTypeSig <- typeSig sigOpts return FunctionLhs { _funLhsInstance, _funLhsBuiltin, _funLhsCoercion, _funLhsName, - _funLhsArgs, - _funLhsColonKw, - _funLhsRetType, + _funLhsTypeSig, _funLhsTerminating } -parseArg :: forall r. (Members '[ParserResultBuilder, JudocStash, PragmasStash, Error ParserError] r) => ParsecS r (SigArg 'Parsed) -parseArg = do +parseArg :: forall r. (Members '[ParserResultBuilder, JudocStash, PragmasStash, Error ParserError] r) => SigOptions -> ParsecS r (SigArg 'Parsed) +parseArg opts = do (openDelim, _sigArgNames, _sigArgImplicit, _sigArgColon) <- P.try $ do (opn, impl) <- implicitOpen let parseArgumentName :: ParsecS r (Argument 'Parsed) = @@ -1366,10 +1387,13 @@ parseArg = do return Nothing _ -> Just <$> parseExpressionAtoms - _sigArgDefault <- optional $ do - _argDefaultAssign <- Irrelevant <$> kw kwAssign - _argDefaultValue <- parseExpressionAtoms - return ArgDefault {..} + _sigArgDefault <- + if + | opts ^. sigAllowDefault -> optional $ do + _argDefaultAssign <- Irrelevant <$> kw kwAssign + _argDefaultValue <- parseExpressionAtoms + return ArgDefault {..} + | otherwise -> return Nothing closeDelim <- implicitClose _sigArgImplicit let _sigArgDelims = Irrelevant (openDelim, closeDelim) return SigArg {..} @@ -1387,16 +1411,14 @@ functionDefinition opts _signBuiltin = P.label "" $ do _signPragmas <- getPragmas _signBody <- parseBody unless - ( isJust (_funLhsColonKw ^. unIrrelevant) - || (P.isBodyExpression _signBody && null _funLhsArgs) + ( isJust (_funLhsTypeSig ^. typeSigColonKw . unIrrelevant) + || (P.isBodyExpression _signBody && null (_funLhsTypeSig ^. typeSigArgs)) ) $ parseFailure off "expected result type" return FunctionDef { _signName = _funLhsName, - _signArgs = _funLhsArgs, - _signColonKw = _funLhsColonKw, - _signRetType = _funLhsRetType, + _signTypeSig = _funLhsTypeSig, _signTerminating = _funLhsTerminating, _signInstance = _funLhsInstance, _signCoercion = _funLhsCoercion, @@ -1436,8 +1458,7 @@ axiomDef _axiomBuiltin = do _axiomDoc <- getJudoc _axiomPragmas <- getPragmas _axiomName <- symbol - _axiomColonKw <- Irrelevant <$> kw kwColon - _axiomType <- parseExpressionAtoms + _axiomTypeSig <- typeSig defaultSigOptions return AxiomDef {..} -------------------------------------------------------------------------------- @@ -1542,8 +1563,8 @@ inductiveDef _inductiveBuiltin = do _inductiveAssignKw <- Irrelevant <$> kw kwAssign P. " "" @@ -1575,12 +1596,11 @@ inductiveParams = inductiveParamsLong <|> inductiveParamsShort rhsGadt :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RhsGadt 'Parsed) rhsGadt = P.label "" $ do - _rhsGadtColon <- Irrelevant <$> kw kwColon - _rhsGadtType <- parseExpressionAtoms P. "" + _rhsGadtTypeSig <- typeSig defaultSigOptions return RhsGadt {..} recordField :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RecordField 'Parsed) -recordField = do +recordField = P.label "" $ do _fieldDoc <- optional stashJudoc >> getJudoc _fieldPragmas <- optional stashPragmas >> getPragmas _fieldBuiltin <- optional builtinRecordField @@ -1588,8 +1608,8 @@ recordField = do _fieldName <- symbol whenJust mayImpl (void . implicitCloseField) let _fieldIsImplicit = fromMaybe ExplicitField mayImpl - _fieldColon <- Irrelevant <$> kw kwColon - _fieldType <- parseExpressionAtoms + _fieldTypeSig <- typeSig defaultSigOptions + let _fieldType = Gen.mkTypeSigType' (Gen.mkWildcardParsed (getLoc _fieldName)) _fieldTypeSig return RecordField {..} rhsAdt :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RhsAdt 'Parsed) @@ -1619,8 +1639,8 @@ recordStatement = pconstructorRhs :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (ConstructorRhs 'Parsed) pconstructorRhs = - ConstructorRhsGadt <$> rhsGadt - <|> ConstructorRhsRecord <$> rhsRecord + ConstructorRhsRecord <$> rhsRecord + <|> ConstructorRhsGadt <$> rhsGadt <|> ConstructorRhsAdt <$> rhsAdt constructorDef :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Symbol -> Irrelevant (Maybe KeywordRef) -> ParsecS r (ConstructorDef 'Parsed) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 7ef0bcd05d..43e03192b1 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -412,7 +412,7 @@ goFunctionDef FunctionDef {..} = do where goBody :: Sem r Internal.Expression goBody = do - commonPatterns <- concatMapM (fmap toList . argToPattern) _signArgs + commonPatterns <- concatMapM (fmap toList . argToPattern) (_signTypeSig ^. typeSigArgs) let goClause :: FunctionClause 'Scoped -> Sem r Internal.LambdaClause goClause FunctionClause {..} = do _lambdaBody <- goExpression _clausenBody @@ -436,14 +436,14 @@ goFunctionDef FunctionDef {..} = do goDefType :: Sem r Internal.Expression goDefType = do - args <- concatMapM (fmap toList . argToParam) _signArgs - ret <- maybe freshHole goExpression _signRetType + args <- concatMapM (fmap toList . argToParam) (_signTypeSig ^. typeSigArgs) + ret <- maybe freshHole goExpression (_signTypeSig ^. typeSigRetType) return (Internal.foldFunType args ret) where freshHole :: Sem r Internal.Expression freshHole = do i <- freshNameId - let loc = maybe (getLoc _signName) getLoc (lastMay _signArgs) + let loc = maybe (getLoc _signName) getLoc (lastMay (_signTypeSig ^. typeSigArgs)) h = mkHole loc i return $ Internal.ExpressionHole h @@ -715,7 +715,7 @@ goConstructorDef retTy ConstructorDef {..} = do goRecordStatement = \case Concrete.RecordStatementSyntax {} -> return Nothing Concrete.RecordStatementField RecordField {..} -> do - ty' <- goExpression _fieldType + ty' <- goTypeSig _fieldTypeSig return $ Just Internal.FunctionParameter @@ -725,7 +725,7 @@ goConstructorDef retTy ConstructorDef {..} = do } goGadtType :: Concrete.RhsGadt 'Scoped -> Sem r Internal.Expression - goGadtType = goExpression . (^. Concrete.rhsGadtType) + goGadtType = goTypeSig . (^. Concrete.rhsGadtTypeSig) goRhs :: Concrete.ConstructorRhs 'Scoped -> Sem r Internal.Expression goRhs = \case @@ -1499,9 +1499,14 @@ goRecordPattern r = do output (Internal.patternArgFromVar Internal.Explicit v) go maxIdx (idx + 1) args +goTypeSig :: (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) => TypeSig 'Scoped -> Sem r Internal.Expression +goTypeSig s = do + ty <- Gen.mkTypeSigType s + goExpression ty + goAxiom :: (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) => AxiomDef 'Scoped -> Sem r Internal.AxiomDef goAxiom a = do - _axiomType' <- goExpression (a ^. axiomType) + _axiomType' <- goTypeSig (a ^. axiomTypeSig) _axiomPragmas' <- goPragmas (a ^. axiomPragmas) let axiom = Internal.AxiomDef diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader.hs b/src/Juvix/Compiler/Pipeline/Package/Loader.hs index 4e16ca3510..542e28f9c4 100644 --- a/src/Juvix/Compiler/Pipeline/Package/Loader.hs +++ b/src/Juvix/Compiler/Pipeline/Package/Loader.hs @@ -80,10 +80,15 @@ toConcrete t p = run . runReader l $ do funDef :: (Member (Reader Interval) r) => Sem r (Statement 'Parsed) funDef = do packageTypeIdentifier <- identifier (t ^. packageDescriptionTypeName) - _signRetType <- Just <$> expressionAtoms' (packageTypeIdentifier :| []) + _typeSigRetType <- Just <$> expressionAtoms' (packageTypeIdentifier :| []) _signName <- symbol Str.package - _signColonKw <- Irrelevant . Just <$> kw kwColon + _typeSigColonKw <- Irrelevant . Just <$> kw kwColon let _signBody = (t ^. packageDescriptionTypeTransform) p + _signTypeSig = + TypeSig + { _typeSigArgs = [], + .. + } return ( StatementFunctionDef FunctionDef @@ -93,7 +98,6 @@ toConcrete t p = run . runReader l $ do _signDoc = Nothing, _signCoercion = Nothing, _signBuiltin = Nothing, - _signArgs = [], .. } ) diff --git a/src/Juvix/Parser/Error.hs b/src/Juvix/Parser/Error.hs index a59d1ae607..af7277fd5e 100644 --- a/src/Juvix/Parser/Error.hs +++ b/src/Juvix/Parser/Error.hs @@ -214,7 +214,7 @@ instance ToGenericError NamedApplicationMissingAt where opts <- fromGenericOptions <$> ask @GenericOptions let lhs :: FunctionLhs 'Parsed = _namedApplicationMissingAtLhs funWord :: Text - | null (lhs ^. funLhsArgs) = "assignment" + | null (lhs ^. funLhsTypeSig . typeSigArgs) = "assignment" | otherwise = "function definition" fun' = ppCode opts _namedApplicationMissingAtFun msg :: Doc CodeAnn = diff --git a/test/Scope/Positive.hs b/test/Scope/Positive.hs index 37b2dd9c25..f4212c48c5 100644 --- a/test/Scope/Positive.hs +++ b/test/Scope/Positive.hs @@ -277,5 +277,9 @@ tests = posTest "Ignore dot files" $(mkRelDir "issue3068") - $(mkRelFile "main.juvix") + $(mkRelFile "main.juvix"), + posTest + "Type signatures" + $(mkRelDir ".") + $(mkRelFile "TypeSignatures.juvix") ] diff --git a/tests/positive/Format.juvix b/tests/positive/Format.juvix index c4933dcfc3..a0b4e67916 100644 --- a/tests/positive/Format.juvix +++ b/tests/positive/Format.juvix @@ -235,8 +235,9 @@ module Comments; -- attached to nothing - axiom a3 -- comment before axiom : - : Type; + axiom a3 + -- comment before axiom : + : Type; num -- comment before type sig : @@ -251,11 +252,12 @@ module Comments; -- attached to nothing 3 - axiom a4 : -- before open pi brace - {-- after open pi brace - a -- before pi : - : Type} - -> Type; + axiom a4 + : -- before open pi brace + {-- after open pi brace + a -- before pi : + : Type} + -> Type; id2 : {A : Type} -> A -> Nat -> A | -- before patternarg braces diff --git a/tests/positive/LetOpen.juvix b/tests/positive/LetOpen.juvix index ce6aa7acd6..879bd54bca 100644 --- a/tests/positive/LetOpen.juvix +++ b/tests/positive/LetOpen.juvix @@ -4,9 +4,10 @@ module M; axiom A : Type; end; -axiom B : let - open M; - in A; +axiom B + : let + open M; + in A; module Separator; @@ -14,10 +15,12 @@ end; axiom A : Type; -axiom C : let - open M hiding {A}; - in A; +axiom C + : let + open M hiding {A}; + in A; -axiom D : let - open M using {A as A'}; - in A'; +axiom D + : let + open M using {A as A'}; + in A'; diff --git a/tests/positive/TypeSignatures.juvix b/tests/positive/TypeSignatures.juvix new file mode 100644 index 0000000000..18fdcd4706 --- /dev/null +++ b/tests/positive/TypeSignatures.juvix @@ -0,0 +1,16 @@ +module TypeSignatures; + +import Stdlib.Data.Nat open; + +axiom f (x : Nat) : Nat; + +g (x : Nat) : Nat := + f@{ + x := x; + }; + +type R := mkR@{rf (x : Nat) : Nat}; + +type R' := mkR' (rf : Nat -> Nat) : R'; + +type RR := mkRR : (Nat -> Nat) -> RR;