Changeset 3077


Ignore:
Timestamp:
Apr 3, 2013, 11:49:45 AM (4 years ago)
Author:
sacerdot
Message:

New extraction.

Location:
extracted
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • extracted/assembly.ml

    r3069 r3077  
    11open Preamble
    22
     3open Div_and_mod
     4
     5open Jmeq
     6
     7open Russell
     8
     9open Util
     10
     11open Bool
     12
     13open Relations
     14
     15open Nat
     16
     17open List
     18
     19open Hints_declaration
     20
     21open Core_notation
     22
     23open Pts
     24
     25open Logic
     26
     27open Types
     28
     29open Extralib
     30
    331open BitVectorTrie
    432
    533open String
    634
     35open Integers
     36
     37open AST
     38
     39open LabelledObjects
     40
     41open Proper
     42
     43open PositiveMap
     44
     45open Deqsets
     46
     47open ErrorMessages
     48
     49open PreIdentifiers
     50
     51open Errors
     52
     53open Lists
     54
     55open Positive
     56
     57open Identifiers
     58
     59open CostLabel
     60
     61open ASM
     62
    763open Exp
    864
     65open Setoids
     66
     67open Monad
     68
     69open Option
     70
     71open Extranat
     72
     73open Vector
     74
     75open FoldStuff
     76
     77open BitVector
     78
    979open Arithmetic
    10 
    11 open Vector
    12 
    13 open FoldStuff
    14 
    15 open BitVector
    16 
    17 open Extranat
    18 
    19 open Integers
    20 
    21 open AST
    22 
    23 open LabelledObjects
    24 
    25 open Proper
    26 
    27 open PositiveMap
    28 
    29 open Deqsets
    30 
    31 open ErrorMessages
    32 
    33 open PreIdentifiers
    34 
    35 open Errors
    36 
    37 open Extralib
    38 
    39 open Setoids
    40 
    41 open Monad
    42 
    43 open Option
    44 
    45 open Div_and_mod
    46 
    47 open Jmeq
    48 
    49 open Russell
    50 
    51 open Util
    52 
    53 open List
    54 
    55 open Lists
    56 
    57 open Bool
    58 
    59 open Relations
    60 
    61 open Nat
    62 
    63 open Positive
    64 
    65 open Hints_declaration
    66 
    67 open Core_notation
    68 
    69 open Pts
    70 
    71 open Logic
    72 
    73 open Types
    74 
    75 open Identifiers
    76 
    77 open CostLabel
    78 
    79 open ASM
    8080
    8181open Fetch
  • extracted/assembly.mli

    r3069 r3077  
    11open Preamble
     2
     3open Div_and_mod
     4
     5open Jmeq
     6
     7open Russell
     8
     9open Util
     10
     11open Bool
     12
     13open Relations
     14
     15open Nat
     16
     17open List
     18
     19open Hints_declaration
     20
     21open Core_notation
     22
     23open Pts
     24
     25open Logic
     26
     27open Types
     28
     29open Extralib
    230
    331open BitVectorTrie
    432
    533open String
    6 
    7 open Exp
    8 
    9 open Arithmetic
    10 
    11 open Vector
    12 
    13 open FoldStuff
    14 
    15 open BitVector
    16 
    17 open Extranat
    1834
    1935open Integers
     
    3551open Errors
    3652
    37 open Extralib
     53open Lists
     54
     55open Positive
     56
     57open Identifiers
     58
     59open CostLabel
     60
     61open ASM
     62
     63open Exp
    3864
    3965open Setoids
     
    4369open Option
    4470
    45 open Div_and_mod
     71open Extranat
    4672
    47 open Jmeq
     73open Vector
    4874
    49 open Russell
     75open FoldStuff
    5076
    51 open Util
     77open BitVector
    5278
    53 open List
    54 
    55 open Lists
    56 
    57 open Bool
    58 
    59 open Relations
    60 
    61 open Nat
    62 
    63 open Positive
    64 
    65 open Hints_declaration
    66 
    67 open Core_notation
    68 
    69 open Pts
    70 
    71 open Logic
    72 
    73 open Types
    74 
    75 open Identifiers
    76 
    77 open CostLabel
    78 
    79 open ASM
     79open Arithmetic
    8080
    8181open Fetch
  • extracted/status.ml

    r3069 r3077  
    11open Preamble
    22
     3open Types
     4
     5open Hints_declaration
     6
     7open Core_notation
     8
     9open Pts
     10
     11open Logic
     12
     13open Jmeq
     14
     15open Russell
     16
    317open BitVectorTrie
    418
     
    4559open Div_and_mod
    4660
    47 open Jmeq
    48 
    49 open Russell
    50 
    5161open Util
    5262
     
    6272
    6373open Positive
    64 
    65 open Hints_declaration
    66 
    67 open Core_notation
    68 
    69 open Pts
    70 
    71 open Logic
    72 
    73 open Types
    7474
    7575open Identifiers
     
    11191119  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
    11201120
     1121(** val update_low_internal_ram :
     1122    'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
     1123    preStatus **)
     1124let update_low_internal_ram code_memory s addr v =
     1125  let old_low_internal_ram = s.low_internal_ram in
     1126  let new_low_internal_ram =
     1127    BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1128      Nat.O))))))) addr v old_low_internal_ram
     1129  in
     1130  set_low_internal_ram code_memory s new_low_internal_ram
     1131
    11211132(** val set_high_internal_ram :
    11221133    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
     
    11401151  p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
    11411152
     1153(** val update_high_internal_ram :
     1154    'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
     1155    preStatus **)
     1156let update_high_internal_ram code_memory s addr v =
     1157  let old_high_internal_ram = s.high_internal_ram in
     1158  let new_high_internal_ram =
     1159    BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1160      Nat.O))))))) addr v old_high_internal_ram
     1161  in
     1162  set_high_internal_ram code_memory s new_high_internal_ram
     1163
    11421164(** val set_external_ram :
    11431165    'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
     
    11611183  old_p3_latch; clock = old_clock }
    11621184
     1185(** val update_external_ram :
     1186    'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
     1187    preStatus **)
     1188let update_external_ram code_memory s addr v =
     1189  let old_external_ram = s.external_ram in
     1190  let new_external_ram =
     1191    BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1192      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1193      Nat.O)))))))))))))))) addr v old_external_ram
     1194  in
     1195  set_external_ram code_memory s new_external_ram
     1196
     1197(** val get_psw_flags : 'a1 -> 'a1 preStatus -> Nat.nat -> Bool.bool **)
     1198let get_psw_flags code_memory s flag =
     1199  let psw = get_8051_sfr code_memory s SFR_PSW in
     1200  Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1201    Nat.O)))))))) psw flag
     1202
    11631203(** val get_cy_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
    11641204let get_cy_flag code_memory s =
    1165   let sfr = s.special_function_registers_8051 in
    1166   let psw =
    1167     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1168       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1169       (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
    1170   in
    1171   Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1172     Nat.O)))))))) psw Nat.O
     1205  get_psw_flags code_memory s Nat.O
    11731206
    11741207(** val get_ac_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
    11751208let get_ac_flag code_memory s =
    1176   let sfr = s.special_function_registers_8051 in
    1177   let psw =
    1178     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1179       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1180       (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
    1181   in
    1182   Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1183     Nat.O)))))))) psw (Nat.S Nat.O)
     1209  get_psw_flags code_memory s (Nat.S Nat.O)
    11841210
    11851211(** val get_fo_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
    11861212let get_fo_flag code_memory s =
    1187   let sfr = s.special_function_registers_8051 in
    1188   let psw =
    1189     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1190       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1191       (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
    1192   in
    1193   Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1194     Nat.O)))))))) psw (Nat.S (Nat.S Nat.O))
     1213  get_psw_flags code_memory s (Nat.S (Nat.S Nat.O))
    11951214
    11961215(** val get_rs1_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
    11971216let get_rs1_flag code_memory s =
    1198   let sfr = s.special_function_registers_8051 in
    1199   let psw =
    1200     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1201       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1202       (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
    1203   in
    1204   Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1205     Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S Nat.O)))
     1217  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S Nat.O)))
    12061218
    12071219(** val get_rs0_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
    12081220let get_rs0_flag code_memory s =
    1209   let sfr = s.special_function_registers_8051 in
    1210   let psw =
    1211     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1212       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1213       (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
    1214   in
    1215   Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1216     Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
     1221  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
    12171222
    12181223(** val get_ov_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
    12191224let get_ov_flag code_memory s =
    1220   let sfr = s.special_function_registers_8051 in
    1221   let psw =
    1222     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1223       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1224       (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
    1225   in
    1226   Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1227     Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     1225  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
    12281226
    12291227(** val get_ud_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
    12301228let get_ud_flag code_memory s =
    1231   let sfr = s.special_function_registers_8051 in
    1232   let psw =
    1233     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1234       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1235       (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
    1236   in
    1237   Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1238     Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
     1229  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1230    Nat.O))))))
    12391231
    12401232(** val get_p_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
    12411233let get_p_flag code_memory s =
    1242   let sfr = s.special_function_registers_8051 in
    1243   let psw =
    1244     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1245       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1246       (Nat.S (Nat.S Nat.O))))))))))))))))))) sfr (sfr_8051_index SFR_PSW)
    1247   in
    1248   Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1249     Nat.O)))))))) psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1250     Nat.O)))))))
     1234  get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1235    (Nat.S Nat.O)))))))
    12511236
    12521237(** val set_flags :
     
    12541239    BitVector.bit -> 'a1 preStatus **)
    12551240let set_flags code_memory s cy ac ov =
    1256   let sfr_psw = get_8051_sfr code_memory s SFR_PSW in
    1257   let old_cy =
    1258     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1259       (Nat.S Nat.O)))))))) sfr_psw Nat.O
    1260   in
    1261   let old_ac =
    1262     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1263       (Nat.S Nat.O)))))))) sfr_psw (Nat.S Nat.O)
    1264   in
    1265   let old_fo =
    1266     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1267       (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S Nat.O))
    1268   in
    1269   let old_rs1 =
    1270     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1271       (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S Nat.O)))
    1272   in
    1273   let old_rs0 =
    1274     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1275       (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
    1276   in
    1277   let old_ov =
    1278     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1279       (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1280       Nat.O)))))
    1281   in
    1282   let old_ud =
    1283     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1284       (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1285       Nat.O))))))
    1286   in
    1287   let old_p =
    1288     Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1289       (Nat.S Nat.O)))))))) sfr_psw (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1290       (Nat.S Nat.O)))))))
    1291   in
     1241  let old_cy = get_cy_flag code_memory s in
     1242  let old_ac = get_ac_flag code_memory s in
     1243  let old_fo = get_fo_flag code_memory s in
     1244  let old_rs1 = get_rs1_flag code_memory s in
     1245  let old_rs0 = get_rs0_flag code_memory s in
     1246  let old_ov = get_ov_flag code_memory s in
     1247  let old_ud = get_ud_flag code_memory s in
     1248  let old_p = get_p_flag code_memory s in
    12921249  let new_ac =
    12931250    match ac with
     
    36353592    Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) r (Nat.S (Nat.S Nat.O))
    36363593  in
    3637   let { Types.fst = un; Types.snd = ln } =
    3638     Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
    3639       (Nat.S Nat.O)))) (get_8051_sfr code_memory s SFR_PSW)
    3640   in
    3641   let { Types.fst = r1; Types.snd = r0 } = { Types.fst =
    3642     (Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) un (Nat.S
    3643       (Nat.S Nat.O))); Types.snd =
    3644     (Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) un (Nat.S
    3645       (Nat.S (Nat.S Nat.O)))) }
    3646   in
     3594  let r1 = get_rs1_flag code_memory s in
     3595  let r0 = get_rs0_flag code_memory s in
    36473596  let offset =
    36483597    match Bool.andb (Bool.notb r1) (Bool.notb r0) with
     
    36863635let set_register code_memory s r v =
    36873636  let address = bit_address_of_register code_memory s r in
    3688   let old_low_internal_ram = s.low_internal_ram in
    3689   let new_low_internal_ram =
    3690     BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3691       Nat.O))))))) address v old_low_internal_ram
    3692   in
    3693   set_low_internal_ram code_memory s new_low_internal_ram
     3637  update_low_internal_ram code_memory s address v
     3638
     3639(** val read_from_external_ram :
     3640    'a1 -> 'a1 preStatus -> BitVector.word -> BitVector.byte **)
     3641let read_from_external_ram code_memory s addr =
     3642  BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3643    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3644    Nat.O)))))))))))))))) addr s.external_ram
     3645    (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3646      Nat.O)))))))))
    36943647
    36953648(** val read_from_internal_ram :
     
    37223675  in
    37233676  (match Vector.head' Nat.O bit_one with
    3724    | Bool.True ->
    3725      let memory =
    3726        BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3727          Nat.O))))))) seven_bits v s.high_internal_ram
    3728      in
    3729      set_high_internal_ram code_memory s memory
    3730    | Bool.False ->
    3731      let memory =
    3732        BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3733          Nat.O))))))) seven_bits v s.low_internal_ram
    3734      in
    3735      set_low_internal_ram code_memory s memory)
     3677   | Bool.True -> update_high_internal_ram code_memory s seven_bits v
     3678   | Bool.False -> update_low_internal_ram code_memory s seven_bits v)
    37363679
    37373680(** val set_arg_16' :
     
    38873830           (Nat.S (Nat.S Nat.O)))))))) address
    38883831       in
    3889        BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3890          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3891          Nat.O)))))))))))))))) padded_address s.external_ram
    3892          (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3893            (Nat.S Nat.O))))))))))
     3832       read_from_external_ram cm s padded_address)
    38943833   | ASM.REGISTER r -> (fun _ -> get_register cm s r)
    38953834   | ASM.ACC_A -> (fun _ -> get_8051_sfr cm s SFR_ACC_A)
     
    39163855           Nat.O)))))))))))))))) dptr padded_acc
    39173856       in
    3918        BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3919          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3920          Nat.O)))))))))))))))) address s.external_ram
    3921          (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3922            (Nat.S Nat.O))))))))))
     3857       read_from_external_ram cm s address)
    39233858   | ASM.ACC_PC ->
    39243859     (fun _ ->
     
    39333868           Nat.O)))))))))))))))) s.program_counter padded_acc
    39343869       in
    3935        BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3936          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3937          Nat.O)))))))))))))))) address s.external_ram
    3938          (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3939            (Nat.S Nat.O))))))))))
     3870       read_from_external_ram cm s address)
    39403871   | ASM.EXT_INDIRECT_DPTR ->
    39413872     (fun _ ->
     
    39463877           (get_8051_sfr cm s SFR_DPL)
    39473878       in
    3948        BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3949          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3950          Nat.O)))))))))))))))) address s.external_ram
    3951          (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3952            (Nat.S Nat.O))))))))))
     3879       read_from_external_ram cm s address)
    39533880   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
    39543881   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
     
    39833910            (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, seven_bits))
    39843911            v
    3985         | Bool.False ->
    3986           let memory =
    3987             BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3988               (Nat.S Nat.O))))))) seven_bits v s.low_internal_ram
    3989           in
    3990           set_low_internal_ram cm s memory))
     3912        | Bool.False -> update_low_internal_ram cm s seven_bits v))
    39913913   | ASM.INDIRECT i ->
    39923914     (fun _ ->
     
    40013923       in
    40023924       (match Vector.head' Nat.O bit_one with
    4003         | Bool.True ->
    4004           let memory =
    4005             BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4006               (Nat.S Nat.O))))))) seven_bits v s.high_internal_ram
    4007           in
    4008           set_high_internal_ram cm s memory
    4009         | Bool.False ->
    4010           let memory =
    4011             BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4012               (Nat.S Nat.O))))))) seven_bits v s.low_internal_ram
    4013           in
    4014           set_low_internal_ram cm s memory))
     3925        | Bool.True -> update_high_internal_ram cm s seven_bits v
     3926        | Bool.False -> update_low_internal_ram cm s seven_bits v))
    40153927   | ASM.EXT_INDIRECT e ->
    40163928     (fun _ ->
     
    40253937           (Nat.S (Nat.S Nat.O)))))))) address
    40263938       in
    4027        let memory =
    4028          BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4029            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4030            (Nat.S Nat.O)))))))))))))))) padded_address v s.external_ram
    4031        in
    4032        set_external_ram cm s memory)
     3939       update_external_ram cm s padded_address v)
    40333940   | ASM.REGISTER r -> (fun _ -> set_register cm s r v)
    40343941   | ASM.ACC_A -> (fun _ -> set_8051_sfr cm s SFR_ACC_A v)
     
    40473954           (get_8051_sfr cm s SFR_DPL)
    40483955       in
    4049        let memory =
    4050          BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4051            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4052            (Nat.S Nat.O)))))))))))))))) address v s.external_ram
    4053        in
    4054        set_external_ram cm s memory)
     3956       update_external_ram cm s address v)
    40553957   | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
    40563958   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
     
    40883990           (Nat.S (Nat.S Nat.O))))))) b
    40893991       in
     3992       let { Types.fst = four_bits; Types.snd = three_bits } =
     3993         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
     3994           (Nat.S Nat.O))) seven_bits
     3995       in
    40903996       (match Vector.head' Nat.O bit_1 with
    40913997        | Bool.True ->
    4092           let { Types.fst = four_bits; Types.snd = three_bits } =
    4093             Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    4094               (Nat.S Nat.O))) seven_bits
    4095           in
    40963998          let trans =
    40973999            Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     
    41084010              three_bits)
    41094011        | Bool.False ->
    4110           let { Types.fst = four_bits; Types.snd = three_bits } =
    4111             Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    4112               (Nat.S Nat.O))) seven_bits
    4113           in
    41144012          let address' =
    41154013            Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
     
    41194017          in
    41204018          let t =
    4121             BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4122               (Nat.S Nat.O))))))) address' s.low_internal_ram
     4019            BitVectorTrie.lookup
     4020              (Nat.plus (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
     4021                (Nat.S Nat.O))))) address' s.low_internal_ram
    41234022              (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    41244023                (Nat.S (Nat.S Nat.O)))))))))
     
    41344033           (Nat.S (Nat.S Nat.O))))))) n
    41354034       in
     4035       let { Types.fst = four_bits; Types.snd = three_bits } =
     4036         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
     4037           (Nat.S Nat.O))) seven_bits
     4038       in
    41364039       (match Vector.head' Nat.O bit_1 with
    41374040        | Bool.True ->
    4138           let { Types.fst = four_bits; Types.snd = three_bits } =
    4139             Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    4140               (Nat.S Nat.O))) seven_bits
    4141           in
    41424041          let trans =
    41434042            Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     
    41554054                three_bits))
    41564055        | Bool.False ->
    4157           let { Types.fst = four_bits; Types.snd = three_bits } =
    4158             Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    4159               (Nat.S Nat.O))) seven_bits
    4160           in
    41614056          let address' =
    41624057            Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
     
    42154110           (Nat.S (Nat.S Nat.O))))))) b
    42164111       in
     4112       let { Types.fst = four_bits; Types.snd = three_bits } =
     4113         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
     4114           (Nat.S Nat.O))) seven_bits
     4115       in
    42174116       (match Vector.head' Nat.O bit_1 with
    42184117        | Bool.True ->
    4219           let { Types.fst = four_bits; Types.snd = three_bits } =
    4220             Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    4221               (Nat.S Nat.O))) seven_bits
    4222           in
    42234118          let trans =
    42244119            Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
     
    42384133          set_bit_addressable_sfr cm s new_sfr trans
    42394134        | Bool.False ->
    4240           let { Types.fst = four_bits; Types.snd = three_bits } =
    4241             Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    4242               (Nat.S Nat.O))) seven_bits
    4243           in
    42444135          let address' =
    42454136            Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
     
    42604151                three_bits) v
    42614152          in
    4262           let memory =
    4263             BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    4264               (Nat.S Nat.O))))))) address' n_bit s.low_internal_ram
    4265           in
    4266           set_low_internal_ram cm s memory))
     4153          update_low_internal_ram cm s address' n_bit))
    42674154   | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
    42684155   | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
  • extracted/status.mli

    r2773 r3077  
    11open Preamble
    22
     3open Types
     4
     5open Hints_declaration
     6
     7open Core_notation
     8
     9open Pts
     10
     11open Logic
     12
     13open Jmeq
     14
     15open Russell
     16
    317open BitVectorTrie
    418
     
    4559open Div_and_mod
    4660
    47 open Jmeq
    48 
    49 open Russell
    50 
    5161open Util
    5262
     
    6272
    6373open Positive
    64 
    65 open Hints_declaration
    66 
    67 open Core_notation
    68 
    69 open Pts
    70 
    71 open Logic
    72 
    73 open Types
    7474
    7575open Identifiers
     
    457457  preStatus
    458458
     459val update_low_internal_ram :
     460  'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
     461  preStatus
     462
    459463val set_high_internal_ram :
    460464  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
    461465  preStatus
    462466
     467val update_high_internal_ram :
     468  'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
     469  preStatus
     470
    463471val set_external_ram :
    464472  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
    465473  preStatus
     474
     475val update_external_ram :
     476  'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
     477  preStatus
     478
     479val get_psw_flags : 'a1 -> 'a1 preStatus -> Nat.nat -> Bool.bool
    466480
    467481val get_cy_flag : 'a1 -> 'a1 preStatus -> Bool.bool
     
    505519  preStatus
    506520
     521val read_from_external_ram :
     522  'a1 -> 'a1 preStatus -> BitVector.word -> BitVector.byte
     523
    507524val read_from_internal_ram :
    508525  'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte
Note: See TracChangeset for help on using the changeset viewer.