Science, Faculty of
Computer Science, Department of
DSpace
UBCV
Ross, Brian James
Master of Science - MSc
University of British Columbia
The feasibility of using Horn clauses as a means of describing and transforming imperative pro-grams is explored. A logical semantics is derived for a typical imperative language. The style of this semantics permits direct translations between the source language and semantical representations. Given the use of Horn clause logic in logic programming, the semantics is particularly useful since models of computation associated with logic programs can be applied to it. Treating the semantics as a logic program means that, in a program transformation context, the semantic representation is particularly well suited to partial evaluation. To support these ideas, an automatic translation system has been implemented which permits translation between programs written in an imperative language and their logical equivalents. In addition, a partial evaluator has been written which meta-interprets the logical representation of an imperative program to produce a partially evaluated result. Using predicative programming, this result can be translated back into the original source code. Thus the system as a whole performs source-to-source transformations of imperative programs.
T H E SEMANTICS AND TRANSFORMATION OF IMPERATIVE PROGRAMS USING HORN CLAUSES By BRIAN JAMES ROSS B.C.Sc., University of Manitoba, 1984 A THESIS SUBMITTED IN PARTIAL FULFILLMENT OF T H E REQUIREMENTS FOR THE DEGREE OF MASTER OF SCIENCE in T H E FACULTY OF GRADUATE STUDIES (DEPARTMENT OF COMPUTER SCIENCE) We accept this thesis as conforming to the required standard T H E UNIVERSITY OF BRITISH COLUMBIA July 1988 © Brian J. Ross, 1988 In presenting this thesis in partial fulfilment of the requirements for an advanced degree at the University of British Columbia, I agree that the Library shall make it freely available for reference and study. I further agree that permission for extensive copying of this thesis for scholarly purposes may be granted by the head of my department or by his or her representatives. It is understood that copying or publication of this thesis for financial gain shall not be allowed without my written permission. Department The University of British Columbia 1956 Main Mall Vancouver, Canada V6T 1Y3 DE-6(3/81) Abstract The feasibility of using Horn clauses as a means of describing and transforming imperative pro-grams is explored. A logical semantics is derived for a typical imperative language. The style of this semantics permits direct translations between the source language and semantical represen-tations. Given the use of Horn clause logic in logic programming, the semantics is particularly useful since models of computation associated with logic programs can be applied to it. Treating the semantics as a logic program means that, in a program transformation context, the semantic representation is particularly well suited to partial evaluation. To support these ideas, an au-tomatic translation system has been implemented which permits translation between programs written in an imperative language and their logical equivalents. In addition, a partial evaluator has been written which meta-interprets the logical representation of an imperative program to produce a partially evaluated result. Using predicative programming, this result can be trans-lated back into the original source code. Thus the system as a whole performs source-to-source transformations of imperative programs. ii Contents Abstract ii List of Figures v Acknowledgement vii 1 Introduction 1 2 Review 4 2.1 Formal Program Semantics 4 2.1.1 Goals of Program Semantics 4 2.1.2 Logical Semantics 5 2.1.3 Denotational Semantics 8 2.1.4 Operational Semantics 9 2.1.5 Algebraic Semantics 9 2.2 Program Transformation 9 2.3 Partial Evaluation 12 3 A n Imperative Language Called Bruce 14 3.1 Design Motivations 14 3.2 Syntax 15 3.3 Operational Semantics 16 4 A Horn Clause Semantics 23 4.1 Design Goals 23 4.2 Basic Bruce Semantics 25 iii 4.3 Program Branches 30 4.4 Logic Program Interpretation and Completeness 33 4.5 Translating Logic to Bruce 35 4.6 Example Translations 37 5 A Bruce-Logic Translation System 46 5.1 The logic generator 46 5.2 The Brucifier 52 6 The Partial Evaluation of Bruce Programs 59 6.1 Partial evaluation and program transformation 59 6.2 Implementation 61 6.3 Example transformations 64 7 Discussion 69 7.1 Related work 69 7.2 Conclusions and further work 72 Bibliography 77 A Partial Evaluator Source 82 B Bruce Parser 89 C Branch Handling 106 D Bruce Generation 117 E Program Printing Utilities 131 F Miscellaneous Code 138 G Binary G C D Basic Semantics 163 H Partially Evaluated Binary G C D Semantics 166 iv List of Figures 3.1 Syntax of expressions 15 3.2 Syntax of higher-level constructs 17 3.3 Definition of Comp 19 3.4 Definition of Buildenv 20 3.5 Example Program . . . 21 3.6 Buildenv Output 21 4.1 Logical semantics of Bruce constructs (no branching) 27 4.2 Branching out of two loops 32 4.3 Converting Branches 37 4.4 Consecutive assignments 37 4.5 While loop 38 4.6 Two alternate Bruce realizations 38 4.7 Subprogram invocation 39 4.8 Branching within a chain 40 4.9 Bruce equivalent 40 4.10 End of file control scheme (initial) 41 4.11 Logical Form 42 4.12 Derived result 43 4.13 Jumping into a repeat loop 44 4.14 Bruce equivalent 45 5.1 Chain rules 47 5.2 While-loop rule 48 5.3 Branching into two loops 49 v 5.4 Basic semantics 50 5.5 Label program 51 5.6 Label program predicate 51 5.7 Final semantics 53 5.8 Branch out of two loops 54 5.9 Basic semantics 54 5.10 Final semantics 55 5.11 Distributed program predicate 55 5.12 While loop matching 56 5.13 Derived Bruce program 57 5.14 Derived Bruce program 58 6.1 Partial evaluator 62 6.2 Goal inhibition 6 3 6.3 Binary powers 65 6.4 Residual programs (n = 5) 65 6.5 Residual programs (x = 2, n = 5) 65 6.6 Binary gcd (u = 7) 66 6.7 A suspended test 67 6.8 Polyvariant logical result 67 6.9 Polyvariant Bruce result 68 vi j Acknowledgement I owe special thanks to my supervisor, Harvey Abramson. His advice and guidance were directly responsible for the success of this thesis. Thanks are also due to Wolfgang Bibel for his helpful suggestions, and for reading the thesis. I also owe thanks to Paul Voda for directing me to Hehner's work; to Doug Westcott for technical assistance and the use of his lexical analysis code; to Matthew Crocker for helpful discussions and moral support; and to the Department of Computer Science for its financial assistance. Finally, my gratitude to my parents, Jack and Marlene Ross, for their unwavering love and support throughout the years. vii C h a p t e r 1 I n t r o d u c t i o n An imperative programming language is one whose design is motivated by the architecture of a von Neumann machine [Backus 78]. Such languages typically involve the update of a "state", which is usually taken to be the current state of the machine's memory. The vast majority of computer applications still make predominant use of imperative programming. Engineering and scientific applications rely on the use of FORTRAN. The "C" language has found a niche as a systems programming language, to a large extent replacing assembler language programming. The Pascal language is currently in vogue as a general purpose programming language. Given the widespread existence of imperative programs, there is still a need to explore new techniques of analysis for this class of programs. Predicate logic continues to enjoy extensive use in the verification and transforma-tion of imperative-style programs [Loeckx etal. 84] [Hoare 85]. With the advent of logic programming and other computational models for predicate logic there are increased op-portunities to apply the logical analysis of programs in semi-automated environments. This thesis explores the feasibility of using Horn clause logic to describe and transform imperative programs. Although declarative logic programming and imperative program-ming represent opposite stylistic philosophies, we will demonstrate that logic programming offers interesting possibilities as a tool for analyzing its "imperative ancestor". The motivating principle behind this thesis is that valid logical manipulations of a 1 CHAPTER 1. INTRODUCTION 2 program's logical semantics reflect correctness-preserving transformations of the program's source. In particular, we will show that imperative programs can be economically de-scribed in Horn clause logic, and that there exist logically valid transformations of these Horn clause axioms which represent useful program transformations of the source. First, the thesis introduces a new logical semantics for imperative-style programs. Given a cor-rect and executable program written in an imperative language, we define for it a logical semantics through the inspection of its syntax. The style of this semantics is most related to ones given by Hehner [Hehner 84a] [Hehner etal. 86], but is somewhat simplified, given its intended use for program transformation. Using the predicative programming paradigm, the logical semantics and source language are intertranslatable. Thus, changes to the log-ical representation reflect corresponding changes to the source program. Interpreting the semantics as a logic program means that one specific type of program transformation - par-tial evaluation - is particularly suitable, since the semantics can be executed using SLDNF resolution. To support the above argument, we implement an imperative program transformation system. We first define a Horn clause semantics for a generic imperative language. Given an operational semantics for the language defined in terms of an abstract machine, we de-fine logical axioms for basic language constructs which describe their operational behavior. The semantics for a program takes the form of a logical theory which describes the complete computational behavior of the program. We prove the feasibility of this semantics by imple-menting an automatic translation system which transforms imperative programs into their logical equivalents, and vice versa. We then implement a partial evaluator which, given a logic program representation of a program, meta-interprets it to produce a partially evalu-ated result. Using predicative programming, this partially evaluated result is translatable into its imperative equivalent. This implementation as a whole is thus a source-to-source transformation system for imperative programs. Chapter 2 reviews the areas of formal program semantics, program transformation, and partial evaluation - topics all relevant to this thesis. Chapter 3 defines a generic CHAPTER 1. INTRODUCTION 3 imperative language called Bruce. Design motivations for the language are discussed, and the language syntax and operational semantics are presented. Chapter 4 presents a new Horn clause semantics for Bruce. Motivations behind the design of the semantics are discussed. Then the semantics themselves are presented, along with some example translations. An implementation of a Bruce-logic translation system is outlined in chapter 5. A technique for optimizing Bruce programs is presented in chapter 6. An evaluation of the work concludes the thesis in chapter 7. Chapter 2 R e v i e w Brief reviews of some areas of computer science relevant to this thesis are now presented. Section 2.1 surveys the field of formal program semantics. Program transformation is discussed in section 2.2. Section 2.3 introduces the concept of partial evaluation. 2 . 1 F o r m a l P r o g r a m S e m a n t i c s 2.1.1 Goals of Program Semantics Programming languages are complex systems. Since conventional programming languages are tailored around the architecture of von Neumann machines, operations in these lan-guages are primarily motivated by hardware considerations. The functionality of program segments as they relate to the original problem specification is often not obvious to the programmer. This occurs because people do not normally define problems and solutions in terms of the hardware of a machine, but instead use natural language, mathematics, or some other human-oriented language. The task of computer programming is to convert a human-oriented specification into a machine-oriented programming language. The difference of expressiveness between programs and problem specifications becomes especially relevant when one wants to formally verify the correctness of a program. Formally proving facts about programs is difficult, since there are two levels of formal abstraction being addressed: (1) the program specification language, and (2) the programming lan-4 CHAPTER 2. REVIEW 5 guage itself, which is a formal language. Relating these two formal systems together is the task of formal program semantics, which have been established to allow people to more easily reason about programs and programming languages. Program semantics provide a means of associating programs and programming languages with objects representing their meaning. For example, these objects might be integers representing the input and output of a program module, and the means of deriving facts about the integers might take the form of functions, logical predicates, or algebraic equations. The main point is that any semantic system adopted must allow correct conclusions to be reached about the program being analyzed, and should ideally provide useful calculi with which these conclusions can be derived with the least amount of effort. A number of methodologies exist which differ in both their models of implementation and their intended purposes as tools for program and language analysis. The main semantic models are: (1) logical semantics, (2) denotational semantics, (3) operational semantics, and (4) algebraic semantics. These systems have found uses in the areas of language description and design, and program verification, synthesis, and transformation. Since some semantic methodologies are specialized for particular analytical purposes, not all semantic paradigms are used for the entire aforementioned list of applications. On the other hand, systems such as the denotational semantics have proved to be quite general in their applicability. We now briefly survey the four major semantic methodologies. Since this thesis focuses on the use of logical semantics, the section on this formalism will be emphasized accordingly. For a good comparative discussion of semantics, see [Moss 81]. [Loeckx etal. 84] presents a comprehensive overview, as well as many example applications. 2.1.2 Logical Semantics The term "logical semantics" can easily lead to confusion, as predicate logic has been used in analyzing programs in a variety of different ways. The term has historically come to represent the use of a specialized form of logic known as Hoare logic. However, the CHAPTER 2. REVIEW 6 last decade has seen other applications of predicate logic as a semantic formalism for programming languages and computation. We distinguish three distinct uses of logic in the field of program semantics: (i) Hoare logics and program verification, (ii) the logical description of computation, and (iii) logic programming. Seminal papers by [Floyd 67] [Hoare 69] [Burstall 69] established the utility of first-order predicate logic as a tool for analyzing the behavior of imperative programs. Out of this work, Hoare logics became established as a standard methodology for program verification. [Apt 81] has a comprehensive review of the field, and [Loeckx etal. 84] has example applications. Hoare logic has defined for it a standard set of axioms and inference rules which are common to most imperative languages; new languages must have new axioms and calculi defined for them (for example, [Hoare etal. 73] has a treatment of Pascal). The axioms specify the computational behavior of program constructs under particular conditions, outlining any logical inferences derivable when these conditions are satisfied. Once an axiom set is established for a language, it is applied to a program to formally prove some property of the code. Hoare logic is a major program verification tool. Its predicate logic basis gives it intuitive appeal. It uses a "flatter" domain space than denotational semantics (see be-low), the domain typically being variable values, which lends considerable simplicity to users interested in program verification. In addition, work in theorem proving has shown the applicability of Hoare-style logic in semi-automated environments [Manna etal. 77]. However, Hoare logic has been criticized for its often unsound and ad hoc axioms, and dissatisfaction has arisen to the ways in which different program constructs have been han-dled [O'Donnell 82]. Hoare logic is also unsuitable in applications requiring more abstract representations of programming languages, and does not address language implementation at all. Whereas Hoare logic is a specialized logic useful in verification, unconstrained first-order predicate logic has found a niche as a general purpose description language for computation and the programming process. One particular paradigm founded in logic CHAPTER 2. REVIEW 7 is predicative programming. Generally speaking, predicative programming is a program-ming discipline in which programs are constructed from logical specifications using first-order logic. Bibel established the term in [Bibel 75], and further illustrates the formal synthesis of programs from logical specifications in [Bibel 85]. Hehner uses the term in a similar sense, with the additional perspective that it is possible to freely intersperse con-ventional imperative-style program code with logic during program analysis and synthesis if one treats syntactic constructs of a programming language as predicates [Hehner 84a] [Hehner etal. 86]. In his system, each construct in a language has a semantic defined for it which can be (i) composed in first-order predicate calculus, (ii) defined in terms of sub-sidiary language constructs, which are likewise logically denned, or (iii) a combination of language constructs and logic. In a mixture of program code and logic, the code portions represent implementable parts of the computation, while the logic represents semantic descriptions. Using predicative programming, the transformation and analysis of code is assured of being logically sound. In addition, predicative programming provides a degree of elegance in merging these two different formal languages into one analytical framework. Hehner defines logical semantics for a typical imperative language in [Hehner 84a] and [Hehner etal. 86]. Examples are given using these semantics in verification and synthesis, as well as illustrating sophisticated aspects of programming. This style of semantics is ex-tended in [Hehner 84b] and [Hoare 85] to describe computations which utilize interprocess communication. A key advantage of logic worth mentioning is that it is easily automated. Work in the-orem proving has enabled the implementation of program transformation and verification systems. Systems such as those described in [Boyer etal. 79] and [Manna etal. 77] utilize logical semantics as an underlying formalism. Logic programming is an active field of computer science. It is a paradigm which uses Robinson's resolution principle [Robinson 65] to solve programs written as Horn clauses, a subset of first-order predicate logic. A logic program can have many semantic interpreta-tions applied to it, namely, a declarative or model theoretic semantics, and a procedural CHAPTER 2. REVIEW 8 or proof theoretic semantics [Clark etal. 81], The programming language Prolog is the current realization of the logic programming ideal [Clocksin etal. 81]. The relevance logic programming has to program semantics is that the statements of a declarative Prolog pro-gram can be directly interpreted as statements of logic. This means that there is no need for Hoare-style logics to be applied to the program when analyzing it, since the program's semantics are explicit in the program text. 2.1.3 Denotational Semantics Denotational semantics is a formalism invented by Scott and Strachey (see [Stoy 77] for an introduction). In general terms, denotational semantics refers to the interpretation of the meaning of a program strictly in terms of the meaning of its constituent parts. It is a math-ematically founded model of program semantics concerned with the theory of domains, and whose basis language is the lambda calculus. In denotational semantics, the meaning of a program is described in terms of a function from some domain to another. The definition of this function may be in terms of other functions, many of which might have complex domains. The strength of denotational semantics lies in its generality. It has been used to describe many different programming languages, such as Algol-like languages [Gordon 79] and Prolog [Allison 86]. Denotational semantics is arguably more descriptively powerful than semantics based in logic due to the high level of abstraction available. Consequently, it has been used in program verification and transformation [Stoy 77], as well as language description and design [Tennent 77] However, its simplicity has suffered at the sake of generality. Denotational descriptions of languages are often very complicated, suggesting that language description is not necessarily a natural application [Ashcroft etal. 82]. The domains which might be required by a particular language are often too abstract for the programmer trying to prove a simple fact about a program segment. In addition, imple-mentability issues are not dealt with. CHAPTER 2. REVIEW 9 2.1.4 Opera t ional Semantics Operational semantics characterize languages in terms of the machine's behavior when processing them. An operational semantics requires the definition of an abstract machine or interpreter for the language in question. This abstract machine must have incorporated within it precise definitions of behavior for the language constructs. Operational semantics are important in describing programming languages from a design and implementation standpoint, but are typically of less use in program verification and transformation. See [Cook 78], [de Bruin 81], and [Moss 81] for examples of operational definitions of languages. 2.1.5 Algebra ic Semantics The latest semantic formalism is algebraic semantics [Guessarian 81]. Algebraic semantics attempts to simplify the semantic notation and analytical calculi of program analysis to its most basic elements. In this scheme, programs are recast into algebraic expressions. Proving program properties is then transformed into proving algebraic problems. For example, to prove the equivalence of two programs, one would define algebraic schemas for the programs, and then through the use of analytical techniques such as induction and term rewriting prove that the program schema are reducible to a common algebraic representation. Algebraic semantics are used in program verification and transformation [Guessarian 81], and synthesis [Broy 84]. 2 . 2 P r o g r a m T r a n s f o r m a t i o n A comprehensive review of program transformation systems up to 1983 is in [Partsch et al. 83], upon which most of the following discussion is based. We forego mentioning many specific transformation systems in this section, and instead survey the systems most relevant to this thesis in section 2.3. [Pepper 84] also contains a detailed treatment of the field. Software engineering up to now has relied on the programmer's expertise in encoding and debugging. This is a process which has proved error prone, and as a consequence, CHAPTER 2. REVIEW 10 expensive. As a result, much research effort is currently being directed into developing more automated programming environments, and is inspiring coordinated developments in software engineering, artificial intelligence, and programming languages. These automatic programming systems, although still at the experimental stage, will eventually allow reli-able programs to be produced with the least amount of technical intervention on the part of the programmer. One key area of automatic programming is program transformation. The term "pro-gram transformation" is a general one; it has been used in reference to program transfor-mation proper, as well as program synthesis and verification. We use the term to mean the conversion of a program into one which is more efficient or contains some desired quality not found in the original program. Program synthesis, on the other hand, is the creation of a program from a formal specification. Both these applications share much basic method-ology, as one can consider the original program given to optimizing transformation systems as the "specification" used by synthesis systems. Program transformation differs from pro-gram compilation in that transformations are typically applied at a higher level than the translations done by compilers. The result of a program transformation is usually a pro-gram in the same source language exhibiting profound improvements, whereas compilers produce code which is more elementary than the source, and is "peep hole" optimized at best. Two basic approaches to program manipulation are found in transformation systems. The generative approach takes a small kernel of basic program transformation schemas and generates more complex ones from them. These schemas might be implemented as general principles of transformation, as is done in section 2.3, rather than through the use of rules per sae. The catalog approach assumes the existence of a knowledge base of program transformations. This collection of transformations might contain programming and data domain knowledge, language specific features, and efficiency information. An advantage of knowledge-based systems is that they can be upgraded with new rules when necessary. CHAPTER 2. REVIEW 11 An important factor in any transformation system is the type of rule set used, as the types and scope of the transformation rules ultimately determine the power of the system as a whole. The most elementary class of rules are the schematic or pattern replacement ones. They specify local optimizations of a program, such as boolean and algebraic simpli-fications. A more powerful class are those which are global. These rules have repercussions on an algorithmic scale, and may specify information dealing with flow analysis and gen-eral programming principles. Lastly, there exist rules which are both local and global in applicability, such as fold and unfold transformations [Darlington etal. 73]. The internal representation of programs and rules is also of importance. Some systems rely on formal program semantics as an underlying representation for programs and trans-formation rules [Manna etal. 77]. Other systems simply use syntactic representations for programs on which textual "source-to-source" transformations are applied [Loveman 77]. There are philosophical differences between these approaches. Formal approaches are mo-tivated by correctness considerations; transformations applied to programs are always as-sured of being sound, sometimes at the expense of transformational efficiency. Syntactic approaches, on the other hand, are more intuitionistic and efficient, but are prone to erroneous modifications should a transformation rule be faulty. A reconciliation is in ap-proaches founded in algebraic semantics [Broy 84], which simplify the representation of programs and rule sets while maintaining correctness considerations. Different degrees of automation exist in transformation systems. User controlled sys-tems give the user the responsibility of applying transformations to a program. The system acts as a repository of powerful editing commands, and does assorted bookkeeping tasks in order to simplify programming. At the other extreme are the fully automated systems. They require the use of heuristics to control the transformation process in order to be practical. Semi-automated systems share features of both these approaches, acting as intelligent editors for the programmer. CHAPTER 2. REVIEW 12 2 . 3 P a r t i a l E v a l u a t i o n Par t i a l evaluation, or mixed computat ion, is a computat ional paradigm which is currently gaining more attention i n research i n logic and functional programming, as wel l as conven-t ional program translat ion. P a r t i a l evaluation can be applied i n areas such as program exe-cut ion, program opt imizat ion and transformation, compiler generation, compiler-compiler generation, and meta-programming. [Ershov 82] gives an in t roduct ion to the concept, and outlines how par t ia l evaluation can be characterized i n either a functional or operational fashion. (1) Funct ional ly : given a program P which computes some function f(X, Y), par t ia l evaluation is the process of obtaining a residual program Px which computes the function f(x,Y) = g(Y), where the da ta value of X is x. Px is also known as the projection of P onto x. (2) Operat ional ly: a program P defines a set C of elementary computations. C i tself is part i t ionable into subsets C U C", where C are called permissible computations, and C" are suspendable computations. Pa r t i a l evaluation is the process which executes C and forms a residual program P^ which defines the computat ion C". These two characterizations are generalized in [Ershov 82] [Ershov 85], i n which par t ia l evaluation is defined by a mapping: M-.PxD^PxD where P are programs and D are data domains. Th is mapping can be parameterized by an ordered set {p} i n which po and p\ are min ima l and max ima l values i n the set respectively. po represents the case when no data is available to the par t ia l evaluator; p\ is the case when al l the data is available. Th is metric - the availabil i ty of da ta - effectively describes the nature of part ia l evaluation: depending on the availabil i ty of data , some parts of a program can be executed, while other portions which need undefined data values are left as residual results. The most difficult problem faced when part ia l ly evaluating a program is controll ing the evaluation process. P a r t i a l evaluation first requires the fixing of data values , usually CHAPTER 2. REVIEW 13 meaning that program parameters are set. Processing commences by executing a l l the code i n which the necessary data is defined, while retaining the code which uses unknown data values. However, undefined values i n a computat ion escalate during processing according to the data flow in the program: any value which uses an undefined value subsequently becomes undefined, and computations using i t become suspendable. P rogram constructs such as loops thus present the possibi l i ty of the infinite generation of residual code. The user is given the responsibil i ty of indica t ing the hal t ing conditions for a part icular applicat ion. Mos t implementations of par t ia l evaluators have been done i n either Lisp or Pro log . Th i s is because programs can be treated as data quite naturally wi th in these languages, which is an advantage when implementing meta-programming environments. A n early Lisp-based implementat ion of a par t ia l evaluator is i n [Beckman etal. 76], which is used for program opt imiza t ion . [Futamura 71] first suggested the use of par t ia l evaluation i n the creation of compiler-compilers , which are programs that transform interpreters in to compilers. [Jones etal. 85] implemented a par t ia l evaluator i n Lisp which was used to generate compilers and a compiler-compiler . T w o par t ia l evaluators based i n Pro log are given i n [Venken 85] and [Takeuchi etal. 85]. The Venken system can process full P ro log programs; cuts and system predicates w i th side-effects are handled. However, control facilities are l imi ted to s imply recursion detection and predicate tagging. The Takeuchi system does not handle meta- logical operators such as cut, but has extensive facilities w i th which the user can control the par t ia l evaluation. Chapter 3 A n I m p e r a t i v e L a n g u a g e C a l l e d B r u c e 3 . 1 D e s i g n M o t i v a t i o n s This thesis concentrates on the semantics and transformation of imperative programs, which are those written in languages tailored around the architecture of von Neumann machines [Backus 78]. A von Neumann machine is an abstract simplification of the con-ventional computer, having a central processing unit (CPU), a memory or store, and a two-way data bus between them. Imperative languages consequently make predominant use of: (a) variables, which represent values in the store (b) control statements, which are extensions of the CPU's jump and test abilities, and (c) assignment statements, which imitate data passing between the CPU and store. Al l programs written in imperative lan-guages share a fundamental computational methodology based on the above features, and the mappings between different imperative languages are usually trivial. A very general view of a computation on a von Neumann machine is: 1. the computer is initialized with variable values 2. as execution proceeds, the variable values are processed 3. execution eventually terminates with result values in particular variables. 14 CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 15 BoolExpr: b ::= true | false \ r(eu...,ek) | (&i V b2) \ (h A b2) | (->&) where r is a relational operator (eg. <,>,<=, etc.), Expr: e ::= x \c \ f(ex, ...,ek) where x is a variable, c is a constant, / is a function (eg. +, *, / , etc.), Figure 3.1: Syntax of expressions Other side effects usually result during a computation, such as output to a printer or screen, or movement of a robot arm or disk head. However, our view of computation will be restricted solely to the observable effects to the program variable values kept in the store. The rest of this chapter introduces an imperative language called Bruce1. Bruce is intended to be a generic language incorporating many traditional imperative features, such as destructive variable assignments, structured control mechanisms, and subprogram modules. For expository reasons, Bruce also includes branches or goto statements as a more primitive control construct. Although Bruce is by no means as robust as languages such as Pascal or "C" , it is sophisticated enough to permit interesting and nontrivial programs to be written in it. In addition, the semantics and transformations we apply to Bruce programs later in this thesis should be easily extended to real programming'languages used in production environments. The definition of Bruce will be in two parts. Section 3.2 outlines the Bruce syntax. This is followed by a presentation of Bruce's operational semantics in section 3.3. This operational semantics will be the basis for the logical semantics introduced in chapter 4. 3 . 2 S y n t a x Brian Ross's Unfriendly Computational Environment CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 16 T h e syntax of Bruce is s imilar to that of Pascal [Wir th et al. 78] and "C"[Kern ighan et al. 78] For the sake of brevity, we forego minute syntactic details i n the following definitions wi th no loss of generality. A s a result, labels and constants are assumed to have conventional denotations. Figure 3.1 has a B N F - s t y l e grammar indicat ing the construction of boolean and math-ematical expressions. Mos t common relational and ari thmetic operators may be used. We assume that conventional operator bindings are adopted, and that parentheses can be dropped without resulting i n interpretive ambiguities. Figure 3.2 has a B N F - s t y l e syntax of Bruce programs. Items enclosed i n brackets, such as statement labels, are opt ional . Items wi th an overbar (as i n a) represent lists of items. A n environment E contains a l l the programs to be executed i n a part icular appl icat ion, and represents the entire computat ional environment. A program P is a conventional program or subprogram. A program is denned by a unique program name Prognamei, parameter and local variable definitions, and a program body. Parameters may be variable or call by address parameters (the vector a), or call by value parameters (the vector e). Note that there are no data types i n Bruce. A chain Q (also referred to as a train) is a sequence of one or more statements separated by semi-colons. Each statement can be optionally labelled. F i n a l l y , a statement S represents a basic Bruce construct. Standard assignments and tests are allowed. Skip commands are nu l l instructions which have no effect whatsoever. C o n t r o l constructs such as while and repeat loops may be used, as well as more pr imi t ive constructs such as branches. Last ly , subprograms can be invoked wi th call statements, where the first list of parameters are variables to be passed by address, and the second list are expressions to be passed by value. 3.3 O p e r a t i o n a l S e m a n t i c s Establ ishing an operational semantics involves the definition of an abstract machine or interpreter. T h e style of this operational semantics is based on those i n [de B r u i n 81] CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 17 Environment: E ::= UP Programs: P ::= Prognamei(a,e) : [local x] { Q } where Progname, and each variable name v £ {a, e,x} is unique in E Chains: Q ::= [Za6e/,:]5 | [label, :] S;Q where each label labeli is unique in E Statements: S ::= skip \ v := e \ if (b) then {Q} else { Q' } | if (b) then {Q} | call Pi(v, e) | while (b) { Q } | repeat { Q } tmii/ (6) | where 6 G BoolExpr,e £ Expr,v £ variable names, Pi £ Programs Figure 3.2: Syntax of higher-level constructs CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 18 and [Cook 78]. This semantics is semi-formal in the sense that mathematical notation is descriptively useful in the operational definitions. However, there is no attempt in utilizing unnecessary rigor in this semantics, as the intent is to illustrate in elementary terms the effects of program statements on the store. We will characterize a computation by its effect on the store, and in particular, the effect on the values of the program variables. A state,cr, is a static representation of the computer store at an instant in time of the computation, and is our basic semantic unit, a is defined as a function which maps program variables to their current values in the domain space Domain: A variant o[e/v] of a state a is a state a' in which a' differs from a only in the mapping of variable v, which is mapped to e. c[e/v] represents the multiple application of a variant to a vector of elements. o~[V(e)/v] represents the multiple application of a variant in which the valuations of e are substituted. A computation sequence, denoted E, is an ordered list of successive states produced during the execution of a program: IC simply returns the final result state of terminating computation sequences. A concate-nation operator * will be used to construct computation sequences from other sequences. a : Var —> Domain E =< oi,o2,...,o-k,... > A function fC is denned as: J. if E does not terminate ok if E' =< o~o,...,o~k > If < <7A, ...,<7(, > and < oy, ...,crz > then E 1 * E 2 = < <7 0 , . . . ,<7 ( , , CT V , . . . , C T 2 > CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 19 1. Comp<E,P, S > <r 2. Comp < E, P, skip > a 3. Comp < E, P, skip; Q » a 4. Comp <E,P, x := e; Q > <r 5. Comp < £ , P, ca// P,(t>, e);Q > o-6. Comp<E,P, if(b)then{Qi}else{Q2};Q3> o-7 . Comp<E,P, i'/(6)i/ien{Q1};Q2>cr 8. Comp<^E,P, while(b){Qi};Q2 > a 9. Comp < .E1, P, repeat{Qi}until(b); Q2 > a 10. Comp < E, P,goto /<;<?> c Comp < E, P, S; skip » a <<T> <cr>* Comp <E,P, Q><T < <r[V < e » <r/x] = <r' > * Comp < £ , P, Q > oJ < <T > * (Comp < E, Pt, Q* » a' = £') *Comp<E,P,Q » a - " where P,(2,y) : {Q'} € £7, <r,- is a fresh state for P,, *' = (^/z])[V(e-)/2/] <r" = af>,/C(E'),G) Comp < E, P, Qi; Q 3 » <r (if W « 6 » = true) Comp <E,P, Q2;Q3><r (if W « 6 >= /a/se) Comp < £ , P , t7(6)f/ien{Q1}e/se{sifcip}.;Q2 » <* Comp<. £ , P ) i / ( & ) { Q i ; u>/»7e(6 ) { Q 1 } } ; Q 2 » * Comp< ^P.Qij i /^ irepeat iQjunt i /^ l jQa > < cr > * Comp < E,P,Q' > a where Q' = Buildenv(PtQi),U : Q,- 6 P Figure 3.3: Definition of Comp Now that the notational tools are defined, the actual operation semantics for Bruce can be established. The first step is to provide a means of interpreting expressions. Two functions, V and W, evaluate arithmetic and boolean expressions respectively "in the usual way": V : Exp —> o —• Domain W : BoolExp —• a —• {true, false} Here, Domain might refer to the natural numbers. A function Comp is used to build S (figure 3.3). The state sequence S for a terminating computation starts at an initial state CTQ, and ends at a state on. Comp takes as its arguments the environment E, a program P, a chain Q, and a state a. E is a source where all available program definitions may be found - a necessity when processing subprogram CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 20 Buildenv(P, Q) = -f < Q » - iiP:{Q';Q) < Q; while(b){Q';Q}; Buildenv(P, Q*) > if Q belongs to a while < Q;if(-~b){repeat{Q';Q}until(b)};Buildenv(P,Q*) > HQ belongs to a repeat < Q\ Buildenv(P, Q*) > if Q belongs to an if where S{Q';Q};Q*, ie. S is the parent statement containing subchain Q, and Q* is the chain following S Figure 3.4: Definition of Buildenv calls. P defines which labels may be used as branch destinations. The chain Q is the program code currently being processed, a is the current state of the store. Some features of Comp are worth explanation. Line 1 simplifies Comp so that op-erational definitions are not duplicated for single- and multiple-statement chains. Lines 2 and 3 define the skip instruction. In line 4, an assignment results in a state variant's creation of a new state cr', which is used by the following chain. Tests (lines 6 and 7) are handled by the execution of the appropriate chain of code according to the value of the test expression. While loops (line 8) are processed by reducing the construct into a test. The body of the test is composed to simulate the iterative nature of the loop should the loop test be positive. Repeat loops (line 9) are handled similarly. Subprogram invocation (line 5) is more complex. A stack mechanism is assumed to exist so that nested subprogram calling, including recursion, can occur. When calling a new program, the pre-existing arguments to Comp are implicitly saved on the stack, and a "fresh" state cr,- is created for the new subprogram to be executed. Before executing the subprogram, multiple variants are performed on 0{ in order to initialize the store with the values of the variable and value parameters being passed. The subprogram is then executed, eventually producing a state sequence S*. Finally, changes in the variable parameters which may have occurred during the subprogram call must be accounted for. This is a mechanical process which we give to a function a. a takes as arguments the old state cr, the final state of £ ' , and the variable parameter vector v, and returns a new state with a set appropriately. State variants would be used in the creation of this new state. CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 21 KMLUM a := 1; goto gl; while (a < b) { repeat { gl: a := a + 2 } until (a == b); a := a + 3; }; a := a + 4 } Figure 3.5: Example Program a := a + 2; .7 Ha ==&)){ repeat { a := a + 2 } imii/ (a == 6); }; a := a + 3; to/w'/e (a < b) { repeat { a := a + 2 } unii/ (a == 6); a := a + 3; }; a := a + 4 Figure 3.6: Buildenv Output CHAPTER 3. AN IMPERATIVE LANGUAGE CALLED BRUCE 22 When processing branches (line 10), Comp makes use of an auxiliary function Buildenv (figure 3.4). The branch itself results in no change to the state, and the chain following the branch is ignored, which reflects the destructive nature branches have on command sequencing. Following the branch is the computation of the chain of code at label,. Us-ing Buildenv, the control context normally found at the branch destination is recreated. Buildenv creates a chain of program code by taking the chain at the destination label and appending appropriate control code for successive parent constructs, resulting in a chain of code which has an appropriate control context. For example, figure 3.5 is a Bruce pro-gram containing a branch into two nested loops. Figure 3.6 contains the code generated by Buildenv for the label gl. Once Comp is defined, we complete the operational semantics of a program using a function M, which is the meaning function of a program: M < P > (T0 = K.(Comp < E,Q,Q > o0) where P : {Q} € E. This can be thought of as the initial module executed in order to start Comp's evaluation of the program. In summary, the Bruce abstract machine (BAM) executes by code manipulation (Comp), expression evaluation (V and W), and writing values to the store (state variants). The fea-ture of this operational semantics worth special attention is the way control is processed by Comp. If one were to observe the contents of Compos chain argument, one would see an ever-changing chain of program instructions. This chain reflects the control context of the program at any particular moment in the computation. This somewhat parallels the way people "hand compute" programs, in that tracing a program's flow of control involves the implicit textual context of statements, in particular, the constructs in which they are nested and the code textually following them. The Bruce machine does this by explicitly constructing this context. Chapter 4 A Horn C l a u s e S e m a n t i c s T h i s chapter introduces a new semantic methodology for imperat ive programs. In partic-ular, a H o r n clause semantics is presented for the Bruce language of chapter 3. Section 4.1 discusses some of the philosophical motivations behind the design of the semantics. The logical semantics for basic Bruce programs, that is , ones in which branches are not used, is given i n section 4.2. The semantics of branches is then detailed i n section 4.3. Section 4.4 discusses the interpretation of the semantics as logic programs, and addresses some completeness issues. Some examples of actual translations of Bruce programs conclude the chapter i n section 4.6. 4 . 1 D e s i g n G o a l s There are a number of design motivations for the logical semantics being introduced i n this chapter. Since computat ion is to be defined solely by the state of the store, the min ima l requirement for the semantics is that it has enough expressive capabil i ty wi th which to describe this characterization of computat ion. This requirement should not be an obstacle, as predicate logic has proved to be a powerful tool i n the semantics of computation and programming languages (see section 2.1.2). Our ma in mot ivat ion, however, is to define a semantic system which allows efficient and powerful transformations of imperat ive-style programs, namely, those wri t ten i n Bruce. 23 CHAPTER 4. A HORN CLAUSE SEMANTICS 24 The fact that the semantics is to be used in a program transformation environment means that its semantic scope can be constrained somewhat, especially when compared to the scope of semantic systems used in program verification environments. The program trans-formation system to be used in this thesis will take as input an imperative program, and will produce a transformed, optimized program as output. A key assumption is that the source program being input is to be considered complete and correct, both syntactically and semantically. This assumption greatly simplifies the scope of the semantics, as we do not have to deal with such issues as the well-formedness of the source code, the termina-tion of mechanisms, the evaluability of expressions, and the matching of data types. More general semantic systems, such as that presented in [Hehner 84a], address such issues. A major goal of the semantics is that there should exist a strong and natural rela-tionship between the source language and its corresponding semantic representation. The predicative programming paradigm offers a solution in this regard. The scheme is to de-fine for every construct of the source language a predicative meaning. This proves to be advantageous when converting between the source and logic, as program constructs can be considered to be predicate labels for their corresponding semantic definitions. Such a mapping between the source language and logic can be utilized in both directions, which is an ideal situation since such conversions will be required by the program transformation process. Finally, it is prudent to consider the recent accomplishments in defining models of com-putation for first-order predicate logic. In particular, work in logic programming has shown the suitability and practicality of Prolog in various theoretical and practical applications. What is especially worth noting is that Prolog is well suited to many types of program transformations. A program written in pure Prolog (one without meta-logical operators) can have many types of transformations applied to it, in fact, any transformation which can be proved to be logically valid. Ascribing a logic programming model to our seman-tics means that a richer, sounder, and more automatable transformation system might be possible. CHAPTER 4. A HORN CLAUSE SEMANTICS 25 4 . 2 B a s i c B r u c e S e m a n t i c s We now present the semantics of Bruce programs having no branches1. In section 3.3 a computational environment E is denned as a particular set of programs. In logic, this environment defines a theory Th(E) = (B,A) where B = (F, P) is a predicative basis, and A is a set of axioms. The basis is composed of a set of function symbols F and a set of predicate symbols P. F contains all the arithmetic, relational, and boolean functors, as well as the domain dependent constants, used in Bruce. P contains the atoms asgn and callasgn, the propositional constants true and false, plus additional predicates dependent upon the structure of the programs in E. The axioms A, collectively known as the program predicate, are created through the principles of predicative programming. The composition of these axioms reflect the syntactic structure of the program, and will be detailed shortly. A mechanism is a basic module of computation which has observable, well denned behavior. Mechanisms are defined by particular syntactic structures of the programming language whose behavior have been predefined in logic. Bruce constructs which exhibit well defined behavior, such as programs, assignments, if tests, loops, and branches, are treated as mechanisms. Mechanisms are also defined by computational events which occur during the execution of a program, such as the evaluation of value parameters during subprogram invocation. Mechanisms fall into two categories: (1) elementary mechanisms, such as assignments, which are described in logic by atoms, and (2) complex mechanisms, which is any construct which requires a predicative definition. Satisfiability in this logical semantics denotes that a mechanism is implementable. An unsatisfiable program predicate, one which evaluates to logical false, is unimplementable or under specified. A consequence of this convention is that the logical values true and false are themselves program specifications, being the universally satisfiable and unsatis-'This semantics is used in the initial stages of defining the semantics of program branches in section 4.3. CHAPTER 4. A HORN CLAUSE SEMANTICS 26 fiable program specifications respectively. We restrict our logical semantics so that all axioms for complex mechanisms are written as Horn clauses. A Horn clause is a formula of predicate logic having the form V ( / J <= C i A C2 A . . . A Cfc) where H is termed the head, and the conjunction of C,'s is called the body. The Cj's are typically input-output relations in most axioms. The informal semantics of this formula is: if the relations C, all hold for some particular instances of memory states, then H holds. The C, relations which represent complex mechanisms require their own subsequent Horn clause definitions, and so on. A program predicate thus has the form: |= V((P <= Si A ... A Sk) A (Si Ti A ... A Tm)... A (Tj ^ W\ A ...) A ...) where the S;'s, T,'s, and W,'s are input-output relations. Input-output relations have included as arguments two state vectors, one for the input state of the computation, and the other for the output state. For example, in the relation if2(vi,Vf) the vectors Vi and Vf represent the initial and final store states during the execution of the mechanism if 2. Each input-output vector represents the state a of the computer's store at a particular instant in time. The elements of input-output vectors are logical variables whose scope is the clause within which they are used, and whose domains are the value domains of the variables used in Bruce. Each element represents the value of a particular variable parameter, value parameter, or local variable during an instant of the computation. Under some circumstances vector elements might be set to domain values2. Such values represent implicit assignments to the Bruce objects that the vector elements represent. Figure 4.1 presents the axiomatic semantics of Bruce constructs without branches. The semantics are logical descriptions of the behavior of Comp in Bruce's operational semantics (figure 3.3). Generally speaking, each complex mechanism in a program is represented by 2 We will see such a phenomenon occur in chapter 6. CHAPTER 4. A HORN CLAUSE SEMANTICS 27 1. Programs: Progname(a,e) : local x { Q } = |= Progname(< a,-,e"j >,< a/,e,- >) <= Q(<ai,ei,Xi>,<a},ef,xf>) 2. Chains: Q = Si;5 2;. . .;5j. d= |= Q(vi, vf) = 5i(t}<, d) A 52(t;i, U2) A ... A £*(€«,_!,£*) 3.Null operation: sfcip 1 = true 4. Assignment: a: := e =f [= as0n(t;,-, v x ,e ,vj) 5.Program invocation: def ca// P(< vi Vj >, < e i , e k >) = |= callasgn(v,x\, e\) A ... A ca//as<7n(t>,xjfc, ej,) AP(< Vl,...,Vj,Xi,...,Xk >,Vf) 6.(a) Test: l/ien { Qi } else { <?2 } A (ifi(vi, vf) <r - - 6 A Q2(i>,-,«/)) »7 ( 6 ) Me Hf |= By) «= 6 A Qifa, €/)) 6.(b) Test: 1/ ( 6 ) then { Qi } d= |= ( i /< (« j , 0 / ) 4= 6 A Q^, vj)) A (ifi(vitVi) -16) 7. While loops: tu/u/e ( 6 ) { Q } d= |= (whilei(vi,vj) <= dAQ^i,^) Awhilei(v2,Vf)) A (whilei(vi, Vi) • £ = - > 6 ) 8. Repeat loops: def repeat { Q } tmii/ ( 6 ) = |=.(repeflrf,-(uj,«/) •£= Q(C,-, €2) A->b A repeati(v2, v/)) A (repeal (v,-, €/) A 6 ) Figure 4.1: Logical semantics of Bruce constructs (no branching) CHAPTER 4. A HORN CLAUSE SEMANTICS 28 a uniquely named predicate. Our scheme is to generate unique predicate names through numbering. For example, a program with three if tests has generated for it three predicates named ifl, if2, and i /3 . The only relevance that a predicate name has is that it is unique; the label name itself is only for notational convenience. When a predicate is being converted into Bruce code, the fact that the predicate might be called if2 does not necessarily imply that it represents an if test, since only the logical form of the predicate is used for the translation. Line 1 specifies the high level semantics of programs, as well as the composition of input-output vectors. A program Progname is defined by the predicative meaning of its main program chain Q. The change to the store when executing Progname is indicated by the changes to the input-output vectors used within the relations for Progname and Q. Within all predicates, input-output vector elements are mapped to their Bruce objects by their positions in the vector. In particular, a program Progname having variable parameters a, value parameters e, and local variables x uses the vector format < a, e,x > throughout the rest of the program predicate. The manner in which vector values are shared between Progname and Q depends upon the nature of the store objects in question. Since local variables (x) are only active during the execution of the program body, they are not used in the predicate header. In addition, value parameters (e) are not changed by the program's execution; thus their final values in the program header are the same as their initial values. The composition of statements is represented in Bruce by chains, which are statements separated by the sequencing operator ";". In logic, this is represented by conjuncting the relations for each statement in the chain (line 2). Intermediate input-output vectors are used to "pass" the value of the store among the relations. As was mentioned above, the relations themselves often have auxiliary definitions. Elementary relations, represented by atoms, define the behavior of elementary mech-anisms. There are four elementary relations representing assignments (line 4), boolean tests, skip statements (line 3), and value parameter evaluation when invoking subpro-grams. asgn(v{,vx,e, vj) is an elementary relation which represents a state variant. vx CHAPTER 4. A HORN CLAUSE SEMANTICS 29 is a logical variable which represents the element in the output vector vj corresponding to the store location for variable x. vj is the state which results after substituting the value of the logical variable vx in vj with the value of expression e in the context of input state Vi. Boolean tests, which are represented by the boolean expression 6 throughout the definitions, are also elementary relations. They implicitly use the input vector appropriate to the context of the test within each definition, skip instructions are simply denned by logical true. Subprogram invocation (line 5) is represented by an input-output relation for the sub-program in question. The input and output vectors within this relation are constructed to match the particular parameter conventions of the program being invoked. An input-output vector with the variable parameters followed by the value parameters is constructed, as is shown in the definition. However, the value parameter elements first require that each expression being passed is evaluated with respect to the current state of the store (v). callasgn(v,x,e) is an elementary relation which equates the value of expression e in the context of the next state v with a logical variable x. These expression values are then placed into the subprogram relation's input vector. The output vector of the subprogram relation represents the final state of the parameters after execution has completed. Since only the variable parameters could have possibly changed, the final values of these elements are appropriately distributed to the current program state. This distribution of parameter values means that any relation following the subprogram call has the final parameter values placed within its input vector. Should the call be the last statement of a chain, then the values may affect the output vector of the predicative header to which the chain belongs. Test constructs have straight-forward definitions. A Bruce if construct with then and else alternatives (line 6(a)) always has one of the two test bodies executed according to the outcome of the boolean test. The corresponding logical semantic mirrors this fact: if the boolean test is true, then chain Q\ is executed, which is abbreviated in the definition by an input-output relation for the chain. Otherwise chain Q2 is executed. In actuality, these chains are represented by conjunctions of relations (as in line (2)). An if construct CHAPTER 4. A HORN CLAUSE SEMANTICS 30 with no else alternative is represented by a clause with a null body (line 6(b)). This is a simplified representation for a chain containing the skip statement used by Comp, which in our semantics is denned as true (line 3). While loops (line 7), are defined by two clauses, one denning the iterative case, and the other the exit condition. The iterative clause specifies a relation which holds if the while test is true, in which case the loop body is executed, and the loop itself iterates. Iteration is defined by a recursive restatement of the relation for the while construct. The treatment of repeat loops (line 8) is similar to that of while loops. 4 . 3 P r o g r a m B r a n c h e s Branches add a dimension of complexity to the semantics of Bruce. A program branch has consequences on the composition of commands, as it destroys statement sequencing. In addition, branching alters the logical semantics of constructs. For example, a branch can be used to jump out of one or more nested loops - an action which dramatically corrupts their normal semantics. The semantics of such a loop is now dependent on the contents of that loop's body. The existence of branches therefore means that the syntactic "surface structure" of a statement is not sufficient for derivation of the semantics. Instead, the semantics are now dependent on code within the statement. Two distinct phenomena occur during the execution of a branch. First, when a branch is executed, every mechanism which is active is in effect halted. In other words, the current control context of the program is terminated. Second, a new control context found at the branch destination is then used to commence subsequent execution. Defining the logical semantics of branches is likewise done in two steps: defining new control contexts, and terminating old control contexts. First, the activation of new control contexts is defined. Our treatment of branches makes use of the concept of continuations [Clint etal. 72] [Stoy 77] [Tennent 81]. In a language with branching, a continuation for a statement is the expected results of all the program computation which will temporally CHAPTER 4. A HORN CLAUSE SEMANTICS 31 follow the statement's execution. The meaning of a branch is therefore the direct effect on the store, which is none, plus the effect of the continuation which, in the case of branches, is the effect of executing the code at the statement label. We treat a branch as a call to the label program identified by the branch destination label: goto labels d= labeli(v{,Vf) Here, v/ represents the final state of the store for the rest of the mechanism's execution, in effect, the continuation for the program. The label program itself is' defined in Bruce's operational semantics by the output of the Buildenv function, which recreates the control context of a labelled statement. Using predicative programming, we define the logical meaning of a branch destination by simply generating a predicate for the code created by Buildenv. Hence, we define for each labelled statement in a program a label program predicate: labeli(vi,vj) Q(vi,Vf) in which Q(vi,Vf) is the predicative meaning of the code generated by Buildenv for that label. The next step is to account for the termination of the current control context caused by a branch. The control context of any statement of a program can be determined as follows. Consider a statement S whose control context is to be found. We expand the program predicate, starting from the main chain, by replacing each parent construct of 5 by its logical definition. This continues until we reach S. Next, distributivity about logical or(v) is used to create a disjunction of terms. This distribution about " V " should be done so that the sequencing of terms is not altered, as this sequence reflects the relative order in which tests and statements are executed during computation. Each disjunct is composed of a mixture of chains of code conjuncted with boolean tests, which is a situation acceptable in predicative programming given the interchangeability of code and logic. Semantically, each disjunct describes a trace of the program control that can occur during execution. The control context of the statement S is represented by the conjunction of relations following each instance of S in the predicate. CHAPTER 4. A HORN CLAUSE SEMANTICS 32 (i) P <*= while(bi){while(b2){goto end}}; end : S (ii) <$= (bi Awhile(b2){goto end};while(bi)W , -<bi);end:S ' while (b )i ^ (bi A(b?/\ goto end;while(b2)v , ., ,1 w -"62); while(b\) V -161);end : 5 u>m/e (62)! <7<rfo end } (it;) 61 A 62 A 50*0 end;u;/ii/e(62); w/ii/e(6i);end : 5 V 61 A -162 A while(b\);end : 5 V -161 A end : 5 } (t>) ««= b1Ab2Aend(vi,Vf) V 61 A -162 A while(bi);end : 5 V -161 A end : 5 where end(v{,vj) -<= S(v;,t;/) Figure 4.2: Branching out of two loops To determine the effect that a branch has on the control context, we must first expand the program predicate as previously described. This expansion produces the semantic description of the control context following the branch. Given the appearance of a branch in a disjunct of the predicate, the termination of the control context at that branch is defined as Ri A ... A Rj-i A goto label, A Rj A ... A Rk =f Ri A ... A Rj-i A labeli(vi, vj) where Rj A ... A Rk is the control context for the branch. The disappearance of Rj A... A Rk from the predicate is equivalent to removing its effect on control. This restructuring is then applied to each disjunct containing the branch. The net effect of the restructuring is to "pre—compile" the effects of the branch on sequencing into the predicate. In summary, the predicative restructuring procedure is as follows: 1. Expand statements by their semantic definitions until a branch is revealed. 2. Distribute the chains of code over the logical or (v) connective until we get a dis-junction of terms. 3. Remove terms and chains of code which sequentially follow the branch. CHAPTER 4. A HORN CLAUSE SEMANTICS 33 4. Replace the branch by a call to its label program. 5. (Optional) Simplify the disjunction by factoring common terms using distributivity. Of course, logical manipulations can be economized and predicative equivalences can be preserved when expanding and simplifying the program predicate. Figure 4.2 shows a program where a branch removes control out of two nested loops (relations are abbreviated). One expansion of each loop (step (hi)) is required in order to produce the chain containing the branch. In step (iv), the chains are distributed through the internal disjunctions, creating a single disjunction of chains. Finally, step (v) shows the removal of the chain following the branch, and the replacement of the branch with a call to the label program (see first disjunct). With respect to the theory Th(E) outlined in section 4.2, the incorporation of branches in the semantics means that the predicative basis B is supplemented with relations for the label programs, and that the axioms A are supplemented with label program predicates. However, an unfortunate aspect of branches is that we can no longer rely on a straight-forward inspection of the program syntax in order to derive program axioms, as is used by the basic semantics, but must instead use the restructuring procedure outlined above. Even though the methodology of deriving axioms has become much less elegant, we still end up with a semantic description for the program which is as logically sound as for programs without branches. Only the formula for axiom derivation has suffered in terms of complexity. 4 . 4 L o g i c P r o g r a m I n t e r p r e t a t i o n a n d C o m p l e t e n e s s Given a program P, we define for it a set of Horn clauses which define the input-output behavior of P and its constituent parts. One last clause to be added to the semantics is a CHAPTER 4. A HORN CLAUSE SEMANTICS 34 goal clause, which represents an invocation of the program: |= ->P(Vi,Vf) The input parameters to P would be appropriately set i n the u,- input vector. The axioms and goal clause for P has a logic program interpretation [Clocksin etal. 81], and has both a procedural and declarative semantics [van Emden etal. 76]. Thus , through the logic programming paradigm, the complete logical semantics of a program can be treated as a logic program, and can be executed using S L D N F resolution [Lloyd 84]. In order to more closely ally our semantics wi th the logic programming concept, we henceforth use the Pro log notat ion from [Clocksin etal. 81] wi th which to write the seman-tics. The typ ica l form of a H o r n clause is now: P ^ C i A C 2 A . . . A C f c d= P : -CUC2, ...,Ck. A l s o , input-output vectors w i l l now be writ ten in terms of Prolog lists: v =< vi,...,vk > d= [vi,v2,...,vk] W e assume that any Pro log interpreter used to execute the semantics has available to i t the ari thmetic and boolean expression evaluators V and W from the operational semantics. The logic program interpretat ion of the semantics also makes the axioms logically stronger. The problem wi th the "bare" logical interpretation of the axioms is that the logical implicat ions used i n the formulas are only par t ia l specifications of the behavior of mechanisms. For example, a mechanism M described by two clauses is logically equivalent to the following: . |= (M <= C i ) A (M C2) = \= M ( d V C2) This states that M is satisfied i f C\ or C2 are satisfied, or both . However, this is only a par t ia l specification of the behavior of M, as when C\ and C2 are both false, M is s t i l l satisfied. W h a t we need is for the impl ica t ion i n each predicate to be read as a logical equivalence, or iff. CHAPTER 4. A HORN CLAUSE SEMANTICS 35 Fortunately, when the semantics are interpreted as a logic program, the predicates be-come logically complete specifications. The completion of a logic program is a logical char-acterization given the effects of SLDNF resolution on program interpretation [Lloyd 84]. If p(h,...,tn) <= Li,...,Lm is one of k clauses denning p, we first transform each clause into p(xi, . . . ,x„) 3yi..3yd((xi = ti) A ... A (xn = tn) A L\ A .. A Lm) where x\,...,xn are new variables, and yi,...,yd are the variables of the original clause. The predicate for p is thus p(xu...,xn) Ex V . . . v £ j t where each Ei has the form 3y1..3yd((xi = f x) A ... A (xn = tn) A I x A .. A Lm) The completed definition of p is then Vx1...Vxn(p(x1, ...,xn) ^ ^ V ... V Ek) This is the logical meaning of a predicate given the effects of SLDNF resolution, and is assumed implicit in all pure Prolog programs. This means that our logical axioms are complete specifications. 4.5 T r a n s l a t i n g L o g i c t o B r u c e Once a program is denned in terms of the preceding semantics, its semantic representation can be transformed and analyzed using the laws of first-order predicate logic. In a program transformation environment, the intent is for the semantics to be manipulated to produce a result which yields greater efficiency or some other desired quality not found in the original source program. This optimized representation should then be transformed back into the source language using predicative programming. CHAPTER 4. A HORN CLAUSE SEMANTICS 36 Compiling a logical representation back into Bruce is the inverse of generating the logic from Bruce. Given a set of axioms, they are matched "backwards" to the Bruce constructs using the axiom schema in figure 4.1 of section 4.2. However, it is possible that a direct match is not possible between the axioms being matched and the definitions for Bruce constructs. As a consequence, logical manipulation of the axioms might be required until a match can be obtained. The conversion of basic Bruce constructs is straight-forward. However, the conversion of branches and branch destinations needs clarification. Branches are treated as label program relations in our semantics. These label programs have embedded in them the continuation of the computation, or in other words, the result of the rest of the computation. As a result, there should never be instances of other goals making use of the output vector of a branch relation. Instead, the output of a label relation is given to the output of the clause within which it resides: P(vi,Vf) •<= C\(vi,V2) A ... A Branch(vk,Vf) Therefore, any complex relation (that is, one with a predicative definition) which is the final goal' of a clause can be considered as a branch. The branch destination is simply the Bruce code derived for the predicate describing the branch relation, prepended with a unique destination label. The placement of the destination code within the Bruce program can become somewhat involved, as the code should not interfere with the control of other program constructs. A solution to this is to unfold the first instance of a branch. When a branch relation is first discovered, instead of creating a branch statement to it, the relation is replaced by the code defining the destination, which is labelled with a destination label. Subsequent branch relations referring to this destination will simply refer to this unfolded code, and can be replaced with branches to it. An example of branch translation is in figure 4.3. Predicate A contains the logical semantics to be converted. Predicate B has the predicate for c\ converted to its Bruce realization. This assignment is unfolded into p in predicate C, and is given the label c\. D has the reference to c2 replaced by its equivalent definition. Finally, this reference to c\ is CHAPTER 4. A HORN CLAUSE SEMANTICS 37 A : |= (p(vi,vf) <= ci(vi,v2) A c2(v2,Vf)) A(c2(vi,vj) Ci(«,-,fJ/)) 5 : |= (j>(0i,G/) <= ci(ut»u 2) A c2(v2,vf)) A(ci(vi,vf) ^=x:=y+l) A(c2(vi,Vf) ><=ci (!>,•,!>/)) C : |=(p(®i,^/) c l : x := y + 1 A c2(v2,vf)) A(c2(vi,vf) <=ci(vi,vj)) D : |= (p(vi, vf) c l : X := y + 1 A ci(t>2, vf)) E : |= (p(vi, Vf) <= (cl : x := y + l;goto cl) Figure 4.3: Converting Branches replaced with a branch, since the code for c\ has already been converted. 4 . 6 E x a m p l e T r a n s l a t i o n s This section presents some example translations of Bruce programs into logic, and vice versa. Al l the examples are generated by an automatic translation system, particulars of which are discussed in chapter 5. Figure 4.4 contains a simple Bruce program with three consecutive assignments to a variable parameter x, along with its semantics. The sequential nature of the Bruce program is captured in the semantics by the naming of the logical variables in the input-output vectors. The result of the final assignment is given to the header for prog. The converted result for the semantics is identical to the original program. prog([x],[]) : { x := x + 1; x := x + 3 prog([Xl],[X2]) : -asgn([Xl],X3,Xl + 1,[X3]), asgn([X3),X4,X3 + 2,[X4]), asgn([X4],X2,X4 + 3, [X2]). } Figure 4.4: Consecutive assignments CHAPTER 4. A HORN CLAUSE SEMANTICS 38 y := i ; while (n > 0) { n := n — 1; y := y * x } } y:= i ; w/ii7e (n > 0) { n := n — 1; y := y * x } } p ( [ y i , X l , J V l ] , [ Y 2 , X l , i V l ] ) : -a s 5 n ( [ y i , X l , 7 V l ] , y 3 , l , [ F 3 , X l , i V l ] ) , wW/cl([r3, X I , Nl], [Y2, X2, N2]). whilel([Yl,Xl,Nl],[Y2,X2,N2]) : -Nl > 0, asgn{[Yl,Xl,Nl],N3,Nl - 1 , [Y1 ,X1 ,N3] ) , asgn([Y 1, X I , JV3], y 3 , Y1 * X I , [F3, X I , iV3]), w/iz/el([y3, X I , JV3], [Y2, X 2 , iV2]). w / i i / e l ( [ y i , X l , i V l ] , [ y i , X l , i V l ] ) : -- . i V l > 0. Figure 4.5: While loop P{[y],[x,n]) : { y : = l ; w/iz/el : i'/ (n > 0) { n := n — 1; y := y * x; goto whilel } } OR Figure 4.6: Two alternate Bruce realizations A more complex Bruce program is in figure 4.5. Two clauses, collectively defining the predicate whilel, describe the while loop. Because changes to the value parameters x and n are not available to any calling mechanisms, the two input-output vector elements corresponding to these objects are not altered in the header for p. Two possible Bruce realizations for the semantics are in figure 4.6. The first program is the same as the original source. The second one, however, replaces the while loop by a branch and test mechanism. Figure 4.7 contains the treatment of subprogram invocations. The four expressions making up the call-by-value argument list are each given callasgn relations, and the logical variables representing the valuation of the expressions are passed to the subprogram. Note the distribution of the new variable argument values into the subsequent assignments occurring after the subprogram call. CHAPTER 4. A HORN CLAUSE SEMANTICS 39 progA([a,b,c],[x,y,z]) : local[games,work] { x := 3; work := 6; call proc([a, b, work], [5,x, y, (3 4- 4)]); c := 8; z := 10 } proc([q,w,e],[rr,r,t,y]) : { q := w } progA([Al,Bl,Cl,Xl,Yl,Zl],[A2,B2,C2,Xl,Yl,Zl]) : -asgn([Al,Bl,Cl,Xl,Yl,Zl,Gal,Wol],X2,3,[Al,Bl,Cl,X2,Yl,Zl,Gal,Wol]), asgn([Al,Bl,Cl,X2,Yl,Zl,Gal,Wol],Wo2,Q,[Al,Bl,Cl,X2,Yl,Zl,Gal,Wo2]), callasgn([Al, Bl, CI, X2, Yl, Zl, Gal, Wo2], Tl, 5), callasgn([Al, Bl,Cl, X2,Yl, Zl, Gal, Wo2],T2, X2), callasgn([Al, Bl, Cl, X2, Yl, Zl, Gal, Wo2], T3, Yl), callasgn([Al, Bl, Cl, X2, Y1, Zl, Gal, Wo2],T4,3 + 4), proc([Al, Bl, Wo2, Tl, T2, T3, T4], [A2, B2, Wo3, T5, T6, Tl, T8]), asgn([A2, B2, C1,X2,Y1,Z1, Gal, Wo3], C2,8, [A2,B2, C2, X2, Yl, Zl, Gal, WoZ]), asgn([A2, B2, C2, X2, Y1,Z1, Gal, WoZ), Z2,10, [A2,B2, C2, X2, Yl, Z2, Gal, WoZ]). proc([Ql,Wl,El,Rrl,Rl,Tl,Yl],[Q2,Wl,El,Rrl,Rl,Tl,Yl]) : -asgn([Ql,Wl,El,Rrl,Rl,Tl,Yl],Q2,Wl,[Q2,Wl,El,Rrl,Rl,Tl,Yl]). Figure 4.7: Subprogram invocation CHAPTER 4. A HORN CLAUSE SEMANTICS 40 prog([Xl,Yl),[X2,Y2}) :-11([X1,Y1],[X2,Y2]). 10([X1,Y1],[X2,Y2)) :-asgn([Xl,Yl],X3,Yl + l,[X3,yi]), asgn([X3, Y1],Y3, X3 + 2, [X3, Y3]), P « f ( [ . , * [ ] ) : { « ( [ X 3 , y 3 U X 2 , y 2 l ) . goto 11; I0:x:=y+1; l2:y:=x + 2; goto 13; l4:x:=y + 4; goto end; l3:y:=x + 3; goto 14; 11 : x := y+ 1; end^-x asgn([Xl,Yl],Y3,Xl + 3,[Xl,YZ}), ' V ' ~ ,4([X1, Y3], [X2, Y2}). } 11([X1,Y1],[X2,Y2]) :-asgn([Xl,Yl],X3,Yl + 1,[X3,Y1]), /2([X3,yi],[X2,y2]). /2([Xl,yi],[X2,F2]) : -asgn([Xl, Y1], Y3, X I + 2, [XI, Y3]), /3([Xl,F3],[X2,y2]). 13([X1,Y1],[X2,Y2}) :-/4([Xl,yi],[X2,F2]) : -asgn([Xl,Yl],X3,Yl + 4,[X3,Y1]), end([X3,yi],[X2,y2]). end([Xl,yi],[Xl,y2]) : -as^n([Xl,yi],y2,Xl,[Xl,y2]). Figure 4.8: Branching within a chain prog([x,y],[]) : { x := y + 1; y:=x + 2; y:=x + 3; x := y + 4; y.-x } Figure 4.9: Bruce equivalent CHAPTER 4. A HORN CLAUSE SEMANTICS 41 prog([y,n],[]): local [x,eof] { n := 0; while (true) { call read([x], [ ]); n := n + 1; if (eof =:= true) { goto end }; y •= y + x };. end : n := n — 1 } Figure 4.10: End of file control scheme (initial) A treatment of program branches is illustrated in figure 4.8. A label predicate is created for each labelled statement in the program. The converted Bruce program in figure 4.9 illustrates an interesting side-effect of the conversion algorithm: since the first instance of any branch is unfolded, the branches in the original program are lost. A more complex branching scheme is illustrated in figure 4.10. This program uses a common control strategy for exiting loops based on an end-of-file condition. The reference to eof represents a system call which signals the end of the input stream. Figure 4.11 has the logical equivalent of the source, and the Bruce program derived from it is in figure 4.12. The old loop structure is lost, as it never represented a true while loop anyway. This new program outlines the control which was implicit in the original source. Note that it would have been possible to simplify the program predicate (for example, the tests true and -ttrue) before generating the final program. One final example is the program in figure 4.13, which contains a jump into the middle of a repeat loop. The program derived after translation into logic (figure 4.14) illustrates the complexity in control which may arise when using jumps. C H A P T E R 4. A HORN CLAUSE SEMANTICS prog([Yl,Nl],[Y2,N2}) :-asgn([Y 1,7Y1, X3, EofZ], N4,0, [71,7Y4, X3, EofZ]), whilel([Yl, N4, X3, EofZ], [Y2, N2, XI, Eofl]). whilel{[Yl,Nl,Xl,Eofl],[Y2,N2,X2,Eof2]) : -true, read([Xl],[X4}), asgn{[Yl,Nl,X4,Eofl],N6,Nl + l,[Yl,N6,X4,Eofl}), testl([Y 1, NQ, X4, E o / l ] , [Y2, N2, X2, Eof2}). whilel([Yl,Nl,Xl,Eofl],[Yl,N2,Xl,Eofl]) : --itrue, asgn([Yl,Nl,Xl,Eofl],N2,Nl - 1 , [ Y 1 , N 2 , X 1 , E o f l ] ) . testl([Yl,Nl,Xl,Eofl],[Y2,N2,X2,Eof2]) : -Eofl =:= true, end([Y 1, /VI, X I , Eofl], [Y2, N2, X2, Eof2]). testl([Yl,Nl,Xl,Eofl],[Y2,N2,X2,Eof2]) : --\Eofl =:= true, asgn([Yl,Nl,Xl,Eofl],Y4,Yl + Xl,[Y4,Nl,Xl,Eofl]), whilel([Y4, N1,X1, Eofl], [Y2, N2, X2, Eo f2]). end([Yl,Nl,Xl,Eofl],[Yl,N2,Xl,Eofl]) : -asgn([Yl,Nl,Xl,Eofl],N2,Nl - l , [y i , J V 2 , X l , £ o / l ] ) . Figure 4.11: Logical Form CHAPTER 4. A HORN CLAUSE SEMANTICS prog([y,n],[]) : local [x,eof]{ n := 0; whilel : if (true) { call read([x], [ ]); n := n + 1; if (eof =:= <rue) { n := n — 1 } e/se { y := y + x; goto whilel } } else { n := n — 1 } } Figure 4.12: Derived result C H A P T E R 4. A HORN CLAUSE SEMANTICS 44 progl([x,y},[}) : { x := x + 1; y.= y + 2; repeat { x := x + 3; / l : y := a; 4- 4 } until (x —:= y); goto ll } progl([Xl,Yl],[X2,Y2}) :-asgn([Xl, Yl], X3,X1 + 1, [X3, Yl}), asgn{[X3,Yl],Y3,Yl + 2,[X3,Y3]), repeatl([X3,Y3],[X4,Y4]), ll([X4,Y4),[X2,Y2]). 11({X1,Y1],[X2,Y2}) :-asgn([Xl, Y1], Y3, XI + 4, [Xl,Y3]), testl{[Xl,Y3],[X3,Y4}), ll([X3,Y4],[X2,Y2]). testl([Xl,Yl],[X2,Y2]) : -- X I =:=Y1, r e p e a a ( [ X l , y i ] , [ X 2 , r 2 ] ) . testl{[Xl,Yl],[Xl,Yl]) : -X 1 = : = Y 1 . r e p e a t l ( [ X l , y i ] , [ X 2 , y 2 ] ) : -asgn{[Xl, Y1], X3, XI + 3, [X3, Yl]), asgn([X3, Yl], Y3, X3 + 4, [ X 3 , y 3 ] ) , - X 3 =:= y 3 , r e p e a f l ( [ X 3 , y 3 ] , [ X 2 , y 2 ] ) . r e p e a < l ( [ X l , y i ] , [ X 3 , y 7 ] ) : -asgn([Xl,Yl],X3,Xl + 3 , [ X 3 , y i ] ) , asgn([X3, Y1], Y3, X3 + 4, [ X 3 , y 3]), X 3 =:= y 3 . Figure 4.13: Jumping into a repeat loop CHAPTER 4. A HORN CLAUSE SEMANTICS 45 progl([x,y},[]) : { x := x + 1; y.= y + 2; repeatl : repeat { x := x + 3; y := x + 4 } unii'Z (x =:= y); ll: y := x 4- 4; 1/ ( n l =:= y) { goto repeatl }; goto 11 } Figure 4.14: Bruce equivalent Chapter 5 A B r u c e - L o g i c T r a n s l a t i o n S y s t e m A Bruce -Log ic t ranslat ion system has been implemented in C P r o l o g [Pereira et al. 84]. T h i s system comprises the front-end (logic generator) and back-end (Bruce generator or Brucifier) of a Bruce transformation system discussed i n chapter 6. T h e complete source l i s t ing of the translat ion system can be found in the appendices. 5 . 1 T h e l o g i c g e n e r a t o r The logic generator reads a Bruce program and generates its logical equivalent. It operates i n three stages: 1. A Bruce program is read and parsed using a definite clause translation grammar ( D C T G ) [Abramson 84]. T h e n , an in i t i a l semantics is created directly from the parse tree of the D C T G . Th i s semantics is complete and adequate i n the case when no branching exists i n the program, pointedly i l lustrat ing the semantic clarity of structured, branchless programming. 2. Should branching be found in the program, label program definitions are created for al l the labelled code i n the program. 46 CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 47 chain ::= statAAS <:> code(Code,In,Out,Defns) :: — SAAicode(Code,In,Out,Defns). chain ::= statAAS, [';'], chainAAQ <:> code(Code,In,Out,Defns) ::— genjchain(Code, In, Out, Defns, S,Q). genjzhain{Code,In,Out,Defns,S,Q) : — SAAcode(Sl,In,X,Dl), QAAcode(S2,X, Out, D2), fuse((Sl,S2),Code), append(Dl, D2, De fns). Figure 5.1: Cha in rules 3. A g a i n , i n the case of branches, the semantics are restructured to reflect the effect of branches on program control . The rest of this section discusses these steps i n more detail . The creation of semantics for basic Bruce programs (section 4.2) is efficiently done through the use of a D C T G . The D C T G specifies how Bruce programs are to be parsed, and once parsed, how semantics are to be generated for the Bruce constructs. Each D C T G rule has associated wi th i t a syntactic component and a semantic component. T h e syntactic component contains a B N F - s t y l e grammar rule for a port ion of the Bruce syntax. The semantic component specifies actions which are to take place at the node of the parse tree associated w i t h that grammar rule. In our implementat ion, a semantic rule builds up a por t ion of the logical axiom associated wi th the context of the grammar rule i n question. T w o rules describing the composi t ion of chains are i n figure 5.1. Items wi th in braces are matched wi th strings i n the input , while stat and chain are references to grammar rules. T h e first rule parses single statement chains, and the second parses mul t ip le statement ones. In the case of single statement chains, the code is directly retrieved at the grammar CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 48 while ::= [while,1 ('], booLexpr^B, [')','{'], chain^Q, ['}'] <:> code(Code,In,Out,Defns) :: — genjwhilecode(Code,In, Out, Defns,B, Q, LoopJabel), addjcurrJabellist(while, Loop Jabel). Figure 5.2: Whi le- loop rule rule for that statement. In the mult iple-statement case, the semantic rule calls a Pro log predicate genjchain which obtains the code for the statement at node S i n the parse tree and adds i t to the code for the rest of the chain at node Q. Obta in ing the code for chain Q results i n a recursive invocat ion of the same grammar rule chain. A typ ica l D C T G rule which parses a statement is the one for while loops i n figure 5.2. T h e syntactic component uses the grammar rules booljexpr and chain. T h e argument Code for the semantic rule code returns the axioms created for the while loop , and the argument Defns returns axioms generated when parsing the loop body. T h e semantic rule uses a predicate genjwhilecode, which generates the predicative text of the ax iom for the loop. Other Bruce constructs are handled similarly. Some bookkeeping is done to ease recompilat ion of the semantics into Bruce later. P rogram parameters and variables are mapped to input-output vectors by their relative positions w i th in the vectors. Consequently, the parameter and variable names, as well as their relative ordering i n the program, are retained. In addi t ion, some features of the C P r o -log interpreter itself are exploited. It is convenient for Bruce to share the bu i l t i n ari thmetic and relat ional operators used by C P r o l o g , as this eases the evaluation of expressions later. T h e existence of a branch i n a Bruce program requires the generation of label predicates and the restructuring of the axioms. B o t h these operations use the existing axiom set during their processing, rather than operate on the original Bruce source program. Labe l predicate generation involves creating a predicate for each labelled statement i n the program. The definition of a label predicate is the predicative meaning of the code generated by the CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 49 prog([x,y],[]) : { repeat { while (x < 0) { x := x + 1; 11: y := x 4- 2 }; x := y- f -3 } uni t / (x =:= y); V := y + 4; jfoio / l ; y := y + 5 Figure 5.3: Branching in to two loops Buildenv function from Bruce's operational semantics. To derive these predicates from the exist ing axioms, conjunctions of goals which compose the control context of the labelled statement are collected. Col lect ing these goals requires traversing the axioms from the statement up through its parent mechanisms un t i l the top program ax iom is reached. T h e predicate generated is refined somewhat by using the fact that branches are semantically represented by label program calls, which can be treated as program continuations. T h e predicate can thus be terminated as soon as a branch is reached, since the continuation for the branch accounts for the rest of the computat ion. Figure 5.3 has a program which contains a branch into the middle of two nested loops. T h e semantics in i t ia l ly generated are i n figure 5.4. The program branch is represented by a goal goto(v{,ll,Vf), which is an "unprocessed" branch. The label ll is tagged by a goal label(ll) i n the first clause of whilel, which is removed after a label program predicate has been created for i t . The label program as denned by Buildenv for ll is i n figure 5.5, and the corresponding label program predicate is i n figure 5.6. The predicate is much more terse than the label program, since code i n the label program is logically described by exist ing predicates from the basic semantics. Note the addit ion of a predicate testl, which is used for describing the control which occurs when branching into the repeat loop. CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 50 prog([Xl,Yl],[X2,Y2]) : -repeatl([Xl,Yl], [ X 3 , 7 3 ] ) , asgn([XZ, 7 3 ] , 7 4 , 7 3 + 4, [ X 3 , 74 ] ) , 5 o i o ( [ X 3 , 7 4 ] , / l , [ X 2 , 7 5 ] ) , asgn{[X2, 7 5 ] , 7 2 , 7 5 + 5, [ X 2 , 72 ] ) . r e p e a * l ( [ X l , 7 l ] , [ X 2 , 7 2 ] ) w / u . e l ( [ X l , 7 l ] , [ X 3 , 7 3 ] ) , a s f f n ( [ X 3 , 7 3 ] , X 4 , 7 3 + 3, [ X 4 , 7 3 ] ) , ^ X 4 =:= 7 3 , r e p e a i l ( [ X 4 , 7 3 ] , [ X 2 , 7 2 ] ) . r e p e a * l ( [ X l , 7 l ] , [ X 2 , 7 2 ] ) : -w / w / e l ( [ X l , 7 l ] , [ X 3 , 7 2 ] ) , asgn([X3, Y2], X 4 , Y2 + 3, [ X 2 , 7 2 ] ) , X2 =:= Y2. whilel([Xl,Yl],[X2,Y2]) : -X I < 0, a s 5 n ( [ X l , 7 1 ] , X 3 , X l - f 1 , [ X 3 , 7 1 ] ) , label(ll), asgn([X3, YI], 7 3 , X 4 + 2, [ X 3 , 7 3 ] ) , w / u 7 e l ( [ X 3 , 7 3 ] , [ X 2 , 7 2 ] ) . w / n 7 e l ( [ X l , 7 l ] , [ X l , 7 l ] ) : -^ X l < 0. Figure 5.4: Basic semantics 5. A BRUCE-LOGIC TRANSLATION SYSTEM Buildenv(prog{...},ll : y := x + 2) <=> y := x + 2; while(x < 0) { x := x + 1; y : = x + 2 }; x := y + 3; if (-,(x =:= y)) { repeat { while (x < 0) { x := x 4-1; y := x + 2 };• x := y + 3 } until (x —.— y) } y := y + 4; (7o£o 11; y := y + 5 Figure 5.5: Labe l program « 1 ( [ X 1 , 7 1 ] , [ X 2 , 7 2 ] ) : -o s c / n ( [ X l , y 1], Y 3 , X I + 2, [ X I , Y 3 ] ) , u > / n 7 e l ( [ X l , Y 3 ] , [ X 3 , Y 4 ] ) , asgn([X3, 7 4 ] , X 4 , 7 4 + 3, [ X 4 , 7 4 ] ) , * e s f l ( [ X 4 , 7 4 ] , [ X 5 , 7 5 ] ) , asgn([X5,75], 7 6 , 7 5 + 4, [ X 5 , 7 6 ] ) , 5 0 f o ( [ X 5 , 7 6 ] , / l , [ X 2 , 7 2 ] ) . i e s i l ( [ X l , 7 l ] , [ X 2 , 7 2 ] ) : -^ X l =:= 7 1 , r e p e a * l ( [ X l , 7 l ] , [ X 2 , 7 2 ] ) . i e s f l ( [ X l , 7 l ] , [ X l , 7 1 ] ) : -X I =:= 7 1 . Figure 5.6: L a b e l program predicate CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 52 The branch restructuring algori thm is a refined version of the dis t r ibut ion procedure out l ined i n section 4.3. The process begins by searching for an instance of an unprocessed branch goal. W h e n such a goal is discovered, the goals following that goal are thrown away, and the goal is replaced by a label program cal l . Then the ancestor clauses of the predicate containing the branch are restructured. However, instead of d is t r ibut ing terms of the whole program predicate, only the clauses whose control is affected by a branch are inspected. In addi t ion, predicative formulas are retained where possible, in order to minimize textual changes to the semantics. The net effect of the restructuring is that every ax iom whose control is affected by the branch is altered as specified i n section 4.3. In terms of the program i n figure 5.3, the resulting branch restructuring i n figure 5.7 is not very interesting. The main program predicate has its branch goal replaced by a label program relation for ll, and the goal following i t has been lost. The branch i n the label program predicate has also been replaced. W h a t is of more interest is the program branch i n figure 5.8, whose basic semantics are i n figure 5.9. The restructured semantics i n figure 5.10 illustrates the effect of the single branch on the control of the two loops. These predicates are a derivation of the distr ibuted program predicate i n figure 5.11, i n which common terms have been factored out and assigned to existing predicate names. 5 . 2 T h e B r u c i f i e r C o m p i l i n g a logical representation back in to Bruce is the inverse of generating the logic from Bruce . Pa t te rn matching is performed on the axioms of a semantic representation to search for matches wi th logical definitions corresponding to Bruce constructs. T h e schema matching used when converting predicates into Bruce is basically a backwards interpre-tat ion of the basic semantics of figure 4.1 i n chapter 4. A measure of nondeterminism is encoded into the Brucifier in order to account for the fact that there is often more than one Bruce implementat ion derivable for a given set of axioms. This nondeterminism means CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 53 prog([Xl,Yl],[X2,Y2}) :-repeatl([Xl,Yl],[X3,Y3]), asgn([X3, Y3], Y4, Y3 + 4, [ X 3 , Y4\), ll([X3,Y4],[X2,Y2]). r e p e a f l ( [ X l , y i ] , [ X 2 , y 2 ] ) : -whilel([Xl,Yl],[X3,Y3]), asgn([X3, Y3], X 4 , Y3 + 3, [ X 4 , F 3 ] ) , ^ X 4 =:= Y3, repeatl([X4, Y3], [X2, Y2]). repeatl([Xl,Yl],[X2,Y2}) : -whilel([Xl,Yl],[X3,Y2]), asgn([X3,Y4],X2,Y2 + 3 , [ X 2 , y 2 ] ) , X 6 = : = Y2. whilel([Xl,Yl],[X2,Y2}) :-X I < 0, a 5 f f n ( [ X l , y i ] , X 3 , X l + l , [ X 3 , y i ] ) , asgn([X3, Yl], Y3, X 4 + 2, [X3,Y3]), w / i i ' / e l ( [ X 3 , y 3 ] , [ X 2 , y 2 ] ) . whilel([Xl,Yl],[Xl,Yl]) : --.XI < 0. / l ( [ X l , y i ] , [ X 2 , y 2 ] ) : -asgn([Xl,Yl], Y3,XI + 2, [X1,Y3]), u ; / i z / e l ( [ X l , y 3 ] , [ X 3 , y 4 ] ) , a ^ n ( [ X 3 , Y4], X4, Y4 + 3, [ X 4 , y 4 ] ) , f e5 f l ( [X4 ,y4 ] , [X5 ,y5 ] ) , asgn([X5, Y5], Y6, Y5 + 4, [ X 5 , Y6]), Z l ( [ X 5 , y 6 ] , [ X 2 , y 2 ] ) . f e s i l ( [ X l , y i ] , [ X 2 , y 2 ] ) : --nXl = : = y i , r e p e a i l ( [ X l , y i ] , [ X 2 , y 2 ] ) . testl([Xl,Yl],[Xl,Yl]) : -X I =:= Yl. Figure 5.7: F i n a l semantics CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 54 prog2([x,y],[]): { while (x > 0) { while (x < 0) { x := x + 1; c/ofo 12 }; x := 7/4-2 }; I2:y:= y + 3 Figure 5.8: Branch out of two loops p r o 5 2 ( [ X l , 7 1 ] , [ X 2 , 7 2 ] ) : -w / u / e 2 ( [ X l , 7 1 ] , [ X 2 , 7 3 ] ) , label(l2), asgn([X2,73], Y2,73 + 5, [X2,72]). w / ™ / e 2 ( [ X l , 7 l ] , [ X 2 , 7 2 ] ) : -X I > 0, w / u 7 e l ( [ X l , 7 1 ] , [ X 3 , 7 3 ] ) , a s 5 n ( [ X 3 , 7 3 ] , X 4 , 7 3 4- 3, [ X 4 , 7 3 ] ) , w / i z 7 e 2 ( [ X 4 , 7 3 ] , [ X 2 , 7 2 ] ) . w / n / e 2 ( [ X l , 7 l ] , [ X l , 7 1 ] ) : -- . X I > 0. w / u 7 e l ( [ X l , 7 1 ] , [ X 2 , 7 2 ] ) : -X I < 0, asgn([Xl, 7 1 ] , X 3 , X I + 1, [ X 3 , 7 1 ] ) , fifoto([X3,7l],Z2,[X4,73]), w / » / e l ( [ X 4 , 7 3 ] , [ X 2 , 7 2 ] ) . w / n 7 e l ( [ X l , 7 1 ] , [ X l , 7 1 ] ) : -- . X I < 0. Figure 5.9: Basic semantics CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 55 prog2([Xl,Yl],[X2,Y2]) : -i o / n 7 e 2 ( [ X l , 7 1 ] , [ X 2 , 7 2 ] ) . while2([Xl,Yl],[X2,Y2\) : -XI > 0, whilel([Xl,Yl],[X2,Y2]). while2([Xl,Yl],[Xl,Y2}) : -- . X I > 0, asgn([Xl, Y1], Y2, YI + 5, [ X I , 72 ] ) . w / i z Z e l ( [ X l , 7 l ] , [ X 2 , 7 2 ] ) : -X I < 0, asgn([Xl, Y1], X 3 , X I + 1, [ X 3 , 7 1 ] ) , / 2 ( [ X 3 , 7 1 ] , [ X 2 , 7 2 ] ) . w / « 7 e l ( [ X l , 7 1 ] , [ X 2 , 7 2 ] ) : -- . X I < 0, a s t / n ( [ X l , 7 l ] , X 3 , 7 1 + 3 , [ X 3 , 7 l ] ) , w / u 7 e 2 ( [ X 3 , 7 1 ] , [ X 2 , 7 2 ] ) . / 2 ( [ X 1 , 7 1 ] , [ X 1 , 7 2 ] ) : -asgn([Xl, 7 1 ] , 7 2 , 7 1 + 5, [ X I , 7 2 ] ) . Figure 5.10: F i n a l semantics prog2 ((x > 0) A (x < 0); x := x + 1 A /2(t>,-, vf)) V((x > 0) A -.(x < 0); x := y + 2; while(x > 0); 12 : y := y + 3) V(-.(x > 0) A 12 : y := y + 3) Figure 5.11: Dis t r ibuted program predicate CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 56 template jmatch(Progname, Vec, Prolog, [A, B],Bruce,Labels, Newlabels) : — isjajwhile(Progname, A, B,Test, Body), getJO(A,.,Out), template jrnatch.goals(Progname,Out, Prolog, Body, BruceJbody, Labels, Newlabels), append Jist([['whileC ,Test,')',' {'], Bruce J)ody, ['}']], Bruce). Figure 5.12: W h i l e loop matching that repeated calls to the Brucif ier for a given set of axioms may result i n different Bruce programs. There are two main matching modules used by the Brucifier. A module called tem-plate-match takes the axioms for a goal and matches them wi th the logical definitions of Bruce constructs. Such matching often requires the logical manipulat ion of predicates, for example, factoring out common terms and unfolding predicate definitions. T h i s module also assures that the Bruce statements generated for a list of goals are sequenced prop-erly. Depending on the nature of the transformations performed on the semantics, goals may have to be ordered w i t h respect to the data flow of their input -output vectors. A typica l matching rule is i n figure 5.12. T h e predicate isja-while succeeds i f clauses A and B represent an instance of a while loop. Body are the goals i n the loop's body, and are matched through use of the other matching module (called templatejmatch-goals i n our implementat ion) . W h e n this succeeds, the Bruce code defining this loop is constructed. T h e other module, templatejmatch.goals, is used for matching goals i n chains. After the goals are ordered, a Bruce construct is derived for each goal. Elementary relations such as assignments are converted directly in to Bruce at this stage. More complex mechanisms (those w i t h external definitions) are converted to Bruce by invoking template-match on the axioms defining the predicate to which the goal is referring. One peculiar i ty of our matching algori thm is that branches always refer to code which has been previously converted. In other words, the first branch i n a program w i l l be unfolded, and subsequent references to i t w i l l refer to this unfolded port ion of code. A CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM 57 prog([x,y],[]): { repeat { whilel : while (x < 0) { x := x + 1; y := x + 2 }; x := y + 3 } u n i i / (a; =:= y) ; y ••= y + 4; t/ := a; + 2; ^ofo whilel } Figure 5.13: Derived Bruce program consequence of this is that branches among statements i n a single chain tend to be unfolded, and might just disappear as a result. For an example of this phenomena, see the program i n figure 4.9 of section 4.6 Las t ly , the conversion of Bruce expressions, such as those i n assignments and boolean tests, requires the use of information about the names of variables and parameters and their relative ordering i n the input -output vectors. Th is information was saved during the parsing of the program. T h e Brucif ied results for the logic programs i n figures 5.7 and 5.10 are i n figures 5.13 and 5.14 respectively. CHAPTER 5. A BRUCE-LOGIC TRANSLATION SYSTEM prog2([x,y},[]): { while2 : if (x > 0) { if (x<0){ x := x + l ; y := y + 5 } e/se { x := y+ 3; <7oto while2 } } else { y y + 5 } } Figure 5.14: Derived Bruce program Chapter 6 T h e P a r t i a l E v a l u a t i o n o f B r u c e P r o g r a m s 6 . 1 P a r t i a l e v a l u a t i o n a n d p r o g r a m t r a n s f o r m a t i o n Once a program is translated in to its logical representation, many types of transformations are possible. Deduct ive transformations and term rewri t ing are two possibilities which would l ikely incorporate a mixture of heuristics and user control i n order to be pract ical . W e chose par t ia l evaluation as our program transformation scheme, as it is easily automated. The par t ia l evaluation of logic programs is also a logically sound transformation formalism, since the meta- interpretat ion of logic programs i n a par t ia l evaluation context is based on S L D N F resolution, which is sound. Th i s means that resulting transformed Bruce programs are correct. Mos t important ly , par t ia l evaluation most clearly illustrates the u t i l i ty of our H o r n clause semantics and its underlying execution model . Pa r t i a l evaluation is a computat ional model which distinguishes executable, permissible code from non-executable, suspendable code [Ershov 82] [Ershov 85]. In imperative pro-grams, permissible code is that which has a l l the necessary store values denned i n order to, for example, evaluate an expression or test. Suspendable code is that i n which a needed value is undefined. In a program transformation setting, input parameters to the program are usually fixed so that the par t ia l evaluator specializes the program wi th respect to that 59 CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 60 set of input . P a r t i a l evaluation then entails executing a l l permissible code, dur ing which a l l suspendable code is retained as a par t ia l ly evaluated program. T h i s residual program is an opt imized, transformed version of the original program. The fol lowing terminology and results are from [Lloyd etal. 87]. The par t ia l evalua-t ion of logic programs has been formally shown to be correct and complete, albeit under part icular conditions. A semantic theory composed i n our Horn clause semantics can be considered to be a definite logic program, since the negation operator used i n negated goals only operates on closed boolean expressions i n which resolution is never used; we could have used a weaker operator, but chose not to for convenience sake. Let P' be a par t ia l ly evaluated program wrt a source program P and goal G. P' is sound i f correct answers for P' and G are also correct for P and G. The par t ia l evaluation of our semantics is therefore sound, since the par t ia l evaluation of al l definite logic programs is sound. The par t ia l evaluation of definite programs is not necessarily complete. P' is complete i f correct answers for P and G are correct for P' and G. However, P' may be specialized wrt goal G, which means that some reference i n P' to a specialized clause of P may no longer be satisfiable. L loyd ' s method of ensuring completeness is to enforce a "closedness" condit ion on P'. Th is condit ion states that any predicate i n P' must remain general enough to satisfy a l l goals which refer to i t , which essentially inhibi ts the par t ia l evaluation from becoming too specialized. We mainta in completeness i n a different manner. G i v e n a program P , a general predicate h of P , and a goal G , we part ia l ly evaluate P wrt G to obtain a program P' containing a specialized predicate h'. Should references to h exist i n P ' which are too general for the specialized predicate h', we supplement P ' wi th h: P" = P ' U {h} W i t h respect to the theory Th(P) defined by the axioms for P , P ' being sound means that |= (Th(P') \= h Th(P) \= h) C H A P T E R 6. THE PARTIAL EVALUATION OF B R U C E PROGRAMS 61 However, P " s incompleteness implies \=-i(Th(P)\=h Th(P')[=h) T h e supplemented theory Th(P") is total ly correct: \=(Th(P)\=h o- Th(P")\=h) 6 . 2 I m p l e m e n t a t i o n W e transform Bruce programs by par t ia l ly evaluating the H o r n clause semantics for them. Once a Bruce program is translated into logic, its representation is asserted in to the Pro log environment, and the par t ia l evaluator is applied to i t wi th respect to given parameter settings. A residual program is eventually created. Should this program be incomplete, it is made complete by adding to i t required clauses from the original general program. T h e n , using predicative programming, the derived predicate is compiled back in to Bruce , resulting i n a transformed, opt imized Bruce program. O u r par t ia l evaluator takes the form of a meta-interpreter wri t ten i n C P r o l o g , and is based on implementations i n [Venken 85], [Takeuchi etal. 85], and [Pereira etal. 87]. The core of the evaluator is i n figure 6.1. T h e first clause of mix par t ia l ly evaluates conjunctions of goals, the results of which are combined together. Clause (2) executes goals which have been determined to be bu i l t in by the builtinjexecutable ut i l i ty. Examples of such goals are the boolean and relational operators used i n Bruce tests. Clause (4) solves goals by unifying a goal wi th a clause, and par t ia l ly evaluating the resulting body. CPro log ' s clause ut i l i ty automatical ly unifies the goal w i t h a clause each t ime clause succeeds. The most difficult problem faced when par t ia l ly evaluating a program is determining when to inh ib i t the par t ia l evaluation process. G o a l inhibi t ion is done i n clause (3) of mix by the inhibited u t i l i ty (see figure 6.2). Our system provides both automatic and user-controlled goal inh ib i t ion . B u i l t i n goals and subprogram calls are inhibi ted by the first two clauses of inhibited. Another automatic feature checks that the variables used i n CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 62 % ( l ) split multiple goals mix((Goal, Rest), Result,Recur) : — i mix(Goal, G Result, Recur), mix(Rest, RResult, Recur), fuse((G Result, RResult), Result). %(2) execute builtin's mix(Goal,true,J) : — builtin jexecutable(Goal), i Goal. %(3) halt interpretation mix (Goal, Goal, Recur) : — inhibited(Goal, Recur), \. %(4) interpret goal mix(Goal, Result, Recur) : — clause(Goal, Body), mix(Body, Result2, [Goal\Recur]), setjmixjresult(Result2, Result). Figure 6.1: Partial evaluator CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 63 %(1) builtin goals inhibited(Goal,_) :— builtin(Goal), %(2) subprogram calls inhibited(Goal,J) : — functor(Goal, Name, _), storematch(N ame, _, _, _, _), t. %(3) key variables are uninstantiated inhibited(Goal, _) : — not varJnst(Goal), j , %(4) loop detected inhibited(Goal, Recur) : — member3(Goal, Recur), I. %(5) no clause for goal inhibited(Goal, _) : — not clause(Goal,S), i Figure 6.2: Goal inhibition CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 64 a loop test are ground before that loop is unfolded (clause (3) of inhibited). W h e n a Bruce program is in i t i a l ly parsed, a record is kept of the variables used by the test expression of each if statement and loop. The par t ia l evaluator uses this information to inhibi t goals corresponding to these constructs should their test variables be uninstantiated. The fourth clause of inhibited checks for loops. F ina l ly , any goal which cannot be unified wi th a clause is inh ib i ted . In addi t ion to these five strategies, the user is allowed to enforce his or her own inh ib i t ion schemes s imply by asserting into Pro log their own inhibited clause. Th i s is v i t a l when the program contains complex looping mechanisms caused by the use of branches. It is also possible for the user to override any automatic inh ib i t ion strategy. 6.3 Example transformations Figure 6.3 has a Bruce program power which computes integral powers using a binary power a lgor i thm (from [Ershov 82]). The two varinst clauses, generated during parsing, are used to indicate to the par t ia l evaluator when to inhibi t the clauses corresponding to the two loops i n the program. B o t h clauses specify that the th i rd data object (the value parameter n) must be instantiated before part ia l ly evaluating the loops. W h e n power is par t ia l ly evaluated w i t h respect to n = 5, par t ia l execution yields the residual logic program and Bruce program i n figure 6.4. Note that a side effect of part ia l evaluation is that some vector values become ground. W h e n converting such a relation back into Bruce , the ground terms impl i c i t l y represent assignments of constants to variables. Par t i a l ly evaluating power w i th bo th x — 2 and n = 5 produces a program which simply sets the output parameter to the result (figure 6.5). A n example of code simplification is the binary gcd program of figure 6.6 (from [Knuth 81]). W e assert goal inh ib i t ion clauses specifying that u must be ground before the label pro-grams 61 and 62 are unfolded, and t must be ground before 64 is unfolded. Eva lua t ing the program wi th u = 7 results i n a residual program which is somewhat simpler than the or iginal , though not a great deal more efficient. The logical form of bingcd and its transformed equivalent can be found in appendices C and D respectively. CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 65 power([y],[x,n]) : { y:= 1; while (n > 0) { while (((n//2) * 2) = n := n / /2 ; x := x * x }; n := n — 1; y := y * a: } } := n ) { power([Yl,Xl,Nl],[Y2,Xl,Nl]) :-asgn([Yl,Xl,Nl],Y3,l,[Y2,Xl,Nl]), while2([Y3, XI, Nl], [Y2, X2, N2]). whilel([Yl,Xl,Nl],[Y2,X2,N2]) : -Nl/12*2=:= Nl, asgn([Yl,Xl,Nl],N3,Nl//2,[Yl,Xl,N3]), asgn([Yl,Xl,N4],X3,Xl*Xl,[Yl,X3,N3]), whilel{[Y I, X3, N3], [Y2, X2, N2]). whilel([Yl,Xl,Nl],[Yl,Xl,Nl}) :-- i V l / / 2 * 2 = : = Nl. while2([Yl,Xl,Nl],[Y2,X2,N2]) : -Nl > 0, whilel([Yl,Xl, Nl], [Y3, X3, N3]), asgn([Y3,X3,N3],N4, N3 - I, [Y3,X3,N4]), asgn([Y3,X3,N4],Y4, Y3 * X3, [Y4,X3,N4\), while2([Y4, X3, N4], [Y2, X2, N2]). while2([Yl,Xl,Nl],[Yl,Xl,Nl]) : --.JV1 > 0. varinst(whilel, [f, f, i]). varinst(while2, [f, f,i]). Figure 6.3: Binary powers power([Yl,Xl,5],[Y2,Xl,5]) : -asgn([l,Xl,4],Y3,l * X I , [ y 3 , X l , 4 ] ) , a 5 f f n ( [ y 3 , X l , 2 ] , X 2 , X l * X 1 , [ F 3 , X 2 , 2 ] ) , asgn([Y3,X2, l],X3,X2 * X2, [Y3,X3,1]), asgn([Y3, X 3 , 0 ] , Y2, Y4 * X 3 , [Y2, X3,0]) . power2([y],[x,n]): { 1 * x; x * x; y * x Figure 6.4: Residual programs (n = 5) power([yi,2,5],[32,2,5]). Figure 6.5: Residual programs (x = 2,n = 5) power3([y],[x,n]) : { y := 32 } CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 6 6 bingcd([gcd], [u,v]) : local [k,p,t]{ k := 0; 6 1 : i / ( ( ( « / / 2 ) * 2) = \ = « ) { goto 62 }; if (((v//2) * 2) = \ = u) { goto 62 }; k := k + 1; u := u / / 2 ; v := w / / 2 ; goto 61; 6 2 : * / ( ( ( « / / 2 ) * 2 ) = \ = « ) { t := 0 - v] goto 64 }; t := u ; 63 : i := t//2; 6 4 : *7(((t / / 2 )* 2) = : = * ) { 50/0 63 }; »7 (* > o) { u := t } e/se { •u := 0 - t }; t := u — v; i/(t = \ = 0 ) { <7o2o 63 }; ca// power([p], [2, A;]); gcd u*p } 6in£fcd([srcd], : /oca/ { t := 0 - v; u := 7; k := 0; i e s M : if (((t//2) * 2) =:= t) { 63 : * := * / / 2 ; goto testA } e/se { if (t > 0) { u := f } e/se { v := 0 - * }; t := u — v; if (* = \ = 0 ) { goto 63 } else { call power([p],[2, k]); gcd := u * p } } } Figure 6.6: B ina ry gcd (u = 7) CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS p{[y,z],[x,cl,c2]) : local [ r l , r 2 ]{ if {x>z){ rl := c l + l ; r2 := c l - 1 } else { rl := c2 - 1; 7-2 := c2 + 1 }; y:=y + r l ; z := z + r2 } Figure 6.7: A suspended test p ( [ 7 l , Z l , X l , 3 , 5 ] , [ 7 2 , Z 2 , X l , 3 , 5 ] ) : -^ X l > ZI, a s g n ( [ 7 l , Z l , X l , 3 , 5 , 4 , 6 ] , 7 2 , 7 l - f 4 , [ 7 2 , Z I , X I , 3 , 5 , 4 , 6 ] ) , asgn([Y2, ZI, XI, 3 ,5 ,4 ,6 ] , Z 2 , ZI + 6, [72 , Z2, XI, 3 ,5 ,4 ,6]) . p ( [ 7 l , Z l , X l , 3 , 5 ] , [ 7 2 , Z 2 , X l , 3 , 5 ] ) : -X I > ZI, a s 0 n ( [ 7 l , Z l , X l , 3 , 5 , 4 , 2 ] , 7 2 , 7 1 + 4, [72 , Z I , X I , 3 ,5 ,4 ,2]) , a 5 5 n ( [ 7 2 , Z l , X l , 3 , 5 , 4 , 2 ] , Z 2 , Z l + 2 , [ 7 2 , Z 2 , X l , 3 , 5 , 4 , 2 ] ) . Figure 6.8: Polyvariant logical result CHAPTER 6. THE PARTIAL EVALUATION OF BRUCE PROGRAMS 68 P2([y,z],[x,cl,c2]) : local [rl,r2] { if [x > z) { y:=y + 4; z := z + 2 } else { y:=y + 4; z := z + 6 } } Figure 6.9: Polyvariant Bruce result Logic elegantly handles polyvariant computational schemes, which are s imply those which entai l par t ia l ly evaluating the bodies of tests and loops whose tests have been sus-pended. In logic, this is natural ly handled by unfolding the suspended test's denning clauses, and retaining the suspended test expression as a goal. Figure 6.7 shows a Bruce program wi th a suspended test (assume x is undefined). Figure 6.9 shows the par t ia l ly evaluated logical result for c l = 3 and c2 = 5, and its Bruce realization is i n figure 6.3. Chapter 7 D i s c u s s i o n Comparisons are given between the work i n this thesis and related work. This is followed by a general discussion of the thesis, along wi th future research possibilities. 7 . 1 R e l a t e d w o r k T h e H o r n clause semantics we use is semantically founded on those given i n [Hehner 84a] and [Hehner etal. 86], which i n turn is similar i n spirit wi th logics used i n program ver-ification [Burs ta l l 69] [Floyd 67] [Hoare 69]. Hehner's semantics describe the behavior of most of Bruce - descriptions which we borrow, albeit i n a simplified and stylist ical ly altered form. We also extend the imperat ive constructs handled by including program branches and ca l l -by-va lue subprogram arguments. Since Hehner uses his logical semantics to study general characteristics of programs and computat ion, his semantics is much more descrip-tive than ours. His system has provisions for describing the evaluabil i ty of expressions, the terminat ion of mechanisms, and the type checking of data. Our semantics ignores such features, as we are concerned wi th the representation of correct and terminat ing programs which are to be transformed. He also employs full first-order predicate calculus in his se-mantics, whereas we use a subset of predicate calculus - H o r n clauses. A stylist ic difference between his system and ours is that he uses fairly informal naming schemes when describ-ing syntactic entities of a program, where we expl ic i t ly represent syntactic constructs w i th 69 CHAPTER 7. DISCUSSION 70 uniquely named predicates. Moss also uses Horn clause logic to semantically describe imperat ive programs [Moss 81] [Moss 82]. The description of a language i n his system takes the form of a sophisticated interpreter which fully describes the syntax and operational semantics of the language. T h e syntax is wr i t ten using a metamorphosis grammar, which is closely akin to the D C T G we use. His semantic rules, l ike ours, take the form of pure Pro log predicates. However, the nature of his semantics differs substantially from ours. Moss's semantic methodology is very robust, as his pr ime mot iva t ion is to describe the complete syntax and operational semantics of different programming languages using pure H o r n clause logic, thereby proving the u t i l i ty and generality of Prolog's descriptive capabilit ies. A theory i n his system is a set of axioms which fully describe the operational semantics of a language, and the domain of discourse of the theory is the universe of possible programs wri t ten i n the language. Programs are translated in to various first-order terms which take the form of convenient data structures. These terms are i n tu rn manipulated by predicates describing various functions of the operational semantics for the language. The domain of discourse of his logical axioms is thus programs and their abstract operational components. He essentially creates pure Pro log interpreters for languages. O u r semantics uses a lower level of abstraction than that of Moss , since a theory i n our system describes the computat ional behavior of a single imperat ive program. We use logical axioms to represent the functionali ty of the program's components, and reserve as our domain of discourse the domains of the store and expressions. The immediate advantage of such a low level description of computat ion is the abi l i ty of mapping, i n both directions, between the source language and logical representation. In addi t ion, the close relationship between the axioms and program means that optimizations of the axioms directly reflect improvements i n the corresponding imperat ive program. Cla rk and van E m d e n have used H o r n clause logic for verifying flowcharts, which can be interpreted as low level representations of imperative computations [Clark etal. 81]. They describe a flowchart's control i n terms of H o r n clauses, and then use a technique CHAPTER 7. DISCUSSION 71 called consequence verification to prove various properties of the computat ion. T h e style of their semantics is very similar to ours. The i r low level description of control relates to our semantics i n that uniquely named predicates represent unique computat ional mechar nisms. In addi t ion, they use logical variable renaming to describe updates to the store. However, their system is intended for use in program verification, so they make no attempt to associate their axioms wi th programming language constructs. O u r methodology for par t ia l ly evaluating imperat ive programs offers interesting com-parisons wi th work done by Ershov [Ershov 82] [Ershov 85]. Ershov par t ia l ly evaluates programs by symbolical ly executing them using an algebraic rewri t ing system. These rewri t ing rules are applied to the text of a program, and eventually yie ld a par t ia l ly eval-uated result. The meta- interpretat ion of our logical semantics very closely parallels the effects of his transformations. Analogies between the transformation system presented i n [Ershov 85] and S L D N F resolution of H o r n clause semantics are as follows: 1. Term reduction: Ershov reduces expressions by replacing a term by its domain value. In our system, this occurs when an asgn, callasgn or boolean test is resolved and the expression value obtained is carried forward i n the computation by the input -output vectors in relations. 2. Variable reduction: Ershov uses variable reduction to carry an assigned value of a variable to other statements using that variable. In our system, Prolog's unification automatical ly "passes" the value of a variable among goals i n a clause, and resolvents of a goal. 3. Assignment reduction: Ershov removes any assignment whose variable value has been distributed, throughout the code. Under S L D resolution, assignments (as wi th a l l goals) automatical ly "disappear" once they are resolved. 4. If and while loop reduction: These reductions are used to simulate the control of tests and loops. A g a i n , S L D resolution parallels these operations. CHAPTER 7. DISCUSSION 72 In fact, the traces of program transformations given by Ershov are very analogous to goal traces obtained when executing our semantics i n Pro log . We believe that our approach to the transformation of imperative programs has advan-tages over Ershov 's approach. The main strength of our formalism is that transformations performed on H o r n clause semantics have semantic interpretations i n logic. Performing program transformations i n logic means that the transformations can be verified for cor-rectness i n logic itself: any valid logical manipulation of the axioms is guaranteed of being a correctness-preserving program transformation. We exploit this fact i n this thesis by proving that our par t ia l evaluation of H o r n clause semantics is logically sound, since the par t ia l evaluation of logic programs can be considered a pure logical transformation scheme [Lloyd etal. 87]. O n the other hand, Ershov's transformation system does not have any strong formal semantic interpretat ion. Consequently, par t ia l evaluation i n his system is not formally proved to be correctness preserving. Our logical semantics offers a substantial improvement to previous techniques for poly-variant par t ia l evaluation, which entails part ia l ly evaluating the bodies of tests and loops whose tests have been suspended [Ershov 85] [Bulyonkov 84]. Previous handl ing of this has been by expl ic i t ly mainta ining memory states of alternate computations, which is required by the under lying algebraic transformation scheme. In logic, this is handled by s imply treating the test as a suspendable goal, which is retained dur ing the meta-interpretat ion process. Separate memory states are automatical ly retained during the evaluation of dif-ferent clauses, since memory states are expl ic i t ly stored as terms of the clauses. 7.2 Conclusions and further work W e have i l lustrated the appl icabi l i ty of H o r n clause logic as a tool for transforming imper-ative programs. We described the semantics of a nont r iv ia l imperative language using a relatively economical set of logical axioms. Us ing the predicative programming paradigm, direct t ranslat ion between semantical representations and the source language is possible. T h i s semantics is also ideally suited to many types of transformations, the one we presented CHAPTER 7. DISCUSSION 73 being par t ia l evaluation. O u r semantics are essentially a logical characterization of the operational semantics for Bruce . O u r approach to the design of the semantics was to first define Bruce i n terms of an abstract machine, and then create logical axioms for different Bruce constructs modelled on the behavior of Bruce 's operational semantics. Whether this intermediate abstract def-in i t ion of Bruce was t ru ly required is debatable, as the H o r n clause definition of constructs is just as intui t ive as the abstract operational definitions, i f not more so. T h e semantics are also abstract enough that machine-dependent features of the language are minimized , preventing i t from being as machine-oriented as other operational semantic systems. Our handl ing of branches i n Bruce uses both logical semantics and algebraic seman-tics. The logical semantics comes in to play during the in i t i a l expansion of the program predicate, since we use the basic axiomatic definitions of program constructs during the expansion process. Dis t r ibu t ing terms of the program predicate, as wel l as removing the control context of the branch, are essentially algebraic operations which are based on logi-cal considerations. O u r defense of this approach is that the formula of axiom derivation has become more complicated. W h e n no branches exist, the surface structure of program statements direct ly define the axioms. W i t h branches, we must use a more sophisticated inspection of the program syntax i n order to derive the axioms. One possible extension of this work is to enhance the semantics to handle more complex imperat ive languages. The inclusion of complex data types would be a relatively s t ra ight-forward extension, and would be especially useful given the preponderance of imperative programs using arrays and other data structures. A real test would be to derive a Horn clause semantics i n the style of this work for an existing programming language such as Pascal . W o r t h investigation is whether this style of logical semantics is applicable to other heterogeneous programming paradigms, such as functional programs. Such research would be i n effect searching for a general description of computat ion. It is l ikely that a more general semantics would have much more complex domains than that of ours, since other CHAPTER 7. DISCUSSION 74 programming paradigms treat programs as data much more easily than do imperat ive languages. Denotat ional semantics might therefore offer some insight into the semantic content of the domains of such a representation. In addi t ion, algebraic semantics might play a role i n denning a more generally applicable semantic formalism. M u c h of the textual processing which we do to our semantics, such as factoring, code dis t r ibut ing, and branch processing, are simple algebraic manipulations of the logical formulas. T h e manipulat ion of more complex semantic expressions might be more easily denned i n terms of algebraic rules. However, i t is advantageous to mainta in a logical basis to the methodology, as predicate logic permits meaningful interpretations and analysis of the domains being described. This thesis offers some philosophical views on the disciplines of programming and pro-gramming language design. A n immediate result of this work is that imperat ive pro-grams are easily described or simulated by logic programs. One might conjecture from this that logic programming subsumes imperat ive programming i n terms of computat ional power. Logic programs are certainly capable of computing any Tur ing-computable func-t ion [Tarnlund 77]. However, a logic program interpreted as a logical theory is governed by the same principles of undecidabi l i ty and effective computabi l i ty as its imperat ive brethren [Boolos et al. 80]. W e should instead surmise that logic programs subsume imperat ive ones i n terms of descriptive power, since the logic program interpretation of our semantics uses a relatively l imi ted subset of Prolog's full descriptive and computat ional capabilit ies. Prolog programs as wri t ten by Pro log programmers use much more complex unification schemes than those used i n our semantics. In addi t ion, "real" Pro log programs are often wri t ten nondeterminist ically, which means that arguments to predicates might be either input or output i n nature. O u r Horn clause semantics are str ict ly deterministic logic programs, being declarative descriptions of deterministic computations. Our semantics offers some insight into alternation trees and and/or models of program-ming [Harel 80]. In a logic programming context context, an alternation tree description of computat ion is just a restatement of the inherent logical semantics of pure Pro log program. Logic programs can be interpreted as and/or trees (or alternation trees), in which clauses CHAPTER 7. DISCUSSION 75 of a predicate represent or-branches, and the goals of a clause represent and-branches. The tree itself is composed of alternate instances of and-nodes and or-nodes (hence the term alternation tree) i n which and-nodes are the parents of or-nodes, and vice versa. A successful computat ion of the tree requires that a l l the and-nodes under an or-node must be successful before the or-node is successful; s imilar ly, at least one or-node under an crod-node must be successful before that and-node succeeds. Besides having theoretical importance i n the semantics of programming, the alternation tree interpretation of logic programs has applications i n parallel processing [Shapiro 87]. T h e parallel execution of an and/or tree means that the or-nodes and arid-nodes of the tree a l l take the form of producers and consumers of data. The data path between the nodes is dependent on the part icular variable usage i n the Pro log program. D a t a transfer between the nodes is done through the unification process. Cas t ing an imperat ive program into our Horn clause semantics means that an and/or model of computat ion is immediately defined for i t . A s wi th a l l pure logic programs, the alternation tree description of the H o r n clause semantics of a Bruce program allows the direct derivation of an and/or model of computat ion. In addi t ion, this al ternation tree gives an in i t i a l parallel execution model for the program. However, a data flow analysis of the tree would probably be needed i n order to derive an efficient model of parallel computat ion. Pa r t i a l evaluation is a scheme which transforms a general program into a more spe-cialized one. However, efficiency is gained at the expense of generality. The ideal goal of program transformation is to transform a program into a more efficient form without any loss of generality. Ex i s t ing systems which do such transformations are unfortunately not very automatable. Nevertheless, it would be interesting to use our semantics i n a more deductive transformational environment. It is l ikely that heuristics and user control would play a large role i n such a transformation system. Another interesting application of our semantics is its use i n a transformation system which transforms an input imperat ive pro-gram into a more "s tyl ized" version. A l s o worth attention is the use of our semantics i n a program verification system, which would again rely on heuristic and user control . CHAPTER 7. DISCUSSION 76 Further work i n controll ing the par t ia l evaluation of imperative programs is needed. In-h ib i t ing recursion on polyvariant computations is difficult to implement i n our system. Th i s can be overcome somewhat by par t ia l ly evaluating each clause i n the program predicate ind iv idua l ly . However, i t is not obvious how constant values can be elegantly propagated to these clauses using this scheme. Cont ro l l ing the par t ia l evaluation process seems to be a research topic problematic to the field of par t ia l evaluation i n general [Lloyd etal. 87]. Ershov expresses the need for a systems programming language ( S P L ) i n which program transformation could be based [Ershov 82]. We believe that our technique offers a more solid semantic foundation for program transformation than his algebraic transformations, and c la im that Horn clause logic using Prolog's execution model is a prime candidate for Ershov's S P L . F i r s t and foremost, pure Pro log has a well-founded underlying mathematical model , namely first-order predicate logic. Us ing logic immediately leads to the opportuni ty of using the many theoretical results, tools and techniques which have been established i n mathemat ica l logic throughout the years. In addi t ion, using the predicative programming paradigm, there is a strong and natura l relationship to the semantics of a language and its syntactic real izat ion. F ina l ly , Pro log has already proven its appl icabi l i ty i n many systems programming applications, for example, [Abramson etal. 88], [Moss 81], and [Shapiro 83]. R e f e r e n c e s [Abramson 84] H . Abramson . Definite Clause Transla t ion Grammars . In Proc. Logic Programming Symp., I E E E , A t l an t i c C i ty , New Jersey, Febru-ary 1984. [Abramson etal. 88] H . Abramson , M . Crocker , B . Ross, and D . Westcott . A F i f th Generat ion Translator W r i t i n g System: Towards an Exper t System for Compi le r Development. In Fifth Generation Comp. Sys. Conf., I F I P S , Tokyo, Japan, 1988. submit ted. [All ison 86] [Apt 81] [Ashcroft etal. 82] [Backus 78] [Beckman etal. 76] [Bibel 75] [Bibel 85] L l o y d A l l i s o n . A practical introduction to denotational semantics. Volume 23 of Cambridge Computer Science Texts, Cambridge U n i -versity Press, 1986. K . R . A p t . Ten years of Hoare's logic: a survey. TOPLAS, 3:431-483, 1981. E . A . Ashcroft and W . W . Wadge. R for Semantics. ACM Transac-tions on Programming Languages and Systems, 4(2):283-294, A p r i l 1982. John Backus. C a n Programming B e Liberated from the von New-mann Style? CACM, 21(8):613-641, August 1978. L . Beckman, A . Haraldson, O . Oskarsson, and E . Sandewall . A par-t i a l evaluator and its use as a programming tool . Artificial Intelli-gence, 7:319-357, 1976. W . B i b e l . Pradikatives programmieren. In GI - 2. Fachtagung uber Automatentheorie und Formale Sprachen, pages 274-283, Springer, 1975. W . B i b e l . Predicat ive programming revisited. In Mathemati-cal method of specification and synthesis of software systems '85, pages 25-40, Wendisch-Rei tz , E . Germany, A p r i l 1985. 77 REFERENCES 78 [Boolos et al. 80] [Boyer et al. 79] [Broy 84] [Bulyonkov 84] [Burstal l 69] [Clark etal. 81] [Clint etal. 72] [Clocksin etal. 81] [Cook 78] [Darlington etal. 73] [de B r u i n 81] [Ershov 82] [Ershov 85] [Floyd 67] George Boolos and Richard Jeffrey. Computability and Logic. Cam-bridge Univers i ty Press, 1980. R . S . Boyer and J .S . Moore . A Computational Logic. ACM Mono-graph Series, Academic Press, 1979. Manfred Broy . Algebraic Methods for P rogram Construct ion: The Project C I P . In P . Pepper, editor, Program Transformation and Programming Environments, pages 199-222, Springer-Verlag, 1984. M . A . Bulyonkov . Polyvariant M i x e d Computa t ion for Analyzer Pro-grams. Acta Informatica, 21:473-484, 1984. R . M . Bur s t a l l . Fo rmal Descript ion of P rogram Structure and Se-mantics i n F i rs t Order Logic . In Mich ie Mel tzer , editor, Machine Intelligence 5, pages 79-98, Elsevier , 1969. K . L . C la rk and M . H . van Emden . Consequence Verification of Flowcharts . IEEE Transactions on Software Engineering, S E -7( l ) :52-60, January 1981. M . C l i n t and C . A . R . Hoare. P rogramming Prov ing : Jumps and Functions. Acta Informatica, 1:214-224, 1972. W . F . C locks in and C S . Me l l i sh . Programming in Prolog. Springer-Ver lag , 1981. S . A . Cook . Soundness and completeness of an axiom system for program verification. SI AM Journal of Computing, 7( l ) :70-90,1978. J . Dar l ing ton and R . M . Burs t a l l . A System which Automat ica l ly Improves Programs. In IJCAI, pages 479-485, X X X , 1973. A . de B r u i n . Goto Statements: Semantics and Deduct ion Systems. Acta Informatica, 15:385-424, 1981. A n d r e i P . Ershov. M i x e d Computa t ion : Potent ia l Appl ica t ions and Problems for Study. Theoretical Computer Science 18, 18:41-67, 1982. A n d r e i P . Ershov. O n M i x e d Computa t ion : Informal Account of the Strict and Polyvariant Computa t iona l Schemes. In M . Broy, editor, Control Flow and Data Flow: Concepts of Distributed Programming, pages 107-120, Springer-Verlag, 1985. R . W . F l o y d . Ass igning Meanings to Programs. In Proc. Symp. Appl. Math., pages 19-32, A m e r . M a t h . S o c , 1967. REFERENCES 79 [Futamura 71] [Gordon 79] [Guessarian 81] [Harel 80] [Hehner 84a] [Hehner 84b] [Hehner et al. 86] [Hoare 69] [Hoare 85] [Hoare etal. 73] [Jones etal. 85] [Kernighan etal. 78] [Knu th 81] [Lloyd 84] [Lloyd et al. 87] Y . Fu tamura . P a r t i a l evaluation of computation process - an ap-proach to a compiler-compiler. Systems - Comput. - Controls, 2(5):45-50, 1971. M . Gordon . The Denotational Description of Programming Lan-guages. Springer-Verlag, New York , 1979. Irene Guessarian. Algebraic Semantics. Vo lume 99 of Lecture Notes in Computer Science, Springer-Verlag, 1981. D a v i d Hare l . A n s / O r Programs: A New Approach to Structured Programming . ACM Transactions on Programming Languages and Systems, 2 ( l ) : l - 1 7 , January 1980. E r i c C . R . Hehner. Predicat ive Programming Pa r t I. 27(2):134-143, February 1984. CACM, Er i c C . R . Hehner. Predicative Programming Par t II. CACM, 27(2), February 1984. E r i c C . R . Hehner, Lorene E . G u p t a , and A n d r e w J . M a l t o n . Pred-icat ive Methodology. Acta Informatica, 23:487-505, 1986. C . A . R . Hoare. A n A x i o m a t i c Basis for Computer Programming. CACM, 12(10):576-583, October 1969. C . A . R . Hoare. Programs are Predicates. In C . A . R . Hoare and J . C . Shepherdson, editors, Mathematical Logic and Programming Lan-guages, pages 141-155, Prent ice-Hal l , 1985. C . A . R . Hoare and N . W i r t h . A n axiomatic definition of the pro-gramming language P A S C A L . Acta Informatica, 2:335-355, 1973. N . D . Jones, P . Sestoft, and H . Sondergaard. A n Exper iment i n Par-t ia l Eva lua t ion : the Generation of a Compi ler Generator. SIGPLAN Notices, 20(8):82-87, August 1985. B . W . Kern ighan and D . M . Ri tchie . The C Programming Language. Prent ice-Hal l , 1978. Dona ld E . K n u t h . Seminumerical Algorithms. Volume 2 of The Art of Computer Programming, Addison-Wesley, 2nd edit ion, 1981. J . W . L l o y d . Foundations of Logic Programming. Springer-Verlag, 1984. J . W . L l o y d and J . C . Shepherdson. Partial Evaluation in Logic Pro-gramming. Technical Report CS-87-09, Universi ty of Br i s to l , Decem-ber 1987. REFERENCES 80 [Loeckx etal. 84] [Loveman 77] [Manna etal. 77] [Moss 81] [Moss 82] [O'DonneU 82] [Partsch et al. 83] [Pepper 84] [Pereira etal. 84] [Pereira etal. 87] [Robinson 65] [Shapiro 83] [Shapiro 87] [Stoy 77] [Takeuchi etal. 85] J . Loeckx and K . Sieber. The Foundations of Program Verification. Wiley-Teubner , 1984. D . B . Loveman. P rogram Improvement by Source-to-Source Trans-formation. JACM, 24(1):121-145, January 1977. Zohar M a n n a and Richard Waldinger . Studies in Automatic Pro-gramming Logic. Elsevier Nor th -Hol land , 1977. Christopher D . S . Moss. The Formal Description of Programming Languages using Predicate Logic. P h D thesis, Imperial College, L o n -don, U . K . , J u l y 1981. Christopher D . S . Moss. How to Define a Language Us ing Pro log . In Conference Record of the 1982 ACM Symposium on Lisp and Func-tional Programming, pages 67-73, A C M , 1982. M . J . O 'DonneU. A Cri t ique of the Foundations of Hoare Style Pro-gramming Logics. CACM, 25(12):927-935, December 1982. H . Partsch and R . Steinbruggen. Program Transformation Systems. Computing Surveys, 15(3):199-236, September 1983. P . Pepper, editor. Program Transformation and Programming Envi-ronments. Springer-Verlag, 1984. F . Pereira, D . Warren , D . Bowen, and L . Pereira. C-Prolog User's Manual, version 1.5 edit ion, November 1984. Fernando C . N . Pereira and Stuart M . Shieber. Prolog and Natural-Language Analysis. Volume 10 of CSLI Lecture Notes, C S L I , 1987. J . A . Robinson. A Machine-Oriented Logic Based on the Resolut ion Pr inc ip le . JACM, 12(1):23-41, January 1965. E . Y . Shapiro. Systems Programming in Concurrent Prolog. Techni-cal Report T R - 0 3 4 , I C O T , Tokyo, Japan, November 1983. E h u d Shapiro. Concurrent Prolog vol. 1 and 2. M I T Press, 1987. J . Stoy. Denotational Semantics. M I T Press, 1977. A . Takeuchi and K . Furukawa. Partial Evaluation of Prolog Pro-grams and its Application to Meta Programming. Technical Re-port T R - 1 2 6 , I C O T , Tokyo, Japan, Ju ly 1985. [Tarnlund 77] S. Ta rn lund . H o r n Clause Computab i l i ty . BIT, 17:215-226, 1977. REFERENCES 81 [Tennent 77] R . D . Tennent. Language Design methods Based on Semantic P r i n -ciples. Acta Informatica, 8:97-112, 1977. [Tennent 81] R . D . Tennent. Principles of Programming Languages. Prent ice-Hal l , 1981. [van E m d e n etal. 76] M . H . van Emden and R . A . K o w a l s k i . The Semantics of Predicate Logic as a Programming Language. JACM, 23(4):733-742, October 1976. [Venken 85] R a f Venken. A Prolog Meta-Interpreter for Pa r t i a l Evalua t ion and its App l i ca t i on to Source to Source Transformation and Query Op-t imisat ion. In T .O 'Shea , editor, Advances in Artificial Intelligence, pages 347-356, Elsevier Science Publishers B . V . (Nor th Hol land) , 1985. [Wir th etal. 78] Niklaus W i r t h and Kath leen Jensen. Pascal User Manual and Re-port. Springer-Verlag, 2d edi t ion, 1978. A p p e n d i x A Partial Evaluator Source % *** % *** Mixed Computation routines % *** % *** - Brian J. Ross % *** Dept. of Computer Science % *** University of British Columbia % *** % % mix(Goal,Mixed): % Goal — top goal to mix (with parameter settings) % Mixed — Mixed Prolog result % % mix/2 finds the Prolog result, given a top level goal. % A Prolog program must be asserted in the Prolog environment before this % routine can run. The steps taken are: % 1. Find the mixed result using topjnixer % 2. Clean up the result from topjnixer. % 3. Add Prolog predicates to make the resulting program complete. mix(Goal,Mixed) : — setof( Results,Goal" top_mixer(Goal,Results),P), add_old_prolog(P,Mixed), % % top_mixer(Goal,Result): 82 APPENDIX A. PARTIAL EVALUATOR SOURCE % Goal — top goal to mix % Result — resulting mixed Prolog program % % topjnixer drive the mixed computation. top_mixer(Goal,Result) :— clause(Goal ,Body) , mix(Body,Resul t2 , [Goal] ) , set_mix_result (Result2 ,Result 3), set_mix_ans( Goal ,Resul t3 ,Resul t ) . % % set_mix_ans(A,B,C): % A — Goal which has been mixed % B — mixed result % C —the form of the result to be passed back to calling program % % set_mix_ans simply formats the result of the mixed computation % the form of a Prolog program. set_mix_ans(Goal,true,Goal) :— !. set_mix_ans(Goal,(_:—true),Goal) :— !. set_mix_ans(Goal,A,(Goal:—A)) :— !. % % mix(Goals,Result,Recur): % Goals — Goals to be mixed % Result — Mixed result % Recur — recursion list % % mix/ 5 is the core of the mixed computation utility. % It is a meta—interpreter which executes the Goals under the current Prolog % environment. The algorithm used simply tries to solve the Goals, halting % further interpretation when Goal inhibition conditions are satisfied: % 1. The goal is a builtin predicate, but it has uninstantiated % variables which prevent it from being executed. % 2. The goal has uninstantiated variables which must be % instantiated according to the 'var_inst' clause. % 3. The goal occurs in the recursion list — a loop las been detected. % 4- No clause exists for solving the goal. % Whenever one of these conditions arise, the goal is saved as a mixed result. APPENDIX A. PARTIAL EVALUATOR SOURCE 84 mix((Goal,Rest),Result,Recur) :— I •> mix(Goal,GResult,Recur), mix(Rest,RResult,Recur), fuse((GResult,RResult),Result). mix(Goal,true,_) :— builtin_execut able( Goal), I Goal. % split multiple goals % execute builtin's mix(Goal,Goal,Recur) :— inhibited(Goal,Recur), % halt interpretation mix(Goal,Result,Recur) :— clause(Goal,Body), mix(Body,Result2,[Goal|Recur]), set_mix_result (Result2,Result). % interpret goal % % set_mix_result(A,B): % A — Mixed result % B — returned result % % setjnixjresult reformats the mixed result. set_mix_result((_:—A),A) :— !. set_mix_result(A,A) :— !. % % inhibited(Goal,Recur): % Goal — current Goal being interpreted % Recur — Current recursion list % % inhibited checks if any Goal inhibition condition exists. mhibited(Goal%_) : - builtm(Goal),! inhibited(Goal^) :— functor(Goal,Name,_), storematch(Name,_,_,_,_), APPENDIX A. PARTIAL EVALUATOR SOURCE inhibited(Goal,_) :— not var jns t (Goal) , ! . inh ib i ted(Goal ,Recur) :— member3(Goal,Recur),!. inh ib i t ed (Goa l^ ) :— not clause(Goal,_),!. % : % unknown_vars(Goal): % Goal — current goal being interpreted % % unknownjvars checks if the builtin Goal has any uninstantiated variables % as part of its executable structure (tests, expressions). unknown_vars(asgn(_,_,E,_)) :— i •> extract va r s (E ,F ) , F \ = = []. unknown_vars(callasgn(_,_,E)) :— i extract va r s (E ,F ) , F \ = = []. unknown_vars(Test) :— is_a_test(Test), i •i extract vars(Test ,F) , F \ = = " []. % % executable_builtin tests if a goal is builtin and executable. % This may be specialized for individual builtin utilities in the future. built in_executable(Goal) :— bui l t in (Goa l ) , not unknownva r s (Goa l ) , I. % % builtin goal list: buil t in( t rue) : - !. bui l t in (asgn(_ ,_^J) : - !. builtin(callasgn(_,_,_)) : - !. bui l t in(Test ) : - is_a_test(Test), !. APPENDIX A. PARTIAL EVALUATOR SOURCE % % varJnst(Goal): % Goal — current goal being interpreted % % var_inst takes Goal and compares its input vector with the variable % instantiation flag settings in the Goal's corresponding var_inst clause. % Each variable in the input vector corresponding to a "i" (instantiated) % setting must be an instantiated/ground variable; else failure. varJns t (Goa l ) :— G o a l =. . [Name,Vec | J , var_inst(Name,Inst), i •> var_inst2(Vec,Inst). var_inst(_). var_inst2([],Q). var_inst2([_|R],[f|S]) : -i var_inst2(R,S). var_inst2([V|R],[i|S]) : -i nonvar (V) , var_inst2(R,S). % : % add_old_prolog(Mixed,New): % Mixed — mixed Prolog program % New — Mixed with added Prolog to make it complete % % addjoldjprolog/ 2 completes the mixed prolog program. add_old_prolog(Mixed,New) : -add_old_prolog(Mixed,Mixed,[],New). % % add_old_prolog(Mixed, Clauses,Done,Ans): % Mixed — Mixed result so far % Clauses — clauses yet to check for completeness % Done — names of predicates completed so far % Ans — final result APPENDIX A. PARTIAL EVALUATOR SOURCE % % add_old_prolog/4 adds to the current Prolog program in Mixed clauses from % the Prolog environment to make it complete. It calls add_old_prolog2 on the % list of goals in each clause of Clause, until all of Clause has been % processed. The names of the predicates completed are stored in Done. add_old_prolog(Mixed,[],_,Mixed). add_old_prolog(Mixed,[A|R],Done,S) :— spli t_clause(A ,u ,Goals) , add_old_prolog2(Mixed,Goals,Done,Done2,More), M i x e d \ = = M o r e , add_old_prolog(More,More,Done2,S). add_old_prolog(Mixed, [A | R] ,Done,S) :— add_old_prolog( M i x e d ,R,Done,S) . % ; % add_old_prolog2(Mixed, Goals, OldDone,NewDone,Ans): % Mixed — Current mixed program % Goals — goal list to process % OldDone — predicates processed so far % NewDone — all the predicates processed after Goals processed % Ans — final result % % add_old_prolog2 completes the Prolog program Mixed with respect to the % goal list Goals. Should a partially ground goal not have a corresponding % partially ground header in Mixed, the general predicate is copied from % the Prolog environment and added to Mixed. The name of the predicate is % saved to avoid duplication later. add_old_prolog2(Mixed,0,Done,Done,Mixed). add_old_prolog2(Mixed,[Goal |Rest],Done,Done2,More) :— not bu i l t in (Goa l ) , functor(Goal,Name,_), member(Name,Done) , i add_old_prolog2(Mixed,Rest ,Done,Done2,More). add_old_prolog2(Mixed,[Goal |Rest],Done,Done2,More) :— not bu i l t in (Goa l ) , APPENDIX A. PARTIAL EVALUATOR SOURCE 88 not head_exists(Goal,Mixed), i •> setof( Clause ,get_clause(Goal,Clause),More2), append(Mixed ,More2 ,More3) , functor(Goal,Name,_), add_old_prolog2(More3,Rest,[Name|Done],Done2,More). add_old_prolog2(Mixed,[_|Rest],Done,Done2,More) :— add_old_prolog2(Mixed,Rest,Done,Done2,More). % \ % get_clause(Goal,Clause): % Goal — (possibly partially) ground goal % Clause — a general clause matching Head % % get_clause retrieves a clause to solve Head without unifying anything in % Head. get_clause(Goal,(Template:—Body)) :— func tor (Goa l ,Name,Ar i ty ) , current_predicat e( Name ,Template), functor(Template ,Name,Ari ty) , c lause(Template,Body). % % head_exists(Goal,Clauses): % Goal — partially ground goal % Clauses — Prolog clauses % % head_exists tests if a clause with a partially ground head corresponding to % Head exists in Clauses. head_exists(Goal , [(H:-B) |Rest]) : -ground_eq( G o a l , H ) . head_exists(Goal,[_|Rest]) :— head_exists(Goal,Rest). Appendix B B r u c e P a r s e r % *** % *** Bruce parser and predicate generator % *** % *** _ Brian J. Ross % *** Dept. of Computer Science % *** University of British Columbia % *** % % This DCTG grammar contains the Bruce syntax. % (BRUCE: Brian Ross's Unfriendly Computation Environment) % The semantic portions allow compilation of a Prolog equivalent for the % Bruce program being parsed. % This grammar expects a list of lexical tokens, as is generated by Westcott's % lexical analyzer. % % The semantics produce a list whose elements are Prolog clauses. % The usual structures being passed through the semantics are: % Code — the code for this construct % In — the initial variable vector % Out — the output variable vector % Defns — list of Prolog code created through the parsing of a construct % Extra arguments are described where appropriate. env ::= prog""P, env"E <:> code(Code) ::— 89 APPENDIX B. BRUCE PARSER P"*code(C), E""code(Defns), append(C,Defns,Code). env ::= Q <:> code([]). prog ::= prog_header""P, ['{'], chain""Q, ['}'] <:> code(Code) ::— gen_prog(Code,P,Q). progjieader ::= label""!, ['('], var_list""V, [','], var_list""E, [')',':'], decls""D <:> code(P,VI,EI,Locals,Evars,In,Out) : : -gen_headercode(P,VI,EI,Locals,In,Out,Evars,L,V,E,D,Proglabel), newJabellist(Proglabel). decls ::= [' local'] , var_list*"L <:> code(Code) ::— L""code(Code). decls ::= [] <:> code(Q). chain ::= stat""S, [';'], chain""Q <:> code(Code,In,Out,Defns) ::— gen_chain(Code,In,Out,Defns,S,Q). chain ::= stat""S <:> code(Code,In,Out,Defns) : : - S""code(Code,In,Out,Defns). chain ::= label"*L, [':'], stat""S, [';'], chain""Q <:> code((label(Label),Code),In,Out,Defns) ::— gen_chain(Code,In,Out,Defns,S,Q), L" "code(Label), APPENDIX B. BRUCE PARSER add_curr_labellist(label,Label). chain ::= l abe l**L , [ ' : ' ] , stat"*S <:> code((label(Label) ,Code),In,Out,Defns) : : -S* "code(Code,In,Out,Defns), L " "code(Label) , add_curr_labellist(label,Label). % % The following are calls to the statement constructs stat ::= test""S <:> code(Code,In,Out,Defns) ::— S" *code(Code,In,Out,Defns). stat ::= proc_cair*S <:> code(Code,In,Out,Defns) ::— S""code(Code,In,Out,Defns). stat ::= while* "S <:> code(Code,In,Out,Defns) : : - S""code(Code,In,Out,Defns). stat ::= repeat" *S <:> code(Code,In,Out,Defns) ::— S" A code(Code,In,Out,Defns) . stat ::= branch" "S <:> code(Code,In,Out,Defns) ::— S" "code(Code,In,Out,Defns). stat ::= skip**S <:> code(Code,In,Out,Defns) ::— S"*code(Code,In,Out,Defns). stat ::= ass ignment* A A <:> code(Code,In,Out,Defns) : : - A**code(Code,In,Out ,Defns) . % % The following are rules which create Prolog construct. APPENDIX B. BRUCE PARSER 92 skip ::= [skip] <:> code(skip(In,In),In,In,[]). assignment ::= l a b e r * V , [ ' : = ' ] , any_expr"*E <:> code(Code,In,Out,Defns) ::— gen_asgn(Code,In,Out,Defns,V,E). test ::= [ ' i f ' , ' ( ' ] , bool_expr" " B , c h a i n * " Q l , [ ' } ' ] , [else,'-C»], chain**Q2, [ ' } ' ] <:> code(Code,In,Out,Defns) ::— gen_testcode(Code,In,0ut,Defns,B,Ql,Q2,If_label) , add_curr_labellist(if,If_label). test ::= ['if,'('], bool_expr""B, [ ' ) ' , ' { ' ] , c h a i n " " Q l , [ ' } ' ] <:> code(Code,In,Out,Defns) ::— gen_tes tcode(Code,In ,Out ,Defns ,B)Ql) ' ' ,H_label), add_curr_labellist(if,If_label). proc_call ::= [call], l abe l "*P , [ ' ( ' ] , vax_l is t""V, [ ' , ' ] , expr_outputs**E,[ ' ) ' ] <:> code(Code,In,Out,Q) ::— gen_cal lcode(Code,In ,Out ,P ,V,E) . while ::= [ w h i l e , ' ( ' ] , bool_expr*"B, [ ' ) ' , ' { ' ] , cha in*"Q, [ ' } ' ] <:> code(Code,In,Out,Defns) ::— gen_whilecode(Code,In,Out,Defns,B,Q,Loop_label) , add_curr_labellist(while,Loop_label). repeat ::= [ repea t , ' { ' ] , cha in"*Q, [ ' } ' , u n t i l , ' ( ' ] , bool_expr""B, [ ' ) ' ] <:> code(Code,In,Out,Defns) ::— gen_repeatcode(Code,In,Out,Defns,B,Q,Loop_label), add_curr_labellist(repeat,Loop_label). branch ::= [goto], l a b e l " " L <:> APPENDIX B. BRUCE PARSER code(Code,In,Out,[]) ::— gen_goto(Code,In,Out,L), goto_found. % % Some miscellaneous expression rules ... label ::= [id(Name)] <:> code(Name). any_expr ::= e x p r " " E <:> code(Expr,In) : : - E*"code(Expr , In) . any_expr ::= bool_expr""B <:> code(Expr,In) ::— B""code(Expr , In ) . bool_expr ::= [true] <:> code(true,_). bool_expr ::= [false] <:> code(false,_). bool_expr ::= label" " V <:> code(Code,In) : : - V""code(Name),var_match(Name,In,Code). bool_expr ::= [ ' ( ' ] , any_expr""A, r e l o p " " B , any_expr*"C, [ ' ) ' ] < : > code((E),In) : : - A " " c o d e ( E l , I n ) , B""code (E2) , C " "code(E3,In), E =. . [E2,E1,E3] . bool .expr ::= [ ' ( ' ] , bool_expr""A, b inbool_op""B, bool_expr""C, <:> code((E),In) : : - A " " c o d e ( E l , I n ) , B""code (E2) , C""code(E3,In) , E =.. [E2,E1,E3] . bool_expr ::= [ ' ( ' , ' " ' ] , bool_expr""A, [ ' ) ' ] APPENDIX B. BRUCE PARSER 94 <:> code("(E),In) : : - A~code(E,In). expr ::= ['('], expr" "A, math_op""B, expr""C, [')'] <:> code((E),In) : : - A""code(El,In), B""code(E2), C" "code(E3,In), E =.. [E2,E1,E3]. % E2 should be defined as a CProlog operator expr ::= [const(Num)] <:> code(Num,_). expr ::= label* "V <:> code(Code,In) ::- V*"code(Name),var_match(Name,In,Code). binbool_op ::= [bool(C)] <:> code(C). relop ::= [rel(C)] <:> code(C). mathpp ::= [math(C)] <:> code(C). % % Lists... % A list of variable labels ... varjist ::= ['['], labeljist""V, [»]'] <:> code(Code) ::— V" "code(Code). % A list of expressions, with appropriate logical variable substitutions... expr_outputs ::= ['['], exprjist""V, [']'] <:> code(Code,In) : : - V""code(Code,In). APPENDIX B. BRUCE PARSER 95 % Generates a label list... l abe l j i s t ::= label* " L , [ ' , ' ] , l a b e l j i s t " " V <:> code([Label|Labels]) : : - L**code(Label) , V"*code(Labels ) . l abe l j i s t ::= label* *L <:> code([Label]) ::— L * *code(Label). l abe l j i s t ::= [] <:> code([]). % Generates an expression list ... expr j i s t ::= e x p r " " E , [ ' , ' ] , expr_l is t""L <:> code(Code,In) ::— E""code(Expr , In ) , L * *code(Elist ,In), append( [Expr] ,El is t ,Code). expr j i s t ::= bool_expr""B, [ ' , ' ] , e x p r j i s t " " L <:> code(Code,In) ::— B " *code(Expr,In) , L""code(El i s t , In ) , append( [Expr] ,E l i s t ,Code) . expr j i s t ::= e x p r " " E <:> code([Code],In) : : - E " *code(Code,In). exp r j i s t ::= bool_expr""B <:> code([Code],In) ::— B""code(Code, In) . expr j i s t ::= [] <:> code( [],_). APPENDIX B. BRUCE PARSER % % Some semantic primitives % asgn(In,Var,Expr,Out) is satisfied by evaluating Expr and saving the value % in logical variable Var, where In contains input values which may be % needed by Expr, and Out is the final output value (variant with logical % variable Var changed). asgn(In ,Var ,Expr ,Out ) :— va lue(Expr ,Var ) . % callasgn(In, Var,Expr) evaluates Expr, saving the value in Var. % The In vector is not directly used. % This is needed to pass expression values in procedure calls. cal lasgn(In,Var ,Expr) :— va lue(Expr ,Var ) . % skip always succeeds. skip(_,_). skip_branch(_,Dest,_) : - w r i t e l ( n l , ' I g n o r i n g b r a n c h t o ' ,Des t ,n l ) . % label inserts do nothing... l a b e l f j . % % Prolog code construction ... % These routines construct Prolog code for the particular constructs % in question. In doing so, they may call semantic portions of the % tree. The code from these calls, if any, is passed back in Defns. % % gen_prog(Code,P,Q): % P — points to header portion of tree % Q — points to main program chain % % Returns in list Code: % p(In,Out) :— Body PLUS definitions for rest of program APPENDIX B. BRUCE PARSER 97 gen_prog(Code,P,Q) : -P"code(Header,VJnp,Ejnp,Locals,Evars,In,Out), Q-*code(Body,In,02,Defns), gen_vec( V_inp ,X 1), append(Xl,Evars,Out), append(Xl,_,02), Pgm =.. [(:-),Header,Body], append([Pgm],Defns,Code). % % genjieadercode (Code, VI, EI, Locals, In, Out, Evars, L, V, E, D, Prog): % Asserts storematch(Prog)B,VI)EI,LOC) % where Prog — program name, % B — label list of var params, val params, and locals resp. % VI — label list of var params % EI — label list of val params % Locals — label list of locals gen_headercode(Code,VI,EI,Locals,In,Out,Evars,L,V,E,D,Prog) :— I/"code(Prog), V"code(VI), E~code(EI), Dcode(Locais), append_list([VI,EI,Locals] ,Varnames), gen_vec( VI ,1 vars), gen_vec(EI,Evars), gen_vec(Locals,Lvars), append(Ivars,Evars,HeaderInp), append(HeaderInp,Lvars,In), Code =.. [Prog,HeaderInp,Out], tassert(storematch(Prog,Varnames,VI,EI,Locals)). % gen_testcode(Code,In,Out,Dems,B)Ql)'' ,Label) :— gen_vec(In,Out), B""code(Booltest,In), Q l " *code(Chainl,In,02,D2), gen_label(test,Label), Code =.. [Label,In,Out], Testhead =.. [Label,In,02], Testhead2 =.. [Label,In,In], APPENDIX B. BRUCE PARSER 98 copy((Testhead :— (Booltest,Chainl)),Testl), copy((Testhead2 : - "(Booltest)),Test2), append([Testl,Test2],D2,Defns). gen_testcode(Code,In,Out,Defns,B,Ql,Q2,Label) :— Q2 \== gen_vec(In,Out), B"*code(Booltest,In), Ql""code(Chainl,In,02,D2), Q2" "code(Chain2,In,03,D3), gen_label(test,Label), Code =.. [Label,In,Out], Testheadl =.. [Label,In,02], Testhead2 =.. [Label,In,03], copy((Testheadl : - (Booltest,Chainl)),Testl), copy((Testhead2 : - (~(Booltest),Chain2)),Test2), append([Testl,Test2],[D2|D3],Defns). % gen_whilecode(Code,In,Out,Defns,B,Q,Label) : -gen_vec(In,Out), gen_vec(In,03), B""code(Booltest,In), Q""code(Chainl,In,02,D2), genjab el( while ,L abel), Code =.. [Label,In,Out], Loopheadl =.. [Label,In,03], Loophead2 =.. [Label,In,In], Loopcall =.. [Label,02,03], copy((Loopheadl :— (Booltest,Chainl,Loopcall)),Loopl), copy((Loophead2 :— "(Booltest)),Loop2), gen_var_inst(Label,Booltest,In,Var_inst), append([Loopl,Loop2,Var_inst],D2,Defns). % % gen_repeatcode(Code,In, Out,Defns,B,Q): gen_repeatcode(Code,In,Out,Defns,B,Q,Label) :— gen_vec(In,Out), gen_vec(In,03), B""code(Booltest,02), APPENDIX B. BRUCE PARSER 99 0 / *code(Cha in l , In ,02 ,D2) , gen_label(repeat, Label ) , Code =. . [Label,In,Out], L o o p h e a d l =.. [Label ,In,03], Loophead2 =.. [Label ,In,02], L o o p c a l l =. . [Labe l ,02 ,03] , copy( (Loopheadl :— (Cha in l ,~ (Boo l t e s t ) ,Loopca l l ) ) ,Loop l ) , copy((Loophead2 :— (Cha in l ,Bool tes t ) ) ,Loop2) , gen_var_inst(Label,Booltest,In,Var_inst), append([Loopl,Loop2,Var_inst] ,D2,Defns) . % gen_cal lcode(Code,In,Out ,P,V,E) : -P*"code(Proc) , V " - c o d e ( V U s t ) , E""code(El i s t , In ) , match_vars( V l i s t , In,Call_ii ivars), % gen_vec(Vlist,I2), % append(I2,I3,In), set_expressions(In,Elist,Call_invals,Ecode), set_expressions(I3 ,Elist ,Call_invals,Ecode), append( Ca l l j nva r s ,Call_invals,In_args), gen_vec(In_args,Out_args), set_outputs(In, C a l l j n v a r s , 0ut_args ,0ut ) , C a l l =. . [Proc,In_args,Out_args], (Ecode = = " - > Code = C a l l ; fuse((Ecode,Call) ,Code)) . gen_asgn(asgn(In,Var_f,Expr,Out),In,Out,[],V,E) :— V " "code(Vname), E""code(Expr , In ) , var_match( Vn am e ,In ,Var_i), vec_variant (In, V a r j ,Var_f , 0 u t ) . % gen_chain(Code,In,Out,Defns,S,Q) :— S " " c o d e ( S l , I n , X , D l ) , Q " " c o d e ( S 2 , X , O u t , D 2 ) , APPENDIX B. BRUCE PARSER fuse((Sl ,S2),Code), append(Dl ,D2 ,Defns). % % gen_goto(Code,In,Out,L): % Code — goto construct % In — input variable vector % Out — output variable vector % L — points to label gen_goto(goto(In,Label,Out),In,Out,L) :— L"*code(Labe l ) , gen_vec(In,Out). % % set_expressions(In,Elist,Call_invals,Ecode) converts expressions in Elist % into callasgn statements in Ecode. Calljnvals are the variables created % to assign the expression values to before the call. s e ^ e x p r e s s i o n s ^ ^ Q , ' ' ) . set_expressions(In,[VarA|A],[VarB | B] ,D) :— v a r ( V a r A ) , set_expressions(In,A,B,C), fuse( (ca l lasgn(In ,VarB,VarA) ,C) ,D) . set_expressions(In,[Expr|A],[Var|B],C) :— set_expressions(In,A,B , D ) , (D = " - > C = cal lasgn(In,Var ,Expr) ; C = (cal lasgn(In,Var ,Expr) ,D)) . % % gotojound asserts 'found_a_branch' if a branch is detected during % parsing. goto_found :— found_a_branch,!. goto_found :— tassert(found_a_branch). % % gen_var_inst generates an instantiation vector for a construct. % This vector simply states which variables are used in the constructs % test, which is used by the mixer later. APPENDIX B. BRUCE PARSER 101 gen_var_inst(Label,Test,Vec,var_inst(Label,Inst)) : -ext rac t_vars( Tes t , T vars), gen_var_inst2(Tvars,Vec,Inst), j , % % gen_var_inst2 creates a Flags vector which consists of letters '%' and % '/'. V corresponds to each variable in Vec which is found in TestVars; % otherwise 'f is inserted. gen_var_inst2(_,0,0) :- !. gen_var_inst2(Vars,[Var|Rest],[Flag|Flags]) : -(member(Var ,Vars) — > F l a g = i F l a g = f ) , gen_var_inst2(Vars,Rest, Flags) . y0 *** % *** Syntax definitions for Westcott's lexical analyzer % *** white_space_char(32). white_space_char( 10). white_space_char(9). white_space_char (12). ? - o p ( 9 0 0 , f x , ' - ' ) . ? -op (1100 ,y fx , ' # ' ) . ? - o p ( 1 0 0 0 , y f x , ' & ' ) . % space % carriage return % tab % form feed op_chars("+" ,math( ' + ' ) ) . o p _ c h a r s ( " - " , m a t l i ( ' - ' ) ) . op_chars("*" ,math( ' * ' ) ) . o p _ c h a r s ( " / " , m a t h ( ' / ' ) ) . op_chars(" / /" ,math( ' / / ' ) ) • op_chars("":" ,bool( '&')) . op_chars("#",bool(' #')). op_chars(" ' " ,bool( ' " * ) ) . op_chars("< M , rel( '< ')) . APPENDIX B. BRUCE PARSER o p . c h a r s t ' ^ V e l ^ ' ) ) . op_chars( "=< " ,rel( '=<'))• op_chars(">=",rel( '>=')) . op_chars( "=:=" ,rel( ' = : = ' ) ) . op_chars(''=\=M ,rel(> =\=')) . punc t_cha r s ( "{" , ' { ' ) . punc t_cha r s ( "}" , ' } ' ) . p u n c t _ c h a r s ( " , " , ' , ' ) . punc t_chars (" ( 'V ( ' ) . p u n c t _ c h a r s ( " ) " , ' ) ' ) . punct_chars(" [",' [ ' ) . punct_chars("] " , ' ] ' ) . p u n c t _ c h a r s ( " ; " , ' ; ' ) . p u n c t _ c h a r s ( " : " , ' : ' ) . punct_chars(" :=" , ' : = ' ) . reserved(local,local). reserved(if4f). reserved(else,else). reserved( while ,while). reserved(repeat,repeat). reserved(until ,until) . reserved(call,call). reserved(goto,goto). reserved(skip,skip). reserved(true,true). reserved(false,false). constant_form( C ,const (C) ) . % *** % *** expression evaluation routines... % *** " T : - not T . A # B : - ( A ; B ) . A k B : - A , B . va lue(Expr ,Val ) :— APPENDIX B. BRUCE PARSER 103 V a l is E x p r . % *** % *** label generation and numbering % *** % % reset_gen_nums sets genjnums to 1. reset_gen_nums :— abolish(gen_nums,4), tassert(gen_nums(l,1,1,1)). % test, while, repeat, label % - % get_gen_num(Type,Num) returns a new unique number for the structure % Type (test,while,repeat,label). get_gen_num(test,Num) :— gen_nums ( N u m , X , Y , Z ) , Next is N u m + 1, abolish(gen_nums,4), tasser t(gen_nums(Next ,X,Y,Z)) . get_gen_num(while,Num) :— gen_nums(X,Num,Y,Z) , Next is N u m + 1, abolish(gen_nums,4), tasser t(gen_nums(X,Next ,Y,Z)) . get_gen_num(repeat,Num) :— gen_nums(X,Y,Num,Z) , Next is N u m + 1, abolish(gen_nums,4), tasser t (gen_nums(X,Y,Next ,Z)) . get_gen_num(labei,Num) :— gen_nums(X,Y,Z ,Num) , Next is N u m + 1, abolish(gen_nums,4), tasser t (gen_nums(X,Y,Z,Next)) . % APPENDIX B. BRUCE PARSER 104 % gen_label(Labeltype,Label) generates a new Label for structure Labeltype. gen_label(Labeltype,Label) :— get_gen_num(Labeltype,Num), a tom_append(Label type,Num,Label) , % % newjabellist resets the labellist for program Prog, and asserts that % Prog is the current program being processed. newJabel l i s t (Prog) :— (retract(labell ist(Prog w ,_)); true), tassert(labellist(Prog,[],[])), tabolish(curr_prog,l) , tassert(curr_prog(Prog)), ; # % % add_curr_labellist(Type,Label) adds Label to the label list for the current % program being processed, determined by currjprog. add_curr_labellist(label,Label) : -curr_prog(Prog), re t rac t ( labe l l i s t (Prog ,Lis t l ,L is t2) ) , append( [Labe l ] ,L i s t l ,Newl i s t l ) , append([Label] ,List2,Newlist2) , tasser t ( label l is t (Prog,Newlis t l ,Newlis t2)) , !_ add_curr_labellist(_,Label) :— curr_prog(Prog), re t rac t ( labe l l i s t (Prog ,Lis t l ,L is t2) ) , append([Label] ,Lis t l ,Newlis t ) , tassert( label l is t(Prog,Newlist ,List2)) , I. % % add approp labellist (Label, Newlabel): % % add_approp_labellist adds Newlabel to the general label list which also % contains Label. APPENDIX B. BRUCE PARSER 105 add_approp_labeIlist(Label,Newlabel) :— l a b e l l i s t ( A , L i s t l , B ) , member2(Label,Listl), r e t r ac t ( l abe l l i s t (A ,L i s t l ,B ) ) , append([Newlabel] ,Lis t l ,Newlis t ) , tassert(labellist(A,Newlist ,B))> i % labelpgm(Clause) is satisfied if Clause is a label program. l a b e l p g m ( ( H : - B ) ) : -functor(H ,Name,_), labellist(_,_,Labels), member2( Name,Lab els). Appendix C B r a n c h H a n d l i n g % *** % *** Prolog branch transformation utilities % *** % *** _ Brian J. Ross % *** Dept. of Computer Science % *** University of British Columbia % *** % % process_branches(Prolog,Newprolog) transforms the clauses in Prolog so % that branches are properly handled. First, all chains of goals following % branches are removed (label programs may exist which contain the code % being thrown away). % Then the prolog is transformed to account for the branches within descendent % predicates, processjbranchesj3 is called to iterate through all the Prolog % clauses. For each one with a goto, the goto goal is changed into a call to % the appropriate label program. Then the parent predicates of the clause % with this goto are transformed. process_branches(Prolog,Newprolog) :— process_branches(Prolog,Prolog,Prolog2), chop_branch_chains(Prolog2,Prolog2,Newprolog), process_branches(Prolog,[],Prolog) :— !. process_branches(Prolog,[Clause|_],Newprolog) :— nnd_goal(Clause ,Head,Lef t ,goto(X,Y,Z) ,Right) , 106 APPENDIX C. BRANCH HANDLING create_labelcal l (goto(X,Y,Z) ,Cal l ) , branch_restruct(Prolog,Clause,Head,Prolog2), insert_goal(Prolog2,Clause,Head,Left ,[Call] ,Right,Prolog3), process_branches(Prolog3,Prolog3,Newprolog), process_branches(Prolog,[JR],Newprolog) : -process_branches(Prolog,R,Newprolog), I, % % branchjrestruct restructures Prolog given a clause with a branch call/ % ancestor of a branch call, Goal. % Case 1: Clause has a parent: % Ancestors of Clause are restructured, and code returned is used to % restructure the sibling of Clause. % Case 2: Clause has no parent: % Clause is a main program clause, and is left alone for now. branch_restruct(Prolog,Clause,Head,Newprolog) : -restruct_parent(Prolog,Head,Pvec,Pcode,New2), restruct_sibling(New2,Clause,Pvec,Pcode,Newprolog), branch_restruct(Prolog%_,_,Prolog) :— I. % % restruct_parent finds the non—label—program parent of Head. % It then pulls goals from the right of the call to Head, resulting in Code. % The branchjrestruct is called on the parent, causing a recursive restructuring % up the tree. restruct_parent(Prolog,Head,Ivec,Code,Newprolog) :— parent_clause(Prolog,Head,Parent,Phead,Left ,Goal,Right) , not labelpgm(Parent) , set_code(Phead,Left ,Goal,Right,Ivec,Code), branch_restruct(Prolog,Parent,Phead,Newprolog), % % restruct_sibling adds Code to the end of the sibling of Clause, % if one exists. APPENDIX C. BRANCH HANDLING 108 restruct_sibling(Prolog,Clause,Vec,Code,Newprolog) :— sibling_clause(Prolog,Clause,Sibling), append_goals(Sibling,Vec,Code,Newsibling), remove_item(Sibling,Prolog,New2), append([Newsibling],New2,Newprolog), restruct_sibling(Prolog,_,_,_,Prolog) : - !. % % setjcode returns the goals to the right of Goal, should they exist, along % with their input vector. set_code(Head,Left,Goal,[],_,[]) :— set_code(Head,Left ,Goal,Right,In,Code) :— get_IO([Head],I l ,01), append(Lef t ,Goal ,G) , get_prev_IO(G,(I l , I l ) , I2 ,02) , get_prev_IO (Right , ( 0 2 , 0 2 ) ,13,03), copy ((13 ,Right) ,(In ,Code)), !. % % restruct_clause restructures a clause by merging Left and Right together. % restruct_clause2 and restruct_prog do the actual reconstruction. restruct_clause(Head,Left,Call,Newclause) :— functor(Head,Name,_), storematch(Name^ v_,_,_), i restruct_prog(Head,Left,Call ,Newclause). restruct_clause(Head,Left,Call,Newclause) :— restruct_clause2(Head,Left,Call,Newclause), I restruct_clause2(Head,[],Right,Code) :— Head =.. [ N a m e , I l , O l ] , get_prev_IO(Right , ( I l , I l ) , I2 ,02) , Newhead =.. [Name, I l ,02] , APPENDIX C. BRANCH HANDLING list_to_body (Right , B o d y ) , copy((Newhead : - Body) ,Code) , !. restruct_clause2(Head,Left,[],Code) :— Head =.. [Name, I l ,01] , get_prev_IO (Left,(II ,11) ,12,02), Newhead =.. [Name, I l ,02] , l is t_to_body(Left ,Body), copy((Newhead :— Body) ,Code) , I . restruct_clause2(Head,Left,Right,Code) :— copy((Head,Left ,Right) , (Head2,Left2,Right2)) , Head2 =.. [Name, I l ,01] , get_prev_IO(Left2,(I l , I l) , I2,02), get_prev_IO(Right2,(02,02) , I3,03) , 0 2 = 13, Newhead =.. [Name, I l ,03] , append(Lef t2 ,Right2 ,B) , l i s t_ to_body(B,Body) , copy((Newhead :— Body) ,Code) , I . % ; % restruct_prolog is almost like restruct_clause2. % It creates a program clause by merging the goals in Left and % Right, but removing local variables from the header 10 vectors. restruct_prog(Head,Left,Right ,Newclause) :— Head =.. [ N a m e , I l , O l ] , get_prev_IO(Left , (I l , I l ) , I2,02), get_prev_IO(Right , (02,02) , I3 ,03) , gen_vec(01,04), append(04,_,03) , Newhead =. . [Name, I l ,04] , append(Lef t ,Right ,B) , l i s t_ to_body(B,Body) , copy((Newhead :— Body),Newclause) , i APPENDIX C. BRANCH HANDLING % createjabelcall changes a goal in goto format to a label call. create_labelcall(goto(In,Label,Out),Call) :— C a l l =. . [Label ,In,Out] , I. % : % chop_branch_chains(Prolog, Clauses, Collect) takes each clause with % label program call and throws away any goals following it. chop_branch_chains(_,[|,[|) : - !. chop_branch_chains(Prolog,[Clause | R] ,T) :— split_clause(Clause,Head,Goals), check_for_branches(Prolog,Goals,Goals2), restruct_clause(Head,[],Goals2,Newclause), chop_branch_chains(Prolog,R,S), (member3(Newclause,S) —> T = S T = [Newclause|S]), !_ chop_branch_chains(Prolog,[Clause|R],[Clause|T]) :— chop_branch_chains(Prolog,R,T), !. insert_goal(Prolog,Clause,Head,Left ,Goal,Right ,Newprolog) :— append_list([Left ,Goal,Right],Goals), l is t_to_body(Goals ,Body), Newclause =. . [(:—),Head,Body], (member3(Newclause,Prolog) — > Newprolog = Pro log remove_item(Clause,Prolog,New2), Newprolog = [Newclause |New2]), i % *** % *** Label program generation % *** APPENDIX C. BRANCH HANDLING 111 % % gen_labelprogs(Prolog,Labelprogs) creates a new prolog environment which % contains predicates for the label programs in Prolog. It calls a % genjabelprogs/ 3 version, where the second argument iterates through % the clauses. % The goals for the label program are obtained, and a label program is created. % Then all label references for the program just created are removed from the % prolog environment. gen_labelprogs(Prolog,Newprolog) :— gen_labelprogs(Prolog,Prolog,Newprolog), gen_labelprogs(Prolog,[],Prolog) :— !. gen_labelprogs(Prolog,[Clause|R],Newprolog) :— find_goal(Clause,Head,Left,label(Label),Right), get_goals(Prolog,Clause,Head,Left ,Label ,Right,In,Out,Goals ,Defns), create_labclause(Label,In,Out,Goals,Labelprog), append_list([[Labelprog],Defns,Prolog],Prolog2), rem_pred_labels(Prolog2,label(Label),Prolog3), genjab elprogs (Prolog3 ,P r olog3 ,Ne wprolog), !_ genJabelprogs(Prolog,[ jR],Newprolog) :— genjab elprogs(Prolog,R,Newprolog), i_ % % getjgoals retrieves the goals to be used for a label program. % If a goal in Right contains a branch, then all the goals % up to and including that goal are used for the label program. % Otherwise, the goals of the parent construct are obtained, and the % result is appended to the goals in Right. get_goals(Prolog,Clause,Head,Left,_,Right,In,Out,Goals,[]) :— branch_under_goals(Prolog,Head,Left,Right,In,Out,Goals), tt get_goals(Prolog,Clause,Head,Left ,Label,Right,In,Out,Goals,Defns) :— create_construct_control(Prolog,Head,Left ,Label ,Right ,Cin,Cout ,Control ,Defnsl) , APPENDIX C. BRANCH HANDLING parent_goals(Prolog,Head,Pin,Pout,Pgoals,Defns2), append(Defnsl,Defns2,Defns), merge_goals(Cin,Cout ,Control ,Pin ,Pout ,Pgoals , In ,Out ,Goals) , I, % % parentjgoals recursively obtains the parent goals to be used by a % label program. The successive parent goals to the right of the call to a % child predicate are obtained and concatenated together. This recursion % stops when (a) the top predicate is reached, or (b) a branch has been % detected under a goal. parent_goals2 is used as a subsidiary call. % Note that label programs are not considered parents. parentj*oals(Prolog,Head,In,Out,Goals,Defns) :— parent_clause(Prolog,Head,Parent,Phead,Left ,Goal,Right) , not labelpgm(Parent) , append(Left ,[Goal] ,L2), functor(Goal,Goallabel ,_), get_goals(Prolog,Parent ,Phead,L2,Goallabel ,Right ,In,Out,Goals ,Defns) . parent_goals(_,_^ .,_,0 ,Q). % : % branchjunderjgoals obtains all the goals up to and including a goal in Right % which contains a branch. It fails should no branches be found under any goal % in Right. branch_under_goals(Prolog,Head,Left ,Right,In,Out,Goals) :— check_for_branches(Prolog,Right,Goals2), ge t_ IO( [Head ] ,HJ , get_prev_IO (Left ,(11,11) ,_,In2), get_prev_IO(Goals2,(In,In),_,Out2), copy((In2,Out2,Goals2) , (fn,Out ,Goals)) . % % check_for_branches does a search for branches under Goals. % It keeps all the goals in Goals up to and including the first one with a % descendent branch. It fails should no descendent branches be found. check_for_branches(_, u, u) :— !,fail . check_for_branches(Prolog,[goto(I,L,0)|_],[goto(I,L,0)]). APPENDIX C. BRANCH HANDLING check_for_branches(Prolog,[Goal|J,[Goal]) :— functor(Goal,Name,_), labellist(_,_,Labels), member(Name,Labels) . check_for_branches(Prolog,[Goal|R],[Goal]) :— descendent_branches(Prolog,Goal). check_for_branches(Prolog,[Goal|R],[Goal|S]) : -checkJbrJ>ranches(Prolog,R,S). % % descendent_branch.es performs a recursive search for branches under goal G. % For efficency, G is analyzed for it's goal type so that needless % search is not done on goals with no descendents (assignments, program calls, % etc). descendent_branches2 is called to iterate through new goal lists % obtained during the search. descendent_branches(Prolog,G) : -member2( G , [asgn(_,_,_,J ,callasgn(_,_,_) ,label(_) ,goto(_,_,_)]), ! f a i l . descendent_branches(Prolog,T) :— is_a_test(T), fai l . descendent_branches(Prolog,Call) :— functor(Call ,Prog,_) , s torematch(Prog^^^,_) , I f a i l . descendent_branches(Prolog,G) :— functor(G ,Lab,_), label l is t(_^,Labels) , member2(Lab,Labels), descendent_branches(Prolog,Goal) :— APPENDIX C. BRANCH HANDLING 114 find_clause(Prolog,Goal,Clause), r emove j tem( Clause ,P rolog ,Prolog2), split_clause(Clause,_,Body), descendent_branches2(Prolog2,Body). descendent_branches2(_,Q) :— !,fail. descendent_branches2(_,[goto(_^,_)|J) : - !. descendent_branches2(Prolog,[Goal|J) : -descendent_branches(Prolog,Goal), descendent_branches2(Prolog,[_|R]) : -descendent_branches2(Prolog,R), % % createjabclause creates a label program. create_labclause(Lab,In,Out,[],Clause) :— Header =. . [Lab,In,Out] , copy(Header,Clause). create_labclause(Lab,In,Out,Goals,(Header :— Body) ) :— copy((In,Out,Goals),(I2,02,Goals2)), Header =. . [Lab,l2,02], list_to_body(Goals2,Body). % % create_construct_control creates a list of goals, Control, which comprise % the particular control sequence needed when junping into the construct % at the point Right. With brace, there are two cases: % (l) jumping into a repeat — since repeat tests are done at the end of % the loop, the repeat test must be simulated. This requires % calling create_repeat_control to create this special control. % (2) jumping into any other mechanism — simply return the goals to the % right of the jump point. create_construct_control(Prolog,Head,Left ,Label,Right,In,Out,Control,Defns) :— functor(Head,Name,_), ge t jab el_r efs (P rolog , N ame, [], [ A ,B ]), tes t_if_repeat(A,B,OutT,Test ,Body), APPENDIX C. BRANCH HANDLING 115 create_repeat_control(OutT,Test3ody,Label,Head,Left,Right,In,Out,Control,Defns). create_construct_control(Prolog,Head,Left^,Right,In,Out,Control,[]) :— ge t_ IO( [Head] , I l J , get_prev_I0(Left , (I l , I l ) ,_ ,02), get_prev_IO(Right , (02,02) , I3 ,03) , copy( (Right , l3 ,03) , (Cont ro l , In ,Out ) ) . % % create_repeat_control creates the control environment for a repeat construct. % The output is % Control = [Body,Test] % Defns = [(Testl :- ~Test,Head),(Testl :- Test)] % all suitably tidied. % The name for Test is externally saved through calling add_approp_labellist. create_repeat_control(Vec,Test ,Body,Label ,Head,Left ,Right,In,Out,Control ,[Dl,D2]) :— copy((Vec,Test ,Body),(Vec2,Test2,Body2)) , copy((Head,Left ,Right) , (Head2,Left2,Right2)) , append(Left2,Rightgoals ,Body2), % get goals after jump point functor(Head,Name,_), get_I0([Head2],Il,_), get_prev_IO(Left2,~(Il,Il),_,02), get_prev_IO(Rightgoals ,(02,02),I3,03), gen_label(test ,Testlabel), gen_vec(Vec2, Vou t ) , H e a d A =. . [Testlabel,Vec2,Vout], HeadB =. . [Testlabel,Vec2,Vec2], C a l l =. . [Name,Vec2,Vout] , l is t_to_body(["(Test2) ,Cal l] ,BodyA), copy ((~HeadA: - B o d y A ) ,D 1), copy( (HeadB: - T e s t 2 ) ,D2) , add_approp_labellist(Label,Testlabel), merge_goals(I3,03,Rightgoals,Vec2,Vout,[HeadA] , In ,Out ,Control ) . % % remjpredjabels simply removes all goals of the form Label from Clauses. % This is done so that we don't construct duplicate label programs. rem_pred_labels([],_,[]) : - !. rem_pred_labels([Clause|R],Label,[Newclause|S]) : -APPENDIX C. BRANCH HANDLING 116 fin d_goal( Clause, Head ,Left ,L ab el ,Right ) , make_clause(Head,Left,Rigbt,Newclause), rem_pred_labels(R,Label,S), rem_pred_labels([Clause|R],Label,[Clause|S]) :— rem_pred_lab els ( R , L a b el , S) , i Appendix D B r u c e G e n e r a t i o n % *** % *** Bruce code generation facility % *** % *** _ Brian J. Ross % *** Dept. of Computer Science % *** University of British Columbia % *** % % brucify(Env) converts the entire Prolog environment in list Env % into Bruce code. bruci fy(Env,Bruce) :— bagof([P | Q] ,X * labellist (P ,Q ,X) .Labels), copy (Env,Env2), program_separate(Env2,Labels,[],Prolog), brucify_programs(Prolog,[],Bruce). % % brucify_programs(Programs,Collect,Result) converts each prolog program % in Programs to Bruce code. brucify_programs( [] ,Bruce,Bruce) . brucify_programs([Progname,Prog|Rest] ,Collect,Bruce) :— get_label_refs(Prog,Progname,[],Clauses), get_IO (Clauses,In,_), 117 APPENDIX D. BRUCE GENERATION 118 t empla te_match(Progname, In ,Prog ,Clauses ,B»[ ] j_ )» r e r n u n usedjab els (B ,B 2), create_outval_asgns(Progname,Clauses,Asgns), chain_append(B2 ,Asgns,Body), bruce_header(Progname,Header), append_list([Header,[ ' {' ] >Body,[ '} ' ]] ,Bruce_prog), brucify_programs(Rest,[Bruce_prog|Collect],Bruce). % % templatejnatch(Progname,Prolog, Clauses,Bruce,Labels,Newlabels): % Matches Clauses to known bruce construct definitions. % NOTE: Should the dataflow of goals be altered, include the two lines noted % below. template_match(_,_,_,[],_,_,_) :— !,fail. template_matcli(Prognarrie u ,Prolog,[Clause],Bruce,Labels,Newlabels) :— % split_clause(Clause,Head,Goals), % < see note above % order_clausejgoals(Goals, Ordered), % <— see note above split_clause( Clause, Head .Ordered), get_IO([Head],In,_), template_match_goals(Progname,In,Prolog,Ordered,Bruce,Labels,Newlabels). % repeat: t e m p l a t e _ m a t c h ( P r o g n a m e , V e c , P r o l o g , [ A , B ] » B r u c e » L a b e l s , N e w l a b e l s ) :— is_a_repeat(Progname,A,B)Test ,Body), g e t _ I O ( A w O u t ) , template_match^oals(Progname,Out ,Prolog,Body,Bruce_body,Labels ,Newlabels) , append_list([[repeat,' { ' ] ,Bnice_body,[ '} > , un t i l , ' ( ' ,Tes t , ' ) ' ]] ,Bruce). % while: t emp la t e_ma tch (P rogname ,Vec ,P ro log , [A ,B]»Bruce ,Labe l s ,Newlabe l s ) :— is_a_while(Progname,A,B,Test ,Body), g e t J O ( A M O u t ) , template_match^oals(Progname,Out,Prolog,Body,Bruce_body,Labels ,Newlabels) , append_l is t ( [ [ 'whi le ( ' , T e s t , ' ) ' , ' { ' ] , B r u c e _ b o d y , [ » } ' ] ] , B r u c e ) . % if: template_match(Progname,Vec,Prolog,[A,B],Bruce,Labels,Newlabels) : -APPENDIX D. BRUCE GENERATION 119 is_an_if(Progname,A,B,Test,Thengoals,Elsegoals), getjb(AMOut), template_match^oals(Progname,Out,Prolog,Thengoals ,Thencode,Labels ,Newlabels2) , (Elsegoals = = Q - > append_l is t ( [ [ ' i f (' / T e s t , ' ) » , ' { ' ] , T h e n c o d e , [ ' } ' ] ] , B r u c e ) , Newlabels = Newlabels2 template_match^oaIs(Progname,Out,Prolog,Elsegoals,Elsecode,Newlabels2,Newlabels) , append_list([[' i f (' , T e s t , ' ) ' , ' { ' ] , T h e n c o d e , [ ' } ' ,else,' { ' ], Elsecode,[ '} ' ] ] ,Bruce)) . template_match(Progname,Vec,Prolog,Clauses,Bruce,Labels,Newlabels) :— factor (Clauses ,Prolog,NewClauses ,NewProlog) , template_match(Progname,Vec,NewProlog,NewClauses,Bruce,Labels ,Newlabels) . % ; ___ % template_match_goals(Progname,Prolog, Goallist,Bruce,Labels,Newlabels): % Matches each goal in Goallist to a construct. % One of three situations is possible: % (a) Finished — empty Goal list % (b) Goal is an assignment: a Bruce assignment is created % (c) Goal is a call assignment: it is temporarily ignored until the % corresponding call is found. % (d) Goal is a procedure call: a Bruce proc. call is created. % (e) Goal refers to a structure previously created: create a % branch to it. % (f) Goal refers to a structure previously created, but step (e) failed: % then fail (unknown structure). % (g) none of the above: then the goal must be a call to a more complex % mechanism. All the clauses relevant to that goal are % extracted, and a template match is performed on them. % case (a) template_match_goals(_,_,_,[],[] , L , L ) . % case (b) template_match^oaIs(Progname,_,Prolog,[asgn(In,Var,Expr,Out) |Rest] ,Bruce,Labels,Newlabels) :— i •> template_match_goals(Progname,Out,Prolog,Rest ,B,Labels,Newlabels) , convert_bruce_expr(Progname,In,Expr,Expr2), convert_bruce_expr(Progname,Out,Var,Var2), chain_append([Var2, ' : = ' ,Expr2] ,B,Bruce) . A P P E N D I X D. B R U C E G E N E R A T I O N 120 % case (c) template_matchj!;oals(Progn^ :— i append(Rest , [cal lasgn(A,B,C)] ,Rest2) , template_match_goals(Progname,Vec,Prolog,Rest2,Bruce,Label,Newlabels). % case (d) template_match_goals(Progname,Vec,Prolog,[Goal|Rest],Bruce,Labels,Newlabels) :— G o a l =. . [Prog,In,Out], storematch(Prog,Vars,Ref,Val,_), i •J collect_callasgns(Rest,In,Calls), gen_vec(Val ,Vl ) , append(Refvec ,Vl , In) , create_val_vector(Vl ,Calls ,Ivec,Valvec), C a l l =. . [Prog,Refvec,Valvec], remove_items2(Calls,Rest,Rest2), t e m p l a t e _ m a t c h _ g o a l s ( P r o g n a m e , O u t , P r o l o g , R e s t 2 , B » L a b e l s , N e w l a b e l s ) , convert_bruce_expr(Progname,Vec,Call ,Call2), chain_append([' c a l l ' ,Ca l l2 ] ,B , Bruce) . % case (e) template_match^oals(Progname,Vec,Prolog,[Goal |Rest] ,[goto,Name],Labels,Labels) :— functor(Goal,Name,_), member 2 (Name , L ab els). % gen_impl_asgns(PrognarnelVec,Goal,Asgns), % remove?? % chain_append(Asgns,[goto,Name],Bruce). % remove?? % case (f) template_match_goals(_,_,_,[Goal|J ,_,Labels,_) :— functor(Goal,Name,_), member2(Name,Labels) , j fa i l . % case (g) template_match_goals(Progname,Vec,Prolog,[Goal|Rest],Bruce,Labels,Newlabels) :— functor(Goal,Name,_), get_label_refs(Prolog,Name,[],Clauses), template_match(Progname,Vec,Prolog,Clauses,BruceA,[Name|Labels] ,Newlabels2), get_IO([Goal],In,Out), APPENDIX D. BRUCE GENERATION 121 gen_impl_asgns(Progname,Vec,In,Asgns), template_match_goals(P rogname ,0 ut ,Prolog,Rest ,BruceB ,Newlabels2,Newlabels), append( [Name, ' : ' ] , B r u c e A , X l ) , chain_append(Asgns,Xl ,X2), chain_append(X2 ,BruceB,Bruce). % % is_an_if(Progname,A,B,Brucetest, Then,Else) % Tests if goals A,B can be matched with a Bruce test construct, and % creates Bruce code if they match. i s_an_i f (Progname,A,B)B r u c e tes t ,Then ,Else) :— test_if_if(A,B,I,Test,Then,Else), convert_bruce_expr(Progname,I,Test,Brucetest). % % is_a_while(Progname,A,B,Brucetest,Body): % Tests A and B for a match with a Bruce while construct, and % creates Bruce code if they match. i s_a_while(Progname,A,B)B r ucetest ,Body) :— test_if_while(A,B,I ,Test ,Body), convert_bruce_expr(Progname,I,Test,Brucetest). % ; % is_a_repeat(Progname,A,B,Brucetest,Body): % Tests A and B for a match with a Bruce repeat construct, % creates Bruce code if they match. is_a_repeat(Progname,A,B)Brucetest ,Body) . _ test_if_repeat(A,B,0,Test ,Body), convert_bruce_expr(Progname,0,Test,Brucetest). % % complementary_tests(BodyA,BodyB,TA,TB) finds an instance of complementary % tests TA and TB in BodyA and BodyB (ie. TA = ~TB). Repeated calls % will return new complementary tests, if any. c o m p l e m e n t a r y _ t e s t s ( B o d y A , B o d y B , T A , T B ) :— member2(TA,BodyA), is_a_test(TA), member2(TB,BodyB), APPENDIX D. BRUCE GENERATION 122 is_a_test(TB), complementary ( T A , T B ) . % % convert_bruce_expr(PrognamelIn,Expr,Conv) created a copy of Expr having % the appropriate Bruce variable names, based on ordering in In. % The result is in Conv, as we don't want to bind the actual logical % variables (lose dataflow information). convert_bruce_expr(Progname,In,Expr,Conv) : _ copy((In ,Expr) , ( In2,Conv)) , set_all_to_vars(In2,In3), storematch(Progname,In3,_,_,_), % % A bruce program header is created... bruce_header(Progname,[A, ' : ' ,local,Locals]) :— storematch(Progname,Vars,Ref ,Val ,Locals) , A =. . [Progname,Ref,Val]. % % recursive_call(Call, Goals, C) is satisfied if a recursive call C to header % Call exists in the Goals list. recursive_call(Call ,Goals,C) :— c o p y ( C a l l , C ) , member2( C , Goals) , same_out_vars(Call,C). % ; % collect_callasgns(Goals,Vars,Calls) finds instances of callasgn goals in Goals % which assign values to variables listed in Vars. The results are in Calls. collect_callasgns([]%_,[]) :— !. collect_callasgns([cal lasgn(A,Var,B) |R],Vars,[cal lasgn(A,Var,B) |D]) : -member(Var ,Vars) , collect_callasgns(R,Vars,D), !. collect_callasgns([_|R],Vars,D) :— collect_callasgns(R, Va r s, D ) , APPENDIX D. BRUCE GENERATION % % create_val_vector(Vars,Calls,Valvec) creates a value parameter list % for a Bruce procedure call. % Variables in Vars which have a corresponding callasgn in Calls are replaced % with the expression in that callasgn. Otherwise that variable is used. create_val_vector([],_,_,[]) :— !. create_val_vector([V| R] ,Callasgns ,1 vec,[T | W]) :— (collect_callasgns(Callasgns,[V] ,[callasgn(Ivec,_,Expr)]) — > create_val_vector(R,Callasgns u ,W), T = E x p r create_val_vector(R,Callasgns,Ivec,W), T = V ) , % % chain_append(A,B,C) appends lists A and B together, such that if B is % nonempty, a semicolon is inserted between them. chain_append(A,[],A) :— !. chain_append([],A,A) :— !. chain_append(A,B>C) :— append_l is t ( [A,[ ' ; ' ] , B ] , C ) , I. % % rem_unused_labels(Bruce,Newbruce) removes labels from the bruce source % which have no branches onto them. rem_unused_labels(Bruce,Newbruce) :— rem_unused_lab els(Bruce ,B ruce,Newbruce), I, rem_unused_lab els (_, Q, D). rem_unused_labels(U,[L, ' : ' |R ] , [L , ' : ' |A]) : -find_goto(L,U), rem_unused_labels(U,R)A.). rem_unused_labels(U,[L, ' : ' | R ] , A ) :— rem_unused_lab els( U ,R , A ) . APPENDIX D. BRUCE GENERATION rem_unused_labels(U,[S | R],[S |A]) :— rem_unused_labels(U,R,A). % find_goto(Label,Bruce) finds a branch to label Label in the Bruce code. find_goto(Label,[goto,Label|J) : - !. find_goto(Label,[S|R]) : -nnd_goto(Label ,R), I. % % test_if_if checks if A and B match with an if construct of Bruce. % The matching criteria are: % (a) complementary tests in A and B % (b) Both tests are dependent on their header input variables test_if_if(A,B,I,Test,Then,Else) : -split_clause( A ,Head A ,B ody A ) , split_clause(B ,HeadB ,Body B ) , c o m p l e m e n t a r y _ t e s t s ( B o d y A , B o d y B , T A , T B ) , dep_in_vars(TA,HeadA), dep_in_vars(TB,HeadB), r e m o v e _ i t e m ( T A , B o d y A , N e w A ) , r emove_ i t em(TB,BodyB,NewB) , se t_ then_else(TA,HeadA,NewA,TB,HeadB,NewB,Tes t ,Then ,Else ,Head) , Head =. . [_,I,J. % % test_if_while checks if A and B match with a while construct of Bruce. % The matching criteria are: % (a) complementary tests in A and B. % (b) Both tests are dependent on their header input variables % (c) One of the clauses has a body consisting only of the test. % (d) The other clause contains a recursive call matching the head. test_if_while(A,B,I,Test,Body) : -sp l i t_c lause (A,HeadA,BodyA) , split_clause(B ,HeadB ,Body B ) , c o m p l e m e n t a r y _ t e s t s ( B o d y A , B o d y B , T A , T B ) , dep_in_vars(TA,HeadA), dep_in_vars(TB ,HeadB) , ( B o d y A = = [TA] , APPENDIX D. BRUCE GENERATION 125 (Test ,Head,Goals) = ( T B , H e a d B , B o d y B ) B o d y B = = [TB] , (Test ,Head,Goals) = ( T A , H e a d A , B o d y A ) ) , recursive_call(Head,Goals,Call) , remove i tems2([Test ,Cal l] ,Goals ,Body), Head =. . L.IJ. % % test_if_while checks if A and B match with a repeat construct of Bruce. % The matching criteria are: % (a) complementary tests in A and B. % (b) One clause contains a recursive call matching the head. % (c) The test in that clause is dependent on the headers input variables. % (d) The test in the other clause uses variables in the headers output % variables list. % (e) The remaining goals which should compose the repeat body are % the same (permutation). test_if_repeat(A,B,0,Test ,Body) :— split_clause( A ,Head A ,B ody A ) , split_clause(B , H e a d B , B o d y B ) , complementary_tes ts (BodyA,BodyB , T A , T B ) , ( recurs ive_ca l l (HeadA,BodyA,Cal l ) , ( T l , B l , T e s t , H 2 , B 2 ) = ( T A , B o d y A , T B , H e a d B , B o d y B ) recurs ive_cal l (HeadB,BodyB,Cal l ) , ( T l , B l , T e s t , H 2 , B 2 ) = ( T B , B o d y B , T A , H e a d A , B o d y A ) ) , dep_in_vars(T 1 ,Ca l l ) , dep_out_vars(Test,H2), remove_item(Test ,B2,Body), remove_i tems2([Tl ,Cal l ] ,Bl ,New2) , permuta t ion(Body,New2) , . H 2 =. . [_,_,0]. % % set_then_else(TA,HeadA,NewA, TB,HeadB,NewB, Test, Then,Else,Head) sets % Test, Then, Else, and Head appropriately. set_then_else(TA,HeadA,[] ,TB,HeadB , N e w B , T B , N e w B , [ ] , H e a d B ) : -N e w B \ = = [], i APPENDIX D. BRUCE GENERATION set_then_else(TA,HeadA,NewA,TB,HeadB,Q,TA,NewA,[],HeadA) : -NewA \== 0, ;# set_then_else(TA,HeadA,NewA,TB,HeadB,NewB,TB,NewB,NewA,HeadB) : -functor(TA, '" ' J , !_ set_then_else(TA,HeadA,NewA,TB,HeadB,NewB,TA,NewA,NewB,HeadA) : - !. % % set_all_to_vars copies A to B, replacing nonvar items with new var ones. set_all_to_vars([],[]) :— !. set_aU_to_vars([A|B],[A|D]) : -var(A), i •» set_all_to_var s( B ,D). set_all_to_vars([A|B],[C|D]) : -set_all_to_vars(B,D), % create_outval_asgns creates an assignment for each call—by—value % parameter for program Progname if that parameter has a ground value in % programs output vector (which can occur through mixed computation). create_outval_asgns(Progname,[(H:—B)],Asgns) :— get_IO([H],_,Out), storematc^Progname^Re-i-*-)-)) gen_vec(Ref,Refvec), append(Refvec>_,Out), set_asgns(Progname,Out,Ref,Refvec,Asgns), % % gen_impl_asgns checks the In vector: for each ground item in In, % an implicit assignment is created. These % assignments represent the effects of the mixed computation. gen_impl_asgns(Progname,Vec,In,Asgns) :— i storematch(Progname,Varsv.,_^), set_asgns (P rogname ,In, Var s ,In, Asgns). APPENDIX D. BRUCE GENERATION 127 % % setjasgns creates an implicit assignment for each item in Vec having % a ground value. set_asgns(_,_,_,0,0) :- !.' set_asgns(Progname,Vec,[Var|R],[S|T],A) :— nonvar(S), t set_asgns(Progname,Vec,R,T,Q), convert_bruce_expr( Progname, Vec, S, S 2), chain_append([Var, ' : = ' , S 2 ] , Q , A ) . set_asgns(Progname,Vec,[_|R],[_|T],A) :— i se t_asgns(Progname,Vec,R,T,A). % *** % *** Prolog factoring utilities % *** % ; % factor (Clauses, Prolog, [NewClause],NewProlog) tries to factor out common % goals in Clauses. Goals may be factored if: % (a) the factorable goals are common between two clauses % (b) dataflow among them is the same % factor extracts two different clauses from Clauses, and calls factorjgoals to % factor out the common goals, if any. % If factor_goals succeeds, then the old clauses are removed from the Prolog % environment, and the new restructured clause NewClause plus the additional % definitions are inserted into the environment, resulting in NewProlog. factor(Clauses,Prolog,[NewClause],NewProlog) :— member2(A,Clauses) , member2(B, Clauses), A \ = = B , factor_goals(A,B,NewClause,NewDefns) , remove_items( [ A , B ] ,P ro log ,X 1), append([NewClause |NewDefns] ,Xl ,NewProlog) , I. APPENDIX D. BRUCE GENERATION 128 % % factor_goals(A,B,NewClause,NewDefns) attempts to factor out common goals in % clauses A and B. If common goals are found, the disjoint goals are % removed from the clauses, and are put into a new predicate defined in % NewDefns. Clauses A and B are merged, resulting in NewClause. % % Factorjgoals first orders the goals in A and B w.r.t. dataflow. % Then common goals on the left side of the goal body are found. % If not successful, common goals on the right side are searched for. % If common goals can be extracted, spawn_clause is called to do the % Prolog code maintenance. factor_goals(A,B,NewClause,NewDefns) :— split_clause( A ,Head A ,B ody A ) , sp l i t_c lause(B,HeadB,BodyB) , order_clause_goals(BodyA,OrdA), or der_clause_goals (B ody B , 0 r d B ) , (Side = left, d u o _ s p l i t ( l e f t , O r d A , C o m m o n A , R e s t A , O r d B , C o m m o n B , R e s t B ) Side = right, d u o _ s p U t ( r i g h t , O r d A , R e s t A , C o m m o n A , O r d B , R e s t B , C o m m o n B ) ) , p e r m u t a t i o n ( C o m m o n A , C o m m o n B ) , spawn_clause(Side ,HeadA,CommonA,Res tA,HeadB,CommonB,Res tB,NewClause ,NewDefns) . % % Spawn_clause creates new Prolog code, given common goal sets CommonA and % CommonB. The two cases are when common goals are found on the left and % right sides of the clauses. The Prolog code creation involves % merging the two clauses into one containing the common goals plus call to % the new predicate, and creating a new predicate containing the disjoint % goals, spawnjeftjnain, spawn_left_aux, etc., do the actual prolog % transformation, dividing the Prolog clause on its left or right side. spawn_clause( le f t ,HeadA,CommonA,Res tA,HeadB,CommonB,Res tB,Newl , [New2,New3]) :— spawn_left_main(Head A , C o m m o n A ,Rest A ,Newlabe l ,Newl) , spawnJef t_aux(Newlabe l ,HeadA,CommonA,Res tA,HeadB,CommonB,Res tB ,New2,New3) , spawn_clause( r igh t ,HeadA,CommonA,Res tA,HeadB,CommonB,Res tB,Newl , [New2,New3]) :— spawn_right_main(HeadA ,Common A ,Rest A ,Newlabe l ,Newl) , spawn_r igh t_aux(Newlabe l ,HeadA,CommonA,Res tA,HeadB,CommonB,Res tB,New2,New3) , APPENDIX D. BRUCE GENERATION 129 spawn_left_main(Head,Conimon,Rest,Newlabel,(Head3 : - Body) ) : -copy((Head,Common,Rest) , (Head2,Common2,Rest2)) , get_prev_IO(Common2,Head2,I2,02), gen_label(label,Newlabel), gen_vec(I2,New0ut), H e a d A =.. [ N a m e J n J , C a l l =. . [Newlabe l ,02 ,New0ut ] , Head3 =.. [Name,In,NewOut], l i s t _ to_body(CommonA,Xl ) , f u s e ( ( X l , C a l l ) , B o d y ) , spawn_lef t_aux(Newlabel ,HeadA,CommonA,Res tA,HeadB,CommonB,Res tB, (Head2 :— Body2),(Head3 c o p y ( ( H e a d A , C o m m o n A , R e s t A , H e a d B , C o m m o n B , R e s t B ) , (HeadA2 ,CommonA2 ,Res tA2 ,HeadB2 ,CommonB2 ,Res tB2) ) , get_prev_IO(CommonA2,HeadA2,_,OA), ge t j> revJO(CommonB2,HeadB2,_ ,OB) , ge t_prev_IO(Res tA2, (OA,OA), I2 ,02) , ge t_prev_IO(RestB2,(OB,OB), I3 ,03) , Head2 =.. [Newlabel,I2,02], Head3 =.. [Newlabel,I3,03], l is t_to_body(RestA2,Body2), l is t_to_body(RestB2,Body3), spawn_right_main(Head,Common,Rest,Newlabel,(Head2 :— Body) ) :— copy((Head,Common,Rest) , (Head2,Common2,Rest2)) , get_prev_IO (Rest 2,Head2,12,0 2), get_prev_IO(Common2,(02,02) ,I3,03) , gen_label(label,Newlabel), gen_vec(I2,NewOut), Head2 =.. [Name,In,Out], C a l l =. . [Newlabel,I2,I3], l i s t_ to_body(Common2,Xl) , f u s e ( ( C a l l , X l ) , B o d y ) , i_ spawn_r igh t_aux(Newlabe l ,HeadA,CommonA,Res tA,HeadB,CommonB,Res tB, (Head2 : - Body2) , (Head c o p y ( ( H e a d A , C o m m o n A , R e s t A , H e a d B , C o m m o n B , R e s t B ) , (HeadA2 ,CommonA2 ,Res tA2 ,HeadB2 ,CommonB2 ,Res tB2) ) , APPENDIX D. BRUCE GENERATION 130 ge t_prev_IO(Res tA2,HeadA2, IA,OA) , ge t_prev_IO(RestB2,HeadB2,IB,OB), Head2 =.. [Newlabe l , IA,OA] , Head3 =.. [Newlabel , IB,OB], l is t_to_body(RestA2,Body2) , l is t_to_body(RestB2,Body3), A p p e n d i x E P r o g r a m P r i n t i n g U t i l i t i e s % *** % *** Bruce program pretty printer % *** % ***- _ Brian J. Ross % *** Dept. of Computer Science % *** University of British Columbia % *** print_bruce(File,B) te l l ing(Old) , t e l l (F i le ) , print_bruce(B), to ld , te l l ing(Old) , I, print_bnice(Q) :— !. print bruce([A|B]) :— n l , print bruce2(A,0) , n l , print_bruce(B), I, print_bruce2( [ ] . print_bruce2( [' {' | R] ,Tab) : -Next tab is Tab + 3, 131 APPENDIX E. PROGRAM PRINTING UTILITIES w r i t e l Q ' { ' ,nl , tab(Nexttab)]) , pr int_bruce2(R,Nexttab) . pr int .br uce2( [ ' } ' , ' ; ' | R] ,Tab) : -Next tab is Tab - 3, wr i t e l ( [n l , t ab (Nex t t ab ) , ' } ; ' ,nl , tab(Nexttab)]), pr int_bruce2(R,Nexttab) . p r i n t _ b r u c e 2 ( [ ' } ' , » u n t i l ' |R] ,Tab) : -Next tab is Tab - 3, wr i te l ( [n l , tab(Next tab) , '} u n t i l ' ] ) , pr int_bruce2(R,Nexttab) . p r i n t _ b r u c e 2 ( [ ' } ' , ' } ' | R ] , T a b ) : -Next tab is Tab - 3, Next tab2 is Next tab - 3, wr i t e l ( [n l , t ab (Nex t t ab ) , ' } ' , n l , t ab (Nex t t ab2) , ' } ' ,nl, tab(Nexttab2)]), pr int_bruce2(R,Nexttab2). print_bruce2([ '>' |R] ,Tab) : -Next tab is Tab - 3, wr i t e l ( [n l , t ab (Nex t t ab ) , ' } ' ,nl, tab(Nexttab)]), pr int_bruce2(R,Nexttab) . p r in t_bruce2( [S , , ; ' |R] ,Tab) : -w r i t e l ( [ S , ' ; ' ,nl , tab(Tab)]), pr int_bruce2(R,Tab). print_bruce2([local|R],Tab) : -wri te l ( [n l , local , ' ' ] ) , pr int_bruce2(R,Tab). print_bruce2([S|R],Tab) : -wri te l ( [S, ' ' ] ) , pr int_bruce2(R,Tab). % *** % *** Prolog program pretty printer ("Peter Piper picked...") yQ *** % % printjprolog/2 prints a beautified version of P into file File. APPENDIX E. PROGRAM PRINTING UTILITIES 133 % It calls print_prolog/1 to do the actual printing. print_prolog(File ,P) :— te l l ing(Old) , te l l (F i le ) , print_prolog(P), to ld , te l l ing(Old) , print_prolog(P) :— copy(P ,Q) , print_prolog2(Q), print_prolog2([]). print_prolog2([A|B]) : -print clause(A), n l , print_prolog2(B). % print_clause(C) beautifies clause C, and then writes it. print_clause([]). print_clause(C) :— beautify ( C ) , C =. . [ ( : - ) | [Head|Body]] , wr i te l (Head , ' : - ' , n l ) , print_goals(Body). print_clause(C) :— w r i t e l ( C , ' . »,nl). % print_goals(G) prints the goals in list G, 1 per line. print_goals([]). print_goals([(A,B)|R]) : -APPENDIX E. PROGRAM PRINTING UTILITIES print_goals([A,B|R]). print_goals([G]) :— tab(5), writel(G,'. »,nl). print_goals([G|R]) : -tab(5), writel(G,' , ' ,nl), print_goals(R). % % beautify(C) sets all the logical variables in clause C to atoms which % represent their Bruce names, which were saved during parsing. % The name numbering is reset each time beautify is invoked. beautify((H:-B)) : -H =.. [Name|Args], nnd_names(Name,Vnames), reset_name_numbering, args_to_list(B,Goals), set_names( [H | Goals], Vnames), beautify (_). % % set_names(Goallist,Varnames) sets the logical variables in the list of goals % to their corr. names in Varnames. % Temporary variables found in 'callasgn' goals are names "tmp". % Goals which represent subprogram calls are skipped (vars are set elsewhere). % Otherwise, each list in a goal's argument list, which is an 10 vector, % is processed. set_names ([],_). set_names([callasgn(_,X,_)|Rest],Vnames) :— set_name( X ,tmp), set_names(Rest,Vnames). set_names([A|Rest],Vnames) :— A =..[Name|_], storematch(Name,Vnames2,_,_,_), APPENDIX E. PROGRAM PRINTING UTILITIES 135 Vnames2 \== Vnames, set_names( Rest, Vnames). set_names([A|Rest],Vnames) : -A =.. U A r g s l . save_lists(Args,Vecs), set_vec_names (Vecs, Vnames), set_names(Rest,Vnames). set_names([_|Rest],Vnames) : -set_names (Rest, Vnames). % % save_lists(L, Vecs) saves each list argument in list L into Vecs. save_lists([],[]). save_lists([A|B],Vecs) :— var (A) , save_lists(B ,Vecs). save_lists([A|B],[A|Vecs]) : -functor ( A , ' .',_)> save_lists(B,Vecs). save_lists([_|B],Vecs) :— save_lists(B ,Vecs). % % find_names(Name,Varnames) finds out what type of mechanism Name represents % and returns the appropriate variable name list. nnd_names(Name,Vnames) :— storematch(Name,Vnames,_,_,_). nnd_names(Name,Vnames) :— labellist(N,L^), member(Name,L), storematch(N, Vnames M _,_). % % set_vec_names(Varlist,Namelist) sets the logical variables in each vector in APPENDIX E. PROGRAM PRINTING UTILITIES % Veclist to atoms. set_vec_names2(Vec,Namelist) sets each logical variable in % Vec to an atom created from the corr. Bruce variable Namelist. set_vec_names( _ _ ) . set_vec_nam.es([V|Rest],Vnames) :— set_vec_names2(V,Vnames), set_vec_names(Rest,Vnames). set_vec_names2([] _). set_vec_names2([V|R],[N|S]) : -set_name(V,N), set_vec_names2(R,S). % % set_name(V,Name) unifies logical variable V to an atom representing the % Prolog variable name. The atom is based on the Bruce variable name Name. % A counter is kept for each variable name, which is updated for each % successful unification. set_name(V,Name) :— not v a r ( V ) , !, set_name(V,Name) :— retract(save_no(Name,Num)), Next is N u m + 1, atom_append(Name,Next ,New), capi tol ize(New,Newname), V = Newname, t assert (save_no( N ame ,Next)) , set_name(V,Name) :— atom_append(Name, l ,New), capitolize( New ,Newname), V = Newname, t assert (s ave_no( N ame, 1)). % % Reset the variable counters... APPENDIX E. PROGRAM PRINTING UTILITIES 137 reset_name_numbering :— abolish(save_no,2). reset_name_numbering. Appendix F M i s c e l l a n e o u s C o d e % *** % *** Main driver % *** % *** _ Brian J. Ross % *** Dept. of Computer Science % *** University of British Columbia y0 *** mixbruce(File,Call) :— translate(File,Prolog), mixcall(File,Call), I, mixcall(File,Call) :— writel('* Mixing program . . . *',nl), mix(Call,Mixed), atom_append(File,' .pmix' ,PFile), writel('* Mixing complete (see "^PFile,"1) *',nl), print prolog(PFile,Mixed), % brucify (Mixed ,B r uce), atom_append(File,'.bmix' ,BFile), writel('* Bruce generated (see "'jBFile,'") *',nl), print_bruce(BFile,Bruce), writel(nl,'* DONE. *',nl), I. 138 APPENDIX F. MISCELLANEOUS CODE mixpro log(F i le ,Ca l l ) :— w r i t e l ( ' * Read ing P r o l o g i n 1 1 ' , F i l e , ' " * ' , n l ) , [File], % mixca l l (Ca l l ) , parse(File) :— translate(Fi le ,Prolog) , w r i t e l ( n l , ' * DONE. * ' , n l ) , I. t ranslate(File ,Prolog) : -start_up, alt_read_file (F i le , D at a), w r i t e l ( ' * " ' , F i l e , ' " r e a d * \ n l ) , % l ex ica l (Lex ,Data) , w r i t e l ( ' * L e x i c a l succeeds * ' , n l ) , % env(Tree,Lex,[]), w r i t e l ( ' * P a r s e succeeds * ' , n l ) , % pretty (Tree), % gen_prolog(File,Tree, Prolog) , a t o m _ a p p e n d ( F i l e , ' . p r o ' , P F i l e ) , w r i t e l ( ' * P r o l o g g e n e r a t e d (see ' " j P F i l e , " ' ) * ' , n l ) , print_prolog( P F i l e ,Prolog), assert_prolog(Prolog), % bruci fy(Prolog ,B) , a tom_append(File , ' . b r u ' , B F i l e ) , w r i t e l ( ' * B ruce g e n e r a t e d (see " » , B F i l e , ' " ) * ' , n l ) , p r in t_bruce(BFi le ,B) , % lexical(Lex,Data) converts the characters Data into lexical tokens % in Lex. l ex ica l (Lex ,Data) :— lex(Lex,_,Data,[]). APPENDIX F. MISCELLANEOUS CODE 140 % some cleaning up... s t a r t j i p :— tabolish, reset_gen_nums, gen_prolog(File,Tree,Prolog) :— Tree" "code(Code), flatten(Code,Prol), writel('* Basic semantics created *',nl), atom_append(File,'. bas' ,BFile), writel('* . . . (see "',BFile,'") *',nl), print_prolog( B File,Prol), (found_a_branch — > gen_labelprogs(Prol,Pro2), writel('* Label programs created *',nl), atom_append(File,' . lab' ,LFile) , writel('* . . . (see "' ,LFile, '") *',nl), print_prolog(LFile,Pro2), % process_branches(Pro2,Prolog), writel('* Branches processed *',nl) Prolog = Prol), % *** % *** Prolog dataflow checking utilities % *** % % order(Goals,A,B) is satisfied if B is dependent on A wrt data flow % One of five tests is performed to determine dataflow ordering: % (a) B's input matches A's output — succeeds. % (b) A's input matches B's output — failure. % (c) variables in test B are a subset of mechanism A's output — succeed. % (d) like (c), but A and B reversed % (e) No direct correlation with A and B, so the list of remaining goals % is used for a recursive dataflow check. APPENDIX F. MISCELLANEOUS CODE 141 order (Goa l s ,A ,B) :— v a r s _ u s e d ( A , V A I , V A O ) , v a r s _ u s e d ( B , V B I , V B O ) , V A O = = V B I , o rde r (Goa l s ,A ,B) :— v a r s u s e d ( A , V A I , V A O ) , v a r s _ u s e d ( B , V B I , V B O ) , V A I = = V B O , i fail. order (Goa l s ,A ,B) :— is_a_test(B), ex t rac t_vars (B,VB) , v a r s _ u s e d ( A , V A I , V A O ) , s u b s e t ( V B , V A O ) , !, order (Goa l s ,A ,B) :— is_a_test(A), ex t rac t_vars (A,VA) , v a r s _ u s e d ( B , V B I , V B O ) , s u b s e t ( V A , V B O ) , I faU. o rde r (Goa l s ,A ,B) :— remove_items([A,B],Goals,G2), member2(C,G2) , remove_i tem(C,G2,G3), o r d e r ( G 3 , A , C ) , o r d e r ( G 3 , C , B ) , % % dep_in_vars(A,B) succeeds if the (input) variables in A are dependent % or a subset of the input variables in B. dep_in_vars(Test,B) :— is_a_test(Test), extract_vars(Test ,TV), vars_used (B ,In,_), subset (TV,In) , APPENDIX F. MISCELLANEOUS CODE 142 dep_in_vars(A,B) :— vars_used(A,InA,_), vars_used(B ,InB,_), subset ( InA,InB) , % % dep_out_vars(A,B) succeeds if the (input) variables in A are dependent % or a subset of the output variables in B. dep_out_vars(Test,B) :— is_a_test(Test), extract_vars(Test ,TV), vars_used(B,_,Out), subse t (TV,Out ) , dep_in_vars(A,B) :— vars_used(A,InA,_), vars_used(B,_,OutB), subse t ( InA,OutB) , I % % same_out_vars(A,B) succeeds if A and B have the same output variables. same_out_vars(A,B) :— vars_used(A,_,OutA), vars_used(B ,_ ,OutB) , O u t A = = O u t B , i % % order_clause_goals(L,S) orders goals in L, resulting in S. order_clause_goals(L,S) :— insor t (L ,S) . % % from Clocksin & Mellish, pp.146 ... insort(0,D) - !• i n so r t ( [X |L ] ,M) : -APPENDIX F. MISCELLANEOUS CODE 143 nsort(L,N), insortx(X,N,M), insortx(X,[A|L],[A|M]) : -order([A|L],A,X), ! •? insortx(X,L,M). insortx(X,L,[X|L]). % *** % *** some variable vector utilities % *** % % gen_vec(A,B) creates a list of 'fresh' variables of the same size as list A. gen_vec([],[]). gen_vec([Name|A],[New|B]) : -gen_vec(A,B)-% % var_match(Name,Input,Var) matches variable Name with the variable names % in storematch for the current program. The corresponding logical variable % in Input is returned in Var. var_match(Name,Input,Var) :— curr_prog(Prog), storemat ch( P rog, Var s,_,_,_), append(A,[Name|B],Vars), count(A,S), T is S + 1, nmember(T,Input,Var), I. % % A variant of Initial is created, in which Var_i is replaced by Var_f. vec_variant(Initial,Varj ,Var_f,Final) :— break(Var_i,A,[B|C] .Initial), append(A,[Var_f|C],Final), i APPENDIX F. MISCELLANEOUS CODE 144 % ; % match_vars(A,B,C) matches variable names in A with their logical % variable values, as are listed in B, resulting in C. match_vars( [],_, _ ) . match_vars([A|L],Input ,[V|R]) :— var_mat ch ( A ,Input, V ) , match_vars(L,Input ,R). 7o % set_outputs(Vars,In,Out,Ans) matches each variable in Vars % with its corresponding output variable, as determined by In and Out. set_outputs( [],_,_,[]). set_outputs([Var|A],In,Out,[Outvar|D]) :— set_output(Var,In,Out,Outvar) , set_outputs(A,In,Out ,D). set_output(Var,__.,Var). set_output(Var,[I |A],[0 |B],Ans) : -(Var = = I - > A n s = O; set_out put (Var , A , B , Ans ) ) . % *** % *** List utilities % *** % % program_separate(Env,Labels,Collect,Prolog) separates predicates into % the sections used by the original Bruce source programs. % The Labels list these predicate names. program_separate(Env,[],Prolog,Prolog). program_separate(Env,[[Prog|Labels] |Rest],Collect,Prolog) :— get_pgms(Env,[Prog|Labels],Some), (Some = = [] - > program_separate(Env,Rest,Collect ,Prolog) program_separate(Env,Rest,[Prog,Some|Collect],Prolog)). % APPENDIX F. MISCELLANEOUS CODE % get_pgms(Env,Labels, Collect,Result) collects all the clauses in Env % which are listed in Labels list. get_pgms(Env,[],[]). get_pgms(Env,[Label |Rest] ,A) : -get_label_refs(Env,Label,[] ,Refs), (Refs = = Q - > get_pgms(Env ,Rest, A ) i get_pgms ( E n v ,Rest , B ) , append(Refs ,B,A)) . % _ % getjabeljrefs(Env, Label, Collect,Result) collects all the clauses in Env % named by Label. get jab el_refs( [] , L abel ,Refs ,Refs). get_label_refs([(Head : - Body) |Rest] ,Label ,Col lect ,Refs) :— i •> . (functor(Head,Label,_) — > get_label_refs(Rest,Label,[(Head : - Body) |Collect] ,Refs) i get jab el_refs (Rest ,L abel, Collect ,Refs)). getJabel_refs([Clause|Rest],Label,Collect,Refs) :— i •> (functor(Clause,Label,_) —> get Jabel_refs(Rest, Labe l , [Clause| Collect],Refs) ge t jab el_refs (Res t ,L abel,Collect , Refs)). f0 *** % *** Miscellaneous Prolog utilities... % *** % % member routine in which the Items may be uninstantiated % (logical variable matching). member(_,[|) : - !,fail. member(I tem,[X|J) :— Item = = X . member(Ans,[_|Rest]) : -APPENDIX F. MISCELLANEOUS CODE 146 member(Ans,Rest). % member2 doesn't handle logical variable objects. member2(Item,[Item |_]). member2(Ans,[_|Rest]) :— member2(Ans,Rest). % memberS tests if the ground parts of terms are equivalent. % (corresponding variables may be different) member3(Goal,[]) : - !,fail. member3(Goal,[Item|_]) :— ground_eq(Goal,Item). member3(Goal,L|R]) : -member3(Goal,R). % \ % ground_eq(A,B) tests if the ground portions of A and B are equivalent. % In other words, terms A and B must be equal, except that variables may be % renamed. ground_eq(A,B) :— var(A), var(B), ground_eq(A,B) :— (var(A) ; var(B)), I fail. ground_eq(A,B) :— A == B, I, ground_eq([Al|A2],[Bl|B2]) : -i ground_eq(Al,Bl), ground_eq(A2,B2). ground_eq(A,B) APPENDIX F. MISCELLANEOUS CODE 147 ! •) A =. . [Name |ArgsA] , B =. . [Name|ArgsB] , g round_eq(ArgsA,ArgsB) . % atomjappend appends atom names together. a tom_append(Atoml ,Atom2,Newatom) : -n a m e ( A t o m l , A ) , name(Atom2,B)> a p p e n d ( A , B , C ) , name(Newatom,C) , i % % Count the number of elements in a list count(Q,0) : - !. count(L |L],N) : -c o u n t ( L , M ) , N is M + 1, % % nmember(N,L,I) retrieves the Nth element I of list L nmember(Num,Lis t , I tem) :— nmember( 1 ,Num,Li s t ,Item), I. nmember(N,N,[Item|_],Item). nmember(Curr,Num,L |Rest] ,Ans) :— Next is C u r r + 1, nmember (Next ,Num,Res t ,Ans) . % % break(Item,Front,End,List) breaks List up into Front and End, such % that Item is the first item in End. break(Item,[],[A|B],[A|B]) : -Item = = A . break(I tem,[B|R] ,E, [B|C]) : -APPENDIX F. MISCELLANEOUS CODE 148 I tem \ = = B , b reak( I t em,R,E ,C) . % args_to_list(A,B) converts the argument structure A to a list B. args_to_list(A,[A]) :— v a r ( A ) , args_to_l is t (A,Tl) : -A =. . [ V , X , A 1 ] , args_ to_ l i s t (X,Xl ) , args_to_l is t (Al ,T) , a p p e n d ( X l , T , T l ) , args_to_list(A,[A]) :— !. % fuse a multi— layered goal list into one flat goal list. fuse((A,true) ,B) : -fuse (A,B) , fuse(( true,A),B) :— fuse(A,B)> f u s e ( ( " , " ) , " ) : - !. f u s e ( ( A , " ) , E ) : -fuse(A,E) , f u s e ( ( " , A ) , E ) : -fuse(A,E) , f u s e ( ( ( " , B ) , C ) , E ) : -fuse( (B,C) ,E) , fuse ( ( (A ,B) ,C) , (D ,E) ) : -fuse(A,D) , fuse( (B,C) ,E) , fuse ( (A,B) , (D,E) ) : -fuse(A,D) , APPENDIX F. MISCELLANEOUS CODE fuse(B,E) , fuse(E,E) . % % get the input and output vectors for an ORDERED list of goals. ge t_ IO( (H: -B) , In ,Out ) : -I •> var s_used ( H ,In , 0 ut ) . get_IO(Goall ist , In,Out) : -member2(First,Goallist), vars_used(First,In,_), rev(Goal l i s t ,Rev) , member2(Last,Rev), vars_used(Last,_,Out), i % % get_prev_IO(Goals,Prev,In,Out) determines the In and Out vectors % for the list of Goals. Should Goals be composed of calls which do not % have intrinsic 10 vectors, the 10 vectors of Prev are returned instead. get_prev_I0(Goals,_,In,Out) :— get_IO(Goals,In,Out) , get_prev_I0(_,Prev,In,0ut) :— get_I0([Prev],In,0ut) , % % get a term's input and output variable vectors ... vars_used(A,_,_) :— is_a_test(A), ! ? fai l . vars_used(A,In,Out) :— A =. . [_,ln,0ut], vars_used(asgn(In,_^.,0ut),ln,0ut) :— APPENDIX F. MISCELLANEOUS CODE varsjised(goto(In,_,Out),In,Out) :— % % extract_vars(V,A) removes all the variables used in V into list A, % without duplicates. extract_vars(V,A) :— extract_vars(V,[],A), I extract_vars(V,Col lect ,A) :— v a r ( V ) , (member(V,Col lec t ) - > A = Collect A = [V | Collect]) . ex t rac t_vars (X,A,A) :— ( X = = [] ; a tom(X) ) . extract_vars([V|R],Collect ,A) : -extract_vars(V,Collect , X ) , ext ract_vars( R , X , A ) . extract va r s (X ,Co l l ec t ,A) :— X =.. UL], extract_vars(L,Col lect ,A) . % test if a term is an expression (namely, a boolean test) ... is_a_test(Thing) :— functor(Thing,Name,_), name(Name,Str ing) , (op_chars(String,bool(_));op_chars(String,rel(_))), is_a_test(Thing) : -member(Thing,[true,false]), % : % test if two expressions are complementary APPENDIX F. MISCELLANEOUS CODE 151 complementa ry(A,B) : - not (not (A =. . [ '~ ' ,B] ) ) -complementa ry(A,B) : - not(not(B =.. [ '"" ' ,A])) . % % remove_item(Item,List,Newlist) removes the first instance of Item in List, % resulting in Newlist. remove_item(_,[|,[|) :— !. remove_item(Item,[Item|X],X) :— remove_item(Item,[X|Y] ,[X|Ans2]) : -remove_item(Item,Y,Ans2), !. % % remove_item2(Item,List,Newlist) removes the first instance of Item in List, % resulting in Newlist. It differs from removejtem in that no unification % is done when matching items. remove_item2(_,Q,Q) :— !. remove_item2(ItemA,[ItemB|X],X) :— Item A = = I temB, ; # remove_item2(Item,[X|Y],[X|Ans2]) : -removeJtem2(Item,Y,Ans2), % split the clause into its Head, and a list of the goals in the Body. split_clause((Head :— Body) ,Head ,Bodyl i s t ) args_to_list(Body,Bodylist) , i % % Copy structure A into B, so that it has unique variables c o p y ( A , B ) : -assert(copied(A)), retract(copied(B)), I APPENDIX F. MISCELLANEOUS CODE % % flatten a multi—layered list into a one—dimension list. flatten(Q,Q) :- !. flatten([[]|A],B) : -flatten(A,B), I, flatten([[A|B]|C],D) : -flatten([A|[B|C]],D), flatten([A|B],[A|C)) : -A \ = = Q, A \== LU, flatten(B,C), | # % % permutation(A,B) checks if the items in list A are a variation of those % in list B, in terms of ordering. permutation(Q,[|). permutation([A|B],C) :— C \ = = [], remove_item(A,C,D), p e r m u t a t i o n ( B , D ) , i , % % append2 is a deterministic append. append2([],L,L) :— !. append2([X|R],L,[X|Rl]) : - append2(R,L,Rl). % % append_list(L,R) appends the lists found in list L together, resulting % in R. append_list([],[]) :— !. append_list([A],A) :— !. append_list([A,[]],A) : - !. append_list([A,B|C],D) : -a p p e n d ( A , B ) E ) , APPENDIX F. MISCELLANEOUS CODE 153 append_lis t([E|C],D), % % subset(A,B) succeeds if the elements in A are all in B. subset( []_,). subset([X|R],U) : -m e m b e r ( X , U ) , subse t (R,U) , I, % ; % remove_items(A,B,C) removes the items in list A from list B, resulting in C. remove_iteiris( [], A , A ) . remove_items([A|B],C,D) :— remove_i tem(A,C,E) , r e m o v e j t e m s ( B , E , D ) , I. % % remove_items2(A,B,C) removes the items in list A from list B, resulting in C. % Unlike removejtems, no unification is done when item matching. remove_items2([],A,A). remove_items2([A|B],C,D) :— remove_item2(A,C,E), remove_items2(B,E,D), !_ % % writeJist(Direction, Write,List) writes the List in the desired % direction(vert,horz), using the goven write routine Write. write_list(__.,[]) : - !. wri te_l is t (ver t ,Wri teRtn, [A|B]) : -W r i t e =. . [Wr i t eRtn ,A] , W r i t e , n l , wri te_l is t (ver t ,Wri teRtr i ,B) , I. write_lis t(horz,WriteRtn,[A]) :— APPENDIX F. MISCELLANEOUS CODE 154 i •> W r i t e =. . [Wr i t eRtn ,A] , W r i t e . wr i t e j i s t (horz ,Wr i t eRtn , [A | B]) : -Wr i t e =. . [Wr i t eRtn ,A] , W r i t e , w r i t e ( ' , ' ) , wr i t e j i s t (horz ,Wr i t eR tn , B ) . % % convert a list of goals to a body of goals l is t_to_body([] ,") : - !. list_to_body([A],A) : - !. l i s t_to_body([A|C], (A,D)) : -l is t_to_body(C,D), i % % duo_split(Side,LI,Leftl,Rightl,L2,Lefts,Right2) splits Ll and L2 into % equal size, non-null parts, depending if Side is 'left' or 'right'. duo_sp l i t ( r igh t ,L l ,Le f t l ,R igh t l ,L2 ,Lef t2 ,R igh t2 ) : -append( Left 1 ,Right 1 ,L 1), L e f t l \ = = [], R i g h t l \ = = [], c o u n t ( R i g h t l , N ) , append(Left2 ,Right2,L2) , count (Right2 ,N) . duo_split(left,L 1 ,Le f t l ,R igh t 1 ,L2,Left2,Right2) : -r e v ( L l , R L l ) , r e v ( L 2 , R L 2 ) , a p p e n d ( R L e f t l , R R i g h t l , R L l ) , R L e f t l \ = = Q, R R i g h t l \ = = [], c o u n t ( R R i g h t l , N ) , append(RLef t2 ,RRigh t2 ,RL2) , coun t (RRigh t2 ,N) , r e v ( R L e f t l , R i g h t l ) , rev(RLef t2 ,Right2) , APPENDIX F. MISCELLANEOUS CODE r e v ( R R i g h t l , L e f t l ) , rev(RRight2 ,Lef t2) . % % list reverser... r e v ( X , R X ) : -revx(X, [ ] ,RX) , ! . r evx(Q,R,R) : -r e v x ( [ X | Y ] , Z , R ) : -r e v x ( Y , [ X | Z ] , R ) . % % find_clause(Prolog,Head, Clause) finds a clause in Prolog with head Head. % Repeated calls return new results. find_clause(Prolog,Head,Clause) :— member2(Clause,Prolog), split_clause( Clause,Head2 ^ ) , not not Head = Head2. % % find_goal(Clause,Head,Left,Goal,Right) finds Goal within the body of % Clause. Left and Right are the goals on each side of the goal. fmd_goal(Clause,Head,Left ,Goal,Right) :— split_clause(Clause,Head,Goals), append(Left , [Goal |Right] , Goals) , !, % % make_clause (Head, Left, Right, Clause) appends lists Left and Right together, % converts them into a body structure, and forms a clause with head Head. % Note: There must already exists proper input—output between the constructs make_clause(Head,[],[],Head). make_clause(Head,Left,[],(Head : - Body) ) :— list_to_body (Lef t ,Body) . APPENDIX F. MISCELLANEOUS CODE 1 5 6 make_clause(Head,[],Right,(Head : - Body) ) :— l is t_to_body(Right ,Body). make_clause(Head,Left,Right,(Head :— Body) ) :— app end( Left ,Right , Goals) , l is t_to_body(Goals ,Body). % % mergejjoalsflA^AfAJB^B^JnfOu^G) appends goal lists A and B into G, % while assuring that the 10 of the two lists is merged. In and Out contain % the 10 of the result. merge_goals(_,_,Q_.,_,0,_,_,[]) :- !. merge_goals(_,_,_,IA,OA,A,In,Out ,G) :— c o p y ( ( I A , O A , A ) , ( I n , O u t , G ) ) , i_ merge_goals(IA,OA,A^_.,0,In,Out,G) :— c o p y ( ( I A , O A , A ) , ( I n , O u t , G ) ) , I. m e r g e _ g o a l s ( I A , O A , A , I B , O B , B , I n , O u t , G ) : -c o p y ( ( I A , O A , A , I B , O B , B ) , ( I n , O A 2 , A 2 , I B 2 , O u t , B 2 ) ) , O A 2 = I B 2 , a p p e n d ( A 2 , B 2 , G ) , I, % % append_goals(Clause,Vec,Code,Newclause) adds the goals in Code to the goals % of Clause, resulting in Newclause. append_goals(Clause,Vec,Code,(Newhead :— Body) ) :— copy((Clause,Vec,Code),(Clause2,Vec2,Code2)) , split_clause(Clause2,Head,Goals), Head =.. [ N a m e , I l , O l ] , get_prev_IO(Goals,(I l , I l) , I2,Vec2), append(Goals ,Code2,G) , get_IO(G,I3,03) , Newhead =.. [Name, I l ,03] , l i s t_ to_body(G,Body) , APPENDIX F. MISCELLANEOUS CODE % : % parent_clause(Prolog,Head,Parent,Phead,Left,Goal,Right): % Prolog — current prolog environment % Head — clause to find a parent for % Parent — the found parent clause % Phead, Left, Goal, Right — the breaking up of Parent such that % Phead is the head, Goal is the call to Head, and Left/Right % are goals to the left and right of Goal % % A parent clause is found. Recursive calls are not used — a clause cannot % be its own parent. parent_clause(Prolog,Head,Paxent,Phead,Left ,Goal,Right) :— copy (Head, Goa l ) , member 2 (P arent ,P rolog), spli t_clause(Parent,Phead,Goals), not Phead = Head , append(Left , [Goal |Right] ,Goals) . % sibling_clause (Prolog, Clause, Sibling) finds a sibling for Clause from Prolog. sibling_clause(Prolog,Clause,Sibling) :— split_clause(Clause,Head,_), copy(Head,I tem), member2(Sibling,Prolog), split_clause(Sibling,Item,_), S ib l ing \ = = Clause. % % assertjprolog(P) tasserts all the code in list P. assert_prolog(_) : - !. assert_prolog([Clause|Rest]) :— tassertz(Clause), assert_prolog(Rest), |# % % Make an atom like Name into one which is capitolized. APPENDIX F. MISCELLANEOUS CODE 158 capi tol ize(Name,Caps) :— name(Name,[A|L]) , A > = 97, A = < 122, A 2 is A - 32, name(Caps , [A2|L]) , capi tol ize(Name,Name). % % Read: (written by Doug Westcott) % % The following routines allow the reading of a file's contents into % prolog in the form of a list of characters' ASCII numbers (the usual % prolog representation of a string). % alt_read_file(File,Contents) :— read_file(File,Contentsl) , reduce_white_space( Content s 1 ,Contents), I, read_file(File,Contents) :— seeing(OldFile) , see(File), getO(Char), read_fi lel(Char,Q,RContents) , seen, seeing(OldFile) , reverse(RContents,Contents) , !. read_nlel(Char,Sofar,Sofar) :— end_of_file(Char), I, read_filel(Char,Sofar,Contents) :— getO(Newchar), read_filel(Newchar,[Char|Sofar],Con tents), i APPENDIX F. MISCELLANEOUS CODE 159 e n d p f f i l e ( - l ) : -?. reduce_white_space(01d,New) :— change_to_spaces(01d,Mid), reduce_spaces(Mid,New), ; # change_to_spaces([Char|Chars],[NewChar|NewChars]) : -change_to_space(Char,NewChar), l •, change_to_spaces(Chars,NewChars), I. change_to_spaces([],[]) :— I. change_to_space(09,32). changeJo_space(10,32). change_to_space( 11,32). change_to_space( 12,32). change_to_space(X,X). reduce_spaces([32,321Chars],NewChars) : -reduce_spaces([32|Chars],NewChars), reduce_spaces([Char|Chars],[Char|NewChars]) :— reduce_spaces(Chars,NewChars), reduce_spaces([],[]) :— % *** % *** Tagged assertion utilities % *** % % tassert routines assert clauses, plus update a tag to be used for % later removal. tassert(Clause) :— set_rem_clause( Clause), assert(Clause), APPENDIX F. MISCELLANEOUS CODE I. tasserta(Clause) :— set_rem_clause( Clause), asserta( Clause), tassertz(Clause) :— set_rem_clause( Clause), assertz(Clause), % ; % set rem_clause tag. If predicate exists already before a tag has been set, % then do not set a remove tag, as this predicate is used elsewhere. set_rem_clause((Head :— Goals)) :— functor (Head,Name,Ar i ty) , set_rem_clause2(Name,Arity), set_rem_clause( Clause) :— functor (Clause ,Name,Ari ty) , set_rem_clause2(Name,Arity), set_rem_clause2(Name,Arity) :— rem_clause(Name,Ari ty) , I. set_rem_clause2(Name,Arity) :— current_predicate(Name,Head), func tor (Head,Name,Ar i ty) , set_rem_clause2(Name,Arity) :— i assertz(rem_clause(Name,Arity)). % % remove a predicate asserted with tassert utility t abo l i sh(Pred ,Ar i ty ) :— rem_clause(Pred,Ari ty) , abo l i sh (Pred ,Ar i ty ) , retract(rem_clause(Pred,Arity)) . tabolish(_,_). APPENDIX F. MISCELLANEOUS CODE 161 % remove all clauses asserted by tassert utilities tabolish :— rem_clause(Name,Ari ty) , abo l i sh (Name,Ar i ty ) , fa i l , tabolish :— abolish(rem_clause,2). % list writing routine (written by Doug Westcott) writel([A|B]) : -wri te_i tem(A), wr i t e l (B) , writel(Q) : -wr i t e l (A) :— writel([A]), 1. w r i t e l ( A , B ) : -wr i te l ( [A,B]) , !. w r i t e l ( A , B , C ) : -wr i t e l ( [A ,B ,C] ) , j . w r i t e l ( A , B , C , D ) : -w r i t e l ( [ A , B , C , D ] ) , w r i t e l ( A , B , C , D , E ) : -w r i t e l ( [ A , B , C , D , E ] ) , ; # w r i t e l ( A , B , C , D , E , F ) : -w r i t e l ( [ A , B , C , D , E , F ] ) , w r i t e l ( A , B , C , D , E , F , G ) : -w r i t e l ( [ A , B , C , D , E , F , G ] ) , APPENDIX F. MISCELLANEOUS CODE 162 w r i t e l ( A , B , C , D , E , F , G , H ) : -w r i t e l ( [ A , B , C , D , E , F , G , H ] ) , w r i t e l ( A , B , C , D , E , F , G , H , I ) : -w r i t e l ( [ A , B , C , D , E , F , G , H , I ] ) , !. w r i t e l ( A , B , C , D , E , F , G , H , I , J ) : -w r i t e l ( [ A , B , C , D , E , F , G , H , I , J ] ) , i , w r i t e j t e m ( X ) :— v a r ( X ) , w r i t e ( X ) , write i tem(nl) :— n l , write_item(tab(N)) :— tab (N) , write_item(X) :— w r i t e ( X ) , Appendix G B i n a r y G C D B a s i c S e m a n t i c s b i n g c d ( [ G c d l , U l , V l ] , [ G c d 2 , U 2 , V 2 ] ) : -a s g n ( [ G c d l , U l , V l , K l , P l , T l ] , K 2 , 0 , [ G c d l , U l , V l , K 2 , P l , T l ] ) , t e s t l ( [ G c d l , U l , V l , K 2 , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 3 , P 2 , T 2 ] ) . t e s t l ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -U 1 / / 2 * 2 = \ = U 1 , b 2 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . t e s t l ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -" U 1 / / 2 * 2 = \ = U 1 , t e s t 2 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . t e s t 2 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -V 1 / / 2 * 2 = \ = V 1 , b 2 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . t e s t 2 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -~ V 1 / / 2 * 2 = \ = V 1 , a s g n ( [ G c d l , U l , V l , K l , P l , T l ] , K 3 , K l + l , [ G c d l , U l , V l , K 3 , P l , T l ] ) , a s g n ( [ G c d l , U l , V l , K 3 , P l , T l ] , U 3 , U l / / 2 , [ G c d l , U 3 , V l , K 3 , P l , T l ] ) , a s g n Q G c d l . U S ^ L K S ^ L T l i v s . V l / ^ i G c d L U S . V S ^ S . P l . T l ] ) , b l ( [ G c d l , U 3 , V 3 , K 3 , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . t e s t 3 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -U l / / 2 * 2 = \ = U 1 , a s g n ( [ G c d l , U l , V l , K l , P l , T l ] , T 3 , 0 - V l , [ G c d l , U l , V l , K l , P l , T 3 ] ) , b 4 ( [ G c d l , U l , V l , K l , P l , T 3 ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . 163 APPENDIX G. BINARY GCD BASIC SEMANTICS 164 t e s t 3 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -- U 1 / / 2 * 2 = \ = U 1 , a s g n ( [ G c d l , U l , V l , K l , P l , T l ] , T 3 , U l , [ G c d l , U l , V l , K l , P l , T 3 ] ) , a s g n ( [ G c d l , U l , V l , K l , P l , T 3 ] , T 4 , T 3 / / 2 , [ G c d l , U l , V l , K l , P l , T 4 ] ) , t e s t 4 ( [ G c d l , U l , V l ) K l , P l , T 4 ] , [ G c d 2 ) U 2 , V 2 , K 2 , P 2 , T 2 ] ) . t e s t 4 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -T 1 / / 2 * 2 = : = T 1 , b 3 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . t e s t 4 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -• T 1 / / 2 * 2 = : = T 1 , t e s t 5 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 3 , U 3 , V 3 , K 3 , P 3 , T 3 ] ) , a s g n ( [ G c d 3 , U 3 , V 3 , K 3 , P 3 , T 3 ] , T 4 , U 3 - V 3 , [ G c d 3 , U 3 , V 3 , K 3 , P 3 , T 4 ] ) , t e s t6 ( [Gcd3 ,U3 ,V3 ,K3 ,P3 ,T4] , [Gcd2 ,U2 ,V2 ,K2 ,P2 ,T2] ) . t e s t 5 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d l , U 2 , V l , K l , P l , T l ] ) : -T 1 > 0 , a s g n ( [ G c d l , U l , V l , K l , P l , T l ] , U 2 , T l , [ G c d l , U 2 , V l , K l , P l , T l ] ) . t e s t 5 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d l , U l , V 2 , K l , P l , T l ] ) : -~T1>0, a s g n ( [ G c d l , U l , V l , K l , P l , T l ] , V 2 , 0 - T l , [ G c d l , U l , V 2 , K l , P l , T l ] ) . t e s t 6 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -T 1 = \ = 0 , b 3 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . t e s t 6 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U l , V l , K 2 , P 2 , T l ] ) : -~ T 1 = \ = 0 , a s g n ( [ G c d l , U l , V l , K l , P l , T l ] , K 2 , K l , [ G c d l , U l , V l , K 2 , P l , T l ] ) , c a l l a s g n ( [ G c d l , U l , V l , K 2 , P l , T l ] , T m p l , 2 ) , c a l l a s g n ( [ G c d l , U l , V l , K 2 , P l , T l ] , T m p 2 , K 2 ) , power([Pl,Tmpl,Tmp2],[P2 % .137447,_137448]), a s g n ( [ G c d l , U l , V l , K 2 , P 2 , T l ] , G c d 2 , U l * P 2 , [ G c d 2 , U l , V l , K 2 , P 2 , T l ] ) . b l ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) t e s t l ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . b 2 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -t e s t 3 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . APPENDIX G. BINARY GCD BASIC SEMANTICS b 3 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -a s g n C f G c d l ^ ^ V ^ K l . P ^ T l J . T S ^ l / ^ ^ G c d ^ U l . V l . K ^ P l . T a ] ) , t e s t 4 ( [ G c d l , U l , V l , K l , P l , T 3 ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . b 4 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -t e s t 4 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . Appendix H P a r t i a l l y E v a l u a t e d B i n a r y G C D S e m a n t i c s b ingcd( [Gcd l ,7 ,Vl ] , [Gcd2 ,U2 ,V2] ) : -a s g n ( [ G c d l , 7 , V l , 0 , P l , T l ] , T 3 , 0 - V l , [ G c d l , 7 , V l , 0 , P l , T 3 ] ) , b 4 ( [ G c d l , 7 , V l , 0 , P l , T 3 ] , [ G c d 2 , U 2 , V 2 , D 7 , P 2 , T 2 ] ) . t e s t 4 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -T 1 / / 2 * 2 = : = T 1 , b 3 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . t e s t 4 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -~ T 1 / / 2 * 2 = : = T 1 , t e s t 5 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 3 , U 3 , V 3 , K 4 , P 4 , T 3 ] ) , a s g n ( [ G c d 3 , U 3 , V 3 , K 3 , P 3 , T 3 ] , T 3 , U 3 - V 3 , [ G c d 3 , U 3 , V 3 , K 3 , P 3 , T 4 ] ) , t e s t6 ( [Gcd3 ,U3 ,V3 ,K3 ,P3 ,T4] , [Gcd2 ,U2 ,V2 ,K2 ,P2 ,T2] ) . t e s t 5 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d l , U 2 , V l , K l , P l , T l ] ) : -T 1 > 0 , a s g n ( [ G c d l , U l , V l , K l , P l , T l ] , U 2 , T l , [ G c d l , U 2 , V l , K l , P l , T l ] ) . t e s t 5 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d l , U l , V 2 , K l , P l , T l ] ) : -"T1>0 , a s g n ( [ G c d l , U l , V l , K l , P l , T l ] , V 2 , 0 - T l , [ G c d l , U l , V 2 , K l , P l , T l ] ) . t e s t 6 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -T 1 = \ = 0 , b 3 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . 166 APPENDIX H. PARTIALLY EVALUATED BINARY GCD SEMANTICS t e s t 6 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U l , V l , K 2 , P 2 , T l ] ) : -~ T 1 = \ = 0 , a s g n ( [ G c d l , U l , V l , K l , P l , T l ] , K 2 , K l , [ G c d l , U l , V l , K 2 , P l , T l ] ) , callasgn( [ G c d l , U 1 , V 1 , K 2 ,P 1 ,T 1] ,Tmp 1,2), c a U a s g n ( [ G c d l , U l , V l , K 2 , P l , T l ] , T m p 2 , K 2 ) , power([P 1 , T m p l , T m p 2 ] , [P2,Tmp3,Tmp4]) , a s g n ( [ G c d l , U l , V l , K 2 , P 2 , T l ] , G c d 2 , U l * P 2 , [ G c d 2 , U l , V l , K 2 , P 2 , T l ] ) . b 3 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -a s g n ( [ G c d l , U l , V l , K l , P l , T l ] , T 3 , T l / / 2 , [ G c d l , U l , V l , K l , P l , T 3 ] ) , t e s t 4 ( [ G c d l , U l , V l , K l , P l , T 3 ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) . b 4 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) : -t e s t 4 ( [ G c d l , U l , V l , K l , P l , T l ] , [ G c d 2 , U 2 , V 2 , K 2 , P 2 , T 2 ] ) .
Thesis/Dissertation
eng
Computer Science
Vancouver : University of British Columbia Library
For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.
Graduate
The semantics and transformation of imperative programs using horn clauses
Text