Project

General

Profile

Download (2.73 KB) Statistics
| Branch: | Tag: | Revision:
1
open Format
2
open LustreSpec
3
open Corelang
4
open Machine_code
5

    
6

    
7
let pp_type fmt t =
8
  match (Types.repr t).Types.tdesc with
9
  | Types.Tbool           -> Format.fprintf fmt "Bool"
10
  | Types.Tint            -> Format.fprintf fmt "Int"
11
  | Types.Tclock _
12
  | Types.Tarray _
13
  | Types.Tstatic _
14
  | Types.Tconst _
15
  | Types.Tarrow _
16
  | _                     -> Format.eprintf "internal error: pp_type %a@." Types.print_ty t; assert false
17
    
18

    
19
let pp_decl_var fmt id = 
20
  Format.fprintf fmt "(declare_var %s %a)"
21
    id.var_id
22
    pp_type id.var_type
23

    
24
let pp_var fmt id = Format.pp_print_string fmt id.var_id
25

    
26
let pp_instr machine_name fmt i =
27
  Format.fprintf fmt "(xxx)"
28

    
29
let rename f = List.map (fun v -> {v with var_id = f v.var_id } )
30
let rename_current machine_name = rename (fun n -> machine_name ^ "." ^ n ^ "_c")
31
let rename_next machine_name = rename (fun n -> machine_name ^ "." ^ n ^ "_x")
32
let rename_machine machine_name = rename (fun n -> machine_name ^ "." ^ n)
33

    
34
let machine_vars m = 
35
  (rename_current m.mname.node_id m.mstatic)@
36
    (rename_next m.mname.node_id m.mstatic)@
37
    (rename_machine m.mname.node_id m.mstep.step_inputs)@
38
    (rename_machine m.mname.node_id m.mstep.step_outputs)
39
    
40
(* Print the machine m: 
41
   two functions: m_init and m_step
42
   - m_init is a predicate over m memories
43
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
44
   We first declare all variables then the two /rules/.
45
*)
46
let print_machine fmt m = 
47
 if m.mname.node_id = arrow_id then () else ( (* We don't print arrow function *)
48
   Format.fprintf fmt "; %s@." m.mname.node_id;
49
   (* Printing variables *)
50
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt 
51
     ((machine_vars m)@(rename_machine m.mname.node_id m.mstep.step_locals));
52

    
53
   (* Declaring predicate *)
54
   Format.fprintf fmt "(declare-rel %s_init (%a))@."
55
     m.mname.node_id
56
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) m.mstatic);
57
   
58
   Format.fprintf fmt "(declare-rel %s_step (%a))@."
59
     m.mname.node_id
60
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (machine_vars m));
61

    
62
   Format.fprintf fmt "(rule (=> (and %a) (%s_init %a)))"
63
     (Utils.fprintf_list ~sep:"@." (pp_instr m.mname.node_id)) m.minit
64
     m.mname.node_id
65
     (Utils.fprintf_list ~sep:" " pp_var) (rename_machine m.mname.node_id m.mstatic);
66

    
67
   Format.fprintf fmt "(rule (=> (and %a) (%s_step %a)))"
68
     (Utils.fprintf_list ~sep:"@." (pp_instr m.mname.node_id)) m.mstep.step_instrs
69
     m.mname.node_id
70
     (Utils.fprintf_list ~sep:" " pp_var) (machine_vars m);
71
   
72
()
73
  )
74

    
75
let main_print fmt = ()
76

    
77
let translate fmt basename prog machines =
78
  List.iter (print_machine fmt) machines;
79
  main_print fmt 
80

    
81

    
82
(* Local Variables: *)
83
(* compile-command:"make -C .." *)
84
(* End: *)
(20-20/45)