diff --git a/src/Makefile b/src/Makefile
index 19230d7a8943a4c9316fcb0c9f75890769c886bc..64016490ee19df0afde63ed801d4eac038500a9f 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 36b117dcbe2d2e8306427d17d8bee3c257e7e819..5c9413900aba11d5e80f62e891479bd6519c5318 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 51d3f24353d054a2d27116e71cba3305b57dc828..2ddfe2c3a90f03d2a58d9b004db054e02cb308fb 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 5117278ff4e4eeafa23a533f890978fb1fe3dcb5..001d8dd74baa36f29849a74ce9f01817a47a8708 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 2d137e21a98272d7b11d4e88f0bbc3b74ae905e4..05d52074d3f83588090eb07e6a5093b6b4f48709 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 efaf5c240a6002832c39f636371152b4984fa8de..e19b2c891883ac05ff8c27c917c36f565b11e14a 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 e3a3e370067bdfce287f51c5e8f1a0c0dbc09a61..0b1cb90f00f498f05e63e75fd11c69654174569d 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 1c196e4f813050ab8cd7ccbd3ce86e81b3321cb1..dafc587602b5b18fe20cf12dd4b85945d1914f3c 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 0af9947e1589b05327ef372407dbea8e9f1ae9b1..6f88b5ccab610bd65bcc9ddcc8a555d37a7e1daa 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 f24e3d2273ef087cfdb66d6dc046d3d0338b2576..b5c20780ca138109fe4cf9381f3a229a1cbf0011 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 ();