[m-rev.] for review: Overhaul of the Syntax chapter of the reference manual
Mark Brown
mark at mercurylang.org
Wed Aug 31 11:28:23 AEST 2022
Re-sent with just the diff attached (in case tarball is too big).
On Wed, Aug 31, 2022 at 11:25 AM Mark Brown <mark at mercurylang.org> wrote:
>
> Hi all,
>
> This makes some significant changes to the Syntax chapter. The
> motivation for these changes comes largely from what questions were
> needing to be asked by programmers with a non-Prolog background who
> were learning Mercury, and what things they were confused about.
>
> The texinfo is for review by Peter, but I've also attached a tarball
> of the split html for anyone else to look through (and pdf and info,
> in case anyone cares).
>
> Cheers,
> Mark
-------------- next part --------------
commit 923a62ae30a236ba11b61020c3636e6909e67925
Author: Mark Brown <mark at mercurylang.org>
Date: Tue Aug 30 07:53:25 2022 +1000
Overhaul of the Syntax chapter of the reference manual
There are three main aims for this change:
1. Don't rely so much on users having knowledge of Prolog (ideally we
wouldn't require it at all, but this change probably doesn't fully achieve
that). Present the information more linearly, i.e., without requiring
so many forward references.
2. Make important information less likely to be overlooked. As it stands,
we give a lot of semantics in the Syntax chapter where users wouldn't
expect to find it (they're more likely to just skim over such a chapter).
We also currently break the chapter up into small sections, some of which
have little information. This works well in the PDF version, but in split
html and info versions where navigation is required it is a pain. People
tend to forget information each time they navigate, and are likely to find
themselves going back and forth between nodes.
3. Remove some inconsistencies in our descriptions and use of terminology,
and try to remove ambiguities.
Changes to terminology
----------------------
These are aimed at being more consistent, as well as dividing things up
into concepts that we need to refer to later on.
- A term is now a core term or a special term. The latter are for list
syntax, etc. Avoid the use of "is parsed as", the significance of which
is not clear, and instead define an equivalence relation via a term
normalization procedure.
- Define "functor" and "principal functor". Don't use "functor" to talk
about terms: the functor is defined as the name/arity pair. Also give
some synonyms we use for functor.
- Core terms are divided into variables, constants, and functor terms.
Functor terms are names on their own or names with arguments
(i.e., "functor terms" are those terms that have meaningful functors).
- "Higher-order terms" are now called "apply terms", since they aren't
necessarily higher-order themselves, and because that is a semantic
concept anyway.
- Data-terms are now referred to as expressions.
- Refer to "field access" rather than "record syntax". It's not made clear
that these are referring to the same feature, so it's better to stick to
one term (at least until full definitions are given).
Changes to document structure
-----------------------------
Sections and subsections of the Syntax chapter have been merged, to provide
a more reasonable amount of information at each node. The Syntax chapter
as a whole has been split into two chapters, Syntax and Semantics (the
existing Semantics chapter is renamed Formal Semantics). The new structure
is as follows:
Syntax
- The opening blurb covers the material from "Syntax overview" and
"Character set". The definitions are put first, and comparisons with
Prolog are put after (in general we try to make such comparisons only
as secondary information).
- "Lexical syntax" covers the material from "Whitespace" and "Tokens".
We also provide comment syntax. Line number directives are no longer
considered tokens, since we are supposed to ignore them when parsing
terms anyway.
- "Terms" covers the material previously in that section. It adds a summary
in the form of grammar rules (but makes it clear all the information is
also in the prose), and a term normalization procedure that is _not_
written in pseudo-Mercury. The grammar is there for people who are likely
to skip the prose but less likely to skip a grammar, and the prose is there
because that's the best way to describe things.
- "Builtin operators" covers the same material as before.
- "Items" covers the material previously in "Items", "Declarations",
"Facts", "Rules", and "DCG-rules". It also adds a summary in the form of
grammar rules.
Semantics
- I've written an introductory section on declarative programming, which
informally introduces the declarative and operational semantics (and why
you want them both).
- "Goals" covers the same material as before, but I have rearranged the
order of the goals so as to avoid forward references, and to put more
commonly used goals earlier.
- "Expressions" covers the material previously in "Data-terms" and its
subsections. The expressions are (mostly) collected into one table, but
field access expressions are kept separate as they require a bit more
explanation. I've used an anchor on this separate bit, however, so maybe
it should be in a section that follows Expressions (i.e., Expressions
should say "see next section for details" or whatever).
- The remaining sections, "State variables", "Variable scoping",
"Implicit quantifiaction", and "Elimination of double negation" are kept
largely as is. (The state variables section is hard to make sense of,
however. I think it might be better in a chapter of its own between
"Semantics" and "Types", even though it might technically be considered
syntax.)
Other changes
-------------
- Names now include sequences of graphic chars and a single semicolon,
which is what our parser actually allows.
- Define operators as separate tokens, even though they overlap with
names (e.g., plus sign is both an operator and a name, but comma is just
an operator). This gives a better account of when parentheses are needed.
Move the point about character literals into the Semantics chapter where
we talk about character literals.
- Use hyphens in meta-variables rather than underscore, per the texinfo
guidelines.
- In Builtin operators, explain that operators are a syntactic concept
and you need to import a module to get, e.g., arithmetic operations.
Point out the user defined operator in the prose rather than in a
footnote. And fix the formatting of that table!
- Try to use a more consistent writing style.
diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index fb2b23eac..80c9fb466 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -83,6 +83,7 @@ into another language, under the above conditions for modified versions.
@menu
* Introduction:: A brief introduction to Mercury.
* Syntax:: A description of Mercury's syntax.
+* Semantics:: A description of Mercury's goals and expressions.
* Types:: Mercury has a strong parametric polymorphic type system.
* Modes:: Modes allow you to specify the direction of data flow.
* Unique modes:: Unique modes allow you to specify when there is only one
@@ -102,7 +103,7 @@ into another language, under the above conditions for modified versions.
* Type conversions:: Converting between subtypes and supertypes.
* Exception handling:: Catching exceptions to recover from exceptional
situations.
-* Semantics:: Declarative and operational semantics of Mercury
+* Formal semantics:: Declarative and operational semantics of Mercury
programs.
* Foreign language interface:: Calling code written in other programming
languages from Mercury code
@@ -160,57 +161,54 @@ for common programming tasks --- see the Mercury Library Reference Manual.
@node Syntax
@chapter Syntax
+A Mercury program consists of a set of @dfn{modules}.
+Each module is a file written using the UTF-8 encoding
+of the Unicode character set,
+and contains a sequence of @dfn{items}.
+Each item is a @dfn{term} followed by a period,
+and is interpreted as either a @dfn{declaration} or a @dfn{clause}
+depending on the form it takes.
+
+Mercury's term syntax is similar to that of Prolog,
+with some notable distinctions:
+
+ at itemize
+ at item String constants are atomic;
+they are not abbreviations for lists of character codes
+(@pxref{Lexical syntax}).
+ at item
+The operator table is fixed and cannot be modified.
+Some operators differ in priority from those used in Prolog
+(@pxref{Builtin operators}).
+ at end itemize
+
+Mercury's clause syntax for defining predicates
+is also similar to that of Prolog,
+including the use of Definite Clause Grammar (DCG) notation.
+Mercury clauses, however, can additionally define functions
+that users may invoke in expressions.
+
@menu
-* Syntax overview::
-* Character set::
-* Whitespace::
-* Tokens::
+* Lexical syntax::
* Terms::
* Builtin operators::
* Items::
-* Declarations::
-* Facts::
-* Rules::
-* Goals::
-* State variables::
-* DCG-rules::
-* DCG-goals::
-* Data-terms::
-* Variable scoping::
-* Implicit quantification::
-* Elimination of double negation::
@end menu
- at node Syntax overview
- at section Syntax overview
-
-Mercury's syntax is similar to the syntax of Prolog,
-with some additional declarations for types, modes, determinism,
-the module system, and pragmas,
-and with the distinction that function symbols
-may stand also for invocations of user-defined functions
-as well as for data constructors.
-
-A Mercury program consists of a set of modules.
-Each module is a file containing a sequence of items
-(declarations and clauses).
-Each item is a term followed by a period.
-Each term is composed of a sequence of tokens,
-and each token is composed of a sequence of characters.
-Like Prolog,
-Mercury has the Definite Clause Grammar (DCG) notation for clauses.
-
- at node Character set
- at section Character set
-
-Mercury program source files must be written
-using the UTF-8 encoding of the Unicode character set.
+ at node Lexical syntax
+ at section Lexical syntax
- at node Whitespace
- at section Whitespace
+Mercury modules are comprised of a sequence of tokens separated by
+any amount of whitespace, comments, and line number directives.
+These separators are mostly ignored by the parser,
+but in some cases whitespace may be required to separate tokens
+that would otherwise be ambiguous.
+In other cases whitespace is not allowed,
+e.g., before the @var{open-ct} token,
+or after a @samp{.} operator
+that would otherwise be interpreted as an @var{end} token.
-In Mercury program source files,
-whitespace is defined to be the following characters:
+Whitespace is defined to be the following characters:
@multitable {CHARACTER_TABULATION} {Unicode_code_point} {Horizontal-tab}
@headitem Unicode name @tab Unicode code point @tab Notes
@@ -222,34 +220,32 @@ whitespace is defined to be the following characters:
@item @sc{carriage return} @tab U+000D @tab
@end multitable
- at node Tokens
- at section Tokens
+The @samp{%} character starts a comment that continues to the end of the line.
+The @samp{/*} character sequence starts a comment that continues until
+the next occurrence of @samp{*/}.
-The different tokens in Mercury are as follows.
-Tokens may be separated by whitespace.
-
- at table @emph
-
- at item line number directive
A line number directive consists of the character @samp{#},
a positive integer specifying the line number, and then a newline.
-A @samp{#@var{line}} directive's only role
-is to specifying the line number;
-it is otherwise ignored by the syntax.
-Line number directives may occur anywhere a token may occur.
-They are used in conjunction with the @samp{pragma source_file} declaration
-to indicate that the Mercury code following was generated by another tool;
-they serve to associate each line in the Mercury code
-with the source file name and line number
-of the original source from which the Mercury code was derived,
-so that the Mercury compiler can issue more informative error messages
-using the original source code locations.
+Line number directives specify a current line number;
+they are used in conjunction with the @samp{pragma source_file} declaration
+(@pxref{Source file name})
+to indicate that errors in the subsequent Mercury code should be
+reported as coming from a different location.
+This is useful if the code in question was generated by another tool,
+in which case the line number can be set to the corresponding location
+in the original source file from which the Mercury code was derived.
+The Mercury compiler can thereby issue more informative error messages
+using locations in the original source file.
A @samp{#@var{line}} directive specifies
the line number for the immediately following line.
Line numbers for lines after that are incremented as usual,
so the second line after a @samp{#100} directive
would be considered to be line number 101.
+The different tokens in Mercury are as follows.
+
+ at table @var
+
@item string
A string is a sequence of characters enclosed in double quotes (@code{"}).
@@ -296,7 +292,8 @@ over more than one source line.
@c to wrap examples as @t will not put quotes around its argument,
@c and we cannot expect readers to figure out which quotes
@c are subject matter and which are decoration.
-A name is either an unquoted name or a quoted name.
+A name is either an unquoted name, a quoted name, a graphic name,
+or a single semicolon character.
An unquoted name is a lowercase letter followed by zero or more letters,
underscores, and digits.
A quoted name is any sequence of zero or more characters
@@ -305,16 +302,37 @@ Within a quoted name,
two adjacent single quotes stand for a single single quote.
Quoted names can also contain
backslash escapes of the same form as for strings.
-
-Note that if a character is an operator,
-then the result of enclosing that character in single quotes
-is also an operator.
-Since e.g.@: @t{:} is an operator,
- at t{':'} is an operator as well,
-which means that e.g.@: @t{Char = ':'} is not valid code.
-To make it valid code, you need to put parentheses around the operator,
-to prevent the scope of the operator from extending to the surrounding code.
-This means that code such as @t{Char = (':')} is valid.
+A graphic name is a sequence of one or more of the following characters
+ at example
+! & * + - : < = > ? @@ ^ ~ \ # $ . /
+ at end example
+where the first character is not @samp{#}.
+
+An unquoted name, graphic name, or semicolon
+is treated as equivalent to a quoted name containing
+the same sequence of characters.
+
+ at item operator
+An operator is one of the builtin operators (@pxref{Builtin operators})
+or a user-defined operator.
+A user-defined operator is a name,
+module qualified name (@pxref{The module system}), or variable,
+enclosed in grave accents (backquotes).
+User-defined operators are left-associative infix operators
+that bind more strongly than most other operators;
+see the builtin operator table for their relative binding strength.
+
+The builtin operators, with the exception of comma, are all names,
+and as such they can be used without arguments supplied.
+For example, @samp{f(+)} is syntactically valid.
+In some cases parentheses may be required
+to limit the scope of an operator without arguments,
+e.g. if it appears as an argument to another operator.
+The comma operator is not a name and therefore requires single quotes
+in order to be used without arguments.
+
+Note that an operator in single quotes is still an operator,
+so any requirement for parentheses will remain unchanged.
@item variable
A variable is an uppercase letter or underscore
@@ -365,8 +383,8 @@ between the radix prefix (i.e.@: @samp{0b}, @samp{0o} and @samp{0x})
and the initial digit.
Similarly, an arbitrary number of underscores
may be inserted between the final digit and the signedness suffix.
-The purpose of the underscores is to improve readability,
-and they do not affect the numeric value of the literal.
+The purpose of the underscores is to improve readability;
+they do not affect the numeric value of the literal.
@c TODO: we should support hexadecimal float literals too.
@item float
@@ -382,14 +400,14 @@ may be inserted between the digits in a floating point literal.
Underscores may @emph{not} occur adjacent to any non-digit characters
(i.e.@: @samp{.}, @samp{e}, @samp{E}, @samp{+} or @samp{-})
in a floating point literal.
-The purpose of the underscores is to improve readability,
-and they do not affect the numeric value of the literal.
+The purpose of the underscores is to improve readability;
+they do not affect the numeric value of the literal.
- at item implementation_defined_literal
+ at item implementation-defined-literal
An implementation-defined literal
consists of a dollar sign (@samp{$}) followed by an unquoted name.
- at item open_ct
+ at item open-ct
A left parenthesis, @samp{(}, that is not preceded by whitespace.
@item open
@@ -398,19 +416,19 @@ A left parenthesis, @samp{(}, that is preceded by whitespace.
@item close
A right parenthesis, @samp{)}.
- at item open_list
+ at item open-list
A left square bracket, @samp{[}.
- at item close_list
+ at item close-list
A right square bracket, @samp{]}.
- at item open_curly
+ at item open-curly
A left curly bracket, @samp{@{}.
- at item close_curly
+ at item close-curly
A right curly bracket, @samp{@}}.
- at item ht_sep
+ at item ht-sep
A ``head-tail separator'', i.e.@: a vertical bar, @samp{|}.
@item comma
@@ -419,85 +437,260 @@ A comma, @samp{,}.
@item end
A full stop (period), @samp{.}.
- at item eof
-The end of file.
-
@end table
@node Terms
@section Terms
-A term is either a variable or a functor.
+Terms are the basic construct
+used by most syntactic forms in Mercury:
+declarations, clauses, and their sub-components,
+all adhere to the syntax rules for terms.
+Thus, the set of syntactically valid declarations
+is a subset of the set of syntactically valid terms,
+and likewise for the set of syntactically valid clauses, etc.
+
+The term syntax is summarized by the following rules.
+(All of this information can be found in the descriptions below the rules.)
+
+ at display
+ at var{term} = @var{core-term} | @var{special-term}
+
+ at var{core-term} = @var{variable} | @var{constant} | @var{functor-term}
+
+ at var{constant} = @var{integer} | @var{float} | @var{string} | @var{implementation-defined-literal}
+
+ at var{functor-term} = @var{name} | @var{name} @var{open-ct} @var{functor-args} @var{close}
+
+ at var{functor-args} = @var{functor-arg} | @var{functor-arg} @samp{,} @var{functor-args}
+
+ at c The following definition of functor arg is more restrictive than our
+ at c implementation, which allows operators with priority > 1000 other
+ at c than the '::' which is explicitly allowed here. In future we may
+ at c lower the priority of '::' and implement the restriction; for this
+ at c reason, we impose the restriction now.
+ at c
+ at c A similar situation applies to list elements and the arguments to
+ at c apply terms. For tuples we already implement the restriction.
+ at c
+ at var{functor-arg} = @var{arg} | @var{arg} @samp{::} @var{arg}
+
+ at var{args} = @var{arg} | @var{arg} @samp{,} @var{args}
-A functor is an integer, a float, a string, a name, a compound term,
-or a higher-order term.
+ at var{arg} = @var{term}, where the term is not an operator term with priority >= 1000
-A compound term is a simple compound term, a list term, a tuple term,
-an operator term, or a parenthesized term.
+ at var{special-term} = @var{operator-term} | @var{list-term} | @var{tuple-term} | @var{apply-term} | @var{paren-term}
-A simple compound term is a name
+ at var{operator-term} = @var{term} @var{operator} @var{term} | @var{operator} @var{term} | @var{operator} @var{term} @var{term},
+ where the term is constructed according to the requirements of the operator
+ (@pxref{Builtin operators})
+
+ at var{list-term} = @samp{[} @var{list-body}? @samp{]}
+
+ at var{list-body} = @var{arg} | @var{arg} @samp{,} @var{list-body} | @var{arg} @var{ht-sep} @var{term}
+
+ at var{tuple-term} = @samp{@{} @var{args}? @samp{@}}
+
+ at var{apply-term} = @var{term} @var{open-ct} @var{args} @var{close},
+ where the term is not a name or operator term
+
+ at var{paren-term} = @samp{(} @var{term} @samp{)}
+ at end display
+
+ at noindent
+Valid terms can be described in the following way.
+
+ at table @var
+
+ at item term
+A term is either a @var{core term} or a @var{special term}.
+A term normalization procedure, given below,
+translates terms that may contain special terms
+into terms that are only constructed from core terms;
+two terms are considered syntactically equivalent
+if they translate to the same term.
+Syntactically equivalent terms can be used interchangeably
+anywhere in a module
+(e.g.@: operator syntax can be used in declarations and clauses,
+in particular those that define an operator).
+
+Note that there can be further equivalences in some contexts,
+e.g.@: an if-then-else can be written in either of two equivalent forms.
+Such equivalences will be covered in the relevant chapters.
+
+ at item core-term
+A core term is a @var{variable}, a @var{constant}, or a @var{functor-term}.
+
+ at item constant
+A constant is an @var{integer}, a @var{float}, a @var{string},
+or an @var{implementation-defined-literal}.
+
+ at item functor-term
+A functor term is either a name or a compound term.
+A compound term is a name followed without any intervening whitespace
+by an open parenthesis (i.e.@: an @var{open-ct} token),
+then followed by a functor argument list and a close parenthesis.
+E.g., @samp{foo(X,Y)} is a compound term,
+whereas @samp{foo (X,Y)} and @samp{foo()} are not
+(the first because the space after @samp{foo} is not allowed,
+the second because the parentheses must be omitted if there are no arguments).
+
+The @dfn{principal functor} of a functor term
+is the name and arity of the term, separated by a slash,
+where the arity is the number of arguments
+(or zero if there are no arguments).
+For example, the principal functor of @samp{foo(bar,baz)} is @samp{foo/2},
+while the principal functor of @samp{foo} is @samp{foo/0}.
+The principal functor of a special term is determined
+ at emph{after} normalization.
+
+Note that the word ``functor'' has a number of definitions,
+but in Mercury it just means
+a symbol to which arguments can be applied,
+and which has no intrinsic meaning of its own.
+It is a syntactic concept that applies to all functor terms.
+In specific contexts functors may also be referred to as
+type constructors, data constructors (or just constructors),
+predicates, functions, etc.
+The principal functor may also be referred to
+as the ``top-level constructor''.
+
+ at item functor-args
+A functor argument list is a sequence of one or more functor arguments,
+separated by commas.
+
+ at item functor-arg
+A functor argument is either a single argument
+or two arguments separated by a @samp{::} operator
+(the latter form is for mode qualifiers; @pxref{Different clauses for different modes}).
+
+ at item args
+An argument list is a sequence of one or more arguments,
+separated by commas.
+
+ at item arg
+An argument is any term, except operator terms where
+the operator does not bind more tightly than comma
+(i.e., where the priority is greater than or equal to 1000).
+In such a situation parentheses can be used,
+e.g.@: @samp{f((A,B))} is a compound term
+with one argument that is a parenthesized operator term,
+whereas @samp{f(A,B)} is a compound term
+with two arguments (and no operators).
+
+ at item special-term
+A special term is an operator term, a list term, a tuple term,
+an apply term, or a parenthesized term.
+The term normalization procedure, below, defines how these terms
+are represented internally as core terms.
+
+ at item operator-term
+An operator term is a term constructed using an operator,
+which complies with the rules for constructing terms using that operator
+(@pxref{Builtin operators}).
+Operator terms can be infix, such as @samp{A + B},
+unary-prefix, such as @samp{not P},
+or binary-prefix, such as @samp{some Vars Goal}.
+
+ at item list-term
+A list term is an open square bracket (an @var{open-list} token),
+followed by an optional list body,
+followed by a close square bracket (a @var{close-list} token).
+If the list body is omitted it is the empty list.
+If present, the list body is an argument list,
+optionally followed by a vertical bar (a @var{ht-sep} token)
+followed by a term.
+E.g., @samp{[]}, @samp{[X]}, and @samp{[1, 2 | Tail]}
+are all valid list terms.
+The argument list gives the elements appearing at the front of the list.
+The term following the vertical bar, if present,
+gives the @dfn{tail} of the list (i.e.@: the remaining elements),
+otherwise the tail is the empty list.
+Note that technically the tail does not have to be a list
+for this to be syntactically valid,
+although generally it would need to be in order to be type correct.
+
+ at item tuple-term
+A tuple term is an open curly bracket (an @var{open-curly} token),
+followed by an optional argument list,
+followed by a close curly bracket (a @var{close-curly} token).
+If the argument list is omitted it is the empty tuple,
+otherwise the arguments give the components of the tuple.
+E.g., @code{@{@}} and @code{@{1,'2',"three"@}} are valid tuple terms.
+
+ at item apply-term
+An apply-term is a ``closure'' term,
+which can be any term other than a name or an operator term,
followed without any intervening whitespace
-by an open parenthesis (i.e.@: an open_ct token),
-a sequence of argument terms separated by commas,
-and a close parenthesis.
+by an open parenthesis (an @var{open-ct} token),
+an argument list, and a close parenthesis (a @var{close} token).
+E.g., @samp{A(B,C)} is a valid apply-term.
+An apply-term represents the closure (i.e.@: a higher-order value)
+applied to the arguments.
+
+Note that although the closure term cannot be an operator term,
+it @emph{can} be a parenthesized term.
+Thus @samp{(Var ^ foo)(Arg1, Arg2)} is a valid apply-term,
+whereas @samp{Var ^ foo(Arg1, Arg2)} is not
+(it is an operator term whose second argument is a compound term).
+
+ at item paren-term
+A parenthesized term is just a term enclosed in parentheses.
+E.g., @code{(X-Y)} is a valid parenthesized term.
+
+ at end table
+
+ at noindent
+The term normalization procedure works by rewriting special terms
+that occur anywhere within a term
+(i.e.@: at the top level or as some descendant)
+according to a set of rewriting rules,
+and repeating until no rules can be further applied.
+The rules are as follows.
-A list term is an open square bracket (i.e.@: an open_list token)
-followed by a sequence of argument terms separated by commas,
-optionally followed by a vertical bar (i.e.@: a ht_sep token)
-followed by a term,
-followed by a close square bracket (i.e.@: a close_list token).
-An empty list term is an open_list token followed by a close_list token.
-List terms are parsed as follows:
@example
-parse('[' ']') = [].
-parse('[' List) = parse_list(List).
-parse_list(Head ',' Tail) = '[|]'(parse_term(Head), parse_list(Tail)).
-parse_list(Head '|' Tail ']') = '[|]'(parse_term(Head), parse_term(Tail)).
-parse_list(Head ']') = '[|]'(parse_term(Head), []).
+ at var{term1} `@var{name}` @var{term2} @expansion{} @var{name}(@var{term1}, @var{term2})
+ at var{term1} `@var{var}` @var{term2} @expansion{} @var{var}(@var{term1}, @var{term2})
+ at var{term1} @var{operator} @var{term2} @expansion{} '@var{operator}'(@var{term1}, @var{term2})
+ at var{operator} @var{term} @expansion{} '@var{operator}'(@var{term})
+ at var{operator} @var{term1} @var{term2} @expansion{} '@var{operator}'(@var{term1}, @var{term2})
+
+[ ] @expansion{} '[]'
+[ @var{arg} ] @expansion{} '[|]'(@var{arg}, '[]')
+[ @var{arg} , @var{list-body} ] @expansion{} '[|]'(@var{arg}, [@var{list-body}])
+[ @var{arg} | @var{term} ] @expansion{} '[|]'(@var{arg}, @var{term})
+
+@{ @} @expansion{} '@{@}'
+@{ @var{args} @} @expansion{} '@{@}'(@var{args})
+
+ at var{term}(@var{args}) @expansion{} ''(@var{term}, @var{args})
+
+( @var{term} ) @expansion{} @var{term}
@end example
-The following terms are all equivalent:
+ at noindent
+For example, the following terms are all syntactically equivalent
+(i.e.@: they are equal after normalization).
+The last is constructed from core terms;
+the others all normalize to this term.
+From the last one it can be seen that
+the principal functor of all of them is @t{'[|]'/2}.
@example
[1, 2, 3]
[1, 2, 3 | []]
[1, 2 | [3]]
[1 | [2, 3]]
-'[|]'(1, '[|]'(2, '[|]'(3, [])))
- at end example
-
-A tuple term is a left curly bracket (i.e.@: an open_curly token)
-followed by a sequence of argument terms separated by commas,
-and a right curly bracket.
-For example, @code{@{1, '2', "three"@}} is a valid tuple term.
-
-An operator term is a term specified using operator notation, as in Prolog.
-Operators can also be formed by enclosing a name, a module qualified name
-(@pxref{The module system}), or a variable between grave accents (backquotes).
-Any name or variable may be used as an operator in this way.
-If @var{fun} is a variable or name,
-then a term of the form @code{@var{X} `@var{fun}` @var{Y}} is equivalent to
- at code{@var{fun}(@var{X}, @var{Y})}. The operator is left associative
-and binds more tightly than every operator other than @samp{^}
-(@pxref{Builtin operators}).
-
-A parenthesized term is just
-an open parenthesis followed by a term and a close parenthesis.
+'[|]'(1, '[|]'(2, '[|]'(3, '[]')))
+ at end example
-A higher-order term is a ``closure'' term,
-which can be any term other than a name or an operator term,
-followed without any intervening whitespace
-by an open parenthesis (i.e.@: an open_ct token),
-a sequence of argument terms separated by commas,
-and a close parenthesis.
-A higher-order term is equivalent to a simple compound term
-whose functor is the empty name,
-and whose arguments are the closure term
-followed by the argument terms of the higher-order term.
-That is, a term such as @code{Term(Arg1, @dots{}, ArgN)} is parsed as
- at code{''(Term, Arg1, @dots{}, ArgN)}.
-Note that the closure term can be a parenthesized term;
-for example, @code{(Term ^ FieldName)(Arg1, Arg2)} is a higher-order term,
-and so it gets parsed as if it were @code{''((Term ^ FieldName), Arg1, Arg2)}.
+ at noindent
+Similarly, the following terms are all syntactically equivalent.
+The principal functor in this case is @t{'+'/2}.
+ at example
+A * B + C
+(A * B) + C
+'+'('*'(A, B), C)
+ at end example
@node Builtin operators
@section Builtin operators
@@ -507,7 +700,9 @@ Operators with a low ``Priority'' bind more tightly
than those with a high ``Priority''.
For example, given that
@code{+} has priority 500 and @code{*} has priority 400,
-the term @code{2 * X + Y} would parse as @code{(2 * X) + Y}.
+the term @code{2 * X + Y} is equivalent to @code{(2 * X) + Y}.
+User-defined operators of the form @code{`@var{op}`}
+are also included in the table to indicate their relative priority.
The ``Specifier'' field indicates
what structure terms constructed with an operator are allowed to take.
@@ -519,6 +714,17 @@ whose priority is lower or equal to that of the operator.
For example, ``yfx'' indicates a left-associative infix operator,
while ``xfy'' indicates a right-associative infix operator.
+Note that operators are a syntactic concept.
+The @samp{+} infix operator, for example, is only a symbol;
+it doesn't mean addition unless you write or import code
+that defines it as addition.
+Modules in the Mercury standard library,
+such as @code{int} and @code{float},
+provide such arithmetic definitions.
+To illustrate further,
+the @samp{-} infix operator is defined as subtraction by those modules
+but is defined as a pair constructor by the @code{pair} module.
+
@example
Operator Specifier Priority
@@ -532,7 +738,7 @@ Operator Specifier Priority
^ fx 100
event fx 100
: yfx 120
-`@var{op}` yfx 120 @footnote{Operator term (@pxref{Terms}).}
+`@var{op}` yfx 120
** xfy 200
- fx 200
\ fx 200
@@ -660,137 +866,491 @@ use_module fx 1199
@node Items
@section Items
-Each item in a Mercury module is either a declaration or a clause.
-If the top-level functor of the term is @samp{:-/1},
-the item is a declaration, otherwise it is a clause.
-There are three types of clauses.
-If the top-level functor of the item is @samp{:-/2}, the item is a rule.
-If the top-level functor is @samp{-->/2}, the item is a DCG rule.
-Otherwise, the item is a fact.
-There are two types of rules and facts.
-If the top-level functor of the head of a rule is @samp{=/2}, the rule
-is a function rule, otherwise it is a predicate rule.
-If the top-level functor of the head of a fact is @samp{=/2}, the fact
-is a function fact, otherwise it is a predicate fact.
-
- at node Declarations
- at section Declarations
-
-The allowed declarations are:
-
- at example
-:- type
-:- solver type
-:- pred
-:- func
-:- inst
-:- mode
-:- typeclass
-:- instance
-:- pragma
-:- promise
-:- initialise
-:- finalise
-:- mutable
-:- module
-:- interface
-:- implementation
-:- import_module
-:- use_module
-:- include_module
-:- end_module
- at end example
-
-The @samp{type}, @samp{solver type}, @samp{pred}, @samp{func}, @samp{typeclass}
-and @samp{instance} declarations are used for the type system,
-the @samp{inst} and @samp{mode} declarations are for the mode system,
-the @samp{pragma} declarations are for the foreign language interface,
-and for compiler hints about inlining,
-and the remainder are for the module system.
-They are described in more detail in their respective chapters.
-
- at node Facts
- at section Facts
-
-A function fact is an item of the form @samp{@var{Head} = @var{Result}}.
-A predicate fact is an item of the form @samp{@var{Head}},
-where the top-level functor of @var{Head}
-is not @code{:-/1}, @code{:-/2}, @code{-->/2}, or @code{=/2}.
-In both cases, the @var{Head} term must not be a variable.
-The top-level functor of the @var{Head}
-determines which predicate or function the fact belongs to;
-the predicate or function must have been declared
-in a preceding @samp{pred} or @samp{func} declaration in this module.
-The @var{Result} (if any) and the arguments of the @var{Head}
-must be valid data-terms
-(optionally annotated with a mode qualifier;
-see @ref{Different clauses for different modes}).
-
-A fact is equivalent to a rule whose body is @samp{true}.
-
- at node Rules
- at section Rules
-
-A function rule is an item of the form
- at samp{@var{Head} = @var{Result} :- @var{Body}}.
-A predicate rule is an item of the form
- at samp{@var{Head} :- @var{Body}}
-where the top-level functor of @samp{Head} is not @code{=/2}.
-In both cases, the @var{Head} term must not be a variable.
-The top-level functor of the @var{Head} determines
-which predicate or function the clause belongs to;
-the predicate or function must have been declared
-in a preceding @samp{pred} or @samp{func} declaration in this module.
-The @var{Result} and the arguments of the @var{Head}
-must be valid data-terms
-(optionally annotated with a mode qualifier;
-see @ref{Different clauses for different modes}).
-The @var{Body} must be a valid goal.
+Items are the top-level syntactic elements of Mercury modules.
+Their syntax is summarized by the following rules.
+(All of this information can be found in the descriptions below the rules.)
- at node Goals
- at section Goals
+ at display
+ at var{item} = (@samp{:-} @var{declaration} | @var{clause}) @var{end}
-A goal is a term of one of the following forms.
+ at var{declaration} = @var{type-system-decl} | @var{mode-system-decl} | @var{module-system-decl}
+ | @var{pragma-decl}
- at table @asis
- at item @code{some @var{Vars} @var{Goal}}
-An existential quantification.
- at var{Goal} must be a valid goal.
- at var{Vars} must be a list
-whose elements are either variables or state variables.
-(A single list may contain both.)
-The case where they are state variables
-is described in @ref{State variables};
-here we discuss the case where they are plain variables.
+ at var{clause} = @var{rule} | @var{dcg-rule} | @var{fact}
-Each existential quantification introduces a new scope.
-The variables in @var{Vars} are local to the goal @var{Goal}:
-for each variable named in @var{Vars},
-any occurrences of variables with that name in @var{Goal}
-are considered to name a different variable
-than any variables with the same name
-that occur outside of the existential quantification.
+ at var{rule} = @var{head-term} @samp{:-} @var{goal}
-Operationally, existential quantification has no effect,
-so apart from its effect on variable scoping,
- at samp{some @var{Vars} @var{Goal}} is the same as @samp{@var{Goal}}.
+ at var{dcg-rule} = @var{predicate-head-term} @samp{-->} @var{dcg-goal}
-Mercury's rules for implicit quantification (@pxref{Implicit quantification})
-mean that variables are often implicitly existentially quantified.
-There is usually no need to write existential quantifiers explicitly.
+ at var{fact} = @var{head-term}, where the principal functor is not @samp{:-/1}, @samp{:-/2}, or @samp{-->/2}
- at item @code{all @var{Vars} @var{Goal}}
-A universal quantification.
- at var{Goal} must be a valid goal.
- at var{Vars} must be a list of variables
-(they may @emph{not} be state variables).
-This goal is an abbreviation for @samp{not (some @var{Vars} not @var{Goal})}.
+ at var{head-term} = @var{function-head-term} | @var{predicate-head-term}
- at item @code{@var{Goal1}, @var{Goal2}}
+ at var{function-head-term} = @var{head} @samp{=} @var{expression}
+
+ at var{predicate-head-term} = @var{head}, where the principal functor is not @samp{=/2}
+
+ at var{head} = @var{functor-term}, where the arguments are expressions
+ at end display
+
+ at noindent
+Valid items can be described in the following way.
+
+ at table @var
+
+ at item item
+Each item in a Mercury module is a term
+followed by an @var{end} token (a period).
+If the principal functor of the term is @samp{:-/1},
+it is a declaration item and the argument is the @dfn{declaration}.
+Otherwise it is a clause item
+and the term is the @dfn{clause}.
+Note that we often use ``declaration'' and ``clause'' informally
+to refer to the items themselves
+(i.e., including the @var{end} token).
+
+ at item declaration
+Declarations in Mercury are used to declare things
+for the type system, the mode system, and the module system,
+as well as to give compiler directives
+regarding a number of features.
+Details of their syntax are covered in later chapters.
+
+ at item type-system-decl
+These declarations relate to the type system.
+ at samp{type} declarations declare and define types
+(@pxref{User-defined types} and @ref{Solver types}).
+ at samp{pred} and @samp{func} declarations declare the types of
+predicates and functions (@pxref{Predicate and function type declarations}).
+ at samp{typeclass} and @samp{instance} declarations declare
+typeclasses and instances (@pxref{Type classes}).
+
+ at item mode-system-decl
+ at samp{inst} and @samp{mode} declarations relate to the mode system
+(@pxref{Modes}).
+
+ at item module-system-decl
+Declarations relating to the module system are:
+ at samp{module},
+ at samp{interface},
+ at samp{implementation},
+ at samp{import_module},
+ at samp{use_module},
+ at samp{include_module},
+ at samp{initialise},
+ at samp{finalise},
+ at samp{mutable},
+and @samp{end_module}.
+(@xref{Modules}.)
+
+ at item pragma-decl
+ at samp{pragma} declarations give compiler directives (@pxref{Pragmas}),
+are used in the foreign language interface
+(@pxref{Foreign language interface}),
+and in the purity system (@pxref{Promising purity}).
+
+ at item clause
+A clause provides part of the definition of a function or predicate.
+There are three types of clauses:
+if the principal functor is @samp{:-/2}, the clause is a rule;
+if the principal functor is @samp{-->/2}, the clause is a DCG-rule;
+otherwise, the clause is a fact.
+
+Each clause has a head term.
+For rules and DCG-rules, the head term is the left hand side.
+For facts the head term is the entire term.
+Rules and DCG-rules also have a body, which is the right hand side.
+
+ at item rule
+A rule is a clause,
+recognizable by the use of @samp{:-/2},
+that has a goal as its body (@pxref{Goals}).
+
+ at item dcg-rule
+A DCG-rule is a clause,
+recognizable by the use of @samp{-->/2},
+that has a predicate head term
+and a DCG-goal as its body.
+It is an abbreviation for a rule
+with two fresh variables implicitly added to the argument list.
+The DCG-goal is transformed into a goal
+that uses these variables in an idiosyncratic way.
+(@xref{DCG-goals}).
+
+DCG notation is intended for writing parsers and sequence generators
+in a particular style;
+in the past it has also been used to thread an implicit state variable,
+typically the I/O state, through code
+(something that can also be done in that style).
+We now recommend that
+DCG notation be reserved for writing parsers and sequence generators,
+and that state variable syntax (@pxref{State variables}),
+which performs a similar transformation but is more flexible,
+be used for other purposes such as threading state variables.
+
+ at item fact
+A fact is a clause that has no body.
+It has the same meaning as a rule
+with a head term identical to the fact,
+and a body of @code{true}.
+
+ at item head-term
+If the principal functor of the head term is @samp{=/2}
+then it is a function head term,
+otherwise it is a predicate head term.
+
+ at item function-head-term
+A function head term is the head term of a clause
+that provides part of a function definition,
+and that is recognizable by the use of @samp{=/2}.
+The term on the left hand side is the function's head;
+the term on the right hand side is an expression
+that represents the function return value.
+
+ at item predicate-head-term
+A predicate head term is a head on its own with no return expression,
+that provides part of a predicate definition.
+
+ at item head
+The head of a function or predicate is a functor term
+whose arguments are expressions (@pxref{Expressions}),
+optionally annotated with mode qualifiers
+(@pxref{Different clauses for different modes}).
+The principal functor determines
+which function or predicate is being defined.
+
+ at end table
+
+ at noindent
+For example, the following three items are clauses.
+The first is a function fact that defines a function named @samp{loop/1},
+a not particularly useful function.
+The second is a predicate fact and the third is a predicate rule,
+which between them define a predicate named @samp{append/3}.
+
+ at example
+loop(X) = 1 + loop(X).
+
+append([], Bs, Bs).
+append([X | As], Bs, [X | Cs]) :-
+ append(As, Bs, Cs).
+ at end example
+
+ at noindent
+The following example contains a number of declaration and clause items,
+and forms a syntactically valid module.
+(The semantics of the clauses will be covered in the next chapter.
+Note that the @code{length/1} function in the standard library
+is implemented more efficiently.)
+
+ at example
+:- module slow_length.
+:- interface.
+:- import_module list.
+
+:- func length(list(T)) = int.
+
+:- implementation.
+:- import_module int. % for '+'
+
+length([]) = 0.
+length([_ | Xs]) = 1 + length(Xs).
+
+:- end_module slow_length.
+ at end example
+
+ at node Semantics
+ at chapter Semantics
+
+This chapter covers the semantics of Mercury clauses,
+and the goals and expressions they contain.
+The first section
+gives an informal introduction to declarative programming;
+if you are already familiar with this topic,
+and logic programming in particular,
+you may wish to skip it and start with @ref{Goals}.
+
+Full details of the language semantics
+can be found in @ref{Formal semantics}.
+
+ at menu
+* Introduction to declarative programming::
+* Goals::
+* State variables::
+* DCG-goals::
+* Expressions::
+* Variable scoping::
+* Implicit quantification::
+* Elimination of double negation::
+ at end menu
+
+ at node Introduction to declarative programming
+ at section Introduction to declarative programming
+
+Declarative programming is concerned with the idea of ``truth''.
+For example, it's true that 1 plus 1 is 2,
+and that the length of the list [1, 2, 3] is 3.
+Statements like this that may be either true or false
+are known as @dfn{propositions},
+e.g., 1 + 1 = 2 and 1 + 2 = 5 are both propositions;
+if + is interpreted as integer addition
+then the first proposition is true and the second is false.
+
+While programming languages that fit withim
+the functional programming or logic programming paradigms
+are typically considered ``declarative'',
+there is no agreed upon definition of the term.
+One notable characteristic of declarative languages, however,
+is that they have both a @dfn{declarative}
+and an @dfn{operational} semantics.
+
+The operational semantics
+defines how programs should be executed by the system;
+programming languages generally provide an operational semantics.
+A declarative semantics is not generally provided,
+and yet is conceptually simpler
+as it is only concerned with what is true about
+the inputs and outputs of code,
+and not the details of execution.
+This is often expressed by saying that
+the declarative semantics is about ``what''
+whereas the operational semantics is about ``how''.
+
+The advantage of having a declarative semantics
+in addition to an operational semantics
+is that, despite its relative simplicity,
+it can be very effective in analysing the correctness of code.
+For deeper analyses,
+the operational semantics can still be used.
+
+ at menu
+* Declarative semantics::
+* Operational semantics::
+ at end menu
+
+ at node Declarative semantics
+ at subsection Declarative semantics
+
+Mercury clauses say things that are true about
+the function or predicate being defined.
+To illustrate we will use an example from the previous chapter.
+(Note that, here and below,
+some declarations would need to be added to make this compile.)
+
+ at example
+length([]) = 0.
+length([_ | Xs]) = 1 + length(Xs).
+ at end example
+
+ at noindent
+Both of these clauses are facts about the function @code{length/1}.
+The first simply states that the length of an empty list is zero.
+The second is a little more complicated because it involves variables,
+but it states that no matter what expressions we substitute for
+the variables @samp{Xs} and @samp{_},
+the length of @samp{[_ | Xs]} will be one greater than
+the length of @samp{Xs}.
+In other words, the length of a non-empty list
+is one greater than the length of its tail.
+
+These two statements are true according to our intuitive idea of length.
+Furthermore, we can see that the clauses cover every possible list,
+since every list is either empty or non-empty,
+and every non-empty list has a tail that is also a list.
+Perhaps surpisingly,
+this is enough to conclude that
+our implementation of list length is correct,
+at least as far as arguments and return values are concerned.
+
+As another example,
+the following clauses define a predicate named @code{append/3},
+which is intended to be true if
+the third argument is the list that results from appending
+the first and second arguments.
+(Equivalently, we could say that it is possible to split the
+list in the third argument to produce the first and second arguments.)
+
+ at example
+append([], Bs, Bs).
+append([X | As], Bs, [X | Cs]) :-
+ append(As, Bs, Cs).
+ at end example
+
+ at noindent
+The first clause is a fact that states
+if you append the empty list and any other list,
+the result will be the same as that other list.
+The second clause is a rule;
+these are taken as logical implications
+in which the body implies the head
+(i.e.@: @samp{:-} is interpreted as reverse implication).
+So this is stating that, for any substitution,
+if @samp{Cs} is the result of appending @samp{As} and @samp{Bs},
+then @samp{[X | Cs]} is the result of appending @samp{[X | As]} and @samp{Bs}.
+
+Again, both clauses are true according to
+the @dfn{intended interpretation},
+which is defined as all of the propositions about
+the functions and predicates in the program
+that the programmer intends to be true.
+And the definition is @dfn{complete},
+meaning that for every proposition that is intended to be true
+there is either a fact that covers it,
+or a rule whose head covers it and (under the same substitution)
+whose body is intended to be true.
+Thus we can conclude in a similar way to above that our code is correct.
+
+The declarative semantics of a Mercury program is defined as
+all of the propositions that can be inferred to be true
+from the clauses of the program
+(with some additional ``axioms'' that are not important right now).
+If the program is producing incorrect output,
+this is saying that there is a difference between
+the declarative semantics and the intended interpretation.
+From the above discussion,
+there must be some clause that is false in the intended interpretation,
+or some definition that is incomplete.
+
+This is the advantage of declarative programming.
+Despite the semantics being relatively simple---you only need
+to know about which propositions are true and which are false,
+and not how the program actually executes---it is
+still effective in reasoning about your program,
+even so far as to be able to localize a bug observed in the output
+down to individual clauses or definitions.
+
+Not every question can be answered by the declarative semantics.
+It doesn't tell us how the program executes,
+so it can't tell us whether our program will terminate,
+for example, or what its computational complexity is.
+For that we need an operational semantics,
+which is the subject of the next section.
+
+ at node Operational semantics
+ at subsection Operational semantics
+
+Execution in Mercury starts with a @dfn{goal}.
+This is a proposition that may contain some variables,
+and the aim of execution is to find a substitution
+for which the proposition is true.
+If it does, we refer to this as @dfn{success},
+and we refer to the substitution that was found as a @dfn{solution}.
+If execution determines that there are no such substitutions,
+we refer to this as @dfn{failure}.
+
+Say, for example,
+we start with a goal of @samp{N = length([1, 2])}.
+Function evaluation is strict,
+depth-first, and left-to-right,
+so we want to call the @code{length/1} function first.
+To do this, we match the argument with
+the heads of the clauses that define the function
+to find the clause that is applicable.
+In this case the second clause matches,
+with the substitution of @code{Xs @expansion{} [2]}
+(the substitution for @samp{_} is irrelevant,
+since any other occurrence of @samp{_}
+is considered a distinct variable).
+Applying this substitution to the body
+then replacing it in the goal gives us a new goal,
+namely @samp{N = 1 + length([2])}.
+
+Repeating this process a second time
+gives us the goal @samp{N = 1 + 1 + length([])}.
+When we call the function the third time
+it will match the @emph{first} clause,
+and the new goal will be @samp{N = 1 + 1 + 0}.
+Now we can evaluate the @samp{+/2} calls
+and get a result of @samp{N = 2}.
+It is trivial to find a substitution that makes this proposition true:
+just map @code{N} to the constant @code{2}.
+
+Now consider the goal @samp{append(As, Bs, [1])}.
+In this case the first two arguments are @dfn{free},
+meaning that they are variables that
+are not mapped to anything in the current substitution,
+and the third argument is @dfn{ground},
+meaning that it doesn't contain any variables
+after applying the current substitution.
+As before we try to match (or @dfn{unify}) the goal with a clause,
+but in this case both clauses match!
+We arbitrarily pick the first one,
+but we also push a @dfn{choice point} onto a stack,
+which will allow us to return to this point later on
+and try the other clause if we need to.
+Matching with the first clause gives us
+the substitution @code{As @expansion{} [], Bs @expansion{} [1]}.
+Since this clause is a fact,
+we succeed with this substitution as our solution.
+
+If a later goal fails,
+we pop the previous choice point off the stack
+in order to search for a different solution.
+This time we want to try unifying our goal with
+the head of the second clause.
+That is, we want to find a substitution such that
+ at code{append(As, Bs, [1]) = append([X1 | As1], Bs1, [X1 | Cs1])}.
+(The variables from the clause have been given a numerical suffix,
+which is to indicate that they came from a different scope
+and are not the same variables as those in the goal.)
+The substitution we use is
+ at code{As @expansion{} [1 | As1], Bs @expansion{} Bs1, X1 @expansion{} 1, Cs1 @expansion{} []};
+you can check that this does indeed unify the two terms.
+Note that information is effectively flowing in both directions:
+variables from both the goal and the clause
+(i.e.@: the caller and callee) are bound by this substitution.
+This is a key difference from pattern matching in many other languages,
+in which only variables in the pattern are bound.
+
+Applying this substitution to the body of the selected clause
+gives us our new goal,
+ at samp{append(As1, Bs1, [])}.
+This time only the first clause matches,
+with the substitution of @code{As1 @expansion{} [], Bs1 @expansion{} []}.
+The clause is a fact,
+so this is a solution to @emph{this} call to append.
+To find the solution to the parent goal we compose this substitution
+with the one from before,
+giving @code{As @expansion{} [1], Bs @expansion{} []}.
+We have now found two solutions for our goal:
+one with @code{As} being the empty list and @code{Bs} being @code{[1]},
+and the other with the bindings for @code{As} and @code{Bs} swapped.
+These are all of the possible solutions;
+if we wanted to search for another
+we would find the choice point stack to be empty,
+hence we would fail.
+
+One final observation is worth making before we finish this section.
+We saw earlier that the arguments at the start of the call
+were either free or ground;
+in each solution we see that the arguments are all ground.
+We consider arguments that are ground at the start to be inputs,
+and arguments that are free at the start and ground at the end
+to be outputs.
+The pattern of inputs and outputs for a predicate or function call
+is known as its @dfn{mode};
+we can declare the mode we have used here as follows.
+
+ at example
+:- mode append(out, out, in) is multi.
+ at end example
+
+ at noindent
+More information can be found in later chapters;
+also, see the Mercury Library Reference Manual
+for the full set of modes declared for @samp{append/3}.
+
+ at node Goals
+ at section Goals
+
+A goal is a term of one of the following forms.
+
+ at table @code
+ at item @var{Goal1}, @var{Goal2}
A conjunction.
@var{Goal1} and @var{Goal2} must be valid goals.
- at item @code{@var{Goal1} & @var{Goal2}}
+ at item @var{Goal1} & @var{Goal2}
A parallel conjunction.
This has the same declarative semantics as the normal conjunction.
Operationally,
@@ -800,62 +1360,43 @@ It is an error for @var{Goal1} or @var{Goal2}
to have a determinism other than @code{det} or @code{cc_multi}.
@xref{Determinism categories}.
- at item @code{@var{Goal1} ; @var{Goal2}}
+ at item @var{Goal1} ; @var{Goal2}
where @var{Goal1} is not of the form
@samp{@var{Goal1a} -> @var{Goal1b}}: a disjunction.
@var{Goal1} and @var{Goal2} must be valid goals.
- at item @code{true}
+ at item true
The empty conjunction.
-Always succeeds.
+Always succeeds exactly once.
- at item @code{fail}
+ at item fail
The empty disjunction.
Always fails.
- at item @code{not @var{Goal}}
- at itemx @code{\+ @var{Goal}}
-A negation.
-The two different syntaxes have identical semantics.
- at var{Goal} must be a valid goal.
-Both forms are equivalent to @samp{if @var{Goal} then fail else true}.
-
- at item @code{@var{Goal1} => @var{Goal2}}
-An implication.
-This is an abbreviation for @samp{not (@var{Goal1}, not @var{Goal2})}.
-
- at item @code{@var{Goal1} <= @var{Goal2}}
-A reverse implication.
-This is an abbreviation for @samp{not (@var{Goal2}, not @var{Goal1})}.
-
- at item @code{@var{Goal1} <=> @var{Goal2}}
-A logical equivalence.
-This is an abbreviation for
- at samp{(@var{Goal1} => @var{Goal2}), (@var{Goal1} <= @var{Goal2}}).
-
- at item @code{if @var{CondGoal} then @var{ThenGoal} else @var{ElseGoal}}
- at itemx @code{@var{CondGoal} -> @var{ThenGoal} ; @var{ElseGoal}}
+ at item if @var{CondGoal} then @var{ThenGoal} else @var{ElseGoal}
+ at itemx @var{CondGoal} -> @var{ThenGoal} ; @var{ElseGoal}
An if-then-else.
The two different syntaxes have identical semantics.
@var{CondGoal}, @var{ThenGoal}, and @var{ElseGoal} must be valid goals.
Note that the ``else'' part is @emph{not} optional.
The declarative semantics of an if-then-else is given by
- at code{( @var{CondGoal}, @var{ThenGoal} ; not(@var{CondGoal}), @var{ElseGoal})},
-but the operational semantics are different,
+ at code{( @var{CondGoal}, @var{ThenGoal} ; not(@var{CondGoal}), @var{ElseGoal} )},
+but the operational semantics is different,
and it is treated differently for the purposes of determinism inference
(@pxref{Determinism}).
Operationally, it executes the @var{CondGoal},
and if that succeeds, then execution continues with the @var{ThenGoal};
otherwise, i.e.@: if @var{CondGoal} fails, it executes the @var{ElseGoal}.
-Note that @var{CondGoal} can be nondeterministic ---
-unlike Prolog, Mercury's if-then-else does not commit
+Note that @var{CondGoal} can be nondeterministic---unlike Prolog,
+Mercury's if-then-else does not commit
to the first solution of the condition if the condition succeeds.
If @var{CondGoal} is an explicit existential quantification,
@code{some @var{Vars} @var{QuantifiedCondGoal}}, then the variables @var{Vars}
are existentially quantified over the conjunction of the goals
- at var{QuantifiedCondGoal} and @var{ThenGoal}.
+ at var{QuantifiedCondGoal} and @var{ThenGoal}
+(see existential quantifications, below).
Explicit existential quantifications that occur as subgoals of @var{CondGoal}
do @emph{not} affect the scope of variables in the ``then'' part.
For example, in
@@ -876,57 +1417,111 @@ the variable @var{V} is only quantified over @var{C}
because the top-level goal of the condition
is not an explicit existential quantification.
- at item @code{@var{Term1} = @var{Term2}}
+ at item not @var{Goal}
+ at itemx \+ @var{Goal}
+A negation.
+The two different syntaxes have identical semantics.
+ at var{Goal} must be a valid goal.
+Both forms are equivalent to @samp{if @var{Goal} then fail else true}.
+
+ at item @var{Expr1} = @var{Expr2}
A unification.
- at var{Term1} and @var{Term2} must be valid data-terms.
+ at var{Expr1} and @var{Expr2} must be valid expressions.
- at item @code{@var{Term1} \= @var{Term2}}
+ at item @var{Expr1} \= @var{Expr2}
An inequality.
- at var{Term1} and @var{Term2} must be valid data-terms.
-This is an abbreviation for @samp{not (@var{Term1} = @var{Term2})}.
+ at var{Expr1} and @var{Expr2} must be valid expressions.
+This is an abbreviation for @samp{not (@var{Expr1} = @var{Expr2})}.
- at item @code{call(Closure)}
- at itemx @code{call(Closure1, Arg1)}
- at itemx @code{call(Closure2, Arg1, Arg2)}
- at itemx @code{call(Closure3, Arg1, Arg2, Arg3)}
+ at item some @var{Vars} @var{Goal}
+An existential quantification.
+ at var{Goal} must be a valid goal.
+ at var{Vars} must be a list
+whose elements are either variables or state variables.
+(A single list may contain both.)
+The case where they are state variables
+is described in @ref{State variables};
+here we discuss the case where they are plain variables.
+
+Each existential quantification introduces a new scope.
+The variables in @var{Vars} are local to the goal @var{Goal}:
+for each variable named in @var{Vars},
+any occurrences of variables with that name in @var{Goal}
+are considered to name a different variable
+than any variables with the same name
+that occur outside of the existential quantification.
+
+Operationally, existential quantification has no effect,
+so apart from its effect on variable scoping,
+ at samp{some @var{Vars} @var{Goal}} is the same as @samp{@var{Goal}}.
+
+Mercury's rules for implicit quantification (@pxref{Implicit quantification})
+mean that variables are often implicitly existentially quantified.
+There is usually no need to write existential quantifiers explicitly.
+
+ at item all @var{Vars} @var{Goal}
+A universal quantification.
+ at var{Goal} must be a valid goal.
+ at var{Vars} must be a list of variables
+(they may @emph{not} be state variables).
+This goal is an abbreviation for @samp{not (some @var{Vars} not @var{Goal})}.
+
+ at item @var{Goal1} => @var{Goal2}
+An implication.
+This is an abbreviation for @samp{not (@var{Goal1}, not @var{Goal2})}.
+
+ at item @var{Goal1} <= @var{Goal2}
+A reverse implication.
+This is an abbreviation for @samp{not (@var{Goal2}, not @var{Goal1})}.
+
+ at item @var{Goal1} <=> @var{Goal2}
+A logical equivalence.
+This is an abbreviation for
+ at samp{(@var{Goal1} => @var{Goal2}), (@var{Goal1} <= @var{Goal2}}).
+
+ at item call(Closure)
+ at itemx call(Closure1, Arg1)
+ at itemx call(Closure2, Arg1, Arg2)
+ at itemx call(Closure3, Arg1, Arg2, Arg3)
@itemx @dots{}
-A higher-order predicate call.
-The closure and arguments must be valid data-terms.
+A higher-order predicate call
+(ordinary first-order predicate calls are documented below).
+The closure and arguments must be valid expressions.
@samp{call(Closure)} just calls the specified closure.
The other forms append the specified arguments
onto the argument list of the closure before calling it.
@xref{Higher-order}.
- at item @code{Var}
- at itemx @code{Var(Arg1)}
- at itemx @code{Var(Arg2)}
- at itemx @code{Var(Arg2, Arg3)}
+ at item Expr
+ at itemx Expr(Arg1)
+ at itemx Expr(Arg1, Arg2)
+ at itemx Expr(Arg1, Arg2, Arg3)
@itemx @dots{}
A higher-order predicate call.
- at var{Var} must be a variable.
-The semantics are exactly the same as for the corresponding higher-order call
+ at var{Expr} must be a valid expression.
+The semantics are the same as for the corresponding higher-order call
using the @code{call/N} syntax,
-i.e.@: @samp{call(Var)}, @samp{call(Var, Arg1)}, etc.
+i.e.@: @samp{call(Expr)}, @samp{call(Expr, Arg1)}, etc.
- at item @code{promise_pure @var{Goal}}
+ at item promise_pure @var{Goal}
A purity cast.
@var{Goal} must be a valid goal.
This goal promises that @var{Goal} implements a pure interface,
even though it may include impure and semipure components.
- at item @code{promise_semipure @var{Goal}}
+ at item promise_semipure @var{Goal}
A purity cast.
@var{Goal} must be a valid goal.
This goal promises that @var{Goal} implements a semipure interface,
even though it may include impure components.
- at item @code{promise_impure @var{Goal}}
+ at item promise_impure @var{Goal}
A purity cast.
@var{Goal} must be a valid goal.
This goal instructs the compiler to treat @var{Goal} as though it were impure,
regardless of its actual purity.
- at item @code{promise_equivalent_solutions @var{Vars} @var{Goal}}
+ at item promise_equivalent_solutions @var{Vars} @var{Goal}
A determinism cast.
@var{Vars} must be a list of variables.
@var{Goal} must be a valid goal.
@@ -947,12 +1542,13 @@ If @var{Goal} has determinism @code{nondet} or @code{cc_nondet} then
@code{promise_equivalent_solutions @var{Vars} @var{Goal}}
has determinism @code{semidet}.
- at item @code{promise_equivalent_solution_sets @var{Vars} @var{Goal}}
+ at item promise_equivalent_solution_sets @var{Vars} @var{Goal}
A determinism cast,
of the kind performed by @code{promise_equivalent_solutions},
on any goals of the form
@code{arbitrary @var{ArbVars} @var{ArbGoal}} inside @var{Goal},
of which there should be at least one.
+ at c XXX "should" or "must"?
@var{Vars} and @var{ArbVars} must be lists of variables,
and @var{Goal} and @var{ArbGoal} must be valid goals.
@var{Vars} must be the set of variables bound by @var{Goal},
@@ -991,14 +1587,14 @@ Goals of the form @code{arbitrary @var{ArbVars} @var{ArbGoal}}
are not allowed to occur outside
@code{promise_equivalent_solution_sets @var{Vars} @var{Goal}} goals.
- at item @code{require_det @var{Goal}}
- at itemx @code{require_semidet @var{Goal}}
- at itemx @code{require_multi @var{Goal}}
- at itemx @code{require_nondet @var{Goal}}
- at itemx @code{require_cc_multi @var{Goal}}
- at itemx @code{require_cc_nondet @var{Goal}}
- at itemx @code{require_erroneous @var{Goal}}
- at itemx @code{require_failure @var{Goal}}
+ at item require_det @var{Goal}
+ at itemx require_semidet @var{Goal}
+ at itemx require_multi @var{Goal}
+ at itemx require_nondet @var{Goal}
+ at itemx require_cc_multi @var{Goal}
+ at itemx require_cc_nondet @var{Goal}
+ at itemx require_erroneous @var{Goal}
+ at itemx require_failure @var{Goal}
A determinism check, typically used to enhance the robustness of code.
@var{Goal} must be a valid goal.
If @var{Goal} is det, then
@@ -1016,7 +1612,7 @@ The @code{require_det} keyword may be replaced with
@code{require_failure},
each of which requires @var{Goal} to have the named determinism.
- at item @code{require_complete_switch [@var{Var}] @var{Goal}}
+ at item require_complete_switch [@var{Var}] @var{Goal}
A switch completeness check, typically used to enhance the robustness of code.
If @var{Goal} is a switch on @var{Var}
and the switch is @emph{complete},
@@ -1028,14 +1624,14 @@ If @var{Goal} is a switch on @var{Var} but is @emph{not} complete,
or @var{Goal} is not a switch on @var{Var} at all,
then the compiler is required to generate an error message.
- at item @code{require_switch_arms_det [@var{Var}] @var{Goal}}
- at itemx @code{require_switch_arms_semidet [@var{Var}] @var{Goal}}
- at itemx @code{require_switch_arms_multi [@var{Var}] @var{Goal}}
- at itemx @code{require_switch_arms_nondet [@var{Var}] @var{Goal}}
- at itemx @code{require_switch_arms_cc_multi [@var{Var}] @var{Goal}}
- at itemx @code{require_switch_arms_cc_nondet [@var{Var}] @var{Goal}}
- at itemx @code{require_switch_arms_erroneous [@var{Var}] @var{Goal}}
- at itemx @code{require_switch_arms_failure [@var{Var}] @var{Goal}}
+ at item require_switch_arms_det [@var{Var}] @var{Goal}
+ at itemx require_switch_arms_semidet [@var{Var}] @var{Goal}
+ at itemx require_switch_arms_multi [@var{Var}] @var{Goal}
+ at itemx require_switch_arms_nondet [@var{Var}] @var{Goal}
+ at itemx require_switch_arms_cc_multi [@var{Var}] @var{Goal}
+ at itemx require_switch_arms_cc_nondet [@var{Var}] @var{Goal}
+ at itemx require_switch_arms_erroneous [@var{Var}] @var{Goal}
+ at itemx require_switch_arms_failure [@var{Var}] @var{Goal}
@code{require_switch_arms_det} is a determinism check,
typically used to enhance the robustness of code.
@var{Goal} must be a valid goal.
@@ -1068,8 +1664,8 @@ in a @code{require_switch_arms_semidet} scope,
even though it would not be ok
to have a det goal in a @code{require_semidet} scope.
- at item @code{disable_warnings [@var{Warning}] @var{Goal}}
- at itemx @code{disable_warning [@var{Warning}] @var{Goal}}
+ at item disable_warnings [@var{Warning}] @var{Goal}
+ at itemx disable_warning [@var{Warning}] @var{Goal}
The Mercury compiler can generate warnings
about several kinds of constructs that whose legal Mercury semantics
is likely to differ from the semantics intended by the programmer.
@@ -1088,20 +1684,20 @@ whose names appear in @code{[@var{Warning}]}.
At the moment, the Mercury compiler supports the disabling of
the following warning categories:
- at table @asis
- at item @code{singleton_vars}
+ at table @code
+ at item singleton_vars
Disable the generation of singleton variable warnings.
- at item @code{suspected_occurs_check_failure}
+ at item suspected_occurs_check_failure
Disable the generation of warnings about code that looks like
it unifies a variable with a term that contains that same variable.
@c @item @code{non_tail_recursive_calls}
@c Disable the generation of warnings about recursive calls
@c that are not @emph{tail}-recursive calls.
- at item @code{suspicious_recursion}
+ at item suspicious_recursion
Disable the generation of warnings about suspicious recursive calls.
- at item @code{no_solution_disjunct}
+ at item no_solution_disjunct
Disable the generation of warnings about disjuncts that can have no solution.
-This is usually done to shut up such a warning a multi-mode predicate
+This is usually done to shut up such a warning in a multi-mode predicate
where the disjunct in question is a switch arm in another mode.
(The difference is that a disjunct that cannot succeed has no meaningful use,
but a switch arm that cannot succeed does have one:
@@ -1119,7 +1715,7 @@ This is intended to make the code read more naturally
regardless of whether the list contains the name of
more than one disabled warning category.
- at item @code{trace @var{Params} @var{Goal}}
+ at item trace @var{Params} @var{Goal}
A trace goal, typically used for debugging or logging.
@var{Goal} must be a valid goal;
@var{Params} must be a valid list of trace parameters.
@@ -1136,7 +1732,7 @@ but to be confined to the provision of extra information
for the user of the program.
See @ref{Trace goals} for the details.
- at item @code{try @var{Params} @var{Goal} @dots{} catch @var{Term} -> @var{CGoal} @dots{}}
+ at item try @var{Params} @var{Goal} @dots{} catch @var{Expr} -> @var{CGoal} @dots{}
A try goal.
Exceptions thrown during the execution of @var{Goal} may be caught and handled.
A summary of the try goal syntax is:
@@ -1146,7 +1742,7 @@ A summary of the try goal syntax is:
try @var{Params} @var{Goal}
then @var{ThenGoal}
else @var{ElseGoal}
- catch @var{Term} -> @var{CatchGoal}
+ catch @var{Expr} -> @var{CatchGoal}
@dots{}
catch_any @var{CatchAnyVar} -> @var{CatchAnyGoal}
@end group
@@ -1154,20 +1750,20 @@ A summary of the try goal syntax is:
See @ref{Exception handling} for the full details.
- at item @code{event @var{Goal}}
+ at item event @var{Goal}
An event goal.
@var{Goal} must be a predicate call.
Event goals are an extension used by the Melbourne Mercury implementation
to support user defined events in the Mercury debugger, @samp{mdb}.
See the ``Debugging'' chapter of the Mercury User's Guide for further details.
- at item @code{@var{Call}}
+ at item @var{Call}
Any goal which does not match any of the above forms
-must be a predicate call.
-The top-level functor of the term determines the predicate called;
-the predicate must be declared in a @code{pred} declaration
-in the module or in the interface of an imported module.
-The arguments must be valid data-terms.
+is a predicate call.
+This must be a functor term;
+the principal functor determines the predicate called,
+which must be visible (@pxref{Modules}).
+The arguments, if present, must be valid expressions.
@end table
@@ -1179,17 +1775,17 @@ as a shorthand for naming intermediate values in a sequence.
That is, where in the plain syntax one might write
@example
main(IO0, IO) :-
- io.write_string("The answer is ", IO0, IO1),
- io.write_int(calculate_answer(@dots{}), IO1, IO2),
- io.nl(IO3, IO).
+ write_string("The answer is ", IO0, IO1),
+ write_int(calculate_answer(@dots{}), IO1, IO2),
+ nl(IO3, IO).
@end example
@noindent
using state variable syntax one could write
@example
main(!IO) :-
- io.write_string("The answer is ", !IO),
- io.write_int(calculate_answer(@dots{}), !IO),
- io.nl(!IO).
+ write_string("The answer is ", !IO),
+ write_int(calculate_answer(@dots{}), !IO),
+ nl(!IO).
@end example
A state variable is written @samp{!. at var{X}} or @samp{!:@var{X}},
@@ -1198,7 +1794,7 @@ An argument @samp{!@var{X}} is shorthand
for two state variable arguments @samp{!. at var{X}, !:@var{X}};
that is,
@samp{p(@dots{}, !@var{X}, @dots{})}
-is parsed as
+is equivalent to
@samp{p(@dots{}, !. at var{X}, !:@var{X}, @dots{})}.
State variables obey special scope rules.
@@ -1209,19 +1805,19 @@ and this can happen in one of four ways:
As @samp{!@var{X}} in the head of a clause.
In this case,
references to state variable @samp{!@var{X}} or to its components
-may appear anywhere in the clause.
+may appear in the clause.
@item
As either @samp{!. at var{X}} or @samp{!:@var{X}} or both
in the head of a clause.
Again, in this case,
references to state variable @samp{!@var{X}} or to its components
-may appear anywhere in the clause.
+may appear in the clause.
@item
As either @samp{!. at var{X}} or @samp{!:@var{X}} or both
in the head of a lambda expression.
In this case,
references to state variable @samp{!@var{X}} or to its components
-may appear anywhere in that lambda expression.
+may appear in that lambda expression.
(The reason that @samp{!@var{X}} may not appear as a parameter term
in the head of a lambda is that
there is no syntax for specifying the modes of the two implied parameters.)
@@ -1229,7 +1825,7 @@ there is no syntax for specifying the modes of the two implied parameters.)
In an explicit quantification such as @samp{some [!@var{X}] @var{Goal}}.
In this case,
references to state variable @samp{!@var{X}} or to its components
-may appear anywhere in @samp{@var{Goal}}.
+may appear in @samp{@var{Goal}}.
@end itemize
A state variable @var{X} in the enclosing scope
@@ -1238,30 +1834,28 @@ may only be referred to as @samp{!. at var{X}}
(unless the enclosing @var{X} is shadowed
by a more local state variable of the same name.)
-For instance, the following clause employing a lambda expression
+For instance, the following clause employs a lambda expression
+and is illegal because
+it implicitly refers to @samp{!:@var{S}} inside the lambda expression.
@example
p(@var{A}, @var{B}, !@var{S}) :-
- F =
- ( pred(@var{C}::in, @var{D}::out) is det :-
+ P = ( pred(@var{C}::in, @var{D}::out) is det :-
q(@var{C}, @var{D}, !@var{S})
),
- ( if F(@var{A}, @var{E}) then
+ ( if P(@var{A}, @var{E}) then
@var{B} = @var{E}
else
@var{B} = @var{A}
).
@end example
@noindent
-is illegal because
-it implicitly refers to @samp{!:@var{S}} inside the lambda expression.
However
@example
p(@var{A}, @var{B}, !@var{S}) :-
- F =
- ( pred(@var{C}::in, @var{D}::out, !. at var{S}::in, !:@var{S}::out) is det :-
+ P = ( pred(@var{C}::in, @var{D}::out, !. at var{S}::in, !:@var{S}::out) is det :-
q(@var{C}, @var{D}, !@var{S})
),
- ( if F(@var{A}, @var{E}, !@var{S}) then
+ ( if P(@var{A}, @var{E}, !@var{S}) then
@var{B} = @var{E}
else
@var{B} = @var{A}
@@ -1282,11 +1876,13 @@ whether they are defined by clauses or lambda expressions.
@samp{!@var{X}} is not a legal function result,
because it stands for two arguments, rather than one.
@item
- at samp{!@var{X}} may not appear as an argument in a function application,
+Neither @samp{!@var{X}} nor @samp{!:@var{X}}
+may appear as an argument in a function application,
because this would not make sense
given the usual interpretation of state variables and functions.
+ at c XXX it appears the implementation does actually allow !:X
(The default mode of functions is that all arguments are input,
-while in the overwhelming majority of cases, @samp{!:@var{X}} is output.)
+while in typical usage, @samp{!:@var{X}} is output.)
@end itemize
Within each clause, the compiler
@@ -1327,10 +1923,10 @@ These cases are as follows.
@item Calls
Given a first order call such as
- at samp{@var{predname}(@var{ArgTerm1}, ..., @var{ArgTermN})}
+ at samp{@var{predname}(@var{Arg1}, ..., @var{ArgN})}
or a higher-order call such as
- at samp{@var{PredVar}(@var{ArgTerm1}, ..., @var{ArgTermN})},
-if any of the @var{ArgTermI} is !@var{X},
+ at samp{@var{Expr}(@var{Arg1}, ..., @var{ArgN})},
+if any of the arguments is !@var{X},
@samp{transform_goal} replaces that argument with two arguments:
!. at var{X} and !:@var{X}.
It then checks whether
@@ -1342,63 +1938,65 @@ If it does, then it replaces @var{Call} with
substitute(@var{Call}, [!. at var{X} -> @var{CurX}, !:@var{X} -> @var{NextX}])
@end example
@item
-If it does not, then it replaces @var{AtomicGoal} with
+If it does not, then it replaces @var{Call} with
@example
substitute(@var{Call}, [!. at var{X} -> @var{CurX}]),
@var{NextX} = @var{CurX}
@end example
@end itemize
Note that !. at var{X} can occur in @var{Call} on its own
-(i.e. without !:@var{X}).
+(i.e.@: without !:@var{X}).
Likewise, !:@var{X} can occur in @var{Call} without !. at var{X},
but this does not need separate handling.
-Note that @var{PredVar} in a higher-order call
-may not be a reference to a state var,
-i.e it may not be !@var{X}, !. at var{X} or !:@var{X}.
+The expression @var{Expr} in a higher-order call
+may not be of the form !@var{X}, !. at var{X} or !:@var{X}.
+It may be parenthesised as (!. at var{X}), however.
@item Unifications
-In a unification @samp{@var{TermA} = @var{TermB}},
-each of @var{TermA} and @var{TermB}
+In a unification @samp{@var{ExprA} = @var{ExprB}},
+each of @var{ExprA} and @var{ExprB}
+are expressions that
may have one of the following four forms:
@itemize
@item
-The term may be !. at var{S} for some state variable @var{S}.
+The expression may be !. at var{S} for some state variable @var{S}.
If @var{S} is @var{X},
-then @samp{transform_goal} replaces the term with @var{CurX}.
+then @samp{transform_goal} replaces the expression with @var{CurX}.
@item
-The term may be !:@var{S} for some state variable @var{S}.
+The expression may be !:@var{S} for some state variable @var{S}.
If @var{S} is @var{X},
-then @samp{transform_goal} replaces the term with @var{NextX}.
+then @samp{transform_goal} replaces the expression with @var{NextX}.
@item
-The term may be a plain variable
-(i.e. variable that does not refer to any state variable).
- at samp{transform_goal} leaves such terms unchanged.
+The expression may be a name, a constant,
+or a variable that is not a state variable,
+ at samp{transform_goal} leaves such expressions unchanged.
@item
-The term may be a non-variable term, which means that
+The expression may be a compound term, which means that
it must have the form
@samp{@var{f}(@var{ArgTerm1}, ..., @var{ArgTermN})}.
- at samp{transform_goal} handles these the same way it handles first order calls.
+ at samp{transform_goal} handles these the same way it handles
+function applications.
@end itemize
-Note that @var{TermA} and @var{TermB} may not have the form !@var{S}.
+Note that @var{ExprA} and @var{ExprB} may not have the form !@var{S}.
@item State variable field updates
A state variable field update goal has the form
@example
-!@var{S} ^ @var{field_list} := @var{Term}
+!@var{S} ^ @var{field_list} := @var{Expr}
@end example
-where @var{field_list} is a valid field list @xref{Record syntax}.
+where @var{field_list} is a valid field list @xref{Field access expressions}.
This means that
@example
-!@var{S} ^ @var{field1} := @var{Term}
-!@var{S} ^ @var{field1} ^ @var{field2} := @var{Term}
-!@var{S} ^ @var{field1} ^ @var{field2} ^ @var{field3} := @var{Term}
+!@var{S} ^ @var{field1} := @var{Expr}
+!@var{S} ^ @var{field1} ^ @var{field2} := @var{Expr}
+!@var{S} ^ @var{field1} ^ @var{field2} ^ @var{field3} := @var{Expr}
@end example
are all valid field update goals.
If @var{S} is @var{X},
@samp{transform_goal} replaces such goals with
@example
- at var{NextX} = @var{CurX} ^ @var{field_list} := @var{Term}
+ at var{NextX} = @var{CurX} ^ @var{field_list} := @var{Expr}
@end example
Otherwise, it leaves the goal unchanged.
@@ -1453,7 +2051,7 @@ so what the value of !:@var{X} would be if it @emph{did} succeed is moot.
Therefore @samp{transform_goal} returns empty disjunctions unchanged.
@item Negations
-Given a negated goal of the form @samp{not @var{NegatedGoal}}
+Given a negated goal of the form @samp{not @var{NegatedGoal}},
@samp{transform_goal}
@itemize
@item creates a fresh variable @var{DummyX}, and then
@@ -1675,35 +2273,6 @@ compute_out(InA, InB, InsC, Out) :-
@end example
@end table
- at node DCG-rules
- at section DCG-rules
-
-Definite Clause Grammar notation
-is intended for writing parsers and sequence generators in a particular style;
-in the past it has also been used to thread an implicit state variable,
-typically the I/O state, through code.
-As a matter of style, we recommend that
-in future DCG notation be reserved for writing parsers and sequence generators,
-and that state variable syntax be used for passing state threads.
-
-DCG-rules in Mercury have identical syntax and semantics
-to DCG-rules in Prolog.
-
-A DCG-rule is an item of the form @samp{@var{Head} --> @var{Body}}.
-The @var{Head} term must not be a variable.
-A DCG-rule is an abbreviation for an ordinary rule
-with two additional implicit arguments appended to the arguments of @var{Head}.
-These arguments are fresh variables,
-which we shall call @var{V_in} and @var{V_out}.
-The @var{Body} must be a valid DCG-goal,
-and is an abbreviation for an ordinary goal.
-The next section defines a mathematical function
- at samp{DCG-transform(@var{V_in}, @var{V_out}, @var{DCG-goal})}
-which specifies the semantics
-of how DCG goals are transformed into ordinary goals.
-(The @samp{DCG-transform} function is purely for the purposes of exposition,
-to define the semantics --- it is not part of the language.)
-
@node DCG-goals
@section DCG-goals
@@ -1777,7 +2346,7 @@ Unifies the implicit DCG input variable V_in,
which must have type @samp{list(_)},
with a list whose initial elements are the terms specified
and whose tail is the implicit DCG output variable V_out.
-The terms must be valid data-terms.
+The terms must be valid expressions.
Semantics:
@example
@@ -1824,7 +2393,7 @@ else
@item =(@var{Term})
A DCG unification.
Unifies @var{Term} with the implicit DCG argument.
- at var{Term} must be a valid data-term.
+ at var{Term} must be a valid expression.
Semantics:
@example
@@ -1835,7 +2404,7 @@ transform(V_in, V_out, =(Term)) = (Term = V_in, V_out = V_in)
A DCG output unification.
Unifies @var{Term} with the implicit DCG output argument,
ignoring the input DCG argument.
- at var{Term} must be a valid data-term.
+ at var{Term} must be a valid expression.
Semantics:
@example
@@ -1846,9 +2415,9 @@ transform(V_in, V_out, :=(Term)) = (V_out = Term)
A DCG field selection.
Unifies @var{Term} with the result of
applying the field selection @var{field_list} to the implicit DCG argument.
- at var{Term} must be a valid data-term.
+ at var{Term} must be a valid expression.
@var{field_list} must be a valid field list.
- at xref{Record syntax}.
+ at xref{Field access expressions}.
Semantics:
@example
@@ -1859,9 +2428,9 @@ transform(V_in, V_out, Term =^ field_list) =
@item ^ @var{field_list} := @var{Term}
A DCG field update.
Replaces a field in the implicit DCG argument.
- at var{Term} must be a valid data-term.
+ at var{Term} must be a valid expression.
@var{field_list} must be a valid field list.
- at xref{Record syntax}.
+ at xref{Field access expressions}.
Semantics:
@example
@@ -1873,6 +2442,7 @@ transform(V_in, V_out, ^ field_list := Term) =
Any term which does not match any of the above forms
must be a DCG predicate call.
If the term is a variable @var{Var},
+ at c XXX Var can be a Term now
it is treated as if it were @samp{call(@var{Var})}.
Then, the two implicit DCG arguments are appended to the specified arguments.
@@ -1884,64 +2454,32 @@ p(A1, @dots{}, AN, V_in, V_out)
@end table
- at node Data-terms
- at section Data-terms
-
-Syntactically, a data-term is just a term.
-
-There are a couple of differences from Prolog.
-The first one is that double-quoted strings are atomic in Mercury,
-they are not abbreviations for lists of character codes.
-The second is that Mercury provides several extensions to Prolog's term syntax:
-Mercury terms may contain
-record field selection and field update expressions,
-conditional (if-then-else) expressions,
-function applications,
-higher-order function applications,
-lambda expressions,
-and explicit type qualifications.
-
-A data-term is either
-a variable, a data-functor, or a special data-term.
-A special data-term is
+ at node Expressions
+ at section Expressions
+
+Syntactically, an expression is just a term.
+Semantically, an expression is
+a variable,
+a literal,
+a functor expression,
+or a special expression.
+A special expression is
a conditional expression,
-a record syntax expression,
a unification expression,
+an explicit type qualification,
+a type conversion expression,
a lambda expression,
-a higher-order function application,
-or an explicit type qualification.
-
- at menu
-* Data-functors::
-* Record syntax::
-* Unification expressions::
-* Conditional expressions::
-* Lambda expressions::
-* Higher-order function applications::
-* Explicit type qualification::
-* Type conversion expressions::
- at end menu
-
- at node Data-functors
- at subsection Data-functors
-
-A data-functor is an integer, a float, a string,
-a name, an implementation-defined literal, or a compound data-term.
-
-Character literals are written as single-character names,
-quoted or unquoted.
-If the character is an operator,
-it will be necessary to enclose the name within parentheses
-in some contexts,
-e.g.@: @t{(':')}.
-
-A compound data-term is a compound term
-which does not match the form of a special data-term (@pxref{Data-terms}),
-and whose arguments are data-terms.
-If a data-functor is a name or a compound data-term,
-its top-level functor must name
-a function, predicate, or data constructor
-declared in the module or in the interface of an imported module.
+an apply expression,
+or a field access expression.
+Note that many terms are interpreted as expressions by Mercury
+in the same way as in Prolog.
+Special expressions, however,
+extend the functionality of Prolog.
+Both special and non-special expressions are covered in this section.
+
+A literal is an integer, a float, a string,
+or an implementation-defined literal
+(note that character literals are a kind of atom; see below).
Implementation-defined literals are symbolic names
whose value represents a property of the compilation environment
@@ -1949,142 +2487,86 @@ or the context in which it appears.
The implementation replaces these symbolic names
with actual constants during compilation.
Implementation-defined literals can only appear within clauses.
-The following literals must be supported by all Mercury implementations:
+The following must be supported by all Mercury implementations:
- at table @asis
- at item @samp{$file}
-a string that gives the name of the file
+ at table @samp
+ at item $file
+A string that gives the name of the file
that contains the module being compiled.
If the name of the file cannot be determined,
then it is replaced by an arbitrary string.
- at item @samp{$line}
-the line number (integer) of the goal in which the literal appears,
+ at item $line
+The line number (integer) of the goal in which the literal appears,
or -1 if it cannot be determined.
- at item @samp{$module}
-a string representation of the fully qualified module name.
+ at item $module
+A string representation of the fully qualified module name.
- at item @samp{$pred}
-a string containing the fully qualified predicate or function name and arity.
+ at item $pred
+A string containing the fully qualified predicate or function name and arity.
@end table
+ at noindent
The Melbourne Mercury implementation
additionally supports the following extension:
- at table @asis
- at item @samp{$grade}
-the grade (string) in which the module is compiled.
+ at table @samp
+ at item $grade
+The grade (string) in which the module is compiled.
@end table
- at node Record syntax
- at subsection Record syntax
-
-Record syntax provides a convenient way
-to select or update fields of data constructors,
-independent of the definition of the constructor.
-Record syntax expressions are transformed into
-sequences of calls to field selection or update functions
-(@pxref{Field access functions}).
-
-A field specifier is a name or a compound data-term.
-A field list is a list of field specifiers separated by @code{^}.
- at code{field}, @code{field1 ^ field2} and @code{field1(A) ^ field2(B, C)}
-are all valid field lists.
-
-If the top-level functor of a field specifier is @samp{@var{field}/N},
-there must be a visible selection function @samp{@var{field}/(N + 1)}.
-If the field specifier occurs in a field update expression,
-there must also be a visible update function
-named @samp{'@var{field} :='/(N + 2)}.
-
-Record syntax expressions have one of the following forms.
-There are also record syntax DCG goals (@pxref{DCG-goals}),
-which provide similar functionality to record syntax expressions,
-except that they act on the DCG arguments of a DCG clause.
+A functor expression is an atom, which is just a name,
+or a compound expression,
+which is a compound term
+that does not match the form of a special expression,
+and whose arguments are expressions.
+If a functor expression is not a character literal,
+its principal functor must be the name of
+a visible function, predicate, or data constructor
+(except for field specifiers,
+for which the corresponding field access function must be visible;
+see below).
+
+Character literals in Mercury are just atoms with a single character,
+possibly quoted.
+Since they sometimes require quotes
+and sometimes require parentheses,
+for code consistency we recommend
+writing all character literals with quotes and
+(except where used as arguments)
+parentheses.
+For example, @code{Char = ('+') ; Char = ('''')}.
+
+Special expressions
+(not including field access expressions,
+which are covered below)
+take one of the following forms.
@table @code
- at item @var{Term} ^ @var{field_list}
-
-A field selection.
-For each field specifier in @var{field_list},
-apply the corresponding selection function in turn.
-
- at var{Term} must be a valid data-term.
- at var{field_list} must be a valid field list.
-
-A field selection is transformed using the following rules:
- at example
-transform(Term ^ Field(Arg1, @dots{})) = Field(Arg1, @dots{}, Term).
-transform(Term ^ Field(Arg1, @dots{}) ^ Rest) =
- transform(Field(Arg1, @dots{}, Term) ^ Rest).
- at end example
-
-Examples:
-
- at code{Term ^ field} is equivalent to @code{field(Term)}.
-
- at code{Term ^ field(Arg)} is equivalent to @code{field(Arg, Term)}.
-
- at w{@code{Term ^ field1(Arg1) ^ field2(Arg2, Arg3)}} is equivalent
-to @w{@code{field2(Arg2, Arg3, field1(Arg1, Term))}}.
-
- at item @var{Term} ^ @var{field_list} := @var{FieldValue}
-
-A field update, returning a copy of @var{Term}
-with the value of the field specified by @var{field_list}
-replaced with @var{FieldValue}.
-
- at var{Term} must be a valid data-term.
- at var{field_list} must be a valid field list.
-
-A field update is transformed using the following rules:
- at example
-transform(Term ^ Field(Arg1, @dots{}) := FieldValue) =
- 'Field :='(Arg1, @dots{}, Term, FieldValue)).
-
-transform(Term0 ^ Field(Arg1, @dots{}) ^ Rest := FieldValue) = Term :-
- OldFieldValue = Field(Arg1, @dots{}, Term0),
- NewFieldValue = transform(OldFieldValue ^ Rest := FieldValue),
- Term = 'Field :='(Arg1, @dots{}, Term0, NewFieldValue).
- at end example
-
-Examples:
-
- at w{@code{Term ^ field := FieldValue}}
-is equivalent to @w{@code{'field :='(Term, FieldValue)}}.
-
- at w{@code{Term ^ field(Arg) := FieldValue}}
-is equivalent to @w{@code{'field :='(Arg, Term, FieldValue)}}.
-
- at w{@code{Term ^ field1(Arg1) ^ field2(Arg2) := FieldValue}}
-is equivalent to the code
- at example
-OldField1 = field1(Arg1, Term),
-NewField1 = 'field2 :='(Arg2, OldField1, FieldValue),
-Result = 'field1 :='(Arg1, Term, NewField1)
- at end example
-
- at end table
-
- at node Unification expressions
- at subsection Unification expressions
-
-A unification expression is an expression of the form
-
- at example
- at var{X} @@ @var{Y}
- at end example
+ at item if @var{Goal} then @var{ThenExpr} else @var{ElseExpr}
+ at itemx @var{Goal} -> @var{ThenExpr} ; @var{ElseExpr}
+A conditional expression.
+ at var{Goal} is a goal;
+ at var{ThenExpr} and @var{ElseExpr} are both expressions.
+The two forms are equivalent.
+The meaning of a conditional expression is that
+if @var{Goal} is true it is equivalent to @var{ThenExpr},
+otherwise it is equivalent to @var{ElseExpr}.
- at noindent
-where @var{X} and @var{Y} are data-terms.
+If @var{Goal} takes the form @code{some [X, Y, Z] @dots{}}
+then the scope of @var{X}, @var{Y}, and @var{Z} includes @var{ThenExpr}.
+See the related discussion regarding if-then-else goals.
+ at item @var{X} @@ @var{Y}
+A unification expression.
+ at var{X} and @var{Y} are both expressions.
The meaning of a unification expression is that the arguments are unified,
and the expression is equivalent to the unified value.
-The strict sequential operational semantics (@pxref{Semantics})
+The strict sequential operational semantics (@pxref{Formal semantics})
of an expression @w{@code{@var{X} @@ @var{Y}}}
is that the expression is replaced by a fresh variable @code{Z},
and immediately after @code{Z} is evaluated,
@@ -2100,62 +2582,54 @@ p(X @@ f(_, _), X).
is equivalent to
@example
-p(H1, H2) :-
- H1 = X,
- H1 = f(_, _),
- H2 = X.
+p(Z, X) :-
+ Z = X,
+ Z = f(_, _).
@end example
-Unification expressions are most useful when writing switches
-(@pxref{Determinism checking and inference}).
-The arguments of a unification expression
+Unification expressions are particularly useful when writing switches
+(@pxref{Determinism checking and inference}),
+as the arguments of a unification expression
are examined when checking for switches.
The arguments of an equivalent user-defined function would not be.
- at node Conditional expressions
- at subsection Conditional expressions
-
-A conditional expression is an expression of either of the two following forms
-
- at example
-(if @var{Goal} then @var{Expression1} else @var{Expression2})
-(@var{Goal} -> @var{Expression1} ; @var{Expression2})
- at end example
-
- at noindent
- at var{Goal} is a goal;
- at var{Expression1} and @var{Expression2} are both data-terms.
-The semantics of a conditional expression is that
-if @var{Goal} is true,
-then the expression has the meaning of @var{Expression1},
-else the expression has the meaning of @var{Expression2}.
-
-If @var{Goal} takes the form @code{some [X, Y, Z] @dots{}}
-then the scope of @var{X}, @var{Y}, and @var{Z} includes @var{Expression1}.
+ at item @var{Expr} : @var{Type}
+An explicit type qualification.
+ at var{Expr} must be a valid expression,
+and @var{Type} must be a valid type (@pxref{Types}).
+These expressions are occasionally useful to resolve ambiguities
+that can arise from overloading or polymorphic types.
- at node Lambda expressions
- at subsection Lambda expressions
+An explicit type qualification constrains
+the specified expression to have the specified type.
+Apart from that,
+the explicit type qualification is equivalent to @var{Expr}.
-A lambda expression is a compound term of one of the following forms
+Currently we also support
+ at code{@var{Expr} `with_type` @var{Type}}
+as an alternative syntax for explicit type qualification.
- at example
-pred(Arg1::Mode1, Arg2::Mode2, @dots{}) is Det :- Goal
-pred(Arg1::Mode1, Arg2::Mode2, @dots{}, DCGMode0, DCGMode1) is Det --> DCGGoal
-func(Arg1::Mode1, Arg2::Mode2, @dots{}) = (Result::Mode) is Det :- Goal
-func(Arg1, Arg2, @dots{}) = (Result) is Det :- Goal
-func(Arg1, Arg2, @dots{}) = Result :- Goal
- at end example
+ at item coerce(Expr)
+A type conversion expression.
+ at var{Expr} must be a valid expression.
+ at xref{Type conversions}.
- at noindent
-where @var{Arg1}, @var{Arg2}, @dots{} are zero or more data-terms,
- at var{Result} is a data-term,
- at var{Mode1}, @var{Mode2}, @dots{} are zero or more modes (@pxref{Modes}),
- at var{DCGMode0} and @var{DCGMode1} are modes (@pxref{Modes}),
- at var{Det} is a determinism (@pxref{Determinism}),
- at var{Goal} is a goal (@pxref{Goals}),
-and @var{DCGGoal} is a DCG Goal (@pxref{DCG-goals}).
-The @samp{:- Goal} part is optional;
+ at item pred(Arg1::Mode1, Arg2::Mode2, @dots{}) is Det :- Goal
+ at itemx pred(Arg1::Mode1, Arg2::Mode2, @dots{}, DCGMode0, DCGMode1) is Det --> DCGGoal
+ at itemx func(Arg1::Mode1, Arg2::Mode2, @dots{}) = (Result::Mode) is Det :- Goal
+ at itemx func(Arg1, Arg2, @dots{}) = (Result) is Det :- Goal
+ at itemx func(Arg1, Arg2, @dots{}) = Result :- Goal
+A lambda expression.
+ at var{Arg1}, @var{Arg2}, @dots{} are zero or more expressions,
+ at var{Result} is an expression,
+ at var{Goal} is a goal,
+ at var{DCGGoal} is a DCG-goal,
+ at var{Mode1}, @var{Mode2}, @dots{}, @var{DCGMode0}, and @var{DCGMode1}
+are modes (@pxref{Modes}),
+and @var{Det} is a determinism category (@pxref{Determinism}).
+The @w{@samp{:- Goal}} part is optional;
if it is not specified, then @samp{:- true} is assumed.
+
A lambda expression denotes a higher-order predicate or function term
whose value is the predicate or function of the specified arguments
determined by the specified goal.
@@ -2164,24 +2638,16 @@ determined by the specified goal.
A lambda expression introduces a new scope:
any variables occurring in the arguments @var{Arg1}, @var{Arg2}, @dots{}
are locally quantified, i.e.@:
-any occurrences of variables with that name in the lambda expression
-are considered to name a different variable than any variables
-with the same name that occur outside of the lambda expression.
+they are distinct from other variables with the same name
+that occur outside of the lambda expression.
For variables which occur in @var{Result} or @var{Goal},
but not in the arguments,
the usual Mercury rules for implicit quantification apply
(@pxref{Implicit quantification}).
The form of lambda expression using @samp{-->} as its top level functor
-is a syntactic abbreviation:
-an expression of the form
-
- at example
-pred(Var1::Mode1, Var2::Mode2, @dots{}, DCGMode0, DCGMode1) is Det --> DCGGoal
- at end example
-
- at noindent
-is equivalent to
+is a syntactic abbreviation.
+It is equivalent to
@example
pred(Var1::Mode1, Var2::Mode2, @dots{},
@@ -2189,79 +2655,115 @@ pred(Var1::Mode1, Var2::Mode2, @dots{},
@end example
@noindent
-where @var{DCGVar0} and @var{DCGVar1} are fresh variables,
-and @var{Goal} is the result of @samp{DCG-transform(DCGVar0, DCGVar1, DCGGoal)}
-where DCG-transform is the function specified in @ref{DCG-goals}.
+where @code{DCGVar0} and @code{DCGVar1} are fresh variables,
+and @code{Goal} is @code{transform(DCGVar0, DCGVar1, DCGGoal)}
+where @code{transform} is the function specified in @ref{DCG-goals}.
+
+ at item apply(@var{Func}, @var{Arg1}, @var{Arg2}, @dots{}, @var{ArgN})
+ at itemx @var{Func}(@var{Arg1}, @var{Arg2}, @dots{}, @var{ArgN})
+An apply expression (i.e.@: a higher-order function call).
+ at var{N} >= 0,
+ at var{Func} is an expression of type @samp{func(T1, T2, @dots{}, Tn) = T},
+and @var{Arg1}, @var{Arg2}, @dots{}, @var{ArgN}
+are expressions of types @samp{T1}, @samp{T2}, @dots{}, @samp{Tn}.
+The type of the apply expression is @var{T}.
+It denotes the result of applying the specified function
+to the specified arguments.
+ at xref{Higher-order}.
- at node Higher-order function applications
- at subsection Higher-order function applications
+ at end table
-A higher-order function application is a compound term
-of one of the following two forms
+ at anchor{Field access expressions}
+ at subheading Field access expressions
- at example
-apply(@var{Func}, @var{Arg1}, @var{Arg2}, @dots{}, @var{ArgN})
- at var{FuncVar}(@var{Arg1}, @var{Arg2}, @dots{}, @var{ArgN})
- at end example
+Field access expressions provide a convenient way
+to select or update fields of data constructors,
+independent of the definition of the constructor.
+Field access expressions are transformed into
+sequences of calls to field selection or update functions
+(@pxref{Field access functions}).
- at noindent
-where @var{N} >= 0, @var{Func} is a term
-of type @samp{func(T1, T2, @dots{}, Tn) = T},
- at var{FuncVar} is a variable of that type, and
- at var{Arg1}, @var{Arg2}, @dots{}, @var{ArgN}
-are terms of types @samp{T1}, @samp{T2}, @dots{}, @samp{Tn}.
-The type of the higher-order function application term is @var{T}.
-It denotes the result of applying the specified function
-to the specified arguments.
- at xref{Higher-order}.
+A field specifier is a functor expression.
+A field list is a sequence of field specifiers
+separated by @code{^} (circumflex).
+E.g., @samp{field}, @samp{field1 ^ field2}
+and @samp{field1(A) ^ field2(B, C)}
+are all valid field lists.
- at node Explicit type qualification
- at subsection Explicit type qualification
+If the principal functor of a field specifier is @code{@var{field}/N},
+there must be a visible selection function @w{@code{@var{field}/(N + 1)}}.
+If the field specifier occurs in a field update expression,
+there must also be a visible update function
+named @w{@code{'@var{field} :='/(N + 2)}}.
-Explicit type qualifications are occasionally useful to resolve ambiguities
-that can arise from overloading or polymorphic types.
+Field access expressions have one of the following forms.
+There are also DCG goals for field access (@pxref{DCG-goals}),
+which provide similar functionality to field access expressions,
+except that they act on the DCG arguments of a DCG clause.
+
+ at table @code
+ at item @var{Expr} ^ @var{field_list}
+
+A field selection.
+For each field specifier in @var{field_list},
+apply the corresponding selection function in turn.
-An explicit type qualification expression is a term of the form
+ at var{Expr} must be a valid expression.
+ at var{field_list} must be a valid field list.
+A field selection is transformed using the following rules:
@example
- at var{Term} : @var{Type}
+transform(Expr ^ Field(Arg1, @dots{})) = Field(Arg1, @dots{}, Expr).
+transform(Expr ^ Field(Arg1, @dots{}) ^ Rest) =
+ transform(Field(Arg1, @dots{}, Expr) ^ Rest).
@end example
- at noindent
- at var{Term} must be a valid data-term.
- at var{Type} must be a valid type (@pxref{Types}).
+Examples:
-An explicit type qualification expression constrains
-the specified term to have the specified type.
-Apart from that, the meaning of an explicit type qualification expression
-is just the same as the specified @var{Term}.
+ at code{Expr ^ field} is equivalent to @code{field(Expr)}.
-Currently we also support the following alternative syntax
-for type qualification:
+ at code{Expr ^ field(Arg)} is equivalent to @code{field(Arg, Expr)}.
- at example
-with_type(@var{Term}, @var{Type})
- at end example
+ at w{@code{Expr ^ field1(Arg1) ^ field2(Arg2, Arg3)}} is equivalent
+to @w{@code{field2(Arg2, Arg3, field1(Arg1, Expr))}}.
- at noindent
-or equivalently, as it is more commonly written,
+ at item @var{Expr} ^ @var{field_list} := @var{FieldExpr}
+A field update, returning a copy of @var{Expr}
+with the value of the field specified by @var{field_list}
+replaced with @var{FieldExpr}.
+
+ at var{Expr} and @var{FieldExpr} must be valid expressions.
+ at var{field_list} must be a valid field list.
+
+A field update is transformed using the following rules:
@example
- at var{Term} `with_type` @var{Type}
+transform(Expr ^ Field(Arg1, @dots{}) := FieldExpr) =
+ 'Field :='(Arg1, @dots{}, Expr, FieldExpr)).
+
+transform(Expr0 ^ Field(Arg1, @dots{}) ^ Rest := FieldExpr) = Expr :-
+ OldFieldValue = Field(Arg1, @dots{}, Expr0),
+ NewFieldValue = transform(OldFieldValue ^ Rest := FieldExpr),
+ Expr = 'Field :='(Arg1, @dots{}, Expr0, NewFieldValue).
@end example
- at node Type conversion expressions
- at subsection Type conversion expressions
+Examples:
+
+ at w{@code{Expr ^ field := FieldExpr}}
+is equivalent to @w{@code{'field :='(Expr, FieldExpr)}}.
-A type conversion expression is a term of the form:
+ at w{@code{Expr ^ field(Arg) := FieldExpr}}
+is equivalent to @w{@code{'field :='(Arg, Expr, FieldExpr)}}.
+ at w{@code{Expr ^ field1(Arg1) ^ field2(Arg2) := FieldExpr}}
+is equivalent to the code
@example
-coerce(Term)
+OldField1 = field1(Arg1, Expr),
+NewField1 = 'field2 :='(Arg2, OldField1, FieldExpr),
+Result = 'field1 :='(Arg1, Expr, NewField1)
@end example
- at var{Term} must be a valid data-term.
-
- at xref{Type conversions}.
+ at end table
@node Variable scoping
@section Variable scoping
@@ -2271,15 +2773,15 @@ ordinary variables, type variables, and inst variables.
Variables occurring in types are called type variables.
Variables occurring in insts or modes are called inst variables.
-Variables that occur in data-terms,
+Variables that occur in expressions,
and that are not inst variables or type variables,
are called ordinary variables.
-(Type variables can occur in data-terms
-in the right-hand [@var{Type}] operand of an explicit type qualification.
-Inst variables can occur in data-terms
-in the right-hand [@var{Mode}] operand of an explicit mode qualification.
-Apart from that, all other variables in data-terms are ordinary variables.)
+Note that type variables can occur in expressions
+in the right-hand (@var{Type}) operand of an explicit type qualification.
+Inst variables can occur in expressions
+in the right-hand (@var{Mode}) operand of an explicit mode qualification.
+Apart from that, all other variables in expressions are ordinary variables.
The three different variable sorts occupy different namespaces:
there is no semantic relationship between two variables of different sorts
@@ -2296,7 +2798,7 @@ or implicitly (@pxref{Implicit quantification}).
The scope of type variables in a predicate or function's type declaration
extends over any explicit type qualifications
-(@pxref{Explicit type qualification})
+(@pxref{Expressions})
in the clauses for that predicate or function,
and over @samp{pragma type_spec} (@pxref{Type specialization}) declarations
for that predicate or function,
@@ -2313,7 +2815,7 @@ The scope of inst variables is the clause or declaration in which they occur.
The rule for implicit quantification in Mercury
is not the same as the usual one in mathematical logic.
-In Mercury, variables that do not occur in the head of a clause
+In Mercury, variables that do not occur in the head term of a clause
are implicitly existentially quantified around their closest enclosing scope
(in a sense to be made precise in the following paragraphs).
This allows most existential quantifiers to be omitted,
@@ -2335,10 +2837,12 @@ or if they are the goals of disjoint (distinct and non-overlapping)
lambda expressions.
If a variable occurs in a negated context
-and does not occur outside of that negated context other than in parallel goals
+and does not occur outside of that negated context
+other than in parallel goals
(and in the case of a variable in the condition of an if-then-else,
other than in the ``then'' part of the if-then-else),
-then that variable is implicitly existentially quantified inside the negation.
+then that variable is implicitly existentially quantified
+inside the negated context.
@node Elimination of double negation
@section Elimination of double negation
@@ -2357,7 +2861,7 @@ with disjunctions.
the logical meaning and type-correctness of the code,
and they preserve or improve mode-correctness:
they never transform code fragments that would be well-moded
-into ones that would be ill-moded.)
+into ones that would be ill-moded. @xref{Modes}.)
@node Types
@chapter Types
@@ -3236,14 +3740,14 @@ This can be useful during program development,
since it allows you to execute parts of a program
while the program's implementation is still incomplete.)
-Note that a predicate defined using DCG notation (@pxref{DCG-rules})
+Note that a predicate defined using DCG notation (@pxref{Items})
will appear to be defined with two fewer arguments than it is declared with.
It will also appear to be called with two fewer arguments
when called from predicates defined using DCG notation.
However, when called from an ordinary predicate or function,
it must have all the arguments it was declared with.
-The compiler infers the types of data-terms,
+The compiler infers the types of expressions,
and in particular the types of variables
and overloaded constructors, functions, and predicates.
A @dfn{type assignment} is an assignment of a type to every variable,
@@ -3277,14 +3781,14 @@ and the type assigned to the result term in a function clause
must exactly match the result type specified
in the corresponding @samp{:- func} declaration.
-The type assigned to each data-term with an explicit type qualification
-(@pxref{Explicit type qualification})
+The type assigned to each expression with an explicit type qualification
+(@pxref{Expressions})
must match the type specified by the type qualification
expression at footnote{The type of an explicitly
type qualified term may be an instance of the type specified by the
qualifier. This allows explicit type qualifications to constrain the
-types of two data-terms to be identical, without knowing the exact types
-of the data-terms. It also allows type qualifications to refer to the
+types of two expressions to be identical, without knowing the exact types
+of the expressions. It also allows type qualifications to refer to the
types of the results of existentially typed predicates or functions.}.
(Here ``match'' means to be an instance of,
@@ -3314,7 +3818,8 @@ which can be used to select and update fields of a term
in a manner independent of the definition of the type.
The Mercury language includes syntactic sugar to make it more convenient
-to select and update fields inside nested terms (@pxref{Record syntax})
+to select and update fields inside nested terms
+(@pxref{Field access expressions})
and to select and update fields of the DCG arguments of a clause
(@pxref{DCG-goals}).
@@ -3334,7 +3839,7 @@ and to select and update fields of the DCG arguments of a clause
Each field label @samp{@var{field}} in a constructor
causes generation of a field selection function @samp{@var{field}/1},
-which takes a data-term of the same type as the constructor
+which takes an expression of the same type as the constructor
and returns the value of the labelled field,
failing if the top-level constructor of the argument
is not the constructor containing the field.
@@ -3342,12 +3847,12 @@ is not the constructor containing the field.
If the declaration of the field is in the interface section of the module,
the corresponding field selection function is also exported from the module.
-By default, this function has no declared modes ---
-the modes are inferred at each call to the function.
+By default, this function has no declared modes---the modes are inferred
+at each call to the function.
However, the type and modes of this function may be explicitly declared,
in which case it will have only the declared modes.
-To create a higher-order term from a field selection function,
+To create a higher-order value from a field selection function,
an explicit lambda expression must be used,
unless a single mode declaration is supplied for the field selection function.
The reason for this is that normally,
@@ -3365,9 +3870,9 @@ The declaration acts as the request for the generation of that code.
Each field label @samp{@var{field}} in a constructor
causes generation of a field update function @samp{'@var{field} :='/2}.
The first argument of this function
-is a data-term of the same type as the constructor.
+is an expression of the same type as the constructor.
The second argument
-is a data-term of the same type as the labelled field.
+is an expression of the same type as the labelled field.
The return value is a copy of the first argument
with the value of the labelled field replaced by the second argument.
@samp{'@var{field} :='/2} fails
@@ -3377,15 +3882,15 @@ is not the constructor containing the labelled field.
If the declaration of the field is in the interface section of the module,
the corresponding field update function is also exported from the module.
-By default, this function has no declared modes ---
-the modes are inferred at each call to the function.
+By default, this function has no declared modes---the modes are inferred
+at each call to the function.
However, the type and modes of this function may be explicitly declared,
in which case it will have only the declared modes.
-To create a higher-order term from a field update function,
+To create a higher-order value from a field update function,
an explicit lambda expression must be used,
unless a single mode declaration is supplied for the field update function.
-The reason for this is that normally, as with field access functions,
+The reason for this is that normally, as with field selection functions,
field update functions are implemented directly as unifications,
without the code of a function being generated for them.
The declaration acts as the request for the generation of that code.
@@ -3491,7 +3996,8 @@ type1(Field1, _) ^ field1 = Field1.
(type1(_, Field2) ^ field1 := Field1) = type1(Field1, Field2).
@end example
-Using these functions and the syntactic sugar described in @ref{Record syntax},
+Using these functions and the syntactic sugar described in
+ at ref{Field access expressions},
programmers can write code such as
@example
@@ -5235,7 +5741,7 @@ its declarative semantics contains a contradiction,
because the additional axioms for the user-defined equality
contradict the standard equality axioms.
That implies that the implementation
-may compute any answer at all (@pxref{Semantics}),
+may compute any answer at all (@pxref{Formal semantics}),
i.e.@: the behaviour of the program is undefined.}.
@end itemize
@@ -8066,8 +8572,8 @@ p_carefully(!IO) :-
).
@end example
- at node Semantics
- at chapter Semantics
+ at node Formal semantics
+ at chapter Formal semantics
A legal Mercury program is one that complies with the syntax,
type, mode, determinism, and module system rules specified in earlier chapters.
@@ -10654,7 +11160,7 @@ The three levels of purity have a total ordering defined upon them
where @code{pure > semipure > impure}.
@node Impurity semantics
- at section Semantics
+ at section Impurity semantics
It is important to the proper operation of impure and semipure code,
to the flexibility of the compiler to optimize pure code,
@@ -10676,7 +11182,7 @@ that Mercury must specify, and Mercury implementations must respect.
The operational semantics
of a Mercury predicate which invokes @emph{impure} code
is a modified form of the @emph{strict sequential} semantics
-(@pxref{Semantics}).
+(@pxref{Formal semantics}).
@emph{Impure} goals may not be reordered relative to any other goals;
not even ``minimal'' reordering as implied by the modes is permitted.
If any such reordering is needed, this is a mode error.
More information about the reviews
mailing list