Project

General

Profile

« Previous | Next » 

Revision b5b745fb

Added by Guillaume DAVY almost 3 years ago

Ada: First support for transition predicate generation.

View differences:

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