From e79159b21e7f666ff915c5fe03c07d621460b2db Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 24 Jul 2023 16:56:13 +0200 Subject: [PATCH] Add record declaration syntax (#2254) - Closes #1641 This pr adds the option to declare constructors with fields. E.g. ``` type Pair (A B : Type) := | mkPair { fst : A; snd : B }; ``` Which is desugared to ``` type Pair (A B : Type) := | mkPair : (fst : A) -> (snd : B) -> Pair A B; ``` making it possible to write ` mkPair (fst := 1; snd := 2)`. Mutli-constructor types are also allowed to have fields. --- .../Concrete/Data/NameSignature/Builder.hs | 17 ++++- src/Juvix/Compiler/Concrete/Language.hs | 74 ++++++++++++++++++- src/Juvix/Compiler/Concrete/Print/Base.hs | 44 +++++++++-- .../FromParsed/Analysis/Scoping.hs | 45 ++++++++++- .../Concrete/Translation/FromSource.hs | 31 +++++++- src/Juvix/Compiler/Internal/Data/InfoTable.hs | 2 + src/Juvix/Compiler/Internal/Extra.hs | 4 +- .../Internal/Translation/FromConcrete.hs | 35 ++++++++- src/Juvix/Data/Effect/ExactPrint.hs | 8 +- src/Juvix/Prelude/Lens.hs | 5 ++ test/Typecheck/Positive.hs | 6 +- tests/positive/Records.juvix | 31 ++++++++ 12 files changed, 276 insertions(+), 26 deletions(-) create mode 100644 tests/positive/Records.juvix diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs index c3e3ad89ec..4c5e8feec3 100644 --- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs +++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs @@ -43,9 +43,24 @@ instance HasNameSignature (FunctionDef 'Parsed) where addAtoms (a ^. signRetType) instance HasNameSignature (InductiveDef 'Parsed, ConstructorDef 'Parsed) where + addArgs :: + forall r. + Members '[NameSignatureBuilder] r => + (InductiveDef 'Parsed, ConstructorDef 'Parsed) -> + Sem r () addArgs (i, c) = do mapM_ addConstructorParams (i ^. inductiveParameters) - addAtoms (c ^. constructorType) + addRhs (c ^. constructorRhs) + where + addRecord :: RhsRecord 'Parsed -> Sem r () + addRecord RhsRecord {..} = mapM_ addField _rhsRecordFields + where + addField :: RecordField 'Parsed -> Sem r () + addField RecordField {..} = addSymbol Explicit _fieldName + addRhs :: ConstructorRhs 'Parsed -> Sem r () + addRhs = \case + ConstructorRhsGadt g -> addAtoms (g ^. rhsGadtType) + ConstructorRhsRecord g -> addRecord g instance HasNameSignature (InductiveDef 'Parsed) where addArgs a = do diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 3da09d7267..4a00485383 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -357,11 +357,10 @@ type InductiveName s = SymbolType s data ConstructorDef (s :: Stage) = ConstructorDef { _constructorPipe :: Irrelevant (Maybe KeywordRef), - _constructorColonKw :: Irrelevant KeywordRef, _constructorName :: InductiveConstructorName s, _constructorDoc :: Maybe (Judoc s), _constructorPragmas :: Maybe ParsedPragmas, - _constructorType :: ExpressionType s + _constructorRhs :: ConstructorRhs s } deriving stock instance Show (ConstructorDef 'Parsed) @@ -376,6 +375,74 @@ deriving stock instance Ord (ConstructorDef 'Parsed) deriving stock instance Ord (ConstructorDef 'Scoped) +data RecordField (s :: Stage) = RecordField + { _fieldName :: SymbolType s, + _fieldColon :: Irrelevant (KeywordRef), + _fieldType :: ExpressionType s + } + +deriving stock instance Show (RecordField 'Parsed) + +deriving stock instance Show (RecordField 'Scoped) + +deriving stock instance Eq (RecordField 'Parsed) + +deriving stock instance Eq (RecordField 'Scoped) + +deriving stock instance Ord (RecordField 'Parsed) + +deriving stock instance Ord (RecordField 'Scoped) + +data RhsRecord (s :: Stage) = RhsRecord + { _rhsRecordDelim :: Irrelevant (KeywordRef, KeywordRef), + _rhsRecordFields :: NonEmpty (RecordField s) + } + +deriving stock instance Show (RhsRecord 'Parsed) + +deriving stock instance Show (RhsRecord 'Scoped) + +deriving stock instance Eq (RhsRecord 'Parsed) + +deriving stock instance Eq (RhsRecord 'Scoped) + +deriving stock instance Ord (RhsRecord 'Parsed) + +deriving stock instance Ord (RhsRecord 'Scoped) + +data RhsGadt (s :: Stage) = RhsGadt + { _rhsGadtColon :: Irrelevant KeywordRef, + _rhsGadtType :: ExpressionType s + } + +deriving stock instance Show (RhsGadt 'Parsed) + +deriving stock instance Show (RhsGadt 'Scoped) + +deriving stock instance Eq (RhsGadt 'Parsed) + +deriving stock instance Eq (RhsGadt 'Scoped) + +deriving stock instance Ord (RhsGadt 'Parsed) + +deriving stock instance Ord (RhsGadt 'Scoped) + +data ConstructorRhs (s :: Stage) + = ConstructorRhsGadt (RhsGadt s) + | ConstructorRhsRecord (RhsRecord s) + +deriving stock instance Show (ConstructorRhs 'Parsed) + +deriving stock instance Show (ConstructorRhs 'Scoped) + +deriving stock instance Eq (ConstructorRhs 'Parsed) + +deriving stock instance Eq (ConstructorRhs 'Scoped) + +deriving stock instance Ord (ConstructorRhs 'Parsed) + +deriving stock instance Ord (ConstructorRhs 'Scoped) + data InductiveParameters (s :: Stage) = InductiveParameters { _inductiveParametersNames :: NonEmpty (SymbolType s), _inductiveParametersType :: ExpressionType s @@ -1334,6 +1401,9 @@ newtype ModuleIndex = ModuleIndex } makeLenses ''PatternArg +makeLenses ''RecordField +makeLenses ''RhsRecord +makeLenses ''RhsGadt makeLenses ''List makeLenses ''ListPattern makeLenses ''UsingItem diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index dc5d92072f..8f29055b4b 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -160,7 +160,7 @@ instance SingI s => PrettyPrint (ListPattern s) where ppCode ListPattern {..} = do let l = ppCode _listpBracketL r = ppCode _listpBracketR - e = sepSemicolon (map ppPatternParensType _listpItems) + e = hsepSemicolon (map ppPatternParensType _listpItems) l <> e <> r instance PrettyPrint Void where @@ -174,7 +174,7 @@ instance PrettyPrint NameBlock where Explicit -> parens ppElem :: (Symbol, Int) -> Sem r () ppElem (sym, idx) = ppCode sym <> ppCode Kw.kwExclamation <> noLoc (pretty idx) - delims (sepSemicolon (map ppElem (toList _nameBlock))) + delims (hsepSemicolon (map ppElem (toList _nameBlock))) instance (PrettyPrint a, PrettyPrint b) => PrettyPrint (a, b) where ppCode (a, b) = tuple [ppCode a, ppCode b] @@ -217,8 +217,8 @@ instance SingI s => PrettyPrint (Iterator s) where let n = ppIdentifierType _iteratorName is = ppCode <$> _iteratorInitializers rngs = ppCode <$> _iteratorRanges - is' = parens . sepSemicolon <$> nonEmpty is - rngs' = parens . sepSemicolon <$> nonEmpty rngs + is' = parens . hsepSemicolon <$> nonEmpty is + rngs' = parens . hsepSemicolon <$> nonEmpty rngs b = ppExpressionType _iteratorBody b' | _iteratorBodyBraces = braces (oneLineOrNextNoIndent b) @@ -241,7 +241,7 @@ instance SingI s => PrettyPrint (List s) where ppCode List {..} = do let l = ppCode _listBracketL r = ppCode _listBracketR - e = sepSemicolon (map ppExpressionType _listItems) + e = hsepSemicolon (map ppExpressionType _listItems) l <> e <> r instance PrettyPrint AmbiguousIterator where @@ -260,7 +260,7 @@ instance SingI s => PrettyPrint (ArgumentBlock s) where (l, r) = case d of Nothing -> (enqueue C.kwParenL, noLoc C.kwParenR) Just (l', r') -> (ppCode l', ppCode r') - l <> sepSemicolon args' <> r + l <> align (sepSemicolon args') <> r where Irrelevant d = _argBlockDelims @@ -897,14 +897,42 @@ instance SingI s => PrettyPrint (NonEmpty (InductiveParameters s)) where instance PrettyPrint a => PrettyPrint (Irrelevant a) where ppCode (Irrelevant a) = ppCode a +instance SingI s => PrettyPrint (RhsGadt s) where + ppCode RhsGadt {..} = + ppCode _rhsGadtColon <+> ppExpressionType _rhsGadtType + +instance SingI s => PrettyPrint (RecordField s) where + ppCode RecordField {..} = + ppSymbolType _fieldName <+> ppCode _fieldColon <+> ppExpressionType _fieldType + +instance SingI s => PrettyPrint (RhsRecord s) where + ppCode RhsRecord {..} = do + let Irrelevant (l, r) = _rhsRecordDelim + fields' + | null (_rhsRecordFields ^. _tail1) = ppCode (_rhsRecordFields ^. _head1) + | otherwise = + line + <> indent + ( sequenceWith + (semicolon >> line) + (ppCode <$> _rhsRecordFields) + ) + <> line + ppCode l <> fields' <> ppCode r + +instance SingI s => PrettyPrint (ConstructorRhs s) where + ppCode = \case + ConstructorRhsGadt r -> ppCode r + ConstructorRhsRecord r -> ppCode r + instance SingI s => PrettyPrint (ConstructorDef s) where ppCode :: forall r. Members '[ExactPrint, Reader Options] r => ConstructorDef s -> Sem r () ppCode ConstructorDef {..} = do let constructorName' = annDef _constructorName (ppSymbolType _constructorName) - constructorType' = ppExpressionType _constructorType + constructorRhs' = ppCode _constructorRhs doc' = ppCode <$> _constructorDoc pragmas' = ppCode <$> _constructorPragmas - pipeHelper <+> nest (doc' ?<> pragmas' ?<> constructorName' <+> ppCode _constructorColonKw <+> constructorType') + pipeHelper <+> nest (doc' ?<> pragmas' ?<> constructorName' <+> constructorRhs') where -- we use this helper so that comments appear before the first optional pipe if the pipe was omitted pipeHelper :: Sem r () diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index d694bf9ed3..eb9e78b4af 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -720,16 +720,53 @@ checkInductiveDef InductiveDef {..} = do -- note that the constructor name is not bound here checkConstructorDef :: S.Symbol -> S.Symbol -> ConstructorDef 'Parsed -> Sem r (ConstructorDef 'Scoped) checkConstructorDef tyName constructorName' ConstructorDef {..} = do - constructorType' <- checkParseExpressionAtoms _constructorType doc' <- mapM checkJudoc _constructorDoc + rhs' <- checkRhs _constructorRhs registerConstructor tyName @$> ConstructorDef { _constructorName = constructorName', - _constructorType = constructorType', + _constructorRhs = rhs', _constructorDoc = doc', _constructorPragmas = _constructorPragmas, - _constructorPipe, - _constructorColonKw + _constructorPipe + } + + checkRhs :: ConstructorRhs 'Parsed -> Sem r (ConstructorRhs 'Scoped) + checkRhs = \case + ConstructorRhsGadt r -> ConstructorRhsGadt <$> checkGadt r + ConstructorRhsRecord r -> ConstructorRhsRecord <$> checkRecord r + + checkRecord :: RhsRecord 'Parsed -> Sem r (RhsRecord 'Scoped) + checkRecord RhsRecord {..} = do + fields' <- checkFields _rhsRecordFields + return + RhsRecord + { _rhsRecordFields = fields', + _rhsRecordDelim + } + where + checkFields :: NonEmpty (RecordField 'Parsed) -> Sem r (NonEmpty (RecordField 'Scoped)) + checkFields (RecordField {..} :| fs) = do + type' <- checkParseExpressionAtoms _fieldType + withLocalScope $ do + name' <- bindVariableSymbol _fieldName + let f = + RecordField + { _fieldType = type', + _fieldName = name', + .. + } + case nonEmpty fs of + Nothing -> return (pure f) + Just fs1 -> (pure f <>) <$> checkFields fs1 + + checkGadt :: RhsGadt 'Parsed -> Sem r (RhsGadt 'Scoped) + checkGadt RhsGadt {..} = do + constructorType' <- checkParseExpressionAtoms _rhsGadtType + return + RhsGadt + { _rhsGadtType = constructorType', + _rhsGadtColon } createExportsTable :: ExportInfo -> HashSet NameId diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 68393ab271..b1bf2934fe 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -1028,13 +1028,38 @@ inductiveParams = parens $ do _inductiveParametersType <- parseExpressionAtoms return InductiveParameters {..} -constructorDef :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (ConstructorDef 'Parsed) +rhsGadt :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (RhsGadt 'Parsed) +rhsGadt = P.label "" $ do + _rhsGadtColon <- Irrelevant <$> kw kwColon + _rhsGadtType <- parseExpressionAtoms P. "" + return RhsGadt {..} + +recordField :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (RecordField 'Parsed) +recordField = do + _fieldName <- symbol + _fieldColon <- Irrelevant <$> kw kwColon + _fieldType <- parseExpressionAtoms + return RecordField {..} + +rhsRecord :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (RhsRecord 'Parsed) +rhsRecord = P.label "" $ do + l <- kw delimBraceL + _rhsRecordFields <- P.sepEndBy1 recordField semicolon + r <- kw delimBraceR + let _rhsRecordDelim = Irrelevant (l, r) + return RhsRecord {..} + +pconstructorRhs :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (ConstructorRhs 'Parsed) +pconstructorRhs = + ConstructorRhsGadt <$> rhsGadt + <|> ConstructorRhsRecord <$> rhsRecord + +constructorDef :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => Irrelevant (Maybe KeywordRef) -> ParsecS r (ConstructorDef 'Parsed) constructorDef _constructorPipe = do _constructorDoc <- optional stashJudoc >> getJudoc _constructorPragmas <- optional stashPragmas >> getPragmas _constructorName <- symbol P. "" - _constructorColonKw <- Irrelevant <$> kw kwColon - _constructorType <- parseExpressionAtoms P. "" + _constructorRhs <- pconstructorRhs return ConstructorDef {..} wildcard :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r Wildcard diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index 5ff82904eb..0505893e25 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -216,6 +216,7 @@ constructorReturnType c = do info <- lookupConstructor c let inductiveParams = fst (constructorArgTypes info) ind = ExpressionIden (IdenInductive (info ^. constructorInfoInductive)) + saturatedTy1 = foldExplicitApplication ind (map (ExpressionIden . IdenVar) inductiveParams) saturatedTy = foldl' ( \t v -> @@ -229,6 +230,7 @@ constructorReturnType c = do ) ind inductiveParams + unless (saturatedTy1 == saturatedTy) impossible return saturatedTy getAxiomBuiltinInfo :: Member (Reader InfoTable) r => Name -> Sem r (Maybe BuiltinAxiom) diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index 27a8c62809..d248e6e7e3 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -265,7 +265,7 @@ patternVariables f p = case p of goApp :: Traversal' ConstructorApp VarName goApp g = traverseOf constrAppParameters (traverse (patternArgVariables g)) -inductiveTypeVarsAssoc :: (Foldable f) => InductiveDef -> f a -> HashMap VarName a +inductiveTypeVarsAssoc :: Foldable f => InductiveDef -> f a -> HashMap VarName a inductiveTypeVarsAssoc def l | length vars < n = impossible | otherwise = HashMap.fromList (zip vars (toList l)) @@ -334,7 +334,7 @@ foldExplicitApplication f = foldApplication f . map (ApplicationArg Explicit) foldApplication :: Expression -> [ApplicationArg] -> Expression foldApplication f args = case args of [] -> f - ((ApplicationArg i a) : as) -> foldApplication (ExpressionApplication (Application f a i)) as + ApplicationArg i a : as -> foldApplication (ExpressionApplication (Application f a i)) as unfoldApplication' :: Application -> (Expression, NonEmpty ApplicationArg) unfoldApplication' (Application l' r' i') = second (|: (ApplicationArg i' r')) (unfoldExpressionApp l') diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 021a5ab3eb..b5a638e0e7 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -634,16 +634,18 @@ goInductive ty@InductiveDef {..} = do _inductiveParameters' <- concatMapM goInductiveParameters _inductiveParameters _inductiveType' <- mapM goExpression _inductiveType _inductivePragmas' <- goPragmas _inductivePragmas + let inductiveName' = goSymbol _inductiveName + constrRetType = Internal.foldExplicitApplication (Internal.toExpression inductiveName') (map (Internal.ExpressionIden . Internal.IdenVar . (^. Internal.inductiveParamName)) _inductiveParameters') _inductiveConstructors' <- local (const _inductivePragmas') $ - mapM goConstructorDef _inductiveConstructors + mapM (goConstructorDef constrRetType) _inductiveConstructors _inductiveExamples' <- goExamples _inductiveDoc let loc = getLoc _inductiveName indDef = Internal.InductiveDef { _inductiveParameters = _inductiveParameters', _inductiveBuiltin = (^. withLocParam) <$> _inductiveBuiltin, - _inductiveName = goSymbol _inductiveName, + _inductiveName = inductiveName', _inductiveType = fromMaybe (Internal.ExpressionUniverse (SmallUniverse loc)) _inductiveType', _inductiveConstructors = toList _inductiveConstructors', _inductiveExamples = _inductiveExamples', @@ -654,11 +656,13 @@ goInductive ty@InductiveDef {..} = do return indDef goConstructorDef :: + forall r. Members [Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r => + Internal.Expression -> ConstructorDef 'Scoped -> Sem r Internal.ConstructorDef -goConstructorDef ConstructorDef {..} = do - ty' <- goExpression _constructorType +goConstructorDef retTy ConstructorDef {..} = do + ty' <- goRhs _constructorRhs examples' <- goExamples _constructorDoc pragmas' <- goPragmas _constructorPragmas return @@ -668,6 +672,29 @@ goConstructorDef ConstructorDef {..} = do _inductiveConstructorName = goSymbol _constructorName, _inductiveConstructorPragmas = pragmas' } + where + goRecord :: Concrete.RhsRecord 'Scoped -> Sem r Internal.Expression + goRecord RhsRecord {..} = do + params <- mapM goField _rhsRecordFields + return (Internal.foldFunType (toList params) retTy) + where + goField :: Concrete.RecordField 'Scoped -> Sem r Internal.FunctionParameter + goField RecordField {..} = do + ty' <- goExpression _fieldType + return + Internal.FunctionParameter + { _paramName = Just (goSymbol _fieldName), + _paramImplicit = Explicit, + _paramType = ty' + } + + goGadt :: Concrete.RhsGadt 'Scoped -> Sem r Internal.Expression + goGadt = goExpression . (^. Concrete.rhsGadtType) + + goRhs :: Concrete.ConstructorRhs 'Scoped -> Sem r Internal.Expression + goRhs = \case + ConstructorRhsGadt r -> goGadt r + ConstructorRhsRecord r -> goRecord r goLiteral :: LiteralLoc -> Internal.LiteralLoc goLiteral = fmap go diff --git a/src/Juvix/Data/Effect/ExactPrint.hs b/src/Juvix/Data/Effect/ExactPrint.hs index 4b5342dc65..11a1c0cbb7 100644 --- a/src/Juvix/Data/Effect/ExactPrint.hs +++ b/src/Juvix/Data/Effect/ExactPrint.hs @@ -95,7 +95,13 @@ blockIndent :: Members '[ExactPrint] r => Sem r () -> Sem r () blockIndent d = hardline <> indent d <> line sepSemicolon :: (Members '[ExactPrint] r, Foldable l) => l (Sem r ()) -> Sem r () -sepSemicolon = sequenceWith (semicolon <> space) +sepSemicolon = grouped . vsepSemicolon + +vsepSemicolon :: (Members '[ExactPrint] r, Foldable l) => l (Sem r ()) -> Sem r () +vsepSemicolon = sequenceWith (semicolon <> line) + +hsepSemicolon :: (Members '[ExactPrint] r, Foldable l) => l (Sem r ()) -> Sem r () +hsepSemicolon = sequenceWith (semicolon <> space) dotted :: (Foldable f, Members '[ExactPrint] r) => f (Sem r ()) -> Sem r () dotted = sequenceWith (noLoc C.kwDot) diff --git a/src/Juvix/Prelude/Lens.hs b/src/Juvix/Prelude/Lens.hs index 05a22a7319..2536a297c3 100644 --- a/src/Juvix/Prelude/Lens.hs +++ b/src/Juvix/Prelude/Lens.hs @@ -6,6 +6,11 @@ import Juvix.Prelude.Base _head1 :: Lens' (NonEmpty a) a _head1 = singular each +_tail1 :: Lens' (NonEmpty a) [a] +_tail1 f (h :| hs) = do + hs' <- f hs + pure (h :| hs') + -- | View a non-empty list as the init part plus the last element. _unsnoc1 :: Lens (NonEmpty a) (NonEmpty b) ([a], a) ([b], b) _unsnoc1 afb la = uncurryF (|:) (afb (maybe [] toList minit, lasta)) diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs index b8d312647e..d1fcbffa11 100644 --- a/test/Typecheck/Positive.hs +++ b/test/Typecheck/Positive.hs @@ -244,7 +244,11 @@ tests = posTest "Named arguments" $(mkRelDir ".") - $(mkRelFile "NamedArguments.juvix") + $(mkRelFile "NamedArguments.juvix"), + posTest + "Record declaration" + $(mkRelDir ".") + $(mkRelFile "Records.juvix") ] <> [ compilationTest t | t <- Compilation.tests ] diff --git a/tests/positive/Records.juvix b/tests/positive/Records.juvix new file mode 100644 index 0000000000..30a7f57ef8 --- /dev/null +++ b/tests/positive/Records.juvix @@ -0,0 +1,31 @@ +module Records; + +type T := + | constructT : T; + +type Pair (A B : Type) := + | mkPair { + fst : A; + snd : B + }; + +p1 : Pair T T := + mkPair (fst := constructT; snd := constructT); + +type EnumRecord := + | C1 { + c1a : T; + c1b : T + } + | C2 { + c2a : T; + c2b : T + }; + +p2 : Pair EnumRecord EnumRecord := + mkPair + (fst := C1 (c1a := constructT; c1b := constructT); + snd := C2 (c2a := constructT; c2b := constructT)); + +type newtype := + | mknewtype {f : T};