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.
anoma · Jul 24, 2023 · e79159b · e79159b
1 parent ea652e5
commit e79159b
Show file tree

Hide file tree

Showing 12 changed files with 276 additions and 26 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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 "<constructor gadt>" $ do
+  _rhsGadtColon <- Irrelevant <$> kw kwColon
+  _rhsGadtType <- parseExpressionAtoms P.<?> "<constructor type>"
+  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 "<constructor record>" $ 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.<?> "<constructor name>"
-  _constructorColonKw <- Irrelevant <$> kw kwColon
-  _constructorType <- parseExpressionAtoms P.<?> "<constructor type>"
+  _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
@@ -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
@@ -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')