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/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.