Ignore:
Timestamp:
Aug 30, 2011, 12:47:18 PM (9 years ago)
Author:
campbell
Message:

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r961 r1139  
    4040  〈0, St_skip〉 init).
    4141
    42 definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
     42definition init_vars : list (ident × region × (list init_data)) → stmt ≝
    4343λvars. foldr ??
    44   (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) St_skip vars.
     44  (λvar,s. St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) St_skip vars.
    4545
    4646definition add_statement : ident → stmt →
     
    6464      | inr _ ⇒ 〈id',f'〉 ]).
    6565
    66 definition empty_vars : list (ident × (list init_data) × region × unit) →
    67                         list (ident × (list init_data) × region × unit) ≝
    68 map ?? (λv. 〈〈〈\fst (\fst (\fst v)),
    69                [Init_space (size_init_data_list (\snd (\fst (\fst v))))]〉,
    70               \snd (\fst v)〉,
    71               \snd v〉).
     66definition empty_vars : list (ident × region × (list init_data)) →
     67                        list (ident × region × nat) ≝
     68map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉,
     69              size_init_data_list (\snd v)〉).
    7270
    73 definition replace_init : Cminor_program → Cminor_program ≝
     71definition replace_init : Cminor_program → Cminor_noinit_program ≝
    7472λp.
    7573  mk_program ??
Note: See TracChangeset for help on using the changeset viewer.