fact: Definition MessagesSpec : ADT MessagesSig := Def ADT { rep := QueryStructure MessagesSchema, Def Constructor0 "Init" : rep := empty,, Def Method1 "AddMessage" (r : rep) (message : MessagesSchema#MESSAGES) : rep * bool := Insert message into r ! MESSAGES, Def Method1 "AddContact" (r : rep) (contact : MessagesSchema#CONTACTS) : rep * bool := Insert contact into r ! CONTACTS, Def Method1 "ContactMessages" (r : rep) (name : string) : rep * list MessageT := msgs <- For (contact in r ! CONTACTS) (messages in r ! MESSAGES) Where (contact!NAME = name) Where (messages!PHONE_NUMBER = contact!PHONE_NUMBER) Return messages!MESSAGE; ret (r, msgs), Def Method1 "RelevantMessages" (r : rep) (search_terms : list string) : rep * list MessageT := msgs <- For (message in r ! MESSAGES) Where (IncludedIn search_terms message!MESSAGE) Return message!MESSAGE; ret (r, msgs) }%methDefParsing.
imports: Fiat.QueryStructure.Automation.MasterPlan