Adt syntax (#2262)

- merge #2260  first

Allows constructors to be defined using Haskell-like Adt syntax.
E.g.
```
module Adt;

type Bool :=
  | true
  | false;

type Pair (A B : Type) :=
  | mkPair A B;

type Nat :=
  | zero
  | suc Nat;
```

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>

src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs

@@ -61,6 +61,7 @@ instance HasNameSignature (InductiveDef 'Parsed, ConstructorDef 'Parsed) where
       addRhs = \case
         ConstructorRhsGadt g -> addAtoms (g ^. rhsGadtType)
         ConstructorRhsRecord g -> addRecord g
+        ConstructorRhsAdt {} -> return ()
 
 instance HasNameSignature (InductiveDef 'Parsed) where
   addArgs a = do

src/Juvix/Compiler/Concrete/Language.hs

@@ -423,6 +423,22 @@ deriving stock instance Ord (RecordField 'Parsed)
 
 deriving stock instance Ord (RecordField 'Scoped)
 
+newtype RhsAdt (s :: Stage) = RhsAdt
+  { _rhsAdtArguments :: [ExpressionType s]
+  }
+
+deriving stock instance Show (RhsAdt 'Parsed)
+
+deriving stock instance Show (RhsAdt 'Scoped)
+
+deriving stock instance Eq (RhsAdt 'Parsed)
+
+deriving stock instance Eq (RhsAdt 'Scoped)
+
+deriving stock instance Ord (RhsAdt 'Parsed)
+
+deriving stock instance Ord (RhsAdt 'Scoped)
+
 data RhsRecord (s :: Stage) = RhsRecord
   { _rhsRecordDelim :: Irrelevant (KeywordRef, KeywordRef),
     _rhsRecordFields :: NonEmpty (RecordField s)
@@ -460,6 +476,7 @@ deriving stock instance Ord (RhsGadt 'Scoped)
 data ConstructorRhs (s :: Stage)
   = ConstructorRhsGadt (RhsGadt s)
   | ConstructorRhsRecord (RhsRecord s)
+  | ConstructorRhsAdt (RhsAdt s)
 
 deriving stock instance Show (ConstructorRhs 'Parsed)
 
@@ -1431,6 +1448,7 @@ makeLenses ''SymbolEntry
 makeLenses ''ModuleSymbolEntry
 makeLenses ''RecordField
 makeLenses ''RhsRecord
+makeLenses ''RhsAdt
 makeLenses ''RhsGadt
 makeLenses ''List
 makeLenses ''ListPattern

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -939,20 +939,35 @@ instance SingI s => PrettyPrint (RhsRecord s) where
                 <> line
     ppCode l <> fields' <> ppCode r
 
+instance SingI s => PrettyPrint (RhsAdt s) where
+  ppCode = align . sep . fmap ppExpressionType . (^. rhsAdtArguments)
+
 instance SingI s => PrettyPrint (ConstructorRhs s) where
+  ppCode :: Members '[ExactPrint, Reader Options] r => ConstructorRhs s -> Sem r ()
   ppCode = \case
     ConstructorRhsGadt r -> ppCode r
     ConstructorRhsRecord r -> ppCode r
+    ConstructorRhsAdt 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)
-        constructorRhs' = ppCode _constructorRhs
+        constructorRhs' = constructorRhsHelper _constructorRhs
         doc' = ppCode <$> _constructorDoc
         pragmas' = ppCode <$> _constructorPragmas
-    pipeHelper <+> nest (doc' ?<> pragmas' ?<> constructorName' <+> constructorRhs')
+    pipeHelper <+> nest (doc' ?<> pragmas' ?<> constructorName' <> constructorRhs')
     where
+      constructorRhsHelper :: ConstructorRhs s -> Sem r ()
+      constructorRhsHelper r = spaceMay <> ppCode r
+        where
+          spaceMay = case r of
+            ConstructorRhsGadt {} -> space
+            ConstructorRhsRecord {} -> space
+            ConstructorRhsAdt a
+              | null (a ^. rhsAdtArguments) -> mempty
+              | otherwise -> space
+
       -- we use this helper so that comments appear before the first optional pipe if the pipe was omitted
       pipeHelper :: Sem r ()
       pipeHelper = case _constructorPipe ^. unIrrelevant of

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -733,6 +733,7 @@ checkInductiveDef InductiveDef {..} = do
     checkRhs = \case
       ConstructorRhsGadt r -> ConstructorRhsGadt <$> checkGadt r
       ConstructorRhsRecord r -> ConstructorRhsRecord <$> checkRecord r
+      ConstructorRhsAdt r -> ConstructorRhsAdt <$> checkAdt r
 
     checkRecord :: RhsRecord 'Parsed -> Sem r (RhsRecord 'Scoped)
     checkRecord RhsRecord {..} = do
@@ -758,6 +759,14 @@ checkInductiveDef InductiveDef {..} = do
               Nothing -> return (pure f)
               Just fs1 -> (pure f <>) <$> checkFields fs1
 
+    checkAdt :: RhsAdt 'Parsed -> Sem r (RhsAdt 'Scoped)
+    checkAdt RhsAdt {..} = do
+      args' <- mapM checkParseExpressionAtoms _rhsAdtArguments
+      return
+        RhsAdt
+          { _rhsAdtArguments = args'
+          }
+
     checkGadt :: RhsGadt 'Parsed -> Sem r (RhsGadt 'Scoped)
     checkGadt RhsGadt {..} = do
       constructorType' <- checkParseExpressionAtoms _rhsGadtType

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -1045,6 +1045,11 @@ recordField = do
   _fieldType <- parseExpressionAtoms
   return RecordField {..}
 
+rhsAdt :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (RhsAdt 'Parsed)
+rhsAdt = P.label "<constructor arguments>" $ do
+  _rhsAdtArguments <- many atomicExpression
+  return RhsAdt {..}
+
 rhsRecord :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (RhsRecord 'Parsed)
 rhsRecord = P.label "<constructor record>" $ do
   l <- kw delimBraceL
@@ -1057,6 +1062,7 @@ pconstructorRhs :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdG
 pconstructorRhs =
   ConstructorRhsGadt <$> rhsGadt
     <|> ConstructorRhsRecord <$> rhsRecord
+    <|> ConstructorRhsAdt <$> rhsAdt
 
 constructorDef :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => Irrelevant (Maybe KeywordRef) -> ParsecS r (ConstructorDef 'Parsed)
 constructorDef _constructorPipe = do
@@ -1174,7 +1180,6 @@ openModule = do
   _openModuleImportKw <- optional (kw kwImport)
   _openModuleName <- name
   whenJust _openModuleImportKw (const (P.lift (importedModule (moduleNameToTopModulePath _openModuleName))))
-  _openParameters <- many atomicExpression
   _openUsingHiding <- optional usingOrHiding
   _openPublicKw <- Irrelevant <$> optional (kw kwPublic)
   let _openPublic = maybe NoPublic (const Public) (_openPublicKw ^. unIrrelevant)
@@ -1193,7 +1198,6 @@ newOpenSyntax :: forall r. (Members '[Error ParserError, PathResolver, Files, In
 newOpenSyntax = do
   im <- import_
   _openModuleKw <- kw kwOpen
-  _openParameters <- many atomicExpression
   _openUsingHiding <- optional usingOrHiding
   _openPublicKw <- Irrelevant <$> optional (kw kwPublic)
   let _openModuleName = topModulePathToName (im ^. importModule)

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -700,6 +700,21 @@ goConstructorDef retTy ConstructorDef {..} = do
         _inductiveConstructorPragmas = pragmas'
       }
   where
+    goAdt :: Concrete.RhsAdt 'Scoped -> Sem r Internal.Expression
+    goAdt RhsAdt {..} = do
+      args <- mapM goArg _rhsAdtArguments
+      return (Internal.foldFunType args retTy)
+      where
+        goArg :: Concrete.Expression -> Sem r Internal.FunctionParameter
+        goArg ty = do
+          ty' <- goExpression ty
+          return
+            Internal.FunctionParameter
+              { _paramName = Nothing,
+                _paramImplicit = Explicit,
+                _paramType = ty'
+              }
+
     goRecord :: Concrete.RhsRecord 'Scoped -> Sem r Internal.Expression
     goRecord RhsRecord {..} = do
       params <- mapM goField _rhsRecordFields
@@ -722,6 +737,7 @@ goConstructorDef retTy ConstructorDef {..} = do
     goRhs = \case
       ConstructorRhsGadt r -> goGadt r
       ConstructorRhsRecord r -> goRecord r
+      ConstructorRhsAdt r -> goAdt r
 
 goLiteral :: LiteralLoc -> Internal.LiteralLoc
 goLiteral = fmap go

src/Juvix/Data/Effect/ExactPrint.hs

@@ -94,6 +94,9 @@ semicolon = noLoc C.kwSemicolon
 blockIndent :: Members '[ExactPrint] r => Sem r () -> Sem r ()
 blockIndent d = hardline <> indent d <> line
 
+sep :: (Members '[ExactPrint] r, Foldable l) => l (Sem r ()) -> Sem r ()
+sep = grouped . vsep
+
 sepSemicolon :: (Members '[ExactPrint] r, Foldable l) => l (Sem r ()) -> Sem r ()
 sepSemicolon = grouped . vsepSemicolon
 
@@ -131,7 +134,7 @@ enclose :: Monad m => m () -> m () -> m () -> m ()
 enclose l r p = l >> p >> r
 
 encloseSep :: (Monad m, Foldable f) => m () -> m () -> m () -> f (m ()) -> m ()
-encloseSep l r sep f = enclose l r (sequenceWith sep f)
+encloseSep l r separator f = enclose l r (sequenceWith separator f)
 
 oneLineOrNextNoIndent :: Members '[ExactPrint] r => Sem r () -> Sem r ()
 oneLineOrNextNoIndent = region P.oneLineOrNextNoIndent

test/Scope/Positive.hs

@@ -246,5 +246,9 @@ tests =
     PosTest
       "Namespaces"
       $(mkRelDir ".")
-      $(mkRelFile "Namespaces.juvix")
+      $(mkRelFile "Namespaces.juvix"),
+    PosTest
+      "Adt"
+      $(mkRelDir ".")
+      $(mkRelFile "Adt.juvix")
   ]

test/Typecheck/Positive.hs

@@ -125,6 +125,10 @@ tests =
       "Inductive"
       $(mkRelDir ".")
       $(mkRelFile "Inductive.juvix"),
+    posTest
+      "ADT"
+      $(mkRelDir ".")
+      $(mkRelFile "Adt.juvix"),
     posTest
       "Operators"
       $(mkRelDir ".")

tests/positive/Adt.juvix

@@ -0,0 +1,27 @@
+module Adt;
+
+type Bool :=
+  | true
+  | false;
+
+type Pair (A B : Type) :=
+  | mkPair A B;
+
+type Nat :=
+  | zero
+  | suc Nat;
+
+c1 : Bool;
+c1 := true;
+
+c2 : Bool;
+c2 := false;
+
+c3 : Pair Bool Bool;
+c3 := mkPair true false;
+
+c4 : Nat;
+c4 := zero;
+
+c5 : Nat;
+c5 := suc zero;