\documentstyle[alltt]{article} \setlength{\headsep}{-.4in} \setlength{\textwidth}{6.5in} \setlength{\textheight}{9in} \setlength{\oddsidemargin}{0in} \newcommand{\warn}{\noindent {\bf Warning:} \hspace{1ex}} \newcommand{\bobj}{\begin{quote}\begin{alltt}} \newcommand{\eobj}{\end{alltt}\end{quote}} \newcommand{\more}{\vspace{.1in}{\begin{center} ||| MORE TO COME HERE ||| \end{center}}\vspace{.1in}} %commands for extended BNF \newcommand{\nt}[1]{\mbox{$\langle\!\!\!$ {\it {#1}} $\!\!\rangle$}} \newcommand{\alt}{$\mid$} \newcommand{\lopt}{$[$} \newcommand{\ropt}{$]$} \newcommand{\lsg}{\{} \newcommand{\rsg}{\}} \newcommand{\itr}{$\ldots$} \newcommand{\itd}{$\ldots$} %\def\baselinestretch{2} \def\newblock{} \hyphenation{Me-se-guer} \newcommand{\ra}{$\rightarrow$} \newcommand{\noi}{\noindent} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{document} \title{\vspace{-.75in}OBJ3's Built-ins} \author{Timothy Winkler and Jos\'e Meseguer \\ SRI International, Menlo Park CA 94025\footnote{This documented was edited for clarity by Joseph Kiniry to be included with the 2.06 release of OBJ3 (June, 2000). Any errors herein are his alone. Please provide feedback to {\tt obj3-feedback@kindsoftware.com}.}} \maketitle \section{Introduction} OBJ3 provides two ways to take advantage of the (Common-)Lisp underlying its implementation: {\em built-in sorts} and {\em built-in righthand sides} for rules; we call rules with such built-in righthand sides {\em built-in rules}. Built-in sorts are sorts whose elements are constants represented by Lisp values. General mechanisms are provided for reading, printing, creating Lisp representations for, and testing sort membership for constants of these sorts. In general, built-in sorts can be used in any context a non-built-in sort can, although a constant of a built-in sort cannot be the lefthand side of a rule. The built-in rules come in two varieties, a simplified version that makes writing rules for functions defined on built-in sorts easy, and a general kind that allows arbitrary actions on the redex to be specified. However, to take full advantage of this latter type of rule, one must be familiar with the internal term representation of OBJ and the implementation functions for manipulating this representation. Built-in rules can be used wherever an ordinary rule can be. \section{Built-in Sorts} Built-in sorts consist of an indefinitely large number of constants. For example. a version of NATS with a built-in sort Nat is equivalent to an idealized non-built-in version of the form \bobj obj NATS is sort Nat . ops 0 1 2 3 4 5 6 7 8 9 10 11 12 13 ... : -> Nat . op _+_ : Nat Nat -> Nat . ... endo \eobj \noindent in which an infinite number of constants have been declared. (The name NATS was chosen to avoid a clash with the predefined object NAT.) Other examples of useful built-in sorts are floating point numbers, identifiers, strings, and arrays. Constants in a built-in sort have an associated Lisp representation. Such a built-in sort is introduced by a declaration of the form \bobj bsort \nt{SortId} (\nt{Token-Predicate} \nt{Creator} \nt{Printer} \nt{Sort-Predicate}) . \eobj \noi Which gives the name of the sort, two Lisp functions used for reading, a function for printing constants of the sort, and a predicate that can be used to test whether a Lisp value represents a constant of the given sort. A sort declaration of this kind can occur wherever an ordinary declaration of a sort can occur. When an OBJ expression is read, it is first lexically analyzed into a sequence of tokens which are either single character symbols, such as ``('' and ``]'', or are sequences of characters delimited by these single character symbols or spaces. Internally such tokens are represented by Lisp strings. The representation of the token ``37'' is the Lisp string {\tt "37"} of length two. \begin{itemize} \item \nt{Token-Predicate} is a Lisp predicate that can be applied to an input token (a Lisp string) to determine if the token is a representation of a value in the built-in sort. (It is applied by funcall.) E.g., for NATS, {\tt "37"} should result in true and {\tt "A+B"} in false. With this mechanism the syntactic representation of a built-in constant can only be a single token. \item \nt{Creator} is a Lisp function that will map a token (a Lisp string) to a Lisp representation for that token as a built-in constant. The Lisp function {\tt read-from-string} is very useful as a creator function for built-in sorts that correspond directly to Lisp types. E.g., {\tt "37"} should be mapped to the Lisp value {\tt 37}. \item \nt{Printer} is a Lisp function that will print out the desired external representation of the internal Lisp value representing one of the built-in sort constants. The Lisp function {\tt prin1} is very useful as a \nt{Printer} function for printing out values that correspond directly to Lisp types. E.g., 37 should be printed by printing the digit {\tt 3} followed by the digit {\tt 7}. Since the user can define the printer function to meet particular needs, there is no assumption that this function is an inverse to the \nt{Creator} function. Indeed, the syntactic representation of a built-in constant may involve many tokens, but then this representation cannot be read in as a built-in constant. \item \nt{Sort-Predicate} should be a Lisp predicate that is true only for Lisp values that are representations of constants in the built-in sort. E.g., {\tt 3} should be considered to be in sort Nat and and {\tt -3} should not. The purpose and use of this predicate will be discussed further below. \end{itemize} For NATS we might have the specific declaration \bobj obj NATS is bsort Nat (obj_NATS\$is_Nat_token obj_NATS\$create_Nat obj_NATS\$print_Nat obj_NATS\$is_Nat) . endo \eobj \noindent where the functions referred to have these definitions \bobj (defun obj_NATS\$is_Nat_token (token) (every #'digit-char-p token)) (defun obj_NATS\$create_Nat (token) (read-from-string token)) (defun obj_NATS\$print_Nat (x) (prin1 x)) (defun obj_NATS\$is_Nat (x) (and (integerp x) (<= 0 x))) \eobj With the above definition of the object NATS one can use the natural number constants. E.g., \bobj OBJ> red 100 . reduce in NATS : 100 rewrites: 0 result Nat: 100 \eobj \noindent As it stands, since only a built-in sort has been introduced, and no associated functions have been defined, this object is not very useful. {\bf Note}: a current implementation restriction does not allow a built-in constant to be the lefthand side of a rule. Built-in constants are always treated as being in reduced form (application of rules would never be attempted). \subsection{Subsorts of Built-in Sorts} It is possible for a built-in sort to be a subsort of another built-in sort, but a non-built-in sort cannot be a subsort of a built-in sort. For the sort of newly created built-in constants to be properly assigned, a sort predicate must be provided for each built-in sort. An example of this will later be seen in a version of the rational numbers using Common Lisp rationals. When there are built-in subsorts of the sort of a newly created built-in constant, then the sort that is assigned to the constant is determined by scanning the list of subsorts, applying the sort predicates to the Lisp value to determine if it lies in the corresponding subsort, and choosing the lowest acceptable sort as the sort of the constant. It is assumed that there is always a unique lowest sort. It is critical only that the sort predicate for a built-in sort should be false for values that are in supersorts of the built-in sort. It is not necessary for it to be false for constants in subsorts of the given sort. If there is no enclosing built-in supersort, since the \nt{Sort-Predicate} function will only be called for built-in constants of that sort (if it is called at all), then it can be constantly true, and have a definition like \bobj (defun obj_NATS\$is_Nat (x) t) \eobj \noindent This will not affect the operational behavior of OBJ in this case. However, it is better for the predicate to be exact in order to allow the easy incorporation of the sort a supersort. \section{Built-in Rules} Built-in rules provide a way of using Lisp expressions to perform computations. This is essential for the usefulness of built-in sorts, but can also be used for non-built-in data. These rules are either of a special {\em simple} form or are {\em general}. {\em Simple} built-in rules can be unconditional or conditional with syntax \bobj bq \nt{Term} = \nt{Lisp Expression} . \alt cbq \nt{Term} = \nt{Lisp Expression} if \nt{BoolTerm} . \eobj \noi The key requirement for simple built-in rules is that {\em all the variables appearing in the lefthand side must have sorts that are built-in sorts}. The lefthand side of the rule is matched against terms in exactly the usual fashion; also, in the conditional case, the condition is just an OBJ term and is treated in exactly the same way as a condition in a non-built-in rule. %The way the rule is applied is that the lefthand side is matched %producing a correspondence between the variables in the lefthand side and %subterms of the term being reduced. %In the simplified case it is %required that all sorts of the variables be built-in sorts. If a match for the variables of the lefthand side is found, where each variable is matched to a built-in constant and which satisfies the condition if the built-in rule is conditional, then the righthand side of the equation is evaluated in a Lisp environment where Lisp variables with names corresponding to the OBJ variables (as usual in Common Lisp, the case, upper or lower, of variables in the Lisp expression is ignored) are bound to the Lisp value corresponding to the built-in constants to which they were matched. Since the variables must match constants of their associated built-in sorts, this forces a bottom-up evaluation strategy regardless of the strategy specified for the operator. The sort of the lefthand side will usually be a built-in sort and the LISP value of the righthand side of the rule will be automatically converted to a built-in constant of that sort. If the sort of the lefthand side is not a built-in sort, then, with one exception that will be mentioned next, the value of the righthand side should be a Lisp representation of a term of that sort (or a subsort of that sort). A special case is that, if the sort of the lefthand side is Bool, then the value of the righthand side Lisp expression can be any Lisp value which will be converted to a Boolean value by mapping {\tt nil} to {\bf false} and all other Lisp values to {\bf true}. For this case, a special conversion is performed which makes it very easy to define predicates. As an example, consider \bobj obj NATS is bsort Nat (obj_NATS\$is_Nat_token obj_NATS\$create_Nat obj_NATS\$print_Nat obj_NATS\$is_Nat) . op _+_ : Nat Nat -> Nat . vars M N : Nat . bq M + N = (+ M N) . endo \eobj \noindent We can then do the following reduction. \bobj OBJ> red 123 + 321 . reduce in NATS : 123 + 321 rewrites: 1 result Nat: 444 \eobj Since the matching of the lefthand side is done in the usual fashion, the operators appearing in the lefthand side may even be associative and commutative. The {\em general} form of a built-in rule has the following syntax \bobj beq \nt{Term} = \nt{Lisp Expression} . \alt cbeq \nt{Term} = \nt{Lisp Expression} if \nt{BoolTerm} . \eobj \noi {\em where now the variables in the lefthand side can have arbitrary sorts}. The lefthand side and condition are treated as usual. The process of applying the rule is a bit different in this case. The lefthand side is matched as usual creating the correspondence between variables in the lefthand side and subterms of the term being rewritten. The righthand side is evaluated in an environment where Lisp variables with names corresponding to the OBJ variables (case is ignored) are bound to the internal OBJ3 representation of the terms matched by the variables. The Lisp value of the righthand side is expected to be an internal OBJ3 representation of a term which then destructively replaces the top-level structure of the term matched. An exception is that, if the Lisp code evaluates the expression {\tt (obj\$rewrite\_fail)}, then the rewrite is aborted and the term is left unchanged. (This has the effect of making the rule conditional in an implicit way; the condition is checked in the Lisp code for the righthand side.) An additional feature is that the righthand side is evaluated in an environment where {\tt module} is bound to the module that the rule comes from. This last feature is necessary to correctly treat general built-in rules in instances of parameterized modules. %{\bf Note}: During the application of a rule, the Lisp variable {\tt %self} is bound to the redex term. This variable can be used in a %built-in righthand side. A simple example is \bobj obj NATS is bsort Nat (obj\_NATS\$is\_Nat\_token obj\_NATS\$create\_Nat obj\_NATS\$print\_Nat obj\_NATS\$is\_Nat) . op _+_ : Nat Nat -> Nat . vars M N : Nat . bq M + N = (+ M N) . op print _ : Nat -> Nat . beq print M = (progn (princ " = ") (term\$print M) (terpri) M) . endo \eobj This definition provides a function, {\tt print}, that is an identity function that has the side-effect of printing the value of its argument preceded by the ``{\tt =}'' sign. A simple example of the the use of {\tt print} is: \bobj OBJ> red (print (3 + 2)) + 4 . reduce in NATS : print (3 + 2) + 4 = 5 rewrites: 3 result Nat: 9 \eobj \noindent The line containing ``{\tt = 5}'' is the output produced by the use of {\tt print}. Such printing functions that are an identity function from the point of view of the rewriting are actually useful. (Typically one may want to add an extra argument that provides a label for the output.) General built-in rules can be written to perform arbitrary transformations on a term using any of the functions defined in the OBJ3 implementation. Thus it is useful to be familiar with the functions provided by the implementation when writing such general built-in rules. Some of those basic functions will be discussed below. Often is is useful to initialize some Lisp variables after certain OBJ objects are created. This can be done using {\tt eval} or {\tt ev}. There are examples of this in the OBJ3 standard prelude. In general, the module that the rules are associated with may be an instance of a parameterized module. In this case, it is necessary to write the rules so that the extra parameter {\tt module} is used to create structures within that module. When locating the correct instance of an operator one must first determine its module, then the sorts of its arguments and result, and then its name. In the case where there are no ambiguities, some simpler functions can be used, e.g., find an operator based only on its name. Functions that are useful for the general built-in rules include the following (note these are all Lisp functions from the OBJ3 implementation). The Lisp functions will be described, in part, by giving declarations similar to OBJ operator declarations. Of course these need to be interpreted as informal descriptions of Lisp functions that may have side-effects and which manipulate particular Lisp representations of the values given as arguments. The sorts that will be referred to are: \begin{itemize} \item Bool, NzNat, Lisp-Value\\ Bool, NzNat, and Lisp-Value are names for the related standard LISP types. \item Sort-Name\\ A Sort-Name is a Lisp string naming a sort. \item Op-Name\\ An Op-Name is a Lisp list of the tokens, represented as Lisp strings, that constitute the name of the operator. For example, the name of {\tt \_+\_ : Nat Nat -> Nat} is {\tt ("\_" "+" "\_")}. \item Sort-Order\\ A Sort-Order is a representation of a partial order on the sorts. \item Sort, Operator, Term, Module, Module-Expression\\ Sort, Operator, Term, Module, and Module-Expression correspond to the Lisp representations of these sorts. Values of the sorts Sort, Operator, Term, and Module are composite objects with many components, some of which are likely not to be of interest here. For these sorts, functions selecting the interesting features of the values are indicated below. \item SortSet\\ SortSet is a set of sorts represented by a list. \item LIST[Term], LIST[Sort]\\ LIST[-] indicates that the values so described will be Lisp lists of the specified sort. \end{itemize} Following is a list of functions that are useful in writing term manipulations functions. \begin{itemize} \item {\tt modexp\_eval\$eval} : Module-Expression \ra Module\\ The argument can be the name of a specific named module, e.g. {\tt "INT"}. This can be used to find specific named modules. \item {\tt sort\$is\_built\_in} : Sort \ra Bool\\ This predicate decides whether the sort given is a built-in sort. \item {\tt module\$sort\_order} : Module \ra Sort-Order\\ This selector provides access to the sort order for the given module, i.e. the representation of the sort structure. \item {\tt sort\_order\$is\_included\_in} : Sort-Order Sort Sort \ra Bool\\ This predicate decides if the first sort is a subsort of the second in the given sort order. \item {\tt sort\_order\$is\_strictly\_included\_in} : Sort-Order Sort Sort \ra Bool\\ Same as above but excludes the case when two sorts are equal. \item {\tt sort\_order\$lower\_sorts} : Sort-Order Sort \ra SortSet\\ This function produces a list of the sorts lower than a given sort in the given sort order. \item {\tt mod\_eval\$\$find\_sort\_in} : Module Sort-Name \ra Sort\\ This function can be used to find the named sort in the given module. A typical sort name is "Int". \item {\tt sort\$name} : Sort \ra Sort-Name\\ This selector provides the name of a given sort. \item {\tt operator\$name} : Operator \ra Op-Name\\ This selector provides the name of the given operator. \item {\tt operator\$is\_same\_operator} : Operator Operator \ra Bool\\ This predicate decides if the two operators are the same operator. \item {\tt operator\$arity} : Operator \ra LIST[Sort]\\ This selector provides the arity of the given operator as a list of sorts, which may be {\tt nil}. \item {\tt operator\$coarity} : Operator \ra Sort\\ This selector provides the co-arity of the given operator. \item {\tt mod\_eval\$\$find\_operator\_in} : Module Op-Name LIST[Sort] Sort \ra Operator\\ This function locates the operator with the given name, arity (list of sorts) and coarity, or returns {\tt nil} if there is none such. \item {\tt mod\_eval\$\$find\_operator\_named\_in} : Module Op-Name \ra Operator\\ This function attempts to locate an operator purely based on its name. \item {\tt term\$is\_var} : Term \ra Bool\\ This predicate decides if a term is a variable. It may be that the terms that you will be manipulating will primarily be ground terms, but, in general, it is preferable to consider the case of variables in definitions of functions. \item {\tt term\$is\_constant} : Term \ra Bool\\ This predicate decides if a term is a constant. \item {\tt term\$head} : Term \ra Operator\\ This function produces the operator that is the head operator of a non-variable term. It is an error to apply this function to a term that is a variable. \item {\tt term\$subterms} : Term \ra LIST[Term]\\ This function produces the list of top-level subterms of the given term. \item {\tt term\$make\_term} : Operator LIST[Term] \ra Term\\ This function creates a new term with the given head operator and list of arguments. \item {\tt term\$make\_term\_with\_sort\_check} : Operator LIST[Term] \ra Term\\ This function is similar to the last, but may replace the operator with a lower operator in the case of overloading. If there is a lower overloaded operator whose arity fits the sorts of the given arguments this operator will be used instead of the given operator. \item {\tt term\$arg\_n} : Term NzNat \ra Term\\ This function gives easy access to the $n$-th (counting from 1) top-level argument of the given term. \item {\tt term\$sort} : Term \ra Sort\\ This function computes the sort of a term whether it is a variable or not. \item {\tt term\$is\_reduced} : Term \ra Bool\\ This function checks whether or not the term has been marked as fully reduced. This flag is updated by side-effect. \item {\tt term\$!replace} : Term Term \ra Term\\ The Lisp representation for the first argument term is destructively altered in such a way that it will appear to have the same term structure as the second term argument. The altered representation of the first term is returned. \item {\tt term\$!update\_lowest\_parse\_on\_top} : Term \ra Term\\ This will update the sort of the term, e.g. in the case where a subterm has been altered and now has a lower sort. \item {\tt term\$retract\_if\_needed} : Sort-Order Term Sort \ra Term\\ This function either returns the term, or a retract applied to the term depending on whether the sort of the term is included in the given sort or not. \vspace{1ex} \item {\tt term\$is\_built\_in\_constant} : Term \ra Bool\\ This predicate decides if the term is a built-in constant or not. \item {\tt term\$similar} : Term Term \ra Bool\\ Tests if the two terms have the same term structure without taking attributes into account. \item {\tt term\$equational\_equal} : Term \ra Bool\\ Tests if the terms have the equivalent structure taking attributes into account. \item {\tt term\$make\_built\_in\_constant} : Sort Lisp-Value \ra Term\\ This function creates a {\em term} which is a built-in constant for the given built-in sort and Lisp value. The sort predicate for the built-in sort is not applied. \item {\tt term\$make\_built\_in\_constant\_with\_sort\_check} : Sort Lisp-Value \ra Term\\ Similar to above, but may replace the given sort by a lower sort. \item {\tt term\$built\_in\_value} : Term \ra Lisp-Value\\ This function produces the Lisp value from a built-in constant. \item {\tt obj\_BOOL\$is\_true} : Term \ra Bool\\ This function tests whether the term given as its argument is the constant {\tt true}. The value is a Lisp boolean, i.e. {\tt T} for {\tt true} and {\tt NIL} for {\tt false}. \item {\tt rew\$!normalize} : Term \ra Term\\ The is the OBJ evaluation function. The term given as an argument is reduced and is updated by side-effect as well as being returned as the value of the function. \end{itemize} The following functions are specific to A and AC terms. \begin{itemize} \item {\tt term\$list\_assoc\_subterms} : Term Operator \ra LIST[Term]\\ This function computes the list of subterms of the given term that are on the fringe of the tree at the top of the term the nodes of which are all terms headed with the given associative operator or operators overloaded by this operator. This can be the whole term. \item {\tt term\$list\_AC\_subterms} : Term Operator \ra LIST[Term]\\ Similar to the above, but for associative-commutative (AC) operators. \item {\tt term\$make\_right\_assoc\_normal\_form} : Operator LIST[Term] \ra Term\\ This function builds a term from the given associative operator and the list of terms by building a right-associated binary tree. \item {\tt term\$make\_right\_assoc\_normal\_form\_with\_sort\_check} : Operator LIST[Term] \ra Term\\ Similar to the above, but may replace the operator by lower operators. \end{itemize} Final note: it is actually possible for subterms of righthand side to be a built-in term, with an interface provided by the prelude object BUILT-IN. The subterm will be a built-in constant of sort {\tt Built-in}. The external syntax is ``{\tt built-in:} \nt{Lisp}''. The value of the constant is a function that will map a substitution (binding of variables to terms) to a term representation (the function will be {\tt funcall}-ed). \section {Larger Example: Rationals} As a somewhat larger example, the rational numbers could be defined using the Common Lisp representation of rationals and based on the existing predefined modules INT, NAT, and NZNAT as follows. \bobj ev (progn (defun obj_RAT\$is_NzRat_token (token) nil) (defun obj_RAT\$create_NzRat (x) (read-from-string x)) (defun obj_RAT\$is_Rat_token (x) nil) (defun obj_RAT\$is_NzRat (x) (and (rationalp x) (not (= 0 x)))) (defun obj_RAT\$print (x) (if (typep x 'ratio) (progn (prin1 (numerator x)) (princ " / ") (prin1 (denominator x))) (prin1 x))) ) . obj RATS is protecting INT . bsort NzRat (obj_RAT\$is_NzRat_token obj_RAT\$create_NzRat obj_RAT\$print obj_RAT\$is_NzRat) . bsort Rat (obj_RAT\$is_Rat_token car obj_RAT\$print rationalp) . subsorts Int < Rat . subsorts NzInt < NzRat < Rat . op _/_ : Rat NzRat -> Rat . op _/_ : NzRat NzRat -> NzRat . op -_ : Rat -> Rat [prec 2] . op -_ : NzRat -> NzRat [prec 2] . op _+_ : Rat Rat -> Rat [assoc comm] . op _*_ : Rat Rat -> Rat [assoc comm] . op _*_ : NzRat NzRat -> NzRat [assoc comm] . op _-_ : Rat Rat -> Rat . vars R S : Rat . vars NS : NzRat . bq - R = (- R) . bq R / NS = (/ R NS) . bq R + S = (+ R S) . bq R * S = (* R S) . bq R - S = (- R S) . jbo \eobj \section{Larger Example: Cells} The basic idea of this example is very simple, namely to provide a parameterized object that creates {\em cells} containing values of a given sort. Such cells are an abstract version of procedural variables that can be modified by side-effects or destructive assignments. Of course, this module is not functional. \bobj *** obj code for cells ev (defun set-cell-rule (i x) (setf (cadr i) x) i) obj CELL[X :: TRIV] is sort Cell . op cell _ : Elt -> Cell . op new-cell _ : Elt -> Cell . op val _ : Cell -> Elt . op set _ _ : Cell Elt -> Cell . var I : Cell . var X : Elt . eq new-cell X = cell X . eq val (cell X) = X . beq set I X = (set-cell-rule I X) . endo *** sample program using this obj TEST is pr CELL[INT] . sort A . subsort Int Cell < A . op _|_ : A A -> A . op dbl _ : A -> A . op incr _ : A -> A . var U V : A . var C : Cell . eq dbl U = U | U . eq incr (U | V) = (incr U) | (incr V) . eq incr C = val (set C (1 + (val C))) . endo red incr (dbl (dbl (dbl (new-cell 0)))) . *** result A: ((1 | 2) | (3 | 4)) | ((5 | 6) | (7 | 8)) \eobj \section {Larger Example: Arrays of Integers} This provides arrays of integers that can be modified by side-effect. It might be useful for a functional program for table-lookup (side-effects only would be used for building the table). \begin{quote}\begin{alltt} ev (defun arrayint$print (x) (princ "[") (dotimes (i (length x)) (when (< 0 i) (princ ",")) (print$check) (prin1 (aref x i))) (princ "]")) obj ARRAYINT is pr INT . bsort ArrayInt ((lambda (x) nil) (lambda (x) (break)) arrayint$print (lambda (x) t)) . op make-array : Nat Int -> ArrayInt . op length _ : ArrayInt -> Nat . op _[_] : ArrayInt Nat -> Int . op _[_] := _ : ArrayInt Nat Int -> ArrayInt . var A : ArrayInt . var I : Int . var N : Nat . bq make-array(N,I) = (make-array (list N) :initial-element I) . bq length(A) = (length A) . bq A[N] = (aref A N) . bq A[N] := I = (progn (setf (aref A N) I) A) . endo \end{alltt}\end{quote} \bobj OBJ> red make-array(10,1) . reduce in ARRAYINT : make-array(10,1) rewrites: 1 result ArrayInt: [1,1,1,1,1,1,1,1,1,1] OBJ> red (make-array(10,1))[5] . reduce in ARRAYINT : make-array(10,1)[5] rewrites: 2 result NzNat: 1 OBJ> red (make-array(10,1))[5] := 33 . reduce in ARRAYINT : make-array(10,1)[5]:= 33 rewrites: 2 result ArrayInt: [1,1,1,1,1,33,1,1,1,1] \eobj \section{Larger Example: Sorting} This provides a parameterized sorting module. The parameter provides the partial order used and the sorting is done using the Lisp function {\tt sort}. One minor interesting point is that an operator named {\tt \_ << \_} is introduced as an alias for the parameter operator {\tt \_ < \_} simply to provide an easy way to locate the parameter operator after instantiation. This is needed because the name of a parameter operator cannot be known for an instance of the parameterized module, where such a parameter may have been mapped to an arbitrary term by the view defining the instantiation. For similar reasons, the operator {\tt \_ << \_} as well as the other operators {\tt \_ , \_} and {\tt empty} appearing in the parameterized SORT module below should not be renamed by a module renaming. The parameter of our sorting module is as usual the theory of partially ordered sets, given by the theory module: \bobj th POSET is sort Elt . op _<_ : Elt Elt -> Bool . vars E1 E2 E3 : Elt . eq E1 < E1 = false . cq E1 < E3 = true if E1 < E2 and E2 < E3 . endth \eobj The function {\tt sort-list} used in the {\tt SORT} module below has two arguments, a module (namely the given instantiation of the parameterized module {\tt SORT}) and a list to be sorted. Its definition is as follows: \begin{quote}\begin{alltt} ev ; NOTE: sort-list will not work if any of the operators found by name, ; i.e. _<<_, empty, and _,_, below are renamed in a module renaming. (defun sort-list (mod l) (let ((test (mod_eval$$find_operator_named_in mod '("_" "<<" "_"))) (empty (mod_eval$$find_operator_named_in mod '("empty"))) (conc (mod_eval$$find_operator_named_in mod '("_" "," "_")))) (if (eq empty (term$head l)) l (let ((sorted (sort (term$list_assoc_subterms l conc) #'(lambda (x y) (obj_BOOL$is_true (rew$!normalize (term$make_term test (list x y))))) ))) (term$make_right_assoc_normal_form_with_sort_check conc sorted) )) )) \end{alltt}\end{quote} We are now ready to define the parameterized {\tt SORT} module which has a built-in equation involving the sort-list function. \bobj obj SORT[ORDER :: POSET] is sort List . subsort Elt < List . op empty : -> List . op _,_ : List List -> List [assoc idr: empty] . op sort _ : List -> List . op _<<_ : Elt Elt -> Bool . vars E1 E2 : Elt . eq E1 << E2 = E1 < E2 . var L : List . beq sort L = (sort-list module L) . endo \eobj Here is a sample reduction for for sorting lists of integers. \bobj obj TEST is pr SORT[INT] . endo red sort (9, 8, 7, 6, 5, 4, 3, 2, 1, 0) . ***> result List: 0,1,2,3,4,5,6,7,8,9 \eobj \end{document}