1 import Base 2 import ./execution_builder.bend as Build 3 import ./execution_declaration.bend as D 4 import ./execution_resource_program.bend as Program 5 import ./execution_resource_recipe.bend as Resources 6 import ./execution_resource_description.bend as Description 7 import ./execution_query_schema.bend as Schema 8 import ./execution_query_admission.bend as Query 9 import ./execution_query_recipe.bend as Recipe 10 import ./execution_composer_layout.bend as L 11 import ./world.bend as W 12 import ./entity_allocator.bend as Allocator 13 import ./deferred_command.bend as Deferred 14 import ./clock_state.bend as Clock 15 import ./execution_lifecycle_notices.bend as Notice 16 17 # Both route inventories come from ONE actual closed compilation. The actual 18 # canonical affine owners remain in World; Data never substitutes for them. 19 type Evidence<-S:Data,-components:L.Layout,-resources:L.Layout,-C:Type,-R:Type,-Ops:Data -> (Type -> Type) -> Type -> Type,-program:Build.FrameworkProgram(~S,~L.columns(~S,components),~C,~R,~Ops)> is Data: 20 Evidence{namespace:U32,handles:List<&2,W.Handle>,queryRecipes:List<&2,Recipe.Recipe>,resourceRecipes:List<&2,Resources.Entry>,componentInfo:List<&2,Schema.Info>,resourceInfo:List<&2,Description.Info>,grants:List<&2,Query.Granted>,queryBook:Schema.Book,resourceBook:Resources.Book} 21 type Inspection<-S:Data,-components:L.Layout,-resources:L.Layout,-C:Type,-R:Type,-E:Data,-Ops:Data -> (Type -> Type) -> Type -> Type,-program:Build.FrameworkProgram(~S,~L.columns(~S,components),~C,~R,~Ops)> is Type: 22 Admitted{world:W.World,compilation:D.Compilation,evidence:Evidence} 23 Refused{world:W.World,compilation:D.Compilation} 24 def lowered(~S:Data,~components:L.Layout,~resources:L.Layout,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~program:Build.FrameworkProgram(~S,~L.columns(~S,components),~C,~R,~Ops),world:W.World,compilation:D.Compilation,namespace:U32,handles:List<&2,W.Handle>,queries:List<&2,Recipe.Recipe>,+resourceRecipes:List<&2,Resources.Entry>,componentInfo:List<&2,Schema.Info>,resourceInfo:List<&2,Description.Info>,result:Query.Lowering) -> Inspection: 25 match result: 26 case Query.LoweringRefused{}:Refused{world,compilation} 27 case Query.Lowered{grants,queryBook}:Admitted{world,compilation,Evidence{namespace,handles,queries,resourceRecipes,componentInfo,resourceInfo,grants,queryBook,Resources.Book{resourceRecipes}}} 28 def supported(~S:Data,~components:L.Layout,~resources:L.Layout,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~program:Build.FrameworkProgram(~S,~L.columns(~S,components),~C,~R,~Ops),world:W.World,compilation:D.Compilation,+namespace:U32,+handles:List<&2,W.Handle>,+componentInfo:List<&2,Schema.Info>,resourceInfo:List<&2,Description.Info>,valid:Bool) -> Inspection: 29 match compilation valid: 30 case compilation False{}:Refused{world,compilation} 31 case D.Unsupported{caps,access,recipes} True{}:Refused{world,D.Unsupported{caps,access,recipes}} 32 case D.Supported{D.Declaration{caps,access},D.Recipes{+queries,+resourceRecipes}} True{}:lowered(~S,~components,~resources,~C,~R,~E,~Ops,~program,world,D.Supported{D.Declaration{caps,access},D.Recipes{queries,resourceRecipes}},namespace,handles,queries,resourceRecipes,componentInfo,resourceInfo,Query.lower(~S,~L.columns(~S,components),~components,~{==},queries,componentInfo,namespace,handles)) 33 def checked_resources(~S:Data,~components:L.Layout,~resources:L.Layout,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~program:Build.FrameworkProgram(~S,~L.columns(~S,components),~C,~R,~Ops),world:W.World,namespace:U32,handles:List<&2,W.Handle>,componentInfo:List<&2,Schema.Info>,resourceInfo:List<&2,Description.Info>,valid:Bool,compilation:D.Compilation) -> Inspection: 34 match compilation: 35 case D.Unsupported{caps,access,recipes}:Refused{world,D.Unsupported{caps,access,recipes}} 36 case D.Supported{declaration,D.Recipes{queries,+resourceRecipes}}:supported(~S,~components,~resources,~C,~R,~E,~Ops,~program,world,D.Supported{declaration,D.Recipes{queries,resourceRecipes}},namespace,handles,componentInfo,resourceInfo,Bool.and(valid,Bool.and(L.unique(resources),Resources.valid(~resources,resourceRecipes)))) 37 def described_resources(~S:Data,~components:L.Layout,~resources:L.Layout,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~program:Build.FrameworkProgram(~S,~L.columns(~S,components),~C,~R,~Ops),compilation:D.Compilation,+namespace:U32,allocator:Allocator.Allocator,columns:L.columns(~S,components),events:List<&2,E>,pending:List>>,registrations:List<&2,W.RegistrationMeta>,next:U32,clock:Clock.State,lifecycle:Notice.Journal,handles:List<&2,W.Handle>,componentInfo:List<&2,Schema.Info>,valid:Bool,result:Description.Description) -> Inspection: 38 match result: 39 case Description.Description{owners,info}:checked_resources(~S,~components,~resources,~C,~R,~E,~Ops,~program,W.World{namespace,allocator,columns,owners,events,pending,registrations,next,clock,lifecycle},namespace,handles,componentInfo,info,valid,compilation) 40 def described_components(~S:Data,~components:L.Layout,~resources:L.Layout,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~program:Build.FrameworkProgram(~S,~L.columns(~S,components),~C,~R,~Ops),compilation:D.Compilation,namespace:U32,allocator:Allocator.Allocator,owners:L.resources(~S,resources),events:List<&2,E>,pending:List>>,registrations:List<&2,W.RegistrationMeta>,next:U32,clock:Clock.State,lifecycle:Notice.Journal,handles:List<&2,W.Handle>,result:Schema.Description) -> Inspection: 41 match result: 42 case Schema.Description{columns,info,valid}:described_resources(~S,~components,~resources,~C,~R,~E,~Ops,~program,compilation,namespace,allocator,columns,events,pending,registrations,next,clock,lifecycle,handles,info,valid,Description.describe(~S,resources,L.AtLeaf{},owners)) 43 def captured(~S:Data,~components:L.Layout,~resources:L.Layout,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~program:Build.FrameworkProgram(~S,~L.columns(~S,components),~C,~R,~Ops),compilation:D.Compilation,result:W.World & List<&2,W.Handle>) -> Inspection: 44 match result: 45 case (W.World{namespace,allocator,columns,owners,events,pending,registrations,next,clock,lifecycle},handles):described_components(~S,~components,~resources,~C,~R,~E,~Ops,~program,compilation,namespace,allocator,owners,events,pending,registrations,next,clock,lifecycle,handles,Schema.describe(~S,components,L.AtLeaf{},columns)) 46 # No clock entry, registration, body, or resource-owner extraction occurs here. 47 def inspect_with_compilation(~S:Data,~components:L.Layout,~resources:L.Layout,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~program:Build.FrameworkProgram(~S,~L.columns(~S,components),~C,~R,~Ops),compilation:D.Compilation,world:W.World) -> Inspection: 48 captured(~S,~components,~resources,~C,~R,~E,~Ops,~program,compilation,W.handles(~S,~L.columns(~S,components),~L.resources(~S,resources),~E,world)) 49 50 def inspect(~S:Data,~components:L.Layout,~resources:L.Layout,~C:Type,~R:Type,~E:Data,~Ops:Data -> (Type -> Type) -> Type -> Type,~program:Build.FrameworkProgram(~S,~L.columns(~S,components),~C,~R,~Ops),world:W.World) -> Inspection: 51 inspect_with_compilation(~S,~components,~resources,~C,~R,~E,~Ops,~program,Program.compile_framework(~S,~L.columns(~S,components),~C,~R,~Ops,~program),world)