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/Clight/toCminor.ma

    r1516 r1605  
    22include "Clight/Csyntax.ma".
    33include "Clight/TypeComparison.ma".
    4 include "utilities/lists.ma".
    5 include "utilities/deppair.ma".
     4include "basics/lists/list.ma".
    65
    76(* Identify local variables that must be allocated memory. *)
     
    427426    ]
    428427| _ ⇒ λ_. Error ? (msg TypeMismatch)
    429 ]. whd @use_sig qed.
     428]. whd normalize nodelta @pi2
     429qed.
    430430
    431431lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.
     
    467467      [ ASTptr r ⇒ λe1'.
    468468          match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with
    469           [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (eject … e1'), ?»
     469          [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (pi1 … e1'), ?»
    470470          | By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1';
    471471                                  OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉
     
    479479      [ ASTptr r ⇒
    480480          match e1' with
    481           [ dp r1 e1' ⇒ region_should_eq r1 r ? e1'
     481          [ mk_DPair r1 e1' ⇒ region_should_eq r1 r ? e1'
    482482          ]
    483483      | _ ⇒ Error ? (msg TypeMismatch)
     
    541541          do e1' ← translate_addr vars e1;
    542542          match e1' with
    543           [ dp r e1' ⇒
     543          [ mk_DPair r e1' ⇒
    544544            do off ← field_offset id fl;
    545545            match access_mode ty with
     
    552552          do e1' ← translate_addr vars e1;
    553553          match e1' with
    554           [ dp r e1' ⇒
     554          [ mk_DPair r e1' ⇒
    555555            match access_mode ty return λx. access_mode ty = x → res ? with
    556556            [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?»
     
    590590          do off ← field_offset id fl;
    591591          match e1' with
    592           [ dp r e1'' ⇒ OK (Σr:region.Σe:CMexpr (ASTptr r).?) («r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» »)
     592          [ mk_DPair r e1'' ⇒ OK (Σr:region.Σe:CMexpr (ASTptr r).?) («r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» »)
    593593          ]
    594594      | Tunion _ _ ⇒ translate_addr vars e1
Note: See TracChangeset for help on using the changeset viewer.