Revision 8605c4a4
Added by Pierre-Loïc Garoche almost 10 years ago
| src/horn_backend.ml | ||
|---|---|---|
| 38 | 38 |
let rename_machine machine_name = rename (fun n -> machine_name ^ "." ^ n) |
| 39 | 39 |
let rename_machine_list machine_name = List.map (rename_machine machine_name) |
| 40 | 40 |
|
| 41 |
let full_memory_vars machine instance = |
|
| 42 |
(rename_current_list machine.mname.node_id machine.mmemory) @ |
|
| 43 |
(rename_next_list machine.mname.node_id machine.mmemory) |
|
| 44 |
|
|
| 41 | 45 |
let machine_vars m = |
| 42 |
(rename_current_list m.mname.node_id m.mmemory)@ |
|
| 43 |
(rename_next_list m.mname.node_id m.mmemory)@ |
|
| 44 | 46 |
(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 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs)@
|
|
| 48 |
full_memory_vars m () |
|
| 47 | 49 |
|
| 50 |
|
|
| 48 | 51 |
(********************************************************************************************) |
| 49 | 52 |
(* Instruction Printing functions *) |
| 50 | 53 |
(********************************************************************************************) |
| ... | ... | |
| 104 | 107 |
let pp_assign m self pp_var fmt var_type var_name value = |
| 105 | 108 |
fprintf fmt "(%a = %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value |
| 106 | 109 |
|
| 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 |
|
| 110 |
let pp_instance_call |
|
| 111 |
machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) = |
|
| 112 |
try (* stateful node instance *) |
|
| 113 |
begin |
|
| 114 |
let (n,_) = List.assoc i m.minstances in |
|
| 115 |
match node_name n, inputs, outputs with |
|
| 116 |
| "_arrow", [i1; i2], [o] -> begin |
|
| 117 |
if init then |
|
| 118 |
pp_assign |
|
| 119 |
m |
|
| 120 |
self |
|
| 121 |
(pp_horn_var m) |
|
| 122 |
(* (pp_horn_val self (pp_horn_var m) fmt o) *) fmt |
|
| 123 |
o.var_type (LocalVar o) i1 |
|
| 124 |
else |
|
| 125 |
pp_assign |
|
| 126 |
m self (pp_horn_var m) fmt |
|
| 127 |
o.var_type (LocalVar o) i2 |
|
| 128 |
|
|
| 129 |
end |
|
| 130 |
| name, _, _ -> |
|
| 131 |
begin |
|
| 132 |
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in |
|
| 133 |
Format.fprintf fmt "(%s_%s %a%t%a%t%a)" |
|
| 134 |
(node_name n) |
|
| 135 |
(if init then "init" else "step") |
|
| 136 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
|
| 137 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
| 138 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs) |
|
| 139 |
(Utils.pp_final_char_if_non_empty " " outputs) |
|
| 140 |
(Utils.fprintf_list ~sep:" " pp_var) (full_memory_vars target_machine i) |
|
| 141 |
|
|
| 142 |
end |
|
| 143 |
end |
|
| 144 |
with Not_found -> ( (* stateless node instance *) |
|
| 145 |
let (n,_) = List.assoc i m.mcalls in |
|
| 137 | 146 |
Format.fprintf fmt "(%s %a%t%a)" |
| 138 | 147 |
(node_name n) |
| 139 | 148 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
| 140 | 149 |
(Utils.pp_final_char_if_non_empty " " inputs) |
| 141 | 150 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs |
| 151 |
) |
|
| 142 | 152 |
|
| 143 | 153 |
let pp_machine_reset (m: machine_t) self fmt inst = |
| 144 | 154 |
let (node, static) = List.assoc inst m.minstances in |
Also available in: Unified diff
Ongoing ...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@144 041b043f-8d7c-46b2-b46e-ef0dd855326e