source: extracted/lTL.ml @ 2890

Last change on this file since 2890 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: 2.8 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
107open Joint_LTL_LIN
108
109(** val lTL : Joint.graph_params **)
110let lTL =
111  Joint_LTL_LIN.lTL_LIN
112
113type ltl_program = Joint.joint_program
114
115(** val dpi1__o__byte_to_ltl_argument__o__inject :
116    (BitVector.byte, 'a1) Types.dPair -> Joint.hdw_argument Types.sig0 **)
117let dpi1__o__byte_to_ltl_argument__o__inject x2 =
118  Joint.hdw_argument_from_byte x2.Types.dpi1
119
120(** val eject__o__byte_to_ltl_argument__o__inject :
121    BitVector.byte Types.sig0 -> Joint.hdw_argument Types.sig0 **)
122let eject__o__byte_to_ltl_argument__o__inject x2 =
123  Joint.hdw_argument_from_byte (Types.pi1 x2)
124
125(** val byte_to_ltl_argument__o__inject :
126    BitVector.byte -> Joint.hdw_argument Types.sig0 **)
127let byte_to_ltl_argument__o__inject x1 =
128  Joint.hdw_argument_from_byte x1
129
130(** val dpi1__o__byte_to_ltl_argument :
131    (BitVector.byte, 'a1) Types.dPair -> Joint.hdw_argument **)
132let dpi1__o__byte_to_ltl_argument x1 =
133  Joint.hdw_argument_from_byte x1.Types.dpi1
134
135(** val eject__o__byte_to_ltl_argument :
136    BitVector.byte Types.sig0 -> Joint.hdw_argument **)
137let eject__o__byte_to_ltl_argument x1 =
138  Joint.hdw_argument_from_byte (Types.pi1 x1)
139
140(** val dpi1__o__reg_to_ltl_argument__o__inject :
141    (I8051.register, 'a1) Types.dPair -> Joint.hdw_argument Types.sig0 **)
142let dpi1__o__reg_to_ltl_argument__o__inject x2 =
143  Joint.hdw_argument_from_reg x2.Types.dpi1
144
145(** val eject__o__reg_to_ltl_argument__o__inject :
146    I8051.register Types.sig0 -> Joint.hdw_argument Types.sig0 **)
147let eject__o__reg_to_ltl_argument__o__inject x2 =
148  Joint.hdw_argument_from_reg (Types.pi1 x2)
149
150(** val reg_to_ltl_argument__o__inject :
151    I8051.register -> Joint.hdw_argument Types.sig0 **)
152let reg_to_ltl_argument__o__inject x1 =
153  Joint.hdw_argument_from_reg x1
154
155(** val dpi1__o__reg_to_ltl_argument :
156    (I8051.register, 'a1) Types.dPair -> Joint.hdw_argument **)
157let dpi1__o__reg_to_ltl_argument x1 =
158  Joint.hdw_argument_from_reg x1.Types.dpi1
159
160(** val eject__o__reg_to_ltl_argument :
161    I8051.register Types.sig0 -> Joint.hdw_argument **)
162let eject__o__reg_to_ltl_argument x1 =
163  Joint.hdw_argument_from_reg (Types.pi1 x1)
164
Note: See TracBrowser for help on using the repository browser.