1 {- 2 * Module for converting vts90 objects into strings and vica-versa 3 -} 4 5 module Core_database where 6 7 import Dcore 8 9 import Sub_Core1 10 11 import Sub_Core2 12 13 import Sub_Core3 14 15 import Sub_Core4 16 17 import Vtslib 18 19 import Core_datatype 20 21 data Constant_tag 22 = BOOL_TAG | TRUE_TAG | FALSE_TAG | UNIV_TAG deriving (Eq) 23 24 data Declaration_tag 25 = SYMBOL_DEC_TAG | AXIOM_DEC_TAG | DEF_TAG | DATA_TAG | 26 DECPAIR_TAG deriving (Eq) 27 28 data Term_tag 29 = SYM_TAG | APP_TAG | PAIR_TAG | BINDER_TAG | 30 CONSTANT_TAG | UNARY_TAG | BINARY_TAG | COND_TAG | 31 CONST_TAG | RECURSE_TAG deriving (Eq) 32 33 data Signature_tag 34 = EMPTY_TAG | EXTEND_TAG | COMBINE_TAG | SHARE_TAG deriving (Eq) 35 36 trm_tag_list 37 = [SYM_TAG, APP_TAG, PAIR_TAG, BINDER_TAG, 38 CONSTANT_TAG, UNARY_TAG, BINARY_TAG, COND_TAG, 39 CONST_TAG, RECURSE_TAG] 40 41 dec_tag_list 42 = [SYMBOL_DEC_TAG, AXIOM_DEC_TAG, DEF_TAG, DATA_TAG, DECPAIR_TAG] 43 44 sgn_tag_list 45 = [EMPTY_TAG,EXTEND_TAG,COMBINE_TAG,SHARE_TAG] 46 47 con_tag_list 48 = [BOOL_TAG, TRUE_TAG, FALSE_TAG, UNIV_TAG] 49 50 unary_tag_list = [Not] 51 52 binary_tag_list 53 = [Eq',And,Or,Issubtype] 54 55 binder_tag_list 56 = [Forall,Exists,Imp,Lambda,Pi,Sigma,Subtype,Choose] 57 58 59 60 {- 61 (* Functions for encoding tags *) 62 63 (* Each function is of type *) 64 (* ???_tag -> string *) 65 -} 66 67 68 encode_trm_tag tag = toEnum (encode tag trm_tag_list) 69 70 encode_dec_tag tag = toEnum (encode tag dec_tag_list) 71 72 encode_sgn_tag tag = toEnum (encode tag sgn_tag_list) 73 74 encode_unary_tag tag = toEnum (encode tag unary_tag_list) 75 76 encode_binary_tag tag = toEnum (encode tag binary_tag_list) 77 78 encode_binder_tag tag = toEnum (encode tag binder_tag_list) 79 80 encode_con_tag tag = toEnum (encode tag con_tag_list) 81 82 83 84 85 86 87 {- 88 (* Functions for decoding strings *) 89 90 (* Each function is of type *) 91 (* string -> ???_tag *) 92 -} 93 94 decode_trm_tag i = trm_tag_list !! i 95 96 decode_dec_tag i = dec_tag_list !! i 97 98 decode_sgn_tag i = sgn_tag_list !! i 99 100 decode_unary_tag i = unary_tag_list !! i 101 102 decode_binary_tag i = binary_tag_list !! i 103 104 decode_binder_tag i = binder_tag_list !! i 105 106 decode_constant_tag i = con_tag_list !! i 107 108 109 110 111 112 {- turn a term into a string -} 113 114 trm_to_str tm 115 = s1 ++ s2 ++ s3 116 where 117 s1 = trm_to_str' tm -- the term 118 s2 = trmL_to_str (other_typ tm) -- its extra types 119 s3 = attL_to_str (get_trm_att tm []) -- its attributes 120 121 122 123 124 125 126 {- turn a declaration into a string -} 127 128 dec_to_str dc 129 = s1 ++ s2 130 where 131 s1 = dec_to_str' dc -- the declaration 132 s2 = attL_to_str (get_dec_att dc) -- its attributes 133 134 135 136 137 138 {- turn a signature into a string -} 139 140 sgn_to_str sg 141 = s1 ++ s2 142 where 143 s1 = sgn_to_str' sg -- the signature 144 s2 = attL_to_str (get_sgn_att sg) -- its attributes 145 146 147 148 149 150 {- turn a term into a string ignoring its extra types and its attributes -} 151 152 trm_to_str' (Sym i j _ _) 153 = encode_trm_tag SYM_TAG : int_to_str i ++ int_to_str j 154 155 trm_to_str' (App tm1 tm2 _ _) 156 = encode_trm_tag APP_TAG : trm_to_str tm1 ++ trm_to_str tm2 157 158 trm_to_str' (Pair tm1 tm2 tm3 _ _) 159 = encode_trm_tag PAIR_TAG : trm_to_str tm1 ++ trm_to_str tm2 160 161 trm_to_str' (Binder b dc tm _ _) 162 = encode_trm_tag BINDER_TAG : [ encode_binder_tag b ] ++ 163 dec_to_str dc ++ trm_to_str tm 164 165 trm_to_str' (Constant c _ _) 166 = encode_trm_tag CONSTANT_TAG : constant_to_str c 167 168 trm_to_str' (Unary c tm _ _) 169 = encode_trm_tag UNARY_TAG : [encode_unary_tag c] ++ trm_to_str tm 170 171 trm_to_str' (Binary' c tm1 tm2 _ _) 172 = encode_trm_tag BINARY_TAG : [encode_binary_tag c] ++ 173 trm_to_str tm1 ++ trm_to_str tm2 174 175 trm_to_str' (Cond dc tm1 tm2 _ _) 176 = encode_trm_tag COND_TAG : dec_to_str dc ++ 177 trm_to_str tm1 ++ trm_to_str tm2 178 179 trm_to_str' (Const i j k _ _) 180 = encode_trm_tag CONST_TAG : int_to_str i ++ 181 int_to_str j ++ int_to_str k 182 183 trm_to_str' (Recurse tmL tm _ _) 184 = encode_trm_tag RECURSE_TAG : trmL_to_str tmL ++ trm_to_str tm 185 186 187 188 189 190 {- turn a declaration into a string ignoring its attributes -} 191 192 dec_to_str' (Symbol_dec tm _) 193 = encode_dec_tag SYMBOL_DEC_TAG : trm_to_str tm 194 195 dec_to_str' (Axiom_dec tm _) 196 = encode_dec_tag AXIOM_DEC_TAG : trm_to_str tm 197 198 dec_to_str' (Def tm1 tm2 _) 199 = encode_dec_tag DEF_TAG : trm_to_str tm1 ++ trm_to_str tm2 200 201 dec_to_str' (Data dcL tmLL _) 202 = encode_dec_tag DATA_TAG : decL_to_str dcL ++ trmLL_to_str tmLL 203 204 dec_to_str' (Decpair dc1 dc2 _) 205 = encode_dec_tag DECPAIR_TAG : dec_to_str dc1 ++ dec_to_str dc2 206 207 208 209 210 211 {- turn a signature into a string ignoring its attributes -} 212 213 sgn_to_str' (Empty _) 214 = [ encode_sgn_tag EMPTY_TAG ] 215 216 sgn_to_str' (Extend dc sg _) 217 = encode_sgn_tag EXTEND_TAG : dec_to_str dc ++ sgn_to_str sg 218 219 sgn_to_str' (Combine sg1 sg2 i _ _) 220 = encode_sgn_tag COMBINE_TAG : sgn_to_str sg1 ++ 221 sgn_to_str sg2 ++ int_to_str i 222 223 sgn_to_str' (Share sg i j k _ _) 224 = encode_sgn_tag SHARE_TAG : sgn_to_str sg ++ 225 int_to_str i ++ int_to_str j ++ int_to_str k 226 227 228 229 230 231 trmL_to_str tmL 232 = int_to_str (length tmL) ++ concat (map trm_to_str tmL) 233 234 trmLL_to_str tmLL 235 = int_to_str (length tmLL) ++ concat (map trmL_to_str tmLL) 236 237 trmLLL_to_str tmLLL 238 = int_to_str (length tmLLL) ++ concat (map trmLL_to_str tmLLL) 239 240 241 242 243 244 decL_to_str dcL 245 = int_to_str (length dcL) ++ concat (map dec_to_str dcL) 246 247 248 249 attL_to_str attL 250 = int_to_str (length attL) ++ concat (map att_to_str attL) 251 252 {- TEMP FUNCTION -} 253 254 att_to_str _ = "*** att_to_str NOT IMPLEMENTED -- core_database ***" 255 256 257 258 constant_to_str T = [ encode_con_tag TRUE_TAG ] 259 260 constant_to_str F = [ encode_con_tag FALSE_TAG ] 261 262 constant_to_str Bool' = [ encode_con_tag BOOL_TAG ] 263 264 constant_to_str (Univ i) = encode_con_tag UNIV_TAG : int_to_str i 265 266 267 268 269 270 271 str_to_trm s 272 = (foldr add_type (set_trm_att tm [] attL) tmL , s3) 273 where 274 (tm,s1) = s_to_trm' s 275 (tmL,s2) = s_to_trmL s1 276 (attL,s3) = str_to_attL s2 277 278 279 str_to_dec s 280 = (set_dec_att dc attL,s2) 281 where 282 (dc,s1) = s_to_dec' s 283 (attL,s2) = str_to_attL s1 284 285 286 str_to_sgn s 287 = (set_sgn_att sg attL,s2) 288 where 289 (sg,s1) = s_to_sgn' s 290 (attL,s2) = str_to_attL s1 291 292 293 s_to_trm' (ch:s1) 294 = case decode_trm_tag ch of 295 SYM_TAG 296 -> (Sym i j [] [] ,s3) 297 where 298 (i,s2) = str_to_int s1 299 (j,s3) = str_to_int s2 300 APP_TAG 301 -> (App tm1 tm2 [] [] ,s3) 302 where 303 (tm1,s2) = str_to_trm s1 304 (tm2,s3) = str_to_trm s2 305 PAIR_TAG 306 -> (Pair tm1 tm2 tm3 [] [] ,s4) 307 where 308 (tm1,s2) = str_to_trm s1 309 (tm2,s3) = str_to_trm s2 310 (tm3,s4) = str_to_trm s3 311 BINDER_TAG 312 -> (Binder b dc tm [] [] ,s4) 313 where 314 (b,s2) = str_to_binder s1 315 (dc,s3) = str_to_dec s2 316 (tm,s4) = str_to_trm s3 317 CONSTANT_TAG 318 -> (Constant c [] [] ,s2) 319 where 320 (c,s2) = str_to_constant s1 321 UNARY_TAG 322 -> (Unary c tm [] [] ,s3) 323 where 324 (c,s2) = str_to_unary s1 325 (tm,s3) = str_to_trm s2 326 BINARY_TAG 327 -> (Binary' c tm1 tm2 [] [] ,s4) 328 where 329 (c,s2) = str_to_binary s1 330 (tm1,s3) = str_to_trm s2 331 (tm2,s4) = str_to_trm s3 332 COND_TAG 333 -> (Cond dc tm1 tm2 [] [] ,s4) 334 where 335 (dc,s2) = str_to_dec s1 336 (tm1,s3) = str_to_trm s2 337 (tm2,s4) = str_to_trm s3 338 CONST_TAG 339 -> (Const i j k [] [] ,s4) 340 where 341 (i,s2) = str_to_int s1 342 (j,s3) = str_to_int s2 343 (k,s4) = str_to_int s3 344 RECURSE_TAG 345 -> (Recurse tmL tm [] [] ,s3) 346 where 347 (tmL,s2) = s_to_trmL s1 348 (tm,s3) = str_to_trm s2 349 350 351 352 353 354 s_to_dec' (ch:s1) 355 = case decode_dec_tag ch of 356 SYMBOL_DEC_TAG 357 -> (Symbol_dec tm [] ,s2) 358 where 359 (tm,s2) = str_to_trm s1 360 AXIOM_DEC_TAG 361 -> (Axiom_dec tm [] ,s2) 362 where 363 (tm,s2) = str_to_trm s1 364 DEF_TAG 365 -> (Def tm1 tm2 [] ,s3) 366 where 367 (tm1,s2) = str_to_trm s1 368 (tm2,s3) = str_to_trm s2 369 DATA_TAG 370 -> (Data dcL tmLL [] ,s3) 371 where 372 (dcL,s2) = s_to_decL s1 373 (tmLL,s3) = s_to_trmLL s2 374 DECPAIR_TAG 375 -> (Decpair dc1 dc2 [] ,s3) 376 where 377 (dc1,s2) = str_to_dec s1 378 (dc2,s3) = str_to_dec s2 379 380 381 382 383 384 s_to_sgn' (ch:s1) 385 = case decode_sgn_tag ch of 386 EMPTY_TAG 387 -> (Empty [], s1) 388 EXTEND_TAG 389 -> (Extend dc sg [] ,s3) 390 where 391 (dc,s2) = str_to_dec s1 392 (sg,s3) = str_to_sgn s2 393 COMBINE_TAG 394 -> (Combine sg1 sg2 i (sm2 ++ map (\ j -> j + i) sm1) [] ,s4) 395 where 396 (sg1,s2) = str_to_sgn s1 397 (sg2,s3) = str_to_sgn s2 398 (i,s4) = str_to_int s3 399 sm1 = get_share_map sg1 400 sm2 = get_share_map sg2 401 SHARE_TAG 402 -> (Share sg i j k (addequivL i j k sm) [] ,s5) 403 where 404 (sg,s2) = str_to_sgn s1 405 (i,s3) = str_to_int s2 406 (j,s4) = str_to_int s3 407 (k,s5) = str_to_int s4 408 sm = get_share_map sg 409 410 411 412 413 414 415 s_to_trmL s = str_to_list str_to_trm s 416 417 418 s_to_trmLL s = str_to_list s_to_trmL s 419 420 421 s_to_trmLLL s = str_to_list s_to_trmLL s 422 423 424 s_to_decL s = str_to_list str_to_dec s 425 426 427 str_to_attL s = str_to_list str_to_att s 428 429 430 str_to_binder (ch:s1) 431 = (decode_binder_tag ch,s1) 432 433 434 str_to_unary (ch:s1) 435 = (decode_unary_tag ch,s1) 436 437 438 str_to_binary :: [Int] -> (Binary_conn, [Int]) 439 440 str_to_binary (ch:s1) 441 = (decode_binary_tag ch,s1) 442 443 444 str_to_constant (ch:s1) 445 = case decode_constant_tag ch of 446 BOOL_TAG -> (Bool',s1) 447 TRUE_TAG -> (T,s1) 448 FALSE_TAG -> (F,s1) 449 UNIV_TAG -> (Univ i,s2) 450 where 451 (i,s2) = str_to_int s1 452 453 {- 454 temp function 455 -} 456 457 str_to_att ( a : x) = ( ( Name_Style , Symbol_Name ( Name [ toEnum a ]) ) , x )