1	import Base
2	import ./ordinary_machine_initialization.bend as Init
3	import ./ordinary_machine_declaration.bend as OD
4	import ./machine.bend as M
5	import ./world.bend as W
6	import ./system.bend as Sys
7	
8	# Each ordinary condition is an actual registered system plus its own revision.
9	# The revision is separate from the Registry's real World-clock cursor.
10	def present(~S:Data,~K:Data,~V:Data,slot:M.Slot<S,K,V>) -> Bool:
11	  match slot:
12	    case M.Missing{}:False{}
13	    case _:True{}
14	def revision_taken(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,pair:R & Init.State<S,K,V>) -> R & (Nat & Bool):
15	  match pair:
16	    case (resource,Init.State{+slot,stream,+revision}):(put(resource,Init.State{slot,stream,revision}),(revision,present(~S,~K,~V,slot)))
17	def observed(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,prior:Nat,pair:W.World<S,C,R,E> & (Nat & Bool)) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Nat & Bool>:
18	  match pair:
19	    case (world,(+current,present)):Sys.Succeeded{world,(current,Bool.and(present,Nat.is_lt(prior,current)))}
20	def runner(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,world:W.World<S,C,R,E>,prior:Nat) -> Sys.Outcome<W.World<S,C,R,E>,Unit,Nat & Bool>:
21	  observed(~S,~K,~V,~R,~take,~put,~C,~E,prior,W.observe_resource(~S,~C,~R,~E,~(Nat & Bool),~(resource => revision_taken(~S,~K,~V,~R,~take,~put,~C,~E,take(resource))),world))
22	type Instance<S:Data,K:Data,V:Data,C:Type,R:Type,E:Data,-take:R -> R & Init.State<S,K,V>,-put:R -> Init.State<S,K,V> -> R> is Type:
23	  Instance{registry:Sys.Registry<S,C,R,E,Nat,Unit,Nat & Bool,runner(~S,~K,~V,~R,~take,~put,~C,~E)>,lastRevision:Nat}
24	type Definition<S:Data,K:Data,V:Data,C:Type,R:Type,E:Data,-take:R -> R & Init.State<S,K,V>,-put:R -> Init.State<S,K,V> -> R> is Type:
25	  Defined{world:W.World<S,C,R,E>,instance:Instance<S,K,V,C,R,E,take,put>}
26	  DefinitionRejected{world:W.World<S,C,R,E>}
27	def registered(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,result:Sys.RegistrationResult<S,C,R,E,Nat,Unit,Nat & Bool,runner(~S,~K,~V,~R,~take,~put,~C,~E)>) -> Definition<S,K,V,C,R,E,take,put>:
28	  match result:
29	    case Sys.Registered{world,registry}:Defined{world,Instance{registry,0n}}
30	    case Sys.RegistrationFailed{world}:DefinitionRejected{world}
31	def define(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,~declaration:OD.Declaration<S,K,V,R,Init.take_slot(~S,~K,~V,~R,~take,~put)>,world:W.World<S,C,R,E>,name:String) -> Definition<S,K,V,C,R,E,take,put>:
32	  registered(~S,~K,~V,~R,~take,~put,~C,~E,Sys.register(~S,~C,~R,~E,~Nat,~Unit,~(Nat & Bool),~runner(~S,~K,~V,~R,~take,~put,~C,~E),world,name,["machine." ++ OD.name(~S,~K,~V,~R,~Init.take_slot(~S,~K,~V,~R,~take,~put),declaration) ++ ".changed"]))
33	type Observed<S:Data,K:Data,V:Data,C:Type,R:Type,E:Data,-take:R -> R & Init.State<S,K,V>,-put:R -> Init.State<S,K,V> -> R> is Type:
34	  Observed{world:W.World<S,C,R,E>,instance:Instance<S,K,V,C,R,E,take,put>,value:Maybe<&2,Bool>}
35	  RegistrationRejected{world:W.World<S,C,R,E>,instance:Instance<S,K,V,C,R,E,take,put>}
36	def completed(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,prior:Nat,result:Sys.RunResult<S,C,R,E,Nat,Unit,Nat & Bool,runner(~S,~K,~V,~R,~take,~put,~C,~E)>) -> Observed<S,K,V,C,R,E,take,put>:
37	  match result:
38	    case Sys.Completed{registry,Sys.Succeeded{world,(revision,value)}}:Observed{world,Instance{registry,revision},Some{value}}
39	    case Sys.Completed{registry,Sys.Failed{world,_}}:Observed{world,Instance{registry,prior},None{}}
40	    case Sys.RegistrationRejected{registry,world,_}:RegistrationRejected{world,Instance{registry,prior}}
41	def run(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,instance:Instance<S,K,V,C,R,E,take,put>,world:W.World<S,C,R,E>) -> Observed<S,K,V,C,R,E,take,put>:
42	  match instance:
43	    case Instance{registry,+prior}:completed(~S,~K,~V,~R,~take,~put,~C,~E,prior,Sys.run(~S,~C,~R,~E,~Nat,~Unit,~(Nat & Bool),~runner(~S,~K,~V,~R,~take,~put,~C,~E),registry,world,prior))
44	def run_if(~S:Data,~K:Data,~V:Data,~R:Type,~take:R -> R & Init.State<S,K,V>,~put:R -> Init.State<S,K,V> -> R,~C:Type,~E:Data,enabled:Bool,instance:Instance<S,K,V,C,R,E,take,put>,world:W.World<S,C,R,E>) -> Observed<S,K,V,C,R,E,take,put>:
45	  match enabled:
46	    case False{}:Observed{world,instance,None{}}
47	    case True{}:run(~S,~K,~V,~R,~take,~put,~C,~E,instance,world)