From 0b053806358355f0092eb53ee86445648a229d41 Mon Sep 17 00:00:00 2001
From: Pascal Raymond <Pascal.Raymond@imag.fr>
Date: Tue, 6 Jul 2010 10:48:48 +0200
Subject: [PATCH] Local constants in nodes added
---
src/eff.ml | 1 -
src/getEff.ml | 1 +
src/instanciateModel.ml | 1 +
src/lazyCompiler.ml | 121 ++++++++++++++++++++++++-
src/licDump.ml | 9 ++
src/licDump.mli | 3 +-
src/parserUtils.ml | 3 +
src/syntaxTreeCore.ml | 3 +-
src/test/should_work/Pascal/access.lus | 24 +++++
src/test/test.res.exp | 107 ++++++++++++++++++++++
src/test/test_ec.res.exp | 6 ++
src/test/test_lv4.res.exp | 28 ++++++
src/verbose.ml | 2 +
src/verbose.mli | 1 +
14 files changed, 303 insertions(+), 7 deletions(-)
create mode 100644 src/test/should_work/Pascal/access.lus
diff --git a/src/eff.ml b/src/eff.ml
index ffe1a86a..d6288ec9 100644
--- a/src/eff.ml
+++ b/src/eff.ml
@@ -387,7 +387,6 @@ type local_env = {
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)
diff --git a/src/getEff.ml b/src/getEff.ml
index b78c043c..673e1b28 100644
--- a/src/getEff.ml
+++ b/src/getEff.ml
@@ -685,6 +685,7 @@ and (translate_predef_static_args: Eff.id_solver ->
name = node_alias_ident;
static_params = [] ;
vars = None;
+ loc_consts = [];
def = Alias { src = lxm_n ; it = by_pos_op };
has_mem = node_eff.has_mem_eff;
is_safe = node_eff.is_safe_eff;
diff --git a/src/instanciateModel.ml b/src/instanciateModel.ml
index b2aa1377..677ef42f 100644
--- a/src/instanciateModel.ml
+++ b/src/instanciateModel.ml
@@ -74,6 +74,7 @@ let (check_arg : tables -> (Ident.t * static_arg srcflagged) list -> check_arg_a
name = s;
static_params = sparams;
vars = Some (ParserUtils.build_node_var inl outl None);
+ loc_consts = [];
def = Alias (flagit by_pos_op arg.src);
has_mem = has_memory;
is_safe = true;
diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml
index 7513cbb7..2f3e434d 100644
--- a/src/lazyCompiler.ml
+++ b/src/lazyCompiler.ml
@@ -14,7 +14,7 @@ let finish_me msg = print_string ("\n\tXXX LazyCompiler:"^msg^" -> finish me!\n
stack description.
*)
exception Recursion_error of (Ident.long as 'id) * (string list as 'stack)
-
+
exception BadCheckRef_error
let recursion_error (lxm : Lxm.t) (stack : string list) =
@@ -654,12 +654,14 @@ and (node_check_interface_do: t -> Eff.node_key -> Lxm.t ->
| _,_ ->
prov_node_exp_eff
-
and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t ->
bool -> Ident.pack_name -> SyntaxTreeCore.node_info srcflagged ->
Eff.node_exp) =
fun this nk lxm symbols provide_flag pack_name node_def ->
let lxm = node_def.src in
+ (* Creates a local_env with just the global bindings,
+ local bindinds will be added later (side effect)
+ *)
let local_env = make_local_env nk in
let node_id_solver = {
(* a [node_id_solver] is a [id_solver] where we begin to look
@@ -704,8 +706,119 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t ->
raise (Compile_error
(lxm,"\n*** Unknown ident: " ^ (Ident.to_string id)))
in
- let make_node_eff node_def_eff =
+ let make_node_eff node_def_eff = (
(* building not aliased nodes *)
+Verbose.exe ~level:3 ( fun () ->
+Printf.printf "* local_env while entering make_node_eff:\n";
+LicDump.dump_local_env local_env
+);
+ (********************************************************)
+ (* LOCAL CONSTANTS are evaluated and added to local_env *)
+ (********************************************************)
+ (* init intermediate table *)
+ let sz = List.length node_def.it.loc_consts in
+ let temp_const_eff_tab : (Ident.long, Eff.const Eff.check_flag) Hashtbl.t =
+ Hashtbl.create sz
+ in
+ let temp_const_def_tab : (Ident.t,(Lxm.t * SyntaxTreeCore.type_exp option * SyntaxTreeCore.val_exp)) Hashtbl.t =
+ Hashtbl.create sz
+ in
+ let init_local_const (lxm, cinfo) = (
+ match cinfo with
+ | DefinedConst (i,topt,ve) -> (
+ Verbose.printf ~level:3 " * local const %s will be treated\n" i;
+ Hashtbl.add temp_const_def_tab i (lxm,topt,ve)
+ )
+ | ExternalConst _
+ | EnumConst _ -> (
+ let msg = "*** abstract constant bot allowed within node "
+ in
+ raise (Compile_error(lxm, msg))
+ )
+ ) in
+ List.iter init_local_const node_def.it.loc_consts ;
+ (* differs from node_id_solver only on id2const *)
+ let rec local_id_solver = {
+ id2var = node_id_solver.id2var;
+ id2const = local_id2const;
+ id2type = node_id_solver.id2type;
+ id2node = node_id_solver.id2node;
+ symbols = node_id_solver.symbols;
+ }
+ and treat_local_const id = (
+ Verbose.printf ~level:3 " * call treat_local_const %s\n" id;
+ let id_key = ("", id) in
+ try (
+ let ce = lookup_const_eff temp_const_eff_tab id_key lxm in
+ Verbose.printf ~level:3 " * const %s already treated = %s\n" id (LicDump.string_of_const_eff ce);
+ ce
+ ) with Not_found -> (
+ let (lxmdef, toptdef, vedef) = Hashtbl.find temp_const_def_tab id in
+ Verbose.printf ~level:3 " * const %s not yet treated ...\n" id ;
+ (* yes, not yet checked *)
+ Hashtbl.add temp_const_eff_tab id_key Checking ;
+ (* computes the value with EvalConst.f id_solver ve ... *)
+ let ce = match (EvalConst.f local_id_solver vedef) with
+ | [ceff] -> (
+ match toptdef with
+ | None -> ceff
+ | Some texp -> (
+ let tdecl = GetEff.typ local_id_solver texp in
+ let teff = Eff.type_of_const ceff in
+ if (tdecl = teff ) then ceff else
+ raise (Compile_error (lxmdef, Printf.sprintf
+ " this constant is declared as '%s' but evaluated as '%s'"
+ (LicDump.string_of_type_eff4msg tdecl)
+ (LicDump.string_of_type_eff4msg teff)
+ )))
+ )
+ | [] -> assert false (* should not occur *)
+ | _::_ -> raise (Compile_error(lxmdef, "bad constant value: tuple not allowed"))
+ in
+ Verbose.printf ~level:3 " * const %s evaluated to %s\n"id (LicDump.string_of_const_eff ce);
+ Hashtbl.replace temp_const_eff_tab id_key (Checked ce) ;
+ ce
+ )
+ )
+ and local_id2const idrf lxm = (
+ (* is id a local const ? *)
+ try (
+ (* certainly NOT if id has a pack *)
+ let id = if (Ident.pack_of_idref idrf = None)
+ then Ident.name_of_idref idrf
+ else raise Not_found
+ in
+ let ce = treat_local_const id in
+ ce
+ ) with Not_found -> (
+ (* not a local constant -> search in global env *)
+ Verbose.printf ~level:3 " * %s not a local const, should be global ?" (Ident.string_of_idref idrf);
+ let ce = node_id_solver.id2const idrf lxm in
+ Verbose.printf ~level:3 " YES -> %s\n" (LicDump.string_of_const_eff ce);
+ ce
+ )
+ ) in
+ (* iters local_id2const n eeach declared constant *)
+ Hashtbl.iter (fun id _ -> let _ = treat_local_const id in ()) temp_const_def_tab ;
+ (* Finally, adds each local const to ICI *)
+ let add_local_const idref ceck = (
+ Verbose.printf ~level:3 " * add_local_const %s = %s\n"
+ (snd idref)
+ (match ceck with
+ | Checking -> "Checking"
+ | Checked ce -> (LicDump.string_of_const_eff ce)
+ | Incorrect -> "Incorrect"
+ );
+ match ceck with
+ | Checked ce -> Hashtbl.add local_env.lenv_const (snd idref) ce
+ | _ -> assert false
+ ) in
+ Hashtbl.iter add_local_const temp_const_eff_tab ;
+
+ (********************************************************)
+ (* LOCAL FLOWS are added to local_env *)
+ (********************************************************)
+ (* (i.e. ins,outs,locs) *)
match node_def.it.vars with
| None -> assert false (* a node with a body should have a profile *)
| Some vars ->
@@ -798,7 +911,7 @@ and (node_check_do: t -> Eff.node_key -> Lxm.t -> SymbolTab.t ->
is_safe_eff = node_def.it.is_safe;
is_polym_eff = !is_polymorphic
}
- in
+ ) in
let (make_alias_node : Eff.node_exp -> node_vars option -> Eff.node_exp) =
fun aliased_node vars_opt ->
(* builds a node that calls the aliased node. It looks like:
diff --git a/src/licDump.ml b/src/licDump.ml
index fdab05d5..2f2a7103 100644
--- a/src/licDump.ml
+++ b/src/licDump.ml
@@ -695,3 +695,12 @@ let print_global_node_error lxm nkey msg = (
flush stderr
)
+
+(* debug *)
+let dump_local_env e = (
+ let pt i t = Printf.printf "type %s = %s\n" i (string_of_type_eff t) in
+ Hashtbl.iter pt e.lenv_types;
+ let pc i t = Printf.printf "const %s = %s\n" i (string_of_const_eff t) in
+ Hashtbl.iter pc e.lenv_const;
+)
+
diff --git a/src/licDump.mli b/src/licDump.mli
index 4c9f36c5..5b6cfba5 100644
--- a/src/licDump.mli
+++ b/src/licDump.mli
@@ -34,4 +34,5 @@ val string_of_clock2 : Eff.clock -> string
val string_of_val_exp_eff : Eff.val_exp -> string
val string_of_val_exp_eff_core : Eff.val_exp_core -> string
-
+(* dump Eff.local_env *)
+val dump_local_env : Eff.local_env -> unit
diff --git a/src/parserUtils.ml b/src/parserUtils.ml
index 2fdb1a69..987a398e 100644
--- a/src/parserUtils.ml
+++ b/src/parserUtils.ml
@@ -402,6 +402,7 @@ let (treat_node_decl : bool -> Lxm.t -> static_param srcflagged list ->
name = nstr;
static_params = statics;
vars = Some vars;
+ loc_consts = locconsts;
def = Body { asserts = asserts ; eqs = eqs };
has_mem = has_memory;
is_safe = true;
@@ -426,6 +427,7 @@ let (treat_node_alias : bool -> Lxm.t -> static_param srcflagged list ->
name = nstr;
static_params = statics;
vars = vars;
+ loc_consts = [];
def = Alias (flagit (CALL_n value) value.src);
has_mem = has_memory;
is_safe = true;
@@ -450,6 +452,7 @@ let treat_abstract_or_extern_node_do (* cf the profile of [treat_abstract_node]
name = Lxm.id lxm;
static_params = [];
vars = Some vars;
+ loc_consts = [];
def = if is_abstract then Abstract else Extern;
has_mem = has_memory;
is_safe = true;
diff --git a/src/syntaxTreeCore.ml b/src/syntaxTreeCore.ml
index a891707b..071a6084 100644
--- a/src/syntaxTreeCore.ml
+++ b/src/syntaxTreeCore.ml
@@ -28,6 +28,7 @@ and node_info = {
static_params : static_param srcflagged list;
vars : node_vars option; (* aliased node may have no i/o decl *)
(* consts : ICI A FAIRE *)
+ loc_consts : (Lxm.t * const_info) list;
def : node_def;
has_mem : bool;
is_safe : bool;
@@ -155,7 +156,7 @@ and static_arg =
(** constant *)
-type const_info =
+and const_info =
| ExternalConst of (Ident.t * type_exp * val_exp option)
| EnumConst of (Ident.t * type_exp)
| DefinedConst of (Ident.t * type_exp option * val_exp)
diff --git a/src/test/should_work/Pascal/access.lus b/src/test/should_work/Pascal/access.lus
new file mode 100644
index 00000000..b9e2f3e8
--- /dev/null
+++ b/src/test/should_work/Pascal/access.lus
@@ -0,0 +1,24 @@
+
+(* Recursive logarithmic, (lustre-v4 like) *)
+
+node quick_access
+ <<type t; const sz: int; const dflt: t>>
+ (tab: t^sz; ix: t) returns (res: t);
+
+const mid : int = sz div 2;
+ z2wde = mid + 1;
+
+let
+ res = with ( sz = 1) then
+ if ix = 0 then tab[0] else dflt
+ else
+ if ix < mid then
+ quick_access<<t, mid, dflt>>(tab[0..mid-1], ix)
+ else
+ quick_access<<t, sz-mid, dflt>>(tab[mid..sz-1], ix-mid)
+ ;
+tel
+
+node quick_access_int8 = quick_access<<int, 8, -1>>;
+
+
diff --git a/src/test/test.res.exp b/src/test/test.res.exp
index c86c89ba..ac653c65 100644
--- a/src/test/test.res.exp
+++ b/src/test/test.res.exp
@@ -8423,6 +8423,113 @@ let
tel
-- end of node v1::v1
+----------------------------------------------------------------------
+====> ../lus2lic -vl 2 should_work/Pascal/access.lus
+Opening file should_work/Pascal/access.lus
+-- ../lus2lic -vl 2 should_work/Pascal/access.lus
+
+
+node n_access::quick_access_int_1_-1(
+ tab:A_int_1;
+ ix:int)
+returns (
+ res:int);
+var
+ _v_1:bool;
+ _v_2:int;
+ _v_3:int;
+let
+ res = _v_3;
+ _v_1 = ix = 0;
+ _v_2 = tab[0];
+ _v_3 = if _v_1 then _v_2 else -1;
+tel
+-- end of node n_access::quick_access_int_1_-1
+
+node n_access::quick_access_int_2_-1(
+ tab:A_int_2;
+ ix:int)
+returns (
+ res:int);
+var
+ _v_1:bool;
+ _v_2:A_int_1;
+ _v_3:int;
+ _v_4:A_int_1;
+ _v_5:int;
+ _v_6:int;
+ _v_7:int;
+let
+ res = _v_7;
+ _v_1 = ix < 1;
+ _v_2 = tab[0 .. 0];
+ _v_3 = n_access::quick_access_int_1_-1(_v_2, ix);
+ _v_4 = tab[1 .. 1];
+ _v_5 = ix - 1;
+ _v_6 = n_access::quick_access_int_1_-1(_v_4, _v_5);
+ _v_7 = if _v_1 then _v_3 else _v_6;
+tel
+-- end of node n_access::quick_access_int_2_-1
+
+node n_access::quick_access_int_4_-1(
+ tab:A_int_4;
+ ix:int)
+returns (
+ res:int);
+var
+ _v_1:bool;
+ _v_2:A_int_2;
+ _v_3:int;
+ _v_4:A_int_2;
+ _v_5:int;
+ _v_6:int;
+ _v_7:int;
+let
+ res = _v_7;
+ _v_1 = ix < 2;
+ _v_2 = tab[0 .. 1];
+ _v_3 = n_access::quick_access_int_2_-1(_v_2, ix);
+ _v_4 = tab[2 .. 3];
+ _v_5 = ix - 2;
+ _v_6 = n_access::quick_access_int_2_-1(_v_4, _v_5);
+ _v_7 = if _v_1 then _v_3 else _v_6;
+tel
+-- end of node n_access::quick_access_int_4_-1
+
+node n_access::quick_access_int_8_-1(
+ tab:A_int_8;
+ ix:int)
+returns (
+ res:int);
+var
+ _v_1:bool;
+ _v_2:A_int_4;
+ _v_3:int;
+ _v_4:A_int_4;
+ _v_5:int;
+ _v_6:int;
+ _v_7:int;
+let
+ res = _v_7;
+ _v_1 = ix < 4;
+ _v_2 = tab[0 .. 3];
+ _v_3 = n_access::quick_access_int_4_-1(_v_2, ix);
+ _v_4 = tab[4 .. 7];
+ _v_5 = ix - 4;
+ _v_6 = n_access::quick_access_int_4_-1(_v_4, _v_5);
+ _v_7 = if _v_1 then _v_3 else _v_6;
+tel
+-- end of node n_access::quick_access_int_8_-1
+node access::quick_access_int8(tab:A_int_8; ix:int) returns (res:int);
+let
+ res = n_access::quick_access_int_8_-1(tab, ix);
+tel
+-- end of node access::quick_access_int8
+-- automatically defined aliases:
+type A_int_8 = int^8;
+type A_int_2 = int^2;
+type A_int_4 = int^4;
+type A_int_1 = int^1;
----------------------------------------------------------------------
====> ../lus2lic -vl 2 should_work/Pascal/consensus.lus
Opening file should_work/Pascal/consensus.lus
diff --git a/src/test/test_ec.res.exp b/src/test/test_ec.res.exp
index 978c958f..e651583c 100644
--- a/src/test/test_ec.res.exp
+++ b/src/test/test_ec.res.exp
@@ -498,6 +498,12 @@ ec2c /tmp/xx.ec
====> ../lus2lic -vl 2 -ec should_work/NONREG/v1.lus -o /tmp/xx.ec
ec2c /tmp/xx.ec
+----------------------------------------------------------------------
+====> ../lus2lic -vl 2 -ec should_work/Pascal/access.lus -o /tmp/xx.ec
+ec2c /tmp/xx.ec
+syntax errors...
+syntax error - at line 5
+
----------------------------------------------------------------------
====> ../lus2lic -vl 2 -ec should_work/Pascal/consensus.lus -o /tmp/xx.ec
ec2c /tmp/xx.ec
diff --git a/src/test/test_lv4.res.exp b/src/test/test_lv4.res.exp
index abc55c7a..2e8d3f62 100644
--- a/src/test/test_lv4.res.exp
+++ b/src/test/test_lv4.res.exp
@@ -791,6 +791,34 @@ lus2ec /tmp/xx.lus uu__uu
lus2ec /tmp/xx.lus v1__v1
--Pollux Version 2.3a
+----------------------------------------------------------------------
+====> ../lus2lic -vl 2 -lv4 should_work/Pascal/access.lus -o /tmp/xx.lus
+lus2ec /tmp/xx.lus n_access__quick_access_int_1_
+--Pollux Version 2.3a
+ syntax error detected while reading `-` (token 49) line 6 in main file xx.lus
+
+1 PolluxErrors found
+lus2ec /tmp/xx.lus n_access__quick_access_int_2_
+--Pollux Version 2.3a
+ syntax error detected while reading `-` (token 49) line 6 in main file xx.lus
+
+1 PolluxErrors found
+lus2ec /tmp/xx.lus n_access__quick_access_int_4_
+--Pollux Version 2.3a
+ syntax error detected while reading `-` (token 49) line 6 in main file xx.lus
+
+1 PolluxErrors found
+lus2ec /tmp/xx.lus n_access__quick_access_int_8_
+--Pollux Version 2.3a
+ syntax error detected while reading `-` (token 49) line 6 in main file xx.lus
+
+1 PolluxErrors found
+lus2ec /tmp/xx.lus access__quick_access_int8
+--Pollux Version 2.3a
+ syntax error detected while reading `-` (token 49) line 6 in main file xx.lus
+
+1 PolluxErrors found
+
----------------------------------------------------------------------
====> ../lus2lic -vl 2 -lv4 should_work/Pascal/consensus.lus -o /tmp/xx.lus
lus2ec /tmp/xx.lus n_consensus__consensus_1
diff --git a/src/verbose.ml b/src/verbose.ml
index 0a278b55..ed10721b 100644
--- a/src/verbose.ml
+++ b/src/verbose.ml
@@ -36,6 +36,8 @@ let printf ?(level=1) s = Printf.kprintf
let print_string ?(level=1) s =
if (!_level >= level) then (print_string s; flush stdout)
+let exe ?(level=1) p =
+ if (!_level >= level) then p ()
(**** VERSION GORE *****)
(*
diff --git a/src/verbose.mli b/src/verbose.mli
index 3124d327..e08817db 100644
--- a/src/verbose.mli
+++ b/src/verbose.mli
@@ -17,4 +17,5 @@ val set_level : int -> unit
val get_level : unit -> int
val printf : ?level:int -> ('a, unit, string, unit) format4 -> 'a
+val exe : ?level:int -> (unit -> unit) -> unit
val print_string : ?level:int -> string -> unit
--
GitLab