source: extracted/joint_LTL_LIN.mli @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 5.9 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open BitVectorTrie
12
13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107type registers_move =
108| From_acc of I8051.register * Types.unit0
109| To_acc of Types.unit0 * I8051.register
110| Int_to_reg of I8051.register * BitVector.byte
111| Int_to_acc of Types.unit0 * BitVector.byte
112
113val registers_move_rect_Type4 :
114  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
115  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
116  BitVector.byte -> 'a1) -> registers_move -> 'a1
117
118val registers_move_rect_Type5 :
119  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
120  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
121  BitVector.byte -> 'a1) -> registers_move -> 'a1
122
123val registers_move_rect_Type3 :
124  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
125  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
126  BitVector.byte -> 'a1) -> registers_move -> 'a1
127
128val registers_move_rect_Type2 :
129  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
130  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
131  BitVector.byte -> 'a1) -> registers_move -> 'a1
132
133val registers_move_rect_Type1 :
134  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
135  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
136  BitVector.byte -> 'a1) -> registers_move -> 'a1
137
138val registers_move_rect_Type0 :
139  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
140  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
141  BitVector.byte -> 'a1) -> registers_move -> 'a1
142
143val registers_move_inv_rect_Type4 :
144  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
145  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
146  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
147  'a1) -> 'a1
148
149val registers_move_inv_rect_Type3 :
150  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
151  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
152  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
153  'a1) -> 'a1
154
155val registers_move_inv_rect_Type2 :
156  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
157  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
158  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
159  'a1) -> 'a1
160
161val registers_move_inv_rect_Type1 :
162  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
163  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
164  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
165  'a1) -> 'a1
166
167val registers_move_inv_rect_Type0 :
168  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
169  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
170  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
171  'a1) -> 'a1
172
173val registers_move_discr : registers_move -> registers_move -> __
174
175val registers_move_jmdiscr : registers_move -> registers_move -> __
176
177type ltl_lin_seq =
178| SAVE_CARRY
179| RESTORE_CARRY
180| LOW_ADDRESS of I8051.register * Graphs.label
181| HIGH_ADDRESS of I8051.register * Graphs.label
182
183val ltl_lin_seq_rect_Type4 :
184  'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
185  Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
186
187val ltl_lin_seq_rect_Type5 :
188  'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
189  Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
190
191val ltl_lin_seq_rect_Type3 :
192  'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
193  Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
194
195val ltl_lin_seq_rect_Type2 :
196  'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
197  Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
198
199val ltl_lin_seq_rect_Type1 :
200  'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
201  Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
202
203val ltl_lin_seq_rect_Type0 :
204  'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
205  Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
206
207val ltl_lin_seq_inv_rect_Type4 :
208  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
209  Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
210  -> 'a1
211
212val ltl_lin_seq_inv_rect_Type3 :
213  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
214  Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
215  -> 'a1
216
217val ltl_lin_seq_inv_rect_Type2 :
218  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
219  Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
220  -> 'a1
221
222val ltl_lin_seq_inv_rect_Type1 :
223  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
224  Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
225  -> 'a1
226
227val ltl_lin_seq_inv_rect_Type0 :
228  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
229  Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
230  -> 'a1
231
232val ltl_lin_seq_discr : ltl_lin_seq -> ltl_lin_seq -> __
233
234val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __
235
236val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list
237
238val lTL_LIN : Joint.unserialized_params
239
Note: See TracBrowser for help on using the repository browser.