add Extra.Sigma

lib/Haskell/Extra/Sigma.agda

@@ -0,0 +1,16 @@
+module Haskell.Extra.Sigma where
+
+record Σ (a : Set) (b : @0 a → Set) : Set where
+  constructor _,_
+  field
+    fst : a
+    snd : b fst
+open Σ public
+
+infix 2 Σ-syntax
+
+Σ-syntax : (a : Set) → (@0 a → Set) → Set
+Σ-syntax = Σ
+{-# COMPILE AGDA2HS Σ-syntax inline #-}
+
+syntax Σ-syntax a (λ x → b) = Σ[ x ∈ a ] b

src/Agda2Hs/Compile/Term.hs

@@ -337,6 +337,7 @@ isSpecialCon :: QName -> Maybe ConCompileRule
 isSpecialCon = prettyShow >>> \case
   "Haskell.Prim.Tuple._,_"          -> Just tupleTerm
   "Haskell.Prim.Tuple._×_×_._,_,_"  -> Just tupleTerm
+  "Haskell.Extra.Sigma._,_"         -> Just tupleTerm
   "Haskell.Extra.Erase.Erased"      -> Just erasedTerm
   "Haskell.Extra.Delay.Delay.now"   -> Just compileErasedApp
   "Haskell.Extra.Delay.Delay.later" -> Just compileErasedApp

src/Agda2Hs/Compile/Type.hs

@@ -46,6 +46,7 @@ isSpecialType :: QName -> Maybe (Elims -> C (Hs.Type ()))
 isSpecialType = prettyShow >>> \case
   "Haskell.Prim.Tuple._×_"    -> Just tupleType
   "Haskell.Prim.Tuple._×_×_"  -> Just tupleType
+  "Haskell.Extra.Sigma.Σ"     -> Just tupleType
   "Haskell.Extra.Erase.Erase" -> Just unitType
   "Haskell.Extra.Delay.Delay" -> Just delayType
   _                           -> Nothing

test/Tuples.agda

@@ -45,3 +45,12 @@ test2 = case t1 of \where
 
 {-# COMPILE AGDA2HS test2 #-}
 
+open import Haskell.Extra.Sigma as S using (Σ-syntax)
+open import Haskell.Extra.Dec
+open import Haskell.Prim using (itsTrue)
+open import Haskell.Extra.Refinement
+
+t4 : Σ[ n ∈ Nat ] (Dec (IsTrue (n <= 5)))
+t4 = 3 S., (True ⟨ itsTrue ⟩)
+
+{-# COMPILE AGDA2HS t4 #-}

test/golden/Tuples.hs

@@ -1,5 +1,7 @@
 module Tuples where
 
+import Numeric.Natural (Natural)
+
 swap :: (a, b) -> (b, a)
 swap (a, b) = (b, a)
 
@@ -25,3 +27,6 @@ test2
   = case t1 of
         (a, b, c) -> c
 
+t4 :: (Natural, Bool)
+t4 = (3, True)
+