Rec pat edge case + more tests

Author: NathanielB123

src/Agda2Hs/Compile/Function.hs

@@ -46,7 +46,7 @@ import Agda2Hs.Compile.Var ( compileDBVar )
 
 import qualified Agda2Hs.Language.Haskell as Hs
 import Agda2Hs.Language.Haskell.Utils
-  ( Strictness, hsName, pApp, patToExp, constrainType, qualifyType )
+  ( Strictness, hsName, pApp, patToExp, constrainType, qualifyType, hsUnqualName )
 
 -- | Compilation rules for specific constructors in patterns.
 isSpecialCon :: QName -> Maybe (Type -> NAPs -> C (Hs.Pat ()))
@@ -305,21 +305,21 @@ compilePats ty (p:ps) = do
     DOType     -> rest
     DOTerm     -> do
       checkNoAsPatterns pat
-      (:) <$> compilePat (unDom a) (extractMaybeName p) pat <*> rest
+      (:) <$> compilePat (unDom a) pat <*> rest
 
 
-compilePat :: Type -> Maybe ArgName -> DeBruijnPattern -> C (Hs.Pat ())
+compilePat :: Type -> DeBruijnPattern -> C (Hs.Pat ())
 
 -- variable pattern
-compilePat ty _ p@(VarP o x)
+compilePat ty p@(VarP o x)
   | PatOWild <- patOrigin o = return $ Hs.PWildCard ()
   | otherwise = do
       n <- hsName <$> compileDBVar (dbPatVarIndex x)
       checkValidVarName n
       return $ Hs.PVar () n
 
 -- special constructor pattern
-compilePat ty _ (ConP ch i ps) = do
+compilePat ty (ConP ch i ps) = do
   Just ((_, _, _), ty) <- getConType ch =<< reduce ty
   let c = conName ch
 
@@ -331,18 +331,23 @@ compilePat ty _ (ConP ch i ps) = do
     return $ pApp c ps
 
 -- literal patterns
-compilePat ty _ (LitP _ l) = compileLitPat l
+compilePat ty (LitP _ l) = compileLitPat l
 
 -- "Inferred" dot patterns that the programmer has explicitly named are
 -- compiled to variable patterns using that given name, wildcards otherwise
-compilePat _ (Just n) (DotP _ _) = do
-  let n' = hsName n
+compilePat _ (DotP (PatternInfo (PatOVar n) _) _) = do
+  let n' = hsName $ prettyShow n
   checkValidVarName n'
   return $ Hs.PVar () n'
-compilePat _ Nothing  (DotP _ _) = return $ Hs.PWildCard ()
+compilePat ty (DotP (PatternInfo PatORec (c:ps)) _) =
+  -- User-written record pattern which has been elaborated to a dot pattern
+  return $ pApp (hsUnqualName $ prettyShow c)
+                (Hs.PVar () . hsName . prettyShow <$> ps)
+compilePat _ (DotP (PatternInfo PatODot _) _) =
+  return $ Hs.PWildCard ()
 
 -- nothing else is supported
-compilePat _ _ p = agda2hsErrorM $ "bad pattern:" <?> prettyTCM p
+compilePat _ p = agda2hsErrorM $ "bad pattern:" <?> prettyTCM p
 
 
 compileErasedConP :: Type -> Strictness -> NAPs -> C (Hs.Pat ())

test/AllTests.agda

@@ -105,6 +105,9 @@ import RuntimeCast
 import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
+import RelevantDotPattern3
+import RelevantDotPattern4
+import RelevantDotPattern5
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -207,4 +210,7 @@ import RuntimeCast
 import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
+import RelevantDotPattern3
+import RelevantDotPattern4
+import RelevantDotPattern5
 #-}

test/RelevantDotPattern3.agda

@@ -0,0 +1,23 @@
+-- Derived from "ErasedPatternLambda"
+open import Haskell.Prelude
+
+Scope = List Bool
+
+data Telescope (@0 α : Scope) : @0 Scope → Type where
+  ExtendTel : ∀ {@0 x β} → Bool → Telescope (x ∷ α) β  → Telescope α (x ∷ β)
+{-# COMPILE AGDA2HS Telescope #-}
+
+caseTelBind : ∀ {@0 x α β} (tel : Telescope α (x ∷ β))
+            → ((a : Bool) (rest : Telescope (x ∷ α) β) → @0 tel ≡ ExtendTel a rest → d)
+            → d
+caseTelBind (ExtendTel a tel) f = f a tel refl
+
+{-# COMPILE AGDA2HS caseTelBind #-}
+
+checkSubst' : ∀ {@0 x α β} (t : Telescope α (x ∷ β)) (ty : Bool) (rest : Telescope (x ∷ α) β) → @0 t ≡ ExtendTel ty rest → Bool
+checkSubst' (ExtendTel ty' rest') ty rest refl = True
+{-# COMPILE AGDA2HS checkSubst' #-}
+
+checkSubst : ∀ {@0 x α β} (t : Telescope α (x ∷ β)) → Bool
+checkSubst t = caseTelBind t (checkSubst' t)
+{-# COMPILE AGDA2HS checkSubst #-}

test/RelevantDotPattern4.agda

@@ -0,0 +1,17 @@
+-- Derived from "ErasedPatternLambda"
+open import Haskell.Prelude
+
+record Foo : Set where
+  no-eta-equality
+  pattern
+  field
+    x : Nat
+    y : Nat
+open Foo public
+
+{-# COMPILE AGDA2HS Foo #-}
+
+foo : ∀ (xy : Foo) x y → @0 xy ≡ record {x = x; y = y} → Nat
+foo record {x = x'; y = y'} x y _ = x
+
+{-# COMPILE AGDA2HS foo #-}

test/RelevantDotPattern5.agda

@@ -0,0 +1,12 @@
+-- Derived from "ErasedPatternLambda"
+open import Haskell.Prelude
+
+data Foo : Set where
+  Mk : Nat → Nat → Foo
+
+{-# COMPILE AGDA2HS Foo #-}
+
+foo : ∀ (xy : Foo) x y → @0 xy ≡ Mk x y → Nat
+foo (Mk x' y') x y _ = x
+
+{-# COMPILE AGDA2HS foo #-}

test/golden/AllTests.hs

@@ -100,4 +100,7 @@ import RuntimeCast
 import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
+import RelevantDotPattern3
+import RelevantDotPattern4
+import RelevantDotPattern5
 

test/golden/RelevantDotPattern3.hs

@@ -0,0 +1,13 @@
+module RelevantDotPattern3 where
+
+data Telescope = ExtendTel Bool Telescope
+
+caseTelBind :: Telescope -> (Bool -> Telescope -> d) -> d
+caseTelBind (ExtendTel a tel) f = f a tel
+
+checkSubst' :: Telescope -> Bool -> Telescope -> Bool
+checkSubst' (ExtendTel ty' rest') ty rest = True
+
+checkSubst :: Telescope -> Bool
+checkSubst t = caseTelBind t (checkSubst' t)
+

test/golden/RelevantDotPattern4.hs

@@ -0,0 +1,9 @@
+module RelevantDotPattern4 where
+
+import Numeric.Natural (Natural)
+
+data Foo = Foo{x :: Natural, y :: Natural}
+
+foo :: Foo -> Natural -> Natural -> Natural
+foo (Foo x' y') x y = x
+

test/golden/RelevantDotPattern5.hs

@@ -0,0 +1,9 @@
+module RelevantDotPattern5 where
+
+import Numeric.Natural (Natural)
+
+data Foo = Mk Natural Natural
+
+foo :: Foo -> Natural -> Natural -> Natural
+foo (Mk x' y') x y = x
+