4 |
4 |
open Machine_code
|
5 |
5 |
|
6 |
6 |
|
|
7 |
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
|
|
8 |
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
|
|
9 |
|
7 |
10 |
let pp_type fmt t =
|
8 |
11 |
match (Types.repr t).Types.tdesc with
|
9 |
12 |
| Types.Tbool -> Format.fprintf fmt "Bool"
|
... | ... | |
13 |
16 |
| Types.Tstatic _
|
14 |
17 |
| Types.Tconst _
|
15 |
18 |
| Types.Tarrow _
|
16 |
|
| _ -> Format.eprintf "internal error: pp_type %a@." Types.print_ty t; assert false
|
|
19 |
| _ -> Format.eprintf "internal error: pp_type %a@."
|
|
20 |
Types.print_ty t; assert false
|
17 |
21 |
|
18 |
22 |
|
19 |
23 |
let pp_decl_var fmt id =
|
... | ... | |
26 |
30 |
let pp_instr machine_name fmt i =
|
27 |
31 |
Format.fprintf fmt "(xxx)"
|
28 |
32 |
|
29 |
|
let rename f = List.map (fun v -> {v with var_id = f v.var_id } )
|
30 |
|
let rename_current machine_name = rename (fun n -> machine_name ^ "." ^ n ^ "_c")
|
|
33 |
let rename f = (fun v -> {v with var_id = f v.var_id } )
|
|
34 |
let rename_current machine_name = rename (fun n -> machine_name ^ "." ^ n ^ "_c")
|
|
35 |
let rename_current_list machine_name = List.map (rename_current machine_name)
|
31 |
36 |
let rename_next machine_name = rename (fun n -> machine_name ^ "." ^ n ^ "_x")
|
|
37 |
let rename_next_list machine_name = List.map (rename_next machine_name)
|
32 |
38 |
let rename_machine machine_name = rename (fun n -> machine_name ^ "." ^ n)
|
|
39 |
let rename_machine_list machine_name = List.map (rename_machine machine_name)
|
33 |
40 |
|
34 |
41 |
let machine_vars m =
|
35 |
|
(rename_current m.mname.node_id m.mstatic)@
|
36 |
|
(rename_next m.mname.node_id m.mstatic)@
|
37 |
|
(rename_machine m.mname.node_id m.mstep.step_inputs)@
|
38 |
|
(rename_machine m.mname.node_id m.mstep.step_outputs)
|
|
42 |
(rename_current_list m.mname.node_id m.mmemory)@
|
|
43 |
(rename_next_list m.mname.node_id m.mmemory)@
|
|
44 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@
|
|
45 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs)
|
|
46 |
|
|
47 |
|
|
48 |
(********************************************************************************************)
|
|
49 |
(* Instruction Printing functions *)
|
|
50 |
(********************************************************************************************)
|
|
51 |
|
|
52 |
let pp_horn_var m fmt id =
|
|
53 |
if Types.is_array_type id.var_type
|
|
54 |
then
|
|
55 |
assert false (* no arrays in Horn output *)
|
|
56 |
else
|
|
57 |
Format.fprintf fmt "%s" id.var_id
|
|
58 |
|
|
59 |
|
|
60 |
(* Used to print boolean constants *)
|
|
61 |
let pp_horn_tag fmt t =
|
|
62 |
pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
|
|
63 |
|
|
64 |
(* Prints a constant value *)
|
|
65 |
let rec pp_horn_const fmt c =
|
|
66 |
match c with
|
|
67 |
| Const_int i -> pp_print_int fmt i
|
|
68 |
| Const_real r -> pp_print_string fmt r
|
|
69 |
| Const_float r -> pp_print_float fmt r
|
|
70 |
| Const_tag t -> pp_horn_tag fmt t
|
|
71 |
| Const_array ca -> assert false
|
|
72 |
|
|
73 |
(* Prints a value expression [v], with internal function calls only.
|
|
74 |
[pp_var] is a printer for variables (typically [pp_c_var_read]),
|
|
75 |
but an offset suffix may be added for array variables
|
|
76 |
*)
|
|
77 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
|
|
78 |
match v with
|
|
79 |
| Cst c -> pp_horn_const fmt c
|
|
80 |
| Array _
|
|
81 |
| Access _ -> assert false (* no arrays *)
|
|
82 |
| Power (v, n) -> assert false
|
|
83 |
| LocalVar v -> pp_var fmt (rename_machine self v)
|
|
84 |
| StateVar v ->
|
|
85 |
if Types.is_array_type v.var_type
|
|
86 |
then assert false
|
|
87 |
else pp_var fmt ((if is_lhs then rename_next else rename_current) self v)
|
|
88 |
| Fun (n, vl) -> Format.fprintf fmt "(%a)" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
|
|
89 |
|
|
90 |
(* Prints a [value] indexed by the suffix list [loop_vars] *)
|
|
91 |
let rec pp_value_suffix self pp_value fmt value =
|
|
92 |
match value with
|
|
93 |
| Fun (n, vl) ->
|
|
94 |
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
|
|
95 |
| _ ->
|
|
96 |
pp_horn_val self pp_value fmt value
|
|
97 |
|
|
98 |
(* type_directed assignment: array vs. statically sized type
|
|
99 |
- [var_type]: type of variable to be assigned
|
|
100 |
- [var_name]: name of variable to be assigned
|
|
101 |
- [value]: assigned value
|
|
102 |
- [pp_var]: printer for variables
|
|
103 |
*)
|
|
104 |
let pp_assign m self pp_var fmt var_type var_name value =
|
|
105 |
fprintf fmt "(%a = %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
|
|
106 |
|
|
107 |
let pp_instance_call machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
|
|
108 |
try (* stateful node instance *) (
|
|
109 |
let (n,_) = List.assoc i m.minstances in
|
|
110 |
match node_name n, inputs, outputs with
|
|
111 |
| "_arrow", [i1; i2], [o] -> (
|
|
112 |
if init then
|
|
113 |
pp_assign
|
|
114 |
m self (pp_horn_val self (pp_horn_var m) fmt o) fmt
|
|
115 |
o.var_type (LocalVar o) i1
|
|
116 |
else
|
|
117 |
pp_assign
|
|
118 |
m self (pp_horn_val self (pp_horn_var m) fmt o) fmt
|
|
119 |
o.var_type (LocalVar o) i2
|
|
120 |
|
|
121 |
)
|
|
122 |
| name, _, _ -> (
|
|
123 |
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in
|
|
124 |
Format.fprintf fmt "(%s_%s %a%txxx%axxx%t%a)"
|
|
125 |
(node_name n) (if init then "init" else "step")
|
|
126 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
|
|
127 |
(Utils.pp_final_char_if_non_empty " " inputs)
|
|
128 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) outputs
|
|
129 |
(Utils.pp_final_char_if_non_empty " " outputs)
|
|
130 |
|
|
131 |
(Utils.fprintf_list ~sep:" " pp_var) (machine_vars target_machine)
|
|
132 |
|
|
133 |
)
|
|
134 |
)
|
|
135 |
with Not_found -> (* stateless node instance *)
|
|
136 |
let (n,_) = List.assoc i m.mcalls in
|
|
137 |
Format.fprintf fmt "(%s %a%t%a)"
|
|
138 |
(node_name n)
|
|
139 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
|
|
140 |
(Utils.pp_final_char_if_non_empty " " inputs)
|
|
141 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs
|
|
142 |
|
|
143 |
let pp_machine_reset (m: machine_t) self fmt inst =
|
|
144 |
let (node, static) = List.assoc inst m.minstances in
|
|
145 |
fprintf fmt "(%a %a%t%s->%s)"
|
|
146 |
pp_machine_reset_name (node_name node)
|
|
147 |
(Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
|
|
148 |
(Utils.pp_final_char_if_non_empty " " static)
|
|
149 |
self inst
|
|
150 |
|
|
151 |
(* TODO *)
|
|
152 |
let rec pp_conditional machines ?(init=false) (m: machine_t) self fmt c tl el =
|
|
153 |
fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
|
|
154 |
(pp_horn_val self (pp_horn_var m)) c
|
|
155 |
(Utils.pp_newline_if_non_empty tl)
|
|
156 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) tl
|
|
157 |
(Utils.pp_newline_if_non_empty el)
|
|
158 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) el
|
|
159 |
|
|
160 |
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
|
|
161 |
match instr with
|
|
162 |
| MReset i ->
|
|
163 |
pp_machine_reset m self fmt i
|
|
164 |
| MLocalAssign (i,v) ->
|
|
165 |
pp_assign
|
|
166 |
m self (pp_horn_var m) fmt
|
|
167 |
i.var_type (LocalVar i) v
|
|
168 |
| MStateAssign (i,v) ->
|
|
169 |
pp_assign
|
|
170 |
m self (pp_horn_var m) fmt
|
|
171 |
i.var_type (StateVar i) v
|
|
172 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i ->
|
|
173 |
pp_machine_instr machines ~init:init m self fmt (MLocalAssign (i0, Fun (i, vl)))
|
|
174 |
| MStep (il, i, vl) ->
|
|
175 |
pp_instance_call machines ~init:init m self fmt i vl il
|
|
176 |
| MBranch (g,hl) ->
|
|
177 |
if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
|
|
178 |
then (* boolean case, needs special treatment in C because truth value is not unique *)
|
|
179 |
(* may disappear if we optimize code by replacing last branch test with default *)
|
|
180 |
let tl = try List.assoc tag_true hl with Not_found -> [] in
|
|
181 |
let el = try List.assoc tag_false hl with Not_found -> [] in
|
|
182 |
pp_conditional machines ~init:init m self fmt g tl el
|
|
183 |
else assert false (* enum type case *)
|
|
184 |
|
|
185 |
|
|
186 |
(**************************************************************)
|
39 |
187 |
|
40 |
188 |
(* Print the machine m:
|
41 |
189 |
two functions: m_init and m_step
|
... | ... | |
43 |
191 |
- m_step is a predicate over old_memories, inputs, new_memories, outputs
|
44 |
192 |
We first declare all variables then the two /rules/.
|
45 |
193 |
*)
|
46 |
|
let print_machine fmt m =
|
47 |
|
if m.mname.node_id = arrow_id then () else ( (* We don't print arrow function *)
|
|
194 |
let print_machine machines fmt m =
|
|
195 |
let pp_instr init = pp_machine_instr machines ~init:init m in
|
|
196 |
if m.mname.node_id = arrow_id then ()
|
|
197 |
else
|
|
198 |
( (* We don't print arrow function *)
|
48 |
199 |
Format.fprintf fmt "; %s@." m.mname.node_id;
|
49 |
200 |
(* Printing variables *)
|
50 |
201 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
|
51 |
|
((machine_vars m)@(rename_machine m.mname.node_id m.mstep.step_locals));
|
52 |
|
|
|
202 |
((machine_vars m)@(rename_machine_list m.mname.node_id m.mstep.step_locals));
|
|
203 |
Format.pp_print_newline fmt ();
|
53 |
204 |
(* Declaring predicate *)
|
54 |
|
Format.fprintf fmt "(declare-rel %s_init (%a))@."
|
55 |
|
m.mname.node_id
|
56 |
|
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) m.mstatic);
|
|
205 |
Format.fprintf fmt "(declare-rel %a (%a))@."
|
|
206 |
pp_machine_reset_name m.mname.node_id
|
|
207 |
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) m.mmemory);
|
57 |
208 |
|
58 |
|
Format.fprintf fmt "(declare-rel %s_step (%a))@."
|
59 |
|
m.mname.node_id
|
|
209 |
Format.fprintf fmt "(declare-rel %a (%a))@."
|
|
210 |
pp_machine_step_name m.mname.node_id
|
60 |
211 |
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (machine_vars m));
|
|
212 |
Format.pp_print_newline fmt ();
|
61 |
213 |
|
62 |
|
Format.fprintf fmt "(rule (=> (and %a) (%s_init %a)))"
|
63 |
|
(Utils.fprintf_list ~sep:"@." (pp_instr m.mname.node_id)) m.minit
|
|
214 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_init %a)@]@.))@.@."
|
|
215 |
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
|
64 |
216 |
m.mname.node_id
|
65 |
|
(Utils.fprintf_list ~sep:" " pp_var) (rename_machine m.mname.node_id m.mstatic);
|
|
217 |
(Utils.fprintf_list ~sep:" " pp_var) (rename_next_list m.mname.node_id m.mmemory);
|
66 |
218 |
|
67 |
|
Format.fprintf fmt "(rule (=> (and %a) (%s_step %a)))"
|
68 |
|
(Utils.fprintf_list ~sep:"@." (pp_instr m.mname.node_id)) m.mstep.step_instrs
|
|
219 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%s_step %a)@]@.))@.@."
|
|
220 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
|
69 |
221 |
m.mname.node_id
|
70 |
222 |
(Utils.fprintf_list ~sep:" " pp_var) (machine_vars m);
|
71 |
223 |
|
... | ... | |
75 |
227 |
let main_print fmt = ()
|
76 |
228 |
|
77 |
229 |
let translate fmt basename prog machines =
|
78 |
|
List.iter (print_machine fmt) machines;
|
|
230 |
List.iter (print_machine machines fmt) (List.rev machines);
|
79 |
231 |
main_print fmt
|
80 |
232 |
|
81 |
233 |
|
In the middle of the coding process. Just pushing thinks
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@143 041b043f-8d7c-46b2-b46e-ef0dd855326e