(** Time-stamp: <modified the 04/02/2009 (at 15:26) by Erwan Jahier> *)

(** 

 *)

(*----------------------------------------------------------------------
        module : Eff
        date :
------------------------------------------------------------------------

        DESCRIPTION :

        D�finition des structures de donn�es utilis�e pour la compil,
        plus des utilitaires pour les messages d'erreurs, de bug etc.
        N.B. on utilise beaucoup l'adjectif "effectif", qui signifie
        simplement "correct".

        REMARQUE GENERALE :

        D'une mani�re g�n�rale, la compil d'une entit� syntaxique
        "toto" est impl�ment�e par une fonction check_toto, qui
        prend en entr�e (entr'autre) un toto et renvoie un
        toto.

        TYPES DE DONNEES :

        - type_ :
        d�notation de type effectif, impl�mente l'�quivalence des types,
        construit � partir d'une type_exp.

        - const :
        d�notation de constante effective,
        construit � partir d'une val_exp => IL S'AGIT DE LA REPRESENTATION
        INTERNE DES CONSTANTES STATIQUES 

        - var_info :
        d�claration de variable,
        construit � partir de var_info.

        - val :
        union entre const et var_info.

        - slice_info :
        d�notation de tranche de tableau,
        construit � partir de slice_info.

        - left :
        version compil�e de left_part

        - eq_info :
        version compil�e de eq_info 

        - node_exp :
        d�notation d'op�ration,
        peut �tre  predef ou utilisateur,
        construit � partir de node_exp.

        - static_arg :
        d�claration d'un static arg

        - pack_env :
        la "grosse" structure de donn�es qui g�re la compilation
        des packages => impl�ment�e dans CheckGlobal pour la partie type/const/function
        (initialisation) et dans CheckNode pour la partie node/template qui
        est faite � la demande.

        - local_env :
        structure qui g�re l'environnement de compilation
        d'un noeud/template.

        TYPES FONCTIONNEL :

        - id_solver (en fait, une structure qui contient plusieurs fonctions,
          une pour traiter les constantes, une pour traiter les types)

        UTILITAIRES :

        - type_of_const : renvoie le type d'une const
        - string_of_type : pretty-print d'un type 
        - string_of_const : pretty-print d'une const 
        - string_of_node_key : pretty-print d'un node_key
        _ string_of_slice :

----------------------------------------------------------------------*)

open Printf 
open Lxm
open SyntaxTree
(* open SyntaxTreeCore *)

(*---------------------------------------------------------------------
Type : id_solver
-----------------------------------------------------------------------
        Joue le r�le d'environnemnt : contient des fonctions
        pour r�soudre les r�ferences aux idents.
        (voir par exemple EvalConst, EvalType)

N.B. On fournit les constructeurs des id_solver courants, voir :
        
----------------------------------------------------------------------*)
type id_solver = {
  (* XXX I should not have [idref] in this module !!! *)
  id2const : Ident.idref -> Lxm.t -> const;
  id2type  : Ident.idref -> Lxm.t -> type_;
  id2node  : Ident.idref -> static_arg list -> Lxm.t -> node_exp;
  id2var   : Ident.idref -> Lxm.t -> var_info;
  symbols  : SymbolTab.t;
}

(*---------------------------------------------------------------------
  Type : type
  -----------------------------------------------------------------------
  D�notation de type imm�diat : l'�quivalence s�mantique des types
  EST l'�quivalence structurelle des type. 
  Par rapport � une type_exp :
  - pas d'alias
  - taille des tableaux r�solues
  ----------------------------------------------------------------------*)

and type_ =
  | Bool_type_eff
  | Int_type_eff
  | Real_type_eff
  | External_type_eff of Ident.long
  | Enum_type_eff     of Ident.long * (Ident.long list)
  | Array_type_eff    of type_ * int
  | Struct_type_eff   of 
      Ident.long * (Ident.t * (type_ * const option)) list
  | Any
  | Overload 
      (* [Overload] is like [Any], except that it can only be [int] or [real] *)


and slice_info = {
(** D�notation de tranche de tableau correcte :
    si A est le tableau d'entr�e, alors S est le tableau
    de sortie avec :
    S[i] = A[first + i*step] pour i = 0 .. width
*)
  se_first : int;
  se_last : int;
  se_step : int;
  se_width : int; (* -> size? *)
}

and left =
(** Version check�e des left_part
  (les idents, les index et les tranches sont r�solus)

  N.B. On conserve aussi le type effectif de chaque noeud
  bien qu'il soit possible de le retrouver. 

  N.B. On garde aussi l'info source des idents au cas ou.*)
  | LeftVarEff   of (var_info * Lxm.t)
  | LeftFieldEff of (left * Ident.t * type_)
  | LeftArrayEff of (left * int * type_)
  | LeftSliceEff of (left * slice_info * type_)


and eq_info = left list * val_exp

and val_exp =
  | CallByPosEff  of (by_pos_op srcflagged * operands)
  | CallByNameEff of
      (by_name_op srcflagged * (Ident.t srcflagged * val_exp) list)

and operands = OperEff of val_exp list

and by_name_op =
  | STRUCT of Ident.pack_name * Ident.idref
  | STRUCT_anonymous


and by_pos_op =
  | Predef of Predef.op * static_arg list
  | CALL of node_exp srcflagged
  | IDENT of Ident.idref (* should be an Ident.t or long, really... *)
  | CONST of Ident.idref * Ident.pack_name

  | PRE
  | ARROW
  | FBY
  | CURRENT

  | WHEN of SyntaxTreeCore.clock_exp
  | TUPLE
  | WITH of val_exp

  | CONCAT
  | HAT of int * val_exp
  | ARRAY of val_exp list
  | STRUCT_ACCESS of Ident.t * type_

(* those are different from [by_pos_op] *)

  | ARRAY_ACCES of int * type_ (* index + type_ of the element *)
  | ARRAY_SLICE of slice_info * type_ 
  | MERGE       of (Ident.t * (Ident.t list))  
   

(*---------------------------------------------------------------------
  Type : const
  -----------------------------------------------------------------------
  D�notation de constante imm�diate
  N.B. les const "portent" leur type :
  - il est implicite pour bool, int, real, 
  - explicite pour extern, enum et struct
  - pour array c'est le TYPE DES ELEMENTS QU'ON TRIMBALE 
  VOIR => type_of_const
  ----------------------------------------------------------------------*)
and const =
    (* type predef *)
    Bool_const_eff of bool
  | Int_const_eff of int (* XXX should be a string ! *)
  | Real_const_eff of string
      (* type atomique non predef : on pr�cise le type *)
  | Extern_const_eff of (Ident.long * type_ * const option)
  | Enum_const_eff   of (Ident.long * type_)
      (* type_ structure : liste (champ,valeur) + type_ structure *)
  | Struct_const_eff of ((Ident.t * const) list * type_)
      (* type_ tableau : liste des valeurs + type_ des elts + taille *)
  | Array_const_eff of (const list * type_)
      (*---------------------------------------------------------------------
        Type: val   
        -----------------------------------------------------------------------
        Une constante ou une variable
        => item de la table des symboles de valeurs
        ----------------------------------------------------------------------*)
(* and val = *)
(*     ConstEff of const *)
(*   | VarEff of var_info *)
      (*---------------------------------------------------------------------
        Type: var_info      
        -----------------------------------------------------------------------
        Info associ�e � un ident de variable
        ----------------------------------------------------------------------*)
      (* ICI � completer/modifier sans doute *)
and var_info = {
  var_name_eff   : Ident.t;
  var_nature_eff : SyntaxTreeCore.var_nature;
  var_number_eff : int;
  var_type_eff   : type_;
  var_clock_eff  : id_clock;
}
and id_clock = Ident.t * clock
      (* 
         A pair made of an ident and its clock.

         The ident is used to relate arguments and parameters
         when clocking node calls (in order to be able to transmit
         the clocking constraints between the node I/O, in EvalClock.f).
      *)
and clock =
  | BaseEff
  | ClockVar of int (* to deal with polymorphic clocks (i.e., constants) *)
  | On of Ident.clk * clock 
      (* The clock expression, and the effective clock the clock var
         e.g., in 
            On((clk_constructor, clk_var), clk )
         clk is the clock of clk_var
      *)

(**********************************************************************************)
(** [node_exp] correspond � une instance de template (ou, cas
    limite, de noeud sans param statique).

    La cl� est un couple ident/liste d'arguments statiques effectifs

    N.B. une horloge formelle est soit None (base) soit l'index d'une
    entr�e (0..nb entr�es-1). Les formal-clocks sont cr��es au cours du
    type-checking (et pas du clock-checking)
*)
and node_exp = {
  node_key_eff : node_key;
  inlist_eff   : var_info list;
  outlist_eff  : var_info list;
  loclist_eff  : var_info list option; (* None => extern or abstract *)
  def_eff      : node_def;
  has_mem_eff  : bool;
  is_safe_eff  : bool;
  is_polym_eff : bool 
}

and node_def =
  | ExternEff
  | AbstractEff
  | BodyEff of node_body

and node_body = {
  asserts_eff : (val_exp srcflagged) list;
  eqs_eff     : (eq_info srcflagged) list;
}

(* key used  for type, constant, and clock tables *)
and item_key = Ident.long
and node_key = item_key * static_arg list
and static_arg =
  | ConstStaticArgEff of (Ident.t * const)
  | TypeStaticArgEff  of (Ident.t * type_)
  | NodeStaticArgEff  of (Ident.t * sarg_node_eff)

and sarg_node_eff = item_key * var_info list * var_info list
        
(****************************************************************************)
(** Type check_flag

   Au cours du check, on conserve le statut des idents :
   
   - Checking => en cours de traitement, permet de lever les r�cursions
   - Checked  => trait� et correct
   - Incorrect => d�j� marqu� comme incorrect (pas besoin d'un nouveau
   message d'erreur)
*)
type 'a check_flag =
    Checking
  | Checked of 'a
  | Incorrect


let (profile_of_node_exp : node_exp -> type_ list * type_ list) =
  fun ne -> 
    List.map (fun vi -> vi.var_type_eff) ne.inlist_eff,
    List.map (fun vi -> vi.var_type_eff) ne.outlist_eff
    
(****************************************************************************)
(* currently not used *)


(* type world_env = { *)
(*   wenv_src : SyntaxTree.pack_or_model list; *)
(*   wenv_mod_srcs : (Ident.t, SyntaxTree.model_info srcflagged) Hashtbl.t ; *)
(*   wenv_pack_srcs :  (Ident.t, SyntaxTree.pack_info srcflagged) Hashtbl.t ; *)
(*   wenv_pack_envs : (Ident.t, pack_env) Hashtbl.t ; *)
(* } *)
(* and pack_env = { *)
(*   penv_world : world_env ; *)
(*   (* penv_src : SyntaxTree.package ; *) *)
(*   penv_type_table  : (Ident.t, type check_flag)   Hashtbl.t ; *)
(*   penv_const_table : (Ident.t, const check_flag)  Hashtbl.t ; *)
(*   penv_oper_table  : (Ident.t, node_half) Hashtbl.t ; *)
(*   penv_node_table : (node_key, node_exp check_flag) Hashtbl.t *)
(* } *)

(* the local tables are indexed by Ident.t, because local idents (var,const, flow)
   cannot have any package name. 

   and for nodes, the only possibility to have an entry in this table is via the
   static parameters.
   
   i.e.  
        min_4 = min_n<< 4, toto<<2>> >> ;

   is not allowed (I think). One has to write something like :

      toto_2 = toto<<2>>;
      min_4 = min_n<< 4, toto_2 >> ;

   It would not be difficult to handle that here though.
*)
type local_env = {
  lenv_node_key : node_key ;
(*   lenv_globals : pack_env ; *)
  lenv_types : (Ident.t, type_) Hashtbl.t ;
  lenv_const : (Ident.t, const) Hashtbl.t ; 
  lenv_nodes : (Ident.t, sarg_node_eff) Hashtbl.t ; 

  lenv_vars  : (Ident.t, var_info) Hashtbl.t ; 
}


let (lookup_type: local_env -> Ident.idref -> Lxm.t -> type_) = 
  fun env id lxm -> 
    Hashtbl.find env.lenv_types (Ident.name_of_idref id)

let (lookup_node: 
       local_env -> Ident.idref -> static_arg list -> Lxm.t -> sarg_node_eff) = 
  fun env id sargs lmx -> Hashtbl.find env.lenv_nodes (Ident.name_of_idref id)
    
let (lookup_const: local_env -> Ident.idref -> Lxm.t -> const) = 
  fun env id lmx ->  
    Hashtbl.find env.lenv_const (Ident.name_of_idref id) 
          
let (lookup_var: local_env -> Ident.t -> Lxm.t -> var_info) = 
  fun env id lmx ->  
    Hashtbl.find env.lenv_vars id

          
let (make_local_env : node_key -> local_env) =
  fun nk ->
    let res =
      {
        lenv_node_key = nk;
        lenv_types = Hashtbl.create 0;
        lenv_const = Hashtbl.create 0;
        lenv_nodes = Hashtbl.create 0;
        lenv_vars  = Hashtbl.create 0;
      }
    in
      (* fill tables using static arg info *)
      List.iter
        (function
           | ConstStaticArgEff(id,ce) -> Hashtbl.add res.lenv_const id ce
           | TypeStaticArgEff(id,te)  -> Hashtbl.add res.lenv_types id te
           | NodeStaticArgEff(id, ne) -> Hashtbl.add res.lenv_nodes id ne
        )
        (snd nk);
      
      res

(****************************************************************************)
(** [type_are_compatible t1 t2] checks that t1 is compatible with t2, i.e., 
    if t1 = t2 or t1 is abstract and not t2.
*)
let (type_are_compatible : type_ -> type_ -> bool) =
  fun te1 te2 -> match te1, te2 with
    | External_type_eff id1, External_type_eff id2 -> id1 = id2
    | External_type_eff _, _ -> true
    | t1, t2 -> t1 = t2

let rec (clock_are_equals : clock -> clock -> bool) =
  fun c1 c2 -> match c1, c2 with
    | On(cid1,_), On(cid2,_) -> cid1 = cid2
(* equivalent ? try both before commit !!! *)
(*     | On(_,c1), On(_,c2) -> clock_are_equals c1 c2 *)
    | c1, c2 -> c1 = c2

let (var_are_compatible : var_info -> var_info -> bool) =
  fun v1 v2 -> 
    (type_are_compatible v1.var_type_eff v2.var_type_eff) &&
      (clock_are_equals (snd v1.var_clock_eff) (snd v2.var_clock_eff))
  
(****************************************************************************)
(* Utilitaires li�s aux node_key *)
let (make_simple_node_key : Ident.long -> node_key) =
  fun nkey -> (nkey, [])

let rec (subst_type : type_ -> type_ -> type_) =
  fun t teff_ext -> match teff_ext with
      (* substitutes [t] in [teff_ext] *)
    | Bool_type_eff -> Bool_type_eff
    | Int_type_eff -> Int_type_eff
    | Real_type_eff -> Real_type_eff
    | External_type_eff l -> External_type_eff l
    | Enum_type_eff(l,el) ->  Enum_type_eff(l,el)
    | Array_type_eff(teff_ext,i) -> 
        Array_type_eff(subst_type t teff_ext, i)
    | Struct_type_eff(l, fl) -> 
        Struct_type_eff(
          l, List.map (fun (id,(teff,copt)) -> (id,(subst_type t teff,copt))) fl)
    | Any 
    | Overload -> t

let rec (is_polymorphic : type_ -> bool) =
  fun t -> match t with
    | Bool_type_eff
    | Int_type_eff 
    | Real_type_eff
    | External_type_eff _
    | Enum_type_eff(_)  -> false
    | Any 
    | Overload -> true
    | Array_type_eff(teff_ext,i) -> is_polymorphic teff_ext
    | Struct_type_eff(l, fl) -> 
        List.exists (fun (_,(teff,_)) -> is_polymorphic teff) fl


let (type_of_const: const -> type_) =
  function
    | Bool_const_eff _ -> Bool_type_eff
    | Int_const_eff  _ -> Int_type_eff
    | Real_const_eff _ -> Real_type_eff
    | Extern_const_eff (s,  teff, vopt) -> teff
    | Enum_const_eff   (s,  teff) -> teff
    | Struct_const_eff (fl, teff) -> teff
    | Array_const_eff  (ct, teff) -> Array_type_eff (teff, List.length ct)
        
let rec (const_to_val_eff: Lxm.t -> const -> val_exp) = 
  fun lxm const -> 
    let mk_by_pos_op by_pos_op_eff =
      CallByPosEff(flagit by_pos_op_eff lxm, OperEff [])
    in
    let id_of_int i = Ident.of_string (string_of_int i) in
      match const with
        | Bool_const_eff b -> 
            mk_by_pos_op (Predef((if b then Predef.TRUE_n else Predef.FALSE_n), []))
        | Int_const_eff  i ->
            mk_by_pos_op (Predef((Predef.ICONST_n (id_of_int i)),[]))
        | Real_const_eff r -> 
            mk_by_pos_op (Predef((Predef.RCONST_n (Ident.of_string r)),[]))
        | Enum_const_eff   (s, _)
        | Extern_const_eff (s, _, None) -> mk_by_pos_op (IDENT (Ident.idref_of_long s))
        | Extern_const_eff (s, _, Some c) -> const_to_val_eff lxm c
        | Array_const_eff  (ct, _) -> 
            mk_by_pos_op (ARRAY (List.map (const_to_val_eff lxm) ct))

        | Struct_const_eff (fl, stype) ->
            let sname = match stype with 
              | Struct_type_eff(sname, _) -> sname
              | _ -> assert false
            in
            let pack = Ident.pack_of_long sname in
            let name_op_flg = flagit (STRUCT(pack, Ident.idref_of_long sname)) lxm in
              (CallByNameEff(
                 name_op_flg, 
                 List.map 
                   (fun (id,const) -> flagit id lxm ,const_to_val_eff lxm const) 
                   fl
               ))
                    

        

let (type_of_left: left -> type_) =
  function
    | LeftVarEff (vi,lxm)   -> vi.var_type_eff 
    | LeftFieldEff(_, _, t) -> t 
    | LeftArrayEff(_, _, t) -> t
    | LeftSliceEff(_, _, t) -> t 

 
let rec (var_info_of_left: left -> var_info) =
  function
    | LeftVarEff   (v, _) -> v
    | LeftFieldEff (left,_,_) -> var_info_of_left left
    | LeftArrayEff (left,_,_) -> var_info_of_left left 
    | LeftSliceEff (left,_,_) -> var_info_of_left left

let (clock_of_left: left -> clock) =
  fun left -> 
    snd (var_info_of_left left).var_clock_eff


(*---------------------------------------------------------------------
Une erreur associ�e � un noeud + 1 lexeme dans le fichier source
----------------------------------------------------------------------*)
exception Compile_node_error of node_key * Lxm.t * string
exception Global_node_error of node_key * string