1	import Base
2	import ./world.bend as W
3	import ./schedule.bend as Sch
4	import ./schedule_provision.bend as SP
5	import ./captured_schedule.bend as Run
6	import ./captured_schedule_composition.bend as Comp
7	import ./ordinary_condition_composition.bend as Cond
8	# Registered condition identities are preflight-only, never executable step IDs.
9	def leaf_identities(leaves:List<&2,Cond.LeafDescription>) -> List<&2,Comp.Identity>:
10	  match leaves:
11	    case []:[]
12	    case Cond.StateChanged{ns,id,name,access} <> rest:Comp.Identity{ns,id,name,access} <> leaf_identities(rest)
13	    case _ <> rest:leaf_identities(rest)
14	def condition_identities(facts:List<&2,Cond.BindingDescription>) -> List<&2,Comp.Identity>:
15	  match facts:
16	    case []:[]
17	    case Cond.BindingDescription{_,Cond.Description{_,_,leaves}} <> rest:List.append(&2,Comp.Identity,leaf_identities(leaves),condition_identities(rest))
18	type Owned<-S:Data,-C:Type,-R:Type,-E:Data,H:Type,B:Type,-Error:Data,-catalog:H -> H & List<&2,Comp.Identity>,-dispatch:H -> W.World<S,C,R,E> -> U32 -> Comp.Outcome<W.World<S,C,R,E>,H,Error>,-select:B -> W.World<S,C,R,E> -> U32 -> Cond.Evaluation<W.World<S,C,R,E>,B>> is Type:
19	  Owned{name:String,plan:SP.Plan<S>,owners:H,conditions:Cond.Bindings<W.World<S,C,R,E>,B,select>}
20	def attach(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~Error:Data,~catalog:H -> H & List<&2,Comp.Identity>,~dispatch:H -> W.World<S,C,R,E> -> U32 -> Comp.Outcome<W.World<S,C,R,E>,H,Error>,~select:B -> W.World<S,C,R,E> -> U32 -> Cond.Evaluation<W.World<S,C,R,E>,B>,schedule:Run.Owned<S,C,R,E,H,Error,catalog,dispatch>,conditions:Cond.Bindings<W.World<S,C,R,E>,B,select>) -> Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>:
21	  match schedule:
22	    case Run.Owned{name,plan,owners}:Owned{name,plan,owners,conditions}
23	def body_done(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~Error:Data,~catalog:H -> H & List<&2,Comp.Identity>,~dispatch:H -> W.World<S,C,R,E> -> U32 -> Comp.Outcome<W.World<S,C,R,E>,H,Error>,~select:B -> W.World<S,C,R,E> -> U32 -> Cond.Evaluation<W.World<S,C,R,E>,B>,next:H -> Cond.Bindings<W.World<S,C,R,E>,B,select> -> W.World<S,C,R,E> -> List<&2,Sch.Observation> -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>,conditions:Cond.Bindings<W.World<S,C,R,E>,B,select>,name:String,plan:SP.Plan<S>,+id:U32,+observations:List<&2,Sch.Observation>,result:Comp.Outcome<W.World<S,C,R,E>,H,Error>) -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>:
24	  match result:
25	    case Comp.Completed{world,owner}:next(owner,conditions,world,List.append(&2,Sch.Observation,observations,[Sch.Ran{id}]))
26	    case Comp.Skipped{world,owner}:next(owner,conditions,world,List.append(&2,Sch.Observation,observations,[Sch.Skipped{id}]))
27	    case Comp.Failed{world,owner,error}:Run.Failed{world,Owned{name,plan,owner,conditions},Cond.SystemError{error},List.append(&2,Sch.Observation,observations,[Sch.Ran{id}])}
28	    case Comp.Refused{world,owner}:Run.Refused{world,Owned{name,plan,owner,conditions},observations}
29	def decision(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~Error:Data,~catalog:H -> H & List<&2,Comp.Identity>,~dispatch:H -> W.World<S,C,R,E> -> U32 -> Comp.Outcome<W.World<S,C,R,E>,H,Error>,~select:B -> W.World<S,C,R,E> -> U32 -> Cond.Evaluation<W.World<S,C,R,E>,B>,next:H -> Cond.Bindings<W.World<S,C,R,E>,B,select> -> W.World<S,C,R,E> -> List<&2,Sch.Observation> -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>,allowed:Bool,owners:H,conditions:Cond.Bindings<W.World<S,C,R,E>,B,select>,world:W.World<S,C,R,E>,name:String,plan:SP.Plan<S>,+id:U32,+observations:List<&2,Sch.Observation>) -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>:
30	  match allowed:
31	    case False{}:next(owners,conditions,world,List.append(&2,Sch.Observation,observations,[Sch.Skipped{id}]))
32	    case True{}:body_done(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,next,conditions,name,plan,id,observations,dispatch(owners,world,id))
33	def condition_done(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~Error:Data,~catalog:H -> H & List<&2,Comp.Identity>,~dispatch:H -> W.World<S,C,R,E> -> U32 -> Comp.Outcome<W.World<S,C,R,E>,H,Error>,~select:B -> W.World<S,C,R,E> -> U32 -> Cond.Evaluation<W.World<S,C,R,E>,B>,next:H -> Cond.Bindings<W.World<S,C,R,E>,B,select> -> W.World<S,C,R,E> -> List<&2,Sch.Observation> -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>,owners:H,facts:List<&2,Cond.BindingDescription>,name:String,plan:SP.Plan<S>,id:U32,observations:List<&2,Sch.Observation>,result:Cond.Evaluation<W.World<S,C,R,E>,B>) -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>:
34	  match result:
35	    case Cond.Value{world,state,value}:decision(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,next,value,owners,Cond.Bindings{state,facts},world,name,plan,id,observations)
36	    case Cond.NoBinding{world,state}:decision(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,next,True{},owners,Cond.Bindings{state,facts},world,name,plan,id,observations)
37	    case Cond.NoValue{world,state}:Run.Failed{world,Owned{name,plan,owners,Cond.Bindings{state,facts}},Cond.ConditionUnavailable{},observations}
38	    case Cond.InvalidRegistration{world,state}:Run.Failed{world,Owned{name,plan,owners,Cond.Bindings{state,facts}},Cond.ConditionRegistrationRejected{},observations}
39	def condition_run(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~Error:Data,~catalog:H -> H & List<&2,Comp.Identity>,~dispatch:H -> W.World<S,C,R,E> -> U32 -> Comp.Outcome<W.World<S,C,R,E>,H,Error>,~select:B -> W.World<S,C,R,E> -> U32 -> Cond.Evaluation<W.World<S,C,R,E>,B>,next:H -> Cond.Bindings<W.World<S,C,R,E>,B,select> -> W.World<S,C,R,E> -> List<&2,Sch.Observation> -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>,owners:H,conditions:Cond.Bindings<W.World<S,C,R,E>,B,select>,world:W.World<S,C,R,E>,name:String,plan:SP.Plan<S>,+id:U32,observations:List<&2,Sch.Observation>) -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>:
40	  match conditions:
41	    case Cond.Bindings{state,facts}:condition_done(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,next,owners,facts,name,plan,id,observations,select(state,world,id))
42	def execute(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~Error:Data,~catalog:H -> H & List<&2,Comp.Identity>,~dispatch:H -> W.World<S,C,R,E> -> U32 -> Comp.Outcome<W.World<S,C,R,E>,H,Error>,~select:B -> W.World<S,C,R,E> -> U32 -> Cond.Evaluation<W.World<S,C,R,E>,B>,steps:List<&2,Sch.Step>,owners:H,conditions:Cond.Bindings<W.World<S,C,R,E>,B,select>,world:W.World<S,C,R,E>,+name:String,+plan:SP.Plan<S>,+observations:List<&2,Sch.Observation>) -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>:
43	  match steps:
44	    case []:Run.Finished{world,Owned{name,plan,owners,conditions},observations}
45	    case Sch.Phase{phase} <> rest:execute(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,rest,owners,conditions,world,name,plan,List.append(&2,Sch.Observation,observations,[Sch.Entered{phase}]))
46	    case Sch.Barrier{} <> rest:execute(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,rest,owners,conditions,W.barrier(~S,~C,~R,~E,world),name,plan,List.append(&2,Sch.Observation,observations,[Sch.Applied{}]))
47	    case Sch.System{+id,_} <> rest:condition_run(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,h => c => w => logs => execute(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,rest,h,c,w,name,plan,logs),owners,conditions,world,name,plan,id,observations)
48	def requirements(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~Error:Data,~catalog:H -> H & List<&2,Comp.Identity>,~dispatch:H -> W.World<S,C,R,E> -> U32 -> Comp.Outcome<W.World<S,C,R,E>,H,Error>,~select:B -> W.World<S,C,R,E> -> U32 -> Cond.Evaluation<W.World<S,C,R,E>,B>,owners:H,conditions:Cond.Bindings<W.World<S,C,R,E>,B,select>,world:W.World<S,C,R,E>,name:String,+plan:SP.Plan<S>,missing:List<&2,SP.Requirement<S>>) -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>:
49	  match missing:
50	    case []:execute(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,SP.flatten(~S,plan),owners,conditions,world,name,plan,[])
51	    case first <> rest:Run.Missing{world,Owned{name,plan,owners,conditions},first <> rest}
52	def available(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~Error:Data,~catalog:H -> H & List<&2,Comp.Identity>,~dispatch:H -> W.World<S,C,R,E> -> U32 -> Comp.Outcome<W.World<S,C,R,E>,H,Error>,~select:B -> W.World<S,C,R,E> -> U32 -> Cond.Evaluation<W.World<S,C,R,E>,B>,owners:H,conditions:Cond.Bindings<W.World<S,C,R,E>,B,select>,name:String,+plan:SP.Plan<S>,result:W.World<S,C,R,E> & List<&2,SP.Requirement<S>>) -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>:
53	  match result:
54	    case (world,provided):requirements(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,owners,conditions,world,name,plan,SP.missing_requirements(~S,SP.unique(~S,SP.requirements(~S,plan)),provided))
55	def allowed(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~Error:Data,~catalog:H -> H & List<&2,Comp.Identity>,~dispatch:H -> W.World<S,C,R,E> -> U32 -> Comp.Outcome<W.World<S,C,R,E>,H,Error>,~select:B -> W.World<S,C,R,E> -> U32 -> Cond.Evaluation<W.World<S,C,R,E>,B>,~provision:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,SP.Requirement<S>>,valid:Bool,owners:H,conditions:Cond.Bindings<W.World<S,C,R,E>,B,select>,world:W.World<S,C,R,E>,name:String,plan:SP.Plan<S>) -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>:
56	  match valid:
57	    case False{}:Run.Refused{world,Owned{name,plan,owners,conditions},[]}
58	    case True{}:available(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,owners,conditions,name,plan,provision(world))
59	def cataloged(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~Error:Data,~catalog:H -> H & List<&2,Comp.Identity>,~dispatch:H -> W.World<S,C,R,E> -> U32 -> Comp.Outcome<W.World<S,C,R,E>,H,Error>,~select:B -> W.World<S,C,R,E> -> U32 -> Cond.Evaluation<W.World<S,C,R,E>,B>,~provision:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,SP.Requirement<S>>,world:W.World<S,C,R,E>,name:String,+plan:SP.Plan<S>,conditions:Cond.Bindings<W.World<S,C,R,E>,B,select>,observed:H & List<&2,Comp.Identity>) -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>:
60	  match world conditions observed:
61	    case W.World{+ns,allocator,store,resource,events,pending,+regs,sid,clock}, Cond.Bindings{state,+facts}, (owners,+entries):allowed(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,~provision,Bool.and(Comp.identities_valid(ns,regs,entries,[]),Bool.and(Comp.identities_valid(ns,regs,condition_identities(facts),[]),Bool.and(Cond.unique_bindings(facts,[]),Bool.and(Cond.binding_targets(facts,SP.flatten(~S,plan)),Bool.and(Run.canonical_steps(SP.flatten(~S,plan)),Sch.valid(SP.flatten(~S,plan),Comp.ids(entries),[])))))),owners,Cond.Bindings{state,facts},W.World{ns,allocator,store,resource,events,pending,regs,sid,clock},name,plan)
62	def run(~S:Data,~C:Type,~R:Type,~E:Data,~H:Type,~B:Type,~Error:Data,~catalog:H -> H & List<&2,Comp.Identity>,~dispatch:H -> W.World<S,C,R,E> -> U32 -> Comp.Outcome<W.World<S,C,R,E>,H,Error>,~select:B -> W.World<S,C,R,E> -> U32 -> Cond.Evaluation<W.World<S,C,R,E>,B>,~provision:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,SP.Requirement<S>>,owner:Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,world:W.World<S,C,R,E>) -> Run.Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,B,Error,catalog,dispatch,select>,S,Cond.Error<Error>>:
63	  match owner:
64	    case Owned{name,plan,owners,conditions}:cataloged(~S,~C,~R,~E,~H,~B,~Error,~catalog,~dispatch,~select,~provision,world,name,plan,conditions,catalog(owners))