Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend_common.ml @ 550e6a83

History | View | Annotate | Download (5.25 KB)

1 85a6f473 Teme
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11
12
open Format
13
open LustreSpec
14
open Corelang
15
open Machine_code
16
17
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
18
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
19 07ceae4c ploc
let pp_machine_stateless_name fmt id = fprintf fmt "%s_fun" id
20 85a6f473 Teme
21
let rec pp_type fmt t =
22
  match (Types.repr t).Types.tdesc with
23
  | Types.Tbool           -> fprintf fmt "Bool"
24
  | Types.Tint            -> fprintf fmt "Int"
25
  | Types.Treal           -> fprintf fmt "Real"
26
  | Types.Tconst ty       -> pp_print_string fmt ty
27
  | Types.Tclock t        -> pp_type fmt t
28 84902260 jbraine
  | Types.Tarray(dim,ty)   -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")"
29
  | Types.Tstatic(d, ty)-> pp_type fmt ty
30 85a6f473 Teme
  | Types.Tarrow _
31
  | _                     -> eprintf "internal error: pp_type %a@."
32
    Types.print_ty t; assert false
33
34
let pp_decl_var fmt id =
35
  fprintf fmt "(declare-var %s %a)"
36
    id.var_id
37
    pp_type id.var_type
38
39
(* let pp_var fmt id = pp_print_string fmt id.var_id  *)
40
41
42
let pp_conj pp fmt l =
43
  match l with
44
    [] -> assert false
45
  | [x] -> pp fmt x
46
  | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:"@ " pp) l
47
48
49
50 a6974c82 ploc
(********************************************************************************************)
51
(*                    Workaround to prevent the use of declared keywords as node name       *)
52
(********************************************************************************************)
53
let registered_keywords = ["implies"]
54
55
let protect_kwd s = 
56
  if List.mem s registered_keywords then
57
    "__" ^ s
58
  else
59
    s
60
61
let node_name n =
62
  let name = node_name n in
63
  protect_kwd name
64
65
66 85a6f473 Teme
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
67
let rename f = (fun v -> {v with var_id = f v.var_id } )
68
let rename_machine p = rename (fun n -> concat p n)
69
let rename_machine_list p = List.map (rename_machine p)
70
71
let rename_current =  rename (fun n -> n ^ "_c")
72
let rename_current_list = List.map rename_current
73
let rename_mid =  rename (fun n -> n ^ "_m")
74
let rename_mid_list = List.map rename_mid
75
let rename_next = rename (fun n -> n ^ "_x")
76
let rename_next_list = List.map rename_next
77
78
let get_machine machines node_name =
79 0dee2bc1 ploc
(*  try *)
80 85a6f473 Teme
  List.find (fun m  -> m.mname.node_id = node_name) machines
81 0dee2bc1 ploc
(* with Not_found -> Format.eprintf "Unable to find machine %s in machines %a@.@?"  *)
82
(*   node_name *)
83
(*   (Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines *)
84
(*   ; assert false *)
85 85a6f473 Teme
86
let local_memory_vars machines machine =
87
  rename_machine_list machine.mname.node_id machine.mmemory
88 0dee2bc1 ploc
    
89
let instances_memory_vars ?(without_arrow=false) machines machine =
90 85a6f473 Teme
  let rec aux fst prefix m =
91
    (
92
      if not fst then (
93
	(rename_machine_list (concat prefix m.mname.node_id) m.mmemory)
94
      )
95
      else []
96
    ) @
97
      List.fold_left (fun accu (id, (n, _)) ->
98
	let name = node_name n in
99
	if without_arrow && name = "_arrow" then
100 0dee2bc1 ploc
	  accu 
101 85a6f473 Teme
	else
102
	  let machine_n = get_machine machines name in
103 0dee2bc1 ploc
	  ( aux false (concat prefix 
104 85a6f473 Teme
			 (if fst then id else concat m.mname.node_id id))
105
	      machine_n ) @ accu
106
      ) [] (m.minstances)
107
  in
108
  aux true machine.mname.node_id machine
109
110 d7e04983 Ploc
(* Extract the arrows of a given node/machine *)
111
let arrow_vars machines machine : LustreSpec.var_decl list =
112
  let rec aux fst prefix m =
113
    List.fold_left (fun accu (id, (n, _)) ->
114
      let name = node_name n in
115
      if name = "_arrow" then
116
	let arrow_machine = Machine_code.arrow_machine in
117
	(rename_machine_list
118
	  (concat prefix (concat (if fst then id else concat m.mname.node_id id) "_arrow"))
119
	  arrow_machine.mmemory
120
	) @ accu
121
      else
122
	let machine_n = get_machine machines name in
123
	( aux false (concat prefix
124
		       (if fst then id else concat m.mname.node_id id))
125
	    machine_n ) @ accu
126
    ) [] (m.minstances)
127
  in
128
  aux true machine.mname.node_id machine
129
130 85a6f473 Teme
let full_memory_vars ?(without_arrow=false) machines machine =
131
  (local_memory_vars machines machine)
132
  @ (instances_memory_vars ~without_arrow machines machine)
133
134
let inout_vars machines m =
135
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)
136
  @ (rename_machine_list m.mname.node_id m.mstep.step_outputs)
137
138
let step_vars machines m =
139
  (inout_vars machines m)
140 0dee2bc1 ploc
  @ (rename_current_list (full_memory_vars machines m)) 
141 85a6f473 Teme
  @ (rename_next_list (full_memory_vars machines m))
142
143
let step_vars_m_x machines m =
144
  (inout_vars machines m)
145 0dee2bc1 ploc
  @ (rename_mid_list (full_memory_vars machines m)) 
146 85a6f473 Teme
  @ (rename_next_list (full_memory_vars machines m))
147
148
let reset_vars machines m =
149 0dee2bc1 ploc
  (rename_current_list (full_memory_vars machines m)) 
150 85a6f473 Teme
  @ (rename_mid_list (full_memory_vars machines m))
151
152
153
(* Local Variables: *)
154
(* compile-command:"make -C ../.." *)
155
(* End: *)