Instance holes

src/Juvix/Compiler/Concrete/Language.hs

@@ -1539,6 +1539,7 @@ data ExpressionAtom (s :: Stage)
   | AtomCase (Case s)
   | AtomNewCase (NewCase s)
   | AtomHole (HoleType s)
+  | AtomInstanceHole (HoleType s)
   | AtomDoubleBraces (DoubleBracesExpression s)
   | AtomBraces (WithLoc (ExpressionType s))
   | AtomLet (Let s)

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -322,6 +322,7 @@ instance (SingI s) => PrettyPrint (ExpressionAtom s) where
     AtomDoubleBraces e -> ppCode e
     AtomBraces e -> braces (ppExpressionType (e ^. withLocParam))
     AtomHole w -> ppHoleType w
+    AtomInstanceHole w -> ppHoleType w
     AtomIterator i -> ppCode i
     AtomNamedApplication i -> ppCode i
 

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -2077,6 +2077,7 @@ checkExpressionAtom e = case e of
   AtomBraces br -> pure . AtomBraces <$> traverseOf withLocParam checkParseExpressionAtoms br
   AtomFunArrow a -> return (pure (AtomFunArrow a))
   AtomHole h -> pure . AtomHole <$> checkHole h
+  AtomInstanceHole h -> pure . AtomInstanceHole <$> checkHole h
   AtomLiteral l -> return (pure (AtomLiteral l))
   AtomList l -> pure . AtomList <$> checkList l
   AtomIterator i -> pure . AtomIterator <$> checkIterator i
@@ -2558,6 +2559,7 @@ parseTerm =
       <|> parseNoInfixIdentifier
       <|> parseParens
       <|> parseHole
+      <|> parseInstanceHole
       <|> parseFunction
       <|> parseLambda
       <|> parseCase
@@ -2578,6 +2580,14 @@ parseTerm =
           AtomHole l -> Just l
           _ -> Nothing
 
+    parseInstanceHole :: Parse Expression
+    parseInstanceHole = ExpressionInstanceHole <$> P.token lit mempty
+      where
+        lit :: ExpressionAtom 'Scoped -> Maybe Hole
+        lit s = case s of
+          AtomInstanceHole l -> Just l
+          _ -> Nothing
+
     parseLiteral :: Parse Expression
     parseLiteral = ExpressionLiteral <$> P.token lit mempty
       where

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -699,17 +699,27 @@ parseExpressionAtoms = do
   return ExpressionAtoms {..}
 
 pdoubleBracesExpression ::
+  forall r.
   (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) =>
   ParsecS r (DoubleBracesExpression 'Parsed)
 pdoubleBracesExpression = do
   l <- kw delimDoubleBraceL
-  _doubleBracesExpression <- parseExpressionAtoms
+  _doubleBracesExpression <- instanceHole <|> parseExpressionAtoms
   r <- kw delimDoubleBraceR
   return
     DoubleBracesExpression
       { _doubleBracesDelims = Irrelevant (l, r),
         ..
       }
+  where
+    instanceHole :: ParsecS r (ExpressionAtoms 'Parsed)
+    instanceHole = do
+      (h, i) <- interval (kw kwHole)
+      return $
+        ExpressionAtoms
+          { _expressionAtoms = NonEmpty.singleton (AtomInstanceHole h),
+            _expressionAtomsLoc = Irrelevant i
+          }
 
 --------------------------------------------------------------------------------
 -- Iterators

tests/Compilation/positive/test061.juvix

@@ -63,4 +63,4 @@ main : IO :=
   printStringLn (f'3 "abba") >>
   printStringLn (f'3 {{M := mkShow (λ{x := x ++str "!"})}} "abba") >>
   printStringLn (f5 "abba" 3) >>
-  printStringLn (Show.show ["a"; "b"; "c"; "d"]);
+  printStringLn (Show.show {{_}} ["a"; "b"; "c"; "d"]);