fact: Definition WheelSensorSpec : ADT WheelSensorSig := Eval simpl in Def ADT { rep := QueryStructure WheelSensorSchema, Def Constructor0 "Init" : rep := empty,, Def Method1 "AddSpeedSubscriber" (r : rep) (addr : IPAddress) : rep * bool := Insert <"topic" :: ``"Speed", "address" :: addr> into r!"subscribers", Def Method1 "AddTirePressureSubscriber" (r : rep) (addr : IPAddress) : rep * bool := Insert <"topic" :: ``"TirePressure", "address" :: addr> into r!"subscribers", Def Method1 "PublishSpeed" (r : rep) (n : nat) : rep * (list (IPAddress* bin)) := `(msg, _) <- encode_SensorData_Spec (inj_SumType SensorTypes SensorIDs[@"Speed"] n) Empty; subs <- For (sub in r!"subscribers") Where (sub!"topic" = ``"Speed") Return (sub!"address", msg); ret (r, subs), Def Method1 "PublishTirePressure" (r : rep) (n : nat) : rep * (list (IPAddress * bin)) := `(msg, _) <- encode_SensorData_Spec (inj_SumType SensorTypes SensorIDs[@"TirePressure"] n) Empty; subs <- For (sub in r!"subscribers") Where (sub!"topic" = ``"TirePressure") Return (sub!"address", msg); ret (r, subs) }%methDefParsing.
imports: Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Coq.Structures.OrderedType Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Compose Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Lib2.WordOpt Fiat.Narcissus.Lib2.NatOpt Fiat.Narcissus.Lib2.StringOpt Fiat.Narcissus.Lib2.EnumOpt Fiat.Narcissus.Lib2.FixListOpt Fiat.Narcissus.Lib2.SumTypeOpt Fiat.Common.SumType Fiat.Examples.Tutorial.Tutorial Fiat.Examples.DnsServer.DecomposeEnumField Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.MasterPlan Fiat.Examples.HACMSDemo.DuplicateFree Fiat.Examples.HACMSDemo.HACMSDemo Bedrock.Word Bedrock.Memory