Changeset 2743 for extracted/joint.mli


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/joint.mli

    r2717 r2743  
    148148val psd_argument_from_reg : Registers.register -> psd_argument
    149149
     150val dpi1__o__reg_to_psd_argument__o__inject :
     151  (Registers.register, 'a1) Types.dPair -> psd_argument Types.sig0
     152
     153val eject__o__reg_to_psd_argument__o__inject :
     154  Registers.register Types.sig0 -> psd_argument Types.sig0
     155
     156val reg_to_psd_argument__o__inject :
     157  Registers.register -> psd_argument Types.sig0
     158
     159val dpi1__o__reg_to_psd_argument :
     160  (Registers.register, 'a1) Types.dPair -> psd_argument
     161
     162val eject__o__reg_to_psd_argument :
     163  Registers.register Types.sig0 -> psd_argument
     164
    150165val psd_argument_from_byte : BitVector.byte -> psd_argument
    151166
     167val dpi1__o__byte_to_psd_argument__o__inject :
     168  (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0
     169
     170val eject__o__byte_to_psd_argument__o__inject :
     171  BitVector.byte Types.sig0 -> psd_argument Types.sig0
     172
     173val byte_to_psd_argument__o__inject :
     174  BitVector.byte -> psd_argument Types.sig0
     175
     176val dpi1__o__byte_to_psd_argument :
     177  (BitVector.byte, 'a1) Types.dPair -> psd_argument
     178
     179val eject__o__byte_to_psd_argument :
     180  BitVector.byte Types.sig0 -> psd_argument
     181
    152182type hdw_argument = I8051.register argument
    153183
    154184val hdw_argument_from_reg : I8051.register -> hdw_argument
    155185
     186val dpi1__o__reg_to_hdw_argument__o__inject :
     187  (I8051.register, 'a1) Types.dPair -> hdw_argument Types.sig0
     188
     189val eject__o__reg_to_hdw_argument__o__inject :
     190  I8051.register Types.sig0 -> hdw_argument Types.sig0
     191
     192val reg_to_hdw_argument__o__inject :
     193  I8051.register -> hdw_argument Types.sig0
     194
     195val dpi1__o__reg_to_hdw_argument :
     196  (I8051.register, 'a1) Types.dPair -> hdw_argument
     197
     198val eject__o__reg_to_hdw_argument : I8051.register Types.sig0 -> hdw_argument
     199
    156200val hdw_argument_from_byte : BitVector.byte -> hdw_argument
     201
     202val dpi1__o__byte_to_hdw_argument__o__inject :
     203  (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0
     204
     205val eject__o__byte_to_hdw_argument__o__inject :
     206  BitVector.byte Types.sig0 -> psd_argument Types.sig0
     207
     208val byte_to_hdw_argument__o__inject :
     209  BitVector.byte -> psd_argument Types.sig0
     210
     211val dpi1__o__byte_to_hdw_argument :
     212  (BitVector.byte, 'a1) Types.dPair -> psd_argument
     213
     214val eject__o__byte_to_hdw_argument :
     215  BitVector.byte Types.sig0 -> psd_argument
    157216
    158217val byte_of_nat : Nat.nat -> BitVector.byte
     
    369428val nOOP : unserialized_params -> AST.ident List.list -> joint_seq
    370429
     430val dpi1__o__extension_seq_to_seq__o__inject :
     431  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
     432  joint_seq Types.sig0
     433
     434val eject__o__extension_seq_to_seq__o__inject :
     435  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
     436  Types.sig0
     437
     438val extension_seq_to_seq__o__inject :
     439  unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0
     440
     441val dpi1__o__extension_seq_to_seq :
     442  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
     443  joint_seq
     444
     445val eject__o__extension_seq_to_seq :
     446  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
     447
    371448type joint_step =
    372449| COST_LABEL of CostLabel.costlabel
     
    443520  __
    444521
     522val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
     523  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
     524  joint_step Types.sig0
     525
     526val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
     527  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
     528  Types.sig0
     529
     530val extension_seq_to_seq__o__seq_to_step__o__inject :
     531  unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0
     532
     533val dpi1__o__seq_to_step__o__inject :
     534  unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair
     535  -> joint_step Types.sig0
     536
     537val eject__o__seq_to_step__o__inject :
     538  unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
     539  joint_step Types.sig0
     540
     541val seq_to_step__o__inject :
     542  unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
     543  Types.sig0
     544
     545val dpi1__o__extension_seq_to_seq__o__seq_to_step :
     546  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
     547  joint_step
     548
     549val eject__o__extension_seq_to_seq__o__seq_to_step :
     550  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
     551
     552val extension_seq_to_seq__o__seq_to_step :
     553  unserialized_params -> AST.ident List.list -> __ -> joint_step
     554
     555val dpi1__o__seq_to_step :
     556  unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair
     557  -> joint_step
     558
     559val eject__o__seq_to_step :
     560  unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
     561  joint_step
     562
    445563val step_labels :
    446564  unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
     
    635753  stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
    636754  __
     755
     756val dpi1__o__fin_step_to_stmt__o__inject :
     757  stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair ->
     758  joint_statement Types.sig0
     759
     760val eject__o__fin_step_to_stmt__o__inject :
     761  stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
     762  joint_statement Types.sig0
     763
     764val fin_step_to_stmt__o__inject :
     765  stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
     766  Types.sig0
     767
     768val dpi1__o__fin_step_to_stmt :
     769  stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair ->
     770  joint_statement
     771
     772val eject__o__fin_step_to_stmt :
     773  stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
     774  joint_statement
    637775
    638776type params = { stmt_pars : stmt_params;
     
    770908val lin_params_to_params : lin_params -> params
    771909
     910val lp_to_p__o__stmt_pars : lin_params -> stmt_params
     911
     912val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> unserialized_params
     913
    772914type graph_params =
    773915  unserialized_params
     
    812954
    813955val graph_params_to_params : graph_params -> params
     956
     957val gp_to_p__o__stmt_pars : graph_params -> stmt_params
     958
     959val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> unserialized_params
    814960
    815961type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
     
    9781124type joint_program = (joint_function, Nat.nat) AST.program
    9791125
    980 val lp_to_p__o__stmt_pars : graph_params -> stmt_params
Note: See TracChangeset for help on using the changeset viewer.