compiledData.ml

(** Time-stamp: <modified the 11/03/2008 (at 16:34) 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_eff :
	dénotation de tranche de tableau,
	construit à partir de slice_info.

	- left_eff :
	version compilée de left_part

	- eq_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 :
	const_and_type_id_solver
----------------------------------------------------------------------*)
type id_solver = {
  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 ;
}

(*---------------------------------------------------------------------
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
  | 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
(*---------------------------------------------------------------------
Type : slice_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
----------------------------------------------------------------------*)
and slice_eff = {
  se_first : int;
  se_last : int;
  se_step : int;
  se_width : int
}
(*---------------------------------------------------------------------
Type : 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.
----------------------------------------------------------------------*)
and left_eff =
    LeftEffVar of (var_info_eff * Lxm.t)
  | LeftEffField of (left_eff * Ident.t * type_eff)
  | LeftEffArray of (left_eff * int * type_eff)
  | LeftEffSlice of (left_eff * slice_eff * type_eff)
(*---------------------------------------------------------------------
Type : eq_eff
-----------------------------------------------------------------------
	Version checkée des eq_info 
	N.B. A COMPLETER SANS DOUTE
----------------------------------------------------------------------*)
and eq_eff = {
  eqf_left_list : left_eff list ;
(* XXX il manque la partie droite!!! *)
}
(*---------------------------------------------------------------------
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_info_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_info_eff = {
  node_key_eff : node_key ;
  inlist_eff   : type_eff list ;
  outlist_eff  : type_eff list ;
  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_eff list;
  eqs_eff     : eq_eff 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)

(** [node_exp_eff]

	Version chéckée des node_exp (expression dénotant une opération).
	Utilisée dans les expressions call, mais aussi comme argument statique
	ou comme définition de noeud (alias). 
	Union entre opérateur prédéfini, user_ext_node_exp_eff et user_node_exp_eff
*)
and node_exp_eff = 
(* XXX faire sauter ce niveau egalement ???? 
   ce serait cool. Mais ca necessite d'etre capable de produire un 
   node_info_eff à chacun des operateurs predefinis.

   Sans la surcharge de + (and friends), ce serait finger in the nose...
*)
  | PredefEff of by_pos_op 
  | NodeEff of node_info_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) =
  function
    | PredefEff _ -> assert false (* finish me? *)
    | NodeEff  ne -> (ne.inlist_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_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_vals  : (Ident.t, val_eff) Hashtbl.t ; 
  lenv_nodes : (Ident.t, node_exp_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 ->  
    match Hashtbl.find env.lenv_vals (Ident.name_of_idref id) with
      | ConstEff ceff -> ceff
      | VarEff _ -> raise Not_found (* should I raise a error there ? *)
	  
let (make_local_env : node_key -> local_env) =
  fun nk ->
    let res =
      {
	lenv_node_key = nk;
	lenv_types = Hashtbl.create 0;
	lenv_vals  = Hashtbl.create 0;
	lenv_nodes = Hashtbl.create 0;
      }
    in
      List.iter
	(function
	   | ConstStaticArgEff(id,ce) -> Hashtbl.add res.lenv_vals id (ConstEff ce)
	   | TypeStaticArgEff(id,te)  -> Hashtbl.add res.lenv_types id te
	   | NodeStaticArgEff(id, ne) -> Hashtbl.add res.lenv_nodes id ne
	)
	(snd nk);
      res

(****************************************************************************)
(* Utilitaires liés aux node_key *)
let (make_simple_node_key : Ident.long -> node_key) =
  fun nkey -> (nkey, [])


(*---------------------------------------------------------------------
Utilitaire: const_and_type_id_solver 
-----------------------------------------------------------------------
Rôle :
	comme son nom l'indique
Entrées :
	id2const, id2type, id2node
Sorties :
	id_solver
Effets de bord :
	aucun. mais peut générer des Internal à l'usage !
---------------------------------------------------------------------*)
let const_and_type_id_solver
    (i2c : Ident.idref -> Lxm.t -> const_eff)
    (i2t : Ident.idref -> Lxm.t -> type_eff)
    (i2o : Ident.idref -> static_arg_eff list -> Lxm.t -> node_exp_eff)
    = 
  {
    id2const = i2c ;
    id2type  = i2t ;
    id2node  = i2o ;
  }

(*---------------------------------------------------------------------
Utilitaire: type_of_const_eff
-----------------------------------------------------------------------
Rôle :
	comme son nom l'indique
Entrées :
	const_eff
Sorties :
	type_eff
Effets de bord :
	aucun
----------------------------------------------------------------------*)
let type_of_const_eff c =
match c with
    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)

(*---------------------------------------------------------------------
Utilitaire: type_of_left_eff
-----------------------------------------------------------------------
Rôle :
	comme son nom l'indique
Entrées :
	left_eff
Sorties :
	type_eff
Effets de bord :
	aucun
----------------------------------------------------------------------*)
let type_of_left_eff l =
match l with
    LeftEffVar (v,lxm) -> v.var_type_eff
  | LeftEffField (l, n, te) -> te
  | LeftEffArray (l, i, te) -> te
  | LeftEffSlice (l, s, te) -> te

(*---------------------------------------------------------------------
Utilitaire: string_of_type_eff
-----------------------------------------------------------------------
Rôle :
	affichage d'une valeur de type (pour debug)
Entrées :
	type_eff
Sorties :
	string
Effets de bord :
----------------------------------------------------------------------*)

let rec string_of_const_eff = (
  function
      Bool_const_eff true -> "true"
    | Bool_const_eff false -> "false"
    | Int_const_eff i -> sprintf "%d" i
    | Real_const_eff r -> sprintf "%f" r
    | Extern_const_eff (s,t) -> (Ident.string_of_long s)
    | Enum_const_eff   (s,t) -> (Ident.string_of_long s)
    | Struct_const_eff (fl, t) -> (
	let string_of_field = 
	  function (id, veff) -> 
	    (Ident.to_string id)^" = "^(string_of_const_eff veff)
	in
	let flst = List.map string_of_field fl in
	  (string_of_type_eff t)^"{"^(String.concat "; " flst)^"}"
      )
    | Array_const_eff (ctab, t) -> (
	let vl = Array.to_list(Array.map string_of_const_eff ctab) in
	  "["^(String.concat ", " vl)^"]"
      )
)

and string_of_type_eff = function
    Bool_type_eff -> "bool"
  | Int_type_eff  -> "int"
  | Real_type_eff -> "real"
  | External_type_eff i -> Ident.string_of_long i
  | Enum_type_eff (i, sl) -> 
      assert (sl <>[]);
      let f sep acc s  = acc ^ sep ^ (Ident.string_of_long s) in
	(List.fold_left (f ", ")  (f "" "enum {" (List.hd sl)) (List.tl sl)) ^ "}"
  | Array_type_eff (ty, sz) -> sprintf "%s^%d" (string_of_type_eff ty) sz
  | Struct_type_eff (i, fl) -> 
      assert (fl <>[]);
      let f sep acc (id, type_eff, const_eff_opt)  = 
	acc ^ sep ^ (Ident.to_string id) ^ " : " ^
	  (string_of_type_eff type_eff) ^
	  match const_eff_opt with
	      None -> ""
	    | Some ce -> " (" ^ (string_of_const_eff ce) ^ ")"
      in
	(List.fold_left (f "; ")  (f "" " {" (List.hd fl)) (List.tl fl)) ^ "}"
	
and string_of_type_eff_list = function
    []  -> ""
  | [x] -> (string_of_type_eff x)
  | l   -> (String.concat " * " (List.map string_of_type_eff l)
)


let rec string_of_node_key (nkey: node_key) = (
  let arg2string (sa : static_arg_eff) =
    match sa with
      | ConstStaticArgEff (id, ceff) -> sprintf "const %s" (string_of_const_eff ceff)
      | TypeStaticArgEff  (id, teff) -> sprintf "type %s" (string_of_type_eff teff)
      | NodeStaticArgEff  (id, opeff) -> (
	  match opeff with
	    | PredefEff posop -> 
		sprintf "operator %s" (SyntaxTreeDump.op2string posop)
	    | NodeEff neff -> 
		sprintf "node %s" (string_of_node_key neff.node_key_eff)
	) 
  in
    match nkey with
      | (ik, []) -> Ident.string_of_long ik
      | (ik, salst) ->
	  let astrings = List.map arg2string salst in
	    sprintf "%s<<%s>>" (Ident.string_of_long ik) (String.concat ", " astrings)
)



let (string_of_node_info_eff: node_info_eff -> string) =
  fun neff -> 
    (string_of_node_key neff.node_key_eff) ^ 
      "(" ^
      (String.concat ", " (List.map string_of_type_eff neff.inlist_eff)) ^
      ") returns (" ^
      (String.concat ", " (List.map string_of_type_eff neff.outlist_eff)) ^
      ") on clock XXX" ^
(*       (if neff.body_eff = None then "<abstract or extern>" else "< ... a body ...>" ) ^ *)
      "\n"


let (string_of_node_exp_eff: node_exp_eff -> string) =
  fun neff -> 
    match neff with
      | PredefEff pn -> SyntaxTreeDump.op2string pn
      | NodeEff neff -> string_of_node_info_eff neff

let string_of_clock (ck : clock_eff) = (
  match ck with
      BaseClockEff -> "<base>"
   |  VarClockEff veff -> (Ident.to_string veff.var_name_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

(*---------------------------------------------------------------------
Formatage standard des erreurs de compil
----------------------------------------------------------------------*)
let node_error_string nkey = (
   Printf.sprintf "While checking %s" (string_of_node_key nkey)
)

(*---------------------------------------------------------------------
Message d'erreur (associé à un lexeme) sur stderr
----------------------------------------------------------------------*)
let print_compile_node_error nkey lxm msg = (
   Printf.eprintf "%s\n" (node_error_string nkey);
  Errors.print_compile_error lxm msg ;
   flush stderr
)

let print_global_node_error nkey msg = (
   Printf.eprintf "%s\n" (node_error_string nkey);
  Errors.print_global_error msg ;
   flush stderr
)