put extra arguments of named applications inside let

src/Juvix/Compiler/Internal/Extra/Base.hs

@@ -405,6 +405,7 @@ foldApplication f args = case nonEmpty args of
 unfoldApplication' :: Application -> (Expression, NonEmpty ApplicationArg)
 unfoldApplication' (Application l' r' i') = second (|: (ApplicationArg i' r')) (unfoldExpressionApp l')
 
+-- TODO make it tail recursive
 unfoldExpressionApp :: Expression -> (Expression, [ApplicationArg])
 unfoldExpressionApp = \case
   ExpressionApplication (Application l r i) ->

src/Juvix/Compiler/Internal/Language.hs

@@ -391,7 +391,7 @@ instance HasAtomicity SimpleLambda where
   atomicity = const Atom
 
 instance HasAtomicity Let where
-  atomicity l = atomicity (l ^. letExpression)
+  atomicity = const (Aggregate letFixity)
 
 instance HasAtomicity Literal where
   atomicity = \case

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -743,7 +743,7 @@ goExpression ::
 goExpression = \case
   ExpressionIdentifier nt -> return (goIden nt)
   ExpressionParensIdentifier nt -> return (goIden nt)
-  ExpressionApplication a -> Internal.ExpressionApplication <$> goApplication a
+  ExpressionApplication a -> goApplication a
   ExpressionCase a -> Internal.ExpressionCase <$> goCase a
   ExpressionNewCase a -> Internal.ExpressionCase <$> goNewCase a
   ExpressionInfixApplication ia -> Internal.ExpressionApplication <$> goInfix ia
@@ -759,19 +759,19 @@ goExpression = \case
   ExpressionHole h -> return (Internal.ExpressionHole h)
   ExpressionInstanceHole h -> return (Internal.ExpressionInstanceHole (fromHole h))
   ExpressionIterator i -> goIterator i
-  ExpressionNamedApplication i -> goNamedApplication i
-  ExpressionNamedApplicationNew i -> goNamedApplicationNew i
+  ExpressionNamedApplication i -> goNamedApplication i []
+  ExpressionNamedApplicationNew i -> goNamedApplicationNew i []
   ExpressionRecordUpdate i -> goRecordUpdateApp i
   ExpressionParensRecordUpdate i -> Internal.ExpressionLambda <$> goRecordUpdate (i ^. parensRecordUpdate)
   where
-    goNamedApplication :: Concrete.NamedApplication 'Scoped -> Sem r Internal.Expression
-    goNamedApplication w = do
+    goNamedApplication :: Concrete.NamedApplication 'Scoped -> [Internal.ApplicationArg] -> Sem r Internal.Expression
+    goNamedApplication w extraArgs = do
       s <- ask @NameSignatures
-      runReader s (runNamedArguments w) >>= goDesugaredNamedApplication
+      runReader s (runNamedArguments w extraArgs) >>= goDesugaredNamedApplication
 
-    goNamedApplicationNew :: Concrete.NamedApplicationNew 'Scoped -> Sem r Internal.Expression
-    goNamedApplicationNew napp = case nonEmpty (napp ^. namedApplicationNewArguments) of
-      Nothing -> return $ goIden (napp ^. namedApplicationNewName)
+    goNamedApplicationNew :: Concrete.NamedApplicationNew 'Scoped -> [Internal.ApplicationArg] -> Sem r Internal.Expression
+    goNamedApplicationNew napp extraArgs = case nonEmpty (napp ^. namedApplicationNewArguments) of
+      Nothing -> return (goIden (napp ^. namedApplicationNewName))
       Just appargs -> do
         let name = napp ^. namedApplicationNewName . scopedIdenName
         sig <- fromJust <$> asks @NameSignatures (^. at (name ^. S.nameId))
@@ -784,7 +784,7 @@ goExpression = \case
                 { _namedAppName = napp ^. namedApplicationNewName,
                   _namedAppArgs = nonEmpty' (createArgumentBlocks (sig ^. nameSignatureArgs))
                 }
-        e <- goNamedApplication napp'
+        e <- goNamedApplication napp' extraArgs
         let l =
               Internal.Let
                 { _letClauses = cls,
@@ -845,8 +845,9 @@ goExpression = \case
               { _appArgIsImplicit = arg ^. argImplicit,
                 _appArg = Internal.toExpression (goSymbol (arg ^. argName))
               }
-          argNames :: NonEmpty Internal.ApplicationArg = mkAppArg <$> a ^. dnamedAppArgs
-          app = Internal.foldApplication (Internal.toExpression fun) (toList argNames)
+          namedArgNames :: NonEmpty Internal.ApplicationArg = mkAppArg <$> a ^. dnamedAppArgs
+          allArgs = toList namedArgNames <> a ^. dnamedExtraArgs
+          app = Internal.foldApplication (Internal.toExpression fun) allArgs
       clauses <- mapM mkClause (a ^. dnamedAppArgs)
       expr <-
         Internal.substitutionE updateKind $
@@ -998,11 +999,26 @@ goExpression = \case
             e' <- goExpression e
             return (Internal.ApplicationArg i e')
 
-    goApplication :: Application -> Sem r Internal.Application
-    goApplication (Application l arg) = do
-      l' <- goExpression l
-      Internal.ApplicationArg {..} <- goApplicationArg arg
-      return (Internal.Application l' _appArg _appArgIsImplicit)
+    goApplication :: Application -> Sem r Internal.Expression
+    goApplication a = do
+      let (f, args) = unfoldApp a
+      args' <- toList <$> mapM goApplicationArg args
+      case f of
+        ExpressionNamedApplication n -> goNamedApplication n args'
+        ExpressionNamedApplicationNew n -> goNamedApplicationNew n args'
+        _ -> do
+          f' <- goExpression f
+          return (Internal.foldApplication f' args')
+      where
+        unfoldApp :: Application -> (Expression, NonEmpty Expression)
+        unfoldApp (Application l' r') =
+          let (f, largs) = go [] l'
+           in (f, largs |: r')
+          where
+            go :: [Expression] -> Expression -> (Expression, [Expression])
+            go ac = \case
+              ExpressionApplication (Application l r) -> go (r : ac) l
+              e -> (e, ac)
 
     goPostfix :: PostfixApplication -> Sem r Internal.Application
     goPostfix (PostfixApplication l op) = do

src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs

@@ -5,6 +5,7 @@ module Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments
     DesugaredNamedApplication,
     dnamedAppIdentifier,
     dnamedAppArgs,
+    dnamedExtraArgs,
     Arg,
     argName,
     argImplicit,
@@ -18,8 +19,8 @@ import Data.HashMap.Strict qualified as HashMap
 import Data.IntMap.Strict qualified as IntMap
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Extra (symbolParsed)
-import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error
+import Juvix.Compiler.Internal.Extra.Base qualified as Internal
 import Juvix.Prelude
 
 type NameSignatures = HashMap NameId (NameSignature 'Scoped)
@@ -42,7 +43,8 @@ data Arg = Arg
 -- | The result of desugaring a named application
 data DesugaredNamedApplication = DesugaredNamedApplication
   { _dnamedAppIdentifier :: ScopedIden,
-    _dnamedAppArgs :: NonEmpty Arg
+    _dnamedAppArgs :: NonEmpty Arg,
+    _dnamedExtraArgs :: [Internal.ApplicationArg]
   }
 
 makeLenses ''BuilderState
@@ -53,17 +55,22 @@ runNamedArguments ::
   forall r.
   (Members '[NameIdGen, Error ScoperError, Reader NameSignatures] r) =>
   NamedApplication 'Scoped ->
+  [Internal.ApplicationArg] ->
   Sem r DesugaredNamedApplication
-runNamedArguments napp = do
+runNamedArguments napp extraArgs = do
   iniSt <- mkIniBuilderState
-  _dnamedAppArgs <-
+  namedArgs <-
     fmap nonEmpty'
       . execOutputList
       . mapError ErrNamedArgumentsError
       . execState iniSt
       $ helper (getLoc napp)
-  let _dnamedAppIdentifier = napp ^. namedAppName
-  return DesugaredNamedApplication {..}
+  return
+    DesugaredNamedApplication
+      { _dnamedAppIdentifier = napp ^. namedAppName,
+        _dnamedAppArgs = namedArgs,
+        _dnamedExtraArgs = extraArgs
+      }
   where
     mkIniBuilderState :: Sem r BuilderState
     mkIniBuilderState = do

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs

@@ -1089,14 +1089,15 @@ holesHelper mhint expr = do
             _appBuilderTypeCtx = mempty,
             _appBuilderArgs = map iniArg args
           }
-  (insertedArgs, st') <- runOutputList (execState iniBuilder goArgs)
+  (insertedArgs, st') <- runOutputList (execState iniBuilder goAllArgs)
   let ty' = mkFinalBuilderType (st' ^. appBuilderType)
       expr' = mkFinalExpression (st' ^. appBuilderLeft) insertedArgs
-  return
-    TypedExpression
-      { _typedType = ty',
-        _typedExpression = expr'
-      }
+  let ret =
+        TypedExpression
+          { _typedType = ty',
+            _typedExpression = expr'
+          }
+  return ret
   where
     mkArg :: InsertedArg -> ApplicationArg
     mkArg i =
@@ -1136,7 +1137,7 @@ holesHelper mhint expr = do
       let ty = fTy ^. typedType
        in runFailDefault (BuilderTypeNoDefaults ty) $ do
             fun <- failMaybe (getFunctionName (fTy ^. typedExpression))
-            infos <- (^. functionInfoDef . funDefArgsInfo) <$> (lookupFunction fun)
+            infos <- (^. functionInfoDef . funDefArgsInfo) <$> lookupFunction fun
             return $ toFunctionDefaultMay fun ty infos
       where
         toFunctionDefaultMay :: Name -> Expression -> [ArgInfo] -> BuilderType
@@ -1147,23 +1148,24 @@ holesHelper mhint expr = do
         toFunctionDefault :: Name -> Expression -> NonEmpty (Indexed ArgInfo) -> FunctionDefault
         toFunctionDefault _argIdFunctionName e (Indexed _argIdIx a :| as) = case e of
           ExpressionFunction f ->
-            FunctionDefault
-              { _functionDefaultLeft = f ^. functionLeft,
-                _functionDefaultRight =
+            let r' =
                   toFunctionDefaultMay
                     _argIdFunctionName
                     (f ^. functionRight)
-                    (map (^. indexedThing) as),
-                _functionDefaultDefault =
-                  let uid =
-                        ArgId
-                          { _argIdDefinitionLoc = Irrelevant (getLoc f),
-                            _argIdName = Irrelevant (a ^. argInfoName),
-                            _argIdFunctionName,
-                            _argIdIx
-                          }
-                   in FunctionDefaultInfo uid <$> a ^. argInfoDefault
-              }
+                    (map (^. indexedThing) as)
+             in FunctionDefault
+                  { _functionDefaultLeft = f ^. functionLeft,
+                    _functionDefaultRight = r',
+                    _functionDefaultDefault =
+                      let uid =
+                            ArgId
+                              { _argIdDefinitionLoc = Irrelevant (getLoc f),
+                                _argIdName = Irrelevant (a ^. argInfoName),
+                                _argIdFunctionName,
+                                _argIdIx
+                              }
+                       in FunctionDefaultInfo uid <$> a ^. argInfoDefault
+                  }
           _ -> impossible
 
     arityCheckBuiltins :: Expression -> [ApplicationArg] -> Sem r ()
@@ -1204,17 +1206,20 @@ holesHelper mhint expr = do
         goImplArgs k (ApplicationArg Implicit _ : as) = goImplArgs (k - 1) as
         goImplArgs _ as = return as
 
-    goArgs :: forall r'. (r' ~ State AppBuilder ': Output InsertedArg ': r) => Sem r' ()
-    goArgs = do
-      peekArg >>= maybe (insertTrailingHolesMay mhint) goNextArg
+    goAllArgs :: forall r'. (r' ~ State AppBuilder ': Output InsertedArg ': r) => Sem r' ()
+    goAllArgs = do
+      goArgs
       gets (^. appBuilderType) >>= applyCtx >>= modify' . set appBuilderType
+
+    goArgs :: forall r'. (r' ~ State AppBuilder ': Output InsertedArg ': r) => Sem r' ()
+    goArgs = peekArg >>= maybe (insertTrailingHolesMay mhint) goNextArg
       where
         insertTrailingHolesMay :: Maybe Expression -> Sem r' ()
         insertTrailingHolesMay = flip whenJust insertTrailingHoles
 
         insertTrailingHoles :: Expression -> Sem r' ()
         insertTrailingHoles hintTy = do
-          builderTy <- gets (^. appBuilderType)
+          builderTy <- gets (^. appBuilderType) >>= applyCtx
           ariHint <- typeArity hintTy
           let (defaults, restExprTy) = peelDefault builderTy
           restExprAri <- typeArity restExprTy
@@ -1236,10 +1241,10 @@ holesHelper mhint expr = do
               mkHoleArg (i, mdef) = do
                 (_appArg, _appBuilderArgIsDefault) <- case i of
                   Explicit -> impossible
+                  ImplicitInstance -> (,ItIsNotDefault) <$> newHoleInstance loc
                   Implicit -> case mdef of
                     Nothing -> (,ItIsNotDefault) <$> newHoleImplicit loc
                     Just (FunctionDefaultInfo uid def) -> return (def, ItIsDefault uid)
-                  ImplicitInstance -> (,ItIsNotDefault) <$> newHoleInstance loc
                 return
                   AppBuilderArg
                     { _appBuilderArg =

src/Juvix/Data/Fixity.hs

@@ -71,27 +71,35 @@ isBinary f = case f ^. fixityArity of
 isUnary :: Fixity -> Bool
 isUnary = not . isBinary
 
+letFixity :: Fixity
+letFixity =
+  Fixity
+    { _fixityPrecedence = PrecArrow,
+      _fixityArity = OpBinary AssocRight,
+      _fixityId = Nothing
+    }
+
 appFixity :: Fixity
 appFixity =
   Fixity
     { _fixityPrecedence = PrecApp,
-      _fixityArity = (OpBinary AssocLeft),
+      _fixityArity = OpBinary AssocLeft,
       _fixityId = Nothing
     }
 
 funFixity :: Fixity
 funFixity =
   Fixity
     { _fixityPrecedence = PrecArrow,
-      _fixityArity = (OpBinary AssocRight),
+      _fixityArity = OpBinary AssocRight,
       _fixityId = Nothing
     }
 
 updateFixity :: Fixity
 updateFixity =
   Fixity
     { _fixityPrecedence = PrecUpdate,
-      _fixityArity = (OpUnary AssocPostfix),
+      _fixityArity = OpUnary AssocPostfix,
       _fixityId = Nothing
     }