From 57431a16a27447f42aae4b1169da95d135fc1165 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Tue, 11 Mar 2008 16:46:15 +0100
Subject: [PATCH] Simplify the node_eff representation as well as change the
names used in order to make it homogoneous with what is done in
SyntaxTreeCore.ml
This commit is related to the previous one actually.
Also remove all this story of node_half_eff that is not
used (yet), and that may not be useful (we'll see later).
Also continue to fix the representation of SyntaxTrreCore.node_info :
-> remove the node alias
-> put the corresponding infomation in node_body field
-> rename node_body field into node_def
-> associate to node_def (instead of a body option) a new union
type made of Abstract, Extern, Alias of ..., Body of ...
This allows us to
- remove an "assert false" to deal with node with body and alias
(this new presentation makes it impossible)
- Deal with Abstract node properly
---
src/Makefile | 2 +-
src/TODO | 21 ++--
src/compiledData.ml | 244 ++++++++++++++++--------------------------
src/evalNode.ml | 4 +-
src/expandPack.ml | 5 +-
src/lazyCompiler.ml | 187 ++++++++++++++++----------------
src/lazyCompiler.mli | 2 +-
src/parser.mly | 9 +-
src/syntaxTreeCore.ml | 25 +++--
src/syntaxTreeDump.ml | 15 ++-
10 files changed, 225 insertions(+), 289 deletions(-)
diff --git a/src/Makefile b/src/Makefile
index 19230d7a..64016490 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -8,7 +8,6 @@ ifndef SOURCES
SOURCES = \
./version.ml \
./global.ml \
- ./parserUtils.ml \
./verbose.mli \
./verbose.ml \
./ident.mli \
@@ -18,6 +17,7 @@ SOURCES = \
./errors.ml \
./syntaxTreeCore.ml \
./syntaxTree.ml \
+ ./parserUtils.ml \
./parser.mly \
./lexer.mll \
./syntaxTreeDump.mli \
diff --git a/src/TODO b/src/TODO
index 36b117dc..5c941390 100644
--- a/src/TODO
+++ b/src/TODO
@@ -34,21 +34,7 @@ implicite. Autorise-t'on ce genre de truc ?
* verifier que chacun des exemples du repertoire "should_fail" à une
correspondance dans le manuel, et reciproquement...
-* Que ce soit pour les types, les constantes, ou les noeuds, il est
-possible syntaxiquement de ne pas leur donner de definition.
-Pour les noeuds, si cela arrive
- - dans la partie "provide", cela correspond à un item abtrait
- - dans la partie "body", cela correspond à un item externe
-
-pour les types et les constantes, le meme objet syntaxique est généré
-par le parseur (ExternalConst et ExternalType).
-
-Mais pour les noeuds, il y en a 2 : ExtNone et AbstractNode.
-
-Il faudrait faire quelque chose,
- - soit rajouter un AbstractConst et un AbstractType
- - soit merger ExtNone et AbstractNode
***********************************************************************************
*** a faire
@@ -62,7 +48,12 @@ Il faudrait faire quelque chose,
une solution crade serait de faire un coup des sed pour rajouter un
espace devant tous les "..".
-une solution propre serait de ne plus utiliser lex...
+une solution propre serait de ne plus utiliser lex... Une autre
+solution serait de reconstruire la bonne onfo au niveau du yacc. Par
+exemple, si apres un "[", on trouve un reel, on bidouille pour
+generer les lexemes qui vont bien, à savoir :
+
+ tk_real+tk_real -> tk_int+tk_dotdot+tk_int
diff --git a/src/compiledData.ml b/src/compiledData.ml
index 51d3f243..2ddfe2c3 100644
--- a/src/compiledData.ml
+++ b/src/compiledData.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 10/03/2008 (at 17:55) by Erwan Jahier> *)
+(** Time-stamp: <modified the 11/03/2008 (at 16:34) by Erwan Jahier> *)
(**
@@ -34,12 +34,12 @@
construit à partir d'une val_exp => IL S'AGIT DE LA REPRESENTATION
INTERNE DES CONSTANTES STATIQUES
- - var_eff :
+ - var_info_eff :
déclaration de variable,
construit à partir de var_info.
- val_eff :
- union entre const_eff et var_eff.
+ union entre const_eff et var_info_eff.
- slice_eff :
dénotation de tranche de tableau,
@@ -51,25 +51,11 @@
- eq_eff :
version compilée de eq_info
- - ext_node_eff :
- déclaration de fonction chéckée
- (info conservée dans la table des symboles pour résoudre les call)
-
- - node_half_eff : (N.B. utilise dans pack_env)
- déclaration de node/template half-chéckée.
- (info conservée dans la table des symboles pour résoudre les call)
-
- - node_half_eff : (N.B. utilise dans pack_env)
- union de ext_node_eff et node_half_eff.
-
- - node_eff :
+ - node_exp_eff :
dénotation d'opération,
- peut être externe, predef ou utilisateur,
+ peut être predef ou utilisateur,
construit à partir de node_exp.
- - user_node_eff :
- noeud/template + arguments statiques effectifs,
-
- static_arg_eff :
déclaration d'un static arg
@@ -117,7 +103,7 @@ N.B. On fournit les constructeurs des id_solver courants, voir :
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_eff ;
+ id2node : Ident.idref -> static_arg_eff list -> Lxm.t -> node_exp_eff ;
}
(*---------------------------------------------------------------------
@@ -133,10 +119,10 @@ 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
+ | 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
-----------------------------------------------------------------------
@@ -164,7 +150,7 @@ Type : left_eff
N.B. On garde aussi l'info source des idents au cas ou.
----------------------------------------------------------------------*)
and left_eff =
- LeftEffVar of (var_eff * Lxm.t)
+ 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)
@@ -176,7 +162,7 @@ Type : eq_eff
----------------------------------------------------------------------*)
and eq_eff = {
eqf_left_list : left_eff list ;
-(* il manque la partie droite!!! *)
+(* XXX il manque la partie droite!!! *)
}
(*---------------------------------------------------------------------
Type : const_eff
@@ -208,122 +194,84 @@ Type: val_eff
----------------------------------------------------------------------*)
and val_eff =
ConstEff of const_eff
- | VarEff of var_eff
+ | VarEff of var_info_eff
(*---------------------------------------------------------------------
-Type: var_eff
+Type: var_info_eff
-----------------------------------------------------------------------
Info associée à un ident de variable
----------------------------------------------------------------------*)
(* ICI à completer/modifier sans doute *)
-and var_eff = {
- vf_name : Ident.t ;
- vf_nature : var_nature ;
- vf_type : type_eff ;
- vf_clock : clock_eff
+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 =
+and clock_eff = (* XXX generalize me!*)
BaseClockEff
- | VarClockEff of var_eff
-(*---------------------------------------------------------------------
-Type : node_half_eff
------------------------------------------------------------------------
- Union des déclarations de node et de function.
- N.B. dans le cas des fonctions, on a un info complétement chéckée
- (ext_node_eff), par contre pour les nodes on a une info
- à peine chéckée, d'où le nom node_half_eff.
- => item de la table des symboles d'opération
-----------------------------------------------------------------------*)
-and node_half_eff =
- ExtNodeRef of ext_node_eff
- | NodeRef of node_half_eff
-(*---------------------------------------------------------------------
-Type : ext_node_eff
------------------------------------------------------------------------
- Construit à partir de ext_ node_info
-----------------------------------------------------------------------*)
-and ext_node_eff = {
- fe_name : Ident.t;
- fe_in_types : type_eff list;
- fe_out_types : type_eff list;
- fe_has_memory : bool;
-}
-(*---------------------------------------------------------------------
-Type : user_node_half_eff
------------------------------------------------------------------------
- correspond à un noeud half-checked : on conserve simplement
- la node_info (on pourra sophistiquer plus tard)
-----------------------------------------------------------------------*)
-and user_node_half_eff = SyntaxTreeCore.node_info srcflagged
-(*---------------------------------------------------------------------
-Type : user_node_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)
+ | VarClockEff of var_info_eff
+
+
-----------------------------------------------------------------------*)
-and user_node_eff = {
- nf_key : node_key ;
- nf_in_types : type_eff list ;
- nf_out_types : type_eff list ;
- nf_in_formal_clocks : int option list ;
- nf_out_formal_clocks : int option list ;
- nf_asserts : val_eff list;
- nf_eqs : eq_eff list;
- nf_has_memory : bool;
+(**********************************************************************************)
+(** [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;
}
-(*---------------------------------------------------------------------
-Type : XXX_key
------------------------------------------------------------------------
-les clés sont des idents complets en général,
-un peu plus compliqué pour les nodes...
-----------------------------------------------------------------------*)
+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
-
-(*---------------------------------------------------------------------
-Type : static_arg_eff
------------------------------------------------------------------------
- associer à un nom de noeud une liste
- de static_arg_eff permet d'identifier de manière unique une
- instance de template.
- N.B. si la liste d'args est vide, c'est un noeud simple.
-----------------------------------------------------------------------*)
and static_arg_eff =
| ConstStaticArgEff of (Ident.t * const_eff)
| TypeStaticArgEff of (Ident.t * type_eff)
- | NodeStaticArgEff of (Ident.t * node_eff)
-(*---------------------------------------------------------------------
-Type : node_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_eff et user_node_eff
-----------------------------------------------------------------------*)
-and node_eff =
+ 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
- | ExtNodeEff of ext_node_eff
- | UserNodeEff of user_node_eff
+ | NodeEff of node_info_eff
-(*---------------------------------------------------------------------
-Type : node_alias
------------------------------------------------------------------------
- item utilisé pour ``résoudre'' les idents d'operation dans
- local_env : dans un local_env, un identificateur utilisé
- dans une expression "call" peut pointer sur un opérateur
- parfaitement défini (node_eff), ou sur un noeud half_checké
-----------------------------------------------------------------------*)
-and node_alias =
- CheckedNode of node_eff
- | HalfCheckedNode of node_half_eff
+(****************************************************************************)
(** Type check_flag
Au cours du check, on conserve le statut des idents :
@@ -339,13 +287,10 @@ type 'a check_flag =
| Incorrect
-(****************************************************************************)
-let (profile_of_node_eff : node_eff -> type_eff list * type_eff list) =
+let (profile_of_node_exp_eff : node_exp_eff -> type_eff list * type_eff list) =
function
- | PredefEff _ -> assert false (* finish me? *)
- | ExtNodeEff ne -> ne.fe_in_types, ne.fe_out_types
- | UserNodeEff ne -> ne.nf_in_types, ne.nf_out_types
-
+ | PredefEff _ -> assert false (* finish me? *)
+ | NodeEff ne -> (ne.inlist_eff, ne.outlist_eff)
(****************************************************************************)
(* currently not used *)
@@ -363,7 +308,7 @@ let (profile_of_node_eff : node_eff -> type_eff list * type_eff list) =
(* 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_eff check_flag) 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)
@@ -388,7 +333,7 @@ type local_env = {
(* 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_eff) Hashtbl.t ;
+ lenv_nodes : (Ident.t, node_exp_eff) Hashtbl.t ;
}
@@ -397,7 +342,7 @@ let (lookup_type: local_env -> Ident.idref -> Lxm.t -> type_eff) =
Hashtbl.find env.lenv_types (Ident.name_of_idref id)
let (lookup_node: local_env -> Ident.idref -> static_arg_eff list -> Lxm.t ->
- node_eff) =
+ 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) =
@@ -446,7 +391,7 @@ Effets de bord :
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_eff)
+ (i2o : Ident.idref -> static_arg_eff list -> Lxm.t -> node_exp_eff)
=
{
id2const = i2c ;
@@ -490,7 +435,7 @@ Effets de bord :
----------------------------------------------------------------------*)
let type_of_left_eff l =
match l with
- LeftEffVar (v,lxm) -> v.vf_type
+ LeftEffVar (v,lxm) -> v.var_type_eff
| LeftEffField (l, n, te) -> te
| LeftEffArray (l, i, te) -> te
| LeftEffSlice (l, s, te) -> te
@@ -566,10 +511,8 @@ let rec string_of_node_key (nkey: node_key) = (
match opeff with
| PredefEff posop ->
sprintf "operator %s" (SyntaxTreeDump.op2string posop)
- | ExtNodeEff feff ->
- sprintf "extern node %s" (Ident.to_string feff.fe_name)
- | UserNodeEff neff ->
- sprintf "node %s" (string_of_node_key neff.nf_key)
+ | NodeEff neff ->
+ sprintf "node %s" (string_of_node_key neff.node_key_eff)
)
in
match nkey with
@@ -579,35 +522,30 @@ let rec string_of_node_key (nkey: node_key) = (
sprintf "%s<<%s>>" (Ident.string_of_long ik) (String.concat ", " astrings)
)
-let (string_of_user_node_eff: user_node_eff -> string) =
- fun neff ->
- (string_of_node_key neff.nf_key) ^
- "(" ^
- (String.concat ", " (List.map string_of_type_eff neff.nf_in_types)) ^
- ") returns (" ^
- (String.concat ", " (List.map string_of_type_eff neff.nf_out_types)) ^
- ") on clock XXX\n"
-let (string_of_ext_node_eff: ext_node_eff -> string) =
+
+let (string_of_node_info_eff: node_info_eff -> string) =
fun neff ->
- "extern " ^ (Ident.to_string neff.fe_name) ^
+ (string_of_node_key neff.node_key_eff) ^
"(" ^
- (String.concat ", " (List.map string_of_type_eff neff.fe_in_types)) ^
+ (String.concat ", " (List.map string_of_type_eff neff.inlist_eff)) ^
") returns (" ^
- (String.concat ", " (List.map string_of_type_eff neff.fe_out_types)) ^
- ")\n"
+ (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_eff: node_eff -> string) =
+let (string_of_node_exp_eff: node_exp_eff -> string) =
fun neff ->
match neff with
- | PredefEff pn -> SyntaxTreeDump.op2string pn
- | ExtNodeEff eneff -> string_of_ext_node_eff eneff
- | UserNodeEff uneff -> string_of_user_node_eff uneff
+ | 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.vf_name)
+ | VarClockEff veff -> (Ident.to_string veff.var_name_eff)
)
diff --git a/src/evalNode.ml b/src/evalNode.ml
index 5117278f..001d8dd7 100644
--- a/src/evalNode.ml
+++ b/src/evalNode.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 10/03/2008 (at 17:39) by Erwan Jahier> *)
+(** Time-stamp: <modified the 11/03/2008 (at 15:09) by Erwan Jahier> *)
open Lxm
@@ -24,7 +24,7 @@ let (get_static_params_from_idref : SymbolTab.t -> Lxm.t -> Ident.idref ->
let rec (f : CompiledData.id_solver -> SymbolTab.t ->
- SyntaxTreeCore.node_exp srcflagged -> CompiledData.node_eff) =
+ SyntaxTreeCore.node_exp srcflagged -> CompiledData.node_exp_eff) =
fun id_solver symbols { src = lxm; it=(idref, static_args) } ->
let static_params = get_static_params_from_idref symbols lxm idref in
let static_args_eff =
diff --git a/src/expandPack.ml b/src/expandPack.ml
index 2d137e21..05d52074 100644
--- a/src/expandPack.ml
+++ b/src/expandPack.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 10/03/2008 (at 17:35) by Erwan Jahier> *)
+(** Time-stamp: <modified the 11/03/2008 (at 15:48) by Erwan Jahier> *)
open Lxm
open SyntaxTree
@@ -89,8 +89,7 @@ let (doit:
name = s;
static_params = None;
vars = Some (ParserUtils.build_node_var inl outl None);
- alias = Some ne;
- body = None;
+ def = Alias ne;
has_mem = has_memory;
is_safe = true;
}
diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml
index efaf5c24..e19b2c89 100644
--- a/src/lazyCompiler.ml
+++ b/src/lazyCompiler.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 11/03/2008 (at 11:04) by Erwan Jahier> *)
+(** Time-stamp: <modified the 11/03/2008 (at 16:34) by Erwan Jahier> *)
open Lxm
@@ -35,13 +35,13 @@ let recursion_error (lxm : Lxm.t) (stack : string list) =
type t = {
src_tab : SyntaxTab.t;
(* table des defs *)
- types : (item_key, CompiledData.type_eff check_flag) Hashtbl.t;
- consts : (item_key, CompiledData.const_eff check_flag) Hashtbl.t;
- nodes : (node_key, CompiledData.node_eff check_flag) Hashtbl.t;
+ types : (item_key, CompiledData.type_eff check_flag) Hashtbl.t;
+ consts : (item_key, CompiledData.const_eff check_flag) Hashtbl.t;
+ nodes : (node_key, CompiledData.node_exp_eff check_flag) Hashtbl.t;
(* table des prov *)
- prov_types : (item_key, CompiledData.type_eff check_flag) Hashtbl.t;
- prov_consts : (item_key, CompiledData.const_eff check_flag) Hashtbl.t;
- prov_nodes : (node_key, CompiledData.node_eff check_flag) Hashtbl.t
+ prov_types : (item_key, CompiledData.type_eff check_flag) Hashtbl.t;
+ prov_consts : (item_key, CompiledData.const_eff check_flag) Hashtbl.t;
+ prov_nodes : (node_key, CompiledData.node_exp_eff check_flag) Hashtbl.t
}
(******************************************************************************)
@@ -189,9 +189,9 @@ let (lookup_const_eff:(item_key, CompiledData.const_eff check_flag) Hashtbl.t ->
Ident.long -> Lxm.t -> CompiledData.const_eff) =
lookup_x_eff "const ref " (fun k -> k)
-let (lookup_node_eff:
- (CompiledData.node_key, CompiledData.node_eff check_flag) Hashtbl.t ->
- CompiledData.node_key -> Lxm.t -> CompiledData.node_eff) =
+let (lookup_node_exp_eff:
+ (CompiledData.node_key, CompiledData.node_exp_eff check_flag) Hashtbl.t ->
+ CompiledData.node_key -> Lxm.t -> CompiledData.node_exp_eff) =
lookup_x_eff "node ref " (fun k -> fst k)
@@ -457,24 +457,39 @@ and (const_check_do : t -> Ident.long -> Lxm.t -> SymbolTab.t -> Ident.pack_name
and (node_check_interface_do: t -> CompiledData.node_key -> Lxm.t ->
SymbolTab.t -> Ident.pack_name -> SyntaxTreeCore.node_info srcflagged ->
- CompiledData.node_eff) =
+ CompiledData.node_exp_eff) =
fun this nk lxm symbols pack_name node_def ->
- let body_node_eff = node_check this nk lxm in
- let prov_node_eff = node_check_do this nk lxm symbols pack_name node_def in
- if prov_node_eff = body_node_eff then
- prov_node_eff
+ let body_node_exp_eff = node_check this nk lxm in
+ let prov_node_exp_eff = node_check_do this nk lxm symbols pack_name node_def in
+ if
+ match prov_node_exp_eff, body_node_exp_eff with
+ | NodeEff prov_node_exp_eff, NodeEff body_node_exp_eff -> (
+ prov_node_exp_eff.node_key_eff = body_node_exp_eff.node_key_eff &&
+ prov_node_exp_eff.inlist_eff = body_node_exp_eff.inlist_eff &&
+ prov_node_exp_eff.outlist_eff = body_node_exp_eff.outlist_eff &&
+ prov_node_exp_eff.clock_inlist_eff = body_node_exp_eff.clock_inlist_eff &&
+ prov_node_exp_eff.clock_outlist_eff = body_node_exp_eff.clock_outlist_eff &&
+ prov_node_exp_eff.has_mem_eff = body_node_exp_eff.has_mem_eff &&
+ prov_node_exp_eff.is_safe_eff = body_node_exp_eff.is_safe_eff &&
+ match prov_node_exp_eff.def_eff, body_node_exp_eff.def_eff with
+ | (AbstractEff,_) -> true
+ | (_,_) -> prov_node_exp_eff.def_eff = body_node_exp_eff.def_eff
+ )
+ | _,_ -> assert false
+ then
+ prov_node_exp_eff
else
- raise(Compile_error (
- node_def.src,
- ("provided node \n\t" ^
- (string_of_node_eff prov_node_eff) ^
- "\n is not compatible with its implementation \n\t" ^
- (string_of_node_eff body_node_eff))))
+ raise(
+ Compile_error (
+ node_def.src,
+ ("provided node \n\t" ^ (string_of_node_exp_eff prov_node_exp_eff) ^
+ "\n is not compatible with its implementation \n\t" ^
+ (string_of_node_exp_eff body_node_exp_eff))))
and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t ->
Ident.pack_name -> SyntaxTreeCore.node_info srcflagged ->
- CompiledData.node_eff) =
+ CompiledData.node_exp_eff) =
fun this nk lxm symbols pack_name node_def ->
(*
- verifier les params statiques ?
@@ -504,17 +519,44 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t ->
with Not_found -> solve_node_idref this symbols pack_name id sargs lxm);
}
in
- match node_def.it.body, node_def.it.alias with
- | None, None -> (
- (* bodyless node that are not alias are abstract or extern;
- they may have a profile
-
- XXX do we compile in the same way ?
- XXX add a flag or something to distinguish extern and abstract nodes?
- *)
+ let make_node_eff node_def_eff =
+ (* building abstract and normal (i.e., with body) nodes *)
+ match node_def.it.vars with
+ | None -> assert false (* a node with a body should have a profile *)
+ | Some vars ->
+ let type_args id =
+ let vi = Hashtbl.find vars.vartable id in
+ EvalType.f node_id_solver vi.it.var_type
+ in
+ let (type_eq : eq_info srcflagged -> eq_eff) =
+ fun eq_info ->
+ finish_me "with with body compilation"; assert false
+ in
+ NodeEff {
+ node_key_eff = nk ;
+ inlist_eff = List.map type_args vars.inlist ;
+ outlist_eff = List.map type_args vars.outlist;
+ clock_inlist_eff = [];(* XXX finish me! *)
+ clock_outlist_eff = [];(* XXX finish me! *)
+ def_eff = node_def_eff;
+ has_mem_eff = node_def.it.has_mem;
+ is_safe_eff = node_def.it.is_safe;
+ }
+ in
+ match node_def.it.def with
+ | Abstract ->
+ make_node_eff AbstractEff
+ | Body nb ->
+ make_node_eff (
+ BodyEff {
+ asserts_eff = []; (* XXX finish me! *)
+ eqs_eff = []; (* List.map type_eq nb.eqs; *)
+ }
+ )
+ | Extern -> (
match node_def.it.vars with
| None ->
- finish_me " abstract or extern node without profile";
+ finish_me "extern node without profile";
assert false
| Some vars ->
let vi_il, vi_ol =
@@ -526,42 +568,32 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t ->
let vi = Hashtbl.find vars.vartable id in
EvalType.f node_id_solver vi.it.var_type
in
-(* make_user_node_eff *)
-(* (List.map aux vi_il) *)
-(* (List.map aux vi_ol) *)
-(* node_def.it.has_mem; *)
-
-
-(* ExtNodeEff { *)
-(* fe_name = en.eni_name; *)
-(* fe_in_types =(List.map type_args en.eni_inputs); *)
-(* fe_out_types = (List.map type_args en.eni_outputs); *)
-(* fe_has_memory = en.eni_has_mem; *)
-(* } *)
-
- UserNodeEff {
- nf_key = nk;
- nf_in_types = List.map type_args vars.inlist;
- nf_out_types = List.map type_args vars.outlist;
- nf_in_formal_clocks = []; (* XXX finish me! *)
- nf_out_formal_clocks = []; (* XXX finish me! *)
- nf_asserts = []; (* XXX finish me! *)
- nf_eqs = []; (* List.map type_eq nb.eqs; *)
- nf_has_memory = node_def.it.has_mem;
+ NodeEff {
+ node_key_eff = nk ;
+ inlist_eff = List.map type_args vars.inlist ;
+ outlist_eff = List.map type_args vars.outlist;
+ clock_inlist_eff = [];(* XXX finish me! *)
+ clock_outlist_eff = [];(* XXX finish me! *)
+ def_eff = ExternEff;
+ has_mem_eff = node_def.it.has_mem;
+ is_safe_eff = node_def.it.is_safe;
}
)
- | None, Some node_alias -> (
+
+
+
+ | Alias node_alias -> (
+ (* just check that the declared profile (if any) matches with the alias *)
let res = EvalNode.f node_id_solver symbols node_alias in
match node_def.it.vars with
| None -> res
- | Some vars ->
- (* check that the declared profile matched with the result *)
+ | Some vars ->
let vi_il, vi_ol =
List.map (fun id -> Hashtbl.find vars.vartable id) vars.inlist,
List.map (fun id -> Hashtbl.find vars.vartable id) vars.outlist
in
let aux vi = EvalType.f node_id_solver vi.it.var_type in
- let (il,ol) = CompiledData.profile_of_node_eff res in
+ let (il,ol) = CompiledData.profile_of_node_exp_eff res in
if
List.map aux vi_il <> il
|| List.map aux vi_ol <> ol
@@ -571,37 +603,12 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t ->
(* that error msg could be more precise *)
else
res
- )
- | Some _, Some _ -> assert false
- (* we cannot have a body and an alias...*)
-
- | Some nb, None -> (
- match node_def.it.vars with
- | None -> assert false (* a node with a body have a profile *)
- | Some vars ->
- let type_args id =
- let vi = Hashtbl.find vars.vartable id in
- EvalType.f node_id_solver vi.it.var_type
- in
- let (type_eq : eq_info srcflagged -> eq_eff) =
- fun eq_info ->
- finish_me "with with body compilation"; assert false
- in
- UserNodeEff {
- nf_key = nk;
- nf_in_types = List.map type_args vars.inlist;
- nf_out_types = List.map type_args vars.outlist;
- nf_in_formal_clocks = []; (* XXX finish me! *)
- nf_out_formal_clocks = []; (* XXX finish me! *)
- nf_asserts = []; (* XXX finish me! *)
- nf_eqs = []; (* List.map type_eq nb.eqs; *)
- nf_has_memory = node_def.it.has_mem;
- }
- )
+ )
+
(** builds and node_key and calls [node_check] *)
and (solve_node_idref : t -> SymbolTab.t -> Ident.pack_name -> Ident.idref ->
- static_arg_eff list -> Lxm.t -> CompiledData.node_eff) =
+ static_arg_eff list -> Lxm.t -> CompiledData.node_exp_eff) =
fun this symbols currpack idr sargs lxm ->
solve_x_idref
node_check_interface node_check SymbolTab.find_node "node"
@@ -614,18 +621,18 @@ and (solve_node_idref : t -> SymbolTab.t -> Ident.pack_name -> Ident.idref ->
)
this symbols currpack idr sargs lxm
-and (node_check: t -> CompiledData.node_key -> Lxm.t -> CompiledData.node_eff) =
+and (node_check: t -> CompiledData.node_key -> Lxm.t -> CompiledData.node_exp_eff) =
fun this nk ->
- x_check this.nodes SymbolTab.find_node node_check_do lookup_node_eff
+ x_check this.nodes SymbolTab.find_node node_check_do lookup_node_exp_eff
(fun nk -> Ident.pack_of_long (fst nk))
(fun nk -> Ident.of_long (fst nk))
this nk
and (node_check_interface:
- t -> CompiledData.node_key -> Lxm.t -> CompiledData.node_eff) =
+ t -> CompiledData.node_key -> Lxm.t -> CompiledData.node_exp_eff) =
fun this nk ->
x_check_interface this.prov_nodes SymbolTab.find_node node_check
- node_check_interface_do lookup_node_eff
+ node_check_interface_do lookup_node_exp_eff
(fun nk -> Ident.pack_of_long (fst nk))
(fun nk -> Ident.of_long (fst nk)) this nk
@@ -679,7 +686,7 @@ let test_nodes pack_name this id ni_f =
flush stdout
| None ->
test_item this "node" node_check_interface CompiledData.string_of_node_key
- string_of_node_eff (fun id -> (Ident.make_long pack_name id, [])) id ni_f
+ string_of_node_exp_eff (fun id -> (Ident.make_long pack_name id, [])) id ni_f
let test (this: t) = (
diff --git a/src/lazyCompiler.mli b/src/lazyCompiler.mli
index e3a3e370..0b1cb90f 100644
--- a/src/lazyCompiler.mli
+++ b/src/lazyCompiler.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 14/02/2008 (at 17:08) by Erwan Jahier> *)
+(** Time-stamp: <modified the 11/03/2008 (at 16:28) by Erwan Jahier> *)
(** nb: compiling = type checking + constant evaluation *)
diff --git a/src/parser.mly b/src/parser.mly
index 1c196e4f..dafc5876 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -224,8 +224,7 @@ let (treat_node_decl : bool -> Lxm.t -> static_param srcflagged list ->
name = nstr;
static_params = Some statics;
vars = Some vars;
- alias = None;
- body = Some { asserts = asserts ; eqs = eqs };
+ def = Body { asserts = asserts ; eqs = eqs };
has_mem = has_memory;
is_safe = true;
}
@@ -249,8 +248,7 @@ let (treat_node_alias : bool -> Lxm.t -> static_param srcflagged list ->
name = nstr;
static_params = Some statics;
vars = vars;
- alias = Some value;
- body = None;
+ def = Alias value;
has_mem = has_memory;
is_safe = true;
}
@@ -274,8 +272,7 @@ let treat_abstract_node_do (* cf the profile of [treat_abstract_node] *)
name = Lxm.id lxm;
static_params = None;
vars = Some vars;
- alias = None;
- body = None;
+ def = Abstract;
has_mem = has_memory;
is_safe = true;
}
diff --git a/src/syntaxTreeCore.ml b/src/syntaxTreeCore.ml
index 0af9947e..6f88b5cc 100644
--- a/src/syntaxTreeCore.ml
+++ b/src/syntaxTreeCore.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 11/03/2008 (at 11:41) by Erwan Jahier> *)
+(** Time-stamp: <modified the 11/03/2008 (at 15:44) by Erwan Jahier> *)
(** (Raw) Abstract syntax tree of source programs. *)
@@ -27,8 +27,7 @@ and node_info = {
name : Ident.t;
static_params : static_param srcflagged list option;
vars : node_vars option; (* aliased node may have no i/o decl *)
- alias : node_exp srcflagged option;
- body : node_body option;
+ def : node_def;
has_mem : bool;
is_safe : bool;
}
@@ -57,6 +56,12 @@ and var_nature =
| VarOutput
| VarLocal
+and node_def =
+ | Extern
+ | Abstract
+ | Body of node_body
+ | Alias of node_exp srcflagged
+
and node_body = {
asserts : (val_exp srcflagged) list;
eqs : (eq_info srcflagged) list;
@@ -168,13 +173,13 @@ and by_name_op =
and node_exp =
(Ident.idref * (static_arg srcflagged list))
- (*
- Params statiques effectifs :
- - val_exp (pour les constantes)
- - type_exp (pour les types)
- - node_exp (pour les node)
- - ident : a résoudre, peut etre const, type ou node
- *)
+
+(** Params statiques effectifs :
+ - val_exp (pour les constantes)
+ - type_exp (pour les types)
+ - node_exp (pour les node)
+ - ident : a résoudre, peut etre const, type ou node
+*)
and static_arg =
| StaticArgIdent of Ident.idref
| StaticArgConst of val_exp
diff --git a/src/syntaxTreeDump.ml b/src/syntaxTreeDump.ml
index f24e3d22..b5c20780 100644
--- a/src/syntaxTreeDump.ml
+++ b/src/syntaxTreeDump.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 10/03/2008 (at 17:06) by Erwan Jahier> *)
+(** Time-stamp: <modified the 11/03/2008 (at 15:48) by Erwan Jahier> *)
open Lxm
@@ -271,13 +271,12 @@ and dump_node (os: Format.formatter) (x: node_info srcflagged) = (
fprintf os "@[<b 3> %a;@]@\n" dump_var_decl_list loclst;
);
- (match ninfo.alias with
- | None -> ()
- | Some {it = nexp; src = lxm} -> fprintf os " = @,%a;@\n" dump_node_exp nexp
- );
- (match ninfo.body with
- | None -> ()
- | Some body -> dump_node_body os body
+ (match ninfo.def with
+ | Extern -> fprintf os "extern"
+ | Abstract -> fprintf os "abstract"
+ | Body body -> dump_node_body os body
+ | Alias {it = nexp; src = lxm} -> fprintf os " = @,%a;@\n" dump_node_exp nexp
+
);
if ninfo.has_mem then () else ();
if ninfo.is_safe then () else ();
--
GitLab