Changeset 3106


Ignore:
Timestamp:
Apr 6, 2013, 7:35:25 PM (4 years ago)
Author:
sacerdot
Message:

New extraction.

Location:
driver/extracted
Files:
24 edited

Legend:

Unmodified
Added
Removed
  • driver/extracted/aSMCosts.ml

    r3080 r3106  
    502502   | Nat.S program_size' ->
    503503     (fun _ ->
    504        (let { Types.fst = eta31588; Types.snd = ticks } =
     504       (let { Types.fst = eta302; Types.snd = ticks } =
    505505          Fetch.fetch prog.ASM.cm program_counter'
    506506        in
    507507       let { Types.fst = instruction; Types.snd = program_counter'' } =
    508          eta31588
     508         eta302
    509509       in
    510510       (fun _ ->
  • driver/extracted/abstractStatus.ml

    r2905 r3106  
    161161| ASM.RealInstruction pre -> aSM_classify00 pre
    162162
    163 (** val current_instruction0 :
    164     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
    165     ASM.instruction **)
    166 let current_instruction0 code_memory program_counter =
    167   (Fetch.fetch code_memory program_counter).Types.fst.Types.fst
    168 
    169163(** val current_instruction :
    170164    BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
    171165    ASM.instruction **)
    172166let current_instruction code_memory s =
    173   current_instruction0 code_memory s.Status.program_counter
     167  (Fetch.fetch code_memory s.Status.program_counter).Types.fst.Types.fst
    174168
    175169(** val current_instruction_label :
    176     BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    177     BitVectorTrie.bitVectorTrie -> Status.status -> CostLabel.costlabel
    178     Types.option **)
     170    BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map ->
     171    Status.status -> CostLabel.costlabel Types.option **)
    179172let current_instruction_label code_memory cost_labels s =
    180173  let pc = s.Status.program_counter in
  • driver/extracted/abstractStatus.mli

    r2905 r3106  
    113113val aSM_classify0 : ASM.instruction -> StructuredTraces.status_class
    114114
    115 val current_instruction0 :
    116   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
    117   ASM.instruction
    118 
    119115val current_instruction :
    120116  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
     
    122118
    123119val current_instruction_label :
    124   BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
    125   BitVectorTrie.bitVectorTrie -> Status.status -> CostLabel.costlabel
    126   Types.option
     120  BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map ->
     121  Status.status -> CostLabel.costlabel Types.option
    127122
    128123val word_deqset : Deqsets.deqSet
  • driver/extracted/compiler.ml

    r3083 r3106  
    531531    Errors.res **)
    532532let assembler observe p =
     533prerr_endline "Y1";
    533534  Obj.magic
    534535    (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    536537        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
    537538          (Policy.jump_expansion' p))) (fun sigma_pol ->
     539prerr_endline "Y2";
    538540      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
    539541      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
     
    542544          Types.snd = sigma }; Types.snd = pol }
    543545      in
     546prerr_endline "Y3";
    544547      let p0 = Assembly.assembly p sigma pol in
     548prerr_endline "Y4";
    545549      let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in
     550prerr_endline "Y5";
    546551      Obj.magic (Errors.OK (Types.pi1 p0))))
    547552
  • driver/extracted/compiler.mli

    r3083 r3106  
    323323  Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res
    324324
     325open Status
     326
     327open Fetch
     328
    325329open Assembly
    326 
    327 open Status
    328 
    329 open Fetch
    330330
    331331open PolicyFront
  • driver/extracted/fetch.ml

    r3080 r3106  
    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 Exp
    418
     
    1529open Div_and_mod
    1630
    17 open Jmeq
    18 
    19 open Russell
    20 
    21 open Types
    22 
    2331open List
    2432
     
    2937open Bool
    3038
    31 open Hints_declaration
    32 
    33 open Core_notation
    34 
    35 open Pts
    36 
    37 open Logic
    38 
    3939open Relations
    4040
     
    7979open ASM
    8080
    81 (** val inefficient_address_of_word_labels_code_mem :
    82     ASM.labelled_instruction List.list -> ASM.identifier ->
    83     BitVector.bitVector **)
    84 let inefficient_address_of_word_labels_code_mem code_mem id =
    85   Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    86     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    87     Nat.O))))))))))))))))
    88     (LabelledObjects.index_of
    89       (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag
    90         id) code_mem)
     81(** val inefficient_address_of_label :
     82    ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat **)
     83let inefficient_address_of_label instr_list id =
     84  LabelledObjects.index_of
     85    (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag id)
     86    instr_list
    9187
    9288type label_map = Nat.nat Identifiers.identifier_map
    9389
    9490(** val create_label_cost_map0 :
    95     ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
    96     BitVectorTrie.bitVectorTrie) Types.prod Types.sig0 **)
     91    ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
     92    Types.prod Types.sig0 **)
    9793let create_label_cost_map0 program =
    9894  (Types.pi1
    9995    (FoldStuff.foldl_strong program (fun prefix x tl _ labels_costs_ppc ->
    100       (let { Types.fst = eta28695; Types.snd = ppc } =
     96      (let { Types.fst = eta19; Types.snd = ppc } =
    10197         Types.pi1 labels_costs_ppc
    10298       in
    10399      (fun _ ->
    104       (let { Types.fst = labels; Types.snd = costs } = eta28695 in
     100      (let { Types.fst = labels; Types.snd = costs } = eta19 in
    105101      (fun _ ->
    106102      (let { Types.fst = label; Types.snd = instr } = x in
     
    135131
    136132(** val create_label_cost_map :
    137     ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
    138     BitVectorTrie.bitVectorTrie) Types.prod **)
     133    ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
     134    Types.prod **)
    139135let create_label_cost_map program =
    140136  Types.pi1 (create_label_cost_map0 program)
     
    142138(** val address_of_word_labels :
    143139    ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word **)
    144 let address_of_word_labels code_mem id =
    145   let labels = (create_label_cost_map code_mem).Types.fst in
     140let address_of_word_labels program id =
     141  let labels = (create_label_cost_map program).Types.fst in
     142  let address_of_label = fun l ->
     143    Identifiers.lookup_def PreIdentifiers.ASMTag labels l Nat.O
     144  in
    146145  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    147146    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    148     Nat.O))))))))))))))))
    149     (Identifiers.lookup_def PreIdentifiers.ASMTag labels id Nat.O)
    150 
    151 (** val bitvector_max_nat : Nat.nat -> Nat.nat **)
    152 let bitvector_max_nat length =
    153   Exp.exp (Nat.S (Nat.S Nat.O)) length
    154 
    155 (** val code_memory_size : Nat.nat **)
    156 let code_memory_size =
    157   bitvector_max_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    158     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    159     Nat.O))))))))))))))))
     147    Nat.O)))))))))))))))) (address_of_label id)
    160148
    161149(** val prod_inv_rect_Type0 :
  • driver/extracted/fetch.mli

    r2999 r3106  
    11open Preamble
     2
     3open Types
     4
     5open Hints_declaration
     6
     7open Core_notation
     8
     9open Pts
     10
     11open Logic
     12
     13open Jmeq
     14
     15open Russell
    216
    317open Exp
     
    1529open Div_and_mod
    1630
    17 open Jmeq
    18 
    19 open Russell
    20 
    21 open Types
    22 
    2331open List
    2432
     
    2836
    2937open Bool
    30 
    31 open Hints_declaration
    32 
    33 open Core_notation
    34 
    35 open Pts
    36 
    37 open Logic
    3838
    3939open Relations
     
    7979open ASM
    8080
    81 val inefficient_address_of_word_labels_code_mem :
    82   ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.bitVector
     81val inefficient_address_of_label :
     82  ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat
    8383
    8484type label_map = Nat.nat Identifiers.identifier_map
    8585
    8686val create_label_cost_map0 :
    87   ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
    88   BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
     87  ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
     88  Types.prod Types.sig0
    8989
    9090val create_label_cost_map :
    91   ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
    92   BitVectorTrie.bitVectorTrie) Types.prod
     91  ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
     92  Types.prod
    9393
    9494val address_of_word_labels :
    9595  ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word
    96 
    97 val bitvector_max_nat : Nat.nat -> Nat.nat
    98 
    99 val code_memory_size : Nat.nat
    10096
    10197val prod_inv_rect_Type0 :
  • driver/extracted/globalenvs.ml

    r3043 r3106  
    314314let add_globals extract_init init_env vars =
    315315  Util.foldl (fun g_st id_init ->
    316     let { Types.fst = eta1345; Types.snd = init_info } = id_init in
    317     let { Types.fst = id; Types.snd = r } = eta1345 in
     316    let { Types.fst = eta1367; Types.snd = init_info } = id_init in
     317    let { Types.fst = id; Types.snd = r } = eta1367 in
    318318    let init = extract_init init_info in
    319319    let { Types.fst = g; Types.snd = st } = g_st in
     
    330330let init_globals extract_init g m vars =
    331331  Util.foldl (fun st id_init ->
    332     let { Types.fst = eta1346; Types.snd = init_info } = id_init in
    333     let { Types.fst = id; Types.snd = r } = eta1346 in
     332    let { Types.fst = eta1368; Types.snd = init_info } = id_init in
     333    let { Types.fst = id; Types.snd = r } = eta1368 in
    334334    let init = extract_init init_info in
    335335    Obj.magic
  • driver/extracted/interpret2.ml

    r3080 r3106  
    468468        policy (Obj.magic st))) (Obj.magic (Status.initialise_status c))
    469469
     470(** val aSM_status :
     471    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     472    (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
     473let aSM_status c sigma policy =
     474  let label_map = (Fetch.create_label_cost_map c.ASM.code).Types.fst in
     475  let symbol_map = Status.construct_datalabels c.ASM.preamble in
     476  let addr_of_label = fun x ->
     477    Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     478      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     479      Nat.O))))))))))))))))
     480      (Identifiers.lookup_def PreIdentifiers.ASMTag label_map x Nat.O)
     481  in
     482  let addr_of_symbol = fun x ->
     483    Identifiers.lookup_def PreIdentifiers.ASMTag symbol_map x
     484      (addr_of_label x)
     485  in
     486  aSM_abstract_status c addr_of_label addr_of_symbol sigma policy
     487
  • driver/extracted/interpret2.mli

    r3080 r3106  
    179179  (BitVector.word -> Bool.bool) -> Measurable.preclassified_system
    180180
     181val aSM_status :
     182  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     183  (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status
     184
  • driver/extracted/joint_printer.ml

    r3043 r3106  
    433433    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
    434434    printing_pass_independent_params -> 'a2 **)
    435 let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_263 =
     435let rec printing_pass_independent_params_rect_Type4 h_mk_printing_pass_independent_params x_25506 =
    436436  let { print_String = print_String0; print_keyword = print_keyword0;
    437437    print_concat = print_concat0; print_empty = print_empty0; print_ident =
     
    439439    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    440440    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
    441     print_bitvector0 } = x_263
     441    print_bitvector0 } = x_25506
    442442  in
    443443  h_mk_printing_pass_independent_params print_String0 print_keyword0
     
    452452    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
    453453    printing_pass_independent_params -> 'a2 **)
    454 let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_265 =
     454let rec printing_pass_independent_params_rect_Type5 h_mk_printing_pass_independent_params x_25508 =
    455455  let { print_String = print_String0; print_keyword = print_keyword0;
    456456    print_concat = print_concat0; print_empty = print_empty0; print_ident =
     
    458458    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    459459    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
    460     print_bitvector0 } = x_265
     460    print_bitvector0 } = x_25508
    461461  in
    462462  h_mk_printing_pass_independent_params print_String0 print_keyword0
     
    471471    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
    472472    printing_pass_independent_params -> 'a2 **)
    473 let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_267 =
     473let rec printing_pass_independent_params_rect_Type3 h_mk_printing_pass_independent_params x_25510 =
    474474  let { print_String = print_String0; print_keyword = print_keyword0;
    475475    print_concat = print_concat0; print_empty = print_empty0; print_ident =
     
    477477    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    478478    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
    479     print_bitvector0 } = x_267
     479    print_bitvector0 } = x_25510
    480480  in
    481481  h_mk_printing_pass_independent_params print_String0 print_keyword0
     
    490490    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
    491491    printing_pass_independent_params -> 'a2 **)
    492 let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_269 =
     492let rec printing_pass_independent_params_rect_Type2 h_mk_printing_pass_independent_params x_25512 =
    493493  let { print_String = print_String0; print_keyword = print_keyword0;
    494494    print_concat = print_concat0; print_empty = print_empty0; print_ident =
     
    496496    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    497497    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
    498     print_bitvector0 } = x_269
     498    print_bitvector0 } = x_25512
    499499  in
    500500  h_mk_printing_pass_independent_params print_String0 print_keyword0
     
    509509    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
    510510    printing_pass_independent_params -> 'a2 **)
    511 let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_271 =
     511let rec printing_pass_independent_params_rect_Type1 h_mk_printing_pass_independent_params x_25514 =
    512512  let { print_String = print_String0; print_keyword = print_keyword0;
    513513    print_concat = print_concat0; print_empty = print_empty0; print_ident =
     
    515515    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    516516    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
    517     print_bitvector0 } = x_271
     517    print_bitvector0 } = x_25514
    518518  in
    519519  h_mk_printing_pass_independent_params print_String0 print_keyword0
     
    528528    BitVector.bitVector -> 'a1) -> 'a2) -> 'a1
    529529    printing_pass_independent_params -> 'a2 **)
    530 let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_273 =
     530let rec printing_pass_independent_params_rect_Type0 h_mk_printing_pass_independent_params x_25516 =
    531531  let { print_String = print_String0; print_keyword = print_keyword0;
    532532    print_concat = print_concat0; print_empty = print_empty0; print_ident =
     
    534534    print_label0; print_OpAccs = print_OpAccs0; print_Op1 = print_Op3;
    535535    print_Op2 = print_Op4; print_nat = print_nat0; print_bitvector =
    536     print_bitvector0 } = x_273
     536    print_bitvector0 } = x_25516
    537537  in
    538538  h_mk_printing_pass_independent_params print_String0 print_keyword0
     
    684684    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    685685    printing_params -> 'a2 **)
    686 let rec printing_params_rect_Type4 p h_mk_printing_params x_301 =
     686let rec printing_params_rect_Type4 p h_mk_printing_params x_25544 =
    687687  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    688688    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    692692    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    693693    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    694     x_301
     694    x_25544
    695695  in
    696696  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    705705    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    706706    printing_params -> 'a2 **)
    707 let rec printing_params_rect_Type5 p h_mk_printing_params x_303 =
     707let rec printing_params_rect_Type5 p h_mk_printing_params x_25546 =
    708708  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    709709    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    713713    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    714714    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    715     x_303
     715    x_25546
    716716  in
    717717  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    726726    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    727727    printing_params -> 'a2 **)
    728 let rec printing_params_rect_Type3 p h_mk_printing_params x_305 =
     728let rec printing_params_rect_Type3 p h_mk_printing_params x_25548 =
    729729  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    730730    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    734734    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    735735    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    736     x_305
     736    x_25548
    737737  in
    738738  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    747747    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    748748    printing_params -> 'a2 **)
    749 let rec printing_params_rect_Type2 p h_mk_printing_params x_307 =
     749let rec printing_params_rect_Type2 p h_mk_printing_params x_25550 =
    750750  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    751751    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    755755    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    756756    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    757     x_307
     757    x_25550
    758758  in
    759759  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    768768    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    769769    printing_params -> 'a2 **)
    770 let rec printing_params_rect_Type1 p h_mk_printing_params x_309 =
     770let rec printing_params_rect_Type1 p h_mk_printing_params x_25552 =
    771771  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    772772    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    776776    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    777777    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    778     x_309
     778    x_25552
    779779  in
    780780  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    789789    -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    790790    printing_params -> 'a2 **)
    791 let rec printing_params_rect_Type0 p h_mk_printing_params x_311 =
     791let rec printing_params_rect_Type0 p h_mk_printing_params x_25554 =
    792792  let { print_pass_ind = print_pass_ind0; print_acc_a_reg = print_acc_a_reg0;
    793793    print_acc_b_reg = print_acc_b_reg0; print_acc_a_arg = print_acc_a_arg0;
     
    797797    print_pair_move = print_pair_move0; print_call_args = print_call_args0;
    798798    print_call_dest = print_call_dest0; print_ext_seq = print_ext_seq0 } =
    799     x_311
     799    x_25554
    800800  in
    801801  h_mk_printing_params print_pass_ind0 print_acc_a_reg0 print_acc_b_reg0
     
    970970    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    971971    print_serialization_params -> 'a2 **)
    972 let rec print_serialization_params_rect_Type4 p h_mk_print_serialization_params x_340 =
     972let rec print_serialization_params_rect_Type4 p h_mk_print_serialization_params x_25583 =
    973973  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
    974     x_340
     974    x_25583
    975975  in
    976976  h_mk_print_serialization_params print_succ0 print_code_point0
     
    979979    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    980980    print_serialization_params -> 'a2 **)
    981 let rec print_serialization_params_rect_Type5 p h_mk_print_serialization_params x_342 =
     981let rec print_serialization_params_rect_Type5 p h_mk_print_serialization_params x_25585 =
    982982  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
    983     x_342
     983    x_25585
    984984  in
    985985  h_mk_print_serialization_params print_succ0 print_code_point0
     
    988988    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    989989    print_serialization_params -> 'a2 **)
    990 let rec print_serialization_params_rect_Type3 p h_mk_print_serialization_params x_344 =
     990let rec print_serialization_params_rect_Type3 p h_mk_print_serialization_params x_25587 =
    991991  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
    992     x_344
     992    x_25587
    993993  in
    994994  h_mk_print_serialization_params print_succ0 print_code_point0
     
    997997    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    998998    print_serialization_params -> 'a2 **)
    999 let rec print_serialization_params_rect_Type2 p h_mk_print_serialization_params x_346 =
     999let rec print_serialization_params_rect_Type2 p h_mk_print_serialization_params x_25589 =
    10001000  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
    1001     x_346
     1001    x_25589
    10021002  in
    10031003  h_mk_print_serialization_params print_succ0 print_code_point0
     
    10061006    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    10071007    print_serialization_params -> 'a2 **)
    1008 let rec print_serialization_params_rect_Type1 p h_mk_print_serialization_params x_348 =
     1008let rec print_serialization_params_rect_Type1 p h_mk_print_serialization_params x_25591 =
    10091009  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
    1010     x_348
     1010    x_25591
    10111011  in
    10121012  h_mk_print_serialization_params print_succ0 print_code_point0
     
    10151015    Joint.params -> ((__ -> 'a1) -> (__ -> 'a1) -> 'a2) -> 'a1
    10161016    print_serialization_params -> 'a2 **)
    1017 let rec print_serialization_params_rect_Type0 p h_mk_print_serialization_params x_350 =
     1017let rec print_serialization_params_rect_Type0 p h_mk_print_serialization_params x_25593 =
    10181018  let { print_succ = print_succ0; print_code_point = print_code_point0 } =
    1019     x_350
     1019    x_25593
    10201020  in
    10211021  h_mk_print_serialization_params print_succ0 print_code_point0
     
    10951095    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
    10961096    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
    1097 let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_368 =
     1097let rec code_iteration_params_rect_Type4 p globals h_mk_code_iteration_params x_25611 =
    10981098  let { cip_print_serialization_params = cip_print_serialization_params0;
    1099     fold_code = fold_code0; print_statementT = print_statementT0 } = x_368
     1099    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25611
    11001100  in
    11011101  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     
    11061106    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
    11071107    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
    1108 let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_370 =
     1108let rec code_iteration_params_rect_Type5 p globals h_mk_code_iteration_params x_25613 =
    11091109  let { cip_print_serialization_params = cip_print_serialization_params0;
    1110     fold_code = fold_code0; print_statementT = print_statementT0 } = x_370
     1110    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25613
    11111111  in
    11121112  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     
    11171117    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
    11181118    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
    1119 let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_372 =
     1119let rec code_iteration_params_rect_Type3 p globals h_mk_code_iteration_params x_25615 =
    11201120  let { cip_print_serialization_params = cip_print_serialization_params0;
    1121     fold_code = fold_code0; print_statementT = print_statementT0 } = x_372
     1121    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25615
    11221122  in
    11231123  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     
    11281128    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
    11291129    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
    1130 let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_374 =
     1130let rec code_iteration_params_rect_Type2 p globals h_mk_code_iteration_params x_25617 =
    11311131  let { cip_print_serialization_params = cip_print_serialization_params0;
    1132     fold_code = fold_code0; print_statementT = print_statementT0 } = x_374
     1132    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25617
    11331133  in
    11341134  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     
    11391139    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
    11401140    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
    1141 let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_376 =
     1141let rec code_iteration_params_rect_Type1 p globals h_mk_code_iteration_params x_25619 =
    11421142  let { cip_print_serialization_params = cip_print_serialization_params0;
    1143     fold_code = fold_code0; print_statementT = print_statementT0 } = x_376
     1143    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25619
    11441144  in
    11451145  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     
    11501150    (__ -> (__ -> 'a2 -> __ -> __) -> __ -> __ -> __ -> __) -> ('a2 -> 'a1)
    11511151    -> 'a3) -> ('a1, 'a2) code_iteration_params -> 'a3 **)
    1152 let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_378 =
     1152let rec code_iteration_params_rect_Type0 p globals h_mk_code_iteration_params x_25621 =
    11531153  let { cip_print_serialization_params = cip_print_serialization_params0;
    1154     fold_code = fold_code0; print_statementT = print_statementT0 } = x_378
     1154    fold_code = fold_code0; print_statementT = print_statementT0 } = x_25621
    11551155  in
    11561156  h_mk_code_iteration_params cip_print_serialization_params0 fold_code0
     
    11661166    Joint.params -> AST.ident List.list -> ('a1, 'a2) code_iteration_params
    11671167    -> (__ -> 'a2 -> 'a3 -> 'a3) -> __ -> __ -> 'a3 -> 'a3 **)
    1168 let rec fold_code0 p globals xxx x_393 x_394 x_395 x_396 =
     1168let rec fold_code0 p globals xxx x_25636 x_25637 x_25638 x_25639 =
    11691169  (let { cip_print_serialization_params = x; fold_code = yyy;
    11701170     print_statementT = x0 } = xxx
    11711171   in
    1172   Obj.magic yyy) __ x_393 x_394 x_395 x_396
     1172  Obj.magic yyy) __ x_25636 x_25637 x_25638 x_25639
    11731173
    11741174(** val print_statementT :
     
    12471247   | Types.None -> b
    12481248   | Types.Some res ->
    1249      let { Types.fst = eta2; Types.snd = m' } = res in
    1250      let { Types.fst = pos; Types.snd = a } = eta2 in
     1249     let { Types.fst = eta32074; Types.snd = m' } = res in
     1250     let { Types.fst = pos; Types.snd = a } = eta32074 in
    12511251     visit_graph next f (f pos a b) (next a) m' y)
    12521252
  • driver/extracted/lINToASM.ml

    r3080 r3106  
    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_21483 =
     142let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_588 =
    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_21483
     145    fresh_cost_label0 } = x_588
    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_21485 =
     154let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_590 =
    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_21485
     157    fresh_cost_label0 } = x_590
    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_21487 =
     166let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_592 =
    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_21487
     169    fresh_cost_label0 } = x_592
    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_21489 =
     178let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_594 =
    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_21489
     181    fresh_cost_label0 } = x_594
    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_21491 =
     190let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_596 =
    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_21491
     193    fresh_cost_label0 } = x_596
    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_21493 =
     202let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_598 =
    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_21493
     205    fresh_cost_label0 } = x_598
    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 = eta28616; Types.snd = lmap0 } =
     305    let { Types.fst = eta2825; 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 } = eta28616 in
     317    let { Types.fst = id; Types.snd = univ } = eta2825 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_21509 =
     1053let rec init_mutable_rect_Type4 h_mk_init_mutable x_614 =
    10541054  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1055     built_code = built_code0; built_preamble = built_preamble0 } = x_21509
     1055    built_code = built_code0; built_preamble = built_preamble0 } = x_614
    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_21511 =
     1063let rec init_mutable_rect_Type5 h_mk_init_mutable x_616 =
    10641064  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1065     built_code = built_code0; built_preamble = built_preamble0 } = x_21511
     1065    built_code = built_code0; built_preamble = built_preamble0 } = x_616
    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_21513 =
     1073let rec init_mutable_rect_Type3 h_mk_init_mutable x_618 =
    10741074  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1075     built_code = built_code0; built_preamble = built_preamble0 } = x_21513
     1075    built_code = built_code0; built_preamble = built_preamble0 } = x_618
    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_21515 =
     1083let rec init_mutable_rect_Type2 h_mk_init_mutable x_620 =
    10841084  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1085     built_code = built_code0; built_preamble = built_preamble0 } = x_21515
     1085    built_code = built_code0; built_preamble = built_preamble0 } = x_620
    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_21517 =
     1093let rec init_mutable_rect_Type1 h_mk_init_mutable x_622 =
    10941094  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1095     built_code = built_code0; built_preamble = built_preamble0 } = x_21517
     1095    built_code = built_code0; built_preamble = built_preamble0 } = x_622
    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_21519 =
     1103let rec init_mutable_rect_Type0 h_mk_init_mutable x_624 =
    11041104  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1105     built_code = built_code0; built_preamble = built_preamble0 } = x_21519
     1105    built_code = built_code0; built_preamble = built_preamble0 } = x_624
    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 = eta28633; Types.snd = data } = id_reg_data in
    1307     let { Types.fst = id; Types.snd = reg } = eta28633 in
     1306    let { Types.fst = eta2842; Types.snd = data } = id_reg_data in
     1307    let { Types.fst = id; Types.snd = reg } = eta2842 in
    13081308    Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id)
    13091309      (fun id0 ->
  • driver/extracted/policy.mli

    r2773 r3106  
    11open Preamble
    22
    3 open Assembly
    4 
    53open Status
    6 
    7 open Fetch
    84
    95open BitVectorTrie
    106
    117open String
    12 
    13 open Exp
    14 
    15 open Arithmetic
    16 
    17 open Vector
    18 
    19 open FoldStuff
    20 
    21 open BitVector
    22 
    23 open Extranat
    248
    259open Integers
     
    4125open Errors
    4226
    43 open Extralib
     27open Lists
     28
     29open Positive
     30
     31open Identifiers
     32
     33open CostLabel
     34
     35open ASM
     36
     37open Exp
    4438
    4539open Setoids
     
    4842
    4943open Option
     44
     45open Extranat
     46
     47open Vector
     48
     49open FoldStuff
     50
     51open BitVector
     52
     53open Arithmetic
     54
     55open Fetch
     56
     57open Assembly
    5058
    5159open Div_and_mod
     
    5765open Util
    5866
    59 open List
    60 
    61 open Lists
    62 
    6367open Bool
    6468
     
    6771open Nat
    6872
    69 open Positive
     73open List
    7074
    7175open Hints_declaration
     
    7983open Types
    8084
    81 open Identifiers
    82 
    83 open CostLabel
    84 
    85 open ASM
     85open Extralib
    8686
    8787open PolicyFront
  • driver/extracted/policyFront.ml

    r3098 r3106  
    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
     31open Status
     32
    333open BitVectorTrie
    434
    535open String
    636
     37open Integers
     38
     39open AST
     40
     41open LabelledObjects
     42
     43open Proper
     44
     45open PositiveMap
     46
     47open Deqsets
     48
     49open ErrorMessages
     50
     51open PreIdentifiers
     52
     53open Errors
     54
     55open Lists
     56
     57open Positive
     58
     59open Identifiers
     60
     61open CostLabel
     62
     63open ASM
     64
    765open Exp
    866
     67open Setoids
     68
     69open Monad
     70
     71open Option
     72
     73open Extranat
     74
     75open Vector
     76
     77open FoldStuff
     78
     79open BitVector
     80
    981open Arithmetic
    1082
    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
    80 
    8183open Fetch
    82 
    83 open Status
    8484
    8585open Assembly
  • driver/extracted/policyFront.mli

    r2773 r3106  
    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
     30
     31open Status
    232
    333open BitVectorTrie
    434
    535open 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
    1836
    1937open Integers
     
    3553open Errors
    3654
    37 open Extralib
     55open Lists
     56
     57open Positive
     58
     59open Identifiers
     60
     61open CostLabel
     62
     63open ASM
     64
     65open Exp
    3866
    3967open Setoids
     
    4371open Option
    4472
    45 open Div_and_mod
     73open Extranat
    4674
    47 open Jmeq
     75open Vector
    4876
    49 open Russell
     77open FoldStuff
    5078
    51 open Util
     79open BitVector
    5280
    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
     81open Arithmetic
    8082
    8183open Fetch
    82 
    83 open Status
    8484
    8585open Assembly
  • driver/extracted/policyStep.ml

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

    r2773 r3106  
    11open Preamble
    22
    3 open Assembly
    4 
    53open Status
    6 
    7 open Fetch
    84
    95open BitVectorTrie
    106
    117open String
    12 
    13 open Exp
    14 
    15 open Arithmetic
    16 
    17 open Vector
    18 
    19 open FoldStuff
    20 
    21 open BitVector
    22 
    23 open Extranat
    248
    259open Integers
     
    4125open Errors
    4226
    43 open Extralib
     27open Lists
     28
     29open Positive
     30
     31open Identifiers
     32
     33open CostLabel
     34
     35open ASM
     36
     37open Exp
    4438
    4539open Setoids
     
    4842
    4943open Option
     44
     45open Extranat
     46
     47open Vector
     48
     49open FoldStuff
     50
     51open BitVector
     52
     53open Arithmetic
     54
     55open Fetch
     56
     57open Assembly
    5058
    5159open Div_and_mod
     
    5765open Util
    5866
    59 open List
    60 
    61 open Lists
    62 
    6367open Bool
    6468
     
    6771open Nat
    6872
    69 open Positive
     73open List
    7074
    7175open Hints_declaration
     
    7983open Types
    8084
    81 open Identifiers
    82 
    83 open CostLabel
    84 
    85 open ASM
     85open Extralib
    8686
    8787open PolicyFront
  • driver/extracted/semantics.ml

    r3080 r3106  
    1515open ASMCosts
    1616
     17open Status
     18
     19open Fetch
     20
    1721open Assembly
    18 
    19 open Status
    20 
    21 open Fetch
    2222
    2323open PolicyFront
     
    316316    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    317317    preclassified_system_pass -> 'a1 **)
    318 let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_25220 =
    319   let pcs_pcs = x_25220 in h_mk_preclassified_system_pass pcs_pcs __
     318let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_3 =
     319  let pcs_pcs = x_3 in h_mk_preclassified_system_pass pcs_pcs __
    320320
    321321(** val preclassified_system_pass_rect_Type5 :
    322322    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    323323    preclassified_system_pass -> 'a1 **)
    324 let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_25222 =
    325   let pcs_pcs = x_25222 in h_mk_preclassified_system_pass pcs_pcs __
     324let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_5 =
     325  let pcs_pcs = x_5 in h_mk_preclassified_system_pass pcs_pcs __
    326326
    327327(** val preclassified_system_pass_rect_Type3 :
    328328    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    329329    preclassified_system_pass -> 'a1 **)
    330 let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_25224 =
    331   let pcs_pcs = x_25224 in h_mk_preclassified_system_pass pcs_pcs __
     330let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_7 =
     331  let pcs_pcs = x_7 in h_mk_preclassified_system_pass pcs_pcs __
    332332
    333333(** val preclassified_system_pass_rect_Type2 :
    334334    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    335335    preclassified_system_pass -> 'a1 **)
    336 let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_25226 =
    337   let pcs_pcs = x_25226 in h_mk_preclassified_system_pass pcs_pcs __
     336let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_9 =
     337  let pcs_pcs = x_9 in h_mk_preclassified_system_pass pcs_pcs __
    338338
    339339(** val preclassified_system_pass_rect_Type1 :
    340340    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    341341    preclassified_system_pass -> 'a1 **)
    342 let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_25228 =
    343   let pcs_pcs = x_25228 in h_mk_preclassified_system_pass pcs_pcs __
     342let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_11 =
     343  let pcs_pcs = x_11 in h_mk_preclassified_system_pass pcs_pcs __
    344344
    345345(** val preclassified_system_pass_rect_Type0 :
    346346    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    347347    preclassified_system_pass -> 'a1 **)
    348 let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_25230 =
    349   let pcs_pcs = x_25230 in h_mk_preclassified_system_pass pcs_pcs __
     348let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_13 =
     349  let pcs_pcs = x_13 in h_mk_preclassified_system_pass pcs_pcs __
    350350
    351351(** val pcs_pcs :
     
    434434| Compiler.Assembly_pass ->
    435435  (fun prog ->
    436     let { Types.fst = eta32049; Types.snd = policy } = Obj.magic prog in
    437     let { Types.fst = code; Types.snd = sigma } = eta32049 in
     436    let { Types.fst = eta4; Types.snd = policy } = Obj.magic prog in
     437    let { Types.fst = code; Types.snd = sigma } = eta4 in
    438438    Interpret2.aSM_preclassified_system code sigma policy)
    439439| Compiler.Object_code_pass ->
  • driver/extracted/semantics.mli

    r3059 r3106  
    1515open ASMCosts
    1616
     17open Status
     18
     19open Fetch
     20
    1721open Assembly
    18 
    19 open Status
    20 
    21 open Fetch
    2222
    2323open PolicyFront
  • driver/extracted/simplifyCasts.ml

    r3059 r3106  
    357357                       (Csyntax.typeof rhs) with
    358358               | Errors.OK _ ->
    359                  (let eta2011 = simplify_expr lhs target_sz target_sg in
     359                 (let eta2033 = simplify_expr lhs target_sz target_sg in
    360360                   (fun _ ->
    361361                   (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
    362                       eta2011
     362                      eta2033
    363363                    in
    364364                   (fun _ ->
    365                    (let eta2010 = simplify_expr rhs target_sz target_sg in
     365                   (let eta2032 = simplify_expr rhs target_sz target_sg in
    366366                     (fun _ ->
    367367                     (let { Types.fst = desired_type_rhs; Types.snd =
    368                         rhs1 } = eta2010
     368                        rhs1 } = eta2032
    369369                      in
    370370                     (fun _ ->
     
    419419               | Bool.True ->
    420420                 (fun _ ->
    421                    (let eta2013 = simplify_expr castee target_sz target_sg in
     421                   (let eta2035 = simplify_expr castee target_sz target_sg in
    422422                     (fun _ ->
    423423                     (let { Types.fst = desired_type; Types.snd = castee1 } =
    424                         eta2013
     424                        eta2035
    425425                      in
    426426                     (fun _ ->
     
    431431                      | Bool.False ->
    432432                        (fun _ ->
    433                           (let eta2012 = simplify_expr castee cast_sz cast_sg
     433                          (let eta2034 = simplify_expr castee cast_sz cast_sg
    434434                           in
    435435                            (fun _ ->
    436436                            (let { Types.fst = desired_type2; Types.snd =
    437                                castee2 } = eta2012
     437                               castee2 } = eta2034
    438438                             in
    439439                            (fun _ ->
     
    449449               | Bool.False ->
    450450                 (fun _ ->
    451                    (let eta2014 = simplify_expr castee cast_sz cast_sg in
     451                   (let eta2036 = simplify_expr castee cast_sz cast_sg in
    452452                     (fun _ ->
    453453                     (let { Types.fst = desired_type2; Types.snd =
    454                         castee2 } = eta2014
     454                        castee2 } = eta2036
    455455                      in
    456456                     (fun _ ->
     
    506506                    (Csyntax.typeof iffalse) with
    507507            | Errors.OK _ ->
    508               (let eta2016 = simplify_expr iftrue target_sz target_sg in
     508              (let eta2038 = simplify_expr iftrue target_sz target_sg in
    509509                (fun _ ->
    510510                (let { Types.fst = desired_true; Types.snd = iftrue1 } =
    511                    eta2016
     511                   eta2038
    512512                 in
    513513                (fun _ ->
    514                 (let eta2015 = simplify_expr iffalse target_sz target_sg in
     514                (let eta2037 = simplify_expr iffalse target_sz target_sg in
    515515                  (fun _ ->
    516516                  (let { Types.fst = desired_false; Types.snd = iffalse1 } =
    517                      eta2015
     517                     eta2037
    518518                   in
    519519                  (fun _ ->
     
    573573       match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with
    574574       | Types.Inl _ ->
    575          (let eta2017 = simplify_expr e1 target_sz target_sg in
     575         (let eta2039 = simplify_expr e1 target_sz target_sg in
    576576           (fun _ ->
    577            (let { Types.fst = desired_type; Types.snd = e2 } = eta2017 in
     577           (let { Types.fst = desired_type; Types.snd = e2 } = eta2039 in
    578578           (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
    579579           ((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __
     
    616616          | Csyntax.Tint (cast_sz, cast_sg) ->
    617617            (fun _ ->
    618               (let eta2018 = simplify_expr castee cast_sz cast_sg in
     618              (let eta2040 = simplify_expr castee cast_sz cast_sg in
    619619                (fun _ ->
    620                 (let { Types.fst = success; Types.snd = castee1 } = eta2018
     620                (let { Types.fst = success; Types.snd = castee1 } = eta2040
    621621                 in
    622622                (fun _ ->
  • driver/extracted/status.ml

    r3080 r3106  
    8989    serialBufferType -> 'a1 **)
    9090let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
    91 | Eight x_21722 -> h_Eight x_21722
    92 | Nine (x_21724, x_21723) -> h_Nine x_21724 x_21723
     91| Eight x_8 -> h_Eight x_8
     92| Nine (x_10, x_9) -> h_Nine x_10 x_9
    9393
    9494(** val serialBufferType_rect_Type5 :
     
    9696    serialBufferType -> 'a1 **)
    9797let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
    98 | Eight x_21728 -> h_Eight x_21728
    99 | Nine (x_21730, x_21729) -> h_Nine x_21730 x_21729
     98| Eight x_14 -> h_Eight x_14
     99| Nine (x_16, x_15) -> h_Nine x_16 x_15
    100100
    101101(** val serialBufferType_rect_Type3 :
     
    103103    serialBufferType -> 'a1 **)
    104104let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
    105 | Eight x_21734 -> h_Eight x_21734
    106 | Nine (x_21736, x_21735) -> h_Nine x_21736 x_21735
     105| Eight x_20 -> h_Eight x_20
     106| Nine (x_22, x_21) -> h_Nine x_22 x_21
    107107
    108108(** val serialBufferType_rect_Type2 :
     
    110110    serialBufferType -> 'a1 **)
    111111let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
    112 | Eight x_21740 -> h_Eight x_21740
    113 | Nine (x_21742, x_21741) -> h_Nine x_21742 x_21741
     112| Eight x_26 -> h_Eight x_26
     113| Nine (x_28, x_27) -> h_Nine x_28 x_27
    114114
    115115(** val serialBufferType_rect_Type1 :
     
    117117    serialBufferType -> 'a1 **)
    118118let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
    119 | Eight x_21746 -> h_Eight x_21746
    120 | Nine (x_21748, x_21747) -> h_Nine x_21748 x_21747
     119| Eight x_32 -> h_Eight x_32
     120| Nine (x_34, x_33) -> h_Nine x_34 x_33
    121121
    122122(** val serialBufferType_rect_Type0 :
     
    124124    serialBufferType -> 'a1 **)
    125125let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
    126 | Eight x_21752 -> h_Eight x_21752
    127 | Nine (x_21754, x_21753) -> h_Nine x_21754 x_21753
     126| Eight x_38 -> h_Eight x_38
     127| Nine (x_40, x_39) -> h_Nine x_40 x_39
    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_21801 -> h_P1 x_21801
    185 | P3 x_21802 -> h_P3 x_21802
    186 | SerialBuffer x_21803 -> h_SerialBuffer x_21803
     184| P1 x_87 -> h_P1 x_87
     185| P3 x_88 -> h_P3 x_88
     186| SerialBuffer x_89 -> h_SerialBuffer x_89
    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_21808 -> h_P1 x_21808
    193 | P3 x_21809 -> h_P3 x_21809
    194 | SerialBuffer x_21810 -> h_SerialBuffer x_21810
     192| P1 x_94 -> h_P1 x_94
     193| P3 x_95 -> h_P3 x_95
     194| SerialBuffer x_96 -> h_SerialBuffer x_96
    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_21815 -> h_P1 x_21815
    201 | P3 x_21816 -> h_P3 x_21816
    202 | SerialBuffer x_21817 -> h_SerialBuffer x_21817
     200| P1 x_101 -> h_P1 x_101
     201| P3 x_102 -> h_P3 x_102
     202| SerialBuffer x_103 -> h_SerialBuffer x_103
    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_21822 -> h_P1 x_21822
    209 | P3 x_21823 -> h_P3 x_21823
    210 | SerialBuffer x_21824 -> h_SerialBuffer x_21824
     208| P1 x_108 -> h_P1 x_108
     209| P3 x_109 -> h_P3 x_109
     210| SerialBuffer x_110 -> h_SerialBuffer x_110
    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_21829 -> h_P1 x_21829
    217 | P3 x_21830 -> h_P3 x_21830
    218 | SerialBuffer x_21831 -> h_SerialBuffer x_21831
     216| P1 x_115 -> h_P1 x_115
     217| P3 x_116 -> h_P3 x_116
     218| SerialBuffer x_117 -> h_SerialBuffer x_117
    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_21836 -> h_P1 x_21836
    225 | P3 x_21837 -> h_P3 x_21837
    226 | SerialBuffer x_21838 -> h_SerialBuffer x_21838
     224| P1 x_122 -> h_P1 x_122
     225| P3 x_123 -> h_P3 x_123
     226| SerialBuffer x_124 -> h_SerialBuffer x_124
    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_22224 =
     733let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_510 =
    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_22224
     739    p3_latch0; clock = clock0 } = x_510
    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_22226 =
     751let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_512 =
    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_22226
     757    p3_latch0; clock = clock0 } = x_512
    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_22228 =
     769let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_514 =
    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_22228
     775    p3_latch0; clock = clock0 } = x_514
    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_22230 =
     787let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_516 =
    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_22230
     793    p3_latch0; clock = clock0 } = x_516
    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_22232 =
     805let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_518 =
    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_22232
     811    p3_latch0; clock = clock0 } = x_518
    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_22234 =
     823let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_520 =
    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_22234
     829    p3_latch0; clock = clock0 } = x_520
    830830  in
    831831  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
  • driver/extracted/switchRemoval.ml

    r3059 r3106  
    174174    lab }; Types.snd = u1 }
    175175  | Csyntax.LScase (sz, tag, st, other_cases) ->
    176     let { Types.fst = eta2108; Types.snd = u1 } =
     176    let { Types.fst = eta2130; Types.snd = u1 } =
    177177      produce_cond e other_cases u exit
    178178    in
    179     let { Types.fst = sub_statements; Types.snd = sub_label } = eta2108 in
     179    let { Types.fst = sub_statements; Types.snd = sub_label } = eta2130 in
    180180    let st' = convert_break_to_goto st exit in
    181181    let { Types.fst = lab; Types.snd = u2 } =
     
    199199    Identifiers.fresh PreIdentifiers.SymbolTag uv
    200200  in
    201   let { Types.fst = eta2109; Types.snd = uv2 } =
     201  let { Types.fst = eta2131; Types.snd = uv2 } =
    202202    produce_cond e switch_cases uv1 exit_label
    203203  in
    204   let { Types.fst = result; Types.snd = useless_label } = eta2109 in
     204  let { Types.fst = result; Types.snd = useless_label } = eta2131 in
    205205  { Types.fst = (Csyntax.Ssequence (result, (Csyntax.Slabel (exit_label,
    206206  Csyntax.Sskip)))); Types.snd = uv2 }
     
    219219    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
    220220  | Csyntax.Ssequence (s1, s2) ->
    221     let { Types.fst = eta2123; Types.snd = u' } = switch_removal s1 u in
    222     let { Types.fst = s1'; Types.snd = acc1 } = eta2123 in
    223     let { Types.fst = eta2122; Types.snd = u'' } = switch_removal s2 u' in
    224     let { Types.fst = s2'; Types.snd = acc2 } = eta2122 in
     221    let { Types.fst = eta2145; Types.snd = u' } = switch_removal s1 u in
     222    let { Types.fst = s1'; Types.snd = acc1 } = eta2145 in
     223    let { Types.fst = eta2144; Types.snd = u'' } = switch_removal s2 u' in
     224    let { Types.fst = s2'; Types.snd = acc2 } = eta2144 in
    225225    { Types.fst = { Types.fst = (Csyntax.Ssequence (s1', s2')); Types.snd =
    226226    (List.append acc1 acc2) }; Types.snd = u'' }
    227227  | Csyntax.Sifthenelse (e, s1, s2) ->
    228     let { Types.fst = eta2125; Types.snd = u' } = switch_removal s1 u in
    229     let { Types.fst = s1'; Types.snd = acc1 } = eta2125 in
    230     let { Types.fst = eta2124; Types.snd = u'' } = switch_removal s2 u' in
    231     let { Types.fst = s2'; Types.snd = acc2 } = eta2124 in
     228    let { Types.fst = eta2147; Types.snd = u' } = switch_removal s1 u in
     229    let { Types.fst = s1'; Types.snd = acc1 } = eta2147 in
     230    let { Types.fst = eta2146; Types.snd = u'' } = switch_removal s2 u' in
     231    let { Types.fst = s2'; Types.snd = acc2 } = eta2146 in
    232232    { Types.fst = { Types.fst = (Csyntax.Sifthenelse (e, s1', s2'));
    233233    Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
    234234  | Csyntax.Swhile (e, body) ->
    235     let { Types.fst = eta2126; Types.snd = u' } = switch_removal body u in
    236     let { Types.fst = body'; Types.snd = acc } = eta2126 in
     235    let { Types.fst = eta2148; Types.snd = u' } = switch_removal body u in
     236    let { Types.fst = body'; Types.snd = acc } = eta2148 in
    237237    { Types.fst = { Types.fst = (Csyntax.Swhile (e, body')); Types.snd =
    238238    acc }; Types.snd = u' }
    239239  | Csyntax.Sdowhile (e, body) ->
    240     let { Types.fst = eta2127; Types.snd = u' } = switch_removal body u in
    241     let { Types.fst = body'; Types.snd = acc } = eta2127 in
     240    let { Types.fst = eta2149; Types.snd = u' } = switch_removal body u in
     241    let { Types.fst = body'; Types.snd = acc } = eta2149 in
    242242    { Types.fst = { Types.fst = (Csyntax.Sdowhile (e, body')); Types.snd =
    243243    acc }; Types.snd = u' }
    244244  | Csyntax.Sfor (s1, e, s2, s3) ->
    245     let { Types.fst = eta2130; Types.snd = u' } = switch_removal s1 u in
    246     let { Types.fst = s1'; Types.snd = acc1 } = eta2130 in
    247     let { Types.fst = eta2129; Types.snd = u'' } = switch_removal s2 u' in
    248     let { Types.fst = s2'; Types.snd = acc2 } = eta2129 in
    249     let { Types.fst = eta2128; Types.snd = u''' } = switch_removal s3 u'' in
    250     let { Types.fst = s3'; Types.snd = acc3 } = eta2128 in
     245    let { Types.fst = eta2152; Types.snd = u' } = switch_removal s1 u in
     246    let { Types.fst = s1'; Types.snd = acc1 } = eta2152 in
     247    let { Types.fst = eta2151; Types.snd = u'' } = switch_removal s2 u' in
     248    let { Types.fst = s2'; Types.snd = acc2 } = eta2151 in
     249    let { Types.fst = eta2150; Types.snd = u''' } = switch_removal s3 u'' in
     250    let { Types.fst = s3'; Types.snd = acc3 } = eta2150 in
    251251    { Types.fst = { Types.fst = (Csyntax.Sfor (s1', e, s2', s3'));
    252252    Types.snd = (List.append acc1 (List.append acc2 acc3)) }; Types.snd =
     
    259259    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
    260260  | Csyntax.Sswitch (e, branches) ->
    261     let { Types.fst = eta2131; Types.snd = u' } =
     261    let { Types.fst = eta2153; Types.snd = u' } =
    262262      switch_removal_branches branches u
    263263    in
    264     let { Types.fst = sf_branches; Types.snd = acc } = eta2131 in
     264    let { Types.fst = sf_branches; Types.snd = acc } = eta2153 in
    265265    let { Types.fst = switch_tmp; Types.snd = u'' } =
    266266      Identifiers.fresh PreIdentifiers.SymbolTag u'
     
    276276    (Csyntax.typeof e) }, acc)) }; Types.snd = u''' }
    277277  | Csyntax.Slabel (label, body) ->
    278     let { Types.fst = eta2132; Types.snd = u' } = switch_removal body u in
    279     let { Types.fst = body'; Types.snd = acc } = eta2132 in
     278    let { Types.fst = eta2154; Types.snd = u' } = switch_removal body u in
     279    let { Types.fst = body'; Types.snd = acc } = eta2154 in
    280280    { Types.fst = { Types.fst = (Csyntax.Slabel (label, body')); Types.snd =
    281281    acc }; Types.snd = u' }
     
    283283    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
    284284  | Csyntax.Scost (cost, body) ->
    285     let { Types.fst = eta2133; Types.snd = u' } = switch_removal body u in
    286     let { Types.fst = body'; Types.snd = acc } = eta2133 in
     285    let { Types.fst = eta2155; Types.snd = u' } = switch_removal body u in
     286    let { Types.fst = body'; Types.snd = acc } = eta2155 in
    287287    { Types.fst = { Types.fst = (Csyntax.Scost (cost, body')); Types.snd =
    288288    acc }; Types.snd = u' }
     
    294294  match l with
    295295  | Csyntax.LSdefault st ->
    296     let { Types.fst = eta2134; Types.snd = u' } = switch_removal st u in
    297     let { Types.fst = st'; Types.snd = acc1 } = eta2134 in
     296    let { Types.fst = eta2156; Types.snd = u' } = switch_removal st u in
     297    let { Types.fst = st'; Types.snd = acc1 } = eta2156 in
    298298    { Types.fst = { Types.fst = (Csyntax.LSdefault st'); Types.snd = acc1 };
    299299    Types.snd = u' }
    300300  | Csyntax.LScase (sz, int, st, tl) ->
    301     let { Types.fst = eta2136; Types.snd = u' } =
     301    let { Types.fst = eta2158; Types.snd = u' } =
    302302      switch_removal_branches tl u
    303303    in
    304     let { Types.fst = tl_result; Types.snd = acc1 } = eta2136 in
    305     let { Types.fst = eta2135; Types.snd = u'' } = switch_removal st u' in
    306     let { Types.fst = st'; Types.snd = acc2 } = eta2135 in
     304    let { Types.fst = tl_result; Types.snd = acc1 } = eta2158 in
     305    let { Types.fst = eta2157; Types.snd = u'' } = switch_removal st u' in
     306    let { Types.fst = st'; Types.snd = acc2 } = eta2157 in
    307307    { Types.fst = { Types.fst = (Csyntax.LScase (sz, int, st', tl_result));
    308308    Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
     
    312312    Identifiers.universe) Types.prod -> 'a1 **)
    313313let ret_st x =
    314   let { Types.fst = eta2137; Types.snd = u } = x in eta2137.Types.fst
     314  let { Types.fst = eta2159; Types.snd = u } = x in eta2159.Types.fst
    315315
    316316(** val ret_vars :
     
    319319    List.list **)
    320320let ret_vars x =
    321   let { Types.fst = eta2138; Types.snd = u } = x in eta2138.Types.snd
     321  let { Types.fst = eta2160; Types.snd = u } = x in eta2160.Types.snd
    322322
    323323(** val ret_u :
     
    325325    Identifiers.universe) Types.prod -> Identifiers.universe **)
    326326let ret_u x =
    327   let { Types.fst = eta2139; Types.snd = u } = x in
    328   let { Types.fst = s; Types.snd = vars } = eta2139 in u
     327  let { Types.fst = eta2161; Types.snd = u } = x in
     328  let { Types.fst = s; Types.snd = vars } = eta2161 in u
    329329
    330330(** val least_identifier : PreIdentifiers.identifier **)
     
    406406let function_switch_removal f =
    407407  let u = Fresh.universe_of_max (max_id_of_function f) in
    408   let { Types.fst = eta2140; Types.snd = u' } =
     408  let { Types.fst = eta2162; Types.snd = u' } =
    409409    switch_removal f.Csyntax.fn_body u
    410410  in
    411   let { Types.fst = st; Types.snd = vars } = eta2140 in
     411  let { Types.fst = st; Types.snd = vars } = eta2162 in
    412412  let result = { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
    413413    f.Csyntax.fn_params; Csyntax.fn_vars =
  • driver/extracted/toCminor.ml

    r3059 r3106  
    20632063    Obj.magic
    20642064      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2065         (fun eta2356 ->
    2066         let result = eta2356 in
     2065        (fun eta2378 ->
     2066        let result = eta2378 in
    20672067        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20682068        (fun _ ->
  • driver/extracted/toRTLabs.ml

    r3059 r3106  
    121121  List.foldr (fun idt rsengen ->
    122122    let { Types.fst = id; Types.snd = ty } = idt in
    123     let { Types.fst = eta2859; Types.snd = gen0 } = rsengen in
    124     let { Types.fst = rs; Types.snd = en0 } = eta2859 in
     123    let { Types.fst = eta2881; Types.snd = gen0 } = rsengen in
     124    let { Types.fst = rs; Types.snd = en0 } = eta2881 in
    125125    let { Types.fst = r; Types.snd = gen' } =
    126126      Identifiers.fresh PreIdentifiers.RegisterTag gen0
     
    13451345  let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in
    13461346  let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in
    1347   (let { Types.fst = eta3086; Types.snd = reggen1 } =
     1347  (let { Types.fst = eta3108; Types.snd = reggen1 } =
    13481348     populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0
    13491349       f.Cminor_syntax.f_params
    13501350   in
    1351   let { Types.fst = params; Types.snd = env1 } = eta3086 in
     1351  let { Types.fst = params; Types.snd = env1 } = eta3108 in
    13521352  (fun _ ->
    1353   (let { Types.fst = eta3085; Types.snd = reggen2 } =
     1353  (let { Types.fst = eta3107; Types.snd = reggen2 } =
    13541354     populate_env env1 reggen1 f.Cminor_syntax.f_vars
    13551355   in
    1356   let { Types.fst = locals0; Types.snd = env0 } = eta3085 in
     1356  let { Types.fst = locals0; Types.snd = env0 } = eta3107 in
    13571357  (fun _ ->
    13581358  (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
Note: See TracChangeset for help on using the changeset viewer.