From a8359ce41a24e7f605dd815a082fddd9fdb4eec6 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Thu, 12 Mar 2009 10:48:09 +0100
Subject: [PATCH] Fix a bug in the node expanser: nodes defined in other
packages were not expanded.
---
src/eff.ml | 4 ++--
src/getEff.mli | 2 +-
src/inline.ml | 6 ++++--
src/lazyCompiler.ml | 14 +++++++++-----
src/licDump.ml | 6 +++---
src/nodesExpand.ml | 17 +++++++++++------
src/split.ml | 8 +++++---
src/structArrayExpand.ml | 8 +++++---
src/uniqueOutput.ml | 4 ++--
9 files changed, 42 insertions(+), 27 deletions(-)
diff --git a/src/eff.ml b/src/eff.ml
index b0e249ce..c567b693 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 5aeb309f..b396988b 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 5ec0f5e0..e46b0414 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 37f9b6b1..fd73920d 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 c5ffcc00..47011893 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 ed69ae72..a1e11226 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 f3bc63e6..8b775722 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 e04c732f..b3c15316 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 6f665dd2..842ac35e 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
--
GitLab