Changeset 2773 for extracted/status.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/status.ml

    r2743 r2773  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open String
    46
     7open Exp
     8
     9open Arithmetic
     10
     11open Vector
     12
     13open FoldStuff
     14
     15open BitVector
     16
     17open Extranat
     18
     19open Integers
     20
     21open AST
     22
    523open LabelledObjects
    624
    7 open BitVectorTrie
    8 
    9 open Exp
    10 
    11 open Arithmetic
    12 
    13 open Integers
    14 
    15 open AST
     25open Proper
     26
     27open PositiveMap
     28
     29open Deqsets
     30
     31open ErrorMessages
     32
     33open PreIdentifiers
     34
     35open Errors
     36
     37open Extralib
     38
     39open Setoids
     40
     41open Monad
     42
     43open Option
     44
     45open Div_and_mod
     46
     47open Jmeq
     48
     49open Russell
     50
     51open Util
     52
     53open List
     54
     55open Lists
     56
     57open Bool
     58
     59open Relations
     60
     61open Nat
     62
     63open Positive
     64
     65open Hints_declaration
     66
     67open Core_notation
     68
     69open Pts
     70
     71open Logic
     72
     73open Types
     74
     75open Identifiers
    1676
    1777open CostLabel
    18 
    19 open Proper
    20 
    21 open PositiveMap
    22 
    23 open Deqsets
    24 
    25 open ErrorMessages
    26 
    27 open PreIdentifiers
    28 
    29 open Errors
    30 
    31 open Extralib
    32 
    33 open Setoids
    34 
    35 open Monad
    36 
    37 open Option
    38 
    39 open Lists
    40 
    41 open Positive
    42 
    43 open Identifiers
    44 
    45 open Extranat
    46 
    47 open Vector
    48 
    49 open Div_and_mod
    50 
    51 open Jmeq
    52 
    53 open Russell
    54 
    55 open Types
    56 
    57 open List
    58 
    59 open Util
    60 
    61 open FoldStuff
    62 
    63 open Bool
    64 
    65 open Hints_declaration
    66 
    67 open Core_notation
    68 
    69 open Pts
    70 
    71 open Logic
    72 
    73 open Relations
    74 
    75 open Nat
    76 
    77 open BitVector
    7878
    7979open ASM
     
    8989    serialBufferType -> 'a1 **)
    9090let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
    91 | Eight x_24138 -> h_Eight x_24138
    92 | Nine (x_24140, x_24139) -> h_Nine x_24140 x_24139
     91| Eight x_19500 -> h_Eight x_19500
     92| Nine (x_19502, x_19501) -> h_Nine x_19502 x_19501
    9393
    9494(** val serialBufferType_rect_Type5 :
     
    9696    serialBufferType -> 'a1 **)
    9797let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
    98 | Eight x_24144 -> h_Eight x_24144
    99 | Nine (x_24146, x_24145) -> h_Nine x_24146 x_24145
     98| Eight x_19506 -> h_Eight x_19506
     99| Nine (x_19508, x_19507) -> h_Nine x_19508 x_19507
    100100
    101101(** val serialBufferType_rect_Type3 :
     
    103103    serialBufferType -> 'a1 **)
    104104let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
    105 | Eight x_24150 -> h_Eight x_24150
    106 | Nine (x_24152, x_24151) -> h_Nine x_24152 x_24151
     105| Eight x_19512 -> h_Eight x_19512
     106| Nine (x_19514, x_19513) -> h_Nine x_19514 x_19513
    107107
    108108(** val serialBufferType_rect_Type2 :
     
    110110    serialBufferType -> 'a1 **)
    111111let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
    112 | Eight x_24156 -> h_Eight x_24156
    113 | Nine (x_24158, x_24157) -> h_Nine x_24158 x_24157
     112| Eight x_19518 -> h_Eight x_19518
     113| Nine (x_19520, x_19519) -> h_Nine x_19520 x_19519
    114114
    115115(** val serialBufferType_rect_Type1 :
     
    117117    serialBufferType -> 'a1 **)
    118118let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
    119 | Eight x_24162 -> h_Eight x_24162
    120 | Nine (x_24164, x_24163) -> h_Nine x_24164 x_24163
     119| Eight x_19524 -> h_Eight x_19524
     120| Nine (x_19526, x_19525) -> h_Nine x_19526 x_19525
    121121
    122122(** val serialBufferType_rect_Type0 :
     
    124124    serialBufferType -> 'a1 **)
    125125let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
    126 | Eight x_24168 -> h_Eight x_24168
    127 | Nine (x_24170, x_24169) -> h_Nine x_24170 x_24169
     126| Eight x_19530 -> h_Eight x_19530
     127| Nine (x_19532, x_19531) -> h_Nine x_19532 x_19531
    128128
    129129(** val serialBufferType_inv_rect_Type4 :
     
    174174
    175175type lineType =
    176 | P2 of BitVector.byte
     176| P1 of BitVector.byte
    177177| P3 of BitVector.byte
    178178| SerialBuffer of serialBufferType
     
    182182    -> 'a1) -> lineType -> 'a1 **)
    183183let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
    184 | P2 x_24217 -> h_P1 x_24217
    185 | P3 x_24218 -> h_P3 x_24218
    186 | SerialBuffer x_24219 -> h_SerialBuffer x_24219
     184| P1 x_19579 -> h_P1 x_19579
     185| P3 x_19580 -> h_P3 x_19580
     186| SerialBuffer x_19581 -> h_SerialBuffer x_19581
    187187
    188188(** val lineType_rect_Type5 :
     
    190190    -> 'a1) -> lineType -> 'a1 **)
    191191let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
    192 | P2 x_24224 -> h_P1 x_24224
    193 | P3 x_24225 -> h_P3 x_24225
    194 | SerialBuffer x_24226 -> h_SerialBuffer x_24226
     192| P1 x_19586 -> h_P1 x_19586
     193| P3 x_19587 -> h_P3 x_19587
     194| SerialBuffer x_19588 -> h_SerialBuffer x_19588
    195195
    196196(** val lineType_rect_Type3 :
     
    198198    -> 'a1) -> lineType -> 'a1 **)
    199199let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
    200 | P2 x_24231 -> h_P1 x_24231
    201 | P3 x_24232 -> h_P3 x_24232
    202 | SerialBuffer x_24233 -> h_SerialBuffer x_24233
     200| P1 x_19593 -> h_P1 x_19593
     201| P3 x_19594 -> h_P3 x_19594
     202| SerialBuffer x_19595 -> h_SerialBuffer x_19595
    203203
    204204(** val lineType_rect_Type2 :
     
    206206    -> 'a1) -> lineType -> 'a1 **)
    207207let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
    208 | P2 x_24238 -> h_P1 x_24238
    209 | P3 x_24239 -> h_P3 x_24239
    210 | SerialBuffer x_24240 -> h_SerialBuffer x_24240
     208| P1 x_19600 -> h_P1 x_19600
     209| P3 x_19601 -> h_P3 x_19601
     210| SerialBuffer x_19602 -> h_SerialBuffer x_19602
    211211
    212212(** val lineType_rect_Type1 :
     
    214214    -> 'a1) -> lineType -> 'a1 **)
    215215let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
    216 | P2 x_24245 -> h_P1 x_24245
    217 | P3 x_24246 -> h_P3 x_24246
    218 | SerialBuffer x_24247 -> h_SerialBuffer x_24247
     216| P1 x_19607 -> h_P1 x_19607
     217| P3 x_19608 -> h_P3 x_19608
     218| SerialBuffer x_19609 -> h_SerialBuffer x_19609
    219219
    220220(** val lineType_rect_Type0 :
     
    222222    -> 'a1) -> lineType -> 'a1 **)
    223223let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
    224 | P2 x_24252 -> h_P1 x_24252
    225 | P3 x_24253 -> h_P3 x_24253
    226 | SerialBuffer x_24254 -> h_SerialBuffer x_24254
     224| P1 x_19614 -> h_P1 x_19614
     225| P3 x_19615 -> h_P3 x_19615
     226| SerialBuffer x_19616 -> h_SerialBuffer x_19616
    227227
    228228(** val lineType_inv_rect_Type4 :
     
    260260  Logic.eq_rect_Type2 x
    261261    (match x with
    262      | P2 a0 -> Obj.magic (fun _ dH -> dH __)
     262     | P1 a0 -> Obj.magic (fun _ dH -> dH __)
    263263     | P3 a0 -> Obj.magic (fun _ dH -> dH __)
    264264     | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y
     
    268268  Logic.eq_rect_Type2 x
    269269    (match x with
    270      | P2 a0 -> Obj.magic (fun _ dH -> dH __)
     270     | P1 a0 -> Obj.magic (fun _ dH -> dH __)
    271271     | P3 a0 -> Obj.magic (fun _ dH -> dH __)
    272272     | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y
     
    731731    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    732732    preStatus -> 'a2 **)
    733 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_24640 =
     733let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_20002 =
    734734  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    735735    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    737737    special_function_registers_8053; special_function_registers_8052 =
    738738    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    739     p3_latch0; clock = clock0 } = x_24640
     739    p3_latch0; clock = clock0 } = x_20002
    740740  in
    741741  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    749749    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    750750    preStatus -> 'a2 **)
    751 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_24642 =
     751let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_20004 =
    752752  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    753753    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    755755    special_function_registers_8053; special_function_registers_8052 =
    756756    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    757     p3_latch0; clock = clock0 } = x_24642
     757    p3_latch0; clock = clock0 } = x_20004
    758758  in
    759759  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    767767    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    768768    preStatus -> 'a2 **)
    769 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_24644 =
     769let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_20006 =
    770770  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    771771    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    773773    special_function_registers_8053; special_function_registers_8052 =
    774774    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    775     p3_latch0; clock = clock0 } = x_24644
     775    p3_latch0; clock = clock0 } = x_20006
    776776  in
    777777  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    785785    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    786786    preStatus -> 'a2 **)
    787 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_24646 =
     787let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_20008 =
    788788  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    789789    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    791791    special_function_registers_8053; special_function_registers_8052 =
    792792    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    793     p3_latch0; clock = clock0 } = x_24646
     793    p3_latch0; clock = clock0 } = x_20008
    794794  in
    795795  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    803803    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    804804    preStatus -> 'a2 **)
    805 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_24648 =
     805let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_20010 =
    806806  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    807807    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    809809    special_function_registers_8053; special_function_registers_8052 =
    810810    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    811     p3_latch0; clock = clock0 } = x_24648
     811    p3_latch0; clock = clock0 } = x_20010
    812812  in
    813813  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    821821    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    822822    preStatus -> 'a2 **)
    823 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_24650 =
     823let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_20012 =
    824824  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    825825    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    827827    special_function_registers_8053; special_function_registers_8052 =
    828828    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    829     p3_latch0; clock = clock0 } = x_24650
     829    p3_latch0; clock = clock0 } = x_20012
    830830  in
    831831  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    36393639      (Nat.S Nat.O)))) (get_8051_sfr code_memory s SFR_PSW)
    36403640  in
    3641   let { Types.fst = r5; Types.snd = r6 } = { Types.fst =
     3641  let { Types.fst = r1; Types.snd = r0 } = { Types.fst =
    36423642    (Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) un (Nat.S
    36433643      (Nat.S Nat.O))); Types.snd =
     
    36463646  in
    36473647  let offset =
    3648     match Bool.andb (Bool.notb r5) (Bool.notb r6) with
     3648    match Bool.andb (Bool.notb r1) (Bool.notb r0) with
    36493649    | Bool.True -> Nat.O
    36503650    | Bool.False ->
    3651       (match Bool.andb (Bool.notb r5) r6 with
     3651      (match Bool.andb (Bool.notb r1) r0 with
    36523652       | Bool.True ->
    36533653         Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
    36543654       | Bool.False ->
    3655          (match Bool.andb r5 r6 with
     3655         (match Bool.andb r1 r0 with
    36563656          | Bool.True ->
    36573657            Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    38223822   | ASM.DIRECT d ->
    38233823     (fun _ ->
    3824        let { Types.fst = hd0; Types.snd = seven_bits } =
     3824       let { Types.fst = hd; Types.snd = seven_bits } =
    38253825         Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    38263826           (Nat.S (Nat.S Nat.O))))))) d
    38273827       in
    3828        (match Vector.head' Nat.O hd0 with
     3828       (match Vector.head' Nat.O hd with
    38293829        | Bool.True ->
    38303830          get_bit_addressable_sfr cm s (Vector.VCons ((Nat.S (Nat.S (Nat.S
     
    38383838   | ASM.INDIRECT i ->
    38393839     (fun _ ->
    3840        let { Types.fst = hd0; Types.snd = seven_bits } =
     3840       let { Types.fst = hd; Types.snd = seven_bits } =
    38413841         Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    38423842           (Nat.S (Nat.S Nat.O)))))))
     
    38453845             (Vector.VCons (Nat.O, i, Vector.VEmpty)))))))
    38463846       in
    3847        (match Vector.head' Nat.O hd0 with
     3847       (match Vector.head' Nat.O hd with
    38483848        | Bool.True ->
    38493849          BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    38563856            (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    38573857              (Nat.S Nat.O)))))))))))
    3858    | ASM.EXT_INDIRECT e0 ->
     3858   | ASM.EXT_INDIRECT e ->
    38593859     (fun _ ->
    38603860       let address =
    38613861         get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
    3862            (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
    3863            e0, Vector.VEmpty))))))
     3862           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, e,
     3863           Vector.VEmpty))))))
    38643864       in
    38653865       let padded_address =
     
    38823882     (fun _ ->
    38833883       let dptr =
    3884          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3884         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    38853885           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    38863886           (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
     
    39223922     (fun _ ->
    39233923       let address =
    3924          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3924         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    39253925           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    39263926           (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
     
    39943994          in
    39953995          set_low_internal_ram cm s memory))
    3996    | ASM.EXT_INDIRECT e0 ->
     3996   | ASM.EXT_INDIRECT e ->
    39973997     (fun _ ->
    39983998       let address =
    39993999         get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
    4000            (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
    4001            e0, Vector.VEmpty))))))
     4000           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, e,
     4001           Vector.VEmpty))))))
    40024002       in
    40034003       let padded_address =
     
    40234023     (fun _ ->
    40244024       let address =
    4025          Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4025         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    40264026           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    40274027           (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
     
    40764076          in
    40774077          let trans =
    4078             Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     4078            Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
    40794079              (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
    40804080              (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons
     
    40944094          in
    40954095          let address' =
    4096             Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
     4096            Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
    40974097              (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
    40984098              Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
     
    41224122          in
    41234123          let trans =
    4124             Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     4124            Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
    41254125              (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
    41264126              (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons
     
    41414141          in
    41424142          let address' =
    4143             Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
     4143            Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
    41444144              (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
    41454145              Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
     
    42034203          in
    42044204          let trans =
    4205             Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     4205            Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
    42064206              (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
    42074207              (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons
     
    42244224          in
    42254225          let address' =
    4226             Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
     4226            Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
    42274227              (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
    42284228              Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
     
    42514251   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
    42524252
    4253 (** val fetch_pseudo_instruction :
    4254     ASM.labelled_instruction List.list -> BitVector.word ->
    4255     (ASM.pseudo_instruction, BitVector.word) Types.prod **)
    4256 let fetch_pseudo_instruction code_mem pc =
    4257   let { Types.fst = lbl; Types.snd = instr } =
    4258     Util.nth_safe
    4259       (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4260         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4261         Nat.O)))))))))))))))) pc) code_mem
    4262   in
    4263   let new_pc =
    4264     Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4265       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4266       Nat.O)))))))))))))))) pc
    4267       (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4268         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4269         Nat.O)))))))))))))))) (Nat.S Nat.O))
    4270   in
    4271   { Types.fst = instr; Types.snd = new_pc }
    4272 
    42734253(** val construct_datalabels :
    4274     ASM.preamble -> BitVector.word Identifiers.identifier_map **)
     4254    (ASM.identifier, BitVector.word) Types.prod List.list -> BitVector.word
     4255    Identifiers.identifier_map **)
    42754256let construct_datalabels the_preamble =
    4276   (Util.foldl (fun t preamble0 ->
     4257  (Util.foldl (fun t preamble ->
    42774258    let { Types.fst = datalabels; Types.snd = addr } = t in
    4278     let { Types.fst = name; Types.snd = size } = preamble0 in
    4279     let { Types.fst = carry; Types.snd = sum0 } =
     4259    let { Types.fst = name; Types.snd = size } = preamble in
     4260    let { Types.fst = carry; Types.snd = sum } =
    42804261      Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    42814262        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    42844265    { Types.fst =
    42854266    (Identifiers.add PreIdentifiers.ASMTag datalabels name addr); Types.snd =
    4286     sum0 }) { Types.fst = (Identifiers.empty_map PreIdentifiers.ASMTag);
     4267    sum }) { Types.fst = (Identifiers.empty_map PreIdentifiers.ASMTag);
    42874268    Types.snd =
    42884269    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
Note: See TracChangeset for help on using the changeset viewer.