Ignore:
Timestamp:
Jul 25, 2011, 2:58:10 PM (9 years ago)
Author:
campbell
Message:

Experimental branch where lookups of local variables in Cminor code always
succeed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma

    r961 r1087  
    2222   away. *)
    2323
    24 definition init_datum : ident → region → init_data → nat (*offset*) → stmt
     24definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_vars s (λ_.False)
    2525λid,r,init,off.
    2626match init_expr init with
     
    3131    ]
    3232].
     33//
     34cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/
     35qed.
    3336
    34 definition init_var : ident → region → list init_data → stmt ≝
     37lemma unpair : ∀A,B,C,D,x. ∀P:A → B → C. ∀Q:A → B → D.
     38  let 〈a,b〉 ≝ x in 〈P a b, Q a b〉 = 〈P (\fst x) (\snd x), Q (\fst x) (\snd x)〉.
     39#A #B #C #D * // qed.
     40
     41lemma sndredex : ∀A,B,C,D,x. ∀R:D → Prop. ∀P:A → C. ∀Q:A → B → D.
     42  R (Q (\fst x) (\snd x)) → R (\snd (let 〈a,b〉 ≝ x in 〈P a, Q a b〉)).
     43#A #B #C #D *; normalize /2/
     44qed.
     45
     46lemma sig_stmt_vars : ∀P:ident → Prop. ∀s:Σs:stmt.stmt_vars s P.
     47  stmt_vars s P.
     48#P * #s #p whd in ⊢ (?%?) //
     49qed.
     50
     51definition init_var : ident → region → list init_data → Σs:stmt. stmt_vars s (λ_.False) ≝
    3552λid,r,init.
    3653\snd (foldr ??
     
    3855   let 〈off,s〉 ≝ os in
    3956     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
    40   〈0, St_skip〉 init).
     57  〈0, dp ? (λx.stmt_vars x (λ_.False)) St_skip ?〉 init).
     58[ whd //
     59| elim init whd //
     60  #h #t #IH whd in ⊢ (?(???%)?) @sndredex whd % [ @sig_stmt_vars | @IH ]
     61] qed.
    4162
    42 definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
    43 λvars. foldr ??
    44   (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) St_skip vars.
     63definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_vars s (λ_.False) ≝
     64λvars. foldr ? (Σs:stmt. stmt_vars s (λ_.False))
     65  (λvar,s. dp ? (λx.stmt_vars x (λ_.False)) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_vars x (λ_.False)) St_skip I) vars.
     66whd % @sig_stmt_vars
     67qed.
    4568
    46 definition add_statement : ident → stmt
     69definition add_statement : ident → (Σs:stmt. stmt_vars s (λ_.False))
    4770                              list (ident × (fundef internal_function)) →
    4871                              list (ident × (fundef internal_function)) ≝
    49 λid,s.
     72λid,s. match s with [ dp s H ⇒
    5073  map ??
    5174    (λidf.
     
    5982                                           (f_vars f)
    6083                                           (f_stacksize f)
    61                                            (St_seq s (f_body f)))〉
     84                                           (St_seq s (f_body f))
     85                                           ?)〉
    6286          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
    6387          ]
    64       | inr _ ⇒ 〈id',f'〉 ]).
     88      | inr _ ⇒ 〈id',f'〉 ]) ].
     89whd %
     90[ @(stmt_vars_mp … H) #i *
     91| //
     92] qed.
    6593
    6694definition empty_vars : list (ident × (list init_data) × region × unit) →
Note: See TracChangeset for help on using the changeset viewer.