Ignore:
Timestamp:
Mar 27, 2013, 4:09:56 PM (7 years ago)
Author:
sacerdot
Message:

New extraction after several bug fixes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/backEndOps.ml

    r2951 r2977  
    402402    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    403403    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    404 let rec eval_rect_Type4 h_mk_Eval x_16349 =
    405   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16349 in
     404let rec eval_rect_Type4 h_mk_Eval x_185 =
     405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_185 in
    406406  h_mk_Eval opaccs0 op4 op5
    407407
     
    411411    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    412412    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    413 let rec eval_rect_Type5 h_mk_Eval x_16351 =
    414   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16351 in
     413let rec eval_rect_Type5 h_mk_Eval x_187 =
     414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_187 in
    415415  h_mk_Eval opaccs0 op4 op5
    416416
     
    420420    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    421421    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    422 let rec eval_rect_Type3 h_mk_Eval x_16353 =
    423   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16353 in
     422let rec eval_rect_Type3 h_mk_Eval x_189 =
     423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_189 in
    424424  h_mk_Eval opaccs0 op4 op5
    425425
     
    429429    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    430430    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    431 let rec eval_rect_Type2 h_mk_Eval x_16355 =
    432   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16355 in
     431let rec eval_rect_Type2 h_mk_Eval x_191 =
     432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_191 in
    433433  h_mk_Eval opaccs0 op4 op5
    434434
     
    438438    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    439439    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    440 let rec eval_rect_Type1 h_mk_Eval x_16357 =
    441   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16357 in
     440let rec eval_rect_Type1 h_mk_Eval x_193 =
     441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_193 in
    442442  h_mk_Eval opaccs0 op4 op5
    443443
     
    447447    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    448448    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    449 let rec eval_rect_Type0 h_mk_Eval x_16359 =
    450   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16359 in
     449let rec eval_rect_Type0 h_mk_Eval x_195 =
     450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_195 in
    451451  h_mk_Eval opaccs0 op4 op5
    452452
     
    705705                 in
    706706                 let { Types.fst = rslt; Types.snd = carry0 } =
    707                    eval0.op3 Bool.False op b2 o1o0.Types.snd
     707                   eval0.op3 Bool.False op o1o0.Types.snd b2
    708708                 in
    709709                 let p0 = Nat.O in
Note: See TracChangeset for help on using the changeset viewer.