Changeset 1605


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

Porting to last standard library of Matita.

Location:
src
Files:
6 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
  • 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
  • src/Cminor/semantics.ma

    r1603 r1605  
    235235
    236236(* TODO: perhaps should do a little type checking? *)
    237 let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Sig ? (λen:env. All ? (λit. present ?? en (\fst it)) ids)) ≝
     237let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids) ≝
    238238match vs with
    239239[ nil ⇒ match ids return λids.res (Σen. All ?? ids) with [ nil ⇒ OK ? «empty_map ??, ?» | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
  • src/Cminor/syntax.ma

    r1603 r1605  
    4242| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
    4343(* ident for returned value, expression to identify fn, args. *)
    44 | St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
    45 | St_tailcall : expr (ASTptr Code) → list (Σt. expr t) → stmt
     44| St_call : option ident → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
     45| St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt
    4646| St_seq : stmt → stmt → stmt
    4747| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
     
    5151(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
    5252| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
    53 | St_return : option (Σt. expr t) → stmt
     53| St_return : option (𝚺t. expr t) → stmt
    5454| St_label : identifier Label → stmt → stmt
    5555| St_goto : identifier Label → stmt
  • src/Cminor/toRTLabs.ma

    r1603 r1605  
    246246 match l return λx.All ? P x → B with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) (foldr_all A B P f b l (proj2 … H))] H.
    247247
    248 definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (present ?? env) ].
    249 
    250 definition choose_regs : ∀le. ∀env:env. ∀es:list (Σt:typ.expr t).
     248definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (present ?? env) ].
     249
     250definition choose_regs : ∀le. ∀env:env. ∀es:list (𝚺t:typ.expr t).
    251251                         ∀f:partial_fn le. All ? (exprtyp_present env) es →
    252252                         list register × (Σf':partial_fn le. fn_graph_included le f f') ≝
    253253λle,env,es,f,Env.
    254   foldr_all (DPair ? (λt:typ.expr t)) ??
     254  foldr_all (𝚺t:typ.expr t) ??
    255255    (λe,p,acc. let 〈rs,f〉 ≝ acc in
    256256             let 〈r,f'〉 ≝ match e return λe.? → ? with [ mk_DPair t e ⇒ λp.choose_reg le env t e (pi1 ?? f) ? ] p in
     
    401401] qed.
    402402
    403 let rec add_exprs (le:label_env) (env:env) (es:list (DPair ? (λt:typ.expr t))) (Env:All ? (exprtyp_present env) es)
    404                   (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le) on es: Sig ? (λf':partial_fn le. fn_graph_included le f f')
     403let rec add_exprs (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)
     404                  (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le) on es: Σf':partial_fn le. fn_graph_included le f f'
    405405match es return λes.All ?? es → |es|=|dsts| → ? with
    406406[ nil ⇒ λ_. match dsts return λx. ?=|x| → Σf':partial_fn le. fn_graph_included le f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
     
    506506qed.
    507507
    508 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env) (exits:Sig ? (λls:list label. All ? (present ?? (pf_graph ? f)) ls)) on s : res (Sig ? (λf':partial_fn label_env. add_stmt_inv label_env s f f')) ≝
    509 match s return λs.stmt_inv env label_env s → res (Sig ? (λf':partial_fn label_env. add_stmt_inv ? s f f')) with
     508let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env) (exits:Σls:list label. All ? (present ?? (pf_graph ? f)) ls) on s : res (Σf':partial_fn label_env. add_stmt_inv label_env s f f') ≝
     509match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env. add_stmt_inv ? s f f') with
    510510[ St_skip ⇒ λ_. OK ? «f, ?»
    511511| St_assign _ x e ⇒ λEnv.
     
    634634| 9,10: #l #H @(present_included … H) repeat @fn_includes_step @I
    635635| @(pi2 ?? (pf_entry ??))
    636 | @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | (*XXX@(stmt_labels_added ???? (pi2 ? (add_stmt_inv ???) ?))*) ]
     636| @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (pi2 ? (add_stmt_inv ???) ?)) ]
    637637| % [ @pi2 | @(pi2 ?? exits) ]
    638638| @(equal_Cminor_labels_added ?? s) [ @refl | (*XXX@(stmt_labels_added ???? (pi2 ? (add_stmt_inv ???) ?))*) ]
Note: See TracChangeset for help on using the changeset viewer.