diff --git a/app/Commands/Dev/InstanceTermination.hs b/app/Commands/Dev/InstanceTermination.hs new file mode 100644 index 0000000000..bc82594d61 --- /dev/null +++ b/app/Commands/Dev/InstanceTermination.hs @@ -0,0 +1,9 @@ +module Commands.Dev.InstanceTermination where + +import Commands.Base +import Commands.Dev.InstanceTermination.Calls qualified as Calls +import Commands.Dev.InstanceTermination.Options + +runCommand :: InstanceTerminationCommand -> Sem r () +runCommand = \case + Calls opts -> Calls.runCommand opts diff --git a/app/Commands/Dev/InstanceTermination/Calls.hs b/app/Commands/Dev/InstanceTermination/Calls.hs new file mode 100644 index 0000000000..16117d88c0 --- /dev/null +++ b/app/Commands/Dev/InstanceTermination/Calls.hs @@ -0,0 +1,7 @@ +module Commands.Dev.InstanceTermination.Calls where + +import Commands.Base +import Commands.Dev.InstanceTermination.Calls.Options + +runCommand :: CallsOptions -> Sem r () +runCommand CallsOptions {} = return () diff --git a/app/Commands/Dev/InstanceTermination/Calls/Options.hs b/app/Commands/Dev/InstanceTermination/Calls/Options.hs new file mode 100644 index 0000000000..2d0ddcebf9 --- /dev/null +++ b/app/Commands/Dev/InstanceTermination/Calls/Options.hs @@ -0,0 +1,36 @@ +module Commands.Dev.InstanceTermination.Calls.Options where + +import CommonOptions +import GlobalOptions +import Juvix.Compiler.Internal.Pretty.Options qualified as Internal + +data CallsOptions = CallsOptions + { _callsShowDecreasingArgs :: Internal.ShowDecrArgs, + _callsInputFile :: AppPath File + } + deriving stock (Data) + +makeLenses ''CallsOptions + +parseCalls :: Parser CallsOptions +parseCalls = do + _callsShowDecreasingArgs <- + option + decrArgsParser + ( long "show-decreasing-args" + <> short 'd' + <> value Internal.ArgRel + <> helpDoc (enumHelp Internal.showDecrArgsHelp) + ) + _callsInputFile <- parseInputFile FileExtJuvix + pure CallsOptions {..} + where + decrArgsParser :: ReadM Internal.ShowDecrArgs + decrArgsParser = enumReader Proxy + +instance CanonicalProjection (GlobalOptions, CallsOptions) Internal.Options where + project (GlobalOptions {..}, CallsOptions {..}) = + Internal.defaultOptions + { Internal._optShowNameIds = _globalShowNameIds, + Internal._optShowDecreasingArgs = _callsShowDecreasingArgs + } diff --git a/app/Commands/Dev/InstanceTermination/Options.hs b/app/Commands/Dev/InstanceTermination/Options.hs new file mode 100644 index 0000000000..f2adbd6996 --- /dev/null +++ b/app/Commands/Dev/InstanceTermination/Options.hs @@ -0,0 +1,29 @@ +module Commands.Dev.InstanceTermination.Options + ( module Commands.Dev.InstanceTermination.Options, + module Commands.Dev.InstanceTermination.Calls.Options, + ) +where + +import Commands.Dev.InstanceTermination.Calls.Options +import Juvix.Prelude +import Options.Applicative + +newtype InstanceTerminationCommand + = Calls CallsOptions + deriving stock (Data) + +parseInstanceTerminationCommand :: Parser InstanceTerminationCommand +parseInstanceTerminationCommand = + hsubparser $ + mconcat + [ commandCalls + ] + where + commandCalls :: Mod CommandFields InstanceTerminationCommand + commandCalls = command "calls" minfo + where + minfo :: ParserInfo InstanceTerminationCommand + minfo = + info + (Calls <$> parseCalls) + (progDesc "Compute the calls table of a .juvix file") diff --git a/app/Commands/Dev/Termination/Calls/Options.hs b/app/Commands/Dev/Termination/Calls/Options.hs index 42639ba678..86b3055199 100644 --- a/app/Commands/Dev/Termination/Calls/Options.hs +++ b/app/Commands/Dev/Termination/Calls/Options.hs @@ -28,22 +28,14 @@ parseCalls = do ) _callsShowDecreasingArgs <- option - decrArgsParser + (enumReader Proxy) ( long "show-decreasing-args" <> short 'd' <> value Internal.ArgRel - <> help "possible values: argument, relation, both" + <> helpDoc (enumHelp Internal.showDecrArgsHelp) ) _callsInputFile <- optional (parseInputFile FileExtJuvix) pure CallsOptions {..} - where - decrArgsParser :: ReadM Internal.ShowDecrArgs - decrArgsParser = eitherReader $ \s -> - case map toLower s of - "argument" -> return Internal.OnlyArg - "relation" -> return Internal.OnlyRel - "both" -> return Internal.ArgRel - _ -> Left "bad argument" instance CanonicalProjection (GlobalOptions, CallsOptions) Internal.Options where project (GlobalOptions {..}, CallsOptions {..}) = diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index 8bf1367232..06f297bd10 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -13,6 +13,7 @@ import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Pretty.Options import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity qualified as New import Juvix.Compiler.Store.Internal.Data.InfoTable +import Juvix.Compiler.Store.Internal.Data.InstanceInfo import Juvix.Data.CodeAnn import Juvix.Data.Keyword.All qualified as Kw import Juvix.Prelude @@ -397,6 +398,9 @@ instance (PrettyCode a, PrettyCode b) => PrettyCode (Either a b) where r' <- ppCode r return ("Right" <+> r') +instance PrettyCode InstanceInfo where + ppCode = ppCode . (^. instanceInfoIden) + instance PrettyCode LocalVars where ppCode LocalVars {..} = ppCode (HashMap.toList _localTypes) diff --git a/src/Juvix/Compiler/Internal/Pretty/Options.hs b/src/Juvix/Compiler/Internal/Pretty/Options.hs index d4b3dbf9a5..0d16fd6cde 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Options.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Options.hs @@ -1,12 +1,25 @@ module Juvix.Compiler.Internal.Pretty.Options where import Juvix.Prelude +import Prelude qualified data ShowDecrArgs = OnlyArg | OnlyRel | ArgRel - deriving stock (Data) + deriving stock (Enum, Bounded, Data) + +instance Show ShowDecrArgs where + show = \case + OnlyArg -> "arg" + OnlyRel -> "rel" + ArgRel -> "both" + +showDecrArgsHelp :: (IsString str) => ShowDecrArgs -> str +showDecrArgsHelp = \case + OnlyRel -> "Show only the size relation" + OnlyArg -> "Show only the argument" + ArgRel -> "Show both the argument and the size relation" defaultOptions :: Options defaultOptions = diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/Base.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/Base.hs index acacb8c58e..79c20c9fcd 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/Base.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Data/Base.hs @@ -44,6 +44,7 @@ data Call = Call newtype LexOrder = LexOrder (NonEmpty Int) data CallMapBuilder' expr :: Effect where + -- | The first argument is the name of the caller AddCall :: FunctionName -> FunCall' expr -> CallMapBuilder' expr m () makeEffect ''CallMapBuilder' 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 43cca44727..4a4f56d1ef 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -20,7 +20,8 @@ import Juvix.Compiler.Internal.Extra.InstanceInfo import Juvix.Compiler.Internal.Pretty import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker (Termination) --- import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.LexOrder import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference @@ -403,12 +404,6 @@ getInstanceInfoHelper funName funTy = do let err = throw (ErrInvalidInstanceType (InvalidInstanceType funTy)) maybe err return (mkInstanceInfo (IdenFunction funName) funTy) --- | Does not normalize the type. TODO should we completely forbid type synonyms in instance declarations? --- getInstanceInfoTermination :: --- (Members '[Error TypeCheckerError] r) => --- FunctionDef -> --- Sem r InstanceInfo --- getInstanceInfoTermination FunctionDef {..} = getInstanceInfoHelper _funDefName _funDefType checkInstanceType :: forall r. (Members '[Error TypeCheckerError, Reader InfoTable, Inference, NameIdGen, ResultBuilder] r) => @@ -580,60 +575,65 @@ checkExpression expectedTy e = do checkResolveInstanceHoles :: forall r. - ( Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, Reader InsertedArgsStack] r + ( Members + '[ Reader InfoTable, + Reader BuiltinsTable, + ResultBuilder, + Error TypeCheckerError, + NameIdGen, + Inference, + Termination, + Reader InsertedArgsStack + ] + r ) => Sem (Output TypedInstanceHole ': r) (NonEmpty MutualStatement) -> Sem r (NonEmpty MutualStatement) checkResolveInstanceHoles s = do (holes, stmts :: NonEmpty MutualStatement) <- runOutputList s - -- infos <- mapM getInstanceInfo (stmts ^.. each . _StatementFunction . filtered isInstance) - -- checkInstanceTermination infos + infos <- mapM getInstanceInfo (stmts ^.. each . _StatementFunction . filtered isInstance) + checkInstanceTermination infos resolveInstanceHoles holes stmts where - --- isInstance :: FunctionDef -> Bool --- isInstance f = case f ^. funDefIsInstanceCoercion of --- Nothing -> False --- Just k -> case k of --- IsInstanceCoercionInstance -> True --- IsInstanceCoercionCoercion -> False + isInstance :: FunctionDef -> Bool + isInstance f = case f ^. funDefIsInstanceCoercion of + Nothing -> False + Just k -> case k of + IsInstanceCoercionInstance -> True + IsInstanceCoercionCoercion -> False -- {Show a} : Show (List a) --- checkInstanceTermination :: --- ( Members --- '[ Reader InfoTable, --- Error TypeCheckerError --- ] --- r --- ) => --- [InstanceInfo] -> --- Sem r () --- checkInstanceTermination instances = do --- -- TODO remove later calls to checkInstanceConstraints --- x :: [(InstanceInfo, [InstanceApp])] <- mapWithM checkInstanceConstraints instances --- undefined --- where --- cmpInstanceParam :: InstanceParam -> InstanceParam -> SizeRel' --- cmpInstanceParam = undefined - --- instanceCallMap :: [(InstanceInfo, [InstanceApp])] -> CallMap' InstanceParam --- instanceCallMap l = run . execCallMapBuilder . forM l $ \(ii, calls) -> --- forM calls $ \(call :: InstanceApp) -> do --- let arsg :: [FunCallArg' InstanceParam] = --- [ FunCallArg --- { _argExpression = x --- } --- | x :: InstanceParam <- call ^. instanceAppArgs --- ] --- let r :: CallRow = --- CallRow --- { --- } --- let c :: FunCall' InstanceParam = --- FunCall --- { --- } --- undefined +checkInstanceTermination :: + ( Members + '[ Reader InfoTable, + Error TypeCheckerError + ] + r + ) => + [InstanceInfo] -> + Sem r () +checkInstanceTermination instances = do + -- TODO remove later calls to checkInstanceConstraints + cm :: CallMap' InstanceParam <- mkInstanceCallMap <$> mapWithM checkInstanceConstraints instances + forM_ (mapWith findOrder (callMapRecursiveBehaviour cm)) $ \(recBehav, morder) -> case morder of + Just {} -> return () + Nothing -> + throw $ + ErrTraitNotTerminatingNew + TraitNotTerminatingNew + { _traitNotTerminatingNew = nonEmpty' [i | i <- instances, i ^. instanceInfoInductive == recBehav ^. recursiveBehaviourFun] + } + where + mkInstanceCallMap :: [(InstanceInfo, [InstanceApp])] -> CallMap' InstanceParam + mkInstanceCallMap l = run (execCallMapBuilder (forM l (uncurry addInstance))) + where + addInstance :: (Members '[CallMapBuilder' InstanceParam] r) => InstanceInfo -> [InstanceApp] -> Sem r () + addInstance i = mapM_ (addConstraint i) + + addConstraint :: (Members '[CallMapBuilder' InstanceParam] r) => InstanceInfo -> InstanceApp -> Sem r () + addConstraint InstanceInfo {..} InstanceApp {..} = do + let c :: FunCall' InstanceParam = mkFunCall cmpInstanceParam _instanceAppHead _instanceInfoParams _instanceAppArgs + addCall _instanceInfoInductive c resolveInstanceHoles :: forall a r. @@ -1001,16 +1001,14 @@ checkPattern = go _wrongNumberArgumentsIndTypeExpectedNumArgs = numParams } ) - when - (numArgs > numParams) - ( throw $ - ErrTooManyArgumentsIndType - WrongNumberArgumentsIndType - { _wrongNumberArgumentsIndTypeActualType = ty, - _wrongNumberArgumentsIndTypeActualNumArgs = numArgs, - _wrongNumberArgumentsIndTypeExpectedNumArgs = numParams - } - ) + when (numArgs > numParams) + . throw + $ ErrTooManyArgumentsIndType + WrongNumberArgumentsIndType + { _wrongNumberArgumentsIndTypeActualType = ty, + _wrongNumberArgumentsIndTypeActualNumArgs = numArgs, + _wrongNumberArgumentsIndTypeExpectedNumArgs = numParams + } return (Right (ind, zipExact params args)) inferExpression' :: 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 2f38e57bc3..2202cd33d3 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -36,6 +36,7 @@ data TypeCheckerError | ErrSubsumedInstance SubsumedInstance | ErrExplicitInstanceArgument ExplicitInstanceArgument | ErrTraitNotTerminating TraitNotTerminating + | ErrTraitNotTerminatingNew TraitNotTerminatingNew | ErrBuiltinNotDefined BuiltinNotDefined | ErrArityCheckerError ArityCheckerError | ErrDefaultArgLoop DefaultArgLoop @@ -65,6 +66,7 @@ instance ToGenericError TypeCheckerError where ErrSubsumedInstance e -> genericError e ErrExplicitInstanceArgument e -> genericError e ErrTraitNotTerminating e -> genericError e + ErrTraitNotTerminatingNew e -> genericError e ErrBuiltinNotDefined e -> genericError e ErrArityCheckerError e -> genericError e ErrDefaultArgLoop e -> genericError e @@ -93,6 +95,7 @@ instance Show TypeCheckerError where ErrSubsumedInstance {} -> "ErrSubsumedInstance" ErrExplicitInstanceArgument {} -> "ErrExplicitInstanceArgument" ErrTraitNotTerminating {} -> "ErrTraitNotTerminating" + ErrTraitNotTerminatingNew {} -> "ErrTraitNotTerminatingNew" ErrArityCheckerError {} -> "ErrArityCheckerError" ErrDefaultArgLoop {} -> "ErrDefaultArgLoop" ErrBuiltinNotDefined {} -> "ErrBuiltinNotDefined" 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 dbc0e2ff3f..d39518468c 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 @@ -586,6 +586,31 @@ instance ToGenericError ExplicitInstanceArgument where where i = getLoc (e ^. explicitInstanceArgumentParameter) +newtype TraitNotTerminatingNew = TraitNotTerminatingNew + { _traitNotTerminatingNew :: NonEmpty InstanceInfo + } + +makeLenses ''TraitNotTerminatingNew + +instance ToGenericError TraitNotTerminatingNew 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 ^. traitNotTerminatingNew)) + msg :: Doc CodeAnn = + "Unable to prove instance-termination." + <+> "Make sure that the constraints are decreasing on the following instances:" + <> line + <> itemize (ppCode opts' <$> (e ^. traitNotTerminatingNew)) + newtype TraitNotTerminating = TraitNotTerminating { _traitNotTerminating :: Expression } diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs index b11b1378f2..bdf1b01433 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs @@ -1,9 +1,11 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Traits.Termination ( checkTraitTermination, + cmpInstanceParam, ) where import Juvix.Compiler.Internal.Extra.InstanceInfo +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data.SizeRelation import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error import Juvix.Prelude @@ -33,3 +35,9 @@ checkStrictSubterm p1 p2 = case p2 of checkSubterm :: InstanceParam -> InstanceParam -> Bool checkSubterm p1 p2 = p1 == p2 || checkStrictSubterm p1 p2 + +cmpInstanceParam :: InstanceParam -> InstanceParam -> Maybe SizeRel' +cmpInstanceParam l r + | checkStrictSubterm l r = Just RLe + | l == r = Just REq + | otherwise = Nothing