mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 19:13:02 +03:00
[ re #524 ] Debug + positivity check
This commit is contained in:
Guillaume ALLAIS
G. Allais
parent
910711afe9
commit
c3082d8465
@ -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
|
||||
|
||||
@ -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 =>
|
||||
|
||||
@ -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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user