Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/backends/Horn/horn_backend_common.ml | ||
---|---|---|
17 | 17 |
let get_machine = Machine_code_common.get_machine |
18 | 18 |
|
19 | 19 |
let machine_reset_name id = id ^ "_reset" |
20 |
let machine_step_name id = id ^ "_step" |
|
21 |
let machine_stateless_name id = id ^ "_fun" |
|
20 |
|
|
21 |
let machine_step_name id = id ^ "_step" |
|
22 |
|
|
23 |
let machine_stateless_name id = id ^ "_fun" |
|
24 |
|
|
22 | 25 |
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id |
26 |
|
|
23 | 27 |
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id |
28 |
|
|
24 | 29 |
let pp_machine_stateless_name fmt id = fprintf fmt "%s_fun" id |
25 | 30 |
|
26 | 31 |
let rec pp_type fmt t = |
27 |
if Types.is_bool_type t then fprintf fmt "Bool" else |
|
28 |
if Types.is_int_type t then fprintf fmt "Int" else |
|
29 |
if Types.is_real_type t then fprintf fmt "Real" else |
|
30 |
match (Types.repr t).Types.tdesc with |
|
31 |
| Types.Tconst ty -> pp_print_string fmt ty |
|
32 |
| Types.Tclock t -> pp_type fmt t |
|
33 |
| Types.Tarray(_,ty) -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")" |
|
34 |
| Types.Tstatic(_, ty) -> pp_type fmt ty |
|
35 |
| Types.Tarrow _ |
|
36 |
| _ -> eprintf "internal error: pp_type %a@." |
|
37 |
Types.print_ty t; assert false |
|
32 |
if Types.is_bool_type t then fprintf fmt "Bool" |
|
33 |
else if Types.is_int_type t then fprintf fmt "Int" |
|
34 |
else if Types.is_real_type t then fprintf fmt "Real" |
|
35 |
else |
|
36 |
match (Types.repr t).Types.tdesc with |
|
37 |
| Types.Tconst ty -> |
|
38 |
pp_print_string fmt ty |
|
39 |
| Types.Tclock t -> |
|
40 |
pp_type fmt t |
|
41 |
| Types.Tarray (_, ty) -> |
|
42 |
fprintf fmt "(Array Int "; |
|
43 |
pp_type fmt ty; |
|
44 |
fprintf fmt ")" |
|
45 |
| Types.Tstatic (_, ty) -> |
|
46 |
pp_type fmt ty |
|
47 |
| Types.Tarrow _ | _ -> |
|
48 |
eprintf "internal error: pp_type %a@." Types.print_ty t; |
|
49 |
assert false |
|
38 | 50 |
|
39 | 51 |
let pp_decl_var fmt id = |
40 |
fprintf fmt "(declare-var %s %a)" |
|
41 |
id.var_id |
|
42 |
pp_type id.var_type |
|
43 |
|
|
44 |
(* let pp_var fmt id = pp_print_string fmt id.var_id *) |
|
52 |
fprintf fmt "(declare-var %s %a)" id.var_id pp_type id.var_type |
|
45 | 53 |
|
54 |
(* let pp_var fmt id = pp_print_string fmt id.var_id *) |
|
46 | 55 |
|
47 | 56 |
let pp_conj pp fmt l = |
48 | 57 |
match l with |
49 |
[] -> assert false |
|
50 |
| [x] -> pp fmt x |
|
51 |
| _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:"@ " pp) l |
|
52 |
|
|
53 |
|
|
58 |
| [] -> |
|
59 |
assert false |
|
60 |
| [ x ] -> |
|
61 |
pp fmt x |
|
62 |
| _ -> |
|
63 |
fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:"@ " pp) l |
|
54 | 64 |
|
55 | 65 |
(********************************************************************************************) |
56 |
(* Workaround to prevent the use of declared keywords as node name *)
|
|
66 |
(* Workaround to prevent the use of declared keywords as node name *)
|
|
57 | 67 |
(********************************************************************************************) |
58 |
let registered_keywords = ["implies"]
|
|
68 |
let registered_keywords = [ "implies" ]
|
|
59 | 69 |
|
60 |
let protect_kwd s = |
|
61 |
if List.mem s registered_keywords then |
|
62 |
"__" ^ s |
|
63 |
else |
|
64 |
s |
|
70 |
let protect_kwd s = if List.mem s registered_keywords then "__" ^ s else s |
|
65 | 71 |
|
66 | 72 |
let node_name n = |
67 | 73 |
let name = node_name n in |
68 | 74 |
protect_kwd name |
69 | 75 |
|
70 |
|
|
71 | 76 |
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x |
72 |
let rename f = (fun v -> {v with var_id = f v.var_id } ) |
|
77 |
|
|
78 |
let rename f v = { v with var_id = f v.var_id } |
|
79 |
|
|
73 | 80 |
let rename_machine p = rename (fun n -> concat p n) |
81 |
|
|
74 | 82 |
let rename_machine_list p = List.map (rename_machine p) |
75 | 83 |
|
76 |
let rename_current = rename (fun n -> n ^ "_c") |
|
84 |
let rename_current = rename (fun n -> n ^ "_c") |
|
85 |
|
|
77 | 86 |
let rename_current_list = List.map rename_current |
78 |
let rename_mid = rename (fun n -> n ^ "_m") |
|
87 |
|
|
88 |
let rename_mid = rename (fun n -> n ^ "_m") |
|
89 |
|
|
79 | 90 |
let rename_mid_list = List.map rename_mid |
91 |
|
|
80 | 92 |
let rename_next = rename (fun n -> n ^ "_x") |
81 |
let rename_next_list = List.map rename_next |
|
82 | 93 |
|
94 |
let rename_next_list = List.map rename_next |
|
83 | 95 |
|
84 | 96 |
let local_memory_vars machine = |
85 | 97 |
rename_machine_list machine.mname.node_id machine.mmemory |
86 |
|
|
87 |
let instances_memory_vars ?(without_arrow=false) machines machine =
|
|
98 |
|
|
99 |
let instances_memory_vars ?(without_arrow = false) machines machine =
|
|
88 | 100 |
let rec aux fst prefix m = |
89 |
( |
|
90 |
if not fst then ( |
|
91 |
(rename_machine_list (concat prefix m.mname.node_id) m.mmemory) |
|
92 |
) |
|
93 |
else [] |
|
94 |
) @ |
|
95 |
List.fold_left (fun accu (id, (n, _)) -> |
|
96 |
let name = node_name n in |
|
97 |
if without_arrow && name = "_arrow" then |
|
98 |
accu |
|
99 |
else |
|
100 |
let machine_n = get_machine machines name in |
|
101 |
( aux false (concat prefix |
|
102 |
(if fst then id else concat m.mname.node_id id)) |
|
103 |
machine_n ) @ accu |
|
104 |
) [] (m.minstances) |
|
101 |
(if not fst then |
|
102 |
rename_machine_list (concat prefix m.mname.node_id) m.mmemory |
|
103 |
else []) |
|
104 |
@ List.fold_left |
|
105 |
(fun accu (id, (n, _)) -> |
|
106 |
let name = node_name n in |
|
107 |
if without_arrow && name = "_arrow" then accu |
|
108 |
else |
|
109 |
let machine_n = get_machine machines name in |
|
110 |
aux false |
|
111 |
(concat prefix (if fst then id else concat m.mname.node_id id)) |
|
112 |
machine_n |
|
113 |
@ accu) |
|
114 |
[] m.minstances |
|
105 | 115 |
in |
106 | 116 |
aux true machine.mname.node_id machine |
107 | 117 |
|
108 | 118 |
(* Extract the arrows of a given node/machine *) |
109 | 119 |
let arrow_vars machines machine : Lustre_types.var_decl list = |
110 | 120 |
let rec aux fst prefix m = |
111 |
List.fold_left (fun accu (id, (n, _)) -> |
|
112 |
let name = node_name n in |
|
113 |
if name = "_arrow" then |
|
114 |
let arrow_machine = Machine_code_common.arrow_machine in |
|
115 |
(rename_machine_list |
|
116 |
(concat prefix (concat (if fst then id else concat m.mname.node_id id) "_arrow")) |
|
117 |
arrow_machine.mmemory |
|
118 |
) @ accu |
|
119 |
else |
|
120 |
let machine_n = get_machine machines name in |
|
121 |
( aux false (concat prefix |
|
122 |
(if fst then id else concat m.mname.node_id id)) |
|
123 |
machine_n ) @ accu |
|
124 |
) [] (m.minstances) |
|
121 |
List.fold_left |
|
122 |
(fun accu (id, (n, _)) -> |
|
123 |
let name = node_name n in |
|
124 |
if name = "_arrow" then |
|
125 |
let arrow_machine = Machine_code_common.arrow_machine in |
|
126 |
rename_machine_list |
|
127 |
(concat prefix |
|
128 |
(concat (if fst then id else concat m.mname.node_id id) "_arrow")) |
|
129 |
arrow_machine.mmemory |
|
130 |
@ accu |
|
131 |
else |
|
132 |
let machine_n = get_machine machines name in |
|
133 |
aux false |
|
134 |
(concat prefix (if fst then id else concat m.mname.node_id id)) |
|
135 |
machine_n |
|
136 |
@ accu) |
|
137 |
[] m.minstances |
|
125 | 138 |
in |
126 | 139 |
aux true machine.mname.node_id machine |
127 | 140 |
|
128 |
let full_memory_vars ?(without_arrow=false) machines machine =
|
|
129 |
(local_memory_vars machine)
|
|
130 |
@ (instances_memory_vars ~without_arrow machines machine)
|
|
141 |
let full_memory_vars ?(without_arrow = false) machines machine =
|
|
142 |
local_memory_vars machine
|
|
143 |
@ instances_memory_vars ~without_arrow machines machine
|
|
131 | 144 |
|
132 | 145 |
let inout_vars m = |
133 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)
|
|
134 |
@ (rename_machine_list m.mname.node_id m.mstep.step_outputs)
|
|
146 |
rename_machine_list m.mname.node_id m.mstep.step_inputs
|
|
147 |
@ rename_machine_list m.mname.node_id m.mstep.step_outputs
|
|
135 | 148 |
|
136 | 149 |
let step_vars machines m = |
137 |
(inout_vars m)
|
|
138 |
@ (rename_current_list (full_memory_vars machines m))
|
|
139 |
@ (rename_next_list (full_memory_vars machines m))
|
|
150 |
inout_vars m
|
|
151 |
@ rename_current_list (full_memory_vars machines m)
|
|
152 |
@ rename_next_list (full_memory_vars machines m)
|
|
140 | 153 |
|
141 | 154 |
let step_vars_m_x machines m = |
142 |
(inout_vars m)
|
|
143 |
@ (rename_mid_list (full_memory_vars machines m))
|
|
144 |
@ (rename_next_list (full_memory_vars machines m))
|
|
155 |
inout_vars m
|
|
156 |
@ rename_mid_list (full_memory_vars machines m)
|
|
157 |
@ rename_next_list (full_memory_vars machines m)
|
|
145 | 158 |
|
146 | 159 |
let reset_vars machines m = |
147 |
(rename_current_list (full_memory_vars machines m))
|
|
148 |
@ (rename_mid_list (full_memory_vars machines m))
|
|
160 |
rename_current_list (full_memory_vars machines m)
|
|
161 |
@ rename_mid_list (full_memory_vars machines m)
|
|
149 | 162 |
|
150 | 163 |
let step_vars_c_m_x machines m = |
151 |
(inout_vars m) |
|
152 |
@ (rename_current_list (full_memory_vars machines m)) |
|
153 |
@ (rename_mid_list (full_memory_vars machines m)) |
|
154 |
@ (rename_next_list (full_memory_vars machines m)) |
|
155 |
|
|
164 |
inout_vars m |
|
165 |
@ rename_current_list (full_memory_vars machines m) |
|
166 |
@ rename_mid_list (full_memory_vars machines m) |
|
167 |
@ rename_next_list (full_memory_vars machines m) |
|
156 | 168 |
|
157 | 169 |
(* Local Variables: *) |
158 | 170 |
(* compile-command:"make -C ../.." *) |
Also available in: Unified diff
reformatting