Changeset 3019 for extracted/interference.ml

Timestamp:

Mar 28, 2013, 5:27:46 PM (7 years ago)

Author:

sacerdot

Message:

New extraction after ERTLptr abortion.

File:

• extracted/interference.ml (modified) (8 diffs)

extracted/interference.ml

@@ -98 +98 @@
 
 open ERTL
-
-open ERTLptr
 
 open Div_and_mod
@@ -136 +134 @@
     (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
 let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
-| Decision_spill x_5765 -> h_decision_spill x_5765
-| Decision_colour x_5766 -> h_decision_colour x_5766
+| Decision_spill x_7 -> h_decision_spill x_7
+| Decision_colour x_8 -> h_decision_colour x_8
 
 (** val decision_rect_Type5 :
     (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
 let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
-| Decision_spill x_5770 -> h_decision_spill x_5770
-| Decision_colour x_5771 -> h_decision_colour x_5771
+| Decision_spill x_12 -> h_decision_spill x_12
+| Decision_colour x_13 -> h_decision_colour x_13
 
 (** val decision_rect_Type3 :
     (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
 let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
-| Decision_spill x_5775 -> h_decision_spill x_5775
-| Decision_colour x_5776 -> h_decision_colour x_5776
+| Decision_spill x_17 -> h_decision_spill x_17
+| Decision_colour x_18 -> h_decision_colour x_18
 
 (** val decision_rect_Type2 :
     (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
 let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
-| Decision_spill x_5780 -> h_decision_spill x_5780
-| Decision_colour x_5781 -> h_decision_colour x_5781
+| Decision_spill x_22 -> h_decision_spill x_22
+| Decision_colour x_23 -> h_decision_colour x_23
 
 (** val decision_rect_Type1 :
     (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
 let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
-| Decision_spill x_5785 -> h_decision_spill x_5785
-| Decision_colour x_5786 -> h_decision_colour x_5786
+| Decision_spill x_27 -> h_decision_spill x_27
+| Decision_colour x_28 -> h_decision_colour x_28
 
 (** val decision_rect_Type0 :
     (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
 let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
-| Decision_spill x_5790 -> h_decision_spill x_5790
-| Decision_colour x_5791 -> h_decision_colour x_5791
+| Decision_spill x_32 -> h_decision_spill x_32
+| Decision_colour x_33 -> h_decision_colour x_33
 
 (** val decision_inv_rect_Type4 :
@@ -219 +217 @@
     Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
     __ -> 'a1) -> coloured_graph -> 'a1 **)
-let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_5826 =
-  let { colouring = colouring0; spilled_no = spilled_no0 } = x_5826 in
+let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_68 =
+  let { colouring = colouring0; spilled_no = spilled_no0 } = x_68 in
   h_mk_coloured_graph colouring0 spilled_no0 __ __
 
@@ -226 +224 @@
     Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
     __ -> 'a1) -> coloured_graph -> 'a1 **)
-let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_5828 =
-  let { colouring = colouring0; spilled_no = spilled_no0 } = x_5828 in
+let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_70 =
+  let { colouring = colouring0; spilled_no = spilled_no0 } = x_70 in
   h_mk_coloured_graph colouring0 spilled_no0 __ __
 
@@ -233 +231 @@
     Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
     __ -> 'a1) -> coloured_graph -> 'a1 **)
-let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_5830 =
-  let { colouring = colouring0; spilled_no = spilled_no0 } = x_5830 in
+let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_72 =
+  let { colouring = colouring0; spilled_no = spilled_no0 } = x_72 in
   h_mk_coloured_graph colouring0 spilled_no0 __ __
 
@@ -240 +238 @@
     Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
     __ -> 'a1) -> coloured_graph -> 'a1 **)
-let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_5832 =
-  let { colouring = colouring0; spilled_no = spilled_no0 } = x_5832 in
+let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_74 =
+  let { colouring = colouring0; spilled_no = spilled_no0 } = x_74 in
   h_mk_coloured_graph colouring0 spilled_no0 __ __
 
@@ -247 +245 @@
     Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
     __ -> 'a1) -> coloured_graph -> 'a1 **)
-let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_5834 =
-  let { colouring = colouring0; spilled_no = spilled_no0 } = x_5834 in
+let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_76 =
+  let { colouring = colouring0; spilled_no = spilled_no0 } = x_76 in
   h_mk_coloured_graph colouring0 spilled_no0 __ __
 
@@ -254 +252 @@
     Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
     __ -> 'a1) -> coloured_graph -> 'a1 **)
-let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_5836 =
-  let { colouring = colouring0; spilled_no = spilled_no0 } = x_5836 in
+let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_78 =
+  let { colouring = colouring0; spilled_no = spilled_no0 } = x_78 in
   h_mk_coloured_graph colouring0 spilled_no0 __ __