Changeset 2249
 Timestamp:
 Jul 24, 2012, 7:40:13 PM (9 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r2232 r2249 1582 1582 (* merge Hlabel_wf with Hstmt_inv and eliminate right away *) 1583 1583 @(stmt_P_mp … (stmt_P_conj … Hstmt_inv Hlabel_wf)) 1584 #s * #Hstmt_vars #Hstmt_labels @conj1584 #s * #Hstmt_vars #Hstmt_labels % 1585 1585 [ 1: (* prove that variables are either parameters or locals *) 1586 1586 @(stmt_vars_mp … Hstmt_vars) #i #t #H 
src/Cminor/initialisation.ma
r2232 r2249 100 100 ] 101 101 ] 102  whd in ⊢ (?(λ_.??(?(λ_.???%)?))?); >(no_labels … H) @(f_inv f)102  whd in match (labels_of ?); >(no_labels … H) @(f_inv f) 103 103 ] qed. 104 104 
src/Cminor/syntax.ma
r2232 r2249 128 128 ]. 129 129 130 record cminor_stmt_inv (env:list (ident × typ)) (labels:list (identifier Label)) (s:stmt) : Prop ≝ { 131 cm_inv_var : stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) env) s; 132 cm_inv_labels : stmt_labels (λl.Exists ? (λl'.l' = l) labels) s 133 }. 134 130 135 record internal_function : Type[0] ≝ 131 136 { f_return : option typ … … 137 142 (* Ensure that variables appear in the params and vars list with the 138 143 correct typ; and that all goto labels used are declared. *) 139 ; f_inv : stmt_P (λs.stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) (f_params @ f_vars)) s ∧ 140 stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body 144 ; f_inv : stmt_P (cminor_stmt_inv (f_params @ f_vars) (labels_of f_body)) f_body 141 145 }. 142 146
Note: See TracChangeset
for help on using the changeset viewer.