blob: 8e4f3284d1e4ceeae6dc6f4aed0b84589aa35e7d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
open Camlcoq
open Datatypes
open List
open AST
open Locations
type status = To_move | Being_moved | Moved
let parallel_move_order lsrc ldst =
let src = array_of_coqlist lsrc
and dst = array_of_coqlist ldst in
let n = Array.length src in
let status = Array.make n To_move in
let moves = ref Coq_nil in
let rec move_one i =
if src.(i) <> dst.(i) then begin
status.(i) <- Being_moved;
for j = 0 to n - 1 do
if src.(j) = dst.(i) then
match status.(j) with
To_move ->
move_one j
| Being_moved ->
let tmp =
match Loc.coq_type src.(j) with
| Tint -> R IT2
| Tfloat -> R FT2 in
moves := Coq_cons (Coq_pair(src.(j), tmp), !moves);
src.(j) <- tmp
| Moved ->
()
done;
moves := Coq_cons(Coq_pair(src.(i), dst.(i)), !moves);
status.(i) <- Moved
end in
for i = 0 to n - 1 do
if status.(i) = To_move then move_one i
done;
List.rev !moves
|
