timetable

1 files changed, 31 insertions, 0 deletions

diff --git a/grammars/timetable/Timetable.gf b/grammars/timetable/Timetable.gf
new file mode 100644
index 000000000..8eab2600b
--- /dev/null
+++ b/grammars/timetable/Timetable.gf
@@ -0,0 +1,31 @@
+abstract Timetable = {
+  cat
+    Table ;
+    TrainList CityList ;
+    City ;
+    CityList ;
+    Train CityList ;
+    Stop ;
+    Time ;
+    Number ;
+
+  fun
+    MkTable : (cs : CityList) -> TrainList cs -> Table ;
+    NilTrain : (cs : CityList) -> TrainList cs ;
+    ConsTrain : 
+      (cs : CityList) -> Number -> Train cs -> TrainList cs -> TrainList cs ;
+    OneCity : City -> CityList ;
+    ConsCity : City -> CityList -> CityList ;
+
+    StopTime : Time -> Stop ;
+    NoStop : Stop ;
+    
+    LocTrain : (c : City) -> Stop -> Train (OneCity c) ;
+    CityTrain : 
+      (c : City) -> Stop -> (cs : CityList) -> 
+        Train cs -> Train (ConsCity c cs) ;
+
+    T : Int -> Time ;
+    N : Int -> Number ;
+    C : String -> City ;
+}