Changeset 2249


Ignore:
Timestamp:
Jul 24, 2012, 7:40:13 PM (7 years ago)
Author:
campbell
Message:

Tweak Cminor invariant to be slightly more readable/extendable.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2232 r2249  
    15821582     (* merge Hlabel_wf with Hstmt_inv and eliminate right away *)
    15831583     @(stmt_P_mp … (stmt_P_conj … Hstmt_inv Hlabel_wf))
    1584      #s * #Hstmt_vars #Hstmt_labels @conj
     1584     #s * #Hstmt_vars #Hstmt_labels %
    15851585     [ 1: (* prove that variables are either parameters or locals *)
    15861586        @(stmt_vars_mp … Hstmt_vars) #i #t #H
  • src/Cminor/initialisation.ma

    r2232 r2249  
    100100  ]
    101101  ]
    102 | whd in ⊢ (?(λ_.??(?(λ_.???%)?))?); >(no_labels … H) @(f_inv f)
     102| whd in match (labels_of ?); >(no_labels … H) @(f_inv f)
    103103] qed.
    104104
  • src/Cminor/syntax.ma

    r2232 r2249  
    128128].
    129129
     130record 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
    130135record internal_function : Type[0] ≝
    131136{ f_return    : option typ
     
    137142     (* Ensure that variables appear in the params and vars list with the
    138143        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
    141145}.
    142146
Note: See TracChangeset for help on using the changeset viewer.