add pattern for 3-uple

agda · Dec 5, 2023 · ccbe3dc · ccbe3dc
1 parent cc79050
commit ccbe3dc
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 1 deletion.
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
@@ -44,7 +44,8 @@ import Agda.TypeChecking.Datatypes (isDataOrRecord)
 
 isSpecialPat :: QName -> Maybe (ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ()))
 isSpecialPat qn = case prettyShow qn of
-  "Haskell.Prim.Tuple._,_"   -> Just tuplePat
+  "Haskell.Prim.Tuple._,_"         -> Just tuplePat
+  "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tuplePat
   "Agda.Builtin.Int.Int.pos" -> Just posIntPat
   "Agda.Builtin.Int.Int.negsuc" -> Just negSucIntPat
   s | s `elem` badConstructors -> Just $ \ _ _ _ -> genericDocError =<<

diff --git a/test/Tuples.agda b/test/Tuples.agda
@@ -38,3 +38,10 @@ test : Int
 test = let (x , y) = pair in x + y
 
 {-# COMPILE AGDA2HS test #-}
+
+test2 : Bool
+test2 = case t1 of \where
+  (a , b , c) → c
+
+{-# COMPILE AGDA2HS test2 #-}
+
diff --git a/test/golden/Tuples.hs b/test/golden/Tuples.hs
@@ -20,3 +20,8 @@ pair = (1, 2)
 test :: Int
 test = fst pair + snd pair
 
+test2 :: Bool
+test2
+  = case t1 of
+        (a, b, c) -> c
+