Use names for dot patterns

Still a bit imperfect: names corresponding to module parameters are
not prefixed by '_'s because these are generated purely based of
the type, while explicitly named dot patterns can have '_'s prefixed

Author: NathanielB123

src/Agda2Hs/Compile/Function.hs

@@ -37,7 +37,7 @@ import Agda.Utils.Size ( Sized(size) )
 
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName )
-import Agda2Hs.Compile.Term ( compileTerm, usableDom, dependentDom )
+import Agda2Hs.Compile.Term ( compileTerm, usableDom, dependentDom, extractMaybeName )
 import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileDomType )
 import Agda2Hs.Compile.TypeDefinition ( compileTypeDef )
 import Agda2Hs.Compile.Types
@@ -294,7 +294,8 @@ compilePats ty ((namedArg -> ProjP po pn):ps) = do
 
   compilePats (absBody b) ps
 
-compilePats ty ((namedArg -> pat):ps) = do
+compilePats ty (p:ps) = do
+  let pat = namedArg p
   (a, b) <- mustBePi ty
   reportSDoc "agda2hs.compile.pattern" 10 $ text "Compiling pattern:" <+> prettyTCM pat
   let rest = compilePats (absApp b (patternToTerm pat)) ps
@@ -304,21 +305,21 @@ compilePats ty ((namedArg -> pat):ps) = do
     DOType     -> rest
     DOTerm     -> do
       checkNoAsPatterns pat
-      (:) <$> compilePat (unDom a) pat <*> rest
+      (:) <$> compilePat (unDom a) (extractMaybeName p) pat <*> rest
 
 
-compilePat :: Type -> DeBruijnPattern -> C (Hs.Pat ())
+compilePat :: Type -> Maybe ArgName -> 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
 
@@ -330,13 +331,18 @@ 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
 
--- dot patterns are compiled to wildcard patterns
-compilePat _ (DotP _ _) = return $ Hs.PWildCard ()
+-- dot patterns are compiled by prefixing with an '_' if it has been given
+-- an explicit name, or a wildcard otherwise
+compilePat _ (Just n) (DotP _ _) = do
+  let n' = hsName $ '_' : n
+  checkValidVarName n'
+  return $ Hs.PVar () n'
+compilePat _ Nothing  (DotP _ _) = 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 ())

src/Agda2Hs/Compile/Term.hs

@@ -576,9 +576,7 @@ compileInlineFunctionApp f ty args = do
     extractPatName _ = __IMPOSSIBLE__
 
     extractName :: NamedArg DeBruijnPattern -> ArgName
-    extractName (unArg -> np)
-      | Just n <- nameOf np = rangedThing (woThing n)
-      | otherwise = extractPatName (namedThing np)
+    extractName p = fromMaybe (extractPatName $ namedArg p) (extractMaybeName p)
 
     etaExpand :: NAPs -> Type -> [Term] -> C Term
     etaExpand [] ty args = do
@@ -594,6 +592,8 @@ compileInlineFunctionApp f ty args = do
       let ai = domInfo dom
       Lam ai . mkAbs (extractName p) <$> etaExpand ps (absBody cod) (raise 1 args ++ [ var 0 ])
 
+extractMaybeName :: NamedArg a -> Maybe ArgName
+extractMaybeName p = rangedThing . woThing <$> nameOf (unArg p)
 
 compileApp :: Hs.Exp () -> Type -> [Term] -> C (Hs.Exp ())
 compileApp = compileApp' . eApp

test/AllTests.agda

@@ -89,6 +89,7 @@ import Issue353
 import RankNTypes
 import ErasedPatternLambda
 import ErasedPatternLambda2
+import ErasedPatternLambda3
 import CustomTuples
 import ProjectionLike
 import FunCon
@@ -190,6 +191,7 @@ import Issue353
 import RankNTypes
 import ErasedPatternLambda
 import ErasedPatternLambda2
+import ErasedPatternLambda3
 import CustomTuples
 import ProjectionLike
 import FunCon

test/ErasedPatternLambda2.agda

@@ -14,7 +14,7 @@ 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
+checkSubst' t ty rest refl = True
 {-# COMPILE AGDA2HS checkSubst' #-}
 
 checkSubst : ∀ {@0 x α β} (t : Telescope α (x ∷ β)) → Bool

test/ErasedPatternLambda3.agda

@@ -0,0 +1,23 @@
+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 #-}
+
+module _ {@0 x α β} (t : Telescope α (x ∷ β)) where
+  checkSubst' : ∀ (ty : Bool) (rest : Telescope (x ∷ α) β) → @0 t ≡ ExtendTel ty rest → Bool
+  checkSubst' ty rest refl = True
+  {-# COMPILE AGDA2HS checkSubst' #-}
+
+  checkSubst : Bool
+  checkSubst = caseTelBind t checkSubst'
+  {-# COMPILE AGDA2HS checkSubst #-}

test/golden/AllTests.hs

@@ -84,6 +84,7 @@ import Issue353
 import RankNTypes
 import ErasedPatternLambda
 import ErasedPatternLambda2
+import ErasedPatternLambda3
 import CustomTuples
 import ProjectionLike
 import FunCon

test/golden/ErasedPatternLambda2.hs

@@ -6,7 +6,7 @@ caseTelBind :: Telescope -> (Bool -> Telescope -> d) -> d
 caseTelBind (ExtendTel a tel) f = f a tel
 
 checkSubst' :: Telescope -> Bool -> Telescope -> Bool
-checkSubst' _ ty rest = True
+checkSubst' _t ty rest = True
 
 checkSubst :: Telescope -> Bool
 checkSubst t = caseTelBind t (checkSubst' t)

test/golden/ErasedPatternLambda3.hs

@@ -0,0 +1,13 @@
+module ErasedPatternLambda3 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' t ty rest = True
+
+checkSubst :: Telescope -> Bool
+checkSubst t = caseTelBind t (checkSubst' t)
+