From 1e9850c8f54bb19ae5ceb04e11578fbb70929985 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 29 Jul 2024 18:44:16 +0200 Subject: [PATCH] Allow instance field declarations (#2916) - Closes #2897 --------- Co-authored-by: Lukasz Czajka --- .../Concrete/Data/NameSignature/Builder.hs | 16 +++-- src/Juvix/Compiler/Concrete/Extra.hs | 8 +-- src/Juvix/Compiler/Concrete/Language/Base.hs | 5 +- src/Juvix/Compiler/Concrete/Print/Base.hs | 6 +- .../FromParsed/Analysis/Scoping.hs | 16 ++++- .../Concrete/Translation/FromSource.hs | 18 +++++ src/Juvix/Compiler/Internal/Data/InfoTable.hs | 2 +- src/Juvix/Compiler/Internal/Extra.hs | 72 ++++++++++++------- src/Juvix/Compiler/Internal/Extra/Base.hs | 6 +- .../Internal/Translation/FromConcrete.hs | 41 +++++++---- .../Analysis/Positivity/Checker.hs | 10 +-- .../Analysis/TypeChecking/CheckerNew.hs | 16 ++--- src/Juvix/Data.hs | 2 + src/Juvix/Data/InstanceHole.hs | 6 +- src/Juvix/Data/IsImplicit.hs | 21 ++++++ src/Juvix/Data/ProjectionKind.hs | 10 +++ src/Juvix/Prelude/Base/Foundation.hs | 10 ++- tests/positive/Internal/InstanceFields.juvix | 28 ++++++++ tests/positive/Isabelle/isabelle/Program.thy | 4 +- 19 files changed, 220 insertions(+), 77 deletions(-) create mode 100644 src/Juvix/Data/ProjectionKind.hs create mode 100644 tests/positive/Internal/InstanceFields.juvix diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index 7aef6d8a72..1bd9bcd77e 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -10,7 +10,6 @@ module Juvix.Compiler.Concrete.Data.NameSignature.Builder ) where -import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Concrete.Data.NameSignature.Error import Juvix.Compiler.Concrete.Extra (symbolParsed) import Juvix.Compiler.Concrete.Gen qualified as Gen @@ -215,6 +214,7 @@ addSymbol' impl mdef sym ty = do NameItem { _nameItemDefault = mdef, _nameItemSymbol = sym, + _nameItemImplicit = impl, _nameItemIndex = idx, _nameItemType = ty } @@ -241,10 +241,16 @@ endBuild' = get @(BuilderState s) >>= throw mkRecordNameSignature :: forall s. (SingI s) => RhsRecord s -> RecordNameSignature s mkRecordNameSignature rhs = RecordNameSignature $ - HashMap.fromList - [ (symbolParsed _nameItemSymbol, NameItem {..}) + hashMap + [ ( symbolParsed _nameItemSymbol, + NameItem + { _nameItemSymbol, + _nameItemIndex, + _nameItemType = field ^. fieldType, + _nameItemImplicit = fromIsImplicitField (field ^. fieldIsImplicit), + _nameItemDefault = Nothing + } + ) | (Indexed _nameItemIndex field) <- indexFrom 0 (toList (rhs ^.. rhsRecordStatements . each . _RecordStatementField)), let _nameItemSymbol :: SymbolType s = field ^. fieldName - _nameItemType = field ^. fieldType - _nameItemDefault :: Maybe (ArgDefault s) = Nothing ] diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs index 941f2f2278..4fb7baf8f5 100644 --- a/src/Juvix/Compiler/Concrete/Extra.hs +++ b/src/Juvix/Compiler/Concrete/Extra.hs @@ -12,7 +12,6 @@ module Juvix.Compiler.Concrete.Extra ) where -import Data.IntMap.Strict qualified as IntMap import Data.List.NonEmpty qualified as NonEmpty import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Language @@ -93,11 +92,8 @@ flattenStatement = \case StatementModule m -> concatMap flattenStatement (m ^. moduleBody) s -> [s] -recordNameSignatureByIndex :: forall s. (SingI s) => RecordNameSignature s -> IntMap Symbol -recordNameSignatureByIndex = IntMap.fromList . (^.. recordNames . each . to mkAssoc) - where - mkAssoc :: NameItem s -> (Int, Symbol) - mkAssoc NameItem {..} = (_nameItemIndex, symbolParsed _nameItemSymbol) +recordNameSignatureByIndex :: RecordNameSignature s -> IntMap (NameItem s) +recordNameSignatureByIndex = indexedByInt (^. nameItemIndex) . (^. recordNames) getExpressionAtomIden :: ExpressionAtom 'Scoped -> Maybe S.Name getExpressionAtomIden = \case diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs index 22a62d8926..806ddbd19b 100644 --- a/src/Juvix/Compiler/Concrete/Language/Base.hs +++ b/src/Juvix/Compiler/Concrete/Language/Base.hs @@ -158,6 +158,7 @@ type ParsedPragmas = WithLoc (WithSource Pragmas) data NameItem (s :: Stage) = NameItem { _nameItemSymbol :: SymbolType s, _nameItemIndex :: Int, + _nameItemImplicit :: IsImplicit, _nameItemType :: ExpressionType s, _nameItemDefault :: Maybe (ArgDefault s) } @@ -304,6 +305,7 @@ deriving stock instance Ord (Statement 'Scoped) data ProjectionDef s = ProjectionDef { _projectionConstructor :: S.Symbol, _projectionField :: SymbolType s, + _projectionKind :: ProjectionKind, _projectionFieldIx :: Int, _projectionFieldBuiltin :: Maybe (WithLoc BuiltinFunction), _projectionDoc :: Maybe (Judoc s), @@ -734,6 +736,7 @@ deriving stock instance Ord (RecordUpdateField 'Scoped) data RecordField (s :: Stage) = RecordField { _fieldName :: SymbolType s, + _fieldIsImplicit :: IsImplicitField, _fieldColon :: Irrelevant (KeywordRef), _fieldType :: ExpressionType s, _fieldBuiltin :: Maybe (WithLoc BuiltinFunction), @@ -2210,7 +2213,7 @@ deriving stock instance Ord (ArgumentBlock 'Scoped) data RecordUpdateExtra = RecordUpdateExtra { _recordUpdateExtraConstructor :: S.Symbol, -- | Implicitly bound fields sorted by index - _recordUpdateExtraVars :: [S.Symbol] + _recordUpdateExtraVars :: IntMap (IsImplicit, S.Symbol) } deriving stock (Generic) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index f68beab04b..f290170bc8 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -1298,10 +1298,14 @@ instance (SingI s) => PrettyPrint (RecordField s) where let doc' = ppCode <$> _fieldDoc pragmas' = ppCode <$> _fieldPragmas builtin' = (<> line) . ppCode <$> _fieldBuiltin + mayBraces :: forall r'. (Members '[ExactPrint] r') => Sem r' () -> Sem r' () + mayBraces = case _fieldIsImplicit of + ExplicitField -> id + ImplicitInstanceField -> doubleBraces doc' ?<> pragmas' ?<> builtin' - ?<> ppSymbolType _fieldName + ?<> mayBraces (ppSymbolType _fieldName) <+> ppCode _fieldColon <+> ppExpressionType _fieldType diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 8405927e1f..ab94a02fe2 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -170,6 +170,7 @@ checkProjectionDef p = do _projectionConstructor = p ^. projectionConstructor, _projectionFieldBuiltin = p ^. projectionFieldBuiltin, _projectionPragmas = p ^. projectionPragmas, + _projectionKind = p ^. projectionKind, _projectionField, _projectionDoc } @@ -1643,10 +1644,16 @@ checkSections sec = topBindings helper { _projectionConstructor = headConstr, _projectionField = field ^. fieldName, _projectionFieldIx = idx, + _projectionKind = kind, _projectionFieldBuiltin = field ^. fieldBuiltin, _projectionDoc = field ^. fieldDoc, _projectionPragmas = field ^. fieldPragmas } + where + kind :: ProjectionKind + kind = case field ^. fieldIsImplicit of + ExplicitField -> ProjectionExplicit + ImplicitInstanceField -> ProjectionCoercion getFields :: Sem (Fail ': s') [RecordStatement 'Parsed] getFields = case i ^. inductiveConstructors of @@ -2665,8 +2672,8 @@ checkRecordUpdate RecordUpdate {..} = do tyName' <- getNameOfKind KNameInductive _recordUpdateTypeName info <- getRecordInfo tyName' let sig = info ^. recordInfoSignature - (vars', fields') <- withLocalScope $ do - vs <- mapM bindVariableSymbol (toList (recordNameSignatureByIndex sig)) + (vars' :: IntMap (IsImplicit, S.Symbol), fields') <- withLocalScope $ do + vs <- mapM bindRecordUpdateVariable (recordNameSignatureByIndex sig) fs <- mapM (checkUpdateField sig) _recordUpdateFields return (vs, fs) let extra' = @@ -2682,6 +2689,11 @@ checkRecordUpdate RecordUpdate {..} = do _recordUpdateAtKw, _recordUpdateDelims } + where + bindRecordUpdateVariable :: NameItem 'Parsed -> Sem r (IsImplicit, S.Symbol) + bindRecordUpdateVariable NameItem {..} = do + v <- bindVariableSymbol _nameItemSymbol + return (_nameItemImplicit, v) checkUpdateField :: (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 83931fe3ec..005711b7d9 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -1409,12 +1409,27 @@ axiomDef _axiomBuiltin = do -- Function expression -------------------------------------------------------------------------------- +implicitOpenField :: + (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => + ParsecS r (KeywordRef, IsImplicitField) +implicitOpenField = + (,ImplicitInstanceField) <$> kw delimDoubleBraceL + <|> (,ExplicitField) <$> kw delimParenL + implicitOpen :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (KeywordRef, IsImplicit) implicitOpen = (,ImplicitInstance) <$> kw delimDoubleBraceL <|> (,Implicit) <$> kw delimBraceL <|> (,Explicit) <$> kw delimParenL +implicitCloseField :: + (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => + IsImplicitField -> + ParsecS r KeywordRef +implicitCloseField = \case + ExplicitField -> kw delimParenR + ImplicitInstanceField -> kw delimDoubleBraceR + implicitClose :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => IsImplicit -> ParsecS r KeywordRef implicitClose = \case Implicit -> kw delimBraceR @@ -1529,7 +1544,10 @@ recordField = do _fieldDoc <- optional stashJudoc >> getJudoc _fieldPragmas <- optional stashPragmas >> getPragmas _fieldBuiltin <- optional builtinRecordField + mayImpl <- optional (snd <$> implicitOpenField) _fieldName <- symbol + whenJust mayImpl (void . implicitCloseField) + let _fieldIsImplicit = fromMaybe ExplicitField mayImpl _fieldColon <- Irrelevant <$> kw kwColon _fieldType <- parseExpressionAtoms return RecordField {..} diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index ead8de0b89..5b04c73950 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -190,7 +190,7 @@ lookupConstructor f = do <> "\nThe registered constructors are: " <> ppTrace (HashMap.keys tbl) -lookupConstructorArgTypes :: (Member (Reader InfoTable) r) => Name -> Sem r ([InductiveParameter], [Expression]) +lookupConstructorArgTypes :: (Member (Reader InfoTable) r) => Name -> Sem r ([InductiveParameter], [FunctionParameter]) lookupConstructorArgTypes = fmap constructorArgTypes . lookupConstructor lookupInductive :: forall r. (Member (Reader InfoTable) r) => InductiveName -> Sem r InductiveInfo diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index a42aaf1e48..524e807ac4 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -7,7 +7,6 @@ module Juvix.Compiler.Internal.Extra where import Data.HashMap.Strict qualified as HashMap -import Data.Stream qualified as Stream import Juvix.Compiler.Internal.Extra.Base import Juvix.Compiler.Internal.Extra.Clonable import Juvix.Compiler.Internal.Extra.DependencyBuilder @@ -15,7 +14,7 @@ import Juvix.Compiler.Internal.Language import Juvix.Compiler.Store.Internal.Data.InfoTable import Juvix.Prelude -constructorArgTypes :: ConstructorInfo -> ([InductiveParameter], [Expression]) +constructorArgTypes :: ConstructorInfo -> ([InductiveParameter], [FunctionParameter]) constructorArgTypes i = ( i ^. constructorInfoInductiveParameters, constructorArgs (i ^. constructorInfoType) @@ -42,7 +41,7 @@ constructorType info = let (inductiveParams, constrArgs) = constructorArgTypes info args = map inductiveToFunctionParam inductiveParams - ++ map unnamedParameter constrArgs + ++ constrArgs saturatedTy = constructorReturnType info in foldFunType args saturatedTy @@ -54,10 +53,6 @@ inductiveToFunctionParam InductiveParameter {..} = _paramType = _inductiveParamType } -constructorImplicity :: ConstructorInfo -> IsImplicit -constructorImplicity info = - if info ^. constructorInfoTrait then ImplicitInstance else Explicit - patternArgFromVar :: IsImplicit -> VarName -> PatternArg patternArgFromVar i v = PatternArg @@ -66,19 +61,32 @@ patternArgFromVar i v = _patternArgPattern = PatternVariable v } --- | Given `mkPair`, returns (mkPair a b, [a, b]) -genConstructorPattern :: (Members '[NameIdGen] r) => Interval -> ConstructorInfo -> Sem r (PatternArg, [VarName]) -genConstructorPattern loc info = genConstructorPattern' impl loc (info ^. constructorInfoName) (length (snd (constructorArgTypes info))) - where - impl = constructorImplicity info +-- | Given `mkApplicative`, returns {{mkApplicative {{funct}}}} var_pure var_ap, [var_pure, var_ap] +genConstructorPattern :: + (Members '[NameIdGen] r) => + Interval -> + IsImplicit -> + ConstructorInfo -> + Sem r (PatternArg, [VarName]) +genConstructorPattern loc traitImplicity info = + genConstructorPattern' traitImplicity loc (info ^. constructorInfoName) (snd (constructorArgTypes info)) -- | Given `mkPair`, returns (mkPair a b, [a, b]) -genConstructorPattern' :: (Members '[NameIdGen] r) => IsImplicit -> Interval -> Name -> Int -> Sem r (PatternArg, [VarName]) -genConstructorPattern' impl loc cname cargs = do - vars <- mapM (freshVar loc) (Stream.take cargs allWords) - return (mkConstructorVarPattern impl cname vars, vars) +genConstructorPattern' :: + (Members '[NameIdGen] r) => + IsImplicit -> + Interval -> + Name -> + [FunctionParameter] -> + Sem r (PatternArg, [VarName]) +genConstructorPattern' traitImplicity loc concstrName cargs = do + vars :: [(IsImplicit, VarName)] <- runStreamOf allWords . forM cargs $ \p -> do + varTxt <- maybe yield return (p ^? paramName . _Just . nameText) + var <- freshVar loc varTxt + return (p ^. paramImplicit, var) + return (mkConstructorVarPattern traitImplicity concstrName vars, snd <$> vars) -mkConstructorVarPattern :: IsImplicit -> Name -> [VarName] -> PatternArg +mkConstructorVarPattern :: IsImplicit -> Name -> [(IsImplicit, VarName)] -> PatternArg mkConstructorVarPattern impl c vars = PatternArg { _patternArgIsImplicit = impl, @@ -88,33 +96,33 @@ mkConstructorVarPattern impl c vars = ConstructorApp { _constrAppConstructor = c, _constrAppType = Nothing, - _constrAppParameters = map (patternArgFromVar Explicit) vars + _constrAppParameters = map (uncurry patternArgFromVar) vars } } --- | Assumes the constructor does not have implicit arguments (which is not --- allowed at the moment). +-- | Generates a projection function for the given constructor and field index. genFieldProjection :: forall r. (Members '[NameIdGen] r) => + ProjectionKind -> FunctionName -> Maybe BuiltinFunction -> Maybe Pragmas -> ConstructorInfo -> Int -> Sem r FunctionDef -genFieldProjection _funDefName _funDefBuiltin mpragmas info fieldIx = do +genFieldProjection kind _funDefName _funDefBuiltin mpragmas info fieldIx = do body' <- genBody let (inductiveParams, constrArgs) = constructorArgTypes info - implicity = constructorImplicity info - saturatedTy = unnamedParameter' implicity (constructorReturnType info) + saturatedTy :: FunctionParameter = unnamedParameter' constructorImplicity (constructorReturnType info) inductiveArgs = map inductiveToFunctionParam inductiveParams - retTy = constrArgs !! fieldIx + param = constrArgs !! fieldIx + retTy = param ^. paramType cloneFunctionDefSameName FunctionDef { _funDefTerminating = False, _funDefInstance = False, - _funDefCoercion = False, + _funDefCoercion = kind == ProjectionCoercion, _funDefArgsInfo = mempty, _funDefPragmas = maybe @@ -127,9 +135,14 @@ genFieldProjection _funDefName _funDefBuiltin mpragmas info fieldIx = do _funDefBuiltin } where + constructorImplicity :: IsImplicit + constructorImplicity + | info ^. constructorInfoTrait = ImplicitInstance + | otherwise = Explicit + genBody :: Sem r Expression genBody = do - (pat, vars) <- genConstructorPattern (getLoc _funDefName) info + (pat, vars) <- genConstructorPattern (getLoc _funDefName) constructorImplicity info let body = toExpression (vars !! fieldIx) cl = LambdaClause @@ -265,5 +278,10 @@ substitutionE m expr Just e -> clone e Nothing -> return (toExpression n) -substituteIndParams :: forall r. (Member NameIdGen r) => [(InductiveParameter, Expression)] -> Expression -> Sem r Expression +substituteIndParams :: + forall r expr. + (Member NameIdGen r, HasExpressions expr) => + [(InductiveParameter, Expression)] -> + expr -> + Sem r expr substituteIndParams = substitutionE . HashMap.fromList . map (first (^. inductiveParamName)) diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs index 9667232eed..2d65b21405 100644 --- a/src/Juvix/Compiler/Internal/Extra/Base.hs +++ b/src/Juvix/Compiler/Internal/Extra/Base.hs @@ -367,10 +367,10 @@ foldFunType l r = go l foldFunTypeExplicit :: [Expression] -> Expression -> Expression foldFunTypeExplicit = foldFunType . map unnamedParameter -viewConstructorType :: Expression -> ([Expression], Expression) -viewConstructorType = first (map (^. paramType)) . unfoldFunType +viewConstructorType :: Expression -> ([FunctionParameter], Expression) +viewConstructorType = unfoldFunType -constructorArgs :: Expression -> [Expression] +constructorArgs :: Expression -> [FunctionParameter] constructorArgs = fst . viewConstructorType unfoldLambdaClauses :: Expression -> Maybe (NonEmpty (NonEmpty PatternArg, Expression)) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index a3634d191d..a605dd60a1 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -353,7 +353,16 @@ goProjectionDef :: goProjectionDef ProjectionDef {..} = do let c = goSymbol _projectionConstructor info <- gets (^?! constructorInfos . at c . _Just) - fun <- Internal.genFieldProjection (goSymbol _projectionField) ((^. withLocParam) <$> _projectionFieldBuiltin) (fmap (^. withLocParam . withSourceValue) _projectionPragmas) info _projectionFieldIx + fun <- + Internal.genFieldProjection + _projectionKind + (goSymbol _projectionField) + ( (^. withLocParam) + <$> _projectionFieldBuiltin + ) + (fmap (^. withLocParam . withSourceValue) _projectionPragmas) + info + _projectionFieldIx whenJust (fun ^. Internal.funDefBuiltin) (registerBuiltinFunction fun) return fun @@ -660,7 +669,7 @@ goConstructorDef retTy ConstructorDef {..} = do Just Internal.FunctionParameter { _paramName = Just (goSymbol _fieldName), - _paramImplicit = Explicit, + _paramImplicit = fromIsImplicitField _fieldIsImplicit, _paramType = ty' } @@ -911,22 +920,30 @@ goExpression = \case repeated :: ScoperError repeated = ErrRepeatedField (RepeatedField (f ^. fieldUpdateName)) - mkArgs :: [Indexed Internal.VarName] -> Sem r [Internal.Expression] + mkArgs :: IntMap (IsImplicit, Internal.VarName) -> Sem r [Internal.ApplicationArg] mkArgs vs = do fieldMap <- mkFieldmap execOutputList $ - go (uncurry Indexed <$> IntMap.toAscList fieldMap) vs + go (uncurry Indexed <$> IntMap.toAscList fieldMap) (intMapToList vs) where - go :: [Indexed (RecordUpdateField 'Scoped)] -> [Indexed Internal.VarName] -> Sem (Output Internal.Expression ': r) () + go :: [Indexed (RecordUpdateField 'Scoped)] -> [Indexed (IsImplicit, Internal.VarName)] -> Sem (Output Internal.ApplicationArg ': r) () go fields = \case [] -> return () - Indexed idx var : vars' -> case getArg idx of + Indexed idx (impl, var) : vars' -> case getArg idx of Nothing -> do - output (Internal.toExpression var) + output + Internal.ApplicationArg + { _appArg = Internal.toExpression var, + _appArgIsImplicit = impl + } go fields vars' Just (arg, fields') -> do val' <- goExpression (arg ^. fieldUpdateValue) - output val' + output + Internal.ApplicationArg + { _appArg = val', + _appArgIsImplicit = impl + } go fields' vars' where getArg :: Int -> Maybe (RecordUpdateField 'Scoped, [Indexed (RecordUpdateField 'Scoped)]) @@ -939,13 +956,13 @@ goExpression = \case mkClause = do let extra = r ^. recordUpdateExtra . unIrrelevant constr = goSymbol (extra ^. recordUpdateExtraConstructor) - vars = map goSymbol (extra ^. recordUpdateExtraVars) - patArg = Internal.mkConstructorVarPattern Explicit constr vars - args <- mkArgs (indexFrom 0 vars) + vars :: IntMap (IsImplicit, Internal.Name) = second goSymbol <$> extra ^. recordUpdateExtraVars + patArg = Internal.mkConstructorVarPattern Explicit constr (toList vars) + args <- mkArgs vars return Internal.LambdaClause { _lambdaPatterns = pure patArg, - _lambdaBody = Internal.foldExplicitApplication (Internal.toExpression constr) args + _lambdaBody = Internal.foldApplication (Internal.toExpression constr) args } goRecordUpdateApp :: Concrete.RecordUpdateApp -> Sem r Internal.Expression diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs index 0560ff4cd4..c319a4fb11 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -28,7 +28,7 @@ data CheckPositivityArgs = CheckPositivityArgs _checkPositivityArgsInductiveName :: Name, _checkPositivityArgsRecursionLimit :: Int, _checkPositivityArgsErrorReference :: Maybe Expression, - _checkPositivityArgsTypeOfConstructor :: Expression + _checkPositivityArgsTypeOfConstructorArg :: Expression } makeLenses ''CheckPositivityArgs @@ -54,7 +54,7 @@ checkPositivity indInfo = do _checkPositivityArgsInductiveName = indInfo ^. inductiveInfoName, _checkPositivityArgsRecursionLimit = numInductives, _checkPositivityArgsErrorReference = Nothing, - _checkPositivityArgsTypeOfConstructor = typeOfConstr + _checkPositivityArgsTypeOfConstructorArg = typeOfConstr ^. paramType } ) @@ -64,8 +64,8 @@ checkStrictlyPositiveOccurrences :: CheckPositivityArgs -> Sem r () checkStrictlyPositiveOccurrences p = do - typeOfConstr <- strongNormalize_ (p ^. checkPositivityArgsTypeOfConstructor) - goExpression False typeOfConstr + typeOfConstrArg <- strongNormalize_ (p ^. checkPositivityArgsTypeOfConstructorArg) + goExpression False typeOfConstrArg where indInfo = p ^. checkPositivityArgsInductive ctorName = p ^. checkPositivityArgsConstructorName @@ -209,7 +209,7 @@ checkStrictlyPositiveOccurrences p = do _checkPositivityArgsInductiveName = pName', _checkPositivityArgsRecursionLimit = recLimit - 1, _checkPositivityArgsErrorReference = Just errorRef, - _checkPositivityArgsTypeOfConstructor = tyConstr' + _checkPositivityArgsTypeOfConstructorArg = tyConstr' ^. paramType } ) args diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index b4ae5f166a..5ed1620a7b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -865,7 +865,7 @@ checkPattern = go (_, psTys) <- constructorArgTypes <$> lookupConstructor c psTys' <- mapM (substituteIndParams ctx) psTys let expectedNum = length psTys - w = map unnamedParameter psTys' + w :: [FunctionParameter] = psTys' when (expectedNum /= length ps) (throw (appErr app expectedNum)) pis <- zipWithM go w ps let appTy = foldExplicitApplication (ExpressionIden inductivename) (map snd ctx) @@ -873,14 +873,12 @@ checkPattern = go appErr :: ConstructorApp -> Int -> TypeCheckerError appErr app expected = - ErrArityCheckerError - ( ErrWrongConstructorAppLength - ( WrongConstructorAppLength - { _wrongConstructorAppLength = app, - _wrongConstructorAppLengthExpected = expected - } - ) - ) + ErrArityCheckerError $ + ErrWrongConstructorAppLength + WrongConstructorAppLength + { _wrongConstructorAppLength = app, + _wrongConstructorAppLengthExpected = expected + } checkSaturatedInductive :: Expression -> Sem r (Either Hole (InductiveName, [(InductiveParameter, Expression)])) checkSaturatedInductive ty = do diff --git a/src/Juvix/Data.hs b/src/Juvix/Data.hs index 0528b976cf..80d71a58cc 100644 --- a/src/Juvix/Data.hs +++ b/src/Juvix/Data.hs @@ -1,6 +1,7 @@ module Juvix.Data ( module Juvix.Data.Effect, module Juvix.Data.Error, + module Juvix.Data.ProjectionKind, module Juvix.Data.NumThreads, module Juvix.Data.Fixity, module Juvix.Data.FileExt, @@ -42,6 +43,7 @@ import Juvix.Data.NameId qualified import Juvix.Data.NumThreads import Juvix.Data.Pragmas import Juvix.Data.Processed +import Juvix.Data.ProjectionKind import Juvix.Data.TopModulePathKey import Juvix.Data.Uid import Juvix.Data.Universe diff --git a/src/Juvix/Data/InstanceHole.hs b/src/Juvix/Data/InstanceHole.hs index d4ded9e11d..7a297bd692 100644 --- a/src/Juvix/Data/InstanceHole.hs +++ b/src/Juvix/Data/InstanceHole.hs @@ -10,7 +10,11 @@ import Juvix.Prelude.Base import Prettyprinter fromHole :: Hole.Hole -> InstanceHole -fromHole (Hole.Hole a b) = InstanceHole a b +fromHole Hole.Hole {..} = + InstanceHole + { _iholeId = _holeId, + _iholeKw = _holeKw + } data InstanceHole = InstanceHole { _iholeId :: NameId, diff --git a/src/Juvix/Data/IsImplicit.hs b/src/Juvix/Data/IsImplicit.hs index 6e2c0639b6..dd252cac59 100644 --- a/src/Juvix/Data/IsImplicit.hs +++ b/src/Juvix/Data/IsImplicit.hs @@ -27,3 +27,24 @@ instance Pretty IsImplicit where Implicit -> "implicit" ImplicitInstance -> "implicit instance" Explicit -> "explicit" + +-- | When we support Implicit record fields we should remove this type in favour +-- of IsImplicit +data IsImplicitField + = ExplicitField + | ImplicitInstanceField + deriving stock (Show, Eq, Ord, Generic, Data) + +instance Hashable IsImplicitField + +instance Serialize IsImplicitField + +instance NFData IsImplicitField + +fromIsImplicitField :: IsImplicitField -> IsImplicit +fromIsImplicitField = \case + ImplicitInstanceField -> ImplicitInstance + ExplicitField -> Explicit + +instance Pretty IsImplicitField where + pretty = pretty . fromIsImplicitField diff --git a/src/Juvix/Data/ProjectionKind.hs b/src/Juvix/Data/ProjectionKind.hs new file mode 100644 index 0000000000..2333eedd38 --- /dev/null +++ b/src/Juvix/Data/ProjectionKind.hs @@ -0,0 +1,10 @@ +module Juvix.Data.ProjectionKind where + +import Juvix.Prelude.Base + +data ProjectionKind + = -- | Projection for regular fields + ProjectionExplicit + | -- | Projection for instance fields + ProjectionCoercion + deriving stock (Show, Eq, Ord, Generic) diff --git a/src/Juvix/Prelude/Base/Foundation.hs b/src/Juvix/Prelude/Base/Foundation.hs index e00a7bac36..7f68400372 100644 --- a/src/Juvix/Prelude/Base/Foundation.hs +++ b/src/Juvix/Prelude/Base/Foundation.hs @@ -672,11 +672,17 @@ popFirstJust f = \case uncurryF :: (Functor f) => (a -> b -> c) -> f (a, b) -> f c uncurryF g input_ = uncurry g <$> input_ +intMapToList :: IntMap a -> [Indexed a] +intMapToList = map (uncurry Indexed) . IntMap.toList + +intMap :: (Foldable f) => f (Int, a) -> IntMap a +intMap = IntMap.fromList . toList + indexedByInt :: (Foldable f) => (a -> Int) -> f a -> IntMap a -indexedByInt getIx l = IntMap.fromList [(getIx i, i) | i <- toList l] +indexedByInt getIx l = intMap [(getIx i, i) | i <- toList l] indexedByHash :: (Foldable f, Hashable k) => (a -> k) -> f a -> HashMap k a -indexedByHash getIx l = HashMap.fromList [(getIx i, i) | i <- toList l] +indexedByHash getIx l = hashMap [(getIx i, i) | i <- toList l] ordSet :: (Foldable f, Ord k) => f k -> Set k ordSet = Set.fromList . toList diff --git a/tests/positive/Internal/InstanceFields.juvix b/tests/positive/Internal/InstanceFields.juvix new file mode 100644 index 0000000000..7e0fd6218a --- /dev/null +++ b/tests/positive/Internal/InstanceFields.juvix @@ -0,0 +1,28 @@ +module InstanceFields; + +trait +type Functor (f : Type -> Type) := + mkFunctor { + map : {A B : Type} -> (A -> B) -> f A -> f B + }; + +trait +type Applicative (f : Type -> Type) := + mkApplicative { + {{ApplicativeFunctor}} : Functor f; + pure : {A : Type} -> A -> f A; + ap : {A B : Type} -> f (A -> B) -> f A -> f B + }; + +trait +type Monad (f : Type -> Type) := + mkMonad { + {{MonadApplicative}} : Applicative f; + bind : {A B : Type} -> f A -> (A -> f B) -> f B + }; + +open Functor; +open Applicative; +open Monad; + +monadMap {A B} {f : Type -> Type} {{Monad f}} (g : A -> B) (x : f A) : f B := map g x; diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index fbe84fce8d..af481b3f4e 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -104,9 +104,9 @@ record R = r2 :: nat fun r1 :: "R ⇒ nat" where - "r1 (mkR a b) = a" + "r1 (mkR r1' r2') = r1'" fun r2 :: "R ⇒ nat" where - "r2 (mkR a b) = b" + "r2 (mkR r1' r2') = r2'" end