[ #242 ] Implement GADT syntax

Author: jespercockx

src/Agda2Hs/Compile.hs

@@ -126,15 +126,16 @@ compile genv tlm _ def =
         (CompileToPragma s   , Function{}) -> [] <$ checkCompileToFunctionPragma def s
 
         (ClassPragma ms      , Record{}  ) -> pure <$> compileRecord (ToClass ms) def
-        (NewTypePragma ds    , Record{}  ) -> pure <$> compileRecord (ToRecord True ds) def
-        (NewTypePragma ds    , Datatype{}) -> compileData True ds def
-        (DefaultPragma ds    , Datatype{}) -> compileData False ds def
+        (NewTypePragma ds    , Record{}  ) -> pure <$> compileRecord (ToRecord ToNewType ds) def
+        (NewTypePragma ds    , Datatype{}) -> compileData ToNewType ds def
+        (GadtPragma ds       , Datatype{}) -> compileData ToGadt ds def
+        (DefaultPragma ds    , Datatype{}) -> compileData ToData ds def
         (DerivePragma s      , _         ) | isInstance -> pure <$> compileInstance (ToDerivation s) def
         (DefaultPragma _     , Axiom{}   ) | isInstance -> pure <$> compileInstance (ToDerivation Nothing) def
         (DefaultPragma _     , _         ) | isInstance -> pure <$> compileInstance ToDefinition def
         (DefaultPragma _     , Axiom{}   ) -> compilePostulate def
         (DefaultPragma _     , Function{}) -> compileFun True def
-        (DefaultPragma ds    , Record{}  ) -> pure <$> compileRecord (ToRecord False ds) def
+        (DefaultPragma ds    , Record{}  ) -> pure <$> compileRecord (ToRecord ToData ds) def
 
         _ -> agda2hsErrorM $ text "Don't know how to compile" <+> prettyTCM (defName def)
 

src/Agda2Hs/Compile/Data.hs

@@ -13,12 +13,13 @@ import Agda.TypeChecking.Telescope
 
 import Agda.Utils.Maybe
 import Agda.Utils.Monad
+import Agda.Utils.Singleton
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 
 import Agda2Hs.AgdaUtils
 
 import Agda2Hs.Compile.Name
-import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
+import Agda2Hs.Compile.Type ( compileType, compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 
@@ -34,8 +35,8 @@ checkNewtype name cs = do
     (Hs.QualConDecl () _ _ (Hs.ConDecl () cName types):_) -> checkNewtypeCon cName types
     _ -> __IMPOSSIBLE__
 
-compileData :: AsNewType -> [Hs.Deriving ()] -> Definition -> C [Hs.Decl ()]
-compileData newtyp ds def = do
+compileData :: DataTarget -> [Hs.Deriving ()] -> Definition -> C [Hs.Decl ()]
+compileData target ds def = do
   let d = hsName $ prettyShow $ qnameName $ defName def
   checkValidTypeName d
   let Datatype{dataPars = n, dataIxs = numIxs, dataCons = cs} = theDef def
@@ -48,12 +49,22 @@ compileData newtyp ds def = do
     -- TODO: filter out erased constructors
     cs <- mapM (compileConstructor params) cs
     let hd = foldl (Hs.DHApp ()) (Hs.DHead () d) binds
+    let htarget = toDataTarget target
 
-    let target = if newtyp then Hs.NewType () else Hs.DataType ()
+    when (target == ToNewType) (checkNewtype d $ map fst cs)
 
-    when newtyp (checkNewtype d cs)
+    return . singleton $ case target of
+      ToGadt -> Hs.GDataDecl () htarget Nothing hd Nothing (map (uncurry conToGadtCon) cs) ds
+      _      -> Hs.DataDecl () htarget Nothing hd (map fst cs) ds
 
-    return [Hs.DataDecl () target Nothing hd cs ds]
+  where
+    conToGadtCon :: Hs.QualConDecl () -> Hs.Type () -> Hs.GadtDecl ()
+    conToGadtCon (Hs.QualConDecl _ tys ctx con) rt = case con of
+      Hs.ConDecl () c ts ->
+        Hs.GadtDecl () c tys ctx Nothing $
+          foldr (Hs.TyFun ()) rt ts
+      Hs.InfixConDecl{} -> __IMPOSSIBLE__
+      Hs.RecDecl{} -> __IMPOSSIBLE__
 
 allIndicesErased :: Type -> C ()
 allIndicesErased t = reduce (unEl t) >>= \case
@@ -64,19 +75,20 @@ allIndicesErased t = reduce (unEl t) >>= \case
     DomForall{}     -> agda2hsError "Not supported: indexed datatypes"
   _ -> return ()
 
-compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ())
+compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl (), Hs.Type ())
 compileConstructor params c = do
   reportSDoc "agda2hs.data.con" 15 $ text "compileConstructor" <+> prettyTCM c
   reportSDoc "agda2hs.data.con" 20 $ text "  params = " <+> prettyTCM params
   ty <- defType <$> getConstInfo c
   reportSDoc "agda2hs.data.con" 30 $ text "  ty (before piApply) = " <+> prettyTCM ty
   ty <- ty `piApplyM` params
   reportSDoc "agda2hs.data.con" 20 $ text "  ty = " <+> prettyTCM ty
-  TelV tel _ <- telView ty
+  TelV tel ret <- telView ty
   let conName = hsName $ prettyShow $ qnameName c
   checkValidConName conName
   args <- compileConstructorArgs tel
-  return $ Hs.QualConDecl () Nothing Nothing $ Hs.ConDecl () conName args
+  hret <- addContext tel $ compileType $ unEl ret
+  return (Hs.QualConDecl () Nothing Nothing $ Hs.ConDecl () conName args, hret)
 
 compileConstructorArgs :: Telescope -> C [Hs.Type ()]
 compileConstructorArgs EmptyTel = return []
@@ -132,12 +144,13 @@ checkCompileToDataPragma def s = noCheckNames $ do
   unless (length rcons == length dcons) $ fail
     "they have a different number of constructors"
   forM_ (zip dcons rcons) $ \(c1, c2) -> do
-    Hs.QualConDecl _ _ _ (Hs.ConDecl _ hsC1 args1) <-
+    (Hs.QualConDecl _ _ _ (Hs.ConDecl _ hsC1 args1) , rt1) <-
       addContext dtel $ compileConstructor (teleArgs dtel) c1
     -- rename parameters of r to match those of d
     rtel' <- renameParameters dtel rtel
-    Hs.QualConDecl _ _ _ (Hs.ConDecl _ hsC2 args2) <-
+    (Hs.QualConDecl _ _ _ (Hs.ConDecl _ hsC2 args2) , rt2) <-
       addContext rtel' $ compileConstructor (teleArgs rtel') c2
+    -- TODO: check that rt1 and rt2 are equal?
     unless (hsC1 == hsC2) $ fail $
       "name of constructor" <+> text (Hs.pp hsC1) <+>
       "does not match" <+> text (Hs.pp hsC2)

src/Agda2Hs/Compile/Record.hs

@@ -114,14 +114,14 @@ compileRecord target def = do
               assts  -> Just (Hs.CxTuple () assts)
         defaultDecls <- compileMinRecords def ms
         return $ Hs.ClassDecl () context hd [] (Just (classDecls ++ map (Hs.ClsDecl ()) defaultDecls))
-      ToRecord newtyp ds -> do
+      ToRecord dtarget ds -> do
         checkValidConName cName
         when (theEtaEquality recEtaEquality' == YesEta) $ agda2hsErrorM $
           "Agda records compiled to Haskell should have eta-equality disabled." <+>
           "Add no-eta-equality to the definition of" <+> (text (pp rName) <> ".")
         (constraints, fieldDecls) <- compileRecFields fieldDecl recFields fieldTel
-        when newtyp $ checkNewtypeCon cName fieldDecls
-        let target = if newtyp then Hs.NewType () else Hs.DataType ()
+        when (dtarget == ToNewType) $ checkNewtypeCon cName fieldDecls
+        let target = toDataTarget dtarget
         compileDataRecord constraints fieldDecls target hd ds
 
   where

src/Agda2Hs/Compile/Types.hs

@@ -210,12 +210,17 @@ data CompiledDom
   | DomDropped
     -- ^ To nothing (e.g. erased proofs)
 
--- | Whether a datatype/record should be compiled as a @newtype@ haskell definition.
-type AsNewType = Bool
+-- | Whether a datatype/record should be compiled as a @newtype@ haskell definition,
+--   a gadt-style datatype, or a regular datatype.
+data DataTarget
+  = ToNewType
+  | ToGadt
+  | ToData
+  deriving (Eq)
 
 -- | Compilation target for an Agda record definition.
 data RecordTarget
-  = ToRecord AsNewType [Hs.Deriving ()]
+  = ToRecord DataTarget [Hs.Deriving ()]
   | ToClass [String]
 
 -- | Compilation target for an Agda instance declaration.

src/Agda2Hs/Compile/Utils.hs

@@ -106,6 +106,11 @@ infixr 0 /\, \/
 f /\ g = \x -> f x && g x
 f \/ g = \x -> f x || g x
 
+toDataTarget :: DataTarget -> Hs.DataOrNew ()
+toDataTarget ToNewType = Hs.NewType ()
+toDataTarget ToData    = Hs.DataType ()
+toDataTarget ToGadt    = Hs.DataType ()
+
 showTCM :: PrettyTCM a => a -> C String
 showTCM x = liftTCM $ show <$> prettyTCM x
 
@@ -200,6 +205,7 @@ hasCompilePragma q = processPragma q <&> \case
   TransparentPragma{} -> True
   CompileToPragma{} -> True
   NewTypePragma{} -> True
+  GadtPragma{} -> True
   DerivePragma{} -> True
 
 -- Exploits the fact that the name of the record type and the name of the record module are the

src/Agda2Hs/Pragma.hs

@@ -56,6 +56,7 @@ data ParsedPragma
   | TransparentPragma
   | NewTypePragma [Hs.Deriving ()]
   | TuplePragma Hs.Boxed
+  | GadtPragma [Hs.Deriving ()]
   | CompileToPragma String
   | DerivePragma (Maybe (Hs.DerivStrategy ()))
   deriving (Eq, Show)
@@ -72,6 +73,9 @@ parseStrategy _          = Nothing
 newtypePragma :: String
 newtypePragma = "newtype"
 
+gadtPragma :: String
+gadtPragma = "gadt"
+
 processDeriving :: Range -> String -> ([Hs.Deriving ()] -> ParsedPragma) -> C ParsedPragma
 processDeriving r d pragma = do
   -- parse a deriving clause for a datatype by tacking it onto a
@@ -95,10 +99,12 @@ processPragma qn = liftTCM (getUniqueCompilerPragma pragmaName qn) >>= \case
     | s == "transparent"          -> return TransparentPragma
     | s == "tuple"                -> return $ TuplePragma Hs.Boxed
     | s == "unboxed-tuple"        -> return $ TuplePragma Hs.Unboxed
+    | s == "gadt"                 -> return $ GadtPragma []
     | "to" `isPrefixOf` s         -> return $ CompileToPragma (drop 3 s)
     | s == newtypePragma          -> return $ NewTypePragma []
     | s == derivePragma           -> return $ DerivePragma Nothing
     | derivePragma `isPrefixOf` s -> return $ DerivePragma (parseStrategy (drop (length derivePragma + 1) s))
     | "deriving"   `isPrefixOf` s -> processDeriving r s DefaultPragma
     | (newtypePragma ++ " deriving") `isPrefixOf` s -> processDeriving r (drop (length newtypePragma + 1) s) NewTypePragma
+    | (gadtPragma ++ " deriving") `isPrefixOf` s -> processDeriving r (drop (length gadtPragma + 1) s) GadtPragma
   _ -> return $ DefaultPragma []

test/AllTests.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --prop #-}
+{-# OPTIONS --prop --polarity #-}
 module AllTests where
 
 import AllCubicalTests
@@ -106,6 +106,7 @@ import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
 import RelevantDotPattern3
+import GadtSyntax
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -209,4 +210,5 @@ import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
 import RelevantDotPattern3
+import GadtSyntax
 #-}

test/GadtSyntax.agda

@@ -0,0 +1,13 @@
+{-# OPTIONS --polarity #-}
+
+open import Haskell.Prelude
+
+data Bol : Set where Tru Fls : Bol
+
+{-# COMPILE AGDA2HS Bol gadt #-}
+
+data Free (f : @++ Set → Set) (a : Set) : Set where
+  Return : a → Free f a
+  Roll : f (Free f a) → Free f a
+
+{-# COMPILE AGDA2HS Free gadt #-}

test/golden/AllTests.hs

@@ -101,4 +101,5 @@ import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
 import RelevantDotPattern3
+import GadtSyntax
 

test/golden/GadtSyntax.hs

@@ -0,0 +1,10 @@
+module GadtSyntax where
+
+data Bol where
+    Tru :: Bol
+    Fls :: Bol
+
+data Free f a where
+    Return :: a -> Free f a
+    Roll :: f (Free f a) -> Free f a
+