Changeset 2743 for extracted/aSM.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/aSM.mli

    r2717 r2743  
    383383  Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode
    384384  Types.sig0 -> addressing_mode
     385
     386type 'x1 dpi1__o__subaddressing_mode = subaddressing_mode
     387
     388type eject__o__subaddressing_mode = subaddressing_mode
     389
     390val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
     391  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     392  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
     393  -> subaddressing_mode Types.sig0
     394
     395val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
     396  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     397  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
     398  -> addressing_mode Types.sig0
     399
     400val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
     401  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     402  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
     403  -> addressing_mode
     404
     405val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
     406  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     407  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
     408  subaddressing_mode Types.sig0
     409
     410val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
     411  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     412  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
     413  addressing_mode Types.sig0
     414
     415val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
     416  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     417  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
     418  addressing_mode
     419
     420val subaddressing_modeel__o__mk_subaddressing_mode__o__inject :
     421  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     422  addressing_mode_tag Vector.vector -> subaddressing_mode ->
     423  subaddressing_mode Types.sig0
     424
     425val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
     426  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     427  addressing_mode_tag Vector.vector -> subaddressing_mode -> addressing_mode
     428  Types.sig0
     429
     430val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel :
     431  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     432  addressing_mode_tag Vector.vector -> subaddressing_mode -> addressing_mode
     433
     434val dpi1__o__mk_subaddressing_mode__o__inject :
     435  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
     436  Vector.vector -> subaddressing_mode Types.sig0
     437
     438val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
     439  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
     440  Vector.vector -> addressing_mode Types.sig0
     441
     442val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel :
     443  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
     444  Vector.vector -> addressing_mode
     445
     446val eject__o__mk_subaddressing_mode__o__inject :
     447  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
     448  -> subaddressing_mode Types.sig0
     449
     450val eject__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
     451  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
     452  -> addressing_mode Types.sig0
     453
     454val eject__o__mk_subaddressing_mode__o__subaddressing_modeel :
     455  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
     456  -> addressing_mode
     457
     458val mk_subaddressing_mode__o__subaddressing_modeel :
     459  Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
     460  addressing_mode
     461
     462val mk_subaddressing_mode__o__subaddressing_modeel__o__inject :
     463  Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
     464  addressing_mode Types.sig0
     465
     466val mk_subaddressing_mode__o__inject :
     467  Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector ->
     468  subaddressing_mode Types.sig0
     469
     470val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode :
     471  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     472  addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) Types.dPair
     473  -> subaddressing_mode
     474
     475val eject__o__subaddressing_modeel__o__mk_subaddressing_mode :
     476  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     477  addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 ->
     478  subaddressing_mode
     479
     480val subaddressing_modeel__o__mk_subaddressing_mode :
     481  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector ->
     482  addressing_mode_tag Vector.vector -> subaddressing_mode ->
     483  subaddressing_mode
     484
     485val dpi1__o__mk_subaddressing_mode :
     486  Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag
     487  Vector.vector -> subaddressing_mode
     488
     489val eject__o__mk_subaddressing_mode :
     490  Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag Vector.vector
     491  -> subaddressing_mode
    385492
    386493type subaddressing_mode_elim_type = __
     
    9311038val instruction_jmdiscr : instruction -> instruction -> __
    9321039
     1040val dpi1__o__RealInstruction__o__inject :
     1041  (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction
     1042  Types.sig0
     1043
     1044val eject__o__RealInstruction__o__inject :
     1045  subaddressing_mode preinstruction Types.sig0 -> instruction Types.sig0
     1046
     1047val realInstruction__o__inject :
     1048  subaddressing_mode preinstruction -> instruction Types.sig0
     1049
     1050val dpi1__o__RealInstruction :
     1051  (subaddressing_mode preinstruction, 'a1) Types.dPair -> instruction
     1052
     1053val eject__o__RealInstruction :
     1054  subaddressing_mode preinstruction Types.sig0 -> instruction
     1055
    9331056val eq_instruction : instruction -> instruction -> Bool.bool
    9341057
     
    10771200val is_call : pseudo_instruction -> Bool.bool
    10781201
    1079 val subaddressing_modeel__o__mk_subaddressing_mode:
    1080  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode_tag Vector.vector -> addressing_mode -> addressing_mode
Note: See TracChangeset for help on using the changeset viewer.