timetable

This commit is contained in:
aarne
2004-04-28 09:08:31 +00:00
parent 1157649c85
commit fa596888f1
3 changed files with 77 additions and 0 deletions

View File

@@ -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 ;
}

View File

@@ -0,0 +1,22 @@
--# -path=.:../prelude
concrete TimetableEng of Timetable = open Prelude in {
lin
MkTable cs ts = ss (["trains on the line from"] ++ cs.s ++ ":" ++ ts.s) ;
NilTrain _ = ss [] ;
ConsTrain cs n t ts = ss (n.s ++ ":" ++ t.s ++ ";") ;
OneCity c = c ;
ConsCity c cs = ss (c.s ++ "to" ++ cs.s) ;
StopTime t = t ;
NoStop = ss ["no stop"] ;
LocTrain c s = cc2 c s ;
CityTrain c s cs t = ss (c.s ++ s.s ++ "," ++ t.s) ;
T i = prefixSS "at" i ;
N n = prefixSS "train" n ;
C s = s ;
}

View File

@@ -0,0 +1,24 @@
--# -path=.:../prelude
concrete TimetableHTML of Timetable = open Prelude in {
lin
MkTable cs ts =
ss ("<table>" ++ "<tr><td></td>"++ cs.s ++ </tr> ++ ts.s ++ "</table>") ;
NilTrain _ = ss [] ;
ConsTrain cs n t ts =
ss ("<tr>" ++ n.s ++ t.s ++ "</tr>") ;
OneCity c = ss ("<td>" ++ c ++ "</td>") ;
ConsCity c cs = ss (c.s ++ "to" ++ cs.s) ;
StopTime t = t ;
NoStop = ss ["no stop"] ;
LocTrain c s = cc2 c s ;
CityTrain c s cs t = ss (c.s ++ s.s ++ "," ++ t.s) ;
T i = prefixSS "at" i ;
N n = prefixSS "train" n ;
C s = s ;
}