From 1eda3e78291f3a5b2f530ae6966e15efad297c39 Mon Sep 17 00:00:00 2001
From: xthirioux <xthirioux@041b043f-8d7c-46b2-b46e-ef0dd855326e>
Date: Tue, 9 Sep 2014 16:03:36 +0000
Subject: [PATCH] - work in progress for automata...
---
src/access.ml | 2 +-
src/automata.ml | 91 ++++++++++++------------------
src/backends/C/c_backend_common.ml | 17 +++++-
src/backends/C/c_backend_header.ml | 5 +-
src/causality.ml | 20 ++++---
src/clock_calculus.ml | 2 +-
src/corelang.ml | 35 +++++++++---
src/corelang.mli | 3 +-
src/inliner.ml | 41 +++++++-------
src/lustreSpec.ml | 16 +++---
src/machine_code.ml | 6 +-
src/normalization.ml | 4 +-
src/optimize_prog.ml | 4 +-
src/parser_lustre.mly | 18 +++---
src/printers.ml | 45 ++++++++++++++-
src/stateless.ml | 2 +-
src/typing.ml | 2 +-
17 files changed, 189 insertions(+), 124 deletions(-)
diff --git a/src/access.ml b/src/access.ml
index 3efc7cae..0797d42e 100755
--- a/src/access.ml
+++ b/src/access.ml
@@ -80,7 +80,7 @@ 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 nd.node_eqs in
+ List.fold_left (fun checks eq -> check_expr checks eq.eq_rhs) checks (get_node_eqs nd) in
nd.node_checks <- CSet.elements checks
let check_top_decl decl =
diff --git a/src/automata.ml b/src/automata.ml
index d587eede..3f1fedb0 100755
--- a/src/automata.ml
+++ b/src/automata.ml
@@ -13,40 +13,6 @@ open Utils
open LustreSpec
open Corelang
-let pp_restart fmt restart =
- Format.fprintf fmt "%s" (if restart then "restart" else "resume")
-
-let pp_unless fmt (_, expr, restart, st) =
- Format.fprintf fmt "unless %a %a %s"
- Printers.pp_expr expr
- pp_restart restart
- st
-
-let pp_until fmt (_, expr, restart, st) =
- Format.fprintf fmt "until %a %a %s"
- Printers.pp_expr expr
- pp_restart restart
- st
-
-let pp_handler fmt handler =
- Format.fprintf fmt "state %s -> %a %a let %a tel %a"
- handler.hand_state
- (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
- (fun fmt locals ->
- match locals with [] -> () | _ ->
- Format.fprintf fmt "@[<v 4>var %a@]@ "
- (Utils.fprintf_list ~sep:"@ "
- (fun fmt v -> Format.fprintf fmt "%a;" Printers.pp_node_var v))
- locals)
- handler.hand_locals
- Printers.pp_node_eqs handler.hand_eqs
- (Utils.fprintf_list ~sep:"@ " pp_until) handler.hand_until
-
-let pp_automata fmt aut =
- Format.fprintf fmt "automaton %s %a"
- aut.aut_id
- (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
-
let mkbool loc b =
mkexpr loc (Expr_const (const_of_bool b))
@@ -62,12 +28,12 @@ let init loc restart state =
let add_branch (loc, expr, restart, st) cont =
mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont))
-let mkhandler loc st unless until locals (eqs, asserts, annots) =
+let mkhandler loc st unless until locals (stmts, asserts, annots) =
{hand_state = st;
hand_unless = unless;
hand_until = until;
hand_locals = locals;
- hand_eqs = eqs;
+ hand_stmts = stmts;
hand_asserts = asserts;
hand_annots = annots;
hand_loc = loc}
@@ -77,27 +43,38 @@ let mkautomata loc id handlers =
aut_handlers = handlers;
aut_loc = loc}
-let handler_read handler =
- List.fold_left (fun read eq -> get_expr_vars read eq.eq_rhs) ISet.empty handler.hand_eqs
-
-let handler_write handler =
- List.fold_left (fun write eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs) ISet.empty handler.hand_eqs
+let rec handler_read reads handler =
+ let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
+ let allvars =
+ List.fold_left (fun read stmt ->
+ match stmt with
+ | Eq eq -> get_expr_vars read eq.eq_rhs
+ | Aut aut -> List.fold_left handler_read read aut.aut_handlers ) reads handler.hand_stmts
+ in ISet.diff allvars locals
+
+let rec handler_write writes handler =
+ let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
+ let allvars =
+ List.fold_left (fun write stmt ->
+ match stmt with
+ | Eq eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs
+ | Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts
+ in ISet.diff allvars locals
let node_of_handler node aut_id handler =
- let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
- let inputs = handler_read handler in
- let outputs = handler_write handler in
+ let inputs = handler_read ISet.empty handler in
+ let outputs = handler_write ISet.empty handler in
{
node_id = Format.sprintf "%s_%s_handler" aut_id handler.hand_state;
node_type = Types.new_var ();
node_clock = Clocks.new_var true;
- node_inputs = List.map (fun v -> get_node_var v node) (ISet.elements (ISet.diff inputs locals));
- node_outputs = List.map (fun v -> get_node_var v node) (ISet.elements (ISet.diff outputs locals));
+ node_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs);
+ node_outputs = List.map (fun v -> get_node_var v node) (ISet.elements outputs);
node_locals = handler.hand_locals;
node_gencalls = [];
node_checks = [];
node_asserts = handler.hand_asserts;
- node_eqs = handler.hand_eqs;
+ node_stmts = handler.hand_stmts;
node_dec_stateless = false;
node_stateless = None;
node_spec = None;
@@ -111,7 +88,7 @@ let expr_of_handler loc restart state node tag =
let arg = mkexpr loc (Expr_tuple (List.map (fun v -> mkident loc v.var_id) node.node_inputs)) in
mkexpr loc (Expr_when (mkexpr loc (Expr_appl (node.node_id, arg, Some (restart, tag_true))), state, tag))
-let assign_aut_handlers loc node actual_r actual_s hnodes =
+let assign_aut_handlers loc actual_r actual_s hnodes =
let outputs = (snd (List.hd hnodes)).node_outputs in
let assign_handlers = List.map (fun (hs, n) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in
let assign_expr = mkexpr loc (Expr_merge (actual_s, assign_handlers)) in
@@ -123,6 +100,12 @@ let typedef_of_automata node aut =
{ tydef_id = tname;
tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)
}
+(*
+let expand_automata_stmt (top_decls, locals, eqs) stmt =
+ match stmt with
+ | Eq eq -> (top_decls, locals, eq::eqs)
+ | Aut aut ->
+
let expand_automata top_node aut =
let node = node_of_top top_node in
@@ -141,7 +124,7 @@ let expand_automata top_node aut =
let fby_until_expr = mkfby aut.aut_loc (init aut.aut_loc tag_false initial) until_expr in
let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in
let hnodes = List.map (fun h -> (h.hand_state, node_of_handler node aut.aut_id h)) aut.aut_handlers in
- let assign_eq = assign_aut_handlers aut.aut_loc node actual_r actual_s hnodes in
+ let assign_eq = assign_aut_handlers aut.aut_loc actual_r actual_s hnodes in
let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in
let tydec_const id = { ty_dec_desc = Tydec_const id; ty_dec_loc = aut.aut_loc } in
let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in
@@ -149,15 +132,15 @@ let expand_automata top_node aut =
mkvar_decl aut.aut_loc (actual_r , tydec_bool, ckdec_any, false);
mkvar_decl aut.aut_loc (incoming_s, tydec_const typedef.tydef_id, ckdec_any, false);
mkvar_decl aut.aut_loc (actual_s , tydec_const typedef.tydef_id, ckdec_any, false)] in
- let eqs' = [unless_eq; assign_eq; until_eq] in
- let node' = { node with node_locals = locals'@node.node_locals; node_eqs = eqs'@node.node_eqs } in
+ let eqs' = [Eq unless_eq; Eq assign_eq; Eq until_eq] in
+ let node' = { node with node_locals = locals'@node.node_locals; node_stmts = eqs'@node.node_stmts } in
(mktop_decl aut.aut_loc owner false (TypeDef typedef)) ::
{ top_node with top_decl_desc = Node node' } ::
(List.map2 (fun h (hs, n) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes)
-
-let node_extract_automata top_decl =
+*)
+let rec node_extract_automata top_decl =
match top_decl.top_decl_desc with
- | Node nd -> [top_decl]
+ | Node nd -> []
| _ -> [top_decl]
(*
let extract_automata top_decls =
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index cced6a98..f6d17695 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -24,15 +24,26 @@ let print_version fmt =
(* Generation of a non-clashing name for the self memory variable (for step and reset functions) *)
let mk_self m =
- mk_new_name (m.mstep.step_inputs@m.mstep.step_outputs@m.mstep.step_locals@m.mmemory) "self"
+ let used name =
+ (List.exists (fun v -> v.var_id = name) m.mstep.step_inputs)
+ || (List.exists (fun v -> v.var_id = name) m.mstep.step_outputs)
+ || (List.exists (fun v -> v.var_id = name) m.mstep.step_locals)
+ || (List.exists (fun v -> v.var_id = name) m.mmemory) in
+ mk_new_name used "self"
(* Generation of a non-clashing name for the instance variable of static allocation macro *)
let mk_instance m =
- mk_new_name (m.mstep.step_inputs@m.mmemory) "inst"
+ let used name =
+ (List.exists (fun v -> v.var_id = name) m.mstep.step_inputs)
+ || (List.exists (fun v -> v.var_id = name) m.mmemory) in
+ mk_new_name used "inst"
(* Generation of a non-clashing name for the attribute variable of static allocation macro *)
let mk_attribute m =
- mk_new_name (m.mstep.step_inputs@m.mmemory) "attr"
+ let used name =
+ (List.exists (fun v -> v.var_id = name) m.mstep.step_inputs)
+ || (List.exists (fun v -> v.var_id = name) m.mmemory) in
+ mk_new_name used "attr"
let mk_call_var_decl loc id =
{ var_id = id;
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 3a7d50d1..c3d67e6f 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -172,7 +172,10 @@ let print_machine_decl_from_header fmt inode =
else
begin
let static_inputs = List.filter (fun v -> v.var_dec_const) inode.nodei_inputs in
- let self = mk_new_name (inode.nodei_inputs@inode.nodei_outputs) "self" in
+ let used name =
+ (List.exists (fun v -> v.var_id = name) inode.nodei_inputs)
+ || (List.exists (fun v -> v.var_id = name) inode.nodei_outputs) in
+ let self = mk_new_name used "self" in
fprintf fmt "extern %a;@.@."
(print_reset_prototype self) (inode.nodei_id, static_inputs);
diff --git a/src/causality.ml b/src/causality.ml
index 0b69051a..2d09cce4 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -121,7 +121,7 @@ let eq_memory_variables mems eq =
match_mem eq.eq_lhs eq.eq_rhs mems
let node_memory_variables nd =
- List.fold_left eq_memory_variables ISet.empty nd.node_eqs
+ List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)
let node_input_variables nd =
List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty nd.node_inputs
@@ -149,7 +149,7 @@ let node_eq_equiv nd =
let first = List.hd eq.eq_lhs in
List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs
)
- nd.node_eqs;
+ (get_node_eqs nd);
eq_equiv
(* Create a tuple of right dimension, according to [expr] type, *)
@@ -255,7 +255,7 @@ let dependence_graph mems inputs node_vars n =
instance_var_cpt := 0;
let g = new_graph (), new_graph () in
(* Basic dependencies *)
- let g = List.fold_right (add_eq_dependencies mems inputs node_vars) n.node_eqs g in
+ let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in
g
end
@@ -312,7 +312,7 @@ module NodeDep = struct
| Node nd ->
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)
let accu = add_vertices [nd.node_id] accu in
- let deps = List.map (fun e -> fst (desome (get_callee e))) (get_calls (fun _ -> true) nd.node_eqs) in
+ let deps = List.map (fun e -> fst (desome (get_callee e))) (get_calls (fun _ -> true) (get_node_eqs nd)) in
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)
add_edges [nd.node_id] deps accu
| _ -> assert false (* should not happen *)
@@ -332,7 +332,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 nd.node_eqs
+ nd.node_gencalls <- get_calls prednode (get_node_eqs nd)
| _ -> ()
) prog
@@ -345,7 +345,11 @@ module CycleDetection = struct
module Cycles = Graph.Components.Make (IdentDepGraph)
let mk_copy_var n id =
- mk_new_name (get_node_vars n) id
+ let used name =
+ (List.exists (fun v -> v.var_id = name) n.node_locals)
+ || (List.exists (fun v -> v.var_id = name) n.node_inputs)
+ || (List.exists (fun v -> v.var_id = name) n.node_outputs)
+ in mk_new_name used id
let mk_copy_eq n var =
let var_decl = get_node_var var n in
@@ -407,7 +411,7 @@ 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) node.node_eqs in
+ 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 rec break vdecls mem_eqs g =
let scc_l = Cycles.scc_list g in
let wrong = List.filter (wrong_partition g) scc_l in
@@ -553,7 +557,7 @@ let global_dependency node =
begin
merge_with g_non_mems g_mems';
add_external_dependency outputs mems g_non_mems;
- { node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals },
+ { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals },
g_non_mems
end
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index 42556941..a1bccd1e 100755
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -771,7 +771,7 @@ 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) nd.node_eqs;
+ List.iter (clock_eq new_env) (get_node_eqs nd);
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
diff --git a/src/corelang.ml b/src/corelang.ml
index 173f33d2..8b794c25 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -68,9 +68,9 @@ let var_decl_of_const c =
var_clock = Clocks.new_var false;
var_loc = c.const_loc }
-let mk_new_name vdecl_list id =
+let mk_new_name used id =
let rec new_name name cpt =
- if List.exists (fun v -> v.var_id = name) vdecl_list
+ if used name
then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
else name
in new_name id 1
@@ -475,8 +475,29 @@ let get_var id var_list =
let get_node_var id node = get_var id (get_node_vars node)
+let get_node_eqs =
+ let get_eqs stmts =
+ List.fold_right
+ (fun stmt res ->
+ match stmt with
+ | Eq eq -> eq :: res
+ | Aut _ -> assert false)
+ stmts
+ [] in
+ let table_eqs = Hashtbl.create 23 in
+ (fun nd ->
+ try
+ let (old, res) = Hashtbl.find table_eqs nd.node_id
+ in if old == nd.node_stmts then res else raise Not_found
+ with Not_found ->
+ let res = get_eqs nd.node_stmts in
+ begin
+ Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
+ res
+ end)
+
let get_node_eq id node =
- List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
+ List.find (fun eq -> List.mem id eq.eq_lhs) (get_node_eqs node)
let get_nodes prog =
List.fold_left (
@@ -639,7 +660,7 @@ let rename_node f_node f_var f_const nd =
rename_expr f_node f_var f_const expr})
nd.node_asserts
in
- let eqs = List.map rename_eq nd.node_eqs 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)
@@ -660,7 +681,7 @@ let rename_node f_node f_var f_const nd =
node_gencalls = gen_calls;
node_checks = node_checks;
node_asserts = node_asserts;
- node_eqs = eqs;
+ node_stmts = node_stmts;
node_dec_stateless = nd.node_dec_stateless;
node_stateless = nd.node_stateless;
node_spec = spec;
@@ -889,7 +910,7 @@ and get_calls_expr_desc nodes expr_desc =
and get_eq_calls nodes eq =
get_expr_calls nodes eq.eq_rhs
and get_node_calls nodes node =
- List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs
+ List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node)
let rec get_expr_vars vars e =
get_expr_desc_vars vars e.expr_desc
@@ -932,7 +953,7 @@ and expr_desc_has_arrows expr_desc =
and eq_has_arrows eq =
expr_has_arrows eq.eq_rhs
and node_has_arrows node =
- List.exists (fun eq -> eq_has_arrows eq) node.node_eqs
+ List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node)
(* Local Variables: *)
(* compile-command:"make -C .." *)
diff --git a/src/corelang.mli b/src/corelang.mli
index 119accfd..d7f17031 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -26,7 +26,7 @@ val mkeq: Location.t -> ident list * expr -> eq
val mkassert: Location.t -> expr -> assert_t
val mktop_decl: Location.t -> ident -> bool -> top_decl_desc -> top_decl
val mkpredef_call: Location.t -> ident -> expr list -> expr
-val mk_new_name: var_decl list -> ident -> ident
+val mk_new_name: (ident -> bool) -> ident -> ident
val node_table : (ident, top_decl) Hashtbl.t
@@ -65,6 +65,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_eq: ident -> node_desc -> eq
val get_node_interface: node_desc -> imported_node_desc
diff --git a/src/inliner.ml b/src/inliner.ml
index 39912ded..f948549e 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -46,7 +46,7 @@ let inline_call orig_expr args reset locals node =
node.node_id uid v;
Format.flush_str_formatter ())
in
- let eqs' = List.map (rename_eq rename) node.node_eqs
+ let eqs' = List.map (rename_eq rename) (get_node_eqs node)
in
let rename_var v = { v with var_id = rename v.var_id } in
let inputs' = List.map rename_var node.node_inputs in
@@ -171,11 +171,11 @@ and inline_node nd nodes =
inline_expr eq.eq_rhs locals nodes
in
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
- ) (nd.node_locals, [], nd.node_asserts) nd.node_eqs
+ ) (nd.node_locals, [], nd.node_asserts) (get_node_eqs nd)
in
{ nd with
node_locals = new_locals;
- node_eqs = eqs;
+ node_stmts = List.map (fun eq -> Eq eq) eqs;
node_asserts = asserts;
}
@@ -241,6 +241,23 @@ let witness filename main_name orig inlined type_env clock_env =
(* Building main node *)
+ let ok_i_eq =
+ { eq_loc = loc;
+ eq_lhs = List.map (fun v -> v.var_id) ok_i;
+ eq_rhs =
+ let inputs = expr_of_expr_list loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in
+ let call_orig =
+ mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in
+ let call_inlined =
+ mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in
+ let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in
+ mkexpr loc (Expr_appl ("=", args, None))
+ } in
+ let ok_eq =
+ { eq_loc = loc;
+ eq_lhs = [ok_ident];
+ eq_rhs = main_ok_expr;
+ } in
let main_node = {
node_id = "check";
node_type = Types.new_var ();
@@ -251,23 +268,7 @@ let witness filename main_name orig inlined type_env clock_env =
node_gencalls = [];
node_checks = [];
node_asserts = [];
- node_eqs = [
- { eq_loc = loc;
- eq_lhs = List.map (fun v -> v.var_id) ok_i;
- eq_rhs =
- let inputs = expr_of_expr_list loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in
- let call_orig =
- mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in
- let call_inlined =
- mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in
- let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in
- mkexpr loc (Expr_appl ("=", args, None))
- };
- { eq_loc = loc;
- eq_lhs = [ok_ident];
- eq_rhs = main_ok_expr;
- }
- ];
+ node_stmts = [Eq ok_i_eq; Eq ok_eq];
node_dec_stateless = false;
node_stateless = None;
node_spec = Some
diff --git a/src/lustreSpec.ml b/src/lustreSpec.ml
index d9f3845f..b981156a 100644
--- a/src/lustreSpec.ml
+++ b/src/lustreSpec.ml
@@ -135,9 +135,13 @@ type assert_t =
{
assert_expr: expr;
assert_loc: Location.t;
- }
+ }
+
+type statement =
+| Eq of eq
+| Aut of automata_desc
-type automata_desc =
+and automata_desc =
{aut_id : ident;
aut_handlers: handler_desc list;
aut_loc: Location.t}
@@ -147,15 +151,11 @@ and handler_desc =
hand_unless: (Location.t * expr * bool * ident) list;
hand_until: (Location.t * expr * bool * ident) list;
hand_locals: var_decl list;
- hand_eqs: eq list;
+ hand_stmts: statement list;
hand_asserts: assert_t list;
hand_annots: expr_annot list;
hand_loc: Location.t}
-type statement =
-| Eq of eq
-| Aut of automata_desc
-
type node_desc =
{node_id: ident;
mutable node_type: Types.type_expr;
@@ -166,7 +166,7 @@ type node_desc =
mutable node_gencalls: expr list;
mutable node_checks: Dimension.dim_expr list;
node_asserts: assert_t list;
- node_eqs: eq list;
+ node_stmts: statement list;
mutable node_dec_stateless: bool;
mutable node_stateless: bool option;
node_spec: node_annot option;
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 715dfc71..b5aaa764 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -156,7 +156,7 @@ let arrow_desc =
node_gencalls = [];
node_checks = [];
node_asserts = [];
- node_eqs= [];
+ node_stmts= [];
node_dec_stateless = false;
node_stateless = Some false;
node_spec = None;
@@ -428,7 +428,7 @@ 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 nd.node_eqs in
+ let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in
let eqs_rev, remainder =
List.fold_left
(fun (accu, node_eqs_remainder) vl ->
@@ -446,7 +446,7 @@ let sort_equations_from_schedule nd sch =
if List.length remainder > 0 then (
Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?"
Printers.pp_node_eqs remainder
- Printers.pp_node_eqs nd.node_eqs;
+ Printers.pp_node_eqs (get_node_eqs nd);
assert false);
List.rev eqs_rev
end
diff --git a/src/normalization.ml b/src/normalization.ml
index 5aafac4d..1272f1da 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -349,7 +349,7 @@ 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) node.node_eqs in
+ List.fold_left (normalize_eq node) ([], orig_vars) (get_node_eqs node) in
(* Normalize the asserts *)
let vars, assert_defs, asserts =
List.fold_left (
@@ -391,7 +391,7 @@ let normalize_node node =
let node =
{ node with
node_locals = new_locals;
- node_eqs = defs @ assert_defs;
+ node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
node_asserts = asserts;
node_annot = norm_traceability::node.node_annot;
}
diff --git a/src/optimize_prog.ml b/src/optimize_prog.ml
index 3ee97710..2214aa0f 100644
--- a/src/optimize_prog.ml
+++ b/src/optimize_prog.ml
@@ -46,7 +46,7 @@ let eq_unfold_consts consts eq =
{ eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }
let node_unfold_consts consts node =
- { node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs }
+ { node with node_stmts = List.map (fun eq -> Eq (eq_unfold_consts consts eq)) (get_node_eqs node) }
let prog_unfold_consts prog =
let consts = List.map const_of_top (get_consts prog) in
@@ -89,7 +89,7 @@ let eq_distribute_when eq =
{ eq with eq_rhs = expr_distribute_when eq.eq_rhs }
let node_distribute_when node =
- { node with node_eqs = List.map eq_distribute_when node.node_eqs }
+ { node with node_stmts = List.map (fun eq -> Eq (eq_distribute_when eq)) (get_node_eqs node) }
let prog_distribute_when prog =
List.map (
diff --git a/src/parser_lustre.mly b/src/parser_lustre.mly
index 2d79df3f..5644c382 100755
--- a/src/parser_lustre.mly
+++ b/src/parser_lustre.mly
@@ -188,8 +188,8 @@ in_lib_opt:
top_decl:
| CONST cdecl_list { List.rev ($2 false) }
-| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL
- {let eqs, asserts, annots = $16 in
+| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL
+ {let stmts, asserts, annots = $16 in
let nd = mktop_decl false (Node
{node_id = $3;
node_type = Types.new_var ();
@@ -200,7 +200,7 @@ top_decl:
node_gencalls = [];
node_checks = [];
node_asserts = asserts;
- node_eqs = eqs;
+ node_stmts = stmts;
node_dec_stateless = $2;
node_stateless = None;
node_spec = $1;
@@ -251,12 +251,12 @@ tag_list:
field_list: { [] }
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
-eq_list:
+stmt_list:
{ [], [], [] }
-| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
-| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
-| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
-| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
+| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}
+| assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
+| ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
+| automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl}
automaton:
AUTOMATON type_ident handler_list { (Automata.mkautomata (get_loc ()) $2 $3); failwith "not implemented" }
@@ -266,7 +266,7 @@ handler_list:
| handler handler_list { $1::$2 }
handler:
- STATE UIDENT ARROW unless_list locals LET eq_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
+ STATE UIDENT ARROW unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
unless_list:
{ [] }
diff --git a/src/printers.ml b/src/printers.ml
index 7ea7105f..a26713e7 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -131,7 +131,48 @@ let pp_node_eq fmt eq =
pp_eq_lhs eq.eq_lhs
pp_expr eq.eq_rhs
-let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq
+let pp_restart fmt restart =
+ Format.fprintf fmt "%s" (if restart then "restart" else "resume")
+
+let pp_unless fmt (_, expr, restart, st) =
+ Format.fprintf fmt "unless %a %a %s"
+ pp_expr expr
+ pp_restart restart
+ st
+
+let pp_until fmt (_, expr, restart, st) =
+ Format.fprintf fmt "until %a %a %s"
+ pp_expr expr
+ pp_restart restart
+ st
+
+let rec pp_handler fmt handler =
+ Format.fprintf fmt "state %s -> %a %a let %a tel %a"
+ handler.hand_state
+ (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
+ (fun fmt locals ->
+ match locals with [] -> () | _ ->
+ Format.fprintf fmt "@[<v 4>var %a@]@ "
+ (Utils.fprintf_list ~sep:"@ "
+ (fun fmt v -> Format.fprintf fmt "%a;" pp_node_var v))
+ locals)
+ handler.hand_locals
+ pp_node_stmts handler.hand_stmts
+ (Utils.fprintf_list ~sep:"@ " pp_until) handler.hand_until
+
+and pp_node_stmt fmt stmt =
+ match stmt with
+ | Eq eq -> pp_node_eq fmt eq
+ | Aut aut -> pp_node_aut fmt aut
+
+and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts
+
+and pp_node_aut fmt aut =
+ Format.fprintf fmt "automaton %s %a"
+ aut.aut_id
+ (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
+
+and pp_node_eqs fmt eqs = fprintf_list ~sep:"@ " pp_node_eq fmt eqs
let rec pp_var_struct_type_field fmt (label, tdesc) =
fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc
@@ -217,7 +258,7 @@ fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2> @ @[<v>%a@ %
checks
) nd.node_checks
(fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot
- pp_node_eqs nd.node_eqs
+ pp_node_stmts nd.node_stmts
pp_asserts nd.node_asserts
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
diff --git a/src/stateless.ml b/src/stateless.ml
index 5fcec93b..3148e032 100755
--- a/src/stateless.ml
+++ b/src/stateless.ml
@@ -36,7 +36,7 @@ let rec check_expr expr =
check_expr e' &&
(Basic_library.is_internal_fun i || check_node (node_from_name i))
and compute_node nd =
- List.for_all (fun eq -> check_expr eq.eq_rhs) nd.node_eqs
+ List.for_all (fun eq -> check_expr eq.eq_rhs) (get_node_eqs nd)
and check_node td =
match td.top_decl_desc with
| Node nd -> (
diff --git a/src/typing.ml b/src/typing.ml
index 718f1d2c..4aaf8fc0 100755
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -619,7 +619,7 @@ let type_node env nd loc =
(fun uvs v -> IMap.add v.var_id () uvs)
IMap.empty vd_env_ol in
let undefined_vars =
- List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
+ List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init (get_node_eqs nd)
in
(* Typing asserts *)
List.iter (fun assert_ ->
--
GitLab