diff --git a/src/eff.ml b/src/eff.ml
index b0e249cebe75361ed53123e135067cd3920c76ac..c567b693a5a1a211ad99880993d7779723b7c18a 100644
--- a/src/eff.ml
+++ b/src/eff.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 11/03/2009 (at 17:36) by Erwan Jahier> *)
+(** Time-stamp: <modified the 12/03/2009 (at 09:54) by Erwan Jahier> *)
(**
@@ -301,7 +301,7 @@ and node_exp = {
and node_def =
| ExternEff
- | AbstractEff
+ | AbstractEff of node_exp option (* None if extern in the provide part *)
| BodyEff of node_body
and node_body = {
diff --git a/src/getEff.mli b/src/getEff.mli
index 5aeb309fadf3cf790f94eac8d7117cbcc76168ca..b396988b2260fb99529d0607065a2e9864457c43 100644
--- a/src/getEff.mli
+++ b/src/getEff.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 03/03/2009 (at 17:22) by Erwan Jahier> *)
+(** Time-stamp: <modified the 12/03/2009 (at 09:17) by Erwan Jahier> *)
(** This module defines functions that translate SyntaxTreeCore datatypes into
diff --git a/src/inline.ml b/src/inline.ml
index 5ec0f5e0d8bb40011977267f94721dd3798de185..e46b0414ce88d828826ce27745d148aa909b29bf 100644
--- a/src/inline.ml
+++ b/src/inline.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 11/03/2009 (at 17:35) by Erwan Jahier> *)
+(** Time-stamp: <modified the 12/03/2009 (at 10:23) by Erwan Jahier> *)
open Lxm
@@ -427,7 +427,9 @@ and (iterators : Eff.local_env -> Eff.id_solver -> Eff.node_exp -> Eff.node_exp)
fun node_env id_solver n ->
match n.def_eff with
| ExternEff
- | AbstractEff -> n
+ | AbstractEff None -> n
+ | AbstractEff (Some pn) ->
+ { n with def_eff = AbstractEff (Some (iterators node_env id_solver pn)) }
| BodyEff b ->
Name.reset_local_var_prefix "acc";
Name.reset_local_var_prefix "cpt";
diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml
index 37f9b6b1b217ef1484fad162267bb92971da15f9..fd73920da5a7448538dd622f01e500052440ec0e 100644
--- a/src/lazyCompiler.ml
+++ b/src/lazyCompiler.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 11/03/2009 (at 16:01) by Erwan Jahier> *)
+(** Time-stamp: <modified the 12/03/2009 (at 09:55) by Erwan Jahier> *)
open Lxm
@@ -643,12 +643,16 @@ and (node_check_interface_do: t -> Eff.node_key -> Lxm.t ->
raise(Compile_error (node_def.src, msg_prefix ^ "safe or unsafe?"))
else if
match prov_node_exp_eff.def_eff, body_node_exp_eff.def_eff with
- | (AbstractEff,_) -> false
+ | (AbstractEff _,_) -> false
| (_,_) -> prov_node_exp_eff.def_eff <> body_node_exp_eff.def_eff
then
raise(Compile_error (node_def.src, msg_prefix ^ "abstract or not?"))
else
- prov_node_exp_eff
+ match prov_node_exp_eff.def_eff, body_node_exp_eff.def_eff with
+ | AbstractEff None, BodyEff node_body ->
+ { prov_node_exp_eff with def_eff = AbstractEff (Some body_node_exp_eff) }
+ | _,_ ->
+ prov_node_exp_eff
and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t ->
bool -> Ident.pack_name -> SyntaxTreeCore.node_info srcflagged ->
@@ -890,7 +894,7 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t ->
(* let's go *)
let res =
match node_def.it.def with
- | Abstract -> make_node_eff (fun () -> AbstractEff)
+ | Abstract -> make_node_eff (fun () -> AbstractEff None)
| Extern -> make_node_eff (fun () -> ExternEff)
| Body nb ->
make_node_eff (
@@ -981,7 +985,7 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t ->
(* if no main node is provided, we take the first node we find,
that has a non-empty body. *)
match res.def_eff with
- | ExternEff | AbstractEff -> false
+ | ExternEff | AbstractEff _ -> false
| BodyEff _ ->
Global.main_node := Ident.string_of_long (fst nk);
true
diff --git a/src/licDump.ml b/src/licDump.ml
index c5ffcc00a94b3a5844a2a6a7c4c179b1d663a50d..4701189386a39565a45b5228e8a88f9fa88be44d 100644
--- a/src/licDump.ml
+++ b/src/licDump.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 11/03/2009 (at 17:42) by Erwan Jahier> *)
+(** Time-stamp: <modified the 12/03/2009 (at 09:41) by Erwan Jahier> *)
open Printf
open Lxm
@@ -536,7 +536,7 @@ and (profile_of_node_exp_eff: Eff.node_exp -> string) =
and (string_of_node_def : Eff.node_def -> string list) =
function
| ExternEff
- | AbstractEff -> []
+ | AbstractEff _ -> []
| BodyEff node_body_eff ->
List.append
(List.map string_of_assert node_body_eff.asserts_eff)
@@ -598,7 +598,7 @@ and (node_of_node_exp_eff: Eff.node_exp -> string) =
(profile_of_node_exp_eff neff)) ^
(match neff.def_eff with
| ExternEff -> ""
- | AbstractEff -> ""
+ | AbstractEff _ -> ""
| BodyEff _ ->
((match neff.loclist_eff with None -> "" | Some [] -> ""
| Some l ->
diff --git a/src/nodesExpand.ml b/src/nodesExpand.ml
index ed69ae7230bccce3bf65ce560215cd31af9b41ae..a1e112269f6d753efe083a42700e2a9651b01cce 100644
--- a/src/nodesExpand.ml
+++ b/src/nodesExpand.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 11/03/2009 (at 16:41) by Erwan Jahier> *)
+(** Time-stamp: <modified the 12/03/2009 (at 10:43) by Erwan Jahier> *)
(**
nb : only user nodes are expanded.
@@ -93,18 +93,19 @@ let new_var str node_env type_eff clock_eff =
var
(********************************************************************************)
-let get_locals node =
+let get_locals node =
match node.loclist_eff with
| None -> []
| Some l -> l
-let (get_node_body : Eff.local_env -> Eff.node_exp -> Eff.node_body option) =
+let rec (get_node_body : Eff.local_env -> Eff.node_exp -> Eff.node_body option) =
fun node_env node ->
match node.def_eff with
| ExternEff
- | AbstractEff -> None
+ | AbstractEff None -> None
+ | AbstractEff (Some node) -> assert false
| BodyEff node_body -> Some node_body
-
+
(********************************************************************************)
type subst = (var_info * var_info) list
@@ -250,6 +251,10 @@ and (expand_eq_aux: Eff.local_env -> Eff.eq_info -> acc option)=
fun node_env (lhs,ve) ->
match ve.core with
| CallByPosEff( { it = Eff.CALL node ; src = lxm }, OperEff vel) ->
+ let node = match node.it.def_eff with
+ | AbstractEff (Some n) -> { it = n ; src = lxm }
+ | _ -> node
+ in
if
let nname = Ident.string_of_long2 (fst node.it.node_key_eff) in
(List.mem nname !Global.dont_expand_nodes)
@@ -302,7 +307,7 @@ let (f : Eff.local_env -> Eff.node_exp -> Eff.node_exp) =
fun n_env n ->
match n.def_eff with
| ExternEff
- | AbstractEff -> n
+ | AbstractEff _ -> n
| BodyEff b ->
let locs = get_locals n in
let acc = List.fold_left (expand_eq n_env) ([],[],locs) b.eqs_eff in
diff --git a/src/split.ml b/src/split.ml
index f3bc63e6ff2295e9c9f2ccb3598033ba27b7396e..8b77572226affa1c9bb3c97bff3319064b32f683 100644
--- a/src/split.ml
+++ b/src/split.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 10/03/2009 (at 14:40) by Erwan Jahier> *)
+(** Time-stamp: <modified the 12/03/2009 (at 10:26) by Erwan Jahier> *)
open Lxm
@@ -311,11 +311,13 @@ and (split_val_exp_list : bool ->
(vel,(eql,vl))
(* exported *)
-let (node : Eff.local_env -> Eff.node_exp -> Eff.node_exp) =
+let rec (node : Eff.local_env -> Eff.node_exp -> Eff.node_exp) =
fun n_env n ->
match n.def_eff with
| ExternEff
- | AbstractEff -> n
+ | AbstractEff None -> n
+ | AbstractEff (Some pn) ->
+ { n with def_eff = AbstractEff (Some (node n_env pn)) }
| BodyEff b ->
Name.reset_local_var_prefix "v";
let loc = match n.loclist_eff with None -> [] | Some l -> l in
diff --git a/src/structArrayExpand.ml b/src/structArrayExpand.ml
index e04c732fdc9540442f94dbb5ff70a28b3a17d59c..b3c153165eb260c262075d7fbf25d60de32c3c6c 100644
--- a/src/structArrayExpand.ml
+++ b/src/structArrayExpand.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 11/03/2009 (at 17:45) by Erwan Jahier> *)
+(** Time-stamp: <modified the 12/03/2009 (at 10:24) by Erwan Jahier> *)
(* Replace structures and arrays by as many variables as necessary.
Since structures can be recursive, it migth be a lot of new variables...
@@ -551,11 +551,13 @@ and (expand_var_info: Eff.local_env -> Eff.id_solver -> var_info list * acc ->
in
aux vi.var_type_eff
-let (node : Eff.id_solver -> Eff.local_env -> Eff.node_exp -> Eff.node_exp) =
+let rec (node : Eff.id_solver -> Eff.local_env -> Eff.node_exp -> Eff.node_exp) =
fun is n_env n ->
match n.def_eff with
| ExternEff
- | AbstractEff -> n
+ | AbstractEff None -> n
+ | AbstractEff (Some pn) ->
+ { n with def_eff = AbstractEff (Some (node is n_env pn)) }
| BodyEff b ->
let loclist = match n.loclist_eff with None -> [] | Some l -> l in
let inlist = n.inlist_eff in
diff --git a/src/uniqueOutput.ml b/src/uniqueOutput.ml
index 6f665dd2af657d349ff21a99ba28254367fa6d24..842ac35eeafec8096f74777b71f2cd6d5b90d27a 100644
--- a/src/uniqueOutput.ml
+++ b/src/uniqueOutput.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 26/01/2009 (at 16:48) by Erwan Jahier> *)
+(** Time-stamp: <modified the 12/03/2009 (at 09:41) by Erwan Jahier> *)
open Lxm
open Errors
@@ -215,7 +215,7 @@ let (check : Eff.node_exp -> Lxm.t -> unit) =
in
match node.def_eff with
| ExternEff
- | AbstractEff -> ()
+ | AbstractEff _ -> ()
| BodyEff{ eqs_eff = eql } ->
let lel = List.flatten (List.map (fun {it=(left,_)} -> left) eql) in
let lel_map = partition_var lel in