1\documentclass{article} 2\usepackage{hyperref} 3\newtheorem{Example}{Example} 4\newcommand{\file}[1]{\texttt{#1}} 5\newcommand{\xAldor}{\textsc{Aldor}} 6\newcommand{\xFriCAS}{\textsc{FriCAS}} 7\usepackage{color} 8\definecolor{bgcode}{rgb}{1,1,0.7} 9\usepackage{listings} 10\lstnewenvironment{code}% 11 {\lstset{basicstyle=\scriptsize\ttfamily,backgroundcolor=\color{bgcode}}}% 12 {} 13 14\begin{document} 15\title{Comments on ax.boot} 16\author{Ralf Hemmecke} 17\date{19-Jun-2008} 18\maketitle 19\begin{abstract} 20 We give an overview of what \file{ax.boot} does and in particular 21 describe the function \verb'makeAxExportForm'. 22\end{abstract} 23\tableofcontents 24 25%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 26\section{Overview} 27%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 28The most important function in \file{ax.boot} is the function 29\verb'makeAxExportForm'. 30% 31The function takes as input a filename and a list of constructors. 32Via LISP it would be called like 33\begin{code} 34(|makeAxExportForm| filename constructors) 35\end{code} 36where \verb'filename' is actually unused and could be removed and 37\verb'constructors' should be a list of constructor names, i.e., names 38of categories, domains, and packages in their unabbreviated form. 39 40For example, in the following way this function is called from within 41a fricas session. 42\begin{code} 43cd /path/to/fricas 44fricas -nosman 45)read src/interp/ax.boot 46)boot makeAxExportForm("unused", (list 'DirectProductCategory)) 47\end{code} 48 49It returns a list that represents the \texttt{.ap} (parsed source) 50(see \verb'aldor -hall') form of the constructors. However, since the 51output is only needed for a construction of an \xAldor{} \xFriCAS{} 52interaction, \verb'makeAxExportForm' will only construct the category 53part of the constructor. 54 55The function is actually used in \file{src/aldor/gendepap.lsp} and is an 56auxiliary part in the construction of the interface for the 57interaction of the \xAldor{} compiler with \xFriCAS{}. 58 59 60 61The basic translation is easily demonstrated with a few examples. For 62better readability, we look at the corresponding SPAD form of the 63constructor (instead of its internal LISP representation). 64 65Let us first state what different situations we identified. 66\begin{enumerate} 67\item Ordinary domains. See Section~\ref{sec:Domain}. 68\item Ordinary categories. See Section~\ref{sec:Category}. 69\item Ordinary categories with default packages. See 70 Section~\ref{sec:Category+Default}. 71\item Ordinary categories with default packages that contain 72 conditional implementations. See 73 Section~\ref{sec:Category+ConditionalDefault}. 74\item Initial domains, i.e., domains that will be extended in the 75 course of building \file{libfricas.al}. These domains are listed in 76 the variable \verb'$extendedDomains'. %$ 77 78 See Sections~\ref{sec:InitDomain} and 79 \ref{sec:ParametrizedInitDomain}. There is a subdivision for these 80 domains. 81 \begin{enumerate} 82 \item For domains that take no arguments, see 83 Section~\ref{sec:InitDomain}. 84 \item For domains that take arguments, see 85 Section~\ref{sec:ParametrizedInitDomain}. 86 \end{enumerate} 87\end{enumerate} 88 89 90 91 92 93%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 94\section{Ordinary Domains}\label{sec:Domain} 95%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 96The domain \verb'Stack'. 97\begin{code} 98Stack(S:SetCategory): StackAggregate S with 99 stack: List S -> % 100 == add 101 Rep := Reference List S 102 ... 103\end{code} 104It is translated into \ldots 105\begin{code} 106(|Sequence| (|Import| NIL |FriCASLib|) (|Import| NIL |Boolean|) 107 (|Export| 108 (|Declare| |Stack| 109 (|Apply| -> (|Declare| |#1| |SetCategory|) 110 (|With| NIL 111 (|Sequence| 112 (|Apply| |StackAggregate| |#1|) 113 (|Declare| |stack| 114 (|Apply| -> 115 (|Comma| (|Apply| |List| |#1|)) 116 %)))))) 117 NIL NIL)) 118\end{code} 119That is the parsed source of the Aldor code \ldots 120\begin{code} 121import from FriCASLib; 122import from Boolean; 123export Stack: (T: SetCategory) -> with { 124 StackAggregate T; 125 stack: List T -> %; 126 } 127\end{code} 128Note that nothing appears before the \verb'with'. No problem because 129that is equivalent to a \verb'Join' in Aldor. 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 150\section{Ordinary Categories}\label{sec:Category} 151%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 152The category \verb'SquareFreeNormalizedTriangularSetCategory' without 153a default package. 154\begin{code} 155SquareFreeNormalizedTriangularSetCategory(_ 156 R: GcdDomain,_ 157 E: OrderedAbelianMonoidSup,_ 158 V: OrderedSet,_ 159 P:RecursivePolynomialCategory(R, E, V)): Category == 160 Join(_ 161 SquareFreeRegularTriangularSetCategory(R,E,V,P),_ 162 NormalizedTriangularSetCategory(R,E,V,P)) 163\end{code} 164It is translated into \ldots 165\begin{code} 166(|Sequence| (|Import| NIL |FriCASLib|) (|Import| NIL |Boolean|) 167 (|Define| 168 (|Declare| |SquareFreeNormalizedTriangularSetCategory| 169 (|Apply| -> 170 (|Comma| (|Declare| |#1| |GcdDomain|) 171 (|Declare| |#2| 172 |OrderedAbelianMonoidSup|) 173 (|Declare| |#3| |OrderedSet|) 174 (|Declare| |#4| 175 (|Apply| |RecursivePolynomialCategory| 176 |#1| |#2| |#3|))) 177 |Category|)) 178 (|Lambda| 179 (|Comma| (|Declare| |#1| |GcdDomain|) 180 (|Declare| |#2| |OrderedAbelianMonoidSup|) 181 (|Declare| |#3| |OrderedSet|) 182 (|Declare| |#4| 183 (|Apply| |RecursivePolynomialCategory| |#1| 184 |#2| |#3|))) 185 |Category| 186 (|Label| |SquareFreeNormalizedTriangularSetCategory| 187 (|With| NIL 188 (|Sequence| 189 (|Apply| |SquareFreeRegularTriangularSetCategory| 190 |#1| |#2| |#3| |#4|) 191 (|Apply| |NormalizedTriangularSetCategory| 192 |#1| |#2| |#3| |#4|))))))) 193\end{code} 194That is the parsed source of the Aldor code \ldots 195\begin{code} 196import from FriCASLib; 197import from Boolean; 198SquareFreeNormalizedTriangularSetCategory: ( 199 R: GcdDomain, 200 E: OrderedAbelianMonoidSup, 201 V: OrderedSet, 202 P: RecursivePolynomialCategory(R, E, V) 203) -> Category == ( 204 R: GcdDomain, 205 E: OrderedAbelianMonoidSup, 206 V: OrderedSet, 207 P: RecursivePolynomialCategory(R, E, V) 208): Category +-> with { 209 SquareFreeRegularTriangularSetCategory(R, E, V, P), 210 NormalizedTriangularSetCategory(R, E, V, P) 211} 212\end{code} 213 Again, nothing appears in front of the \verb'with'. No problem 214 because that is equivalent to a \verb'Join' in Aldor. 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 234\section{Ordinary Categories with Default Packages} 235\label{sec:Category+Default} 236%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 237The category \verb'StringAggregate' with default package. 238\begin{code} 239StringAggregate: Category == OneDimensionalArrayAggregate Character with 240 lowerCase : % -> % 241 lowerCase_!: % -> % 242 upperCase : % -> % 243 ... 244 rightTrim: (%, CharacterClass) -> % 245 elt: (%, %) -> % 246 add 247 trim(s: %, c: Character) == leftTrim(rightTrim(s, c), c) 248 trim(s: %, cc: CharacterClass) == leftTrim(rightTrim(s, cc), cc) 249 lowerCase s == lowerCase_! copy s 250 upperCase s == upperCase_! copy s 251 prefix?(s, t) == substring?(s, t, minIndex t) 252 coerce(c:Character):% == new(1, c) 253 elt(s:%, t:%): % == concat(s,t)$% 254\end{code} 255It is translated into \ldots 256\begin{code} 257(|Sequence| (|Import| NIL |FriCASLib|) (|Import| NIL |Boolean|) 258 (|Foreign| (|Declare| |dummyDefault| |Exit|) |Lisp|) 259 (|Define| (|Declare| |StringAggregate| |Category|) 260 (|With| NIL 261 (|Sequence| 262 (|Apply| |OneDimensionalArrayAggregate| 263 |Character|) 264 (|Declare| |lowerCase| (|Apply| -> (|Comma| %) %)) 265 (|Declare| |lowerCase!| (|Apply| -> (|Comma| %) %)) 266 (|Declare| |upperCase| (|Apply| -> (|Comma| %) %)) 267 ... 268 (|Declare| |rightTrim| 269 (|Apply| -> (|Comma| % |CharacterClass|) %)) 270 (|Declare| |apply| (|Apply| -> (|Comma| % %) %)) 271 (|Default| 272 (|Sequence| 273 (|Define| 274 (|Declare| |coerce| 275 (|Apply| -> (|Comma| |Character|) 276 %)) 277 (|Lambda| 278 (|Comma| 279 (|Declare| |t#1| |Character|)) 280 % 281 (|Label| |coerce| |dummyDefault|))) 282 (|Define| 283 (|Declare| |apply| 284 (|Apply| -> (|Comma| % %) %)) 285 (|Lambda| 286 (|Comma| (|Declare| |t#1| %) 287 (|Declare| |t#2| %)) 288 % (|Label| |apply| |dummyDefault|))) 289 (|Define| 290 (|Declare| |lowerCase| 291 (|Apply| -> (|Comma| %) %)) 292 (|Lambda| (|Comma| (|Declare| |t#1| %)) 293 % 294 (|Label| |lowerCase| 295 |dummyDefault|))) 296 ... 297 )))))) 298\end{code} 299That is the parsed source of the Aldor code \ldots 300\begin{code} 301import from FriCASLib; 302import from Boolean; 303import dummyDefault: Exit from Foreign Lisp; 304StringAggregate: Category == with { 305 OneDimensionalArrayAggregate Character; 306 lowerCase: % -> %; 307 lowerCase!: % -> %; 308 upperCase: % -> %; 309 ... 310 rightTrim: (%, CharacterClass) -> %; 311 apply: (%, %) -> % 312 default { 313 coerce: Character -> % == (t: Character): % +-> dummyDefault; 314 apply: (%, %) -> % == (t1: %, t2: %): % +-> dummyDefault; 315 lowerCase: % -> % == (t: %): % +-> dummyDefault; 316 ... 317} 318\end{code} 319It is important to note that the actual default functions are given by 320a dummy implementation that is imported from LISP. 321 322And again, nothing appears in front of the \verb'with'. No problem 323because that is equivalent to a \verb'Join' in Aldor. 324 325Note that the \verb'elt' function is translated into \verb'apply'. 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 346\section{Ordinary Categories with Conditional Default Packages} 347\label{sec:Category+ConditionalDefault}. 348%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 349 350The category \verb'DirectProductCategory' with default conditional 351exports and conditional default implementations. 352 353 354 355\begin{code} 356DirectProductCategory(dim : NonNegativeInteger, R : Type) : Category == 357 Join(IndexedAggregate(Integer, R), CoercibleTo Vector R, _ 358 AbelianProductCategory(R), finiteAggregate) with 359 -- attribute to indicate an aggregate of finite size 360 directProduct : Vector R -> % 361 ++ directProduct(v) converts the vector v to 362 ++ a direct product. Error: if the length of v is 363 ++ different from dim. 364 if R has SetCategory then FullyRetractableTo R 365 if R has Ring then 366 DifferentialExtension R 367 FullyLinearlyExplicitOver R 368 if R has AbelianMonoid and R has Monoid then 369 unitVector : PositiveInteger -> % 370 ++ unitVector(n) produces a vector with 1 in position n and 371 ++ zero elsewhere. 372 if R has SemiRng then 373 SemiRng 374 BiModule(R, R) 375 if R has AbelianMonoid then 376 dot : (%, %) -> R 377 ++ dot(x, y) computes the inner product of the vectors x and y. 378 if R has Monoid then Monoid 379 if R has SemiGroup then 380 SemiGroup 381 _* : (R, %) -> % 382 ++ r * y multiplies the element r times each component of the 383 ++ vector y. 384 _* : (%, R) -> % 385 ++ y * r multiplies each component of the vector y by the element r. 386 if R has Finite then Finite 387 if R has CommutativeRing then 388 Algebra R 389 CommutativeRing 390 if R has unitsKnown then unitsKnown 391 if R has OrderedSet then OrderedSet 392 if R has OrderedAbelianMonoidSup then OrderedAbelianMonoidSup 393 if R has Field then VectorSpace R 394 add 395 if R has Ring then 396 equation2R : Vector % -> Matrix R 397 398 coerce(n : Integer) : % == n::R::% 399 characteristic() == characteristic()$R 400 differentiate(z : %, d : R -> R) == map(d, z) 401 402 equation2R v == 403 ans : Matrix(R) := new(dim, #v, 0) 404 for i in minRowIndex ans .. maxRowIndex ans repeat 405 for j in minColIndex ans .. maxColIndex ans repeat 406 qsetelt!(ans, i, j, qelt(qelt(v, j), i)) 407 ans 408 409 reducedSystem(m : Matrix %) : Matrix(R) == 410 empty? m => new(dim*nrows(m), ncols(m), 0) 411 reduce(vertConcat, [equation2R row(m, i) 412 for i in minRowIndex m .. maxRowIndex m])$List(Matrix R) 413 414 reducedSystem(m : Matrix %, v : Vector %): 415 Record(mat : Matrix R, vec : Vector R) == 416 vh : Vector(R) := 417 empty? v => empty() 418 rh := reducedSystem(v::Matrix %)@Matrix(R) 419 column(rh, minColIndex rh) 420 [reducedSystem(m)@Matrix(R), vh] 421 422 if R has Field then 423 x / b == x * inv b 424 dimension() == dim::CardinalNumber 425 426 if R has Finite then 427 size() == size()$R ^ dim 428 429 index n == 430 s := size()$R 431 r := new(dim, index(1)$R)$Vector(R) 432 n0 : Integer := n-1 433 for i in 1..dim repeat 434 d := divide(n0, s) 435 r.i := index((1+d.remainder)::PositiveInteger)$R 436 n0 := d.quotient 437 438 directProduct r 439 440 lookup v == 441 s := size()$R 442 pow : NonNegativeInteger := 1 443 res : Integer := 1 444 for i in 1..dim repeat 445 res := res + (lookup(v.i)$R - 1)*pow 446 pow := pow * s 447 448 res::PositiveInteger 449\end{code} 450 451It is translated into \ldots 452\begin{code} 453(|Sequence| (|Import| NIL |AxiomLib|) (|Import| NIL |Boolean|) 454 (|Foreign| (|Declare| |dummyDefault| |Exit|) |Lisp|) 455 (|Define| 456 (|Declare| |DirectProductCategory| 457 (|Apply| -> 458 (|Comma| 459 . #1=((|Declare| |#1| |NonNegativeInteger|) 460 (|Declare| |#2| |Type|))) 461 |Category|)) 462 (|Lambda| (|Comma| . #1#) |Category| 463 (|Label| |DirectProductCategory| 464 (|With| NIL 465 (|Sequence| 466 (|Apply| |IndexedAggregate| |Integer| |#2|) 467 (|Apply| |CoercibleTo| (|Apply| |Vector| |#2|)) 468 (|Apply| |AbelianProductCategory| |#2|) 469 |finiteAggregate| 470 (|Declare| |directProduct| 471 (|Apply| -> 472 (|Comma| (|Apply| |Vector| |#2|)) %)) 473 (|If| (|Test| (|Has| |#2| |SetCategory|)) 474 (|Apply| |FullyRetractableTo| 475 (|PretendTo| |#2| |SetCategory|)) 476 NIL) 477 (|If| (|Test| (|Has| |#2| |Ring|)) 478 (|Sequence| 479 (|Apply| |DifferentialExtension| 480 (|PretendTo| |#2| |Ring|)) 481 (|Apply| |FullyLinearlyExplicitOver| 482 (|PretendTo| |#2| |Ring|))) 483 NIL) 484 (|If| (|Test| (|Has| |#2| |AbelianMonoid|)) 485 (|If| (|Test| (|Has| |#2| |Monoid|)) 486 (|Declare| |unitVector| 487 (|Apply| -> (|Comma| |PositiveInteger|) 488 %)) 489 NIL) 490 NIL) 491 (|If| (|Test| (|Has| |#2| |SemiRng|)) 492 (|Sequence| |SemiRng| 493 (|Apply| |BiModule| 494 (|PretendTo| |#2| |SemiRng|) 495 (|PretendTo| |#2| |SemiRng|)) 496 (|If| 497 (|Test| 498 (|Has| |#2| |AbelianMonoid|)) 499 (|Declare| |dot| 500 (|Apply| -> (|Comma| % %) 501 |#2|)) 502 NIL)) 503 NIL) 504 (|If| (|Test| (|Has| |#2| |Monoid|)) |Monoid| 505 NIL) 506 (|If| (|Test| (|Has| |#2| |SemiGroup|)) 507 (|Sequence| |SemiGroup| 508 (|Declare| * 509 (|Apply| -> (|Comma| |#2| %) 510 %)) 511 (|Declare| * 512 (|Apply| -> (|Comma| % |#2|) 513 %))) 514 NIL) 515 (|If| (|Test| (|Has| |#2| |Finite|)) |Finite| 516 NIL) 517 (|If| (|Test| (|Has| |#2| |CommutativeRing|)) 518 (|Sequence| 519 (|Apply| |Algebra| 520 (|PretendTo| |#2| |CommutativeRing|)) 521 |CommutativeRing|) 522 NIL) 523 (|If| (|Test| (|Has| |#2| |unitsKnown|)) 524 |unitsKnown| NIL) 525 (|If| (|Test| (|Has| |#2| |OrderedSet|)) 526 |OrderedSet| NIL) 527 (|If| 528 (|Test| 529 (|Has| |#2| |OrderedAbelianMonoidSup|)) 530 |OrderedAbelianMonoidSup| NIL) 531 (|If| (|Test| (|Has| |#2| |Field|)) 532 (|Apply| |VectorSpace| 533 (|PretendTo| |#2| |Field|)) 534 NIL) 535 (|Default| 536 (|Sequence| 537 (|Define| 538 (|Declare| / 539 (|Apply| -> (|Comma| % |#2|) %)) 540 (|Lambda| 541 (|Comma| (|Declare| |t#1| %) 542 (|Declare| |t#2| |#2|)) 543 % (|Label| / |dummyDefault|))) 544 (|Define| 545 (|Declare| |characteristic| 546 (|Apply| -> (|Comma|) 547 |NonNegativeInteger|)) 548 (|Lambda| (|Comma|) |NonNegativeInteger| 549 (|Label| |characteristic| 550 |dummyDefault|))) 551 (|Define| 552 (|Declare| |coerce| 553 (|Apply| -> (|Comma| |Integer|) %)) 554 (|Lambda| 555 (|Comma| (|Declare| |t#1| |Integer|)) % 556 (|Label| |coerce| |dummyDefault|))) 557 (|Define| 558 (|Declare| |differentiate| 559 (|Apply| -> 560 (|Comma| % 561 #2=(|Apply| -> (|Comma| |#2|) |#2|)) 562 %)) 563 (|Lambda| 564 (|Comma| (|Declare| |t#1| %) 565 (|Declare| |t#2| #2#)) 566 % 567 (|Label| |differentiate| 568 |dummyDefault|))) 569 (|Define| 570 (|Declare| |dimension| 571 (|Apply| -> (|Comma|) |CardinalNumber|)) 572 (|Lambda| (|Comma|) |CardinalNumber| 573 (|Label| |dimension| 574 |dummyDefault|))) 575 (|Define| 576 (|Declare| |index| 577 (|Apply| -> (|Comma| |PositiveInteger|) 578 %)) 579 (|Lambda| 580 (|Comma| 581 (|Declare| |t#1| |PositiveInteger|)) 582 % (|Label| |index| |dummyDefault|))) 583 (|Define| 584 (|Declare| |lookup| 585 (|Apply| -> (|Comma| %) 586 |PositiveInteger|)) 587 (|Lambda| (|Comma| (|Declare| |t#1| %)) 588 |PositiveInteger| 589 (|Label| |lookup| 590 |dummyDefault|))) 591 (|Define| 592 (|Declare| |reducedSystem| 593 (|Apply| -> 594 (|Comma| 595 #3=(|Apply| |Matrix| 596 (|PretendTo| % |AbelianMonoid|))) 597 #4=(|Apply| |Matrix| 598 (|PretendTo| |#2| 599 |AbelianMonoid|)))) 600 (|Lambda| (|Comma| (|Declare| |t#1| #3#)) 601 #4# 602 (|Label| |reducedSystem| 603 |dummyDefault|))) 604 (|Define| 605 (|Declare| |reducedSystem| 606 (|Apply| -> 607 (|Comma| 608 #5=(|Apply| |Matrix| 609 (|PretendTo| % |AbelianMonoid|)) 610 #6=(|Apply| |Vector| 611 (|PretendTo| % |Type|))) 612 #7=(|Apply| |Record| 613 (|Declare| |mat| 614 (|Apply| |Matrix| 615 (|PretendTo| |#2| 616 |AbelianMonoid|))) 617 (|Declare| |vec| 618 (|Apply| |Vector| 619 (|PretendTo| |#2| |Type|)))))) 620 (|Lambda| 621 (|Comma| (|Declare| |t#1| #5#) 622 (|Declare| |t#2| #6#)) 623 #7# 624 (|Label| |reducedSystem| 625 |dummyDefault|))) 626 (|Define| 627 (|Declare| |size| 628 (|Apply| -> (|Comma|) 629 |NonNegativeInteger|)) 630 (|Lambda| (|Comma|) |NonNegativeInteger| 631 (|Label| |size| 632 |dummyDefault|))))))))))) 633\end{code} 634That is the parsed source of the Aldor code \ldots 635\begin{code} 636import from AxiomLib; 637import from Boolean; 638import dummyDefault: Exit from Foreign Lisp; 639\end{code} 640 641 642 643 644 645 646 647%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 648\section{Initial Domains without Arguments} 649\label{sec:InitDomain} 650%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 651\begin{code} 652SingleInteger(): Join(IntegerNumberSystem,Logic,OpenMath) with 653 canonical 654 canonicalsClosed 655 noetherian 656 max : () -> % 657 min : () -> % 658 "not": % -> % 659 "~" : % -> % 660 "/\": (%, %) -> % 661 "\/" : (%, %) -> % 662 "xor": (%, %) -> % 663 Not : % -> % 664 And : (%,%) -> % 665 Or : (%,%) -> % 666 == add 667 ... 668\end{code} 669It is translated into \ldots 670\begin{code} 671(|Sequence| (|Import| NIL |FriCASLib|) (|Import| NIL |Boolean|) 672 (|Extend| 673 (|Define| 674 (|Declare| |SingleInteger| 675 (|With| NIL 676 (|Sequence| |IntegerNumberSystem| |Logic| 677 |OpenMath| 678 (|RestrictTo| |canonical| |Category|) 679 (|RestrictTo| |canonicalsClosed| 680 |Category|) 681 (|RestrictTo| |noetherian| |Category|) 682 (|Declare| |max| (|Apply| -> (|Comma|) %)) 683 (|Declare| |min| (|Apply| -> (|Comma|) %)) 684 (|Declare| |not| 685 (|Apply| -> (|Comma| %) %)) 686 (|Declare| ~ (|Apply| -> (|Comma| %) %)) 687 (|Declare| |/\\| 688 (|Apply| -> (|Comma| % %) %)) 689 (|Declare| |\\/| 690 (|Apply| -> (|Comma| % %) %)) 691 (|Declare| |xor| 692 (|Apply| -> (|Comma| % %) %)) 693 (|Declare| |Not| 694 (|Apply| -> (|Comma| %) %)) 695 (|Declare| |And| 696 (|Apply| -> (|Comma| % %) %)) 697 (|Declare| |Or| 698 (|Apply| -> (|Comma| % %) %))))) 699 (|Add| (|PretendTo| (|Add| NIL NIL) 700 (|With| NIL 701 (|Sequence| |IntegerNumberSystem| 702 |Logic| |OpenMath| 703 (|RestrictTo| |canonical| 704 |Category|) 705 (|RestrictTo| |canonicalsClosed| 706 |Category|) 707 (|RestrictTo| |noetherian| 708 |Category|) 709 (|Declare| |max| 710 (|Apply| -> (|Comma|) %)) 711 (|Declare| |min| 712 (|Apply| -> (|Comma|) %)) 713 (|Declare| |not| 714 (|Apply| -> (|Comma| %) %)) 715 (|Declare| ~ 716 (|Apply| -> (|Comma| %) %)) 717 (|Declare| |/\\| 718 (|Apply| -> (|Comma| % %) %)) 719 (|Declare| |\\/| 720 (|Apply| -> (|Comma| % %) %)) 721 (|Declare| |xor| 722 (|Apply| -> (|Comma| % %) %)) 723 (|Declare| |Not| 724 (|Apply| -> (|Comma| %) %)) 725 (|Declare| |And| 726 (|Apply| -> (|Comma| % %) %)) 727 (|Declare| |Or| 728 (|Apply| -> (|Comma| % %) %))))) 729 NIL)))) 730\end{code} 731That is the parsed source of the Aldor code \ldots 732\begin{code} 733import from FriCASLib; 734import from Boolean; 735extend SingleInteger: with { 736 IntegerNumberSystem; 737 Logic; 738 OpenMath; 739 canonical @ Category; 740 canonicalsClosed @ Category; 741 noetherian @ Category; 742 max: () -> %; 743 min: () -> %; 744 _not: % -> %; 745 ~: % -> %; 746 /\: (%, %) -> %; 747 \/: (%, %) -> %; 748 xor: (%, %) -> %; 749 Not: % -> %; 750 And: (%,%) -> %; 751 Or : (%,%) -> %; 752} 753 == (add pretend with { 754 IntegerNumberSystem; 755 Logic; 756 OpenMath; 757 canonical @ Category; 758 canonicalsClosed @ Category; 759 noetherian @ Category; 760 max: () -> %; 761 min: () -> %; 762 _not: % -> %; 763 ~: % -> %; 764 /\: (%, %) -> %; 765 \/: (%, %) -> %; 766 xor: (%, %) -> %; 767 Not: % -> %; 768 And: (%,%) -> %; 769 Or : (%,%) -> %; 770}) add; 771\end{code} 772 773 774 775 776 777 778 779 780 781 782 783%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 784\section{Initial Domains with Arguments} 785\label{sec:ParametrizedInitDomain} 786%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 787\begin{code} 788SegmentBinding(S:Type): Type with 789 equation: (Symbol, Segment S) -> % 790 variable: % -> Symbol 791 segment : % -> Segment S 792 if S has SetCategory then SetCategory 793 == add 794 Rep := Record(var:Symbol, seg:Segment S) 795 ... 796\end{code} 797It is translated into \ldots 798\begin{code} 799(|Sequence| (|Import| NIL |FriCASLib|) (|Import| NIL |Boolean|) 800 (|Sequence| 801 (|Define| 802 (|Declare| |SegmentBindingExtendCategory| 803 (|Apply| -> (|Declare| |#1| |Type|) |Category|)) 804 (|Lambda| (|Comma| (|Declare| |#1| |Type|)) |Category| 805 (|Label| |SegmentBindingExtendCategory| 806 (|With| NIL 807 (|Sequence| 808 (|Declare| |equation| 809 (|Apply| -> 810 (|Comma| |Symbol| 811 (|Apply| |Segment| |#1|)) 812 %)) 813 (|Declare| |variable| 814 (|Apply| -> (|Comma| %) |Symbol|)) 815 (|Declare| |segment| 816 (|Apply| -> (|Comma| %) 817 (|Apply| |Segment| |#1|))) 818 (|If| 819 (|Test| 820 (|Has| |#1| |SetCategory|)) 821 |SetCategory| NIL)))))) 822 (|Extend| 823 (|Define| 824 (|Declare| |SegmentBinding| 825 (|Apply| -> (|Declare| |#1| |Type|) 826 (|Apply| |SegmentBindingExtendCategory| 827 |#1|))) 828 (|Lambda| (|Comma| (|Declare| |#1| |Type|)) 829 (|Apply| |SegmentBindingExtendCategory| |#1|) 830 (|Label| |SegmentBinding| 831 (|Add| (|PretendTo| (|Add| NIL NIL) 832 (|Apply| 833 |SegmentBindingExtendCategory| 834 |#1|)) 835 NIL))))))) 836\end{code} 837That is the parsed source of the Aldor code \ldots 838\begin{code} 839import from FriCASLib; 840import from Boolean; 841SegmentBindingExtendCategory: (S: Type) -> Category == 842 (T: Type): Category +-> with { 843 equation: (Symbol, Segment S) -> %; 844 variable: % -> Symbol; 845 segment : % -> Segment S; 846 if S has SetCategory then SetCategory; 847} 848extend SegmentBinding: (S: Type) -> SegmentBindingExtendCategory S == 849 (S: Type): SegmentBindingExtendCategory S +-> 850 (add pretend SegmentBindingExtendCategory S) add; 851\end{code} 852The last lines are actually equivalent to 853\begin{code} 854extend SegmentBinding(S: Type): SegmentBindingExtendCategory S == 855 (add pretend SegmentBindingExtendCategory S) add; 856\end{code} 857\end{document} 858