Changeset 2743 for extracted/eRTLptrToLTL.ml

Timestamp:

Feb 27, 2013, 9:27:58 PM (8 years ago)

Author:

sacerdot

Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:

• extracted/eRTLptrToLTL.ml (modified) (10 diffs)

extracted/eRTLptrToLTL.ml

@@ -132 +132 @@
 
 open TranslateUtils
+
+(** val dpi1__o__Reg_to_dec__o__inject :
+    (I8051.register, 'a1) Types.dPair -> Interference.decision Types.sig0 **)
+let dpi1__o__Reg_to_dec__o__inject x2 =
+  Interference.Decision_colour x2.Types.dpi1
+
+(** val eject__o__Reg_to_dec__o__inject :
+    I8051.register Types.sig0 -> Interference.decision Types.sig0 **)
+let eject__o__Reg_to_dec__o__inject x2 =
+  Interference.Decision_colour (Types.pi1 x2)
+
+(** val reg_to_dec__o__inject :
+    I8051.register -> Interference.decision Types.sig0 **)
+let reg_to_dec__o__inject x1 =
+  Interference.Decision_colour x1
+
+(** val dpi1__o__Reg_to_dec :
+    (I8051.register, 'a1) Types.dPair -> Interference.decision **)
+let dpi1__o__Reg_to_dec x1 =
+  Interference.Decision_colour x1.Types.dpi1
+
+(** val eject__o__Reg_to_dec :
+    I8051.register Types.sig0 -> Interference.decision **)
+let eject__o__Reg_to_dec x1 =
+  Interference.Decision_colour (Types.pi1 x1)
 
 type arg_decision =
@@ -142 +167 @@
     arg_decision -> 'a1 **)
 let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
-| Arg_decision_colour x_492 -> h_arg_decision_colour x_492
-| Arg_decision_spill x_493 -> h_arg_decision_spill x_493
-| Arg_decision_imm x_494 -> h_arg_decision_imm x_494
+| Arg_decision_colour x_21681 -> h_arg_decision_colour x_21681
+| Arg_decision_spill x_21682 -> h_arg_decision_spill x_21682
+| Arg_decision_imm x_21683 -> h_arg_decision_imm x_21683
 
 (** val arg_decision_rect_Type5 :
@@ -150 +175 @@
     arg_decision -> 'a1 **)
 let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
-| Arg_decision_colour x_499 -> h_arg_decision_colour x_499
-| Arg_decision_spill x_500 -> h_arg_decision_spill x_500
-| Arg_decision_imm x_501 -> h_arg_decision_imm x_501
+| Arg_decision_colour x_21688 -> h_arg_decision_colour x_21688
+| Arg_decision_spill x_21689 -> h_arg_decision_spill x_21689
+| Arg_decision_imm x_21690 -> h_arg_decision_imm x_21690
 
 (** val arg_decision_rect_Type3 :
@@ -158 +183 @@
     arg_decision -> 'a1 **)
 let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
-| Arg_decision_colour x_506 -> h_arg_decision_colour x_506
-| Arg_decision_spill x_507 -> h_arg_decision_spill x_507
-| Arg_decision_imm x_508 -> h_arg_decision_imm x_508
+| Arg_decision_colour x_21695 -> h_arg_decision_colour x_21695
+| Arg_decision_spill x_21696 -> h_arg_decision_spill x_21696
+| Arg_decision_imm x_21697 -> h_arg_decision_imm x_21697
 
 (** val arg_decision_rect_Type2 :
@@ -166 +191 @@
     arg_decision -> 'a1 **)
 let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
-| Arg_decision_colour x_513 -> h_arg_decision_colour x_513
-| Arg_decision_spill x_514 -> h_arg_decision_spill x_514
-| Arg_decision_imm x_515 -> h_arg_decision_imm x_515
+| Arg_decision_colour x_21702 -> h_arg_decision_colour x_21702
+| Arg_decision_spill x_21703 -> h_arg_decision_spill x_21703
+| Arg_decision_imm x_21704 -> h_arg_decision_imm x_21704
 
 (** val arg_decision_rect_Type1 :
@@ -174 +199 @@
     arg_decision -> 'a1 **)
 let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
-| Arg_decision_colour x_520 -> h_arg_decision_colour x_520
-| Arg_decision_spill x_521 -> h_arg_decision_spill x_521
-| Arg_decision_imm x_522 -> h_arg_decision_imm x_522
+| Arg_decision_colour x_21709 -> h_arg_decision_colour x_21709
+| Arg_decision_spill x_21710 -> h_arg_decision_spill x_21710
+| Arg_decision_imm x_21711 -> h_arg_decision_imm x_21711
 
 (** val arg_decision_rect_Type0 :
@@ -182 +207 @@
     arg_decision -> 'a1 **)
 let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
-| Arg_decision_colour x_527 -> h_arg_decision_colour x_527
-| Arg_decision_spill x_528 -> h_arg_decision_spill x_528
-| Arg_decision_imm x_529 -> h_arg_decision_imm x_529
+| Arg_decision_colour x_21716 -> h_arg_decision_colour x_21716
+| Arg_decision_spill x_21717 -> h_arg_decision_spill x_21717
+| Arg_decision_imm x_21718 -> h_arg_decision_imm x_21718
 
 (** val arg_decision_inv_rect_Type4 :
@@ -231 +256 @@
      | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
      | Arg_decision_imm a0 -> Obj.magic (fun _ dH -> dH __)) y
+
+(** val dpi1__o__Reg_to_arg_dec__o__inject :
+    (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **)
+let dpi1__o__Reg_to_arg_dec__o__inject x2 =
+  Arg_decision_colour x2.Types.dpi1
+
+(** val eject__o__Reg_to_arg_dec__o__inject :
+    I8051.register Types.sig0 -> arg_decision Types.sig0 **)
+let eject__o__Reg_to_arg_dec__o__inject x2 =
+  Arg_decision_colour (Types.pi1 x2)
+
+(** val reg_to_arg_dec__o__inject :
+    I8051.register -> arg_decision Types.sig0 **)
+let reg_to_arg_dec__o__inject x1 =
+  Arg_decision_colour x1
+
+(** val dpi1__o__Reg_to_arg_dec :
+    (I8051.register, 'a1) Types.dPair -> arg_decision **)
+let dpi1__o__Reg_to_arg_dec x1 =
+  Arg_decision_colour x1.Types.dpi1
+
+(** val eject__o__Reg_to_arg_dec :
+    I8051.register Types.sig0 -> arg_decision **)
+let eject__o__Reg_to_arg_dec x1 =
+  Arg_decision_colour (Types.pi1 x1)
 
 (** val preserve_carry_bit :
@@ -246 +296 @@
 let a =
   Types.It
+
+(** val dpi1__o__beval_of_byte__o__inject :
+    (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval Types.sig0 **)
+let dpi1__o__beval_of_byte__o__inject x2 =
+  ByteValues.BVByte x2.Types.dpi1
+
+(** val eject__o__beval_of_byte__o__inject :
+    BitVector.byte Types.sig0 -> ByteValues.beval Types.sig0 **)
+let eject__o__beval_of_byte__o__inject x2 =
+  ByteValues.BVByte (Types.pi1 x2)
+
+(** val beval_of_byte__o__inject :
+    BitVector.byte -> ByteValues.beval Types.sig0 **)
+let beval_of_byte__o__inject x1 =
+  ByteValues.BVByte x1
+
+(** val dpi1__o__beval_of_byte :
+    (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval **)
+let dpi1__o__beval_of_byte x1 =
+  ByteValues.BVByte x1.Types.dpi1
+
+(** val eject__o__beval_of_byte :
+    BitVector.byte Types.sig0 -> ByteValues.beval **)
+let eject__o__beval_of_byte x1 =
+  ByteValues.BVByte (Types.pi1 x1)
 
 (** val set_dp_by_offset :
@@ -514 +589 @@
 | Interference.Decision_colour r -> Arg_decision_colour r
 
+(** val reg_to_dec__o__dec_arg_dec__o__inject :
+    I8051.register -> arg_decision Types.sig0 **)
+let reg_to_dec__o__dec_arg_dec__o__inject x0 =
+  dec_to_arg_dec (Interference.Decision_colour x0)
+
+(** val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject :
+    (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **)
+let dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 =
+  dec_to_arg_dec (dpi1__o__Reg_to_dec x2)
+
+(** val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject :
+    I8051.register Types.sig0 -> arg_decision Types.sig0 **)
+let eject__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 =
+  dec_to_arg_dec (eject__o__Reg_to_dec x2)
+
+(** val dpi1__o__dec_arg_dec__o__inject :
+    (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0 **)
+let dpi1__o__dec_arg_dec__o__inject x2 =
+  dec_to_arg_dec x2.Types.dpi1
+
+(** val eject__o__dec_arg_dec__o__inject :
+    Interference.decision Types.sig0 -> arg_decision Types.sig0 **)
+let eject__o__dec_arg_dec__o__inject x2 =
+  dec_to_arg_dec (Types.pi1 x2)
+
+(** val dec_arg_dec__o__inject :
+    Interference.decision -> arg_decision Types.sig0 **)
+let dec_arg_dec__o__inject x1 =
+  dec_to_arg_dec x1
+
+(** val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision **)
+let reg_to_dec__o__dec_arg_dec x0 =
+  dec_to_arg_dec (Interference.Decision_colour x0)
+
+(** val dpi1__o__Reg_to_dec__o__dec_arg_dec :
+    (I8051.register, 'a1) Types.dPair -> arg_decision **)
+let dpi1__o__Reg_to_dec__o__dec_arg_dec x1 =
+  dec_to_arg_dec (dpi1__o__Reg_to_dec x1)
+
+(** val eject__o__Reg_to_dec__o__dec_arg_dec :
+    I8051.register Types.sig0 -> arg_decision **)
+let eject__o__Reg_to_dec__o__dec_arg_dec x1 =
+  dec_to_arg_dec (eject__o__Reg_to_dec x1)
+
+(** val dpi1__o__dec_arg_dec :
+    (Interference.decision, 'a1) Types.dPair -> arg_decision **)
+let dpi1__o__dec_arg_dec x1 =
+  dec_to_arg_dec x1.Types.dpi1
+
+(** val eject__o__dec_arg_dec :
+    Interference.decision Types.sig0 -> arg_decision **)
+let eject__o__dec_arg_dec x1 =
+  dec_to_arg_dec (Types.pi1 x1)
+
 (** val translate_op1 :
     AST.ident List.list -> Bool.bool -> BackEndOps.op1 ->