fact: Definition GithubSpec : ADT _ := Def ADT { rep := QueryStructure GithubSchema, Def Constructor0 "Init" : rep := empty,, Def Method1 "AddRepository" (r : rep) (repository : GithubSchema#REPOSITORIES) : rep * bool := Insert repository into r!REPOSITORIES, Def Method1 "AddCommit" (r : rep) (commit : GithubSchema#COMMITS) : rep * bool := Insert commit into r!COMMITS, Def Method1 "PopularProjects" (r : rep) (star_threshold : nat) : rep * (list string) := res <- For (repository in r!REPOSITORIES) Where (repository!STAR >= star_threshold) Return repository!PROJECT_NAME; ret (r, res), Def Method1 "ProjectCommits" (r : rep) (project : string) : rep * list hash := res <- For (commit in r!COMMITS) Where (commit!PROJECT_NAME = project) Return commit!HASH; ret (r, res), Def Method1 "RecentProjects" (r : rep) (date_threshold : nat) : rep * list string := res <- For (repository in r!REPOSITORIES) ( c <- Count (For (commit in r!COMMITS) Where (commit!PROJECT_NAME = repository!PROJECT_NAME) Where (commit!CREATED_AT >= date_threshold) Return ()); If (c == 0) Then ret [ ] Else ret [repository!PROJECT_NAME]); ret (r, res) }%methDefParsing.
imports: Fiat.QueryStructure.Automation.MasterPlan