Changeset 3069


Ignore:
Timestamp:
Apr 2, 2013, 2:09:34 PM (4 years ago)
Author:
sacerdot
Message:

New extraction.

Location:
extracted
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • extracted/assembly.ml

    r3065 r3069  
    26442644| ASM.JMP arg -> List.Cons ((ASM.RealInstruction (ASM.JMP arg)), List.Nil)
    26452645
     2646(** val is_code : AST.region -> Bool.bool **)
     2647let is_code = function
     2648| AST.XData -> Bool.False
     2649| AST.Code -> Bool.True
     2650
    26462651(** val expand_pseudo_instruction :
    26472652    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
    26482653    -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
    2649     BitVector.word) -> ASM.pseudo_instruction -> ASM.instruction List.list **)
     2654    (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
     2655    ASM.instruction List.list **)
    26502656let expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels = function
    26512657| ASM.Instruction instr ->
     
    27142720     List.Cons ((ASM.LCALL address), List.Nil))
    27152721| ASM.Mov (d, trgt, off) ->
    2716   let addr =
    2717     (Arithmetic.add_16_with_carry (lookup_datalabels trgt) off Bool.False).Types.fst
     2722  let { Types.fst = r; Types.snd = addr } = lookup_datalabels trgt in
     2723  let addr0 = (Arithmetic.add_16_with_carry addr off Bool.False).Types.fst in
     2724  let addr1 =
     2725    match is_code r with
     2726    | Bool.True -> sigma addr0
     2727    | Bool.False -> addr0
    27182728  in
    27192729  (match d with
    27202730   | Types.Inl x ->
    2721      let address = ASM.DATA16 addr in
     2731     let address = ASM.DATA16 addr1 in
    27222732     List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
    27232733     (Types.Inr { Types.fst = ASM.DPTR; Types.snd = address }))))), List.Nil)
     
    27282738          (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    27292739            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    2730             (Nat.S (Nat.S Nat.O)))))))) addr).Types.fst
     2740            (Nat.S (Nat.S Nat.O)))))))) addr1).Types.fst
    27312741        | ASM.LOW ->
    27322742          (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    27332743            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    2734             (Nat.S (Nat.S Nat.O)))))))) addr).Types.snd)
     2744            (Nat.S (Nat.S Nat.O)))))))) addr1).Types.snd)
    27352745     in
    27362746     (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
     
    27442754      | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
    27452755      | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
    2746       | ASM.REGISTER r ->
     2756      | ASM.REGISTER r0 ->
    27472757        (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
    27482758          (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
    2749           (ASM.REGISTER r); Types.snd = v }))))))), List.Nil))
     2759          (ASM.REGISTER r0); Types.snd = v }))))))), List.Nil))
    27502760      | ASM.ACC_A ->
    27512761        (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
     
    27702780    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
    27712781    -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
    2772     BitVector.word) -> ASM.pseudo_instruction -> (Nat.nat, Bool.bool
    2773     Vector.vector List.list) Types.prod **)
     2782    (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
     2783    (Nat.nat, Bool.bool Vector.vector List.list) Types.prod **)
    27742784let assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels i =
    27752785  let pseudos =
     
    27832793
    27842794(** val instruction_size :
    2785     (ASM.identifier -> BitVector.word) -> (ASM.identifier -> BitVector.word)
    2786     -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
    2787     BitVector.word -> ASM.pseudo_instruction -> Nat.nat **)
     2795    (ASM.identifier -> BitVector.word) -> (ASM.identifier -> (AST.region,
     2796    BitVector.word) Types.prod) -> (BitVector.word -> BitVector.word) ->
     2797    (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.pseudo_instruction
     2798    -> Nat.nat **)
    27882799let instruction_size lookup_labels lookup_datalabels sigma policy ppc i =
    27892800  (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
     
    28082819  in
    28092820  let lookup_datalabels = fun x ->
    2810     Identifiers.lookup_def PreIdentifiers.ASMTag datalabels x
    2811       (sigma (lookup_labels x))
     2821    match Identifiers.lookup PreIdentifiers.ASMTag
     2822            (Status.construct_datalabels preamble) x with
     2823    | Types.None -> { Types.fst = AST.Code; Types.snd = (lookup_labels x) }
     2824    | Types.Some addr -> { Types.fst = AST.XData; Types.snd = addr }
    28122825  in
    28132826  (let { Types.fst = next_pc; Types.snd = revcode } =
  • extracted/assembly.mli

    r3065 r3069  
    144144  ASM.preinstruction -> ASM.instruction List.list
    145145
     146val is_code : AST.region -> Bool.bool
     147
    146148val expand_pseudo_instruction :
    147149  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
    148150  (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
    149   BitVector.word) -> ASM.pseudo_instruction -> ASM.instruction List.list
     151  (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
     152  ASM.instruction List.list
    150153
    151154val assembly_1_pseudoinstruction :
    152155  (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) ->
    153156  (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
    154   BitVector.word) -> ASM.pseudo_instruction -> (Nat.nat, Bool.bool
    155   Vector.vector List.list) Types.prod
     157  (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
     158  (Nat.nat, Bool.bool Vector.vector List.list) Types.prod
    156159
    157160val instruction_size :
    158   (ASM.identifier -> BitVector.word) -> (ASM.identifier -> BitVector.word) ->
    159   (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
    160   BitVector.word -> ASM.pseudo_instruction -> Nat.nat
     161  (ASM.identifier -> BitVector.word) -> (ASM.identifier -> (AST.region,
     162  BitVector.word) Types.prod) -> (BitVector.word -> BitVector.word) ->
     163  (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.pseudo_instruction
     164  -> Nat.nat
    161165
    162166val assembly :
  • extracted/interpret.ml

    r3064 r3069  
    16311631              | Types.Inr r'' ->
    16321632                let { Types.fst = addr1; Types.snd = addr2 } = r'' in
    1633                 Status.set_arg_16 cm s0 (Status.get_arg_16 cm s0 addr2) addr1)
     1633                Status.set_arg_16 cm s0
     1634                  (Status.get_arg_16 cm s0
     1635                    (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
     1636                      (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Data16,
     1637                      Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O),
     1638                      ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr,
     1639                      Vector.VEmpty)))) addr2)) addr1)
    16341640           | Types.Inr r ->
    16351641             let { Types.fst = addr1; Types.snd = addr2 } = r in
     
    19301936       Status.set_program_counter cm s2 new_pc)
    19311937   | ASM.NOP -> (fun _ -> let s0 = add_ticks1 s in s0)
    1932    | ASM.JMP x ->
    1933      (fun _ ->
    1934        let s0 = add_ticks1 s in
    1935        let dptr =
    1936          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1937            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1938            (Nat.S (Nat.S Nat.O))))))))
    1939            (Status.get_8051_sfr cm s0 Status.SFR_DPH)
    1940            (Status.get_8051_sfr cm s0 Status.SFR_DPL)
    1941        in
    1942        let big_acc =
    1943          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1944            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1945            (Nat.S (Nat.S Nat.O))))))))
    1946            (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1947              (Nat.S Nat.O)))))))))
    1948            (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
    1949        in
     1938   | ASM.JMP acc_dptr ->
     1939     (fun _ ->
     1940       let s0 = add_ticks1 s in
    19501941       let jmp_addr =
    1951          Arithmetic.add
    1952            (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1953              Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1954              (Nat.S Nat.O))))))))) big_acc dptr
     1942         Status.get_arg_16 cm s0
     1943           (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
     1944             Nat.O) (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty))
     1945             (Vector.VCons ((Nat.S Nat.O), ASM.Data16, (Vector.VCons (Nat.O,
     1946             ASM.Acc_dptr, Vector.VEmpty)))) acc_dptr)
    19551947       in
    19561948       Status.set_program_counter cm s0 jmp_addr)) __
     
    35013493              | Types.Inr r'' ->
    35023494                let { Types.fst = addr1; Types.snd = addr2 } = r'' in
    3503                 Status.set_arg_16 cm s0 (Status.get_arg_16 cm s0 addr2) addr1)
     3495                Status.set_arg_16 cm s0
     3496                  (Status.get_arg_16 cm s0
     3497                    (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O
     3498                      (Nat.S Nat.O) (Vector.VCons (Nat.O, ASM.Data16,
     3499                      Vector.VEmpty)) (Vector.VCons ((Nat.S Nat.O),
     3500                      ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr,
     3501                      Vector.VEmpty)))) addr2)) addr1)
    35043502           | Types.Inr r ->
    35053503             let { Types.fst = addr1; Types.snd = addr2 } = r in
     
    38163814       Status.set_program_counter cm s2 new_pc)) __)) __)
    38173815   | ASM.NOP -> (fun _ -> let s0 = add_ticks2 s in s0)
    3818    | ASM.JMP x ->
    3819      (fun _ ->
    3820        let s0 = add_ticks1 s in
    3821        let dptr =
    3822          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3823            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3824            (Nat.S (Nat.S Nat.O))))))))
    3825            (Status.get_8051_sfr cm s0 Status.SFR_DPH)
    3826            (Status.get_8051_sfr cm s0 Status.SFR_DPL)
    3827        in
    3828        let big_acc =
    3829          Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3830            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3831            (Nat.S (Nat.S Nat.O))))))))
    3832            (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3833              (Nat.S Nat.O)))))))))
    3834            (Status.get_8051_sfr cm s0 Status.SFR_ACC_A)
    3835        in
     3816   | ASM.JMP acc_dptr ->
     3817     (fun _ ->
     3818       let s0 = add_ticks1 s in
    38363819       let jmp_addr =
    3837          Arithmetic.add
    3838            (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3839              Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3840              (Nat.S Nat.O))))))))) big_acc dptr
    3841        in
    3842        let new_pc =
    3843          Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3844            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    3845            Nat.O)))))))))))))))) s0.Status.program_counter jmp_addr
    3846        in
    3847        Status.set_program_counter cm s0 new_pc)) __
     3820         Status.get_arg_16 cm s0
     3821           (ASM.subaddressing_modeel__o__mk_subaddressing_mode Nat.O (Nat.S
     3822             Nat.O) (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty))
     3823             (Vector.VCons ((Nat.S Nat.O), ASM.Data16, (Vector.VCons (Nat.O,
     3824             ASM.Acc_dptr, Vector.VEmpty)))) acc_dptr)
     3825       in
     3826       Status.set_program_counter cm s0 jmp_addr)) __
    38483827
    38493828(** val compute_target_of_unconditional_jump :
  • extracted/lINToASM.ml

    r3059 r3069  
    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 = eta154; 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 } = eta154 in
    318318    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
    319319    u.ident_map; label_map =
     
    10401040      Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
    10411041
    1042 type init_mutable = { virtual_dptr : Z.z; actual_dptr : Z.z;
     1042type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod;
     1043                      actual_dptr : (ASM.identifier, Z.z) Types.prod;
    10431044                      built_code : ASM.labelled_instruction List.list
    10441045                                   List.list;
     
    10471048
    10481049(** val init_mutable_rect_Type4 :
    1049     (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
    1050     (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
    1051     init_mutable -> 'a1 **)
    1052 let rec init_mutable_rect_Type4 h_mk_init_mutable x_21509 =
     1050    ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     1051    ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     1052    BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
     1053let rec init_mutable_rect_Type4 h_mk_init_mutable x_614 =
    10531054  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1054     built_code = built_code0; built_preamble = built_preamble0 } = x_21509
     1055    built_code = built_code0; built_preamble = built_preamble0 } = x_614
    10551056  in
    10561057  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
    10571058
    10581059(** val init_mutable_rect_Type5 :
    1059     (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
    1060     (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
    1061     init_mutable -> 'a1 **)
    1062 let rec init_mutable_rect_Type5 h_mk_init_mutable x_21511 =
     1060    ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     1061    ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     1062    BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
     1063let rec init_mutable_rect_Type5 h_mk_init_mutable x_616 =
    10631064  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1064     built_code = built_code0; built_preamble = built_preamble0 } = x_21511
     1065    built_code = built_code0; built_preamble = built_preamble0 } = x_616
    10651066  in
    10661067  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
    10671068
    10681069(** val init_mutable_rect_Type3 :
    1069     (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
    1070     (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
    1071     init_mutable -> 'a1 **)
    1072 let rec init_mutable_rect_Type3 h_mk_init_mutable x_21513 =
     1070    ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     1071    ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     1072    BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
     1073let rec init_mutable_rect_Type3 h_mk_init_mutable x_618 =
    10731074  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1074     built_code = built_code0; built_preamble = built_preamble0 } = x_21513
     1075    built_code = built_code0; built_preamble = built_preamble0 } = x_618
    10751076  in
    10761077  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
    10771078
    10781079(** val init_mutable_rect_Type2 :
    1079     (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
    1080     (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
    1081     init_mutable -> 'a1 **)
    1082 let rec init_mutable_rect_Type2 h_mk_init_mutable x_21515 =
     1080    ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     1081    ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     1082    BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
     1083let rec init_mutable_rect_Type2 h_mk_init_mutable x_620 =
    10831084  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1084     built_code = built_code0; built_preamble = built_preamble0 } = x_21515
     1085    built_code = built_code0; built_preamble = built_preamble0 } = x_620
    10851086  in
    10861087  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
    10871088
    10881089(** val init_mutable_rect_Type1 :
    1089     (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
    1090     (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
    1091     init_mutable -> 'a1 **)
    1092 let rec init_mutable_rect_Type1 h_mk_init_mutable x_21517 =
     1090    ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     1091    ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     1092    BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
     1093let rec init_mutable_rect_Type1 h_mk_init_mutable x_622 =
    10931094  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1094     built_code = built_code0; built_preamble = built_preamble0 } = x_21517
     1095    built_code = built_code0; built_preamble = built_preamble0 } = x_622
    10951096  in
    10961097  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
    10971098
    10981099(** val init_mutable_rect_Type0 :
    1099     (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
    1100     (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
    1101     init_mutable -> 'a1 **)
    1102 let rec init_mutable_rect_Type0 h_mk_init_mutable x_21519 =
     1100    ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     1101    ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     1102    BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
     1103let rec init_mutable_rect_Type0 h_mk_init_mutable x_624 =
    11031104  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
    1104     built_code = built_code0; built_preamble = built_preamble0 } = x_21519
     1105    built_code = built_code0; built_preamble = built_preamble0 } = x_624
    11051106  in
    11061107  h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
    11071108
    1108 (** val virtual_dptr : init_mutable -> Z.z **)
     1109(** val virtual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod **)
    11091110let rec virtual_dptr xxx =
    11101111  xxx.virtual_dptr
    11111112
    1112 (** val actual_dptr : init_mutable -> Z.z **)
     1113(** val actual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod **)
    11131114let rec actual_dptr xxx =
    11141115  xxx.actual_dptr
     
    11251126
    11261127(** val init_mutable_inv_rect_Type4 :
    1127     init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list
    1128     List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> __
    1129     -> 'a1) -> 'a1 **)
     1128    init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
     1129    Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
     1130    (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
     1131    'a1 **)
    11301132let init_mutable_inv_rect_Type4 hterm h1 =
    11311133  let hcut = init_mutable_rect_Type4 h1 hterm in hcut __
    11321134
    11331135(** val init_mutable_inv_rect_Type3 :
    1134     init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list
    1135     List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> __
    1136     -> 'a1) -> 'a1 **)
     1136    init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
     1137    Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
     1138    (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
     1139    'a1 **)
    11371140let init_mutable_inv_rect_Type3 hterm h1 =
    11381141  let hcut = init_mutable_rect_Type3 h1 hterm in hcut __
    11391142
    11401143(** val init_mutable_inv_rect_Type2 :
    1141     init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list
    1142     List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> __
    1143     -> 'a1) -> 'a1 **)
     1144    init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
     1145    Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
     1146    (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
     1147    'a1 **)
    11441148let init_mutable_inv_rect_Type2 hterm h1 =
    11451149  let hcut = init_mutable_rect_Type2 h1 hterm in hcut __
    11461150
    11471151(** val init_mutable_inv_rect_Type1 :
    1148     init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list
    1149     List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> __
    1150     -> 'a1) -> 'a1 **)
     1152    init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
     1153    Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
     1154    (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
     1155    'a1 **)
    11511156let init_mutable_inv_rect_Type1 hterm h1 =
    11521157  let hcut = init_mutable_rect_Type1 h1 hterm in hcut __
    11531158
    11541159(** val init_mutable_inv_rect_Type0 :
    1155     init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list
    1156     List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> __
    1157     -> 'a1) -> 'a1 **)
     1160    init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier,
     1161    Z.z) Types.prod -> ASM.labelled_instruction List.list List.list ->
     1162    (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
     1163    'a1 **)
    11581164let init_mutable_inv_rect_Type0 hterm h1 =
    11591165  let hcut = init_mutable_rect_Type0 h1 hterm in hcut __
     
    11821188    built_preamble = acc2 } = mut
    11831189  in
    1184   let off = Z.zminus virt act in
    11851190  let pre =
    1186     match Z.eqZb off Z.OZ with
    1187     | Bool.True -> List.Nil
     1191    match Identifiers.eq_identifier PreIdentifiers.ASMTag virt.Types.fst
     1192            act.Types.fst with
     1193    | Bool.True ->
     1194      let off = Z.zminus virt.Types.snd act.Types.snd in
     1195      (match Z.eqZb off Z.OZ with
     1196       | Bool.True -> List.Nil
     1197       | Bool.False ->
     1198         (match Z.eqZb off (Z.z_of_nat (Nat.S Nat.O)) with
     1199          | Bool.True ->
     1200            List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction
     1201              (ASM.INC ASM.DPTR)) }, List.Nil)
     1202          | Bool.False ->
     1203            List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Mov
     1204              ((Types.Inl ASM.DPTR), virt.Types.fst,
     1205              (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1206                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1207                (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) virt.Types.snd))) },
     1208              List.Nil)))
    11881209    | Bool.False ->
    1189       (match Z.eqZb off (Z.z_of_nat (Nat.S Nat.O)) with
    1190        | Bool.True ->
    1191          List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction
    1192            (ASM.INC ASM.DPTR)) }, List.Nil)
    1193        | Bool.False ->
    1194          List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction
    1195            (ASM.MOV (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR;
    1196            Types.snd = (ASM.DATA16
    1197            (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1198              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1199              (Nat.S (Nat.S Nat.O)))))))))))))))) virt)) }))))) }, List.Nil))
     1210      List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Mov ((Types.Inl
     1211        ASM.DPTR), virt.Types.fst,
     1212        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1213          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1214          (Nat.S Nat.O)))))))))))))))) virt.Types.snd))) }, List.Nil)
    12001215  in
    12011216  let post =
     
    12131228          Nat.O))))))))))))))))))) }
    12141229  in
    1215   { virtual_dptr = (Z.zsucc virt); actual_dptr = virt; built_code =
    1216   (List.Cons
     1230  { virtual_dptr = { Types.fst = virt.Types.fst; Types.snd =
     1231  (Z.zsucc virt.Types.snd) }; actual_dptr = virt; built_code = (List.Cons
    12171232  ((List.append pre (List.Cons (post, (List.Cons ({ Types.fst = Types.None;
    12181233     Types.snd = (ASM.Instruction (ASM.MOVX (Types.Inr { Types.fst =
     
    12641279           (store_byte by2 (store_byte by1 (store_byte by0 mut))))
    12651280     | AST.Init_space n ->
     1281       let { Types.fst = virt_id; Types.snd = virt_off } = mut.virtual_dptr
     1282       in
    12661283       Monad.m_return0 (Monad.smax_def State.state_monad) { virtual_dptr =
    1267          (Z.zplus (Z.z_of_nat n) mut.virtual_dptr); actual_dptr =
    1268          mut.actual_dptr; built_code = mut.built_code; built_preamble =
    1269          mut.built_preamble }
     1284         { Types.fst = virt_id; Types.snd =
     1285         (Z.zplus (Z.z_of_nat n) virt_off) }; actual_dptr = mut.actual_dptr;
     1286         built_code = mut.built_code; built_preamble = mut.built_preamble }
    12701287     | AST.Init_null ->
    12711288       let z =
     
    12871304let do_store_global m_mut id_reg_data =
    12881305  Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut ->
    1289     let { Types.fst = eta28633; Types.snd = data } = id_reg_data in
    1290     let { Types.fst = id; Types.snd = reg } = eta28633 in
     1306    let { Types.fst = eta171; Types.snd = data } = id_reg_data in
     1307    let { Types.fst = id; Types.snd = reg } = eta171 in
    12911308    Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id)
    12921309      (fun id0 ->
    1293       let mut0 = { virtual_dptr = mut.virtual_dptr; actual_dptr =
    1294         mut.actual_dptr; built_code = mut.built_code; built_preamble =
    1295         (List.Cons ({ Types.fst = id0; Types.snd =
    1296         (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1310      let mut0 = { virtual_dptr = { Types.fst = id0; Types.snd = Z.OZ };
     1311        actual_dptr = mut.actual_dptr; built_code = mut.built_code;
     1312        built_preamble = (List.Cons ({ Types.fst = id0; Types.snd =
     1313        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    12971314          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1298           (Nat.S Nat.O)))))))))))))))) mut.virtual_dptr) },
    1299         mut.built_preamble)) }
     1315          (Nat.S (Nat.S Nat.O))))))))))))))))
     1316          (Globalenvs.size_init_data_list data)) }, mut.built_preamble)) }
    13001317      in
    13011318      Util.foldl do_store_init_data
     
    13171334    Monad.m_bind0 (Monad.smax_def State.state_monad) State.state_get
    13181335      (fun u ->
    1319       let start_sp =
    1320         Z.zopp
    1321           (Z.z_of_nat (Nat.S
    1322             (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p)))
     1336      let dummy_dptr = { Types.fst = Positive.One; Types.snd =
     1337        (Z.zopp (Z.z_of_nat (Nat.S Nat.O))) }
    13231338      in
    1324       let mut = { virtual_dptr = start_sp; actual_dptr = Z.OZ; built_code =
    1325         List.Nil; built_preamble = List.Nil }
     1339      let mut = { virtual_dptr = dummy_dptr; actual_dptr = dummy_dptr;
     1340        built_code = List.Nil; built_preamble = List.Nil }
    13261341      in
    13271342      Monad.m_bind0 (Monad.smax_def State.state_monad)
     
    13361351              (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    13371352                (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    1338                 (Nat.S (Nat.S (Nat.S Nat.O))))))))) start_sp)
     1353                (Nat.S (Nat.S (Nat.S Nat.O)))))))))
     1354              (Z.zopp
     1355                (Z.z_of_nat (Nat.S
     1356                  (Joint.globals_stacksize
     1357                    (Joint.lin_params_to_params LIN.lIN) p)))))
    13391358        in
    13401359        let init_isp = ASM.DATA
  • extracted/lINToASM.mli

    r3059 r3069  
    254254  Joint.joint_function) Types.prod -> __
    255255
    256 type init_mutable = { virtual_dptr : Z.z; actual_dptr : Z.z;
     256type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod;
     257                      actual_dptr : (ASM.identifier, Z.z) Types.prod;
    257258                      built_code : ASM.labelled_instruction List.list
    258259                                   List.list;
     
    261262
    262263val init_mutable_rect_Type4 :
    263   (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
    264   (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
    265   init_mutable -> 'a1
     264  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     265  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     266  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
    266267
    267268val init_mutable_rect_Type5 :
    268   (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
    269   (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
    270   init_mutable -> 'a1
     269  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     270  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     271  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
    271272
    272273val init_mutable_rect_Type3 :
    273   (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
    274   (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
    275   init_mutable -> 'a1
     274  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     275  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     276  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
    276277
    277278val init_mutable_rect_Type2 :
    278   (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
    279   (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
    280   init_mutable -> 'a1
     279  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     280  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     281  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
    281282
    282283val init_mutable_rect_Type1 :
    283   (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
    284   (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
    285   init_mutable -> 'a1
     284  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     285  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     286  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
    286287
    287288val init_mutable_rect_Type0 :
    288   (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
    289   (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
    290   init_mutable -> 'a1
    291 
    292 val virtual_dptr : init_mutable -> Z.z
    293 
    294 val actual_dptr : init_mutable -> Z.z
     289  ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     290  ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     291  BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1
     292
     293val virtual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod
     294
     295val actual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod
    295296
    296297val built_code : init_mutable -> ASM.labelled_instruction List.list List.list
     
    300301
    301302val init_mutable_inv_rect_Type4 :
    302   init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list
    303   -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
    304   'a1
     303  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
     304  Types.prod -> ASM.labelled_instruction List.list List.list ->
     305  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
    305306
    306307val init_mutable_inv_rect_Type3 :
    307   init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list
    308   -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
    309   'a1
     308  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
     309  Types.prod -> ASM.labelled_instruction List.list List.list ->
     310  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
    310311
    311312val init_mutable_inv_rect_Type2 :
    312   init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list
    313   -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
    314   'a1
     313  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
     314  Types.prod -> ASM.labelled_instruction List.list List.list ->
     315  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
    315316
    316317val init_mutable_inv_rect_Type1 :
    317   init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list
    318   -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
    319   'a1
     318  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
     319  Types.prod -> ASM.labelled_instruction List.list List.list ->
     320  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
    320321
    321322val init_mutable_inv_rect_Type0 :
    322   init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list
    323   -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
    324   'a1
     323  init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z)
     324  Types.prod -> ASM.labelled_instruction List.list List.list ->
     325  (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1
    325326
    326327val init_mutable_discr : init_mutable -> init_mutable -> __
  • extracted/status.ml

    r3059 r3069  
    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
     
    37803780    'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.word **)
    37813781let get_arg_16 cm s a =
    3782   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Data16,
    3783            Vector.VEmpty)) a with
     3782  (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
     3783           ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty))))
     3784           a with
    37843785   | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
    37853786   | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
     
    37913792   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
    37923793   | ASM.DATA16 d -> (fun _ -> d)
    3793    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
     3794   | ASM.ACC_DPTR ->
     3795     (fun _ ->
     3796       let dptr =
     3797         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3798           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3799           (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
     3800           (get_8051_sfr cm s SFR_DPL)
     3801       in
     3802       let big_acc =
     3803         Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3804           (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3805           (Nat.S (Nat.S Nat.O))))))))
     3806           (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3807             (Nat.S Nat.O))))))))) (get_8051_sfr cm s SFR_ACC_A)
     3808       in
     3809       Arithmetic.add
     3810         (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3811           Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     3812           (Nat.S Nat.O))))))))) big_acc dptr)
    37943813   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
    37953814   | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
     
    42544273    (ASM.identifier, BitVector.word) Types.prod List.list -> BitVector.word
    42554274    Identifiers.identifier_map **)
    4256 let construct_datalabels =
    4257   Util.foldl (fun datalabels preamble ->
    4258     let { Types.fst = name; Types.snd = addr } = preamble in
    4259     Identifiers.add PreIdentifiers.ASMTag datalabels name addr)
    4260     (Identifiers.empty_map PreIdentifiers.ASMTag)
    4261 
     4275let construct_datalabels the_preamble =
     4276  (Util.foldl (fun t preamble ->
     4277    let { Types.fst = datalabels; Types.snd = addr } = t in
     4278    let { Types.fst = name; Types.snd = size } = preamble in
     4279    let { Types.fst = addr0; Types.snd = carry } =
     4280      Arithmetic.sub_16_with_carry addr size Bool.False
     4281    in
     4282    { Types.fst =
     4283    (Identifiers.add PreIdentifiers.ASMTag datalabels name addr0);
     4284    Types.snd = addr0 }) { Types.fst =
     4285    (Identifiers.empty_map PreIdentifiers.ASMTag); Types.snd =
     4286    (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4287      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     4288      Nat.O))))))))))))))))) } the_preamble).Types.fst
     4289
Note: See TracChangeset for help on using the changeset viewer.