Add support for unboxed datatypes, singletons

lib/Haskell/Extra/Singleton.agda

@@ -0,0 +1,28 @@
+module Haskell.Extra.Singleton where
+
+open import Haskell.Prelude hiding (pure; _<*>_)
+
+data Singleton (a : Set) : @0 a → Set where
+  MkSingl : ∀ x → Singleton a x
+{-# COMPILE AGDA2HS Singleton unboxed #-}
+
+module Idiom where
+
+  pure : {a : Set} (x : a) → Singleton a x
+  pure x = MkSingl x
+  {-# COMPILE AGDA2HS pure inline #-}
+
+  _<*>_ : {a b : Set} {@0 f : a → b} {@0 x : a}
+        → Singleton (a → b) f → Singleton a x → Singleton b (f x)
+  MkSingl f <*> MkSingl x = MkSingl (f x)
+  {-# COMPILE AGDA2HS _<*>_ inline #-}
+
+open Idiom public renaming (pure to pureSingl; _<*>_ to apSingl)
+
+fmapSingl
+  : {a b : Set} (f : a → b) {@0 x : a}
+  → Singleton a x
+  → Singleton b (f x)
+fmapSingl f (MkSingl x) = MkSingl (f x)
+{-# COMPILE AGDA2HS fmapSingl inline #-}
+

src/Agda2Hs/Compile.hs

@@ -20,10 +20,10 @@ import Agda.Utils.Monad ( whenM, anyM, when )
 import qualified Language.Haskell.Exts.Extension as Hs
 
 import Agda2Hs.Compile.ClassInstance ( compileInstance )
-import Agda2Hs.Compile.Data ( compileData )
+import Agda2Hs.Compile.Data ( compileData, checkUnboxedDataPragma )
 import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma, checkInlinePragma )
 import Agda2Hs.Compile.Postulate ( compilePostulate )
-import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma )
+import Agda2Hs.Compile.Record ( compileRecord, checkUnboxedRecordPragma )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils ( setCurrentRangeQ, tellExtension, primModules, isClassName )
 import Agda2Hs.Pragma
@@ -88,7 +88,8 @@ compile opts tlm _ def =
       case (p , theDef def) of
         (NoPragma            , _         ) -> return []
         (ExistingClassPragma , _         ) -> return []
-        (UnboxPragma s       , Record{}  ) -> [] <$ checkUnboxPragma def
+        (UnboxPragma s       , Record{}  ) -> [] <$ checkUnboxedRecordPragma def
+        (UnboxPragma s       , Datatype{}) -> [] <$ checkUnboxedDataPragma def
         (TransparentPragma   , Function{}) -> [] <$ checkTransparentPragma def
         (InlinePragma        , Function{}) -> [] <$ checkInlinePragma def
         (TuplePragma b       , Record{}  ) -> return []

src/Agda2Hs/Compile/Data.hs

@@ -2,7 +2,7 @@ module Agda2Hs.Compile.Data where
 
 import qualified Language.Haskell.Exts.Syntax as Hs
 
-import Control.Monad ( when )
+import Control.Monad ( unless, when )
 import Agda.Compiler.Backend
 import Agda.Syntax.Common
 import Agda.Syntax.Internal
@@ -14,8 +14,9 @@ import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Telescope
 
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
+import Agda.Utils.Monad ( mapMaybeM )
 
-import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds )
+import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.HsUtils
@@ -46,15 +47,15 @@ compileData newtyp ds def = do
     when newtyp (checkNewtype d cs)
 
     return [Hs.DataDecl () target Nothing hd cs ds]
-  where
-    allIndicesErased :: Type -> C ()
-    allIndicesErased t = reduce (unEl t) >>= \case
-      Pi dom t -> compileDomType (absName t) dom >>= \case
-        DomDropped      -> allIndicesErased (unAbs t)
-        DomType{}       -> genericDocError =<< text "Not supported: indexed datatypes"
-        DomConstraint{} -> genericDocError =<< text "Not supported: constraints in types"
-        DomForall{}     -> genericDocError =<< text "Not supported: indexed datatypes"
-      _ -> return ()
+
+allIndicesErased :: Type -> C ()
+allIndicesErased t = reduce (unEl t) >>= \case
+  Pi dom t -> compileDomType (absName t) dom >>= \case
+    DomDropped      -> allIndicesErased (unAbs t)
+    DomType{}       -> genericDocError =<< text "Not supported: indexed datatypes"
+    DomConstraint{} -> genericDocError =<< text "Not supported: constraints in types"
+    DomForall{}     -> genericDocError =<< text "Not supported: indexed datatypes"
+  _ -> return ()
 
 compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ())
 compileConstructor params c = do
@@ -77,3 +78,42 @@ compileConstructorArgs (ExtendTel a tel) = compileDomType (absName tel) a >>= \c
   DomConstraint hsA -> genericDocError =<< text "Not supported: constructors with class constraints"
   DomDropped        -> underAbstraction a tel compileConstructorArgs
   DomForall{}       -> __IMPOSSIBLE__
+
+
+checkUnboxedDataPragma :: Definition -> C ()
+checkUnboxedDataPragma def = do
+  let Datatype{..} = theDef def
+
+  -- unboxed datatypes shouldn't be recursive
+  unless (all null dataMutual) $ genericDocError
+    =<< text "Unboxed datatype" <+> prettyTCM (defName def)
+    <+> text "cannot be recursive"
+
+  TelV tel t <- telViewUpTo dataPars (defType def)
+  let params :: [Arg Term] = teleArgs tel
+
+  allIndicesErased t
+
+  case dataCons of
+    [con] -> do
+      info <- getConstInfo con
+      let Constructor {..} = theDef info
+      ty <- defType info `piApplyM` params
+      TelV conTel _ <- telView ty
+      args <- nonErasedArgs conTel
+      unless (length args == 1) $ genericDocError
+        =<< text "Unboxed datatype" <+> prettyTCM (defName def)
+        <+> text "should have a single constructor with exactly one non-erased argument."
+
+    _     -> genericDocError =<< text "Unboxed datatype" <+> prettyTCM (defName def)
+                             <+> text "must have exactly one constructor."
+
+  where
+    nonErasedArgs :: Telescope -> C [String]
+    nonErasedArgs EmptyTel = return []
+    nonErasedArgs (ExtendTel a tel) = compileDom a >>= \case
+      DODropped  -> underAbstraction a tel nonErasedArgs
+      DOType     -> genericDocError =<< text "Type argument in unboxed datatype not supported"
+      DOInstance -> genericDocError =<< text "Instance argument in unboxed datatype not supported"
+      DOTerm     -> (absName tel:) <$> underAbstraction a tel nonErasedArgs
+

src/Agda2Hs/Compile/Function.hs

@@ -399,7 +399,7 @@ checkInlinePragma def@Defn{defName = f} = do
     [c] ->
       unlessM (allowedPats (namedClausePats c)) $ genericDocError =<<
         "Cannot make function" <+> prettyTCM (defName def) <+> "inlinable." <+>
-        "Inline functions can only use variable patterns or transparent record constructor patterns."
+        "Inline functions can only use variable patterns or unboxed constructor patterns."
     _ ->
       genericDocError =<<
         "Cannot make function" <+> prettyTCM f <+> "inlinable." <+>
@@ -408,11 +408,16 @@ checkInlinePragma def@Defn{defName = f} = do
   where allowedPat :: DeBruijnPattern -> C Bool
         allowedPat VarP{} = pure True
         -- only allow matching on (unboxed) record constructors
-        allowedPat (ConP ch ci cargs) =
+        allowedPat (ConP ch ci cargs) = do
+          reportSDoc "agda2hs.compile.inline" 18 $ "Checking unboxing of constructor: "<+> prettyTCM ch
           isUnboxConstructor (conName ch) >>= \case
             Just _  -> allowedPats cargs
             Nothing -> pure False
-        allowedPat _ = pure False
+        -- NOTE(flupe): dot patterns should really only be allowed for *erased* arguments, I think.
+        allowedPat (DotP _ _) = pure True
+        allowedPat p = do
+          reportSDoc "agda2hs.compile.inline" 18 $ "Unsupported pattern"  <+> prettyTCM p
+          pure False
 
         allowedPats :: NAPs -> C Bool
         allowedPats pats = allM pats (allowedPat . dget . dget)

src/Agda2Hs/Compile/Record.hs

@@ -29,6 +29,7 @@ import Agda2Hs.Compile.Function ( compileFun )
 import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
+import Agda2Hs.Compile.Data ( allIndicesErased )
 import Agda2Hs.HsUtils
 
 -- | Primitive fields and default implementations
@@ -170,10 +171,9 @@ compileRecord target def = do
       let conDecl = Hs.QualConDecl () Nothing Nothing $ Hs.RecDecl () cName fieldDecls
       return $ Hs.DataDecl () don Nothing hd [conDecl] ds
 
-checkUnboxPragma :: Definition -> C ()
-checkUnboxPragma def = do
+checkUnboxedRecordPragma :: Definition -> C ()
+checkUnboxedRecordPragma def = do
   let Record{..} = theDef def
-
   -- recRecursive can be used again after agda 2.6.4.2 is released
   -- see agda/agda#7042
   unless (all null recMutual) $ genericDocError
@@ -197,3 +197,4 @@ checkUnboxPragma def = do
       DOType -> genericDocError =<< text "Type field in unboxed record not supported"
       DOInstance -> genericDocError =<< text "Instance field in unboxed record not supported"
       DOTerm -> (absName tel:) <$> underAbstraction a tel nonErasedFields
+

src/Agda2Hs/Compile/Term.hs

@@ -53,13 +53,13 @@ type DefCompileRule = Type -> [Term] -> C (Hs.Exp ())
 
 isSpecialDef :: QName -> Maybe DefCompileRule
 isSpecialDef q = case prettyShow q of
-  _ | isExtendedLambdaName q     -> Just (lambdaCase q)
-  "Haskell.Prim.if_then_else_"   -> Just ifThenElse
-  "Haskell.Prim.case_of_"        -> Just caseOf
-  "Haskell.Prim.the"             -> Just expTypeSig
-  "Haskell.Extra.Delay.runDelay" -> Just compileErasedApp
+  _ | isExtendedLambdaName q            -> Just (lambdaCase q)
+  "Haskell.Prim.if_then_else_"          -> Just ifThenElse
+  "Haskell.Prim.case_of_"               -> Just caseOf
+  "Haskell.Prim.the"                    -> Just expTypeSig
+  "Haskell.Extra.Delay.runDelay"        -> Just compileErasedApp
   "Agda.Builtin.Word.primWord64FromNat" -> Just primWord64FromNat
-  _                              -> Nothing
+  _                                     -> Nothing
 
 
 -- | Compile a @\where@ to the equivalent @\case@ expression.
@@ -153,6 +153,8 @@ compileSpined c tm ty (e@(Proj o q):es) = do
   ty' <- shouldBeProjectible t ty o q
   compileSpined (compileProj q ty t ty') (tm . (e:)) ty' es
 compileSpined c tm ty (e@(Apply (unArg -> x)):es) = do
+  reportSDoc "agda2hs.compile.inline" 18 $ text "spined term" <+> prettyTCM (tm (e:es))
+  reportSDoc "agda2hs.compile.inline" 18 $ text "spined type" <+> prettyTCM ty
   (a, b) <- mustBePi ty
   compileSpined (c . (x:)) (tm . (e:)) (absApp b x) es
 compileSpined _ _ _ _ = __IMPOSSIBLE__
@@ -536,11 +538,65 @@ compileInlineFunctionApp f ty args = do
 
   def <- getConstInfo f
 
-  let ty' = defType def
-  let Function{funClauses = cs} = theDef def
-  let [Clause{namedClausePats = pats}] = filter (isJust . clauseBody) cs
+  let Function{ funClauses = cs } = theDef def
+  let [ Clause { namedClausePats = pats
+               , clauseBody = Just body
+               , clauseTel
+               } ] = filter (isJust . clauseBody) cs
+
+  reportSDoc "agda2hs.compile.inline" 18 $ text "inline function pats " <+> pretty pats
+  reportSDoc "agda2hs.compile.inline" 18 $ text "inline function args " <+> prettyTCM args
+  reportSDoc "agda2hs.compile.inline" 18 $ text "inline function length of tel" <+> prettyTCM (length clauseTel)
+  reportSDoc "agda2hs.compile.inline" 18 $ text "ctxt" <+> (prettyTCM =<< getContextArgs)
 
   ty'' <- piApplyM ty args
+  let ntel = length clauseTel
+
+  -- body' <- addContext clauseTel $ do
+  -- sub <- matchPats pats (raise ntel args)
+    -- reportSDoc "agda2hs.compile.inline" 18 $ text "Generated substitution: " <+> prettyTCM body
+
+
+  addContext (KeepNames clauseTel) $ do
+    matchPats pats (raise ntel args) (compileTerm (raise ntel ty'')) body
+    -- reportSDoc "agda2hs.compile.inline" 18 $ text "function body before substitution: " <+> prettyTCM body
+    -- reportSDoc "agda2hs.compile.inline" 18 $ text "function body after substitution: "  <+> prettyTCM body'
+    -- compileTerm (raise ntel ty'') body'
+
+  where
+    matchPats :: NAPs -> [Term] -> (Term -> C (Hs.Exp ())) -> Term -> C (Hs.Exp ()) -- Substitution
+    matchPats [] [] c tm = c tm -- pure IdS
+    matchPats (pat:naps) (t:ts) c tm -- dot patterns are ignored
+      | DotP _ _ <- namedThing (unArg pat) = matchPats naps ts c tm
+    matchPats (pat:naps) (t:ts) c tm = do
+      -- each pattern of inlined funtions match a single variable
+      let var = dbPatVarIndex $ extractPatVar (namedThing $ unArg pat)
+      reportSDoc "agda2hs.compile.inline" 18
+        $ text "replacing db var" <+> prettyTCM (Var var []) <+> text "with" <+> prettyTCM t
+
+      -- TODO: improve this
+      matchPats naps ts c (applySubst (inplaceS var t) tm)
+      -- composeS (singletonS (dbPatVarIndex var) t) <$> matchPats naps ts
+    matchPats (pat:naps) [] c tm = do
+      -- exhausted explicit arguments, yet the inline function is not fully applied.
+      -- we eta-expand with as many missing arguments
+      let name = dbPatVarName (extractPatVar (namedThing $ unArg pat))
+      hsLambda name <$> matchPats naps [] c tm
+      -- mkLam (defaultArg name) <$> matchPats naps [] tm
+
+    extractPatVar :: DeBruijnPattern -> DBPatVar
+    extractPatVar (VarP _ v) = v
+    extractPatVar (ConP _ _ args) =
+      let arg = namedThing $ unArg $ head $ filter (usableModality `and2M` visible) args
+      in extractPatVar arg
+    extractPatVar _ = __IMPOSSIBLE__
+
+
+-- NOTE(flupe): for now, we assume that inline functions are fully applied
+--              once this works, we need to add back eta-expansion.
+
+  -- undefined
+  {-
   -- NOTE(flupe): very flimsy, there has to be a better way
   etaExpand (drop (length args) pats) ty' args >>= compileTerm ty''
 
@@ -571,6 +627,7 @@ compileInlineFunctionApp f ty args = do
       (dom, cod) <- mustBePi ty
       let ai = domInfo dom
       Lam ai . mkAbs (extractName p) <$> etaExpand ps (absBody cod) (raise 1 args ++ [ var 0 ])
+      -}
 
 
 compileApp :: Hs.Exp () -> Type -> [Term] -> C (Hs.Exp ())

src/Agda2Hs/Compile/Type.hs

@@ -9,6 +9,7 @@ import Control.Monad.Trans ( lift )
 import Control.Monad.Reader ( asks )
 import Data.List ( find )
 import Data.Maybe ( mapMaybe, isJust )
+import Data.Foldable ( toList )
 import qualified Data.Set as Set ( singleton )
 
 import qualified Language.Haskell.Exts.Syntax as Hs
@@ -21,6 +22,7 @@ import Agda.Syntax.Common
 import Agda.Syntax.Internal
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
+import Agda.TypeChecking.Datatypes
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Reduce ( reduce, unfoldDefinitionStep )
 import Agda.TypeChecking.Substitute
@@ -76,7 +78,7 @@ delayType [] = genericDocError =<< text "Cannot compile unapplied Delay type"
 compileTypeWithStrictness :: Term -> C (Strictness, Hs.Type ())
 compileTypeWithStrictness t = do
   s <- case t of
-    Def f es -> fromMaybe Lazy <$> isUnboxRecord f
+    Def f es -> fromMaybe Lazy <$> isUnboxType f
     _        -> return Lazy
   ty <- compileType t
   pure (s, ty)
@@ -106,7 +108,7 @@ compileType t = do
               <+> text "in Haskell type"
          | Just semantics <- isSpecialType f -> setCurrentRange f $ semantics es
          | Just args <- allApplyElims es ->
-             ifJustM (isUnboxRecord f) (\_ -> compileUnboxType f args) $
+             ifJustM (isUnboxType f) (\_ -> compileUnboxType f args) $
              ifJustM (isTupleRecord f) (\b -> compileTupleType f b args) $
              ifM (isTransparentFunction f) (compileTransparentType (defType def) args) $
              ifM (isInlinedFunction f) (compileInlineType f es) $ do
@@ -174,11 +176,31 @@ compileTelSize (ExtendTel a tel) = compileDom a >>= \case
 compileUnboxType :: QName -> Args -> C (Hs.Type ())
 compileUnboxType r pars = do
   def <- getConstInfo r
-  let tel = recTel (theDef def) `apply` pars
+
+  tel <- case theDef def of
+
+    Record{recTel} -> pure (recTel `apply` pars)
+
+    Datatype{dataCons = [con]} -> do
+      -- NOTE(flupe): con is the *only* constructor of the unboxed datatype
+      Constructor { conSrcCon } <- theDef <$> getConstInfo con
+      -- we retrieve its type
+      Just (_, ty) <- getConType conSrcCon (El (DummyS "some level") (apply (Def r []) pars))
+      theTel <$> telView ty
+
   compileTel tel >>= \case
     [t] -> return t
     _   -> __IMPOSSIBLE__
 
+  where
+    compileTel :: Telescope -> C [Hs.Type ()]
+    compileTel EmptyTel = return []
+    compileTel (ExtendTel a tel) = compileDom a >>= \case
+      DODropped  -> underAbstraction a tel compileTel
+      DOInstance -> __IMPOSSIBLE__
+      DOType     -> __IMPOSSIBLE__
+      DOTerm     -> (:) <$> compileType (unEl $ unDom a) <*> underAbstraction a tel compileTel
+
 compileTupleType :: QName -> Hs.Boxed -> Args -> C (Hs.Type ())
 compileTupleType r b pars = do
   tellUnboxedTuples b
@@ -192,7 +214,6 @@ compileTransparentType ty args = compileTypeArgs ty args >>= \case
   (v:vs) -> return $ v `tApp` vs
   []     -> __IMPOSSIBLE__
 
-
 compileInlineType :: QName -> Elims -> C (Hs.Type ())
 compileInlineType f args = do
   Function { funClauses = cs } <- theDef <$> getConstInfo f