source: extracted/initialisation.ml @ 2717

Last change on this file since 2717 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 5.6 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open CostLabel
6
7open FrontEndVal
8
9open Hide
10
11open ByteValues
12
13open GenMem
14
15open FrontEndMem
16
17open Proper
18
19open PositiveMap
20
21open Deqsets
22
23open Extralib
24
25open Lists
26
27open Identifiers
28
29open Integers
30
31open AST
32
33open Division
34
35open Exp
36
37open Arithmetic
38
39open Extranat
40
41open Vector
42
43open FoldStuff
44
45open BitVector
46
47open Z
48
49open BitVectorZ
50
51open Pointers
52
53open ErrorMessages
54
55open Option
56
57open Setoids
58
59open Monad
60
61open Positive
62
63open PreIdentifiers
64
65open Errors
66
67open Div_and_mod
68
69open Jmeq
70
71open Russell
72
73open Util
74
75open Bool
76
77open Relations
78
79open Nat
80
81open List
82
83open Hints_declaration
84
85open Core_notation
86
87open Pts
88
89open Logic
90
91open Types
92
93open Coqlib
94
95open Values
96
97open FrontEndOps
98
99open Cminor_syntax
100
101open Extra_bool
102
103open Globalenvs
104
105(** val init_expr :
106    AST.init_data -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option **)
107let init_expr = function
108| AST.Init_int8 i ->
109  Types.Some { Types.dpi1 = (AST.ASTint (AST.I8, AST.Unsigned)); Types.dpi2 =
110    (Cminor_syntax.Cst ((AST.ASTint (AST.I8, AST.Unsigned)),
111    (FrontEndOps.Ointconst (AST.I8, AST.Unsigned, i)))) }
112| AST.Init_int16 i ->
113  Types.Some { Types.dpi1 = (AST.ASTint (AST.I16, AST.Unsigned));
114    Types.dpi2 = (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Unsigned)),
115    (FrontEndOps.Ointconst (AST.I16, AST.Unsigned, i)))) }
116| AST.Init_int32 i ->
117  Types.Some { Types.dpi1 = (AST.ASTint (AST.I32, AST.Unsigned));
118    Types.dpi2 = (Cminor_syntax.Cst ((AST.ASTint (AST.I32, AST.Unsigned)),
119    (FrontEndOps.Ointconst (AST.I32, AST.Unsigned, i)))) }
120| AST.Init_space n -> Types.None
121| AST.Init_null ->
122  Types.Some { Types.dpi1 = AST.ASTptr; Types.dpi2 = (Cminor_syntax.Op1
123    ((AST.ASTint (AST.I8, AST.Unsigned)), AST.ASTptr, (FrontEndOps.Optrofint
124    (AST.I8, AST.Unsigned)), (Cminor_syntax.Cst ((AST.ASTint (AST.I8,
125    AST.Unsigned)), (FrontEndOps.Ointconst (AST.I8, AST.Unsigned,
126    (BitVector.zero (AST.bitsize_of_intsize AST.I8)))))))) }
127| AST.Init_addrof (id, off) ->
128  Types.Some { Types.dpi1 = AST.ASTptr; Types.dpi2 = (Cminor_syntax.Cst
129    (AST.ASTptr, (FrontEndOps.Oaddrsymbol (id, off)))) }
130
131(** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **)
132let option_jmdiscr x y =
133  Logic.eq_rect_Type2 x
134    (match x with
135     | Types.None -> Obj.magic (fun _ dH -> dH)
136     | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y
137
138(** val dPair_jmdiscr :
139    ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __ **)
140let dPair_jmdiscr x y =
141  Logic.eq_rect_Type2 x
142    (let { Types.dpi1 = a0; Types.dpi2 = a10 } = x in
143    Obj.magic (fun _ dH -> dH __ __)) y
144
145(** val init_datum :
146    AST.ident -> AST.region -> AST.init_data -> Nat.nat -> Cminor_syntax.stmt
147    Types.sig0 **)
148let init_datum id r init off =
149  (match init_expr init with
150   | Types.None -> (fun _ -> Cminor_syntax.St_skip)
151   | Types.Some x ->
152     (fun _ ->
153       (let { Types.dpi1 = t; Types.dpi2 = e0 } = x in
154       (fun _ -> Cminor_syntax.St_store (t, (Cminor_syntax.Cst (AST.ASTptr,
155       (FrontEndOps.Oaddrsymbol (id, off)))), e0))) __)) __
156
157(** val init_var :
158    AST.ident -> AST.region -> AST.init_data List.list -> Cminor_syntax.stmt
159    Types.sig0 **)
160let init_var id r init =
161  (List.foldr (fun datum os ->
162    let { Types.fst = off; Types.snd = s } = os in
163    { Types.fst = (Nat.plus off (Globalenvs.size_init_data datum));
164    Types.snd = (Cminor_syntax.St_seq
165    ((Types.pi1 (init_datum id r datum off)), s)) }) { Types.fst = Nat.O;
166    Types.snd = (Types.pi1 Cminor_syntax.St_skip) } init).Types.snd
167
168(** val init_vars :
169    ((AST.ident, AST.region) Types.prod, AST.init_data List.list) Types.prod
170    List.list -> Cminor_syntax.stmt Types.sig0 **)
171let init_vars vars =
172  List.foldr (fun var s -> Cminor_syntax.St_seq ((Types.pi1 s),
173    (Types.pi1
174      (init_var var.Types.fst.Types.fst var.Types.fst.Types.snd
175        var.Types.snd)))) Cminor_syntax.St_skip vars
176
177(** val add_statement :
178    CostLabel.costlabel -> AST.ident -> Cminor_syntax.stmt Types.sig0 ->
179    (AST.ident, Cminor_syntax.internal_function AST.fundef) Types.prod
180    List.list -> (AST.ident, Cminor_syntax.internal_function AST.fundef)
181    Types.prod List.list **)
182let add_statement cost id s =
183  let s0 = s in
184  List.map (fun idf ->
185    let { Types.fst = id'; Types.snd = f' } = idf in
186    (match AST.ident_eq id id' with
187     | Types.Inl _ ->
188       (match f' with
189        | AST.Internal f ->
190          { Types.fst = id; Types.snd = (AST.Internal
191            { Cminor_syntax.f_return = f.Cminor_syntax.f_return;
192            Cminor_syntax.f_params = f.Cminor_syntax.f_params;
193            Cminor_syntax.f_vars = f.Cminor_syntax.f_vars;
194            Cminor_syntax.f_stacksize = f.Cminor_syntax.f_stacksize;
195            Cminor_syntax.f_body = (Cminor_syntax.St_cost (cost,
196            (Cminor_syntax.St_seq (s0, f.Cminor_syntax.f_body)))) }) }
197        | AST.External f -> { Types.fst = id; Types.snd = (AST.External f) })
198     | Types.Inr _ -> { Types.fst = id'; Types.snd = f' }))
199
200(** val empty_vars :
201    ((AST.ident, AST.region) Types.prod, AST.init_data List.list) Types.prod
202    List.list -> ((AST.ident, AST.region) Types.prod, Nat.nat) Types.prod
203    List.list **)
204let empty_vars =
205  List.map (fun v -> { Types.fst = { Types.fst = v.Types.fst.Types.fst;
206    Types.snd = v.Types.fst.Types.snd }; Types.snd =
207    (Globalenvs.size_init_data_list v.Types.snd) })
208
209(** val replace_init :
210    CostLabel.costlabel -> Cminor_syntax.cminor_program ->
211    Cminor_syntax.cminor_noinit_program **)
212let replace_init cost p =
213  { AST.prog_vars = (empty_vars p.AST.prog_vars); AST.prog_funct =
214    (add_statement cost p.AST.prog_main (init_vars p.AST.prog_vars)
215      p.AST.prog_funct); AST.prog_main = p.AST.prog_main }
216
Note: See TracBrowser for help on using the repository browser.