Changeset 3080


Ignore:
Timestamp:
Apr 3, 2013, 5:27:02 PM (4 years ago)
Author:
sacerdot
Message:

New extraction.

Location:
extracted
Files:
15 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSMCosts.ml

    r3059 r3080  
    7575open Div_and_mod
    7676
     77open Util
     78
     79open List
     80
     81open Lists
     82
     83open Bool
     84
     85open Relations
     86
     87open Nat
     88
     89open Positive
     90
     91open Identifiers
     92
     93open CostLabel
     94
     95open ASM
     96
     97open Types
     98
     99open Hints_declaration
     100
     101open Core_notation
     102
     103open Pts
     104
     105open Logic
     106
    77107open Jmeq
    78108
    79109open Russell
    80 
    81 open Util
    82 
    83 open List
    84 
    85 open Lists
    86 
    87 open Bool
    88 
    89 open Relations
    90 
    91 open Nat
    92 
    93 open Positive
    94 
    95 open Hints_declaration
    96 
    97 open Core_notation
    98 
    99 open Pts
    100 
    101 open Logic
    102 
    103 open Types
    104 
    105 open Identifiers
    106 
    107 open CostLabel
    108 
    109 open ASM
    110110
    111111open Status
     
    502502   | Nat.S program_size' ->
    503503     (fun _ ->
    504        (let { Types.fst = eta31464; Types.snd = ticks } =
     504       (let { Types.fst = eta31588; Types.snd = ticks } =
    505505          Fetch.fetch prog.ASM.cm program_counter'
    506506        in
    507507       let { Types.fst = instruction; Types.snd = program_counter'' } =
    508          eta31464
     508         eta31588
    509509       in
    510510       (fun _ ->
  • extracted/aSMCosts.mli

    r2910 r3080  
    7575open Div_and_mod
    7676
    77 open Jmeq
    78 
    79 open Russell
    80 
    8177open Util
    8278
     
    9389open Positive
    9490
     91open Identifiers
     92
     93open CostLabel
     94
     95open ASM
     96
     97open Types
     98
    9599open Hints_declaration
    96100
     
    101105open Logic
    102106
    103 open Types
     107open Jmeq
    104108
    105 open Identifiers
    106 
    107 open CostLabel
    108 
    109 open ASM
     109open Russell
    110110
    111111open Status
  • extracted/aSMCostsSplit.ml

    r2997 r3080  
    7575open Div_and_mod
    7676
    77 open Jmeq
    78 
    79 open Russell
    80 
    8177open Util
    8278
     
    9389open Positive
    9490
     91open Identifiers
     92
     93open CostLabel
     94
     95open ASM
     96
     97open Types
     98
    9599open Hints_declaration
    96100
     
    101105open Logic
    102106
    103 open Types
     107open Jmeq
    104108
    105 open Identifiers
    106 
    107 open CostLabel
    108 
    109 open ASM
     109open Russell
    110110
    111111open Status
  • extracted/aSMCostsSplit.mli

    r2997 r3080  
    7575open Div_and_mod
    7676
    77 open Jmeq
    78 
    79 open Russell
    80 
    8177open Util
    8278
     
    9389open Positive
    9490
     91open Identifiers
     92
     93open CostLabel
     94
     95open ASM
     96
     97open Types
     98
    9599open Hints_declaration
    96100
     
    101105open Logic
    102106
    103 open Types
     107open Jmeq
    104108
    105 open Identifiers
    106 
    107 open CostLabel
    108 
    109 open ASM
     109open Russell
    110110
    111111open Status
  • extracted/eRTLToLTL.ml

    r3073 r3080  
    179179    arg_decision -> 'a1 **)
    180180let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    181 | Arg_decision_colour x_9 -> h_arg_decision_colour x_9
    182 | Arg_decision_spill x_10 -> h_arg_decision_spill x_10
    183 | Arg_decision_imm x_11 -> h_arg_decision_imm x_11
     181| Arg_decision_colour x_19045 -> h_arg_decision_colour x_19045
     182| Arg_decision_spill x_19046 -> h_arg_decision_spill x_19046
     183| Arg_decision_imm x_19047 -> h_arg_decision_imm x_19047
    184184
    185185(** val arg_decision_rect_Type5 :
     
    187187    arg_decision -> 'a1 **)
    188188let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    189 | Arg_decision_colour x_16 -> h_arg_decision_colour x_16
    190 | Arg_decision_spill x_17 -> h_arg_decision_spill x_17
    191 | Arg_decision_imm x_18 -> h_arg_decision_imm x_18
     189| Arg_decision_colour x_19052 -> h_arg_decision_colour x_19052
     190| Arg_decision_spill x_19053 -> h_arg_decision_spill x_19053
     191| Arg_decision_imm x_19054 -> h_arg_decision_imm x_19054
    192192
    193193(** val arg_decision_rect_Type3 :
     
    195195    arg_decision -> 'a1 **)
    196196let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    197 | Arg_decision_colour x_23 -> h_arg_decision_colour x_23
    198 | Arg_decision_spill x_24 -> h_arg_decision_spill x_24
    199 | Arg_decision_imm x_25 -> h_arg_decision_imm x_25
     197| Arg_decision_colour x_19059 -> h_arg_decision_colour x_19059
     198| Arg_decision_spill x_19060 -> h_arg_decision_spill x_19060
     199| Arg_decision_imm x_19061 -> h_arg_decision_imm x_19061
    200200
    201201(** val arg_decision_rect_Type2 :
     
    203203    arg_decision -> 'a1 **)
    204204let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    205 | Arg_decision_colour x_30 -> h_arg_decision_colour x_30
    206 | Arg_decision_spill x_31 -> h_arg_decision_spill x_31
    207 | Arg_decision_imm x_32 -> h_arg_decision_imm x_32
     205| Arg_decision_colour x_19066 -> h_arg_decision_colour x_19066
     206| Arg_decision_spill x_19067 -> h_arg_decision_spill x_19067
     207| Arg_decision_imm x_19068 -> h_arg_decision_imm x_19068
    208208
    209209(** val arg_decision_rect_Type1 :
     
    211211    arg_decision -> 'a1 **)
    212212let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    213 | Arg_decision_colour x_37 -> h_arg_decision_colour x_37
    214 | Arg_decision_spill x_38 -> h_arg_decision_spill x_38
    215 | Arg_decision_imm x_39 -> h_arg_decision_imm x_39
     213| Arg_decision_colour x_19073 -> h_arg_decision_colour x_19073
     214| Arg_decision_spill x_19074 -> h_arg_decision_spill x_19074
     215| Arg_decision_imm x_19075 -> h_arg_decision_imm x_19075
    216216
    217217(** val arg_decision_rect_Type0 :
     
    219219    arg_decision -> 'a1 **)
    220220let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    221 | Arg_decision_colour x_44 -> h_arg_decision_colour x_44
    222 | Arg_decision_spill x_45 -> h_arg_decision_spill x_45
    223 | Arg_decision_imm x_46 -> h_arg_decision_imm x_46
     221| Arg_decision_colour x_19080 -> h_arg_decision_colour x_19080
     222| Arg_decision_spill x_19081 -> h_arg_decision_spill x_19081
     223| Arg_decision_imm x_19082 -> h_arg_decision_imm x_19082
    224224
    225225(** val arg_decision_inv_rect_Type4 :
  • extracted/fetch.ml

    r3068 r3080  
    143143    ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word **)
    144144let address_of_word_labels code_mem id =
    145 prerr_endline "ADDRESS_OF_WORD_LABELS";
    146145  let labels = (create_label_cost_map code_mem).Types.fst in
    147146  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  • extracted/interpret.ml

    r3069 r3080  
    4545open Div_and_mod
    4646
     47open Util
     48
     49open List
     50
     51open Lists
     52
     53open Bool
     54
     55open Relations
     56
     57open Nat
     58
     59open Positive
     60
     61open Identifiers
     62
     63open CostLabel
     64
     65open ASM
     66
     67open Types
     68
     69open Hints_declaration
     70
     71open Core_notation
     72
     73open Pts
     74
     75open Logic
     76
    4777open Jmeq
    4878
    4979open 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 Status
  • extracted/interpret.mli

    r3043 r3080  
    4545open Div_and_mod
    4646
    47 open Jmeq
    48 
    49 open Russell
    50 
    5147open Util
    5248
     
    6359open Positive
    6460
     61open Identifiers
     62
     63open CostLabel
     64
     65open ASM
     66
     67open Types
     68
    6569open Hints_declaration
    6670
     
    7175open Logic
    7276
    73 open Types
     77open Jmeq
    7478
    75 open Identifiers
    76 
    77 open CostLabel
    78 
    79 open ASM
     79open Russell
    8080
    8181open Status
  • extracted/interpret2.ml

    r3065 r3080  
    7575open Div_and_mod
    7676
     77open Util
     78
     79open List
     80
     81open Lists
     82
     83open Bool
     84
     85open Relations
     86
     87open Nat
     88
     89open Positive
     90
     91open Identifiers
     92
     93open CostLabel
     94
     95open ASM
     96
     97open Types
     98
     99open Hints_declaration
     100
     101open Core_notation
     102
     103open Pts
     104
     105open Logic
     106
    77107open Jmeq
    78108
    79109open Russell
    80 
    81 open Util
    82 
    83 open List
    84 
    85 open Lists
    86 
    87 open Bool
    88 
    89 open Relations
    90 
    91 open Nat
    92 
    93 open Positive
    94 
    95 open Hints_declaration
    96 
    97 open Core_notation
    98 
    99 open Pts
    100 
    101 open Logic
    102 
    103 open Types
    104 
    105 open Identifiers
    106 
    107 open CostLabel
    108 
    109 open ASM
    110110
    111111open Status
  • extracted/interpret2.mli

    r3064 r3080  
    7575open Div_and_mod
    7676
    77 open Jmeq
    78 
    79 open Russell
    80 
    8177open Util
    8278
     
    9389open Positive
    9490
     91open Identifiers
     92
     93open CostLabel
     94
     95open ASM
     96
     97open Types
     98
    9599open Hints_declaration
    96100
     
    101105open Logic
    102106
    103 open Types
     107open Jmeq
    104108
    105 open Identifiers
    106 
    107 open CostLabel
    108 
    109 open ASM
     109open Russell
    110110
    111111open Status
  • extracted/lINToASM.ml

    r3069 r3080  
    140140    Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    141141    Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
    142 let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_588 =
     142let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_21483 =
    143143  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    144144    ident_map0; label_map = label_map0; fresh_cost_label =
    145     fresh_cost_label0 } = x_588
     145    fresh_cost_label0 } = x_21483
    146146  in
    147147  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    152152    Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    153153    Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
    154 let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_590 =
     154let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_21485 =
    155155  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    156156    ident_map0; label_map = label_map0; fresh_cost_label =
    157     fresh_cost_label0 } = x_590
     157    fresh_cost_label0 } = x_21485
    158158  in
    159159  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    164164    Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    165165    Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
    166 let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_592 =
     166let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_21487 =
    167167  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    168168    ident_map0; label_map = label_map0; fresh_cost_label =
    169     fresh_cost_label0 } = x_592
     169    fresh_cost_label0 } = x_21487
    170170  in
    171171  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    176176    Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    177177    Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
    178 let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_594 =
     178let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_21489 =
    179179  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    180180    ident_map0; label_map = label_map0; fresh_cost_label =
    181     fresh_cost_label0 } = x_594
     181    fresh_cost_label0 } = x_21489
    182182  in
    183183  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    188188    Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    189189    Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
    190 let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_596 =
     190let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_21491 =
    191191  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    192192    ident_map0; label_map = label_map0; fresh_cost_label =
    193     fresh_cost_label0 } = x_596
     193    fresh_cost_label0 } = x_21491
    194194  in
    195195  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    200200    Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    201201    Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
    202 let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_598 =
     202let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_21493 =
    203203  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    204204    ident_map0; label_map = label_map0; fresh_cost_label =
    205     fresh_cost_label0 } = x_598
     205    fresh_cost_label0 } = x_21493
    206206  in
    207207  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    303303        (Identifiers.empty_map PreIdentifiers.LabelTag)
    304304    in
    305     let { Types.fst = eta154; Types.snd = lmap0 } =
     305    let { Types.fst = eta28616; Types.snd = lmap0 } =
    306306      match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
    307307      | Types.None ->
     
    315315          lmap }
    316316    in
    317     let { Types.fst = id; Types.snd = univ } = eta154 in
     317    let { Types.fst = id; Types.snd = univ } = eta28616 in
    318318    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
    319319    u.ident_map; label_map =
     
    10511051    ASM.labelled_instruction List.list List.list -> (ASM.identifier,
    10521052    BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
    1053 let rec init_mutable_rect_Type4 h_mk_init_mutable x_614 =
     1053let rec init_mutable_rect_Type4 h_mk_init_mutable x_21509 =
    10541054  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1055     built_code = built_code0; built_preamble = built_preamble0 } = x_614
     1055    built_code = built_code0; built_preamble = built_preamble0 } = x_21509
    10561056  in
    10571057  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
     
    10611061    ASM.labelled_instruction List.list List.list -> (ASM.identifier,
    10621062    BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
    1063 let rec init_mutable_rect_Type5 h_mk_init_mutable x_616 =
     1063let rec init_mutable_rect_Type5 h_mk_init_mutable x_21511 =
    10641064  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1065     built_code = built_code0; built_preamble = built_preamble0 } = x_616
     1065    built_code = built_code0; built_preamble = built_preamble0 } = x_21511
    10661066  in
    10671067  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
     
    10711071    ASM.labelled_instruction List.list List.list -> (ASM.identifier,
    10721072    BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
    1073 let rec init_mutable_rect_Type3 h_mk_init_mutable x_618 =
     1073let rec init_mutable_rect_Type3 h_mk_init_mutable x_21513 =
    10741074  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1075     built_code = built_code0; built_preamble = built_preamble0 } = x_618
     1075    built_code = built_code0; built_preamble = built_preamble0 } = x_21513
    10761076  in
    10771077  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
     
    10811081    ASM.labelled_instruction List.list List.list -> (ASM.identifier,
    10821082    BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
    1083 let rec init_mutable_rect_Type2 h_mk_init_mutable x_620 =
     1083let rec init_mutable_rect_Type2 h_mk_init_mutable x_21515 =
    10841084  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1085     built_code = built_code0; built_preamble = built_preamble0 } = x_620
     1085    built_code = built_code0; built_preamble = built_preamble0 } = x_21515
    10861086  in
    10871087  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
     
    10911091    ASM.labelled_instruction List.list List.list -> (ASM.identifier,
    10921092    BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
    1093 let rec init_mutable_rect_Type1 h_mk_init_mutable x_622 =
     1093let rec init_mutable_rect_Type1 h_mk_init_mutable x_21517 =
    10941094  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1095     built_code = built_code0; built_preamble = built_preamble0 } = x_622
     1095    built_code = built_code0; built_preamble = built_preamble0 } = x_21517
    10961096  in
    10971097  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
     
    11011101    ASM.labelled_instruction List.list List.list -> (ASM.identifier,
    11021102    BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
    1103 let rec init_mutable_rect_Type0 h_mk_init_mutable x_624 =
     1103let rec init_mutable_rect_Type0 h_mk_init_mutable x_21519 =
    11041104  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1105     built_code = built_code0; built_preamble = built_preamble0 } = x_624
     1105    built_code = built_code0; built_preamble = built_preamble0 } = x_21519
    11061106  in
    11071107  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
     
    13041304let do_store_global m_mut id_reg_data =
    13051305  Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut ->
    1306     let { Types.fst = eta171; Types.snd = data } = id_reg_data in
    1307     let { Types.fst = id; Types.snd = reg } = eta171 in
     1306    let { Types.fst = eta28633; Types.snd = data } = id_reg_data in
     1307    let { Types.fst = id; Types.snd = reg } = eta28633 in
    13081308    Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id)
    13091309      (fun id0 ->
  • extracted/semantics.ml

    r3059 r3080  
    434434| Compiler.Assembly_pass ->
    435435  (fun prog ->
    436     let { Types.fst = eta31925; Types.snd = policy } = Obj.magic prog in
    437     let { Types.fst = code; Types.snd = sigma } = eta31925 in
     436    let { Types.fst = eta32049; Types.snd = policy } = Obj.magic prog in
     437    let { Types.fst = code; Types.snd = sigma } = eta32049 in
    438438    Interpret2.aSM_preclassified_system code sigma policy)
    439439| Compiler.Object_code_pass ->
  • extracted/status.ml

    r3077 r3080  
    8989    serialBufferType -> 'a1 **)
    9090let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
    91 | Eight x_8 -> h_Eight x_8
    92 | Nine (x_10, x_9) -> h_Nine x_10 x_9
     91| Eight x_21722 -> h_Eight x_21722
     92| Nine (x_21724, x_21723) -> h_Nine x_21724 x_21723
    9393
    9494(** val serialBufferType_rect_Type5 :
     
    9696    serialBufferType -> 'a1 **)
    9797let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
    98 | Eight x_14 -> h_Eight x_14
    99 | Nine (x_16, x_15) -> h_Nine x_16 x_15
     98| Eight x_21728 -> h_Eight x_21728
     99| Nine (x_21730, x_21729) -> h_Nine x_21730 x_21729
    100100
    101101(** val serialBufferType_rect_Type3 :
     
    103103    serialBufferType -> 'a1 **)
    104104let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
    105 | Eight x_20 -> h_Eight x_20
    106 | Nine (x_22, x_21) -> h_Nine x_22 x_21
     105| Eight x_21734 -> h_Eight x_21734
     106| Nine (x_21736, x_21735) -> h_Nine x_21736 x_21735
    107107
    108108(** val serialBufferType_rect_Type2 :
     
    110110    serialBufferType -> 'a1 **)
    111111let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
    112 | Eight x_26 -> h_Eight x_26
    113 | Nine (x_28, x_27) -> h_Nine x_28 x_27
     112| Eight x_21740 -> h_Eight x_21740
     113| Nine (x_21742, x_21741) -> h_Nine x_21742 x_21741
    114114
    115115(** val serialBufferType_rect_Type1 :
     
    117117    serialBufferType -> 'a1 **)
    118118let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
    119 | Eight x_32 -> h_Eight x_32
    120 | Nine (x_34, x_33) -> h_Nine x_34 x_33
     119| Eight x_21746 -> h_Eight x_21746
     120| Nine (x_21748, x_21747) -> h_Nine x_21748 x_21747
    121121
    122122(** val serialBufferType_rect_Type0 :
     
    124124    serialBufferType -> 'a1 **)
    125125let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
    126 | Eight x_38 -> h_Eight x_38
    127 | Nine (x_40, x_39) -> h_Nine x_40 x_39
     126| Eight x_21752 -> h_Eight x_21752
     127| Nine (x_21754, x_21753) -> h_Nine x_21754 x_21753
    128128
    129129(** val serialBufferType_inv_rect_Type4 :
     
    182182    -> 'a1) -> lineType -> 'a1 **)
    183183let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
    184 | P1 x_87 -> h_P1 x_87
    185 | P3 x_88 -> h_P3 x_88
    186 | SerialBuffer x_89 -> h_SerialBuffer x_89
     184| P1 x_21801 -> h_P1 x_21801
     185| P3 x_21802 -> h_P3 x_21802
     186| SerialBuffer x_21803 -> h_SerialBuffer x_21803
    187187
    188188(** val lineType_rect_Type5 :
     
    190190    -> 'a1) -> lineType -> 'a1 **)
    191191let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
    192 | P1 x_94 -> h_P1 x_94
    193 | P3 x_95 -> h_P3 x_95
    194 | SerialBuffer x_96 -> h_SerialBuffer x_96
     192| P1 x_21808 -> h_P1 x_21808
     193| P3 x_21809 -> h_P3 x_21809
     194| SerialBuffer x_21810 -> h_SerialBuffer x_21810
    195195
    196196(** val lineType_rect_Type3 :
     
    198198    -> 'a1) -> lineType -> 'a1 **)
    199199let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
    200 | P1 x_101 -> h_P1 x_101
    201 | P3 x_102 -> h_P3 x_102
    202 | SerialBuffer x_103 -> h_SerialBuffer x_103
     200| P1 x_21815 -> h_P1 x_21815
     201| P3 x_21816 -> h_P3 x_21816
     202| SerialBuffer x_21817 -> h_SerialBuffer x_21817
    203203
    204204(** val lineType_rect_Type2 :
     
    206206    -> 'a1) -> lineType -> 'a1 **)
    207207let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
    208 | P1 x_108 -> h_P1 x_108
    209 | P3 x_109 -> h_P3 x_109
    210 | SerialBuffer x_110 -> h_SerialBuffer x_110
     208| P1 x_21822 -> h_P1 x_21822
     209| P3 x_21823 -> h_P3 x_21823
     210| SerialBuffer x_21824 -> h_SerialBuffer x_21824
    211211
    212212(** val lineType_rect_Type1 :
     
    214214    -> 'a1) -> lineType -> 'a1 **)
    215215let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
    216 | P1 x_115 -> h_P1 x_115
    217 | P3 x_116 -> h_P3 x_116
    218 | SerialBuffer x_117 -> h_SerialBuffer x_117
     216| P1 x_21829 -> h_P1 x_21829
     217| P3 x_21830 -> h_P3 x_21830
     218| SerialBuffer x_21831 -> h_SerialBuffer x_21831
    219219
    220220(** val lineType_rect_Type0 :
     
    222222    -> 'a1) -> lineType -> 'a1 **)
    223223let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
    224 | P1 x_122 -> h_P1 x_122
    225 | P3 x_123 -> h_P3 x_123
    226 | SerialBuffer x_124 -> h_SerialBuffer x_124
     224| P1 x_21836 -> h_P1 x_21836
     225| P3 x_21837 -> h_P3 x_21837
     226| SerialBuffer x_21838 -> h_SerialBuffer x_21838
    227227
    228228(** val lineType_inv_rect_Type4 :
     
    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_510 =
     733let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_22224 =
    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_510
     739    p3_latch0; clock = clock0 } = x_22224
    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_512 =
     751let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_22226 =
    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_512
     757    p3_latch0; clock = clock0 } = x_22226
    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_514 =
     769let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_22228 =
    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_514
     775    p3_latch0; clock = clock0 } = x_22228
    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_516 =
     787let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_22230 =
    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_516
     793    p3_latch0; clock = clock0 } = x_22230
    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_518 =
     805let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_22232 =
    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_518
     811    p3_latch0; clock = clock0 } = x_22232
    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_520 =
     823let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_22234 =
    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_520
     829    p3_latch0; clock = clock0 } = x_22234
    830830  in
    831831  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
  • extracted/statusProofs.ml

    r2773 r3080  
    4545open Div_and_mod
    4646
    47 open Jmeq
    48 
    49 open Russell
    50 
    5147open Util
    5248
     
    6359open Positive
    6460
     61open Identifiers
     62
     63open CostLabel
     64
     65open ASM
     66
     67open Types
     68
    6569open Hints_declaration
    6670
     
    7175open Logic
    7276
    73 open Types
     77open Jmeq
    7478
    75 open Identifiers
    76 
    77 open CostLabel
    78 
    79 open ASM
     79open Russell
    8080
    8181open Status
  • extracted/statusProofs.mli

    r2773 r3080  
    4545open Div_and_mod
    4646
    47 open Jmeq
    48 
    49 open Russell
    50 
    5147open Util
    5248
     
    6359open Positive
    6460
     61open Identifiers
     62
     63open CostLabel
     64
     65open ASM
     66
     67open Types
     68
    6569open Hints_declaration
    6670
     
    7175open Logic
    7276
    73 open Types
     77open Jmeq
    7478
    75 open Identifiers
    76 
    77 open CostLabel
    78 
    79 open ASM
     79open Russell
    8080
    8181open Status
Note: See TracChangeset for help on using the changeset viewer.