diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 3570ac7506..ce7fe5f65c 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -52,6 +52,13 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO * The compiler now parses `~x.fun` as unquoting `x` rather than `x.fun` and `~(f 5).fun` as unquoting `(f 5)` rather than `(f 5).fun`. +* Add new pragma `%tcinline_fuel` to avoid totality checker from infinitely + inlining recursive function with `%tcinline` and hang forever. The default + value of `%tcinline_fuel` is `1000`. + +* Fix a bug in `CallGraph.idr` that caused compiler to hang forever even when + `%tcinline_fuel` is set. + * LHS of `with`-applications are parsed as `PWithApp` instead of `PApp`. As a consequence, `IWithApp` appears in `TTImp` values in elaborator scripts instead of `IApp`, as it should have been. diff --git a/CONTRIBUTORS b/CONTRIBUTORS index 58c15bb497..df5c99da8d 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -14,6 +14,7 @@ Andre Kuhlenschmidt André Videla Andy Lok Anthony Lodi +Anton Ping Arnaud Bailly Brian Wignall Bryn Keller diff --git a/docs/source/reference/pragmas.rst b/docs/source/reference/pragmas.rst index f4b1f06fe0..d78e529db0 100644 --- a/docs/source/reference/pragmas.rst +++ b/docs/source/reference/pragmas.rst @@ -151,6 +151,12 @@ the ``minimal`` directive priority over the ``compact`` directive if both are pr See the section for each codegen under :ref:`sect-execs` for available directives. +``%tcinline_fuel`` +-------------------- + +Set fuel to avoid totality checker from infinitely inlining recursive function with `%tcinline` and hang +forever. The default value is 1000. (See ``%tcinline`` pragma) + Pragmas on declarations ======================= diff --git a/src/Core/Context.idr b/src/Core/Context.idr index c12e21cd2d..739a43ff8c 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -2262,6 +2262,17 @@ setNFThreshold : {auto c : Ref Ctxt Defs} -> Nat -> Core () setNFThreshold max = update Ctxt { options->elabDirectives->nfThreshold := max } +export +setTcInlineFuel : {auto c : Ref Ctxt Defs} -> + Nat -> Core () +setTcInlineFuel fuel = update Ctxt { options->elabDirectives->tcInlineFuel := fuel } + +export +getTcInlineFuel : {auto c : Ref Ctxt Defs} -> Core Nat +getTcInlineFuel = do + defs <- get Ctxt + pure (tcInlineFuel (elabDirectives (options defs))) + export setSearchTimeout : {auto c : Ref Ctxt Defs} -> Integer -> Core () diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 5391bb02b8..a5142f69a9 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -132,6 +132,7 @@ record ElabDirectives where -- in addition to postfix (dot) projections -- default: yes prefixRecordProjections : Bool + tcInlineFuel : Nat public export record Session where @@ -230,7 +231,7 @@ defaultSession = MkSessionOpts False CoveringOnly False False Chez [] 1000 False export defaultElab : ElabDirectives -defaultElab = MkElabDirectives True True CoveringOnly 3 50 25 True +defaultElab = MkElabDirectives True True CoveringOnly 3 50 25 True 1000 -- FIXME: This turns out not to be reliably portable, since different systems -- may have tools with the same name but different required arugments. We diff --git a/src/Core/Termination/CallGraph.idr b/src/Core/Termination/CallGraph.idr index 1acf42a08f..185292996d 100644 --- a/src/Core/Termination/CallGraph.idr +++ b/src/Core/Termination/CallGraph.idr @@ -70,23 +70,24 @@ mutual findSC : {vars : _} -> {auto c : Ref Ctxt Defs} -> Defs -> Env Term vars -> Guardedness -> + List Name -> -- to avoid caseblock looping List (Term vars) -> -- LHS args Term vars -> -- RHS Core (List SCCall) - findSC {vars} defs env g pats (Bind fc n b sc) + findSC {vars} defs env g cbs pats (Bind fc n b sc) = pure $ !(findSCbinder b) ++ - !(findSC defs (b :: env) g (map weaken pats) sc) + !(findSC defs (b :: env) g cbs (map weaken pats) sc) where findSCbinder : Binder (Term vars) -> Core (List SCCall) - findSCbinder (Let _ c val ty) = findSC defs env g pats val + findSCbinder (Let _ c val ty) = findSC defs env g cbs pats val findSCbinder b = pure [] -- only types, no need to look -- If we're Guarded and find a Delay, continue with the argument as InDelay - findSC defs env Guarded pats (TDelay _ _ _ tm) - = findSC defs env InDelay pats tm - findSC defs env g pats (TDelay _ _ _ tm) - = findSC defs env g pats tm - findSC defs env g pats tm + findSC defs env Guarded cbs pats (TDelay _ _ _ tm) + = findSC defs env InDelay cbs pats tm + findSC defs env g cbs pats (TDelay _ _ _ tm) + = findSC defs env g cbs pats tm + findSC defs env g cbs pats tm = do let (fn, args) = getFnArgs tm -- if it's a 'case' or 'if' just go straight into the arguments Nothing <- handleCase fn args @@ -97,42 +98,42 @@ mutual -- If we're InDelay and find a constructor (or a function call which is -- guaranteed to return a constructor; AllGuarded set), continue as InDelay (InDelay, Ref fc (DataCon _ _) cn, args) => - do scs <- traverse (findSC defs env InDelay pats) args + do scs <- traverse (findSC defs env InDelay cbs pats) args pure (concat scs) -- If we're InDelay otherwise, just check the arguments, the -- function call is okay (InDelay, _, args) => - do scs <- traverse (findSC defs env Unguarded pats) args + do scs <- traverse (findSC defs env Unguarded cbs pats) args pure (concat scs) (Guarded, Ref fc (DataCon _ _) cn, args) => do Just ty <- lookupTyExact cn (gamma defs) | Nothing => do log "totality" 50 $ "Lookup failed" - findSCcall defs env Guarded pats fc cn args - findSCcall defs env Guarded pats fc cn args + findSCcall defs env Guarded cbs pats fc cn args + findSCcall defs env Guarded cbs pats fc cn args (Toplevel, Ref fc (DataCon _ _) cn, args) => do Just ty <- lookupTyExact cn (gamma defs) | Nothing => do log "totality" 50 $ "Lookup failed" - findSCcall defs env Guarded pats fc cn args - findSCcall defs env Guarded pats fc cn args + findSCcall defs env Guarded cbs pats fc cn args + findSCcall defs env Guarded cbs pats fc cn args (_, Ref fc Func fn, args) => do logC "totality" 50 $ pure $ "Looking up type of " ++ show !(toFullNames fn) Just ty <- lookupTyExact fn (gamma defs) | Nothing => do log "totality" 50 $ "Lookup failed" - findSCcall defs env Unguarded pats fc fn args - findSCcall defs env Unguarded pats fc fn args + findSCcall defs env Unguarded cbs pats fc fn args + findSCcall defs env Unguarded cbs pats fc fn args (_, f, args) => - do scs <- traverse (findSC defs env Unguarded pats) args + do scs <- traverse (findSC defs env Unguarded cbs pats) args pure (concat scs) where handleCase : Term vars -> List (Term vars) -> Core (Maybe (List SCCall)) handleCase (Ref fc nt n) args = do n' <- toFullNames n if caseFn n' - then Just <$> findSCcall defs env g pats fc n args + then Just <$> findSCcall defs env g cbs pats fc n args else pure Nothing handleCase _ _ = pure Nothing @@ -303,23 +304,24 @@ mutual findSCcall : {vars : _} -> {auto c : Ref Ctxt Defs} -> Defs -> Env Term vars -> Guardedness -> + List Name -> -- to avoid caseblock looping List (Term vars) -> FC -> Name -> List (Term vars) -> Core (List SCCall) - findSCcall defs env g pats fc fn_in args + findSCcall defs env g cbs pats fc fn_in args -- Under 'assert_total' we assume that all calls are fine, so leave -- the size change list empty = do fn <- getFullName fn_in logC "totality.termination.sizechange" 10 $ do pure $ "Looking under " ++ show !(toFullNames fn) aSmaller <- resolved (gamma defs) (NS builtinNS (UN $ Basic "assert_smaller")) cond [(fn == NS builtinNS (UN $ Basic "assert_total"), pure []) - ,(caseFn fn, - do scs1 <- traverse (findSC defs env g pats) args + ,(caseFn fn && not (elem fn cbs), + do scs1 <- traverse (findSC defs env g (fn::cbs) pats) args mps <- getCasePats defs fn pats args - scs2 <- traverse (findInCase defs g) $ fromMaybe [] mps + scs2 <- traverse (findInCase defs g (fn::cbs)) $ fromMaybe [] mps pure (concat (scs1 ++ scs2))) ] - (do scs <- traverse (findSC defs env g pats) args + (do scs <- traverse (findSC defs env g cbs pats) args pure ([MkSCCall fn (fromListList (map (mkChange defs aSmaller pats) args)) @@ -328,23 +330,25 @@ mutual findInCase : {auto c : Ref Ctxt Defs} -> Defs -> Guardedness -> + List Name -> -- to avoid caseblock looping (vs ** (Env Term vs, List (Term vs), Term vs)) -> Core (List SCCall) - findInCase defs g (_ ** (env, pats, tm)) + findInCase defs g cbs (_ ** (env, pats, tm)) = do logC "totality" 10 $ do ps <- traverse toFullNames pats pure ("Looking in case args " ++ show ps) logTermNF "totality" 10 " =" env tm rhs <- normaliseOpts tcOnly defs env tm - findSC defs env g pats (delazy defs rhs) + findSC defs env g cbs pats (delazy defs rhs) findCalls : {auto c : Ref Ctxt Defs} -> Defs -> (vars ** (Env Term vars, Term vars, Term vars)) -> Core (List SCCall) findCalls defs (_ ** (env, lhs, rhs_in)) = do let pargs = getArgs (delazy defs lhs) - rhs <- normaliseOpts tcOnly defs env rhs_in - findSC defs env Toplevel pargs (delazy defs rhs) + fuel <- getTcInlineFuel + rhs <- normaliseOpts ({fuel := Just fuel} tcOnly) defs env rhs_in + findSC defs env Toplevel [] pargs (delazy defs rhs) getSC : {auto c : Ref Ctxt Defs} -> Defs -> Def -> Core (List SCCall) diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index c8dc88d8c8..56590965d8 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -1332,6 +1332,7 @@ mutual Overloadable n => pure [IPragma fc [] (\nest, env => setNameFlag fc n Overloadable)] Extension e => pure [IPragma fc [] (\nest, env => setExtension e)] DefaultTotality tot => pure [IPragma fc [] (\_, _ => setDefaultTotalityOption tot)] + TcInlineFuel n => pure [IPragma fc [] (\nest, env => setTcInlineFuel n)] desugarDecl ps (PBuiltin fc type name) = pure [IBuiltin fc type name] export diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index e02f1591c2..a33e9a6b76 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1534,6 +1534,10 @@ directive fname indents tot <- totalityOpt fname atEnd indents pure (DefaultTotality tot) + <|> do decoratedPragma fname "tcinline_fuel" + fuel <- decorate fname Keyword $ intLit + atEnd indents + pure (TcInlineFuel (fromInteger fuel)) fix : Rule Fixity fix diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index b456956eb5..2252589015 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -381,6 +381,7 @@ mutual AutoImplicitDepth : Nat -> Directive NFMetavarThreshold : Nat -> Directive SearchTimeout : Integer -> Directive + TcInlineFuel : Nat -> Directive public export PField : Type diff --git a/tests/idris2/total/total025/Issue-2995.idr b/tests/idris2/total/total025/Issue-2995.idr new file mode 100644 index 0000000000..330cc0c41c --- /dev/null +++ b/tests/idris2/total/total025/Issue-2995.idr @@ -0,0 +1,15 @@ +-- see https://github.com/idris-lang/Idris2/issues/2995 + +%default total + +%tcinline +zs : Stream Nat +zs = Z :: zs + +%tcinline +zs' : Stream Nat -> Stream Nat +zs' xs = Z :: zs' xs + +%tcinline +zs'' : Stream Nat -> Stream Nat +zs'' = \xs => Z :: zs'' xs diff --git a/tests/idris2/total/total025/expected b/tests/idris2/total/total025/expected new file mode 100644 index 0000000000..ac470e3ab6 --- /dev/null +++ b/tests/idris2/total/total025/expected @@ -0,0 +1 @@ +1/1: Building Issue-2995 (Issue-2995.idr) diff --git a/tests/idris2/total/total025/run b/tests/idris2/total/total025/run new file mode 100755 index 0000000000..d9d5542e83 --- /dev/null +++ b/tests/idris2/total/total025/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Issue-2995.idr diff --git a/tests/idris2/total/total026/Issue-2995.idr b/tests/idris2/total/total026/Issue-2995.idr new file mode 100644 index 0000000000..772bced9e4 --- /dev/null +++ b/tests/idris2/total/total026/Issue-2995.idr @@ -0,0 +1,16 @@ +-- see https://github.com/idris-lang/Idris2/issues/2995 + +%default total + +%tcinline +incAll : Stream Nat -> Stream Nat +incAll (x::xs) = S x :: incAll xs + +%tcinline +incAll' : Stream Nat -> Stream Nat +incAll' = \(x::xs) => S x :: incAll' xs + +%tcinline +incAll'' : Stream Nat -> Stream Nat +incAll'' = \ys => case ys of + (x :: xs) => S x :: incAll'' xs diff --git a/tests/idris2/total/total026/expected b/tests/idris2/total/total026/expected new file mode 100644 index 0000000000..ac470e3ab6 --- /dev/null +++ b/tests/idris2/total/total026/expected @@ -0,0 +1 @@ +1/1: Building Issue-2995 (Issue-2995.idr) diff --git a/tests/idris2/total/total026/run b/tests/idris2/total/total026/run new file mode 100755 index 0000000000..d9d5542e83 --- /dev/null +++ b/tests/idris2/total/total026/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Issue-2995.idr diff --git a/tests/idris2/total/total027/TcInlineFuel.idr b/tests/idris2/total/total027/TcInlineFuel.idr new file mode 100644 index 0000000000..1b152050bf --- /dev/null +++ b/tests/idris2/total/total027/TcInlineFuel.idr @@ -0,0 +1,18 @@ +%default total + +%tcinline_fuel 42 + +%tcinline +f : Nat -> a -> a +f Z x = x +f (S k) x = f k x + +-- this will typecheck +g1 : Nat -> Nat +g1 Z = Z +g1 (S k) = g1 (f 41 k) + +-- but this will not +g2 : Nat -> Nat +g2 Z = Z +g2 (S k) = g2 (f 42 k) \ No newline at end of file diff --git a/tests/idris2/total/total027/expected b/tests/idris2/total/total027/expected new file mode 100644 index 0000000000..e729b411a1 --- /dev/null +++ b/tests/idris2/total/total027/expected @@ -0,0 +1,11 @@ +1/1: Building TcInlineFuel (TcInlineFuel.idr) +Error: g2 is not total, possibly not terminating due to recursive path Main.g2 + +TcInlineFuel:16:1--16:16 + 12 | g1 Z = Z + 13 | g1 (S k) = g1 (f 41 k) + 14 | + 15 | -- but this will not + 16 | g2 : Nat -> Nat + ^^^^^^^^^^^^^^^ + diff --git a/tests/idris2/total/total027/run b/tests/idris2/total/total027/run new file mode 100755 index 0000000000..1329f3b9d4 --- /dev/null +++ b/tests/idris2/total/total027/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check TcInlineFuel.idr