1	import Base
2	import ../src/cache.bend as C
3	import ../src/codec.bend as Codec
4	import ../src/public.bend as Pub
5	import ../src/driver.bend as D
6	import ../spec/cache.bend as S
7	import ../spec/clock.bend as Clock
8	import ../spec/operations.bend as O
9	import ../spec/public_commands.bend as PC
10	import ../spec/equivalence.bend as E
11	import ../types/model.bend as T
12	import ./refinement.bend as F
13	import ./invariants.bend as Inv
14	import ./disabled.bend as Disabled
15	import ./spec_lookup.bend as Lookup
16	import ./public_relation.bend as R
17	import ./public_finish.bend as Finish
18	import ./extensional_states.bend as Ext
19	import ./remove_refinement.bend as Remove
20	
21	# Whole public Remove through the actual start/drive machine, every event list.
22	def remove(-V: Data, zero_key: String, +zero_value: V, +c: C.Cache<String, V>, +key: String, +events: List<&2, Clock.ClockEvent>, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, disabled: {Disabled.flag(String, V, c) == False{} : Bool}) -> R.results(~String, ~Lookup.string_same, V, D.execute(~String, ~Codec.string_encode, V, zero_key, zero_value, c, events, Pub.Remove{key}), PC.execute(~String, ~Lookup.string_same, V, F.abstract(String, V, c), zero_key, zero_value, events, R.command(String, V, Pub.Remove{key}))):
23	  %Equal.sym(D.Outcome<String, V>, D.drive(String, V, zero_value, events, Pub.finish_step(String, V, zero_value, C.remove(String, V, Codec.string_encode, c, key), Pub.Flag{})), Finish.returned(V, zero_value, C.remove(String, V, Codec.string_encode, c, key), Pub.Flag{}, events, 0n), Finish.drive_step(V, zero_value, C.remove(String, V, Codec.string_encode, c, key), Pub.Flag{}, events)) : R.results(~String, ~Lookup.string_same, V, _, PC.observation(~String, ~Lookup.string_same, V, zero_key, zero_value, PC.Flag{}, S.remove(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key), events, 0n))
24	  Finish.finished(V, zero_key, zero_value, C.remove(String, V, Codec.string_encode, c, key), Pub.Flag{}, S.remove(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key), events, 0n, {==}, Remove.operation(V, c, key, valid, disabled))