The following is a canonical list of all error messages generated by the Prop translator. Each message is prefixed by the file name and line number in which the error occurs. Most of these errors messages are self explanatory; more detailed explanations are provided below.
| Error | Explanation |
| unknown option option | The translator does not recognize the command line option. Type prop to see a list of options. |
| Error in command: command | The translator fails when trying to execution command. When multiple files are specified in a command line, prop invokes itself on each of the file. |
| pat with type type is not unifiable | Pattern has not been declared to be a unifiable type. |
| Sorry: pattern not supported in rewriting: pat | Pattern pat is not supported. Currently, logical pattern connectives are not supported in rewriting. You'll have to rewrite them into non-logical form. |
| Unknown complexity operator: op | |
| accessor is undefined for view pattern: pat | An accessor function has not been declared for a constructor. When using datatype views |
| arity mismatch (expecting n) in pattern: pat | Pattern pat is expected to have arity n. The arity is the number of expressions that you're matching concurrently. If you are matching n objects then there must be n patterns for each rule. |
| arity mismatch in logical pattern: pat | Logical patterns do not match the arity of a pattern. |
| bad constructor type type | |
| bad view constructor pattern: pat | |
| can't find include file file | Additional search paths can be specified with the -I option |
| component #i not found in constructor con | Datatype constructor con does not have a component named #i. This can happen when you write a record constructor expression and misspelt one of the labels. |
| component l not found in constructor con | Datatype constructor con does not have a labeled component l. |
| constructor con already has print formats | |
| constructor con is not a class | |
| constructor con is not a lexeme | A constructor is used as a terminal in the parser but it has not been declared to be a lexeme. |
| constructor con doesn't take labeled arguments | You're trying to use record constructor syntax on a constructor take does not take record arguments. |
| constructor con is undefined | |
| cyclic type definition in type id = type | Type abbreviations cannot be cyclic. For recursive types, use datatype definitions. |
| datatype T is not a lexeme type | T is used as a terminal within syntax class when it has not been declared as a lexeme type. All non-terminals must be a defined using the lexeme qualifier. |
| determinism det not recognized |
| Error | Explanation |
| duplicated definition of pattern constructor 'con' | The constructor con has already been in another datatype. Prop does not allow overloading of constructor names. |
| duplicated label 'l' in expression: exp | A record type has one of its labels duplicated. |
| duplicated label 'l' in type type | |
| duplicated pattern variable 'id'. Use option -N | By default, pattern variables may not be duplicated within a pattern. Non-linear patterns are allowed only when the option -N is invoked. |
| edge e is not defined in graphtype id | |
| empty type list in rewrite (...) ... | |
| expecting c1 ... c2 (from line l) but found c3 ... c4 instead | Quotation symbols are not properly balanced. |
| expecting non-terminal nt to have type t1 but found t2 | Non-terminal nt has already been defined to have a synthesized attribute type of t1 but t2 is found. This can happen if you have rules with the same lhs non-terminal previously defined. |
| expecting type t1 but found t2 in pattern variable 'v' | Prop performs type inference on all the lhs patterns to determine the types of all variables. Type errors can occur if the patterns are miswritten. |
| expecting type t1 but found t2 | |
| flexible vector pattern currently not supported in rewriting: pat | |
| format #i used on constructor con | |
| format #l used on non-record constructor con | |
| function name mismatch: expecting f ... | |
| illegal character c | |
| illegal context type: type | A context type in a matchscan statement must be previously defined to be datatype. The unit constructors of the datatype can be used as context values. |
| illegal context(s) in pattern pat | |
| illegal format '_' on constructor con | |
| illegal incomplete record pattern: pat | |
| illegal print format 'c' in constructor con | |
| illegal record label 'l' in expression: exp | |
| illegal width in bitfield 'id (n)' | |
| inherited attribute 'type' can only be used in treeparser mode in rewrite class id |
| Error | Explanation |
| law id(...) = pat is not invertible | Pattern pat cannot be treated as an expression. It may involve logical patterns and wild cards. |
| law 'id': bound variable 'v' is absent in body exp | A parameter variable v must be present within the body of a law. |
| law 'id': type type cannot be used in parameter id | |
| lexeme id is undefined | |
| lexeme class id is undefined | |
| lexeme pattern is undefined for constructor con | |
| lexeme {id} already defined as regexp | |
| lexeme {id} is undefined in regexp | |
| missing '}' in regular expression regexp | |
| missing label 'l' in expression: con exp | |
| missing non-terminal in tree grammar rule: nt | |
| missing type type in the traversal list of rewrite class id | Within the rewriting rules, you have used a pattern that involve a constructor of type type directly but no such types are defined in the rewrite class definition. You should add the type to the traversal list. |
| missing type info in expression exp : type | Sometimes prop fails to infer the type of an expression within a match statement. It such cases it is necessary to help out the translator by adding additional type information in the patterns. For example, rewrite some pattern p as (p : t) where t is the type of p. |
| missing type info in function f type | Similar to above |
| missing type info in rule: f pat : type | Similar to above. |
| missing view selector for pattern: pat | |
| multiple mixed polarity pattern variable 'v' | |
| multiple unit constructors in polymorphic type id arg is not supported | |
| negative cost cost is illegal | |
| node id is not defined in graphtype id | |
| non lexeme type type in pattern pat | |
| non-relation type type in pattern: pat | |
| pattern is undefined for lexeme l | |
| pattern scope stack overflows | |
| pattern scope stack underflows |
| Error | Explanation |
| pattern variable 'v' has no binding at this point | |
| persist object id is undefined for con | |
| persistence pid name already allocated for type type | |
| persistence redefined for type type | |
| precedence symbol must be terminal: term | |
| predicate p: expecting type t1 but found t2 | |
| redefinition of bitfield 'field'. | |
| redefinition of constructor 'con' | |
| redefinition of datatype id | |
| redefinition of lexeme class id | |
| replacement not in rewrite class: rewrite exp | |
| rewrite class id has already been defined | |
| rewrite class id is undefined | |
| rule r has incomplete type type | |
| rule r is of a non datatype: type | |
| syntax class id has already been defined | |
| syntax class id is undefined | |
| synthesized attribute 'type' can only be used in treeparser mode in rewrite class id | |
| the class representation of constructor id has been elided | |
| this rule is never selected: r | |
| this rule is never used: r | |
| too few arguments arg in instantiation of type scheme type | |
| too many arguments arg in instantiation of type scheme type | |
| type type is not a datatype | |
| type type is undefined |
| Error | Explanation |
| type id = type is not a datatype | |
| type id has already been defined as type | |
| type id has unknown class: C | |
| type 'type' is not rewritable in treeparser mode rewrite class id | All datatypes used within the treeparser mode of rewriting must be defined with the rewrite qualifier. |
| type error in pattern pat: type | |
| type mismatch between nonterminal nt(type t1) and rule r(type t2) | |
| type mismatch in pattern: pat | |
| type mismatch in rule r | |
| type mismatch in rule r pat | |
| type or constructor con is undefined | |
| unable to apply pattern scheme pat | |
| unbalanced c1 ... c2 at end of file | |
| undefined non-terminal nt | |
| unification fails occurs check with t1 and t2 | |
| unmatched ending quote c | |
| unrecognized quoted expression `exp` | |
| unrecognized quoted pattern `pat` |