source: Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma @ 1087

Last change on this file since 1087 was 1087, checked in by campbell, 10 years ago

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

File size: 4.2 KB
Line 
1
2(* Replace initialisation of global variables with equivalent Cminor code. *)
3
4include "Cminor/syntax.ma".
5include "common/Globalenvs.ma".
6
7(* XXX having to specify the return type in the match is annoying. *)
8definition init_expr : init_data → option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) ≝
9λinit.
10match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with
11[ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst I8 i)))
12| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst I16 i)))
13| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst I32 i)))
14| Init_float32 f       ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f)))
15| Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
16| Init_space n         ⇒ None ?
17| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst I8 (zero ?)))))
18| Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
19].
20
21(* Produces a few extra skips - hopefully the compiler will optimise these
22   away. *)
23
24definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_vars s (λ_.False) ≝
25λid,r,init,off.
26match init_expr init with
27[ None ⇒ St_skip
28| Some x ⇒
29    match x with [ dp chunk e ⇒
30      St_store ? r chunk (Cst ? (Oaddrsymbol id off)) e
31    ]
32].
33//
34cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/
35qed.
36
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) ≝
52λid,r,init.
53\snd (foldr ??
54  (λdatum,os.
55   let 〈off,s〉 ≝ os in
56     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
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.
62
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.
68
69definition add_statement : ident → (Σs:stmt. stmt_vars s (λ_.False)) →
70                              list (ident × (fundef internal_function)) →
71                              list (ident × (fundef internal_function)) ≝
72λid,s. match s with [ dp s H ⇒
73  map ??
74    (λidf.
75      let 〈id',f'〉 ≝ idf in
76      match ident_eq id id' with
77      [ inl _ ⇒
78          match f' with
79          [ Internal f ⇒ 〈id, Internal ? (mk_internal_function
80                                           (f_return f)
81                                           (f_params f)
82                                           (f_vars f)
83                                           (f_stacksize f)
84                                           (St_seq s (f_body f))
85                                           ?)〉
86          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
87          ]
88      | inr _ ⇒ 〈id',f'〉 ]) ].
89whd %
90[ @(stmt_vars_mp … H) #i *
91| //
92] qed.
93
94definition empty_vars : list (ident × (list init_data) × region × unit) →
95                        list (ident × (list init_data) × region × unit) ≝
96map ?? (λv. 〈〈〈\fst (\fst (\fst v)),
97               [Init_space (size_init_data_list (\snd (\fst (\fst v))))]〉,
98              \snd (\fst v)〉,
99              \snd v〉).
100
101definition replace_init : Cminor_program → Cminor_program ≝
102λp.
103  mk_program ??
104    (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
105    (prog_main ?? p)
106    (empty_vars (prog_vars ?? p)).
107   
Note: See TracBrowser for help on using the repository browser.