[ fix agda#310 ] compile Sigma pattern

jespercockx · Apr 12, 2024 · 1ddeb68 · 1ddeb68
1 parent 4e66970
commit 1ddeb68
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 0 deletions.
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
@@ -56,6 +56,7 @@ isSpecialCon qn = case prettyShow qn of
   "Haskell.Prim.Tuple._,_"         -> Just tuplePat
   "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tuplePat
   "Haskell.Extra.Erase.Erased"     -> Just tuplePat
+  "Haskell.Extra.Sigma._,_"        -> Just tuplePat
   "Agda.Builtin.Int.Int.pos"       -> Just posIntPat
   "Agda.Builtin.Int.Int.negsuc"    -> Just negSucIntPat
   _                                -> Nothing

diff --git a/test/Tuples.agda b/test/Tuples.agda
@@ -54,3 +54,8 @@ t4 : Σ[ n ∈ Nat ] (Dec (IsTrue (n <= 5)))
 t4 = 3 S., (True ⟨ itsTrue ⟩)
 
 {-# COMPILE AGDA2HS t4 #-}
+
+t5 : Σ[ x ∈ a ] b → a
+t5 p = case p of λ where (x S., y) → x
+
+{-# COMPILE AGDA2HS t5 #-}
diff --git a/test/golden/Tuples.hs b/test/golden/Tuples.hs
@@ -30,3 +30,8 @@ test2
 t4 :: (Natural, Bool)
 t4 = (3, True)
 
+t5 :: (a, b) -> a
+t5 p
+  = case p of
+        (x, y) -> x
+