Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend_common.ml @ 9f77bff7

History | View | Annotate | Download (4.11 KB)

1
(********************************************************************)
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
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id
20

    
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
  | Types.Tarray(dim,ty)   -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")"
29
  | Types.Tstatic(d, ty)-> pp_type fmt ty
30
  | 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
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
51
let rename f = (fun v -> {v with var_id = f v.var_id } )
52
let rename_machine p = rename (fun n -> concat p n)
53
let rename_machine_list p = List.map (rename_machine p)
54

    
55
let rename_current =  rename (fun n -> n ^ "_c")
56
let rename_current_list = List.map rename_current
57
let rename_mid =  rename (fun n -> n ^ "_m")
58
let rename_mid_list = List.map rename_mid
59
let rename_next = rename (fun n -> n ^ "_x")
60
let rename_next_list = List.map rename_next
61

    
62
let get_machine machines node_name =
63
(*  try *)
64
  List.find (fun m  -> m.mname.node_id = node_name) machines
65
(* with Not_found -> Format.eprintf "Unable to find machine %s in machines %a@.@?"  *)
66
(*   node_name *)
67
(*   (Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines *)
68
(*   ; assert false *)
69

    
70
let local_memory_vars machines machine =
71
  rename_machine_list machine.mname.node_id machine.mmemory
72

    
73
let instances_memory_vars ?(without_arrow=false) machines machine =
74
  let rec aux fst prefix m =
75
    (
76
      if not fst then (
77
	(rename_machine_list (concat prefix m.mname.node_id) m.mmemory)
78
      )
79
      else []
80
    ) @
81
      List.fold_left (fun accu (id, (n, _)) ->
82
	let name = node_name n in
83
	if without_arrow && name = "_arrow" then
84
	  accu
85
	else
86
	  let machine_n = get_machine machines name in
87
	  ( aux false (concat prefix
88
			 (if fst then id else concat m.mname.node_id id))
89
	      machine_n ) @ accu
90
      ) [] (m.minstances)
91
  in
92
  aux true machine.mname.node_id machine
93

    
94
let full_memory_vars ?(without_arrow=false) machines machine =
95
  (local_memory_vars machines machine)
96
  @ (instances_memory_vars ~without_arrow machines machine)
97

    
98
let inout_vars machines m =
99
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)
100
  @ (rename_machine_list m.mname.node_id m.mstep.step_outputs)
101

    
102
let step_vars machines m =
103
  (inout_vars machines m)
104
  @ (rename_current_list (full_memory_vars machines m))
105
  @ (rename_next_list (full_memory_vars machines m))
106

    
107
let step_vars_m_x machines m =
108
  (inout_vars machines m)
109
  @ (rename_mid_list (full_memory_vars machines m))
110
  @ (rename_next_list (full_memory_vars machines m))
111

    
112
let reset_vars machines m =
113
  (rename_current_list (full_memory_vars machines m))
114
  @ (rename_mid_list (full_memory_vars machines m))
115

    
116

    
117
(* Local Variables: *)
118
(* compile-command:"make -C ../.." *)
119
(* End: *)