1	import Base
2	import ./world.bend as W
3	import ./schedule.bend as Sch
4	import ./schedule_provision.bend as SP
5	# Closed ordinary blueprint. Affine callable fields are freshly projected from
6	# the same closed declaration index; no captured owner or registered guard state.
7	# Closed named condition blueprint indexed by its World-threading predicate.
8	# Contains no captured affine guard owner or registered reader state. Predicate
9	# is trusted setup; its returned World survives regardless of Bool result.
10	type Declaration<-S:Data,-C:Type,-R:Type,-E:Data,-predicate:W.World<S,C,R,E> -> W.World<S,C,R,E> & Bool> is Data:Declaration{name:String}
11	# Owned condition-plan builder/evaluator plus ordered condition names.
12	# Ordinary constructors derive slots and descriptions from the same program.
13	# Raw construction remains trusted; this is not a registered stateful guard.
14	type Program<-S:Data,-C:Type,-R:Type,-E:Data,-Ids:Data> is Type:
15	  Program{width:Nat,build:Ids -> SP.Plan<S>,names:List<&2,String>,evaluate:W.World<S,C,R,E> -> U32 -> W.World<S,C,R,E> & Bool}
16	# Materialized condition program: width, operational plan and ordered names.
17	# Metadata is detached; it does not grant runtime registration authority.
18	type Entries<S:Data> is Data:Entries{width:Nat,plan:SP.Plan<S>,names:List<&2,String>}
19	# Name a closed predicate for ordinary condition routing and descriptions.
20	# Does not evaluate it, register a system or allocate a reader/capture owner.
21	def named(~S:Data,~C:Type,~R:Type,~E:Data,~predicate:W.World<S,C,R,E> -> W.World<S,C,R,E> & Bool,name:String) -> Declaration<S,C,R,E,predicate>:Declaration{name}
22	# Return the condition's authored name, without evaluating its predicate.
23	def leaf_name(~S:Data,~C:Type,~R:Type,~E:Data,~predicate:W.World<S,C,R,E> -> W.World<S,C,R,E> & Bool,leaf:Declaration<S,C,R,E,predicate>) -> String:
24	  match leaf:
25	    case Declaration{name}:name
26	# Build one system placement and its condition slot from the same leaf.
27	# identify maps authored Ids to a registration ID; requirements are explicit
28	# plan metadata. Does not invoke predicate or system body during construction.
29	def system(~S:Data,~C:Type,~R:Type,~E:Data,~Ids:Data,~predicate:W.World<S,C,R,E> -> W.World<S,C,R,E> & Bool,~identify:Ids -> U32,requirements:List<&2,SP.Requirement<S>>,leaf:Declaration<S,C,R,E,predicate>) -> Program<S,C,R,E,Ids>:
30	  Program{1n,ids => SP.Entry{Sch.System{identify(ids),0},requirements},[leaf_name(~S,~C,~R,~E,~predicate,leaf)],world => slot => predicate(world)}
31	# Build a named phase placement with requirements and no condition slot.
32	# Phase metadata does not evaluate a guard or execute registered systems.
33	def phase(~S:Data,~C:Type,~R:Type,~E:Data,~Ids:Data,name:String,requirements:List<&2,SP.Requirement<S>>) -> Program<S,C,R,E,Ids>:
34	  Program{0n,ids => SP.Entry{Sch.Phase{name},requirements},[],world => slot => (world,False{})}
35	# Build an explicit structural barrier placement with requirements and no
36	# condition slot. Constructing the program does not apply pending commands.
37	def barrier(~S:Data,~C:Type,~R:Type,~E:Data,~Ids:Data,requirements:List<&2,SP.Requirement<S>>) -> Program<S,C,R,E,Ids>:
38	  Program{0n,ids => SP.Entry{Sch.Barrier{},requirements},[],world => slot => (world,False{})}
39	def shifted(~S:Data,plan:SP.Plan<S>,+offset:U32) -> SP.Plan<S>:
40	  match plan:
41	    case SP.Empty{}:SP.Empty{}
42	    case SP.Entry{Sch.System{id,slot},requirements}:SP.Entry{Sch.System{id,(slot + offset : U32)},requirements}
43	    case SP.Entry{Sch.Phase{name},requirements}:SP.Entry{Sch.Phase{name},requirements}
44	    case SP.Entry{Sch.Barrier{},requirements}:SP.Entry{Sch.Barrier{},requirements}
45	    case SP.Sequence{left,right}:SP.Sequence{shifted(~S,left,offset),shifted(~S,right,offset)}
46	def built_pair(~S:Data,~Ids:Data,first:Ids -> SP.Plan<S>,second:Ids -> SP.Plan<S>,offset:Nat,+ids:Ids) -> SP.Plan<S>:SP.Sequence{first(ids),shifted(~S,second(ids),U32.from_nat(offset))}
47	def selected(~S:Data,~C:Type,~R:Type,~E:Data,chosen:Bool,left:W.World<S,C,R,E> -> U32 -> W.World<S,C,R,E> & Bool,right:W.World<S,C,R,E> -> U32 -> W.World<S,C,R,E> & Bool,world:W.World<S,C,R,E>,slot:U32,offset:Nat) -> W.World<S,C,R,E> & Bool:
48	  match chosen:
49	    case True{}:left(world,slot)
50	    case False{}:right(world,(slot - U32.from_nat(offset) : U32))
51	def evaluated_pair(~S:Data,~C:Type,~R:Type,~E:Data,left:W.World<S,C,R,E> -> U32 -> W.World<S,C,R,E> & Bool,right:W.World<S,C,R,E> -> U32 -> W.World<S,C,R,E> & Bool,+offset:Nat,world:W.World<S,C,R,E>,+slot:U32) -> W.World<S,C,R,E> & Bool:selected(~S,~C,~R,~E,Nat.is_lt(U32.to_nat(slot),offset),left,right,world,slot,offset)
52	# Compose programs in authored order, shifting right-side system condition
53	# slots by left width. Preserves names/requirements and World-threading routing;
54	# does not evaluate predicates or reorder systems by dependency.
55	def sequence(~S:Data,~C:Type,~R:Type,~E:Data,~Ids:Data,first:Program<S,C,R,E,Ids>,second:Program<S,C,R,E,Ids>) -> Program<S,C,R,E,Ids>:
56	  match first second:
57	    case Program{+leftWidth,leftBuild,leftNames,leftEval} Program{rightWidth,rightBuild,rightNames,rightEval}:Program{Nat.add(leftWidth,rightWidth),ids => built_pair(~S,~Ids,leftBuild,rightBuild,leftWidth,ids),List.append(&2,String,leftNames,rightNames),world => slot => evaluated_pair(~S,~C,~R,~E,leftEval,rightEval,leftWidth,world,slot)}
58	# Consume a program to obtain its slot-indexed World-threading evaluator.
59	# Use slots from the matching materialized/validated program; arbitrary callback
60	# mutations or host effects are not transactionally isolated by this adapter.
61	def evaluator(~S:Data,~C:Type,~R:Type,~E:Data,~Ids:Data,program:Program<S,C,R,E,Ids>) -> W.World<S,C,R,E> -> U32 -> W.World<S,C,R,E> & Bool:
62	  match program:
63	    case Program{_,_,_,evaluate}:evaluate
64	def built(~S:Data,~Ids:Data,width:Nat,names:List<&2,String>,result:SP.Plan<S>) -> Entries<S>:Entries{width,result,names}
65	# Build detached Entries from authored Ids, retaining plan order/names.
66	# Does not validate registration liveness or run guards; valid checks structural
67	# slot bounds before ordinary schedule attachment checks actual registration IDs.
68	def materialize(~S:Data,~C:Type,~R:Type,~E:Data,~Ids:Data,declaration:Program<S,C,R,E,Ids>,ids:Ids) -> Entries<S>:
69	  match declaration:
70	    case Program{width,build,names,_}:built(~S,~Ids,width,names,build(ids))
71	# Advanced structural check that each system's condition slot is below width.
72	# Does not check World association, live registrations or predicate provenance.
73	def slots(~S:Data,plan:SP.Plan<S>,+width:Nat) -> Bool:
74	  match plan:
75	    case SP.Empty{}:True{}
76	    case SP.Entry{Sch.System{_,slot},_}:Nat.is_lt(U32.to_nat(slot),width)
77	    case SP.Entry{Sch.Phase{_},_}:True{}
78	    case SP.Entry{Sch.Barrier{},_}:True{}
79	    case SP.Sequence{left,right}:Bool.and(slots(~S,left,width),slots(~S,right,width))
80	# Structural validation only. Trusted closed constructors establish provenance.
81	# Check width/name length agreement, representable slot range and slot bounds.
82	# Structural validation only: trusted constructors establish correspondence
83	# between predicates, names and plan; this is not runtime authority validation.
84	def valid(~S:Data,entries:Entries<S>) -> Bool:
85	  match entries:
86	    case Entries{+width,plan,names}:Bool.and(Nat.is_eq(width,List.length(&2,String,names)),Bool.and(Nat.is_le(width,1n+U32.to_nat(4294967295)),slots(~S,plan,width)))
87	# Consume Entries and return its operational plan without evaluating guards.
88	def plan(~S:Data,entries:Entries<S>) -> SP.Plan<S>:
89	  match entries:
90	    case Entries{_,plan,_}:plan
91	# Detached name lookup by Nat position, returning None outside the list.
92	# Names are descriptive; finding one supplies no execution authority.
93	def lookup(names:List<&2,String>,index:Nat) -> Maybe<&2,String>:
94	  match names index:
95	    case [] _:None{}
96	    case first <> _ 0n:Some{first}
97	    case _ <> rest 1n+prior:lookup(rest,prior)
98	# Return the optional authored name for a materialized condition slot.
99	# Does not validate a registration or execute the corresponding predicate.
100	def condition_name(~S:Data,entries:Entries<S>,slot:U32) -> Maybe<&2,String>:
101	  match entries:
102	    case Entries{_,_,names}:lookup(names,U32.to_nat(slot))