Ignore:
Timestamp:
Dec 10, 2012, 2:33:40 PM (7 years ago)
Author:
tranquil
Message:

in BackEndOps?, cleaner def of be_op2
new statement of fetch_statement_sigma_commute and first part of further lemmas

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/BackEndOps.ma

    r2462 r2548  
    221221    ]
    222222  | BVnull p1 ⇒
    223     match op with
    224     [ Xor
    225       match a2 with
    226       [ BVptr ptr2 p2
     223    match a2 with
     224    [ BVptr ptr2 p2
     225      match op with
     226      [ Xor
    227227        if eqb p1 p2 then
    228228          return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉
    229229        else
    230230          Error … [MSG UnsupportedOp]
    231       | BVnull p2 ⇒
     231      | _ ⇒ Error … [MSG UnsupportedOp]
     232      ]
     233    | BVnull p2 ⇒
     234      match op with
     235      [ Xor ⇒
    232236        if eqb p1 p2 then
    233237          return 〈BVXor (None ?) (None ?) p1, carry〉
     
    239243    ]
    240244  | BVXor ptr1_opt ptr1_opt' p1 ⇒
    241     match op with
    242     [ Or
    243       match a2 with
    244       [ BVByte b2
     245    match a2 with
     246    [ BVByte b2
     247      match op with
     248      [ Or
    245249        if eq_bv … (bv_zero …) b2 then return 〈a1, carry〉
    246250        else Error … [MSG UnsupportedOp]
    247       | BVnonzero ⇒ return 〈BVnonzero, carry〉
    248       | BVXor ptr2_opt ptr2_opt' p2 ⇒
     251      | _ ⇒ Error … [MSG UnsupportedOp]
     252      ]
     253    | BVnonzero ⇒
     254      match op with
     255      [ Or ⇒
     256        return 〈BVnonzero, carry〉
     257      | _ ⇒ Error … [MSG UnsupportedOp]
     258      ]
     259    | BVXor ptr2_opt ptr2_opt' p2 ⇒
     260      match op with
     261      [ Or ⇒
    249262        if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then
    250263          let eq_at ≝ λp,ptr1,ptr2.
     
    262275    ]
    263276  | BVnonzero ⇒
    264     match op with
    265     [ Or ⇒
    266       match a2 with
    267       [ BVByte _ ⇒ return 〈BVnonzero, carry〉
    268       | BVnonzero ⇒ return 〈BVnonzero, carry〉
    269       | BVXor _ _ _ ⇒ return 〈BVnonzero, carry〉
     277    match a2 with
     278    [ BVByte _ ⇒
     279      match op with
     280      [ Or ⇒ return 〈BVnonzero, carry〉
     281      | _ ⇒ Error … [MSG UnsupportedOp]
     282      ]
     283    | BVnonzero ⇒
     284      match op with
     285      [ Or ⇒ return 〈BVnonzero, carry〉
     286      | _ ⇒ Error … [MSG UnsupportedOp]
     287      ]
     288    | BVXor _ _ _ ⇒
     289      match op with
     290      [ Or ⇒ return 〈BVnonzero, carry〉
    270291      | _ ⇒ Error … [MSG UnsupportedOp]
    271292      ]
Note: See TracChangeset for help on using the changeset viewer.