Changeset 2468 for src/common/Values.ma


Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (7 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Values.ma

    r2176 r2468  
    1818
    1919include "utilities/Coqlib.ma".
    20 include "common/Floats.ma".
     20(*include "common/Floats.ma".*)
    2121include "common/Errors.ma".
    2222include "common/Pointers.ma".
     
    2525(* * A value is either:
    2626- a machine integer;
    27 - a floating-point number;
     27- /* a floating-point number; */ No more
    2828- a pointer: a triple giving the representation of the pointer (in terms of the
    2929             memory regions such a pointer could address), a memory address and
     
    3737  | Vundef: val
    3838  | Vint: ∀sz:intsize. bvint sz → val
    39   | Vfloat: float → val
     39(*  | Vfloat: float → val*)
    4040  | Vnull: (*region →*) val
    4141  | Vptr: pointer → val.
     
    5252inductive val_typ : val → typ → Prop ≝
    5353  | VTint: ∀sz,sg,i. val_typ (Vint sz i) (ASTint sz sg)
    54   | VTfloat: ∀sz,f. val_typ (Vfloat f) (ASTfloat sz)
     54(*  | VTfloat: ∀sz,f. val_typ (Vfloat f) (ASTfloat sz)*)
    5555  | VTnull: val_typ Vnull ASTptr
    5656  | VTptr: ∀b,o. val_typ (Vptr (mk_pointer b o)) ASTptr.
     
    109109  ].
    110110
     111(*
    111112definition negf : val → val ≝ λv.
    112113  match v with
     
    115116  ].
    116117
     118
    117119definition absf : val → val ≝ λv.
    118120  match v with
     
    121123  ].
    122124
     125
    123126definition intoffloat : intsize → val → val ≝ λsz,v.
    124127  match v with
     
    143146  [ Vint sz n ⇒ Vfloat (floatofintu ? n)
    144147  | _ ⇒ Vundef
    145   ].
     148  ]. *)
    146149
    147150definition notint : val → val ≝ λv.
     
    171174  ].
    172175
     176(*
    173177definition singleoffloat : val → val ≝ λv.
    174178  match v with
    175179  [ Vfloat f ⇒ Vfloat (singleoffloat f)
    176180  | _ ⇒ Vundef
    177   ].
     181  ]. *)
    178182
    179183(* TODO: add zero to null? *)
     
    334338  end.
    335339*)
     340
     341(*
    336342definition addf ≝ λv1,v2: val.
    337343  match v1 with
     
    360366    [ Vfloat f2 ⇒ Vfloat (Fdiv f1 f2)
    361367    | _ ⇒ Vundef ]
    362   | _ ⇒ Vundef ].
     368  | _ ⇒ Vundef ]. *)
    363369
    364370definition cmp_match : comparison → val ≝ λc.
     
    451457  | _ ⇒ Vundef ].
    452458
     459
     460(*
    453461definition cmpf ≝ λc: comparison. λsz:intsize. λv1,v2: val.
    454462  match v1 with
     
    456464    [ Vfloat f2 ⇒ of_bool (Fcmp c f1 f2)
    457465    | _ ⇒ Vundef ]
    458   | _ ⇒ Vundef ].
     466  | _ ⇒ Vundef ]. *)
    459467
    460468(* * [load_result] is used in the memory model (library [Mem])
     
    487495    | _ ⇒ Vundef
    488496    ]
    489   | Vfloat f ⇒
     497(*  | Vfloat f ⇒
    490498    match chunk with
    491499    [ ASTfloat sz ⇒ match sz with [ F32 ⇒ Vfloat(singleoffloat f) | F64 ⇒ Vfloat f ]
    492500    | _ ⇒ Vundef
    493     ]
     501    ] *)
    494502  | _ ⇒ Vundef
    495503  ].
     
    10801088  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
    10811089#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 #e3 cases chunk
    1082 [ #sz #sg | | #sz ] whd in ⊢ (?%?); //;
     1090[ #sz #sg | ] whd in ⊢ (?%?); //;
    10831091qed.
    10841092
Note: See TracChangeset for help on using the changeset viewer.