Revision 58fd528a
Added by Pierre-Loïc Garoche almost 5 years ago
| src/tools/tiny/tiny_utils.ml | ||
|---|---|---|
| 1 | 1 |
|
| 2 | 2 |
module Ast = Tiny.Ast |
| 3 | 3 |
|
| 4 |
|
|
| 5 |
let lloc_to_tloc loc = Tiny.Location.dummy (*TODO*) |
|
| 4 |
let gen_loc () = Tiny.Location.dummy () |
|
| 5 |
|
|
| 6 |
let lloc_to_tloc loc = Tiny.Location.location_of_positions loc.Location.loc_start loc.Location.loc_end |
|
| 6 | 7 |
|
| 7 |
let tloc_to_lloc loc = Location.dummy_loc (*TODO*)
|
|
| 8 |
let tloc_to_lloc loc = assert false (*Location.dummy_loc (*TODO*) *)
|
|
| 8 | 9 |
|
| 9 | 10 |
|
| 10 | 11 |
let ltyp_to_ttyp t = |
| ... | ... | |
| 21 | 22 |
Ast.Cst(Q.of_int 0, "false"); |
| 22 | 23 |
expr_loc = loc; |
| 23 | 24 |
expr_type = Ast.BoolT } |
| 25 |
|
|
| 26 |
let cst_num loc t q = |
|
| 27 |
{ Ast.expr_desc =
|
|
| 28 |
Ast.Cst(q, Q.to_string q); |
|
| 29 |
expr_loc = loc; |
|
| 30 |
expr_type = t } |
|
| 24 | 31 |
|
| 25 | 32 |
let rec real_to_q man exp = |
| 26 | 33 |
if exp = 0 then |
| ... | ... | |
| 34 | 41 |
|
| 35 | 42 |
let instr_loc i = |
| 36 | 43 |
match i.Machine_code_types.lustre_eq with |
| 37 |
| None -> Tiny.Location.dummy
|
|
| 44 |
| None -> gen_loc ()
|
|
| 38 | 45 |
| Some eq -> lloc_to_tloc eq.eq_loc |
| 39 | 46 |
|
| 40 | 47 |
let rec lval_to_texpr loc _val = |
| 41 | 48 |
let build d v = |
| 42 | 49 |
Ast.{ expr_desc = d;
|
| 43 |
expr_loc = loc;
|
|
| 50 |
expr_loc = gen_loc ();
|
|
| 44 | 51 |
expr_type = v } |
| 45 | 52 |
in |
| 46 | 53 |
let new_desc = |
| ... | ... | |
| 76 | 83 |
Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Zero) |
| 77 | 84 |
| "!=", [v1;v2] -> |
| 78 | 85 |
Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.NonZero) |
| 86 |
| "uminus", [v1] -> Ast.Binop (Ast.Minus, cst_num loc t_arg Q.zero, v1) |
|
| 79 | 87 |
| _ -> Format.eprintf "No tiny translation for operator %s@.@?" op; assert false |
| 80 | 88 |
) |
| 81 | 89 |
| _ -> assert false (* no array. access or power *) |
| ... | ... | |
| 150 | 158 |
| [i] -> instr_to_stm i |
| 151 | 159 |
| i::il -> |
| 152 | 160 |
let i' = instr_to_stm i in |
| 153 |
Ast.Seq (instr_loc i, i', (instrl_to_stm il))
|
|
| 161 |
Ast.Seq (gen_loc (), i', (instrl_to_stm il))
|
|
| 154 | 162 |
in |
| 155 | 163 |
instrl_to_stm m.Machine_code_types.mstep.step_instrs |
| 156 | 164 |
|
| 157 |
let read_var loc bounds_opt v =
|
|
| 165 |
let read_var bounds_opt v = |
|
| 158 | 166 |
let min, max = |
| 159 | 167 |
match bounds_opt with |
| 160 | 168 |
Some (min,max) -> min, max |
| ... | ... | |
| 162 | 170 |
in |
| 163 | 171 |
let range = {
|
| 164 | 172 |
Ast.expr_desc = Ast.Rand (min,max); |
| 165 |
expr_loc = loc;
|
|
| 173 |
expr_loc = gen_loc ();
|
|
| 166 | 174 |
expr_type = ltyp_to_ttyp (v.Lustre_types.var_type) |
| 167 | 175 |
} |
| 168 | 176 |
in |
| 169 |
Ast.Asn (loc, v.var_id, range)
|
|
| 177 |
Ast.Asn (gen_loc (), v.var_id, range)
|
|
| 170 | 178 |
|
| 171 |
let rec read_vars loc bounds_inputs vl =
|
|
| 179 |
let rec read_vars bounds_inputs vl = |
|
| 172 | 180 |
match vl with |
| 173 |
[] -> Ast.Nop loc
|
|
| 181 |
[] -> Ast.Nop (gen_loc ())
|
|
| 174 | 182 |
| [v] -> read_var |
| 175 |
loc |
|
| 176 | 183 |
(if List.mem_assoc v.Lustre_types.var_id bounds_inputs then |
| 177 | 184 |
Some (List.assoc v.Lustre_types.var_id bounds_inputs) |
| 178 | 185 |
else |
| 179 | 186 |
None) |
| 180 | 187 |
v |
| 181 | 188 |
| v::tl -> |
| 182 |
Ast.Seq (loc,
|
|
| 189 |
Ast.Seq (gen_loc (),
|
|
| 183 | 190 |
read_var |
| 184 |
loc |
|
| 185 | 191 |
(if List.mem_assoc v.Lustre_types.var_id bounds_inputs then |
| 186 | 192 |
Some (List.assoc v.Lustre_types.var_id bounds_inputs) |
| 187 | 193 |
else |
| 188 | 194 |
None) |
| 189 | 195 |
v, |
| 190 |
read_vars loc bounds_inputs tl
|
|
| 196 |
read_vars bounds_inputs tl |
|
| 191 | 197 |
) |
| 192 | 198 |
|
| 193 | 199 |
let machine_to_ast bounds_input m = |
| 194 |
let loc = Tiny.Location.dummy in |
|
| 195 |
let read_vars = read_vars loc bounds_input m.Machine_code_types.mstep.step_inputs in |
|
| 200 |
let read_vars = read_vars bounds_input m.Machine_code_types.mstep.step_inputs in |
|
| 196 | 201 |
let ast_loop_first = machine_body_to_ast true m in |
| 197 | 202 |
let ast_loop_run = machine_body_to_ast false m in |
| 198 |
let ast_loop_body = Ast.Seq (loc, read_vars, ast_loop_run) in
|
|
| 199 |
let loop = Ast.While(loc, cst_bool loc true, ast_loop_body) in
|
|
| 200 |
Ast.Seq (loc, read_vars, (Ast.Seq (loc, ast_loop_first, loop)))
|
|
| 203 |
let ast_loop_body = Ast.Seq (gen_loc (), read_vars, ast_loop_run) in
|
|
| 204 |
let loop = Ast.While(gen_loc (), cst_bool (gen_loc ()) true, ast_loop_body) in
|
|
| 205 |
Ast.Seq (gen_loc (), read_vars, (Ast.Seq (gen_loc (), ast_loop_first, loop)))
|
|
| 201 | 206 |
|
| 202 | 207 |
let machine_to_env m = |
| 203 | 208 |
|
Also available in: Unified diff
Added some missing locations in tiny plugin