Ignore:
Timestamp:
Feb 25, 2013, 9:54:49 PM (7 years ago)
Author:
sacerdot
Message:

Exported again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/backEndOps.ml

    r2717 r2730  
    8080
    8181open ByteValues
     82
     83(** val divmodZ : Z.z -> Z.z -> (Z.z, Z.z) Types.prod **)
     84let divmodZ x y =
     85  match x with
     86  | Z.OZ -> { Types.fst = Z.OZ; Types.snd = Z.OZ }
     87  | Z.Pos n ->
     88    (match y with
     89     | Z.OZ -> { Types.fst = Z.OZ; Types.snd = Z.OZ }
     90     | Z.Pos m ->
     91       let { Types.fst = q; Types.snd = r } = Division.divide n m in
     92       { Types.fst = (Division.natp_to_Z q); Types.snd =
     93       (Division.natp_to_Z r) }
     94     | Z.Neg m ->
     95       let { Types.fst = q; Types.snd = r } = Division.divide n m in
     96       (match r with
     97        | Division.Pzero ->
     98          { Types.fst = (Division.natp_to_negZ q); Types.snd = Z.OZ }
     99        | Division.Ppos x0 ->
     100          { Types.fst = (Z.zpred (Division.natp_to_negZ q)); Types.snd =
     101            (Z.zplus y (Division.natp_to_Z r)) }))
     102  | Z.Neg n ->
     103    (match y with
     104     | Z.OZ -> { Types.fst = Z.OZ; Types.snd = Z.OZ }
     105     | Z.Pos m ->
     106       let { Types.fst = q; Types.snd = r } = Division.divide n m in
     107       (match r with
     108        | Division.Pzero ->
     109          { Types.fst = (Division.natp_to_negZ q); Types.snd = Z.OZ }
     110        | Division.Ppos x0 ->
     111          { Types.fst = (Z.zpred (Division.natp_to_negZ q)); Types.snd =
     112            (Z.zminus y (Division.natp_to_Z r)) })
     113     | Z.Neg m ->
     114       let { Types.fst = q; Types.snd = r } = Division.divide n m in
     115       { Types.fst = (Division.natp_to_Z q); Types.snd =
     116       (Division.natp_to_Z r) })
    82117
    83118type opAccs =
     
    367402    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    368403    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    369 let rec eval_rect_Type4 h_mk_Eval x_15751 =
    370   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_15751 in
     404let rec eval_rect_Type4 h_mk_Eval x_6259 =
     405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_6259 in
    371406  h_mk_Eval opaccs0 op4 op5
    372407
     
    376411    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    377412    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    378 let rec eval_rect_Type5 h_mk_Eval x_15753 =
    379   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_15753 in
     413let rec eval_rect_Type5 h_mk_Eval x_6261 =
     414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_6261 in
    380415  h_mk_Eval opaccs0 op4 op5
    381416
     
    385420    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    386421    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    387 let rec eval_rect_Type3 h_mk_Eval x_15755 =
    388   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_15755 in
     422let rec eval_rect_Type3 h_mk_Eval x_6263 =
     423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_6263 in
    389424  h_mk_Eval opaccs0 op4 op5
    390425
     
    394429    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    395430    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    396 let rec eval_rect_Type2 h_mk_Eval x_15757 =
    397   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_15757 in
     431let rec eval_rect_Type2 h_mk_Eval x_6265 =
     432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_6265 in
    398433  h_mk_Eval opaccs0 op4 op5
    399434
     
    403438    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    404439    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    405 let rec eval_rect_Type1 h_mk_Eval x_15759 =
    406   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_15759 in
     440let rec eval_rect_Type1 h_mk_Eval x_6267 =
     441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_6267 in
    407442  h_mk_Eval opaccs0 op4 op5
    408443
     
    412447    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    413448    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    414 let rec eval_rect_Type0 h_mk_Eval x_15761 =
    415   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_15761 in
     449let rec eval_rect_Type0 h_mk_Eval x_6269 =
     450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_6269 in
    416451  h_mk_Eval opaccs0 op4 op5
    417452
     
    487522    opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    488523    BitVector.byte) Types.prod **)
    489 let opaccs_implementation _ =
    490   failwith "AXIOM TO BE REALIZED"
     524let opaccs_implementation op4 by1 by2 =
     525  let n1 =
     526    BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     527      (Nat.S (Nat.S (Nat.S Nat.O)))))))) by1
     528  in
     529  let n2 =
     530    BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     531      (Nat.S (Nat.S (Nat.S Nat.O)))))))) by2
     532  in
     533  (match op4 with
     534   | Mul ->
     535     let prod0 =
     536       Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     537         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     538         (Nat.S Nat.O))))))))
     539         (BitVectorZ.bitvector_of_Z
     540           (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     541             Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     542             (Nat.S Nat.O))))))))) (Z.z_times n1 n2))
     543     in
     544     { Types.fst = prod0.Types.snd; Types.snd = prod0.Types.fst }
     545   | DivuModu ->
     546     (match Z.eqZb n2 Z.OZ with
     547      | Bool.True -> { Types.fst = by1; Types.snd = by2 }
     548      | Bool.False ->
     549        let { Types.fst = q; Types.snd = r } = divmodZ n1 n2 in
     550        { Types.fst =
     551        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     552          (Nat.S (Nat.S Nat.O)))))))) q); Types.snd =
     553        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     554          (Nat.S (Nat.S Nat.O)))))))) r) }))
    491555
    492556(** val op1_implementation : op1 -> BitVector.byte -> BitVector.byte **)
    493 let op1_implementation _ =
    494   failwith "AXIOM TO BE REALIZED"
     557let op1_implementation op4 by =
     558  match op4 with
     559  | Cmpl ->
     560    BitVector.negation_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     561      (Nat.S Nat.O)))))))) by
     562  | Inc ->
     563    Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     564      Nat.O)))))))) by
     565      (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     566        (Nat.S (Nat.S Nat.O)))))))) (Nat.S Nat.O))
     567  | Rl ->
     568    Vector.rotate_left (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     569      (Nat.S Nat.O)))))))) (Nat.S Nat.O) by
    495570
    496571(** val op2_implementation :
    497572    BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    498573    (BitVector.byte, BitVector.bit) Types.prod **)
    499 let op2_implementation _ =
    500   failwith "AXIOM TO BE REALIZED"
     574let op2_implementation carry op4 by1 by2 =
     575  match op4 with
     576  | Add ->
     577    let { Types.fst = res1; Types.snd = flags } =
     578      Arithmetic.add_8_with_carry by1 by2 Bool.False
     579    in
     580    { Types.fst = res1; Types.snd =
     581    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
     582  | Addc ->
     583    let { Types.fst = res1; Types.snd = flags } =
     584      Arithmetic.add_8_with_carry by1 by2 carry
     585    in
     586    { Types.fst = res1; Types.snd =
     587    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
     588  | Sub ->
     589    let { Types.fst = res1; Types.snd = flags } =
     590      Arithmetic.sub_8_with_carry by1 by2 carry
     591    in
     592    { Types.fst = res1; Types.snd =
     593    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
     594  | And ->
     595    { Types.fst =
     596      (BitVector.conjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     597        (Nat.S (Nat.S Nat.O)))))))) by1 by2); Types.snd = carry }
     598  | Or ->
     599    { Types.fst =
     600      (BitVector.inclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     601        (Nat.S (Nat.S (Nat.S Nat.O)))))))) by1 by2); Types.snd = carry }
     602  | Xor ->
     603    { Types.fst =
     604      (BitVector.exclusive_disjunction_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     605        (Nat.S (Nat.S (Nat.S Nat.O)))))))) by1 by2); Types.snd = carry }
    501606
    502607(** val eval0 : eval **)
Note: See TracChangeset for help on using the changeset viewer.