99 open Hints_declaration
121 (** val graph_to_lin_statement :
122 Joint.uns_params -> AST.ident List.list -> 'a1 Identifiers.identifier_map
123 -> Joint.joint_statement -> Joint.joint_statement **)
124 let graph_to_lin_statement p globals visited = function
125 | Joint.Sequential (c, nxt) ->
127 | Joint.COST_LABEL x -> Joint.Sequential (c, (Obj.magic Types.It))
128 | Joint.CALL (x, x0, x1) -> Joint.Sequential (c, (Obj.magic Types.It))
129 | Joint.COND (a, ltrue) ->
130 (match Identifiers.member PreIdentifiers.LabelTag visited
132 | Bool.True -> Joint.FCOND (a, ltrue, (Obj.magic nxt))
133 | Bool.False -> Joint.Sequential (c, (Obj.magic Types.It)))
134 | Joint.Step_seq x -> Joint.Sequential (c, (Obj.magic Types.It)))
135 | Joint.Final c -> Joint.Final c
136 | Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
139 ('a1 -> Bool.bool) -> 'a1 List.list -> ('a1, 'a1 List.list) Types.prod
141 let rec chop test = function
142 | List.Nil -> Types.None
143 | List.Cons (x, l') ->
145 | Bool.True -> chop test l'
148 (Monad.m_return0 (Monad.max_def Option.option) { Types.fst = x;
151 type graph_visit_ret_type =
152 ((Nat.nat Identifiers.identifier_map, Identifiers.identifier_set)
153 Types.prod, __) Types.prod Types.sig0
155 (** val graph_visit :
156 Joint.uns_params -> AST.ident List.list -> __ ->
157 Identifiers.identifier_set -> Nat.nat Identifiers.identifier_map -> __ ->
158 Graphs.label List.list -> Nat.nat -> Nat.nat -> Graphs.label ->
159 graph_visit_ret_type **)
160 let rec graph_visit p globals g required visited generated visiting gen_length n entry =
161 (match chop (fun x -> Identifiers.member PreIdentifiers.LabelTag visited x)
164 (fun _ -> { Types.fst = { Types.fst = visited; Types.snd = required };
165 Types.snd = generated })
168 let vis_hd = pr.Types.fst in
169 let vis_tl = pr.Types.snd in
171 | Nat.O -> (fun _ -> assert false (* absurd case *))
175 Identifiers.add PreIdentifiers.LabelTag visited vis_hd
179 Identifiers.lookup_safe PreIdentifiers.LabelTag (Obj.magic g)
182 let translated_statement =
183 graph_to_lin_statement p globals visited' statement
185 let generated' = List.Cons ({ Types.fst = (Types.Some vis_hd);
186 Types.snd = translated_statement }, (Obj.magic generated))
189 Identifiers.union_set PreIdentifiers.LabelTag
190 (Identifiers.set_from_list PreIdentifiers.LabelTag
191 (Joint.stmt_explicit_labels (Joint.lp_to_p__o__stmt_pars p)
192 globals translated_statement)) required
196 (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars p);
197 Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
198 Joint.has_fcond = Bool.False } globals statement) vis_tl
202 | Joint.Sequential (s, nxt) ->
204 | Joint.COST_LABEL x ->
205 (match Identifiers.member PreIdentifiers.LabelTag visited'
208 { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
209 (Identifiers.add_set PreIdentifiers.LabelTag
210 (Identifiers.empty_set PreIdentifiers.LabelTag)
211 (Obj.magic nxt)) }; Types.snd = (List.Cons
212 ({ Types.fst = Types.None; Types.snd =
213 (let x0 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
216 { Types.fst = { Types.fst = Nat.O; Types.snd =
217 (Identifiers.empty_set PreIdentifiers.LabelTag) };
218 Types.snd = List.Nil })
219 | Joint.CALL (x, x0, x1) ->
220 (match Identifiers.member PreIdentifiers.LabelTag visited'
223 { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
224 (Identifiers.add_set PreIdentifiers.LabelTag
225 (Identifiers.empty_set PreIdentifiers.LabelTag)
226 (Obj.magic nxt)) }; Types.snd = (List.Cons
227 ({ Types.fst = Types.None; Types.snd =
228 (let x2 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
231 { Types.fst = { Types.fst = Nat.O; Types.snd =
232 (Identifiers.empty_set PreIdentifiers.LabelTag) };
233 Types.snd = List.Nil })
234 | Joint.COND (x, x0) ->
235 { Types.fst = { Types.fst = Nat.O; Types.snd =
236 (Identifiers.empty_set PreIdentifiers.LabelTag) };
237 Types.snd = List.Nil }
238 | Joint.Step_seq x ->
239 (match Identifiers.member PreIdentifiers.LabelTag visited'
242 { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
243 (Identifiers.add_set PreIdentifiers.LabelTag
244 (Identifiers.empty_set PreIdentifiers.LabelTag)
245 (Obj.magic nxt)) }; Types.snd = (List.Cons
246 ({ Types.fst = Types.None; Types.snd =
247 (let x0 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
250 { Types.fst = { Types.fst = Nat.O; Types.snd =
251 (Identifiers.empty_set PreIdentifiers.LabelTag) };
252 Types.snd = List.Nil }))
254 { Types.fst = { Types.fst = Nat.O; Types.snd =
255 (Identifiers.empty_set PreIdentifiers.LabelTag) };
256 Types.snd = List.Nil }
257 | Joint.FCOND (x0, x1, x2) ->
258 { Types.fst = { Types.fst = Nat.O; Types.snd =
259 (Identifiers.empty_set PreIdentifiers.LabelTag) };
260 Types.snd = List.Nil }
262 graph_visit p globals g
263 (Identifiers.union_set PreIdentifiers.LabelTag
264 add_req_gen.Types.fst.Types.snd required') visited'
265 (Obj.magic (List.append add_req_gen.Types.snd generated'))
267 (Nat.plus add_req_gen.Types.fst.Types.fst (Nat.S gen_length))
270 (** val branch_compress :
271 Joint.graph_params -> AST.ident List.list -> __ -> Graphs.label
273 let branch_compress p globals g entry =
276 (** val filter_labels :
277 PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> Bool.bool)
278 -> 'a1 LabelledObjects.labelled_obj List.list -> (__, 'a1) Types.prod
280 let filter_labels tag test c =
282 let { Types.fst = l_opt; Types.snd = x } = s in
284 (Monad.m_bind0 (Monad.max_def Option.option) l_opt (fun l ->
286 | Bool.True -> Monad.m_return0 (Monad.max_def Option.option) l
287 | Bool.False -> Obj.magic Types.None)); Types.snd = x }) (Obj.magic c)
289 (** val linearise_code :
290 Joint.uns_params -> AST.ident List.list -> __ -> Graphs.label Types.sig0
291 -> (__, Graphs.label -> Nat.nat Types.option) Types.prod Types.sig0 **)
292 let linearise_code p globals g entry_sig =
293 let g0 = branch_compress p globals g entry_sig in
295 graph_visit p globals g0 (Identifiers.empty_set PreIdentifiers.LabelTag)
296 (Identifiers.empty_map PreIdentifiers.LabelTag) (Obj.magic List.Nil)
297 (List.Cons ((Types.pi1 entry_sig), List.Nil)) Nat.O
298 (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic g0))
299 (Types.pi1 entry_sig)
301 let sigma = triple.Types.fst.Types.fst in
302 let required = triple.Types.fst.Types.snd in
303 let crev = triple.Types.snd in
304 let lbld_code = Util.rev (Obj.magic crev) in
307 (filter_labels PreIdentifiers.LabelTag (fun l ->
308 Identifiers.member PreIdentifiers.LabelTag required l) lbld_code));
309 Types.snd = (Identifiers.lookup PreIdentifiers.LabelTag sigma) }
311 (** val linearise_int_fun :
312 Joint.uns_params -> AST.ident List.list ->
313 Joint.joint_closed_internal_function ->
314 (Joint.joint_closed_internal_function, Graphs.label -> Nat.nat
315 Types.option) Types.prod Types.sig0 **)
316 let linearise_int_fun p globals f_sig =
318 linearise_code p globals (Types.pi1 f_sig).Joint.joint_if_code
319 (Obj.magic (Types.pi1 f_sig).Joint.joint_if_entry)
321 let code = (Types.pi1 code_sigma).Types.fst in
322 let sigma = (Types.pi1 code_sigma).Types.snd in
323 { Types.fst = { Joint.joint_if_luniverse =
324 (Types.pi1 f_sig).Joint.joint_if_luniverse; Joint.joint_if_runiverse =
325 (Types.pi1 f_sig).Joint.joint_if_runiverse; Joint.joint_if_result =
326 (Types.pi1 f_sig).Joint.joint_if_result; Joint.joint_if_params =
327 (Types.pi1 f_sig).Joint.joint_if_params; Joint.joint_if_stacksize =
328 (Types.pi1 f_sig).Joint.joint_if_stacksize;
329 Joint.joint_if_local_stacksize =
330 (Types.pi1 f_sig).Joint.joint_if_local_stacksize; Joint.joint_if_code =
331 code; Joint.joint_if_entry = (Obj.magic Nat.O) }; Types.snd = sigma }
334 Joint.uns_params -> Joint.joint_program -> Joint.joint_program **)
336 Joint.transform_joint_program (Joint.graph_params_to_params p)
337 (Joint.lin_params_to_params p) (fun globals f_in ->
338 (Types.pi1 (linearise_int_fun p globals f_in)).Types.fst) pr