add some checks again

src/Agda2Hs/Compile/Function.hs

@@ -51,12 +51,23 @@ import Agda.TypeChecking.Datatypes (isDataOrRecord)
 -- | Compilation rules for specific constructors in patterns.
 isSpecialCon :: QName -> Maybe (Type -> NAPs -> C (Hs.Pat ()))
 isSpecialCon qn = case prettyShow qn of
+  s | s `elem` badConstructors     -> Just itsBad
   "Haskell.Prim.Tuple._,_"         -> Just tuplePat
   "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tuplePat
   "Haskell.Extra.Erase.Erased"     -> Just tuplePat
   "Agda.Builtin.Int.Int.pos"       -> Just posIntPat
   "Agda.Builtin.Int.Int.negsuc"    -> Just negSucIntPat
   _                                -> Nothing
+  where
+    badConstructors =
+      [ "Agda.Builtin.Nat.Nat.zero"
+      , "Agda.Builtin.Nat.Nat.suc"
+      , "Haskell.Extra.Delay.Delay.now"
+      , "Haskell.Extra.Delay.Delay.later"
+      ]
+
+    itsBad :: Type -> NAPs -> C (Hs.Pat ())
+    itsBad _ _ = genericDocError =<< "constructor `" <> prettyTCM qn <> "` not supported in patterns"
 
 -- | Translate list of patterns into a Haskell n-uple pattern.
 tuplePat :: Type -> NAPs -> C (Hs.Pat ())
@@ -91,23 +102,6 @@ compileLitNatPat = \case
     , [p] <- ps -> (1+) <$> compileLitNatPat (namedArg p)
   p -> genericDocError =<< "not a literal natural number pattern:" <?> prettyTCM p
 
-  {-
-  case prettyShow qn of
-  s | s `elem` badConstructors     -> Just $ \ _ -> genericDocError =<<
-    "constructor `" <> prettyTCM qn <> "` not supported in patterns"
-  _                                -> Nothing
-  where
-    badConstructors =
-      [ "Agda.Builtin.Nat.Nat.zero"
-      , "Agda.Builtin.Nat.Nat.suc"
-      , "Haskell.Extra.Delay.Delay.now"
-      , "Haskell.Extra.Delay.Delay.later"
-      ]
-
-
-
-
--}
 
 compileFun, compileFun'
   :: Bool -- ^ Whether the type signature shuuld also be generated
@@ -216,10 +210,21 @@ compileClause' curModule x ty c@Clause{..} = do
 compilePats :: Type -> NAPs -> C [Hs.Pat ()]
 compilePats _ [] = pure []
 compilePats ty ((namedArg -> ProjP po pn):ps) = do
+  reportSDoc "agda2hs.compile" 6 $ "compiling copattern: " <+> text (prettyShow pn)
+  -- NOTE: should be fine for unboxed records
+  unlessM (asks copatternsEnabled `or2M` (isJust <$> isUnboxProjection pn)) $
+    genericDocError =<< "not supported in Haskell: copatterns"
   Just (unEl -> Pi a b) <- getDefType pn ty -- ????
   compilePats (absBody b) ps
 
--- TODO: use shouldBePi or mustBePi
+-- -- copatterns patterns
+-- compilePat ty (ProjP _ q) = do
+--   reportSDoc "agda2hs.compile" 6 $ "compiling copattern: " <+> text (prettyShow q)
+--   unlessM (asks copatternsEnabled) $
+--     genericDocError =<< "not supported in Haskell: copatterns"
+--   let x = hsName $ prettyShow q
+--   return $ Hs.PVar () x
+
 compilePats ty ((namedArg -> pat):ps) = do
   (a, b) <- mustBePi ty
   reportSDoc "agda2hs.compile.pattern" 5 $ text "Compiling pattern:" <+> prettyTCM pat
@@ -259,13 +264,6 @@ compilePat ty (ConP ch i ps) = do
 -- literal patterns
 compilePat ty (LitP _ l) = compileLitPat l
 
--- copatterns patterns
-compilePat ty (ProjP _ q) = do
-  reportSDoc "agda2hs.compile" 6 $ "compiling copattern: " <+> text (prettyShow q)
-  unlessM (asks copatternsEnabled) $
-    genericDocError =<< "not supported in Haskell: copatterns"
-  let x = hsName $ prettyShow q
-  return $ Hs.PVar () x
 
 -- nothing else is supported
 compilePat _ p = genericDocError =<< "bad pattern:" <?> prettyTCM p

test/AllTests.agda

@@ -65,7 +65,7 @@ import TypeSignature
 -- import ModuleParametersImports
 import Coerce
 -- import Inlining
-import EraseType
+-- import EraseType
 import Issue257
 import Delay
 -- import Issue264
@@ -134,7 +134,7 @@ import TypeSignature
 -- import ModuleParametersImports
 import Coerce
 -- import Inlining
-import EraseType
+-- import EraseType
 import Delay
 -- import Issue264
 #-}

test/UnboxPragma.agda

@@ -19,16 +19,16 @@ sort1 xs = xs [ looksfine ]
 
 {-# COMPILE AGDA2HS sort1 #-}
 
--- sort2 : List Int → ∃ (List Int) IsSorted
--- sort2 xs .el = xs
--- sort2 xs .pf = looksfine
--- 
--- {-# COMPILE AGDA2HS sort2 #-}
-
--- sort3 : List Int → ∃ (List Int) IsSorted
--- sort3 xs = xs [ sort2 xs .pf ]
--- 
--- {-# COMPILE AGDA2HS sort3 #-}
+sort2 : List Int → ∃ (List Int) IsSorted
+sort2 xs .el = xs
+sort2 xs .pf = looksfine
+
+{-# COMPILE AGDA2HS sort2 #-}
+
+sort3 : List Int → ∃ (List Int) IsSorted
+sort3 xs = xs [ sort2 xs .pf ]
+
+{-# COMPILE AGDA2HS sort3 #-}
 
 sortAll : List (List Int)
 sortAll = map el (map (λ xs → xs [ looksfine {xs} ]) ((1 ∷ 2 ∷ []) ∷ (3 ∷ []) ∷ []))

test/golden/AllTests.hs

@@ -1,33 +1,33 @@
 module AllTests where
 
-import Issue14
+-- import Issue14
 import Issue65
 import Issue69
 import Issue73
 import Fixities
 import LanguageConstructs
 import Numbers
 import Pragmas
-import Sections
-import Test
+-- import Sections
+-- import Test
 import Tree
 import Tuples
-import Where
+-- import Where
 import TypeSynonyms
-import CanonicalInstance
+-- import CanonicalInstance
 import Coinduction
-import ConstrainedInstance
+-- import ConstrainedInstance
 import Datatypes
 import Records
 import Default
-import DefaultMethods
+-- import DefaultMethods
 import Vector
 import Issue90
 import Issue93
-import QualifiedModule
+-- import QualifiedModule
 import Superclass
 import UnboxPragma
-import ScopedTypeVariables
+-- import ScopedTypeVariables
 import LiteralPatterns
 import Issue92
 import HeightMirror
@@ -37,18 +37,18 @@ import BangPatterns
 import Issue94
 import DoNotation
 import NewTypePragma
-import Importer
-import QualifiedImports
-import CommonQualifiedImports
+-- import Importer
+-- import QualifiedImports
+-- import CommonQualifiedImports
 import RequalifiedImports
-import QualifiedPrelude
+-- import QualifiedPrelude
 import AutoLambdaCaseInCase
 import AutoLambdaCaseInBind
 import WitnessedFlows
 import Kinds
 import LawfulOrd
 import Deriving
-import ErasedLocalDefinitions
+-- import ErasedLocalDefinitions
 import TypeOperators
 import ErasedTypeArguments
 import TypeOperatorExport
@@ -57,13 +57,13 @@ import IOFile
 import IOInput
 import Issue200
 import Issue169
-import Issue210
+-- import Issue210
 import TypeSignature
 -- import ModuleParameters
 -- import ModuleParametersImports
 import Coerce
-import Inlining
-import EraseType
+-- import Inlining
+-- import EraseType
 import Delay
 -- import Issue264