Revision b5b745fb
Added by Guillaume DAVY over 4 years ago
| src/backends/Ada/ada_backend_wrapper.ml | ||
|---|---|---|
| 43 | 43 |
(* Locals *) |
| 44 | 44 |
let locals = |
| 45 | 45 |
[[build_text_io_package_local "Integer";build_text_io_package_local "Float"]] |
| 46 |
@(if statefull then [[AdaLocalVar (build_pp_state_decl_from_subinstance (asprintf "%t" pp_state_name, ([], machine)))]] else []) |
|
| 47 |
@(if machine.mstep.step_inputs != [] then [List.map build_pp_var_decl_local machine.mstep.step_inputs] else [])
|
|
| 48 |
@(if machine.mstep.step_outputs != [] then [List.map build_pp_var_decl_local machine.mstep.step_outputs] else [])
|
|
| 46 |
@(if statefull then [[AdaLocalVar (build_pp_state_decl_from_subinstance AdaNoMode None (asprintf "%t" pp_state_name, ([], machine)))]] else [])
|
|
| 47 |
@(if machine.mstep.step_inputs != [] then [List.map (build_pp_var_decl_local None) machine.mstep.step_inputs] else [])
|
|
| 48 |
@(if machine.mstep.step_outputs != [] then [List.map (build_pp_var_decl_local None) machine.mstep.step_outputs] else [])
|
|
| 49 | 49 |
in |
| 50 | 50 |
|
| 51 | 51 |
(* Stream instructions *) |
| ... | ... | |
| 54 | 54 |
let pp_read fmt var = |
| 55 | 55 |
match get_basic var with |
| 56 | 56 |
| Types.Basic.Tbool -> |
| 57 |
fprintf fmt "%a := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
|
|
| 58 |
pp_var_name var
|
|
| 57 |
fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
|
|
| 58 |
(pp_var_name var)
|
|
| 59 | 59 |
| _ -> |
| 60 |
fprintf fmt "%a := %a'Value(Ada.Text_IO.Get_Line)"
|
|
| 61 |
pp_var_name var
|
|
| 60 |
fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)"
|
|
| 61 |
(pp_var_name var)
|
|
| 62 | 62 |
pp_var_type var |
| 63 | 63 |
in |
| 64 | 64 |
let pp_write fmt var = |
| 65 | 65 |
match get_basic var with |
| 66 | 66 |
| Types.Basic.Tbool -> |
| 67 |
fprintf fmt "Ada.Text_IO.Put_Line(\"'%a': '\" & (if %a then \"1\" else \"0\") & \"' \")"
|
|
| 68 |
pp_var_name var
|
|
| 69 |
pp_var_name var
|
|
| 67 |
fprintf fmt "Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \"' \")"
|
|
| 68 |
(pp_var_name var)
|
|
| 69 |
(pp_var_name var)
|
|
| 70 | 70 |
| Types.Basic.Tint -> |
| 71 |
fprintf fmt "Ada.Text_IO.Put(\"'%a': '\");@,Integer_IO.Put(%a);@,Ada.Text_IO.Put_Line(\"' \")"
|
|
| 72 |
pp_var_name var
|
|
| 73 |
pp_var_name var
|
|
| 71 |
fprintf fmt "Ada.Text_IO.Put(\"'%t': '\");@,Integer_IO.Put(%t);@,Ada.Text_IO.Put_Line(\"' \")"
|
|
| 72 |
(pp_var_name var)
|
|
| 73 |
(pp_var_name var)
|
|
| 74 | 74 |
| Types.Basic.Treal -> |
| 75 |
fprintf fmt "Ada.Text_IO.Put(\"'%a': '\");@,Float_IO.Put(%a, Fore=>0, Aft=> 15, Exp => 0);@,Ada.Text_IO.Put_Line(\"' \")"
|
|
| 76 |
pp_var_name var
|
|
| 77 |
pp_var_name var
|
|
| 75 |
fprintf fmt "Ada.Text_IO.Put(\"'%t': '\");@,Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,Ada.Text_IO.Put_Line(\"' \")"
|
|
| 76 |
(pp_var_name var)
|
|
| 77 |
(pp_var_name var)
|
|
| 78 | 78 |
| Types.Basic.Tstring | Types.Basic.Trat -> assert false (* Could not be the top level inputs *) |
| 79 | 79 |
in |
| 80 | 80 |
|
| 81 | 81 |
(* Loop instructions *) |
| 82 | 82 |
let pp_loop fmt = |
| 83 |
let args = pp_state_name::(List.map (fun x fmt -> pp_var_name fmt x) (machine.mstep.step_inputs@machine.mstep.step_outputs)) in
|
|
| 83 |
let args = pp_state_name::(List.map pp_var_name (machine.mstep.step_inputs@machine.mstep.step_outputs)) in
|
|
| 84 | 84 |
fprintf fmt "while not Ada.Text_IO.End_Of_File loop@, @[<v>%a;@,%a;@,%a;@]@,end loop" |
| 85 | 85 |
(Utils.fprintf_list ~sep:";@," pp_read) machine.mstep.step_inputs |
| 86 | 86 |
pp_call (pp_package_access (pp_package, pp_step_procedure_name), [args]) |
Also available in: Unified diff
Ada: First support for transition predicate generation.