]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blobdiff - extracted/status.ml
projects / pkg-cerco / acc-trusted.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
Imported Upstream version 0.2
[pkg-cerco/acc-trusted.git] / extracted / status.ml
diff --git a/extracted/status.ml b/extracted/status.ml
index 7a08f700e269d4d3d107d26b91c98a3fe44febcb..2abe567963465f02ac48df2f6c24a92c223a0ac1 100644 (file)
--- a/extracted/status.ml
+++ b/extracted/status.ml
@@ -88,43 +88,43 @@ type serialBufferType =
     (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
     serialBufferType -> 'a1 **)
 let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
-| Eight x_21722 -> h_Eight x_21722
-| Nine (x_21724, x_21723) -> h_Nine x_21724 x_21723
+| Eight x_8 -> h_Eight x_8
+| Nine (x_10, x_9) -> h_Nine x_10 x_9
 
 (** val serialBufferType_rect_Type5 :
     (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
     serialBufferType -> 'a1 **)
 let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
-| Eight x_21728 -> h_Eight x_21728
-| Nine (x_21730, x_21729) -> h_Nine x_21730 x_21729
+| Eight x_14 -> h_Eight x_14
+| Nine (x_16, x_15) -> h_Nine x_16 x_15
 
 (** val serialBufferType_rect_Type3 :
     (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
     serialBufferType -> 'a1 **)
 let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
-| Eight x_21734 -> h_Eight x_21734
-| Nine (x_21736, x_21735) -> h_Nine x_21736 x_21735
+| Eight x_20 -> h_Eight x_20
+| Nine (x_22, x_21) -> h_Nine x_22 x_21
 
 (** val serialBufferType_rect_Type2 :
     (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
     serialBufferType -> 'a1 **)
 let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
-| Eight x_21740 -> h_Eight x_21740
-| Nine (x_21742, x_21741) -> h_Nine x_21742 x_21741
+| Eight x_26 -> h_Eight x_26
+| Nine (x_28, x_27) -> h_Nine x_28 x_27
 
 (** val serialBufferType_rect_Type1 :
     (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
     serialBufferType -> 'a1 **)
 let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
-| Eight x_21746 -> h_Eight x_21746
-| Nine (x_21748, x_21747) -> h_Nine x_21748 x_21747
+| Eight x_32 -> h_Eight x_32
+| Nine (x_34, x_33) -> h_Nine x_34 x_33
 
 (** val serialBufferType_rect_Type0 :
     (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
     serialBufferType -> 'a1 **)
 let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
-| Eight x_21752 -> h_Eight x_21752
-| Nine (x_21754, x_21753) -> h_Nine x_21754 x_21753
+| Eight x_38 -> h_Eight x_38
+| Nine (x_40, x_39) -> h_Nine x_40 x_39
 
 (** val serialBufferType_inv_rect_Type4 :
     serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
@@ -181,49 +181,49 @@ type lineType =
     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
     -> 'a1) -> lineType -> 'a1 **)
 let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
-| P1 x_21801 -> h_P1 x_21801
-| P3 x_21802 -> h_P3 x_21802
-| SerialBuffer x_21803 -> h_SerialBuffer x_21803
+| P1 x_87 -> h_P1 x_87
+| P3 x_88 -> h_P3 x_88
+| SerialBuffer x_89 -> h_SerialBuffer x_89
 
 (** val lineType_rect_Type5 :
     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
     -> 'a1) -> lineType -> 'a1 **)
 let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
-| P1 x_21808 -> h_P1 x_21808
-| P3 x_21809 -> h_P3 x_21809
-| SerialBuffer x_21810 -> h_SerialBuffer x_21810
+| P1 x_94 -> h_P1 x_94
+| P3 x_95 -> h_P3 x_95
+| SerialBuffer x_96 -> h_SerialBuffer x_96
 
 (** val lineType_rect_Type3 :
     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
     -> 'a1) -> lineType -> 'a1 **)
 let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
-| P1 x_21815 -> h_P1 x_21815
-| P3 x_21816 -> h_P3 x_21816
-| SerialBuffer x_21817 -> h_SerialBuffer x_21817
+| P1 x_101 -> h_P1 x_101
+| P3 x_102 -> h_P3 x_102
+| SerialBuffer x_103 -> h_SerialBuffer x_103
 
 (** val lineType_rect_Type2 :
     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
     -> 'a1) -> lineType -> 'a1 **)
 let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
-| P1 x_21822 -> h_P1 x_21822
-| P3 x_21823 -> h_P3 x_21823
-| SerialBuffer x_21824 -> h_SerialBuffer x_21824
+| P1 x_108 -> h_P1 x_108
+| P3 x_109 -> h_P3 x_109
+| SerialBuffer x_110 -> h_SerialBuffer x_110
 
 (** val lineType_rect_Type1 :
     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
     -> 'a1) -> lineType -> 'a1 **)
 let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
-| P1 x_21829 -> h_P1 x_21829
-| P3 x_21830 -> h_P3 x_21830
-| SerialBuffer x_21831 -> h_SerialBuffer x_21831
+| P1 x_115 -> h_P1 x_115
+| P3 x_116 -> h_P3 x_116
+| SerialBuffer x_117 -> h_SerialBuffer x_117
 
 (** val lineType_rect_Type0 :
     (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
     -> 'a1) -> lineType -> 'a1 **)
 let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
-| P1 x_21836 -> h_P1 x_21836
-| P3 x_21837 -> h_P3 x_21837
-| SerialBuffer x_21838 -> h_SerialBuffer x_21838
+| P1 x_122 -> h_P1 x_122
+| P3 x_123 -> h_P3 x_123
+| SerialBuffer x_124 -> h_SerialBuffer x_124
 
 (** val lineType_inv_rect_Type4 :
     lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
@@ -730,13 +730,13 @@ type 'm preStatus = { low_internal_ram : BitVector.byte
     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
     preStatus -> 'a2 **)
-let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_22224 =
+let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_510 =
   let { low_internal_ram = low_internal_ram0; high_internal_ram =
     high_internal_ram0; external_ram = external_ram0; program_counter =
     program_counter0; special_function_registers_8051 =
     special_function_registers_8053; special_function_registers_8052 =
     special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
-    p3_latch0; clock = clock0 } = x_22224
+    p3_latch0; clock = clock0 } = x_510
   in
   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     program_counter0 special_function_registers_8053
@@ -748,13 +748,13 @@ let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_22224 =
     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
     preStatus -> 'a2 **)
-let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_22226 =
+let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_512 =
   let { low_internal_ram = low_internal_ram0; high_internal_ram =
     high_internal_ram0; external_ram = external_ram0; program_counter =
     program_counter0; special_function_registers_8051 =
     special_function_registers_8053; special_function_registers_8052 =
     special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
-    p3_latch0; clock = clock0 } = x_22226
+    p3_latch0; clock = clock0 } = x_512
   in
   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     program_counter0 special_function_registers_8053
@@ -766,13 +766,13 @@ let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_22226 =
     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
     preStatus -> 'a2 **)
-let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_22228 =
+let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_514 =
   let { low_internal_ram = low_internal_ram0; high_internal_ram =
     high_internal_ram0; external_ram = external_ram0; program_counter =
     program_counter0; special_function_registers_8051 =
     special_function_registers_8053; special_function_registers_8052 =
     special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
-    p3_latch0; clock = clock0 } = x_22228
+    p3_latch0; clock = clock0 } = x_514
   in
   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     program_counter0 special_function_registers_8053
@@ -784,13 +784,13 @@ let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_22228 =
     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
     preStatus -> 'a2 **)
-let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_22230 =
+let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_516 =
   let { low_internal_ram = low_internal_ram0; high_internal_ram =
     high_internal_ram0; external_ram = external_ram0; program_counter =
     program_counter0; special_function_registers_8051 =
     special_function_registers_8053; special_function_registers_8052 =
     special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
-    p3_latch0; clock = clock0 } = x_22230
+    p3_latch0; clock = clock0 } = x_516
   in
   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     program_counter0 special_function_registers_8053
@@ -802,13 +802,13 @@ let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_22230 =
     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
     preStatus -> 'a2 **)
-let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_22232 =
+let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_518 =
   let { low_internal_ram = low_internal_ram0; high_internal_ram =
     high_internal_ram0; external_ram = external_ram0; program_counter =
     program_counter0; special_function_registers_8051 =
     special_function_registers_8053; special_function_registers_8052 =
     special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
-    p3_latch0; clock = clock0 } = x_22232
+    p3_latch0; clock = clock0 } = x_518
   in
   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     program_counter0 special_function_registers_8053
@@ -820,13 +820,13 @@ let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_22232 =
     -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
     Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
     preStatus -> 'a2 **)
-let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_22234 =
+let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_520 =
   let { low_internal_ram = low_internal_ram0; high_internal_ram =
     high_internal_ram0; external_ram = external_ram0; program_counter =
     program_counter0; special_function_registers_8051 =
     special_function_registers_8053; special_function_registers_8052 =
     special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
-    p3_latch0; clock = clock0 } = x_22234
+    p3_latch0; clock = clock0 } = x_520
   in
   h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     program_counter0 special_function_registers_8053
Unnamed repository; edit this file 'description' to name the repository.