Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/backEndOps.ml

    r2743 r2773  
    1717open Extralib
    1818
     19open Lists
     20
     21open Identifiers
     22
     23open Integers
     24
     25open AST
     26
     27open Division
     28
     29open Exp
     30
     31open Arithmetic
     32
    1933open Setoids
    2034
     
    2236
    2337open Option
    24 
    25 open Lists
    26 
    27 open Identifiers
    28 
    29 open Integers
    30 
    31 open AST
    32 
    33 open Division
    34 
    35 open Exp
    36 
    37 open Arithmetic
    3838
    3939open Extranat
     
    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_18831 =
    405   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18831 in
     404let rec eval_rect_Type4 h_mk_Eval x_14141 =
     405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14141 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_18833 =
    414   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18833 in
     413let rec eval_rect_Type5 h_mk_Eval x_14143 =
     414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14143 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_18835 =
    423   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18835 in
     422let rec eval_rect_Type3 h_mk_Eval x_14145 =
     423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14145 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_18837 =
    432   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18837 in
     431let rec eval_rect_Type2 h_mk_Eval x_14147 =
     432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14147 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_18839 =
    441   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18839 in
     440let rec eval_rect_Type1 h_mk_Eval x_14149 =
     441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14149 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_18841 =
    450   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18841 in
     449let rec eval_rect_Type0 h_mk_Eval x_14151 =
     450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_14151 in
    451451  h_mk_Eval opaccs0 op4 op5
    452452
     
    522522    opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
    523523    BitVector.byte) Types.prod **)
    524 let opaccs_implementation op4 by1 by2 =
     524let opaccs_implementation op by1 by2 =
    525525  let n1 =
    526526    BitVectorZ.z_of_unsigned_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    531531      (Nat.S (Nat.S (Nat.S Nat.O)))))))) by2
    532532  in
    533   (match op4 with
     533  (match op with
    534534   | Mul ->
    535      let prod0 =
     535     let prod =
    536536       Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    537537         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    542542             (Nat.S Nat.O))))))))) (Z.z_times n1 n2))
    543543     in
    544      { Types.fst = prod0.Types.snd; Types.snd = prod0.Types.fst }
     544     { Types.fst = prod.Types.snd; Types.snd = prod.Types.fst }
    545545   | DivuModu ->
    546546     (match Z.eqZb n2 Z.OZ with
     
    555555
    556556(** val op1_implementation : op1 -> BitVector.byte -> BitVector.byte **)
    557 let op1_implementation op4 by =
    558   match op4 with
     557let op1_implementation op by =
     558  match op with
    559559  | Cmpl ->
    560560    BitVector.negation_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    572572    BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    573573    (BitVector.byte, BitVector.bit) Types.prod **)
    574 let op2_implementation carry op4 by1 by2 =
    575   match op4 with
     574let op2_implementation carry op by1 by2 =
     575  match op with
    576576  | Add ->
    577     let { Types.fst = res1; Types.snd = flags } =
     577    let { Types.fst = res; Types.snd = flags } =
    578578      Arithmetic.add_8_with_carry by1 by2 Bool.False
    579579    in
    580     { Types.fst = res1; Types.snd =
     580    { Types.fst = res; Types.snd =
    581581    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
    582582  | Addc ->
    583     let { Types.fst = res1; Types.snd = flags } =
     583    let { Types.fst = res; Types.snd = flags } =
    584584      Arithmetic.add_8_with_carry by1 by2 carry
    585585    in
    586     { Types.fst = res1; Types.snd =
     586    { Types.fst = res; Types.snd =
    587587    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
    588588  | Sub ->
    589     let { Types.fst = res1; Types.snd = flags } =
     589    let { Types.fst = res; Types.snd = flags } =
    590590      Arithmetic.sub_8_with_carry by1 by2 carry
    591591    in
    592     { Types.fst = res1; Types.snd =
     592    { Types.fst = res; Types.snd =
    593593    (Vector.get_index' Nat.O (Nat.S (Nat.S Nat.O)) flags) }
    594594  | And ->
     
    613613    opAccs -> ByteValues.beval -> ByteValues.beval -> (ByteValues.beval,
    614614    ByteValues.beval) Types.prod Errors.res **)
    615 let be_opaccs op4 a b =
     615let be_opaccs op a b =
    616616  Obj.magic
    617617    (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    621621        (Obj.magic (ByteValues.byte_of_val ErrorMessages.UnsupportedOp b))
    622622        (fun b' ->
    623         let { Types.fst = a''; Types.snd = b'' } = eval0.opaccs op4 a' b' in
     623        let { Types.fst = a''; Types.snd = b'' } = eval0.opaccs op a' b' in
    624624        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    625625          (ByteValues.BVByte a''); Types.snd = (ByteValues.BVByte b'') })))
    626626
    627627(** val be_op1 : op1 -> ByteValues.beval -> ByteValues.beval Errors.res **)
    628 let be_op1 op4 a =
     628let be_op1 op a =
    629629  Obj.magic
    630630    (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    632632      (fun a' ->
    633633      Monad.m_return0 (Monad.max_def Errors.res0) (ByteValues.BVByte
    634         (eval0.op0 op4 a'))))
     634        (eval0.op0 op a'))))
    635635
    636636(** val op2_bytes :
     
    638638    BitVector.byte Vector.vector -> (BitVector.byte Vector.vector,
    639639    BitVector.bit) Types.prod **)
    640 let op2_bytes op4 n carry =
     640let op2_bytes op n carry =
    641641  let f = fun n0 b1 b2 pr ->
    642642    let { Types.fst = res_tl; Types.snd = carry0 } = pr in
    643643    let { Types.fst = res_hd; Types.snd = carry' } =
    644       eval0.op3 carry0 op4 b1 b2
     644      eval0.op3 carry0 op b1 b2
    645645    in
    646646    { Types.fst = (Vector.VCons (n0, res_hd, res_tl)); Types.snd = carry' }
     
    652652    (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **)
    653653let be_add_sub_byte is_add carry a1 b2 =
    654   let op4 =
     654  let op =
    655655    match is_add with
    656656    | Bool.True -> Addc
     
    674674         (fun carry' ->
    675675         let { Types.fst = rslt; Types.snd = carry'' } =
    676            eval0.op3 carry' op4 b1 b2
     676           eval0.op3 carry' op b1 b2
    677677         in
    678678         Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     
    703703                 in
    704704                 let { Types.fst = rslt; Types.snd = carry0 } =
    705                    eval0.op3 Bool.False op4 b2 o1o0.Types.snd
     705                   eval0.op3 Bool.False op b2 o1o0.Types.snd
    706706                 in
    707707                 let p0 = Nat.O in
    708708                 let ptr' = { Pointers.pblock = ptr.Pointers.pblock;
    709709                   Pointers.poff =
    710                    (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     710                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    711711                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
    712712                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) o1o0.Types.fst
     
    750750                   in
    751751                   let { Types.fst = rslt; Types.snd = ignore } =
    752                      op2_bytes op4 (Nat.S (Nat.S Nat.O)) Bool.False o1o1
     752                     op2_bytes op (Nat.S (Nat.S Nat.O)) Bool.False o1o1
    753753                       (Vector.VCons ((Nat.S Nat.O), b2, (Vector.VCons
    754754                       (Nat.O, by'0, Vector.VEmpty))))
     
    763763                   Errors.OK { Types.fst = (ByteValues.BVptr (ptr'0, part1));
    764764                   Types.snd = (ByteValues.BBptrcarry (is_add, ptr'0, part1,
    765                    (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     765                   (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    766766                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
    767767                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 by'0))) })
     
    798798    ('a1 -> 'a1 -> Bool.bool) -> 'a1 Types.option -> 'a1 Types.option ->
    799799    Bool.bool **)
    800 let eq_opt eq0 m n =
     800let eq_opt eq m n =
    801801  match m with
    802802  | Types.None ->
     
    807807    (match n with
    808808     | Types.None -> Bool.False
    809      | Types.Some b -> eq0 a b)
     809     | Types.Some b -> eq a b)
    810810
    811811(** val be_op2 :
    812812    ByteValues.bebit -> op2 -> ByteValues.beval -> ByteValues.beval ->
    813813    (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res **)
    814 let be_op2 carry op4 a1 a2 =
     814let be_op2 carry op a1 a2 =
    815815  match a1 with
    816816  | ByteValues.BVundef ->
     
    823823         List.Nil))
    824824     | ByteValues.BVnonzero ->
    825        (match op4 with
     825       (match op with
    826826        | Add ->
    827827          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    844844            List.Nil)))
    845845     | ByteValues.BVXor (x, x0, x1) ->
    846        (match op4 with
     846       (match op with
    847847        | Add ->
    848848          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    865865            List.Nil)))
    866866     | ByteValues.BVByte x ->
    867        (match op4 with
     867       (match op with
    868868        | Add ->
    869869          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    894894       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    895895         List.Nil)))
    896   | ByteValues.BVXor (ptr1_opt, ptr1_opt', p3) ->
     896  | ByteValues.BVXor (ptr1_opt, ptr1_opt', p1) ->
    897897    (match a2 with
    898898     | ByteValues.BVundef ->
     
    900900         List.Nil))
    901901     | ByteValues.BVnonzero ->
    902        (match op4 with
     902       (match op with
    903903        | Add ->
    904904          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    920920          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    921921            List.Nil)))
    922      | ByteValues.BVXor (ptr2_opt, ptr2_opt', p4) ->
    923        (match op4 with
     922     | ByteValues.BVXor (ptr2_opt, ptr2_opt', p2) ->
     923       (match op with
    924924        | Add ->
    925925          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    936936        | Or ->
    937937          (match Bool.orb
    938                    (Bool.andb (Nat.eqb (ByteValues.part_no p3) Nat.O)
    939                      (Nat.eqb (ByteValues.part_no p4) (Nat.S Nat.O)))
    940                    (Bool.andb (Nat.eqb (ByteValues.part_no p3) (Nat.S Nat.O))
    941                      (Nat.eqb (ByteValues.part_no p4) Nat.O)) with
     938                   (Bool.andb (Nat.eqb (ByteValues.part_no p1) Nat.O)
     939                     (Nat.eqb (ByteValues.part_no p2) (Nat.S Nat.O)))
     940                   (Bool.andb (Nat.eqb (ByteValues.part_no p1) (Nat.S Nat.O))
     941                     (Nat.eqb (ByteValues.part_no p2) Nat.O)) with
    942942           | Bool.True ->
    943943             let eq_at = fun p ptr1 ptr2 ->
     
    954954                     (ByteValues.part_no p)))
    955955             in
    956              (match Bool.andb (eq_opt (eq_at p3) ptr1_opt ptr1_opt')
    957                       (eq_opt (eq_at p4) ptr2_opt ptr2_opt') with
     956             (match Bool.andb (eq_opt (eq_at p1) ptr1_opt ptr1_opt')
     957                      (eq_opt (eq_at p2) ptr2_opt ptr2_opt') with
    958958              | Bool.True ->
    959959                Obj.magic
     
    973973            List.Nil)))
    974974     | ByteValues.BVByte b2 ->
    975        (match op4 with
     975       (match op with
    976976        | Add ->
    977977          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    10161016         List.Nil))
    10171017     | ByteValues.BVnonzero ->
    1018        (match op4 with
     1018       (match op with
    10191019        | Add ->
    10201020          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    10461046           (fun carry0 ->
    10471047           let { Types.fst = result; Types.snd = carry1 } =
    1048              eval0.op3 carry0 op4 b1 b2
     1048             eval0.op3 carry0 op b1 b2
    10491049           in
    10501050           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     
    10551055         List.Nil))
    10561056     | ByteValues.BVptr (x, x0) ->
    1057        (match op4 with
     1057       (match op with
    10581058        | Add ->
    10591059          be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a2 b1
     
    10741074       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    10751075         List.Nil)))
    1076   | ByteValues.BVnull p3 ->
     1076  | ByteValues.BVnull p1 ->
    10771077    (match a2 with
    10781078     | ByteValues.BVundef ->
     
    10881088       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    10891089         List.Nil))
    1090      | ByteValues.BVnull p4 ->
    1091        (match op4 with
     1090     | ByteValues.BVnull p2 ->
     1091       (match op with
    10921092        | Add ->
    10931093          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    11061106            List.Nil))
    11071107        | Xor ->
    1108           (match Nat.eqb (ByteValues.part_no p3) (ByteValues.part_no p4) with
     1108          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
    11091109           | Bool.True ->
    11101110             Obj.magic
    11111111               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    1112                  (ByteValues.BVXor (Types.None, Types.None, p3)); Types.snd =
     1112                 (ByteValues.BVXor (Types.None, Types.None, p1)); Types.snd =
    11131113                 carry })
    11141114           | Bool.False ->
    11151115             Errors.Error (List.Cons ((Errors.MSG
    11161116               ErrorMessages.UnsupportedOp), List.Nil))))
    1117      | ByteValues.BVptr (ptr2, p4) ->
    1118        (match op4 with
     1117     | ByteValues.BVptr (ptr2, p2) ->
     1118       (match op with
    11191119        | Add ->
    11201120          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    11331133            List.Nil))
    11341134        | Xor ->
    1135           (match Nat.eqb (ByteValues.part_no p3) (ByteValues.part_no p4) with
     1135          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
    11361136           | Bool.True ->
    11371137             Obj.magic
    11381138               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    1139                  (ByteValues.BVXor (Types.None, (Types.Some ptr2), p3));
     1139                 (ByteValues.BVXor (Types.None, (Types.Some ptr2), p1));
    11401140                 Types.snd = carry })
    11411141           | Bool.False ->
     
    11451145       Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    11461146         List.Nil)))
    1147   | ByteValues.BVptr (ptr1, p3) ->
     1147  | ByteValues.BVptr (ptr1, p1) ->
    11481148    (match a2 with
    11491149     | ByteValues.BVundef ->
     
    11571157         List.Nil))
    11581158     | ByteValues.BVByte b2 ->
    1159        (match op4 with
     1159       (match op with
    11601160        | Add ->
    11611161          be_add_sub_byte Bool.True (ByteValues.BBbit Bool.False) a1 b2
     
    11711171          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
    11721172            List.Nil)))
    1173      | ByteValues.BVnull p4 ->
    1174        (match op4 with
     1173     | ByteValues.BVnull p2 ->
     1174       (match op with
    11751175        | Add ->
    11761176          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    11891189            List.Nil))
    11901190        | Xor ->
    1191           (match Nat.eqb (ByteValues.part_no p3) (ByteValues.part_no p4) with
     1191          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
    11921192           | Bool.True ->
    11931193             Obj.magic
    11941194               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    1195                  (ByteValues.BVXor ((Types.Some ptr1), Types.None, p3));
     1195                 (ByteValues.BVXor ((Types.Some ptr1), Types.None, p1));
    11961196                 Types.snd = carry })
    11971197           | Bool.False ->
    11981198             Errors.Error (List.Cons ((Errors.MSG
    11991199               ErrorMessages.UnsupportedOp), List.Nil))))
    1200      | ByteValues.BVptr (ptr2, p4) ->
    1201        (match op4 with
     1200     | ByteValues.BVptr (ptr2, p2) ->
     1201       (match op with
    12021202        | Add ->
    12031203          Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnsupportedOp),
     
    12121212                      (Pointers.eq_block ptr1.Pointers.pblock
    12131213                        ptr2.Pointers.pblock)
    1214                       (Nat.eqb (ByteValues.part_no p3)
    1215                         (ByteValues.part_no p4)) with
     1214                      (Nat.eqb (ByteValues.part_no p1)
     1215                        (ByteValues.part_no p2)) with
    12161216              | Bool.True ->
    12171217                Obj.magic
     
    12231223                      byte_at AST.size_pointer
    12241224                        (Pointers.offv ptr1.Pointers.poff)
    1225                         (ByteValues.part_no p3)
     1225                        (ByteValues.part_no p1)
    12261226                    in
    12271227                    let by2 =
    12281228                      byte_at AST.size_pointer
    12291229                        (Pointers.offv ptr2.Pointers.poff)
    1230                         (ByteValues.part_no p3)
     1230                        (ByteValues.part_no p1)
    12311231                    in
    12321232                    let { Types.fst = result; Types.snd = carry1 } =
     
    12491249            List.Nil))
    12501250        | Xor ->
    1251           (match Nat.eqb (ByteValues.part_no p3) (ByteValues.part_no p4) with
     1251          (match Nat.eqb (ByteValues.part_no p1) (ByteValues.part_no p2) with
    12521252           | Bool.True ->
    12531253             Obj.magic
    12541254               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    12551255                 (ByteValues.BVXor ((Types.Some ptr1), (Types.Some ptr2),
    1256                  p3)); Types.snd = carry })
     1256                 p1)); Types.snd = carry })
    12571257           | Bool.False ->
    12581258             Errors.Error (List.Cons ((Errors.MSG
Note: See TracChangeset for help on using the changeset viewer.