From c3082d8465f42345842aa36d3d7993d6b2f76712 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Thu, 26 Nov 2020 10:50:43 +0000 Subject: [PATCH] [ re #524 ] Debug + positivity check --- src/Core/Core.idr | 4 ++++ src/Core/Termination.idr | 39 ++++++++++++++++++++------------------ src/TTImp/ProcessDecls.idr | 16 ++++++++++++---- 3 files changed, 37 insertions(+), 22 deletions(-) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index d6eee7edf..28a7510ee 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -438,6 +438,10 @@ export %inline (<$>) : (a -> b) -> Core a -> Core b (<$>) f (MkCore a) = MkCore (map (map f) a) +export %inline +ignore : Core a -> Core () +ignore = map (\ _ => ()) + -- Monad (specialised) export %inline (>>=) : Core a -> (a -> Core b) -> Core b diff --git a/src/Core/Termination.idr b/src/Core/Termination.idr index 1d3e8b1fa..a2f422f19 100644 --- a/src/Core/Termination.idr +++ b/src/Core/Termination.idr @@ -25,8 +25,10 @@ totRefs defs (n :: ns) | Nothing => pure rest case isTerminating (totality d) of IsTerminating => pure rest - Unchecked => pure rest - bad => case rest of + 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]) @@ -43,7 +45,7 @@ export checkIfGuarded : {auto c : Ref Ctxt Defs} -> FC -> Name -> Core () checkIfGuarded fc n - = do log "totality.termination.guarded" 6 $ "Check if Guarded: " ++ show n + = do log "totality.termination.guarded" 6 $ "Check if Guarded: " ++ show !(toFullNames n) defs <- get Ctxt Just (PMDef _ _ _ _ pats) <- lookupDefExact n (gamma defs) | _ => pure () @@ -363,7 +365,7 @@ mutual = do Just gdef <- lookupCtxtExact fn_in (gamma defs) | Nothing => throw (UndefinedName fc fn_in) let fn = fullname gdef - log "totality.termination.sizechange" 10 $ "Looking under " ++ show fn + log "totality.termination.sizechange" 10 $ "Looking under " ++ show !(toFullNames fn) aSmaller <- resolved (gamma defs) (NS builtinNS (UN "assert_smaller")) cond [(fn == NS builtinNS (UN "assert_total"), pure []), (caseFn fn, @@ -410,7 +412,7 @@ 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 n + = do log "totality.termination.sizechange" 5 $ "Calculating Size Change: " ++ show !(toFullNames n) defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) | Nothing => throw (UndefinedName loc n) @@ -447,15 +449,15 @@ checkSC : {auto a : Ref APos Arg} -> List (Name, List (Maybe Arg)) -> -- calls we've seen so far Core Terminating checkSC defs f args path - = do log "totality.termination.sizechange" 7 $ "Checking Size Change Graph: " ++ show f + = do log "totality.termination.sizechange" 7 $ "Checking Size Change Graph: " ++ show !(toFullNames f) let pos = (f, map (map Builtin.fst) args) if pos `elem` path - then do log "totality.termination.sizechange.inPath" 8 $ "Checking arguments: " ++ show f + then do log "totality.termination.sizechange.inPath" 8 $ "Checking arguments: " ++ show !(toFullNames f) toFullNames $ checkDesc (mapMaybe (map Builtin.snd) args) path else case !(lookupCtxtExact f (gamma defs)) of - Nothing => do log "totality.termination.sizechange.isTerminating" 8 $ "Size Change Graph is Terminating for: " ++ show f + Nothing => do log "totality.termination.sizechange.isTerminating" 8 $ "Size Change Graph is Terminating for: " ++ show !(toFullNames f) pure IsTerminating - Just def => do log "totality.termination.sizechange.needsChecking" 8 $ "Size Change Graph needs traversing: " ++ show f + Just def => do log "totality.termination.sizechange.needsChecking" 8 $ "Size Change Graph needs traversing: " ++ show !(toFullNames f) continue (sizeChange def) (pos :: path) where -- Look for something descending in the list of size changes @@ -492,7 +494,7 @@ checkSC defs f args path let Unchecked = isTerminating (totality gdef) | IsTerminating => pure IsTerminating | _ => pure (NotTerminating (BadCall [fnCall sc])) - log "totality.termination.sizechange.checkCall" 8 $ "CheckCall Size Change Graph: " ++ show (fnCall sc) + log "totality.termination.sizechange.checkCall" 8 $ "CheckCall Size Change Graph: " ++ show !(toFullNames (fnCall sc)) term <- checkSC defs (fnCall sc) (mkArgs (fnArgs sc)) path if not inpath then case term of @@ -501,12 +503,12 @@ checkSC defs f args path -- was mutually recursive, so start again with new -- arguments (that is, where we'd start if the -- function was the top level thing we were checking) - do log "totality.termination.sizechange.checkCall.inPathNot.restart" 9 $ "ReChecking Size Change Graph: " ++ show (fnCall sc) + do log "totality.termination.sizechange.checkCall.inPathNot.restart" 9 $ "ReChecking Size Change Graph: " ++ show !(toFullNames (fnCall sc)) args' <- initArgs (length (fnArgs sc)) checkSC defs (fnCall sc) args' path - t => do log "totality.termination.sizechange.checkCall.inPathNot.return" 9 $ "Have result: " ++ show (fnCall sc) + t => do log "totality.termination.sizechange.checkCall.inPathNot.return" 9 $ "Have result: " ++ show !(toFullNames (fnCall sc)) pure t - else do log "totality.termination.sizechange.checkCall.inPath" 9 $ "Have Result: " ++ show (fnCall sc) + else do log "totality.termination.sizechange.checkCall.inPath" 9 $ "Have Result: " ++ show !(toFullNames (fnCall sc)) pure term getWorst : Terminating -> List Terminating -> Terminating @@ -524,7 +526,7 @@ calcTerminating : {auto c : Ref Ctxt Defs} -> FC -> Name -> Core Terminating calcTerminating loc n = do defs <- get Ctxt - log "totality.termination.calc" 7 $ "Calculating termination: " ++ show n + log "totality.termination.calc" 7 $ "Calculating termination: " ++ show !(toFullNames n) case !(lookupCtxtExact n (gamma defs)) of Nothing => throw (UndefinedName loc n) Just def => @@ -558,7 +560,7 @@ checkTerminating : {auto c : Ref Ctxt Defs} -> FC -> Name -> Core Terminating checkTerminating loc n = do tot <- getTotality loc n - log "totality.termination" 6 $ "Checking termination: " ++ show n + log "totality.termination" 6 $ "Checking termination: " ++ show !(toFullNames n) case isTerminating tot of Unchecked => do tot' <- calcTerminating loc n @@ -651,7 +653,7 @@ 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 n + 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 @@ -670,7 +672,7 @@ checkPositive : {auto c : Ref Ctxt Defs} -> checkPositive loc n_in = do n <- toResolvedNames n_in tot <- getTotality loc n - log "totality.positivity" 6 $ "Checking positivity: " ++ show n + log "totality.positivity" 6 $ "Checking positivity: " ++ show !(toFullNames n) case isTerminating tot of Unchecked => do (tot', cons) <- calcPositive loc n @@ -679,6 +681,7 @@ checkPositive loc n_in pure tot' t => pure t + -- Check and record totality of the given name; positivity if it's a data -- type, termination if it's a function export @@ -690,7 +693,7 @@ checkTotal loc n_in | Nothing => throw (UndefinedName loc n_in) let n = Resolved nidx tot <- getTotality loc n - log "totality" 5 $ "Checking totality: " ++ show n + log "totality" 5 $ "Checking totality: " ++ show !(toFullNames n) defs <- get Ctxt case isTerminating tot of Unchecked => diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr index 6569e3a13..810dc7c0c 100644 --- a/src/TTImp/ProcessDecls.idr +++ b/src/TTImp/ProcessDecls.idr @@ -72,14 +72,22 @@ checkTotalityOK n = do defs <- get Ctxt Just gdef <- lookupCtxtExact n (gamma defs) | Nothing => pure Nothing + let fc = location gdef + + -- #524: need to check positivity even if we're not in a total context + -- because a definition coming later may need to know it is positive + case definition gdef of + (TCon _ _ _ _ _ _ _ _) => ignore $ checkPositive fc n + _ => pure () + + -- Once that is done, we build up errors if necessary let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef)) let tot = totality gdef - let fc = location gdef log "totality" 3 $ show n ++ " must be: " ++ show treq case treq of - PartialOK => pure Nothing - CoveringOnly => checkCovering fc (isCovering tot) - Total => checkTotality fc + PartialOK => pure Nothing + CoveringOnly => checkCovering fc (isCovering tot) + Total => checkTotality fc where checkCovering : FC -> Covering -> Core (Maybe Error) checkCovering fc IsCovering = pure Nothing