Project

General

Profile

Download (8.16 KB) Statistics
| Branch: | Tag: | Revision:
1 230b168e Guillaume DAVY
2
open Machine_code_types
3
open Lustre_types
4
(*
5
open Corelang
6
open Machine_code_common
7
*)
8
9
let is_machine_statefull m = m.mmemory != [] || m.mcalls != []
10
11
(** Return true if its the arrow machine
12
   @param machine the machine to test
13
*)
14
let is_arrow machine = String.equal Arrow.arrow_id machine.mname.node_id
15
16
(** Extract a node from an instance.
17
   @param instance the instance
18
**)
19
let extract_node instance =
20
  let (_, (node, _)) = instance in
21
  match node.top_decl_desc with
22
    | Node nd         -> nd
23
    | _ -> assert false (*TODO*)
24
25
(** Extract from a machine list the one corresponding to the given instance.
26
      assume that the machine is in the list.
27
   @param machines list of all machines
28
   @param instance instance of a machine
29
   @return the machine corresponding to hte given instance
30
**)
31
let get_machine machines instance =
32
    let id = (extract_node instance).node_id in
33
    try
34
      List.find (function m -> m.mname.node_id=id) machines
35
    with
36
      Not_found -> assert false (*TODO*)
37
38
(** Test if two types are the same.
39
   @param typ1 the first type
40
   @param typ2 the second type
41
**)
42
let pp_eq_type typ1 typ2 = 
43
  let get_basic typ = match (Types.repr typ).Types.tdesc with
44
    | Types.Tbasic Types.Basic.Tint -> Types.Basic.Tint
45
    | Types.Tbasic Types.Basic.Treal -> Types.Basic.Treal
46
    | Types.Tbasic Types.Basic.Tbool -> Types.Basic.Tbool
47
    | _ -> assert false (*TODO*)
48
  in
49
  get_basic typ1 = get_basic typ2
50
51
(** Extract all the inputs and outputs.
52
   @param machine the machine
53
   @return a list of all the var_decl of a macine
54
**)
55
let get_all_vars_machine m =
56
  m.mmemory@m.mstep.step_inputs@m.mstep.step_outputs@m.mstatic
57
58
(** Check if a type is polymorphic.
59
   @param typ the type
60
   @return true if its polymorphic
61
**)
62
let is_Tunivar typ = (Types.repr typ).tdesc == Types.Tunivar
63
64
(** Find all polymorphic type : Types.Tunivar in a machine.
65
   @param machine the machine
66
   @return a list of id corresponding to polymorphic type
67
**)
68
let find_all_polymorphic_type m =
69
  let vars = get_all_vars_machine m in
70
  let extract id = id.var_type.tid in
71
  let polymorphic_type_vars =
72
    List.filter (function x-> is_Tunivar x.var_type) vars in
73
  List.sort_uniq (-) (List.map extract polymorphic_type_vars)
74
75
76
(** Check if a submachine is statefull.
77
    @param submachine a submachine
78
    @return true if the submachine is statefull
79
**)
80
let is_submachine_statefull submachine =
81
    not (snd (snd submachine)).mname.node_dec_stateless
82
83
(** Find a submachine step call in a list of instructions.
84
    @param ident submachine instance ident
85
    @param instr_list List of instruction sto search
86
    @return a list of pair containing input types and output types for each step call found
87
**)
88
let rec find_submachine_step_call ident instr_list =
89
  let search_instr instruction = 
90
    match instruction.instr_desc with
91
      | MStep (il, i, vl) when String.equal i ident -> [
92
        (List.map (function x-> x.value_type) vl,
93
            List.map (function x-> x.var_type) il)]
94
      | MBranch (_, l) -> List.flatten
95
          (List.map (function x, y -> find_submachine_step_call ident y) l)
96
      | _ -> []
97
  in
98
  List.flatten (List.map search_instr instr_list)
99
100
(** Check that two types are the same.
101
   @param t1 a type
102
   @param t2 an other type
103
   @param return true if the two types are Tbasic or Tunivar and equal
104
**)
105
let rec check_type_equal (t1:Types.type_expr) (t2:Types.type_expr) =
106
  match (Types.repr t1).Types.tdesc, (Types.repr t2).Types.tdesc with
107
    | Types.Tbasic x, Types.Tbasic y -> x = y
108
    | Types.Tunivar,  Types.Tunivar  -> t1.tid = t2.tid
109
    | Types.Ttuple l, _ -> assert (List.length l = 1); check_type_equal (List.hd l) t2
110
    | _, Types.Ttuple l -> assert (List.length l = 1); check_type_equal t1 (List.hd l)
111
    | Types.Tstatic (_, t), _ -> check_type_equal t t2
112
    | _, Types.Tstatic (_, t) -> check_type_equal t1 t
113
    | _ -> assert false
114
115
(** Extend a substitution to unify the two given types. Only the
116
  first type can be polymorphic.
117
    @param subsitution the base substitution
118
    @param type_poly the type which can be polymorphic
119
    @param typ the type to match type_poly with
120
**)
121
let unification (substituion:(int*Types.type_expr) list) ((type_poly:Types.type_expr), (typ:Types.type_expr)) =
122
  assert(not (is_Tunivar typ));
123
  (* If type_poly is polymorphic *)
124
  if is_Tunivar type_poly then
125
    (* If a subsitution exists for it *)
126
    if List.mem_assoc type_poly.tid substituion then
127
    begin
128
      (* We check that the type corresponding to type_poly in the subsitution
129
         match typ *)
130
      (try
131
        assert(check_type_equal (List.assoc type_poly.tid substituion) typ)
132
      with
133
        Not_found -> assert false);
134
      (* We return the original substituion, it is already correct *)
135
      substituion
136
    end
137
    (* If type_poly is not in the subsitution *)
138
    else
139
      (* We add it to the substituion *)
140
      (type_poly.tid, typ)::substituion
141
  (* iftype_poly is not polymorphic *)
142
  else
143
  begin
144
    (* We check that type_poly and typ are the same *)
145
    assert(check_type_equal type_poly typ);
146
    (* We return the original substituion, it is already correct *)
147
    substituion
148
  end
149
150
(** Check that two calls are equal. A call is
151
  a pair of list of types, the inputs and the outputs.
152
   @param calls a list of pair of list of types
153
   @param return true if the two pairs are equal
154
**)
155
let check_call_equal (i1, o1) (i2, o2) =
156
  (List.for_all2 check_type_equal i1 i2)
157
    && (List.for_all2 check_type_equal i1 i2)
158
159
(** Check that all the elements of list of calls are equal to one.
160
  A call is a pair of list of types, the inputs and the outputs.
161
   @param call a pair of list of types
162
   @param calls a list of pair of list of types
163
   @param return true if all the elements are equal
164
**)
165
let check_calls call calls =
166
  List.for_all (check_call_equal call) calls
167
168
(** Extract from a subinstance that can have polymorphic type the instantiation
169
    of all its polymorphic type instanciation for a given machine. It searches
170
    the step calls and extract a substitution for all polymorphic type from
171
    it.
172
   @param machine the machine which instantiate the subinstance
173
   @param ident the identifier of the instance which permits to find the step call
174
   @param submachine the machine corresponding to the subinstance
175
   @return the correspondance between polymorphic type id and their instantiation
176
**)
177
let get_substitution machine ident submachine =
178
  (* extract the calls to submachines from the machine *)
179
  let calls = find_submachine_step_call ident machine.mstep.step_instrs in
180
  (* extract the first call  *)
181
  let call = match calls with
182
              (* assume that there is always one call to a subinstance *)
183
              | []    -> assert(false)
184
              | h::t  -> h in
185
  (* assume that all the calls to a subinstance are using the same type *)
186
  assert(check_calls call calls);
187
  (* make a list of all types from input and output vars *)
188
  let call_types = (fst call)@(snd call) in
189
  (* extract all the input and output vars from the submachine *)
190
  let machine_vars = submachine.mstep.step_inputs@submachine.mstep.step_outputs in
191
  (* keep only the type of vars *)
192
  let machine_types = List.map (function x-> x.var_type) machine_vars in
193
  (* assume that there is the same numer of input and output in the submachine
194
      and the call *)
195
  assert (List.length machine_types = List.length call_types);
196
  (* Unify the two lists of types *)
197
  let substitution = List.fold_left unification [] (List.combine machine_types call_types) in
198
  (* Assume that our substitution match all the possible
199
       polymorphic type of the node *)
200
  let polymorphic_types = find_all_polymorphic_type submachine in
201
  assert (List.length polymorphic_types = List.length substitution);
202
  (try
203
    assert (List.for_all (fun x -> List.mem_assoc x substitution) polymorphic_types)
204
  with
205
    Not_found -> assert false);
206
  substitution
207
208
209
(** Extract from a machine the instance corresponding to the identifier,
210
      assume that the identifier exists in the instances of the machine.
211
212
   @param identifier the instance identifier
213
   @param machine a machine
214
   @return the instance of machine.minstances corresponding to identifier
215
**)
216
let get_instance identifier typed_submachines =
217
  try
218
    List.assoc identifier typed_submachines
219
  with Not_found -> assert false