(** Time-stamp: <modified the 19/05/2008 (at 16:44) by Erwan Jahier> *)

(** 

 *)

(*----------------------------------------------------------------------
	module : CompiledData
	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_eff.

	TYPES DE DONNEES :

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

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

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

	- val_eff :
	union entre const_eff et var_info_eff.

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

	- left_eff :
	version compil�e de left_part

	- eq_info_eff :
	version compil�e de eq_info 

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

	- static_arg_eff :
	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_eff : renvoie le type_eff d'une const_eff
	- string_of_type_eff : pretty-print d'un type_eff 
	- string_of_const_eff : pretty-print d'une const_eff 
	- string_of_node_key : pretty-print d'un node_key
	_ string_of_slice_eff :

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

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_eff;
  id2type  : Ident.idref -> Lxm.t -> type_eff;
  id2node  : Ident.idref -> static_arg_eff list -> Lxm.t -> node_exp_eff;
  id2var   : Ident.idref -> Lxm.t -> var_info_eff;
  symbols  : SymbolTab.t;
}

(*---------------------------------------------------------------------
  Type : type_eff
  -----------------------------------------------------------------------
  D�notation de type imm�diat : l'�quivalence s�mantique des types
  EST l'�quivalence structurelle des type_eff. 
  Par rapport � une type_exp :
  - pas d'alias
  - taille des tableaux r�solues
  ----------------------------------------------------------------------*)
and type_eff =
  | Bool_type_eff
  | Int_type_eff
  | Real_type_eff
  | External_type_eff of Ident.long (* XXX nom mal choisi ?? peut-etre Abstract aussi... *)
  | Enum_type_eff     of Ident.long * (Ident.long list)
  | Array_type_eff    of type_eff * int
  | Struct_type_eff   of Ident.long * (Ident.t * (type_eff * const_eff option)) list
      
and slice_info_eff = {
(** 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_eff =
(** 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. 
  (voir type_of_left_eff)

  N.B. On garde aussi l'info source des idents au cas ou.*)
  | LeftVarEff   of (var_info_eff * Lxm.t)
  | LeftFieldEff of (left_eff * Ident.t * type_eff)
  | LeftArrayEff of (left_eff * int * type_eff)
  | LeftSliceEff of (left_eff * slice_info_eff * type_eff)


and eq_info_eff = left_eff list * val_exp_eff

and val_exp_eff =
  | CallByPosEff  of (by_pos_op_eff srcflagged * operands_eff)
  | CallByNameEff of
      (by_name_op_eff srcflagged * (Ident.t srcflagged * val_exp_eff) list)

and operands_eff = OperEff of val_exp_eff list

and by_name_op_eff =
  | STRUCT_eff of Ident.idref
  | STRUCT_anonymous_eff


and by_pos_op_eff =
  | Predef_eff of Predef.op * static_arg_eff list
  | CALL_eff of node_exp_eff srcflagged
  | IDENT_eff  of Ident.idref

  | PRE_eff
  | ARROW_eff
  | FBY_eff
  | CURRENT_eff

  | WHEN_eff
  | TUPLE_eff
  | WITH_eff

  | CONCAT_eff
  | HAT_eff of int * type_eff
  | ARRAY_eff
  | STRUCT_ACCESS_eff of Ident.t

(* those are different from [by_pos_op] *)

  | ARRAY_ACCES_eff of int * type_eff (* index + type of the element *)
  | ARRAY_SLICE_eff of slice_info_eff * type_eff 
  | MERGE_eff       of (Ident.t * (Ident.t list))  
   

(*---------------------------------------------------------------------
  Type : const_eff
  -----------------------------------------------------------------------
  D�notation de constante imm�diate
  N.B. les const_eff "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_eff
  ----------------------------------------------------------------------*)
and const_eff =
    (* type predef *)
    Bool_const_eff of bool
  | Int_const_eff of int
  | Real_const_eff of float
      (* type atomique non predef : on pr�cise le type *)
  | Extern_const_eff of (Ident.long * type_eff)
  | Enum_const_eff   of (Ident.long * type_eff)
      (* type structure : liste (champ,valeur) + type structure *)
  | Struct_const_eff of ((Ident.t * const_eff) list * type_eff)
      (* type tableau : liste des valeurs + type des elts + taille *)
  | Array_const_eff of (const_eff array * type_eff)
      (*---------------------------------------------------------------------
	Type: val_eff	
	-----------------------------------------------------------------------
	Une constante ou une variable
	=> item de la table des symboles de valeurs
	----------------------------------------------------------------------*)
(* and val_eff = *)
(*     ConstEff of const_eff *)
(*   | VarEff of var_info_eff *)
      (*---------------------------------------------------------------------
	Type: var_info_eff	
	-----------------------------------------------------------------------
	Info associ�e � un ident de variable
	----------------------------------------------------------------------*)
      (* ICI � completer/modifier sans doute *)
and var_info_eff = {
  var_name_eff   : Ident.t ;
  var_nature_eff : var_nature ;
  var_type_eff   : type_eff ;
  (*   var_clock_eff  : clock_eff	 *)
}
and clock_eff = (* XXX generalize me!*)
    BaseClockEff
  | VarClockEff of var_info_eff




(**********************************************************************************)
(** [node_exp_eff] 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_eff = {
  node_key_eff : node_key ;
  inlist_eff   : (Ident.t * type_eff) list ;
  outlist_eff  : (Ident.t * type_eff) list ;
  loclist_eff  : (Ident.t * type_eff) list option; (* None => extern or abstract *)
  clock_inlist_eff  : int option list ;
  clock_outlist_eff : int option list ;
  def_eff      : node_def_eff;
  has_mem_eff  : bool;
  is_safe_eff  : bool;
}
and node_def_eff =
  | ExternEff
  | AbstractEff
  | BodyEff of node_body_eff

and node_body_eff = {
  asserts_eff : (val_exp_eff srcflagged) list;
  eqs_eff     : (eq_info_eff srcflagged) list;
}

(* key used  for type, constant, and clock tables *)
and item_key = Ident.long
and node_key = item_key * static_arg_eff list
and static_arg_eff =
  | ConstStaticArgEff of (Ident.t * const_eff)
  | TypeStaticArgEff  of (Ident.t * type_eff)
  | NodeStaticArgEff  of (Ident.t * node_exp_eff)



(****************************************************************************)
(** 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_eff : node_exp_eff -> type_eff list * type_eff list) =
  fun ne -> 
    (snd (List.split ne.inlist_eff), 
     snd (List.split 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_eff check_flag)   Hashtbl.t ; *)
(*   penv_const_table : (Ident.t, const_eff check_flag)  Hashtbl.t ; *)
(*   penv_oper_table  : (Ident.t, node_half_eff) Hashtbl.t ; *)
(*   penv_node_table : (node_key, node_exp_eff 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. But for the time being, we cannot have parametrised nodes
   in argument of parametric node (can we?)
   
   i.e.  
        min_4 = min_n<< 4, toto<<2>> >> ;

   is not allowed (I think). One has to to 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_eff) Hashtbl.t ;
  lenv_const : (Ident.t, const_eff) Hashtbl.t ; 
  lenv_nodes : (Ident.t, node_exp_eff) Hashtbl.t ; 

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


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

let (lookup_node: local_env -> Ident.idref -> static_arg_eff list -> Lxm.t -> 
      node_exp_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_eff) = 
  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_eff) = 
  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

(****************************************************************************)
(** [types_are_compatible t1 t2] checks that t1 is compatible with t2, i.e., 
    if t1 = t2 or t1 is abstract and not t2.
*)
let (types_are_compatible : type_eff -> type_eff -> 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
  
  
(****************************************************************************)
(* Utilitaires li�s aux node_key *)
let (make_simple_node_key : Ident.long -> node_key) =
  fun nkey -> (nkey, [])



let (type_of_const_eff: const_eff -> type_eff) =
  function
    | Bool_const_eff v -> Bool_type_eff
    | Int_const_eff  v -> Int_type_eff
    | Real_const_eff v -> Real_type_eff 
    | Extern_const_eff (s,  teff) -> teff
    | Enum_const_eff   (s,  teff) -> teff
    | Struct_const_eff (fl, teff) -> teff
    | Array_const_eff  (ct, teff) -> Array_type_eff (teff, Array.length ct)
	

let (type_eff_of_left_eff: left_eff -> type_eff) =
  function
    | LeftVarEff (vi_eff,lxm)   -> vi_eff.var_type_eff 
    | LeftFieldEff(_, _, t_eff) -> t_eff 
    | LeftArrayEff(_, _, t_eff) -> t_eff
    | LeftSliceEff(_, _, t_eff) -> t_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