From 333e3a25e7862b51b01a590fd526c0a5dc7b18fa Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Mon, 18 Dec 2017 09:57:21 +0100
Subject: [PATCH] [general] Refactor get_node_eqs to produce (eqs, auts) with
automatons
---
src/access.ml | 4 +-
src/algebraicLoop.ml | 5 +-
src/causality.ml | 43 ++++--
src/clock_calculus.ml | 16 +-
src/clocks.ml | 32 +++-
src/corelang.ml | 343 ++++++++++++++++++++++++++----------------
src/corelang.mli | 13 +-
src/dimension.ml | 10 +-
src/inliner.ml | 168 +++++++++++----------
src/machine_code.ml | 8 +-
src/mpfr.ml | 6 +-
src/mutation.ml | 6 +-
src/normalization.ml | 4 +-
src/printers.ml | 3 +-
src/stateless.ml | 6 +-
src/types.ml | 1 +
src/typing.ml | 6 +-
17 files changed, 428 insertions(+), 246 deletions(-)
diff --git a/src/access.ml b/src/access.ml
index 0797d42e..a3754a08 100755
--- a/src/access.ml
+++ b/src/access.ml
@@ -80,7 +80,9 @@ let check_node nd =
let checks =
List.fold_left check_var_decl checks (get_node_vars nd) in
let checks =
- List.fold_left (fun checks eq -> check_expr checks eq.eq_rhs) checks (get_node_eqs nd) in
+ let eqs, auts = get_node_eqs nd in
+ assert (auts = []); (* Not checking automata yet . *)
+ List.fold_left (fun checks eq -> check_expr checks eq.eq_rhs) checks eqs in
nd.node_checks <- CSet.elements checks
let check_top_decl decl =
diff --git a/src/algebraicLoop.ml b/src/algebraicLoop.ml
index f863bb7e..36ca3590 100644
--- a/src/algebraicLoop.ml
+++ b/src/algebraicLoop.ml
@@ -43,8 +43,9 @@ struct
let resolve node partition : call list =
let partition = ISet.of_list partition in
(* Preprocessing calls: associate to each of them the eq.lhs associated *)
- let eqs = get_node_eqs node in
- let calls_expr = Causality.NodeDep.get_calls (fun _ -> true) eqs in
+ let calls_expr = Causality.NodeDep.get_calls (fun _ -> true) node in
+ let eqs, auts = get_node_eqs node in
+ assert (auts = []); (* TODO voir si on peut acceder directement aux eqs qui font les calls *)
let calls = List.map (
fun expr ->
let eq = List.find (fun eq ->
diff --git a/src/causality.ml b/src/causality.ml
index 447b464e..7e7a42cc 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -88,8 +88,14 @@ let add_vertices vtc g =
let new_graph () =
IdentDepGraph.create ()
+
module ExprDep = struct
-
+ let get_node_eqs nd =
+ let eqs, auts = get_node_eqs nd in
+ if auts != [] then assert false (* No call on causality on a Lustre model
+ with automaton. They should be expanded by now. *);
+ eqs
+
let instance_var_cpt = ref 0
(* read vars represent input/mem read-only vars,
@@ -317,12 +323,27 @@ module NodeDep = struct
| Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
| _ -> None
- let get_calls prednode eqs =
- let deps =
- List.fold_left
- (fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
- ESet.empty
- eqs in
+ let get_calls prednode nd =
+ let accu f init objl = List.fold_left (fun accu o -> ESet.union accu (f o)) init objl in
+ let get_eq_calls eq = get_expr_calls prednode eq.eq_rhs in
+ let rec get_stmt_calls s =
+ match s with Eq eq -> get_eq_calls eq | Aut aut -> get_aut_calls aut
+ and get_aut_calls aut =
+ let get_handler_calls h =
+ let get_cond_calls c = accu (fun (_,e,_,_) -> get_expr_calls prednode e) ESet.empty c in
+ let until = get_cond_calls h.hand_until in
+ let unless = get_cond_calls h.hand_unless in
+ let calls = ESet.union until unless in
+ let calls = accu get_stmt_calls calls h.hand_stmts in
+ let calls = accu (fun a -> get_expr_calls prednode a.assert_expr) calls h.hand_asserts in
+ (* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *)
+ calls
+ in
+ accu get_handler_calls ESet.empty aut.aut_handlers
+ in
+ let eqs, auts = get_node_eqs nd in
+ let deps = accu get_eq_calls ESet.empty eqs in
+ let deps = accu get_aut_calls deps auts in
ESet.elements deps
let dependence_graph prog =
@@ -335,7 +356,7 @@ module NodeDep = struct
let accu = add_vertices [nd.node_id] accu in
let deps = List.map
(fun e -> fst (desome (get_callee e)))
- (get_calls (fun _ -> true) (get_node_eqs nd))
+ (get_calls (fun _ -> true) nd)
in
(* Adding assert expressions deps *)
let deps_asserts =
@@ -378,7 +399,7 @@ module NodeDep = struct
match td.top_decl_desc with
| Node nd ->
let prednode n = is_generic_node (Hashtbl.find node_table n) in
- nd.node_gencalls <- get_calls prednode (get_node_eqs nd)
+ nd.node_gencalls <- get_calls prednode nd
| _ -> ()
) prog
@@ -459,7 +480,9 @@ module CycleDetection = struct
- a modified acyclic version of [g]
*)
let break_cycles node mems g =
- let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) (get_node_eqs node) in
+ let eqs , auts = get_node_eqs node in
+ assert (auts = []); (* TODO: check: For the moment we assume that auts are expanded by now *)
+ let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) eqs in
let rec break vdecls mem_eqs g =
let scc_l = Cycles.scc_list g in
let wrong = List.filter (wrong_partition g) scc_l in
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index 6c368487..e585db3b 100755
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -681,7 +681,9 @@ let clock_node env loc nd =
let new_env = clock_var_decl_list env false nd.node_inputs in
let new_env = clock_var_decl_list new_env true nd.node_outputs in
let new_env = clock_var_decl_list new_env true nd.node_locals in
- List.iter (clock_eq new_env) (get_node_eqs nd);
+ let eqs, auts = get_node_eqs nd in (* TODO XXX: perform the clocking on auts.
+ For the moment, it is ignored *)
+ List.iter (clock_eq new_env) eqs;
let ck_ins = clock_of_vlist nd.node_inputs in
let ck_outs = clock_of_vlist nd.node_outputs in
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
@@ -690,14 +692,14 @@ let clock_node env loc nd =
(* Local variables may contain first-order carrier variables that should be generalized.
That's not the case for types. *)
try_generalize ck_node loc;
-(*
- List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;
- List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*)
+ (*
+ List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;
+ List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*)
(*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*)
(* TODO : Xavier pourquoi ai je cette erreur ? *)
-(* if (is_main && is_polymorphic ck_node) then
- raise (Error (loc,(Cannot_be_polymorphic ck_node)));
-*)
+ (* if (is_main && is_polymorphic ck_node) then
+ raise (Error (loc,(Cannot_be_polymorphic ck_node)));
+ *)
Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
nd.node_clock <- ck_node;
Env.add_value env nd.node_id ck_node
diff --git a/src/clocks.ml b/src/clocks.ml
index 8756e247..c148d482 100755
--- a/src/clocks.ml
+++ b/src/clocks.ml
@@ -33,7 +33,7 @@ and carrier_expr =
{mutable carrier_desc: carrier_desc;
mutable carrier_scoped: bool;
carrier_id: int}
-
+
type clock_expr =
{mutable cdesc: clock_desc;
mutable cscoped: bool;
@@ -422,6 +422,36 @@ let uneval const cr =
| Carry_name -> cr.carrier_desc <- Carry_const const
| _ -> assert false
+
+(* Used in rename functions in Corelang. We have to propagate the renaming to
+ ids of variables clocking the signals *)
+
+(* Carrier are not renamed. They corresponds to enumerated type constants *)
+(*
+let rec rename_carrier f c =
+ { c with carrier_desc = rename_carrier_desc fvar c.carrier_desc }
+and rename_carrier_desc f
+let re = rename_carrier f
+ match cd with
+ | Carry_const id -> Carry_const (f id)
+ | Carry_link ce -> Carry_link (re ce)
+ | _ -> cd
+*)
+
+
+let rec rename_clock_expr fvar c =
+ { c with cdesc = rename_clock_desc fvar c.cdesc }
+and rename_clock_desc fvar cd =
+ let re = rename_clock_expr fvar in
+ match cd with
+ | Carrow (c1, c2) -> Carrow (re c1, re c2)
+ | Ctuple cl -> Ctuple (List.map re cl)
+ | Con (c1, car, id) -> Con (re c1, car, fvar id)
+ | Cvar
+ | Cunivar -> cd
+ | Clink c -> Clink (re c)
+ | Ccarrying (car, c) -> Ccarrying (car, re c)
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/corelang.ml b/src/corelang.ml
index 3f335713..8446d910 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -130,7 +130,17 @@ let consts_of_enum_type top_decl =
match top_decl.top_decl_desc with
| TypeDef tdef ->
(match tdef.tydef_desc with
- | Tydec_enum tags -> List.map (fun tag -> let cdecl = { const_id = tag; const_loc = top_decl.top_decl_loc; const_value = Const_tag tag; const_type = Type_predef.type_const tdef.tydef_id } in { top_decl with top_decl_desc = Const cdecl }) tags
+ | Tydec_enum tags ->
+ List.map
+ (fun tag ->
+ let cdecl = {
+ const_id = tag;
+ const_loc = top_decl.top_decl_loc;
+ const_value = Const_tag tag;
+ const_type = Type_predef.type_const tdef.tydef_id
+ } in
+ { top_decl with top_decl_desc = Const cdecl })
+ tags
| _ -> [])
| _ -> assert false
@@ -538,16 +548,17 @@ let get_node_var id node =
(* Format.eprintf "Unable to find variable %s in node %s@.@?" id node.node_id; *)
raise Not_found
end
-
+
+
let get_node_eqs =
let get_eqs stmts =
List.fold_right
- (fun stmt res ->
+ (fun stmt (res_eq, res_aut) ->
match stmt with
- | Eq eq -> eq :: res
- | Aut _ -> assert false)
+ | Eq eq -> eq :: res_eq, res_aut
+ | Aut aut -> res_eq, aut::res_aut)
stmts
- [] in
+ ([], []) in
let table_eqs = Hashtbl.create 23 in
(fun nd ->
try
@@ -561,8 +572,12 @@ let get_node_eqs =
end)
let get_node_eq id node =
- List.find (fun eq -> List.mem id eq.eq_lhs) (get_node_eqs node)
-
+ let eqs, auts = get_node_eqs node in
+ try
+ List.find (fun eq -> List.mem id eq.eq_lhs) eqs
+ with
+ Not_found -> (* Shall be defined in automata auts *) raise Not_found
+
let get_nodes prog =
List.fold_left (
fun nodes decl ->
@@ -630,70 +645,34 @@ let rec rename_carrier rename cck =
| Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
| _ -> cck
-(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
+ (*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
(* applies the renaming function [fvar] to all variables of expression [expr] *)
- let rec expr_replace_var fvar expr =
- { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
-
- and expr_desc_replace_var fvar expr_desc =
- match expr_desc with
- | Expr_const _ -> expr_desc
- | Expr_ident i -> Expr_ident (fvar i)
- | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el)
- | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d)
- | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d)
- | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el)
- | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)
- | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2)
- | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)
- | Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
- | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
- | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
- | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i')
-
-(* Applies the renaming function [fvar] to every rhs
- only when the corresponding lhs satisfies predicate [pvar] *)
- let eq_replace_rhs_var pvar fvar eq =
- let pvar l = List.exists pvar l in
- let rec replace lhs rhs =
- { rhs with expr_desc =
- match lhs with
- | [] -> assert false
- | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs.expr_desc else rhs.expr_desc
- | _ ->
- (match rhs.expr_desc with
- | Expr_tuple tl ->
- Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
- | Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs ->
- let args = expr_list_of_expr arg in
- Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
- | Expr_array _
- | Expr_access _
- | Expr_power _
- | Expr_const _
- | Expr_ident _
- | Expr_appl _ ->
- if pvar lhs
- then expr_desc_replace_var fvar rhs.expr_desc
- else rhs.expr_desc
- | Expr_ite (c, t, e) -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
- | Expr_arrow (e1, e2) -> Expr_arrow (replace lhs e1, replace lhs e2)
- | Expr_fby (e1, e2) -> Expr_fby (replace lhs e1, replace lhs e2)
- | Expr_pre e' -> Expr_pre (replace lhs e')
- | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
- in Expr_when (replace lhs e', i', l)
- | Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i
- in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
- )
- }
- in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
+ (* let rec expr_replace_var fvar expr = *)
+ (* { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc } *)
-
- let rec rename_expr f_node f_var f_const expr =
- { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
- and rename_expr_desc f_node f_var f_const expr_desc =
- let re = rename_expr f_node f_var f_const in
+ (* and expr_desc_replace_var fvar expr_desc = *)
+ (* match expr_desc with *)
+ (* | Expr_const _ -> expr_desc *)
+ (* | Expr_ident i -> Expr_ident (fvar i) *)
+ (* | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el) *)
+ (* | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d) *)
+ (* | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d) *)
+ (* | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el) *)
+ (* | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e) *)
+ (* | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) *)
+ (* | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2) *)
+ (* | Expr_pre e' -> Expr_pre (expr_replace_var fvar e') *)
+ (* | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) *)
+ (* | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) *)
+ (* | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i') *)
+
+
+
+ let rec rename_expr f_node f_var expr =
+ { expr with expr_desc = rename_expr_desc f_node f_var expr.expr_desc }
+ and rename_expr_desc f_node f_var expr_desc =
+ let re = rename_expr f_node f_var in
match expr_desc with
| Expr_const _ -> expr_desc
| Expr_ident i -> Expr_ident (f_var i)
@@ -710,61 +689,114 @@ let rec rename_carrier rename cck =
Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
| Expr_appl (i, e', i') ->
Expr_appl (f_node i, re e', Utils.option_map re i')
-
- let rename_node_annot f_node f_var f_const expr =
- expr
- (* TODO assert false *)
-
- let rename_expr_annot f_node f_var f_const annot =
- annot
- (* TODO assert false *)
-
-let rename_node f_node f_var f_const nd =
- let rename_var v = { v with var_id = f_var v.var_id } in
- let rename_eq eq = { eq with
- eq_lhs = List.map f_var eq.eq_lhs;
- eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
- }
- in
- let inputs = List.map rename_var nd.node_inputs in
- let outputs = List.map rename_var nd.node_outputs in
- let locals = List.map rename_var nd.node_locals in
- let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
- let node_checks = List.map (Dimension.expr_replace_var f_var) nd.node_checks in
- let node_asserts = List.map
- (fun a ->
- {a with assert_expr =
- let expr = a.assert_expr in
- rename_expr f_node f_var f_const expr})
- nd.node_asserts
- in
- let node_stmts = List.map (fun eq -> Eq (rename_eq eq)) (get_node_eqs nd) in
- let spec =
- Utils.option_map
- (fun s -> rename_node_annot f_node f_var f_const s)
- nd.node_spec
- in
- let annot =
- List.map
- (fun s -> rename_expr_annot f_node f_var f_const s)
- nd.node_annot
- in
- {
- node_id = f_node nd.node_id;
- node_type = nd.node_type;
- node_clock = nd.node_clock;
- node_inputs = inputs;
- node_outputs = outputs;
- node_locals = locals;
- node_gencalls = gen_calls;
- node_checks = node_checks;
- node_asserts = node_asserts;
- node_stmts = node_stmts;
- node_dec_stateless = nd.node_dec_stateless;
- node_stateless = nd.node_stateless;
- node_spec = spec;
- node_annot = annot;
- }
+
+ let rename_dec_type f_node f_var t = assert false (*
+ Types.rename_dim_type (Dimension.rename f_node f_var) t*)
+
+ let rename_dec_clock f_node f_var c = assert false (*
+ Clocks.rename_clock_expr f_var c*)
+
+ let rename_var f_node f_var v = {
+ v with
+ var_id = f_var v.var_id;
+ var_dec_type = rename_dec_type f_node f_var v.var_type;
+ var_dec_clock = rename_dec_clock f_node f_var v.var_clock
+ }
+
+ let rename_vars f_node f_var = List.map (rename_var f_node f_var)
+
+ let rec rename_eq f_node f_var eq = { eq with
+ eq_lhs = List.map f_var eq.eq_lhs;
+ eq_rhs = rename_expr f_node f_var eq.eq_rhs
+ }
+ and rename_handler f_node f_var h = {h with
+ hand_state = f_var h.hand_state;
+ hand_unless = List.map (
+ fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
+ ) h.hand_unless;
+ hand_until = List.map (
+ fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
+ ) h.hand_until;
+ hand_locals = rename_vars f_node f_var h.hand_locals;
+ hand_stmts = rename_stmts f_node f_var h.hand_stmts;
+ hand_annots = rename_annots f_node f_var h.hand_annots;
+
+ }
+ and rename_aut f_node f_var aut = { aut with
+ aut_id = f_var aut.aut_id;
+ aut_handlers = List.map (rename_handler f_node f_var) aut.aut_handlers;
+ }
+ and rename_stmts f_node f_var stmts = List.map (fun stmt -> match stmt with
+ | Eq eq -> Eq (rename_eq f_node f_var eq)
+ | Aut at -> Aut (rename_aut f_node f_var at))
+ stmts
+ and rename_annotl f_node f_var annots =
+ List.map
+ (fun (key, value) -> key, rename_eexpr f_node f_var value)
+ annots
+ and rename_annot f_node f_var annot =
+ { annot with annots = rename_annotl f_node f_var annot.annots }
+ and rename_annots f_node f_var annots =
+ List.map (rename_annot f_node f_var) annots
+and rename_eexpr f_node f_var ee =
+ { ee with
+ eexpr_tag = Utils.new_tag ();
+ eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;
+ eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_node f_var vdecls) ee.eexpr_quantifiers;
+ eexpr_normalized = Utils.option_map
+ (fun (vdecl, eqs, vdecls) ->
+ rename_var f_node f_var vdecl,
+ List.map (rename_eq f_node f_var) eqs,
+ rename_vars f_node f_var vdecls
+ ) ee.eexpr_normalized;
+
+ }
+
+
+
+
+ let rename_node f_node f_var nd =
+ let rename_var = rename_var f_node f_var in
+ let rename_expr = rename_expr f_node f_var in
+ let rename_stmts = rename_stmts f_node f_var in
+ let inputs = List.map rename_var nd.node_inputs in
+ let outputs = List.map rename_var nd.node_outputs in
+ let locals = List.map rename_var nd.node_locals in
+ let gen_calls = List.map rename_expr nd.node_gencalls in
+ let node_checks = List.map (Dimension.rename f_node f_var) nd.node_checks in
+ let node_asserts = List.map
+ (fun a ->
+ {a with assert_expr =
+ let expr = a.assert_expr in
+ rename_expr expr})
+ nd.node_asserts
+ in
+ let node_stmts = rename_stmts nd.node_stmts
+
+
+ in
+ let spec =
+ Utils.option_map
+ (fun s -> assert false; (*rename_node_annot f_node f_var s*) ) (* TODO: implement! *)
+ nd.node_spec
+ in
+ let annot = rename_annots f_node f_var nd.node_annot in
+ {
+ node_id = f_node nd.node_id;
+ node_type = nd.node_type;
+ node_clock = nd.node_clock;
+ node_inputs = inputs;
+ node_outputs = outputs;
+ node_locals = locals;
+ node_gencalls = gen_calls;
+ node_checks = node_checks;
+ node_asserts = node_asserts;
+ node_stmts = node_stmts;
+ node_dec_stateless = nd.node_dec_stateless;
+ node_stateless = nd.node_stateless;
+ node_spec = spec;
+ node_annot = annot;
+ }
let rename_const f_const c =
@@ -780,7 +812,7 @@ let rename_prog f_node f_var f_const prog =
List.fold_left (fun accu top ->
(match top.top_decl_desc with
| Node nd ->
- { top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
+ { top with top_decl_desc = Node (rename_node f_node f_var nd) }
| Const c ->
{ top with top_decl_desc = Const (rename_const f_const c) }
| TypeDef tdef ->
@@ -791,6 +823,44 @@ let rename_prog f_node f_var f_const prog =
) [] prog
)
+(* Applies the renaming function [fvar] to every rhs
+ only when the corresponding lhs satisfies predicate [pvar] *)
+ let eq_replace_rhs_var pvar fvar eq =
+ let pvar l = List.exists pvar l in
+ let rec replace lhs rhs =
+ { rhs with expr_desc =
+ match lhs with
+ | [] -> assert false
+ | [_] -> if pvar lhs then rename_expr_desc (fun x -> x) fvar rhs.expr_desc else rhs.expr_desc
+ | _ ->
+ (match rhs.expr_desc with
+ | Expr_tuple tl ->
+ Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
+ | Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs ->
+ let args = expr_list_of_expr arg in
+ Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
+ | Expr_array _
+ | Expr_access _
+ | Expr_power _
+ | Expr_const _
+ | Expr_ident _
+ | Expr_appl _ ->
+ if pvar lhs
+ then rename_expr_desc (fun x -> x) fvar rhs.expr_desc
+ else rhs.expr_desc
+ | Expr_ite (c, t, e) -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
+ | Expr_arrow (e1, e2) -> Expr_arrow (replace lhs e1, replace lhs e2)
+ | Expr_fby (e1, e2) -> Expr_fby (replace lhs e1, replace lhs e2)
+ | Expr_pre e' -> Expr_pre (replace lhs e')
+ | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
+ in Expr_when (replace lhs e', i', l)
+ | Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i
+ in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
+ )
+ }
+ in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
+
+
(**********************************************************************)
(* Pretty printers *)
@@ -964,8 +1034,24 @@ let rec get_expr_calls nodes e =
and get_eq_calls nodes eq =
get_expr_calls nodes eq.eq_rhs
+and get_aut_handler_calls nodes h =
+ List.fold_left (fun accu stmt -> match stmt with
+ | Eq eq -> Utils.ISet.union (get_eq_calls nodes eq) accu
+ | Aut aut' -> Utils.ISet.union (get_aut_calls nodes aut') accu
+ ) Utils.ISet.empty h.hand_stmts
+and get_aut_calls nodes aut =
+ List.fold_left (fun accu h -> Utils.ISet.union (get_aut_handler_calls nodes h) accu)
+ Utils.ISet.empty aut.aut_handlers
and get_node_calls nodes node =
- List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node)
+ let eqs, auts = get_node_eqs node in
+ let aut_calls =
+ List.fold_left
+ (fun accu aut -> Utils.ISet.union (get_aut_calls nodes aut) accu)
+ Utils.ISet.empty auts
+ in
+ List.fold_left
+ (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu)
+ aut_calls eqs
let get_expr_vars e =
let rec get_expr_vars vars e =
@@ -1010,8 +1096,11 @@ and expr_desc_has_arrows expr_desc =
and eq_has_arrows eq =
expr_has_arrows eq.eq_rhs
+and aut_has_arrows aut = List.exists (fun h -> List.exists (fun stmt -> match stmt with Eq eq -> eq_has_arrows eq | Aut aut' -> aut_has_arrows aut') h.hand_stmts ) aut.aut_handlers
and node_has_arrows node =
- List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node)
+ let eqs, auts = get_node_eqs node in
+ List.exists (fun eq -> eq_has_arrows eq) eqs || List.exists (fun aut -> aut_has_arrows aut) auts
+
let copy_var_decl vdecl =
diff --git a/src/corelang.mli b/src/corelang.mli
index ea020ab9..17726b40 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -75,7 +75,7 @@ val const_impl: constant -> constant -> constant
val get_node_vars: node_desc -> var_decl list
val get_node_var: ident -> node_desc -> var_decl
-val get_node_eqs: node_desc -> eq list
+val get_node_eqs: node_desc -> eq list * automata_desc list
val get_node_eq: ident -> node_desc -> eq
val get_node_interface: node_desc -> imported_node_desc
@@ -124,10 +124,17 @@ val rename_static: (ident -> Dimension.dim_expr) -> type_dec_desc -> type_dec_de
val rename_carrier: (ident -> ident) -> clock_dec_desc -> clock_dec_desc
val get_expr_vars: expr -> Utils.ISet.t
-val expr_replace_var: (ident -> ident) -> expr -> expr
+(*val expr_replace_var: (ident -> ident) -> expr -> expr*)
+
val eq_replace_rhs_var: (ident -> bool) -> (ident -> ident) -> eq -> eq
-(** rename_prog f_node f_var f_const prog *)
+(** val rename_expr f_node f_var expr *)
+val rename_expr : (ident -> ident) -> (ident -> ident) -> expr -> expr
+(** val rename_eq f_node f_var eq *)
+val rename_eq : (ident -> ident) -> (ident -> ident) -> eq -> eq
+(** val rename_aut f_node f_var aut *)
+val rename_aut : (ident -> ident) -> (ident -> ident) -> automata_desc -> automata_desc
+(** rename_prog f_node f_var prog *)
val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program -> program
val substitute_expr: var_decl list -> eq list -> expr -> expr
diff --git a/src/dimension.ml b/src/dimension.ml
index ec0b2f26..4a46d85a 100644
--- a/src/dimension.ml
+++ b/src/dimension.ml
@@ -338,17 +338,17 @@ let unify ?(semi=false) dim1 dim2 =
| _ -> raise (Unify (dim1, dim2))
in unif dim1 dim2
-let rec expr_replace_var fvar e =
- { e with dim_desc = expr_replace_var_desc fvar e.dim_desc }
-and expr_replace_var_desc fvar e =
- let re = expr_replace_var fvar in
+let rec rename fnode fvar e =
+ { e with dim_desc = expr_replace_var_desc fnode fvar e.dim_desc }
+and expr_replace_var_desc fnode fvar e =
+ let re = rename fnode fvar in
match e with
| Dvar
| Dunivar
| Dbool _
| Dint _ -> e
| Dident v -> Dident (fvar v)
- | Dappl (id, el) -> Dappl (id, List.map re el)
+ | Dappl (id, el) -> Dappl (fnode id, List.map re el)
| Dite (g,t,e) -> Dite (re g, re t, re e)
| Dlink e -> Dlink (re e)
diff --git a/src/inliner.ml b/src/inliner.ml
index 0aab3f3d..33935a03 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -32,14 +32,15 @@ let is_node_var node v =
ignore (Corelang.get_node_var v node); true
with Not_found -> false
-let rename_expr rename expr = expr_replace_var rename expr
-
+(* let rename_expr rename expr = expr_replace_var rename expr *)
+(*
let rename_eq rename eq =
{ eq with
eq_lhs = List.map rename eq.eq_lhs;
eq_rhs = rename_expr rename eq.eq_rhs
}
-
+*)
+
let rec add_expr_reset_cond cond expr =
let aux = add_expr_reset_cond cond in
let new_desc =
@@ -113,7 +114,9 @@ let inline_call node loc uid args reset locals caller =
if v = tag_true || v = tag_false || not (is_node_var node v) then v else
Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
in
- let eqs' = List.map (rename_eq rename) (get_node_eqs node) in
+ let eqs, auts = get_node_eqs node in
+ let eqs' = List.map (rename_eq (fun x -> x) rename) eqs in
+ let auts' = List.map (rename_aut (fun x -> x) rename) auts in
let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in
let static_inputs, dynamic_inputs = List.partition (fun (vdecl, arg) -> vdecl.var_dec_const) input_arg_list in
let static_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) static_inputs in
@@ -134,7 +137,7 @@ let inline_call node loc uid args reset locals caller =
{ v.var_dec_type with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc },
{ v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc },
v.var_dec_const,
- Utils.option_map (rename_expr rename) v.var_dec_value) in
+ Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value) in
begin
(*
(try
@@ -162,13 +165,17 @@ in
assert (node.node_gencalls = []);
(* Expressing reset locally in equations *)
- let eqs_r' =
+ let eqs_r' =
+ let all_eqs = (List.map (fun eq -> Eq eq) eqs') @ (List.map (fun aut -> Aut aut) auts') in
match reset with
- None -> eqs'
- | Some cond -> List.map (add_eq_reset_cond cond) eqs'
+ None -> all_eqs
+ | Some cond -> (
+ assert (auts' = []); (* TODO: we do not handle properly automaton in case of reset call *)
+ List.map (fun eq -> Eq (add_eq_reset_cond cond eq)) eqs'
+ )
in
- let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs',
- expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in
+ let assign_inputs = Eq (mkeq loc (List.map (fun v -> v.var_id) inputs',
+ expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs))) in
let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
in
let asserts' = (* We rename variables in assert expressions *)
@@ -176,7 +183,7 @@ in
(fun a ->
{a with assert_expr =
let expr = a.assert_expr in
- rename_expr rename expr
+ rename_expr (fun x -> x) rename expr
})
node.node_asserts
in
@@ -224,91 +231,94 @@ let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
match expr.expr_desc with
| Expr_appl (id, args, reset) ->
- let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in
- if List.exists (check_node_name id) nodes && (* the current node call is provided
- as arguments nodes *)
- (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated,
- it is explicitely inlined here *)
- then (
- (* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *)
- (* The node should be inlined *)
- (* let _ = Format.eprintf "Inlining call to %s@." id in *)
- let called = try List.find (check_node_name id) nodes
- with Not_found -> (assert false) in
- let called = node_of_top called in
- let called' = inline_node called nodes in
- let expr, locals', eqs'', asserts'', annots'' =
- inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
- expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
- )
- else
- (* let _ = Format.eprintf "Not inlining call to %s@." id in *)
- { expr with expr_desc = Expr_appl(id, args', reset)},
- locals',
- eqs',
- asserts',
- annots'
+ let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in
+ if List.exists (check_node_name id) nodes && (* the current node call is provided
+ as arguments nodes *)
+ (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated,
+ it is explicitely inlined here *)
+ then (
+ (* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *)
+ (* The node should be inlined *)
+ (* let _ = Format.eprintf "Inlining call to %s@." id in *)
+ let called = try List.find (check_node_name id) nodes
+ with Not_found -> (assert false) in
+ let called = node_of_top called in
+ let called' = inline_node called nodes in
+ let expr, locals', eqs'', asserts'', annots'' =
+ inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
+ expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
+ )
+ else
+ (* let _ = Format.eprintf "Not inlining call to %s@." id in *)
+ { expr with expr_desc = Expr_appl(id, args', reset)},
+ locals',
+ eqs',
+ asserts',
+ annots'
(* For other cases, we just keep the structure, but convert sub-expressions *)
| Expr_const _
| Expr_ident _ -> expr, locals, [], [], []
| Expr_tuple el ->
- let el', l', eqs', asserts', annots' = inline_tuple el in
- { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'
+ let el', l', eqs', asserts', annots' = inline_tuple el in
+ { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'
| Expr_ite (g, t, e) ->
- let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in
- { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots'
+ let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in
+ { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots'
| Expr_arrow (e1, e2) ->
- let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
- { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots'
+ let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
+ { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots'
| Expr_fby (e1, e2) ->
- let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
- { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots'
+ let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
+ { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots'
| Expr_array el ->
- let el', l', eqs', asserts', annots' = inline_tuple el in
- { expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'
+ let el', l', eqs', asserts', annots' = inline_tuple el in
+ { expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'
| Expr_access (e, dim) ->
- let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
- { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots'
+ let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
+ { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots'
| Expr_power (e, dim) ->
- let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
- { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots'
+ let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
+ { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots'
| Expr_pre e ->
- let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
- { expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots'
+ let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
+ { expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots'
| Expr_when (e, id, label) ->
- let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
- { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots'
+ let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
+ { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots'
| Expr_merge (id, branches) ->
- let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in
- let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
- { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots'
+ let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in
+ let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
+ { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots'
and inline_node ?(selection_on_annotation=false) node nodes =
try copy_node (Hashtbl.find inline_table node.node_id)
with Not_found ->
- let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
- let new_locals, eqs, asserts, annots =
- List.fold_left (fun (locals, eqs, asserts, annots) eq ->
- let eq_rhs', locals', new_eqs', asserts', annots' =
- inline_expr eq.eq_rhs locals node nodes
- in
- locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts, annots'@annots
- ) (node.node_locals, [], node.node_asserts, node.node_annot) (get_node_eqs node)
- in
- let inlined =
- { node with
- node_locals = new_locals;
- node_stmts = List.map (fun eq -> Eq eq) eqs;
- node_asserts = asserts;
- node_annot = annots;
- }
- in
- begin
- (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
- Hashtbl.add inline_table node.node_id inlined;
- inlined
- end
+ let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
+ let eqs, auts = get_node_eqs node in
+ assert (auts = []); (* No inlining of automaton yet. One should visit each
+ handler eqs and perform similar computation *)
+ let new_locals, stmts, asserts, annots =
+ List.fold_left (fun (locals, stmts, asserts, annots) eq ->
+ let eq_rhs', locals', new_stmts', asserts', annots' =
+ inline_expr eq.eq_rhs locals node nodes
+ in
+ locals', Eq { eq with eq_rhs = eq_rhs' }::new_stmts'@stmts, asserts'@asserts, annots'@annots
+ ) (node.node_locals, [], node.node_asserts, node.node_annot) eqs
+ in
+ let inlined =
+ { node with
+ node_locals = new_locals;
+ node_stmts = stmts;
+ node_asserts = asserts;
+ node_annot = annots;
+ }
+ in
+ begin
+ (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
+ Hashtbl.add inline_table node.node_id inlined;
+ inlined
+ end
let inline_all_calls node nodes =
let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
@@ -333,7 +343,7 @@ let witness filename main_name orig inlined type_env clock_env =
let inlined_rename = rename_local_node inlined "inlined_" in
let identity = (fun x -> x) in
let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in
- let orig = rename_prog orig_rename identity identity orig in
+ let orig = rename_prog orig_rename (* f_node *) identity (* f_var *) identity (* f_const *) orig in
let inlined = rename_prog inlined_rename identity identity inlined in
let nodes_origs, others = List.partition is_node orig in
let nodes_inlined, _ = List.partition is_node inlined in
diff --git a/src/machine_code.ml b/src/machine_code.ml
index eca08aec..7288d6ac 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -555,7 +555,9 @@ let sort_equations_from_schedule nd sch =
(* Format.eprintf "%s schedule: %a@." *)
(* nd.node_id *)
(* (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch; *)
- let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in
+ let eqs, auts = get_node_eqs nd in
+ assert (auts = []); (* Automata should be expanded by now *)
+ let split_eqs = Splitting.tuple_split_eq_list eqs in
let eqs_rev, remainder =
List.fold_left
(fun (accu, node_eqs_remainder) vl ->
@@ -571,9 +573,11 @@ let sort_equations_from_schedule nd sch =
in
begin
if List.length remainder > 0 then (
+ let eqs, auts = get_node_eqs nd in
+ assert (auts = []); (* Automata should be expanded by now *)
Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?"
Printers.pp_node_eqs remainder
- Printers.pp_node_eqs (get_node_eqs nd);
+ Printers.pp_node_eqs eqs;
assert false);
List.rev eqs_rev
end
diff --git a/src/mpfr.ml b/src/mpfr.ml
index d310936c..ddf1dec5 100755
--- a/src/mpfr.ml
+++ b/src/mpfr.ml
@@ -221,8 +221,10 @@ let inject_node node =
let is_local v =
List.for_all ((!=) v) inputs_outputs in
let orig_vars = inputs_outputs@node.node_locals in
- let defs, vars =
- List.fold_left (inject_eq node) ([], orig_vars) (get_node_eqs node) in
+ let defs, vars =
+ let eqs, auts = get_node_eqs node in
+ if auts != [] then assert false; (* Automata should be expanded by now. *)
+ List.fold_left (inject_eq node) ([], orig_vars) eqs in
(* Normalize the asserts *)
let vars, assert_defs, asserts =
List.fold_left (
diff --git a/src/mutation.ml b/src/mutation.ml
index a907de23..f5a94911 100644
--- a/src/mutation.ml
+++ b/src/mutation.ml
@@ -103,8 +103,10 @@ let rec compute_records_expr expr =
let compute_records_eq eq = compute_records_expr eq.eq_rhs
-let compute_records_node nd =
- merge_records (List.map compute_records_eq (get_node_eqs nd))
+let compute_records_node nd =
+ let eqs, auts = get_node_eqs nd in
+ assert (auts=[]); (* Automaton should be expanded by now *)
+ merge_records (List.map compute_records_eq eqs)
let compute_records_top_decl td =
match td.top_decl_desc with
diff --git a/src/normalization.ml b/src/normalization.ml
index 7cdb1a6a..ccc8d8d5 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -399,7 +399,9 @@ let normalize_node node =
List.for_all ((!=) v) inputs_outputs in
let orig_vars = inputs_outputs@node.node_locals in
let defs, vars =
- List.fold_left (normalize_eq node) ([], orig_vars) (get_node_eqs node) in
+ let eqs, auts = get_node_eqs node in
+ if auts != [] then assert false; (* Automata should be expanded by now. *)
+ List.fold_left (normalize_eq node) ([], orig_vars) eqs in
(* Normalize the asserts *)
let vars, assert_defs, asserts =
List.fold_left (
diff --git a/src/printers.ml b/src/printers.ml
index 3b02fb91..5c1282fb 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -332,7 +332,8 @@ let pp_decl fmt decl =
| TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
let pp_prog fmt prog =
- (* we first print types *)
+ (* we first print types: the function SortProg.sort could do the job but ut
+ introduces a cyclic dependance *)
let type_decl, others =
List.partition (fun decl -> match decl.top_decl_desc with TypeDef _ -> true | _ -> false) prog
in
diff --git a/src/stateless.ml b/src/stateless.ml
index 10acf40c..eee1401b 100755
--- a/src/stateless.ml
+++ b/src/stateless.ml
@@ -36,8 +36,10 @@ let rec check_expr expr =
| Expr_appl (i, e', i') ->
check_expr e' &&
(Basic_library.is_stateless_fun i || check_node (node_from_name i))
-and compute_node nd =
- List.for_all (fun eq -> check_expr eq.eq_rhs) (get_node_eqs nd)
+and compute_node nd = (* returns true iff the node is stateless.*)
+ let eqs, aut = get_node_eqs nd in
+ aut = [] && (* A node containinig an automaton will be stateful *)
+ List.for_all (fun eq -> check_expr eq.eq_rhs) eqs
and check_node td =
match td.top_decl_desc with
| Node nd -> (
diff --git a/src/types.ml b/src/types.ml
index 8c4bf2de..b7f0374a 100755
--- a/src/types.ml
+++ b/src/types.ml
@@ -355,6 +355,7 @@ let rec is_polymorphic ty =
let mktyptuple nb typ =
let array = Array.make nb typ in
Ttuple (Array.to_list array)
+
(* Local Variables: *)
diff --git a/src/typing.ml b/src/typing.ml
index 283f41f0..0aed94cb 100755
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -562,6 +562,8 @@ let rec check_type_declaration loc cty =
| Tydec_clock ty
| Tydec_array (_, ty) -> check_type_declaration loc ty
| Tydec_const tname ->
+ Format.printf "TABLE: %a@." print_type_table ();
+ (* TODO REMOVE *)
if not (Hashtbl.mem type_table cty)
then raise (Error (loc, Unbound_type tname));
| _ -> ()
@@ -622,7 +624,9 @@ let type_node env nd loc =
(fun uvs v -> ISet.add v.var_id uvs)
ISet.empty vd_env_ol in
let undefined_vars =
- List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init (get_node_eqs nd)
+ let eqs, auts = get_node_eqs nd in
+ (* TODO XXX: il faut typer les handlers de l'automate *)
+ List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
in
(* Typing asserts *)
List.iter (fun assert_ ->
--
GitLab