#ifndef TO_ADA_CLASS
#define TO_ADA_CLASS

// to_ada: a parser that turns ada subprograms and their associated ZENO
// specifications into full Ada programs that meet certain characteristics
// of their specifications.

#include "zeno_tree.h"
#include "symbol_tree.h"
#include "operation.h"
#include "tree_content.h"
#include "strings.h"
#include "info_unit.h"

// home brew support: variables used within lex and yacc source files.
extern int last_token;
extern int ZENO_OPENED;

// E_N_R_H_E_R_E: if this is defined, then it means that a particular check
// WILL be made for return statements used as ZENO conclusions: if the result
// associated with the consequence concluding the operation has a type of Nil,
// then the compiler will flag any return with an expression as an error.
// e.g., say an operation check_erroneous_value has a consequence called
// value_is_erroneous, and that consequence has a Nil result.  If the return
// statement used as a conclusion is in the form: return;, then everything
// is fine.  but if it is in the form: return <expression>;, then the compiler
// reports an error for that statement.
#define ENSURE_NIL_RESULTS_HAVE_EMPTY_RETURN_EXPRESSIONS

class to_ada
{
public:
  // the constructor takes a file name for the pre-processor to obtain Ada
  // and ZENO information from and it takes a symbol_tree that will be modified
  // to include the symbols defined in the file.  the symbol_tree should be at
  // the outermost (or library) scope when it is given to the constructor.
  to_ada(string file_name, symbol_tree *current_tables);
  ~to_ada();

  // parser_only: if the pre-processor is to only emit Ada and not look at the
  // ZENO specifications, then this is TRUE.
  int parser_only();
  void set_parser_only();

  // symbols: returns a pointer to the symbol tree.
  symbol_tree *symbols();

// The following routines all create a zeno_contents node for the zeno_tree
// being constructed.  They are each responsible for managing the storage of
// the zeno_trees passed to them.

  // format: called to print out the program unit when parsed.
  void format(zeno_tree *to_format);

  // save_spec: adds the specification to the symbol table.
  zeno_tree *save_spec(zeno_tree *op_spec);

  enum ada_consequence_types { NOT_FAILURE, FAILURE };

  // add_consequence: stuffs the information for the result and outcome of a
  // consequence into a consequence node in the zeno_tree.
  zeno_tree *add_consequence
    (zeno_tree *cons_name, zeno_tree *out_name, zeno_tree *res_name,
     ada_consequence_types ada_conseq_class);

  // add_consequences: updates a list of consequences by adding a new member to
  // the list.
  zeno_tree *add_consequences
    (zeno_tree *new_consequence, zeno_tree *conseq_list);

  // add_conclusion: creates a conclusion object and returns it.
  zeno_tree *add_conclusion(zeno_tree *indicator);

  // add_connection_conclusion: attaches the conclusion engendered by this
  // connection to it.
  zeno_tree *add_connection_conclusion
    (zeno_tree *connected, zeno_tree *concluded);

  // add_connection: creates a connection node for the operation specified
  // when it concludes with the consequence specified.
  zeno_tree *add_connection
    (zeno_tree *operation_name, zeno_tree *consequence_name);

  // make_operation: creates an operation node from the operation name and the
  // specifications for its consequences.
  zeno_tree *make_operation(zeno_tree *name, zeno_tree *consequence_specs);

  // add_outcome: creates a node containing an outcome.
  zeno_tree *add_outcome(zeno_tree *result_expr, zeno_tree *type_spec);

  // add_result: creates a node containing a result.
  zeno_tree *add_result
    (zeno_tree *characteristic_predicate, zeno_tree *type_spec);

  // connect_submerged_zeno: establishes a connection between a piece of ada
  // code and a previously found connection, conclusion, or both.
  zeno_tree *connect_submerged_zeno
    (zeno_tree *specified_label, zeno_tree *zeno_connection,
     zeno_tree *code_block);

  // mangle_subprg_spec: modifies the specification of the ada subprogram by
  // taking into account the need to return a ZENO consequence.
  // functions are turned into procedures to allow the result of the function
  // to be passed in the consequence.  if the p_c_d flag is true, then a
  // type definition for the consequence type used to return information is
  // included in front of the subprogram specification.

// perhaps this should be called by a tree traversal routine after the
// entire tree has been assembled for this file?

  zeno_tree *mangle_subprg_spec(zeno_tree *zeno_spec, zeno_tree *subprg_spec,
				int prepend_consequence_definition);

  // mangle_subprg_body: modifies the body of a subprogram appropriately to
  // guarantee the parts of its spec that can be guaranteed currently.
  // these include:
  //
  zeno_tree *mangle_subprg_body(zeno_tree *zeno_spec, zeno_tree *subprg_body);

  // mangle_possible_operation_name: looks up the name held in the tree and
  // inserts the appropriate ada code for dealing with its consequences if
  // it is actually listed in the symbol table as an operation.
  zeno_tree *mangle_possible_operation_name
    (zeno_tree *name_to_examine, zeno_tree *semicolon_after);

  // patch_zeno_user: connects operation invocations to their continuations
  // in an operation using ZENO.
  zeno_tree *patch_zeno_user(zeno_tree *subprg_body);

  // check_well_form: makes sure that the zeno object in the tree specified is
  // well formed.
  void check_well_form(zeno_tree *z_object, char *func_name);

  // add_scope: pushes a new scope onto the symbol tree.  if the parser is
  // in the parser only mode, then this does nothing.
  void add_scope(zeno_tree *scope_name);
  void add_scope(string scope_name);

  // remove_scope: pops the current scope off of the symbol tree.  a nil
  // operation if the parser is set to parser only.
  void remove_scope();

  // current_consequence_number: an increasing number that is used to
  // distinguish the variables used to hold returned consequences.
  int current_consequence_number;

  // current_info_unit: the structure holding the information needed per each
  // block of ada.
  info_unit *current_info_unit;

private:
  // parse_only: a flag telling the preprocessor not to mangle ZENO specs.
  int parse_only;

  // source_tree: the symbol tree that is having current file's operations and
  // operation users added to it.
  symbol_tree *source_tree;

  // set_up_conclusion: mangles the zeno conclusion that is held at the
  // specified index.  the ada code around the zeno conclusion is mutated into
  // the zeno form.
  void set_up_conclusion(int symbol_index);

  // resolve_connection: the unresolved connection is connected to the
  // appropriate connection found in the source code.
  void resolve_connection(connection *unresolved, connection *found);

  // create_end_of_internal_frame: creates a tree containing:
  //    end; exception when others => consequence.outcome =
  zeno_tree *create_end_of_internal_frame();

  // create_end_of_external_frame: creates a tree containing:
  //    ; return; end
  zeno_tree *create_end_of_external_frame();

  // create_operation_frame: returns a tree containing the basic operation
  // structure.
  zeno_tree *create_operation_frame
    (operation *zeno_spec, zeno_tree *subprg_spec);

  // patch_zeno_connections: composes the fully implemented zeno operation from
  // the partial form after the connections have been specified.  since the
  // parse of the operation does not encounter the connections until the entire
  // frame has been seen, the locations where control is transferred must be
  // specified at the end of parsing the operation.  the necessary connections
  // are retrieved from the symbol table.
  zeno_tree *patch_zeno_connections
    (zeno_tree *zeno_spec, zeno_tree *partial_implementation);

  // lookup_failure_consequence: finds the consequence that is specified for
  // the possibility of ada sub-unit failure.  it is an error if more than one
  // are specified.  if none is specified, then NIL is returned.
  zeno_tree *lookup_failure_consequence(operation *zeno_spec);

  // create_consequence_type: returns the type definition needed for an
  // operation's consequence to be returned.
  zeno_tree *create_consequence_type(zeno_tree *zeno_spec);

  // print_nodule: a simple debugging function that assumes that the contents
  // are the ada type.  it prints out the text held.
  friend void print_nodule(tree *to_print);

  // create_info_unit: creates a new info unit to hold per scope information
  // during parsing.
  info_unit *create_info_unit();
};

#endif