diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs index dcbb48045..69b3f3520 100644 --- a/src/Juvix/Compiler/Internal/Extra/Base.hs +++ b/src/Juvix/Compiler/Internal/Extra/Base.hs @@ -292,7 +292,7 @@ inductiveTypeVarsAssoc def l vars :: [VarName] vars = def ^.. inductiveParameters . each . inductiveParamName -substitutionApp :: forall r. (Member NameIdGen r) => (Maybe Name, Expression) -> Expression -> Sem r Expression +substitutionApp :: forall r expr. (Member NameIdGen r, HasExpressions expr) => (Maybe Name, Expression) -> expr -> Sem r expr substitutionApp (mv, ty) = case mv of Nothing -> return Just v -> substitutionE (HashMap.singleton v ty) @@ -300,7 +300,7 @@ substitutionApp (mv, ty) = case mv of localsToSubsE :: LocalVars -> Subs localsToSubsE l = ExpressionIden . IdenVar <$> l ^. localTyMap -substitutionE :: forall r. (Member NameIdGen r) => Subs -> Expression -> Sem r Expression +substitutionE :: forall r expr. (Member NameIdGen r, HasExpressions expr) => Subs -> expr -> Sem r expr substitutionE m = leafExpressions goLeaf where goLeaf :: Expression -> Sem r Expression diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index 23e8567b1..794ee6bf6 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -331,6 +331,16 @@ instance PrettyCode Module where instance PrettyCode Interval where ppCode = return . annotate AnnCode . pretty +instance PrettyCode New.ArgId where + ppCode a = case a ^. New.argIdName . unIrrelevant of + Nothing -> do + f' <- ppCode (a ^. New.argIdFunctionName) + return (ordinal (a ^. New.argIdIx) <+> "argument of" <+> f') + Just n -> do + n' <- ppCode n + loc' <- ppCode (getLoc n) + return (n' <+> "at" <+> loc') + instance PrettyCode New.ArityParameter where ppCode = return . pretty 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 3158c79f8..f696d9e95 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -9,6 +9,7 @@ where import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet +import Data.List.NonEmpty qualified as NonEmpty import Juvix.Compiler.Builtins.Effect import Juvix.Compiler.Concrete.Data.Highlight.Input import Juvix.Compiler.Internal.Data.Cast @@ -33,13 +34,35 @@ import Juvix.Prelude hiding (fromEither) type MCache = Cache ModuleIndex Module +data FunctionDefault = FunctionDefault + { _functionDefaultLeft :: FunctionParameter, + _functionDefaultDefault :: Maybe (ArgId, Expression), + _functionDefaultRight :: BuilderType + } + +-- TODO better name +data BuilderType + = BuilderTypeNoDefaults Expression + | BuilderTypeDefaults FunctionDefault + +data IsDefault + = ItIsDefault ArgId + | ItIsNotDefault + +data AppBuilderArg = AppBuilderArg + { _appBuilderArgIsDefault :: IsDefault, + _appBuilderArg :: ApplicationArg + } + data AppBuilder = AppBuilder { _appBuilder :: Expression, - _appBuilderType :: Expression, - _appBuilderArgs :: [ApplicationArg] + _appBuilderType :: BuilderType, + _appBuilderArgs :: [AppBuilderArg] } makeLenses ''AppBuilder +makeLenses ''AppBuilderArg +makeLenses ''FunctionDefault registerConstructor :: (Members '[HighlightBuilder, State TypesTable, Reader InfoTable] r) => ConstructorDef -> Sem r () registerConstructor ctr = do @@ -78,7 +101,7 @@ checkModuleNoCache :: (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache, Termination] r) => ModuleIndex -> Sem r Module -checkModuleNoCache (ModuleIndex Module {..}) = do +checkModuleNoCache (ModuleIndex Module {..}) = runReader (mempty @InsertedArgsStack) $ do _moduleBody' <- evalState (mempty :: NegativeTypeParameters) . checkModuleBody @@ -93,7 +116,7 @@ checkModuleNoCache (ModuleIndex Module {..}) = do } checkModuleBody :: - (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache, Termination] r) => + (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache, Termination, Reader InsertedArgsStack] r) => ModuleBody -> Sem r ModuleBody checkModuleBody ModuleBody {..} = do @@ -112,14 +135,14 @@ checkImport :: checkImport = traverseOf importModule checkModuleIndex checkMutualBlock :: - (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination] r) => + (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination, Reader InsertedArgsStack] r) => MutualBlock -> Sem r MutualBlock checkMutualBlock s = runReader emptyLocalVars (checkTopMutualBlock s) checkInductiveDef :: forall r. - (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters, Output Example, Builtins, Termination, Output TypedHole, Output CastHole, Reader LocalVars] r) => + (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters, Output Example, Builtins, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) => InductiveDef -> Sem r InductiveDef checkInductiveDef InductiveDef {..} = runInferenceDef $ do @@ -185,7 +208,7 @@ withEmptyVars :: Sem (Reader LocalVars ': r) a -> Sem r a withEmptyVars = runReader emptyLocalVars checkTopMutualBlock :: - (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination] r) => + (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination, Reader InsertedArgsStack] r) => MutualBlock -> Sem r MutualBlock checkTopMutualBlock (MutualBlock ds) = @@ -193,7 +216,7 @@ checkTopMutualBlock (MutualBlock ds) = resolveCastHoles :: forall a r. - (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Inference, Output Example, Output TypedHole, State TypesTable, Termination] r) => + (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Inference, Output Example, Output TypedHole, State TypesTable, Termination, Reader InsertedArgsStack] r) => Sem (Output CastHole ': r) a -> Sem r a resolveCastHoles s = do @@ -222,7 +245,7 @@ resolveCastHoles s = do getNatTy = mkBuiltinInductive BuiltinNat checkMutualStatement :: - (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination] r) => + (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination, Reader InsertedArgsStack] r) => MutualStatement -> Sem r MutualStatement checkMutualStatement = \case @@ -250,7 +273,7 @@ unfoldFunType' e = do checkFunctionDef :: forall r. - (Members '[HighlightBuilder, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Inference, Termination, Output TypedHole, Output CastHole] r) => + (Members '[HighlightBuilder, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => FunctionDef -> Sem r FunctionDef checkFunctionDef FunctionDef {..} = do @@ -300,7 +323,7 @@ checkFunctionDef FunctionDef {..} = do withLocalTypeMaybe (p ^. paramName) (p ^. paramType) (go rest) checkIsType :: - (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole, Output CastHole] r) => + (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => Interval -> Expression -> Sem r Expression @@ -308,7 +331,7 @@ checkIsType = checkExpression . smallUniverseE checkDefType :: forall r. - (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole, Output CastHole] r) => + (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => Expression -> Sem r Expression checkDefType ty = checkIsType loc ty @@ -388,7 +411,7 @@ checkCoercionType FunctionDef {..} = case mi of ImplicitInstance -> throw (ErrWrongCoercionArgument (WrongCoercionArgument fp)) checkExample :: - (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Output Example, State TypesTable, Termination] r) => + (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Output Example, State TypesTable, Termination, Reader InsertedArgsStack] r) => Example -> Sem r Example checkExample e = do @@ -398,7 +421,7 @@ checkExample e = do checkExpression :: forall r. - (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Reader LocalVars, Inference, Output Example, Output TypedHole, State TypesTable, Termination, Output CastHole] r) => + (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Reader LocalVars, Inference, Output Example, Output TypedHole, State TypesTable, Termination, Output CastHole, Reader InsertedArgsStack] r) => Expression -> Expression -> Sem r Expression @@ -425,7 +448,7 @@ checkExpression expectedTy e = do resolveInstanceHoles :: forall a r. (HasExpressions a) => - (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Inference, Output Example, State TypesTable, Termination] r) => + (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Inference, Output Example, State TypesTable, Termination, Reader InsertedArgsStack] r) => Sem (Output TypedHole ': r) a -> Sem r a resolveInstanceHoles s = do @@ -443,7 +466,7 @@ resolveInstanceHoles s = do $ checkExpression _typedHoleType t checkFunctionParameter :: - (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole, Output CastHole] r) => + (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => FunctionParameter -> Sem r FunctionParameter checkFunctionParameter FunctionParameter {..} = do @@ -460,7 +483,7 @@ checkFunctionParameter FunctionParameter {..} = do } inferExpression :: - (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination] r) => + (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Reader InsertedArgsStack] r) => -- | type hint Maybe Expression -> Expression -> @@ -475,7 +498,7 @@ lookupVar v = do err = error $ "internal error: could not find var " <> ppTrace v <> " at " <> ppTrace (getLoc v) checkFunctionBody :: - (Members '[Reader LocalVars, Reader InfoTable, NameIdGen, Error TypeCheckerError, Output Example, Output TypedHole, State TypesTable, State HighlightInput, State FunctionsTable, Builtins, Inference, Termination, Output CastHole] r) => + (Members '[Reader LocalVars, Reader InfoTable, NameIdGen, Error TypeCheckerError, Output Example, Output TypedHole, State TypesTable, State HighlightInput, State FunctionsTable, Builtins, Inference, Termination, Output CastHole, Reader InsertedArgsStack] r) => Expression -> Expression -> Sem r Expression @@ -501,7 +524,7 @@ checkFunctionBody expectedTy body = -- | helper function for lambda functions and case branches checkClause :: forall r. - (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole, Output CastHole] r) => + (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => Interval -> -- | Type Expression -> @@ -754,7 +777,7 @@ checkPattern = go inferExpression' :: forall r. - (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Output TypedHole, Builtins, Termination, Output CastHole] r) => + (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Output TypedHole, Builtins, Termination, Output CastHole, Reader InsertedArgsStack, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression @@ -763,7 +786,7 @@ inferExpression' = holesHelper -- | Checks anything but an Application. Does not insert holes inferLeftAppExpression :: forall r. - (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Output TypedHole, Builtins, Termination, Output CastHole] r) => + (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Output TypedHole, Builtins, Termination, Output CastHole, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression @@ -991,7 +1014,7 @@ inferLeftAppExpression mhint e = case e of return (TypedExpression kind (ExpressionIden i)) -- | The hint is used for trailing holes only -holesHelper :: forall r. (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Output TypedHole, Builtins, Termination, Output CastHole] r) => Maybe Expression -> Expression -> Sem r TypedExpression +holesHelper :: forall r. (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Output TypedHole, Builtins, Termination, Output CastHole, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression holesHelper mhint expr = do let (f, args) = unfoldExpressionApp expr hint @@ -999,19 +1022,78 @@ holesHelper mhint expr = do | otherwise = Nothing arityCheckBuiltins f args fTy <- inferLeftAppExpression hint f - let iniBuilder = + iniBuilderType <- mkInitBuilderType fTy + let iniArg :: ApplicationArg -> AppBuilderArg + iniArg a = + AppBuilderArg + { _appBuilderArgIsDefault = ItIsNotDefault, + _appBuilderArg = a + } + iniBuilder = AppBuilder { _appBuilder = fTy ^. typedExpression, - _appBuilderType = fTy ^. typedType, - _appBuilderArgs = args + _appBuilderType = iniBuilderType, + _appBuilderArgs = map iniArg args } st' <- execState iniBuilder goArgs + let ty' = mkFinalBuilderType (st' ^. appBuilderType) return TypedExpression - { _typedType = st' ^. appBuilderType, + { _typedType = ty', _typedExpression = st' ^. appBuilder } where + mkFinalBuilderType :: BuilderType -> Expression + mkFinalBuilderType = \case + BuilderTypeNoDefaults e -> e + BuilderTypeDefaults f -> + ExpressionFunction + Function + { _functionLeft = f ^. functionDefaultLeft, + _functionRight = mkFinalBuilderType (f ^. functionDefaultRight) + } + + getFunctionName :: Expression -> Maybe Name + getFunctionName = \case + ExpressionIden (IdenFunction fun) -> Just fun + _ -> Nothing + + mkInitBuilderType :: TypedExpression -> Sem r BuilderType + mkInitBuilderType fTy = do + 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) + where + toFunctionDefaultMay :: Name -> Expression -> [ArgInfo] -> BuilderType + toFunctionDefaultMay funName ty infos = + let ixInfos = nonEmpty (indexFrom 0 infos) + in maybe (BuilderTypeNoDefaults ty) (BuilderTypeDefaults . toFunctionDefault funName ty) ixInfos + + toFunctionDefault :: Name -> Expression -> NonEmpty (Indexed ArgInfo) -> FunctionDefault + toFunctionDefault _argIdFunctionName e (Indexed _argIdIx a :| as) = case e of + ExpressionFunction f -> + FunctionDefault + { _functionDefaultLeft = f ^. functionLeft, + _functionDefaultRight = + 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 + } + _ -> impossible + arityCheckBuiltins :: Expression -> [ApplicationArg] -> Sem r () arityCheckBuiltins f args = do case f of @@ -1060,57 +1142,121 @@ holesHelper mhint expr = do insertTrailingHoles hintTy = do builderTy <- gets (^. appBuilderType) ariHint <- typeArity hintTy - ariExpr <- typeArity builderTy + (defaults, restExprTy) <- peelDefault builderTy + restExprAri <- typeArity restExprTy let preImplicits :: Arity -> [IsImplicit] preImplicits = takeWhile isImplicitOrInstance . map (^. arityParameterImplicit) . unfoldArity - preAriExpr = preImplicits ariExpr + preImplicitsTypeRest = preImplicits restExprAri preAriHint = preImplicits ariHint + preImplicitsInType = + length + ( takeWhile + isImplicitOrInstance + (map fst defaults ++ preImplicitsTypeRest) + ) loc <- getLoc <$> gets (^. appBuilder) - let toBeInserted :: [IsImplicit] = take (length preAriExpr - length preAriHint) preAriExpr - mkHoleArg :: IsImplicit -> Sem r' ApplicationArg - mkHoleArg i = - ApplicationArg i <$> case i of + let numberOfExtraHoles = preImplicitsInType - length preAriHint + toBeInserted :: [(IsImplicit, Maybe (ArgId, Expression))] = + take numberOfExtraHoles (defaults <> (map (,Nothing) preImplicitsTypeRest)) + mkHoleArg :: (IsImplicit, Maybe (ArgId, Expression)) -> Sem r' AppBuilderArg + mkHoleArg (i, mdef) = do + (_appArg, _appBuilderArgIsDefault) <- case i of Explicit -> impossible - Implicit -> newHoleImplicit loc - ImplicitInstance -> newHoleInstance loc + Implicit -> case mdef of + Nothing -> (,ItIsNotDefault) <$> newHoleImplicit loc + Just (uid, def) -> return (def, ItIsDefault uid) + ImplicitInstance -> (,ItIsNotDefault) <$> newHoleInstance loc + return + AppBuilderArg + { _appBuilderArg = + ApplicationArg + { _appArgIsImplicit = i, + _appArg + }, + _appBuilderArgIsDefault + } trailingHoles <- mapM mkHoleArg toBeInserted mapM_ addTrailingHole trailingHoles where - addTrailingHole :: ApplicationArg -> Sem r' () - addTrailingHole a = do - fun <- peekFunctionType (a ^. appArgIsImplicit) - modify' (over appBuilderArgs (a :)) - checkMatchingArg a fun + peelDefault :: BuilderType -> Sem r' ([(IsImplicit, Maybe (ArgId, Expression))], Expression) + peelDefault bty = runOutputList (go bty) + where + go :: BuilderType -> Sem (Output (IsImplicit, Maybe (ArgId, Expression)) ': r') Expression + go = \case + BuilderTypeNoDefaults e -> return e + BuilderTypeDefaults d -> do + let impl = d ^. functionDefaultLeft . paramImplicit + output (impl, d ^. functionDefaultDefault) + go (d ^. functionDefaultRight) - checkMatchingArg :: ApplicationArg -> Function -> Sem r' () + addTrailingHole :: AppBuilderArg -> Sem r' () + addTrailingHole holeArg = do + fun <- peekFunctionType (holeArg ^. appBuilderArg . appArgIsImplicit) + modify' (over appBuilderArgs (holeArg :)) + checkMatchingArg holeArg fun + + checkLoop :: AppBuilderArg -> Sem r' () + checkLoop arg = case arg ^. appBuilderArgIsDefault of + ItIsNotDefault -> return () + ItIsDefault uid -> do + st <- asks (^. insertedArgsStack) + case span (/= uid) st of + (_, []) -> return () + (c, _) -> + let cyc = NonEmpty.reverse (uid :| c) + in throw (ErrDefaultArgLoop (DefaultArgLoop cyc)) + + checkMatchingArg :: AppBuilderArg -> FunctionDefault -> Sem r' () checkMatchingArg arg fun = do dropArg - let funParam = fun ^. functionLeft + let funParam = fun ^. functionDefaultLeft funL = funParam ^. paramType - funR = fun ^. functionRight - arg' <- checkExpression funL (arg ^. appArg) - let subs :: Expression -> Sem r' Expression = substitutionApp (funParam ^. paramName, arg') + 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 :)) + 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 ^. appArgIsImplicit + _appImplicit = arg ^. appBuilderArg . appArgIsImplicit } - funR' <- subs funR + funR' <- subsBuilderType funR modify' (set appBuilderType funR') modify' (over appBuilder applyArg) - goNextArg :: ApplicationArg -> Sem r' () + goNextArg :: AppBuilderArg -> Sem r' () goNextArg arg = do - let i = arg ^. appArgIsImplicit + let i = arg ^. appBuilderArg . appArgIsImplicit fun <- peekFunctionType i insertMiddleHoleOrCheck fun i where - insertMiddleHoleOrCheck :: Function -> IsImplicit -> Sem r' () + insertMiddleHoleOrCheck :: FunctionDefault -> IsImplicit -> Sem r' () insertMiddleHoleOrCheck fun argImpl = - let funParam = fun ^. functionLeft + let funParam = fun ^. functionDefaultLeft funImpl = funParam ^. paramImplicit checkThisArg = checkMatchingArg arg fun >> goArgs in case (argImpl, funImpl) of @@ -1128,11 +1274,18 @@ holesHelper mhint expr = do insertMiddleHole impl = do l <- gets (^. appBuilder) let loc = getLoc l - h <- case impl of - Implicit -> newHoleImplicit loc - ImplicitInstance -> newHoleInstance loc + (h, _appBuilderArgIsDefault) <- case impl of + ImplicitInstance -> (,ItIsNotDefault) <$> newHoleInstance loc Explicit -> impossible - modify' (over appBuilderArgs (ApplicationArg impl h :)) + Implicit -> case fun ^. functionDefaultDefault of + Nothing -> (,ItIsNotDefault) <$> newHoleImplicit loc + Just (uid, e) -> return (e, ItIsDefault uid) + let a = + AppBuilderArg + { _appBuilderArg = ApplicationArg impl h, + _appBuilderArgIsDefault + } + modify' (over appBuilderArgs (a :)) goArgs throwExpectedExplicit :: Sem r' a @@ -1146,32 +1299,46 @@ holesHelper mhint expr = do _expectedExplicitArgumentIx = error "FIXME" } - peekFunctionType :: IsImplicit -> Sem r' Function + peekFunctionType :: IsImplicit -> Sem r' FunctionDefault peekFunctionType impl = do - ty <- gets (^. appBuilderType) >>= weakNormalize - case ty of - ExpressionFunction f -> return f - ExpressionHole h -> holeRefineToFunction impl h - _ -> throwExpectedFunTy - where - throwExpectedFunTy :: Sem r' a - throwExpectedFunTy = do - l <- gets (^. appBuilder) - builderTy <- gets (^. appBuilderType) - args <- gets (^. appBuilderArgs) - let a :: Expression = foldApplication l args - throw $ - ErrExpectedFunctionType - ExpectedFunctionType - { _expectedFunctionTypeExpression = a, - _expectedFunctionTypeLeft = l, - _expectedFunctionTypeType = builderTy - } + bty <- gets (^. appBuilderType) + case bty of + BuilderTypeNoDefaults ty -> fromNoDefault <$> peekFunctionNoDefaults ty + BuilderTypeDefaults s -> return s + where + fromNoDefault :: Function -> FunctionDefault + fromNoDefault f = + FunctionDefault + { _functionDefaultLeft = f ^. functionLeft, + _functionDefaultDefault = Nothing, + _functionDefaultRight = BuilderTypeNoDefaults (f ^. functionRight) + } + peekFunctionNoDefaults :: Expression -> Sem r' Function + peekFunctionNoDefaults ty0 = do + ty <- weakNormalize ty0 + case ty of + ExpressionFunction f -> return f + ExpressionHole h -> holeRefineToFunction impl h + _ -> throwExpectedFunTy + where + throwExpectedFunTy :: Sem r' a + throwExpectedFunTy = do + l <- gets (^. appBuilder) + builderTy <- gets (^. appBuilderType) + args <- gets (^. appBuilderArgs) + let a :: Expression = foldApplication l (map (^. appBuilderArg) args) + throw $ + ErrExpectedFunctionType + ExpectedFunctionType + { _expectedFunctionTypeExpression = a, + _expectedFunctionTypeLeft = l, + _expectedFunctionTypeType = (mkFinalBuilderType builderTy) + } dropArg :: Sem r' () dropArg = modify' (over appBuilderArgs (drop 1)) - peekArg :: Sem r' (Maybe ApplicationArg) + peekArg :: Sem r' (Maybe AppBuilderArg) peekArg = do b <- get return (head <$> nonEmpty (b ^. appBuilderArgs)) 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 5c0e9c200..4c4cf557b 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 @@ -4,9 +4,17 @@ import Juvix.Compiler.Internal.Extra import Juvix.Prelude import Juvix.Prelude.Pretty +data ArgId = ArgId + { _argIdFunctionName :: Name, + _argIdIx :: Int, + _argIdDefinitionLoc :: Irrelevant Interval, + _argIdName :: Irrelevant (Maybe Name) + } + deriving stock (Eq, Ord) + -- | Used to detect of cycles of default arguments in the arity checker. newtype InsertedArgsStack = InsertedArgsStack - { _insertedArgsStack :: [Name] + { _insertedArgsStack :: [ArgId] } deriving newtype (Monoid, Semigroup) @@ -20,9 +28,6 @@ data InsertedArg = InsertedArg _insertedArgDefault :: Bool } --- pattern ArityParam :: IsImplicit -> ArityParameter --- pattern ArityParam impl <- ArityParameter {_arityParameterImplicit = impl} - data Blocking = BlockingVar VarName | BlockingHole Hole @@ -65,11 +70,15 @@ instance Eq ArityParameter where (ari, impl) == (ari', impl') makeLenses ''UnfoldedArity +makeLenses ''ArgId makeLenses ''FunctionArity makeLenses ''InsertedArg makeLenses ''ArityParameter makeLenses ''InsertedArgsStack +instance HasLoc ArgId where + getLoc = (^. argIdDefinitionLoc . unIrrelevant) + arityParameterName :: Lens' ArityParameter (Maybe Name) arityParameterName = arityParameterInfo . argInfoName diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs index 7ca7e8fb8..894d22831 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -35,6 +35,7 @@ data TypeCheckerError | ErrExplicitInstanceArgument ExplicitInstanceArgument | ErrTraitNotTerminating TraitNotTerminating | ErrArityCheckerError ArityCheckerError + | ErrDefaultArgLoop DefaultArgLoop instance ToGenericError TypeCheckerError where genericError :: (Member (Reader GenericOptions) r) => TypeCheckerError -> Sem r GenericError @@ -62,3 +63,4 @@ instance ToGenericError TypeCheckerError where ErrExplicitInstanceArgument e -> genericError e ErrTraitNotTerminating e -> genericError e ErrArityCheckerError e -> genericError e + ErrDefaultArgLoop e -> genericError e diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs index fdded058b..0fdb48226 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs @@ -3,6 +3,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Er import Juvix.Compiler.Internal.Data.InstanceInfo import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Pretty (fromGenericOptions) +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Pretty import Juvix.Data.PPOutput import Juvix.Prelude @@ -620,3 +621,27 @@ instance ToGenericError TraitNotTerminating where <+> ppCode opts' (e ^. traitNotTerminating) <> line <> "Each parameter of a trait in an instance argument must be structurally smaller than some parameter of the trait in the instance target" + +newtype DefaultArgLoop = DefaultArgLoop + { _defaultArgLoop :: NonEmpty ArgId + } + +makeLenses ''DefaultArgLoop + +instance ToGenericError DefaultArgLoop where + genericError e = ask >>= generr + where + generr opts = + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = ppOutput msg, + _genericErrorIntervals = [i] + } + where + opts' = fromGenericOptions opts + i = getLoc (head (e ^. defaultArgLoop)) + msg :: Doc Ann = + "Inserting default arguments caused a loop. The involved arguments are:" + <> line + <> itemize (ppCode opts' <$> e ^. defaultArgLoop) diff --git a/test/Typecheck/PositiveNew.hs b/test/Typecheck/PositiveNew.hs index 9ac651b98..a2ae510b2 100644 --- a/test/Typecheck/PositiveNew.hs +++ b/test/Typecheck/PositiveNew.hs @@ -56,10 +56,7 @@ extraTests = ignored :: HashSet String ignored = HashSet.fromList - [ "Test066: Import function with a function call in default argument", - "Test068: Dependent default values inserted in the arity checker", - "Test069: Dependent default values for Ord trait", - "Test070: Nested default values and named arguments", + [ "Test070: Nested default values and named arguments", "Test071: Named application", -- This test does not pass with the new hole insertion algorithm "Test046: Polymorphic type arguments"