Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/backends/Horn/horn_backend_common.ml
17 17
let get_machine = Machine_code_common.get_machine
18 18

  
19 19
let machine_reset_name id = id ^ "_reset"
20
let machine_step_name id = id ^ "_step" 
21
let machine_stateless_name id = id ^ "_fun" 
20

  
21
let machine_step_name id = id ^ "_step"
22

  
23
let machine_stateless_name id = id ^ "_fun"
24

  
22 25
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
26

  
23 27
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
28

  
24 29
let pp_machine_stateless_name fmt id = fprintf fmt "%s_fun" id
25 30

  
26 31
let rec pp_type fmt t =
27
  if Types.is_bool_type t  then fprintf fmt "Bool" else
28
  if Types.is_int_type t then fprintf fmt "Int" else 
29
  if Types.is_real_type t then fprintf fmt "Real" else 
30
  match (Types.repr t).Types.tdesc with
31
  | Types.Tconst ty       -> pp_print_string fmt ty
32
  | Types.Tclock t        -> pp_type fmt t
33
  | Types.Tarray(_,ty)    -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")"
34
  | Types.Tstatic(_, ty)  -> pp_type fmt ty
35
  | Types.Tarrow _
36
  | _                     -> eprintf "internal error: pp_type %a@."
37
    Types.print_ty t; assert false
32
  if Types.is_bool_type t then fprintf fmt "Bool"
33
  else if Types.is_int_type t then fprintf fmt "Int"
34
  else if Types.is_real_type t then fprintf fmt "Real"
35
  else
36
    match (Types.repr t).Types.tdesc with
37
    | Types.Tconst ty ->
38
      pp_print_string fmt ty
39
    | Types.Tclock t ->
40
      pp_type fmt t
41
    | Types.Tarray (_, ty) ->
42
      fprintf fmt "(Array Int ";
43
      pp_type fmt ty;
44
      fprintf fmt ")"
45
    | Types.Tstatic (_, ty) ->
46
      pp_type fmt ty
47
    | Types.Tarrow _ | _ ->
48
      eprintf "internal error: pp_type %a@." Types.print_ty t;
49
      assert false
38 50

  
39 51
let pp_decl_var fmt id =
40
  fprintf fmt "(declare-var %s %a)"
41
    id.var_id
42
    pp_type id.var_type
43

  
44
(* let pp_var fmt id = pp_print_string fmt id.var_id  *)
52
  fprintf fmt "(declare-var %s %a)" id.var_id pp_type id.var_type
45 53

  
54
(* let pp_var fmt id = pp_print_string fmt id.var_id *)
46 55

  
47 56
let pp_conj pp fmt l =
48 57
  match l with
49
    [] -> assert false
50
  | [x] -> pp fmt x
51
  | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:"@ " pp) l
52

  
53

  
58
  | [] ->
59
    assert false
60
  | [ x ] ->
61
    pp fmt x
62
  | _ ->
63
    fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:"@ " pp) l
54 64

  
55 65
(********************************************************************************************)
56
(*                    Workaround to prevent the use of declared keywords as node name       *)
66
(* Workaround to prevent the use of declared keywords as node name *)
57 67
(********************************************************************************************)
58
let registered_keywords = ["implies"]
68
let registered_keywords = [ "implies" ]
59 69

  
60
let protect_kwd s = 
61
  if List.mem s registered_keywords then
62
    "__" ^ s
63
  else
64
    s
70
let protect_kwd s = if List.mem s registered_keywords then "__" ^ s else s
65 71

  
66 72
let node_name n =
67 73
  let name = node_name n in
68 74
  protect_kwd name
69 75

  
70

  
71 76
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
72
let rename f = (fun v -> {v with var_id = f v.var_id } )
77

  
78
let rename f v = { v with var_id = f v.var_id }
79

  
73 80
let rename_machine p = rename (fun n -> concat p n)
81

  
74 82
let rename_machine_list p = List.map (rename_machine p)
75 83

  
76
let rename_current =  rename (fun n -> n ^ "_c")
84
let rename_current = rename (fun n -> n ^ "_c")
85

  
77 86
let rename_current_list = List.map rename_current
78
let rename_mid =  rename (fun n -> n ^ "_m")
87

  
88
let rename_mid = rename (fun n -> n ^ "_m")
89

  
79 90
let rename_mid_list = List.map rename_mid
91

  
80 92
let rename_next = rename (fun n -> n ^ "_x")
81
let rename_next_list = List.map rename_next
82 93

  
94
let rename_next_list = List.map rename_next
83 95

  
84 96
let local_memory_vars machine =
85 97
  rename_machine_list machine.mname.node_id machine.mmemory
86
    
87
let instances_memory_vars ?(without_arrow=false) machines machine =
98

  
99
let instances_memory_vars ?(without_arrow = false) machines machine =
88 100
  let rec aux fst prefix m =
89
    (
90
      if not fst then (
91
	(rename_machine_list (concat prefix m.mname.node_id) m.mmemory)
92
      )
93
      else []
94
    ) @
95
      List.fold_left (fun accu (id, (n, _)) ->
96
	let name = node_name n in
97
	if without_arrow && name = "_arrow" then
98
	  accu 
99
	else
100
	  let machine_n = get_machine machines name in
101
	  ( aux false (concat prefix 
102
			 (if fst then id else concat m.mname.node_id id))
103
	      machine_n ) @ accu
104
      ) [] (m.minstances)
101
    (if not fst then
102
     rename_machine_list (concat prefix m.mname.node_id) m.mmemory
103
    else [])
104
    @ List.fold_left
105
        (fun accu (id, (n, _)) ->
106
          let name = node_name n in
107
          if without_arrow && name = "_arrow" then accu
108
          else
109
            let machine_n = get_machine machines name in
110
            aux false
111
              (concat prefix (if fst then id else concat m.mname.node_id id))
112
              machine_n
113
            @ accu)
114
        [] m.minstances
105 115
  in
106 116
  aux true machine.mname.node_id machine
107 117

  
108 118
(* Extract the arrows of a given node/machine *)
109 119
let arrow_vars machines machine : Lustre_types.var_decl list =
110 120
  let rec aux fst prefix m =
111
    List.fold_left (fun accu (id, (n, _)) ->
112
      let name = node_name n in
113
      if name = "_arrow" then
114
	let arrow_machine = Machine_code_common.arrow_machine in
115
	(rename_machine_list
116
	  (concat prefix (concat (if fst then id else concat m.mname.node_id id) "_arrow"))
117
	  arrow_machine.mmemory
118
	) @ accu
119
      else
120
	let machine_n = get_machine machines name in
121
	( aux false (concat prefix
122
		       (if fst then id else concat m.mname.node_id id))
123
	    machine_n ) @ accu
124
    ) [] (m.minstances)
121
    List.fold_left
122
      (fun accu (id, (n, _)) ->
123
        let name = node_name n in
124
        if name = "_arrow" then
125
          let arrow_machine = Machine_code_common.arrow_machine in
126
          rename_machine_list
127
            (concat prefix
128
               (concat (if fst then id else concat m.mname.node_id id) "_arrow"))
129
            arrow_machine.mmemory
130
          @ accu
131
        else
132
          let machine_n = get_machine machines name in
133
          aux false
134
            (concat prefix (if fst then id else concat m.mname.node_id id))
135
            machine_n
136
          @ accu)
137
      [] m.minstances
125 138
  in
126 139
  aux true machine.mname.node_id machine
127 140

  
128
let full_memory_vars ?(without_arrow=false) machines machine =
129
  (local_memory_vars machine)
130
  @ (instances_memory_vars ~without_arrow machines machine)
141
let full_memory_vars ?(without_arrow = false) machines machine =
142
  local_memory_vars machine
143
  @ instances_memory_vars ~without_arrow machines machine
131 144

  
132 145
let inout_vars m =
133
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)
134
  @ (rename_machine_list m.mname.node_id m.mstep.step_outputs)
146
  rename_machine_list m.mname.node_id m.mstep.step_inputs
147
  @ rename_machine_list m.mname.node_id m.mstep.step_outputs
135 148

  
136 149
let step_vars machines m =
137
  (inout_vars m)
138
  @ (rename_current_list (full_memory_vars machines m)) 
139
  @ (rename_next_list (full_memory_vars machines m))
150
  inout_vars m
151
  @ rename_current_list (full_memory_vars machines m)
152
  @ rename_next_list (full_memory_vars machines m)
140 153

  
141 154
let step_vars_m_x machines m =
142
  (inout_vars m)
143
  @ (rename_mid_list (full_memory_vars machines m)) 
144
  @ (rename_next_list (full_memory_vars machines m))
155
  inout_vars m
156
  @ rename_mid_list (full_memory_vars machines m)
157
  @ rename_next_list (full_memory_vars machines m)
145 158

  
146 159
let reset_vars machines m =
147
  (rename_current_list (full_memory_vars machines m)) 
148
  @ (rename_mid_list (full_memory_vars machines m))
160
  rename_current_list (full_memory_vars machines m)
161
  @ rename_mid_list (full_memory_vars machines m)
149 162

  
150 163
let step_vars_c_m_x machines m =
151
  (inout_vars m)
152
  @ (rename_current_list (full_memory_vars machines m)) 
153
  @ (rename_mid_list (full_memory_vars machines m)) 
154
  @ (rename_next_list (full_memory_vars machines m))
155

  
164
  inout_vars m
165
  @ rename_current_list (full_memory_vars machines m)
166
  @ rename_mid_list (full_memory_vars machines m)
167
  @ rename_next_list (full_memory_vars machines m)
156 168

  
157 169
(* Local Variables: *)
158 170
(* compile-command:"make -C ../.." *)

Also available in: Unified diff