Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal_utils.ml @ a703ed0c

History | View | Annotate | Download (3.41 KB)

1
open Lustre_types
2
open Utils
3
   
4

    
5
let compute_sliced_vars vars_to_keep deps nd =
6
  let is_variable vid = 
7
    List.exists
8
      (fun v -> v.var_id = vid)
9
      nd.node_locals
10
  in
11
  let find_variable vid = 
12
      List.find
13
        (fun v -> v.var_id = vid)
14
        nd.node_locals
15
  in  
16

    
17
  (* Returns the vars required to compute v. 
18
     Memories are specifically identified. *)
19
  let coi_var v =
20
    let vname = v.var_id in
21
    let sliced_deps =
22
      Causality.slice_graph deps vname
23
    in
24
    Format.eprintf "sliced graph for %a: %a@."
25
      Printers.pp_var v
26
      Causality.pp_dep_graph sliced_deps;
27
    let vset, memset =
28
      IdentDepGraph.fold_vertex
29
        (fun vname (vset,memset)  ->
30
          if Causality.ExprDep.is_read_var vname
31
          then
32
            let vname' = String.sub vname 1 (-1 + String.length vname) in
33
            if is_variable vname' then
34
              ISet.add vname' vset,
35
              ISet.add vname' memset
36
            else
37
              vset, memset
38
          else
39
            ISet.add vname vset, memset
40
        )
41
        sliced_deps
42
        (ISet.singleton vname, ISet.empty)
43
    in
44
    Format.eprintf "COI of var %s: (%a // %a)@."
45
      v.var_id
46
      (fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements vset)
47
      (fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements memset)
48
    ;
49
      vset, memset
50
  in
51

    
52
  (* Computes the variables required to compute
53
     vl. Variables /seen/ do not need to 
54
     be computed *) 
55
  let rec coi_vars vl seen = 
56
    List.fold_left
57
      (fun accu v ->
58
        let vset, memset = coi_var v in
59
        (* We handle the new mems 
60
           discovered in  the coi *)
61
        let memset =
62
          ISet.filter (
63
              fun vid ->
64
              not
65
                (List.exists
66
                   (fun v -> v.var_id = vid)
67
                   vl
68
                ) 
69
            ) memset
70
        in
71
        let memset_vars = 
72
          ISet.fold (
73
              fun vid accu ->
74
              (find_variable vid)::accu
75
            ) memset [] 
76
        in
77
        let vset' =
78
          coi_vars memset_vars (vl@seen)
79
        in
80
        ISet.union accu (ISet.union vset vset')
81
      )
82
      ISet.empty
83
      (List.filter
84
         (fun v -> not (List.mem v seen))
85
         vl
86
      )
87
  in
88
  ISet.elements (coi_vars vars_to_keep []) 
89

    
90

    
91
  (* If existing outputs are included in vars_to_keep, just slice the content.
92
   Otherwise outputs are replaced by vars_to_keep *)
93
let slice_node vars_to_keep deps nd =
94
  let coi_vars =
95
    compute_sliced_vars vars_to_keep deps nd
96
  in
97
  Format.eprintf "COI Vars: %a@."
98
    (Utils.fprintf_list ~sep:"," Format.pp_print_string)
99
     coi_vars;
100
  let outputs =
101
    List.filter
102
      (
103
        fun v -> List.mem v.var_id coi_vars 
104
      ) nd.node_outputs
105
  in
106
  let outputs = match outputs with
107
      [] -> (
108
      Format.eprintf "No visible output variable, subtituting with provided vars@ ";
109
      vars_to_keep
110
    )
111
    | l -> l
112
  in
113
  let locals =
114
    List.filter (fun v -> List.mem v.var_id coi_vars) nd.node_locals
115
  in
116
  let stmts =
117
    List.filter (
118
        fun stmt ->
119
        match stmt with
120
        | Aut _ -> assert false
121
        | Eq eq -> (
122
          match eq.eq_lhs with
123
            [vid] -> List.mem vid coi_vars
124
          | _ -> assert false
125
        (* should not happen after inlining and normalization *)
126
        )
127
      ) nd.node_stmts
128
  in
129
  { nd
130
  with
131
    node_outputs = outputs;
132
    node_locals = locals;
133
    node_stmts = stmts 
134
  }