module ExampleDatabase where
open import Data.String
open import Data.Nat
open import Data.List
open import Data.Product
open import Schema
departmentsTable : TableType
departmentsTable =
("DNAME" , string 100) ∷
("ADDRESS" , string 100) ∷
[]
programsTable : TableType
programsTable =
("PNAME" , string 100) ∷
("ABBR" , string 10) ∷
[]
branchesTable : TableType
branchesTable =
("BID" , number) ∷
("BNAME" , string 100) ∷
("BPROGRAM" , string 100) ∷
[]
studentsTable : TableType
studentsTable =
("SID" , number) ∷
("SNAME" , string 100) ∷
("SBRANCH" , number) ∷
[]
coursesTable : TableType
coursesTable =
("CODE" , string 10) ∷
("CNAME" , string 100) ∷
("CREDIT" , number) ∷
("CDEPARTMENT" , string 100) ∷
("NSTUDENTS" , number) ∷
[]
classifiedCoursesTable : TableType
classifiedCoursesTable =
("CCOURSE" , string 10) ∷
("CTYPE" , string 20) ∷
[]
departmentsProgramsTable : TableType
departmentsProgramsTable =
("DPDEPARTMENT" , string 100) ∷
("DPPROGRAM" , string 100) ∷
[]
branchRecommendedCoursesTable : TableType
branchRecommendedCoursesTable =
("RCOURSE" , string 10) ∷
("RBRANCH" , number) ∷
[]
branchMandatoryCoursesTable : TableType
branchMandatoryCoursesTable =
("BMCOURSE" , string 10) ∷
("BMBRANCH" , number) ∷
[]
programMandatoryCoursesTable : TableType
programMandatoryCoursesTable =
("PMCOURSE" , string 10) ∷
("PMPROGRAM" , string 100) ∷
[]
requiredCoursesTable : TableType
requiredCoursesTable =
("DEPENDENT" , string 10) ∷
("REQUIRED" , string 10) ∷
[]
coursesStudentsTable : TableType
coursesStudentsTable =
("CSCOURSE" , string 10) ∷
("CSSTUDENT" , number) ∷
("EVENTDATE" , string 19) ∷
("STATUS" , number) ∷
[]
universitySchema : Schema
universitySchema =
("Departments" , departmentsTable) ∷
("Programs" , programsTable) ∷
("Branches" , branchesTable) ∷
("Students" , studentsTable) ∷
("Courses" , coursesTable) ∷
("ClassifiedCourses" , classifiedCoursesTable) ∷
("DepartmentsPrograms" , departmentsProgramsTable) ∷
("BranchRecommendedCourses" , branchRecommendedCoursesTable) ∷
("BranchMandatoryCourses" , branchMandatoryCoursesTable) ∷
("ProgramMandatoryCourses" , programMandatoryCoursesTable) ∷
("RequiredCourses" , requiredCoursesTable) ∷
("CoursesStudents" , coursesStudentsTable) ∷
[]