Skip to content

Commit

Permalink
put extra arguments of named applications inside let
Browse files Browse the repository at this point in the history
  • Loading branch information
janmasrovira authored and paulcadman committed Nov 30, 2023
1 parent eaa4dbc commit 84adb78
Show file tree
Hide file tree
Showing 6 changed files with 90 additions and 53 deletions.
1 change: 1 addition & 0 deletions src/Juvix/Compiler/Internal/Extra/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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) ->
Expand Down
2 changes: 1 addition & 1 deletion src/Juvix/Compiler/Internal/Language.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
50 changes: 33 additions & 17 deletions src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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))
Expand All @@ -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,
Expand Down Expand Up @@ -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 $
Expand Down Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ module Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments
DesugaredNamedApplication,
dnamedAppIdentifier,
dnamedAppArgs,
dnamedExtraArgs,
Arg,
argName,
argImplicit,
Expand All @@ -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)
Expand All @@ -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
Expand All @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down Expand Up @@ -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
Expand All @@ -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 ()
Expand Down Expand Up @@ -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
Expand All @@ -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 =
Expand Down
14 changes: 11 additions & 3 deletions src/Juvix/Data/Fixity.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
}

Expand Down

0 comments on commit 84adb78

Please sign in to comment.