(** Time-stamp: <modified the 01/06/2011 (at 13:21) 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 Errors
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 types.
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
| Abstract_type_eff of Ident.long * type_
| 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] *)
(* Utile : arguments et profils *)
and node_profile = (Ident.t * type_) list * (Ident.t * type_) list
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 =
{ core : val_exp_core ;
typ : type_ list ;
(* An empty list means that its type has not been computed (EvalType.f) yet.
a cleaner solution would be to define two versions of val_exp: one with
type info, and one without. But it is a big mutually recursive thing,
and doing that would be a little bit heavy...
*)
clk : clock list
(* ditto *)
}
and val_exp_core =
| 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... *)
| 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
(* those are different from [by_pos_op] *)
| ARRAY_ACCES of int
| ARRAY_SLICE of slice_info
| 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_)
| Abstract_const_eff of (Ident.long * type_ * const * bool)
(* if the abstract const is exported (i.e., defined in the provided part),
then the bool flag is set to true. Well, it is not really an abstract
constant in that case...
nb: well, are exported abstract constant useful at all? I don't
know, but it is not a reason to handle them unproperly...
*)
| 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_)
| Tuple_const_eff of const list
(*---------------------------------------------------------------------
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 of node_exp option (* None if extern in the provide part *)
| 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 =
(* may be a tuple *)
| ConstStaticArgEff of (Ident.t * const)
| TypeStaticArgEff of (Ident.t * type_)
| NodeStaticArgEff of (Ident.t * sarg_node_eff * node_exp)
and sarg_node_eff = node_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 ;
}
(* Just to group those 3 ones *)
type node_env = {
local : local_env;
global: id_solver;
}
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
| Abstract_type_eff _, _ -> true
| Any, _ -> true
| _, Any -> true
| Overload, Real_type_eff | Real_type_eff, Overload
| Overload, Int_type_eff | Int_type_eff, Overload -> 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))
let ident_of_type = function
| Bool_type_eff -> Ident.out_of_pack "bool"
| Int_type_eff -> Ident.out_of_pack "int"
| Real_type_eff -> Ident.out_of_pack "real"
| External_type_eff id
| Abstract_type_eff (id, _)
| Enum_type_eff (id, _)
| Struct_type_eff (id, _) -> id
| Any -> Ident.out_of_pack "any"
| Overload -> Ident.out_of_pack "anynum"
| _ -> assert false
(****************************************************************************)
(* 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)
| Abstract_type_eff(l,t) -> Abstract_type_eff(l,t)
| 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 _
| Abstract_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
(* Ne doit �tre appel�e que pour les constantes simple
*)
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) -> teff
| Abstract_const_eff (s, teff, _v, _is_exported) -> 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)
| Tuple_const_eff cl ->
print_internal_error "Eff.type_of_const" "should not have been called for a tuple";
assert false
(* accepte un UNIQUE niveau de tuple
*)
let (types_of_const: const -> type_ list) =
function
| Tuple_const_eff cl -> List.map type_of_const cl
| c -> [type_of_const c]
(* const list *)
(* Ignore the abstraction layer (necessary when expanding struct) *)
(* XXX not used anymore. This is very suspect... *)
let (true_type_of_const: const -> type_) =
function
| Abstract_const_eff (s, teff, _v, _is_exported) -> teff
| teff -> type_of_const teff
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
(* RIEN A FAIRE ICI ??
let find_var_info lxm vars id =
try Hashtbl.find vars.SyntaxTreeCore.vartable id
with Not_found ->
raise (Errors.Compile_error (lxm,"\n*** Unknown ident: " ^ (Ident.to_string id)))
*)
(*---------------------------------------------------------------------
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