0 | module Core.Termination.SizeChange

  2 | import Core.Context.Log

  4 | import Core.Termination.References

  6 | import Libraries.Data.NameMap

  8 | import Libraries.Data.SparseMatrix

 10 | import Data.List1

 11 | import Data.SortedSet

 13 | %default covering

 27 | Arg : Type

 28 | Arg = Nat

 35 | Change : {- f g -} Type

 36 | Change = Matrix SizeChange

 44 | public export

 45 | CallSeq : {- f g -} Type

 46 | CallSeq = List (FC, Name)

 52 | record Graph {- f g -} where

 53 |   constructor MkGraph

 54 |   change : Change {- f g -}

 55 |   seq : CallSeq {- f g -}

 58 | WorkList : Type

 59 | WorkList = SortedSet (Name, Name, Graph)

 63 | SCSet : Type

 64 | SCSet = NameMap {- \ f => -}

 65 |       $ NameMap {- \ g => -}

 66 |       $ SortedSet $ Graph {- f g -}

 72 | Eq Graph where

 73 |   (==) a1 a2 = a1.change == a2.change

 75 | Ord Graph where

 76 |   compare a1 a2 = compare a1.change a2.change

 78 | Show Graph where

 79 |   show a = show a.change ++ "\n    via call seq: " ++ show a.seq ++ "\n"

 85 | initSCSet : SCSet

 86 | initSCSet = empty

 88 | lookupMap : Name -> NameMap (NameMap v) -> NameMap v

 89 | lookupMap n m = fromMaybe empty (lookup n m)

 91 | lookupSet : Ord v => Name -> NameMap (SortedSet v) -> SortedSet v

 92 | lookupSet n m = fromMaybe empty (lookup n m)

 94 | lookupGraphs : Name -> Name -> SCSet -> SortedSet Graph

 95 | lookupGraphs f g = lookupSet g . lookupMap f

 98 | selectDom : Name -> SCSet -> SCSet

 99 | selectDom f s = insert f (lookupMap f s) empty

102 | selectCod : Name -> SCSet -> SCSet

103 | selectCod g s = map (\m => insert g (lookupSet g m) empty) s

105 | foldl : (acc -> Name -> Name -> Graph -> acc) -> acc -> SCSet -> acc

106 | foldl f_acc acc

107 |     = foldlNames (\acc, f =>

108 |         foldlNames (\acc, g =>

109 |           foldl (\acc, c => f_acc acc f g c) acc)

110 |           acc)

111 |         acc

113 | insertGraph : (f, g : Name) -> Graph {- f g -} -> SCSet -> SCSet

114 | insertGraph f g ch s

115 |   = let s_f = lookupMap f s in

116 |     let s_fg = lookupSet g s_f in

117 |     insert f (insert g (insert ch s_fg) s_f) s

124 | composeChange : Change {- f g -} -> Change {- g h -} -> Change {- f h -}

126 |     -- We use the SizeChange monoid: Unknown is a 0, Same is a neutral

127 |     = mult

131 | composeGraph : Graph {- f g -} -> Graph {- g h -} -> Graph {- f h -}

132 | composeGraph a1 a2

133 |     = MkGraph

134 |         (composeChange a1.change a2.change)

135 |         (a1.seq ++ a2.seq)

138 | preCompose : (f : Name) -> Graph {- f g -} -> -- /!\ g bound later

139 |              SCSet ->

140 |              WorkList ->

141 |              (g : Name) -> (h : Name) -> Graph {- g h -} ->

142 |              WorkList

143 | preCompose f ch1 s work _ h ch2

144 |    = let ch : Graph {- f h -} = composeGraph ch1 ch2 in

145 |      if contains ch (lookupGraphs f h s) then

146 |        work

147 |      else

148 |        insert (f, h, ch) work

151 | postCompose : (h : Name) -> Graph {- g h -} -> -- /!\ g bound later

152 |               SCSet ->

153 |               WorkList ->

154 |               (f : Name) -> (g : Name) -> Graph {- f g -} ->

155 |               WorkList

156 | postCompose h ch2 s work f _ ch1

157 |    = let ch : Graph {- f h -} = composeGraph ch1 ch2 in

158 |      if contains ch (lookupGraphs f h s) then

159 |        work

160 |      else

161 |        insert (f, h, ch) work

164 |   addGraph : (f, g : Name) -> Graph {- f g -} ->

165 |              WorkList ->

166 |              SCSet ->

167 |              SCSet

168 |   addGraph f g ch work s_in

169 |       = let s = insertGraph f g ch s_in

170 |             -- Now that (ch : Graph f g) has been added, we need to update

171 |             -- the graph with the paths it has extended i.e.

173 |             -- the ones start in g

174 |             after = selectDom g s

175 |             work_pre = foldl (preCompose f ch s) work after

177 |             -- and the ones ending in f

178 |             before = selectCod f s

179 |             work_post = foldl (postCompose g ch s) work_pre before in

181 |         -- And then we need to close over all of these new paths too

182 |         transitiveClosure work_post s

184 |   transitiveClosure : WorkList ->

185 |                       SCSet ->

186 |                       SCSet

187 |   transitiveClosure work s

188 |       = case pop work of

189 |              Nothing => s

190 |              Just ((f, g, ch), work) =>

191 |                addGraph f g ch work s

194 | prefixCallSeq : NameMap (FC, Name) -> (g : Name) -> {- Exists \ f => -} CallSeq {- f g -}

195 | prefixCallSeq pred g = go g []

196 |   where

197 |     go : Name -> CallSeq -> CallSeq

198 |     go g seq

199 |         = let Just (l, f) = lookup g pred

200 |              | Nothing => seq in

201 |           if f == g then -- we've reached the entry point!

202 |             seq

203 |           else

204 |             go f ((l, g) :: seq)

208 | checkNonDesc : (a : Graph) -> Maybe Graph

209 | checkNonDesc a = if any selfDecArc a.change then Nothing else Just a

210 |   where

211 |     selfDecArc : (Nat, Vector1 SizeChange) -> Bool

212 |     selfDecArc (i, xs) = lookupOrd i xs == Just Smaller

215 | findLoops : SCSet ->

216 |             NameMap {- $ \ f => -} (Maybe (Graph {- f f -} ))

217 | findLoops s

218 |     = -- An `SCSet` is non-terminating iff it contains a size graph that is

219 |       -- idempotent, i.e. stable under self-composition,

220 |       let loops = filterEndos (\a => composeChange a.change a.change == a.change) s in

221 |       -- and has no self-decreasing arcs.

222 |       map (foldMap checkNonDesc) loops

223 |     where

224 |       filterEndos : (Graph -> Bool) -> SCSet -> NameMap (List Graph)

225 |       filterEndos p = mapWithKey (\f, m => filter p (Prelude.toList (lookupSet f m)))

227 | findNonTerminatingLoop : SCSet -> Maybe (Name, Graph)

228 | findNonTerminatingLoop s = findNonTerminating (findLoops s)

229 |     where

230 |       -- select first non-terminating loop

231 |       -- TODO: find smallest

232 |       findNonTerminating : NameMap (Maybe Graph) -> Maybe (Name, Graph)

233 |       findNonTerminating = foldlNames (\acc, g, m => map (g,) m <+> acc) empty

236 | setPrefixTerminating : {auto c : Ref Ctxt Defs} ->

237 |                        CallSeq -> Name -> Core ()

238 | setPrefixTerminating [] g = pure ()

239 | setPrefixTerminating (_ :: []) g = pure ()

240 | setPrefixTerminating ((l, f) :: p) g

241 |     = do setTerminating l f (NotTerminating (BadPath p g))

242 |          setPrefixTerminating p g

244 | addFunctions : {auto c : Ref Ctxt Defs} ->

245 |               Defs ->

246 |               List GlobalDef -> -- functions we're adding

247 |               NameMap (FC, Name) -> -- functions we've already seen (and their predecessor)

248 |               WorkList ->

249 |               Core (Either Terminating (WorkList, NameMap (FC, Name)))

250 | addFunctions defs [] pred work

251 |     = pure $ Right (work, pred)

252 | addFunctions defs (d1 :: ds) pred work

253 |     = do calls <- foldlC resolveCall [] d1.sizeChange

254 |          let Nothing = find isNonTerminating calls

255 |             | Just (d2, l, _) =>

256 |               do let g = d2.fullname

257 |                  let init = prefixCallSeq pred d1.fullname ++ [(l, g)]

258 |                  setPrefixTerminating init g

259 |                  pure $ Left (NotTerminating (BadPath init g))

260 |          let (ds, pred, work) = foldl addCall (ds, pred, work) (filter isUnchecked calls)

261 |          addFunctions defs ds pred work

262 |   where

263 |     resolveCall : List (GlobalDef, FC, (Name, Name, Graph)) ->

264 |                   SCCall ->

265 |                   Core (List (GlobalDef, FC, (Name, Name, Graph)))

266 |     resolveCall calls (MkSCCall g ch l)

267 |         = do Just d2 <- lookupCtxtExact g (gamma defs)

268 |                 | Nothing => do logC "totality.termination.calc" 7 $ do pure "Not found: \{show g}"

269 |                                 pure calls

270 |              pure ((d2, l, (d1.fullname, d2.fullname, MkGraph ch [(l, d2.fullname)])) :: calls)

272 |     addCall : (List GlobalDef, NameMap (FC, Name), WorkList) ->

273 |                   (GlobalDef, FC, (Name, Name, Graph)) ->

274 |                   (List GlobalDef, NameMap (FC, Name), WorkList)

275 |     addCall (ds, pred, work_in) (d2, l, c)

276 |         = let work = insert c work_in in

277 |           case lookup d2.fullname pred of

278 |                Just _ =>

279 |                  (ds, pred, work)

280 |                Nothing =>

281 |                  (d2 :: ds, insert d2.fullname (l, d1.fullname) pred, work)

283 |     isNonTerminating : (GlobalDef, _, _) -> Bool

284 |     isNonTerminating (d2, _, _)

285 |         = case d2.totality.isTerminating of

286 |                NotTerminating _ => True

287 |                _ => False

289 |     isUnchecked : (GlobalDef, _, _) -> Bool

290 |     isUnchecked (d2, _, _)

291 |         = case d2.totality.isTerminating of

292 |                Unchecked => True

293 |                _ => False

295 | initWork : {auto c : Ref Ctxt Defs} ->

296 |            Defs ->

297 |            GlobalDef -> -- entry

298 |            Core (Either Terminating (WorkList, NameMap (FC, Name)))

299 | initWork defs def = addFunctions defs [def] (insert def.fullname (def.location, def.fullname) empty) empty

302 | calcTerminating : {auto c : Ref Ctxt Defs} ->

303 |                   FC -> Name -> Core Terminating

304 | calcTerminating loc n

305 |     = do defs <- get Ctxt

306 |          logC "totality.termination.calc" 7 $ do pure $ "Calculating termination: " ++ show !(toFullNames n)

307 |          Just def <- lookupCtxtExact n (gamma defs)

308 |            | Nothing => undefinedName loc n

309 |          IsTerminating <- totRefs defs (nub !(addCases defs (keys (refersTo def))))

310 |            | bad => pure bad

311 |          Right (work, pred) <- initWork defs def

312 |            | Left bad => pure bad

313 |          let s = transitiveClosure work initSCSet

314 |          let Nothing = findNonTerminatingLoop s

315 |            | Just (g, loop) =>

316 |                ifThenElse (def.fullname == g)

317 |                  (pure $ NotTerminating (RecPath loop.seq))

318 |                  (do setTerminating EmptyFC g (NotTerminating (RecPath loop.seq))

319 |                      let init = prefixCallSeq pred g

320 |                      setPrefixTerminating init g

321 |                      pure $ NotTerminating (BadPath init g))

322 |          pure IsTerminating

323 |   where

324 |     addCases' : Defs -> NameMap () -> List Name -> Core (List Name)

325 |     addCases' defs all [] = pure (keys all)

326 |     addCases' defs all (n :: ns)

327 |         = case lookup n all of

328 |              Just _ => addCases' defs all ns

329 |              Nothing =>

330 |                if caseFn !(getFullName n)

331 |                   then case !(lookupCtxtExact n (gamma defs)) of

332 |                             Just def => addCases' defs (insert n () all)

333 |                                                   (keys (refersTo def) ++ ns)

334 |                             Nothing => addCases' defs (insert n () all) ns

335 |                   else addCases' defs (insert n () all) ns

337 |     addCases : Defs -> List Name -> Core (List Name)

338 |     addCases defs ns = addCases' defs empty ns