-
Erwan Jahier authoredErwan Jahier authored
eff.ml 15.26 KiB
(** Time-stamp: <modified the 02/09/2008 (at 11:12) 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 val_exp
| TUPLE
| WITH of val_exp
| CONCAT
| HAT of int * val_exp
| ARRAY
| STRUCT_ACCESS of Ident.t
(* 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
| Real_const_eff of float
(* 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 array * 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 : clock;
}
and clock =
| BaseEff (* it's not bezef... *)
| On of Ident.t * clock
| ClockVar of int (* to deal with polymorphic clocks (i.e., constants) *)
(**********************************************************************************)
(** [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;
lxm : Lxm.t;
}
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 * node_exp)
(****************************************************************************)
(** 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. 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_) Hashtbl.t ;
lenv_const : (Ident.t, const) Hashtbl.t ;
lenv_nodes : (Ident.t, node_exp) 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 ->
node_exp) =
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(_,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 v1.var_clock_eff 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 (type_of_const: const -> type_) =
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, vopt) -> 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_of_left: left -> type_) =
function
| LeftVarEff (vi,lxm) -> vi.var_type_eff
| LeftFieldEff(_, _, t) -> t
| LeftArrayEff(_, _, t) -> t
| LeftSliceEff(_, _, t) -> t
let rec (clock_of_left: left -> clock) =
function
| LeftVarEff (var_info, _) -> var_info.var_clock_eff
| LeftFieldEff (left,_,_) -> clock_of_left left
| LeftArrayEff (left,_,_) -> clock_of_left left
| LeftSliceEff (left,_,_) -> clock_of_left left
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
(*---------------------------------------------------------------------
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