source: extracted/initialisation.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 5.6 KB
Line 
1open Preamble
2
3open CostLabel
4
5open FrontEndVal
6
7open Hide
8
9open ByteValues
10
11open GenMem
12
13open FrontEndMem
14
15open Proper
16
17open PositiveMap
18
19open Deqsets
20
21open Extralib
22
23open Lists
24
25open Identifiers
26
27open Floats
28
29open Integers
30
31open AST
32
33open Division
34
35open Arithmetic
36
37open Extranat
38
39open Vector
40
41open FoldStuff
42
43open BitVector
44
45open Z
46
47open BitVectorZ
48
49open Pointers
50
51open Option
52
53open Setoids
54
55open Monad
56
57open Positive
58
59open Char
60
61open String
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_float32 f -> Types.None
121| AST.Init_float64 f -> Types.None
122| AST.Init_space n -> Types.None
123| AST.Init_null ->
124  Types.Some { Types.dpi1 = AST.ASTptr; Types.dpi2 = (Cminor_syntax.Op1
125    ((AST.ASTint (AST.I8, AST.Unsigned)), AST.ASTptr, (FrontEndOps.Optrofint
126    (AST.I8, AST.Unsigned)), (Cminor_syntax.Cst ((AST.ASTint (AST.I8,
127    AST.Unsigned)), (FrontEndOps.Ointconst (AST.I8, AST.Unsigned,
128    (BitVector.zero (AST.bitsize_of_intsize AST.I8)))))))) }
129| AST.Init_addrof (id, off) ->
130  Types.Some { Types.dpi1 = AST.ASTptr; Types.dpi2 = (Cminor_syntax.Cst
131    (AST.ASTptr, (FrontEndOps.Oaddrsymbol (id, off)))) }
132
133(** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **)
134let option_jmdiscr x y =
135  Logic.eq_rect_Type2 x
136    (match x with
137     | Types.None -> Obj.magic (fun _ dH -> dH)
138     | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y
139
140(** val dPair_jmdiscr :
141    ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __ **)
142let dPair_jmdiscr x y =
143  Logic.eq_rect_Type2 x
144    (let { Types.dpi1 = a0; Types.dpi2 = a10 } = x in
145    Obj.magic (fun _ dH -> dH __ __)) y
146
147(** val init_datum :
148    AST.ident -> AST.region -> AST.init_data -> Nat.nat -> Cminor_syntax.stmt
149    Types.sig0 **)
150let init_datum id r init off =
151  (match init_expr init with
152   | Types.None -> (fun _ -> Cminor_syntax.St_skip)
153   | Types.Some x ->
154     (fun _ ->
155       (let { Types.dpi1 = t; Types.dpi2 = e0 } = x in
156       (fun _ -> Cminor_syntax.St_store (t, (Cminor_syntax.Cst (AST.ASTptr,
157       (FrontEndOps.Oaddrsymbol (id, off)))), e0))) __)) __
158
159(** val init_var :
160    AST.ident -> AST.region -> AST.init_data List.list -> Cminor_syntax.stmt
161    Types.sig0 **)
162let init_var id r init =
163  (List.foldr (fun datum os ->
164    let { Types.fst = off; Types.snd = s } = os in
165    { Types.fst = (Nat.plus off (Globalenvs.size_init_data datum));
166    Types.snd = (Cminor_syntax.St_seq
167    ((Types.pi1 (init_datum id r datum off)), s)) }) { Types.fst = Nat.O;
168    Types.snd = (Types.pi1 Cminor_syntax.St_skip) } init).Types.snd
169
170(** val init_vars :
171    ((AST.ident, AST.region) Types.prod, AST.init_data List.list) Types.prod
172    List.list -> Cminor_syntax.stmt Types.sig0 **)
173let init_vars vars =
174  List.foldr (fun var s -> Cminor_syntax.St_seq ((Types.pi1 s),
175    (Types.pi1
176      (init_var var.Types.fst.Types.fst var.Types.fst.Types.snd
177        var.Types.snd)))) Cminor_syntax.St_skip vars
178
179(** val add_statement :
180    CostLabel.costlabel -> AST.ident -> Cminor_syntax.stmt Types.sig0 ->
181    (AST.ident, Cminor_syntax.internal_function AST.fundef) Types.prod
182    List.list -> (AST.ident, Cminor_syntax.internal_function AST.fundef)
183    Types.prod List.list **)
184let add_statement cost id s =
185  let s0 = s in
186  List.map (fun idf ->
187    let { Types.fst = id'; Types.snd = f' } = idf in
188    (match AST.ident_eq id id' with
189     | Types.Inl _ ->
190       (match f' with
191        | AST.Internal f ->
192          { Types.fst = id; Types.snd = (AST.Internal
193            { Cminor_syntax.f_return = f.Cminor_syntax.f_return;
194            Cminor_syntax.f_params = f.Cminor_syntax.f_params;
195            Cminor_syntax.f_vars = f.Cminor_syntax.f_vars;
196            Cminor_syntax.f_stacksize = f.Cminor_syntax.f_stacksize;
197            Cminor_syntax.f_body = (Cminor_syntax.St_cost (cost,
198            (Cminor_syntax.St_seq (s0, f.Cminor_syntax.f_body)))) }) }
199        | AST.External f -> { Types.fst = id; Types.snd = (AST.External f) })
200     | Types.Inr _ -> { Types.fst = id'; Types.snd = f' }))
201
202(** val empty_vars :
203    ((AST.ident, AST.region) Types.prod, AST.init_data List.list) Types.prod
204    List.list -> ((AST.ident, AST.region) Types.prod, Nat.nat) Types.prod
205    List.list **)
206let empty_vars =
207  List.map (fun v -> { Types.fst = { Types.fst = v.Types.fst.Types.fst;
208    Types.snd = v.Types.fst.Types.snd }; Types.snd =
209    (Globalenvs.size_init_data_list v.Types.snd) })
210
211(** val replace_init :
212    CostLabel.costlabel -> Cminor_syntax.cminor_program ->
213    Cminor_syntax.cminor_noinit_program **)
214let replace_init cost p =
215  { AST.prog_vars = (empty_vars p.AST.prog_vars); AST.prog_funct =
216    (add_statement cost p.AST.prog_main (init_vars p.AST.prog_vars)
217      p.AST.prog_funct); AST.prog_main = p.AST.prog_main }
218
Note: See TracBrowser for help on using the repository browser.