1***( 2 3 This file is part of the Maude 2 interpreter. 4 5 Copyright 1997-2014 SRI International, Menlo Park, CA 94025, USA. 6 7 This program is free software; you can redistribute it and/or modify 8 it under the terms of the GNU General Public License as published by 9 the Free Software Foundation; either version 2 of the License, or 10 (at your option) any later version. 11 12 This program is distributed in the hope that it will be useful, 13 but WITHOUT ANY WARRANTY; without even the implied warranty of 14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 15 GNU General Public License for more details. 16 17 You should have received a copy of the GNU General Public License 18 along with this program; if not, write to the Free Software 19 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA. 20 21) 22 23*** 24*** Maude interpreter standard prelude. 25*** Version alpha109 26*** 27*** Some of the overall structure is taken from the OBJ3 28*** interpreter standard prelude. 29*** 30 31set include BOOL off . 32 33fmod TRUTH-VALUE is 34 sort Bool . 35 op true : -> Bool [ctor special (id-hook SystemTrue)] . 36 op false : -> Bool [ctor special (id-hook SystemFalse)] . 37endfm 38 39fmod BOOL-OPS is 40 protecting TRUTH-VALUE . 41 op _and_ : Bool Bool -> Bool [assoc comm prec 55] . 42 op _or_ : Bool Bool -> Bool [assoc comm prec 59] . 43 op _xor_ : Bool Bool -> Bool [assoc comm prec 57] . 44 op not_ : Bool -> Bool [prec 53] . 45 op _implies_ : Bool Bool -> Bool [gather (e E) prec 61] . 46 vars A B C : Bool . 47 eq true and A = A . 48 eq false and A = false . 49 eq A and A = A . 50 eq false xor A = A . 51 eq A xor A = false . 52 eq A and (B xor C) = A and B xor A and C . 53 eq not A = A xor true . 54 eq A or B = A and B xor A xor B . 55 eq A implies B = not(A xor A and B) . 56endfm 57 58fmod TRUTH is 59 protecting TRUTH-VALUE . 60 op if_then_else_fi : Bool Universal Universal -> Universal 61 [poly (2 3 0) 62 special (id-hook BranchSymbol 63 term-hook 1 (true) 64 term-hook 2 (false))] . 65 66 op _==_ : Universal Universal -> Bool 67 [prec 51 poly (1 2) 68 special (id-hook EqualitySymbol 69 term-hook equalTerm (true) 70 term-hook notEqualTerm (false))] . 71 72 op _=/=_ : Universal Universal -> Bool 73 [prec 51 poly (1 2) 74 special (id-hook EqualitySymbol 75 term-hook equalTerm (false) 76 term-hook notEqualTerm (true))] . 77endfm 78 79fmod BOOL is 80 protecting BOOL-OPS . 81 protecting TRUTH . 82endfm 83 84fmod EXT-BOOL is 85 protecting BOOL . 86 op _and-then_ : Bool Bool -> Bool [strat (1 0) gather (e E) prec 55] . 87 op _or-else_ : Bool Bool -> Bool [strat (1 0) gather (e E) prec 59] . 88 var B : [Bool] . 89 eq true and-then B = B . 90 eq false and-then B = false . 91 eq true or-else B = true . 92 eq false or-else B = B . 93endfm 94 95*** 96*** Builtin data types. 97*** 98 99fmod NAT is 100 protecting BOOL . 101 sorts Zero NzNat Nat . 102 subsort Zero NzNat < Nat . 103 op 0 : -> Zero [ctor] . 104 105 op s_ : Nat -> NzNat 106 [ctor iter 107 special (id-hook SuccSymbol 108 term-hook zeroTerm (0))] . 109 110 op _+_ : NzNat Nat -> NzNat 111 [assoc comm prec 33 112 special (id-hook ACU_NumberOpSymbol (+) 113 op-hook succSymbol (s_ : Nat ~> NzNat))] . 114 op _+_ : Nat Nat -> Nat [ditto] . 115 116 op sd : Nat Nat -> Nat 117 [comm 118 special (id-hook CUI_NumberOpSymbol (sd) 119 op-hook succSymbol (s_ : Nat ~> NzNat))] . 120 121 op _*_ : NzNat NzNat -> NzNat 122 [assoc comm prec 31 123 special (id-hook ACU_NumberOpSymbol (*) 124 op-hook succSymbol (s_ : Nat ~> NzNat))] . 125 op _*_ : Nat Nat -> Nat [ditto] . 126 127 op _quo_ : Nat NzNat -> Nat 128 [prec 31 gather (E e) 129 special (id-hook NumberOpSymbol (quo) 130 op-hook succSymbol (s_ : Nat ~> NzNat))] . 131 132 op _rem_ : Nat NzNat -> Nat 133 [prec 31 gather (E e) 134 special (id-hook NumberOpSymbol (rem) 135 op-hook succSymbol (s_ : Nat ~> NzNat))] . 136 137 op _^_ : Nat Nat -> Nat 138 [prec 29 gather (E e) 139 special (id-hook NumberOpSymbol (^) 140 op-hook succSymbol (s_ : Nat ~> NzNat))] . 141 op _^_ : NzNat Nat -> NzNat [ditto] . 142 143 op modExp : Nat Nat NzNat ~> Nat 144 [special (id-hook NumberOpSymbol (modExp) 145 op-hook succSymbol (s_ : Nat ~> NzNat))] . 146 147 op gcd : NzNat Nat -> NzNat 148 [assoc comm 149 special (id-hook ACU_NumberOpSymbol (gcd) 150 op-hook succSymbol (s_ : Nat ~> NzNat))] . 151 op gcd : Nat Nat -> Nat [ditto] . 152 153 op lcm : NzNat NzNat -> NzNat 154 [assoc comm 155 special (id-hook ACU_NumberOpSymbol (lcm) 156 op-hook succSymbol (s_ : Nat ~> NzNat))] . 157 op lcm : Nat Nat -> Nat [ditto] . 158 159 op min : NzNat NzNat -> NzNat 160 [assoc comm 161 special (id-hook ACU_NumberOpSymbol (min) 162 op-hook succSymbol (s_ : Nat ~> NzNat))] . 163 op min : Nat Nat -> Nat [ditto] . 164 165 op max : NzNat Nat -> NzNat 166 [assoc comm 167 special (id-hook ACU_NumberOpSymbol (max) 168 op-hook succSymbol (s_ : Nat ~> NzNat))] . 169 op max : Nat Nat -> Nat [ditto] . 170 171 op _xor_ : Nat Nat -> Nat 172 [assoc comm prec 55 173 special (id-hook ACU_NumberOpSymbol (xor) 174 op-hook succSymbol (s_ : Nat ~> NzNat))] . 175 176 op _&_ : Nat Nat -> Nat 177 [assoc comm prec 53 178 special (id-hook ACU_NumberOpSymbol (&) 179 op-hook succSymbol (s_ : Nat ~> NzNat))] . 180 181 op _|_ : NzNat Nat -> NzNat 182 [assoc comm prec 57 183 special (id-hook ACU_NumberOpSymbol (|) 184 op-hook succSymbol (s_ : Nat ~> NzNat))] . 185 op _|_ : Nat Nat -> Nat [ditto] . 186 187 op _>>_ : Nat Nat -> Nat 188 [prec 35 gather (E e) 189 special (id-hook NumberOpSymbol (>>) 190 op-hook succSymbol (s_ : Nat ~> NzNat))] . 191 192 op _<<_ : Nat Nat -> Nat 193 [prec 35 gather (E e) 194 special (id-hook NumberOpSymbol (<<) 195 op-hook succSymbol (s_ : Nat ~> NzNat))] . 196 197 op _<_ : Nat Nat -> Bool 198 [prec 37 199 special (id-hook NumberOpSymbol (<) 200 op-hook succSymbol (s_ : Nat ~> NzNat) 201 term-hook trueTerm (true) 202 term-hook falseTerm (false))] . 203 204 op _<=_ : Nat Nat -> Bool 205 [prec 37 206 special (id-hook NumberOpSymbol (<=) 207 op-hook succSymbol (s_ : Nat ~> NzNat) 208 term-hook trueTerm (true) 209 term-hook falseTerm (false))] . 210 211 op _>_ : Nat Nat -> Bool 212 [prec 37 213 special (id-hook NumberOpSymbol (>) 214 op-hook succSymbol (s_ : Nat ~> NzNat) 215 term-hook trueTerm (true) 216 term-hook falseTerm (false))] . 217 218 op _>=_ : Nat Nat -> Bool 219 [prec 37 220 special (id-hook NumberOpSymbol (>=) 221 op-hook succSymbol (s_ : Nat ~> NzNat) 222 term-hook trueTerm (true) 223 term-hook falseTerm (false))] . 224 225 op _divides_ : NzNat Nat -> Bool 226 [prec 51 227 special (id-hook NumberOpSymbol (divides) 228 op-hook succSymbol (s_ : Nat ~> NzNat) 229 term-hook trueTerm (true) 230 term-hook falseTerm (false))] . 231endfm 232 233fmod INT is 234 protecting NAT . 235 sorts NzInt Int . 236 subsorts NzNat < NzInt Nat < Int . 237 238 op -_ : NzNat -> NzInt 239 [ctor 240 special (id-hook MinusSymbol 241 op-hook succSymbol (s_ : Nat ~> NzNat) 242 op-hook minusSymbol (-_ : NzNat ~> Int))] . 243 op -_ : NzInt -> NzInt [ditto] . 244 op -_ : Int -> Int [ditto] . 245 246 op _+_ : Int Int -> Int 247 [assoc comm prec 33 248 special (id-hook ACU_NumberOpSymbol (+) 249 op-hook succSymbol (s_ : Nat ~> NzNat) 250 op-hook minusSymbol (-_ : NzNat ~> Int))] . 251 252 op _-_ : Int Int -> Int 253 [prec 33 gather (E e) 254 special (id-hook NumberOpSymbol (-) 255 op-hook succSymbol (s_ : Nat ~> NzNat) 256 op-hook minusSymbol (-_ : NzNat ~> Int))] . 257 258 op _*_ : NzInt NzInt -> NzInt 259 [assoc comm prec 31 260 special (id-hook ACU_NumberOpSymbol (*) 261 op-hook succSymbol (s_ : Nat ~> NzNat) 262 op-hook minusSymbol (-_ : NzNat ~> Int))] . 263 op _*_ : Int Int -> Int [ditto] . 264 265 op _quo_ : Int NzInt -> Int 266 [prec 31 gather (E e) 267 special (id-hook NumberOpSymbol (quo) 268 op-hook succSymbol (s_ : Nat ~> NzNat) 269 op-hook minusSymbol (-_ : NzNat ~> Int))] . 270 271 op _rem_ : Int NzInt -> Int 272 [prec 31 gather (E e) 273 special (id-hook NumberOpSymbol (rem) 274 op-hook succSymbol (s_ : Nat ~> NzNat) 275 op-hook minusSymbol (-_ : NzNat ~> Int))] . 276 277 op _^_ : Int Nat -> Int 278 [prec 29 gather (E e) 279 special (id-hook NumberOpSymbol (^) 280 op-hook succSymbol (s_ : Nat ~> NzNat) 281 op-hook minusSymbol (-_ : NzNat ~> Int))] . 282 op _^_ : NzInt Nat -> NzInt [ditto] . 283 284 op abs : NzInt -> NzNat 285 [special (id-hook NumberOpSymbol (abs) 286 op-hook succSymbol (s_ : Nat ~> NzNat) 287 op-hook minusSymbol (-_ : NzNat ~> Int))] . 288 op abs : Int -> Nat [ditto] . 289 290 op gcd : NzInt Int -> NzNat 291 [assoc comm 292 special (id-hook ACU_NumberOpSymbol (gcd) 293 op-hook succSymbol (s_ : Nat ~> NzNat) 294 op-hook minusSymbol (-_ : NzNat ~> Int))] . 295 op gcd : Int Int -> Nat [ditto] . 296 297 op lcm : NzInt NzInt -> NzNat 298 [assoc comm 299 special (id-hook ACU_NumberOpSymbol (lcm) 300 op-hook succSymbol (s_ : Nat ~> NzNat) 301 op-hook minusSymbol (-_ : NzNat ~> Int))] . 302 op lcm : Int Int -> Nat [ditto] . 303 304 op min : NzInt NzInt -> NzInt 305 [assoc comm 306 special (id-hook ACU_NumberOpSymbol (min) 307 op-hook succSymbol (s_ : Nat ~> NzNat) 308 op-hook minusSymbol (-_ : NzNat ~> Int))] . 309 op min : Int Int -> Int [ditto] . 310 311 op max : NzInt NzInt -> NzInt 312 [assoc comm 313 special (id-hook ACU_NumberOpSymbol (max) 314 op-hook succSymbol (s_ : Nat ~> NzNat) 315 op-hook minusSymbol (-_ : NzNat ~> Int))] . 316 op max : Int Int -> Int [ditto] . 317 op max : NzNat Int -> NzNat [ditto] . 318 op max : Nat Int -> Nat [ditto] . 319 320 op ~_ : Int -> Int 321 [special (id-hook NumberOpSymbol (~) 322 op-hook succSymbol (s_ : Nat ~> NzNat) 323 op-hook minusSymbol (-_ : NzNat ~> Int))] . 324 325 op _xor_ : Int Int -> Int 326 [assoc comm prec 55 327 special (id-hook ACU_NumberOpSymbol (xor) 328 op-hook succSymbol (s_ : Nat ~> NzNat) 329 op-hook minusSymbol (-_ : NzNat ~> Int))] . 330 331 op _&_ : Nat Int -> Nat 332 [assoc comm prec 53 333 special (id-hook ACU_NumberOpSymbol (&) 334 op-hook succSymbol (s_ : Nat ~> NzNat) 335 op-hook minusSymbol (-_ : NzNat ~> Int))] . 336 op _&_ : Int Int -> Int [ditto] . 337 338 op _|_ : NzInt Int -> NzInt 339 [assoc comm prec 57 340 special (id-hook ACU_NumberOpSymbol (|) 341 op-hook succSymbol (s_ : Nat ~> NzNat) 342 op-hook minusSymbol (-_ : NzNat ~> Int))] . 343 op _|_ : Int Int -> Int [ditto] . 344 345 op _>>_ : Int Nat -> Int 346 [prec 35 gather (E e) 347 special (id-hook NumberOpSymbol (>>) 348 op-hook succSymbol (s_ : Nat ~> NzNat) 349 op-hook minusSymbol (-_ : NzNat ~> Int))] . 350 351 op _<<_ : Int Nat -> Int 352 [prec 35 gather (E e) 353 special (id-hook NumberOpSymbol (<<) 354 op-hook succSymbol (s_ : Nat ~> NzNat) 355 op-hook minusSymbol (-_ : NzNat ~> Int))] . 356 357 op _<_ : Int Int -> Bool 358 [prec 37 359 special (id-hook NumberOpSymbol (<) 360 op-hook succSymbol (s_ : Nat ~> NzNat) 361 op-hook minusSymbol (-_ : NzNat ~> Int) 362 term-hook trueTerm (true) 363 term-hook falseTerm (false))] . 364 365 op _<=_ : Int Int -> Bool 366 [prec 37 367 special (id-hook NumberOpSymbol (<=) 368 op-hook succSymbol (s_ : Nat ~> NzNat) 369 op-hook minusSymbol (-_ : NzNat ~> Int) 370 term-hook trueTerm (true) 371 term-hook falseTerm (false))] . 372 373 op _>_ : Int Int -> Bool 374 [prec 37 375 special (id-hook NumberOpSymbol (>) 376 op-hook succSymbol (s_ : Nat ~> NzNat) 377 op-hook minusSymbol (-_ : NzNat ~> Int) 378 term-hook trueTerm (true) 379 term-hook falseTerm (false))] . 380 381 op _>=_ : Int Int -> Bool 382 [prec 37 383 special (id-hook NumberOpSymbol (>=) 384 op-hook succSymbol (s_ : Nat ~> NzNat) 385 op-hook minusSymbol (-_ : NzNat ~> Int) 386 term-hook trueTerm (true) 387 term-hook falseTerm (false))] . 388 389 op _divides_ : NzInt Int -> Bool 390 [prec 51 391 special (id-hook NumberOpSymbol (divides) 392 op-hook succSymbol (s_ : Nat ~> NzNat) 393 op-hook minusSymbol (-_ : NzNat ~> Int) 394 term-hook trueTerm (true) 395 term-hook falseTerm (false))] . 396endfm 397 398fmod RAT is 399 protecting INT . 400 sorts PosRat NzRat Rat . 401 subsorts NzInt < NzRat Int < Rat . 402 subsorts NzNat < PosRat < NzRat . 403 404 op _/_ : NzInt NzNat -> NzRat 405 [ctor prec 31 gather (E e) 406 special (id-hook DivisionSymbol 407 op-hook succSymbol (s_ : Nat ~> NzNat) 408 op-hook minusSymbol (-_ : NzNat ~> Int))] . 409 410 var I J : NzInt . 411 var N M : NzNat . 412 var K : Int . 413 var Z : Nat . 414 var Q : NzRat . 415 var R : Rat . 416 417 op _/_ : NzNat NzNat -> PosRat [ctor ditto] . 418 op _/_ : PosRat PosRat -> PosRat [ditto] . 419 op _/_ : NzRat NzRat -> NzRat [ditto] . 420 op _/_ : Rat NzRat -> Rat [ditto] . 421 eq 0 / Q = 0 . 422 eq I / - N = - I / N . 423 eq (I / N) / (J / M) = (I * M) / (J * N) . 424 eq (I / N) / J = I / (J * N) . 425 eq I / (J / M) = (I * M) / J . 426 427 op -_ : NzRat -> NzRat [ditto] . 428 op -_ : Rat -> Rat [ditto] . 429 eq - (I / N) = - I / N . 430 431 op _+_ : PosRat PosRat -> PosRat [ditto] . 432 op _+_ : PosRat Nat -> PosRat [ditto] . 433 op _+_ : Rat Rat -> Rat [ditto] . 434 eq I / N + J / M = (I * M + J * N) / (N * M) . 435 eq I / N + K = (I + K * N) / N . 436 437 op _-_ : Rat Rat -> Rat [ditto] . 438 eq I / N - J / M = (I * M - J * N) / (N * M) . 439 eq I / N - K = (I - K * N) / N . 440 eq K - J / M = (K * M - J ) / M . 441 442 op _*_ : PosRat PosRat -> PosRat [ditto] . 443 op _*_ : NzRat NzRat -> NzRat [ditto] . 444 op _*_ : Rat Rat -> Rat [ditto] . 445 eq Q * 0 = 0 . 446 eq (I / N) * (J / M) = (I * J) / (N * M). 447 eq (I / N) * K = (I * K) / N . 448 449 op _quo_ : PosRat PosRat -> Nat [ditto] . 450 op _quo_ : Rat NzRat -> Int [ditto] . 451 eq (I / N) quo Q = I quo (N * Q) . 452 eq K quo (J / M) = (K * M) quo J . 453 454 op _rem_ : Rat NzRat -> Rat [ditto] . 455 eq (I / N) rem (J / M) = ((I * M) rem (J * N)) / (N * M) . 456 eq K rem (J / M) = ((K * M) rem J) / M . 457 eq (I / N) rem J = (I rem (J * N)) / N . 458 459 op _^_ : PosRat Nat -> PosRat [ditto] . 460 op _^_ : NzRat Nat -> NzRat [ditto] . 461 op _^_ : Rat Nat -> Rat [ditto] . 462 eq (I / N) ^ Z = (I ^ Z) / (N ^ Z) . 463 464 op abs : NzRat -> PosRat [ditto] . 465 op abs : Rat -> Rat [ditto] . 466 eq abs(I / N) = abs(I) / N . 467 468 op gcd : NzRat Rat -> PosRat [ditto] . 469 op gcd : Rat Rat -> Rat [ditto] . 470 eq gcd(I / N, R) = gcd(I, N * R) / N . 471 472 op lcm : NzRat NzRat -> PosRat [ditto] . 473 op lcm : Rat Rat -> Rat [ditto] . 474 eq lcm(I / N, R) = lcm(I, N * R) / N . 475 476 op min : PosRat PosRat -> PosRat [ditto] . 477 op min : NzRat NzRat -> NzRat [ditto] . 478 op min : Rat Rat -> Rat [ditto] . 479 eq min(I / N, R) = min(I, N * R) / N . 480 481 op max : PosRat Rat -> PosRat [ditto] . 482 op max : NzRat NzRat -> NzRat [ditto] . 483 op max : Rat Rat -> Rat [ditto] . 484 eq max(I / N, R) = max(I, N * R) / N . 485 486 op _<_ : Rat Rat -> Bool [ditto] . 487 eq (I / N) < (J / M) = (I * M) < (J * N) . 488 eq (I / N) < K = I < (K * N) . 489 eq K < (J / M) = (K * M) < J . 490 491 op _<=_ : Rat Rat -> Bool [ditto] . 492 eq (I / N) <= (J / M) = (I * M) <= (J * N) . 493 eq (I / N) <= K = I <= (K * N) . 494 eq K <= (J / M) = (K * M) <= J . 495 496 op _>_ : Rat Rat -> Bool [ditto] . 497 eq (I / N) > (J / M) = (I * M) > (J * N) . 498 eq (I / N) > K = I > (K * N) . 499 eq K > (J / M) = (K * M) > J . 500 501 op _>=_ : Rat Rat -> Bool [ditto] . 502 eq (I / N) >= (J / M) = (I * M) >= (J * N) . 503 eq (I / N) >= K = I >= (K * N) . 504 eq K >= (J / M) = (K * M) >= J . 505 506 op _divides_ : NzRat Rat -> Bool [ditto] . 507 eq (I / N) divides K = I divides N * K . 508 eq Q divides (J / M) = Q * M divides J . 509 510 op trunc : PosRat -> Nat . 511 op trunc : Rat -> Int . 512 eq trunc(K) = K . 513 eq trunc(I / N) = I quo N . 514 515 op frac : Rat -> Rat . 516 eq frac(K) = 0 . 517 eq frac(I / N) = (I rem N) / N . 518 519 op floor : PosRat -> Nat . 520 op floor : Rat -> Int . 521 op ceiling : PosRat -> NzNat . 522 op ceiling : Rat -> Int . 523 eq floor(K) = K . 524 eq ceiling(K) = K . 525 eq floor(N / M) = N quo M . 526 eq ceiling(N / M) = ((N + M) - 1) quo M . 527 eq floor(- N / M) = - ceiling(N / M) . 528 eq ceiling(- N / M) = - floor(N / M) . 529endfm 530 531fmod FLOAT is 532 protecting BOOL . 533 sorts FiniteFloat Float . 534 subsort FiniteFloat < Float . 535 536*** pseudo constructor for the set of double precision floats 537 op <Floats> : -> FiniteFloat [special (id-hook FloatSymbol)] . 538 op <Floats> : -> Float [ditto] . 539 540 op -_ : Float -> Float 541 [prec 15 542 special (id-hook FloatOpSymbol (-) 543 op-hook floatSymbol (<Floats> : ~> Float))] . 544 545 op -_ : FiniteFloat -> FiniteFloat [ditto] . 546 547 op _+_ : Float Float -> Float 548 [prec 33 gather (E e) 549 special (id-hook FloatOpSymbol (+) 550 op-hook floatSymbol (<Floats> : ~> Float))] . 551 552 op _-_ : Float Float -> Float 553 [prec 33 gather (E e) 554 special (id-hook FloatOpSymbol (-) 555 op-hook floatSymbol (<Floats> : ~> Float))] . 556 557 op _*_ : Float Float -> Float 558 [prec 31 gather (E e) 559 special (id-hook FloatOpSymbol (*) 560 op-hook floatSymbol (<Floats> : ~> Float))] . 561 562 op _/_ : Float Float ~> Float 563 [prec 31 gather (E e) 564 special (id-hook FloatOpSymbol (/) 565 op-hook floatSymbol (<Floats> : ~> Float))] . 566 567 op _rem_ : Float Float ~> Float 568 [prec 31 gather (E e) 569 special (id-hook FloatOpSymbol (rem) 570 op-hook floatSymbol (<Floats> : ~> Float))] . 571 572 op _^_ : Float Float ~> Float 573 [prec 29 gather (E e) 574 special (id-hook FloatOpSymbol (^) 575 op-hook floatSymbol (<Floats> : ~> Float))] . 576 577 op abs : Float -> Float 578 [special (id-hook FloatOpSymbol (abs) 579 op-hook floatSymbol (<Floats> : ~> Float))] . 580 581 op abs : FiniteFloat -> FiniteFloat [ditto] . 582 583 op floor : Float -> Float 584 [special (id-hook FloatOpSymbol (floor) 585 op-hook floatSymbol (<Floats> : ~> Float))] . 586 587 op ceiling : Float -> Float 588 [special (id-hook FloatOpSymbol (ceiling) 589 op-hook floatSymbol (<Floats> : ~> Float))] . 590 591 op min : Float Float -> Float 592 [special (id-hook FloatOpSymbol (min) 593 op-hook floatSymbol (<Floats> : ~> Float))] . 594 595 op max : Float Float -> Float 596 [special (id-hook FloatOpSymbol (max) 597 op-hook floatSymbol (<Floats> : ~> Float))] . 598 599 op sqrt : Float ~> Float 600 [special (id-hook FloatOpSymbol (sqrt) 601 op-hook floatSymbol (<Floats> : ~> Float))] . 602 603 op exp : Float -> Float 604 [special (id-hook FloatOpSymbol (exp) 605 op-hook floatSymbol (<Floats> : ~> Float))] . 606 607 op log : Float ~> Float 608 [special (id-hook FloatOpSymbol (log) 609 op-hook floatSymbol (<Floats> : ~> Float))] . 610 611 op sin : Float -> Float 612 [special (id-hook FloatOpSymbol (sin) 613 op-hook floatSymbol (<Floats> : ~> Float))] . 614 615 op cos : Float -> Float 616 [special (id-hook FloatOpSymbol (cos) 617 op-hook floatSymbol (<Floats> : ~> Float))] . 618 619 op tan : Float -> Float 620 [special (id-hook FloatOpSymbol (tan) 621 op-hook floatSymbol (<Floats> : ~> Float))] . 622 623 op asin : Float ~> Float 624 [special (id-hook FloatOpSymbol (asin) 625 op-hook floatSymbol (<Floats> : ~> Float))] . 626 627 op acos : Float ~> Float 628 [special (id-hook FloatOpSymbol (acos) 629 op-hook floatSymbol (<Floats> : ~> Float))] . 630 631 op atan : Float -> Float 632 [special (id-hook FloatOpSymbol (atan) 633 op-hook floatSymbol (<Floats> : ~> Float))] . 634 635 op atan : Float Float -> Float 636 [special (id-hook FloatOpSymbol (atan) 637 op-hook floatSymbol (<Floats> : ~> Float))] . 638 639 op _<_ : Float Float -> Bool 640 [prec 51 641 special (id-hook FloatOpSymbol (<) 642 op-hook floatSymbol (<Floats> : ~> Float) 643 term-hook trueTerm (true) 644 term-hook falseTerm (false))] . 645 646 op _<=_ : Float Float -> Bool 647 [prec 51 648 special (id-hook FloatOpSymbol (<=) 649 op-hook floatSymbol (<Floats> : ~> Float) 650 term-hook trueTerm (true) 651 term-hook falseTerm (false))] . 652 653 op _>_ : Float Float -> Bool 654 [prec 51 655 special (id-hook FloatOpSymbol (>) 656 op-hook floatSymbol (<Floats> : ~> Float) 657 term-hook trueTerm (true) 658 term-hook falseTerm (false))] . 659 660 op _>=_ : Float Float -> Bool 661 [prec 51 662 special (id-hook FloatOpSymbol (>=) 663 op-hook floatSymbol (<Floats> : ~> Float) 664 term-hook trueTerm (true) 665 term-hook falseTerm (false))] . 666 667 op pi : -> FiniteFloat . 668 eq pi = 3.1415926535897931 . 669 670 op _=[_]_ : Float FiniteFloat Float -> Bool [prec 51 format (d d d d d s d)] . 671 var X Y : Float . 672 var Z : FiniteFloat . 673 eq X =[Z] Y = abs(X - Y) < Z . 674endfm 675 676fmod STRING is 677 protecting NAT . 678 sorts String Char FindResult . 679 subsort Char < String . 680 subsort Nat < FindResult . 681 682*** pseudo constructor for the infinite set of strings 683 op <Strings> : -> Char [special (id-hook StringSymbol)] . 684 op <Strings> : -> String [ditto] . 685 686 op notFound : -> FindResult [ctor] . 687 688 op ascii : Char -> Nat 689 [special (id-hook StringOpSymbol (ascii) 690 op-hook stringSymbol (<Strings> : ~> Char) 691 op-hook succSymbol (s_ : Nat ~> NzNat))] . 692 693 op char : Nat ~> Char 694 [special (id-hook StringOpSymbol (char) 695 op-hook stringSymbol (<Strings> : ~> Char) 696 op-hook succSymbol (s_ : Nat ~> NzNat))] . 697 698 op _+_ : String String -> String 699 [prec 33 gather (E e) 700 special (id-hook StringOpSymbol (+) 701 op-hook stringSymbol (<Strings> : ~> String))] . 702 703 op length : String -> Nat 704 [special (id-hook StringOpSymbol (length) 705 op-hook stringSymbol (<Strings> : ~> String) 706 op-hook succSymbol (s_ : Nat ~> NzNat))] . 707 708 op substr : String Nat Nat -> String 709 [special (id-hook StringOpSymbol (substr) 710 op-hook stringSymbol (<Strings> : ~> String) 711 op-hook succSymbol (s_ : Nat ~> NzNat))] . 712 713 op find : String String Nat -> FindResult 714 [special (id-hook StringOpSymbol (find) 715 op-hook stringSymbol (<Strings> : ~> String) 716 op-hook succSymbol (s_ : Nat ~> NzNat) 717 term-hook notFoundTerm (notFound))] . 718 719 op rfind : String String Nat -> FindResult 720 [special (id-hook StringOpSymbol (rfind) 721 op-hook stringSymbol (<Strings> : ~> String) 722 op-hook succSymbol (s_ : Nat ~> NzNat) 723 term-hook notFoundTerm (notFound))] . 724 725 op _<_ : String String -> Bool 726 [prec 37 727 special (id-hook StringOpSymbol (<) 728 op-hook stringSymbol (<Strings> : ~> String) 729 term-hook trueTerm (true) 730 term-hook falseTerm (false))] . 731 732 op _<=_ : String String -> Bool 733 [prec 37 734 special (id-hook StringOpSymbol (<=) 735 op-hook stringSymbol (<Strings> : ~> String) 736 term-hook trueTerm (true) 737 term-hook falseTerm (false))] . 738 739 op _>_ : String String -> Bool 740 [prec 37 741 special (id-hook StringOpSymbol (>) 742 op-hook stringSymbol (<Strings> : ~> String) 743 term-hook trueTerm (true) 744 term-hook falseTerm (false))] . 745 746 op _>=_ : String String -> Bool 747 [prec 37 748 special (id-hook StringOpSymbol (>=) 749 op-hook stringSymbol (<Strings> : ~> String) 750 term-hook trueTerm (true) 751 term-hook falseTerm (false))] . 752endfm 753 754fmod CONVERSION is 755 protecting RAT . 756 protecting FLOAT . 757 protecting STRING . 758 sort DecFloat . 759 op <_,_,_> : Int String Int -> DecFloat [ctor] . 760 761 op float : Rat -> Float 762 [special (id-hook FloatOpSymbol (float) 763 op-hook floatSymbol (<Floats> : ~> Float) 764 op-hook succSymbol (s_ : Nat ~> NzNat) 765 op-hook minusSymbol (-_ : NzNat ~> Int) 766 op-hook divisionSymbol (_/_ : NzInt NzNat ~> NzRat))] . 767 768 op rat : FiniteFloat -> Rat 769 [special (id-hook FloatOpSymbol (rat) 770 op-hook floatSymbol (<Floats> : ~> Float) 771 op-hook succSymbol (s_ : Nat ~> NzNat) 772 op-hook minusSymbol (-_ : NzNat ~> Int) 773 op-hook divisionSymbol (_/_ : NzInt NzNat ~> NzRat))] . 774 775 op string : Rat NzNat ~> String 776 [special (id-hook StringOpSymbol (string) 777 op-hook stringSymbol (<Strings> : ~> String) 778 op-hook succSymbol (s_ : Nat ~> NzNat) 779 op-hook minusSymbol (-_ : NzNat ~> Int) 780 op-hook divisionSymbol (_/_ : NzInt NzNat ~> NzRat))] . 781 782 op rat : String NzNat ~> Rat 783 [special (id-hook StringOpSymbol (rat) 784 op-hook stringSymbol (<Strings> : ~> String) 785 op-hook succSymbol (s_ : Nat ~> NzNat) 786 op-hook minusSymbol (-_ : NzNat ~> Int) 787 op-hook divisionSymbol (_/_ : NzInt NzNat ~> NzRat))] . 788 789 op string : Float -> String 790 [special (id-hook StringOpSymbol (string) 791 op-hook stringSymbol (<Strings> : ~> String) 792 op-hook floatSymbol (<Floats> : ~> Float))] . 793 794 op float : String ~> Float 795 [special (id-hook StringOpSymbol (float) 796 op-hook stringSymbol (<Strings> : ~> String) 797 op-hook floatSymbol (<Floats> : ~> Float))] . 798 799 op decFloat : Float Nat -> DecFloat 800 [special (id-hook StringOpSymbol (decFloat) 801 op-hook stringSymbol (<Strings> : ~> String) 802 op-hook floatSymbol (<Floats> : ~> Float) 803 op-hook succSymbol (s_ : Nat ~> NzNat) 804 op-hook minusSymbol (-_ : NzNat ~> Int) 805 op-hook decFloatSymbol 806 (<_,_,_> : Int String Int ~> DecFloat))] . 807endfm 808 809fmod RANDOM is 810 protecting NAT . 811 op random : Nat -> Nat 812 [special (id-hook RandomOpSymbol 813 op-hook succSymbol (s_ : Nat ~> NzNat))] . 814endfm 815 816fmod QID is 817 protecting STRING . 818 sort Qid . 819 820*** pseudo constructor for the infinite set of quoted identifiers 821 op <Qids> : -> Qid [special (id-hook QuotedIdentifierSymbol)] . 822 823 op string : Qid -> String 824 [special (id-hook QuotedIdentifierOpSymbol (string) 825 op-hook quotedIdentifierSymbol (<Qids> : ~> Qid) 826 op-hook stringSymbol (<Strings> : ~> String))] . 827 828 op qid : String ~> Qid 829 [special (id-hook QuotedIdentifierOpSymbol (qid) 830 op-hook quotedIdentifierSymbol (<Qids> : ~> Qid) 831 op-hook stringSymbol (<Strings> : ~> String))] . 832endfm 833 834*** 835*** Standard theories and views. 836*** 837 838fth TRIV is 839 sort Elt . 840endfth 841 842view TRIV from TRIV to TRIV is endv 843 844view Bool from TRIV to BOOL is 845 sort Elt to Bool . 846endv 847 848view Nat from TRIV to NAT is 849 sort Elt to Nat . 850endv 851 852view Int from TRIV to INT is 853 sort Elt to Int . 854endv 855 856view Rat from TRIV to RAT is 857 sort Elt to Rat . 858endv 859 860view Float from TRIV to FLOAT is 861 sort Elt to Float . 862endv 863 864view String from TRIV to STRING is 865 sort Elt to String . 866endv 867 868view Qid from TRIV to QID is 869 sort Elt to Qid . 870endv 871 872fth STRICT-WEAK-ORDER is 873 protecting BOOL . 874 including TRIV . 875 op _<_ : Elt Elt -> Bool . 876 vars X Y Z : Elt . 877 ceq X < Z = true if X < Y /\ Y < Z [nonexec label transitive] . 878 eq X < X = false [nonexec label irreflexive] . 879 ceq X < Y or Y < X or Y < Z or Z < Y = true if X < Z or Z < X 880 [nonexec label incomparability-transitive] . 881endfth 882 883view STRICT-WEAK-ORDER from TRIV to STRICT-WEAK-ORDER is endv 884 885fth STRICT-TOTAL-ORDER is 886 inc STRICT-WEAK-ORDER . 887 vars X Y : Elt . 888 ceq X = Y if X < Y = false /\ Y < X = false [nonexec label total] . 889endfth 890 891view STRICT-TOTAL-ORDER from STRICT-WEAK-ORDER to STRICT-TOTAL-ORDER is endv 892 893view Nat< from STRICT-TOTAL-ORDER to NAT is 894 sort Elt to Nat . 895endv 896 897view Int< from STRICT-TOTAL-ORDER to INT is 898 sort Elt to Int . 899endv 900 901view Rat< from STRICT-TOTAL-ORDER to RAT is 902 sort Elt to Rat . 903endv 904 905view Float< from STRICT-TOTAL-ORDER to FLOAT is 906 sort Elt to Float . 907endv 908 909view String< from STRICT-TOTAL-ORDER to STRING is 910 sort Elt to String . 911endv 912 913fth TOTAL-PREORDER is 914 protecting BOOL . 915 including TRIV . 916 op _<=_ : Elt Elt -> Bool . 917 vars X Y Z : Elt . 918 eq X <= X = true [nonexec label reflexive] . 919 ceq X <= Z = true if X <= Y /\ Y <= Z [nonexec label transitive] . 920 eq X <= Y or Y <= X = true [nonexec label total] . 921endfth 922 923view TOTAL-PREORDER from TRIV to TOTAL-PREORDER is endv 924 925fth TOTAL-ORDER is 926 inc TOTAL-PREORDER . 927 vars X Y : Elt . 928 ceq X = Y if X <= Y /\ Y <= X [nonexec label antisymmetric] . 929endfth 930 931view TOTAL-ORDER from TOTAL-PREORDER to TOTAL-ORDER is endv 932 933view Nat<= from TOTAL-ORDER to NAT is 934 sort Elt to Nat . 935endv 936 937view Int<= from TOTAL-ORDER to INT is 938 sort Elt to Int . 939endv 940 941view Rat<= from TOTAL-ORDER to RAT is 942 sort Elt to Rat . 943endv 944 945view Float<= from TOTAL-ORDER to FLOAT is 946 sort Elt to Float . 947endv 948 949view String<= from TOTAL-ORDER to STRING is 950 sort Elt to String . 951endv 952 953fth DEFAULT is 954 including TRIV . 955 op 0 : -> Elt . 956endfth 957 958view DEFAULT from TRIV to DEFAULT is endv 959 960view Nat0 from DEFAULT to NAT is 961 sort Elt to Nat . 962endv 963 964view Int0 from DEFAULT to INT is 965 sort Elt to Int . 966endv 967 968view Rat0 from DEFAULT to RAT is 969 sort Elt to Rat . 970endv 971 972view Float0 from DEFAULT to FLOAT is 973 sort Elt to Float . 974 op 0 to term 0.0 . 975endv 976 977view String0 from DEFAULT to STRING is 978 sort Elt to String . 979 op 0 to term "" . 980endv 981 982view Qid0 from DEFAULT to QID is 983 sort Elt to Qid . 984 op 0 to term ' . 985endv 986 987*** 988*** Container data types defined in Maude. 989*** 990 991fmod LIST{X :: TRIV} is 992 protecting NAT . 993 sorts NeList{X} List{X} . 994 subsort X$Elt < NeList{X} < List{X} . 995 996 op nil : -> List{X} [ctor] . 997 op __ : List{X} List{X} -> List{X} [ctor assoc id: nil prec 25] . 998 op __ : NeList{X} List{X} -> NeList{X} [ctor ditto] . 999 op __ : List{X} NeList{X} -> NeList{X} [ctor ditto] . 1000 1001 var E E' : X$Elt . 1002 vars A L : List{X} . 1003 var C : Nat . 1004 1005 op append : List{X} List{X} -> List{X} . 1006 op append : NeList{X} List{X} -> NeList{X} . 1007 op append : List{X} NeList{X} -> NeList{X} . 1008 eq append(A, L) = A L . 1009 1010 op head : NeList{X} -> X$Elt . 1011 eq head(E L) = E . 1012 1013 op tail : NeList{X} -> List{X} . 1014 eq tail(E L) = L . 1015 1016 op last : NeList{X} -> X$Elt . 1017 eq last(L E) = E . 1018 1019 op front : NeList{X} -> List{X} . 1020 eq front(L E) = L . 1021 1022 op occurs : X$Elt List{X} -> Bool . 1023 eq occurs(E, nil) = false . 1024 eq occurs(E, E' L) = if E == E' then true else occurs(E, L) fi . 1025 1026 op reverse : List{X} -> List{X} . 1027 op reverse : NeList{X} -> NeList{X} . 1028 eq reverse(L) = $reverse(L, nil) . 1029 1030 op $reverse : List{X} List{X} -> List{X} . 1031 eq $reverse(nil, A) = A . 1032 eq $reverse(E L, A) = $reverse(L, E A). 1033 1034 op size : List{X} -> Nat . 1035 op size : NeList{X} -> NzNat . 1036 eq size(L) = $size(L, 0) . 1037 1038 op $size : List{X} Nat -> Nat . 1039 eq $size(nil, C) = C . 1040 eq $size(E L, C) = $size(L, C + 1) . 1041endfm 1042 1043fmod WEAKLY-SORTABLE-LIST{X :: STRICT-WEAK-ORDER} is 1044 protecting LIST{STRICT-WEAK-ORDER}{X} * 1045 (sort NeList{STRICT-WEAK-ORDER}{X} to NeList{X}, 1046 sort List{STRICT-WEAK-ORDER}{X} to List{X}) . 1047 sort $Split{X} . 1048 1049 vars E E' : X$Elt . 1050 vars A A' L L' : List{X} . 1051 var N : NeList{X} . 1052 1053 op sort : List{X} -> List{X} . 1054 op sort : NeList{X} -> NeList{X} . 1055 eq sort(nil) = nil . 1056 eq sort(E) = E . 1057 eq sort(E N) = $sort($split(E N, nil, nil)) . 1058 1059 op $sort : $Split{X} -> List{X} . 1060 eq $sort($split(nil, L, L')) = $merge(sort(L), sort(L'), nil) . 1061 1062 op $split : List{X} List{X} List{X} -> $Split{X} [ctor] . 1063 eq $split(E, A, A') = $split(nil, A E, A') . 1064 eq $split(E L E', A, A') = $split(L, A E, E' A') . 1065 1066 op merge : List{X} List{X} -> List{X} . 1067 op merge : NeList{X} List{X} -> NeList{X} . 1068 op merge : List{X} NeList{X} -> NeList{X} . 1069 eq merge(L, L') = $merge(L, L', nil) . 1070 1071 op $merge : List{X} List{X} List{X} -> List{X} . 1072 eq $merge(L, nil, A) = A L . 1073 eq $merge(nil, L, A) = A L . 1074 eq $merge(E L, E' L', A) = 1075 if E' < E then $merge(E L, L', A E') 1076 else $merge(L, E' L', A E) 1077 fi . 1078endfm 1079 1080fmod SORTABLE-LIST{X :: STRICT-TOTAL-ORDER} is 1081 protecting WEAKLY-SORTABLE-LIST{STRICT-TOTAL-ORDER}{X} * 1082 (sort NeList{STRICT-TOTAL-ORDER}{X} to NeList{X}, 1083 sort List{STRICT-TOTAL-ORDER}{X} to List{X}) . 1084endfm 1085 1086fmod WEAKLY-SORTABLE-LIST'{X :: TOTAL-PREORDER} is 1087 protecting LIST{TOTAL-PREORDER}{X} * 1088 (sort NeList{TOTAL-PREORDER}{X} to NeList{X}, 1089 sort List{TOTAL-PREORDER}{X} to List{X}) . 1090 sort $Split{X} . 1091 1092 vars E E' : X$Elt . 1093 vars A A' L L' : List{X} . 1094 var N : NeList{X} . 1095 1096 op sort : List{X} -> List{X} . 1097 op sort : NeList{X} -> NeList{X} . 1098 eq sort(nil) = nil . 1099 eq sort(E) = E . 1100 eq sort(E N) = $sort($split(E N, nil, nil)) . 1101 1102 op $sort : $Split{X} -> List{X} . 1103 eq $sort($split(nil, L, L')) = $merge(sort(L), sort(L'), nil) . 1104 1105 op $split : List{X} List{X} List{X} -> $Split{X} [ctor] . 1106 eq $split(E, A, A') = $split(nil, A E, A') . 1107 eq $split(E L E', A, A') = $split(L, A E, E' A') . 1108 1109 op merge : List{X} List{X} -> List{X} . 1110 op merge : NeList{X} List{X} -> NeList{X} . 1111 op merge : List{X} NeList{X} -> NeList{X} . 1112 eq merge(L, L') = $merge(L, L', nil) . 1113 1114 op $merge : List{X} List{X} List{X} -> List{X} . 1115 eq $merge(L, nil, A) = A L . 1116 eq $merge(nil, L, A) = A L . 1117 eq $merge(E L, E' L', A) = 1118 if E <= E' then $merge(L, E' L', A E) 1119 else $merge(E L, L', A E') 1120 fi . 1121endfm 1122 1123fmod SORTABLE-LIST'{X :: TOTAL-ORDER} is 1124 protecting WEAKLY-SORTABLE-LIST'{TOTAL-ORDER}{X} * 1125 (sort NeList{TOTAL-ORDER}{X} to NeList{X}, 1126 sort List{TOTAL-ORDER}{X} to List{X}) . 1127endfm 1128 1129fmod SET{X :: TRIV} is 1130 protecting EXT-BOOL . 1131 protecting NAT . 1132 sorts NeSet{X} Set{X} . 1133 subsort X$Elt < NeSet{X} < Set{X} . 1134 1135 op empty : -> Set{X} [ctor] . 1136 op _,_ : Set{X} Set{X} -> Set{X} [ctor assoc comm id: empty prec 121 format (d r os d)] . 1137 op _,_ : NeSet{X} Set{X} -> NeSet{X} [ctor ditto] . 1138 1139 var E : X$Elt . 1140 var N : NeSet{X} . 1141 vars A S S' : Set{X} . 1142 var C : Nat . 1143 1144 eq N, N = N . 1145 1146 op insert : X$Elt Set{X} -> Set{X} . 1147 eq insert(E, S) = E, S . 1148 1149 op delete : X$Elt Set{X} -> Set{X} . 1150 eq delete(E, (E, S)) = delete(E, S) . 1151 eq delete(E, S) = S [owise] . 1152 1153 op _in_ : X$Elt Set{X} -> Bool . 1154 eq E in (E, S) = true . 1155 eq E in S = false [owise] . 1156 1157 op |_| : Set{X} -> Nat . 1158 op |_| : NeSet{X} -> NzNat . 1159 eq | S | = $card(S, 0) . 1160 1161 op $card : Set{X} Nat -> Nat . 1162 eq $card(empty, C) = C . 1163 eq $card((N, N, S), C) = $card((N, S), C) . 1164 eq $card((E, S), C) = $card(S, C + 1) [owise] . 1165 1166 op union : Set{X} Set{X} -> Set{X} . 1167 op union : NeSet{X} Set{X} -> NeSet{X} . 1168 op union : Set{X} NeSet{X} -> NeSet{X} . 1169 eq union(S, S') = S, S' . 1170 1171 op intersection : Set{X} Set{X} -> Set{X} . 1172 eq intersection(S, empty) = empty . 1173 eq intersection(S, N) = $intersect(S, N, empty) . 1174 1175 op $intersect : Set{X} Set{X} Set{X} -> Set{X} . 1176 eq $intersect(empty, S', A) = A . 1177 eq $intersect((E, S), S', A) = $intersect(S, S', if E in S' then E, A else A fi) . 1178 1179 op _\_ : Set{X} Set{X} -> Set{X} [gather (E e)]. 1180 eq S \ empty = S . 1181 eq S \ N = $diff(S, N, empty) . 1182 1183 op $diff : Set{X} Set{X} Set{X} -> Set{X} . 1184 eq $diff(empty, S', A) = A . 1185 eq $diff((E, S), S', A) = $diff(S, S', if E in S' then A else E, A fi) . 1186 1187 op _subset_ : Set{X} Set{X} -> Bool . 1188 eq empty subset S' = true . 1189 eq (E, S) subset S' = E in S' and-then S subset S' . 1190 1191 op _psubset_ : Set{X} Set{X} -> Bool . 1192 eq S psubset S' = S =/= S' and-then S subset S' . 1193endfm 1194 1195fmod LIST-AND-SET{X :: TRIV} is 1196 protecting LIST{X} . 1197 protecting SET{X} . 1198 1199 var E : X$Elt . 1200 vars A L : List{X} . 1201 var S : Set{X} . 1202 1203 op makeSet : List{X} -> Set{X} . 1204 op makeSet : NeList{X} -> NeSet{X} . 1205 eq makeSet(L) = $makeSet(L, empty) . 1206 1207 op $makeSet : List{X} Set{X} -> Set{X} . 1208 op $makeSet : NeList{X} Set{X} -> NeSet{X} . 1209 op $makeSet : List{X} NeSet{X} -> NeSet{X} . 1210 eq $makeSet(nil, S) = S . 1211 eq $makeSet(E L, S) = $makeSet(L, (E, S)) . 1212 1213 op filter : List{X} Set{X} -> List{X} . 1214 eq filter(L, S) = $filter(L, S, nil) . 1215 1216 op $filter : List{X} Set{X} List{X} -> List{X} . 1217 eq $filter(nil, S, A) = A . 1218 eq $filter(E L, S, A) = $filter(L, S, if E in S then A E else A fi) . 1219 1220 op filterOut : List{X} Set{X} -> List{X} . 1221 eq filterOut(L, S) = $filterOut(L, S, nil) . 1222 1223 op $filterOut : List{X} Set{X} List{X} -> List{X} . 1224 eq $filterOut(nil, S, A) = A . 1225 eq $filterOut(E L, S, A) = $filterOut(L, S, if E in S then A else A E fi) . 1226endfm 1227 1228fmod SORTABLE-LIST-AND-SET{X :: STRICT-TOTAL-ORDER} is 1229 protecting SORTABLE-LIST{X} . 1230*** 1231*** This double renaming is needed for correct sharing of a renamed 1232*** copy of LIST since Core Maude does not evaluate the composition 1233*** of renamings but applies them sequentially. 1234*** 1235 protecting LIST-AND-SET{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} * 1236 (sort NeList{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to NeList{STRICT-TOTAL-ORDER}{X}, 1237 sort List{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to List{STRICT-TOTAL-ORDER}{X}) * 1238 (sort NeList{STRICT-TOTAL-ORDER}{X} to NeList{X}, 1239 sort List{STRICT-TOTAL-ORDER}{X} to List{X}, 1240 sort NeSet{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to NeSet{X}, 1241 sort Set{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to Set{X}) . 1242 1243 var E : X$Elt . 1244 var L : List{X} . 1245 var S : Set{X} . 1246 1247 op makeList : Set{X} -> List{X} . 1248 op makeList : NeSet{X} -> NeList{X} . 1249 eq makeList(S) = $makeList(S, nil) . 1250 1251 op $makeList : Set{X} List{X} -> List{X} . 1252 op $makeList : NeSet{X} List{X} -> NeList{X} . 1253 op $makeList : Set{X} NeList{X} -> NeList{X} . 1254 eq $makeList(empty, L) = sort(L) . 1255 eq $makeList((E, E, S), L) = $makeList((E, S), L) . 1256 eq $makeList((E, S), L) = $makeList(S, E L) [owise] . 1257endfm 1258 1259fmod SORTABLE-LIST-AND-SET'{X :: TOTAL-ORDER} is 1260 protecting SORTABLE-LIST'{X} . 1261*** 1262*** This double renaming is needed for the same reasons as above. 1263*** 1264 protecting LIST-AND-SET{TOTAL-PREORDER}{TOTAL-ORDER}{X} * 1265 (sort NeList{TOTAL-PREORDER}{TOTAL-ORDER}{X} to NeList{TOTAL-ORDER}{X}, 1266 sort List{TOTAL-PREORDER}{TOTAL-ORDER}{X} to List{TOTAL-ORDER}{X}) * 1267 (sort NeList{TOTAL-ORDER}{X} to NeList{X}, 1268 sort List{TOTAL-ORDER}{X} to List{X}, 1269 sort NeSet{TOTAL-PREORDER}{TOTAL-ORDER}{X} to NeSet{X}, 1270 sort Set{TOTAL-PREORDER}{TOTAL-ORDER}{X} to Set{X}) . 1271 1272 var E : X$Elt . 1273 var L : List{X} . 1274 var S : Set{X} . 1275 1276 op makeList : Set{X} -> List{X} . 1277 op makeList : NeSet{X} -> NeList{X} . 1278 eq makeList(S) = $makeList(S, nil) . 1279 1280 op $makeList : Set{X} List{X} -> List{X} . 1281 op $makeList : NeSet{X} List{X} -> NeList{X} . 1282 op $makeList : Set{X} NeList{X} -> NeList{X} . 1283 eq $makeList(empty, L) = sort(L) . 1284 eq $makeList((E, E, S), L) = $makeList((E, S), L) . 1285 eq $makeList((E, S), L) = $makeList(S, E L) [owise] . 1286endfm 1287 1288fmod LIST*{X :: TRIV} is 1289 protecting NAT . 1290 sorts Item{X} PreList{X} NeList{X} List{X} . 1291 subsort X$Elt List{X} < Item{X} < PreList{X} . 1292 subsort NeList{X} < List{X} . 1293 1294 op __ : PreList{X} PreList{X} -> PreList{X} [ctor assoc prec 25] . 1295 op [_] : PreList{X} -> NeList{X} [ctor] . 1296 op [] : -> List{X} [ctor] . 1297 1298 vars A P : PreList{X} . 1299 var L : List{X} . 1300 var E E' : Item{X} . 1301 var C : Nat . 1302 1303 op append : List{X} List{X} -> List{X} . 1304 op append : NeList{X} List{X} -> NeList{X} . 1305 op append : List{X} NeList{X} -> NeList{X} . 1306 eq append([], L) = L . 1307 eq append(L, []) = L . 1308 eq append([P], [A]) = [P A] . 1309 1310 op head : NeList{X} -> Item{X} . 1311 eq head([E]) = E . 1312 eq head([E P]) = E . 1313 1314 op tail : NeList{X} -> List{X} . 1315 eq tail([E]) = [] . 1316 eq tail([E P]) = [P] . 1317 1318 op last : NeList{X} -> Item{X} . 1319 eq last([E]) = E . 1320 eq last([P E]) = E . 1321 1322 op front : NeList{X} -> List{X} . 1323 eq front([E]) = [] . 1324 eq front([P E]) = [P] . 1325 1326 op occurs : Item{X} List{X} -> Bool . 1327 eq occurs(E, []) = false . 1328 eq occurs(E, [E']) = (E == E') . 1329 eq occurs(E, [E' P]) = if E == E' then true else occurs(E, [P]) fi . 1330 1331 op reverse : List{X} -> List{X} . 1332 op reverse : NeList{X} -> NeList{X} . 1333 eq reverse([]) = [] . 1334 eq reverse([E]) = [E] . 1335 eq reverse([E P]) = [$reverse(P, E)] . 1336 1337 op $reverse : PreList{X} PreList{X} -> PreList{X} . 1338 eq $reverse(E, A) = E A . 1339 eq $reverse(E P, A) = $reverse(P, E A). 1340 1341 op size : List{X} -> Nat . 1342 op size : NeList{X} -> NzNat . 1343 eq size([]) = 0 . 1344 eq size([P]) = $size(P, 0) . 1345 1346 op $size : PreList{X} Nat -> NzNat . 1347 eq $size(E, C) = C + 1 . 1348 eq $size(E P, C) = $size(P, C + 1) . 1349endfm 1350 1351fmod SET*{X :: TRIV} is 1352 protecting EXT-BOOL . 1353 protecting NAT . 1354 sorts Element{X} PreSet{X} NeSet{X} Set{X} . 1355 subsort X$Elt Set{X} < Element{X} < PreSet{X} . 1356 subsort NeSet{X} < Set{X} . 1357 1358 op _,_ : PreSet{X} PreSet{X} -> PreSet{X} [ctor assoc comm prec 121 format (d r os d)] . 1359 op {_} : PreSet{X} -> NeSet{X} [ctor] . 1360 op {} : -> Set{X} [ctor] . 1361 1362 vars P Q : PreSet{X} . 1363 vars A S : Set{X} . 1364 var E : Element{X} . 1365 var N : NeSet{X} . 1366 var C : Nat . 1367 1368 eq {P, P} = {P} . 1369 eq {P, P, Q} = {P, Q} . 1370 1371 op insert : Element{X} Set{X} -> Set{X} . 1372 eq insert(E, {}) = {E} . 1373 eq insert(E, {P}) = {E, P} . 1374 1375 op delete : Element{X} Set{X} -> Set{X} . 1376 eq delete(E, {E}) = {} . 1377 eq delete(E, {E, P}) = delete(E, {P}) . 1378 eq delete(E, S) = S [owise] . 1379 1380 op _in_ : Element{X} Set{X} -> Bool . 1381 eq E in {E} = true . 1382 eq E in {E, P} = true . 1383 eq E in S = false [owise] . 1384 1385 op |_| : Set{X} -> Nat . 1386 op |_| : NeSet{X} -> NzNat . 1387 eq | {} | = 0 . 1388 eq | {P} | = $card(P, 0) . 1389 1390 op $card : PreSet{X} Nat -> Nat . 1391 eq $card(E, C) = C + 1 . 1392 eq $card((N, N, P), C) = $card((N, P), C) . 1393 eq $card((E, P), C) = $card(P, C + 1) [owise] . 1394 1395 op union : Set{X} Set{X} -> Set{X} . 1396 op union : NeSet{X} Set{X} -> NeSet{X} . 1397 op union : Set{X} NeSet{X} -> NeSet{X} . 1398 eq union({}, S) = S . 1399 eq union(S, {}) = S . 1400 eq union({P}, {Q}) = {P, Q} . 1401 1402 op intersection : Set{X} Set{X} -> Set{X} . 1403 eq intersection({}, S) = {} . 1404 eq intersection(S, {}) = {} . 1405 eq intersection({P}, N) = $intersect(P, N, {}) . 1406 1407 op $intersect : PreSet{X} Set{X} Set{X} -> Set{X} . 1408 eq $intersect(E, S, A) = if E in S then insert(E, A) else A fi . 1409 eq $intersect((E, P), S, A) = $intersect(P, S, $intersect(E, S, A)) . 1410 1411 op _\_ : Set{X} Set{X} -> Set{X} [gather (E e)] . 1412 eq {} \ S = {} . 1413 eq S \ {} = S . 1414 eq {P} \ N = $diff(P, N, {}) . 1415 1416 op $diff : PreSet{X} Set{X} Set{X} -> Set{X} . 1417 eq $diff(E, S, A) = if E in S then A else insert(E, A) fi . 1418 eq $diff((E, P), S, A) = $diff(P, S, $diff(E, S, A)) . 1419 1420 op 2^_ : Set{X} -> Set{X} . 1421 eq 2^{} = {{}} . 1422 eq 2^{E} = {{}, {E}} . 1423 eq 2^{E, P} = union(2^{P}, $augment(2^{P}, E, {})) . 1424 1425 op $augment : NeSet{X} Element{X} Set{X} -> Set{X} . 1426 eq $augment({S}, E, A) = insert(insert(E, S), A) . 1427 eq $augment({S, P}, E, A) = $augment({P}, E, $augment({S}, E, A)) . 1428 1429 op _subset_ : Set{X} Set{X} -> Bool . 1430 eq {} subset S = true . 1431 eq {E} subset S = E in S . 1432 eq {E, P} subset S = E in S and-then {P} subset S . 1433 1434 op _psubset_ : Set{X} Set{X} -> Bool . 1435 eq A psubset S = A =/= S and-then A subset S . 1436endfm 1437 1438fmod MAP{X :: TRIV, Y :: TRIV} is 1439 protecting BOOL . 1440 sorts Entry{X,Y} Map{X,Y} . 1441 subsort Entry{X,Y} < Map{X,Y} . 1442 1443 op _|->_ : X$Elt Y$Elt -> Entry{X,Y} [ctor] . 1444 op empty : -> Map{X,Y} [ctor] . 1445 op _,_ : Map{X,Y} Map{X,Y} -> Map{X,Y} [ctor assoc comm id: empty prec 121 format (d r os d)] . 1446 op undefined : -> [Y$Elt] [ctor] . 1447 1448 var D : X$Elt . 1449 vars R R' : Y$Elt . 1450 var M : Map{X,Y} . 1451 1452 op insert : X$Elt Y$Elt Map{X,Y} -> Map{X,Y} . 1453 eq insert(D, R, (M, D |-> R')) = 1454 if $hasMapping(M, D) then insert(D, R, M) 1455 else (M, D |-> R) 1456 fi . 1457 eq insert(D, R, M) = (M, D |-> R) [owise] . 1458 1459 op _[_] : Map{X,Y} X$Elt -> [Y$Elt] [prec 23] . 1460 eq (M, D |-> R)[D] = 1461 if $hasMapping(M, D) then undefined 1462 else R 1463 fi . 1464 eq M[D] = undefined [owise] . 1465 1466 op $hasMapping : Map{X,Y} X$Elt -> Bool . 1467 eq $hasMapping((M, D |-> R), D) = true . 1468 eq $hasMapping(M, D) = false [owise] . 1469endfm 1470 1471fmod ARRAY{X :: TRIV, Y :: DEFAULT} is 1472 protecting BOOL . 1473 sorts Entry{X,Y} Array{X,Y} . 1474 subsort Entry{X,Y} < Array{X,Y} . 1475 1476 op _|->_ : X$Elt Y$Elt -> Entry{X,Y} [ctor] . 1477 op empty : -> Array{X,Y} [ctor] . 1478 op _;_ : Array{X,Y} Array{X,Y} -> Array{X,Y} [ctor assoc comm id: empty prec 71 format (d r os d)] . 1479 1480 var D : X$Elt . 1481 vars R R' : Y$Elt . 1482 var A : Array{X,Y} . 1483 1484 op insert : X$Elt Y$Elt Array{X,Y} -> Array{X,Y} . 1485 eq insert(D, R, (A ; D |-> R')) = 1486 if $hasMapping(A, D) then insert(D, R, A) 1487 else if R == 0 then A else (A ; D |-> R) fi 1488 fi . 1489 1490 eq insert(D, R, A) = if R == 0 then A else (A ; D |-> R) fi [owise] . 1491 1492 op _[_] : Array{X,Y} X$Elt -> Y$Elt [prec 23] . 1493 eq (A ; D |-> R)[D] = 1494 if $hasMapping(A, D) then 0 1495 else R 1496 fi . 1497 eq A[D] = 0 [owise] . 1498 1499 op $hasMapping : Array{X,Y} X$Elt -> Bool . 1500 eq $hasMapping((A ; D |-> R), D) = true . 1501 eq $hasMapping(A, D) = false [owise] . 1502endfm 1503 1504*** 1505*** Container instantiations on builtin data types needed by the metalevel. 1506*** 1507 1508fmod NAT-LIST is 1509 protecting LIST{Nat} * (sort NeList{Nat} to NeNatList, sort List{Nat} to NatList) . 1510endfm 1511 1512fmod QID-LIST is 1513 protecting LIST{Qid} * (sort NeList{Qid} to NeQidList, sort List{Qid} to QidList) . 1514endfm 1515 1516fmod QID-SET is 1517 protecting SET{Qid} * (sort NeSet{Qid} to NeQidSet, sort Set{Qid} to QidSet) . 1518endfm 1519 1520*** 1521*** The metalevel. 1522*** 1523 1524fmod META-TERM is 1525 protecting QID . 1526 1527*** types 1528 sorts Sort Kind Type . 1529 subsorts Sort Kind < Type < Qid . 1530 op <Qids> : -> Sort [special (id-hook QuotedIdentifierSymbol (sortQid))] . 1531 op <Qids> : -> Kind [special (id-hook QuotedIdentifierSymbol (kindQid))] . 1532 1533*** terms 1534 sorts Constant Variable TermQid GroundTerm Term NeGroundTermList GroundTermList NeTermList TermList . 1535 subsorts Constant Variable < TermQid < Qid Term . 1536 subsorts Constant < GroundTerm < Term NeGroundTermList < NeTermList . 1537 subsorts NeGroundTermList < NeTermList GroundTermList < TermList . 1538 op <Qids> : -> Constant [special (id-hook QuotedIdentifierSymbol (constantQid))] . 1539 op <Qids> : -> Variable [special (id-hook QuotedIdentifierSymbol (variableQid))] . 1540 op empty : -> GroundTermList [ctor] . 1541 op _,_ : NeGroundTermList GroundTermList -> NeGroundTermList [ctor assoc id: empty gather (e E) prec 121] . 1542 op _,_ : GroundTermList NeGroundTermList -> NeGroundTermList [ctor ditto] . 1543 op _,_ : GroundTermList GroundTermList -> GroundTermList [ctor ditto] . 1544 op _,_ : NeTermList TermList -> NeTermList [ctor ditto] . 1545 op _,_ : TermList NeTermList -> NeTermList [ctor ditto] . 1546 op _,_ : TermList TermList -> TermList [ctor ditto] . 1547 op _[_] : Qid NeGroundTermList -> GroundTerm [ctor] . 1548 op _[_] : Qid NeTermList -> Term [ctor] . 1549 1550*** extraction of names and types 1551 op getName : Constant -> Qid . 1552 op getType : Constant -> Type . 1553 var C : Constant . 1554 eq getName(C) = qid(substr(string(C), 1555 0, 1556 rfind(string(C), ".", length(string(C))))) . 1557 eq getType(C) = qid(substr(string(C), 1558 rfind(string(C), ".", length(string(C))) + 1, 1559 length(string(C)))) . 1560 1561 op getName : Variable -> Qid . 1562 op getType : Variable -> Type . 1563 var V : Variable . 1564 eq getName(V) = qid(substr(string(V), 1565 0, 1566 rfind(string(V), ":", length(string(V))))) . 1567 eq getType(V) = qid(substr(string(V), 1568 rfind(string(V), ":", length(string(V))) + 1, 1569 length(string(V)))) . 1570 1571*** substitutions 1572 sorts Assignment Substitution . 1573 subsort Assignment < Substitution . 1574 op _<-_ : Variable Term -> Assignment [ctor prec 63 format (nt d d d)] . 1575 op none : -> Substitution [ctor] . 1576 op _;_ : Substitution Substitution -> Substitution 1577 [ctor assoc comm id: none prec 65] . 1578 eq A:Assignment ; A:Assignment = A:Assignment . 1579 1580*** contexts (terms with a single hole) 1581 sorts Context NeCTermList GTermList . 1582 subsort Context < NeCTermList < GTermList . 1583 subsorts TermList < GTermList . 1584 1585 op [] : -> Context [ctor] . 1586 op _,_ : TermList NeCTermList -> NeCTermList [ctor ditto] . 1587 op _,_ : NeCTermList TermList -> NeCTermList [ctor ditto] . 1588 op _,_ : GTermList GTermList -> GTermList [ctor ditto] . 1589 op _[_] : Qid NeCTermList -> Context [ctor] . 1590endfm 1591 1592fmod META-MODULE is 1593 protecting META-TERM . 1594 protecting NAT-LIST . 1595 protecting QID-LIST . 1596 protecting QID-SET * (op empty to none, op _,_ to _;_ [prec 43]) . 1597 1598*** subsort declarations 1599 sorts SubsortDecl SubsortDeclSet . 1600 subsort SubsortDecl < SubsortDeclSet . 1601 op subsort_<_. : Sort Sort -> SubsortDecl [ctor] . 1602 op none : -> SubsortDeclSet [ctor] . 1603 op __ : SubsortDeclSet SubsortDeclSet -> SubsortDeclSet 1604 [ctor assoc comm id: none format (d ni d)] . 1605 eq S:SubsortDecl S:SubsortDecl = S:SubsortDecl . 1606 1607*** sort, kind and type sets 1608 sorts EmptyTypeSet NeSortSet NeKindSet NeTypeSet SortSet KindSet TypeSet . 1609 subsort EmptyTypeSet < SortSet KindSet < TypeSet < QidSet . 1610 subsort Sort < NeSortSet < SortSet . 1611 subsort Kind < NeKindSet < KindSet . 1612 subsort Type NeSortSet NeKindSet < NeTypeSet < TypeSet NeQidSet . 1613 op none : -> EmptyTypeSet [ctor] . 1614 op _;_ : TypeSet TypeSet -> TypeSet [ctor ditto] . 1615 op _;_ : NeTypeSet TypeSet -> NeTypeSet [ctor ditto] . 1616 op _;_ : SortSet SortSet -> SortSet [ctor ditto] . 1617 op _;_ : NeSortSet SortSet -> NeSortSet [ctor ditto] . 1618 op _;_ : KindSet KindSet -> KindSet [ctor ditto] . 1619 op _;_ : NeKindSet KindSet -> NeKindSet [ctor ditto] . 1620 op _;_ : EmptyTypeSet EmptyTypeSet -> EmptyTypeSet [ctor ditto] . 1621 1622*** type lists 1623 sort NeTypeList TypeList . 1624 subsorts Type < NeTypeList < TypeList < QidList . 1625 subsorts NeTypeList < NeQidList . 1626 op nil : -> TypeList [ctor] . 1627 op __ : TypeList TypeList -> TypeList [ctor ditto] . 1628 op __ : NeTypeList TypeList -> NeTypeList [ctor ditto] . 1629 op __ : TypeList NeTypeList -> NeTypeList [ctor ditto] . 1630 eq T:TypeList ; T:TypeList = T:TypeList . 1631 1632*** sets of type lists 1633 sort TypeListSet . 1634 subsort TypeList TypeSet < TypeListSet . 1635 op _;_ : TypeListSet TypeListSet -> TypeListSet [ctor ditto] . 1636 1637*** attribute sets 1638 sorts Attr AttrSet . 1639 subsort Attr < AttrSet . 1640 op none : -> AttrSet [ctor] . 1641 op __ : AttrSet AttrSet -> AttrSet [ctor assoc comm id: none] . 1642 eq A:Attr A:Attr = A:Attr . 1643 1644*** renamings 1645 sorts Renaming RenamingSet . 1646 subsort Renaming < RenamingSet . 1647 op sort_to_ : Qid Qid -> Renaming [ctor] . 1648 op op_to_[_] : Qid Qid AttrSet -> Renaming 1649 [ctor format (d d d d s d d d)] . 1650 op op_:_->_to_[_] : Qid TypeList Type Qid AttrSet -> Renaming 1651 [ctor format (d d d d d d d d s d d d)] . 1652 op label_to_ : Qid Qid -> Renaming [ctor] . 1653 op _,_ : RenamingSet RenamingSet -> RenamingSet 1654 [ctor assoc comm prec 43 format (d d ni d)] . 1655 1656*** parameter lists 1657 sort EmptyCommaList NeParameterList ParameterList . 1658 subsorts Sort < NeParameterList < ParameterList . 1659 subsort EmptyCommaList < GroundTermList ParameterList . 1660 op empty : -> EmptyCommaList [ctor] . 1661 op _,_ : ParameterList ParameterList -> ParameterList [ctor ditto] . 1662 op _,_ : NeParameterList ParameterList -> NeParameterList [ctor ditto] . 1663 op _,_ : ParameterList NeParameterList -> NeParameterList [ctor ditto] . 1664 op _,_ : EmptyCommaList EmptyCommaList -> EmptyCommaList [ctor ditto] . 1665 1666*** module expressions 1667 sort ModuleExpression . 1668 subsort Qid < ModuleExpression . 1669 op _+_ : ModuleExpression ModuleExpression -> ModuleExpression 1670 [ctor assoc comm] . 1671 op _*(_) : ModuleExpression RenamingSet -> ModuleExpression 1672 [ctor prec 39 format (d d s n++i n--i d)] . 1673 op _{_} : ModuleExpression ParameterList -> ModuleExpression [ctor prec 37]. 1674 1675*** parameter declarations 1676 sorts ParameterDecl NeParameterDeclList ParameterDeclList . 1677 subsorts ParameterDecl < NeParameterDeclList < ParameterDeclList . 1678 op _::_ : Sort ModuleExpression -> ParameterDecl . 1679 op nil : -> ParameterDeclList [ctor] . 1680 op _,_ : ParameterDeclList ParameterDeclList -> ParameterDeclList [ctor assoc id: nil prec 121] . 1681 op _,_ : NeParameterDeclList ParameterDeclList -> NeParameterDeclList [ctor ditto] . 1682 op _,_ : ParameterDeclList NeParameterDeclList -> NeParameterDeclList [ctor ditto] . 1683 1684*** importations 1685 sorts Import ImportList . 1686 subsort Import < ImportList . 1687 op protecting_. : ModuleExpression -> Import [ctor] . 1688 op extending_. : ModuleExpression -> Import [ctor] . 1689 op including_. : ModuleExpression -> Import [ctor] . 1690 op nil : -> ImportList [ctor] . 1691 op __ : ImportList ImportList -> ImportList 1692 [ctor assoc id: nil format (d ni d)] . 1693 1694*** hooks 1695 sorts Hook NeHookList HookList . 1696 subsort Hook < NeHookList < HookList . 1697 op id-hook : Qid QidList -> Hook [ctor format (nssss d)] . 1698 op op-hook : Qid Qid QidList Qid -> Hook [ctor format (nssss d)] . 1699 op term-hook : Qid Term -> Hook [ctor format (nssss d)] . 1700 op nil : -> HookList [ctor] . 1701 op __ : HookList HookList -> HookList [ctor assoc id: nil] . 1702 op __ : NeHookList HookList -> NeHookList [ctor ditto] . 1703 op __ : HookList NeHookList -> NeHookList [ctor ditto] . 1704 1705*** operator attributes 1706 op assoc : -> Attr [ctor] . 1707 op comm : -> Attr [ctor] . 1708 op idem : -> Attr [ctor] . 1709 op iter : -> Attr [ctor] . 1710 op id : Term -> Attr [ctor] . 1711 op left-id : Term -> Attr [ctor] . 1712 op right-id : Term -> Attr [ctor] . 1713 op strat : NeNatList -> Attr [ctor] . 1714 op memo : -> Attr [ctor] . 1715 op prec : Nat -> Attr [ctor] . 1716 op gather : QidList -> Attr [ctor] . 1717 op format : QidList -> Attr [ctor] . 1718 op ctor : -> Attr [ctor] . 1719 op config : -> Attr [ctor] . 1720 op object : -> Attr [ctor] . 1721 op msg : -> Attr [ctor] . 1722 op frozen : NeNatList -> Attr [ctor] . 1723 op poly : NeNatList -> Attr [ctor] . 1724 op special : NeHookList -> Attr [ctor] . 1725 1726*** statement attributes 1727 op label : Qid -> Attr [ctor] . 1728 op metadata : String -> Attr [ctor] . 1729 op owise : -> Attr [ctor] . 1730 op nonexec : -> Attr [ctor] . 1731 op variant : -> Attr [ctor] . 1732 op print : QidList -> Attr [ctor] . 1733 1734*** operator declarations 1735 sorts OpDecl OpDeclSet . 1736 subsort OpDecl < OpDeclSet . 1737 op (op_:_->_[_].) : Qid TypeList Type AttrSet -> OpDecl 1738 [ctor format (d d d d d d s d d s d)] . 1739 op none : -> OpDeclSet [ctor] . 1740 op __ : OpDeclSet OpDeclSet -> OpDeclSet 1741 [ctor assoc comm id: none format (d ni d)] . 1742 eq O:OpDecl O:OpDecl = O:OpDecl . 1743 1744*** conditions 1745 sorts EqCondition Condition . 1746 subsort EqCondition < Condition . 1747 op nil : -> EqCondition [ctor] . 1748 op _=_ : Term Term -> EqCondition [ctor prec 71] . 1749 op _:_ : Term Sort -> EqCondition [ctor prec 71] . 1750 op _:=_ : Term Term -> EqCondition [ctor prec 71] . 1751 op _=>_ : Term Term -> Condition [ctor prec 71] . 1752 op _/\_ : EqCondition EqCondition -> EqCondition [ctor assoc id: nil prec 73] . 1753 op _/\_ : Condition Condition -> Condition [ctor assoc id: nil prec 73] . 1754 1755*** membership axioms 1756 sorts MembAx MembAxSet . 1757 subsort MembAx < MembAxSet . 1758 op mb_:_[_]. : Term Sort AttrSet -> MembAx 1759 [ctor format (d d d d s d d s d)] . 1760 op cmb_:_if_[_]. : Term Sort EqCondition AttrSet -> MembAx 1761 [ctor format (d d d d d d s d d s d)] . 1762 op none : -> MembAxSet [ctor] . 1763 op __ : MembAxSet MembAxSet -> MembAxSet 1764 [ctor assoc comm id: none format (d ni d)] . 1765 eq M:MembAx M:MembAx = M:MembAx . 1766 1767*** equations 1768 sorts Equation EquationSet . 1769 subsort Equation < EquationSet . 1770 op eq_=_[_]. : Term Term AttrSet -> Equation 1771 [ctor format (d d d d s d d s d)] . 1772 op ceq_=_if_[_]. : Term Term EqCondition AttrSet -> Equation 1773 [ctor format (d d d d d d s d d s d)] . 1774 op none : -> EquationSet [ctor] . 1775 op __ : EquationSet EquationSet -> EquationSet 1776 [ctor assoc comm id: none format (d ni d)] . 1777 eq E:Equation E:Equation = E:Equation . 1778 1779*** rules 1780 sorts Rule RuleSet . 1781 subsort Rule < RuleSet . 1782 op rl_=>_[_]. : Term Term AttrSet -> Rule 1783 [ctor format (d d d d s d d s d)] . 1784 op crl_=>_if_[_]. : Term Term Condition AttrSet -> Rule 1785 [ctor format (d d d d d d s d d s d)] . 1786 op none : -> RuleSet [ctor] . 1787 op __ : RuleSet RuleSet -> RuleSet 1788 [ctor assoc comm id: none format (d ni d)] . 1789 eq R:Rule R:Rule = R:Rule . 1790 1791*** modules 1792 sorts FModule SModule FTheory STheory Module . 1793 subsorts FModule < SModule < Module . 1794 subsorts FTheory < STheory < Module . 1795 sort Header . 1796 subsort Qid < Header . 1797 op _{_} : Qid ParameterDeclList -> Header [ctor] . 1798 op fmod_is_sorts_.____endfm : Header ImportList SortSet SubsortDeclSet 1799 OpDeclSet MembAxSet EquationSet -> FModule [ctor gather (& & & & & & &) 1800 format (d d s n++i ni d d ni ni ni ni n--i d)] . 1801 op mod_is_sorts_._____endm : Header ImportList SortSet SubsortDeclSet 1802 OpDeclSet MembAxSet EquationSet RuleSet -> SModule 1803 [ctor gather (& & & & & & & &) 1804 format (d d s n++i ni d d ni ni ni ni ni n--i d)] . 1805 op fth_is_sorts_.____endfth : Qid ImportList SortSet SubsortDeclSet 1806 OpDeclSet MembAxSet EquationSet -> FTheory [ctor gather (& & & & & & &) 1807 format (d d d n++i ni d d ni ni ni ni n--i d)] . 1808 op th_is_sorts_._____endth : Qid ImportList SortSet SubsortDeclSet 1809 OpDeclSet MembAxSet EquationSet RuleSet -> STheory 1810 [ctor gather (& & & & & & & &) 1811 format (d d d n++i ni d d ni ni ni ni ni n--i d)] . 1812 op [_] : Qid -> Module . 1813 eq [Q:Qid] = (th Q:Qid is including Q:Qid . 1814 sorts none . none none none none none endth) . 1815 1816*** projection functions 1817 var Q : Qid . 1818 var PDL : ParameterDeclList . 1819 var H : Header . 1820 var M : Module . 1821 var IL : ImportList . 1822 var SS : SortSet . 1823 var SSDS : SubsortDeclSet . 1824 var OPDS : OpDeclSet . 1825 var MAS : MembAxSet . 1826 var EQS : EquationSet . 1827 var RLS : RuleSet . 1828 1829 op getName : Module -> Qid . 1830 eq getName(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = Q . 1831 eq getName(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = Q . 1832 eq getName(fmod Q{PDL} is IL sorts SS . SSDS OPDS MAS EQS endfm) = Q . 1833 eq getName(mod Q{PDL} is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = Q . 1834 eq getName(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = Q . 1835 eq getName(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = Q . 1836 1837 op getImports : Module -> ImportList . 1838 eq getImports(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = IL . 1839 eq getImports(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = IL . 1840 eq getImports(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = IL . 1841 eq getImports(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = IL . 1842 1843 op getSorts : Module -> SortSet . 1844 eq getSorts(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = SS . 1845 eq getSorts(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = SS . 1846 eq getSorts(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = SS . 1847 eq getSorts(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = SS . 1848 1849 op getSubsorts : Module -> SubsortDeclSet . 1850 eq getSubsorts(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = SSDS . 1851 eq getSubsorts(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = SSDS . 1852 eq getSubsorts(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = SSDS . 1853 eq getSubsorts(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = SSDS . 1854 1855 op getOps : Module -> OpDeclSet . 1856 eq getOps(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = OPDS . 1857 eq getOps(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = OPDS . 1858 eq getOps(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = OPDS . 1859 eq getOps(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = OPDS . 1860 1861 op getMbs : Module -> MembAxSet . 1862 eq getMbs(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = MAS . 1863 eq getMbs(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = MAS . 1864 eq getMbs(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = MAS . 1865 eq getMbs(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = MAS . 1866 1867 op getEqs : Module -> EquationSet . 1868 eq getEqs(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = EQS . 1869 eq getEqs(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = EQS . 1870 eq getEqs(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = EQS . 1871 eq getEqs(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = EQS . 1872 1873 op getRls : Module -> RuleSet . 1874 eq getRls(fmod H is IL sorts SS . SSDS OPDS MAS EQS endfm) = none . 1875 eq getRls(mod H is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = RLS . 1876 eq getRls(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = none . 1877 eq getRls(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = RLS . 1878endfm 1879 1880fmod META-VIEW is 1881 protecting META-MODULE . 1882 1883*** sort mappings 1884 sorts SortMapping SortMappingSet . 1885 subsort SortMapping < SortMappingSet . 1886 op sort_to_. : Sort Sort -> SortMapping [ctor] . 1887 op none : -> SortMappingSet [ctor] . 1888 op __ : SortMappingSet SortMappingSet -> SortMappingSet 1889 [ctor assoc comm id: none format (d ni d)] . 1890 eq S:SortMapping S:SortMapping = S:SortMapping . 1891 1892*** operator mappings 1893 sorts OpMapping OpMappingSet . 1894 subsort OpMapping < OpMappingSet . 1895 1896 op (op_to_.) : Qid Qid -> OpMapping [ctor] . 1897 op (op_:_->_to_.) : Qid TypeList Type Qid -> OpMapping [ctor] . 1898 op (op_to term_.) : Term Term -> OpMapping [ctor] . 1899 1900 op none : -> OpMappingSet [ctor] . 1901 op __ : OpMappingSet OpMappingSet -> OpMappingSet 1902 [ctor assoc comm id: none format (d ni d)] . 1903 eq O:OpMapping O:OpMapping = O:OpMapping . 1904 1905 sort View . 1906 op view_from_to_is__endv : Header ModuleExpression ModuleExpression 1907 SortMappingSet OpMappingSet -> View [ctor gather (& & & & &) 1908 format (d d d d d d d n++i ni n--i d)] . 1909 1910*** projection functions 1911 var Q : Qid . 1912 vars ME ME' : ModuleExpression . 1913 var SMS : SortMappingSet . 1914 var OMS : OpMappingSet . 1915 1916 op getName : View -> Qid . 1917 eq getName(view Q from ME to ME' is SMS OMS endv) = Q . 1918 1919 op getFrom : View -> ModuleExpression . 1920 eq getFrom(view Q from ME to ME' is SMS OMS endv) = ME . 1921 1922 op getTo : View -> ModuleExpression . 1923 eq getTo(view Q from ME to ME' is SMS OMS endv) = ME' . 1924 1925 op getSortMappings : View -> SortMappingSet . 1926 eq getSortMappings(view Q from ME to ME' is SMS OMS endv) = SMS . 1927 1928 op getOpMappings : View -> OpMappingSet . 1929 eq getOpMappings(view Q from ME to ME' is SMS OMS endv) = OMS . 1930endfm 1931 1932fmod META-LEVEL is 1933 protecting META-VIEW . 1934 1935*** bounds 1936 sort Bound . 1937 subsort Nat < Bound . 1938 op unbounded : -> Bound [ctor] . 1939 1940*** parents 1941 sort Parent . 1942 subsort Nat < Parent . 1943 op none : -> Parent . 1944 1945*** argument values 1946 sort Type? . 1947 subsort Type < Type? . 1948 op anyType : -> Type? [ctor] . 1949 1950*** options for metaPrettyPrint() 1951 sorts PrintOption PrintOptionSet . 1952 subsort PrintOption < PrintOptionSet . 1953 ops mixfix with-parens flat format number rat : -> PrintOption [ctor] . 1954 op none : -> PrintOptionSet [ctor] . 1955 op __ : PrintOptionSet PrintOptionSet -> PrintOptionSet [ctor assoc comm id: none] . 1956 1957*** unification problems 1958 sorts UnificandPair UnificationProblem . 1959 subsort UnificandPair < UnificationProblem . 1960 op _=?_ : Term Term -> UnificandPair [ctor prec 71] . 1961 op _/\_ : UnificationProblem UnificationProblem -> UnificationProblem [ctor assoc comm prec 73] . 1962 1963*** success results 1964 sorts ResultPair ResultTriple Result4Tuple MatchPair TraceStep Trace 1965 UnificationPair UnificationTriple Variant SmtResult . 1966 subsort TraceStep < Trace . 1967 1968 op {_,_} : Term Type -> ResultPair [ctor] . 1969 op {_,_,_} : Term Type Substitution -> ResultTriple [ctor] . 1970 op {_,_,_,_} : Term Type Substitution Context -> Result4Tuple [ctor] . 1971 op {_,_} : Substitution Context -> MatchPair [ctor] . 1972 op {_,_} : Substitution Nat -> UnificationPair [ctor] . 1973 op {_,_,_} : Substitution Substitution Nat -> UnificationTriple [ctor] . 1974 op {_,_,_,_,_} : Term Substitution Nat Parent Bool -> Variant [ctor] . 1975 op {_,_,_} : Term Type Rule -> TraceStep [ctor] . 1976 op nil : -> Trace [ctor] . 1977 op __ : Trace Trace -> Trace [ctor assoc id: nil format (d n d)] . 1978 op {_,_,_,_} : Term Substitution Term Nat -> SmtResult [ctor] . 1979 1980*** failure results 1981 sorts ResultPair? ResultTriple? Result4Tuple? MatchPair? Substitution? Trace? 1982 UnificationPair? UnificationTriple? Variant? SmtResult? . 1983 subsort ResultPair < ResultPair? . 1984 subsort ResultTriple < ResultTriple? . 1985 subsort Result4Tuple < Result4Tuple? . 1986 subsort MatchPair < MatchPair? . 1987 subsort UnificationPair < UnificationPair? . 1988 subsort UnificationTriple < UnificationTriple? . 1989 subsort Variant < Variant? . 1990 subsort Substitution < Substitution? . 1991 subsort Trace < Trace? . 1992 subsort SmtResult < SmtResult? . 1993 1994 op noParse : Nat -> ResultPair? [ctor] . 1995 op ambiguity : ResultPair ResultPair -> ResultPair? [ctor] . 1996 op failure : -> ResultPair? [ctor] . 1997 1998 op failure : -> ResultTriple? [ctor] . 1999 op failure : -> Result4Tuple? [ctor] . 2000 op noUnifier : -> UnificationPair? [ctor] . 2001 op noUnifier : -> UnificationTriple? [ctor] . 2002 op noUnifierIncomplete : -> UnificationPair? [ctor] . 2003 op noUnifierIncomplete : -> UnificationTriple? [ctor] . 2004 op noVariant : -> Variant? [ctor] . 2005 op noVariantIncomplete : -> Variant? [ctor] . 2006 op noMatch : -> Substitution? [ctor] . 2007 op noMatch : -> MatchPair? [ctor] . 2008 op failure : -> Trace? [ctor] . 2009 op failure : -> SmtResult? [ctor] . 2010 2011*** projection functions 2012 op getTerm : ResultPair -> Term . 2013 eq getTerm({T:Term, T:Type}) = T:Term . 2014 op getType : ResultPair -> Type . 2015 eq getType({T:Term, T:Type}) = T:Type . 2016 2017 op getTerm : ResultTriple -> Term . 2018 eq getTerm({T:Term, T:Type, S:Substitution}) = T:Term . 2019 op getType : ResultTriple -> Type . 2020 eq getType({T:Term, T:Type, S:Substitution}) = T:Type . 2021 op getSubstitution : ResultTriple -> Substitution . 2022 eq getSubstitution({T:Term, T:Type, S:Substitution}) = S:Substitution . 2023 2024 op getTerm : Result4Tuple -> Term . 2025 eq getTerm({T:Term, T:Type, S:Substitution, C:Context}) = T:Term . 2026 op getType : Result4Tuple -> Type . 2027 eq getType({T:Term, T:Type, S:Substitution, C:Context}) = T:Type . 2028 op getSubstitution : Result4Tuple -> Substitution . 2029 eq getSubstitution({T:Term, T:Type, S:Substitution, C:Context}) = S:Substitution . 2030 op getContext : Result4Tuple -> Context . 2031 eq getContext({T:Term, T:Type, S:Substitution, C:Context}) = C:Context . 2032 2033 op getSubstitution : MatchPair -> Substitution . 2034 eq getSubstitution({S:Substitution, C:Context}) = S:Substitution . 2035 op getContext : MatchPair -> Context . 2036 eq getContext({S:Substitution, C:Context}) = C:Context . 2037 2038*** descent functions 2039 op metaReduce : Module Term ~> ResultPair 2040 [special ( 2041 id-hook MetaLevelOpSymbol (metaReduce) 2042 2043 op-hook qidSymbol (<Qids> : ~> Qid) 2044 op-hook metaTermSymbol (_[_] : Qid NeTermList ~> Term) 2045 op-hook metaArgSymbol (_,_ : NeTermList NeTermList ~> NeTermList) 2046 op-hook emptyTermListSymbol (empty : ~> GroundTermList) 2047 2048 op-hook assignmentSymbol (_<-_ : Qid Term ~> Assignment) 2049 op-hook substitutionSymbol 2050 (_;_ : Substitution Substitution ~> Substitution) 2051 op-hook emptySubstitutionSymbol (none : ~> Substitution) 2052 op-hook holeSymbol ([] : ~> Context) 2053 2054 op-hook headerSymbol (_{_} : Qid ParameterDeclList ~> Header) 2055 op-hook parameterDeclSymbol (_::_ : Sort ModuleExpression ~> ParameterDecl) 2056 op-hook parameterDeclListSymbol (_,_ : ParameterDeclList ParameterDeclList ~> ParameterDeclList) 2057 2058 op-hook emptyAttrSetSymbol (none : ~> AttrSet) 2059 op-hook attrSetSymbol (__ : AttrSet AttrSet ~> AttrSet) 2060 2061 op-hook sortRenamingSymbol (sort_to_ : Qid Qid ~> Renaming) 2062 op-hook opRenamingSymbol (op_to_[_] : Qid Qid AttrSet ~> Renaming) 2063 op-hook opRenamingSymbol2 2064 (op_:_->_to_[_] : Qid TypeList Type Qid AttrSet ~> Renaming) 2065 op-hook labelRenamingSymbol (label_to_ : Qid Qid ~> Renaming) 2066 op-hook renamingSetSymbol (_,_ : RenamingSet RenamingSet ~> RenamingSet) 2067 2068 op-hook sumSymbol 2069 (_+_ : ModuleExpression ModuleExpression ~> ModuleExpression) 2070 op-hook renamingSymbol 2071 (_*(_) : ModuleExpression RenamingSet ~> ModuleExpression) 2072 op-hook instantiationSymbol 2073 (_{_} : ModuleExpression ParameterList ~> ModuleExpression) 2074 2075 op-hook protectingSymbol (protecting_. : ModuleExpression ~> Import) 2076 op-hook extendingSymbol (extending_. : ModuleExpression ~> Import) 2077 op-hook includingSymbol (including_. : ModuleExpression ~> Import) 2078 op-hook nilImportListSymbol (nil : ~> ImportList) 2079 op-hook importListSymbol (__ : ImportList ImportList ~> ImportList) 2080 2081 op-hook emptySortSetSymbol (none : ~> SortSet) 2082 op-hook sortSetSymbol (_;_ : SortSet SortSet ~> SortSet) 2083 2084 op-hook subsortSymbol (subsort_<_. : Sort Sort ~> SubsortDecl) 2085 op-hook emptySubsortDeclSetSymbol (none : ~> SubsortDeclSet) 2086 op-hook subsortDeclSetSymbol 2087 (__ : SubsortDeclSet SubsortDeclSet ~> SubsortDeclSet) 2088 2089 op-hook nilQidListSymbol (nil : ~> QidList) 2090 op-hook qidListSymbol (__ : QidList QidList ~> QidList) 2091 2092 op-hook succSymbol (s_ : Nat ~> NzNat) 2093 op-hook natListSymbol (__ : NeNatList NeNatList ~> NeNatList) 2094 op-hook unboundedSymbol (unbounded : ~> Bound) 2095 op-hook noParentSymbol (none : ~> Parent) 2096 2097 op-hook stringSymbol (<Strings> : ~> String) 2098 op-hook idHookSymbol (id-hook : Qid QidList ~> Hook) 2099 op-hook opHookSymbol (op-hook : Qid Qid QidList Qid ~> Hook) 2100 op-hook termHookSymbol (term-hook : Qid Term ~> Hook) 2101 op-hook hookListSymbol (__ : HookList HookList ~> HookList) 2102 2103 op-hook assocSymbol (assoc : ~> Attr) 2104 op-hook commSymbol (comm : ~> Attr) 2105 op-hook idemSymbol (idem : ~> Attr) 2106 op-hook iterSymbol (iter : ~> Attr) 2107 op-hook idSymbol (id : Term ~> Attr) 2108 op-hook leftIdSymbol (left-id : Term ~> Attr) 2109 op-hook rightIdSymbol (right-id : Term ~> Attr) 2110 op-hook stratSymbol (strat : NeNatList ~> Attr) 2111 op-hook memoSymbol (memo : ~> Attr) 2112 op-hook precSymbol (prec : Nat ~> Attr) 2113 op-hook gatherSymbol (gather : QidList ~> Attr) 2114 op-hook formatSymbol (format : QidList ~> Attr) 2115 op-hook ctorSymbol (ctor : ~> Attr) 2116 op-hook frozenSymbol (frozen : NeNatList ~> Attr) 2117 op-hook polySymbol (poly : NeNatList ~> Attr) 2118 op-hook configSymbol (config : ~> Attr) 2119 op-hook objectSymbol (object : ~> Attr) 2120 op-hook msgSymbol (msg : ~> Attr) 2121 op-hook specialSymbol (special : NeHookList ~> Attr) 2122 2123 op-hook labelSymbol (label : Qid ~> Attr) 2124 op-hook metadataSymbol (metadata : String ~> Attr) 2125 op-hook owiseSymbol (owise : ~> Attr) 2126 op-hook variantAttrSymbol (variant : ~> Attr) 2127 op-hook nonexecSymbol (nonexec : ~> Attr) 2128 op-hook printSymbol (print : QidList ~> Attr) 2129 2130 op-hook opDeclSymbol 2131 (op_:_->_[_]. : Qid TypeList Type AttrSet ~> OpDecl) 2132 op-hook emptyOpDeclSetSymbol (none : ~> OpDeclSet) 2133 op-hook opDeclSetSymbol (__ : OpDeclSet OpDeclSet ~> OpDeclSet) 2134 2135 op-hook noConditionSymbol (nil : ~> EqCondition) 2136 op-hook equalityConditionSymbol (_=_ : Term Term ~> EqCondition) 2137 op-hook sortTestConditionSymbol (_:_ : Term Sort ~> EqCondition) 2138 op-hook matchConditionSymbol (_:=_ : Term Term ~> EqCondition) 2139 op-hook rewriteConditionSymbol (_=>_ : Term Term ~> Condition) 2140 op-hook conjunctionSymbol (_/\_ : Condition Condition ~> Condition) 2141 2142 op-hook mbSymbol (mb_:_[_]. : Term Sort AttrSet ~> MembAx) 2143 op-hook cmbSymbol 2144 (cmb_:_if_[_]. : Term Sort EqCondition AttrSet ~> MembAx) 2145 op-hook emptyMembAxSetSymbol (none : ~> MembAxSet) 2146 op-hook membAxSetSymbol (__ : MembAxSet MembAxSet ~> MembAxSet) 2147 2148 op-hook eqSymbol (eq_=_[_]. : Term Term AttrSet ~> Equation) 2149 op-hook ceqSymbol 2150 (ceq_=_if_[_]. : Term Term EqCondition AttrSet ~> Equation) 2151 op-hook emptyEquationSetSymbol (none : ~> EquationSet) 2152 op-hook equationSetSymbol 2153 (__ : EquationSet EquationSet ~> EquationSet) 2154 2155 op-hook rlSymbol (rl_=>_[_]. : Term Term AttrSet ~> Rule) 2156 op-hook crlSymbol 2157 (crl_=>_if_[_]. : Term Term Condition AttrSet ~> Rule) 2158 op-hook emptyRuleSetSymbol (none : ~> RuleSet) 2159 op-hook ruleSetSymbol (__ : RuleSet RuleSet ~> RuleSet) 2160 2161 op-hook fmodSymbol 2162 (fmod_is_sorts_.____endfm : 2163 Qid ImportList SortSet SubsortDeclSet OpDeclSet 2164 MembAxSet EquationSet ~> FModule) 2165 op-hook fthSymbol 2166 (fth_is_sorts_.____endfth : 2167 Qid ImportList SortSet SubsortDeclSet OpDeclSet 2168 MembAxSet EquationSet ~> FModule) 2169 op-hook modSymbol 2170 (mod_is_sorts_._____endm : 2171 Qid ImportList SortSet SubsortDeclSet OpDeclSet 2172 MembAxSet EquationSet RuleSet ~> Module) 2173 op-hook thSymbol 2174 (th_is_sorts_._____endth : 2175 Qid ImportList SortSet SubsortDeclSet OpDeclSet 2176 MembAxSet EquationSet RuleSet ~> Module) 2177 2178 op-hook sortMappingSymbol (sort_to_. : Sort Sort ~> SortMapping [ctor] .) 2179 op-hook emptySortMappingSetSymbol (none : ~> SortMappingSet) 2180 op-hook sortMappingSetSymbol 2181 (__ : SortMappingSet SortMappingSet ~> SortMappingSet) 2182 2183 op-hook opMappingSymbol (op_to_. : Qid Qid ~> OpMapping) 2184 op-hook opSpecificMappingSymbol (op_:_->_to_. : Qid TypeList Type Qid ~> OpMapping) 2185 op-hook opTermMappingSymbol (op_to`term_. : Term Term ~> OpMapping) 2186 2187 op-hook emptyOpMappingSetSymbol (none : ~> OpMappingSet) 2188 op-hook opMappingSetSymbol 2189 (__ : OpMappingSet OpMappingSet ~> OpMappingSet) 2190 2191 op-hook viewSymbol 2192 (view_from_to_is__endv : Header ModuleExpression ModuleExpression 2193 SortMappingSet OpMappingSet ~> View) 2194 2195 op-hook anyTypeSymbol (anyType : ~> Type?) 2196 2197 op-hook unificandPairSymbol (_=?_ : Term Term ~> UnificandPair) 2198 op-hook unificationConjunctionSymbol 2199 (_/\_ : UnificationProblem UnificationProblem ~> UnificationProblem) 2200 2201 op-hook resultPairSymbol ({_,_} : Term Type ~> ResultPair) 2202 op-hook resultTripleSymbol 2203 ({_,_,_} : Term Type Substitution ~> ResultTriple) 2204 op-hook result4TupleSymbol 2205 ({_,_,_,_} : Term Type Substitution Context ~> Result4Tuple) 2206 op-hook matchPairSymbol ({_,_} : Substitution Context ~> MatchPair) 2207 op-hook unificationPairSymbol ({_,_} : Substitution Nat ~> UnificationPair) 2208 op-hook unificationTripleSymbol ({_,_,_} : Substitution Substitution Nat ~> UnificationTriple) 2209 op-hook variantSymbol ({_,_,_,_,_} : Term Substitution Nat Parent Bool ~> Variant) 2210 op-hook smtResultSymbol ({_,_,_,_} : Term Substitution Term Nat ~> SmtResult) 2211 2212 op-hook traceStepSymbol ({_,_,_} : Term Type Rule ~> TraceStep) 2213 op-hook nilTraceSymbol (nil : ~> Trace) 2214 op-hook traceSymbol (__ : Trace Trace ~> Trace) 2215 2216 op-hook noParseSymbol (noParse : Nat ~> ResultPair?) 2217 op-hook ambiguitySymbol (ambiguity : ResultPair ResultPair ~> ResultPair?) 2218 op-hook failure2Symbol (failure : ~> ResultPair?) 2219 op-hook failure3Symbol (failure : ~> ResultTriple?) 2220 op-hook failure4Symbol (failure : ~> Result4Tuple?) 2221 op-hook noUnifierPairSymbol (noUnifier : ~> UnificationPair?) 2222 op-hook noUnifierTripleSymbol (noUnifier : ~> UnificationTriple?) 2223 op-hook noUnifierIncompletePairSymbol (noUnifierIncomplete : ~> UnificationPair?) 2224 op-hook noUnifierIncompleteTripleSymbol (noUnifierIncomplete : ~> UnificationTriple?) 2225 op-hook noVariantSymbol (noVariant : ~> Variant?) 2226 op-hook noVariantIncompleteSymbol (noVariantIncomplete : ~> Variant?) 2227 op-hook noMatchSubstSymbol (noMatch : ~> Substitution?) 2228 op-hook noMatchPairSymbol (noMatch : ~> MatchPair?) 2229 op-hook failureTraceSymbol (failure : ~> Trace?) 2230 op-hook smtFailureSymbol (failure : ~> SmtResult?) 2231 2232 op-hook mixfixSymbol (mixfix : ~> PrintOption) 2233 op-hook withParensSymbol (with-parens : ~> PrintOption) 2234 op-hook flatSymbol (flat : ~> PrintOption) 2235 op-hook formatPrintOptionSymbol (format : ~> PrintOption) 2236 op-hook numberSymbol (number : ~> PrintOption) 2237 op-hook ratSymbol (rat : ~> PrintOption) 2238 op-hook emptyPrintOptionSetSymbol (none : ~> PrintOptionSet) 2239 op-hook printOptionSetSymbol (__ : PrintOptionSet PrintOptionSet ~> PrintOptionSet) 2240 2241 term-hook trueTerm (true) 2242 term-hook falseTerm (false))] . 2243 2244 op metaNormalize : Module Term ~> ResultPair 2245 [special ( 2246 id-hook MetaLevelOpSymbol (metaNormalize) 2247 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2248 2249 op metaRewrite : Module Term Bound ~> ResultPair 2250 [special ( 2251 id-hook MetaLevelOpSymbol (metaRewrite) 2252 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2253 2254 op metaFrewrite : Module Term Bound Nat ~> ResultPair 2255 [special ( 2256 id-hook MetaLevelOpSymbol (metaFrewrite) 2257 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2258 2259 op metaApply : Module Term Qid Substitution Nat ~> ResultTriple? 2260 [special ( 2261 id-hook MetaLevelOpSymbol (metaApply) 2262 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2263 2264 op metaXapply : Module Term Qid Substitution Nat Bound Nat ~> Result4Tuple? 2265 [special ( 2266 id-hook MetaLevelOpSymbol (metaXapply) 2267 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2268 2269 op metaMatch : Module Term Term Condition Nat ~> Substitution? 2270 [special ( 2271 id-hook MetaLevelOpSymbol (metaMatch) 2272 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2273 2274 op metaXmatch : Module Term Term Condition Nat Bound Nat ~> MatchPair? 2275 [special ( 2276 id-hook MetaLevelOpSymbol (metaXmatch) 2277 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2278 2279 op metaUnify : Module UnificationProblem Nat Nat ~> UnificationPair? 2280 [special ( 2281 id-hook MetaLevelOpSymbol (metaUnify) 2282 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2283 2284 op metaDisjointUnify : Module UnificationProblem Nat Nat ~> UnificationTriple? 2285 [special ( 2286 id-hook MetaLevelOpSymbol (metaDisjointUnify) 2287 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2288 2289 op metaSearch : Module Term Term Condition Qid Bound Nat ~> ResultTriple? 2290 [special ( 2291 id-hook MetaLevelOpSymbol (metaSearch) 2292 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2293 2294 op metaSearchPath : Module Term Term Condition Qid Bound Nat ~> Trace? 2295 [special ( 2296 id-hook MetaLevelOpSymbol (metaSearchPath) 2297 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2298 2299 op metaNarrow : Module Term Term Qid Bound Nat ~> ResultTriple? 2300 [special ( 2301 id-hook MetaLevelOpSymbol (metaNarrow) 2302 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2303 2304 op metaNarrow : Module Term Qid Bound Bool Nat ~> ResultPair? 2305 [special ( 2306 id-hook MetaLevelOpSymbol (metaNarrow2) 2307 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2308 2309 op metaGetVariant : Module Term TermList Nat Nat ~> Variant? 2310 [special ( 2311 id-hook MetaLevelOpSymbol (metaGetVariant) 2312 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2313 2314 op metaGetIrredundantVariant : Module Term TermList Nat Nat ~> Variant? 2315 [special ( 2316 id-hook MetaLevelOpSymbol (metaGetIrredundantVariant) 2317 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2318 2319 op metaVariantUnify : Module UnificationProblem TermList Nat Nat ~> UnificationPair? 2320 [special ( 2321 id-hook MetaLevelOpSymbol (metaVariantUnify) 2322 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2323 2324 op metaVariantDisjointUnify : Module UnificationProblem TermList Nat Nat ~> UnificationTriple? 2325 [special ( 2326 id-hook MetaLevelOpSymbol (metaVariantDisjointUnify) 2327 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2328 2329 op sortLeq : Module Type Type ~> Bool 2330 [special ( 2331 id-hook MetaLevelOpSymbol (metaSortLeq) 2332 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2333 2334 op sameKind : Module Type Type ~> Bool 2335 [special ( 2336 id-hook MetaLevelOpSymbol (metaSameKind) 2337 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2338 2339 op lesserSorts : Module Type ~> SortSet 2340 [special ( 2341 id-hook MetaLevelOpSymbol (metaLesserSorts) 2342 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2343 2344 op glbSorts : Module Type Type ~> TypeSet 2345 [special ( 2346 id-hook MetaLevelOpSymbol (metaGlbSorts) 2347 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2348 2349 op leastSort : Module Term ~> Type 2350 [special ( 2351 id-hook MetaLevelOpSymbol (metaLeastSort) 2352 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2353 2354 op completeName : Module Type ~> Type 2355 [special ( 2356 id-hook MetaLevelOpSymbol (metaCompleteName) 2357 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2358 2359 op metaParse : Module QidList Type? ~> ResultPair? 2360 [special ( 2361 id-hook MetaLevelOpSymbol (metaParse) 2362 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2363 2364 op metaPrettyPrint : Module Term PrintOptionSet ~> QidList 2365 [special ( 2366 id-hook MetaLevelOpSymbol (metaPrettyPrint) 2367 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2368 2369 op metaCheck : Module Term ~> Bool 2370 [special ( 2371 id-hook MetaLevelOpSymbol (metaCheck) 2372 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2373 2374 op metaSmtSearch : Module Term Term Condition Qid Nat Bound Nat ~> SmtResult? 2375 [special ( 2376 id-hook MetaLevelOpSymbol (metaSmtSearch) 2377 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2378 2379 op wellFormed : Module -> Bool 2380 [special ( 2381 id-hook MetaLevelOpSymbol (metaWellFormedModule) 2382 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2383 2384 op wellFormed : Module Term ~> Bool 2385 [special ( 2386 id-hook MetaLevelOpSymbol (metaWellFormedTerm) 2387 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2388 2389 op wellFormed : Module Substitution ~> Bool 2390 [special ( 2391 id-hook MetaLevelOpSymbol (metaWellFormedSubstitution) 2392 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2393 2394 op getKind : Module Type ~> Kind 2395 [special ( 2396 id-hook MetaLevelOpSymbol (metaGetKind) 2397 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2398 2399 op getKinds : Module ~> KindSet 2400 [special ( 2401 id-hook MetaLevelOpSymbol (metaGetKinds) 2402 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2403 2404 op maximalSorts : Module Kind ~> SortSet 2405 [special ( 2406 id-hook MetaLevelOpSymbol (metaMaximalSorts) 2407 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2408 2409 op minimalSorts : Module Kind ~> SortSet 2410 [special ( 2411 id-hook MetaLevelOpSymbol (metaMinimalSorts) 2412 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2413 2414 op maximalAritySet : Module Qid TypeList Sort ~> TypeListSet 2415 [special ( 2416 id-hook MetaLevelOpSymbol (metaMaximalAritySet) 2417 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2418 2419 op upModule : Qid Bool ~> Module 2420 [special ( 2421 id-hook MetaLevelOpSymbol (metaUpModule) 2422 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2423 2424 op upImports : Qid ~> ImportList 2425 [special ( 2426 id-hook MetaLevelOpSymbol (metaUpImports) 2427 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2428 2429 op upSorts : Qid Bool ~> SortSet 2430 [special ( 2431 id-hook MetaLevelOpSymbol (metaUpSorts) 2432 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2433 2434 op upSubsortDecls : Qid Bool ~> SubsortDeclSet 2435 [special ( 2436 id-hook MetaLevelOpSymbol (metaUpSubsortDecls) 2437 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2438 2439 op upOpDecls : Qid Bool ~> OpDeclSet 2440 [special ( 2441 id-hook MetaLevelOpSymbol (metaUpOpDecls) 2442 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2443 2444 op upMbs : Qid Bool ~> MembAxSet 2445 [special ( 2446 id-hook MetaLevelOpSymbol (metaUpMbs) 2447 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2448 2449 op upEqs : Qid Bool ~> EquationSet 2450 [special ( 2451 id-hook MetaLevelOpSymbol (metaUpEqs) 2452 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2453 2454 op upRls : Qid Bool ~> RuleSet 2455 [special ( 2456 id-hook MetaLevelOpSymbol (metaUpRls) 2457 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2458 2459 op upView : Qid ~> View 2460 [special ( 2461 id-hook MetaLevelOpSymbol (metaUpView) 2462 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2463 2464 op upTerm : Universal -> Term 2465 [poly (1) 2466 special ( 2467 id-hook MetaLevelOpSymbol (metaUpTerm) 2468 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2469 2470 op downTerm : Term Universal -> Universal 2471 [poly (2 0) 2472 special ( 2473 id-hook MetaLevelOpSymbol (metaDownTerm) 2474 op-hook shareWith (metaReduce : Module Term ~> ResultPair))] . 2475 2476*** backward compatibility 2477 op metaPrettyPrint : Module Term ~> QidList . 2478 eq metaPrettyPrint(M:Module, T:Term) = metaPrettyPrint(M:Module, T:Term, mixfix flat format number rat) . 2479endfm 2480 2481*** 2482*** System modules. 2483*** 2484 2485mod COUNTER is 2486 protecting NAT . 2487 op counter : -> [Nat] 2488 [special (id-hook CounterSymbol 2489 op-hook succSymbol (s_ : Nat ~> NzNat))] . 2490endm 2491 2492mod LOOP-MODE is 2493 protecting QID-LIST . 2494 sorts State System . 2495 op [_,_,_] : QidList State QidList -> System 2496 [ctor special ( 2497 id-hook LoopSymbol 2498 op-hook qidSymbol (<Qids> : ~> Qid) 2499 op-hook nilQidListSymbol (nil : ~> QidList) 2500 op-hook qidListSymbol (__ : QidList QidList ~> QidList))] . 2501endm 2502 2503mod CONFIGURATION is 2504 sorts Attribute AttributeSet . 2505 subsort Attribute < AttributeSet . 2506 op none : -> AttributeSet [ctor] . 2507 op _,_ : AttributeSet AttributeSet -> AttributeSet [ctor assoc comm id: none] . 2508 2509 sorts Oid Cid Object Msg Portal Configuration . 2510 subsort Object Msg Portal < Configuration . 2511 op <_:_|_> : Oid Cid AttributeSet -> Object [ctor object] . 2512 op none : -> Configuration [ctor] . 2513 op __ : Configuration Configuration -> Configuration [ctor config assoc comm id: none] . 2514 op <> : -> Portal [ctor] . 2515endm 2516 2517set include BOOL on . 2518set omod include CONFIGURATION on . 2519 2520select CONVERSION . 2521