def walk.spec

bolt@1.27.0.0 · src/rules/imports.bend:105

import Base

105# a worklist walk; each read file enters todo once, and a start that was
106# not read imports nothing, so fuel as many as the files never runs out
107# (src/rules/LAWS.bend unsafe_shut). The spec `walk` is proven against
108# (imp.walk), and what the laws' proofs reason over
109def walk.spec(
110  fuel: Nat,
111  todo: List<&2, String>,
112  +seen: List<&2, String>,
113  +es: List<&2, Edge>,
114  +read: List<&2, String>
115) -> List<&2, String>:
116  match fuel todo:
117    case 0n t:
118      seen
119    case 1n+f Nil{}:
120      seen
121    case 1n+f Con{p, rest}:
122      +found = fresh.spec(deps.spec(es, p), seen, read)
123      walk.spec(f, List.append(&2, String, found, rest), List.append(&2, String, List.reverse(&2, String, found), seen),
124        es, read)