Project

General

Profile

« Previous | Next » 

Revision 6cbbe1c1

Added by LĂ©lio Brun 8 months ago

start again with spec representation

View differences:

src/machine_code_common.ml
3 3
open Spec_types
4 4
open Spec_common
5 5
open Corelang
6
  
6
open Utils.Format
7

  
7 8
let print_statelocaltag = true
8 9

  
9 10
let is_memory m id =
......
16 17
  | Var v    ->
17 18
     if is_memory m v then
18 19
       if print_statelocaltag then
19
	 Format.fprintf fmt "%s(S)" v.var_id
20
	 fprintf fmt "{%s}" v.var_id
20 21
       else
21
	 Format.pp_print_string fmt v.var_id 
22
	 pp_print_string fmt v.var_id
22 23
     else     
23 24
       if print_statelocaltag then
24
	 Format.fprintf fmt "%s(L)" v.var_id
25
	 fprintf fmt "%s" v.var_id
25 26
       else
26
	 Format.pp_print_string fmt v.var_id
27
  | Array vl      -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val)  vl
28
  | Access (t, i) -> Format.fprintf fmt "%a[%a]" pp_val t pp_val i
29
  | Power (v, n)  -> Format.fprintf fmt "(%a^%a)" pp_val v pp_val n
30
  | Fun (n, vl)   -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val)  vl
27
	 pp_print_string fmt v.var_id
28
  | Array vl      -> fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val)  vl
29
  | Access (t, i) -> fprintf fmt "%a[%a]" pp_val t pp_val i
30
  | Power (v, n)  -> fprintf fmt "(%a^%a)" pp_val v pp_val n
31
  | Fun (n, vl)   -> fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val)  vl
32

  
33
module PrintSpec = PrintSpec(struct
34
    type t = value_t
35
    type ctx = machine_t
36
    let pp_val = pp_val
37
  end)
31 38

  
32 39
let rec  pp_instr m fmt i =
33 40
 let     pp_val = pp_val m and
34 41
      pp_branch = pp_branch m in
35 42
  let _ =
36 43
    match i.instr_desc with
37
    | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
38
    | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
39
    | MReset i           -> Format.fprintf fmt "reset %s" i
40
    | MNoReset i         -> Format.fprintf fmt "noreset %s" i
44
    | MLocalAssign (i,v) -> fprintf fmt "%s := %a" i.var_id pp_val v
45
    | MStateAssign (i,v) -> fprintf fmt "{%s} := %a" i.var_id pp_val v
46
    | MReset i           -> fprintf fmt "reset %s" i
47
    | MNoReset i         -> fprintf fmt "noreset %s" i
41 48
    | MStep (il, i, vl)  ->
42
       Format.fprintf fmt "%a = %s (%a)"
43
	 (Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
49
       fprintf fmt "%a = %s (%a)"
50
	 (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) il
44 51
	 i
45 52
	 (Utils.fprintf_list ~sep:", " pp_val) vl
46 53
    | MBranch (g,hl)     ->
47
       Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
54
       fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
48 55
	 pp_val g
49 56
	 (Utils.fprintf_list ~sep:"@," pp_branch) hl
50
    | MComment s -> Format.pp_print_string fmt s
51
    | MSpec s -> Format.pp_print_string fmt ("@" ^ s)
57
    | MComment s -> pp_print_string fmt s
58
    | MSpec s -> pp_print_string fmt ("@" ^ s)
52 59
       
53 60
  in
54 61
  (* Annotation *)
55 62
  (* let _ = *)
56
  (*   match i.lustre_expr with None -> () | Some e -> Format.fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
63
  (*   match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
57 64
  (* in *)
58
  let _ = 
59
    match i.lustre_eq with None -> () | Some eq -> Format.fprintf fmt " -- original eq: %a" Printers.pp_node_eq eq
60
  in
61
  ()
62
    
65
  begin match i.lustre_eq with
66
  | None -> ()
67
  | Some eq -> fprintf fmt " -- original eq: %a" Printers.pp_node_eq eq
68
  end;
69
  fprintf fmt "@ --%@ %a" (PrintSpec.pp_spec m) i.instr_spec
70

  
71

  
63 72
and pp_branch m fmt (t, h) =
64
  Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," (pp_instr m)) h
73
  fprintf fmt "@[<v 2>%s:@,%a@]" t
74
    (pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)) h
65 75

  
66
and pp_instrs m fmt il =
67
  Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," (pp_instr m)) il
76
let pp_instrs m =
77
  pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)
68 78

  
69 79

  
70 80
(* merge log: get_node_def was in c0f8 *)
......
74 84
    let (decl, _) = List.assoc id m.mcalls in
75 85
    Corelang.node_of_top decl
76 86
  with Not_found -> ( 
77
    (* Format.eprintf "Unable to find node %s in list [%a]@.@?" *)
87
    (* eprintf "Unable to find node %s in list [%a]@.@?" *)
78 88
    (*   id *)
79
    (*   (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> Format.fprintf fmt "%s" n)) m.mcalls *)
89
    (*   (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> fprintf fmt "%s" n)) m.mcalls *)
80 90
    (* ; *)
81 91
    raise Not_found
82 92
  )
......
85 95
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
86 96

  
87 97
let pp_step m fmt s =
88
  Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
89
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs
90
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs
91
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals
92
    (Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val m fmt c)) s.step_checks
93
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) s.step_instrs
94
    (Utils.fprintf_list ~sep:", " (pp_val m)) s.step_asserts
98
  let pp_list = pp_print_list ~pp_sep:pp_print_comma in
99
  fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
100
    (pp_list Printers.pp_var) s.step_inputs
101
    (pp_list Printers.pp_var) s.step_outputs
102
    (pp_list Printers.pp_var) s.step_locals
103
    (pp_list (fun fmt (_, c) -> pp_val m fmt c))
104
    s.step_checks
105
    (pp_instrs m) s.step_instrs
106
    (pp_list (pp_val m)) s.step_asserts
95 107

  
96 108

  
97 109
let pp_static_call fmt (node, args) =
98
 Format.fprintf fmt "%s<%a>"
110
 fprintf fmt "%s<%a>"
99 111
   (node_name node)
100 112
   (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args
101 113

  
102 114
let pp_machine fmt m =
103
  Format.fprintf fmt
115
  fprintf fmt
104 116
    "@[<v 2>machine %s@ \
105 117
     mem      : %a@ \
106 118
     instances: %a@ \
......
112 124
     annot    : @[%a@]@]@ "
113 125
    m.mname.node_id
114 126
    (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
115
    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
127
    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
116 128
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.minit
117 129
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.mconst
118 130
    (pp_step m) m.mstep
119 131
    (fun fmt -> match m.mspec.mnode_spec with
120 132
       | None -> ()
121
       | Some (NodeSpec id) -> Format.fprintf fmt "cocospec: %s" id
133
       | Some (NodeSpec id) -> fprintf fmt "cocospec: %s" id
122 134
       | Some (Contract spec) -> Printers.pp_spec fmt spec)
123 135
    (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
124 136

  
125 137
let pp_machines fmt ml =
126
  Format.fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml
138
  fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml
127 139

  
128 140
  
129 141
let rec is_const_value v =
......
159 171

  
160 172
let mk_conditional ?lustre_eq c t e =
161 173
  mkinstr ?lustre_eq
162
    (Ternary (Val c,
163
              And (List.map get_instr_spec t),
164
              And (List.map get_instr_spec e)))
174
    (* (Ternary (Val c,
175
     *           And (List.map get_instr_spec t),
176
     *           And (List.map get_instr_spec e))) *)
177
    True
165 178
    (MBranch(c, [
166 179
         (tag_true, t);
167 180
         (tag_false, e) ]))
168 181

  
169 182
let mk_branch ?lustre_eq c br =
170 183
  mkinstr ?lustre_eq
171
    (And (List.map (fun (l, instrs) ->
172
         Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
173
         br))
184
    (* (And (List.map (fun (l, instrs) ->
185
     *      Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
186
     *      br)) *)
187
    True
174 188
    (MBranch (c, br))
175 189

  
176 190
let mk_assign ?lustre_eq x v =
177 191
  mkinstr ?lustre_eq
178
    (Equal (Var x, Val v))
192
    (* (Equal (Var x, Val v)) *)
193
    True
179 194
    (MLocalAssign (x, v))
180 195

  
181 196
let mk_val v t =
......
290 305
 try
291 306
    Utils.desome (get_machine_opt machines node_name) 
292 307
 with Utils.DeSome ->
293
   Format.eprintf "Unable to find machine %s in machines %a@.@?"
308
   eprintf "Unable to find machine %s in machines %a@.@?"
294 309
     node_name
295
     (Utils.fprintf_list ~sep:", " (fun fmt m -> Format.pp_print_string fmt m.mname.node_id)) machines
310
     (Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines
296 311
      ; assert false
297 312
     
298 313
let get_const_assign m id =

Also available in: Unified diff