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

Last change on this file since 1087 was 1087, checked in by campbell, 9 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.