add error message for missing arguments

anoma · Jul 14, 2023 · 90cbfa4 · 90cbfa4
1 parent 617bc01
commit 90cbfa4
Show file tree

Hide file tree

Showing 3 changed files with 83 additions and 19 deletions.
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs
@@ -106,9 +106,18 @@ helper loc = do
           | lastBlock ->
               unless
                 (IntMap.keys args == [0 .. IntMap.size args - 1])
-                (error "missing explicit arg")
-          | otherwise -> unless (null omittedArgs) (error "missing explicit arg before last block")
+                (missingErr (nonEmpty' (map fst (filterMissing (HashMap.toList omittedArgs)))))
+          | otherwise -> whenJust (nonEmpty (HashMap.keys omittedArgs)) missingErr
       forM_ args output
+      where
+        filterMissing :: [(Symbol, Int)] -> [(Symbol, Int)]
+        filterMissing = case maximumGiven of
+          Nothing -> id
+          Just m -> filter ((< m) . snd)
+        maximumGiven :: Maybe Int
+        maximumGiven = fst <$> IntMap.lookupMax args
+        missingErr :: NonEmpty Symbol -> Sem r ()
+        missingErr = throw . ErrMissingArguments . MissingArguments loc
 
     emitImplicit :: Bool -> HashMap Symbol Int -> IntMap Expression -> Sem r ()
     emitImplicit lastBlock omittedArgs args = go 0 (IntMap.toAscList args)

diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments/Error.hs
@@ -44,26 +44,30 @@ instance ToGenericError UnexpectedArguments where
     opts <- fromGenericOptions <$> ask
     let _genericErrorLoc = getLocSpan _unexpectedArguments
         _genericErrorMessage :: AnsiText
-        _genericErrorMessage = prettyError $ "Unexpected named arguments:" <+> itemize (ppCode opts <$> _unexpectedArguments)
+        _genericErrorMessage =
+          prettyError $
+            "Unexpected named arguments:"
+              <> line
+              <> itemize (ppCode opts <$> _unexpectedArguments)
         _genericErrorIntervals = getLoc <$> toList _unexpectedArguments
     return GenericError {..}
 
 data MissingArguments = MissingArguments
-  { _missingArgumentsApplication :: NamedApplication 'Scoped,
-    _missingArguments :: NonEmpty Symbol,
-    _missingArgumentsImplicit :: IsImplicit
+  { _missingArgumentsLoc :: Interval,
+    _missingArguments :: NonEmpty Symbol
   }
   deriving stock (Show)
 
 instance ToGenericError MissingArguments where
   genericError MissingArguments {..} = do
     opts <- fromGenericOptions <$> ask
-    let i = getLoc _missingArgumentsApplication
+    let i = _missingArgumentsLoc
         _genericErrorLoc = i
         _genericErrorMessage :: AnsiText
         _genericErrorMessage =
           prettyError $
-            "Missing arguments:"
-              <+> itemize (ppCode opts <$> _missingArguments)
+            "Missing arguments in named application:"
+              <> line
+              <> itemize (ppCode opts <$> _missingArguments)
         _genericErrorIntervals = pure i
     return GenericError {..}
diff --git a/tests/positive/NamedArguments.juvix b/tests/positive/NamedArguments.juvix
@@ -1,15 +1,23 @@
 module NamedArguments;
 
 axiom a : Type;
+
 axiom b : Type;
+
 axiom c : Type;
+
 axiom d : Type;
+
 axiom e : Type;
+
 axiom f : Type;
+
 axiom g : Type;
+
 axiom h : Type;
 
-type Unit := unit : Unit;
+type Unit :=
+  | unit : Unit;
 
 axiom fun1 : (a : Type) -> (b : Type) -> {c : Type} -> Type;
 
@@ -19,26 +27,69 @@ t1 : Type := fun1 (a := a) (b := b) {c := c};
 -- skip implicit at the end
 t1' : {_ : Type} -> Type := fun1 (b := b) (a := a);
 
-axiom fun2 : (a : Type) -> (b : Type) -> {c : Type} -> {d : Type} -> Type;
+axiom fun2 : (a : Type)
+  -> (b : Type)
+  -> {c : Type}
+  -> {d : Type}
+  -> Type;
 
 -- skip implicit in implicit group
 t2 : {_ : Type} -> Type := fun2 (a := a) (b := b) {c := d};
 
-axiom fun3 : (a : Type) -> (b : Type) -> {c : Type} -> {d : c} -> Type;
+axiom fun3 : (a : Type)
+  -> (b : Type)
+  -> {c : Type}
+  -> {d : c}
+  -> Type;
 
 -- skip implicit in the middle
 t3 : Type := fun3 (a := a) (b := b) {d := unit};
 
-axiom fun4 : (a : Type) -> (b : Type) -> {c : Type} -> (d : c) -> Type;
+axiom fun4 : (a : Type)
+  -> (b : Type)
+  -> {c : Type}
+  -> (d : c)
+  -> Type;
 
 -- skip implicit in the middle
 t4 : Type := fun4 (a := a) (b := b) (d := unit);
 
-axiom fun5 : (a : Type) -> (b : Type) -> {c c' : Type} -> (d : c) -> (d' : c') -> Type;
+axiom fun5 : (a : Type)
+  -> (b : Type)
+  -> {c c' : Type}
+  -> (d : c)
+  -> (d' : c')
+  -> Type;
+
+t5 : Type :=
+  fun5 (a := a) (b := b) (d' := unit) (d := unit);
+
+t5' : Type :=
+  fun5 (a := a; b := b) (d' := unit) (d := unit);
+
+axiom fun6 : {a : Type}
+  -> (b : Type)
+  -> {c c' : Type}
+  -> (d : c)
+  -> (d' : c')
+  -> (a' : a)
+  -> Type;
+
+t6 : Type :=
+  fun6 (b := b) (d' := unit) (d := unit) (a' := unit);
+
+t6' : Type :=
+  fun6 (d' := unit; d := unit; a' := unit; b := b);
+
+module FakeRecords;
+
+  type Pair (A B : Type) :=
+    | mkPair : (fst : A) -> (snd : B) -> Pair A B;
+
+  pp : Pair (B := Unit; A := Type) :=
+    mkPair (snd := unit; fst := Type);
 
-t5 : Type := fun5 (a := a) (b := b) (d' := unit) (d := unit);
-t5' : Type := fun5 (a := a; b := b) (d' := unit) (d := unit);
+  pp2 : Pair (B := Unit; A := Type) :=
+    mkPair (fst := Type) unit;
 
-axiom fun6 : {a : Type} -> (b : Type) -> {c c' : Type} -> (d : c) -> (d' : c') -> (a' : a) -> Type;
-t6 : Type := fun6 (b := b) (d' := unit) (d := unit) (a' := unit);
-t6' : Type := fun6 (d' := unit; d := unit; a' := unit; b := b);
+end;