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_adb.ml
26 26
module Main =
27 27
struct
28 28

  
29
  (** Printing function for basic assignement [var_name := value].
29
  (** Printing function for basic assignement [var := value].
30 30

  
31 31
      @param fmt the formater to print on
32 32
      @param var_name the name of the variable
33 33
      @param value the value to be assigned
34 34
   **)
35
  let pp_basic_assign m fmt var_name value =
35
  let pp_assign env fmt var value =
36 36
    fprintf fmt "%a := %a"
37
      (pp_access_var m) var_name
38
      (pp_value m) value
37
      (pp_var env) var
38
      (pp_value env) value
39 39

  
40 40
  (** Printing function for instruction. See
41 41
      {!type:Machine_code_types.instr_t} for more details on
......
46 46
      @param fmt the formater to print on
47 47
      @param instr the instruction to print
48 48
   **)
49
  let rec pp_machine_instr typed_submachines machine instr fmt =
50
    let pp_instr = pp_machine_instr typed_submachines machine in
49
  let rec pp_machine_instr typed_submachines env instr fmt =
50
    let pp_instr = pp_machine_instr typed_submachines env in
51 51
    (* Print args for a step call *)
52 52
    let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
53 53
    (* Print a when branch of a case *)
......
57 57
    (* Print a case *)
58 58
    let pp_case fmt (g, hl) =
59 59
      fprintf fmt "case %a is@,%aend case"
60
        (pp_value machine) g
60
        (pp_value env) g
61 61
        pp_block (List.map pp_when hl)
62 62
    in
63 63
    (* Print a if *)
......
65 65
       first check that we don't have a negation and a else case, if so it
66 66
       inverses the two branch and remove the negation doing a recursive
67 67
       call. *)
68
    let rec pp_if neg fmt (g, instrs1, instrs2) =
69
      match neg, instrs2 with
70
        | true, Some x -> pp_if false fmt (g, x, Some instrs1)
71
        | _ ->
72
          let pp_cond =
73
            if neg then
74
              fun fmt x -> fprintf fmt "! (%a)" (pp_value machine) x
75
            else
76
              pp_value machine
77
          in
78
          let pp_else = match instrs2 with
79
            | None -> fun fmt -> fprintf fmt ""
80
            | Some i2 -> fun fmt ->
81
                fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
82
          in
83
          fprintf fmt "if %a then@,%a%tend if"
84
            pp_cond g
85
            pp_block (List.map pp_instr instrs1)
86
            pp_else
68
    let pp_if fmt (neg, g, instrs1, instrs2) =
69
      let pp_cond =
70
        if neg then
71
          fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
72
        else
73
          pp_value env
74
      in
75
      let pp_else = match instrs2 with
76
        | None -> fun fmt -> fprintf fmt ""
77
        | Some i2 -> fun fmt ->
78
            fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
79
      in
80
      fprintf fmt "if %a then@,%a%tend if"
81
        pp_cond g
82
        pp_block (List.map pp_instr instrs1)
83
        pp_else
87 84
    in
88 85
    match get_instr_desc instr with
89 86
      (* no reset *)
......
95 92
          let args = if is_machine_statefull submachine then [[pp_state i]] else [] in
96 93
          pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
97 94
      | MLocalAssign (ident, value) ->
98
          pp_basic_assign machine fmt ident value
95
          pp_assign env fmt ident value
99 96
      | MStateAssign (ident, value) ->
100
          pp_basic_assign machine fmt ident value
97
          pp_assign env fmt ident value
101 98
      | MStep ([i0], i, vl) when is_builtin_fun i ->
102 99
          let value = mk_val (Fun (i, vl)) i0.var_type in
103
          pp_basic_assign machine fmt i0 value
100
            pp_assign env fmt i0 value
104 101
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
105 102
          let (substitution, submachine) = get_instance i typed_submachines in
106 103
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
107
          let input = List.map (fun x fmt -> pp_value machine fmt x) vl in
108
          let output = List.map (fun x fmt -> pp_var_name fmt x) il in
104
          let input = List.map (fun x fmt -> pp_value env fmt x) vl in
105
          let output = List.map pp_var_name il in
109 106
          let args =
110 107
            (if is_machine_statefull submachine then [[pp_state i]] else [])
111 108
              @(if input!=[] then [input] else [])
......
114 111
          pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
115 112
      | MBranch (_, []) -> assert false
116 113
      | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
117
          let neg = c1=tag_false in
118
          let other = match tl with
119
            | []         -> None
120
            | [(c2, i2)] -> Some i2
121
            | _          -> assert false
122
          in
123
          pp_if neg fmt (g, i1, other)
114
          pp_if fmt (build_if g c1 i1 tl)
124 115
      | MBranch (g, hl) -> pp_case fmt (g, hl)
125 116
      | MComment s  ->
126 117
          let lines = String.split_on_char '\n' s in
......
133 124
     @param fmt the formater to print on
134 125
     @param machine the machine
135 126
  **)
136
  let pp_step_definition typed_submachines fmt (m, m_spec_opt) =
137
    let spec_instrs = match m_spec_opt with
138
      | None -> []
139
      | Some m -> m.mstep.step_instrs
127
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt) =
128
    let transform_local_to_state_assign instr = match instr.instr_desc with
129
      | MLocalAssign (ident, value) -> 
130
          { instr_desc = MStateAssign (ident, value);
131
            lustre_eq= instr.lustre_eq }
132
      | x -> instr
140 133
    in
141
    let spec_locals = match m_spec_opt with
134
    let spec_instrs = match m_spec_opt with
142 135
      | None -> []
143
      | Some m -> m.mstep.step_locals
136
      | Some m_spec -> List.map transform_local_to_state_assign m_spec.mstep.step_instrs
144 137
    in
145
    let pp_local_list = List.map build_pp_var_decl_local (m.mstep.step_locals@spec_locals) in
146
    let pp_instr_list = List.map (pp_machine_instr typed_submachines m) (m.mstep.step_instrs@spec_instrs) in
138
    let pp_local_list = List.map (build_pp_var_decl_local None) (m.mstep.step_locals) in
139
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (m.mstep.step_instrs@spec_instrs) in
147 140
    let content = AdaProcedureContent ((if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
148 141
    pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
149 142

  
......
153 146
     @param fmt the formater to print on
154 147
     @param machine the machine
155 148
  **)
156
  let pp_reset_definition typed_submachines fmt m =
149
  let pp_reset_definition env typed_submachines fmt m =
157 150
    let build_assign = function var ->
158 151
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
159 152
    in
160 153
    let assigns = List.map build_assign m.mmemory in
161
    let pp_instr_list = List.map (pp_machine_instr typed_submachines m) (assigns@m.minit) in
154
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (assigns@m.minit) in
162 155
    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt (AdaProcedureContent ([], pp_instr_list))
163 156

  
164 157
  (** Print the package definition(ads) of a machine.
......
172 165
     @param m the machine
173 166
  **)
174 167
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
168
    let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
175 169
    let pp_reset fmt =
176 170
      if is_machine_statefull machine then
177
        fprintf fmt "%a;@,@," (pp_reset_definition typed_submachines) machine
171
        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) machine
178 172
      else
179 173
        fprintf fmt ""
180 174
    in
......
194 188
        pp_reset
195 189
        
196 190
        (*Define the step procedure*)
197
        (pp_step_definition typed_submachines) (machine, opt_spec_machine)
191
        (pp_step_definition env typed_submachines) (machine, opt_spec_machine)
198 192
    in
199 193
    fprintf fmt "%a%t%a;@."
200 194
      

Also available in: Unified diff