Named arguments (#2250)

- closes #1991 

This pr implements named arguments as described in #1991. It does not
yet implement optional arguments, which should be added in a later pr as
they are not required for record syntax.

# Syntax Overview

Named arguments are a convenient mehcanism to provide arguments, where
we give the arguments by name instead of by position. Anything with a
type signature can have named arguments, i.e. functions, types,
constructors and axioms.

For instance, if we have (note that named arguments can also appear on
the rhs of the `:`):
```
fun : {A B : Type} (f : A -> B) : (x : A) -> B := ... ;
```
With the traditional positional application, we would write
```
fun suc zero
```
With named arguments we can write the following:
1. `fun (f := suc) (x := zero)`.
2. We can change the order: `fun (x := zero) (f := suc)`.
3. We can group the arguments: `fun (x := zero; f := suc)`.
4. We can partially apply functions with named arguments: `fun (f :=
suc) zero`.
5. We can provide implicit arguments analogously (with braces): `fun {A
:= Nat; B := Nat} (f := suc; x := zero)`.
6. We can skip implicit arguments: `fun {B := Nat} (f := suc; x :=
zero)`.

What we cannot do:
1. Skip explicit arguments. E.g. `fun (x := zero)`.
2. Mix explicit and implicit arguments in the same group. E.g. `fun (A
:= Nat; f := suc)`
3. Provide explicit and implicit arguments in different order. E.g. `fun
(f := suc; x := zero) {A := Nat}`.

.hlint.yaml

@@ -17,6 +17,7 @@
         - LambdaCase
         - NoImplicitPrelude
         - OverloadedStrings
+        - QuantifiedConstraints
         - QuasiQuotes
         - RecordWildCards
         - StandaloneKindSignatures

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -31,7 +31,7 @@ instance Hashable BuiltinPrim
 instance Pretty BuiltinPrim where
   pretty = \case
     BuiltinsInductive i -> pretty i
-    BuiltinsConstructor {} -> impossible
+    BuiltinsConstructor c -> pretty c
     BuiltinsFunction f -> pretty f
     BuiltinsAxiom a -> pretty a
 
@@ -58,6 +58,17 @@ instance Pretty BuiltinInductive where
     BuiltinInt -> Str.int_
     BuiltinList -> Str.list
 
+instance Pretty BuiltinConstructor where
+  pretty = \case
+    BuiltinNatZero -> Str.zero
+    BuiltinNatSuc -> Str.suc
+    BuiltinBoolTrue -> Str.true
+    BuiltinBoolFalse -> Str.false
+    BuiltinIntOfNat -> Str.ofNat
+    BuiltinIntNegSuc -> Str.negSuc
+    BuiltinListNil -> Str.nil
+    BuiltinListCons -> Str.cons
+
 data BuiltinConstructor
   = BuiltinNatZero
   | BuiltinNatSuc

src/Juvix/Compiler/Concrete/Data/Name.hs

@@ -22,6 +22,9 @@ instance HasLoc Name where
     NameQualified q -> getLoc q
     NameUnqualified s -> getLoc s
 
+instance HasAtomicity Name where
+  atomicity = const Atom
+
 instance Pretty QualifiedName where
   pretty (QualifiedName (SymbolPath path) s) =
     let symbols = snoc (toList path) s

src/Juvix/Compiler/Concrete/Data/NameSignature.hs

@@ -0,0 +1,8 @@
+module Juvix.Compiler.Concrete.Data.NameSignature
+  ( module Juvix.Compiler.Concrete.Data.NameSignature.Base,
+    module Juvix.Compiler.Concrete.Data.NameSignature.Builder,
+  )
+where
+
+import Juvix.Compiler.Concrete.Data.NameSignature.Base
+import Juvix.Compiler.Concrete.Data.NameSignature.Builder

src/Juvix/Compiler/Concrete/Data/NameSignature/Base.hs

@@ -0,0 +1,21 @@
+module Juvix.Compiler.Concrete.Data.NameSignature.Base where
+
+import Juvix.Compiler.Concrete.Data.Name
+import Juvix.Prelude hiding (show)
+
+data NameBlock = NameBlock
+  { -- | Symbols map to themselves so we can retrive the location
+    -- | NOTE the index is wrt to the block, not the whole signature.
+    _nameBlock :: HashMap Symbol (Symbol, Int),
+    _nameImplicit :: IsImplicit
+  }
+  deriving stock (Show)
+
+-- | Two consecutive blocks should have different implicitness
+newtype NameSignature = NameSignature
+  { _nameSignatureArgs :: [NameBlock]
+  }
+  deriving stock (Show)
+
+makeLenses ''NameSignature
+makeLenses ''NameBlock

src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs

@@ -0,0 +1,168 @@
+module Juvix.Compiler.Concrete.Data.NameSignature.Builder
+  ( mkNameSignature,
+    HasNameSignature,
+    module Juvix.Compiler.Concrete.Data.NameSignature.Base,
+    -- to supress unused warning
+    getBuilder,
+  )
+where
+
+import Juvix.Compiler.Concrete.Data.NameSignature.Base
+import Juvix.Compiler.Concrete.Data.NameSignature.Error
+import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error
+import Juvix.Prelude
+
+data NameSignatureBuilder m a where
+  AddSymbol :: IsImplicit -> Symbol -> NameSignatureBuilder m ()
+  EndBuild :: NameSignatureBuilder m a
+  -- | for debugging
+  GetBuilder :: NameSignatureBuilder m BuilderState
+
+data BuilderState = BuilderState
+  { _stateCurrentImplicit :: Maybe IsImplicit,
+    _stateNextIx :: Int,
+    -- | maps to itself
+    _stateSymbols :: HashMap Symbol Symbol,
+    _stateReverseClosedBlocks :: [NameBlock],
+    _stateCurrentBlock :: HashMap Symbol (Symbol, Int)
+  }
+
+makeLenses ''BuilderState
+makeSem ''NameSignatureBuilder
+
+class HasNameSignature d where
+  addArgs :: Members '[NameSignatureBuilder] r => d -> Sem r ()
+
+instance HasNameSignature (AxiomDef 'Parsed) where
+  addArgs :: Members '[NameSignatureBuilder] r => AxiomDef 'Parsed -> Sem r ()
+  addArgs a = addAtoms (a ^. axiomType)
+
+instance HasNameSignature (FunctionDef 'Parsed) where
+  addArgs a = do
+    mapM_ addSigArg (a ^. signArgs)
+    addAtoms (a ^. signRetType)
+
+instance HasNameSignature (InductiveDef 'Parsed, InductiveConstructorDef 'Parsed) where
+  addArgs (i, c) = do
+    mapM_ addConstructorParams (i ^. inductiveParameters)
+    addAtoms (c ^. constructorType)
+
+instance HasNameSignature (InductiveDef 'Parsed) where
+  addArgs a = do
+    mapM_ addInductiveParams (a ^. inductiveParameters)
+    whenJust (a ^. inductiveType) addAtoms
+
+mkNameSignature ::
+  (Members '[Error ScoperError] r, HasNameSignature d) =>
+  d ->
+  Sem r NameSignature
+mkNameSignature d = do
+  fmap (fromBuilderState . fromLeft impossible)
+    . mapError ErrNameSignature
+    . runError @BuilderState
+    . evalState iniBuilderState
+    . re
+    $ do
+      addArgs d
+      endBuild
+
+iniBuilderState :: BuilderState
+iniBuilderState =
+  BuilderState
+    { _stateCurrentImplicit = Nothing,
+      _stateNextIx = 0,
+      _stateSymbols = mempty,
+      _stateReverseClosedBlocks = [],
+      _stateCurrentBlock = mempty
+    }
+
+fromBuilderState :: BuilderState -> NameSignature
+fromBuilderState b =
+  NameSignature
+    { _nameSignatureArgs = reverse (addCurrent (b ^. stateReverseClosedBlocks))
+    }
+  where
+    addCurrent :: [NameBlock] -> [NameBlock]
+    addCurrent
+      | null (b ^. stateCurrentBlock) = id
+      | Just i <- b ^. stateCurrentImplicit = (NameBlock (b ^. stateCurrentBlock) i :)
+      | otherwise = id
+
+addAtoms :: forall r. Members '[NameSignatureBuilder] r => ExpressionAtoms 'Parsed -> Sem r ()
+addAtoms atoms = addAtom . (^. expressionAtoms . _head1) $ atoms
+  where
+    addAtom :: ExpressionAtom 'Parsed -> Sem r ()
+    addAtom = \case
+      AtomFunction f -> do
+        addParameters (f ^. funParameters)
+        addAtoms (f ^. funReturn)
+      _ -> endBuild
+
+    addParameters :: FunctionParameters 'Parsed -> Sem r ()
+    addParameters FunctionParameters {..} = forM_ _paramNames addParameter
+      where
+        addParameter :: FunctionParameter 'Parsed -> Sem r ()
+        addParameter = \case
+          FunctionParameterName s -> addSymbol _paramImplicit s
+          FunctionParameterWildcard {} -> endBuild
+
+addInductiveParams' :: Members '[NameSignatureBuilder] r => IsImplicit -> InductiveParameters 'Parsed -> Sem r ()
+addInductiveParams' i a = forM_ (a ^. inductiveParametersNames) (addSymbol i)
+
+addInductiveParams :: Members '[NameSignatureBuilder] r => InductiveParameters 'Parsed -> Sem r ()
+addInductiveParams = addInductiveParams' Explicit
+
+addConstructorParams :: Members '[NameSignatureBuilder] r => InductiveParameters 'Parsed -> Sem r ()
+addConstructorParams = addInductiveParams' Implicit
+
+addSigArg :: Members '[NameSignatureBuilder] r => SigArg 'Parsed -> Sem r ()
+addSigArg a = forM_ (a ^. sigArgNames) (addSymbol (a ^. sigArgImplicit))
+
+type Re r = State BuilderState ': Error BuilderState ': Error NameSignatureError ': r
+
+re ::
+  forall r a.
+  Sem (NameSignatureBuilder ': r) a ->
+  Sem (Re r) a
+re = reinterpret3 $ \case
+  AddSymbol impl k -> addSymbol' impl k
+  EndBuild -> endBuild'
+  GetBuilder -> get
+{-# INLINE re #-}
+
+addSymbol' :: forall r. IsImplicit -> Symbol -> Sem (Re r) ()
+addSymbol' impl sym = do
+  curImpl <- gets (^. stateCurrentImplicit)
+  if
+      | Just impl == curImpl -> addToCurrentBlock
+      | otherwise -> startNewBlock
+  where
+    errDuplicateName :: Symbol -> Sem (Re r) ()
+    errDuplicateName _dupNameFirst =
+      throw $
+        ErrDuplicateName
+          DuplicateName
+            { _dupNameSecond = sym,
+              ..
+            }
+
+    addToCurrentBlock :: Sem (Re r) ()
+    addToCurrentBlock = do
+      idx <- (sym,) <$> gets (^. stateNextIx)
+      modify' (over stateNextIx succ)
+      whenJustM (gets (^. stateSymbols . at sym)) errDuplicateName
+      modify' (set (stateSymbols . at sym) (Just sym))
+      modify' (set (stateCurrentBlock . at sym) (Just idx))
+
+    startNewBlock :: Sem (Re r) ()
+    startNewBlock = do
+      curBlock <- gets (^. stateCurrentBlock)
+      mcurImpl <- gets (^. stateCurrentImplicit)
+      modify' (set stateCurrentImplicit (Just impl))
+      modify' (set stateCurrentBlock mempty)
+      modify' (set stateNextIx 0)
+      whenJust mcurImpl $ \curImpl -> modify' (over stateReverseClosedBlocks (NameBlock curBlock curImpl :))
+      addSymbol' impl sym
+
+endBuild' :: Sem (Re r) a
+endBuild' = get @BuilderState >>= throw

src/Juvix/Compiler/Concrete/Data/NameSignature/Error.hs

@@ -0,0 +1,31 @@
+module Juvix.Compiler.Concrete.Data.NameSignature.Error where
+
+import Juvix.Compiler.Concrete.Language
+import Juvix.Compiler.Concrete.Pretty.Options (fromGenericOptions)
+import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pretty
+import Juvix.Prelude
+
+newtype NameSignatureError = ErrDuplicateName DuplicateName
+  deriving stock (Show)
+
+instance ToGenericError NameSignatureError where
+  genericError = \case
+    ErrDuplicateName d -> genericError d
+
+data DuplicateName = DuplicateName
+  { _dupNameFirst :: Symbol,
+    _dupNameSecond :: Symbol
+  }
+  deriving stock (Show)
+
+instance ToGenericError DuplicateName where
+  genericError DuplicateName {..} = do
+    opts <- fromGenericOptions <$> ask
+    let _genericErrorLoc = getLoc _dupNameSecond
+        _genericErrorMessage :: AnsiText
+        _genericErrorMessage =
+          prettyError $
+            "The symbol" <+> ppCode opts _dupNameFirst <+> "cannot be repeated"
+        _genericErrorIntervals = map getLoc [_dupNameFirst, _dupNameSecond]
+
+    return GenericError {..}

src/Juvix/Compiler/Concrete/Data/Scope.hs

@@ -5,6 +5,7 @@ module Juvix.Compiler.Concrete.Data.Scope
 where
 
 import Juvix.Compiler.Concrete.Data.InfoTable
+import Juvix.Compiler.Concrete.Data.NameSignature.Base
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Language
 import Juvix.Prelude
@@ -65,7 +66,8 @@ makeLenses ''ScopeParameters
 data ScoperState = ScoperState
   { _scoperModulesCache :: ModulesCache,
     _scoperModules :: HashMap S.ModuleNameId (ModuleRef' 'S.NotConcrete),
-    _scoperScope :: HashMap TopModulePath Scope
+    _scoperScope :: HashMap TopModulePath Scope,
+    _scoperSignatures :: HashMap S.NameId NameSignature
   }
 
 makeLenses ''ScoperState

src/Juvix/Compiler/Concrete/Extra.hs

@@ -7,6 +7,8 @@ module Juvix.Compiler.Concrete.Extra
     groupStatements,
     flattenStatement,
     migrateFunctionSyntax,
+    fromAmbiguousIterator,
+    ambiguousIteratorToAtoms,
   )
 where
 
@@ -188,3 +190,46 @@ migrateFunctionSyntax m = over moduleBody (mapMaybe goStatement) m
             }
     getClauses :: S.Symbol -> [FunctionClause 'Scoped]
     getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction]
+
+fromAmbiguousIterator :: AmbiguousIterator -> Iterator 'Parsed
+fromAmbiguousIterator AmbiguousIterator {..} =
+  Iterator
+    { _iteratorName = _ambiguousIteratorName,
+      _iteratorRanges = [],
+      _iteratorBody = _ambiguousIteratorBody,
+      _iteratorBodyBraces = _ambiguousIteratorBodyBraces,
+      _iteratorInitializers = map mkInitializer (toList _ambiguousIteratorInitializers),
+      _iteratorParens = _ambiguousIteratorParens
+    }
+  where
+    mkInitializer :: NamedArgument 'Parsed -> Initializer 'Parsed
+    mkInitializer a@NamedArgument {..} =
+      Initializer
+        { _initializerAssignKw = _namedArgAssignKw,
+          _initializerPattern = PatternAtoms (pure (PatternAtomIden (NameUnqualified _namedArgName))) (getLoc a),
+          _initializerExpression = _namedArgValue
+        }
+
+ambiguousIteratorToAtoms :: AmbiguousIterator -> ExpressionAtoms 'Parsed
+ambiguousIteratorToAtoms AmbiguousIterator {..} =
+  ExpressionAtoms
+    { _expressionAtomsLoc = getLoc napp,
+      _expressionAtoms = pure (AtomNamedApplication napp) <> body
+    }
+  where
+    body :: NonEmpty (ExpressionAtom 'Parsed)
+    body
+      | _ambiguousIteratorBodyBraces = pure (AtomBraces (WithLoc (getLoc _ambiguousIteratorBody) _ambiguousIteratorBody))
+      | otherwise = _ambiguousIteratorBody ^. expressionAtoms
+    napp =
+      NamedApplication
+        { _namedAppName = _ambiguousIteratorName,
+          _namedAppSignature = Irrelevant (),
+          _namedAppArgs =
+            pure
+              ArgumentBlock
+                { _argBlockDelims = Irrelevant Nothing,
+                  _argBlockImplicit = Explicit,
+                  _argBlockArgs = _ambiguousIteratorInitializers
+                }
+        }