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

• ManTa 3.1 is case sensitive. In a ManTa file spaces, CR/LF and tabulators are ignored.
• Comments should be between /* and */.  Nested comments are not allowed.
• The reserved keywords in ADT definitions are: ADT, INITIALS, CONSTRUCTORS, SELECTORS, AXIOMS, ERROR, EQUAL, if, then, else, fi, (i), (c), =, ->, :, *, (, ), [, ] and comma ','.
• The reserved keywords giving terms to rewrite are ERROR, EQUAL, if, then, else, fi, (, ), and comma
• The reserved keywords giving conjectures to prove are ERROR, EQUAL, if, then, else, fi, =, (, ) and comma
• Identifiers must begin with a letter (uppercase or lowercase) and then other letters, digits and underscores '_'.  The maximum length of an identifier is 32.

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

conjExpr=
    expr = expr

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).

• Commentaries are not affected
• Characters should be between quotes ' (e.g. 'a').  They are translated  to char(N) where N is the ASCII code of the character (in ManTa notation).  Some special sequences that are allowed are:
• '\n' Line Feed,   '\r' -> Carriage return, '\t' tabulator, '\b' Backspace, '\"' , '\\' the backslash, '\'', '\d' the character with ASCII code d (d a number written in decimal).
• Strings should be between double quotes " (e.g. "This is a string").  They are translated to lists (constructed by nil_string and cons_string).   A string can include some special sequences:
•   \" to represent ", \n  line feed, \r carriage return, \t tabulator, \b backspace, \' to represent ', \\ is backslash, \d where d is a decimal number (at most 3 digits) and represents the character with ASCII code d.
The numbers should be written in decimal and only integer positive numbers are converted to the notation SUC(SUC....SUC(ZERO)...).

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)

• The identifiers should be meaningful
• The ADTs identifiers should begin with an uppercase letter.  (e.g. AbsType)
• Functions (initials, constructros and selectors) should begin with a lowercase (e.g. absType)
• The parameters of an ADT should be in uppercase
• Variable names should be short but meaningful, they should be in lowercase (don´t use variables i nor c, since the symbols (i) and (c) are reserved)
• Although the name of an initial or constructor can be the ADT name, this is not recommended since it could cause problems when translating to pogramming languages

Contents The Abstract Syntax Tree