[fix #215] handle automatic projections from let pattern of tuples

src/Agda2Hs/Compile/Term.hs

@@ -5,7 +5,7 @@ import Control.Monad ( unless )
 import Control.Monad.Reader
 
 import Data.List ( isPrefixOf )
-import Data.Maybe ( fromMaybe, isJust )
+import Data.Maybe ( fromMaybe, isJust, listToMaybe )
 import qualified Data.Text as Text ( unpack )
 
 import qualified Language.Haskell.Exts as Hs
@@ -46,6 +46,7 @@ isSpecialTerm q = case prettyShow q of
   "Haskell.Prim.case_of_"                       -> Just caseOf
   "Haskell.Prim.Monad.Do.Monad._>>=_"           -> Just bind
   "Haskell.Prim.Monad.Do.Monad._>>_"            -> Just sequ
+  "Haskell.Prim.Tuple.Pair.fst"                 -> Just (const tupleProj)
   "Agda.Builtin.FromNat.Number.fromNat"         -> Just fromNat
   "Agda.Builtin.FromNeg.Negative.fromNeg"       -> Just fromNeg
   "Agda.Builtin.FromString.IsString.fromString" -> Just fromString
@@ -66,6 +67,13 @@ tupleTerm cons i es = do
   ts <- mapM compileTerm xs
   return $ Hs.Tuple () Hs.Boxed ts
 
+tupleProj :: Elims -> C (Hs.Exp ())
+tupleProj elims = do
+  let t = unArg $ fromMaybe __IMPOSSIBLE__ (listToMaybe =<< allApplyElims elims)
+  case unSpine1 t of
+    Def q es | q ~~ "Haskell.Prim.Tuple.Pair.snd" -> compileTerm t
+    _ -> Hs.App () (hsVar "fst") <$> compileTerm t
+
 ifThenElse :: QName -> Elims -> C (Hs.Exp ())
 ifThenElse _ es = compileElims es >>= \case
   -- fully applied

test/Tuples.agda

@@ -33,3 +33,13 @@ t3 : Bool × (Bool × Bool)
 t3 = True , (False , True)
 
 {-# COMPILE AGDA2HS t3 #-}
+
+pair : Int × Int
+pair = (1 , 2)
+
+{-# COMPILE AGDA2HS pair #-}
+
+test : Int
+test = let (x , y) = pair in x + y
+
+{-# COMPILE AGDA2HS test #-}

test/golden/Tuples.hs

@@ -17,3 +17,9 @@ t2 = ((True, False), True)
 t3 :: (Bool, (Bool, Bool))
 t3 = (True, (False, True))
 
+pair :: (Int, Int)
+pair = (1, 2)
+
+test :: Int
+test = fst pair + snd pair
+