EMoP documentation

Essentials

EMoP stands for Existential modules for Prolog: this is a syntactical layer over Prolog extending the language with a first-class module system. The theoritical background is the notion of first-class modules in the LCC language family [HFS08]. GNU Prolog is used as underlying Prolog compiler: EMoP programs are first compiled to Prolog programs, then the GNU Prolog compiler compiles the latter to native executable (more on compilation chain). The syntax still distinguishes in three levels, clauses, goals and terms, and the two following special forms are added to the syntax of goals.

A module value carries a list of clauses and an environment: this is therefore a closure with several entry-points. Closures adds to Prolog a form of high-order programming and object-oriented programming with relatively simple semantics.

An EMoP file, example.mpl, is a goal which performs basically initialization tasks and should unifies a module to the atom example. This is the only place where a module can be unified to an atom: everywhere else, modules should be considered as opaque values and can only be unified with variables (more on module unification).

module example [Message] {
    main :-
       io.std:print_endline(Message).
},
Message = 'Hello world.'

io.std is an atom referring to the file io/std.mpl (more on organizing code into files). The generated executable example executes example:main once all modules initialized.

EMoP has a functional syntax: a unquoted sub-term is considered by default to be a predicate name with an additional last argument, the result value of the sub-term. If no such predicate exists in the scope, then a term is constructed as in Prolog and a warning is issued. Arbitrary Herbrand terms can be constructed by quoting the function symbol between '...'. If necessary, predicates can be quoted between `...'. Declaring data-structure constructors allows the programmer to construct Herbrand terms without quoting.

Modules as first-class values

Predicates receiving modules as parameters

Predicates can take modules as parameters, that covers the common idioms of high-order programming. The typical example is the list iterator (defined in the standard library data.list).

iter([], _).
iter([H | T], M) :-
   M:do(H),
   iter(T, M).

Such a predicate can be used as follow: the following goal prints the elements of a list.

module M [] {
   do(X) :-
      io.std:print(X).
},
data.list:iter(['a', 'b', 'c'], M).

Building a module to pass it immediately to a predicate is a recurring programming pattern. When the module to be passed is the last argument of the predicate and is used nowhere else, as in the previous goal, goals can be rewritten in a more idiomatic way with the following syntactic sugar.

data.list:iter(['a', 'b', 'c']) [] {
   do(X) :-
      io.std:print(X).
}

Note that the predicate preceding an immediate module should always have a (possibly empty) sequence of arguments. For example, the predicate control.iter:findall(M, L) unifies L with the list of the successive values of X for all the successes of M:do(X). Anticipating with functional syntax, it can be used as follows.

module example {
   main :-
      io.std:print_endline(control.iter:findall() { do = ('a'; 'b'; 'c'). }).
}

If there are several modules to be passed in parameter, they can be written one after the other.

Predicates unifying their parameters with modules

The idiom dual to the previous section is to define predicates unifying some of their parameters with new modules. The following predicate unifies its parameter M such that M:do(X) checks if X is between I and J (number comparisons are defined in data.number). Note that a module prefix can span to a sequence of goals.

between(I, J, M) :-
   module M [I, J] {
      do(X) :-
         data.number:(I =< X, X =< J).
   }.

The following goal uses this predicate to check if all the elements of the list L are between 1 and 10.

between(1, 10, M),
data.list:iter(L, M)

Unification of modules

Several module definitions can be unified to the same variable. If a predicate spans in several module definitions, clauses are executed in the order in which modules have been defined. In other words, the two following goals are equivalent (note that the call to q do not need to be prefixed thanks to scopes).

module M [] {
   p(X) :-
      q(X).

   q(X) :-
      X = 1,
      !.
},
module M [] {
   q(X) :-
      X = 2.
},
M:p(X)
module M [] {
   p(X) :-
      q(X).

   q(X) :-
      X = 1,
      !.


   q(X) :-
      X = 2.
},
M:p(X)

The environments are independent from one module definition to another. If there is a cut in one module definition, this cut spans to the clauses of the subsequent module definitions too.

More generally, the unification of two modules is the concatenation of their clauses. The unification should therefor be directed for this operation to be semantically well-defined: one module should have its clauses executed first. For this reason, the standard Prolog unification is disabled for modules: if M and M' are two modules, M = M' is equivalent to M == M', in other words it will succeed if and only if M and M' are already unified to the same module. There is a dedicated predicate for module unification: data.module:unify(M, M') succeeds if M and M' are modules or fresh variables, and unifies them to the module carrying first the clauses of M, then the module of M'. In particular, some module definitions can define predicates that are not in the scope of other module definitions. In the following example, the call to the predicate q is not resolved in the

data.module:unify(M) [some variables] {
   (a list of clauses)
}
is equivalent to
module M [some variables] {
   (a list of clauses)
}

that is to say that the list of clauses is appended at the end of M.

Module unification can be seen as a generalization of Prolog asserta and assertz predicates. Note that assertions are dynamic clauses typically interpreted whereas module definitions are compiled. Module unification is the basis of inheritance for object-oriented programming.

Scope for unprefixed calls

If a call is not prefixed by a module, the predicate is looked for in the current module definition. If it is not found, it is looked for in the parent definition (the module containing the predicate which the current module is defined in), and then in each englobing modules successively. If no such predicate exists in any ancestor, an error is raised if the predicate has no argument. Otherwise the predicate is considered as a term construction (since EMoP has a functional syntax, the goal p(A, B, C) is equivalent to C = p(A, B)) and a warning is issued if the predicate is unquoted (please refer to the section about constructors for details on term construction).

More formally, each module definition is associated to a signature, which contains the set of the functors of predicates declared in this module definition (and syntax definitions). The scope is the list of all signatures of englobing modules, from the current to the uppest one (and imports can add the signatures of other modules to the scope). An unprefixed call is resolved to the first signature in the scope which contains the predicate which matches the functor of the call.

With module unification, the same module value can have several definitions, each having a distinct scope. In the following example, the call to q is not resolved in the scope of the first module definition.

module M [] {
   p :-
      q.
},
module M [] {
   q.
}

The correct scope can be obtained by adding an empty definition of q in the first module definition.

module M [] {
   p :-
      q.

   q :-
      fail.
},
module M [] {
   q.
}

If a call to p or q is inserted between the two module definitions, it will lead to a failure since the only clause for q will fail. In a debugging context, it is often preferable to raise call exceptions for undefined predicates. The following syntax declares q/0 (where 0 is the arity of q) in the scope of the first module without defining it.

module M [] {
   p :-
      q.

   abstract: q/0.
},
module M [] {
   q.
}

As the syntax suggests, this declaration corresponds to abstract methods in object-oriented programming.

Default environment

If no environment is given, the default is to take all the free variables of the current clause and its own environment.

between(I, J, M) :-
   module M {
      do(X) :-
         data.number:(I =< X, X =< J).
   }.

is therefore equivalent to

between(I, J, M) :-
   module M [I, J, M] {
      do(X) :-
         data.number:(I =< X, X =< J).
   }.
and
data.list:iter(L) {
   do(X) :-
      io.std:format('~q is an element of ~q.', [X, L]).
}
is equivalent to
data.list:iter(L) [L] {
   do(X) :-
      io.std:format('~q is an element of ~q.', [X, L]).
}

Printing modules

If a module is printed (for example, with io.std:print(M)), by default, the text <module[n]> is displayed, where n is a number uniquely identifying the module.

This default text can be changed by defining a predicate portray(S) in the module, where S is the output stream where the display takes place.

module example {
   main :-
      module M {
         portray(S) :-
            S:print('M.example').
      },
      io.std:print(M).
}

Functional syntax

Calls in terms

A sub-term with n arguments is considered as a call to the predicate of n + 1 parameters with the same functor, the last parameter is considered as the result value of the term. In the following example, the variables L0 and L1 are only used as intermediary results.

data.list:(
   append(A, B, L0),
   reverse(L0, L1),
   append(L1, C, Result)
)

This predicate can be rewritten equivalently as follows.

Result = data.list:append(data.list:reverse(data.list:append(A, B)), C)

Note that the prefix module should be repeated as a prefix does not apply to the sub-term of a predicate. Local scopes can be used instead.

Result = data.list.(append(reverse(append(A, B)), C))

Arithmetic operators defined in data.number are typically used as functions.

Product = data.number.(X * X' + Y * Y')

is equivalent to

data.number:'*'(X * X', Xp),
data.number:'*'(Y * Y', Yp),
data.number:'+'(Xp + Yp, Product)

Comparison operators have also a functional version so that they return their last argument. A =< B =< C is parentherized as (A =< B) =< C and is therefore equivalent to A =< B, B =< C.

Calls produced by a sub-term are sequenced from left to right and from the deepest to the top ones.

Note that the notion of function is mere syntactic: a predicate does not lost its reversibility when used as a function. Thanks to the reversibility of data.number:'+', the following predicate counts from 0 to N - 1.

count(0) :-
   !.
count(N) :-
   N = data.number:(M + 1),
   io.std:print_endline(M),
   count(M).

If functions are used is the arguments of the head of a clause, the goals are inserted at the beginning of the body. The previous example can be rewritten as follows.

count(0) :-
   !.
count(data.number:(M + 1)) :-
   io.std:print_endline(M),
   count(M).

Function definition

Predicates naturally expressed as functions can be defined with the following alternative syntax for clauses.

append(L, L') = rev_append(reverse(L), L').

This clause is equivalent to

append(L, L', Result) :-
   reverse(L, L0),
   rev_append(L0, L', Result).

The two syntax for clauses, with :- and =, can be freely mixed.

Modules in terms

Modules can be written in sub-terms, they are replaced by their variable.

data.module:unify(module M { p(1) }, M').

is equivalent to

module M {
   p(1)
},
data.module:unify(M, M').

Note that if the module name is omitted, a fresh variable is introduced. The above example can therefore be rewritten as follows.

data.module:unify(module { p(1) }, M').

Combined with function definition, this syntax leads to the following idiomatic form for defining parameterized modules.

between(I, J) = module {
   do(X) :-
      data.number.(I =< X =< J)
}

The short-hand for anonymous modules as last arguments can also be used with functions. Consider the following two-lists version of iter defined in data.list, which iterates a binary predicate over the items of two lists of the same length (the typical use is as a map-list function).

iter([], _M) = [].
iter([H | T], M) = [M:do(H) | iter(T, M)].

This predicate can be called in the following way.

module example {
   import: data.number.

   main :-
      L' = data.list:iter([1, 2, 3]) { do(X) = X * 2 }.
}

The sequence operator

Checks or side-effects (cuts, logs, ...) often have to be interleaved between function calls, this can be done with the >> operator: in the general case, the goal A >> B is simply equivalent to A, B, and the term A >> B first executes the goal A and then evaluates to the term B.

pred(X) = data.number.((X > 0) >> X - 1).

is equivalent to

pred(X, Y) :-
   data.number.(
      X > 0,
      Y = X - 1
   ).

This is typically used to cut in function definitions.

import data.number.
pred'(0) = ! >> 0.
pred'(N + 1) = N.

If there is no cut in A and if B is of the form X = Y, B' with B' possibly empty, then A >> B is expanded as (X = Y, A) >> B, that is to say unification are anticipated.

Constructors

Unquoted terms are generally evaluated as function calls, and, by default, Herbrand terms are constructed only if no suitable predicate exists. If a function symbol is quoted between '...', a Herbrand term is constructed.

To construct a Herbrand term without quoting, data structures can be declared in the scope, with the benefits that errors like misspelling will then produce helpful warnings. Term construction can be obtained by defining predicates which return the constructed term: the following predicate constructs terms of signature f/2, that is to say terms with the functor f and arity 3.

module example {
   f(X, Y) = data.term:make(data.string:atom("f"), [X, Y]).

   main :-
     io.std:print_endline(f(1, 2)).
}

Of course, such a definition is inefficient and leads to bad argument indexing. There is therefore a built-in notion of constructors, which is essentially equivalent semantically (same use, same scope, ...), but generates more efficient code.

module example {
   constructor: f/2.

   main :-
     io.std:print_endline(f(1, 2)).
}

Several constructors can be listed in the same directive constructor:, optionally comma-separated.

In both cases, the goal X = f(1, 2) is treated identically to f(1, 2, X)

There is an observable semantics particularity with constructors: contrary to predicates, constructors are applied before the evaluation of their arguments. Therefore X = f(io.std:print) is equivalent to X = f(Y), io.std:print(Y). This is particularly useful for tail-recursion.

iter([], _M) = [].
iter([H | T], M) = [M:do(H) | iter(T, M)].

is equivalent to

iter([], _M, []).
iter([H | T], M, [H' | T']) :-
  M:do(H, H'),
  M:iter(T, T').

which is tail-recursive.

Modules for programming in the large

Organizing code into files

Each EMoP file associates one module to an atom: this atom a should corresponds to the name of the file a.mpl. Moreover, if the atom contains dots, as in a.b.c, then the file should be c.mpl and located in a path ending by a/b/.

These conventions allow EMoP compiler to solve dependencies automatically: in the module a.b.c, every call prefixed by an atom will adds a dependency to the corresponding files which will be looked in the directory ../../ relatively to the directory where c.mpl is. Then, if a file is not found in this directory, the directories listed in the environment variable EMOPPATH (colon separated) will be explored. If there is no variable EMOPPATH, then the directory ../lib relatively to the location of the compiler executable will be used by default.

Mutual dependencies are allowed. As a current limitation, the compiler can overlook a dependency if there is no call syntactically prefixed by the atom (for example, if the atom is obtained from a more complex data structure). Such dependencies can be explicited on the command line by adding them in the front of the main file of the program. The file module considered as main, that is to say the module whose main predicate is executed, comes last (more on compilation chain).

Hiding implementation details

Since modules are accessible only to goals which have the module variable in their scope, auxiliary predicates can be hidden from the outside of a predicate, a module or a file, by defining internal modules.

For a predicate with auxiliary definitions, the module variable is just never unified with a parameter of the predicate.

print_X_Y_times(X, Y) :-
   module M {
      aux(I) :-
         data.number.(
            I > 0,
         ->
            io.std:print_endline(X),
            aux(I - 1)
         ;
            true
         ).
   },
   M:aux(Y).

For auxiliary predicates of a whole module, a common pattern is to split the module in two: a public and a private part. Environments allow each module to see the other.

p(Public) :-
   module Public [Private] {
      q :-
         Private:q.
   },
   module Private [Public] {
      q :-
         r.

      r :-
         io.std:print_endline('The predicate r is not visible from the outside, it is only callable through q from the outside.').
   }.

This pattern is often used at the level of a whole file to hide implementation details.

module example [Impl] {
   p :-
      Impl:q.
},
module Impl {
   q :-
      io.std:print_endline('This is an hidden predicate, callable only through p.').
}

Importing signatures

Modules can import signatures from other modules. Predicates from the imported modules can then be called without prefix.

module example {
   import: data.number, data.list, io.std.

   main :-
      iter(1 .. 10) {
          do(X) :-
             print_endline(X).
      }.
}

When several imported modules define the same predicate, the last imported one takes precedence. Predicates defined in the current module definition have always precedence to any imported module. Imports only affect the following clauses and not the previous ones. More formally, the signature of a newly imported module is inserted at the second place in the scope. Therefore the signature of the current module remains the first one, and the last imported module comes before the others. Note that the signature of the current module definition is not affected by imports. In particular, if other module definitions import the current module, they will not see the imported predicates.

A goal or a term can locally import a module too. The local import syntax is module-name.(expression), where the dot and the open parenthesis are written one after the other without any space. The local import spans between the parentheses.

io.std:print(data.list.(append(L1, append(L2, L3))))

In local imports, predicates defined in the imported module have precedence to any other predicates, even to the predicates defined in the current module. Formally, their signatures are inserted at the first place in the scope. Intuitively, local import can be seen as a more liberal form of call prefixing than the colon: local import affects the sub-terms too (see functional syntax), calls can be mixed between the current and the imported modules, and the syntax extensions are imported too.

Imported modules can be any term which evaluates to a module such that the compiler can determine its signature statically. That is the case for, exhaustively:

File module names

The module is added to dependencies as usual.

io.std:print(data.list.(append(L1, append(L2, L3))))
Variables unified to a module

The variable can also have been unified to another variable associated to a statically known signature, recursively. The following example shows the private definition of a predicate q.

module example {
   import: Impl.

   p :-
      r.

   q :-
      io.std:print_endline('This predicate can be called without prefix from Impl').
},
module Impl {
   import example.

   r :-
      io.std:print_endline('This is an hidden predicate, callable only through p.'),
      q.
}
Module definitions

Typically used to define private predicates. This gives a shorter way to write the previous example.

module example {
   import: module {
      r :-
         io.std:print_endline('This is an hidden predicate, callable only through p.'),
         q.
   }.

   p :-
      r.

   q :-
      io.std:print_endline('This predicate can be called without prefix from the imported module since the module example is englobing.').
}

The term in import can include initialization code.

module example {
   import:
      (Counter = data.ref.backtrackable:new(0)) >>
      module {
         count = data.number:(Counter++)
      }.

   main :-
      io.std:print_endline(count),
      io.std:print_endline(count).
}
Variables which appear as arguments

Only if it is an argument of a call to a predicate in a module with a statically known signature (recursively) if this predicate has a clause where this argument is a variable which is unified to (a variable unified to, recursively) a module, or if this predicate is a simple sequence of calls to predicates in the same module definition or prefixed by a variable with a known signature and these predicates are statically known to unify this variable to a signature (recursively).

module example {
  concatenate(Separator) = module {
     '+'(A, B) = data.atom.(concat(A, concat(Separator, B)))
  }.

  main :-
     io.std:print_endline(concatenate(' ').('a' + 'b' + 'c'))
}

The term in import is evaluated at the definition of the module which contains the import, with the scope of that module (environment variables are accessible, predicates of that module can be called) and in the order of imports. The semantics of a cut in the term is the natural one considering that the import belongs to the goal where the module appears: all the choice point introduced by the parent predicate are removed.

Syntax and parsing

Extending the syntax with new operators

Module definitions can introduce new operators at the three positions prefix, infix and postfix. An operator can be any valid unquoted identifier. Operators can then be used from their introduction up to the end of the module definition. These operators can be used anywhere but as the head functor of a clause.

Infix (binary) operators

Infix operators can be non-associative (a op b op c is disallowed), left associative (a op b op c is parsed (a op b) op c) or right associative (a op b op c is parsed a op (b op c)).

In the standard library, the module data.list defines the binary operator ++ to append two lists.

module data.list {
   (...)
   syntax: infix right associative '++'.

   syntax: '=' < '++' < ':'. 

   '++'(A, B) = append(A, B).
   (...)

The second syntax directive declares that ++ has a greater precedence than = but a smaller precedence than :.

This operator can be used as follows.

module example {
   main :-
      io.std:print_endline(data.list.([0, 1] ++ [2] ++ [3, 4, 5])).
}

The concatenation can be defined as the binary operator ''.

module example {
   syntax: infix left associative ''.
   syntax: '=' < '' < ':'.

   `'(A, B) = data.list:append(A, B).

   main :-
      io.std:print_endline(['a'] ['b', 'c'] ['d']).
}

The module data.ref defines the binary operator <- to set the value of a reference.

module data.ref {
   (...)
   syntax: infix '<-'.

   syntax: '<-' = '='.

   '<-'(X, V) :-
      X:set(V).
   (...)
}

The second syntax directive declares that <- has the same precedence than =, this is equivalent to '<-' < '=' and '=' < '<-'. Since <- is declared non-associative, X <- A <- B raises a syntax error.

Prefix operators

The following excerpt from the module data.ref shows how the prefix operator ? is defined to get the value of a reference.

module data.ref {
   (...)
   syntax: prefix '?'.

   syntax: prefix '-' < '?' < ':'. 

   '?'(X) = X:get.
   (...)
}

The second syntax directive declares that ? has a greater precedence than the prefix operator - but a smaller precedence than :. If it is not specified whether the precedence applies to the prefix, infix or postfix version of the operator, the last declared version is taken by default.

The following example uses the operators of data.ref to calculate the Nth element of the Fibonacci sequence.

module fibonacci {
   fib(N, Result) :-
      data.ref.non_backtrackable.(
         X = new(0),
         Y = new(1)
      ),
      data.ref.(
         for(_, 1, N),
         Z = ?Y,
         Y <- data.number.(?X + ?Y),
         X <- Z,
         fail
      ;
         Result = ?X
      ).
}
Postfix operators

The following excerpt from module data.number defines the postfix operator ! to calculate the factorial.

module data.number {
   (...)
   syntax: postfix '!'.

   syntax: prefix '-' < '!' < ':'. 

   '!'(N) = (N > 2, !) >> N * (N - 1)!.
   '!'(_) = 1.
   (...)
}

Operator aliases

Operators are usually parsed as functors with the same name. The as modifier can specify a different functor name. This is typically useful to distinguish prefix and postfix operators with the same name.

module data.number {
   (...)
   syntax: prefix '++' as '++|'.
   syntax: prefix '--' as '--|'.
   syntax: postfix '++' as '|++'.
   syntax: postfix '--' as '|--'.
   (...)
}
The following example succeeds.
module example {
   import: data.number.

   constructor: '++|'/1, '|++'/1.

   main :-
      ++('a'++) = '++|'('|++'('a')).
}

Modular definition of the preorder of precedence

The declaration of an operator subsumes any previous declaration of this operator (with the same position) in the scope. In particular, (re)declaring an operator guarantees that it is fresh of any precedence declaration. Precedences define a preorder between the operators in each signature: two operators are compatible (i.e. can appear within the same expression without parentheses) if and only if they are comparable and either the comparison is strict or they are equivalent and their associativity is the same.

The precedence between two operators is calculated considering the smallest sub-scope (i.e. a prefix of the scope as a list of signature, that is to say the closest signatures) such that the union of the preorders defined in the signatures of this sub-scope makes these two operators comparable. This behavior allows modular declaration of precedences but can be counter-intuitive. The typical use is the redeclaration of a precedence.

module example {
   constructor: - / 2, * / 2.

   syntax: infix left associative '-' '*'.
   syntax: '-' < '*'.

   main :-
      io.std:print_endline(1 * 2 - 3 * 4),
      io.std:print_endline(module { syntax: '*' < '-' }.(1 * 2 - 3 * 4)).
}

Here, in both printed expressions, the sub-scope is reduced to a single signature: in the first expression, * has a greater precedence than -, and the converse in the second. Now, if a third operator + leads to consider both signatures, the two declarations - < * and * < - leads to + = *, i.e. the two operators have the same precedence.

module example {
   constructor: - / 2, * / 2, + / 2.

   syntax: infix left associative '-' '*' '+'.
   syntax: '+' = '-' < '*'.

   main :-
      io.std:print_endline(1 * 2 - 3 * 4),
      io.std:print_endline(module { syntax: '*' < '-' }.(1 * 2 + 3 * 4)).
}

Default syntax

The module emop.syntax:syntax is by convention imported by any other modules.

module emop.syntax {
   syntax(X) :-
      logic(X),
      comparisons(X),
      arithmetic(X),
      module X {
         syntax: '\\+' < '=' < infix '+'.
         syntax: prefix '+' < ':'.
      },
      level(X),
      functional_logic(X),
      pipe_match(X),
      implicit_do(X).

   logic = module {
      constructor: '.'/2, ','/2, '[]'/0, top/0.

      syntax: infix right associative '.' ';' '->' ',' '>>'.
      syntax: infix ':-'.
      syntax: prefix '\\+'.
      syntax: infix left associative ':'.
      syntax: postfix '.()'.

      syntax: '.' < ':-' < ';' < '->' < ',' < '\\+' < '>>' < ':' = '.()'.
   }.

   comparisons = module {
      syntax: infix left associative '=' '<' '>' '=<' '>=' '\\=' '=='.

      syntax: '=' = '<' = '>' = '=<' = '>=' = '\\=' = '=='.
   }.

   arithmetic = module {
      syntax: infix left associative '+' '-' '*' '/' 'mod' 'quo'.
      syntax: infix right associative '**'.
      syntax: prefix '+' '-'.

      syntax: infix '+' = infix '-' < '*' = '/' = 'mod' = 'quo'.
      syntax: '*' < '**' < prefix '+' = prefix '-'.
   }.

   (...)
}

The three last predicates level, functional_logic and pipe_match define notations and are described in the next paragraphs.

Notations

Notations define rewriting rules to be applied to goals and terms before the compilation. Notations defined in functional_logic rewrite the ->, ; and = operators in term position such that choice points, conditionals and unifications can be written in terms.

module emop.syntax {
   (...)

   functional_logic = module {
      notation: (term) (P -> Q) -> (P -> true) >> Q.
      notation: (term) (P -> Q; R) -> (P -> X = Q; X = R) >> X.
      notation: (term) (P; Q) -> (X = P; X = Q) >> X.
      notation: (term) (A = B) -> (X = A, X = B) >> X.
   }.

   (...)
}

With such notations, the goal

A = ('a'; 'b')

is rewritten, with a fresh variable X,

A = ((X = 'a'; X = 'b') >> X)

which is equivalent to

(X = 'a'; X = 'b'), A = X

The rewriting system defined by notations is applied to the abstract syntax tree until fix-point. The rewriting strategy is top-down, parallel, with restart, applying the first applicable rule declared in the closest signature in the scope.

Top-down

Notations are first tried to be applied to the root before the sub-terms. The following example prints u in the first line and c in the second line.

module example {
   notation: (term) 'a'('b') -> 'u'.
   notation: (term) 'b' -> 'c'.

   main :-
      io.std:print_endline('a'('b')),
      io.std:print_endline('b').
}
Parallel

If no notations are applicable to the root, the rewriting is applied to every child in parallel. The following example prints w.

module example {
   notation: (term) 'a'('b', 'c') -> 'u'.
   notation: (term) 'a'('c', 'b') -> 'v'.
   notation: (term) 'a'('c', 'c') -> 'w'.
   notation: (term) 'b' -> 'c'.

   main :-
      io.std:print_endline('a'('b', 'b')).
}
With restart

After that sub-terms have been rewritten one step, rewriting is restarted up to fix-point from the root. The following example prints u.

module example {
   notation: (term) 'a'('c') -> 'u'.
   notation: (term) 'b' -> 'c'.
   notation: (term) 'c' -> 'd'.

   main :-
      io.std:print_endline('a'('b')).
}
Using the first applicable rule

Notations defined in the current module have the precedence on all rules defined elsewhere in the scope. More formally, notations are tried in the order of the signatures in the scope. In each signature, notations defined first have precedence. The following example prints u then v.

module example {
   notation: (term) 'a'('b') -> 'u'.
   notation: (term) 'a'(X) -> 'v'.

   main :-
      io.std:print_endline('a'('b')),
      io.std:print_endline('a'('c')).
}

In the left-hand side of the ->, variables bind any sub-term and unquoted function symbols match any function symbol with the correct arity. Variables followed with a * bind any sequence of arguments in a predicate. The following example prints f(b,c,a).

module example {
   notation: (term) 'first_to_last'(p(X, A*)) -> p(A*, X).

   main :-
      io.std:print_endline('first_to_last'('f'('a', 'b', 'c'))).
}

For variables bound to a sequence of arguments, the * is optional in the right hand-side: they will expand to arguments if they appear under a predicate, or to a sequence separated by commas (typically, a logic conjunction) if they appear elsewhere.

Levels goal and term are defined as follows. Other levels can be defined.

module emop.syntax {
   (...)

   level = module {
      level: (goal) (goal, goal).
      level: (goal) (goal; goal).
      level: (goal) (goal -> goal).
      level: (goal) (goal >> goal).
      level: (goal) (term:goal).
      level: (goal) 'catch'(goal, term, goal).
      level: (goal) (\+ goal).

      level: (term) (goal -> term).
      level: (term) (goal >> term).

      level: (goal, term) p(term*).
   }.

   (...)
}

Levels for child are deduced from the level of the root using the first applicable level in the closest signature in the scope. level: (goal, term) p(term*) specifies that, by default, any sub-term of a term or a goal is on level term.

Pipes and matches

Notations are used to define a syntax for sequencing functional operations and for pattern matching.

The basic use of pipes is described by the following notations.

module emop.syntax {
   (...)

   pipe_match = module {
      (...)
      notation: (goal, term) (A | X:p(Gamma*)) -> X:p(A, Gamma).
      notation: (goal, term) (A | p(Gamma*)) -> p(A, Gamma).
      (...)
   }.

   (...)
}

Therefore, X | f(1) | g(2) | h(3) = Y is rewritten h(g(f(X, 1), 2), 3) = Y, which is equivalent to f(X, 1, A), g(A, 2, B), h(B, 3, Y).

Logic operators are defined in pipes as follows.

module emop.syntax {
   (...)

   pipe_match = module {
      (...)
      notation: (goal, term) (A | (P >> Q)) -> (A = X) >> P >> (X | Q).
      notation: (goal, term) (A | (P -> Q)) -> (A = X) >> (P -> X | Q).
      notation: (goal, term) (A | (P -> Q; R)) -> (A = X) >> (P -> X | Q; X | R).
      notation: (goal, term) (A | (P; Q)) -> (A = X) >> (X | P; X | Q).
      (...)
      notation: (goal, term) (A | (P & Q)) -> (A = X) >> (X | P) >> (X | Q).
      notation: (goal, term) ((P & Q) | A) -> (A = X) >> (P | X) >> (Q | X).
      (...)
   }.

   (...)
}

Therefore, >> inserts a side-effect P before piping to Q, -> does the same but cuts the choice-points of P. In (A | (P -> Q; R)), P can be used as a condition to pipe either to Q or R. The pipe (A | (P; Q)) is non-deterministic between two actions P and Q. The pipe (A | (P & Q)) pipes the same value A to the actions P and Q and ((P & Q) | A) pipes the value P to A and then the value Q to A.

Pipes to variables and numbers are synonymous to =: the previous example can be written X | f(1) | g(2) | h(3) | Y, and more generally intermediate results can be bound to variables such in X | f(1) | g(2) | Z | h(3) | Y.

module emop.syntax {
   (...)

   pipe_match = module {
      (...)
      notation: (goal) (A | X) | X: var; X: number -> A = X.
      notation: (term) (A | V) | V: var -> (A = X, X = V) >> X.
      notation: (term) (A | N) | N: number -> (A = N) >> N.
      (...)
   }.

   (...)
}

The part of notations between | and -> is a guard to check side-conditions of the rewriting rule, as usual the conjunction is denoted , and the disjunction is denoted ;.

Pattern-matching is a set of notations for term deconstruction. The basic rules are

module emop.syntax {
   (...)

   pipe_match = module {
      (...)
      notation: (term) A match V | V: var -> (A = X, X = V) >> X.
      notation: (term) A match N | N: number -> (A = N) >> N.
      notation: (goal, term) A match (P >> Q) -> (A = X, P) >> (X match Q).
      notation: (goal, term) A match (P => Q) -> (A = X) >> (X match P) >> Q.
      notation: (goal, term) A match (P -> Q) -> (A = X) >> (X match P -> Q).
      notation: (goal, term) A match (P -> Q; R) -> (A = X) >> (X match P -> Q; X match R).
      notation: (goal, term) A match (P; Q) -> (A = X) >> (X match P; X match Q).
      notation: (goal) A match X:p(B*) -> (A = X:p(C*)) >> ((C match B)*).
      notation: (goal) A match p(B*) -> (A = p(C*)) >> ((C match B)*).
      (...)
   }.

   (...)
}

A fresh sequence variable in the right-hand side of a rule generates a sequence of fresh variables: the length of the sequence is fixed in expressions like (C match B)* where several sequences occur: these sequences should have the same length, and the expression is replaced by a sequence of expressions where variables are mapped to the elements of the respective sequences at the same positions: if C is C1, C2, C3 and B is B1, B2, B3, then the expression (C match B)* is expanded to C1 match B1, C2 match B2, C3 match B3.

The following example prints c.

module example {
   import: data.list.

   check(X) =
      X match (
         'first'([A] ++ _)
      ->
         A
      ;
         'last'(_ ++ [B])
      ->
         B
      ).

   main :-
      io.std:print_endline(check('last'(['a', 'b', 'c']))).
}

It is worth noticing that match reverses the order of function calls with respect to functional notation: top-most function in pattern is applied first. The following repetition operator is defined in data.list.

module data.list {
   (...)

   syntax: postfix '*'.

   syntax: '++' < postfix '*' < ':'.

   `*'(X, Y) :-
      Y match ([]; X ++ X*).

   (...)
}

In Y match X ++ X*, the concatenation is applied first and then the recursive call: if = was used instead of match, the predicate would still have the same successes but with a quadratic time complexity instead of linear and would loop instead of fail.

In term position, pattern matching destructs then reconstructs the matched term.

module emop.syntax {
   (...)

   pipe_match = module {
      (...)
      notation: (term) A match X:p(B*) -> (A = X:p(C*)) >> X:p((C match B)*).
      notation: (term) A match p(B*) -> (A = p(C*)) >> p((C match B)*).
      (...)
   }.

   (...)
}

The pattern-matching

module example {
   import: data.list, data.number.

   check(X) =
      X match (
         'incr_last'(L ++ [B])
      ->
         'incr_last'(L ++ [B + 1])
      ).

   main :-
      io.std:print_endline(check('incr_last'([1, 2, 3]))).
}

can be rewritten

module example {
   import: data.list, data.number.

   check(X) =
      X match (
         'incr_last'(_ ++ [B -> B + 1])
      ).

   main :-
      io.std:print_endline(check('incr_last'([1, 2, 3]))).
}

Pattern-matching and pipes can be interleaved.

module emop.syntax {
   (...)

   pipe_match = module {
      (...)
      notation: (goal, term) (A | match B) -> A match B.
      notation: (goal, term) (A | | B) -> A | B.
      notation: (goal, term) (A match match B) -> A match B.
      notation: (goal, term) (A match | B) -> A | B.
      (...)
   }.
}.

With these notations, the last example can be rewritten as follows.

module example {
   import: data.list, data.number.

   check(X) =
      X match (
         'incr_last'(_ ++ [ | succ ])
      ).

   main :-
      io.std:print_endline(check('incr_last'([1, 2, 3]))).
}

Guards depending on scope

The module data.ref.auto defines the following notation to implicitly replace every reference (recognized as modules defining a predicate get/1) by its value.

module data.ref.auto {
   (...)
   notation: (term) A | A : var, (A:'get') / 1: predicate -> ?A.
   (...)
}

A level protected is defined to prevent this notation to be applied recursively or to be applied at places where a reference is expected.

module data.ref.auto {
   (...)
   import: data.number.

   level: (term) ?protected.
   level: (term, goal) (protected++).
   level: (term, goal) (protected--).
   level: (term, goal) (++protected).
   level: (term, goal) (--protected).
   (...)
}

The following example demonstrates how this module can be used.

module example {
   import: data.number.

   main :-
      X = data.ref.backtrackable:new(0),
      data.ref.auto.(
         io.std:print_endline(X),
         X <- X + 1,
         io.std:print_endline(X),
         io.std:print_endline(++X)
      ).
}

In the guard, the kind predicate matches any predicate, constructor matches any constructor and symbol any predicate or constructor. If the function symbol is bound from the head of the notation, the arity can be omitted (it is implicitly the arity of the matched term). The arity can be any arithmetic expression, and the prefix operator # can be used to get the arity of a term or the length of a sequence. The following example defines the concatenation to behave like a match on constructors and like a pipe on predicates.

module example {
   import: data.number.

   syntax: infix left associative ''.
   syntax: prefix '+' < '' < ':'.

   notation: (goal) A c(B*) | c : constructor -> (A = c(C*)) >> ((C B)*).
   notation: (term) A c(B*) | c : constructor -> (A = c(C*)) >> c((C B)*).
   notation: (goal) A p(B*) | p/(#B* + 1) : predicate -> p(A, B*).
   notation: (term) A p(B*) | p/(#B* + 2) : predicate -> p(A, B*).

   check(X) = X 'a'(succ).

   main :-
      io.std:print_endline(check('a'(1))).
}

Implicit do

The following notations ease passing an arbitrary predicate when a module with a do with one or two arguments is expected.

implicit_do = module {
   notation: (term) X:f(Gamma*, '*', Delta*) ->
      module { do(A) :- X:f(Gamma*, A, Delta*) }.

   notation: (term) f(Gamma*, '*', Delta*) ->
      module { do(A) :- f(Gamma*, A, Delta*) }.

   notation: (term) X:f(Gamma*, '<', Delta*, '>', Epsilon*) ->
      module { do(A, B) :- X:f(Gamma*, A, Delta*, B, Epsilon*) }.

   notation: (term) f(Gamma*, '<', Delta*, '>', Epsilon*) ->
      module { do(A, B) :- f(Gamma*, A, Delta*, B, Epsilon*) }.

   notation: (term) X:f(Gamma*, '>', Delta*, '<', Epsilon*) ->
      module { do(A, B) :- X:f(Gamma*, B, Delta*, A, Epsilon*) }.

   notation: (term) f(Gamma*, '>', Delta*, '<', Epsilon*) ->
      module { do(A, B) :- f(Gamma*, B, Delta*, A, Epsilon*) }.
}

The following example enumerates the prefixes of a list.

module example {
   main :-
      io.std:print_endline(
         control.iter:findall(data.list:append(*, _, "abcd"))
      ).
}

These notations can also be useful when the distinguished arguments of the functional syntax or the pipes or matches are not at the right place.

module example {
   main :-
      'filename.suffix'
      | data.atom:concat(>, '.suffix', <):do
      | io.std:print_endline.
}

Using the parser in programs

The syntax defined in a module can be used to parse files at run-time. The following example parses a file with the comma as the only allowed operator.

module example {
   main :-
      Ast = emop.parse:file('test_file') {
         syntax: infix right associative ','
      },
      io.std:print_endline(emop.parse:term(Ast)).
}

Ast is unified with a representation of the abstract syntax tree with positions and some other decorations. emop.parse:term(Ast) converts the Ast into a simple Herbrand term. Syntaxes can be composed as usual. The following example uses the arithmetic syntax of EMoP augmented with cos and sin prefix operators.

module example {
   main :-
      emop.syntax:arithmetic(M),
      module M {
         syntax: prefix 'cos' 'sin'.
         syntax: prefix '+' = 'cos' = 'sin'.
      },
      Ast = emop.parse:file('test_file', M),
      io.std:print_endline(emop.parse:term(Ast)).
}

Constraint programming

Domains and constraints

If X is a variable or a list of variables, data.fd:set_domain(X, Min, Max) constraints the domain of this or these variables to be between If Min and If Max.

The module data.fd.fac defines arithmetic constraints with full-AC propagation. The module data.fd.pac defines arithmetic constraints with partial-AC propagation. Symbolic constraints such as element element_var and all_different are defined in data.fd.

Labeling and optimization

data.fd:labeling(X) enumerates satisfiable instantiations of the variable or the list of variables X.

If M is a module with a predicate objective(X) unifying X with a number, then data.fd:minimize(M) finds an instantiation for which X is minimal and data.fd:maximize(M) finds an instantiation for which X is maximal.

Modules for object-oriented programming

Modules and classes

A module is a set of predicates with some data in the environment, it corresponds therefore to what is called singleton class or immediate object, a class with exactly one instance. Modules being first-class values, a more general notion of class can be encoded as a predicate which returns a module: this module is the instance and the predicate acts as a constructor.

module example {
   import: data.ref.

   point(Origin) =
      (X = data.ref.backtrackable:new(Origin)) >>
      module {
         get_x = ?X.

         move(D) :-
            X <- ?X + D.
      }.

   main :-
      P = point(0),
      io.std:print_endline(P:get_x),
      P:move(3),
      io.std:print_endline(P:get_x).
}

Inheritance is obtained by module unification.

colored_point(Origin, Color) =
   module {
      color = Color.
   } = point(Origin).

The module definition of M defining the child class with the predicate color precedes usually the calls to constructors of the parent classes, here point. In this way, if the child class redefines clauses for predicates already define in an ancestor, the clauses of the child class will be called first. Overriding a predicate relies on cut (to suppress the choice points leading to the inherited clauses) or fail (to hand over the ancestor definitions). The following example declares a point which can only be moved with a positive distance, i.e. the predicate move fails for any non-positive input.

forward_point(Origin) =
   module {
      move(D) :-
         (
            D > 0
         ->
            fail
         ;
            !,
            fail
         ).
   } = point(Origin).

Abstract methods

Abstract predicates corresponds to methods which are left undefined in the base class and are implemented by derived classes, aka abstract methods. Their declaration in the base class adds them to the scope, that allows other predicates in the base class to call them.

abstract_point(Origin) =
   module {
      abstract: get_x / 1, set_x / 1.

      move(D) :-
         set_x(get_x + D).
   }.

point(Origin) =
   (X = data.ref.backtrackable:new(Origin)) >>
   (
      module {
         get_x = ?X.
         set_x(X') :-
            X <- X'.
      } = abstract_point(Origin)
   ).

Multiple inheritance

A module can, of course, be unified to instances from several ancestor classes.

point(Origin) =
   (X = data.ref.backtrackable:new(Origin)) >>
   module {
      get_x = ?X.

      move(D) :-
         X <- ?X + D.
   }.

color(Color) =
   module {
      color = Color.
   }.

colored_point(Origin, Color) =
   point(Origin) = color(Color).

However, if a module is unified to both an instance of colored_point and an instance forward_point, each of these two ancestors will unify the resulting module to its own instance of point: this is a form of static multiple inheritance which is undesirable in this case. To encode virtual inheritance, constructors should be decomposed in two parts, a virtual constructor which does everything but the unification to the virtual bases (this constructor will be used in derived classes), and a concrete constructor which achieves the work of the virtual one by making these unifications.

virtual_colored_point(Color) = color(Color).

colored_point(Origin, Color) =
   virtual_colored_point(Color) = point(Origin).

virtual_forward_point =
   module {
      move(D) :-
         (
            D > 0
         ->
            fail
         ;
            !,
            fail
         ).
   }.

forward_point(Origin) =
   virtual_forward_point = point(Origin).

colored_forward_point(Origin, Color) =
   virtual_colored_point(Color) =
   virtual_forward_point =
   point(Origin).

Reference

Top-level

The top-level interactive loop is obtained when emop is launched without argument.

The top-level queries the user for a goal and execute it. If a goal depends from a named module, this module is compiled and loaded on the fly, except if this module has been statically compiled with the top-level. If a file has changed from the last run-time compilation, the user is prompted for reloading it (but a statically compiled module is never recompiled). A goal can define a named module and this module is available until this definition is backtracked. Directives import, constructor, syntax, level and notation can be used in place of goal at top-level.

Goals are executed in sequence and fresh variables are accumulated, their current values are displayed before each prompt. The current number of goals in the sequence is displayed in the prompt. The sequence can be backtracked by entering the query backtrack in the top-level (this is not a goal, the query should be exactly backtrack). When a goal has several solutions, the empty query goes to the next one.

A custom top-level can be defined. To create a top-level with a custom set of statically compiled module, just build these modules with emop.top as main module. A program can execute a top-level at any time with a custom syntax by creating a top-level with emop.top:new/1. This function without argument returns a module with two predicates: the predicate import/1 adds a module in the scope of top-level goals, and loop/0 runs the top-level loop. Remember to import at least emop.syntax:syntax if top-level goals have to use the EMoP default syntax.

module example {
   main :-
      emop.top:new.(
         import(emop.syntax:syntax),
         import() {
            syntax: infix '#'.
            constructor: '#'/2.
         },
         loop
      ).
}

Syntax

The source files are supposed to be encoded in UTF-8.

An identifier is either

Note that in any case, an ending dot is not considered to belong to an identifier if it is not preceded itself by another dot, therefore the dot operator that separates clauses can be written next to the last identifier of the clause.

Quotes:

An unquoted identifier is a variable if it is not followed by a sequence of arguments and if its initial letter is an ASCII upper-case letter between A and Z or an underscore. In X(), X is followed by an empty sequence of arguments, therefore it is read as the predicate `X'.

Exception handling

As in Prolog, exceptions are thrown with throw(E) and caught with catch(G, E', G'): if G throws an exception, then either E can be unified with E', then G is backtracked and G' is executed, or E cannot be unified with E', then E is thrown again. An uncaught exception interrupts the execution with an error message and with the exit code 1.

When a call is prefixed by M and M is uninstanciated, the exception error(instanciation_error(emop_call / 3), Pos) is thrown where Pos identifies position of the call in the code. If M is not a valid module, the exception error(unknown_module, Pos) is thrown. If the called predicate F / N is not defined in M, the exception error(unknown_predicate(F / N), Pos) is thrown.

Sockets

net.socket:inet(M) creates a new INET socket and returns a module M with the following predicates.

Example.
module example {
   main :-
      net.socket:inet.(
         bind('localhost', Port),
         listen(5),
         Stream = accept
      ),
      Stream:write('hello'),
      Stream:read_term(T).
}

Compilation chain

The emop command compiles all the modules listed in the command-line and their dependencies and build an executable which runs the initialization code of each module and then runs the predicate main of the last listed module. Dependencies are file modules which appear in import directives or as a call prefix. The --deps option makes the compiler list all the modules involved during the compilation to the standard output.

Modules explicitly listed in the command-line are initialized in the order of their appearance. Dependencies are initialized before the modules in the command-line which depend on them and, more generally, a module A is guaranteed to be initialized before a module B if B depends on A but not the converse. In case of mutual dependencies between modules not listed in the command-line, the initialization order is unspecified.

Therefore, it is safe to call modules from the standard library during the initialization since they are guaranteed to be initialized before.

If .pl, .wam, .c or .o files are listed in the command-line, they will be listed first in the command-line for the linking phase with gplc.

From a source file path/to/example.mpl, the following object files are generated.

path/to/example.mpi
The interface file which sums up the information gathered during the compilation (dependencies, module signatures, syntax definitions) to allow subsequent compilations to obtain these informations without having to recompile the file if it is unchanged.
path/to/example.o
Generated by gplc from example.wam.

The folowing intermediary files are generated in a temporary directory, they are usually deleted except if an explicit --temp-dir is given.

(temp-dir)/path.to.example.pl
The Prolog expansion of the EMoP code.
(temp-dir)/path.to.example.unpatched.wam
Generated by gplc from example.pl.
(temp-dir)/path.to..wam
Obtained from example.unpatched.wam by substituting cut instructions to get correct cut semantics.

At the end of the compilation, supposing that the main module is example.mpl, a file example.link.pl is generated, which contains the code for calling initializers and for dispatching module calls. Then, this file, all the object files, and the runtime (usually runtime.o, or runtime_debug.o if a trace was requested) are linked together by gplc.

Cuts

The cut goal ! suppresses all the choice points introduced since the call to the current predicate, including choices between its clauses and choice points introduced by the ; operator, the repeat keyword and so on. Choice points for clauses from other module definitions are removed as well.

This behavior does not correspond exactly to the ! in the underlying Prolog implementation: as for example, in GNU Prolog, a ! in the condition of a -> only cuts up to the beginning of the condition, including the choice point for the optional else part (this can vary from one Prolog implementation to another). Moreover, module definitions are compiled as disjoint sets of predicates since there is no notion of module unification at Prolog level, this is up to the EMoP runtime to try to execute the predicates defined in the module definitions successively. Choice points between one module definition to the other are therefore beyond the scope of the Prolog !. The ! semantics have therefore to be changed to fit the EMoP ! specification.

At Prolog level, each compiled EMoP predicate has an additional parameter. This cut level is an opaque value which can be used in the WAM low-level version of cut to choose up to which choice points cut should act. Since GNU Prolog is used to translate the Prolog code to WAM and there is no access to this low-level version of cut through the Prolog built-ins, the WAM code generated by gplc is patched, and the patched version is then compiled with gplc to native code. The Prolog code produced by the EMoP compiler has been designed so that its semantics is correct even unpatched, except that the ! scope is the one provided by GNU Prolog. Therefore, a code without ! neither in conditions and nor in clauses which span on several module definitions do not need to be patched.

The patch works as follows. There are indeed two distinct steps. The EMoP runtime is patched to get the cut level before introducing the choice points between the different module definitions. The compiled EMoP modules are patched to cut at a given cut level. The WAM instruction

cut(v)

cuts to the cut level stored in the WAM variable v. To unify a variable Cut the current cut level, the Prolog version of the EMoP runtime executes the goal

!, Cut = '$cut'

which emits, between some loads and stores, the sequence of WAM instructions

cut(v), put_atom('$cut', r)

where v is a WAM variable and r a WAM register. The tool patch_runtime acts as a filter on WAM files to replace such a sequence of instructions by

put_value(v, r)

storing the cut level at the place where the atom '$cut' was stored.

Conversely, to cut up to a cut level Cut, the Prolog code produced an EMoP cut is

Cut = '$cut', !

which emits, between some loads and stores, the sequence of WAM instructions

get_atom('$cut', r), cut(v)

where r a WAM register and v is the WAM variable where the cut level of the current Prolog clause has been stored. The EMoP compiler replaces such a sequence of instructions by

cut('x'(r))

cutting up to the cut level which is in Cut (where the Prolog code pretended to expect the atom '$cut'). It is worth noticing that if nothing is patched, the initially fresh variable Cut is just unified to '$cut' by the runtime (and the ! is just a nop since there is no choice point to cut at this place) and that an EMoP cut just unifies Cut with '$cut' which is the value that Cut already has, before cutting.

Such a patch relies on the fact that, fortunately, GNU Prolog does not try to optimize such code (in particular the superfluous cut in the runtime). One can expect to have to adapt this patch for future versions of GNU Prolog.

As an experimental feature, the EMoP code can obtain the current cut level through the variable `$CutLevel` and can cut at a given cut level with the goal !(Level). In particular, ! is equivalent to !(`$CutLevel`).

Bibliography