1	# ez/timer: the clock ez/clock's budget is kept by. `date -d` works out the
2	# deadline at the start and `test -gt` does the one comparison at the end,
3	# both run through snap's foreign effect. This half lives apart from ez/clock
4	# because bend 2.0.32 fails a proof whose imports reach foreign code, so a law
5	# may import ez/clock but never this.
6	import Base
7	import 0xead4c7939c9eaca8d47da53b4496b731/main.bend as R
8	import ../share/env.bend as Env
9	import ./clock.bend as Clock
10	
11	# how many seconds a whole run may take. Five minutes is what the gate is held
12	# to; a tree that honestly needs longer says so in EZ_DEADLINE, and "0" turns
13	# the budget off for someone bisecting with the cache cold.
14	def seconds() -> IO(String):
15	  Env.var("EZ_DEADLINE", "300")
16	
17	# the second the run must be finished by, worked out once at the start so that
18	# nothing later has to add anything up
19	def by(+secs: String) -> IO(String):
20	  do IO<String>:
21	    +out : String <- R.exec(["date", "-d", "+" ++ secs ++ " seconds", "+%s"])
22	    return String.trim(R.text(out))
23	
24	# the deadline, or "" when there is none
25	def start.go(keep: Bool, +secs: String) -> IO(String):
26	  match keep:
27	    case False{}:
28	      IO.pure(String, "")
29	    case True{}:
30	      by(secs)
31	
32	# the deadline, or "" when there is none
33	def start(+secs: String) -> IO(String):
34	  start.go(Clock.on(secs), secs)
35	
36	# whether the deadline has gone by
37	def over.now(+deadline: String) -> IO(Bool):
38	  do IO<Bool>:
39	    +now : String <- R.exec(["date", "+%s"])
40	    +cmp : String <- R.exec(["test", String.trim(R.text(now)), "-gt", deadline])
41	    return R.ok(cmp)
42	
43	# whether the run has outstayed its budget, which a run with no budget never
44	# has
45	def over.go(none: Bool, +deadline: String) -> IO(Bool):
46	  match none:
47	    case True{}:
48	      IO.pure(Bool, False{})
49	    case False{}:
50	      over.now(deadline)
51	
52	# whether the run has outstayed its budget, which a run with no budget never
53	# has
54	def over(+deadline: String) -> IO(Bool):
55	  over.go(String.is_empty(deadline), deadline)