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
  | 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.
    expr ,arguments
  | expr
The arguments of function should be separated with comma ','.
    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. 
    axiom axioms
  | axiom
The user can give axioms only for selectors 
    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.
A function can have empty domain (they are constants)
    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.
    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) 
    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
    selector selectors
  | selector
User should give at least one selector for each ADT.  If it has generators it must have at least an equality.
    ident ,notEmptyParameters
  | ident
An ADT can have parameters (in that case it is a generic ADT). 
In this version of ManTa the parameters are not fully supported.  Hence their dynamic semantics will not be described in this document.
  ADT ident [parameters ]
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

 2.4 Conjectures Syntax
    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)


The Abstract Syntax Tree