mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 02:31:50 +03:00
[ refactor ] split up Core.Termination
This commit is contained in:
Guillaume Allais
G. Allais
parent
6edbfc59a5
commit
c6b96080c2
@ -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,
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
354
src/Core/Termination/CallGraph.idr
Normal file
354
src/Core/Termination/CallGraph.idr
Normal file
@ -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)
|
||||
198
src/Core/Termination/Positivity.idr
Normal file
198
src/Core/Termination/Positivity.idr
Normal file
@ -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
|
||||
256
src/Core/Termination/SizeChange.idr
Normal file
256
src/Core/Termination/SizeChange.idr
Normal file
@ -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
|
||||
@ -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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user