99 open Hints_declaration
123 (** val lIN : Joint.lin_params **)
125 Joint_LTL_LIN.lTL_LIN
127 type lin_program = Joint.joint_program
129 (** val lIN_premain : lin_program -> Joint.joint_closed_internal_function **)
131 let l3 = Positive.P1 Positive.One in
132 let code = List.Cons ({ Types.fst = Types.None; Types.snd =
133 (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
134 (Obj.magic Types.It))) }, (List.Cons ({ Types.fst = Types.None;
135 Types.snd = (Joint.Sequential ((Joint.CALL ((Types.Inl
136 p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
137 (Obj.magic Types.It))), (Obj.magic Types.It))) }, (List.Cons
138 ({ Types.fst = (Types.Some l3); Types.snd = (Joint.Final (Joint.GOTO
139 l3)) }, List.Nil)))))
141 { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0 Positive.One));
142 Joint.joint_if_runiverse = Positive.One; Joint.joint_if_result =
143 (Obj.magic Types.It); Joint.joint_if_params = (Obj.magic Types.It);
144 Joint.joint_if_stacksize = Nat.O; Joint.joint_if_local_stacksize = Nat.O;
145 Joint.joint_if_code = (Obj.magic code); Joint.joint_if_entry =