ManTa 3 
With ManTa a user can: specify ADT, propose terms to rewrite (find
normal form), or propose conjectures to be proved. Each one has a specific
syntax
2.1
Lexical Conventios

2.2
ADT Syntax in BNF

ident = ['A''Z' 'a''z'] ['A''Z' 'a''z' '0''9' '_']*  An identifier should begin with a letter. We could allow more identifiers (e.g. $, %, &, etc), but this could make difficult the translation to some programming languages 
expr =
 ERROR  EQUAL( expr , expr )  if expr thenexprelseexprfi  ident ( arguments )  ident 
The expressions are built with: ERROR, EQUAL(.,.) if . then . else
. fi. Functions instanced and constants.
Constants are treated as functions without parameters (empty domain), they should be written without parenthesis. 
arguments =
expr ,arguments  expr 
The arguments of function should be separated with comma ','. 
axiom=
expr =expr 
An axiom is an equality between expressions. It's not an assignment but a rewriting rule (the left side rewrites in the rigth one) as will be seen later. 
axioms =
axiom axioms  axiom 
The user can give axioms only for selectors 
notEmptyDomain=
ident (i) *notEmptyDomain  ident * notEmptyDomain  ident (i)  ident 
The domain of a function can be a product of ADTs each one of them can be inductive (used to make induction in proofs) or not. 
domain=
notEmptyDomain  
A function can have empty domain (they are constants) 
generator =
ident :domain>ident 
A generator is a function whose codomain should be the defined ADT. There are two kinds of them: initials and constructors. However the differences are not captured here but with the static semantics. 
generators =
generator generators  
User should not give axioms for generators. Note that an ADT can have no generators in that case it is an extension (just a set of new selectors to extend other ADTs) 
selector =
ident (c):domain>ident ident :domain>ident 
A selector is a function with axioms given by the user. The presented rule only describes the signature for a selector, the sintax of the axioms was already presented (see axiom) 
selectors =
selector selectors  selector 
User should give at least one selector for each ADT. If it has generators it must have at least an equality. 
notEmptyParameters =
ident ,notEmptyParameters  ident 
An ADT can have parameters (in that case it is a generic ADT). 
parameters=
notEmptyParameters  
In this version of ManTa the parameters are not fully supported. Hence their dynamic semantics will not be described in this document. 
adt=
ADT ident [parameters ] INITIALS generators CONSTRUCTORS generators SELECTORS selectors AXIOMS axioms 
An ADT has a name, it can have parameters, generators called initials (they don´t include the defined ADT in it's domain) and generators called constructors (they include the ADT in it's domain). Each declared selector should have axioms to define it's behavior on generators 
There are available a lexical analyzer to
be used with ocamllex, and a parser to be used
with ocamlyacc. They can be adapted easily to other tools (e.g. flex
and bison).
2.3
Normalization Syntax

normExpr=
expr
2.4 Conjectures
Syntax

conjExpr=
expr = expr
2.5 Predefined
Abstract Data Types

The only primitive ADT in ManTa is BOOL. It defines boolean values TRUE, FALSE and the functions AND(.,.), OR(.,.), NOT(.), IMP(.,.), EQ_BOOL(.,.). It's required by the built in function if E1 then E2 else E3 fi, whose first parameter (E1) must have type BOOL.
Other predefined ADTs are: NAT (natural numbers), Char and String. By default these types can't be modified.
In adition to those types there are some classical ADT: List,
Queue,
Stack.
2.6 The preprocessor

Writing ManTa files (ADT, conjectures or terms to rewrite) that require
the primitive types NAT, Char
and String is difficult,
boring and prone to errors. This is so since the numbers have to
be represented as SUC(SUC...(SUC(ZERO))..), the character
as char(SUC(SUC(...SUC(ZERO)...)) and the String
as lists of characters.
With a preprocessor the user can write easier and faster by using numbers,
character constants and strings. The preprocessor receives
such files as inputs, transforms them to ManTa syntax and writes files.
The preprocessor works only at lexical level, it doesn't check the syntax of the file (so it can be used with any file, i.e. specifications, terms to rewrite or conjectures).
2.7 The postprocessor

This component should be the inverse of the preprocessor. It receives
a ManTa file and it returns a text file easy to read. (NAT ground
terms translated to numbers, special characters translated, strings translated,
etc.)
2.8 Suggested
conventions

To facilitate writing and reading ADTs and conjectures, some conventions are suggested (inspired in the Java Language conventions)
