From f5b75edd91389f0a45045b707abfa36c746e8d54 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 30 Jan 2025 16:57:47 +0000
Subject: Modify definition of data types.

---
 src/Inky.idr             |  2 +-
 src/Inky/Term/Parser.idr | 26 ++++++++++++++------------
 src/Inky/Type/Pretty.idr |  5 ++---
 3 files changed, 17 insertions(+), 16 deletions(-)

(limited to 'src')

diff --git a/src/Inky.idr b/src/Inky.idr
index 3f6b755..7fa9cad 100644
--- a/src/Inky.idr
+++ b/src/Inky.idr
@@ -76,7 +76,7 @@ readFileOrStdin (Just path) = withFile path Read throw readFile
 lexInkyString : HasErr (WithBounds String) es => String -> App es (List (WithBounds InkyToken))
 lexInkyString file = do
   let (tokens, _, _, "") = lex tokenMap file
-    | (_, line, col, rest) => 
+    | (_, line, col, rest) =>
       throw (MkBounded "unexpected character" False (MkBounds line col line col))
   pure (filter (\x => relevant x.val.kind) tokens)
 
diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr
index e977bc2..5cfd06b 100644
--- a/src/Inky/Term/Parser.idr
+++ b/src/Inky/Term/Parser.idr
@@ -37,6 +37,7 @@ data InkyKind
   | FoldCase
   | Fold
   | By
+  | Data
   | Nat
   | List
   | Suc
@@ -78,6 +79,7 @@ Eq InkyKind where
   FoldCase == FoldCase = True
   Fold == Fold = True
   By == By = True
+  Data == Data = True
   Nat == Nat = True
   List == List = True
   Suc == Suc = True
@@ -120,6 +122,7 @@ Interpolation InkyKind where
   interpolate FoldCase = "'foldcase'"
   interpolate Fold = "'fold'"
   interpolate By = "'by'"
+  interpolate Data = "'Data'"
   interpolate Nat = "'Nat'"
   interpolate List = "'List'"
   interpolate Suc = "'suc'"
@@ -167,6 +170,7 @@ TokenKind InkyKind where
   tokValue FoldCase = const ()
   tokValue Fold = const ()
   tokValue By = const ()
+  tokValue Data = const ()
   tokValue Nat = const ()
   tokValue List = const ()
   tokValue Suc = const ()
@@ -204,6 +208,7 @@ keywords =
   , ("foldcase", FoldCase)
   , ("fold", Fold)
   , ("by", By)
+  , ("data", Data)
   , ("Nat", Nat)
   , ("List", List)
   , ("suc", Suc)
@@ -393,17 +398,6 @@ parseList3 (x :: xs) =
 
 -- Types -----------------------------------------------------------------------
 
-OpenOrFixpointType : TypeParser [<] [<"openType"]
-OpenOrFixpointType =
-  OneOf
-    [ mkFix <$>
-      Seq [match Backslash, match TypeIdent, match DoubleArrow, Var (%%% "openType")]
-    , Var (%%% "openType")
-    ]
-  where
-  mkFix : HList [(), String, (), TypeFun] -> TypeFun
-  mkFix [_, x, _, a] = MkParseFun (\ctx => TFix x <$> a.try (ctx :< x))
-
 AtomType : TypeParser [<"openType"] [<]
 AtomType =
   OneOf
@@ -411,7 +405,7 @@ AtomType =
     , MkParseFun (\_ => Ok TNat) <$ match Nat
     , mkProd <$> enclose (match AngleOpen) (match AngleClose) row
     , mkSum <$> enclose (match BracketOpen) (match BracketClose) row
-    , enclose (match ParenOpen) (match ParenClose) OpenOrFixpointType
+    , enclose (match ParenOpen) (match ParenClose) (Var (%%% "openType"))
     ]
   where
   row : InkyParser True [<] [<"openType" :- TypeFun] (List $ WithBounds $ Assoc TypeFun)
@@ -428,11 +422,19 @@ AppType =
   OneOf
     [ AtomType
     , match List **> mkList <$> weaken (S Z) AtomType
+    , mkFix <$> Seq
+      [ match Data
+      , match TypeIdent
+      , weaken (S Z) AtomType
+      ]
     ]
   where
   mkList : TypeFun -> TypeFun
   mkList x = MkParseFun (\ctx => TList <$> x.try ctx)
 
+  mkFix : HList [(), String, TypeFun] -> TypeFun
+  mkFix [_, x, a] = MkParseFun (\ctx => TFix x <$> a.try (ctx :< x))
+
 export
 OpenType : TypeParser [<] [<]
 OpenType =
diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr
index 03b9964..7cd185c 100644
--- a/src/Inky/Type/Pretty.idr
+++ b/src/Inky/Type/Pretty.idr
@@ -78,9 +78,8 @@ lessPrettyType (TSum (MkRow as _)) d =
       (neutral <++> concatWith (surround $ line <+> ";" <++> neutral) parts <+> line)
       (concatWith (surround $ ";" <++> neutral) parts)
 lessPrettyType (TFix x a) d =
-  group $ align $ hang 2 $ parens $
-    "\\" <+> pretty x <++> "=>" <+> line <+>
-    prettyType a Open
+  group $ align $ hang 2 $ parenthesise (d < App) $
+    pretty "data" <++> pretty x <+> line <+> prettyType a Atom
 
 lessPrettyTypeCtx [<] d = [<]
 lessPrettyTypeCtx (as :< (x :- a)) d =
-- 
cgit v1.2.3