// -*- mode: C++; c-file-style: "stroustrup"; c-basic-offset: 4; indent-tabs-mode: nil; -*-

/* libutap - Uppaal Timed Automata Parser.
   Copyright (C) 2002-2006 Uppsala University and Aalborg University.

   This library is free software; you can redistribute it and/or
   modify it under the terms of the GNU Lesser General Public License
   as published by the Free Software Foundation; either version 2.1 of
   the License, or (at your option) any later version.

   This library is distributed in the hope that it will be useful, but
   WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
   Lesser General Public License for more details.

   You should have received a copy of the GNU Lesser General Public
   License along with this library; if not, write to the Free Software
   Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
   USA
*/

#ifndef UTAP_INTERMEDIATE_HH
#define UTAP_INTERMEDIATE_HH

#include <list>
#include <vector>
#include <map>
#include <exception>

#include "utap/symbols.h"
#include "utap/expression.h"
#include "utap/position.h"

namespace UTAP
{
    /** Base type for variables, clocks, etc.  The user data of the
        corresponding symbol_t points to this structure,
        i.e. v.uid.getData() is a pointer to v.
    */
    struct variable_t
    {
        symbol_t uid;      /**< The symbol of the variables */
        expression_t expr; /**< The initialiser */
    };

    /** Information about a location.
        The symbol's user data points to this structure, i.e.
        s.uid.getData() is a pointer to s. Notice that the rate list
        is generated by the type checker; until then the rate
        expressions are part of the invariant.
    */
    struct state_t
    {
        symbol_t uid;                /**< The symbol of the location */
        expression_t invariant; /**< The invariant */
        expression_t costrate;  /**< Rate expression */
        int32_t locNr;                /**< Location number in template */
    };

    /** Information about an edge.  Edges have a source (src) and a
        destination (dst) locations. The guard, synchronisation and
        assignment are stored as expressions.
    */
    struct edge_t
    {
        int nr;                        /**< Placement in input file */
        bool control;           /**< Controllable (true/false) */
        state_t *src;                /**< Pointer to source location */
        state_t *dst;                /**< Pointer to destination location */
        frame_t select;         /**< Frame for non-deterministic select */
        expression_t guard;        /**< The guard */
        expression_t assign;        /**< The assignment */
        expression_t sync;        /**< The synchronisation */
    };

    class BlockStatement; // Forward declaration

    /** Information about a function. The symbol's user data points to
        this structure, i.e. f.uid.getData() is a pointer to f.
    */
    struct function_t
    {
        symbol_t uid;               /**< The symbol of the function. */
        std::set<symbol_t> changes; /**< Variables changed by this function. */
        std::set<symbol_t> depends; /**< Variables the function depends on. */
        std::list<variable_t> variables; /**< Local variables. */
        BlockStatement *body;       /**< Pointer to the block. */
        function_t() : body(NULL) {}
        ~function_t();
    };

    struct progress_t
    {
        expression_t guard;
        expression_t measure;
    };

    /**
     * Structure holding declarations of various types. Used by
     * templates and block statements.
     */
    struct declarations_t
    {
        frame_t frame;
        std::list<variable_t> variables;        /**< Variables */
        std::list<function_t> functions;        /**< Functions */
        std::list<progress_t> progress;         /**< Progress measures */

        /** Add function declaration. */
        bool addFunction(type_t type, std::string, function_t *&);
    };

    /** 
     * Partial instance of a template. Every template is also a
     * partial instance of itself and therefore template_t is derived
     * from instance_t. A complete instance is just a partial instance
     * without any parameters.
     *
     * Even though it is possible to make partial instances of partial
     * instances, they are not represented hierarchically: All
     * parameters and arguments are merged into this one
     * struct. Therefore \a parameters contains both bound and unbound
     * symbols: Unbound symbols are parameters of this instance. Bound
     * symbols are inherited from another instance. Symbols in \a
     * parameters are ordered such that unbound symbols are listed
     * first, i.e., uid.getType().size() == parameters.getSize().
     *
     * \a mapping binds parameters to expressions.
     *
     * \a arguments is the number of arguments given by the partial
     * instance. The first \a arguments bound symbols of \a parameters
     * are the corresponding parameters. For templates, \a arguments
     * is obviously 0.
     *
     * Restricted variables are those that are used either directly or
     * indirectly in the definition of array sizes. Any restricted
     * parameters have restriction on the kind of arguments they
     * accept (they must not depend on any free process parameters).
     *
     * If i is an instance, then i.uid.getData() == i. 
     */
    struct instance_t
    {
        symbol_t uid;                                   /**< The name */
        frame_t parameters;                       /**< The parameters */
        std::map<symbol_t, expression_t> mapping; /**< The arguments */
        size_t arguments;
        size_t unbound;
        struct template_t *templ;
        std::set<symbol_t> restricted;          /**< Restricted variables */
    };

    /**
     * Information about a template. A template is a parameterised
     * automaton with local declarations of variables and functions.
     */
    struct template_t : public instance_t, declarations_t
    {
        symbol_t init;                                /**< The initial location */
        frame_t templateset;                    /**< Template set decls */
        std::list<state_t> states;                /**< Locations */
        std::list<edge_t> edges;                /**< Edges */

        /** Add another location to template. */
        state_t &addLocation(std::string, expression_t inv);

        /** Add edge to template. */
        edge_t &addEdge(symbol_t src, symbol_t dst, bool type);
    };


    /** 
     * Channel priority information. The expression must be a a
     * channel or an array of channels.
     */
    struct chan_priority_t
    {
        expression_t chanElement;
        int chanPriority;
    };

    class TimedAutomataSystem;

    class SystemVisitor
    {
    public:
        virtual ~SystemVisitor() {}
        virtual void visitSystemBefore(TimedAutomataSystem *) {}
        virtual void visitSystemAfter(TimedAutomataSystem *) {}
        virtual void visitVariable(variable_t &) {}
        virtual bool visitTemplateBefore(template_t &) { return true; }
        virtual void visitTemplateAfter(template_t &) {}
        virtual void visitState(state_t &) {}
        virtual void visitEdge(edge_t &) {}
        virtual void visitInstance(instance_t &) {}
        virtual void visitProcess(instance_t &) {}
        virtual void visitFunction(function_t &) {}
        virtual void visitTypeDef(symbol_t) {}
        virtual void visitProgressMeasure(progress_t &) {}
    };

    class TimedAutomataSystem
    {
    public:
        TimedAutomataSystem();
        virtual ~TimedAutomataSystem();

        /** Returns the global declarations of the system. */
        declarations_t &getGlobals();

        /** Returns the templates of the system. */
        std::list<template_t> &getTemplates();

        /** Returns the processes of the system. */
        std::list<instance_t> &getProcesses();

        void addPosition(
            uint32_t position, uint32_t offset, uint32_t line, std::string path);
        const Positions::line_t &findPosition(uint32_t position) const;

        variable_t *addVariableToFunction(
            function_t *, frame_t, type_t, std::string, expression_t initital);
        variable_t *addVariable(
            declarations_t *, type_t type, std::string, expression_t initial);
        void addProgressMeasure(
            declarations_t *, expression_t guard, expression_t measure);

        template_t &addTemplate(std::string, frame_t params);
        instance_t &addInstance(
            std::string name, instance_t &instance, frame_t params, 
            const std::vector<expression_t> &arguments);
        void addProcess(instance_t &instance);
        void accept(SystemVisitor &);

        void setBeforeUpdate(expression_t);
        expression_t getBeforeUpdate();
        void setAfterUpdate(expression_t);
        expression_t getAfterUpdate();

        /* The default priority for channels is also used for 'tau
         * transitions' (i.e. non-synchronizing transitions).
         */
        void setChanPriority(expression_t chan, int priority);
        const std::list<chan_priority_t>& getChanPriorities() const;
        std::list<chan_priority_t>& getMutableChanPriorities();
        void setDefaultChanPriority(int priority);
        int getTauPriority() const;

        /** Sets process priority for process \a name. */
        void setProcPriority(const char* name, int priority);

        /** Returns process priority for process \a name. */
        int getProcPriority(const char* name) const;

        /** Returns true if system has some priority declaration. */
        bool hasPriorityDeclaration() const;

    protected:
        bool hasPriorities;
        int defaultChanPriority;
        std::list<chan_priority_t> chanPriorities;
        std::map<std::string,int> procPriority;

    protected:
        // The list of templates.
        std::list<template_t> templates;

        // The list of template instances.
        std::list<instance_t> instances;

        // List of processes.
        std::list<instance_t> processes;

        // Global declarations
        declarations_t global;

        expression_t beforeUpdate;
        expression_t afterUpdate;

        variable_t *addVariable(
            std::list<variable_t> &variables, frame_t frame,
            type_t type, std::string);

    public:
        void addError(position_t, std::string);
        void addWarning(position_t, std::string);
        bool hasErrors() const;
        bool hasWarnings() const;
        const std::vector<error_t> &getErrors() const;
        const std::vector<error_t> &getWarnings() const;
        void clearErrors();
        void clearWarnings();

    private:
        std::vector<error_t> errors;
        std::vector<error_t> warnings;
        Positions positions;
    };
}

#endif