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_composition.bend as Comp
6	type Owned<-S:Data,-C:Type,-R:Type,-E:Data,H: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>> is Type:
7	  Owned{name:String,plan:SP.Plan<S>,owners:H}
8	type Run<World:Type,Owner:Type,S:Data,Error:Data> is Type:
9	  Finished{world:World,owner:Owner,observations:List<&2,Sch.Observation>}
10	  Failed{world:World,owner:Owner,error:Error,observations:List<&2,Sch.Observation>}
11	  Refused{world:World,owner:Owner,observations:List<&2,Sch.Observation>}
12	  Missing{world:World,owner:Owner,requirements:List<&2,SP.Requirement<S>>}
13	# Conditions belong to typed leaves; only the canonical zero placeholder is
14	# accepted in the reused data-only plan. Arbitrary dispatcher slots are refused.
15	def canonical_steps(steps:List<&2,Sch.Step>) -> Bool:
16	  match steps:
17	    case []:True{}
18	    case Sch.System{_,slot} <> rest:Bool.and(U32.is_eq(slot,0),canonical_steps(rest))
19	    case _ <> rest:canonical_steps(rest)
20	def compose(~S:Data,~C:Type,~R:Type,~E:Data,~H: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>,name:String,plan:SP.Plan<S>,owners:H) -> Owned<S,C,R,E,H,Error,catalog,dispatch>:
21	  Owned{name,plan,owners}
22	def after(~S:Data,~C:Type,~R:Type,~E:Data,~H: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>,next:H -> W.World<S,C,R,E> -> List<&2,Sch.Observation> -> Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,Error,catalog,dispatch>,S,Error>,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<W.World<S,C,R,E>,Owned<S,C,R,E,H,Error,catalog,dispatch>,S,Error>:
23	  match result:
24	    case Comp.Completed{world,owner}:next(owner,world,List.append(&2,Sch.Observation,observations,[Sch.Ran{id}]))
25	    case Comp.Skipped{world,owner}:next(owner,world,List.append(&2,Sch.Observation,observations,[Sch.Skipped{id}]))
26	    case Comp.Failed{world,owner,error}:Failed{world,Owned{name,plan,owner},error,List.append(&2,Sch.Observation,observations,[Sch.Ran{id}])}
27	    case Comp.Refused{world,owner}:Refused{world,Owned{name,plan,owner},observations}
28	def execute(~S:Data,~C:Type,~R:Type,~E:Data,~H: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>,steps:List<&2,Sch.Step>,owners:H,world:W.World<S,C,R,E>,+name:String,+plan:SP.Plan<S>,+observations:List<&2,Sch.Observation>) -> Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,Error,catalog,dispatch>,S,Error>:
29	  match steps:
30	    case []:Finished{world,Owned{name,plan,owners},observations}
31	    case Sch.Phase{phase} <> rest:execute(~S,~C,~R,~E,~H,~Error,~catalog,~dispatch,rest,owners,world,name,plan,List.append(&2,Sch.Observation,observations,[Sch.Entered{phase}]))
32	    case Sch.Barrier{} <> rest:execute(~S,~C,~R,~E,~H,~Error,~catalog,~dispatch,rest,owners,W.barrier(~S,~C,~R,~E,world),name,plan,List.append(&2,Sch.Observation,observations,[Sch.Applied{}]))
33	    case Sch.System{+id,_} <> rest:after(~S,~C,~R,~E,~H,~Error,~catalog,~dispatch,h => w => logs => execute(~S,~C,~R,~E,~H,~Error,~catalog,~dispatch,rest,h,w,name,plan,logs),name,plan,id,observations,dispatch(owners,world,id))
34	def requirements(~S:Data,~C:Type,~R:Type,~E:Data,~H: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>,owners:H,world:W.World<S,C,R,E>,name:String,+plan:SP.Plan<S>,missing:List<&2,SP.Requirement<S>>) -> Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,Error,catalog,dispatch>,S,Error>:
35	  match missing:
36	    case []:execute(~S,~C,~R,~E,~H,~Error,~catalog,~dispatch,SP.flatten(~S,plan),owners,world,name,plan,[])
37	    case first <> rest:Missing{world,Owned{name,plan,owners},first <> rest}
38	def available(~S:Data,~C:Type,~R:Type,~E:Data,~H: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>,owners:H,name:String,+plan:SP.Plan<S>,result:W.World<S,C,R,E> & List<&2,SP.Requirement<S>>) -> Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,Error,catalog,dispatch>,S,Error>:
39	  match result:
40	    case (world,provided):requirements(~S,~C,~R,~E,~H,~Error,~catalog,~dispatch,owners,world,name,plan,SP.missing_requirements(~S,SP.unique(~S,SP.requirements(~S,plan)),provided))
41	def allowed(~S:Data,~C:Type,~R:Type,~E:Data,~H: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>,~provision:W.World<S,C,R,E> -> W.World<S,C,R,E> & List<&2,SP.Requirement<S>>,valid:Bool,owners:H,world:W.World<S,C,R,E>,name:String,plan:SP.Plan<S>) -> Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,Error,catalog,dispatch>,S,Error>:
42	  match valid:
43	    case False{}:Refused{world,Owned{name,plan,owners},[]}
44	    case True{}:available(~S,~C,~R,~E,~H,~Error,~catalog,~dispatch,owners,name,plan,provision(world))
45	def cataloged(~S:Data,~C:Type,~R:Type,~E:Data,~H: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>,~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>,observed:H & List<&2,Comp.Identity>) -> Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,Error,catalog,dispatch>,S,Error>:
46	  match world observed:
47	    case W.World{+ns,allocator,store,resource,events,pending,+regs,sid,clock}, (owners,+entries):allowed(~S,~C,~R,~E,~H,~Error,~catalog,~dispatch,~provision,Bool.and(Comp.identities_valid(ns,regs,entries,[]),Bool.and(canonical_steps(SP.flatten(~S,plan)),Sch.valid(SP.flatten(~S,plan),Comp.ids(entries),[]))),owners,W.World{ns,allocator,store,resource,events,pending,regs,sid,clock},name,plan)
48	def run(~S:Data,~C:Type,~R:Type,~E:Data,~H: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>,~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,Error,catalog,dispatch>,world:W.World<S,C,R,E>) -> Run<W.World<S,C,R,E>,Owned<S,C,R,E,H,Error,catalog,dispatch>,S,Error>:
49	  match owner:
50	    case Owned{name,plan,owners}:cataloged(~S,~C,~R,~E,~H,~Error,~catalog,~dispatch,~provision,world,name,plan,catalog(owners))