From c6b96080c232526572ccd9e81dd249e6f924c0da Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 8 Feb 2023 11:15:21 +0000 Subject: [PATCH] [ refactor ] split up Core.Termination --- idris2api.ipkg | 3 + src/Core/Name.idr | 8 + src/Core/Termination.idr | 770 +--------------------------- src/Core/Termination/CallGraph.idr | 354 +++++++++++++ src/Core/Termination/Positivity.idr | 198 +++++++ src/Core/Termination/SizeChange.idr | 256 +++++++++ src/TTImp/ProcessDef.idr | 1 + 7 files changed, 825 insertions(+), 765 deletions(-) create mode 100644 src/Core/Termination/CallGraph.idr create mode 100644 src/Core/Termination/Positivity.idr create mode 100644 src/Core/Termination/SizeChange.idr diff --git a/idris2api.ipkg b/idris2api.ipkg index 7778a0817..d30f09b94 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -82,6 +82,9 @@ modules = Core.Primitives, Core.Reflect, Core.SchemeEval, + Core.Termination.CallGraph, + Core.Termination.SizeChange, + Core.Termination.Positivity, Core.Termination, Core.Transform, Core.TT, diff --git a/src/Core/Name.idr b/src/Core/Name.idr index f36fdcc42..d973aa285 100644 --- a/src/Core/Name.idr +++ b/src/Core/Name.idr @@ -156,6 +156,14 @@ isField : UserName -> Maybe String isField (Field str) = Just str isField _ = Nothing +export +caseFn : Name -> Bool +caseFn (CaseBlock _ _) = True +caseFn (DN _ n) = caseFn n +caseFn (NS _ n) = caseFn n +caseFn _ = False + + export displayUserName : UserName -> String displayUserName (Basic n) = n diff --git a/src/Core/Termination.idr b/src/Core/Termination.idr index 91ed866df..96d7f4c8b 100644 --- a/src/Core/Termination.idr +++ b/src/Core/Termination.idr @@ -7,6 +7,10 @@ import Core.Normalise import Core.TT import Core.Value +import Core.Termination.CallGraph +import Core.Termination.Positivity +import Core.Termination.SizeChange + import Libraries.Data.NameMap import Libraries.Data.SortedMap import Libraries.Data.SortedSet @@ -15,28 +19,6 @@ import Data.String %default covering --- Check that the names a function refers to are terminating -totRefs : {auto c : Ref Ctxt Defs} -> - Defs -> List Name -> Core Terminating -totRefs defs [] = pure IsTerminating -totRefs defs (n :: ns) - = do rest <- totRefs defs ns - Just d <- lookupCtxtExact n (gamma defs) - | Nothing => pure rest - case isTerminating (totality d) of - IsTerminating => pure rest - Unchecked => do - log "totality" 20 $ "Totality unchecked for " ++ show !(toFullNames n) - pure rest - _ => case rest of - NotTerminating (BadCall ns) - => toFullNames $ NotTerminating (BadCall (n :: ns)) - _ => toFullNames $ NotTerminating (BadCall [n]) - -totRefsIn : {auto c : Ref Ctxt Defs} -> - Defs -> Term vars -> Core Terminating -totRefsIn defs ty = totRefs defs (keys (getRefs (Resolved (-1)) ty)) - -- Check if all branches end up as constructor arguments, with no other -- function application, and set 'AllGuarded' if so. -- This is to check whether a function can be considered a constructor form @@ -87,587 +69,6 @@ checkIfGuarded fc n then allGuarded ps else pure False --- Equal for the purposes of size change means, ignoring as patterns, all --- non-metavariable positions are equal -scEq : Term vars -> Term vars -> Bool -scEq (Local _ _ idx _) (Local _ _ idx' _) = idx == idx' -scEq (Ref _ _ n) (Ref _ _ n') = n == n' -scEq (Meta _ _ i args) _ = True -scEq _ (Meta _ _ i args) = True -scEq (Bind _ _ b sc) (Bind _ _ b' sc') = False -- not checkable -scEq (App _ f a) (App _ f' a') = scEq f f' && scEq a a' -scEq (As _ _ a p) p' = scEq p p' -scEq p (As _ _ a p') = scEq p p' -scEq (TDelayed _ _ t) (TDelayed _ _ t') = scEq t t' -scEq (TDelay _ _ t x) (TDelay _ _ t' x') = scEq t t' && scEq x x' -scEq (TForce _ _ t) (TForce _ _ t') = scEq t t' -scEq (PrimVal _ c) (PrimVal _ c') = c == c' -scEq (Erased _ _) (Erased _ _) = True -scEq (TType _ _) (TType _ _) = True -scEq _ _ = False - -data Guardedness = Toplevel | Unguarded | Guarded | InDelay - -Show Guardedness where - show Toplevel = "Toplevel" - show Unguarded = "Unguarded" - show Guarded = "Guarded" - show InDelay = "InDelay" - --- Remove all force and delay annotations which are nothing to do with --- coinduction meaning that all Delays left guard coinductive calls. -delazy : Defs -> Term vars -> Term vars -delazy defs (TDelayed fc r tm) - = let tm' = delazy defs tm in - case r of - LInf => TDelayed fc r tm' - _ => tm' -delazy defs (TDelay fc r ty tm) - = let ty' = delazy defs ty - tm' = delazy defs tm in - case r of - LInf => TDelay fc r ty' tm' - _ => tm' -delazy defs (TForce fc r t) - = case r of - LInf => TForce fc r (delazy defs t) - _ => delazy defs t -delazy defs (Meta fc n i args) = Meta fc n i (map (delazy defs) args) -delazy defs (Bind fc x b sc) - = Bind fc x (map (delazy defs) b) (delazy defs sc) -delazy defs (App fc f a) = App fc (delazy defs f) (delazy defs a) -delazy defs (As fc s a p) = As fc s (delazy defs a) (delazy defs p) -delazy defs tm = tm - -mutual - findSC : {vars : _} -> - {auto c : Ref Ctxt Defs} -> - Defs -> Env Term vars -> Guardedness -> - List (Nat, Term vars) -> -- LHS args and their position - Term vars -> -- Right hand side - Core (List SCCall) - findSC {vars} defs env g pats (Bind fc n b sc) - = pure $ - !(findSCbinder b) ++ - !(findSC defs (b :: env) g (map (\ (p, tm) => (p, weaken tm)) pats) sc) - where - findSCbinder : Binder (Term vars) -> Core (List SCCall) - findSCbinder (Let _ c val ty) = findSC defs env g 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 - = do let (fn, args) = getFnArgs tm - -- if it's a 'case' or 'if' just go straight into the arguments - Nothing <- handleCase fn args - | Just res => pure res - fn' <- conIfGuarded fn -- pretend it's a data constructor if - -- it has the AllGuarded flag - case (g, fn', args) of - -- 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 - 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 - pure (concat scs) - (Guarded, Ref fc (DataCon _ _) cn, args) => - do scs <- traverse (findSC defs env Guarded pats) args - pure (concat scs) - (Toplevel, Ref fc (DataCon _ _) cn, args) => - do scs <- traverse (findSC defs env Guarded pats) args - pure (concat scs) - (_, 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 0 args - arity <- getArity defs [] ty - findSCcall defs env Unguarded pats fc fn arity args - (_, f, args) => - do scs <- traverse (findSC defs env Unguarded 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 4 args - else pure Nothing - handleCase _ _ = pure Nothing - - conIfGuarded : Term vars -> Core (Term vars) - conIfGuarded (Ref fc Func n) - = do defs <- get Ctxt - Just gdef <- lookupCtxtExact n (gamma defs) - | Nothing => pure $ Ref fc Func n - if AllGuarded `elem` flags gdef - then pure $ Ref fc (DataCon 0 0) n - else pure $ Ref fc Func n - conIfGuarded tm = pure tm - - -- Expand the size change argument list with 'Nothing' to match the given - -- arity (i.e. the arity of the function we're calling) to ensure that - -- it's noted that we don't know the size change relationship with the - -- extra arguments. - expandToArity : Nat -> List (Maybe (Nat, SizeChange)) -> - List (Maybe (Nat, SizeChange)) - expandToArity Z xs = xs - expandToArity (S k) (x :: xs) = x :: expandToArity k xs - expandToArity (S k) [] = Nothing :: expandToArity k [] - - -- Return whether first argument is structurally smaller than the second. - smaller : Bool -> -- Have we gone under a constructor yet? - Defs -> - Maybe (Term vars) -> -- Asserted bigger thing - Term vars -> -- Term we're checking - Term vars -> -- Argument it might be smaller than - Bool - smaller inc defs big _ (Erased _ _) = False -- Never smaller than an erased thing! - -- for an as pattern, it's smaller if it's smaller than either part - smaller inc defs big s (As _ _ p t) - = smaller inc defs big s p || smaller inc defs big s t - smaller True defs big s t - = s == t || smallerArg True defs big s t - smaller inc defs big s t = smallerArg inc defs big s t - - assertedSmaller : Maybe (Term vars) -> Term vars -> Bool - assertedSmaller (Just b) a = scEq b a - assertedSmaller _ _ = False - - smallerArg : Bool -> Defs -> - Maybe (Term vars) -> Term vars -> Term vars -> Bool - smallerArg inc defs big (As _ _ _ s) tm = smallerArg inc defs big s tm - smallerArg inc defs big s tm - -- If we hit a pattern that is equal to a thing we've asserted_smaller, - -- the argument must be smaller - = assertedSmaller big tm || - case getFnArgs tm of - (Ref _ (DataCon t a) cn, args) - => any (smaller True defs big s) args - _ => case s of - App _ f _ => smaller inc defs big f tm - -- Higher order recursive argument - _ => False - - -- if the argument is an 'assert_smaller', return the thing it's smaller than - asserted : Name -> Term vars -> Maybe (Term vars) - asserted aSmaller tm - = case getFnArgs tm of - (Ref _ nt fn, [_, _, b, _]) - => if fn == aSmaller - then Just b - else Nothing - _ => Nothing - - -- Calculate the size change for the given argument. - -- i.e., return the size relationship of the given argument with an entry - -- in 'pats'; the position in 'pats' and the size change. - -- Nothing if there is no relation with any of them. - mkChange : Defs -> Name -> - (pats : List (Nat, Term vars)) -> - (arg : Term vars) -> - Maybe (Nat, SizeChange) - mkChange defs aSmaller [] arg = Nothing - mkChange defs aSmaller ((i, As _ _ p parg) :: pats) arg - = mkChange defs aSmaller ((i, p) :: (i, parg) :: pats) arg - mkChange defs aSmaller ((i, parg) :: pats) arg - = cond [(scEq arg parg, Just (i, Same)), - (smaller False defs (asserted aSmaller arg) arg parg, Just (i, Smaller))] - (mkChange defs aSmaller pats arg) - - -- Given a name of a case function, and a list of the arguments being - -- passed to it, update the pattern list so that it's referring to the LHS - -- of the case block function and return the corresponding RHS. - -- This way, we can build case blocks directly into the size change graph - -- rather than treating the definitions separately. - getCasePats : {auto c : Ref Ctxt Defs} -> - {vars : _} -> - Defs -> Name -> List (Nat, Term vars) -> - List (Term vars) -> - Core (Maybe (List (vs ** (Env Term vs, - List (Nat, Term vs), Term vs)))) - getCasePats {vars} defs n pats args - = do Just (PMDef _ _ _ _ pdefs) <- lookupDefExact n (gamma defs) - | _ => pure Nothing - log "totality" 20 $ - unwords ["Looking at the", show (length pdefs), "cases of", show n] - let pdefs' = map matchArgs pdefs - logC "totality" 20 $ do - old <- for pdefs $ \ (_ ** (_, lhs, rhs)) => do - lhs <- toFullNames lhs - rhs <- toFullNames rhs - pure $ " " ++ show lhs ++ " => " ++ show rhs - new <- for pdefs' $ \ (_ ** (_, lhs, rhs)) => do - lhs <- traverse (toFullNames . snd) lhs - rhs <- toFullNames rhs - pure $ " " ++ show lhs ++ " => " ++ show rhs - pure $ unlines $ "Updated" :: old ++ " to:" :: new - pure $ Just pdefs' - - where - updateRHS : {vs, vs' : _} -> - List (Term vs, Term vs') -> Term vs -> Term vs' - updateRHS {vs} {vs'} ms tm - = case lookupTm tm ms of - Nothing => urhs tm - Just t => t - where - urhs : Term vs -> Term vs' - urhs (Local fc _ _ _) = Erased fc Placeholder - urhs (Ref fc nt n) = Ref fc nt n - urhs (Meta fc m i margs) = Meta fc m i (map (updateRHS ms) margs) - urhs (App fc f a) = App fc (updateRHS ms f) (updateRHS ms a) - urhs (As fc s a p) = As fc s (updateRHS ms a) (updateRHS ms p) - urhs (TDelayed fc r ty) = TDelayed fc r (updateRHS ms ty) - urhs (TDelay fc r ty tm) - = TDelay fc r (updateRHS ms ty) (updateRHS ms tm) - urhs (TForce fc r tm) = TForce fc r (updateRHS ms tm) - urhs (Bind fc x b sc) - = Bind fc x (map (updateRHS ms) b) - (updateRHS (map (\vt => (weaken (fst vt), weaken (snd vt))) ms) sc) - urhs (PrimVal fc c) = PrimVal fc c - urhs (Erased fc Impossible) = Erased fc Impossible - urhs (Erased fc Placeholder) = Erased fc Placeholder - urhs (Erased fc (Dotted t)) = Erased fc (Dotted (updateRHS ms t)) - urhs (TType fc u) = TType fc u - - lookupTm : Term vs -> List (Term vs, Term vs') -> Maybe (Term vs') - lookupTm tm [] = Nothing - lookupTm (As fc s p tm) tms -- Want to keep the pattern and the variable, - -- if there was an @ in the parent - = do tm' <- lookupTm tm tms - Just $ As fc s tm' (urhs tm) - lookupTm tm ((As fc s p tm', v) :: tms) - = if tm == p - then Just v - else do tm' <- lookupTm tm ((tm', v) :: tms) - Just $ As fc s (urhs p) tm' - lookupTm tm ((tm', v) :: tms) - = if tm == tm' - then Just v - else lookupTm tm tms - - updatePat : {vs, vs' : _} -> - List (Term vs, Term vs') -> (Nat, Term vs) -> (Nat, Term vs') - updatePat ms (n, tm) = (n, updateRHS ms tm) - - matchArgs : (vs ** (Env Term vs, Term vs, Term vs)) -> - (vs ** (Env Term vs, List (Nat, Term vs), Term vs)) - matchArgs (_ ** (env', lhs, rhs)) - = let patMatch = reverse (zip args (getArgs lhs)) in - (_ ** (env', map (updatePat patMatch) pats, rhs)) - - caseFn : Name -> Bool - caseFn (CaseBlock _ _) = True - caseFn (DN _ n) = caseFn n - caseFn (NS _ n) = caseFn n - caseFn _ = False - - findSCcall : {vars : _} -> - {auto c : Ref Ctxt Defs} -> - Defs -> Env Term vars -> Guardedness -> - List (Nat, Term vars) -> - FC -> Name -> Nat -> List (Term vars) -> - Core (List SCCall) - findSCcall defs env g pats fc fn_in arity args - -- Under 'assert_total' we assume that all calls are fine, so leave - -- the size change list empty - = do fn <- getFullName fn_in - log "totality.termination.sizechange" 10 $ "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 - mps <- getCasePats defs fn pats args - scs2 <- traverse (findInCase defs g) $ fromMaybe [] mps - pure (concat (scs1 ++ scs2))) - ] - (do scs <- traverse (findSC defs env g pats) args - pure ([MkSCCall fn - (expandToArity arity - (map (mkChange defs aSmaller pats) args)) - fc] - ++ concat scs)) - - findInCase : {auto c : Ref Ctxt Defs} -> - Defs -> Guardedness -> - (vs ** (Env Term vs, List (Nat, Term vs), Term vs)) -> - Core (List SCCall) - findInCase defs g (_ ** (env, pats, tm)) - = do logC "totality" 10 $ - do ps <- traverse toFullNames (map snd 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) - -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 - (zip (take (length pargs) [0..]) pargs) (delazy defs rhs) - -getSC : {auto c : Ref Ctxt Defs} -> - Defs -> Def -> Core (List SCCall) -getSC defs (PMDef _ args _ _ pats) - = do sc <- traverse (findCalls defs) pats - pure $ nub (concat sc) -getSC defs _ = pure [] - -export -calculateSizeChange : {auto c : Ref Ctxt Defs} -> - FC -> Name -> Core (List SCCall) -calculateSizeChange loc n - = do log "totality.termination.sizechange" 5 $ "Calculating Size Change: " ++ show !(toFullNames n) - defs <- get Ctxt - Just def <- lookupCtxtExact n (gamma defs) - | Nothing => undefinedName loc n - getSC defs (definition def) - -Arg : Type -Arg = Nat - -Change : Type -Change = List (Maybe (Arg, SizeChange)) - -Path : Type -Path = List (FC, Name) - -record ArgChange where - constructor MkArgChange - change : Change - path : Path - --- ignore path -Eq ArgChange where - (==) a1 a2 = a1.change == a2.change - -Ord ArgChange where - compare a1 a2 = compare a1.change a2.change - -Show ArgChange where - show a = show a.change ++ " @" ++ show a.path - --- sc-graphs to be added -WorkList : Type -WorkList = SortedSet (Name, Name, ArgChange) - --- transitively-closed (modulo work list) set of sc-graphs -SCSet : Type -SCSet = NameMap (NameMap (SortedSet ArgChange)) - -lookupMap : Name -> NameMap (NameMap v) -> NameMap v -lookupMap n m = fromMaybe empty (lookup n m) - -lookupSet : Ord v => Name -> NameMap (SortedSet v) -> SortedSet v -lookupSet n m = fromMaybe empty (lookup n m) - -lookupGraphs : Name -> Name -> SCSet -> SortedSet ArgChange -lookupGraphs f g = lookupSet g . lookupMap f - -selectDom : Name -> SCSet -> SCSet -selectDom f s = insert f (lookupMap f s) empty - -selectCod : Name -> SCSet -> SCSet -selectCod g s = map (\m => insert g (lookupSet g m) empty) s - -foldl : (acc -> Name -> Name -> ArgChange -> acc) -> acc -> SCSet -> acc -foldl f_acc acc - = foldlNames (\acc, f => - foldlNames (\acc, g => - foldl (\acc, c => f_acc acc f g c) acc) - acc) - acc - -insertGraph : Name -> Name -> ArgChange -> SCSet -> SCSet -insertGraph f g ch s - = let s_f = lookupMap f s in - let s_fg = lookupSet g s_f in - insert f (insert g (insert ch s_fg) s_f) s - -composeChange : Change -> Change -> Change -composeChange c1 c2 - = map ((=<<) (\(i, r) => updateArg r <$> getArg i c1)) c2 - where - getArg : forall a . Nat -> List (Maybe a) -> Maybe a - getArg _ [] = Nothing - getArg Z (x :: xs) = x - getArg (S k) (x :: xs) = getArg k xs - - updateArg : SizeChange -> (Arg, SizeChange) -> (Arg, SizeChange) - updateArg c arg@(_, Unknown) = arg - updateArg Unknown (i, _) = (i, Unknown) - updateArg c (i, Same) = (i, c) - updateArg c arg@(_, Smaller) = arg - -composeArgChange : ArgChange -> ArgChange -> ArgChange -composeArgChange a1 a2 - = MkArgChange - (composeChange a1.change a2.change) - (a1.path ++ a2.path) - -preCompose : Name -> ArgChange -> - SCSet -> - WorkList -> - Name -> Name -> ArgChange -> - WorkList -preCompose f ch1 s work _ h ch2 - = let ch = composeArgChange ch1 ch2 in - if contains ch (lookupGraphs f h s) then - work - else - insert (f, h, ch) work - -postCompose : Name -> ArgChange -> - SCSet -> - WorkList -> - Name -> Name -> ArgChange -> - WorkList -postCompose h ch2 s work f _ ch1 - = let ch = composeArgChange ch1 ch2 in - if contains ch (lookupGraphs f h s) then - work - else - insert (f, h, ch) work - -mutual - addGraph : {auto c : Ref Ctxt Defs} -> - Name -> Name -> ArgChange -> - WorkList -> - SCSet -> - SCSet - addGraph f g ch work s_in - = let s = insertGraph f g ch s_in - after = selectDom g s - work_pre = foldl (preCompose f ch s) work after - before = selectCod f s - work_post = foldl (postCompose g ch s) work_pre before in - transitiveClosure work_post s - - transitiveClosure : {auto c : Ref Ctxt Defs} -> - WorkList -> - SCSet -> - SCSet - transitiveClosure work s - = case pop work of - Nothing => s - Just ((f, g, ch), work) => - addGraph f g ch work s - --- find (potential) chain of calls to given function (inclusive) -prefixPath : NameMap (FC, Name) -> Name -> Path -prefixPath pred g = go g [] - where - go : Name -> Path -> Path - go g path - = let Just (l, f) = lookup g pred - | Nothing => path in - if f == g then -- we've reached the entry point! - path - else - go f ((l, g) :: path) - -findLoops : {auto c : Ref Ctxt Defs} -> SCSet -> Core (NameMap (Maybe Path)) -findLoops s - = do let loops = filterEndos (\a => composeChange a.change a.change == a.change) s - log "totality.termination.calc" 7 $ "Loops: " ++ show loops - let terms = map (foldMap (\a => checkDesc a.change a.path)) loops - pure terms - where - filterEndos : (ArgChange -> Bool) -> SCSet -> NameMap (List ArgChange) - filterEndos p = mapWithKey (\f, m => filter p (Data.SortedSet.toList (lookupSet f m))) - - checkDesc : Change -> Path -> Maybe Path - checkDesc [] p = Just p - checkDesc (Just (_, Smaller) :: _) p = Nothing - checkDesc (_ :: xs) p = checkDesc xs p - -findNonTerminatingLoop : {auto c : Ref Ctxt Defs} -> SCSet -> Core (Maybe (Name, Path)) -findNonTerminatingLoop s - = do loops <- findLoops s - pure $ findNonTerminating loops - where - findNonTerminating : NameMap (Maybe Path) -> Maybe (Name, Path) - findNonTerminating = foldlNames (\acc, g, m => map (g,) m <+> acc) empty - -setPrefixTerminating : {auto c : Ref Ctxt Defs} -> - Path -> Name -> Core () -setPrefixTerminating [] g = pure () -setPrefixTerminating (_ :: []) g = pure () -setPrefixTerminating ((l, f) :: p) g - = do setTerminating l f (NotTerminating (BadPath p g)) - setPrefixTerminating p g - -addFunctions : {auto c : Ref Ctxt Defs} -> - Defs -> - List GlobalDef -> -- functions we're adding - NameMap (FC, Name) -> -- functions we've already seen (and their predecessor) - WorkList -> - Core (Either Terminating (WorkList, NameMap (FC, Name))) -addFunctions defs [] pred work - = pure $ Right (work, pred) -addFunctions defs (d1 :: ds) pred work - = do log "totality.termination.calc" 8 $ "Adding function: " ++ show d1.fullname - calls <- foldlC resolveCall [] d1.sizeChange - let Nothing = find isNonTerminating calls - | Just (d2, l, _) => do let g = d2.fullname - log "totality.termination.calc" 7 $ "Non-terminating function call: " ++ show g - let init = prefixPath pred d1.fullname ++ [(l, g)] - setPrefixTerminating init g - pure $ Left (NotTerminating (BadPath init g)) - let (ds, pred, work) = foldl addCall (ds, pred, work) (filter isUnchecked calls) - addFunctions defs ds pred work - where - resolveCall : List (GlobalDef, FC, (Name, Name, ArgChange)) -> - SCCall -> - Core (List (GlobalDef, FC, (Name, Name, ArgChange))) - resolveCall calls (MkSCCall g ch l) - = do Just d2 <- lookupCtxtExact g (gamma defs) - | Nothing => do log "totality.termination.calc" 7 $ "Not found: " ++ show g - pure calls - pure ((d2, l, (d1.fullname, d2.fullname, MkArgChange ch [(l, d2.fullname)])) :: calls) - - addCall : (List GlobalDef, NameMap (FC, Name), WorkList) -> - (GlobalDef, FC, (Name, Name, ArgChange)) -> - (List GlobalDef, NameMap (FC, Name), WorkList) - addCall (ds, pred, work_in) (d2, l, c) - = let work = insert c work_in in - case lookup d2.fullname pred of - Just _ => - (ds, pred, work) - Nothing => - (d2 :: ds, insert d2.fullname (l, d1.fullname) pred, work) - - isNonTerminating : (GlobalDef, _, _) -> Bool - isNonTerminating (d2, _, _) - = case d2.totality.isTerminating of - NotTerminating _ => True - _ => False - - isUnchecked : (GlobalDef, _, _) -> Bool - isUnchecked (d2, _, _) - = case d2.totality.isTerminating of - Unchecked => True - _ => False - -initWork : {auto c : Ref Ctxt Defs} -> - Defs -> - GlobalDef -> -- entry - Core (Either Terminating (WorkList, NameMap (FC, Name))) -initWork defs def = addFunctions defs [def] (insert def.fullname (def.location, def.fullname) empty) empty - calcTerminating : {auto c : Ref Ctxt Defs} -> FC -> Name -> Core Terminating calcTerminating loc n @@ -679,7 +80,7 @@ calcTerminating loc n | bad => pure bad Right (work, pred) <- initWork defs def | Left bad => pure bad - let s = transitiveClosure work empty + let s = transitiveClosure work initSCSet Nothing <- findNonTerminatingLoop s | Just (g, loop) => ifThenElse (def.fullname == g) @@ -720,167 +121,6 @@ checkTerminating loc n pure tot' t => pure t -isAssertTotal : Ref Ctxt Defs => NHead{} -> Core Bool -isAssertTotal (NRef _ fn_in) = - do fn <- getFullName fn_in - pure (fn == NS builtinNS (UN $ Basic "assert_total")) -isAssertTotal _ = pure False - -nameIn : {auto c : Ref Ctxt Defs} -> - Defs -> List Name -> NF [] -> Core Bool -nameIn defs tyns (NBind fc x b sc) - = if !(nameIn defs tyns !(evalClosure defs (binderType b))) - then pure True - else do let nm = Ref fc Bound (MN ("NAMEIN_" ++ show x) 0) - let arg = toClosure defaultOpts [] nm - sc' <- sc defs arg - nameIn defs tyns sc' -nameIn defs tyns (NApp _ nh args) - = do False <- isAssertTotal nh - | True => pure False - anyM (nameIn defs tyns) - !(traverse (evalClosure defs . snd) args) -nameIn defs tyns (NTCon _ n _ _ args) - = if n `elem` tyns - then pure True - else do args' <- traverse (evalClosure defs . snd) args - anyM (nameIn defs tyns) args' -nameIn defs tyns (NDCon _ n _ _ args) - = anyM (nameIn defs tyns) - !(traverse (evalClosure defs . snd) args) -nameIn defs tyns (NDelayed fc lr ty) = nameIn defs tyns ty -nameIn defs tyns _ = pure False - --- Check an argument type doesn't contain a negative occurrence of any of --- the given type names -posArg : {auto c : Ref Ctxt Defs} -> - Defs -> List Name -> NF [] -> Core Terminating - -posArgs : {auto c : Ref Ctxt Defs} -> - Defs -> List Name -> List (Closure []) -> Core Terminating -posArgs defs tyn [] = pure IsTerminating -posArgs defs tyn (x :: xs) - = do xNF <- evalClosure defs x - logNF "totality.positivity" 50 "Checking parameter for positivity" [] xNF - IsTerminating <- posArg defs tyn xNF - | err => pure err - posArgs defs tyn xs - --- a tyn can only appear in the parameter positions of --- tc; report positivity failure if it appears anywhere else -posArg defs tyns nf@(NTCon loc tc _ _ args) = - do logNF "totality.positivity" 50 "Found a type constructor" [] nf - testargs <- case !(lookupDefExact tc (gamma defs)) of - Just (TCon _ _ params _ _ _ _ _) => do - log "totality.positivity" 50 $ - unwords [show tc, "has", show (length params), "parameters"] - pure $ splitParams 0 params (map snd args) - _ => throw (GenericMsg loc (show tc ++ " not a data type")) - let (params, indices) = testargs - False <- anyM (nameIn defs tyns) !(traverse (evalClosure defs) indices) - | True => pure (NotTerminating NotStrictlyPositive) - posArgs defs tyns params - where - splitParams : Nat -> List Nat -> List (Closure []) -> - ( List (Closure []) -- parameters (to be checked for strict positivity) - , List (Closure []) -- indices (to be checked for no mention at all) - ) - splitParams i ps [] = ([], []) - splitParams i ps (x :: xs) - = if i `elem` ps - then mapFst (x ::) (splitParams (S i) ps xs) - else mapSnd (x ::) (splitParams (S i) ps xs) --- a tyn can not appear as part of ty -posArg defs tyns nf@(NBind fc x (Pi _ _ e ty) sc) - = do logNF "totality.positivity" 50 "Found a Pi-type" [] nf - if !(nameIn defs tyns !(evalClosure defs ty)) - then pure (NotTerminating NotStrictlyPositive) - else do let nm = Ref fc Bound (MN ("POSCHECK_" ++ show x) 1) - let arg = toClosure defaultOpts [] nm - sc' <- sc defs arg - posArg defs tyns sc' -posArg defs tyns nf@(NApp fc nh args) - = do False <- isAssertTotal nh - | True => do logNF "totality.positivity" 50 "Trusting an assertion" [] nf - pure IsTerminating - logNF "totality.positivity" 50 "Found an application" [] nf - args <- traverse (evalClosure defs . snd) args - pure $ if !(anyM (nameIn defs tyns) args) - then NotTerminating NotStrictlyPositive - else IsTerminating -posArg defs tyn (NDelayed fc lr ty) = posArg defs tyn ty -posArg defs tyn nf - = do logNF "totality.positivity" 50 "Reached the catchall" [] nf - pure IsTerminating - -checkPosArgs : {auto c : Ref Ctxt Defs} -> - Defs -> List Name -> NF [] -> Core Terminating -checkPosArgs defs tyns (NBind fc x (Pi _ _ e ty) sc) - = case !(posArg defs tyns !(evalClosure defs ty)) of - IsTerminating => - do let nm = Ref fc Bound (MN ("POSCHECK_" ++ show x) 0) - let arg = toClosure defaultOpts [] nm - checkPosArgs defs tyns !(sc defs arg) - bad => pure bad -checkPosArgs defs tyns nf - = do logNF "totality.positivity" 50 "Giving up on non-Pi type" [] nf - pure IsTerminating - -checkCon : {auto c : Ref Ctxt Defs} -> - Defs -> List Name -> Name -> Core Terminating -checkCon defs tyns cn - = case !(lookupTyExact cn (gamma defs)) of - Nothing => do log "totality.positivity" 20 $ - "Couldn't find constructor " ++ show cn - pure Unchecked - Just ty => - case !(totRefsIn defs ty) of - IsTerminating => - do tyNF <- nf defs [] ty - logNF "totality.positivity" 20 "Checking the type " [] tyNF - checkPosArgs defs tyns tyNF - bad => pure bad - -checkData : {auto c : Ref Ctxt Defs} -> - Defs -> List Name -> List Name -> Core Terminating -checkData defs tyns [] = pure IsTerminating -checkData defs tyns (c :: cs) - = do log "totality.positivity" 40 $ - "Checking positivity of constructor " ++ show c - case !(checkCon defs tyns c) of - IsTerminating => checkData defs tyns cs - bad => pure bad - -blockingAssertTotal : {auto c : Ref Ctxt Defs} -> FC -> Core a -> Core a -blockingAssertTotal loc ma - = do defs <- get Ctxt - let at = NS builtinNS (UN $ Basic "assert_total") - Just _ <- lookupCtxtExact at (gamma defs) - | Nothing => ma - setVisibility loc at Private - a <- ma - setVisibility loc at Public - pure a - --- Calculate whether a type satisfies the strict positivity condition, and --- return whether it's terminating, along with its data constructors -calcPositive : {auto c : Ref Ctxt Defs} -> - FC -> Name -> Core (Terminating, List Name) -calcPositive loc n - = do defs <- get Ctxt - log "totality.positivity" 6 $ "Calculating positivity: " ++ show !(toFullNames n) - case !(lookupDefTyExact n (gamma defs)) of - Just (TCon _ _ _ _ _ tns dcons _, ty) => - case !(totRefsIn defs ty) of - IsTerminating => - do log "totality.positivity" 30 $ - "Now checking constructors of " ++ show !(toFullNames n) - t <- blockingAssertTotal loc $ checkData defs (n :: tns) dcons - pure (t , dcons) - bad => pure (bad, dcons) - Just _ => throw (GenericMsg loc (show n ++ " not a data type")) - Nothing => undefinedName loc n - -- Check whether a data type satisfies the strict positivity condition, and -- record in the context export diff --git a/src/Core/Termination/CallGraph.idr b/src/Core/Termination/CallGraph.idr new file mode 100644 index 000000000..a54131fbd --- /dev/null +++ b/src/Core/Termination/CallGraph.idr @@ -0,0 +1,354 @@ +module Core.Termination.CallGraph + +import Core.Context +import Core.Context.Log +import Core.Env +import Core.Normalise +import Core.Value + +import Data.String + +%default covering + +data Guardedness = Toplevel | Unguarded | Guarded | InDelay + +Show Guardedness where + show Toplevel = "Toplevel" + show Unguarded = "Unguarded" + show Guarded = "Guarded" + show InDelay = "InDelay" + +-- Equal for the purposes of size change means, ignoring as patterns, all +-- non-metavariable positions are equal +scEq : Term vars -> Term vars -> Bool +scEq (Local _ _ idx _) (Local _ _ idx' _) = idx == idx' +scEq (Ref _ _ n) (Ref _ _ n') = n == n' +scEq (Meta _ _ i args) _ = True +scEq _ (Meta _ _ i args) = True +scEq (Bind _ _ b sc) (Bind _ _ b' sc') = False -- not checkable +scEq (App _ f a) (App _ f' a') = scEq f f' && scEq a a' +scEq (As _ _ a p) p' = scEq p p' +scEq p (As _ _ a p') = scEq p p' +scEq (TDelayed _ _ t) (TDelayed _ _ t') = scEq t t' +scEq (TDelay _ _ t x) (TDelay _ _ t' x') = scEq t t' && scEq x x' +scEq (TForce _ _ t) (TForce _ _ t') = scEq t t' +scEq (PrimVal _ c) (PrimVal _ c') = c == c' +scEq (Erased _ _) (Erased _ _) = True +scEq (TType _ _) (TType _ _) = True +scEq _ _ = False + +-- Remove all force and delay annotations which are nothing to do with +-- coinduction meaning that all Delays left guard coinductive calls. +delazy : Defs -> Term vars -> Term vars +delazy defs (TDelayed fc r tm) + = let tm' = delazy defs tm in + case r of + LInf => TDelayed fc r tm' + _ => tm' +delazy defs (TDelay fc r ty tm) + = let ty' = delazy defs ty + tm' = delazy defs tm in + case r of + LInf => TDelay fc r ty' tm' + _ => tm' +delazy defs (TForce fc r t) + = case r of + LInf => TForce fc r (delazy defs t) + _ => delazy defs t +delazy defs (Meta fc n i args) = Meta fc n i (map (delazy defs) args) +delazy defs (Bind fc x b sc) + = Bind fc x (map (delazy defs) b) (delazy defs sc) +delazy defs (App fc f a) = App fc (delazy defs f) (delazy defs a) +delazy defs (As fc s a p) = As fc s (delazy defs a) (delazy defs p) +delazy defs tm = tm + +mutual + findSC : {vars : _} -> + {auto c : Ref Ctxt Defs} -> + Defs -> Env Term vars -> Guardedness -> + List (Nat, Term vars) -> -- LHS args and their position + Term vars -> -- Right hand side + Core (List SCCall) + findSC {vars} defs env g pats (Bind fc n b sc) + = pure $ + !(findSCbinder b) ++ + !(findSC defs (b :: env) g (map (\ (p, tm) => (p, weaken tm)) pats) sc) + where + findSCbinder : Binder (Term vars) -> Core (List SCCall) + findSCbinder (Let _ c val ty) = findSC defs env g 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 + = do let (fn, args) = getFnArgs tm + -- if it's a 'case' or 'if' just go straight into the arguments + Nothing <- handleCase fn args + | Just res => pure res + fn' <- conIfGuarded fn -- pretend it's a data constructor if + -- it has the AllGuarded flag + case (g, fn', args) of + -- 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 + 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 + pure (concat scs) + (Guarded, Ref fc (DataCon _ _) cn, args) => + do scs <- traverse (findSC defs env Guarded pats) args + pure (concat scs) + (Toplevel, Ref fc (DataCon _ _) cn, args) => + do scs <- traverse (findSC defs env Guarded pats) args + pure (concat scs) + (_, 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 0 args + arity <- getArity defs [] ty + findSCcall defs env Unguarded pats fc fn arity args + (_, f, args) => + do scs <- traverse (findSC defs env Unguarded 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 4 args + else pure Nothing + handleCase _ _ = pure Nothing + + conIfGuarded : Term vars -> Core (Term vars) + conIfGuarded (Ref fc Func n) + = do defs <- get Ctxt + Just gdef <- lookupCtxtExact n (gamma defs) + | Nothing => pure $ Ref fc Func n + if AllGuarded `elem` flags gdef + then pure $ Ref fc (DataCon 0 0) n + else pure $ Ref fc Func n + conIfGuarded tm = pure tm + + -- Expand the size change argument list with 'Nothing' to match the given + -- arity (i.e. the arity of the function we're calling) to ensure that + -- it's noted that we don't know the size change relationship with the + -- extra arguments. + expandToArity : Nat -> List (Maybe (Nat, SizeChange)) -> + List (Maybe (Nat, SizeChange)) + expandToArity Z xs = xs + expandToArity (S k) (x :: xs) = x :: expandToArity k xs + expandToArity (S k) [] = Nothing :: expandToArity k [] + + -- Return whether first argument is structurally smaller than the second. + smaller : Bool -> -- Have we gone under a constructor yet? + Defs -> + Maybe (Term vars) -> -- Asserted bigger thing + Term vars -> -- Term we're checking + Term vars -> -- Argument it might be smaller than + Bool + smaller inc defs big _ (Erased _ _) = False -- Never smaller than an erased thing! + -- for an as pattern, it's smaller if it's smaller than either part + smaller inc defs big s (As _ _ p t) + = smaller inc defs big s p || smaller inc defs big s t + smaller True defs big s t + = s == t || smallerArg True defs big s t + smaller inc defs big s t = smallerArg inc defs big s t + + assertedSmaller : Maybe (Term vars) -> Term vars -> Bool + assertedSmaller (Just b) a = scEq b a + assertedSmaller _ _ = False + + smallerArg : Bool -> Defs -> + Maybe (Term vars) -> Term vars -> Term vars -> Bool + smallerArg inc defs big (As _ _ _ s) tm = smallerArg inc defs big s tm + smallerArg inc defs big s tm + -- If we hit a pattern that is equal to a thing we've asserted_smaller, + -- the argument must be smaller + = assertedSmaller big tm || + case getFnArgs tm of + (Ref _ (DataCon t a) cn, args) + => any (smaller True defs big s) args + _ => case s of + App _ f _ => smaller inc defs big f tm + -- Higher order recursive argument + _ => False + + -- if the argument is an 'assert_smaller', return the thing it's smaller than + asserted : Name -> Term vars -> Maybe (Term vars) + asserted aSmaller tm + = case getFnArgs tm of + (Ref _ nt fn, [_, _, b, _]) + => if fn == aSmaller + then Just b + else Nothing + _ => Nothing + + -- Calculate the size change for the given argument. + -- i.e., return the size relationship of the given argument with an entry + -- in 'pats'; the position in 'pats' and the size change. + -- Nothing if there is no relation with any of them. + mkChange : Defs -> Name -> + (pats : List (Nat, Term vars)) -> + (arg : Term vars) -> + Maybe (Nat, SizeChange) + mkChange defs aSmaller [] arg = Nothing + mkChange defs aSmaller ((i, As _ _ p parg) :: pats) arg + = mkChange defs aSmaller ((i, p) :: (i, parg) :: pats) arg + mkChange defs aSmaller ((i, parg) :: pats) arg + = cond [(scEq arg parg, Just (i, Same)), + (smaller False defs (asserted aSmaller arg) arg parg, Just (i, Smaller))] + (mkChange defs aSmaller pats arg) + + -- Given a name of a case function, and a list of the arguments being + -- passed to it, update the pattern list so that it's referring to the LHS + -- of the case block function and return the corresponding RHS. + -- This way, we can build case blocks directly into the size change graph + -- rather than treating the definitions separately. + getCasePats : {auto c : Ref Ctxt Defs} -> + {vars : _} -> + Defs -> Name -> List (Nat, Term vars) -> + List (Term vars) -> + Core (Maybe (List (vs ** (Env Term vs, + List (Nat, Term vs), Term vs)))) + getCasePats {vars} defs n pats args + = do Just (PMDef _ _ _ _ pdefs) <- lookupDefExact n (gamma defs) + | _ => pure Nothing + log "totality" 20 $ + unwords ["Looking at the", show (length pdefs), "cases of", show n] + let pdefs' = map matchArgs pdefs + logC "totality" 20 $ do + old <- for pdefs $ \ (_ ** (_, lhs, rhs)) => do + lhs <- toFullNames lhs + rhs <- toFullNames rhs + pure $ " " ++ show lhs ++ " => " ++ show rhs + new <- for pdefs' $ \ (_ ** (_, lhs, rhs)) => do + lhs <- traverse (toFullNames . snd) lhs + rhs <- toFullNames rhs + pure $ " " ++ show lhs ++ " => " ++ show rhs + pure $ unlines $ "Updated" :: old ++ " to:" :: new + pure $ Just pdefs' + + where + updateRHS : {vs, vs' : _} -> + List (Term vs, Term vs') -> Term vs -> Term vs' + updateRHS {vs} {vs'} ms tm + = case lookupTm tm ms of + Nothing => urhs tm + Just t => t + where + urhs : Term vs -> Term vs' + urhs (Local fc _ _ _) = Erased fc Placeholder + urhs (Ref fc nt n) = Ref fc nt n + urhs (Meta fc m i margs) = Meta fc m i (map (updateRHS ms) margs) + urhs (App fc f a) = App fc (updateRHS ms f) (updateRHS ms a) + urhs (As fc s a p) = As fc s (updateRHS ms a) (updateRHS ms p) + urhs (TDelayed fc r ty) = TDelayed fc r (updateRHS ms ty) + urhs (TDelay fc r ty tm) + = TDelay fc r (updateRHS ms ty) (updateRHS ms tm) + urhs (TForce fc r tm) = TForce fc r (updateRHS ms tm) + urhs (Bind fc x b sc) + = Bind fc x (map (updateRHS ms) b) + (updateRHS (map (\vt => (weaken (fst vt), weaken (snd vt))) ms) sc) + urhs (PrimVal fc c) = PrimVal fc c + urhs (Erased fc Impossible) = Erased fc Impossible + urhs (Erased fc Placeholder) = Erased fc Placeholder + urhs (Erased fc (Dotted t)) = Erased fc (Dotted (updateRHS ms t)) + urhs (TType fc u) = TType fc u + + lookupTm : Term vs -> List (Term vs, Term vs') -> Maybe (Term vs') + lookupTm tm [] = Nothing + lookupTm (As fc s p tm) tms -- Want to keep the pattern and the variable, + -- if there was an @ in the parent + = do tm' <- lookupTm tm tms + Just $ As fc s tm' (urhs tm) + lookupTm tm ((As fc s p tm', v) :: tms) + = if tm == p + then Just v + else do tm' <- lookupTm tm ((tm', v) :: tms) + Just $ As fc s (urhs p) tm' + lookupTm tm ((tm', v) :: tms) + = if tm == tm' + then Just v + else lookupTm tm tms + + updatePat : {vs, vs' : _} -> + List (Term vs, Term vs') -> (Nat, Term vs) -> (Nat, Term vs') + updatePat ms (n, tm) = (n, updateRHS ms tm) + + matchArgs : (vs ** (Env Term vs, Term vs, Term vs)) -> + (vs ** (Env Term vs, List (Nat, Term vs), Term vs)) + matchArgs (_ ** (env', lhs, rhs)) + = let patMatch = reverse (zip args (getArgs lhs)) in + (_ ** (env', map (updatePat patMatch) pats, rhs)) + + findSCcall : {vars : _} -> + {auto c : Ref Ctxt Defs} -> + Defs -> Env Term vars -> Guardedness -> + List (Nat, Term vars) -> + FC -> Name -> Nat -> List (Term vars) -> + Core (List SCCall) + findSCcall defs env g pats fc fn_in arity args + -- Under 'assert_total' we assume that all calls are fine, so leave + -- the size change list empty + = do fn <- getFullName fn_in + log "totality.termination.sizechange" 10 $ "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 + mps <- getCasePats defs fn pats args + scs2 <- traverse (findInCase defs g) $ fromMaybe [] mps + pure (concat (scs1 ++ scs2))) + ] + (do scs <- traverse (findSC defs env g pats) args + pure ([MkSCCall fn + (expandToArity arity + (map (mkChange defs aSmaller pats) args)) + fc] + ++ concat scs)) + + findInCase : {auto c : Ref Ctxt Defs} -> + Defs -> Guardedness -> + (vs ** (Env Term vs, List (Nat, Term vs), Term vs)) -> + Core (List SCCall) + findInCase defs g (_ ** (env, pats, tm)) + = do logC "totality" 10 $ + do ps <- traverse toFullNames (map snd 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) + +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 + (zip (take (length pargs) [0..]) pargs) (delazy defs rhs) + +getSC : {auto c : Ref Ctxt Defs} -> + Defs -> Def -> Core (List SCCall) +getSC defs (PMDef _ args _ _ pats) + = do sc <- traverse (findCalls defs) pats + pure $ nub (concat sc) +getSC defs _ = pure [] + +export +calculateSizeChange : {auto c : Ref Ctxt Defs} -> + FC -> Name -> Core (List SCCall) +calculateSizeChange loc n + = do log "totality.termination.sizechange" 5 $ "Calculating Size Change: " ++ show !(toFullNames n) + defs <- get Ctxt + Just def <- lookupCtxtExact n (gamma defs) + | Nothing => undefinedName loc n + getSC defs (definition def) diff --git a/src/Core/Termination/Positivity.idr b/src/Core/Termination/Positivity.idr new file mode 100644 index 000000000..ce6716df3 --- /dev/null +++ b/src/Core/Termination/Positivity.idr @@ -0,0 +1,198 @@ +module Core.Termination.Positivity + +import Core.Context +import Core.Context.Log +import Core.Env +import Core.Normalise +import Core.Value + +import Data.String + +import Libraries.Data.NameMap + +%default covering + +-- Check that the names a function refers to are terminating +export +totRefs : {auto c : Ref Ctxt Defs} -> + Defs -> List Name -> Core Terminating +totRefs defs [] = pure IsTerminating +totRefs defs (n :: ns) + = do rest <- totRefs defs ns + Just d <- lookupCtxtExact n (gamma defs) + | Nothing => pure rest + case isTerminating (totality d) of + IsTerminating => pure rest + Unchecked => do + log "totality" 20 $ "Totality unchecked for " ++ show !(toFullNames n) + pure rest + _ => case rest of + NotTerminating (BadCall ns) + => toFullNames $ NotTerminating (BadCall (n :: ns)) + _ => toFullNames $ NotTerminating (BadCall [n]) + +totRefsIn : {auto c : Ref Ctxt Defs} -> + Defs -> Term vars -> Core Terminating +totRefsIn defs ty = totRefs defs (keys (getRefs (Resolved (-1)) ty)) + +isAssertTotal : Ref Ctxt Defs => NHead{} -> Core Bool +isAssertTotal (NRef _ fn_in) = + do fn <- getFullName fn_in + pure (fn == NS builtinNS (UN $ Basic "assert_total")) +isAssertTotal _ = pure False + +nameIn : {auto c : Ref Ctxt Defs} -> + Defs -> List Name -> NF [] -> Core Bool +nameIn defs tyns (NBind fc x b sc) + = if !(nameIn defs tyns !(evalClosure defs (binderType b))) + then pure True + else do let nm = Ref fc Bound (MN ("NAMEIN_" ++ show x) 0) + let arg = toClosure defaultOpts [] nm + sc' <- sc defs arg + nameIn defs tyns sc' +nameIn defs tyns (NApp _ nh args) + = do False <- isAssertTotal nh + | True => pure False + anyM (nameIn defs tyns) + !(traverse (evalClosure defs . snd) args) +nameIn defs tyns (NTCon _ n _ _ args) + = if n `elem` tyns + then pure True + else do args' <- traverse (evalClosure defs . snd) args + anyM (nameIn defs tyns) args' +nameIn defs tyns (NDCon _ n _ _ args) + = anyM (nameIn defs tyns) + !(traverse (evalClosure defs . snd) args) +nameIn defs tyns (NDelayed fc lr ty) = nameIn defs tyns ty +nameIn defs tyns _ = pure False + +-- Check an argument type doesn't contain a negative occurrence of any of +-- the given type names +posArg : {auto c : Ref Ctxt Defs} -> + Defs -> List Name -> NF [] -> Core Terminating + +posArgs : {auto c : Ref Ctxt Defs} -> + Defs -> List Name -> List (Closure []) -> Core Terminating +posArgs defs tyn [] = pure IsTerminating +posArgs defs tyn (x :: xs) + = do xNF <- evalClosure defs x + logNF "totality.positivity" 50 "Checking parameter for positivity" [] xNF + IsTerminating <- posArg defs tyn xNF + | err => pure err + posArgs defs tyn xs + +-- a tyn can only appear in the parameter positions of +-- tc; report positivity failure if it appears anywhere else +posArg defs tyns nf@(NTCon loc tc _ _ args) = + do logNF "totality.positivity" 50 "Found a type constructor" [] nf + testargs <- case !(lookupDefExact tc (gamma defs)) of + Just (TCon _ _ params _ _ _ _ _) => do + log "totality.positivity" 50 $ + unwords [show tc, "has", show (length params), "parameters"] + pure $ splitParams 0 params (map snd args) + _ => throw (GenericMsg loc (show tc ++ " not a data type")) + let (params, indices) = testargs + False <- anyM (nameIn defs tyns) !(traverse (evalClosure defs) indices) + | True => pure (NotTerminating NotStrictlyPositive) + posArgs defs tyns params + where + splitParams : Nat -> List Nat -> List (Closure []) -> + ( List (Closure []) -- parameters (to be checked for strict positivity) + , List (Closure []) -- indices (to be checked for no mention at all) + ) + splitParams i ps [] = ([], []) + splitParams i ps (x :: xs) + = if i `elem` ps + then mapFst (x ::) (splitParams (S i) ps xs) + else mapSnd (x ::) (splitParams (S i) ps xs) +-- a tyn can not appear as part of ty +posArg defs tyns nf@(NBind fc x (Pi _ _ e ty) sc) + = do logNF "totality.positivity" 50 "Found a Pi-type" [] nf + if !(nameIn defs tyns !(evalClosure defs ty)) + then pure (NotTerminating NotStrictlyPositive) + else do let nm = Ref fc Bound (MN ("POSCHECK_" ++ show x) 1) + let arg = toClosure defaultOpts [] nm + sc' <- sc defs arg + posArg defs tyns sc' +posArg defs tyns nf@(NApp fc nh args) + = do False <- isAssertTotal nh + | True => do logNF "totality.positivity" 50 "Trusting an assertion" [] nf + pure IsTerminating + logNF "totality.positivity" 50 "Found an application" [] nf + args <- traverse (evalClosure defs . snd) args + pure $ if !(anyM (nameIn defs tyns) args) + then NotTerminating NotStrictlyPositive + else IsTerminating +posArg defs tyn (NDelayed fc lr ty) = posArg defs tyn ty +posArg defs tyn nf + = do logNF "totality.positivity" 50 "Reached the catchall" [] nf + pure IsTerminating + +checkPosArgs : {auto c : Ref Ctxt Defs} -> + Defs -> List Name -> NF [] -> Core Terminating +checkPosArgs defs tyns (NBind fc x (Pi _ _ e ty) sc) + = case !(posArg defs tyns !(evalClosure defs ty)) of + IsTerminating => + do let nm = Ref fc Bound (MN ("POSCHECK_" ++ show x) 0) + let arg = toClosure defaultOpts [] nm + checkPosArgs defs tyns !(sc defs arg) + bad => pure bad +checkPosArgs defs tyns nf + = do logNF "totality.positivity" 50 "Giving up on non-Pi type" [] nf + pure IsTerminating + +checkCon : {auto c : Ref Ctxt Defs} -> + Defs -> List Name -> Name -> Core Terminating +checkCon defs tyns cn + = case !(lookupTyExact cn (gamma defs)) of + Nothing => do log "totality.positivity" 20 $ + "Couldn't find constructor " ++ show cn + pure Unchecked + Just ty => + case !(totRefsIn defs ty) of + IsTerminating => + do tyNF <- nf defs [] ty + logNF "totality.positivity" 20 "Checking the type " [] tyNF + checkPosArgs defs tyns tyNF + bad => pure bad + +checkData : {auto c : Ref Ctxt Defs} -> + Defs -> List Name -> List Name -> Core Terminating +checkData defs tyns [] = pure IsTerminating +checkData defs tyns (c :: cs) + = do log "totality.positivity" 40 $ + "Checking positivity of constructor " ++ show c + case !(checkCon defs tyns c) of + IsTerminating => checkData defs tyns cs + bad => pure bad + +blockingAssertTotal : {auto c : Ref Ctxt Defs} -> FC -> Core a -> Core a +blockingAssertTotal loc ma + = do defs <- get Ctxt + let at = NS builtinNS (UN $ Basic "assert_total") + Just _ <- lookupCtxtExact at (gamma defs) + | Nothing => ma + setVisibility loc at Private + a <- ma + setVisibility loc at Public + pure a + +-- Calculate whether a type satisfies the strict positivity condition, and +-- return whether it's terminating, along with its data constructors +export +calcPositive : {auto c : Ref Ctxt Defs} -> + FC -> Name -> Core (Terminating, List Name) +calcPositive loc n + = do defs <- get Ctxt + log "totality.positivity" 6 $ "Calculating positivity: " ++ show !(toFullNames n) + case !(lookupDefTyExact n (gamma defs)) of + Just (TCon _ _ _ _ _ tns dcons _, ty) => + case !(totRefsIn defs ty) of + IsTerminating => + do log "totality.positivity" 30 $ + "Now checking constructors of " ++ show !(toFullNames n) + t <- blockingAssertTotal loc $ checkData defs (n :: tns) dcons + pure (t , dcons) + bad => pure (bad, dcons) + Just _ => throw (GenericMsg loc (show n ++ " not a data type")) + Nothing => undefinedName loc n diff --git a/src/Core/Termination/SizeChange.idr b/src/Core/Termination/SizeChange.idr new file mode 100644 index 000000000..e70914ff6 --- /dev/null +++ b/src/Core/Termination/SizeChange.idr @@ -0,0 +1,256 @@ +module Core.Termination.SizeChange + +import Core.Context +import Core.Context.Log +import Core.Name + +import Libraries.Data.NameMap +import Libraries.Data.SortedMap +import Libraries.Data.SortedSet + +%default covering + +Arg : Type +Arg = Nat + +Change : Type +Change = List (Maybe (Arg, SizeChange)) + +public export +Path : Type +Path = List (FC, Name) + +export +record ArgChange where + constructor MkArgChange + change : Change + path : Path + +-- ignore path +Eq ArgChange where + (==) a1 a2 = a1.change == a2.change + +Ord ArgChange where + compare a1 a2 = compare a1.change a2.change + +Show ArgChange where + show a = show a.change ++ " @" ++ show a.path + +-- sc-graphs to be added +export +WorkList : Type +WorkList = SortedSet (Name, Name, ArgChange) + +-- transitively-closed (modulo work list) set of sc-graphs +export +SCSet : Type +SCSet = NameMap (NameMap (SortedSet ArgChange)) + +export +initSCSet : SCSet +initSCSet = empty + +lookupMap : Name -> NameMap (NameMap v) -> NameMap v +lookupMap n m = fromMaybe empty (lookup n m) + +lookupSet : Ord v => Name -> NameMap (SortedSet v) -> SortedSet v +lookupSet n m = fromMaybe empty (lookup n m) + +lookupGraphs : Name -> Name -> SCSet -> SortedSet ArgChange +lookupGraphs f g = lookupSet g . lookupMap f + +selectDom : Name -> SCSet -> SCSet +selectDom f s = insert f (lookupMap f s) empty + +selectCod : Name -> SCSet -> SCSet +selectCod g s = map (\m => insert g (lookupSet g m) empty) s + +foldl : (acc -> Name -> Name -> ArgChange -> acc) -> acc -> SCSet -> acc +foldl f_acc acc + = foldlNames (\acc, f => + foldlNames (\acc, g => + foldl (\acc, c => f_acc acc f g c) acc) + acc) + acc + +insertGraph : Name -> Name -> ArgChange -> SCSet -> SCSet +insertGraph f g ch s + = let s_f = lookupMap f s in + let s_fg = lookupSet g s_f in + insert f (insert g (insert ch s_fg) s_f) s + +composeChange : Change -> Change -> Change +composeChange c1 c2 + = map ((=<<) (\(i, r) => updateArg r <$> getArg i c1)) c2 + where + getArg : forall a . Nat -> List (Maybe a) -> Maybe a + getArg _ [] = Nothing + getArg Z (x :: xs) = x + getArg (S k) (x :: xs) = getArg k xs + + updateArg : SizeChange -> (Arg, SizeChange) -> (Arg, SizeChange) + updateArg c arg@(_, Unknown) = arg + updateArg Unknown (i, _) = (i, Unknown) + updateArg c (i, Same) = (i, c) + updateArg c arg@(_, Smaller) = arg + +composeArgChange : ArgChange -> ArgChange -> ArgChange +composeArgChange a1 a2 + = MkArgChange + (composeChange a1.change a2.change) + (a1.path ++ a2.path) + +preCompose : Name -> ArgChange -> + SCSet -> + WorkList -> + Name -> Name -> ArgChange -> + WorkList +preCompose f ch1 s work _ h ch2 + = let ch = composeArgChange ch1 ch2 in + if contains ch (lookupGraphs f h s) then + work + else + insert (f, h, ch) work + +postCompose : Name -> ArgChange -> + SCSet -> + WorkList -> + Name -> Name -> ArgChange -> + WorkList +postCompose h ch2 s work f _ ch1 + = let ch = composeArgChange ch1 ch2 in + if contains ch (lookupGraphs f h s) then + work + else + insert (f, h, ch) work + +mutual + addGraph : {auto c : Ref Ctxt Defs} -> + Name -> Name -> ArgChange -> + WorkList -> + SCSet -> + SCSet + addGraph f g ch work s_in + = let s = insertGraph f g ch s_in + after = selectDom g s + work_pre = foldl (preCompose f ch s) work after + before = selectCod f s + work_post = foldl (postCompose g ch s) work_pre before in + transitiveClosure work_post s + + export + transitiveClosure : {auto c : Ref Ctxt Defs} -> + WorkList -> + SCSet -> + SCSet + transitiveClosure work s + = case pop work of + Nothing => s + Just ((f, g, ch), work) => + addGraph f g ch work s + +-- find (potential) chain of calls to given function (inclusive) +export +prefixPath : NameMap (FC, Name) -> Name -> Path +prefixPath pred g = go g [] + where + go : Name -> Path -> Path + go g path + = let Just (l, f) = lookup g pred + | Nothing => path in + if f == g then -- we've reached the entry point! + path + else + go f ((l, g) :: path) + +findLoops : {auto c : Ref Ctxt Defs} -> SCSet -> Core (NameMap (Maybe Path)) +findLoops s + = do let loops = filterEndos (\a => composeChange a.change a.change == a.change) s + log "totality.termination.calc" 7 $ "Loops: " ++ show loops + let terms = map (foldMap (\a => checkDesc a.change a.path)) loops + pure terms + where + filterEndos : (ArgChange -> Bool) -> SCSet -> NameMap (List ArgChange) + filterEndos p = mapWithKey (\f, m => filter p (Data.SortedSet.toList (lookupSet f m))) + + checkDesc : Change -> Path -> Maybe Path + checkDesc [] p = Just p + checkDesc (Just (_, Smaller) :: _) p = Nothing + checkDesc (_ :: xs) p = checkDesc xs p + +export +findNonTerminatingLoop : {auto c : Ref Ctxt Defs} -> SCSet -> Core (Maybe (Name, Path)) +findNonTerminatingLoop s + = do loops <- findLoops s + pure $ findNonTerminating loops + where + findNonTerminating : NameMap (Maybe Path) -> Maybe (Name, Path) + findNonTerminating = foldlNames (\acc, g, m => map (g,) m <+> acc) empty + +export +setPrefixTerminating : {auto c : Ref Ctxt Defs} -> + Path -> Name -> Core () +setPrefixTerminating [] g = pure () +setPrefixTerminating (_ :: []) g = pure () +setPrefixTerminating ((l, f) :: p) g + = do setTerminating l f (NotTerminating (BadPath p g)) + setPrefixTerminating p g + +addFunctions : {auto c : Ref Ctxt Defs} -> + Defs -> + List GlobalDef -> -- functions we're adding + NameMap (FC, Name) -> -- functions we've already seen (and their predecessor) + WorkList -> + Core (Either Terminating (WorkList, NameMap (FC, Name))) +addFunctions defs [] pred work + = pure $ Right (work, pred) +addFunctions defs (d1 :: ds) pred work + = do log "totality.termination.calc" 8 $ "Adding function: " ++ show d1.fullname + calls <- foldlC resolveCall [] d1.sizeChange + let Nothing = find isNonTerminating calls + | Just (d2, l, _) => do let g = d2.fullname + log "totality.termination.calc" 7 $ "Non-terminating function call: " ++ show g + let init = prefixPath pred d1.fullname ++ [(l, g)] + setPrefixTerminating init g + pure $ Left (NotTerminating (BadPath init g)) + let (ds, pred, work) = foldl addCall (ds, pred, work) (filter isUnchecked calls) + addFunctions defs ds pred work + where + resolveCall : List (GlobalDef, FC, (Name, Name, ArgChange)) -> + SCCall -> + Core (List (GlobalDef, FC, (Name, Name, ArgChange))) + resolveCall calls (MkSCCall g ch l) + = do Just d2 <- lookupCtxtExact g (gamma defs) + | Nothing => do log "totality.termination.calc" 7 $ "Not found: " ++ show g + pure calls + pure ((d2, l, (d1.fullname, d2.fullname, MkArgChange ch [(l, d2.fullname)])) :: calls) + + addCall : (List GlobalDef, NameMap (FC, Name), WorkList) -> + (GlobalDef, FC, (Name, Name, ArgChange)) -> + (List GlobalDef, NameMap (FC, Name), WorkList) + addCall (ds, pred, work_in) (d2, l, c) + = let work = insert c work_in in + case lookup d2.fullname pred of + Just _ => + (ds, pred, work) + Nothing => + (d2 :: ds, insert d2.fullname (l, d1.fullname) pred, work) + + isNonTerminating : (GlobalDef, _, _) -> Bool + isNonTerminating (d2, _, _) + = case d2.totality.isTerminating of + NotTerminating _ => True + _ => False + + isUnchecked : (GlobalDef, _, _) -> Bool + isUnchecked (d2, _, _) + = case d2.totality.isTerminating of + Unchecked => True + _ => False + +export +initWork : {auto c : Ref Ctxt Defs} -> + Defs -> + GlobalDef -> -- entry + Core (Either Terminating (WorkList, NameMap (FC, Name))) +initWork defs def = addFunctions defs [def] (insert def.fullname (def.location, def.fullname) empty) empty diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index 771f77267..eb43e9db4 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -13,6 +13,7 @@ import Core.LinearCheck import Core.Metadata import Core.Normalise import Core.Termination +import Core.Termination.CallGraph import Core.Transform import Core.Value import Core.UnifyState