99 open Hints_declaration
123 (** val lTL : Joint.graph_params **)
125 Joint_LTL_LIN.lTL_LIN
127 type ltl_program = Joint.joint_program
129 (** val dpi1__o__byte_to_ltl_argument__o__inject :
130 (BitVector.byte, 'a1) Types.dPair -> Joint.hdw_argument Types.sig0 **)
131 let dpi1__o__byte_to_ltl_argument__o__inject x2 =
132 Joint.hdw_argument_from_byte x2.Types.dpi1
134 (** val eject__o__byte_to_ltl_argument__o__inject :
135 BitVector.byte Types.sig0 -> Joint.hdw_argument Types.sig0 **)
136 let eject__o__byte_to_ltl_argument__o__inject x2 =
137 Joint.hdw_argument_from_byte (Types.pi1 x2)
139 (** val byte_to_ltl_argument__o__inject :
140 BitVector.byte -> Joint.hdw_argument Types.sig0 **)
141 let byte_to_ltl_argument__o__inject x1 =
142 Joint.hdw_argument_from_byte x1
144 (** val dpi1__o__byte_to_ltl_argument :
145 (BitVector.byte, 'a1) Types.dPair -> Joint.hdw_argument **)
146 let dpi1__o__byte_to_ltl_argument x1 =
147 Joint.hdw_argument_from_byte x1.Types.dpi1
149 (** val eject__o__byte_to_ltl_argument :
150 BitVector.byte Types.sig0 -> Joint.hdw_argument **)
151 let eject__o__byte_to_ltl_argument x1 =
152 Joint.hdw_argument_from_byte (Types.pi1 x1)
154 (** val dpi1__o__reg_to_ltl_argument__o__inject :
155 (I8051.register, 'a1) Types.dPair -> Joint.hdw_argument Types.sig0 **)
156 let dpi1__o__reg_to_ltl_argument__o__inject x2 =
157 Joint.hdw_argument_from_reg x2.Types.dpi1
159 (** val eject__o__reg_to_ltl_argument__o__inject :
160 I8051.register Types.sig0 -> Joint.hdw_argument Types.sig0 **)
161 let eject__o__reg_to_ltl_argument__o__inject x2 =
162 Joint.hdw_argument_from_reg (Types.pi1 x2)
164 (** val reg_to_ltl_argument__o__inject :
165 I8051.register -> Joint.hdw_argument Types.sig0 **)
166 let reg_to_ltl_argument__o__inject x1 =
167 Joint.hdw_argument_from_reg x1
169 (** val dpi1__o__reg_to_ltl_argument :
170 (I8051.register, 'a1) Types.dPair -> Joint.hdw_argument **)
171 let dpi1__o__reg_to_ltl_argument x1 =
172 Joint.hdw_argument_from_reg x1.Types.dpi1
174 (** val eject__o__reg_to_ltl_argument :
175 I8051.register Types.sig0 -> Joint.hdw_argument **)
176 let eject__o__reg_to_ltl_argument x1 =
177 Joint.hdw_argument_from_reg (Types.pi1 x1)
179 (** val lTL_premain : ltl_program -> Joint.joint_closed_internal_function **)
181 let l1 = Positive.One in
182 let l2 = Positive.P0 Positive.One in
183 let l3 = Positive.P1 Positive.One in
184 let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
185 Positive.One)); Joint.joint_if_runiverse = Positive.One;
186 Joint.joint_if_result = (Obj.magic Types.It); Joint.joint_if_params =
187 (Obj.magic Types.It); Joint.joint_if_stacksize = Nat.O;
188 Joint.joint_if_local_stacksize = Nat.O; Joint.joint_if_code =
189 (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
190 Joint.joint_if_entry = (Obj.magic l1) }
194 (Joint.prog_names (Joint.graph_params_to_params lTL) p) l1
195 (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
200 (Joint.prog_names (Joint.graph_params_to_params lTL) p) l2
201 (Joint.Sequential ((Joint.CALL ((Types.Inl
202 p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
203 (Obj.magic Types.It))), (Obj.magic l3))) res0
207 (Joint.prog_names (Joint.graph_params_to_params lTL) p) l3 (Joint.Final
208 (Joint.GOTO l3)) res1