Changeset 2624 for src/Cminor


Ignore:
Timestamp:
Feb 6, 2013, 6:39:21 PM (7 years ago)
Author:
campbell
Message:

Properly evict unused and axiomatised Floats.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r2601 r2624  
    1212| Init_int16 i         ⇒ Some ? (mk_DPair ?? (ASTint I16 Unsigned) (Cst ? (Ointconst I16 Unsigned i)))
    1313| Init_int32 i         ⇒ Some ? (mk_DPair ?? (ASTint I32 Unsigned) (Cst ? (Ointconst I32 Unsigned i)))
    14 | Init_float32 f       ⇒ None ? (*Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst F32 f)))*)
    15 | Init_float64 f       ⇒ None ? (*Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst F64 f)))*)
     14(*| Init_float32 f       ⇒ None ? (*Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst F32 f)))*)
     15| Init_float64 f       ⇒ None ? (*Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst F64 f)))*)*)
    1616| Init_space n         ⇒ None ?
    1717| Init_null            ⇒ Some ? (mk_DPair ?? ASTptr (Op1 (ASTint I8 Unsigned) ? (Optrofint ??) (Cst ? (Ointconst I8 Unsigned (zero ?)))))
     
    3939].
    4040% /3/
    41 cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p;
     41cases init in p; [ 5: | 6: #a #b | *: #a ] #p normalize in p;
    4242destruct;/4 by stmt_labels_mp, conj/
    4343qed.
Note: See TracChangeset for help on using the changeset viewer.