[ first part of #105 ] Add support for compiling records to Haskell t…

…uples

agda2hs.cabal

@@ -86,4 +86,5 @@ executable agda2hs
                        ViewPatterns
                        NamedFieldPuns
                        PatternSynonyms
+                       NondecreasingIndentation
   ghc-options:         -Werror -rtsopts

src/Agda2Hs/Compile.hs

@@ -91,6 +91,7 @@ compile opts tlm _ def =
         (UnboxPragma s       , Record{}  ) -> [] <$ checkUnboxPragma def
         (TransparentPragma   , Function{}) -> [] <$ checkTransparentPragma def
         (InlinePragma        , Function{}) -> [] <$ checkInlinePragma def
+        (TuplePragma b       , Record{}  ) -> return []
 
         (ClassPragma ms      , Record{}  ) -> pure <$> compileRecord (ToClass ms) def
         (NewTypePragma ds    , Record{}  ) -> pure <$> compileRecord (ToRecord True ds) def

src/Agda2Hs/Compile/Function.hs

@@ -302,16 +302,14 @@ compilePat ty p@(VarP o x)
 -- special constructor pattern
 compilePat ty (ConP ch i ps) = do
   Just ((_, _, _), ty) <- getConType ch =<< reduce ty
+  let c = conName ch
 
-  case isSpecialCon (conName ch) of
-    Just semantics -> setCurrentRange ch $ semantics ty ps
-    Nothing -> do
-      isUnboxConstructor (conName ch) >>= \case
-        Just s -> compileErasedConP ty ps >>= addPatBang s
-        Nothing -> do
-          ps <- compilePats ty ps
-          c <- compileQName (conName ch)
-          return $ pApp c ps
+  ifJust (isSpecialCon c) (\semantics -> setCurrentRange ch $ semantics ty ps) $ do
+  ifJustM (isUnboxConstructor c) (\s -> compileErasedConP ty s ps) $ do
+  ifJustM (isTupleConstructor c) (\b -> compileTupleConP ty b ps) $ do
+    ps <- compilePats ty ps
+    c <- compileQName (conName ch)
+    return $ pApp c ps
 
 -- literal patterns
 compilePat ty (LitP _ l) = compileLitPat l
@@ -321,16 +319,20 @@ compilePat ty (LitP _ l) = compileLitPat l
 compilePat _ p = genericDocError =<< "bad pattern:" <?> prettyTCM p
 
 
-compileErasedConP :: Type -> NAPs -> C (Hs.Pat ())
-compileErasedConP ty ps = compilePats ty ps <&> \case
-  [p] -> p
+compileErasedConP :: Type -> Strictness -> NAPs -> C (Hs.Pat ())
+compileErasedConP ty s ps = compilePats ty ps >>= \case
+  [p] -> addPatBang s p
   _   -> __IMPOSSIBLE__
 
 compileLitPat :: Literal -> C (Hs.Pat ())
 compileLitPat = \case
   LitChar c -> return $ Hs.charP c
   l -> genericDocError =<< "bad literal pattern:" <?> prettyTCM l
 
+compileTupleConP :: Type -> Hs.Boxed -> NAPs -> C (Hs.Pat ())
+compileTupleConP ty b ps = do
+  ps <- compilePats ty ps
+  return $ Hs.PTuple () b ps
 
 -- Local (where) declarations ---------------------------------------------
 

src/Agda2Hs/Compile/Term.hs

@@ -1,6 +1,6 @@
 module Agda2Hs.Compile.Term where
 
-import Control.Arrow ( (>>>), (&&&) )
+import Control.Arrow ( (>>>), (&&&), second )
 import Control.Monad ( unless )
 import Control.Monad.Reader
 
@@ -30,13 +30,14 @@ import Agda.TypeChecking.ProjectionLike ( reduceProjectionLike )
 
 import Agda.Utils.Lens
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
+import Agda.Utils.Maybe
 import Agda.Utils.Monad
 import Agda.Utils.Size
 
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName )
 
-import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..) )
+import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTelSize )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var ( compileDBVar )
@@ -229,6 +230,8 @@ compileProj q tty t ty args | Just rule <- isSpecialProj q = rule tty t ty args
 compileProj q tty t ty args =
   -- unboxed projection: we drop the projection
   ifM (isJust <$> isUnboxProjection q) (eApp <$> compileTerm tty t <*> compileArgs ty args) $
+  -- tuple projection: TODO
+  ifM (isJust <$> isTupleProjection q) (genericError "Not supported: tuple projections") $
   -- class projection: we check the instance and drop it
   ifM (isClassFunction q) (compileClassFun q tty t ty args) $
 
@@ -365,22 +368,47 @@ compileErasedApp ty args = do
 
 
 compileCon :: ConHead -> ConInfo -> Type -> [Term] -> C (Hs.Exp ())
-compileCon h i ty args
-  | Just semantics <- isSpecialCon (conName h)
-  = semantics ty args
 compileCon h i ty args = do
-  isUnboxConstructor (conName h) >>= \case
-    Just _  -> compileErasedApp ty args
-    Nothing -> do
-      info <- getConstInfo (conName h)
-      -- the constructor may be a copy introduced by module application,
-      -- therefore we need to find the original constructor
-      if defCopy info then
-        let Constructor{conSrcCon = ch'} = theDef info in
-        compileCon ch' i ty args
-      else do
-        con <- Hs.Con () <$> compileQName (conName h)
-        compileApp con ty args
+  let c = conName h
+  ifJust  (isSpecialCon c)       (\semantics -> semantics ty args) $ do
+  ifJustM (isUnboxConstructor c) (\_ -> compileErasedApp ty args)  $ do
+  ifJustM (isTupleConstructor c) (\b -> compileTuple ty b args)    $ do
+    info <- getConstInfo c
+    -- the constructor may be a copy introduced by module application,
+    -- therefore we need to find the original constructor
+    if defCopy info then
+      let Constructor{conSrcCon = ch'} = theDef info in
+      compileCon ch' i ty args
+    else do
+      con <- Hs.Con () <$> compileQName c
+      compileApp con ty args
+
+compileTuple :: Type -> Hs.Boxed -> [Term] -> C (Hs.Exp ())
+compileTuple ty b args = do
+  tellUnboxedTuples b
+  (ty', vs) <- compileArgs' ty args
+  TelV tel _ <- telView ty'
+  missing <- compileTelSize tel
+  let given = size vs
+  if -- No arguments: return unit constructor () or (# #)
+     | given == 0 && missing == 0 -> return $
+         Hs.Con () $ Hs.Special () $ case b of
+           Hs.Boxed -> Hs.UnitCon ()
+           Hs.Unboxed -> Hs.UnboxedSingleCon ()
+     -- All arguments missing: return tuple constructor
+     -- e.g. (,) or (#,#)
+     | given == 0 -> return $
+         Hs.Con () $ Hs.Special () $ Hs.TupleCon () b missing
+     -- All arguments given: return tuple
+     -- e.g. (v1 , v2) or (# v1 , v2 #)
+     | missing == 0 -> return $ Hs.Tuple () b vs
+     -- Some arguments given, some missing: return tuple section
+     -- e.g. (v1 ,) or (# v1, #)
+     | otherwise -> do
+         tellExtension $ Hs.TupleSections
+         return $ Hs.TupleSection () b $
+           map Just vs ++ replicate missing Nothing
+
 
 
 -- * Term compilation
@@ -525,16 +553,18 @@ compileApp' acc ty args = acc <$> compileArgs ty args
 
 -- | Compile a list of arguments applied to a function of the given type.
 compileArgs :: Type -> [Term] -> C [Hs.Exp ()]
-compileArgs ty [] = pure []
-compileArgs ty (x:xs) = do
+compileArgs ty args = snd <$> compileArgs' ty args
+
+compileArgs' :: Type -> [Term] -> C (Type, [Hs.Exp ()])
+compileArgs' ty [] = pure (ty, [])
+compileArgs' ty (x:xs) = do
   (a, b) <- mustBePi ty
-  let rest = compileArgs (absApp b x) xs
+  let rest = compileArgs' (absApp b x) xs
   compileDom a >>= \case
     DODropped  -> rest
     DOInstance -> checkInstance x *> rest
     DOType     -> rest
-    DOTerm     -> (:) <$> compileTerm (unDom a) x
-                      <*> rest
+    DOTerm     -> second . (:) <$> compileTerm (unDom a) x <*> rest
 
 clauseToAlt :: Hs.Match () -> C (Hs.Alt ())
 clauseToAlt (Hs.Match _ _ [p] rhs wh) = pure $ Hs.Alt () p rhs wh

src/Agda2Hs/Compile/Type.hs

@@ -107,6 +107,7 @@ compileType t = do
          | Just semantics <- isSpecialType f -> setCurrentRange f $ semantics es
          | Just args <- allApplyElims es ->
              ifJustM (isUnboxRecord 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
                vs <- compileTypeArgs (defType def) args
@@ -152,6 +153,23 @@ compileTypeArgs ty (x:xs) = do
       (:) <$> compileType (unArg x) <*> rest
     DOTerm -> fail "Type-level term argument not supported"
 
+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
+
+-- Version of @compileTel@ that just computes the size,
+-- and avoids compiling the types themselves.
+compileTelSize :: Telescope -> C Int
+compileTelSize EmptyTel = return 0
+compileTelSize (ExtendTel a tel) = compileDom a >>= \case
+  DODropped -> underAbstraction a tel compileTelSize
+  DOInstance -> __IMPOSSIBLE__
+  DOType -> __IMPOSSIBLE__
+  DOTerm -> (1+) <$> underAbstraction a tel compileTelSize
 
 compileUnboxType :: QName -> Args -> C (Hs.Type ())
 compileUnboxType r pars = do
@@ -160,16 +178,15 @@ compileUnboxType r pars = do
   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
+  def <- getConstInfo r
+  let tel = recTel (theDef def) `apply` pars
+  ts <- compileTel tel
+  return $ Hs.TyTuple () b ts
+
 compileTransparentType :: Type -> Args -> C (Hs.Type ())
 compileTransparentType ty args = compileTypeArgs ty args >>= \case
   (v:vs) -> return $ v `tApp` vs

src/Agda2Hs/Compile/Utils.hs

@@ -200,6 +200,23 @@ isUnboxProjection :: QName -> C (Maybe Strictness)
 isUnboxProjection q =
   caseMaybeM (liftTCM $ getRecordOfField q) (return Nothing) isUnboxRecord
 
+isTupleRecord :: QName -> C (Maybe Hs.Boxed)
+isTupleRecord q = do
+  getConstInfo q >>= \case
+    Defn{defName = r, theDef = Record{}} ->
+      processPragma r <&> \case
+        TuplePragma b -> Just b
+        _             -> Nothing
+    _ -> return Nothing
+
+isTupleConstructor :: QName -> C (Maybe Hs.Boxed)
+isTupleConstructor q =
+  caseMaybeM (isRecordConstructor q) (return Nothing) $ isTupleRecord . fst
+
+isTupleProjection :: QName -> C (Maybe Hs.Boxed)
+isTupleProjection q =
+  caseMaybeM (liftTCM $ getRecordOfField q) (return Nothing) isTupleRecord
+
 isTransparentFunction :: QName -> C Bool
 isTransparentFunction q = do
   getConstInfo q >>= \case
@@ -288,6 +305,10 @@ tellImport imp = tell $ CompileOutput [imp] []
 tellExtension :: Hs.KnownExtension -> C ()
 tellExtension pr = tell $ CompileOutput [] [pr]
 
+tellUnboxedTuples :: Hs.Boxed -> C ()
+tellUnboxedTuples Hs.Boxed = return ()
+tellUnboxedTuples Hs.Unboxed = tellExtension $ Hs.UnboxedTuples
+
 addPatBang :: Strictness -> Hs.Pat () -> C (Hs.Pat ())
 addPatBang Strict p = tellExtension Hs.BangPatterns >>
   return (Hs.PBangPat () p)

src/Agda2Hs/Pragma.hs

@@ -55,6 +55,7 @@ data ParsedPragma
   | UnboxPragma Strictness
   | TransparentPragma
   | NewTypePragma [Hs.Deriving ()]
+  | TuplePragma Hs.Boxed
   | DerivePragma (Maybe (Hs.DerivStrategy ()))
   deriving (Eq, Show)
 
@@ -91,6 +92,8 @@ processPragma qn = liftTCM (getUniqueCompilerPragma pragmaName qn) >>= \case
     | s == "unboxed"              -> return $ UnboxPragma Lazy
     | s == "unboxed-strict"       -> return $ UnboxPragma Strict
     | s == "transparent"          -> return TransparentPragma
+    | s == "tuple"                -> return $ TuplePragma Hs.Boxed
+    | s == "unboxed-tuple"        -> return $ TuplePragma Hs.Unboxed
     | s == newtypePragma          -> return $ NewTypePragma []
     | s == derivePragma           -> return $ DerivePragma Nothing
     | derivePragma `isPrefixOf` s -> return $ DerivePragma (parseStrategy (drop (length derivePragma + 1) s))

test/AllTests.agda

@@ -86,6 +86,7 @@ import Issue302
 import Issue309
 import Issue317
 import ErasedPatternLambda
+import CustomTuples
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -169,4 +170,5 @@ import Issue302
 import Issue309
 import Issue317
 import ErasedPatternLambda
+import CustomTuples
 #-}

test/CustomTuples.agda

@@ -0,0 +1,50 @@
+open import Haskell.Prelude
+
+record Stuff (a : Set) : Set where
+  no-eta-equality; pattern
+  constructor stuff
+  field
+    something : Int
+    more : a
+    another : Bool
+
+{-# COMPILE AGDA2HS Stuff unboxed-tuple #-}
+
+foo : Stuff Int → Stuff Bool → Stuff Char
+foo (stuff a b c) (stuff x y z) = stuff (a + b + x) 'x' (or (c ∷ y ∷ z ∷ []))
+
+{-# COMPILE AGDA2HS foo #-}
+
+bare : Int → Char → Bool → Stuff Char
+bare = stuff
+
+{-# COMPILE AGDA2HS bare #-}
+
+section : a → Bool → Stuff a
+section = stuff 42
+
+{-# COMPILE AGDA2HS section #-}
+
+record NoStuff : Set where
+  no-eta-equality; pattern
+  constructor dontlook
+
+{-# COMPILE AGDA2HS NoStuff tuple #-}
+
+bar : NoStuff → NoStuff
+bar dontlook = dontlook
+
+{-# COMPILE AGDA2HS bar #-}
+
+-- This is legal, basically the same as an unboxed record.
+record Legal (a : Set) : Set where
+  constructor mkLegal
+  field
+    theA : a
+
+{-# COMPILE AGDA2HS Legal tuple #-}
+
+baz : Legal Int → Legal Int
+baz (mkLegal x) = mkLegal 42
+
+{-# COMPILE AGDA2HS baz #-}

test/golden/AllTests.hs

@@ -81,4 +81,5 @@ import Issue302
 import Issue309
 import Issue317
 import ErasedPatternLambda
+import CustomTuples
 

test/golden/CustomTuples.hs

@@ -0,0 +1,21 @@
+{-# LANGUAGE UnboxedTuples, TupleSections #-}
+module CustomTuples where
+
+foo ::
+    (# Int, Int, Bool #) ->
+      (# Int, Bool, Bool #) -> (# Int, Char, Bool #)
+foo (# a, b, c #) (# x, y, z #)
+  = (# a + b + x, 'x', or [c, y, z] #)
+
+bare :: Int -> Char -> Bool -> (# Int, Char, Bool #)
+bare = (# ,, #)
+
+section :: a -> Bool -> (# Int, a, Bool #)
+section = (# 42, , #)
+
+bar :: () -> ()
+bar () = ()
+
+baz :: (Int) -> (Int)
+baz (x) = (42)
+