Project

General

Profile

« Previous | Next » 

Revision b5b745fb

Added by Guillaume DAVY over 4 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