1	import Base
2	import ./ordinary_condition_composition.bend as Old
3	import ./ordinary_check_declaration.bend as D
4	import ./world.bend as W
5	import ./check.bend as K
6	
7	type Shape is Data:
8	  Existing{description:Old.Description}
9	  Check{name:String}
10	  Constant{value:Bool}
11	  Not{inner:Shape}
12	  And{left:Shape,right:Shape}
13	  Or{left:Shape,right:Shape}
14	type Description is Data:Description{shape:Shape,uses:List<&2,D.Use>}
15	type Error is Data:
16	  CheckError{error:K.Error}
17	  NoValue{}
18	  InvalidRegistration{}
19	  NoBinding{}
20	type Evaluation<World:Type,Owner:Type> is Type:
21	  Evaluation{world:World,owner:Owner,result:Result<&2,&2,Error,Bool>}
22	type Condition<World:Type,Owner:Type,-evaluate:Owner -> World -> Evaluation<World,Owner>> is Type:
23	  Condition{owner:Owner,description:Description}
24	type Returned<World:Type,Owner:Type,-evaluate:Owner -> World -> Evaluation<World,Owner>> is Type:
25	  Returned{world:World,condition:Condition<World,Owner,evaluate>,result:Result<&2,&2,Error,Bool>}
26	def check_result(value:Result<&2,&2,K.Error,Bool>) -> Result<&2,&2,Error,Bool>:
27	  match value:
28	    case Done{value}:Done{value}
29	    case Fail{error}:Fail{CheckError{error}}
30	def lifted_returned(~World:Type,~Owner:Type,value:Old.Evaluation<World,Owner>) -> Evaluation<World,Owner>:
31	  match value:
32	    case Old.Value{world,owner,value}:Evaluation{world,owner,Done{value}}
33	    case Old.NoValue{world,owner}:Evaluation{world,owner,Fail{NoValue{}}}
34	    case Old.InvalidRegistration{world,owner}:Evaluation{world,owner,Fail{InvalidRegistration{}}}
35	    case Old.NoBinding{world,owner}:Evaluation{world,owner,Fail{NoBinding{}}}
36	def lift_run(~World:Type,~Owner:Type,~evaluate:Owner -> World -> Old.Evaluation<World,Owner>,owner:Owner,world:World) -> Evaluation<World,Owner>:lifted_returned(~World,~Owner,evaluate(owner,world))
37	def lift(~World:Type,~Owner:Type,~evaluate:Owner -> World -> Old.Evaluation<World,Owner>,value:Old.Condition<World,Owner,evaluate>) -> Condition<World,Owner,lift_run(~World,~Owner,~evaluate)>:
38	  match value:
39	    case Old.Condition{owner,description}:Condition{owner,Description{Existing{description},[]}}
40	def check_returned(~S:Data,~C:Type,~R:Type,~E:Data,~Args:Data,args:Args,value:K.Checked<S,C,R,E>) -> Evaluation<W.World<S,C,R,E>,Args>:
41	  match value:
42	    case K.Checked{world,result}:Evaluation{world,args,check_result(result)}
43	def check_shared(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Type -> Type,~Args:Data,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & Bool,~declaration:D.Declaration<S,C,R,E,Ops>,+args:Args,world:W.World<S,C,R,E>) -> Evaluation<W.World<S,C,R,E>,Args>:
44	  check_returned(~S,~C,~R,~E,~Args,args,K.run(~S,~C,~R,~E,~Ops,~Args,~body,~D.plan(~S,~C,~R,~E,~Ops,declaration),args,world))
45	def check_run(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Type -> Type,~Args:Data,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & Bool,~declaration:D.Declaration<S,C,R,E,Ops>,args:Args,world:W.World<S,C,R,E>) -> Evaluation<W.World<S,C,R,E>,Args>:
46	  check_shared(~S,~C,~R,~E,~Ops,~Args,~body,~declaration,args,world)
47	def check(~S:Data,~C:Type,~R:Type,~E:Data,~Ops:Type -> Type,~Args:Data,~body:@-H:Type -> @-caps:Ops(H) -> Args -> H -> H & Bool,~declaration:D.Declaration<S,C,R,E,Ops>,name:String,args:Args) -> Condition<W.World<S,C,R,E>,Args,check_run(~S,~C,~R,~E,~Ops,~Args,~body,~declaration)>:
48	  Condition{args,Description{Check{name},D.uses(~S,~C,~R,~E,~Ops,declaration)}}
49	def constant_shared(~World:Type,+value:Bool,world:World) -> Evaluation<World,Bool>:Evaluation{world,value,Done{value}}
50	def constant_run(~World:Type,value:Bool,world:World) -> Evaluation<World,Bool>:constant_shared(~World,value,world)
51	def constant(~World:Type,+value:Bool) -> Condition<World,Bool,constant_run(~World)>:Condition{value,Description{Constant{value},[]}}
52	def returned(~World:Type,~Owner:Type,~evaluate:Owner -> World -> Evaluation<World,Owner>,description:Description,value:Evaluation<World,Owner>) -> Returned<World,Owner,evaluate>:
53	  match value:
54	    case Evaluation{world,owner,result}:Returned{world,Condition{owner,description},result}
55	def run(~World:Type,~Owner:Type,~evaluate:Owner -> World -> Evaluation<World,Owner>,value:Condition<World,Owner,evaluate>,world:World) -> Returned<World,Owner,evaluate>:
56	  match value:
57	    case Condition{owner,description}:returned(~World,~Owner,~evaluate,description,evaluate(owner,world))
58	def negate(value:Result<&2,&2,Error,Bool>) -> Result<&2,&2,Error,Bool>:
59	  match value:
60	    case Done{value}:Done{Bool.not(value)}
61	    case Fail{error}:Fail{error}
62	def negated(~World:Type,~Owner:Type,value:Evaluation<World,Owner>) -> Evaluation<World,Owner>:
63	  match value:
64	    case Evaluation{world,owner,result}:Evaluation{world,owner,negate(result)}
65	def not_run(~World:Type,~Owner:Type,~evaluate:Owner -> World -> Evaluation<World,Owner>,owner:Owner,world:World) -> Evaluation<World,Owner>:negated(~World,~Owner,evaluate(owner,world))
66	def not(~World:Type,~Owner:Type,~evaluate:Owner -> World -> Evaluation<World,Owner>,value:Condition<World,Owner,evaluate>) -> Condition<World,Owner,not_run(~World,~Owner,~evaluate)>:
67	  match value:
68	    case Condition{owner,Description{shape,uses}}:Condition{owner,Description{Not{shape},uses}}
69	def right_returned(~World:Type,~Left:Type,~Right:Type,left:Left,value:Evaluation<World,Right>) -> Evaluation<World,Left & Right>:
70	  match value:
71	    case Evaluation{world,right,result}:Evaluation{world,(left,right),result}
72	def selected(~World:Type,~Left:Type,~Right:Type,~right_run:Right -> World -> Evaluation<World,Right>,allowed:Bool,left:Left,right:Right,world:World,+value:Bool) -> Evaluation<World,Left & Right>:
73	  match allowed:
74	    case False{}:Evaluation{world,(left,right),Done{value}}
75	    case True{}:right_returned(~World,~Left,~Right,left,right_run(right,world))
76	def same_bool(a:Bool,b:Bool) -> Bool:
77	  match a b:
78	    case True{} True{}:True{}
79	    case False{} False{}:True{}
80	    case _ _:False{}
81	def left_returned(~World:Type,~Left:Type,~Right:Type,~right_run:Right -> World -> Evaluation<World,Right>,on:Bool,right:Right,value:Evaluation<World,Left>) -> Evaluation<World,Left & Right>:
82	  match value:
83	    case Evaluation{world,left,Fail{error}}:Evaluation{world,(left,right),Fail{error}}
84	    case Evaluation{world,left,Done{+value}}:selected(~World,~Left,~Right,~right_run,same_bool(on,value),left,right,world,value)
85	def combined_run(~World:Type,~Left:Type,~Right:Type,~left_run:Left -> World -> Evaluation<World,Left>,~right_run:Right -> World -> Evaluation<World,Right>,~on:Bool,owners:Left & Right,world:World) -> Evaluation<World,Left & Right>:
86	  match owners:
87	    case (left,right):left_returned(~World,~Left,~Right,~right_run,on,right,left_run(left,world))
88	def and_then(~World:Type,~Left:Type,~Right:Type,~left_run:Left -> World -> Evaluation<World,Left>,~right_run:Right -> World -> Evaluation<World,Right>,left:Condition<World,Left,left_run>,right:Condition<World,Right,right_run>) -> Condition<World,Left & Right,combined_run(~World,~Left,~Right,~left_run,~right_run,~True{})>:
89	  match left right:
90	    case Condition{left,Description{ls,lu}} Condition{right,Description{rs,ru}}:Condition{(left,right),Description{And{ls,rs},List.append(&2,D.Use,lu,ru)}}
91	def or_else(~World:Type,~Left:Type,~Right:Type,~left_run:Left -> World -> Evaluation<World,Left>,~right_run:Right -> World -> Evaluation<World,Right>,left:Condition<World,Left,left_run>,right:Condition<World,Right,right_run>) -> Condition<World,Left & Right,combined_run(~World,~Left,~Right,~left_run,~right_run,~False{})>:
92	  match left right:
93	    case Condition{left,Description{ls,lu}} Condition{right,Description{rs,ru}}:Condition{(left,right),Description{Or{ls,rs},List.append(&2,D.Use,lu,ru)}}