Changeset 2743 for extracted/lTL.ml


Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/lTL.ml

    r2717 r2743  
    113113type ltl_program = Joint.joint_program
    114114
     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 TracChangeset for help on using the changeset viewer.