Newer
Older
Erwan Jahier
committed
(** Time-stamp: <modified the 29/09/2010 (at 16:20) by Erwan Jahier> *)
Erwan Jahier
committed
let finish_me msg = print_string ("\n\tXXX LazyCompiler:"^msg^" -> finish me!\n")
Erwan Jahier
committed
(******************************************************************************)
(** Returns the ident on which the recursion was detected, plus an execution
Erwan Jahier
committed
stack description.
exception Recursion_error of (Ident.long as 'id) * (string list as 'stack)
Erwan Jahier
committed
let recursion_error (lxm : Lxm.t) (stack : string list) =
Erwan Jahier
committed
| s::[] -> s
| s::l -> s^"\n > "^(string_of_stack l)
in
raise ( Compile_error
(lxm, "Recursion loop detected: \n*** " ^(string_of_stack stack)
Erwan Jahier
committed
(******************************************************************************)
Erwan Jahier
committed
src_tab : SyntaxTab.t;
types : (Eff.item_key, Eff.type_ Eff.check_flag) Hashtbl.t;
consts : (Eff.item_key, Eff.const Eff.check_flag) Hashtbl.t;
nodes : (Eff.node_key, Eff.node_exp Eff.check_flag) Hashtbl.t;
prov_types : (Eff.item_key, Eff.type_ Eff.check_flag) Hashtbl.t;
prov_consts : (Eff.item_key, Eff.const Eff.check_flag) Hashtbl.t;
prov_nodes : (Eff.node_key, Eff.node_exp Eff.check_flag) Hashtbl.t
Erwan Jahier
committed
(******************************************************************************)
(* exported *)
let (create : SyntaxTab.t -> t) =
fun tbl ->
let nodes_tbl = Hashtbl.create 0 in
let prov_nodes_tbl = Hashtbl.create 0 in
List.iter
(fun op ->
let op_str = Predef.op2string op in
let op_eff = PredefEvalType.make_node_exp_eff None op (Lxm.dummy op_str) [] in
let op_key = Predef.op_to_long op, [] in
Hashtbl.add nodes_tbl op_key (Eff.Checked op_eff);
Hashtbl.add prov_nodes_tbl op_key (Eff.Checked op_eff)
)
Predef.iterable_op;
{
src_tab = tbl;
types = Hashtbl.create 0;
consts = Hashtbl.create 0;
nodes = nodes_tbl;
prov_types = Hashtbl.create 0;
prov_consts = Hashtbl.create 0;
prov_nodes = prov_nodes_tbl;
}
Erwan Jahier
committed
(******************************************************************************)
(** Type checking + constant checking/evaluation
This is performed (lazily) by 10 mutually recursive functions:
--------------
(1) [type_check env type_name lxm]: type check the type id [type_name]
(2) [type_check_do]: untabulated version of [type_check] (do the real work).
(3) [type_check_interface]: ditto, but for the interface part
(4) [type_check_interface_do]: untabulated version (do the real work)
(5) [solve_type_idref] solves constant reference (w.r.t. short/long ident)
(6) [const_check env const_name lxm]: eval/check the constant [const_name]
(7) [const_check_do] : untabulated version (do the real work)
(8) [const_check_interface]: ditto, but for the interface part
(9) [const_check_interface_do]: untabulated version (do the real work)
(10) [solve_const_idref] solves constant reference (w.r.t. short/long ident)
checking nodes
--------------
(11) [node_check env node_name lxm]: check the node [node_name]
checking a node means checking its interface and checking it equations/asserts.
checking an equation means checking that the type and clock of the
left part is the same as the ones of the rigth part.
(12) [node_check_do] : untabulated version (do the real work)
(13) [node_check_interface]: ditto, but for the interface part
(14) [node_check_interface_do]: untabulated version (do the real work)
(15) [solve_node_idref] solves constant reference (w.r.t. short/long ident)
XXX checking clocks
-------------------
nb: for x in {type, const, node, clock}, there are several functions
that returns [x_eff]:
o tabulates its result
o takes an x_key and returns an [x_eff]
o lookups its (syntaxic) definition (x_info) via the symbolTab.t
o calls [GetEff.X] to translate its sub-terms
- [GetEff.X]
o takes a [x_exp] (i.e., an expression) and returns an [x_eff]
o compute the effective static args (for nodes)
o calls [solve_x_idref] (via [id_solver]) to translate its sub-terms
o takes an idref (plus a Eff.static_arg list for x=node!)
o perform name resolution
o calls [x_check] (loop!)
nb2: the top-level call is [node_check], on a node that necessarily contains
no static parameters.
(* Before starting, let's define a few utilitary functions. *)
(** Intermediary results are put into a table. This tabulation handling
is common to type and constant checking, and is performed by the
2 following functions.
Since [x] is meant to stand for [type], [const], or [node], those 2
functions will lead to the definition of 6 functions:
[type_check], [const_check], [node_check],
[type_check_interface], [const_check_interface], [node_check_interface].
let x_check
tab find_x x_check_do lookup_x_eff pack_of_x_key name_of_x_key this x_key lxm =
try lookup_x_eff tab x_key lxm
let (x_pack,xn) = (pack_of_x_key x_key, name_of_x_key x_key) in
let x_pack_symbols = SyntaxTab.pack_body_env this.src_tab x_pack in
let x_def = match find_x x_pack_symbols xn lxm with
| SymbolTab.Local x_def -> x_def
| SymbolTab.Imported (lid,_) ->
print_string ("*** " ^ (Ident.string_of_long lid) ^ "???\n" ^
(Lxm.details lxm));
assert false (* should not occur *)
let res = x_check_do this x_key lxm x_pack_symbols false x_pack x_def in
Hashtbl.replace tab x_key (Eff.Checked res);
tab find_x x_check x_check_interface_do lookup_x_eff
pack_of_x_key name_of_x_key this x_key lxm =
try lookup_x_eff tab x_key lxm
let (xp,xn) = (pack_of_x_key x_key, name_of_x_key x_key) in
let xp_prov_symbols_opt = SyntaxTab.pack_prov_env this.src_tab xp lxm in
let res = (* [xp] migth have no provided symbol table *)
match xp_prov_symbols_opt with
| None ->
(* if [xp] have no provided symbol table, the whole package is exported. *)
x_check this x_key lxm
| Some xp_prov_symbols ->
let x_def = match find_x xp_prov_symbols xn lxm with
| SymbolTab.Local x -> x
| SymbolTab.Imported _ -> assert false (* should not occur *)
in
x_check_interface_do this x_key lxm xp_prov_symbols xp x_def
Hashtbl.replace tab x_key (Eff.Checked res);
res
(* Returns the tabulated [type] or [const], if it has already been computed;
otherwise, raise [Not_found] otherwise. *)
let lookup_x_eff x_label id_of_x_key x_tab x_key lxm =
match Hashtbl.find x_tab x_key with
| Eff.Checked res -> res
| Eff.Checking ->
raise (Recursion_error (id_of_x_key x_key, [x_label^(Lxm.details lxm)]))
| Eff.Incorrect -> raise (BadCheckRef_error)
let (lookup_type_eff: (Eff.item_key, Eff.type_ Eff.check_flag) Hashtbl.t ->
Ident.long -> Lxm.t -> Eff.type_) =
let (lookup_const_eff:(Eff.item_key, Eff.const Eff.check_flag) Hashtbl.t ->
Ident.long -> Lxm.t -> Eff.const) =
let (lookup_node_exp_eff:
(Eff.node_key, Eff.node_exp Eff.check_flag) Hashtbl.t ->
Eff.node_key -> Lxm.t -> Eff.node_exp) =
fun tbl key lxm ->
try lookup_x_eff "node ref " (fun k -> fst k) tbl key lxm
with
Not_found ->
if fst (fst key) = "Lustre" then (
let msg = "*** " ^ (snd (fst key)) ^ ": unknown Lustre operator. "^
"Available operators are:\n" ^
(Hashtbl.fold (fun (long,_) _ acc -> acc ^ ("\t - "^ (Ident.string_of_long long ) ^ "\n")) tbl "")
in
raise (Compile_error(lxm, msg))
)
else
raise Not_found
(* lookup_x_eff "node ref " (fun k -> fst k) *)
(** This function performs the identifier (idref) resolution,
i.e., when an ident is not explicitely prefixed by a module
name, we decide here to which module it belongs.
The [provide_flag] indicates whether that function was called
from a provide part or not.
*)
x_check_interface x_check find_x x_label to_x_key this symbols
provide_flag currpack idr sargs lxm =
let s = Ident.name_of_idref idr in
match Ident.pack_of_idref idr with
| Some p ->
if p = currpack
then x_check this (to_x_key currpack s) lxm
else x_check_interface this (to_x_key p s) lxm
(* no pack name: it must be in the symbols table *)
try
match (find_x symbols s lxm) with
| SymbolTab.Local x_info ->
if provide_flag
then x_check_interface this (to_x_key currpack s) lxm
else x_check this (to_x_key currpack s) lxm
| SymbolTab.Imported(fid,params) ->
let (pi,si) = (Ident.pack_of_long fid, Ident.of_long fid) in
assert(params=[]); (* todo *)
x_check_interface this (to_x_key pi si) lxm
(raise (Compile_error(lxm,"unbounded " ^ x_label ^ " ident")))
(* And now we can start the big mutually recursive definition... *)
(** Tabulated version of [type_check_do]. *)
let rec (type_check : t -> Ident.long -> Lxm.t -> Eff.type_) =
x_check this.types SymbolTab.find_type type_check_do lookup_type_eff
Ident.pack_of_long Ident.of_long this
and (const_check : t -> Ident.long -> Lxm.t -> Eff.const) =
x_check this.consts SymbolTab.find_const const_check_do lookup_const_eff
Ident.pack_of_long Ident.of_long this
(** Tabulated version of [type_check_interface_do]. *)
and (type_check_interface: t -> Ident.long -> Lxm.t -> Eff.type_) =
x_check_interface
this.prov_types SymbolTab.find_type type_check type_check_interface_do
lookup_type_eff Ident.pack_of_long Ident.of_long this
(** Tabulated version of [const_check_interface_do]. *)
and (const_check_interface: t -> Ident.long -> Lxm.t -> Eff.const) =
fun this ->
x_check_interface
this.prov_consts SymbolTab.find_const const_check const_check_interface_do
lookup_const_eff Ident.pack_of_long Ident.of_long this
and (solve_type_idref : t -> SymbolTab.t -> bool -> Ident.pack_name ->
fun this symbols provide_flag currpack idr lxm ->
type_check_interface type_check SymbolTab.find_type "type"
(fun p id -> Ident.make_long p id)
this symbols provide_flag currpack idr [] lxm
and (solve_const_idref : t -> SymbolTab.t -> bool -> Ident.pack_name ->
fun this symbols provide_flag currpack idr lxm ->
const_check_interface const_check SymbolTab.find_const "const"
(fun p id -> Ident.make_long p id)
this symbols provide_flag currpack idr [] lxm
and (type_check_interface_do: t -> Ident.long -> Lxm.t -> SymbolTab.t ->
Ident.pack_name -> SyntaxTreeCore.type_info srcflagged ->
fun this type_name lxm prov_symbols pack_name type_def ->
(* We type check the interface and the body.
For non-abstract types, we also check that both effective types are
the same. *)
let body_type_eff = type_check this type_name lxm in
type_check_do this type_name lxm prov_symbols true pack_name type_def
if Eff.type_are_compatible prov_type_eff body_type_eff then
raise(Compile_error (
type_def.src,
("provided type \n\t" ^
Erwan Jahier
committed
(LicDump.string_of_type_eff4msg prov_type_eff) ^
"\n is not compatible with its implementation \n\t" ^
Erwan Jahier
committed
(LicDump.string_of_type_eff4msg body_type_eff))))
and (const_check_interface_do: t -> Ident.long -> Lxm.t -> SymbolTab.t ->
let prov_const_eff = const_check_do this cn lxm prov_symbols true p const_def in
match prov_const_eff, body_const_eff with
| Eff.Extern_const_eff (_), _ -> assert false
| Eff.Abstract_const_eff (id, teff, v, is_exported),
Eff.Abstract_const_eff (body_id, body_teff, body_v, body_is_exported)
->
assert false
(* indeed, how can a body constant be extern and have a value? *)
| Eff.Abstract_const_eff (id, teff, v, is_exported),
Eff.Extern_const_eff (body_id, body_teff)
->
if (id <> cn) then assert false
else if not (Eff.type_are_compatible teff body_teff) then
raise(Compile_error (
const_def.src,
("provided constant type \n***\t" ^
(LicDump.string_of_type_eff4msg teff) ^
" is not compatible with its implementation \n***\t" ^
(LicDump.string_of_type_eff4msg body_teff) ^ "")))
else if
is_exported
then
raise(Compile_error (const_def.src, " constant values mismatch"))
else
Eff.Extern_const_eff (body_id, body_teff)
| Eff.Abstract_const_eff (id, teff, v, is_exported), _ ->
let body_teff = Eff.type_of_const body_const_eff in
if (id <> cn) then assert false
else if not (Eff.type_are_compatible teff body_teff) then
raise(Compile_error (
const_def.src,
("provided constant type \n***\t" ^
(LicDump.string_of_type_eff4msg teff) ^
" is not compatible with its implementation \n***\t" ^
(LicDump.string_of_type_eff4msg body_teff) ^ "")))
else
if is_exported && body_const_eff <> v then
raise(Compile_error (const_def.src, " constant values mismatch"))
else
Eff.Abstract_const_eff (id, teff, body_const_eff, is_exported)
| Eff.Enum_const_eff (_, _), _
| Eff.Bool_const_eff _, _
| Eff.Int_const_eff _, _
| Eff.Real_const_eff _, _
| Eff.Struct_const_eff (_,_), _
| Eff.Array_const_eff (_,_), _
if prov_const_eff = body_const_eff then
body_const_eff
else
raise(Compile_error (
const_def.src,
"\n*** provided constant does not match with its definition."))
and (type_check_do: t -> Ident.long -> Lxm.t -> SymbolTab.t -> bool ->
Ident.pack_name -> SyntaxTreeCore.type_info srcflagged ->
fun this type_name lxm symbols provide_flag pack_name type_def ->
(* Solveur d'idref pour les appels eval_type/eval_const *)
let id_solver = {
id2var = (fun idref lxm -> raise (Unknown_var(lxm,idref)) (* should not occur *));
id2const = solve_const_idref this symbols provide_flag pack_name;
id2type = solve_type_idref this symbols provide_flag pack_name;
id2node = solve_node_idref this symbols provide_flag pack_name;
symbols = symbols;
match type_def.it with
| ArrayType _ -> finish_me " array handling "; assert false
| ExternalType s -> (
let lid = Ident.make_long pack_name s in
let idref = Ident.idref_of_long lid in
try
Abstract_type_eff (lid, id_solver.id2type idref lxm)
with e ->
External_type_eff (lid)
| AliasedType (s, texp) -> GetEff.typ id_solver texp
| EnumType (s, clst) -> (
let n = Ident.make_long pack_name s in
let add_pack_name x = Ident.make_long pack_name x.it in
Enum_type_eff (n, List.map add_pack_name clst)
)
| StructType sti -> (
let make_field (fname : Ident.t) =
let field_def = Hashtbl.find sti.st_ftable fname in
let teff = GetEff.typ id_solver field_def.it.fd_type in
match field_def.it.fd_value with
| None -> (fname, (teff, None))
| Some vexp -> (
let veff = EvalConst.f id_solver vexp in
match veff with
| [v] -> (
if (tv = teff) then (fname, (teff, Some v)) else
raise
(Compile_error(field_def.src, Printf.sprintf
" this field is declared as '%s' but evaluated as '%s'"
Erwan Jahier
committed
(LicDump.string_of_type_eff4msg teff)
(LicDump.string_of_type_eff4msg tv)))
)
| [] -> assert false (* should not occur *)
| _::_ ->
raise (Compile_error(field_def.src,
"bad field value: tuple not allowed"))
)
in
let n = Ident.make_long pack_name sti.st_name in
let eff_fields = List.map make_field sti.st_flist in
Struct_type_eff (n, eff_fields)
)
let is_struct_or_array = match type_eff with
| Array_type_eff(_)
| Struct_type_eff(_) -> true
| Any | Overload | Bool_type_eff | Int_type_eff | Real_type_eff
| External_type_eff(_) | Abstract_type_eff(_) | Enum_type_eff(_)
-> false
if
(not provide_flag)
&& (not (!Global.expand_structs & is_struct_or_array))
(* && not !Global.ec (* ec does not need type decl at all *) *)
then
output_string !Global.oc (LicDump.type_decl type_name type_eff);
type_eff
with
(* capte et complete/stoppe les recursions *)
Recursion_error (root, stack) ->
if (root = type_name) then recursion_error type_def.src stack else
raise ( Recursion_error (root, ("type ref "^(Lxm.details lxm))::stack))
and (const_check_do : t -> Ident.long -> Lxm.t -> SymbolTab.t -> bool ->
Ident.pack_name -> SyntaxTreeCore.const_info srcflagged ->
fun this cn lxm symbols provide_flag currpack const_def ->
(* [cn] and [lxm] are used for recursion errors.
[symbols] is the current symbol table.
(* Solveur d'idref pour les les appels eval_type/eval_const *)
id2var = (fun idref lxm -> assert false (* should not occur *));
id2const = solve_const_idref this symbols provide_flag currpack;
id2type = solve_type_idref this symbols provide_flag currpack;
id2node = solve_node_idref this symbols provide_flag currpack;
symbols = symbols;
match const_def.it with
| ExternalConst (id, texp, val_opt) ->
let lid = Ident.make_long currpack id in
let teff = GetEff.typ id_solver texp in
if provide_flag then
match val_opt with
| None ->
(* we put a fake value here as we don't know yet the
concrete value. this will be filled in
const_check_interface_do. I could have put an option
type, but that would make quite a lot of noise in the
remaining...
*)
Abstract_const_eff(lid, teff, Int_const_eff (-666), false)
| Some c ->
let ceff = match EvalConst.f id_solver c with
| [ceff] -> ceff
| _ -> assert false
in
Abstract_const_eff(lid, teff, ceff, true)
else
(match val_opt with
| None -> Extern_const_eff(lid, teff)
| Some c -> assert false
(* indeed, how can a body constant be extern and have a value? *)
)
| EnumConst (id, texp) ->
Enum_const_eff ((Ident.make_long currpack id), GetEff.typ id_solver texp)
| DefinedConst (id, texp_opt, vexp ) -> (
match (EvalConst.f id_solver vexp) with
| [ceff] -> (
match texp_opt with
| None -> ceff
| Some texp -> (
let tdecl = GetEff.typ id_solver texp in
if (tdecl = teff ) then ceff else
raise
(Compile_error (const_def.src, 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(const_def.src,
"bad constant value: tuple not allowed"))
in
let is_struct_or_array = match const_eff with
| Struct_const_eff _ -> true
| Array_const_eff _ -> true
| _ -> false
in
let is_extern_const =
Erwan Jahier
committed
match const_eff with
| Enum_const_eff(_) ->
!Global.expand_enums (* When expanding enums, we treat them as extern const *)
&& not provide_flag (* Avoid to define them twice *)
| Extern_const_eff(_)
-> true
| _ -> false
(not provide_flag
&& (not (!Global.expand_structs & is_struct_or_array))
Erwan Jahier
committed
&& (not !Global.ec) (* ec does not need constant decl, except extern ones *)
) || is_extern_const
output_string !Global.oc (LicDump.const_decl cn const_eff);
) with Recursion_error (root, stack) -> (
(* capte et complete/stoppe les recursions *)
if (root = cn) then recursion_error const_def.src stack else
(* on complete la stack *)
raise (Recursion_error (root, ("const ref "^(Lxm.details lxm))::stack))
)
(******************************************************************************)
and (node_check_interface_do: t -> Eff.node_key -> Lxm.t ->
SymbolTab.t -> Ident.pack_name -> SyntaxTreeCore.node_info srcflagged ->
fun this nk lxm symbols pn node_def ->
let body_node_exp_eff = node_check this nk lxm in
let prov_node_exp_eff = node_check_do this nk lxm symbols true pn node_def in
(** [type_eff_are_compatible t1 t2] checks that t1 is compatible with t2, i.e.,
let msg_prefix =
("provided node for " ^ (Ident.string_of_long (fst nk)) ^
let str_of_var = LicDump.type_string_of_var_info_eff4msg in
let type_is_not_comp v1 v2 = not (Eff.var_are_compatible v1 v2) in
(* Checking the type profile (w.r.t the body and the provided part) *)
let ibtypes = List.map (fun v -> v.var_type_eff) body_node_exp_eff.inlist_eff
and iptypes = List.map (fun v -> v.var_type_eff) prov_node_exp_eff.inlist_eff
and obtypes = List.map (fun v -> v.var_type_eff) body_node_exp_eff.outlist_eff
and optypes = List.map (fun v -> v.var_type_eff) prov_node_exp_eff.outlist_eff
in
let topt = UnifyType.profile_is_compatible nk
node_def.src (iptypes,ibtypes) (optypes,obtypes)
in
let _ =
(* the type profile seems ok, but it may need to unfreeze some
polymorphic nodes *)
match topt with
| None -> ()
| Some t -> GetEff.dump_polymorphic_nodes t
in
if
prov_node_exp_eff.node_key_eff <> body_node_exp_eff.node_key_eff
then
raise(Compile_error (node_def.src, msg_prefix ^ " ??? "))
else if
(* ougth to be checked above: well, it eats no bread to keep that check *)
(List.exists2 type_is_not_comp
prov_node_exp_eff.inlist_eff body_node_exp_eff.inlist_eff)
then
let msg = msg_prefix ^ "bad input profile. \n*** " ^
(String.concat "*" (List.map str_of_var prov_node_exp_eff.inlist_eff)) ^
" <> " ^
(String.concat "*" (List.map str_of_var body_node_exp_eff.inlist_eff))
in
raise(Compile_error (node_def.src, msg))
else if
(List.exists2 type_is_not_comp
prov_node_exp_eff.outlist_eff body_node_exp_eff.outlist_eff)
(* ougth to be checked above: well, it eats no bread to keep that check *)
then
let msg = msg_prefix ^ "bad output profile. \n*** " ^
(String.concat "*" (List.map str_of_var prov_node_exp_eff.outlist_eff)) ^
" <> " ^
(String.concat "*" (List.map str_of_var body_node_exp_eff.outlist_eff))
in
raise(Compile_error (node_def.src, msg))
else if
prov_node_exp_eff.has_mem_eff <> body_node_exp_eff.has_mem_eff
then
raise(Compile_error (node_def.src, msg_prefix ^ " node or function?"))
else if
prov_node_exp_eff.is_safe_eff <> body_node_exp_eff.is_safe_eff
then
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
| (_,_) -> prov_node_exp_eff.def_eff <> body_node_exp_eff.def_eff
raise(Compile_error (node_def.src, msg_prefix ^ "abstract or not?"))
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 ->
fun this nk lxm symbols provide_flag pack_name node_def ->
Erwan Jahier
committed
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
into the local environement before looking at the global
one. *)
id2var = (* var can only be local to the node *)
try lookup_var local_env (Ident.of_idref id) lxm
with Not_found ->
raise (Unknown_var(lxm,id))
);
id2const =
Erwan Jahier
committed
with Not_found ->
solve_const_idref this symbols provide_flag pack_name id lxm);
id2type =
Erwan Jahier
committed
with Not_found ->
solve_type_idref this symbols provide_flag pack_name id lxm);
id2node =
Erwan Jahier
committed
(try
let node_id, inlist, outlist = lookup_node local_env id sargs lxm in
let node_id = Ident.idref_of_long node_id in
solve_node_idref this symbols provide_flag pack_name node_id [] lxm
(* node_check this (node_id,[]) lxm *)
Erwan Jahier
committed
with
Not_found ->
solve_node_idref this symbols provide_flag pack_name id sargs lxm
| _ -> assert false)
);
Erwan Jahier
committed
let find_var_info lxm vars id =
try Hashtbl.find vars.vartable id
with Not_found ->
raise (Compile_error
(lxm,"\n*** Unknown ident: " ^ (Ident.to_string id)))
in
(* building not aliased nodes *)
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
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 ->
Erwan Jahier
committed
let is_polymorphic = ref false in
Erwan Jahier
committed
let vi = find_var_info lxm vars id in
let t_eff = GetEff.typ node_id_solver vi.it.var_type in
let _ = if Eff.is_polymorphic t_eff then is_polymorphic := true in
let c_eff = GetEff.clock node_id_solver vi.it in
let vi_eff = {
var_name_eff = vi.it.var_name;
var_nature_eff = vi.it.var_nature;
var_number_eff = vi.it.var_number;
var_type_eff = t_eff;
var_clock_eff = c_eff;
}
in
Hashtbl.add local_env.lenv_types id t_eff;
Hashtbl.add local_env.lenv_vars id vi_eff;
vi_eff
in
let (sort_vars : Ident.t list -> Ident.t list) =
fun l ->
(* I cannot use List.sort as I only have a partial order on vars
-> hence I perform a topological sort *)
Erwan Jahier
committed
match (find_var_info lxm vars v1).it.var_clock with
| NamedClock({it=(_,v1clk)}) -> v1clk = v2 || depends_on v1clk v2
in
let rec aux acc l = match l with
| [] -> acc
| v::tail -> (
Erwan Jahier
committed
match (find_var_info lxm vars v).it.var_clock with
| Base ->
if List.mem v acc then
aux acc tail
else
aux (v::acc) tail
| NamedClock( { it=(_,v2) ; src=lxm }) ->
if List.mem v2 acc then
aux (v::acc) tail
else if
depends_on v2 v
then
raise (
Compile_error (
lxm,
"\n*** Clock dependency loop: " ^
(Ident.to_string v) ^ " depends on " ^
(Ident.to_string v2) ^ ", which depends on " ^
(Ident.to_string v))
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
else
let l1,l2 = List.partition (fun v -> v=v2) l in
if l1 = [] then
(* v depends on a clock not in l *)
aux (v::acc) tail
else
aux acc (v2::l2)
)
in
List.rev(aux [] l)
in
let vars_in_sorted = sort_vars vars.inlist
and vars_out_sorted = sort_vars vars.outlist in
let inlist = List.map type_args vars_in_sorted
and outlist = List.map type_args vars_out_sorted
and loclist =
match vars.loclist with
| None -> None
| Some loclist ->
let vars_loc_sorted = sort_vars loclist in
Some (List.map type_args vars_loc_sorted)
in
let unsort l_id l_vi =
let tab = List.map (fun vi -> vi.var_name_eff, vi) l_vi in
try List.map (fun id -> List.assoc id tab) l_id
with Not_found -> assert false
in
let inlist2 = unsort vars.inlist inlist
and outlist2 = unsort vars.outlist outlist in
{
node_key_eff = nk;
inlist_eff = inlist2;
outlist_eff = outlist2;
loclist_eff = loclist;
def_eff = node_def_eff ();
has_mem_eff = node_def.it.has_mem;
is_safe_eff = node_def.it.is_safe;
Erwan Jahier
committed
is_polym_eff = !is_polymorphic
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:
node alias_node(ins) returns (outs);
let
outs = aliased_node(ins);
tel
When instanciating models with polymorphic operators, it
may happen that some exported user nodes become
polymorphic (via node alias precisely). But in that case,
a non-polymorphic profile is given in the package provided
part. In such a case, we can use the types of the provided
part (itl and otl) instead of the polymorphic ones.
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
let (il,ol) = Eff.profile_of_node_exp aliased_node in
let (il_decl, ol_decl) =
match vars_opt with
| None -> (il,ol) (* no type profile is declared; we use the alias one *)
| Some vars ->
(* a type profile is declared; let's check there are compatible *)
let vi_il, vi_ol =
List.map (fun id -> find_var_info lxm vars id) vars.inlist,
List.map (fun id -> find_var_info lxm vars id) vars.outlist
in
let aux vi = GetEff.typ node_id_solver vi.it.var_type in
let (il_decl, ol_decl) = List.map aux vi_il, List.map aux vi_ol in
let i_unif_res = UnifyType.f il_decl il
and o_unif_res = UnifyType.f ol_decl ol
in
(match i_unif_res with
| UnifyType.Ko msg -> raise(Compile_error(lxm, msg))
| UnifyType.Equal -> ()
| UnifyType.Unif t -> GetEff.dump_polymorphic_nodes t
);
(match o_unif_res with
| UnifyType.Ko msg -> raise(Compile_error (lxm, msg))
| UnifyType.Equal -> ()
| UnifyType.Unif t -> GetEff.dump_polymorphic_nodes t
);
(* ok, there are compatible. We use the declared profile. *)
(il_decl, ol_decl)
in
let instanciate_var_info vi t = { vi with var_type_eff = t } in
let vil = List.map2 instanciate_var_info aliased_node.inlist_eff il_decl
and vol = List.map2 instanciate_var_info aliased_node.outlist_eff ol_decl in
let (outs:Eff.left list) = List.map (fun vi -> LeftVarEff (vi, lxm)) vol in
Erwan Jahier
committed
let tl = List.map Eff.type_of_left outs in
let cl = List.map (fun l -> (Eff.var_info_of_left l).var_clock_eff) outs in
let (aliased_node_call : Eff.val_exp) =
{ core =
CallByPosEff(
(Lxm.flagit (Eff.CALL(Lxm.flagit aliased_node lxm)) lxm,
OperEff
(List.map
(fun vi -> (* build operands*)
let ve = {
typ = [vi.var_type_eff];
clk = [snd vi.var_clock_eff];
core = CallByPosEff(
Lxm.flagit (Eff.IDENT(
Ident.to_idref vi.var_name_eff)) lxm, OperEff [])}
in
ve
)
vil)));
typ = tl;
clk = List.map snd cl;
}
in
inlist_eff = vil;
outlist_eff = vol;
loclist_eff = None;
def_eff = BodyEff(
{ asserts_eff = [];
eqs_eff = [Lxm.flagit (outs, aliased_node_call) lxm]
});