source: src/Cminor/initialisation.ma @ 2963

Last change on this file since 2963 was 2793, checked in by campbell, 8 years ago

Oops, gave fields wrong order during initialisation.

File size: 4.9 KB
RevLine 
[758]1
2(* Replace initialisation of global variables with equivalent Cminor code. *)
3
[2601]4include "Cminor/Cminor_syntax.ma".
[758]5include "common/Globalenvs.ma".
6
[880]7(* XXX having to specify the return type in the match is annoying. *)
[1872]8definition init_expr : init_data → option (𝚺t:typ. expr t) ≝
[758]9λinit.
[1872]10match init return λ_.option (𝚺t:typ. expr t) with
[1878]11[ Init_int8 i          ⇒ Some ? (mk_DPair ?? (ASTint I8 Unsigned) (Cst ? (Ointconst I8 Unsigned i)))
12| Init_int16 i         ⇒ Some ? (mk_DPair ?? (ASTint I16 Unsigned) (Cst ? (Ointconst I16 Unsigned i)))
13| Init_int32 i         ⇒ Some ? (mk_DPair ?? (ASTint I32 Unsigned) (Cst ? (Ointconst I32 Unsigned i)))
[2624]14(*| Init_float32 f       ⇒ None ? (*Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst F32 f)))*)
15| Init_float64 f       ⇒ None ? (*Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst F64 f)))*)*)
[758]16| Init_space n         ⇒ None ?
[2176]17| Init_null            ⇒ Some ? (mk_DPair ?? ASTptr (Op1 (ASTint I8 Unsigned) ? (Optrofint ??) (Cst ? (Ointconst I8 Unsigned (zero ?)))))
18| Init_addrof   id off ⇒ Some ? (mk_DPair ?? ASTptr (Cst ? (Oaddrsymbol id off)))
[758]19].
20
[2251]21(* None of the additional code introduces locals, labels or returns. *)
[1316]22definition stmt_inv : stmt → Prop ≝
[2251]23  stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s ∧ match s with [ St_return _ ⇒ False | _ ⇒ True ]).
[1401]24 
25discriminator option.
[1605]26discriminator DPair.
[1316]27
[758]28(* Produces a few extra skips - hopefully the compiler will optimise these
29   away. *)
30
[1316]31definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s ≝
[881]32λid,r,init,off.
[758]33match init_expr init with
34[ None ⇒ St_skip
35| Some x ⇒
[1872]36    match x with [ mk_DPair t e ⇒
[2176]37      St_store t (Cst ? (Oaddrsymbol id off)) e
[880]38    ]
[758]39].
[2252]40% /3/
[2624]41cases init in p; [ 5: | 6: #a #b | *: #a ] #p normalize in p;
[2252]42destruct;/4 by stmt_labels_mp, conj/
[1316]43qed.
[758]44
[1316]45definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝
[881]46λid,r,init.
[2793]47\snd (foldl ??
48  (λos,datum.
[758]49   let 〈off,s〉 ≝ os in
[961]50     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
[1605]51  〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init).
[2252]52[ % /3/
[2793]53| cut (stmt_inv St_skip) [ % /3/ ]
54  generalize in match St_skip;
55  generalize in match 0;
56  elim init
57  [ #off #s #H @H
58  | #h #t #IH #off #s #H whd in ⊢ (?(???%)); @breakup_pair @IH
[2252]59    %
60    [ /3/
[2793]61    | % [ @(pi2 … (init_datum …)) | @H ]
[2252]62    ]
[2793]63  ]
[1316]64] qed.
[758]65
[1316]66definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
67λvars. foldr ? (Σs:stmt. stmt_inv s)
[2252]68  (λvar,s. mk_Sig ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (mk_Sig ? (λx.stmt_inv x ) St_skip ?) vars.
69[ % [ /3/ | % [ @(pi2 … s) | @(pi2 … (init_var …)) ] ]
70| /4/
71] qed.
[758]72
[1316]73lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
74#s elim s //
[2252]75[ #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?);
[1316]76  >(IH1 H1) >(IH2 H2) @refl
[2252]77| #sz #sg #e #s1 #s2 #IH1 #IH2 * #_ * #H1 #H2 whd in ⊢ (??%?);
[1316]78  >(IH1 H1) >(IH2 H2) @refl
[2251]79| #l #s #IH * * * #_ *
[2252]80| #l #s #IH * #_ #H @(IH H)
[1316]81] qed.
82
[2319]83(* FIXME: we need to add a new initialisation function instead of augmenting
84   main, because this currently breaks a recursive main function. *)
85
86definition add_statement : costlabel → ident → (Σs:stmt. stmt_inv s) →
[758]87                              list (ident × (fundef internal_function)) →
88                              list (ident × (fundef internal_function)) ≝
[2319]89λcost,id,s. match s with [ mk_Sig s H ⇒
[758]90  map ??
91    (λidf.
92      let 〈id',f'〉 ≝ idf in
93      match ident_eq id id' with
94      [ inl _ ⇒
95          match f' with
96          [ Internal f ⇒ 〈id, Internal ? (mk_internal_function
[887]97                                           (f_return f)
[758]98                                           (f_params f)
99                                           (f_vars f)
[1631]100                                           (f_distinct f)
[758]101                                           (f_stacksize f)
[2319]102                                           (St_cost cost (St_seq s (f_body f)))
[1316]103                                           ?)〉
[758]104          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
105          ]
[1316]106      | inr _ ⇒ 〈id',f'〉 ]) ].
107%
[2252]108[ % //
109| %
[2319]110 [ % //
111 | % [ @(stmt_P_mp … H) #s * * #V #L #R %
[2252]112    [ @(stmt_vars_mp … V) #i #t *
113    | @(stmt_labels_mp … L) #l *
114    | cases s in R ⊢ %; // #x *
115    ]
116  | whd in match (labels_of ?); >(no_labels … H) @(f_inv f)
[1316]117  ]
[2319]118 ]
[1316]119] qed.
[758]120
[1139]121definition empty_vars : list (ident × region × (list init_data)) →
122                        list (ident × region × nat) ≝
123map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉,
124              size_init_data_list (\snd v)〉).
[758]125
[2319]126definition replace_init : costlabel → Cminor_program → Cminor_noinit_program ≝
127λcost,p.
[758]128  mk_program ??
[1224]129    (empty_vars (prog_vars ?? p))
[2319]130    (add_statement cost (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
[1599]131    (prog_main ?? p).
Note: See TracBrowser for help on using the repository browser.