From 9305f6979c627c6066732583be3cc15ce3ecb6cb Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 24 Aug 2023 00:25:39 +0200 Subject: [PATCH] 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 c298679f02..21fe2520c0 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -410,6 +410,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 3d3a3fade9..8e3c0b2d41 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 + | ⊥ := ⊤ + | ⊤ := ⊥;