``The name X is already used for Y.''There is a double definition. X refers to a name that as already been defined somewhere else in your specification. Y refers to this previous definition and indicates which kind of definition (formalism, phylum, operator) it is.
This message can be either an error message or a warning. In AS, you can give the same name to define a type (formalism or phylum) and an operator, however in this case a warning message will be emitted by the type checker. Note that it is not possible to give the same name to a formalism and to a phylum belonging to this formalism.
``The type X is not defined.''X refers to the use of an undefined type name. To define a phylum, one have to either define an operator belonging to this phylum or to include some other phylum in it. To refer to a phylum belonging to an other formalism, use the form P::L where P is the name of a phylum belonging to the formalism L.
``I cannot find the formalism X.''The formalism X cannot be found by the system. X must be a Centaur formalism and must appear in the list given by Centaur when clicking on ``Reload/Formalism''. Check your resources if this formalism exists and is not accessible by Centaur.
If Centaur is not running on the same computer than Eclipse, verify that both computer can see the same file system.
Using an AS-defined Formalism in the Centaur Environment
``The formalism X does not define Y.''X refers to a formalism name. Y refers to a phylum that do not belong to X as expected by the expression Y::X.
``The phylum X is closed.''X refers to a phylum that is closed, i.e. it is not possible to modify this phylum by defining new constructors or by including some other phylum in it.
This is the case for phyla defined as the union of other phyla.
``The phylum X should be a singleton to be used in a lambda definition.''Only singleton phylum (i.e. containing exactly one constructor) can be used as binder in second-order types.
X refers to a phylum defined locally that contains more than one operator and gives you the list of operators belonging to this phylum.
``The phylum X (= Y) should be a singleton to be used in a lambda definition.''Only singleton phylum (i.e. containing exactly one constructor) can be used as binder in second order types.
X refers to an imported phylum that contains more than one operator. The tag Y gives you the list of operators belonging to this phylum.
``In phylum X, Y should be defined with signature Z to be usable in a lambda definition.''X refers to a phylum name occurrence in a second-order type expression. When X is not an imported phylum, Y refers to the definition of the unique constructor belonging to X. Z gives you the acceptable signature such that Y can be used in a lambda definition.
``The phylum X is not effective.''X refers to a phylum definition. This phylum is not effective, i.e. it is not possible to construct a ground term of type X.
Even if this fact is reported by the type-checker as a warning, most of the time this is an error in the design of your abstract syntax.
However, if the formalism that you are defining is intended to be extended by adding some constructors, X can become effective only after the extension.
``The name meta is not allowed for an operator.''The operator name ``meta'' is reserved. When creating a formalism for the VTP of Centaur, a special operator named ``meta'' used to create schemes (or incomplete trees) in Centaur will be added to every phylum of the syntax. This node must not be defined or redefined in an AS specification. The tag ``meta'' refers to the incorrect declaration.
``The name X is both defined as Y and imported from Z.''A name is both imported from some external formalism Z as an operator and defined in the present specification, leading to a name conflict. Y refers to the local definition of X and indicate the kind of definition involved, while X and Z refers to the place where it has been imported from Z.
This message can be either an error message or a warning. In AS, you can give the same name to define a type (formalism or phylum) and an operator, however in this case a warning message will be emitted by the type checker. Note that it is not possible to give the same name to a formalism and to a phylum belonging to this formalism.
Names,
Typed Names
Complete Definition of an Abstract Syntax
``The two phyla X and Y are identical (=Z).''X and Y refers to two phyla that contains exactly the same constructors. Z gives the list of these constructors.
This may be due to a circular inclusion of phyla.
``The formalism X is not defined using as.''X refers to a formalism that is imported in your specification, but that is not defined using AS. Only formalisms defined with AS can be extended.
``The file X defining Y cannot be read.''The formalism Y is defined with AS, but for some reason the file necessary to perform its extension cannot be read. It must be in the directory containing its AS specification.
If Centaur is not running on the same computer than Eclipse, check that both computer can see the same file system.
Using an AS-defined Formalism in the Centaur Environment
``You can't define and extend X at the same time.''Modular specifications must be stratified. ``define'' and ``extend'' refers to the places in your specification where X is used. One of them must be incorrect.
Formalism Extension,
Complete Definition of an Abstract Syntax
Thierry Despeyroux