From c237f292a7b71b769d7f99e196619d2fb4aa90bf Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Thu, 30 Nov 2023 19:17:00 +0100 Subject: [PATCH] Add dependent defaults for the new typechecker (#2541) This pr adds support for default values that depend on previous arguments. For instance, see [test071](https://github.com/anoma/juvix/blob/ca7d0fa06d7fca30c8d9abe87dfb2afc1b9bd8c9/tests/Compilation/positive/test071.juvix). - After #2540 is implemented, we'll be able to remove the old type checker (including the aritychecker). --- src/Juvix/Compiler/Internal/Data/InfoTable.hs | 12 +- src/Juvix/Compiler/Internal/Extra/Base.hs | 42 +++- src/Juvix/Compiler/Internal/Language.hs | 2 +- .../Internal/Translation/FromConcrete.hs | 60 ++--- .../FromConcrete/NamedArguments.hs | 19 +- .../Analysis/TypeChecking/Checker.hs | 2 +- .../Analysis/TypeChecking/CheckerNew.hs | 206 +++++++++++------- .../Analysis/TypeChecking/CheckerNew/Arity.hs | 5 +- src/Juvix/Data/Fixity.hs | 14 +- test/Compilation/PositiveNew.hs | 4 +- test/Typecheck/PositiveNew.hs | 4 +- 11 files changed, 236 insertions(+), 134 deletions(-) diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index cf6a87bd1a..fc6d04ec6e 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -4,6 +4,7 @@ module Juvix.Compiler.Internal.Data.InfoTable extendWithReplExpression, lookupConstructor, lookupConstructorArgTypes, + lookupFunctionMaybe, lookupFunction, lookupConstructorReturnType, lookupInductive, @@ -169,7 +170,7 @@ lookupConstructor f = do $ "impossible: " <> ppTrace f <> " is not in the InfoTable\n" - <> "The registered constructors are: " + <> "\nThe registered constructors are: " <> ppTrace (HashMap.keys tbl) lookupConstructorArgTypes :: (Member (Reader InfoTable) r) => Name -> Sem r ([InductiveParameter], [Expression]) @@ -188,13 +189,16 @@ lookupInductive f = do $ "impossible: " <> ppTrace f <> " is not in the InfoTable\n" - <> "The registered inductives are: " + <> "\nThe registered inductives are: " <> ppTrace (HashMap.keys tbl) +lookupFunctionMaybe :: forall r. (Member (Reader InfoTable) r) => Name -> Sem r (Maybe FunctionInfo) +lookupFunctionMaybe f = HashMap.lookup f <$> asks (^. infoFunctions) + lookupFunction :: forall r. (Member (Reader InfoTable) r) => Name -> Sem r FunctionInfo lookupFunction f = do err <- impossibleErr - HashMap.lookupDefault err f <$> asks (^. infoFunctions) + fromMaybe err <$> lookupFunctionMaybe f where impossibleErr :: Sem r a impossibleErr = do @@ -205,7 +209,7 @@ lookupFunction f = do <> ppTrace f <> " is not in the InfoTable\n" <> ppTrace (getLoc f) - <> "The registered functions are: " + <> "\nThe registered functions are: " <> ppTrace (HashMap.keys tbl) lookupAxiom :: (Member (Reader InfoTable) r) => Name -> Sem r AxiomInfo diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs index 43508eaf08..c4a62eb109 100644 --- a/src/Juvix/Compiler/Internal/Extra/Base.hs +++ b/src/Juvix/Compiler/Internal/Extra/Base.hs @@ -12,8 +12,6 @@ type Rename = HashMap VarName VarName type Subs = HashMap VarName Expression -type VarMap = HashMap VarName VarName - data ApplicationArg = ApplicationArg { _appArgIsImplicit :: IsImplicit, _appArg :: Expression @@ -126,9 +124,14 @@ instance HasExpressions SimpleLambda where pure (SimpleLambda bi' b') instance HasExpressions FunctionParameter where - leafExpressions f (FunctionParameter m i e) = do - e' <- leafExpressions f e - pure (FunctionParameter m i e') + leafExpressions f FunctionParameter {..} = do + ty' <- leafExpressions f _paramType + pure + FunctionParameter + { _paramType = ty', + _paramName, + _paramImplicit + } instance HasExpressions Function where leafExpressions f (Function l r) = do @@ -136,6 +139,18 @@ instance HasExpressions Function where r' <- leafExpressions f r pure (Function l' r') +instance HasExpressions ApplicationArg where + leafExpressions f ApplicationArg {..} = do + arg' <- leafExpressions f _appArg + pure + ApplicationArg + { _appArg = arg', + _appArgIsImplicit + } + +instance (HasExpressions a) => HasExpressions (Maybe a) where + leafExpressions = _Just . leafExpressions + instance HasExpressions Application where leafExpressions f (Application l r i) = do l' <- leafExpressions f l @@ -292,16 +307,24 @@ inductiveTypeVarsAssoc def l vars :: [VarName] vars = def ^.. inductiveParameters . each . inductiveParamName -substitutionApp :: forall r expr. (Member NameIdGen r, HasExpressions expr) => (Maybe Name, Expression) -> expr -> Sem r expr +substitutionApp :: (Maybe Name, Expression) -> Subs substitutionApp (mv, ty) = case mv of - Nothing -> return - Just v -> substitutionE (HashMap.singleton v ty) + Nothing -> mempty + Just v -> HashMap.singleton v ty localsToSubsE :: LocalVars -> Subs localsToSubsE l = ExpressionIden . IdenVar <$> l ^. localTyMap +subsKind :: [Name] -> NameKind -> Subs +subsKind uids k = + HashMap.fromList + [ (s, toExpression s') | s <- uids, let s' = toExpression (set nameKind k s) + ] + substitutionE :: forall r expr. (Member NameIdGen r, HasExpressions expr) => Subs -> expr -> Sem r expr -substitutionE m = leafExpressions goLeaf +substitutionE m + | null m = pure + | otherwise = leafExpressions goLeaf where goLeaf :: Expression -> Sem r Expression goLeaf = \case @@ -382,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) -> diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index 6f28e8d526..415c49716b 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/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 diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 826096ae86..d666edb900 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/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,35 +759,32 @@ 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)) cls <- goArgs appargs let args :: [Internal.Name] = appargs ^.. each . namedArgumentNewFunDef . signName . to goSymbol -- changes the kind from Variable to Function - updateKind :: Internal.Subs = - HashMap.fromList - [ (s, Internal.toExpression s') | s <- args, let s' = Internal.IdenFunction (set Internal.nameKind KNameFunction s) - ] + updateKind :: Internal.Subs = Internal.subsKind args KNameFunction napp' = Concrete.NamedApplication { _namedAppName = napp ^. namedApplicationNewName, _namedAppArgs = nonEmpty' (createArgumentBlocks (sig ^. nameSignatureArgs)) } - e <- goNamedApplication napp' + e <- goNamedApplication napp' extraArgs let l = Internal.Let { _letClauses = cls, @@ -841,18 +838,16 @@ goExpression = \case goDesugaredNamedApplication :: DesugaredNamedApplication -> Sem r Internal.Expression goDesugaredNamedApplication a = do let fun = goScopedIden (a ^. dnamedAppIdentifier) - updateKind :: Internal.Subs = - HashMap.fromList - [ (s, Internal.ExpressionIden s') | s <- a ^.. dnamedAppArgs . each . argName . to goSymbol, let s' = Internal.IdenFunction (set Internal.nameKind KNameFunction s) - ] + updateKind :: Internal.Subs = Internal.subsKind (a ^.. dnamedAppArgs . each . argName . to goSymbol) KNameFunction mkAppArg :: Arg -> Internal.ApplicationArg mkAppArg arg = Internal.ApplicationArg { _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 $ @@ -1004,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 diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs index 4bbb194f5a..59e8855bc2 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs +++ b/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 diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs index aeefd4d702..5af202871b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs @@ -915,7 +915,7 @@ inferExpression' hint e = case e of <> ppTrace (Application l r iapp) ) ) - ty <- substitutionApp (paraName, r') funR + ty <- substitutionE (substitutionApp (paraName, r')) funR return TypedExpression { _typedExpression = diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index f97e142a48..6dd87e37ff 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -34,13 +34,17 @@ import Juvix.Prelude hiding (fromEither) type MCache = Cache ModuleIndex Module +data FunctionDefaultInfo = FunctionDefaultInfo + { _functionDefaultArgId :: ArgId, + _functionDefaultValue :: Expression + } + data FunctionDefault = FunctionDefault { _functionDefaultLeft :: FunctionParameter, - _functionDefaultDefault :: Maybe (ArgId, Expression), + _functionDefaultDefault :: Maybe FunctionDefaultInfo, _functionDefaultRight :: BuilderType } --- TODO better name data BuilderType = BuilderTypeNoDefaults Expression | BuilderTypeDefaults FunctionDefault @@ -55,14 +59,51 @@ data AppBuilderArg = AppBuilderArg } data AppBuilder = AppBuilder - { _appBuilder :: Expression, + { _appBuilderLeft :: Expression, _appBuilderType :: BuilderType, + _appBuilderTypeCtx :: Subs, _appBuilderArgs :: [AppBuilderArg] } makeLenses ''AppBuilder makeLenses ''AppBuilderArg makeLenses ''FunctionDefault +makeLenses ''FunctionDefaultInfo + +instance HasExpressions FunctionDefaultInfo where + leafExpressions f i = do + val' <- leafExpressions f (i ^. functionDefaultValue) + pure + FunctionDefaultInfo + { _functionDefaultValue = val', + _functionDefaultArgId = i ^. functionDefaultArgId + } + +instance HasExpressions FunctionDefault where + leafExpressions f FunctionDefault {..} = do + l' <- leafExpressions f _functionDefaultLeft + r' <- leafExpressions f _functionDefaultRight + d' <- leafExpressions f _functionDefaultDefault + pure + FunctionDefault + { _functionDefaultLeft = l', + _functionDefaultRight = r', + _functionDefaultDefault = d' + } + +instance HasExpressions BuilderType where + leafExpressions f = \case + BuilderTypeNoDefaults e -> BuilderTypeNoDefaults <$> leafExpressions f e + BuilderTypeDefaults l -> BuilderTypeDefaults <$> leafExpressions f l + +instance HasExpressions AppBuilderArg where + leafExpressions f AppBuilderArg {..} = do + a' <- leafExpressions f _appBuilderArg + pure + AppBuilderArg + { _appBuilderArg = a', + _appBuilderArgIsDefault + } registerConstructor :: (Members '[HighlightBuilder, State TypesTable, Reader InfoTable] r) => ConstructorDef -> Sem r () registerConstructor ctr = do @@ -1043,18 +1084,30 @@ holesHelper mhint expr = do } iniBuilder = AppBuilder - { _appBuilder = fTy ^. typedExpression, + { _appBuilderLeft = fTy ^. typedExpression, _appBuilderType = iniBuilderType, + _appBuilderTypeCtx = mempty, _appBuilderArgs = map iniArg args } - st' <- execState iniBuilder goArgs + (insertedArgs, st') <- runOutputList (execState iniBuilder goAllArgs) let ty' = mkFinalBuilderType (st' ^. appBuilderType) - return - TypedExpression - { _typedType = ty', - _typedExpression = st' ^. appBuilder - } + expr' = mkFinalExpression (st' ^. appBuilderLeft) insertedArgs + let ret = + TypedExpression + { _typedType = ty', + _typedExpression = expr' + } + return ret where + mkArg :: InsertedArg -> ApplicationArg + mkArg i = + ApplicationArg + { _appArg = i ^. insertedValue, + _appArgIsImplicit = i ^. insertedImplicit + } + mkFinalExpression :: Expression -> [InsertedArg] -> Expression + mkFinalExpression f args = foldApplication f (map mkArg args) + mkFinalBuilderType :: BuilderType -> Expression mkFinalBuilderType = \case BuilderTypeNoDefaults e -> e @@ -1065,19 +1118,27 @@ holesHelper mhint expr = do _functionRight = mkFinalBuilderType (f ^. functionDefaultRight) } + extendCtx :: (Members '[State AppBuilder] r') => FunctionParameter -> Expression -> Sem r' () + extendCtx funParam arg' = whenJust (funParam ^. paramName) $ \nm -> do + modify' (over appBuilderTypeCtx (set (at nm) (Just arg'))) + + applyCtx :: (Members '[State AppBuilder, NameIdGen] r', HasExpressions expr) => expr -> Sem r' expr + applyCtx x = do + s <- gets (^. appBuilderTypeCtx) + substitutionE s x + getFunctionName :: Expression -> Maybe Name getFunctionName = \case ExpressionIden (IdenFunction fun) -> Just fun _ -> Nothing mkInitBuilderType :: TypedExpression -> Sem r BuilderType - mkInitBuilderType fTy = do + mkInitBuilderType fTy = let ty = fTy ^. typedType - case getFunctionName (fTy ^. typedExpression) of - Just fun -> do - infos <- (^. functionInfoDef . funDefArgsInfo) <$> lookupFunction fun - return $ toFunctionDefaultMay fun ty infos - Nothing -> return (BuilderTypeNoDefaults ty) + in runFailDefault (BuilderTypeNoDefaults ty) $ do + fun <- failMaybe (getFunctionName (fTy ^. typedExpression)) + infos <- (^. functionInfoDef . funDefArgsInfo) <$> lookupFunction fun + return $ toFunctionDefaultMay fun ty infos where toFunctionDefaultMay :: Name -> Expression -> [ArgInfo] -> BuilderType toFunctionDefaultMay funName ty infos = @@ -1087,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 (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 () @@ -1144,7 +1206,12 @@ holesHelper mhint expr = do goImplArgs k (ApplicationArg Implicit _ : as) = goImplArgs (k - 1) as goImplArgs _ as = return as - goArgs :: forall r'. (r' ~ State AppBuilder ': r) => Sem r' () + 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' () @@ -1152,9 +1219,9 @@ holesHelper mhint expr = do insertTrailingHoles :: Expression -> Sem r' () insertTrailingHoles hintTy = do - builderTy <- gets (^. appBuilderType) + builderTy <- gets (^. appBuilderType) >>= applyCtx ariHint <- typeArity hintTy - (defaults, restExprTy) <- peelDefault builderTy + let (defaults, restExprTy) = peelDefault builderTy restExprAri <- typeArity restExprTy let preImplicits :: Arity -> [IsImplicit] preImplicits = takeWhile isImplicitOrInstance . map (^. arityParameterImplicit) . unfoldArity @@ -1166,18 +1233,18 @@ holesHelper mhint expr = do isImplicitOrInstance (map fst defaults ++ preImplicitsTypeRest) ) - loc <- getLoc <$> gets (^. appBuilder) + loc <- getLoc <$> gets (^. appBuilderLeft) let numberOfExtraHoles = preImplicitsInType - length preAriHint - toBeInserted :: [(IsImplicit, Maybe (ArgId, Expression))] = - take numberOfExtraHoles (defaults <> (map (,Nothing) preImplicitsTypeRest)) - mkHoleArg :: (IsImplicit, Maybe (ArgId, Expression)) -> Sem r' AppBuilderArg + toBeInserted :: [(IsImplicit, Maybe FunctionDefaultInfo)] = + take numberOfExtraHoles (defaults <> map (,Nothing) preImplicitsTypeRest) + mkHoleArg :: (IsImplicit, Maybe FunctionDefaultInfo) -> Sem r' AppBuilderArg mkHoleArg (i, mdef) = do (_appArg, _appBuilderArgIsDefault) <- case i of Explicit -> impossible + ImplicitInstance -> (,ItIsNotDefault) <$> newHoleInstance loc Implicit -> case mdef of Nothing -> (,ItIsNotDefault) <$> newHoleImplicit loc - Just (uid, def) -> return (def, ItIsDefault uid) - ImplicitInstance -> (,ItIsNotDefault) <$> newHoleInstance loc + Just (FunctionDefaultInfo uid def) -> return (def, ItIsDefault uid) return AppBuilderArg { _appBuilderArg = @@ -1190,10 +1257,10 @@ holesHelper mhint expr = do trailingHoles <- mapM mkHoleArg toBeInserted mapM_ addTrailingHole trailingHoles where - peelDefault :: BuilderType -> Sem r' ([(IsImplicit, Maybe (ArgId, Expression))], Expression) - peelDefault bty = runOutputList (go bty) + peelDefault :: BuilderType -> ([(IsImplicit, Maybe FunctionDefaultInfo)], Expression) + peelDefault = run . runOutputList . go where - go :: BuilderType -> Sem (Output (IsImplicit, Maybe (ArgId, Expression)) ': r') Expression + go :: BuilderType -> Sem '[Output (IsImplicit, Maybe FunctionDefaultInfo)] Expression go = \case BuilderTypeNoDefaults e -> return e BuilderTypeDefaults d -> do @@ -1202,7 +1269,8 @@ holesHelper mhint expr = do go (d ^. functionDefaultRight) addTrailingHole :: AppBuilderArg -> Sem r' () - addTrailingHole holeArg = do + addTrailingHole holeArg0 = do + holeArg <- applyCtx holeArg0 fun <- peekFunctionType (holeArg ^. appBuilderArg . appArgIsImplicit) modify' (over appBuilderArgs (holeArg :)) checkMatchingArg holeArg fun @@ -1223,42 +1291,27 @@ holesHelper mhint expr = do dropArg let funParam = fun ^. functionDefaultLeft funL = funParam ^. paramType - funR = fun ^. functionDefaultRight checkLeft :: Sem r' Expression checkLeft = do checkLoop arg let adjustCtx = case fun ^. functionDefaultDefault of Nothing -> id - Just (uid, _) -> local (over insertedArgsStack (uid :)) + Just dinfo -> local (over insertedArgsStack (dinfo ^. functionDefaultArgId :)) adjustCtx (checkExpression funL (arg ^. appBuilderArg . appArg)) arg' <- checkLeft - let subsE :: (HasExpressions expr) => expr -> Sem r' expr - subsE = substitutionApp (funParam ^. paramName, arg') - subsBuilderType :: BuilderType -> Sem r' BuilderType = \case - BuilderTypeNoDefaults e -> BuilderTypeNoDefaults <$> subsE e - BuilderTypeDefaults FunctionDefault {..} -> do - def' <- mapM (secondM subsE) _functionDefaultDefault - l' <- subsE _functionDefaultLeft - r' <- subsBuilderType _functionDefaultRight - return - ( BuilderTypeDefaults - FunctionDefault - { _functionDefaultLeft = l', - _functionDefaultDefault = def', - _functionDefaultRight = r' - } - ) - applyArg :: Expression -> Expression - applyArg l = - ExpressionApplication - Application - { _appLeft = l, - _appRight = arg', - _appImplicit = arg ^. appBuilderArg . appArgIsImplicit + let applyArg :: Sem r' () + applyArg = do + extendCtx funParam arg' + output + InsertedArg + { _insertedImplicit = arg ^. appBuilderArg . appArgIsImplicit, + _insertedValue = arg', + _insertedArgDefault = case arg ^. appBuilderArgIsDefault of + ItIsDefault {} -> True + ItIsNotDefault -> False } - funR' <- subsBuilderType funR - modify' (set appBuilderType funR') - modify' (over appBuilder applyArg) + modify' (set appBuilderType (fun ^. functionDefaultRight)) + applyArg goNextArg :: AppBuilderArg -> Sem r' () goNextArg arg = do @@ -1284,14 +1337,14 @@ holesHelper mhint expr = do where insertMiddleHole :: IsImplicit -> Sem r' () insertMiddleHole impl = do - l <- gets (^. appBuilder) + l <- gets (^. appBuilderLeft) let loc = getLoc l (h, _appBuilderArgIsDefault) <- case impl of ImplicitInstance -> (,ItIsNotDefault) <$> newHoleInstance loc Explicit -> impossible Implicit -> case fun ^. functionDefaultDefault of Nothing -> (,ItIsNotDefault) <$> newHoleImplicit loc - Just (uid, e) -> return (e, ItIsDefault uid) + Just (FunctionDefaultInfo uid e) -> return (e, ItIsDefault uid) let a = AppBuilderArg { _appBuilderArg = ApplicationArg impl h, @@ -1302,7 +1355,7 @@ holesHelper mhint expr = do throwExpectedExplicit :: Sem r' a throwExpectedExplicit = do - l <- gets (^. appBuilder) + l <- gets (^. appBuilderLeft) throw . ErrArityCheckerError $ ErrExpectedExplicitArgument @@ -1314,9 +1367,10 @@ holesHelper mhint expr = do peekFunctionType :: IsImplicit -> Sem r' FunctionDefault peekFunctionType impl = do bty <- gets (^. appBuilderType) - case bty of + x <- case bty of BuilderTypeNoDefaults ty -> fromNoDefault <$> peekFunctionNoDefaults ty BuilderTypeDefaults s -> return s + applyCtx x where fromNoDefault :: Function -> FunctionDefault fromNoDefault f = @@ -1335,7 +1389,7 @@ holesHelper mhint expr = do where throwExpectedFunTy :: Sem r' a throwExpectedFunTy = do - l <- gets (^. appBuilder) + l <- gets (^. appBuilderLeft) builderTy <- gets (^. appBuilderType) args <- gets (^. appBuilderArgs) let a :: Expression = foldApplication l (map (^. appBuilderArg) args) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Arity.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Arity.hs index 11e5b50ae3..463d049fa0 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Arity.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Arity.hs @@ -1,6 +1,5 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity where -import Juvix.Compiler.Internal.Extra.Base import Juvix.Compiler.Internal.Language import Juvix.Prelude import Juvix.Prelude.Pretty @@ -22,8 +21,8 @@ newtype InsertedArgsStack = InsertedArgsStack -- | Helper type used during insertion of default arguments in the arity -- checker. data InsertedArg = InsertedArg - { _insertedArgName :: Name, - _insertedArg :: ApplicationArg, + { _insertedImplicit :: IsImplicit, + _insertedValue :: Expression, -- | True if this corresponds to an automatically inserted default argument. -- False if it is an inserted hole or an argument present in the source code. _insertedArgDefault :: Bool diff --git a/src/Juvix/Data/Fixity.hs b/src/Juvix/Data/Fixity.hs index fcafc74742..9f391e759c 100644 --- a/src/Juvix/Data/Fixity.hs +++ b/src/Juvix/Data/Fixity.hs @@ -71,11 +71,19 @@ 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 } @@ -83,7 +91,7 @@ funFixity :: Fixity funFixity = Fixity { _fixityPrecedence = PrecArrow, - _fixityArity = (OpBinary AssocRight), + _fixityArity = OpBinary AssocRight, _fixityId = Nothing } @@ -91,7 +99,7 @@ updateFixity :: Fixity updateFixity = Fixity { _fixityPrecedence = PrecUpdate, - _fixityArity = (OpUnary AssocPostfix), + _fixityArity = OpUnary AssocPostfix, _fixityId = Nothing } diff --git a/test/Compilation/PositiveNew.hs b/test/Compilation/PositiveNew.hs index 6d7d00cfb6..154cd35749 100644 --- a/test/Compilation/PositiveNew.hs +++ b/test/Compilation/PositiveNew.hs @@ -50,9 +50,7 @@ extraTests = ignored :: HashSet String ignored = HashSet.fromList - [ "Test070: Nested default values and named arguments", - "Test071: Named application (Ord instance with default cmp)", - "Test046: Polymorphic type arguments", + [ "Test046: Polymorphic type arguments", -- TODO allow lambda branches of different number of patterns "Test027: Church numerals" ] diff --git a/test/Typecheck/PositiveNew.hs b/test/Typecheck/PositiveNew.hs index 0577942e61..bec2e5a9c8 100644 --- a/test/Typecheck/PositiveNew.hs +++ b/test/Typecheck/PositiveNew.hs @@ -43,8 +43,6 @@ extraTests = [] ignored :: HashSet String ignored = HashSet.fromList - [ "Test070: Nested default values and named arguments", - "Test071: Named application (Ord instance with default cmp)", - -- This test does not pass with the new hole insertion algorithm + [ -- This test does not pass with the new hole insertion algorithm "Test046: Polymorphic type arguments" ]