Small refactor + new test

Rather than trying to extract the dot pattern name with nameOf,
we make use of the PatOrigin in PatternInfo

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, extractMaybeName )
+import Agda2Hs.Compile.Term ( compileTerm, usableDom, dependentDom )
 import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileDomType )
 import Agda2Hs.Compile.TypeDefinition ( compileTypeDef )
 import Agda2Hs.Compile.Types
@@ -294,8 +294,7 @@ compilePats ty ((namedArg -> ProjP po pn):ps) = do
 
   compilePats (absBody b) ps
 
-compilePats ty (p:ps) = do
-  let pat = namedArg p
+compilePats ty ((namedArg -> pat):ps) = do
   (a, b) <- mustBePi ty
   reportSDoc "agda2hs.compile.pattern" 10 $ text "Compiling pattern:" <+> prettyTCM pat
   let rest = compilePats (absApp b (patternToTerm pat)) ps
@@ -305,21 +304,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 +330,19 @@ 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 _ (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,7 @@ import RuntimeCast
 import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
+import RelevantDotPattern3
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -207,4 +208,5 @@ import RuntimeCast
 import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
+import RelevantDotPattern3
 #-}

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/golden/AllTests.hs

@@ -100,4 +100,5 @@ import RuntimeCast
 import Issue306
 import RelevantDotPattern1
 import RelevantDotPattern2
+import RelevantDotPattern3
 

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)
+