From 6dec8aaa7e1d56c3abd85ee7dc976b85e2437853 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 22 Sep 2023 18:41:25 +0200
Subject: [PATCH] Instance holes

---
 src/Juvix/Compiler/Concrete/Language.hs              |  1 +
 src/Juvix/Compiler/Concrete/Print/Base.hs            |  1 +
 .../Translation/FromParsed/Analysis/Scoping.hs       | 10 ++++++++++
 .../Compiler/Concrete/Translation/FromSource.hs      | 12 +++++++++++-
 tests/Compilation/positive/test061.juvix             |  2 +-
 5 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs
index ccd6d47f2b..b8d85fea53 100644
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 6be7ca0454..ec33bcc80d 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/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
 
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 5ecc97a65a..31b678df0b 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 36f98fefd5..bd873c7f72 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/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
diff --git a/tests/Compilation/positive/test061.juvix b/tests/Compilation/positive/test061.juvix
index 84e37d3b5c..e7622d29a3 100644
--- a/tests/Compilation/positive/test061.juvix
+++ b/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"]);