0 | module Core.Termination
  1 |
  2 | import Core.Context.Log
  3 | import Core.Env
  4 | import Core.Normalise
  5 | import Core.Value
  6 |
  7 | import Core.Termination.CallGraph
  8 | import Core.Termination.Positivity
  9 | import Core.Termination.SizeChange
 10 |
 11 | import Libraries.Data.NameMap
 12 |
 13 | %default covering
 14 |
 15 | -- Check if all branches end up as constructor arguments, with no other
 16 | -- function application, and set 'AllGuarded' if so.
 17 | -- This is to check whether a function can be considered a constructor form
 18 | -- for the sake of termination checking (and might have other uses...)
 19 | export
 20 | checkIfGuarded : {auto c : Ref Ctxt Defs} ->
 21 |                  FC -> Name -> Core ()
 22 | checkIfGuarded fc n
 23 |     = do logC "totality.termination.guarded" 6 $ do pure $ "Check if Guarded: " ++ show !(toFullNames n)
 24 |          defs <- get Ctxt
 25 |          Just (PMDef _ _ _ _ pats) <- lookupDefExact n (gamma defs)
 26 |               | _ => pure ()
 27 |          t <- allGuarded pats
 28 |          when t $ setFlag fc n AllGuarded
 29 |   where
 30 |     guardedNF : Defs -> Env Term vars -> NF vars -> Core Bool
 31 |     guardedNF defs env (NDCon _ _ _ _ args) = pure True
 32 |     guardedNF defs env (NApp _ (NRef _ n) args)
 33 |         = do Just gdef <- lookupCtxtExact n (gamma defs)
 34 |                   | Nothing => pure False
 35 |              pure (AllGuarded `elem` flags gdef)
 36 |     guardedNF defs env _ = pure False
 37 |
 38 |     checkNotFn : Defs -> Name -> Core Bool
 39 |     checkNotFn defs n
 40 |         = do Just gdef <- lookupCtxtExact n (gamma defs)
 41 |                   | Nothing => pure False
 42 |              case definition gdef of
 43 |                   DCon {} => pure True
 44 |                   _ => pure (multiplicity gdef == erased
 45 |                               || (AllGuarded `elem` flags gdef))
 46 |
 47 |     guarded : {vars : _} -> Env Term vars -> Term vars -> Core Bool
 48 |     guarded env tm
 49 |         = do defs <- get Ctxt
 50 |              empty <- clearDefs defs
 51 |              tmnf <- nf empty env tm
 52 |              if !(guardedNF defs env tmnf)
 53 |                 then do Just gdef <- lookupCtxtExact n (gamma defs)
 54 |                              | Nothing => pure False
 55 |                         allM (checkNotFn defs) (keys (refersTo gdef))
 56 |                 else pure False
 57 |
 58 |     allGuarded : List (vs ** (Env Term vs, Term vs, Term vs)) -> Core Bool
 59 |     allGuarded [] = pure True
 60 |     allGuarded ((_ ** (env, lhs, rhs)) :: ps)
 61 |         = if !(guarded env rhs)
 62 |              then allGuarded ps
 63 |              else pure False
 64 |
 65 | -- Check whether a function is terminating, and record in the context
 66 | export
 67 | checkTerminating : {auto c : Ref Ctxt Defs} ->
 68 |                    FC -> Name -> Core Terminating
 69 | checkTerminating loc n
 70 |     = do tot <- getTotality loc n
 71 |          logC "totality.termination" 6 $ do pure $ "Checking termination: " ++ show !(toFullNames n)
 72 |          case isTerminating tot of
 73 |               Unchecked =>
 74 |                  do tot' <- calcTerminating loc n
 75 |                     setTerminating loc n tot'
 76 |                     pure tot'
 77 |               t => pure t
 78 |
 79 | -- Check whether a data type satisfies the strict positivity condition, and
 80 | -- record in the context
 81 | export
 82 | checkPositive : {auto c : Ref Ctxt Defs} ->
 83 |                 FC -> Name -> Core Terminating
 84 | checkPositive loc n_in
 85 |     = do n <- toResolvedNames n_in
 86 |          tot <- getTotality loc n
 87 |          logC "totality.positivity" 6 $ do pure $ "Checking positivity: " ++ show !(toFullNames n)
 88 |          case isTerminating tot of
 89 |               Unchecked =>
 90 |                   do (tot', cons) <- calcPositive loc n
 91 |                      setTerminating loc n tot'
 92 |                      traverse_ (\c => setTerminating loc c tot') cons
 93 |                      pure tot'
 94 |               t => pure t
 95 |
 96 |
 97 | -- Check and record totality of the given name; positivity if it's a data
 98 | -- type, termination if it's a function
 99 | export
100 | checkTotal : {auto c : Ref Ctxt Defs} ->
101 |              FC -> Name -> Core Terminating
102 | checkTotal loc n_in
103 |     = do defs <- get Ctxt
104 |          let Just nidx = getNameID n_in (gamma defs)
105 |              | Nothing => undefinedName loc n_in
106 |          let n = Resolved nidx
107 |          tot <- getTotality loc n
108 |          logC "totality" 5 $ do pure $ "Checking totality: " ++ show !(toFullNames n)
109 |          defs <- get Ctxt
110 |          case isTerminating tot of
111 |               Unchecked => do
112 |                   mgdef <- lookupCtxtExact n (gamma defs)
113 |                   case definition <$> mgdef of
114 |                        Just (TCon {})
115 |                            => checkPositive loc n
116 |                        _ => do whenJust (refersToM =<< mgdef) $ \ refs =>
117 |                                  log "totality" 5 $ "  Mutually defined with:"
118 |                                                  ++ show !(traverse toFullNames (keys refs))
119 |                                checkTerminating loc n
120 |               t => pure t
121 |