rewards.bend
gralha-bendquest@0.1.0.0 · 285 lines · 29 definitions
1
2import Base
3import gralha-bendquest@0.1.0.0/game.bend as G
4import gralha-bendquest@0.1.0.0/health.bend as H
5import gralha-bendquest@0.1.0.0/growth.bend as Growth
6
7type Rewards.Result is Data:
8 Rewards.Result{hero: G.Bq.Hero, xp: U32, levels: U32}
9
10def Rewards.hero(result: Rewards.Result) -> G.Bq.Hero:
11 match result:
12 case Rewards.Result{hero, xp, levels}:
13 hero
14
15def Rewards.level(hero: G.Bq.Hero) -> Nat:
16 match hero:
17 case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
18 level
19
20def Rewards.charm_amount(has_bonus: Bool) -> U32:
21 match has_bonus:
22 case True{}:
23 30
24 case False{}:
25 0
26
27def Rewards.charm_bonus(charm: G.Bq.Maybe(Nat)) -> U32:
28 match charm:
29 case Fail{unit}:
30 0
31 case Done{kind}:
32 Rewards.charm_amount(U32.is_eq(U32.from_nat(kind), 17))
33
34def Rewards.maximum(+hero: G.Bq.Hero, ceiling: U32) -> U32:
35 match hero:
36 case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
37 Growth.Growth.maximum(level, vitality, Rewards.charm_bonus(charm), ceiling)
38
39def Rewards.cost(+level: U32) -> U32:
40 U32.mul(U32.mul(25, level), level)
41
42def Rewards.eligible(+hero: G.Bq.Hero, +xp: U32) -> Bool:
43 +level = U32.from_nat(Rewards.level(hero))
44 Bool.and(U32.is_lt(level, 20), U32.is_ge(xp, Rewards.cost(level)))
45
46def Rewards.loop(fuel: Nat, eligible: Bool, +hero: G.Bq.Hero, +xp: U32, +levels: U32) -> Rewards.Result:
47 match fuel:
48 case Zero{}:
49 Rewards.Result{hero, xp, levels}
50 case Succ{remaining}:
51 match eligible:
52 case False{}:
53 Rewards.Result{hero, xp, levels}
54 case True{}:
55 +next_hero = G.Bq.hero_step(G.Bq.HOp.LevelUp{}, hero)
56 +next_xp = U32.sub(xp, Rewards.cost(U32.from_nat(Rewards.level(hero))))
57 Rewards.loop(remaining, Rewards.eligible(next_hero, next_xp), next_hero, next_xp, U32.add(levels, 1))
58
59def Rewards.go(fuel: Nat, +hero: G.Bq.Hero, +xp: U32, levels: U32) -> Rewards.Result:
60 Rewards.loop(fuel, Rewards.eligible(hero, xp), hero, xp, levels)
61
62def Rewards.gain(+hero: G.Bq.Hero, xp: U32, gained: U32) -> Rewards.Result:
63 Rewards.go(20n, hero, U32.add(xp, gained), 0)
64
65law Rewards.level_up_health:
66 for +hero: G.Bq.Hero
67 for +hp: U32
68 for +ceiling: U32
69 for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
70 {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(G.Bq.hero_step(G.Bq.HOp.LevelUp{}, hero), ceiling))) == True{} : Bool}
71
72def Rewards.level_up_health(hero, hp, ceiling, valid):
73 match hero:
74 case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
75 Growth.Growth.level_up_preserves_health(hp, level, vitality, Rewards.charm_bonus(charm), ceiling, valid)
76
77law Rewards.loop_health:
78 for +fuel: Nat
79 for +eligible: Bool
80 for +hero: G.Bq.Hero
81 for +xp: U32
82 for +levels: U32
83 for +hp: U32
84 for +ceiling: U32
85 for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
86 {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(Rewards.hero(Rewards.loop(fuel, eligible, hero, xp, levels)), ceiling))) == True{} : Bool}
87
88def Rewards.loop_health(fuel, eligible, hero, xp, levels, hp, ceiling, valid):
89 match fuel:
90 case Zero{}:
91 valid
92 case Succ{remaining}:
93 match eligible:
94 case False{}:
95 valid
96 case True{}:
97 +next_hero = G.Bq.hero_step(G.Bq.HOp.LevelUp{}, hero)
98 +next_xp = U32.sub(xp, Rewards.cost(U32.from_nat(Rewards.level(hero))))
99 Rewards.loop_health(remaining, Rewards.eligible(next_hero, next_xp), next_hero, next_xp, U32.add(levels, 1), hp, ceiling, Rewards.level_up_health(hero, hp, ceiling, valid))
100
101law Rewards.gain_health:
102 for +hero: G.Bq.Hero
103 for +xp: U32
104 for +gained: U32
105 for +hp: U32
106 for +ceiling: U32
107 for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
108 {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(Rewards.hero(Rewards.gain(hero, xp, gained)), ceiling))) == True{} : Bool}
109
110def Rewards.gain_health(hero, xp, gained, hp, ceiling, valid):
111 Rewards.loop_health(20n, Rewards.eligible(hero, U32.add(xp, gained)), hero, U32.add(xp, gained), 0, hp, ceiling, valid)
112
113law Rewards.loop_equipped:
114 for +fuel: Nat
115 for +eligible: Bool
116 for +hero: G.Bq.Hero
117 for +xp: U32
118 for +levels: U32
119 for +valid: G.Bq.WellEquipped(hero)
120 G.Bq.WellEquipped(Rewards.hero(Rewards.loop(fuel, eligible, hero, xp, levels)))
121
122def Rewards.loop_equipped(fuel, eligible, hero, xp, levels, valid):
123 match fuel:
124 case Zero{}:
125 valid
126 case Succ{remaining}:
127 match eligible:
128 case False{}:
129 valid
130 case True{}:
131 +next_hero = G.Bq.hero_step(G.Bq.HOp.LevelUp{}, hero)
132 +next_xp = U32.sub(xp, Rewards.cost(U32.from_nat(Rewards.level(hero))))
133 Rewards.loop_equipped(remaining, Rewards.eligible(next_hero, next_xp), next_hero, next_xp, U32.add(levels, 1), G.Bq.ops_respect_requirements(G.Bq.HOp.LevelUp{}, hero, valid))
134
135law Rewards.gain_equipped:
136 for +hero: G.Bq.Hero
137 for +xp: U32
138 for +gained: U32
139 for +valid: G.Bq.WellEquipped(hero)
140 G.Bq.WellEquipped(Rewards.hero(Rewards.gain(hero, xp, gained)))
141
142def Rewards.gain_equipped(hero, xp, gained, valid):
143 Rewards.loop_equipped(20n, Rewards.eligible(hero, U32.add(xp, gained)), hero, U32.add(xp, gained), 0, valid)
144
145
146def Rewards.add_item(hero: G.Bq.Hero, kind: U32) -> G.Bq.Hero:
147 match hero:
148 case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
149 G.Bq.Hero.Hero{G.Bq.Bag.add(G.Bq.one(U32.to_nat(kind)), inv), wea, arm, hel, charm, gold, level, strength, agility, vitality, points}
150
151def Rewards.add_gold(hero: G.Bq.Hero, amount: U32) -> G.Bq.Hero:
152 match hero:
153 case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
154 G.Bq.Hero.Hero{inv, wea, arm, hel, charm, G.Bq.Nat.add(U32.to_nat(amount), gold), level, strength, agility, vitality, points}
155
156def Rewards.sidequest_nat(quest: Nat, hero: G.Bq.Hero) -> G.Bq.Hero:
157 match quest:
158 case Zero{}:
159 Rewards.add_item(Rewards.add_item(Rewards.add_item(hero, 0), 0), 0)
160 case Succ{rest}:
161 match rest:
162 case Zero{}:
163 Rewards.add_item(hero, 13)
164 case Succ{later}:
165 Rewards.add_item(hero, 16)
166
167def Rewards.sidequest(hero: G.Bq.Hero, quest: U32) -> G.Bq.Hero:
168 Rewards.sidequest_nat(U32.to_nat(quest), hero)
169
170law Rewards.add_item_health:
171 for +hero: G.Bq.Hero
172 for +kind: U32
173 for +hp: U32
174 for +ceiling: U32
175 for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
176 {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(Rewards.add_item(hero, kind), ceiling))) == True{} : Bool}
177
178def Rewards.add_item_health(hero, kind, hp, ceiling, valid):
179 match hero:
180 case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
181 valid
182
183law Rewards.add_item_equipped:
184 for +hero: G.Bq.Hero
185 for +kind: U32
186 for +valid: G.Bq.WellEquipped(hero)
187 G.Bq.WellEquipped(Rewards.add_item(hero, kind))
188
189def Rewards.add_item_equipped(hero, kind, valid):
190 match hero:
191 case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
192 valid
193
194law Rewards.add_gold_health:
195 for +hero: G.Bq.Hero
196 for +amount: U32
197 for +hp: U32
198 for +ceiling: U32
199 for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
200 {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(Rewards.add_gold(hero, amount), ceiling))) == True{} : Bool}
201
202def Rewards.add_gold_health(hero, amount, hp, ceiling, valid):
203 match hero:
204 case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
205 valid
206
207law Rewards.add_gold_equipped:
208 for +hero: G.Bq.Hero
209 for +amount: U32
210 for +valid: G.Bq.WellEquipped(hero)
211 G.Bq.WellEquipped(Rewards.add_gold(hero, amount))
212
213def Rewards.add_gold_equipped(hero, amount, valid):
214 match hero:
215 case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
216 valid
217
218law Rewards.sidequest_nat_health:
219 for +quest: Nat
220 for +hero: G.Bq.Hero
221 for +hp: U32
222 for +ceiling: U32
223 for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
224 {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(Rewards.sidequest_nat(quest, hero), ceiling))) == True{} : Bool}
225
226def Rewards.sidequest_nat_health(quest, hero, hp, ceiling, valid):
227 match quest:
228 case Zero{}:
229 Rewards.add_item_health(Rewards.add_item(Rewards.add_item(hero, 0), 0), 0, hp, ceiling, Rewards.add_item_health(Rewards.add_item(hero, 0), 0, hp, ceiling, Rewards.add_item_health(hero, 0, hp, ceiling, valid)))
230 case Succ{rest}:
231 match rest:
232 case Zero{}:
233 Rewards.add_item_health(hero, 13, hp, ceiling, valid)
234 case Succ{later}:
235 Rewards.add_item_health(hero, 16, hp, ceiling, valid)
236
237law Rewards.sidequest_nat_equipped:
238 for +quest: Nat
239 for +hero: G.Bq.Hero
240 for +valid: G.Bq.WellEquipped(hero)
241 G.Bq.WellEquipped(Rewards.sidequest_nat(quest, hero))
242
243def Rewards.sidequest_nat_equipped(quest, hero, valid):
244 match quest:
245 case Zero{}:
246 Rewards.add_item_equipped(Rewards.add_item(Rewards.add_item(hero, 0), 0), 0, Rewards.add_item_equipped(Rewards.add_item(hero, 0), 0, Rewards.add_item_equipped(hero, 0, valid)))
247 case Succ{rest}:
248 match rest:
249 case Zero{}:
250 Rewards.add_item_equipped(hero, 13, valid)
251 case Succ{later}:
252 Rewards.add_item_equipped(hero, 16, valid)
253
254law Rewards.sidequest_health:
255 for +hero: G.Bq.Hero
256 for +quest: U32
257 for +hp: U32
258 for +ceiling: U32
259 for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
260 {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(Rewards.sidequest(hero, quest), ceiling))) == True{} : Bool}
261
262def Rewards.sidequest_health(hero, quest, hp, ceiling, valid):
263 Rewards.sidequest_nat_health(U32.to_nat(quest), hero, hp, ceiling, valid)
264
265law Rewards.sidequest_equipped:
266 for +hero: G.Bq.Hero
267 for +quest: U32
268 for +valid: G.Bq.WellEquipped(hero)
269 G.Bq.WellEquipped(Rewards.sidequest(hero, quest))
270
271def Rewards.sidequest_equipped(hero, quest, valid):
272 Rewards.sidequest_nat_equipped(U32.to_nat(quest), hero, valid)
273
274law Rewards.maximum_positive:
275 for +hero: G.Bq.Hero
276 for +ceiling: U32
277 for +limit_positive: {G.Bq.Nat.le(1n, U32.to_nat(ceiling)) == True{} : Bool}
278 {G.Bq.Nat.le(1n, U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
279
280def Rewards.maximum_positive(hero, ceiling, limit_positive):
281 match hero:
282 case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
283 H.Health.cap_nat_word_positive(Nat.add(U32.to_nat(Rewards.charm_bonus(charm)), G.Bq.max_hp(level, vitality)), ceiling,
284 (%Equal.sym(Nat, Nat.add(U32.to_nat(Rewards.charm_bonus(charm)), G.Bq.max_hp(level, vitality)), G.Bq.Nat.add(U32.to_nat(Rewards.charm_bonus(charm)), G.Bq.max_hp(level, vitality)), H.Health.add_agrees(U32.to_nat(Rewards.charm_bonus(charm)), G.Bq.max_hp(level, vitality))) : {G.Bq.Nat.le(1n, _) == True{} : Bool};
285 H.Health.le_trans(1n, G.Bq.max_hp(level, vitality), G.Bq.Nat.add(U32.to_nat(Rewards.charm_bonus(charm)), G.Bq.max_hp(level, vitality)), {==}, Growth.Growth.le_add_prefix(U32.to_nat(Rewards.charm_bonus(charm)), G.Bq.max_hp(level, vitality)))), limit_positive)