Changeset 1605 for src/Clight


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

Porting to last standard library of Matita.

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r1566 r1605  
    719719  (REACTIVE: ∀tr,s1,e1.
    720720    execution_isteps tr s e s1 e1 →
    721     (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)))
     721    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
    722722  : traceinf' ≝ ?.
    723723lapply (REACTIVE E0 s e (isteps_none …));
     
    739739let corec reactive_traceinf'' ge s e
    740740  (EXEC:exec_from ge s e)
    741   (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
     741  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    742742  (REACTIVE: ∀tr,s1,e1.
    743743    execution_isteps tr s e s1 e1 →
    744     (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)))
     744    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
    745745  : traceinf' ≝ ?.
    746746cases REACTIVE0; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H
     
    771771let corec show_reactive' ge s e
    772772  (EXEC:exec_from ge s e)
    773   (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
     773  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    774774  (REACTIVE: ∀tr1,s1,e1.
    775775    execution_isteps tr1 s e s1 e1 →
    776     (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)))
     776    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
    777777  : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?.
    778778(*>(unroll_traceinf' (reactive_traceinf'' …)) *)
     
    791791  ∀REACTIVE:∀tr,s1,e1.
    792792    execution_isteps tr s e s1 e1 →
    793     (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)).
     793    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0).
    794794  execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC ? REACTIVE)) s e.
    795795[ #ge #s #e #EXEC #REACTIVE
  • 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.