From 2bbd850e9c4084a099137d9e717f8fcb5d0f537d Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 22 Aug 2023 09:52:33 +0200 Subject: [PATCH 01/18] wip --- src/Juvix/Compiler/Concrete/Extra.hs | 1 + src/Juvix/Compiler/Concrete/Keywords.hs | 2 + src/Juvix/Compiler/Concrete/Language.hs | 122 +++++++++++------- src/Juvix/Compiler/Concrete/Print/Base.hs | 6 + .../FromParsed/Analysis/Scoping.hs | 13 ++ src/Juvix/Data/Keyword/All.hs | 3 + src/Juvix/Extra/Strings.hs | 3 + 7 files changed, 105 insertions(+), 45 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs index 229718b7cb..142ab7643e 100644 --- a/src/Juvix/Compiler/Concrete/Extra.hs +++ b/src/Juvix/Compiler/Concrete/Extra.hs @@ -87,6 +87,7 @@ groupStatements = \case (StatementSyntax (SyntaxFixity _), _) -> False (StatementSyntax (SyntaxOperator o), s) -> definesSymbol (o ^. opSymbol) s (StatementSyntax (SyntaxIterator i), s) -> definesSymbol (i ^. iterSymbol) s + (StatementSyntax (SyntaxAlias {}), _) -> False (StatementImport _, StatementImport _) -> True (StatementImport i, StatementOpenModule o) -> case sing :: SStage s of SParsed -> True diff --git a/src/Juvix/Compiler/Concrete/Keywords.hs b/src/Juvix/Compiler/Concrete/Keywords.hs index e0105a6602..5a15532c11 100644 --- a/src/Juvix/Compiler/Concrete/Keywords.hs +++ b/src/Juvix/Compiler/Concrete/Keywords.hs @@ -39,6 +39,7 @@ import Juvix.Data.Keyword.All kwLambda, kwLet, kwMapsTo, + kwAlias, kwModule, kwOpen, kwOperator, @@ -94,5 +95,6 @@ nonKeywords = kwEq, kwFixity, kwOperator, + kwAlias, kwIterator ] diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 8ce805532f..ab7322abc9 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -250,10 +250,31 @@ deriving stock instance Ord (Import 'Parsed) deriving stock instance Ord (Import 'Scoped) +data AliasDef (s :: Stage) = AliasDef + { + _aliasSyntaxKw :: Irrelevant KeywordRef, + _aliasAliasKw :: Irrelevant KeywordRef, + _aliasName :: SymbolType s, + _aliasAsName :: IdentifierType s + } + +deriving stock instance (Show (AliasDef 'Parsed)) + +deriving stock instance (Show (AliasDef 'Scoped)) + +deriving stock instance (Eq (AliasDef 'Parsed)) + +deriving stock instance (Eq (AliasDef 'Scoped)) + +deriving stock instance (Ord (AliasDef 'Parsed)) + +deriving stock instance (Ord (AliasDef 'Scoped)) + data SyntaxDef (s :: Stage) = SyntaxFixity (FixitySyntaxDef s) | SyntaxOperator OperatorSyntaxDef | SyntaxIterator IteratorSyntaxDef + | SyntaxAlias (AliasDef s) deriving stock instance (Show (SyntaxDef 'Parsed)) @@ -267,12 +288,6 @@ deriving stock instance (Ord (SyntaxDef 'Parsed)) deriving stock instance (Ord (SyntaxDef 'Scoped)) -instance HasLoc (SyntaxDef s) where - getLoc = \case - SyntaxFixity t -> getLoc t - SyntaxOperator t -> getLoc t - SyntaxIterator t -> getLoc t - data FixitySyntaxDef (s :: Stage) = FixitySyntaxDef { _fixitySymbol :: SymbolType s, _fixityDoc :: Maybe (Judoc s), @@ -963,16 +978,16 @@ newtype ModuleRef' (c :: S.IsConcrete) = ModuleRef' { _unModuleRef' :: Σ ModuleIsTop (TyCon1 (ModuleRef'' c)) } -instance SingI c => Show (ModuleRef' c) where +instance (SingI c) => Show (ModuleRef' c) where show = show . getModuleRefNameId -instance SingI c => Eq (ModuleRef' c) where +instance (SingI c) => Eq (ModuleRef' c) where (==) = (==) `on` getModuleRefNameId -instance SingI c => Ord (ModuleRef' c) where +instance (SingI c) => Ord (ModuleRef' c) where compare = compare `on` getModuleRefNameId -getNameRefId :: forall c. SingI c => RefNameType c -> S.NameId +getNameRefId :: forall c. (SingI c) => RefNameType c -> S.NameId getNameRefId = case sing :: S.SIsConcrete c of S.SConcrete -> (^. S.nameId) S.SNotConcrete -> (^. S.nameId) @@ -983,7 +998,7 @@ getModuleRefExportInfo (ModuleRef' (_ :&: ModuleRef'' {..})) = _moduleExportInfo getModuleRefNameType :: ModuleRef' c -> RefNameType c getModuleRefNameType (ModuleRef' (_ :&: ModuleRef'' {..})) = _moduleRefName -getModuleRefNameId :: forall c. SingI c => ModuleRef' c -> S.NameId +getModuleRefNameId :: forall c. (SingI c) => ModuleRef' c -> S.NameId getModuleRefNameId (ModuleRef' (t :&: ModuleRef'' {..})) = case sing :: S.SIsConcrete c of S.SConcrete -> case t of @@ -997,7 +1012,7 @@ data ModuleRef'' (c :: S.IsConcrete) (t :: ModuleIsTop) = ModuleRef'' _moduleRefModule :: Module 'Scoped t } -instance Show (RefNameType s) => Show (ModuleRef'' s t) where +instance (Show (RefNameType s)) => Show (ModuleRef'' s t) where show ModuleRef'' {..} = show _moduleRefName instance Eq (ModuleRef'' 'S.Concrete t) where @@ -1021,7 +1036,7 @@ newtype FixitySymbolEntry = FixitySymbolEntry } deriving stock (Show) -instance SingI t => CanonicalProjection (ModuleRef'' c t) (ModuleRef' c) where +instance (SingI t) => CanonicalProjection (ModuleRef'' c t) (ModuleRef' c) where project r = ModuleRef' (sing :&: r) -- | Symbols that a module exports @@ -1683,6 +1698,17 @@ makeLenses ''ModuleIndex makeLenses ''ArgumentBlock makeLenses ''NamedArgument makeLenses ''NamedApplication +makeLenses ''AliasDef + +instance SingI s => HasLoc (AliasDef s) where + getLoc AliasDef {..} = getLoc _aliasSyntaxKw <> getLocIdentifierType _aliasAsName + +instance SingI s => HasLoc (SyntaxDef s) where + getLoc = \case + SyntaxFixity t -> getLoc t + SyntaxOperator t -> getLoc t + SyntaxIterator t -> getLoc t + SyntaxAlias t -> getLoc t instance Eq ModuleIndex where (==) = (==) `on` (^. moduleIxModule . modulePath) @@ -1690,10 +1716,10 @@ instance Eq ModuleIndex where instance Hashable ModuleIndex where hashWithSalt s = hashWithSalt s . (^. moduleIxModule . modulePath) -instance SingI s => HasLoc (NamedArgument s) where +instance (SingI s) => HasLoc (NamedArgument s) where getLoc NamedArgument {..} = getLocSymbolType _namedArgName <> getLocExpressionType _namedArgValue -instance SingI s => HasLoc (ArgumentBlock s) where +instance (SingI s) => HasLoc (ArgumentBlock s) where getLoc ArgumentBlock {..} = case d of Just (l, r) -> getLoc l <> getLoc r Nothing -> getLocSpan _argBlockArgs @@ -1727,7 +1753,7 @@ instance HasAtomicity Expression where ExpressionRecordUpdate {} -> Aggregate updateFixity ExpressionParensRecordUpdate {} -> Atom -expressionAtomicity :: forall s. SingI s => ExpressionType s -> Atomicity +expressionAtomicity :: forall s. (SingI s) => ExpressionType s -> Atomicity expressionAtomicity e = case sing :: SStage s of SParsed -> atomicity e SScoped -> atomicity e @@ -1744,7 +1770,7 @@ instance HasAtomicity (Let 'Scoped) where instance HasAtomicity (PatternAtom 'Parsed) where atomicity = const Atom -instance SingI s => HasAtomicity (FunctionParameters s) where +instance (SingI s) => HasAtomicity (FunctionParameters s) where atomicity p | not (null (p ^. paramNames)) || p ^. paramImplicit == Implicit = Atom | otherwise = case sing :: SStage s of @@ -1763,7 +1789,7 @@ instance HasLoc (InductiveDef s) where instance HasLoc ModuleRef where getLoc (ModuleRef' (_ :&: r)) = getLoc r -instance SingI s => HasLoc (AxiomDef s) where +instance (SingI s) => HasLoc (AxiomDef s) where getLoc m = getLoc (m ^. axiomKw) <> getLocExpressionType (m ^. axiomType) instance HasLoc (OpenModule 'Scoped) where @@ -1821,22 +1847,22 @@ instance HasLoc (Function 'Scoped) where instance HasLoc (Let 'Scoped) where getLoc l = getLoc (l ^. letKw) <> getLoc (l ^. letExpression) -instance SingI s => HasLoc (CaseBranch s) where +instance (SingI s) => HasLoc (CaseBranch s) where getLoc c = getLoc (c ^. caseBranchPipe) <> getLocExpressionType (c ^. caseBranchExpression) -instance SingI s => HasLoc (Case s) where +instance (SingI s) => HasLoc (Case s) where getLoc c = getLoc (c ^. caseKw) <> getLoc (c ^. caseBranches . to last) instance HasLoc (List s) where getLoc List {..} = getLoc _listBracketL <> getLoc _listBracketR -instance SingI s => HasLoc (NamedApplication s) where +instance (SingI s) => HasLoc (NamedApplication s) where getLoc NamedApplication {..} = getLocIdentifierType _namedAppName <> getLoc (last _namedAppArgs) -instance SingI s => HasLoc (RecordUpdateField s) where +instance (SingI s) => HasLoc (RecordUpdateField s) where getLoc f = getLocSymbolType (f ^. fieldUpdateName) <> getLocExpressionType (f ^. fieldUpdateValue) -instance SingI s => HasLoc (RecordUpdate s) where +instance (SingI s) => HasLoc (RecordUpdate s) where getLoc r = getLoc (r ^. recordUpdateAtKw) <> getLocSpan (r ^. recordUpdateFields) instance HasLoc RecordUpdateApp where @@ -1866,15 +1892,15 @@ instance HasLoc Expression where ExpressionRecordUpdate i -> getLoc i ExpressionParensRecordUpdate i -> getLoc i -getLocIdentifierType :: forall s. SingI s => IdentifierType s -> Interval +getLocIdentifierType :: forall s. (SingI s) => IdentifierType s -> Interval getLocIdentifierType e = case sing :: SStage s of SParsed -> getLoc e SScoped -> getLoc e -instance SingI s => HasLoc (Iterator s) where +instance (SingI s) => HasLoc (Iterator s) where getLoc Iterator {..} = getLocIdentifierType _iteratorName <> getLocExpressionType _iteratorBody -instance SingI s => HasLoc (Import s) where +instance (SingI s) => HasLoc (Import s) where getLoc Import {..} = case sing :: SStage s of SParsed -> getLoc _importModule SScoped -> getLoc _importModule @@ -1891,12 +1917,12 @@ instance (SingI s, SingI t) => HasLoc (Module s t) where SModuleLocal -> getLoc (m ^. modulePath) SModuleTop -> getLoc (m ^. modulePath) -getLocSymbolType :: forall s. SingI s => SymbolType s -> Interval +getLocSymbolType :: forall s. (SingI s) => SymbolType s -> Interval getLocSymbolType = case sing :: SStage s of SParsed -> getLoc SScoped -> getLoc -getLocExpressionType :: forall s. SingI s => ExpressionType s -> Interval +getLocExpressionType :: forall s. (SingI s) => ExpressionType s -> Interval getLocExpressionType = case sing :: SStage s of SParsed -> getLoc SScoped -> getLoc @@ -1906,17 +1932,17 @@ instance HasLoc (SigArg s) where where Irrelevant (l, r) = _sigArgDelims -instance SingI s => HasLoc (NewFunctionClause s) where +instance (SingI s) => HasLoc (NewFunctionClause s) where getLoc NewFunctionClause {..} = getLoc _clausenPipeKw <> getLocExpressionType _clausenBody -instance SingI s => HasLoc (FunctionDefBody s) where +instance (SingI s) => HasLoc (FunctionDefBody s) where getLoc = \case SigBodyExpression e -> getLocExpressionType e SigBodyClauses cl -> getLocSpan cl -instance SingI s => HasLoc (FunctionDef s) where +instance (SingI s) => HasLoc (FunctionDef s) where getLoc FunctionDef {..} = (getLoc <$> _signDoc) ?<> (getLoc <$> _signPragmas) @@ -1955,28 +1981,28 @@ instance HasLoc PatternBinding where instance HasLoc (ListPattern s) where getLoc l = getLoc (l ^. listpBracketL) <> getLoc (l ^. listpBracketR) -getLocPatternParensType :: forall s. SingI s => PatternParensType s -> Interval +getLocPatternParensType :: forall s. (SingI s) => PatternParensType s -> Interval getLocPatternParensType = case sing :: SStage s of SScoped -> getLoc SParsed -> getLoc -instance SingI s => HasLoc (RecordPatternAssign s) where +instance (SingI s) => HasLoc (RecordPatternAssign s) where getLoc a = getLoc (a ^. recordPatternAssignField) <> getLocPatternParensType (a ^. recordPatternAssignPattern) -instance SingI s => HasLoc (FieldPun s) where +instance (SingI s) => HasLoc (FieldPun s) where getLoc f = getLocSymbolType (f ^. fieldPunField) -instance SingI s => HasLoc (RecordPatternItem s) where +instance (SingI s) => HasLoc (RecordPatternItem s) where getLoc = \case RecordPatternItemAssign a -> getLoc a RecordPatternItemFieldPun a -> getLoc a -instance SingI s => HasLoc (RecordPattern s) where +instance (SingI s) => HasLoc (RecordPattern s) where getLoc r = getLocIdentifierType (r ^. recordPatternConstructor) <>? (getLocSpan <$> nonEmpty (r ^. recordPatternItems)) -instance SingI s => HasLoc (PatternAtom s) where +instance (SingI s) => HasLoc (PatternAtom s) where getLoc = \case PatternAtomIden i -> getLocIden i PatternAtomWildcard w -> getLoc w @@ -2116,7 +2142,7 @@ instance IsApe ScopedIden ApeLeaf where } ) -instance SingI s => IsApe (ArgumentBlock s) ApeLeaf where +instance (SingI s) => IsApe (ArgumentBlock s) ApeLeaf where toApe b = ApeLeaf ( Leaf @@ -2125,7 +2151,7 @@ instance SingI s => IsApe (ArgumentBlock s) ApeLeaf where } ) -toApeIdentifierType :: forall s. SingI s => IdentifierType s -> Ape ApeLeaf +toApeIdentifierType :: forall s. (SingI s) => IdentifierType s -> Ape ApeLeaf toApeIdentifierType = case sing :: SStage s of SParsed -> toApe SScoped -> toApe @@ -2139,7 +2165,7 @@ instance IsApe Name ApeLeaf where } ) -instance SingI s => IsApe (NamedApplication s) ApeLeaf where +instance (SingI s) => IsApe (NamedApplication s) ApeLeaf where toApe NamedApplication {..} = mkApps f (toApe <$> _namedAppArgs) where f = toApeIdentifierType _namedAppName @@ -2278,11 +2304,17 @@ instance HasNameKind SymbolEntry where exportAllNames :: SimpleFold ExportInfo (S.Name' ()) exportAllNames = - exportSymbols . each . symbolEntry - <> exportModuleSymbols . each . moduleEntry - <> exportFixitySymbols . each . fixityEntry - -exportNameSpace :: forall ns. SingI ns => Lens' ExportInfo (HashMap Symbol (NameSpaceEntryType ns)) + exportSymbols + . each + . symbolEntry + <> exportModuleSymbols + . each + . moduleEntry + <> exportFixitySymbols + . each + . fixityEntry + +exportNameSpace :: forall ns. (SingI ns) => Lens' ExportInfo (HashMap Symbol (NameSpaceEntryType ns)) exportNameSpace = case sing :: SNameSpace ns of SNameSpaceSymbols -> exportSymbols SNameSpaceModules -> exportModuleSymbols diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 0fc5fd60ad..ef6819b248 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -421,11 +421,17 @@ instance SingI s => PrettyPrint (Import s) where Nothing -> Nothing Just as -> Just (ppCode Kw.kwAs <+> ppModulePathType as) +instance SingI s => PrettyPrint (AliasDef s) where + ppCode AliasDef {..} = + ppCode _aliasSyntaxKw <+> ppCode _aliasAliasKw <+> ppSymbolType _aliasName + <+> ppCode Kw.kwAssign <+> ppIdentifierType _aliasAsName + instance SingI s => PrettyPrint (SyntaxDef s) where ppCode = \case SyntaxFixity f -> ppCode f SyntaxOperator op -> ppCode op SyntaxIterator it -> ppCode it + SyntaxAlias it -> ppCode it instance PrettyPrint Literal where ppCode = noLoc . ppLiteral diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 455bdbe704..c0ce3d6780 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -2236,9 +2236,21 @@ checkSyntaxDef :: Sem r (SyntaxDef 'Scoped) checkSyntaxDef = \case SyntaxFixity fixDef -> SyntaxFixity <$> checkFixitySyntaxDef fixDef + SyntaxAlias a -> SyntaxAlias <$> checkAliasDef a SyntaxOperator opDef -> return $ SyntaxOperator opDef SyntaxIterator iterDef -> return $ SyntaxIterator iterDef +checkAliasDef :: + (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperSyntax] r) => + AliasDef 'Parsed -> + Sem r (AliasDef 'Scoped) +checkAliasDef = undefined + +reserveAliasDef :: (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperSyntax] r) => + AliasDef 'Parsed -> + Sem r () +reserveAliasDef = undefined + resolveSyntaxDef :: (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperSyntax] r) => SyntaxDef 'Parsed -> @@ -2247,6 +2259,7 @@ resolveSyntaxDef = \case SyntaxFixity fixDef -> resolveFixitySyntaxDef fixDef SyntaxOperator opDef -> resolveOperatorSyntaxDef opDef SyntaxIterator iterDef -> resolveIteratorSyntaxDef iterDef + SyntaxAlias a -> reserveAliasDef a ------------------------------------------------------------------------------- -- Check precedences are comparable diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs index 76731e917c..d110a8d23c 100644 --- a/src/Juvix/Data/Keyword/All.hs +++ b/src/Juvix/Data/Keyword/All.hs @@ -88,6 +88,9 @@ kwRightArrow = unicodeKw Str.toAscii Str.toUnicode kwSyntax :: Keyword kwSyntax = asciiKw Str.syntax +kwAlias :: Keyword +kwAlias = asciiKw Str.alias + kwFixity :: Keyword kwFixity = asciiKw Str.fixity diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 20f5088cca..682aed61e5 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -56,6 +56,9 @@ hiding = "hiding" include :: (IsString s) => s include = "include" +alias :: (IsString s) => s +alias = "alias" + import_ :: (IsString s) => s import_ = "import" From 7958b88bbd6bddfb8df6fd1465cd7ba0f0fee81e Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 23 Aug 2023 08:23:10 +0200 Subject: [PATCH 02/18] wip --- src/Juvix/Compiler/Concrete/Data/Scope.hs | 2 +- .../Compiler/Concrete/Data/Scope/Base.hs | 1 + src/Juvix/Compiler/Concrete/Language.hs | 102 +++++++++++------- src/Juvix/Compiler/Concrete/Print/Base.hs | 9 +- .../FromParsed/Analysis/Scoping.hs | 71 ++++++++---- .../Analysis/Scoping/Error/Types.hs | 4 +- 6 files changed, 127 insertions(+), 62 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/Scope.hs b/src/Juvix/Compiler/Concrete/Data/Scope.hs index 5a22dd1d32..4be28b29c6 100644 --- a/src/Juvix/Compiler/Concrete/Data/Scope.hs +++ b/src/Juvix/Compiler/Concrete/Data/Scope.hs @@ -16,7 +16,7 @@ import Juvix.Prelude nsEntry :: forall ns. SingI ns => Lens' (NameSpaceEntryType ns) (S.Name' ()) nsEntry = case sing :: SNameSpace ns of SNameSpaceModules -> moduleEntry - SNameSpaceSymbols -> symbolEntry + SNameSpaceSymbols -> preSymbolName SNameSpaceFixities -> fixityEntry mkModuleRef' :: SingI t => ModuleRef'' 'S.NotConcrete t -> ModuleRef' 'S.NotConcrete diff --git a/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs b/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs index ac387e824a..670475858c 100644 --- a/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs +++ b/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs @@ -59,6 +59,7 @@ data ScoperState = ScoperState -- | Local and top modules _scoperModules :: HashMap S.ModuleNameId (ModuleRef' 'S.NotConcrete), _scoperScope :: HashMap TopModulePath Scope, + _scoperAlias :: HashMap S.NameId PreSymbolEntry, _scoperSignatures :: HashMap S.NameId NameSignature, -- | Indexed by the inductive type. This is used for record updates _scoperRecordFields :: HashMap S.NameId RecordInfo, diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index ab7322abc9..9f08668dfc 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -44,7 +44,7 @@ type Delims = Irrelevant (Maybe (KeywordRef, KeywordRef)) type NameSpaceEntryType :: NameSpace -> GHC.Type type family NameSpaceEntryType s = res | res -> s where - NameSpaceEntryType 'NameSpaceSymbols = SymbolEntry + NameSpaceEntryType 'NameSpaceSymbols = PreSymbolEntry NameSpaceEntryType 'NameSpaceModules = ModuleSymbolEntry NameSpaceEntryType 'NameSpaceFixities = FixitySymbolEntry @@ -251,11 +251,10 @@ deriving stock instance Ord (Import 'Parsed) deriving stock instance Ord (Import 'Scoped) data AliasDef (s :: Stage) = AliasDef - { - _aliasSyntaxKw :: Irrelevant KeywordRef, - _aliasAliasKw :: Irrelevant KeywordRef, - _aliasName :: SymbolType s, - _aliasAsName :: IdentifierType s + { _aliasDefSyntaxKw :: Irrelevant KeywordRef, + _aliasDefAliasKw :: Irrelevant KeywordRef, + _aliasDefName :: SymbolType s, + _aliasDefAsName :: IdentifierType s } deriving stock instance (Show (AliasDef 'Parsed)) @@ -1021,10 +1020,24 @@ instance Eq (ModuleRef'' 'S.Concrete t) where instance Ord (ModuleRef'' 'S.Concrete t) where compare (ModuleRef'' n _ _) (ModuleRef'' n' _ _) = compare n n' +newtype Alias = Alias + { _aliasName :: S.Name' () + } + deriving stock (Show) + +-- | Either an alias or a symbol entry. +data PreSymbolEntry + = PreSymbolAlias Alias + | PreSymbolFinal SymbolEntry + deriving stock (Show) + +-- | A symbol which is not an alias. newtype SymbolEntry = SymbolEntry { _symbolEntry :: S.Name' () } - deriving stock (Show) + deriving stock (Show, Eq, Ord, Generic) + +instance Hashable SymbolEntry newtype ModuleSymbolEntry = ModuleSymbolEntry { _moduleEntry :: S.Name' () @@ -1041,7 +1054,7 @@ instance (SingI t) => CanonicalProjection (ModuleRef'' c t) (ModuleRef' c) where -- | Symbols that a module exports data ExportInfo = ExportInfo - { _exportSymbols :: HashMap Symbol SymbolEntry, + { _exportSymbols :: HashMap Symbol PreSymbolEntry, _exportModuleSymbols :: HashMap Symbol ModuleSymbolEntry, _exportFixitySymbols :: HashMap Symbol FixitySymbolEntry } @@ -1069,23 +1082,11 @@ deriving stock instance Ord (OpenModule 'Parsed) deriving stock instance Ord (OpenModule 'Scoped) -type ScopedIden = ScopedIden' 'S.Concrete - -newtype ScopedIden' (n :: S.IsConcrete) = ScopedIden - { _scopedIden :: RefNameType n +data ScopedIden = ScopedIden + { _scopedIden :: S.Name, + _scopedIdenAlias :: Maybe S.Name } - -deriving stock instance - (Eq (RefNameType s)) => Eq (ScopedIden' s) - -deriving stock instance - (Ord (RefNameType s)) => Ord (ScopedIden' s) - -deriving stock instance - (Show (RefNameType s)) => Show (ScopedIden' s) - -identifierName :: forall n. ScopedIden' n -> RefNameType n -identifierName (ScopedIden n) = n + deriving stock (Show, Eq, Ord) data Expression = ExpressionIdentifier ScopedIden @@ -1216,18 +1217,12 @@ data InfixApplication = InfixApplication } deriving stock (Show, Eq, Ord) -instance HasFixity InfixApplication where - getFixity (InfixApplication _ op _) = fromMaybe impossible (identifierName op ^. S.nameFixity) - data PostfixApplication = PostfixApplication { _postfixAppParameter :: Expression, _postfixAppOperator :: ScopedIden } deriving stock (Show, Eq, Ord) -instance HasFixity PostfixApplication where - getFixity (PostfixApplication _ op) = fromMaybe impossible (identifierName op ^. S.nameFixity) - data Let (s :: Stage) = Let { _letKw :: KeywordRef, _letInKw :: Irrelevant KeywordRef, @@ -1628,6 +1623,7 @@ newtype ModuleIndex = ModuleIndex } makeLenses ''PatternArg +makeLenses ''Alias makeLenses ''FieldPun makeLenses ''RecordPatternAssign makeLenses ''RecordPattern @@ -1639,7 +1635,7 @@ makeLenses ''RecordUpdateField makeLenses ''NonDefinitionsSection makeLenses ''DefinitionsSection makeLenses ''ProjectionDef -makeLenses ''ScopedIden' +makeLenses ''ScopedIden makeLenses ''SymbolEntry makeLenses ''ModuleSymbolEntry makeLenses ''FixitySymbolEntry @@ -1700,10 +1696,10 @@ makeLenses ''NamedArgument makeLenses ''NamedApplication makeLenses ''AliasDef -instance SingI s => HasLoc (AliasDef s) where - getLoc AliasDef {..} = getLoc _aliasSyntaxKw <> getLocIdentifierType _aliasAsName +instance (SingI s) => HasLoc (AliasDef s) where + getLoc AliasDef {..} = getLoc _aliasDefSyntaxKw <> getLocIdentifierType _aliasDefAsName -instance SingI s => HasLoc (SyntaxDef s) where +instance (SingI s) => HasLoc (SyntaxDef s) where getLoc = \case SyntaxFixity t -> getLoc t SyntaxOperator t -> getLoc t @@ -2185,7 +2181,7 @@ instance IsApe InfixApplication ApeLeaf where { _infixFixity = getFixity i, _infixLeft = toApe l, _infixRight = toApe r, - _infixIsDelimiter = isDelimiterStr (prettyText (identifierName op ^. S.nameConcrete)), + _infixIsDelimiter = isDelimiterStr (prettyText (op ^. scopedIden . S.nameConcrete)), _infixOp = ApeLeafExpression (ExpressionIdentifier op) } @@ -2281,6 +2277,14 @@ judocExamples (Judoc bs) = concatMap goGroup bs JudocExample e -> [e] _ -> mempty +instance HasLoc Alias where + getLoc = (^. aliasName . S.nameDefined) + +instance HasLoc PreSymbolEntry where + getLoc = \case + PreSymbolAlias a -> getLoc a + PreSymbolFinal a -> getLoc a + instance HasLoc SymbolEntry where getLoc = (^. symbolEntry . S.nameDefined) @@ -2306,7 +2310,7 @@ exportAllNames :: SimpleFold ExportInfo (S.Name' ()) exportAllNames = exportSymbols . each - . symbolEntry + . preSymbolName <> exportModuleSymbols . each . moduleEntry @@ -2324,3 +2328,29 @@ _ConstructorRhsRecord :: Traversal' (ConstructorRhs s) (RhsRecord s) _ConstructorRhsRecord f rhs = case rhs of ConstructorRhsRecord r -> ConstructorRhsRecord <$> f r _ -> pure rhs + +_DefinitionSyntax :: Traversal' (Definition s) (SyntaxDef s) +_DefinitionSyntax f x = case x of + DefinitionSyntax r -> DefinitionSyntax <$> f r + _ -> pure x + +_SyntaxAlias :: Traversal' (SyntaxDef s) (AliasDef s) +_SyntaxAlias f x = case x of + SyntaxAlias r -> SyntaxAlias <$> f r + _ -> pure x + +instance HasFixity PostfixApplication where + getFixity (PostfixApplication _ op) = fromMaybe impossible (op ^. scopedIden . S.nameFixity) + +instance HasFixity InfixApplication where + getFixity (InfixApplication _ op _) = fromMaybe impossible (op ^. scopedIden . S.nameFixity) + +-- preSymbolFinal :: Lens' PreSymbolEntry SymbolEntry +-- preSymbolFinal f = \case +-- PreSymbolAlias a -> PreSymbolAlias <$> traverseOf aliasEntry (preSymbolFinal f) a +-- PreSymbolFinal a -> PreSymbolFinal <$> f a + +preSymbolName :: Lens' PreSymbolEntry (S.Name' ()) +preSymbolName f = \case + PreSymbolAlias a -> PreSymbolAlias <$> traverseOf aliasName f a + PreSymbolFinal a -> PreSymbolFinal <$> traverseOf symbolEntry f a diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index ef6819b248..a5e3020d0d 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -423,8 +423,8 @@ instance SingI s => PrettyPrint (Import s) where instance SingI s => PrettyPrint (AliasDef s) where ppCode AliasDef {..} = - ppCode _aliasSyntaxKw <+> ppCode _aliasAliasKw <+> ppSymbolType _aliasName - <+> ppCode Kw.kwAssign <+> ppIdentifierType _aliasAsName + ppCode _aliasDefSyntaxKw <+> ppCode _aliasDefAliasKw <+> ppSymbolType _aliasDefName + <+> ppCode Kw.kwAssign <+> ppIdentifierType _aliasDefAsName instance SingI s => PrettyPrint (SyntaxDef s) where ppCode = \case @@ -1056,6 +1056,11 @@ instance SingI s => PrettyPrint (Statement s) where StatementAxiom a -> ppCode a StatementProjectionDef a -> ppCode a +instance PrettyPrint PreSymbolEntry where + ppCode = \case + PreSymbolAlias a -> undefined + PreSymbolFinal a -> undefined + instance PrettyPrint SymbolEntry where ppCode ent = noLoc diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index c0ce3d6780..2c3a0dcc34 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -39,6 +39,7 @@ iniScoperState = _scoperScope = mempty, _scoperSignatures = mempty, _scoperRecordFields = mempty, + _scoperAlias = mempty, _scoperConstructorFields = mempty } @@ -197,7 +198,7 @@ reserveSymbolSignatureOf :: Sem r S.Symbol reserveSymbolSignatureOf k d s = do sig <- mkNameSignature d - reserveSymbolOf k (Just sig) s + reserveSymbolOf False k (Just sig) s reserveSymbolOf :: forall (nameKind :: NameKind) (ns :: NameSpace) r. @@ -205,11 +206,12 @@ reserveSymbolOf :: ns ~ NameKindNameSpace nameKind, SingI ns ) => + Bool -> Sing nameKind -> Maybe NameSignature -> Symbol -> Sem r S.Symbol -reserveSymbolOf k nameSig s = do +reserveSymbolOf isAlias k nameSig s = do checkNotBound path <- gets (^. scopePath) strat <- ask @@ -217,11 +219,15 @@ reserveSymbolOf k nameSig s = do whenJust nameSig (modify' . set (scoperSignatures . at (s' ^. S.nameId)) . Just) modify (set (scopeNameSpaceLocal sns . at s) (Just s')) registerName (S.unqualifiedSymbol s') - let entry :: NameSpaceEntryType (NameKindNameSpace nameKind) + let + u = S.unConcrete s' + entry :: NameSpaceEntryType (NameKindNameSpace nameKind) entry = - let symE = SymbolEntry (S.unConcrete s') - modE = ModuleSymbolEntry (S.unConcrete s') - fixE = FixitySymbolEntry (S.unConcrete s') + let symE + | isAlias = PreSymbolAlias (Alias u) + | otherwise = PreSymbolFinal (SymbolEntry u) + modE = ModuleSymbolEntry u + fixE = FixitySymbolEntry u in case k of SKNameConstructor -> symE SKNameInductive -> symE @@ -272,7 +278,7 @@ bindVariableSymbol :: Members '[Error ScoperError, NameIdGen, State Scope, InfoTableBuilder, State ScoperState] r => Symbol -> Sem r S.Symbol -bindVariableSymbol = localBindings . ignoreSyntax . reserveSymbolOf SKNameLocal Nothing +bindVariableSymbol = localBindings . ignoreSyntax . reserveSymbolOf False SKNameLocal Nothing reserveInductiveSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r => @@ -284,7 +290,7 @@ reserveProjectionSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, State ScoperState] r => ProjectionDef 'Parsed -> Sem r S.Symbol -reserveProjectionSymbol d = reserveSymbolOf SKNameFunction Nothing (d ^. projectionField) +reserveProjectionSymbol d = reserveSymbolOf False SKNameFunction Nothing (d ^. projectionField) reserveConstructorSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r => @@ -407,7 +413,7 @@ getModuleExportInfo m = fromMaybeM err (gets (^? scoperModules . at (m ^. module -- | Do not call directly. Looks for a symbol in (possibly) nested local modules lookupSymbolAux :: forall r. - Members '[State ScoperState, State Scope, Output ModuleSymbolEntry, Output SymbolEntry, Output FixitySymbolEntry] r => + Members '[State ScoperState, State Scope, Output ModuleSymbolEntry, Output PreSymbolEntry, Output FixitySymbolEntry] r => [Symbol] -> Symbol -> Sem r () @@ -467,7 +473,7 @@ lookupQualifiedSymbol :: forall r. Members '[State Scope, State ScoperState] r => ([Symbol], Symbol) -> - Sem r ([SymbolEntry], [ModuleSymbolEntry], [FixitySymbolEntry]) + Sem r ([PreSymbolEntry], [ModuleSymbolEntry], [FixitySymbolEntry]) lookupQualifiedSymbol sms = do (es, (ms, fs)) <- runOutputList $ runOutputList $ execOutputList $ go sms return (es, ms, fs) @@ -507,12 +513,19 @@ lookupQualifiedSymbol sms = do ref <- toList t ] +-- | This assumes that alias do not have cycles. +normalizePreSymbolEntry :: Members '[State ScoperState] r => PreSymbolEntry -> Sem r SymbolEntry +normalizePreSymbolEntry = \case + PreSymbolFinal a -> return a + PreSymbolAlias a -> gets (^?! scoperAlias . at (a ^. aliasName . S.nameId) . _Just) >>= normalizePreSymbolEntry + checkQualifiedExpr :: (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r) => QualifiedName -> Sem r ScopedIden checkQualifiedExpr q@(QualifiedName (SymbolPath p) sym) = do es <- fst3 <$> lookupQualifiedSymbol (toList p, sym) + -- TODO handle aliases case es of [] -> notInScope [e] -> entryToScopedIden q' e @@ -521,12 +534,19 @@ checkQualifiedExpr q@(QualifiedName (SymbolPath p) sym) = do q' = NameQualified q notInScope = throw (ErrQualSymNotInScope (QualSymNotInScope q)) -entryToScopedIden :: Members '[InfoTableBuilder] r => Name -> SymbolEntry -> Sem r ScopedIden +entryToScopedIden :: Members '[InfoTableBuilder, State ScoperState] r => + Name -> PreSymbolEntry -> Sem r ScopedIden entryToScopedIden name e = do let scopedName :: S.Name - scopedName = set S.nameConcrete name (e ^. symbolEntry) + scopedName = set S.nameConcrete name (e ^. preSymbolName) + si <- case e of + PreSymbolFinal f -> return ScopedIden { + _scopedIden = set S.nameConcrete name (f ^. symbolEntry), + _scopedIdenAlias = Nothing + } + PreSymbolAlias {} -> undefined registerName scopedName - return (ScopedIden (set S.nameConcrete name (e ^. symbolEntry))) + return si -- | We gather all symbols which have been defined or marked to be public in the given scope. exportScope :: @@ -605,7 +625,7 @@ resolveFixitySyntaxDef :: FixitySyntaxDef 'Parsed -> Sem r () resolveFixitySyntaxDef fdef@FixitySyntaxDef {..} = topBindings $ do - sym <- reserveSymbolOf SKNameFixity Nothing _fixitySymbol + sym <- reserveSymbolOf False SKNameFixity Nothing _fixitySymbol let loc = getLoc _fixityInfo fi = _fixityInfo ^. withLocParam . withSourceValue same <- checkMaybeFixity loc $ fi ^. FI.fixityPrecSame @@ -1100,6 +1120,7 @@ checkSections sec = do goDefinitions :: DefinitionsSection 'Parsed -> Sem r' (DefinitionsSection 'Scoped) goDefinitions DefinitionsSection {..} = do mapM_ reserveDefinition _definitionsSection + mapM_ scanAlias (_definitionsSection ^.. each . _DefinitionSyntax . _SyntaxAlias) sec' <- mapM goDefinition _definitionsSection next' <- mapM goNonDefinitions _definitionsNext return @@ -1108,6 +1129,9 @@ checkSections sec = do _definitionsSection = sec' } where + scanAlias :: AliasDef 'Parsed -> Sem r' () + scanAlias = undefined + reserveDefinition :: Definition 'Parsed -> Sem r' () reserveDefinition = \case DefinitionSyntax s -> resolveSyntaxDef s @@ -1256,7 +1280,7 @@ reserveLocalModuleSymbol :: Symbol -> Sem r S.Symbol reserveLocalModuleSymbol = - ignoreSyntax . reserveSymbolOf SKNameLocalModule Nothing + ignoreSyntax . reserveSymbolOf False SKNameLocalModule Nothing checkLocalModule :: forall r. @@ -1634,7 +1658,10 @@ checkRecordPattern :: Sem r (RecordPattern 'Scoped) checkRecordPattern r = do c' <- getNameOfKind KNameConstructor (r ^. recordPatternConstructor) - let s = ScopedIden c' + let s = ScopedIden { + _scopedIden = c', + _scopedIdenAlias = undefined + } fields <- fromMaybeM (return (RecordNameSignature mempty)) (gets (^. scoperConstructorFields . at (c' ^. S.nameId))) l' <- if @@ -1819,6 +1846,7 @@ checkUnqualified s = do scope <- get -- Lookup at the global scope entries <- fst3 <$> lookupQualifiedSymbol ([], s) + -- TODO handle aliases case resolveShadowing entries of [] -> throw (ErrSymNotInScope (NotInScope s scope)) [x] -> entryToScopedIden n x @@ -1837,7 +1865,7 @@ checkFixitySymbol s = do case resolveShadowing entries of [] -> throw (ErrSymNotInScope (NotInScope s scope)) [x] -> return $ entryToSymbol x s - es -> throw (ErrAmbiguousSym (AmbiguousSym n (map (SymbolEntry . (^. fixityEntry)) es))) + es -> throw (ErrAmbiguousSym (AmbiguousSym n (map (PreSymbolFinal . SymbolEntry . (^. fixityEntry)) es))) where n = NameUnqualified s @@ -1907,6 +1935,7 @@ lookupNameOfKind :: Name -> Sem r (Maybe S.Name) lookupNameOfKind nameKind n = do + -- TODO handle alias entries <- mapMaybe filterEntry . fst3 <$> lookupQualifiedSymbol (path, sym) case entries of [] -> return Nothing @@ -2077,7 +2106,7 @@ checkIterator :: Sem r (Iterator 'Scoped) checkIterator iter = do _iteratorName <- checkName (iter ^. iteratorName) - case identifierName _iteratorName ^. S.nameIterator of + case _iteratorName ^. scopedIden . S.nameIterator of Just IteratorAttribs {..} -> do case _iteratorAttribsInitNum of Just n @@ -2345,7 +2374,7 @@ makeExpressionTable (ExpressionAtoms atoms _) = [recordUpdate] : [appOpExplicit] AssocNone -> P.InfixN | otherwise = Nothing where - S.Name' {..} = identifierName iden + S.Name' {..} = iden ^. scopedIden parseSymbolId :: S.NameId -> Parse ScopedIden parseSymbolId uid = P.token getIdentifierWithId mempty @@ -2353,7 +2382,7 @@ makeExpressionTable (ExpressionAtoms atoms _) = [recordUpdate] : [appOpExplicit] getIdentifierWithId :: ExpressionAtom 'Scoped -> Maybe ScopedIden getIdentifierWithId s = case s of AtomIdentifier iden - | uid == identifierName iden ^. S.nameId -> Just iden + | uid == iden ^. scopedIden . S.nameId -> Just iden _ -> Nothing recordUpdate :: P.Operator Parse Expression @@ -2540,7 +2569,7 @@ parseTerm = identifierNoFixity :: ExpressionAtom 'Scoped -> Maybe ScopedIden identifierNoFixity s = case s of AtomIdentifier iden - | not (S.hasFixity (identifierName iden)) -> Just iden + | not (S.hasFixity (iden ^. scopedIden)) -> Just iden _ -> Nothing parseBraces :: Parse Expression diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs index 3d8f8baee2..53fcdd445b 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs @@ -209,7 +209,7 @@ instance ToGenericError DuplicateIterator where locs = vsep $ map (pretty . getLoc) [_dupIteratorFirst, _dupIteratorFirst] data ExportEntries - = ExportEntriesSymbols (NonEmpty SymbolEntry) + = ExportEntriesSymbols (NonEmpty PreSymbolEntry) | ExportEntriesModules (NonEmpty ModuleSymbolEntry) | ExportEntriesFixities (NonEmpty FixitySymbolEntry) deriving stock (Show) @@ -382,7 +382,7 @@ instance ToGenericError UnusedIteratorDef where data AmbiguousSym = AmbiguousSym { _ambiguousSymName :: Name, - _ambiguousSymEntires :: [SymbolEntry] + _ambiguousSymEntires :: [PreSymbolEntry] } deriving stock (Show) From 27ceeba2640d26ae538f58f8f119a6066db82cc5 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 23 Aug 2023 17:12:50 +0200 Subject: [PATCH 03/18] ScopedIden --- src/Juvix/Compiler/Concrete/Extra.hs | 2 +- src/Juvix/Compiler/Concrete/Keywords.hs | 3 +- src/Juvix/Compiler/Concrete/Language.hs | 84 ++++++----- src/Juvix/Compiler/Concrete/Print/Base.hs | 7 +- .../FromParsed/Analysis/Scoping.hs | 142 +++++++++--------- 5 files changed, 127 insertions(+), 111 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs index 142ab7643e..9103a0752d 100644 --- a/src/Juvix/Compiler/Concrete/Extra.hs +++ b/src/Juvix/Compiler/Concrete/Extra.hs @@ -147,6 +147,6 @@ getExpressionAtomIden = \case getPatternAtomIden :: PatternAtom 'Scoped -> Maybe S.Name getPatternAtomIden = \case PatternAtomIden i -> case i of - PatternScopedConstructor c -> Just c + PatternScopedConstructor c -> Just (c ^. scopedIdenName) _ -> Nothing _ -> Nothing diff --git a/src/Juvix/Compiler/Concrete/Keywords.hs b/src/Juvix/Compiler/Concrete/Keywords.hs index 5a15532c11..c0acf1da3b 100644 --- a/src/Juvix/Compiler/Concrete/Keywords.hs +++ b/src/Juvix/Compiler/Concrete/Keywords.hs @@ -18,6 +18,8 @@ import Juvix.Data.Keyword.All delimParenR, delimSemicolon, -- keywords + + kwAlias, kwAs, kwAssign, kwAt, @@ -39,7 +41,6 @@ import Juvix.Data.Keyword.All kwLambda, kwLet, kwMapsTo, - kwAlias, kwModule, kwOpen, kwOperator, diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 9f08668dfc..b607307472 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -653,23 +653,17 @@ data PatternApp = PatternApp data PatternInfixApp = PatternInfixApp { _patInfixLeft :: PatternArg, - _patInfixConstructor :: S.Name, + _patInfixConstructor :: ScopedIden, _patInfixRight :: PatternArg } deriving stock (Show, Eq, Ord) -instance HasFixity PatternInfixApp where - getFixity (PatternInfixApp _ op _) = fromMaybe impossible (op ^. S.nameFixity) - data PatternPostfixApp = PatternPostfixApp { _patPostfixParameter :: PatternArg, - _patPostfixConstructor :: S.Name + _patPostfixConstructor :: ScopedIden } deriving stock (Show, Eq, Ord) -instance HasFixity PatternPostfixApp where - getFixity (PatternPostfixApp _ op) = fromMaybe impossible (op ^. S.nameFixity) - data PatternArg = PatternArg { _patternArgIsImplicit :: IsImplicit, _patternArgName :: Maybe S.Symbol, @@ -679,7 +673,7 @@ data PatternArg = PatternArg data Pattern = PatternVariable (SymbolType 'Scoped) - | PatternConstructor S.Name + | PatternConstructor ScopedIden | PatternApplication PatternApp | PatternList (ListPattern 'Scoped) | PatternInfixApplication PatternInfixApp @@ -689,27 +683,9 @@ data Pattern | PatternRecord (RecordPattern 'Scoped) deriving stock (Show, Eq, Ord) -instance HasAtomicity (ListPattern s) where - atomicity = const Atom - -instance HasAtomicity (RecordPattern s) where - atomicity = const Atom - -instance HasAtomicity Pattern where - atomicity e = case e of - PatternVariable {} -> Atom - PatternConstructor {} -> Atom - PatternApplication {} -> Aggregate appFixity - PatternInfixApplication a -> Aggregate (getFixity a) - PatternPostfixApplication p -> Aggregate (getFixity p) - PatternWildcard {} -> Atom - PatternList l -> atomicity l - PatternEmpty {} -> Atom - PatternRecord r -> atomicity r - data PatternScopedIden = PatternScopedVar S.Symbol - | PatternScopedConstructor S.Name + | PatternScopedConstructor ScopedIden deriving stock (Show, Ord, Eq) data PatternBinding = PatternBinding @@ -2125,7 +2101,7 @@ instance IsApe PatternInfixApp ApeLeaf where { _infixFixity = getFixity i, _infixLeft = toApe l, _infixRight = toApe r, - _infixIsDelimiter = isDelimiterStr (prettyText (op ^. S.nameConcrete)), + _infixIsDelimiter = isDelimiterStr (prettyText (op ^. scopedIdenName . S.nameConcrete)), _infixOp = ApeLeafPattern (PatternConstructor op) } @@ -2312,11 +2288,11 @@ exportAllNames = . each . preSymbolName <> exportModuleSymbols - . each - . moduleEntry + . each + . moduleEntry <> exportFixitySymbols - . each - . fixityEntry + . each + . fixityEntry exportNameSpace :: forall ns. (SingI ns) => Lens' ExportInfo (HashMap Symbol (NameSpaceEntryType ns)) exportNameSpace = case sing :: SNameSpace ns of @@ -2339,18 +2315,50 @@ _SyntaxAlias f x = case x of SyntaxAlias r -> SyntaxAlias <$> f r _ -> pure x +scopedIdenName :: Lens' ScopedIden S.Name +scopedIdenName f n = case n ^. scopedIdenAlias of + Nothing -> scopedIden f n + Just a -> do + a' <- f a + pure (set scopedIdenAlias (Just a') n) + +scopedIdenFixity :: ScopedIden -> Maybe Fixity +scopedIdenFixity s = fromMaybe (s ^. scopedIden . S.nameFixity) (s ^? scopedIdenAlias . _Just . S.nameFixity) + +scopedIdenNameId :: ScopedIden -> NameId +scopedIdenNameId s = fromMaybe (s ^. scopedIden . S.nameId) (s ^? scopedIdenAlias . _Just . S.nameId) + instance HasFixity PostfixApplication where getFixity (PostfixApplication _ op) = fromMaybe impossible (op ^. scopedIden . S.nameFixity) instance HasFixity InfixApplication where getFixity (InfixApplication _ op _) = fromMaybe impossible (op ^. scopedIden . S.nameFixity) --- preSymbolFinal :: Lens' PreSymbolEntry SymbolEntry --- preSymbolFinal f = \case --- PreSymbolAlias a -> PreSymbolAlias <$> traverseOf aliasEntry (preSymbolFinal f) a --- PreSymbolFinal a -> PreSymbolFinal <$> f a - preSymbolName :: Lens' PreSymbolEntry (S.Name' ()) preSymbolName f = \case PreSymbolAlias a -> PreSymbolAlias <$> traverseOf aliasName f a PreSymbolFinal a -> PreSymbolFinal <$> traverseOf symbolEntry f a + +instance HasFixity PatternInfixApp where + getFixity (PatternInfixApp _ op _) = fromMaybe impossible (op ^. scopedIdenName . S.nameFixity) + +instance HasFixity PatternPostfixApp where + getFixity (PatternPostfixApp _ op) = fromMaybe impossible (op ^. scopedIdenName . S.nameFixity) + +instance HasAtomicity (ListPattern s) where + atomicity = const Atom + +instance HasAtomicity (RecordPattern s) where + atomicity = const Atom + +instance HasAtomicity Pattern where + atomicity e = case e of + PatternVariable {} -> Atom + PatternConstructor {} -> Atom + PatternApplication {} -> Aggregate appFixity + PatternInfixApplication a -> Aggregate (getFixity a) + PatternPostfixApplication p -> Aggregate (getFixity p) + PatternWildcard {} -> Atom + PatternList l -> atomicity l + PatternEmpty {} -> Atom + PatternRecord r -> atomicity r diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index a5e3020d0d..e448ffc49f 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -423,8 +423,11 @@ instance SingI s => PrettyPrint (Import s) where instance SingI s => PrettyPrint (AliasDef s) where ppCode AliasDef {..} = - ppCode _aliasDefSyntaxKw <+> ppCode _aliasDefAliasKw <+> ppSymbolType _aliasDefName - <+> ppCode Kw.kwAssign <+> ppIdentifierType _aliasDefAsName + ppCode _aliasDefSyntaxKw + <+> ppCode _aliasDefAliasKw + <+> ppSymbolType _aliasDefName + <+> ppCode Kw.kwAssign + <+> ppIdentifierType _aliasDefAsName instance SingI s => PrettyPrint (SyntaxDef s) where ppCode = \case diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 2c3a0dcc34..60d7deca62 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -219,13 +219,12 @@ reserveSymbolOf isAlias k nameSig s = do whenJust nameSig (modify' . set (scoperSignatures . at (s' ^. S.nameId)) . Just) modify (set (scopeNameSpaceLocal sns . at s) (Just s')) registerName (S.unqualifiedSymbol s') - let - u = S.unConcrete s' + let u = S.unConcrete s' entry :: NameSpaceEntryType (NameKindNameSpace nameKind) entry = let symE - | isAlias = PreSymbolAlias (Alias u) - | otherwise = PreSymbolFinal (SymbolEntry u) + | isAlias = PreSymbolAlias (Alias u) + | otherwise = PreSymbolFinal (SymbolEntry u) modE = ModuleSymbolEntry u fixE = FixitySymbolEntry u in case k of @@ -451,7 +450,7 @@ mkModuleEntry (ModuleRef' (t :&: m)) = ModuleSymbolEntry $ case t of lookInExport :: forall r. - Members '[State ScoperState, Output SymbolEntry, Output ModuleSymbolEntry, Output FixitySymbolEntry] r => + Members '[State ScoperState, Output PreSymbolEntry, Output ModuleSymbolEntry, Output FixitySymbolEntry] r => Symbol -> [Symbol] -> ExportInfo -> @@ -475,12 +474,12 @@ lookupQualifiedSymbol :: ([Symbol], Symbol) -> Sem r ([PreSymbolEntry], [ModuleSymbolEntry], [FixitySymbolEntry]) lookupQualifiedSymbol sms = do - (es, (ms, fs)) <- runOutputList $ runOutputList $ execOutputList $ go sms + (es, (ms, fs)) <- runOutputList . runOutputList . execOutputList $ go sms return (es, ms, fs) where go :: forall r'. - Members '[State ScoperState, State Scope, Output SymbolEntry, Output ModuleSymbolEntry, Output FixitySymbolEntry] r' => + Members '[State ScoperState, State Scope, Output PreSymbolEntry, Output ModuleSymbolEntry, Output FixitySymbolEntry] r' => ([Symbol], Symbol) -> Sem r' () go (path, sym) = do @@ -534,17 +533,28 @@ checkQualifiedExpr q@(QualifiedName (SymbolPath p) sym) = do q' = NameQualified q notInScope = throw (ErrQualSymNotInScope (QualSymNotInScope q)) -entryToScopedIden :: Members '[InfoTableBuilder, State ScoperState] r => - Name -> PreSymbolEntry -> Sem r ScopedIden +entryToScopedIden :: + Members '[InfoTableBuilder, State ScoperState] r => + Name -> + PreSymbolEntry -> + Sem r ScopedIden entryToScopedIden name e = do let scopedName :: S.Name scopedName = set S.nameConcrete name (e ^. preSymbolName) si <- case e of - PreSymbolFinal f -> return ScopedIden { - _scopedIden = set S.nameConcrete name (f ^. symbolEntry), - _scopedIdenAlias = Nothing - } - PreSymbolAlias {} -> undefined + PreSymbolFinal {} -> + return + ScopedIden + { _scopedIden = scopedName, + _scopedIdenAlias = Nothing + } + PreSymbolAlias {} -> do + e' <- normalizePreSymbolEntry e + return + ScopedIden + { _scopedIdenAlias = Just scopedName, + _scopedIden = set S.nameConcrete name (e' ^. symbolEntry) + } registerName scopedName return si @@ -1130,7 +1140,7 @@ checkSections sec = do } where scanAlias :: AliasDef 'Parsed -> Sem r' () - scanAlias = undefined + scanAlias a = undefined reserveDefinition :: Definition 'Parsed -> Sem r' () reserveDefinition = \case @@ -1658,20 +1668,16 @@ checkRecordPattern :: Sem r (RecordPattern 'Scoped) checkRecordPattern r = do c' <- getNameOfKind KNameConstructor (r ^. recordPatternConstructor) - let s = ScopedIden { - _scopedIden = c', - _scopedIdenAlias = undefined - } - fields <- fromMaybeM (return (RecordNameSignature mempty)) (gets (^. scoperConstructorFields . at (c' ^. S.nameId))) + fields <- fromMaybeM (return (RecordNameSignature mempty)) (gets (^. scoperConstructorFields . at (c' ^. scopedIden . S.nameId))) l' <- if | null (r ^. recordPatternItems) -> return [] | otherwise -> do - when (null (fields ^. recordNames)) (throw (noFields s)) + when (null (fields ^. recordNames)) (throw (noFields c')) runReader fields (mapM checkItem (r ^. recordPatternItems)) return RecordPattern - { _recordPatternConstructor = s, + { _recordPatternConstructor = c', _recordPatternSignature = Irrelevant fields, _recordPatternItems = l' } @@ -1901,15 +1907,13 @@ checkPatternName :: checkPatternName n = do c <- getConstructorRef case c of - Just constr -> do - registerName constr - return (PatternScopedConstructor constr) -- the symbol is a constructor + Just constr -> return (PatternScopedConstructor constr) -- the symbol is a constructor Nothing -> case n of NameUnqualified {} -> PatternScopedVar <$> bindVariableSymbol sym -- the symbol is a variable NameQualified {} -> nameNotInScope n where sym = snd (splitName n) - getConstructorRef :: Sem r (Maybe S.Name) + getConstructorRef :: Sem r (Maybe ScopedIden) getConstructorRef = lookupNameOfKind KNameConstructor n nameNotInScope :: forall r a. Members '[Error ScoperError, State Scope] r => Name -> Sem r a @@ -1922,31 +1926,32 @@ nameNotInScope n = err >>= throw getNameOfKind :: forall r. - Members '[Error ScoperError, State Scope, State ScoperState] r => + Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r => NameKind -> Name -> - Sem r S.Name + Sem r ScopedIden getNameOfKind nameKind n = fromMaybeM (nameNotInScope n) (lookupNameOfKind nameKind n) lookupNameOfKind :: forall r. - Members '[Error ScoperError, State Scope, State ScoperState] r => + Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r => NameKind -> Name -> - Sem r (Maybe S.Name) + Sem r (Maybe ScopedIden) lookupNameOfKind nameKind n = do - -- TODO handle alias - entries <- mapMaybe filterEntry . fst3 <$> lookupQualifiedSymbol (path, sym) + entries <- lookupQualifiedSymbol (path, sym) >>= mapMaybeM filterEntry . fst3 case entries of [] -> return Nothing - [e] -> return (Just (set S.nameConcrete n e)) -- There is one constructor with such a name - es -> throw (ErrAmbiguousSym (AmbiguousSym n (map SymbolEntry es))) + [(_, s)] -> return (Just s) -- There is one constructor with such a name + es -> throw (ErrAmbiguousSym (AmbiguousSym n (map fst es))) where (path, sym) = splitName n - filterEntry :: SymbolEntry -> Maybe (S.Name' ()) - filterEntry e - | nameKind == getNameKind e = Just (e ^. symbolEntry) - | otherwise = Nothing + filterEntry :: PreSymbolEntry -> Sem r (Maybe (PreSymbolEntry, ScopedIden)) + filterEntry e = do + e' <- entryToScopedIden n e + return $ do + guard (nameKind == getNameKind e') + return (e, e') checkPatternBinding :: Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => @@ -2017,8 +2022,7 @@ checkExpressionAtom e = case e of checkRecordUpdate :: forall r. Members '[Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, NameIdGen] r => RecordUpdate 'Parsed -> Sem r (RecordUpdate 'Scoped) checkRecordUpdate RecordUpdate {..} = do tyName' <- getNameOfKind KNameInductive _recordUpdateTypeName - registerName tyName' - info <- getRecordInfo (ScopedIden tyName') + info <- getRecordInfo tyName' let sig = info ^. recordInfoSignature (vars', fields') <- withLocalScope $ do vs <- mapM bindVariableSymbol (toList (recordNameSignatureByIndex sig)) @@ -2032,7 +2036,7 @@ checkRecordUpdate RecordUpdate {..} = do } return RecordUpdate - { _recordUpdateTypeName = ScopedIden tyName', + { _recordUpdateTypeName = tyName', _recordUpdateFields = fields', _recordUpdateExtra = Irrelevant extra', _recordUpdateAtKw, @@ -2275,7 +2279,8 @@ checkAliasDef :: Sem r (AliasDef 'Scoped) checkAliasDef = undefined -reserveAliasDef :: (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperSyntax] r) => +reserveAliasDef :: + (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperSyntax] r) => AliasDef 'Parsed -> Sem r () reserveAliasDef = undefined @@ -2598,43 +2603,42 @@ makePatternTable :: PatternAtoms 'Scoped -> [[P.Operator ParsePat PatternArg]] makePatternTable (PatternAtoms latoms _) = [appOp] : operators where - getConstructorRef :: PatternAtom 'Scoped -> Maybe S.Name + getConstructorRef :: PatternAtom 'Scoped -> Maybe ScopedIden getConstructorRef = \case PatternAtomIden i -> case i of PatternScopedConstructor c -> Just c _ -> Nothing _ -> Nothing operators = mkSymbolTable (mapMaybe getConstructorRef (toList latoms)) - mkSymbolTable :: [S.Name] -> [[P.Operator ParsePat PatternArg]] + mkSymbolTable :: [ScopedIden] -> [[P.Operator ParsePat PatternArg]] mkSymbolTable = reverse . map (map snd) . groupSortOn' fst . mapMaybe unqualifiedSymbolOp where - unqualifiedSymbolOp :: S.Name -> Maybe (Precedence, P.Operator ParsePat PatternArg) - unqualifiedSymbolOp S.Name' {..} - | Just Fixity {..} <- _nameFixity, - _nameKind == KNameConstructor = Just $ - case _fixityArity of - Unary u -> (_fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId)) - where - unaryApp :: S.Name -> PatternArg -> PatternArg - unaryApp constrName = case u of - AssocPostfix -> explicitP . PatternPostfixApplication . (`PatternPostfixApp` constrName) - Binary b -> (_fixityPrecedence, infixLRN (binaryInfixApp <$> parseSymbolId _nameId)) - where - binaryInfixApp :: S.Name -> PatternArg -> PatternArg -> PatternArg - binaryInfixApp name argLeft = explicitP . PatternInfixApplication . PatternInfixApp argLeft name - infixLRN :: ParsePat (PatternArg -> PatternArg -> PatternArg) -> P.Operator ParsePat PatternArg - infixLRN = case b of - AssocLeft -> P.InfixL - AssocRight -> P.InfixR - AssocNone -> P.InfixN - | otherwise = Nothing - parseSymbolId :: S.NameId -> ParsePat S.Name + unqualifiedSymbolOp :: ScopedIden -> Maybe (Precedence, P.Operator ParsePat PatternArg) + unqualifiedSymbolOp constr = run . runFail $ do + Fixity {..} <- failMaybe (scopedIdenFixity constr) + let _nameId = scopedIdenNameId constr + return $ case _fixityArity of + Unary u -> (_fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId)) + where + unaryApp :: ScopedIden -> PatternArg -> PatternArg + unaryApp constrName = case u of + AssocPostfix -> explicitP . PatternPostfixApplication . (`PatternPostfixApp` constrName) + Binary b -> (_fixityPrecedence, infixLRN (binaryInfixApp <$> parseSymbolId _nameId)) + where + binaryInfixApp :: ScopedIden -> PatternArg -> PatternArg -> PatternArg + binaryInfixApp name argLeft = explicitP . PatternInfixApplication . PatternInfixApp argLeft name + infixLRN :: ParsePat (PatternArg -> PatternArg -> PatternArg) -> P.Operator ParsePat PatternArg + infixLRN = case b of + AssocLeft -> P.InfixL + AssocRight -> P.InfixR + AssocNone -> P.InfixN + parseSymbolId :: S.NameId -> ParsePat ScopedIden parseSymbolId uid = P.token getConstructorRefWithId mempty where - getConstructorRefWithId :: PatternAtom 'Scoped -> Maybe S.Name + getConstructorRefWithId :: PatternAtom 'Scoped -> Maybe ScopedIden getConstructorRefWithId s = do ref <- getConstructorRef s - guard (ref ^. S.nameId == uid) + guard (scopedIdenNameId ref == uid) return ref -- Application by juxtaposition. @@ -2681,10 +2685,10 @@ parsePatternTerm = do explicitP . PatternConstructor <$> P.token constructorNoFixity mempty where - constructorNoFixity :: PatternAtom 'Scoped -> Maybe S.Name + constructorNoFixity :: PatternAtom 'Scoped -> Maybe ScopedIden constructorNoFixity s = case s of PatternAtomIden (PatternScopedConstructor ref) - | not (S.hasFixity n) -> Just ref + | not (S.hasFixity (n ^. scopedIdenName)) -> Just ref where n = ref _ -> Nothing From 4738ea3309c437072f15be8d1a3a7904a1aa7216 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 23 Aug 2023 19:00:06 +0200 Subject: [PATCH 04/18] translate and parse --- src/Juvix/Compiler/Concrete/Language.hs | 5 +- src/Juvix/Compiler/Concrete/Print/Base.hs | 7 ++- .../FromParsed/Analysis/Scoping.hs | 51 +++++++++++++++---- .../FromParsed/Analysis/Scoping/Error.hs | 2 + .../Analysis/Scoping/Error/Types.hs | 22 ++++++++ .../Concrete/Translation/FromSource.hs | 16 ++++-- .../Internal/Translation/FromConcrete.hs | 21 ++++---- tests/positive/Alias.juvix | 11 ++++ 8 files changed, 108 insertions(+), 27 deletions(-) create mode 100644 tests/positive/Alias.juvix diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index b607307472..c3e37018e7 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -37,7 +37,7 @@ import Juvix.Data.Keyword import Juvix.Data.NameKind import Juvix.Parser.Lexer (isDelimiterStr) import Juvix.Prelude hiding (show) -import Juvix.Prelude.Pretty (prettyText) +import Juvix.Prelude.Pretty (Pretty, pretty, prettyText) import Prelude (show) type Delims = Irrelevant (Maybe (KeywordRef, KeywordRef)) @@ -1749,6 +1749,9 @@ instance (SingI s) => HasAtomicity (FunctionParameters s) where SParsed -> atomicity (p ^. paramType) SScoped -> atomicity (p ^. paramType) +instance Pretty ScopedIden where + pretty = pretty . (^. scopedIdenName) + instance HasLoc ScopedIden where getLoc = getLoc . (^. scopedIden) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index e448ffc49f..eccb67c632 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -1061,8 +1061,11 @@ instance SingI s => PrettyPrint (Statement s) where instance PrettyPrint PreSymbolEntry where ppCode = \case - PreSymbolAlias a -> undefined - PreSymbolFinal a -> undefined + PreSymbolAlias a -> ppCode a + PreSymbolFinal a -> ppCode a + +instance PrettyPrint Alias where + ppCode _ = noLoc "TODO PrettyPrint Alias" instance PrettyPrint SymbolEntry where ppCode ent = diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 60d7deca62..d8340a5fe5 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -285,6 +285,13 @@ reserveInductiveSymbol :: Sem r S.Symbol reserveInductiveSymbol d = reserveSymbolSignatureOf SKNameInductive d (d ^. inductiveName) +-- | The NameKind assigned to the alias is irrelevant. +reserveAliasSymbol :: + Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, State ScoperState] r => + Symbol -> + Sem r S.Symbol +reserveAliasSymbol = reserveSymbolOf True SKNameLocal Nothing + reserveProjectionSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, State ScoperState] r => ProjectionDef 'Parsed -> @@ -518,13 +525,12 @@ normalizePreSymbolEntry = \case PreSymbolFinal a -> return a PreSymbolAlias a -> gets (^?! scoperAlias . at (a ^. aliasName . S.nameId) . _Just) >>= normalizePreSymbolEntry -checkQualifiedExpr :: +checkQualifiedName :: (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r) => QualifiedName -> Sem r ScopedIden -checkQualifiedExpr q@(QualifiedName (SymbolPath p) sym) = do +checkQualifiedName q@(QualifiedName (SymbolPath p) sym) = do es <- fst3 <$> lookupQualifiedSymbol (toList p, sym) - -- TODO handle aliases case es of [] -> notInScope [e] -> entryToScopedIden q' e @@ -533,6 +539,11 @@ checkQualifiedExpr q@(QualifiedName (SymbolPath p) sym) = do q' = NameQualified q notInScope = throw (ErrQualSymNotInScope (QualSymNotInScope q)) +scopedIdenToPreSymbolEntry :: ScopedIden -> PreSymbolEntry +scopedIdenToPreSymbolEntry s = case s ^. scopedIdenAlias of + Just a -> PreSymbolAlias (Alias (S.unConcrete a)) + Nothing -> PreSymbolFinal (SymbolEntry (S.unConcrete (s ^. scopedIden))) + entryToScopedIden :: Members '[InfoTableBuilder, State ScoperState] r => Name -> @@ -1140,7 +1151,20 @@ checkSections sec = do } where scanAlias :: AliasDef 'Parsed -> Sem r' () - scanAlias a = undefined + scanAlias a = do + aliasId <- gets (^?! scopeLocalSymbols . at (a ^. aliasDefName) . _Just . S.nameId) + asName <- scopedIdenToPreSymbolEntry <$> checkName (a ^. aliasDefAsName) + modify' (set (scoperAlias . at aliasId) (Just asName)) + checkLoop aliasId + where + checkLoop :: NameId -> Sem r' () + checkLoop = evalState (mempty :: HashSet NameId) . go + where + go :: Members '[State (HashSet NameId), Error ScoperError, State ScoperState] s => NameId -> Sem s () + go i = do + whenM (gets (HashSet.member i)) (throw (ErrAliasCycle (AliasCycle a))) + modify' (HashSet.insert i) + whenJustM (gets (^? scoperAlias . at i . _Just . preSymbolName . S.nameId)) go reserveDefinition :: Definition 'Parsed -> Sem r' () reserveDefinition = \case @@ -1852,7 +1876,6 @@ checkUnqualified s = do scope <- get -- Lookup at the global scope entries <- fst3 <$> lookupQualifiedSymbol ([], s) - -- TODO handle aliases case resolveShadowing entries of [] -> throw (ErrSymNotInScope (NotInScope s scope)) [x] -> entryToScopedIden n x @@ -1995,7 +2018,7 @@ checkName :: Name -> Sem r ScopedIden checkName n = case n of - NameQualified q -> checkQualifiedExpr q + NameQualified q -> checkQualifiedName q NameUnqualified s -> checkUnqualified s checkExpressionAtom :: @@ -2277,16 +2300,24 @@ checkAliasDef :: (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperSyntax] r) => AliasDef 'Parsed -> Sem r (AliasDef 'Scoped) -checkAliasDef = undefined +checkAliasDef AliasDef {..} = do + aliasName' :: S.Symbol <- gets (^?! scopeLocalSymbols . at _aliasDefName . _Just) + asName' <- checkName _aliasDefAsName + return + AliasDef + { _aliasDefName = aliasName', + _aliasDefAsName = asName', + .. + } reserveAliasDef :: - (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperSyntax] r) => + (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperSyntax, Reader BindingStrategy] r) => AliasDef 'Parsed -> Sem r () -reserveAliasDef = undefined +reserveAliasDef = void . reserveAliasSymbol . (^. aliasDefName) resolveSyntaxDef :: - (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperSyntax] r) => + (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperSyntax, Reader BindingStrategy] r) => SyntaxDef 'Parsed -> Sem r () resolveSyntaxDef = \case diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs index 9131bec2e6..c791f06aef 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs @@ -46,6 +46,7 @@ data ScoperError | ErrConstructorNotARecord ConstructorNotARecord | ErrPrecedenceInconsistency PrecedenceInconsistencyError | ErrIncomparablePrecedences IncomaprablePrecedences + | ErrAliasCycle AliasCycle instance ToGenericError ScoperError where genericError = \case @@ -83,3 +84,4 @@ instance ToGenericError ScoperError where ErrConstructorNotARecord e -> genericError e ErrPrecedenceInconsistency e -> genericError e ErrIncomparablePrecedences e -> genericError e + ErrAliasCycle e -> genericError e diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs index 53fcdd445b..874f3083e4 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs @@ -829,3 +829,25 @@ instance ToGenericError IncomaprablePrecedences where where i :: Interval i = getLoc _incomparablePrecedencesName1 + +newtype AliasCycle = AliasCycle + { _aliasCycleDef :: (AliasDef 'Parsed) + } + deriving stock (Show) + +instance ToGenericError AliasCycle where + genericError AliasCycle {..} = do + opts <- fromGenericOptions <$> ask + let msg = + "The definition of" + <+> ppCode opts (_aliasCycleDef ^. aliasDefName) + <+> "creates an alias cycle." + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = mkAnsiText msg, + _genericErrorIntervals = [i] + } + where + i :: Interval + i = getLoc _aliasCycleDef diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 03f9d537a0..53aba4d005 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -500,9 +500,19 @@ builtinStatement = do syntaxDef :: forall r. (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (SyntaxDef 'Parsed) syntaxDef = do syn <- kw kwSyntax - (SyntaxFixity <$> fixitySyntaxDef syn) - <|> (SyntaxOperator <$> operatorSyntaxDef syn) - <|> (SyntaxIterator <$> iteratorSyntaxDef syn) + SyntaxFixity <$> fixitySyntaxDef syn + <|> SyntaxOperator <$> operatorSyntaxDef syn + <|> SyntaxIterator <$> iteratorSyntaxDef syn + <|> SyntaxAlias <$> aliasDef syn + +aliasDef :: forall r. (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => KeywordRef -> ParsecS r (AliasDef 'Parsed) +aliasDef synKw = do + let _aliasDefSyntaxKw = Irrelevant synKw + _aliasDefAliasKw <- Irrelevant <$> kw kwAlias + _aliasDefName <- symbol + kw kwAssign + _aliasDefAsName <- name + return AliasDef {..} -------------------------------------------------------------------------------- -- Operator syntax declaration diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 015012ec84..23c74b57e1 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -182,10 +182,12 @@ goPragmas p = do p' <- ask return $ p' <> p ^. _Just . withLocParam . withSourceValue -goName :: S.Name -> Internal.Name -goName name = +goScopedIden :: ScopedIden -> Internal.Name +goScopedIden iden = set Internal.namePretty prettyStr (goSymbol (S.nameUnqualify name)) where + name :: S.Name + name = iden ^. scopedIden prettyStr :: Text prettyStr = prettyText name @@ -841,7 +843,7 @@ goExpression = \case KNameTopModule -> impossible KNameFixity -> impossible where - n' = goName (x ^. scopedIden) + n' = goScopedIden x goLet :: Let 'Scoped -> Sem r Internal.Let goLet l = do @@ -992,7 +994,7 @@ goPatternApplication a = uncurry mkConstructorApp <$> viewApp (PatternApplicatio goPatternConstructor :: Members '[Builtins, NameIdGen, Error ScoperError] r => - S.Name -> + ScopedIden -> Sem r Internal.ConstructorApp goPatternConstructor a = uncurry mkConstructorApp <$> viewApp (PatternConstructor a) @@ -1010,17 +1012,17 @@ goPostfixPatternApplication a = uncurry mkConstructorApp <$> viewApp (PatternPos viewApp :: forall r. Members '[Builtins, NameIdGen, Error ScoperError] r => Pattern -> Sem r (Internal.ConstrName, [Internal.PatternArg]) viewApp p = case p of - PatternConstructor c -> return (goConstructorRef c, []) + PatternConstructor c -> return (goScopedIden c, []) PatternApplication app@(PatternApp _ r) -> do r' <- goPatternArg r second (`snoc` r') <$> viewAppLeft app PatternInfixApplication (PatternInfixApp l c r) -> do l' <- goPatternArg l r' <- goPatternArg r - return (goConstructorRef c, [l', r']) + return (goScopedIden c, [l', r']) PatternPostfixApplication (PatternPostfixApp l c) -> do l' <- goPatternArg l - return (goConstructorRef c, [l']) + return (goScopedIden c, [l']) PatternVariable {} -> err PatternRecord {} -> err PatternWildcard {} -> err @@ -1033,9 +1035,6 @@ viewApp p = case p of | otherwise = viewApp (l ^. patternArgPattern) err = throw (ErrConstructorExpectedLeftApplication (ConstructorExpectedLeftApplication p)) -goConstructorRef :: S.Name -> Internal.Name -goConstructorRef n = goName n - goPatternArg :: Members '[Builtins, NameIdGen, Error ScoperError] r => PatternArg -> Sem r Internal.PatternArg goPatternArg p = do pat' <- goPattern (p ^. patternArgPattern) @@ -1060,7 +1059,7 @@ goPattern p = case p of goRecordPattern :: forall r. Members '[NameIdGen, Error ScoperError, Builtins] r => RecordPattern 'Scoped -> Sem r Internal.Pattern goRecordPattern r = do - let constr = goName (r ^. recordPatternConstructor . scopedIden) + let constr = goScopedIden (r ^. recordPatternConstructor) params' <- mkPatterns return ( Internal.PatternConstructorApp diff --git a/tests/positive/Alias.juvix b/tests/positive/Alias.juvix new file mode 100644 index 0000000000..d8c4c6c402 --- /dev/null +++ b/tests/positive/Alias.juvix @@ -0,0 +1,11 @@ +module Alias; + +module M; + axiom T : Type; -- line 4 + syntax alias A := T; -- line 5 +end; +syntax alias A := M.T; -- line 7 +open M; +axiom K : A; -- line 9 + +end; From b253eaca95f26cb96080661e637dd6d30b263322 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 23 Aug 2023 19:16:09 +0200 Subject: [PATCH 05/18] pp Alias --- src/Juvix/Compiler/Concrete/Print/Base.hs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index eccb67c632..2b89ea2e98 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -1065,7 +1065,15 @@ instance PrettyPrint PreSymbolEntry where PreSymbolFinal a -> ppCode a instance PrettyPrint Alias where - ppCode _ = noLoc "TODO PrettyPrint Alias" + ppCode a = + noLoc + ( kindWord + P.<+> C.code ((pretty (a ^. aliasName . S.nameVerbatim))) + P.<+> "defined at" + P.<+> pretty (getLoc a) + ) + where + kindWord :: Doc Ann = "Alias" instance PrettyPrint SymbolEntry where ppCode ent = From 7b5cefe2786b95fc82fd5bc5d684d64ad9db16cb Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 23 Aug 2023 23:58:24 +0200 Subject: [PATCH 06/18] fix loop and add test --- .../FromParsed/Analysis/Scoping.hs | 39 ++++++++++--------- test/Scope/Negative.hs | 7 ++++ tests/negative/AliasCycle.juvix | 5 +++ 3 files changed, 32 insertions(+), 19 deletions(-) create mode 100644 tests/negative/AliasCycle.juvix diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index d8340a5fe5..0df754e302 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -528,22 +528,17 @@ normalizePreSymbolEntry = \case checkQualifiedName :: (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r) => QualifiedName -> - Sem r ScopedIden + Sem r PreSymbolEntry checkQualifiedName q@(QualifiedName (SymbolPath p) sym) = do es <- fst3 <$> lookupQualifiedSymbol (toList p, sym) case es of [] -> notInScope - [e] -> entryToScopedIden q' e + [e] -> return e _ -> throw (ErrAmbiguousSym (AmbiguousSym q' es)) where q' = NameQualified q notInScope = throw (ErrQualSymNotInScope (QualSymNotInScope q)) -scopedIdenToPreSymbolEntry :: ScopedIden -> PreSymbolEntry -scopedIdenToPreSymbolEntry s = case s ^. scopedIdenAlias of - Just a -> PreSymbolAlias (Alias (S.unConcrete a)) - Nothing -> PreSymbolFinal (SymbolEntry (S.unConcrete (s ^. scopedIden))) - entryToScopedIden :: Members '[InfoTableBuilder, State ScoperState] r => Name -> @@ -1153,7 +1148,7 @@ checkSections sec = do scanAlias :: AliasDef 'Parsed -> Sem r' () scanAlias a = do aliasId <- gets (^?! scopeLocalSymbols . at (a ^. aliasDefName) . _Just . S.nameId) - asName <- scopedIdenToPreSymbolEntry <$> checkName (a ^. aliasDefAsName) + asName <- checkName (a ^. aliasDefAsName) modify' (set (scoperAlias . at aliasId) (Just asName)) checkLoop aliasId where @@ -1868,17 +1863,17 @@ scopedFunction fref n = do registerName scoped return scoped -checkUnqualified :: +checkUnqualifiedName :: (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r) => Symbol -> - Sem r ScopedIden -checkUnqualified s = do + Sem r PreSymbolEntry +checkUnqualifiedName s = do scope <- get -- Lookup at the global scope entries <- fst3 <$> lookupQualifiedSymbol ([], s) case resolveShadowing entries of [] -> throw (ErrSymNotInScope (NotInScope s scope)) - [x] -> entryToScopedIden n x + [x] -> return x es -> throw (ErrAmbiguousSym (AmbiguousSym n es)) where n = NameUnqualified s @@ -2016,17 +2011,23 @@ checkPatternAtom = \case checkName :: (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r) => Name -> - Sem r ScopedIden + Sem r PreSymbolEntry checkName n = case n of NameQualified q -> checkQualifiedName q - NameUnqualified s -> checkUnqualified s + NameUnqualified s -> checkUnqualifiedName s + +checkScopedIden :: + (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r) => + Name -> + Sem r ScopedIden +checkScopedIden n = checkName n >>= entryToScopedIden n checkExpressionAtom :: Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => ExpressionAtom 'Parsed -> Sem r (NonEmpty (ExpressionAtom 'Scoped)) checkExpressionAtom e = case e of - AtomIdentifier n -> pure . AtomIdentifier <$> checkName n + AtomIdentifier n -> pure . AtomIdentifier <$> checkScopedIden n AtomLambda lam -> pure . AtomLambda <$> checkLambda lam AtomCase c -> pure . AtomCase <$> checkCase c AtomLet letBlock -> pure . AtomLet <$> checkLet letBlock @@ -2087,7 +2088,7 @@ checkNamedApplication :: NamedApplication 'Parsed -> Sem r (NamedApplication 'Scoped) checkNamedApplication napp = do - _namedAppName <- checkName (napp ^. namedAppName) + _namedAppName <- checkScopedIden (napp ^. namedAppName) _namedAppSignature <- Irrelevant <$> getNameSignature _namedAppName _namedAppArgs <- mapM checkArgumentBlock (napp ^. namedAppArgs) return NamedApplication {..} @@ -2132,7 +2133,7 @@ checkIterator :: Iterator 'Parsed -> Sem r (Iterator 'Scoped) checkIterator iter = do - _iteratorName <- checkName (iter ^. iteratorName) + _iteratorName <- checkScopedIden (iter ^. iteratorName) case _iteratorName ^. scopedIden . S.nameIterator of Just IteratorAttribs {..} -> do case _iteratorAttribsInitNum of @@ -2215,7 +2216,7 @@ checkParens :: checkParens e@(ExpressionAtoms as _) = case as of p :| [] -> case p of AtomIdentifier s -> do - scopedId <- checkName s + scopedId <- checkScopedIden s let scopedIdenNoFix = over scopedIden (set S.nameFixity Nothing) scopedId return (ExpressionParensIdentifier scopedIdenNoFix) AtomIterator i -> ExpressionIterator . set iteratorParens True <$> checkIterator i @@ -2302,7 +2303,7 @@ checkAliasDef :: Sem r (AliasDef 'Scoped) checkAliasDef AliasDef {..} = do aliasName' :: S.Symbol <- gets (^?! scopeLocalSymbols . at _aliasDefName . _Just) - asName' <- checkName _aliasDefAsName + asName' <- checkScopedIden _aliasDefAsName return AliasDef { _aliasDefName = aliasName', diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index 44ab638c2f..57f6cae954 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -322,5 +322,12 @@ scoperErrorTests = $(mkRelFile "IncomparablePrecedences.juvix") $ \case ErrIncomparablePrecedences {} -> Nothing + _ -> wrongError, + NegTest + "Alias cycle" + $(mkRelDir ".") + $(mkRelFile "AliasCycle.juvix") + $ \case + ErrAliasCycle {} -> Nothing _ -> wrongError ] diff --git a/tests/negative/AliasCycle.juvix b/tests/negative/AliasCycle.juvix new file mode 100644 index 0000000000..2e6ce0838a --- /dev/null +++ b/tests/negative/AliasCycle.juvix @@ -0,0 +1,5 @@ +module AliasCycle; + +syntax alias x1 := x2; +syntax alias x2 := x3; +syntax alias x3 := x1; From 06d6839a4079eff850290729c098ebb3c61726ff Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 00:25:39 +0200 Subject: [PATCH 07/18] set namekind --- src/Juvix/Compiler/Concrete/Print/Base.hs | 1 + .../Translation/FromParsed/Analysis/Scoping.hs | 12 +++++++----- tests/positive/Alias.juvix | 18 ++++++++++-------- 3 files changed, 18 insertions(+), 13 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 2b89ea2e98..fe1abfeffb 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -406,6 +406,7 @@ instance SingI t => PrettyPrint (ModuleRef'' 'S.NotConcrete t) where instance PrettyPrint (ModuleRef'' 'S.Concrete t) where ppCode m = ppCode (m ^. moduleRefName) +-- FIXME this is wrong instance PrettyPrint ScopedIden where ppCode = ppCode . (^. scopedIden) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 0df754e302..b2e0d38af5 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -545,8 +545,10 @@ entryToScopedIden :: PreSymbolEntry -> Sem r ScopedIden entryToScopedIden name e = do - let scopedName :: S.Name - scopedName = set S.nameConcrete name (e ^. preSymbolName) + let helper :: S.Name' x -> S.Name + helper = set S.nameConcrete name + scopedName :: S.Name + scopedName = helper (e ^. preSymbolName) si <- case e of PreSymbolFinal {} -> return @@ -558,10 +560,10 @@ entryToScopedIden name e = do e' <- normalizePreSymbolEntry e return ScopedIden - { _scopedIdenAlias = Just scopedName, - _scopedIden = set S.nameConcrete name (e' ^. symbolEntry) + { _scopedIdenAlias = Just (set S.nameKind (getNameKind e') scopedName), + _scopedIden = helper (e' ^. symbolEntry) } - registerName scopedName + registerName (si ^. scopedIdenName) return si -- | We gather all symbols which have been defined or marked to be public in the given scope. diff --git a/tests/positive/Alias.juvix b/tests/positive/Alias.juvix index d8c4c6c402..7d0702e1a7 100644 --- a/tests/positive/Alias.juvix +++ b/tests/positive/Alias.juvix @@ -1,11 +1,13 @@ module Alias; -module M; - axiom T : Type; -- line 4 - syntax alias A := T; -- line 5 -end; -syntax alias A := M.T; -- line 7 -open M; -axiom K : A; -- line 9 +syntax alias Boolean := Bool; +syntax alias ⊥ := false; +syntax alias ⊤ := true; -end; +type Bool := + | false + | true; + +not : Boolean -> Boolean + | ⊥ := ⊤ + | ⊤ := ⊥; From 49fec40863e3a410c386ef6fb119769cf1bb885f Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 13:00:42 +0200 Subject: [PATCH 08/18] refactor AName --- src/Juvix/Compiler/Concrete/Data/Highlight.hs | 14 ++++----- .../Concrete/Data/InfoTableBuilder.hs | 2 +- .../Compiler/Concrete/Data/ScopedName.hs | 29 ++++++++++++++----- src/Juvix/Compiler/Concrete/Print/Base.hs | 5 ++-- .../FromParsed/Analysis/Scoping.hs | 28 +++--------------- 5 files changed, 36 insertions(+), 42 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/Highlight.hs b/src/Juvix/Compiler/Concrete/Data/Highlight.hs index 4459c3d767..d67b7c000f 100644 --- a/src/Juvix/Compiler/Concrete/Data/Highlight.hs +++ b/src/Juvix/Compiler/Concrete/Data/Highlight.hs @@ -67,14 +67,14 @@ goFaceName n = do return (WithLoc (getLoc n) (PropertyFace f)) goGotoProperty :: AName -> WithLoc PropertyGoto -goGotoProperty (AName n) = WithLoc (getLoc n) PropertyGoto {..} +goGotoProperty n = WithLoc (getLoc n) PropertyGoto {..} where - _gotoPos = n ^. nameDefined . intervalStart - _gotoFile = n ^. nameDefined . intervalFile + _gotoPos = n ^. anameDefinedLoc . intervalStart + _gotoFile = n ^. anameDefinedLoc . intervalFile goDocProperty :: Scoped.DocTable -> Internal.TypesTable -> AName -> Maybe (WithLoc PropertyDoc) -goDocProperty doctbl tbl a@(AName n) = do - let ty :: Maybe Internal.Expression = tbl ^. at (n ^. nameId) - d <- ppDocDefault a ty (doctbl ^. at (n ^. nameId)) +goDocProperty doctbl tbl a = do + let ty :: Maybe Internal.Expression = tbl ^. at (a ^. anameDocId) + d <- ppDocDefault a ty (doctbl ^. at (a ^. anameDocId)) let (_docText, _docSExp) = renderEmacs (layoutPretty defaultLayoutOptions d) - return (WithLoc (getLoc n) PropertyDoc {..}) + return (WithLoc (getLoc a) PropertyDoc {..}) diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs index 92f743cffe..ced01531bc 100644 --- a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs @@ -57,7 +57,7 @@ toState = reinterpret $ \case in do modify (set (infoFunctions . at ref) (Just info)) registerDoc (f ^. signName . nameId) j - RegisterName n -> modify (over highlightNames (cons (S.AName n))) + RegisterName n -> modify (over highlightNames (cons (S.anameFromName n))) RegisterModule m -> do let j = m ^. moduleDoc modify (over infoModules (HashMap.insert (m ^. modulePath) m)) diff --git a/src/Juvix/Compiler/Concrete/Data/ScopedName.hs b/src/Juvix/Compiler/Concrete/Data/ScopedName.hs index 3b7bc12fec..7605bb62df 100644 --- a/src/Juvix/Compiler/Concrete/Data/ScopedName.hs +++ b/src/Juvix/Compiler/Concrete/Data/ScopedName.hs @@ -79,7 +79,27 @@ data Name' n = Name' } deriving stock (Show) +-- | For highlighting +data AName = AName + { _anameLoc :: Interval, + _anameDefinedLoc :: Interval, + _anameKind :: NameKind, + _anameDocId :: NameId, + _anameVerbatim :: Text + } + makeLenses ''Name' +makeLenses ''AName + +anameFromName :: HasLoc c => Name' c -> AName +anameFromName n = + AName + { _anameLoc = getLoc n, + _anameDefinedLoc = n ^. nameDefined, + _anameKind = getNameKind n, + _anameDocId = n ^. nameId, + _anameVerbatim = n ^. nameVerbatim + } instance HasNameKind (Name' n) where getNameKind = (^. nameKind) @@ -90,16 +110,11 @@ instance (HasLoc n) => HasLoc (Name' n) where instance (Pretty a) => Pretty (Name' a) where pretty = pretty . (^. nameConcrete) -data AName = forall c. - (HasLoc c) => - AName - {_aName :: Name' c} - instance HasLoc AName where - getLoc (AName c) = getLoc c + getLoc = (^. anameLoc) instance HasNameKind AName where - getNameKind (AName c) = getNameKind c + getNameKind = (^. anameKind) hasFixity :: Name' s -> Bool hasFixity n = isJust (n ^. nameFixity) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index fe1abfeffb..620763e2b0 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -230,7 +230,7 @@ instance SingI s => PrettyPrint (Iterator s) where hang (n <+?> is' <+?> rngs' <> b') instance PrettyPrint S.AName where - ppCode (S.AName n) = annotated (AnnKind (S.getNameKind n)) (noLoc (pretty (n ^. S.nameVerbatim))) + ppCode n = annotated (AnnKind (S.getNameKind n)) (noLoc (pretty (n ^. S.anameVerbatim))) instance PrettyPrint FunctionInfo where ppCode = \case @@ -406,9 +406,8 @@ instance SingI t => PrettyPrint (ModuleRef'' 'S.NotConcrete t) where instance PrettyPrint (ModuleRef'' 'S.Concrete t) where ppCode m = ppCode (m ^. moduleRefName) --- FIXME this is wrong instance PrettyPrint ScopedIden where - ppCode = ppCode . (^. scopedIden) + ppCode = ppCode . (^. scopedIdenName) instance SingI s => PrettyPrint (Import s) where ppCode :: forall r. Members '[ExactPrint, Reader Options] r => Import s -> Sem r () diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index b2e0d38af5..3f7e2a4389 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -218,7 +218,7 @@ reserveSymbolOf isAlias k nameSig s = do s' <- freshSymbol (fromSing k) s whenJust nameSig (modify' . set (scoperSignatures . at (s' ^. S.nameId)) . Just) modify (set (scopeNameSpaceLocal sns . at s) (Just s')) - registerName (S.unqualifiedSymbol s') + registerName s' let u = S.unConcrete s' entry :: NameSpaceEntryType (NameKindNameSpace nameKind) entry = @@ -1341,7 +1341,7 @@ checkLocalModule Module {..} = do mref :: ModuleRef' 'S.NotConcrete mref = mkModuleRef' @'ModuleLocal ModuleRef'' {..} modify (over scoperModules (HashMap.insert moduleId mref)) - registerName (S.unqualifiedSymbol _modulePath') + registerName _modulePath' return _moduleRefModule where inheritScope :: Sem r () @@ -1469,7 +1469,7 @@ checkOpenModuleNoImport importModuleHint OpenModule {..} ) entry <- maybe err return mentry let scopedSym = entryToSymbol entry s - registerName (S.unqualifiedSymbol scopedSym) + registerName scopedSym return scopedSym checkHidingList :: HidingList 'Parsed -> Sem r (HidingList 'Scoped) @@ -1515,7 +1515,7 @@ checkOpenModuleNoImport importModuleHint OpenModule {..} let scopedAs = do c <- i ^. usingAs return (set S.nameConcrete c scopedSym) - mapM_ (registerName . S.unqualifiedSymbol) scopedAs + mapM_ registerName scopedAs return UsingItem { _usingSymbol = scopedSym, @@ -1845,26 +1845,6 @@ checkLambdaClause LambdaClause {..} = withLocalScope $ do _lambdaAssignKw } -scopedVar :: - Members '[InfoTableBuilder] r => - S.Symbol -> - Symbol -> - Sem r S.Symbol -scopedVar s n = do - let scoped = set S.nameConcrete n s - registerName (S.unqualifiedSymbol scoped) - return scoped - -scopedFunction :: - (Members '[InfoTableBuilder] r) => - RefNameType 'S.NotConcrete -> - Symbol -> - Sem r S.Name -scopedFunction fref n = do - let scoped :: S.Name = set S.nameConcrete (NameUnqualified n) fref - registerName scoped - return scoped - checkUnqualifiedName :: (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r) => Symbol -> From da976b0e307ae2dcc00e23152eba3f78bd50e5f4 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 15:09:02 +0200 Subject: [PATCH 09/18] register scoped iden --- src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs | 12 ++++++++++++ src/Juvix/Compiler/Concrete/Language.hs | 2 +- .../Translation/FromParsed/Analysis/Scoping.hs | 2 +- 3 files changed, 14 insertions(+), 2 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs index ced01531bc..6e846280fd 100644 --- a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs @@ -16,6 +16,7 @@ data InfoTableBuilder m a where RegisterInductive :: InductiveDef 'Scoped -> InfoTableBuilder m () RegisterFunctionDef :: FunctionDef 'Scoped -> InfoTableBuilder m () RegisterName :: HasLoc c => S.Name' c -> InfoTableBuilder m () + RegisterScopedIden :: ScopedIden -> InfoTableBuilder m () RegisterModule :: Module 'Scoped 'ModuleTop -> InfoTableBuilder m () RegisterFixity :: FixityDef -> InfoTableBuilder m () RegisterPrecedence :: S.NameId -> S.NameId -> InfoTableBuilder m () @@ -58,6 +59,7 @@ toState = reinterpret $ \case modify (set (infoFunctions . at ref) (Just info)) registerDoc (f ^. signName . nameId) j RegisterName n -> modify (over highlightNames (cons (S.anameFromName n))) + RegisterScopedIden n -> modify (over highlightNames (cons (anameFromScopedIden n))) RegisterModule m -> do let j = m ^. moduleDoc modify (over infoModules (HashMap.insert (m ^. modulePath) m)) @@ -84,3 +86,13 @@ runInfoTableBuilder tab = runState tab . toState ignoreInfoTableBuilder :: Members '[HighlightBuilder] r => Sem (InfoTableBuilder ': r) a -> Sem r a ignoreInfoTableBuilder = evalState emptyInfoTable . toState + +anameFromScopedIden :: ScopedIden -> AName +anameFromScopedIden s = + AName + { _anameLoc = getLoc s, + _anameKind = getNameKind s, + _anameDocId = s ^. scopedIden . nameId, + _anameDefinedLoc = s ^. scopedIdenName . nameDefined, + _anameVerbatim = s ^. scopedIdenName . nameVerbatim + } diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index c3e37018e7..e935b783c8 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -1753,7 +1753,7 @@ instance Pretty ScopedIden where pretty = pretty . (^. scopedIdenName) instance HasLoc ScopedIden where - getLoc = getLoc . (^. scopedIden) + getLoc = getLoc . (^. scopedIdenName) instance SingI s => HasLoc (InductiveParameters s) where getLoc i = getLocSymbolType (i ^. inductiveParametersNames . _head1) <>? (getLocExpressionType <$> (i ^? inductiveParametersRhs . _Just . inductiveParametersType)) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 3f7e2a4389..c763dba4e6 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -563,7 +563,7 @@ entryToScopedIden name e = do { _scopedIdenAlias = Just (set S.nameKind (getNameKind e') scopedName), _scopedIden = helper (e' ^. symbolEntry) } - registerName (si ^. scopedIdenName) + registerScopedIden si return si -- | We gather all symbols which have been defined or marked to be public in the given scope. From cb9222adda0a5c7e84b866cff07419b8edfaaac6 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 16:22:07 +0200 Subject: [PATCH 10/18] let wip --- src/Juvix/Compiler/Concrete/Language.hs | 18 +++++++++++++++++- test/Typecheck/Positive.hs | 6 +++++- tests/positive/Alias.juvix | 2 ++ 3 files changed, 24 insertions(+), 2 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index e935b783c8..e3c3d4e5c5 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -1199,10 +1199,26 @@ data PostfixApplication = PostfixApplication } deriving stock (Show, Eq, Ord) +data LetStatement (s :: Stage) = + LetFunctionDef (FunctionDef s) + | LetAlias (AliasDef s) + +deriving stock instance Show (LetStatement 'Parsed) + +deriving stock instance Show (LetStatement 'Scoped) + +deriving stock instance Eq (LetStatement 'Parsed) + +deriving stock instance Eq (LetStatement 'Scoped) + +deriving stock instance Ord (LetStatement 'Parsed) + +deriving stock instance Ord (LetStatement 'Scoped) + data Let (s :: Stage) = Let { _letKw :: KeywordRef, _letInKw :: Irrelevant KeywordRef, - _letFunDefs :: NonEmpty (FunctionDef s), + _letFunDefs :: NonEmpty (LetStatement s), _letExpression :: ExpressionType s } diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs index 4c6e2a0475..1a04dcd439 100644 --- a/test/Typecheck/Positive.hs +++ b/test/Typecheck/Positive.hs @@ -276,7 +276,11 @@ tests = posTest "Issue 2296 (Pi types with lhs arity other than unit)" $(mkRelDir "issue2296") - $(mkRelFile "M.juvix") + $(mkRelFile "M.juvix"), + posTest + "Alias" + $(mkRelDir ".") + $(mkRelFile "Alias.juvix") ] <> [ compilationTest t | t <- Compilation.tests ] diff --git a/tests/positive/Alias.juvix b/tests/positive/Alias.juvix index 7d0702e1a7..d18148f393 100644 --- a/tests/positive/Alias.juvix +++ b/tests/positive/Alias.juvix @@ -1,9 +1,11 @@ module Alias; +-- aliases are allowed to forward reference syntax alias Boolean := Bool; syntax alias ⊥ := false; syntax alias ⊤ := true; +--- Truth value type Bool := | false | true; From 34b7fec129e05aab161ef0a481374a165c2de731 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 17:19:39 +0200 Subject: [PATCH 11/18] alias in let --- src/Juvix/Compiler/Concrete/Language.hs | 6 ++-- src/Juvix/Compiler/Concrete/Print/Base.hs | 5 +++ .../FromParsed/Analysis/Scoping.hs | 34 +++++++++++++------ .../Concrete/Translation/FromSource.hs | 7 +++- .../Internal/Translation/FromConcrete.hs | 29 ++++++++-------- 5 files changed, 52 insertions(+), 29 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index e3c3d4e5c5..5b1c9086e1 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -1199,9 +1199,9 @@ data PostfixApplication = PostfixApplication } deriving stock (Show, Eq, Ord) -data LetStatement (s :: Stage) = - LetFunctionDef (FunctionDef s) - | LetAlias (AliasDef s) +data LetStatement (s :: Stage) + = LetFunctionDef (FunctionDef s) + | LetAliasDef (AliasDef s) deriving stock instance Show (LetStatement 'Parsed) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 620763e2b0..11efb45e0b 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -451,6 +451,11 @@ instance SingI s => PrettyPrint (LambdaClause s) where lambdaPipe' = ppCode <$> _lambdaPipe ^. unIrrelevant lambdaPipe' lambdaParameters' <+> ppCode _lambdaAssignKw <> oneLineOrNext lambdaBody' +instance SingI s => PrettyPrint (LetStatement s) where + ppCode = \case + LetFunctionDef f -> ppCode f + LetAliasDef f -> ppCode f + instance SingI s => PrettyPrint (Let s) where ppCode Let {..} = do let letFunDefs' = blockIndent (ppBlock _letFunDefs) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index c763dba4e6..c9362f3d63 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1257,8 +1257,13 @@ checkSections sec = do _ -> fail _ -> fail -mkLetSections :: [FunctionDef 'Parsed] -> StatementSections 'Parsed -mkLetSections = mkSections . map StatementFunctionDef +mkLetSections :: [LetStatement 'Parsed] -> StatementSections 'Parsed +mkLetSections = mkSections . map toTopStatement + where + toTopStatement :: LetStatement 'Parsed -> Statement 'Parsed + toTopStatement = \case + LetFunctionDef f -> StatementFunctionDef f + LetAliasDef f -> StatementSyntax (SyntaxAlias f) mkSections :: [Statement 'Parsed] -> StatementSections 'Parsed mkSections = \case @@ -1645,8 +1650,8 @@ checkFunction f = do -- | for now functions defined in let clauses cannot be infix operators checkLetFunDefs :: Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => - NonEmpty (FunctionDef 'Parsed) -> - Sem r (NonEmpty (FunctionDef 'Scoped)) + NonEmpty (LetStatement 'Parsed) -> + Sem r (NonEmpty (LetStatement 'Scoped)) checkLetFunDefs = localBindings . ignoreSyntax @@ -1655,28 +1660,35 @@ checkLetFunDefs = . mkLetSections . toList where - fromSections :: StatementSections s -> NonEmpty (FunctionDef s) + fromSections :: StatementSections s -> NonEmpty (LetStatement s) fromSections = \case SectionsEmpty -> impossible SectionsDefinitions d -> fromDefs d SectionsNonDefinitions d -> fromNonDefs d where - fromDefs :: DefinitionsSection s -> NonEmpty (FunctionDef s) + fromDefs :: DefinitionsSection s -> NonEmpty (LetStatement s) fromDefs DefinitionsSection {..} = (fromDef <$> _definitionsSection) <>? (fromNonDefs <$> _definitionsNext) where - fromDef :: Definition s -> FunctionDef s + fromSyn :: SyntaxDef s -> LetStatement s + fromSyn = \case + SyntaxAlias a -> LetAliasDef a + SyntaxFixity {} -> impossible + SyntaxOperator {} -> impossible + SyntaxIterator {} -> impossible + + fromDef :: Definition s -> LetStatement s fromDef = \case - DefinitionFunctionDef d -> d + DefinitionFunctionDef d -> LetFunctionDef d + DefinitionSyntax syn -> fromSyn syn DefinitionInductive {} -> impossible DefinitionProjectionDef {} -> impossible DefinitionAxiom {} -> impossible - DefinitionSyntax {} -> impossible - fromNonDefs :: NonDefinitionsSection s -> NonEmpty (FunctionDef s) + fromNonDefs :: NonDefinitionsSection s -> NonEmpty (LetStatement s) fromNonDefs NonDefinitionsSection {..} = (fromNonDef <$> _nonDefinitionsSection) <>? (fromDefs <$> _nonDefinitionsNext) where - fromNonDef :: NonDefinition s -> FunctionDef s + fromNonDef :: NonDefinition s -> LetStatement s fromNonDef = \case NonDefinitionImport {} -> impossible NonDefinitionModule {} -> impossible diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 53aba4d005..adf9237574 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -836,10 +836,15 @@ letFunDef = do optional_ stashPragmas functionDefinition Nothing +letStatement :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (LetStatement 'Parsed) +letStatement = + LetFunctionDef <$> functionDefinition Nothing + <|> LetAliasDef <$> (kw kwSyntax >>= aliasDef) + letBlock :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Let 'Parsed) letBlock = do _letKw <- kw kwLet - _letFunDefs <- P.sepEndBy1 letFunDef semicolon + _letFunDefs <- P.sepEndBy1 letStatement semicolon _letInKw <- Irrelevant <$> kw kwIn _letExpression <- parseExpressionAtoms return Let {..} diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 23c74b57e1..6aa479fdd4 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -404,12 +404,6 @@ goOpenModule :: Sem r (Maybe Internal.Import) goOpenModule o = goOpenModule' o -goLetFunctionDef :: - Members '[Builtins, NameIdGen, Reader Pragmas, Error ScoperError] r => - FunctionDef 'Scoped -> - Sem r Internal.FunctionDef -goLetFunctionDef = goTopFunctionDef - goProjectionDef :: forall r. Members '[NameIdGen, State ConstructorInfos] r => @@ -745,7 +739,7 @@ goExpression = \case ExpressionLiteral l -> return (Internal.ExpressionLiteral (goLiteral l)) ExpressionLambda l -> Internal.ExpressionLambda <$> goLambda l ExpressionBraces b -> throw (ErrAppLeftImplicit (AppLeftImplicit b)) - ExpressionLet l -> Internal.ExpressionLet <$> goLet l + ExpressionLet l -> goLet l ExpressionList l -> goList l ExpressionUniverse uni -> return (Internal.ExpressionUniverse (goUniverse uni)) ExpressionFunction func -> Internal.ExpressionFunction <$> goFunction func @@ -845,19 +839,26 @@ goExpression = \case where n' = goScopedIden x - goLet :: Let 'Scoped -> Sem r Internal.Let + goLet :: Let 'Scoped -> Sem r Internal.Expression goLet l = do _letExpression <- goExpression (l ^. letExpression) - _letClauses <- goLetFunDefs (l ^. letFunDefs) - return Internal.Let {..} + clauses <- goLetFunDefs (l ^. letFunDefs) + return $ case nonEmpty clauses of + Just _letClauses -> Internal.ExpressionLet Internal.Let {..} + Nothing -> _letExpression where - goLetFunDefs :: NonEmpty (FunctionDef 'Scoped) -> Sem r (NonEmpty Internal.LetClause) + goLetFunDefs :: NonEmpty (LetStatement 'Scoped) -> Sem r [Internal.LetClause] goLetFunDefs cl = fmap goSCC <$> preLetStatements cl - preLetStatements :: NonEmpty (FunctionDef 'Scoped) -> Sem r (NonEmpty (SCC Internal.PreLetStatement)) + preLetStatements :: NonEmpty (LetStatement 'Scoped) -> Sem r [SCC Internal.PreLetStatement] preLetStatements cl = do - pre <- mapM (fmap Internal.PreLetFunctionDef . goLetFunctionDef) cl - return (buildLetMutualBlocks pre) + pre <- mapMaybeM preLetStatement (toList cl) + return $ maybe [] (toList . buildLetMutualBlocks) (nonEmpty pre) + where + preLetStatement :: LetStatement 'Scoped -> Sem r (Maybe Internal.PreLetStatement) + preLetStatement = \case + LetFunctionDef f -> Just . Internal.PreLetFunctionDef <$> goTopFunctionDef f + LetAliasDef {} -> return Nothing goSCC :: SCC Internal.PreLetStatement -> Internal.LetClause goSCC = \case From 9142c7f5e098dc883048090cf57851c6dcc333bf Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 17:31:20 +0200 Subject: [PATCH 12/18] extend example --- tests/positive/Alias.juvix | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/tests/positive/Alias.juvix b/tests/positive/Alias.juvix index d18148f393..4c7e4903f2 100644 --- a/tests/positive/Alias.juvix +++ b/tests/positive/Alias.juvix @@ -1,5 +1,7 @@ module Alias; +import Stdlib.Data.Fixity open; + -- aliases are allowed to forward reference syntax alias Boolean := Bool; syntax alias ⊥ := false; @@ -13,3 +15,28 @@ type Bool := not : Boolean -> Boolean | ⊥ := ⊤ | ⊤ := ⊥; + +not2 (b : Boolean) : Boolean := + let + syntax alias yes := ⊤; + syntax alias no := ⊥; + in case b + | no := yes + | yes := no; + +module ExportAlias; + syntax alias Binary := Bool; + syntax alias one := ⊤; + syntax alias zero := ⊥; +end; + +open ExportAlias; + +syntax operator || logical; +|| : Binary -> Binary -> Binary + | zero b := b + | one _ := one; + +syntax alias or := ||; + +or3 (a b c : Binary) : Binary := or (or a b) c; From eb20dfd6ee37f429be5392043c1d055bf1da5656 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 17:57:45 +0200 Subject: [PATCH 13/18] fixities --- .../Translation/FromParsed/Analysis/Scoping.hs | 16 ++++++++-------- tests/positive/Alias.juvix | 8 ++++++++ 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index c9362f3d63..088a4af872 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -285,12 +285,12 @@ reserveInductiveSymbol :: Sem r S.Symbol reserveInductiveSymbol d = reserveSymbolSignatureOf SKNameInductive d (d ^. inductiveName) --- | The NameKind assigned to the alias is irrelevant. +-- | The NameKind assigned to the alias is irrelevant. We assign it KNameFunction so it can have fixity. reserveAliasSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, State ScoperState] r => Symbol -> Sem r S.Symbol -reserveAliasSymbol = reserveSymbolOf True SKNameLocal Nothing +reserveAliasSymbol = reserveSymbolOf True SKNameFunction Nothing reserveProjectionSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, State ScoperState] r => @@ -1701,7 +1701,7 @@ checkRecordPattern :: Sem r (RecordPattern 'Scoped) checkRecordPattern r = do c' <- getNameOfKind KNameConstructor (r ^. recordPatternConstructor) - fields <- fromMaybeM (return (RecordNameSignature mempty)) (gets (^. scoperConstructorFields . at (c' ^. scopedIden . S.nameId))) + fields <- fromMaybeM (return (RecordNameSignature mempty)) (gets (^. scoperConstructorFields . at (c' ^. scopedIdenName . S.nameId))) l' <- if | null (r ^. recordPatternItems) -> return [] @@ -2128,7 +2128,7 @@ checkIterator :: Sem r (Iterator 'Scoped) checkIterator iter = do _iteratorName <- checkScopedIden (iter ^. iteratorName) - case _iteratorName ^. scopedIden . S.nameIterator of + case _iteratorName ^. scopedIdenName . S.nameIterator of Just IteratorAttribs {..} -> do case _iteratorAttribsInitNum of Just n @@ -2211,7 +2211,7 @@ checkParens e@(ExpressionAtoms as _) = case as of p :| [] -> case p of AtomIdentifier s -> do scopedId <- checkScopedIden s - let scopedIdenNoFix = over scopedIden (set S.nameFixity Nothing) scopedId + let scopedIdenNoFix = over scopedIdenName (set S.nameFixity Nothing) scopedId return (ExpressionParensIdentifier scopedIdenNoFix) AtomIterator i -> ExpressionIterator . set iteratorParens True <$> checkIterator i AtomCase c -> ExpressionCase . set caseParens True <$> checkCase c @@ -2405,7 +2405,7 @@ makeExpressionTable (ExpressionAtoms atoms _) = [recordUpdate] : [appOpExplicit] AssocNone -> P.InfixN | otherwise = Nothing where - S.Name' {..} = iden ^. scopedIden + S.Name' {..} = iden ^. scopedIdenName parseSymbolId :: S.NameId -> Parse ScopedIden parseSymbolId uid = P.token getIdentifierWithId mempty @@ -2413,7 +2413,7 @@ makeExpressionTable (ExpressionAtoms atoms _) = [recordUpdate] : [appOpExplicit] getIdentifierWithId :: ExpressionAtom 'Scoped -> Maybe ScopedIden getIdentifierWithId s = case s of AtomIdentifier iden - | uid == iden ^. scopedIden . S.nameId -> Just iden + | uid == iden ^. scopedIdenName . S.nameId -> Just iden _ -> Nothing recordUpdate :: P.Operator Parse Expression @@ -2600,7 +2600,7 @@ parseTerm = identifierNoFixity :: ExpressionAtom 'Scoped -> Maybe ScopedIden identifierNoFixity s = case s of AtomIdentifier iden - | not (S.hasFixity (iden ^. scopedIden)) -> Just iden + | not (S.hasFixity (iden ^. scopedIdenName)) -> Just iden _ -> Nothing parseBraces :: Parse Expression diff --git a/tests/positive/Alias.juvix b/tests/positive/Alias.juvix index 4c7e4903f2..c4207b6398 100644 --- a/tests/positive/Alias.juvix +++ b/tests/positive/Alias.juvix @@ -40,3 +40,11 @@ syntax operator || logical; syntax alias or := ||; or3 (a b c : Binary) : Binary := or (or a b) c; + +type Pair := + | mkPair Binary Binary; + +syntax operator , pair; +syntax alias , := mkPair; + +myPair : Pair := one , ⊥; From 498f7c308b3126575f78a06b1a82fa178df243da Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 18:18:42 +0200 Subject: [PATCH 14/18] scopedIdenFinal --- app/Commands/Repl.hs | 4 ++-- .../Compiler/Concrete/Data/InfoTableBuilder.hs | 2 +- src/Juvix/Compiler/Concrete/Extra.hs | 2 +- src/Juvix/Compiler/Concrete/Language.hs | 18 ++++++------------ .../Translation/FromParsed/Analysis/Scoping.hs | 14 +++++++------- .../Internal/Translation/FromConcrete.hs | 2 +- tests/positive/Alias.juvix | 5 +++++ 7 files changed, 23 insertions(+), 24 deletions(-) diff --git a/app/Commands/Repl.hs b/app/Commands/Repl.hs index aa3ed22c73..412de596f5 100644 --- a/app/Commands/Repl.hs +++ b/app/Commands/Repl.hs @@ -277,7 +277,7 @@ printDocumentation = replParseIdentifiers >=> printIdentifiers printIdentifier :: Concrete.ScopedIden -> Repl () printIdentifier s = do - let n = s ^. Concrete.scopedIden . Scoped.nameId + let n = s ^. Concrete.scopedIdenFinal . Scoped.nameId mdoc <- case getNameKind s of KNameAxiom -> getDocAxiom n KNameInductive -> getDocInductive n @@ -334,7 +334,7 @@ printDefinition = replParseIdentifiers >=> printIdentifiers printIdentifier :: Concrete.ScopedIden -> Repl () printIdentifier s = - let n = s ^. Concrete.scopedIden . Scoped.nameId + let n = s ^. Concrete.scopedIdenFinal . Scoped.nameId in case getNameKind s of KNameAxiom -> printAxiom n KNameInductive -> printInductive n diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs index 6e846280fd..c754f2cc37 100644 --- a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs @@ -92,7 +92,7 @@ anameFromScopedIden s = AName { _anameLoc = getLoc s, _anameKind = getNameKind s, - _anameDocId = s ^. scopedIden . nameId, + _anameDocId = s ^. scopedIdenFinal . nameId, _anameDefinedLoc = s ^. scopedIdenName . nameDefined, _anameVerbatim = s ^. scopedIdenName . nameVerbatim } diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs index 9103a0752d..ecbffa5c66 100644 --- a/src/Juvix/Compiler/Concrete/Extra.hs +++ b/src/Juvix/Compiler/Concrete/Extra.hs @@ -141,7 +141,7 @@ recordNameSignatureByIndex = IntMap.fromList . (^.. recordNames . each . to swap getExpressionAtomIden :: ExpressionAtom 'Scoped -> Maybe S.Name getExpressionAtomIden = \case - AtomIdentifier nm -> Just (nm ^. scopedIden) + AtomIdentifier nm -> Just (nm ^. scopedIdenName) _ -> Nothing getPatternAtomIden :: PatternAtom 'Scoped -> Maybe S.Name diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 5b1c9086e1..8661c832e5 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -1059,7 +1059,7 @@ deriving stock instance Ord (OpenModule 'Parsed) deriving stock instance Ord (OpenModule 'Scoped) data ScopedIden = ScopedIden - { _scopedIden :: S.Name, + { _scopedIdenFinal :: S.Name, _scopedIdenAlias :: Maybe S.Name } deriving stock (Show, Eq, Ord) @@ -2176,7 +2176,7 @@ instance IsApe InfixApplication ApeLeaf where { _infixFixity = getFixity i, _infixLeft = toApe l, _infixRight = toApe r, - _infixIsDelimiter = isDelimiterStr (prettyText (op ^. scopedIden . S.nameConcrete)), + _infixIsDelimiter = isDelimiterStr (prettyText (op ^. scopedIdenName . S.nameConcrete)), _infixOp = ApeLeafExpression (ExpressionIdentifier op) } @@ -2296,7 +2296,7 @@ symbolEntryNameId :: SymbolEntry -> NameId symbolEntryNameId = (^. symbolEntry . S.nameId) instance HasNameKind ScopedIden where - getNameKind = getNameKind . (^. scopedIden) + getNameKind = getNameKind . (^. scopedIdenFinal) instance HasNameKind SymbolEntry where getNameKind = getNameKind . (^. symbolEntry) @@ -2336,22 +2336,16 @@ _SyntaxAlias f x = case x of scopedIdenName :: Lens' ScopedIden S.Name scopedIdenName f n = case n ^. scopedIdenAlias of - Nothing -> scopedIden f n + Nothing -> scopedIdenFinal f n Just a -> do a' <- f a pure (set scopedIdenAlias (Just a') n) -scopedIdenFixity :: ScopedIden -> Maybe Fixity -scopedIdenFixity s = fromMaybe (s ^. scopedIden . S.nameFixity) (s ^? scopedIdenAlias . _Just . S.nameFixity) - -scopedIdenNameId :: ScopedIden -> NameId -scopedIdenNameId s = fromMaybe (s ^. scopedIden . S.nameId) (s ^? scopedIdenAlias . _Just . S.nameId) - instance HasFixity PostfixApplication where - getFixity (PostfixApplication _ op) = fromMaybe impossible (op ^. scopedIden . S.nameFixity) + getFixity (PostfixApplication _ op) = fromMaybe impossible (op ^. scopedIdenName . S.nameFixity) instance HasFixity InfixApplication where - getFixity (InfixApplication _ op _) = fromMaybe impossible (op ^. scopedIden . S.nameFixity) + getFixity (InfixApplication _ op _) = fromMaybe impossible (op ^. scopedIdenName . S.nameFixity) preSymbolName :: Lens' PreSymbolEntry (S.Name' ()) preSymbolName f = \case diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 088a4af872..c88645ea76 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -553,7 +553,7 @@ entryToScopedIden name e = do PreSymbolFinal {} -> return ScopedIden - { _scopedIden = scopedName, + { _scopedIdenFinal = scopedName, _scopedIdenAlias = Nothing } PreSymbolAlias {} -> do @@ -561,7 +561,7 @@ entryToScopedIden name e = do return ScopedIden { _scopedIdenAlias = Just (set S.nameKind (getNameKind e') scopedName), - _scopedIden = helper (e' ^. symbolEntry) + _scopedIdenFinal = helper (e' ^. symbolEntry) } registerScopedIden si return si @@ -2106,14 +2106,14 @@ getRecordInfo :: ScopedIden -> Sem r RecordInfo getRecordInfo indTy = - fromMaybeM err (gets (^. scoperRecordFields . at (indTy ^. scopedIden . S.nameId))) + fromMaybeM err (gets (^. scoperRecordFields . at (indTy ^. scopedIdenFinal . S.nameId))) where err :: Sem r a err = throw (ErrNotARecord (NotARecord indTy)) getNameSignature :: Members '[State ScoperState, Error ScoperError] r => ScopedIden -> Sem r NameSignature getNameSignature s = do - sig <- maybeM (throw err) return (lookupNameSignature (s ^. scopedIden . S.nameId)) + sig <- maybeM (throw err) return (lookupNameSignature (s ^. scopedIdenFinal . S.nameId)) when (null (sig ^. nameSignatureArgs)) (throw err) return sig where @@ -2641,8 +2641,8 @@ makePatternTable (PatternAtoms latoms _) = [appOp] : operators where unqualifiedSymbolOp :: ScopedIden -> Maybe (Precedence, P.Operator ParsePat PatternArg) unqualifiedSymbolOp constr = run . runFail $ do - Fixity {..} <- failMaybe (scopedIdenFixity constr) - let _nameId = scopedIdenNameId constr + Fixity {..} <- failMaybe (constr ^. scopedIdenName . S.nameFixity) + let _nameId = constr ^. scopedIdenName . S.nameId return $ case _fixityArity of Unary u -> (_fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId)) where @@ -2664,7 +2664,7 @@ makePatternTable (PatternAtoms latoms _) = [appOp] : operators getConstructorRefWithId :: PatternAtom 'Scoped -> Maybe ScopedIden getConstructorRefWithId s = do ref <- getConstructorRef s - guard (scopedIdenNameId ref == uid) + guard (ref ^. scopedIdenName . S.nameId == uid) return ref -- Application by juxtaposition. diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 6aa479fdd4..3a5a870974 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -187,7 +187,7 @@ goScopedIden iden = set Internal.namePretty prettyStr (goSymbol (S.nameUnqualify name)) where name :: S.Name - name = iden ^. scopedIden + name = iden ^. scopedIdenFinal prettyStr :: Text prettyStr = prettyText name diff --git a/tests/positive/Alias.juvix b/tests/positive/Alias.juvix index c4207b6398..307aebf9bb 100644 --- a/tests/positive/Alias.juvix +++ b/tests/positive/Alias.juvix @@ -48,3 +48,8 @@ syntax operator , pair; syntax alias , := mkPair; myPair : Pair := one , ⊥; + +localAlias : Binary -> Binary + | b := let + syntax alias b' := b + in b'; From bf585168a3f9e6382ca5839048a37be23f0f2c46 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 18:31:53 +0200 Subject: [PATCH 15/18] add alias name kind --- app/Commands/Repl.hs | 2 ++ .../Concrete/Data/Highlight/RenderEmacs.hs | 1 + src/Juvix/Compiler/Concrete/Data/NameSpace.hs | 1 + .../FromParsed/Analysis/Scoping.hs | 20 ++++++++++--------- src/Juvix/Compiler/Internal/Extra.hs | 1 + .../Internal/Translation/FromConcrete.hs | 1 + src/Juvix/Data/NameKind.hs | 14 +++++++------ tests/positive/Alias.juvix | 9 +++++---- 8 files changed, 30 insertions(+), 19 deletions(-) diff --git a/app/Commands/Repl.hs b/app/Commands/Repl.hs index 412de596f5..a4a04c8158 100644 --- a/app/Commands/Repl.hs +++ b/app/Commands/Repl.hs @@ -286,6 +286,7 @@ printDocumentation = replParseIdentifiers >=> printIdentifiers KNameConstructor -> getDocConstructor n KNameLocalModule -> impossible KNameTopModule -> impossible + KNameAlias -> impossible KNameFixity -> impossible printDoc mdoc where @@ -344,6 +345,7 @@ printDefinition = replParseIdentifiers >=> printIdentifiers KNameLocalModule -> impossible KNameTopModule -> impossible KNameFixity -> impossible + KNameAlias -> impossible where printLocation :: HasLoc s => s -> Repl () printLocation def = do diff --git a/src/Juvix/Compiler/Concrete/Data/Highlight/RenderEmacs.hs b/src/Juvix/Compiler/Concrete/Data/Highlight/RenderEmacs.hs index 34abc5c7db..2387176b7a 100644 --- a/src/Juvix/Compiler/Concrete/Data/Highlight/RenderEmacs.hs +++ b/src/Juvix/Compiler/Concrete/Data/Highlight/RenderEmacs.hs @@ -16,6 +16,7 @@ nameKindFace = \case KNameLocalModule -> Just FaceModule KNameAxiom -> Just FaceAxiom KNameLocal -> Nothing + KNameAlias -> Nothing KNameFixity -> Nothing fromCodeAnn :: CodeAnn -> Maybe EmacsProperty diff --git a/src/Juvix/Compiler/Concrete/Data/NameSpace.hs b/src/Juvix/Compiler/Concrete/Data/NameSpace.hs index 8142571e66..d2d1dfcf52 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSpace.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSpace.hs @@ -20,6 +20,7 @@ $(genSingletons [''NameSpace]) type NameKindNameSpace :: NameKind -> NameSpace type family NameKindNameSpace s = res where NameKindNameSpace 'KNameLocal = 'NameSpaceSymbols + NameKindNameSpace 'KNameAlias = 'NameSpaceSymbols NameKindNameSpace 'KNameConstructor = 'NameSpaceSymbols NameKindNameSpace 'KNameInductive = 'NameSpaceSymbols NameKindNameSpace 'KNameFunction = 'NameSpaceSymbols diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index c88645ea76..0f3af4605f 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -198,7 +198,7 @@ reserveSymbolSignatureOf :: Sem r S.Symbol reserveSymbolSignatureOf k d s = do sig <- mkNameSignature d - reserveSymbolOf False k (Just sig) s + reserveSymbolOf k (Just sig) s reserveSymbolOf :: forall (nameKind :: NameKind) (ns :: NameSpace) r. @@ -206,12 +206,11 @@ reserveSymbolOf :: ns ~ NameKindNameSpace nameKind, SingI ns ) => - Bool -> Sing nameKind -> Maybe NameSignature -> Symbol -> Sem r S.Symbol -reserveSymbolOf isAlias k nameSig s = do +reserveSymbolOf k nameSig s = do checkNotBound path <- gets (^. scopePath) strat <- ask @@ -229,6 +228,7 @@ reserveSymbolOf isAlias k nameSig s = do fixE = FixitySymbolEntry u in case k of SKNameConstructor -> symE + SKNameAlias -> symE SKNameInductive -> symE SKNameFunction -> symE SKNameAxiom -> symE @@ -245,6 +245,9 @@ reserveSymbolOf isAlias k nameSig s = do modify (over scopeNameSpace (HashMap.alter (Just . addS entry) s)) return s' where + isAlias = case k of + SKNameAlias -> True + _ -> False sns :: Sing ns = sing checkNotBound :: Sem r () checkNotBound = do @@ -277,7 +280,7 @@ bindVariableSymbol :: Members '[Error ScoperError, NameIdGen, State Scope, InfoTableBuilder, State ScoperState] r => Symbol -> Sem r S.Symbol -bindVariableSymbol = localBindings . ignoreSyntax . reserveSymbolOf False SKNameLocal Nothing +bindVariableSymbol = localBindings . ignoreSyntax . reserveSymbolOf SKNameLocal Nothing reserveInductiveSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r => @@ -285,18 +288,17 @@ reserveInductiveSymbol :: Sem r S.Symbol reserveInductiveSymbol d = reserveSymbolSignatureOf SKNameInductive d (d ^. inductiveName) --- | The NameKind assigned to the alias is irrelevant. We assign it KNameFunction so it can have fixity. reserveAliasSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, State ScoperState] r => Symbol -> Sem r S.Symbol -reserveAliasSymbol = reserveSymbolOf True SKNameFunction Nothing +reserveAliasSymbol = reserveSymbolOf SKNameAlias Nothing reserveProjectionSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, State ScoperState] r => ProjectionDef 'Parsed -> Sem r S.Symbol -reserveProjectionSymbol d = reserveSymbolOf False SKNameFunction Nothing (d ^. projectionField) +reserveProjectionSymbol d = reserveSymbolOf SKNameFunction Nothing (d ^. projectionField) reserveConstructorSymbol :: Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r => @@ -643,7 +645,7 @@ resolveFixitySyntaxDef :: FixitySyntaxDef 'Parsed -> Sem r () resolveFixitySyntaxDef fdef@FixitySyntaxDef {..} = topBindings $ do - sym <- reserveSymbolOf False SKNameFixity Nothing _fixitySymbol + sym <- reserveSymbolOf SKNameFixity Nothing _fixitySymbol let loc = getLoc _fixityInfo fi = _fixityInfo ^. withLocParam . withSourceValue same <- checkMaybeFixity loc $ fi ^. FI.fixityPrecSame @@ -1316,7 +1318,7 @@ reserveLocalModuleSymbol :: Symbol -> Sem r S.Symbol reserveLocalModuleSymbol = - ignoreSyntax . reserveSymbolOf False SKNameLocalModule Nothing + ignoreSyntax . reserveSymbolOf SKNameLocalModule Nothing checkLocalModule :: forall r. diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index 020de1b830..763911d682 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -457,6 +457,7 @@ instance IsExpression Name where KNameLocalModule -> impossible KNameTopModule -> impossible KNameFixity -> impossible + KNameAlias -> impossible instance IsExpression SmallUniverse where toExpression = ExpressionUniverse diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 3a5a870974..046f66fd20 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -834,6 +834,7 @@ goExpression = \case KNameFunction -> Internal.IdenFunction n' KNameConstructor -> Internal.IdenConstructor n' KNameLocalModule -> impossible + KNameAlias -> impossible KNameTopModule -> impossible KNameFixity -> impossible where diff --git a/src/Juvix/Data/NameKind.hs b/src/Juvix/Data/NameKind.hs index b90eef0c71..9274c075ff 100644 --- a/src/Juvix/Data/NameKind.hs +++ b/src/Juvix/Data/NameKind.hs @@ -19,8 +19,10 @@ data NameKind KNameLocalModule | -- | A top module name. KNameTopModule - | -- | A fixity name + | -- | A fixity name. KNameFixity + | -- | An alias name. Only used in the declaration site. + KNameAlias deriving stock (Show, Eq, Data) $(genSingletons [''NameKind]) @@ -50,6 +52,7 @@ nameKindText = \case KNameLocalModule -> "local module" KNameTopModule -> "module" KNameFixity -> "fixity" + KNameAlias -> "alias" isExprKind :: HasNameKind a => a -> Bool isExprKind k = case getNameKind k of @@ -73,6 +76,7 @@ canBeCompiled k = case getNameKind k of KNameLocalModule -> False KNameTopModule -> False KNameFixity -> False + KNameAlias -> False canHaveFixity :: HasNameKind a => a -> Bool canHaveFixity k = case getNameKind k of @@ -80,6 +84,7 @@ canHaveFixity k = case getNameKind k of KNameInductive -> True KNameFunction -> True KNameAxiom -> True + KNameAlias -> True KNameLocal -> False KNameLocalModule -> False KNameTopModule -> False @@ -90,6 +95,7 @@ canBeIterator k = case getNameKind k of KNameFunction -> True KNameAxiom -> True KNameConstructor -> False + KNameAlias -> False KNameInductive -> False KNameLocal -> False KNameLocalModule -> False @@ -104,10 +110,6 @@ nameKindAnsi k = case k of KNameLocalModule -> color Cyan KNameFunction -> colorDull Yellow KNameLocal -> mempty + KNameAlias -> mempty KNameTopModule -> color Cyan KNameFixity -> mempty - -isFunctionKind :: HasNameKind a => a -> Bool -isFunctionKind k = case getNameKind k of - KNameFunction -> True - _ -> False diff --git a/tests/positive/Alias.juvix b/tests/positive/Alias.juvix index 307aebf9bb..59bb5af871 100644 --- a/tests/positive/Alias.juvix +++ b/tests/positive/Alias.juvix @@ -47,9 +47,10 @@ type Pair := syntax operator , pair; syntax alias , := mkPair; -myPair : Pair := one , ⊥; +myPair : Pair := one, ⊥; localAlias : Binary -> Binary - | b := let - syntax alias b' := b - in b'; + | b := + let + syntax alias b' := b; + in b'; From a43a5ffa470231fcddca91a5284a9913cc9c837b Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 18:34:50 +0200 Subject: [PATCH 16/18] ormolu --- .../Concrete/Translation/FromParsed/Analysis/Scoping.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 0f3af4605f..2d6e2ba5ae 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -245,7 +245,7 @@ reserveSymbolOf k nameSig s = do modify (over scopeNameSpace (HashMap.alter (Just . addS entry) s)) return s' where - isAlias = case k of + isAlias = case k of SKNameAlias -> True _ -> False sns :: Sing ns = sing From 9d707d06cd67f98b546d64dbd5bb6dc6b99982b9 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 18:48:49 +0200 Subject: [PATCH 17/18] html --- src/Juvix/Compiler/Backend/Html/Translation/FromTyped/Source.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped/Source.hs b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped/Source.hs index 4a33989c6b..da6e0c86cd 100644 --- a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped/Source.hs +++ b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped/Source.hs @@ -293,6 +293,7 @@ putTag ann x = case ann of S.KNameLocal -> "ju-var" S.KNameAxiom -> "ju-axiom" S.KNameLocalModule -> "ju-var" + S.KNameAlias -> "ju-var" S.KNameTopModule -> "ju-var" S.KNameFixity -> "ju-fixity" ) From 2ab5125e8586e4e9450f699a20803137cce20095 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 23:21:23 +0200 Subject: [PATCH 18/18] pragmas in let --- src/Juvix/Compiler/Concrete/Translation/FromSource.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index adf9237574..96ac1f7312 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -838,7 +838,7 @@ letFunDef = do letStatement :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (LetStatement 'Parsed) letStatement = - LetFunctionDef <$> functionDefinition Nothing + LetFunctionDef <$> letFunDef <|> LetAliasDef <$> (kw kwSyntax >>= aliasDef) letBlock :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Let 'Parsed)