library Basic/CharactersAndStrings version 1.0 %authors: T. Mossakowski, M. Roggenbach, L. Schroeder %date: 18 June 2002 %{ This library provides the datatypes characters and strings. The characters are defined to be the subset 0..255 of the natural numbers, and then constants for different representations (ASCII, decimal, octal, hexadecimal) are introduced. }% %string emptyString, __:@:__ from Basic/Numbers get Nat from Basic/StructuredDatatypes get List spec Char = %mono Nat then %mono %% characters are generated from natural numbers 0..255 type Char ::= chr(ord:Nat)? forall n:Nat; c:Char . def chr(n) <=> n <= 255 %(chr_dom)% . chr(ord(c))=c %(chr_ord_inverse)% %% definition of individual characters by decimal codes: ops '\000' : Char = chr(0); %(slash_000)% '\001' : Char = chr(1); %(slash_001)% '\002' : Char = chr(2); %(slash_002)% '\003' : Char = chr(3); %(slash_003)% '\004' : Char = chr(4); %(slash_004)% '\005' : Char = chr(5); %(slash_005)% '\006' : Char = chr(6); %(slash_006)% '\007' : Char = chr(7); %(slash_007)% '\008' : Char = chr(8); %(slash_008)% '\009' : Char = chr(9); %(slash_009)% '\010' : Char = chr(10); %(slash_010)% '\011' : Char = chr(11); %(slash_011)% '\012' : Char = chr(12); %(slash_012)% '\013' : Char = chr(13); %(slash_013)% '\014' : Char = chr(14); %(slash_014)% '\015' : Char = chr(15); %(slash_015)% '\016' : Char = chr(16); %(slash_016)% '\017' : Char = chr(17); %(slash_017)% '\018' : Char = chr(18); %(slash_018)% '\019' : Char = chr(19); %(slash_019)% '\020' : Char = chr(20); %(slash_020)% '\021' : Char = chr(21); %(slash_021)% '\022' : Char = chr(22); %(slash_022)% '\023' : Char = chr(23); %(slash_023)% '\024' : Char = chr(24); %(slash_024)% '\025' : Char = chr(25); %(slash_025)% '\026' : Char = chr(26); %(slash_026)% '\027' : Char = chr(27); %(slash_027)% '\028' : Char = chr(28); %(slash_028)% '\029' : Char = chr(29); %(slash_029)% '\030' : Char = chr(30); %(slash_030)% '\031' : Char = chr(31); %(slash_031)% '\032' : Char = chr(32); %(slash_032)% '\033' : Char = chr(33); %(slash_033)% '\034' : Char = chr(34); %(slash_034)% '\035' : Char = chr(35); %(slash_035)% '\036' : Char = chr(36); %(slash_036)% '\037' : Char = chr(37); %(slash_037)% '\038' : Char = chr(38); %(slash_038)% '\039' : Char = chr(39); %(slash_039)% '\040' : Char = chr(40); %(slash_040)% '\041' : Char = chr(41); %(slash_041)% '\042' : Char = chr(42); %(slash_042)% '\043' : Char = chr(43); %(slash_043)% '\044' : Char = chr(44); %(slash_044)% '\045' : Char = chr(45); %(slash_045)% '\046' : Char = chr(46); %(slash_046)% '\047' : Char = chr(47); %(slash_047)% '\048' : Char = chr(48); %(slash_048)% '\049' : Char = chr(49); %(slash_049)% '\050' : Char = chr(50); %(slash_050)% '\051' : Char = chr(51); %(slash_051)% '\052' : Char = chr(52); %(slash_052)% '\053' : Char = chr(53); %(slash_053)% '\054' : Char = chr(54); %(slash_054)% '\055' : Char = chr(55); %(slash_055)% '\056' : Char = chr(56); %(slash_056)% '\057' : Char = chr(57); %(slash_057)% '\058' : Char = chr(58); %(slash_058)% '\059' : Char = chr(59); %(slash_059)% '\060' : Char = chr(60); %(slash_060)% '\061' : Char = chr(61); %(slash_061)% '\062' : Char = chr(62); %(slash_062)% '\063' : Char = chr(63); %(slash_063)% '\064' : Char = chr(64); %(slash_064)% '\065' : Char = chr(65); %(slash_065)% '\066' : Char = chr(66); %(slash_066)% '\067' : Char = chr(67); %(slash_067)% '\068' : Char = chr(68); %(slash_068)% '\069' : Char = chr(69); %(slash_069)% '\070' : Char = chr(70); %(slash_070)% '\071' : Char = chr(71); %(slash_071)% '\072' : Char = chr(72); %(slash_072)% '\073' : Char = chr(73); %(slash_073)% '\074' : Char = chr(74); %(slash_074)% '\075' : Char = chr(75); %(slash_075)% '\076' : Char = chr(76); %(slash_076)% '\077' : Char = chr(77); %(slash_077)% '\078' : Char = chr(78); %(slash_078)% '\079' : Char = chr(79); %(slash_079)% '\080' : Char = chr(80); %(slash_080)% '\081' : Char = chr(81); %(slash_081)% '\082' : Char = chr(82); %(slash_082)% '\083' : Char = chr(83); %(slash_083)% '\084' : Char = chr(84); %(slash_084)% '\085' : Char = chr(85); %(slash_085)% '\086' : Char = chr(86); %(slash_086)% '\087' : Char = chr(87); %(slash_087)% '\088' : Char = chr(88); %(slash_088)% '\089' : Char = chr(89); %(slash_089)% '\090' : Char = chr(90); %(slash_090)% '\091' : Char = chr(91); %(slash_091)% '\092' : Char = chr(92); %(slash_092)% '\093' : Char = chr(93); %(slash_093)% '\094' : Char = chr(94); %(slash_094)% '\095' : Char = chr(95); %(slash_095)% '\096' : Char = chr(96); %(slash_096)% '\097' : Char = chr(97); %(slash_097)% '\098' : Char = chr(98); %(slash_098)% '\099' : Char = chr(99); %(slash_099)% '\100' : Char = chr(100); %(slash_100)% '\101' : Char = chr(101); %(slash_101)% '\102' : Char = chr(102); %(slash_102)% '\103' : Char = chr(103); %(slash_103)% '\104' : Char = chr(104); %(slash_104)% '\105' : Char = chr(105); %(slash_105)% '\106' : Char = chr(106); %(slash_106)% '\107' : Char = chr(107); %(slash_107)% '\108' : Char = chr(108); %(slash_108)% '\109' : Char = chr(109); %(slash_109)% '\110' : Char = chr(110); %(slash_110)% '\111' : Char = chr(111); %(slash_111)% '\112' : Char = chr(112); %(slash_112)% '\113' : Char = chr(113); %(slash_113)% '\114' : Char = chr(114); %(slash_114)% '\115' : Char = chr(115); %(slash_115)% '\116' : Char = chr(116); %(slash_116)% '\117' : Char = chr(117); %(slash_117)% '\118' : Char = chr(118); %(slash_118)% '\119' : Char = chr(119); %(slash_119)% '\120' : Char = chr(120); %(slash_120)% '\121' : Char = chr(121); %(slash_121)% '\122' : Char = chr(122); %(slash_122)% '\123' : Char = chr(123); %(slash_123)% '\124' : Char = chr(124); %(slash_124)% '\125' : Char = chr(125); %(slash_125)% '\126' : Char = chr(126); %(slash_126)% '\127' : Char = chr(127); %(slash_127)% '\128' : Char = chr(128); %(slash_128)% '\129' : Char = chr(129); %(slash_129)% '\130' : Char = chr(130); %(slash_130)% '\131' : Char = chr(131); %(slash_131)% '\132' : Char = chr(132); %(slash_132)% '\133' : Char = chr(133); %(slash_133)% '\134' : Char = chr(134); %(slash_134)% '\135' : Char = chr(135); %(slash_135)% '\136' : Char = chr(136); %(slash_136)% '\137' : Char = chr(137); %(slash_137)% '\138' : Char = chr(138); %(slash_138)% '\139' : Char = chr(139); %(slash_139)% '\140' : Char = chr(140); %(slash_140)% '\141' : Char = chr(141); %(slash_141)% '\142' : Char = chr(142); %(slash_142)% '\143' : Char = chr(143); %(slash_143)% '\144' : Char = chr(144); %(slash_144)% '\145' : Char = chr(145); %(slash_145)% '\146' : Char = chr(146); %(slash_146)% '\147' : Char = chr(147); %(slash_147)% '\148' : Char = chr(148); %(slash_148)% '\149' : Char = chr(149); %(slash_149)% '\150' : Char = chr(150); %(slash_150)% '\151' : Char = chr(151); %(slash_151)% '\152' : Char = chr(152); %(slash_152)% '\153' : Char = chr(153); %(slash_153)% '\154' : Char = chr(154); %(slash_154)% '\155' : Char = chr(155); %(slash_155)% '\156' : Char = chr(156); %(slash_156)% '\157' : Char = chr(157); %(slash_157)% '\158' : Char = chr(158); %(slash_158)% '\159' : Char = chr(159); %(slash_159)% '\160' : Char = chr(160); %(slash_160)% '\161' : Char = chr(161); %(slash_161)% '\162' : Char = chr(162); %(slash_162)% '\163' : Char = chr(163); %(slash_163)% '\164' : Char = chr(164); %(slash_164)% '\165' : Char = chr(165); %(slash_165)% '\166' : Char = chr(166); %(slash_166)% '\167' : Char = chr(167); %(slash_167)% '\168' : Char = chr(168); %(slash_168)% '\169' : Char = chr(169); %(slash_169)% '\170' : Char = chr(170); %(slash_170)% '\171' : Char = chr(171); %(slash_171)% '\172' : Char = chr(172); %(slash_172)% '\173' : Char = chr(173); %(slash_173)% '\174' : Char = chr(174); %(slash_174)% '\175' : Char = chr(175); %(slash_175)% '\176' : Char = chr(176); %(slash_176)% '\177' : Char = chr(177); %(slash_177)% '\178' : Char = chr(178); %(slash_178)% '\179' : Char = chr(179); %(slash_179)% '\180' : Char = chr(180); %(slash_180)% '\181' : Char = chr(181); %(slash_181)% '\182' : Char = chr(182); %(slash_182)% '\183' : Char = chr(183); %(slash_183)% '\184' : Char = chr(184); %(slash_184)% '\185' : Char = chr(185); %(slash_185)% '\186' : Char = chr(186); %(slash_186)% '\187' : Char = chr(187); %(slash_187)% '\188' : Char = chr(188); %(slash_188)% '\189' : Char = chr(189); %(slash_189)% '\190' : Char = chr(190); %(slash_190)% '\191' : Char = chr(191); %(slash_191)% '\192' : Char = chr(192); %(slash_192)% '\193' : Char = chr(193); %(slash_193)% '\194' : Char = chr(194); %(slash_194)% '\195' : Char = chr(195); %(slash_195)% '\196' : Char = chr(196); %(slash_196)% '\197' : Char = chr(197); %(slash_197)% '\198' : Char = chr(198); %(slash_198)% '\199' : Char = chr(199); %(slash_199)% '\200' : Char = chr(200); %(slash_200)% '\201' : Char = chr(201); %(slash_201)% '\202' : Char = chr(202); %(slash_202)% '\203' : Char = chr(203); %(slash_203)% '\204' : Char = chr(204); %(slash_204)% '\205' : Char = chr(205); %(slash_205)% '\206' : Char = chr(206); %(slash_206)% '\207' : Char = chr(207); %(slash_207)% '\208' : Char = chr(208); %(slash_208)% '\209' : Char = chr(209); %(slash_209)% '\210' : Char = chr(210); %(slash_210)% '\211' : Char = chr(211); %(slash_211)% '\212' : Char = chr(212); %(slash_212)% '\213' : Char = chr(213); %(slash_213)% '\214' : Char = chr(214); %(slash_214)% '\215' : Char = chr(215); %(slash_215)% '\216' : Char = chr(216); %(slash_216)% '\217' : Char = chr(217); %(slash_217)% '\218' : Char = chr(218); %(slash_218)% '\219' : Char = chr(219); %(slash_219)% '\220' : Char = chr(220); %(slash_220)% '\221' : Char = chr(221); %(slash_221)% '\222' : Char = chr(222); %(slash_222)% '\223' : Char = chr(223); %(slash_223)% '\224' : Char = chr(224); %(slash_224)% '\225' : Char = chr(225); %(slash_225)% '\226' : Char = chr(226); %(slash_226)% '\227' : Char = chr(227); %(slash_227)% '\228' : Char = chr(228); %(slash_228)% '\229' : Char = chr(229); %(slash_229)% '\230' : Char = chr(230); %(slash_230)% '\231' : Char = chr(231); %(slash_231)% '\232' : Char = chr(232); %(slash_232)% '\233' : Char = chr(233); %(slash_233)% '\234' : Char = chr(234); %(slash_234)% '\235' : Char = chr(235); %(slash_235)% '\236' : Char = chr(236); %(slash_236)% '\237' : Char = chr(237); %(slash_237)% '\238' : Char = chr(238); %(slash_238)% '\239' : Char = chr(239); %(slash_239)% '\240' : Char = chr(240); %(slash_240)% '\241' : Char = chr(241); %(slash_241)% '\242' : Char = chr(242); %(slash_242)% '\243' : Char = chr(243); %(slash_243)% '\244' : Char = chr(244); %(slash_244)% '\245' : Char = chr(245); %(slash_245)% '\246' : Char = chr(246); %(slash_246)% '\247' : Char = chr(247); %(slash_247)% '\248' : Char = chr(248); %(slash_248)% '\249' : Char = chr(249); %(slash_249)% '\250' : Char = chr(250); %(slash_250)% '\251' : Char = chr(251); %(slash_251)% '\252' : Char = chr(252); %(slash_252)% '\253' : Char = chr(253); %(slash_253)% '\254' : Char = chr(254); %(slash_254)% '\255' : Char = chr(255); %(slash_255)% %% definition of the printable characters %% This relies on the character names ops ' ' : Char = '\032'; %(printable_32)% '!' : Char = '\033'; %(printable_33)% '\"' : Char = '\034'; %(printable_34)% '#' : Char = '\035'; %(printable_35)% '$' : Char = '\036'; %(printable_36)% '%' : Char = '\037'; %(printable_37)% '&' : Char = '\038'; %(printable_38)% '\'' : Char = '\039'; %(printable_39)% '(' : Char = '\040'; %(printable_40)% ')' : Char = '\041'; %(printable_41)% '*' : Char = '\042'; %(printable_42)% '+' : Char = '\043'; %(printable_43)% ',' : Char = '\044'; %(printable_44)% '-' : Char = '\045'; %(printable_45)% '.' : Char = '\046'; %(printable_46)% '/' : Char = '\047'; %(printable_47)% '0' : Char = '\048'; %(printable_48)% '1' : Char = '\049'; %(printable_49)% '2' : Char = '\050'; %(printable_50)% '3' : Char = '\051'; %(printable_51)% '4' : Char = '\052'; %(printable_52)% '5' : Char = '\053'; %(printable_53)% '6' : Char = '\054'; %(printable_54)% '7' : Char = '\055'; %(printable_55)% '8' : Char = '\056'; %(printable_56)% '9' : Char = '\057'; %(printable_57)% ':' : Char = '\058'; %(printable_58)% ';' : Char = '\059'; %(printable_59)% '<' : Char = '\060'; %(printable_60)% '=' : Char = '\061'; %(printable_61)% '>' : Char = '\062'; %(printable_62)% '?' : Char = '\063'; %(printable_63)% '@' : Char = '\064'; %(printable_64)% 'A' : Char = '\065'; %(printable_65)% 'B' : Char = '\066'; %(printable_66)% 'C' : Char = '\067'; %(printable_67)% 'D' : Char = '\068'; %(printable_68)% 'E' : Char = '\069'; %(printable_69)% 'F' : Char = '\070'; %(printable_70)% 'G' : Char = '\071'; %(printable_71)% 'H' : Char = '\072'; %(printable_72)% 'I' : Char = '\073'; %(printable_73)% 'J' : Char = '\074'; %(printable_74)% 'K' : Char = '\075'; %(printable_75)% 'L' : Char = '\076'; %(printable_76)% 'M' : Char = '\077'; %(printable_77)% 'N' : Char = '\078'; %(printable_78)% 'O' : Char = '\079'; %(printable_79)% 'P' : Char = '\080'; %(printable_80)% 'Q' : Char = '\081'; %(printable_81)% 'R' : Char = '\082'; %(printable_82)% 'S' : Char = '\083'; %(printable_83)% 'T' : Char = '\084'; %(printable_84)% 'U' : Char = '\085'; %(printable_85)% 'V' : Char = '\086'; %(printable_86)% 'W' : Char = '\087'; %(printable_87)% 'X' : Char = '\088'; %(printable_88)% 'Y' : Char = '\089'; %(printable_89)% 'Z' : Char = '\090'; %(printable_90)% '[' : Char = '\091'; %(printable_91)% '\\' : Char = '\092'; %(printable_92)% ']' : Char = '\093'; %(printable_93)% '^' : Char = '\094'; %(printable_94)% '_' : Char = '\095'; %(printable_95)% '`' : Char = '\096'; %(printable_96)% 'a' : Char = '\097'; %(printable_97)% 'b' : Char = '\098'; %(printable_98)% 'c' : Char = '\099'; %(printable_99)% 'd' : Char = '\100' ; %(printable_100)% 'e' : Char = '\101' ; %(printable_101)% 'f' : Char = '\102' ; %(printable_102)% 'g' : Char = '\103' ; %(printable_103)% 'h' : Char = '\104' ; %(printable_104)% 'i' : Char = '\105' ; %(printable_105)% 'j' : Char = '\106' ; %(printable_106)% 'k' : Char = '\107' ; %(printable_107)% 'l' : Char = '\108' ; %(printable_108)% 'm' : Char = '\109' ; %(printable_109)% 'n' : Char = '\110' ; %(printable_110)% 'o' : Char = '\111' ; %(printable_111)% 'p' : Char = '\112' ; %(printable_112)% 'q' : Char = '\113' ; %(printable_113)% 'r' : Char = '\114' ; %(printable_114)% 's' : Char = '\115' ; %(printable_115)% 't' : Char = '\116' ; %(printable_116)% 'u' : Char = '\117' ; %(printable_117)% 'v' : Char = '\118' ; %(printable_118)% 'w' : Char = '\119' ; %(printable_119)% 'x' : Char = '\120' ; %(printable_120)% 'y' : Char = '\121' ; %(printable_121)% 'z' : Char = '\122' ; %(printable_122)% '{' : Char = '\123' ; %(printable_123)% '|' : Char = '\124' ; %(printable_124)% '}' : Char = '\125' ; %(printable_125)% '~' : Char = '\126' ; %(printable_126)% %% Iso-Latin-1 character number 160 is displayed as space, %% but internally is different from character 32 (space) ' ' : Char = '\160' ; %(printable_160)% '¡' : Char = '\161' ; %(printable_161)% '¢' : Char = '\162' ; %(printable_162)% '£' : Char = '\163' ; %(printable_163)% '¤' : Char = '\164' ; %(printable_164)% '¥' : Char = '\165' ; %(printable_165)% '¦' : Char = '\166' ; %(printable_166)% '§' : Char = '\167' ; %(printable_167)% '¨' : Char = '\168' ; %(printable_168)% '©' : Char = '\169' ; %(printable_169)% 'ª' : Char = '\170' ; %(printable_170)% '«' : Char = '\171' ; %(printable_171)% '¬' : Char = '\172' ; %(printable_172)% '­' : Char = '\173' ; %(printable_173)% '®' : Char = '\174' ; %(printable_174)% '¯' : Char = '\175' ; %(printable_175)% '°' : Char = '\176' ; %(printable_176)% '±' : Char = '\177' ; %(printable_177)% '²' : Char = '\178' ; %(printable_178)% '³' : Char = '\179' ; %(printable_179)% '´' : Char = '\180' ; %(printable_180)% 'µ' : Char = '\181' ; %(printable_181)% '¶' : Char = '\182' ; %(printable_182)% '·' : Char = '\183' ; %(printable_183)% '¸' : Char = '\184' ; %(printable_184)% '¹' : Char = '\185' ; %(printable_185)% 'º' : Char = '\186' ; %(printable_186)% '»' : Char = '\187' ; %(printable_187)% '¼' : Char = '\188' ; %(printable_188)% '½' : Char = '\189' ; %(printable_189)% '¾' : Char = '\190' ; %(printable_190)% '¿' : Char = '\191' ; %(printable_191)% 'À' : Char = '\192' ; %(printable_192)% 'Á' : Char = '\193' ; %(printable_193)% 'Â' : Char = '\194' ; %(printable_194)% 'Ã' : Char = '\195' ; %(printable_195)% 'Ä' : Char = '\196' ; %(printable_196)% 'Å' : Char = '\197' ; %(printable_197)% 'Æ' : Char = '\198' ; %(printable_198)% 'Ç' : Char = '\199' ; %(printable_199)% 'È' : Char = '\200' ; %(printable_200)% 'É' : Char = '\201' ; %(printable_201)% 'Ê' : Char = '\202' ; %(printable_202)% 'Ë' : Char = '\203' ; %(printable_203)% 'Ì' : Char = '\204' ; %(printable_204)% 'Í' : Char = '\205' ; %(printable_205)% 'Î' : Char = '\206' ; %(printable_206)% 'Ï' : Char = '\207' ; %(printable_207)% 'Ð' : Char = '\208' ; %(printable_208)% 'Ñ' : Char = '\209' ; %(printable_209)% 'Ò' : Char = '\210' ; %(printable_210)% 'Ó' : Char = '\211' ; %(printable_211)% 'Ô' : Char = '\212' ; %(printable_212)% 'Õ' : Char = '\213' ; %(printable_213)% 'Ö' : Char = '\214' ; %(printable_214)% '×' : Char = '\215' ; %(printable_215)% 'Ø' : Char = '\216' ; %(printable_216)% 'Ù' : Char = '\217' ; %(printable_217)% 'Ú' : Char = '\218' ; %(printable_218)% 'Û' : Char = '\219' ; %(printable_219)% 'Ü' : Char = '\220' ; %(printable_220)% 'Ý' : Char = '\221' ; %(printable_221)% 'Þ' : Char = '\222' ; %(printable_222)% 'ß' : Char = '\223' ; %(printable_223)% 'à' : Char = '\224' ; %(printable_224)% 'á' : Char = '\225' ; %(printable_225)% 'â' : Char = '\226' ; %(printable_226)% 'ã' : Char = '\227' ; %(printable_227)% 'ä' : Char = '\228' ; %(printable_228)% 'å' : Char = '\229' ; %(printable_229)% 'æ' : Char = '\230' ; %(printable_230)% 'ç' : Char = '\231' ; %(printable_231)% 'è' : Char = '\232' ; %(printable_232)% 'é' : Char = '\233' ; %(printable_233)% 'ê' : Char = '\234' ; %(printable_234)% 'ë' : Char = '\235' ; %(printable_235)% 'ì' : Char = '\236' ; %(printable_236)% 'í' : Char = '\237' ; %(printable_237)% 'î' : Char = '\238' ; %(printable_238)% 'ï' : Char = '\239' ; %(printable_239)% 'ð' : Char = '\240' ; %(printable_240)% 'ñ' : Char = '\241' ; %(printable_241)% 'ò' : Char = '\242' ; %(printable_242)% 'ó' : Char = '\243' ; %(printable_243)% 'ô' : Char = '\244' ; %(printable_244)% 'õ' : Char = '\245' ; %(printable_245)% 'ö' : Char = '\246' ; %(printable_246)% '÷' : Char = '\247' ; %(printable_247)% 'ø' : Char = '\248' ; %(printable_248)% 'ù' : Char = '\249' ; %(printable_249)% 'ú' : Char = '\250' ; %(printable_250)% 'û' : Char = '\251' ; %(printable_251)% 'ü' : Char = '\252' ; %(printable_252)% 'ý' : Char = '\253' ; %(printable_253)% 'þ' : Char = '\254' ; %(printable_254)% 'ÿ' : Char = '\255' ; %(printable_255)% preds isLetter(c:Char) <=> ( (ord('A') <= ord(c) /\ ord(c) <= ord('Z')) \/ (ord('a') <= ord(c) /\ ord(c) <= ord('z')) ); %(isLetter_def)% isDigit(c:Char) <=> ord('0') <= ord(c) /\ ord(c) <= ord('9'); %(isDigit_def)% isPrintable(c:Char) <=> ( (ord(' ') <= ord(c) /\ ord(c) <= ord('~') ) \/ (ord(' ') <= ord(c) /\ ord(c) <= ord('ÿ')) ) %(isPrintable_def)% %% definition of characters by octal codes, i.e. '\o ppp', %% where p in {0,1,...,7} : ops '\o000' : Char = '\000'; %(slash_o000)% '\o001' : Char = '\001'; %(slash_o001)% '\o002' : Char = '\002'; %(slash_o002)% '\o003' : Char = '\003'; %(slash_o003)% '\o004' : Char = '\004'; %(slash_o004)% '\o005' : Char = '\005'; %(slash_o005)% '\o006' : Char = '\006'; %(slash_o006)% '\o007' : Char = '\007'; %(slash_o007)% '\o010' : Char = '\008'; %(slash_o010)% '\o011' : Char = '\009'; %(slash_o011)% '\o012' : Char = '\010'; %(slash_o012)% '\o013' : Char = '\011'; %(slash_o013)% '\o014' : Char = '\012'; %(slash_o014)% '\o015' : Char = '\013'; %(slash_o015)% '\o016' : Char = '\014'; %(slash_o016)% '\o017' : Char = '\015'; %(slash_o017)% '\o020' : Char = '\016'; %(slash_o020)% '\o021' : Char = '\017'; %(slash_o021)% '\o022' : Char = '\018'; %(slash_o022)% '\o023' : Char = '\019'; %(slash_o023)% '\o024' : Char = '\020'; %(slash_o024)% '\o025' : Char = '\021'; %(slash_o025)% '\o026' : Char = '\022'; %(slash_o026)% '\o027' : Char = '\023'; %(slash_o027)% '\o030' : Char = '\024'; %(slash_o030)% '\o031' : Char = '\025'; %(slash_o031)% '\o032' : Char = '\026'; %(slash_o032)% '\o033' : Char = '\027'; %(slash_o033)% '\o034' : Char = '\028'; %(slash_o034)% '\o035' : Char = '\029'; %(slash_o035)% '\o036' : Char = '\030'; %(slash_o036)% '\o037' : Char = '\031'; %(slash_o037)% '\o040' : Char = '\032'; %(slash_o040)% '\o041' : Char = '\033'; %(slash_o041)% '\o042' : Char = '\034'; %(slash_o042)% '\o043' : Char = '\035'; %(slash_o043)% '\o044' : Char = '\036'; %(slash_o044)% '\o045' : Char = '\037'; %(slash_o045)% '\o046' : Char = '\038'; %(slash_o046)% '\o047' : Char = '\039'; %(slash_o047)% '\o050' : Char = '\040'; %(slash_o050)% '\o051' : Char = '\041'; %(slash_o051)% '\o052' : Char = '\042'; %(slash_o052)% '\o053' : Char = '\043'; %(slash_o053)% '\o054' : Char = '\044'; %(slash_o054)% '\o055' : Char = '\045'; %(slash_o055)% '\o056' : Char = '\046'; %(slash_o056)% '\o057' : Char = '\047'; %(slash_o057)% '\o060' : Char = '\048'; %(slash_o060)% '\o061' : Char = '\049'; %(slash_o061)% '\o062' : Char = '\050'; %(slash_o062)% '\o063' : Char = '\051'; %(slash_o063)% '\o064' : Char = '\052'; %(slash_o064)% '\o065' : Char = '\053'; %(slash_o065)% '\o066' : Char = '\054'; %(slash_o066)% '\o067' : Char = '\055'; %(slash_o067)% '\o070' : Char = '\056'; %(slash_o070)% '\o071' : Char = '\057'; %(slash_o071)% '\o072' : Char = '\058'; %(slash_o072)% '\o073' : Char = '\059'; %(slash_o073)% '\o074' : Char = '\060'; %(slash_o074)% '\o075' : Char = '\061'; %(slash_o075)% '\o076' : Char = '\062'; %(slash_o076)% '\o077' : Char = '\063'; %(slash_o077)% '\o100' : Char = '\064'; %(slash_o100)% '\o101' : Char = '\065'; %(slash_o101)% '\o102' : Char = '\066'; %(slash_o102)% '\o103' : Char = '\067'; %(slash_o103)% '\o104' : Char = '\068'; %(slash_o104)% '\o105' : Char = '\069'; %(slash_o105)% '\o106' : Char = '\070'; %(slash_o106)% '\o107' : Char = '\071'; %(slash_o107)% '\o110' : Char = '\072'; %(slash_o110)% '\o111' : Char = '\073'; %(slash_o111)% '\o112' : Char = '\074'; %(slash_o112)% '\o113' : Char = '\075'; %(slash_o113)% '\o114' : Char = '\076'; %(slash_o114)% '\o115' : Char = '\077'; %(slash_o115)% '\o116' : Char = '\078'; %(slash_o116)% '\o117' : Char = '\079'; %(slash_o117)% '\o120' : Char = '\080'; %(slash_o120)% '\o121' : Char = '\081'; %(slash_o121)% '\o122' : Char = '\082'; %(slash_o122)% '\o123' : Char = '\083'; %(slash_o123)% '\o124' : Char = '\084'; %(slash_o124)% '\o125' : Char = '\085'; %(slash_o125)% '\o126' : Char = '\086'; %(slash_o126)% '\o127' : Char = '\087'; %(slash_o127)% '\o130' : Char = '\088'; %(slash_o130)% '\o131' : Char = '\089'; %(slash_o131)% '\o132' : Char = '\090'; %(slash_o132)% '\o133' : Char = '\091'; %(slash_o133)% '\o134' : Char = '\092'; %(slash_o134)% '\o135' : Char = '\093'; %(slash_o135)% '\o136' : Char = '\094'; %(slash_o136)% '\o137' : Char = '\095'; %(slash_o137)% '\o140' : Char = '\096'; %(slash_o140)% '\o141' : Char = '\097'; %(slash_o141)% '\o142' : Char = '\098'; %(slash_o142)% '\o143' : Char = '\099'; %(slash_o143)% '\o144' : Char = '\100'; %(slash_o144)% '\o145' : Char = '\101'; %(slash_o145)% '\o146' : Char = '\102'; %(slash_o146)% '\o147' : Char = '\103'; %(slash_o147)% '\o150' : Char = '\104'; %(slash_o150)% '\o151' : Char = '\105'; %(slash_o151)% '\o152' : Char = '\106'; %(slash_o152)% '\o153' : Char = '\107'; %(slash_o153)% '\o154' : Char = '\108'; %(slash_o154)% '\o155' : Char = '\109'; %(slash_o155)% '\o156' : Char = '\110'; %(slash_o156)% '\o157' : Char = '\111'; %(slash_o157)% '\o160' : Char = '\112'; %(slash_o160)% '\o161' : Char = '\113'; %(slash_o161)% '\o162' : Char = '\114'; %(slash_o162)% '\o163' : Char = '\115'; %(slash_o163)% '\o164' : Char = '\116'; %(slash_o164)% '\o165' : Char = '\117'; %(slash_o165)% '\o166' : Char = '\118'; %(slash_o166)% '\o167' : Char = '\119'; %(slash_o167)% '\o170' : Char = '\120'; %(slash_o170)% '\o171' : Char = '\121'; %(slash_o171)% '\o172' : Char = '\122'; %(slash_o172)% '\o173' : Char = '\123'; %(slash_o173)% '\o174' : Char = '\124'; %(slash_o174)% '\o175' : Char = '\125'; %(slash_o175)% '\o176' : Char = '\126'; %(slash_o176)% '\o177' : Char = '\127'; %(slash_o177)% '\o200' : Char = '\128'; %(slash_o200)% '\o201' : Char = '\129'; %(slash_o201)% '\o202' : Char = '\130'; %(slash_o202)% '\o203' : Char = '\131'; %(slash_o203)% '\o204' : Char = '\132'; %(slash_o204)% '\o205' : Char = '\133'; %(slash_o205)% '\o206' : Char = '\134'; %(slash_o206)% '\o207' : Char = '\135'; %(slash_o207)% '\o210' : Char = '\136'; %(slash_o210)% '\o211' : Char = '\137'; %(slash_o211)% '\o212' : Char = '\138'; %(slash_o212)% '\o213' : Char = '\139'; %(slash_o213)% '\o214' : Char = '\140'; %(slash_o214)% '\o215' : Char = '\141'; %(slash_o215)% '\o216' : Char = '\142'; %(slash_o216)% '\o217' : Char = '\143'; %(slash_o217)% '\o220' : Char = '\144'; %(slash_o220)% '\o221' : Char = '\145'; %(slash_o221)% '\o222' : Char = '\146'; %(slash_o222)% '\o223' : Char = '\147'; %(slash_o223)% '\o224' : Char = '\148'; %(slash_o224)% '\o225' : Char = '\149'; %(slash_o225)% '\o226' : Char = '\150'; %(slash_o226)% '\o227' : Char = '\151'; %(slash_o227)% '\o230' : Char = '\152'; %(slash_o230)% '\o231' : Char = '\153'; %(slash_o231)% '\o232' : Char = '\154'; %(slash_o232)% '\o233' : Char = '\155'; %(slash_o233)% '\o234' : Char = '\156'; %(slash_o234)% '\o235' : Char = '\157'; %(slash_o235)% '\o236' : Char = '\158'; %(slash_o236)% '\o237' : Char = '\159'; %(slash_o237)% '\o240' : Char = '\160'; %(slash_o240)% '\o241' : Char = '\161'; %(slash_o241)% '\o242' : Char = '\162'; %(slash_o242)% '\o243' : Char = '\163'; %(slash_o243)% '\o244' : Char = '\164'; %(slash_o244)% '\o245' : Char = '\165'; %(slash_o245)% '\o246' : Char = '\166'; %(slash_o246)% '\o247' : Char = '\167'; %(slash_o247)% '\o250' : Char = '\168'; %(slash_o250)% '\o251' : Char = '\169'; %(slash_o251)% '\o252' : Char = '\170'; %(slash_o252)% '\o253' : Char = '\171'; %(slash_o253)% '\o254' : Char = '\172'; %(slash_o254)% '\o255' : Char = '\173'; %(slash_o255)% '\o256' : Char = '\174'; %(slash_o256)% '\o257' : Char = '\175'; %(slash_o257)% '\o260' : Char = '\176'; %(slash_o260)% '\o261' : Char = '\177'; %(slash_o261)% '\o262' : Char = '\178'; %(slash_o262)% '\o263' : Char = '\179'; %(slash_o263)% '\o264' : Char = '\180'; %(slash_o264)% '\o265' : Char = '\181'; %(slash_o265)% '\o266' : Char = '\182'; %(slash_o266)% '\o267' : Char = '\183'; %(slash_o267)% '\o270' : Char = '\184'; %(slash_o270)% '\o271' : Char = '\185'; %(slash_o271)% '\o272' : Char = '\186'; %(slash_o272)% '\o273' : Char = '\187'; %(slash_o273)% '\o274' : Char = '\188'; %(slash_o274)% '\o275' : Char = '\189'; %(slash_o275)% '\o276' : Char = '\190'; %(slash_o276)% '\o277' : Char = '\191'; %(slash_o277)% '\o300' : Char = '\192'; %(slash_o300)% '\o301' : Char = '\193'; %(slash_o301)% '\o302' : Char = '\194'; %(slash_o302)% '\o303' : Char = '\195'; %(slash_o303)% '\o304' : Char = '\196'; %(slash_o304)% '\o305' : Char = '\197'; %(slash_o305)% '\o306' : Char = '\198'; %(slash_o306)% '\o307' : Char = '\199'; %(slash_o307)% '\o310' : Char = '\200'; %(slash_o310)% '\o311' : Char = '\201'; %(slash_o311)% '\o312' : Char = '\202'; %(slash_o312)% '\o313' : Char = '\203'; %(slash_o313)% '\o314' : Char = '\204'; %(slash_o314)% '\o315' : Char = '\205'; %(slash_o315)% '\o316' : Char = '\206'; %(slash_o316)% '\o317' : Char = '\207'; %(slash_o317)% '\o320' : Char = '\208'; %(slash_o320)% '\o321' : Char = '\209'; %(slash_o321)% '\o322' : Char = '\210'; %(slash_o322)% '\o323' : Char = '\211'; %(slash_o323)% '\o324' : Char = '\212'; %(slash_o324)% '\o325' : Char = '\213'; %(slash_o325)% '\o326' : Char = '\214'; %(slash_o326)% '\o327' : Char = '\215'; %(slash_o327)% '\o330' : Char = '\216'; %(slash_o330)% '\o331' : Char = '\217'; %(slash_o331)% '\o332' : Char = '\218'; %(slash_o332)% '\o333' : Char = '\219'; %(slash_o333)% '\o334' : Char = '\220'; %(slash_o334)% '\o335' : Char = '\221'; %(slash_o335)% '\o336' : Char = '\222'; %(slash_o336)% '\o337' : Char = '\223'; %(slash_o337)% '\o340' : Char = '\224'; %(slash_o340)% '\o341' : Char = '\225'; %(slash_o341)% '\o342' : Char = '\226'; %(slash_o342)% '\o343' : Char = '\227'; %(slash_o343)% '\o344' : Char = '\228'; %(slash_o344)% '\o345' : Char = '\229'; %(slash_o345)% '\o346' : Char = '\230'; %(slash_o346)% '\o347' : Char = '\231'; %(slash_o347)% '\o350' : Char = '\232'; %(slash_o350)% '\o351' : Char = '\233'; %(slash_o351)% '\o352' : Char = '\234'; %(slash_o352)% '\o353' : Char = '\235'; %(slash_o353)% '\o354' : Char = '\236'; %(slash_o354)% '\o355' : Char = '\237'; %(slash_o355)% '\o356' : Char = '\238'; %(slash_o356)% '\o357' : Char = '\239'; %(slash_o357)% '\o360' : Char = '\240'; %(slash_o360)% '\o361' : Char = '\241'; %(slash_o361)% '\o362' : Char = '\242'; %(slash_o362)% '\o363' : Char = '\243'; %(slash_o363)% '\o364' : Char = '\244'; %(slash_o364)% '\o365' : Char = '\245'; %(slash_o365)% '\o366' : Char = '\246'; %(slash_o366)% '\o367' : Char = '\247'; %(slash_o367)% '\o370' : Char = '\248'; %(slash_o370)% '\o371' : Char = '\249'; %(slash_o371)% '\o372' : Char = '\250'; %(slash_o372)% '\o373' : Char = '\251'; %(slash_o373)% '\o374' : Char = '\252'; %(slash_o374)% '\o375' : Char = '\253'; %(slash_o375)% '\o376' : Char = '\254'; %(slash_o376)% '\o377' : Char = '\255'; %(slash_o377)% %% definition of characters by hexadecimal codes, i.e. '\xhh', %% where h in {0,1,..., F} : ops '\x00' : Char = '\000'; %(slash_x00)% '\x01' : Char = '\001'; %(slash_x01)% '\x02' : Char = '\002'; %(slash_x02)% '\x03' : Char = '\003'; %(slash_x03)% '\x04' : Char = '\004'; %(slash_x04)% '\x05' : Char = '\005'; %(slash_x05)% '\x06' : Char = '\006'; %(slash_x06)% '\x07' : Char = '\007'; %(slash_x07)% '\x08' : Char = '\008'; %(slash_x08)% '\x09' : Char = '\009'; %(slash_x09)% '\x0A' : Char = '\010'; %(slash_x0A)% '\x0B' : Char = '\011'; %(slash_x0B)% '\x0C' : Char = '\012'; %(slash_x0C)% '\x0D' : Char = '\013'; %(slash_x0D)% '\x0E' : Char = '\014'; %(slash_x0E)% '\x0F' : Char = '\015'; %(slash_x0F)% '\x10' : Char = '\016'; %(slash_x10)% '\x11' : Char = '\017'; %(slash_x11)% '\x12' : Char = '\018'; %(slash_x12)% '\x13' : Char = '\019'; %(slash_x13)% '\x14' : Char = '\020'; %(slash_x14)% '\x15' : Char = '\021'; %(slash_x15)% '\x16' : Char = '\022'; %(slash_x16)% '\x17' : Char = '\023'; %(slash_x17)% '\x18' : Char = '\024'; %(slash_x18)% '\x19' : Char = '\025'; %(slash_x19)% '\x1A' : Char = '\026'; %(slash_x1A)% '\x1B' : Char = '\027'; %(slash_x1B)% '\x1C' : Char = '\028'; %(slash_x1C)% '\x1D' : Char = '\029'; %(slash_x1D)% '\x1E' : Char = '\030'; %(slash_x1E)% '\x1F' : Char = '\031'; %(slash_x1F)% '\x20' : Char = '\032'; %(slash_x20)% '\x21' : Char = '\033'; %(slash_x21)% '\x22' : Char = '\034'; %(slash_x22)% '\x23' : Char = '\035'; %(slash_x23)% '\x24' : Char = '\036'; %(slash_x24)% '\x25' : Char = '\037'; %(slash_x25)% '\x26' : Char = '\038'; %(slash_x26)% '\x27' : Char = '\039'; %(slash_x27)% '\x28' : Char = '\040'; %(slash_x28)% '\x29' : Char = '\041'; %(slash_x29)% '\x2A' : Char = '\042'; %(slash_x2A)% '\x2B' : Char = '\043'; %(slash_x2B)% '\x2C' : Char = '\044'; %(slash_x2C)% '\x2D' : Char = '\045'; %(slash_x2D)% '\x2E' : Char = '\046'; %(slash_x2E)% '\x2F' : Char = '\047'; %(slash_x2F)% '\x30' : Char = '\048'; %(slash_x30)% '\x31' : Char = '\049'; %(slash_x31)% '\x32' : Char = '\050'; %(slash_x32)% '\x33' : Char = '\051'; %(slash_x33)% '\x34' : Char = '\052'; %(slash_x34)% '\x35' : Char = '\053'; %(slash_x35)% '\x36' : Char = '\054'; %(slash_x36)% '\x37' : Char = '\055'; %(slash_x37)% '\x38' : Char = '\056'; %(slash_x38)% '\x39' : Char = '\057'; %(slash_x39)% '\x3A' : Char = '\058'; %(slash_x3A)% '\x3B' : Char = '\059'; %(slash_x3B)% '\x3C' : Char = '\060'; %(slash_x3C)% '\x3D' : Char = '\061'; %(slash_x3D)% '\x3E' : Char = '\062'; %(slash_x3E)% '\x3F' : Char = '\063'; %(slash_x3F)% '\x40' : Char = '\064'; %(slash_x40)% '\x41' : Char = '\065'; %(slash_x41)% '\x42' : Char = '\066'; %(slash_x42)% '\x43' : Char = '\067'; %(slash_x43)% '\x44' : Char = '\068'; %(slash_x44)% '\x45' : Char = '\069'; %(slash_x45)% '\x46' : Char = '\070'; %(slash_x46)% '\x47' : Char = '\071'; %(slash_x47)% '\x48' : Char = '\072'; %(slash_x48)% '\x49' : Char = '\073'; %(slash_x49)% '\x4A' : Char = '\074'; %(slash_x4A)% '\x4B' : Char = '\075'; %(slash_x4B)% '\x4C' : Char = '\076'; %(slash_x4C)% '\x4D' : Char = '\077'; %(slash_x4D)% '\x4E' : Char = '\078'; %(slash_x4E)% '\x4F' : Char = '\079'; %(slash_x4F)% '\x50' : Char = '\080'; %(slash_x50)% '\x51' : Char = '\081'; %(slash_x51)% '\x52' : Char = '\082'; %(slash_x52)% '\x53' : Char = '\083'; %(slash_x53)% '\x54' : Char = '\084'; %(slash_x54)% '\x55' : Char = '\085'; %(slash_x55)% '\x56' : Char = '\086'; %(slash_x56)% '\x57' : Char = '\087'; %(slash_x57)% '\x58' : Char = '\088'; %(slash_x58)% '\x59' : Char = '\089'; %(slash_x59)% '\x5A' : Char = '\090'; %(slash_x5A)% '\x5B' : Char = '\091'; %(slash_x5B)% '\x5C' : Char = '\092'; %(slash_x5C)% '\x5D' : Char = '\093'; %(slash_x5D)% '\x5E' : Char = '\094'; %(slash_x5E)% '\x5F' : Char = '\095'; %(slash_x5F)% '\x60' : Char = '\096'; %(slash_x60)% '\x61' : Char = '\097'; %(slash_x61)% '\x62' : Char = '\098'; %(slash_x62)% '\x63' : Char = '\099'; %(slash_x63)% '\x64' : Char = '\100'; %(slash_x64)% '\x65' : Char = '\101'; %(slash_x65)% '\x66' : Char = '\102'; %(slash_x66)% '\x67' : Char = '\103'; %(slash_x67)% '\x68' : Char = '\104'; %(slash_x68)% '\x69' : Char = '\105'; %(slash_x69)% '\x6A' : Char = '\106'; %(slash_x6A)% '\x6B' : Char = '\107'; %(slash_x6B)% '\x6C' : Char = '\108'; %(slash_x6C)% '\x6D' : Char = '\109'; %(slash_x6D)% '\x6E' : Char = '\110'; %(slash_x6E)% '\x6F' : Char = '\111'; %(slash_x6F)% '\x70' : Char = '\112'; %(slash_x70)% '\x71' : Char = '\113'; %(slash_x71)% '\x72' : Char = '\114'; %(slash_x72)% '\x73' : Char = '\115'; %(slash_x73)% '\x74' : Char = '\116'; %(slash_x74)% '\x75' : Char = '\117'; %(slash_x75)% '\x76' : Char = '\118'; %(slash_x76)% '\x77' : Char = '\119'; %(slash_x77)% '\x78' : Char = '\120'; %(slash_x78)% '\x79' : Char = '\121'; %(slash_x79)% '\x7A' : Char = '\122'; %(slash_x7A)% '\x7B' : Char = '\123'; %(slash_x7B)% '\x7C' : Char = '\124'; %(slash_x7C)% '\x7D' : Char = '\125'; %(slash_x7D)% '\x7E' : Char = '\126'; %(slash_x7E)% '\x7F' : Char = '\127'; %(slash_x7F)% '\x80' : Char = '\128'; %(slash_x80)% '\x81' : Char = '\129'; %(slash_x81)% '\x82' : Char = '\130'; %(slash_x82)% '\x83' : Char = '\131'; %(slash_x83)% '\x84' : Char = '\132'; %(slash_x84)% '\x85' : Char = '\133'; %(slash_x85)% '\x86' : Char = '\134'; %(slash_x86)% '\x87' : Char = '\135'; %(slash_x87)% '\x88' : Char = '\136'; %(slash_x88)% '\x89' : Char = '\137'; %(slash_x89)% '\x8A' : Char = '\138'; %(slash_x8A)% '\x8B' : Char = '\139'; %(slash_x8B)% '\x8C' : Char = '\140'; %(slash_x8C)% '\x8D' : Char = '\141'; %(slash_x8D)% '\x8E' : Char = '\142'; %(slash_x8E)% '\x8F' : Char = '\143'; %(slash_x8F)% '\x90' : Char = '\144'; %(slash_x90)% '\x91' : Char = '\145'; %(slash_x91)% '\x92' : Char = '\146'; %(slash_x92)% '\x93' : Char = '\147'; %(slash_x93)% '\x94' : Char = '\148'; %(slash_x94)% '\x95' : Char = '\149'; %(slash_x95)% '\x96' : Char = '\150'; %(slash_x96)% '\x97' : Char = '\151'; %(slash_x97)% '\x98' : Char = '\152'; %(slash_x98)% '\x99' : Char = '\153'; %(slash_x99)% '\x9A' : Char = '\154'; %(slash_x9A)% '\x9B' : Char = '\155'; %(slash_x9B)% '\x9C' : Char = '\156'; %(slash_x9C)% '\x9D' : Char = '\157'; %(slash_x9D)% '\x9E' : Char = '\158'; %(slash_x9E)% '\x9F' : Char = '\159'; %(slash_x9F)% '\xA0' : Char = '\160'; %(slash_xA0)% '\xA1' : Char = '\161'; %(slash_xA1)% '\xA2' : Char = '\162'; %(slash_xA2)% '\xA3' : Char = '\163'; %(slash_xA3)% '\xA4' : Char = '\164'; %(slash_xA4)% '\xA5' : Char = '\165'; %(slash_xA5)% '\xA6' : Char = '\166'; %(slash_xA6)% '\xA7' : Char = '\167'; %(slash_xA7)% '\xA8' : Char = '\168'; %(slash_xA8)% '\xA9' : Char = '\169'; %(slash_xA9)% '\xAA' : Char = '\170'; %(slash_xAA)% '\xAB' : Char = '\171'; %(slash_xAB)% '\xAC' : Char = '\172'; %(slash_xAC)% '\xAD' : Char = '\173'; %(slash_xAD)% '\xAE' : Char = '\174'; %(slash_xAE)% '\xAF' : Char = '\175'; %(slash_xAF)% '\xB0' : Char = '\176'; %(slash_xB0)% '\xB1' : Char = '\177'; %(slash_xB1)% '\xB2' : Char = '\178'; %(slash_xB2)% '\xB3' : Char = '\179'; %(slash_xB3)% '\xB4' : Char = '\180'; %(slash_xB4)% '\xB5' : Char = '\181'; %(slash_xB5)% '\xB6' : Char = '\182'; %(slash_xB6)% '\xB7' : Char = '\183'; %(slash_xB7)% '\xB8' : Char = '\184'; %(slash_xB8)% '\xB9' : Char = '\185'; %(slash_xB9)% '\xBA' : Char = '\186'; %(slash_xBA)% '\xBB' : Char = '\187'; %(slash_xBB)% '\xBC' : Char = '\188'; %(slash_xBC)% '\xBD' : Char = '\189'; %(slash_xBD)% '\xBE' : Char = '\190'; %(slash_xBE)% '\xBF' : Char = '\191'; %(slash_xBF)% '\xC0' : Char = '\192'; %(slash_xC0)% '\xC1' : Char = '\193'; %(slash_xC1)% '\xC2' : Char = '\194'; %(slash_xC2)% '\xC3' : Char = '\195'; %(slash_xC3)% '\xC4' : Char = '\196'; %(slash_xC4)% '\xC5' : Char = '\197'; %(slash_xC5)% '\xC6' : Char = '\198'; %(slash_xC6)% '\xC7' : Char = '\199'; %(slash_xC7)% '\xC8' : Char = '\200'; %(slash_xC8)% '\xC9' : Char = '\201'; %(slash_xC9)% '\xCA' : Char = '\202'; %(slash_xCA)% '\xCB' : Char = '\203'; %(slash_xCB)% '\xCC' : Char = '\204'; %(slash_xCC)% '\xCD' : Char = '\205'; %(slash_xCD)% '\xCE' : Char = '\206'; %(slash_xCE)% '\xCF' : Char = '\207'; %(slash_xCF)% '\xD0' : Char = '\208'; %(slash_xD0)% '\xD1' : Char = '\209'; %(slash_xD1)% '\xD2' : Char = '\210'; %(slash_xD2)% '\xD3' : Char = '\211'; %(slash_xD3)% '\xD4' : Char = '\212'; %(slash_xD4)% '\xD5' : Char = '\213'; %(slash_xD5)% '\xD6' : Char = '\214'; %(slash_xD6)% '\xD7' : Char = '\215'; %(slash_xD7)% '\xD8' : Char = '\216'; %(slash_xD8)% '\xD9' : Char = '\217'; %(slash_xD9)% '\xDA' : Char = '\218'; %(slash_xDA)% '\xDB' : Char = '\219'; %(slash_xDB)% '\xDC' : Char = '\220'; %(slash_xDC)% '\xDD' : Char = '\221'; %(slash_xDD)% '\xDE' : Char = '\222'; %(slash_xDE)% '\xDF' : Char = '\223'; %(slash_xDF)% '\xE0' : Char = '\224'; %(slash_xE0)% '\xE1' : Char = '\225'; %(slash_xE1)% '\xE2' : Char = '\226'; %(slash_xE2)% '\xE3' : Char = '\227'; %(slash_xE3)% '\xE4' : Char = '\228'; %(slash_xE4)% '\xE5' : Char = '\229'; %(slash_xE5)% '\xE6' : Char = '\230'; %(slash_xE6)% '\xE7' : Char = '\231'; %(slash_xE7)% '\xE8' : Char = '\232'; %(slash_xE8)% '\xE9' : Char = '\233'; %(slash_xE9)% '\xEA' : Char = '\234'; %(slash_xEA)% '\xEB' : Char = '\235'; %(slash_xEB)% '\xEC' : Char = '\236'; %(slash_xEC)% '\xED' : Char = '\237'; %(slash_xED)% '\xEE' : Char = '\238'; %(slash_xEE)% '\xEF' : Char = '\239'; %(slash_xEF)% '\xF0' : Char = '\240'; %(slash_xF0)% '\xF1' : Char = '\241'; %(slash_xF1)% '\xF2' : Char = '\242'; %(slash_xF2)% '\xF3' : Char = '\243'; %(slash_xF3)% '\xF4' : Char = '\244'; %(slash_xF4)% '\xF5' : Char = '\245'; %(slash_xF5)% '\xF6' : Char = '\246'; %(slash_xF6)% '\xF7' : Char = '\247'; %(slash_xF7)% '\xF8' : Char = '\248'; %(slash_xF8)% '\xF9' : Char = '\249'; %(slash_xF9)% '\xFA' : Char = '\250'; %(slash_xFA)% '\xFB' : Char = '\251'; %(slash_xFB)% '\xFC' : Char = '\252'; %(slash_xFC)% '\xFD' : Char = '\253'; %(slash_xFD)% '\xFE' : Char = '\254'; %(slash_xFE)% '\xFF' : Char = '\255'; %(slash_xFF)% %% special characters: ops NUL:Char = '\000'; %(NUL_def)% SOH:Char = '\001'; %(SOH_def)% SYX:Char = '\002'; %(SYX_def)% ETX:Char = '\003'; %(ETX_def)% EOT:Char = '\004'; %(EOT_def)% ENQ:Char = '\005'; %(ENQ_def)% ACK:Char = '\006'; %(ACK_def)% BEL:Char = '\007'; %(BEL_def)% BS:Char = '\008'; %(BS_def)% HT:Char = '\009'; %(HT_def)% LF:Char = '\010'; %(LF_def)% VT:Char = '\011'; %(VT_def)% FF:Char = '\012'; %(FF_def)% CR:Char = '\013'; %(CR_def)% SO:Char = '\014'; %(SO_def)% SI:Char = '\015'; %(SI_def)% DLE:Char = '\016'; %(DLE_def)% DC1:Char = '\017'; %(DC1_def)% DC2:Char = '\018'; %(DC2_def)% DC3:Char = '\019'; %(DC3_def)% DC4:Char = '\020'; %(DC4_def)% NAK:Char = '\021'; %(NAK_def)% SYN:Char = '\022'; %(SYN_def)% ETB:Char = '\023'; %(ETB_def)% CAN:Char = '\024'; %(CAN_def)% EM:Char = '\025'; %(EM_def)% SUB:Char = '\026'; %(SUB_def)% ESC:Char = '\027'; %(ESC_def)% FS:Char = '\028'; %(FS_def)% GS:Char = '\029'; %(GS_def)% RS:Char = '\030'; %(RS_def)% US:Char = '\031'; %(US_def)% SP:Char = '\032'; %(SP_def)% DEL:Char = '\127'; %(DEL_def)% %% alternative names for special characters: ops NL:Char = LF; %(NL_def)% NP:Char = FF; %(NP_def)% %% character constants: ops '\n' : Char = NL; %(slash_n)% '\t' : Char = HT; %(slash_t)% '\v' : Char = VT; %(slash_v)% '\b' : Char = BS; %(slash_b)% '\r' : Char = CR; %(slash_r)% '\f' : Char = FF; %(slash_f)% '\a' : Char = BEL; %(slash_a)% '\?' : Char = '?'; %(slash_quest)% end spec String = %mono List [Char fit sort Elem |-> Char] with sort List[Char] |-> String, ops [] |-> emptyString, __::__ |-> __:@:__ end