summaryrefslogtreecommitdiff
path: root/grammars/timetable/Timetable.gf
diff options
context:
space:
mode:
Diffstat (limited to 'grammars/timetable/Timetable.gf')
-rw-r--r--grammars/timetable/Timetable.gf31
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 ;
+}