module Core.Termination import Core.CaseTreeimport Core.Contextimport Core.Envimport Core.Normaliseimport Core.TTimport Core.Value import Control.Monad.State import Data.NameMapimport Data.List import Debug.Trace %default covering -- Check that the names a function refers to are terminatingtotRefs : {auto c : Ref Ctxt Defs} ->          Defs -> List Name -> Core TerminatingtotRefs defs [] = pure IsTerminatingtotRefs 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 => pure rest              bad => 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 TerminatingtotRefsIn defs ty = totRefs defs (keys (getRefs (Resolved (-1)) ty)) -- Equal for the purposes of size change means, ignoring as patterns, all-- non-metavariable positions are equalscEq : Term vars -> Term vars -> BoolscEq (Local _ _ idx _) (Local _ _ idx' _) = idx == idx'scEq (Ref _ _ n) (Ref _ _ n') = n == n'scEq (Meta _ _ i args) _ = TruescEq _ (Meta _ _ i args) = TruescEq (Bind _ _ b sc) (Bind _ _ b' sc') = False -- not checkablescEq (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 _ _) = TruescEq (TType _) (TType _) = TruescEq _ _ = False data Guardedness = Toplevel | Unguarded | Guarded | InDelay Show Guardedness where  show Toplevel = "Toplevel"  show Unguarded = "Unguarded"  show Guarded = "Guarded"  show InDelay = "InDelay" mutual  findSC : {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 tm      = case (g, getFnArgs tm) 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)             (Toplevel, Ref fc (DataCon _ _) cn, args) =>                 do scs <- traverse (findSC defs env Guarded pats) args                    pure (concat scs)             (_, Ref fc Func fn, args) =>                 do Just ty <- lookupTyExact fn (gamma defs)                         | Nothing =>                              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)   -- 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      = if s == t           then True           else 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 s tm        -- If we hit a pattern that is equal to a thing we've asserted_smaller,        -- the argument must be smaller      = if assertedSmaller big tm           then True           else 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 : 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      = case !(lookupDefExact n (gamma defs)) of             Just (PMDef _ _ _ _ pdefs)                => pure $ Just (map matchArgs pdefs)             _ => pure Nothing    where      lookupTm : Term vs -> List (Term vs, Term vs') -> Maybe (Term vs')      lookupTm tm [] = Nothing      lookupTm tm ((As _ _ p tm', v) :: tms)          = if tm == p               then Just v               else lookupTm tm ((tm', v) :: tms)      lookupTm tm ((tm', v) :: tms)          = if tm == tm'               then Just v               else lookupTm tm tms       updateRHS : 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 False          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 i) = Erased fc i          urhs (TType fc) = TType fc       updatePat : 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 : {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 Just gdef <- lookupCtxtExact fn_in (gamma defs)                | Nothing => throw (UndefinedName fc fn_in)           let fn = fullname gdef           log 10 $ "Looking under " ++ show fn           aSmaller <- resolved (gamma defs) (NS ["Builtin"] (UN "assert_smaller"))           cond [(fn == NS ["Builtin"] (UN "assert_total"), pure []),              (caseFn fn,                  do mps <- getCasePats defs fn pats args                     case mps of                          Nothing => pure []                          Just ps => do scs <- traverse (findInCase defs g) ps                                        pure (concat scs))]              (do scs <- traverse (findSC defs env g pats) args                  pure ([MkSCCall fn                           (expandToArity arity                                (map (mkChange defs aSmaller pats) args))]                           ++ 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 10 (do ps <- traverse toFullNames (map snd pats)                      pure ("Looking in case args " ++ show ps))          logTermNF 10 "        =" env tm          rhs <- normaliseOpts tcOnly defs env tm          findSC defs env g pats rhs -- 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 varsdelazy 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 tdelazy 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 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 (concat sc)getSC defs _ = pure [] exportcalculateSizeChange : {auto c : Ref Ctxt Defs} ->                      FC -> Name -> Core (List SCCall)calculateSizeChange loc n    = do defs <- get Ctxt         Just def <- lookupCtxtExact n (gamma defs)              | Nothing => throw (UndefinedName loc n)         getSC defs (definition def) Arg : TypeArg = Int data APos : Type where firstArg : ArgfirstArg = 0 nextArg : Arg -> ArgnextArg x = x + 1 initArgs : {auto a : Ref APos Arg} ->           Nat -> Core (List (Maybe (Arg, SizeChange)))initArgs Z = pure []initArgs (S k)    = do arg <- get APos         put APos (nextArg arg)         args' <- initArgs k         pure (Just (arg, Same) :: args') -- Traverse the size change graph. When we reach a point we've seen before,-- at least one of the arguments must have got smaller, otherwise it's-- potentially non-terminating-- TODO: If we encounter a name where we already know its termination status,-- use that rather than continuing to traverse the graph!checkSC : {auto a : Ref APos Arg} ->          {auto c : Ref Ctxt Defs} ->          Defs ->          Name -> -- function we're checking          List (Maybe (Arg, SizeChange)) -> -- functions arguments and change          List (Name, List (Maybe Arg)) -> -- calls we've seen so far          Core TerminatingcheckSC defs f args path   = let pos = (f, map (map fst) args) in         if pos `elem` path            then toFullNames $ checkDesc (mapMaybe (map snd) args) path            else case !(lookupCtxtExact f (gamma defs)) of                      Nothing => pure IsTerminating                      Just def => continue (sizeChange def) (pos :: path)  where    -- Look for something descending in the list of size changes    checkDesc : List SizeChange -> List (Name, List (Maybe Arg)) -> Terminating    checkDesc [] path = NotTerminating (RecPath (reverse (map fst path)))    checkDesc (Smaller :: _) _ = IsTerminating    checkDesc (_ :: xs) path = checkDesc xs path     getPos : List a -> Nat -> Maybe a    getPos [] _ = Nothing    getPos (x :: xs) Z = Just x    getPos (x :: xs) (S k) = getPos xs k     updateArg : SizeChange -> Maybe (Arg, SizeChange) -> Maybe (Arg, SizeChange)    updateArg c Nothing = Nothing    updateArg c arg@(Just (i, Unknown)) = arg    updateArg Unknown (Just (i, _)) = Just (i, Unknown)    updateArg c (Just (i, Same)) = Just (i, c)    updateArg c arg = arg     mkArgs : List (Maybe (Nat, SizeChange)) -> List (Maybe (Arg, SizeChange))    mkArgs [] = []    mkArgs (Nothing :: xs) = Nothing :: mkArgs xs    mkArgs (Just (pos, c) :: xs)        = case getPos args pos of               Nothing => Nothing :: mkArgs xs               Just arg => updateArg c arg :: mkArgs xs     checkCall : List (Name, List (Maybe Arg)) -> SCCall -> Core Terminating    checkCall path sc        = do let inpath = fnCall sc `elem` map fst path             term <- checkSC defs (fnCall sc) (mkArgs (fnArgs sc)) path             if not inpath                then case term of                       NotTerminating (RecPath _) =>                          -- might have lost information while assuming this                          -- 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 args' <- initArgs (length (fnArgs sc))                             checkSC defs (fnCall sc) args' path                       t => pure t                else pure term     getWorst : Terminating -> List Terminating -> Terminating    getWorst term [] = term    getWorst term (IsTerminating :: xs) = getWorst term xs    getWorst term (Unchecked :: xs) = getWorst Unchecked xs    getWorst term (bad :: xs) = bad     continue : List SCCall -> List (Name, List (Maybe Arg)) -> Core Terminating    continue scs path        = do allTerm <- traverse (checkCall path) scs             pure (getWorst IsTerminating allTerm) calcTerminating : {auto c : Ref Ctxt Defs} ->                  FC -> Name -> Core TerminatingcalcTerminating loc n    = do defs <- get Ctxt         case !(lookupCtxtExact n (gamma defs)) of              Nothing => throw (UndefinedName loc n)              Just def =>                case !(totRefs defs (nub !(addCases defs (keys (refersTo def))))) of                     IsTerminating =>                        do let ty = type def                           a <- newRef APos firstArg                           args <- initArgs !(getArity defs [] ty)                           checkSC defs n args []                     bad => pure bad  where    addCases' : Defs -> NameMap () -> List Name -> Core (List Name)    addCases' defs all [] = pure (keys all)    addCases' defs all (n :: ns)        = case lookup n all of             Just _ => addCases' defs all ns             Nothing =>               if caseFn !(getFullName n)                  then case !(lookupCtxtExact n (gamma defs)) of                            Just def => addCases' defs (insert n () all)                                                  (keys (refersTo def) ++ ns)                            Nothing => addCases' defs (insert n () all) ns                  else addCases' defs (insert n () all) ns     addCases : Defs -> List Name -> Core (List Name)    addCases defs ns = addCases' defs empty ns -- Check whether a function is terminating, and record in the contextexportcheckTerminating : {auto c : Ref Ctxt Defs} ->                   FC -> Name -> Core TerminatingcheckTerminating loc n    = do tot <- getTotality loc n         case isTerminating tot of              Unchecked =>                 do tot' <- calcTerminating loc n                    setTerminating loc n tot'                    pure tot'              t => pure t nameIn : Defs -> List Name -> NF [] -> Core BoolnameIn defs tyns (NBind fc x b sc)    = if !(nameIn defs tyns (binderType b))         then pure True         else do sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))                 nameIn defs tyns sc'nameIn defs tyns (NApp _ _ args)    = anyM (nameIn defs tyns)           !(traverse (evalClosure defs) args)nameIn defs tyns (NTCon _ n _ _ args)    = if n `elem` tyns         then pure True         else do args' <- traverse (evalClosure defs) args                 anyM (nameIn defs tyns) args'nameIn defs tyns (NDCon _ n _ _ args)    = anyM (nameIn defs tyns)           !(traverse (evalClosure defs) args)nameIn defs tyns _ = pure False -- Check an argument type doesn't contain a negative occurrence of any of-- the given type namesposArg : Defs -> List Name -> NF [] -> Core Terminating-- a tyn can only appear in the parameter positions of-- tc; report positivity failure if it appears anywhere elseposArg defs tyns (NTCon _ tc _ _ args)    = let testargs : List (Closure [])             = case !(lookupDefExact tc (gamma defs)) of                    Just (TCon _ _ params _ _ _ _ _) =>                         dropParams 0 params args                    _ => args in          if !(anyM (nameIn defs tyns)                  !(traverse (evalClosure defs) testargs))             then pure (NotTerminating NotStrictlyPositive)

Lines 1–500 of 594. Load more