From e939f8fe9fd01f1ab4b3a29bb19ae8a0abb3ee06 Mon Sep 17 00:00:00 2001 From: janmasrovira Date: Thu, 21 Jul 2022 16:54:08 +0300 Subject: [PATCH] Keep qualified names (#1392) * keep qualified names * add comment * add pretty field to Abstract Name * add test * Add shell test * Add another test * fix shell test Co-authored-by: Jonathan Cubides --- src/Juvix/Syntax/Abstract/Language/Extra.hs | 1 + src/Juvix/Syntax/Abstract/Name.hs | 13 ++++++- src/Juvix/Syntax/Abstract/Pretty/Ann.hs | 7 +++- src/Juvix/Syntax/Abstract/Pretty/Base.hs | 9 +---- src/Juvix/Syntax/Concrete/Name.hs | 16 +++++++- src/Juvix/Syntax/Concrete/Scoped/Name.hs | 4 ++ .../Syntax/Concrete/Scoped/Name/NameKind.hs | 3 ++ src/Juvix/Syntax/MicroJuvix/Pretty/Ann.hs | 3 ++ src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs | 9 +---- src/Juvix/Syntax/MicroJuvix/TypeChecker.hs | 7 +++- .../Translation/MicroJuvixToMonoJuvix.hs | 37 +++++++------------ src/Juvix/Translation/ScopedToAbstract.hs | 8 +++- tests/negative/issue1344/D.juvix | 8 ++++ tests/negative/issue1344/M.juvix | 11 ++++++ tests/negative/issue1344/Other.juvix | 7 ++++ tests/negative/issue1344/U.juvix | 6 +++ tests/negative/issue1344/errorD.test | 8 ++++ tests/negative/issue1344/errorM.test | 8 ++++ tests/negative/issue1344/juvix.yaml | 0 19 files changed, 119 insertions(+), 46 deletions(-) create mode 100644 tests/negative/issue1344/D.juvix create mode 100644 tests/negative/issue1344/M.juvix create mode 100644 tests/negative/issue1344/Other.juvix create mode 100644 tests/negative/issue1344/U.juvix create mode 100644 tests/negative/issue1344/errorD.test create mode 100644 tests/negative/issue1344/errorM.test create mode 100644 tests/negative/issue1344/juvix.yaml diff --git a/src/Juvix/Syntax/Abstract/Language/Extra.hs b/src/Juvix/Syntax/Abstract/Language/Extra.hs index 26b601767..79f364f81 100644 --- a/src/Juvix/Syntax/Abstract/Language/Extra.hs +++ b/src/Juvix/Syntax/Abstract/Language/Extra.hs @@ -272,5 +272,6 @@ freshVar n = do { _nameId = uid, _nameText = n, _nameKind = KNameLocal, + _namePretty = n, _nameLoc = error "freshVar with no location" } diff --git a/src/Juvix/Syntax/Abstract/Name.hs b/src/Juvix/Syntax/Abstract/Name.hs index c6be72386..e012a77f9 100644 --- a/src/Juvix/Syntax/Abstract/Name.hs +++ b/src/Juvix/Syntax/Abstract/Name.hs @@ -16,6 +16,7 @@ data Name = Name { _nameText :: Text, _nameId :: NameId, _nameKind :: NameKind, + _namePretty :: Text, -- How to print this name in error messages _nameLoc :: Interval } deriving stock (Show) @@ -42,10 +43,20 @@ instance HasNameKind Name where instance Pretty Name where pretty n = - pretty (n ^. nameText) + pretty (n ^. namePretty) <> "@" <> pretty (n ^. nameId) +prettyName :: HasNameKindAnn a => Bool -> Name -> Doc a +prettyName showNameId n = + annotate + (annNameKind (n ^. nameKind)) + (pretty (n ^. namePretty) uid) + where + uid + | showNameId = Just ("@" <> pretty (n ^. nameId)) + | otherwise = Nothing + type FunctionName = Name type ConstructorName = Name diff --git a/src/Juvix/Syntax/Abstract/Pretty/Ann.hs b/src/Juvix/Syntax/Abstract/Pretty/Ann.hs index e324b45a1..c894c221b 100644 --- a/src/Juvix/Syntax/Abstract/Pretty/Ann.hs +++ b/src/Juvix/Syntax/Abstract/Pretty/Ann.hs @@ -1,11 +1,11 @@ module Juvix.Syntax.Abstract.Pretty.Ann where import Juvix.Prelude -import Juvix.Syntax.Concrete.Scoped.Name qualified as S +import Juvix.Syntax.Concrete.Scoped.Name.NameKind import Juvix.Syntax.Concrete.Scoped.Pretty.Base qualified as S data Ann - = AnnKind S.NameKind + = AnnKind NameKind | AnnKeyword | AnnImportant | AnnLiteralString @@ -21,3 +21,6 @@ fromScopedAnn s = case s of S.AnnRef {} -> Nothing S.AnnLiteralString -> Just AnnLiteralInteger S.AnnLiteralInteger -> Just AnnLiteralString + +instance HasNameKindAnn Ann where + annNameKind = AnnKind diff --git a/src/Juvix/Syntax/Abstract/Pretty/Base.hs b/src/Juvix/Syntax/Abstract/Pretty/Base.hs index 06814d696..ba9038afa 100644 --- a/src/Juvix/Syntax/Abstract/Pretty/Base.hs +++ b/src/Juvix/Syntax/Abstract/Pretty/Base.hs @@ -159,14 +159,7 @@ instance PrettyCode NameId where instance PrettyCode Name where ppCode n = do showNameId <- asks (^. optShowNameIds) - uid <- - if - | showNameId -> Just . ("@" <>) <$> ppCode (n ^. nameId) - | otherwise -> return Nothing - return - $ annotate (AnnKind (n ^. nameKind)) - $ pretty (n ^. nameText) - uid + return (prettyName showNameId n) instance PrettyCode Function where ppCode Function {..} = do diff --git a/src/Juvix/Syntax/Concrete/Name.hs b/src/Juvix/Syntax/Concrete/Name.hs index 4ee9554d0..2d2c861e2 100644 --- a/src/Juvix/Syntax/Concrete/Name.hs +++ b/src/Juvix/Syntax/Concrete/Name.hs @@ -2,6 +2,7 @@ module Juvix.Syntax.Concrete.Name where import Data.List.NonEmpty.Extra qualified as NonEmpty import Juvix.Prelude +import Juvix.Prelude.Pretty import Juvix.Syntax.Loc type Symbol = WithLoc Text @@ -18,10 +19,23 @@ data Name deriving stock (Show, Eq, Ord) instance HasLoc Name where - getLoc n = case n of + getLoc = \case NameQualified q -> getLoc q NameUnqualified s -> getLoc s +instance Pretty QualifiedName where + pretty (QualifiedName (Path path) s) = + let symbols = snoc (toList path) s + in dotted (map pretty symbols) + where + dotted :: Foldable f => f (Doc a) -> Doc a + dotted = concatWith (surround ".") + +instance Pretty Name where + pretty = \case + NameQualified q -> pretty q + NameUnqualified s -> pretty s + newtype Path = Path { _pathParts :: NonEmpty Symbol } diff --git a/src/Juvix/Syntax/Concrete/Scoped/Name.hs b/src/Juvix/Syntax/Concrete/Scoped/Name.hs index 547f2b0d8..bd078c009 100644 --- a/src/Juvix/Syntax/Concrete/Scoped/Name.hs +++ b/src/Juvix/Syntax/Concrete/Scoped/Name.hs @@ -6,6 +6,7 @@ module Juvix.Syntax.Concrete.Scoped.Name where import Juvix.Prelude +import Juvix.Prelude.Pretty import Juvix.Syntax.Concrete.Name qualified as C import Juvix.Syntax.Concrete.Scoped.Name.NameKind import Juvix.Syntax.Concrete.Scoped.VisibilityAnn @@ -90,6 +91,9 @@ instance HasNameKind (Name' n) where instance HasLoc n => HasLoc (Name' n) where getLoc = getLoc . (^. nameConcrete) +instance Pretty a => Pretty (Name' a) where + pretty = pretty . (^. nameConcrete) + data AName = forall c. HasLoc c => AName diff --git a/src/Juvix/Syntax/Concrete/Scoped/Name/NameKind.hs b/src/Juvix/Syntax/Concrete/Scoped/Name/NameKind.hs index 5e04a7eda..2ce221de9 100644 --- a/src/Juvix/Syntax/Concrete/Scoped/Name/NameKind.hs +++ b/src/Juvix/Syntax/Concrete/Scoped/Name/NameKind.hs @@ -24,6 +24,9 @@ data NameKind class HasNameKind a where getNameKind :: a -> NameKind +class HasNameKindAnn a where + annNameKind :: NameKind -> a + instance HasNameKind NameKind where getNameKind = id diff --git a/src/Juvix/Syntax/MicroJuvix/Pretty/Ann.hs b/src/Juvix/Syntax/MicroJuvix/Pretty/Ann.hs index f64acaf1d..6df36b2a1 100644 --- a/src/Juvix/Syntax/MicroJuvix/Pretty/Ann.hs +++ b/src/Juvix/Syntax/MicroJuvix/Pretty/Ann.hs @@ -7,3 +7,6 @@ data Ann | AnnKeyword | AnnLiteralString | AnnLiteralInteger + +instance HasNameKindAnn Ann where + annNameKind = AnnKind diff --git a/src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs b/src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs index 3576d30d9..7a421dc74 100644 --- a/src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs +++ b/src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs @@ -34,14 +34,7 @@ instance PrettyCode NameId where instance PrettyCode Name where ppCode n = do showNameId <- asks (^. optShowNameIds) - uid <- - if - | showNameId -> Just . ("@" <>) <$> ppCode (n ^. nameId) - | otherwise -> return Nothing - return - $ annotate (AnnKind (n ^. nameKind)) - $ pretty (n ^. nameText) - uid + return (prettyName showNameId n) instance PrettyCode Iden where ppCode :: Member (Reader Options) r => Iden -> Sem r (Doc Ann) diff --git a/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs b/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs index 79d42e82f..f16dee28f 100644 --- a/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs +++ b/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs @@ -349,10 +349,13 @@ freshHole l = do literalType :: Members '[NameIdGen] r => LiteralLoc -> Sem r TypedExpression literalType l = do uid <- freshNameId - let typeVar = + let strA :: Text + strA = "A" + typeVar = Name - { _nameText = "A", + { _nameText = strA, _nameId = uid, + _namePretty = strA, _nameKind = KNameLocal, _nameLoc = getLoc l } diff --git a/src/Juvix/Translation/MicroJuvixToMonoJuvix.hs b/src/Juvix/Translation/MicroJuvixToMonoJuvix.hs index 4997674a7..94aa25398 100644 --- a/src/Juvix/Translation/MicroJuvixToMonoJuvix.hs +++ b/src/Juvix/Translation/MicroJuvixToMonoJuvix.hs @@ -67,7 +67,7 @@ cloneName' n = do return (set Micro.nameId fresh n) cloneName :: Members '[NameIdGen] r => Micro.Name -> Sem r Name -cloneName n = goName <$> cloneName' n +cloneName n = cloneName' n addConcreteInfo :: NonEmpty Micro.ConcreteType -> ConcreteIdenInfo -> Maybe PolyIdenInfo -> PolyIdenInfo addConcreteInfo t c = \case @@ -164,7 +164,7 @@ goModule Micro.Module {..} = do _moduleBody' <- goModuleBody _moduleBody return Module - { _moduleName = goName _moduleName, + { _moduleName = _moduleName, _moduleBody = _moduleBody' } @@ -199,20 +199,11 @@ goAxiomDef Micro.AxiomDef {..} = do let _axiomBuiltin' = _axiomBuiltin return AxiomDef - { _axiomName = goName _axiomName, + { _axiomName = _axiomName, _axiomBuiltin = _axiomBuiltin', _axiomType = _axiomType' } -goName :: Micro.Name -> Name -goName n = - Name - { _nameText = n ^. Micro.nameText, - _nameId = n ^. Micro.nameId, - _nameLoc = n ^. Micro.nameLoc, - _nameKind = n ^. Micro.nameKind - } - lookupPolyConstructor :: Members '[Reader ConcreteTable] r => Micro.ConstructorName -> @@ -267,7 +258,7 @@ goInductiveDefConcrete def = do constructors' <- mapM goConstructor (def ^. Micro.inductiveConstructors) return InductiveDef - { _inductiveName = goName (def ^. Micro.inductiveName), + { _inductiveName = def ^. Micro.inductiveName, _inductiveBuiltin = def ^. Micro.inductiveBuiltin, _inductiveConstructors = constructors' } @@ -277,7 +268,7 @@ goInductiveDefConcrete def = do params' <- mapM (goType . Micro.mkConcreteType') (c ^. Micro.constructorParameters) return InductiveConstructorDef - { _constructorName = goName (c ^. Micro.constructorName), + { _constructorName = c ^. Micro.constructorName, _constructorParameters = params' } @@ -327,10 +318,10 @@ goExpression = go return (foldApplication fun' tailArgs') goIden :: Micro.Iden -> Iden goIden = \case - Micro.IdenFunction f -> IdenFunction (goName f) - Micro.IdenVar v -> IdenVar (goName v) - Micro.IdenAxiom a -> IdenAxiom (goName a) - Micro.IdenConstructor c -> IdenConstructor (goName c) + Micro.IdenFunction f -> IdenFunction f + Micro.IdenVar v -> IdenVar v + Micro.IdenAxiom a -> IdenAxiom a + Micro.IdenConstructor c -> IdenConstructor c Micro.IdenInductive {} -> impossible goFunctionDefConcrete :: @@ -351,7 +342,7 @@ goFunctionDefConcrete n d = do } where funName :: Name - funName = fromMaybe (goName (d ^. Micro.funDefName)) n + funName = fromMaybe (d ^. Micro.funDefName) n concreteTy :: Micro.ConcreteType concreteTy = Micro.mkConcreteType' (d ^. Micro.funDefType) patternTys :: [Micro.ConcreteType] @@ -460,7 +451,7 @@ goPatternArg ty = goPattern ty . (^. Micro.patternArgPattern) goPattern :: forall r. Members '[Reader ConcreteTable, Reader Micro.InfoTable] r => Micro.ConcreteType -> Micro.Pattern -> Sem r Pattern goPattern ty = \case - Micro.PatternVariable v -> return (PatternVariable (goName v)) + Micro.PatternVariable v -> return (PatternVariable v) Micro.PatternConstructorApp capp -> PatternConstructorApp <$> goApp capp Micro.PatternWildcard {} -> return PatternWildcard where @@ -468,7 +459,7 @@ goPattern ty = \case goApp capp = case ty ^. Micro.unconcreteType of Micro.ExpressionIden Micro.IdenInductive {} -> do let c' :: Name - c' = goName (capp ^. Micro.constrAppConstructor) + c' = capp ^. Micro.constrAppConstructor cInfo <- Micro.lookupConstructor (capp ^. Micro.constrAppConstructor) let psTysConcrete = map Micro.mkConcreteType' (cInfo ^. Micro.constructorInfoArgs) ps' <- zipWithM goPatternArg psTysConcrete (capp ^. Micro.constrAppParameters) @@ -535,8 +526,8 @@ goType = go . (^. Micro.unconcreteType) return (Function l' r') goIden :: Micro.Iden -> TypeIden goIden = \case - Micro.IdenAxiom a -> TypeIdenAxiom (goName a) - Micro.IdenInductive i -> TypeIdenInductive (goName i) + Micro.IdenAxiom a -> TypeIdenAxiom a + Micro.IdenInductive i -> TypeIdenInductive i Micro.IdenVar {} -> impossible Micro.IdenFunction {} -> impossible Micro.IdenConstructor {} -> impossible diff --git a/src/Juvix/Translation/ScopedToAbstract.hs b/src/Juvix/Translation/ScopedToAbstract.hs index 4ff394619..9bc669dde 100644 --- a/src/Juvix/Translation/ScopedToAbstract.hs +++ b/src/Juvix/Translation/ScopedToAbstract.hs @@ -8,6 +8,7 @@ import Data.HashMap.Strict qualified as HashMap import Juvix.Builtins import Juvix.Internal.NameIdGen import Juvix.Prelude +import Juvix.Prelude.Pretty import Juvix.Syntax.Abstract.AbstractResult import Juvix.Syntax.Abstract.InfoTableBuilder import Juvix.Syntax.Abstract.Language qualified as Abstract @@ -73,7 +74,11 @@ goModule m = case sing :: SModuleIsTop t of SModuleLocal -> goSymbol n goName :: S.Name -> Abstract.Name -goName = goSymbol . S.nameUnqualify +goName name = + set Abstract.namePretty prettyStr (goSymbol (S.nameUnqualify name)) + where + prettyStr :: Text + prettyStr = prettyText name goSymbol :: S.Symbol -> Abstract.Name goSymbol s = @@ -81,6 +86,7 @@ goSymbol s = { _nameText = S.symbolText s, _nameId = s ^. S.nameId, _nameKind = getNameKind s, + _namePretty = S.symbolText s, _nameLoc = s ^. S.nameConcrete . symbolLoc } diff --git a/tests/negative/issue1344/D.juvix b/tests/negative/issue1344/D.juvix new file mode 100644 index 000000000..ba23c0e34 --- /dev/null +++ b/tests/negative/issue1344/D.juvix @@ -0,0 +1,8 @@ +module D; + import Other; + import U; + + u : Other.Unit; + u ≔ U.t; + +end; diff --git a/tests/negative/issue1344/M.juvix b/tests/negative/issue1344/M.juvix new file mode 100644 index 000000000..f055108ed --- /dev/null +++ b/tests/negative/issue1344/M.juvix @@ -0,0 +1,11 @@ +module M; + import Other; + + inductive Unit { + t : Unit; + }; + + u : Other.Unit; + u ≔ t; + +end; diff --git a/tests/negative/issue1344/Other.juvix b/tests/negative/issue1344/Other.juvix new file mode 100644 index 000000000..fcebd795d --- /dev/null +++ b/tests/negative/issue1344/Other.juvix @@ -0,0 +1,7 @@ +module Other; + + inductive Unit { + t : Unit; + }; + +end; diff --git a/tests/negative/issue1344/U.juvix b/tests/negative/issue1344/U.juvix new file mode 100644 index 000000000..59fe4dbf7 --- /dev/null +++ b/tests/negative/issue1344/U.juvix @@ -0,0 +1,6 @@ +module U; + inductive Unit { + t : Unit; + }; + +end; \ No newline at end of file diff --git a/tests/negative/issue1344/errorD.test b/tests/negative/issue1344/errorD.test new file mode 100644 index 000000000..f977a2290 --- /dev/null +++ b/tests/negative/issue1344/errorD.test @@ -0,0 +1,8 @@ +$ juvix typecheck tests/negative/issue1344/D.juvix --no-colors +>2 /.*\.juvix\:[0-9]+\:[0-9]+\-[0-9]+\: error\: +The expression U.t has type: + Unit +but is expected to have type: + Other.Unit +/ +>= 1 diff --git a/tests/negative/issue1344/errorM.test b/tests/negative/issue1344/errorM.test new file mode 100644 index 000000000..6a242a477 --- /dev/null +++ b/tests/negative/issue1344/errorM.test @@ -0,0 +1,8 @@ +$ juvix typecheck tests/negative/issue1344/M.juvix --no-colors +>2 /.*\.juvix\:[0-9]+\:[0-9]+\-[0-9]+\: error\: +The expression t has type: + Unit +but is expected to have type: + Other.Unit +/ +>= 1 \ No newline at end of file diff --git a/tests/negative/issue1344/juvix.yaml b/tests/negative/issue1344/juvix.yaml new file mode 100644 index 000000000..e69de29bb