Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (8 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

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

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

    r1102 r1153  
    5454] qed.
    5555
    56 definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_inv s ≝
     56definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
    5757λvars. foldr ? (Σs:stmt. stmt_inv s)
    58   (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
     58  (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
    5959% [ % [ % // | @(use_sig ? stmt_inv) ] | @(use_sig ? stmt_inv) ]
    6060qed.
     
    102102] qed.
    103103
    104 definition empty_vars : list (ident × (list init_data) × region × unit) →
    105                         list (ident × (list init_data) × region × unit) ≝
    106 map ?? (λv. 〈〈〈\fst (\fst (\fst v)),
    107                [Init_space (size_init_data_list (\snd (\fst (\fst v))))]〉,
    108               \snd (\fst v)〉,
    109               \snd v〉).
     104definition empty_vars : list (ident × region × (list init_data)) →
     105                        list (ident × region × nat) ≝
     106map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉,
     107              size_init_data_list (\snd v)〉).
    110108
    111 definition replace_init : Cminor_program → Cminor_program ≝
     109definition replace_init : Cminor_program → Cminor_noinit_program ≝
    112110λp.
    113111  mk_program ??
Note: See TracChangeset for help on using the changeset viewer.