Data definitions with record syntax.

3 files changed, 31 insertions, 1 deletions

diff --git a/prototypes/Infer.hs b/prototypes/Infer.hs
index bee972b2..836cef48 100644
--- a/prototypes/Infer.hs
+++ b/prototypes/Infer.hs
@@ -1375,7 +1375,11 @@ parseStmt ns e =
             let mkConTy (_, ts') = foldr (uncurry SPi) (foldl SAppV (SGlobal x) $ downTo (length ts') $ length ts) ts'
             cs <-
                  do keyword "where" *> localIndentation Ge (localAbsoluteIndentation $ many $ typedId' ns Nothing nps)
-             <|> do keyword "=" *> sepBy1 ((,) <$> (pure <$> lcIdents ns) <*> (mkConTy <$> telescope (typeNS ns) Nothing nps)) (keyword "|")
+             <|> do keyword "=" *>
+                      sepBy1 ((,) <$> (pure <$> lcIdents ns)
+                                  <*> (    braces (mkConTy <$> (telescopeDataFields (typeNS ns) nps))
+                                       <|> (mkConTy <$> telescope (typeNS ns) Nothing nps)) )
+                                      (keyword "|")
              <|> pure []
             return $ pure $ Data x ts t $ concatMap (\(vs, t) -> (,) <$> vs <*> pure t) cs
  <|> do (vs, t) <- try $ typedId' ns Nothing []
@@ -1404,6 +1408,13 @@ parseStmt ns e =
                 return $ mkLets' ge dcls
             return $ pure $ FunAlt n ts gu $ f rhs
  <|> pure . uncurry ValueDef <$> valueDef ns e
+ where
+   telescopeDataFields ns vs = option (vs, []) $ do
+       (x, vt) <- do name <- var (expNS ns)
+                     operator "::"
+                     term <- parseTerm ns PrecAtom vs
+                     return (name, (Visible, term))
+       (id *** (vt:)) <$> (comma *> telescopeDataFields ns (x: vs) <|> pure (vs, []))
 
 type DBNames = [SName]  -- De Bruijn variable names
 
diff --git a/prototypes/tests/accept/data.lc b/prototypes/tests/accept/data.lc
new file mode 100644
index 00000000..60731eb8
--- /dev/null
+++ b/prototypes/tests/accept/data.lc
@@ -0,0 +1,18 @@
+data Data0 = Data0
+
+data Data1 a b c = Data1 a b c
+
+data Data2 = Data21 Int
+           | Data22 { x :: Int, y::Int }
+           | Data23 { x :: Int }
+           | Data24 { }
+
+data Data5 a5 b5 c5 = Data51 { a5::a5}
+                    | Data52 { a5::a5, b5::b5, c5::c5 }
+                    | Data53 Int a5 Float b5 c5
+
+{-
+f (Data41 {}) = 5
+f (Data42 {c4=c}) = c
+f d = a4 d
+-}
diff --git a/prototypes/tests/reject/data.lc b/prototypes/tests/reject/data.lc
new file mode 100644
index 00000000..4f609a33
--- /dev/null
+++ b/prototypes/tests/reject/data.lc
@@ -0,0 +1 @@
+data Data1 = Data1 a b c