1	import Base
2	import ../types/model.bend as T
3	
4	# Abstract outcomes of requesting the caller's clock. Sample has already passed
5	# the signed-64-bit millisecond validation. The other constructors distinguish
6	# provider exceptions from rejected samples. A host conversion proof must map
7	# real provider outcomes to these cases; it is not assumed here.
8	type ClockEvent is Data:
9	  Sample{milliseconds: T.Int64}
10	  InvalidSample{reason: String}
11	  ProviderException{reason: String}
12	
13	type Error is Data:
14	  Exhausted{}
15	  Invalid{reason: String}
16	  Thrown{reason: String}
17	
18	type Reply is Data:
19	  Accepted{milliseconds: T.Int64, remaining: List<&2, ClockEvent>}
20	  Rejected{error: Error, remaining: List<&2, ClockEvent>}
21	
22	# Each evaluation denotes exactly one request, including a failed request.
23	# Merely retaining a clock stream does not request or validate its next event.
24	def request(events: List<&2, ClockEvent>) -> Reply:
25	  match events:
26	    case Nil{}: Rejected{Exhausted{}, Nil{}}
27	    case Con{Sample{now}, tail}: Accepted{now, tail}
28	    case Con{InvalidSample{reason}, tail}: Rejected{Invalid{reason}, tail}
29	    case Con{ProviderException{reason}, tail}: Rejected{Thrown{reason}, tail}