Changeset 2582 for src/common


Ignore:
Timestamp:
Jan 15, 2013, 3:58:12 PM (7 years ago)
Author:
garnier
Message:

Some progress on CL to CM.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r2468 r2582  
    6666  | Ocmpu: ∀sz,sg'.   comparison -> binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint I8 sg') (**r integer unsigned comparison *)
    6767(*  | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') *) (**r float comparison *)
    68   | Oaddp: ∀sz.    binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r add an integer to a pointer *)
     68  | Oaddpi: ∀sz.   binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r add an integer to a pointer *)
     69  | Oaddip: ∀sz.   binary_operation  (ASTint sz Signed)  ASTptr                ASTptr              (**r add an integer to a pointer *)
    6970  | Osubpi: ∀sz.   binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r subtract int from a pointers *)
    70   | Osubpp: ∀sz.   binary_operation  ASTptr               ASTptr              (ASTint sz Signed)   (**r subtract two pointers *)
     71  | Osubpp: ∀sz.   binary_operation  ASTptr               ASTptr              (ASTint sz Unsigned)   (**r subtract two pointers *)
    7172  | Ocmpp: ∀sg'. comparison → binary_operation ASTptr     ASTptr              (ASTint I8 sg').  (**r compare pointers *)
    7273
     
    213214
    214215(* NB: requires arguments to be presented pointer first. *)
    215 definition ev_addp ≝ λv1,v2: val.
     216definition ev_addpi ≝ λv1,v2: val.
    216217  match v1 with
    217218  [ Vptr ptr1 ⇒ match v2 with
     
    468469  | Ocmpu _ _ c ⇒ ev_cmpu c
    469470(*  | Ocmpf _ _ c ⇒ ev_cmpf c *)
    470   | Oaddp _ ⇒ ev_addp
     471  | Oaddpi _ ⇒ ev_addpi
     472  | Oaddip _ ⇒ (λx,y. ev_addpi y x)
    471473  | Osubpi _ ⇒ ev_subpi
    472474  | Osubpp sz ⇒ ev_subpp sz
     
    504506  whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct // *)
    505507(* pointers *)
    506 | 16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
     508| 16,18: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
    507509  whd in ⊢ (??%? → ?); [ 3,4: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
     510| 17: #sz  #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) % [ 2: #b #o ]
     511  whd in ⊢ (??%? → ?); [ 2: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
    508512| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
    509513  whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?); | ] #E destruct //
Note: See TracChangeset for help on using the changeset viewer.