Ignore:
Timestamp:
Dec 14, 2011, 1:18:30 PM (8 years ago)
Author:
sacerdot
Message:

Porting to last standard library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r1599 r1605  
    44include "Cminor/syntax.ma".
    55include "common/Globalenvs.ma".
    6 include "utilities/deppair.ma".
    76
    87(* XXX having to specify the return type in the match is annoying. *)
    9 definition init_expr : init_data → option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) ≝
     8definition init_expr : init_data → option (𝚺c:memory_chunk. expr (typ_of_memory_chunk c)) ≝
    109λinit.
    11 match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with
    12 [ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst I8 i)))
    13 | Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst I16 i)))
    14 | Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst I32 i)))
    15 | Init_float32 f       ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f)))
    16 | Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
     10match init return λ_.option (𝚺c:memory_chunk. expr (typ_of_memory_chunk c)) with
     11[ Init_int8 i          ⇒ Some ? (mk_DPair ?? Mint8unsigned (Cst ? (Ointconst I8 i)))
     12| Init_int16 i         ⇒ Some ? (mk_DPair ?? Mint16unsigned (Cst ? (Ointconst I16 i)))
     13| Init_int32 i         ⇒ Some ? (mk_DPair ?? Mint32 (Cst ? (Ointconst I32 i)))
     14| Init_float32 f       ⇒ Some ? (mk_DPair ?? Mfloat32 (Cst ? (Ofloatconst f)))
     15| Init_float64 f       ⇒ Some ? (mk_DPair ?? Mfloat64 (Cst ? (Ofloatconst f)))
    1716| Init_space n         ⇒ None ?
    18 | Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 (zero ?)))))
    19 | Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
     17| Init_null r          ⇒ Some ? (mk_DPair ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 (zero ?)))))
     18| Init_addrof r id off ⇒ Some ? (mk_DPair ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
    2019].
    2120
     
    2524 
    2625discriminator option.
    27 discriminator Sig.
     26discriminator DPair.
    2827
    2928(* Produces a few extra skips - hopefully the compiler will optimise these
     
    3534[ None ⇒ St_skip
    3635| Some x ⇒
    37     match x with [ dp chunk e ⇒
     36    match x with [ mk_DPair chunk e ⇒
    3837      St_store ? r chunk (Cst ? (Oaddrsymbol id off)) e
    3938    ]
     
    5049   let 〈off,s〉 ≝ os in
    5150     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
    52   〈0, dp ? (λx.stmt_inv x) St_skip ?〉 init).
     51  〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init).
    5352[ % //
    5453| elim init
    5554  [ % //
    56   | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ]
     55  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair whd in ⊢ (?%); % [ % [ % // | @(pi2 ? stmt_inv) ] | @IH ]
    5756] qed.
    5857
Note: See TracChangeset for help on using the changeset viewer.