From 56d4fc92724daa90cfd9ae96d4751d19ea748315 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 27 Jul 2023 19:31:52 +0200 Subject: [PATCH 01/17] fix spacing of nullary constructors --- src/Juvix/Compiler/Concrete/Print/Base.hs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index cdcb7e5c2f..6114540c7e 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -961,12 +961,12 @@ instance SingI s => PrettyPrint (ConstructorDef s) where constructorRhsHelper :: ConstructorRhs s -> Sem r () constructorRhsHelper r = spaceMay <> ppCode r where - spaceMay = case r of - ConstructorRhsGadt {} -> space - ConstructorRhsRecord {} -> space - ConstructorRhsAdt a - | null (a ^. rhsAdtArguments) -> mempty - | otherwise -> space + spaceMay = case r of + ConstructorRhsGadt {} -> space + ConstructorRhsRecord {} -> space + ConstructorRhsAdt a + | null (a ^. rhsAdtArguments) -> mempty + | otherwise -> space -- we use this helper so that comments appear before the first optional pipe if the pipe was omitted pipeHelper :: Sem r () From d14b4193e5f032a7fd26aecb4b58d4f99ef952f7 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 27 Jul 2023 19:34:03 +0200 Subject: [PATCH 02/17] ormolu --- src/Juvix/Compiler/Concrete/Print/Base.hs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 6114540c7e..cdcb7e5c2f 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -961,12 +961,12 @@ instance SingI s => PrettyPrint (ConstructorDef s) where constructorRhsHelper :: ConstructorRhs s -> Sem r () constructorRhsHelper r = spaceMay <> ppCode r where - spaceMay = case r of - ConstructorRhsGadt {} -> space - ConstructorRhsRecord {} -> space - ConstructorRhsAdt a - | null (a ^. rhsAdtArguments) -> mempty - | otherwise -> space + spaceMay = case r of + ConstructorRhsGadt {} -> space + ConstructorRhsRecord {} -> space + ConstructorRhsAdt a + | null (a ^. rhsAdtArguments) -> mempty + | otherwise -> space -- we use this helper so that comments appear before the first optional pipe if the pipe was omitted pipeHelper :: Sem r () From 49683b927be3003884b51cc63f50b92122a58ea6 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 28 Jul 2023 00:58:53 +0200 Subject: [PATCH 03/17] wip --- src/Juvix/Compiler/Concrete/Data/Name.hs | 5 ++ src/Juvix/Compiler/Concrete/Language.hs | 40 ++++++++++++++ src/Juvix/Compiler/Concrete/Print/Base.hs | 24 ++++++++ .../FromParsed/Analysis/Scoping.hs | 55 +++++++++++++------ .../Analysis/Scoping/Error/Types.hs | 5 +- .../Concrete/Translation/FromSource.hs | 22 ++++++-- 6 files changed, 129 insertions(+), 22 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/Name.hs b/src/Juvix/Compiler/Concrete/Data/Name.hs index 8fac2ed369..b52cc4df67 100644 --- a/src/Juvix/Compiler/Concrete/Data/Name.hs +++ b/src/Juvix/Compiler/Concrete/Data/Name.hs @@ -97,3 +97,8 @@ moduleNameToTopModulePath = \case NameQualified (QualifiedName (SymbolPath p) s) -> TopModulePath (toList p) s instance Hashable TopModulePath + +splitName :: Name -> ([Symbol], Symbol) +splitName = \case + NameQualified (QualifiedName (SymbolPath p) s) -> (toList p, s) + NameUnqualified s -> ([], s) diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 8b30a770a7..081748f248 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -405,6 +405,24 @@ deriving stock instance Ord (ConstructorDef 'Parsed) deriving stock instance Ord (ConstructorDef 'Scoped) +data RecordUpdateField (s :: Stage) = RecordUpdateField + { _fieldUpdateName :: Symbol, + _fieldUpdateAssignKw :: Irrelevant (KeywordRef), + _fieldUpdateValue :: ExpressionType s + } + +deriving stock instance Show (RecordUpdateField 'Parsed) + +deriving stock instance Show (RecordUpdateField 'Scoped) + +deriving stock instance Eq (RecordUpdateField 'Parsed) + +deriving stock instance Eq (RecordUpdateField 'Scoped) + +deriving stock instance Ord (RecordUpdateField 'Parsed) + +deriving stock instance Ord (RecordUpdateField 'Scoped) + data RecordField (s :: Stage) = RecordField { _fieldName :: SymbolType s, _fieldColon :: Irrelevant (KeywordRef), @@ -1252,6 +1270,25 @@ deriving stock instance Ord (ArgumentBlock 'Parsed) deriving stock instance Ord (ArgumentBlock 'Scoped) +data RecordUpdate (s :: Stage) = RecordUpdate + { _recordUpdateAtKw :: Irrelevant KeywordRef, + _recordUpdateDelims :: Irrelevant (KeywordRef, KeywordRef), + _recordUpdateTypeName :: IdentifierType s, + _recordUpdateFields :: NonEmpty (RecordUpdateField s) + } + +deriving stock instance Show (RecordUpdate 'Parsed) + +deriving stock instance Show (RecordUpdate 'Scoped) + +deriving stock instance Eq (RecordUpdate 'Parsed) + +deriving stock instance Eq (RecordUpdate 'Scoped) + +deriving stock instance Ord (RecordUpdate 'Parsed) + +deriving stock instance Ord (RecordUpdate 'Scoped) + data NamedApplication (s :: Stage) = NamedApplication { _namedAppName :: IdentifierType s, _namedAppArgs :: NonEmpty (ArgumentBlock s), @@ -1279,6 +1316,7 @@ data ExpressionAtom (s :: Stage) | AtomHole (HoleType s) | AtomBraces (WithLoc (ExpressionType s)) | AtomLet (Let s) + | AtomRecordUpdate (RecordUpdate s) | AtomUniverse Universe | AtomFunction (Function s) | AtomFunArrow KeywordRef @@ -1440,6 +1478,8 @@ newtype ModuleIndex = ModuleIndex } makeLenses ''PatternArg +makeLenses ''RecordUpdate +makeLenses ''RecordUpdateField makeLenses ''NonDefinitionsSection makeLenses ''DefinitionsSection makeLenses ''ProjectionDef diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index cdcb7e5c2f..251ec02691 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -271,6 +271,29 @@ instance SingI s => PrettyPrint (NamedApplication s) where -- ppCode :: Members '[ExactPrint, Reader Options] r => NamedApplication s -> Sem r () ppCode = apeHelper +instance SingI s => PrettyPrint (RecordUpdateField s) where + ppCode RecordUpdateField {..} = + ppCode _fieldUpdateName <+> ppCode _fieldUpdateAssignKw <+> ppExpressionType _fieldUpdateValue + +instance SingI s => PrettyPrint (RecordUpdate s) where + ppCode RecordUpdate {..} = do + let Irrelevant (l, r) = _recordUpdateDelims + fields' + | null (_recordUpdateFields ^. _tail1) = ppCode (_recordUpdateFields ^. _head1) + | otherwise = + line + <> indent + ( sequenceWith + (semicolon >> line) + (ppCode <$> _recordUpdateFields) + ) + <> line + ppCode _recordUpdateAtKw + <> ppIdentifierType _recordUpdateTypeName + <> ppCode l + <> fields' + <> ppCode r + instance SingI s => PrettyPrint (ExpressionAtom s) where ppCode = \case AtomIdentifier n -> ppIdentifierType n @@ -279,6 +302,7 @@ instance SingI s => PrettyPrint (ExpressionAtom s) where AtomCase c -> ppCode c AtomList l -> ppCode l AtomUniverse uni -> ppCode uni + AtomRecordUpdate u -> ppCode u AtomFunction fun -> ppCode fun AtomLiteral lit -> ppCode lit AtomFunArrow a -> ppCode a diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index c8d68575df..41670601cb 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1711,23 +1711,31 @@ checkPatternName n = do return (PatternScopedConstructor constr) -- the symbol is a constructor Nothing -> PatternScopedVar <$> bindVariableSymbol sym -- the symbol is a variable where - (path, sym) = case n of - NameQualified (QualifiedName (SymbolPath p) s) -> (toList p, s) - NameUnqualified s -> ([], s) - -- check whether the symbol is a constructor in scope + sym = snd (splitName n) getConstructorRef :: Sem r (Maybe S.Name) - getConstructorRef = do - entries <- mapMaybe getConstructor . fst <$> lookupQualifiedSymbol (path, sym) - case entries of - [] -> case SymbolPath <$> nonEmpty path of - Nothing -> return Nothing -- There is no constructor with such a name - Just pth -> throw (ErrQualSymNotInScope (QualSymNotInScope (QualifiedName pth sym))) - [e] -> return (Just (set S.nameConcrete n e)) -- There is one constructor with such a name - es -> throw (ErrAmbiguousSym (AmbiguousSym n (map SymbolEntry es))) - getConstructor :: SymbolEntry -> Maybe (S.Name' ()) - getConstructor e = case getNameKind e of - KNameConstructor -> Just (e ^. symbolEntry) - _ -> Nothing + getConstructorRef = lookupSymbolOfKind KNameConstructor n + +lookupSymbolOfKind :: + forall r. + Members '[Error ScoperError, State Scope, NameIdGen, State ScoperState, InfoTableBuilder] r => + NameKind -> + Name -> + Sem r (Maybe S.Name) +lookupSymbolOfKind nameKind n = do + entries <- mapMaybe filterEntry . fst <$> lookupQualifiedSymbol (path, sym) + case entries of + [] -> case SymbolPath <$> nonEmpty path of + -- TODO! handle Nothing differnently for non-constructors!!! + Nothing -> return Nothing -- There is no constructor with such a name + Just pth -> throw (ErrQualSymNotInScope (QualSymNotInScope (QualifiedName pth sym))) + [e] -> return (Just (set S.nameConcrete n e)) -- There is one constructor with such a name + es -> throw (ErrAmbiguousSym (AmbiguousSym n (map SymbolEntry es))) + where + (path, sym) = splitName n + filterEntry :: SymbolEntry -> Maybe (S.Name' ()) + filterEntry e + | nameKind == getNameKind e = Just (e ^. symbolEntry) + | otherwise = Nothing checkPatternBinding :: Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => @@ -1793,6 +1801,21 @@ checkExpressionAtom e = case e of AtomIterator i -> pure . AtomIterator <$> checkIterator i AtomNamedApplication i -> pure . AtomNamedApplication <$> checkNamedApplication i AtomAmbiguousIterator i -> checkAmbiguousIterator i + AtomRecordUpdate i -> pure . AtomRecordUpdate <$> checkRecordUpdate i + +checkRecordUpdate :: forall r. RecordUpdate 'Parsed -> Sem r (RecordUpdate 'Scoped) +checkRecordUpdate RecordUpdate {..} = do + tyName' <- fromMaybeM notInScope (lookupSymbolOfKind KNameInductive _recordUpdateTypeName) + return + RecordUpdate + { _recordUpdateTypeName = ScopedIden (tyName'), + _recordUpdateAtKw, + _recordUpdateDelims + } + where + notInScope :: Sem r a + notInScope = do + throw (ErrQualSymNotInScope (QualSymNotInScope _recordUpdateTypeName)) checkAmbiguousIterator :: forall r. 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 05aa98846d..9f2136391c 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 @@ -319,12 +319,13 @@ makeLenses ''NotInScope instance ToGenericError NotInScope where genericError e@NotInScope {..} = ask >>= generr where + loc =getLoc (e ^. notInScopeSymbol) generr opts = return GenericError - { _genericErrorLoc = e ^. notInScopeSymbol . symbolLoc, + { _genericErrorLoc = loc, _genericErrorMessage = prettyError msg, - _genericErrorIntervals = [e ^. notInScopeSymbol . symbolLoc] + _genericErrorIntervals = [loc] } where opts' = fromGenericOptions opts diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index e9d0545a4e..9633ff5ef6 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -591,11 +591,24 @@ importedModule t = unlessM (moduleVisited t) go txt <- readFile' path eitherM throw (const (return ())) (runModuleParser path txt) --------------------------------------------------------------------------------- --- Expression --------------------------------------------------------------------------------- +recordUpdateField :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (RecordUpdateField 'Parsed) +recordUpdateField = do + _fieldUpdateName <- symbol + _fieldUpdateAssignKw <- Irrelevant <$> kw kwColon + _fieldUpdateValue <- parseExpressionAtoms + return RecordUpdateField {..} + +recordUpdate :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (RecordUpdate 'Parsed) +recordUpdate = do + _recordUpdateAtKw <- Irrelevant <$> kw kwAt + _recordUpdateTypeName <- name + l <- kw delimBraceL + _recordUpdateFields <- P.sepEndBy1 recordUpdateField semicolon + r <- kw delimBraceL + let _recordUpdateDelims = Irrelevant (l, r) + return RecordUpdate {..} -expressionAtom :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (ExpressionAtom 'Parsed) +expressionAtom :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (ExpressionAtom 'Parsed) expressionAtom = P.label "" $ AtomLiteral <$> P.try literal @@ -612,6 +625,7 @@ expressionAtom = <|> AtomHole <$> hole <|> AtomParens <$> parens parseExpressionAtoms <|> AtomBraces <$> withLoc (braces parseExpressionAtoms) + <|> AtomRecordUpdate <$> recordUpdate parseExpressionAtoms :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => From 512a4aa6cf0b087888cb15ce307e5df427b12adb Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Sat, 29 Jul 2023 12:34:37 +0200 Subject: [PATCH 04/17] parse, scope, print record updates --- runtime/src/juvix/info.h | 1 + .../Compiler/Backend/C/Translation/FromReg.hs | 1 + .../Concrete/Data/NameSignature/Base.hs | 6 + .../Concrete/Data/NameSignature/Builder.hs | 10 ++ .../Compiler/Concrete/Data/Scope/Base.hs | 4 +- src/Juvix/Compiler/Concrete/Language.hs | 35 ++++++ src/Juvix/Compiler/Concrete/Print/Base.hs | 5 + .../FromParsed/Analysis/Scoping.hs | 107 ++++++++++++++---- .../FromParsed/Analysis/Scoping/Error.hs | 2 + .../Analysis/Scoping/Error/Types.hs | 24 +++- .../Concrete/Translation/FromSource.hs | 4 +- .../Internal/Translation/FromConcrete.hs | 5 + src/Juvix/Data/Fixity.hs | 21 ++-- test/Scope/Negative.hs | 7 ++ tests/negative/NoNamedArguments.juvix | 5 + tests/positive/Records.juvix | 9 ++ 16 files changed, 208 insertions(+), 38 deletions(-) create mode 100644 tests/negative/NoNamedArguments.juvix diff --git a/runtime/src/juvix/info.h b/runtime/src/juvix/info.h index 0b2bc95f81..e764aa87fa 100644 --- a/runtime/src/juvix/info.h +++ b/runtime/src/juvix/info.h @@ -10,6 +10,7 @@ typedef struct { assoc_t assoc; } fixity_t; +#define PREC_MINUS_OMEGA1 (-2) #define PREC_MINUS_OMEGA (-1) #define PREC_OMEGA 100000 diff --git a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs index 1d8ea5c9a6..bc98daac24 100644 --- a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs @@ -66,6 +66,7 @@ fromReg lims tab = getPrec :: Precedence -> Expression getPrec = \case + PrecMinusOmega1 -> macroVar "PREC_MINUS_OMEGA1" PrecMinusOmega -> macroVar "PREC_MINUS_OMEGA" PrecOmega -> macroVar "PREC_OMEGA" PrecNat n -> integer n diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Base.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Base.hs index e5a5daf5b1..30f776cfea 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Base.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Base.hs @@ -17,5 +17,11 @@ newtype NameSignature = NameSignature } deriving stock (Show) +newtype RecordNameSignature = RecordNameSignature + { _recordNames :: HashMap Symbol (Symbol, Int) + } + deriving stock (Show) + makeLenses ''NameSignature +makeLenses ''RecordNameSignature makeLenses ''NameBlock diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index a189c39279..b18ce0854c 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -1,5 +1,6 @@ module Juvix.Compiler.Concrete.Data.NameSignature.Builder ( mkNameSignature, + mkRecordNameSignature, HasNameSignature, module Juvix.Compiler.Concrete.Data.NameSignature.Base, -- to supress unused warning @@ -7,6 +8,7 @@ module Juvix.Compiler.Concrete.Data.NameSignature.Builder ) where +import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Concrete.Data.NameSignature.Base import Juvix.Compiler.Concrete.Data.NameSignature.Error import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error @@ -182,3 +184,11 @@ addSymbol' impl sym = do endBuild' :: Sem (Re r) a endBuild' = get @BuilderState >>= throw + +mkRecordNameSignature :: RhsRecord 'Parsed -> RecordNameSignature +mkRecordNameSignature rhs = + RecordNameSignature + ( HashMap.fromList + [ (s, (s, idx)) | (Indexed idx field) <- indexFrom 0 (toList (rhs ^. rhsRecordFields)), let s = field ^. fieldName + ] + ) diff --git a/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs b/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs index 02413be719..4c4921e0c0 100644 --- a/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs +++ b/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs @@ -52,7 +52,9 @@ data ScoperState = ScoperState -- | Local and top modules _scoperModules :: HashMap S.ModuleNameId (ModuleRef' 'S.NotConcrete), _scoperScope :: HashMap TopModulePath Scope, - _scoperSignatures :: HashMap S.NameId NameSignature + _scoperSignatures :: HashMap S.NameId NameSignature, + -- | Indexed by the inductive type. This is meant to be used for record updates + _scoperRecordSignatures :: HashMap S.NameId RecordNameSignature } data SymbolFixity = SymbolFixity diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 081748f248..a9c9681a54 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -942,6 +942,7 @@ data Expression | ExpressionLiteral LiteralLoc | ExpressionFunction (Function 'Scoped) | ExpressionHole (HoleType 'Scoped) + | ExpressionRecordUpdate RecordUpdateApp | ExpressionBraces (WithLoc Expression) | ExpressionIterator (Iterator 'Scoped) | ExpressionNamedApplication (NamedApplication 'Scoped) @@ -1289,6 +1290,12 @@ deriving stock instance Ord (RecordUpdate 'Parsed) deriving stock instance Ord (RecordUpdate 'Scoped) +data RecordUpdateApp = RecordUpdateApp + { _recordAppUpdate :: RecordUpdate 'Scoped, + _recordAppExpression :: Expression + } + deriving stock (Show, Eq, Ord) + data NamedApplication (s :: Stage) = NamedApplication { _namedAppName :: IdentifierType s, _namedAppArgs :: NonEmpty (ArgumentBlock s), @@ -1479,6 +1486,7 @@ newtype ModuleIndex = ModuleIndex makeLenses ''PatternArg makeLenses ''RecordUpdate +makeLenses ''RecordUpdateApp makeLenses ''RecordUpdateField makeLenses ''NonDefinitionsSection makeLenses ''DefinitionsSection @@ -1581,6 +1589,7 @@ instance HasAtomicity Expression where ExpressionCase c -> atomicity c ExpressionIterator i -> atomicity i ExpressionNamedApplication i -> atomicity i + ExpressionRecordUpdate {} -> Aggregate updateFixity expressionAtomicity :: forall s. SingI s => ExpressionType s -> Atomicity expressionAtomicity e = case sing :: SStage s of @@ -1693,6 +1702,15 @@ instance HasLoc (List s) where instance SingI s => HasLoc (NamedApplication s) where getLoc NamedApplication {..} = getLocIdentifierType _namedAppName <> getLoc (last _namedAppArgs) +instance SingI s => HasLoc (RecordUpdateField s) where + getLoc f = getLoc (f ^. fieldUpdateName) <> getLocExpressionType (f ^. fieldUpdateValue) + +instance SingI s => HasLoc (RecordUpdate s) where + getLoc r = getLoc (r ^. recordUpdateAtKw) <> getLocSpan (r ^. recordUpdateFields) + +instance HasLoc RecordUpdateApp where + getLoc r = getLoc (r ^. recordAppExpression) <> getLoc (r ^. recordAppUpdate) + instance HasLoc Expression where getLoc = \case ExpressionIdentifier i -> getLoc i @@ -1711,6 +1729,7 @@ instance HasLoc Expression where ExpressionBraces i -> getLoc i ExpressionIterator i -> getLoc i ExpressionNamedApplication i -> getLoc i + ExpressionRecordUpdate i -> getLoc i getLocIdentifierType :: forall s. SingI s => IdentifierType s -> Interval getLocIdentifierType e = case sing :: SStage s of @@ -2016,6 +2035,16 @@ instance IsApe (Function 'Scoped) ApeLeaf where _infixOp = ApeLeafFunctionKw kw } +instance IsApe RecordUpdateApp ApeLeaf where + toApe :: RecordUpdateApp -> Ape ApeLeaf + toApe a = + ApePostfix + Postfix + { _postfixFixity = updateFixity, + _postfixOp = ApeLeafAtom (sing :&: AtomRecordUpdate (a ^. recordAppUpdate)), + _postfixLeft = toApe (a ^. recordAppExpression) + } + instance IsApe Expression ApeLeaf where toApe e = case e of ExpressionApplication a -> toApe a @@ -2023,6 +2052,7 @@ instance IsApe Expression ApeLeaf where ExpressionPostfixApplication a -> toApe a ExpressionFunction a -> toApe a ExpressionNamedApplication a -> toApe a + ExpressionRecordUpdate a -> toApe a ExpressionParensIdentifier {} -> leaf ExpressionIdentifier {} -> leaf ExpressionList {} -> leaf @@ -2106,3 +2136,8 @@ exportNameSpace :: forall ns. SingI ns => Lens' ExportInfo (HashMap Symbol (Name exportNameSpace = case sing :: SNameSpace ns of SNameSpaceSymbols -> exportSymbols SNameSpaceModules -> exportModuleSymbols + +_ConstructorRhsRecord :: Traversal' (ConstructorRhs s) (RhsRecord s) +_ConstructorRhsRecord f rhs = case rhs of + ConstructorRhsRecord r -> ConstructorRhsRecord <$> f r + _ -> pure rhs diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 251ec02691..e240f6922e 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -577,6 +577,7 @@ instance SingI s => PrettyPrint (Lambda s) where instance PrettyPrint Precedence where ppCode = \case + PrecMinusOmega1 -> noLoc (pretty ("-ω₁" :: Text)) PrecMinusOmega -> noLoc (pretty ("-ω" :: Text)) PrecNat n -> noLoc (pretty n) PrecOmega -> noLoc (pretty ("ω" :: Text)) @@ -610,6 +611,9 @@ instance PrettyPrint IteratorSyntaxDef where <+> iterSymbol' <+?> fmap ppCode _iterAttribs +instance PrettyPrint RecordUpdateApp where + ppCode = apeHelper + instance PrettyPrint Expression where ppCode = \case ExpressionIdentifier n -> ppCode n @@ -628,6 +632,7 @@ instance PrettyPrint Expression where ExpressionCase c -> ppCode c ExpressionIterator i -> ppCode i ExpressionNamedApplication i -> ppCode i + ExpressionRecordUpdate i -> ppCode i instance PrettyPrint (WithSource Pragmas) where ppCode pragma = do diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 41670601cb..7181ea759b 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -35,7 +35,8 @@ iniScoperState = { _scoperModulesCache = ModulesCache mempty, _scoperModules = mempty, _scoperScope = mempty, - _scoperSignatures = mempty + _scoperSignatures = mempty, + _scoperRecordSignatures = mempty } scopeCheck :: @@ -1015,9 +1016,23 @@ checkSections sec = do where reserveInductive :: InductiveDef 'Parsed -> Sem r' () reserveInductive d = do - void (reserveInductiveSymbol d) + i <- reserveInductiveSymbol d constrs <- mapM (reserveConstructorSymbol d) (d ^. inductiveConstructors) void (defineInductiveModule (head constrs) d) + ignoreFail (registerRecord i) + where + registerRecord :: S.Symbol -> Sem (Fail ': r') () + registerRecord ind = do + case d ^. inductiveConstructors of + mkRec :| [] -> do + fs <- + failMaybe $ + mkRec + ^? constructorRhs + . _ConstructorRhsRecord + . to mkRecordNameSignature + modify' (set (scoperRecordSignatures . at (ind ^. S.nameId)) (Just fs)) + _ -> fail goDefinition :: Definition 'Parsed -> Sem r' (Definition 'Scoped) goDefinition = \case @@ -1709,25 +1724,40 @@ checkPatternName n = do Just constr -> do registerName constr return (PatternScopedConstructor constr) -- the symbol is a constructor - Nothing -> PatternScopedVar <$> bindVariableSymbol sym -- the symbol is a variable + 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 = lookupSymbolOfKind KNameConstructor n + getConstructorRef = lookupNameOfKind KNameConstructor n + +nameNotInScope :: forall r a. Members '[Error ScoperError, State Scope] r => Name -> Sem r a +nameNotInScope n = err >>= throw + where + err :: Sem r ScoperError + err = case n of + NameQualified q -> return (ErrQualSymNotInScope (QualSymNotInScope q)) + NameUnqualified s -> ErrSymNotInScope . NotInScope s <$> get -lookupSymbolOfKind :: +getNameOfKind :: forall r. - Members '[Error ScoperError, State Scope, NameIdGen, State ScoperState, InfoTableBuilder] r => + Members '[Error ScoperError, State Scope, State ScoperState] r => + NameKind -> + Name -> + Sem r S.Name +getNameOfKind nameKind n = fromMaybeM (nameNotInScope n) (lookupNameOfKind nameKind n) + +lookupNameOfKind :: + forall r. + Members '[Error ScoperError, State Scope, State ScoperState] r => NameKind -> Name -> Sem r (Maybe S.Name) -lookupSymbolOfKind nameKind n = do +lookupNameOfKind nameKind n = do entries <- mapMaybe filterEntry . fst <$> lookupQualifiedSymbol (path, sym) case entries of - [] -> case SymbolPath <$> nonEmpty path of - -- TODO! handle Nothing differnently for non-constructors!!! - Nothing -> return Nothing -- There is no constructor with such a name - Just pth -> throw (ErrQualSymNotInScope (QualSymNotInScope (QualifiedName pth sym))) + [] -> 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))) where @@ -1803,19 +1833,31 @@ checkExpressionAtom e = case e of AtomAmbiguousIterator i -> checkAmbiguousIterator i AtomRecordUpdate i -> pure . AtomRecordUpdate <$> checkRecordUpdate i -checkRecordUpdate :: forall r. RecordUpdate 'Parsed -> Sem r (RecordUpdate 'Scoped) +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' <- fromMaybeM notInScope (lookupSymbolOfKind KNameInductive _recordUpdateTypeName) + tyName' <- getNameOfKind KNameInductive _recordUpdateTypeName + sig <- getRecordNameSignature (ScopedIden tyName') + fields' <- mapM (checkField sig) _recordUpdateFields return RecordUpdate - { _recordUpdateTypeName = ScopedIden (tyName'), + { _recordUpdateTypeName = ScopedIden tyName', + _recordUpdateFields = fields', _recordUpdateAtKw, _recordUpdateDelims } where - notInScope :: Sem r a - notInScope = do - throw (ErrQualSymNotInScope (QualSymNotInScope _recordUpdateTypeName)) + -- TODO check repetitions + -- TODO check membership + -- TODO should we do this when translating to internal? + checkField :: RecordNameSignature -> RecordUpdateField 'Parsed -> Sem r (RecordUpdateField 'Scoped) + checkField _ f = do + value' <- checkParseExpressionAtoms (f ^. fieldUpdateValue) + return + RecordUpdateField + { _fieldUpdateName = f ^. fieldUpdateName, + _fieldUpdateAssignKw = f ^. fieldUpdateAssignKw, + _fieldUpdateValue = value' + } checkAmbiguousIterator :: forall r. @@ -1852,16 +1894,27 @@ checkNamedApplication napp = do _argBlockArgs <- mapM checkNamedArg (b ^. argBlockArgs) return ArgumentBlock {..} +getRecordNameSignature :: + forall r. + Members '[State ScoperState, Error ScoperError] r => + ScopedIden -> + Sem r RecordNameSignature +getRecordNameSignature indTy = + fromMaybeM err (gets (^. scoperRecordSignatures . at (indTy ^. scopedIden . 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 (getNameSignatureMay s) + sig <- maybeM (throw err) return (lookupNameSignature (s ^. scopedIden . S.nameId)) when (null (sig ^. nameSignatureArgs)) (throw err) return sig where err = ErrNoNameSignature (NoNameSignature s) -getNameSignatureMay :: Members '[State ScoperState] r => ScopedIden -> Sem r (Maybe NameSignature) -getNameSignatureMay s = gets (^. scoperSignatures . at (identifierName s ^. S.nameId)) +lookupNameSignature :: Members '[State ScoperState] r => S.NameId -> Sem r (Maybe NameSignature) +lookupNameSignature s = gets (^. scoperSignatures . at s) checkIterator :: Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => @@ -2033,7 +2086,7 @@ checkSyntaxDef = \case makeExpressionTable :: ExpressionAtoms 'Scoped -> [[P.Operator Parse Expression]] -makeExpressionTable (ExpressionAtoms atoms _) = [appOpExplicit] : operators ++ [[functionOp]] +makeExpressionTable (ExpressionAtoms atoms _) = [recordUpdate] : [appOpExplicit] : operators ++ [[functionOp]] where operators = mkSymbolTable idens @@ -2080,13 +2133,23 @@ makeExpressionTable (ExpressionAtoms atoms _) = [appOpExplicit] : operators ++ [ | uid == identifierName iden ^. S.nameId -> Just iden _ -> Nothing + recordUpdate :: P.Operator Parse Expression + recordUpdate = P.Postfix (mkRecUpdate <$> P.token getRecUpdate mempty) + where + getRecUpdate :: ExpressionAtom 'Scoped -> (Maybe (RecordUpdate 'Scoped)) + getRecUpdate = \case + AtomRecordUpdate u -> Just u + _ -> Nothing + mkRecUpdate :: RecordUpdate 'Scoped -> Expression -> Expression + mkRecUpdate u = ExpressionRecordUpdate . RecordUpdateApp u + -- Application by juxtaposition. appOpExplicit :: P.Operator Parse Expression appOpExplicit = P.InfixL (return app) where app :: Expression -> Expression -> Expression app f x = - ExpressionApplication + ExpressionApplication $ Application { _applicationFunction = f, _applicationParameter = x 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 7672d0eb6d..28bb38afef 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs @@ -42,6 +42,7 @@ data ScoperError | ErrNameSignature NameSignatureError | ErrNoNameSignature NoNameSignature | ErrNamedArgumentsError NamedArgumentsError + | ErrNotARecord NotARecord instance ToGenericError ScoperError where genericError = \case @@ -75,3 +76,4 @@ instance ToGenericError ScoperError where ErrNameSignature e -> genericError e ErrNoNameSignature e -> genericError e ErrNamedArgumentsError e -> genericError e + ErrNotARecord 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 9f2136391c..05ecfb37c1 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 @@ -319,7 +319,7 @@ makeLenses ''NotInScope instance ToGenericError NotInScope where genericError e@NotInScope {..} = ask >>= generr where - loc =getLoc (e ^. notInScopeSymbol) + loc = getLoc (e ^. notInScopeSymbol) generr opts = return GenericError @@ -766,3 +766,25 @@ instance ToGenericError NoNameSignature where where i :: Interval i = getLoc _noNameSignatureIden + +newtype NotARecord = NotARecord + { _notARecord :: ScopedIden + } + deriving stock (Show) + +instance ToGenericError NotARecord where + genericError NotARecord {..} = do + opts <- fromGenericOptions <$> ask + let msg = + "The identifier" + <+> ppCode opts _notARecord + <+> "is not a record type" + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = mkAnsiText msg, + _genericErrorIntervals = [i] + } + where + i :: Interval + i = getLoc _notARecord diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 9633ff5ef6..78fde87ec7 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -594,7 +594,7 @@ importedModule t = unlessM (moduleVisited t) go recordUpdateField :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (RecordUpdateField 'Parsed) recordUpdateField = do _fieldUpdateName <- symbol - _fieldUpdateAssignKw <- Irrelevant <$> kw kwColon + _fieldUpdateAssignKw <- Irrelevant <$> kw kwAssign _fieldUpdateValue <- parseExpressionAtoms return RecordUpdateField {..} @@ -604,7 +604,7 @@ recordUpdate = do _recordUpdateTypeName <- name l <- kw delimBraceL _recordUpdateFields <- P.sepEndBy1 recordUpdateField semicolon - r <- kw delimBraceL + r <- kw delimBraceR let _recordUpdateDelims = Irrelevant (l, r) return RecordUpdate {..} diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index c432e25487..414d7fa787 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -803,10 +803,15 @@ goExpression = \case ExpressionHole h -> return (Internal.ExpressionHole h) ExpressionIterator i -> goIterator i ExpressionNamedApplication i -> goNamedApplication i + ExpressionRecordUpdate i -> goRecordUpdate i where goNamedApplication :: Concrete.NamedApplication 'Scoped -> Sem r Internal.Expression goNamedApplication = runNamedArguments >=> goExpression + -- TODO record update + goRecordUpdate :: Concrete.RecordUpdateApp -> Sem r Internal.Expression + goRecordUpdate = goExpression . (^. Concrete.recordAppExpression) + goList :: Concrete.List 'Scoped -> Sem r Internal.Expression goList l = do nil_ <- getBuiltinName loc BuiltinListNil diff --git a/src/Juvix/Data/Fixity.hs b/src/Juvix/Data/Fixity.hs index 446b37a4ad..8a29c81097 100644 --- a/src/Juvix/Data/Fixity.hs +++ b/src/Juvix/Data/Fixity.hs @@ -2,21 +2,15 @@ module Juvix.Data.Fixity where import Juvix.Prelude.Base +-- | Note that the order of the constructors is important due to the `Ord` +-- instance. +-- TODO should we rename PrecMinusOmega to PrecApp, PrecMinusOmega1 to PrecUpdate, and PrecOmega to PrecFunction/Arrow? data Precedence - = PrecMinusOmega + = PrecMinusOmega1 + | PrecMinusOmega | PrecNat Natural | PrecOmega - deriving stock (Show, Eq, Data) - -instance Ord Precedence where - compare a b = case (a, b) of - (PrecMinusOmega, PrecMinusOmega) -> EQ - (PrecMinusOmega, _) -> LT - (PrecNat _, PrecMinusOmega) -> GT - (PrecNat n, PrecNat m) -> compare n m - (PrecNat _, PrecOmega) -> LT - (PrecOmega, PrecOmega) -> EQ - (PrecOmega, _) -> GT + deriving stock (Show, Eq, Data, Ord) data UnaryAssoc = AssocPostfix deriving stock (Show, Eq, Ord, Data) @@ -80,6 +74,9 @@ appFixity = Fixity PrecOmega (Binary AssocLeft) funFixity :: Fixity funFixity = Fixity PrecMinusOmega (Binary AssocRight) +updateFixity :: Fixity +updateFixity = Fixity PrecMinusOmega1 (Unary AssocPostfix) + atomParens :: (Fixity -> Bool) -> Atomicity -> Fixity -> Bool atomParens associates argAtom opInf = case argAtom of Atom -> False diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index 5f7dd82802..f8da35c574 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -315,5 +315,12 @@ scoperErrorTests = $(mkRelFile "RepeatedNameSignature.juvix") $ \case ErrNameSignature ErrDuplicateName {} -> Nothing + _ -> wrongError, + NegTest + "No named arguments" + $(mkRelDir ".") + $(mkRelFile "NoNamedArguments.juvix") + $ \case + ErrNoNameSignature ErrNoNameSignature {} -> Nothing _ -> wrongError ] diff --git a/tests/negative/NoNamedArguments.juvix b/tests/negative/NoNamedArguments.juvix new file mode 100644 index 0000000000..7ba02fbfbc --- /dev/null +++ b/tests/negative/NoNamedArguments.juvix @@ -0,0 +1,5 @@ +module NoNamedArguments; + +axiom T : Type; + +axiom B : T (x := Type); diff --git a/tests/positive/Records.juvix b/tests/positive/Records.juvix index b62320feb9..0f57f4a739 100644 --- a/tests/positive/Records.juvix +++ b/tests/positive/Records.juvix @@ -35,3 +35,12 @@ p3 : Pair T T -> T := Pair.fst; open Pair; p4 {A : Type} : Pair A T -> A := fst; + +type Bool := false | true; + +module Update; + x : Pair Bool Bool := mkPair false false; + + x' : Pair Bool Bool := x @Pair {fst := true}; + +end; From fe0f60ea3161bea464144bd0e798232b800e18dc Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 31 Jul 2023 11:46:18 +0200 Subject: [PATCH 05/17] compile record updates --- src/Juvix/Compiler/Concrete/Language.hs | 25 ++++++- src/Juvix/Compiler/Concrete/Print/Base.hs | 2 +- .../FromParsed/Analysis/Scoping.hs | 8 ++- src/Juvix/Compiler/Internal/Extra.hs | 22 +++++-- .../Internal/Translation/FromConcrete.hs | 66 +++++++++++++++++-- tests/positive/Records.juvix | 10 +-- 6 files changed, 111 insertions(+), 22 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index a9c9681a54..4483ead3f5 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -22,7 +22,7 @@ import Juvix.Compiler.Concrete.Data.Literal import Juvix.Compiler.Concrete.Data.ModuleIsTop import Juvix.Compiler.Concrete.Data.Name import Juvix.Compiler.Concrete.Data.NameRef -import Juvix.Compiler.Concrete.Data.NameSignature.Base (NameSignature) +import Juvix.Compiler.Concrete.Data.NameSignature.Base import Juvix.Compiler.Concrete.Data.NameSpace import Juvix.Compiler.Concrete.Data.PublicAnn import Juvix.Compiler.Concrete.Data.ScopedName qualified as S @@ -46,6 +46,16 @@ type family NameSpaceEntryType s = res | res -> s where NameSpaceEntryType 'NameSpaceSymbols = SymbolEntry NameSpaceEntryType 'NameSpaceModules = ModuleSymbolEntry +type RecordUpdateExtraType :: Stage -> GHC.Type +type family RecordUpdateExtraType s = res | res -> s where + RecordUpdateExtraType 'Parsed = () + RecordUpdateExtraType 'Scoped = RecordUpdateExtra + +type FieldUpdateArgIxType :: Stage -> GHC.Type +type family FieldUpdateArgIxType s = res | res -> s where + FieldUpdateArgIxType 'Parsed = () + FieldUpdateArgIxType 'Scoped = Int + type SymbolType :: Stage -> GHC.Type type family SymbolType s = res | res -> s where SymbolType 'Parsed = Symbol @@ -406,7 +416,8 @@ deriving stock instance Ord (ConstructorDef 'Parsed) deriving stock instance Ord (ConstructorDef 'Scoped) data RecordUpdateField (s :: Stage) = RecordUpdateField - { _fieldUpdateName :: Symbol, + { _fieldUpdateName :: SymbolType s, + _fieldUpdateArgIx :: FieldUpdateArgIxType s, _fieldUpdateAssignKw :: Irrelevant (KeywordRef), _fieldUpdateValue :: ExpressionType s } @@ -1271,10 +1282,17 @@ deriving stock instance Ord (ArgumentBlock 'Parsed) deriving stock instance Ord (ArgumentBlock 'Scoped) +data RecordUpdateExtra = RecordUpdateExtra + { _recordUpdateExtraConstructor :: S.Symbol, + _recordUpdateExtraSignature :: RecordNameSignature + } + deriving stock (Show) + data RecordUpdate (s :: Stage) = RecordUpdate { _recordUpdateAtKw :: Irrelevant KeywordRef, _recordUpdateDelims :: Irrelevant (KeywordRef, KeywordRef), _recordUpdateTypeName :: IdentifierType s, + _recordUpdateExtra :: Irrelevant (RecordUpdateExtraType s), _recordUpdateFields :: NonEmpty (RecordUpdateField s) } @@ -1485,6 +1503,7 @@ newtype ModuleIndex = ModuleIndex } makeLenses ''PatternArg +makeLenses ''RecordUpdateExtra makeLenses ''RecordUpdate makeLenses ''RecordUpdateApp makeLenses ''RecordUpdateField @@ -1703,7 +1722,7 @@ instance SingI s => HasLoc (NamedApplication s) where getLoc NamedApplication {..} = getLocIdentifierType _namedAppName <> getLoc (last _namedAppArgs) instance SingI s => HasLoc (RecordUpdateField s) where - getLoc f = getLoc (f ^. fieldUpdateName) <> getLocExpressionType (f ^. fieldUpdateValue) + getLoc f = getLocSymbolType (f ^. fieldUpdateName) <> getLocExpressionType (f ^. fieldUpdateValue) instance SingI s => HasLoc (RecordUpdate s) where getLoc r = getLoc (r ^. recordUpdateAtKw) <> getLocSpan (r ^. recordUpdateFields) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index e240f6922e..a7549cdf8f 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -273,7 +273,7 @@ instance SingI s => PrettyPrint (NamedApplication s) where instance SingI s => PrettyPrint (RecordUpdateField s) where ppCode RecordUpdateField {..} = - ppCode _fieldUpdateName <+> ppCode _fieldUpdateAssignKw <+> ppExpressionType _fieldUpdateValue + ppSymbolType _fieldUpdateName <+> ppCode _fieldUpdateAssignKw <+> ppExpressionType _fieldUpdateValue instance SingI s => PrettyPrint (RecordUpdate s) where ppCode RecordUpdate {..} = do diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 7181ea759b..f8e5b9d998 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1836,8 +1836,9 @@ 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' sig <- getRecordNameSignature (ScopedIden tyName') - fields' <- mapM (checkField sig) _recordUpdateFields + fields' <- withLocalScope $ mapM (checkField sig) _recordUpdateFields return RecordUpdate { _recordUpdateTypeName = ScopedIden tyName', @@ -1846,15 +1847,16 @@ checkRecordUpdate RecordUpdate {..} = do _recordUpdateDelims } where - -- TODO check repetitions + -- TODO check repetitions? done by bindvariablesymbol -- TODO check membership -- TODO should we do this when translating to internal? checkField :: RecordNameSignature -> RecordUpdateField 'Parsed -> Sem r (RecordUpdateField 'Scoped) checkField _ f = do + name' <- bindVariableSymbol (f ^. fieldUpdateName) value' <- checkParseExpressionAtoms (f ^. fieldUpdateValue) return RecordUpdateField - { _fieldUpdateName = f ^. fieldUpdateName, + { _fieldUpdateName = name', _fieldUpdateAssignKw = f ^. fieldUpdateAssignKw, _fieldUpdateValue = value' } diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index 364b2e1e05..975ee116b1 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -253,6 +253,12 @@ unnamedParameter ty = _paramType = ty } +singletonRename :: VarName -> VarName -> Rename +singletonRename = HashMap.singleton + +renameVar :: VarName -> VarName -> Expression -> Expression +renameVar a b = substitutionE (renameToSubsE (singletonRename a b)) + renameToSubsE :: Rename -> SubsE renameToSubsE = fmap (ExpressionIden . IdenVar) @@ -704,14 +710,16 @@ patternArgFromVar i v = } -- | Given `mkPair`, returns (mkPair a b, [a, b]) -genConstructorPattern :: Members '[NameIdGen] r => ConstructorInfo -> Sem r (PatternArg, [VarName]) -genConstructorPattern info = do - let nargs = length (snd (constructorArgTypes info)) - loc = getLoc (info ^. constructorInfoName) - vars <- mapM (freshVar loc) (Stream.take nargs allWords) +genConstructorPattern :: Members '[NameIdGen] r => Interval -> ConstructorInfo -> Sem r (PatternArg, [VarName]) +genConstructorPattern loc info = genConstructorPattern' loc (info ^. constructorInfoName) (length (snd (constructorArgTypes info))) + +-- | Given `mkPair`, returns (mkPair a b, [a, b]) +genConstructorPattern' :: Members '[NameIdGen] r => Interval -> Name -> Int -> Sem r (PatternArg, [VarName]) +genConstructorPattern' loc cname cargs = do + vars <- mapM (freshVar loc) (Stream.take cargs allWords) let app = ConstructorApp - { _constrAppConstructor = info ^. constructorInfoName, + { _constrAppConstructor = cname, _constrAppParameters = map (patternArgFromVar Explicit) vars, _constrAppType = Nothing } @@ -751,7 +759,7 @@ genFieldProjection _funDefName info fieldIx = do where genClause :: Sem r FunctionClause genClause = do - (pat, vars) <- genConstructorPattern info + (pat, vars) <- genConstructorPattern (getLoc _funDefName) info let body = toExpression (vars !! fieldIx) return FunctionClause diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 414d7fa787..7b26ba83a1 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -5,14 +5,17 @@ module Juvix.Compiler.Internal.Translation.FromConcrete where import Data.HashMap.Strict qualified as HashMap +import Data.IntMap.Strict qualified as IntMap import Data.List.NonEmpty qualified as NonEmpty import Juvix.Compiler.Builtins +import Juvix.Compiler.Concrete.Data.NameSignature.Base import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Extra qualified as Concrete import Juvix.Compiler.Concrete.Language qualified as Concrete import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error import Juvix.Compiler.Internal.Data.NameDependencyInfo qualified as Internal +import Juvix.Compiler.Internal.Extra (foldExplicitApplication) import Juvix.Compiler.Internal.Extra qualified as Internal import Juvix.Compiler.Internal.Extra.DependencyBuilder import Juvix.Compiler.Internal.Language (varFromWildcard) @@ -803,14 +806,69 @@ goExpression = \case ExpressionHole h -> return (Internal.ExpressionHole h) ExpressionIterator i -> goIterator i ExpressionNamedApplication i -> goNamedApplication i - ExpressionRecordUpdate i -> goRecordUpdate i + ExpressionRecordUpdate i -> goRecordUpdateApp i where goNamedApplication :: Concrete.NamedApplication 'Scoped -> Sem r Internal.Expression goNamedApplication = runNamedArguments >=> goExpression - -- TODO record update - goRecordUpdate :: Concrete.RecordUpdateApp -> Sem r Internal.Expression - goRecordUpdate = goExpression . (^. Concrete.recordAppExpression) + goRecordUpdate :: Concrete.RecordUpdate 'Scoped -> Sem r Internal.Lambda + goRecordUpdate r = do + cl <- mkClause + return + Internal.Lambda + { _lambdaType = Nothing, + _lambdaClauses = pure cl + } + where + numFields = length (r ^. recordUpdateExtra . unIrrelevant . recordUpdateExtraSignature . recordNames) + + -- fields indexed by field index. + fieldMap :: IntMap (RecordUpdateField 'Scoped) + fieldMap = + IntMap.fromList + [ (f ^. fieldUpdateArgIx, f) + | f <- r ^.. recordUpdateFields . each + ] + + mkArgs :: [Indexed Internal.VarName] -> Sem r [Internal.Expression] + mkArgs = execOutputList . go (uncurry Indexed <$> IntMap.toAscList fieldMap) + where + go :: [Indexed (RecordUpdateField 'Scoped)] -> [Indexed Internal.VarName] -> Sem (Output Internal.Expression ': r) () + go fields = \case + [] -> return () + Indexed idx var : vars' -> case getArg idx of + Nothing -> do + output (Internal.toExpression var) + go fields vars' + Just (arg, fields') -> do + let fieldVar = goSymbol (arg ^. fieldUpdateName) + val' <- goExpression (arg ^. fieldUpdateValue) + output (Internal.renameVar fieldVar var val') + go fields' vars' + where + getArg :: Int -> Maybe (RecordUpdateField 'Scoped, [Indexed (RecordUpdateField 'Scoped)]) + getArg idx = do + Indexed fidx arg :| fs <- nonEmpty fields + guard (idx == fidx) + return (arg, fs) + + mkClause :: Sem r Internal.LambdaClause + mkClause = do + let loc = getLoc r + constr = goSymbol (r ^. recordUpdateExtra . unIrrelevant . recordUpdateExtraConstructor) + (patArg, vars) <- Internal.genConstructorPattern' loc constr numFields + args <- mkArgs (indexFrom 0 vars) + return + Internal.LambdaClause + { _lambdaPatterns = pure patArg, + _lambdaBody = foldExplicitApplication (Internal.toExpression constr) args + } + + goRecordUpdateApp :: Concrete.RecordUpdateApp -> Sem r Internal.Expression + goRecordUpdateApp r = do + expr' <- goExpression (r ^. recordAppExpression) + lam <- Internal.ExpressionLambda <$> goRecordUpdate (r ^. recordAppUpdate) + return $ foldExplicitApplication lam [expr'] goList :: Concrete.List 'Scoped -> Sem r Internal.Expression goList l = do diff --git a/tests/positive/Records.juvix b/tests/positive/Records.juvix index 0f57f4a739..f5fcca6202 100644 --- a/tests/positive/Records.juvix +++ b/tests/positive/Records.juvix @@ -36,11 +36,13 @@ open Pair; p4 {A : Type} : Pair A T -> A := fst; -type Bool := false | true; +type Bool := + | false + | true; module Update; - x : Pair Bool Bool := mkPair false false; - - x' : Pair Bool Bool := x @Pair {fst := true}; + x : Pair Bool Bool := mkPair false false; + x' : Pair Bool Bool := x @Pair{fst := fst true}; + -- x' : Pair Bool Bool := λ {(Pair fst0 snd1) := Pair (val1 [ghost ↦ fst0]) (val2)} x @Pair{fst := true}; end; From ce3d3bd748681caf8ee0eefa3e115cff5b636b96 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 31 Jul 2023 12:07:09 +0200 Subject: [PATCH 06/17] record info --- .../Compiler/Concrete/Data/Scope/Base.hs | 8 +++- .../FromParsed/Analysis/Scoping.hs | 39 +++++++++++++------ .../Concrete/Translation/FromSource.hs | 2 + 3 files changed, 36 insertions(+), 13 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs b/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs index 4c4921e0c0..bd39c3b066 100644 --- a/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs +++ b/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs @@ -47,6 +47,11 @@ data ScopeParameters = ScopeParameters _scopeParsedModules :: HashMap TopModulePath (Module 'Parsed 'ModuleTop) } +data RecordInfo = RecordInfo + { _recordInfoConstructor :: S.Symbol, + _recordInfoSignature :: RecordNameSignature + } + data ScoperState = ScoperState { _scoperModulesCache :: ModulesCache, -- | Local and top modules @@ -54,7 +59,7 @@ data ScoperState = ScoperState _scoperScope :: HashMap TopModulePath Scope, _scoperSignatures :: HashMap S.NameId NameSignature, -- | Indexed by the inductive type. This is meant to be used for record updates - _scoperRecordSignatures :: HashMap S.NameId RecordNameSignature + _scoperRecordSignatures :: HashMap S.NameId RecordInfo } data SymbolFixity = SymbolFixity @@ -86,3 +91,4 @@ makeLenses ''SymbolFixity makeLenses ''ScoperState makeLenses ''ScopeParameters makeLenses ''ModulesCache +makeLenses ''RecordInfo diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index f8e5b9d998..a895113ad1 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1019,10 +1019,10 @@ checkSections sec = do i <- reserveInductiveSymbol d constrs <- mapM (reserveConstructorSymbol d) (d ^. inductiveConstructors) void (defineInductiveModule (head constrs) d) - ignoreFail (registerRecord i) + ignoreFail (registerRecord (head constrs) i) where - registerRecord :: S.Symbol -> Sem (Fail ': r') () - registerRecord ind = do + registerRecord :: S.Symbol -> S.Symbol -> Sem (Fail ': r') () + registerRecord mconstr ind = do case d ^. inductiveConstructors of mkRec :| [] -> do fs <- @@ -1031,7 +1031,12 @@ checkSections sec = do ^? constructorRhs . _ConstructorRhsRecord . to mkRecordNameSignature - modify' (set (scoperRecordSignatures . at (ind ^. S.nameId)) (Just fs)) + let info = + RecordInfo + { _recordInfoSignature = fs, + _recordInfoConstructor = mconstr + } + modify' (set (scoperRecordSignatures . at (ind ^. S.nameId)) (Just info)) _ -> fail goDefinition :: Definition 'Parsed -> Sem r' (Definition 'Scoped) @@ -1837,29 +1842,39 @@ checkRecordUpdate :: forall r. Members '[Error ScoperError, State Scope, State S checkRecordUpdate RecordUpdate {..} = do tyName' <- getNameOfKind KNameInductive _recordUpdateTypeName registerName tyName' - sig <- getRecordNameSignature (ScopedIden tyName') + info <- getRecordInfo (ScopedIden tyName') + let sig = info ^. recordInfoSignature fields' <- withLocalScope $ mapM (checkField sig) _recordUpdateFields + let extra' = + RecordUpdateExtra + { _recordUpdateExtraSignature = sig, + _recordUpdateExtraConstructor = info ^. recordInfoConstructor + } return RecordUpdate { _recordUpdateTypeName = ScopedIden tyName', _recordUpdateFields = fields', + _recordUpdateExtra = Irrelevant extra', _recordUpdateAtKw, _recordUpdateDelims } where - -- TODO check repetitions? done by bindvariablesymbol - -- TODO check membership - -- TODO should we do this when translating to internal? + -- TODO check repetitions? done by bindvariablesymbol, but error msg is not that good checkField :: RecordNameSignature -> RecordUpdateField 'Parsed -> Sem r (RecordUpdateField 'Scoped) - checkField _ f = do + checkField sig f = do name' <- bindVariableSymbol (f ^. fieldUpdateName) value' <- checkParseExpressionAtoms (f ^. fieldUpdateValue) + idx' <- maybe (throw unexpectedField) return (sig ^? recordNames . at (f ^. fieldUpdateName) . _Just . _2) return RecordUpdateField { _fieldUpdateName = name', + _fieldUpdateArgIx = idx', _fieldUpdateAssignKw = f ^. fieldUpdateAssignKw, _fieldUpdateValue = value' } + where + unexpectedField :: ScoperError + unexpectedField = error "TODO: unexpected field" checkAmbiguousIterator :: forall r. @@ -1896,12 +1911,12 @@ checkNamedApplication napp = do _argBlockArgs <- mapM checkNamedArg (b ^. argBlockArgs) return ArgumentBlock {..} -getRecordNameSignature :: +getRecordInfo :: forall r. Members '[State ScoperState, Error ScoperError] r => ScopedIden -> - Sem r RecordNameSignature -getRecordNameSignature indTy = + Sem r RecordInfo +getRecordInfo indTy = fromMaybeM err (gets (^. scoperRecordSignatures . at (indTy ^. scopedIden . S.nameId))) where err :: Sem r a diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 78fde87ec7..7d60bcfb8b 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -596,6 +596,7 @@ recordUpdateField = do _fieldUpdateName <- symbol _fieldUpdateAssignKw <- Irrelevant <$> kw kwAssign _fieldUpdateValue <- parseExpressionAtoms + let _fieldUpdateArgIx = () return RecordUpdateField {..} recordUpdate :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (RecordUpdate 'Parsed) @@ -606,6 +607,7 @@ recordUpdate = do _recordUpdateFields <- P.sepEndBy1 recordUpdateField semicolon r <- kw delimBraceR let _recordUpdateDelims = Irrelevant (l, r) + _recordUpdateExtra = Irrelevant () return RecordUpdate {..} expressionAtom :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (ExpressionAtom 'Parsed) From ef00f29e9b188ebe4b22487e03af27128ee825d8 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 31 Jul 2023 12:10:08 +0200 Subject: [PATCH 07/17] fix test --- tests/positive/Records.juvix | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/tests/positive/Records.juvix b/tests/positive/Records.juvix index f5fcca6202..89bb24cf96 100644 --- a/tests/positive/Records.juvix +++ b/tests/positive/Records.juvix @@ -41,8 +41,6 @@ type Bool := | true; module Update; - x : Pair Bool Bool := mkPair false false; - - x' : Pair Bool Bool := x @Pair{fst := fst true}; - -- x' : Pair Bool Bool := λ {(Pair fst0 snd1) := Pair (val1 [ghost ↦ fst0]) (val2)} x @Pair{fst := true}; + f {A B : Type} (p : Pair A B) : Pair Bool B := + p @Pair{fst := true}; end; From ac5fb77aedca3bc17fef3d3372ac02b4ed356871 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 31 Jul 2023 12:29:02 +0200 Subject: [PATCH 08/17] add positive test --- test/Compilation/Positive.hs | 7 ++++++- tests/Compilation/positive/out/test060.out | 1 + tests/Compilation/positive/test060.juvix | 24 ++++++++++++++++++++++ 3 files changed, 31 insertions(+), 1 deletion(-) create mode 100644 tests/Compilation/positive/out/test060.out create mode 100644 tests/Compilation/positive/test060.juvix diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index b8dec6aa2b..ca73df4969 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -354,5 +354,10 @@ tests = "Test059: Builtin list" $(mkRelDir ".") $(mkRelFile "test059.juvix") - $(mkRelFile "out/test059.out") + $(mkRelFile "out/test059.out"), + posTest + "Test060: Record update" + $(mkRelDir ".") + $(mkRelFile "test060.juvix") + $(mkRelFile "out/test060.out") ] diff --git a/tests/Compilation/positive/out/test060.out b/tests/Compilation/positive/out/test060.out new file mode 100644 index 0000000000..cbaa3efc2b --- /dev/null +++ b/tests/Compilation/positive/out/test060.out @@ -0,0 +1 @@ +mkTriple 3 6 2 diff --git a/tests/Compilation/positive/test060.juvix b/tests/Compilation/positive/test060.juvix new file mode 100644 index 0000000000..8146c371c7 --- /dev/null +++ b/tests/Compilation/positive/test060.juvix @@ -0,0 +1,24 @@ +-- record updates +module test060; + +import Stdlib.Data.Nat open; +import Stdlib.System.IO open; + +type Triple (A B C : Type) := + | mkTriple { + fst : A; + snd : B; + thd : C; + }; + +main : Triple Nat Nat Nat; +main := + let + p : Triple Nat Nat Nat := mkTriple 2 2 2; + p' : + Triple Nat Nat Nat := + p @Triple{ + fst := fst + 1; + snd := snd * 3 + }; + in p'; From 0800805060b23d4a84abdbe6c91d4732a52b2cb1 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 31 Jul 2023 12:50:41 +0200 Subject: [PATCH 09/17] parens record update --- src/Juvix/Compiler/Concrete/Language.hs | 13 +++++++ src/Juvix/Compiler/Concrete/Print/Base.hs | 4 ++ .../FromParsed/Analysis/Scoping.hs | 15 ++++--- .../Internal/Translation/FromConcrete.hs | 39 ++++++++++--------- tests/Compilation/positive/out/test060.out | 2 +- tests/Compilation/positive/test060.juvix | 3 +- 6 files changed, 49 insertions(+), 27 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 4483ead3f5..fc8d66a4d0 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -954,6 +954,7 @@ data Expression | ExpressionFunction (Function 'Scoped) | ExpressionHole (HoleType 'Scoped) | ExpressionRecordUpdate RecordUpdateApp + | ExpressionParensRecordUpdate ParensRecordUpdate | ExpressionBraces (WithLoc Expression) | ExpressionIterator (Iterator 'Scoped) | ExpressionNamedApplication (NamedApplication 'Scoped) @@ -1288,6 +1289,11 @@ data RecordUpdateExtra = RecordUpdateExtra } deriving stock (Show) +newtype ParensRecordUpdate = ParensRecordUpdate + { _parensRecordUpdate :: RecordUpdate 'Scoped + } + deriving stock (Show, Eq, Ord) + data RecordUpdate (s :: Stage) = RecordUpdate { _recordUpdateAtKw :: Irrelevant KeywordRef, _recordUpdateDelims :: Irrelevant (KeywordRef, KeywordRef), @@ -1503,6 +1509,7 @@ newtype ModuleIndex = ModuleIndex } makeLenses ''PatternArg +makeLenses ''ParensRecordUpdate makeLenses ''RecordUpdateExtra makeLenses ''RecordUpdate makeLenses ''RecordUpdateApp @@ -1609,6 +1616,7 @@ instance HasAtomicity Expression where ExpressionIterator i -> atomicity i ExpressionNamedApplication i -> atomicity i ExpressionRecordUpdate {} -> Aggregate updateFixity + ExpressionParensRecordUpdate {} -> Atom expressionAtomicity :: forall s. SingI s => ExpressionType s -> Atomicity expressionAtomicity e = case sing :: SStage s of @@ -1730,6 +1738,9 @@ instance SingI s => HasLoc (RecordUpdate s) where instance HasLoc RecordUpdateApp where getLoc r = getLoc (r ^. recordAppExpression) <> getLoc (r ^. recordAppUpdate) +instance HasLoc ParensRecordUpdate where + getLoc = getLoc . (^. parensRecordUpdate) + instance HasLoc Expression where getLoc = \case ExpressionIdentifier i -> getLoc i @@ -1749,6 +1760,7 @@ instance HasLoc Expression where ExpressionIterator i -> getLoc i ExpressionNamedApplication i -> getLoc i ExpressionRecordUpdate i -> getLoc i + ExpressionParensRecordUpdate i -> getLoc i getLocIdentifierType :: forall s. SingI s => IdentifierType s -> Interval getLocIdentifierType e = case sing :: SStage s of @@ -2072,6 +2084,7 @@ instance IsApe Expression ApeLeaf where ExpressionFunction a -> toApe a ExpressionNamedApplication a -> toApe a ExpressionRecordUpdate a -> toApe a + ExpressionParensRecordUpdate {} -> leaf ExpressionParensIdentifier {} -> leaf ExpressionIdentifier {} -> leaf ExpressionList {} -> leaf diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index a7549cdf8f..9cfe68c17f 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -614,6 +614,9 @@ instance PrettyPrint IteratorSyntaxDef where instance PrettyPrint RecordUpdateApp where ppCode = apeHelper +instance PrettyPrint ParensRecordUpdate where + ppCode = parens . ppCode . (^. parensRecordUpdate) + instance PrettyPrint Expression where ppCode = \case ExpressionIdentifier n -> ppCode n @@ -633,6 +636,7 @@ instance PrettyPrint Expression where ExpressionIterator i -> ppCode i ExpressionNamedApplication i -> ppCode i ExpressionRecordUpdate i -> ppCode i + ExpressionParensRecordUpdate i -> ppCode i instance PrettyPrint (WithSource Pragmas) where ppCode pragma = do diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index a895113ad1..410ec9c50f 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -2019,12 +2019,15 @@ checkParens :: ExpressionAtoms 'Parsed -> Sem r Expression checkParens e@(ExpressionAtoms as _) = case as of - AtomIdentifier s :| [] -> do - scopedId <- checkName s - let scopedIdenNoFix = over scopedIden (set S.nameFixity Nothing) scopedId - return (ExpressionParensIdentifier scopedIdenNoFix) - AtomIterator i :| [] -> ExpressionIterator . set iteratorParens True <$> checkIterator i - AtomCase c :| [] -> ExpressionCase . set caseParens True <$> checkCase c + p :| [] -> case p of + AtomIdentifier s -> do + scopedId <- checkName s + let scopedIdenNoFix = over scopedIden (set S.nameFixity Nothing) scopedId + return (ExpressionParensIdentifier scopedIdenNoFix) + AtomIterator i -> ExpressionIterator . set iteratorParens True <$> checkIterator i + AtomCase c -> ExpressionCase . set caseParens True <$> checkCase c + AtomRecordUpdate u -> ExpressionParensRecordUpdate . ParensRecordUpdate <$> checkRecordUpdate u + _ -> checkParseExpressionAtoms e _ -> checkParseExpressionAtoms e checkExpressionAtoms :: diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 7b26ba83a1..b8740ea61e 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -807,6 +807,7 @@ goExpression = \case ExpressionIterator i -> goIterator i ExpressionNamedApplication i -> goNamedApplication i ExpressionRecordUpdate i -> goRecordUpdateApp i + ExpressionParensRecordUpdate i -> Internal.ExpressionLambda <$> goRecordUpdate (i ^. parensRecordUpdate) where goNamedApplication :: Concrete.NamedApplication 'Scoped -> Sem r Internal.Expression goNamedApplication = runNamedArguments >=> goExpression @@ -832,25 +833,25 @@ goExpression = \case mkArgs :: [Indexed Internal.VarName] -> Sem r [Internal.Expression] mkArgs = execOutputList . go (uncurry Indexed <$> IntMap.toAscList fieldMap) - where - go :: [Indexed (RecordUpdateField 'Scoped)] -> [Indexed Internal.VarName] -> Sem (Output Internal.Expression ': r) () - go fields = \case - [] -> return () - Indexed idx var : vars' -> case getArg idx of - Nothing -> do - output (Internal.toExpression var) - go fields vars' - Just (arg, fields') -> do - let fieldVar = goSymbol (arg ^. fieldUpdateName) - val' <- goExpression (arg ^. fieldUpdateValue) - output (Internal.renameVar fieldVar var val') - go fields' vars' - where - getArg :: Int -> Maybe (RecordUpdateField 'Scoped, [Indexed (RecordUpdateField 'Scoped)]) - getArg idx = do - Indexed fidx arg :| fs <- nonEmpty fields - guard (idx == fidx) - return (arg, fs) + where + go :: [Indexed (RecordUpdateField 'Scoped)] -> [Indexed Internal.VarName] -> Sem (Output Internal.Expression ': r) () + go fields = \case + [] -> return () + Indexed idx var : vars' -> case getArg idx of + Nothing -> do + output (Internal.toExpression var) + go fields vars' + Just (arg, fields') -> do + let fieldVar = goSymbol (arg ^. fieldUpdateName) + val' <- goExpression (arg ^. fieldUpdateValue) + output (Internal.renameVar fieldVar var val') + go fields' vars' + where + getArg :: Int -> Maybe (RecordUpdateField 'Scoped, [Indexed (RecordUpdateField 'Scoped)]) + getArg idx = do + Indexed fidx arg :| fs <- nonEmpty fields + guard (idx == fidx) + return (arg, fs) mkClause :: Sem r Internal.LambdaClause mkClause = do diff --git a/tests/Compilation/positive/out/test060.out b/tests/Compilation/positive/out/test060.out index cbaa3efc2b..9cf9bd99f6 100644 --- a/tests/Compilation/positive/out/test060.out +++ b/tests/Compilation/positive/out/test060.out @@ -1 +1 @@ -mkTriple 3 6 2 +mkTriple 30 6 2 diff --git a/tests/Compilation/positive/test060.juvix b/tests/Compilation/positive/test060.juvix index 8146c371c7..2d9bb04617 100644 --- a/tests/Compilation/positive/test060.juvix +++ b/tests/Compilation/positive/test060.juvix @@ -21,4 +21,5 @@ main := fst := fst + 1; snd := snd * 3 }; - in p'; + f : Triple Nat Nat Nat -> Triple Nat Nat Nat := (@Triple {fst := fst * 10}); + in f p'; From 83b75a13dab1e1a83b362fc0c2ba4183b3482487 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 31 Jul 2023 16:09:20 +0200 Subject: [PATCH 10/17] fix typo --- test/Scope/Negative.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index f8da35c574..e5637f1d49 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -321,6 +321,6 @@ scoperErrorTests = $(mkRelDir ".") $(mkRelFile "NoNamedArguments.juvix") $ \case - ErrNoNameSignature ErrNoNameSignature {} -> Nothing + ErrNoNameSignature NoNameSignature {} -> Nothing _ -> wrongError ] From 94a4cac40b62ebe0b52ea16794e04b488871bdf0 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Tue, 1 Aug 2023 17:41:39 +0100 Subject: [PATCH 11/17] Add a negative scope test for ErrNotARecord --- test/Scope/Negative.hs | 7 +++++++ tests/negative/NotARecord.juvix | 6 ++++++ 2 files changed, 13 insertions(+) create mode 100644 tests/negative/NotARecord.juvix diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index e5637f1d49..d01f2a3520 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -322,5 +322,12 @@ scoperErrorTests = $(mkRelFile "NoNamedArguments.juvix") $ \case ErrNoNameSignature NoNameSignature {} -> Nothing + _ -> wrongError, + NegTest + "Not a record" + $(mkRelDir ".") + $(mkRelFile "NotARecord.juvix") + $ \case + ErrNotARecord NotARecord {} -> Nothing _ -> wrongError ] diff --git a/tests/negative/NotARecord.juvix b/tests/negative/NotARecord.juvix new file mode 100644 index 0000000000..cdc8ca4f2a --- /dev/null +++ b/tests/negative/NotARecord.juvix @@ -0,0 +1,6 @@ +module NotARecord; + +type T := t; + +f : T; +f := t @T{x := 1}; From a66e6cedbd41af4cf87374cb058d9089d761693a Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 3 Aug 2023 19:07:47 +0200 Subject: [PATCH 12/17] add unexpected field error --- .../FromParsed/Analysis/Scoping.hs | 4 ++-- .../FromParsed/Analysis/Scoping/Error.hs | 2 ++ .../Analysis/Scoping/Error/Types.hs | 21 +++++++++++++++++++ test/Scope/Negative.hs | 7 +++++++ tests/negative/UnexpectedField.juvix | 10 +++++++++ 5 files changed, 42 insertions(+), 2 deletions(-) create mode 100644 tests/negative/UnexpectedField.juvix diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index f79d39ead3..6c6a23ffcc 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1857,7 +1857,7 @@ checkRecordUpdate RecordUpdate {..} = do _recordUpdateDelims } where - -- TODO check repetitions? done by bindvariablesymbol, but error msg is not that good + -- TODO checking repetitions is done by bindVariableSymbol, but error msg is not that good checkField :: RecordNameSignature -> RecordUpdateField 'Parsed -> Sem r (RecordUpdateField 'Scoped) checkField sig f = do name' <- bindVariableSymbol (f ^. fieldUpdateName) @@ -1872,7 +1872,7 @@ checkRecordUpdate RecordUpdate {..} = do } where unexpectedField :: ScoperError - unexpectedField = error "TODO: unexpected field" + unexpectedField = ErrUnexpectedField (UnexpectedField (f ^. fieldUpdateName)) checkNamedApplication :: forall r. 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 28bb38afef..bbc847feb9 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs @@ -43,6 +43,7 @@ data ScoperError | ErrNoNameSignature NoNameSignature | ErrNamedArgumentsError NamedArgumentsError | ErrNotARecord NotARecord + | ErrUnexpectedField UnexpectedField instance ToGenericError ScoperError where genericError = \case @@ -77,3 +78,4 @@ instance ToGenericError ScoperError where ErrNoNameSignature e -> genericError e ErrNamedArgumentsError e -> genericError e ErrNotARecord e -> genericError e + ErrUnexpectedField 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 05ecfb37c1..6d26dc4711 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 @@ -788,3 +788,24 @@ instance ToGenericError NotARecord where where i :: Interval i = getLoc _notARecord + +newtype UnexpectedField = UnexpectedField + { _unexpectedField :: Symbol + } + deriving stock (Show) + +instance ToGenericError UnexpectedField where + genericError UnexpectedField {..} = do + opts <- fromGenericOptions <$> ask + let msg = + "Unexpected field" + <+> ppCode opts _unexpectedField + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = mkAnsiText msg, + _genericErrorIntervals = [i] + } + where + i :: Interval + i = getLoc _unexpectedField diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index d01f2a3520..86eb6d7cb8 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -329,5 +329,12 @@ scoperErrorTests = $(mkRelFile "NotARecord.juvix") $ \case ErrNotARecord NotARecord {} -> Nothing + _ -> wrongError, + NegTest + "Unexpected field in record update" + $(mkRelDir ".") + $(mkRelFile "UnexpectedFieldUpdate.juvix") + $ \case + ErrUnexpectedField UnexpectedField {} -> Nothing _ -> wrongError ] diff --git a/tests/negative/UnexpectedField.juvix b/tests/negative/UnexpectedField.juvix new file mode 100644 index 0000000000..3c7680e14a --- /dev/null +++ b/tests/negative/UnexpectedField.juvix @@ -0,0 +1,10 @@ +module UnexpectedField; + +type T := t; + +type R := mkR { + r : T; +}; + +f : R; +f := (mkR t) @R{x := 1}; From 5a1fac91ce18e231dbc3a916dbb9655456c08616 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 3 Aug 2023 19:47:27 +0200 Subject: [PATCH 13/17] rename test --- .../{UnexpectedField.juvix => UnexpectedFieldUpdate.juvix} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename tests/negative/{UnexpectedField.juvix => UnexpectedFieldUpdate.juvix} (71%) diff --git a/tests/negative/UnexpectedField.juvix b/tests/negative/UnexpectedFieldUpdate.juvix similarity index 71% rename from tests/negative/UnexpectedField.juvix rename to tests/negative/UnexpectedFieldUpdate.juvix index 3c7680e14a..ecee0e04f7 100644 --- a/tests/negative/UnexpectedField.juvix +++ b/tests/negative/UnexpectedFieldUpdate.juvix @@ -1,4 +1,4 @@ -module UnexpectedField; +module UnexpectedFieldUpdate; type T := t; From 0dcf80f886eeb4255971402de9cf24fd2eaf8304 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 4 Aug 2023 17:29:15 +0200 Subject: [PATCH 14/17] bind all fields --- src/Juvix/Compiler/Concrete/Extra.hs | 6 ++++ src/Juvix/Compiler/Concrete/Language.hs | 4 ++- .../FromParsed/Analysis/Scoping.hs | 11 +++--- .../FromParsed/Analysis/Scoping/Error.hs | 2 ++ .../Analysis/Scoping/Error/Types.hs | 21 +++++++++++ src/Juvix/Compiler/Internal/Extra.hs | 31 ++++++++-------- .../Internal/Translation/FromConcrete.hs | 35 +++++++++++-------- 7 files changed, 74 insertions(+), 36 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs index ddfff65665..e31763e1bf 100644 --- a/src/Juvix/Compiler/Concrete/Extra.hs +++ b/src/Juvix/Compiler/Concrete/Extra.hs @@ -7,11 +7,14 @@ module Juvix.Compiler.Concrete.Extra groupStatements, flattenStatement, migrateFunctionSyntax, + recordNameSignatureByIndex, ) where import Data.HashMap.Strict qualified as HashMap +import Data.IntMap.Strict qualified as IntMap import Data.List.NonEmpty qualified as NonEmpty +import Juvix.Compiler.Concrete.Data.NameSignature.Base import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Keywords import Juvix.Compiler.Concrete.Language @@ -191,3 +194,6 @@ migrateFunctionSyntax m = over moduleBody (mapMaybe goStatement) m } getClauses :: S.Symbol -> [FunctionClause 'Scoped] getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction] + +recordNameSignatureByIndex :: RecordNameSignature -> IntMap Symbol +recordNameSignatureByIndex = IntMap.fromList . (^.. recordNames . each . to swap) diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index b5aa1cdbc6..572b5db768 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -411,7 +411,7 @@ deriving stock instance Ord (ConstructorDef 'Parsed) deriving stock instance Ord (ConstructorDef 'Scoped) data RecordUpdateField (s :: Stage) = RecordUpdateField - { _fieldUpdateName :: SymbolType s, + { _fieldUpdateName :: Symbol, _fieldUpdateArgIx :: FieldUpdateArgIxType s, _fieldUpdateAssignKw :: Irrelevant (KeywordRef), _fieldUpdateValue :: ExpressionType s @@ -1266,6 +1266,8 @@ deriving stock instance Ord (ArgumentBlock 'Scoped) data RecordUpdateExtra = RecordUpdateExtra { _recordUpdateExtraConstructor :: S.Symbol, + -- | Implicitly bound fields sorted by index + _recordUpdateExtraVars :: [S.Symbol], _recordUpdateExtraSignature :: RecordNameSignature } deriving stock (Show) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 6c6a23ffcc..4a90b7d242 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -15,6 +15,7 @@ import Juvix.Compiler.Concrete.Data.Name qualified as N import Juvix.Compiler.Concrete.Data.NameSignature import Juvix.Compiler.Concrete.Data.Scope import Juvix.Compiler.Concrete.Data.ScopedName qualified as S +import Juvix.Compiler.Concrete.Extra (recordNameSignatureByIndex) import Juvix.Compiler.Concrete.Extra qualified as P import Juvix.Compiler.Concrete.Gen qualified as G import Juvix.Compiler.Concrete.Language @@ -1842,10 +1843,14 @@ checkRecordUpdate RecordUpdate {..} = do registerName tyName' info <- getRecordInfo (ScopedIden tyName') let sig = info ^. recordInfoSignature - fields' <- withLocalScope $ mapM (checkField sig) _recordUpdateFields + (vars', fields') <- withLocalScope $ do + vs <- mapM bindVariableSymbol (toList (recordNameSignatureByIndex sig)) + fs <- mapM (checkField sig) _recordUpdateFields + return (vs, fs) let extra' = RecordUpdateExtra { _recordUpdateExtraSignature = sig, + _recordUpdateExtraVars = vars', _recordUpdateExtraConstructor = info ^. recordInfoConstructor } return @@ -1857,15 +1862,13 @@ checkRecordUpdate RecordUpdate {..} = do _recordUpdateDelims } where - -- TODO checking repetitions is done by bindVariableSymbol, but error msg is not that good checkField :: RecordNameSignature -> RecordUpdateField 'Parsed -> Sem r (RecordUpdateField 'Scoped) checkField sig f = do - name' <- bindVariableSymbol (f ^. fieldUpdateName) value' <- checkParseExpressionAtoms (f ^. fieldUpdateValue) idx' <- maybe (throw unexpectedField) return (sig ^? recordNames . at (f ^. fieldUpdateName) . _Just . _2) return RecordUpdateField - { _fieldUpdateName = name', + { _fieldUpdateName = f ^. fieldUpdateName, _fieldUpdateArgIx = idx', _fieldUpdateAssignKw = f ^. fieldUpdateAssignKw, _fieldUpdateValue = value' 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 bbc847feb9..d8e698e05e 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs @@ -44,6 +44,7 @@ data ScoperError | ErrNamedArgumentsError NamedArgumentsError | ErrNotARecord NotARecord | ErrUnexpectedField UnexpectedField + | ErrRepeatedField RepeatedField instance ToGenericError ScoperError where genericError = \case @@ -79,3 +80,4 @@ instance ToGenericError ScoperError where ErrNamedArgumentsError e -> genericError e ErrNotARecord e -> genericError e ErrUnexpectedField e -> genericError e + ErrRepeatedField 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 6d26dc4711..5509390f98 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 @@ -809,3 +809,24 @@ instance ToGenericError UnexpectedField where where i :: Interval i = getLoc _unexpectedField + +newtype RepeatedField = RepeatedField + { _repeatedField :: Symbol + } + deriving stock (Show) + +instance ToGenericError RepeatedField where + genericError RepeatedField {..} = do + opts <- fromGenericOptions <$> ask + let msg = + "Repeated field" + <+> ppCode opts _repeatedField + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = mkAnsiText msg, + _genericErrorIntervals = [i] + } + where + i :: Interval + i = getLoc _repeatedField diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index 975ee116b1..30aece2f1a 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -256,9 +256,6 @@ unnamedParameter ty = singletonRename :: VarName -> VarName -> Rename singletonRename = HashMap.singleton -renameVar :: VarName -> VarName -> Expression -> Expression -renameVar a b = substitutionE (renameToSubsE (singletonRename a b)) - renameToSubsE :: Rename -> SubsE renameToSubsE = fmap (ExpressionIden . IdenVar) @@ -717,19 +714,21 @@ genConstructorPattern loc info = genConstructorPattern' loc (info ^. constructor genConstructorPattern' :: Members '[NameIdGen] r => Interval -> Name -> Int -> Sem r (PatternArg, [VarName]) genConstructorPattern' loc cname cargs = do vars <- mapM (freshVar loc) (Stream.take cargs allWords) - let app = - ConstructorApp - { _constrAppConstructor = cname, - _constrAppParameters = map (patternArgFromVar Explicit) vars, - _constrAppType = Nothing - } - pat = - PatternArg - { _patternArgIsImplicit = Explicit, - _patternArgName = Nothing, - _patternArgPattern = PatternConstructorApp app - } - return (pat, vars) + return (mkConstructorVarPattern cname vars, vars) + +mkConstructorVarPattern :: Name -> [VarName] -> PatternArg +mkConstructorVarPattern c vars = + PatternArg + { _patternArgIsImplicit = Explicit, + _patternArgName = Nothing, + _patternArgPattern = + PatternConstructorApp + ConstructorApp + { _constrAppConstructor = c, + _constrAppType = Nothing, + _constrAppParameters = map (patternArgFromVar Explicit) vars + } + } -- | Assumes the constructor does not have implicit arguments (which is not -- allowed at the moment). diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index b8740ea61e..75afb74d75 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -8,7 +8,6 @@ import Data.HashMap.Strict qualified as HashMap import Data.IntMap.Strict qualified as IntMap import Data.List.NonEmpty qualified as NonEmpty import Juvix.Compiler.Builtins -import Juvix.Compiler.Concrete.Data.NameSignature.Base import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Extra qualified as Concrete import Juvix.Compiler.Concrete.Language qualified as Concrete @@ -821,18 +820,24 @@ goExpression = \case _lambdaClauses = pure cl } where - numFields = length (r ^. recordUpdateExtra . unIrrelevant . recordUpdateExtraSignature . recordNames) - -- fields indexed by field index. - fieldMap :: IntMap (RecordUpdateField 'Scoped) - fieldMap = - IntMap.fromList - [ (f ^. fieldUpdateArgIx, f) - | f <- r ^.. recordUpdateFields . each - ] + mkFieldmap :: Sem r (IntMap (RecordUpdateField 'Scoped)) + mkFieldmap = execState mempty $ mapM go (r ^. recordUpdateFields) + where + go :: RecordUpdateField 'Scoped -> Sem (State (IntMap (RecordUpdateField 'Scoped)) ': r) () + go f = do + let idx = f ^. fieldUpdateArgIx + whenM (gets @(IntMap (RecordUpdateField 'Scoped)) (IntMap.member idx)) (throw repeated) + modify' (IntMap.insert idx f) + where + repeated :: ScoperError + repeated = undefined mkArgs :: [Indexed Internal.VarName] -> Sem r [Internal.Expression] - mkArgs = execOutputList . go (uncurry Indexed <$> IntMap.toAscList fieldMap) + mkArgs vs = do + fieldMap <- mkFieldmap + execOutputList $ + go (uncurry Indexed <$> IntMap.toAscList fieldMap) vs where go :: [Indexed (RecordUpdateField 'Scoped)] -> [Indexed Internal.VarName] -> Sem (Output Internal.Expression ': r) () go fields = \case @@ -842,9 +847,8 @@ goExpression = \case output (Internal.toExpression var) go fields vars' Just (arg, fields') -> do - let fieldVar = goSymbol (arg ^. fieldUpdateName) val' <- goExpression (arg ^. fieldUpdateValue) - output (Internal.renameVar fieldVar var val') + output val' go fields' vars' where getArg :: Int -> Maybe (RecordUpdateField 'Scoped, [Indexed (RecordUpdateField 'Scoped)]) @@ -855,9 +859,10 @@ goExpression = \case mkClause :: Sem r Internal.LambdaClause mkClause = do - let loc = getLoc r - constr = goSymbol (r ^. recordUpdateExtra . unIrrelevant . recordUpdateExtraConstructor) - (patArg, vars) <- Internal.genConstructorPattern' loc constr numFields + let extra = r ^. recordUpdateExtra . unIrrelevant + constr = goSymbol (extra ^. recordUpdateExtraConstructor) + vars = map goSymbol (extra ^. recordUpdateExtraVars) + patArg = Internal.mkConstructorVarPattern constr vars args <- mkArgs (indexFrom 0 vars) return Internal.LambdaClause From 0f0ff248d27fb926acc8e25d89bc89484eac56bb Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 4 Aug 2023 17:38:08 +0200 Subject: [PATCH 15/17] test --- .../Compiler/Internal/Translation/FromConcrete.hs | 2 +- test/Typecheck/Positive.hs | 4 ++++ tests/positive/Records2.juvix | 15 +++++++++++++++ 3 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 tests/positive/Records2.juvix diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 75afb74d75..40c4ab00ab 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -831,7 +831,7 @@ goExpression = \case modify' (IntMap.insert idx f) where repeated :: ScoperError - repeated = undefined + repeated = ErrRepeatedField (RepeatedField (f ^. fieldUpdateName)) mkArgs :: [Indexed Internal.VarName] -> Sem r [Internal.Expression] mkArgs vs = do diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs index 7a97964193..6a6cc4bab8 100644 --- a/test/Typecheck/Positive.hs +++ b/test/Typecheck/Positive.hs @@ -253,6 +253,10 @@ tests = "Record declaration" $(mkRelDir ".") $(mkRelFile "Records.juvix"), + posTest + "Record update" + $(mkRelDir ".") + $(mkRelFile "Records2.juvix"), posTest "Record projections" $(mkRelDir ".") diff --git a/tests/positive/Records2.juvix b/tests/positive/Records2.juvix new file mode 100644 index 0000000000..1f34b74fa8 --- /dev/null +++ b/tests/positive/Records2.juvix @@ -0,0 +1,15 @@ +module Records2; + +import Stdlib.Data.Nat.Base open; + +type Pair (A B : Type) := + | mkPair { + pfst : A; + psnd : B + }; + +main : Pair Nat Nat; +main := + let + p : Pair Nat Nat := mkPair 2 2; + in p @Pair{pfst := pfst + psnd}; From 082321e3ad4ea7ba08632177d5d1b53f198df118 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 4 Aug 2023 17:45:43 +0200 Subject: [PATCH 16/17] ormolu --- src/Juvix/Compiler/Internal/Translation/FromConcrete.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 40c4ab00ab..1a4a0fca7b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -830,8 +830,8 @@ goExpression = \case whenM (gets @(IntMap (RecordUpdateField 'Scoped)) (IntMap.member idx)) (throw repeated) modify' (IntMap.insert idx f) where - repeated :: ScoperError - repeated = ErrRepeatedField (RepeatedField (f ^. fieldUpdateName)) + repeated :: ScoperError + repeated = ErrRepeatedField (RepeatedField (f ^. fieldUpdateName)) mkArgs :: [Indexed Internal.VarName] -> Sem r [Internal.Expression] mkArgs vs = do From 78e16b851f5e2c625288b3471241d57997ce34d8 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 7 Aug 2023 11:14:13 +0200 Subject: [PATCH 17/17] update test --- tests/Compilation/positive/out/test060.out | 2 +- tests/Compilation/positive/test060.juvix | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/Compilation/positive/out/test060.out b/tests/Compilation/positive/out/test060.out index 9cf9bd99f6..58abf6b064 100644 --- a/tests/Compilation/positive/out/test060.out +++ b/tests/Compilation/positive/out/test060.out @@ -1 +1 @@ -mkTriple 30 6 2 +mkTriple 30 10 2 diff --git a/tests/Compilation/positive/test060.juvix b/tests/Compilation/positive/test060.juvix index 2d9bb04617..c1d2609193 100644 --- a/tests/Compilation/positive/test060.juvix +++ b/tests/Compilation/positive/test060.juvix @@ -19,7 +19,7 @@ main := Triple Nat Nat Nat := p @Triple{ fst := fst + 1; - snd := snd * 3 + snd := snd * 3 + thd + fst }; f : Triple Nat Nat Nat -> Triple Nat Nat Nat := (@Triple {fst := fst * 10}); in f p';