Changeset 2717 for extracted/aSM.mli


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSM.mli

    r2649 r2717  
    6060
    6161open Identifiers
     62
     63open BitVectorTrie
     64
     65open Exp
    6266
    6367open Arithmetic
     
    433437| RETI
    434438| NOP
     439| JMP of subaddressing_mode
    435440
    436441val preinstruction_rect_Type4 :
     
    466471  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
    467472  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
    468   subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> 'a1 preinstruction ->
    469   'a2
     473  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
     474  'a2) -> 'a1 preinstruction -> 'a2
    470475
    471476val preinstruction_rect_Type5 :
     
    501506  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
    502507  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
    503   subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> 'a1 preinstruction ->
    504   'a2
     508  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
     509  'a2) -> 'a1 preinstruction -> 'a2
    505510
    506511val preinstruction_rect_Type3 :
     
    536541  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
    537542  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
    538   subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> 'a1 preinstruction ->
    539   'a2
     543  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
     544  'a2) -> 'a1 preinstruction -> 'a2
    540545
    541546val preinstruction_rect_Type2 :
     
    571576  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
    572577  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
    573   subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> 'a1 preinstruction ->
    574   'a2
     578  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
     579  'a2) -> 'a1 preinstruction -> 'a2
    575580
    576581val preinstruction_rect_Type1 :
     
    606611  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
    607612  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
    608   subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> 'a1 preinstruction ->
    609   'a2
     613  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
     614  'a2) -> 'a1 preinstruction -> 'a2
    610615
    611616val preinstruction_rect_Type0 :
     
    641646  'a2) -> (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) ->
    642647  (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode ->
    643   subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> 'a1 preinstruction ->
    644   'a2
     648  subaddressing_mode -> 'a2) -> 'a2 -> 'a2 -> 'a2 -> (subaddressing_mode ->
     649  'a2) -> 'a1 preinstruction -> 'a2
    645650
    646651val preinstruction_inv_rect_Type4 :
     
    680685  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
    681686  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
    682   'a2) -> 'a2
     687  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
    683688
    684689val preinstruction_inv_rect_Type3 :
     
    718723  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
    719724  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
    720   'a2) -> 'a2
     725  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
    721726
    722727val preinstruction_inv_rect_Type2 :
     
    756761  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
    757762  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
    758   'a2) -> 'a2
     763  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
    759764
    760765val preinstruction_inv_rect_Type1 :
     
    794799  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
    795800  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
    796   'a2) -> 'a2
     801  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
    797802
    798803val preinstruction_inv_rect_Type0 :
     
    832837  subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode ->
    833838  subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> (__ -> 'a2) -> (__ ->
    834   'a2) -> 'a2
     839  'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2
    835840
    836841val preinstruction_discr : 'a1 preinstruction -> 'a1 preinstruction -> __
     
    848853| LJMP of subaddressing_mode
    849854| SJMP of subaddressing_mode
    850 | JMP of subaddressing_mode
    851855| MOVC of subaddressing_mode * subaddressing_mode
    852856| RealInstruction of subaddressing_mode preinstruction
     
    855859  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    856860  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    857   (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    858   (subaddressing_mode -> subaddressing_mode -> 'a1) -> (subaddressing_mode
    859   preinstruction -> 'a1) -> instruction -> 'a1
     861  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
     862  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
    860863
    861864val instruction_rect_Type5 :
    862865  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    863866  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    864   (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    865   (subaddressing_mode -> subaddressing_mode -> 'a1) -> (subaddressing_mode
    866   preinstruction -> 'a1) -> instruction -> 'a1
     867  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
     868  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
    867869
    868870val instruction_rect_Type3 :
    869871  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    870872  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    871   (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    872   (subaddressing_mode -> subaddressing_mode -> 'a1) -> (subaddressing_mode
    873   preinstruction -> 'a1) -> instruction -> 'a1
     873  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
     874  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
    874875
    875876val instruction_rect_Type2 :
    876877  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    877878  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    878   (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    879   (subaddressing_mode -> subaddressing_mode -> 'a1) -> (subaddressing_mode
    880   preinstruction -> 'a1) -> instruction -> 'a1
     879  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
     880  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
    881881
    882882val instruction_rect_Type1 :
    883883  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    884884  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    885   (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    886   (subaddressing_mode -> subaddressing_mode -> 'a1) -> (subaddressing_mode
    887   preinstruction -> 'a1) -> instruction -> 'a1
     885  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
     886  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
    888887
    889888val instruction_rect_Type0 :
    890889  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    891890  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    892   (subaddressing_mode -> 'a1) -> (subaddressing_mode -> 'a1) ->
    893   (subaddressing_mode -> subaddressing_mode -> 'a1) -> (subaddressing_mode
    894   preinstruction -> 'a1) -> instruction -> 'a1
     891  (subaddressing_mode -> 'a1) -> (subaddressing_mode -> subaddressing_mode ->
     892  'a1) -> (subaddressing_mode preinstruction -> 'a1) -> instruction -> 'a1
    895893
    896894val instruction_inv_rect_Type4 :
     
    898896  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
    899897  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
    900   __ -> 'a1) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a1) ->
    901   (subaddressing_mode preinstruction -> __ -> 'a1) -> 'a1
     898  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
     899  __ -> 'a1) -> 'a1
    902900
    903901val instruction_inv_rect_Type3 :
     
    905903  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
    906904  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
    907   __ -> 'a1) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a1) ->
    908   (subaddressing_mode preinstruction -> __ -> 'a1) -> 'a1
     905  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
     906  __ -> 'a1) -> 'a1
    909907
    910908val instruction_inv_rect_Type2 :
     
    912910  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
    913911  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
    914   __ -> 'a1) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a1) ->
    915   (subaddressing_mode preinstruction -> __ -> 'a1) -> 'a1
     912  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
     913  __ -> 'a1) -> 'a1
    916914
    917915val instruction_inv_rect_Type1 :
     
    919917  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
    920918  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
    921   __ -> 'a1) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a1) ->
    922   (subaddressing_mode preinstruction -> __ -> 'a1) -> 'a1
     919  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
     920  __ -> 'a1) -> 'a1
    923921
    924922val instruction_inv_rect_Type0 :
     
    926924  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
    927925  __ -> 'a1) -> (subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode ->
    928   __ -> 'a1) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a1) ->
    929   (subaddressing_mode preinstruction -> __ -> 'a1) -> 'a1
     926  subaddressing_mode -> __ -> 'a1) -> (subaddressing_mode preinstruction ->
     927  __ -> 'a1) -> 'a1
    930928
    931929val instruction_discr : instruction -> instruction -> __
     
    934932
    935933val eq_instruction : instruction -> instruction -> Bool.bool
     934
     935type word_side =
     936| HIGH
     937| LOW
     938
     939val word_side_rect_Type4 : 'a1 -> 'a1 -> word_side -> 'a1
     940
     941val word_side_rect_Type5 : 'a1 -> 'a1 -> word_side -> 'a1
     942
     943val word_side_rect_Type3 : 'a1 -> 'a1 -> word_side -> 'a1
     944
     945val word_side_rect_Type2 : 'a1 -> 'a1 -> word_side -> 'a1
     946
     947val word_side_rect_Type1 : 'a1 -> 'a1 -> word_side -> 'a1
     948
     949val word_side_rect_Type0 : 'a1 -> 'a1 -> word_side -> 'a1
     950
     951val word_side_inv_rect_Type4 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     952
     953val word_side_inv_rect_Type3 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     954
     955val word_side_inv_rect_Type2 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     956
     957val word_side_inv_rect_Type1 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     958
     959val word_side_inv_rect_Type0 : word_side -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     960
     961val word_side_discr : word_side -> word_side -> __
     962
     963val word_side_jmdiscr : word_side -> word_side -> __
    936964
    937965type pseudo_instruction =
     
    940968| Cost of CostLabel.costlabel
    941969| Jmp of identifier0
     970| Jnz of subaddressing_mode * identifier0 * identifier0
     971| MovSuccessor of subaddressing_mode * word_side * identifier0
    942972| Call of identifier0
    943973| Mov of subaddressing_mode * identifier0
     
    945975val pseudo_instruction_rect_Type4 :
    946976  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    947   (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (identifier0 ->
    948   'a1) -> (subaddressing_mode -> identifier0 -> 'a1) -> pseudo_instruction ->
    949   'a1
     977  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
     978  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
     979  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
     980  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
    950981
    951982val pseudo_instruction_rect_Type5 :
    952983  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    953   (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (identifier0 ->
    954   'a1) -> (subaddressing_mode -> identifier0 -> 'a1) -> pseudo_instruction ->
    955   'a1
     984  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
     985  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
     986  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
     987  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
    956988
    957989val pseudo_instruction_rect_Type3 :
    958990  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    959   (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (identifier0 ->
    960   'a1) -> (subaddressing_mode -> identifier0 -> 'a1) -> pseudo_instruction ->
    961   'a1
     991  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
     992  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
     993  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
     994  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
    962995
    963996val pseudo_instruction_rect_Type2 :
    964997  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    965   (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (identifier0 ->
    966   'a1) -> (subaddressing_mode -> identifier0 -> 'a1) -> pseudo_instruction ->
    967   'a1
     998  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
     999  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
     1000  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
     1001  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
    9681002
    9691003val pseudo_instruction_rect_Type1 :
    9701004  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    971   (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (identifier0 ->
    972   'a1) -> (subaddressing_mode -> identifier0 -> 'a1) -> pseudo_instruction ->
    973   'a1
     1005  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
     1006  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
     1007  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
     1008  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
    9741009
    9751010val pseudo_instruction_rect_Type0 :
    9761011  (identifier0 preinstruction -> 'a1) -> (String.string -> 'a1) ->
    977   (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (identifier0 ->
    978   'a1) -> (subaddressing_mode -> identifier0 -> 'a1) -> pseudo_instruction ->
    979   'a1
     1012  (CostLabel.costlabel -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode
     1013  -> identifier0 -> identifier0 -> 'a1) -> (subaddressing_mode -> word_side
     1014  -> identifier0 -> 'a1) -> (identifier0 -> 'a1) -> (subaddressing_mode ->
     1015  identifier0 -> 'a1) -> pseudo_instruction -> 'a1
    9801016
    9811017val pseudo_instruction_inv_rect_Type4 :
    9821018  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
    9831019  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    984   (identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
     1020  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
     1021  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     1022  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    9851023  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
    9861024
     
    9881026  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
    9891027  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    990   (identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
     1028  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
     1029  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     1030  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    9911031  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
    9921032
     
    9941034  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
    9951035  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    996   (identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
     1036  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
     1037  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     1038  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    9971039  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
    9981040
     
    10001042  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
    10011043  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    1002   (identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
     1044  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
     1045  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     1046  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    10031047  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
    10041048
     
    10061050  pseudo_instruction -> (identifier0 preinstruction -> __ -> 'a1) ->
    10071051  (String.string -> __ -> 'a1) -> (CostLabel.costlabel -> __ -> 'a1) ->
    1008   (identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
     1052  (identifier0 -> __ -> 'a1) -> (subaddressing_mode -> identifier0 ->
     1053  identifier0 -> __ -> 'a1) -> (subaddressing_mode -> word_side ->
     1054  identifier0 -> __ -> 'a1) -> (identifier0 -> __ -> 'a1) ->
    10091055  (subaddressing_mode -> identifier0 -> __ -> 'a1) -> 'a1
    10101056
     
    10161062type labelled_instruction = pseudo_instruction LabelledObjects.labelled_obj
    10171063
    1018 type preamble =
    1019   (Nat.nat Identifiers.identifier_map, (identifier0, BitVector.word)
    1020   Types.prod List.list) Types.prod
     1064type preamble = (identifier0, BitVector.word) Types.prod List.list
    10211065
    10221066type assembly_program = instruction List.list
Note: See TracChangeset for help on using the changeset viewer.