Compile dot patterns (#440)

* Compile dot patterns to wildcards

Arguably it might be nice to retain names (e.g. prefixed by an |_|)
when the dot pattern isn't provided explicitly, but this info
does not appear to be retained by the time we reach internal syntax

* 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

* Stop prefixing with '_'s

This stays consistent with the behaviour on module parameters and
has less chance of weird edge-cases

* Rename new tests

I got rid of the pattern lambdas to make them, so the test name doesn't
really make sense anymore

* 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

@@ -332,6 +332,14 @@ compilePat ty (ConP ch i ps) = do
 -- literal patterns
 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 _ (DotP (PatternInfo (PatOVar n) _) _) = do
+  let n' = hsName $ prettyShow n
+  checkValidVarName n'
+  return $ Hs.PVar () n'
+compilePat _ (DotP (PatternInfo PatODot _) _) =
+  return $ Hs.PWildCard ()
 
 -- nothing else is supported
 compilePat _ p = agda2hsErrorM $ "bad pattern:" <?> prettyTCM p

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

@@ -103,6 +103,9 @@ import Issue408
 import CompileTo
 import RuntimeCast
 import Issue306
+import RelevantDotPattern1
+import RelevantDotPattern2
+import RelevantDotPattern3
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -203,4 +206,7 @@ import Issue408
 import CompileTo
 import RuntimeCast
 import Issue306
+import RelevantDotPattern1
+import RelevantDotPattern2
+import RelevantDotPattern3
 #-}

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

test/RelevantDotPattern2.agda

@@ -0,0 +1,24 @@
+-- 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 #-}
+
+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/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

@@ -98,4 +98,7 @@ import Issue408
 import CompileTo
 import RuntimeCast
 import Issue306
+import RelevantDotPattern1
+import RelevantDotPattern2
+import RelevantDotPattern3
 

test/golden/RelevantDotPattern1.hs

@@ -0,0 +1,13 @@
+module RelevantDotPattern1 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)
+

test/golden/RelevantDotPattern2.hs

@@ -0,0 +1,13 @@
+module RelevantDotPattern2 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)
+

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