Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Aliasing #2301

Merged
merged 18 commits into from
Aug 25, 2023
6 changes: 4 additions & 2 deletions app/Commands/Repl.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -286,6 +286,7 @@ printDocumentation = replParseIdentifiers >=> printIdentifiers
KNameConstructor -> getDocConstructor n
KNameLocalModule -> impossible
KNameTopModule -> impossible
KNameAlias -> impossible
KNameFixity -> impossible
printDoc mdoc
where
Expand Down Expand Up @@ -334,7 +335,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
Expand All @@ -344,6 +345,7 @@ printDefinition = replParseIdentifiers >=> printIdentifiers
KNameLocalModule -> impossible
KNameTopModule -> impossible
KNameFixity -> impossible
KNameAlias -> impossible
where
printLocation :: HasLoc s => s -> Repl ()
printLocation def = do
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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"
)
Expand Down
14 changes: 7 additions & 7 deletions src/Juvix/Compiler/Concrete/Data/Highlight.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {..})
1 change: 1 addition & 0 deletions src/Juvix/Compiler/Concrete/Data/Highlight/RenderEmacs.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ nameKindFace = \case
KNameLocalModule -> Just FaceModule
KNameAxiom -> Just FaceAxiom
KNameLocal -> Nothing
KNameAlias -> Nothing
KNameFixity -> Nothing

fromCodeAnn :: CodeAnn -> Maybe EmacsProperty
Expand Down
14 changes: 13 additions & 1 deletion src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 ()
Expand Down Expand Up @@ -57,7 +58,8 @@ 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)))
RegisterScopedIden n -> modify (over highlightNames (cons (anameFromScopedIden n)))
RegisterModule m -> do
let j = m ^. moduleDoc
modify (over infoModules (HashMap.insert (m ^. modulePath) m))
Expand All @@ -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 ^. scopedIdenFinal . nameId,
_anameDefinedLoc = s ^. scopedIdenName . nameDefined,
_anameVerbatim = s ^. scopedIdenName . nameVerbatim
}
1 change: 1 addition & 0 deletions src/Juvix/Compiler/Concrete/Data/NameSpace.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Juvix/Compiler/Concrete/Data/Scope.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions src/Juvix/Compiler/Concrete/Data/Scope/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
29 changes: 22 additions & 7 deletions src/Juvix/Compiler/Concrete/Data/ScopedName.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down
5 changes: 3 additions & 2 deletions src/Juvix/Compiler/Concrete/Extra.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -140,12 +141,12 @@ 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
getPatternAtomIden = \case
PatternAtomIden i -> case i of
PatternScopedConstructor c -> Just c
PatternScopedConstructor c -> Just (c ^. scopedIdenName)
_ -> Nothing
_ -> Nothing
3 changes: 3 additions & 0 deletions src/Juvix/Compiler/Concrete/Keywords.hs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ import Juvix.Data.Keyword.All
delimParenR,
delimSemicolon,
-- keywords

kwAlias,
kwAs,
kwAssign,
kwAt,
Expand Down Expand Up @@ -94,5 +96,6 @@ nonKeywords =
kwEq,
kwFixity,
kwOperator,
kwAlias,
kwIterator
]
Loading
Loading