Project

General

Profile

« Previous | Next » 

Revision dcbf9d3a

Added by Pierre-Loïc Garoche almost 8 years ago

The missing file

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@142 041b043f-8d7c-46b2-b46e-ef0dd855326e

View differences:

src/horn_backend.ml
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: *)

Also available in: Unified diff