1	import Base
2	import ./ordinary_checked_condition.bend as Cond
3	import ./ordinary_checked_bindings.bend as B
4	import ./check.bend as K
5	import ./world.bend as W
6	import ./system.bend as Sys
7	import ./schedule.bend as Sch
8	import ./schedule_provision.bend as SP
9	# Same membership/duplicate/namespace, step and SP needs behavior as
10	# ordinary-condition-composition. Only selected Check errors differ in transport.
11	type Error<BodyError:Data> is Data:
12	  SystemError{error:BodyError}
13	  CheckError{error:K.Error}
14	  ConditionUnavailable{}
15	  ConditionRegistrationRejected{}
16	
17	type Attachment<S:Data,C:Type,R:Type,E:Data,H:Type,B:Type,-select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>> is Type:
18	  Attached{schedule:Sch.Schedule<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>>}
19	  AttachmentRejected{schedule:Sch.Schedule<S,C,R,E,H>,bindings:B.Bindings<W.World<S,C,R,E>,B,select>}
20	def attached(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,allowed:Bool,namespace:U32,name:String,+steps:List<&2,Sch.Step>,owners:H,bindings:B.Bindings<W.World<S,C,R,E>,B,select>,facts:List<&2,B.Description>) -> Attachment<S,C,R,E,H,B,select>:
21	  match allowed:
22	    case False{}:AttachmentRejected{Sch.Schedule{namespace,name,steps,owners},bindings}
23	    case True{}:Attached{Sch.Schedule{namespace,name,steps,(owners,bindings)}}
24	def attach(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,schedule:Sch.Schedule<S,C,R,E,H>,bindings:B.Bindings<W.World<S,C,R,E>,B,select>) -> Attachment<S,C,R,E,H,B,select>:
25	  match schedule bindings:
26	    case Sch.Schedule{namespace,name,+steps,owners} B.Bindings{state,+facts}:attached(~S,~C,~R,~E,~H,~B,~select,Bool.and(B.unique(facts,[]),B.targets(facts,steps)),namespace,name,steps,owners,B.Bindings{state,facts},facts)
27	
28	def body_outcome(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,bindings:B.Bindings<W.World<S,C,R,E>,B,select>,owners:H,outcome:Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>) -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & Sys.Outcome<W.World<S,C,R,E>,Error<BodyError>,Unit>:
29	  match outcome:
30	    case Sys.Succeeded{world,value}:((owners,bindings),Sys.Succeeded{world,value})
31	    case Sys.Failed{world,error}:((owners,bindings),Sys.Failed{world,SystemError{error}})
32	def body_returned(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,bindings:B.Bindings<W.World<S,C,R,E>,B,select>,returned:H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>) -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & Sys.Outcome<W.World<S,C,R,E>,Error<BodyError>,Unit>:
33	  match returned:
34	    case (owners,outcome):body_outcome(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,bindings,owners,outcome)
35	def body_dispatch(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,owners:H & B.Bindings<W.World<S,C,R,E>,B,select>,world:W.World<S,C,R,E>,id:U32) -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & Sys.Outcome<W.World<S,C,R,E>,Error<BodyError>,Unit>:
36	  match owners:
37	    case (gameplay,bindings):body_returned(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,bindings,dispatch(gameplay,world,id))
38	def guard_decision_with_barrier(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,~barrier:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & W.World<S,C,R,E>,next:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> List<&2,Sch.Observation> -> Sch.RunResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>,value:Bool,owners:H,bindings:B.Bindings<W.World<S,C,R,E>,B,select>,world:W.World<S,C,R,E>,+namespace:U32,+name:String,+all:List<&2,Sch.Step>,+observations:List<&2,Sch.Observation>,+id:U32) -> Sch.RunResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>:
39	  match value:
40	    case False{}:next((owners,bindings),world,List.append(&2,Sch.Observation,observations,[Sch.Skipped{id}]))
41	    case True{}:Sch.after_dispatch(~S,~C,~R,~E,~(H & B.Bindings<W.World<S,C,R,E>,B,select>),~Error<BodyError>,next,body_dispatch(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,(owners,bindings),world,id),namespace,name,all,observations,id)
42	def guard_returned_with_barrier(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,~barrier:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & W.World<S,C,R,E>,next:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> List<&2,Sch.Observation> -> Sch.RunResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>,facts:List<&2,B.Description>,owners:H,result:B.Selection<W.World<S,C,R,E>,B>,namespace:U32,name:String,all:List<&2,Sch.Step>,observations:List<&2,Sch.Observation>,id:U32) -> Sch.RunResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>:
43	  match result:
44	    case B.Selected{world,state,Done{value}}:guard_decision_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,next,value,owners,B.Bindings{state,facts},world,namespace,name,all,observations,id)
45	    case B.Unbound{world,state}:guard_decision_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,next,True{},owners,B.Bindings{state,facts},world,namespace,name,all,observations,id)
46	    case B.Selected{world,state,Fail{Cond.CheckError{error}}}:Sch.Failed{Sch.Schedule{namespace,name,all,(owners,B.Bindings{state,facts})},world,CheckError{error},observations}
47	    case B.Selected{world,state,Fail{Cond.NoValue{}}}:Sch.Failed{Sch.Schedule{namespace,name,all,(owners,B.Bindings{state,facts})},world,ConditionUnavailable{},observations}
48	    case B.Selected{world,state,Fail{Cond.InvalidRegistration{}}}:Sch.Failed{Sch.Schedule{namespace,name,all,(owners,B.Bindings{state,facts})},world,ConditionRegistrationRejected{},observations}
49	    case B.Selected{world,state,Fail{Cond.NoBinding{}}}:guard_decision_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,next,True{},owners,B.Bindings{state,facts},world,namespace,name,all,observations,id)
50	def guard_with_barrier(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,~barrier:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & W.World<S,C,R,E>,next:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> List<&2,Sch.Observation> -> Sch.RunResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>,owners:H & B.Bindings<W.World<S,C,R,E>,B,select>,world:W.World<S,C,R,E>,namespace:U32,name:String,all:List<&2,Sch.Step>,observations:List<&2,Sch.Observation>,+id:U32) -> Sch.RunResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>:
51	  match owners:
52	    case (gameplay,B.Bindings{state,facts}):guard_returned_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,next,facts,gameplay,select(state,world,id),namespace,name,all,observations,id)
53	def execute_with_barrier(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,~barrier:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & W.World<S,C,R,E>,steps:List<&2,Sch.Step>,owners:H & B.Bindings<W.World<S,C,R,E>,B,select>,world:W.World<S,C,R,E>,+namespace:U32,+name:String,+all:List<&2,Sch.Step>,observations:List<&2,Sch.Observation>) -> Sch.RunResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>:
54	  match steps:
55	    case []:Sch.Finished{Sch.Schedule{namespace,name,all,owners},world,observations}
56	    case Sch.Phase{phase} <> rest:execute_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,rest,owners,world,namespace,name,all,List.append(&2,Sch.Observation,observations,[Sch.Entered{phase}]))
57	    case Sch.Barrier{} <> rest:Sch.after_skip(~S,~C,~R,~E,~(H & B.Bindings<W.World<S,C,R,E>,B,select>),~Error<BodyError>,h => w => obs => execute_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,rest,h,w,namespace,name,all,obs),barrier(owners,world),List.append(&2,Sch.Observation,observations,[Sch.Applied{}]))
58	    case Sch.System{id,_} <> rest:guard_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,h => w => obs => execute_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,rest,h,w,namespace,name,all,obs),owners,world,namespace,name,all,observations,id)
59	def run_checked_with_barrier(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,~barrier:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & W.World<S,C,R,E>,allowed:Bool,schedule:Sch.Schedule<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>>,world:W.World<S,C,R,E>) -> Sch.RunResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>:
60	  match allowed schedule:
61	    case False{} schedule:Sch.Rejected{schedule,world}
62	    case True{} Sch.Schedule{+namespace,+name,+steps,owners}:execute_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,steps,owners,world,namespace,name,steps,[])
63	def run_namespaced_with_barrier(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,~barrier:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & W.World<S,C,R,E>,schedule:Sch.Schedule<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>>,observed:W.World<S,C,R,E> & U32) -> Sch.RunResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>:
64	  match schedule observed:
65	    case Sch.Schedule{+namespace,name,+steps,(gameplay,B.Bindings{state,+facts})}, (world,actual):run_checked_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,Bool.and(U32.is_eq(namespace,actual),Bool.and(B.unique(facts,[]),B.targets(facts,steps))),Sch.Schedule{namespace,name,steps,(gameplay,B.Bindings{state,facts})},world)
66	def run_schedule_with_barrier(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,~barrier:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & W.World<S,C,R,E>,schedule:Sch.Schedule<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>>,world:W.World<S,C,R,E>) -> Sch.RunResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>:
67	  run_namespaced_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,schedule,W.namespace(~S,~C,~R,~E,world))
68	
69	def provision_checked_with_barrier(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,~barrier:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & W.World<S,C,R,E>,missing:List<&2,SP.Requirement<S>>,schedule:Sch.Schedule<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>>,world:W.World<S,C,R,E>,needs:List<&2,SP.Requirement<S>>) -> SP.ProvisionResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>:
70	  match missing:
71	    case first <> rest:SP.Missing{SP.Provisioned{schedule,needs},world,first <> rest}
72	    case []:SP.Executed{run_schedule_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,schedule,world),needs}
73	def provision_available_with_barrier(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,~barrier:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & W.World<S,C,R,E>,observed:W.World<S,C,R,E> & List<&2,SP.Requirement<S>>,schedule:Sch.Schedule<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>>,+needs:List<&2,SP.Requirement<S>>) -> SP.ProvisionResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>:
74	  match observed:
75	    case (world,available):provision_checked_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,SP.missing_requirements(~S,needs,available),schedule,world,needs)
76	def run_provisioned_with_barrier(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,~barrier:(H & B.Bindings<W.World<S,C,R,E>,B,select>) -> W.World<S,C,R,E> -> (H & B.Bindings<W.World<S,C,R,E>,B,select>) & W.World<S,C,R,E>,~provision:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,SP.Requirement<S>>,schedule:SP.Provisioned<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>>,world:W.World<S,C,R,E>) -> SP.ProvisionResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>:
77	  match schedule:
78	    case SP.Provisioned{schedule,needs}:provision_available_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~barrier,provision(world),schedule,needs)
79	
80	def run_schedule(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,schedule:Sch.Schedule<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>>,world:W.World<S,C,R,E>) -> Sch.RunResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>:
81	  run_schedule_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~Sch.default_barrier(~S,~C,~R,~E,~(H & B.Bindings<W.World<S,C,R,E>,B,select>)),schedule,world)
82	
83	def run_provisioned(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~select:B -> W.World<S,C,R,E> -> U32 -> B.Selection<W.World<S,C,R,E>,B>,~BodyError:Data,~dispatch:H -> W.World<S,C,R,E> -> U32 -> H & Sys.Outcome<W.World<S,C,R,E>,BodyError,Unit>,~provision:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,SP.Requirement<S>>,schedule:SP.Provisioned<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>>,world:W.World<S,C,R,E>) -> SP.ProvisionResult<S,C,R,E,H & B.Bindings<W.World<S,C,R,E>,B,select>,Error<BodyError>>:
84	  run_provisioned_with_barrier(~S,~C,~R,~E,~H,~B,~select,~BodyError,~dispatch,~Sch.default_barrier(~S,~C,~R,~E,~(H & B.Bindings<W.World<S,C,R,E>,B,select>)),~provision,schedule,world)